%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO226+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:38 EDT 2024
% Result : Theorem 3.44s 3.59s
% Output : Refutation 3.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GEO226+2 : TPTP v8.1.2. Released v3.3.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n025.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 07:49:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.44/3.59 % Version: 1.5
% 3.44/3.59 % SZS status Theorem
% 3.44/3.59 % SZS output start CNFRefutation
% 3.44/3.59 fof(apart1,axiom,(![X]:(~distinct_points(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart1)).
% 3.44/3.59 fof(c75,plain,(![X]:~distinct_points(X,X)),inference(fof_simplification,[status(thm)],[apart1])).
% 3.44/3.59 fof(c76,plain,(![X43]:~distinct_points(X43,X43)),inference(variable_rename,[status(thm)],[c75])).
% 3.44/3.59 cnf(c77,plain,~distinct_points(X47,X47),inference(split_conjunct,[status(thm)],[c76])).
% 3.44/3.59 fof(con,conjecture,(![L]:(![M]:(((line(L)&line(M))&convergent_lines(L,M))=>(?[X]:(point(X)=>((~apart_point_and_line(X,L))&(~apart_point_and_line(X,M)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 3.44/3.59 fof(c0,negated_conjecture,(~(![L]:(![M]:(((line(L)&line(M))&convergent_lines(L,M))=>(?[X]:(point(X)=>((~apart_point_and_line(X,L))&(~apart_point_and_line(X,M))))))))),inference(assume_negation,[status(cth)],[con])).
% 3.44/3.59 fof(c1,negated_conjecture,(~(![L]:(![M]:(((line(L)&line(M))&convergent_lines(L,M))=>(?[X]:(point(X)=>(~apart_point_and_line(X,L)&~apart_point_and_line(X,M)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 3.44/3.59 fof(c2,negated_conjecture,(?[L]:(?[M]:(((line(L)&line(M))&convergent_lines(L,M))&(![X]:(point(X)&(apart_point_and_line(X,L)|apart_point_and_line(X,M))))))),inference(fof_nnf,[status(thm)],[c1])).
% 3.44/3.59 fof(c3,negated_conjecture,(?[L]:(?[M]:(((line(L)&line(M))&convergent_lines(L,M))&((![X]:point(X))&(![X]:(apart_point_and_line(X,L)|apart_point_and_line(X,M))))))),inference(shift_quantors,[status(thm)],[c2])).
% 3.44/3.59 fof(c4,negated_conjecture,(?[X2]:(?[X3]:(((line(X2)&line(X3))&convergent_lines(X2,X3))&((![X4]:point(X4))&(![X5]:(apart_point_and_line(X5,X2)|apart_point_and_line(X5,X3))))))),inference(variable_rename,[status(thm)],[c3])).
% 3.44/3.59 fof(c6,negated_conjecture,(![X4]:(![X5]:(((line(skolem0001)&line(skolem0002))&convergent_lines(skolem0001,skolem0002))&(point(X4)&(apart_point_and_line(X5,skolem0001)|apart_point_and_line(X5,skolem0002)))))),inference(shift_quantors,[status(thm)],[fof(c5,negated_conjecture,(((line(skolem0001)&line(skolem0002))&convergent_lines(skolem0001,skolem0002))&((![X4]:point(X4))&(![X5]:(apart_point_and_line(X5,skolem0001)|apart_point_and_line(X5,skolem0002))))),inference(skolemize,[status(esa)],[c4])).])).
% 3.44/3.59 cnf(c9,negated_conjecture,convergent_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c6])).
% 3.44/3.59 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)).
% 3.44/3.59 fof(c40,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])).
% 3.44/3.59 fof(c41,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)],[c40])).
% 3.44/3.59 fof(c43,plain,(![X26]:(![X27]:(![X28]:(~convergent_lines(X26,X27)|((~apart_point_and_line(X28,X26)&~apart_point_and_line(X28,X27))|distinct_points(X28,intersection_point(X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,(![X26]:(![X27]:(~convergent_lines(X26,X27)|(![X28]:((~apart_point_and_line(X28,X26)&~apart_point_and_line(X28,X27))|distinct_points(X28,intersection_point(X26,X27))))))),inference(variable_rename,[status(thm)],[c41])).])).
% 3.44/3.59 fof(c44,plain,(![X26]:(![X27]:(![X28]:((~convergent_lines(X26,X27)|(~apart_point_and_line(X28,X26)|distinct_points(X28,intersection_point(X26,X27))))&(~convergent_lines(X26,X27)|(~apart_point_and_line(X28,X27)|distinct_points(X28,intersection_point(X26,X27)))))))),inference(distribute,[status(thm)],[c43])).
% 3.44/3.59 cnf(c46,plain,~convergent_lines(X106,X104)|~apart_point_and_line(X105,X104)|distinct_points(X105,intersection_point(X106,X104)),inference(split_conjunct,[status(thm)],[c44])).
% 3.44/3.59 cnf(c11,negated_conjecture,apart_point_and_line(X50,skolem0001)|apart_point_and_line(X50,skolem0002),inference(split_conjunct,[status(thm)],[c6])).
% 3.44/3.59 cnf(c45,plain,~convergent_lines(X101,X99)|~apart_point_and_line(X100,X101)|distinct_points(X100,intersection_point(X101,X99)),inference(split_conjunct,[status(thm)],[c44])).
% 3.44/3.59 cnf(c134,plain,~convergent_lines(skolem0001,X222)|distinct_points(X223,intersection_point(skolem0001,X222))|apart_point_and_line(X223,skolem0002),inference(resolution,[status(thm)],[c45, c11])).
% 3.44/3.59 cnf(c329,plain,distinct_points(X464,intersection_point(skolem0001,skolem0002))|apart_point_and_line(X464,skolem0002),inference(resolution,[status(thm)],[c134, c9])).
% 3.44/3.59 cnf(c769,plain,apart_point_and_line(intersection_point(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c329, c77])).
% 3.44/3.59 cnf(c780,plain,~convergent_lines(X2324,skolem0002)|distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(X2324,skolem0002)),inference(resolution,[status(thm)],[c769, c46])).
% 3.44/3.59 cnf(c8409,plain,distinct_points(intersection_point(skolem0001,skolem0002),intersection_point(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c780, c9])).
% 3.44/3.59 cnf(c8623,plain,$false,inference(resolution,[status(thm)],[c8409, c77])).
% 3.44/3.59 % SZS output end CNFRefutation
% 3.44/3.59
% 3.44/3.59 % Initial clauses : 23
% 3.44/3.59 % Processed clauses : 356
% 3.44/3.59 % Factors computed : 289
% 3.44/3.59 % Resolvents computed: 8271
% 3.44/3.59 % Tautologies deleted: 0
% 3.44/3.59 % Forward subsumed : 986
% 3.44/3.59 % Backward subsumed : 3
% 3.44/3.59 % -------- CPU Time ---------
% 3.44/3.59 % User time : 3.230 s
% 3.44/3.59 % System time : 0.021 s
% 3.44/3.59 % Total time : 3.251 s
%------------------------------------------------------------------------------