%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO192+2 : 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:24 EDT 2024
% Result : Theorem 4.67s 4.86s
% Output : Refutation 4.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GEO192+2 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n015.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 07:43:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 4.67/4.86 % Version: 1.5
% 4.67/4.86 % SZS status Theorem
% 4.67/4.86 % SZS output start CNFRefutation
% 4.67/4.86 fof(con,conjecture,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(apart_point_and_line(intersection_point(X,Y),Z)=>(distinct_lines(X,Z)&distinct_lines(Y,Z))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 4.67/4.86 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(apart_point_and_line(intersection_point(X,Y),Z)=>(distinct_lines(X,Z)&distinct_lines(Y,Z)))))))),inference(assume_negation,[status(cth)],[con])).
% 4.67/4.86 fof(c1,negated_conjecture,(?[X]:(?[Y]:(?[Z]:(convergent_lines(X,Y)&(apart_point_and_line(intersection_point(X,Y),Z)&(~distinct_lines(X,Z)|~distinct_lines(Y,Z))))))),inference(fof_nnf,[status(thm)],[c0])).
% 4.67/4.86 fof(c2,negated_conjecture,(?[X]:(?[Y]:(convergent_lines(X,Y)&(?[Z]:(apart_point_and_line(intersection_point(X,Y),Z)&(~distinct_lines(X,Z)|~distinct_lines(Y,Z))))))),inference(shift_quantors,[status(thm)],[c1])).
% 4.67/4.86 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(convergent_lines(X2,X3)&(?[X4]:(apart_point_and_line(intersection_point(X2,X3),X4)&(~distinct_lines(X2,X4)|~distinct_lines(X3,X4))))))),inference(variable_rename,[status(thm)],[c2])).
% 4.67/4.86 fof(c4,negated_conjecture,(convergent_lines(skolem0001,skolem0002)&(apart_point_and_line(intersection_point(skolem0001,skolem0002),skolem0003)&(~distinct_lines(skolem0001,skolem0003)|~distinct_lines(skolem0002,skolem0003)))),inference(skolemize,[status(esa)],[c3])).
% 4.67/4.86 cnf(c7,negated_conjecture,~distinct_lines(skolem0001,skolem0003)|~distinct_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 4.67/4.86 fof(apart2,axiom,(![X]:(~distinct_lines(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart2)).
% 4.67/4.86 fof(c56,plain,(![X]:~distinct_lines(X,X)),inference(fof_simplification,[status(thm)],[apart2])).
% 4.67/4.86 fof(c57,plain,(![X33]:~distinct_lines(X33,X33)),inference(variable_rename,[status(thm)],[c56])).
% 4.67/4.86 cnf(c58,plain,~distinct_lines(X36,X36),inference(split_conjunct,[status(thm)],[c57])).
% 4.67/4.86 fof(apart5,axiom,(![X]:(![Y]:(![Z]:(distinct_lines(X,Y)=>(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart5)).
% 4.67/4.86 fof(c43,plain,(![X]:(![Y]:(![Z]:(~distinct_lines(X,Y)|(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),inference(fof_nnf,[status(thm)],[apart5])).
% 4.67/4.86 fof(c44,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|(![Z]:(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),inference(shift_quantors,[status(thm)],[c43])).
% 4.67/4.86 fof(c46,plain,(![X26]:(![X27]:(![X28]:(~distinct_lines(X26,X27)|(distinct_lines(X26,X28)|distinct_lines(X27,X28)))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,(![X26]:(![X27]:(~distinct_lines(X26,X27)|(![X28]:(distinct_lines(X26,X28)|distinct_lines(X27,X28)))))),inference(variable_rename,[status(thm)],[c44])).])).
% 4.67/4.86 cnf(c47,plain,~distinct_lines(X69,X68)|distinct_lines(X69,X70)|distinct_lines(X68,X70),inference(split_conjunct,[status(thm)],[c46])).
% 4.67/4.86 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart3)).
% 4.67/4.86 fof(c53,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 4.67/4.86 fof(c54,plain,(![X32]:~convergent_lines(X32,X32)),inference(variable_rename,[status(thm)],[c53])).
% 4.67/4.86 cnf(c55,plain,~convergent_lines(X35,X35),inference(split_conjunct,[status(thm)],[c54])).
% 4.67/4.86 fof(apart1,axiom,(![X]:(~distinct_points(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart1)).
% 4.67/4.86 fof(c59,plain,(![X]:~distinct_points(X,X)),inference(fof_simplification,[status(thm)],[apart1])).
% 4.67/4.86 fof(c60,plain,(![X34]:~distinct_points(X34,X34)),inference(variable_rename,[status(thm)],[c59])).
% 4.67/4.86 cnf(c61,plain,~distinct_points(X37,X37),inference(split_conjunct,[status(thm)],[c60])).
% 4.67/4.86 fof(apart6,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart6)).
% 4.67/4.86 fof(c38,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),inference(fof_nnf,[status(thm)],[apart6])).
% 4.67/4.86 fof(c39,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(convergent_lines(X,Z)|convergent_lines(Y,Z)))))),inference(shift_quantors,[status(thm)],[c38])).
% 4.67/4.86 fof(c41,plain,(![X23]:(![X24]:(![X25]:(~convergent_lines(X23,X24)|(convergent_lines(X23,X25)|convergent_lines(X24,X25)))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,(![X23]:(![X24]:(~convergent_lines(X23,X24)|(![X25]:(convergent_lines(X23,X25)|convergent_lines(X24,X25)))))),inference(variable_rename,[status(thm)],[c39])).])).
% 4.67/4.86 cnf(c42,plain,~convergent_lines(X47,X46)|convergent_lines(X47,X48)|convergent_lines(X46,X48),inference(split_conjunct,[status(thm)],[c41])).
% 4.67/4.86 cnf(c5,negated_conjecture,convergent_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 4.67/4.86 cnf(c65,plain,convergent_lines(skolem0001,X53)|convergent_lines(skolem0002,X53),inference(resolution,[status(thm)],[c42, c5])).
% 4.67/4.86 cnf(c68,plain,convergent_lines(skolem0002,X81)|convergent_lines(skolem0001,X82)|convergent_lines(X81,X82),inference(resolution,[status(thm)],[c65, c42])).
% 4.67/4.86 cnf(c122,plain,convergent_lines(skolem0002,X84)|convergent_lines(X84,skolem0001),inference(resolution,[status(thm)],[c68, c55])).
% 4.67/4.86 cnf(c129,plain,convergent_lines(X176,skolem0001)|convergent_lines(skolem0002,X177)|convergent_lines(X176,X177),inference(resolution,[status(thm)],[c122, c42])).
% 4.67/4.86 cnf(c423,plain,convergent_lines(X179,skolem0001)|convergent_lines(X179,skolem0002),inference(resolution,[status(thm)],[c129, c55])).
% 4.67/4.86 fof(con2,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>((apart_point_and_line(Z,X)|apart_point_and_line(Z,Y))=>distinct_points(Z,intersection_point(X,Y))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', con2)).
% 4.67/4.86 fof(c24,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|((~apart_point_and_line(Z,X)&~apart_point_and_line(Z,Y))|distinct_points(Z,intersection_point(X,Y))))))),inference(fof_nnf,[status(thm)],[con2])).
% 4.67/4.86 fof(c25,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:((~apart_point_and_line(Z,X)&~apart_point_and_line(Z,Y))|distinct_points(Z,intersection_point(X,Y))))))),inference(shift_quantors,[status(thm)],[c24])).
% 4.67/4.86 fof(c27,plain,(![X17]:(![X18]:(![X19]:(~convergent_lines(X17,X18)|((~apart_point_and_line(X19,X17)&~apart_point_and_line(X19,X18))|distinct_points(X19,intersection_point(X17,X18))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,(![X17]:(![X18]:(~convergent_lines(X17,X18)|(![X19]:((~apart_point_and_line(X19,X17)&~apart_point_and_line(X19,X18))|distinct_points(X19,intersection_point(X17,X18))))))),inference(variable_rename,[status(thm)],[c25])).])).
% 4.67/4.86 fof(c28,plain,(![X17]:(![X18]:(![X19]:((~convergent_lines(X17,X18)|(~apart_point_and_line(X19,X17)|distinct_points(X19,intersection_point(X17,X18))))&(~convergent_lines(X17,X18)|(~apart_point_and_line(X19,X18)|distinct_points(X19,intersection_point(X17,X18)))))))),inference(distribute,[status(thm)],[c27])).
% 4.67/4.86 cnf(c30,plain,~convergent_lines(X60,X61)|~apart_point_and_line(X59,X61)|distinct_points(X59,intersection_point(X60,X61)),inference(split_conjunct,[status(thm)],[c28])).
% 4.67/4.86 cnf(c6,negated_conjecture,apart_point_and_line(intersection_point(skolem0001,skolem0002),skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 4.67/4.86 fof(ceq2,axiom,(![X]:(![Y]:(![Z]:(apart_point_and_line(X,Y)=>(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', ceq2)).
% 4.67/4.86 fof(c11,plain,(![X]:(![Y]:(![Z]:(~apart_point_and_line(X,Y)|(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq2])).
% 4.67/4.86 fof(c12,plain,(![X]:(![Y]:(~apart_point_and_line(X,Y)|(![Z]:(distinct_lines(Y,Z)|apart_point_and_line(X,Z)))))),inference(shift_quantors,[status(thm)],[c11])).
% 4.67/4.86 fof(c14,plain,(![X7]:(![X8]:(![X9]:(~apart_point_and_line(X7,X8)|(distinct_lines(X8,X9)|apart_point_and_line(X7,X9)))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,(![X7]:(![X8]:(~apart_point_and_line(X7,X8)|(![X9]:(distinct_lines(X8,X9)|apart_point_and_line(X7,X9)))))),inference(variable_rename,[status(thm)],[c12])).])).
% 4.67/4.86 cnf(c15,plain,~apart_point_and_line(X40,X41)|distinct_lines(X41,X42)|apart_point_and_line(X40,X42),inference(split_conjunct,[status(thm)],[c14])).
% 4.67/4.86 cnf(c63,plain,distinct_lines(skolem0003,X79)|apart_point_and_line(intersection_point(skolem0001,skolem0002),X79),inference(resolution,[status(thm)],[c15, c6])).
% 4.67/4.86 cnf(c107,plain,distinct_lines(skolem0003,X180)|~convergent_lines(X181,X180)|distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(X181,X180)),inference(resolution,[status(thm)],[c63, c30])).
% 4.67/4.86 cnf(c439,plain,distinct_lines(skolem0003,skolem0002)|distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(X1491,skolem0002))|convergent_lines(X1491,skolem0001),inference(resolution,[status(thm)],[c107, c423])).
% 4.67/4.86 cnf(c8870,plain,distinct_lines(skolem0003,skolem0002)|convergent_lines(skolem0001,skolem0001),inference(resolution,[status(thm)],[c439, c61])).
% 4.67/4.86 cnf(c8918,plain,distinct_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c8870, c55])).
% 4.67/4.86 cnf(c8919,plain,distinct_lines(skolem0003,X1492)|distinct_lines(skolem0002,X1492),inference(resolution,[status(thm)],[c8918, c47])).
% 4.67/4.86 cnf(c8921,plain,distinct_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c8919, c58])).
% 4.67/4.86 cnf(c8928,plain,~distinct_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c8921, c7])).
% 4.67/4.86 cnf(c29,plain,~convergent_lines(X56,X57)|~apart_point_and_line(X55,X56)|distinct_points(X55,intersection_point(X56,X57)),inference(split_conjunct,[status(thm)],[c28])).
% 4.67/4.86 cnf(c110,plain,distinct_lines(skolem0003,X196)|~convergent_lines(X196,X195)|distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(X196,X195)),inference(resolution,[status(thm)],[c63, c29])).
% 4.67/4.86 cnf(c517,plain,distinct_lines(skolem0003,X1826)|distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(X1826,skolem0002))|convergent_lines(X1826,skolem0001),inference(resolution,[status(thm)],[c110, c423])).
% 4.67/4.86 cnf(c11974,plain,distinct_lines(skolem0003,skolem0001)|convergent_lines(skolem0001,skolem0001),inference(resolution,[status(thm)],[c517, c61])).
% 4.67/4.86 cnf(c12027,plain,distinct_lines(skolem0003,skolem0001),inference(resolution,[status(thm)],[c11974, c55])).
% 4.67/4.86 cnf(c12081,plain,distinct_lines(skolem0003,X1831)|distinct_lines(skolem0001,X1831),inference(resolution,[status(thm)],[c12027, c47])).
% 4.67/4.86 cnf(c12083,plain,distinct_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c12081, c58])).
% 4.67/4.86 cnf(c12092,plain,$false,inference(resolution,[status(thm)],[c12083, c8928])).
% 4.67/4.86 % SZS output end CNFRefutation
% 4.67/4.86
% 4.67/4.86 % Initial clauses : 17
% 4.67/4.86 % Processed clauses : 383
% 4.67/4.86 % Factors computed : 334
% 4.67/4.86 % Resolvents computed: 11697
% 4.67/4.86 % Tautologies deleted: 5
% 4.67/4.86 % Forward subsumed : 1157
% 4.67/4.86 % Backward subsumed : 122
% 4.67/4.86 % -------- CPU Time ---------
% 4.67/4.86 % User time : 4.491 s
% 4.67/4.86 % System time : 0.035 s
% 4.67/4.86 % Total time : 4.526 s
%------------------------------------------------------------------------------