Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 3000 next slice time: 128
ott+4_7_bs=off:drc=off:fde=none:lcm=predicate:nwc=1.2:nicw=on:ptb=off:ssec=off:sgo=on:spl=backtracking_116 on FEQ061

WATCH: 0.00 CPU 0.01 WC

WATCH: 2.99 CPU 3.02 WC

WATCH: 6.01 CPU 6.03 WC

WATCH: 9.01 CPU 9.04 WC

WATCH: 12.02 CPU 12.05 WC
Time limit reached!
------------------------------
Version: Vampire 1.8 (revision 1280)
Termination reason: Time limit

Active clauses: 2179
Passive clauses: 38870
Generated clauses: 663372
Final active clauses: 1943
Final passive clauses: 29602
Input formulas: 27
Initial clauses: 28

Unused predicate definitions: 1
Splitted inequalities: 1

Fw demodulations: 310828
Bw demodulations: 4519

Forward subsumptions: 304650
Fw demodulations to eq. taut.: 9024
Bw demodulations to eq. taut.: 2806

Forward superposition: 185310
Backward superposition: 162444
Self superposition: 323

Memory used [KB]: 318161
Time elapsed: 12.968 s
------------------------------
% remaining time: 2869 next slice time: 402
ott+11_7_bs=off:cond=on:drc=off:ep=on:gsp=input_only:lcm=predicate:nwc=1.3:nicw=on:ptb=off:ssec=off:sio=off:spl=backtracking:sp=occurrence:updr=off_365 on FEQ061

WATCH: 15.02 CPU 15.06 WC

WATCH: 18.02 CPU 18.07 WC

WATCH: 21.02 CPU 21.08 WC

WATCH: 24.04 CPU 24.09 WC

WATCH: 27.04 CPU 27.10 WC

WATCH: 30.05 CPU 30.11 WC

WATCH: 33.05 CPU 33.12 WC

WATCH: 36.07 CPU 36.13 WC

WATCH: 39.07 CPU 39.13 WC

WATCH: 42.07 CPU 42.14 WC
Refutation found. Thanks to Tanya!
% SZS status Theorem for FEQ061
% SZS output start Proof for FEQ061
1159816. $false (0:0) [subsumption resolution 1159749,86]
86. sP0(one) (0:2) [inequality splitting 83,85]
85. ~sP0(addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),antidomain(antidomain(sK2)))) (0:20) [inequality splitting name introduction]
83. addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),antidomain(antidomain(sK2))) != one (0:21) [definition unfolding 49,79,58,58]
58. antidomain(antidomain(X0)) = domain(X0) (0:6) [cnf transformation 32]
32. ! [X0] : antidomain(antidomain(X0)) = domain(X0)[rectify 16]
16. ! [X3] : antidomain(antidomain(X3)) = domain(X3)[input]
79. antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))) = forward_box(X0,X1) (0:17) [definition unfolding 64,77,78,77]
78. antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))) = forward_diamond(X0,X1) (0:11) [definition unfolding 67,58,58]
67. domain(multiplication(X0,domain(X1))) = forward_diamond(X0,X1) (0:9) [cnf transformation 40]
40. ! [X0,X1] : domain(multiplication(X0,domain(X1))) = forward_diamond(X0,X1)[rectify 23]
23. ! [X3,X4] : domain(multiplication(X3,domain(X4))) = forward_diamond(X3,X4)[input]
77. antidomain(antidomain(antidomain(X0))) = c(X0) (0:7) [definition unfolding 59,58]
59. antidomain(domain(X0)) = c(X0) (0:6) [cnf transformation 33]
33. ! [X0] : antidomain(domain(X0)) = c(X0)[rectify 22]
22. ! [X3] : antidomain(domain(X3)) = c(X3)[input]
64. c(forward_diamond(X0,c(X1))) = forward_box(X0,X1) (0:9) [cnf transformation 37]
37. ! [X0,X1] : c(forward_diamond(X0,c(X1))) = forward_box(X0,X1)[rectify 26]
26. ! [X3,X4] : c(forward_diamond(X3,c(X4))) = forward_box(X3,X4)[input]
49. addition(forward_box(sK0,domain(sK1)),domain(sK2)) != one (0:9) [cnf transformation 46]
46. addition(domain(sK1),backward_box(sK0,domain(sK2))) = one & addition(forward_box(sK0,domain(sK1)),domain(sK2)) != one[skolemisation 45]
45. ? [X0,X1,X2] : (addition(domain(X1),backward_box(X0,domain(X2))) = one & addition(forward_box(X0,domain(X1)),domain(X2)) != one)[ennf transformation 29]
29. ~! [X0,X1,X2] : (addition(domain(X1),backward_box(X0,domain(X2))) = one => addition(forward_box(X0,domain(X1)),domain(X2)) = one)[rectify 28]
28. ~! [X3,X4,X5] : (addition(domain(X4),backward_box(X3,domain(X5))) = one => addition(forward_box(X3,domain(X4)),domain(X5)) = one)[negated conjecture 27]
27. ! [X3,X4,X5] : (addition(domain(X4),backward_box(X3,domain(X5))) = one => addition(forward_box(X3,domain(X4)),domain(X5)) = one)[input]
1159749. ~sP0(one) (0:2) [backward demodulation 1159748,1461]
1461. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1))))) (0:10) [forward demodulation 1460,1455]
1455. antidomain(X41) = antidomain(antidomain(antidomain(X41))) (2:7) [backward demodulation 1454,1012]
1012. multiplication(antidomain(antidomain(antidomain(X41))),antidomain(X41)) = antidomain(antidomain(antidomain(X41))) (2:12) [forward demodulation 993,51]
51. multiplication(X0,one) = X0 (0:5) [cnf transformation 11]
11. ! [X0] : multiplication(X0,one) = X0[input]
993. multiplication(antidomain(antidomain(antidomain(X41))),one) = multiplication(antidomain(antidomain(antidomain(X41))),antidomain(X41)) (2:14) [superposition 615,87]
87. addition(antidomain(X0),antidomain(antidomain(X0))) = one (0:8) [backward demodulation 63,61]
61. addition(antidomain(antidomain(X0)),antidomain(X0)) = one (0:8) [cnf transformation 35]
35. ! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one[rectify 13]
13. ! [X3] : addition(antidomain(antidomain(X3)),antidomain(X3)) = one[input]
63. addition(X0,X1) = addition(X1,X0) (0:7) [cnf transformation 12]
12. ! [X0,X1] : addition(X0,X1) = addition(X1,X0)[input]
615. multiplication(antidomain(X20),X21) = multiplication(antidomain(X20),addition(X21,X20)) (1:11) [forward demodulation 581,50]
50. addition(X0,zero) = X0 (0:5) [cnf transformation 2]
2. ! [X0] : addition(X0,zero) = X0[input]
581. multiplication(antidomain(X20),addition(X21,X20)) = addition(multiplication(antidomain(X20),X21),zero) (1:13) [superposition 75,57]
57. multiplication(antidomain(X0),X0) = zero (0:6) [cnf transformation 31]
31. ! [X0] : multiplication(antidomain(X0),X0) = zero[rectify 19]
19. ! [X3] : multiplication(antidomain(X3),X3) = zero[input]
75. multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) (0:13) [cnf transformation 9]
9. ! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2))[input]
1454. multiplication(antidomain(antidomain(X0)),X0) = X0 (2:7) [forward demodulation 1430,53]
53. multiplication(one,X0) = X0 (0:5) [cnf transformation 8]
8. ! [X0] : multiplication(one,X0) = X0[input]
1430. multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0) (2:9) [superposition 1102,87]
1102. multiplication(X29,X28) = multiplication(addition(antidomain(X28),X29),X28) (1:10) [forward demodulation 1053,96]
96. addition(zero,X0) = X0 (1:5) [superposition 63,50]
1053. multiplication(addition(antidomain(X28),X29),X28) = addition(zero,multiplication(X29,X28)) (1:12) [superposition 76,57]
76. multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) (0:13) [cnf transformation 7]
7. ! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2))[input]
1460. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(sK1))))))) (0:12) [forward demodulation 1459,1455]
1459. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))) (0:14) [forward demodulation 1458,1455]
1458. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))) (0:16) [forward demodulation 1456,1455]
1456. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))) (0:18) [backward demodulation 1455,89]
89. ~sP0(addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) (0:20) [forward demodulation 85,63]
1159748. addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = one (12:11) [forward demodulation 1159747,153]
153. addition(one,antidomain(X12)) = one (2:6) [forward demodulation 144,63]
144. addition(antidomain(X12),one) = one (2:6) [superposition 118,87]
118. addition(X2,X3) = addition(X2,addition(X2,X3)) (1:9) [superposition 73,52]
52. addition(X0,X0) = X0 (0:5) [cnf transformation 4]
4. ! [X0] : addition(X0,X0) = X0[input]
73. addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0) (0:11) [cnf transformation 44]
44. ! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0)[rectify 3]
3. ! [X2,X1,X0] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2)[input]
1159747. addition(one,antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) (12:17) [forward demodulation 1159746,123]
123. addition(one,X17) = addition(antidomain(X16),addition(antidomain(antidomain(X16)),X17)) (1:12) [superposition 73,87]
1159746. addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(sK2),addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1))))) (12:22) [forward demodulation 1159745,127]
127. addition(X7,addition(X8,X9)) = addition(X9,addition(X7,X8)) (1:11) [superposition 73,63]
1159745. addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(antidomain(sK2)),addition(antidomain(multiplication(sK0,antidomain(sK1))),antidomain(sK2))) (12:22) [forward demodulation 1159744,133]
133. addition(X4,addition(X5,X6)) = addition(X5,addition(X4,X6)) (1:11) [forward demodulation 119,73]
119. addition(X4,addition(X5,X6)) = addition(addition(X5,X4),X6) (1:11) [superposition 73,63]
1159744. addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(antidomain(antidomain(sK2)),antidomain(sK2))) (12:22) [forward demodulation 1159743,71453]
71453. antidomain(antidomain(X60)) = coantidomain(antidomain(X60)) (6:7) [forward demodulation 71452,9694]
9694. addition(antidomain(antidomain(X16)),coantidomain(antidomain(X16))) = antidomain(antidomain(X16)) (3:11) [forward demodulation 9693,51]
9693. multiplication(antidomain(antidomain(X16)),one) = addition(antidomain(antidomain(X16)),coantidomain(antidomain(X16))) (3:13) [forward demodulation 9692,154]
154. addition(one,coantidomain(X13)) = one (2:6) [forward demodulation 145,63]
145. addition(coantidomain(X13),one) = one (2:6) [superposition 118,88]
88. addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one (0:8) [backward demodulation 63,62]
62. addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one (0:8) [cnf transformation 36]
36. ! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one[rectify 15]
15. ! [X3] : addition(coantidomain(coantidomain(X3)),coantidomain(X3)) = one[input]
9692. multiplication(antidomain(antidomain(X16)),addition(one,coantidomain(antidomain(X16)))) = addition(antidomain(antidomain(X16)),coantidomain(antidomain(X16))) (3:17) [forward demodulation 9665,620]
620. multiplication(X8,addition(X9,one)) = multiplication(X8,addition(one,X9)) (1:11) [forward demodulation 586,607]
607. multiplication(X8,addition(X9,one)) = addition(X8,multiplication(X8,X9)) (1:11) [forward demodulation 576,63]
576. multiplication(X8,addition(X9,one)) = addition(multiplication(X8,X9),X8) (1:11) [superposition 75,51]
586. multiplication(X8,addition(one,X9)) = addition(X8,multiplication(X8,X9)) (1:11) [superposition 75,51]
9665. multiplication(antidomain(antidomain(X16)),addition(coantidomain(antidomain(X16)),one)) = addition(antidomain(antidomain(X16)),coantidomain(antidomain(X16))) (3:17) [superposition 607,5099]
5099. multiplication(antidomain(antidomain(X46)),coantidomain(antidomain(X46))) = coantidomain(antidomain(X46)) (2:11) [forward demodulation 5042,53]
5042. multiplication(one,coantidomain(antidomain(X46))) = multiplication(antidomain(antidomain(X46)),coantidomain(antidomain(X46))) (2:13) [superposition 1098,87]
1098. multiplication(X17,coantidomain(X16)) = multiplication(addition(X16,X17),coantidomain(X16)) (1:11) [forward demodulation 1048,96]
1048. multiplication(addition(X16,X17),coantidomain(X16)) = addition(zero,multiplication(X17,coantidomain(X16))) (1:13) [superposition 76,56]
56. multiplication(X0,coantidomain(X0)) = zero (0:6) [cnf transformation 30]
30. ! [X0] : multiplication(X0,coantidomain(X0)) = zero[rectify 20]
20. ! [X3] : multiplication(X3,coantidomain(X3)) = zero[input]
71452. addition(antidomain(antidomain(X60)),coantidomain(antidomain(X60))) = coantidomain(antidomain(X60)) (6:11) [forward demodulation 71451,63]
71451. addition(coantidomain(antidomain(X60)),antidomain(antidomain(X60))) = coantidomain(antidomain(X60)) (6:11) [forward demodulation 71450,51]
71450. multiplication(coantidomain(antidomain(X60)),one) = addition(coantidomain(antidomain(X60)),antidomain(antidomain(X60))) (6:13) [forward demodulation 71449,153]
71449. multiplication(coantidomain(antidomain(X60)),addition(one,antidomain(antidomain(X60)))) = addition(coantidomain(antidomain(X60)),antidomain(antidomain(X60))) (6:17) [forward demodulation 71374,620]
71374. multiplication(coantidomain(antidomain(X60)),addition(antidomain(antidomain(X60)),one)) = addition(coantidomain(antidomain(X60)),antidomain(antidomain(X60))) (6:17) [superposition 607,66983]
66983. multiplication(coantidomain(antidomain(X20)),antidomain(antidomain(X20))) = antidomain(antidomain(X20)) (5:11) [superposition 66852,1455]
66852. multiplication(coantidomain(antidomain(X11)),X11) = X11 (4:7) [forward demodulation 66714,53]
66714. multiplication(one,X11) = multiplication(coantidomain(antidomain(X11)),X11) (4:9) [superposition 2449,88]
2449. multiplication(X10,X9) = multiplication(addition(X10,coantidomain(coantidomain(antidomain(X9)))),X9) (3:12) [forward demodulation 2416,50]
2416. multiplication(addition(X10,coantidomain(coantidomain(antidomain(X9)))),X9) = addition(multiplication(X10,X9),zero) (3:14) [superposition 76,2382]
2382. multiplication(coantidomain(coantidomain(antidomain(X2))),X2) = zero (2:8) [forward demodulation 2345,51]
2345. multiplication(coantidomain(coantidomain(antidomain(X2))),multiplication(X2,one)) = zero (2:10) [superposition 223,2230]
2230. one = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X21))),X21)) (1:9) [forward demodulation 2229,154]
2229. addition(one,coantidomain(multiplication(coantidomain(coantidomain(antidomain(X21))),X21))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X21))),X21)) (1:17) [forward demodulation 2156,113]
113. one = coantidomain(zero) (2:4) [forward demodulation 112,96]
112. addition(zero,coantidomain(zero)) = one (2:6) [superposition 88,90]
90. zero = coantidomain(one) (1:4) [superposition 56,53]
2156. addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(X21))),X21))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X21))),X21)) (1:18) [superposition 69,57]
69. addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) (0:18) [cnf transformation 42]
42. ! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))[rectify 17]
17. ! [X3,X4] : addition(coantidomain(multiplication(X3,X4)),coantidomain(multiplication(coantidomain(coantidomain(X3)),X4))) = coantidomain(multiplication(coantidomain(coantidomain(X3)),X4))[input]
223. multiplication(X7,multiplication(X8,coantidomain(multiplication(X7,X8)))) = zero (1:10) [superposition 74,56]
74. multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2) (0:11) [cnf transformation 1]
1. ! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2)[input]
1159743. addition(coantidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:22) [forward demodulation 1159742,53]
1159742. multiplication(one,addition(coantidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1))))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:24) [forward demodulation 1159741,153]
1159741. multiplication(addition(one,antidomain(sK2)),addition(coantidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1))))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:27) [forward demodulation 1159740,630]
630. multiplication(X5,addition(X6,X7)) = multiplication(X5,addition(X7,X6)) (1:11) [forward demodulation 594,75]
594. multiplication(X5,addition(X6,X7)) = addition(multiplication(X5,X7),multiplication(X5,X6)) (1:13) [superposition 75,63]
1159740. multiplication(addition(one,antidomain(sK2)),addition(antidomain(multiplication(sK0,antidomain(sK1))),coantidomain(antidomain(sK2)))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:27) [forward demodulation 1159739,7037]
7037. multiplication(addition(X43,X44),addition(X46,X45)) = multiplication(addition(X44,X43),addition(X45,X46)) (2:15) [superposition 1110,630]
1110. multiplication(addition(X9,X11),X10) = multiplication(addition(X11,X9),X10) (1:11) [forward demodulation 1060,76]
1060. multiplication(addition(X9,X11),X10) = addition(multiplication(X11,X10),multiplication(X9,X10)) (1:13) [superposition 76,63]
1159739. multiplication(addition(antidomain(sK2),one),addition(coantidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1))))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:27) [forward demodulation 1159516,630]
1159516. multiplication(addition(antidomain(sK2),one),addition(antidomain(multiplication(sK0,antidomain(sK1))),coantidomain(antidomain(sK2)))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),addition(coantidomain(antidomain(sK2)),antidomain(sK2))) (12:27) [superposition 4426,1154780]
1154780. multiplication(antidomain(sK2),antidomain(multiplication(sK0,antidomain(sK1)))) = antidomain(sK2) (11:11) [forward demodulation 1154779,1455]
1154779. multiplication(antidomain(sK2),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) = antidomain(sK2) (11:13) [forward demodulation 1154448,51]
1154448. multiplication(antidomain(sK2),one) = multiplication(antidomain(sK2),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) (11:15) [superposition 15422,87]
15422. multiplication(antidomain(sK2),X1) = multiplication(antidomain(sK2),addition(antidomain(antidomain(multiplication(sK0,antidomain(sK1)))),X1)) (10:16) [forward demodulation 15396,96]
15396. multiplication(antidomain(sK2),addition(antidomain(antidomain(multiplication(sK0,antidomain(sK1)))),X1)) = addition(zero,multiplication(antidomain(sK2),X1)) (10:18) [superposition 75,15338]
15338. multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1))))) = zero (9:11) [forward demodulation 15307,53]
15307. multiplication(one,multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) = zero (9:13) [superposition 57,15159]
15159. one = antidomain(multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) (8:12) [forward demodulation 15158,153]
15158. addition(one,antidomain(multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1))))))) = antidomain(multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) (8:23) [forward demodulation 15135,108]
108. one = antidomain(zero) (2:4) [forward demodulation 107,96]
107. addition(zero,antidomain(zero)) = one (2:6) [superposition 87,93]
93. zero = antidomain(one) (1:4) [superposition 57,51]
15135. addition(antidomain(zero),antidomain(multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1))))))) = antidomain(multiplication(antidomain(sK2),antidomain(antidomain(multiplication(sK0,antidomain(sK1)))))) (8:24) [superposition 70,15099]
15099. multiplication(antidomain(sK2),multiplication(sK0,antidomain(sK1))) = zero (7:9) [forward demodulation 15073,55]
55. multiplication(X0,zero) = zero (0:5) [cnf transformation 6]
6. ! [X0] : multiplication(X0,zero) = zero[input]
15073. multiplication(antidomain(sK2),zero) = multiplication(antidomain(sK2),multiplication(sK0,antidomain(sK1))) (7:12) [superposition 729,15048]
15048. multiplication(coantidomain(coantidomain(antidomain(sK2))),multiplication(sK0,antidomain(sK1))) = zero (6:11) [forward demodulation 15047,1455]
15047. multiplication(coantidomain(coantidomain(antidomain(sK2))),multiplication(sK0,antidomain(antidomain(antidomain(sK1))))) = zero (6:13) [forward demodulation 15024,74]
15024. multiplication(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0),antidomain(antidomain(antidomain(sK1)))) = zero (6:13) [superposition 8500,14154]
14154. multiplication(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)),antidomain(sK1)) = antidomain(sK1) (5:13) [forward demodulation 14114,53]
14114. multiplication(one,antidomain(sK1)) = multiplication(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)),antidomain(sK1)) (5:15) [superposition 1102,13888]
13888. addition(antidomain(antidomain(sK1)),coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))) = one (4:13) [forward demodulation 13887,4268]
4268. coantidomain(X47) = coantidomain(coantidomain(coantidomain(X47))) (2:7) [forward demodulation 4267,707]
707. multiplication(X0,coantidomain(coantidomain(X0))) = X0 (2:7) [forward demodulation 686,51]
686. multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))) (2:9) [superposition 621,88]
621. multiplication(X10,X11) = multiplication(X10,addition(coantidomain(X10),X11)) (1:10) [forward demodulation 587,96]
587. multiplication(X10,addition(coantidomain(X10),X11)) = addition(zero,multiplication(X10,X11)) (1:12) [superposition 75,56]
4267. multiplication(coantidomain(X47),coantidomain(coantidomain(coantidomain(X47)))) = coantidomain(coantidomain(coantidomain(X47))) (2:12) [forward demodulation 4232,53]
4232. multiplication(one,coantidomain(coantidomain(coantidomain(X47)))) = multiplication(coantidomain(X47),coantidomain(coantidomain(coantidomain(X47)))) (2:14) [superposition 1082,88]
1082. multiplication(X17,coantidomain(X16)) = multiplication(addition(X17,X16),coantidomain(X16)) (1:11) [forward demodulation 1033,50]
1033. multiplication(addition(X17,X16),coantidomain(X16)) = addition(multiplication(X17,coantidomain(X16)),zero) (1:13) [superposition 76,56]
13887. addition(antidomain(antidomain(sK1)),coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = one (4:15) [forward demodulation 13828,154]
13828. addition(one,coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = addition(antidomain(antidomain(sK1)),coantidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) (4:25) [superposition 1623,9529]
9529. addition(antidomain(coantidomain(X15)),coantidomain(coantidomain(X15))) = coantidomain(coantidomain(X15)) (3:11) [forward demodulation 9528,63]
9528. addition(coantidomain(coantidomain(X15)),antidomain(coantidomain(X15))) = coantidomain(coantidomain(X15)) (3:11) [forward demodulation 9527,53]
9527. multiplication(one,coantidomain(coantidomain(X15))) = addition(coantidomain(coantidomain(X15)),antidomain(coantidomain(X15))) (3:13) [forward demodulation 9526,153]
9526. multiplication(addition(one,antidomain(coantidomain(X15))),coantidomain(coantidomain(X15))) = addition(coantidomain(coantidomain(X15)),antidomain(coantidomain(X15))) (3:17) [forward demodulation 9488,1110]
9488. multiplication(addition(antidomain(coantidomain(X15)),one),coantidomain(coantidomain(X15))) = addition(coantidomain(coantidomain(X15)),antidomain(coantidomain(X15))) (3:17) [superposition 1085,3974]
3974. multiplication(antidomain(coantidomain(X47)),coantidomain(coantidomain(X47))) = antidomain(coantidomain(X47)) (2:11) [forward demodulation 3913,51]
3913. multiplication(antidomain(coantidomain(X47)),one) = multiplication(antidomain(coantidomain(X47)),coantidomain(coantidomain(X47))) (2:13) [superposition 628,88]
628. multiplication(antidomain(X20),X21) = multiplication(antidomain(X20),addition(X20,X21)) (1:11) [forward demodulation 591,96]
591. multiplication(antidomain(X20),addition(X20,X21)) = addition(zero,multiplication(antidomain(X20),X21)) (1:13) [superposition 75,57]
1085. multiplication(addition(X27,one),X26) = addition(X26,multiplication(X27,X26)) (1:11) [forward demodulation 1037,63]
1037. multiplication(addition(X27,one),X26) = addition(multiplication(X27,X26),X26) (1:11) [superposition 76,53]
1623. addition(one,X0) = addition(antidomain(antidomain(sK1)),addition(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))),X0)) (1:19) [superposition 73,1463]
1463. addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))) = one (0:15) [forward demodulation 1462,1455]
1462. addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))) = one (0:17) [forward demodulation 1457,1455]
1457. addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))))) = one (0:19) [backward demodulation 1455,84]
84. addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))),sK0))))))) = one (0:21) [definition unfolding 48,58,82,58]
82. antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))) = backward_box(X0,X1) (0:17) [definition unfolding 65,77,80,77]
80. coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))) = backward_diamond(X0,X1) (0:11) [definition unfolding 68,60,60]
60. codomain(X0) = coantidomain(coantidomain(X0)) (0:6) [cnf transformation 34]
34. ! [X0] : codomain(X0) = coantidomain(coantidomain(X0))[rectify 14]
14. ! [X3] : codomain(X3) = coantidomain(coantidomain(X3))[input]
68. codomain(multiplication(codomain(X1),X0)) = backward_diamond(X0,X1) (0:9) [cnf transformation 41]
41. ! [X0,X1] : codomain(multiplication(codomain(X1),X0)) = backward_diamond(X0,X1)[rectify 21]
21. ! [X3,X4] : codomain(multiplication(codomain(X4),X3)) = backward_diamond(X3,X4)[input]
65. c(backward_diamond(X0,c(X1))) = backward_box(X0,X1) (0:9) [cnf transformation 38]
38. ! [X0,X1] : c(backward_diamond(X0,c(X1))) = backward_box(X0,X1)[rectify 25]
25. ! [X3,X4] : c(backward_diamond(X3,c(X4))) = backward_box(X3,X4)[input]
48. addition(domain(sK1),backward_box(sK0,domain(sK2))) = one (0:9) [cnf transformation 46]
8500. multiplication(X8,antidomain(antidomain(multiplication(coantidomain(X8),X9)))) = zero (3:10) [forward demodulation 8332,53]
8332. multiplication(one,multiplication(X8,antidomain(antidomain(multiplication(coantidomain(X8),X9))))) = zero (3:12) [superposition 57,2787]
2787. one = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1))))) (2:11) [forward demodulation 2786,153]
2786. addition(one,antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1))))) (2:21) [forward demodulation 2673,108]
2673. addition(antidomain(zero),antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1)))))) = antidomain(multiplication(X0,antidomain(antidomain(multiplication(coantidomain(X0),X1))))) (2:22) [superposition 70,228]
228. multiplication(X4,multiplication(coantidomain(X4),X5)) = zero (1:8) [forward demodulation 216,54]
54. multiplication(zero,X0) = zero (0:5) [cnf transformation 5]
5. ! [X0] : multiplication(zero,X0) = zero[input]
216. multiplication(zero,X5) = multiplication(X4,multiplication(coantidomain(X4),X5)) (1:10) [superposition 74,56]
729. multiplication(X6,X7) = multiplication(X6,multiplication(coantidomain(coantidomain(X6)),X7)) (3:11) [superposition 74,707]
70. addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))) (0:18) [cnf transformation 43]
43. ! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1))))[rectify 18]
18. ! [X3,X4] : addition(antidomain(multiplication(X3,X4)),antidomain(multiplication(X3,antidomain(antidomain(X4))))) = antidomain(multiplication(X3,antidomain(antidomain(X4))))[input]
4426. multiplication(addition(X7,one),addition(X8,coantidomain(X7))) = addition(X8,addition(coantidomain(X7),multiplication(X7,X8))) (2:17) [forward demodulation 4425,762]
762. addition(X11,addition(X12,X10)) = addition(X11,addition(X10,X12)) (2:11) [superposition 133,127]
4425. multiplication(addition(X7,one),addition(X8,coantidomain(X7))) = addition(X8,addition(multiplication(X7,X8),coantidomain(X7))) (2:17) [forward demodulation 4424,133]
4424. multiplication(addition(X7,one),addition(X8,coantidomain(X7))) = addition(multiplication(X7,X8),addition(X8,coantidomain(X7))) (2:17) [forward demodulation 4340,63]
4340. multiplication(addition(X7,one),addition(X8,coantidomain(X7))) = addition(addition(X8,coantidomain(X7)),multiplication(X7,X8)) (2:17) [superposition 1085,608]
608. multiplication(X10,X11) = multiplication(X10,addition(X11,coantidomain(X10))) (1:10) [forward demodulation 577,50]
577. multiplication(X10,addition(X11,coantidomain(X10))) = addition(multiplication(X10,X11),zero) (1:12) [superposition 75,56]
% SZS output end Proof for FEQ061
------------------------------
Version: Vampire 1.8 (revision 1280)
Termination reason: Refutation

Active clauses: 1523
Passive clauses: 50196
Generated clauses: 1159752
Final active clauses: 1277
Final passive clauses: 38866
Input formulas: 27
Initial clauses: 22

Function definitions: 8
Splitted inequalities: 1

Fw subsumption resolutions: 1
Fw demodulations: 646371
Bw demodulations: 6561

Simple tautologies: 1
Forward subsumptions: 434662
Fw demodulations to eq. taut.: 28391
Bw demodulations to eq. taut.: 3492

Binary resolution: 1
Forward superposition: 253867
Backward superposition: 252445
Self superposition: 484

Memory used [KB]: 984035
Time elapsed: 31.667 s
------------------------------
% Success in time 44.8 s

WATCH: 44.73 CPU 44.80 WC

FINAL WATCH: 44.73 CPU 44.80 WC