%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO255+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:47 EDT 2024
% Result : Theorem 18.80s 18.98s
% Output : Refutation 18.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO255+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n025.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 9 08:32:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 18.80/18.98 % Version: 1.5
% 18.80/18.98 % SZS status Theorem
% 18.80/18.98 % SZS output start CNFRefutation
% 18.80/18.98 fof(con,conjecture,(![L]:(![A]:(![B]:((line(L)&distinct_points(A,B))=>(~(before_on_line(L,A,B)&before_on_line(L,B,A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 18.80/18.98 fof(c0,negated_conjecture,(~(![L]:(![A]:(![B]:((line(L)&distinct_points(A,B))=>(~(before_on_line(L,A,B)&before_on_line(L,B,A)))))))),inference(assume_negation,[status(cth)],[con])).
% 18.80/18.98 fof(c1,negated_conjecture,(?[L]:(?[A]:(?[B]:((line(L)&distinct_points(A,B))&(before_on_line(L,A,B)&before_on_line(L,B,A)))))),inference(fof_nnf,[status(thm)],[c0])).
% 18.80/18.98 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((line(X2)&distinct_points(X3,X4))&(before_on_line(X2,X3,X4)&before_on_line(X2,X4,X3)))))),inference(variable_rename,[status(thm)],[c1])).
% 18.80/18.98 fof(c3,negated_conjecture,((line(skolem0001)&distinct_points(skolem0002,skolem0003))&(before_on_line(skolem0001,skolem0002,skolem0003)&before_on_line(skolem0001,skolem0003,skolem0002))),inference(skolemize,[status(esa)],[c2])).
% 18.80/18.98 cnf(c6,negated_conjecture,before_on_line(skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 18.80/18.98 fof(bf_def,axiom,(![L]:(![A]:(![B]:(before_on_line(L,A,B)<=>(((distinct_points(A,B)&(~(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))&(~(left_apart_point(B,L)|left_apart_point(B,reverse_line(L)))))&(~unequally_directed_lines(L,line_connecting(A,B)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', bf_def)).
% 18.80/18.98 fof(c123,plain,(![L]:(![A]:(![B]:(before_on_line(L,A,B)<=>(((distinct_points(A,B)&(~(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))&(~(left_apart_point(B,L)|left_apart_point(B,reverse_line(L)))))&~unequally_directed_lines(L,line_connecting(A,B))))))),inference(fof_simplification,[status(thm)],[bf_def])).
% 18.80/18.98 fof(c124,plain,(![L]:(![A]:(![B]:((~before_on_line(L,A,B)|(((distinct_points(A,B)&(~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L))))&(~left_apart_point(B,L)&~left_apart_point(B,reverse_line(L))))&~unequally_directed_lines(L,line_connecting(A,B))))&((((~distinct_points(A,B)|(left_apart_point(A,L)|left_apart_point(A,reverse_line(L))))|(left_apart_point(B,L)|left_apart_point(B,reverse_line(L))))|unequally_directed_lines(L,line_connecting(A,B)))|before_on_line(L,A,B)))))),inference(fof_nnf,[status(thm)],[c123])).
% 18.80/18.98 fof(c125,plain,((![L]:(![A]:(![B]:(~before_on_line(L,A,B)|(((distinct_points(A,B)&(~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L))))&(~left_apart_point(B,L)&~left_apart_point(B,reverse_line(L))))&~unequally_directed_lines(L,line_connecting(A,B)))))))&(![L]:(![A]:(![B]:((((~distinct_points(A,B)|(left_apart_point(A,L)|left_apart_point(A,reverse_line(L))))|(left_apart_point(B,L)|left_apart_point(B,reverse_line(L))))|unequally_directed_lines(L,line_connecting(A,B)))|before_on_line(L,A,B)))))),inference(shift_quantors,[status(thm)],[c124])).
% 18.80/18.98 fof(c127,plain,(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:(![X79]:((~before_on_line(X74,X75,X76)|(((distinct_points(X75,X76)&(~left_apart_point(X75,X74)&~left_apart_point(X75,reverse_line(X74))))&(~left_apart_point(X76,X74)&~left_apart_point(X76,reverse_line(X74))))&~unequally_directed_lines(X74,line_connecting(X75,X76))))&((((~distinct_points(X78,X79)|(left_apart_point(X78,X77)|left_apart_point(X78,reverse_line(X77))))|(left_apart_point(X79,X77)|left_apart_point(X79,reverse_line(X77))))|unequally_directed_lines(X77,line_connecting(X78,X79)))|before_on_line(X77,X78,X79))))))))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((![X74]:(![X75]:(![X76]:(~before_on_line(X74,X75,X76)|(((distinct_points(X75,X76)&(~left_apart_point(X75,X74)&~left_apart_point(X75,reverse_line(X74))))&(~left_apart_point(X76,X74)&~left_apart_point(X76,reverse_line(X74))))&~unequally_directed_lines(X74,line_connecting(X75,X76)))))))&(![X77]:(![X78]:(![X79]:((((~distinct_points(X78,X79)|(left_apart_point(X78,X77)|left_apart_point(X78,reverse_line(X77))))|(left_apart_point(X79,X77)|left_apart_point(X79,reverse_line(X77))))|unequally_directed_lines(X77,line_connecting(X78,X79)))|before_on_line(X77,X78,X79)))))),inference(variable_rename,[status(thm)],[c125])).])).
% 18.80/18.98 fof(c128,plain,(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:(![X79]:(((((~before_on_line(X74,X75,X76)|distinct_points(X75,X76))&((~before_on_line(X74,X75,X76)|~left_apart_point(X75,X74))&(~before_on_line(X74,X75,X76)|~left_apart_point(X75,reverse_line(X74)))))&((~before_on_line(X74,X75,X76)|~left_apart_point(X76,X74))&(~before_on_line(X74,X75,X76)|~left_apart_point(X76,reverse_line(X74)))))&(~before_on_line(X74,X75,X76)|~unequally_directed_lines(X74,line_connecting(X75,X76))))&((((~distinct_points(X78,X79)|(left_apart_point(X78,X77)|left_apart_point(X78,reverse_line(X77))))|(left_apart_point(X79,X77)|left_apart_point(X79,reverse_line(X77))))|unequally_directed_lines(X77,line_connecting(X78,X79)))|before_on_line(X77,X78,X79))))))))),inference(distribute,[status(thm)],[c127])).
% 18.80/18.98 cnf(c134,plain,~before_on_line(X172,X170,X171)|~unequally_directed_lines(X172,line_connecting(X170,X171)),inference(split_conjunct,[status(thm)],[c128])).
% 18.80/18.98 fof(oag5,axiom,(![L]:(~unequally_directed_lines(L,L))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag5)).
% 18.80/18.98 fof(c93,plain,(![L]:~unequally_directed_lines(L,L)),inference(fof_simplification,[status(thm)],[oag5])).
% 18.80/18.98 fof(c94,plain,(![X57]:~unequally_directed_lines(X57,X57)),inference(variable_rename,[status(thm)],[c93])).
% 18.80/18.98 cnf(c95,plain,~unequally_directed_lines(X98,X98),inference(split_conjunct,[status(thm)],[c94])).
% 18.80/18.98 fof(oag6,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/GEO007+0.ax', oag6)).
% 18.80/18.98 fof(c88,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,M)|(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(fof_nnf,[status(thm)],[oag6])).
% 18.80/18.98 fof(c89,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c88])).
% 18.80/18.98 fof(c91,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(c90,plain,(![X54]:(![X55]:(~unequally_directed_lines(X54,X55)|(![X56]:(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(variable_rename,[status(thm)],[c89])).])).
% 18.80/18.98 cnf(c92,plain,~unequally_directed_lines(X157,X156)|unequally_directed_lines(X157,X155)|unequally_directed_lines(X156,X155),inference(split_conjunct,[status(thm)],[c91])).
% 18.80/18.98 cnf(c4,negated_conjecture,line(skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 18.80/18.98 fof(oag8,axiom,(![L]:(![M]:((line(L)&line(M))=>(unequally_directed_lines(L,M)|unequally_directed_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag8)).
% 18.80/18.98 fof(c76,plain,(![L]:(![M]:((~line(L)|~line(M))|(unequally_directed_lines(L,M)|unequally_directed_lines(L,reverse_line(M)))))),inference(fof_nnf,[status(thm)],[oag8])).
% 18.80/18.98 fof(c77,plain,(![X49]:(![X50]:((~line(X49)|~line(X50))|(unequally_directed_lines(X49,X50)|unequally_directed_lines(X49,reverse_line(X50)))))),inference(variable_rename,[status(thm)],[c76])).
% 18.80/18.98 cnf(c78,plain,~line(X207)|~line(X206)|unequally_directed_lines(X207,X206)|unequally_directed_lines(X207,reverse_line(X206)),inference(split_conjunct,[status(thm)],[c77])).
% 18.80/18.98 cnf(c233,plain,~line(X216)|unequally_directed_lines(X216,X216)|unequally_directed_lines(X216,reverse_line(X216)),inference(factor,[status(thm)],[c78])).
% 18.80/18.98 cnf(c248,plain,unequally_directed_lines(skolem0001,skolem0001)|unequally_directed_lines(skolem0001,reverse_line(skolem0001)),inference(resolution,[status(thm)],[c233, c4])).
% 18.80/18.98 cnf(c264,plain,unequally_directed_lines(skolem0001,reverse_line(skolem0001)),inference(resolution,[status(thm)],[c248, c95])).
% 18.80/18.98 cnf(c275,plain,unequally_directed_lines(skolem0001,X241)|unequally_directed_lines(reverse_line(skolem0001),X241),inference(resolution,[status(thm)],[c264, c92])).
% 18.80/18.98 cnf(c278,plain,unequally_directed_lines(reverse_line(skolem0001),line_connecting(X289,X290))|~before_on_line(skolem0001,X289,X290),inference(resolution,[status(thm)],[c275, c134])).
% 18.80/18.98 cnf(c335,plain,unequally_directed_lines(reverse_line(skolem0001),line_connecting(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c278, c6])).
% 18.80/18.98 fof(oag7,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/GEO007+0.ax', oag7)).
% 18.80/18.98 fof(c79,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)],[oag7])).
% 18.80/18.98 fof(c80,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)],[c79])).
% 18.80/18.98 fof(c82,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(c81,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)],[c80])).])).
% 18.80/18.98 fof(c83,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)],[c82])).
% 18.80/18.98 cnf(c86,plain,~unequally_directed_lines(X230,X228)|~unequally_directed_lines(X230,reverse_line(X228))|unequally_directed_lines(X230,reverse_line(X229))|unequally_directed_lines(X228,X229),inference(split_conjunct,[status(thm)],[c83])).
% 18.80/18.98 fof(oagco9,axiom,(![A]:(![B]:(~unequally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco9)).
% 18.80/18.98 fof(c28,plain,(![A]:(![B]:~unequally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A))))),inference(fof_simplification,[status(thm)],[oagco9])).
% 18.80/18.98 fof(c29,plain,(![X23]:(![X24]:~unequally_directed_lines(line_connecting(X23,X24),reverse_line(line_connecting(X24,X23))))),inference(variable_rename,[status(thm)],[c28])).
% 18.80/18.98 cnf(c30,plain,~unequally_directed_lines(line_connecting(X147,X148),reverse_line(line_connecting(X148,X147))),inference(split_conjunct,[status(thm)],[c29])).
% 18.80/18.98 cnf(c7,negated_conjecture,before_on_line(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 18.80/18.98 cnf(c334,plain,unequally_directed_lines(reverse_line(skolem0001),line_connecting(skolem0003,skolem0002)),inference(resolution,[status(thm)],[c278, c7])).
% 18.80/18.98 cnf(c337,plain,unequally_directed_lines(reverse_line(skolem0001),X429)|unequally_directed_lines(line_connecting(skolem0003,skolem0002),X429),inference(resolution,[status(thm)],[c334, c92])).
% 18.80/18.98 cnf(c654,plain,unequally_directed_lines(reverse_line(skolem0001),reverse_line(line_connecting(skolem0002,skolem0003))),inference(resolution,[status(thm)],[c337, c30])).
% 18.80/18.98 cnf(c667,plain,~unequally_directed_lines(reverse_line(skolem0001),line_connecting(skolem0002,skolem0003))|unequally_directed_lines(reverse_line(skolem0001),reverse_line(X2920))|unequally_directed_lines(line_connecting(skolem0002,skolem0003),X2920),inference(resolution,[status(thm)],[c654, c86])).
% 18.80/18.98 cnf(c39379,plain,unequally_directed_lines(reverse_line(skolem0001),reverse_line(X2921))|unequally_directed_lines(line_connecting(skolem0002,skolem0003),X2921),inference(resolution,[status(thm)],[c667, c335])).
% 18.80/18.98 cnf(c39513,plain,unequally_directed_lines(line_connecting(skolem0002,skolem0003),skolem0001),inference(resolution,[status(thm)],[c39379, c95])).
% 18.80/18.98 cnf(c39598,plain,unequally_directed_lines(line_connecting(skolem0002,skolem0003),X2923)|unequally_directed_lines(skolem0001,X2923),inference(resolution,[status(thm)],[c39513, c92])).
% 18.80/18.98 cnf(c39796,plain,unequally_directed_lines(skolem0001,line_connecting(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c39598, c95])).
% 18.80/18.98 cnf(c39920,plain,~before_on_line(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c39796, c134])).
% 18.80/18.98 cnf(c39936,plain,$false,inference(resolution,[status(thm)],[c39920, c6])).
% 18.80/18.98 % SZS output end CNFRefutation
% 18.80/18.98
% 18.80/18.98 % Initial clauses : 62
% 18.80/18.98 % Processed clauses : 594
% 18.80/18.98 % Factors computed : 505
% 18.80/18.98 % Resolvents computed: 39287
% 18.80/18.98 % Tautologies deleted: 8
% 18.80/18.98 % Forward subsumed : 1142
% 18.80/18.98 % Backward subsumed : 8
% 18.80/18.98 % -------- CPU Time ---------
% 18.80/18.98 % User time : 18.523 s
% 18.80/18.98 % System time : 0.114 s
% 18.80/18.98 % Total time : 18.637 s
%------------------------------------------------------------------------------