%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO086-1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.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:16 PM UTC 2026
% Result : Unsatisfiable 0.27s 1.61s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 53)
% Comments :
%------------------------------------------------------------------------------
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/sandbox/benchmark/Axioms/GEO004-0.ax',meet_defn_30) ).
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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',sum_defn_11) ).
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/sandbox/benchmark/Axioms/GEO004-0.ax',sum_defn_7) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',meet_defn_29) ).
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/sandbox/benchmark/Axioms/GEO004-0.ax',c7_43) ).
cnf(meet_defn_26,axiom,
( end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',end_point_defn_19) ).
cnf(c4_38,axiom,
( meet(X1,ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',c8_44) ).
cnf(meet_defn_24,axiom,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',meet_defn_24) ).
cnf(meet_defn_25,axiom,
( incident_c(X1,X3)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',c4_39) ).
cnf(c9_45,axiom,
( incident_c(ax0_sk13(X1,X2),X2)
| incident_c(ax0_sk13(X1,X2),X1)
| X2 = X1 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',part_of_defn_3) ).
cnf(end_point_defn_16,axiom,
( part_of(ax0_sk4(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',c6_41) ).
cnf(sum_defn_5,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',inner_point_defn_23) ).
cnf(c6_42,axiom,
( ~ end_point(X1,X2)
| X1 != ax0_sk11(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',c6_42) ).
cnf(inner_point_defn_22,axiom,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',inner_point_defn_22) ).
cnf(inner_point_defn_21,axiom,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO004-0.ax',end_point_defn_13) ).
cnf(closed_defn_31,axiom,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',closed_defn_31) ).
cnf(c1_35,axiom,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',c1_35) ).
cnf(open_defn_33,axiom,
( end_point(ax0_sk7(X1),X1)
| ~ open(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',open_defn_33) ).
cnf(open_defn_34,axiom,
( open(X2)
| ~ end_point(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',open_defn_34) ).
cnf(closed_defn_32,axiom,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',closed_defn_32) ).
cnf(c3_37,axiom,
inner_point(ax0_sk8(X1),X1),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-0.ax',c3_37) ).
cnf(theorem_2_7_2_68,negated_conjecture,
part_of(sk15,sk14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_2_7_2_68) ).
cnf(theorem_2_7_2_69,negated_conjecture,
~ open(sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_2_7_2_69) ).
cnf(theorem_2_7_2_67,negated_conjecture,
open(sk14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_2_7_2_67) ).
cnf(i_0_46,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_47,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_48,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_49,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_50,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_51,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_52,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_53,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_54,axiom,
( end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_26,
[final] ).
cnf(i_0_55,axiom,
( end_point(X4,X3)
| ~ meet(X1,X2,X3)
| ~ incident_c(X4,X2)
| ~ incident_c(X4,X3) ),
meet_defn_27,
[final] ).
cnf(i_0_56,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_57,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_58,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_59,axiom,
( meet(X1,ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_38,
[final] ).
cnf(i_0_60,axiom,
( X2 = X1
| ~ incident_c(ax0_sk13(X1,X2),X1)
| ~ incident_c(ax0_sk13(X1,X2),X2) ),
c9_48,
[final] ).
cnf(i_0_61,axiom,
( ax0_sk12(X3,X2) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
c8_44,
[final] ).
cnf(i_0_62,axiom,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
meet_defn_24,
[final] ).
cnf(i_0_63,axiom,
( incident_c(X1,X3)
| ~ meet(X1,X2,X3) ),
meet_defn_25,
[final] ).
cnf(i_0_64,axiom,
( X2 = sum(ax0_sk9(X1,X2),ax0_sk10(X1,X2))
| ~ inner_point(X1,X2) ),
c4_39,
[final] ).
cnf(i_0_65,axiom,
( incident_c(ax0_sk13(X1,X2),X2)
| incident_c(ax0_sk13(X1,X2),X1)
| X2 = X1 ),
c9_45,
[final] ).
cnf(i_0_66,axiom,
( part_of(X1,X2)
| ~ incident_c(ax0_sk1(X1,X2),X2) ),
part_of_defn_3,
[final] ).
cnf(i_0_67,axiom,
( part_of(ax0_sk4(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_16,
[final] ).
cnf(i_0_68,axiom,
( part_of(ax0_sk3(X2,X1),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_15,
[final] ).
cnf(i_0_69,axiom,
( incident_c(X1,ax0_sk4(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_18,
[final] ).
cnf(i_0_70,axiom,
( incident_c(X1,ax0_sk3(X2,X1))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
end_point_defn_17,
[final] ).
cnf(i_0_71,axiom,
( incident_c(X4,X2)
| incident_c(X4,X3)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X1) ),
sum_defn_4,
[final] ).
cnf(i_0_72,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_73,axiom,
( end_point(ax0_sk11(X1,X2),X2)
| ~ end_point(X1,X2) ),
c6_41,
[final] ).
cnf(i_0_74,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X2) ),
sum_defn_5,
[final] ).
cnf(i_0_75,axiom,
( incident_c(X4,X1)
| X1 != sum(X2,X3)
| ~ incident_c(X4,X3) ),
sum_defn_6,
[final] ).
cnf(i_0_76,axiom,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
part_of_defn_1,
[final] ).
cnf(i_0_77,axiom,
( incident_c(ax0_sk1(X1,X2),X1)
| part_of(X1,X2) ),
part_of_defn_2,
[final] ).
cnf(i_0_78,axiom,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
inner_point_defn_23,
[final] ).
cnf(i_0_79,axiom,
( ~ end_point(X1,X2)
| X1 != ax0_sk11(X1,X2) ),
c6_42,
[final] ).
cnf(i_0_80,axiom,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inner_point_defn_22,
[final] ).
cnf(i_0_81,axiom,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inner_point_defn_21,
[final] ).
cnf(i_0_82,axiom,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
end_point_defn_13,
[final] ).
cnf(i_0_83,axiom,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
closed_defn_31,
[final] ).
cnf(i_0_84,axiom,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
c1_35,
[final] ).
cnf(i_0_85,axiom,
( end_point(ax0_sk7(X1),X1)
| ~ open(X1) ),
open_defn_33,
[final] ).
cnf(i_0_86,axiom,
( open(X2)
| ~ end_point(X1,X2) ),
open_defn_34,
[final] ).
cnf(i_0_87,axiom,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
closed_defn_32,
[final] ).
cnf(i_0_88,axiom,
inner_point(ax0_sk8(X1),X1),
c3_37,
[final] ).
cnf(i_0_89,negated_conjecture,
part_of(sk15,sk14),
theorem_2_7_2_68,
[final] ).
cnf(i_0_90,negated_conjecture,
~ open(sk15),
theorem_2_7_2_69,
[final] ).
cnf(i_0_91,negated_conjecture,
open(sk14),
theorem_2_7_2_67,
[final] ).
cnf(i_0_92,axiom,
X1 = X1 ).
cnf(i_0_93,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_94,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_95,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_96,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_97,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_98,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_101,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_102,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_103,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_113,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_92_001,axiom,
X1 = X1 ).
cnf(i_0_93_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_94_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_95_004,axiom,
( X1 != X2
| ax0_sk11(X1,X3) = ax0_sk11(X2,X3) ) ).
cnf(i_0_96_005,axiom,
( X1 != X2
| ax0_sk11(X3,X1) = ax0_sk11(X3,X2) ) ).
cnf(i_0_97_006,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_98_007,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_99_008,axiom,
( X1 != X2
| ax0_sk12(X1,X3) = ax0_sk12(X2,X3) ) ).
cnf(i_0_100_009,axiom,
( X1 != X2
| ax0_sk12(X3,X1) = ax0_sk12(X3,X2) ) ).
cnf(i_0_101_010,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_102_011,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_103_012,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_104_013,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_105_014,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_106_015,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_107_016,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_108_017,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_109_018,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_110_019,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_111_020,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_112_021,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_113_022,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_114,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[53]) ).
cnf(i_0_115,plain,
( ~ incident_c(X1,sum(X2,X3))
| incident_c(X1,X2)
| incident_c(X1,X3) ),
inference(equality_inference,[],[71]) ).
cnf(i_0_116,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[74]) ).
cnf(i_0_117,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(equality_inference,[],[75]) ).
cnf(i_0_118,plain,
~ end_point(X1,sk15),
inference(scs_inference,[],[i_0_90,i_0_86]) ).
cnf(i_0_119,plain,
( open(X1)
| ~ end_point(X2,X1) ),
inference(rename_variables,[],[i_0_86]) ).
cnf(i_0_120,plain,
incident_c(ax0_sk8(X1),X1),
inference(scs_inference,[],[i_0_90,i_0_88,i_0_86,i_0_81]) ).
cnf(i_0_121,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_81]) ).
cnf(i_0_122,plain,
closed(sk15),
inference(scs_inference,[],[i_0_90,i_0_88,i_0_86,i_0_81,i_0_87]) ).
cnf(i_0_123,plain,
( end_point(ax0_sk6(X1),X1)
| closed(X1) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_124,plain,
incident_c(ax0_sk8(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_90,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116]) ).
cnf(i_0_125,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_126,plain,
incident_c(ax0_sk8(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_90,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117]) ).
cnf(i_0_127,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_117]) ).
cnf(i_0_128,plain,
incident_c(ax0_sk8(sk15),sk14),
inference(scs_inference,[],[i_0_89,i_0_90,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76]) ).
cnf(i_0_129,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_130,plain,
sk15 = sk14,
inference(scs_inference,[],[i_0_89,i_0_90,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76,i_0_84]) ).
cnf(i_0_131,plain,
( open(X1)
| ~ part_of(X1,X2)
| X1 = X2 ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_132,plain,
sk14 != sk15,
inference(scs_inference,[],[i_0_89,i_0_90,i_0_91,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76,i_0_84,i_0_113]) ).
cnf(i_0_133,plain,
closed(sk14),
inference(scs_inference,[],[i_0_89,i_0_90,i_0_91,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76,i_0_84,i_0_113,i_0_110]) ).
cnf(i_0_134,plain,
~ end_point(X1,sk14),
inference(scs_inference,[],[i_0_89,i_0_90,i_0_91,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76,i_0_84,i_0_113,i_0_110,i_0_83]) ).
cnf(i_0_135,plain,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
inference(rename_variables,[],[i_0_83]) ).
cnf(i_0_136,plain,
$false,
inference(scs_inference,[],[i_0_89,i_0_90,i_0_91,i_0_88,i_0_86,i_0_81,i_0_87,i_0_116,i_0_117,i_0_76,i_0_84,i_0_113,i_0_110,i_0_83,i_0_93]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO086-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.32 % Computer : n029.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:40:44 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.33 % start to proof: theBenchmark
% 0.27/1.61 % Version : CSE_E---1.7
% 0.27/1.61 % Problem : theBenchmark.p
% 0.27/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.27/1.61 % SZS output start CNFRefutation
% See solution above
% 0.27/1.68 % Total time : 1.270s
%------------------------------------------------------------------------------