%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO231+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:39 EDT 2024
% Result : Theorem 9.67s 9.87s
% Output : Refutation 9.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO231+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.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 07:48:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 9.67/9.87 % Version: 1.5
% 9.67/9.87 % SZS status Theorem
% 9.67/9.87 % SZS output start CNFRefutation
% 9.67/9.87 fof(a4_defns,axiom,(![X]:(![Y]:(equally_directed_lines(X,Y)<=>(~unequally_directed_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a4_defns)).
% 9.67/9.87 fof(c163,plain,(![X]:(![Y]:(equally_directed_lines(X,Y)<=>~unequally_directed_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a4_defns])).
% 9.67/9.87 fof(c164,plain,(![X]:(![Y]:((~equally_directed_lines(X,Y)|~unequally_directed_lines(X,Y))&(unequally_directed_lines(X,Y)|equally_directed_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c163])).
% 9.67/9.87 fof(c165,plain,((![X]:(![Y]:(~equally_directed_lines(X,Y)|~unequally_directed_lines(X,Y))))&(![X]:(![Y]:(unequally_directed_lines(X,Y)|equally_directed_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c164])).
% 9.67/9.87 fof(c167,plain,(![X98]:(![X99]:(![X100]:(![X101]:((~equally_directed_lines(X98,X99)|~unequally_directed_lines(X98,X99))&(unequally_directed_lines(X100,X101)|equally_directed_lines(X100,X101))))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,((![X98]:(![X99]:(~equally_directed_lines(X98,X99)|~unequally_directed_lines(X98,X99))))&(![X100]:(![X101]:(unequally_directed_lines(X100,X101)|equally_directed_lines(X100,X101))))),inference(variable_rename,[status(thm)],[c165])).])).
% 9.67/9.87 cnf(c168,plain,~equally_directed_lines(X152,X153)|~unequally_directed_lines(X152,X153),inference(split_conjunct,[status(thm)],[c167])).
% 9.67/9.87 fof(a5_defns,axiom,(![X]:(![Y]:(equally_directed_opposite_lines(X,Y)<=>(~unequally_directed_opposite_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a5_defns)).
% 9.67/9.87 fof(c156,plain,(![X]:(![Y]:(equally_directed_opposite_lines(X,Y)<=>~unequally_directed_opposite_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5_defns])).
% 9.67/9.87 fof(c157,plain,(![X]:(![Y]:((~equally_directed_opposite_lines(X,Y)|~unequally_directed_opposite_lines(X,Y))&(unequally_directed_opposite_lines(X,Y)|equally_directed_opposite_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c156])).
% 9.67/9.87 fof(c158,plain,((![X]:(![Y]:(~equally_directed_opposite_lines(X,Y)|~unequally_directed_opposite_lines(X,Y))))&(![X]:(![Y]:(unequally_directed_opposite_lines(X,Y)|equally_directed_opposite_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c157])).
% 9.67/9.87 fof(c160,plain,(![X94]:(![X95]:(![X96]:(![X97]:((~equally_directed_opposite_lines(X94,X95)|~unequally_directed_opposite_lines(X94,X95))&(unequally_directed_opposite_lines(X96,X97)|equally_directed_opposite_lines(X96,X97))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,((![X94]:(![X95]:(~equally_directed_opposite_lines(X94,X95)|~unequally_directed_opposite_lines(X94,X95))))&(![X96]:(![X97]:(unequally_directed_opposite_lines(X96,X97)|equally_directed_opposite_lines(X96,X97))))),inference(variable_rename,[status(thm)],[c158])).])).
% 9.67/9.87 cnf(c162,plain,unequally_directed_opposite_lines(X147,X148)|equally_directed_opposite_lines(X147,X148),inference(split_conjunct,[status(thm)],[c160])).
% 9.67/9.87 fof(a1_defns,axiom,(![X]:(![Y]:(unequally_directed_opposite_lines(X,Y)<=>unequally_directed_lines(X,reverse_line(Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a1_defns)).
% 9.67/9.87 fof(c182,plain,(![X]:(![Y]:((~unequally_directed_opposite_lines(X,Y)|unequally_directed_lines(X,reverse_line(Y)))&(~unequally_directed_lines(X,reverse_line(Y))|unequally_directed_opposite_lines(X,Y))))),inference(fof_nnf,[status(thm)],[a1_defns])).
% 9.67/9.87 fof(c183,plain,((![X]:(![Y]:(~unequally_directed_opposite_lines(X,Y)|unequally_directed_lines(X,reverse_line(Y)))))&(![X]:(![Y]:(~unequally_directed_lines(X,reverse_line(Y))|unequally_directed_opposite_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c182])).
% 9.67/9.87 fof(c185,plain,(![X110]:(![X111]:(![X112]:(![X113]:((~unequally_directed_opposite_lines(X110,X111)|unequally_directed_lines(X110,reverse_line(X111)))&(~unequally_directed_lines(X112,reverse_line(X113))|unequally_directed_opposite_lines(X112,X113))))))),inference(shift_quantors,[status(thm)],[fof(c184,plain,((![X110]:(![X111]:(~unequally_directed_opposite_lines(X110,X111)|unequally_directed_lines(X110,reverse_line(X111)))))&(![X112]:(![X113]:(~unequally_directed_lines(X112,reverse_line(X113))|unequally_directed_opposite_lines(X112,X113))))),inference(variable_rename,[status(thm)],[c183])).])).
% 9.67/9.87 cnf(c186,plain,~unequally_directed_opposite_lines(X187,X186)|unequally_directed_lines(X187,reverse_line(X186)),inference(split_conjunct,[status(thm)],[c185])).
% 9.67/9.87 cnf(c195,plain,unequally_directed_lines(X270,reverse_line(X271))|equally_directed_opposite_lines(X270,X271),inference(resolution,[status(thm)],[c186, c162])).
% 9.67/9.87 cnf(c296,plain,equally_directed_opposite_lines(X305,X306)|~equally_directed_lines(X305,reverse_line(X306)),inference(resolution,[status(thm)],[c195, c168])).
% 9.67/9.87 fof(con,conjecture,(![L]:(![M]:(![N]:((equally_directed_opposite_lines(L,M)&equally_directed_lines(L,N))=>equally_directed_opposite_lines(M,N))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 9.67/9.87 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:((equally_directed_opposite_lines(L,M)&equally_directed_lines(L,N))=>equally_directed_opposite_lines(M,N)))))),inference(assume_negation,[status(cth)],[con])).
% 9.67/9.87 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:((equally_directed_opposite_lines(L,M)&equally_directed_lines(L,N))&~equally_directed_opposite_lines(M,N))))),inference(fof_nnf,[status(thm)],[c0])).
% 9.67/9.87 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((equally_directed_opposite_lines(X2,X3)&equally_directed_lines(X2,X4))&~equally_directed_opposite_lines(X3,X4))))),inference(variable_rename,[status(thm)],[c1])).
% 9.67/9.87 fof(c3,negated_conjecture,((equally_directed_opposite_lines(skolem0001,skolem0002)&equally_directed_lines(skolem0001,skolem0003))&~equally_directed_opposite_lines(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c2])).
% 9.67/9.87 cnf(c4,negated_conjecture,equally_directed_opposite_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 9.67/9.87 cnf(c161,plain,~equally_directed_opposite_lines(X145,X146)|~unequally_directed_opposite_lines(X145,X146),inference(split_conjunct,[status(thm)],[c160])).
% 9.67/9.87 cnf(c169,plain,unequally_directed_lines(X155,X154)|equally_directed_lines(X155,X154),inference(split_conjunct,[status(thm)],[c167])).
% 9.67/9.87 cnf(c187,plain,~unequally_directed_lines(X191,reverse_line(X190))|unequally_directed_opposite_lines(X191,X190),inference(split_conjunct,[status(thm)],[c185])).
% 9.67/9.87 cnf(c199,plain,unequally_directed_opposite_lines(X281,X280)|equally_directed_lines(X281,reverse_line(X280)),inference(resolution,[status(thm)],[c187, c169])).
% 9.67/9.87 cnf(c316,plain,equally_directed_lines(X325,reverse_line(X324))|~equally_directed_opposite_lines(X325,X324),inference(resolution,[status(thm)],[c199, c161])).
% 9.67/9.87 cnf(c353,plain,equally_directed_lines(skolem0001,reverse_line(skolem0002)),inference(resolution,[status(thm)],[c316, c4])).
% 9.67/9.87 fof(ax5_basics,axiom,(![L]:equally_directed_lines(L,L)),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax5_basics)).
% 9.67/9.87 fof(c90,plain,(![X57]:equally_directed_lines(X57,X57)),inference(variable_rename,[status(thm)],[ax5_basics])).
% 9.67/9.87 cnf(c91,plain,equally_directed_lines(X118,X118),inference(split_conjunct,[status(thm)],[c90])).
% 9.67/9.87 fof(ax6_basics,axiom,(![L]:(![M]:(![N]:(unequally_directed_lines(L,M)=>(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax6_basics)).
% 9.67/9.87 fof(c85,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,M)|(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(fof_nnf,[status(thm)],[ax6_basics])).
% 9.67/9.87 fof(c86,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c85])).
% 9.67/9.87 fof(c88,plain,(![X54]:(![X55]:(![X56]:(~unequally_directed_lines(X54,X55)|(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(shift_quantors,[status(thm)],[fof(c87,plain,(![X54]:(![X55]:(~unequally_directed_lines(X54,X55)|(![X56]:(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(variable_rename,[status(thm)],[c86])).])).
% 9.67/9.87 cnf(c89,plain,~unequally_directed_lines(X296,X297)|unequally_directed_lines(X296,X295)|unequally_directed_lines(X297,X295),inference(split_conjunct,[status(thm)],[c88])).
% 9.67/9.88 cnf(c341,plain,unequally_directed_lines(X494,X495)|unequally_directed_lines(X493,X495)|equally_directed_lines(X494,X493),inference(resolution,[status(thm)],[c89, c169])).
% 9.67/9.88 cnf(c673,plain,unequally_directed_lines(X897,X898)|equally_directed_lines(X896,X897)|~equally_directed_lines(X896,X898),inference(resolution,[status(thm)],[c341, c168])).
% 9.67/9.88 cnf(c2681,plain,unequally_directed_lines(X899,X900)|equally_directed_lines(X900,X899),inference(resolution,[status(thm)],[c673, c91])).
% 9.67/9.88 cnf(c2694,plain,equally_directed_lines(X907,X906)|~equally_directed_lines(X906,X907),inference(resolution,[status(thm)],[c2681, c168])).
% 9.67/9.88 cnf(c2850,plain,equally_directed_lines(reverse_line(skolem0002),skolem0001),inference(resolution,[status(thm)],[c2694, c353])).
% 9.67/9.88 cnf(c5,negated_conjecture,equally_directed_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 9.67/9.88 cnf(c2845,plain,equally_directed_lines(skolem0003,skolem0001),inference(resolution,[status(thm)],[c2694, c5])).
% 9.67/9.88 cnf(c2989,plain,unequally_directed_lines(X1086,skolem0001)|equally_directed_lines(skolem0003,X1086),inference(resolution,[status(thm)],[c2845, c673])).
% 9.67/9.88 cnf(c5938,plain,equally_directed_lines(skolem0003,X1217)|~equally_directed_lines(X1217,skolem0001),inference(resolution,[status(thm)],[c2989, c168])).
% 9.67/9.88 cnf(c7763,plain,equally_directed_lines(skolem0003,reverse_line(skolem0002)),inference(resolution,[status(thm)],[c5938, c2850])).
% 9.67/9.88 cnf(c7838,plain,equally_directed_opposite_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c7763, c296])).
% 9.67/9.88 fof(ax8_basics,axiom,(![L]:(![M]:(unequally_directed_lines(L,M)|unequally_directed_lines(L,reverse_line(M))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax8_basics)).
% 9.67/9.88 fof(c74,plain,(![X49]:(![X50]:(unequally_directed_lines(X49,X50)|unequally_directed_lines(X49,reverse_line(X50))))),inference(variable_rename,[status(thm)],[ax8_basics])).
% 9.67/9.88 cnf(c75,plain,unequally_directed_lines(X173,X172)|unequally_directed_lines(X173,reverse_line(X172)),inference(split_conjunct,[status(thm)],[c74])).
% 9.67/9.88 cnf(c198,plain,unequally_directed_opposite_lines(X193,X192)|unequally_directed_lines(X193,X192),inference(resolution,[status(thm)],[c187, c75])).
% 9.67/9.88 cnf(c202,plain,unequally_directed_lines(X197,X196)|~equally_directed_opposite_lines(X197,X196),inference(resolution,[status(thm)],[c198, c161])).
% 9.67/9.88 cnf(c206,plain,unequally_directed_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c202, c4])).
% 9.67/9.88 cnf(c342,plain,unequally_directed_lines(skolem0001,X351)|unequally_directed_lines(skolem0002,X351),inference(resolution,[status(thm)],[c89, c206])).
% 9.67/9.88 cnf(c391,plain,unequally_directed_lines(skolem0002,X389)|~equally_directed_lines(skolem0001,X389),inference(resolution,[status(thm)],[c342, c168])).
% 9.67/9.88 cnf(c433,plain,unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c391, c5])).
% 9.67/9.88 cnf(c6,negated_conjecture,~equally_directed_opposite_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 9.67/9.88 cnf(c189,plain,unequally_directed_opposite_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c162, c6])).
% 9.67/9.88 cnf(c194,plain,unequally_directed_lines(skolem0002,reverse_line(skolem0003)),inference(resolution,[status(thm)],[c186, c189])).
% 9.67/9.88 fof(ax7_basics,axiom,(![L]:(![M]:(![N]:((unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M)))=>((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax7_basics)).
% 9.67/9.88 fof(c76,plain,(![L]:(![M]:(![N]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),inference(fof_nnf,[status(thm)],[ax7_basics])).
% 9.67/9.88 fof(c77,plain,(![L]:(![M]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|(![N]:((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),inference(shift_quantors,[status(thm)],[c76])).
% 9.67/9.88 fof(c79,plain,(![X51]:(![X52]:(![X53]:((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|((unequally_directed_lines(X51,X53)&unequally_directed_lines(X51,reverse_line(X53)))|(unequally_directed_lines(X52,X53)&unequally_directed_lines(X52,reverse_line(X53)))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,(![X51]:(![X52]:((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(![X53]:((unequally_directed_lines(X51,X53)&unequally_directed_lines(X51,reverse_line(X53)))|(unequally_directed_lines(X52,X53)&unequally_directed_lines(X52,reverse_line(X53)))))))),inference(variable_rename,[status(thm)],[c77])).])).
% 9.67/9.88 fof(c80,plain,(![X51]:(![X52]:(![X53]:((((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,X53)|unequally_directed_lines(X52,X53)))&((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,X53)|unequally_directed_lines(X52,reverse_line(X53)))))&(((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,reverse_line(X53))|unequally_directed_lines(X52,X53)))&((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,reverse_line(X53))|unequally_directed_lines(X52,reverse_line(X53))))))))),inference(distribute,[status(thm)],[c79])).
% 9.67/9.88 cnf(c82,plain,~unequally_directed_lines(X268,X267)|~unequally_directed_lines(X268,reverse_line(X267))|unequally_directed_lines(X268,X269)|unequally_directed_lines(X267,reverse_line(X269)),inference(split_conjunct,[status(thm)],[c80])).
% 9.67/9.88 cnf(c285,plain,~unequally_directed_lines(skolem0002,skolem0003)|unequally_directed_lines(skolem0002,X715)|unequally_directed_lines(skolem0003,reverse_line(X715)),inference(resolution,[status(thm)],[c82, c194])).
% 9.67/9.88 cnf(c1656,plain,unequally_directed_lines(skolem0002,X2827)|unequally_directed_lines(skolem0003,reverse_line(X2827)),inference(resolution,[status(thm)],[c285, c433])).
% 9.67/9.88 cnf(c22324,plain,unequally_directed_lines(skolem0002,X2828)|unequally_directed_opposite_lines(skolem0003,X2828),inference(resolution,[status(thm)],[c1656, c187])).
% 9.67/9.88 cnf(c22396,plain,unequally_directed_opposite_lines(skolem0003,X2829)|~equally_directed_lines(skolem0002,X2829),inference(resolution,[status(thm)],[c22324, c168])).
% 9.67/9.88 cnf(c22422,plain,unequally_directed_opposite_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c22396, c91])).
% 9.67/9.88 cnf(c22436,plain,~equally_directed_opposite_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c22422, c161])).
% 9.67/9.88 cnf(c22445,plain,$false,inference(resolution,[status(thm)],[c22436, c7838])).
% 9.67/9.88 % SZS output end CNFRefutation
% 9.67/9.88
% 9.67/9.88 % Initial clauses : 69
% 9.67/9.88 % Processed clauses : 670
% 9.67/9.88 % Factors computed : 88
% 9.67/9.88 % Resolvents computed: 22170
% 9.67/9.88 % Tautologies deleted: 8
% 9.67/9.88 % Forward subsumed : 1519
% 9.67/9.88 % Backward subsumed : 8
% 9.67/9.88 % -------- CPU Time ---------
% 9.67/9.88 % User time : 9.419 s
% 9.67/9.88 % System time : 0.070 s
% 9.67/9.88 % Total time : 9.489 s
%------------------------------------------------------------------------------