%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 08:39:25 AM UTC 2026
% Result : Unsatisfiable 190.13s 205.38s
% Output : Proof 191.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_G1A,axiom,
( ~ point(Z2)
| ~ point(Z1)
| Z1 = Z2
| on(Z1,line_from_to(Z1,Z2)) ),
file('GEO003-0.ax',axiom_G1A) ).
cnf(axiom_G1B,axiom,
( ~ point(Z2)
| ~ point(Z1)
| Z1 = Z2
| on(Z2,line_from_to(Z1,Z2)) ),
file('GEO003-0.ax',axiom_G1B) ).
cnf(axiom_G1C,axiom,
( ~ point(Z2)
| ~ point(Z1)
| Z1 = Z2
| line(line_from_to(Z1,Z2)) ),
file('GEO003-0.ax',axiom_G1C) ).
cnf(axiom_G1D,axiom,
( ~ line(Y4)
| ~ line(Y3)
| ~ point(Z2)
| ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ),
file('GEO003-0.ax',axiom_G1D) ).
cnf(axiom_G2A,axiom,
( ~ line(Y1)
| on(point_1_on_line(Y1),Y1) ),
file('GEO003-0.ax',axiom_G2A) ).
cnf(axiom_G2B,axiom,
( ~ line(Y1)
| on(point_2_on_line(Y1),Y1) ),
file('GEO003-0.ax',axiom_G2B) ).
cnf(axiom_G2C,axiom,
( ~ line(Y1)
| point(point_1_on_line(Y1)) ),
file('GEO003-0.ax',axiom_G2C) ).
cnf(axiom_G2D,axiom,
( ~ line(Y1)
| point(point_2_on_line(Y1)) ),
file('GEO003-0.ax',axiom_G2D) ).
cnf(axiom_G2E,axiom,
( ~ line(Y1)
| point_1_on_line(Y1) != point_2_on_line(Y1) ),
file('GEO003-0.ax',axiom_G2E) ).
cnf(axiom_G3A,axiom,
( ~ line(Y1)
| ~ on(point_not_on_line(Y1),Y1) ),
file('GEO003-0.ax',axiom_G3A) ).
cnf(axiom_G3B,axiom,
( ~ line(Y1)
| point(point_not_on_line(Y1)) ),
file('GEO003-0.ax',axiom_G3B) ).
cnf(axiom_G4A,axiom,
line(at_least_one_line),
file('GEO003-0.ax',axiom_G4A) ).
cnf(axiom_G5A,axiom,
( on(point_on_plane(Z1),Z1)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G5A) ).
cnf(axiom_G5B,axiom,
( point(point_on_plane(Z1))
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G5B) ).
cnf(axiom_G6A,axiom,
( ~ on(point_not_on_plane(Z1),Z1)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G6A) ).
cnf(axiom_G6B,axiom,
( point(point_not_on_plane(Z1))
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G6B) ).
cnf(axiom_G7A,axiom,
( X2 = X3
| X1 = X3
| X1 = X2
| collinear(X1,X2,X3)
| ~ point(X3)
| ~ point(X2)
| ~ point(X1)
| on(X1,plane_for_points(X1,X2,X3)) ),
file('GEO003-0.ax',axiom_G7A) ).
cnf(axiom_G7B,axiom,
( X2 = X3
| X1 = X3
| X1 = X2
| collinear(X1,X2,X3)
| ~ point(X3)
| ~ point(X2)
| ~ point(X1)
| on(X2,plane_for_points(X1,X2,X3)) ),
file('GEO003-0.ax',axiom_G7B) ).
cnf(axiom_G7C,axiom,
( X2 = X3
| X1 = X3
| X1 = X2
| collinear(X1,X2,X3)
| ~ point(X3)
| ~ point(X2)
| ~ point(X1)
| on(X3,plane_for_points(X1,X2,X3)) ),
file('GEO003-0.ax',axiom_G7C) ).
cnf(axiom_G7D,axiom,
( X2 = X3
| X1 = X3
| X1 = X2
| collinear(X1,X2,X3)
| ~ point(X3)
| ~ point(X2)
| ~ point(X1)
| plane(plane_for_points(X1,X2,X3)) ),
file('GEO003-0.ax',axiom_G7D) ).
cnf(axiom_G7E,axiom,
( Z1 = Z2
| ~ plane(Z2)
| ~ on(X3,Z2)
| ~ on(X2,Z2)
| ~ on(X1,Z2)
| ~ plane(Z1)
| ~ on(X3,Z1)
| ~ on(X2,Z1)
| ~ on(X1,Z1)
| X2 = X3
| X1 = X3
| X1 = X2
| collinear(X1,X2,X3)
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('GEO003-0.ax',axiom_G7E) ).
cnf(axiom_G8A,axiom,
( on(Y1,Z1)
| X1 = X2
| ~ line(Y1)
| ~ point(X2)
| ~ point(X1)
| ~ plane(Z1)
| ~ on(X2,Z1)
| ~ on(X1,Z1)
| ~ on(X2,Y1)
| ~ on(X1,Y1) ),
file('GEO003-0.ax',axiom_G8A) ).
cnf(axiom_G9A,axiom,
( on(common_point_on_planes(Z1,Z2,X1),Z1)
| ~ point(X1)
| ~ on(X1,Z2)
| ~ on(X1,Z1)
| Z1 = Z2
| ~ plane(Z2)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G9A) ).
cnf(axiom_G9B,axiom,
( on(common_point_on_planes(Z1,Z2,X1),Z2)
| ~ point(X1)
| ~ on(X1,Z2)
| ~ on(X1,Z1)
| Z1 = Z2
| ~ plane(Z2)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G9B) ).
cnf(axiom_G9C,axiom,
( point(common_point_on_planes(Z1,Z2,X1))
| ~ point(X1)
| ~ on(X1,Z2)
| ~ on(X1,Z1)
| Z1 = Z2
| ~ plane(Z2)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G9C) ).
cnf(axiom_G9D,axiom,
( X1 != common_point_on_planes(Z1,Z2,X1)
| ~ point(X1)
| ~ on(X1,Z2)
| ~ on(X1,Z1)
| Z1 = Z2
| ~ plane(Z2)
| ~ plane(Z1) ),
file('GEO003-0.ax',axiom_G9D) ).
cnf(axiom_G10A,axiom,
( ~ collinear(X1,X2,X3)
| on(X1,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('GEO003-0.ax',axiom_G10A) ).
cnf(axiom_G10B,axiom,
( ~ collinear(X1,X2,X3)
| on(X2,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('GEO003-0.ax',axiom_G10B) ).
cnf(axiom_G10C,axiom,
( ~ collinear(X1,X2,X3)
| on(X3,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('GEO003-0.ax',axiom_G10C) ).
cnf(axiom_G10D,axiom,
( ~ collinear(X1,X2,X3)
| line(line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('GEO003-0.ax',axiom_G10D) ).
cnf(axiom_G10E,axiom,
( ~ line(Y)
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1)
| ~ on(X3,Y)
| ~ on(X2,Y)
| ~ on(X1,Y)
| collinear(X1,X2,X3) ),
file('GEO003-0.ax',axiom_G10E) ).
cnf(point1,hypothesis,
point(point1),
file('theBenchmark.p',point1) ).
cnf(point2,hypothesis,
point(point2),
file('theBenchmark.p',point2) ).
cnf(point3,hypothesis,
point(point3),
file('theBenchmark.p',point3) ).
cnf(line,hypothesis,
line(a_line),
file('theBenchmark.p',line) ).
cnf(point1_on_line,hypothesis,
on(point1,a_line),
file('theBenchmark.p',point1_on_line) ).
cnf(point2_on_line,hypothesis,
on(point2,a_line),
file('theBenchmark.p',point2_on_line) ).
cnf(point3_not_on_line,hypothesis,
~ on(point3,a_line),
file('theBenchmark.p',point3_not_on_line) ).
cnf(point1_not_point2,hypothesis,
point1 != point2,
file('theBenchmark.p',point1_not_point2) ).
cnf(point1_not_point3,hypothesis,
point1 != point3,
file('theBenchmark.p',point1_not_point3) ).
cnf(point2_not_point3,hypothesis,
point2 != point3,
file('theBenchmark.p',point2_not_point3) ).
cnf(prove_points_noncollinear,negated_conjecture,
collinear(point1,point2,point3),
file('theBenchmark.p',prove_points_noncollinear) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( line_from_to(Eq_x_0,Eq_x_1) = line_from_to(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( point_1_on_line(Eq_x_0) = point_1_on_line(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( point_2_on_line(Eq_x_0) = point_2_on_line(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( point_not_on_line(Eq_x_0) = point_not_on_line(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( point_on_plane(Eq_x_0) = point_on_plane(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( point_not_on_plane(Eq_x_0) = point_not_on_plane(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( plane_for_points(Eq_x_0,Eq_x_1,Eq_x_2) = plane_for_points(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( common_point_on_planes(Eq_x_0,Eq_x_1,Eq_x_2) = common_point_on_planes(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( line_through_3_points(Eq_x_0,Eq_x_1,Eq_x_2) = line_through_3_points(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( on(Eq_y_0,Eq_y_1)
| ~ on(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( point(Eq_y_0)
| ~ point(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( line(Eq_y_0)
| ~ line(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( plane(Eq_y_0)
| ~ plane(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( collinear(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ collinear(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.49 % CPULimit : 300
% 0.08/15.49 % WCLimit : 300
% 0.08/15.49 % DateTime : Sat Sep 19 07:21:14 UTC 2026
% 0.08/15.49 % CPUTime :
% 190.13/205.38 % SZS status Unsatisfiable for theBenchmark
% 190.13/205.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------