%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n001.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 75.74s 13.92s % Output : CNFRefutation 75.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.57 % Computer : n001.cluster.edu % 0.10/0.57 % Model : x86_64 x86_64 % 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.57 % Memory : 8046.5625MB % 0.10/0.57 % OS : Linux 6.8.0-71-generic % 0.10/0.57 % CPULimit : 300 % 0.10/0.57 % WCLimit : 300 % 0.10/0.57 % DateTime : Sat Sep 26 21:10:29 UTC 2026 % 0.10/0.57 % CPUTime : % 0.10/0.57 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.74/13.92 % SZS status Theorem for theBenchmark.p % 75.74/13.92 % SZS output start CNFRefutation for theBenchmark.p % 75.74/13.92 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))))))))))))))))))))))))))))). % 75.74/13.92 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))))))))))))))). % 75.74/13.92 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)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 75.74/13.92 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 75.74/13.92 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 75.74/13.92 fof(ax6, axiom, (e0 = op(e1,op(op(e1,e1),op(e1,e1))) & (e2 = op(op(e1,e1),op(e1,e1)) & (e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) & e4 = op(e1,e1))))). % 75.74/13.92 fof(co1, conjecture, ~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = 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))))))))))))))))))))))))))))))))). % 75.74/13.92 fof(negated_conjecture, negated_conjecture, ~~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = 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])). % 75.74/13.92 cnf(c14, plain, op(e2,e4) = e2 | op(e2,e4) = e0 | op(e2,e4) = e4 | op(e2,e4) = e1 | op(e2,e4) = e3, inference(clausification, [status(esa)], [ax1])). % 75.74/13.92 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])). % 75.74/13.92 cnf(c19, plain, op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e4, inference(clausification, [status(esa)], [ax1])). % 75.74/13.92 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])). % 75.74/13.92 cnf(c23, plain, op(e4,e3) = e4 | op(e4,e3) = e2 | op(e4,e3) = e1 | op(e4,e3) = e0 | op(e4,e3) = e3, inference(clausification, [status(esa)], [ax1])). % 75.74/13.92 cnf(c26, plain, op(e0,unit) = e0, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c27, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c28, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c29, plain, op(unit,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c30, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c31, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c32, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c33, plain, op(unit,e4) = e4, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c34, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 cnf(c35, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 75.74/13.92 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])). % 75.74/13.92 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])). % 75.74/13.92 cnf(c56, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e4) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [ax3])). % 75.74/13.92 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])). % 75.74/13.92 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])). % 75.74/13.92 cnf(c76, plain, op(e4,e1) = e0 | op(e4,e0) = e0 | op(e4,e4) = e0 | op(e4,e3) = e0 | op(e4,e2) = e0, inference(clausification, [status(esa)], [ax3])). % 75.74/13.92 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])). % 75.74/13.92 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])). % 75.74/13.92 cnf(c83, plain, op(e3,e4) = e3 | op(e4,e4) = e3 | op(e2,e4) = e3 | op(e1,e4) = e3 | op(e0,e4) = e3, inference(clausification, [status(esa)], [ax3])). % 75.74/13.92 cnf(c90, plain, op(e1,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c94, plain, op(e2,e0) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c109, plain, op(e0,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c112, plain, op(e1,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c114, plain, op(e2,e2) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c119, plain, op(e0,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c124, plain, op(e2,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c125, plain, op(e3,e3) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c127, plain, op(e0,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c128, plain, op(e0,e4) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c129, plain, op(e0,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c132, plain, op(e1,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c133, plain, op(e2,e4) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c134, plain, op(e2,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c135, plain, op(e3,e4) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c138, plain, op(e0,e0) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c140, plain, op(e0,e1) != op(e0,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c144, plain, op(e0,e2) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c150, plain, op(e1,e1) != op(e1,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c151, plain, op(e1,e1) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c152, plain, op(e1,e1) != op(e1,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c156, plain, op(e2,e0) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c159, plain, op(e2,e0) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c164, plain, op(e2,e2) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c168, plain, op(e3,e0) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c169, plain, op(e3,e0) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c171, plain, op(e3,e1) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c173, plain, op(e3,e2) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c175, plain, op(e3,e3) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c177, plain, op(e4,e0) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c178, plain, op(e4,e0) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c179, plain, op(e4,e0) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c182, plain, op(e4,e1) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c183, plain, op(e4,e2) != op(e4,e3), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c184, plain, op(e4,e2) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c185, plain, op(e4,e3) != op(e4,e4), inference(clausification, [status(esa)], [ax4])). % 75.74/13.92 cnf(c186, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c187, plain, e0 != e2, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c188, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c189, plain, e0 != e4, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c193, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c194, plain, e2 != e4, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c195, plain, e3 != e4, inference(clausification, [status(esa)], [ax5])). % 75.74/13.92 cnf(c196, plain, e0 = op(e1,op(op(e1,e1),op(e1,e1))), inference(clausification, [status(esa)], [ax6])). % 75.74/13.92 cnf(c197, plain, e2 = op(op(e1,e1),op(e1,e1)), inference(clausification, [status(esa)], [ax6])). % 75.74/13.92 cnf(c198, plain, e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))), inference(clausification, [status(esa)], [ax6])). % 75.74/13.92 cnf(c199, plain, e4 = op(e1,e1), inference(clausification, [status(esa)], [ax6])). % 75.74/13.92 cnf(c200, plain, op(e2,e2) = e0 | op(e4,e4) = e0 | op(e1,e1) = e0 | op(e0,e0) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c201, plain, op(e2,e2) = e1 | op(e1,e1) = e1 | op(e3,e3) = e1 | op(e0,e0) = e1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c206, plain, X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | op(op(e4,e4),e4) = e4 | X22 | X23, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c207, plain, X0 | X1 | X2 | X3 | X4 | X5 | op(op(e4,e4),e4) != e4 | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c208, plain, ~X0 | op(e3,e4) != op(e4,e3), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c211, plain, ~X0 | op(e2,e4) != op(e4,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c214, plain, ~X0 | op(e1,e4) != op(e4,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c217, plain, ~X0 | op(e0,e4) != op(e4,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c220, plain, ~X0 | op(e4,e3) != op(e3,e4), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c223, plain, ~X0 | op(e3,e3) != op(e3,e3), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c226, plain, ~X0 | op(e2,e3) != op(e3,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c229, plain, ~X0 | op(e1,e3) != op(e3,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c232, plain, ~X0 | op(e0,e3) != op(e3,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c235, plain, ~X0 | op(e4,e2) != op(e2,e4), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c238, plain, ~X0 | op(e3,e2) != op(e2,e3), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c241, plain, ~X0 | op(e2,e2) != op(e2,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c244, plain, ~X0 | op(e1,e2) != op(e2,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c247, plain, ~X0 | op(e0,e2) != op(e2,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c250, plain, ~X0 | op(e4,e1) != op(e1,e4), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c253, plain, ~X0 | op(e3,e1) != op(e1,e3), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c257, plain, ~X0 | op(op(e1,e2),e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c259, plain, ~X0 | op(e1,e1) != op(e1,e1), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c262, plain, ~X0 | op(e0,e1) != op(e1,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c267, plain, ~X0 | op(op(e0,e4),e0) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c270, plain, ~X0 | op(op(e0,e3),e0) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c271, plain, ~X0 | op(e2,e0) != op(e0,e2), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c276, plain, ~X0 | op(op(e0,e1),e0) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(c277, plain, ~X0 | op(e0,e0) != op(e0,e0), inference(clausification, [status(esa)], [negated_conjecture])). % 75.74/13.92 cnf(d0, plain, e4 != op(e1,e4), inference(demodulation, [status(thm)], [c152,c199])). % 75.74/13.92 cnf(d1, plain, e2 = op(e4,op(e1,e1)), inference(demodulation, [status(thm)], [c197,c199])). % 75.74/13.92 cnf(d2, plain, e2 = op(e4,e4), inference(demodulation, [status(thm)], [d1,c199])). % 75.74/13.92 cnf(d3, plain, e3 = op(op(e4,op(e1,e1)),op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [c198,c199])). % 75.74/13.92 cnf(d4, plain, e3 = op(op(e4,e4),op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [d3,c199])). % 75.74/13.92 cnf(d5, plain, e3 = op(e2,op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [d4,d2])). % 75.74/13.92 cnf(d6, plain, e3 = op(e2,op(e4,op(e1,e1))), inference(demodulation, [status(thm)], [d5,c199])). % 75.74/13.92 cnf(d7, plain, e3 = op(e2,op(e4,e4)), inference(demodulation, [status(thm)], [d6,c199])). % 75.74/13.92 cnf(d8, plain, e3 = op(e2,e2), inference(demodulation, [status(thm)], [d7,d2])). % 75.74/13.92 cnf(d9, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | op(e4,e4) = e0 | e4 = e0, inference(demodulation, [status(thm)], [c200,c199])). % 75.74/13.92 cnf(d10, plain, op(e4,e2) != e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | e4 = e0, inference(superposition, [status(thm)], [d9,c184])). % 75.74/13.92 cnf(d11, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e2) != e0 | e4 = e0, inference(demodulation, [status(thm)], [d10,d8])). % 75.74/13.92 cnf(d12, plain, e0 = op(e1,op(e4,op(e1,e1))), inference(demodulation, [status(thm)], [c196,c199])). % 75.74/13.92 cnf(d13, plain, e0 = op(e1,op(e4,e4)), inference(demodulation, [status(thm)], [d12,c199])). % 75.74/13.92 cnf(d14, plain, e0 = op(e1,e2), inference(demodulation, [status(thm)], [d13,d2])). % 75.74/13.92 cnf(d15, plain, e4 != op(e1,e2), inference(demodulation, [status(thm)], [c150,c199])). % 75.74/13.92 cnf(d16, plain, e4 != e0, inference(demodulation, [status(thm)], [d15,d14])). % 75.74/13.92 cnf(d17, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e2) != e0, inference(resolution, [status(thm)], [d16,d11])). % 75.74/13.92 cnf(d18, plain, e0 = e2 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2 | op(e4,e0) = e0 | op(e4,e3) = e0 | op(e4,e2) = e0 | op(e4,e1) = e0, inference(superposition, [status(thm)], [c76,c80])). % 75.74/13.92 cnf(d19, plain, op(e4,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e0 | op(e4,e3) = e2 | op(e4,e2) = e0 | op(e4,e2) = e2 | op(e4,e1) = e0 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c187,d18])). % 75.74/13.92 cnf(d20, plain, op(e4,e2) != e2, inference(demodulation, [status(thm)], [c184,d2])). % 75.74/13.92 cnf(d21, plain, op(e4,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e0 | op(e4,e3) = e2 | op(e4,e2) = e0 | op(e4,e1) = e0 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d20,d19])). % 75.74/13.92 cnf(d22, plain, op(e4,e3) != e2, inference(demodulation, [status(thm)], [c185,d2])). % 75.74/13.92 cnf(d23, plain, op(e4,e0) = e0 | op(e4,e0) = e2 | op(e4,e3) = e0 | op(e4,e2) = e0 | op(e4,e1) = e0 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d22,d21])). % 75.74/13.92 cnf(d24, plain, op(e4,e0) != e2, inference(demodulation, [status(thm)], [c179,d2])). % 75.74/13.92 cnf(d25, plain, op(e4,e0) = e0 | op(e4,e3) = e0 | op(e4,e2) = e0 | op(e4,e1) = e0 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d24,d23])). % 75.74/13.92 cnf(d26, plain, op(e4,e1) != e2, inference(demodulation, [status(thm)], [c182,d2])). % 75.74/13.92 cnf(d27, plain, op(e4,e0) = e0 | op(e4,e3) = e0 | op(e4,e2) = e0 | op(e4,e1) = e0, inference(resolution, [status(thm)], [d26,d25])). % 75.74/13.92 cnf(d28, plain, e0 != e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e0) = e0 | op(e4,e3) = e0 | op(e4,e1) = e0, inference(superposition, [status(thm)], [d27,d17])). % 75.74/13.92 cnf(d29, plain, op(e4,e0) != e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | e4 = e0, inference(superposition, [status(thm)], [d9,c179])). % 75.74/13.92 cnf(d30, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e0) != e0 | e4 = e0, inference(demodulation, [status(thm)], [d29,d8])). % 75.74/13.92 cnf(d31, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e0) != e0, inference(resolution, [status(thm)], [d16,d30])). % 75.74/13.92 cnf(d32, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e4,e3) = e0 | op(e4,e1) = e0 | e0 != e0 | e3 = e0, inference(resolution, [status(thm)], [d31,d28])). % 75.74/13.92 cnf(d33, plain, op(e4,e3) != e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | e4 = e0, inference(superposition, [status(thm)], [d9,c185])). % 75.74/13.92 cnf(d34, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e3) != e0 | e4 = e0, inference(demodulation, [status(thm)], [d33,d8])). % 75.74/13.92 cnf(d35, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e3) != e0, inference(resolution, [status(thm)], [d16,d34])). % 75.74/13.92 cnf(d36, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e4,e1) = e0 | e0 != e0 | e3 = e0, inference(resolution, [status(thm)], [d35,d32])). % 75.74/13.92 cnf(d37, plain, op(e4,e1) != e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | e4 = e0, inference(superposition, [status(thm)], [d9,c182])). % 75.74/13.92 cnf(d38, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e1) != e0 | e4 = e0, inference(demodulation, [status(thm)], [d37,d8])). % 75.74/13.92 cnf(d39, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e1) != e0, inference(resolution, [status(thm)], [d16,d38])). % 75.74/13.92 cnf(d40, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e0,e0) = e0 | op(e3,e3) = e0 | e0 != e0 | e3 = e0, inference(resolution, [status(thm)], [d39,d36])). % 75.74/13.92 cnf(d41, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0, inference(equality_resolution, [status(thm)], [d40])). % 75.74/13.92 cnf(d42, plain, op(e4,e4) = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [c35,c33])). % 75.74/13.92 cnf(d43, plain, e2 = e4 | unit = e0 | unit = e3 | unit = e2 | unit = e1, inference(demodulation, [status(thm)], [d42,d2])). % 75.74/13.92 cnf(d44, plain, unit = e0 | unit = e3 | unit = e2 | unit = e1, inference(resolution, [status(thm)], [c194,d43])). % 75.74/13.92 cnf(d45, plain, op(e1,e2) = e1 | unit = e0 | unit = e3 | unit = e1, inference(superposition, [status(thm)], [d44,c28])). % 75.74/13.92 cnf(d46, plain, e0 = e1 | unit = e0 | unit = e3 | unit = e1, inference(demodulation, [status(thm)], [d45,d14])). % 75.74/13.92 cnf(d47, plain, unit = e0 | unit = e3 | unit = e1, inference(resolution, [status(thm)], [c186,d46])). % 75.74/13.92 cnf(d48, plain, op(e3,e3) = e3 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d47,c31])). % 75.74/13.92 cnf(d49, plain, e3 = e0 | op(e0,e0) = e0 | e3 = e0 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d48,d41])). % 75.74/13.92 cnf(d50, plain, op(e0,e3) = e0 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d47,c26])). % 75.74/13.92 cnf(d51, plain, op(e0,e0) != e0 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d50,c138])). % 75.74/13.92 cnf(d52, plain, unit = e0 | unit = e1 | e3 = e0 | unit = e0 | unit = e1, inference(resolution, [status(thm)], [d51,d49])). % 75.74/13.92 cnf(d53, plain, op(e2,e0) = e2 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d52,c30])). % 75.74/13.92 cnf(d54, plain, e0 != op(e4,e2), inference(demodulation, [status(thm)], [c112,d14])). % 75.74/13.92 cnf(d55, plain, e3 != op(e4,e2), inference(demodulation, [status(thm)], [c114,d8])). % 75.74/13.92 cnf(d56, plain, op(e4,e0) != e4 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e1, inference(superposition, [status(thm)], [c22,c177])). % 75.74/13.92 cnf(d57, plain, op(e4,e0) != e4 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e1, inference(resolution, [status(thm)], [d20,d56])). % 75.74/13.92 cnf(d58, plain, op(e4,e0) = e4 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d52,c34])). % 75.74/13.92 cnf(d59, plain, e4 != e4 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d58,d57])). % 75.74/13.92 cnf(d60, plain, op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d59])). % 75.74/13.92 cnf(d61, plain, e3 != e3 | op(e4,e2) = e0 | op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d60,d55])). % 75.74/13.92 cnf(d62, plain, op(e4,e2) = e0 | op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d61])). % 75.74/13.92 cnf(d63, plain, e0 != e0 | op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d62,d54])). % 75.74/13.92 cnf(d64, plain, e0 = op(e1,e2) | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2, inference(superposition, [status(thm)], [c80,d13])). % 75.74/13.92 cnf(d65, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2 | e0 = e0, inference(demodulation, [status(thm)], [d64,d14])). % 75.74/13.92 cnf(d66, plain, op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e1) = e2 | e0 = e0, inference(resolution, [status(thm)], [d20,d65])). % 75.74/13.92 cnf(d67, plain, op(e4,e0) = e2 | op(e4,e1) = e2 | e0 = e0, inference(resolution, [status(thm)], [d22,d66])). % 75.74/13.92 cnf(d68, plain, op(e4,e1) = e2 | e0 = e0, inference(resolution, [status(thm)], [d24,d67])). % 75.74/13.92 cnf(d69, plain, e0 = e0, inference(resolution, [status(thm)], [d26,d68])). % 75.74/13.92 cnf(d70, plain, op(e4,e2) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d69,d63])). % 75.74/13.92 cnf(d71, plain, e1 != op(e4,e3) | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d70,c183])). % 75.74/13.92 cnf(d72, plain, op(e4,e0) != e4 | op(e4,e3) = e0 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e3) = e1, inference(superposition, [status(thm)], [c23,c178])). % 75.74/13.92 cnf(d73, plain, op(e4,e0) != e4 | op(e4,e3) = e0 | op(e4,e3) = e3 | op(e4,e3) = e1, inference(resolution, [status(thm)], [d22,d72])). % 75.74/13.92 cnf(d74, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | op(e4,e4) = e1 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [c201,d8])). % 75.74/13.92 cnf(d75, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | e2 = e1 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d74,d2])). % 75.74/13.92 cnf(d76, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | e2 = e1 | e4 = e1, inference(demodulation, [status(thm)], [d75,c199])). % 75.74/13.92 cnf(d77, plain, e3 = e1 | op(e0,e0) = e1 | e3 = e1 | e2 = e1 | e4 = e1 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d48,d76])). % 75.74/13.92 cnf(d78, plain, e0 = e1 | e3 = e1 | e2 = e1 | e4 = e1 | unit = e0 | unit = e1 | e3 = e0 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d49,d77])). % 75.74/13.92 cnf(d79, plain, e3 = e0 | e3 = e1 | e2 = e1 | e4 = e1 | unit = e0 | unit = e1, inference(resolution, [status(thm)], [c186,d78])). % 75.74/13.92 cnf(d80, plain, e4 != op(e1,e3), inference(demodulation, [status(thm)], [c151,c199])). % 75.74/13.92 cnf(d81, plain, op(e1,e3) = e1 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d47,c28])). % 75.74/13.92 cnf(d82, plain, e4 != e1 | unit = e0 | unit = e1, inference(superposition, [status(thm)], [d81,d80])). % 75.74/13.92 cnf(d83, plain, unit = e0 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e0 | unit = e1, inference(resolution, [status(thm)], [d82,d79])). % 75.74/13.92 cnf(d84, plain, op(e4,e0) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c34])). % 75.74/13.92 cnf(d85, plain, e4 != e4 | op(e4,e3) = e0 | op(e4,e3) = e3 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d84,d73])). % 75.74/13.92 cnf(d86, plain, op(e4,e3) = e0 | op(e4,e3) = e3 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d85])). % 75.74/13.92 cnf(d87, plain, op(e0,e3) != e3 | op(e4,e3) = e0 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d86,c119])). % 75.74/13.92 cnf(d88, plain, op(e0,e3) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c31])). % 75.74/13.92 cnf(d89, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e4,e3) = e0 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d88,d87])). % 75.74/13.92 cnf(d90, plain, e3 != e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d70,d55])). % 75.74/13.92 cnf(d91, plain, e3 = e0 | unit = e1 | op(e4,e3) = e0 | op(e4,e3) = e1 | e3 = e0 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d90,d89])). % 75.74/13.92 cnf(d92, plain, op(e0,e2) != e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d70,c109])). % 75.74/13.92 cnf(d93, plain, op(e0,e2) = e2 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d52,c29])). % 75.74/13.92 cnf(d94, plain, e2 != e1 | e3 = e0 | unit = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d93,d92])). % 75.74/13.92 cnf(d95, plain, e3 = e0 | unit = e1 | op(e4,e3) = e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d94,d91])). % 75.74/13.92 cnf(d96, plain, op(e2,e3) != e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d95,c124])). % 75.74/13.92 cnf(d97, plain, e0 != op(e3,e4) | op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e2) = e0 | op(e2,e1) = e0, inference(superposition, [status(thm)], [c56,c133])). % 75.74/13.92 cnf(d98, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | e3 = e0 | op(e2,e1) = e0 | e0 != op(e3,e4), inference(demodulation, [status(thm)], [d97,d8])). % 75.74/13.92 cnf(d99, plain, op(e0,e4) != e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e2 | op(e3,e4) = e1, inference(superposition, [status(thm)], [c19,c128])). % 75.74/13.92 cnf(d100, plain, op(e3,e4) != e2, inference(demodulation, [status(thm)], [c135,d2])). % 75.74/13.92 cnf(d101, plain, op(e0,e4) != e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e1, inference(resolution, [status(thm)], [d100,d99])). % 75.74/13.92 cnf(d102, plain, op(e0,e4) = e4 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d52,c33])). % 75.74/13.92 cnf(d103, plain, e4 != e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d102,d101])). % 75.74/13.92 cnf(d104, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d103])). % 75.74/13.92 cnf(d105, plain, op(e3,e0) != e3 | op(e3,e4) = e0 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d104,c169])). % 75.74/13.92 cnf(d106, plain, op(e3,e0) = e3 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d52,c32])). % 75.74/13.92 cnf(d107, plain, e3 = e0 | unit = e1 | op(e3,e4) = e0 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d106,d105])). % 75.74/13.92 cnf(d108, plain, e0 != e0 | op(e2,e0) = e0 | op(e2,e3) = e0 | e3 = e0 | op(e2,e1) = e0 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d107,d98])). % 75.74/13.92 cnf(d109, plain, op(e3,e4) = e1 | op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d69,d108])). % 75.74/13.92 cnf(d110, plain, e0 != e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e0) = e0 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d109,d96])). % 75.74/13.92 cnf(d111, plain, op(e3,e4) = e1 | op(e2,e0) = e0 | op(e2,e1) = e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d69,d110])). % 75.74/13.92 cnf(d112, plain, e1 != e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e0) = e0 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d111,d71])). % 75.74/13.92 cnf(d113, plain, op(e3,e4) = e1 | op(e2,e0) = e0 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d112])). % 75.74/13.92 cnf(d114, plain, e0 = e2 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d113,d53])). % 75.74/13.92 cnf(d115, plain, op(e3,e4) = e1 | op(e2,e1) = e0 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [c187,d114])). % 75.74/13.92 cnf(d116, plain, op(e3,e4) != e0 | ~'Ts0' | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d89,c208])). % 75.74/13.92 cnf(d117, plain, op(e0,e4) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c33])). % 75.74/13.92 cnf(d118, plain, e4 != e4 | op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,d101])). % 75.74/13.92 cnf(d119, plain, op(e3,e4) = e0 | op(e3,e4) = e3 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d118])). % 75.74/13.92 cnf(d120, plain, op(e3,e0) != e3 | op(e3,e4) = e0 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d119,c169])). % 75.74/13.92 cnf(d121, plain, op(e3,e0) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c32])). % 75.74/13.92 cnf(d122, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e4) = e0 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d121,d120])). % 75.74/13.92 cnf(d123, plain, e0 != e0 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts0' | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d122,d116])). % 75.74/13.92 cnf(d124, plain, op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts0', inference(resolution, [status(thm)], [d69,d123])). % 75.74/13.92 cnf(d125, plain, e3 != op(e2,e4), inference(demodulation, [status(thm)], [c164,d8])). % 75.74/13.92 cnf(d126, plain, op(e0,e4) != e4 | op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e2 | op(e2,e4) = e1, inference(superposition, [status(thm)], [c14,c127])). % 75.74/13.92 cnf(d127, plain, op(e2,e4) != e2, inference(demodulation, [status(thm)], [c134,d2])). % 75.74/13.92 cnf(d128, plain, op(e0,e4) != e4 | op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e1, inference(resolution, [status(thm)], [d127,d126])). % 75.74/13.92 cnf(d129, plain, e4 != e4 | op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d102,d128])). % 75.74/13.92 cnf(d130, plain, op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d129])). % 75.74/13.92 cnf(d131, plain, e3 != e3 | op(e2,e4) = e0 | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d130,d125])). % 75.74/13.92 cnf(d132, plain, op(e2,e4) = e0 | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d131])). % 75.74/13.92 cnf(d133, plain, e0 != op(e3,e4) | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d132,c133])). % 75.74/13.92 cnf(d134, plain, e0 != e0 | op(e2,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d107,d133])). % 75.74/13.92 cnf(d135, plain, op(e3,e4) = e1 | op(e2,e4) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d69,d134])). % 75.74/13.92 cnf(d136, plain, e3 != e1 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d135,d125])). % 75.74/13.92 cnf(d137, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | e2 = e1 | unit = e1 | ~'Ts0', inference(resolution, [status(thm)], [d136,d124])). % 75.74/13.92 cnf(d138, plain, op(e2,e0) != e1 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d135,c159])). % 75.74/13.92 cnf(d139, plain, e2 != e1 | op(e3,e4) = e1 | e3 = e0 | unit = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d53,d138])). % 75.74/13.92 cnf(d140, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | unit = e1 | ~'Ts0', inference(resolution, [status(thm)], [d139,d137])). % 75.74/13.92 cnf(d141, plain, op(e0,e2) = e1 | ~'Ts16', inference(demodulation, [status(thm)], [c257,d14])). % 75.74/13.92 cnf(d142, plain, e4 != e4 | op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d84,d57])). % 75.74/13.92 cnf(d143, plain, op(e4,e2) = e0 | op(e4,e2) = e3 | op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d142])). % 75.74/13.92 cnf(d144, plain, e3 != e3 | op(e4,e2) = e0 | op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d143,d55])). % 75.74/13.92 cnf(d145, plain, op(e4,e2) = e0 | op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d144])). % 75.74/13.92 cnf(d146, plain, e0 != e0 | op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d145,d54])). % 75.74/13.92 cnf(d147, plain, op(e4,e2) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d69,d146])). % 75.74/13.92 cnf(d148, plain, e1 != op(e2,e4) | ~'Ts9' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d147,c235])). % 75.74/13.92 cnf(d149, plain, e4 != e4 | op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,d128])). % 75.74/13.92 cnf(d150, plain, op(e2,e4) = e0 | op(e2,e4) = e3 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d149])). % 75.74/13.92 cnf(d151, plain, e3 != e3 | op(e2,e4) = e0 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d150,d125])). % 75.74/13.92 cnf(d152, plain, op(e2,e4) = e0 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d151])). % 75.74/13.92 cnf(d153, plain, e0 != op(e3,e4) | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d152,c133])). % 75.74/13.92 cnf(d154, plain, e0 != e0 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d122,d153])). % 75.74/13.92 cnf(d155, plain, op(e3,e4) = e1 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d69,d154])). % 75.74/13.92 cnf(d156, plain, e1 != e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts9' | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d155,d148])). % 75.74/13.92 cnf(d157, plain, op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts9', inference(equality_resolution, [status(thm)], [d156])). % 75.74/13.92 cnf(d158, plain, op(e0,e4) != e4 | op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e2) = e4 | op(e2,e1) = e4, inference(superposition, [status(thm)], [c64,c127])). % 75.74/13.92 cnf(d159, plain, op(e0,e4) != e4 | op(e2,e0) = e4 | op(e2,e3) = e4 | e3 = e4 | op(e2,e1) = e4, inference(demodulation, [status(thm)], [d158,d8])). % 75.74/13.92 cnf(d160, plain, op(e0,e4) != e4 | op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e1) = e4, inference(resolution, [status(thm)], [c195,d159])). % 75.74/13.92 cnf(d161, plain, e4 != e4 | op(e2,e0) = e4 | op(e2,e3) = e4 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,d160])). % 75.74/13.92 cnf(d162, plain, op(e2,e0) != e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d84,c94])). % 75.74/13.92 cnf(d163, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e2,e3) = e4 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | e4 != e4 | unit = e1, inference(resolution, [status(thm)], [d162,d161])). % 75.74/13.92 cnf(d164, plain, op(e2,e3) = e4 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d163])). % 75.74/13.92 cnf(d165, plain, op(e3,e2) != e4 | ~'Ts10' | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d164,c238])). % 75.74/13.92 cnf(d166, plain, op(e4,e0) != e4 | op(e0,e2) = e4 | op(e3,e2) = e4 | op(e2,e2) = e4 | op(e1,e2) = e4, inference(superposition, [status(thm)], [c65,c177])). % 75.74/13.92 cnf(d167, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | e3 = e4 | op(e4,e0) != e4 | op(e1,e2) = e4, inference(demodulation, [status(thm)], [d166,d8])). % 75.74/13.92 cnf(d168, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | e3 = e4 | op(e4,e0) != e4 | e0 = e4, inference(demodulation, [status(thm)], [d167,d14])). % 75.74/13.92 cnf(d169, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | e3 = e4 | op(e4,e0) != e4, inference(resolution, [status(thm)], [c189,d168])). % 75.74/13.92 cnf(d170, plain, op(e0,e2) = e4 | op(e3,e2) = e4 | op(e4,e0) != e4, inference(resolution, [status(thm)], [c195,d169])). % 75.74/13.92 cnf(d171, plain, e4 != e4 | op(e0,e2) = e4 | op(e3,e2) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d84,d170])). % 75.74/13.92 cnf(d172, plain, op(e0,e2) != e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,c144])). % 75.74/13.92 cnf(d173, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e2) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | e4 != e4 | unit = e1, inference(resolution, [status(thm)], [d172,d171])). % 75.74/13.92 cnf(d174, plain, op(e3,e2) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d173])). % 75.74/13.92 cnf(d175, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts10', inference(resolution, [status(thm)], [d174,d165])). % 75.74/13.92 cnf(d176, plain, op(e2,e4) != e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts11' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(demodulation, [status(thm)], [c207,d2])). % 75.74/13.92 cnf(d177, plain, ~'Ts11', inference(equality_resolution, [status(thm)], [c241])). % 75.74/13.92 cnf(d178, plain, op(e2,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)], [d177,d176])). % 75.74/13.92 cnf(d179, plain, ~'Ts17', inference(equality_resolution, [status(thm)], [c259])). % 75.74/13.92 cnf(d180, plain, op(e2,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)], [d179,d178])). % 75.74/13.92 cnf(d181, plain, ~'Ts23', inference(equality_resolution, [status(thm)], [c277])). % 75.74/13.92 cnf(d182, plain, op(e2,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)], [d181,d180])). % 75.74/13.92 cnf(d183, plain, ~'Ts5', inference(equality_resolution, [status(thm)], [c223])). % 75.74/13.92 cnf(d184, plain, op(e2,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)], [d183,d182])). % 75.74/13.92 cnf(d185, plain, op(e2,e4) = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts11' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(demodulation, [status(thm)], [c206,d2])). % 75.74/13.92 cnf(d186, plain, op(e2,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)], [d177,d185])). % 75.74/13.92 cnf(d187, plain, op(e2,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)], [d179,d186])). % 75.74/13.92 cnf(d188, plain, op(e2,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)], [d181,d187])). % 75.74/13.92 cnf(d189, plain, op(e2,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)], [d183,d188])). % 75.74/13.92 cnf(d190, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d189,d184])). % 75.74/13.92 cnf(d191, plain, e2 = e3 | op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | op(e4,e1) = e3 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2, inference(superposition, [status(thm)], [c80,c82])). % 75.74/13.92 cnf(d192, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e1) = e3 | op(e4,e1) = e2, inference(resolution, [status(thm)], [c193,d191])). % 75.74/13.92 cnf(d193, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e3) = e2 | op(e4,e2) = e3 | op(e4,e1) = e3 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d20,d192])). % 75.74/13.92 cnf(d194, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e3) = e3 | op(e4,e2) = e3 | op(e4,e1) = e3 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d22,d193])). % 75.74/13.92 cnf(d195, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | op(e4,e1) = e3 | op(e4,e1) = e2, inference(resolution, [status(thm)], [d24,d194])). % 75.74/13.92 cnf(d196, plain, op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e2) = e3 | op(e4,e1) = e3, inference(resolution, [status(thm)], [d26,d195])). % 75.74/13.92 cnf(d197, plain, e3 = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e4,e0) = e3 | op(e4,e3) = e3 | op(e4,e1) = e3, inference(superposition, [status(thm)], [d196,d147])). % 75.74/13.92 cnf(d198, plain, op(e0,e3) != e3 | op(e4,e0) = e3 | op(e4,e1) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d197,c119])). % 75.74/13.92 cnf(d199, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e4,e0) = e3 | op(e4,e1) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d88,d198])). % 75.74/13.92 cnf(d200, plain, e3 = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e4,e1) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d199,d84])). % 75.74/13.92 cnf(d201, plain, op(e4,e1) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [c195,d200])). % 75.74/13.92 cnf(d202, plain, op(e1,e4) != e3 | ~'Ts2' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d201,c214])). % 75.74/13.92 cnf(d203, plain, e2 = e3 | op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e1,e4) = e3 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2, inference(superposition, [status(thm)], [c80,c83])). % 75.74/13.92 cnf(d204, plain, op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e2) = e2 | op(e4,e1) = e2 | op(e1,e4) = e3, inference(resolution, [status(thm)], [c193,d203])). % 75.74/13.92 cnf(d205, plain, op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e4,e0) = e2 | op(e4,e3) = e2 | op(e4,e1) = e2 | op(e1,e4) = e3, inference(resolution, [status(thm)], [d20,d204])). % 75.74/13.92 cnf(d206, plain, op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e4,e0) = e2 | op(e4,e1) = e2 | op(e1,e4) = e3, inference(resolution, [status(thm)], [d22,d205])). % 75.74/13.92 cnf(d207, plain, op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e4,e1) = e2 | op(e1,e4) = e3, inference(resolution, [status(thm)], [d24,d206])). % 75.74/13.92 cnf(d208, plain, op(e0,e4) = e3 | op(e3,e4) = e3 | op(e2,e4) = e3 | op(e1,e4) = e3, inference(resolution, [status(thm)], [d26,d207])). % 75.74/13.92 cnf(d209, plain, e3 = e0 | op(e2,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e4) = e3 | op(e3,e4) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [d208,d152])). % 75.74/13.92 cnf(d210, plain, e3 = e1 | op(e0,e4) = e3 | op(e3,e4) = e3 | op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e4) = e3 | op(e3,e4) = e3 | op(e1,e4) = e3, inference(superposition, [status(thm)], [d208,d209])). % 75.74/13.92 cnf(d211, plain, e3 = e0 | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e4) = e3 | op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d210,d122])). % 75.74/13.92 cnf(d212, plain, e3 = e1 | op(e0,e4) = e3 | op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e4) = e3 | op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d210,d211])). % 75.74/13.92 cnf(d213, plain, e3 = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d212,d117])). % 75.74/13.92 cnf(d214, plain, op(e1,e4) = e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [c195,d213])). % 75.74/13.92 cnf(d215, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts2', inference(resolution, [status(thm)], [d214,d202])). % 75.74/13.92 cnf(d216, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d215,d190])). % 75.74/13.92 cnf(d217, plain, op(e2,e0) = e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c30])). % 75.74/13.92 cnf(d218, plain, e2 != op(e2,e1) | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d217,c156])). % 75.74/13.92 cnf(d219, plain, op(e0,e1) = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | op(e4,e1) = e2 | e4 = e2, inference(demodulation, [status(thm)], [c51,c199])). % 75.74/13.92 cnf(d220, plain, op(e0,e1) = e2 | op(e3,e1) = e2 | op(e2,e1) = e2 | e4 = e2, inference(resolution, [status(thm)], [d26,d219])). % 75.74/13.92 cnf(d221, plain, e2 != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e1) = e2 | op(e3,e1) = e2 | e4 = e2, inference(superposition, [status(thm)], [d220,d218])). % 75.74/13.92 cnf(d222, plain, op(e0,e4) != e2, inference(demodulation, [status(thm)], [c129,d2])). % 75.74/13.92 cnf(d223, plain, e4 != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,d222])). % 75.74/13.92 cnf(d224, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e0,e1) = e2 | op(e3,e1) = e2 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d223,d221])). % 75.74/13.92 cnf(d225, plain, op(e0,e2) = e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c29])). % 75.74/13.92 cnf(d226, plain, op(e0,e1) != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d225,c140])). % 75.74/13.92 cnf(d227, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e1) = e2 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d226,d224])). % 75.74/13.92 cnf(d228, plain, op(e3,e1) = e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(equality_resolution, [status(thm)], [d227])). % 75.74/13.92 cnf(d229, plain, op(e1,e3) != e2 | ~'Ts7' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d228,c229])). % 75.74/13.92 cnf(d230, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e2) = e2 | op(e1,e4) = e2 | e4 = e2, inference(demodulation, [status(thm)], [c50,c199])). % 75.74/13.92 cnf(d231, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | e0 = e2 | op(e1,e4) = e2 | e4 = e2, inference(demodulation, [status(thm)], [d230,d14])). % 75.74/13.92 cnf(d232, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | op(e1,e4) = e2 | e4 = e2, inference(resolution, [status(thm)], [c187,d231])). % 75.74/13.92 cnf(d233, plain, op(e1,e4) != e2, inference(demodulation, [status(thm)], [c132,d2])). % 75.74/13.92 cnf(d234, plain, op(e1,e0) = e2 | op(e1,e3) = e2 | e4 = e2, inference(resolution, [status(thm)], [d233,d232])). % 75.74/13.92 cnf(d235, plain, e2 != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts7' | op(e1,e0) = e2 | e4 = e2, inference(superposition, [status(thm)], [d234,d229])). % 75.74/13.92 cnf(d236, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e1,e0) = e2 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1 | ~'Ts7', inference(resolution, [status(thm)], [d223,d235])). % 75.74/13.92 cnf(d237, plain, op(e1,e0) != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d217,c90])). % 75.74/13.92 cnf(d238, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1 | ~'Ts7', inference(resolution, [status(thm)], [d237,d236])). % 75.74/13.92 cnf(d239, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts7', inference(equality_resolution, [status(thm)], [d238])). % 75.74/13.92 cnf(d240, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d239,d216])). % 75.74/13.92 cnf(d241, plain, op(e0,e3) != e3 | ~'Ts8' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d121,c232])). % 75.74/13.92 cnf(d242, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts8', inference(resolution, [status(thm)], [d88,d241])). % 75.74/13.92 cnf(d243, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d242,d240])). % 75.74/13.92 cnf(d244, plain, e2 != op(e0,e2) | ~'Ts21' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d217,c271])). % 75.74/13.92 cnf(d245, plain, e2 != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts21' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d225,d244])). % 75.74/13.92 cnf(d246, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts21', inference(equality_resolution, [status(thm)], [d245])). % 75.74/13.92 cnf(d247, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d246,d243])). % 75.74/13.92 cnf(d248, plain, op(e0,e1) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c27])). % 75.74/13.92 cnf(d249, plain, e1 != op(e1,e0) | ~'Ts18' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d248,c262])). % 75.74/13.92 cnf(d250, plain, op(e1,e0) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d83,c28])). % 75.74/13.92 cnf(d251, plain, e1 != e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts18' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d250,d249])). % 75.74/13.92 cnf(d252, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts18', inference(equality_resolution, [status(thm)], [d251])). % 75.74/13.92 cnf(d253, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d252,d247])). % 75.74/13.92 cnf(d254, plain, op(e4,e0) != e4 | ~'Ts19' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d117,c267])). % 75.74/13.92 cnf(d255, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts19', inference(resolution, [status(thm)], [d84,d254])). % 75.74/13.92 cnf(d256, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d255,d253])). % 75.74/13.92 cnf(d257, plain, op(e3,e0) != e3 | ~'Ts20' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d88,c270])). % 75.74/13.92 cnf(d258, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts20', inference(resolution, [status(thm)], [d121,d257])). % 75.74/13.92 cnf(d259, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d258,d256])). % 75.74/13.92 cnf(d260, plain, op(e0,e2) != e2 | ~'Ts13' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d217,c247])). % 75.74/13.92 cnf(d261, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts13', inference(resolution, [status(thm)], [d225,d260])). % 75.74/13.92 cnf(d262, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d261,d259])). % 75.74/13.92 cnf(d263, plain, op(e1,e0) != e1 | ~'Ts22' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d248,c276])). % 75.74/13.92 cnf(d264, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts22', inference(resolution, [status(thm)], [d250,d263])). % 75.74/13.92 cnf(d265, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d264,d262])). % 75.74/13.92 cnf(d266, plain, op(e0,e4) != e4 | ~'Ts3' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d84,c217])). % 75.74/13.92 cnf(d267, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts3', inference(resolution, [status(thm)], [d117,d266])). % 75.74/13.92 cnf(d268, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d267,d265])). % 75.74/13.92 cnf(d269, plain, e2 != op(e1,e3) | ~'Ts15' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d228,c253])). % 75.74/13.92 cnf(d270, plain, e2 != e2 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts15' | op(e1,e0) = e2 | e4 = e2, inference(superposition, [status(thm)], [d234,d269])). % 75.74/13.92 cnf(d271, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e1,e0) = e2 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1 | ~'Ts15', inference(resolution, [status(thm)], [d223,d270])). % 75.74/13.92 cnf(d272, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 != e2 | e2 = e1 | unit = e1 | ~'Ts15', inference(resolution, [status(thm)], [d237,d271])). % 75.74/13.92 cnf(d273, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts15', inference(equality_resolution, [status(thm)], [d272])). % 75.74/13.92 cnf(d274, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts10', inference(resolution, [status(thm)], [d273,d268])). % 75.74/13.92 cnf(d275, plain, e3 != op(e1,e4) | ~'Ts14' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d201,c250])). % 75.74/13.92 cnf(d276, plain, e3 != e3 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts14' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d214,d275])). % 75.74/13.92 cnf(d277, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts14', inference(equality_resolution, [status(thm)], [d276])). % 75.74/13.92 cnf(d278, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts10', inference(resolution, [status(thm)], [d277,d274])). % 75.74/13.92 cnf(d279, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts12' | 'Ts16' | 'Ts9' | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d278,d175])). % 75.74/13.92 cnf(d280, plain, e4 != op(e3,e2) | ~'Ts6' | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d164,c226])). % 75.74/13.92 cnf(d281, plain, e4 != e4 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts6' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d174,d280])). % 75.74/13.92 cnf(d282, plain, op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts6', inference(equality_resolution, [status(thm)], [d281])). % 75.74/13.92 cnf(d283, plain, op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts1' | 'Ts0' | 'Ts12' | 'Ts16' | 'Ts9', inference(resolution, [status(thm)], [d282,d279])). % 75.74/13.92 cnf(d284, plain, op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts1' | 'Ts0' | 'Ts12' | 'Ts16' | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(resolution, [status(thm)], [d283,d157])). % 75.74/13.92 cnf(d285, plain, op(e2,e4) != e1 | ~'Ts1' | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d147,c211])). % 75.74/13.92 cnf(d286, plain, e1 != e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts1' | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d155,d285])). % 75.74/13.92 cnf(d287, plain, op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d286])). % 75.74/13.92 cnf(d288, plain, op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts0' | 'Ts12' | 'Ts16', inference(resolution, [status(thm)], [d287,d284])). % 75.74/13.92 cnf(d289, plain, op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts0' | 'Ts12' | op(e0,e2) = e1, inference(resolution, [status(thm)], [d288,d141])). % 75.74/13.92 cnf(d290, plain, op(e0,e2) != e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d147,c109])). % 75.74/13.92 cnf(d291, plain, e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts0' | 'Ts12', inference(resolution, [status(thm)], [d290,d289])). % 75.74/13.92 cnf(d292, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | e2 = e1 | unit = e1 | 'Ts4' | 'Ts0' | 'Ts12', inference(resolution, [status(thm)], [d136,d291])). % 75.74/13.92 cnf(d293, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | unit = e1 | 'Ts4' | 'Ts0' | 'Ts12', inference(resolution, [status(thm)], [d139,d292])). % 75.74/13.92 cnf(d294, plain, e0 != op(e2,e1) | ~'Ts12', inference(demodulation, [status(thm)], [c244,d14])). % 75.74/13.92 cnf(d295, plain, e0 != e0 | ~'Ts12' | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d115,d294])). % 75.74/13.92 cnf(d296, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | ~'Ts12', inference(resolution, [status(thm)], [d69,d295])). % 75.74/13.92 cnf(d297, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | unit = e1 | 'Ts4' | 'Ts0', inference(resolution, [status(thm)], [d296,d293])). % 75.74/13.92 cnf(d298, plain, op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | unit = e1 | 'Ts4' | op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d297,d140])). % 75.74/13.92 cnf(d299, plain, e0 != op(e3,e4) | ~'Ts4' | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d89,c220])). % 75.74/13.92 cnf(d300, plain, e0 != e0 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts4' | op(e3,e4) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1, inference(superposition, [status(thm)], [d122,d299])). % 75.74/13.92 cnf(d301, plain, op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | e3 = e1 | e2 = e1 | unit = e1 | ~'Ts4', inference(resolution, [status(thm)], [d69,d300])). % 75.74/13.92 cnf(d302, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | e2 = e1 | unit = e1 | ~'Ts4', inference(resolution, [status(thm)], [d136,d301])). % 75.74/13.92 cnf(d303, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | unit = e1 | ~'Ts4', inference(resolution, [status(thm)], [d139,d302])). % 75.74/13.92 cnf(d304, plain, op(e3,e4) = e1 | op(e4,e3) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d303,d298])). % 75.74/13.92 cnf(d305, plain, e1 != e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d304,d71])). % 75.74/13.92 cnf(d306, plain, op(e3,e4) = e1 | op(e2,e1) = e4 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d305])). % 75.74/13.92 cnf(d307, plain, e4 = e0 | op(e3,e4) = e1 | e3 = e0 | unit = e1 | op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d306,d115])). % 75.74/13.92 cnf(d308, plain, op(e3,e4) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d16,d307])). % 75.74/13.92 cnf(d309, plain, op(e3,e3) != e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d308,c175])). % 75.74/13.92 cnf(d310, plain, op(e3,e3) != e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d95,c125])). % 75.74/13.92 cnf(d311, plain, e4 != e4 | op(e0,e2) = e4 | op(e3,e2) = e4 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d58,d170])). % 75.74/13.92 cnf(d312, plain, op(e0,e2) != e4 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d102,c144])). % 75.74/13.92 cnf(d313, plain, e3 = e0 | unit = e1 | op(e3,e2) = e4 | e3 = e0 | e4 != e4 | unit = e1, inference(resolution, [status(thm)], [d312,d311])). % 75.74/13.92 cnf(d314, plain, op(e3,e2) = e4 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d313])). % 75.74/13.92 cnf(d315, plain, e4 != op(e3,e3) | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d314,c173])). % 75.74/13.92 cnf(d316, plain, e4 != e4 | e3 = e0 | unit = e1 | op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e1, inference(superposition, [status(thm)], [c18,d315])). % 75.74/13.92 cnf(d317, plain, op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e2 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d316])). % 75.74/13.92 cnf(d318, plain, op(e3,e1) != e2 | op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d317,c171])). % 75.74/13.92 cnf(d319, plain, e2 != op(e2,e1) | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d53,c156])). % 75.74/13.92 cnf(d320, plain, e2 != e2 | e3 = e0 | unit = e1 | op(e0,e1) = e2 | op(e3,e1) = e2 | e4 = e2, inference(superposition, [status(thm)], [d220,d319])). % 75.74/13.92 cnf(d321, plain, e4 != e2 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d102,d222])). % 75.74/13.92 cnf(d322, plain, e3 = e0 | unit = e1 | op(e0,e1) = e2 | op(e3,e1) = e2 | e3 = e0 | e2 != e2 | unit = e1, inference(resolution, [status(thm)], [d321,d320])). % 75.74/13.92 cnf(d323, plain, op(e0,e1) != e2 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d93,c140])). % 75.74/13.92 cnf(d324, plain, e3 = e0 | unit = e1 | op(e3,e1) = e2 | e3 = e0 | e2 != e2 | unit = e1, inference(resolution, [status(thm)], [d323,d322])). % 75.74/13.92 cnf(d325, plain, op(e3,e1) = e2 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d324])). % 75.74/13.92 cnf(d326, plain, e3 = e0 | unit = e1 | op(e3,e3) = e0 | op(e3,e3) = e3 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d325,d318])). % 75.74/13.92 cnf(d327, plain, op(e3,e0) != e3 | op(e3,e3) = e0 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d326,c168])). % 75.74/13.92 cnf(d328, plain, e3 = e0 | unit = e1 | op(e3,e3) = e0 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d106,d327])). % 75.74/13.92 cnf(d329, plain, e0 != e0 | op(e4,e3) = e1 | e3 = e0 | unit = e1 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d328,d310])). % 75.74/13.92 cnf(d330, plain, op(e3,e3) = e1 | op(e4,e3) = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d69,d329])). % 75.74/13.92 cnf(d331, plain, e1 != e1 | e3 = e0 | unit = e1 | op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(superposition, [status(thm)], [d330,d71])). % 75.74/13.92 cnf(d332, plain, op(e3,e3) = e1 | e3 = e0 | unit = e1, inference(equality_resolution, [status(thm)], [d331])). % 75.74/13.92 cnf(d333, plain, e3 = e0 | unit = e1 | e3 = e0 | unit = e1, inference(resolution, [status(thm)], [d332,d309])). % 75.74/13.92 cnf(d334, plain, op(e1,e4) = e4 | e3 = e0, inference(superposition, [status(thm)], [d333,c33])). % 75.74/13.92 cnf(d335, plain, e4 != e4 | e3 = e0, inference(superposition, [status(thm)], [d334,d0])). % 75.74/13.92 cnf(d336, plain, e3 = e0, inference(equality_resolution, [status(thm)], [d335])). % 75.74/13.92 cnf(d337, plain, e0 != e0, inference(demodulation, [status(thm)], [c188,d336])). % 75.74/13.92 cnf(d338, plain, $false, inference(resolution, [status(thm)], [d69,d337])). % 75.74/13.92 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------