%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO554+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:16 EDT 2024
% Result : Theorem 25.98s 26.18s
% Output : Refutation 25.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO554+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n013.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 08:04:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 25.98/26.18 % Version: 1.5
% 25.98/26.18 % SZS status Theorem
% 25.98/26.18 % SZS output start CNFRefutation
% 25.98/26.18 fof(exemplo6GDDFULL012014,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:((((((((((perp(C,A,C,B)&circle(A,C,NWPNT1,NWPNT2))&circle(B,C,NWPNT3,NWPNT4))&circle(A,C,D,NWPNT5))&coll(C,D,E))&circle(B,C,E,NWPNT6))&coll(B,E,F))&circle(B,C,F,NWPNT7))&circle(A,C,G,NWPNT8))&circle(B,C,G,NWPNT9))=>coll(D,F,G)))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL012014)).
% 25.98/26.18 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:((((((((((perp(C,A,C,B)&circle(A,C,NWPNT1,NWPNT2))&circle(B,C,NWPNT3,NWPNT4))&circle(A,C,D,NWPNT5))&coll(C,D,E))&circle(B,C,E,NWPNT6))&coll(B,E,F))&circle(B,C,F,NWPNT7))&circle(A,C,G,NWPNT8))&circle(B,C,G,NWPNT9))=>coll(D,F,G))))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012014])).
% 25.98/26.18 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:(?[NWPNT7]:(?[NWPNT8]:(?[NWPNT9]:((((((((((perp(C,A,C,B)&circle(A,C,NWPNT1,NWPNT2))&circle(B,C,NWPNT3,NWPNT4))&circle(A,C,D,NWPNT5))&coll(C,D,E))&circle(B,C,E,NWPNT6))&coll(B,E,F))&circle(B,C,F,NWPNT7))&circle(A,C,G,NWPNT8))&circle(B,C,G,NWPNT9))&~coll(D,F,G)))))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 25.98/26.18 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((((((((perp(C,A,C,B)&(?[NWPNT1]:(?[NWPNT2]:circle(A,C,NWPNT1,NWPNT2))))&(?[NWPNT3]:(?[NWPNT4]:circle(B,C,NWPNT3,NWPNT4))))&(?[NWPNT5]:circle(A,C,D,NWPNT5)))&coll(C,D,E))&(?[NWPNT6]:circle(B,C,E,NWPNT6)))&coll(B,E,F))&(?[NWPNT7]:circle(B,C,F,NWPNT7)))&(?[NWPNT8]:circle(A,C,G,NWPNT8)))&(?[NWPNT9]:circle(B,C,G,NWPNT9)))&~coll(D,F,G))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 25.98/26.18 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((((perp(X4,X2,X4,X3)&(?[X9]:(?[X10]:circle(X2,X4,X9,X10))))&(?[X11]:(?[X12]:circle(X3,X4,X11,X12))))&(?[X13]:circle(X2,X4,X5,X13)))&coll(X4,X5,X6))&(?[X14]:circle(X3,X4,X6,X14)))&coll(X3,X6,X7))&(?[X15]:circle(X3,X4,X7,X15)))&(?[X16]:circle(X2,X4,X8,X16)))&(?[X17]:circle(X3,X4,X8,X17)))&~coll(X5,X7,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 25.98/26.18 fof(c15,negated_conjecture,((((((((((perp(skolem0003,skolem0001,skolem0003,skolem0002)&circle(skolem0001,skolem0003,skolem0008,skolem0009))&circle(skolem0002,skolem0003,skolem0010,skolem0011))&circle(skolem0001,skolem0003,skolem0004,skolem0012))&coll(skolem0003,skolem0004,skolem0005))&circle(skolem0002,skolem0003,skolem0005,skolem0013))&coll(skolem0002,skolem0005,skolem0006))&circle(skolem0002,skolem0003,skolem0006,skolem0014))&circle(skolem0001,skolem0003,skolem0007,skolem0015))&circle(skolem0002,skolem0003,skolem0007,skolem0016))&~coll(skolem0004,skolem0006,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 25.98/26.18 cnf(c26,negated_conjecture,~coll(skolem0004,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 25.98/26.18 fof(ruleD1,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(A,C,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD1)).
% 25.98/26.18 fof(c409,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(A,C,B))))),inference(fof_nnf,[status(thm)],[ruleD1])).
% 25.98/26.18 fof(c410,plain,(![X536]:(![X537]:(![X538]:(~coll(X536,X537,X538)|coll(X536,X538,X537))))),inference(variable_rename,[status(thm)],[c409])).
% 25.98/26.18 cnf(c411,plain,~coll(X581,X582,X580)|coll(X581,X580,X582),inference(split_conjunct,[status(thm)],[c410])).
% 25.98/26.18 fof(ruleD2,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD2)).
% 25.98/26.18 fof(c406,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD2])).
% 25.98/26.18 fof(c407,plain,(![X533]:(![X534]:(![X535]:(~coll(X533,X534,X535)|coll(X534,X533,X535))))),inference(variable_rename,[status(thm)],[c406])).
% 25.98/26.18 cnf(c408,plain,~coll(X570,X571,X569)|coll(X571,X570,X569),inference(split_conjunct,[status(thm)],[c407])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c403,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 25.98/26.18 fof(c404,plain,(![X529]:(![X530]:(![X531]:(![X532]:((~coll(X529,X530,X531)|~coll(X529,X530,X532))|coll(X531,X532,X529)))))),inference(variable_rename,[status(thm)],[c403])).
% 25.98/26.18 cnf(c405,plain,~coll(X730,X731,X729)|~coll(X730,X731,X732)|coll(X729,X732,X730),inference(split_conjunct,[status(thm)],[c404])).
% 25.98/26.18 cnf(c482,plain,~coll(X733,X735,X734)|coll(X734,X734,X733),inference(factor,[status(thm)],[c405])).
% 25.98/26.18 cnf(c20,negated_conjecture,coll(skolem0003,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 25.98/26.18 cnf(c418,plain,coll(skolem0004,skolem0003,skolem0005),inference(resolution,[status(thm)],[c408, c20])).
% 25.98/26.18 cnf(c505,plain,coll(skolem0005,skolem0005,skolem0004),inference(resolution,[status(thm)],[c482, c418])).
% 25.98/26.18 cnf(c22,negated_conjecture,coll(skolem0002,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 25.98/26.18 cnf(c424,plain,coll(skolem0002,skolem0006,skolem0005),inference(resolution,[status(thm)],[c411, c22])).
% 25.98/26.18 cnf(c429,plain,coll(skolem0006,skolem0002,skolem0005),inference(resolution,[status(thm)],[c424, c408])).
% 25.98/26.18 cnf(c499,plain,coll(skolem0005,skolem0005,skolem0006),inference(resolution,[status(thm)],[c482, c429])).
% 25.98/26.18 cnf(c532,plain,~coll(skolem0005,skolem0005,X952)|coll(X952,skolem0006,skolem0005),inference(resolution,[status(thm)],[c499, c405])).
% 25.98/26.18 cnf(c884,plain,coll(skolem0004,skolem0006,skolem0005),inference(resolution,[status(thm)],[c532, c505])).
% 25.98/26.18 cnf(c893,plain,coll(skolem0004,skolem0005,skolem0006),inference(resolution,[status(thm)],[c884, c411])).
% 25.98/26.18 cnf(c907,plain,coll(skolem0006,skolem0006,skolem0004),inference(resolution,[status(thm)],[c893, c482])).
% 25.98/26.18 cnf(c936,plain,~coll(skolem0006,skolem0006,X1484)|coll(X1484,skolem0004,skolem0006),inference(resolution,[status(thm)],[c907, c405])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c192,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 25.98/26.18 fof(c193,plain,(![X172]:(![X173]:(![X174]:(~para(X172,X173,X172,X174)|coll(X172,X173,X174))))),inference(variable_rename,[status(thm)],[c192])).
% 25.98/26.18 cnf(c194,plain,~para(X633,X632,X633,X634)|coll(X633,X632,X634),inference(split_conjunct,[status(thm)],[c193])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c289,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])).
% 25.98/26.18 fof(c290,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)],[c289])).
% 25.98/26.18 fof(c292,plain,(![X304]:(![X305]:(![X306]:(![X307]:(![X308]:(![X309]:(~eqangle(X304,X305,X308,X309,X306,X307,X308,X309)|para(X304,X305,X306,X307)))))))),inference(shift_quantors,[status(thm)],[fof(c291,plain,(![X304]:(![X305]:(![X306]:(![X307]:((![X308]:(![X309]:~eqangle(X304,X305,X308,X309,X306,X307,X308,X309)))|para(X304,X305,X306,X307)))))),inference(variable_rename,[status(thm)],[c290])).])).
% 25.98/26.18 cnf(c293,plain,~eqangle(X1087,X1089,X1086,X1090,X1088,X1085,X1086,X1090)|para(X1087,X1089,X1088,X1085),inference(split_conjunct,[status(thm)],[c292])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c353,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])).
% 25.98/26.18 fof(c354,plain,(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(~eqangle(X450,X451,X452,X453,X454,X455,X456,X457)|eqangle(X452,X453,X450,X451,X456,X457,X454,X455)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 25.98/26.18 cnf(c355,plain,~eqangle(X1227,X1226,X1228,X1225,X1230,X1223,X1224,X1229)|eqangle(X1228,X1225,X1227,X1226,X1224,X1229,X1230,X1223),inference(split_conjunct,[status(thm)],[c354])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c284,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])).
% 25.98/26.18 fof(c285,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)],[c284])).
% 25.98/26.18 fof(c287,plain,(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(~para(X298,X299,X300,X301)|eqangle(X298,X299,X302,X303,X300,X301,X302,X303)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X298]:(![X299]:(![X300]:(![X301]:(~para(X298,X299,X300,X301)|(![X302]:(![X303]:eqangle(X298,X299,X302,X303,X300,X301,X302,X303)))))))),inference(variable_rename,[status(thm)],[c285])).])).
% 25.98/26.18 cnf(c288,plain,~para(X1080,X1079,X1083,X1081)|eqangle(X1080,X1079,X1082,X1084,X1083,X1081,X1082,X1084),inference(split_conjunct,[status(thm)],[c287])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 25.98/26.18 fof(c389,plain,(![X507]:(![X508]:(![X509]:(![X510]:(~perp(X507,X508,X509,X510)|perp(X509,X510,X507,X508)))))),inference(variable_rename,[status(thm)],[c388])).
% 25.98/26.18 cnf(c390,plain,~perp(X672,X673,X671,X674)|perp(X671,X674,X672,X673),inference(split_conjunct,[status(thm)],[c389])).
% 25.98/26.18 cnf(c16,negated_conjecture,perp(skolem0003,skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 25.98/26.18 fof(c392,plain,(![X511]:(![X512]:(![X513]:(![X514]:(~perp(X511,X512,X513,X514)|perp(X511,X512,X514,X513)))))),inference(variable_rename,[status(thm)],[c391])).
% 25.98/26.18 cnf(c393,plain,~perp(X678,X675,X677,X676)|perp(X678,X675,X676,X677),inference(split_conjunct,[status(thm)],[c392])).
% 25.98/26.18 cnf(c463,plain,perp(skolem0003,skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c393, c16])).
% 25.98/26.18 cnf(c467,plain,perp(skolem0002,skolem0003,skolem0003,skolem0001),inference(resolution,[status(thm)],[c463, c390])).
% 25.98/26.18 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)).
% 25.98/26.18 fof(c385,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])).
% 25.98/26.18 fof(c386,plain,(![X501]:(![X502]:(![X503]:(![X504]:(![X505]:(![X506]:((~perp(X501,X502,X503,X504)|~perp(X503,X504,X505,X506))|para(X501,X502,X505,X506)))))))),inference(variable_rename,[status(thm)],[c385])).
% 25.98/26.18 cnf(c387,plain,~perp(X1281,X1280,X1278,X1282)|~perp(X1278,X1282,X1279,X1283)|para(X1281,X1280,X1279,X1283),inference(split_conjunct,[status(thm)],[c386])).
% 25.98/26.18 cnf(c1407,plain,~perp(X2572,X2573,skolem0003,skolem0001)|para(X2572,X2573,skolem0002,skolem0003),inference(resolution,[status(thm)],[c387, c463])).
% 25.98/26.18 cnf(c5955,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1407, c467])).
% 25.98/26.18 cnf(c5987,plain,eqangle(skolem0002,skolem0003,X2751,X2750,skolem0002,skolem0003,X2751,X2750),inference(resolution,[status(thm)],[c5955, c288])).
% 25.98/26.18 cnf(c7960,plain,eqangle(X2953,X2954,skolem0002,skolem0003,X2953,X2954,skolem0002,skolem0003),inference(resolution,[status(thm)],[c5987, c355])).
% 25.98/26.18 cnf(c10906,plain,para(X2955,X2956,X2955,X2956),inference(resolution,[status(thm)],[c7960, c293])).
% 25.98/26.18 cnf(c10925,plain,coll(X2957,X2958,X2958),inference(resolution,[status(thm)],[c10906, c194])).
% 25.98/26.18 cnf(c11043,plain,coll(X2963,X2963,X2964),inference(resolution,[status(thm)],[c10925, c482])).
% 25.98/26.18 cnf(c11661,plain,coll(X3022,skolem0004,skolem0006),inference(resolution,[status(thm)],[c11043, c936])).
% 25.98/26.18 cnf(c12741,plain,coll(skolem0004,X3091,skolem0006),inference(resolution,[status(thm)],[c11661, c408])).
% 25.98/26.18 cnf(c13744,plain,coll(skolem0004,skolem0006,X3167),inference(resolution,[status(thm)],[c12741, c411])).
% 25.98/26.18 cnf(c14702,plain,$false,inference(resolution,[status(thm)],[c13744, c26])).
% 25.98/26.18 % SZS output end CNFRefutation
% 25.98/26.18
% 25.98/26.18 % Initial clauses : 138
% 25.98/26.18 % Processed clauses : 1807
% 25.98/26.18 % Factors computed : 112
% 25.98/26.18 % Resolvents computed: 14234
% 25.98/26.18 % Tautologies deleted: 8
% 25.98/26.18 % Forward subsumed : 2577
% 25.98/26.18 % Backward subsumed : 1005
% 25.98/26.18 % -------- CPU Time ---------
% 25.98/26.18 % User time : 25.794 s
% 25.98/26.18 % System time : 0.037 s
% 25.98/26.18 % Total time : 25.831 s
%------------------------------------------------------------------------------