%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO641+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:28 EDT 2024
% Result : Theorem 166.80s 167.01s
% Output : Refutation 166.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GEO641+1 : TPTP v8.1.2. Released v7.5.0.
% 0.13/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:03:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 166.80/167.01 % Version: 1.5
% 166.80/167.01 % SZS status Theorem
% 166.80/167.01 % SZS output start CNFRefutation
% 166.80/167.01 fof(exemplo6GDDFULL81109107,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![U]:(![V]:(![NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))=>para(U,V,B,C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL81109107)).
% 166.80/167.01 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![U]:(![V]:(![NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))=>para(U,V,B,C))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL81109107])).
% 166.80/167.01 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[U]:(?[V]:(?[NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))&~para(U,V,B,C)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 166.80/167.01 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[U]:(?[V]:((((((((circle(O,A,B,C)&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))&~para(U,V,B,C))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 166.80/167.01 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((circle(X5,X2,X3,X4)&(?[X9]:circle(X5,X2,X6,X9)))&perp(X2,X3,X6,X7))&perp(X2,X6,X3,X7))&perp(X3,X6,X2,X7))&perp(X2,X4,X6,X8))&perp(X2,X6,X4,X8))&perp(X4,X6,X2,X8))&~para(X7,X8,X3,X4))))))))),inference(variable_rename,[status(thm)],[c13])).
% 166.80/167.01 fof(c15,negated_conjecture,((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0008))&perp(skolem0001,skolem0002,skolem0005,skolem0006))&perp(skolem0001,skolem0005,skolem0002,skolem0006))&perp(skolem0002,skolem0005,skolem0001,skolem0006))&perp(skolem0001,skolem0003,skolem0005,skolem0007))&perp(skolem0001,skolem0005,skolem0003,skolem0007))&perp(skolem0003,skolem0005,skolem0001,skolem0007))&~para(skolem0006,skolem0007,skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c14])).
% 166.80/167.01 cnf(c24,negated_conjecture,~para(skolem0006,skolem0007,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c226,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cong(X216,X218,X217,X218)|~cong(X216,X219,X217,X219))|perp(X216,X217,X218,X219)))))),inference(variable_rename,[status(thm)],[c225])).
% 166.80/167.01 cnf(c227,plain,~cong(X912,X914,X913,X914)|~cong(X912,X915,X913,X915)|perp(X912,X913,X914,X915),inference(split_conjunct,[status(thm)],[c226])).
% 166.80/167.01 cnf(c815,plain,~cong(X916,X918,X917,X918)|perp(X916,X917,X918,X918),inference(factor,[status(thm)],[c227])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c240,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c239])).
% 166.80/167.01 cnf(c241,plain,~perp(X889,X891,X891,X890)|~midp(X892,X889,X890)|cong(X889,X892,X891,X892),inference(split_conjunct,[status(thm)],[c240])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c163,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))|perp(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))))))|perp(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c161])).])).
% 166.80/167.01 cnf(c164,plain,~eqangle(X1167,X1166,X1165,X1163,X1160,X1164,X1162,X1161)|~perp(X1160,X1164,X1162,X1161)|perp(X1167,X1166,X1165,X1163),inference(split_conjunct,[status(thm)],[c163])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c346,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X426,X427,X430,X431,X428,X429,X432,X433)))))))))),inference(variable_rename,[status(thm)],[c345])).
% 166.80/167.01 cnf(c347,plain,~eqangle(X1374,X1379,X1377,X1378,X1375,X1373,X1376,X1380)|eqangle(X1374,X1379,X1375,X1373,X1377,X1378,X1376,X1380),inference(split_conjunct,[status(thm)],[c346])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c285,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c284,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c283])).])).
% 166.80/167.01 cnf(c286,plain,~para(X819,X823,X824,X822)|eqangle(X819,X823,X820,X821,X824,X822,X820,X821),inference(split_conjunct,[status(thm)],[c285])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 166.80/167.01 fof(c399,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c398])).
% 166.80/167.01 cnf(c400,plain,~para(X761,X762,X759,X760)|para(X761,X762,X760,X759),inference(split_conjunct,[status(thm)],[c399])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c290,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c289,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c288])).])).
% 166.80/167.01 cnf(c291,plain,~eqangle(X827,X828,X829,X826,X825,X830,X829,X826)|para(X827,X828,X825,X830),inference(split_conjunct,[status(thm)],[c290])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 166.80/167.01 fof(c387,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c386])).
% 166.80/167.01 cnf(c388,plain,~perp(X609,X610,X608,X607)|perp(X608,X607,X609,X610),inference(split_conjunct,[status(thm)],[c387])).
% 166.80/167.01 cnf(c19,negated_conjecture,perp(skolem0001,skolem0005,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 166.80/167.01 fof(c390,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c389])).
% 166.80/167.01 cnf(c391,plain,~perp(X629,X630,X627,X628)|perp(X629,X630,X628,X627),inference(split_conjunct,[status(thm)],[c390])).
% 166.80/167.01 cnf(c447,plain,perp(skolem0001,skolem0005,skolem0006,skolem0002),inference(resolution,[status(thm)],[c391, c19])).
% 166.80/167.01 cnf(c477,plain,perp(skolem0006,skolem0002,skolem0001,skolem0005),inference(resolution,[status(thm)],[c447, c388])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c384,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c383])).
% 166.80/167.01 cnf(c385,plain,~perp(X1115,X1119,X1118,X1117)|~perp(X1118,X1117,X1116,X1114)|para(X1115,X1119,X1116,X1114),inference(split_conjunct,[status(thm)],[c384])).
% 166.80/167.01 cnf(c874,plain,~perp(X1122,X1123,skolem0001,skolem0005)|para(X1122,X1123,skolem0006,skolem0002),inference(resolution,[status(thm)],[c385, c447])).
% 166.80/167.01 cnf(c923,plain,para(skolem0006,skolem0002,skolem0006,skolem0002),inference(resolution,[status(thm)],[c874, c477])).
% 166.80/167.01 cnf(c946,plain,eqangle(skolem0006,skolem0002,X1208,X1209,skolem0006,skolem0002,X1208,X1209),inference(resolution,[status(thm)],[c923, c286])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c352,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 166.80/167.01 cnf(c353,plain,~eqangle(X1394,X1390,X1391,X1389,X1395,X1393,X1392,X1396)|eqangle(X1391,X1389,X1394,X1390,X1392,X1396,X1395,X1393),inference(split_conjunct,[status(thm)],[c352])).
% 166.80/167.01 cnf(c1448,plain,eqangle(X1585,X1586,skolem0006,skolem0002,X1585,X1586,skolem0006,skolem0002),inference(resolution,[status(thm)],[c353, c946])).
% 166.80/167.01 cnf(c1785,plain,para(X1587,X1588,X1587,X1588),inference(resolution,[status(thm)],[c1448, c291])).
% 166.80/167.01 cnf(c1792,plain,para(X1614,X1613,X1613,X1614),inference(resolution,[status(thm)],[c1785, c400])).
% 166.80/167.01 cnf(c1959,plain,eqangle(X1838,X1837,X1836,X1839,X1837,X1838,X1836,X1839),inference(resolution,[status(thm)],[c1792, c286])).
% 166.80/167.01 cnf(c2210,plain,eqangle(X1861,X1863,X1863,X1861,X1862,X1860,X1862,X1860),inference(resolution,[status(thm)],[c1959, c347])).
% 166.80/167.01 cnf(c2236,plain,~perp(X2627,X2626,X2627,X2626)|perp(X2624,X2625,X2625,X2624),inference(resolution,[status(thm)],[c2210, c164])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 166.80/167.01 fof(c364,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c363])).
% 166.80/167.01 cnf(c365,plain,~cyclic(X596,X593,X595,X594)|cyclic(X596,X595,X593,X594),inference(split_conjunct,[status(thm)],[c364])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c402,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c401])).
% 166.80/167.01 cnf(c403,plain,~coll(X776,X778,X777)|~coll(X776,X778,X775)|coll(X777,X775,X776),inference(split_conjunct,[status(thm)],[c402])).
% 166.80/167.01 cnf(c564,plain,~coll(X781,X780,X779)|coll(X779,X779,X781),inference(factor,[status(thm)],[c403])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 166.80/167.01 fof(c191,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c190])).
% 166.80/167.01 cnf(c192,plain,~para(X571,X570,X571,X572)|coll(X571,X570,X572),inference(split_conjunct,[status(thm)],[c191])).
% 166.80/167.01 cnf(c1797,plain,coll(X1594,X1593,X1593),inference(resolution,[status(thm)],[c1785, c192])).
% 166.80/167.01 cnf(c1859,plain,coll(X1595,X1595,X1596),inference(resolution,[status(thm)],[c1797, c564])).
% 166.80/167.01 cnf(c1889,plain,~coll(X1812,X1812,X1813)|coll(X1813,X1811,X1812),inference(resolution,[status(thm)],[c1859, c403])).
% 166.80/167.01 cnf(c2193,plain,coll(X1815,X1814,X1816),inference(resolution,[status(thm)],[c1889, c1859])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c273,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c272])).
% 166.80/167.01 cnf(c274,plain,~eqangle(X1292,X1293,X1292,X1291,X1294,X1293,X1294,X1291)|~coll(X1292,X1294,X1291)|cyclic(X1293,X1291,X1292,X1294),inference(split_conjunct,[status(thm)],[c273])).
% 166.80/167.01 cnf(c1836,plain,eqangle(X1771,X1772,X1770,X1773,X1771,X1772,X1770,X1773),inference(resolution,[status(thm)],[c1785, c286])).
% 166.80/167.01 cnf(c2112,plain,~coll(X1983,X1983,X1985)|cyclic(X1984,X1985,X1983,X1983),inference(resolution,[status(thm)],[c1836, c274])).
% 166.80/167.01 cnf(c2305,plain,cyclic(X1987,X1988,X1986,X1986),inference(resolution,[status(thm)],[c2112, c2193])).
% 166.80/167.01 cnf(c2313,plain,cyclic(X1997,X1995,X1996,X1995),inference(resolution,[status(thm)],[c2305, c365])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c270,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276))|cong(X272,X273,X275,X276)))))))),inference(shift_quantors,[status(thm)],[fof(c269,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((![X277]:(((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276)))|cong(X272,X273,X275,X276))))))),inference(variable_rename,[status(thm)],[c268])).])).
% 166.80/167.01 cnf(c271,plain,~cyclic(X1284,X1288,X1286,X1283)|~cyclic(X1284,X1288,X1286,X1285)|~cyclic(X1284,X1288,X1286,X1287)|~eqangle(X1286,X1284,X1286,X1288,X1287,X1283,X1287,X1285)|cong(X1284,X1288,X1283,X1285),inference(split_conjunct,[status(thm)],[c270])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c348,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])).
% 166.80/167.01 fof(c349,plain,(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(~eqangle(X434,X435,X436,X437,X438,X439,X440,X441)|eqangle(X438,X439,X440,X441,X434,X435,X436,X437)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 166.80/167.01 cnf(c350,plain,~eqangle(X1384,X1388,X1385,X1387,X1382,X1381,X1386,X1383)|eqangle(X1382,X1381,X1386,X1383,X1384,X1388,X1385,X1387),inference(split_conjunct,[status(thm)],[c349])).
% 166.80/167.01 cnf(c2241,plain,eqangle(X1904,X1905,X1904,X1905,X1906,X1907,X1907,X1906),inference(resolution,[status(thm)],[c2210, c350])).
% 166.80/167.01 cnf(c2265,plain,~cyclic(X2651,X2651,X2653,X2652)|cong(X2651,X2651,X2652,X2652),inference(resolution,[status(thm)],[c2241, c271])).
% 166.80/167.01 cnf(c2901,plain,cong(X2654,X2654,X2654,X2654),inference(resolution,[status(thm)],[c2265, c2313])).
% 166.80/167.01 cnf(c2919,plain,perp(X2667,X2667,X2667,X2667),inference(resolution,[status(thm)],[c2901, c815])).
% 166.80/167.01 cnf(c2944,plain,perp(X2676,X2677,X2677,X2676),inference(resolution,[status(thm)],[c2919, c2236])).
% 166.80/167.01 cnf(c2981,plain,~midp(X2858,X2859,X2859)|cong(X2859,X2858,X2857,X2858),inference(resolution,[status(thm)],[c2944, c241])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c188,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c187])).
% 166.80/167.01 cnf(c189,plain,~cong(X784,X782,X784,X783)|~coll(X784,X782,X783)|midp(X784,X782,X783),inference(split_conjunct,[status(thm)],[c188])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 166.80/167.01 fof(c340,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c339])).
% 166.80/167.01 cnf(c341,plain,~cong(X587,X588,X586,X585)|cong(X587,X588,X585,X586),inference(split_conjunct,[status(thm)],[c340])).
% 166.80/167.01 cnf(c2916,plain,~coll(X2702,X2702,X2702)|midp(X2702,X2702,X2702),inference(resolution,[status(thm)],[c2901, c189])).
% 166.80/167.01 cnf(c3015,plain,midp(X2703,X2703,X2703),inference(resolution,[status(thm)],[c2916, c2193])).
% 166.80/167.01 cnf(c3677,plain,cong(X2860,X2860,X2861,X2860),inference(resolution,[status(thm)],[c2981, c3015])).
% 166.80/167.01 cnf(c3688,plain,cong(X2865,X2865,X2865,X2866),inference(resolution,[status(thm)],[c3677, c341])).
% 166.80/167.01 cnf(c3713,plain,~coll(X2947,X2947,X2946)|midp(X2947,X2947,X2946),inference(resolution,[status(thm)],[c3688, c189])).
% 166.80/167.01 cnf(c3968,plain,midp(X2948,X2948,X2949),inference(resolution,[status(thm)],[c3713, c2193])).
% 166.80/167.01 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)).
% 166.80/167.01 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 166.80/167.01 fof(c396,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c395])).
% 166.80/167.01 cnf(c397,plain,~para(X755,X757,X756,X758)|para(X756,X758,X755,X757),inference(split_conjunct,[status(thm)],[c396])).
% 166.80/167.01 fof(ruleD46,axiom,(![A]:(![B]:(![O]:(cong(O,A,O,B)=>eqangle(O,A,A,B,A,B,O,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD46)).
% 166.80/167.01 fof(c258,plain,(![A]:(![B]:(![O]:(~cong(O,A,O,B)|eqangle(O,A,A,B,A,B,O,B))))),inference(fof_nnf,[status(thm)],[ruleD46])).
% 166.80/167.01 fof(c259,plain,(![X259]:(![X260]:(![X261]:(~cong(X261,X259,X261,X260)|eqangle(X261,X259,X259,X260,X259,X260,X261,X260))))),inference(variable_rename,[status(thm)],[c258])).
% 166.80/167.01 cnf(c260,plain,~cong(X797,X798,X797,X799)|eqangle(X797,X798,X798,X799,X798,X799,X797,X799),inference(split_conjunct,[status(thm)],[c259])).
% 166.80/167.01 cnf(c3708,plain,eqangle(X2918,X2918,X2918,X2919,X2918,X2919,X2918,X2919),inference(resolution,[status(thm)],[c3688, c260])).
% 166.80/167.01 cnf(c3823,plain,para(X2920,X2920,X2920,X2921),inference(resolution,[status(thm)],[c3708, c291])).
% 166.80/167.01 cnf(c3829,plain,para(X2923,X2923,X2922,X2923),inference(resolution,[status(thm)],[c3823, c400])).
% 166.80/167.01 cnf(c3915,plain,para(X2933,X2932,X2932,X2932),inference(resolution,[status(thm)],[c3829, c397])).
% 166.80/167.01 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)).
% 166.80/167.01 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])).
% 166.80/167.01 fof(c197,plain,(![X172]:(![X173]:(![X174]:(![X175]:(![X176]:(((~midp(X176,X172,X173)|~para(X172,X174,X173,X175))|~para(X172,X175,X173,X174))|midp(X176,X174,X175))))))),inference(variable_rename,[status(thm)],[c196])).
% 166.80/167.01 cnf(c198,plain,~midp(X1195,X1196,X1198)|~para(X1196,X1197,X1198,X1199)|~para(X1196,X1199,X1198,X1197)|midp(X1195,X1197,X1199),inference(split_conjunct,[status(thm)],[c197])).
% 166.80/167.01 cnf(c1121,plain,~midp(X4025,X4024,X4026)|~para(X4024,X4023,X4026,X4023)|midp(X4025,X4023,X4023),inference(factor,[status(thm)],[c198])).
% 166.80/167.01 cnf(c8158,plain,~midp(X4458,X4457,X4456)|midp(X4458,X4456,X4456),inference(resolution,[status(thm)],[c1121, c3915])).
% 166.80/167.01 cnf(c9337,plain,midp(X4460,X4461,X4461),inference(resolution,[status(thm)],[c8158, c3968])).
% 166.80/167.01 cnf(c9344,plain,cong(X4469,X4470,X4468,X4470),inference(resolution,[status(thm)],[c9337, c2981])).
% 166.80/167.01 cnf(c9377,plain,perp(X4489,X4490,X4488,X4488),inference(resolution,[status(thm)],[c9344, c815])).
% 166.80/167.01 cnf(c3690,plain,perp(X2867,X2868,X2867,X2867),inference(resolution,[status(thm)],[c3677, c815])).
% 166.80/167.01 cnf(c3734,plain,perp(X2888,X2888,X2888,X2887),inference(resolution,[status(thm)],[c3690, c388])).
% 166.80/167.01 cnf(c3770,plain,~perp(X15921,X15923,X15924,X15924)|para(X15921,X15923,X15924,X15922),inference(resolution,[status(thm)],[c3734, c385])).
% 166.80/167.01 cnf(c36527,plain,para(X15940,X15938,X15937,X15939),inference(resolution,[status(thm)],[c3770, c9377])).
% 166.80/167.01 cnf(c36584,plain,$false,inference(resolution,[status(thm)],[c36527, c24])).
% 166.80/167.01 % SZS output end CNFRefutation
% 166.80/167.01
% 166.80/167.01 % Initial clauses : 136
% 166.80/167.01 % Processed clauses : 2353
% 166.80/167.01 % Factors computed : 568
% 166.80/167.01 % Resolvents computed: 35676
% 166.80/167.01 % Tautologies deleted: 42
% 166.80/167.01 % Forward subsumed : 10019
% 166.80/167.01 % Backward subsumed : 1423
% 166.80/167.01 % -------- CPU Time ---------
% 166.80/167.01 % User time : 166.537 s
% 166.80/167.01 % System time : 0.089 s
% 166.80/167.01 % Total time : 166.626 s
%------------------------------------------------------------------------------