%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO603+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:23 EDT 2024
% Result : Theorem 6.64s 6.86s
% Output : Refutation 6.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO603+1 : TPTP v8.1.2. Released v7.5.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.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:09:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 6.64/6.86 % Version: 1.5
% 6.64/6.86 % SZS status Theorem
% 6.64/6.86 % SZS output start CNFRefutation
% 6.64/6.86 fof(exemplo6GDDFULL618065,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((circle(D,A,B,C)&coll(E,A,B))¶(B,C,F,E))&coll(F,A,C))&circle(G,A,E,F))=>coll(A,G,D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL618065)).
% 6.64/6.86 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((circle(D,A,B,C)&coll(E,A,B))¶(B,C,F,E))&coll(F,A,C))&circle(G,A,E,F))=>coll(A,G,D)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618065])).
% 6.64/6.86 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(((((circle(D,A,B,C)&coll(E,A,B))¶(B,C,F,E))&coll(F,A,C))&circle(G,A,E,F))&~coll(A,G,D))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 6.64/6.86 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((circle(X5,X2,X3,X4)&coll(X6,X2,X3))¶(X3,X4,X7,X6))&coll(X7,X2,X4))&circle(X8,X2,X6,X7))&~coll(X2,X8,X5))))))))),inference(variable_rename,[status(thm)],[c12])).
% 6.64/6.86 fof(c14,negated_conjecture,(((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0005,skolem0001,skolem0002))¶(skolem0002,skolem0003,skolem0006,skolem0005))&coll(skolem0006,skolem0001,skolem0003))&circle(skolem0007,skolem0001,skolem0005,skolem0006))&~coll(skolem0001,skolem0007,skolem0004)),inference(skolemize,[status(esa)],[c13])).
% 6.64/6.86 cnf(c20,negated_conjecture,~coll(skolem0001,skolem0007,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 6.64/6.86 fof(c398,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c397])).
% 6.64/6.86 cnf(c399,plain,~coll(X716,X715,X714)|~coll(X716,X715,X717)|coll(X714,X717,X716),inference(split_conjunct,[status(thm)],[c398])).
% 6.64/6.86 cnf(c479,plain,~coll(X720,X718,X719)|coll(X719,X719,X720),inference(factor,[status(thm)],[c399])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c186,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 6.64/6.86 fof(c187,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c186])).
% 6.64/6.86 cnf(c188,plain,~para(X609,X607,X609,X608)|coll(X609,X607,X608),inference(split_conjunct,[status(thm)],[c187])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c283,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])).
% 6.64/6.86 fof(c284,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)],[c283])).
% 6.64/6.86 fof(c286,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(c285,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)],[c284])).])).
% 6.64/6.86 cnf(c287,plain,~eqangle(X1075,X1074,X1078,X1079,X1076,X1077,X1078,X1079)|para(X1075,X1074,X1076,X1077),inference(split_conjunct,[status(thm)],[c286])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c347,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])).
% 6.64/6.86 fof(c348,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)],[c347])).
% 6.64/6.86 cnf(c349,plain,~eqangle(X1214,X1219,X1216,X1213,X1212,X1217,X1218,X1215)|eqangle(X1216,X1213,X1214,X1219,X1218,X1215,X1212,X1217),inference(split_conjunct,[status(thm)],[c348])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c278,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])).
% 6.64/6.86 fof(c279,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)],[c278])).
% 6.64/6.86 fof(c281,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(c280,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)],[c279])).])).
% 6.64/6.86 cnf(c282,plain,~para(X1068,X1072,X1073,X1069)|eqangle(X1068,X1072,X1070,X1071,X1073,X1069,X1070,X1071),inference(split_conjunct,[status(thm)],[c281])).
% 6.64/6.86 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)).
% 6.64/6.86 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 6.64/6.86 fof(c395,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c394])).
% 6.64/6.86 cnf(c396,plain,~para(X674,X676,X677,X675)|para(X674,X676,X675,X677),inference(split_conjunct,[status(thm)],[c395])).
% 6.64/6.86 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 6.64/6.86 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 6.64/6.86 fof(c392,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~para(X512,X513,X514,X515)|para(X514,X515,X512,X513)))))),inference(variable_rename,[status(thm)],[c391])).
% 6.64/6.86 cnf(c393,plain,~para(X657,X655,X656,X654)|para(X656,X654,X657,X655),inference(split_conjunct,[status(thm)],[c392])).
% 6.64/6.86 cnf(c17,negated_conjecture,para(skolem0002,skolem0003,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 6.64/6.86 cnf(c448,plain,para(skolem0006,skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c393, c17])).
% 6.64/6.86 cnf(c452,plain,para(skolem0006,skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c396, c448])).
% 6.64/6.86 cnf(c457,plain,para(skolem0003,skolem0002,skolem0006,skolem0005),inference(resolution,[status(thm)],[c452, c393])).
% 6.64/6.86 cnf(c462,plain,para(skolem0003,skolem0002,skolem0005,skolem0006),inference(resolution,[status(thm)],[c457, c396])).
% 6.64/6.86 cnf(c451,plain,para(skolem0002,skolem0003,skolem0005,skolem0006),inference(resolution,[status(thm)],[c396, c17])).
% 6.64/6.86 cnf(c454,plain,para(skolem0005,skolem0006,skolem0002,skolem0003),inference(resolution,[status(thm)],[c451, c393])).
% 6.64/6.86 cnf(c459,plain,para(skolem0005,skolem0006,skolem0003,skolem0002),inference(resolution,[status(thm)],[c454, c396])).
% 6.64/6.86 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 6.64/6.86 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD6])).
% 6.64/6.86 fof(c389,plain,(![X506]:(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:((~para(X506,X507,X508,X509)|~para(X508,X509,X510,X511))|para(X506,X507,X510,X511)))))))),inference(variable_rename,[status(thm)],[c388])).
% 6.64/6.86 cnf(c390,plain,~para(X1276,X1280,X1279,X1278)|~para(X1279,X1278,X1281,X1277)|para(X1276,X1280,X1281,X1277),inference(split_conjunct,[status(thm)],[c389])).
% 6.64/6.86 cnf(c1399,plain,~para(X2702,X2701,skolem0005,skolem0006)|para(X2702,X2701,skolem0003,skolem0002),inference(resolution,[status(thm)],[c390, c459])).
% 6.64/6.86 cnf(c3401,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1399, c462])).
% 6.64/6.86 cnf(c3423,plain,eqangle(skolem0003,skolem0002,X2712,X2711,skolem0003,skolem0002,X2712,X2711),inference(resolution,[status(thm)],[c3401, c282])).
% 6.64/6.86 cnf(c3503,plain,eqangle(X2727,X2728,skolem0003,skolem0002,X2727,X2728,skolem0003,skolem0002),inference(resolution,[status(thm)],[c3423, c349])).
% 6.64/6.86 cnf(c3558,plain,para(X2730,X2729,X2730,X2729),inference(resolution,[status(thm)],[c3503, c287])).
% 6.64/6.86 cnf(c3597,plain,coll(X2732,X2731,X2731),inference(resolution,[status(thm)],[c3558, c188])).
% 6.64/6.86 cnf(c3728,plain,coll(X2739,X2739,X2738),inference(resolution,[status(thm)],[c3597, c479])).
% 6.64/6.86 cnf(c3989,plain,~coll(X3337,X3337,X3338)|coll(X3338,X3339,X3337),inference(resolution,[status(thm)],[c3728, c399])).
% 6.64/6.86 cnf(c6199,plain,coll(X3344,X3342,X3343),inference(resolution,[status(thm)],[c3989, c3728])).
% 6.64/6.86 cnf(c6247,plain,$false,inference(resolution,[status(thm)],[c6199, c20])).
% 6.64/6.86 % SZS output end CNFRefutation
% 6.64/6.86
% 6.64/6.86 % Initial clauses : 133
% 6.64/6.86 % Processed clauses : 951
% 6.64/6.86 % Factors computed : 90
% 6.64/6.86 % Resolvents computed: 5867
% 6.64/6.86 % Tautologies deleted: 6
% 6.64/6.86 % Forward subsumed : 1746
% 6.64/6.86 % Backward subsumed : 582
% 6.64/6.86 % -------- CPU Time ---------
% 6.64/6.86 % User time : 6.486 s
% 6.64/6.86 % System time : 0.023 s
% 6.64/6.86 % Total time : 6.509 s
%------------------------------------------------------------------------------