%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO218+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:34 EDT 2024
% Result : Theorem 0.66s 0.91s
% Output : Refutation 0.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO218+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n008.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.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:06:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.66/0.91 % Version: 1.5
% 0.66/0.91 % SZS status Theorem
% 0.66/0.91 % SZS output start CNFRefutation
% 0.66/0.91 fof(con,conjecture,(![L]:(![M]:(![N]:((parallel_lines(L,M)&orthogonal_lines(L,N))=>orthogonal_lines(M,N))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 0.66/0.91 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:((parallel_lines(L,M)&orthogonal_lines(L,N))=>orthogonal_lines(M,N)))))),inference(assume_negation,[status(cth)],[con])).
% 0.66/0.91 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:((parallel_lines(L,M)&orthogonal_lines(L,N))&~orthogonal_lines(M,N))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.66/0.91 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((parallel_lines(X2,X3)&orthogonal_lines(X2,X4))&~orthogonal_lines(X3,X4))))),inference(variable_rename,[status(thm)],[c1])).
% 0.66/0.91 fof(c3,negated_conjecture,((parallel_lines(skolem0001,skolem0002)&orthogonal_lines(skolem0001,skolem0003))&~orthogonal_lines(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c2])).
% 0.66/0.91 cnf(c5,negated_conjecture,orthogonal_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.66/0.91 fof(a5,axiom,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>(~unorthogonal_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a5)).
% 0.66/0.91 fof(c7,plain,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>~unorthogonal_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5])).
% 0.66/0.91 fof(c8,plain,(![X]:(![Y]:((~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))&(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.66/0.91 fof(c9,plain,((![X]:(![Y]:(~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))))&(![X]:(![Y]:(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.66/0.91 fof(c11,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))&(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,((![X5]:(![X6]:(~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))))&(![X7]:(![X8]:(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.66/0.91 cnf(c12,plain,~orthogonal_lines(X108,X107)|~unorthogonal_lines(X108,X107),inference(split_conjunct,[status(thm)],[c11])).
% 0.66/0.91 cnf(c4,negated_conjecture,parallel_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 0.66/0.91 fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a3)).
% 0.66/0.91 fof(c21,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 0.66/0.91 fof(c22,plain,(![X]:(![Y]:((~parallel_lines(X,Y)|~convergent_lines(X,Y))&(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c21])).
% 0.66/0.91 fof(c23,plain,((![X]:(![Y]:(~parallel_lines(X,Y)|~convergent_lines(X,Y))))&(![X]:(![Y]:(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.66/0.91 fof(c25,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~parallel_lines(X13,X14)|~convergent_lines(X13,X14))&(convergent_lines(X15,X16)|parallel_lines(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X13]:(![X14]:(~parallel_lines(X13,X14)|~convergent_lines(X13,X14))))&(![X15]:(![X16]:(convergent_lines(X15,X16)|parallel_lines(X15,X16))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.66/0.91 cnf(c26,plain,~parallel_lines(X117,X118)|~convergent_lines(X117,X118),inference(split_conjunct,[status(thm)],[c25])).
% 0.66/0.91 fof(p1,axiom,(![X]:(![Y]:(distinct_lines(X,Y)=>convergent_lines(X,Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+1.ax', p1)).
% 0.66/0.91 fof(c101,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|convergent_lines(X,Y)))),inference(fof_nnf,[status(thm)],[p1])).
% 0.66/0.91 fof(c102,plain,(![X61]:(![X62]:(~distinct_lines(X61,X62)|convergent_lines(X61,X62)))),inference(variable_rename,[status(thm)],[c101])).
% 0.66/0.91 cnf(c103,plain,~distinct_lines(X164,X163)|convergent_lines(X164,X163),inference(split_conjunct,[status(thm)],[c102])).
% 0.66/0.91 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart3)).
% 0.66/0.91 fof(c153,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 0.66/0.91 fof(c154,plain,(![X93]:~convergent_lines(X93,X93)),inference(variable_rename,[status(thm)],[c153])).
% 0.66/0.91 cnf(c155,plain,~convergent_lines(X96,X96),inference(split_conjunct,[status(thm)],[c154])).
% 0.66/0.91 fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 0.66/0.91 fof(c104,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 0.66/0.91 fof(c105,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c104])).
% 0.66/0.91 fof(c107,plain,(![X63]:(![X64]:(![X65]:(~convergent_lines(X63,X64)|(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X63]:(![X64]:(~convergent_lines(X63,X64)|(![X65]:(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(variable_rename,[status(thm)],[c105])).])).
% 0.66/0.91 cnf(c108,plain,~convergent_lines(X301,X300)|distinct_lines(X300,X302)|convergent_lines(X301,X302),inference(split_conjunct,[status(thm)],[c107])).
% 0.66/0.91 fof(coipo1,axiom,(![L]:(![M]:(~((~convergent_lines(L,M))&(~unorthogonal_lines(L,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', coipo1)).
% 0.66/0.91 fof(c66,plain,(![L]:(![M]:(~(~convergent_lines(L,M)&~unorthogonal_lines(L,M))))),inference(fof_simplification,[status(thm)],[coipo1])).
% 0.66/0.91 fof(c67,plain,(![L]:(![M]:(convergent_lines(L,M)|unorthogonal_lines(L,M)))),inference(fof_nnf,[status(thm)],[c66])).
% 0.66/0.91 fof(c68,plain,(![X39]:(![X40]:(convergent_lines(X39,X40)|unorthogonal_lines(X39,X40)))),inference(variable_rename,[status(thm)],[c67])).
% 0.66/0.91 cnf(c69,plain,convergent_lines(X141,X140)|unorthogonal_lines(X141,X140),inference(split_conjunct,[status(thm)],[c68])).
% 0.66/0.91 cnf(c180,plain,convergent_lines(X186,X185)|~orthogonal_lines(X186,X185),inference(resolution,[status(thm)],[c69, c12])).
% 0.66/0.91 cnf(c203,plain,convergent_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c180, c5])).
% 0.66/0.91 cnf(c359,plain,distinct_lines(skolem0003,X303)|convergent_lines(skolem0001,X303),inference(resolution,[status(thm)],[c108, c203])).
% 0.66/0.91 cnf(c370,plain,distinct_lines(skolem0003,X312)|~parallel_lines(skolem0001,X312),inference(resolution,[status(thm)],[c359, c26])).
% 0.66/0.91 cnf(c403,plain,distinct_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c370, c4])).
% 0.66/0.91 cnf(c411,plain,convergent_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c403, c103])).
% 0.66/0.91 cnf(c417,plain,distinct_lines(skolem0002,X337)|convergent_lines(skolem0003,X337),inference(resolution,[status(thm)],[c411, c108])).
% 0.66/0.91 cnf(c473,plain,distinct_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c417, c155])).
% 0.66/0.91 cnf(c482,plain,convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c473, c103])).
% 0.66/0.91 cnf(c6,negated_conjecture,~orthogonal_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.66/0.91 cnf(c13,plain,unorthogonal_lines(X109,X110)|orthogonal_lines(X109,X110),inference(split_conjunct,[status(thm)],[c11])).
% 0.66/0.91 cnf(c164,plain,unorthogonal_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c13, c6])).
% 0.66/0.91 fof(cotno1,axiom,(![L]:(![M]:(![N]:((((~convergent_lines(L,M))|(~unorthogonal_lines(L,M)))&((~convergent_lines(L,N))|(~unorthogonal_lines(L,N))))=>((~convergent_lines(M,N))|(~unorthogonal_lines(M,N))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 0.66/0.91 fof(c58,plain,(![L]:(![M]:(![N]:(((~convergent_lines(L,M)|~unorthogonal_lines(L,M))&(~convergent_lines(L,N)|~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_simplification,[status(thm)],[cotno1])).
% 0.66/0.91 fof(c59,plain,(![L]:(![M]:(![N]:(((convergent_lines(L,M)&unorthogonal_lines(L,M))|(convergent_lines(L,N)&unorthogonal_lines(L,N)))|(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c58])).
% 0.66/0.91 fof(c60,plain,(![X36]:(![X37]:(![X38]:(((convergent_lines(X36,X37)&unorthogonal_lines(X36,X37))|(convergent_lines(X36,X38)&unorthogonal_lines(X36,X38)))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))),inference(variable_rename,[status(thm)],[c59])).
% 0.66/0.91 fof(c61,plain,(![X36]:(![X37]:(![X38]:((((convergent_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((convergent_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38))))&(((unorthogonal_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((unorthogonal_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))))),inference(distribute,[status(thm)],[c60])).
% 0.66/0.91 cnf(c63,plain,convergent_lines(X197,X195)|unorthogonal_lines(X197,X196)|~convergent_lines(X195,X196)|~unorthogonal_lines(X195,X196),inference(split_conjunct,[status(thm)],[c61])).
% 0.66/0.91 cnf(c221,plain,convergent_lines(X416,skolem0002)|unorthogonal_lines(X416,skolem0003)|~convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c63, c164])).
% 0.66/0.91 cnf(c718,plain,convergent_lines(X469,skolem0002)|unorthogonal_lines(X469,skolem0003),inference(resolution,[status(thm)],[c221, c482])).
% 0.66/0.91 cnf(c848,plain,unorthogonal_lines(X505,skolem0003)|~parallel_lines(X505,skolem0002),inference(resolution,[status(thm)],[c718, c26])).
% 0.66/0.91 cnf(c1019,plain,unorthogonal_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c848, c4])).
% 0.66/0.91 cnf(c1021,plain,~orthogonal_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1019, c12])).
% 0.66/0.91 cnf(c1047,plain,$false,inference(resolution,[status(thm)],[c1021, c5])).
% 0.66/0.91 % SZS output end CNFRefutation
% 0.66/0.91
% 0.66/0.91 % Initial clauses : 49
% 0.66/0.91 % Processed clauses : 187
% 0.66/0.91 % Factors computed : 9
% 0.66/0.91 % Resolvents computed: 877
% 0.66/0.91 % Tautologies deleted: 8
% 0.66/0.91 % Forward subsumed : 154
% 0.66/0.91 % Backward subsumed : 4
% 0.66/0.91 % -------- CPU Time ---------
% 0.66/0.91 % User time : 0.543 s
% 0.66/0.91 % System time : 0.017 s
% 0.66/0.91 % Total time : 0.560 s
%------------------------------------------------------------------------------