Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 2999 next slice time: 125
ott-1_20_bd=off:bs=off:drc=off:lcm=predicate:nwc=3:sio=off:spl=off:sp=reverse_arity_113 on FEQ073

WATCH: 0.00 CPU 0.01 WC

WATCH: 3.00 CPU 3.02 WC

WATCH: 6.01 CPU 6.03 WC

WATCH: 9.02 CPU 9.05 WC
Refutation found. Thanks to Tanya!
% SZS status Theorem for FEQ073
% SZS output start Proof for FEQ073
337272. $false (19:0) [trivial inequality removal 337034]
337034. star(a) != star(a) (19:5) [superposition 53,335696]
335696. addition(star(X1),multiplication(X1,multiplication(X1,multiplication(X1,X1)))) = star(X1) (18:13) [forward demodulation 335695,37]
37. multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)) (0:11) [cnf transformation 14]
14. ! [X0,X1,X2] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2))[input]
335695. addition(star(X1),multiplication(multiplication(X1,X1),multiplication(X1,X1))) = star(X1) (18:13) [forward demodulation 335051,147968]
147968. addition(star(X51),star(multiplication(X51,X51))) = star(X51) (16:10) [forward demodulation 147967,33]
33. addition(X0,X1) = addition(X1,X0) (0:7) [cnf transformation 16]
16. ! [X0,X1] : addition(X0,X1) = addition(X1,X0)[input]
147967. addition(star(multiplication(X51,X51)),star(X51)) = star(X51) (16:10) [forward demodulation 147966,147394]
147394. multiplication(star(X0),star(multiplication(X0,X0))) = star(X0) (15:10) [resolution 147246,117470]
117470. ~leq(multiplication(X2,addition(one,X1)),X2) | multiplication(X2,star(X1)) = X2 (14:13) [superposition 115183,33]
115183. ~leq(multiplication(X0,addition(X1,one)),X0) | multiplication(X0,star(X1)) = X0 (13:13) [forward demodulation 115182,1537]
1537. multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1)) (1:11) [forward demodulation 1509,33]
1509. multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0) (1:11) [superposition 38,25]
25. multiplication(X0,one) = X0 (0:5) [cnf transformation 12]
12. ! [X0] : multiplication(X0,one) = X0[input]
38. multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) (0:13) [cnf transformation 3]
3. ! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))[input]
115182. ~leq(addition(X0,multiplication(X0,X1)),X0) | multiplication(X0,star(X1)) = X0 (13:13) [forward demodulation 115116,33]
115116. multiplication(X0,star(X1)) = X0 | ~leq(addition(multiplication(X0,X1),X0),X0) (13:13) [resolution 114908,40]
40. leq(multiplication(X2,star(X1)),X0) | ~leq(addition(multiplication(X0,X1),X2),X0) (0:13) [cnf transformation 21]
21. ! [X0,X1,X2] : (~leq(addition(multiplication(X0,X1),X2),X0) | leq(multiplication(X2,star(X1)),X0))[ennf transformation 15]
15. ! [X0,X1,X2] : (leq(addition(multiplication(X0,X1),X2),X0) => leq(multiplication(X2,star(X1)),X0))[input]
114908. ~leq(multiplication(X3,star(X2)),X3) | multiplication(X3,star(X2)) = X3 (12:12) [forward demodulation 114907,1241]
1241. addition(one,star(X12)) = star(X12) (3:7) [superposition 69,1154]
1154. addition(one,addition(star(X2),multiplication(X2,star(X2)))) = star(X2) (2:12) [forward demodulation 1132,386]
386. addition(X13,addition(X14,X12)) = addition(X13,addition(X12,X14)) (2:11) [superposition 84,78]
78. addition(X7,addition(X8,X9)) = addition(X9,addition(X7,X8)) (1:11) [superposition 36,33]
36. addition(addition(X2,X1),X0) = addition(X2,addition(X1,X0)) (0:11) [cnf transformation 20]
20. ! [X0,X1,X2] : addition(addition(X2,X1),X0) = addition(X2,addition(X1,X0))[rectify 7]
7. ! [X2,X1,X0] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2))[input]
84. addition(X4,addition(X5,X6)) = addition(X5,addition(X4,X6)) (1:11) [forward demodulation 70,36]
70. addition(X4,addition(X5,X6)) = addition(addition(X5,X4),X6) (1:11) [superposition 36,33]
1132. addition(one,addition(multiplication(X2,star(X2)),star(X2))) = star(X2) (2:12) [superposition 58,78]
58. addition(star(X0),addition(one,multiplication(X0,star(X0)))) = star(X0) (1:12) [forward demodulation 55,33]
55. addition(addition(one,multiplication(X0,star(X0))),star(X0)) = star(X0) (1:12) [resolution 31,35]
35. ~leq(X0,X1) | addition(X0,X1) = X1 (0:8) [cnf transformation 23]
23. ! [X0,X1] : ((addition(X0,X1) != X1 | leq(X0,X1)) & (~leq(X0,X1) | addition(X0,X1) = X1))[nnf transformation 9]
9. ! [X0,X1] : (addition(X0,X1) = X1 <=> leq(X0,X1))[input]
31. leq(addition(one,multiplication(X0,star(X0))),star(X0)) (0:9) [cnf transformation 10]
10. ! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0))[input]
69. addition(X2,X3) = addition(X2,addition(X2,X3)) (1:9) [superposition 36,27]
27. addition(X0,X0) = X0 (0:5) [cnf transformation 13]
13. ! [X0] : addition(X0,X0) = X0[input]
114907. multiplication(X3,addition(one,star(X2))) = X3 | ~leq(multiplication(X3,star(X2)),X3) (12:14) [forward demodulation 114784,1545]
1545. multiplication(X0,addition(X1,one)) = multiplication(X0,addition(one,X1)) (1:11) [forward demodulation 1514,1537]
1514. multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)) (1:11) [superposition 38,25]
114784. ~leq(multiplication(X3,star(X2)),X3) | multiplication(X3,addition(star(X2),one)) = X3 (12:14) [superposition 100253,1241]
100253. ~leq(multiplication(X2,addition(one,X1)),X2) | multiplication(X2,addition(X1,one)) = X2 (11:14) [superposition 4281,33]
4281. ~leq(multiplication(X6,addition(X7,one)),X6) | multiplication(X6,addition(X7,one)) = X6 (10:14) [forward demodulation 4280,1537]
4280. addition(X6,multiplication(X6,X7)) = X6 | ~leq(multiplication(X6,addition(X7,one)),X6) (10:14) [forward demodulation 4239,33]
4239. ~leq(multiplication(X6,addition(X7,one)),X6) | addition(multiplication(X6,X7),X6) = X6 (10:14) [superposition 3759,1537]
3759. ~leq(addition(X0,X1),X0) | addition(X1,X0) = X0 (9:10) [resolution 3732,35]
3732. leq(X5,X6) | ~leq(addition(X6,X5),X6) (8:8) [forward demodulation 3731,25]
3731. leq(X5,X6) | ~leq(addition(multiplication(X6,one),X5),X6) (8:10) [forward demodulation 3693,25]
3693. leq(multiplication(X5,one),X6) | ~leq(addition(multiplication(X6,one),X5),X6) (8:12) [superposition 40,3674]
3674. one = star(one) (7:4) [resolution 3598,3562]
3562. ~leq(one,one) | one = star(one) (4:7) [superposition 3528,27]
3528. ~leq(addition(one,X30),one) | one = star(X30) (3:9) [forward demodulation 3527,1241]
3527. addition(one,star(X30)) = one | ~leq(addition(one,X30),one) (3:11) [forward demodulation 3498,33]
3498. ~leq(addition(one,X30),one) | addition(star(X30),one) = one (3:11) [superposition 2621,28]
28. multiplication(one,X0) = X0 (0:5) [cnf transformation 5]
5. ! [X0] : multiplication(one,X0) = X0[input]
2621. ~leq(addition(one,multiplication(X0,X1)),X0) | addition(star(X1),X0) = X0 (2:13) [resolution 2610,35]
2610. leq(star(X24),X25) | ~leq(addition(one,multiplication(X25,X24)),X25) (1:11) [forward demodulation 2595,33]
2595. leq(star(X24),X25) | ~leq(addition(multiplication(X25,X24),one),X25) (1:11) [superposition 40,28]
3598. leq(one,one) (6:3) [superposition 59,3597]
3597. one = star(zero) (5:4) [subsumption resolution 3596,27]
3596. one = star(zero) | addition(one,one) != one (5:9) [resolution 3565,34]
34. leq(X0,X1) | addition(X0,X1) != X1 (0:8) [cnf transformation 23]
3565. ~leq(one,one) | one = star(zero) (4:7) [superposition 3528,26]
26. addition(X0,zero) = X0 (0:5) [cnf transformation 2]
2. ! [X0] : addition(X0,zero) = X0[input]
59. leq(one,star(zero)) (1:4) [forward demodulation 57,26]
57. leq(addition(one,zero),star(zero)) (1:6) [superposition 31,29]
29. zero = multiplication(zero,X0) (0:5) [cnf transformation 1]
1. ! [X0] : zero = multiplication(zero,X0)[input]
147246. leq(multiplication(star(X176),addition(one,multiplication(X176,X176))),star(X176)) (12:11) [forward demodulation 147245,130896]
130896. star(X20) = star(star(X20)) (16:6) [subsumption resolution 130895,27]
130895. addition(star(X20),star(X20)) != star(X20) | star(X20) = star(star(X20)) (16:14) [forward demodulation 130894,1277]
1277. addition(star(X2),X3) = addition(one,addition(star(X2),X3)) (4:11) [superposition 36,1241]
130894. addition(one,addition(star(X20),star(X20))) != star(X20) | star(X20) = star(star(X20)) (16:16) [forward demodulation 130852,84]
130852. addition(star(X20),addition(one,star(X20))) != star(X20) | star(X20) = star(star(X20)) (16:16) [superposition 6229,130272]
130272. multiplication(star(X27),star(X27)) = star(X27) (15:8) [subsumption resolution 130271,31]
130271. ~leq(addition(one,multiplication(X27,star(X27))),star(X27)) | multiplication(star(X27),star(X27)) = star(X27) (15:17) [forward demodulation 130270,1241]
130270. ~leq(addition(one,multiplication(X27,addition(one,star(X27)))),star(X27)) | multiplication(star(X27),star(X27)) = star(X27) (15:19) [forward demodulation 130216,1560]
1560. addition(X29,multiplication(X26,addition(X27,X28))) = addition(X29,multiplication(X26,addition(X28,X27))) (2:15) [forward demodulation 1530,1529]
1529. addition(X25,multiplication(X22,addition(X23,X24))) = addition(multiplication(X22,X24),addition(X25,multiplication(X22,X23))) (2:17) [superposition 78,38]
1530. addition(X29,multiplication(X26,addition(X27,X28))) = addition(multiplication(X26,X27),addition(X29,multiplication(X26,X28))) (2:17) [superposition 84,38]
130216. multiplication(star(X27),star(X27)) = star(X27) | ~leq(addition(one,multiplication(X27,addition(star(X27),one))),star(X27)) (15:19) [resolution 117492,2990]
2990. leq(star(X2),X3) | ~leq(addition(one,multiplication(X2,addition(X3,one))),X3) (8:13) [forward demodulation 2989,1537]
2989. ~leq(addition(one,addition(X2,multiplication(X2,X3))),X3) | leq(star(X2),X3) (8:13) [forward demodulation 2988,386]
2988. ~leq(addition(one,addition(multiplication(X2,X3),X2)),X3) | leq(star(X2),X3) (8:13) [forward demodulation 2973,84]
2973. leq(star(X2),X3) | ~leq(addition(multiplication(X2,X3),addition(one,X2)),X3) (8:13) [superposition 41,1684]
1684. multiplication(star(X0),addition(one,X0)) = star(X0) (7:9) [superposition 1631,33]
1631. multiplication(star(X12),addition(X12,one)) = star(X12) (6:9) [superposition 1537,1445]
1445. addition(star(X1),multiplication(star(X1),X1)) = star(X1) (5:10) [superposition 1205,1277]
1205. addition(one,addition(star(X2),multiplication(star(X2),X2))) = star(X2) (2:12) [forward demodulation 1184,386]
1184. addition(one,addition(multiplication(star(X2),X2),star(X2))) = star(X2) (2:12) [superposition 66,78]
66. addition(star(X0),addition(one,multiplication(star(X0),X0))) = star(X0) (1:12) [forward demodulation 63,33]
63. addition(addition(one,multiplication(star(X0),X0)),star(X0)) = star(X0) (1:12) [resolution 32,35]
32. leq(addition(one,multiplication(star(X0),X0)),star(X0)) (0:9) [cnf transformation 4]
4. ! [X0] : leq(addition(one,multiplication(star(X0),X0)),star(X0))[input]
41. leq(multiplication(star(X0),X2),X1) | ~leq(addition(multiplication(X0,X1),X2),X1) (0:13) [cnf transformation 22]
22. ! [X0,X1,X2] : (~leq(addition(multiplication(X0,X1),X2),X1) | leq(multiplication(star(X0),X2),X1))[ennf transformation 6]
6. ! [X0,X1,X2] : (leq(addition(multiplication(X0,X1),X2),X1) => leq(multiplication(star(X0),X2),X1))[input]
117492. ~leq(star(X24),star(X24)) | multiplication(star(X24),star(X24)) = star(X24) (14:13) [superposition 115183,1631]
6229. addition(X1,addition(one,multiplication(X1,X1))) != X1 | star(X1) = X1 (13:13) [forward demodulation 6213,33]
6213. star(X1) = X1 | addition(addition(one,multiplication(X1,X1)),X1) != X1 (13:13) [resolution 4601,34]
4601. ~leq(addition(one,multiplication(X0,X0)),X0) | star(X0) = X0 (12:11) [resolution 4545,2997]
2997. leq(star(X12),X13) | ~leq(addition(one,multiplication(X12,X13)),X13) (1:11) [forward demodulation 2980,33]
2980. leq(star(X12),X13) | ~leq(addition(multiplication(X12,X13),one),X13) (1:11) [superposition 41,25]
4545. ~leq(star(X44),X44) | star(X44) = X44 (11:8) [forward demodulation 4512,2094]
2094. addition(X17,star(X17)) = star(X17) (7:7) [forward demodulation 2093,1241]
2093. addition(X17,addition(one,star(X17))) = star(X17) (7:9) [forward demodulation 2092,386]
2092. addition(X17,addition(star(X17),one)) = star(X17) (7:9) [forward demodulation 2091,84]
2091. addition(star(X17),addition(X17,one)) = star(X17) (7:9) [forward demodulation 2090,33]
2090. addition(addition(X17,one),star(X17)) = star(X17) (7:9) [forward demodulation 2089,1631]
2089. multiplication(star(X17),addition(X17,one)) = addition(addition(X17,one),star(X17)) (7:13) [forward demodulation 2088,1241]
2088. multiplication(addition(one,star(X17)),addition(X17,one)) = addition(addition(X17,one),star(X17)) (7:15) [forward demodulation 2045,1606]
1606. multiplication(addition(X11,one),X10) = multiplication(addition(one,X11),X10) (1:11) [forward demodulation 1576,1601]
1601. multiplication(addition(X11,one),X10) = addition(X10,multiplication(X11,X10)) (1:11) [forward demodulation 1571,33]
1571. multiplication(addition(X11,one),X10) = addition(multiplication(X11,X10),X10) (1:11) [superposition 39,28]
39. multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) (0:13) [cnf transformation 8]
8. ! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))[input]
1576. multiplication(addition(one,X11),X10) = addition(X10,multiplication(X11,X10)) (1:11) [superposition 39,28]
2045. multiplication(addition(star(X17),one),addition(X17,one)) = addition(addition(X17,one),star(X17)) (7:15) [superposition 1601,1631]
4512. ~leq(star(X44),X44) | addition(X44,star(X44)) = X44 (11:10) [superposition 4293,2094]
4293. ~leq(addition(X38,X39),X38) | addition(X38,X39) = X38 (10:10) [forward demodulation 4292,77]
77. addition(X5,X6) = addition(X5,addition(X6,addition(X5,X6))) (1:11) [superposition 36,27]
4292. addition(X38,addition(X39,addition(X38,X39))) = X38 | ~leq(addition(X38,X39),X38) (10:14) [forward demodulation 4251,33]
4251. ~leq(addition(X38,X39),X38) | addition(addition(X39,addition(X38,X39)),X38) = X38 (10:14) [superposition 3759,77]
147245. leq(multiplication(star(star(X176)),addition(one,multiplication(X176,X176))),star(star(X176))) (12:13) [forward demodulation 147244,117806]
117806. star(star(X0)) = star(star(star(X0))) (16:8) [superposition 117795,1241]
117795. star(star(X59)) = star(addition(one,X59)) (15:8) [forward demodulation 117794,11219]
11219. addition(star(star(X47)),star(addition(one,X47))) = star(star(X47)) (9:12) [forward demodulation 11218,33]
11218. addition(star(addition(one,X47)),star(star(X47))) = star(star(X47)) (9:12) [subsumption resolution 11217,1808]
1808. leq(star(star(X3)),star(star(X3))) (9:7) [forward demodulation 1798,1241]
1798. leq(addition(one,star(star(X3))),star(star(X3))) (9:9) [superposition 32,1705]
1705. multiplication(star(star(X0)),star(X0)) = star(star(X0)) (8:10) [superposition 1684,1241]
11217. ~leq(star(star(X47)),star(star(X47))) | addition(star(addition(one,X47)),star(star(X47))) = star(star(X47)) (9:19) [forward demodulation 11157,1241]
11157. ~leq(addition(one,star(star(X47))),star(star(X47))) | addition(star(addition(one,X47)),star(star(X47))) = star(star(X47)) (9:21) [superposition 3001,11018]
11018. multiplication(addition(one,X0),star(star(X0))) = star(star(X0)) (8:11) [superposition 10931,33]
10931. multiplication(addition(X2,one),star(star(X2))) = star(star(X2)) (7:11) [superposition 2166,2192]
2192. multiplication(star(X0),star(star(X0))) = star(star(X0)) (6:10) [superposition 2162,1241]
2162. multiplication(addition(one,X0),star(X0)) = star(X0) (5:9) [superposition 2054,33]
2054. multiplication(addition(X13,one),star(X13)) = star(X13) (4:9) [superposition 1601,1266]
1266. addition(star(X22),multiplication(X22,star(X22))) = star(X22) (3:10) [forward demodulation 1265,69]
1265. addition(star(X22),addition(star(X22),multiplication(X22,star(X22)))) = star(X22) (3:13) [forward demodulation 1247,33]
1247. addition(addition(star(X22),multiplication(X22,star(X22))),star(X22)) = star(X22) (3:13) [superposition 92,1154]
92. addition(X2,X1) = addition(X1,addition(X2,X1)) (2:9) [superposition 69,33]
2166. multiplication(star(X0),X1) = multiplication(addition(X0,one),multiplication(star(X0),X1)) (5:13) [superposition 37,2054]
3001. ~leq(addition(one,multiplication(X0,X1)),X1) | addition(star(X0),X1) = X1 (2:13) [resolution 2997,35]
117794. addition(star(star(X59)),star(addition(one,X59))) = star(addition(one,X59)) (15:13) [subsumption resolution 117793,3049]
3049. leq(star(addition(one,X0)),star(addition(one,X0))) (3:9) [forward demodulation 3004,1719]
1719. multiplication(star(addition(one,X14)),addition(one,X14)) = star(addition(one,X14)) (8:13) [superposition 1684,69]
3004. leq(multiplication(star(addition(one,X0)),addition(one,X0)),star(addition(one,X0))) (3:13) [superposition 1907,33]
1907. leq(multiplication(star(addition(one,X26)),addition(X26,one)),star(addition(one,X26))) (2:13) [forward demodulation 1856,1651]
1651. multiplication(star(X47),addition(X48,one)) = addition(one,multiplication(star(X47),addition(X48,one))) (5:15) [superposition 1277,1537]
1856. leq(addition(one,multiplication(star(addition(one,X26)),addition(X26,one))),star(addition(one,X26))) (2:15) [superposition 32,1545]
117793. ~leq(star(addition(one,X59)),star(addition(one,X59))) | addition(star(star(X59)),star(addition(one,X59))) = star(addition(one,X59)) (15:22) [forward demodulation 117697,22959]
22959. addition(X10,star(addition(X10,X11))) = star(addition(X10,X11)) (9:11) [forward demodulation 22733,2094]
22733. addition(X10,addition(addition(X10,X11),star(addition(X10,X11)))) = star(addition(X10,X11)) (9:15) [superposition 2132,69]
2132. addition(X3,addition(X4,star(addition(X3,X4)))) = star(addition(X3,X4)) (8:13) [superposition 2094,36]
117697. ~leq(addition(one,star(addition(one,X59))),star(addition(one,X59))) | addition(star(star(X59)),star(addition(one,X59))) = star(addition(one,X59)) (15:24) [superposition 2621,117466]
117466. multiplication(star(addition(one,X2)),star(X2)) = star(addition(one,X2)) (14:12) [resolution 115183,1907]
147244. leq(multiplication(star(star(star(X176))),addition(one,multiplication(X176,X176))),star(star(star(X176)))) (12:15) [forward demodulation 147099,1545]
147099. leq(multiplication(star(star(star(X176))),addition(multiplication(X176,X176),one)),star(star(star(X176)))) (12:15) [superposition 141445,55581]
55581. addition(multiplication(X50,X50),star(star(X50))) = star(star(X50)) (11:11) [forward demodulation 54717,2864]
2864. addition(X12,star(star(X11))) = addition(X11,addition(X12,star(star(X11)))) (10:13) [superposition 84,2794]
2794. addition(X46,star(star(X46))) = star(star(X46)) (9:9) [superposition 2136,2094]
2136. addition(star(X3),X4) = addition(X3,addition(star(X3),X4)) (8:11) [superposition 36,2094]
54717. addition(X50,addition(multiplication(X50,X50),star(star(X50)))) = star(star(X50)) (11:13) [superposition 1635,31409]
31409. addition(star(star(X23)),multiplication(X23,addition(X23,one))) = star(star(X23)) (10:13) [forward demodulation 31242,33]
31242. addition(multiplication(X23,addition(X23,one)),star(star(X23))) = star(star(X23)) (10:13) [superposition 23005,26856]
26856. addition(star(X47),star(multiplication(X47,addition(X47,one)))) = star(X47) (9:12) [forward demodulation 26855,33]
26855. addition(star(multiplication(X47,addition(X47,one))),star(X47)) = star(X47) (9:12) [subsumption resolution 26798,32]
26798. ~leq(addition(one,multiplication(star(X47),X47)),star(X47)) | addition(star(multiplication(X47,addition(X47,one))),star(X47)) = star(X47) (9:21) [superposition 2621,18587]
18587. multiplication(star(X0),X0) = multiplication(star(X0),multiplication(X0,addition(X0,one))) (8:13) [superposition 1693,2050]
2050. multiplication(X0,addition(X0,one)) = multiplication(addition(X0,one),X0) (2:11) [superposition 1601,1537]
1693. multiplication(star(X9),X10) = multiplication(star(X9),multiplication(addition(X9,one),X10)) (7:13) [superposition 37,1631]
23005. addition(X73,star(addition(X74,star(X73)))) = star(addition(X74,star(X73))) (9:13) [forward demodulation 22753,2094]
22753. addition(X73,addition(addition(X74,star(X73)),star(addition(X74,star(X73))))) = star(addition(X74,star(X73))) (9:18) [superposition 2132,2141]
2141. addition(X12,star(X11)) = addition(X11,addition(X12,star(X11))) (8:11) [superposition 84,2094]
1635. addition(X13,multiplication(X11,addition(X12,one))) = addition(X11,addition(multiplication(X11,X12),X13)) (2:15) [superposition 78,1537]
141445. leq(multiplication(star(addition(X152,X153)),addition(X152,one)),star(addition(X152,X153))) (11:13) [forward demodulation 141444,130896]
141444. leq(multiplication(star(star(addition(X152,X153))),addition(X152,one)),star(star(addition(X152,X153)))) (11:15) [forward demodulation 141443,117806]
141443. leq(multiplication(star(star(star(addition(X152,X153)))),addition(X152,one)),star(star(star(addition(X152,X153))))) (11:17) [forward demodulation 141442,1651]
141442. leq(addition(one,multiplication(star(star(star(addition(X152,X153)))),addition(X152,one))),star(star(star(addition(X152,X153))))) (11:19) [forward demodulation 141441,1815]
1815. multiplication(star(star(X11)),addition(X12,one)) = multiplication(star(star(X11)),addition(X12,star(X11))) (9:16) [forward demodulation 1814,1537]
1814. multiplication(star(star(X11)),addition(X12,star(X11))) = addition(star(star(X11)),multiplication(star(star(X11)),X12)) (9:18) [forward demodulation 1803,33]
1803. multiplication(star(star(X11)),addition(X12,star(X11))) = addition(multiplication(star(star(X11)),X12),star(star(X11))) (9:18) [superposition 38,1705]
141441. leq(addition(one,multiplication(star(star(star(addition(X152,X153)))),addition(X152,star(star(addition(X152,X153)))))),star(star(star(addition(X152,X153))))) (11:23) [forward demodulation 140875,1560]
140875. leq(addition(one,multiplication(star(star(star(addition(X152,X153)))),addition(star(star(addition(X152,X153))),X152))),star(star(star(addition(X152,X153))))) (11:23) [superposition 1958,23366]
23366. addition(X75,star(star(addition(X75,X76)))) = star(star(addition(X75,X76))) (10:13) [superposition 22959,2132]
1958. leq(addition(one,multiplication(star(addition(X43,X44)),addition(X44,X43))),star(addition(X43,X44))) (2:15) [superposition 32,1553]
1553. multiplication(X5,addition(X6,X7)) = multiplication(X5,addition(X7,X6)) (1:11) [forward demodulation 1520,38]
1520. multiplication(X5,addition(X6,X7)) = addition(multiplication(X5,X7),multiplication(X5,X6)) (1:13) [superposition 38,33]
147966. multiplication(star(X51),star(multiplication(X51,X51))) = addition(star(multiplication(X51,X51)),star(X51)) (16:15) [forward demodulation 147965,1241]
147965. multiplication(addition(one,star(X51)),star(multiplication(X51,X51))) = addition(star(multiplication(X51,X51)),star(X51)) (16:17) [forward demodulation 147802,1606]
147802. multiplication(addition(star(X51),one),star(multiplication(X51,X51))) = addition(star(multiplication(X51,X51)),star(X51)) (16:17) [superposition 1601,147394]
335051. addition(star(X1),star(multiplication(X1,X1))) = addition(star(X1),multiplication(multiplication(X1,X1),multiplication(X1,X1))) (18:18) [superposition 148124,131355]
131355. addition(star(X46),multiplication(X46,X46)) = star(X46) (17:9) [forward demodulation 131040,50788]
50788. addition(star(X96),multiplication(X96,X97)) = addition(star(X96),multiplication(X96,addition(X97,one))) (9:15) [forward demodulation 50787,33]
50787. addition(star(X96),multiplication(X96,X97)) = addition(multiplication(X96,addition(X97,one)),star(X96)) (9:15) [forward demodulation 49982,33]
49982. addition(multiplication(X96,X97),star(X96)) = addition(multiplication(X96,addition(X97,one)),star(X96)) (9:15) [superposition 1632,2141]
1632. addition(multiplication(X4,addition(X5,one)),X6) = addition(X4,addition(multiplication(X4,X5),X6)) (2:15) [superposition 36,1537]
131040. addition(star(X46),multiplication(X46,addition(X46,one))) = star(X46) (17:11) [superposition 31409,130896]
148124. addition(star(X60),X61) = addition(star(X60),addition(star(multiplication(X60,X60)),X61)) (17:14) [superposition 36,147968]
53. addition(star(a),multiplication(a,multiplication(a,multiplication(a,a)))) != star(a) (1:13) [forward demodulation 52,33]
52. addition(multiplication(a,multiplication(a,multiplication(a,a))),star(a)) != star(a) (1:13) [resolution 34,24]
24. ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a)) (0:10) [cnf transformation 19]
19. ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))[flattening 18]
18. ~leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))[negated conjecture 17]
17. leq(multiplication(a,multiplication(a,multiplication(a,a))),star(a))[input]
% SZS output end Proof for FEQ073
------------------------------
Version: Vampire 1.8 (revision 1280)
Termination reason: Refutation

Active clauses: 974
Passive clauses: 19765
Generated clauses: 337085
Final active clauses: 974
Final passive clauses: 18791
Input formulas: 17
Initial clauses: 18

Trivial inequalities: 409
Fw subsumption resolutions: 1893
Fw demodulations: 212258

Simple tautologies: 2943
Equational tautologies: 2
Forward subsumptions: 96293
Fw demodulations to eq. taut.: 3285

Binary resolution: 4725
Forward superposition: 73181
Backward superposition: 44567
Self superposition: 193
Equality resolution: 5

Memory used [KB]: 221702
Time elapsed: 10.281 s
------------------------------
% Success in time 10.31 s

WATCH: 10.27 CPU 10.34 WC

FINAL WATCH: 10.27 CPU 10.34 WC