%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG058+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:20 AM UTC 2026 % Result : Theorem 83.19s 12.84s % Output : CNFRefutation 83.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : ALG058+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/0.36 % Computer : n011.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 21:04:29 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 83.19/12.84 % SZS status Theorem for theBenchmark.p % 83.19/12.84 % SZS output start CNFRefutation for theBenchmark.p % 83.19/12.84 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))))))))))))))))))))))))))))). % 83.19/12.84 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))))))))))))))). % 83.19/12.84 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)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 83.19/12.84 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 83.19/12.84 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 83.19/12.84 fof(ax6, axiom, (e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)) & (e1 = op(op(e2,e2),e2) & (e3 = op(e2,e2) & e4 = op(op(e2,e2),op(e2,e2)))))). % 83.19/12.84 fof(co1, conjecture, ~(((((op(e0,e0) != e0 | (op(e0,e0) = e0 & e0 != unit)) & ((op(e0,e1) != e0 | (op(e0,e0) = e1 & e0 != unit)) & ((op(e0,e2) != e0 | (op(e0,e0) = e2 & e0 != unit)) & ((op(e0,e3) != e0 | (op(e0,e0) = e3 & e0 != unit)) & ((op(e0,e4) != e0 | (op(e0,e0) = e4 & e0 != unit)) & ((op(e1,e0) != e0 | (op(e1,e0) = e0 & e0 != unit)) & ((op(e1,e1) != e0 | (op(e1,e0) = e1 & e0 != unit)) & ((op(e1,e2) != e0 | (op(e1,e0) = e2 & e0 != unit)) & ((op(e1,e3) != e0 | (op(e1,e0) = e3 & e0 != unit)) & ((op(e1,e4) != e0 | (op(e1,e0) = e4 & e0 != unit)) & ((op(e2,e0) != e0 | (op(e2,e0) = e0 & e0 != unit)) & ((op(e2,e1) != e0 | (op(e2,e0) = e1 & e0 != unit)) & ((op(e2,e2) != e0 | (op(e2,e0) = e2 & e0 != unit)) & ((op(e2,e3) != e0 | (op(e2,e0) = e3 & e0 != unit)) & ((op(e2,e4) != e0 | (op(e2,e0) = e4 & e0 != unit)) & ((op(e3,e0) != e0 | (op(e3,e0) = e0 & e0 != unit)) & ((op(e3,e1) != e0 | (op(e3,e0) = e1 & e0 != unit)) & ((op(e3,e2) != e0 | (op(e3,e0) = e2 & e0 != unit)) & ((op(e3,e3) != e0 | (op(e3,e0) = e3 & e0 != unit)) & ((op(e3,e4) != e0 | (op(e3,e0) = e4 & e0 != unit)) & ((op(e4,e0) != e0 | (op(e4,e0) = e0 & e0 != unit)) & ((op(e4,e1) != e0 | (op(e4,e0) = e1 & e0 != unit)) & ((op(e4,e2) != e0 | (op(e4,e0) = e2 & e0 != unit)) & ((op(e4,e3) != e0 | (op(e4,e0) = e3 & e0 != unit)) & (op(e4,e4) != e0 | (op(e4,e0) = e4 & e0 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e1 | (op(e0,e1) = e0 & e1 != unit)) & ((op(e0,e1) != e1 | (op(e0,e1) = e1 & e1 != unit)) & ((op(e0,e2) != e1 | (op(e0,e1) = e2 & e1 != unit)) & ((op(e0,e3) != e1 | (op(e0,e1) = e3 & e1 != unit)) & ((op(e0,e4) != e1 | (op(e0,e1) = e4 & e1 != unit)) & ((op(e1,e0) != e1 | (op(e1,e1) = e0 & e1 != unit)) & ((op(e1,e1) != e1 | (op(e1,e1) = e1 & e1 != unit)) & ((op(e1,e2) != e1 | (op(e1,e1) = e2 & e1 != unit)) & ((op(e1,e3) != e1 | (op(e1,e1) = e3 & e1 != unit)) & ((op(e1,e4) != e1 | (op(e1,e1) = e4 & e1 != unit)) & ((op(e2,e0) != e1 | (op(e2,e1) = e0 & e1 != unit)) & ((op(e2,e1) != e1 | (op(e2,e1) = e1 & e1 != unit)) & ((op(e2,e2) != e1 | (op(e2,e1) = e2 & e1 != unit)) & ((op(e2,e3) != e1 | (op(e2,e1) = e3 & e1 != unit)) & ((op(e2,e4) != e1 | (op(e2,e1) = e4 & e1 != unit)) & ((op(e3,e0) != e1 | (op(e3,e1) = e0 & e1 != unit)) & ((op(e3,e1) != e1 | (op(e3,e1) = e1 & e1 != unit)) & ((op(e3,e2) != e1 | (op(e3,e1) = e2 & e1 != unit)) & ((op(e3,e3) != e1 | (op(e3,e1) = e3 & e1 != unit)) & ((op(e3,e4) != e1 | (op(e3,e1) = e4 & e1 != unit)) & ((op(e4,e0) != e1 | (op(e4,e1) = e0 & e1 != unit)) & ((op(e4,e1) != e1 | (op(e4,e1) = e1 & e1 != unit)) & ((op(e4,e2) != e1 | (op(e4,e1) = e2 & e1 != unit)) & ((op(e4,e3) != e1 | (op(e4,e1) = e3 & e1 != unit)) & (op(e4,e4) != e1 | (op(e4,e1) = e4 & e1 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e2 | (op(e0,e2) = e0 & e2 != unit)) & ((op(e0,e1) != e2 | (op(e0,e2) = e1 & e2 != unit)) & ((op(e0,e2) != e2 | (op(e0,e2) = e2 & e2 != unit)) & ((op(e0,e3) != e2 | (op(e0,e2) = e3 & e2 != unit)) & ((op(e0,e4) != e2 | (op(e0,e2) = e4 & e2 != unit)) & ((op(e1,e0) != e2 | (op(e1,e2) = e0 & e2 != unit)) & ((op(e1,e1) != e2 | (op(e1,e2) = e1 & e2 != unit)) & ((op(e1,e2) != e2 | (op(e1,e2) = e2 & e2 != unit)) & ((op(e1,e3) != e2 | (op(e1,e2) = e3 & e2 != unit)) & ((op(e1,e4) != e2 | (op(e1,e2) = e4 & e2 != unit)) & ((op(e2,e0) != e2 | (op(e2,e2) = e0 & e2 != unit)) & ((op(e2,e1) != e2 | (op(e2,e2) = e1 & e2 != unit)) & ((op(e2,e2) != e2 | (op(e2,e2) = e2 & e2 != unit)) & ((op(e2,e3) != e2 | (op(e2,e2) = e3 & e2 != unit)) & ((op(e2,e4) != e2 | (op(e2,e2) = e4 & e2 != unit)) & ((op(e3,e0) != e2 | (op(e3,e2) = e0 & e2 != unit)) & ((op(e3,e1) != e2 | (op(e3,e2) = e1 & e2 != unit)) & ((op(e3,e2) != e2 | (op(e3,e2) = e2 & e2 != unit)) & ((op(e3,e3) != e2 | (op(e3,e2) = e3 & e2 != unit)) & ((op(e3,e4) != e2 | (op(e3,e2) = e4 & e2 != unit)) & ((op(e4,e0) != e2 | (op(e4,e2) = e0 & e2 != unit)) & ((op(e4,e1) != e2 | (op(e4,e2) = e1 & e2 != unit)) & ((op(e4,e2) != e2 | (op(e4,e2) = e2 & e2 != unit)) & ((op(e4,e3) != e2 | (op(e4,e2) = e3 & e2 != unit)) & (op(e4,e4) != e2 | (op(e4,e2) = e4 & e2 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e3 | (op(e0,e3) = e0 & e3 != unit)) & ((op(e0,e1) != e3 | (op(e0,e3) = e1 & e3 != unit)) & ((op(e0,e2) != e3 | (op(e0,e3) = e2 & e3 != unit)) & ((op(e0,e3) != e3 | (op(e0,e3) = e3 & e3 != unit)) & ((op(e0,e4) != e3 | (op(e0,e3) = e4 & e3 != unit)) & ((op(e1,e0) != e3 | (op(e1,e3) = e0 & e3 != unit)) & ((op(e1,e1) != e3 | (op(e1,e3) = e1 & e3 != unit)) & ((op(e1,e2) != e3 | (op(e1,e3) = e2 & e3 != unit)) & ((op(e1,e3) != e3 | (op(e1,e3) = e3 & e3 != unit)) & ((op(e1,e4) != e3 | (op(e1,e3) = e4 & e3 != unit)) & ((op(e2,e0) != e3 | (op(e2,e3) = e0 & e3 != unit)) & ((op(e2,e1) != e3 | (op(e2,e3) = e1 & e3 != unit)) & ((op(e2,e2) != e3 | (op(e2,e3) = e2 & e3 != unit)) & ((op(e2,e3) != e3 | (op(e2,e3) = e3 & e3 != unit)) & ((op(e2,e4) != e3 | (op(e2,e3) = e4 & e3 != unit)) & ((op(e3,e0) != e3 | (op(e3,e3) = e0 & e3 != unit)) & ((op(e3,e1) != e3 | (op(e3,e3) = e1 & e3 != unit)) & ((op(e3,e2) != e3 | (op(e3,e3) = e2 & e3 != unit)) & ((op(e3,e3) != e3 | (op(e3,e3) = e3 & e3 != unit)) & ((op(e3,e4) != e3 | (op(e3,e3) = e4 & e3 != unit)) & ((op(e4,e0) != e3 | (op(e4,e3) = e0 & e3 != unit)) & ((op(e4,e1) != e3 | (op(e4,e3) = e1 & e3 != unit)) & ((op(e4,e2) != e3 | (op(e4,e3) = e2 & e3 != unit)) & ((op(e4,e3) != e3 | (op(e4,e3) = e3 & e3 != unit)) & (op(e4,e4) != e3 | (op(e4,e3) = e4 & e3 != unit)))))))))))))))))))))))))) | ((op(e0,e0) != e4 | (op(e0,e4) = e0 & e4 != unit)) & ((op(e0,e1) != e4 | (op(e0,e4) = e1 & e4 != unit)) & ((op(e0,e2) != e4 | (op(e0,e4) = e2 & e4 != unit)) & ((op(e0,e3) != e4 | (op(e0,e4) = e3 & e4 != unit)) & ((op(e0,e4) != e4 | (op(e0,e4) = e4 & e4 != unit)) & ((op(e1,e0) != e4 | (op(e1,e4) = e0 & e4 != unit)) & ((op(e1,e1) != e4 | (op(e1,e4) = e1 & e4 != unit)) & ((op(e1,e2) != e4 | (op(e1,e4) = e2 & e4 != unit)) & ((op(e1,e3) != e4 | (op(e1,e4) = e3 & e4 != unit)) & ((op(e1,e4) != e4 | (op(e1,e4) = e4 & e4 != unit)) & ((op(e2,e0) != e4 | (op(e2,e4) = e0 & e4 != unit)) & ((op(e2,e1) != e4 | (op(e2,e4) = e1 & e4 != unit)) & ((op(e2,e2) != e4 | (op(e2,e4) = e2 & e4 != unit)) & ((op(e2,e3) != e4 | (op(e2,e4) = e3 & e4 != unit)) & ((op(e2,e4) != e4 | (op(e2,e4) = e4 & e4 != unit)) & ((op(e3,e0) != e4 | (op(e3,e4) = e0 & e4 != unit)) & ((op(e3,e1) != e4 | (op(e3,e4) = e1 & e4 != unit)) & ((op(e3,e2) != e4 | (op(e3,e4) = e2 & e4 != unit)) & ((op(e3,e3) != e4 | (op(e3,e4) = e3 & e4 != unit)) & ((op(e3,e4) != e4 | (op(e3,e4) = e4 & e4 != unit)) & ((op(e4,e0) != e4 | (op(e4,e4) = e0 & e4 != unit)) & ((op(e4,e1) != e4 | (op(e4,e4) = e1 & e4 != unit)) & ((op(e4,e2) != e4 | (op(e4,e4) = e2 & e4 != unit)) & ((op(e4,e3) != e4 | (op(e4,e4) = e3 & e4 != unit)) & (op(e4,e4) != e4 | (op(e4,e4) = e4 & e4 != unit)))))))))))))))))))))))))))))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4))))))))))))))))))))))))))))). % 83.19/12.84 fof(negated_conjecture, negated_conjecture, ~~(((((op(e0,e0) != e0 | (op(e0,e0) = e0 & e0 != unit)) & ((op(e0,e1) != e0 | (op(e0,e0) = e1 & e0 != unit)) & ((op(e0,e2) != e0 | (op(e0,e0) = e2 & e0 != unit)) & ((op(e0,e3) != e0 | (op(e0,e0) = e3 & e0 != unit)) & ((op(e0,e4) != e0 | (op(e0,e0) = e4 & e0 != unit)) & ((op(e1,e0) != e0 | (op(e1,e0) = e0 & e0 != unit)) & ((op(e1,e1) != e0 | (op(e1,e0) = e1 & e0 != unit)) & ((op(e1,e2) != e0 | (op(e1,e0) = e2 & e0 != unit)) & ((op(e1,e3) != e0 | (op(e1,e0) = e3 & e0 != unit)) & ((op(e1,e4) != e0 | (op(e1,e0) = e4 & e0 != unit)) & ((op(e2,e0) != e0 | (op(e2,e0) = e0 & e0 != unit)) & ((op(e2,e1) != e0 | (op(e2,e0) = e1 & e0 != unit)) & ((op(e2,e2) != e0 | (op(e2,e0) = e2 & e0 != unit)) & ((op(e2,e3) != e0 | (op(e2,e0) = e3 & e0 != unit)) & ((op(e2,e4) != e0 | (op(e2,e0) = e4 & e0 != unit)) & ((op(e3,e0) != e0 | (op(e3,e0) = e0 & e0 != unit)) & ((op(e3,e1) != e0 | (op(e3,e0) = e1 & e0 != unit)) & ((op(e3,e2) != e0 | (op(e3,e0) = e2 & e0 != unit)) & ((op(e3,e3) != e0 | (op(e3,e0) = e3 & e0 != unit)) & ((op(e3,e4) != e0 | (op(e3,e0) = e4 & e0 != unit)) & ((op(e4,e0) != e0 | (op(e4,e0) = e0 & e0 != unit)) & ((op(e4,e1) != e0 | (op(e4,e0) = e1 & e0 != unit)) & ((op(e4,e2) != e0 | (op(e4,e0) = e2 & e0 != unit)) & ((op(e4,e3) != e0 | (op(e4,e0) = e3 & e0 != unit)) & (op(e4,e4) != e0 | (op(e4,e0) = e4 & e0 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e1 | (op(e0,e1) = e0 & e1 != unit)) & ((op(e0,e1) != e1 | (op(e0,e1) = e1 & e1 != unit)) & ((op(e0,e2) != e1 | (op(e0,e1) = e2 & e1 != unit)) & ((op(e0,e3) != e1 | (op(e0,e1) = e3 & e1 != unit)) & ((op(e0,e4) != e1 | (op(e0,e1) = e4 & e1 != unit)) & ((op(e1,e0) != e1 | (op(e1,e1) = e0 & e1 != unit)) & ((op(e1,e1) != e1 | (op(e1,e1) = e1 & e1 != unit)) & ((op(e1,e2) != e1 | (op(e1,e1) = e2 & e1 != unit)) & ((op(e1,e3) != e1 | (op(e1,e1) = e3 & e1 != unit)) & ((op(e1,e4) != e1 | (op(e1,e1) = e4 & e1 != unit)) & ((op(e2,e0) != e1 | (op(e2,e1) = e0 & e1 != unit)) & ((op(e2,e1) != e1 | (op(e2,e1) = e1 & e1 != unit)) & ((op(e2,e2) != e1 | (op(e2,e1) = e2 & e1 != unit)) & ((op(e2,e3) != e1 | (op(e2,e1) = e3 & e1 != unit)) & ((op(e2,e4) != e1 | (op(e2,e1) = e4 & e1 != unit)) & ((op(e3,e0) != e1 | (op(e3,e1) = e0 & e1 != unit)) & ((op(e3,e1) != e1 | (op(e3,e1) = e1 & e1 != unit)) & ((op(e3,e2) != e1 | (op(e3,e1) = e2 & e1 != unit)) & ((op(e3,e3) != e1 | (op(e3,e1) = e3 & e1 != unit)) & ((op(e3,e4) != e1 | (op(e3,e1) = e4 & e1 != unit)) & ((op(e4,e0) != e1 | (op(e4,e1) = e0 & e1 != unit)) & ((op(e4,e1) != e1 | (op(e4,e1) = e1 & e1 != unit)) & ((op(e4,e2) != e1 | (op(e4,e1) = e2 & e1 != unit)) & ((op(e4,e3) != e1 | (op(e4,e1) = e3 & e1 != unit)) & (op(e4,e4) != e1 | (op(e4,e1) = e4 & e1 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e2 | (op(e0,e2) = e0 & e2 != unit)) & ((op(e0,e1) != e2 | (op(e0,e2) = e1 & e2 != unit)) & ((op(e0,e2) != e2 | (op(e0,e2) = e2 & e2 != unit)) & ((op(e0,e3) != e2 | (op(e0,e2) = e3 & e2 != unit)) & ((op(e0,e4) != e2 | (op(e0,e2) = e4 & e2 != unit)) & ((op(e1,e0) != e2 | (op(e1,e2) = e0 & e2 != unit)) & ((op(e1,e1) != e2 | (op(e1,e2) = e1 & e2 != unit)) & ((op(e1,e2) != e2 | (op(e1,e2) = e2 & e2 != unit)) & ((op(e1,e3) != e2 | (op(e1,e2) = e3 & e2 != unit)) & ((op(e1,e4) != e2 | (op(e1,e2) = e4 & e2 != unit)) & ((op(e2,e0) != e2 | (op(e2,e2) = e0 & e2 != unit)) & ((op(e2,e1) != e2 | (op(e2,e2) = e1 & e2 != unit)) & ((op(e2,e2) != e2 | (op(e2,e2) = e2 & e2 != unit)) & ((op(e2,e3) != e2 | (op(e2,e2) = e3 & e2 != unit)) & ((op(e2,e4) != e2 | (op(e2,e2) = e4 & e2 != unit)) & ((op(e3,e0) != e2 | (op(e3,e2) = e0 & e2 != unit)) & ((op(e3,e1) != e2 | (op(e3,e2) = e1 & e2 != unit)) & ((op(e3,e2) != e2 | (op(e3,e2) = e2 & e2 != unit)) & ((op(e3,e3) != e2 | (op(e3,e2) = e3 & e2 != unit)) & ((op(e3,e4) != e2 | (op(e3,e2) = e4 & e2 != unit)) & ((op(e4,e0) != e2 | (op(e4,e2) = e0 & e2 != unit)) & ((op(e4,e1) != e2 | (op(e4,e2) = e1 & e2 != unit)) & ((op(e4,e2) != e2 | (op(e4,e2) = e2 & e2 != unit)) & ((op(e4,e3) != e2 | (op(e4,e2) = e3 & e2 != unit)) & (op(e4,e4) != e2 | (op(e4,e2) = e4 & e2 != unit)))))))))))))))))))))))))) | (((op(e0,e0) != e3 | (op(e0,e3) = e0 & e3 != unit)) & ((op(e0,e1) != e3 | (op(e0,e3) = e1 & e3 != unit)) & ((op(e0,e2) != e3 | (op(e0,e3) = e2 & e3 != unit)) & ((op(e0,e3) != e3 | (op(e0,e3) = e3 & e3 != unit)) & ((op(e0,e4) != e3 | (op(e0,e3) = e4 & e3 != unit)) & ((op(e1,e0) != e3 | (op(e1,e3) = e0 & e3 != unit)) & ((op(e1,e1) != e3 | (op(e1,e3) = e1 & e3 != unit)) & ((op(e1,e2) != e3 | (op(e1,e3) = e2 & e3 != unit)) & ((op(e1,e3) != e3 | (op(e1,e3) = e3 & e3 != unit)) & ((op(e1,e4) != e3 | (op(e1,e3) = e4 & e3 != unit)) & ((op(e2,e0) != e3 | (op(e2,e3) = e0 & e3 != unit)) & ((op(e2,e1) != e3 | (op(e2,e3) = e1 & e3 != unit)) & ((op(e2,e2) != e3 | (op(e2,e3) = e2 & e3 != unit)) & ((op(e2,e3) != e3 | (op(e2,e3) = e3 & e3 != unit)) & ((op(e2,e4) != e3 | (op(e2,e3) = e4 & e3 != unit)) & ((op(e3,e0) != e3 | (op(e3,e3) = e0 & e3 != unit)) & ((op(e3,e1) != e3 | (op(e3,e3) = e1 & e3 != unit)) & ((op(e3,e2) != e3 | (op(e3,e3) = e2 & e3 != unit)) & ((op(e3,e3) != e3 | (op(e3,e3) = e3 & e3 != unit)) & ((op(e3,e4) != e3 | (op(e3,e3) = e4 & e3 != unit)) & ((op(e4,e0) != e3 | (op(e4,e3) = e0 & e3 != unit)) & ((op(e4,e1) != e3 | (op(e4,e3) = e1 & e3 != unit)) & ((op(e4,e2) != e3 | (op(e4,e3) = e2 & e3 != unit)) & ((op(e4,e3) != e3 | (op(e4,e3) = e3 & e3 != unit)) & (op(e4,e4) != e3 | (op(e4,e3) = e4 & e3 != unit)))))))))))))))))))))))))) | ((op(e0,e0) != e4 | (op(e0,e4) = e0 & e4 != unit)) & ((op(e0,e1) != e4 | (op(e0,e4) = e1 & e4 != unit)) & ((op(e0,e2) != e4 | (op(e0,e4) = e2 & e4 != unit)) & ((op(e0,e3) != e4 | (op(e0,e4) = e3 & e4 != unit)) & ((op(e0,e4) != e4 | (op(e0,e4) = e4 & e4 != unit)) & ((op(e1,e0) != e4 | (op(e1,e4) = e0 & e4 != unit)) & ((op(e1,e1) != e4 | (op(e1,e4) = e1 & e4 != unit)) & ((op(e1,e2) != e4 | (op(e1,e4) = e2 & e4 != unit)) & ((op(e1,e3) != e4 | (op(e1,e4) = e3 & e4 != unit)) & ((op(e1,e4) != e4 | (op(e1,e4) = e4 & e4 != unit)) & ((op(e2,e0) != e4 | (op(e2,e4) = e0 & e4 != unit)) & ((op(e2,e1) != e4 | (op(e2,e4) = e1 & e4 != unit)) & ((op(e2,e2) != e4 | (op(e2,e4) = e2 & e4 != unit)) & ((op(e2,e3) != e4 | (op(e2,e4) = e3 & e4 != unit)) & ((op(e2,e4) != e4 | (op(e2,e4) = e4 & e4 != unit)) & ((op(e3,e0) != e4 | (op(e3,e4) = e0 & e4 != unit)) & ((op(e3,e1) != e4 | (op(e3,e4) = e1 & e4 != unit)) & ((op(e3,e2) != e4 | (op(e3,e4) = e2 & e4 != unit)) & ((op(e3,e3) != e4 | (op(e3,e4) = e3 & e4 != unit)) & ((op(e3,e4) != e4 | (op(e3,e4) = e4 & e4 != unit)) & ((op(e4,e0) != e4 | (op(e4,e4) = e0 & e4 != unit)) & ((op(e4,e1) != e4 | (op(e4,e4) = e1 & e4 != unit)) & ((op(e4,e2) != e4 | (op(e4,e4) = e2 & e4 != unit)) & ((op(e4,e3) != e4 | (op(e4,e4) = e3 & e4 != unit)) & (op(e4,e4) != e4 | (op(e4,e4) = e4 & e4 != unit)))))))))))))))))))))))))))))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4)))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 83.19/12.84 cnf(c15, plain, op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e4, inference(clausification, [status(esa)], [ax1])). % 83.19/12.84 cnf(c25, plain, op(unit,e0) = e0, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c26, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c28, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c30, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c31, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c32, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c33, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c34, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c35, plain, op(e0,unit) = e0, inference(clausification, [status(esa)], [ax2])). % 83.19/12.84 cnf(c51, plain, op(e3,e0) = e0 | op(e3,e4) = e0 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0, inference(clausification, [status(esa)], [ax3])). % 83.19/12.84 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])). % 83.19/12.84 cnf(c94, plain, op(e4,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c117, plain, op(e1,e3) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c123, plain, op(e2,e2) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c128, plain, op(e3,e2) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c129, plain, op(e3,e4) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c134, plain, op(e4,e4) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c141, plain, op(e3,e4) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c144, plain, op(e3,e4) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c146, plain, op(e2,e4) != op(e2,e3), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c154, plain, op(e1,e4) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c161, plain, op(e4,e4) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c172, plain, op(e3,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c181, plain, op(e4,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 83.19/12.84 cnf(c186, plain, e1 != e0, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c187, plain, e3 != e0, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c188, plain, e2 != e1, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c189, plain, e4 != e1, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c190, plain, e4 != e2, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c191, plain, e4 != e3, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c192, plain, e3 != e2, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c193, plain, e3 != e1, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c194, plain, e4 != e0, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c195, plain, e2 != e0, inference(clausification, [status(esa)], [ax5])). % 83.19/12.84 cnf(c196, plain, op(op(op(e2,e2),e2),op(op(e2,e2),e2)) = e0, inference(clausification, [status(esa)], [ax6])). % 83.19/12.84 cnf(c197, plain, op(e2,e2) = e3, inference(clausification, [status(esa)], [ax6])). % 83.19/12.84 cnf(c198, plain, op(op(e2,e2),op(e2,e2)) = e4, inference(clausification, [status(esa)], [ax6])). % 83.19/12.84 cnf(c199, plain, op(op(e2,e2),e2) = e1, inference(clausification, [status(esa)], [ax6])). % 83.19/12.84 cnf(c200, plain, X0 | X1 | X2 | X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c201, plain, X0 | op(e0,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c203, plain, X0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c210, plain, ~X0 | op(e1,e1) != e0 | op(e1,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c211, plain, ~X0 | op(e1,e1) != e0 | unit != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c252, plain, ~X0 | op(e0,e1) != e0 | op(e0,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c264, plain, ~X0 | op(e2,e0) != e2 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c268, plain, ~X0 | op(e2,e4) != e2 | op(e2,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c292, plain, ~X0 | op(e2,e1) != e2 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c322, plain, ~X0 | op(e3,e3) != e4 | op(e3,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c323, plain, ~X0 | op(e3,e3) != e4 | unit != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c324, plain, ~X0 | op(e4,e0) != e4 | op(e4,e4) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c332, plain, ~X0 | op(e4,e1) != e4 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c366, plain, ~X0 | op(e2,e2) != e3 | op(e2,e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c370, plain, ~X0 | op(e3,e1) != e3 | op(e3,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c388, plain, ~X0 | op(e3,e0) != e3 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c428, plain, ~X0 | op(e4,e4) != e1 | op(e4,e1) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c430, plain, ~X0 | op(e4,e3) != e1 | op(e4,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c434, plain, ~X0 | op(e3,e4) != e1 | op(e3,e1) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c436, plain, ~X0 | op(e3,e2) != e1 | op(e3,e1) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c437, plain, ~X0 | op(e3,e2) != e1 | unit != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c440, plain, ~X0 | op(e2,e3) != e1 | op(e2,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c456, plain, ~X0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c457, plain, ~X0 | X1 | op(e0,e0) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c459, plain, ~X0 | X1 | op(e4,e4) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c462, plain, ~X0 | X1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c463, plain, ~X0 | X1 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c466, plain, ~X0 | X1 | op(e2,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c468, plain, ~X0 | X1 | op(e4,e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c469, plain, ~X0 | X1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c472, plain, ~X0 | X1 | op(e4,e4) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c474, plain, ~X0 | X1 | op(e0,e0) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c475, plain, ~X0 | X1 | op(e4,e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c477, plain, ~X0 | X1 | op(e2,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c478, plain, ~X0 | X1 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c481, plain, ~X0 | X1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c483, plain, ~X0 | X1 | op(e1,e1) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c486, plain, ~X0 | X1 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c487, plain, ~X0 | X1 | op(e3,e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c490, plain, ~X0 | X1 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c495, plain, ~X0 | X1 | op(e3,e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c496, plain, ~X0 | X1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c499, plain, ~X0 | X1 | op(e1,e1) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c501, plain, ~X0 | X1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c504, plain, ~X0 | X1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c505, plain, ~X0 | X1 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c507, plain, ~X0 | X1 | op(e0,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(c510, plain, ~X0 | X1 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 83.19/12.84 cnf(d0, plain, op(e3,e2) = e1, inference(demodulation, [status(thm)], [c199,c197])). % 83.19/12.84 cnf(d1, plain, e1 != op(e3,e1), inference(demodulation, [status(thm)], [c128,d0])). % 83.19/12.84 cnf(d2, plain, op(e3,e1) = e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c32])). % 83.19/12.84 cnf(d3, plain, op(e3,e4) != e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d2,c129])). % 83.19/12.84 cnf(d4, plain, op(e1,e0) = e0 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c25])). % 83.19/12.84 cnf(d5, plain, unit != e1 | ~'Ts4', inference(resolution, [status(thm)], [d0,c437])). % 83.19/12.84 cnf(d6, plain, e1 != e1 | ~'Ts4' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,d5])). % 83.19/12.84 cnf(d7, plain, unit = e0 | unit = e3 | unit = e2 | unit = e4 | ~'Ts4', inference(equality_resolution, [status(thm)], [d6])). % 83.19/12.84 cnf(d8, plain, op(e3,op(e2,e2)) = e4, inference(demodulation, [status(thm)], [c198,c197])). % 83.19/12.84 cnf(d9, plain, op(e3,e3) = e4, inference(demodulation, [status(thm)], [d8,c197])). % 83.19/12.84 cnf(d10, plain, e4 = e1 | op(e3,e1) != e3 | ~'Ts3', inference(demodulation, [status(thm)], [c370,d9])). % 83.19/12.84 cnf(d11, plain, op(e3,e1) != e3 | ~'Ts3', inference(resolution, [status(thm)], [c189,d10])). % 83.19/12.84 cnf(d12, plain, e3 != e3 | ~'Ts3' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d2,d11])). % 83.19/12.84 cnf(d13, plain, unit = e0 | unit = e3 | unit = e2 | unit = e4 | ~'Ts3', inference(equality_resolution, [status(thm)], [d12])). % 83.19/12.84 cnf(d14, plain, e3 = e1 | op(e2,e1) != e2 | ~'Ts1', inference(demodulation, [status(thm)], [c292,c197])). % 83.19/12.84 cnf(d15, plain, op(e2,e1) != e2 | ~'Ts1', inference(resolution, [status(thm)], [c193,d14])). % 83.19/12.84 cnf(d16, plain, op(e2,e1) = e2 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c33])). % 83.19/12.84 cnf(d17, plain, e2 != e2 | ~'Ts1' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d16,d15])). % 83.19/12.84 cnf(d18, plain, unit = e0 | unit = e3 | unit = e2 | unit = e4 | ~'Ts1', inference(equality_resolution, [status(thm)], [d17])). % 83.19/12.84 cnf(d19, plain, op(e3,e4) = e3 | ~'Ts2', inference(resolution, [status(thm)], [d9,c322])). % 83.19/12.84 cnf(d20, plain, op(e3,e4) = e3 | 'Ts4' | 'Ts3' | 'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d19,c200])). % 83.19/12.84 cnf(d21, plain, op(op(e3,e2),op(op(e2,e2),e2)) = e0, inference(demodulation, [status(thm)], [c196,c197])). % 83.19/12.84 cnf(d22, plain, op(op(e3,e2),op(e3,e2)) = e0, inference(demodulation, [status(thm)], [d21,c197])). % 83.19/12.84 cnf(d23, plain, op(e1,op(e3,e2)) = e0, inference(demodulation, [status(thm)], [d22,d0])). % 83.19/12.84 cnf(d24, plain, op(e1,e1) = e0, inference(demodulation, [status(thm)], [d23,d0])). % 83.19/12.84 cnf(d25, plain, op(e1,e0) = e1 | ~'Ts0', inference(resolution, [status(thm)], [d24,c210])). % 83.19/12.84 cnf(d26, plain, op(e1,e0) = e1 | op(e3,e4) = e3 | 'Ts4' | 'Ts3' | 'Ts1', inference(resolution, [status(thm)], [d25,d20])). % 83.19/12.84 cnf(d27, plain, op(e3,e4) = e3 | op(e1,e0) = e1 | 'Ts4' | 'Ts3' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d26,d18])). % 83.19/12.84 cnf(d28, plain, op(e3,e4) = e3 | op(e1,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | 'Ts4' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d27,d13])). % 83.19/12.84 cnf(d29, plain, op(e3,e4) = e3 | op(e1,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d28,d7])). % 83.19/12.84 cnf(d30, plain, e1 = e0 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e3,e4) = e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d29,d4])). % 83.19/12.84 cnf(d31, plain, op(e3,e4) = e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c186,d30])). % 83.19/12.84 cnf(d32, plain, e3 != e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d31,d3])). % 83.19/12.84 cnf(d33, plain, unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(equality_resolution, [status(thm)], [d32])). % 83.19/12.84 cnf(d34, plain, op(e4,e0) = e0 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d33,c25])). % 83.19/12.84 cnf(d35, plain, e0 != op(e3,e0) | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d34,c181])). % 83.19/12.84 cnf(d36, plain, op(e3,e0) = e0 | e4 = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(demodulation, [status(thm)], [c51,d9])). % 83.19/12.84 cnf(d37, plain, op(e3,e0) = e0 | e1 = e0 | op(e3,e4) = e0 | op(e3,e1) = e0 | e4 = e0, inference(demodulation, [status(thm)], [d36,d0])). % 83.19/12.84 cnf(d38, plain, op(e3,e0) = e0 | e1 = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(resolution, [status(thm)], [c194,d37])). % 83.19/12.84 cnf(d39, plain, op(e3,e0) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(resolution, [status(thm)], [c186,d38])). % 83.19/12.84 cnf(d40, plain, op(e2,e4) = e2 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d33,c33])). % 83.19/12.84 cnf(d41, plain, e2 != op(e2,e3) | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d40,c146])). % 83.19/12.84 cnf(d42, plain, op(e1,e4) = e1 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d33,c34])). % 83.19/12.84 cnf(d43, plain, e1 != op(e1,e0) | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d42,c154])). % 83.19/12.84 cnf(d44, plain, op(e3,e1) = e2 | ~'Ts4', inference(resolution, [status(thm)], [d0,c436])). % 83.19/12.84 cnf(d45, plain, op(e2,e3) = e2 | ~'Ts3', inference(resolution, [status(thm)], [c197,c366])). % 83.19/12.84 cnf(d46, plain, e3 = e4 | op(e2,e4) != e2 | ~'Ts1', inference(demodulation, [status(thm)], [c268,c197])). % 83.19/12.84 cnf(d47, plain, op(e0,e1) = e0 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c35])). % 83.19/12.84 cnf(d48, plain, e0 != e0 | op(e0,e0) = e1 | ~'Ts0' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d47,c252])). % 83.19/12.84 cnf(d49, plain, op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | ~'Ts0', inference(equality_resolution, [status(thm)], [d48])). % 83.19/12.84 cnf(d50, plain, op(e4,e1) = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c31])). % 83.19/12.84 cnf(d51, plain, e4 != e4 | op(e4,e4) = e1 | ~'Ts2' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d50,c332])). % 83.19/12.84 cnf(d52, plain, op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | ~'Ts2', inference(equality_resolution, [status(thm)], [d51])). % 83.19/12.84 cnf(d53, plain, op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | 'Ts4' | 'Ts3' | 'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d52,c200])). % 83.19/12.84 cnf(d54, plain, op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | 'Ts4' | 'Ts3' | 'Ts1' | op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d53,d49])). % 83.19/12.84 cnf(d55, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | 'Ts4' | 'Ts3' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d54,d18])). % 83.19/12.84 cnf(d56, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | 'Ts4' | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d55,d13])). % 83.19/12.84 cnf(d57, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [d56,d7])). % 83.19/12.84 cnf(d58, plain, op(e1,e1) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [c30,c26])). % 83.19/12.84 cnf(d59, plain, e3 = e0 | ~'Ts5', inference(demodulation, [status(thm)], [c456,c197])). % 83.19/12.84 cnf(d60, plain, ~'Ts5', inference(resolution, [status(thm)], [c187,d59])). % 83.19/12.84 cnf(d61, plain, op(e4,e4) = e0 | ~'Ts6', inference(resolution, [status(thm)], [d60,c459])). % 83.19/12.84 cnf(d62, plain, e4 = e1 | 'Ts6' | ~'Ts7', inference(demodulation, [status(thm)], [c462,d9])). % 83.19/12.84 cnf(d63, plain, 'Ts6' | ~'Ts7', inference(resolution, [status(thm)], [c189,d62])). % 83.19/12.84 cnf(d64, plain, e3 = e0 | 'Ts7' | ~'Ts8', inference(demodulation, [status(thm)], [c463,c197])). % 83.19/12.84 cnf(d65, plain, 'Ts7' | ~'Ts8', inference(resolution, [status(thm)], [c187,d64])). % 83.19/12.84 cnf(d66, plain, e4 = e1 | 'Ts9' | ~'Ts10', inference(demodulation, [status(thm)], [c469,d9])). % 83.19/12.84 cnf(d67, plain, 'Ts9' | ~'Ts10', inference(resolution, [status(thm)], [c189,d66])). % 83.19/12.84 cnf(d68, plain, e4 = e2 | 'Ts15' | ~'Ts16', inference(demodulation, [status(thm)], [c487,d9])). % 83.19/12.84 cnf(d69, plain, 'Ts15' | ~'Ts16', inference(resolution, [status(thm)], [c190,d68])). % 83.19/12.84 cnf(d70, plain, e4 = e0 | 'Ts16' | ~'Ts17', inference(demodulation, [status(thm)], [c490,d9])). % 83.19/12.84 cnf(d71, plain, 'Ts16' | ~'Ts17', inference(resolution, [status(thm)], [c194,d70])). % 83.19/12.84 cnf(d72, plain, e4 = e2 | 'Ts17' | ~'Ts18', inference(demodulation, [status(thm)], [c495,d9])). % 83.19/12.84 cnf(d73, plain, 'Ts17' | ~'Ts18', inference(resolution, [status(thm)], [c190,d72])). % 83.19/12.84 cnf(d74, plain, e3 = e1 | 'Ts18' | ~'Ts19', inference(demodulation, [status(thm)], [c496,c197])). % 83.19/12.84 cnf(d75, plain, 'Ts18' | ~'Ts19', inference(resolution, [status(thm)], [c193,d74])). % 83.19/12.84 cnf(d76, plain, e3 = e1 | 'Ts20' | ~'Ts21', inference(demodulation, [status(thm)], [c504,c197])). % 83.19/12.84 cnf(d77, plain, 'Ts20' | ~'Ts21', inference(resolution, [status(thm)], [c193,d76])). % 83.19/12.84 cnf(d78, plain, e4 = e0 | ~'Ts23' | 'Ts22', inference(demodulation, [status(thm)], [c510,d9])). % 83.19/12.84 cnf(d79, plain, ~'Ts23' | 'Ts22', inference(resolution, [status(thm)], [c194,d78])). % 83.19/12.84 cnf(d80, plain, 'Ts22' | op(e0,e0) = e1, inference(resolution, [status(thm)], [d79,c201])). % 83.19/12.84 cnf(d81, plain, op(e0,e0) = e1 | op(e0,e0) = e1 | 'Ts21', inference(resolution, [status(thm)], [d80,c507])). % 83.19/12.84 cnf(d82, plain, op(e0,e0) = e1 | 'Ts20', inference(resolution, [status(thm)], [d81,d77])). % 83.19/12.84 cnf(d83, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | 'Ts19', inference(resolution, [status(thm)], [d82,c499])). % 83.19/12.84 cnf(d84, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | 'Ts18', inference(resolution, [status(thm)], [d83,d75])). % 83.19/12.84 cnf(d85, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | 'Ts17', inference(resolution, [status(thm)], [d84,d73])). % 83.19/12.84 cnf(d86, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | 'Ts16', inference(resolution, [status(thm)], [d85,d71])). % 83.19/12.84 cnf(d87, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | 'Ts15', inference(resolution, [status(thm)], [d86,d69])). % 83.19/12.84 cnf(d88, plain, op(e0,e0) = e1 | op(e1,e1) = e4 | op(e4,e4) = e3 | 'Ts14', inference(resolution, [status(thm)], [d87,c486])). % 83.19/12.84 cnf(d89, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e1,e1) = e4 | op(e1,e1) = e4 | 'Ts13', inference(resolution, [status(thm)], [d88,c483])). % 83.19/12.84 cnf(d90, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e1,e1) = e4 | op(e4,e4) = e3 | 'Ts12', inference(resolution, [status(thm)], [d89,c478])). % 83.19/12.84 cnf(d91, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e1,e1) = e4 | op(e4,e4) = e2 | 'Ts11', inference(resolution, [status(thm)], [d90,c475])). % 83.19/12.84 cnf(d92, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | op(e4,e4) = e0 | 'Ts10', inference(resolution, [status(thm)], [d91,c472])). % 83.19/12.84 cnf(d93, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | 'Ts9', inference(resolution, [status(thm)], [d92,d67])). % 83.19/12.84 cnf(d94, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | op(e4,e4) = e2 | 'Ts8', inference(resolution, [status(thm)], [d93,c468])). % 83.19/12.84 cnf(d95, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | 'Ts7', inference(resolution, [status(thm)], [d94,d65])). % 83.19/12.84 cnf(d96, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | 'Ts6', inference(resolution, [status(thm)], [d95,d63])). % 83.19/12.84 cnf(d97, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | op(e1,e1) = e4 | op(e4,e4) = e0, inference(resolution, [status(thm)], [d96,d61])). % 83.19/12.84 cnf(d98, plain, e4 = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2, inference(superposition, [status(thm)], [d97,d58])). % 83.19/12.84 cnf(d99, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e2 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c189,d98])). % 83.19/12.84 cnf(d100, plain, e2 = e1 | op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d99,d57])). % 83.19/12.84 cnf(d101, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c188,d100])). % 83.19/12.84 cnf(d102, plain, e3 = e1 | op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d101,d57])). % 83.19/12.84 cnf(d103, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c193,d102])). % 83.19/12.84 cnf(d104, plain, e1 = e0 | op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d57,d103])). % 83.19/12.84 cnf(d105, plain, op(e0,e0) = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c186,d104])). % 83.19/12.84 cnf(d106, plain, op(e0,e0) = e4 | ~'Ts6', inference(resolution, [status(thm)], [d60,c457])). % 83.19/12.84 cnf(d107, plain, e3 = e4 | 'Ts8' | ~'Ts9', inference(demodulation, [status(thm)], [c466,c197])). % 83.19/12.84 cnf(d108, plain, e3 = e4 | 'Ts11' | ~'Ts12', inference(demodulation, [status(thm)], [c477,c197])). % 83.19/12.84 cnf(d109, plain, 'Ts22' | op(e1,e1) = e0, inference(resolution, [status(thm)], [d79,c203])). % 83.19/12.84 cnf(d110, plain, op(e1,e1) = e0 | op(e1,e1) = e0 | 'Ts21', inference(resolution, [status(thm)], [d109,c505])). % 83.19/12.84 cnf(d111, plain, op(e1,e1) = e0 | 'Ts20', inference(resolution, [status(thm)], [d110,d77])). % 83.19/12.84 cnf(d112, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | 'Ts19', inference(resolution, [status(thm)], [d111,c499])). % 83.19/12.84 cnf(d113, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | 'Ts18', inference(resolution, [status(thm)], [d112,d75])). % 83.19/12.84 cnf(d114, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | 'Ts17', inference(resolution, [status(thm)], [d113,d73])). % 83.19/12.84 cnf(d115, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | 'Ts16', inference(resolution, [status(thm)], [d114,d71])). % 83.19/12.84 cnf(d116, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | 'Ts15', inference(resolution, [status(thm)], [d115,d69])). % 83.19/12.84 cnf(d117, plain, op(e1,e1) = e0 | op(e1,e1) = e4 | op(e4,e4) = e3 | 'Ts14', inference(resolution, [status(thm)], [d116,c486])). % 83.19/12.84 cnf(d118, plain, op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | op(e1,e1) = e4 | 'Ts13', inference(resolution, [status(thm)], [d117,c483])). % 83.19/12.84 cnf(d119, plain, op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | op(e4,e4) = e3 | 'Ts12', inference(resolution, [status(thm)], [d118,c478])). % 83.19/12.84 cnf(d120, plain, op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | 'Ts11', inference(resolution, [status(thm)], [d119,d108])). % 83.19/12.84 cnf(d121, plain, op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | op(e0,e0) = e4 | 'Ts10', inference(resolution, [status(thm)], [d120,c474])). % 83.19/12.84 cnf(d122, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | 'Ts9', inference(resolution, [status(thm)], [d121,d67])). % 83.19/12.84 cnf(d123, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | e3 = e4 | 'Ts8', inference(resolution, [status(thm)], [d122,d107])). % 83.19/12.84 cnf(d124, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | 'Ts7', inference(resolution, [status(thm)], [d123,d65])). % 83.19/12.84 cnf(d125, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | 'Ts6', inference(resolution, [status(thm)], [d124,d63])). % 83.19/12.84 cnf(d126, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | op(e1,e1) = e4 | e3 = e4 | op(e0,e0) = e4, inference(resolution, [status(thm)], [d125,d106])). % 83.19/12.84 cnf(d127, plain, e4 = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | e3 = e4, inference(superposition, [status(thm)], [d126,d58])). % 83.19/12.84 cnf(d128, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | op(e1,e1) = e0 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c189,d127])). % 83.19/12.84 cnf(d129, plain, e1 = e0 | op(e0,e0) = e4 | op(e4,e4) = e3 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d58,d128])). % 83.19/12.84 cnf(d130, plain, op(e0,e0) = e4 | op(e4,e4) = e3 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c186,d129])). % 83.19/12.84 cnf(d131, plain, e3 != op(e3,e4) | op(e0,e0) = e4 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d130,c161])). % 83.19/12.84 cnf(d132, plain, e3 != e3 | op(e0,e0) = e4 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d31,d131])). % 83.19/12.84 cnf(d133, plain, op(e0,e0) = e4 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(equality_resolution, [status(thm)], [d132])). % 83.19/12.84 cnf(d134, plain, e4 = e1 | unit = e0 | unit = e3 | unit = e2 | unit = e4 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(superposition, [status(thm)], [d133,d105])). % 83.19/12.84 cnf(d135, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e4, inference(resolution, [status(thm)], [c189,d134])). % 83.19/12.84 cnf(d136, plain, op(e2,e4) = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d135,c33])). % 83.19/12.84 cnf(d137, plain, e2 != e2 | e3 = e4 | ~'Ts1' | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d136,d46])). % 83.19/12.84 cnf(d138, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2 | ~'Ts1', inference(equality_resolution, [status(thm)], [d137])). % 83.19/12.84 cnf(d139, plain, unit != e4 | ~'Ts2', inference(resolution, [status(thm)], [d9,c323])). % 83.19/12.84 cnf(d140, plain, e4 != e4 | ~'Ts2' | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d135,d139])). % 83.19/12.84 cnf(d141, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2 | ~'Ts2', inference(equality_resolution, [status(thm)], [d140])). % 83.19/12.84 cnf(d142, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2 | 'Ts4' | 'Ts3' | 'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d141,c200])). % 83.19/12.84 cnf(d143, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2 | 'Ts4' | 'Ts3' | 'Ts1' | op(e1,e0) = e1, inference(resolution, [status(thm)], [d142,d25])). % 83.19/12.84 cnf(d144, plain, op(e1,e0) = e1 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | 'Ts4' | 'Ts3' | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(resolution, [status(thm)], [d143,d138])). % 83.19/12.84 cnf(d145, plain, op(e1,e0) = e1 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | 'Ts4' | op(e2,e3) = e2, inference(resolution, [status(thm)], [d144,d45])). % 83.19/12.84 cnf(d146, plain, op(e2,e3) = e2 | op(e1,e0) = e1 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | op(e3,e1) = e2, inference(resolution, [status(thm)], [d145,d44])). % 83.19/12.84 cnf(d147, plain, e1 != e1 | unit = e0 | unit = e3 | unit = e2 | op(e3,e1) = e2 | op(e2,e3) = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d146,d43])). % 83.19/12.84 cnf(d148, plain, op(e3,e1) = e2 | op(e2,e3) = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(equality_resolution, [status(thm)], [d147])). % 83.19/12.84 cnf(d149, plain, e2 != e2 | unit = e0 | unit = e3 | unit = e2 | op(e3,e1) = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d148,d41])). % 83.19/12.84 cnf(d150, plain, op(e3,e1) = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(equality_resolution, [status(thm)], [d149])). % 83.19/12.84 cnf(d151, plain, e2 = e0 | op(e3,e0) = e0 | op(e3,e4) = e0 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d150,d39])). % 83.19/12.84 cnf(d152, plain, op(e3,e0) = e0 | op(e3,e4) = e0 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(resolution, [status(thm)], [c195,d151])). % 83.19/12.84 cnf(d153, plain, op(e3,e4) = e3 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d33,c32])). % 83.19/12.84 cnf(d154, plain, e3 = e0 | op(e3,e0) = e0 | e3 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d153,d152])). % 83.19/12.84 cnf(d155, plain, op(e3,e0) = e0 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(resolution, [status(thm)], [c187,d154])). % 83.19/12.84 cnf(d156, plain, e0 != e0 | unit = e0 | unit = e3 | unit = e2 | e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(superposition, [status(thm)], [d155,d35])). % 83.19/12.84 cnf(d157, plain, e3 = e4 | unit = e0 | unit = e3 | unit = e2, inference(equality_resolution, [status(thm)], [d156])). % 83.19/12.84 cnf(d158, plain, op(e2,e2) = e2 | e3 = e4 | unit = e0 | unit = e3, inference(superposition, [status(thm)], [d157,c33])). % 83.19/12.84 cnf(d159, plain, e3 = e2 | e3 = e4 | unit = e0 | unit = e3, inference(demodulation, [status(thm)], [d158,c197])). % 83.19/12.84 cnf(d160, plain, e3 = e4 | unit = e0 | unit = e3, inference(resolution, [status(thm)], [c192,d159])). % 83.19/12.84 cnf(d161, plain, op(e3,e1) = e1 | e3 = e4 | unit = e0, inference(superposition, [status(thm)], [d160,c26])). % 83.19/12.84 cnf(d162, plain, e1 != e1 | e3 = e4 | unit = e0, inference(superposition, [status(thm)], [d161,d1])). % 83.19/12.84 cnf(d163, plain, e3 = e4 | unit = e0, inference(equality_resolution, [status(thm)], [d162])). % 83.19/12.84 cnf(d164, plain, op(e0,e0) = e0 | e3 = e4, inference(superposition, [status(thm)], [d163,c25])). % 83.19/12.84 cnf(d165, plain, op(e0,e3) = e3 | e3 = e4, inference(superposition, [status(thm)], [d163,c28])). % 83.19/12.84 cnf(d166, plain, op(e3,e0) != e3 | e4 = e0 | ~'Ts3', inference(demodulation, [status(thm)], [c388,d9])). % 83.19/12.84 cnf(d167, plain, op(e3,e0) != e3 | ~'Ts3', inference(resolution, [status(thm)], [c194,d166])). % 83.19/12.84 cnf(d168, plain, op(e3,e0) = e3 | e3 = e4, inference(superposition, [status(thm)], [d163,c32])). % 83.19/12.84 cnf(d169, plain, e3 != e3 | ~'Ts3' | e3 = e4, inference(superposition, [status(thm)], [d168,d167])). % 83.19/12.84 cnf(d170, plain, e3 = e4 | ~'Ts3', inference(equality_resolution, [status(thm)], [d169])). % 83.19/12.84 cnf(d171, plain, op(e2,e0) != e2 | e3 = e0 | ~'Ts1', inference(demodulation, [status(thm)], [c264,c197])). % 83.19/12.84 cnf(d172, plain, op(e2,e0) != e2 | ~'Ts1', inference(resolution, [status(thm)], [c187,d171])). % 83.19/12.84 cnf(d173, plain, op(e2,e0) = e2 | e3 = e4, inference(superposition, [status(thm)], [d163,c33])). % 83.19/12.84 cnf(d174, plain, e2 != e2 | ~'Ts1' | e3 = e4, inference(superposition, [status(thm)], [d173,d172])). % 83.19/12.84 cnf(d175, plain, e3 = e4 | ~'Ts1', inference(equality_resolution, [status(thm)], [d174])). % 83.19/12.84 cnf(d176, plain, unit != e0 | ~'Ts0', inference(resolution, [status(thm)], [d24,c211])). % 83.19/12.84 cnf(d177, plain, e0 != e0 | ~'Ts0' | e3 = e4, inference(superposition, [status(thm)], [d163,d176])). % 83.19/12.84 cnf(d178, plain, e3 = e4 | ~'Ts0', inference(equality_resolution, [status(thm)], [d177])). % 83.19/12.84 cnf(d179, plain, e3 = e4 | op(e3,e4) = e3 | 'Ts4' | 'Ts3' | 'Ts1', inference(resolution, [status(thm)], [d178,d20])). % 83.19/12.84 cnf(d180, plain, op(e3,e4) = e3 | e3 = e4 | 'Ts4' | 'Ts3' | e3 = e4, inference(resolution, [status(thm)], [d179,d175])). % 83.19/12.84 cnf(d181, plain, op(e3,e4) = e3 | e3 = e4 | 'Ts4' | e3 = e4, inference(resolution, [status(thm)], [d180,d170])). % 83.19/12.84 cnf(d182, plain, op(e3,e4) = e3 | e3 = e4 | op(e3,e1) = e2, inference(resolution, [status(thm)], [d181,d44])). % 83.19/12.84 cnf(d183, plain, op(e3,e4) != e2 | op(e3,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d182,c129])). % 83.19/12.84 cnf(d184, plain, e1 != e1 | op(e3,e1) = e4 | ~'Ts4' | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e4, inference(superposition, [status(thm)], [c15,c434])). % 83.19/12.84 cnf(d185, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e4 | op(e3,e1) = e4 | ~'Ts4', inference(equality_resolution, [status(thm)], [d184])). % 83.19/12.84 cnf(d186, plain, op(e3,e4) != e4, inference(demodulation, [status(thm)], [c141,d9])). % 83.19/12.84 cnf(d187, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e1) = e4 | ~'Ts4', inference(resolution, [status(thm)], [d186,d185])). % 83.19/12.84 cnf(d188, plain, op(e3,e4) = e3 | e3 = e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e1) = e4, inference(resolution, [status(thm)], [d181,d187])). % 83.19/12.84 cnf(d189, plain, e4 = e2 | op(e3,e4) = e3 | e3 = e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | e3 = e4, inference(superposition, [status(thm)], [d188,d182])). % 83.19/12.84 cnf(d190, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | e3 = e4, inference(resolution, [status(thm)], [c190,d189])). % 83.19/12.84 cnf(d191, plain, e2 != e2 | op(e3,e4) = e3 | e3 = e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d190,d183])). % 83.19/12.84 cnf(d192, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | e3 = e4, inference(equality_resolution, [status(thm)], [d191])). % 83.19/12.84 cnf(d193, plain, e3 != op(e3,e0) | op(e3,e4) = e0 | e3 = e4, inference(superposition, [status(thm)], [d192,c144])). % 83.19/12.84 cnf(d194, plain, e3 != e3 | op(e3,e4) = e0 | e3 = e4 | e3 = e4, inference(superposition, [status(thm)], [d168,d193])). % 83.19/12.84 cnf(d195, plain, op(e3,e4) = e0 | e3 = e4, inference(equality_resolution, [status(thm)], [d194])). % 83.19/12.84 cnf(d196, plain, e3 != op(e2,e1), inference(demodulation, [status(thm)], [c123,c197])). % 83.19/12.84 cnf(d197, plain, op(e4,e0) = e4 | e3 = e4, inference(superposition, [status(thm)], [d163,c31])). % 83.19/12.84 cnf(d198, plain, e4 != e4 | op(e4,e4) = e0 | ~'Ts2' | e3 = e4, inference(superposition, [status(thm)], [d197,c324])). % 83.19/12.84 cnf(d199, plain, op(e4,e4) = e0 | e3 = e4 | ~'Ts2', inference(equality_resolution, [status(thm)], [d198])). % 83.19/12.84 cnf(d200, plain, op(e4,e4) = e0 | e3 = e4 | 'Ts4' | 'Ts3' | 'Ts1' | 'Ts0', inference(resolution, [status(thm)], [d199,c200])). % 83.19/12.84 cnf(d201, plain, op(e4,e4) = e0 | e3 = e4 | 'Ts4' | 'Ts3' | 'Ts1' | e3 = e4, inference(resolution, [status(thm)], [d200,d178])). % 83.19/12.84 cnf(d202, plain, op(e4,e4) = e0 | e3 = e4 | 'Ts4' | 'Ts3' | e3 = e4, inference(resolution, [status(thm)], [d201,d175])). % 83.19/12.84 cnf(d203, plain, op(e4,e4) = e0 | e3 = e4 | 'Ts4' | e3 = e4, inference(resolution, [status(thm)], [d202,d170])). % 83.19/12.84 cnf(d204, plain, e1 != op(e1,e0) | op(e0,e3) = e1 | op(e3,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1, inference(superposition, [status(thm)], [c69,c117])). % 83.19/12.84 cnf(d205, plain, op(e0,e3) = e1 | e4 = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | e1 != op(e1,e0), inference(demodulation, [status(thm)], [d204,d9])). % 83.19/12.84 cnf(d206, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | e1 != op(e1,e0), inference(resolution, [status(thm)], [c189,d205])). % 83.19/12.84 cnf(d207, plain, op(e1,e0) = e1 | e3 = e4, inference(superposition, [status(thm)], [d163,c34])). % 83.19/12.84 cnf(d208, plain, e1 != e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | e3 = e4, inference(superposition, [status(thm)], [d207,d206])). % 83.19/12.84 cnf(d209, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e3) = e1 | e3 = e4, inference(equality_resolution, [status(thm)], [d208])). % 83.19/12.84 cnf(d210, plain, e1 != e1 | op(e4,e1) = e3 | ~'Ts4' | op(e0,e3) = e1 | op(e2,e3) = e1 | e3 = e4, inference(superposition, [status(thm)], [d209,c430])). % 83.19/12.84 cnf(d211, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e1) = e3 | e3 = e4 | ~'Ts4', inference(equality_resolution, [status(thm)], [d210])). % 83.19/12.84 cnf(d212, plain, op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e1) = e3 | e3 = e4 | op(e4,e4) = e0 | e3 = e4, inference(resolution, [status(thm)], [d211,d203])). % 83.19/12.84 cnf(d213, plain, op(e4,e4) != e3 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e4) = e0 | e3 = e4, inference(superposition, [status(thm)], [d212,c134])). % 83.19/12.84 cnf(d214, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | 'Ts11', inference(resolution, [status(thm)], [d90,d108])). % 83.19/12.84 cnf(d215, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | op(e4,e4) = e0 | 'Ts10', inference(resolution, [status(thm)], [d214,c472])). % 83.19/12.84 cnf(d216, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | 'Ts9', inference(resolution, [status(thm)], [d215,d67])). % 83.19/12.84 cnf(d217, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | e3 = e4 | 'Ts8', inference(resolution, [status(thm)], [d216,d107])). % 83.19/12.84 cnf(d218, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | 'Ts7', inference(resolution, [status(thm)], [d217,d65])). % 83.19/12.84 cnf(d219, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | 'Ts6', inference(resolution, [status(thm)], [d218,d63])). % 83.19/12.84 cnf(d220, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e1,e1) = e4 | e3 = e4 | op(e4,e4) = e0, inference(resolution, [status(thm)], [d219,d61])). % 83.19/12.84 cnf(d221, plain, op(e4,e1) != e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d220,c94])). % 83.19/12.84 cnf(d222, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | 'Ts19', inference(resolution, [status(thm)], [d82,c501])). % 83.19/12.84 cnf(d223, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | 'Ts18', inference(resolution, [status(thm)], [d222,d75])). % 83.19/12.84 cnf(d224, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | 'Ts17', inference(resolution, [status(thm)], [d223,d73])). % 83.19/12.84 cnf(d225, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | 'Ts16', inference(resolution, [status(thm)], [d224,d71])). % 83.19/12.84 cnf(d226, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | 'Ts15', inference(resolution, [status(thm)], [d225,d69])). % 83.19/12.84 cnf(d227, plain, op(e0,e0) = e1 | op(e4,e4) = e1 | op(e4,e4) = e3 | 'Ts14', inference(resolution, [status(thm)], [d226,c486])). % 83.19/12.84 cnf(d228, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e4,e4) = e1 | op(e4,e4) = e1 | 'Ts13', inference(resolution, [status(thm)], [d227,c481])). % 83.19/12.84 cnf(d229, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e4,e4) = e1 | op(e4,e4) = e3 | 'Ts12', inference(resolution, [status(thm)], [d228,c478])). % 83.19/12.84 cnf(d230, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | 'Ts11', inference(resolution, [status(thm)], [d229,d108])). % 83.19/12.84 cnf(d231, plain, op(e0,e0) = e1 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | op(e4,e4) = e0 | 'Ts10', inference(resolution, [status(thm)], [d230,c472])). % 83.19/12.84 cnf(d232, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | 'Ts9', inference(resolution, [status(thm)], [d231,d67])). % 83.19/12.84 cnf(d233, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | e3 = e4 | 'Ts8', inference(resolution, [status(thm)], [d232,d107])). % 83.19/12.84 cnf(d234, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | 'Ts7', inference(resolution, [status(thm)], [d233,d65])). % 83.19/12.84 cnf(d235, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | 'Ts6', inference(resolution, [status(thm)], [d234,d63])). % 83.19/12.84 cnf(d236, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e4) = e1 | e3 = e4 | op(e4,e4) = e0, inference(resolution, [status(thm)], [d235,d61])). % 83.19/12.84 cnf(d237, plain, e1 != e1 | op(e4,e1) = e4 | ~'Ts4' | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d236,c428])). % 83.19/12.84 cnf(d238, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e1) = e4 | e3 = e4 | ~'Ts4', inference(equality_resolution, [status(thm)], [d237])). % 83.19/12.84 cnf(d239, plain, op(e4,e4) = e0 | e3 = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | op(e4,e1) = e4 | e3 = e4, inference(resolution, [status(thm)], [d203,d238])). % 83.19/12.84 cnf(d240, plain, e4 != e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | e3 = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d239,d221])). % 83.19/12.84 cnf(d241, plain, op(e0,e0) = e1 | op(e4,e4) = e0 | op(e4,e4) = e3 | e3 = e4, inference(equality_resolution, [status(thm)], [d240])). % 83.19/12.84 cnf(d242, plain, e3 != e3 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e4) = e0 | e3 = e4 | op(e0,e0) = e1 | op(e4,e4) = e0 | e3 = e4, inference(superposition, [status(thm)], [d241,d213])). % 83.19/12.84 cnf(d243, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | op(e4,e4) = e0 | e3 = e4, inference(equality_resolution, [status(thm)], [d242])). % 83.19/12.84 cnf(d244, plain, e0 != op(e3,e4) | op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | e3 = e4, inference(superposition, [status(thm)], [d243,c161])). % 83.19/12.84 cnf(d245, plain, e0 != e0 | op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | e3 = e4 | e3 = e4, inference(superposition, [status(thm)], [d195,d244])). % 83.19/12.84 cnf(d246, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e3) = e1 | e3 = e4, inference(equality_resolution, [status(thm)], [d245])). % 83.19/12.84 cnf(d247, plain, e1 != e1 | op(e2,e1) = e3 | ~'Ts4' | op(e0,e0) = e1 | op(e0,e3) = e1 | e3 = e4, inference(superposition, [status(thm)], [d246,c440])). % 83.19/12.84 cnf(d248, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e1) = e3 | e3 = e4 | ~'Ts4', inference(equality_resolution, [status(thm)], [d247])). % 83.19/12.84 cnf(d249, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e2,e1) = e3 | e3 = e4 | op(e3,e4) = e3 | e3 = e4, inference(resolution, [status(thm)], [d248,d181])). % 83.19/12.84 cnf(d250, plain, e3 != e3 | op(e0,e0) = e1 | op(e0,e3) = e1 | op(e3,e4) = e3 | e3 = e4, inference(superposition, [status(thm)], [d249,d196])). % 83.19/12.84 cnf(d251, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | op(e3,e4) = e3 | e3 = e4, inference(equality_resolution, [status(thm)], [d250])). % 83.19/12.84 cnf(d252, plain, e3 = e0 | e3 = e4 | op(e0,e0) = e1 | op(e0,e3) = e1 | e3 = e4, inference(superposition, [status(thm)], [d251,d195])). % 83.19/12.84 cnf(d253, plain, op(e0,e0) = e1 | op(e0,e3) = e1 | e3 = e4, inference(resolution, [status(thm)], [c187,d252])). % 83.19/12.84 cnf(d254, plain, e1 = e3 | e3 = e4 | op(e0,e0) = e1 | e3 = e4, inference(superposition, [status(thm)], [d253,d165])). % 83.19/12.84 cnf(d255, plain, op(e3,e2) != e3, inference(demodulation, [status(thm)], [c172,c197])). % 83.19/12.84 cnf(d256, plain, e1 != e3, inference(demodulation, [status(thm)], [d255,d0])). % 83.19/12.84 cnf(d257, plain, op(e0,e0) = e1 | e3 = e4, inference(resolution, [status(thm)], [d256,d254])). % 83.19/12.84 cnf(d258, plain, e1 = e0 | e3 = e4 | e3 = e4, inference(superposition, [status(thm)], [d257,d164])). % 83.19/12.84 cnf(d259, plain, e3 = e4, inference(resolution, [status(thm)], [c186,d258])). % 83.19/12.84 cnf(d260, plain, e3 != e3, inference(demodulation, [status(thm)], [c191,d259])). % 83.19/12.84 cnf(d261, plain, $false, inference(equality_resolution, [status(thm)], [d260])). % 83.19/12.84 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------