% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for tree
% SZS output start Proof for tree
1. ! [X0,X1,X2] : mul(mul(X1,X0),mul(X0,mul(X2,X1))) = X0 [input]
2. ! [X0] : mul(1,X0) = 2 [input]
3. ! [X0,X1] : mul(mul(mul(X0,2),2),mul(mul(X1,2),2)) = mul(mul(mul(X0,X1),2),2) [input]
4. ~! [X0,X1] : mul(mul(mul(X0,2),2),mul(mul(X1,2),2)) = mul(mul(mul(X0,X1),2),2) [negated conjecture 3]
5. ? [X0,X1] : mul(mul(mul(X0,2),2),mul(mul(X1,2),2)) != mul(mul(mul(X0,X1),2),2) [ennf transformation 4]
6. ? [X0,X1] : mul(mul(mul(X0,2),2),mul(mul(X1,2),2)) != mul(mul(mul(X0,X1),2),2) => mul(mul(mul(sK0,2),2),mul(mul(sK1,2),2)) != mul(mul(mul(sK0,sK1),2),2) [choice axiom]
7. mul(mul(mul(sK0,2),2),mul(mul(sK1,2),2)) != mul(mul(mul(sK0,sK1),2),2) [skolemisation 5,6]
8. mul(mul(X1,X0),mul(X0,mul(X2,X1))) = X0 [cnf transformation 1]
9. mul(1,X0) = 2 [cnf transformation 2]
10. mul(mul(mul(sK0,2),2),mul(mul(sK1,2),2)) != mul(mul(mul(sK0,sK1),2),2) [cnf transformation 7]
11. mul(2,mul(X0,mul(X1,1))) = X0 [superposition 8,9]
12. mul(X1,mul(X2,X0)) = mul(X1,mul(mul(X1,mul(X2,X0)),mul(X3,mul(X0,X1)))) [superposition 8,8]
13. mul(mul(X0,X1),mul(X1,2)) = X1 [superposition 8,9]
14. mul(mul(mul(X1,mul(X2,X0)),X3),mul(X3,X1)) = X3 [superposition 8,8]
15. 1 = mul(mul(X1,1),2) [superposition 8,9]
16. mul(X0,X1) = mul(mul(mul(X2,X0),mul(X0,X1)),X1) [superposition 8,8]
17. 1 = mul(2,2) [superposition 15,9]
18. mul(mul(2,X1),mul(X1,1)) = X1 [superposition 8,15]
22. mul(2,mul(X0,2)) = X0 [superposition 11,9]
29. mul(X0,1) = mul(2,1) [superposition 22,15]
30. 2 = mul(2,1) [superposition 22,17]
32. mul(mul(mul(X0,2),X1),mul(X1,X0)) = X1 [superposition 8,22]
34. 2 = mul(X0,1) [backward demodulation 29,30]
36. mul(mul(2,X1),2) = X1 [backward demodulation 18,34]
42. mul(X1,2) = mul(X1,mul(mul(X1,2),2)) [superposition 13,13]
56. mul(mul(mul(X3,X1),X4),mul(X4,X3)) = X4 [superposition 14,8]
68. mul(mul(X1,X2),2) = mul(mul(X1,X2),mul(mul(mul(X1,X2),2),X0)) [superposition 14,13]
78. mul(X3,X0) = mul(X3,mul(mul(X3,X0),2)) [superposition 13,14]
96. mul(mul(X3,X0),X4) = mul(mul(X3,mul(mul(X3,X0),X4)),X4) [superposition 16,14]
134. mul(mul(2,X1),mul(X1,X0)) = X1 [superposition 8,36]
175. mul(X0,mul(X4,X3)) = mul(X0,mul(mul(X0,mul(X4,X3)),X3)) [superposition 12,14]
191. mul(mul(2,mul(X0,X1)),2) = mul(mul(2,mul(X0,X1)),mul(X2,mul(X1,2))) [superposition 36,12]
198. mul(X0,X1) = mul(mul(2,mul(X0,X1)),mul(X2,mul(X1,2))) [forward demodulation 191,36]
326. mul(mul(X0,X1),X2) = mul(mul(mul(mul(X2,X0),X3),mul(mul(X0,X1),X2)),X2) [superposition 56,56]
331. 2 = mul(mul(mul(mul(X0,2),X1),2),X0) [superposition 56,22]
1497. 2 = mul(mul(mul(mul(mul(X0,X1),2),X2),2),mul(2,X1)) [superposition 175,331]
2135. mul(X0,2) = mul(mul(2,mul(X0,2)),mul(X1,mul(mul(mul(X0,2),2),2))) [superposition 198,42]
2150. mul(mul(2,X0),mul(X2,mul(mul(X0,X1),2))) = X0 [superposition 198,134]
2265. mul(X0,2) = mul(X0,mul(X1,mul(mul(mul(X0,2),2),2))) [forward demodulation 2135,22]
2669. mul(X0,mul(mul(X0,X2),2)) = mul(mul(mul(2,X0),X1),mul(mul(X0,X2),2)) [superposition 96,2150]
2746. mul(X0,X2) = mul(mul(mul(2,X0),X1),mul(mul(X0,X2),2)) [forward demodulation 2669,78]
6668. 2 = mul(mul(mul(mul(mul(X1,mul(X0,2)),2),X2),2),X0) [superposition 1497,22]
12201. mul(mul(mul(X0,X1),2),mul(mul(mul(mul(X0,X1),2),2),2)) = mul(X1,mul(mul(mul(mul(X0,X1),2),2),2)) [superposition 16,2265]
12317. mul(mul(mul(X0,X1),2),2) = mul(X1,mul(mul(mul(mul(X0,X1),2),2),2)) [forward demodulation 12201,68]
15053. mul(mul(mul(X0,X2),X3),mul(X3,mul(mul(2,X0),X1))) = X3 [superposition 14,2746]
19557. mul(2,mul(X1,mul(mul(mul(X0,mul(X1,2)),2),X2))) = X1 [superposition 32,6668]
23067. mul(mul(mul(mul(X0,2),X1),X2),mul(X2,mul(X0,X3))) = X2 [superposition 15053,22]
25381. mul(X0,2) = mul(X0,mul(mul(mul(X1,mul(X0,2)),2),X2)) [superposition 36,19557]
33110. mul(X1,mul(X0,X2)) = mul(X1,mul(mul(X1,mul(X0,X2)),mul(mul(X0,2),X3))) [superposition 23067,23067]
37156. mul(mul(2,X0),mul(mul(mul(X1,X0),2),X2)) = X0 [superposition 25381,36]
38922. mul(mul(mul(X1,X0),2),2) = mul(mul(mul(X1,X0),2),mul(mul(X0,2),X2)) [superposition 25381,37156]
317618. mul(X0,X2) = mul(mul(mul(mul(X1,mul(2,X0)),2),2),mul(mul(X0,X2),2)) [superposition 2746,12317]
737659. mul(mul(X1,2),X0) = mul(mul(mul(mul(X0,X1),2),2),X0) [superposition 326,38922]
742113. mul(mul(mul(X1,X0),2),mul(mul(X0,2),X1)) = mul(mul(mul(X1,2),2),mul(mul(X0,2),X1)) [superposition 737659,32]
743026. mul(mul(mul(X1,X0),2),2) = mul(mul(mul(X1,2),2),mul(mul(X0,2),X1)) [forward demodulation 742113,38922]
1242246. mul(mul(mul(X1,2),2),mul(X0,X1)) = mul(mul(mul(X1,mul(2,X0)),2),2) [superposition 743026,36]
1279208. mul(X1,X2) = mul(mul(mul(mul(X0,2),2),mul(X1,X0)),mul(mul(X1,X2),2)) [superposition 317618,1242246]
1341556. mul(mul(mul(X0,2),2),mul(X1,X0)) = mul(mul(mul(X0,2),2),mul(X1,2)) [superposition 33110,1279208]
1380435. mul(mul(mul(X0,2),2),mul(mul(X1,2),2)) = mul(mul(mul(X0,X1),2),2) [superposition 1341556,743026]
1485717. mul(mul(mul(sK0,sK1),2),2) != mul(mul(mul(sK0,sK1),2),2) [superposition 10,1380435]
1486046. $false [trivial inequality removal 1485717]
% SZS output end Proof for tree
% ------------------------------
% Version: Vampire 4.9 (commit )
% Termination reason: Refutation

% Memory used [KB]: 589665
% Time elapsed: 53.341 s
% ------------------------------
% ------------------------------