%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO147-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:36 AM UTC 2026
% Result : Unsatisfiable 30.14s 30.43s
% Output : Proof 30.14s
% 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(between_c_defn_1,axiom,
( B != D
| ~ between_c(A,B,C,D) ),
file('GEO004-1.ax',between_c_defn_1) ).
cnf(between_c_defn_2,axiom,
( part_of(ax1_sk1(D,C,B,A),A)
| ~ between_c(A,B,C,D) ),
file('GEO004-1.ax',between_c_defn_2) ).
cnf(between_c_defn_3,axiom,
( end_point(B,ax1_sk1(D,C,B,A))
| ~ between_c(A,B,C,D) ),
file('GEO004-1.ax',between_c_defn_3) ).
cnf(between_c_defn_4,axiom,
( end_point(D,ax1_sk1(D,C,B,A))
| ~ between_c(A,B,C,D) ),
file('GEO004-1.ax',between_c_defn_4) ).
cnf(between_c_defn_5,axiom,
( inner_point(C,ax1_sk1(D,C,B,A))
| ~ between_c(A,B,C,D) ),
file('GEO004-1.ax',between_c_defn_5) ).
cnf(between_c_defn_6,axiom,
( between_c(D,A,E,B)
| ~ inner_point(E,C)
| ~ end_point(B,C)
| ~ end_point(A,C)
| ~ part_of(C,D)
| A = B ),
file('GEO004-1.ax',between_c_defn_6) ).
cnf(between_o_defn_1,axiom,
( ordered_by(A,D,C)
| ordered_by(A,B,C)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',between_o_defn_1) ).
cnf(between_o_defn_2,axiom,
( ordered_by(A,C,B)
| ordered_by(A,B,C)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',between_o_defn_2) ).
cnf(between_o_defn_3,axiom,
( ordered_by(A,D,C)
| ordered_by(A,C,D)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',between_o_defn_3) ).
cnf(between_o_defn_4,axiom,
( ordered_by(A,C,B)
| ordered_by(A,C,D)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',between_o_defn_4) ).
cnf(between_o_defn_5,axiom,
( between_o(A,B,C,D)
| ~ ordered_by(A,C,D)
| ~ ordered_by(A,B,C) ),
file('GEO004-2.ax',between_o_defn_5) ).
cnf(between_o_defn_6,axiom,
( between_o(A,D,C,B)
| ~ ordered_by(A,C,D)
| ~ ordered_by(A,B,C) ),
file('GEO004-2.ax',between_o_defn_6) ).
cnf(start_point_defn_7,axiom,
( incident_o(A,B)
| ~ start_point(A,B) ),
file('GEO004-2.ax',start_point_defn_7) ).
cnf(start_point_defn_8,axiom,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| A = C
| ~ start_point(A,B) ),
file('GEO004-2.ax',start_point_defn_8) ).
cnf(start_point_defn_9,axiom,
( start_point(A,B)
| A != ax2_sk1(B,A)
| ~ incident_o(A,B) ),
file('GEO004-2.ax',start_point_defn_9) ).
cnf(start_point_defn_10,axiom,
( start_point(A,B)
| incident_o(ax2_sk1(B,A),B)
| ~ incident_o(A,B) ),
file('GEO004-2.ax',start_point_defn_10) ).
cnf(start_point_defn_11,axiom,
( start_point(A,B)
| ~ ordered_by(B,A,ax2_sk1(B,A))
| ~ incident_o(A,B) ),
file('GEO004-2.ax',start_point_defn_11) ).
cnf(finish_point_defn_12,axiom,
( incident_o(A,B)
| ~ finish_point(A,B) ),
file('GEO004-2.ax',finish_point_defn_12) ).
cnf(finish_point_defn_13,axiom,
( ordered_by(B,C,A)
| ~ incident_o(C,B)
| A = C
| ~ finish_point(A,B) ),
file('GEO004-2.ax',finish_point_defn_13) ).
cnf(finish_point_defn_14,axiom,
( finish_point(A,B)
| A != ax2_sk2(B,A)
| ~ incident_o(A,B) ),
file('GEO004-2.ax',finish_point_defn_14) ).
cnf(finish_point_defn_15,axiom,
( finish_point(A,B)
| incident_o(ax2_sk2(B,A),B)
| ~ incident_o(A,B) ),
file('GEO004-2.ax',finish_point_defn_15) ).
cnf(finish_point_defn_16,axiom,
( finish_point(A,B)
| ~ ordered_by(B,ax2_sk2(B,A),A)
| ~ incident_o(A,B) ),
file('GEO004-2.ax',finish_point_defn_16) ).
cnf(o1_17,axiom,
( incident_o(B,A)
| ~ ordered_by(A,B,C) ),
file('GEO004-2.ax',o1_17) ).
cnf(o1_18,axiom,
( incident_o(C,A)
| ~ ordered_by(A,B,C) ),
file('GEO004-2.ax',o1_18) ).
cnf(o2_19,axiom,
open(ax2_sk3(A)),
file('GEO004-2.ax',o2_19) ).
cnf(o2_20,axiom,
( incident_c(A,ax2_sk3(B))
| ~ incident_o(A,B) ),
file('GEO004-2.ax',o2_20) ).
cnf(o2_21,axiom,
( incident_o(A,B)
| ~ incident_c(A,ax2_sk3(B)) ),
file('GEO004-2.ax',o2_21) ).
cnf(o3_22,axiom,
( incident_c(E,ax2_sk4(A,D,C,B))
| ~ incident_o(E,A)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',o3_22) ).
cnf(o3_23,axiom,
( incident_o(E,A)
| ~ incident_c(E,ax2_sk4(A,D,C,B))
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',o3_23) ).
cnf(o3_24,axiom,
( between_c(ax2_sk4(A,D,C,B),B,C,D)
| ~ between_o(A,B,C,D) ),
file('GEO004-2.ax',o3_24) ).
cnf(o3_25,axiom,
( between_o(B,E,D,C)
| ~ between_c(A,E,D,C)
| incident_c(ax2_sk5(A,B,C,D,E),A)
| incident_o(ax2_sk5(A,B,C,D,E),B) ),
file('GEO004-2.ax',o3_25) ).
cnf(o3_26,axiom,
( between_o(B,E,D,C)
| ~ between_c(A,E,D,C)
| ~ incident_o(ax2_sk5(A,B,C,D,E),B)
| incident_o(ax2_sk5(A,B,C,D,E),B) ),
file('GEO004-2.ax',o3_26) ).
cnf(o3_27,axiom,
( between_o(B,E,D,C)
| ~ between_c(A,E,D,C)
| incident_c(ax2_sk5(A,B,C,D,E),A)
| ~ incident_c(ax2_sk5(A,B,C,D,E),A) ),
file('GEO004-2.ax',o3_27) ).
cnf(o3_28,axiom,
( between_o(B,E,D,C)
| ~ between_c(A,E,D,C)
| ~ incident_o(ax2_sk5(A,B,C,D,E),B)
| ~ incident_c(ax2_sk5(A,B,C,D,E),A) ),
file('GEO004-2.ax',o3_28) ).
cnf(o4_29,axiom,
start_point(ax2_sk6(A),A),
file('GEO004-2.ax',o4_29) ).
cnf(o5_30,axiom,
( incident_c(D,A)
| ~ incident_o(D,ax2_sk7(A,C,B))
| ~ incident_c(C,A)
| ~ incident_c(B,A)
| B = C
| ~ open(A) ),
file('GEO004-2.ax',o5_30) ).
cnf(o5_31,axiom,
( incident_o(D,ax2_sk7(A,C,B))
| ~ incident_c(D,A)
| ~ incident_c(C,A)
| ~ incident_c(B,A)
| B = C
| ~ open(A) ),
file('GEO004-2.ax',o5_31) ).
cnf(o5_32,axiom,
( ordered_by(ax2_sk7(A,C,B),B,C)
| ~ incident_c(C,A)
| ~ incident_c(B,A)
| B = C
| ~ open(A) ),
file('GEO004-2.ax',o5_32) ).
cnf(o6_33,axiom,
( A = B
| ordered_by(B,ax2_sk8(B,A),ax2_sk9(B,A))
| ordered_by(A,ax2_sk8(B,A),ax2_sk9(B,A)) ),
file('GEO004-2.ax',o6_33) ).
cnf(o6_34,axiom,
( A = B
| ~ ordered_by(A,ax2_sk8(B,A),ax2_sk9(B,A))
| ordered_by(A,ax2_sk8(B,A),ax2_sk9(B,A)) ),
file('GEO004-2.ax',o6_34) ).
cnf(o6_35,axiom,
( B = A
| ordered_by(A,ax2_sk8(A,B),ax2_sk9(A,B))
| ~ ordered_by(A,ax2_sk8(A,B),ax2_sk9(A,B)) ),
file('GEO004-2.ax',o6_35) ).
cnf(o6_36,axiom,
( B = A
| ~ ordered_by(B,ax2_sk8(A,B),ax2_sk9(A,B))
| ~ ordered_by(A,ax2_sk8(A,B),ax2_sk9(A,B)) ),
file('GEO004-2.ax',o6_36) ).
cnf(underlying_curve_defn_37,axiom,
( incident_c(C,A)
| ~ incident_o(C,B)
| A != underlying_curve(B) ),
file('GEO004-2.ax',underlying_curve_defn_37) ).
cnf(underlying_curve_defn_38,axiom,
( incident_o(C,B)
| ~ incident_c(C,A)
| A != underlying_curve(B) ),
file('GEO004-2.ax',underlying_curve_defn_38) ).
cnf(underlying_curve_defn_39,axiom,
( B = underlying_curve(A)
| incident_c(ax2_sk10(A,B),B)
| incident_o(ax2_sk10(A,B),A) ),
file('GEO004-2.ax',underlying_curve_defn_39) ).
cnf(underlying_curve_defn_40,axiom,
( B = underlying_curve(A)
| ~ incident_o(ax2_sk10(A,B),A)
| incident_o(ax2_sk10(A,B),A) ),
file('GEO004-2.ax',underlying_curve_defn_40) ).
cnf(underlying_curve_defn_41,axiom,
( B = underlying_curve(A)
| incident_c(ax2_sk10(A,B),B)
| ~ incident_c(ax2_sk10(A,B),B) ),
file('GEO004-2.ax',underlying_curve_defn_41) ).
cnf(underlying_curve_defn_42,axiom,
( B = underlying_curve(A)
| ~ incident_o(ax2_sk10(A,B),A)
| ~ incident_c(ax2_sk10(A,B),B) ),
file('GEO004-2.ax',underlying_curve_defn_42) ).
cnf(connect_defn_1,axiom,
( once(at_the_same_time(at(A,C),at(B,C)))
| ~ connect(A,B,C) ),
file('GEO004-3.ax',connect_defn_1) ).
cnf(connect_defn_2,axiom,
( connect(A,C,B)
| ~ once(at_the_same_time(at(A,B),at(C,B))) ),
file('GEO004-3.ax',connect_defn_2) ).
cnf(symmetry_of_at_the_same_time_3,axiom,
( once(at_the_same_time(B,A))
| ~ once(at_the_same_time(A,B)) ),
file('GEO004-3.ax',symmetry_of_at_the_same_time_3) ).
cnf(symmetry_of_at_the_same_time_4,axiom,
( once(at_the_same_time(B,A))
| ~ once(at_the_same_time(A,B)) ),
file('GEO004-3.ax',symmetry_of_at_the_same_time_4) ).
cnf(assciativity_of_at_the_same_time_5,axiom,
( once(at_the_same_time(A,at_the_same_time(B,C)))
| ~ once(at_the_same_time(at_the_same_time(A,B),C)) ),
file('GEO004-3.ax',assciativity_of_at_the_same_time_5) ).
cnf(assciativity_of_at_the_same_time_6,axiom,
( once(at_the_same_time(at_the_same_time(A,B),C))
| ~ once(at_the_same_time(A,at_the_same_time(B,C))) ),
file('GEO004-3.ax',assciativity_of_at_the_same_time_6) ).
cnf(idempotence_of_at_the_same_time_7,axiom,
( once(at_the_same_time(A,A))
| ~ once(A) ),
file('GEO004-3.ax',idempotence_of_at_the_same_time_7) ).
cnf(conjunction_at_the_same_time_8,axiom,
( once(A)
| ~ once(at_the_same_time(A,B)) ),
file('GEO004-3.ax',conjunction_at_the_same_time_8) ).
cnf(conjunction_at_the_same_time_9,axiom,
( once(B)
| ~ once(at_the_same_time(A,B)) ),
file('GEO004-3.ax',conjunction_at_the_same_time_9) ).
cnf(at_on_trajectory_10,axiom,
( incident_o(B,trajectory_of(A))
| ~ once(at(A,B)) ),
file('GEO004-3.ax',at_on_trajectory_10) ).
cnf(at_on_trajectory_11,axiom,
( once(at(B,A))
| ~ incident_o(A,trajectory_of(B)) ),
file('GEO004-3.ax',at_on_trajectory_11) ).
cnf(trajectories_are_oriented_curves_12,axiom,
trajectory_of(A) = ax3_sk1(A),
file('GEO004-3.ax',trajectories_are_oriented_curves_12) ).
cnf(homogeneous_behaviour_13,axiom,
( ~ ordered_by(trajectory_of(C),F,D)
| ~ ordered_by(trajectory_of(A),B,E)
| ~ once(at_the_same_time(at(A,E),at(C,F)))
| ~ once(at_the_same_time(at(A,B),at(C,D))) ),
file('GEO004-3.ax',homogeneous_behaviour_13) ).
cnf(localization_14,axiom,
( once(at_the_same_time(A,at(B,ax3_sk2(B,A))))
| ~ once(A) ),
file('GEO004-3.ax',localization_14) ).
cnf(t13_156,negated_conjecture,
connect(sk28,sk29,sk27),
file('theBenchmark.p',t13_156) ).
cnf(t13_157,negated_conjecture,
( ~ incident_o(sk27,trajectory_of(sk29))
| ~ incident_o(sk27,trajectory_of(sk28)) ),
file('theBenchmark.p',t13_157) ).
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(o3_26_true,plain,
$true,
inference(clause_is_true,[status(thm)],[o3_26]) ).
cnf(o3_27_true,plain,
$true,
inference(clause_is_true,[status(thm)],[o3_27]) ).
cnf(o6_34_true,plain,
$true,
inference(clause_is_true,[status(thm)],[o6_34]) ).
cnf(o6_35_true,plain,
$true,
inference(clause_is_true,[status(thm)],[o6_35]) ).
cnf(underlying_curve_defn_40_true,plain,
$true,
inference(clause_is_true,[status(thm)],[underlying_curve_defn_40]) ).
cnf(underlying_curve_defn_41_true,plain,
$true,
inference(clause_is_true,[status(thm)],[underlying_curve_defn_41]) ).
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,
( ax1_sk1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = ax1_sk1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( ax2_sk1(Eq_x_0,Eq_x_1) = ax2_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_20,axiom,
( ax2_sk2(Eq_x_0,Eq_x_1) = ax2_sk2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( ax2_sk3(Eq_x_0) = ax2_sk3(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( ax2_sk4(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = ax2_sk4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( ax2_sk5(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = ax2_sk5(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( ax2_sk6(Eq_x_0) = ax2_sk6(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( ax2_sk7(Eq_x_0,Eq_x_1,Eq_x_2) = ax2_sk7(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_26,axiom,
( ax2_sk8(Eq_x_0,Eq_x_1) = ax2_sk8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( ax2_sk9(Eq_x_0,Eq_x_1) = ax2_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_28,axiom,
( underlying_curve(Eq_x_0) = underlying_curve(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( ax2_sk10(Eq_x_0,Eq_x_1) = ax2_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_30,axiom,
( at(Eq_x_0,Eq_x_1) = at(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( at_the_same_time(Eq_x_0,Eq_x_1) = at_the_same_time(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( trajectory_of(Eq_x_0) = trajectory_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( ax3_sk1(Eq_x_0) = ax3_sk1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( ax3_sk2(Eq_x_0,Eq_x_1) = ax3_sk2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,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_36,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_37,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_38,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_39,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_40,axiom,
( closed(Eq_y_0)
| ~ closed(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( open(Eq_y_0)
| ~ open(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( between_c(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ between_c(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( between_o(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ between_o(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( ordered_by(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ordered_by(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_45,axiom,
( start_point(Eq_y_0,Eq_y_1)
| ~ start_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_46,axiom,
( incident_o(Eq_y_0,Eq_y_1)
| ~ incident_o(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_47,axiom,
( finish_point(Eq_y_0,Eq_y_1)
| ~ finish_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_48,axiom,
( connect(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ connect(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_49,axiom,
( once(Eq_y_0)
| ~ once(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.02 % Problem : GEO147-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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 07:35:52 UTC 2026
% 0.08/0.35 % CPUTime :
% 30.14/30.43 % SZS status Unsatisfiable for theBenchmark
% 30.14/30.43 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------