%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG130+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:38 AM UTC 2026 % Result : Unsatisfiable 44.42s 7.62s % Output : CNFRefutation 44.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG130+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.09/0.35 % Computer : n001.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 26 21:20:44 UTC 2026 % 0.12/0.36 % CPUTime : % 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 44.42/7.62 % SZS status Unsatisfiable for theBenchmark.p % 44.42/7.62 % SZS output start CNFRefutation for theBenchmark.p % 44.42/7.62 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))))))))))))))))))). % 44.42/7.62 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))))))))))))))))))))))))))))))))))). % 44.42/7.62 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))))))))))))))))))))))))))))))))))))))))))))))))). % 44.42/7.62 fof(ax4, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e1 != e2 & (e1 != e3 & e2 != e3)))))). % 44.42/7.62 fof(ax5, axiom, (op(op(e0,e0),e0) = e0 & (op(op(e0,e1),e0) = e1 & (op(op(e0,e2),e0) = e2 & (op(op(e0,e3),e0) = e3 & (op(op(e1,e0),e1) = e0 & (op(op(e1,e1),e1) = e1 & (op(op(e1,e2),e1) = e2 & (op(op(e1,e3),e1) = e3 & (op(op(e2,e0),e2) = e0 & (op(op(e2,e1),e2) = e1 & (op(op(e2,e2),e2) = e2 & (op(op(e2,e3),e2) = e3 & (op(op(e3,e0),e3) = e0 & (op(op(e3,e1),e3) = e1 & (op(op(e3,e2),e3) = e2 & (op(op(e3,e3),e3) = e3 & ((op(e0,op(e0,e0)) = op(e0,e0) & (op(e0,op(e1,e0)) = op(e1,e0) & (op(e0,op(e2,e0)) = op(e2,e0) & op(e0,op(e3,e0)) = op(e3,e0)))) | ((op(e1,op(e0,e1)) = op(e0,e1) & (op(e1,op(e1,e1)) = op(e1,e1) & (op(e1,op(e2,e1)) = op(e2,e1) & op(e1,op(e3,e1)) = op(e3,e1)))) | ((op(e2,op(e0,e2)) = op(e0,e2) & (op(e2,op(e1,e2)) = op(e1,e2) & (op(e2,op(e2,e2)) = op(e2,e2) & op(e2,op(e3,e2)) = op(e3,e2)))) | (op(e3,op(e0,e3)) = op(e0,e3) & (op(e3,op(e1,e3)) = op(e1,e3) & (op(e3,op(e2,e3)) = op(e2,e3) & op(e3,op(e3,e3)) = op(e3,e3)))))))))))))))))))))))). % 44.42/7.62 fof(ax11, axiom, ~((e0 = op(op(e2,e3),op(e2,e3)) & e1 = op(e2,e3)))). % 44.42/7.62 fof(ax13, axiom, ~((e1 = op(op(e3,e0),op(e3,e0)) & e2 = op(e3,e0)))). % 44.42/7.62 fof(ax23, axiom, ~((e2 = op(op(e1,e3),op(e1,e3)) & e0 = op(e1,e3)))). % 44.42/7.62 fof(ax26, axiom, ~((e3 = op(op(e0,e1),op(e0,e1)) & e2 = op(e0,e1)))). % 44.42/7.62 cnf(c0, plain, op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c1, plain, op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c2, plain, op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c3, plain, op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c6, plain, op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c9, plain, op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c10, plain, op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/7.62 cnf(c20, plain, op(e0,e0) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e3) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c21, plain, op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c24, plain, op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c28, plain, op(e1,e0) = e2 | op(e1,e1) = e2 | op(e1,e2) = e2 | op(e1,e3) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c42, plain, op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c44, plain, op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/7.62 cnf(c48, plain, op(e0,e0) != op(e1,e0), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c51, plain, op(e1,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c52, plain, op(e1,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c53, plain, op(e2,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c55, plain, op(e0,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c57, plain, op(e1,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c60, plain, op(e0,e2) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c62, plain, op(e0,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c66, plain, op(e0,e3) != op(e1,e3), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c69, plain, op(e1,e3) != op(e2,e3), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c75, plain, op(e0,e1) != op(e0,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c79, plain, op(e1,e0) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c81, plain, op(e1,e1) != op(e1,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c87, plain, op(e2,e1) != op(e2,e2), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c88, plain, op(e2,e1) != op(e2,e3), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c94, plain, op(e3,e1) != op(e3,e3), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c95, plain, op(e3,e2) != op(e3,e3), inference(clausification, [status(esa)], [ax3])). % 44.42/7.62 cnf(c96, plain, e0 != e1, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c97, plain, e0 != e2, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c98, plain, e0 != e3, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c99, plain, e1 != e2, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c100, plain, e1 != e3, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c101, plain, e2 != e3, inference(clausification, [status(esa)], [ax4])). % 44.42/7.62 cnf(c102, plain, op(op(e0,e0),e0) = e0, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c103, plain, op(op(e0,e1),e0) = e1, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c104, plain, op(op(e0,e2),e0) = e2, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c105, plain, op(op(e0,e3),e0) = e3, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c106, plain, op(op(e1,e0),e1) = e0, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c107, plain, op(op(e1,e1),e1) = e1, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c108, plain, op(op(e1,e2),e1) = e2, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c109, plain, op(op(e1,e3),e1) = e3, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c110, plain, op(op(e2,e0),e2) = e0, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c111, plain, op(op(e2,e1),e2) = e1, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c112, plain, op(op(e2,e2),e2) = e2, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c113, plain, op(op(e2,e3),e2) = e3, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c114, plain, op(op(e3,e0),e3) = e0, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c115, plain, op(op(e3,e1),e3) = e1, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c116, plain, op(op(e3,e2),e3) = e2, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c117, plain, op(op(e3,e3),e3) = e3, inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c118, plain, X0 | X1 | X2 | op(e3,op(e0,e3)) = op(e0,e3), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c120, plain, X0 | X1 | X2 | op(e3,op(e2,e3)) = op(e2,e3), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c121, plain, X0 | X1 | X2 | op(e3,op(e3,e3)) = op(e3,e3), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c122, plain, ~X0 | op(e2,op(e0,e2)) = op(e0,e2), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c123, plain, ~X0 | op(e2,op(e1,e2)) = op(e1,e2), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c124, plain, ~X0 | op(e2,op(e2,e2)) = op(e2,e2), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c126, plain, ~X0 | op(e1,op(e0,e1)) = op(e0,e1), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c128, plain, ~X0 | op(e1,op(e2,e1)) = op(e2,e1), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c130, plain, ~X0 | op(e0,op(e0,e0)) = op(e0,e0), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c132, plain, ~X0 | op(e0,op(e2,e0)) = op(e2,e0), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c133, plain, ~X0 | op(e0,op(e3,e0)) = op(e3,e0), inference(clausification, [status(esa)], [ax5])). % 44.42/7.62 cnf(c139, plain, e0 != op(op(e2,e3),op(e2,e3)) | e1 != op(e2,e3), inference(clausification, [status(esa)], [ax11])). % 44.42/7.62 cnf(c141, plain, e1 != op(op(e3,e0),op(e3,e0)) | e2 != op(e3,e0), inference(clausification, [status(esa)], [ax13])). % 44.42/7.62 cnf(c151, plain, e2 != op(op(e1,e3),op(e1,e3)) | e0 != op(e1,e3), inference(clausification, [status(esa)], [ax23])). % 44.42/7.62 cnf(c154, plain, e3 != op(op(e0,e1),op(e0,e1)) | e2 != op(e0,e1), inference(clausification, [status(esa)], [ax26])). % 44.42/7.62 cnf(d0, plain, op(e3,e0) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | op(e0,e0) = e1, inference(superposition, [status(thm)], [c0,c102])). % 44.42/7.62 cnf(d1, plain, op(e0,e3) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | op(e0,e0) = e1, inference(superposition, [status(thm)], [d0,c114])). % 44.42/7.62 cnf(d2, plain, op(e0,e3) = op(e0,e0) | ~'Ts2' | op(e0,e0) = e0 | op(e0,e0) = e2 | op(e0,e0) = e1, inference(superposition, [status(thm)], [c0,c130])). % 44.42/7.62 cnf(d3, plain, op(e0,e0) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | op(e0,e0) = e1 | op(e0,e0) = e0 | op(e0,e0) = e2 | op(e0,e0) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d2,d1])). % 44.42/7.62 cnf(d4, plain, op(e1,e0) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | ~'Ts2', inference(superposition, [status(thm)], [d3,c102])). % 44.42/7.62 cnf(d5, plain, op(e0,e1) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | ~'Ts2', inference(superposition, [status(thm)], [d4,c106])). % 44.42/7.62 cnf(d6, plain, op(e0,e1) = op(e0,e0) | ~'Ts2' | op(e0,e0) = e0 | op(e0,e0) = e2 | ~'Ts2', inference(superposition, [status(thm)], [d3,c130])). % 44.42/7.62 cnf(d7, plain, op(e0,e0) = e0 | op(e0,e0) = e0 | op(e0,e0) = e2 | ~'Ts2' | op(e0,e0) = e0 | op(e0,e0) = e2 | ~'Ts2', inference(superposition, [status(thm)], [d6,d5])). % 44.42/7.62 cnf(d8, plain, op(e2,e0) = e0 | op(e0,e0) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d7,c102])). % 44.42/7.62 cnf(d9, plain, op(e0,e2) = e0 | op(e0,e0) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d8,c110])). % 44.42/7.62 cnf(d10, plain, op(e0,e2) = op(e0,e0) | ~'Ts2' | op(e0,e0) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d7,c130])). % 44.42/7.62 cnf(d11, plain, op(e0,e0) = e0 | op(e0,e0) = e0 | ~'Ts2' | op(e0,e0) = e0 | ~'Ts2', inference(superposition, [status(thm)], [d10,d9])). % 44.42/7.62 cnf(d12, plain, op(e3,e0) = e3 | op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1, inference(superposition, [status(thm)], [c3,c105])). % 44.42/7.62 cnf(d13, plain, op(e3,e3) = e0 | op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1, inference(superposition, [status(thm)], [d12,c114])). % 44.42/7.62 cnf(d14, plain, op(e3,e3) = op(e0,e3) | 'Ts0' | 'Ts2' | 'Ts1' | op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1, inference(superposition, [status(thm)], [c3,c118])). % 44.42/7.62 cnf(d15, plain, op(e0,e3) = e0 | op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1 | op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d14,d13])). % 44.42/7.62 cnf(d16, plain, op(e1,e0) = e3 | op(e0,e3) = e0 | op(e0,e3) = e2 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d15,c105])). % 44.42/7.62 cnf(d17, plain, op(e3,e1) = e0 | op(e0,e3) = e0 | op(e0,e3) = e2 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d16,c106])). % 44.42/7.62 cnf(d18, plain, op(e3,e2) = e1 | op(e2,e1) = e0 | op(e2,e1) = e2 | op(e2,e1) = e1, inference(superposition, [status(thm)], [c9,c111])). % 44.42/7.62 cnf(d19, plain, op(e1,e3) = e2 | op(e2,e1) = e0 | op(e2,e1) = e2 | op(e2,e1) = e1, inference(superposition, [status(thm)], [d18,c116])). % 44.42/7.62 cnf(d20, plain, op(e1,e3) = op(e2,e1) | ~'Ts1' | op(e2,e1) = e0 | op(e2,e1) = e2 | op(e2,e1) = e1, inference(superposition, [status(thm)], [c9,c128])). % 44.42/7.62 cnf(d21, plain, op(e2,e1) = e2 | op(e2,e1) = e0 | op(e2,e1) = e2 | op(e2,e1) = e1 | op(e2,e1) = e0 | op(e2,e1) = e2 | op(e2,e1) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d20,d19])). % 44.42/7.62 cnf(d22, plain, op(e1,e1) = op(e2,e1) | ~'Ts1' | op(e2,e1) = e0 | op(e2,e1) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d21,c128])). % 44.42/7.62 cnf(d23, plain, op(e2,e1) = e0 | op(e2,e1) = e2 | ~'Ts1', inference(resolution, [status(thm)], [c57,d22])). % 44.42/7.62 cnf(d24, plain, op(e2,e2) = e1 | op(e2,e1) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d23,c111])). % 44.42/7.62 cnf(d25, plain, op(e0,e1) != e0 | op(e2,e2) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d24,c55])). % 44.42/7.62 cnf(d26, plain, op(e3,e0) = e1 | op(e0,e1) = e0 | op(e0,e1) = e2 | op(e0,e1) = e1, inference(superposition, [status(thm)], [c1,c103])). % 44.42/7.62 cnf(d27, plain, op(e1,e3) = e0 | op(e0,e1) = e0 | op(e0,e1) = e2 | op(e0,e1) = e1, inference(superposition, [status(thm)], [d26,c114])). % 44.42/7.62 cnf(d28, plain, op(e1,e3) = op(e0,e1) | ~'Ts1' | op(e0,e1) = e0 | op(e0,e1) = e2 | op(e0,e1) = e1, inference(superposition, [status(thm)], [c1,c126])). % 44.42/7.62 cnf(d29, plain, op(e0,e1) = e0 | op(e0,e1) = e0 | op(e0,e1) = e2 | op(e0,e1) = e1 | op(e0,e1) = e0 | op(e0,e1) = e2 | op(e0,e1) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d28,d27])). % 44.42/7.62 cnf(d30, plain, op(e1,e0) = e1 | op(e0,e1) = e0 | op(e0,e1) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d29,c103])). % 44.42/7.62 cnf(d31, plain, op(e1,e1) = e0 | op(e0,e1) = e0 | op(e0,e1) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d30,c106])). % 44.42/7.62 cnf(d32, plain, op(e1,e1) = op(e0,e1) | ~'Ts1' | op(e0,e1) = e0 | op(e0,e1) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d29,c126])). % 44.42/7.62 cnf(d33, plain, op(e0,e1) = e0 | op(e0,e1) = e0 | op(e0,e1) = e2 | ~'Ts1' | op(e0,e1) = e0 | op(e0,e1) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d32,d31])). % 44.42/7.62 cnf(d34, plain, op(e2,e0) = e1 | op(e0,e1) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d33,c103])). % 44.42/7.62 cnf(d35, plain, op(e1,e2) = e0 | op(e0,e1) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d34,c110])). % 44.42/7.62 cnf(d36, plain, op(e1,e2) = op(e0,e1) | ~'Ts1' | op(e0,e1) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d33,c126])). % 44.42/7.62 cnf(d37, plain, op(e0,e1) = e0 | op(e0,e1) = e0 | ~'Ts1' | op(e0,e1) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d36,d35])). % 44.42/7.62 cnf(d38, plain, e0 != e0 | op(e2,e2) = e1 | ~'Ts1' | ~'Ts1', inference(superposition, [status(thm)], [d37,d25])). % 44.42/7.62 cnf(d39, plain, op(e2,e2) = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d38])). % 44.42/7.62 cnf(d40, plain, op(e2,e3) = e0 | op(e0,e0) = e2 | op(e2,e0) = e2 | op(e1,e0) = e2, inference(superposition, [status(thm)], [c21,c114])). % 44.42/7.62 cnf(d41, plain, op(e0,e0) = e1 | ~'Ts1', inference(superposition, [status(thm)], [d37,c103])). % 44.42/7.62 cnf(d42, plain, op(e1,e0) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d41,c102])). % 44.42/7.62 cnf(d43, plain, e0 = e2 | op(e0,e0) = e2 | op(e2,e0) = e2 | op(e2,e3) = e0 | ~'Ts1', inference(superposition, [status(thm)], [d42,d40])). % 44.42/7.62 cnf(d44, plain, op(e0,e0) = e2 | op(e2,e0) = e2 | op(e2,e3) = e0 | ~'Ts1', inference(resolution, [status(thm)], [c97,d43])). % 44.42/7.62 cnf(d45, plain, op(e0,e2) = e3 | op(e0,e0) = e2 | op(e2,e0) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d44,c113])). % 44.42/7.62 cnf(d46, plain, op(e2,e2) = e0 | op(e0,e0) = e2 | op(e0,e2) = e3 | ~'Ts1', inference(superposition, [status(thm)], [d45,c110])). % 44.42/7.62 cnf(d47, plain, e0 = e1 | ~'Ts1' | op(e0,e0) = e2 | op(e0,e2) = e3 | ~'Ts1', inference(superposition, [status(thm)], [d46,d39])). % 44.42/7.62 cnf(d48, plain, op(e0,e0) = e2 | op(e0,e2) = e3 | ~'Ts1', inference(resolution, [status(thm)], [c96,d47])). % 44.42/7.62 cnf(d49, plain, op(e3,e0) = e2 | op(e0,e0) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d48,c104])). % 44.42/7.62 cnf(d50, plain, e1 != op(op(e3,e0),e2) | e2 != op(e3,e0) | op(e0,e0) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d49,c141])). % 44.42/7.62 cnf(d51, plain, e1 != op(e2,e2) | op(e0,e0) = e2 | e2 != op(e3,e0) | ~'Ts1' | op(e0,e0) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d49,d50])). % 44.42/7.62 cnf(d52, plain, e1 != e1 | op(e0,e0) = e2 | e2 != op(e3,e0) | ~'Ts1' | ~'Ts1', inference(superposition, [status(thm)], [d39,d51])). % 44.42/7.62 cnf(d53, plain, e2 != e2 | op(e0,e0) = e2 | e1 != e1 | ~'Ts1' | op(e0,e0) = e2 | ~'Ts1', inference(superposition, [status(thm)], [d49,d52])). % 44.42/7.62 cnf(d54, plain, op(e0,e0) = e2 | e2 != e2 | ~'Ts1', inference(equality_resolution, [status(thm)], [d53])). % 44.42/7.62 cnf(d55, plain, op(e0,e0) = e2 | ~'Ts1', inference(equality_resolution, [status(thm)], [d54])). % 44.42/7.62 cnf(d56, plain, e1 = e2 | ~'Ts1' | ~'Ts1', inference(superposition, [status(thm)], [d41,d55])). % 44.42/7.62 cnf(d57, plain, ~'Ts1', inference(resolution, [status(thm)], [c99,d56])). % 44.42/7.62 cnf(d58, plain, op(e0,e3) = e0 | op(e0,e3) = e2 | op(e3,e1) = e0 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,d17])). % 44.42/7.62 cnf(d59, plain, op(e3,op(e0,e3)) = op(e0,e3) | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,c118])). % 44.42/7.62 cnf(d60, plain, op(e0,e3) = e0 | op(e0,e3) = e2 | op(e0,e3) = e1 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,d15])). % 44.42/7.62 cnf(d61, plain, op(e3,e1) = op(e0,e3) | 'Ts0' | 'Ts2' | op(e0,e3) = e0 | op(e0,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d60,d59])). % 44.42/7.62 cnf(d62, plain, op(e0,e3) = e0 | op(e0,e3) = e0 | op(e0,e3) = e2 | 'Ts0' | 'Ts2' | op(e0,e3) = e0 | op(e0,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d61,d58])). % 44.42/7.62 cnf(d63, plain, op(e2,e0) = e3 | op(e0,e3) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d62,c105])). % 44.42/7.62 cnf(d64, plain, op(e3,e2) = e0 | op(e0,e3) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d63,c110])). % 44.42/7.62 cnf(d65, plain, op(e3,e2) = op(e0,e3) | 'Ts0' | 'Ts2' | op(e0,e3) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d62,d59])). % 44.42/7.62 cnf(d66, plain, op(e0,e3) = e0 | op(e0,e3) = e0 | 'Ts0' | 'Ts2' | op(e0,e3) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d65,d64])). % 44.42/7.62 cnf(d67, plain, op(e0,e0) = e3 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d66,c105])). % 44.42/7.62 cnf(d68, plain, op(e3,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d67,c102])). % 44.42/7.62 cnf(d69, plain, op(e1,e0) != e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d68,c52])). % 44.42/7.62 cnf(d70, plain, op(e3,e1) = op(e3,e3) | 'Ts0' | 'Ts2' | 'Ts1' | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1, inference(superposition, [status(thm)], [c42,c121])). % 44.42/7.62 cnf(d71, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1 | 'Ts0' | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [c94,d70])). % 44.42/7.62 cnf(d72, plain, op(e1,e3) = e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d71,c115])). % 44.42/7.62 cnf(d73, plain, op(e1,e3) = e2 | op(e1,e3) = e1 | op(e3,e0) = e1 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d72,c116])). % 44.42/7.62 cnf(d74, plain, op(e1,e3) = e2 | op(e1,e3) = e1 | op(e3,e0) = e1 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,d73])). % 44.42/7.62 cnf(d75, plain, e0 = e1 | op(e1,e3) = e2 | op(e1,e3) = e1 | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d68,d74])). % 44.42/7.62 cnf(d76, plain, op(e1,e3) = e2 | op(e1,e3) = e1 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [c96,d75])). % 44.42/7.62 cnf(d77, plain, op(e1,e1) = e3 | op(e1,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d76,c109])). % 44.42/7.62 cnf(d78, plain, e2 != op(e2,e3) | op(e1,e1) = e3 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d77,c69])). % 44.42/7.62 cnf(d79, plain, op(e3,e2) = op(e3,e3) | 'Ts0' | 'Ts2' | 'Ts1' | op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e1) = e2, inference(superposition, [status(thm)], [c44,c121])). % 44.42/7.62 cnf(d80, plain, op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e1) = e2 | 'Ts0' | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [c95,d79])). % 44.42/7.62 cnf(d81, plain, op(e2,e3) = e1 | op(e3,e0) = e2 | op(e3,e2) = e2 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d80,c115])). % 44.42/7.62 cnf(d82, plain, op(e2,e3) = e2 | op(e2,e3) = e1 | op(e3,e0) = e2 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [d81,c116])). % 44.42/7.62 cnf(d83, plain, op(e2,e3) = e2 | op(e2,e3) = e1 | op(e3,e0) = e2 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,d82])). % 44.42/7.62 cnf(d84, plain, e0 = e2 | op(e2,e3) = e2 | op(e2,e3) = e1 | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d68,d83])). % 44.42/7.62 cnf(d85, plain, op(e2,e3) = e2 | op(e2,e3) = e1 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [c97,d84])). % 44.42/7.62 cnf(d86, plain, op(e1,e2) = e3 | op(e2,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d85,c113])). % 44.42/7.62 cnf(d87, plain, op(e3,e1) = e2 | op(e2,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d86,c108])). % 44.42/7.62 cnf(d88, plain, op(e3,op(e2,e3)) = op(e2,e3) | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [d57,c120])). % 44.42/7.62 cnf(d89, plain, op(e3,e1) = op(e2,e3) | 'Ts0' | 'Ts2' | op(e2,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d85,d88])). % 44.42/7.62 cnf(d90, plain, op(e2,e3) = e2 | op(e2,e3) = e2 | 'Ts0' | 'Ts2' | op(e2,e3) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d89,d87])). % 44.42/7.62 cnf(d91, plain, e2 != e2 | op(e1,e1) = e3 | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d90,d78])). % 44.42/7.62 cnf(d92, plain, op(e1,e1) = e3 | 'Ts0' | 'Ts2', inference(equality_resolution, [status(thm)], [d91])). % 44.42/7.62 cnf(d93, plain, op(e0,e3) != e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0, inference(superposition, [status(thm)], [c24,c66])). % 44.42/7.62 cnf(d94, plain, e0 != e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d66,d93])). % 44.42/7.62 cnf(d95, plain, op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0 | 'Ts0' | 'Ts2', inference(equality_resolution, [status(thm)], [d94])). % 44.42/7.62 cnf(d96, plain, e0 = e3 | 'Ts0' | 'Ts2' | op(e1,e0) = e0 | op(e1,e2) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d95,d92])). % 44.42/7.62 cnf(d97, plain, op(e1,e0) = e0 | op(e1,e2) = e0 | 'Ts0' | 'Ts2', inference(resolution, [status(thm)], [c98,d96])). % 44.42/7.62 cnf(d98, plain, op(e0,e1) = e2 | op(e1,e0) = e0 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d97,c108])). % 44.42/7.62 cnf(d99, plain, e0 != e0 | 'Ts0' | 'Ts2' | op(e0,e1) = e2 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d98,d69])). % 44.42/7.62 cnf(d100, plain, op(e0,e1) = e2 | 'Ts0' | 'Ts2', inference(equality_resolution, [status(thm)], [d99])). % 44.42/7.62 cnf(d101, plain, e3 != op(e2,op(e0,e1)) | e2 != op(e0,e1) | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d100,c154])). % 44.42/7.62 cnf(d102, plain, e3 != op(e2,e2) | e2 != op(e0,e1) | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d100,d101])). % 44.42/7.62 cnf(d103, plain, op(e2,e2) = e3 | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d90,c113])). % 44.42/7.62 cnf(d104, plain, e3 != e3 | e2 != op(e0,e1) | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d103,d102])). % 44.42/7.62 cnf(d105, plain, e2 != e2 | e3 != e3 | 'Ts0' | 'Ts2' | 'Ts0' | 'Ts2', inference(superposition, [status(thm)], [d100,d104])). % 44.42/7.62 cnf(d106, plain, e2 != e2 | 'Ts0' | 'Ts2', inference(equality_resolution, [status(thm)], [d105])). % 44.42/7.62 cnf(d107, plain, 'Ts0' | 'Ts2', inference(equality_resolution, [status(thm)], [d106])). % 44.42/7.62 cnf(d108, plain, op(e0,e1) = e3 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e1) = e0, inference(superposition, [status(thm)], [c24,c109])). % 44.42/7.62 cnf(d109, plain, op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0 | op(e1,e2) = e0, inference(superposition, [status(thm)], [d108,c107])). % 44.42/7.62 cnf(d110, plain, op(e0,e2) != e0 | op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0, inference(superposition, [status(thm)], [d109,c60])). % 44.42/7.62 cnf(d111, plain, op(e3,e0) = e2 | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1, inference(superposition, [status(thm)], [c2,c104])). % 44.42/7.62 cnf(d112, plain, op(e2,e3) = e0 | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1, inference(superposition, [status(thm)], [d111,c114])). % 44.42/7.62 cnf(d113, plain, op(e2,e3) = op(e0,e2) | ~'Ts0' | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1, inference(superposition, [status(thm)], [c2,c122])). % 44.42/7.62 cnf(d114, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d113,d112])). % 44.42/7.62 cnf(d115, plain, op(e1,e0) = e2 | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d114,c104])). % 44.42/7.62 cnf(d116, plain, op(e2,e1) = e0 | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d115,c106])). % 44.42/7.62 cnf(d117, plain, op(e2,e1) = op(e0,e2) | ~'Ts0' | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d114,c122])). % 44.42/7.62 cnf(d118, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts0' | op(e0,e2) = e0 | op(e0,e2) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d117,d116])). % 44.42/7.62 cnf(d119, plain, op(e2,e0) = e2 | op(e0,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d118,c104])). % 44.42/7.62 cnf(d120, plain, op(e2,e2) = e0 | op(e0,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d119,c110])). % 44.42/7.62 cnf(d121, plain, op(e2,e2) = op(e0,e2) | ~'Ts0' | op(e0,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d118,c122])). % 44.42/7.62 cnf(d122, plain, op(e0,e2) = e0 | op(e0,e2) = e0 | ~'Ts0' | op(e0,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d121,d120])). % 44.42/7.62 cnf(d123, plain, op(e2,e0) = op(e0,e2) | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d122,c122])). % 44.42/7.62 cnf(d124, plain, op(e0,e0) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d122,c104])). % 44.42/7.62 cnf(d125, plain, op(e2,e0) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d124,c102])). % 44.42/7.62 cnf(d126, plain, e0 = op(e0,e2) | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d125,d123])). % 44.42/7.62 cnf(d127, plain, e0 != e0 | op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d126,d110])). % 44.42/7.62 cnf(d128, plain, op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d127])). % 44.42/7.62 cnf(d129, plain, e0 != op(e2,e0) | op(e0,e1) = e1 | op(e0,e1) = e3 | ~'Ts0', inference(superposition, [status(thm)], [d128,c51])). % 44.42/7.62 cnf(d130, plain, e0 != e0 | op(e0,e1) = e1 | op(e0,e1) = e3 | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d125,d129])). % 44.42/7.62 cnf(d131, plain, op(e0,e1) = e1 | op(e0,e1) = e3 | ~'Ts0', inference(equality_resolution, [status(thm)], [d130])). % 44.42/7.62 cnf(d132, plain, op(e3,e0) = e1 | op(e0,e1) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d131,c103])). % 44.42/7.62 cnf(d133, plain, op(e1,e3) = e0 | op(e0,e1) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d132,c114])). % 44.42/7.62 cnf(d134, plain, e2 != op(e0,op(e1,e3)) | e0 != op(e1,e3) | op(e0,e1) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d133,c151])). % 44.42/7.62 cnf(d135, plain, e2 != op(e0,e0) | op(e0,e1) = e1 | e0 != op(e1,e3) | ~'Ts0' | op(e0,e1) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d133,d134])). % 44.42/7.62 cnf(d136, plain, e2 != e2 | op(e0,e1) = e1 | e0 != op(e1,e3) | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d124,d135])). % 44.42/7.62 cnf(d137, plain, e0 != e0 | op(e0,e1) = e1 | e2 != e2 | ~'Ts0' | op(e0,e1) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d133,d136])). % 44.42/7.62 cnf(d138, plain, op(e0,e1) = e1 | e0 != e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d137])). % 44.42/7.62 cnf(d139, plain, op(e0,e1) = e1 | ~'Ts0', inference(equality_resolution, [status(thm)], [d138])). % 44.42/7.62 cnf(d140, plain, op(e1,e0) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d139,c103])). % 44.42/7.62 cnf(d141, plain, op(e1,e1) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d140,c106])). % 44.42/7.62 cnf(d142, plain, e0 != op(e1,e2) | ~'Ts0', inference(superposition, [status(thm)], [d141,c81])). % 44.42/7.62 cnf(d143, plain, op(e3,e1) = e2 | op(e1,e2) = e0 | op(e1,e2) = e2 | op(e1,e2) = e1, inference(superposition, [status(thm)], [c6,c108])). % 44.42/7.62 cnf(d144, plain, op(e2,e3) = e1 | op(e1,e2) = e0 | op(e1,e2) = e2 | op(e1,e2) = e1, inference(superposition, [status(thm)], [d143,c115])). % 44.42/7.62 cnf(d145, plain, op(e1,e0) != e1 | op(e2,e3) = e1 | op(e1,e2) = e0 | op(e1,e2) = e2, inference(superposition, [status(thm)], [d144,c79])). % 44.42/7.62 cnf(d146, plain, e1 != e1 | op(e2,e3) = e1 | op(e1,e2) = e0 | op(e1,e2) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d140,d145])). % 44.42/7.62 cnf(d147, plain, op(e2,e3) = e1 | op(e1,e2) = e0 | op(e1,e2) = e2 | ~'Ts0', inference(equality_resolution, [status(thm)], [d146])). % 44.42/7.62 cnf(d148, plain, op(e2,e1) = e2 | op(e2,e3) = e1 | op(e1,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d147,c108])). % 44.42/7.62 cnf(d149, plain, e0 != e0 | ~'Ts0' | op(e2,e1) = e2 | op(e2,e3) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d148,d142])). % 44.42/7.62 cnf(d150, plain, op(e2,e1) = e2 | op(e2,e3) = e1 | ~'Ts0', inference(equality_resolution, [status(thm)], [d149])). % 44.42/7.62 cnf(d151, plain, op(e1,e2) = e3 | op(e2,e1) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d150,c113])). % 44.42/7.62 cnf(d152, plain, op(e2,e3) = op(e1,e2) | ~'Ts0' | op(e2,e1) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d151,c123])). % 44.42/7.62 cnf(d153, plain, op(e2,e3) = e3 | op(e2,e1) = e2 | ~'Ts0' | op(e2,e1) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d152,d151])). % 44.42/7.62 cnf(d154, plain, e1 = e3 | op(e2,e1) = e2 | ~'Ts0' | op(e2,e1) = e2 | ~'Ts0', inference(superposition, [status(thm)], [d150,d153])). % 44.42/7.62 cnf(d155, plain, op(e2,e1) = e2 | ~'Ts0', inference(resolution, [status(thm)], [c100,d154])). % 44.42/7.62 cnf(d156, plain, op(e2,e2) = e1 | ~'Ts0', inference(superposition, [status(thm)], [d155,c111])). % 44.42/7.62 cnf(d157, plain, op(e2,e1) = op(e2,e2) | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d156,c124])). % 44.42/7.62 cnf(d158, plain, ~'Ts0', inference(resolution, [status(thm)], [c87,d157])). % 44.42/7.62 cnf(d159, plain, 'Ts2', inference(resolution, [status(thm)], [d158,d107])). % 44.42/7.62 cnf(d160, plain, op(e0,e0) = e0, inference(resolution, [status(thm)], [d159,d11])). % 44.42/7.62 cnf(d161, plain, e0 != op(e1,e0), inference(demodulation, [status(thm)], [c48,d160])). % 44.42/7.62 cnf(d162, plain, op(e0,e1) = e2 | op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0, inference(superposition, [status(thm)], [d109,c108])). % 44.42/7.62 cnf(d163, plain, e0 = e2 | op(e0,e2) = e2 | op(e0,e1) = e2 | op(e0,e3) = e2, inference(demodulation, [status(thm)], [c20,d160])). % 44.42/7.62 cnf(d164, plain, op(e0,e2) = e2 | op(e0,e1) = e2 | op(e0,e3) = e2, inference(resolution, [status(thm)], [c97,d163])). % 44.42/7.62 cnf(d165, plain, op(e2,e0) = e3 | op(e0,e2) = e2 | op(e0,e1) = e2, inference(superposition, [status(thm)], [d164,c105])). % 44.42/7.62 cnf(d166, plain, op(e0,op(e2,e0)) = op(e2,e0), inference(resolution, [status(thm)], [d159,c132])). % 44.42/7.62 cnf(d167, plain, op(e0,e3) = op(e2,e0) | op(e0,e2) = e2 | op(e0,e1) = e2, inference(superposition, [status(thm)], [d165,d166])). % 44.42/7.62 cnf(d168, plain, op(e0,e3) = e3 | op(e0,e2) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e1) = e2, inference(superposition, [status(thm)], [d167,d165])). % 44.42/7.62 cnf(d169, plain, e2 = e3 | op(e0,e2) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e1) = e2, inference(superposition, [status(thm)], [d164,d168])). % 44.42/7.62 cnf(d170, plain, op(e0,e2) = e2 | op(e0,e1) = e2, inference(resolution, [status(thm)], [c101,d169])). % 44.42/7.62 cnf(d171, plain, op(e2,e0) = e1 | op(e0,e2) = e2, inference(superposition, [status(thm)], [d170,c103])). % 44.42/7.62 cnf(d172, plain, op(e0,e1) = op(e2,e0) | op(e0,e2) = e2, inference(superposition, [status(thm)], [d171,d166])). % 44.42/7.62 cnf(d173, plain, op(e0,e1) = e1 | op(e0,e2) = e2 | op(e0,e2) = e2, inference(superposition, [status(thm)], [d172,d171])). % 44.42/7.62 cnf(d174, plain, e1 = e2 | op(e0,e2) = e2 | op(e0,e2) = e2, inference(superposition, [status(thm)], [d173,d170])). % 44.42/7.62 cnf(d175, plain, op(e0,e2) = e2, inference(resolution, [status(thm)], [c99,d174])). % 44.42/7.62 cnf(d176, plain, op(e0,e1) != e2, inference(demodulation, [status(thm)], [c75,d175])). % 44.42/7.62 cnf(d177, plain, op(e0,e1) = e1 | op(e0,e1) = e3 | op(e1,e0) = e0, inference(resolution, [status(thm)], [d176,d162])). % 44.42/7.62 cnf(d178, plain, e0 != e0 | op(e0,e1) = e1 | op(e0,e1) = e3, inference(superposition, [status(thm)], [d177,d161])). % 44.42/7.62 cnf(d179, plain, op(e2,e0) = e2, inference(demodulation, [status(thm)], [c104,d175])). % 44.42/7.62 cnf(d180, plain, op(e2,e2) = e0, inference(demodulation, [status(thm)], [c110,d179])). % 44.42/7.62 cnf(d181, plain, op(e3,e2) = e2 | op(e2,e2) = e0 | op(e2,e2) = e2 | op(e2,e2) = e1, inference(superposition, [status(thm)], [c10,c112])). % 44.42/7.62 cnf(d182, plain, op(e0,e2) != e2 | op(e2,e2) = e0 | op(e2,e2) = e2 | op(e2,e2) = e1, inference(superposition, [status(thm)], [d181,c62])). % 44.42/7.62 cnf(d183, plain, op(e2,e2) = e0 | op(e2,e2) = e2 | op(e2,e2) = e1, inference(resolution, [status(thm)], [d175,d182])). % 44.42/7.62 cnf(d184, plain, e0 = e0 | op(e2,e2) = e2 | op(e2,e2) = e1, inference(demodulation, [status(thm)], [d183,d180])). % 44.42/7.62 cnf(d185, plain, e0 = e0 | e0 = e2 | op(e2,e2) = e1, inference(demodulation, [status(thm)], [d184,d180])). % 44.42/7.62 cnf(d186, plain, e0 = e0 | e0 = e2 | e0 = e1, inference(demodulation, [status(thm)], [d185,d180])). % 44.42/7.62 cnf(d187, plain, e0 = e0 | e0 = e2, inference(resolution, [status(thm)], [c96,d186])). % 44.42/7.62 cnf(d188, plain, e0 = e0, inference(resolution, [status(thm)], [c97,d187])). % 44.42/7.62 cnf(d189, plain, op(e0,e1) = e1 | op(e0,e1) = e3, inference(resolution, [status(thm)], [d188,d178])). % 44.42/7.62 cnf(d190, plain, op(e3,e0) = e1 | op(e0,e1) = e1, inference(superposition, [status(thm)], [d189,c103])). % 44.42/7.62 cnf(d191, plain, op(e0,op(e3,e0)) = op(e3,e0), inference(resolution, [status(thm)], [d159,c133])). % 44.42/7.62 cnf(d192, plain, op(e0,e1) = op(e3,e0) | op(e0,e1) = e1, inference(superposition, [status(thm)], [d190,d191])). % 44.42/7.62 cnf(d193, plain, op(e0,e1) = e1 | op(e0,e1) = e1 | op(e0,e1) = e1, inference(superposition, [status(thm)], [d192,d190])). % 44.42/7.62 cnf(d194, plain, op(e1,e0) = e1, inference(demodulation, [status(thm)], [c103,d193])). % 44.42/7.62 cnf(d195, plain, op(e1,e1) = e0, inference(demodulation, [status(thm)], [c106,d194])). % 44.42/7.62 cnf(d196, plain, e2 != op(e3,e0), inference(demodulation, [status(thm)], [c53,d179])). % 44.42/7.62 cnf(d197, plain, op(e2,e3) = e3 | op(e3,e0) = e2 | op(e3,e2) = e2 | op(e3,e1) = e2, inference(superposition, [status(thm)], [c44,c117])). % 44.42/7.62 cnf(d198, plain, op(e2,e3) = e1 | op(e2,e3) = e3 | op(e3,e0) = e2 | op(e3,e2) = e2, inference(superposition, [status(thm)], [d197,c115])). % 44.42/7.62 cnf(d199, plain, op(e0,e2) != e2 | op(e2,e3) = e1 | op(e2,e3) = e3 | op(e3,e0) = e2, inference(superposition, [status(thm)], [d198,c62])). % 44.42/7.62 cnf(d200, plain, op(e2,e3) = e1 | op(e2,e3) = e3 | op(e3,e0) = e2, inference(resolution, [status(thm)], [d175,d199])). % 44.42/7.62 cnf(d201, plain, e2 != e2 | op(e2,e3) = e1 | op(e2,e3) = e3, inference(superposition, [status(thm)], [d200,d196])). % 44.42/7.62 cnf(d202, plain, op(e2,e3) = e1 | op(e2,e3) = e3, inference(equality_resolution, [status(thm)], [d201])). % 44.42/7.62 cnf(d203, plain, op(e2,e1) != e3 | op(e2,e3) = e1, inference(superposition, [status(thm)], [d202,c88])). % 44.42/7.62 cnf(d204, plain, e2 != op(e1,e2), inference(demodulation, [status(thm)], [c60,d175])). % 44.42/7.62 cnf(d205, plain, op(e1,e0) != e2, inference(demodulation, [status(thm)], [c51,d179])). % 44.42/7.62 cnf(d206, plain, op(e1,e2) = e2 | op(e1,e1) = e2 | op(e1,e3) = e2, inference(resolution, [status(thm)], [d205,c28])). % 44.42/7.62 cnf(d207, plain, op(e1,e2) = e2 | e0 = e2 | op(e1,e3) = e2, inference(demodulation, [status(thm)], [d206,d195])). % 44.42/7.62 cnf(d208, plain, op(e1,e2) = e2 | op(e1,e3) = e2, inference(resolution, [status(thm)], [c97,d207])). % 44.42/7.62 cnf(d209, plain, op(e2,e1) = e3 | op(e1,e2) = e2, inference(superposition, [status(thm)], [d208,c109])). % 44.42/7.62 cnf(d210, plain, e2 != e2 | op(e2,e1) = e3, inference(superposition, [status(thm)], [d209,d204])). % 44.42/7.62 cnf(d211, plain, op(e2,e1) = e3, inference(equality_resolution, [status(thm)], [d210])). % 44.42/7.62 cnf(d212, plain, op(e2,e3) = e1, inference(resolution, [status(thm)], [d211,d203])). % 44.42/7.62 cnf(d213, plain, e0 != op(e1,op(e2,e3)) | e1 != op(e2,e3), inference(demodulation, [status(thm)], [c139,d212])). % 44.42/7.62 cnf(d214, plain, e0 != op(e1,e1) | e1 != op(e2,e3), inference(demodulation, [status(thm)], [d213,d212])). % 44.42/7.62 cnf(d215, plain, e0 != op(e1,e1) | e1 != e1, inference(demodulation, [status(thm)], [d214,d212])). % 44.42/7.62 cnf(d216, plain, e0 != e0 | e1 != e1, inference(demodulation, [status(thm)], [d215,d195])). % 44.42/7.62 cnf(d217, plain, op(e0,op(e0,e1)) = op(e3,e0) | op(e0,e1) = e1, inference(superposition, [status(thm)], [d192,d191])). % 44.42/7.62 cnf(d218, plain, op(e0,e1) = op(e3,e0) | op(e0,e1) = e1, inference(demodulation, [status(thm)], [d217,d193])). % 44.42/7.62 cnf(d219, plain, e1 = op(e3,e0) | op(e0,e1) = e1, inference(demodulation, [status(thm)], [d218,d193])). % 44.42/7.62 cnf(d220, plain, e1 = op(e3,e0) | e1 = e1, inference(demodulation, [status(thm)], [d219,d193])). % 44.42/7.62 cnf(d221, plain, e1 != op(e3,e0), inference(demodulation, [status(thm)], [c52,d194])). % 44.42/7.62 cnf(d222, plain, e1 = e1, inference(resolution, [status(thm)], [d221,d220])). % 44.42/7.62 cnf(d223, plain, e0 != e0, inference(resolution, [status(thm)], [d222,d216])). % 44.42/7.62 cnf(d224, plain, $false, inference(resolution, [status(thm)], [d188,d223])). % 44.42/7.62 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------