%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO185+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:21:21 EDT 2024
% Result : Theorem 3.66s 3.83s
% Output : Refutation 3.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO185+3 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n024.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 08:33:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 3.66/3.83 % Version: 1.5
% 3.66/3.83 % SZS status Theorem
% 3.66/3.83 % SZS output start CNFRefutation
% 3.66/3.83 fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a3)).
% 3.66/3.83 fof(c22,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 3.66/3.83 fof(c23,plain,(![X]:(![Y]:((~parallel_lines(X,Y)|~convergent_lines(X,Y))&(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c22])).
% 3.66/3.83 fof(c24,plain,((![X]:(![Y]:(~parallel_lines(X,Y)|~convergent_lines(X,Y))))&(![X]:(![Y]:(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c23])).
% 3.66/3.83 fof(c26,plain,(![X14]:(![X15]:(![X16]:(![X17]:((~parallel_lines(X14,X15)|~convergent_lines(X14,X15))&(convergent_lines(X16,X17)|parallel_lines(X16,X17))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X14]:(![X15]:(~parallel_lines(X14,X15)|~convergent_lines(X14,X15))))&(![X16]:(![X17]:(convergent_lines(X16,X17)|parallel_lines(X16,X17))))),inference(variable_rename,[status(thm)],[c24])).])).
% 3.66/3.83 cnf(c27,plain,~parallel_lines(X120,X121)|~convergent_lines(X120,X121),inference(split_conjunct,[status(thm)],[c26])).
% 3.66/3.83 fof(ax2,axiom,(![X]:(![Y]:(equal_lines(X,Y)<=>(~distinct_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', ax2)).
% 3.66/3.83 fof(c29,plain,(![X]:(![Y]:(equal_lines(X,Y)<=>~distinct_lines(X,Y)))),inference(fof_simplification,[status(thm)],[ax2])).
% 3.66/3.83 fof(c30,plain,(![X]:(![Y]:((~equal_lines(X,Y)|~distinct_lines(X,Y))&(distinct_lines(X,Y)|equal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c29])).
% 3.66/3.83 fof(c31,plain,((![X]:(![Y]:(~equal_lines(X,Y)|~distinct_lines(X,Y))))&(![X]:(![Y]:(distinct_lines(X,Y)|equal_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c30])).
% 3.66/3.83 fof(c33,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~equal_lines(X18,X19)|~distinct_lines(X18,X19))&(distinct_lines(X20,X21)|equal_lines(X20,X21))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X18]:(![X19]:(~equal_lines(X18,X19)|~distinct_lines(X18,X19))))&(![X20]:(![X21]:(distinct_lines(X20,X21)|equal_lines(X20,X21))))),inference(variable_rename,[status(thm)],[c31])).])).
% 3.66/3.83 cnf(c35,plain,distinct_lines(X131,X132)|equal_lines(X131,X132),inference(split_conjunct,[status(thm)],[c33])).
% 3.66/3.83 fof(p1,axiom,(![X]:(![Y]:(distinct_lines(X,Y)=>convergent_lines(X,Y)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 3.66/3.83 fof(c102,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|convergent_lines(X,Y)))),inference(fof_nnf,[status(thm)],[p1])).
% 3.66/3.83 fof(c103,plain,(![X62]:(![X63]:(~distinct_lines(X62,X63)|convergent_lines(X62,X63)))),inference(variable_rename,[status(thm)],[c102])).
% 3.66/3.83 cnf(c104,plain,~distinct_lines(X163,X162)|convergent_lines(X163,X162),inference(split_conjunct,[status(thm)],[c103])).
% 3.66/3.83 cnf(c191,plain,convergent_lines(X187,X188)|equal_lines(X187,X188),inference(resolution,[status(thm)],[c104, c35])).
% 3.66/3.83 cnf(c203,plain,equal_lines(X200,X199)|~parallel_lines(X200,X199),inference(resolution,[status(thm)],[c191, c27])).
% 3.66/3.83 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart3)).
% 3.66/3.83 fof(c154,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 3.66/3.83 fof(c155,plain,(![X94]:~convergent_lines(X94,X94)),inference(variable_rename,[status(thm)],[c154])).
% 3.66/3.83 cnf(c156,plain,~convergent_lines(X97,X97),inference(split_conjunct,[status(thm)],[c155])).
% 3.66/3.83 cnf(c28,plain,convergent_lines(X125,X124)|parallel_lines(X125,X124),inference(split_conjunct,[status(thm)],[c26])).
% 3.66/3.83 fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 3.66/3.83 fof(c105,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 3.66/3.83 fof(c106,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c105])).
% 3.66/3.83 fof(c108,plain,(![X64]:(![X65]:(![X66]:(~convergent_lines(X64,X65)|(distinct_lines(X65,X66)|convergent_lines(X64,X66)))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,(![X64]:(![X65]:(~convergent_lines(X64,X65)|(![X66]:(distinct_lines(X65,X66)|convergent_lines(X64,X66)))))),inference(variable_rename,[status(thm)],[c106])).])).
% 3.66/3.83 cnf(c109,plain,~convergent_lines(X320,X319)|distinct_lines(X319,X321)|convergent_lines(X320,X321),inference(split_conjunct,[status(thm)],[c108])).
% 3.66/3.83 cnf(c360,plain,distinct_lines(X876,X877)|convergent_lines(X875,X877)|parallel_lines(X875,X876),inference(resolution,[status(thm)],[c109, c28])).
% 3.66/3.83 cnf(c1284,plain,distinct_lines(X884,X885)|parallel_lines(X885,X884),inference(resolution,[status(thm)],[c360, c156])).
% 3.66/3.83 cnf(c1313,plain,parallel_lines(X919,X918)|convergent_lines(X918,X919),inference(resolution,[status(thm)],[c1284, c104])).
% 3.66/3.83 cnf(c1405,plain,convergent_lines(X964,X963)|equal_lines(X963,X964),inference(resolution,[status(thm)],[c1313, c203])).
% 3.66/3.83 cnf(c1536,plain,equal_lines(X1039,X1040)|~parallel_lines(X1040,X1039),inference(resolution,[status(thm)],[c1405, c27])).
% 3.66/3.83 fof(cp1,axiom,(![X]:(![Y]:(~convergent_lines(parallel_through_point(Y,X),Y)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp1)).
% 3.66/3.83 fof(c99,plain,(![X]:(![Y]:~convergent_lines(parallel_through_point(Y,X),Y))),inference(fof_simplification,[status(thm)],[cp1])).
% 3.66/3.83 fof(c100,plain,(![X60]:(![X61]:~convergent_lines(parallel_through_point(X61,X60),X61))),inference(variable_rename,[status(thm)],[c99])).
% 3.66/3.83 cnf(c101,plain,~convergent_lines(parallel_through_point(X107,X106),X107),inference(split_conjunct,[status(thm)],[c100])).
% 3.66/3.83 cnf(c204,plain,equal_lines(parallel_through_point(X194,X193),X194),inference(resolution,[status(thm)],[c191, c101])).
% 3.66/3.83 cnf(c34,plain,~equal_lines(X128,X127)|~distinct_lines(X128,X127),inference(split_conjunct,[status(thm)],[c33])).
% 3.66/3.83 cnf(c1311,plain,parallel_lines(X895,X896)|~equal_lines(X896,X895),inference(resolution,[status(thm)],[c1284, c34])).
% 3.66/3.83 cnf(c1341,plain,parallel_lines(X898,parallel_through_point(X898,X899)),inference(resolution,[status(thm)],[c1311, c204])).
% 3.66/3.83 cnf(c1357,plain,equal_lines(X907,parallel_through_point(X907,X906)),inference(resolution,[status(thm)],[c1341, c203])).
% 3.66/3.83 cnf(c1280,plain,distinct_lines(X1950,X1952)|parallel_lines(parallel_through_point(X1952,X1951),X1950),inference(resolution,[status(thm)],[c360, c101])).
% 3.66/3.83 cnf(c5836,plain,parallel_lines(parallel_through_point(X2489,X2491),X2490)|~equal_lines(X2490,X2489),inference(resolution,[status(thm)],[c1280, c34])).
% 3.66/3.83 cnf(c8751,plain,parallel_lines(parallel_through_point(parallel_through_point(X2501,X2503),X2502),X2501),inference(resolution,[status(thm)],[c5836, c1357])).
% 3.66/3.83 cnf(c8849,plain,equal_lines(X2507,parallel_through_point(parallel_through_point(X2507,X2508),X2509)),inference(resolution,[status(thm)],[c8751, c1536])).
% 3.66/3.83 fof(cp2,axiom,(![X]:(![Y]:(~apart_point_and_line(X,parallel_through_point(Y,X))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp2)).
% 3.66/3.83 fof(c96,plain,(![X]:(![Y]:~apart_point_and_line(X,parallel_through_point(Y,X)))),inference(fof_simplification,[status(thm)],[cp2])).
% 3.66/3.83 fof(c97,plain,(![X58]:(![X59]:~apart_point_and_line(X58,parallel_through_point(X59,X58)))),inference(variable_rename,[status(thm)],[c96])).
% 3.66/3.83 cnf(c98,plain,~apart_point_and_line(X105,parallel_through_point(X104,X105)),inference(split_conjunct,[status(thm)],[c97])).
% 3.66/3.83 fof(a4,axiom,(![X]:(![Y]:(incident_point_and_line(X,Y)<=>(~apart_point_and_line(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a4)).
% 3.66/3.83 fof(c15,plain,(![X]:(![Y]:(incident_point_and_line(X,Y)<=>~apart_point_and_line(X,Y)))),inference(fof_simplification,[status(thm)],[a4])).
% 3.66/3.83 fof(c16,plain,(![X]:(![Y]:((~incident_point_and_line(X,Y)|~apart_point_and_line(X,Y))&(apart_point_and_line(X,Y)|incident_point_and_line(X,Y))))),inference(fof_nnf,[status(thm)],[c15])).
% 3.66/3.83 fof(c17,plain,((![X]:(![Y]:(~incident_point_and_line(X,Y)|~apart_point_and_line(X,Y))))&(![X]:(![Y]:(apart_point_and_line(X,Y)|incident_point_and_line(X,Y))))),inference(shift_quantors,[status(thm)],[c16])).
% 3.66/3.83 fof(c19,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~incident_point_and_line(X10,X11)|~apart_point_and_line(X10,X11))&(apart_point_and_line(X12,X13)|incident_point_and_line(X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X10]:(![X11]:(~incident_point_and_line(X10,X11)|~apart_point_and_line(X10,X11))))&(![X12]:(![X13]:(apart_point_and_line(X12,X13)|incident_point_and_line(X12,X13))))),inference(variable_rename,[status(thm)],[c17])).])).
% 3.66/3.83 cnf(c21,plain,apart_point_and_line(X117,X116)|incident_point_and_line(X117,X116),inference(split_conjunct,[status(thm)],[c19])).
% 3.66/3.83 fof(ceq2,axiom,(![X]:(![Y]:(![Z]:(apart_point_and_line(X,Y)=>(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq2)).
% 3.66/3.83 fof(c110,plain,(![X]:(![Y]:(![Z]:(~apart_point_and_line(X,Y)|(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq2])).
% 3.66/3.83 fof(c111,plain,(![X]:(![Y]:(~apart_point_and_line(X,Y)|(![Z]:(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),inference(shift_quantors,[status(thm)],[c110])).
% 3.66/3.83 fof(c113,plain,(![X67]:(![X68]:(![X69]:(~apart_point_and_line(X67,X68)|(distinct_lines(X68,X69)|apart_point_and_line(X67,X69)))))),inference(shift_quantors,[status(thm)],[fof(c112,plain,(![X67]:(![X68]:(~apart_point_and_line(X67,X68)|(![X69]:(distinct_lines(X68,X69)|apart_point_and_line(X67,X69)))))),inference(variable_rename,[status(thm)],[c111])).])).
% 3.66/3.83 cnf(c114,plain,~apart_point_and_line(X323,X325)|distinct_lines(X325,X324)|apart_point_and_line(X323,X324),inference(split_conjunct,[status(thm)],[c113])).
% 3.66/3.83 cnf(c381,plain,distinct_lines(X1498,X1499)|apart_point_and_line(X1497,X1499)|incident_point_and_line(X1497,X1498),inference(resolution,[status(thm)],[c114, c21])).
% 3.66/3.83 cnf(c3465,plain,distinct_lines(X2278,parallel_through_point(X2277,X2276))|incident_point_and_line(X2276,X2278),inference(resolution,[status(thm)],[c381, c98])).
% 3.66/3.83 cnf(c7555,plain,incident_point_and_line(X3022,X3021)|~equal_lines(X3021,parallel_through_point(X3020,X3022)),inference(resolution,[status(thm)],[c3465, c34])).
% 3.66/3.83 cnf(c11122,plain,incident_point_and_line(X3024,X3023),inference(resolution,[status(thm)],[c7555, c8849])).
% 3.66/3.83 fof(con,conjecture,(![X]:(![Y]:(![U]:(![V]:(((distinct_points(X,Y)&convergent_lines(U,V))&equal_points(X,intersection_point(U,V)))=>(incident_point_and_line(X,U)&incident_point_and_line(X,V))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 3.66/3.83 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![U]:(![V]:(((distinct_points(X,Y)&convergent_lines(U,V))&equal_points(X,intersection_point(U,V)))=>(incident_point_and_line(X,U)&incident_point_and_line(X,V)))))))),inference(assume_negation,[status(cth)],[con])).
% 3.66/3.83 fof(c1,negated_conjecture,(?[X]:(?[Y]:(?[U]:(?[V]:(((distinct_points(X,Y)&convergent_lines(U,V))&equal_points(X,intersection_point(U,V)))&(~incident_point_and_line(X,U)|~incident_point_and_line(X,V))))))),inference(fof_nnf,[status(thm)],[c0])).
% 3.66/3.83 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((distinct_points(X2,X3)&convergent_lines(X4,X5))&equal_points(X2,intersection_point(X4,X5)))&(~incident_point_and_line(X2,X4)|~incident_point_and_line(X2,X5))))))),inference(variable_rename,[status(thm)],[c1])).
% 3.66/3.83 fof(c3,negated_conjecture,(((distinct_points(skolem0001,skolem0002)&convergent_lines(skolem0003,skolem0004))&equal_points(skolem0001,intersection_point(skolem0003,skolem0004)))&(~incident_point_and_line(skolem0001,skolem0003)|~incident_point_and_line(skolem0001,skolem0004))),inference(skolemize,[status(esa)],[c2])).
% 3.66/3.83 cnf(c7,negated_conjecture,~incident_point_and_line(skolem0001,skolem0003)|~incident_point_and_line(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 3.66/3.83 cnf(c11132,plain,~incident_point_and_line(skolem0001,skolem0003),inference(resolution,[status(thm)],[c11122, c7])).
% 3.66/3.83 cnf(c11136,plain,$false,inference(resolution,[status(thm)],[c11132, c11122])).
% 3.66/3.83 % SZS output end CNFRefutation
% 3.66/3.83
% 3.66/3.83 % Initial clauses : 50
% 3.66/3.83 % Processed clauses : 522
% 3.66/3.83 % Factors computed : 52
% 3.66/3.83 % Resolvents computed: 10922
% 3.66/3.83 % Tautologies deleted: 12
% 3.66/3.83 % Forward subsumed : 1071
% 3.66/3.83 % Backward subsumed : 68
% 3.66/3.83 % -------- CPU Time ---------
% 3.66/3.83 % User time : 3.452 s
% 3.66/3.83 % System time : 0.033 s
% 3.66/3.83 % Total time : 3.485 s
%------------------------------------------------------------------------------