%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG068+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 : n011.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:21 AM UTC 2026 % Result : Theorem 62.94s 8.76s % Output : CNFRefutation 62.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG068+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.08/0.35 % Computer : n011.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 21:05:30 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 62.94/8.76 % SZS status Theorem for theBenchmark.p % 62.94/8.76 % SZS output start CNFRefutation for theBenchmark.p % 62.94/8.76 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))))))))))))))))))))))))))))). % 62.94/8.76 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))))))))))))))). % 62.94/8.76 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)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 62.94/8.76 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 62.94/8.76 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 62.94/8.76 fof(ax6, axiom, (e0 = op(op(e4,e2),op(e4,e2)) & (e1 = op(e4,e2) & e3 = op(e2,e4)))). % 62.94/8.76 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,e0) != op(e0,e0) & (op(op(e0,e0),e0) = e0 & op(op(e0,e0),e0) != e0)) | ((op(e1,e0) != op(e0,e1) & (op(op(e0,e1),e1) = e0 & op(op(e0,e1),e0) != e1)) | ((op(e2,e0) != op(e0,e2) & (op(op(e0,e2),e2) = e0 & op(op(e0,e2),e0) != e2)) | ((op(e3,e0) != op(e0,e3) & (op(op(e0,e3),e3) = e0 & op(op(e0,e3),e0) != e3)) | ((op(e4,e0) != op(e0,e4) & (op(op(e0,e4),e4) = e0 & op(op(e0,e4),e0) != e4)) | ((op(e0,e1) != op(e1,e0) & (op(op(e1,e0),e0) = e1 & op(op(e1,e0),e1) != e0)) | ((op(e1,e1) != op(e1,e1) & (op(op(e1,e1),e1) = e1 & op(op(e1,e1),e1) != e1)) | ((op(e2,e1) != op(e1,e2) & (op(op(e1,e2),e2) = e1 & op(op(e1,e2),e1) != e2)) | ((op(e3,e1) != op(e1,e3) & (op(op(e1,e3),e3) = e1 & op(op(e1,e3),e1) != e3)) | ((op(e4,e1) != op(e1,e4) & (op(op(e1,e4),e4) = e1 & op(op(e1,e4),e1) != e4)) | ((op(e0,e2) != op(e2,e0) & (op(op(e2,e0),e0) = e2 & op(op(e2,e0),e2) != e0)) | ((op(e1,e2) != op(e2,e1) & (op(op(e2,e1),e1) = e2 & op(op(e2,e1),e2) != e1)) | ((op(e2,e2) != op(e2,e2) & (op(op(e2,e2),e2) = e2 & op(op(e2,e2),e2) != e2)) | ((op(e3,e2) != op(e2,e3) & (op(op(e2,e3),e3) = e2 & op(op(e2,e3),e2) != e3)) | ((op(e4,e2) != op(e2,e4) & (op(op(e2,e4),e4) = e2 & op(op(e2,e4),e2) != e4)) | ((op(e0,e3) != op(e3,e0) & (op(op(e3,e0),e0) = e3 & op(op(e3,e0),e3) != e0)) | ((op(e1,e3) != op(e3,e1) & (op(op(e3,e1),e1) = e3 & op(op(e3,e1),e3) != e1)) | ((op(e2,e3) != op(e3,e2) & (op(op(e3,e2),e2) = e3 & op(op(e3,e2),e3) != e2)) | ((op(e3,e3) != op(e3,e3) & (op(op(e3,e3),e3) = e3 & op(op(e3,e3),e3) != e3)) | ((op(e4,e3) != op(e3,e4) & (op(op(e3,e4),e4) = e3 & op(op(e3,e4),e3) != e4)) | ((op(e0,e4) != op(e4,e0) & (op(op(e4,e0),e0) = e4 & op(op(e4,e0),e4) != e0)) | ((op(e1,e4) != op(e4,e1) & (op(op(e4,e1),e1) = e4 & op(op(e4,e1),e4) != e1)) | ((op(e2,e4) != op(e4,e2) & (op(op(e4,e2),e2) = e4 & op(op(e4,e2),e4) != e2)) | ((op(e3,e4) != op(e4,e3) & (op(op(e4,e3),e3) = e4 & op(op(e4,e3),e4) != e3)) | (op(e4,e4) != op(e4,e4) & (op(op(e4,e4),e4) = e4 & op(op(e4,e4),e4) != e4))))))))))))))))))))))))))))))))))))))))))))))))))))). % 62.94/8.76 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,e0) != op(e0,e0) & (op(op(e0,e0),e0) = e0 & op(op(e0,e0),e0) != e0)) | ((op(e1,e0) != op(e0,e1) & (op(op(e0,e1),e1) = e0 & op(op(e0,e1),e0) != e1)) | ((op(e2,e0) != op(e0,e2) & (op(op(e0,e2),e2) = e0 & op(op(e0,e2),e0) != e2)) | ((op(e3,e0) != op(e0,e3) & (op(op(e0,e3),e3) = e0 & op(op(e0,e3),e0) != e3)) | ((op(e4,e0) != op(e0,e4) & (op(op(e0,e4),e4) = e0 & op(op(e0,e4),e0) != e4)) | ((op(e0,e1) != op(e1,e0) & (op(op(e1,e0),e0) = e1 & op(op(e1,e0),e1) != e0)) | ((op(e1,e1) != op(e1,e1) & (op(op(e1,e1),e1) = e1 & op(op(e1,e1),e1) != e1)) | ((op(e2,e1) != op(e1,e2) & (op(op(e1,e2),e2) = e1 & op(op(e1,e2),e1) != e2)) | ((op(e3,e1) != op(e1,e3) & (op(op(e1,e3),e3) = e1 & op(op(e1,e3),e1) != e3)) | ((op(e4,e1) != op(e1,e4) & (op(op(e1,e4),e4) = e1 & op(op(e1,e4),e1) != e4)) | ((op(e0,e2) != op(e2,e0) & (op(op(e2,e0),e0) = e2 & op(op(e2,e0),e2) != e0)) | ((op(e1,e2) != op(e2,e1) & (op(op(e2,e1),e1) = e2 & op(op(e2,e1),e2) != e1)) | ((op(e2,e2) != op(e2,e2) & (op(op(e2,e2),e2) = e2 & op(op(e2,e2),e2) != e2)) | ((op(e3,e2) != op(e2,e3) & (op(op(e2,e3),e3) = e2 & op(op(e2,e3),e2) != e3)) | ((op(e4,e2) != op(e2,e4) & (op(op(e2,e4),e4) = e2 & op(op(e2,e4),e2) != e4)) | ((op(e0,e3) != op(e3,e0) & (op(op(e3,e0),e0) = e3 & op(op(e3,e0),e3) != e0)) | ((op(e1,e3) != op(e3,e1) & (op(op(e3,e1),e1) = e3 & op(op(e3,e1),e3) != e1)) | ((op(e2,e3) != op(e3,e2) & (op(op(e3,e2),e2) = e3 & op(op(e3,e2),e3) != e2)) | ((op(e3,e3) != op(e3,e3) & (op(op(e3,e3),e3) = e3 & op(op(e3,e3),e3) != e3)) | ((op(e4,e3) != op(e3,e4) & (op(op(e3,e4),e4) = e3 & op(op(e3,e4),e3) != e4)) | ((op(e0,e4) != op(e4,e0) & (op(op(e4,e0),e0) = e4 & op(op(e4,e0),e4) != e0)) | ((op(e1,e4) != op(e4,e1) & (op(op(e4,e1),e1) = e4 & op(op(e4,e1),e4) != e1)) | ((op(e2,e4) != op(e4,e2) & (op(op(e4,e2),e2) = e4 & op(op(e4,e2),e4) != e2)) | ((op(e3,e4) != op(e4,e3) & (op(op(e4,e3),e3) = e4 & op(op(e4,e3),e4) != e3)) | (op(e4,e4) != op(e4,e4) & (op(op(e4,e4),e4) = e4 & op(op(e4,e4),e4) != e4)))))))))))))))))))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 62.94/8.76 cnf(c7, plain, op(e1,e2) = e0 | op(e1,e2) = e2 | op(e1,e2) = e4 | op(e1,e2) = e3 | op(e1,e2) = e1, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 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])). % 62.94/8.76 cnf(c12, plain, op(e2,e2) = e4 | op(e2,e2) = e0 | op(e2,e2) = e3 | op(e2,e2) = e1 | op(e2,e2) = e2, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 cnf(c18, plain, op(e3,e3) = e2 | op(e3,e3) = e4 | op(e3,e3) = e1 | op(e3,e3) = e3 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 cnf(c21, plain, op(e4,e1) = e1 | op(e4,e1) = e0 | op(e4,e1) = e4 | op(e4,e1) = e2 | op(e4,e1) = e3, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 cnf(c22, plain, op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e1 | op(e4,e2) = e0 | op(e4,e2) = e4, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 cnf(c24, plain, op(e4,e4) = e4 | op(e4,e4) = e0 | op(e4,e4) = e1 | op(e4,e4) = e2 | op(e4,e4) = e3, inference(clausification, [status(esa)], [ax1])). % 62.94/8.76 cnf(c27, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c28, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c29, plain, op(unit,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c30, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c31, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c32, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c33, plain, op(unit,e4) = e4, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c34, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c35, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 62.94/8.76 cnf(c50, 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)], [ax3])). % 62.94/8.76 cnf(c51, plain, op(e2,e1) = e2 | op(e1,e1) = e2 | op(e4,e1) = e2 | op(e0,e1) = e2 | op(e3,e1) = e2, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 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])). % 62.94/8.76 cnf(c54, plain, op(e1,e0) = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4 | op(e1,e1) = e4, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c55, plain, op(e4,e1) = e4 | op(e2,e1) = e4 | op(e1,e1) = e4 | op(e3,e1) = e4 | op(e0,e1) = e4, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c58, plain, op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e3) = e1 | op(e2,e4) = e1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c64, plain, op(e2,e2) = e4 | op(e2,e4) = e4 | op(e2,e1) = e4 | op(e2,e3) = e4 | op(e2,e0) = e4, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c65, plain, op(e3,e2) = e4 | op(e2,e2) = e4 | op(e0,e2) = e4 | op(e1,e2) = e4 | op(e4,e2) = e4, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c79, plain, op(e1,e4) = e1 | op(e2,e4) = e1 | op(e3,e4) = e1 | op(e0,e4) = e1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 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])). % 62.94/8.76 cnf(c81, plain, op(e2,e4) = e2 | op(e3,e4) = e2 | op(e0,e4) = e2 | op(e4,e4) = e2 | op(e1,e4) = e2, inference(clausification, [status(esa)], [ax3])). % 62.94/8.76 cnf(c82, 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)], [ax3])). % 62.94/8.76 cnf(c97, plain, op(e0,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c103, plain, op(e2,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c105, plain, op(e3,e1) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c109, plain, op(e0,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c110, plain, op(e1,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c111, plain, op(e1,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c112, plain, op(e1,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c114, plain, op(e2,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c116, plain, op(e0,e3) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c118, plain, op(e0,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c119, plain, op(e0,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c121, plain, op(e1,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c122, plain, op(e1,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c125, plain, op(e3,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c127, plain, op(e0,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c130, plain, op(e1,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c134, plain, op(e2,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c146, plain, op(e1,e0) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c148, plain, op(e1,e0) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c149, plain, op(e1,e0) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c153, plain, op(e1,e2) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c154, plain, op(e1,e2) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c156, plain, op(e2,e0) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c157, plain, op(e2,e0) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c162, plain, op(e2,e1) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.76 cnf(c164, plain, op(e2,e2) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c166, plain, op(e3,e0) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c176, plain, op(e4,e0) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c177, plain, op(e4,e0) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c179, plain, op(e4,e0) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c180, plain, op(e4,e1) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c182, plain, op(e4,e1) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c184, plain, op(e4,e2) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 62.94/8.77 cnf(c186, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c188, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c190, plain, e1 != e2, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c191, plain, e1 != e3, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c192, plain, e1 != e4, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c193, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c194, plain, e2 != e4, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c195, plain, e3 != e4, inference(clausification, [status(esa)], [ax5])). % 62.94/8.77 cnf(c196, plain, e0 = op(op(e4,e2),op(e4,e2)), inference(clausification, [status(esa)], [ax6])). % 62.94/8.77 cnf(c197, plain, e1 = op(e4,e2), inference(clausification, [status(esa)], [ax6])). % 62.94/8.77 cnf(c198, plain, e3 = op(e2,e4), inference(clausification, [status(esa)], [ax6])). % 62.94/8.77 cnf(c204, plain, op(e1,e1) != e0 | op(e1,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c206, plain, op(e1,e1) != e2 | op(e1,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c207, plain, op(e1,e1) != e3 | op(e1,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c208, plain, op(e1,e1) != e4 | op(e1,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c210, plain, op(e2,e2) != e1 | op(e2,e1) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c213, plain, op(e2,e2) != e4 | op(e2,e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c215, plain, op(e3,e3) != e1 | op(e3,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c218, plain, op(e3,e3) != e4 | op(e3,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c221, plain, op(e4,e4) != e2 | op(e4,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c224, plain, X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | op(e4,e4) != op(e4,e4) | X15 | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c229, plain, ~X0 | op(op(e4,e3),e4) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c232, plain, ~X0 | op(op(e4,e2),e4) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c235, plain, ~X0 | op(op(e4,e1),e4) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c236, plain, ~X0 | op(e0,e4) != op(e4,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c240, plain, ~X0 | op(op(e3,e4),e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c242, plain, ~X0 | op(e3,e3) != op(e3,e3), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c246, plain, ~X0 | op(op(e3,e2),e2) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c249, plain, ~X0 | op(op(e3,e1),e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c251, plain, ~X0 | op(e0,e3) != op(e3,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c255, plain, ~X0 | op(op(e2,e4),e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c258, plain, ~X0 | op(op(e2,e3),e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c260, plain, ~X0 | op(e2,e2) != op(e2,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c265, plain, ~X0 | op(op(e2,e1),e2) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c266, plain, ~X0 | op(e0,e2) != op(e2,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c271, plain, ~X0 | op(op(e1,e4),e1) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c274, plain, ~X0 | op(op(e1,e3),e1) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c277, plain, ~X0 | op(op(e1,e2),e1) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c278, plain, ~X0 | op(e1,e1) != op(e1,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c283, plain, ~X0 | op(op(e1,e0),e1) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c284, plain, ~X0 | op(e4,e0) != op(e0,e4), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c289, plain, ~X0 | op(op(e0,e3),e0) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c290, plain, ~X0 | op(e2,e0) != op(e0,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c293, plain, ~X0 | op(e1,e0) != op(e0,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(c296, plain, ~X0 | op(e0,e0) != op(e0,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.94/8.77 cnf(d0, plain, e0 = op(e1,op(e4,e2)), inference(demodulation, [status(thm)], [c196,c197])). % 62.94/8.77 cnf(d1, plain, e0 = op(e1,e1), inference(demodulation, [status(thm)], [d0,c197])). % 62.94/8.77 cnf(d2, plain, op(e1,e0) = e1 | e0 != e0, inference(demodulation, [status(thm)], [c204,d1])). % 62.94/8.77 cnf(d3, plain, op(e1,e0) = e1, inference(equality_resolution, [status(thm)], [d2])). % 62.94/8.77 cnf(d4, plain, e1 != op(e1,e3), inference(demodulation, [status(thm)], [c148,d3])). % 62.94/8.77 cnf(d5, plain, e1 != op(e1,e4), inference(demodulation, [status(thm)], [c149,d3])). % 62.94/8.77 cnf(d6, plain, op(e1,e1) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c35,c28])). % 62.94/8.77 cnf(d7, plain, op(e1,e0) != e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d6,c146])). % 62.94/8.77 cnf(d8, plain, e1 != e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(demodulation, [status(thm)], [d7,d3])). % 62.94/8.77 cnf(d9, plain, unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(equality_resolution, [status(thm)], [d8])). % 62.94/8.77 cnf(d10, plain, op(e1,e4) = e1 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d9,c28])). % 62.94/8.77 cnf(d11, plain, e1 != e1 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d10,d5])). % 62.94/8.77 cnf(d12, plain, unit = e0 | unit = e3 | unit = e2, inference(equality_resolution, [status(thm)], [d11])). % 62.94/8.77 cnf(d13, plain, op(e2,e4) = e4 | unit = e0 | unit = e3, inference(superposition, [status(thm)], [d12,c33])). % 62.94/8.77 cnf(d14, plain, e3 = e4 | unit = e0 | unit = e3, inference(demodulation, [status(thm)], [d13,c198])). % 62.94/8.77 cnf(d15, plain, unit = e0 | unit = e3, inference(resolution, [status(thm)], [c195,d14])). % 62.94/8.77 cnf(d16, plain, op(e1,e3) = e1 | unit = e0, inference(superposition, [status(thm)], [d15,c28])). % 62.94/8.77 cnf(d17, plain, e1 != e1 | unit = e0, inference(superposition, [status(thm)], [d16,d4])). % 62.94/8.77 cnf(d18, plain, unit = e0, inference(equality_resolution, [status(thm)], [d17])). % 62.94/8.77 cnf(d19, plain, op(e0,e3) = e3, inference(demodulation, [status(thm)], [c31,d18])). % 62.94/8.77 cnf(d20, plain, e3 != op(e1,e3), inference(demodulation, [status(thm)], [c116,d19])). % 62.94/8.77 cnf(d21, plain, op(e0,e2) = e2, inference(demodulation, [status(thm)], [c29,d18])). % 62.94/8.77 cnf(d22, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | op(e2,e2) = e4 | e1 = e4 | op(e1,e2) = e4, inference(demodulation, [status(thm)], [c65,c197])). % 62.94/8.77 cnf(d23, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | op(e2,e2) = e4 | op(e1,e2) = e4, inference(resolution, [status(thm)], [c192,d22])). % 62.94/8.77 cnf(d24, plain, e2 = e4 | op(e3,e2) = e4 | op(e2,e2) = e4 | op(e1,e2) = e4, inference(demodulation, [status(thm)], [d23,d21])). % 62.94/8.77 cnf(d25, plain, op(e3,e2) = e4 | op(e2,e2) = e4 | op(e1,e2) = e4, inference(resolution, [status(thm)], [c194,d24])). % 62.94/8.77 cnf(d26, plain, e4 != op(e1,e3) | op(e3,e2) = e4 | op(e2,e2) = e4, inference(superposition, [status(thm)], [d25,c153])). % 62.94/8.77 cnf(d27, plain, op(e2,e2) != e4 | e3 = e2, inference(demodulation, [status(thm)], [c213,c198])). % 62.94/8.77 cnf(d28, plain, op(e2,e0) = e2, inference(demodulation, [status(thm)], [c30,d18])). % 62.94/8.77 cnf(d29, plain, e2 != op(e2,e1), inference(demodulation, [status(thm)], [c156,d28])). % 62.94/8.77 cnf(d30, plain, e3 != op(e4,e3), inference(demodulation, [status(thm)], [c119,d19])). % 62.94/8.77 cnf(d31, plain, e3 != op(e4,e4), inference(demodulation, [status(thm)], [c134,c198])). % 62.94/8.77 cnf(d32, plain, op(e4,e2) != e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e4,e4) = e4, inference(superposition, [status(thm)], [c24,c184])). % 62.94/8.77 cnf(d33, plain, e1 != e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e4,e4) = e4, inference(demodulation, [status(thm)], [d32,c197])). % 62.94/8.77 cnf(d34, plain, e1 = e4 | op(e4,e4) != e2, inference(demodulation, [status(thm)], [c221,c197])). % 62.94/8.77 cnf(d35, plain, op(e4,e4) != e2, inference(resolution, [status(thm)], [c192,d34])). % 62.94/8.77 cnf(d36, plain, e1 != e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e4, inference(resolution, [status(thm)], [d35,d33])). % 62.94/8.77 cnf(d37, plain, op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e4, inference(equality_resolution, [status(thm)], [d36])). % 62.94/8.77 cnf(d38, plain, op(e4,e0) != e4 | op(e4,e4) = e0 | op(e4,e4) = e3, inference(superposition, [status(thm)], [d37,c179])). % 62.94/8.77 cnf(d39, plain, op(e4,e0) = e4, inference(demodulation, [status(thm)], [c34,d18])). % 62.94/8.77 cnf(d40, plain, op(e4,e4) = e0 | op(e4,e4) = e3, inference(resolution, [status(thm)], [d39,d38])). % 62.94/8.77 cnf(d41, plain, e3 != e3 | op(e4,e4) = e0, inference(superposition, [status(thm)], [d40,d31])). % 62.94/8.77 cnf(d42, plain, op(e4,e4) = e0, inference(equality_resolution, [status(thm)], [d41])). % 62.94/8.77 cnf(d43, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | e1 = e3 | op(e4,e4) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [c82,c197])). % 62.94/8.77 cnf(d44, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e4) = e3 | op(e4,e1) = e3, inference(resolution, [status(thm)], [c191,d43])). % 62.94/8.77 cnf(d45, plain, e4 = e3 | op(e4,e3) = e3 | op(e4,e4) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d44,d39])). % 62.94/8.77 cnf(d46, plain, op(e4,e3) = e3 | e0 = e3 | op(e4,e1) = e3 | e4 = e3, inference(demodulation, [status(thm)], [d45,d42])). % 62.94/8.77 cnf(d47, plain, op(e4,e3) = e3 | op(e4,e1) = e3 | e4 = e3, inference(resolution, [status(thm)], [c188,d46])). % 62.94/8.77 cnf(d48, plain, op(e0,e4) = e4, inference(demodulation, [status(thm)], [c33,d18])). % 62.94/8.77 cnf(d49, plain, op(e0,e4) != e3, inference(demodulation, [status(thm)], [c127,c198])). % 62.94/8.77 cnf(d50, plain, e4 != e3, inference(demodulation, [status(thm)], [d49,d48])). % 62.94/8.77 cnf(d51, plain, op(e4,e3) = e3 | op(e4,e1) = e3, inference(resolution, [status(thm)], [d50,d47])). % 62.94/8.77 cnf(d52, plain, op(e0,e1) = e1, inference(demodulation, [status(thm)], [c27,d18])). % 62.94/8.77 cnf(d53, plain, e2 != e2 | op(e1,e2) = e1 | op(e0,e1) = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2, inference(superposition, [status(thm)], [c51,c206])). % 62.94/8.77 cnf(d54, plain, op(e0,e1) = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2 | op(e1,e2) = e1, inference(equality_resolution, [status(thm)], [d53])). % 62.94/8.77 cnf(d55, plain, op(e1,e2) != e1, inference(demodulation, [status(thm)], [c112,c197])). % 62.94/8.77 cnf(d56, plain, op(e0,e1) = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d55,d54])). % 62.94/8.77 cnf(d57, plain, e1 = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2, inference(demodulation, [status(thm)], [d56,d52])). % 62.94/8.77 cnf(d58, plain, op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c190,d57])). % 62.94/8.77 cnf(d59, plain, e2 = e3 | op(e4,e3) = e3 | op(e3,e1) = e2 | op(e2,e1) = e2, inference(superposition, [status(thm)], [d58,d51])). % 62.94/8.77 cnf(d60, plain, op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e3) = e3, inference(resolution, [status(thm)], [c193,d59])). % 62.94/8.77 cnf(d61, plain, e3 != e3 | op(e3,e1) = e2 | op(e2,e1) = e2, inference(superposition, [status(thm)], [d60,d30])). % 62.94/8.77 cnf(d62, plain, op(e3,e1) = e2 | op(e2,e1) = e2, inference(equality_resolution, [status(thm)], [d61])). % 62.94/8.77 cnf(d63, plain, e2 != e2 | op(e3,e1) = e2, inference(superposition, [status(thm)], [d62,d29])). % 62.94/8.77 cnf(d64, plain, op(e3,e1) = e2, inference(equality_resolution, [status(thm)], [d63])). % 62.94/8.77 cnf(d65, plain, op(e3,e0) = e3, inference(demodulation, [status(thm)], [c32,d18])). % 62.94/8.77 cnf(d66, plain, e3 != op(e3,e1), inference(demodulation, [status(thm)], [c166,d65])). % 62.94/8.77 cnf(d67, plain, e3 != e2, inference(demodulation, [status(thm)], [d66,d64])). % 62.94/8.77 cnf(d68, plain, op(e2,e2) != e4, inference(resolution, [status(thm)], [d67,d27])). % 62.94/8.77 cnf(d69, plain, op(e3,e2) = e4 | e4 != op(e1,e3), inference(resolution, [status(thm)], [d68,d26])). % 62.94/8.77 cnf(d70, plain, op(e1,e0) != e1 | op(e1,e3) = e0 | op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4, inference(superposition, [status(thm)], [c8,c148])). % 62.94/8.77 cnf(d71, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | op(e1,e3) = e2 | op(e1,e3) = e4, inference(resolution, [status(thm)], [d3,d70])). % 62.94/8.77 cnf(d72, plain, op(e3,e1) != e2 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e4) = e2, inference(superposition, [status(thm)], [c80,c105])). % 62.94/8.77 cnf(d73, plain, op(e3,e1) != e2 | op(e4,e0) = e2 | op(e4,e3) = e2 | e1 = e2 | op(e4,e4) = e2, inference(demodulation, [status(thm)], [d72,c197])). % 62.94/8.77 cnf(d74, plain, op(e3,e1) != e2 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e4) = e2, inference(resolution, [status(thm)], [c190,d73])). % 62.94/8.77 cnf(d75, plain, op(e3,e1) != e2 | op(e4,e0) = e2 | op(e4,e3) = e2, inference(resolution, [status(thm)], [d35,d74])). % 62.94/8.77 cnf(d76, plain, op(e3,e1) != e2 | e4 = e2 | op(e4,e3) = e2, inference(demodulation, [status(thm)], [d75,d39])). % 62.94/8.77 cnf(d77, plain, op(e4,e3) = e2 | e4 = e2, inference(resolution, [status(thm)], [d64,d76])). % 62.94/8.77 cnf(d78, plain, e1 != op(e2,e1), inference(demodulation, [status(thm)], [c97,d52])). % 62.94/8.77 cnf(d79, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | op(e2,e2) = e1 | e3 = e1 | op(e2,e1) = e1, inference(demodulation, [status(thm)], [c58,c198])). % 62.94/8.77 cnf(d80, plain, op(e2,e2) != e1, inference(demodulation, [status(thm)], [c114,c197])). % 62.94/8.77 cnf(d81, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | op(e2,e1) = e1 | e3 = e1, inference(resolution, [status(thm)], [d80,d79])). % 62.94/8.77 cnf(d82, plain, e2 = e1 | op(e2,e3) = e1 | op(e2,e1) = e1 | e3 = e1, inference(demodulation, [status(thm)], [d81,d28])). % 62.94/8.77 cnf(d83, plain, op(e0,e2) != e1, inference(demodulation, [status(thm)], [c109,c197])). % 62.94/8.77 cnf(d84, plain, e2 != e1, inference(demodulation, [status(thm)], [d83,d21])). % 62.94/8.77 cnf(d85, plain, op(e2,e3) = e1 | op(e2,e1) = e1 | e3 = e1, inference(resolution, [status(thm)], [d84,d82])). % 62.94/8.77 cnf(d86, plain, e1 != e1 | op(e2,e3) = e1 | e3 = e1, inference(superposition, [status(thm)], [d85,d78])). % 62.94/8.77 cnf(d87, plain, op(e2,e3) = e1 | e3 = e1, inference(equality_resolution, [status(thm)], [d86])). % 62.94/8.77 cnf(d88, plain, e4 != op(e4,e1), inference(demodulation, [status(thm)], [c176,d39])). % 62.94/8.77 cnf(d89, plain, e1 != op(e4,e2) | op(e4,e1) = e0 | op(e4,e1) = e3 | op(e4,e1) = e2 | op(e4,e1) = e4, inference(superposition, [status(thm)], [c21,c180])). % 62.94/8.77 cnf(d90, plain, op(e4,e1) = e0 | op(e4,e1) = e3 | op(e4,e1) = e2 | op(e4,e1) = e4 | e1 != e1, inference(demodulation, [status(thm)], [d89,c197])). % 62.94/8.77 cnf(d91, plain, op(e4,e1) != e0, inference(demodulation, [status(thm)], [c182,d42])). % 62.94/8.77 cnf(d92, plain, op(e4,e1) = e3 | op(e4,e1) = e2 | op(e4,e1) = e4 | e1 != e1, inference(resolution, [status(thm)], [d91,d90])). % 62.94/8.77 cnf(d93, plain, op(e4,e1) = e3 | op(e4,e1) = e2 | op(e4,e1) = e4, inference(equality_resolution, [status(thm)], [d92])). % 62.94/8.77 cnf(d94, plain, e4 != e4 | op(e4,e1) = e3 | op(e4,e1) = e2, inference(superposition, [status(thm)], [d93,d88])). % 62.94/8.77 cnf(d95, plain, op(e4,e1) = e3 | op(e4,e1) = e2, inference(equality_resolution, [status(thm)], [d94])). % 62.94/8.77 cnf(d96, plain, op(e3,e1) != e2 | op(e4,e1) = e3, inference(superposition, [status(thm)], [d95,c105])). % 62.94/8.77 cnf(d97, plain, op(e4,e1) = e3, inference(resolution, [status(thm)], [d64,d96])). % 62.94/8.77 cnf(d98, plain, op(e4,e1) != e1, inference(demodulation, [status(thm)], [c180,c197])). % 62.94/8.77 cnf(d99, plain, e3 != e1, inference(demodulation, [status(thm)], [d98,d97])). % 62.94/8.77 cnf(d100, plain, op(e2,e3) = e1, inference(resolution, [status(thm)], [d99,d87])). % 62.94/8.77 cnf(d101, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | e3 = e4 | op(e2,e1) = e4, inference(demodulation, [status(thm)], [c64,c198])). % 62.94/8.77 cnf(d102, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e1) = e4, inference(resolution, [status(thm)], [c195,d101])). % 62.94/8.77 cnf(d103, plain, e2 = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e1) = e4, inference(demodulation, [status(thm)], [d102,d28])). % 62.94/8.77 cnf(d104, plain, op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e1) = e4, inference(resolution, [status(thm)], [c194,d103])). % 62.94/8.77 cnf(d105, plain, op(e2,e3) = e4 | op(e2,e1) = e4, inference(resolution, [status(thm)], [d68,d104])). % 62.94/8.77 cnf(d106, plain, e1 = e4 | op(e2,e1) = e4, inference(demodulation, [status(thm)], [d105,d100])). % 62.94/8.77 cnf(d107, plain, op(e2,e1) = e4, inference(resolution, [status(thm)], [c192,d106])). % 62.94/8.77 cnf(d108, plain, op(e2,e1) != e2, inference(demodulation, [status(thm)], [c103,d64])). % 62.94/8.77 cnf(d109, plain, e4 != e2, inference(demodulation, [status(thm)], [d108,d107])). % 62.94/8.77 cnf(d110, plain, op(e4,e3) = e2, inference(resolution, [status(thm)], [d109,d77])). % 62.94/8.77 cnf(d111, plain, op(e1,e3) != e2, inference(demodulation, [status(thm)], [c122,d110])). % 62.94/8.77 cnf(d112, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | op(e1,e3) = e4, inference(resolution, [status(thm)], [d111,d71])). % 62.94/8.77 cnf(d113, plain, e4 != e4 | op(e3,e2) = e4 | op(e1,e3) = e0 | op(e1,e3) = e3, inference(superposition, [status(thm)], [d112,d69])). % 62.94/8.77 cnf(d114, plain, e4 != e4 | op(e1,e4) = e1 | op(e0,e1) = e4 | op(e3,e1) = e4 | op(e2,e1) = e4 | op(e4,e1) = e4, inference(superposition, [status(thm)], [c55,c208])). % 62.94/8.77 cnf(d115, plain, op(e0,e1) = e4 | op(e3,e1) = e4 | op(e2,e1) = e4 | op(e4,e1) = e4 | op(e1,e4) = e1, inference(equality_resolution, [status(thm)], [d114])). % 62.94/8.77 cnf(d116, plain, op(e1,e0) != e1 | op(e0,e1) = e4 | op(e3,e1) = e4 | op(e2,e1) = e4 | op(e4,e1) = e4, inference(superposition, [status(thm)], [d115,c149])). % 62.94/8.77 cnf(d117, plain, op(e0,e1) = e4 | op(e3,e1) = e4 | op(e2,e1) = e4 | op(e4,e1) = e4, inference(resolution, [status(thm)], [d3,d116])). % 62.94/8.77 cnf(d118, plain, e1 = e4 | op(e3,e1) = e4 | op(e2,e1) = e4 | op(e4,e1) = e4, inference(demodulation, [status(thm)], [d117,d52])). % 62.94/8.77 cnf(d119, plain, e1 = e4 | e2 = e4 | op(e2,e1) = e4 | op(e4,e1) = e4, inference(demodulation, [status(thm)], [d118,d64])). % 62.94/8.77 cnf(d120, plain, e1 = e4 | e2 = e4 | e4 = e4 | op(e4,e1) = e4, inference(demodulation, [status(thm)], [d119,d107])). % 62.94/8.77 cnf(d121, plain, e1 = e4 | e2 = e4 | e4 = e4 | e3 = e4, inference(demodulation, [status(thm)], [d120,d97])). % 62.94/8.77 cnf(d122, plain, e1 = e4 | e4 = e4 | e3 = e4, inference(resolution, [status(thm)], [c194,d121])). % 62.94/8.77 cnf(d123, plain, e4 = e4 | e3 = e4, inference(resolution, [status(thm)], [c192,d122])). % 62.94/8.77 cnf(d124, plain, e4 = e4, inference(resolution, [status(thm)], [c195,d123])). % 62.94/8.77 cnf(d125, plain, op(e3,e2) = e4 | op(e1,e3) = e0 | op(e1,e3) = e3, inference(resolution, [status(thm)], [d124,d113])). % 62.94/8.77 cnf(d126, plain, e3 != e3 | op(e3,e2) = e4 | op(e1,e3) = e0, inference(superposition, [status(thm)], [d125,d20])). % 62.94/8.77 cnf(d127, plain, e3 != e3 | op(e1,e3) = e1 | op(e0,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(superposition, [status(thm)], [c53,c207])). % 62.94/8.77 cnf(d128, plain, op(e0,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3 | op(e1,e3) = e1, inference(equality_resolution, [status(thm)], [d127])). % 62.94/8.77 cnf(d129, plain, op(e1,e0) != e1 | op(e0,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(superposition, [status(thm)], [d128,c148])). % 62.94/8.77 cnf(d130, plain, op(e0,e1) = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(resolution, [status(thm)], [d3,d129])). % 62.94/8.77 cnf(d131, plain, e1 = e3 | op(e3,e1) = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d130,d52])). % 62.94/8.77 cnf(d132, plain, e1 = e3 | e2 = e3 | op(e2,e1) = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d131,d64])). % 62.94/8.77 cnf(d133, plain, e1 = e3 | e2 = e3 | e4 = e3 | op(e4,e1) = e3, inference(demodulation, [status(thm)], [d132,d107])). % 62.94/8.77 cnf(d134, plain, e1 = e3 | e2 = e3 | e4 = e3 | e3 = e3, inference(demodulation, [status(thm)], [d133,d97])). % 62.94/8.77 cnf(d135, plain, e1 = e3 | e4 = e3 | e3 = e3, inference(resolution, [status(thm)], [c193,d134])). % 62.94/8.77 cnf(d136, plain, e4 = e3 | e3 = e3, inference(resolution, [status(thm)], [c191,d135])). % 62.94/8.77 cnf(d137, plain, e3 = e3, inference(resolution, [status(thm)], [d50,d136])). % 62.94/8.77 cnf(d138, plain, op(e3,e2) = e4 | op(e1,e3) = e0, inference(resolution, [status(thm)], [d137,d126])). % 62.94/8.77 cnf(d139, plain, e3 != op(e3,e3), inference(demodulation, [status(thm)], [c118,d19])). % 62.94/8.77 cnf(d140, plain, e1 != e1 | op(e3,e1) = e3 | op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e4, inference(superposition, [status(thm)], [c18,c215])). % 62.94/8.77 cnf(d141, plain, op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e4 | op(e3,e1) = e3, inference(equality_resolution, [status(thm)], [d140])). % 62.94/8.77 cnf(d142, plain, op(e3,e0) != e3 | op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e4, inference(superposition, [status(thm)], [d141,c166])). % 62.94/8.77 cnf(d143, plain, op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e4, inference(resolution, [status(thm)], [d65,d142])). % 62.94/8.77 cnf(d144, plain, op(e3,e3) != e2 | e4 = e2, inference(superposition, [status(thm)], [d77,c125])). % 62.94/8.77 cnf(d145, plain, op(e3,e3) != e2, inference(resolution, [status(thm)], [d109,d144])). % 62.94/8.77 cnf(d146, plain, op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e4, inference(resolution, [status(thm)], [d145,d143])). % 62.94/8.77 cnf(d147, plain, op(e1,e0) != e1 | op(e0,e4) = e1 | op(e3,e4) = e1 | op(e2,e4) = e1 | op(e4,e4) = e1, inference(superposition, [status(thm)], [c79,c149])). % 62.94/8.77 cnf(d148, plain, op(e0,e4) = e1 | op(e3,e4) = e1 | e3 = e1 | op(e4,e4) = e1 | op(e1,e0) != e1, inference(demodulation, [status(thm)], [d147,c198])). % 62.94/8.77 cnf(d149, plain, op(e0,e4) = e1 | op(e3,e4) = e1 | e3 = e1 | op(e4,e4) = e1, inference(resolution, [status(thm)], [d3,d148])). % 62.94/8.77 cnf(d150, plain, e4 = e1 | op(e3,e4) = e1 | op(e4,e4) = e1 | e3 = e1, inference(demodulation, [status(thm)], [d149,d48])). % 62.94/8.77 cnf(d151, plain, e4 = e1 | op(e3,e4) = e1 | e0 = e1 | e3 = e1, inference(demodulation, [status(thm)], [d150,d42])). % 62.94/8.77 cnf(d152, plain, e4 = e1 | op(e3,e4) = e1 | e3 = e1, inference(resolution, [status(thm)], [c186,d151])). % 62.94/8.77 cnf(d153, plain, op(e4,e0) != e1, inference(demodulation, [status(thm)], [c177,c197])). % 62.94/8.77 cnf(d154, plain, e4 != e1, inference(demodulation, [status(thm)], [d153,d39])). % 62.94/8.77 cnf(d155, plain, op(e3,e4) = e1 | e3 = e1, inference(resolution, [status(thm)], [d154,d152])). % 62.94/8.77 cnf(d156, plain, op(e3,e4) = e1, inference(resolution, [status(thm)], [d99,d155])). % 62.94/8.77 cnf(d157, plain, op(e3,e3) != e4 | e1 = e3, inference(demodulation, [status(thm)], [c218,d156])). % 62.94/8.77 cnf(d158, plain, op(e3,e3) != e4, inference(resolution, [status(thm)], [c191,d157])). % 62.94/8.77 cnf(d159, plain, op(e3,e3) = e0 | op(e3,e3) = e3, inference(resolution, [status(thm)], [d158,d146])). % 62.94/8.77 cnf(d160, plain, e3 != e3 | op(e3,e3) = e0, inference(superposition, [status(thm)], [d159,d139])). % 62.94/8.77 cnf(d161, plain, op(e3,e3) = e0, inference(resolution, [status(thm)], [d137,d160])). % 62.94/8.77 cnf(d162, plain, op(e1,e3) != e0, inference(demodulation, [status(thm)], [c121,d161])). % 62.94/8.77 cnf(d163, plain, op(e3,e2) = e4, inference(resolution, [status(thm)], [d162,d138])). % 62.94/8.77 cnf(d164, plain, op(e4,e2) = e3 | ~'Ts6', inference(demodulation, [status(thm)], [c246,d163])). % 62.94/8.77 cnf(d165, plain, e1 = e3 | ~'Ts6', inference(demodulation, [status(thm)], [d164,c197])). % 62.94/8.77 cnf(d166, plain, ~'Ts6', inference(resolution, [status(thm)], [c191,d165])). % 62.94/8.77 cnf(d167, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | op(e4,e4) = e2 | op(e1,e4) = e2, inference(demodulation, [status(thm)], [c81,c198])). % 62.94/8.77 cnf(d168, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | op(e1,e4) = e2 | e3 = e2, inference(resolution, [status(thm)], [d35,d167])). % 62.94/8.77 cnf(d169, plain, e4 = e2 | op(e3,e4) = e2 | op(e1,e4) = e2 | e3 = e2, inference(demodulation, [status(thm)], [d168,d48])). % 62.94/8.77 cnf(d170, plain, op(e3,e4) = e2 | op(e1,e4) = e2 | e4 = e2, inference(resolution, [status(thm)], [d67,d169])). % 62.94/8.77 cnf(d171, plain, e1 = e2 | op(e1,e4) = e2 | e4 = e2, inference(demodulation, [status(thm)], [d170,d156])). % 62.94/8.77 cnf(d172, plain, op(e1,e4) = e2 | e4 = e2, inference(resolution, [status(thm)], [c190,d171])). % 62.94/8.77 cnf(d173, plain, op(e1,e4) = e2, inference(resolution, [status(thm)], [d109,d172])). % 62.94/8.77 cnf(d174, plain, e4 != e4 | op(e1,e4) = e1 | op(e1,e0) = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4, inference(superposition, [status(thm)], [c54,c208])). % 62.94/8.77 cnf(d175, plain, op(e1,e0) = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4 | op(e1,e4) = e1, inference(equality_resolution, [status(thm)], [d174])). % 62.94/8.77 cnf(d176, plain, op(e1,e0) != e1 | op(e1,e0) = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4, inference(superposition, [status(thm)], [d175,c149])). % 62.94/8.77 cnf(d177, plain, op(e1,e0) = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4, inference(resolution, [status(thm)], [d3,d176])). % 62.94/8.77 cnf(d178, plain, e1 = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | op(e1,e4) = e4, inference(demodulation, [status(thm)], [d177,d3])). % 62.94/8.77 cnf(d179, plain, e1 = e4 | op(e1,e3) = e4 | op(e1,e2) = e4 | e2 = e4, inference(demodulation, [status(thm)], [d178,d173])). % 62.94/8.77 cnf(d180, plain, e1 = e4 | op(e1,e3) = e4 | op(e1,e2) = e4, inference(resolution, [status(thm)], [c194,d179])). % 62.94/8.77 cnf(d181, plain, op(e1,e3) = e4 | op(e1,e2) = e4, inference(resolution, [status(thm)], [c192,d180])). % 62.94/8.77 cnf(d182, plain, op(e1,e2) != e4, inference(demodulation, [status(thm)], [c111,d163])). % 62.94/8.77 cnf(d183, plain, op(e1,e3) = e4, inference(resolution, [status(thm)], [d182,d181])). % 62.94/8.77 cnf(d184, plain, ~'Ts11', inference(equality_resolution, [status(thm)], [c260])). % 62.94/8.77 cnf(d185, plain, op(e4,e4) != op(e4,e4) | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(resolution, [status(thm)], [d184,c224])). % 62.94/8.77 cnf(d186, plain, ~'Ts17', inference(equality_resolution, [status(thm)], [c278])). % 62.94/8.77 cnf(d187, plain, op(e4,e4) != op(e4,e4) | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(resolution, [status(thm)], [d186,d185])). % 62.94/8.77 cnf(d188, plain, ~'Ts23', inference(equality_resolution, [status(thm)], [c296])). % 62.94/8.77 cnf(d189, plain, op(e4,e4) != op(e4,e4) | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d188,d187])). % 62.94/8.77 cnf(d190, plain, ~'Ts5', inference(equality_resolution, [status(thm)], [c242])). % 62.94/8.77 cnf(d191, plain, op(e4,e4) != op(e4,e4) | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d190,d189])). % 62.94/8.77 cnf(d192, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(equality_resolution, [status(thm)], [d191])). % 62.94/8.77 cnf(d193, plain, op(e1,e1) != e0 | ~'Ts18', inference(demodulation, [status(thm)], [c283,d3])). % 62.94/8.77 cnf(d194, plain, e0 != e0 | ~'Ts18', inference(demodulation, [status(thm)], [d193,d1])). % 62.94/8.77 cnf(d195, plain, ~'Ts18', inference(equality_resolution, [status(thm)], [d194])). % 62.94/8.77 cnf(d196, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d195,d192])). % 62.94/8.77 cnf(d197, plain, e1 != op(e0,e1) | ~'Ts22', inference(demodulation, [status(thm)], [c293,d3])). % 62.94/8.77 cnf(d198, plain, e1 != e1 | ~'Ts22', inference(demodulation, [status(thm)], [d197,d52])). % 62.94/8.77 cnf(d199, plain, ~'Ts22', inference(equality_resolution, [status(thm)], [d198])). % 62.94/8.77 cnf(d200, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d199,d196])). % 62.94/8.77 cnf(d201, plain, op(e3,e0) != e3 | ~'Ts20', inference(demodulation, [status(thm)], [c289,d19])). % 62.94/8.77 cnf(d202, plain, e3 != e3 | ~'Ts20', inference(demodulation, [status(thm)], [d201,d65])). % 62.94/8.77 cnf(d203, plain, ~'Ts20', inference(equality_resolution, [status(thm)], [d202])). % 62.94/8.77 cnf(d204, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d203,d200])). % 62.94/8.77 cnf(d205, plain, e2 != op(e0,e2) | ~'Ts21', inference(demodulation, [status(thm)], [c290,d28])). % 62.94/8.77 cnf(d206, plain, e2 != e2 | ~'Ts21', inference(demodulation, [status(thm)], [d205,d21])). % 62.94/8.77 cnf(d207, plain, ~'Ts21', inference(equality_resolution, [status(thm)], [d206])). % 62.94/8.77 cnf(d208, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d207,d204])). % 62.94/8.77 cnf(d209, plain, e3 != op(e3,e0) | ~'Ts8', inference(demodulation, [status(thm)], [c251,d19])). % 62.94/8.77 cnf(d210, plain, e3 != e3 | ~'Ts8', inference(demodulation, [status(thm)], [d209,d65])). % 62.94/8.77 cnf(d211, plain, ~'Ts8', inference(equality_resolution, [status(thm)], [d210])). % 62.94/8.77 cnf(d212, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d211,d208])). % 62.94/8.77 cnf(d213, plain, e4 != op(e0,e4) | ~'Ts19', inference(demodulation, [status(thm)], [c284,d39])). % 62.94/8.77 cnf(d214, plain, e4 != e4 | ~'Ts19', inference(demodulation, [status(thm)], [d213,d48])). % 62.94/8.77 cnf(d215, plain, ~'Ts19', inference(equality_resolution, [status(thm)], [d214])). % 62.94/8.77 cnf(d216, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d215,d212])). % 62.94/8.77 cnf(d217, plain, op(e0,e2) != e2 | ~'Ts13', inference(demodulation, [status(thm)], [c266,d28])). % 62.94/8.77 cnf(d218, plain, e2 != e2 | ~'Ts13', inference(demodulation, [status(thm)], [d217,d21])). % 62.94/8.77 cnf(d219, plain, ~'Ts13', inference(equality_resolution, [status(thm)], [d218])). % 62.94/8.77 cnf(d220, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d219,d216])). % 62.94/8.77 cnf(d221, plain, op(e0,e4) != e4 | ~'Ts3', inference(demodulation, [status(thm)], [c236,d39])). % 62.94/8.77 cnf(d222, plain, e4 != e4 | ~'Ts3', inference(demodulation, [status(thm)], [d221,d48])). % 62.94/8.77 cnf(d223, plain, ~'Ts3', inference(equality_resolution, [status(thm)], [d222])). % 62.94/8.77 cnf(d224, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d223,d220])). % 62.94/8.77 cnf(d225, plain, op(e3,e4) = e2 | ~'Ts9', inference(demodulation, [status(thm)], [c255,c198])). % 62.94/8.77 cnf(d226, plain, e1 = e2 | ~'Ts9', inference(demodulation, [status(thm)], [d225,d156])). % 62.94/8.77 cnf(d227, plain, ~'Ts9', inference(resolution, [status(thm)], [c190,d226])). % 62.94/8.77 cnf(d228, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts7' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d227,d224])). % 62.94/8.77 cnf(d229, plain, op(e2,e1) = e3 | ~'Ts7', inference(demodulation, [status(thm)], [c249,d64])). % 62.94/8.77 cnf(d230, plain, op(e2,e1) != e3, inference(demodulation, [status(thm)], [c162,c198])). % 62.94/8.77 cnf(d231, plain, ~'Ts7', inference(resolution, [status(thm)], [d230,d229])). % 62.94/8.77 cnf(d232, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d231,d228])). % 62.94/8.77 cnf(d233, plain, op(e3,e4) != e1 | ~'Ts2', inference(demodulation, [status(thm)], [c235,d97])). % 62.94/8.77 cnf(d234, plain, e1 != e1 | ~'Ts2', inference(demodulation, [status(thm)], [d233,d156])). % 62.94/8.77 cnf(d235, plain, ~'Ts2', inference(equality_resolution, [status(thm)], [d234])). % 62.94/8.77 cnf(d236, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d235,d232])). % 62.94/8.77 cnf(d237, plain, op(e4,e2) != e1 | ~'Ts12' | op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e4) = e4, inference(superposition, [status(thm)], [c64,c265])). % 62.94/8.77 cnf(d238, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e4) = e4 | e1 != e1 | ~'Ts12', inference(demodulation, [status(thm)], [d237,c197])). % 62.94/8.77 cnf(d239, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | e3 = e4 | e1 != e1 | ~'Ts12', inference(demodulation, [status(thm)], [d238,c198])). % 62.94/8.77 cnf(d240, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | e1 != e1 | ~'Ts12', inference(resolution, [status(thm)], [c195,d239])). % 62.94/8.77 cnf(d241, plain, op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | ~'Ts12', inference(equality_resolution, [status(thm)], [d240])). % 62.94/8.77 cnf(d242, plain, e2 = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | ~'Ts12', inference(demodulation, [status(thm)], [d241,d28])). % 62.94/8.77 cnf(d243, plain, op(e2,e3) = e4 | op(e2,e2) = e4 | ~'Ts12', inference(resolution, [status(thm)], [c194,d242])). % 62.94/8.77 cnf(d244, plain, op(e2,e3) = e4 | ~'Ts12', inference(resolution, [status(thm)], [d68,d243])). % 62.94/8.77 cnf(d245, plain, e1 = e4 | ~'Ts12', inference(demodulation, [status(thm)], [d244,d100])). % 62.94/8.77 cnf(d246, plain, ~'Ts12', inference(resolution, [status(thm)], [c192,d245])). % 62.94/8.77 cnf(d247, plain, 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts16' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d246,d236])). % 62.94/8.77 cnf(d248, plain, op(e1,e4) = e3 | ~'Ts4', inference(demodulation, [status(thm)], [c240,d156])). % 62.94/8.77 cnf(d249, plain, op(e1,e4) != e3, inference(demodulation, [status(thm)], [c130,c198])). % 62.94/8.77 cnf(d250, plain, ~'Ts4', inference(resolution, [status(thm)], [d249,d248])). % 62.94/8.77 cnf(d251, plain, 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts16' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d250,d247])). % 62.94/8.77 cnf(d252, plain, op(e2,e4) != e3 | ~'Ts0' | e4 = e2, inference(superposition, [status(thm)], [d77,c229])). % 62.94/8.77 cnf(d253, plain, e3 != e3 | e4 = e2 | ~'Ts0', inference(demodulation, [status(thm)], [d252,c198])). % 62.94/8.77 cnf(d254, plain, e4 = e2 | ~'Ts0', inference(equality_resolution, [status(thm)], [d253])). % 62.94/8.77 cnf(d255, plain, ~'Ts0', inference(resolution, [status(thm)], [d109,d254])). % 62.94/8.77 cnf(d256, plain, 'Ts6' | 'Ts1' | 'Ts14' | 'Ts16' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d255,d251])). % 62.94/8.77 cnf(d257, plain, op(e1,e4) != e2 | ~'Ts1' | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e4, inference(superposition, [status(thm)], [c22,c232])). % 62.94/8.77 cnf(d258, plain, e2 != e2 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e4 | ~'Ts1' | op(e0,e4) = e2 | op(e3,e4) = e2 | op(e2,e4) = e2 | op(e4,e4) = e2, inference(superposition, [status(thm)], [c81,d257])). % 62.94/8.77 cnf(d259, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e4 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(demodulation, [status(thm)], [d258,c198])). % 62.94/8.77 cnf(d260, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e4 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(demodulation, [status(thm)], [d259,c197])). % 62.94/8.77 cnf(d261, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | e1 = e3 | op(e4,e2) = e2 | op(e4,e2) = e4 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(demodulation, [status(thm)], [d260,c197])). % 62.94/8.77 cnf(d262, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | e1 = e3 | e1 = e2 | op(e4,e2) = e4 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(demodulation, [status(thm)], [d261,c197])). % 62.94/8.77 cnf(d263, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | e1 = e3 | e1 = e2 | e1 = e4 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(demodulation, [status(thm)], [d262,c197])). % 62.94/8.77 cnf(d264, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | e1 = e3 | e1 = e2 | op(e4,e4) = e2 | e2 != e2 | ~'Ts1', inference(resolution, [status(thm)], [c192,d263])). % 62.94/8.77 cnf(d265, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | op(e4,e4) = e2 | e3 = e2 | e2 != e2 | e1 = e0 | e1 = e2 | ~'Ts1', inference(resolution, [status(thm)], [c191,d264])). % 62.94/8.77 cnf(d266, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | op(e4,e4) = e2 | e3 = e2 | e2 != e2 | e1 = e0 | ~'Ts1', inference(resolution, [status(thm)], [c190,d265])). % 62.94/8.77 cnf(d267, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e2 != e2 | e1 = e0 | ~'Ts1', inference(resolution, [status(thm)], [d35,d266])). % 62.94/8.77 cnf(d268, plain, op(e0,e4) = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | ~'Ts1', inference(equality_resolution, [status(thm)], [d267])). % 62.94/8.77 cnf(d269, plain, e4 = e2 | op(e3,e4) = e2 | e3 = e2 | e1 = e0 | ~'Ts1', inference(demodulation, [status(thm)], [d268,d48])). % 62.94/8.77 cnf(d270, plain, e1 != op(e4,e4), inference(demodulation, [status(thm)], [c184,c197])). % 62.94/8.77 cnf(d271, plain, e1 != e0, inference(demodulation, [status(thm)], [d270,d42])). % 62.94/8.77 cnf(d272, plain, op(e3,e4) = e2 | e3 = e2 | e4 = e2 | ~'Ts1', inference(resolution, [status(thm)], [d271,d269])). % 62.94/8.77 cnf(d273, plain, op(e3,e4) = e2 | e4 = e2 | ~'Ts1', inference(resolution, [status(thm)], [d67,d272])). % 62.94/8.77 cnf(d274, plain, e1 = e2 | e4 = e2 | ~'Ts1', inference(demodulation, [status(thm)], [d273,d156])). % 62.94/8.77 cnf(d275, plain, e4 = e2 | ~'Ts1', inference(resolution, [status(thm)], [c190,d274])). % 62.94/8.77 cnf(d276, plain, ~'Ts1', inference(resolution, [status(thm)], [d109,d275])). % 62.94/8.77 cnf(d277, plain, 'Ts6' | 'Ts14' | 'Ts16' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d276,d256])). % 62.94/8.77 cnf(d278, plain, op(e1,e3) = e2 | ~'Ts10', inference(demodulation, [status(thm)], [c258,d100])). % 62.94/8.77 cnf(d279, plain, ~'Ts10', inference(resolution, [status(thm)], [d111,d278])). % 62.94/8.77 cnf(d280, plain, 'Ts6' | 'Ts14' | 'Ts16' | 'Ts15', inference(resolution, [status(thm)], [d279,d277])). % 62.94/8.77 cnf(d281, plain, e2 != e2 | op(e1,e2) = e1 | op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(superposition, [status(thm)], [c50,c206])). % 62.94/8.77 cnf(d282, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e2) = e1 | op(e1,e4) = e2, inference(equality_resolution, [status(thm)], [d281])). % 62.94/8.77 cnf(d283, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(resolution, [status(thm)], [d55,d282])). % 62.94/8.77 cnf(d284, plain, e1 = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(demodulation, [status(thm)], [d283,d3])). % 62.94/8.77 cnf(d285, plain, op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2, inference(resolution, [status(thm)], [c190,d284])). % 62.94/8.77 cnf(d286, plain, op(e2,e1) != e4 | ~'Ts14' | op(e1,e3) = e2 | op(e1,e2) = e2, inference(superposition, [status(thm)], [d285,c271])). % 62.94/8.77 cnf(d287, plain, op(e1,e3) = e2 | op(e1,e2) = e2 | ~'Ts14', inference(resolution, [status(thm)], [d107,d286])). % 62.94/8.77 cnf(d288, plain, op(e1,e2) = e2 | ~'Ts14', inference(resolution, [status(thm)], [d111,d287])). % 62.94/8.77 cnf(d289, plain, op(e1,e2) != e2, inference(demodulation, [status(thm)], [c154,d173])). % 62.94/8.77 cnf(d290, plain, ~'Ts14', inference(resolution, [status(thm)], [d289,d288])). % 62.94/8.77 cnf(d291, plain, 'Ts6' | 'Ts16' | 'Ts15', inference(resolution, [status(thm)], [d290,d280])). % 62.94/8.77 cnf(d292, plain, op(e4,e1) != e3 | ~'Ts15' | op(e1,e3) = e0 | op(e1,e3) = e3, inference(superposition, [status(thm)], [d112,c274])). % 62.94/8.77 cnf(d293, plain, e3 != e3 | op(e1,e3) = e0 | op(e1,e3) = e3 | ~'Ts15', inference(demodulation, [status(thm)], [d292,d97])). % 62.94/8.77 cnf(d294, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | ~'Ts15', inference(resolution, [status(thm)], [d137,d293])). % 62.94/8.77 cnf(d295, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | 'Ts6' | 'Ts16', inference(resolution, [status(thm)], [d294,d291])). % 62.94/8.77 cnf(d296, plain, e1 != op(e4,e2) | op(e1,e2) = e0 | op(e1,e2) = e3 | op(e1,e2) = e2 | op(e1,e2) = e4, inference(superposition, [status(thm)], [c7,c112])). % 62.94/8.77 cnf(d297, plain, op(e1,e2) = e0 | op(e1,e2) = e3 | op(e1,e2) = e2 | op(e1,e2) = e4 | e1 != e1, inference(demodulation, [status(thm)], [d296,c197])). % 62.94/8.77 cnf(d298, plain, op(e1,e2) = e0 | op(e1,e2) = e3 | op(e1,e2) = e4 | e1 != e1, inference(resolution, [status(thm)], [d289,d297])). % 62.94/8.77 cnf(d299, plain, op(e1,e2) = e0 | op(e1,e2) = e3 | op(e1,e2) = e4, inference(equality_resolution, [status(thm)], [d298])). % 62.94/8.77 cnf(d300, plain, e4 != op(e1,e3) | op(e1,e2) = e0 | op(e1,e2) = e3, inference(superposition, [status(thm)], [d299,c153])). % 62.94/8.77 cnf(d301, plain, e2 != op(e2,e2), inference(demodulation, [status(thm)], [c157,d28])). % 62.94/8.77 cnf(d302, plain, e1 != e1 | op(e2,e1) = e2 | op(e2,e2) = e0 | op(e2,e2) = e3 | op(e2,e2) = e2 | op(e2,e2) = e4, inference(superposition, [status(thm)], [c12,c210])). % 62.94/8.77 cnf(d303, plain, op(e2,e2) = e0 | op(e2,e2) = e3 | op(e2,e2) = e2 | op(e2,e2) = e4 | op(e2,e1) = e2, inference(equality_resolution, [status(thm)], [d302])). % 62.94/8.77 cnf(d304, plain, e2 != op(e3,e1) | op(e2,e2) = e0 | op(e2,e2) = e3 | op(e2,e2) = e2 | op(e2,e2) = e4, inference(superposition, [status(thm)], [d303,c103])). % 62.94/8.77 cnf(d305, plain, op(e2,e2) != e3, inference(demodulation, [status(thm)], [c164,c198])). % 62.94/8.77 cnf(d306, plain, op(e2,e2) = e0 | op(e2,e2) = e2 | op(e2,e2) = e4 | e2 != op(e3,e1), inference(resolution, [status(thm)], [d305,d304])). % 62.94/8.77 cnf(d307, plain, op(e2,e2) = e0 | op(e2,e2) = e2 | op(e2,e2) = e4 | e2 != e2, inference(demodulation, [status(thm)], [d306,d64])). % 62.94/8.77 cnf(d308, plain, op(e2,e2) = e0 | op(e2,e2) = e2 | e2 != e2, inference(resolution, [status(thm)], [d68,d307])). % 62.94/8.77 cnf(d309, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | e1 = e2 | op(e4,e4) = e2 | op(e4,e1) = e2, inference(demodulation, [status(thm)], [c80,c197])). % 62.94/8.77 cnf(d310, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e1) = e2 | e1 = e2, inference(resolution, [status(thm)], [d35,d309])). % 62.94/8.77 cnf(d311, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c190,d310])). % 62.94/8.77 cnf(d312, plain, e4 = e2 | op(e4,e3) = e2 | op(e4,e1) = e2, inference(demodulation, [status(thm)], [d311,d39])). % 62.94/8.77 cnf(d313, plain, op(e4,e3) = e2 | e3 = e2 | e4 = e2, inference(demodulation, [status(thm)], [d312,d97])). % 62.94/8.77 cnf(d314, plain, e2 = e2 | e3 = e2 | e4 = e2, inference(demodulation, [status(thm)], [d313,d110])). % 62.94/8.77 cnf(d315, plain, e2 = e2 | e3 = e2, inference(resolution, [status(thm)], [d109,d314])). % 62.94/8.77 cnf(d316, plain, e2 = e2, inference(resolution, [status(thm)], [d67,d315])). % 62.94/8.77 cnf(d317, plain, op(e2,e2) = e0 | op(e2,e2) = e2, inference(resolution, [status(thm)], [d316,d308])). % 62.94/8.77 cnf(d318, plain, e2 != e2 | op(e2,e2) = e0, inference(superposition, [status(thm)], [d317,d301])). % 62.94/8.77 cnf(d319, plain, op(e2,e2) = e0, inference(resolution, [status(thm)], [d316,d318])). % 62.94/8.77 cnf(d320, plain, op(e1,e2) != e0, inference(demodulation, [status(thm)], [c110,d319])). % 62.94/8.77 cnf(d321, plain, op(e1,e2) = e3 | e4 != op(e1,e3), inference(resolution, [status(thm)], [d320,d300])). % 62.94/8.77 cnf(d322, plain, e4 != e4 | op(e1,e2) = e3 | op(e1,e3) = e0 | op(e1,e3) = e3, inference(superposition, [status(thm)], [d112,d321])). % 62.94/8.77 cnf(d323, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | op(e1,e2) = e3, inference(resolution, [status(thm)], [d124,d322])). % 62.94/8.77 cnf(d324, plain, op(e3,e1) != e2 | ~'Ts16' | op(e1,e3) = e0 | op(e1,e3) = e3, inference(superposition, [status(thm)], [d323,c277])). % 62.94/8.77 cnf(d325, plain, e2 != e2 | op(e1,e3) = e0 | op(e1,e3) = e3 | ~'Ts16', inference(demodulation, [status(thm)], [d324,d64])). % 62.94/8.77 cnf(d326, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | ~'Ts16', inference(resolution, [status(thm)], [d316,d325])). % 62.94/8.77 cnf(d327, plain, op(e1,e3) = e0 | op(e1,e3) = e3 | op(e1,e3) = e0 | op(e1,e3) = e3 | 'Ts6', inference(resolution, [status(thm)], [d326,d295])). % 62.94/8.77 cnf(d328, plain, op(e1,e3) = e3 | 'Ts6', inference(resolution, [status(thm)], [d162,d327])). % 62.94/8.77 cnf(d329, plain, e4 = e3 | 'Ts6', inference(demodulation, [status(thm)], [d328,d183])). % 62.94/8.77 cnf(d330, plain, 'Ts6', inference(resolution, [status(thm)], [d50,d329])). % 62.94/8.77 cnf(d331, plain, $false, inference(resolution, [status(thm)], [d330,d166])). % 62.94/8.77 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------