%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO237+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:41 EDT 2024
% Result : Theorem 0.42s 0.60s
% Output : Refutation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO237+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n023.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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 08:33:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.42/0.60 % Version: 1.5
% 0.42/0.60 % SZS status Theorem
% 0.42/0.60 % SZS output start CNFRefutation
% 0.42/0.60 fof(oag10,axiom,(![A]:(![L]:(~(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag10)).
% 0.42/0.60 fof(c67,plain,(![A]:(![L]:(~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L))))),inference(fof_nnf,[status(thm)],[oag10])).
% 0.42/0.60 fof(c68,plain,((![A]:(![L]:~left_apart_point(A,L)))&(![A]:(![L]:~left_apart_point(A,reverse_line(L))))),inference(shift_quantors,[status(thm)],[c67])).
% 0.42/0.60 fof(c70,plain,(![X44]:(![X45]:(![X46]:(![X47]:(~left_apart_point(X44,X45)&~left_apart_point(X46,reverse_line(X47))))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X44]:(![X45]:~left_apart_point(X44,X45)))&(![X46]:(![X47]:~left_apart_point(X46,reverse_line(X47))))),inference(variable_rename,[status(thm)],[c68])).])).
% 0.42/0.60 cnf(c71,plain,~left_apart_point(X97,X98),inference(split_conjunct,[status(thm)],[c70])).
% 0.42/0.60 fof(con,conjecture,(![A]:(![B]:(![C]:(![L]:(apart_point_and_line(C,L)=>(divides_points(L,A,B)=>(divides_points(L,A,C)|divides_points(L,B,C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.42/0.60 fof(c0,negated_conjecture,(~(![A]:(![B]:(![C]:(![L]:(apart_point_and_line(C,L)=>(divides_points(L,A,B)=>(divides_points(L,A,C)|divides_points(L,B,C))))))))),inference(assume_negation,[status(cth)],[con])).
% 0.42/0.60 fof(c1,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[L]:(apart_point_and_line(C,L)&(divides_points(L,A,B)&(~divides_points(L,A,C)&~divides_points(L,B,C)))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.42/0.60 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(apart_point_and_line(X4,X5)&(divides_points(X5,X2,X3)&(~divides_points(X5,X2,X4)&~divides_points(X5,X3,X4)))))))),inference(variable_rename,[status(thm)],[c1])).
% 0.42/0.60 fof(c3,negated_conjecture,(apart_point_and_line(skolem0003,skolem0004)&(divides_points(skolem0004,skolem0001,skolem0002)&(~divides_points(skolem0004,skolem0001,skolem0003)&~divides_points(skolem0004,skolem0002,skolem0003)))),inference(skolemize,[status(esa)],[c2])).
% 0.42/0.60 cnf(c5,negated_conjecture,divides_points(skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 0.42/0.60 fof(div_def,axiom,(![A]:(![B]:(![L]:(divides_points(L,A,B)<=>((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', div_def)).
% 0.42/0.60 fof(c136,plain,(![A]:(![B]:(![L]:((~divides_points(L,A,B)|((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L))))&(((~left_apart_point(A,L)|~left_apart_point(B,reverse_line(L)))&(~left_apart_point(A,reverse_line(L))|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(fof_nnf,[status(thm)],[div_def])).
% 0.42/0.60 fof(c137,plain,((![A]:(![B]:(![L]:(~divides_points(L,A,B)|((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L)))))))&(![A]:(![B]:(![L]:(((~left_apart_point(A,L)|~left_apart_point(B,reverse_line(L)))&(~left_apart_point(A,reverse_line(L))|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(shift_quantors,[status(thm)],[c136])).
% 0.42/0.60 fof(c139,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:((~divides_points(X83,X81,X82)|((left_apart_point(X81,X83)&left_apart_point(X82,reverse_line(X83)))|(left_apart_point(X81,reverse_line(X83))&left_apart_point(X82,X83))))&(((~left_apart_point(X84,X86)|~left_apart_point(X85,reverse_line(X86)))&(~left_apart_point(X84,reverse_line(X86))|~left_apart_point(X85,X86)))|divides_points(X86,X84,X85))))))))),inference(shift_quantors,[status(thm)],[fof(c138,plain,((![X81]:(![X82]:(![X83]:(~divides_points(X83,X81,X82)|((left_apart_point(X81,X83)&left_apart_point(X82,reverse_line(X83)))|(left_apart_point(X81,reverse_line(X83))&left_apart_point(X82,X83)))))))&(![X84]:(![X85]:(![X86]:(((~left_apart_point(X84,X86)|~left_apart_point(X85,reverse_line(X86)))&(~left_apart_point(X84,reverse_line(X86))|~left_apart_point(X85,X86)))|divides_points(X86,X84,X85)))))),inference(variable_rename,[status(thm)],[c137])).])).
% 0.42/0.60 fof(c140,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:((((~divides_points(X83,X81,X82)|(left_apart_point(X81,X83)|left_apart_point(X81,reverse_line(X83))))&(~divides_points(X83,X81,X82)|(left_apart_point(X81,X83)|left_apart_point(X82,X83))))&((~divides_points(X83,X81,X82)|(left_apart_point(X82,reverse_line(X83))|left_apart_point(X81,reverse_line(X83))))&(~divides_points(X83,X81,X82)|(left_apart_point(X82,reverse_line(X83))|left_apart_point(X82,X83)))))&(((~left_apart_point(X84,X86)|~left_apart_point(X85,reverse_line(X86)))|divides_points(X86,X84,X85))&((~left_apart_point(X84,reverse_line(X86))|~left_apart_point(X85,X86))|divides_points(X86,X84,X85)))))))))),inference(distribute,[status(thm)],[c139])).
% 0.42/0.60 cnf(c142,plain,~divides_points(X171,X173,X172)|left_apart_point(X173,X171)|left_apart_point(X172,X171),inference(split_conjunct,[status(thm)],[c140])).
% 0.42/0.60 cnf(c163,plain,left_apart_point(skolem0001,skolem0004)|left_apart_point(skolem0002,skolem0004),inference(resolution,[status(thm)],[c142, c5])).
% 0.42/0.60 cnf(c164,plain,left_apart_point(skolem0002,skolem0004),inference(resolution,[status(thm)],[c163, c71])).
% 0.42/0.60 cnf(c166,plain,$false,inference(resolution,[status(thm)],[c164, c71])).
% 0.42/0.60 % SZS output end CNFRefutation
% 0.42/0.60
% 0.42/0.60 % Initial clauses : 62
% 0.42/0.60 % Processed clauses : 28
% 0.42/0.60 % Factors computed : 0
% 0.42/0.60 % Resolvents computed: 4
% 0.42/0.60 % Tautologies deleted: 0
% 0.42/0.60 % Forward subsumed : 12
% 0.42/0.60 % Backward subsumed : 1
% 0.42/0.60 % -------- CPU Time ---------
% 0.42/0.60 % User time : 0.230 s
% 0.42/0.60 % System time : 0.015 s
% 0.42/0.60 % Total time : 0.245 s
%------------------------------------------------------------------------------