%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO611+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:24 EDT 2024
% Result : Theorem 54.99s 55.17s
% Output : Refutation 54.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : GEO611+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 07:56:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 54.99/55.17 % Version: 1.5
% 54.99/55.17 % SZS status Theorem
% 54.99/55.17 % SZS output start CNFRefutation
% 54.99/55.17 fof(exemplo6GDDFULL618073,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:((((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&perp(F,E,A,C))&coll(F,A,C))&perp(G,E,A,B))&coll(G,A,B))&circle(D,E,H,NWPNT2))&coll(H,E,G))=>para(G,F,H,C)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618073)).
% 54.99/55.17 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:((((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&perp(F,E,A,C))&coll(F,A,C))&perp(G,E,A,B))&coll(G,A,B))&circle(D,E,H,NWPNT2))&coll(H,E,G))=>para(G,F,H,C))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618073])).
% 54.99/55.17 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(?[NWPNT1]:(?[NWPNT2]:((((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&perp(F,E,A,C))&coll(F,A,C))&perp(G,E,A,B))&coll(G,A,B))&circle(D,E,H,NWPNT2))&coll(H,E,G))&~para(G,F,H,C)))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 54.99/55.17 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:((((((((circle(D,A,B,C)&(?[NWPNT1]:circle(D,A,E,NWPNT1)))&perp(F,E,A,C))&coll(F,A,C))&perp(G,E,A,B))&coll(G,A,B))&(?[NWPNT2]:circle(D,E,H,NWPNT2)))&coll(H,E,G))&~para(G,F,H,C)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 54.99/55.17 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((circle(X5,X2,X3,X4)&(?[X10]:circle(X5,X2,X6,X10)))&perp(X7,X6,X2,X4))&coll(X7,X2,X4))&perp(X8,X6,X2,X3))&coll(X8,X2,X3))&(?[X11]:circle(X5,X6,X9,X11)))&coll(X9,X6,X8))&~para(X8,X7,X9,X4)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 54.99/55.17 fof(c15,negated_conjecture,((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0009))&perp(skolem0006,skolem0005,skolem0001,skolem0003))&coll(skolem0006,skolem0001,skolem0003))&perp(skolem0007,skolem0005,skolem0001,skolem0002))&coll(skolem0007,skolem0001,skolem0002))&circle(skolem0004,skolem0005,skolem0008,skolem0010))&coll(skolem0008,skolem0005,skolem0007))&~para(skolem0007,skolem0006,skolem0008,skolem0003)),inference(skolemize,[status(esa)],[c14])).
% 54.99/55.17 cnf(c24,negated_conjecture,~para(skolem0007,skolem0006,skolem0008,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 54.99/55.17 fof(c402,plain,(![X523]:(![X524]:(![X525]:(![X526]:((~coll(X523,X524,X525)|~coll(X523,X524,X526))|coll(X525,X526,X523)))))),inference(variable_rename,[status(thm)],[c401])).
% 54.99/55.17 cnf(c403,plain,~coll(X747,X746,X745)|~coll(X747,X746,X744)|coll(X745,X744,X747),inference(split_conjunct,[status(thm)],[c402])).
% 54.99/55.17 cnf(c519,plain,~coll(X748,X750,X749)|coll(X749,X749,X748),inference(factor,[status(thm)],[c403])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 54.99/55.17 fof(c191,plain,(![X166]:(![X167]:(![X168]:(~para(X166,X167,X166,X168)|coll(X166,X167,X168))))),inference(variable_rename,[status(thm)],[c190])).
% 54.99/55.17 cnf(c192,plain,~para(X656,X655,X656,X654)|coll(X656,X655,X654),inference(split_conjunct,[status(thm)],[c191])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c287,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])).
% 54.99/55.17 fof(c288,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)],[c287])).
% 54.99/55.17 fof(c290,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(c289,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)],[c288])).])).
% 54.99/55.17 cnf(c291,plain,~eqangle(X1088,X1090,X1091,X1092,X1089,X1093,X1091,X1092)|para(X1088,X1090,X1089,X1093),inference(split_conjunct,[status(thm)],[c290])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c351,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])).
% 54.99/55.17 fof(c352,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)],[c351])).
% 54.99/55.17 cnf(c353,plain,~eqangle(X1227,X1226,X1232,X1228,X1230,X1231,X1233,X1229)|eqangle(X1232,X1228,X1227,X1226,X1233,X1229,X1230,X1231),inference(split_conjunct,[status(thm)],[c352])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c282,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])).
% 54.99/55.17 fof(c283,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)],[c282])).
% 54.99/55.17 fof(c285,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(c284,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)],[c283])).])).
% 54.99/55.17 cnf(c286,plain,~para(X1082,X1083,X1086,X1087)|eqangle(X1082,X1083,X1084,X1085,X1086,X1087,X1084,X1085),inference(split_conjunct,[status(thm)],[c285])).
% 54.99/55.17 cnf(c20,negated_conjecture,perp(skolem0007,skolem0005,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 54.99/55.17 fof(c387,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X503,X504,X501,X502)))))),inference(variable_rename,[status(thm)],[c386])).
% 54.99/55.17 cnf(c388,plain,~perp(X691,X690,X692,X689)|perp(X692,X689,X691,X690),inference(split_conjunct,[status(thm)],[c387])).
% 54.99/55.17 cnf(c473,plain,perp(skolem0001,skolem0002,skolem0007,skolem0005),inference(resolution,[status(thm)],[c388, c20])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c383,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])).
% 54.99/55.17 fof(c384,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)],[c383])).
% 54.99/55.17 cnf(c385,plain,~perp(X1262,X1263,X1264,X1267)|~perp(X1264,X1267,X1266,X1265)|para(X1262,X1263,X1266,X1265),inference(split_conjunct,[status(thm)],[c384])).
% 54.99/55.17 cnf(c1513,plain,~perp(X2657,X2656,skolem0001,skolem0002)|para(X2657,X2656,skolem0007,skolem0005),inference(resolution,[status(thm)],[c385, c473])).
% 54.99/55.17 cnf(c5780,plain,para(skolem0007,skolem0005,skolem0007,skolem0005),inference(resolution,[status(thm)],[c1513, c20])).
% 54.99/55.17 cnf(c5818,plain,eqangle(skolem0007,skolem0005,X3589,X3588,skolem0007,skolem0005,X3589,X3588),inference(resolution,[status(thm)],[c5780, c286])).
% 54.99/55.17 cnf(c7846,plain,eqangle(X3673,X3674,skolem0007,skolem0005,X3673,X3674,skolem0007,skolem0005),inference(resolution,[status(thm)],[c5818, c353])).
% 54.99/55.17 cnf(c8141,plain,para(X3676,X3675,X3676,X3675),inference(resolution,[status(thm)],[c7846, c291])).
% 54.99/55.17 cnf(c8186,plain,coll(X3678,X3677,X3677),inference(resolution,[status(thm)],[c8141, c192])).
% 54.99/55.17 cnf(c8283,plain,coll(X3683,X3683,X3684),inference(resolution,[status(thm)],[c8186, c519])).
% 54.99/55.17 cnf(c8604,plain,~coll(X5213,X5213,X5212)|coll(X5212,X5211,X5213),inference(resolution,[status(thm)],[c8283, c403])).
% 54.99/55.17 cnf(c15969,plain,coll(X5221,X5220,X5219),inference(resolution,[status(thm)],[c8604, c8283])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c187,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 54.99/55.17 fof(c188,plain,(![X163]:(![X164]:(![X165]:((~cong(X163,X164,X163,X165)|~coll(X163,X164,X165))|midp(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c187])).
% 54.99/55.17 cnf(c189,plain,~cong(X936,X938,X936,X937)|~coll(X936,X938,X937)|midp(X936,X938,X937),inference(split_conjunct,[status(thm)],[c188])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 54.99/55.17 fof(c340,plain,(![X412]:(![X413]:(![X414]:(![X415]:(~cong(X412,X413,X414,X415)|cong(X412,X413,X415,X414)))))),inference(variable_rename,[status(thm)],[c339])).
% 54.99/55.17 cnf(c341,plain,~cong(X662,X663,X664,X661)|cong(X662,X663,X661,X664),inference(split_conjunct,[status(thm)],[c340])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 54.99/55.17 fof(c337,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X410,X411,X408,X409)))))),inference(variable_rename,[status(thm)],[c336])).
% 54.99/55.17 cnf(c338,plain,~cong(X660,X659,X658,X657)|cong(X658,X657,X660,X659),inference(split_conjunct,[status(thm)],[c337])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c196,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])).
% 54.99/55.17 fof(c197,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)],[c196])).
% 54.99/55.17 cnf(c198,plain,~midp(X947,X945,X948)|~para(X945,X946,X948,X944)|~para(X945,X944,X948,X946)|midp(X947,X946,X944),inference(split_conjunct,[status(thm)],[c197])).
% 54.99/55.17 cnf(c1022,plain,~midp(X2073,X2072,X2071)|~para(X2072,X2070,X2071,X2070)|midp(X2073,X2070,X2070),inference(factor,[status(thm)],[c198])).
% 54.99/55.17 cnf(c8171,plain,~midp(X4981,X4982,X4982)|midp(X4981,X4980,X4980),inference(resolution,[status(thm)],[c8141, c1022])).
% 54.99/55.17 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 54.99/55.17 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 54.99/55.17 fof(c367,plain,(![X473]:(![X474]:(![X475]:(![X476]:(~cyclic(X473,X474,X475,X476)|cyclic(X473,X474,X476,X475)))))),inference(variable_rename,[status(thm)],[c366])).
% 54.99/55.17 cnf(c368,plain,~cyclic(X686,X688,X687,X685)|cyclic(X686,X688,X685,X687),inference(split_conjunct,[status(thm)],[c367])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 54.99/55.17 fof(c364,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X471,X470,X472)))))),inference(variable_rename,[status(thm)],[c363])).
% 54.99/55.17 cnf(c365,plain,~cyclic(X671,X670,X672,X669)|cyclic(X671,X672,X670,X669),inference(split_conjunct,[status(thm)],[c364])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c272,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])).
% 54.99/55.17 fof(c273,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)],[c272])).
% 54.99/55.17 cnf(c274,plain,~eqangle(X1070,X1073,X1070,X1071,X1072,X1073,X1072,X1071)|~coll(X1070,X1072,X1071)|cyclic(X1073,X1071,X1070,X1072),inference(split_conjunct,[status(thm)],[c273])).
% 54.99/55.17 cnf(c8192,plain,eqangle(X4992,X4993,X4995,X4994,X4992,X4993,X4995,X4994),inference(resolution,[status(thm)],[c8141, c286])).
% 54.99/55.17 cnf(c15793,plain,~coll(X5608,X5608,X5609)|cyclic(X5607,X5609,X5608,X5608),inference(resolution,[status(thm)],[c8192, c274])).
% 54.99/55.17 cnf(c16805,plain,cyclic(X5615,X5614,X5613,X5613),inference(resolution,[status(thm)],[c15793, c15969])).
% 54.99/55.17 cnf(c16808,plain,cyclic(X5624,X5622,X5623,X5622),inference(resolution,[status(thm)],[c16805, c365])).
% 54.99/55.17 cnf(c16815,plain,cyclic(X5633,X5631,X5631,X5632),inference(resolution,[status(thm)],[c16808, c368])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c267,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])).
% 54.99/55.17 fof(c268,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)],[c267])).
% 54.99/55.17 fof(c270,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(c269,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)],[c268])).])).
% 54.99/55.17 cnf(c271,plain,~cyclic(X1065,X1066,X1064,X1069)|~cyclic(X1065,X1066,X1064,X1067)|~cyclic(X1065,X1066,X1064,X1068)|~eqangle(X1064,X1065,X1064,X1066,X1068,X1069,X1068,X1067)|cong(X1065,X1066,X1069,X1067),inference(split_conjunct,[status(thm)],[c270])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c345,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])).
% 54.99/55.17 fof(c346,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)],[c345])).
% 54.99/55.17 cnf(c347,plain,~eqangle(X1212,X1217,X1211,X1215,X1214,X1216,X1210,X1213)|eqangle(X1212,X1217,X1214,X1216,X1211,X1215,X1210,X1213),inference(split_conjunct,[status(thm)],[c346])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 54.99/55.17 fof(c399,plain,(![X519]:(![X520]:(![X521]:(![X522]:(~para(X519,X520,X521,X522)|para(X519,X520,X522,X521)))))),inference(variable_rename,[status(thm)],[c398])).
% 54.99/55.17 cnf(c400,plain,~para(X736,X737,X735,X734)|para(X736,X737,X734,X735),inference(split_conjunct,[status(thm)],[c399])).
% 54.99/55.17 cnf(c8179,plain,para(X3700,X3701,X3701,X3700),inference(resolution,[status(thm)],[c8141, c400])).
% 54.99/55.17 cnf(c9382,plain,eqangle(X5374,X5373,X5376,X5375,X5373,X5374,X5376,X5375),inference(resolution,[status(thm)],[c8179, c286])).
% 54.99/55.17 cnf(c16371,plain,eqangle(X5417,X5418,X5420,X5419,X5417,X5418,X5419,X5420),inference(resolution,[status(thm)],[c9382, c353])).
% 54.99/55.17 cnf(c16445,plain,eqangle(X5471,X5470,X5471,X5470,X5468,X5469,X5469,X5468),inference(resolution,[status(thm)],[c16371, c347])).
% 54.99/55.17 cnf(c16531,plain,~cyclic(X6656,X6656,X6654,X6655)|cong(X6656,X6656,X6655,X6655),inference(resolution,[status(thm)],[c16445, c271])).
% 54.99/55.17 cnf(c17423,plain,cong(X6657,X6657,X6658,X6658),inference(resolution,[status(thm)],[c16531, c16815])).
% 54.99/55.17 cnf(c17444,plain,~coll(X6724,X6724,X6724)|midp(X6724,X6724,X6724),inference(resolution,[status(thm)],[c17423, c189])).
% 54.99/55.17 cnf(c17563,plain,midp(X6725,X6725,X6725),inference(resolution,[status(thm)],[c17444, c15969])).
% 54.99/55.17 cnf(c17684,plain,midp(X6728,X6727,X6727),inference(resolution,[status(thm)],[c17563, c8171])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c239,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])).
% 54.99/55.17 fof(c240,plain,(![X234]:(![X235]:(![X236]:(![X237]:((~perp(X234,X235,X235,X236)|~midp(X237,X234,X236))|cong(X234,X237,X235,X237)))))),inference(variable_rename,[status(thm)],[c239])).
% 54.99/55.17 cnf(c241,plain,~perp(X1018,X1017,X1017,X1016)|~midp(X1015,X1018,X1016)|cong(X1018,X1015,X1017,X1015),inference(split_conjunct,[status(thm)],[c240])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c160,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])).
% 54.99/55.17 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(shift_quantors,[status(thm)],[c160])).
% 54.99/55.17 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(shift_quantors,[status(thm)],[fof(c162,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)],[c161])).])).
% 54.99/55.17 cnf(c164,plain,~eqangle(X909,X907,X906,X912,X908,X913,X911,X910)|~perp(X908,X913,X911,X910)|perp(X909,X907,X906,X912),inference(split_conjunct,[status(thm)],[c163])).
% 54.99/55.17 cnf(c16372,plain,eqangle(X5425,X5426,X5426,X5425,X5424,X5423,X5424,X5423),inference(resolution,[status(thm)],[c9382, c347])).
% 54.99/55.17 cnf(c16451,plain,~perp(X6588,X6586,X6588,X6586)|perp(X6589,X6587,X6587,X6589),inference(resolution,[status(thm)],[c16372, c164])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c225,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])).
% 54.99/55.17 fof(c226,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)],[c225])).
% 54.99/55.17 cnf(c227,plain,~cong(X991,X993,X992,X993)|~cong(X991,X994,X992,X994)|perp(X991,X992,X993,X994),inference(split_conjunct,[status(thm)],[c226])).
% 54.99/55.17 cnf(c1043,plain,~cong(X996,X995,X997,X995)|perp(X996,X997,X995,X995),inference(factor,[status(thm)],[c227])).
% 54.99/55.17 cnf(c17441,plain,perp(X6673,X6673,X6673,X6673),inference(resolution,[status(thm)],[c17423, c1043])).
% 54.99/55.17 cnf(c17461,plain,perp(X6683,X6682,X6682,X6683),inference(resolution,[status(thm)],[c17441, c16451])).
% 54.99/55.17 cnf(c17488,plain,~midp(X7704,X7706,X7706)|cong(X7706,X7704,X7705,X7704),inference(resolution,[status(thm)],[c17461, c241])).
% 54.99/55.17 cnf(c19809,plain,cong(X7709,X7707,X7708,X7707),inference(resolution,[status(thm)],[c17488, c17684])).
% 54.99/55.17 cnf(c19810,plain,cong(X7710,X7711,X7711,X7712),inference(resolution,[status(thm)],[c19809, c341])).
% 54.99/55.17 cnf(c19845,plain,cong(X7735,X7734,X7736,X7735),inference(resolution,[status(thm)],[c19810, c338])).
% 54.99/55.17 cnf(c19873,plain,cong(X7752,X7754,X7752,X7753),inference(resolution,[status(thm)],[c19845, c341])).
% 54.99/55.17 cnf(c19944,plain,~coll(X8074,X8072,X8073)|midp(X8074,X8072,X8073),inference(resolution,[status(thm)],[c19873, c189])).
% 54.99/55.17 cnf(c21197,plain,midp(X8077,X8076,X8075),inference(resolution,[status(thm)],[c19944, c15969])).
% 54.99/55.17 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)).
% 54.99/55.17 fof(c264,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])).
% 54.99/55.17 fof(c265,plain,(![X269]:(![X270]:(![X271]:(![X272]:(![X273]:((~midp(X272,X269,X270)|~midp(X273,X269,X271))|para(X272,X273,X270,X271))))))),inference(variable_rename,[status(thm)],[c264])).
% 54.99/55.17 cnf(c266,plain,~midp(X1059,X1062,X1061)|~midp(X1060,X1062,X1063)|para(X1059,X1060,X1061,X1063),inference(split_conjunct,[status(thm)],[c265])).
% 54.99/55.17 cnf(c17867,plain,~midp(X11885,X11884,X11882)|para(X11885,X11883,X11882,X11884),inference(resolution,[status(thm)],[c17684, c266])).
% 54.99/55.17 cnf(c24411,plain,para(X11886,X11889,X11888,X11887),inference(resolution,[status(thm)],[c17867, c21197])).
% 54.99/55.17 cnf(c24423,plain,$false,inference(resolution,[status(thm)],[c24411, c24])).
% 54.99/55.17 % SZS output end CNFRefutation
% 54.99/55.17
% 54.99/55.17 % Initial clauses : 136
% 54.99/55.17 % Processed clauses : 2900
% 54.99/55.17 % Factors computed : 165
% 54.99/55.17 % Resolvents computed: 23861
% 54.99/55.17 % Tautologies deleted: 12
% 54.99/55.17 % Forward subsumed : 7916
% 54.99/55.17 % Backward subsumed : 2462
% 54.99/55.17 % -------- CPU Time ---------
% 54.99/55.17 % User time : 54.752 s
% 54.99/55.17 % System time : 0.058 s
% 54.99/55.17 % Total time : 54.810 s
%------------------------------------------------------------------------------