%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO226+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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 0.46s 0.65s
% Output : Refutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO226+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.33 % Computer : n012.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Thu May 9 08:04:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.46/0.65 % Version: 1.5
% 0.46/0.65 % SZS status Theorem
% 0.46/0.65 % SZS output start CNFRefutation
% 0.46/0.65 fof(con,conjecture,(![L]:(![M]:(((line(L)&line(M))&convergent_lines(L,M))=>(?[X]:(point(X)=>(incident_point_and_line(X,L)&incident_point_and_line(X,M))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 0.46/0.65 fof(c0,negated_conjecture,(~(![L]:(![M]:(((line(L)&line(M))&convergent_lines(L,M))=>(?[X]:(point(X)=>(incident_point_and_line(X,L)&incident_point_and_line(X,M)))))))),inference(assume_negation,[status(cth)],[con])).
% 0.46/0.65 fof(c1,negated_conjecture,(?[L]:(?[M]:(((line(L)&line(M))&convergent_lines(L,M))&(![X]:(point(X)&(~incident_point_and_line(X,L)|~incident_point_and_line(X,M))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.46/0.65 fof(c2,negated_conjecture,(?[L]:(?[M]:(((line(L)&line(M))&convergent_lines(L,M))&((![X]:point(X))&(![X]:(~incident_point_and_line(X,L)|~incident_point_and_line(X,M))))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.46/0.65 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(((line(X2)&line(X3))&convergent_lines(X2,X3))&((![X4]:point(X4))&(![X5]:(~incident_point_and_line(X5,X2)|~incident_point_and_line(X5,X3))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.46/0.65 fof(c5,negated_conjecture,(![X4]:(![X5]:(((line(skolem0001)&line(skolem0002))&convergent_lines(skolem0001,skolem0002))&(point(X4)&(~incident_point_and_line(X5,skolem0001)|~incident_point_and_line(X5,skolem0002)))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((line(skolem0001)&line(skolem0002))&convergent_lines(skolem0001,skolem0002))&((![X4]:point(X4))&(![X5]:(~incident_point_and_line(X5,skolem0001)|~incident_point_and_line(X5,skolem0002))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.46/0.65 cnf(c8,negated_conjecture,convergent_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c5])).
% 0.46/0.65 fof(ci3,axiom,(![X]:(![Y]:(convergent_lines(X,Y)=>(~apart_point_and_line(intersection_point(X,Y),X))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci3)).
% 0.46/0.65 fof(c130,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_simplification,[status(thm)],[ci3])).
% 0.46/0.65 fof(c131,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),X)))),inference(fof_nnf,[status(thm)],[c130])).
% 0.46/0.65 fof(c132,plain,(![X79]:(![X80]:(~convergent_lines(X79,X80)|~apart_point_and_line(intersection_point(X79,X80),X79)))),inference(variable_rename,[status(thm)],[c131])).
% 0.46/0.65 cnf(c133,plain,~convergent_lines(X281,X282)|~apart_point_and_line(intersection_point(X281,X282),X281),inference(split_conjunct,[status(thm)],[c132])).
% 0.46/0.65 fof(a4,axiom,(![X]:(![Y]:(incident_point_and_line(X,Y)<=>(~apart_point_and_line(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a4)).
% 0.46/0.65 fof(c18,plain,(![X]:(![Y]:(incident_point_and_line(X,Y)<=>~apart_point_and_line(X,Y)))),inference(fof_simplification,[status(thm)],[a4])).
% 0.46/0.65 fof(c19,plain,(![X]:(![Y]:((~incident_point_and_line(X,Y)|~apart_point_and_line(X,Y))&(apart_point_and_line(X,Y)|incident_point_and_line(X,Y))))),inference(fof_nnf,[status(thm)],[c18])).
% 0.46/0.65 fof(c20,plain,((![X]:(![Y]:(~incident_point_and_line(X,Y)|~apart_point_and_line(X,Y))))&(![X]:(![Y]:(apart_point_and_line(X,Y)|incident_point_and_line(X,Y))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.46/0.65 fof(c22,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~incident_point_and_line(X10,X11)|~apart_point_and_line(X10,X11))&(apart_point_and_line(X12,X13)|incident_point_and_line(X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X10]:(![X11]:(~incident_point_and_line(X10,X11)|~apart_point_and_line(X10,X11))))&(![X12]:(![X13]:(apart_point_and_line(X12,X13)|incident_point_and_line(X12,X13))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.46/0.65 cnf(c23,plain,~incident_point_and_line(X116,X117)|~apart_point_and_line(X116,X117),inference(split_conjunct,[status(thm)],[c22])).
% 0.46/0.65 cnf(c24,plain,apart_point_and_line(X118,X119)|incident_point_and_line(X118,X119),inference(split_conjunct,[status(thm)],[c22])).
% 0.46/0.65 cnf(c10,negated_conjecture,~incident_point_and_line(X109,skolem0001)|~incident_point_and_line(X109,skolem0002),inference(split_conjunct,[status(thm)],[c5])).
% 0.46/0.65 cnf(c171,plain,apart_point_and_line(X224,skolem0002)|~incident_point_and_line(X224,skolem0001),inference(resolution,[status(thm)],[c24, c10])).
% 0.46/0.65 cnf(c232,plain,apart_point_and_line(X263,skolem0002)|apart_point_and_line(X263,skolem0001),inference(resolution,[status(thm)],[c171, c24])).
% 0.46/0.65 cnf(c282,plain,apart_point_and_line(X271,skolem0001)|~incident_point_and_line(X271,skolem0002),inference(resolution,[status(thm)],[c232, c23])).
% 0.46/0.65 fof(ci4,axiom,(![X]:(![Y]:(convergent_lines(X,Y)=>(~apart_point_and_line(intersection_point(X,Y),Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci4)).
% 0.46/0.65 fof(c126,plain,(![X]:(![Y]:(convergent_lines(X,Y)=>~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_simplification,[status(thm)],[ci4])).
% 0.46/0.65 fof(c127,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|~apart_point_and_line(intersection_point(X,Y),Y)))),inference(fof_nnf,[status(thm)],[c126])).
% 0.46/0.65 fof(c128,plain,(![X77]:(![X78]:(~convergent_lines(X77,X78)|~apart_point_and_line(intersection_point(X77,X78),X78)))),inference(variable_rename,[status(thm)],[c127])).
% 0.46/0.65 cnf(c129,plain,~convergent_lines(X280,X279)|~apart_point_and_line(intersection_point(X280,X279),X279),inference(split_conjunct,[status(thm)],[c128])).
% 0.46/0.65 cnf(c306,plain,~convergent_lines(X316,X317)|incident_point_and_line(intersection_point(X316,X317),X317),inference(resolution,[status(thm)],[c129, c24])).
% 0.46/0.65 cnf(c357,plain,incident_point_and_line(intersection_point(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c306, c8])).
% 0.46/0.65 cnf(c362,plain,apart_point_and_line(intersection_point(skolem0001,skolem0002),skolem0001),inference(resolution,[status(thm)],[c357, c282])).
% 0.46/0.65 cnf(c373,plain,~convergent_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c362, c133])).
% 0.46/0.65 cnf(c374,plain,$false,inference(resolution,[status(thm)],[c373, c8])).
% 0.46/0.65 % SZS output end CNFRefutation
% 0.46/0.65
% 0.46/0.65 % Initial clauses : 51
% 0.46/0.65 % Processed clauses : 94
% 0.46/0.65 % Factors computed : 0
% 0.46/0.65 % Resolvents computed: 212
% 0.46/0.65 % Tautologies deleted: 5
% 0.46/0.65 % Forward subsumed : 30
% 0.46/0.65 % Backward subsumed : 2
% 0.46/0.65 % -------- CPU Time ---------
% 0.46/0.65 % User time : 0.286 s
% 0.46/0.65 % System time : 0.007 s
% 0.46/0.65 % Total time : 0.293 s
%------------------------------------------------------------------------------