%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO660+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:31 EDT 2024
% Result : Theorem 48.84s 49.05s
% Output : Refutation 48.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO660+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 07:59:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 48.84/49.05 % Version: 1.5
% 48.84/49.05 % SZS status Theorem
% 48.84/49.05 % SZS output start CNFRefutation
% 48.84/49.05 fof(exemplo7Book00EE02E02319,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((((((perp(C,A,C,B)&perp(D,C,A,B))&coll(D,A,B))&coll(E,C,D))&coll(F,A,B))&eqangle(B,A,A,E,E,A,A,C))&eqangle(D,C,C,F,F,C,C,B))&coll(G,B,C))&coll(G,A,E))=>para(E,F,C,B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo7Book00EE02E02319)).
% 48.84/49.05 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((((((perp(C,A,C,B)&perp(D,C,A,B))&coll(D,A,B))&coll(E,C,D))&coll(F,A,B))&eqangle(B,A,A,E,E,A,A,C))&eqangle(D,C,C,F,F,C,C,B))&coll(G,B,C))&coll(G,A,E))=>para(E,F,C,B)))))))))),inference(assume_negation,[status(cth)],[exemplo7Book00EE02E02319])).
% 48.84/49.05 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(((((((((perp(C,A,C,B)&perp(D,C,A,B))&coll(D,A,B))&coll(E,C,D))&coll(F,A,B))&eqangle(B,A,A,E,E,A,A,C))&eqangle(D,C,C,F,F,C,C,B))&coll(G,B,C))&coll(G,A,E))&~para(E,F,C,B))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 48.84/49.05 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:((?[G]:((((((((perp(C,A,C,B)&perp(D,C,A,B))&coll(D,A,B))&coll(E,C,D))&coll(F,A,B))&eqangle(B,A,A,E,E,A,A,C))&eqangle(D,C,C,F,F,C,C,B))&coll(G,B,C))&coll(G,A,E)))&~para(E,F,C,B)))))))),inference(shift_quantors,[status(thm)],[c12])).
% 48.84/49.05 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((?[X8]:((((((((perp(X4,X2,X4,X3)&perp(X5,X4,X2,X3))&coll(X5,X2,X3))&coll(X6,X4,X5))&coll(X7,X2,X3))&eqangle(X3,X2,X2,X6,X6,X2,X2,X4))&eqangle(X5,X4,X4,X7,X7,X4,X4,X3))&coll(X8,X3,X4))&coll(X8,X2,X6)))&~para(X6,X7,X4,X3)))))))),inference(variable_rename,[status(thm)],[c13])).
% 48.84/49.05 fof(c15,negated_conjecture,(((((((((perp(skolem0003,skolem0001,skolem0003,skolem0002)&perp(skolem0004,skolem0003,skolem0001,skolem0002))&coll(skolem0004,skolem0001,skolem0002))&coll(skolem0005,skolem0003,skolem0004))&coll(skolem0006,skolem0001,skolem0002))&eqangle(skolem0002,skolem0001,skolem0001,skolem0005,skolem0005,skolem0001,skolem0001,skolem0003))&eqangle(skolem0004,skolem0003,skolem0003,skolem0006,skolem0006,skolem0003,skolem0003,skolem0002))&coll(skolem0007,skolem0002,skolem0003))&coll(skolem0007,skolem0001,skolem0005))&~para(skolem0005,skolem0006,skolem0003,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 48.84/49.05 cnf(c25,negated_conjecture,~para(skolem0005,skolem0006,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 48.84/49.05 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 48.84/49.05 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 48.84/49.05 fof(c403,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c402])).
% 48.84/49.05 cnf(c404,plain,~coll(X757,X758,X759)|~coll(X757,X758,X756)|coll(X759,X756,X757),inference(split_conjunct,[status(thm)],[c403])).
% 48.84/49.05 cnf(c566,plain,~coll(X760,X761,X762)|coll(X762,X762,X760),inference(factor,[status(thm)],[c404])).
% 48.84/49.05 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 48.84/49.05 fof(c191,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 48.84/49.05 fof(c192,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c191])).
% 48.84/49.05 cnf(c193,plain,~para(X671,X670,X671,X669)|coll(X671,X670,X669),inference(split_conjunct,[status(thm)],[c192])).
% 48.84/49.05 fof(ruleD39,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(eqangle(A,B,P,Q,C,D,P,Q)=>para(A,B,C,D)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 48.84/49.05 fof(c288,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 48.84/49.05 fof(c289,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c288])).
% 48.84/49.05 fof(c291,plain,(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)|para(X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c290,plain,(![X295]:(![X296]:(![X297]:(![X298]:((![X299]:(![X300]:~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)))|para(X295,X296,X297,X298)))))),inference(variable_rename,[status(thm)],[c289])).])).
% 48.84/49.05 cnf(c292,plain,~eqangle(X1063,X1060,X1062,X1061,X1064,X1059,X1062,X1061)|para(X1063,X1060,X1064,X1059),inference(split_conjunct,[status(thm)],[c291])).
% 48.84/49.05 fof(ruleD19,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(C,D,A,B,U,V,P,Q)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 48.84/49.05 fof(c352,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 48.84/49.05 fof(c353,plain,(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(~eqangle(X441,X442,X443,X444,X445,X446,X447,X448)|eqangle(X443,X444,X441,X442,X447,X448,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c352])).
% 48.84/49.05 cnf(c354,plain,~eqangle(X1214,X1220,X1213,X1218,X1215,X1219,X1217,X1216)|eqangle(X1213,X1218,X1214,X1220,X1217,X1216,X1215,X1219),inference(split_conjunct,[status(thm)],[c353])).
% 48.84/49.05 fof(ruleD40,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(para(A,B,C,D)=>eqangle(A,B,P,Q,C,D,P,Q)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 48.84/49.05 fof(c283,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 48.84/49.05 fof(c284,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c283])).
% 48.84/49.05 fof(c286,plain,(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(~para(X289,X290,X291,X292)|eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(shift_quantors,[status(thm)],[fof(c285,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~para(X289,X290,X291,X292)|(![X293]:(![X294]:eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(variable_rename,[status(thm)],[c284])).])).
% 48.84/49.05 cnf(c287,plain,~para(X1056,X1058,X1054,X1053)|eqangle(X1056,X1058,X1057,X1055,X1054,X1053,X1057,X1055),inference(split_conjunct,[status(thm)],[c286])).
% 48.84/49.05 cnf(c16,negated_conjecture,perp(skolem0003,skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 48.84/49.05 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 48.84/49.05 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 48.84/49.05 fof(c388,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c387])).
% 48.84/49.05 cnf(c389,plain,~perp(X701,X698,X700,X699)|perp(X700,X699,X701,X698),inference(split_conjunct,[status(thm)],[c388])).
% 48.84/49.05 cnf(c508,plain,perp(skolem0003,skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c389, c16])).
% 48.84/49.05 fof(ruleD9,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((perp(A,B,C,D)&perp(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 48.84/49.05 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 48.84/49.05 fof(c385,plain,(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:((~perp(X492,X493,X494,X495)|~perp(X494,X495,X496,X497))|para(X492,X493,X496,X497)))))))),inference(variable_rename,[status(thm)],[c384])).
% 48.84/49.05 cnf(c386,plain,~perp(X1268,X1267,X1265,X1264)|~perp(X1265,X1264,X1266,X1269)|para(X1268,X1267,X1266,X1269),inference(split_conjunct,[status(thm)],[c385])).
% 48.84/49.05 cnf(c1506,plain,~perp(X2721,X2720,skolem0003,skolem0002)|para(X2721,X2720,skolem0003,skolem0001),inference(resolution,[status(thm)],[c386, c508])).
% 48.84/49.05 cnf(c6199,plain,para(skolem0003,skolem0001,skolem0003,skolem0001),inference(resolution,[status(thm)],[c1506, c16])).
% 48.84/49.05 cnf(c6230,plain,eqangle(skolem0003,skolem0001,X3504,X3505,skolem0003,skolem0001,X3504,X3505),inference(resolution,[status(thm)],[c6199, c287])).
% 48.84/49.06 cnf(c8042,plain,eqangle(X3610,X3611,skolem0003,skolem0001,X3610,X3611,skolem0003,skolem0001),inference(resolution,[status(thm)],[c6230, c354])).
% 48.84/49.06 cnf(c8659,plain,para(X3613,X3612,X3613,X3612),inference(resolution,[status(thm)],[c8042, c292])).
% 48.84/49.06 cnf(c8667,plain,coll(X3614,X3615,X3615),inference(resolution,[status(thm)],[c8659, c193])).
% 48.84/49.06 cnf(c8871,plain,coll(X3624,X3624,X3625),inference(resolution,[status(thm)],[c8667, c566])).
% 48.84/49.06 cnf(c9669,plain,~coll(X4719,X4719,X4718)|coll(X4718,X4720,X4719),inference(resolution,[status(thm)],[c8871, c404])).
% 48.84/49.06 cnf(c17151,plain,coll(X4721,X4722,X4723),inference(resolution,[status(thm)],[c9669, c8871])).
% 48.84/49.06 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 48.84/49.06 fof(c188,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 48.84/49.06 fof(c189,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c188])).
% 48.84/49.06 cnf(c190,plain,~cong(X934,X933,X934,X935)|~coll(X934,X933,X935)|midp(X934,X933,X935),inference(split_conjunct,[status(thm)],[c189])).
% 48.84/49.06 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 48.84/49.06 fof(c340,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 48.84/49.06 fof(c341,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c340])).
% 48.84/49.06 cnf(c342,plain,~cong(X684,X683,X685,X682)|cong(X684,X683,X682,X685),inference(split_conjunct,[status(thm)],[c341])).
% 48.84/49.06 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 48.84/49.06 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 48.84/49.06 fof(c338,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c337])).
% 48.84/49.06 cnf(c339,plain,~cong(X675,X672,X673,X674)|cong(X673,X674,X675,X672),inference(split_conjunct,[status(thm)],[c338])).
% 48.84/49.06 fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)¶(A,C,B,D))¶(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 48.84/49.06 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 48.84/49.06 fof(c198,plain,(![X171]:(![X172]:(![X173]:(![X174]:(![X175]:(((~midp(X175,X171,X172)|~para(X171,X173,X172,X174))|~para(X171,X174,X172,X173))|midp(X175,X173,X174))))))),inference(variable_rename,[status(thm)],[c197])).
% 48.84/49.06 cnf(c199,plain,~midp(X942,X941,X943)|~para(X941,X945,X943,X944)|~para(X941,X944,X943,X945)|midp(X942,X945,X944),inference(split_conjunct,[status(thm)],[c198])).
% 48.84/49.06 cnf(c1249,plain,~midp(X2401,X2400,X2399)|~para(X2400,X2398,X2399,X2398)|midp(X2401,X2398,X2398),inference(factor,[status(thm)],[c199])).
% 48.84/49.06 cnf(c8675,plain,~midp(X4491,X4490,X4490)|midp(X4491,X4492,X4492),inference(resolution,[status(thm)],[c8659, c1249])).
% 48.84/49.06 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 48.84/49.06 fof(c273,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])).
% 48.84/49.06 fof(c274,plain,(![X277]:(![X278]:(![X279]:(![X280]:((~eqangle(X279,X277,X279,X278,X280,X277,X280,X278)|~coll(X279,X280,X278))|cyclic(X277,X278,X279,X280)))))),inference(variable_rename,[status(thm)],[c273])).
% 48.84/49.06 cnf(c275,plain,~eqangle(X1044,X1043,X1044,X1042,X1041,X1043,X1041,X1042)|~coll(X1044,X1041,X1042)|cyclic(X1043,X1042,X1044,X1041),inference(split_conjunct,[status(thm)],[c274])).
% 48.84/49.06 cnf(c8686,plain,eqangle(X4500,X4501,X4498,X4499,X4500,X4501,X4498,X4499),inference(resolution,[status(thm)],[c8659, c287])).
% 48.84/49.06 cnf(c16782,plain,~coll(X5078,X5078,X5077)|cyclic(X5079,X5077,X5078,X5078),inference(resolution,[status(thm)],[c8686, c275])).
% 48.84/49.06 cnf(c17693,plain,cyclic(X5081,X5082,X5080,X5080),inference(resolution,[status(thm)],[c16782, c17151])).
% 48.84/49.06 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 48.84/49.06 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(fof_nnf,[status(thm)],[ruleD43])).
% 48.84/49.06 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(shift_quantors,[status(thm)],[c268])).
% 48.84/49.06 fof(c271,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275))|cong(X271,X272,X274,X275)))))))),inference(shift_quantors,[status(thm)],[fof(c270,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((![X276]:(((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275)))|cong(X271,X272,X274,X275))))))),inference(variable_rename,[status(thm)],[c269])).])).
% 48.84/49.06 cnf(c272,plain,~cyclic(X1036,X1039,X1037,X1040)|~cyclic(X1036,X1039,X1037,X1038)|~cyclic(X1036,X1039,X1037,X1035)|~eqangle(X1037,X1036,X1037,X1039,X1035,X1040,X1035,X1038)|cong(X1036,X1039,X1040,X1038),inference(split_conjunct,[status(thm)],[c271])).
% 48.84/49.06 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 48.84/49.06 fof(c349,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])).
% 48.84/49.06 fof(c350,plain,(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(~eqangle(X433,X434,X435,X436,X437,X438,X439,X440)|eqangle(X437,X438,X439,X440,X433,X434,X435,X436)))))))))),inference(variable_rename,[status(thm)],[c349])).
% 48.84/49.06 cnf(c351,plain,~eqangle(X1212,X1209,X1205,X1206,X1208,X1211,X1210,X1207)|eqangle(X1208,X1211,X1210,X1207,X1212,X1209,X1205,X1206),inference(split_conjunct,[status(thm)],[c350])).
% 48.84/49.06 fof(ruleD21,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(A,B,P,Q,C,D,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 48.84/49.06 fof(c346,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 48.84/49.06 fof(c347,plain,(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(~eqangle(X425,X426,X427,X428,X429,X430,X431,X432)|eqangle(X425,X426,X429,X430,X427,X428,X431,X432)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 48.84/49.06 cnf(c348,plain,~eqangle(X1201,X1202,X1199,X1204,X1200,X1203,X1198,X1197)|eqangle(X1201,X1202,X1200,X1203,X1199,X1204,X1198,X1197),inference(split_conjunct,[status(thm)],[c347])).
% 48.84/49.06 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 48.84/49.06 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 48.84/49.06 fof(c400,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c399])).
% 48.84/49.06 cnf(c401,plain,~para(X740,X741,X742,X743)|para(X740,X741,X743,X742),inference(split_conjunct,[status(thm)],[c400])).
% 48.84/49.06 cnf(c8676,plain,para(X3640,X3641,X3641,X3640),inference(resolution,[status(thm)],[c8659, c401])).
% 48.84/49.06 cnf(c9867,plain,eqangle(X4866,X4865,X4863,X4864,X4865,X4866,X4863,X4864),inference(resolution,[status(thm)],[c8676, c287])).
% 48.84/49.06 cnf(c17573,plain,eqangle(X4895,X4897,X4897,X4895,X4896,X4894,X4896,X4894),inference(resolution,[status(thm)],[c9867, c348])).
% 48.84/49.06 cnf(c17614,plain,eqangle(X4930,X4931,X4930,X4931,X4933,X4932,X4932,X4933),inference(resolution,[status(thm)],[c17573, c351])).
% 48.84/49.06 cnf(c17648,plain,~cyclic(X6036,X6036,X6034,X6035)|cong(X6036,X6036,X6035,X6035),inference(resolution,[status(thm)],[c17614, c272])).
% 48.84/49.06 cnf(c18403,plain,cong(X6038,X6038,X6037,X6037),inference(resolution,[status(thm)],[c17648, c17693])).
% 48.84/49.06 cnf(c18427,plain,~coll(X6089,X6089,X6089)|midp(X6089,X6089,X6089),inference(resolution,[status(thm)],[c18403, c190])).
% 48.84/49.06 cnf(c18532,plain,midp(X6090,X6090,X6090),inference(resolution,[status(thm)],[c18427, c17151])).
% 48.84/49.06 cnf(c18534,plain,midp(X6094,X6093,X6093),inference(resolution,[status(thm)],[c18532, c8675])).
% 48.84/49.06 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 48.84/49.06 fof(c240,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 48.84/49.06 fof(c241,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c240])).
% 48.84/49.06 cnf(c242,plain,~perp(X996,X998,X998,X997)|~midp(X995,X996,X997)|cong(X996,X995,X998,X995),inference(split_conjunct,[status(thm)],[c241])).
% 48.84/49.06 fof(ruleD74,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)&perp(P,Q,U,V))=>perp(A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 48.84/49.06 fof(c161,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 48.84/49.06 fof(c162,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c161])).
% 48.84/49.06 fof(c164,plain,(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:((~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))|perp(X124,X125,X126,X127)))))))))),inference(shift_quantors,[status(thm)],[fof(c163,plain,(![X124]:(![X125]:(![X126]:(![X127]:((![X128]:(![X129]:(![X130]:(![X131]:(~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))))))|perp(X124,X125,X126,X127)))))),inference(variable_rename,[status(thm)],[c162])).])).
% 48.84/49.06 cnf(c165,plain,~eqangle(X904,X905,X908,X906,X910,X909,X903,X907)|~perp(X910,X909,X903,X907)|perp(X904,X905,X908,X906),inference(split_conjunct,[status(thm)],[c164])).
% 48.84/49.06 cnf(c17626,plain,~perp(X6014,X6012,X6014,X6012)|perp(X6013,X6015,X6015,X6013),inference(resolution,[status(thm)],[c17573, c165])).
% 48.84/49.06 fof(ruleD56,axiom,(![A]:(![B]:(![P]:(![Q]:((cong(A,P,B,P)&cong(A,Q,B,Q))=>perp(A,B,P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 48.84/49.06 fof(c226,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 48.84/49.06 fof(c227,plain,(![X215]:(![X216]:(![X217]:(![X218]:((~cong(X215,X217,X216,X217)|~cong(X215,X218,X216,X218))|perp(X215,X216,X217,X218)))))),inference(variable_rename,[status(thm)],[c226])).
% 48.84/49.06 cnf(c228,plain,~cong(X980,X979,X982,X979)|~cong(X980,X981,X982,X981)|perp(X980,X982,X979,X981),inference(split_conjunct,[status(thm)],[c227])).
% 48.84/49.06 cnf(c1294,plain,~cong(X1071,X1072,X1073,X1072)|perp(X1071,X1073,X1072,X1072),inference(factor,[status(thm)],[c228])).
% 48.84/49.06 cnf(c18410,plain,perp(X6051,X6051,X6051,X6051),inference(resolution,[status(thm)],[c18403, c1294])).
% 48.84/49.06 cnf(c18430,plain,perp(X6060,X6061,X6061,X6060),inference(resolution,[status(thm)],[c18410, c17626])).
% 48.84/49.06 cnf(c18474,plain,~midp(X6951,X6952,X6952)|cong(X6952,X6951,X6950,X6951),inference(resolution,[status(thm)],[c18430, c242])).
% 48.84/49.06 cnf(c20122,plain,cong(X6955,X6953,X6954,X6953),inference(resolution,[status(thm)],[c18474, c18534])).
% 48.84/49.06 cnf(c20136,plain,cong(X6965,X6964,X6964,X6966),inference(resolution,[status(thm)],[c20122, c342])).
% 48.84/49.06 cnf(c20174,plain,cong(X6987,X6988,X6989,X6987),inference(resolution,[status(thm)],[c20136, c339])).
% 48.84/49.06 cnf(c20230,plain,cong(X7004,X7005,X7004,X7006),inference(resolution,[status(thm)],[c20174, c342])).
% 48.84/49.06 cnf(c20254,plain,~coll(X7216,X7215,X7217)|midp(X7216,X7215,X7217),inference(resolution,[status(thm)],[c20230, c190])).
% 48.84/49.06 cnf(c20860,plain,midp(X7222,X7221,X7223),inference(resolution,[status(thm)],[c20254, c17151])).
% 48.84/49.06 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 48.84/49.06 fof(c265,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~midp(E,A,B)|~midp(F,A,C))|para(E,F,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD44])).
% 48.84/49.06 fof(c266,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c265])).
% 48.84/49.06 cnf(c267,plain,~midp(X1034,X1032,X1030)|~midp(X1033,X1032,X1031)|para(X1034,X1033,X1030,X1031),inference(split_conjunct,[status(thm)],[c266])).
% 48.84/49.06 cnf(c18557,plain,~midp(X10724,X10722,X10723)|para(X10724,X10725,X10723,X10722),inference(resolution,[status(thm)],[c18534, c267])).
% 48.84/49.06 cnf(c23713,plain,para(X10728,X10727,X10729,X10726),inference(resolution,[status(thm)],[c18557, c20860])).
% 48.84/49.06 cnf(c23720,plain,$false,inference(resolution,[status(thm)],[c23713, c25])).
% 48.84/49.06 % SZS output end CNFRefutation
% 48.84/49.06
% 48.84/49.06 % Initial clauses : 137
% 48.84/49.06 % Processed clauses : 2633
% 48.84/49.06 % Factors computed : 166
% 48.84/49.06 % Resolvents computed: 23158
% 48.84/49.06 % Tautologies deleted: 12
% 48.84/49.06 % Forward subsumed : 7519
% 48.84/49.06 % Backward subsumed : 2167
% 48.84/49.06 % -------- CPU Time ---------
% 48.84/49.06 % User time : 48.662 s
% 48.84/49.06 % System time : 0.051 s
% 48.84/49.06 % Total time : 48.713 s
%------------------------------------------------------------------------------