%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:16:59 AM UTC 2026
% Result : Unsatisfiable 6.33s 11.52s
% Output : CNFRefutation 6.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 17
% Syntax : Number of formulae : 109 ( 32 unt; 0 def)
% Number of atoms : 544 ( 230 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 672 ( 237 ~; 435 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-3 aty)
% Number of variables : 74 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_G10A,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ collinear(VAR_0,VAR_1,VAR_2)
| on(VAR_0,line_through_3_points(VAR_0,VAR_1,VAR_2))
| VAR_1 = VAR_2
| VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ point(VAR_2)
| ~ point(VAR_1)
| ~ point(VAR_0) ),
file('theBenchmark.p',axiom_G10A) ).
cnf(c_1,plain,
( ~ collinear(A,B,C)
| on(A,line_through_3_points(A,B,C))
| B = C
| A = C
| A = B
| ~ point(C)
| ~ point(B)
| ~ point(A) ),
inference(clausify,[status(thm)],[axiom_G10A]) ).
fof(axiom_G10B,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ collinear(VAR_0,VAR_1,VAR_2)
| on(VAR_1,line_through_3_points(VAR_0,VAR_1,VAR_2))
| VAR_1 = VAR_2
| VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ point(VAR_2)
| ~ point(VAR_1)
| ~ point(VAR_0) ),
file('theBenchmark.p',axiom_G10B) ).
cnf(c_7,plain,
( ~ collinear(A,B,C)
| on(B,line_through_3_points(A,B,C))
| B = C
| A = C
| A = B
| ~ point(C)
| ~ point(B)
| ~ point(A) ),
inference(clausify,[status(thm)],[axiom_G10B]) ).
fof(axiom_G10C,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ collinear(VAR_0,VAR_1,VAR_2)
| on(VAR_2,line_through_3_points(VAR_0,VAR_1,VAR_2))
| VAR_1 = VAR_2
| VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ point(VAR_2)
| ~ point(VAR_1)
| ~ point(VAR_0) ),
file('theBenchmark.p',axiom_G10C) ).
cnf(c_8,plain,
( ~ collinear(A,B,C)
| on(C,line_through_3_points(A,B,C))
| B = C
| A = C
| A = B
| ~ point(C)
| ~ point(B)
| ~ point(A) ),
inference(clausify,[status(thm)],[axiom_G10C]) ).
fof(axiom_G10D,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ collinear(VAR_0,VAR_1,VAR_2)
| line(line_through_3_points(VAR_0,VAR_1,VAR_2))
| VAR_1 = VAR_2
| VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ point(VAR_2)
| ~ point(VAR_1)
| ~ point(VAR_0) ),
file('theBenchmark.p',axiom_G10D) ).
cnf(c_9,plain,
( ~ collinear(A,B,C)
| line(line_through_3_points(A,B,C))
| B = C
| A = C
| A = B
| ~ point(C)
| ~ point(B)
| ~ point(A) ),
inference(clausify,[status(thm)],[axiom_G10D]) ).
fof(axiom_G10E,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ line(VAR_3)
| VAR_1 = VAR_2
| VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ point(VAR_2)
| ~ point(VAR_1)
| ~ point(VAR_0)
| ~ on(VAR_2,VAR_3)
| ~ on(VAR_1,VAR_3)
| ~ on(VAR_0,VAR_3)
| collinear(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',axiom_G10E) ).
cnf(c_10,plain,
( ~ line(D)
| B = C
| A = C
| A = B
| ~ point(C)
| ~ point(B)
| ~ point(A)
| ~ on(C,D)
| ~ on(B,D)
| ~ on(A,D)
| collinear(A,B,C) ),
inference(clausify,[status(thm)],[axiom_G10E]) ).
fof(prove_points_noncollinear,axiom,
collinear(point1,point2,point3),
file('theBenchmark.p',prove_points_noncollinear) ).
cnf(c_11,plain,
collinear(point1,point2,point3),
inference(clausify,[status(thm)],[prove_points_noncollinear]) ).
cnf(c_12,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolve,[status(thm)],[c_11,c_1]) ).
cnf(c_833,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_12]) ).
cnf(c_834,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point2 = point3
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_833]) ).
cnf(c_13,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_834]) ).
cnf(c_14,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolve,[status(thm)],[c_11,c_7]) ).
cnf(c_835,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_14]) ).
cnf(c_836,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point2 = point3
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_835]) ).
cnf(c_15,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_836]) ).
cnf(c_16,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolve,[status(thm)],[c_11,c_8]) ).
cnf(c_837,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_16]) ).
cnf(c_838,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point2 = point3
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_837]) ).
cnf(c_17,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_838]) ).
cnf(c_18,plain,
( line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolve,[status(thm)],[c_11,c_9]) ).
cnf(c_839,plain,
( line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_18]) ).
cnf(c_840,plain,
( line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_839]) ).
cnf(c_19,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(copy,[status(thm)],[c_840]) ).
cnf(c_24,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(resolve,[status(thm)],[c_10,c_8]) ).
cnf(c_841,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_24]) ).
cnf(c_842,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| A = D
| A = C
| ~ point(D)
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_841]) ).
cnf(c_843,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| A = D
| A = C
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_842]) ).
cnf(c_844,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| A = D
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_843]) ).
cnf(c_845,plain,
( on(D,line_through_3_points(A,C,D))
| C = D
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_25,plain,
( on(D,line_through_3_points(A,C,D))
| ~ line(B)
| C = D
| A = D
| A = C
| ~ point(D)
| ~ point(C)
| ~ point(A)
| ~ on(D,B)
| ~ on(C,B)
| ~ on(A,B) ),
inference(copy,[status(thm)],[c_845]) ).
fof(point2_not_point3,axiom,
point2 != point3,
file('theBenchmark.p',point2_not_point3) ).
cnf(c_68,plain,
point2 != point3,
inference(clausify,[status(thm)],[point2_not_point3]) ).
cnf(c_69,plain,
point3 != point2,
inference(copy,[status(thm)],[c_68]) ).
fof(point1_not_point3,axiom,
point1 != point3,
file('theBenchmark.p',point1_not_point3) ).
cnf(c_70,plain,
point1 != point3,
inference(clausify,[status(thm)],[point1_not_point3]) ).
cnf(c_71,plain,
point3 != point1,
inference(copy,[status(thm)],[c_70]) ).
fof(point1_not_point2,axiom,
point1 != point2,
file('theBenchmark.p',point1_not_point2) ).
cnf(c_72,plain,
point1 != point2,
inference(clausify,[status(thm)],[point1_not_point2]) ).
cnf(c_73,plain,
point2 != point1,
inference(copy,[status(thm)],[c_72]) ).
fof(point3_not_on_line,axiom,
~ on(point3,a_line),
file('theBenchmark.p',point3_not_on_line) ).
cnf(c_74,plain,
~ on(point3,a_line),
inference(clausify,[status(thm)],[point3_not_on_line]) ).
fof(point2_on_line,axiom,
on(point2,a_line),
file('theBenchmark.p',point2_on_line) ).
cnf(c_75,plain,
on(point2,a_line),
inference(clausify,[status(thm)],[point2_on_line]) ).
fof(point1_on_line,axiom,
on(point1,a_line),
file('theBenchmark.p',point1_on_line) ).
cnf(c_76,plain,
on(point1,a_line),
inference(clausify,[status(thm)],[point1_on_line]) ).
fof(line,axiom,
line(a_line),
file('theBenchmark.p',line) ).
cnf(c_77,plain,
line(a_line),
inference(clausify,[status(thm)],[line]) ).
fof(point3,axiom,
point(point3),
file('theBenchmark.p',point3) ).
cnf(c_78,plain,
point(point3),
inference(clausify,[status(thm)],[point3]) ).
fof(point2,axiom,
point(point2),
file('theBenchmark.p',point2) ).
cnf(c_79,plain,
point(point2),
inference(clausify,[status(thm)],[point2]) ).
fof(point1,axiom,
point(point1),
file('theBenchmark.p',point1) ).
cnf(c_80,plain,
point(point1),
inference(clausify,[status(thm)],[point1]) ).
fof(axiom_G1D,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ line(VAR_3)
| ~ line(VAR_1)
| ~ point(VAR_2)
| ~ point(VAR_0)
| ~ on(VAR_2,VAR_3)
| ~ on(VAR_0,VAR_3)
| VAR_1 = VAR_3
| ~ on(VAR_2,VAR_1)
| VAR_0 = VAR_2
| ~ on(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_G1D) ).
cnf(c_100,plain,
( ~ line(D)
| ~ line(B)
| ~ point(C)
| ~ point(A)
| ~ on(C,D)
| ~ on(A,D)
| B = D
| ~ on(C,B)
| A = C
| ~ on(A,B) ),
inference(clausify,[status(thm)],[axiom_G1D]) ).
cnf(c_846,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2) ),
inference(resolve,[status(thm)],[c_80,c_19]) ).
cnf(c_847,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3) ),
inference(resolve,[status(thm)],[c_79,c_846]) ).
cnf(c_848,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1 ),
inference(resolve,[status(thm)],[c_78,c_847]) ).
cnf(c_849,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1 ),
inference(resolve,[status(thm)],[c_73,c_848]) ).
cnf(c_850,plain,
( line(line_through_3_points(point1,point2,point3))
| point3 = point2 ),
inference(resolve,[status(thm)],[c_71,c_849]) ).
cnf(c_116,plain,
line(line_through_3_points(point1,point2,point3)),
inference(resolve,[status(thm)],[c_69,c_850]) ).
cnf(c_851,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2) ),
inference(resolve,[status(thm)],[c_80,c_17]) ).
cnf(c_852,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3) ),
inference(resolve,[status(thm)],[c_79,c_851]) ).
cnf(c_853,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1 ),
inference(resolve,[status(thm)],[c_78,c_852]) ).
cnf(c_854,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1 ),
inference(resolve,[status(thm)],[c_73,c_853]) ).
cnf(c_855,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point3 = point2 ),
inference(resolve,[status(thm)],[c_71,c_854]) ).
cnf(c_117,plain,
on(point3,line_through_3_points(point1,point2,point3)),
inference(resolve,[status(thm)],[c_69,c_855]) ).
cnf(c_856,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2) ),
inference(resolve,[status(thm)],[c_80,c_15]) ).
cnf(c_857,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3) ),
inference(resolve,[status(thm)],[c_79,c_856]) ).
cnf(c_858,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1 ),
inference(resolve,[status(thm)],[c_78,c_857]) ).
cnf(c_859,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1 ),
inference(resolve,[status(thm)],[c_73,c_858]) ).
cnf(c_860,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point3 = point2 ),
inference(resolve,[status(thm)],[c_71,c_859]) ).
cnf(c_118,plain,
on(point2,line_through_3_points(point1,point2,point3)),
inference(resolve,[status(thm)],[c_69,c_860]) ).
cnf(c_861,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3)
| ~ point(point2) ),
inference(resolve,[status(thm)],[c_80,c_13]) ).
cnf(c_862,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1
| ~ point(point3) ),
inference(resolve,[status(thm)],[c_79,c_861]) ).
cnf(c_863,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1
| point2 = point1 ),
inference(resolve,[status(thm)],[c_78,c_862]) ).
cnf(c_864,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2
| point3 = point1 ),
inference(resolve,[status(thm)],[c_73,c_863]) ).
cnf(c_865,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point3 = point2 ),
inference(resolve,[status(thm)],[c_71,c_864]) ).
cnf(c_119,plain,
on(point1,line_through_3_points(point1,point2,point3)),
inference(resolve,[status(thm)],[c_69,c_865]) ).
cnf(c_866,plain,
( ~ line(B)
| ~ line(a_line)
| ~ point(A)
| ~ point(point2)
| ~ on(A,B)
| ~ on(point2,B)
| a_line = B
| ~ on(A,a_line)
| point2 = A ),
inference(resolve,[status(thm)],[c_100,c_75]) ).
cnf(c_867,plain,
( ~ line(A)
| ~ line(a_line)
| ~ point(point1)
| ~ point(point2)
| ~ on(point1,A)
| ~ on(point2,A)
| a_line = A
| point2 = point1 ),
inference(resolve,[status(thm)],[c_866,c_76]) ).
cnf(c_868,plain,
( ~ line(line_through_3_points(point1,point2,point3))
| ~ line(a_line)
| ~ point(point1)
| ~ point(point2)
| ~ on(point1,line_through_3_points(point1,point2,point3))
| a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_867,c_118]) ).
cnf(c_869,plain,
( ~ line(line_through_3_points(point1,point2,point3))
| ~ line(a_line)
| ~ point(point1)
| ~ point(point2)
| a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_868,c_119]) ).
cnf(c_870,plain,
( ~ line(line_through_3_points(point1,point2,point3))
| ~ line(a_line)
| ~ point(point1)
| a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_869,c_79]) ).
cnf(c_871,plain,
( ~ line(line_through_3_points(point1,point2,point3))
| ~ line(a_line)
| a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_870,c_80]) ).
cnf(c_872,plain,
( ~ line(line_through_3_points(point1,point2,point3))
| a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_871,c_77]) ).
cnf(c_873,plain,
( a_line = line_through_3_points(point1,point2,point3)
| point2 = point1 ),
inference(resolve,[status(thm)],[c_872,c_116]) ).
cnf(c_874,plain,
( line_through_3_points(point1,point2,point3) = a_line
| point2 = point1 ),
inference(copy,[status(thm)],[c_873]) ).
cnf(c_822,plain,
line_through_3_points(point1,point2,point3) = a_line,
inference(resolve,[status(thm)],[c_73,c_874]) ).
cnf(c_875,plain,
( on(B,line_through_3_points(point1,A,B))
| ~ line(line_through_3_points(point1,point2,point3))
| A = B
| point1 = B
| point1 = A
| ~ point(B)
| ~ point(A)
| ~ point(point1)
| ~ on(B,line_through_3_points(point1,point2,point3))
| ~ on(A,line_through_3_points(point1,point2,point3)) ),
inference(resolve,[status(thm)],[c_25,c_119]) ).
cnf(c_876,plain,
( on(A,line_through_3_points(point1,point2,A))
| ~ line(line_through_3_points(point1,point2,point3))
| point2 = A
| point1 = A
| point1 = point2
| ~ point(A)
| ~ point(point2)
| ~ point(point1)
| ~ on(A,line_through_3_points(point1,point2,point3)) ),
inference(resolve,[status(thm)],[c_875,c_118]) ).
cnf(c_877,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| ~ line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolve,[status(thm)],[c_876,c_117]) ).
cnf(c_878,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| ~ line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2) ),
inference(resolve,[status(thm)],[c_877,c_80]) ).
cnf(c_879,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| ~ line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3) ),
inference(resolve,[status(thm)],[c_878,c_79]) ).
cnf(c_880,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| ~ line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2 ),
inference(resolve,[status(thm)],[c_879,c_78]) ).
cnf(c_881,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2 ),
inference(resolve,[status(thm)],[c_880,c_116]) ).
cnf(c_882,plain,
( on(point3,a_line)
| point2 = point3
| point1 = point3
| point1 = point2 ),
inference(paramod,[status(thm)],[c_822,c_881]) ).
cnf(c_883,plain,
( on(point3,a_line)
| point2 = point3
| point1 = point3
| point2 = point1 ),
inference(copy,[status(thm)],[c_882]) ).
cnf(c_884,plain,
( on(point3,a_line)
| point2 = point3
| point3 = point1
| point2 = point1 ),
inference(copy,[status(thm)],[c_883]) ).
cnf(c_885,plain,
( on(point3,a_line)
| point3 = point2
| point3 = point1
| point2 = point1 ),
inference(copy,[status(thm)],[c_884]) ).
cnf(c_886,plain,
( on(point3,a_line)
| point3 = point2
| point3 = point1 ),
inference(resolve,[status(thm)],[c_73,c_885]) ).
cnf(c_887,plain,
( on(point3,a_line)
| point3 = point2 ),
inference(resolve,[status(thm)],[c_71,c_886]) ).
cnf(c_888,plain,
on(point3,a_line),
inference(resolve,[status(thm)],[c_69,c_887]) ).
cnf(c_832,plain,
$false,
inference(resolve,[status(thm)],[c_74,c_888]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/10.60 % Computer : n014.cluster.edu
% 0.02/10.60 % Model : x86_64 x86_64
% 0.02/10.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/10.60 % Memory : 8046.5625MB
% 0.02/10.60 % OS : Linux 6.8.0-71-generic
% 0.02/10.60 % CPULimit : 300
% 0.02/10.60 % WCLimit : 300
% 0.02/10.60 % DateTime : Fri Sep 25 12:39:43 UTC 2026
% 0.02/10.60 % CPUTime :
% 0.02/10.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/10.60 % Process 244875 was started by sandbox on n014,
% 0.02/10.60 % Fri Sep 25 12:39:43 2026
% 0.02/10.60 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.02/10.61
% 0.02/10.61 % From the command line: assign(max_seconds, 300).
% 6.33/11.52
% 6.33/11.52 % SZS status Unsatisfiable for theBenchmark
% 6.33/11.52
% 6.33/11.52 % Proof 1 at 0.82 (+ 0.08) seconds.
% 6.33/11.52 % Length of proof is 36.
% 6.33/11.52 % Level of proof is 5.
% 6.33/11.52 % Maximum clause weight is 42.000.
% 6.33/11.52 % Given clauses 71.
% 6.33/11.52
% 6.33/11.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------