%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO173+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:16 EDT 2024
% Result : Theorem 41.78s 42.00s
% Output : Refutation 41.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO173+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n016.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 9 08:00:53 EDT 2024
% 0.13/0.33 % CPUTime :
% 41.78/42.00 % Version: 1.5
% 41.78/42.00 % SZS status Theorem
% 41.78/42.00 % SZS output start CNFRefutation
% 41.78/42.00 fof(con,conjecture,(![X]:(![Y]:(![U]:(![V]:(((distinct_points(X,Y)&convergent_lines(U,V))&distinct_lines(U,line_connecting(X,Y)))=>(apart_point_and_line(X,U)|apart_point_and_line(Y,U))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 41.78/42.00 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![U]:(![V]:(((distinct_points(X,Y)&convergent_lines(U,V))&distinct_lines(U,line_connecting(X,Y)))=>(apart_point_and_line(X,U)|apart_point_and_line(Y,U)))))))),inference(assume_negation,[status(cth)],[con])).
% 41.78/42.00 fof(c1,negated_conjecture,(?[X]:(?[Y]:(?[U]:(?[V]:(((distinct_points(X,Y)&convergent_lines(U,V))&distinct_lines(U,line_connecting(X,Y)))&(~apart_point_and_line(X,U)&~apart_point_and_line(Y,U))))))),inference(fof_nnf,[status(thm)],[c0])).
% 41.78/42.00 fof(c2,negated_conjecture,(?[X]:(?[Y]:(?[U]:(((distinct_points(X,Y)&(?[V]:convergent_lines(U,V)))&distinct_lines(U,line_connecting(X,Y)))&(~apart_point_and_line(X,U)&~apart_point_and_line(Y,U)))))),inference(shift_quantors,[status(thm)],[c1])).
% 41.78/42.00 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((distinct_points(X2,X3)&(?[X5]:convergent_lines(X4,X5)))&distinct_lines(X4,line_connecting(X2,X3)))&(~apart_point_and_line(X2,X4)&~apart_point_and_line(X3,X4)))))),inference(variable_rename,[status(thm)],[c2])).
% 41.78/42.00 fof(c4,negated_conjecture,(((distinct_points(skolem0001,skolem0002)&convergent_lines(skolem0003,skolem0004))&distinct_lines(skolem0003,line_connecting(skolem0001,skolem0002)))&(~apart_point_and_line(skolem0001,skolem0003)&~apart_point_and_line(skolem0002,skolem0003))),inference(skolemize,[status(esa)],[c3])).
% 41.78/42.00 cnf(c5,negated_conjecture,distinct_points(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 41.78/42.00 fof(ci1,axiom,(![X]:(![Y]:(distinct_points(X,Y)=>(~apart_point_and_line(X,line_connecting(X,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci1)).
% 41.78/42.00 fof(c40,plain,(![X]:(![Y]:(distinct_points(X,Y)=>~apart_point_and_line(X,line_connecting(X,Y))))),inference(fof_simplification,[status(thm)],[ci1])).
% 41.78/42.00 fof(c41,plain,(![X]:(![Y]:(~distinct_points(X,Y)|~apart_point_and_line(X,line_connecting(X,Y))))),inference(fof_nnf,[status(thm)],[c40])).
% 41.78/42.00 fof(c42,plain,(![X25]:(![X26]:(~distinct_points(X25,X26)|~apart_point_and_line(X25,line_connecting(X25,X26))))),inference(variable_rename,[status(thm)],[c41])).
% 41.78/42.00 cnf(c43,plain,~distinct_points(X53,X52)|~apart_point_and_line(X53,line_connecting(X53,X52)),inference(split_conjunct,[status(thm)],[c42])).
% 41.78/42.00 fof(ci2,axiom,(![X]:(![Y]:(distinct_points(X,Y)=>(~apart_point_and_line(Y,line_connecting(X,Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci2)).
% 41.78/42.00 fof(c36,plain,(![X]:(![Y]:(distinct_points(X,Y)=>~apart_point_and_line(Y,line_connecting(X,Y))))),inference(fof_simplification,[status(thm)],[ci2])).
% 41.78/42.00 fof(c37,plain,(![X]:(![Y]:(~distinct_points(X,Y)|~apart_point_and_line(Y,line_connecting(X,Y))))),inference(fof_nnf,[status(thm)],[c36])).
% 41.78/42.00 fof(c38,plain,(![X23]:(![X24]:(~distinct_points(X23,X24)|~apart_point_and_line(X24,line_connecting(X23,X24))))),inference(variable_rename,[status(thm)],[c37])).
% 41.78/42.00 cnf(c39,plain,~distinct_points(X47,X46)|~apart_point_and_line(X46,line_connecting(X47,X46)),inference(split_conjunct,[status(thm)],[c38])).
% 41.78/42.00 cnf(c8,negated_conjecture,~apart_point_and_line(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 41.78/42.00 cnf(c9,negated_conjecture,~apart_point_and_line(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 41.78/42.00 fof(apart1,axiom,(![X]:(~distinct_points(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart1)).
% 41.78/42.00 fof(c65,plain,(![X]:~distinct_points(X,X)),inference(fof_simplification,[status(thm)],[apart1])).
% 41.78/42.00 fof(c66,plain,(![X38]:~distinct_points(X38,X38)),inference(variable_rename,[status(thm)],[c65])).
% 41.78/42.00 cnf(c67,plain,~distinct_points(X41,X41),inference(split_conjunct,[status(thm)],[c66])).
% 41.78/42.00 fof(apart4,axiom,(![X]:(![Y]:(![Z]:(distinct_points(X,Y)=>(distinct_points(X,Z)|distinct_points(Y,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart4)).
% 41.78/42.00 fof(c54,plain,(![X]:(![Y]:(![Z]:(~distinct_points(X,Y)|(distinct_points(X,Z)|distinct_points(Y,Z)))))),inference(fof_nnf,[status(thm)],[apart4])).
% 41.78/42.00 fof(c55,plain,(![X]:(![Y]:(~distinct_points(X,Y)|(![Z]:(distinct_points(X,Z)|distinct_points(Y,Z)))))),inference(shift_quantors,[status(thm)],[c54])).
% 41.78/42.00 fof(c57,plain,(![X33]:(![X34]:(![X35]:(~distinct_points(X33,X34)|(distinct_points(X33,X35)|distinct_points(X34,X35)))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,(![X33]:(![X34]:(~distinct_points(X33,X34)|(![X35]:(distinct_points(X33,X35)|distinct_points(X34,X35)))))),inference(variable_rename,[status(thm)],[c55])).])).
% 41.78/42.00 cnf(c58,plain,~distinct_points(X74,X75)|distinct_points(X74,X76)|distinct_points(X75,X76),inference(split_conjunct,[status(thm)],[c57])).
% 41.78/42.00 cnf(c102,plain,distinct_points(skolem0001,X78)|distinct_points(skolem0002,X78),inference(resolution,[status(thm)],[c58, c5])).
% 41.78/42.00 cnf(c104,plain,distinct_points(skolem0002,skolem0001),inference(resolution,[status(thm)],[c102, c67])).
% 41.78/42.00 cnf(c7,negated_conjecture,distinct_lines(skolem0003,line_connecting(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c4])).
% 41.78/42.00 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/sandbox2/benchmark/Axioms/GEO006+0.ax', cu1)).
% 41.78/42.00 fof(c25,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])).
% 41.78/42.00 fof(c26,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)],[c25])).
% 41.78/42.00 cnf(c27,plain,~distinct_points(X66,X68)|~distinct_lines(X67,X65)|apart_point_and_line(X66,X67)|apart_point_and_line(X66,X65)|apart_point_and_line(X68,X67)|apart_point_and_line(X68,X65),inference(split_conjunct,[status(thm)],[c26])).
% 41.78/42.00 cnf(c82,plain,~distinct_points(X111,X110)|apart_point_and_line(X111,skolem0003)|apart_point_and_line(X111,line_connecting(skolem0001,skolem0002))|apart_point_and_line(X110,skolem0003)|apart_point_and_line(X110,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c27, c7])).
% 41.78/42.00 cnf(c205,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)],[c82, c104])).
% 41.78/42.00 cnf(c1267,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)],[c205, c9])).
% 41.78/42.00 cnf(c42290,plain,apart_point_and_line(skolem0002,line_connecting(skolem0001,skolem0002))|apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1267, c8])).
% 41.78/42.00 cnf(c53752,plain,apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002))|~distinct_points(skolem0001,skolem0002),inference(resolution,[status(thm)],[c42290, c39])).
% 41.78/42.00 cnf(c53813,plain,apart_point_and_line(skolem0001,line_connecting(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53752, c5])).
% 41.78/42.00 cnf(c53941,plain,~distinct_points(skolem0001,skolem0002),inference(resolution,[status(thm)],[c53813, c43])).
% 41.78/42.00 cnf(c53997,plain,$false,inference(resolution,[status(thm)],[c53941, c5])).
% 41.78/42.00 % SZS output end CNFRefutation
% 41.78/42.00
% 41.78/42.00 % Initial clauses : 19
% 41.78/42.00 % Processed clauses : 780
% 41.78/42.00 % Factors computed : 2403
% 41.78/42.00 % Resolvents computed: 51646
% 41.78/42.00 % Tautologies deleted: 1
% 41.78/42.00 % Forward subsumed : 3307
% 41.78/42.00 % Backward subsumed : 116
% 41.78/42.00 % -------- CPU Time ---------
% 41.78/42.00 % User time : 41.442 s
% 41.78/42.00 % System time : 0.193 s
% 41.78/42.00 % Total time : 41.635 s
%------------------------------------------------------------------------------