%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO234+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:40 EDT 2024
% Result : Theorem 7.51s 7.67s
% Output : Refutation 7.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO234+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n029.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 07:50:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 7.51/7.67 % Version: 1.5
% 7.51/7.67 % SZS status Theorem
% 7.51/7.67 % SZS output start CNFRefutation
% 7.51/7.67 fof(con,conjecture,(![L]:(![M]:(![N]:(unequally_directed_opposite_lines(L,M)=>(unequally_directed_lines(L,N)|unequally_directed_opposite_lines(M,N)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 7.51/7.67 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:(unequally_directed_opposite_lines(L,M)=>(unequally_directed_lines(L,N)|unequally_directed_opposite_lines(M,N))))))),inference(assume_negation,[status(cth)],[con])).
% 7.51/7.67 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:(unequally_directed_opposite_lines(L,M)&(~unequally_directed_lines(L,N)&~unequally_directed_opposite_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c0])).
% 7.51/7.67 fof(c2,negated_conjecture,(?[L]:(?[M]:(unequally_directed_opposite_lines(L,M)&(?[N]:(~unequally_directed_lines(L,N)&~unequally_directed_opposite_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c1])).
% 7.51/7.67 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(unequally_directed_opposite_lines(X2,X3)&(?[X4]:(~unequally_directed_lines(X2,X4)&~unequally_directed_opposite_lines(X3,X4)))))),inference(variable_rename,[status(thm)],[c2])).
% 7.51/7.67 fof(c4,negated_conjecture,(unequally_directed_opposite_lines(skolem0001,skolem0002)&(~unequally_directed_lines(skolem0001,skolem0003)&~unequally_directed_opposite_lines(skolem0002,skolem0003))),inference(skolemize,[status(esa)],[c3])).
% 7.51/7.67 cnf(c7,negated_conjecture,~unequally_directed_opposite_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 7.51/7.67 fof(a1_defns,axiom,(![X]:(![Y]:(unequally_directed_opposite_lines(X,Y)<=>unequally_directed_lines(X,reverse_line(Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax', a1_defns)).
% 7.51/7.67 fof(c183,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])).
% 7.51/7.67 fof(c184,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)],[c183])).
% 7.51/7.67 fof(c186,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(c185,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)],[c184])).])).
% 7.51/7.67 cnf(c188,plain,~unequally_directed_lines(X193,reverse_line(X192))|unequally_directed_opposite_lines(X193,X192),inference(split_conjunct,[status(thm)],[c186])).
% 7.51/7.67 cnf(c6,negated_conjecture,~unequally_directed_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 7.51/7.67 fof(ax5_basics,axiom,(![L]:equally_directed_lines(L,L)),file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax', ax5_basics)).
% 7.51/7.67 fof(c91,plain,(![X57]:equally_directed_lines(X57,X57)),inference(variable_rename,[status(thm)],[ax5_basics])).
% 7.51/7.67 cnf(c92,plain,equally_directed_lines(X118,X118),inference(split_conjunct,[status(thm)],[c91])).
% 7.51/7.67 fof(a4_defns,axiom,(![X]:(![Y]:(equally_directed_lines(X,Y)<=>(~unequally_directed_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax', a4_defns)).
% 7.51/7.67 fof(c164,plain,(![X]:(![Y]:(equally_directed_lines(X,Y)<=>~unequally_directed_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a4_defns])).
% 7.51/7.67 fof(c165,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)],[c164])).
% 7.51/7.67 fof(c166,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)],[c165])).
% 7.51/7.67 fof(c168,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(c167,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)],[c166])).])).
% 7.51/7.67 cnf(c169,plain,~equally_directed_lines(X152,X153)|~unequally_directed_lines(X152,X153),inference(split_conjunct,[status(thm)],[c168])).
% 7.51/7.67 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/sandbox/benchmark/Axioms/GEO009+0.ax', ax6_basics)).
% 7.51/7.67 fof(c86,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])).
% 7.51/7.67 fof(c87,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c86])).
% 7.51/7.67 fof(c89,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(c88,plain,(![X54]:(![X55]:(~unequally_directed_lines(X54,X55)|(![X56]:(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(variable_rename,[status(thm)],[c87])).])).
% 7.51/7.67 cnf(c90,plain,~unequally_directed_lines(X286,X287)|unequally_directed_lines(X286,X288)|unequally_directed_lines(X287,X288),inference(split_conjunct,[status(thm)],[c89])).
% 7.51/7.67 fof(ax8_basics,axiom,(![L]:(![M]:(unequally_directed_lines(L,M)|unequally_directed_lines(L,reverse_line(M))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax', ax8_basics)).
% 7.51/7.67 fof(c75,plain,(![X49]:(![X50]:(unequally_directed_lines(X49,X50)|unequally_directed_lines(X49,reverse_line(X50))))),inference(variable_rename,[status(thm)],[ax8_basics])).
% 7.51/7.67 cnf(c76,plain,unequally_directed_lines(X176,X177)|unequally_directed_lines(X176,reverse_line(X177)),inference(split_conjunct,[status(thm)],[c75])).
% 7.51/7.67 cnf(c205,plain,unequally_directed_opposite_lines(X197,X196)|unequally_directed_lines(X197,X196),inference(resolution,[status(thm)],[c188, c76])).
% 7.51/7.67 cnf(c212,plain,unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c205, c7])).
% 7.51/7.67 cnf(c340,plain,unequally_directed_lines(skolem0002,X347)|unequally_directed_lines(skolem0003,X347),inference(resolution,[status(thm)],[c90, c212])).
% 7.51/7.67 cnf(c398,plain,unequally_directed_lines(skolem0002,X392)|~equally_directed_lines(skolem0003,X392),inference(resolution,[status(thm)],[c340, c169])).
% 7.51/7.67 cnf(c170,plain,unequally_directed_lines(X155,X154)|equally_directed_lines(X155,X154),inference(split_conjunct,[status(thm)],[c168])).
% 7.51/7.67 cnf(c339,plain,unequally_directed_lines(X475,X474)|unequally_directed_lines(X473,X474)|equally_directed_lines(X475,X473),inference(resolution,[status(thm)],[c90, c170])).
% 7.51/7.67 cnf(c569,plain,unequally_directed_lines(X481,skolem0003)|equally_directed_lines(X481,skolem0001),inference(resolution,[status(thm)],[c339, c6])).
% 7.51/7.67 cnf(c651,plain,equally_directed_lines(X497,skolem0001)|~equally_directed_lines(X497,skolem0003),inference(resolution,[status(thm)],[c569, c169])).
% 7.51/7.67 cnf(c745,plain,equally_directed_lines(skolem0003,skolem0001),inference(resolution,[status(thm)],[c651, c92])).
% 7.51/7.67 cnf(c762,plain,unequally_directed_lines(skolem0002,skolem0001),inference(resolution,[status(thm)],[c745, c398])).
% 7.51/7.67 cnf(c772,plain,unequally_directed_lines(skolem0002,X518)|unequally_directed_lines(skolem0001,X518),inference(resolution,[status(thm)],[c762, c90])).
% 7.51/7.67 cnf(c920,plain,unequally_directed_lines(skolem0001,X528)|~equally_directed_lines(skolem0002,X528),inference(resolution,[status(thm)],[c772, c169])).
% 7.51/7.67 cnf(c1016,plain,unequally_directed_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c920, c92])).
% 7.51/7.67 cnf(c5,negated_conjecture,unequally_directed_opposite_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 7.51/7.67 cnf(c187,plain,~unequally_directed_opposite_lines(X189,X188)|unequally_directed_lines(X189,reverse_line(X188)),inference(split_conjunct,[status(thm)],[c186])).
% 7.51/7.67 cnf(c200,plain,unequally_directed_lines(skolem0001,reverse_line(skolem0002)),inference(resolution,[status(thm)],[c187, c5])).
% 7.51/7.67 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/sandbox/benchmark/Axioms/GEO009+0.ax', ax7_basics)).
% 7.51/7.67 fof(c77,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])).
% 7.51/7.67 fof(c78,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)],[c77])).
% 7.51/7.67 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(X51,reverse_line(X53)))|(unequally_directed_lines(X52,X53)&unequally_directed_lines(X52,reverse_line(X53)))))))),inference(shift_quantors,[status(thm)],[fof(c79,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)],[c78])).])).
% 7.51/7.67 fof(c81,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)],[c80])).
% 7.51/7.67 cnf(c83,plain,~unequally_directed_lines(X260,X258)|~unequally_directed_lines(X260,reverse_line(X258))|unequally_directed_lines(X260,X259)|unequally_directed_lines(X258,reverse_line(X259)),inference(split_conjunct,[status(thm)],[c81])).
% 7.51/7.67 cnf(c288,plain,~unequally_directed_lines(skolem0001,skolem0002)|unequally_directed_lines(skolem0001,X642)|unequally_directed_lines(skolem0002,reverse_line(X642)),inference(resolution,[status(thm)],[c83, c200])).
% 7.51/7.67 cnf(c1471,plain,unequally_directed_lines(skolem0001,X2680)|unequally_directed_lines(skolem0002,reverse_line(X2680)),inference(resolution,[status(thm)],[c288, c1016])).
% 7.51/7.67 cnf(c17571,plain,unequally_directed_lines(skolem0002,reverse_line(skolem0003)),inference(resolution,[status(thm)],[c1471, c6])).
% 7.51/7.67 cnf(c17670,plain,unequally_directed_opposite_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c17571, c188])).
% 7.51/7.67 cnf(c17677,plain,$false,inference(resolution,[status(thm)],[c17670, c7])).
% 7.51/7.67 % SZS output end CNFRefutation
% 7.51/7.67
% 7.51/7.67 % Initial clauses : 69
% 7.51/7.67 % Processed clauses : 637
% 7.51/7.67 % Factors computed : 83
% 7.51/7.67 % Resolvents computed: 17409
% 7.51/7.67 % Tautologies deleted: 8
% 7.51/7.67 % Forward subsumed : 1458
% 7.51/7.67 % Backward subsumed : 6
% 7.51/7.67 % -------- CPU Time ---------
% 7.51/7.67 % User time : 7.283 s
% 7.51/7.67 % System time : 0.045 s
% 7.51/7.67 % Total time : 7.328 s
%------------------------------------------------------------------------------