%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO117-1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n015.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 : Tue May 5 04:19:21 PM UTC 2026
% Result : Unsatisfiable 0.27s 1.60s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 115)
% Comments :
%------------------------------------------------------------------------------
cnf(o3_28,axiom,
( between_o(X2,X5,X4,X3)
| ~ incident_c(ax2_sk5(X1,X2,X3,X4,X5),X1)
| ~ incident_o(ax2_sk5(X1,X2,X3,X4,X5),X2)
| ~ between_c(X1,X5,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o3_28) ).
cnf(o3_25,axiom,
( incident_o(ax2_sk5(X1,X2,X3,X4,X5),X2)
| incident_c(ax2_sk5(X1,X2,X3,X4,X5),X1)
| between_o(X2,X5,X4,X3)
| ~ between_c(X1,X5,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o3_25) ).
cnf(o3_23,axiom,
( incident_o(X5,X1)
| ~ between_o(X1,X2,X3,X4)
| ~ incident_c(X5,ax2_sk4(X1,X4,X3,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o3_23) ).
cnf(o3_24,axiom,
( between_c(ax2_sk4(X1,X4,X3,X2),X2,X3,X4)
| ~ between_o(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o3_24) ).
cnf(o3_22,axiom,
( incident_c(X5,ax2_sk4(X1,X4,X3,X2))
| ~ between_o(X1,X2,X3,X4)
| ~ incident_o(X5,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o3_22) ).
cnf(between_c_defn_2,axiom,
( part_of(ax1_sk1(X4,X3,X2,X1),X1)
| ~ between_c(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_2) ).
cnf(between_c_defn_5,axiom,
( inner_point(X3,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_5) ).
cnf(between_c_defn_3,axiom,
( end_point(X2,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_3) ).
cnf(between_c_defn_4,axiom,
( end_point(X4,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_4) ).
cnf(between_o_defn_2,axiom,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_2) ).
cnf(between_o_defn_4,axiom,
( ordered_by(X1,X3,X4)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_4) ).
cnf(between_o_defn_1,axiom,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X4,X3)
| ~ between_o(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_1) ).
cnf(between_o_defn_3,axiom,
( ordered_by(X1,X3,X4)
| ordered_by(X1,X4,X3)
| ~ between_o(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_3) ).
cnf(meet_defn_30,axiom,
( meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| ~ end_point(ax0_sk5(X3,X2,X1),X2)
| ~ end_point(ax0_sk5(X3,X2,X1),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_30) ).
cnf(between_o_defn_5,axiom,
( between_o(X1,X2,X3,X4)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_5) ).
cnf(between_o_defn_6,axiom,
( between_o(X1,X4,X3,X2)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',between_o_defn_6) ).
cnf(sum_defn_12,axiom,
( X3 = sum(X2,X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_12) ).
cnf(sum_defn_11,axiom,
( X3 = sum(X2,X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X2)
| ~ incident_c(ax0_sk2(X1,X2,X3),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_11) ).
cnf(between_c_defn_1,axiom,
( ~ between_c(X1,X2,X3,X4)
| X2 != X4 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_1) ).
cnf(sum_defn_7,axiom,
( incident_c(ax0_sk2(X1,X2,X3),X3)
| incident_c(ax0_sk2(X1,X2,X3),X2)
| incident_c(ax0_sk2(X1,X2,X3),X1)
| X3 = sum(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_7) ).
cnf(between_c_defn_6,axiom,
( X1 = X2
| between_c(X4,X1,X5,X2)
| ~ part_of(X3,X4)
| ~ end_point(X1,X3)
| ~ end_point(X2,X3)
| ~ inner_point(X5,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_6) ).
cnf(o6_36,axiom,
( X2 = X1
| ~ ordered_by(X1,ax2_sk8(X1,X2),ax2_sk9(X1,X2))
| ~ ordered_by(X2,ax2_sk8(X1,X2),ax2_sk9(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o6_36) ).
cnf(o5_30,axiom,
( X2 = X3
| incident_c(X4,X1)
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1)
| ~ incident_o(X4,ax2_sk7(X1,X3,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o5_30) ).
cnf(c2_36,axiom,
( part_of(X3,X4)
| part_of(X4,X3)
| part_of(X1,X3)
| part_of(X3,X1)
| part_of(X1,X4)
| part_of(X4,X1)
| ~ part_of(X1,X2)
| ~ part_of(X3,X2)
| ~ part_of(X4,X2)
| ~ end_point(X5,X1)
| ~ end_point(X5,X3)
| ~ end_point(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c2_36) ).
cnf(meet_defn_28,axiom,
( incident_c(ax0_sk5(X3,X2,X1),X2)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_28) ).
cnf(meet_defn_29,axiom,
( incident_c(ax0_sk5(X3,X2,X1),X3)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_29) ).
cnf(o5_32,axiom,
( X2 = X3
| ordered_by(ax2_sk7(X1,X3,X2),X2,X3)
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o5_32) ).
cnf(o6_33,axiom,
( ordered_by(X1,ax2_sk8(X2,X1),ax2_sk9(X2,X1))
| ordered_by(X2,ax2_sk8(X2,X1),ax2_sk9(X2,X1))
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o6_33) ).
cnf(o5_31,axiom,
( X2 = X3
| incident_o(X4,ax2_sk7(X1,X3,X2))
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1)
| ~ incident_c(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o5_31) ).
cnf(c7_43,axiom,
( meet(X5,X3,X4)
| ~ closed(X1)
| ~ meet(X2,X3,X4)
| X1 != sum(X3,X4)
| ~ end_point(X5,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c7_43) ).
cnf(finish_point_defn_16,axiom,
( finish_point(X1,X2)
| ~ incident_o(X1,X2)
| ~ ordered_by(X2,ax2_sk2(X2,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',finish_point_defn_16) ).
cnf(start_point_defn_11,axiom,
( start_point(X1,X2)
| ~ incident_o(X1,X2)
| ~ ordered_by(X2,X1,ax2_sk1(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',start_point_defn_11) ).
cnf(meet_defn_26,axiom,
( end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_26) ).
cnf(meet_defn_27,axiom,
( end_point(X4,X3)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_27) ).
cnf(end_point_defn_14,axiom,
( part_of(X3,X4)
| part_of(X4,X3)
| ~ end_point(X1,X2)
| ~ part_of(X3,X2)
| ~ part_of(X4,X2)
| ~ incident_c(X1,X3)
| ~ incident_c(X1,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_14) ).
cnf(end_point_defn_20,axiom,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ part_of(ax0_sk4(X2,X1),ax0_sk3(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_20) ).
cnf(end_point_defn_19,axiom,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ part_of(ax0_sk3(X2,X1),ax0_sk4(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_19) ).
cnf(underlying_curve_defn_42,axiom,
( X2 = underlying_curve(X1)
| ~ incident_c(ax2_sk10(X1,X2),X2)
| ~ incident_o(ax2_sk10(X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',underlying_curve_defn_42) ).
cnf(c4_38,axiom,
( meet(X1,ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c4_38) ).
cnf(c9_48,axiom,
( X2 = X1
| ~ incident_c(ax0_sk13(X1,X2),X1)
| ~ incident_c(ax0_sk13(X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c9_48) ).
cnf(c8_44,axiom,
( ax0_sk12(X3,X2) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c8_44) ).
cnf(start_point_defn_8,axiom,
( X1 = X3
| ordered_by(X2,X1,X3)
| ~ start_point(X1,X2)
| ~ incident_o(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',start_point_defn_8) ).
cnf(finish_point_defn_13,axiom,
( X1 = X3
| ordered_by(X2,X3,X1)
| ~ finish_point(X1,X2)
| ~ incident_o(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',finish_point_defn_13) ).
cnf(o1_17,axiom,
( incident_o(X2,X1)
| ~ ordered_by(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o1_17) ).
cnf(o1_18,axiom,
( incident_o(X3,X1)
| ~ ordered_by(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o1_18) ).
cnf(meet_defn_24,axiom,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_24) ).
cnf(meet_defn_25,axiom,
( incident_c(X1,X3)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_25) ).
cnf(c4_39,axiom,
( X2 = sum(ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c4_39) ).
cnf(underlying_curve_defn_39,axiom,
( incident_o(ax2_sk10(X1,X2),X1)
| incident_c(ax2_sk10(X1,X2),X2)
| X2 = underlying_curve(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',underlying_curve_defn_39) ).
cnf(c9_45,axiom,
( incident_c(ax0_sk13(X1,X2),X2)
| incident_c(ax0_sk13(X1,X2),X1)
| X2 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c9_45) ).
cnf(part_of_defn_3,axiom,
( part_of(X1,X2)
| ~ incident_c(ax0_sk1(X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_3) ).
cnf(finish_point_defn_15,axiom,
( incident_o(ax2_sk2(X2,X1),X2)
| finish_point(X1,X2)
| ~ incident_o(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',finish_point_defn_15) ).
cnf(start_point_defn_10,axiom,
( incident_o(ax2_sk1(X2,X1),X2)
| start_point(X1,X2)
| ~ incident_o(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',start_point_defn_10) ).
cnf(end_point_defn_16,axiom,
( part_of(ax0_sk4(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_16) ).
cnf(end_point_defn_15,axiom,
( part_of(ax0_sk3(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_15) ).
cnf(end_point_defn_18,axiom,
( incident_c(X1,ax0_sk4(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_18) ).
cnf(end_point_defn_17,axiom,
( incident_c(X1,ax0_sk3(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_17) ).
cnf(sum_defn_4,axiom,
( incident_c(X4,X2)
| incident_c(X4,X3)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_4) ).
cnf(c5_40,axiom,
( X1 = X3
| X1 = X4
| X3 = X4
| ~ end_point(X1,X2)
| ~ end_point(X3,X2)
| ~ end_point(X4,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c5_40) ).
cnf(c6_41,axiom,
( end_point(ax0_sk11(X1,X2),X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c6_41) ).
cnf(finish_point_defn_14,axiom,
( finish_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk2(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',finish_point_defn_14) ).
cnf(start_point_defn_9,axiom,
( start_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk1(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',start_point_defn_9) ).
cnf(sum_defn_5,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_5) ).
cnf(sum_defn_6,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_6) ).
cnf(part_of_defn_1,axiom,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_1) ).
cnf(part_of_defn_2,axiom,
( incident_c(ax0_sk1(X1,X2),X1)
| part_of(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_2) ).
cnf(inner_point_defn_23,axiom,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_23) ).
cnf(theorem_4_4_133,negated_conjecture,
ordered_by(sk25,sk26,sk26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_4_133) ).
cnf(o2_21,axiom,
( incident_o(X1,X2)
| ~ incident_c(X1,ax2_sk3(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o2_21) ).
cnf(c6_42,axiom,
( ~ end_point(X1,X2)
| X1 != ax0_sk11(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c6_42) ).
cnf(underlying_curve_defn_38,axiom,
( incident_o(X3,X2)
| X1 != underlying_curve(X2)
| ~ incident_c(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',underlying_curve_defn_38) ).
cnf(underlying_curve_defn_37,axiom,
( incident_c(X3,X1)
| X1 != underlying_curve(X2)
| ~ incident_o(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',underlying_curve_defn_37) ).
cnf(inner_point_defn_22,axiom,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_22) ).
cnf(o2_20,axiom,
( incident_c(X1,ax2_sk3(X2))
| ~ incident_o(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o2_20) ).
cnf(finish_point_defn_12,axiom,
( incident_o(X1,X2)
| ~ finish_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',finish_point_defn_12) ).
cnf(start_point_defn_7,axiom,
( incident_o(X1,X2)
| ~ start_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',start_point_defn_7) ).
cnf(inner_point_defn_21,axiom,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_21) ).
cnf(end_point_defn_13,axiom,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_13) ).
cnf(closed_defn_31,axiom,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',closed_defn_31) ).
cnf(c1_35,axiom,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c1_35) ).
cnf(open_defn_33,axiom,
( end_point(ax0_sk7(X1),X1)
| ~ open(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',open_defn_33) ).
cnf(open_defn_34,axiom,
( open(X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',open_defn_34) ).
cnf(closed_defn_32,axiom,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',closed_defn_32) ).
cnf(o4_29,axiom,
start_point(ax2_sk6(X1),X1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o4_29) ).
cnf(c3_37,axiom,
inner_point(ax0_sk8(X1),X1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c3_37) ).
cnf(o2_19,axiom,
open(ax2_sk3(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o2_19) ).
cnf(i_0_86,axiom,
( between_o(X2,X5,X4,X3)
| ~ incident_c(ax2_sk5(X1,X2,X3,X4,X5),X1)
| ~ incident_o(ax2_sk5(X1,X2,X3,X4,X5),X2)
| ~ between_c(X1,X5,X4,X3) ),
o3_28,
[final] ).
cnf(i_0_87,axiom,
( incident_o(ax2_sk5(X1,X2,X3,X4,X5),X2)
| incident_c(ax2_sk5(X1,X2,X3,X4,X5),X1)
| between_o(X2,X5,X4,X3)
| ~ between_c(X1,X5,X4,X3) ),
o3_25,
[final] ).
cnf(i_0_88,axiom,
( incident_o(X5,X1)
| ~ between_o(X1,X2,X3,X4)
| ~ incident_c(X5,ax2_sk4(X1,X4,X3,X2)) ),
o3_23,
[final] ).
cnf(i_0_89,axiom,
( between_c(ax2_sk4(X1,X4,X3,X2),X2,X3,X4)
| ~ between_o(X1,X2,X3,X4) ),
o3_24,
[final] ).
cnf(i_0_90,axiom,
( incident_c(X5,ax2_sk4(X1,X4,X3,X2))
| ~ between_o(X1,X2,X3,X4)
| ~ incident_o(X5,X1) ),
o3_22,
[final] ).
cnf(i_0_91,axiom,
( part_of(ax1_sk1(X4,X3,X2,X1),X1)
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_2,
[final] ).
cnf(i_0_92,axiom,
( inner_point(X3,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_5,
[final] ).
cnf(i_0_93,axiom,
( end_point(X2,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_3,
[final] ).
cnf(i_0_94,axiom,
( end_point(X4,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_4,
[final] ).
cnf(i_0_95,axiom,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X2,X3,X4) ),
between_o_defn_2,
[final] ).
cnf(i_0_96,axiom,
( ordered_by(X1,X3,X4)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X2,X3,X4) ),
between_o_defn_4,
[final] ).
cnf(i_0_97,axiom,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X4,X3)
| ~ between_o(X1,X2,X3,X4) ),
between_o_defn_1,
[final] ).
cnf(i_0_98,axiom,
( ordered_by(X1,X3,X4)
| ordered_by(X1,X4,X3)
| ~ between_o(X1,X2,X3,X4) ),
between_o_defn_3,
[final] ).
cnf(i_0_99,axiom,
( meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| ~ end_point(ax0_sk5(X3,X2,X1),X2)
| ~ end_point(ax0_sk5(X3,X2,X1),X3) ),
meet_defn_30,
[final] ).
cnf(i_0_100,axiom,
( between_o(X1,X2,X3,X4)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
between_o_defn_5,
[final] ).
cnf(i_0_101,axiom,
( between_o(X1,X4,X3,X2)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
between_o_defn_6,
[final] ).
cnf(i_0_102,axiom,
( X3 = sum(X2,X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X3) ),
sum_defn_12,
[final] ).
cnf(i_0_103,axiom,
( X3 = sum(X2,X1)
| ~ incident_c(ax0_sk2(X1,X2,X3),X2)
| ~ incident_c(ax0_sk2(X1,X2,X3),X3) ),
sum_defn_11,
[final] ).
cnf(i_0_104,axiom,
( ~ between_c(X1,X2,X3,X4)
| X2 != X4 ),
between_c_defn_1,
[final] ).
cnf(i_0_105,axiom,
( incident_c(ax0_sk2(X1,X2,X3),X3)
| incident_c(ax0_sk2(X1,X2,X3),X2)
| incident_c(ax0_sk2(X1,X2,X3),X1)
| X3 = sum(X2,X1) ),
sum_defn_7,
[final] ).
cnf(i_0_106,axiom,
( X1 = X2
| between_c(X4,X1,X5,X2)
| ~ part_of(X3,X4)
| ~ end_point(X1,X3)
| ~ end_point(X2,X3)
| ~ inner_point(X5,X3) ),
between_c_defn_6,
[final] ).
cnf(i_0_107,axiom,
( X2 = X1
| ~ ordered_by(X1,ax2_sk8(X1,X2),ax2_sk9(X1,X2))
| ~ ordered_by(X2,ax2_sk8(X1,X2),ax2_sk9(X1,X2)) ),
o6_36,
[final] ).
cnf(i_0_108,axiom,
( X2 = X3
| incident_c(X4,X1)
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1)
| ~ incident_o(X4,ax2_sk7(X1,X3,X2)) ),
o5_30,
[final] ).
cnf(i_0_109,axiom,
( part_of(X3,X4)
| part_of(X4,X3)
| part_of(X1,X3)
| part_of(X3,X1)
| part_of(X1,X4)
| part_of(X4,X1)
| ~ part_of(X1,X2)
| ~ part_of(X3,X2)
| ~ part_of(X4,X2)
| ~ end_point(X5,X1)
| ~ end_point(X5,X3)
| ~ end_point(X5,X4) ),
c2_36,
[final] ).
cnf(i_0_110,axiom,
( incident_c(ax0_sk5(X3,X2,X1),X2)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
meet_defn_28,
[final] ).
cnf(i_0_111,axiom,
( incident_c(ax0_sk5(X3,X2,X1),X3)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
meet_defn_29,
[final] ).
cnf(i_0_112,axiom,
( X2 = X3
| ordered_by(ax2_sk7(X1,X3,X2),X2,X3)
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1) ),
o5_32,
[final] ).
cnf(i_0_113,axiom,
( ordered_by(X1,ax2_sk8(X2,X1),ax2_sk9(X2,X1))
| ordered_by(X2,ax2_sk8(X2,X1),ax2_sk9(X2,X1))
| X1 = X2 ),
o6_33,
[final] ).
cnf(i_0_114,axiom,
( X2 = X3
| incident_o(X4,ax2_sk7(X1,X3,X2))
| ~ open(X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X3,X1)
| ~ incident_c(X4,X1) ),
o5_31,
[final] ).
cnf(i_0_115,axiom,
( meet(X5,X3,X4)
| ~ closed(X1)
| ~ meet(X2,X3,X4)
| X1 != sum(X3,X4)
| ~ end_point(X5,X3) ),
c7_43,
[final] ).
cnf(i_0_116,axiom,
( finish_point(X1,X2)
| ~ incident_o(X1,X2)
| ~ ordered_by(X2,ax2_sk2(X2,X1),X1) ),
finish_point_defn_16,
[final] ).
cnf(i_0_117,axiom,
( start_point(X1,X2)
| ~ incident_o(X1,X2)
| ~ ordered_by(X2,X1,ax2_sk1(X2,X1)) ),
start_point_defn_11,
[final] ).
cnf(i_0_118,axiom,
( end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_26,
[final] ).
cnf(i_0_119,axiom,
( end_point(X4,X3)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_27,
[final] ).
cnf(i_0_120,axiom,
( part_of(X3,X4)
| part_of(X4,X3)
| ~ end_point(X1,X2)
| ~ part_of(X3,X2)
| ~ part_of(X4,X2)
| ~ incident_c(X1,X3)
| ~ incident_c(X1,X4) ),
end_point_defn_14,
[final] ).
cnf(i_0_121,axiom,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ part_of(ax0_sk4(X2,X1),ax0_sk3(X2,X1)) ),
end_point_defn_20,
[final] ).
cnf(i_0_122,axiom,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ part_of(ax0_sk3(X2,X1),ax0_sk4(X2,X1)) ),
end_point_defn_19,
[final] ).
cnf(i_0_123,axiom,
( X2 = underlying_curve(X1)
| ~ incident_c(ax2_sk10(X1,X2),X2)
| ~ incident_o(ax2_sk10(X1,X2),X1) ),
underlying_curve_defn_42,
[final] ).
cnf(i_0_124,axiom,
( meet(X1,ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_38,
[final] ).
cnf(i_0_125,axiom,
( X2 = X1
| ~ incident_c(ax0_sk13(X1,X2),X1)
| ~ incident_c(ax0_sk13(X1,X2),X2) ),
c9_48,
[final] ).
cnf(i_0_126,axiom,
( ax0_sk12(X3,X2) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
c8_44,
[final] ).
cnf(i_0_127,axiom,
( X1 = X3
| ordered_by(X2,X1,X3)
| ~ start_point(X1,X2)
| ~ incident_o(X3,X2) ),
start_point_defn_8,
[final] ).
cnf(i_0_128,axiom,
( X1 = X3
| ordered_by(X2,X3,X1)
| ~ finish_point(X1,X2)
| ~ incident_o(X3,X2) ),
finish_point_defn_13,
[final] ).
cnf(i_0_129,axiom,
( incident_o(X2,X1)
| ~ ordered_by(X1,X2,X3) ),
o1_17,
[final] ).
cnf(i_0_130,axiom,
( incident_o(X3,X1)
| ~ ordered_by(X1,X2,X3) ),
o1_18,
[final] ).
cnf(i_0_131,axiom,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
meet_defn_24,
[final] ).
cnf(i_0_132,axiom,
( incident_c(X1,X3)
| ~ meet(X1,X2,X3) ),
meet_defn_25,
[final] ).
cnf(i_0_133,axiom,
( X2 = sum(ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_39,
[final] ).
cnf(i_0_134,axiom,
( incident_o(ax2_sk10(X1,X2),X1)
| incident_c(ax2_sk10(X1,X2),X2)
| X2 = underlying_curve(X1) ),
underlying_curve_defn_39,
[final] ).
cnf(i_0_135,axiom,
( incident_c(ax0_sk13(X1,X2),X2)
| incident_c(ax0_sk13(X1,X2),X1)
| X2 = X1 ),
c9_45,
[final] ).
cnf(i_0_136,axiom,
( part_of(X1,X2)
| ~ incident_c(ax0_sk1(X1,X2),X2) ),
part_of_defn_3,
[final] ).
cnf(i_0_137,axiom,
( incident_o(ax2_sk2(X2,X1),X2)
| finish_point(X1,X2)
| ~ incident_o(X1,X2) ),
finish_point_defn_15,
[final] ).
cnf(i_0_138,axiom,
( incident_o(ax2_sk1(X2,X1),X2)
| start_point(X1,X2)
| ~ incident_o(X1,X2) ),
start_point_defn_10,
[final] ).
cnf(i_0_139,axiom,
( part_of(ax0_sk4(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_16,
[final] ).
cnf(i_0_140,axiom,
( part_of(ax0_sk3(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_15,
[final] ).
cnf(i_0_141,axiom,
( incident_c(X1,ax0_sk4(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_18,
[final] ).
cnf(i_0_142,axiom,
( incident_c(X1,ax0_sk3(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_17,
[final] ).
cnf(i_0_143,axiom,
( incident_c(X4,X2)
| incident_c(X4,X3)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X1) ),
sum_defn_4,
[final] ).
cnf(i_0_144,axiom,
( X1 = X3
| X1 = X4
| X3 = X4
| ~ end_point(X1,X2)
| ~ end_point(X3,X2)
| ~ end_point(X4,X2) ),
c5_40,
[final] ).
cnf(i_0_145,axiom,
( end_point(ax0_sk11(X1,X2),X2)
| ~ end_point(X1,X2) ),
c6_41,
[final] ).
cnf(i_0_146,axiom,
( finish_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk2(X2,X1) ),
finish_point_defn_14,
[final] ).
cnf(i_0_147,axiom,
( start_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk1(X2,X1) ),
start_point_defn_9,
[final] ).
cnf(i_0_148,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X2) ),
sum_defn_5,
[final] ).
cnf(i_0_149,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X3) ),
sum_defn_6,
[final] ).
cnf(i_0_150,axiom,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
part_of_defn_1,
[final] ).
cnf(i_0_151,axiom,
( incident_c(ax0_sk1(X1,X2),X1)
| part_of(X1,X2) ),
part_of_defn_2,
[final] ).
cnf(i_0_152,axiom,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
inner_point_defn_23,
[final] ).
cnf(i_0_153,negated_conjecture,
ordered_by(sk25,sk26,sk26),
theorem_4_4_133,
[final] ).
cnf(i_0_154,axiom,
( incident_o(X1,X2)
| ~ incident_c(X1,ax2_sk3(X2)) ),
o2_21,
[final] ).
cnf(i_0_155,axiom,
( ~ end_point(X1,X2)
| X1 != ax0_sk11(X1,X2) ),
c6_42,
[final] ).
cnf(i_0_156,axiom,
( incident_o(X3,X2)
| X1 != underlying_curve(X2)
| ~ incident_c(X3,X1) ),
underlying_curve_defn_38,
[final] ).
cnf(i_0_157,axiom,
( incident_c(X3,X1)
| X1 != underlying_curve(X2)
| ~ incident_o(X3,X2) ),
underlying_curve_defn_37,
[final] ).
cnf(i_0_158,axiom,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inner_point_defn_22,
[final] ).
cnf(i_0_159,axiom,
( incident_c(X1,ax2_sk3(X2))
| ~ incident_o(X1,X2) ),
o2_20,
[final] ).
cnf(i_0_160,axiom,
( incident_o(X1,X2)
| ~ finish_point(X1,X2) ),
finish_point_defn_12,
[final] ).
cnf(i_0_161,axiom,
( incident_o(X1,X2)
| ~ start_point(X1,X2) ),
start_point_defn_7,
[final] ).
cnf(i_0_162,axiom,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inner_point_defn_21,
[final] ).
cnf(i_0_163,axiom,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
end_point_defn_13,
[final] ).
cnf(i_0_164,axiom,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
closed_defn_31,
[final] ).
cnf(i_0_165,axiom,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
c1_35,
[final] ).
cnf(i_0_166,axiom,
( end_point(ax0_sk7(X1),X1)
| ~ open(X1) ),
open_defn_33,
[final] ).
cnf(i_0_167,axiom,
( open(X2)
| ~ end_point(X1,X2) ),
open_defn_34,
[final] ).
cnf(i_0_168,axiom,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
closed_defn_32,
[final] ).
cnf(i_0_169,axiom,
start_point(ax2_sk6(X1),X1),
o4_29,
[final] ).
cnf(i_0_170,axiom,
inner_point(ax0_sk8(X1),X1),
c3_37,
[final] ).
cnf(i_0_171,axiom,
open(ax2_sk3(X1)),
o2_19,
[final] ).
cnf(i_0_172,axiom,
X1 = X1 ).
cnf(i_0_173,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_174,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_175,axiom,
( X1 != X2
| ax2_sk2(X1,X3) = ax2_sk2(X2,X3) ) ).
cnf(i_0_176,axiom,
( X1 != X2
| ax2_sk2(X3,X1) = ax2_sk2(X3,X2) ) ).
cnf(i_0_177,axiom,
( X1 != X2
| ax2_sk1(X1,X3) = ax2_sk1(X2,X3) ) ).
cnf(i_0_178,axiom,
( X1 != X2
| ax2_sk1(X3,X1) = ax2_sk1(X3,X2) ) ).
cnf(i_0_179,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_213,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_214,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_215,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_172_001,axiom,
X1 = X1 ).
cnf(i_0_173_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_174_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_175_004,axiom,
( X1 != X2
| ax2_sk2(X1,X3) = ax2_sk2(X2,X3) ) ).
cnf(i_0_176_005,axiom,
( X1 != X2
| ax2_sk2(X3,X1) = ax2_sk2(X3,X2) ) ).
cnf(i_0_177_006,axiom,
( X1 != X2
| ax2_sk1(X1,X3) = ax2_sk1(X2,X3) ) ).
cnf(i_0_178_007,axiom,
( X1 != X2
| ax2_sk1(X3,X1) = ax2_sk1(X3,X2) ) ).
cnf(i_0_179_008,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_180_009,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_181_010,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_182_011,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_183_012,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_184_013,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_185_014,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_186_015,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_187_016,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_188_017,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_189_018,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_190_019,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_191_020,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_192_021,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_193_022,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_194_023,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_195_024,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_196_025,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_197_026,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_198_027,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_199_028,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_200_029,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_201_030,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_202_031,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_203_032,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_204_033,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_205_034,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_206_035,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_207_036,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_208_037,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_209_038,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_210_039,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_211_040,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_212_041,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_213_042,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_214_043,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_215_044,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_216,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[104]) ).
cnf(i_0_217,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[115]) ).
cnf(i_0_218,plain,
( ~ incident_c(X1,sum(X2,X3))
| incident_c(X1,X2)
| incident_c(X1,X3) ),
inference(equality_inference,[],[143]) ).
cnf(i_0_219,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[148]) ).
cnf(i_0_220,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(equality_inference,[],[149]) ).
cnf(i_0_221,plain,
( ~ incident_c(X1,underlying_curve(X2))
| incident_o(X1,X2) ),
inference(equality_inference,[],[156]) ).
cnf(i_0_222,plain,
( ~ incident_o(X1,X2)
| incident_c(X1,underlying_curve(X2)) ),
inference(equality_inference,[],[157]) ).
cnf(i_0_223,plain,
~ between_o(X1,X2,X3,X2),
inference(scs_inference,[],[i_0_216,i_0_89]) ).
cnf(i_0_224,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_216]) ).
cnf(i_0_225,plain,
( between_c(ax2_sk4(X1,X2,X3,X4),X4,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(rename_variables,[],[i_0_89]) ).
cnf(i_0_226,plain,
incident_c(ax0_sk8(X1),X1),
inference(scs_inference,[],[i_0_216,i_0_170,i_0_89,i_0_162]) ).
cnf(i_0_227,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_162]) ).
cnf(i_0_228,plain,
incident_c(ax0_sk8(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_216,i_0_170,i_0_89,i_0_162,i_0_219]) ).
cnf(i_0_229,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_219]) ).
cnf(i_0_230,plain,
incident_c(ax0_sk8(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_216,i_0_170,i_0_89,i_0_162,i_0_219,i_0_220]) ).
cnf(i_0_231,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_220]) ).
cnf(i_0_232,plain,
incident_o(ax0_sk8(ax2_sk3(X1)),X1),
inference(scs_inference,[],[i_0_216,i_0_170,i_0_89,i_0_162,i_0_219,i_0_220,i_0_154]) ).
cnf(i_0_233,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_154]) ).
cnf(i_0_234,plain,
incident_o(ax2_sk6(X1),X1),
inference(scs_inference,[],[i_0_216,i_0_169,i_0_170,i_0_89,i_0_162,i_0_219,i_0_220,i_0_154,i_0_161]) ).
cnf(i_0_235,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_161]) ).
cnf(i_0_236,plain,
$false,
inference(scs_inference,[],[i_0_153,i_0_216,i_0_169,i_0_170,i_0_89,i_0_162,i_0_219,i_0_220,i_0_154,i_0_161,i_0_100]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO117-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n015.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 17:43:31 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 0.27/1.60 % Version : CSE_E---1.7
% 0.27/1.60 % Problem : theBenchmark.p
% 0.27/1.60 % SZS status Unsatisfiable for theBenchmark.p
% 0.27/1.60 % SZS output start CNFRefutation
% See solution above
% 0.27/1.66 % Total time : 1.270s
%------------------------------------------------------------------------------