%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG139+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 : n014.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:39 AM UTC 2026 % Result : Unsatisfiable 104.92s 21.68s % Output : CNFRefutation 104.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : ALG139+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/5.47 % Computer : n014.cluster.edu % 0.17/5.47 % Model : x86_64 x86_64 % 0.17/5.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/5.47 % Memory : 8046.5625MB % 0.17/5.47 % OS : Linux 6.8.0-71-generic % 0.17/5.47 % CPULimit : 300 % 0.17/5.47 % WCLimit : 300 % 0.17/5.47 % DateTime : Sat Sep 26 21:15:51 UTC 2026 % 0.17/5.47 % CPUTime : % 0.17/5.47 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 104.92/21.68 % SZS status Unsatisfiable for theBenchmark.p % 104.92/21.68 % SZS output start CNFRefutation for theBenchmark.p % 104.92/21.68 fof(ax1, axiom, ((op(e0,e0) = e0 | (op(e0,e0) = e1 | (op(e0,e0) = e2 | op(e0,e0) = e3))) & ((op(e0,e1) = e0 | (op(e0,e1) = e1 | (op(e0,e1) = e2 | op(e0,e1) = e3))) & ((op(e0,e2) = e0 | (op(e0,e2) = e1 | (op(e0,e2) = e2 | op(e0,e2) = e3))) & ((op(e0,e3) = e0 | (op(e0,e3) = e1 | (op(e0,e3) = e2 | op(e0,e3) = e3))) & ((op(e1,e0) = e0 | (op(e1,e0) = e1 | (op(e1,e0) = e2 | op(e1,e0) = e3))) & ((op(e1,e1) = e0 | (op(e1,e1) = e1 | (op(e1,e1) = e2 | op(e1,e1) = e3))) & ((op(e1,e2) = e0 | (op(e1,e2) = e1 | (op(e1,e2) = e2 | op(e1,e2) = e3))) & ((op(e1,e3) = e0 | (op(e1,e3) = e1 | (op(e1,e3) = e2 | op(e1,e3) = e3))) & ((op(e2,e0) = e0 | (op(e2,e0) = e1 | (op(e2,e0) = e2 | op(e2,e0) = e3))) & ((op(e2,e1) = e0 | (op(e2,e1) = e1 | (op(e2,e1) = e2 | op(e2,e1) = e3))) & ((op(e2,e2) = e0 | (op(e2,e2) = e1 | (op(e2,e2) = e2 | op(e2,e2) = e3))) & ((op(e2,e3) = e0 | (op(e2,e3) = e1 | (op(e2,e3) = e2 | op(e2,e3) = e3))) & ((op(e3,e0) = e0 | (op(e3,e0) = e1 | (op(e3,e0) = e2 | op(e3,e0) = e3))) & ((op(e3,e1) = e0 | (op(e3,e1) = e1 | (op(e3,e1) = e2 | op(e3,e1) = e3))) & ((op(e3,e2) = e0 | (op(e3,e2) = e1 | (op(e3,e2) = e2 | op(e3,e2) = e3))) & (op(e3,e3) = e0 | (op(e3,e3) = e1 | (op(e3,e3) = e2 | op(e3,e3) = e3))))))))))))))))))). % 104.92/21.68 fof(ax2, axiom, ((op(e0,e0) = e0 | (op(e0,e1) = e0 | (op(e0,e2) = e0 | op(e0,e3) = e0))) & ((op(e0,e0) = e0 | (op(e1,e0) = e0 | (op(e2,e0) = e0 | op(e3,e0) = e0))) & ((op(e0,e0) = e1 | (op(e0,e1) = e1 | (op(e0,e2) = e1 | op(e0,e3) = e1))) & ((op(e0,e0) = e1 | (op(e1,e0) = e1 | (op(e2,e0) = e1 | op(e3,e0) = e1))) & ((op(e0,e0) = e2 | (op(e0,e1) = e2 | (op(e0,e2) = e2 | op(e0,e3) = e2))) & ((op(e0,e0) = e2 | (op(e1,e0) = e2 | (op(e2,e0) = e2 | op(e3,e0) = e2))) & ((op(e0,e0) = e3 | (op(e0,e1) = e3 | (op(e0,e2) = e3 | op(e0,e3) = e3))) & ((op(e0,e0) = e3 | (op(e1,e0) = e3 | (op(e2,e0) = e3 | op(e3,e0) = e3))) & ((op(e1,e0) = e0 | (op(e1,e1) = e0 | (op(e1,e2) = e0 | op(e1,e3) = e0))) & ((op(e0,e1) = e0 | (op(e1,e1) = e0 | (op(e2,e1) = e0 | op(e3,e1) = e0))) & ((op(e1,e0) = e1 | (op(e1,e1) = e1 | (op(e1,e2) = e1 | op(e1,e3) = e1))) & ((op(e0,e1) = e1 | (op(e1,e1) = e1 | (op(e2,e1) = e1 | op(e3,e1) = e1))) & ((op(e1,e0) = e2 | (op(e1,e1) = e2 | (op(e1,e2) = e2 | op(e1,e3) = e2))) & ((op(e0,e1) = e2 | (op(e1,e1) = e2 | (op(e2,e1) = e2 | op(e3,e1) = e2))) & ((op(e1,e0) = e3 | (op(e1,e1) = e3 | (op(e1,e2) = e3 | op(e1,e3) = e3))) & ((op(e0,e1) = e3 | (op(e1,e1) = e3 | (op(e2,e1) = e3 | op(e3,e1) = e3))) & ((op(e2,e0) = e0 | (op(e2,e1) = e0 | (op(e2,e2) = e0 | op(e2,e3) = e0))) & ((op(e0,e2) = e0 | (op(e1,e2) = e0 | (op(e2,e2) = e0 | op(e3,e2) = e0))) & ((op(e2,e0) = e1 | (op(e2,e1) = e1 | (op(e2,e2) = e1 | op(e2,e3) = e1))) & ((op(e0,e2) = e1 | (op(e1,e2) = e1 | (op(e2,e2) = e1 | op(e3,e2) = e1))) & ((op(e2,e0) = e2 | (op(e2,e1) = e2 | (op(e2,e2) = e2 | op(e2,e3) = e2))) & ((op(e0,e2) = e2 | (op(e1,e2) = e2 | (op(e2,e2) = e2 | op(e3,e2) = e2))) & ((op(e2,e0) = e3 | (op(e2,e1) = e3 | (op(e2,e2) = e3 | op(e2,e3) = e3))) & ((op(e0,e2) = e3 | (op(e1,e2) = e3 | (op(e2,e2) = e3 | op(e3,e2) = e3))) & ((op(e3,e0) = e0 | (op(e3,e1) = e0 | (op(e3,e2) = e0 | op(e3,e3) = e0))) & ((op(e0,e3) = e0 | (op(e1,e3) = e0 | (op(e2,e3) = e0 | op(e3,e3) = e0))) & ((op(e3,e0) = e1 | (op(e3,e1) = e1 | (op(e3,e2) = e1 | op(e3,e3) = e1))) & ((op(e0,e3) = e1 | (op(e1,e3) = e1 | (op(e2,e3) = e1 | op(e3,e3) = e1))) & ((op(e3,e0) = e2 | (op(e3,e1) = e2 | (op(e3,e2) = e2 | op(e3,e3) = e2))) & ((op(e0,e3) = e2 | (op(e1,e3) = e2 | (op(e2,e3) = e2 | op(e3,e3) = e2))) & ((op(e3,e0) = e3 | (op(e3,e1) = e3 | (op(e3,e2) = e3 | op(e3,e3) = e3))) & (op(e0,e3) = e3 | (op(e1,e3) = e3 | (op(e2,e3) = e3 | op(e3,e3) = e3))))))))))))))))))))))))))))))))))). % 104.92/21.68 fof(ax3, axiom, (op(e0,e0) != op(e1,e0) & (op(e0,e0) != op(e2,e0) & (op(e0,e0) != op(e3,e0) & (op(e1,e0) != op(e2,e0) & (op(e1,e0) != op(e3,e0) & (op(e2,e0) != op(e3,e0) & (op(e0,e1) != op(e1,e1) & (op(e0,e1) != op(e2,e1) & (op(e0,e1) != op(e3,e1) & (op(e1,e1) != op(e2,e1) & (op(e1,e1) != op(e3,e1) & (op(e2,e1) != op(e3,e1) & (op(e0,e2) != op(e1,e2) & (op(e0,e2) != op(e2,e2) & (op(e0,e2) != op(e3,e2) & (op(e1,e2) != op(e2,e2) & (op(e1,e2) != op(e3,e2) & (op(e2,e2) != op(e3,e2) & (op(e0,e3) != op(e1,e3) & (op(e0,e3) != op(e2,e3) & (op(e0,e3) != op(e3,e3) & (op(e1,e3) != op(e2,e3) & (op(e1,e3) != op(e3,e3) & (op(e2,e3) != op(e3,e3) & (op(e0,e0) != op(e0,e1) & (op(e0,e0) != op(e0,e2) & (op(e0,e0) != op(e0,e3) & (op(e0,e1) != op(e0,e2) & (op(e0,e1) != op(e0,e3) & (op(e0,e2) != op(e0,e3) & (op(e1,e0) != op(e1,e1) & (op(e1,e0) != op(e1,e2) & (op(e1,e0) != op(e1,e3) & (op(e1,e1) != op(e1,e2) & (op(e1,e1) != op(e1,e3) & (op(e1,e2) != op(e1,e3) & (op(e2,e0) != op(e2,e1) & (op(e2,e0) != op(e2,e2) & (op(e2,e0) != op(e2,e3) & (op(e2,e1) != op(e2,e2) & (op(e2,e1) != op(e2,e3) & (op(e2,e2) != op(e2,e3) & (op(e3,e0) != op(e3,e1) & (op(e3,e0) != op(e3,e2) & (op(e3,e0) != op(e3,e3) & (op(e3,e1) != op(e3,e2) & (op(e3,e1) != op(e3,e3) & op(e3,e2) != op(e3,e3))))))))))))))))))))))))))))))))))))))))))))))))). % 104.92/21.68 fof(ax4, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e1 != e2 & (e1 != e3 & e2 != e3)))))). % 104.92/21.68 fof(ax5, axiom, (((op(e0,e0) = e0 & op(e0,e0) != e0) | ((op(e1,e1) = e0 & op(e0,e0) != e1) | ((op(e2,e2) = e0 & op(e0,e0) != e2) | (op(e3,e3) = e0 & op(e0,e0) != e3)))) & (((op(e0,e0) = e1 & op(e1,e1) != e0) | ((op(e1,e1) = e1 & op(e1,e1) != e1) | ((op(e2,e2) = e1 & op(e1,e1) != e2) | (op(e3,e3) = e1 & op(e1,e1) != e3)))) & (((op(e0,e0) = e2 & op(e2,e2) != e0) | ((op(e1,e1) = e2 & op(e2,e2) != e1) | ((op(e2,e2) = e2 & op(e2,e2) != e2) | (op(e3,e3) = e2 & op(e2,e2) != e3)))) & ((op(e0,e0) = e3 & op(e3,e3) != e0) | ((op(e1,e1) = e3 & op(e3,e3) != e1) | ((op(e2,e2) = e3 & op(e3,e3) != e2) | (op(e3,e3) = e3 & op(e3,e3) != e3)))))))). % 104.92/21.68 fof(ax6, axiom, ~((e0 = op(op(e2,e2),e2) & (e1 = op(op(e2,e2),op(e2,e2)) & e3 = op(e2,e2))))). % 104.92/21.68 fof(ax7, axiom, ~((e0 = op(op(e3,e3),e3) & (e1 = op(op(e3,e3),op(e3,e3)) & e2 = op(e3,e3))))). % 104.92/21.68 fof(ax11, axiom, ~((e0 = op(op(e2,e2),e2) & (e3 = op(op(e2,e2),op(e2,e2)) & e1 = op(e2,e2))))). % 104.92/21.68 fof(ax12, axiom, ~((e1 = op(op(e2,e2),e2) & (e0 = op(op(e2,e2),op(e2,e2)) & e3 = op(e2,e2))))). % 104.92/21.68 fof(ax14, axiom, ~((e1 = op(op(e0,e0),e0) & (e2 = op(op(e0,e0),op(e0,e0)) & e3 = op(e0,e0))))). % 104.92/21.68 fof(ax16, axiom, ~((e1 = op(op(e0,e0),e0) & (e3 = op(op(e0,e0),op(e0,e0)) & e2 = op(e0,e0))))). % 104.92/21.68 fof(ax17, axiom, ~((e1 = op(op(e2,e2),e2) & (e3 = op(op(e2,e2),op(e2,e2)) & e0 = op(e2,e2))))). % 104.92/21.68 fof(ax18, axiom, ~((e2 = op(op(e1,e1),e1) & (e0 = op(op(e1,e1),op(e1,e1)) & e3 = op(e1,e1))))). % 104.92/21.68 fof(ax20, axiom, ~((e2 = op(op(e0,e0),e0) & (e1 = op(op(e0,e0),op(e0,e0)) & e3 = op(e0,e0))))). % 104.92/21.68 fof(ax21, axiom, ~((e2 = op(op(e3,e3),e3) & (e1 = op(op(e3,e3),op(e3,e3)) & e0 = op(e3,e3))))). % 104.92/21.68 fof(ax22, axiom, ~((e2 = op(op(e0,e0),e0) & (e3 = op(op(e0,e0),op(e0,e0)) & e1 = op(e0,e0))))). % 104.92/21.68 fof(ax27, axiom, ~((e3 = op(op(e2,e2),e2) & (e1 = op(op(e2,e2),op(e2,e2)) & e0 = op(e2,e2))))). % 104.92/21.68 cnf(c2, plain, op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c4, plain, op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c6, plain, op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c8, plain, op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c12, plain, op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c14, plain, op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 104.92/21.68 cnf(c19, plain, op(e0,e0) = e1 | op(e1,e0) = e1 | op(e2,e0) = e1 | op(e3,e0) = e1, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c21, plain, op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c22, plain, op(e0,e0) = e3 | op(e0,e1) = e3 | op(e0,e2) = e3 | op(e0,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c24, plain, op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c32, plain, op(e2,e0) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0 | op(e2,e3) = e0, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c33, plain, op(e0,e2) = e0 | op(e1,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c35, plain, op(e0,e2) = e1 | op(e1,e2) = e1 | op(e2,e2) = e1 | op(e3,e2) = e1, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c40, plain, op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c41, plain, op(e0,e3) = e0 | op(e1,e3) = e0 | op(e2,e3) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c42, plain, op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c44, plain, op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c45, plain, op(e0,e3) = e2 | op(e1,e3) = e2 | op(e2,e3) = e2 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c46, plain, op(e3,e0) = e3 | op(e3,e1) = e3 | op(e3,e2) = e3 | op(e3,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 104.92/21.68 cnf(c48, plain, op(e0,e0) != op(e1,e0), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c49, plain, op(e0,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c50, plain, op(e0,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c51, plain, op(e1,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c53, plain, op(e2,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c54, plain, op(e0,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c57, plain, op(e1,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c58, plain, op(e1,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c60, plain, op(e0,e2) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c61, plain, op(e0,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c62, plain, op(e0,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c63, plain, op(e1,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c64, plain, op(e1,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c65, plain, op(e2,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c67, plain, op(e0,e3) != op(e2,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c70, plain, op(e1,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c73, plain, op(e0,e0) != op(e0,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c78, plain, op(e1,e0) != op(e1,e1), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c79, plain, op(e1,e0) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c80, plain, op(e1,e0) != op(e1,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c81, plain, op(e1,e1) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c82, plain, op(e1,e1) != op(e1,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c85, plain, op(e2,e0) != op(e2,e2), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c86, plain, op(e2,e0) != op(e2,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c89, plain, op(e2,e2) != op(e2,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c92, plain, op(e3,e0) != op(e3,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c95, plain, op(e3,e2) != op(e3,e3), inference(clausification, [status(esa)], [ax3])). % 104.92/21.68 cnf(c96, plain, e0 != e1, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c97, plain, e0 != e2, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c98, plain, e0 != e3, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c99, plain, e1 != e2, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c100, plain, e1 != e3, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c101, plain, e2 != e3, inference(clausification, [status(esa)], [ax4])). % 104.92/21.68 cnf(c102, plain, op(e0,e0) = e0 | op(e1,e1) = e0 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c103, plain, op(e0,e0) = e0 | op(e0,e0) != e1 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c104, plain, op(e0,e0) != e0 | op(e1,e1) = e0 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c106, plain, op(e0,e0) = e1 | op(e1,e1) = e1 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c107, plain, op(e0,e0) = e1 | op(e1,e1) != e1 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c108, plain, op(e1,e1) != e0 | op(e1,e1) = e1 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c110, plain, op(e0,e0) = e2 | op(e1,e1) = e2 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c111, plain, op(e0,e0) = e2 | op(e2,e2) != e1 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c112, plain, op(e2,e2) != e0 | op(e1,e1) = e2 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c114, plain, op(e0,e0) = e3 | op(e1,e1) = e3 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c116, plain, op(e3,e3) != e0 | op(e1,e1) = e3 | X0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c118, plain, ~X0 | op(e2,e2) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c119, plain, ~X0 | op(e2,e2) = e0 | op(e0,e0) != e3, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c120, plain, ~X0 | op(e0,e0) != e2 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c122, plain, ~X0 | op(e2,e2) = e1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c124, plain, ~X0 | op(e1,e1) != e2 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c126, plain, ~X0 | op(e2,e2) = e2 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c127, plain, ~X0 | op(e2,e2) = e2 | op(e2,e2) != e3, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c128, plain, ~X0 | op(e2,e2) != e2 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c130, plain, ~X0 | op(e2,e2) = e3 | op(e3,e3) = e3, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c131, plain, ~X0 | op(e2,e2) = e3 | op(e3,e3) != e3, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c132, plain, ~X0 | op(e3,e3) != e2 | op(e3,e3) = e3, inference(clausification, [status(esa)], [ax5])). % 104.92/21.68 cnf(c134, plain, e0 != op(op(e2,e2),e2) | e1 != op(op(e2,e2),op(e2,e2)) | e3 != op(e2,e2), inference(clausification, [status(esa)], [ax6])). % 104.92/21.68 cnf(c135, plain, e0 != op(op(e3,e3),e3) | e1 != op(op(e3,e3),op(e3,e3)) | e2 != op(e3,e3), inference(clausification, [status(esa)], [ax7])). % 104.92/21.68 cnf(c139, plain, e0 != op(op(e2,e2),e2) | e3 != op(op(e2,e2),op(e2,e2)) | e1 != op(e2,e2), inference(clausification, [status(esa)], [ax11])). % 104.92/21.68 cnf(c140, plain, e1 != op(op(e2,e2),e2) | e0 != op(op(e2,e2),op(e2,e2)) | e3 != op(e2,e2), inference(clausification, [status(esa)], [ax12])). % 104.92/21.68 cnf(c142, plain, e1 != op(op(e0,e0),e0) | e2 != op(op(e0,e0),op(e0,e0)) | e3 != op(e0,e0), inference(clausification, [status(esa)], [ax14])). % 104.92/21.68 cnf(c144, plain, e1 != op(op(e0,e0),e0) | e3 != op(op(e0,e0),op(e0,e0)) | e2 != op(e0,e0), inference(clausification, [status(esa)], [ax16])). % 104.92/21.68 cnf(c145, plain, e1 != op(op(e2,e2),e2) | e3 != op(op(e2,e2),op(e2,e2)) | e0 != op(e2,e2), inference(clausification, [status(esa)], [ax17])). % 104.92/21.68 cnf(c146, plain, e2 != op(op(e1,e1),e1) | e0 != op(op(e1,e1),op(e1,e1)) | e3 != op(e1,e1), inference(clausification, [status(esa)], [ax18])). % 104.92/21.68 cnf(c148, plain, e2 != op(op(e0,e0),e0) | e1 != op(op(e0,e0),op(e0,e0)) | e3 != op(e0,e0), inference(clausification, [status(esa)], [ax20])). % 104.92/21.68 cnf(c149, plain, e2 != op(op(e3,e3),e3) | e1 != op(op(e3,e3),op(e3,e3)) | e0 != op(e3,e3), inference(clausification, [status(esa)], [ax21])). % 104.92/21.68 cnf(c150, plain, e2 != op(op(e0,e0),e0) | e3 != op(op(e0,e0),op(e0,e0)) | e1 != op(e0,e0), inference(clausification, [status(esa)], [ax22])). % 104.92/21.68 cnf(c155, plain, e3 != op(op(e2,e2),e2) | e1 != op(op(e2,e2),op(e2,e2)) | e0 != op(e2,e2), inference(clausification, [status(esa)], [ax27])). % 104.92/21.68 cnf(d0, plain, e2 = e3 | op(e0,e0) = e3 | 'Ts3' | op(e0,e0) = e2 | 'Ts2', inference(superposition, [status(thm)], [c110,c114])). % 104.92/21.68 cnf(d1, plain, op(e0,e0) = e2 | op(e0,e0) = e3 | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c101,d0])). % 104.92/21.68 cnf(d2, plain, e3 != e3 | op(e2,e2) = e0 | ~'Ts0' | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,c119])). % 104.92/21.68 cnf(d3, plain, op(e0,e0) = e2 | op(e2,e2) = e0 | ~'Ts0' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d2])). % 104.92/21.68 cnf(d4, plain, e3 != op(e0,op(e2,e2)) | e0 != op(e2,e2) | e1 != op(op(e2,e2),e2) | op(e0,e0) = e2 | ~'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d3,c145])). % 104.92/21.68 cnf(d5, plain, e3 != op(e0,e0) | op(e0,e0) = e2 | e0 != op(e2,e2) | e1 != op(op(e2,e2),e2) | ~'Ts0' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | ~'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d3,d4])). % 104.92/21.68 cnf(d6, plain, e1 != op(e0,e2) | op(e0,e0) = e2 | e0 != op(e2,e2) | e3 != op(e0,e0) | ~'Ts0' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | ~'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d3,d5])). % 104.92/21.68 cnf(d7, plain, e3 != e3 | op(e0,e0) = e2 | e0 != op(e2,e2) | e1 != op(e0,e2) | ~'Ts0' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,d6])). % 104.92/21.68 cnf(d8, plain, op(e1,e0) != e2 | op(e0,e0) = e2 | 'Ts2', inference(superposition, [status(thm)], [c110,c78])). % 104.92/21.68 cnf(d9, plain, e1 != op(e3,op(e0,e0)) | e2 != op(op(e0,e0),e0) | e3 != op(e0,e0) | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,c148])). % 104.92/21.68 cnf(d10, plain, e1 != op(e3,e3) | op(e0,e0) = e2 | e2 != op(op(e0,e0),e0) | e3 != op(e0,e0) | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,d9])). % 104.92/21.68 cnf(d11, plain, e2 != op(e3,e0) | op(e0,e0) = e2 | e1 != op(e3,e3) | e3 != op(e0,e0) | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,d10])). % 104.92/21.68 cnf(d12, plain, e3 != e3 | op(e0,e0) = e2 | e2 != op(e3,e0) | e1 != op(e3,e3) | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,d11])). % 104.92/21.68 cnf(d13, plain, e2 != e2 | op(e3,e3) = e1 | ~'Ts1' | op(e0,e0) = e2 | 'Ts2', inference(superposition, [status(thm)], [c110,c124])). % 104.92/21.68 cnf(d14, plain, op(e0,e0) = e2 | op(e3,e3) = e1 | ~'Ts1' | 'Ts2', inference(equality_resolution, [status(thm)], [d13])). % 104.92/21.68 cnf(d15, plain, e1 != e1 | op(e0,e0) = e2 | e2 != op(e3,e0) | e3 != e3 | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | ~'Ts1' | 'Ts2', inference(superposition, [status(thm)], [d14,d12])). % 104.92/21.68 cnf(d16, plain, op(e3,e0) != e1 | op(e0,e0) = e2 | ~'Ts1' | 'Ts2', inference(superposition, [status(thm)], [d14,c92])). % 104.92/21.68 cnf(d17, plain, op(e0,e0) != e3 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e3,e0) = e1, inference(superposition, [status(thm)], [c12,c50])). % 104.92/21.68 cnf(d18, plain, e3 != e3 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e0,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d1,d17])). % 104.92/21.68 cnf(d19, plain, op(e0,e0) = e2 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e3,e0) = e1 | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d18])). % 104.92/21.68 cnf(d20, plain, e1 != e1 | op(e0,e0) = e2 | ~'Ts1' | 'Ts2' | op(e0,e0) = e2 | op(e3,e0) = e0 | op(e3,e0) = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d19,d16])). % 104.92/21.68 cnf(d21, plain, op(e0,e0) = e2 | op(e3,e0) = e0 | op(e3,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d20])). % 104.92/21.68 cnf(d22, plain, e2 != e2 | op(e0,e0) = e2 | e1 != e1 | e3 != e3 | ~'Ts1' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | op(e3,e0) = e0 | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d21,d15])). % 104.92/21.68 cnf(d23, plain, op(e0,e0) = e2 | op(e3,e0) = e0 | e2 != e2 | e1 != e1 | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d22])). % 104.92/21.68 cnf(d24, plain, op(e0,e0) = e2 | op(e3,e0) = e0 | e2 != e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d23])). % 104.92/21.68 cnf(d25, plain, op(e0,e0) = e2 | op(e3,e0) = e0 | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d24])). % 104.92/21.68 cnf(d26, plain, e0 = e2 | op(e0,e0) = e2 | op(e2,e0) = e2 | op(e1,e0) = e2 | op(e0,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d25,c21])). % 104.92/21.68 cnf(d27, plain, op(e0,e0) = e2 | op(e2,e0) = e2 | op(e1,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c97,d26])). % 104.92/21.68 cnf(d28, plain, e2 != e2 | op(e0,e0) = e2 | 'Ts2' | op(e0,e0) = e2 | op(e2,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d27,d8])). % 104.92/21.68 cnf(d29, plain, op(e0,e0) = e2 | op(e2,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d28])). % 104.92/21.68 cnf(d30, plain, op(e3,e2) != e1 | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,c95])). % 104.92/21.68 cnf(d31, plain, e1 != e1 | op(e2,e2) = e1 | ~'Ts1' | op(e0,e2) = e1 | op(e2,e2) = e1 | op(e1,e2) = e1, inference(superposition, [status(thm)], [c35,d30])). % 104.92/21.68 cnf(d32, plain, op(e0,e2) = e1 | op(e2,e2) = e1 | op(e1,e2) = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d31])). % 104.92/21.68 cnf(d33, plain, op(e1,e0) != e1 | op(e0,e2) = e1 | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d32,c79])). % 104.92/21.68 cnf(d34, plain, op(e3,e0) != e1 | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,c92])). % 104.92/21.68 cnf(d35, plain, e1 != e1 | op(e2,e2) = e1 | ~'Ts1' | op(e0,e0) = e1 | op(e2,e0) = e1 | op(e1,e0) = e1, inference(superposition, [status(thm)], [c19,d34])). % 104.92/21.68 cnf(d36, plain, op(e0,e0) = e1 | op(e2,e0) = e1 | op(e2,e2) = e1 | op(e1,e0) = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d35])). % 104.92/21.68 cnf(d37, plain, e1 != e1 | op(e0,e2) = e1 | op(e2,e2) = e1 | ~'Ts1' | op(e0,e0) = e1 | op(e2,e0) = e1 | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d36,d33])). % 104.92/21.68 cnf(d38, plain, op(e0,e0) = e1 | op(e0,e2) = e1 | op(e2,e0) = e1 | op(e2,e2) = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d37])). % 104.92/21.68 cnf(d39, plain, e1 != e1 | op(e0,e0) = e2 | 'Ts2' | op(e0,e0) = e1 | op(e0,e2) = e1 | op(e2,e0) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d38,c111])). % 104.92/21.68 cnf(d40, plain, op(e0,e0) = e2 | op(e0,e0) = e1 | op(e0,e2) = e1 | op(e2,e0) = e1 | ~'Ts1' | 'Ts2', inference(equality_resolution, [status(thm)], [d39])). % 104.92/21.68 cnf(d41, plain, e1 = e2 | op(e0,e0) = e2 | ~'Ts1' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | op(e0,e0) = e1 | op(e0,e2) = e1 | ~'Ts1' | 'Ts2', inference(superposition, [status(thm)], [d40,d29])). % 104.92/21.68 cnf(d42, plain, op(e0,e0) = e2 | op(e0,e0) = e1 | op(e0,e2) = e1 | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c99,d41])). % 104.92/21.68 cnf(d43, plain, e1 != e1 | op(e0,e0) = e2 | e0 != op(e2,e2) | e3 != e3 | ~'Ts0' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | op(e0,e0) = e1 | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d42,d7])). % 104.92/21.68 cnf(d44, plain, e0 != e0 | op(e0,e0) = e2 | op(e0,e0) = e1 | e1 != e1 | e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | ~'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d3,d43])). % 104.92/21.68 cnf(d45, plain, op(e0,e0) = e2 | op(e0,e0) = e1 | e0 != e0 | e1 != e1 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d44])). % 104.92/21.68 cnf(d46, plain, op(e0,e0) = e2 | op(e0,e0) = e1 | e0 != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d45])). % 104.92/21.68 cnf(d47, plain, op(e0,e0) = e2 | op(e0,e0) = e1 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d46])). % 104.92/21.68 cnf(d48, plain, e1 = e3 | op(e0,e0) = e2 | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d47,d1])). % 104.92/21.68 cnf(d49, plain, op(e0,e0) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c100,d48])). % 104.92/21.68 cnf(d50, plain, e2 != e2 | op(e3,e3) = e0 | ~'Ts0' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d49,c120])). % 104.92/21.68 cnf(d51, plain, op(e3,e3) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d50])). % 104.92/21.68 cnf(d52, plain, e0 != e0 | op(e1,e1) = e3 | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,c116])). % 104.92/21.68 cnf(d53, plain, op(e1,e1) = e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d52])). % 104.92/21.68 cnf(d54, plain, e0 != op(e3,op(e1,e1)) | e2 != op(op(e1,e1),e1) | e3 != op(e1,e1) | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d53,c146])). % 104.92/21.68 cnf(d55, plain, e2 != op(e3,e1) | e0 != op(e3,op(e1,e1)) | e3 != op(e1,e1) | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d53,d54])). % 104.92/21.68 cnf(d56, plain, e0 != op(e3,e3) | e2 != op(e3,e1) | e3 != op(e1,e1) | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d53,d55])). % 104.92/21.68 cnf(d57, plain, e3 != e3 | e0 != op(e3,e3) | e2 != op(e3,e1) | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d53,d56])). % 104.92/21.68 cnf(d58, plain, e0 = e2 | op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e1) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,c44])). % 104.92/21.68 cnf(d59, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e1) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c97,d58])). % 104.92/21.68 cnf(d60, plain, e2 != e2 | e0 != op(e3,e3) | e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e3,e0) = e2 | op(e3,e2) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d59,d57])). % 104.92/21.68 cnf(d61, plain, e0 != e0 | op(e3,e0) = e2 | op(e3,e2) = e2 | e2 != e2 | e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,d60])). % 104.92/21.68 cnf(d62, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | e0 != e0 | e2 != e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d61])). % 104.92/21.68 cnf(d63, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | e0 != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d62])). % 104.92/21.68 cnf(d64, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d63])). % 104.92/21.68 cnf(d65, plain, op(e1,e2) != e2 | op(e3,e0) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d64,c64])). % 104.92/21.68 cnf(d66, plain, e3 != op(e1,e2) | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d53,c81])). % 104.92/21.68 cnf(d67, plain, e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e1,e2) = e0 | op(e1,e2) = e2 | op(e1,e2) = e1, inference(superposition, [status(thm)], [c6,d66])). % 104.92/21.68 cnf(d68, plain, op(e1,e2) = e0 | op(e1,e2) = e2 | op(e1,e2) = e1 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d67])). % 104.92/21.68 cnf(d69, plain, e1 != op(e2,e2) | op(e1,e2) = e0 | op(e1,e2) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d68,c63])). % 104.92/21.68 cnf(d70, plain, e0 = e1 | op(e2,e2) = e1 | ~'Ts1' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,c122])). % 104.92/21.68 cnf(d71, plain, op(e2,e2) = e1 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c96,d70])). % 104.92/21.68 cnf(d72, plain, e1 != e1 | op(e1,e2) = e0 | op(e1,e2) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d71,d69])). % 104.92/21.68 cnf(d73, plain, op(e1,e2) = e0 | op(e1,e2) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d72])). % 104.92/21.68 cnf(d74, plain, e2 != e2 | op(e3,e0) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d73,d65])). % 104.92/21.68 cnf(d75, plain, op(e1,e2) = e0 | op(e3,e0) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d74])). % 104.92/21.68 cnf(d76, plain, op(e0,e0) != e2 | op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d75,c50])). % 104.92/21.68 cnf(d77, plain, e2 != e2 | op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d49,d76])). % 104.92/21.68 cnf(d78, plain, op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d77])). % 104.92/21.68 cnf(d79, plain, op(e1,e0) != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d78,c79])). % 104.92/21.68 cnf(d80, plain, op(e1,e3) != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,c70])). % 104.92/21.68 cnf(d81, plain, e0 != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0, inference(superposition, [status(thm)], [c24,d80])). % 104.92/21.68 cnf(d82, plain, op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d81])). % 104.92/21.68 cnf(d83, plain, e0 = e3 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d82,d53])). % 104.92/21.68 cnf(d84, plain, op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c98,d83])). % 104.92/21.68 cnf(d85, plain, op(e0,e2) != e0 | op(e1,e0) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d84,c60])). % 104.92/21.68 cnf(d86, plain, e0 = e1 | op(e2,e2) = e1 | ~'Ts1' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c122])). % 104.92/21.68 cnf(d87, plain, op(e2,e2) = e0 | op(e2,e2) = e1 | ~'Ts0' | ~'Ts1', inference(resolution, [status(thm)], [c96,d86])). % 104.92/21.68 cnf(d88, plain, e3 != op(e1,op(e2,e2)) | e0 != op(op(e2,e2),e2) | e1 != op(e2,e2) | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d87,c139])). % 104.92/21.68 cnf(d89, plain, e3 != op(e1,e1) | op(e2,e2) = e0 | e0 != op(op(e2,e2),e2) | e1 != op(e2,e2) | ~'Ts0' | ~'Ts1' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d87,d88])). % 104.92/21.68 cnf(d90, plain, e0 != op(e1,e2) | op(e2,e2) = e0 | e1 != op(e2,e2) | e3 != op(e1,e1) | ~'Ts0' | ~'Ts1' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d87,d89])). % 104.92/21.68 cnf(d91, plain, e0 != e0 | op(e1,e1) = e3 | 'Ts3' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c116])). % 104.92/21.68 cnf(d92, plain, op(e2,e2) = e0 | op(e1,e1) = e3 | ~'Ts0' | 'Ts3', inference(equality_resolution, [status(thm)], [d91])). % 104.92/21.68 cnf(d93, plain, e3 != e3 | op(e2,e2) = e0 | e0 != op(e1,e2) | e1 != op(e2,e2) | ~'Ts0' | ~'Ts1' | op(e2,e2) = e0 | ~'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d92,d90])). % 104.92/21.68 cnf(d94, plain, e1 != e1 | op(e2,e2) = e0 | e0 != op(e1,e2) | e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts3' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d87,d93])). % 104.92/21.68 cnf(d95, plain, op(e3,e2) != e0 | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c95])). % 104.92/21.68 cnf(d96, plain, e0 != e0 | op(e2,e2) = e0 | ~'Ts0' | op(e0,e2) = e0 | op(e2,e2) = e0 | op(e1,e2) = e0, inference(superposition, [status(thm)], [c33,d95])). % 104.92/21.68 cnf(d97, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | op(e1,e2) = e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d96])). % 104.92/21.68 cnf(d98, plain, e0 != e0 | op(e2,e2) = e0 | e1 != e1 | e3 != e3 | ~'Ts0' | ~'Ts1' | 'Ts3' | op(e0,e2) = e0 | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d97,d94])). % 104.92/21.68 cnf(d99, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | e0 != e0 | e1 != e1 | ~'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d98])). % 104.92/21.68 cnf(d100, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | e0 != e0 | ~'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d99])). % 104.92/21.68 cnf(d101, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d100])). % 104.92/21.68 cnf(d102, plain, e0 != e0 | op(e1,e1) = e2 | 'Ts2' | op(e0,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts3', inference(superposition, [status(thm)], [d101,c112])). % 104.92/21.68 cnf(d103, plain, op(e0,e2) = e0 | op(e1,e1) = e2 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d102])). % 104.92/21.68 cnf(d104, plain, e2 != e2 | op(e3,e3) = e1 | ~'Ts1' | op(e0,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d103,c124])). % 104.92/21.68 cnf(d105, plain, op(e0,e2) = e0 | op(e3,e3) = e1 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d104])). % 104.92/21.68 cnf(d106, plain, e0 = e1 | op(e0,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d51,d105])). % 104.92/21.68 cnf(d107, plain, op(e0,e2) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c96,d106])). % 104.92/21.68 cnf(d108, plain, e0 != e0 | op(e1,e0) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d107,d85])). % 104.92/21.68 cnf(d109, plain, op(e1,e0) = e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d108])). % 104.92/21.68 cnf(d110, plain, e0 != e0 | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d109,d79])). % 104.92/21.68 cnf(d111, plain, ~'Ts0' | ~'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d110])). % 104.92/21.68 cnf(d112, plain, e1 != e1 | op(e0,e0) = e1 | 'Ts1' | op(e0,e0) = e1 | 'Ts1', inference(superposition, [status(thm)], [c106,c107])). % 104.92/21.68 cnf(d113, plain, op(e0,e0) = e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d112])). % 104.92/21.68 cnf(d114, plain, e1 != e1 | op(e0,e0) = e0 | 'Ts0' | 'Ts1', inference(superposition, [status(thm)], [d113,c103])). % 104.92/21.68 cnf(d115, plain, op(e0,e0) = e0 | 'Ts0' | 'Ts1', inference(equality_resolution, [status(thm)], [d114])). % 104.92/21.68 cnf(d116, plain, e0 = e1 | 'Ts1' | 'Ts0' | 'Ts1', inference(superposition, [status(thm)], [d115,d113])). % 104.92/21.68 cnf(d117, plain, 'Ts0' | 'Ts1', inference(resolution, [status(thm)], [c96,d116])). % 104.92/21.68 cnf(d118, plain, e0 = e2 | op(e0,e0) = e2 | 'Ts2' | op(e0,e0) = e0 | 'Ts0', inference(superposition, [status(thm)], [c102,c110])). % 104.92/21.68 cnf(d119, plain, op(e0,e0) = e0 | op(e0,e0) = e2 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [c97,d118])). % 104.92/21.68 cnf(d120, plain, e3 = e0 | op(e0,e0) = e0 | 'Ts0' | op(e0,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [c114,c102])). % 104.92/21.68 cnf(d121, plain, e3 = e2 | op(e0,e0) = e0 | 'Ts0' | 'Ts2' | op(e0,e0) = e0 | e3 = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d120,d119])). % 104.92/21.68 cnf(d122, plain, e3 = e2 | op(e0,e0) = e2 | 'Ts2' | op(e0,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [c114,c110])). % 104.92/21.68 cnf(d123, plain, e3 = e0 | e3 = e0 | e3 = e2 | 'Ts0' | 'Ts2' | 'Ts3' | op(e0,e0) = e2 | e3 = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d122,d121])). % 104.92/21.68 cnf(d124, plain, e2 = e3 | op(e0,e0) = e0 | e3 = e0 | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,d120])). % 104.92/21.68 cnf(d125, plain, op(e0,e0) = e0 | e3 = e0 | 'Ts0' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c101,d124])). % 104.92/21.68 cnf(d126, plain, e0 = e2 | e3 = e0 | e3 = e2 | 'Ts0' | 'Ts2' | 'Ts3' | e3 = e0 | 'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d125,d123])). % 104.92/21.68 cnf(d127, plain, e3 = e0 | e3 = e2 | 'Ts0' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c97,d126])). % 104.92/21.68 cnf(d128, plain, e2 != e2 | e3 = e0 | 'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d127,c101])). % 104.92/21.68 cnf(d129, plain, e3 = e0 | 'Ts0' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d128])). % 104.92/21.68 cnf(d130, plain, e0 != e0 | 'Ts0' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d129,c98])). % 104.92/21.68 cnf(d131, plain, 'Ts0' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d130])). % 104.92/21.68 cnf(d132, plain, e3 != e3 | op(e2,e2) = e3 | ~'Ts3' | op(e2,e2) = e3 | ~'Ts3', inference(superposition, [status(thm)], [c130,c131])). % 104.92/21.68 cnf(d133, plain, op(e2,e2) = e3 | ~'Ts3', inference(equality_resolution, [status(thm)], [d132])). % 104.92/21.68 cnf(d134, plain, e1 != op(e3,op(e2,e2)) | e0 != op(op(e2,e2),e2) | e3 != op(e2,e2) | ~'Ts3', inference(superposition, [status(thm)], [d133,c134])). % 104.92/21.68 cnf(d135, plain, e1 != op(e3,e3) | e0 != op(op(e2,e2),e2) | e3 != op(e2,e2) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d134])). % 104.92/21.68 cnf(d136, plain, e0 != op(e3,e2) | e1 != op(e3,e3) | e3 != op(e2,e2) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d135])). % 104.92/21.68 cnf(d137, plain, e3 != e3 | e0 != op(e3,e2) | e1 != op(e3,e3) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d136])). % 104.92/21.68 cnf(d138, plain, e1 != e1 | e0 != op(e3,e2) | e3 != e3 | ~'Ts3' | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,d137])). % 104.92/21.68 cnf(d139, plain, e0 = e1 | op(e2,e2) = e1 | ~'Ts1' | op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c40,c122])). % 104.92/21.68 cnf(d140, plain, op(e2,e2) = e1 | op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | ~'Ts1', inference(resolution, [status(thm)], [c96,d139])). % 104.92/21.68 cnf(d141, plain, op(e1,e1) != e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d140,c58])). % 104.92/21.68 cnf(d142, plain, e0 != e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts1' | op(e0,e0) = e0 | 'Ts0', inference(superposition, [status(thm)], [c102,d141])). % 104.92/21.68 cnf(d143, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | op(e3,e2) = e0 | 'Ts0' | ~'Ts1', inference(equality_resolution, [status(thm)], [d142])). % 104.92/21.68 cnf(d144, plain, e0 != e0 | op(e2,e2) = e1 | e1 != e1 | e3 != e3 | ~'Ts1' | ~'Ts3' | op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | 'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d143,d138])). % 104.92/21.68 cnf(d145, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | e0 != e0 | e1 != e1 | 'Ts0' | ~'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d144])). % 104.92/21.68 cnf(d146, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | e0 != e0 | 'Ts0' | ~'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d145])). % 104.92/21.68 cnf(d147, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d146])). % 104.92/21.68 cnf(d148, plain, op(e2,e0) != e0 | op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d147,c53])). % 104.92/21.68 cnf(d149, plain, e3 != op(e2,op(e0,e0)) | e2 != op(e0,e0) | e1 != op(op(e0,e0),e0) | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,c144])). % 104.92/21.68 cnf(d150, plain, e3 != op(e2,e2) | op(e0,e0) = e0 | e2 != op(e0,e0) | e1 != op(op(e0,e0),e0) | 'Ts0' | 'Ts2' | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,d149])). % 104.92/21.68 cnf(d151, plain, e1 != op(e2,e0) | op(e0,e0) = e0 | e2 != op(e0,e0) | e3 != op(e2,e2) | 'Ts0' | 'Ts2' | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,d150])). % 104.92/21.68 cnf(d152, plain, e3 != e3 | op(e0,e0) = e0 | e2 != op(e0,e0) | e1 != op(e2,e0) | 'Ts0' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d133,d151])). % 104.92/21.68 cnf(d153, plain, op(e2,e0) != e3 | ~'Ts3', inference(superposition, [status(thm)], [d133,c85])). % 104.92/21.68 cnf(d154, plain, e3 != e3 | ~'Ts3' | op(e2,e0) = e0 | op(e2,e0) = e2 | op(e2,e0) = e1, inference(superposition, [status(thm)], [c8,d153])). % 104.92/21.68 cnf(d155, plain, op(e2,e0) = e0 | op(e2,e0) = e2 | op(e2,e0) = e1 | ~'Ts3', inference(equality_resolution, [status(thm)], [d154])). % 104.92/21.68 cnf(d156, plain, e1 != e1 | op(e0,e0) = e0 | e2 != op(e0,e0) | e3 != e3 | 'Ts0' | 'Ts2' | ~'Ts3' | op(e2,e0) = e0 | op(e2,e0) = e2 | ~'Ts3', inference(superposition, [status(thm)], [d155,d152])). % 104.92/21.68 cnf(d157, plain, e2 != e2 | op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e0) = e2 | e1 != e1 | e3 != e3 | 'Ts0' | 'Ts2' | ~'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,d156])). % 104.92/21.68 cnf(d158, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e0) = e2 | e2 != e2 | e1 != e1 | 'Ts0' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d157])). % 104.92/21.68 cnf(d159, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e0) = e2 | e2 != e2 | 'Ts0' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d158])). % 104.92/21.68 cnf(d160, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e0) = e2 | 'Ts0' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d159])). % 104.92/21.68 cnf(d161, plain, op(e0,e0) != e2 | op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d160,c49])). % 104.92/21.68 cnf(d162, plain, e2 != e2 | op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | 'Ts2' | ~'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d119,d161])). % 104.92/21.68 cnf(d163, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d162])). % 104.92/21.68 cnf(d164, plain, e0 != e0 | op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | ~'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d163,d148])). % 104.92/21.68 cnf(d165, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d164])). % 104.92/21.68 cnf(d166, plain, e1 = e3 | ~'Ts3' | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d165,d133])). % 104.92/21.68 cnf(d167, plain, op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c100,d166])). % 104.92/21.68 cnf(d168, plain, e0 != e0 | op(e1,e1) = e0 | 'Ts0' | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d167,c104])). % 104.92/21.68 cnf(d169, plain, op(e1,e1) = e0 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d168])). % 104.92/21.68 cnf(d170, plain, e0 = e2 | op(e0,e0) = e2 | 'Ts2' | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d169,c110])). % 104.92/21.68 cnf(d171, plain, op(e0,e0) = e2 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c97,d170])). % 104.92/21.68 cnf(d172, plain, e0 = e2 | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3' | 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d167,d171])). % 104.92/21.68 cnf(d173, plain, 'Ts0' | ~'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c97,d172])). % 104.92/21.68 cnf(d174, plain, 'Ts0' | ~'Ts1' | 'Ts2' | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d173,d131])). % 104.92/21.68 cnf(d175, plain, 'Ts0' | 'Ts2' | 'Ts0', inference(resolution, [status(thm)], [d174,d117])). % 104.92/21.68 cnf(d176, plain, e3 != e3 | op(e2,e2) = e2 | ~'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d133,c127])). % 104.92/21.68 cnf(d177, plain, op(e2,e2) = e2 | ~'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d176])). % 104.92/21.68 cnf(d178, plain, e2 = e3 | ~'Ts3' | ~'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d177,d133])). % 104.92/21.68 cnf(d179, plain, ~'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c101,d178])). % 104.92/21.68 cnf(d180, plain, e0 = e3 | op(e0,e0) = e3 | 'Ts3' | op(e0,e0) = e0 | 'Ts0', inference(superposition, [status(thm)], [c102,c114])). % 104.92/21.68 cnf(d181, plain, op(e0,e0) = e0 | op(e0,e0) = e3 | 'Ts0' | 'Ts3', inference(resolution, [status(thm)], [c98,d180])). % 104.92/21.68 cnf(d182, plain, e2 != op(e3,op(e0,e0)) | e1 != op(op(e0,e0),e0) | e3 != op(e0,e0) | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,c142])). % 104.92/21.68 cnf(d183, plain, e1 != op(e3,e0) | op(e0,e0) = e0 | e2 != op(e3,op(e0,e0)) | e3 != op(e0,e0) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d182])). % 104.92/21.68 cnf(d184, plain, e2 != op(e3,e3) | op(e0,e0) = e0 | e1 != op(e3,e0) | e3 != op(e0,e0) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d183])). % 104.92/21.68 cnf(d185, plain, e3 != e3 | op(e0,e0) = e0 | e2 != op(e3,e3) | e1 != op(e3,e0) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d184])). % 104.92/21.68 cnf(d186, plain, e2 = e3 | op(e3,e0) = e3 | op(e3,e2) = e3 | op(e3,e1) = e3 | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,c46])). % 104.92/21.68 cnf(d187, plain, op(e2,e2) = e2 | op(e3,e0) = e3 | op(e3,e2) = e3 | op(e3,e1) = e3 | ~'Ts2', inference(resolution, [status(thm)], [c101,d186])). % 104.92/21.68 cnf(d188, plain, e1 = e2 | op(e2,e2) = e2 | ~'Ts2' | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(superposition, [status(thm)], [c42,c126])). % 104.92/21.68 cnf(d189, plain, op(e2,e2) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1 | ~'Ts2', inference(resolution, [status(thm)], [c99,d188])). % 104.92/21.68 cnf(d190, plain, e1 = e3 | op(e2,e2) = e2 | op(e3,e0) = e3 | op(e3,e2) = e3 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d189,d187])). % 104.92/21.68 cnf(d191, plain, op(e2,e2) = e2 | op(e3,e0) = e1 | op(e3,e0) = e3 | op(e3,e2) = e1 | op(e3,e2) = e3 | ~'Ts2', inference(resolution, [status(thm)], [c100,d190])). % 104.92/21.68 cnf(d192, plain, e0 = e2 | op(e2,e2) = e2 | ~'Ts2' | op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c40,c126])). % 104.92/21.68 cnf(d193, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | ~'Ts2', inference(resolution, [status(thm)], [c97,d192])). % 104.92/21.68 cnf(d194, plain, e0 = e3 | op(e2,e2) = e2 | op(e3,e0) = e3 | op(e3,e2) = e3 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d193,d187])). % 104.92/21.68 cnf(d195, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e3 | op(e3,e2) = e0 | op(e3,e2) = e3 | ~'Ts2', inference(resolution, [status(thm)], [c98,d194])). % 104.92/21.68 cnf(d196, plain, e0 = e1 | op(e2,e2) = e2 | op(e3,e0) = e1 | op(e3,e2) = e1 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d193,d189])). % 104.92/21.68 cnf(d197, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e2) = e0 | op(e3,e2) = e1 | ~'Ts2', inference(resolution, [status(thm)], [c96,d196])). % 104.92/21.68 cnf(d198, plain, e1 = e3 | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e3 | op(e3,e2) = e0 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e2) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d197,d195])). % 104.92/21.68 cnf(d199, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | op(e3,e2) = e0 | ~'Ts2', inference(resolution, [status(thm)], [c100,d198])). % 104.92/21.68 cnf(d200, plain, e0 = e3 | op(e2,e2) = e2 | op(e3,e0) = e1 | op(e3,e0) = e3 | op(e3,e2) = e1 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | ~'Ts2', inference(superposition, [status(thm)], [d199,d191])). % 104.92/21.68 cnf(d201, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | op(e3,e2) = e1 | ~'Ts2', inference(resolution, [status(thm)], [c98,d200])). % 104.92/21.68 cnf(d202, plain, e0 = e1 | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | ~'Ts2' | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | ~'Ts2', inference(superposition, [status(thm)], [d199,d201])). % 104.92/21.68 cnf(d203, plain, op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e3 | ~'Ts2', inference(resolution, [status(thm)], [c96,d202])). % 104.92/21.68 cnf(d204, plain, op(e0,e0) != e3 | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d203,c50])). % 104.92/21.68 cnf(d205, plain, e3 != e3 | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | ~'Ts2' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d204])). % 104.92/21.68 cnf(d206, plain, op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | op(e3,e0) = e1 | 'Ts0' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d205])). % 104.92/21.68 cnf(d207, plain, e1 != e1 | op(e0,e0) = e0 | e2 != op(e3,e3) | e3 != e3 | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | 'Ts0' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d206,d185])). % 104.92/21.68 cnf(d208, plain, e2 != e2 | op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | e1 != e1 | e3 != e3 | 'Ts0' | ~'Ts2' | 'Ts3' | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,d207])). % 104.92/21.68 cnf(d209, plain, op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | e2 != e2 | e1 != e1 | 'Ts0' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d208])). % 104.92/21.68 cnf(d210, plain, op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | e2 != e2 | 'Ts0' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d209])). % 104.92/21.68 cnf(d211, plain, op(e0,e0) = e0 | op(e2,e2) = e2 | op(e3,e0) = e0 | 'Ts0' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d210])). % 104.92/21.68 cnf(d212, plain, op(e2,e0) != e0 | op(e0,e0) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d211,c53])). % 104.92/21.68 cnf(d213, plain, e1 = e2 | op(e2,e2) = e2 | ~'Ts2' | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,c126])). % 104.92/21.68 cnf(d214, plain, op(e2,e2) = e2 | op(e2,e2) = e1 | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c99,d213])). % 104.92/21.68 cnf(d215, plain, e0 != op(e2,e1) | op(e0,e0) = e0 | 'Ts0', inference(superposition, [status(thm)], [c102,c57])). % 104.92/21.68 cnf(d216, plain, op(e0,e3) != e0 | op(e2,e0) = e0 | op(e2,e2) = e0 | op(e2,e1) = e0, inference(superposition, [status(thm)], [c32,c67])). % 104.92/21.68 cnf(d217, plain, e1 != op(e2,op(e3,e3)) | e0 != op(op(e3,e3),e3) | e2 != op(e3,e3) | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,c135])). % 104.92/21.68 cnf(d218, plain, e1 != op(e2,e2) | op(e2,e2) = e2 | e0 != op(op(e3,e3),e3) | e2 != op(e3,e3) | ~'Ts2' | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,d217])). % 104.92/21.68 cnf(d219, plain, e0 != op(e2,e3) | op(e2,e2) = e2 | e2 != op(e3,e3) | e1 != op(e2,e2) | ~'Ts2' | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,d218])). % 104.92/21.68 cnf(d220, plain, e1 != e1 | op(e2,e2) = e2 | e0 != op(e2,e3) | e2 != op(e3,e3) | ~'Ts2' | op(e2,e2) = e2 | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d214,d219])). % 104.92/21.68 cnf(d221, plain, e2 != e2 | op(e2,e2) = e2 | e0 != op(e2,e3) | e1 != e1 | ~'Ts1' | ~'Ts2' | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,d220])). % 104.92/21.68 cnf(d222, plain, e0 = e2 | op(e2,e2) = e2 | ~'Ts2' | op(e0,e3) = e0 | op(e2,e3) = e0 | op(e1,e3) = e0, inference(superposition, [status(thm)], [c41,c126])). % 104.92/21.68 cnf(d223, plain, op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | op(e1,e3) = e0 | ~'Ts2', inference(resolution, [status(thm)], [c97,d222])). % 104.92/21.68 cnf(d224, plain, op(e1,e1) != e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d223,c82])). % 104.92/21.68 cnf(d225, plain, e0 != e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | ~'Ts2' | op(e0,e0) = e0 | 'Ts0', inference(superposition, [status(thm)], [c102,d224])). % 104.92/21.68 cnf(d226, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | 'Ts0' | ~'Ts2', inference(equality_resolution, [status(thm)], [d225])). % 104.92/21.68 cnf(d227, plain, e0 != e0 | op(e2,e2) = e2 | e2 != e2 | e1 != e1 | ~'Ts1' | ~'Ts2' | op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d226,d221])). % 104.92/21.68 cnf(d228, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | e0 != e0 | e2 != e2 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d227])). % 104.92/21.68 cnf(d229, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | e0 != e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d228])). % 104.92/21.68 cnf(d230, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d229])). % 104.92/21.68 cnf(d231, plain, e2 != e2 | op(e3,e3) = e2 | ~'Ts2' | op(e0,e0) = e0 | op(e0,e3) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d230,c128])). % 104.92/21.68 cnf(d232, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e3,e3) = e2 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d231])). % 104.92/21.68 cnf(d233, plain, e1 = e2 | op(e0,e0) = e0 | op(e0,e3) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,d232])). % 104.92/21.68 cnf(d234, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c99,d233])). % 104.92/21.68 cnf(d235, plain, e1 = e2 | op(e0,e0) = e0 | op(e0,e3) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | op(e0,e0) = e0 | op(e0,e3) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d234,d230])). % 104.92/21.68 cnf(d236, plain, op(e0,e0) = e0 | op(e0,e3) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c99,d235])). % 104.92/21.68 cnf(d237, plain, e0 != e0 | op(e2,e0) = e0 | op(e2,e2) = e0 | op(e2,e1) = e0 | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d236,d216])). % 104.92/21.68 cnf(d238, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e2) = e0 | op(e2,e1) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d237])). % 104.92/21.68 cnf(d239, plain, e0 != e0 | op(e0,e0) = e0 | 'Ts0' | op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e2) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d238,d215])). % 104.92/21.68 cnf(d240, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e2) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d239])). % 104.92/21.68 cnf(d241, plain, e0 = e1 | op(e2,e2) = e2 | ~'Ts1' | ~'Ts2' | op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d240,d214])). % 104.92/21.68 cnf(d242, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c96,d241])). % 104.92/21.68 cnf(d243, plain, e0 = e2 | op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d240,d242])). % 104.92/21.68 cnf(d244, plain, op(e0,e0) = e0 | op(e2,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c97,d243])). % 104.92/21.68 cnf(d245, plain, e0 != e0 | op(e0,e0) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts2' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d244,d212])). % 104.92/21.68 cnf(d246, plain, op(e0,e0) = e0 | op(e2,e2) = e2 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d245])). % 104.92/21.68 cnf(d247, plain, e1 != op(e3,op(e0,e0)) | e2 != op(op(e0,e0),e0) | e3 != op(e0,e0) | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,c148])). % 104.92/21.68 cnf(d248, plain, e1 != op(e3,e3) | op(e0,e0) = e0 | e2 != op(op(e0,e0),e0) | e3 != op(e0,e0) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d247])). % 104.92/21.68 cnf(d249, plain, e2 != op(e3,e0) | op(e0,e0) = e0 | e1 != op(e3,e3) | e3 != op(e0,e0) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d248])). % 104.92/21.68 cnf(d250, plain, e3 != e3 | op(e0,e0) = e0 | e2 != op(e3,e0) | e1 != op(e3,e3) | 'Ts0' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d249])). % 104.92/21.68 cnf(d251, plain, e1 != e1 | op(e0,e0) = e0 | e2 != op(e3,e0) | e3 != e3 | 'Ts0' | 'Ts3' | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,d250])). % 104.92/21.68 cnf(d252, plain, e3 != e3 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e3,e0) = e1 | op(e0,e0) = e0 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d181,d17])). % 104.92/21.68 cnf(d253, plain, op(e0,e0) = e0 | op(e3,e0) = e0 | op(e3,e0) = e2 | op(e3,e0) = e1 | 'Ts0' | 'Ts3', inference(equality_resolution, [status(thm)], [d252])). % 104.92/21.68 cnf(d254, plain, e1 != e1 | op(e2,e2) = e1 | ~'Ts1' | op(e0,e0) = e0 | op(e3,e0) = e0 | op(e3,e0) = e2 | 'Ts0' | 'Ts3', inference(superposition, [status(thm)], [d253,d34])). % 104.92/21.69 cnf(d255, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | op(e3,e0) = e2 | 'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d254])). % 104.92/21.69 cnf(d256, plain, e2 != e2 | op(e0,e0) = e0 | op(e2,e2) = e1 | e1 != e1 | e3 != e3 | 'Ts0' | ~'Ts1' | 'Ts3' | op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | 'Ts0' | ~'Ts1' | 'Ts3', inference(superposition, [status(thm)], [d255,d251])). % 104.92/21.69 cnf(d257, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | e2 != e2 | e1 != e1 | 'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d256])). % 104.92/21.69 cnf(d258, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | e2 != e2 | 'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d257])). % 104.92/21.69 cnf(d259, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | op(e3,e0) = e0 | 'Ts0' | ~'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d258])). % 104.92/21.69 cnf(d260, plain, op(e2,e0) != e0 | op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | 'Ts3', inference(superposition, [status(thm)], [d259,c53])). % 104.92/21.69 cnf(d261, plain, e0 != e0 | op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d244,d260])). % 104.92/21.69 cnf(d262, plain, op(e0,e0) = e0 | op(e2,e2) = e1 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d261])). % 104.92/21.69 cnf(d263, plain, e1 = e2 | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3' | op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d262,d246])). % 104.92/21.69 cnf(d264, plain, op(e0,e0) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c99,d263])). % 104.92/21.69 cnf(d265, plain, e0 != e0 | op(e1,e1) = e0 | 'Ts0' | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d264,c104])). % 104.92/21.69 cnf(d266, plain, op(e1,e1) = e0 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d265])). % 104.92/21.69 cnf(d267, plain, e0 = e3 | op(e0,e0) = e3 | 'Ts3' | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d266,c114])). % 104.92/21.69 cnf(d268, plain, op(e0,e0) = e3 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c98,d267])). % 104.92/21.69 cnf(d269, plain, e0 = e3 | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3' | 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d264,d268])). % 104.92/21.69 cnf(d270, plain, 'Ts0' | ~'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c98,d269])). % 104.92/21.69 cnf(d271, plain, 'Ts0' | ~'Ts1' | 'Ts3' | 'Ts0', inference(resolution, [status(thm)], [d270,d175])). % 104.92/21.69 cnf(d272, plain, 'Ts0' | 'Ts3' | 'Ts0', inference(resolution, [status(thm)], [d271,d117])). % 104.92/21.69 cnf(d273, plain, 'Ts0' | ~'Ts2', inference(resolution, [status(thm)], [d272,d179])). % 104.92/21.69 cnf(d274, plain, 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d273,d175])). % 104.92/21.69 cnf(d275, plain, ~'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [d274,d111])). % 104.92/21.69 cnf(d276, plain, e3 = e1 | 'Ts1' | op(e0,e0) = e2 | e3 = e2 | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d122,d113])). % 104.92/21.69 cnf(d277, plain, e1 = e2 | e3 = e2 | e3 = e1 | 'Ts1' | 'Ts2' | 'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d276])). % 104.92/21.69 cnf(d278, plain, e3 = e2 | e3 = e1 | 'Ts1' | 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c99,d277])). % 104.92/21.69 cnf(d279, plain, e1 != e1 | e3 = e2 | 'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d278,c100])). % 104.92/21.69 cnf(d280, plain, e3 = e2 | 'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d279])). % 104.92/21.69 cnf(d281, plain, e2 != e2 | 'Ts1' | 'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d280,c101])). % 104.92/21.69 cnf(d282, plain, 'Ts1' | 'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d281])). % 104.92/21.69 cnf(d283, plain, e1 != op(e0,op(e3,e3)) | e0 != op(e3,e3) | e2 != op(op(e3,e3),e3) | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c149])). % 104.92/21.69 cnf(d284, plain, e1 != op(e0,e0) | op(e2,e2) = e0 | e0 != op(e3,e3) | e2 != op(op(e3,e3),e3) | ~'Ts0' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,d283])). % 104.92/21.69 cnf(d285, plain, e2 != op(e0,e3) | op(e2,e2) = e0 | e0 != op(e3,e3) | e1 != op(e0,e0) | ~'Ts0' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,d284])). % 104.92/21.69 cnf(d286, plain, e1 != e1 | op(e2,e2) = e0 | e0 != op(e3,e3) | e2 != op(e0,e3) | ~'Ts0' | 'Ts1', inference(superposition, [status(thm)], [d113,d285])). % 104.92/21.69 cnf(d287, plain, op(e1,e3) != e0 | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c70])). % 104.92/21.69 cnf(d288, plain, e0 != e0 | op(e2,e2) = e0 | ~'Ts0' | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0, inference(superposition, [status(thm)], [c24,d287])). % 104.92/21.69 cnf(d289, plain, op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d288])). % 104.92/21.69 cnf(d290, plain, e0 != e0 | op(e1,e1) = e1 | 'Ts1' | op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d289,c108])). % 104.92/21.69 cnf(d291, plain, op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e1 | ~'Ts0' | 'Ts1', inference(equality_resolution, [status(thm)], [d290])). % 104.92/21.69 cnf(d292, plain, e0 = e1 | op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0' | 'Ts1' | op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d289,d291])). % 104.92/21.69 cnf(d293, plain, op(e2,e2) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | ~'Ts0' | 'Ts1', inference(resolution, [status(thm)], [c96,d292])). % 104.92/21.69 cnf(d294, plain, op(e0,e2) != e0 | op(e2,e2) = e0 | op(e1,e0) = e0 | ~'Ts0' | 'Ts1', inference(superposition, [status(thm)], [d293,c60])). % 104.92/21.69 cnf(d295, plain, e0 != op(e3,op(e2,e2)) | e1 != op(op(e2,e2),e2) | e3 != op(e2,e2) | ~'Ts3', inference(superposition, [status(thm)], [d133,c140])). % 104.92/21.69 cnf(d296, plain, e1 != op(e3,e2) | e0 != op(e3,op(e2,e2)) | e3 != op(e2,e2) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d295])). % 104.92/21.69 cnf(d297, plain, e0 != op(e3,e3) | e1 != op(e3,e2) | e3 != op(e2,e2) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d296])). % 104.92/21.69 cnf(d298, plain, e3 != e3 | e0 != op(e3,e3) | e1 != op(e3,e2) | ~'Ts3' | ~'Ts3', inference(superposition, [status(thm)], [d133,d297])). % 104.92/21.69 cnf(d299, plain, op(e2,e2) != e3 | op(e3,e2) = e0 | op(e3,e2) = e2 | op(e3,e2) = e1, inference(superposition, [status(thm)], [c14,c65])). % 104.92/21.69 cnf(d300, plain, e3 != e3 | op(e3,e2) = e0 | op(e3,e2) = e2 | op(e3,e2) = e1 | ~'Ts3', inference(superposition, [status(thm)], [d133,d299])). % 104.92/21.69 cnf(d301, plain, op(e3,e2) = e0 | op(e3,e2) = e2 | op(e3,e2) = e1 | ~'Ts3', inference(equality_resolution, [status(thm)], [d300])). % 104.92/21.69 cnf(d302, plain, e1 != e1 | e0 != op(e3,e3) | e3 != e3 | ~'Ts3' | op(e3,e2) = e0 | op(e3,e2) = e2 | ~'Ts3', inference(superposition, [status(thm)], [d301,d298])). % 104.92/21.69 cnf(d303, plain, e0 != e0 | op(e3,e2) = e0 | op(e3,e2) = e2 | e1 != e1 | e3 != e3 | ~'Ts3' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,d302])). % 104.92/21.69 cnf(d304, plain, op(e2,e2) = e0 | op(e3,e2) = e0 | op(e3,e2) = e2 | e0 != e0 | e1 != e1 | ~'Ts0' | ~'Ts3', inference(equality_resolution, [status(thm)], [d303])). % 104.92/21.69 cnf(d305, plain, op(e2,e2) = e0 | op(e3,e2) = e0 | op(e3,e2) = e2 | e0 != e0 | ~'Ts0' | ~'Ts3', inference(equality_resolution, [status(thm)], [d304])). % 104.92/21.69 cnf(d306, plain, op(e2,e2) = e0 | op(e3,e2) = e0 | op(e3,e2) = e2 | ~'Ts0' | ~'Ts3', inference(equality_resolution, [status(thm)], [d305])). % 104.92/21.69 cnf(d307, plain, op(e0,e2) != e2 | op(e2,e2) = e0 | op(e3,e2) = e0 | ~'Ts0' | ~'Ts3', inference(superposition, [status(thm)], [d306,c62])). % 104.92/21.69 cnf(d308, plain, op(e0,e2) != e3 | ~'Ts3', inference(superposition, [status(thm)], [d133,c61])). % 104.92/21.69 cnf(d309, plain, e3 != e3 | ~'Ts3' | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1, inference(superposition, [status(thm)], [c2,d308])). % 104.92/21.69 cnf(d310, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | ~'Ts3', inference(equality_resolution, [status(thm)], [d309])). % 104.92/21.69 cnf(d311, plain, op(e0,e0) != e1 | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts3', inference(superposition, [status(thm)], [d310,c73])). % 104.92/21.69 cnf(d312, plain, e1 != e1 | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d311])). % 104.92/21.69 cnf(d313, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | 'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d312])). % 104.92/21.69 cnf(d314, plain, e2 != e2 | op(e2,e2) = e0 | op(e3,e2) = e0 | ~'Ts0' | ~'Ts3' | op(e0,e2) = e0 | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d313,d307])). % 104.92/21.69 cnf(d315, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d314])). % 104.92/21.69 cnf(d316, plain, e0 != e0 | op(e2,e2) = e0 | ~'Ts0' | op(e0,e2) = e0 | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d315,d95])). % 104.92/21.69 cnf(d317, plain, op(e0,e2) = e0 | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d316])). % 104.92/21.69 cnf(d318, plain, e0 = e3 | ~'Ts3' | op(e0,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d317,d133])). % 104.92/21.69 cnf(d319, plain, op(e0,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(resolution, [status(thm)], [c98,d318])). % 104.92/21.69 cnf(d320, plain, e0 != e0 | op(e2,e2) = e0 | op(e1,e0) = e0 | ~'Ts0' | 'Ts1' | ~'Ts0' | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d319,d294])). % 104.92/21.69 cnf(d321, plain, op(e2,e2) = e0 | op(e1,e0) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d320])). % 104.92/21.69 cnf(d322, plain, e0 != op(e2,e0) | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d321,c51])). % 104.92/21.69 cnf(d323, plain, e2 != e2 | op(e3,e3) = e3 | ~'Ts3' | op(e0,e3) = e2 | op(e2,e3) = e2 | op(e1,e3) = e2, inference(superposition, [status(thm)], [c45,c132])). % 104.92/21.69 cnf(d324, plain, op(e0,e3) = e2 | op(e2,e3) = e2 | op(e1,e3) = e2 | op(e3,e3) = e3 | ~'Ts3', inference(equality_resolution, [status(thm)], [d323])). % 104.92/21.69 cnf(d325, plain, e2 = e3 | op(e0,e3) = e2 | op(e2,e3) = e2 | op(e1,e3) = e2 | ~'Ts3' | op(e0,e3) = e2 | op(e2,e3) = e2 | op(e1,e3) = e2, inference(superposition, [status(thm)], [c45,d324])). % 104.92/21.69 cnf(d326, plain, op(e0,e3) = e2 | op(e2,e3) = e2 | op(e1,e3) = e2 | ~'Ts3', inference(resolution, [status(thm)], [c101,d325])). % 104.92/21.69 cnf(d327, plain, op(e1,e1) != e2 | op(e0,e3) = e2 | op(e2,e3) = e2 | ~'Ts3', inference(superposition, [status(thm)], [d326,c82])). % 104.92/21.69 cnf(d328, plain, e2 != e2 | op(e0,e3) = e2 | op(e2,e3) = e2 | ~'Ts3' | op(e0,e0) = e2 | 'Ts2', inference(superposition, [status(thm)], [c110,d327])). % 104.92/21.69 cnf(d329, plain, op(e0,e0) = e2 | op(e0,e3) = e2 | op(e2,e3) = e2 | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d328])). % 104.92/21.69 cnf(d330, plain, op(e2,e0) != e2 | op(e0,e0) = e2 | op(e0,e3) = e2 | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d329,c86])). % 104.92/21.69 cnf(d331, plain, op(e0,e0) != e1 | op(e2,e0) = e0 | op(e2,e0) = e2 | ~'Ts3', inference(superposition, [status(thm)], [d155,c49])). % 104.92/21.69 cnf(d332, plain, e1 != e1 | op(e2,e0) = e0 | op(e2,e0) = e2 | ~'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d331])). % 104.92/21.69 cnf(d333, plain, op(e2,e0) = e0 | op(e2,e0) = e2 | 'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d332])). % 104.92/21.69 cnf(d334, plain, e2 != e2 | op(e0,e0) = e2 | op(e0,e3) = e2 | 'Ts2' | ~'Ts3' | op(e2,e0) = e0 | 'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d333,d330])). % 104.92/21.69 cnf(d335, plain, op(e0,e0) = e2 | op(e0,e3) = e2 | op(e2,e0) = e0 | 'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d334])). % 104.92/21.69 cnf(d336, plain, e0 != e0 | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | ~'Ts3' | op(e0,e0) = e2 | op(e0,e3) = e2 | 'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d335,d322])). % 104.92/21.69 cnf(d337, plain, op(e0,e0) = e2 | op(e0,e3) = e2 | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d336])). % 104.92/21.69 cnf(d338, plain, e0 = e3 | ~'Ts3' | op(e0,e0) = e2 | op(e0,e3) = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d337,d133])). % 104.92/21.69 cnf(d339, plain, op(e0,e0) = e2 | op(e0,e3) = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c98,d338])). % 104.92/21.69 cnf(d340, plain, e2 != e2 | op(e2,e2) = e0 | e0 != op(e3,e3) | e1 != e1 | ~'Ts0' | 'Ts1' | op(e0,e0) = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d339,d286])). % 104.92/21.69 cnf(d341, plain, e0 != e0 | op(e0,e0) = e2 | op(e2,e2) = e0 | e2 != e2 | e1 != e1 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,d340])). % 104.92/21.69 cnf(d342, plain, op(e0,e0) = e2 | op(e2,e2) = e0 | e0 != e0 | e2 != e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d341])). % 104.92/21.69 cnf(d343, plain, op(e0,e0) = e2 | op(e2,e2) = e0 | e0 != e0 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d342])). % 104.92/21.69 cnf(d344, plain, op(e0,e0) = e2 | op(e2,e2) = e0 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(equality_resolution, [status(thm)], [d343])). % 104.92/21.69 cnf(d345, plain, e0 = e3 | ~'Ts3' | op(e0,e0) = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(superposition, [status(thm)], [d344,d133])). % 104.92/21.69 cnf(d346, plain, op(e0,e0) = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c98,d345])). % 104.92/21.69 cnf(d347, plain, e1 = e2 | ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d346])). % 104.92/21.69 cnf(d348, plain, ~'Ts0' | 'Ts1' | 'Ts2' | ~'Ts3', inference(resolution, [status(thm)], [c99,d347])). % 104.92/21.69 cnf(d349, plain, ~'Ts0' | 'Ts1' | 'Ts2' | 'Ts1' | 'Ts2', inference(resolution, [status(thm)], [d348,d282])). % 104.92/21.69 cnf(d350, plain, 'Ts1' | 'Ts2', inference(resolution, [status(thm)], [d274,d349])). % 104.92/21.69 cnf(d351, plain, e0 = e2 | op(e2,e2) = e2 | ~'Ts2' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,c126])). % 104.92/21.69 cnf(d352, plain, op(e2,e2) = e0 | op(e2,e2) = e2 | ~'Ts0' | ~'Ts2', inference(resolution, [status(thm)], [c97,d351])). % 104.92/21.69 cnf(d353, plain, e2 != e2 | op(e3,e3) = e2 | ~'Ts2' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d352,c128])). % 104.92/21.69 cnf(d354, plain, op(e2,e2) = e0 | op(e3,e3) = e2 | ~'Ts0' | ~'Ts2', inference(equality_resolution, [status(thm)], [d353])). % 104.92/21.69 cnf(d355, plain, e0 = e2 | op(e2,e2) = e0 | ~'Ts0' | ~'Ts2' | op(e2,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [c118,d354])). % 104.92/21.69 cnf(d356, plain, op(e2,e2) = e0 | ~'Ts0' | ~'Ts2', inference(resolution, [status(thm)], [c97,d355])). % 104.92/21.69 cnf(d357, plain, e1 != op(e0,op(e2,e2)) | e0 != op(e2,e2) | e3 != op(op(e2,e2),e2) | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,c155])). % 104.92/21.69 cnf(d358, plain, e3 != op(e0,e2) | e0 != op(e2,e2) | e1 != op(e0,op(e2,e2)) | ~'Ts0' | ~'Ts2' | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,d357])). % 104.92/21.69 cnf(d359, plain, e1 != op(e0,e0) | e0 != op(e2,e2) | e3 != op(e0,e2) | ~'Ts0' | ~'Ts2' | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,d358])). % 104.92/21.69 cnf(d360, plain, op(e0,e1) != e3 | op(e0,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [c114,c54])). % 104.92/21.69 cnf(d361, plain, op(e1,e0) != e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d223,c80])). % 104.92/21.69 cnf(d362, plain, e3 != op(e1,op(e0,e0)) | e2 != op(op(e0,e0),e0) | e1 != op(e0,e0) | 'Ts1', inference(superposition, [status(thm)], [d113,c150])). % 104.92/21.69 cnf(d363, plain, e3 != op(e1,e1) | e2 != op(op(e0,e0),e0) | e1 != op(e0,e0) | 'Ts1' | 'Ts1', inference(superposition, [status(thm)], [d113,d362])). % 104.92/21.69 cnf(d364, plain, e2 != op(e1,e0) | e1 != op(e0,e0) | e3 != op(e1,e1) | 'Ts1' | 'Ts1', inference(superposition, [status(thm)], [d113,d363])). % 104.92/21.69 cnf(d365, plain, e3 != e3 | e2 != op(e1,e0) | e1 != op(e0,e0) | 'Ts1' | op(e0,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [c114,d364])). % 104.92/21.69 cnf(d366, plain, e1 != e1 | op(e0,e0) = e3 | e2 != op(e1,e0) | e3 != e3 | 'Ts1' | 'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d365])). % 104.92/21.69 cnf(d367, plain, op(e1,e0) != e3 | op(e0,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [c114,c78])). % 104.92/21.69 cnf(d368, plain, e3 != e3 | op(e0,e0) = e3 | 'Ts3' | op(e1,e0) = e0 | op(e1,e0) = e2 | op(e1,e0) = e1, inference(superposition, [status(thm)], [c4,d367])). % 104.92/21.69 cnf(d369, plain, op(e0,e0) = e3 | op(e1,e0) = e0 | op(e1,e0) = e2 | op(e1,e0) = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d368])). % 104.92/21.69 cnf(d370, plain, op(e0,e0) != e1 | op(e0,e0) = e3 | op(e1,e0) = e0 | op(e1,e0) = e2 | 'Ts3', inference(superposition, [status(thm)], [d369,c48])). % 104.92/21.69 cnf(d371, plain, e1 != e1 | op(e0,e0) = e3 | op(e1,e0) = e0 | op(e1,e0) = e2 | 'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d370])). % 104.92/21.69 cnf(d372, plain, op(e0,e0) = e3 | op(e1,e0) = e0 | op(e1,e0) = e2 | 'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d371])). % 104.92/21.69 cnf(d373, plain, e2 != e2 | op(e0,e0) = e3 | e1 != e1 | e3 != e3 | 'Ts1' | 'Ts3' | op(e0,e0) = e3 | op(e1,e0) = e0 | 'Ts1' | 'Ts3', inference(superposition, [status(thm)], [d372,d366])). % 104.92/21.69 cnf(d374, plain, op(e0,e0) = e3 | op(e1,e0) = e0 | e2 != e2 | e1 != e1 | 'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d373])). % 104.92/21.69 cnf(d375, plain, op(e0,e0) = e3 | op(e1,e0) = e0 | e2 != e2 | 'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d374])). % 104.92/21.69 cnf(d376, plain, op(e0,e0) = e3 | op(e1,e0) = e0 | 'Ts1' | 'Ts3', inference(equality_resolution, [status(thm)], [d375])). % 104.92/21.69 cnf(d377, plain, e0 != e0 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | ~'Ts2' | op(e0,e0) = e3 | 'Ts1' | 'Ts3', inference(superposition, [status(thm)], [d376,d361])). % 104.92/21.69 cnf(d378, plain, op(e0,e0) = e3 | op(e0,e3) = e0 | op(e2,e2) = e2 | op(e2,e3) = e0 | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d377])). % 104.92/21.69 cnf(d379, plain, op(e2,e2) != e0 | op(e0,e0) = e3 | op(e0,e3) = e0 | op(e2,e2) = e2 | 'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d378,c89])). % 104.92/21.69 cnf(d380, plain, e0 != e0 | op(e0,e0) = e3 | op(e0,e3) = e0 | op(e2,e2) = e2 | 'Ts1' | ~'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,d379])). % 104.92/21.69 cnf(d381, plain, op(e0,e0) = e3 | op(e0,e3) = e0 | op(e2,e2) = e2 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d380])). % 104.92/21.69 cnf(d382, plain, e0 = e2 | op(e0,e0) = e3 | op(e0,e3) = e0 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,d381])). % 104.92/21.69 cnf(d383, plain, op(e0,e0) = e3 | op(e0,e3) = e0 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c97,d382])). % 104.92/21.69 cnf(d384, plain, e0 = e3 | op(e0,e0) = e3 | op(e0,e2) = e3 | op(e0,e1) = e3 | op(e0,e0) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d383,c22])). % 104.92/21.69 cnf(d385, plain, op(e0,e0) = e3 | op(e0,e2) = e3 | op(e0,e1) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c98,d384])). % 104.92/21.69 cnf(d386, plain, e3 != e3 | op(e0,e0) = e3 | 'Ts3' | op(e0,e0) = e3 | op(e0,e2) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d385,d360])). % 104.92/21.69 cnf(d387, plain, op(e0,e0) = e3 | op(e0,e2) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d386])). % 104.92/21.69 cnf(d388, plain, e3 != e3 | e0 != op(e2,e2) | e1 != op(e0,e0) | ~'Ts0' | ~'Ts2' | op(e0,e0) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(superposition, [status(thm)], [d387,d359])). % 104.92/21.69 cnf(d389, plain, e1 != e1 | op(e0,e0) = e3 | e0 != op(e2,e2) | e3 != e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d388])). % 104.92/21.69 cnf(d390, plain, e0 != e0 | op(e0,e0) = e3 | e1 != e1 | e3 != e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3' | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d356,d389])). % 104.92/21.69 cnf(d391, plain, op(e0,e0) = e3 | e0 != e0 | e1 != e1 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d390])). % 104.92/21.69 cnf(d392, plain, op(e0,e0) = e3 | e0 != e0 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d391])). % 104.92/21.69 cnf(d393, plain, op(e0,e0) = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(equality_resolution, [status(thm)], [d392])). % 104.92/21.69 cnf(d394, plain, e1 = e3 | ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3' | 'Ts1', inference(superposition, [status(thm)], [d113,d393])). % 104.92/21.69 cnf(d395, plain, ~'Ts0' | 'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [c100,d394])). % 104.92/21.69 cnf(d396, plain, 'Ts1' | ~'Ts2' | 'Ts3', inference(resolution, [status(thm)], [d274,d395])). % 104.92/21.69 cnf(d397, plain, 'Ts1' | 'Ts3' | 'Ts1', inference(resolution, [status(thm)], [d396,d350])). % 104.92/21.69 cnf(d398, plain, 'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [d397,d179])). % 104.92/21.69 cnf(d399, plain, 'Ts1' | 'Ts1', inference(resolution, [status(thm)], [d398,d350])). % 104.92/21.69 cnf(d400, plain, 'Ts2' | 'Ts3', inference(resolution, [status(thm)], [d399,d275])). % 104.92/21.69 cnf(d401, plain, e2 = e1 | op(e2,e2) = e1 | ~'Ts1' | op(e2,e2) = e2 | ~'Ts2', inference(superposition, [status(thm)], [c126,c122])). % 104.92/21.69 cnf(d402, plain, e2 = e1 | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts2', inference(superposition, [status(thm)], [d352,d87])). % 104.92/21.69 cnf(d403, plain, e0 = e1 | op(e2,e2) = e2 | e2 = e1 | ~'Ts1' | ~'Ts2' | e2 = e1 | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d402,d401])). % 104.92/21.69 cnf(d404, plain, op(e2,e2) = e2 | e2 = e1 | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c96,d403])). % 104.92/21.69 cnf(d405, plain, e1 = e2 | op(e2,e2) = e0 | ~'Ts0' | ~'Ts2' | op(e2,e2) = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d87,d352])). % 104.92/21.69 cnf(d406, plain, op(e2,e2) = e0 | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c99,d405])). % 104.92/21.69 cnf(d407, plain, e0 = e2 | e2 = e1 | ~'Ts0' | ~'Ts1' | ~'Ts2' | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d406,d404])). % 104.92/21.69 cnf(d408, plain, e2 = e1 | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [c97,d407])). % 104.92/21.69 cnf(d409, plain, e2 != e2 | ~'Ts0' | ~'Ts1' | ~'Ts2', inference(superposition, [status(thm)], [d408,c99])). % 104.92/21.69 cnf(d410, plain, ~'Ts0' | ~'Ts1' | ~'Ts2', inference(equality_resolution, [status(thm)], [d409])). % 104.92/21.69 cnf(d411, plain, ~'Ts1' | ~'Ts2', inference(resolution, [status(thm)], [d274,d410])). % 104.92/21.69 cnf(d412, plain, ~'Ts2', inference(resolution, [status(thm)], [d399,d411])). % 104.92/21.69 cnf(d413, plain, 'Ts3', inference(resolution, [status(thm)], [d412,d400])). % 104.92/21.69 cnf(d414, plain, e1 = e0 | op(e2,e2) = e0 | ~'Ts0' | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,c118])). % 104.92/21.69 cnf(d415, plain, e1 = e3 | ~'Ts3' | op(e2,e2) = e0 | e1 = e0 | ~'Ts0' | ~'Ts1', inference(superposition, [status(thm)], [d414,d133])). % 104.92/21.69 cnf(d416, plain, op(e2,e2) = e0 | e1 = e0 | ~'Ts0' | ~'Ts1' | ~'Ts3', inference(resolution, [status(thm)], [c100,d415])). % 104.92/21.69 cnf(d417, plain, e0 = e3 | ~'Ts3' | e1 = e0 | ~'Ts0' | ~'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d416,d133])). % 104.92/21.69 cnf(d418, plain, e1 = e0 | ~'Ts0' | ~'Ts1' | ~'Ts3', inference(resolution, [status(thm)], [c98,d417])). % 104.92/21.69 cnf(d419, plain, e0 != e0 | ~'Ts0' | ~'Ts1' | ~'Ts3', inference(superposition, [status(thm)], [d418,c96])). % 104.92/21.69 cnf(d420, plain, ~'Ts0' | ~'Ts1' | ~'Ts3', inference(equality_resolution, [status(thm)], [d419])). % 104.92/21.69 cnf(d421, plain, ~'Ts1' | ~'Ts3', inference(resolution, [status(thm)], [d274,d420])). % 104.92/21.69 cnf(d422, plain, ~'Ts3', inference(resolution, [status(thm)], [d399,d421])). % 104.92/21.69 cnf(d423, plain, $false, inference(resolution, [status(thm)], [d422,d413])). % 104.92/21.69 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------