%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO238+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:42 EDT 2024
% Result : Theorem 1.29s 1.47s
% Output : Refutation 1.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO238+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % 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 07:48:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 1.29/1.47 % Version: 1.5
% 1.29/1.47 % SZS status Theorem
% 1.29/1.47 % SZS output start CNFRefutation
% 1.29/1.47 fof(ax10_basics,axiom,(![A]:(![L]:(~(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax10_basics)).
% 1.29/1.47 fof(c66,plain,(![A]:(![L]:(~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L))))),inference(fof_nnf,[status(thm)],[ax10_basics])).
% 1.29/1.47 fof(c67,plain,((![A]:(![L]:~left_apart_point(A,L)))&(![A]:(![L]:~left_apart_point(A,reverse_line(L))))),inference(shift_quantors,[status(thm)],[c66])).
% 1.29/1.47 fof(c69,plain,(![X44]:(![X45]:(![X46]:(![X47]:(~left_apart_point(X44,X45)&~left_apart_point(X46,reverse_line(X47))))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X44]:(![X45]:~left_apart_point(X44,X45)))&(![X46]:(![X47]:~left_apart_point(X46,reverse_line(X47))))),inference(variable_rename,[status(thm)],[c67])).])).
% 1.29/1.47 cnf(c70,plain,~left_apart_point(X117,X118),inference(split_conjunct,[status(thm)],[c69])).
% 1.29/1.47 fof(a2_defns,axiom,(![X]:(![Y]:(right_apart_point(X,Y)<=>left_apart_point(X,reverse_line(Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a2_defns)).
% 1.29/1.47 fof(c177,plain,(![X]:(![Y]:((~right_apart_point(X,Y)|left_apart_point(X,reverse_line(Y)))&(~left_apart_point(X,reverse_line(Y))|right_apart_point(X,Y))))),inference(fof_nnf,[status(thm)],[a2_defns])).
% 1.29/1.47 fof(c178,plain,((![X]:(![Y]:(~right_apart_point(X,Y)|left_apart_point(X,reverse_line(Y)))))&(![X]:(![Y]:(~left_apart_point(X,reverse_line(Y))|right_apart_point(X,Y))))),inference(shift_quantors,[status(thm)],[c177])).
% 1.29/1.47 fof(c180,plain,(![X107]:(![X108]:(![X109]:(![X110]:((~right_apart_point(X107,X108)|left_apart_point(X107,reverse_line(X108)))&(~left_apart_point(X109,reverse_line(X110))|right_apart_point(X109,X110))))))),inference(shift_quantors,[status(thm)],[fof(c179,plain,((![X107]:(![X108]:(~right_apart_point(X107,X108)|left_apart_point(X107,reverse_line(X108)))))&(![X109]:(![X110]:(~left_apart_point(X109,reverse_line(X110))|right_apart_point(X109,X110))))),inference(variable_rename,[status(thm)],[c178])).])).
% 1.29/1.47 cnf(c181,plain,~right_apart_point(X177,X176)|left_apart_point(X177,reverse_line(X176)),inference(split_conjunct,[status(thm)],[c180])).
% 1.29/1.47 fof(con,conjecture,(![A]:(![B]:(![C]:(![L]:((divides_points(L,A,B)÷s_points(L,A,C))=>(~divides_points(L,B,C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 1.29/1.47 fof(c0,negated_conjecture,(~(![A]:(![B]:(![C]:(![L]:((divides_points(L,A,B)÷s_points(L,A,C))=>(~divides_points(L,B,C)))))))),inference(assume_negation,[status(cth)],[con])).
% 1.29/1.47 fof(c1,negated_conjecture,(~(![A]:(![B]:(![C]:(![L]:((divides_points(L,A,B)÷s_points(L,A,C))=>~divides_points(L,B,C))))))),inference(fof_simplification,[status(thm)],[c0])).
% 1.29/1.47 fof(c2,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[L]:((divides_points(L,A,B)÷s_points(L,A,C))÷s_points(L,B,C)))))),inference(fof_nnf,[status(thm)],[c1])).
% 1.29/1.47 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((divides_points(X5,X2,X3)÷s_points(X5,X2,X4))÷s_points(X5,X3,X4)))))),inference(variable_rename,[status(thm)],[c2])).
% 1.29/1.47 fof(c4,negated_conjecture,((divides_points(skolem0004,skolem0001,skolem0002)÷s_points(skolem0004,skolem0001,skolem0003))÷s_points(skolem0004,skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c3])).
% 1.29/1.47 cnf(c5,negated_conjecture,divides_points(skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 1.29/1.47 fof(a8_defns,axiom,(![A]:(![B]:(![L]:(divides_points(L,A,B)<=>((left_apart_point(A,L)&right_apart_point(B,L))|(right_apart_point(A,L)&left_apart_point(B,L))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a8_defns)).
% 1.29/1.47 fof(c130,plain,(![A]:(![B]:(![L]:((~divides_points(L,A,B)|((left_apart_point(A,L)&right_apart_point(B,L))|(right_apart_point(A,L)&left_apart_point(B,L))))&(((~left_apart_point(A,L)|~right_apart_point(B,L))&(~right_apart_point(A,L)|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(fof_nnf,[status(thm)],[a8_defns])).
% 1.29/1.47 fof(c131,plain,((![A]:(![B]:(![L]:(~divides_points(L,A,B)|((left_apart_point(A,L)&right_apart_point(B,L))|(right_apart_point(A,L)&left_apart_point(B,L)))))))&(![A]:(![B]:(![L]:(((~left_apart_point(A,L)|~right_apart_point(B,L))&(~right_apart_point(A,L)|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(shift_quantors,[status(thm)],[c130])).
% 1.29/1.47 fof(c133,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:((~divides_points(X83,X81,X82)|((left_apart_point(X81,X83)&right_apart_point(X82,X83))|(right_apart_point(X81,X83)&left_apart_point(X82,X83))))&(((~left_apart_point(X84,X86)|~right_apart_point(X85,X86))&(~right_apart_point(X84,X86)|~left_apart_point(X85,X86)))|divides_points(X86,X84,X85))))))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X81]:(![X82]:(![X83]:(~divides_points(X83,X81,X82)|((left_apart_point(X81,X83)&right_apart_point(X82,X83))|(right_apart_point(X81,X83)&left_apart_point(X82,X83)))))))&(![X84]:(![X85]:(![X86]:(((~left_apart_point(X84,X86)|~right_apart_point(X85,X86))&(~right_apart_point(X84,X86)|~left_apart_point(X85,X86)))|divides_points(X86,X84,X85)))))),inference(variable_rename,[status(thm)],[c131])).])).
% 1.29/1.47 fof(c134,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:((((~divides_points(X83,X81,X82)|(left_apart_point(X81,X83)|right_apart_point(X81,X83)))&(~divides_points(X83,X81,X82)|(left_apart_point(X81,X83)|left_apart_point(X82,X83))))&((~divides_points(X83,X81,X82)|(right_apart_point(X82,X83)|right_apart_point(X81,X83)))&(~divides_points(X83,X81,X82)|(right_apart_point(X82,X83)|left_apart_point(X82,X83)))))&(((~left_apart_point(X84,X86)|~right_apart_point(X85,X86))|divides_points(X86,X84,X85))&((~right_apart_point(X84,X86)|~left_apart_point(X85,X86))|divides_points(X86,X84,X85)))))))))),inference(distribute,[status(thm)],[c133])).
% 1.29/1.47 cnf(c135,plain,~divides_points(X476,X477,X475)|left_apart_point(X477,X476)|right_apart_point(X477,X476),inference(split_conjunct,[status(thm)],[c134])).
% 1.29/1.47 cnf(c476,plain,left_apart_point(skolem0001,skolem0004)|right_apart_point(skolem0001,skolem0004),inference(resolution,[status(thm)],[c135, c5])).
% 1.29/1.47 cnf(c4573,plain,right_apart_point(skolem0001,skolem0004),inference(resolution,[status(thm)],[c476, c70])).
% 1.29/1.47 cnf(c4576,plain,left_apart_point(skolem0001,reverse_line(skolem0004)),inference(resolution,[status(thm)],[c4573, c181])).
% 1.29/1.47 cnf(c4579,plain,$false,inference(resolution,[status(thm)],[c4576, c70])).
% 1.29/1.47 % SZS output end CNFRefutation
% 1.29/1.47
% 1.29/1.47 % Initial clauses : 69
% 1.29/1.47 % Processed clauses : 252
% 1.29/1.47 % Factors computed : 15
% 1.29/1.47 % Resolvents computed: 4376
% 1.29/1.47 % Tautologies deleted: 8
% 1.29/1.47 % Forward subsumed : 426
% 1.29/1.47 % Backward subsumed : 3
% 1.29/1.47 % -------- CPU Time ---------
% 1.29/1.47 % User time : 1.101 s
% 1.29/1.47 % System time : 0.030 s
% 1.29/1.47 % Total time : 1.131 s
%------------------------------------------------------------------------------