%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO234+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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 238.58s 238.80s
% Output : Refutation 238.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO234+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n002.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:11:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 238.58/238.80 % Version: 1.5
% 238.58/238.80 % SZS status Theorem
% 238.58/238.80 % SZS output start CNFRefutation
% 238.58/238.80 fof(oag5,axiom,(![L]:(~unequally_directed_lines(L,L))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag5)).
% 238.58/238.80 fof(c93,plain,(![L]:~unequally_directed_lines(L,L)),inference(fof_simplification,[status(thm)],[oag5])).
% 238.58/238.80 fof(c94,plain,(![X57]:~unequally_directed_lines(X57,X57)),inference(variable_rename,[status(thm)],[c93])).
% 238.58/238.80 cnf(c95,plain,~unequally_directed_lines(X98,X98),inference(split_conjunct,[status(thm)],[c94])).
% 238.58/238.80 fof(con,conjecture,(![L]:(![M]:(![N]:(unequally_directed_lines(L,reverse_line(M))=>(unequally_directed_lines(L,N)|unequally_directed_lines(M,reverse_line(N))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 238.58/238.80 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:(unequally_directed_lines(L,reverse_line(M))=>(unequally_directed_lines(L,N)|unequally_directed_lines(M,reverse_line(N)))))))),inference(assume_negation,[status(cth)],[con])).
% 238.58/238.80 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:(unequally_directed_lines(L,reverse_line(M))&(~unequally_directed_lines(L,N)&~unequally_directed_lines(M,reverse_line(N))))))),inference(fof_nnf,[status(thm)],[c0])).
% 238.58/238.80 fof(c2,negated_conjecture,(?[L]:(?[M]:(unequally_directed_lines(L,reverse_line(M))&(?[N]:(~unequally_directed_lines(L,N)&~unequally_directed_lines(M,reverse_line(N))))))),inference(shift_quantors,[status(thm)],[c1])).
% 238.58/238.80 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(unequally_directed_lines(X2,reverse_line(X3))&(?[X4]:(~unequally_directed_lines(X2,X4)&~unequally_directed_lines(X3,reverse_line(X4))))))),inference(variable_rename,[status(thm)],[c2])).
% 238.58/238.80 fof(c4,negated_conjecture,(unequally_directed_lines(skolem0001,reverse_line(skolem0002))&(~unequally_directed_lines(skolem0001,skolem0003)&~unequally_directed_lines(skolem0002,reverse_line(skolem0003)))),inference(skolemize,[status(esa)],[c3])).
% 238.58/238.80 cnf(c7,negated_conjecture,~unequally_directed_lines(skolem0002,reverse_line(skolem0003)),inference(split_conjunct,[status(thm)],[c4])).
% 238.58/238.80 fof(oag6,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/GEO007+0.ax', oag6)).
% 238.58/238.80 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])).
% 238.58/238.80 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])).
% 238.58/238.80 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])).])).
% 238.58/238.80 cnf(c92,plain,~unequally_directed_lines(X154,X156)|unequally_directed_lines(X154,X155)|unequally_directed_lines(X156,X155),inference(split_conjunct,[status(thm)],[c91])).
% 238.58/238.80 cnf(c6,negated_conjecture,~unequally_directed_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 238.58/238.80 cnf(c5,negated_conjecture,unequally_directed_lines(skolem0001,reverse_line(skolem0002)),inference(split_conjunct,[status(thm)],[c4])).
% 238.58/238.80 cnf(c163,plain,unequally_directed_lines(skolem0001,X170)|unequally_directed_lines(reverse_line(skolem0002),X170),inference(resolution,[status(thm)],[c92, c5])).
% 238.58/238.80 cnf(c166,plain,unequally_directed_lines(reverse_line(skolem0002),skolem0003),inference(resolution,[status(thm)],[c163, c6])).
% 238.58/238.80 cnf(c171,plain,unequally_directed_lines(reverse_line(skolem0002),X171)|unequally_directed_lines(skolem0003,X171),inference(resolution,[status(thm)],[c166, c92])).
% 238.58/238.80 cnf(c175,plain,unequally_directed_lines(skolem0003,reverse_line(skolem0002)),inference(resolution,[status(thm)],[c171, c95])).
% 238.58/238.80 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/sandbox2/benchmark/Axioms/GEO007+0.ax', oag7)).
% 238.58/238.80 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])).
% 238.58/238.80 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])).
% 238.58/238.80 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])).])).
% 238.58/238.80 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])).
% 238.58/238.80 cnf(c85,plain,~unequally_directed_lines(X241,X243)|~unequally_directed_lines(X241,reverse_line(X243))|unequally_directed_lines(X241,X242)|unequally_directed_lines(X243,reverse_line(X242)),inference(split_conjunct,[status(thm)],[c83])).
% 238.58/238.80 cnf(c249,plain,~unequally_directed_lines(skolem0003,skolem0002)|unequally_directed_lines(skolem0003,X553)|unequally_directed_lines(skolem0002,reverse_line(X553)),inference(resolution,[status(thm)],[c85, c175])).
% 238.58/238.80 cnf(c86,plain,~unequally_directed_lines(X246,X248)|~unequally_directed_lines(X246,reverse_line(X248))|unequally_directed_lines(X246,reverse_line(X247))|unequally_directed_lines(X248,X247),inference(split_conjunct,[status(thm)],[c83])).
% 238.58/238.80 cnf(c168,plain,unequally_directed_lines(skolem0001,X280)|unequally_directed_lines(reverse_line(skolem0002),X279)|unequally_directed_lines(X280,X279),inference(resolution,[status(thm)],[c163, c92])).
% 238.58/238.80 cnf(c368,plain,unequally_directed_lines(skolem0001,skolem0002)|unequally_directed_lines(reverse_line(skolem0002),reverse_line(skolem0003)),inference(resolution,[status(thm)],[c168, c7])).
% 238.58/238.80 cnf(c1216,plain,unequally_directed_lines(skolem0001,skolem0002)|~unequally_directed_lines(reverse_line(skolem0002),skolem0003)|unequally_directed_lines(reverse_line(skolem0002),reverse_line(X6660))|unequally_directed_lines(skolem0003,X6660),inference(resolution,[status(thm)],[c368, c86])).
% 238.58/238.80 cnf(c220213,plain,unequally_directed_lines(skolem0001,skolem0002)|unequally_directed_lines(reverse_line(skolem0002),reverse_line(X6666))|unequally_directed_lines(skolem0003,X6666),inference(resolution,[status(thm)],[c1216, c166])).
% 238.58/238.80 cnf(c222872,plain,unequally_directed_lines(skolem0001,skolem0002)|unequally_directed_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c220213, c95])).
% 238.58/238.80 cnf(c223136,plain,unequally_directed_lines(skolem0003,skolem0002)|unequally_directed_lines(skolem0001,X6667)|unequally_directed_lines(skolem0002,X6667),inference(resolution,[status(thm)],[c222872, c92])).
% 238.58/238.80 cnf(c224212,plain,unequally_directed_lines(skolem0003,skolem0002)|unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c223136, c6])).
% 238.58/238.80 cnf(c225221,plain,unequally_directed_lines(skolem0002,skolem0003)|unequally_directed_lines(skolem0003,X6687)|unequally_directed_lines(skolem0002,X6687),inference(resolution,[status(thm)],[c224212, c92])).
% 238.58/238.80 cnf(c229050,plain,unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c225221, c95])).
% 238.58/238.80 cnf(c229250,plain,unequally_directed_lines(skolem0002,X6688)|unequally_directed_lines(skolem0003,X6688),inference(resolution,[status(thm)],[c229050, c92])).
% 238.58/238.80 cnf(c229323,plain,unequally_directed_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c229250, c95])).
% 238.58/238.80 cnf(c229535,plain,unequally_directed_lines(skolem0003,X6697)|unequally_directed_lines(skolem0002,reverse_line(X6697)),inference(resolution,[status(thm)],[c229323, c249])).
% 238.58/238.80 cnf(c230521,plain,unequally_directed_lines(skolem0003,skolem0003),inference(resolution,[status(thm)],[c229535, c7])).
% 238.58/238.80 cnf(c230589,plain,$false,inference(resolution,[status(thm)],[c230521, c95])).
% 238.58/238.80 % SZS output end CNFRefutation
% 238.58/238.80
% 238.58/238.80 % Initial clauses : 61
% 238.58/238.80 % Processed clauses : 1302
% 238.58/238.80 % Factors computed : 513
% 238.58/238.80 % Resolvents computed: 229945
% 238.58/238.80 % Tautologies deleted: 5
% 238.58/238.80 % Forward subsumed : 3597
% 238.58/238.80 % Backward subsumed : 190
% 238.58/238.80 % -------- CPU Time ---------
% 238.58/238.80 % User time : 237.730 s
% 238.58/238.80 % System time : 0.713 s
% 238.58/238.80 % Total time : 238.443 s
%------------------------------------------------------------------------------