%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 06:47:20 AM UTC 2026 % Result : Theorem 38.34s 10.49s % Output : CNFRefutation 38.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/5.38 % Computer : n016.cluster.edu % 0.09/5.38 % Model : x86_64 x86_64 % 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/5.38 % Memory : 8046.5625MB % 0.09/5.38 % OS : Linux 6.8.0-71-generic % 0.09/5.38 % CPULimit : 300 % 0.09/5.38 % WCLimit : 300 % 0.09/5.38 % DateTime : Sat Sep 26 21:09:53 UTC 2026 % 0.09/5.38 % CPUTime : % 0.09/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 38.34/10.49 % SZS status Theorem for theBenchmark.p % 38.34/10.49 % SZS output start CNFRefutation for theBenchmark.p % 38.34/10.49 fof(ax4, axiom, (op(e0,e0) != op(e1,e0) & (op(e0,e0) != op(e2,e0) & (op(e0,e0) != op(e3,e0) & (op(e0,e0) != op(e4,e0) & (op(e1,e0) != op(e2,e0) & (op(e1,e0) != op(e3,e0) & (op(e1,e0) != op(e4,e0) & (op(e2,e0) != op(e3,e0) & (op(e2,e0) != op(e4,e0) & (op(e3,e0) != op(e4,e0) & (op(e0,e1) != op(e1,e1) & (op(e0,e1) != op(e2,e1) & (op(e0,e1) != op(e3,e1) & (op(e0,e1) != op(e4,e1) & (op(e1,e1) != op(e2,e1) & (op(e1,e1) != op(e3,e1) & (op(e1,e1) != op(e4,e1) & (op(e2,e1) != op(e3,e1) & (op(e2,e1) != op(e4,e1) & (op(e3,e1) != op(e4,e1) & (op(e0,e2) != op(e1,e2) & (op(e0,e2) != op(e2,e2) & (op(e0,e2) != op(e3,e2) & (op(e0,e2) != op(e4,e2) & (op(e1,e2) != op(e2,e2) & (op(e1,e2) != op(e3,e2) & (op(e1,e2) != op(e4,e2) & (op(e2,e2) != op(e3,e2) & (op(e2,e2) != op(e4,e2) & (op(e3,e2) != op(e4,e2) & (op(e0,e3) != op(e1,e3) & (op(e0,e3) != op(e2,e3) & (op(e0,e3) != op(e3,e3) & (op(e0,e3) != op(e4,e3) & (op(e1,e3) != op(e2,e3) & (op(e1,e3) != op(e3,e3) & (op(e1,e3) != op(e4,e3) & (op(e2,e3) != op(e3,e3) & (op(e2,e3) != op(e4,e3) & (op(e3,e3) != op(e4,e3) & (op(e0,e4) != op(e1,e4) & (op(e0,e4) != op(e2,e4) & (op(e0,e4) != op(e3,e4) & (op(e0,e4) != op(e4,e4) & (op(e1,e4) != op(e2,e4) & (op(e1,e4) != op(e3,e4) & (op(e1,e4) != op(e4,e4) & (op(e2,e4) != op(e3,e4) & (op(e2,e4) != op(e4,e4) & (op(e3,e4) != op(e4,e4) & (op(e0,e0) != op(e0,e1) & (op(e0,e0) != op(e0,e2) & (op(e0,e0) != op(e0,e3) & (op(e0,e0) != op(e0,e4) & (op(e0,e1) != op(e0,e2) & (op(e0,e1) != op(e0,e3) & (op(e0,e1) != op(e0,e4) & (op(e0,e2) != op(e0,e3) & (op(e0,e2) != op(e0,e4) & (op(e0,e3) != op(e0,e4) & (op(e1,e0) != op(e1,e1) & (op(e1,e0) != op(e1,e2) & (op(e1,e0) != op(e1,e3) & (op(e1,e0) != op(e1,e4) & (op(e1,e1) != op(e1,e2) & (op(e1,e1) != op(e1,e3) & (op(e1,e1) != op(e1,e4) & (op(e1,e2) != op(e1,e3) & (op(e1,e2) != op(e1,e4) & (op(e1,e3) != op(e1,e4) & (op(e2,e0) != op(e2,e1) & (op(e2,e0) != op(e2,e2) & (op(e2,e0) != op(e2,e3) & (op(e2,e0) != op(e2,e4) & (op(e2,e1) != op(e2,e2) & (op(e2,e1) != op(e2,e3) & (op(e2,e1) != op(e2,e4) & (op(e2,e2) != op(e2,e3) & (op(e2,e2) != op(e2,e4) & (op(e2,e3) != op(e2,e4) & (op(e3,e0) != op(e3,e1) & (op(e3,e0) != op(e3,e2) & (op(e3,e0) != op(e3,e3) & (op(e3,e0) != op(e3,e4) & (op(e3,e1) != op(e3,e2) & (op(e3,e1) != op(e3,e3) & (op(e3,e1) != op(e3,e4) & (op(e3,e2) != op(e3,e3) & (op(e3,e2) != op(e3,e4) & (op(e3,e3) != op(e3,e4) & (op(e4,e0) != op(e4,e1) & (op(e4,e0) != op(e4,e2) & (op(e4,e0) != op(e4,e3) & (op(e4,e0) != op(e4,e4) & (op(e4,e1) != op(e4,e2) & (op(e4,e1) != op(e4,e3) & (op(e4,e1) != op(e4,e4) & (op(e4,e2) != op(e4,e3) & (op(e4,e2) != op(e4,e4) & op(e4,e3) != op(e4,e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 38.34/10.49 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 38.34/10.49 fof(ax6, axiom, (e0 = op(e1,op(op(e1,e1),op(e1,e1))) & (e2 = op(op(e1,e1),op(e1,e1)) & (e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) & e4 = op(e1,e1))))). % 38.34/10.49 fof(co1, conjecture, ~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = e4 | op(e4,e4) = e4)))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4))))))))))))))))))))))))))))))))). % 38.34/10.49 fof(negated_conjecture, negated_conjecture, ~~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = e4 | op(e4,e4) = e4)))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4)))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 38.34/10.49 cnf(c150, plain, op(e1,e1) != op(e1,e2), inference(clausification, [status(esa)], [ax4])). % 38.34/10.49 cnf(c186, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c187, plain, e0 != e2, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c188, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c190, plain, e1 != e2, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c191, plain, e1 != e3, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c192, plain, e1 != e4, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c193, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c194, plain, e2 != e4, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c195, plain, e3 != e4, inference(clausification, [status(esa)], [ax5])). % 38.34/10.49 cnf(c196, plain, e0 = op(e1,op(op(e1,e1),op(e1,e1))), inference(clausification, [status(esa)], [ax6])). % 38.34/10.49 cnf(c197, plain, e2 = op(op(e1,e1),op(e1,e1)), inference(clausification, [status(esa)], [ax6])). % 38.34/10.49 cnf(c198, plain, e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))), inference(clausification, [status(esa)], [ax6])). % 38.34/10.49 cnf(c199, plain, e4 = op(e1,e1), inference(clausification, [status(esa)], [ax6])). % 38.34/10.49 cnf(c200, plain, op(e2,e2) = e0 | op(e4,e4) = e0 | op(e1,e1) = e0 | op(e0,e0) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c201, plain, op(e2,e2) = e1 | op(e1,e1) = e1 | op(e3,e3) = e1 | op(e0,e0) = e1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c205, plain, X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | op(e4,e4) = e4 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c208, plain, ~X0 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c212, plain, ~X0 | op(e2,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c214, plain, ~X0 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c217, plain, ~X0 | op(e4,e4) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c221, plain, ~X0 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c223, plain, ~X0 | op(e3,e3) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c225, plain, ~X0 | op(e3,e3) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c226, plain, ~X0 | op(e3,e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c230, plain, ~X0 | op(e1,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c232, plain, ~X0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c233, plain, ~X0 | op(e0,e0) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c235, plain, ~X0 | op(e2,e2) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c239, plain, ~X0 | op(e3,e3) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c241, plain, ~X0 | op(e2,e2) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c243, plain, ~X0 | op(e2,e2) != e2, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c244, plain, ~X0 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c247, plain, ~X0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c251, plain, ~X0 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c253, plain, ~X0 | op(e1,e1) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c257, plain, ~X0 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c259, plain, ~X0 | op(e1,e1) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c261, plain, ~X0 | op(e1,e1) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c262, plain, ~X0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c266, plain, ~X0 | op(e4,e4) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c268, plain, ~X0 | op(e0,e0) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c269, plain, ~X0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c272, plain, ~X0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c275, plain, ~X0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c277, plain, ~X0 | op(e0,e0) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(c279, plain, ~X0 | op(e0,e0) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 38.34/10.49 cnf(d0, plain, e2 = op(e4,op(e1,e1)), inference(demodulation, [status(thm)], [c197,c199])). % 38.34/10.49 cnf(d1, plain, e2 = op(e4,e4), inference(demodulation, [status(thm)], [d0,c199])). % 38.34/10.49 cnf(d2, plain, e3 = op(op(e4,op(e1,e1)),op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [c198,c199])). % 38.34/10.49 cnf(d3, plain, e3 = op(op(e4,e4),op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [d2,c199])). % 38.34/10.49 cnf(d4, plain, e3 = op(e2,op(op(e1,e1),op(e1,e1))), inference(demodulation, [status(thm)], [d3,d1])). % 38.34/10.49 cnf(d5, plain, e3 = op(e2,op(e4,op(e1,e1))), inference(demodulation, [status(thm)], [d4,c199])). % 38.34/10.49 cnf(d6, plain, e3 = op(e2,op(e4,e4)), inference(demodulation, [status(thm)], [d5,c199])). % 38.34/10.49 cnf(d7, plain, e3 = op(e2,e2), inference(demodulation, [status(thm)], [d6,d1])). % 38.34/10.49 cnf(d8, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | op(e4,e4) = e1 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [c201,d7])). % 38.34/10.49 cnf(d9, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | e2 = e1 | op(e1,e1) = e1, inference(demodulation, [status(thm)], [d8,d1])). % 38.34/10.49 cnf(d10, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1 | e2 = e1 | e4 = e1, inference(demodulation, [status(thm)], [d9,c199])). % 38.34/10.49 cnf(d11, plain, e3 = e1 | ~'Ts16', inference(demodulation, [status(thm)], [c257,d7])). % 38.34/10.49 cnf(d12, plain, e2 = e0 | ~'Ts3', inference(demodulation, [status(thm)], [c217,d1])). % 38.34/10.49 cnf(d13, plain, e3 = e0 | ~'Ts21', inference(demodulation, [status(thm)], [c272,d7])). % 38.34/10.49 cnf(d14, plain, e4 = e3 | ~'Ts15', inference(demodulation, [status(thm)], [c253,c199])). % 38.34/10.49 cnf(d15, plain, e2 = e1 | ~'Ts2', inference(demodulation, [status(thm)], [c214,d1])). % 38.34/10.49 cnf(d16, plain, e2 = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts11' | 'Ts5' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(demodulation, [status(thm)], [c205,d1])). % 38.34/10.49 cnf(d17, plain, ~'Ts5' | ~'Ts5', inference(resolution, [status(thm)], [c223,c225])). % 38.34/10.49 cnf(d18, plain, e2 = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts11' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(resolution, [status(thm)], [d17,d16])). % 38.34/10.49 cnf(d19, plain, ~'Ts11' | ~'Ts11', inference(resolution, [status(thm)], [c241,c243])). % 38.34/10.49 cnf(d20, plain, e2 = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts17' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(resolution, [status(thm)], [d19,d18])). % 38.34/10.49 cnf(d21, plain, ~'Ts17' | ~'Ts17', inference(resolution, [status(thm)], [c259,c261])). % 38.34/10.49 cnf(d22, plain, e2 = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2' | 'Ts23', inference(resolution, [status(thm)], [d21,d20])). % 38.34/10.49 cnf(d23, plain, ~'Ts23' | ~'Ts23', inference(resolution, [status(thm)], [c279,c277])). % 38.34/10.49 cnf(d24, plain, e2 = e4 | 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d23,d22])). % 38.34/10.49 cnf(d25, plain, 'Ts4' | 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [c194,d24])). % 38.34/10.49 cnf(d26, plain, e2 = e3 | ~'Ts4', inference(demodulation, [status(thm)], [c221,d1])). % 38.34/10.49 cnf(d27, plain, ~'Ts4', inference(resolution, [status(thm)], [c193,d26])). % 38.34/10.49 cnf(d28, plain, 'Ts13' | 'Ts6' | 'Ts1' | 'Ts0' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d27,d25])). % 38.34/10.49 cnf(d29, plain, e2 = e3 | ~'Ts0', inference(demodulation, [status(thm)], [c208,d1])). % 38.34/10.49 cnf(d30, plain, ~'Ts0', inference(resolution, [status(thm)], [c193,d29])). % 38.34/10.49 cnf(d31, plain, 'Ts13' | 'Ts6' | 'Ts1' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts9' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d30,d28])). % 38.34/10.49 cnf(d32, plain, e3 = e4 | ~'Ts9', inference(demodulation, [status(thm)], [c235,d7])). % 38.34/10.49 cnf(d33, plain, ~'Ts9', inference(resolution, [status(thm)], [c195,d32])). % 38.34/10.49 cnf(d34, plain, 'Ts13' | 'Ts6' | 'Ts1' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d33,d31])). % 38.34/10.49 cnf(d35, plain, e3 = e4 | ~'Ts1', inference(demodulation, [status(thm)], [c212,d7])). % 38.34/10.49 cnf(d36, plain, ~'Ts1', inference(resolution, [status(thm)], [c195,d35])). % 38.34/10.49 cnf(d37, plain, 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts22' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d36,d34])). % 38.34/10.49 cnf(d38, plain, e4 = e0 | ~'Ts22', inference(demodulation, [status(thm)], [c275,c199])). % 38.34/10.49 cnf(d39, plain, e0 = op(e1,op(e4,op(e1,e1))), inference(demodulation, [status(thm)], [c196,c199])). % 38.34/10.49 cnf(d40, plain, e0 = op(e1,op(e4,e4)), inference(demodulation, [status(thm)], [d39,c199])). % 38.34/10.49 cnf(d41, plain, e0 = op(e1,e2), inference(demodulation, [status(thm)], [d40,d1])). % 38.34/10.49 cnf(d42, plain, e4 != op(e1,e2), inference(demodulation, [status(thm)], [c150,c199])). % 38.34/10.49 cnf(d43, plain, e4 != e0, inference(demodulation, [status(thm)], [d42,d41])). % 38.34/10.49 cnf(d44, plain, ~'Ts22', inference(resolution, [status(thm)], [d43,d38])). % 38.34/10.49 cnf(d45, plain, 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts18' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d44,d37])). % 38.34/10.49 cnf(d46, plain, e4 = e0 | ~'Ts18', inference(demodulation, [status(thm)], [c262,c199])). % 38.34/10.49 cnf(d47, plain, ~'Ts18', inference(resolution, [status(thm)], [d43,d46])). % 38.34/10.49 cnf(d48, plain, 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | 'Ts2', inference(resolution, [status(thm)], [d47,d45])). % 38.34/10.49 cnf(d49, plain, 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts14' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15' | e2 = e1, inference(resolution, [status(thm)], [d48,d15])). % 38.34/10.49 cnf(d50, plain, e2 = e1 | ~'Ts14', inference(demodulation, [status(thm)], [c251,d1])). % 38.34/10.49 cnf(d51, plain, e2 = e1 | e2 = e1 | 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | 'Ts15', inference(resolution, [status(thm)], [d50,d49])). % 38.34/10.49 cnf(d52, plain, e2 = e1 | 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts7' | 'Ts21' | 'Ts20' | 'Ts10' | e4 = e3, inference(resolution, [status(thm)], [d51,d14])). % 38.34/10.49 cnf(d53, plain, e4 = e3 | ~'Ts7', inference(demodulation, [status(thm)], [c230,c199])). % 38.34/10.49 cnf(d54, plain, e4 = e3 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21' | 'Ts20' | 'Ts10', inference(resolution, [status(thm)], [d53,d52])). % 38.34/10.49 cnf(d55, plain, e2 = e1 | e4 = e3 | 'Ts13' | 'Ts6' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21' | 'Ts20' | op(e3,e3) = e2, inference(resolution, [status(thm)], [d54,c239])). % 38.34/10.49 cnf(d56, plain, op(e3,e3) = e2 | op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21' | 'Ts20', inference(resolution, [status(thm)], [c226,d55])). % 38.34/10.49 cnf(d57, plain, op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21' | op(e3,e3) = e0, inference(resolution, [status(thm)], [d56,c269])). % 38.34/10.49 cnf(d58, plain, op(e3,e3) = e0 | op(e3,e3) = e0 | op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21', inference(resolution, [status(thm)], [c232,d57])). % 38.34/10.49 cnf(d59, plain, op(e3,e3) = e0 | op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | e3 = e0, inference(resolution, [status(thm)], [d58,d13])). % 38.34/10.49 cnf(d60, plain, e3 = e0 | ~'Ts13', inference(demodulation, [status(thm)], [c247,d7])). % 38.34/10.49 cnf(d61, plain, e3 = e0 | op(e3,e3) = e0 | op(e3,e3) = e2 | e3 = e0 | e2 = e1 | e4 = e3 | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3', inference(resolution, [status(thm)], [d60,d59])). % 38.34/10.49 cnf(d62, plain, op(e3,e3) = e0 | op(e3,e3) = e2 | e3 = e0 | e2 = e1 | e4 = e3 | 'Ts19' | 'Ts12' | 'Ts16' | e2 = e0, inference(resolution, [status(thm)], [d61,d12])). % 38.34/10.49 cnf(d63, plain, e2 = e0 | ~'Ts19', inference(demodulation, [status(thm)], [c266,d1])). % 38.34/10.49 cnf(d64, plain, e2 = e0 | op(e3,e3) = e0 | op(e3,e3) = e2 | e3 = e0 | e2 = e0 | e2 = e1 | e4 = e3 | 'Ts12' | 'Ts16', inference(resolution, [status(thm)], [d63,d62])). % 38.34/10.49 cnf(d65, plain, op(e3,e3) = e0 | op(e3,e3) = e2 | e3 = e0 | e2 = e0 | e2 = e1 | e4 = e3 | 'Ts12' | e3 = e1, inference(resolution, [status(thm)], [d64,d11])). % 38.34/10.49 cnf(d66, plain, e3 = e1 | ~'Ts12', inference(demodulation, [status(thm)], [c244,d7])). % 38.34/10.49 cnf(d67, plain, e3 = e1 | op(e3,e3) = e0 | op(e3,e3) = e2 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3, inference(resolution, [status(thm)], [d66,d65])). % 38.34/10.49 cnf(d68, plain, e2 = e1 | op(e0,e0) = e1 | e3 = e1 | e2 = e1 | e4 = e1 | op(e3,e3) = e0 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3, inference(superposition, [status(thm)], [d67,d10])). % 38.34/10.49 cnf(d69, plain, e0 = e1 | op(e0,e0) = e1 | e3 = e1 | e2 = e1 | e4 = e1 | op(e0,e0) = e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1, inference(superposition, [status(thm)], [d68,d10])). % 38.34/10.49 cnf(d70, plain, op(e0,e0) = e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1, inference(resolution, [status(thm)], [c186,d69])). % 38.34/10.49 cnf(d71, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | op(e4,e4) = e0 | op(e1,e1) = e0, inference(demodulation, [status(thm)], [c200,d7])). % 38.34/10.49 cnf(d72, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | e2 = e0 | op(e1,e1) = e0, inference(demodulation, [status(thm)], [d71,d1])). % 38.34/10.49 cnf(d73, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | e2 = e0 | e4 = e0, inference(demodulation, [status(thm)], [d72,c199])). % 38.34/10.49 cnf(d74, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0 | e2 = e0, inference(resolution, [status(thm)], [d43,d73])). % 38.34/10.49 cnf(d75, plain, op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts8' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21' | op(e0,e0) = e3, inference(resolution, [status(thm)], [d56,c268])). % 38.34/10.49 cnf(d76, plain, op(e0,e0) = e3 | op(e0,e0) = e3 | op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | 'Ts21', inference(resolution, [status(thm)], [c233,d75])). % 38.34/10.49 cnf(d77, plain, op(e0,e0) = e3 | op(e3,e3) = e2 | e2 = e1 | e4 = e3 | 'Ts13' | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3' | e3 = e0, inference(resolution, [status(thm)], [d76,d13])). % 38.34/10.49 cnf(d78, plain, e3 = e0 | op(e0,e0) = e3 | op(e3,e3) = e2 | e3 = e0 | e2 = e1 | e4 = e3 | 'Ts19' | 'Ts12' | 'Ts16' | 'Ts3', inference(resolution, [status(thm)], [d60,d77])). % 38.34/10.49 cnf(d79, plain, op(e0,e0) = e3 | op(e3,e3) = e2 | e3 = e0 | e2 = e1 | e4 = e3 | 'Ts19' | 'Ts12' | 'Ts16' | e2 = e0, inference(resolution, [status(thm)], [d78,d12])). % 38.34/10.49 cnf(d80, plain, e2 = e0 | op(e0,e0) = e3 | op(e3,e3) = e2 | e3 = e0 | e2 = e0 | e2 = e1 | e4 = e3 | 'Ts12' | 'Ts16', inference(resolution, [status(thm)], [d63,d79])). % 38.34/10.49 cnf(d81, plain, op(e0,e0) = e3 | op(e3,e3) = e2 | e3 = e0 | e2 = e0 | e2 = e1 | e4 = e3 | 'Ts12' | e3 = e1, inference(resolution, [status(thm)], [d80,d11])). % 38.34/10.49 cnf(d82, plain, e3 = e1 | op(e0,e0) = e3 | op(e3,e3) = e2 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3, inference(resolution, [status(thm)], [d66,d81])). % 38.34/10.49 cnf(d83, plain, e2 = e0 | op(e0,e0) = e0 | e3 = e0 | e2 = e0 | op(e0,e0) = e3 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3, inference(superposition, [status(thm)], [d82,d74])). % 38.34/10.49 cnf(d84, plain, e3 = e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1 | op(e0,e0) = e0 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3, inference(superposition, [status(thm)], [d83,d70])). % 38.34/10.49 cnf(d85, plain, e0 = e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1, inference(superposition, [status(thm)], [d84,d70])). % 38.34/10.49 cnf(d86, plain, e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e3 | e4 = e1, inference(resolution, [status(thm)], [c186,d85])). % 38.34/10.49 cnf(d87, plain, e3 != e3 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e1, inference(superposition, [status(thm)], [d86,c195])). % 38.34/10.49 cnf(d88, plain, e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1 | e4 = e1, inference(equality_resolution, [status(thm)], [d87])). % 38.34/10.49 cnf(d89, plain, e1 != e1 | e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1, inference(superposition, [status(thm)], [d88,c192])). % 38.34/10.49 cnf(d90, plain, e3 = e0 | e3 = e1 | e2 = e0 | e2 = e1, inference(equality_resolution, [status(thm)], [d89])). % 38.34/10.49 cnf(d91, plain, e0 != e0 | e3 = e0 | e3 = e1 | e2 = e1, inference(superposition, [status(thm)], [d90,c187])). % 38.34/10.49 cnf(d92, plain, e3 = e0 | e3 = e1 | e2 = e1, inference(equality_resolution, [status(thm)], [d91])). % 38.34/10.49 cnf(d93, plain, e1 != e1 | e3 = e0 | e3 = e1, inference(superposition, [status(thm)], [d92,c190])). % 38.34/10.49 cnf(d94, plain, e3 = e0 | e3 = e1, inference(equality_resolution, [status(thm)], [d93])). % 38.34/10.49 cnf(d95, plain, e0 != e0 | e3 = e1, inference(superposition, [status(thm)], [d94,c188])). % 38.34/10.49 cnf(d96, plain, e3 = e1, inference(equality_resolution, [status(thm)], [d95])). % 38.34/10.49 cnf(d97, plain, e1 != e1, inference(demodulation, [status(thm)], [c191,d96])). % 38.34/10.49 cnf(d98, plain, $false, inference(equality_resolution, [status(thm)], [d97])). % 38.34/10.49 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------