%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO184+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:21 EDT 2024
% Result : Theorem 72.34s 72.56s
% Output : Refutation 72.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO184+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n010.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 08:04:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 72.34/72.56 % Version: 1.5
% 72.34/72.56 % SZS status Theorem
% 72.34/72.56 % SZS output start CNFRefutation
% 72.34/72.56 fof(con,conjecture,(![X]:(![Y]:(![U]:(![V]:((((distinct_points(X,Y)&convergent_lines(U,V))&(~apart_point_and_line(X,U)))&(~apart_point_and_line(Y,U)))=>(~distinct_lines(U,line_connecting(X,Y)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 72.34/72.56 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![U]:(![V]:((((distinct_points(X,Y)&convergent_lines(U,V))&(~apart_point_and_line(X,U)))&(~apart_point_and_line(Y,U)))=>(~distinct_lines(U,line_connecting(X,Y))))))))),inference(assume_negation,[status(cth)],[con])).
% 72.34/72.56 fof(c1,negated_conjecture,(~(![X]:(![Y]:(![U]:(![V]:((((distinct_points(X,Y)&convergent_lines(U,V))&~apart_point_and_line(X,U))&~apart_point_and_line(Y,U))=>~distinct_lines(U,line_connecting(X,Y)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 72.34/72.56 fof(c2,negated_conjecture,(?[X]:(?[Y]:(?[U]:(?[V]:((((distinct_points(X,Y)&convergent_lines(U,V))&~apart_point_and_line(X,U))&~apart_point_and_line(Y,U))&distinct_lines(U,line_connecting(X,Y))))))),inference(fof_nnf,[status(thm)],[c1])).
% 72.34/72.56 fof(c3,negated_conjecture,(?[X]:(?[Y]:(?[U]:((((distinct_points(X,Y)&(?[V]:convergent_lines(U,V)))&~apart_point_and_line(X,U))&~apart_point_and_line(Y,U))&distinct_lines(U,line_connecting(X,Y)))))),inference(shift_quantors,[status(thm)],[c2])).
% 72.34/72.56 fof(c4,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((((distinct_points(X2,X3)&(?[X5]:convergent_lines(X4,X5)))&~apart_point_and_line(X2,X4))&~apart_point_and_line(X3,X4))&distinct_lines(X4,line_connecting(X2,X3)))))),inference(variable_rename,[status(thm)],[c3])).
% 72.34/72.56 fof(c5,negated_conjecture,((((distinct_points(skolem0001,skolem0002)&convergent_lines(skolem0003,skolem0004))&~apart_point_and_line(skolem0001,skolem0003))&~apart_point_and_line(skolem0002,skolem0003))&distinct_lines(skolem0003,line_connecting(skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c4])).
% 72.34/72.56 cnf(c6,negated_conjecture,distinct_points(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c5])).
% 72.34/72.56 fof(ci1,axiom,(![X]:(![Y]:(distinct_points(X,Y)=>(~apart_point_and_line(X,line_connecting(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci1)).
% 72.34/72.56 fof(c41,plain,(![X]:(![Y]:(distinct_points(X,Y)=>~apart_point_and_line(X,line_connecting(X,Y))))),inference(fof_simplification,[status(thm)],[ci1])).
% 72.34/72.56 fof(c42,plain,(![X]:(![Y]:(~distinct_points(X,Y)|~apart_point_and_line(X,line_connecting(X,Y))))),inference(fof_nnf,[status(thm)],[c41])).
% 72.34/72.56 fof(c43,plain,(![X25]:(![X26]:(~distinct_points(X25,X26)|~apart_point_and_line(X25,line_connecting(X25,X26))))),inference(variable_rename,[status(thm)],[c42])).
% 72.34/72.56 cnf(c44,plain,~distinct_points(X52,X53)|~apart_point_and_line(X52,line_connecting(X52,X53)),inference(split_conjunct,[status(thm)],[c43])).
% 72.34/72.56 fof(ci2,axiom,(![X]:(![Y]:(distinct_points(X,Y)=>(~apart_point_and_line(Y,line_connecting(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci2)).
% 72.34/72.56 fof(c37,plain,(![X]:(![Y]:(distinct_points(X,Y)=>~apart_point_and_line(Y,line_connecting(X,Y))))),inference(fof_simplification,[status(thm)],[ci2])).
% 72.34/72.56 fof(c38,plain,(![X]:(![Y]:(~distinct_points(X,Y)|~apart_point_and_line(Y,line_connecting(X,Y))))),inference(fof_nnf,[status(thm)],[c37])).
% 72.34/72.56 fof(c39,plain,(![X23]:(![X24]:(~distinct_points(X23,X24)|~apart_point_and_line(X24,line_connecting(X23,X24))))),inference(variable_rename,[status(thm)],[c38])).
% 72.34/72.56 cnf(c40,plain,~distinct_points(X46,X47)|~apart_point_and_line(X47,line_connecting(X46,X47)),inference(split_conjunct,[status(thm)],[c39])).
% 72.34/72.56 cnf(c8,negated_conjecture,~apart_point_and_line(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 72.34/72.56 cnf(c9,negated_conjecture,~apart_point_and_line(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 72.34/72.56 fof(apart1,axiom,(![X]:(~distinct_points(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart1)).
% 72.34/72.56 fof(c66,plain,(![X]:~distinct_points(X,X)),inference(fof_simplification,[status(thm)],[apart1])).
% 72.34/72.56 fof(c67,plain,(![X38]:~distinct_points(X38,X38)),inference(variable_rename,[status(thm)],[c66])).
% 72.34/72.56 cnf(c68,plain,~distinct_points(X41,X41),inference(split_conjunct,[status(thm)],[c67])).
% 72.34/72.56 fof(apart4,axiom,(![X]:(![Y]:(![Z]:(distinct_points(X,Y)=>(distinct_points(X,Z)|distinct_points(Y,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart4)).
% 72.34/72.56 fof(c55,plain,(![X]:(![Y]:(![Z]:(~distinct_points(X,Y)|(distinct_points(X,Z)|distinct_points(Y,Z)))))),inference(fof_nnf,[status(thm)],[apart4])).
% 72.34/72.56 fof(c56,plain,(![X]:(![Y]:(~distinct_points(X,Y)|(![Z]:(distinct_points(X,Z)|distinct_points(Y,Z)))))),inference(shift_quantors,[status(thm)],[c55])).
% 72.34/72.56 fof(c58,plain,(![X33]:(![X34]:(![X35]:(~distinct_points(X33,X34)|(distinct_points(X33,X35)|distinct_points(X34,X35)))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,(![X33]:(![X34]:(~distinct_points(X33,X34)|(![X35]:(distinct_points(X33,X35)|distinct_points(X34,X35)))))),inference(variable_rename,[status(thm)],[c56])).])).
% 72.34/72.56 cnf(c59,plain,~distinct_points(X75,X76)|distinct_points(X75,X74)|distinct_points(X76,X74),inference(split_conjunct,[status(thm)],[c58])).
% 72.34/72.56 cnf(c103,plain,distinct_points(skolem0001,X78)|distinct_points(skolem0002,X78),inference(resolution,[status(thm)],[c59, c6])).
% 72.34/72.56 cnf(c105,plain,distinct_points(skolem0002,skolem0001),inference(resolution,[status(thm)],[c103, c68])).
% 72.34/72.56 cnf(c10,negated_conjecture,distinct_lines(skolem0003,line_connecting(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c5])).
% 72.34/72.56 fof(cu1,axiom,(![X]:(![Y]:(![U]:(![V]:((distinct_points(X,Y)&distinct_lines(U,V))=>(((apart_point_and_line(X,U)|apart_point_and_line(X,V))|apart_point_and_line(Y,U))|apart_point_and_line(Y,V))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', cu1)).
% 72.34/72.56 fof(c26,plain,(![X]:(![Y]:(![U]:(![V]:((~distinct_points(X,Y)|~distinct_lines(U,V))|(((apart_point_and_line(X,U)|apart_point_and_line(X,V))|apart_point_and_line(Y,U))|apart_point_and_line(Y,V))))))),inference(fof_nnf,[status(thm)],[cu1])).
% 72.34/72.56 fof(c27,plain,(![X15]:(![X16]:(![X17]:(![X18]:((~distinct_points(X15,X16)|~distinct_lines(X17,X18))|(((apart_point_and_line(X15,X17)|apart_point_and_line(X15,X18))|apart_point_and_line(X16,X17))|apart_point_and_line(X16,X18))))))),inference(variable_rename,[status(thm)],[c26])).
% 72.34/72.56 cnf(c28,plain,~distinct_points(X67,X66)|~distinct_lines(X65,X68)|apart_point_and_line(X67,X65)|apart_point_and_line(X67,X68)|apart_point_and_line(X66,X65)|apart_point_and_line(X66,X68),inference(split_conjunct,[status(thm)],[c27])).
% 72.34/72.56 cnf(c85,plain,~distinct_points(X121,X122)|apart_point_and_line(X121,skolem0003)|apart_point_and_line(X121,line_connecting(skolem0001,skolem0002))|apart_point_and_line(X122,skolem0003)|apart_point_and_line(X122,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c28, c10])).
% 72.34/72.56 cnf(c224,plain,apart_point_and_line(skolem0002,skolem0003)|apart_point_and_line(skolem0002,line_connecting(skolem0001,skolem0002))|apart_point_and_line(skolem0001,skolem0003)|apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c85, c105])).
% 72.34/72.56 cnf(c1574,plain,apart_point_and_line(skolem0002,line_connecting(skolem0001,skolem0002))|apart_point_and_line(skolem0001,skolem0003)|apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c224, c9])).
% 72.34/72.56 cnf(c72638,plain,apart_point_and_line(skolem0002,line_connecting(skolem0001,skolem0002))|apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1574, c8])).
% 72.34/72.56 cnf(c72646,plain,apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002))|~distinct_points(skolem0001,skolem0002),inference(resolution,[status(thm)],[c72638, c40])).
% 72.34/72.56 cnf(c72817,plain,apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c72646, c6])).
% 72.34/72.56 cnf(c72938,plain,~distinct_points(skolem0001,skolem0002),inference(resolution,[status(thm)],[c72817, c44])).
% 72.34/72.56 cnf(c72999,plain,$false,inference(resolution,[status(thm)],[c72938, c6])).
% 72.34/72.56 % SZS output end CNFRefutation
% 72.34/72.56
% 72.34/72.56 % Initial clauses : 19
% 72.34/72.56 % Processed clauses : 1012
% 72.34/72.56 % Factors computed : 2895
% 72.34/72.56 % Resolvents computed: 70150
% 72.34/72.56 % Tautologies deleted: 1
% 72.34/72.56 % Forward subsumed : 4258
% 72.34/72.56 % Backward subsumed : 164
% 72.34/72.56 % -------- CPU Time ---------
% 72.34/72.56 % User time : 71.956 s
% 72.34/72.56 % System time : 0.265 s
% 72.34/72.56 % Total time : 72.221 s
%------------------------------------------------------------------------------