%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO233+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 18.08s 18.28s
% Output : Refutation 18.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO233+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n009.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 07:43:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 18.08/18.28 % Version: 1.5
% 18.08/18.28 % SZS status Theorem
% 18.08/18.28 % SZS output start CNFRefutation
% 18.08/18.28 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)).
% 18.08/18.28 fof(c154,plain,(![X]:(![Y]:(equally_directed_opposite_lines(X,Y)<=>~unequally_directed_opposite_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5_defns])).
% 18.08/18.28 fof(c155,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)],[c154])).
% 18.08/18.28 fof(c156,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)],[c155])).
% 18.08/18.28 fof(c158,plain,(![X92]:(![X93]:(![X94]:(![X95]:((~equally_directed_opposite_lines(X92,X93)|~unequally_directed_opposite_lines(X92,X93))&(unequally_directed_opposite_lines(X94,X95)|equally_directed_opposite_lines(X94,X95))))))),inference(shift_quantors,[status(thm)],[fof(c157,plain,((![X92]:(![X93]:(~equally_directed_opposite_lines(X92,X93)|~unequally_directed_opposite_lines(X92,X93))))&(![X94]:(![X95]:(unequally_directed_opposite_lines(X94,X95)|equally_directed_opposite_lines(X94,X95))))),inference(variable_rename,[status(thm)],[c156])).])).
% 18.08/18.28 cnf(c159,plain,~equally_directed_opposite_lines(X143,X144)|~unequally_directed_opposite_lines(X143,X144),inference(split_conjunct,[status(thm)],[c158])).
% 18.08/18.28 fof(con,conjecture,(![L]:equally_directed_lines(reverse_line(reverse_line(L)),L)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 18.08/18.28 fof(c0,negated_conjecture,(~(![L]:equally_directed_lines(reverse_line(reverse_line(L)),L))),inference(assume_negation,[status(cth)],[con])).
% 18.08/18.28 fof(c1,negated_conjecture,(?[L]:~equally_directed_lines(reverse_line(reverse_line(L)),L)),inference(fof_nnf,[status(thm)],[c0])).
% 18.08/18.28 fof(c2,negated_conjecture,(?[X2]:~equally_directed_lines(reverse_line(reverse_line(X2)),X2)),inference(variable_rename,[status(thm)],[c1])).
% 18.08/18.28 fof(c3,negated_conjecture,~equally_directed_lines(reverse_line(reverse_line(skolem0001)),skolem0001),inference(skolemize,[status(esa)],[c2])).
% 18.08/18.28 cnf(c4,negated_conjecture,~equally_directed_lines(reverse_line(reverse_line(skolem0001)),skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 18.08/18.28 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)).
% 18.08/18.28 fof(c180,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])).
% 18.08/18.28 fof(c181,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)],[c180])).
% 18.08/18.28 fof(c183,plain,(![X108]:(![X109]:(![X110]:(![X111]:((~unequally_directed_opposite_lines(X108,X109)|unequally_directed_lines(X108,reverse_line(X109)))&(~unequally_directed_lines(X110,reverse_line(X111))|unequally_directed_opposite_lines(X110,X111))))))),inference(shift_quantors,[status(thm)],[fof(c182,plain,((![X108]:(![X109]:(~unequally_directed_opposite_lines(X108,X109)|unequally_directed_lines(X108,reverse_line(X109)))))&(![X110]:(![X111]:(~unequally_directed_lines(X110,reverse_line(X111))|unequally_directed_opposite_lines(X110,X111))))),inference(variable_rename,[status(thm)],[c181])).])).
% 18.08/18.28 cnf(c185,plain,~unequally_directed_lines(X186,reverse_line(X187))|unequally_directed_opposite_lines(X186,X187),inference(split_conjunct,[status(thm)],[c183])).
% 18.08/18.28 fof(ax5_basics,axiom,(![L]:equally_directed_lines(L,L)),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax5_basics)).
% 18.08/18.28 fof(c88,plain,(![X55]:equally_directed_lines(X55,X55)),inference(variable_rename,[status(thm)],[ax5_basics])).
% 18.08/18.28 cnf(c89,plain,equally_directed_lines(X116,X116),inference(split_conjunct,[status(thm)],[c88])).
% 18.08/18.28 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)).
% 18.08/18.28 fof(c161,plain,(![X]:(![Y]:(equally_directed_lines(X,Y)<=>~unequally_directed_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a4_defns])).
% 18.08/18.28 fof(c162,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)],[c161])).
% 18.08/18.28 fof(c163,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)],[c162])).
% 18.08/18.28 fof(c165,plain,(![X96]:(![X97]:(![X98]:(![X99]:((~equally_directed_lines(X96,X97)|~unequally_directed_lines(X96,X97))&(unequally_directed_lines(X98,X99)|equally_directed_lines(X98,X99))))))),inference(shift_quantors,[status(thm)],[fof(c164,plain,((![X96]:(![X97]:(~equally_directed_lines(X96,X97)|~unequally_directed_lines(X96,X97))))&(![X98]:(![X99]:(unequally_directed_lines(X98,X99)|equally_directed_lines(X98,X99))))),inference(variable_rename,[status(thm)],[c163])).])).
% 18.08/18.28 cnf(c166,plain,~equally_directed_lines(X148,X147)|~unequally_directed_lines(X148,X147),inference(split_conjunct,[status(thm)],[c165])).
% 18.08/18.28 cnf(c167,plain,unequally_directed_lines(X150,X149)|equally_directed_lines(X150,X149),inference(split_conjunct,[status(thm)],[c165])).
% 18.08/18.28 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)).
% 18.08/18.28 fof(c83,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])).
% 18.08/18.28 fof(c84,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c83])).
% 18.08/18.28 fof(c86,plain,(![X52]:(![X53]:(![X54]:(~unequally_directed_lines(X52,X53)|(unequally_directed_lines(X52,X54)|unequally_directed_lines(X53,X54)))))),inference(shift_quantors,[status(thm)],[fof(c85,plain,(![X52]:(![X53]:(~unequally_directed_lines(X52,X53)|(![X54]:(unequally_directed_lines(X52,X54)|unequally_directed_lines(X53,X54)))))),inference(variable_rename,[status(thm)],[c84])).])).
% 18.08/18.28 cnf(c87,plain,~unequally_directed_lines(X329,X330)|unequally_directed_lines(X329,X328)|unequally_directed_lines(X330,X328),inference(split_conjunct,[status(thm)],[c86])).
% 18.08/18.28 cnf(c319,plain,unequally_directed_lines(X451,X450)|unequally_directed_lines(X452,X450)|equally_directed_lines(X451,X452),inference(resolution,[status(thm)],[c87, c167])).
% 18.08/18.28 cnf(c403,plain,unequally_directed_lines(X524,X525)|equally_directed_lines(X526,X524)|~equally_directed_lines(X526,X525),inference(resolution,[status(thm)],[c319, c166])).
% 18.08/18.28 cnf(c526,plain,unequally_directed_lines(X528,X527)|equally_directed_lines(X527,X528),inference(resolution,[status(thm)],[c403, c89])).
% 18.08/18.28 cnf(c530,plain,equally_directed_lines(reverse_line(X628),X629)|unequally_directed_opposite_lines(X629,X628),inference(resolution,[status(thm)],[c526, c185])).
% 18.08/18.28 cnf(c784,plain,unequally_directed_opposite_lines(skolem0001,reverse_line(skolem0001)),inference(resolution,[status(thm)],[c530, c4])).
% 18.08/18.28 cnf(c813,plain,~equally_directed_opposite_lines(skolem0001,reverse_line(skolem0001)),inference(resolution,[status(thm)],[c784, c159])).
% 18.08/18.28 cnf(c184,plain,~unequally_directed_opposite_lines(X181,X180)|unequally_directed_lines(X181,reverse_line(X180)),inference(split_conjunct,[status(thm)],[c183])).
% 18.08/18.28 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)).
% 18.08/18.28 fof(c72,plain,(![X47]:(![X48]:(unequally_directed_lines(X47,X48)|unequally_directed_lines(X47,reverse_line(X48))))),inference(variable_rename,[status(thm)],[ax8_basics])).
% 18.08/18.28 cnf(c73,plain,unequally_directed_lines(X167,X168)|unequally_directed_lines(X167,reverse_line(X168)),inference(split_conjunct,[status(thm)],[c72])).
% 18.08/18.28 cnf(c192,plain,unequally_directed_opposite_lines(X188,X189)|unequally_directed_lines(X188,X189),inference(resolution,[status(thm)],[c185, c73])).
% 18.08/18.28 cnf(c197,plain,unequally_directed_opposite_lines(X193,X192)|~equally_directed_lines(X193,X192),inference(resolution,[status(thm)],[c192, c166])).
% 18.08/18.28 cnf(c200,plain,unequally_directed_opposite_lines(X194,X194),inference(resolution,[status(thm)],[c197, c89])).
% 18.08/18.28 cnf(c204,plain,unequally_directed_lines(X199,reverse_line(X199)),inference(resolution,[status(thm)],[c200, c184])).
% 18.08/18.28 cnf(c206,plain,~equally_directed_lines(X201,reverse_line(X201)),inference(resolution,[status(thm)],[c204, c166])).
% 18.08/18.28 fof(ax11_basics,axiom,(![L]:(![M]:(~(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax11_basics)).
% 18.08/18.28 fof(c57,plain,(![L]:(![M]:(~left_convergent_lines(L,M)&~left_convergent_lines(L,reverse_line(M))))),inference(fof_nnf,[status(thm)],[ax11_basics])).
% 18.08/18.28 fof(c58,plain,((![L]:(![M]:~left_convergent_lines(L,M)))&(![L]:(![M]:~left_convergent_lines(L,reverse_line(M))))),inference(shift_quantors,[status(thm)],[c57])).
% 18.08/18.28 fof(c60,plain,(![X37]:(![X38]:(![X39]:(![X40]:(~left_convergent_lines(X37,X38)&~left_convergent_lines(X39,reverse_line(X40))))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X37]:(![X38]:~left_convergent_lines(X37,X38)))&(![X39]:(![X40]:~left_convergent_lines(X39,reverse_line(X40))))),inference(variable_rename,[status(thm)],[c58])).])).
% 18.08/18.28 cnf(c61,plain,~left_convergent_lines(X112,X113),inference(split_conjunct,[status(thm)],[c60])).
% 18.08/18.28 cnf(c160,plain,unequally_directed_opposite_lines(X146,X145)|equally_directed_opposite_lines(X146,X145),inference(split_conjunct,[status(thm)],[c158])).
% 18.08/18.28 cnf(c191,plain,unequally_directed_lines(X251,reverse_line(X250))|equally_directed_opposite_lines(X251,X250),inference(resolution,[status(thm)],[c184, c160])).
% 18.08/18.28 fof(ax9_basics,axiom,(![L]:(![M]:((unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M)))=>(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax9_basics)).
% 18.08/18.28 fof(c69,plain,(![L]:(![M]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),inference(fof_nnf,[status(thm)],[ax9_basics])).
% 18.08/18.28 fof(c70,plain,(![X45]:(![X46]:((~unequally_directed_lines(X45,X46)|~unequally_directed_lines(X45,reverse_line(X46)))|(left_convergent_lines(X45,X46)|left_convergent_lines(X45,reverse_line(X46)))))),inference(variable_rename,[status(thm)],[c69])).
% 18.08/18.28 cnf(c71,plain,~unequally_directed_lines(X273,X274)|~unequally_directed_lines(X273,reverse_line(X274))|left_convergent_lines(X273,X274)|left_convergent_lines(X273,reverse_line(X274)),inference(split_conjunct,[status(thm)],[c70])).
% 18.08/18.28 cnf(c261,plain,~unequally_directed_lines(X646,X647)|left_convergent_lines(X646,X647)|left_convergent_lines(X646,reverse_line(X647))|equally_directed_opposite_lines(X646,X647),inference(resolution,[status(thm)],[c71, c191])).
% 18.08/18.28 cnf(c943,plain,left_convergent_lines(X7231,X7232)|left_convergent_lines(X7231,reverse_line(X7232))|equally_directed_opposite_lines(X7231,X7232)|equally_directed_lines(X7231,X7232),inference(resolution,[status(thm)],[c261, c167])).
% 18.08/18.28 cnf(c35023,plain,left_convergent_lines(X7236,X7237)|equally_directed_opposite_lines(X7236,X7237)|equally_directed_lines(X7236,X7237),inference(resolution,[status(thm)],[c943, c61])).
% 18.08/18.28 cnf(c35235,plain,equally_directed_opposite_lines(X7238,X7239)|equally_directed_lines(X7238,X7239),inference(resolution,[status(thm)],[c35023, c61])).
% 18.08/18.28 cnf(c35565,plain,equally_directed_opposite_lines(X7241,reverse_line(X7241)),inference(resolution,[status(thm)],[c35235, c206])).
% 18.08/18.28 cnf(c35663,plain,$false,inference(resolution,[status(thm)],[c35565, c813])).
% 18.08/18.28 % SZS output end CNFRefutation
% 18.08/18.28
% 18.08/18.28 % Initial clauses : 67
% 18.08/18.28 % Processed clauses : 758
% 18.08/18.28 % Factors computed : 118
% 18.08/18.28 % Resolvents computed: 35622
% 18.08/18.28 % Tautologies deleted: 8
% 18.08/18.28 % Forward subsumed : 2234
% 18.08/18.28 % Backward subsumed : 13
% 18.08/18.28 % -------- CPU Time ---------
% 18.08/18.28 % User time : 17.842 s
% 18.08/18.28 % System time : 0.084 s
% 18.08/18.28 % Total time : 17.926 s
%------------------------------------------------------------------------------