%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO124-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 : n027.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:23 PM UTC 2026
% Result : Unsatisfiable 0.44s 1.60s
% Output : CNFRefutation 0.64s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 117)
% 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(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(corollary_4_10_1_134,negated_conjecture,
start_point(sk27,sk25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_4_10_1_134) ).
cnf(corollary_4_10_1_133,negated_conjecture,
start_point(sk26,sk25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_4_10_1_133) ).
cnf(o2_19,axiom,
open(ax2_sk3(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-2.ax',o2_19) ).
cnf(corollary_4_10_1_135,negated_conjecture,
sk26 != sk27,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_4_10_1_135) ).
cnf(i_0_88,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_89,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_90,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_91,axiom,
( between_c(ax2_sk4(X1,X4,X3,X2),X2,X3,X4)
| ~ between_o(X1,X2,X3,X4) ),
o3_24,
[final] ).
cnf(i_0_92,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_93,axiom,
( part_of(ax1_sk1(X4,X3,X2,X1),X1)
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_2,
[final] ).
cnf(i_0_94,axiom,
( inner_point(X3,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_5,
[final] ).
cnf(i_0_95,axiom,
( end_point(X2,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_3,
[final] ).
cnf(i_0_96,axiom,
( end_point(X4,ax1_sk1(X4,X3,X2,X1))
| ~ between_c(X1,X2,X3,X4) ),
between_c_defn_4,
[final] ).
cnf(i_0_97,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_98,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_99,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_100,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_101,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_102,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_103,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_104,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_105,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_106,axiom,
( ~ between_c(X1,X2,X3,X4)
| X2 != X4 ),
between_c_defn_1,
[final] ).
cnf(i_0_107,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_108,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_109,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_110,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_111,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_112,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_113,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_114,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_115,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_116,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_117,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_118,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_119,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_120,axiom,
( end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_26,
[final] ).
cnf(i_0_121,axiom,
( end_point(X4,X3)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_27,
[final] ).
cnf(i_0_122,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_123,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_124,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_125,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_126,axiom,
( meet(X1,ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_38,
[final] ).
cnf(i_0_127,axiom,
( X2 = X1
| ~ incident_c(ax0_sk13(X1,X2),X1)
| ~ incident_c(ax0_sk13(X1,X2),X2) ),
c9_48,
[final] ).
cnf(i_0_128,axiom,
( ax0_sk12(X3,X2) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
c8_44,
[final] ).
cnf(i_0_129,axiom,
( X1 = X3
| ordered_by(X2,X1,X3)
| ~ start_point(X1,X2)
| ~ incident_o(X3,X2) ),
start_point_defn_8,
[final] ).
cnf(i_0_130,axiom,
( X1 = X3
| ordered_by(X2,X3,X1)
| ~ finish_point(X1,X2)
| ~ incident_o(X3,X2) ),
finish_point_defn_13,
[final] ).
cnf(i_0_131,axiom,
( incident_o(X2,X1)
| ~ ordered_by(X1,X2,X3) ),
o1_17,
[final] ).
cnf(i_0_132,axiom,
( incident_o(X3,X1)
| ~ ordered_by(X1,X2,X3) ),
o1_18,
[final] ).
cnf(i_0_133,axiom,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
meet_defn_24,
[final] ).
cnf(i_0_134,axiom,
( incident_c(X1,X3)
| ~ meet(X1,X2,X3) ),
meet_defn_25,
[final] ).
cnf(i_0_135,axiom,
( X2 = sum(ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_39,
[final] ).
cnf(i_0_136,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_137,axiom,
( incident_c(ax0_sk13(X1,X2),X2)
| incident_c(ax0_sk13(X1,X2),X1)
| X2 = X1 ),
c9_45,
[final] ).
cnf(i_0_138,axiom,
( part_of(X1,X2)
| ~ incident_c(ax0_sk1(X1,X2),X2) ),
part_of_defn_3,
[final] ).
cnf(i_0_139,axiom,
( incident_o(ax2_sk2(X2,X1),X2)
| finish_point(X1,X2)
| ~ incident_o(X1,X2) ),
finish_point_defn_15,
[final] ).
cnf(i_0_140,axiom,
( incident_o(ax2_sk1(X2,X1),X2)
| start_point(X1,X2)
| ~ incident_o(X1,X2) ),
start_point_defn_10,
[final] ).
cnf(i_0_141,axiom,
( part_of(ax0_sk4(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_16,
[final] ).
cnf(i_0_142,axiom,
( part_of(ax0_sk3(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_15,
[final] ).
cnf(i_0_143,axiom,
( incident_c(X1,ax0_sk4(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_18,
[final] ).
cnf(i_0_144,axiom,
( incident_c(X1,ax0_sk3(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_17,
[final] ).
cnf(i_0_145,axiom,
( incident_c(X4,X2)
| incident_c(X4,X3)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X1) ),
sum_defn_4,
[final] ).
cnf(i_0_146,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_147,axiom,
( end_point(ax0_sk11(X1,X2),X2)
| ~ end_point(X1,X2) ),
c6_41,
[final] ).
cnf(i_0_148,axiom,
( finish_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk2(X2,X1) ),
finish_point_defn_14,
[final] ).
cnf(i_0_149,axiom,
( start_point(X1,X2)
| ~ incident_o(X1,X2)
| X1 != ax2_sk1(X2,X1) ),
start_point_defn_9,
[final] ).
cnf(i_0_150,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X2) ),
sum_defn_5,
[final] ).
cnf(i_0_151,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X3) ),
sum_defn_6,
[final] ).
cnf(i_0_152,axiom,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
part_of_defn_1,
[final] ).
cnf(i_0_153,axiom,
( incident_c(ax0_sk1(X1,X2),X1)
| part_of(X1,X2) ),
part_of_defn_2,
[final] ).
cnf(i_0_154,axiom,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
inner_point_defn_23,
[final] ).
cnf(i_0_155,axiom,
( incident_o(X1,X2)
| ~ incident_c(X1,ax2_sk3(X2)) ),
o2_21,
[final] ).
cnf(i_0_156,axiom,
( ~ end_point(X1,X2)
| X1 != ax0_sk11(X1,X2) ),
c6_42,
[final] ).
cnf(i_0_157,axiom,
( incident_o(X3,X2)
| X1 != underlying_curve(X2)
| ~ incident_c(X3,X1) ),
underlying_curve_defn_38,
[final] ).
cnf(i_0_158,axiom,
( incident_c(X3,X1)
| X1 != underlying_curve(X2)
| ~ incident_o(X3,X2) ),
underlying_curve_defn_37,
[final] ).
cnf(i_0_159,axiom,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inner_point_defn_22,
[final] ).
cnf(i_0_160,axiom,
( incident_c(X1,ax2_sk3(X2))
| ~ incident_o(X1,X2) ),
o2_20,
[final] ).
cnf(i_0_161,axiom,
( incident_o(X1,X2)
| ~ finish_point(X1,X2) ),
finish_point_defn_12,
[final] ).
cnf(i_0_162,axiom,
( incident_o(X1,X2)
| ~ start_point(X1,X2) ),
start_point_defn_7,
[final] ).
cnf(i_0_163,axiom,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inner_point_defn_21,
[final] ).
cnf(i_0_164,axiom,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
end_point_defn_13,
[final] ).
cnf(i_0_165,axiom,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
closed_defn_31,
[final] ).
cnf(i_0_166,axiom,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
c1_35,
[final] ).
cnf(i_0_167,axiom,
( end_point(ax0_sk7(X1),X1)
| ~ open(X1) ),
open_defn_33,
[final] ).
cnf(i_0_168,axiom,
( open(X2)
| ~ end_point(X1,X2) ),
open_defn_34,
[final] ).
cnf(i_0_169,axiom,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
closed_defn_32,
[final] ).
cnf(i_0_170,axiom,
start_point(ax2_sk6(X1),X1),
o4_29,
[final] ).
cnf(i_0_171,axiom,
inner_point(ax0_sk8(X1),X1),
c3_37,
[final] ).
cnf(i_0_172,negated_conjecture,
start_point(sk27,sk25),
corollary_4_10_1_134,
[final] ).
cnf(i_0_173,negated_conjecture,
start_point(sk26,sk25),
corollary_4_10_1_133,
[final] ).
cnf(i_0_174,axiom,
open(ax2_sk3(X1)),
o2_19,
[final] ).
cnf(i_0_175,negated_conjecture,
sk26 != sk27,
corollary_4_10_1_135,
[final] ).
cnf(i_0_176,axiom,
X1 = X1 ).
cnf(i_0_177,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_178,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_179,axiom,
( X1 != X2
| ax2_sk2(X1,X3) = ax2_sk2(X2,X3) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ax2_sk2(X3,X1) = ax2_sk2(X3,X2) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ax2_sk1(X1,X3) = ax2_sk1(X2,X3) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ax2_sk1(X3,X1) = ax2_sk1(X3,X2) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_213,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_214,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_215,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_216,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_217,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_218,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_219,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_176_001,axiom,
X1 = X1 ).
cnf(i_0_177_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_178_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_179_004,axiom,
( X1 != X2
| ax2_sk2(X1,X3) = ax2_sk2(X2,X3) ) ).
cnf(i_0_180_005,axiom,
( X1 != X2
| ax2_sk2(X3,X1) = ax2_sk2(X3,X2) ) ).
cnf(i_0_181_006,axiom,
( X1 != X2
| ax2_sk1(X1,X3) = ax2_sk1(X2,X3) ) ).
cnf(i_0_182_007,axiom,
( X1 != X2
| ax2_sk1(X3,X1) = ax2_sk1(X3,X2) ) ).
cnf(i_0_183_008,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_184_009,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_185_010,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_186_011,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_187_012,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_188_013,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_189_014,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_190_015,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_191_016,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_192_017,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_193_018,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_194_019,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_195_020,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_196_021,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_197_022,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_198_023,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_199_024,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_200_025,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_201_026,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_202_027,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_203_028,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_204_029,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_205_030,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_206_031,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_207_032,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_208_033,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_209_034,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_210_035,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_211_036,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_212_037,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_213_038,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_214_039,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_215_040,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_216_041,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_217_042,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_218_043,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_219_044,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_220,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[106]) ).
cnf(i_0_221,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[117]) ).
cnf(i_0_222,plain,
( ~ incident_c(X1,sum(X2,X3))
| incident_c(X1,X2)
| incident_c(X1,X3) ),
inference(equality_inference,[],[145]) ).
cnf(i_0_223,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[150]) ).
cnf(i_0_224,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(equality_inference,[],[151]) ).
cnf(i_0_225,plain,
( ~ incident_c(X1,underlying_curve(X2))
| incident_o(X1,X2) ),
inference(equality_inference,[],[157]) ).
cnf(i_0_226,plain,
( ~ incident_o(X1,X2)
| incident_c(X1,underlying_curve(X2)) ),
inference(equality_inference,[],[158]) ).
cnf(i_0_227,plain,
incident_o(sk27,sk25),
inference(scs_inference,[],[i_0_172,i_0_162]) ).
cnf(i_0_228,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_162]) ).
cnf(i_0_229,plain,
~ between_o(X1,X2,X3,X2),
inference(scs_inference,[],[i_0_172,i_0_220,i_0_162,i_0_91]) ).
cnf(i_0_230,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_220]) ).
cnf(i_0_231,plain,
( between_c(ax2_sk4(X1,X2,X3,X4),X4,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(rename_variables,[],[i_0_91]) ).
cnf(i_0_232,plain,
incident_c(ax0_sk8(X1),X1),
inference(scs_inference,[],[i_0_172,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163]) ).
cnf(i_0_233,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_163]) ).
cnf(i_0_234,plain,
ordered_by(sk25,sk26,sk27),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129]) ).
cnf(i_0_235,plain,
( ~ start_point(X1,X2)
| ~ incident_o(X3,X2)
| X1 = X3
| ordered_by(X2,X1,X3) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_236,plain,
incident_c(ax0_sk8(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223]) ).
cnf(i_0_237,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_238,plain,
incident_c(ax0_sk8(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224]) ).
cnf(i_0_239,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_240,plain,
incident_o(ax0_sk8(ax2_sk3(X1)),X1),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155]) ).
cnf(i_0_241,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_242,plain,
( X1 != X2
| ~ between_o(X3,X1,X4,X2) ),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_191]) ).
cnf(i_0_243,plain,
~ ordered_by(sk25,sk27,sk26),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_191,i_0_102]) ).
cnf(i_0_244,plain,
( ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4)
| between_o(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_102]) ).
cnf(i_0_245,plain,
( X1 != sk26
| ~ between_o(sk25,sk26,sk27,X1) ),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_191,i_0_102,i_0_193]) ).
cnf(i_0_246,plain,
( open(X1)
| ax2_sk3(X2) != X1 ),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_171,i_0_174,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_191,i_0_102,i_0_193,i_0_194]) ).
cnf(i_0_247,plain,
( X1 != X2
| ~ between_c(X3,X2,X4,X1) ),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_230,i_0_171,i_0_174,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_191,i_0_102,i_0_193,i_0_194,i_0_207]) ).
cnf(i_0_248,plain,
( X1 = underlying_curve(X2)
| incident_o(ax2_sk10(X2,X1),X2)
| incident_c(ax2_sk10(X2,X1),X1) ),
inference(rename_variables,[],[i_0_136]) ).
cnf(i_0_249,plain,
( incident_c(ax0_sk8(ax2_sk3(X1)),X2)
| ~ between_c(X3,underlying_curve(X4),X5,X6)
| ~ part_of(ax2_sk3(X1),X2) ),
inference(scs_inference,[],[i_0_172,i_0_173,i_0_175,i_0_220,i_0_230,i_0_171,i_0_174,i_0_162,i_0_91,i_0_163,i_0_129,i_0_223,i_0_224,i_0_155,i_0_102,i_0_207,i_0_152]) ).
cnf(i_0_250,plain,
~ between_o(X1,X2,X3,X2),
inference(equality_inference,[],[242]) ).
cnf(i_0_251,plain,
~ between_o(sk25,sk26,sk27,sk26),
inference(equality_inference,[],[245]) ).
cnf(i_0_252,plain,
open(ax2_sk3(X1)),
inference(equality_inference,[],[246]) ).
cnf(i_0_253,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[247]) ).
cnf(i_0_254,plain,
incident_o(sk26,sk25),
inference(scs_inference,[],[i_0_173,i_0_162]) ).
cnf(i_0_255,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_162]) ).
cnf(i_0_256,plain,
incident_c(ax0_sk8(X1),sum(sum(X1,X2),X3)),
inference(scs_inference,[],[i_0_173,i_0_236,i_0_162,i_0_223]) ).
cnf(i_0_257,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_258,plain,
incident_c(ax0_sk8(X1),sum(X2,sum(X1,X3))),
inference(scs_inference,[],[i_0_173,i_0_236,i_0_162,i_0_223,i_0_224]) ).
cnf(i_0_259,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_260,plain,
( incident_o(ax0_sk8(ax2_sk4(X1,X2,X3,X4)),X1)
| ~ between_o(X1,X4,X3,X2) ),
inference(scs_inference,[],[i_0_173,i_0_236,i_0_232,i_0_162,i_0_223,i_0_224,i_0_90]) ).
cnf(i_0_261,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_262,plain,
( ~ incident_c(X1,ax2_sk4(X2,X3,X4,X5))
| incident_o(X1,X2)
| ~ between_o(X2,X5,X4,X3) ),
inference(rename_variables,[],[i_0_90]) ).
cnf(i_0_264,plain,
incident_c(ax0_sk8(X1),sum(sum(X2,X1),X3)),
inference(scs_inference,[],[i_0_238,i_0_223]) ).
cnf(i_0_265,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_266,plain,
incident_c(ax0_sk8(X1),sum(X2,sum(X3,X1))),
inference(scs_inference,[],[i_0_238,i_0_223,i_0_224]) ).
cnf(i_0_267,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_268,plain,
incident_o(ax2_sk6(X1),X1),
inference(scs_inference,[],[i_0_238,i_0_170,i_0_223,i_0_224,i_0_162]) ).
cnf(i_0_269,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_162]) ).
cnf(i_0_270,plain,
( X1 != sk25
| ~ ordered_by(X1,sk27,sk26) ),
inference(scs_inference,[],[i_0_238,i_0_243,i_0_170,i_0_223,i_0_224,i_0_162,i_0_214]) ).
cnf(i_0_271,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X3,X2,X4) ),
inference(rename_variables,[],[i_0_97]) ).
cnf(i_0_272,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_273,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_275,plain,
~ ordered_by(sk25,sk27,sk26),
inference(equality_inference,[],[270]) ).
cnf(i_0_276,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(sum(X1,X3),X4),X2) ),
inference(scs_inference,[],[i_0_256,i_0_152]) ).
cnf(i_0_277,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_278,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(sum(sum(X1,X3),X4),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_256,i_0_152,i_0_155]) ).
cnf(i_0_279,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_280,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(sum(sum(X1,X4),X5),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_256,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_281,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_282,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(sum(sum(X1,X4),X5),ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_256,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_283,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_284,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_285,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_286,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_288,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(X1,X3),X2) ),
inference(scs_inference,[],[i_0_236,i_0_152]) ).
cnf(i_0_289,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_290,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(sum(X1,X3),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_236,i_0_152,i_0_155]) ).
cnf(i_0_291,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_292,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(sum(X1,X4),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_236,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_293,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_294,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(sum(X1,X4),ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_236,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_295,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_296,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_297,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_299,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(X3,X1),X2) ),
inference(scs_inference,[],[i_0_238,i_0_152]) ).
cnf(i_0_300,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_301,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(sum(X3,X1),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_238,i_0_152,i_0_155]) ).
cnf(i_0_302,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_303,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(sum(X4,X1),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_238,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_304,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_305,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(sum(X4,X1),ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_238,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_306,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_307,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_309,plain,
( X1 != sk27
| ~ ordered_by(sk25,X1,sk26) ),
inference(scs_inference,[],[i_0_243,i_0_215]) ).
cnf(i_0_310,plain,
( X1 != sk26
| ~ ordered_by(sk25,sk27,X1) ),
inference(scs_inference,[],[i_0_243,i_0_215,i_0_216]) ).
cnf(i_0_311,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(X3,sum(X1,X4)),X2) ),
inference(scs_inference,[],[i_0_258,i_0_243,i_0_215,i_0_216,i_0_152]) ).
cnf(i_0_312,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_313,plain,
( X1 != X2
| ~ between_o(X3,X2,X4,X1) ),
inference(scs_inference,[],[i_0_258,i_0_243,i_0_229,i_0_215,i_0_216,i_0_152,i_0_193]) ).
cnf(i_0_314,plain,
( X1 = sum(X2,X3)
| incident_c(ax0_sk2(X3,X2,X1),X1)
| incident_c(ax0_sk2(X3,X2,X1),X2)
| incident_c(ax0_sk2(X3,X2,X1),X3) ),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_315,plain,
( ~ between_o(X1,sum(X2,X3),X4,X5)
| incident_c(ax0_sk2(X3,X2,X5),X5)
| incident_c(ax0_sk2(X3,X2,X5),X3)
| incident_c(ax0_sk2(X3,X2,X5),X2) ),
inference(scs_inference,[],[i_0_258,i_0_243,i_0_229,i_0_193,i_0_107]) ).
cnf(i_0_316,plain,
~ ordered_by(sk25,sk27,sk26),
inference(equality_inference,[],[309]) ).
cnf(i_0_317,plain,
~ ordered_by(sk25,sk27,sk26),
inference(equality_inference,[],[310]) ).
cnf(i_0_318,plain,
~ between_o(X1,X2,X3,X2),
inference(equality_inference,[],[313]) ).
cnf(i_0_319,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(sum(X3,X1),X4),X2) ),
inference(scs_inference,[],[i_0_264,i_0_152]) ).
cnf(i_0_320,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_321,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(sum(sum(X3,X1),X4),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_264,i_0_152,i_0_155]) ).
cnf(i_0_322,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_323,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(sum(sum(X4,X1),X5),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_264,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_324,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_325,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(sum(sum(X4,X1),X5),ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_264,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_326,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_327,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_328,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_329,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_331,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(sum(X3,sum(X4,X1)),X2) ),
inference(scs_inference,[],[i_0_266,i_0_152]) ).
cnf(i_0_332,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_333,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(sum(X3,sum(X4,X1)),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_266,i_0_152,i_0_155]) ).
cnf(i_0_334,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_335,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(sum(X4,sum(X5,X1)),ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_266,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_336,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_337,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(sum(X4,sum(X5,X1)),ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_266,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_338,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_339,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_340,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_341,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_343,plain,
( incident_c(ax0_sk8(X1),X2)
| ~ part_of(X1,X2) ),
inference(scs_inference,[],[i_0_232,i_0_152]) ).
cnf(i_0_344,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_345,plain,
( incident_o(ax0_sk8(X1),X2)
| ~ part_of(X1,ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_232,i_0_152,i_0_155]) ).
cnf(i_0_346,plain,
( ~ incident_c(X1,ax2_sk3(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_155]) ).
cnf(i_0_347,plain,
( incident_c(ax0_sk8(X1),sum(ax2_sk3(X2),X3))
| ~ part_of(X1,ax2_sk3(X2)) ),
inference(scs_inference,[],[i_0_232,i_0_152,i_0_155,i_0_223]) ).
cnf(i_0_348,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_223]) ).
cnf(i_0_349,plain,
( incident_c(ax0_sk8(X1),sum(X2,ax2_sk3(X3)))
| ~ part_of(X1,ax2_sk3(X3)) ),
inference(scs_inference,[],[i_0_232,i_0_152,i_0_155,i_0_223,i_0_224]) ).
cnf(i_0_350,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_351,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_352,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_354,plain,
( end_point(ax0_sk8(X1),sum(X1,X2))
| ~ meet(X3,sum(X1,X2),sum(X1,X2)) ),
inference(scs_inference,[],[i_0_236,i_0_120]) ).
cnf(i_0_355,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X2)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_356,plain,
( ~ inner_point(ax0_sk8(X1),sum(X1,X2))
| ~ meet(X3,sum(X1,X2),sum(X1,X2)) ),
inference(scs_inference,[],[i_0_236,i_0_120,i_0_159]) ).
cnf(i_0_357,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_358,plain,
( ax0_sk8(sum(X1,X2)) != ax0_sk8(X1)
| ~ meet(X3,sum(X1,X2),sum(X1,X2)) ),
inference(scs_inference,[],[i_0_236,i_0_171,i_0_120,i_0_159,i_0_210]) ).
cnf(i_0_359,plain,
inner_point(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_360,plain,
( X1 != sum(X1,X2)
| ~ meet(X3,sum(X1,X2),sum(X1,X2)) ),
inference(scs_inference,[],[i_0_236,i_0_171,i_0_359,i_0_120,i_0_159,i_0_210,i_0_211]) ).
cnf(i_0_361,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_362,plain,
( ~ incident_c(X1,ax2_sk4(X2,X3,X4,X5))
| incident_o(X1,X2)
| ~ between_o(X2,X5,X4,X3) ),
inference(rename_variables,[],[i_0_90]) ).
cnf(i_0_364,plain,
( end_point(ax0_sk8(X1),sum(X2,X1))
| ~ meet(X3,sum(X2,X1),sum(X2,X1)) ),
inference(scs_inference,[],[i_0_238,i_0_121]) ).
cnf(i_0_365,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X3)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_121]) ).
cnf(i_0_366,plain,
( ~ inner_point(ax0_sk8(X1),sum(X2,X1))
| ~ meet(X3,sum(X2,X1),sum(X2,X1)) ),
inference(scs_inference,[],[i_0_238,i_0_121,i_0_159]) ).
cnf(i_0_367,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_368,plain,
( ax0_sk8(sum(X1,X2)) != ax0_sk8(X2)
| ~ meet(X3,sum(X1,X2),sum(X1,X2)) ),
inference(scs_inference,[],[i_0_238,i_0_171,i_0_121,i_0_159,i_0_210]) ).
cnf(i_0_369,plain,
inner_point(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_370,plain,
( X1 != sum(X2,X1)
| ~ meet(X3,sum(X2,X1),sum(X2,X1)) ),
inference(scs_inference,[],[i_0_238,i_0_171,i_0_369,i_0_121,i_0_159,i_0_210,i_0_211]) ).
cnf(i_0_371,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_372,plain,
( ~ incident_c(X1,ax2_sk4(X2,X3,X4,X5))
| incident_o(X1,X2)
| ~ between_o(X2,X5,X4,X3) ),
inference(rename_variables,[],[i_0_90]) ).
cnf(i_0_374,plain,
( end_point(ax0_sk8(X1),sum(sum(X1,X2),X3))
| ~ meet(X4,sum(sum(X1,X2),X3),sum(sum(X1,X2),X3)) ),
inference(scs_inference,[],[i_0_256,i_0_120]) ).
cnf(i_0_375,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X2)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_376,plain,
( ~ inner_point(ax0_sk8(X1),sum(sum(X1,X2),X3))
| ~ meet(X4,sum(sum(X1,X2),X3),sum(sum(X1,X2),X3)) ),
inference(scs_inference,[],[i_0_256,i_0_120,i_0_159]) ).
cnf(i_0_377,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_378,plain,
( X1 != sum(sum(X1,X2),X3)
| ~ meet(X4,sum(sum(X1,X2),X3),sum(sum(X1,X2),X3)) ),
inference(scs_inference,[],[i_0_256,i_0_171,i_0_120,i_0_159,i_0_211]) ).
cnf(i_0_379,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(rename_variables,[],[i_0_100]) ).
cnf(i_0_380,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_382,plain,
( end_point(ax0_sk8(X1),sum(X2,sum(X1,X3)))
| ~ meet(X4,sum(X2,sum(X1,X3)),sum(X2,sum(X1,X3))) ),
inference(scs_inference,[],[i_0_258,i_0_121]) ).
cnf(i_0_383,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X3)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_121]) ).
cnf(i_0_384,plain,
( ~ inner_point(ax0_sk8(X1),sum(X2,sum(X1,X3)))
| ~ meet(X4,sum(X2,sum(X1,X3)),sum(X2,sum(X1,X3))) ),
inference(scs_inference,[],[i_0_258,i_0_121,i_0_159]) ).
cnf(i_0_385,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_387,plain,
( sk27 = ax2_sk6(sk25)
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129]) ).
cnf(i_0_388,plain,
incident_o(ax2_sk6(X1),X1),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_389,plain,
( ~ start_point(X1,X2)
| ~ incident_o(X3,X2)
| X1 = X3
| ordered_by(X2,X1,X3) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_390,plain,
( ~ between_c(X1,sk27,X2,ax2_sk6(sk25))
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129,i_0_106]) ).
cnf(i_0_391,plain,
( X1 != X2
| ~ between_c(X3,X1,X4,X2) ),
inference(rename_variables,[],[i_0_106]) ).
cnf(i_0_392,plain,
( ax2_sk6(sk25) = sk27
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129,i_0_106,i_0_177]) ).
cnf(i_0_393,plain,
( ~ between_o(X1,sk27,X2,ax2_sk6(sk25))
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129,i_0_106,i_0_177,i_0_242]) ).
cnf(i_0_394,plain,
( ~ between_c(X1,ax2_sk6(sk25),X2,sk27)
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129,i_0_106,i_0_177,i_0_242,i_0_247]) ).
cnf(i_0_395,plain,
( ~ between_o(X1,ax2_sk6(sk25),X2,sk27)
| ordered_by(sk25,sk27,ax2_sk6(sk25)) ),
inference(scs_inference,[],[i_0_172,i_0_268,i_0_129,i_0_106,i_0_177,i_0_242,i_0_247,i_0_313]) ).
cnf(i_0_396,plain,
( ordered_by(sk25,sk27,ax2_sk6(sk25))
| sk26 != ax2_sk6(sk25) ),
inference(scs_inference,[],[i_0_172,i_0_175,i_0_268,i_0_129,i_0_106,i_0_177,i_0_242,i_0_247,i_0_313,i_0_178]) ).
cnf(i_0_397,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_398,plain,
( ~ incident_c(X1,ax2_sk4(X2,X3,X4,X5))
| incident_o(X1,X2)
| ~ between_o(X2,X5,X4,X3) ),
inference(rename_variables,[],[i_0_90]) ).
cnf(i_0_400,plain,
( end_point(ax0_sk8(X1),sum(sum(X2,X1),X3))
| ~ meet(X4,sum(sum(X2,X1),X3),sum(sum(X2,X1),X3)) ),
inference(scs_inference,[],[i_0_264,i_0_120]) ).
cnf(i_0_401,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X2)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_402,plain,
( ~ inner_point(ax0_sk8(X1),sum(sum(X2,X1),X3))
| ~ meet(X4,sum(sum(X2,X1),X3),sum(sum(X2,X1),X3)) ),
inference(scs_inference,[],[i_0_264,i_0_120,i_0_159]) ).
cnf(i_0_403,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_404,plain,
( X1 != sum(sum(X2,X1),X3)
| ~ meet(X4,sum(sum(X2,X1),X3),sum(sum(X2,X1),X3)) ),
inference(scs_inference,[],[i_0_220,i_0_264,i_0_171,i_0_120,i_0_159,i_0_204,i_0_205,i_0_206,i_0_207,i_0_211]) ).
cnf(i_0_406,plain,
( end_point(ax0_sk8(X1),sum(X2,sum(X3,X1)))
| ~ meet(X4,sum(X2,sum(X3,X1)),sum(X2,sum(X3,X1))) ),
inference(scs_inference,[],[i_0_266,i_0_121]) ).
cnf(i_0_407,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| end_point(X1,X3)
| ~ meet(X4,X2,X3) ),
inference(rename_variables,[],[i_0_121]) ).
cnf(i_0_408,plain,
( ~ inner_point(ax0_sk8(X1),sum(X2,sum(X3,X1)))
| ~ meet(X4,sum(X2,sum(X3,X1)),sum(X2,sum(X3,X1))) ),
inference(scs_inference,[],[i_0_266,i_0_121,i_0_159]) ).
cnf(i_0_409,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_410,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_412,plain,
( ax2_sk6(sk25) = sk27
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129]) ).
cnf(i_0_413,plain,
start_point(ax2_sk6(X1),X1),
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_414,plain,
( ~ start_point(X1,X2)
| ~ incident_o(X3,X2)
| X1 = X3
| ordered_by(X2,X1,X3) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_415,plain,
( ~ between_c(X1,ax2_sk6(sk25),X2,sk27)
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129,i_0_106]) ).
cnf(i_0_416,plain,
( X1 != X2
| ~ between_c(X3,X1,X4,X2) ),
inference(rename_variables,[],[i_0_106]) ).
cnf(i_0_417,plain,
( ~ between_o(X1,ax2_sk6(sk25),X2,sk27)
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129,i_0_106,i_0_91]) ).
cnf(i_0_418,plain,
( between_c(ax2_sk4(X1,X2,X3,X4),X4,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(rename_variables,[],[i_0_91]) ).
cnf(i_0_419,plain,
( sk27 = ax2_sk6(sk25)
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129,i_0_106,i_0_91,i_0_177]) ).
cnf(i_0_420,plain,
( ~ between_o(X1,sk27,X2,ax2_sk6(sk25))
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129,i_0_106,i_0_91,i_0_177,i_0_242]) ).
cnf(i_0_421,plain,
( ~ between_c(X1,sk27,X2,ax2_sk6(sk25))
| ordered_by(sk25,ax2_sk6(sk25),sk27) ),
inference(scs_inference,[],[i_0_227,i_0_170,i_0_129,i_0_106,i_0_91,i_0_177,i_0_242,i_0_247]) ).
cnf(i_0_422,plain,
( ordered_by(sk25,ax2_sk6(sk25),sk27)
| sk26 != ax2_sk6(sk25) ),
inference(scs_inference,[],[i_0_175,i_0_227,i_0_170,i_0_129,i_0_106,i_0_91,i_0_177,i_0_242,i_0_247,i_0_178]) ).
cnf(i_0_423,plain,
incident_c(ax0_sk8(X1),X1),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_424,plain,
( ~ incident_c(X1,ax2_sk4(X2,X3,X4,X5))
| incident_o(X1,X2)
| ~ between_o(X2,X5,X4,X3) ),
inference(rename_variables,[],[i_0_90]) ).
cnf(i_0_425,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_426,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_427,plain,
~ between_o(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_429,plain,
sk27 = sk26,
inference(scs_inference,[],[i_0_172,i_0_254,i_0_243,i_0_129]) ).
cnf(i_0_430,plain,
( ~ start_point(X1,X2)
| ~ incident_o(X3,X2)
| X1 = X3
| ordered_by(X2,X1,X3) ),
inference(rename_variables,[],[i_0_129]) ).
cnf(i_0_431,plain,
~ between_c(X1,sk27,X2,sk26),
inference(scs_inference,[],[i_0_172,i_0_254,i_0_243,i_0_129,i_0_106]) ).
cnf(i_0_432,plain,
( X1 != X2
| ~ between_c(X3,X1,X4,X2) ),
inference(rename_variables,[],[i_0_106]) ).
cnf(i_0_433,plain,
~ between_o(X1,sk27,X2,sk26),
inference(scs_inference,[],[i_0_172,i_0_254,i_0_243,i_0_129,i_0_106,i_0_91]) ).
cnf(i_0_434,plain,
( between_c(ax2_sk4(X1,X2,X3,X4),X4,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(rename_variables,[],[i_0_91]) ).
cnf(i_0_435,plain,
~ between_o(X1,sk26,X2,sk27),
inference(scs_inference,[],[i_0_172,i_0_254,i_0_243,i_0_129,i_0_106,i_0_91,i_0_313]) ).
cnf(i_0_436,plain,
$false,
inference(scs_inference,[],[i_0_172,i_0_175,i_0_254,i_0_243,i_0_129,i_0_106,i_0_91,i_0_313,i_0_177]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO124-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.13/0.32 % Computer : n027.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Mon May 4 17:42:34 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.33 % start to proof: theBenchmark
% 0.44/1.60 % Version : CSE_E---1.7
% 0.44/1.60 % Problem : theBenchmark.p
% 0.44/1.60 % SZS status Unsatisfiable for theBenchmark.p
% 0.44/1.60 % SZS output start CNFRefutation
% See solution above
% 0.64/1.86 % Total time : 1.271s
%------------------------------------------------------------------------------