%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO646+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:29 EDT 2024
% Result : Theorem 36.47s 36.68s
% Output : Refutation 36.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO646+1 : TPTP v8.1.2. Released v7.5.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n021.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:32:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 36.47/36.68 % Version: 1.5
% 36.47/36.68 % SZS status Theorem
% 36.47/36.68 % SZS output start CNFRefutation
% 36.47/36.68 fof(exemplo6GDDFULLmoreE0133,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:((((((((((circle(A,B,NWPNT1,NWPNT2)&perp(A,B,B,D))&circle(A,B,C,NWPNT3))&perp(A,C,C,D))&circle(A,B,E,NWPNT4))&coll(F,D,E))&circle(A,B,F,NWPNT5))&midp(G,E,F))&coll(C,G,H))&circle(A,C,H,NWPNT6))=>para(E,F,B,H)))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0133)).
% 36.47/36.68 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:((((((((((circle(A,B,NWPNT1,NWPNT2)&perp(A,B,B,D))&circle(A,B,C,NWPNT3))&perp(A,C,C,D))&circle(A,B,E,NWPNT4))&coll(F,D,E))&circle(A,B,F,NWPNT5))&midp(G,E,F))&coll(C,G,H))&circle(A,C,H,NWPNT6))=>para(E,F,B,H))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0133])).
% 36.47/36.68 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:((((((((((circle(A,B,NWPNT1,NWPNT2)&perp(A,B,B,D))&circle(A,B,C,NWPNT3))&perp(A,C,C,D))&circle(A,B,E,NWPNT4))&coll(F,D,E))&circle(A,B,F,NWPNT5))&midp(G,E,F))&coll(C,G,H))&circle(A,C,H,NWPNT6))&~para(E,F,B,H)))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 36.47/36.68 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(((((((((((?[NWPNT1]:(?[NWPNT2]:circle(A,B,NWPNT1,NWPNT2)))&perp(A,B,B,D))&(?[NWPNT3]:circle(A,B,C,NWPNT3)))&perp(A,C,C,D))&(?[NWPNT4]:circle(A,B,E,NWPNT4)))&coll(F,D,E))&(?[NWPNT5]:circle(A,B,F,NWPNT5)))&midp(G,E,F))&coll(C,G,H))&(?[NWPNT6]:circle(A,C,H,NWPNT6)))&~para(E,F,B,H)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 36.47/36.68 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((((?[X10]:(?[X11]:circle(X2,X3,X10,X11)))&perp(X2,X3,X3,X5))&(?[X12]:circle(X2,X3,X4,X12)))&perp(X2,X4,X4,X5))&(?[X13]:circle(X2,X3,X6,X13)))&coll(X7,X5,X6))&(?[X14]:circle(X2,X3,X7,X14)))&midp(X8,X6,X7))&coll(X4,X8,X9))&(?[X15]:circle(X2,X4,X9,X15)))&~para(X6,X7,X3,X9)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 36.47/36.68 fof(c15,negated_conjecture,((((((((((circle(skolem0001,skolem0002,skolem0009,skolem0010)&perp(skolem0001,skolem0002,skolem0002,skolem0004))&circle(skolem0001,skolem0002,skolem0003,skolem0011))&perp(skolem0001,skolem0003,skolem0003,skolem0004))&circle(skolem0001,skolem0002,skolem0005,skolem0012))&coll(skolem0006,skolem0004,skolem0005))&circle(skolem0001,skolem0002,skolem0006,skolem0013))&midp(skolem0007,skolem0005,skolem0006))&coll(skolem0003,skolem0007,skolem0008))&circle(skolem0001,skolem0003,skolem0008,skolem0014))&~para(skolem0005,skolem0006,skolem0002,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 36.47/36.68 cnf(c26,negated_conjecture,~para(skolem0005,skolem0006,skolem0002,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 36.47/36.68 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 36.47/36.68 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 36.47/36.68 fof(c398,plain,(![X519]:(![X520]:(![X521]:(![X522]:(~para(X519,X520,X521,X522)|para(X521,X522,X519,X520)))))),inference(variable_rename,[status(thm)],[c397])).
% 36.47/36.68 cnf(c399,plain,~para(X758,X756,X757,X755)|para(X757,X755,X758,X756),inference(split_conjunct,[status(thm)],[c398])).
% 36.47/36.68 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 36.47/36.68 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 36.47/36.68 fof(c389,plain,(![X505]:(![X506]:(![X507]:(![X508]:(~perp(X505,X506,X507,X508)|perp(X507,X508,X505,X506)))))),inference(variable_rename,[status(thm)],[c388])).
% 36.47/36.68 cnf(c390,plain,~perp(X718,X717,X716,X719)|perp(X716,X719,X718,X717),inference(split_conjunct,[status(thm)],[c389])).
% 36.47/36.68 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 36.47/36.68 fof(c341,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 36.47/36.68 fof(c342,plain,(![X416]:(![X417]:(![X418]:(![X419]:(~cong(X416,X417,X418,X419)|cong(X416,X417,X419,X418)))))),inference(variable_rename,[status(thm)],[c341])).
% 36.47/36.68 cnf(c343,plain,~cong(X686,X685,X684,X683)|cong(X686,X685,X683,X684),inference(split_conjunct,[status(thm)],[c342])).
% 36.47/36.68 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 36.47/36.68 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 36.47/36.68 fof(c339,plain,(![X412]:(![X413]:(![X414]:(![X415]:(~cong(X412,X413,X414,X415)|cong(X414,X415,X412,X413)))))),inference(variable_rename,[status(thm)],[c338])).
% 36.47/36.68 cnf(c340,plain,~cong(X675,X673,X674,X676)|cong(X674,X676,X675,X673),inference(split_conjunct,[status(thm)],[c339])).
% 36.47/36.68 cnf(c23,negated_conjecture,midp(skolem0007,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 36.47/36.68 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 36.47/36.68 fof(c379,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 36.47/36.68 fof(c380,plain,(![X490]:(![X491]:(![X492]:(~midp(X492,X491,X490)|midp(X492,X490,X491))))),inference(variable_rename,[status(thm)],[c379])).
% 36.47/36.68 cnf(c381,plain,~midp(X566,X565,X564)|midp(X566,X564,X565),inference(split_conjunct,[status(thm)],[c380])).
% 36.47/36.68 cnf(c419,plain,midp(skolem0007,skolem0006,skolem0005),inference(resolution,[status(thm)],[c381, c23])).
% 36.47/36.68 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 36.47/36.68 fof(c186,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 36.47/36.68 fof(c187,plain,(![X164]:(![X165]:(![X166]:(~midp(X164,X165,X166)|cong(X164,X165,X164,X166))))),inference(variable_rename,[status(thm)],[c186])).
% 36.47/36.68 cnf(c188,plain,~midp(X668,X667,X669)|cong(X668,X667,X668,X669),inference(split_conjunct,[status(thm)],[c187])).
% 36.47/36.68 cnf(c483,plain,cong(skolem0007,skolem0006,skolem0007,skolem0005),inference(resolution,[status(thm)],[c188, c419])).
% 36.47/36.68 cnf(c488,plain,cong(skolem0007,skolem0006,skolem0005,skolem0007),inference(resolution,[status(thm)],[c343, c483])).
% 36.47/36.68 cnf(c490,plain,cong(skolem0005,skolem0007,skolem0007,skolem0006),inference(resolution,[status(thm)],[c488, c340])).
% 36.47/36.68 cnf(c498,plain,cong(skolem0005,skolem0007,skolem0006,skolem0007),inference(resolution,[status(thm)],[c490, c343])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 36.47/36.68 fof(c227,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])).
% 36.47/36.68 fof(c228,plain,(![X222]:(![X223]:(![X224]:(![X225]:((~cong(X222,X224,X223,X224)|~cong(X222,X225,X223,X225))|perp(X222,X223,X224,X225)))))),inference(variable_rename,[status(thm)],[c227])).
% 36.47/36.68 cnf(c229,plain,~cong(X992,X993,X994,X993)|~cong(X992,X991,X994,X991)|perp(X992,X994,X993,X991),inference(split_conjunct,[status(thm)],[c228])).
% 36.47/36.68 cnf(c1130,plain,~cong(X1021,X1022,X1023,X1022)|perp(X1021,X1023,X1022,X1022),inference(factor,[status(thm)],[c229])).
% 36.47/36.68 cnf(c1214,plain,perp(skolem0005,skolem0006,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1130, c498])).
% 36.47/36.68 cnf(c1225,plain,perp(skolem0007,skolem0007,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1214, c390])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 36.47/36.68 fof(c385,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])).
% 36.47/36.68 fof(c386,plain,(![X499]:(![X500]:(![X501]:(![X502]:(![X503]:(![X504]:((~perp(X499,X500,X501,X502)|~perp(X501,X502,X503,X504))|para(X499,X500,X503,X504)))))))),inference(variable_rename,[status(thm)],[c385])).
% 36.47/36.68 cnf(c387,plain,~perp(X1269,X1270,X1272,X1273)|~perp(X1272,X1273,X1274,X1271)|para(X1269,X1270,X1274,X1271),inference(split_conjunct,[status(thm)],[c386])).
% 36.47/36.68 cnf(c1635,plain,~perp(X2903,X2902,skolem0007,skolem0007)|para(X2903,X2902,skolem0005,skolem0006),inference(resolution,[status(thm)],[c387, c1225])).
% 36.47/36.68 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 36.47/36.68 fof(c241,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])).
% 36.47/36.68 fof(c242,plain,(![X238]:(![X239]:(![X240]:(![X241]:((~perp(X238,X239,X239,X240)|~midp(X241,X238,X240))|cong(X238,X241,X239,X241)))))),inference(variable_rename,[status(thm)],[c241])).
% 36.47/36.68 cnf(c243,plain,~perp(X1010,X1007,X1007,X1009)|~midp(X1008,X1010,X1009)|cong(X1010,X1008,X1007,X1008),inference(split_conjunct,[status(thm)],[c242])).
% 36.47/36.68 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 36.47/36.68 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 36.47/36.68 fof(c392,plain,(![X509]:(![X510]:(![X511]:(![X512]:(~perp(X509,X510,X511,X512)|perp(X509,X510,X512,X511)))))),inference(variable_rename,[status(thm)],[c391])).
% 36.47/36.68 cnf(c393,plain,~perp(X727,X725,X728,X726)|perp(X727,X725,X726,X728),inference(split_conjunct,[status(thm)],[c392])).
% 36.47/36.68 cnf(c482,plain,cong(skolem0007,skolem0005,skolem0007,skolem0006),inference(resolution,[status(thm)],[c188, c23])).
% 36.47/36.68 cnf(c489,plain,cong(skolem0007,skolem0005,skolem0006,skolem0007),inference(resolution,[status(thm)],[c343, c482])).
% 36.47/36.68 cnf(c493,plain,cong(skolem0006,skolem0007,skolem0007,skolem0005),inference(resolution,[status(thm)],[c489, c340])).
% 36.47/36.68 cnf(c501,plain,cong(skolem0006,skolem0007,skolem0005,skolem0007),inference(resolution,[status(thm)],[c493, c343])).
% 36.47/36.68 cnf(c1213,plain,perp(skolem0006,skolem0005,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1130, c501])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 36.47/36.68 fof(c382,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])).
% 36.47/36.68 fof(c383,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~para(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|perp(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c382])).
% 36.47/36.68 cnf(c384,plain,~para(X1263,X1267,X1268,X1266)|~perp(X1268,X1266,X1265,X1264)|perp(X1263,X1267,X1265,X1264),inference(split_conjunct,[status(thm)],[c383])).
% 36.47/36.68 cnf(c1588,plain,~para(X2820,X2821,skolem0006,skolem0005)|perp(X2820,X2821,skolem0007,skolem0007),inference(resolution,[status(thm)],[c384, c1213])).
% 36.47/36.68 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 36.47/36.68 fof(c266,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])).
% 36.47/36.68 fof(c267,plain,(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((~midp(X276,X273,X274)|~midp(X277,X273,X275))|para(X276,X277,X274,X275))))))),inference(variable_rename,[status(thm)],[c266])).
% 36.47/36.68 cnf(c268,plain,~midp(X1048,X1050,X1047)|~midp(X1049,X1050,X1051)|para(X1048,X1049,X1047,X1051),inference(split_conjunct,[status(thm)],[c267])).
% 36.47/36.68 cnf(c1292,plain,~midp(X1062,X1063,X1064)|para(X1062,X1062,X1064,X1064),inference(factor,[status(thm)],[c268])).
% 36.47/36.68 cnf(c1302,plain,para(skolem0007,skolem0007,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1292, c23])).
% 36.47/36.68 cnf(c1313,plain,para(skolem0006,skolem0006,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1302, c399])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 36.47/36.68 fof(c394,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])).
% 36.47/36.68 fof(c395,plain,(![X513]:(![X514]:(![X515]:(![X516]:(![X517]:(![X518]:((~para(X513,X514,X515,X516)|~para(X515,X516,X517,X518))|para(X513,X514,X517,X518)))))))),inference(variable_rename,[status(thm)],[c394])).
% 36.47/36.68 cnf(c396,plain,~para(X1278,X1275,X1280,X1279)|~para(X1280,X1279,X1277,X1276)|para(X1278,X1275,X1277,X1276),inference(split_conjunct,[status(thm)],[c395])).
% 36.47/36.68 cnf(c1648,plain,~para(X2921,X2922,skolem0006,skolem0006)|para(X2921,X2922,skolem0007,skolem0007),inference(resolution,[status(thm)],[c396, c1313])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 36.47/36.68 fof(c335,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])).
% 36.47/36.68 fof(c336,plain,(![X406]:(![X407]:(![X408]:(![X409]:(![X410]:(![X411]:((~cong(X406,X407,X408,X409)|~cong(X408,X409,X410,X411))|cong(X406,X407,X410,X411)))))))),inference(variable_rename,[status(thm)],[c335])).
% 36.47/36.68 cnf(c337,plain,~cong(X1200,X1202,X1204,X1199)|~cong(X1204,X1199,X1201,X1203)|cong(X1200,X1202,X1201,X1203),inference(split_conjunct,[status(thm)],[c336])).
% 36.47/36.68 cnf(c1443,plain,~cong(X2648,X2649,skolem0007,skolem0005)|cong(X2648,X2649,skolem0006,skolem0007),inference(resolution,[status(thm)],[c337, c489])).
% 36.47/36.68 cnf(c6897,plain,cong(skolem0006,skolem0007,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1443, c493])).
% 36.47/36.68 cnf(c6954,plain,perp(skolem0006,skolem0006,skolem0007,skolem0007),inference(resolution,[status(thm)],[c6897, c1130])).
% 36.47/36.68 cnf(c1217,plain,perp(skolem0007,skolem0007,skolem0006,skolem0005),inference(resolution,[status(thm)],[c1213, c390])).
% 36.47/36.68 cnf(c1629,plain,~perp(X2891,X2890,skolem0007,skolem0007)|para(X2891,X2890,skolem0006,skolem0005),inference(resolution,[status(thm)],[c387, c1217])).
% 36.47/36.68 cnf(c8351,plain,para(skolem0006,skolem0006,skolem0006,skolem0005),inference(resolution,[status(thm)],[c1629, c6954])).
% 36.47/36.68 cnf(c9131,plain,para(skolem0006,skolem0005,skolem0006,skolem0006),inference(resolution,[status(thm)],[c8351, c399])).
% 36.47/36.68 cnf(c9563,plain,para(skolem0006,skolem0005,skolem0007,skolem0007),inference(resolution,[status(thm)],[c9131, c1648])).
% 36.47/36.68 cnf(c9678,plain,para(skolem0007,skolem0007,skolem0006,skolem0005),inference(resolution,[status(thm)],[c9563, c399])).
% 36.47/36.68 cnf(c9741,plain,perp(skolem0007,skolem0007,skolem0007,skolem0007),inference(resolution,[status(thm)],[c9678, c1588])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 36.47/36.68 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(fof_nnf,[status(thm)],[ruleD74])).
% 36.47/36.68 fof(c163,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)],[c162])).
% 36.47/36.68 fof(c165,plain,(![X131]:(![X132]:(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:((~eqangle(X131,X132,X133,X134,X135,X136,X137,X138)|~perp(X135,X136,X137,X138))|perp(X131,X132,X133,X134)))))))))),inference(shift_quantors,[status(thm)],[fof(c164,plain,(![X131]:(![X132]:(![X133]:(![X134]:((![X135]:(![X136]:(![X137]:(![X138]:(~eqangle(X131,X132,X133,X134,X135,X136,X137,X138)|~perp(X135,X136,X137,X138))))))|perp(X131,X132,X133,X134)))))),inference(variable_rename,[status(thm)],[c163])).])).
% 36.47/36.68 cnf(c166,plain,~eqangle(X912,X911,X916,X910,X913,X917,X914,X915)|~perp(X913,X917,X914,X915)|perp(X912,X911,X916,X910),inference(split_conjunct,[status(thm)],[c165])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 36.47/36.68 fof(c347,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])).
% 36.47/36.68 fof(c348,plain,(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(~eqangle(X432,X433,X434,X435,X436,X437,X438,X439)|eqangle(X432,X433,X436,X437,X434,X435,X438,X439)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 36.47/36.68 cnf(c349,plain,~eqangle(X1224,X1223,X1217,X1220,X1221,X1219,X1222,X1218)|eqangle(X1224,X1223,X1221,X1219,X1217,X1220,X1222,X1218),inference(split_conjunct,[status(thm)],[c348])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 36.47/36.68 fof(c284,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])).
% 36.47/36.68 fof(c285,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)],[c284])).
% 36.47/36.68 fof(c287,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~para(X296,X297,X298,X299)|eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X296]:(![X297]:(![X298]:(![X299]:(~para(X296,X297,X298,X299)|(![X300]:(![X301]:eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))))))),inference(variable_rename,[status(thm)],[c285])).])).
% 36.47/36.68 cnf(c288,plain,~para(X1078,X1079,X1077,X1074)|eqangle(X1078,X1079,X1076,X1075,X1077,X1074,X1076,X1075),inference(split_conjunct,[status(thm)],[c287])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 36.47/36.68 fof(c289,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])).
% 36.47/36.68 fof(c290,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)],[c289])).
% 36.47/36.68 fof(c292,plain,(![X302]:(![X303]:(![X304]:(![X305]:(![X306]:(![X307]:(~eqangle(X302,X303,X306,X307,X304,X305,X306,X307)|para(X302,X303,X304,X305)))))))),inference(shift_quantors,[status(thm)],[fof(c291,plain,(![X302]:(![X303]:(![X304]:(![X305]:((![X306]:(![X307]:~eqangle(X302,X303,X306,X307,X304,X305,X306,X307)))|para(X302,X303,X304,X305)))))),inference(variable_rename,[status(thm)],[c290])).])).
% 36.47/36.68 cnf(c293,plain,~eqangle(X1085,X1086,X1083,X1082,X1084,X1081,X1083,X1082)|para(X1085,X1086,X1084,X1081),inference(split_conjunct,[status(thm)],[c292])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 36.47/36.68 fof(c353,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])).
% 36.47/36.68 fof(c354,plain,(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(~eqangle(X448,X449,X450,X451,X452,X453,X454,X455)|eqangle(X450,X451,X448,X449,X454,X455,X452,X453)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 36.47/36.68 cnf(c355,plain,~eqangle(X1237,X1233,X1236,X1235,X1234,X1238,X1239,X1240)|eqangle(X1236,X1235,X1237,X1233,X1239,X1240,X1234,X1238),inference(split_conjunct,[status(thm)],[c354])).
% 36.47/36.68 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 36.47/36.68 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 36.47/36.68 fof(c401,plain,(![X523]:(![X524]:(![X525]:(![X526]:(~para(X523,X524,X525,X526)|para(X523,X524,X526,X525)))))),inference(variable_rename,[status(thm)],[c400])).
% 36.47/36.68 cnf(c402,plain,~para(X767,X766,X768,X765)|para(X767,X766,X765,X768),inference(split_conjunct,[status(thm)],[c401])).
% 36.47/36.68 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 36.47/36.68 fof(c201,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])).
% 36.47/36.68 fof(c202,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c201])).
% 36.47/36.68 fof(c204,plain,(![X183]:(![X184]:(![X185]:(![X186]:(![X187]:((~midp(X187,X183,X184)|~midp(X187,X185,X186))|para(X183,X185,X184,X186))))))),inference(shift_quantors,[status(thm)],[fof(c203,plain,(![X183]:(![X184]:(![X185]:(![X186]:((![X187]:(~midp(X187,X183,X184)|~midp(X187,X185,X186)))|para(X183,X185,X184,X186)))))),inference(variable_rename,[status(thm)],[c202])).])).
% 36.47/36.68 cnf(c205,plain,~midp(X954,X953,X955)|~midp(X954,X957,X956)|para(X953,X957,X955,X956),inference(split_conjunct,[status(thm)],[c204])).
% 36.47/36.68 cnf(c1074,plain,~midp(skolem0007,X1648,X1649)|para(X1648,skolem0005,X1649,skolem0006),inference(resolution,[status(thm)],[c205, c23])).
% 36.47/36.68 cnf(c2958,plain,para(skolem0006,skolem0005,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1074, c419])).
% 36.47/36.68 cnf(c2969,plain,para(skolem0006,skolem0005,skolem0006,skolem0005),inference(resolution,[status(thm)],[c2958, c402])).
% 36.47/36.68 cnf(c2974,plain,eqangle(skolem0006,skolem0005,X2384,X2383,skolem0006,skolem0005,X2384,X2383),inference(resolution,[status(thm)],[c2969, c288])).
% 36.47/36.68 cnf(c4938,plain,eqangle(X3338,X3339,skolem0006,skolem0005,X3338,X3339,skolem0006,skolem0005),inference(resolution,[status(thm)],[c2974, c355])).
% 36.47/36.68 cnf(c10489,plain,para(X3341,X3340,X3341,X3340),inference(resolution,[status(thm)],[c4938, c293])).
% 36.47/36.68 cnf(c10551,plain,eqangle(X3908,X3909,X3910,X3907,X3908,X3909,X3910,X3907),inference(resolution,[status(thm)],[c10489, c288])).
% 36.47/36.68 cnf(c15690,plain,eqangle(X4161,X4163,X4161,X4163,X4160,X4162,X4160,X4162),inference(resolution,[status(thm)],[c10551, c349])).
% 36.47/36.68 cnf(c16282,plain,~perp(X5182,X5183,X5182,X5183)|perp(X5181,X5180,X5181,X5180),inference(resolution,[status(thm)],[c15690, c166])).
% 36.47/36.68 cnf(c18059,plain,perp(X5185,X5184,X5185,X5184),inference(resolution,[status(thm)],[c16282, c9741])).
% 36.47/36.68 cnf(c18096,plain,perp(X5191,X5190,X5190,X5191),inference(resolution,[status(thm)],[c18059, c393])).
% 36.47/36.68 cnf(c18130,plain,~midp(X5353,X5351,X5351)|cong(X5351,X5353,X5352,X5353),inference(resolution,[status(thm)],[c18096, c243])).
% 36.47/36.68 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 36.47/36.68 fof(c198,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])).
% 36.47/36.68 fof(c199,plain,(![X178]:(![X179]:(![X180]:(![X181]:(![X182]:(((~midp(X182,X178,X179)|~para(X178,X180,X179,X181))|~para(X178,X181,X179,X180))|midp(X182,X180,X181))))))),inference(variable_rename,[status(thm)],[c198])).
% 36.47/36.68 cnf(c200,plain,~midp(X952,X951,X948)|~para(X951,X949,X948,X950)|~para(X951,X950,X948,X949)|midp(X952,X949,X950),inference(split_conjunct,[status(thm)],[c199])).
% 36.47/36.68 cnf(c1072,plain,~midp(X2264,X2267,X2265)|~para(X2267,X2266,X2265,X2266)|midp(X2264,X2266,X2266),inference(factor,[status(thm)],[c200])).
% 36.47/36.68 cnf(c10544,plain,~midp(X3901,X3903,X3903)|midp(X3901,X3902,X3902),inference(resolution,[status(thm)],[c10489, c1072])).
% 36.47/36.68 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 36.47/36.68 fof(c403,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 36.47/36.68 fof(c404,plain,(![X527]:(![X528]:(![X529]:(![X530]:((~coll(X527,X528,X529)|~coll(X527,X528,X530))|coll(X529,X530,X527)))))),inference(variable_rename,[status(thm)],[c403])).
% 36.47/36.68 cnf(c405,plain,~coll(X778,X776,X777)|~coll(X778,X776,X775)|coll(X777,X775,X778),inference(split_conjunct,[status(thm)],[c404])).
% 36.47/36.68 cnf(c584,plain,~coll(X781,X780,X779)|coll(X779,X779,X781),inference(factor,[status(thm)],[c405])).
% 36.47/36.68 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 36.47/36.68 fof(c192,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 36.47/36.68 fof(c193,plain,(![X170]:(![X171]:(![X172]:(~para(X170,X171,X170,X172)|coll(X170,X171,X172))))),inference(variable_rename,[status(thm)],[c192])).
% 36.47/36.68 cnf(c194,plain,~para(X672,X670,X672,X671)|coll(X672,X670,X671),inference(split_conjunct,[status(thm)],[c193])).
% 36.47/36.68 cnf(c10510,plain,coll(X3346,X3345,X3345),inference(resolution,[status(thm)],[c10489, c194])).
% 36.47/36.68 cnf(c10575,plain,coll(X3347,X3347,X3348),inference(resolution,[status(thm)],[c10510, c584])).
% 36.47/36.68 cnf(c10797,plain,~coll(X4042,X4042,X4041)|coll(X4041,X4040,X4042),inference(resolution,[status(thm)],[c10575, c405])).
% 36.47/36.68 cnf(c15938,plain,coll(X4045,X4044,X4043),inference(resolution,[status(thm)],[c10797, c10575])).
% 36.47/36.68 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 36.47/36.68 fof(c189,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 36.47/36.68 fof(c190,plain,(![X167]:(![X168]:(![X169]:((~cong(X167,X168,X167,X169)|~coll(X167,X168,X169))|midp(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c189])).
% 36.47/36.68 cnf(c191,plain,~cong(X942,X940,X942,X941)|~coll(X942,X940,X941)|midp(X942,X940,X941),inference(split_conjunct,[status(thm)],[c190])).
% 36.47/36.68 fof(ruleD42b,axiom,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&coll(P,Q,B))=>cyclic(A,B,P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 36.47/36.68 fof(c274,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|~coll(P,Q,B))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD42b])).
% 36.47/36.68 fof(c275,plain,(![X284]:(![X285]:(![X286]:(![X287]:((~eqangle(X286,X284,X286,X285,X287,X284,X287,X285)|~coll(X286,X287,X285))|cyclic(X284,X285,X286,X287)))))),inference(variable_rename,[status(thm)],[c274])).
% 36.47/36.68 cnf(c276,plain,~eqangle(X1058,X1060,X1058,X1059,X1061,X1060,X1061,X1059)|~coll(X1058,X1061,X1059)|cyclic(X1060,X1059,X1058,X1061),inference(split_conjunct,[status(thm)],[c275])).
% 36.47/36.68 cnf(c15680,plain,~coll(X4343,X4343,X4341)|cyclic(X4342,X4341,X4343,X4343),inference(resolution,[status(thm)],[c10551, c276])).
% 36.47/36.68 cnf(c16829,plain,cyclic(X4349,X4350,X4348,X4348),inference(resolution,[status(thm)],[c15680, c15938])).
% 36.47/36.68 fof(ruleD43,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((cyclic(A,B,C,P)&cyclic(A,B,C,Q))&cyclic(A,B,C,R))&eqangle(C,A,C,B,R,P,R,Q))=>cong(A,B,P,Q)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 36.47/36.68 fof(c269,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 36.47/36.68 fof(c270,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c269])).
% 36.47/36.68 fof(c272,plain,(![X278]:(![X279]:(![X280]:(![X281]:(![X282]:(![X283]:((((~cyclic(X278,X279,X280,X281)|~cyclic(X278,X279,X280,X282))|~cyclic(X278,X279,X280,X283))|~eqangle(X280,X278,X280,X279,X283,X281,X283,X282))|cong(X278,X279,X281,X282)))))))),inference(shift_quantors,[status(thm)],[fof(c271,plain,(![X278]:(![X279]:(![X280]:(![X281]:(![X282]:((![X283]:(((~cyclic(X278,X279,X280,X281)|~cyclic(X278,X279,X280,X282))|~cyclic(X278,X279,X280,X283))|~eqangle(X280,X278,X280,X279,X283,X281,X283,X282)))|cong(X278,X279,X281,X282))))))),inference(variable_rename,[status(thm)],[c270])).])).
% 36.47/36.68 cnf(c273,plain,~cyclic(X1053,X1057,X1054,X1055)|~cyclic(X1053,X1057,X1054,X1056)|~cyclic(X1053,X1057,X1054,X1052)|~eqangle(X1054,X1053,X1054,X1057,X1052,X1055,X1052,X1056)|cong(X1053,X1057,X1055,X1056),inference(split_conjunct,[status(thm)],[c272])).
% 36.47/36.68 cnf(c10542,plain,para(X3368,X3367,X3367,X3368),inference(resolution,[status(thm)],[c10489, c402])).
% 36.47/36.68 cnf(c11428,plain,eqangle(X4145,X4144,X4146,X4143,X4144,X4145,X4146,X4143),inference(resolution,[status(thm)],[c10542, c288])).
% 36.47/36.68 cnf(c16260,plain,eqangle(X4181,X4182,X4184,X4183,X4181,X4182,X4183,X4184),inference(resolution,[status(thm)],[c11428, c355])).
% 36.47/36.68 cnf(c16366,plain,eqangle(X4235,X4237,X4235,X4237,X4236,X4234,X4234,X4236),inference(resolution,[status(thm)],[c16260, c349])).
% 36.47/36.68 cnf(c16479,plain,~cyclic(X5388,X5388,X5387,X5386)|cong(X5388,X5388,X5386,X5386),inference(resolution,[status(thm)],[c16366, c273])).
% 36.47/36.68 cnf(c18835,plain,cong(X5391,X5391,X5392,X5392),inference(resolution,[status(thm)],[c16479, c16829])).
% 36.47/36.68 cnf(c18845,plain,~coll(X5413,X5413,X5413)|midp(X5413,X5413,X5413),inference(resolution,[status(thm)],[c18835, c191])).
% 36.47/36.68 cnf(c18891,plain,midp(X5414,X5414,X5414),inference(resolution,[status(thm)],[c18845, c15938])).
% 36.47/36.68 cnf(c18901,plain,midp(X5416,X5415,X5415),inference(resolution,[status(thm)],[c18891, c10544])).
% 36.47/36.68 cnf(c18936,plain,cong(X5437,X5439,X5438,X5439),inference(resolution,[status(thm)],[c18901, c18130])).
% 36.47/36.68 cnf(c19104,plain,perp(X5466,X5464,X5465,X5465),inference(resolution,[status(thm)],[c18936, c1130])).
% 36.47/36.68 cnf(c19360,plain,para(X5585,X5586,skolem0005,skolem0006),inference(resolution,[status(thm)],[c19104, c1635])).
% 36.47/36.68 cnf(c19740,plain,para(skolem0005,skolem0006,X5646,X5647),inference(resolution,[status(thm)],[c19360, c399])).
% 36.47/36.68 cnf(c19989,plain,$false,inference(resolution,[status(thm)],[c19740, c26])).
% 36.47/36.68 % SZS output end CNFRefutation
% 36.47/36.68
% 36.47/36.68 % Initial clauses : 138
% 36.47/36.68 % Processed clauses : 2320
% 36.47/36.68 % Factors computed : 145
% 36.47/36.68 % Resolvents computed: 19466
% 36.47/36.68 % Tautologies deleted: 19
% 36.47/36.68 % Forward subsumed : 5170
% 36.47/36.68 % Backward subsumed : 1472
% 36.47/36.68 % -------- CPU Time ---------
% 36.47/36.68 % User time : 36.270 s
% 36.47/36.68 % System time : 0.038 s
% 36.47/36.68 % Total time : 36.308 s
%------------------------------------------------------------------------------