%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO192+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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 0.16s 0.55s
% Output : Refutation 0.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : GEO192+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.11 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Thu May 9 08:09:22 EDT 2024
% 0.11/0.30 % CPUTime :
% 0.16/0.55 % Version: 1.5
% 0.16/0.55 % SZS status Theorem
% 0.16/0.55 % SZS output start CNFRefutation
% 0.16/0.55 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/sandbox/benchmark/theBenchmark.p', con)).
% 0.16/0.55 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])).
% 0.16/0.55 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])).
% 0.16/0.55 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])).
% 0.16/0.55 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])).
% 0.16/0.55 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])).
% 0.16/0.55 cnf(c7,negated_conjecture,~distinct_lines(skolem0001,skolem0003)|~distinct_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 0.16/0.55 fof(apart2,axiom,(![X]:(~distinct_lines(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart2)).
% 0.16/0.55 fof(c60,plain,(![X]:~distinct_lines(X,X)),inference(fof_simplification,[status(thm)],[apart2])).
% 0.16/0.55 fof(c61,plain,(![X36]:~distinct_lines(X36,X36)),inference(variable_rename,[status(thm)],[c60])).
% 0.16/0.55 cnf(c62,plain,~distinct_lines(X39,X39),inference(split_conjunct,[status(thm)],[c61])).
% 0.16/0.55 fof(apart5,axiom,(![X]:(![Y]:(![Z]:(distinct_lines(X,Y)=>(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart5)).
% 0.16/0.55 fof(c47,plain,(![X]:(![Y]:(![Z]:(~distinct_lines(X,Y)|(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),inference(fof_nnf,[status(thm)],[apart5])).
% 0.16/0.55 fof(c48,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|(![Z]:(distinct_lines(X,Z)|distinct_lines(Y,Z)))))),inference(shift_quantors,[status(thm)],[c47])).
% 0.16/0.55 fof(c50,plain,(![X29]:(![X30]:(![X31]:(~distinct_lines(X29,X30)|(distinct_lines(X29,X31)|distinct_lines(X30,X31)))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,(![X29]:(![X30]:(~distinct_lines(X29,X30)|(![X31]:(distinct_lines(X29,X31)|distinct_lines(X30,X31)))))),inference(variable_rename,[status(thm)],[c48])).])).
% 0.16/0.55 cnf(c51,plain,~distinct_lines(X69,X71)|distinct_lines(X69,X70)|distinct_lines(X71,X70),inference(split_conjunct,[status(thm)],[c50])).
% 0.16/0.55 cnf(c5,negated_conjecture,convergent_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 0.16/0.55 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)).
% 0.16/0.55 fof(c26,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_simplification,[status(thm)],[ci4])).
% 0.16/0.55 fof(c27,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_nnf,[status(thm)],[c26])).
% 0.16/0.55 fof(c28,plain,(![X18]:(![X19]:(~convergent_lines(X18,X19)|~apart_point_and_line(intersection_point(X18,X19),X19)))),inference(variable_rename,[status(thm)],[c27])).
% 0.16/0.55 cnf(c29,plain,~convergent_lines(X42,X41)|~apart_point_and_line(intersection_point(X42,X41),X41),inference(split_conjunct,[status(thm)],[c28])).
% 0.16/0.55 cnf(c6,negated_conjecture,apart_point_and_line(intersection_point(skolem0001,skolem0002),skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 0.16/0.55 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/sandbox/benchmark/Axioms/GEO006+0.ax', ceq2)).
% 0.16/0.55 fof(c13,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])).
% 0.16/0.55 fof(c14,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)],[c13])).
% 0.16/0.55 fof(c16,plain,(![X8]:(![X9]:(![X10]:(~apart_point_and_line(X8,X9)|(distinct_lines(X9,X10)|apart_point_and_line(X8,X10)))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X8]:(![X9]:(~apart_point_and_line(X8,X9)|(![X10]:(distinct_lines(X9,X10)|apart_point_and_line(X8,X10)))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.16/0.55 cnf(c17,plain,~apart_point_and_line(X53,X54)|distinct_lines(X54,X52)|apart_point_and_line(X53,X52),inference(split_conjunct,[status(thm)],[c16])).
% 0.16/0.55 cnf(c67,plain,distinct_lines(skolem0003,X77)|apart_point_and_line(intersection_point(skolem0001,skolem0002),X77),inference(resolution,[status(thm)],[c17, c6])).
% 0.16/0.55 cnf(c108,plain,distinct_lines(skolem0003,skolem0002)|~convergent_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c67, c29])).
% 0.16/0.55 cnf(c115,plain,distinct_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c108, c5])).
% 0.16/0.55 cnf(c116,plain,distinct_lines(skolem0003,X78)|distinct_lines(skolem0002,X78),inference(resolution,[status(thm)],[c115, c51])).
% 0.16/0.55 cnf(c119,plain,distinct_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c116, c62])).
% 0.16/0.55 cnf(c127,plain,~distinct_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c119, c7])).
% 0.16/0.55 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)).
% 0.16/0.55 fof(c30,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_simplification,[status(thm)],[ci3])).
% 0.16/0.55 fof(c31,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_nnf,[status(thm)],[c30])).
% 0.16/0.55 fof(c32,plain,(![X20]:(![X21]:(~convergent_lines(X20,X21)|~apart_point_and_line(intersection_point(X20,X21),X20)))),inference(variable_rename,[status(thm)],[c31])).
% 0.16/0.55 cnf(c33,plain,~convergent_lines(X44,X43)|~apart_point_and_line(intersection_point(X44,X43),X44),inference(split_conjunct,[status(thm)],[c32])).
% 0.16/0.55 cnf(c112,plain,distinct_lines(skolem0003,skolem0001)|~convergent_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c67, c33])).
% 0.16/0.55 cnf(c274,plain,distinct_lines(skolem0003,skolem0001),inference(resolution,[status(thm)],[c112, c5])).
% 0.16/0.55 cnf(c290,plain,distinct_lines(skolem0003,X134)|distinct_lines(skolem0001,X134),inference(resolution,[status(thm)],[c274, c51])).
% 0.16/0.55 cnf(c312,plain,distinct_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c290, c62])).
% 0.16/0.55 cnf(c320,plain,$false,inference(resolution,[status(thm)],[c312, c127])).
% 0.16/0.55 % SZS output end CNFRefutation
% 0.16/0.55
% 0.16/0.55 % Initial clauses : 17
% 0.16/0.55 % Processed clauses : 60
% 0.16/0.55 % Factors computed : 9
% 0.16/0.55 % Resolvents computed: 258
% 0.16/0.55 % Tautologies deleted: 1
% 0.16/0.55 % Forward subsumed : 53
% 0.16/0.55 % Backward subsumed : 4
% 0.16/0.55 % -------- CPU Time ---------
% 0.16/0.55 % User time : 0.224 s
% 0.16/0.55 % System time : 0.015 s
% 0.16/0.55 % Total time : 0.239 s
%------------------------------------------------------------------------------