%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO559+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:17 EDT 2024
% Result : Theorem 126.44s 126.65s
% Output : Refutation 126.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GEO559+1 : TPTP v8.1.2. Released v7.5.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 07:56:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 126.44/126.65 % Version: 1.5
% 126.44/126.65 % SZS status Theorem
% 126.44/126.65 % SZS output start CNFRefutation
% 126.44/126.65 fof(exemplo6GDDFULL012019,conjecture,(![A]:(![B]:(![C]:(![O]:(![F]:(![P]:(![E]:(![D]:(![NWPNT1]:(![NWPNT2]:((((((circle(O,A,B,C)&circle(P,A,B,F))&circle(P,A,E,NWPNT1))&coll(E,A,C))&circle(O,B,D,NWPNT2))&coll(D,B,F))=>para(C,D,E,F)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL012019)).
% 126.44/126.65 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![F]:(![P]:(![E]:(![D]:(![NWPNT1]:(![NWPNT2]:((((((circle(O,A,B,C)&circle(P,A,B,F))&circle(P,A,E,NWPNT1))&coll(E,A,C))&circle(O,B,D,NWPNT2))&coll(D,B,F))=>para(C,D,E,F))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012019])).
% 126.44/126.65 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[F]:(?[P]:(?[E]:(?[D]:(?[NWPNT1]:(?[NWPNT2]:((((((circle(O,A,B,C)&circle(P,A,B,F))&circle(P,A,E,NWPNT1))&coll(E,A,C))&circle(O,B,D,NWPNT2))&coll(D,B,F))&~para(C,D,E,F)))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 126.44/126.65 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[F]:(?[P]:(?[E]:(?[D]:((((((circle(O,A,B,C)&circle(P,A,B,F))&(?[NWPNT1]:circle(P,A,E,NWPNT1)))&coll(E,A,C))&(?[NWPNT2]:circle(O,B,D,NWPNT2)))&coll(D,B,F))&~para(C,D,E,F)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 126.44/126.65 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((circle(X5,X2,X3,X4)&circle(X7,X2,X3,X6))&(?[X10]:circle(X7,X2,X8,X10)))&coll(X8,X2,X4))&(?[X11]:circle(X5,X3,X9,X11)))&coll(X9,X3,X6))&~para(X4,X9,X8,X6)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 126.44/126.65 fof(c15,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0006,skolem0001,skolem0002,skolem0005))&circle(skolem0006,skolem0001,skolem0007,skolem0009))&coll(skolem0007,skolem0001,skolem0003))&circle(skolem0004,skolem0002,skolem0008,skolem0010))&coll(skolem0008,skolem0002,skolem0005))&~para(skolem0003,skolem0008,skolem0007,skolem0005)),inference(skolemize,[status(esa)],[c14])).
% 126.44/126.65 cnf(c22,negated_conjecture,~para(skolem0003,skolem0008,skolem0007,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 126.44/126.65 fof(c400,plain,(![X523]:(![X524]:(![X525]:(![X526]:((~coll(X523,X524,X525)|~coll(X523,X524,X526))|coll(X525,X526,X523)))))),inference(variable_rename,[status(thm)],[c399])).
% 126.44/126.65 cnf(c401,plain,~coll(X689,X687,X688)|~coll(X689,X687,X690)|coll(X688,X690,X689),inference(split_conjunct,[status(thm)],[c400])).
% 126.44/126.65 cnf(c451,plain,~coll(X692,X691,X693)|coll(X693,X693,X692),inference(factor,[status(thm)],[c401])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 126.44/126.65 fof(c189,plain,(![X166]:(![X167]:(![X168]:(~para(X166,X167,X166,X168)|coll(X166,X167,X168))))),inference(variable_rename,[status(thm)],[c188])).
% 126.44/126.65 cnf(c190,plain,~para(X610,X611,X610,X612)|coll(X610,X611,X612),inference(split_conjunct,[status(thm)],[c189])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c285,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])).
% 126.44/126.65 fof(c286,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)],[c285])).
% 126.44/126.65 fof(c288,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(c287,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)],[c286])).])).
% 126.44/126.65 cnf(c289,plain,~eqangle(X1135,X1139,X1137,X1134,X1138,X1136,X1137,X1134)|para(X1135,X1139,X1138,X1136),inference(split_conjunct,[status(thm)],[c288])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c349,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])).
% 126.44/126.65 fof(c350,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)],[c349])).
% 126.44/126.65 cnf(c351,plain,~eqangle(X1342,X1343,X1337,X1341,X1344,X1338,X1339,X1340)|eqangle(X1337,X1341,X1342,X1343,X1339,X1340,X1344,X1338),inference(split_conjunct,[status(thm)],[c350])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c280,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])).
% 126.44/126.65 fof(c281,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)],[c280])).
% 126.44/126.65 fof(c283,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(c282,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)],[c281])).])).
% 126.44/126.65 cnf(c284,plain,~para(X1119,X1123,X1120,X1121)|eqangle(X1119,X1123,X1122,X1124,X1120,X1121,X1122,X1124),inference(split_conjunct,[status(thm)],[c283])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 126.44/126.65 fof(c385,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X503,X504,X501,X502)))))),inference(variable_rename,[status(thm)],[c384])).
% 126.44/126.65 cnf(c386,plain,~perp(X649,X652,X651,X650)|perp(X651,X650,X649,X652),inference(split_conjunct,[status(thm)],[c385])).
% 126.44/126.65 cnf(c16,negated_conjecture,circle(skolem0004,skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 126.44/126.65 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 126.44/126.65 fof(c71,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 126.44/126.65 fof(c72,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c71])).
% 126.44/126.65 fof(c73,plain,(![X54]:(![X55]:(![X56]:(![X57]:(~circle(X57,X54,X55,X56)|(?[X58]:perp(X58,X54,X54,X57))))))),inference(variable_rename,[status(thm)],[c72])).
% 126.44/126.65 fof(c74,plain,(![X54]:(![X55]:(![X56]:(![X57]:(~circle(X57,X54,X55,X56)|perp(skolem0019(X54,X55,X56,X57),X54,X54,X57)))))),inference(skolemize,[status(esa)],[c73])).
% 126.44/126.65 cnf(c75,plain,~circle(X786,X787,X784,X785)|perp(skolem0019(X787,X784,X785,X786),X787,X787,X786),inference(split_conjunct,[status(thm)],[c74])).
% 126.44/126.65 cnf(c681,plain,perp(skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001,skolem0001,skolem0004),inference(resolution,[status(thm)],[c75, c16])).
% 126.44/126.65 cnf(c961,plain,perp(skolem0001,skolem0004,skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001),inference(resolution,[status(thm)],[c681, c386])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c381,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])).
% 126.44/126.65 fof(c382,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)],[c381])).
% 126.44/126.65 cnf(c383,plain,~perp(X1263,X1267,X1265,X1264)|~perp(X1265,X1264,X1268,X1266)|para(X1263,X1267,X1268,X1266),inference(split_conjunct,[status(thm)],[c382])).
% 126.44/126.65 cnf(c950,plain,~perp(X1841,X1842,skolem0019(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001)|para(X1841,X1842,skolem0001,skolem0004),inference(resolution,[status(thm)],[c681, c383])).
% 126.44/126.65 cnf(c3318,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c950, c961])).
% 126.44/126.65 cnf(c4983,plain,eqangle(skolem0001,skolem0004,X3909,X3908,skolem0001,skolem0004,X3909,X3908),inference(resolution,[status(thm)],[c3318, c284])).
% 126.44/126.65 cnf(c11207,plain,eqangle(X5351,X5352,skolem0001,skolem0004,X5351,X5352,skolem0001,skolem0004),inference(resolution,[status(thm)],[c4983, c351])).
% 126.44/126.65 cnf(c14869,plain,para(X5353,X5354,X5353,X5354),inference(resolution,[status(thm)],[c11207, c289])).
% 126.44/126.65 cnf(c14909,plain,coll(X5356,X5355,X5355),inference(resolution,[status(thm)],[c14869, c190])).
% 126.44/126.65 cnf(c15299,plain,coll(X5363,X5363,X5362),inference(resolution,[status(thm)],[c14909, c451])).
% 126.44/126.65 cnf(c15546,plain,~coll(X7431,X7431,X7432)|coll(X7432,X7433,X7431),inference(resolution,[status(thm)],[c15299, c401])).
% 126.44/126.65 cnf(c26035,plain,coll(X7439,X7440,X7438),inference(resolution,[status(thm)],[c15546, c15299])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c185,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 126.44/126.65 fof(c186,plain,(![X163]:(![X164]:(![X165]:((~cong(X163,X164,X163,X165)|~coll(X163,X164,X165))|midp(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c185])).
% 126.44/126.65 cnf(c187,plain,~cong(X959,X958,X959,X960)|~coll(X959,X958,X960)|midp(X959,X958,X960),inference(split_conjunct,[status(thm)],[c186])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 126.44/126.65 fof(c338,plain,(![X412]:(![X413]:(![X414]:(![X415]:(~cong(X412,X413,X414,X415)|cong(X412,X413,X415,X414)))))),inference(variable_rename,[status(thm)],[c337])).
% 126.44/126.65 cnf(c339,plain,~cong(X618,X620,X617,X619)|cong(X618,X620,X619,X617),inference(split_conjunct,[status(thm)],[c338])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 126.44/126.65 fof(c335,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X410,X411,X408,X409)))))),inference(variable_rename,[status(thm)],[c334])).
% 126.44/126.65 cnf(c336,plain,~cong(X614,X615,X616,X613)|cong(X616,X613,X614,X615),inference(split_conjunct,[status(thm)],[c335])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c194,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])).
% 126.44/126.65 fof(c195,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)],[c194])).
% 126.44/126.65 cnf(c196,plain,~midp(X969,X971,X973)|~para(X971,X970,X973,X972)|~para(X971,X972,X973,X970)|midp(X969,X970,X972),inference(split_conjunct,[status(thm)],[c195])).
% 126.44/126.65 cnf(c835,plain,~midp(X1200,X1203,X1202)|~para(X1203,X1201,X1202,X1201)|midp(X1200,X1201,X1201),inference(factor,[status(thm)],[c196])).
% 126.44/126.65 cnf(c14917,plain,~midp(X7213,X7211,X7211)|midp(X7213,X7212,X7212),inference(resolution,[status(thm)],[c14869, c835])).
% 126.44/126.65 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 126.44/126.65 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 126.44/126.65 fof(c359,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X466,X465,X467,X468)))))),inference(variable_rename,[status(thm)],[c358])).
% 126.44/126.65 cnf(c360,plain,~cyclic(X623,X624,X621,X622)|cyclic(X624,X623,X621,X622),inference(split_conjunct,[status(thm)],[c359])).
% 126.44/126.65 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 126.44/126.65 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 126.44/126.65 fof(c362,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X471,X470,X472)))))),inference(variable_rename,[status(thm)],[c361])).
% 126.44/126.65 cnf(c363,plain,~cyclic(X641,X643,X644,X642)|cyclic(X641,X644,X643,X642),inference(split_conjunct,[status(thm)],[c362])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c270,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])).
% 126.44/126.65 fof(c271,plain,(![X280]:(![X281]:(![X282]:(![X283]:((~eqangle(X282,X280,X282,X281,X283,X280,X283,X281)|~coll(X282,X283,X281))|cyclic(X280,X281,X282,X283)))))),inference(variable_rename,[status(thm)],[c270])).
% 126.44/126.65 cnf(c272,plain,~eqangle(X1103,X1105,X1103,X1106,X1104,X1105,X1104,X1106)|~coll(X1103,X1104,X1106)|cyclic(X1105,X1106,X1103,X1104),inference(split_conjunct,[status(thm)],[c271])).
% 126.44/126.65 cnf(c14884,plain,eqangle(X7200,X7201,X7202,X7199,X7200,X7201,X7202,X7199),inference(resolution,[status(thm)],[c14869, c284])).
% 126.44/126.65 cnf(c25611,plain,~coll(X7771,X7771,X7772)|cyclic(X7773,X7772,X7771,X7771),inference(resolution,[status(thm)],[c14884, c272])).
% 126.44/126.65 cnf(c26611,plain,cyclic(X7778,X7779,X7777,X7777),inference(resolution,[status(thm)],[c25611, c26035])).
% 126.44/126.65 cnf(c26613,plain,cyclic(X7782,X7780,X7781,X7780),inference(resolution,[status(thm)],[c26611, c363])).
% 126.44/126.65 cnf(c26627,plain,cyclic(X7800,X7799,X7798,X7800),inference(resolution,[status(thm)],[c26613, c360])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c265,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])).
% 126.44/126.65 fof(c266,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)],[c265])).
% 126.44/126.65 fof(c268,plain,(![X274]:(![X275]:(![X276]:(![X277]:(![X278]:(![X279]:((((~cyclic(X274,X275,X276,X277)|~cyclic(X274,X275,X276,X278))|~cyclic(X274,X275,X276,X279))|~eqangle(X276,X274,X276,X275,X279,X277,X279,X278))|cong(X274,X275,X277,X278)))))))),inference(shift_quantors,[status(thm)],[fof(c267,plain,(![X274]:(![X275]:(![X276]:(![X277]:(![X278]:((![X279]:(((~cyclic(X274,X275,X276,X277)|~cyclic(X274,X275,X276,X278))|~cyclic(X274,X275,X276,X279))|~eqangle(X276,X274,X276,X275,X279,X277,X279,X278)))|cong(X274,X275,X277,X278))))))),inference(variable_rename,[status(thm)],[c266])).])).
% 126.44/126.65 cnf(c269,plain,~cyclic(X1096,X1099,X1100,X1101)|~cyclic(X1096,X1099,X1100,X1097)|~cyclic(X1096,X1099,X1100,X1098)|~eqangle(X1100,X1096,X1100,X1099,X1098,X1101,X1098,X1097)|cong(X1096,X1099,X1101,X1097),inference(split_conjunct,[status(thm)],[c268])).
% 126.44/126.65 fof(ruleD20,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 126.44/126.65 fof(c346,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD20])).
% 126.44/126.65 fof(c347,plain,(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(~eqangle(X436,X437,X438,X439,X440,X441,X442,X443)|eqangle(X440,X441,X442,X443,X436,X437,X438,X439)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 126.44/126.65 cnf(c348,plain,~eqangle(X1332,X1330,X1336,X1335,X1333,X1334,X1329,X1331)|eqangle(X1333,X1334,X1329,X1331,X1332,X1330,X1336,X1335),inference(split_conjunct,[status(thm)],[c347])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c343,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])).
% 126.44/126.65 fof(c344,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)],[c343])).
% 126.44/126.65 cnf(c345,plain,~eqangle(X1325,X1321,X1324,X1323,X1322,X1326,X1328,X1327)|eqangle(X1325,X1321,X1322,X1326,X1324,X1323,X1328,X1327),inference(split_conjunct,[status(thm)],[c344])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 126.44/126.65 fof(c397,plain,(![X519]:(![X520]:(![X521]:(![X522]:(~para(X519,X520,X521,X522)|para(X519,X520,X522,X521)))))),inference(variable_rename,[status(thm)],[c396])).
% 126.44/126.65 cnf(c398,plain,~para(X679,X678,X680,X677)|para(X679,X678,X677,X680),inference(split_conjunct,[status(thm)],[c397])).
% 126.44/126.65 cnf(c14901,plain,para(X5377,X5378,X5378,X5377),inference(resolution,[status(thm)],[c14869, c398])).
% 126.44/126.65 cnf(c16401,plain,eqangle(X7568,X7567,X7569,X7566,X7567,X7568,X7569,X7566),inference(resolution,[status(thm)],[c14901, c284])).
% 126.44/126.65 cnf(c26343,plain,eqangle(X7607,X7608,X7608,X7607,X7609,X7606,X7609,X7606),inference(resolution,[status(thm)],[c16401, c345])).
% 126.44/126.65 cnf(c26412,plain,eqangle(X7669,X7667,X7669,X7667,X7670,X7668,X7668,X7670),inference(resolution,[status(thm)],[c26343, c348])).
% 126.44/126.65 cnf(c26472,plain,~cyclic(X8720,X8720,X8718,X8719)|cong(X8720,X8720,X8719,X8719),inference(resolution,[status(thm)],[c26412, c269])).
% 126.44/126.65 cnf(c27370,plain,cong(X8721,X8721,X8721,X8721),inference(resolution,[status(thm)],[c26472, c26627])).
% 126.44/126.65 cnf(c27379,plain,~coll(X8785,X8785,X8785)|midp(X8785,X8785,X8785),inference(resolution,[status(thm)],[c27370, c187])).
% 126.44/126.65 cnf(c27578,plain,midp(X8786,X8786,X8786),inference(resolution,[status(thm)],[c27379, c26035])).
% 126.44/126.65 cnf(c27904,plain,midp(X8789,X8788,X8788),inference(resolution,[status(thm)],[c27578, c14917])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c237,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])).
% 126.44/126.65 fof(c238,plain,(![X234]:(![X235]:(![X236]:(![X237]:((~perp(X234,X235,X235,X236)|~midp(X237,X234,X236))|cong(X234,X237,X235,X237)))))),inference(variable_rename,[status(thm)],[c237])).
% 126.44/126.65 cnf(c239,plain,~perp(X1044,X1043,X1043,X1042)|~midp(X1045,X1044,X1042)|cong(X1044,X1045,X1043,X1045),inference(split_conjunct,[status(thm)],[c238])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c158,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])).
% 126.44/126.65 fof(c159,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)],[c158])).
% 126.44/126.65 fof(c161,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(c160,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)],[c159])).])).
% 126.44/126.65 cnf(c162,plain,~eqangle(X922,X927,X923,X924,X925,X928,X926,X929)|~perp(X925,X928,X926,X929)|perp(X922,X927,X923,X924),inference(split_conjunct,[status(thm)],[c161])).
% 126.44/126.65 cnf(c26408,plain,~perp(X8684,X8682,X8684,X8682)|perp(X8681,X8683,X8683,X8681),inference(resolution,[status(thm)],[c26343, c162])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c223,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])).
% 126.44/126.65 fof(c224,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)],[c223])).
% 126.44/126.65 cnf(c225,plain,~cong(X1020,X1019,X1018,X1019)|~cong(X1020,X1021,X1018,X1021)|perp(X1020,X1018,X1019,X1021),inference(split_conjunct,[status(thm)],[c224])).
% 126.44/126.65 cnf(c862,plain,~cong(X1022,X1023,X1024,X1023)|perp(X1022,X1024,X1023,X1023),inference(factor,[status(thm)],[c225])).
% 126.44/126.65 cnf(c27376,plain,perp(X8734,X8734,X8734,X8734),inference(resolution,[status(thm)],[c27370, c862])).
% 126.44/126.65 cnf(c27462,plain,perp(X8760,X8761,X8761,X8760),inference(resolution,[status(thm)],[c27376, c26408])).
% 126.44/126.65 cnf(c27551,plain,~midp(X9566,X9565,X9565)|cong(X9565,X9566,X9564,X9566),inference(resolution,[status(thm)],[c27462, c239])).
% 126.44/126.65 cnf(c29914,plain,cong(X9569,X9567,X9568,X9567),inference(resolution,[status(thm)],[c27551, c27904])).
% 126.44/126.65 cnf(c29941,plain,cong(X9581,X9583,X9583,X9582),inference(resolution,[status(thm)],[c29914, c339])).
% 126.44/126.65 cnf(c29990,plain,cong(X9594,X9595,X9593,X9594),inference(resolution,[status(thm)],[c29941, c336])).
% 126.44/126.65 cnf(c30090,plain,cong(X9624,X9622,X9624,X9623),inference(resolution,[status(thm)],[c29990, c339])).
% 126.44/126.65 cnf(c30114,plain,~coll(X9817,X9819,X9818)|midp(X9817,X9819,X9818),inference(resolution,[status(thm)],[c30090, c187])).
% 126.44/126.65 cnf(c31975,plain,midp(X9824,X9823,X9825),inference(resolution,[status(thm)],[c30114, c26035])).
% 126.44/126.65 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)).
% 126.44/126.65 fof(c262,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])).
% 126.44/126.65 fof(c263,plain,(![X269]:(![X270]:(![X271]:(![X272]:(![X273]:((~midp(X272,X269,X270)|~midp(X273,X269,X271))|para(X272,X273,X270,X271))))))),inference(variable_rename,[status(thm)],[c262])).
% 126.44/126.65 cnf(c264,plain,~midp(X1091,X1090,X1088)|~midp(X1087,X1090,X1089)|para(X1091,X1087,X1088,X1089),inference(split_conjunct,[status(thm)],[c263])).
% 126.44/126.65 cnf(c28075,plain,~midp(X12897,X12898,X12899)|para(X12897,X12896,X12899,X12898),inference(resolution,[status(thm)],[c27904, c264])).
% 126.44/126.65 cnf(c35188,plain,para(X12903,X12901,X12900,X12902),inference(resolution,[status(thm)],[c28075, c31975])).
% 126.44/126.65 cnf(c35225,plain,$false,inference(resolution,[status(thm)],[c35188, c22])).
% 126.44/126.65 % SZS output end CNFRefutation
% 126.44/126.65
% 126.44/126.65 % Initial clauses : 134
% 126.44/126.65 % Processed clauses : 4137
% 126.44/126.65 % Factors computed : 189
% 126.44/126.65 % Resolvents computed: 34630
% 126.44/126.65 % Tautologies deleted: 15
% 126.44/126.65 % Forward subsumed : 10916
% 126.44/126.65 % Backward subsumed : 3570
% 126.44/126.65 % -------- CPU Time ---------
% 126.44/126.65 % User time : 126.199 s
% 126.44/126.65 % System time : 0.074 s
% 126.44/126.65 % Total time : 126.273 s
%------------------------------------------------------------------------------