%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO080-1 : TPTP v9.3.1. Released v2.4.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 : 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 : Thu Sep 24 08:39:26 AM UTC 2026
% Result : Unsatisfiable 0.13s 10.40s
% Output : Proof 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(part_of_defn_1,axiom,
( incident_c(C,B)
| ~ incident_c(C,A)
| ~ part_of(A,B) ),
file('GEO004-0.ax',part_of_defn_1) ).
cnf(part_of_defn_2,axiom,
( part_of(A,B)
| incident_c(ax0_sk1(A,B),A) ),
file('GEO004-0.ax',part_of_defn_2) ).
cnf(part_of_defn_3,axiom,
( part_of(A,B)
| ~ incident_c(ax0_sk1(A,B),B) ),
file('GEO004-0.ax',part_of_defn_3) ).
cnf(sum_defn_4,axiom,
( incident_c(D,C)
| incident_c(D,B)
| ~ incident_c(D,A)
| A != sum(B,C) ),
file('GEO004-0.ax',sum_defn_4) ).
cnf(sum_defn_5,axiom,
( incident_c(D,A)
| ~ incident_c(D,B)
| A != sum(B,C) ),
file('GEO004-0.ax',sum_defn_5) ).
cnf(sum_defn_6,axiom,
( incident_c(D,A)
| ~ incident_c(D,C)
| A != sum(B,C) ),
file('GEO004-0.ax',sum_defn_6) ).
cnf(sum_defn_7,axiom,
( C = sum(B,A)
| incident_c(ax0_sk2(A,B,C),A)
| incident_c(ax0_sk2(A,B,C),B)
| incident_c(ax0_sk2(A,B,C),C) ),
file('GEO004-0.ax',sum_defn_7) ).
cnf(sum_defn_8,axiom,
( C = sum(B,A)
| ~ incident_c(ax0_sk2(A,B,C),C)
| incident_c(ax0_sk2(A,B,C),C) ),
file('GEO004-0.ax',sum_defn_8) ).
cnf(sum_defn_9,axiom,
( C = sum(B,A)
| incident_c(ax0_sk2(A,B,C),A)
| incident_c(ax0_sk2(A,B,C),B)
| ~ incident_c(ax0_sk2(A,B,C),B) ),
file('GEO004-0.ax',sum_defn_9) ).
cnf(sum_defn_10,axiom,
( C = sum(B,A)
| incident_c(ax0_sk2(A,B,C),A)
| incident_c(ax0_sk2(A,B,C),B)
| ~ incident_c(ax0_sk2(A,B,C),A) ),
file('GEO004-0.ax',sum_defn_10) ).
cnf(sum_defn_11,axiom,
( C = sum(B,A)
| ~ incident_c(ax0_sk2(A,B,C),C)
| ~ incident_c(ax0_sk2(A,B,C),B) ),
file('GEO004-0.ax',sum_defn_11) ).
cnf(sum_defn_12,axiom,
( C = sum(B,A)
| ~ incident_c(ax0_sk2(A,B,C),C)
| ~ incident_c(ax0_sk2(A,B,C),A) ),
file('GEO004-0.ax',sum_defn_12) ).
cnf(end_point_defn_13,axiom,
( incident_c(A,B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',end_point_defn_13) ).
cnf(end_point_defn_14,axiom,
( part_of(D,C)
| part_of(C,D)
| ~ incident_c(A,D)
| ~ incident_c(A,C)
| ~ part_of(D,B)
| ~ part_of(C,B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',end_point_defn_14) ).
cnf(end_point_defn_15,axiom,
( end_point(A,B)
| part_of(ax0_sk3(B,A),B)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_15) ).
cnf(end_point_defn_16,axiom,
( end_point(A,B)
| part_of(ax0_sk4(B,A),B)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_16) ).
cnf(end_point_defn_17,axiom,
( end_point(A,B)
| incident_c(A,ax0_sk3(B,A))
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_17) ).
cnf(end_point_defn_18,axiom,
( end_point(A,B)
| incident_c(A,ax0_sk4(B,A))
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_18) ).
cnf(end_point_defn_19,axiom,
( end_point(A,B)
| ~ part_of(ax0_sk3(B,A),ax0_sk4(B,A))
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_19) ).
cnf(end_point_defn_20,axiom,
( end_point(A,B)
| ~ part_of(ax0_sk4(B,A),ax0_sk3(B,A))
| ~ incident_c(A,B) ),
file('GEO004-0.ax',end_point_defn_20) ).
cnf(inner_point_defn_21,axiom,
( incident_c(A,B)
| ~ inner_point(A,B) ),
file('GEO004-0.ax',inner_point_defn_21) ).
cnf(inner_point_defn_22,axiom,
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
file('GEO004-0.ax',inner_point_defn_22) ).
cnf(inner_point_defn_23,axiom,
( inner_point(A,B)
| end_point(A,B)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',inner_point_defn_23) ).
cnf(meet_defn_24,axiom,
( incident_c(A,B)
| ~ meet(A,B,C) ),
file('GEO004-0.ax',meet_defn_24) ).
cnf(meet_defn_25,axiom,
( incident_c(A,C)
| ~ meet(A,B,C) ),
file('GEO004-0.ax',meet_defn_25) ).
cnf(meet_defn_26,axiom,
( end_point(D,B)
| ~ incident_c(D,C)
| ~ incident_c(D,B)
| ~ meet(A,B,C) ),
file('GEO004-0.ax',meet_defn_26) ).
cnf(meet_defn_27,axiom,
( end_point(D,C)
| ~ incident_c(D,C)
| ~ incident_c(D,B)
| ~ meet(A,B,C) ),
file('GEO004-0.ax',meet_defn_27) ).
cnf(meet_defn_28,axiom,
( meet(A,B,C)
| incident_c(ax0_sk5(C,B,A),B)
| ~ incident_c(A,C)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',meet_defn_28) ).
cnf(meet_defn_29,axiom,
( meet(A,B,C)
| incident_c(ax0_sk5(C,B,A),C)
| ~ incident_c(A,C)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',meet_defn_29) ).
cnf(meet_defn_30,axiom,
( meet(A,B,C)
| ~ end_point(ax0_sk5(C,B,A),C)
| ~ end_point(ax0_sk5(C,B,A),B)
| ~ incident_c(A,C)
| ~ incident_c(A,B) ),
file('GEO004-0.ax',meet_defn_30) ).
cnf(closed_defn_31,axiom,
( ~ end_point(B,A)
| ~ closed(A) ),
file('GEO004-0.ax',closed_defn_31) ).
cnf(closed_defn_32,axiom,
( closed(A)
| end_point(ax0_sk6(A),A) ),
file('GEO004-0.ax',closed_defn_32) ).
cnf(open_defn_33,axiom,
( end_point(ax0_sk7(A),A)
| ~ open(A) ),
file('GEO004-0.ax',open_defn_33) ).
cnf(open_defn_34,axiom,
( open(B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',open_defn_34) ).
cnf(c1_35,axiom,
( open(A)
| A = B
| ~ part_of(A,B) ),
file('GEO004-0.ax',c1_35) ).
cnf(c2_36,axiom,
( part_of(D,A)
| part_of(A,D)
| part_of(C,A)
| part_of(A,C)
| part_of(D,C)
| part_of(C,D)
| ~ end_point(E,D)
| ~ end_point(E,C)
| ~ end_point(E,A)
| ~ part_of(D,B)
| ~ part_of(C,B)
| ~ part_of(A,B) ),
file('GEO004-0.ax',c2_36) ).
cnf(c3_37,axiom,
inner_point(ax0_sk8(A),A),
file('GEO004-0.ax',c3_37) ).
cnf(c4_38,axiom,
( meet(A,ax0_sk9(A,B),ax0_sk10(A,B))
| ~ inner_point(A,B) ),
file('GEO004-0.ax',c4_38) ).
cnf(c4_39,axiom,
( B = sum(ax0_sk9(A,B),ax0_sk10(A,B))
| ~ inner_point(A,B) ),
file('GEO004-0.ax',c4_39) ).
cnf(c5_40,axiom,
( C = D
| A = D
| A = C
| ~ end_point(D,B)
| ~ end_point(C,B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',c5_40) ).
cnf(c6_41,axiom,
( end_point(ax0_sk11(A,B),B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',c6_41) ).
cnf(c6_42,axiom,
( A != ax0_sk11(A,B)
| ~ end_point(A,B) ),
file('GEO004-0.ax',c6_42) ).
cnf(c7_43,axiom,
( meet(E,C,D)
| ~ end_point(E,C)
| A != sum(C,D)
| ~ meet(B,C,D)
| ~ closed(A) ),
file('GEO004-0.ax',c7_43) ).
cnf(c8_44,axiom,
( ax0_sk12(C,B) = sum(B,C)
| ~ meet(A,B,C) ),
file('GEO004-0.ax',c8_44) ).
cnf(c9_45,axiom,
( B = A
| incident_c(ax0_sk13(A,B),A)
| incident_c(ax0_sk13(A,B),B) ),
file('GEO004-0.ax',c9_45) ).
cnf(c9_46,axiom,
( B = A
| ~ incident_c(ax0_sk13(A,B),B)
| incident_c(ax0_sk13(A,B),B) ),
file('GEO004-0.ax',c9_46) ).
cnf(c9_47,axiom,
( B = A
| incident_c(ax0_sk13(A,B),A)
| ~ incident_c(ax0_sk13(A,B),A) ),
file('GEO004-0.ax',c9_47) ).
cnf(c9_48,axiom,
( B = A
| ~ incident_c(ax0_sk13(A,B),B)
| ~ incident_c(ax0_sk13(A,B),A) ),
file('GEO004-0.ax',c9_48) ).
cnf(prove_reflexivity,negated_conjecture,
~ part_of(sk14,sk14),
file('theBenchmark.p',prove_reflexivity) ).
cnf(sum_defn_8_true,plain,
$true,
inference(clause_is_true,[status(thm)],[sum_defn_8]) ).
cnf(sum_defn_9_true,plain,
$true,
inference(clause_is_true,[status(thm)],[sum_defn_9]) ).
cnf(sum_defn_10_true,plain,
$true,
inference(clause_is_true,[status(thm)],[sum_defn_10]) ).
cnf(c9_46_true,plain,
$true,
inference(clause_is_true,[status(thm)],[c9_46]) ).
cnf(c9_47_true,plain,
$true,
inference(clause_is_true,[status(thm)],[c9_47]) ).
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,
( ax0_sk1(Eq_x_0,Eq_x_1) = ax0_sk1(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,
( sum(Eq_x_0,Eq_x_1) = sum(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( ax0_sk2(Eq_x_0,Eq_x_1,Eq_x_2) = ax0_sk2(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_7,axiom,
( ax0_sk3(Eq_x_0,Eq_x_1) = ax0_sk3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( ax0_sk4(Eq_x_0,Eq_x_1) = ax0_sk4(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( ax0_sk5(Eq_x_0,Eq_x_1,Eq_x_2) = ax0_sk5(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_10,axiom,
( ax0_sk6(Eq_x_0) = ax0_sk6(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( ax0_sk7(Eq_x_0) = ax0_sk7(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( ax0_sk8(Eq_x_0) = ax0_sk8(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( ax0_sk9(Eq_x_0,Eq_x_1) = ax0_sk9(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( ax0_sk10(Eq_x_0,Eq_x_1) = ax0_sk10(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( ax0_sk11(Eq_x_0,Eq_x_1) = ax0_sk11(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( ax0_sk12(Eq_x_0,Eq_x_1) = ax0_sk12(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( ax0_sk13(Eq_x_0,Eq_x_1) = ax0_sk13(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( part_of(Eq_y_0,Eq_y_1)
| ~ part_of(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( incident_c(Eq_y_0,Eq_y_1)
| ~ incident_c(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( end_point(Eq_y_0,Eq_y_1)
| ~ end_point(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( inner_point(Eq_y_0,Eq_y_1)
| ~ inner_point(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( meet(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ meet(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(equality_23,axiom,
( closed(Eq_y_0)
| ~ closed(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( open(Eq_y_0)
| ~ open(Eq_x_0)
| 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 : GEO080-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 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.09/10.36 % Computer : n014.cluster.edu
% 0.09/10.36 % Model : x86_64 x86_64
% 0.09/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.36 % Memory : 8046.5625MB
% 0.09/10.36 % OS : Linux 6.8.0-71-generic
% 0.09/10.36 % CPULimit : 300
% 0.09/10.36 % WCLimit : 300
% 0.09/10.36 % DateTime : Sat Sep 19 07:20:01 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.13/10.40 % SZS status Unsatisfiable for theBenchmark
% 0.13/10.40 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------