%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 06:47:42 AM UTC 2026 % Result : Theorem 131.54s 17.51s % Output : CNFRefutation 131.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.36 % Computer : n015.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 26 21:24:59 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 131.54/17.51 % SZS status Theorem for theBenchmark.p % 131.54/17.51 % SZS output start CNFRefutation for theBenchmark.p % 131.54/17.51 fof(ax1, axiom, ((op(e0,e0) = e0 | (op(e0,e0) = e1 | (op(e0,e0) = e2 | (op(e0,e0) = e3 | op(e0,e0) = e4)))) & ((op(e0,e1) = e0 | (op(e0,e1) = e1 | (op(e0,e1) = e2 | (op(e0,e1) = e3 | op(e0,e1) = e4)))) & ((op(e0,e2) = e0 | (op(e0,e2) = e1 | (op(e0,e2) = e2 | (op(e0,e2) = e3 | op(e0,e2) = e4)))) & ((op(e0,e3) = e0 | (op(e0,e3) = e1 | (op(e0,e3) = e2 | (op(e0,e3) = e3 | op(e0,e3) = e4)))) & ((op(e0,e4) = e0 | (op(e0,e4) = e1 | (op(e0,e4) = e2 | (op(e0,e4) = e3 | op(e0,e4) = e4)))) & ((op(e1,e0) = e0 | (op(e1,e0) = e1 | (op(e1,e0) = e2 | (op(e1,e0) = e3 | op(e1,e0) = e4)))) & ((op(e1,e1) = e0 | (op(e1,e1) = e1 | (op(e1,e1) = e2 | (op(e1,e1) = e3 | op(e1,e1) = e4)))) & ((op(e1,e2) = e0 | (op(e1,e2) = e1 | (op(e1,e2) = e2 | (op(e1,e2) = e3 | op(e1,e2) = e4)))) & ((op(e1,e3) = e0 | (op(e1,e3) = e1 | (op(e1,e3) = e2 | (op(e1,e3) = e3 | op(e1,e3) = e4)))) & ((op(e1,e4) = e0 | (op(e1,e4) = e1 | (op(e1,e4) = e2 | (op(e1,e4) = e3 | op(e1,e4) = e4)))) & ((op(e2,e0) = e0 | (op(e2,e0) = e1 | (op(e2,e0) = e2 | (op(e2,e0) = e3 | op(e2,e0) = e4)))) & ((op(e2,e1) = e0 | (op(e2,e1) = e1 | (op(e2,e1) = e2 | (op(e2,e1) = e3 | op(e2,e1) = e4)))) & ((op(e2,e2) = e0 | (op(e2,e2) = e1 | (op(e2,e2) = e2 | (op(e2,e2) = e3 | op(e2,e2) = e4)))) & ((op(e2,e3) = e0 | (op(e2,e3) = e1 | (op(e2,e3) = e2 | (op(e2,e3) = e3 | op(e2,e3) = e4)))) & ((op(e2,e4) = e0 | (op(e2,e4) = e1 | (op(e2,e4) = e2 | (op(e2,e4) = e3 | op(e2,e4) = e4)))) & ((op(e3,e0) = e0 | (op(e3,e0) = e1 | (op(e3,e0) = e2 | (op(e3,e0) = e3 | op(e3,e0) = e4)))) & ((op(e3,e1) = e0 | (op(e3,e1) = e1 | (op(e3,e1) = e2 | (op(e3,e1) = e3 | op(e3,e1) = e4)))) & ((op(e3,e2) = e0 | (op(e3,e2) = e1 | (op(e3,e2) = e2 | (op(e3,e2) = e3 | op(e3,e2) = e4)))) & ((op(e3,e3) = e0 | (op(e3,e3) = e1 | (op(e3,e3) = e2 | (op(e3,e3) = e3 | op(e3,e3) = e4)))) & ((op(e3,e4) = e0 | (op(e3,e4) = e1 | (op(e3,e4) = e2 | (op(e3,e4) = e3 | op(e3,e4) = e4)))) & ((op(e4,e0) = e0 | (op(e4,e0) = e1 | (op(e4,e0) = e2 | (op(e4,e0) = e3 | op(e4,e0) = e4)))) & ((op(e4,e1) = e0 | (op(e4,e1) = e1 | (op(e4,e1) = e2 | (op(e4,e1) = e3 | op(e4,e1) = e4)))) & ((op(e4,e2) = e0 | (op(e4,e2) = e1 | (op(e4,e2) = e2 | (op(e4,e2) = e3 | op(e4,e2) = e4)))) & ((op(e4,e3) = e0 | (op(e4,e3) = e1 | (op(e4,e3) = e2 | (op(e4,e3) = e3 | op(e4,e3) = e4)))) & (op(e4,e4) = e0 | (op(e4,e4) = e1 | (op(e4,e4) = e2 | (op(e4,e4) = e3 | op(e4,e4) = e4))))))))))))))))))))))))))))). % 131.54/17.51 fof(ax2, axiom, ((op(e0,e0) = e0 | (op(e0,e1) = e0 | (op(e0,e2) = e0 | (op(e0,e3) = e0 | op(e0,e4) = e0)))) & ((op(e0,e0) = e0 | (op(e1,e0) = e0 | (op(e2,e0) = e0 | (op(e3,e0) = e0 | op(e4,e0) = e0)))) & ((op(e0,e0) = e1 | (op(e0,e1) = e1 | (op(e0,e2) = e1 | (op(e0,e3) = e1 | op(e0,e4) = e1)))) & ((op(e0,e0) = e1 | (op(e1,e0) = e1 | (op(e2,e0) = e1 | (op(e3,e0) = e1 | op(e4,e0) = e1)))) & ((op(e0,e0) = e2 | (op(e0,e1) = e2 | (op(e0,e2) = e2 | (op(e0,e3) = e2 | op(e0,e4) = e2)))) & ((op(e0,e0) = e2 | (op(e1,e0) = e2 | (op(e2,e0) = e2 | (op(e3,e0) = e2 | op(e4,e0) = e2)))) & ((op(e0,e0) = e3 | (op(e0,e1) = e3 | (op(e0,e2) = e3 | (op(e0,e3) = e3 | op(e0,e4) = e3)))) & ((op(e0,e0) = e3 | (op(e1,e0) = e3 | (op(e2,e0) = e3 | (op(e3,e0) = e3 | op(e4,e0) = e3)))) & ((op(e0,e0) = e4 | (op(e0,e1) = e4 | (op(e0,e2) = e4 | (op(e0,e3) = e4 | op(e0,e4) = e4)))) & ((op(e0,e0) = e4 | (op(e1,e0) = e4 | (op(e2,e0) = e4 | (op(e3,e0) = e4 | op(e4,e0) = e4)))) & ((op(e1,e0) = e0 | (op(e1,e1) = e0 | (op(e1,e2) = e0 | (op(e1,e3) = e0 | op(e1,e4) = e0)))) & ((op(e0,e1) = e0 | (op(e1,e1) = e0 | (op(e2,e1) = e0 | (op(e3,e1) = e0 | op(e4,e1) = e0)))) & ((op(e1,e0) = e1 | (op(e1,e1) = e1 | (op(e1,e2) = e1 | (op(e1,e3) = e1 | op(e1,e4) = e1)))) & ((op(e0,e1) = e1 | (op(e1,e1) = e1 | (op(e2,e1) = e1 | (op(e3,e1) = e1 | op(e4,e1) = e1)))) & ((op(e1,e0) = e2 | (op(e1,e1) = e2 | (op(e1,e2) = e2 | (op(e1,e3) = e2 | op(e1,e4) = e2)))) & ((op(e0,e1) = e2 | (op(e1,e1) = e2 | (op(e2,e1) = e2 | (op(e3,e1) = e2 | op(e4,e1) = e2)))) & ((op(e1,e0) = e3 | (op(e1,e1) = e3 | (op(e1,e2) = e3 | (op(e1,e3) = e3 | op(e1,e4) = e3)))) & ((op(e0,e1) = e3 | (op(e1,e1) = e3 | (op(e2,e1) = e3 | (op(e3,e1) = e3 | op(e4,e1) = e3)))) & ((op(e1,e0) = e4 | (op(e1,e1) = e4 | (op(e1,e2) = e4 | (op(e1,e3) = e4 | op(e1,e4) = e4)))) & ((op(e0,e1) = e4 | (op(e1,e1) = e4 | (op(e2,e1) = e4 | (op(e3,e1) = e4 | op(e4,e1) = e4)))) & ((op(e2,e0) = e0 | (op(e2,e1) = e0 | (op(e2,e2) = e0 | (op(e2,e3) = e0 | op(e2,e4) = e0)))) & ((op(e0,e2) = e0 | (op(e1,e2) = e0 | (op(e2,e2) = e0 | (op(e3,e2) = e0 | op(e4,e2) = e0)))) & ((op(e2,e0) = e1 | (op(e2,e1) = e1 | (op(e2,e2) = e1 | (op(e2,e3) = e1 | op(e2,e4) = e1)))) & ((op(e0,e2) = e1 | (op(e1,e2) = e1 | (op(e2,e2) = e1 | (op(e3,e2) = e1 | op(e4,e2) = e1)))) & ((op(e2,e0) = e2 | (op(e2,e1) = e2 | (op(e2,e2) = e2 | (op(e2,e3) = e2 | op(e2,e4) = e2)))) & ((op(e0,e2) = e2 | (op(e1,e2) = e2 | (op(e2,e2) = e2 | (op(e3,e2) = e2 | op(e4,e2) = e2)))) & ((op(e2,e0) = e3 | (op(e2,e1) = e3 | (op(e2,e2) = e3 | (op(e2,e3) = e3 | op(e2,e4) = e3)))) & ((op(e0,e2) = e3 | (op(e1,e2) = e3 | (op(e2,e2) = e3 | (op(e3,e2) = e3 | op(e4,e2) = e3)))) & ((op(e2,e0) = e4 | (op(e2,e1) = e4 | (op(e2,e2) = e4 | (op(e2,e3) = e4 | op(e2,e4) = e4)))) & ((op(e0,e2) = e4 | (op(e1,e2) = e4 | (op(e2,e2) = e4 | (op(e3,e2) = e4 | op(e4,e2) = e4)))) & ((op(e3,e0) = e0 | (op(e3,e1) = e0 | (op(e3,e2) = e0 | (op(e3,e3) = e0 | op(e3,e4) = e0)))) & ((op(e0,e3) = e0 | (op(e1,e3) = e0 | (op(e2,e3) = e0 | (op(e3,e3) = e0 | op(e4,e3) = e0)))) & ((op(e3,e0) = e1 | (op(e3,e1) = e1 | (op(e3,e2) = e1 | (op(e3,e3) = e1 | op(e3,e4) = e1)))) & ((op(e0,e3) = e1 | (op(e1,e3) = e1 | (op(e2,e3) = e1 | (op(e3,e3) = e1 | op(e4,e3) = e1)))) & ((op(e3,e0) = e2 | (op(e3,e1) = e2 | (op(e3,e2) = e2 | (op(e3,e3) = e2 | op(e3,e4) = e2)))) & ((op(e0,e3) = e2 | (op(e1,e3) = e2 | (op(e2,e3) = e2 | (op(e3,e3) = e2 | op(e4,e3) = e2)))) & ((op(e3,e0) = e3 | (op(e3,e1) = e3 | (op(e3,e2) = e3 | (op(e3,e3) = e3 | op(e3,e4) = e3)))) & ((op(e0,e3) = e3 | (op(e1,e3) = e3 | (op(e2,e3) = e3 | (op(e3,e3) = e3 | op(e4,e3) = e3)))) & ((op(e3,e0) = e4 | (op(e3,e1) = e4 | (op(e3,e2) = e4 | (op(e3,e3) = e4 | op(e3,e4) = e4)))) & ((op(e0,e3) = e4 | (op(e1,e3) = e4 | (op(e2,e3) = e4 | (op(e3,e3) = e4 | op(e4,e3) = e4)))) & ((op(e4,e0) = e0 | (op(e4,e1) = e0 | (op(e4,e2) = e0 | (op(e4,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e4) = e0 | (op(e1,e4) = e0 | (op(e2,e4) = e0 | (op(e3,e4) = e0 | op(e4,e4) = e0)))) & ((op(e4,e0) = e1 | (op(e4,e1) = e1 | (op(e4,e2) = e1 | (op(e4,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e4) = e1 | (op(e1,e4) = e1 | (op(e2,e4) = e1 | (op(e3,e4) = e1 | op(e4,e4) = e1)))) & ((op(e4,e0) = e2 | (op(e4,e1) = e2 | (op(e4,e2) = e2 | (op(e4,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e4) = e2 | (op(e1,e4) = e2 | (op(e2,e4) = e2 | (op(e3,e4) = e2 | op(e4,e4) = e2)))) & ((op(e4,e0) = e3 | (op(e4,e1) = e3 | (op(e4,e2) = e3 | (op(e4,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e4) = e3 | (op(e1,e4) = e3 | (op(e2,e4) = e3 | (op(e3,e4) = e3 | op(e4,e4) = e3)))) & ((op(e4,e0) = e4 | (op(e4,e1) = e4 | (op(e4,e2) = e4 | (op(e4,e3) = e4 | op(e4,e4) = e4)))) & (op(e0,e4) = e4 | (op(e1,e4) = e4 | (op(e2,e4) = e4 | (op(e3,e4) = e4 | op(e4,e4) = e4)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 131.54/17.51 fof(ax3, axiom, (op(op(e0,e0),op(e0,e0)) = e0 & (op(op(e1,e0),op(e0,e1)) = e0 & (op(op(e2,e0),op(e0,e2)) = e0 & (op(op(e3,e0),op(e0,e3)) = e0 & (op(op(e4,e0),op(e0,e4)) = e0 & (op(op(e0,e1),op(e1,e0)) = e1 & (op(op(e1,e1),op(e1,e1)) = e1 & (op(op(e2,e1),op(e1,e2)) = e1 & (op(op(e3,e1),op(e1,e3)) = e1 & (op(op(e4,e1),op(e1,e4)) = e1 & (op(op(e0,e2),op(e2,e0)) = e2 & (op(op(e1,e2),op(e2,e1)) = e2 & (op(op(e2,e2),op(e2,e2)) = e2 & (op(op(e3,e2),op(e2,e3)) = e2 & (op(op(e4,e2),op(e2,e4)) = e2 & (op(op(e0,e3),op(e3,e0)) = e3 & (op(op(e1,e3),op(e3,e1)) = e3 & (op(op(e2,e3),op(e3,e2)) = e3 & (op(op(e3,e3),op(e3,e3)) = e3 & (op(op(e4,e3),op(e3,e4)) = e3 & (op(op(e0,e4),op(e4,e0)) = e4 & (op(op(e1,e4),op(e4,e1)) = e4 & (op(op(e2,e4),op(e4,e2)) = e4 & (op(op(e3,e4),op(e4,e3)) = e4 & op(op(e4,e4),op(e4,e4)) = e4))))))))))))))))))))))))). % 131.54/17.51 fof(ax4, axiom, (op(e0,e0) != op(e1,e0) & (op(e0,e0) != op(e2,e0) & (op(e0,e0) != op(e3,e0) & (op(e0,e0) != op(e4,e0) & (op(e1,e0) != op(e2,e0) & (op(e1,e0) != op(e3,e0) & (op(e1,e0) != op(e4,e0) & (op(e2,e0) != op(e3,e0) & (op(e2,e0) != op(e4,e0) & (op(e3,e0) != op(e4,e0) & (op(e0,e1) != op(e1,e1) & (op(e0,e1) != op(e2,e1) & (op(e0,e1) != op(e3,e1) & (op(e0,e1) != op(e4,e1) & (op(e1,e1) != op(e2,e1) & (op(e1,e1) != op(e3,e1) & (op(e1,e1) != op(e4,e1) & (op(e2,e1) != op(e3,e1) & (op(e2,e1) != op(e4,e1) & (op(e3,e1) != op(e4,e1) & (op(e0,e2) != op(e1,e2) & (op(e0,e2) != op(e2,e2) & (op(e0,e2) != op(e3,e2) & (op(e0,e2) != op(e4,e2) & (op(e1,e2) != op(e2,e2) & (op(e1,e2) != op(e3,e2) & (op(e1,e2) != op(e4,e2) & (op(e2,e2) != op(e3,e2) & (op(e2,e2) != op(e4,e2) & (op(e3,e2) != op(e4,e2) & (op(e0,e3) != op(e1,e3) & (op(e0,e3) != op(e2,e3) & (op(e0,e3) != op(e3,e3) & (op(e0,e3) != op(e4,e3) & (op(e1,e3) != op(e2,e3) & (op(e1,e3) != op(e3,e3) & (op(e1,e3) != op(e4,e3) & (op(e2,e3) != op(e3,e3) & (op(e2,e3) != op(e4,e3) & (op(e3,e3) != op(e4,e3) & (op(e0,e4) != op(e1,e4) & (op(e0,e4) != op(e2,e4) & (op(e0,e4) != op(e3,e4) & (op(e0,e4) != op(e4,e4) & (op(e1,e4) != op(e2,e4) & (op(e1,e4) != op(e3,e4) & (op(e1,e4) != op(e4,e4) & (op(e2,e4) != op(e3,e4) & (op(e2,e4) != op(e4,e4) & (op(e3,e4) != op(e4,e4) & (op(e0,e0) != op(e0,e1) & (op(e0,e0) != op(e0,e2) & (op(e0,e0) != op(e0,e3) & (op(e0,e0) != op(e0,e4) & (op(e0,e1) != op(e0,e2) & (op(e0,e1) != op(e0,e3) & (op(e0,e1) != op(e0,e4) & (op(e0,e2) != op(e0,e3) & (op(e0,e2) != op(e0,e4) & (op(e0,e3) != op(e0,e4) & (op(e1,e0) != op(e1,e1) & (op(e1,e0) != op(e1,e2) & (op(e1,e0) != op(e1,e3) & (op(e1,e0) != op(e1,e4) & (op(e1,e1) != op(e1,e2) & (op(e1,e1) != op(e1,e3) & (op(e1,e1) != op(e1,e4) & (op(e1,e2) != op(e1,e3) & (op(e1,e2) != op(e1,e4) & (op(e1,e3) != op(e1,e4) & (op(e2,e0) != op(e2,e1) & (op(e2,e0) != op(e2,e2) & (op(e2,e0) != op(e2,e3) & (op(e2,e0) != op(e2,e4) & (op(e2,e1) != op(e2,e2) & (op(e2,e1) != op(e2,e3) & (op(e2,e1) != op(e2,e4) & (op(e2,e2) != op(e2,e3) & (op(e2,e2) != op(e2,e4) & (op(e2,e3) != op(e2,e4) & (op(e3,e0) != op(e3,e1) & (op(e3,e0) != op(e3,e2) & (op(e3,e0) != op(e3,e3) & (op(e3,e0) != op(e3,e4) & (op(e3,e1) != op(e3,e2) & (op(e3,e1) != op(e3,e3) & (op(e3,e1) != op(e3,e4) & (op(e3,e2) != op(e3,e3) & (op(e3,e2) != op(e3,e4) & (op(e3,e3) != op(e3,e4) & (op(e4,e0) != op(e4,e1) & (op(e4,e0) != op(e4,e2) & (op(e4,e0) != op(e4,e3) & (op(e4,e0) != op(e4,e4) & (op(e4,e1) != op(e4,e2) & (op(e4,e1) != op(e4,e3) & (op(e4,e1) != op(e4,e4) & (op(e4,e2) != op(e4,e3) & (op(e4,e2) != op(e4,e4) & op(e4,e3) != op(e4,e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 131.54/17.51 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 131.54/17.51 fof(ax6, axiom, (e0 = op(e4,op(e4,e4)) & (e1 = op(e4,e4) & (e2 = op(op(e4,op(e4,e4)),op(e4,e4)) & e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4))))))). % 131.54/17.51 fof(co1, conjecture, ~((((op(e0,e0) != e0 & (op(e1,e0) != e1 & (op(e2,e0) != e2 & (op(e3,e0) != e3 & op(e4,e0) != e4)))) | ((op(e0,e1) != e0 & (op(e1,e1) != e1 & (op(e2,e1) != e2 & (op(e3,e1) != e3 & op(e4,e1) != e4)))) | ((op(e0,e2) != e0 & (op(e1,e2) != e1 & (op(e2,e2) != e2 & (op(e3,e2) != e3 & op(e4,e2) != e4)))) | ((op(e0,e3) != e0 & (op(e1,e3) != e1 & (op(e2,e3) != e2 & (op(e3,e3) != e3 & op(e4,e3) != e4)))) | (op(e0,e4) != e0 & (op(e1,e4) != e1 & (op(e2,e4) != e2 & (op(e3,e4) != e3 & op(e4,e4) != e4)))))))) & ((op(e0,e0) != e0 & (op(e0,e1) != e1 & (op(e0,e2) != e2 & (op(e0,e3) != e3 & op(e0,e4) != e4)))) | ((op(e1,e0) != e0 & (op(e1,e1) != e1 & (op(e1,e2) != e2 & (op(e1,e3) != e3 & op(e1,e4) != e4)))) | ((op(e2,e0) != e0 & (op(e2,e1) != e1 & (op(e2,e2) != e2 & (op(e2,e3) != e3 & op(e2,e4) != e4)))) | ((op(e3,e0) != e0 & (op(e3,e1) != e1 & (op(e3,e2) != e2 & (op(e3,e3) != e3 & op(e3,e4) != e4)))) | (op(e4,e0) != e0 & (op(e4,e1) != e1 & (op(e4,e2) != e2 & (op(e4,e3) != e3 & op(e4,e4) != e4))))))))))). % 131.54/17.51 fof(negated_conjecture, negated_conjecture, ~~((((op(e0,e0) != e0 & (op(e1,e0) != e1 & (op(e2,e0) != e2 & (op(e3,e0) != e3 & op(e4,e0) != e4)))) | ((op(e0,e1) != e0 & (op(e1,e1) != e1 & (op(e2,e1) != e2 & (op(e3,e1) != e3 & op(e4,e1) != e4)))) | ((op(e0,e2) != e0 & (op(e1,e2) != e1 & (op(e2,e2) != e2 & (op(e3,e2) != e3 & op(e4,e2) != e4)))) | ((op(e0,e3) != e0 & (op(e1,e3) != e1 & (op(e2,e3) != e2 & (op(e3,e3) != e3 & op(e4,e3) != e4)))) | (op(e0,e4) != e0 & (op(e1,e4) != e1 & (op(e2,e4) != e2 & (op(e3,e4) != e3 & op(e4,e4) != e4)))))))) & ((op(e0,e0) != e0 & (op(e0,e1) != e1 & (op(e0,e2) != e2 & (op(e0,e3) != e3 & op(e0,e4) != e4)))) | ((op(e1,e0) != e0 & (op(e1,e1) != e1 & (op(e1,e2) != e2 & (op(e1,e3) != e3 & op(e1,e4) != e4)))) | ((op(e2,e0) != e0 & (op(e2,e1) != e1 & (op(e2,e2) != e2 & (op(e2,e3) != e3 & op(e2,e4) != e4)))) | ((op(e3,e0) != e0 & (op(e3,e1) != e1 & (op(e3,e2) != e2 & (op(e3,e3) != e3 & op(e3,e4) != e4)))) | (op(e4,e0) != e0 & (op(e4,e1) != e1 & (op(e4,e2) != e2 & (op(e4,e3) != e3 & op(e4,e4) != e4)))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 131.54/17.51 cnf(c3, plain, op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1 | op(e0,e3) = e0 | op(e0,e3) = e3, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c4, plain, op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e3 | op(e0,e4) = e1 | op(e0,e4) = e0, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c5, plain, op(e1,e0) = e0 | op(e1,e0) = e4 | op(e1,e0) = e1 | op(e1,e0) = e3 | op(e1,e0) = e2, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c13, plain, op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e4, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c15, plain, op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e4 | op(e3,e0) = e3 | op(e3,e0) = e2, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c19, plain, op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e4, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c20, plain, op(e4,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e4 | op(e4,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 131.54/17.51 cnf(c25, plain, op(e0,e2) = e0 | op(e0,e1) = e0 | op(e0,e4) = e0 | op(e0,e3) = e0 | op(e0,e0) = e0, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c26, plain, op(e2,e0) = e0 | op(e1,e0) = e0 | op(e3,e0) = e0 | op(e4,e0) = e0 | op(e0,e0) = e0, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c27, plain, op(e0,e1) = e1 | op(e0,e4) = e1 | op(e0,e0) = e1 | op(e0,e2) = e1 | op(e0,e3) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c28, plain, op(e2,e0) = e1 | op(e4,e0) = e1 | op(e1,e0) = e1 | op(e0,e0) = e1 | op(e3,e0) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c30, plain, op(e2,e0) = e2 | op(e0,e0) = e2 | op(e1,e0) = e2 | op(e3,e0) = e2 | op(e4,e0) = e2, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c33, plain, op(e0,e1) = e4 | op(e0,e2) = e4 | op(e0,e3) = e4 | op(e0,e4) = e4 | op(e0,e0) = e4, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c34, plain, op(e1,e0) = e4 | op(e3,e0) = e4 | op(e4,e0) = e4 | op(e2,e0) = e4 | op(e0,e0) = e4, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c36, plain, op(e4,e1) = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | op(e0,e1) = e0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c37, plain, op(e1,e4) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | op(e1,e1) = e1 | op(e1,e2) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c38, plain, op(e2,e1) = e1 | op(e4,e1) = e1 | op(e0,e1) = e1 | op(e1,e1) = e1 | op(e3,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c39, plain, op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e1) = e2 | op(e1,e4) = e2 | op(e1,e0) = e2, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c41, plain, op(e1,e3) = e3 | op(e1,e0) = e3 | op(e1,e4) = e3 | op(e1,e2) = e3 | op(e1,e1) = e3, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c42, plain, op(e0,e1) = e3 | op(e4,e1) = e3 | op(e1,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c45, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e4) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c49, plain, op(e2,e1) = e2 | op(e2,e3) = e2 | op(e2,e0) = e2 | op(e2,e4) = e2 | op(e2,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c57, plain, op(e3,e4) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1 | op(e3,e3) = e1 | op(e3,e0) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c58, plain, op(e2,e3) = e1 | op(e1,e3) = e1 | op(e0,e3) = e1 | op(e4,e3) = e1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c59, plain, op(e3,e2) = e2 | op(e3,e3) = e2 | op(e3,e1) = e2 | op(e3,e0) = e2 | op(e3,e4) = e2, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c62, plain, op(e2,e3) = e3 | op(e1,e3) = e3 | op(e3,e3) = e3 | op(e0,e3) = e3 | op(e4,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c64, plain, op(e4,e3) = e4 | op(e1,e3) = e4 | op(e0,e3) = e4 | op(e2,e3) = e4 | op(e3,e3) = e4, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c69, plain, op(e4,e2) = e2 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e4) = e2 | op(e4,e1) = e2, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c71, plain, op(e4,e2) = e3 | op(e4,e4) = e3 | op(e4,e1) = e3 | op(e4,e0) = e3 | op(e4,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c73, plain, op(e4,e3) = e4 | op(e4,e4) = e4 | op(e4,e1) = e4 | op(e4,e0) = e4 | op(e4,e2) = e4, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c74, plain, op(e4,e4) = e4 | op(e2,e4) = e4 | op(e0,e4) = e4 | op(e1,e4) = e4 | op(e3,e4) = e4, inference(clausification, [status(esa)], [ax2])). % 131.54/17.51 cnf(c75, plain, op(op(e0,e0),op(e0,e0)) = e0, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c76, plain, op(op(e1,e0),op(e0,e1)) = e0, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c77, plain, op(op(e2,e0),op(e0,e2)) = e0, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c78, plain, op(op(e3,e0),op(e0,e3)) = e0, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c79, plain, op(op(e4,e0),op(e0,e4)) = e0, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c80, plain, op(op(e0,e1),op(e1,e0)) = e1, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c81, plain, op(op(e1,e1),op(e1,e1)) = e1, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c82, plain, op(op(e2,e1),op(e1,e2)) = e1, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c84, plain, op(op(e4,e1),op(e1,e4)) = e1, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c86, plain, op(op(e1,e2),op(e2,e1)) = e2, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c89, plain, op(op(e4,e2),op(e2,e4)) = e2, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c90, plain, op(op(e0,e3),op(e3,e0)) = e3, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c91, plain, op(op(e1,e3),op(e3,e1)) = e3, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c92, plain, op(op(e2,e3),op(e3,e2)) = e3, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c94, plain, op(op(e4,e3),op(e3,e4)) = e3, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c95, plain, op(op(e0,e4),op(e4,e0)) = e4, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c98, plain, op(op(e3,e4),op(e4,e3)) = e4, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c99, plain, op(op(e4,e4),op(e4,e4)) = e4, inference(clausification, [status(esa)], [ax3])). % 131.54/17.51 cnf(c100, plain, op(e0,e0) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c101, plain, op(e0,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c102, plain, op(e0,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c105, plain, op(e1,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c106, plain, op(e1,e0) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c107, plain, op(e2,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c108, plain, op(e2,e0) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c109, plain, op(e3,e0) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c110, plain, op(e0,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c111, plain, op(e0,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c112, plain, op(e0,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c113, plain, op(e0,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c114, plain, op(e1,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c116, plain, op(e1,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c117, plain, op(e2,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c118, plain, op(e2,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c119, plain, op(e3,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c120, plain, op(e0,e2) != op(e1,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c121, plain, op(e0,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c122, plain, op(e0,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c123, plain, op(e0,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c130, plain, op(e0,e3) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c131, plain, op(e0,e3) != op(e2,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c132, plain, op(e0,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c135, plain, op(e1,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c137, plain, op(e2,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c141, plain, op(e0,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c142, plain, op(e0,e4) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c143, plain, op(e0,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c146, plain, op(e1,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c148, plain, op(e2,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c149, plain, op(e3,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c150, plain, op(e0,e0) != op(e0,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c151, plain, op(e0,e0) != op(e0,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c152, plain, op(e0,e0) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c153, plain, op(e0,e0) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c155, plain, op(e0,e1) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c157, plain, op(e0,e2) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c159, plain, op(e0,e3) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c160, plain, op(e1,e0) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c163, plain, op(e1,e0) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c165, plain, op(e1,e1) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c166, plain, op(e1,e1) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c169, plain, op(e1,e3) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c170, plain, op(e2,e0) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c171, plain, op(e2,e0) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c173, plain, op(e2,e0) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c175, plain, op(e2,e1) != op(e2,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c176, plain, op(e2,e1) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c179, plain, op(e2,e3) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c180, plain, op(e3,e0) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c182, plain, op(e3,e0) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c184, plain, op(e3,e1) != op(e3,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c186, plain, op(e3,e1) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c189, plain, op(e3,e3) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c190, plain, op(e4,e0) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c191, plain, op(e4,e0) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c192, plain, op(e4,e0) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c193, plain, op(e4,e0) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c198, plain, op(e4,e2) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c199, plain, op(e4,e3) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 131.54/17.51 cnf(c200, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c201, plain, e0 != e2, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c202, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c203, plain, e0 != e4, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c204, plain, e1 != e2, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c205, plain, e1 != e3, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c206, plain, e1 != e4, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c207, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c208, plain, e2 != e4, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c209, plain, e3 != e4, inference(clausification, [status(esa)], [ax5])). % 131.54/17.51 cnf(c210, plain, e0 = op(e4,op(e4,e4)), inference(clausification, [status(esa)], [ax6])). % 131.54/17.51 cnf(c211, plain, e1 = op(e4,e4), inference(clausification, [status(esa)], [ax6])). % 131.54/17.51 cnf(c212, plain, e2 = op(op(e4,op(e4,e4)),op(e4,e4)), inference(clausification, [status(esa)], [ax6])). % 131.54/17.51 cnf(c213, plain, e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4))), inference(clausification, [status(esa)], [ax6])). % 131.54/17.51 cnf(c214, plain, X0 | X1 | X2 | X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c215, plain, X0 | X1 | X2 | X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c220, plain, ~X0 | op(e4,e3) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c221, plain, ~X0 | op(e0,e4) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c228, plain, ~X0 | op(e2,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c234, plain, ~X0 | op(e3,e1) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c237, plain, ~X0 | op(e1,e0) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c242, plain, ~X0 | op(e3,e1) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c248, plain, ~X0 | op(e4,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c249, plain, ~X0 | op(e4,e3) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c251, plain, ~X0 | op(e2,e0) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c252, plain, ~X0 | op(e2,e1) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c253, plain, ~X0 | op(e2,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c256, plain, ~X0 | op(e1,e0) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c259, plain, ~X0 | op(e1,e3) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c262, plain, ~X0 | op(e0,e1) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(c265, plain, ~X0 | op(e0,e4) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 131.54/17.51 cnf(d0, plain, e0 = op(e4,e1), inference(demodulation, [status(thm)], [c210,c211])). % 131.54/17.51 cnf(d1, plain, e3 = op(op(e4,e1),op(e4,op(e4,e4))), inference(demodulation, [status(thm)], [c213,c211])). % 131.54/17.51 cnf(d2, plain, e3 = op(e0,op(e4,op(e4,e4))), inference(demodulation, [status(thm)], [d1,d0])). % 131.54/17.51 cnf(d3, plain, e3 = op(e0,op(e4,e1)), inference(demodulation, [status(thm)], [d2,c211])). % 131.54/17.51 cnf(d4, plain, e3 = op(e0,e0), inference(demodulation, [status(thm)], [d3,d0])). % 131.54/17.51 cnf(d5, plain, op(e3,op(e0,e0)) = e0, inference(demodulation, [status(thm)], [c75,d4])). % 131.54/17.51 cnf(d6, plain, op(e3,e3) = e0, inference(demodulation, [status(thm)], [d5,d4])). % 131.54/17.51 cnf(d7, plain, e2 = op(op(e4,e1),op(e4,e4)), inference(demodulation, [status(thm)], [c212,c211])). % 131.54/17.51 cnf(d8, plain, e2 = op(e0,op(e4,e4)), inference(demodulation, [status(thm)], [d7,d0])). % 131.54/17.51 cnf(d9, plain, e2 = op(e0,e1), inference(demodulation, [status(thm)], [d8,c211])). % 131.54/17.51 cnf(d10, plain, op(e0,e1) != e2 | op(e3,e0) = e2 | op(e3,e3) = e2 | op(e3,e2) = e2 | op(e3,e4) = e2, inference(superposition, [status(thm)], [c59,c112])). % 131.54/17.51 cnf(d11, plain, e2 != e2 | op(e3,e0) = e2 | op(e3,e3) = e2 | op(e3,e2) = e2 | op(e3,e4) = e2, inference(demodulation, [status(thm)], [d10,d9])). % 131.54/17.51 cnf(d12, plain, e2 != e2 | op(e3,e0) = e2 | e0 = e2 | op(e3,e2) = e2 | op(e3,e4) = e2, inference(demodulation, [status(thm)], [d11,d6])). % 131.54/17.51 cnf(d13, plain, e2 != e2 | op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e4) = e2, inference(resolution, [status(thm)], [c201,d12])). % 131.54/17.51 cnf(d14, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e4) = e2, inference(equality_resolution, [status(thm)], [d13])). % 131.54/17.51 cnf(d15, plain, op(e4,e2) != e1, inference(demodulation, [status(thm)], [c198,c211])). % 131.54/17.51 cnf(d16, plain, e3 != op(e0,e3), inference(demodulation, [status(thm)], [c152,d4])). % 131.54/17.51 cnf(d17, plain, e2 != op(e0,e3), inference(demodulation, [status(thm)], [c155,d9])). % 131.54/17.51 cnf(d18, plain, op(op(e3,e0),e1) = e0 | op(e0,e3) = e0 | op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4, inference(superposition, [status(thm)], [c3,c78])). % 131.54/17.51 cnf(d19, plain, op(e0,e3) != e0, inference(demodulation, [status(thm)], [c132,d6])). % 131.54/17.51 cnf(d20, plain, op(op(e3,e0),e1) = e0 | op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4, inference(resolution, [status(thm)], [d19,d18])). % 131.54/17.51 cnf(d21, plain, e2 != op(e3,e0) | op(e0,e0) = e2 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(superposition, [status(thm)], [c30,c105])). % 131.54/17.51 cnf(d22, plain, e3 = e2 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | e2 != op(e3,e0), inference(demodulation, [status(thm)], [d21,d4])). % 131.54/17.51 cnf(d23, plain, op(e0,e0) != e2, inference(demodulation, [status(thm)], [c150,d9])). % 131.54/17.51 cnf(d24, plain, e3 != e2, inference(demodulation, [status(thm)], [d23,d4])). % 131.54/17.51 cnf(d25, plain, op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | e2 != op(e3,e0), inference(resolution, [status(thm)], [d24,d22])). % 131.54/17.51 cnf(d26, plain, op(e1,op(e4,e4)) = e4, inference(demodulation, [status(thm)], [c99,c211])). % 131.54/17.51 cnf(d27, plain, op(e1,e1) = e4, inference(demodulation, [status(thm)], [d26,c211])). % 131.54/17.51 cnf(d28, plain, op(e3,op(e1,e1)) = e1 | op(e0,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(superposition, [status(thm)], [c42,c81])). % 131.54/17.51 cnf(d29, plain, e2 = e3 | op(e3,op(e1,e1)) = e1 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d28,d9])). % 131.54/17.51 cnf(d30, plain, e2 = e3 | op(e3,e4) = e1 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d29,d27])). % 131.54/17.51 cnf(d31, plain, e2 = e3 | op(e3,e4) = e1 | op(e3,e1) = e3 | op(e2,e1) = e3 | e0 = e3, inference(demodulation, [status(thm)], [d30,d0])). % 131.54/17.51 cnf(d32, plain, e2 = e3 | op(e3,e4) = e1 | op(e3,e1) = e3 | op(e2,e1) = e3, inference(resolution, [status(thm)], [c202,d31])). % 131.54/17.51 cnf(d33, plain, op(e3,e4) = e1 | op(e3,e1) = e3 | op(e2,e1) = e3, inference(resolution, [status(thm)], [c207,d32])). % 131.54/17.51 cnf(d34, plain, op(e3,e4) != e1, inference(demodulation, [status(thm)], [c149,c211])). % 131.54/17.51 cnf(d35, plain, op(e3,e1) = e3 | op(e2,e1) = e3, inference(resolution, [status(thm)], [d34,d33])). % 131.54/17.51 cnf(d36, plain, op(e1,op(e1,e1)) = e1 | op(e0,e1) = e1 | op(e3,e1) = e1 | op(e2,e1) = e1 | op(e4,e1) = e1, inference(superposition, [status(thm)], [c38,c81])). % 131.54/17.51 cnf(d37, plain, e2 = e1 | op(e3,e1) = e1 | op(e2,e1) = e1 | op(e4,e1) = e1 | op(e1,op(e1,e1)) = e1, inference(demodulation, [status(thm)], [d36,d9])). % 131.54/17.51 cnf(d38, plain, e2 = e1 | op(e3,e1) = e1 | op(e2,e1) = e1 | e0 = e1 | op(e1,op(e1,e1)) = e1, inference(demodulation, [status(thm)], [d37,d0])). % 131.54/17.51 cnf(d39, plain, e2 = e1 | op(e3,e1) = e1 | op(e2,e1) = e1 | e0 = e1 | op(e1,e4) = e1, inference(demodulation, [status(thm)], [d38,d27])). % 131.54/17.51 cnf(d40, plain, e2 = e1 | op(e3,e1) = e1 | op(e2,e1) = e1 | op(e1,e4) = e1, inference(resolution, [status(thm)], [c200,d39])). % 131.54/17.51 cnf(d41, plain, op(e1,e4) != e1, inference(demodulation, [status(thm)], [c146,c211])). % 131.54/17.51 cnf(d42, plain, op(e3,e1) = e1 | op(e2,e1) = e1 | e2 = e1, inference(resolution, [status(thm)], [d41,d40])). % 131.54/17.51 cnf(d43, plain, e1 = e3 | op(e3,e1) = e3 | op(e3,e1) = e1 | e2 = e1, inference(superposition, [status(thm)], [d42,d35])). % 131.54/17.51 cnf(d44, plain, op(e3,e1) = e3 | op(e3,e1) = e1 | e2 = e1, inference(resolution, [status(thm)], [c205,d43])). % 131.54/17.51 cnf(d45, plain, op(e3,e0) != e1 | op(e3,e1) = e3 | e2 = e1, inference(superposition, [status(thm)], [d44,c180])). % 131.54/17.51 cnf(d46, plain, op(e3,e0) = e1 | op(e3,e3) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(resolution, [status(thm)], [d34,c57])). % 131.54/17.51 cnf(d47, plain, op(e3,e0) = e1 | e0 = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(demodulation, [status(thm)], [d46,d6])). % 131.54/17.51 cnf(d48, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(resolution, [status(thm)], [c200,d47])). % 131.54/17.51 cnf(d49, plain, e2 = e0 | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0 | op(e0,e0) = e2 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(superposition, [status(thm)], [c30,c26])). % 131.54/17.51 cnf(d50, plain, e3 = e0 | op(e0,e0) = e2 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e2 | e2 = e0, inference(demodulation, [status(thm)], [d49,d4])). % 131.54/17.51 cnf(d51, plain, e3 = e0 | e3 = e2 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e2 | e2 = e0, inference(demodulation, [status(thm)], [d50,d4])). % 131.54/17.51 cnf(d52, plain, e3 = e0 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e2 | e2 = e0, inference(resolution, [status(thm)], [d24,d51])). % 131.54/17.51 cnf(d53, plain, op(e0,e1) != e0, inference(demodulation, [status(thm)], [c113,d0])). % 131.54/17.51 cnf(d54, plain, e2 != e0, inference(demodulation, [status(thm)], [d53,d9])). % 131.54/17.51 cnf(d55, plain, op(e3,e0) = e0 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e2 | e3 = e0, inference(resolution, [status(thm)], [d54,d52])). % 131.54/17.51 cnf(d56, plain, op(e4,e0) != e0, inference(demodulation, [status(thm)], [c190,d0])). % 131.54/17.51 cnf(d57, plain, op(e3,e0) = e0 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e2 | e3 = e0, inference(resolution, [status(thm)], [d56,d55])). % 131.54/17.51 cnf(d58, plain, op(e3,e0) != e0, inference(demodulation, [status(thm)], [c182,d6])). % 131.54/17.51 cnf(d59, plain, op(e3,e0) = e2 | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e4,e0) = e2 | e3 = e0, inference(resolution, [status(thm)], [d58,d57])). % 131.54/17.51 cnf(d60, plain, op(op(e0,e1),e1) = e1 | op(e0,e0) = e1 | op(e3,e0) = e1 | op(e2,e0) = e1 | op(e4,e0) = e1, inference(superposition, [status(thm)], [c28,c80])). % 131.54/17.51 cnf(d61, plain, op(e2,e1) = e1 | op(e0,e0) = e1 | op(e3,e0) = e1 | op(e2,e0) = e1 | op(e4,e0) = e1, inference(demodulation, [status(thm)], [d60,d9])). % 131.54/17.51 cnf(d62, plain, op(e2,e1) = e1 | e3 = e1 | op(e3,e0) = e1 | op(e2,e0) = e1 | op(e4,e0) = e1, inference(demodulation, [status(thm)], [d61,d4])). % 131.54/17.51 cnf(d63, plain, op(e4,e0) != e1, inference(demodulation, [status(thm)], [c193,c211])). % 131.54/17.51 cnf(d64, plain, op(e2,e1) = e1 | e3 = e1 | op(e3,e0) = e1 | op(e2,e0) = e1, inference(resolution, [status(thm)], [d63,d62])). % 131.54/17.51 cnf(d65, plain, e1 != e1 | ~'Ts7' | op(e3,e0) = e1 | op(e2,e0) = e1 | e3 = e1, inference(superposition, [status(thm)], [d64,c252])). % 131.54/17.51 cnf(d66, plain, op(e3,e0) = e1 | op(e2,e0) = e1 | e3 = e1 | ~'Ts7', inference(equality_resolution, [status(thm)], [d65])). % 131.54/17.51 cnf(d67, plain, e0 != e0 | ~'Ts8' | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(superposition, [status(thm)], [c26,c256])). % 131.54/17.51 cnf(d68, plain, e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0 | e0 != e0 | ~'Ts8', inference(demodulation, [status(thm)], [d67,d4])). % 131.54/17.51 cnf(d69, plain, e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | e0 != e0 | ~'Ts8', inference(resolution, [status(thm)], [d56,d68])). % 131.54/17.51 cnf(d70, plain, op(e2,e0) = e0 | e0 != e0 | e3 = e0 | ~'Ts8', inference(resolution, [status(thm)], [d58,d69])). % 131.54/17.51 cnf(d71, plain, op(e2,e0) = e0 | e3 = e0 | ~'Ts8', inference(equality_resolution, [status(thm)], [d70])). % 131.54/17.51 cnf(d72, plain, e1 != e1 | ~'Ts5' | op(e3,e1) = e3 | e2 = e1, inference(superposition, [status(thm)], [d44,c242])). % 131.54/17.51 cnf(d73, plain, op(e3,e1) = e3 | e2 = e1 | ~'Ts5', inference(equality_resolution, [status(thm)], [d72])). % 131.54/17.51 cnf(d74, plain, op(e3,e1) = e3 | e2 = e1 | 'Ts9' | 'Ts6' | 'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d73,c215])). % 131.54/17.51 cnf(d75, plain, op(e3,e1) = e3 | e2 = e1 | 'Ts9' | 'Ts6' | 'Ts7' | op(e2,e0) = e0 | e3 = e0, inference(resolution, [status(thm)], [d74,d71])). % 131.54/17.51 cnf(d76, plain, op(e2,e1) != e0, inference(demodulation, [status(thm)], [c118,d0])). % 131.54/17.51 cnf(d77, plain, e3 != e0 | op(e3,e1) = e3, inference(superposition, [status(thm)], [d35,d76])). % 131.54/17.51 cnf(d78, plain, op(e3,e1) = e3 | op(e3,e1) = e3 | op(e2,e0) = e0 | e2 = e1 | 'Ts9' | 'Ts6' | 'Ts7', inference(resolution, [status(thm)], [d77,d75])). % 131.54/17.51 cnf(d79, plain, op(e3,e1) = e3 | op(e2,e0) = e0 | e2 = e1 | 'Ts9' | 'Ts6' | op(e3,e0) = e1 | op(e2,e0) = e1 | e3 = e1, inference(resolution, [status(thm)], [d78,d66])). % 131.54/17.51 cnf(d80, plain, e2 != op(e2,e1), inference(demodulation, [status(thm)], [c111,d9])). % 131.54/17.51 cnf(d81, plain, e2 != e1 | op(e3,e0) = e1 | op(e2,e0) = e1 | e3 = e1, inference(superposition, [status(thm)], [d64,d80])). % 131.54/17.51 cnf(d82, plain, op(e3,e0) = e1 | op(e2,e0) = e1 | e3 = e1 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e2,e0) = e1 | e3 = e1 | 'Ts9' | 'Ts6', inference(resolution, [status(thm)], [d81,d79])). % 131.54/17.51 cnf(d83, plain, op(e0,e1) != e4, inference(demodulation, [status(thm)], [c110,d27])). % 131.54/17.51 cnf(d84, plain, op(e0,e0) = e4 | op(e0,e3) = e4 | op(e0,e2) = e4 | op(e0,e4) = e4, inference(resolution, [status(thm)], [d83,c33])). % 131.54/17.51 cnf(d85, plain, e3 = e4 | op(e0,e3) = e4 | op(e0,e2) = e4 | op(e0,e4) = e4, inference(demodulation, [status(thm)], [d84,d4])). % 131.54/17.51 cnf(d86, plain, op(e0,e3) = e4 | op(e0,e2) = e4 | op(e0,e4) = e4, inference(resolution, [status(thm)], [c209,d85])). % 131.54/17.51 cnf(d87, plain, e4 != op(e4,e2) | op(e0,e3) = e4 | op(e0,e4) = e4, inference(superposition, [status(thm)], [d86,c123])). % 131.54/17.51 cnf(d88, plain, e4 != op(e1,e3), inference(demodulation, [status(thm)], [c165,d27])). % 131.54/17.51 cnf(d89, plain, e4 != e4 | op(e0,e3) = e4 | op(e3,e3) = e4 | op(e2,e3) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [c64,d88])). % 131.54/17.51 cnf(d90, plain, op(e0,e3) = e4 | e0 = e4 | op(e2,e3) = e4 | op(e4,e3) = e4 | e4 != e4, inference(demodulation, [status(thm)], [d89,d6])). % 131.54/17.51 cnf(d91, plain, op(e0,e3) = e4 | op(e2,e3) = e4 | op(e4,e3) = e4 | e4 != e4, inference(resolution, [status(thm)], [c203,d90])). % 131.54/17.51 cnf(d92, plain, op(e0,e3) = e4 | op(e2,e3) = e4 | op(e4,e3) = e4, inference(equality_resolution, [status(thm)], [d91])). % 131.54/17.51 cnf(d93, plain, e3 != op(e1,e4) | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [c62,c169])). % 131.54/17.51 cnf(d94, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != op(e1,e4), inference(demodulation, [status(thm)], [d93,d6])). % 131.54/17.51 cnf(d95, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != op(e1,e4), inference(resolution, [status(thm)], [c202,d94])). % 131.54/17.51 cnf(d96, plain, op(e2,e3) != e0, inference(demodulation, [status(thm)], [c137,d6])). % 131.54/17.51 cnf(d97, plain, e1 = e3 | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1, inference(superposition, [status(thm)], [c58,c62])). % 131.54/17.51 cnf(d98, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | e0 = e3 | op(e3,e3) = e1 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3 | op(e4,e3) = e1 | e1 = e3, inference(demodulation, [status(thm)], [d97,d6])). % 131.54/17.51 cnf(d99, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | e0 = e3 | e0 = e1 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3 | op(e4,e3) = e1 | e1 = e3, inference(demodulation, [status(thm)], [d98,d6])). % 131.54/17.51 cnf(d100, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | e0 = e3 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3 | op(e4,e3) = e1 | e1 = e3, inference(resolution, [status(thm)], [c200,d99])). % 131.54/17.51 cnf(d101, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3 | op(e4,e3) = e1 | e1 = e3, inference(resolution, [status(thm)], [c202,d100])). % 131.54/17.51 cnf(d102, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3 | op(e4,e3) = e1, inference(resolution, [status(thm)], [c205,d101])). % 131.54/17.51 cnf(d103, plain, op(e4,e3) != e1, inference(demodulation, [status(thm)], [c199,c211])). % 131.54/17.51 cnf(d104, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e2,e3) = e1 | op(e4,e3) = e3, inference(resolution, [status(thm)], [d103,d102])). % 131.54/17.51 cnf(d105, plain, op(e0,e3) != e1 | op(e2,e3) = e0 | op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e4, inference(superposition, [status(thm)], [c13,c131])). % 131.54/17.51 cnf(d106, plain, op(e0,e3) != e1 | op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e4, inference(resolution, [status(thm)], [d96,d105])). % 131.54/17.51 cnf(d107, plain, op(e0,e4) != e1, inference(demodulation, [status(thm)], [c143,c211])). % 131.54/17.51 cnf(d108, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | op(e0,e1) = e1, inference(resolution, [status(thm)], [d107,c27])). % 131.54/17.51 cnf(d109, plain, e3 = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | op(e0,e1) = e1, inference(demodulation, [status(thm)], [d108,d4])). % 131.54/17.51 cnf(d110, plain, e3 = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | e2 = e1, inference(demodulation, [status(thm)], [d109,d9])). % 131.54/17.51 cnf(d111, plain, op(e0,op(e0,e1)) = e0 | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(superposition, [status(thm)], [c26,c76])). % 131.54/17.51 cnf(d112, plain, op(e0,e2) = e0 | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(demodulation, [status(thm)], [d111,d9])). % 131.54/17.51 cnf(d113, plain, op(e0,e2) = e0 | e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(demodulation, [status(thm)], [d112,d4])). % 131.54/17.51 cnf(d114, plain, op(e0,e2) = e0 | e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0, inference(resolution, [status(thm)], [d56,d113])). % 131.54/17.51 cnf(d115, plain, op(e0,e2) = e0 | op(e2,e0) = e0 | e3 = e0, inference(resolution, [status(thm)], [d58,d114])). % 131.54/17.51 cnf(d116, plain, op(e0,op(e0,e2)) = e0 | op(e0,e2) = e0 | e3 = e0, inference(superposition, [status(thm)], [d115,c77])). % 131.54/17.51 cnf(d117, plain, op(e0,e3) = e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e1,e3) = e1, inference(resolution, [status(thm)], [d103,c58])). % 131.54/17.51 cnf(d118, plain, op(e0,e3) = e1 | e0 = e1 | op(e2,e3) = e1 | op(e1,e3) = e1, inference(demodulation, [status(thm)], [d117,d6])). % 131.54/17.51 cnf(d119, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e1,e3) = e1, inference(resolution, [status(thm)], [c200,d118])). % 131.54/17.51 cnf(d120, plain, op(e1,op(e3,e1)) = e3 | op(e0,e3) = e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1, inference(superposition, [status(thm)], [c58,c91])). % 131.54/17.51 cnf(d121, plain, op(e0,e3) = e1 | e0 = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | op(e1,op(e3,e1)) = e3, inference(demodulation, [status(thm)], [d120,d6])). % 131.54/17.51 cnf(d122, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | op(e1,op(e3,e1)) = e3, inference(resolution, [status(thm)], [c200,d121])). % 131.54/17.51 cnf(d123, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e1,op(e3,e1)) = e3, inference(resolution, [status(thm)], [d103,d122])). % 131.54/17.51 cnf(d124, plain, e3 != op(e2,e3) | op(e3,e1) = e3, inference(superposition, [status(thm)], [d35,c175])). % 131.54/17.51 cnf(d125, plain, e1 != e1 | ~'Ts9' | op(e0,e0) = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | op(e0,e4) = e1, inference(superposition, [status(thm)], [c27,c262])). % 131.54/17.51 cnf(d126, plain, e3 = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | op(e0,e4) = e1 | e1 != e1 | ~'Ts9', inference(demodulation, [status(thm)], [d125,d4])). % 131.54/17.51 cnf(d127, plain, e3 = e1 | op(e0,e3) = e1 | op(e0,e2) = e1 | e1 != e1 | ~'Ts9', inference(resolution, [status(thm)], [d107,d126])). % 131.54/17.51 cnf(d128, plain, op(e0,e3) = e1 | op(e0,e2) = e1 | e3 = e1 | ~'Ts9', inference(equality_resolution, [status(thm)], [d127])). % 131.54/17.51 cnf(d129, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | e1 = e2 | op(e4,e1) = e2, inference(demodulation, [status(thm)], [c69,c211])). % 131.54/17.51 cnf(d130, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c204,d129])). % 131.54/17.51 cnf(d131, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | e0 = e2, inference(demodulation, [status(thm)], [d130,d0])). % 131.54/17.51 cnf(d132, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2, inference(resolution, [status(thm)], [c201,d131])). % 131.54/17.51 cnf(d133, plain, e2 != e2 | ~'Ts6' | op(e4,e0) = e2 | op(e4,e3) = e2, inference(superposition, [status(thm)], [d132,c248])). % 131.54/17.51 cnf(d134, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | ~'Ts6', inference(equality_resolution, [status(thm)], [d133])). % 131.54/17.51 cnf(d135, plain, e0 != e0 | ~'Ts7' | op(e0,e2) = e0 | e3 = e0, inference(superposition, [status(thm)], [d115,c251])). % 131.54/17.51 cnf(d136, plain, op(e0,e2) = e0 | e3 = e0 | ~'Ts7', inference(equality_resolution, [status(thm)], [d135])). % 131.54/17.51 cnf(d137, plain, e3 != e3 | ~'Ts8' | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [c62,c259])). % 131.54/17.51 cnf(d138, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != e3 | ~'Ts8', inference(demodulation, [status(thm)], [d137,d6])). % 131.54/17.51 cnf(d139, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != e3 | ~'Ts8', inference(resolution, [status(thm)], [c202,d138])). % 131.54/17.51 cnf(d140, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | ~'Ts8', inference(equality_resolution, [status(thm)], [d139])). % 131.54/17.51 cnf(d141, plain, op(e3,e1) = e3 | e2 = e1 | 'Ts9' | 'Ts6' | 'Ts7' | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(resolution, [status(thm)], [d74,d140])). % 131.54/17.51 cnf(d142, plain, op(e0,e3) = e3 | op(e3,e1) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e2 = e1 | 'Ts9' | 'Ts6' | op(e0,e2) = e0 | e3 = e0, inference(resolution, [status(thm)], [d141,d136])). % 131.54/17.51 cnf(d143, plain, op(e3,e1) = e3 | op(e0,e3) = e3 | op(e0,e2) = e0 | op(e3,e1) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e2 = e1 | 'Ts9' | 'Ts6', inference(resolution, [status(thm)], [d77,d142])). % 131.54/17.51 cnf(d144, plain, op(e0,e3) = e3 | op(e0,e2) = e0 | op(e3,e1) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e2 = e1 | 'Ts9' | op(e4,e0) = e2 | op(e4,e3) = e2, inference(resolution, [status(thm)], [d143,d134])). % 131.54/17.51 cnf(d145, plain, e2 != e1 | op(e4,e0) = e2 | op(e4,e3) = e2, inference(superposition, [status(thm)], [d132,d15])). % 131.54/17.51 cnf(d146, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e0,e3) = e3 | op(e0,e2) = e0 | op(e3,e1) = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | 'Ts9', inference(resolution, [status(thm)], [d145,d144])). % 131.54/17.51 cnf(d147, plain, op(e0,e3) = e3 | op(e0,e2) = e0 | op(e3,e1) = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e0,e3) = e1 | op(e0,e2) = e1 | e3 = e1, inference(resolution, [status(thm)], [d146,d128])). % 131.54/17.51 cnf(d148, plain, e3 != e3 | op(e3,e1) = e3 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d147,d124])). % 131.54/17.51 cnf(d149, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(equality_resolution, [status(thm)], [d148])). % 131.54/17.51 cnf(d150, plain, op(e1,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d149,d123])). % 131.54/17.51 cnf(d151, plain, e3 = e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e2,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d150,d119])). % 131.54/17.51 cnf(d152, plain, op(e3,op(e3,e1)) = e3 | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [c62,c91])). % 131.54/17.51 cnf(d153, plain, op(e0,e3) = e3 | op(e3,op(e3,e1)) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(demodulation, [status(thm)], [d152,d6])). % 131.54/17.51 cnf(d154, plain, op(e0,e3) = e3 | op(e3,op(e3,e1)) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(resolution, [status(thm)], [c202,d153])). % 131.54/17.51 cnf(d155, plain, op(e3,e3) = e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d149,d154])). % 131.54/17.51 cnf(d156, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | e0 = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(demodulation, [status(thm)], [d155,d6])). % 131.54/17.51 cnf(d157, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(resolution, [status(thm)], [c202,d156])). % 131.54/17.51 cnf(d158, plain, e3 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e0,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d157,d151])). % 131.54/17.51 cnf(d159, plain, op(e0,e1) = e0 | op(e0,e2) = e0 | e3 = e0 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d158,d116])). % 131.54/17.51 cnf(d160, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | e2 = e0 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1, inference(demodulation, [status(thm)], [d159,d9])). % 131.54/17.51 cnf(d161, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e0,e2) = e0 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1, inference(resolution, [status(thm)], [d54,d160])). % 131.54/17.51 cnf(d162, plain, e0 = e1 | e3 = e1 | op(e0,e3) = e1 | e2 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1, inference(superposition, [status(thm)], [d161,d110])). % 131.54/17.51 cnf(d163, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1 | e2 = e1, inference(resolution, [status(thm)], [c200,d162])). % 131.54/17.51 cnf(d164, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1, inference(resolution, [status(thm)], [d145,d163])). % 131.54/17.51 cnf(d165, plain, e1 != e1 | op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e4 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e0 | e3 = e1, inference(superposition, [status(thm)], [d164,d106])). % 131.54/17.51 cnf(d166, plain, e3 != op(e3,e3) | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [c62,c135])). % 131.54/17.51 cnf(d167, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != op(e3,e3), inference(demodulation, [status(thm)], [d166,d6])). % 131.54/17.51 cnf(d168, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != e0, inference(demodulation, [status(thm)], [d167,d6])). % 131.54/17.51 cnf(d169, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e3 != e0, inference(resolution, [status(thm)], [c202,d168])). % 131.54/17.51 cnf(d170, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e1 != e1, inference(resolution, [status(thm)], [d169,d165])). % 131.54/17.51 cnf(d171, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e2,e3) = e2 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(equality_resolution, [status(thm)], [d170])). % 131.54/17.51 cnf(d172, plain, e2 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d171,d104])). % 131.54/17.51 cnf(d173, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(resolution, [status(thm)], [d145,d172])). % 131.54/17.51 cnf(d174, plain, e3 != e0 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d173,d96])). % 131.54/17.51 cnf(d175, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(resolution, [status(thm)], [d164,d174])). % 131.54/17.51 cnf(d176, plain, e1 = e4 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d104,d175])). % 131.54/17.51 cnf(d177, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(resolution, [status(thm)], [c206,d176])). % 131.54/17.51 cnf(d178, plain, e3 = e4 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d177,d175])). % 131.54/17.51 cnf(d179, plain, op(e0,e3) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(resolution, [status(thm)], [c209,d178])). % 131.54/17.51 cnf(d180, plain, op(e1,op(e3,e0)) = e3 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d179,c90])). % 131.54/17.51 cnf(d181, plain, e3 != op(e3,e0), inference(demodulation, [status(thm)], [c102,d4])). % 131.54/17.51 cnf(d182, plain, op(op(e3,e0),e1) = e0 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d179,c78])). % 131.54/17.51 cnf(d183, plain, op(op(e0,e3),e1) = e3 | op(e3,e0) = e0 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4, inference(superposition, [status(thm)], [c15,c90])). % 131.54/17.51 cnf(d184, plain, op(op(e0,e3),e1) = e3 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4, inference(resolution, [status(thm)], [d58,d183])). % 131.54/17.51 cnf(d185, plain, op(e1,e1) = e3 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d179,d184])). % 131.54/17.51 cnf(d186, plain, op(e0,e3) = e3 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e4 = e3 | e3 = e1, inference(demodulation, [status(thm)], [d185,d27])). % 131.54/17.51 cnf(d187, plain, op(e0,e0) != e1 | op(e3,e0) = e0 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4, inference(superposition, [status(thm)], [c15,c102])). % 131.54/17.51 cnf(d188, plain, e3 != e1 | op(e3,e0) = e0 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4, inference(demodulation, [status(thm)], [d187,d4])). % 131.54/17.51 cnf(d189, plain, e3 != e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4, inference(resolution, [status(thm)], [d58,d188])). % 131.54/17.51 cnf(d190, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e0,e3) = e3 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e4 = e3, inference(resolution, [status(thm)], [d189,d186])). % 131.54/17.51 cnf(d191, plain, op(e2,e1) = e0 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e3,e0) = e3 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e4 = e3, inference(superposition, [status(thm)], [d190,d182])). % 131.54/17.51 cnf(d192, plain, op(e0,e3) = e3 | op(e3,e0) = e3 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e4 = e3, inference(resolution, [status(thm)], [d76,d191])). % 131.54/17.51 cnf(d193, plain, e3 != e3 | op(e0,e3) = e3 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e4 = e3, inference(superposition, [status(thm)], [d192,d181])). % 131.54/17.51 cnf(d194, plain, op(e0,e3) = e3 | op(e3,e0) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e4 = e3, inference(equality_resolution, [status(thm)], [d193])). % 131.54/17.51 cnf(d195, plain, op(e1,e4) = e3 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e4 = e3, inference(superposition, [status(thm)], [d194,d180])). % 131.54/17.51 cnf(d196, plain, e3 != e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1 | e4 = e3, inference(superposition, [status(thm)], [d195,d95])). % 131.54/17.51 cnf(d197, plain, e4 != e3 | op(e0,e3) = e3 | op(e3,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [c62,d88])). % 131.54/17.51 cnf(d198, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e4 != e3, inference(demodulation, [status(thm)], [d197,d6])). % 131.54/17.51 cnf(d199, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | e4 != e3, inference(resolution, [status(thm)], [c202,d198])). % 131.54/17.51 cnf(d200, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 != e3 | e3 = e1, inference(resolution, [status(thm)], [d199,d196])). % 131.54/17.51 cnf(d201, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(equality_resolution, [status(thm)], [d200])). % 131.54/17.51 cnf(d202, plain, e3 = e4 | op(e0,e3) = e4 | op(e4,e3) = e4 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d201,d92])). % 131.54/17.51 cnf(d203, plain, op(e0,e3) = e3 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c209,d202])). % 131.54/17.51 cnf(d204, plain, e3 != e3 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d203,d16])). % 131.54/17.51 cnf(d205, plain, op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d204])). % 131.54/17.51 cnf(d206, plain, e1 = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | e3 = e1, inference(superposition, [status(thm)], [d179,d205])). % 131.54/17.51 cnf(d207, plain, op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c206,d206])). % 131.54/17.51 cnf(d208, plain, e3 = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d207,d205])). % 131.54/17.51 cnf(d209, plain, op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c209,d208])). % 131.54/17.51 cnf(d210, plain, op(op(e3,e4),e2) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d209,c98])). % 131.54/17.51 cnf(d211, plain, e0 != op(e3,e4), inference(demodulation, [status(thm)], [c189,d6])). % 131.54/17.51 cnf(d212, plain, op(e2,op(e3,e4)) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d209,c94])). % 131.54/17.51 cnf(d213, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e4, inference(resolution, [status(thm)], [d34,c19])). % 131.54/17.51 cnf(d214, plain, op(e2,e2) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4, inference(superposition, [status(thm)], [d213,d210])). % 131.54/17.51 cnf(d215, plain, op(e2,e2) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4, inference(superposition, [status(thm)], [d213,d212])). % 131.54/17.51 cnf(d216, plain, e3 = e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d215,d214])). % 131.54/17.51 cnf(d217, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c209,d216])). % 131.54/17.51 cnf(d218, plain, op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d217,d212])). % 131.54/17.51 cnf(d219, plain, e3 != e3 | op(e3,e1) = e3 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d218,d124])). % 131.54/17.51 cnf(d220, plain, op(e3,e4) = e0 | op(e3,e4) = e4 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d219])). % 131.54/17.51 cnf(d221, plain, e3 != op(e3,e4) | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d220,c186])). % 131.54/17.51 cnf(d222, plain, e3 != e3 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d217,d221])). % 131.54/17.51 cnf(d223, plain, op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d222])). % 131.54/17.51 cnf(d224, plain, e0 != e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d223,d211])). % 131.54/17.51 cnf(d225, plain, op(e0,op(e1,e1)) = e1 | op(e0,e1) = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | op(e4,e1) = e0, inference(superposition, [status(thm)], [c36,c81])). % 131.54/17.51 cnf(d226, plain, op(e0,e4) = e1 | op(e0,e1) = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | op(e4,e1) = e0, inference(demodulation, [status(thm)], [d225,d27])). % 131.54/17.51 cnf(d227, plain, op(e0,e4) = e1 | e2 = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | op(e4,e1) = e0, inference(demodulation, [status(thm)], [d226,d9])). % 131.54/17.51 cnf(d228, plain, op(e0,e4) = e1 | e2 = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | e0 = e0, inference(demodulation, [status(thm)], [d227,d0])). % 131.54/17.51 cnf(d229, plain, e2 = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | e0 = e0, inference(resolution, [status(thm)], [d107,d228])). % 131.54/17.51 cnf(d230, plain, op(e3,e1) != e0, inference(demodulation, [status(thm)], [c119,d0])). % 131.54/17.51 cnf(d231, plain, e2 = e0 | op(e2,e1) = e0 | e0 = e0, inference(resolution, [status(thm)], [d230,d229])). % 131.54/17.51 cnf(d232, plain, op(e2,e1) = e0 | e0 = e0, inference(resolution, [status(thm)], [d54,d231])). % 131.54/17.51 cnf(d233, plain, e0 = e0, inference(resolution, [status(thm)], [d76,d232])). % 131.54/17.51 cnf(d234, plain, op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [d233,d224])). % 131.54/17.51 cnf(d235, plain, op(e4,e2) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d234,d210])). % 131.54/17.51 cnf(d236, plain, e4 != e4 | op(e0,e3) = e4 | op(e0,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d235,d87])). % 131.54/17.51 cnf(d237, plain, op(e0,e4) != e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d234,c142])). % 131.54/17.51 cnf(d238, plain, op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | e4 != e4, inference(resolution, [status(thm)], [d237,d236])). % 131.54/17.51 cnf(d239, plain, op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d238])). % 131.54/17.51 cnf(d240, plain, e3 != op(e2,e4) | op(e3,e1) = e3, inference(superposition, [status(thm)], [d35,c176])). % 131.54/17.51 cnf(d241, plain, op(e2,e4) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d234,d212])). % 131.54/17.51 cnf(d242, plain, e3 != e3 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d241,d240])). % 131.54/17.51 cnf(d243, plain, op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d242])). % 131.54/17.51 cnf(d244, plain, op(e3,e3) = e3 | op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d243,d154])). % 131.54/17.51 cnf(d245, plain, op(e0,e3) = e3 | e0 = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(demodulation, [status(thm)], [d244,d6])). % 131.54/17.51 cnf(d246, plain, op(e0,e3) = e3 | op(e2,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c202,d245])). % 131.54/17.51 cnf(d247, plain, e3 != op(e2,e4) | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d246,c179])). % 131.54/17.51 cnf(d248, plain, e3 != e3 | op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d241,d247])). % 131.54/17.51 cnf(d249, plain, op(e0,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d248])). % 131.54/17.51 cnf(d250, plain, e3 = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d249,d239])). % 131.54/17.51 cnf(d251, plain, op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c209,d250])). % 131.54/17.51 cnf(d252, plain, e3 != e3 | ~'Ts6' | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d251,c249])). % 131.54/17.51 cnf(d253, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | ~'Ts6', inference(equality_resolution, [status(thm)], [d252])). % 131.54/17.51 cnf(d254, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e2,e0) = e1 | e3 = e1 | 'Ts9', inference(resolution, [status(thm)], [d253,d82])). % 131.54/17.51 cnf(d255, plain, op(op(e3,e4),e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d251,c98])). % 131.54/17.51 cnf(d256, plain, op(e3,op(e3,e4)) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d251,c94])). % 131.54/17.51 cnf(d257, plain, op(e2,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4, inference(superposition, [status(thm)], [d213,d255])). % 131.54/17.51 cnf(d258, plain, e4 != op(e2,e4) | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d257,c179])). % 131.54/17.51 cnf(d259, plain, op(e0,e4) = e4 | op(e3,e4) = e4 | op(e2,e4) = e4 | e1 = e4 | op(e1,e4) = e4, inference(demodulation, [status(thm)], [c74,c211])). % 131.54/17.51 cnf(d260, plain, op(e0,e4) = e4 | op(e3,e4) = e4 | op(e2,e4) = e4 | op(e1,e4) = e4, inference(resolution, [status(thm)], [c206,d259])). % 131.54/17.51 cnf(d261, plain, op(op(e4,e1),e4) = e1 | op(e0,e4) = e4 | op(e3,e4) = e4 | op(e2,e4) = e4, inference(superposition, [status(thm)], [d260,c84])). % 131.54/17.51 cnf(d262, plain, op(e0,e4) = e1 | op(e0,e4) = e4 | op(e3,e4) = e4 | op(e2,e4) = e4, inference(demodulation, [status(thm)], [d261,d0])). % 131.54/17.51 cnf(d263, plain, op(e0,e4) = e4 | op(e3,e4) = e4 | op(e2,e4) = e4, inference(resolution, [status(thm)], [d107,d262])). % 131.54/17.51 cnf(d264, plain, e4 != e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e0,e4) = e4 | op(e3,e4) = e4, inference(superposition, [status(thm)], [d263,d258])). % 131.54/17.51 cnf(d265, plain, op(e0,e4) = e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d264])). % 131.54/17.51 cnf(d266, plain, op(e3,e3) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e0,e4) = e4 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d265,d256])). % 131.54/17.51 cnf(d267, plain, op(e0,e4) = e4 | e0 = e3 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(demodulation, [status(thm)], [d266,d6])). % 131.54/17.51 cnf(d268, plain, op(e0,e4) = e4 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c202,d267])). % 131.54/17.51 cnf(d269, plain, e0 != e0 | op(e0,e4) = e4 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d268,d211])). % 131.54/17.51 cnf(d270, plain, op(e0,e4) = e4 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [d233,d269])). % 131.54/17.51 cnf(d271, plain, op(e4,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e0,e4) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d270,d255])). % 131.54/17.51 cnf(d272, plain, e4 != e4 | ~'Ts9' | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d271,c265])). % 131.54/17.51 cnf(d273, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | ~'Ts9', inference(equality_resolution, [status(thm)], [d272])). % 131.54/17.51 cnf(d274, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e2,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [d273,d254])). % 131.54/17.51 cnf(d275, plain, e1 = e2 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e4,e0) = e2 | e3 = e0 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d274,d59])). % 131.54/17.51 cnf(d276, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0 | e3 = e1, inference(resolution, [status(thm)], [c204,d275])). % 131.54/17.51 cnf(d277, plain, op(e3,e1) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [d77,d276])). % 131.54/17.51 cnf(d278, plain, e1 = e2 | op(e0,e0) = e2 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e0,e0) = e1 | op(e3,e0) = e1 | op(e2,e0) = e1 | op(e4,e0) = e1, inference(superposition, [status(thm)], [c28,c30])). % 131.54/17.51 cnf(d279, plain, e3 = e2 | op(e0,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e1 | e1 = e2, inference(demodulation, [status(thm)], [d278,d4])). % 131.54/17.51 cnf(d280, plain, e3 = e2 | e3 = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e1 | e1 = e2, inference(demodulation, [status(thm)], [d279,d4])). % 131.54/17.51 cnf(d281, plain, e3 = e2 | e3 = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e1, inference(resolution, [status(thm)], [c204,d280])). % 131.54/17.51 cnf(d282, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e1 | e3 = e1, inference(resolution, [status(thm)], [d24,d281])). % 131.54/17.51 cnf(d283, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e1 | op(e4,e0) = e2 | e3 = e1, inference(resolution, [status(thm)], [d63,d282])). % 131.54/17.51 cnf(d284, plain, e0 = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e2,e0) = e2 | op(e4,e0) = e2 | e3 = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d277,d283])). % 131.54/17.51 cnf(d285, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c200,d284])). % 131.54/17.51 cnf(d286, plain, e2 = e0 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d285,d277])). % 131.54/17.51 cnf(d287, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [d54,d286])). % 131.54/17.51 cnf(d288, plain, e3 = e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d287,d48])). % 131.54/17.51 cnf(d289, plain, op(op(e2,e3),e1) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d288,c92])). % 131.54/17.51 cnf(d290, plain, op(e4,e1) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | op(e0,e3) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d92,d289])). % 131.54/17.51 cnf(d291, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e0 = e3 | e3 = e1, inference(demodulation, [status(thm)], [d290,d0])). % 131.54/17.51 cnf(d292, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c202,d291])). % 131.54/17.51 cnf(d293, plain, e1 != e1 | op(e3,e1) = e3 | e2 = e1 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d292,d45])). % 131.54/17.51 cnf(d294, plain, e3 != op(e3,e1) | op(e3,e1) = e3, inference(superposition, [status(thm)], [d35,c117])). % 131.54/17.51 cnf(d295, plain, e3 != e1 | op(e3,e1) = e3 | op(e3,e1) = e3 | e2 = e1, inference(superposition, [status(thm)], [d44,d294])). % 131.54/17.51 cnf(d296, plain, op(e3,e1) = e3 | e2 = e1 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | e1 != e1, inference(resolution, [status(thm)], [d295,d293])). % 131.54/17.51 cnf(d297, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(equality_resolution, [status(thm)], [d296])). % 131.54/17.51 cnf(d298, plain, e1 = e3 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | op(e3,e0) = e1 | op(e3,e2) = e1, inference(superposition, [status(thm)], [d48,d297])). % 131.54/17.51 cnf(d299, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(resolution, [status(thm)], [c205,d298])). % 131.54/17.51 cnf(d300, plain, op(e0,e1) != e1 | op(e3,e0) = e1 | op(e3,e3) = e1 | op(e3,e2) = e1 | op(e3,e4) = e1, inference(superposition, [status(thm)], [c57,c112])). % 131.54/17.51 cnf(d301, plain, e2 != e1 | op(e3,e0) = e1 | op(e3,e3) = e1 | op(e3,e2) = e1 | op(e3,e4) = e1, inference(demodulation, [status(thm)], [d300,d9])). % 131.54/17.51 cnf(d302, plain, e2 != e1 | op(e3,e0) = e1 | e0 = e1 | op(e3,e2) = e1 | op(e3,e4) = e1, inference(demodulation, [status(thm)], [d301,d6])). % 131.54/17.51 cnf(d303, plain, e2 != e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e4) = e1, inference(resolution, [status(thm)], [c200,d302])). % 131.54/17.51 cnf(d304, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | e2 != e1, inference(resolution, [status(thm)], [d34,d303])). % 131.54/17.51 cnf(d305, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d304,d299])). % 131.54/17.51 cnf(d306, plain, op(op(e2,e3),e1) = e3 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d305,c92])). % 131.54/17.51 cnf(d307, plain, op(e4,e1) = e3 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e0,e3) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d92,d306])). % 131.54/17.51 cnf(d308, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e0 = e3, inference(demodulation, [status(thm)], [d307,d0])). % 131.54/17.51 cnf(d309, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [c202,d308])). % 131.54/17.51 cnf(d310, plain, e2 != e1 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d309,d25])). % 131.54/17.51 cnf(d311, plain, e3 != e0 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(superposition, [status(thm)], [d297,d230])). % 131.54/17.51 cnf(d312, plain, op(op(e0,e1),e0) = e1 | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(superposition, [status(thm)], [c26,c80])). % 131.54/17.51 cnf(d313, plain, op(e2,e0) = e1 | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(demodulation, [status(thm)], [d312,d9])). % 131.54/17.51 cnf(d314, plain, op(e2,e0) = e1 | e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0 | op(e4,e0) = e0, inference(demodulation, [status(thm)], [d313,d4])). % 131.54/17.51 cnf(d315, plain, op(e2,e0) = e1 | e3 = e0 | op(e3,e0) = e0 | op(e2,e0) = e0, inference(resolution, [status(thm)], [d56,d314])). % 131.54/17.51 cnf(d316, plain, op(e2,e0) = e0 | op(e2,e0) = e1 | e3 = e0, inference(resolution, [status(thm)], [d58,d315])). % 131.54/17.51 cnf(d317, plain, e1 != op(e3,e0) | op(e2,e0) = e0 | e3 = e0, inference(superposition, [status(thm)], [d316,c107])). % 131.54/17.51 cnf(d318, plain, e1 != e1 | op(e2,e0) = e0 | e3 = e0 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d292,d317])). % 131.54/17.51 cnf(d319, plain, e3 != op(e2,e0), inference(demodulation, [status(thm)], [c101,d4])). % 131.54/17.51 cnf(d320, plain, e3 != e1 | op(e2,e0) = e0 | e3 = e0, inference(superposition, [status(thm)], [d316,d319])). % 131.54/17.51 cnf(d321, plain, op(e2,e0) = e0 | e3 = e0 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0 | e1 != e1, inference(resolution, [status(thm)], [d320,d318])). % 131.54/17.51 cnf(d322, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e2,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0, inference(equality_resolution, [status(thm)], [d321])). % 131.54/17.51 cnf(d323, plain, op(e2,op(e0,e1)) = e0 | op(e0,e0) = e2 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(superposition, [status(thm)], [c30,c76])). % 131.54/17.51 cnf(d324, plain, e3 = e2 | op(e3,e0) = e2 | op(e2,op(e0,e1)) = e0 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(demodulation, [status(thm)], [d323,d4])). % 131.54/17.51 cnf(d325, plain, e3 = e2 | op(e3,e0) = e2 | op(e2,e2) = e0 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(demodulation, [status(thm)], [d324,d9])). % 131.54/17.51 cnf(d326, plain, op(e3,e0) = e2 | op(e2,e2) = e0 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(resolution, [status(thm)], [d24,d325])). % 131.54/17.51 cnf(d327, plain, op(e2,e0) != e0 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d326,c171])). % 131.54/17.51 cnf(d328, plain, e0 != e0 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0, inference(superposition, [status(thm)], [d322,d327])). % 131.54/17.51 cnf(d329, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0, inference(resolution, [status(thm)], [d233,d328])). % 131.54/17.51 cnf(d330, plain, e2 = e0 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0, inference(superposition, [status(thm)], [d329,d322])). % 131.54/17.51 cnf(d331, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e0, inference(resolution, [status(thm)], [d54,d330])). % 131.54/17.51 cnf(d332, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(resolution, [status(thm)], [d331,d311])). % 131.54/17.51 cnf(d333, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e2,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d332,d310])). % 131.54/17.51 cnf(d334, plain, e2 != op(e3,e0) | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d333,c107])). % 131.54/17.51 cnf(d335, plain, e2 != e1 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d309,d334])). % 131.54/17.51 cnf(d336, plain, op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e0,e3) = e4 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d332,d335])). % 131.54/17.51 cnf(d337, plain, op(e2,e1) = e0 | op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d336,d20])). % 131.54/17.51 cnf(d338, plain, op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d76,d337])). % 131.54/17.51 cnf(d339, plain, e2 != e2 | op(e0,e3) = e3 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d338,d17])). % 131.54/17.51 cnf(d340, plain, op(e0,e3) = e3 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(equality_resolution, [status(thm)], [d339])). % 131.54/17.51 cnf(d341, plain, e3 != e3 | op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d340,d16])). % 131.54/17.51 cnf(d342, plain, op(e0,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(equality_resolution, [status(thm)], [d341])). % 131.54/17.51 cnf(d343, plain, op(e0,e2) != e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d288,c122])). % 131.54/17.51 cnf(d344, plain, e1 != e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | e3 = e1 | op(e0,e3) = e1 | e2 = e1, inference(superposition, [status(thm)], [d110,d343])). % 131.54/17.51 cnf(d345, plain, op(e0,e3) = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | e2 = e1, inference(equality_resolution, [status(thm)], [d344])). % 131.54/17.51 cnf(d346, plain, e1 != e1 | op(e3,e1) = e3 | e2 = e1 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1 | e2 = e1, inference(superposition, [status(thm)], [d345,d45])). % 131.54/17.51 cnf(d347, plain, op(e3,e1) = e3 | e2 = e1 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | e1 != e1, inference(resolution, [status(thm)], [d295,d346])). % 131.54/17.51 cnf(d348, plain, op(e0,e3) = e1 | op(e3,e0) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(equality_resolution, [status(thm)], [d347])). % 131.54/17.51 cnf(d349, plain, e1 != op(e2,e3) | op(e3,e1) = e1 | e2 = e1, inference(superposition, [status(thm)], [d42,c175])). % 131.54/17.51 cnf(d350, plain, op(e1,e3) = e3 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(superposition, [status(thm)], [d348,d123])). % 131.54/17.51 cnf(d351, plain, e1 = e3 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e2,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | op(e0,e3) = e1 | op(e2,e3) = e1, inference(superposition, [status(thm)], [d119,d350])). % 131.54/17.51 cnf(d352, plain, op(e0,e3) = e1 | op(e3,e0) = e2 | op(e2,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(resolution, [status(thm)], [c205,d351])). % 131.54/17.51 cnf(d353, plain, e1 != e1 | op(e3,e1) = e1 | e2 = e1 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(superposition, [status(thm)], [d352,d349])). % 131.54/17.51 cnf(d354, plain, op(e0,e3) = e1 | op(e3,e0) = e2 | op(e3,e1) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(equality_resolution, [status(thm)], [d353])). % 131.54/17.51 cnf(d355, plain, e1 = e3 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(superposition, [status(thm)], [d354,d348])). % 131.54/17.51 cnf(d356, plain, op(e0,e3) = e1 | op(e3,e0) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(resolution, [status(thm)], [c205,d355])). % 131.54/17.51 cnf(d357, plain, op(op(e0,e3),e2) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(superposition, [status(thm)], [d356,c90])). % 131.54/17.51 cnf(d358, plain, op(e4,e2) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d342,d357])). % 131.54/17.51 cnf(d359, plain, op(e4,op(e3,e0)) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d342,c90])). % 131.54/17.51 cnf(d360, plain, e1 = e2 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d288,d14])). % 131.54/17.51 cnf(d361, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c204,d360])). % 131.54/17.51 cnf(d362, plain, e1 != e1 | op(e3,e1) = e3 | e2 = e1 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d361,d45])). % 131.54/17.51 cnf(d363, plain, op(e3,e1) = e3 | e2 = e1 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | e1 != e1, inference(resolution, [status(thm)], [d295,d362])). % 131.54/17.51 cnf(d364, plain, op(e3,e0) = e2 | op(e3,e4) = e2 | op(e3,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(equality_resolution, [status(thm)], [d363])). % 131.54/17.51 cnf(d365, plain, e1 = e3 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1 | op(e3,e0) = e1 | op(e3,e2) = e1, inference(superposition, [status(thm)], [d48,d364])). % 131.54/17.51 cnf(d366, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4 | e2 = e1, inference(resolution, [status(thm)], [c205,d365])). % 131.54/17.51 cnf(d367, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d304,d366])). % 131.54/17.51 cnf(d368, plain, e1 = e2 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d367,d14])). % 131.54/17.51 cnf(d369, plain, op(e3,e0) = e2 | op(e3,e0) = e1 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [c204,d368])). % 131.54/17.51 cnf(d370, plain, e3 != e1 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d369,d181])). % 131.54/17.51 cnf(d371, plain, e4 != op(e0,e4) | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d342,c159])). % 131.54/17.51 cnf(d372, plain, e4 != e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(superposition, [status(thm)], [d271,d371])). % 131.54/17.51 cnf(d373, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | e3 = e1, inference(equality_resolution, [status(thm)], [d372])). % 131.54/17.51 cnf(d374, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | op(e3,e0) = e2 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d373,d370])). % 131.54/17.51 cnf(d375, plain, op(e4,e2) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e3,e4) = e2 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d374,d359])). % 131.54/17.51 cnf(d376, plain, e2 != e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e2) = e3, inference(superposition, [status(thm)], [d375,d34])). % 131.54/17.51 cnf(d377, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e2) = e3 | op(e0,e3) = e1 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e2) = e3, inference(resolution, [status(thm)], [d376,d358])). % 131.54/17.51 cnf(d378, plain, e1 = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e2) = e3, inference(superposition, [status(thm)], [d377,d342])). % 131.54/17.51 cnf(d379, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e2) = e3, inference(resolution, [status(thm)], [c206,d378])). % 131.54/17.51 cnf(d380, plain, e3 != e1 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d379,d15])). % 131.54/17.51 cnf(d381, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d373,d380])). % 131.54/17.51 cnf(d382, plain, op(op(e3,e4),e4) = e4 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d381,c98])). % 131.54/17.51 cnf(d383, plain, op(e4,op(e3,e4)) = e3 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d381,c94])). % 131.54/17.51 cnf(d384, plain, op(e4,e2) = e3 | op(e4,e0) = e2 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e4, inference(superposition, [status(thm)], [d213,d383])). % 131.54/17.51 cnf(d385, plain, op(e3,e4) = e4 | op(e4,e0) = e2 | op(e3,e4) = e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e2) = e3, inference(superposition, [status(thm)], [d384,d382])). % 131.54/17.51 cnf(d386, plain, e0 != e0 | op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e2) = e3, inference(superposition, [status(thm)], [d385,d211])). % 131.54/17.51 cnf(d387, plain, op(e3,e4) = e4 | op(e4,e0) = e2 | op(e4,e2) = e3, inference(resolution, [status(thm)], [d233,d386])). % 131.54/17.51 cnf(d388, plain, op(e4,e4) = e4 | op(e4,e0) = e2 | op(e4,e0) = e2 | op(e4,e2) = e3, inference(superposition, [status(thm)], [d387,d382])). % 131.54/17.51 cnf(d389, plain, op(e4,e0) = e2 | op(e4,e2) = e3 | e1 = e4, inference(demodulation, [status(thm)], [d388,c211])). % 131.54/17.51 cnf(d390, plain, op(e4,e0) = e2 | op(e4,e2) = e3, inference(resolution, [status(thm)], [c206,d389])). % 131.54/17.51 cnf(d391, plain, op(e4,e0) != e3 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d390,c191])). % 131.54/17.51 cnf(d392, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | e1 = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [c71,c211])). % 131.54/17.51 cnf(d393, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | op(e4,e1) = e3, inference(resolution, [status(thm)], [c205,d392])). % 131.54/17.51 cnf(d394, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | e0 = e3, inference(demodulation, [status(thm)], [d393,d0])). % 131.54/17.51 cnf(d395, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3, inference(resolution, [status(thm)], [c202,d394])). % 131.54/17.51 cnf(d396, plain, e3 = e4 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1 | op(e4,e0) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d395,d235])). % 131.54/17.51 cnf(d397, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | e3 = e1, inference(resolution, [status(thm)], [c209,d396])). % 131.54/17.51 cnf(d398, plain, e3 != e1 | op(e4,e0) = e3 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d395,d15])). % 131.54/17.51 cnf(d399, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d398,d397])). % 131.54/17.51 cnf(d400, plain, e3 != e1 | op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d399,d103])). % 131.54/17.51 cnf(d401, plain, op(e4,e0) = e2 | op(e4,e3) = e4 | op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d373,d400])). % 131.54/17.51 cnf(d402, plain, op(e4,e0) != e4 | op(e4,e0) = e3 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d401,c192])). % 131.54/17.51 cnf(d403, plain, op(e4,e0) = e0 | op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e0) = e4, inference(resolution, [status(thm)], [d63,c20])). % 131.54/17.51 cnf(d404, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e0) = e4, inference(resolution, [status(thm)], [d56,d403])). % 131.54/17.51 cnf(d405, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e0) = e3 | op(e4,e0) = e2, inference(resolution, [status(thm)], [d404,d402])). % 131.54/17.51 cnf(d406, plain, op(e4,e0) = e2 | op(e4,e0) = e2, inference(resolution, [status(thm)], [d405,d391])). % 131.54/17.51 cnf(d407, plain, op(e3,e0) != e2, inference(demodulation, [status(thm)], [c109,d406])). % 131.54/17.51 cnf(d408, plain, op(e3,e2) = e2 | op(e3,e4) = e2, inference(resolution, [status(thm)], [d407,d14])). % 131.54/17.51 cnf(d409, plain, op(op(e1,e0),e2) = e0, inference(demodulation, [status(thm)], [c76,d9])). % 131.54/17.51 cnf(d410, plain, e3 != op(e1,e0), inference(demodulation, [status(thm)], [c100,d4])). % 131.54/17.51 cnf(d411, plain, op(op(e0,e1),e1) = e1 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2 | op(e1,e0) = e4, inference(superposition, [status(thm)], [c5,c80])). % 131.54/17.51 cnf(d412, plain, op(e2,e1) = e1 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2 | op(e1,e0) = e4, inference(demodulation, [status(thm)], [d411,d9])). % 131.54/17.51 cnf(d413, plain, op(e1,e0) != e4, inference(demodulation, [status(thm)], [c160,d27])). % 131.54/17.51 cnf(d414, plain, op(e2,e1) = e1 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2, inference(resolution, [status(thm)], [d413,d412])). % 131.54/17.51 cnf(d415, plain, e2 != op(e4,e0) | op(e2,e1) = e1 | op(e1,e0) = e0 | op(e1,e0) = e3, inference(superposition, [status(thm)], [d414,c106])). % 131.54/17.51 cnf(d416, plain, e2 != e2 | op(e2,e1) = e1 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d405,d415])). % 131.54/17.51 cnf(d417, plain, op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e0 | op(e1,e0) = e3, inference(equality_resolution, [status(thm)], [d416])). % 131.54/17.51 cnf(d418, plain, e3 != e3 | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e0, inference(superposition, [status(thm)], [d417,d410])). % 131.54/17.51 cnf(d419, plain, op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e0, inference(equality_resolution, [status(thm)], [d418])). % 131.54/17.51 cnf(d420, plain, op(e2,e1) = e1 | e2 = e3 | op(e1,e0) = e0, inference(demodulation, [status(thm)], [d419,d406])). % 131.54/17.51 cnf(d421, plain, op(e2,e1) = e1 | op(e1,e0) = e0, inference(resolution, [status(thm)], [c207,d420])). % 131.54/17.51 cnf(d422, plain, op(e0,e2) = e0 | op(e2,e1) = e1, inference(superposition, [status(thm)], [d421,d409])). % 131.54/17.51 cnf(d423, plain, e1 != op(e3,e1) | op(e0,e2) = e0, inference(superposition, [status(thm)], [d422,c117])). % 131.54/17.51 cnf(d424, plain, e0 != op(e4,e1) | op(e0,e0) = e0 | op(e0,e3) = e0 | op(e0,e2) = e0 | op(e0,e4) = e0, inference(superposition, [status(thm)], [c25,c113])). % 131.54/17.51 cnf(d425, plain, e3 = e0 | op(e0,e3) = e0 | op(e0,e2) = e0 | op(e0,e4) = e0 | e0 != op(e4,e1), inference(demodulation, [status(thm)], [d424,d4])). % 131.54/17.51 cnf(d426, plain, e3 = e0 | op(e0,e3) = e0 | op(e0,e2) = e0 | op(e0,e4) = e0 | e0 != e0, inference(demodulation, [status(thm)], [d425,d0])). % 131.54/17.51 cnf(d427, plain, e3 = e0 | op(e0,e2) = e0 | op(e0,e4) = e0 | e0 != e0, inference(resolution, [status(thm)], [d19,d426])). % 131.54/17.51 cnf(d428, plain, op(e0,e2) = e0 | op(e0,e4) = e0 | e3 = e0, inference(resolution, [status(thm)], [d233,d427])). % 131.54/17.51 cnf(d429, plain, op(e0,e2) = e0 | op(e2,e1) = e1 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d419,d409])). % 131.54/17.51 cnf(d430, plain, e1 = e3 | op(e3,e1) = e3 | op(e0,e2) = e0 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d429,d35])). % 131.54/17.51 cnf(d431, plain, op(e0,e2) = e0 | op(e3,e1) = e3 | op(e4,e0) = e3, inference(resolution, [status(thm)], [c205,d430])). % 131.54/17.51 cnf(d432, plain, e3 != e0 | op(e0,e2) = e0 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d431,d230])). % 131.54/17.51 cnf(d433, plain, op(e0,e2) = e0 | e2 = e3 | e3 != e0, inference(demodulation, [status(thm)], [d432,d406])). % 131.54/17.51 cnf(d434, plain, op(e0,e2) = e0 | e3 != e0, inference(resolution, [status(thm)], [c207,d433])). % 131.54/17.51 cnf(d435, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | op(e0,e4) = e0, inference(resolution, [status(thm)], [d434,d428])). % 131.54/17.51 cnf(d436, plain, op(op(e2,e0),e0) = e0 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d435,c77])). % 131.54/17.51 cnf(d437, plain, op(op(e0,e1),e4) = e1 | op(e0,e0) = e4 | op(e3,e0) = e4 | op(e2,e0) = e4 | op(e4,e0) = e4, inference(superposition, [status(thm)], [c34,c80])). % 131.54/17.51 cnf(d438, plain, op(e2,e4) = e1 | op(e0,e0) = e4 | op(e3,e0) = e4 | op(e2,e0) = e4 | op(e4,e0) = e4, inference(demodulation, [status(thm)], [d437,d9])). % 131.54/17.51 cnf(d439, plain, op(e2,e4) = e1 | e3 = e4 | op(e3,e0) = e4 | op(e2,e0) = e4 | op(e4,e0) = e4, inference(demodulation, [status(thm)], [d438,d4])). % 131.54/17.51 cnf(d440, plain, op(e2,e4) = e1 | op(e3,e0) = e4 | op(e2,e0) = e4 | op(e4,e0) = e4, inference(resolution, [status(thm)], [c209,d439])). % 131.54/17.51 cnf(d441, plain, op(e2,e4) != e1, inference(demodulation, [status(thm)], [c148,c211])). % 131.54/17.51 cnf(d442, plain, op(e3,e0) = e4 | op(e2,e0) = e4 | op(e4,e0) = e4, inference(resolution, [status(thm)], [d441,d440])). % 131.54/17.51 cnf(d443, plain, op(e3,e0) = e4 | op(e2,e0) = e4 | e2 = e4, inference(demodulation, [status(thm)], [d442,d406])). % 131.54/17.51 cnf(d444, plain, op(e3,e0) = e4 | op(e2,e0) = e4, inference(resolution, [status(thm)], [c208,d443])). % 131.54/17.51 cnf(d445, plain, op(e4,e0) = e0 | op(e0,e4) = e0 | op(e3,e0) = e4, inference(superposition, [status(thm)], [d444,d436])). % 131.54/17.51 cnf(d446, plain, op(e0,e4) = e0 | op(e3,e0) = e4 | e2 = e0, inference(demodulation, [status(thm)], [d445,d406])). % 131.54/17.51 cnf(d447, plain, op(e0,e4) = e0 | op(e3,e0) = e4, inference(resolution, [status(thm)], [d54,d446])). % 131.54/17.51 cnf(d448, plain, e0 != op(e4,e1) | op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e2) = e0 | op(e2,e4) = e0, inference(superposition, [status(thm)], [c45,c118])). % 131.54/17.51 cnf(d449, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e2) = e0 | op(e2,e4) = e0 | e0 != e0, inference(demodulation, [status(thm)], [d448,d0])). % 131.54/17.51 cnf(d450, plain, op(e2,e0) = e0 | op(e2,e2) = e0 | op(e2,e4) = e0 | e0 != e0, inference(resolution, [status(thm)], [d96,d449])). % 131.54/17.51 cnf(d451, plain, op(e2,e0) = e0 | op(e2,e2) = e0 | op(e2,e4) = e0, inference(resolution, [status(thm)], [d233,d450])). % 131.54/17.51 cnf(d452, plain, op(e0,e2) != e0 | op(e2,e0) = e0 | op(e2,e4) = e0, inference(superposition, [status(thm)], [d451,c121])). % 131.54/17.51 cnf(d453, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | op(e2,e0) = e0, inference(resolution, [status(thm)], [d434,d115])). % 131.54/17.51 cnf(d454, plain, op(e2,e0) = e0 | op(e2,e0) = e0 | op(e2,e4) = e0, inference(resolution, [status(thm)], [d453,d452])). % 131.54/17.51 cnf(d455, plain, e4 = e0 | op(e2,e4) = e0 | op(e3,e0) = e4, inference(superposition, [status(thm)], [d444,d454])). % 131.54/17.51 cnf(d456, plain, e4 != op(e4,e1), inference(demodulation, [status(thm)], [c116,d27])). % 131.54/17.51 cnf(d457, plain, e4 != e0, inference(demodulation, [status(thm)], [d456,d0])). % 131.54/17.51 cnf(d458, plain, op(e3,e0) = e4 | op(e2,e4) = e0, inference(resolution, [status(thm)], [d457,d455])). % 131.54/17.51 cnf(d459, plain, op(e0,e4) != e0 | op(e3,e0) = e4, inference(superposition, [status(thm)], [d458,c141])). % 131.54/17.51 cnf(d460, plain, op(e3,e0) = e4 | op(e3,e0) = e4, inference(resolution, [status(thm)], [d459,d447])). % 131.54/17.51 cnf(d461, plain, e4 = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(demodulation, [status(thm)], [d48,d460])). % 131.54/17.51 cnf(d462, plain, e4 != op(e2,e1), inference(demodulation, [status(thm)], [c114,d27])). % 131.54/17.51 cnf(d463, plain, e4 != e1 | op(e3,e1) = e1 | e2 = e1, inference(superposition, [status(thm)], [d42,d462])). % 131.54/17.51 cnf(d464, plain, e2 != e1, inference(demodulation, [status(thm)], [d63,d406])). % 131.54/17.51 cnf(d465, plain, op(e3,e1) = e1 | e4 != e1, inference(resolution, [status(thm)], [d464,d463])). % 131.54/17.51 cnf(d466, plain, op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(resolution, [status(thm)], [d465,d461])). % 131.54/17.51 cnf(d467, plain, e1 != e1 | op(e0,e2) = e0 | op(e3,e2) = e1, inference(superposition, [status(thm)], [d466,d423])). % 131.54/17.51 cnf(d468, plain, op(e0,e2) = e0 | op(e3,e2) = e1, inference(equality_resolution, [status(thm)], [d467])). % 131.54/17.51 cnf(d469, plain, e1 = e2 | op(e3,e4) = e2 | op(e0,e2) = e0, inference(superposition, [status(thm)], [d468,d408])). % 131.54/17.51 cnf(d470, plain, op(e0,e2) = e0 | op(e3,e4) = e2, inference(resolution, [status(thm)], [c204,d469])). % 131.54/17.51 cnf(d471, plain, e3 = e1 | op(e0,e3) = e1 | op(e0,e2) = e1, inference(resolution, [status(thm)], [d464,d110])). % 131.54/17.51 cnf(d472, plain, op(e0,op(e1,e4)) = e1, inference(demodulation, [status(thm)], [c84,d0])). % 131.54/17.51 cnf(d473, plain, op(op(e1,e3),e1) = e3 | op(e3,e1) = e3 | e2 = e1, inference(superposition, [status(thm)], [d44,c91])). % 131.54/17.51 cnf(d474, plain, op(op(e1,e3),e1) = e3 | op(e3,e1) = e3, inference(resolution, [status(thm)], [d464,d473])). % 131.54/17.51 cnf(d475, plain, op(op(e1,e2),e3) = e2 | op(e3,e1) = e3, inference(superposition, [status(thm)], [d35,c86])). % 131.54/17.51 cnf(d476, plain, op(e3,op(e1,e1)) = e1 | op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [c41,c81])). % 131.54/17.51 cnf(d477, plain, op(e3,e4) = e1 | op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3, inference(demodulation, [status(thm)], [d476,d27])). % 131.54/17.51 cnf(d478, plain, op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3, inference(resolution, [status(thm)], [d34,d477])). % 131.54/17.51 cnf(d479, plain, op(e3,e3) = e2 | op(e3,e1) = e3 | op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [d478,d475])). % 131.54/17.51 cnf(d480, plain, e0 = e2 | op(e3,e1) = e3 | op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e4) = e3, inference(demodulation, [status(thm)], [d479,d6])). % 131.54/17.51 cnf(d481, plain, op(e3,e1) = e3 | op(e1,e0) = e3 | op(e1,e3) = e3 | op(e1,e4) = e3, inference(resolution, [status(thm)], [c201,d480])). % 131.54/17.51 cnf(d482, plain, op(e3,e1) = e3 | op(e3,e1) = e3 | op(e3,e1) = e3 | op(e1,e0) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [d481,d474])). % 131.54/17.51 cnf(d483, plain, e3 != e3 | op(e3,e1) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [d482,d410])). % 131.54/17.51 cnf(d484, plain, op(e3,e1) = e3 | op(e1,e4) = e3, inference(equality_resolution, [status(thm)], [d483])). % 131.54/17.51 cnf(d485, plain, op(e0,e3) = e1 | op(e3,e1) = e3, inference(superposition, [status(thm)], [d484,d472])). % 131.54/17.51 cnf(d486, plain, e3 != op(e3,e2) | op(e0,e3) = e1, inference(superposition, [status(thm)], [d485,c184])). % 131.54/17.51 cnf(d487, plain, e3 = e1 | op(e3,e2) = e1 | op(e0,e3) = e1, inference(superposition, [status(thm)], [d485,d466])). % 131.54/17.51 cnf(d488, plain, op(e2,op(e1,e0)) = e1, inference(demodulation, [status(thm)], [c80,d9])). % 131.54/17.51 cnf(d489, plain, op(e2,e0) = e1 | op(e2,e1) = e1, inference(superposition, [status(thm)], [d421,d488])). % 131.54/17.51 cnf(d490, plain, e1 != op(e3,e1) | op(e2,e0) = e1, inference(superposition, [status(thm)], [d489,c117])). % 131.54/17.51 cnf(d491, plain, e1 != e1 | op(e2,e0) = e1 | op(e3,e2) = e1, inference(superposition, [status(thm)], [d466,d490])). % 131.54/17.51 cnf(d492, plain, op(e3,e2) = e1 | op(e2,e0) = e1, inference(equality_resolution, [status(thm)], [d491])). % 131.54/17.51 cnf(d493, plain, e3 != e1 | op(e3,e2) = e1, inference(superposition, [status(thm)], [d492,d319])). % 131.54/17.51 cnf(d494, plain, op(e3,e2) = e1 | op(e0,e3) = e1 | op(e3,e2) = e1, inference(resolution, [status(thm)], [d493,d487])). % 131.54/17.51 cnf(d495, plain, e3 != e1 | op(e0,e3) = e1 | op(e0,e3) = e1, inference(superposition, [status(thm)], [d494,d486])). % 131.54/17.51 cnf(d496, plain, op(e0,e3) = e1 | op(e0,e3) = e1 | op(e0,e2) = e1, inference(resolution, [status(thm)], [d495,d471])). % 131.54/17.51 cnf(d497, plain, op(e0,e2) != e1 | op(e0,e3) = e1, inference(superposition, [status(thm)], [d494,c122])). % 131.54/17.51 cnf(d498, plain, op(e0,e3) = e1 | op(e0,e3) = e1, inference(resolution, [status(thm)], [d497,d496])). % 131.54/17.51 cnf(d499, plain, e1 != op(e1,e3), inference(demodulation, [status(thm)], [c130,d498])). % 131.54/17.51 cnf(d500, plain, op(op(e0,e3),e4) = e3, inference(demodulation, [status(thm)], [c90,d460])). % 131.54/17.51 cnf(d501, plain, op(e1,e4) = e3, inference(demodulation, [status(thm)], [d500,d498])). % 131.54/17.51 cnf(d502, plain, op(op(e1,e2),e1) = e2 | op(e3,e1) = e1 | e2 = e1, inference(superposition, [status(thm)], [d42,c86])). % 131.54/17.51 cnf(d503, plain, op(e1,op(e1,e1)) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | op(e1,e2) = e1 | op(e1,e4) = e1, inference(superposition, [status(thm)], [c37,c81])). % 131.54/17.51 cnf(d504, plain, op(e1,e4) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | op(e1,e2) = e1 | op(e1,e4) = e1, inference(demodulation, [status(thm)], [d503,d27])). % 131.54/17.51 cnf(d505, plain, op(e1,e0) = e1 | op(e1,e3) = e1 | op(e1,e2) = e1 | op(e1,e4) = e1, inference(resolution, [status(thm)], [d41,d504])). % 131.54/17.51 cnf(d506, plain, op(e1,e1) = e2 | op(e3,e1) = e1 | e2 = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | op(e1,e4) = e1, inference(superposition, [status(thm)], [d505,d502])). % 131.54/17.51 cnf(d507, plain, op(e3,e1) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | e3 = e1 | op(e1,e1) = e2 | e2 = e1, inference(demodulation, [status(thm)], [d506,d501])). % 131.54/17.51 cnf(d508, plain, op(e3,e1) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | e3 = e1 | e4 = e2 | e2 = e1, inference(demodulation, [status(thm)], [d507,d27])). % 131.54/17.51 cnf(d509, plain, op(e3,e1) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | e3 = e1 | e4 = e2, inference(resolution, [status(thm)], [d464,d508])). % 131.54/17.51 cnf(d510, plain, e4 != e2, inference(demodulation, [status(thm)], [d407,d460])). % 131.54/17.51 cnf(d511, plain, op(e3,e1) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1 | e3 = e1, inference(resolution, [status(thm)], [d510,d509])). % 131.54/17.51 cnf(d512, plain, e3 != e1, inference(demodulation, [status(thm)], [d16,d498])). % 131.54/17.51 cnf(d513, plain, op(e3,e1) = e1 | op(e1,e0) = e1 | op(e1,e3) = e1, inference(resolution, [status(thm)], [d512,d511])). % 131.54/17.51 cnf(d514, plain, e1 != e1 | op(e3,e1) = e1 | op(e1,e0) = e1, inference(superposition, [status(thm)], [d513,d499])). % 131.54/17.51 cnf(d515, plain, op(e3,e1) = e1 | op(e1,e0) = e1, inference(equality_resolution, [status(thm)], [d514])). % 131.54/17.51 cnf(d516, plain, op(e1,e2) = e0 | op(e3,e1) = e1, inference(superposition, [status(thm)], [d515,d409])). % 131.54/17.51 cnf(d517, plain, op(e0,e2) != e0 | op(e3,e1) = e1, inference(superposition, [status(thm)], [d516,c120])). % 131.54/17.51 cnf(d518, plain, op(e2,op(e0,e4)) = e0, inference(demodulation, [status(thm)], [c79,d406])). % 131.54/17.51 cnf(d519, plain, op(op(e0,e4),e2) = e4 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d405,c95])). % 131.54/17.51 cnf(d520, plain, e3 != op(e0,e4), inference(demodulation, [status(thm)], [c153,d4])). % 131.54/17.51 cnf(d521, plain, op(e2,op(e0,e4)) = e0 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d405,c79])). % 131.54/17.51 cnf(d522, plain, op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e2 | op(e0,e4) = e4, inference(resolution, [status(thm)], [d107,c4])). % 131.54/17.51 cnf(d523, plain, op(e2,e2) = e0 | op(e4,e0) = e3 | op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e4, inference(superposition, [status(thm)], [d522,d521])). % 131.54/17.51 cnf(d524, plain, op(e2,e2) = e4 | op(e4,e0) = e3 | op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e4, inference(superposition, [status(thm)], [d522,d519])). % 131.54/17.51 cnf(d525, plain, e4 = e0 | op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e4 | op(e4,e0) = e3 | op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e4 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d524,d523])). % 131.54/17.51 cnf(d526, plain, op(e0,e4) = e0 | op(e0,e4) = e3 | op(e0,e4) = e4 | op(e4,e0) = e3, inference(resolution, [status(thm)], [d457,d525])). % 131.54/17.51 cnf(d527, plain, e3 != e3 | op(e0,e4) = e0 | op(e0,e4) = e4 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d526,d520])). % 131.54/17.51 cnf(d528, plain, op(e0,e4) = e0 | op(e0,e4) = e4 | op(e4,e0) = e3, inference(equality_resolution, [status(thm)], [d527])). % 131.54/17.51 cnf(d529, plain, op(e0,e2) = e4 | op(e4,e0) = e3 | op(e0,e4) = e4 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d528,d519])). % 131.54/17.51 cnf(d530, plain, e4 != op(e4,e2) | op(e0,e4) = e4 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d529,c123])). % 131.54/17.51 cnf(d531, plain, op(e0,e4) = e4 | e2 = e3 | e4 != op(e4,e2), inference(demodulation, [status(thm)], [d530,d406])). % 131.54/17.51 cnf(d532, plain, op(e0,e4) = e4 | e4 != op(e4,e2), inference(resolution, [status(thm)], [c207,d531])). % 131.54/17.51 cnf(d533, plain, op(e4,e0) = e4 | op(e4,e3) = e4 | op(e4,e2) = e4 | e1 = e4 | op(e4,e1) = e4, inference(demodulation, [status(thm)], [c73,c211])). % 131.54/17.51 cnf(d534, plain, op(e4,e0) = e4 | op(e4,e3) = e4 | op(e4,e2) = e4 | op(e4,e1) = e4, inference(resolution, [status(thm)], [c206,d533])). % 131.54/17.51 cnf(d535, plain, op(e4,e0) = e4 | op(e4,e3) = e4 | op(e4,e2) = e4 | e0 = e4, inference(demodulation, [status(thm)], [d534,d0])). % 131.54/17.51 cnf(d536, plain, op(e4,e0) = e4 | op(e4,e3) = e4 | op(e4,e2) = e4, inference(resolution, [status(thm)], [c203,d535])). % 131.54/17.51 cnf(d537, plain, e2 = e4 | op(e4,e3) = e4 | op(e4,e2) = e4, inference(demodulation, [status(thm)], [d536,d406])). % 131.54/17.51 cnf(d538, plain, op(e4,e3) = e4 | op(e4,e2) = e4, inference(resolution, [status(thm)], [c208,d537])). % 131.54/17.51 cnf(d539, plain, e4 != e4 | op(e0,e4) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d538,d532])). % 131.54/17.51 cnf(d540, plain, op(op(e0,e4),e2) = e4, inference(demodulation, [status(thm)], [c95,d406])). % 131.54/17.51 cnf(d541, plain, op(op(e0,e4),e2) = e4 | e2 = e3, inference(demodulation, [status(thm)], [d519,d406])). % 131.54/17.51 cnf(d542, plain, e4 = e4 | e2 = e3, inference(demodulation, [status(thm)], [d541,d540])). % 131.54/17.51 cnf(d543, plain, e4 = e4, inference(resolution, [status(thm)], [c207,d542])). % 131.54/17.51 cnf(d544, plain, op(e0,e4) = e4 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d543,d539])). % 131.54/17.51 cnf(d545, plain, op(e2,e4) = e0 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d544,d518])). % 131.54/17.51 cnf(d546, plain, e1 = e4 | op(e2,e3) = e4 | op(e4,e3) = e4, inference(demodulation, [status(thm)], [d92,d498])). % 131.54/17.51 cnf(d547, plain, op(e2,e3) = e4 | op(e4,e3) = e4, inference(resolution, [status(thm)], [c206,d546])). % 131.54/17.51 cnf(d548, plain, op(e0,e1) != e2 | op(e2,e0) = e2 | op(e2,e3) = e2 | op(e2,e2) = e2 | op(e2,e4) = e2, inference(superposition, [status(thm)], [c49,c111])). % 131.54/17.51 cnf(d549, plain, e2 != e2 | op(e2,e0) = e2 | op(e2,e3) = e2 | op(e2,e2) = e2 | op(e2,e4) = e2, inference(demodulation, [status(thm)], [d548,d9])). % 131.54/17.51 cnf(d550, plain, op(e2,e0) = e2 | op(e2,e3) = e2 | op(e2,e2) = e2 | op(e2,e4) = e2, inference(equality_resolution, [status(thm)], [d549])). % 131.54/17.51 cnf(d551, plain, op(e2,e0) != e2, inference(demodulation, [status(thm)], [c108,d406])). % 131.54/17.51 cnf(d552, plain, op(e2,e3) = e2 | op(e2,e2) = e2 | op(e2,e4) = e2, inference(resolution, [status(thm)], [d551,d550])). % 131.54/17.51 cnf(d553, plain, e2 != e2 | ~'Ts7' | op(e2,e3) = e2 | op(e2,e4) = e2, inference(superposition, [status(thm)], [d552,c253])). % 131.54/17.51 cnf(d554, plain, op(e2,e3) = e2 | op(e2,e4) = e2 | ~'Ts7', inference(equality_resolution, [status(thm)], [d553])). % 131.54/17.51 cnf(d555, plain, op(e2,e0) != e1 | op(e3,e1) = e1 | e2 = e1, inference(superposition, [status(thm)], [d42,c170])). % 131.54/17.51 cnf(d556, plain, op(e3,e1) = e1 | op(e2,e0) != e1, inference(resolution, [status(thm)], [d464,d555])). % 131.54/17.51 cnf(d557, plain, op(e1,op(e0,e1)) = e0 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2 | op(e1,e0) = e4, inference(superposition, [status(thm)], [c5,c76])). % 131.54/17.51 cnf(d558, plain, op(e1,e2) = e0 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2 | op(e1,e0) = e4, inference(demodulation, [status(thm)], [d557,d9])). % 131.54/17.51 cnf(d559, plain, op(e1,e2) = e0 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2, inference(resolution, [status(thm)], [d413,d558])). % 131.54/17.51 cnf(d560, plain, op(e0,e2) != e0 | op(e1,e0) = e0 | op(e1,e0) = e3 | op(e1,e0) = e2, inference(superposition, [status(thm)], [d559,c120])). % 131.54/17.51 cnf(d561, plain, op(e1,e0) != e2, inference(demodulation, [status(thm)], [c106,d406])). % 131.54/17.51 cnf(d562, plain, op(e0,e2) != e0 | op(e1,e0) = e0 | op(e1,e0) = e3, inference(resolution, [status(thm)], [d561,d560])). % 131.54/17.51 cnf(d563, plain, op(e1,e0) != e3, inference(demodulation, [status(thm)], [c163,d501])). % 131.54/17.51 cnf(d564, plain, op(e0,e2) != e0 | op(e1,e0) = e0, inference(resolution, [status(thm)], [d563,d562])). % 131.54/17.51 cnf(d565, plain, e0 != op(e2,e4) | op(e0,e2) = e0 | e3 = e0, inference(superposition, [status(thm)], [d115,c173])). % 131.54/17.51 cnf(d566, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | e0 != op(e2,e4), inference(resolution, [status(thm)], [d434,d565])). % 131.54/17.51 cnf(d567, plain, e0 != e0 | op(e0,e2) = e0 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d545,d566])). % 131.54/17.51 cnf(d568, plain, op(e0,e2) = e0 | op(e4,e3) = e4, inference(resolution, [status(thm)], [d233,d567])). % 131.54/17.51 cnf(d569, plain, e0 != e0 | op(e1,e0) = e0 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d568,d564])). % 131.54/17.51 cnf(d570, plain, op(e4,e3) = e4 | op(e1,e0) = e0, inference(resolution, [status(thm)], [d233,d569])). % 131.54/17.51 cnf(d571, plain, op(e2,e0) = e1 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d570,d488])). % 131.54/17.51 cnf(d572, plain, e1 != e1 | op(e3,e1) = e1 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d571,d556])). % 131.54/17.51 cnf(d573, plain, op(e3,e1) = e1 | op(e4,e3) = e4, inference(equality_resolution, [status(thm)], [d572])). % 131.54/17.51 cnf(d574, plain, e1 != e1 | ~'Ts5' | op(e4,e3) = e4, inference(superposition, [status(thm)], [d573,c242])). % 131.54/17.51 cnf(d575, plain, op(e4,e3) = e4 | ~'Ts5', inference(equality_resolution, [status(thm)], [d574])). % 131.54/17.51 cnf(d576, plain, op(e4,e3) = e4 | 'Ts9' | 'Ts6' | 'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d575,c215])). % 131.54/17.51 cnf(d577, plain, e4 != e4 | op(e0,e4) = e4 | op(e4,e0) = e3 | op(e4,e0) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d536,d530])). % 131.54/17.51 cnf(d578, plain, op(e0,e4) = e4 | op(e4,e0) = e3 | op(e4,e0) = e4 | op(e4,e3) = e4, inference(equality_resolution, [status(thm)], [d577])). % 131.54/17.51 cnf(d579, plain, e4 != e4 | ~'Ts9' | op(e4,e0) = e3 | op(e4,e0) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d578,c265])). % 131.54/17.51 cnf(d580, plain, op(e4,e0) = e3 | op(e4,e0) = e4 | op(e4,e3) = e4 | ~'Ts9', inference(equality_resolution, [status(thm)], [d579])). % 131.54/17.51 cnf(d581, plain, e2 = e3 | op(e4,e0) = e4 | op(e4,e3) = e4 | ~'Ts9', inference(demodulation, [status(thm)], [d580,d406])). % 131.54/17.51 cnf(d582, plain, e2 = e3 | e2 = e4 | op(e4,e3) = e4 | ~'Ts9', inference(demodulation, [status(thm)], [d581,d406])). % 131.54/17.51 cnf(d583, plain, op(e4,e3) = e4 | e2 = e4 | ~'Ts9', inference(resolution, [status(thm)], [c207,d582])). % 131.54/17.51 cnf(d584, plain, op(e4,e3) = e4 | ~'Ts9', inference(resolution, [status(thm)], [c208,d583])). % 131.54/17.51 cnf(d585, plain, op(e4,e3) = e4 | op(e4,e3) = e4 | 'Ts6' | 'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d584,d576])). % 131.54/17.51 cnf(d586, plain, e0 != e0 | ~'Ts8' | op(e4,e3) = e4, inference(superposition, [status(thm)], [d570,c256])). % 131.54/17.51 cnf(d587, plain, op(e4,e3) = e4 | ~'Ts8', inference(resolution, [status(thm)], [d233,d586])). % 131.54/17.51 cnf(d588, plain, op(e4,e3) = e4 | op(e4,e3) = e4 | 'Ts6' | 'Ts7', inference(resolution, [status(thm)], [d587,d585])). % 131.54/17.51 cnf(d589, plain, e2 = e3 | op(e4,e3) = e3 | op(e4,e2) = e3, inference(demodulation, [status(thm)], [d395,d406])). % 131.54/17.51 cnf(d590, plain, op(e4,e3) = e3 | op(e4,e2) = e3, inference(resolution, [status(thm)], [c207,d589])). % 131.54/17.51 cnf(d591, plain, e3 = e4 | op(e4,e3) = e4 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d590,d538])). % 131.54/17.51 cnf(d592, plain, op(e4,e3) = e3 | op(e4,e3) = e4, inference(resolution, [status(thm)], [c209,d591])). % 131.54/17.51 cnf(d593, plain, e3 != e3 | ~'Ts6' | op(e4,e3) = e4, inference(superposition, [status(thm)], [d592,c249])). % 131.54/17.51 cnf(d594, plain, op(e4,e3) = e4 | ~'Ts6', inference(equality_resolution, [status(thm)], [d593])). % 131.54/17.51 cnf(d595, plain, op(e4,e3) = e4 | op(e4,e3) = e4 | 'Ts7', inference(resolution, [status(thm)], [d594,d588])). % 131.54/17.51 cnf(d596, plain, op(e4,e3) = e4 | op(e2,e3) = e2 | op(e2,e4) = e2, inference(resolution, [status(thm)], [d595,d554])). % 131.54/17.51 cnf(d597, plain, e2 = e4 | op(e4,e3) = e4 | op(e2,e4) = e2 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d596,d547])). % 131.54/17.51 cnf(d598, plain, op(e2,e4) = e2 | op(e4,e3) = e4, inference(resolution, [status(thm)], [c208,d597])). % 131.54/17.51 cnf(d599, plain, e2 = e0 | op(e4,e3) = e4 | op(e4,e3) = e4, inference(superposition, [status(thm)], [d598,d545])). % 131.54/17.51 cnf(d600, plain, op(e4,e3) = e4, inference(resolution, [status(thm)], [d54,d599])). % 131.54/17.51 cnf(d601, plain, op(e3,op(e2,e4)) = e2 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d590,c89])). % 131.54/17.51 cnf(d602, plain, op(e2,e0) = e1 | op(e2,e1) = e1 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d419,d488])). % 131.54/17.51 cnf(d603, plain, e1 = e3 | op(e3,e1) = e3 | op(e2,e0) = e1 | op(e4,e0) = e3, inference(superposition, [status(thm)], [d602,d35])). % 131.54/17.51 cnf(d604, plain, op(e3,e1) = e3 | op(e2,e0) = e1 | op(e4,e0) = e3, inference(resolution, [status(thm)], [c205,d603])). % 131.54/17.51 cnf(d605, plain, op(e3,e1) = e3 | op(e2,e0) = e1 | e2 = e3, inference(demodulation, [status(thm)], [d604,d406])). % 131.54/17.51 cnf(d606, plain, op(e3,e1) = e3 | op(e2,e0) = e1, inference(resolution, [status(thm)], [c207,d605])). % 131.54/17.51 cnf(d607, plain, e1 = e0 | op(e2,e4) = e0 | op(e3,e1) = e3, inference(superposition, [status(thm)], [d606,d454])). % 131.54/17.51 cnf(d608, plain, e1 != e0 | op(e3,e1) = e3 | e2 = e1, inference(superposition, [status(thm)], [d44,d230])). % 131.54/17.51 cnf(d609, plain, op(e3,e1) = e3 | e1 != e0, inference(resolution, [status(thm)], [d464,d608])). % 131.54/17.51 cnf(d610, plain, op(e3,e1) = e3 | op(e3,e1) = e3 | op(e2,e4) = e0, inference(resolution, [status(thm)], [d609,d607])). % 131.54/17.51 cnf(d611, plain, op(e3,e0) = e2 | op(e4,e3) = e3 | op(e3,e1) = e3, inference(superposition, [status(thm)], [d610,d601])). % 131.54/17.51 cnf(d612, plain, e4 = e2 | op(e3,e1) = e3 | op(e4,e3) = e3, inference(demodulation, [status(thm)], [d611,d460])). % 131.54/17.51 cnf(d613, plain, op(e3,e1) = e3 | op(e4,e3) = e3, inference(resolution, [status(thm)], [d510,d612])). % 131.54/17.51 cnf(d614, plain, e3 = e1 | op(e3,e2) = e1 | op(e4,e3) = e3, inference(superposition, [status(thm)], [d613,d466])). % 131.54/17.51 cnf(d615, plain, e2 = e3 | op(e4,e3) = e3 | e3 != e1, inference(demodulation, [status(thm)], [d398,d406])). % 131.54/17.51 cnf(d616, plain, op(e4,e3) = e3 | e3 != e1, inference(resolution, [status(thm)], [c207,d615])). % 131.54/17.51 cnf(d617, plain, op(e4,e3) = e3 | op(e3,e2) = e1 | op(e4,e3) = e3, inference(resolution, [status(thm)], [d616,d614])). % 131.54/17.51 cnf(d618, plain, op(e3,e2) = e1 | e4 = e3, inference(demodulation, [status(thm)], [d617,d600])). % 131.54/17.51 cnf(d619, plain, e4 != op(e1,e4), inference(demodulation, [status(thm)], [c166,d27])). % 131.54/17.51 cnf(d620, plain, e4 != e3, inference(demodulation, [status(thm)], [d619,d501])). % 131.54/17.51 cnf(d621, plain, op(e3,e2) = e1, inference(resolution, [status(thm)], [d620,d618])). % 131.54/17.51 cnf(d622, plain, op(e3,e1) != e1, inference(demodulation, [status(thm)], [c184,d621])). % 131.54/17.51 cnf(d623, plain, op(e0,e2) != e0, inference(resolution, [status(thm)], [d622,d517])). % 131.54/17.51 cnf(d624, plain, op(e3,e4) = e2, inference(resolution, [status(thm)], [d623,d470])). % 131.54/17.51 cnf(d625, plain, op(op(e3,e4),e4) = e4, inference(demodulation, [status(thm)], [c98,d600])). % 131.54/17.51 cnf(d626, plain, op(e2,e4) = e4, inference(demodulation, [status(thm)], [d625,d624])). % 131.54/17.51 cnf(d627, plain, op(e0,e2) = e0 | op(e3,e1) = e3 | e2 = e3, inference(demodulation, [status(thm)], [d431,d406])). % 131.54/17.51 cnf(d628, plain, op(e0,e2) = e0 | op(e3,e1) = e3, inference(resolution, [status(thm)], [c207,d627])). % 131.54/17.51 cnf(d629, plain, op(op(e1,e3),e3) = e3 | op(e0,e2) = e0, inference(superposition, [status(thm)], [d628,c91])). % 131.54/17.51 cnf(d630, plain, op(e2,op(e1,e1)) = e1 | op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(superposition, [status(thm)], [c39,c81])). % 131.54/17.51 cnf(d631, plain, op(e2,e4) = e1 | op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(demodulation, [status(thm)], [d630,d27])). % 131.54/17.51 cnf(d632, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(resolution, [status(thm)], [d441,d631])). % 131.54/17.51 cnf(d633, plain, op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(resolution, [status(thm)], [d561,d632])). % 131.54/17.51 cnf(d634, plain, op(e1,e3) = e2 | op(e1,e2) = e2 | e3 = e2, inference(demodulation, [status(thm)], [d633,d501])). % 131.54/17.51 cnf(d635, plain, op(e1,e3) = e2 | op(e1,e2) = e2, inference(resolution, [status(thm)], [d24,d634])). % 131.54/17.51 cnf(d636, plain, op(e1,op(e1,e2)) = e1 | op(e0,e2) = e0, inference(superposition, [status(thm)], [d422,c82])). % 131.54/17.51 cnf(d637, plain, op(e1,e2) = e1 | op(e0,e2) = e0 | op(e1,e3) = e2, inference(superposition, [status(thm)], [d635,d636])). % 131.54/17.51 cnf(d638, plain, e1 = e2 | op(e1,e3) = e2 | op(e0,e2) = e0 | op(e1,e3) = e2, inference(superposition, [status(thm)], [d637,d635])). % 131.54/17.51 cnf(d639, plain, op(e0,e2) = e0 | op(e1,e3) = e2, inference(resolution, [status(thm)], [c204,d638])). % 131.54/17.51 cnf(d640, plain, op(e2,e3) = e3 | op(e0,e2) = e0 | op(e0,e2) = e0, inference(superposition, [status(thm)], [d639,d629])). % 131.54/17.51 cnf(d641, plain, op(e2,e3) = e3, inference(resolution, [status(thm)], [d623,d640])). % 131.54/17.51 cnf(d642, plain, e2 != e2 | ~'Ts2' | op(e2,e3) = e2 | op(e2,e4) = e2, inference(superposition, [status(thm)], [d552,c228])). % 131.54/17.51 cnf(d643, plain, op(e2,e3) = e2 | op(e2,e4) = e2 | ~'Ts2', inference(equality_resolution, [status(thm)], [d642])). % 131.54/17.51 cnf(d644, plain, ~'Ts0', inference(resolution, [status(thm)], [d600,c220])). % 131.54/17.51 cnf(d645, plain, 'Ts4' | 'Ts3' | 'Ts1' | 'Ts2', inference(resolution, [status(thm)], [d644,c214])). % 131.54/17.51 cnf(d646, plain, e0 != e0 | op(e1,e0) = e0 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d435,d564])). % 131.54/17.51 cnf(d647, plain, op(e0,e4) = e0 | op(e1,e0) = e0, inference(resolution, [status(thm)], [d233,d646])). % 131.54/17.51 cnf(d648, plain, op(e2,e0) = e1 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d647,d488])). % 131.54/17.51 cnf(d649, plain, e1 != e1 | op(e3,e1) = e1 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d648,d556])). % 131.54/17.51 cnf(d650, plain, e1 != op(e0,e3) | e3 = e1 | op(e0,e3) = e1 | e2 = e1, inference(superposition, [status(thm)], [d110,c157])). % 131.54/17.51 cnf(d651, plain, op(e0,e3) = e1 | e3 = e1 | e1 != op(e0,e3), inference(resolution, [status(thm)], [d464,d650])). % 131.54/17.51 cnf(d652, plain, op(e0,e3) = e1 | op(e0,e3) = e1 | e1 != op(e0,e3), inference(resolution, [status(thm)], [d495,d651])). % 131.54/17.51 cnf(d653, plain, e0 = e1 | e3 = e1 | op(e0,e3) = e1 | e2 = e1 | op(e0,e4) = e0 | e3 = e0, inference(superposition, [status(thm)], [d428,d110])). % 131.54/17.51 cnf(d654, plain, op(e0,e3) = e1 | op(e0,e4) = e0 | e3 = e0 | e3 = e1 | e2 = e1, inference(resolution, [status(thm)], [c200,d653])). % 131.54/17.52 cnf(d655, plain, op(e0,e3) = e1 | op(e0,e4) = e0 | e3 = e0 | e3 = e1, inference(resolution, [status(thm)], [d464,d654])). % 131.54/17.52 cnf(d656, plain, e3 != op(e0,e2), inference(demodulation, [status(thm)], [c151,d4])). % 131.54/17.52 cnf(d657, plain, e3 != e0 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d435,d656])). % 131.54/17.52 cnf(d658, plain, op(e0,e4) = e0 | op(e0,e3) = e1 | op(e0,e4) = e0 | e3 = e1, inference(resolution, [status(thm)], [d657,d655])). % 131.54/17.52 cnf(d659, plain, op(e0,e3) = e1 | op(e0,e3) = e1 | op(e0,e4) = e0, inference(resolution, [status(thm)], [d495,d658])). % 131.54/17.52 cnf(d660, plain, e1 != e1 | op(e0,e3) = e1 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d659,d652])). % 131.54/17.52 cnf(d661, plain, e1 = e1 | op(e0,e4) = e0 | e1 != e1, inference(demodulation, [status(thm)], [d660,d498])). % 131.54/17.52 cnf(d662, plain, op(e0,e4) = e0 | e1 != e1 | op(e0,e4) = e0 | op(e3,e1) = e1, inference(resolution, [status(thm)], [d661,d649])). % 131.54/17.52 cnf(d663, plain, op(e0,e4) = e0 | op(e3,e1) = e1, inference(equality_resolution, [status(thm)], [d662])). % 131.54/17.52 cnf(d664, plain, e1 = e3 | op(e4,e3) = e3 | op(e0,e4) = e0, inference(superposition, [status(thm)], [d663,d613])). % 131.54/17.52 cnf(d665, plain, op(e0,e4) = e0 | op(e4,e3) = e3, inference(resolution, [status(thm)], [c205,d664])). % 131.54/17.52 cnf(d666, plain, e0 != e0 | ~'Ts1' | op(e4,e3) = e3, inference(superposition, [status(thm)], [d665,c221])). % 131.54/17.52 cnf(d667, plain, op(e4,e3) = e3 | ~'Ts1', inference(resolution, [status(thm)], [d233,d666])). % 131.54/17.52 cnf(d668, plain, e4 = e3 | ~'Ts1', inference(demodulation, [status(thm)], [d667,d600])). % 131.54/17.52 cnf(d669, plain, ~'Ts1', inference(resolution, [status(thm)], [d620,d668])). % 131.54/17.52 cnf(d670, plain, 'Ts4' | 'Ts3' | 'Ts2', inference(resolution, [status(thm)], [d669,d645])). % 131.54/17.52 cnf(d671, plain, e3 != e3 | ~'Ts3' | op(e4,e3) = e3, inference(superposition, [status(thm)], [d613,c234])). % 131.54/17.52 cnf(d672, plain, op(e4,e3) = e3 | ~'Ts3', inference(equality_resolution, [status(thm)], [d671])). % 131.54/17.52 cnf(d673, plain, e4 = e3 | ~'Ts3', inference(demodulation, [status(thm)], [d672,d600])). % 131.54/17.52 cnf(d674, plain, ~'Ts3', inference(resolution, [status(thm)], [d620,d673])). % 131.54/17.52 cnf(d675, plain, 'Ts4' | 'Ts2', inference(resolution, [status(thm)], [d674,d670])). % 131.54/17.52 cnf(d676, plain, e1 != e1 | ~'Ts4' | op(e3,e1) = e1, inference(superposition, [status(thm)], [d515,c237])). % 131.54/17.52 cnf(d677, plain, op(e3,e1) = e1 | ~'Ts4', inference(equality_resolution, [status(thm)], [d676])). % 131.54/17.52 cnf(d678, plain, ~'Ts4', inference(resolution, [status(thm)], [d622,d677])). % 131.54/17.52 cnf(d679, plain, 'Ts2', inference(resolution, [status(thm)], [d678,d675])). % 131.54/17.52 cnf(d680, plain, op(e2,e3) = e2 | op(e2,e4) = e2, inference(resolution, [status(thm)], [d679,d643])). % 131.54/17.52 cnf(d681, plain, e3 = e2 | op(e2,e4) = e2, inference(demodulation, [status(thm)], [d680,d641])). % 131.54/17.52 cnf(d682, plain, e3 = e2 | e4 = e2, inference(demodulation, [status(thm)], [d681,d626])). % 131.54/17.52 cnf(d683, plain, e3 = e2, inference(resolution, [status(thm)], [d510,d682])). % 131.54/17.52 cnf(d684, plain, $false, inference(resolution, [status(thm)], [d24,d683])). % 131.54/17.52 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------