%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : GEO610+1 : TPTP v9.3.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n020.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 07:15:30 AM UTC 2026 % Result : Theorem 47.03s 25.41s % Output : CNFRefutation 47.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : GEO610+1 : TPTP v9.3.1. Released v7.5.0. % 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.43 % Computer : n020.cluster.edu % 0.18/0.43 % Model : x86_64 x86_64 % 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.43 % Memory : 8046.5625MB % 0.18/0.43 % OS : Linux 6.8.0-71-generic % 0.18/0.43 % CPULimit : 300 % 0.18/0.43 % WCLimit : 300 % 0.18/0.43 % DateTime : Fri Sep 25 13:45:19 UTC 2026 % 0.18/0.44 % CPUTime : % 0.18/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.03/25.41 % SZS status Theorem for theBenchmark.p % 47.03/25.41 % SZS output start CNFRefutation for theBenchmark.p % 47.03/25.41 fof(ruleD1, axiom, ! [X0] : ! [X1] : ! [X2] : ((coll(X0,X1,X2) => coll(X0,X2,X1)))). % 47.03/25.41 fof(ruleD2, axiom, ! [X0] : ! [X1] : ! [X2] : ((coll(X0,X1,X2) => coll(X1,X0,X2)))). % 47.03/25.41 fof(ruleD3, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((coll(X0,X1,X2) & coll(X0,X1,X3)) => coll(X2,X3,X0)))). % 47.03/25.41 fof(ruleD4, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((para(X0,X1,X2,X3) => para(X0,X1,X3,X2)))). % 47.03/25.41 fof(ruleD8, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((perp(X0,X1,X2,X3) => perp(X2,X3,X0,X1)))). % 47.03/25.41 fof(ruleD9, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((perp(X0,X1,X2,X3) & perp(X2,X3,X4,X5)) => para(X0,X1,X4,X5)))). % 47.03/25.41 fof(ruleD11, axiom, ! [X0] : ! [X1] : ! [X2] : ((midp(X2,X1,X0) => midp(X2,X0,X1)))). % 47.03/25.41 fof(ruleD12, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((cong(X3,X0,X3,X1) & cong(X3,X0,X3,X2)) => circle(X3,X0,X1,X2)))). % 47.03/25.41 fof(ruleD14, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((cyclic(X0,X1,X2,X3) => cyclic(X0,X1,X3,X2)))). % 47.03/25.41 fof(ruleD15, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((cyclic(X0,X1,X2,X3) => cyclic(X0,X2,X1,X3)))). % 47.03/25.41 fof(ruleD16, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((cyclic(X0,X1,X2,X3) => cyclic(X1,X0,X2,X3)))). % 47.03/25.41 fof(ruleD18, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : ((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) => eqangle(X1,X0,X2,X3,X4,X5,X6,X7)))). % 47.03/25.41 fof(ruleD19, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : ((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) => eqangle(X2,X3,X0,X1,X6,X7,X4,X5)))). % 47.03/25.41 fof(ruleD20, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : ((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) => eqangle(X4,X5,X6,X7,X0,X1,X2,X3)))). % 47.03/25.41 fof(ruleD21, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : ((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) => eqangle(X0,X1,X4,X5,X2,X3,X6,X7)))). % 47.03/25.41 fof(ruleD22, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : ! [X8] : ! [X9] : ! [X10] : ! [X11] : (((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) & eqangle(X4,X5,X6,X7,X8,X9,X10,X11)) => eqangle(X0,X1,X2,X3,X8,X9,X10,X11)))). % 47.03/25.41 fof(ruleD39, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ((eqangle(X0,X1,X4,X5,X2,X3,X4,X5) => para(X0,X1,X2,X3)))). % 47.03/25.41 fof(ruleD40, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ((para(X0,X1,X2,X3) => eqangle(X0,X1,X4,X5,X2,X3,X4,X5)))). % 47.03/25.41 fof(ruleD41, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((cyclic(X0,X1,X2,X3) => eqangle(X2,X0,X2,X1,X3,X0,X3,X1)))). % 47.03/25.41 fof(ruleD42b, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((eqangle(X2,X0,X2,X1,X3,X0,X3,X1) & coll(X2,X3,X1)) => cyclic(X0,X1,X2,X3)))). % 47.03/25.41 fof(ruleD43, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((cyclic(X0,X1,X2,X3) & (cyclic(X0,X1,X2,X4) & (cyclic(X0,X1,X2,X5) & eqangle(X2,X0,X2,X1,X5,X3,X5,X4)))) => cong(X0,X1,X3,X4)))). % 47.03/25.41 fof(ruleD45, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((midp(X3,X0,X1) & (para(X3,X4,X1,X2) & coll(X4,X0,X2))) => midp(X4,X0,X2)))). % 47.03/25.41 fof(ruleD46, axiom, ! [X0] : ! [X1] : ! [X2] : ((cong(X2,X0,X2,X1) => eqangle(X2,X0,X0,X1,X0,X1,X2,X1)))). % 47.03/25.41 fof(ruleD50, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((circle(X3,X0,X1,X2) & midp(X4,X1,X2)) => eqangle(X0,X1,X0,X2,X3,X1,X3,X4)))). % 47.03/25.41 fof(ruleD66, axiom, ! [X0] : ! [X1] : ! [X2] : ((para(X0,X1,X0,X2) => coll(X0,X1,X2)))). % 47.03/25.41 fof(ruleD67, axiom, ! [X0] : ! [X1] : ! [X2] : (((cong(X0,X1,X0,X2) & coll(X0,X1,X2)) => midp(X0,X1,X2)))). % 47.03/25.41 fof(ruleD68, axiom, ! [X0] : ! [X1] : ! [X2] : ((midp(X0,X1,X2) => cong(X0,X1,X0,X2)))). % 47.03/25.41 fof(ruleD73, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : (((eqangle(X0,X1,X2,X3,X4,X5,X6,X7) & para(X4,X5,X6,X7)) => para(X0,X1,X2,X3)))). % 47.03/25.41 fof(exemplo6GDDFULL618072, conjecture, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : (((circle(X3,X0,X1,X2) & (circle(X3,X0,X4,X7) & (perp(X5,X4,X0,X2) & (coll(X5,X0,X2) & (perp(X6,X4,X0,X1) & coll(X6,X0,X1)))))) => (eqangle(X5,X4,X4,X6,X2,X4,X4,X1) & ((eqangle(X4,X5,X5,X6,X4,X2,X2,X1) | eqangle(X5,X4,X4,X6,X2,X4,X4,X1)) & ((eqangle(X4,X5,X5,X6,X4,X1,X1,X2) | eqangle(X5,X4,X4,X6,X4,X2,X2,X1)) & ((eqangle(X4,X5,X5,X6,X2,X4,X4,X1) | eqangle(X5,X4,X4,X6,X4,X2,X2,X1)) & ((eqangle(X4,X5,X5,X6,X4,X1,X1,X2) | eqangle(X5,X4,X4,X6,X4,X1,X1,X2)) & ((eqangle(X4,X5,X5,X6,X2,X4,X4,X1) | eqangle(X5,X4,X4,X6,X4,X1,X1,X2)) & eqangle(X4,X5,X5,X6,X4,X2,X2,X1)))))))))). % 47.03/25.41 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : (((circle(X3,X0,X1,X2) & (circle(X3,X0,X4,X7) & (perp(X5,X4,X0,X2) & (coll(X5,X0,X2) & (perp(X6,X4,X0,X1) & coll(X6,X0,X1)))))) => (eqangle(X5,X4,X4,X6,X2,X4,X4,X1) & ((eqangle(X4,X5,X5,X6,X4,X2,X2,X1) | eqangle(X5,X4,X4,X6,X2,X4,X4,X1)) & ((eqangle(X4,X5,X5,X6,X4,X1,X1,X2) | eqangle(X5,X4,X4,X6,X4,X2,X2,X1)) & ((eqangle(X4,X5,X5,X6,X2,X4,X4,X1) | eqangle(X5,X4,X4,X6,X4,X2,X2,X1)) & ((eqangle(X4,X5,X5,X6,X4,X1,X1,X2) | eqangle(X5,X4,X4,X6,X4,X1,X1,X2)) & ((eqangle(X4,X5,X5,X6,X2,X4,X4,X1) | eqangle(X5,X4,X4,X6,X4,X1,X1,X2)) & eqangle(X4,X5,X5,X6,X4,X2,X2,X1))))))))), inference(negate_conjecture, [status(cth)], [exemplo6GDDFULL618072])). % 47.03/25.41 cnf(c0, plain, ~coll(X0,X1,X2) | coll(X0,X2,X1), inference(clausification, [status(esa)], [ruleD1])). % 47.03/25.41 cnf(c1, plain, ~coll(X0,X1,X2) | coll(X1,X0,X2), inference(clausification, [status(esa)], [ruleD2])). % 47.03/25.41 cnf(c2, plain, ~coll(X0,X1,X2) | ~coll(X0,X1,X3) | coll(X2,X3,X0), inference(clausification, [status(esa)], [ruleD3])). % 47.03/25.41 cnf(c3, plain, ~para(X0,X1,X2,X3) | para(X0,X1,X3,X2), inference(clausification, [status(esa)], [ruleD4])). % 47.03/25.41 cnf(c7, plain, ~perp(X0,X1,X2,X3) | perp(X2,X3,X0,X1), inference(clausification, [status(esa)], [ruleD8])). % 47.03/25.41 cnf(c8, plain, ~perp(X0,X1,X2,X3) | ~perp(X2,X3,X4,X5) | para(X0,X1,X4,X5), inference(clausification, [status(esa)], [ruleD9])). % 47.03/25.41 cnf(c10, plain, ~midp(X0,X1,X2) | midp(X0,X2,X1), inference(clausification, [status(esa)], [ruleD11])). % 47.03/25.41 cnf(c11, plain, ~cong(X0,X1,X0,X2) | ~cong(X0,X1,X0,X3) | circle(X0,X1,X2,X3), inference(clausification, [status(esa)], [ruleD12])). % 47.03/25.41 cnf(c13, plain, ~cyclic(X0,X1,X2,X3) | cyclic(X0,X1,X3,X2), inference(clausification, [status(esa)], [ruleD14])). % 47.03/25.41 cnf(c14, plain, ~cyclic(X0,X1,X2,X3) | cyclic(X0,X2,X1,X3), inference(clausification, [status(esa)], [ruleD15])). % 47.03/25.41 cnf(c15, plain, ~cyclic(X0,X1,X2,X3) | cyclic(X1,X0,X2,X3), inference(clausification, [status(esa)], [ruleD16])). % 47.03/25.41 cnf(c17, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | eqangle(X1,X0,X2,X3,X4,X5,X6,X7), inference(clausification, [status(esa)], [ruleD18])). % 47.03/25.41 cnf(c18, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | eqangle(X2,X3,X0,X1,X6,X7,X4,X5), inference(clausification, [status(esa)], [ruleD19])). % 47.03/25.41 cnf(c19, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | eqangle(X4,X5,X6,X7,X0,X1,X2,X3), inference(clausification, [status(esa)], [ruleD20])). % 47.03/25.41 cnf(c20, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | eqangle(X0,X1,X4,X5,X2,X3,X6,X7), inference(clausification, [status(esa)], [ruleD21])). % 47.03/25.41 cnf(c21, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | ~eqangle(X4,X5,X6,X7,X8,X9,X10,X11) | eqangle(X0,X1,X2,X3,X8,X9,X10,X11), inference(clausification, [status(esa)], [ruleD22])). % 47.03/25.41 cnf(c38, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X2,X3) | para(X0,X1,X4,X5), inference(clausification, [status(esa)], [ruleD39])). % 47.03/25.41 cnf(c39, plain, ~para(X0,X1,X2,X3) | eqangle(X0,X1,X4,X5,X2,X3,X4,X5), inference(clausification, [status(esa)], [ruleD40])). % 47.03/25.41 cnf(c40, plain, ~cyclic(X0,X1,X2,X3) | eqangle(X2,X0,X2,X1,X3,X0,X3,X1), inference(clausification, [status(esa)], [ruleD41])). % 47.03/25.41 cnf(c42, plain, ~eqangle(X0,X1,X0,X2,X3,X1,X3,X2) | ~coll(X0,X3,X2) | cyclic(X1,X2,X0,X3), inference(clausification, [status(esa)], [ruleD42b])). % 47.03/25.41 cnf(c43, plain, ~cyclic(X0,X1,X2,X3) | cong(X0,X1,X4,X3) | ~cyclic(X0,X1,X2,X4) | ~cyclic(X0,X1,X2,X5) | ~eqangle(X2,X0,X2,X1,X5,X4,X5,X3), inference(clausification, [status(esa)], [ruleD43])). % 47.03/25.41 cnf(c45, plain, ~midp(X0,X1,X2) | ~para(X0,X3,X2,X4) | ~coll(X3,X1,X4) | midp(X3,X1,X4), inference(clausification, [status(esa)], [ruleD45])). % 47.03/25.41 cnf(c46, plain, ~cong(X0,X1,X0,X2) | eqangle(X0,X1,X1,X2,X1,X2,X0,X2), inference(clausification, [status(esa)], [ruleD46])). % 47.03/25.41 cnf(c50, plain, ~circle(X0,X1,X2,X3) | ~midp(X4,X2,X3) | eqangle(X1,X2,X1,X3,X0,X2,X0,X4), inference(clausification, [status(esa)], [ruleD50])). % 47.03/25.41 cnf(c66, plain, ~para(X0,X1,X0,X2) | coll(X0,X1,X2), inference(clausification, [status(esa)], [ruleD66])). % 47.03/25.41 cnf(c67, plain, ~cong(X0,X1,X0,X2) | ~coll(X0,X1,X2) | midp(X0,X1,X2), inference(clausification, [status(esa)], [ruleD67])). % 47.03/25.41 cnf(c68, plain, ~midp(X0,X1,X2) | cong(X0,X1,X0,X2), inference(clausification, [status(esa)], [ruleD68])). % 47.03/25.41 cnf(c73, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | ~para(X4,X5,X6,X7) | para(X0,X1,X2,X3), inference(clausification, [status(esa)], [ruleD73])). % 47.03/25.41 cnf(c115, plain, perp(sK529,sK528,sK524,sK526), inference(clausification, [status(esa)], [negated_conjecture])). % 47.03/25.41 cnf(c120, plain, ~eqangle(sK529,sK528,sK528,sK530,sK526,sK528,sK528,sK525) | ~X0(sK525,sK526,sK528,sK529,sK530), inference(clausification, [status(esa)], [negated_conjecture])). % 47.03/25.41 cnf(c121, plain, X0(X1,X2,X3,X4,X5) | ~eqangle(X3,X4,X4,X5,X3,X1,X1,X2) | ~eqangle(X3,X4,X4,X5,X2,X3,X3,X1) | ~eqangle(X3,X4,X4,X5,X3,X2,X2,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 47.03/25.41 cnf(c128, plain, X0(X1,X2,X3,X4,X5) | ~eqangle(X4,X3,X3,X5,X3,X2,X2,X1) | ~X6(X1,X2,X3,X4,X5), inference(clausification, [status(esa)], [negated_conjecture])). % 47.03/25.41 cnf(d0, plain, ~para(X0,X1,X2,X3) | ~eqangle(X2,X3,X4,X5,X6,X7,X8,X9) | eqangle(X0,X1,X4,X5,X6,X7,X8,X9), inference(resolution, [status(thm)], [c39,c21])). % 47.03/25.41 cnf(d1, plain, ~midp(X0,X1,X2) | ~circle(X3,X4,X1,X2) | eqangle(X4,X1,X3,X1,X4,X2,X3,X0), inference(resolution, [status(thm)], [c50,c20])). % 47.03/25.41 cnf(d2, plain, ~midp(X0,X1,X2) | ~circle(X3,X4,X1,X2) | ~para(X5,X6,X4,X1) | eqangle(X5,X6,X3,X1,X4,X2,X3,X0), inference(resolution, [status(thm)], [d1,d0])). % 47.03/25.41 cnf(d3, plain, ~para(sK529,sK528,sK526,sK530) | ~midp(sK525,sK530,sK528) | ~circle(sK528,sK526,sK530,sK528) | ~'Ts523'(sK525,sK526,sK528,sK529,sK530), inference(resolution, [status(thm)], [d2,c120])). % 47.03/25.41 cnf(d4, plain, ~cong(X0,X0,X0,X1) | para(X0,X0,X0,X1), inference(resolution, [status(thm)], [c46,c38])). % 47.03/25.41 cnf(d5, plain, para(X0,X0,X0,X1) | ~midp(X0,X0,X1), inference(resolution, [status(thm)], [d4,c68])). % 47.03/25.41 cnf(d6, plain, ~midp(X0,X0,X1) | ~coll(X0,X2,X1) | midp(X0,X2,X1) | ~midp(X0,X2,X0), inference(resolution, [status(thm)], [d5,c45])). % 47.03/25.41 cnf(d7, plain, perp(sK524,sK526,sK529,sK528), inference(resolution, [status(thm)], [c115,c7])). % 47.03/25.41 cnf(d8, plain, para(X0,X1,sK524,sK526) | ~perp(X0,X1,sK529,sK528), inference(resolution, [status(thm)], [c115,c8])). % 47.03/25.41 cnf(d9, plain, para(sK524,sK526,sK524,sK526), inference(resolution, [status(thm)], [d8,d7])). % 47.03/25.41 cnf(d10, plain, ~para(X0,X1,X2,X3) | eqangle(X4,X5,X0,X1,X4,X5,X2,X3), inference(resolution, [status(thm)], [c39,c18])). % 47.03/25.41 cnf(d11, plain, ~para(X0,X1,X0,X1) | para(X2,X3,X2,X3), inference(resolution, [status(thm)], [d10,c38])). % 47.03/25.41 cnf(d12, plain, para(X0,X1,X0,X1), inference(resolution, [status(thm)], [d11,d9])). % 47.03/25.41 cnf(d13, plain, coll(X0,X1,X1), inference(resolution, [status(thm)], [d12,c66])). % 47.03/25.41 cnf(d14, plain, coll(X0,X1,X0), inference(resolution, [status(thm)], [d13,c1])). % 47.03/25.41 cnf(d15, plain, coll(X0,X0,X1), inference(resolution, [status(thm)], [d14,c0])). % 47.03/25.41 cnf(d16, plain, coll(X0,X1,X2) | ~coll(X2,X2,X0), inference(resolution, [status(thm)], [d15,c2])). % 47.03/25.41 cnf(d17, plain, coll(X0,X1,X2), inference(resolution, [status(thm)], [d15,d16])). % 47.03/25.41 cnf(d18, plain, midp(X0,X1,X2) | ~midp(X0,X1,X0) | ~midp(X0,X0,X2), inference(resolution, [status(thm)], [d17,d6])). % 47.03/25.41 cnf(d19, plain, midp(X0,X1,X2) | ~cong(X0,X1,X0,X2), inference(resolution, [status(thm)], [d17,c67])). % 47.03/25.41 cnf(d20, plain, ~cyclic(X0,X1,X2,X3) | eqangle(X2,X1,X2,X0,X3,X1,X3,X0), inference(resolution, [status(thm)], [c40,c18])). % 47.03/25.41 cnf(d21, plain, ~cyclic(X0,X1,X2,X3) | eqangle(X1,X2,X2,X0,X3,X1,X3,X0), inference(resolution, [status(thm)], [d20,c17])). % 47.03/25.41 cnf(d22, plain, ~cyclic(X0,X1,X1,X2) | cong(X1,X0,X1,X0) | ~cyclic(X1,X0,X1,X1) | ~cyclic(X1,X0,X1,X2) | ~cyclic(X1,X0,X1,X0), inference(resolution, [status(thm)], [d21,c43])). % 47.03/25.41 cnf(d23, plain, ~coll(X0,X0,X1) | cyclic(X2,X1,X0,X0) | ~para(X0,X2,X0,X2), inference(resolution, [status(thm)], [c42,c39])). % 47.03/25.41 cnf(d24, plain, ~coll(X0,X0,X1) | cyclic(X2,X1,X0,X0), inference(resolution, [status(thm)], [d12,d23])). % 47.03/25.41 cnf(d25, plain, cyclic(X0,X1,X2,X2), inference(resolution, [status(thm)], [d17,d24])). % 47.03/25.41 cnf(d26, plain, cyclic(X0,X1,X2,X1), inference(resolution, [status(thm)], [d25,c14])). % 47.03/25.41 cnf(d27, plain, cong(X0,X1,X0,X1) | ~cyclic(X0,X1,X0,X2) | ~cyclic(X0,X1,X0,X0) | ~cyclic(X1,X0,X0,X2), inference(resolution, [status(thm)], [d26,d22])). % 47.03/25.41 cnf(d28, plain, cyclic(X0,X1,X1,X2), inference(resolution, [status(thm)], [d26,c13])). % 47.03/25.41 cnf(d29, plain, cong(X0,X1,X0,X1) | ~cyclic(X0,X1,X0,X2) | ~cyclic(X0,X1,X0,X0), inference(resolution, [status(thm)], [d28,d27])). % 47.03/25.41 cnf(d30, plain, cong(X0,X1,X0,X1) | ~cyclic(X0,X1,X0,X2), inference(resolution, [status(thm)], [d25,d29])). % 47.03/25.41 cnf(d31, plain, cyclic(X0,X1,X0,X2), inference(resolution, [status(thm)], [d28,c15])). % 47.03/25.41 cnf(d32, plain, cong(X0,X1,X0,X1), inference(resolution, [status(thm)], [d31,d30])). % 47.03/25.41 cnf(d33, plain, midp(X0,X1,X1), inference(resolution, [status(thm)], [d32,d19])). % 47.03/25.41 cnf(d34, plain, ~coll(X0,X1,X0) | midp(X0,X1,X0) | ~midp(X2,X1,X2), inference(resolution, [status(thm)], [d12,c45])). % 47.03/25.41 cnf(d35, plain, ~midp(X0,X1,X0) | midp(X2,X1,X2), inference(resolution, [status(thm)], [d17,d34])). % 47.03/25.41 cnf(d36, plain, midp(X0,X1,X0), inference(resolution, [status(thm)], [d35,d33])). % 47.03/25.41 cnf(d37, plain, midp(X0,X1,X2) | ~midp(X0,X0,X2), inference(resolution, [status(thm)], [d36,d18])). % 47.03/25.41 cnf(d38, plain, midp(X0,X0,X1), inference(resolution, [status(thm)], [d36,c10])). % 47.03/25.41 cnf(d39, plain, midp(X0,X1,X2), inference(resolution, [status(thm)], [d38,d37])). % 47.03/25.41 cnf(d40, plain, ~para(sK529,sK528,sK526,sK530) | ~circle(sK528,sK526,sK530,sK528) | ~'Ts523'(sK525,sK526,sK528,sK529,sK530), inference(resolution, [status(thm)], [d39,d3])). % 47.03/25.41 cnf(d41, plain, ~para(X0,X1,X2,X3) | eqangle(X2,X3,X4,X5,X0,X1,X4,X5), inference(resolution, [status(thm)], [c39,c19])). % 47.03/25.41 cnf(d42, plain, ~para(X0,X1,X2,X3) | ~para(X0,X1,X4,X5) | para(X2,X3,X4,X5), inference(resolution, [status(thm)], [d41,c73])). % 47.03/25.41 cnf(d43, plain, ~midp(X0,X0,X1) | para(X0,X1,X2,X3) | ~para(X0,X0,X2,X3), inference(resolution, [status(thm)], [d5,d42])). % 47.03/25.41 cnf(d44, plain, para(X0,X1,X2,X3) | ~para(X0,X0,X2,X3), inference(resolution, [status(thm)], [d38,d43])). % 47.03/25.41 cnf(d45, plain, ~midp(X0,X0,X1) | para(X0,X0,X1,X0), inference(resolution, [status(thm)], [d5,c3])). % 47.03/25.41 cnf(d46, plain, para(X0,X0,X1,X0), inference(resolution, [status(thm)], [d38,d45])). % 47.03/25.41 cnf(d47, plain, para(X0,X1,X2,X0), inference(resolution, [status(thm)], [d46,d44])). % 47.03/25.41 cnf(d48, plain, ~cong(X0,X1,X0,X2) | eqangle(X1,X2,X0,X1,X0,X2,X1,X2), inference(resolution, [status(thm)], [c46,c18])). % 47.03/25.41 cnf(d49, plain, ~cong(X0,X1,X0,X2) | ~para(X3,X4,X1,X2) | eqangle(X3,X4,X0,X1,X0,X2,X1,X2), inference(resolution, [status(thm)], [d48,d0])). % 47.03/25.41 cnf(d50, plain, ~para(X0,X1,X2,X3) | ~cong(X4,X2,X4,X3) | ~para(X4,X3,X2,X3) | para(X0,X1,X4,X2), inference(resolution, [status(thm)], [d49,c73])). % 47.03/25.41 cnf(d51, plain, cong(X0,X1,X0,X2), inference(resolution, [status(thm)], [d39,c68])). % 47.03/25.41 cnf(d52, plain, ~para(X0,X1,X2,X1) | para(X3,X4,X0,X2) | ~para(X3,X4,X2,X1), inference(resolution, [status(thm)], [d51,d50])). % 47.03/25.41 cnf(d53, plain, ~cong(X0,X1,X0,X2) | eqangle(X0,X2,X1,X2,X1,X2,X0,X1), inference(resolution, [status(thm)], [d48,c19])). % 47.03/25.41 cnf(d54, plain, ~cong(X0,X1,X0,X2) | ~para(X1,X2,X0,X1) | para(X0,X2,X1,X2), inference(resolution, [status(thm)], [d53,c73])). % 47.03/25.41 cnf(d55, plain, ~para(X0,X1,X2,X0) | para(X2,X1,X0,X1), inference(resolution, [status(thm)], [d51,d54])). % 47.03/25.41 cnf(d56, plain, para(X0,X1,X2,X1), inference(resolution, [status(thm)], [d47,d55])). % 47.03/25.41 cnf(d57, plain, ~para(X0,X1,X2,X3) | para(X0,X1,X4,X2), inference(resolution, [status(thm)], [d56,d52])). % 47.03/25.41 cnf(d58, plain, para(X0,X1,X2,X3), inference(resolution, [status(thm)], [d57,d47])). % 47.03/25.41 cnf(d59, plain, ~circle(sK528,sK526,sK530,sK528) | ~'Ts523'(sK525,sK526,sK528,sK529,sK530), inference(resolution, [status(thm)], [d58,d40])). % 47.03/25.41 cnf(d60, plain, ~midp(X0,X1,X2) | ~cong(X0,X1,X0,X3) | circle(X0,X1,X3,X2), inference(resolution, [status(thm)], [c68,c11])). % 47.03/25.41 cnf(d61, plain, ~midp(X0,X1,X2) | circle(X0,X1,X3,X2) | ~midp(X0,X1,X3), inference(resolution, [status(thm)], [d60,c68])). % 47.03/25.41 cnf(d62, plain, ~midp(X0,X1,X2) | circle(X0,X1,X3,X2), inference(resolution, [status(thm)], [d39,d61])). % 47.03/25.41 cnf(d63, plain, circle(X0,X1,X2,X3), inference(resolution, [status(thm)], [d39,d62])). % 47.03/25.41 cnf(d64, plain, ~'Ts523'(sK525,sK526,sK528,sK529,sK530), inference(resolution, [status(thm)], [d63,d59])). % 47.03/25.41 cnf(d65, plain, ~para(X0,X1,X2,X3) | eqangle(X0,X1,X2,X3,X4,X5,X4,X5), inference(resolution, [status(thm)], [c39,c20])). % 47.03/25.41 cnf(d66, plain, ~para(X0,X1,X2,X3) | ~eqangle(X4,X5,X4,X5,X6,X7,X8,X9) | eqangle(X0,X1,X2,X3,X6,X7,X8,X9), inference(resolution, [status(thm)], [d65,c21])). % 47.03/25.41 cnf(d67, plain, ~cong(X0,X1,X0,X2) | eqangle(X1,X2,X0,X2,X0,X1,X1,X2), inference(resolution, [status(thm)], [c46,c19])). % 47.03/25.41 cnf(d68, plain, ~cong(X0,X1,X0,X2) | ~para(X3,X4,X1,X2) | eqangle(X3,X4,X0,X2,X0,X1,X1,X2), inference(resolution, [status(thm)], [d67,d0])). % 47.03/25.41 cnf(d69, plain, ~para(X0,X1,X2,X1) | ~cong(X0,X2,X0,X1) | ~para(X3,X4,X5,X6) | eqangle(X3,X4,X5,X6,X0,X2,X2,X1), inference(resolution, [status(thm)], [d68,d66])). % 47.03/25.41 cnf(d70, plain, ~para(X0,X1,X2,X3) | ~para(X4,X5,X6,X5) | eqangle(X0,X1,X2,X3,X4,X6,X6,X5), inference(resolution, [status(thm)], [d51,d69])). % 47.03/25.41 cnf(d71, plain, ~para(X0,X1,X2,X3) | eqangle(X0,X1,X2,X3,X4,X5,X5,X6), inference(resolution, [status(thm)], [d56,d70])). % 47.03/25.41 cnf(d72, plain, eqangle(X0,X1,X2,X3,X4,X5,X5,X6), inference(resolution, [status(thm)], [d58,d71])). % 47.03/25.41 cnf(d73, plain, 'Ts523'(X0,X1,X2,X3,X4) | ~'Ts522'(X0,X1,X2,X3,X4), inference(resolution, [status(thm)], [d72,c128])). % 47.03/25.41 cnf(d74, plain, ~para(X0,X1,X2,X3) | ~eqangle(X4,X5,X2,X3,X6,X7,X8,X9) | eqangle(X4,X5,X0,X1,X6,X7,X8,X9), inference(resolution, [status(thm)], [d10,c21])). % 47.03/25.41 cnf(d75, plain, ~midp(X0,X1,X2) | ~circle(X3,X4,X1,X2) | eqangle(X1,X4,X4,X2,X3,X1,X3,X0), inference(resolution, [status(thm)], [c50,c17])). % 47.03/25.41 cnf(d76, plain, ~midp(X0,X1,X2) | ~circle(X3,X4,X1,X2) | eqangle(X1,X4,X3,X1,X4,X2,X3,X0), inference(resolution, [status(thm)], [d75,c20])). % 47.03/25.41 cnf(d77, plain, ~midp(X0,X1,X2) | ~circle(X3,X4,X1,X2) | ~para(X5,X6,X3,X1) | eqangle(X1,X4,X5,X6,X4,X2,X3,X0), inference(resolution, [status(thm)], [d76,d74])). % 47.03/25.41 cnf(d78, plain, ~para(X0,X1,X2,X3) | ~circle(X2,X4,X3,X5) | eqangle(X3,X4,X0,X1,X4,X5,X2,X6), inference(resolution, [status(thm)], [d39,d77])). % 47.03/25.41 cnf(d79, plain, ~circle(X0,X1,X2,X3) | eqangle(X2,X1,X4,X5,X1,X3,X0,X6), inference(resolution, [status(thm)], [d58,d78])). % 47.03/25.41 cnf(d80, plain, eqangle(X0,X1,X2,X3,X1,X4,X5,X6), inference(resolution, [status(thm)], [d63,d79])). % 47.03/25.41 cnf(d81, plain, eqangle(X0,X1,X2,X3,X4,X0,X5,X6), inference(resolution, [status(thm)], [d80,c19])). % 47.03/25.41 cnf(d82, plain, ~para(X0,X1,X2,X3) | eqangle(X4,X5,X0,X1,X5,X4,X2,X3), inference(resolution, [status(thm)], [d10,c17])). % 47.03/25.41 cnf(d83, plain, ~para(X0,X1,X2,X3) | eqangle(X0,X1,X4,X5,X2,X3,X5,X4), inference(resolution, [status(thm)], [d82,c18])). % 47.03/25.41 cnf(d84, plain, ~para(X0,X1,X2,X3) | ~eqangle(X2,X3,X4,X5,X6,X7,X8,X9) | eqangle(X0,X1,X5,X4,X6,X7,X8,X9), inference(resolution, [status(thm)], [d83,c21])). % 47.03/25.41 cnf(d85, plain, ~eqangle(X0,X1,X2,X3,X4,X5,X6,X7) | eqangle(X8,X9,X3,X2,X4,X5,X6,X7), inference(resolution, [status(thm)], [d58,d84])). % 47.03/25.41 cnf(d86, plain, eqangle(X0,X1,X2,X3,X4,X5,X6,X7), inference(resolution, [status(thm)], [d85,d81])). % 47.03/25.41 cnf(d87, plain, ~para(X0,X1,X2,X3) | ~para(X4,X5,X6,X7) | eqangle(X4,X5,X0,X1,X7,X6,X2,X3), inference(resolution, [status(thm)], [d82,d0])). % 47.03/25.41 cnf(d88, plain, ~para(X0,X1,X2,X0) | ~para(X1,X3,X2,X4) | ~eqangle(X0,X1,X1,X3,X2,X0,X0,X4) | ~eqangle(X0,X1,X1,X3,X0,X4,X4,X2) | 'Ts522'(X4,X2,X0,X1,X3), inference(resolution, [status(thm)], [d87,c121])). % 47.03/25.41 cnf(d89, plain, ~para(X0,X1,X2,X3) | ~para(X4,X0,X2,X4) | ~eqangle(X4,X0,X0,X1,X4,X3,X3,X2) | 'Ts522'(X3,X2,X4,X0,X1), inference(resolution, [status(thm)], [d86,d88])). % 47.03/25.41 cnf(d90, plain, ~para(X0,X1,X2,X3) | ~eqangle(X4,X0,X0,X1,X4,X3,X3,X2) | 'Ts522'(X3,X2,X4,X0,X1), inference(resolution, [status(thm)], [d58,d89])). % 47.03/25.41 cnf(d91, plain, ~para(X0,X1,X2,X3) | 'Ts522'(X3,X2,X4,X0,X1), inference(resolution, [status(thm)], [d90,d86])). % 47.03/25.41 cnf(d92, plain, 'Ts522'(X0,X1,X2,X3,X4), inference(resolution, [status(thm)], [d58,d91])). % 47.03/25.41 cnf(d93, plain, 'Ts523'(X0,X1,X2,X3,X4), inference(resolution, [status(thm)], [d92,d73])). % 47.03/25.41 cnf(d94, plain, $false, inference(resolution, [status(thm)], [d93,d64])). % 47.03/25.41 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------