%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO215+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:33 EDT 2024
% Result : Theorem 6.33s 6.54s
% Output : Refutation 6.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO215+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n015.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:59:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 6.33/6.54 % Version: 1.5
% 6.33/6.54 % SZS status Theorem
% 6.33/6.54 % SZS output start CNFRefutation
% 6.33/6.54 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart3)).
% 6.33/6.54 fof(c88,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 6.33/6.54 fof(c89,plain,(![X55]:~convergent_lines(X55,X55)),inference(variable_rename,[status(thm)],[c88])).
% 6.33/6.54 cnf(c90,plain,~convergent_lines(X58,X58),inference(split_conjunct,[status(thm)],[c89])).
% 6.33/6.54 fof(con,conjecture,(![L]:(![M]:(![N]:(convergent_lines(L,M)=>(unorthogonal_lines(L,N)|unorthogonal_lines(M,N)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 6.33/6.54 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:(convergent_lines(L,M)=>(unorthogonal_lines(L,N)|unorthogonal_lines(M,N))))))),inference(assume_negation,[status(cth)],[con])).
% 6.33/6.54 fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:(convergent_lines(L,M)&(~unorthogonal_lines(L,N)&~unorthogonal_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c0])).
% 6.33/6.54 fof(c2,negated_conjecture,(?[L]:(?[M]:(convergent_lines(L,M)&(?[N]:(~unorthogonal_lines(L,N)&~unorthogonal_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c1])).
% 6.33/6.54 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(convergent_lines(X2,X3)&(?[X4]:(~unorthogonal_lines(X2,X4)&~unorthogonal_lines(X3,X4)))))),inference(variable_rename,[status(thm)],[c2])).
% 6.33/6.54 fof(c4,negated_conjecture,(convergent_lines(skolem0001,skolem0002)&(~unorthogonal_lines(skolem0001,skolem0003)&~unorthogonal_lines(skolem0002,skolem0003))),inference(skolemize,[status(esa)],[c3])).
% 6.33/6.54 cnf(c5,negated_conjecture,convergent_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 6.33/6.54 fof(ax6,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ax6)).
% 6.33/6.54 fof(c73,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),inference(fof_nnf,[status(thm)],[ax6])).
% 6.33/6.54 fof(c74,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),inference(shift_quantors,[status(thm)],[c73])).
% 6.33/6.54 fof(c76,plain,(![X46]:(![X47]:(![X48]:(~convergent_lines(X46,X47)|(convergent_lines(X46,X48)|convergent_lines(X47,X48)))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,(![X46]:(![X47]:(~convergent_lines(X46,X47)|(![X48]:(convergent_lines(X46,X48)|convergent_lines(X47,X48)))))),inference(variable_rename,[status(thm)],[c74])).])).
% 6.33/6.54 cnf(c77,plain,~convergent_lines(X127,X126)|convergent_lines(X127,X128)|convergent_lines(X126,X128),inference(split_conjunct,[status(thm)],[c76])).
% 6.33/6.54 cnf(c149,plain,convergent_lines(skolem0001,X129)|convergent_lines(skolem0002,X129),inference(resolution,[status(thm)],[c77, c5])).
% 6.33/6.54 cnf(c158,plain,convergent_lines(skolem0002,skolem0001),inference(resolution,[status(thm)],[c149, c90])).
% 6.33/6.54 fof(ci4,axiom,(![X]:(![Y]:(convergent_lines(X,Y)=>(~apart_point_and_line(intersection_point(X,Y),Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci4)).
% 6.33/6.54 fof(c57,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_simplification,[status(thm)],[ci4])).
% 6.33/6.54 fof(c58,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_nnf,[status(thm)],[c57])).
% 6.33/6.54 fof(c59,plain,(![X38]:(![X39]:(~convergent_lines(X38,X39)|~apart_point_and_line(intersection_point(X38,X39),X39)))),inference(variable_rename,[status(thm)],[c58])).
% 6.33/6.54 cnf(c60,plain,~convergent_lines(X86,X85)|~apart_point_and_line(intersection_point(X86,X85),X85),inference(split_conjunct,[status(thm)],[c59])).
% 6.33/6.54 fof(ci3,axiom,(![X]:(![Y]:(convergent_lines(X,Y)=>(~apart_point_and_line(intersection_point(X,Y),X))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci3)).
% 6.33/6.54 fof(c61,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_simplification,[status(thm)],[ci3])).
% 6.33/6.54 fof(c62,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_nnf,[status(thm)],[c61])).
% 6.33/6.54 fof(c63,plain,(![X40]:(![X41]:(~convergent_lines(X40,X41)|~apart_point_and_line(intersection_point(X40,X41),X40)))),inference(variable_rename,[status(thm)],[c62])).
% 6.33/6.54 cnf(c64,plain,~convergent_lines(X87,X88)|~apart_point_and_line(intersection_point(X87,X88),X87),inference(split_conjunct,[status(thm)],[c63])).
% 6.33/6.54 cnf(c6,negated_conjecture,~unorthogonal_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 6.33/6.54 cnf(c7,negated_conjecture,~unorthogonal_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 6.33/6.54 fof(ouo1,axiom,(![A]:(![L]:(![M]:(![N]:(distinct_lines(L,M)=>(((apart_point_and_line(A,L)|apart_point_and_line(A,M))|unorthogonal_lines(L,N))|unorthogonal_lines(M,N))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 6.33/6.54 fof(c8,plain,(![A]:(![L]:(![M]:(![N]:(~distinct_lines(L,M)|(((apart_point_and_line(A,L)|apart_point_and_line(A,M))|unorthogonal_lines(L,N))|unorthogonal_lines(M,N))))))),inference(fof_nnf,[status(thm)],[ouo1])).
% 6.33/6.54 fof(c9,plain,(![A]:(![L]:(![M]:(~distinct_lines(L,M)|(![N]:(((apart_point_and_line(A,L)|apart_point_and_line(A,M))|unorthogonal_lines(L,N))|unorthogonal_lines(M,N))))))),inference(shift_quantors,[status(thm)],[c8])).
% 6.33/6.54 fof(c11,plain,(![X5]:(![X6]:(![X7]:(![X8]:(~distinct_lines(X6,X7)|(((apart_point_and_line(X5,X6)|apart_point_and_line(X5,X7))|unorthogonal_lines(X6,X8))|unorthogonal_lines(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,(![X5]:(![X6]:(![X7]:(~distinct_lines(X6,X7)|(![X8]:(((apart_point_and_line(X5,X6)|apart_point_and_line(X5,X7))|unorthogonal_lines(X6,X8))|unorthogonal_lines(X7,X8))))))),inference(variable_rename,[status(thm)],[c9])).])).
% 6.33/6.54 cnf(c12,plain,~distinct_lines(X72,X73)|apart_point_and_line(X74,X72)|apart_point_and_line(X74,X73)|unorthogonal_lines(X72,X71)|unorthogonal_lines(X73,X71),inference(split_conjunct,[status(thm)],[c11])).
% 6.33/6.54 fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 6.33/6.54 fof(c39,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 6.33/6.54 fof(c40,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c39])).
% 6.33/6.54 fof(c42,plain,(![X25]:(![X26]:(![X27]:(~convergent_lines(X25,X26)|(distinct_lines(X26,X27)|convergent_lines(X25,X27)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X25]:(![X26]:(~convergent_lines(X25,X26)|(![X27]:(distinct_lines(X26,X27)|convergent_lines(X25,X27)))))),inference(variable_rename,[status(thm)],[c40])).])).
% 6.33/6.54 cnf(c43,plain,~convergent_lines(X97,X98)|distinct_lines(X98,X96)|convergent_lines(X97,X96),inference(split_conjunct,[status(thm)],[c42])).
% 6.33/6.54 cnf(c108,plain,distinct_lines(skolem0002,X99)|convergent_lines(skolem0001,X99),inference(resolution,[status(thm)],[c43, c5])).
% 6.33/6.54 cnf(c116,plain,distinct_lines(skolem0002,skolem0001),inference(resolution,[status(thm)],[c108, c90])).
% 6.33/6.54 cnf(c117,plain,apart_point_and_line(X218,skolem0002)|apart_point_and_line(X218,skolem0001)|unorthogonal_lines(skolem0002,X219)|unorthogonal_lines(skolem0001,X219),inference(resolution,[status(thm)],[c116, c12])).
% 6.33/6.54 cnf(c387,plain,apart_point_and_line(X1994,skolem0002)|apart_point_and_line(X1994,skolem0001)|unorthogonal_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c117, c7])).
% 6.33/6.54 cnf(c9142,plain,apart_point_and_line(X1995,skolem0002)|apart_point_and_line(X1995,skolem0001),inference(resolution,[status(thm)],[c387, c6])).
% 6.33/6.54 cnf(c9144,plain,apart_point_and_line(intersection_point(skolem0002,X2691),skolem0001)|~convergent_lines(skolem0002,X2691),inference(resolution,[status(thm)],[c9142, c64])).
% 6.33/6.54 cnf(c16430,plain,apart_point_and_line(intersection_point(skolem0002,skolem0001),skolem0001),inference(resolution,[status(thm)],[c9144, c158])).
% 6.33/6.54 cnf(c16517,plain,~convergent_lines(skolem0002,skolem0001),inference(resolution,[status(thm)],[c16430, c60])).
% 6.33/6.54 cnf(c16622,plain,$false,inference(resolution,[status(thm)],[c16517, c158])).
% 6.33/6.54 % SZS output end CNFRefutation
% 6.33/6.54
% 6.33/6.54 % Initial clauses : 28
% 6.33/6.54 % Processed clauses : 516
% 6.33/6.54 % Factors computed : 249
% 6.33/6.54 % Resolvents computed: 16386
% 6.33/6.54 % Tautologies deleted: 4
% 6.33/6.54 % Forward subsumed : 1010
% 6.33/6.54 % Backward subsumed : 12
% 6.33/6.54 % -------- CPU Time ---------
% 6.33/6.54 % User time : 6.140 s
% 6.33/6.54 % System time : 0.045 s
% 6.33/6.54 % Total time : 6.185 s
%------------------------------------------------------------------------------