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