%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG065+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 : n016.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:20 AM UTC 2026 % Result : Theorem 42.24s 10.87s % Output : CNFRefutation 42.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG065+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/5.37 % Computer : n016.cluster.edu % 0.09/5.37 % Model : x86_64 x86_64 % 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/5.37 % Memory : 8046.5625MB % 0.09/5.37 % OS : Linux 6.8.0-71-generic % 0.09/5.37 % CPULimit : 300 % 0.09/5.37 % WCLimit : 300 % 0.09/5.37 % DateTime : Sat Sep 26 21:10:06 UTC 2026 % 0.09/5.37 % CPUTime : % 0.09/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 42.24/10.87 % SZS status Theorem for theBenchmark.p % 42.24/10.87 % SZS output start CNFRefutation for theBenchmark.p % 42.24/10.87 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))))))))))))))))))))))))))))). % 42.24/10.87 fof(ax2, axiom, (op(unit,e0) = e0 & (op(e0,unit) = e0 & (op(unit,e1) = e1 & (op(e1,unit) = e1 & (op(unit,e2) = e2 & (op(e2,unit) = e2 & (op(unit,e3) = e3 & (op(e3,unit) = e3 & (op(unit,e4) = e4 & (op(e4,unit) = e4 & (unit = e0 | (unit = e1 | (unit = e2 | (unit = e3 | unit = e4))))))))))))))). % 42.24/10.87 fof(ax3, 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)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 42.24/10.87 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 42.24/10.87 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 42.24/10.87 fof(ax6, axiom, (e0 = op(op(e4,e2),op(e4,e2)) & (e1 = op(e4,e2) & e3 = op(e2,e4)))). % 42.24/10.87 fof(co1, conjecture, ~(((op(e0,e0) != e0 | op(e0,e0) = e0) & ((op(e0,e0) != e1 | op(e0,e1) = e0) & ((op(e0,e0) != e2 | op(e0,e2) = e0) & ((op(e0,e0) != e3 | op(e0,e3) = e0) & ((op(e0,e0) != e4 | op(e0,e4) = e0) & ((op(e1,e1) != e0 | op(e1,e0) = e1) & ((op(e1,e1) != e1 | op(e1,e1) = e1) & ((op(e1,e1) != e2 | op(e1,e2) = e1) & ((op(e1,e1) != e3 | op(e1,e3) = e1) & ((op(e1,e1) != e4 | op(e1,e4) = e1) & ((op(e2,e2) != e0 | op(e2,e0) = e2) & ((op(e2,e2) != e1 | op(e2,e1) = e2) & ((op(e2,e2) != e2 | op(e2,e2) = e2) & ((op(e2,e2) != e3 | op(e2,e3) = e2) & ((op(e2,e2) != e4 | op(e2,e4) = e2) & ((op(e3,e3) != e0 | op(e3,e0) = e3) & ((op(e3,e3) != e1 | op(e3,e1) = e3) & ((op(e3,e3) != e2 | op(e3,e2) = e3) & ((op(e3,e3) != e3 | op(e3,e3) = e3) & ((op(e3,e3) != e4 | op(e3,e4) = e3) & ((op(e4,e4) != e0 | op(e4,e0) = e4) & ((op(e4,e4) != e1 | op(e4,e1) = e4) & ((op(e4,e4) != e2 | op(e4,e2) = e4) & ((op(e4,e4) != e3 | op(e4,e3) = e4) & ((op(e4,e4) != e4 | op(e4,e4) = e4) & (((op(e0,op(e0,e0)) != e0 & op(e0,op(e0,e0)) = e0) | ((op(e1,op(e1,e0)) != e0 & op(e0,op(e1,e0)) = e1) | ((op(e2,op(e2,e0)) != e0 & op(e0,op(e2,e0)) = e2) | ((op(e3,op(e3,e0)) != e0 & op(e0,op(e3,e0)) = e3) | (op(e4,op(e4,e0)) != e0 & op(e0,op(e4,e0)) = e4))))) & (((op(e0,op(e0,e1)) != e1 & op(e1,op(e0,e1)) = e0) | ((op(e1,op(e1,e1)) != e1 & op(e1,op(e1,e1)) = e1) | ((op(e2,op(e2,e1)) != e1 & op(e1,op(e2,e1)) = e2) | ((op(e3,op(e3,e1)) != e1 & op(e1,op(e3,e1)) = e3) | (op(e4,op(e4,e1)) != e1 & op(e1,op(e4,e1)) = e4))))) & (((op(e0,op(e0,e2)) != e2 & op(e2,op(e0,e2)) = e0) | ((op(e1,op(e1,e2)) != e2 & op(e2,op(e1,e2)) = e1) | ((op(e2,op(e2,e2)) != e2 & op(e2,op(e2,e2)) = e2) | ((op(e3,op(e3,e2)) != e2 & op(e2,op(e3,e2)) = e3) | (op(e4,op(e4,e2)) != e2 & op(e2,op(e4,e2)) = e4))))) & (((op(e0,op(e0,e3)) != e3 & op(e3,op(e0,e3)) = e0) | ((op(e1,op(e1,e3)) != e3 & op(e3,op(e1,e3)) = e1) | ((op(e2,op(e2,e3)) != e3 & op(e3,op(e2,e3)) = e2) | ((op(e3,op(e3,e3)) != e3 & op(e3,op(e3,e3)) = e3) | (op(e4,op(e4,e3)) != e3 & op(e3,op(e4,e3)) = e4))))) & ((op(e0,op(e0,e4)) != e4 & op(e4,op(e0,e4)) = e0) | ((op(e1,op(e1,e4)) != e4 & op(e4,op(e1,e4)) = e1) | ((op(e2,op(e2,e4)) != e4 & op(e4,op(e2,e4)) = e2) | ((op(e3,op(e3,e4)) != e4 & op(e4,op(e3,e4)) = e3) | (op(e4,op(e4,e4)) != e4 & op(e4,op(e4,e4)) = e4)))))))))))))))))))))))))))))))))))). % 42.24/10.87 fof(negated_conjecture, negated_conjecture, ~~(((op(e0,e0) != e0 | op(e0,e0) = e0) & ((op(e0,e0) != e1 | op(e0,e1) = e0) & ((op(e0,e0) != e2 | op(e0,e2) = e0) & ((op(e0,e0) != e3 | op(e0,e3) = e0) & ((op(e0,e0) != e4 | op(e0,e4) = e0) & ((op(e1,e1) != e0 | op(e1,e0) = e1) & ((op(e1,e1) != e1 | op(e1,e1) = e1) & ((op(e1,e1) != e2 | op(e1,e2) = e1) & ((op(e1,e1) != e3 | op(e1,e3) = e1) & ((op(e1,e1) != e4 | op(e1,e4) = e1) & ((op(e2,e2) != e0 | op(e2,e0) = e2) & ((op(e2,e2) != e1 | op(e2,e1) = e2) & ((op(e2,e2) != e2 | op(e2,e2) = e2) & ((op(e2,e2) != e3 | op(e2,e3) = e2) & ((op(e2,e2) != e4 | op(e2,e4) = e2) & ((op(e3,e3) != e0 | op(e3,e0) = e3) & ((op(e3,e3) != e1 | op(e3,e1) = e3) & ((op(e3,e3) != e2 | op(e3,e2) = e3) & ((op(e3,e3) != e3 | op(e3,e3) = e3) & ((op(e3,e3) != e4 | op(e3,e4) = e3) & ((op(e4,e4) != e0 | op(e4,e0) = e4) & ((op(e4,e4) != e1 | op(e4,e1) = e4) & ((op(e4,e4) != e2 | op(e4,e2) = e4) & ((op(e4,e4) != e3 | op(e4,e3) = e4) & ((op(e4,e4) != e4 | op(e4,e4) = e4) & (((op(e0,op(e0,e0)) != e0 & op(e0,op(e0,e0)) = e0) | ((op(e1,op(e1,e0)) != e0 & op(e0,op(e1,e0)) = e1) | ((op(e2,op(e2,e0)) != e0 & op(e0,op(e2,e0)) = e2) | ((op(e3,op(e3,e0)) != e0 & op(e0,op(e3,e0)) = e3) | (op(e4,op(e4,e0)) != e0 & op(e0,op(e4,e0)) = e4))))) & (((op(e0,op(e0,e1)) != e1 & op(e1,op(e0,e1)) = e0) | ((op(e1,op(e1,e1)) != e1 & op(e1,op(e1,e1)) = e1) | ((op(e2,op(e2,e1)) != e1 & op(e1,op(e2,e1)) = e2) | ((op(e3,op(e3,e1)) != e1 & op(e1,op(e3,e1)) = e3) | (op(e4,op(e4,e1)) != e1 & op(e1,op(e4,e1)) = e4))))) & (((op(e0,op(e0,e2)) != e2 & op(e2,op(e0,e2)) = e0) | ((op(e1,op(e1,e2)) != e2 & op(e2,op(e1,e2)) = e1) | ((op(e2,op(e2,e2)) != e2 & op(e2,op(e2,e2)) = e2) | ((op(e3,op(e3,e2)) != e2 & op(e2,op(e3,e2)) = e3) | (op(e4,op(e4,e2)) != e2 & op(e2,op(e4,e2)) = e4))))) & (((op(e0,op(e0,e3)) != e3 & op(e3,op(e0,e3)) = e0) | ((op(e1,op(e1,e3)) != e3 & op(e3,op(e1,e3)) = e1) | ((op(e2,op(e2,e3)) != e3 & op(e3,op(e2,e3)) = e2) | ((op(e3,op(e3,e3)) != e3 & op(e3,op(e3,e3)) = e3) | (op(e4,op(e4,e3)) != e3 & op(e3,op(e4,e3)) = e4))))) & ((op(e0,op(e0,e4)) != e4 & op(e4,op(e0,e4)) = e0) | ((op(e1,op(e1,e4)) != e4 & op(e4,op(e1,e4)) = e1) | ((op(e2,op(e2,e4)) != e4 & op(e4,op(e2,e4)) = e2) | ((op(e3,op(e3,e4)) != e4 & op(e4,op(e3,e4)) = e3) | (op(e4,op(e4,e4)) != e4 & op(e4,op(e4,e4)) = e4))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 42.24/10.87 cnf(c6, plain, op(e1,e1) = e2 | op(e1,e1) = e1 | op(e1,e1) = e0 | op(e1,e1) = e3 | op(e1,e1) = e4, inference(clausification, [status(esa)], [ax1])). % 42.24/10.87 cnf(c8, plain, op(e1,e3) = e2 | op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e3 | op(e1,e3) = e4, inference(clausification, [status(esa)], [ax1])). % 42.24/10.87 cnf(c16, plain, op(e3,e1) = e4 | op(e3,e1) = e0 | op(e3,e1) = e3 | op(e3,e1) = e1 | op(e3,e1) = e2, inference(clausification, [status(esa)], [ax1])). % 42.24/10.87 cnf(c26, plain, op(e0,unit) = e0, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c27, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c28, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c30, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c31, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c32, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c34, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c35, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 42.24/10.87 cnf(c52, 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)], [ax3])). % 42.24/10.87 cnf(c53, 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)], [ax3])). % 42.24/10.87 cnf(c57, plain, op(e1,e2) = e0 | op(e0,e2) = e0 | op(e3,e2) = e0 | op(e2,e2) = e0 | op(e4,e2) = e0, inference(clausification, [status(esa)], [ax3])). % 42.24/10.87 cnf(c67, plain, op(e1,e3) = e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | op(e0,e3) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax3])). % 42.24/10.87 cnf(c69, 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)], [ax3])). % 42.24/10.87 cnf(c76, plain, op(e4,e1) = e0 | op(e4,e0) = e0 | op(e4,e4) = e0 | op(e4,e3) = e0 | op(e4,e2) = e0, inference(clausification, [status(esa)], [ax3])). % 42.24/10.87 cnf(c80, 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)], [ax3])). % 42.24/10.87 cnf(c94, plain, op(e2,e0) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c98, plain, op(e0,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c101, plain, op(e1,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c102, plain, op(e1,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c112, plain, op(e1,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c116, plain, op(e0,e3) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c130, plain, op(e1,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c137, plain, op(e0,e0) != op(e0,e2), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c146, plain, op(e1,e0) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c148, plain, op(e1,e0) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c149, plain, op(e1,e0) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c151, plain, op(e1,e1) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c162, plain, op(e2,e1) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c165, plain, op(e2,e3) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c166, plain, op(e3,e0) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c173, plain, op(e3,e2) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 42.24/10.87 cnf(c186, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c187, plain, e0 != e2, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c188, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c189, plain, e0 != e4, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c190, plain, e1 != e2, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c191, plain, e1 != e3, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c192, plain, e1 != e4, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c193, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c195, plain, e3 != e4, inference(clausification, [status(esa)], [ax5])). % 42.24/10.87 cnf(c196, plain, e0 = op(op(e4,e2),op(e4,e2)), inference(clausification, [status(esa)], [ax6])). % 42.24/10.87 cnf(c197, plain, e1 = op(e4,e2), inference(clausification, [status(esa)], [ax6])). % 42.24/10.87 cnf(c198, plain, e3 = op(e2,e4), inference(clausification, [status(esa)], [ax6])). % 42.24/10.87 cnf(c204, plain, op(e1,e1) != e0 | op(e1,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c206, plain, op(e1,e1) != e2 | op(e1,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c215, plain, op(e3,e3) != e1 | op(e3,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c221, plain, op(e4,e4) != e2 | op(e4,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c224, plain, op(e0,op(e0,e0)) != e0 | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c234, plain, ~X0 | op(e3,op(e3,e0)) != e0 | op(e4,op(e4,e0)) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(c238, plain, ~X0 | op(e1,op(e1,e0)) != e0 | op(e2,op(e2,e0)) != e0 | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 42.24/10.87 cnf(d0, plain, e0 = op(e1,op(e4,e2)), inference(demodulation, [status(thm)], [c196,c197])). % 42.24/10.87 cnf(d1, plain, e0 = op(e1,e1), inference(demodulation, [status(thm)], [d0,c197])). % 42.24/10.87 cnf(d2, plain, op(e1,e0) = e1 | e0 != e0, inference(demodulation, [status(thm)], [c204,d1])). % 42.24/10.87 cnf(d3, plain, op(e1,e0) = e1, inference(equality_resolution, [status(thm)], [d2])). % 42.24/10.87 cnf(d4, plain, e1 != op(e1,e4), inference(demodulation, [status(thm)], [c149,d3])). % 42.24/10.87 cnf(d5, plain, e1 != op(e1,e3), inference(demodulation, [status(thm)], [c148,d3])). % 42.24/10.87 cnf(d6, plain, op(e0,e1) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c27])). % 42.24/10.87 cnf(d7, plain, e1 = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3 | op(e1,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d6,c53])). % 42.24/10.87 cnf(d8, plain, op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3 | e0 = e3 | e1 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(demodulation, [status(thm)], [d7,d1])). % 42.24/10.87 cnf(d9, plain, op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3 | e1 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c188,d8])). % 42.24/10.87 cnf(d10, plain, op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c191,d9])). % 42.24/10.87 cnf(d11, plain, op(e2,e1) != e3, inference(demodulation, [status(thm)], [c162,c198])). % 42.24/10.87 cnf(d12, plain, op(e3,e1) = e3 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d11,d10])). % 42.24/10.87 cnf(d13, plain, op(e3,e0) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c32])). % 42.24/10.87 cnf(d14, plain, e3 != op(e3,e1) | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d13,c166])). % 42.24/10.87 cnf(d15, plain, e1 != op(e3,e1) | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d6,c98])). % 42.24/10.87 cnf(d16, plain, e0 != op(e3,e1) | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [c6,c101])). % 42.24/10.87 cnf(d17, plain, op(e1,e2) != e1, inference(demodulation, [status(thm)], [c112,c197])). % 42.24/10.87 cnf(d18, plain, op(e1,e1) != e2, inference(resolution, [status(thm)], [d17,c206])). % 42.24/10.87 cnf(d19, plain, op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e3,e1), inference(resolution, [status(thm)], [d18,d16])). % 42.24/10.87 cnf(d20, plain, e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e3,e1), inference(demodulation, [status(thm)], [d19,d1])). % 42.24/10.87 cnf(d21, plain, e0 = e3 | e0 = e4 | op(e1,e1) = e1 | e0 != op(e3,e1), inference(demodulation, [status(thm)], [d20,d1])). % 42.24/10.87 cnf(d22, plain, e0 = e3 | e0 = e4 | e0 = e1 | e0 != op(e3,e1), inference(demodulation, [status(thm)], [d21,d1])). % 42.24/10.87 cnf(d23, plain, e0 = e4 | e0 = e1 | e0 != op(e3,e1), inference(resolution, [status(thm)], [c188,d22])). % 42.24/10.87 cnf(d24, plain, e0 != op(e3,e1) | e0 = e4, inference(resolution, [status(thm)], [c186,d23])). % 42.24/10.87 cnf(d25, plain, e0 != op(e3,e1), inference(resolution, [status(thm)], [c189,d24])). % 42.24/10.87 cnf(d26, plain, e0 != e0 | op(e3,e1) = e3 | op(e3,e1) = e2 | op(e3,e1) = e4 | op(e3,e1) = e1, inference(superposition, [status(thm)], [c16,d25])). % 42.24/10.87 cnf(d27, plain, op(e1,e1) = e0 | op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(resolution, [status(thm)], [d18,c6])). % 42.24/10.87 cnf(d28, plain, e0 = e0 | op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d27,d1])). % 42.24/10.87 cnf(d29, plain, e0 = e0 | e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d28,d1])). % 42.24/10.87 cnf(d30, plain, e0 = e0 | e0 = e3 | e0 = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d29,d1])). % 42.24/10.87 cnf(d31, plain, e0 = e0 | e0 = e3 | e0 = e4 | e0 = e1, inference(demodulation, [status(thm)], [d30,d1])). % 42.24/10.87 cnf(d32, plain, e0 = e0 | e0 = e4 | e0 = e1, inference(resolution, [status(thm)], [c188,d31])). % 42.24/10.87 cnf(d33, plain, e0 = e0 | e0 = e4, inference(resolution, [status(thm)], [c186,d32])). % 42.24/10.87 cnf(d34, plain, e0 = e0, inference(resolution, [status(thm)], [c189,d33])). % 42.24/10.87 cnf(d35, plain, op(e3,e1) = e3 | op(e3,e1) = e2 | op(e3,e1) = e4 | op(e3,e1) = e1, inference(resolution, [status(thm)], [d34,d26])). % 42.24/10.87 cnf(d36, plain, e1 != e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e1) = e3 | op(e3,e1) = e2 | op(e3,e1) = e4, inference(superposition, [status(thm)], [d35,d15])). % 42.24/10.87 cnf(d37, plain, e0 != e0 | op(e1,e0) = e1 | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [c6,c204])). % 42.24/10.87 cnf(d38, plain, op(e1,e0) = e1 | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(equality_resolution, [status(thm)], [d37])). % 42.24/10.87 cnf(d39, plain, op(e1,e0) = e1 | op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(resolution, [status(thm)], [d18,d38])). % 42.24/10.87 cnf(d40, plain, e1 = e1 | op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d39,d3])). % 42.24/10.87 cnf(d41, plain, e1 = e1 | e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d40,d1])). % 42.24/10.87 cnf(d42, plain, e1 = e1 | e0 = e3 | e0 = e4 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d41,d1])). % 42.24/10.87 cnf(d43, plain, e1 = e1 | e0 = e3 | e0 = e4 | e0 = e1, inference(demodulation, [status(thm)], [d42,d1])). % 42.24/10.87 cnf(d44, plain, e1 = e1 | e0 = e4 | e0 = e1, inference(resolution, [status(thm)], [c188,d43])). % 42.24/10.87 cnf(d45, plain, e1 = e1 | e0 = e4, inference(resolution, [status(thm)], [c186,d44])). % 42.24/10.87 cnf(d46, plain, e1 = e1, inference(resolution, [status(thm)], [c189,d45])). % 42.24/10.87 cnf(d47, plain, op(e3,e1) = e3 | op(e3,e1) = e2 | op(e3,e1) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d46,d36])). % 42.24/10.87 cnf(d48, plain, e3 != e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e1) = e2 | op(e3,e1) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d47,d14])). % 42.24/10.87 cnf(d49, plain, op(e3,e1) = e2 | op(e3,e1) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d48])). % 42.24/10.87 cnf(d50, plain, e3 = e4 | op(e3,e1) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d12,d49])). % 42.24/10.87 cnf(d51, plain, op(e3,e1) = e2 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c195,d50])). % 42.24/10.87 cnf(d52, plain, e2 = e3 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d51,d12])). % 42.24/10.87 cnf(d53, plain, op(e4,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c193,d52])). % 42.24/10.87 cnf(d54, plain, op(e2,e0) != e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e4) = e2 | op(e4,e1) = e2, inference(superposition, [status(thm)], [c80,c94])). % 42.24/10.87 cnf(d55, plain, op(e2,e0) != e2 | op(e4,e3) = e2 | e1 = e2 | op(e4,e4) = e2 | op(e4,e1) = e2, inference(demodulation, [status(thm)], [d54,c197])). % 42.24/10.87 cnf(d56, plain, e1 = e4 | op(e4,e4) != e2, inference(demodulation, [status(thm)], [c221,c197])). % 42.24/10.87 cnf(d57, plain, op(e4,e4) != e2, inference(resolution, [status(thm)], [c192,d56])). % 42.24/10.87 cnf(d58, plain, op(e2,e0) != e2 | op(e4,e3) = e2 | e1 = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d57,d55])). % 42.24/10.87 cnf(d59, plain, op(e2,e0) != e2 | op(e4,e3) = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c190,d58])). % 42.24/10.87 cnf(d60, plain, op(e2,e0) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c30])). % 42.24/10.87 cnf(d61, plain, e2 != e2 | op(e4,e3) = e2 | op(e4,e1) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d60,d59])). % 42.24/10.87 cnf(d62, plain, op(e4,e3) = e2 | op(e4,e1) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d61])). % 42.24/10.87 cnf(d63, plain, e2 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e3) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d62,d53])). % 42.24/10.87 cnf(d64, plain, op(e4,e3) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c193,d63])). % 42.24/10.87 cnf(d65, plain, op(e0,e3) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c31])). % 42.24/10.87 cnf(d66, plain, e1 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | op(e1,e3) = e1, inference(superposition, [status(thm)], [c69,d65])). % 42.24/10.87 cnf(d67, plain, op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | op(e1,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c191,d66])). % 42.24/10.87 cnf(d68, plain, e1 != e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d67,d5])). % 42.24/10.87 cnf(d69, plain, op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d46,d68])). % 42.24/10.87 cnf(d70, plain, e1 != e1 | op(e3,e1) = e3 | op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d69,c215])). % 42.24/10.87 cnf(d71, plain, op(e3,e1) = e3 | op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d46,d70])). % 42.24/10.87 cnf(d72, plain, e3 != e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d71,d14])). % 42.24/10.87 cnf(d73, plain, op(e2,e3) = e1 | op(e4,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d72])). % 42.24/10.87 cnf(d74, plain, e1 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d73,d64])). % 42.24/10.87 cnf(d75, plain, op(e2,e3) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c190,d74])). % 42.24/10.87 cnf(d76, plain, op(e4,e0) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c34])). % 42.24/10.87 cnf(d77, plain, op(e4,e4) != e0 | op(e3,op(e3,e0)) != e0 | ~'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d76,c234])). % 42.24/10.87 cnf(d78, plain, op(e3,e3) != e0 | op(e4,e4) != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d13,d77])). % 42.24/10.87 cnf(d79, plain, e0 != op(e4,e1) | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [c6,c102])). % 42.24/10.87 cnf(d80, plain, op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e4,e1), inference(resolution, [status(thm)], [d18,d79])). % 42.24/10.87 cnf(d81, plain, e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e4,e1), inference(demodulation, [status(thm)], [d80,d1])). % 42.24/10.87 cnf(d82, plain, e0 = e3 | e0 = e4 | op(e1,e1) = e1 | e0 != op(e4,e1), inference(demodulation, [status(thm)], [d81,d1])). % 42.24/10.87 cnf(d83, plain, e0 = e3 | e0 = e4 | e0 = e1 | e0 != op(e4,e1), inference(demodulation, [status(thm)], [d82,d1])). % 42.24/10.87 cnf(d84, plain, e0 = e4 | e0 = e1 | e0 != op(e4,e1), inference(resolution, [status(thm)], [c188,d83])). % 42.24/10.87 cnf(d85, plain, e0 != op(e4,e1) | e0 = e4, inference(resolution, [status(thm)], [c186,d84])). % 42.24/10.87 cnf(d86, plain, e0 != op(e4,e1), inference(resolution, [status(thm)], [c189,d85])). % 42.24/10.87 cnf(d87, plain, op(e4,e0) = e0 | op(e4,e3) = e0 | e1 = e0 | op(e4,e4) = e0 | op(e4,e1) = e0, inference(demodulation, [status(thm)], [c76,c197])). % 42.24/10.87 cnf(d88, plain, e1 != op(e1,e1) | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [d38,c146])). % 42.24/10.87 cnf(d89, plain, e1 != e0 | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1 | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [c6,d88])). % 42.24/10.87 cnf(d90, plain, op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e1 != e0, inference(resolution, [status(thm)], [d18,d89])). % 42.24/10.87 cnf(d91, plain, e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e1 != e0, inference(demodulation, [status(thm)], [d90,d1])). % 42.24/10.87 cnf(d92, plain, e0 = e3 | e0 = e4 | op(e1,e1) = e1 | e1 != e0, inference(demodulation, [status(thm)], [d91,d1])). % 42.24/10.87 cnf(d93, plain, e0 = e3 | e0 = e4 | e0 = e1 | e1 != e0, inference(demodulation, [status(thm)], [d92,d1])). % 42.24/10.87 cnf(d94, plain, e0 = e4 | e0 = e1 | e1 != e0, inference(resolution, [status(thm)], [c188,d93])). % 42.24/10.87 cnf(d95, plain, e0 = e4 | e1 != e0, inference(resolution, [status(thm)], [c186,d94])). % 42.24/10.87 cnf(d96, plain, e1 != e0, inference(resolution, [status(thm)], [c189,d95])). % 42.24/10.87 cnf(d97, plain, op(e4,e0) = e0 | op(e4,e3) = e0 | op(e4,e4) = e0 | op(e4,e1) = e0, inference(resolution, [status(thm)], [d96,d87])). % 42.24/10.87 cnf(d98, plain, e0 = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e3) = e0 | op(e4,e4) = e0 | op(e4,e1) = e0, inference(superposition, [status(thm)], [d97,d76])). % 42.24/10.87 cnf(d99, plain, op(e4,e3) = e0 | op(e4,e4) = e0 | op(e4,e1) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c189,d98])). % 42.24/10.87 cnf(d100, plain, e0 != e0 | op(e4,e3) = e0 | op(e4,e4) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d99,d86])). % 42.24/10.87 cnf(d101, plain, op(e4,e3) = e0 | op(e4,e4) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d34,d100])). % 42.24/10.87 cnf(d102, plain, e0 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e4) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d101,d64])). % 42.24/10.87 cnf(d103, plain, op(e4,e4) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c187,d102])). % 42.24/10.87 cnf(d104, plain, e0 != e0 | op(e3,e3) != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d103,d78])). % 42.24/10.87 cnf(d105, plain, op(e3,e3) != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts0', inference(resolution, [status(thm)], [d34,d104])). % 42.24/10.87 cnf(d106, plain, e0 != op(e1,e3) | op(e1,e1) = e3 | op(e1,e1) = e2 | op(e1,e1) = e4 | op(e1,e1) = e1, inference(superposition, [status(thm)], [c6,c151])). % 42.24/10.87 cnf(d107, plain, op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e1,e3), inference(resolution, [status(thm)], [d18,d106])). % 42.24/10.87 cnf(d108, plain, e0 = e3 | op(e1,e1) = e4 | op(e1,e1) = e1 | e0 != op(e1,e3), inference(demodulation, [status(thm)], [d107,d1])). % 42.24/10.87 cnf(d109, plain, e0 = e3 | e0 = e4 | op(e1,e1) = e1 | e0 != op(e1,e3), inference(demodulation, [status(thm)], [d108,d1])). % 42.24/10.87 cnf(d110, plain, e0 = e3 | e0 = e4 | e0 = e1 | e0 != op(e1,e3), inference(demodulation, [status(thm)], [d109,d1])). % 42.24/10.87 cnf(d111, plain, e0 = e4 | e0 = e1 | e0 != op(e1,e3), inference(resolution, [status(thm)], [c188,d110])). % 42.24/10.87 cnf(d112, plain, e0 != op(e1,e3) | e0 = e4, inference(resolution, [status(thm)], [c186,d111])). % 42.24/10.87 cnf(d113, plain, e0 != op(e1,e3), inference(resolution, [status(thm)], [c189,d112])). % 42.24/10.87 cnf(d114, plain, e0 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e3) = e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | op(e1,e3) = e0, inference(superposition, [status(thm)], [c67,d65])). % 42.24/10.87 cnf(d115, plain, op(e3,e3) = e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | op(e1,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c188,d114])). % 42.24/10.87 cnf(d116, plain, e0 != e0 | op(e3,e3) = e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d115,d113])). % 42.24/10.87 cnf(d117, plain, op(e3,e3) = e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d34,d116])). % 42.24/10.87 cnf(d118, plain, e0 != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts0' | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d117,d105])). % 42.24/10.87 cnf(d119, plain, op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts0', inference(resolution, [status(thm)], [d34,d118])). % 42.24/10.87 cnf(d120, plain, op(e0,e0) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c26])). % 42.24/10.87 cnf(d121, plain, op(e0,e0) != e0 | 'Ts1' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d120,c224])). % 42.24/10.87 cnf(d122, plain, e0 != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts1' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d120,d121])). % 42.24/10.87 cnf(d123, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d122])). % 42.24/10.87 cnf(d124, plain, op(e2,op(e2,e0)) != e0 | op(e1,e1) != e0 | ~'Ts1' | 'Ts0', inference(demodulation, [status(thm)], [c238,d3])). % 42.24/10.87 cnf(d125, plain, op(e2,op(e2,e0)) != e0 | e0 != e0 | ~'Ts1' | 'Ts0', inference(demodulation, [status(thm)], [d124,d1])). % 42.24/10.87 cnf(d126, plain, op(e2,op(e2,e0)) != e0 | ~'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d34,d125])). % 42.24/10.87 cnf(d127, plain, op(e2,e2) != e0 | ~'Ts1' | 'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d60,d126])). % 42.24/10.87 cnf(d128, plain, op(e3,e2) != e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d117,c173])). % 42.24/10.87 cnf(d129, plain, op(e1,e0) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c35,c28])). % 42.24/10.87 cnf(d130, plain, e1 = e3 | op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3 | op(e1,e1) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d129,c52])). % 42.24/10.87 cnf(d131, plain, op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3 | e0 = e3 | e1 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(demodulation, [status(thm)], [d130,d1])). % 42.24/10.87 cnf(d132, plain, op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3 | e1 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c188,d131])). % 42.24/10.87 cnf(d133, plain, op(e1,e3) = e3 | op(e1,e2) = e3 | op(e1,e4) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c191,d132])). % 42.24/10.87 cnf(d134, plain, op(e1,e4) != e3, inference(demodulation, [status(thm)], [c130,c198])). % 42.24/10.87 cnf(d135, plain, op(e1,e3) = e3 | op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d134,d133])). % 42.24/10.87 cnf(d136, plain, e3 != op(e1,e3) | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d65,c116])). % 42.24/10.87 cnf(d137, plain, e0 != e0 | op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4 | op(e1,e3) = e1, inference(superposition, [status(thm)], [c8,d113])). % 42.24/10.87 cnf(d138, plain, op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4 | op(e1,e3) = e1, inference(resolution, [status(thm)], [d34,d137])). % 42.24/10.87 cnf(d139, plain, e1 != e1 | op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4, inference(superposition, [status(thm)], [d138,d5])). % 42.24/10.87 cnf(d140, plain, op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4, inference(resolution, [status(thm)], [d46,d139])). % 42.24/10.87 cnf(d141, plain, e3 != e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e1,e3) = e2 | op(e1,e3) = e4, inference(superposition, [status(thm)], [d140,d136])). % 42.24/10.87 cnf(d142, plain, op(e1,e3) = e2 | op(e1,e3) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d141])). % 42.24/10.87 cnf(d143, plain, e3 = e4 | op(e1,e3) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d135,d142])). % 42.24/10.87 cnf(d144, plain, op(e1,e3) = e2 | op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c195,d143])). % 42.24/10.87 cnf(d145, plain, e2 = e3 | op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d144,d135])). % 42.24/10.87 cnf(d146, plain, op(e1,e2) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c193,d145])). % 42.24/10.87 cnf(d147, plain, e0 != op(e0,e2) | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d120,c137])). % 42.24/10.87 cnf(d148, plain, op(e0,e2) = e0 | op(e3,e2) = e0 | op(e2,e2) = e0 | e1 = e0 | op(e1,e2) = e0, inference(demodulation, [status(thm)], [c57,c197])). % 42.24/10.87 cnf(d149, plain, op(e0,e2) = e0 | op(e3,e2) = e0 | op(e2,e2) = e0 | op(e1,e2) = e0, inference(resolution, [status(thm)], [d96,d148])). % 42.24/10.87 cnf(d150, plain, e0 != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e2) = e0 | op(e2,e2) = e0 | op(e1,e2) = e0, inference(superposition, [status(thm)], [d149,d147])). % 42.24/10.87 cnf(d151, plain, op(e3,e2) = e0 | op(e2,e2) = e0 | op(e1,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d34,d150])). % 42.24/10.87 cnf(d152, plain, e0 = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e3,e2) = e0 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d151,d146])). % 42.24/10.87 cnf(d153, plain, op(e3,e2) = e0 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c188,d152])). % 42.24/10.87 cnf(d154, plain, e0 != e0 | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d153,d128])). % 42.24/10.87 cnf(d155, plain, op(e2,e3) = e0 | op(e2,e2) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d34,d154])). % 42.24/10.87 cnf(d156, plain, e0 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e3) = e0 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d155,d64])). % 42.24/10.87 cnf(d157, plain, op(e2,e3) = e0 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c187,d156])). % 42.24/10.87 cnf(d158, plain, e0 = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d157,d75])). % 42.24/10.87 cnf(d159, plain, op(e2,e2) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c186,d158])). % 42.24/10.87 cnf(d160, plain, e0 != e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts1' | 'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d159,d127])). % 42.24/10.87 cnf(d161, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d34,d160])). % 42.24/10.87 cnf(d162, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts0' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d161,d123])). % 42.24/10.87 cnf(d163, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e3) = e0 | op(e4,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d162,d119])). % 42.24/10.87 cnf(d164, plain, e0 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d163,d64])). % 42.24/10.87 cnf(d165, plain, op(e2,e3) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c187,d164])). % 42.24/10.87 cnf(d166, plain, e0 = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d165,d75])). % 42.24/10.87 cnf(d167, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c186,d166])). % 42.24/10.87 cnf(d168, plain, op(e1,e1) = e1 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d167,c28])). % 42.24/10.87 cnf(d169, plain, e0 = e1 | unit = e3 | unit = e2 | unit = e4, inference(demodulation, [status(thm)], [d168,d1])). % 42.24/10.87 cnf(d170, plain, unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c186,d169])). % 42.24/10.87 cnf(d171, plain, op(e1,e3) = e1 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d170,c28])). % 42.24/10.87 cnf(d172, plain, e1 != e1 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d171,d5])). % 42.24/10.87 cnf(d173, plain, unit = e2 | unit = e4, inference(resolution, [status(thm)], [d46,d172])). % 42.24/10.87 cnf(d174, plain, op(e1,e4) = e1 | unit = e2, inference(superposition, [status(thm)], [d173,c28])). % 42.24/10.87 cnf(d175, plain, e1 != e1 | unit = e2, inference(superposition, [status(thm)], [d174,d4])). % 42.24/10.87 cnf(d176, plain, unit = e2, inference(resolution, [status(thm)], [d46,d175])). % 42.24/10.87 cnf(d177, plain, op(e2,e3) = e3, inference(demodulation, [status(thm)], [c31,d176])). % 42.24/10.87 cnf(d178, plain, op(e2,e3) != e3, inference(demodulation, [status(thm)], [c165,c198])). % 42.24/10.87 cnf(d179, plain, $false, inference(resolution, [status(thm)], [d178,d177])). % 42.24/10.87 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------