%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO220+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:36 EDT 2024
% Result : Theorem 0.48s 0.66s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GEO220+3 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 07:50:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.48/0.66 % Version: 1.5
% 0.48/0.66 % SZS status Theorem
% 0.48/0.66 % SZS output start CNFRefutation
% 0.48/0.66 fof(con,conjecture,(![L]:(![M]:(![N]:((orthogonal_lines(L,M)&orthogonal_lines(L,N))=>parallel_lines(M,N))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 0.48/0.66 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:((orthogonal_lines(L,M)&orthogonal_lines(L,N))=>parallel_lines(M,N)))))),inference(assume_negation,[status(cth)],[con])).
% 0.48/0.66 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:((orthogonal_lines(L,M)&orthogonal_lines(L,N))&~parallel_lines(M,N))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.48/0.66 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((orthogonal_lines(X2,X3)&orthogonal_lines(X2,X4))&~parallel_lines(X3,X4))))),inference(variable_rename,[status(thm)],[c1])).
% 0.48/0.66 fof(c3,negated_conjecture,((orthogonal_lines(skolem0001,skolem0002)&orthogonal_lines(skolem0001,skolem0003))&~parallel_lines(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c2])).
% 0.48/0.66 cnf(c5,negated_conjecture,orthogonal_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.48/0.66 fof(a5,axiom,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>(~unorthogonal_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a5)).
% 0.48/0.66 fof(c7,plain,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>~unorthogonal_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5])).
% 0.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 cnf(c12,plain,~orthogonal_lines(X107,X108)|~unorthogonal_lines(X107,X108),inference(split_conjunct,[status(thm)],[c11])).
% 0.48/0.66 cnf(c4,negated_conjecture,orthogonal_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 0.48/0.66 cnf(c6,negated_conjecture,~parallel_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.48/0.66 fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a3)).
% 0.48/0.66 fof(c21,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 0.48/0.66 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.48/0.66 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.48/0.66 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.48/0.66 cnf(c27,plain,convergent_lines(X123,X124)|parallel_lines(X123,X124),inference(split_conjunct,[status(thm)],[c25])).
% 0.48/0.66 cnf(c170,plain,convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c27, c6])).
% 0.48/0.66 fof(couo1,axiom,(![L]:(![M]:(![N]:(((~unorthogonal_lines(L,M))&(~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', couo1)).
% 0.48/0.66 fof(c54,plain,(![L]:(![M]:(![N]:((~unorthogonal_lines(L,M)&~unorthogonal_lines(L,N))=>~convergent_lines(M,N))))),inference(fof_simplification,[status(thm)],[couo1])).
% 0.48/0.66 fof(c55,plain,(![L]:(![M]:(![N]:((unorthogonal_lines(L,M)|unorthogonal_lines(L,N))|~convergent_lines(M,N))))),inference(fof_nnf,[status(thm)],[c54])).
% 0.48/0.66 fof(c56,plain,(![X33]:(![X34]:(![X35]:((unorthogonal_lines(X33,X34)|unorthogonal_lines(X33,X35))|~convergent_lines(X34,X35))))),inference(variable_rename,[status(thm)],[c55])).
% 0.48/0.66 cnf(c57,plain,unorthogonal_lines(X184,X182)|unorthogonal_lines(X184,X183)|~convergent_lines(X182,X183),inference(split_conjunct,[status(thm)],[c56])).
% 0.48/0.66 cnf(c198,plain,unorthogonal_lines(X216,skolem0002)|unorthogonal_lines(X216,skolem0003),inference(resolution,[status(thm)],[c57, c170])).
% 0.48/0.66 cnf(c233,plain,unorthogonal_lines(X255,skolem0003)|~orthogonal_lines(X255,skolem0002),inference(resolution,[status(thm)],[c198, c12])).
% 0.48/0.66 cnf(c343,plain,unorthogonal_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c233, c4])).
% 0.48/0.66 cnf(c347,plain,~orthogonal_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c343, c12])).
% 0.48/0.66 cnf(c352,plain,$false,inference(resolution,[status(thm)],[c347, c5])).
% 0.48/0.66 % SZS output end CNFRefutation
% 0.48/0.66
% 0.48/0.66 % Initial clauses : 49
% 0.48/0.66 % Processed clauses : 75
% 0.48/0.66 % Factors computed : 0
% 0.48/0.66 % Resolvents computed: 191
% 0.48/0.66 % Tautologies deleted: 5
% 0.48/0.66 % Forward subsumed : 25
% 0.48/0.66 % Backward subsumed : 0
% 0.48/0.66 % -------- CPU Time ---------
% 0.48/0.66 % User time : 0.264 s
% 0.48/0.66 % System time : 0.020 s
% 0.48/0.66 % Total time : 0.284 s
%------------------------------------------------------------------------------