%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO614+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:22:24 EDT 2024
% Result : Theorem 274.04s 274.24s
% Output : Refutation 274.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO614+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n012.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:25:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 274.04/274.24 % Version: 1.5
% 274.04/274.24 % SZS status Theorem
% 274.04/274.24 % SZS output start CNFRefutation
% 274.04/274.24 fof(exemplo6GDDFULL618076,conjecture,(![A]:(![B]:(![C]:(![O]:(![G]:(![E]:(![K]:(![H]:(![N]:(![NWPNT1]:(((((((((circle(O,A,B,C)&midp(G,C,B))&coll(E,O,G))&circle(O,A,E,NWPNT1))&perp(K,E,A,B))&coll(K,A,B))&perp(H,A,O,G))&coll(H,O,G))&circle(N,K,G,H))=>perp(E,K,K,N)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL618076)).
% 274.04/274.24 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![G]:(![E]:(![K]:(![H]:(![N]:(![NWPNT1]:(((((((((circle(O,A,B,C)&midp(G,C,B))&coll(E,O,G))&circle(O,A,E,NWPNT1))&perp(K,E,A,B))&coll(K,A,B))&perp(H,A,O,G))&coll(H,O,G))&circle(N,K,G,H))=>perp(E,K,K,N))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618076])).
% 274.04/274.24 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[G]:(?[E]:(?[K]:(?[H]:(?[N]:(?[NWPNT1]:(((((((((circle(O,A,B,C)&midp(G,C,B))&coll(E,O,G))&circle(O,A,E,NWPNT1))&perp(K,E,A,B))&coll(K,A,B))&perp(H,A,O,G))&coll(H,O,G))&circle(N,K,G,H))&~perp(E,K,K,N)))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 274.04/274.24 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[G]:(?[E]:(?[K]:(?[H]:(?[N]:(((((((((circle(O,A,B,C)&midp(G,C,B))&coll(E,O,G))&(?[NWPNT1]:circle(O,A,E,NWPNT1)))&perp(K,E,A,B))&coll(K,A,B))&perp(H,A,O,G))&coll(H,O,G))&circle(N,K,G,H))&~perp(E,K,K,N))))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 274.04/274.24 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((((circle(X5,X2,X3,X4)&midp(X6,X4,X3))&coll(X7,X5,X6))&(?[X11]:circle(X5,X2,X7,X11)))&perp(X8,X7,X2,X3))&coll(X8,X2,X3))&perp(X9,X2,X5,X6))&coll(X9,X5,X6))&circle(X10,X8,X6,X9))&~perp(X7,X8,X8,X10))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 274.04/274.24 fof(c15,negated_conjecture,(((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&midp(skolem0005,skolem0003,skolem0002))&coll(skolem0006,skolem0004,skolem0005))&circle(skolem0004,skolem0001,skolem0006,skolem0010))&perp(skolem0007,skolem0006,skolem0001,skolem0002))&coll(skolem0007,skolem0001,skolem0002))&perp(skolem0008,skolem0001,skolem0004,skolem0005))&coll(skolem0008,skolem0004,skolem0005))&circle(skolem0009,skolem0007,skolem0005,skolem0008))&~perp(skolem0006,skolem0007,skolem0007,skolem0009)),inference(skolemize,[status(esa)],[c14])).
% 274.04/274.24 cnf(c25,negated_conjecture,~perp(skolem0006,skolem0007,skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 274.04/274.24 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 274.04/274.24 fof(c388,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X503,X504,X501,X502)))))),inference(variable_rename,[status(thm)],[c387])).
% 274.04/274.24 cnf(c389,plain,~perp(X723,X724,X722,X725)|perp(X722,X725,X723,X724),inference(split_conjunct,[status(thm)],[c388])).
% 274.04/274.24 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 274.04/274.24 fof(c390,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 274.04/274.24 fof(c391,plain,(![X505]:(![X506]:(![X507]:(![X508]:(~perp(X505,X506,X507,X508)|perp(X505,X506,X508,X507)))))),inference(variable_rename,[status(thm)],[c390])).
% 274.04/274.24 cnf(c392,plain,~perp(X732,X733,X730,X731)|perp(X732,X733,X731,X730),inference(split_conjunct,[status(thm)],[c391])).
% 274.04/274.24 cnf(c20,negated_conjecture,perp(skolem0007,skolem0006,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 cnf(c532,plain,perp(skolem0007,skolem0006,skolem0002,skolem0001),inference(resolution,[status(thm)],[c392, c20])).
% 274.04/274.24 cnf(c541,plain,perp(skolem0002,skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c532, c389])).
% 274.04/274.24 cnf(c557,plain,perp(skolem0002,skolem0001,skolem0006,skolem0007),inference(resolution,[status(thm)],[c541, c392])).
% 274.04/274.24 fof(ruleD10,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&perp(C,D,E,F))=>perp(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 274.04/274.24 fof(c381,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~perp(C,D,E,F))|perp(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD10])).
% 274.04/274.24 fof(c382,plain,(![X489]:(![X490]:(![X491]:(![X492]:(![X493]:(![X494]:((~para(X489,X490,X491,X492)|~perp(X491,X492,X493,X494))|perp(X489,X490,X493,X494)))))))),inference(variable_rename,[status(thm)],[c381])).
% 274.04/274.24 cnf(c383,plain,~para(X1267,X1266,X1265,X1262)|~perp(X1265,X1262,X1263,X1264)|perp(X1267,X1266,X1263,X1264),inference(split_conjunct,[status(thm)],[c382])).
% 274.04/274.24 cnf(c1542,plain,~para(X2701,X2702,skolem0002,skolem0001)|perp(X2701,X2702,skolem0006,skolem0007),inference(resolution,[status(thm)],[c383, c557])).
% 274.04/274.24 fof(ruleD9,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((perp(A,B,C,D)&perp(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 274.04/274.24 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 274.04/274.24 fof(c385,plain,(![X495]:(![X496]:(![X497]:(![X498]:(![X499]:(![X500]:((~perp(X495,X496,X497,X498)|~perp(X497,X498,X499,X500))|para(X495,X496,X499,X500)))))))),inference(variable_rename,[status(thm)],[c384])).
% 274.04/274.24 cnf(c386,plain,~perp(X1273,X1271,X1269,X1274)|~perp(X1269,X1274,X1270,X1272)|para(X1273,X1271,X1270,X1272),inference(split_conjunct,[status(thm)],[c385])).
% 274.04/274.24 cnf(c16,negated_conjecture,circle(skolem0004,skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 fof(ruleD53,axiom,(![A]:(![B]:(![C]:(![O]:((circle(O,A,B,C)&coll(O,A,C))=>perp(A,B,B,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD53)).
% 274.04/274.24 fof(c235,plain,(![A]:(![B]:(![C]:(![O]:((~circle(O,A,B,C)|~coll(O,A,C))|perp(A,B,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD53])).
% 274.04/274.24 fof(c236,plain,(![A]:(![B]:(![C]:((![O]:(~circle(O,A,B,C)|~coll(O,A,C)))|perp(A,B,B,C))))),inference(shift_quantors,[status(thm)],[c235])).
% 274.04/274.24 fof(c238,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~circle(X233,X230,X231,X232)|~coll(X233,X230,X232))|perp(X230,X231,X231,X232)))))),inference(shift_quantors,[status(thm)],[fof(c237,plain,(![X230]:(![X231]:(![X232]:((![X233]:(~circle(X233,X230,X231,X232)|~coll(X233,X230,X232)))|perp(X230,X231,X231,X232))))),inference(variable_rename,[status(thm)],[c236])).])).
% 274.04/274.24 cnf(c239,plain,~circle(X996,X997,X995,X994)|~coll(X996,X997,X994)|perp(X997,X995,X995,X994),inference(split_conjunct,[status(thm)],[c238])).
% 274.04/274.24 cnf(c1215,plain,~coll(skolem0004,skolem0001,skolem0003)|perp(skolem0001,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c239, c16])).
% 274.04/274.24 fof(ruleD1,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(A,C,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD1)).
% 274.04/274.24 fof(c408,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(A,C,B))))),inference(fof_nnf,[status(thm)],[ruleD1])).
% 274.04/274.24 fof(c409,plain,(![X530]:(![X531]:(![X532]:(~coll(X530,X531,X532)|coll(X530,X532,X531))))),inference(variable_rename,[status(thm)],[c408])).
% 274.04/274.24 cnf(c410,plain,~coll(X590,X588,X589)|coll(X590,X589,X588),inference(split_conjunct,[status(thm)],[c409])).
% 274.04/274.24 fof(ruleD2,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD2)).
% 274.04/274.24 fof(c405,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD2])).
% 274.04/274.24 fof(c406,plain,(![X527]:(![X528]:(![X529]:(~coll(X527,X528,X529)|coll(X528,X527,X529))))),inference(variable_rename,[status(thm)],[c405])).
% 274.04/274.24 cnf(c407,plain,~coll(X572,X573,X571)|coll(X573,X572,X571),inference(split_conjunct,[status(thm)],[c406])).
% 274.04/274.24 cnf(c23,negated_conjecture,coll(skolem0008,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 cnf(c446,plain,coll(skolem0008,skolem0005,skolem0004),inference(resolution,[status(thm)],[c410, c23])).
% 274.04/274.24 cnf(c459,plain,coll(skolem0005,skolem0008,skolem0004),inference(resolution,[status(thm)],[c446, c407])).
% 274.04/274.24 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 274.04/274.24 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 274.04/274.24 fof(c403,plain,(![X523]:(![X524]:(![X525]:(![X526]:((~coll(X523,X524,X525)|~coll(X523,X524,X526))|coll(X525,X526,X523)))))),inference(variable_rename,[status(thm)],[c402])).
% 274.04/274.24 cnf(c404,plain,~coll(X784,X781,X783)|~coll(X784,X781,X782)|coll(X783,X782,X784),inference(split_conjunct,[status(thm)],[c403])).
% 274.04/274.24 cnf(c600,plain,~coll(skolem0005,skolem0008,X1268)|coll(X1268,skolem0004,skolem0005),inference(resolution,[status(thm)],[c404, c459])).
% 274.04/274.24 cnf(c585,plain,~coll(X787,X785,X786)|coll(X786,X786,X787),inference(factor,[status(thm)],[c404])).
% 274.04/274.24 cnf(c21,negated_conjecture,coll(skolem0007,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 cnf(c428,plain,coll(skolem0001,skolem0007,skolem0002),inference(resolution,[status(thm)],[c407, c21])).
% 274.04/274.24 cnf(c627,plain,coll(skolem0002,skolem0002,skolem0001),inference(resolution,[status(thm)],[c585, c428])).
% 274.04/274.24 cnf(c17,negated_conjecture,midp(skolem0005,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 fof(ruleD69,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD69)).
% 274.04/274.24 fof(c182,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD69])).
% 274.04/274.24 fof(c183,plain,(![X157]:(![X158]:(![X159]:(~midp(X157,X158,X159)|coll(X157,X158,X159))))),inference(variable_rename,[status(thm)],[c182])).
% 274.04/274.24 cnf(c184,plain,~midp(X557,X558,X559)|coll(X557,X558,X559),inference(split_conjunct,[status(thm)],[c183])).
% 274.04/274.24 cnf(c417,plain,coll(skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c184, c17])).
% 274.04/274.24 cnf(c611,plain,coll(skolem0002,skolem0002,skolem0005),inference(resolution,[status(thm)],[c585, c417])).
% 274.04/274.24 cnf(c660,plain,~coll(skolem0002,skolem0002,X1321)|coll(X1321,skolem0005,skolem0002),inference(resolution,[status(thm)],[c611, c404])).
% 274.04/274.24 cnf(c1629,plain,coll(skolem0001,skolem0005,skolem0002),inference(resolution,[status(thm)],[c660, c627])).
% 274.04/274.24 cnf(c1642,plain,coll(skolem0001,skolem0002,skolem0005),inference(resolution,[status(thm)],[c1629, c410])).
% 274.04/274.24 cnf(c1666,plain,coll(skolem0005,skolem0005,skolem0001),inference(resolution,[status(thm)],[c1642, c585])).
% 274.04/274.24 cnf(c614,plain,coll(skolem0005,skolem0005,skolem0008),inference(resolution,[status(thm)],[c585, c23])).
% 274.04/274.24 cnf(c675,plain,~coll(skolem0005,skolem0005,X1506)|coll(X1506,skolem0008,skolem0005),inference(resolution,[status(thm)],[c614, c404])).
% 274.04/274.24 cnf(c2152,plain,coll(skolem0001,skolem0008,skolem0005),inference(resolution,[status(thm)],[c675, c1666])).
% 274.04/274.24 cnf(c2172,plain,coll(skolem0008,skolem0001,skolem0005),inference(resolution,[status(thm)],[c2152, c407])).
% 274.04/274.24 cnf(c2212,plain,coll(skolem0008,skolem0005,skolem0001),inference(resolution,[status(thm)],[c2172, c410])).
% 274.04/274.24 cnf(c2305,plain,coll(skolem0005,skolem0008,skolem0001),inference(resolution,[status(thm)],[c2212, c407])).
% 274.04/274.24 cnf(c2455,plain,coll(skolem0001,skolem0004,skolem0005),inference(resolution,[status(thm)],[c2305, c600])).
% 274.04/274.24 cnf(c2596,plain,coll(skolem0001,skolem0005,skolem0004),inference(resolution,[status(thm)],[c2455, c410])).
% 274.04/274.24 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 274.04/274.24 fof(c378,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 274.04/274.24 fof(c379,plain,(![X486]:(![X487]:(![X488]:(~midp(X488,X487,X486)|midp(X488,X486,X487))))),inference(variable_rename,[status(thm)],[c378])).
% 274.04/274.24 cnf(c380,plain,~midp(X560,X561,X562)|midp(X560,X562,X561),inference(split_conjunct,[status(thm)],[c379])).
% 274.04/274.24 cnf(c419,plain,midp(skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c380, c17])).
% 274.04/274.24 cnf(c421,plain,coll(skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c419, c184])).
% 274.04/274.24 cnf(c605,plain,~coll(skolem0005,skolem0002,X1298)|coll(X1298,skolem0003,skolem0005),inference(resolution,[status(thm)],[c404, c421])).
% 274.04/274.24 cnf(c1641,plain,coll(skolem0005,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1629, c407])).
% 274.04/274.24 cnf(c1662,plain,coll(skolem0005,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1641, c410])).
% 274.04/274.24 cnf(c1699,plain,coll(skolem0001,skolem0003,skolem0005),inference(resolution,[status(thm)],[c1662, c605])).
% 274.04/274.24 cnf(c1764,plain,coll(skolem0001,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1699, c410])).
% 274.04/274.24 cnf(c1840,plain,~coll(skolem0001,skolem0005,X2470)|coll(X2470,skolem0003,skolem0001),inference(resolution,[status(thm)],[c1764, c404])).
% 274.04/274.24 cnf(c6883,plain,coll(skolem0004,skolem0003,skolem0001),inference(resolution,[status(thm)],[c1840, c2596])).
% 274.04/274.24 cnf(c6900,plain,coll(skolem0004,skolem0001,skolem0003),inference(resolution,[status(thm)],[c6883, c410])).
% 274.04/274.24 cnf(c6944,plain,perp(skolem0001,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c6900, c1215])).
% 274.04/274.24 cnf(c7065,plain,perp(skolem0002,skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c6944, c389])).
% 274.04/274.24 cnf(c7089,plain,perp(skolem0002,skolem0003,skolem0002,skolem0001),inference(resolution,[status(thm)],[c7065, c392])).
% 274.04/274.24 cnf(c7106,plain,~perp(X13652,X13653,skolem0002,skolem0003)|para(X13652,X13653,skolem0002,skolem0001),inference(resolution,[status(thm)],[c7089, c386])).
% 274.04/274.24 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 274.04/274.24 fof(c340,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 274.04/274.24 fof(c341,plain,(![X412]:(![X413]:(![X414]:(![X415]:(~cong(X412,X413,X414,X415)|cong(X412,X413,X415,X414)))))),inference(variable_rename,[status(thm)],[c340])).
% 274.04/274.24 cnf(c342,plain,~cong(X688,X690,X689,X691)|cong(X688,X690,X691,X689),inference(split_conjunct,[status(thm)],[c341])).
% 274.04/274.24 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 274.04/274.24 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 274.04/274.24 fof(c338,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X410,X411,X408,X409)))))),inference(variable_rename,[status(thm)],[c337])).
% 274.04/274.24 cnf(c339,plain,~cong(X685,X687,X684,X686)|cong(X684,X686,X685,X687),inference(split_conjunct,[status(thm)],[c338])).
% 274.04/274.24 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 274.04/274.24 fof(c185,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 274.04/274.24 fof(c186,plain,(![X160]:(![X161]:(![X162]:(~midp(X160,X161,X162)|cong(X160,X161,X160,X162))))),inference(variable_rename,[status(thm)],[c185])).
% 274.04/274.24 cnf(c187,plain,~midp(X676,X675,X677)|cong(X676,X675,X676,X677),inference(split_conjunct,[status(thm)],[c186])).
% 274.04/274.24 cnf(c498,plain,cong(skolem0005,skolem0003,skolem0005,skolem0002),inference(resolution,[status(thm)],[c187, c17])).
% 274.04/274.24 cnf(c503,plain,cong(skolem0005,skolem0003,skolem0002,skolem0005),inference(resolution,[status(thm)],[c342, c498])).
% 274.04/274.24 cnf(c505,plain,cong(skolem0002,skolem0005,skolem0005,skolem0003),inference(resolution,[status(thm)],[c503, c339])).
% 274.04/274.24 cnf(c513,plain,cong(skolem0002,skolem0005,skolem0003,skolem0005),inference(resolution,[status(thm)],[c505, c342])).
% 274.04/274.24 fof(ruleD56,axiom,(![A]:(![B]:(![P]:(![Q]:((cong(A,P,B,P)&cong(A,Q,B,Q))=>perp(A,B,P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 274.04/274.24 fof(c226,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 274.04/274.24 fof(c227,plain,(![X218]:(![X219]:(![X220]:(![X221]:((~cong(X218,X220,X219,X220)|~cong(X218,X221,X219,X221))|perp(X218,X219,X220,X221)))))),inference(variable_rename,[status(thm)],[c226])).
% 274.04/274.24 cnf(c228,plain,~cong(X983,X984,X985,X984)|~cong(X983,X982,X985,X982)|perp(X983,X985,X984,X982),inference(split_conjunct,[status(thm)],[c227])).
% 274.04/274.24 cnf(c1196,plain,~cong(X1056,X1054,X1055,X1054)|perp(X1056,X1055,X1054,X1054),inference(factor,[status(thm)],[c228])).
% 274.04/274.24 cnf(c1303,plain,perp(skolem0002,skolem0003,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1196, c513])).
% 274.04/274.24 cnf(c1317,plain,perp(skolem0005,skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1303, c389])).
% 274.04/274.24 cnf(c1535,plain,~para(X2683,X2684,skolem0005,skolem0005)|perp(X2683,X2684,skolem0002,skolem0003),inference(resolution,[status(thm)],[c383, c1317])).
% 274.04/274.24 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 274.04/274.24 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 274.04/274.24 fof(c397,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X517,X518,X515,X516)))))),inference(variable_rename,[status(thm)],[c396])).
% 274.04/274.24 cnf(c398,plain,~para(X767,X769,X768,X770)|para(X768,X770,X767,X769),inference(split_conjunct,[status(thm)],[c397])).
% 274.04/274.24 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 274.04/274.24 fof(c265,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~midp(E,A,B)|~midp(F,A,C))|para(E,F,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD44])).
% 274.04/274.24 fof(c266,plain,(![X269]:(![X270]:(![X271]:(![X272]:(![X273]:((~midp(X272,X269,X270)|~midp(X273,X269,X271))|para(X272,X273,X270,X271))))))),inference(variable_rename,[status(thm)],[c265])).
% 274.04/274.24 cnf(c267,plain,~midp(X1039,X1038,X1040)|~midp(X1036,X1038,X1037)|para(X1039,X1036,X1040,X1037),inference(split_conjunct,[status(thm)],[c266])).
% 274.04/274.24 cnf(c1249,plain,~midp(X1042,X1043,X1041)|para(X1042,X1042,X1041,X1041),inference(factor,[status(thm)],[c267])).
% 274.04/274.24 cnf(c1253,plain,para(skolem0005,skolem0005,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1249, c17])).
% 274.04/274.24 cnf(c1276,plain,para(skolem0002,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1253, c398])).
% 274.04/274.24 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 274.04/274.24 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD6])).
% 274.04/274.24 fof(c394,plain,(![X509]:(![X510]:(![X511]:(![X512]:(![X513]:(![X514]:((~para(X509,X510,X511,X512)|~para(X511,X512,X513,X514))|para(X509,X510,X513,X514)))))))),inference(variable_rename,[status(thm)],[c393])).
% 274.04/274.24 cnf(c395,plain,~para(X1282,X1281,X1283,X1278)|~para(X1283,X1278,X1280,X1279)|para(X1282,X1281,X1280,X1279),inference(split_conjunct,[status(thm)],[c394])).
% 274.04/274.24 cnf(c1582,plain,~para(X2764,X2765,skolem0002,skolem0002)|para(X2764,X2765,skolem0005,skolem0005),inference(resolution,[status(thm)],[c395, c1276])).
% 274.04/274.24 fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)¶(A,C,B,D))¶(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 274.04/274.24 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 274.04/274.24 fof(c198,plain,(![X174]:(![X175]:(![X176]:(![X177]:(![X178]:(((~midp(X178,X174,X175)|~para(X174,X176,X175,X177))|~para(X174,X177,X175,X176))|midp(X178,X176,X177))))))),inference(variable_rename,[status(thm)],[c197])).
% 274.04/274.24 cnf(c199,plain,~midp(X945,X947,X944)|~para(X947,X946,X944,X948)|~para(X947,X948,X944,X946)|midp(X945,X946,X948),inference(split_conjunct,[status(thm)],[c198])).
% 274.04/274.24 cnf(c1185,plain,~midp(X2293,X2294,X2292)|~para(X2294,X2291,X2292,X2291)|midp(X2293,X2291,X2291),inference(factor,[status(thm)],[c199])).
% 274.04/274.24 cnf(c22,negated_conjecture,perp(skolem0008,skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 274.04/274.24 cnf(c525,plain,perp(skolem0004,skolem0005,skolem0008,skolem0001),inference(resolution,[status(thm)],[c389, c22])).
% 274.04/274.24 cnf(c1555,plain,~perp(X2718,X2719,skolem0008,skolem0001)|para(X2718,X2719,skolem0004,skolem0005),inference(resolution,[status(thm)],[c386, c22])).
% 274.04/274.24 cnf(c8083,plain,para(skolem0004,skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c1555, c525])).
% 274.04/274.24 cnf(c8218,plain,~midp(X6192,skolem0004,skolem0004)|midp(X6192,skolem0005,skolem0005),inference(resolution,[status(thm)],[c8083, c1185])).
% 274.04/274.24 cnf(c524,plain,perp(skolem0001,skolem0002,skolem0007,skolem0006),inference(resolution,[status(thm)],[c389, c20])).
% 274.04/274.24 cnf(c530,plain,perp(skolem0001,skolem0002,skolem0006,skolem0007),inference(resolution,[status(thm)],[c392, c524])).
% 274.04/274.24 cnf(c535,plain,perp(skolem0006,skolem0007,skolem0001,skolem0002),inference(resolution,[status(thm)],[c530, c389])).
% 274.04/274.24 cnf(c548,plain,perp(skolem0006,skolem0007,skolem0002,skolem0001),inference(resolution,[status(thm)],[c535, c392])).
% 274.04/274.24 cnf(c1557,plain,~perp(X2722,X2723,skolem0006,skolem0007)|para(X2722,X2723,skolem0002,skolem0001),inference(resolution,[status(thm)],[c386, c548])).
% 274.04/274.24 cnf(c8158,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1557, c557])).
% 274.04/274.24 cnf(c8369,plain,~midp(X6217,skolem0002,skolem0002)|midp(X6217,skolem0001,skolem0001),inference(resolution,[status(thm)],[c8158, c1185])).
% 274.04/274.24 cnf(c497,plain,cong(skolem0005,skolem0002,skolem0005,skolem0003),inference(resolution,[status(thm)],[c187, c419])).
% 274.04/274.24 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 274.04/274.24 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 274.04/274.24 fof(c335,plain,(![X402]:(![X403]:(![X404]:(![X405]:(![X406]:(![X407]:((~cong(X402,X403,X404,X405)|~cong(X404,X405,X406,X407))|cong(X402,X403,X406,X407)))))))),inference(variable_rename,[status(thm)],[c334])).
% 274.04/274.24 cnf(c336,plain,~cong(X1181,X1180,X1183,X1185)|~cong(X1183,X1185,X1184,X1182)|cong(X1181,X1180,X1184,X1182),inference(split_conjunct,[status(thm)],[c335])).
% 274.04/274.24 cnf(c1472,plain,~cong(X2622,X2621,skolem0005,skolem0003)|cong(X2622,X2621,skolem0005,skolem0002),inference(resolution,[status(thm)],[c336, c498])).
% 274.04/274.24 cnf(c7403,plain,cong(skolem0005,skolem0002,skolem0005,skolem0002),inference(resolution,[status(thm)],[c1472, c497])).
% 274.04/274.24 cnf(c7424,plain,perp(skolem0005,skolem0005,skolem0002,skolem0002),inference(resolution,[status(thm)],[c7403, c1196])).
% 274.04/274.24 cnf(c7443,plain,perp(skolem0002,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c7424, c389])).
% 274.04/274.24 cnf(c504,plain,cong(skolem0005,skolem0002,skolem0003,skolem0005),inference(resolution,[status(thm)],[c342, c497])).
% 274.04/274.24 cnf(c508,plain,cong(skolem0003,skolem0005,skolem0005,skolem0002),inference(resolution,[status(thm)],[c504, c339])).
% 274.04/274.24 cnf(c516,plain,cong(skolem0003,skolem0005,skolem0002,skolem0005),inference(resolution,[status(thm)],[c508, c342])).
% 274.04/274.24 cnf(c1302,plain,perp(skolem0003,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1196, c516])).
% 274.04/274.24 cnf(c1309,plain,perp(skolem0005,skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1302, c389])).
% 274.04/274.24 cnf(c1559,plain,~perp(X2726,X2727,skolem0005,skolem0005)|para(X2726,X2727,skolem0003,skolem0002),inference(resolution,[status(thm)],[c386, c1309])).
% 274.04/274.24 cnf(c8223,plain,para(skolem0002,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1559, c7443])).
% 274.04/274.24 cnf(c8505,plain,~midp(X6240,skolem0002,skolem0003)|midp(X6240,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8223, c1185])).
% 274.04/274.24 cnf(c18668,plain,midp(skolem0005,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8505, c419])).
% 274.04/274.24 cnf(c18715,plain,midp(skolem0005,skolem0001,skolem0001),inference(resolution,[status(thm)],[c18668, c8369])).
% 274.04/274.24 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 274.04/274.24 fof(c74,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 274.04/274.24 fof(c75,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c74])).
% 274.04/274.24 fof(c76,plain,(![X54]:(![X55]:(![X56]:(![X57]:(~circle(X57,X54,X55,X56)|(?[X58]:perp(X58,X54,X54,X57))))))),inference(variable_rename,[status(thm)],[c75])).
% 274.04/274.24 fof(c77,plain,(![X54]:(![X55]:(![X56]:(![X57]:(~circle(X57,X54,X55,X56)|perp(skolem0019(X54,X55,X56,X57),X54,X54,X57)))))),inference(skolemize,[status(esa)],[c76])).
% 274.04/274.25 cnf(c78,plain,~circle(X764,X766,X763,X765)|perp(skolem0019(X766,X763,X765,X764),X766,X766,X764),inference(split_conjunct,[status(thm)],[c77])).
% 274.04/274.25 cnf(c582,plain,perp(skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001,skolem0001,skolem0004),inference(resolution,[status(thm)],[c78, c16])).
% 274.04/274.25 cnf(c2283,plain,~perp(X3696,X3697,skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001)|para(X3696,X3697,skolem0001,skolem0004),inference(resolution,[status(thm)],[c582, c386])).
% 274.04/274.25 cnf(c2291,plain,perp(skolem0001,skolem0004,skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001),inference(resolution,[status(thm)],[c582, c389])).
% 274.04/274.25 cnf(c11168,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c2291, c2283])).
% 274.04/274.25 cnf(c11186,plain,~midp(X6496,skolem0001,skolem0001)|midp(X6496,skolem0004,skolem0004),inference(resolution,[status(thm)],[c11168, c1185])).
% 274.04/274.25 cnf(c20398,plain,midp(skolem0005,skolem0004,skolem0004),inference(resolution,[status(thm)],[c11186, c18715])).
% 274.04/274.25 cnf(c20443,plain,midp(skolem0005,skolem0005,skolem0005),inference(resolution,[status(thm)],[c20398, c8218])).
% 274.04/274.25 fof(ruleD39,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(eqangle(A,B,P,Q,C,D,P,Q)=>para(A,B,C,D)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 274.04/274.25 fof(c288,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 274.04/274.25 fof(c289,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c288])).
% 274.04/274.25 fof(c291,plain,(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(~eqangle(X298,X299,X302,X303,X300,X301,X302,X303)|para(X298,X299,X300,X301)))))))),inference(shift_quantors,[status(thm)],[fof(c290,plain,(![X298]:(![X299]:(![X300]:(![X301]:((![X302]:(![X303]:~eqangle(X298,X299,X302,X303,X300,X301,X302,X303)))|para(X298,X299,X300,X301)))))),inference(variable_rename,[status(thm)],[c289])).])).
% 274.04/274.25 cnf(c292,plain,~eqangle(X1077,X1073,X1076,X1074,X1078,X1075,X1076,X1074)|para(X1077,X1073,X1078,X1075),inference(split_conjunct,[status(thm)],[c291])).
% 274.04/274.25 fof(ruleD19,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(C,D,A,B,U,V,P,Q)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 274.04/274.25 fof(c352,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 274.04/274.25 fof(c353,plain,(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(~eqangle(X444,X445,X446,X447,X448,X449,X450,X451)|eqangle(X446,X447,X444,X445,X450,X451,X448,X449)))))))))),inference(variable_rename,[status(thm)],[c352])).
% 274.04/274.25 cnf(c354,plain,~eqangle(X1228,X1223,X1224,X1221,X1227,X1225,X1226,X1222)|eqangle(X1224,X1221,X1228,X1223,X1226,X1222,X1227,X1225),inference(split_conjunct,[status(thm)],[c353])).
% 274.04/274.25 fof(ruleD40,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(para(A,B,C,D)=>eqangle(A,B,P,Q,C,D,P,Q)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 274.04/274.25 fof(c283,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 274.04/274.25 fof(c284,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c283])).
% 274.04/274.25 fof(c286,plain,(![X292]:(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(~para(X292,X293,X294,X295)|eqangle(X292,X293,X296,X297,X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c285,plain,(![X292]:(![X293]:(![X294]:(![X295]:(~para(X292,X293,X294,X295)|(![X296]:(![X297]:eqangle(X292,X293,X296,X297,X294,X295,X296,X297)))))))),inference(variable_rename,[status(thm)],[c284])).])).
% 274.04/274.25 cnf(c287,plain,~para(X1065,X1068,X1069,X1066)|eqangle(X1065,X1068,X1070,X1067,X1069,X1066,X1070,X1067),inference(split_conjunct,[status(thm)],[c286])).
% 274.04/274.25 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 274.04/274.25 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 274.04/274.25 fof(c400,plain,(![X519]:(![X520]:(![X521]:(![X522]:(~para(X519,X520,X521,X522)|para(X519,X520,X522,X521)))))),inference(variable_rename,[status(thm)],[c399])).
% 274.04/274.25 cnf(c401,plain,~para(X774,X773,X771,X772)|para(X774,X773,X772,X771),inference(split_conjunct,[status(thm)],[c400])).
% 274.04/274.25 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 274.04/274.25 fof(c200,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 274.04/274.25 fof(c201,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c200])).
% 274.04/274.25 fof(c203,plain,(![X179]:(![X180]:(![X181]:(![X182]:(![X183]:((~midp(X183,X179,X180)|~midp(X183,X181,X182))|para(X179,X181,X180,X182))))))),inference(shift_quantors,[status(thm)],[fof(c202,plain,(![X179]:(![X180]:(![X181]:(![X182]:((![X183]:(~midp(X183,X179,X180)|~midp(X183,X181,X182)))|para(X179,X181,X180,X182)))))),inference(variable_rename,[status(thm)],[c201])).])).
% 274.04/274.25 cnf(c204,plain,~midp(X951,X952,X949)|~midp(X951,X953,X950)|para(X952,X953,X949,X950),inference(split_conjunct,[status(thm)],[c203])).
% 274.04/274.25 cnf(c1193,plain,~midp(skolem0005,X2249,X2248)|para(X2249,skolem0002,X2248,skolem0003),inference(resolution,[status(thm)],[c204, c419])).
% 274.04/274.25 cnf(c5822,plain,para(skolem0003,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1193, c17])).
% 274.04/274.25 cnf(c5838,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c5822, c401])).
% 274.04/274.25 cnf(c5864,plain,eqangle(skolem0003,skolem0002,X5653,X5652,skolem0003,skolem0002,X5653,X5652),inference(resolution,[status(thm)],[c5838, c287])).
% 274.04/274.25 cnf(c17506,plain,eqangle(X8177,X8178,skolem0003,skolem0002,X8177,X8178,skolem0003,skolem0002),inference(resolution,[status(thm)],[c5864, c354])).
% 274.04/274.25 cnf(c23748,plain,para(X8180,X8179,X8180,X8179),inference(resolution,[status(thm)],[c17506, c292])).
% 274.04/274.25 cnf(c23808,plain,~midp(X11169,X11171,X11171)|midp(X11169,X11170,X11170),inference(resolution,[status(thm)],[c23748, c1185])).
% 274.04/274.25 cnf(c40224,plain,midp(skolem0005,X11172,X11172),inference(resolution,[status(thm)],[c23808, c20443])).
% 274.04/274.25 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 274.04/274.25 fof(c240,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 274.04/274.25 fof(c241,plain,(![X234]:(![X235]:(![X236]:(![X237]:((~perp(X234,X235,X235,X236)|~midp(X237,X234,X236))|cong(X234,X237,X235,X237)))))),inference(variable_rename,[status(thm)],[c240])).
% 274.04/274.25 cnf(c242,plain,~perp(X1001,X1000,X1000,X998)|~midp(X999,X1001,X998)|cong(X1001,X999,X1000,X999),inference(split_conjunct,[status(thm)],[c241])).
% 274.04/274.25 fof(ruleD74,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)&perp(P,Q,U,V))=>perp(A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 274.04/274.25 fof(c161,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 274.04/274.25 fof(c162,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c161])).
% 274.04/274.25 fof(c164,plain,(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:(![X134]:((~eqangle(X127,X128,X129,X130,X131,X132,X133,X134)|~perp(X131,X132,X133,X134))|perp(X127,X128,X129,X130)))))))))),inference(shift_quantors,[status(thm)],[fof(c163,plain,(![X127]:(![X128]:(![X129]:(![X130]:((![X131]:(![X132]:(![X133]:(![X134]:(~eqangle(X127,X128,X129,X130,X131,X132,X133,X134)|~perp(X131,X132,X133,X134))))))|perp(X127,X128,X129,X130)))))),inference(variable_rename,[status(thm)],[c162])).])).
% 274.04/274.25 cnf(c165,plain,~eqangle(X909,X908,X907,X906,X912,X910,X913,X911)|~perp(X912,X910,X913,X911)|perp(X909,X908,X907,X906),inference(split_conjunct,[status(thm)],[c164])).
% 274.04/274.25 cnf(c23795,plain,para(X8204,X8205,X8205,X8204),inference(resolution,[status(thm)],[c23748, c401])).
% 274.04/274.25 cnf(c26175,plain,eqangle(X11748,X11746,X11749,X11747,X11746,X11748,X11749,X11747),inference(resolution,[status(thm)],[c23795, c287])).
% 274.04/274.25 cnf(c43186,plain,~perp(X13395,X13396,X13397,X13398)|perp(X13396,X13395,X13397,X13398),inference(resolution,[status(thm)],[c26175, c165])).
% 274.04/274.25 cnf(c1530,plain,~para(X2673,X2674,skolem0005,skolem0005)|perp(X2673,X2674,skolem0003,skolem0002),inference(resolution,[status(thm)],[c383, c1309])).
% 274.04/274.25 cnf(c1252,plain,para(skolem0005,skolem0005,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1249, c419])).
% 274.04/274.25 cnf(c1264,plain,para(skolem0003,skolem0003,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1252, c398])).
% 274.04/274.25 cnf(c1583,plain,~para(X2766,X2767,skolem0003,skolem0003)|para(X2766,X2767,skolem0005,skolem0005),inference(resolution,[status(thm)],[c395, c1264])).
% 274.04/274.25 cnf(c1473,plain,~cong(X2624,X2623,skolem0005,skolem0002)|cong(X2624,X2623,skolem0005,skolem0003),inference(resolution,[status(thm)],[c336, c497])).
% 274.04/274.25 cnf(c7434,plain,cong(skolem0005,skolem0003,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1473, c498])).
% 274.04/274.25 cnf(c7491,plain,perp(skolem0005,skolem0005,skolem0003,skolem0003),inference(resolution,[status(thm)],[c7434, c1196])).
% 274.04/274.25 cnf(c7533,plain,perp(skolem0003,skolem0003,skolem0005,skolem0005),inference(resolution,[status(thm)],[c7491, c389])).
% 274.04/274.25 cnf(c8222,plain,para(skolem0003,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1559, c7533])).
% 274.04/274.25 cnf(c8483,plain,para(skolem0003,skolem0002,skolem0003,skolem0003),inference(resolution,[status(thm)],[c8222, c398])).
% 274.04/274.25 cnf(c8769,plain,para(skolem0003,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c8483, c1583])).
% 274.04/274.25 cnf(c9026,plain,perp(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c8769, c1530])).
% 274.04/274.25 fof(ruleD21,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(A,B,P,Q,C,D,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 274.04/274.25 fof(c346,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 274.04/274.25 fof(c347,plain,(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(![X435]:(~eqangle(X428,X429,X430,X431,X432,X433,X434,X435)|eqangle(X428,X429,X432,X433,X430,X431,X434,X435)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 274.04/274.25 cnf(c348,plain,~eqangle(X1204,X1209,X1203,X1207,X1206,X1205,X1202,X1208)|eqangle(X1204,X1209,X1206,X1205,X1203,X1207,X1202,X1208),inference(split_conjunct,[status(thm)],[c347])).
% 274.04/274.25 cnf(c23785,plain,eqangle(X11164,X11166,X11165,X11163,X11164,X11166,X11165,X11163),inference(resolution,[status(thm)],[c23748, c287])).
% 274.04/274.25 cnf(c40201,plain,eqangle(X11782,X11780,X11782,X11780,X11781,X11783,X11781,X11783),inference(resolution,[status(thm)],[c23785, c348])).
% 274.04/274.25 cnf(c43281,plain,~perp(X14020,X14022,X14020,X14022)|perp(X14021,X14019,X14021,X14019),inference(resolution,[status(thm)],[c40201, c165])).
% 274.04/274.25 cnf(c47567,plain,perp(X14024,X14023,X14024,X14023),inference(resolution,[status(thm)],[c43281, c9026])).
% 274.04/274.25 cnf(c47607,plain,perp(X14078,X14079,X14079,X14078),inference(resolution,[status(thm)],[c47567, c43186])).
% 274.04/274.25 cnf(c47650,plain,~midp(X14294,X14295,X14295)|cong(X14295,X14294,X14296,X14294),inference(resolution,[status(thm)],[c47607, c242])).
% 274.04/274.25 cnf(c48319,plain,cong(X14297,skolem0005,X14298,skolem0005),inference(resolution,[status(thm)],[c47650, c40224])).
% 274.04/274.25 cnf(c48347,plain,perp(X14305,X14304,skolem0005,skolem0005),inference(resolution,[status(thm)],[c48319, c1196])).
% 274.04/274.25 cnf(c7445,plain,~perp(X14528,X14529,skolem0005,skolem0005)|para(X14528,X14529,skolem0002,skolem0002),inference(resolution,[status(thm)],[c7424, c386])).
% 274.04/274.25 cnf(c49080,plain,para(X14531,X14530,skolem0002,skolem0002),inference(resolution,[status(thm)],[c7445, c48347])).
% 274.04/274.25 cnf(c49107,plain,para(X14532,X14533,skolem0005,skolem0005),inference(resolution,[status(thm)],[c49080, c1582])).
% 274.04/274.25 cnf(c49123,plain,perp(X14542,X14543,skolem0002,skolem0003),inference(resolution,[status(thm)],[c49107, c1535])).
% 274.04/274.25 cnf(c49196,plain,para(X14574,X14575,skolem0002,skolem0001),inference(resolution,[status(thm)],[c49123, c7106])).
% 274.04/274.25 cnf(c49335,plain,perp(X14623,X14622,skolem0006,skolem0007),inference(resolution,[status(thm)],[c49196, c1542])).
% 274.04/274.25 cnf(c49415,plain,perp(skolem0006,skolem0007,X14655,X14654),inference(resolution,[status(thm)],[c49335, c389])).
% 274.04/274.25 cnf(c49506,plain,$false,inference(resolution,[status(thm)],[c49415, c25])).
% 274.04/274.25 % SZS output end CNFRefutation
% 274.04/274.25
% 274.04/274.25 % Initial clauses : 137
% 274.04/274.25 % Processed clauses : 5698
% 274.04/274.25 % Factors computed : 308
% 274.04/274.25 % Resolvents computed: 48815
% 274.04/274.25 % Tautologies deleted: 26
% 274.04/274.25 % Forward subsumed : 16190
% 274.04/274.25 % Backward subsumed : 3180
% 274.04/274.25 % -------- CPU Time ---------
% 274.04/274.25 % User time : 273.801 s
% 274.04/274.25 % System time : 0.074 s
% 274.04/274.25 % Total time : 273.875 s
%------------------------------------------------------------------------------