%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO541+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:14 EDT 2024
% Result : Theorem 70.74s 70.91s
% Output : Refutation 70.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GEO541+1 : TPTP v8.1.2. Released v7.5.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n002.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:25:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 70.74/70.91 % Version: 1.5
% 70.74/70.91 % SZS status Theorem
% 70.74/70.91 % SZS output start CNFRefutation
% 70.74/70.91 fof(exemplo6GDDFULL012001,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&midp(F,C,B))&midp(G,D,E))=>perp(F,G,D,E))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL012001)).
% 70.74/70.91 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&midp(F,C,B))&midp(G,D,E))=>perp(F,G,D,E)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012001])).
% 70.74/70.91 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&midp(F,C,B))&midp(G,D,E))&~perp(F,G,D,E))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 70.74/70.91 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((perp(X5,X4,X2,X3)&coll(X5,X2,X3))&perp(X6,X3,X2,X4))&coll(X6,X2,X4))&midp(X7,X4,X3))&midp(X8,X5,X6))&~perp(X7,X8,X5,X6))))))))),inference(variable_rename,[status(thm)],[c12])).
% 70.74/70.91 fof(c14,negated_conjecture,((((((perp(skolem0004,skolem0003,skolem0001,skolem0002)&coll(skolem0004,skolem0001,skolem0002))&perp(skolem0005,skolem0002,skolem0001,skolem0003))&coll(skolem0005,skolem0001,skolem0003))&midp(skolem0006,skolem0003,skolem0002))&midp(skolem0007,skolem0004,skolem0005))&~perp(skolem0006,skolem0007,skolem0004,skolem0005)),inference(skolemize,[status(esa)],[c13])).
% 70.74/70.91 cnf(c21,negated_conjecture,~perp(skolem0006,skolem0007,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 70.74/70.91 fof(c384,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c383])).
% 70.74/70.91 cnf(c385,plain,~perp(X742,X740,X743,X741)|perp(X743,X741,X742,X740),inference(split_conjunct,[status(thm)],[c384])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 70.74/70.91 fof(c337,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c336])).
% 70.74/70.91 cnf(c338,plain,~cong(X689,X691,X690,X688)|cong(X689,X691,X688,X690),inference(split_conjunct,[status(thm)],[c337])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 70.74/70.91 fof(c334,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c333])).
% 70.74/70.91 cnf(c335,plain,~cong(X684,X683,X681,X682)|cong(X681,X682,X684,X683),inference(split_conjunct,[status(thm)],[c334])).
% 70.74/70.91 cnf(c20,negated_conjecture,midp(skolem0007,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 70.74/70.91 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 70.74/70.91 fof(c374,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 70.74/70.91 fof(c375,plain,(![X483]:(![X484]:(![X485]:(~midp(X485,X484,X483)|midp(X485,X483,X484))))),inference(variable_rename,[status(thm)],[c374])).
% 70.74/70.91 cnf(c376,plain,~midp(X559,X558,X557)|midp(X559,X557,X558),inference(split_conjunct,[status(thm)],[c375])).
% 70.74/70.91 cnf(c416,plain,midp(skolem0007,skolem0005,skolem0004),inference(resolution,[status(thm)],[c376, c20])).
% 70.74/70.91 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 70.74/70.91 fof(c181,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 70.74/70.91 fof(c182,plain,(![X157]:(![X158]:(![X159]:(~midp(X157,X158,X159)|cong(X157,X158,X157,X159))))),inference(variable_rename,[status(thm)],[c181])).
% 70.74/70.91 cnf(c183,plain,~midp(X674,X673,X672)|cong(X674,X673,X674,X672),inference(split_conjunct,[status(thm)],[c182])).
% 70.74/70.91 cnf(c496,plain,cong(skolem0007,skolem0005,skolem0007,skolem0004),inference(resolution,[status(thm)],[c183, c416])).
% 70.74/70.91 cnf(c510,plain,cong(skolem0007,skolem0005,skolem0004,skolem0007),inference(resolution,[status(thm)],[c338, c496])).
% 70.74/70.91 cnf(c521,plain,cong(skolem0004,skolem0007,skolem0007,skolem0005),inference(resolution,[status(thm)],[c510, c335])).
% 70.74/70.91 cnf(c531,plain,cong(skolem0004,skolem0007,skolem0005,skolem0007),inference(resolution,[status(thm)],[c521, c338])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c222,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])).
% 70.74/70.91 fof(c223,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)],[c222])).
% 70.74/70.91 cnf(c224,plain,~cong(X979,X980,X981,X980)|~cong(X979,X982,X981,X982)|perp(X979,X981,X980,X982),inference(split_conjunct,[status(thm)],[c223])).
% 70.74/70.91 cnf(c1272,plain,~cong(X1114,X1113,X1115,X1113)|perp(X1114,X1115,X1113,X1113),inference(factor,[status(thm)],[c224])).
% 70.74/70.91 cnf(c1470,plain,perp(skolem0004,skolem0005,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1272, c531])).
% 70.74/70.91 cnf(c1490,plain,perp(skolem0007,skolem0007,skolem0004,skolem0005),inference(resolution,[status(thm)],[c1470, c385])).
% 70.74/70.91 fof(ruleD10,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&perp(C,D,E,F))=>perp(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 70.74/70.91 fof(c377,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~perp(C,D,E,F))|perp(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD10])).
% 70.74/70.91 fof(c378,plain,(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:((~para(X486,X487,X488,X489)|~perp(X488,X489,X490,X491))|perp(X486,X487,X490,X491)))))))),inference(variable_rename,[status(thm)],[c377])).
% 70.74/70.91 cnf(c379,plain,~para(X1261,X1259,X1260,X1264)|~perp(X1260,X1264,X1263,X1262)|perp(X1261,X1259,X1263,X1262),inference(split_conjunct,[status(thm)],[c378])).
% 70.74/70.91 cnf(c1624,plain,~para(X2929,X2928,skolem0007,skolem0007)|perp(X2929,X2928,skolem0004,skolem0005),inference(resolution,[status(thm)],[c379, c1490])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c193,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])).
% 70.74/70.91 fof(c194,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)],[c193])).
% 70.74/70.91 cnf(c195,plain,~midp(X942,X945,X941)|~para(X945,X944,X941,X943)|~para(X945,X943,X941,X944)|midp(X942,X944,X943),inference(split_conjunct,[status(thm)],[c194])).
% 70.74/70.91 cnf(c1199,plain,~midp(X2394,X2392,X2391)|~para(X2392,X2393,X2391,X2393)|midp(X2394,X2393,X2393),inference(factor,[status(thm)],[c195])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 70.74/70.91 fof(c387,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X502,X503,X505,X504)))))),inference(variable_rename,[status(thm)],[c386])).
% 70.74/70.91 cnf(c388,plain,~perp(X750,X752,X753,X751)|perp(X750,X752,X751,X753),inference(split_conjunct,[status(thm)],[c387])).
% 70.74/70.91 cnf(c17,negated_conjecture,perp(skolem0005,skolem0002,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 70.74/70.91 cnf(c559,plain,perp(skolem0001,skolem0003,skolem0005,skolem0002),inference(resolution,[status(thm)],[c385, c17])).
% 70.74/70.91 cnf(c573,plain,perp(skolem0001,skolem0003,skolem0002,skolem0005),inference(resolution,[status(thm)],[c388, c559])).
% 70.74/70.91 cnf(c583,plain,perp(skolem0002,skolem0005,skolem0001,skolem0003),inference(resolution,[status(thm)],[c573, c385])).
% 70.74/70.91 cnf(c602,plain,perp(skolem0002,skolem0005,skolem0003,skolem0001),inference(resolution,[status(thm)],[c583, c388])).
% 70.74/70.91 cnf(c570,plain,perp(skolem0005,skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c388, c17])).
% 70.74/70.91 cnf(c574,plain,perp(skolem0003,skolem0001,skolem0005,skolem0002),inference(resolution,[status(thm)],[c570, c385])).
% 70.74/70.91 cnf(c593,plain,perp(skolem0003,skolem0001,skolem0002,skolem0005),inference(resolution,[status(thm)],[c574, c388])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c380,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])).
% 70.74/70.91 fof(c381,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)],[c380])).
% 70.74/70.91 cnf(c382,plain,~perp(X1266,X1267,X1268,X1269)|~perp(X1268,X1269,X1270,X1271)|para(X1266,X1267,X1270,X1271),inference(split_conjunct,[status(thm)],[c381])).
% 70.74/70.91 cnf(c1660,plain,~perp(X2983,X2984,skolem0003,skolem0001)|para(X2983,X2984,skolem0002,skolem0005),inference(resolution,[status(thm)],[c382, c593])).
% 70.74/70.91 cnf(c8262,plain,para(skolem0002,skolem0005,skolem0002,skolem0005),inference(resolution,[status(thm)],[c1660, c602])).
% 70.74/70.91 cnf(c8301,plain,~midp(X3827,skolem0002,skolem0002)|midp(X3827,skolem0005,skolem0005),inference(resolution,[status(thm)],[c8262, c1199])).
% 70.74/70.91 cnf(c19,negated_conjecture,midp(skolem0006,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 70.74/70.91 cnf(c417,plain,midp(skolem0006,skolem0002,skolem0003),inference(resolution,[status(thm)],[c376, c19])).
% 70.74/70.91 cnf(c499,plain,cong(skolem0006,skolem0003,skolem0006,skolem0002),inference(resolution,[status(thm)],[c183, c19])).
% 70.74/70.91 cnf(c511,plain,cong(skolem0006,skolem0003,skolem0002,skolem0006),inference(resolution,[status(thm)],[c338, c499])).
% 70.74/70.91 cnf(c524,plain,cong(skolem0002,skolem0006,skolem0006,skolem0003),inference(resolution,[status(thm)],[c511, c335])).
% 70.74/70.91 cnf(c534,plain,cong(skolem0002,skolem0006,skolem0003,skolem0006),inference(resolution,[status(thm)],[c524, c338])).
% 70.74/70.91 cnf(c498,plain,cong(skolem0006,skolem0002,skolem0006,skolem0003),inference(resolution,[status(thm)],[c183, c417])).
% 70.74/70.91 cnf(c509,plain,cong(skolem0006,skolem0002,skolem0003,skolem0006),inference(resolution,[status(thm)],[c338, c498])).
% 70.74/70.91 cnf(c518,plain,cong(skolem0003,skolem0006,skolem0006,skolem0002),inference(resolution,[status(thm)],[c509, c335])).
% 70.74/70.91 cnf(c528,plain,cong(skolem0003,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c518, c338])).
% 70.74/70.91 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 70.74/70.91 fof(c330,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 70.74/70.91 fof(c331,plain,(![X399]:(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:((~cong(X399,X400,X401,X402)|~cong(X401,X402,X403,X404))|cong(X399,X400,X403,X404)))))))),inference(variable_rename,[status(thm)],[c330])).
% 70.74/70.91 cnf(c332,plain,~cong(X1178,X1176,X1177,X1180)|~cong(X1177,X1180,X1179,X1181)|cong(X1178,X1176,X1179,X1181),inference(split_conjunct,[status(thm)],[c331])).
% 70.74/70.91 cnf(c1551,plain,~cong(X2852,X2853,skolem0003,skolem0006)|cong(X2852,X2853,skolem0002,skolem0006),inference(resolution,[status(thm)],[c332, c528])).
% 70.74/70.91 cnf(c7091,plain,cong(skolem0002,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c1551, c534])).
% 70.74/70.91 cnf(c7141,plain,perp(skolem0002,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c7091, c1272])).
% 70.74/70.91 cnf(c1468,plain,perp(skolem0003,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1272, c528])).
% 70.74/70.91 cnf(c1474,plain,perp(skolem0006,skolem0006,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1468, c385])).
% 70.74/70.91 cnf(c1661,plain,~perp(X2985,X2986,skolem0006,skolem0006)|para(X2985,X2986,skolem0003,skolem0002),inference(resolution,[status(thm)],[c382, c1474])).
% 70.74/70.91 cnf(c8287,plain,para(skolem0002,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1661, c7141])).
% 70.74/70.91 cnf(c8366,plain,~midp(X3837,skolem0002,skolem0003)|midp(X3837,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8287, c1199])).
% 70.74/70.91 cnf(c11185,plain,midp(skolem0006,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8366, c417])).
% 70.74/70.91 cnf(c11206,plain,midp(skolem0006,skolem0005,skolem0005),inference(resolution,[status(thm)],[c11185, c8301])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c284,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])).
% 70.74/70.91 fof(c285,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)],[c284])).
% 70.74/70.91 fof(c287,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(c286,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)],[c285])).])).
% 70.74/70.91 cnf(c288,plain,~eqangle(X1064,X1060,X1059,X1062,X1061,X1063,X1059,X1062)|para(X1064,X1060,X1061,X1063),inference(split_conjunct,[status(thm)],[c287])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c348,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])).
% 70.74/70.91 fof(c349,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)],[c348])).
% 70.74/70.91 cnf(c350,plain,~eqangle(X1218,X1224,X1220,X1223,X1222,X1221,X1219,X1217)|eqangle(X1220,X1223,X1218,X1224,X1219,X1217,X1222,X1221),inference(split_conjunct,[status(thm)],[c349])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c279,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])).
% 70.74/70.91 fof(c280,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)],[c279])).
% 70.74/70.91 fof(c282,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(c281,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)],[c280])).])).
% 70.74/70.91 cnf(c283,plain,~para(X1058,X1053,X1054,X1056)|eqangle(X1058,X1053,X1057,X1055,X1054,X1056,X1057,X1055),inference(split_conjunct,[status(thm)],[c282])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 70.74/70.91 fof(c396,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c395])).
% 70.74/70.91 cnf(c397,plain,~para(X787,X784,X785,X786)|para(X787,X784,X786,X785),inference(split_conjunct,[status(thm)],[c396])).
% 70.74/70.91 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 70.74/70.91 fof(c196,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 70.74/70.91 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c196])).
% 70.74/70.91 fof(c199,plain,(![X176]:(![X177]:(![X178]:(![X179]:(![X180]:((~midp(X180,X176,X177)|~midp(X180,X178,X179))|para(X176,X178,X177,X179))))))),inference(shift_quantors,[status(thm)],[fof(c198,plain,(![X176]:(![X177]:(![X178]:(![X179]:((![X180]:(~midp(X180,X176,X177)|~midp(X180,X178,X179)))|para(X176,X178,X177,X179)))))),inference(variable_rename,[status(thm)],[c197])).])).
% 70.74/70.91 cnf(c200,plain,~midp(X947,X949,X950)|~midp(X947,X948,X946)|para(X949,X948,X950,X946),inference(split_conjunct,[status(thm)],[c199])).
% 70.74/70.91 cnf(c1213,plain,~midp(skolem0007,X2030,X2031)|para(X2030,skolem0005,X2031,skolem0004),inference(resolution,[status(thm)],[c200, c416])).
% 70.74/70.91 cnf(c4649,plain,para(skolem0004,skolem0005,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1213, c20])).
% 70.74/70.91 cnf(c4660,plain,para(skolem0004,skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c4649, c397])).
% 70.74/70.91 cnf(c4691,plain,eqangle(skolem0004,skolem0005,X3593,X3592,skolem0004,skolem0005,X3593,X3592),inference(resolution,[status(thm)],[c4660, c283])).
% 70.74/70.91 cnf(c10369,plain,eqangle(X4698,X4697,skolem0004,skolem0005,X4698,X4697,skolem0004,skolem0005),inference(resolution,[status(thm)],[c4691, c350])).
% 70.74/70.91 cnf(c17530,plain,para(X4699,X4700,X4699,X4700),inference(resolution,[status(thm)],[c10369, c288])).
% 70.74/70.91 cnf(c17566,plain,~midp(X6062,X6063,X6063)|midp(X6062,X6061,X6061),inference(resolution,[status(thm)],[c17530, c1199])).
% 70.74/70.91 cnf(c25744,plain,midp(skolem0006,X6070,X6070),inference(resolution,[status(thm)],[c17566, c11206])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c261,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])).
% 70.74/70.91 fof(c262,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c261])).
% 70.74/70.91 cnf(c263,plain,~midp(X1034,X1033,X1032)|~midp(X1031,X1033,X1030)|para(X1034,X1031,X1032,X1030),inference(split_conjunct,[status(thm)],[c262])).
% 70.74/70.91 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)).
% 70.74/70.91 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 70.74/70.91 fof(c393,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~para(X512,X513,X514,X515)|para(X514,X515,X512,X513)))))),inference(variable_rename,[status(thm)],[c392])).
% 70.74/70.91 cnf(c394,plain,~para(X779,X777,X776,X778)|para(X776,X778,X779,X777),inference(split_conjunct,[status(thm)],[c393])).
% 70.74/70.91 cnf(c4657,plain,para(skolem0005,skolem0004,skolem0004,skolem0005),inference(resolution,[status(thm)],[c4649, c394])).
% 70.74/70.91 cnf(c4676,plain,para(skolem0005,skolem0004,skolem0005,skolem0004),inference(resolution,[status(thm)],[c4657, c397])).
% 70.74/70.91 cnf(c5623,plain,~midp(X3787,skolem0005,skolem0005)|midp(X3787,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1199, c4676])).
% 70.74/70.91 cnf(c497,plain,cong(skolem0007,skolem0004,skolem0007,skolem0005),inference(resolution,[status(thm)],[c183, c20])).
% 70.74/70.91 cnf(c508,plain,cong(skolem0007,skolem0004,skolem0005,skolem0007),inference(resolution,[status(thm)],[c338, c497])).
% 70.74/70.91 cnf(c514,plain,cong(skolem0005,skolem0007,skolem0007,skolem0004),inference(resolution,[status(thm)],[c508, c335])).
% 70.74/70.91 cnf(c1560,plain,~cong(X2870,X2871,skolem0007,skolem0004)|cong(X2870,X2871,skolem0005,skolem0007),inference(resolution,[status(thm)],[c332, c508])).
% 70.74/70.91 cnf(c7263,plain,cong(skolem0005,skolem0007,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1560, c514])).
% 70.74/70.91 cnf(c7355,plain,perp(skolem0005,skolem0005,skolem0007,skolem0007),inference(resolution,[status(thm)],[c7263, c1272])).
% 70.74/70.91 cnf(c1664,plain,~perp(X2991,X2992,skolem0007,skolem0007)|para(X2991,X2992,skolem0004,skolem0005),inference(resolution,[status(thm)],[c382, c1490])).
% 70.74/70.91 cnf(c8355,plain,para(skolem0005,skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c1664, c7355])).
% 70.74/70.91 cnf(c8540,plain,~midp(X4338,skolem0005,skolem0004)|midp(X4338,skolem0005,skolem0005),inference(resolution,[status(thm)],[c8355, c1199])).
% 70.74/70.91 cnf(c15197,plain,midp(skolem0007,skolem0005,skolem0005),inference(resolution,[status(thm)],[c8540, c416])).
% 70.74/70.91 cnf(c15216,plain,midp(skolem0007,skolem0004,skolem0004),inference(resolution,[status(thm)],[c15197, c5623])).
% 70.74/70.91 cnf(c25741,plain,midp(skolem0007,X6067,X6067),inference(resolution,[status(thm)],[c17566, c15216])).
% 70.74/70.91 cnf(c25905,plain,~midp(X8083,X8082,X8081)|para(X8083,skolem0007,X8081,X8082),inference(resolution,[status(thm)],[c25741, c263])).
% 70.74/70.91 cnf(c29430,plain,para(skolem0006,skolem0007,X8085,X8085),inference(resolution,[status(thm)],[c25905, c25744])).
% 70.74/70.91 cnf(c29456,plain,perp(skolem0006,skolem0007,skolem0004,skolem0005),inference(resolution,[status(thm)],[c29430, c1624])).
% 70.74/70.91 cnf(c29537,plain,$false,inference(resolution,[status(thm)],[c29456, c21])).
% 70.74/70.91 % SZS output end CNFRefutation
% 70.74/70.91
% 70.74/70.91 % Initial clauses : 134
% 70.74/70.91 % Processed clauses : 3329
% 70.74/70.91 % Factors computed : 205
% 70.74/70.91 % Resolvents computed: 28928
% 70.74/70.91 % Tautologies deleted: 28
% 70.74/70.91 % Forward subsumed : 7405
% 70.74/70.91 % Backward subsumed : 1814
% 70.74/70.91 % -------- CPU Time ---------
% 70.74/70.91 % User time : 70.470 s
% 70.74/70.91 % System time : 0.070 s
% 70.74/70.91 % Total time : 70.540 s
%------------------------------------------------------------------------------