%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO111-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:19:54 PM UTC 2026
% Result : Unsatisfiable 8.32s 1.93s
% Output : CNFRefutation 8.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 51
% Syntax : Number of formulae : 680 ( 54 unt; 0 def)
% Number of atoms : 2050 ( 234 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 2044 ( 674 ~;1370 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 1420 ( 0 sgn1420 !; 0 ?;1229 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( incident_c(X2,X1)
| ~ incident_c(X2,X0)
| ~ part_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_1) ).
fof(f2,axiom,
! [X0,X1] :
( part_of(X0,X1)
| incident_c(ax0_sk1(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_2) ).
fof(f3,axiom,
! [X0,X1] :
( part_of(X0,X1)
| ~ incident_c(ax0_sk1(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',part_of_defn_3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] :
( incident_c(X3,X2)
| incident_c(X3,X1)
| ~ incident_c(X3,X0)
| X0 != sum(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_4) ).
fof(f5,plain,
! [X2,X3,X0,X1] :
( incident_c(X3,X2)
| incident_c(X3,X1)
| ~ incident_c(X3,X0)
| sum(X1,X2) != X0 ),
inference(reorient_equations,[],[f4]) ).
fof(f6,axiom,
! [X2,X3,X0,X1] :
( incident_c(X3,X0)
| ~ incident_c(X3,X1)
| X0 != sum(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_5) ).
fof(f7,plain,
! [X2,X3,X0,X1] :
( incident_c(X3,X0)
| ~ incident_c(X3,X1)
| sum(X1,X2) != X0 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X2,X3,X0,X1] :
( incident_c(X3,X0)
| ~ incident_c(X3,X2)
| X0 != sum(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_6) ).
fof(f9,plain,
! [X2,X3,X0,X1] :
( incident_c(X3,X0)
| ~ incident_c(X3,X2)
| sum(X1,X2) != X0 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X2,X0,X1] :
( X2 = sum(X1,X0)
| incident_c(ax0_sk2(X0,X1,X2),X0)
| incident_c(ax0_sk2(X0,X1,X2),X1)
| incident_c(ax0_sk2(X0,X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_7) ).
fof(f11,plain,
! [X2,X0,X1] :
( sum(X1,X0) = X2
| incident_c(ax0_sk2(X0,X1,X2),X0)
| incident_c(ax0_sk2(X0,X1,X2),X1)
| incident_c(ax0_sk2(X0,X1,X2),X2) ),
inference(reorient_equations,[],[f10]) ).
fof(f18,axiom,
! [X2,X0,X1] :
( X2 = sum(X1,X0)
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_11) ).
fof(f19,plain,
! [X2,X0,X1] :
( sum(X1,X0) = X2
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X1) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X2,X0,X1] :
( X2 = sum(X1,X0)
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',sum_defn_12) ).
fof(f21,plain,
! [X2,X0,X1] :
( sum(X1,X0) = X2
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X0) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0,X1] :
( incident_c(X0,X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_13) ).
fof(f23,axiom,
! [X2,X3,X0,X1] :
( part_of(X3,X2)
| part_of(X2,X3)
| ~ incident_c(X0,X3)
| ~ incident_c(X0,X2)
| ~ part_of(X3,X1)
| ~ part_of(X2,X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_14) ).
fof(f24,axiom,
! [X0,X1] :
( end_point(X0,X1)
| part_of(ax0_sk3(X1,X0),X1)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_15) ).
fof(f25,axiom,
! [X0,X1] :
( end_point(X0,X1)
| part_of(ax0_sk4(X1,X0),X1)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_16) ).
fof(f26,axiom,
! [X0,X1] :
( end_point(X0,X1)
| incident_c(X0,ax0_sk3(X1,X0))
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_17) ).
fof(f27,axiom,
! [X0,X1] :
( end_point(X0,X1)
| incident_c(X0,ax0_sk4(X1,X0))
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_18) ).
fof(f28,axiom,
! [X0,X1] :
( end_point(X0,X1)
| ~ part_of(ax0_sk3(X1,X0),ax0_sk4(X1,X0))
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_19) ).
fof(f29,axiom,
! [X0,X1] :
( end_point(X0,X1)
| ~ part_of(ax0_sk4(X1,X0),ax0_sk3(X1,X0))
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',end_point_defn_20) ).
fof(f30,axiom,
! [X0,X1] :
( incident_c(X0,X1)
| ~ inner_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_21) ).
fof(f31,axiom,
! [X0,X1] :
( ~ end_point(X0,X1)
| ~ inner_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_22) ).
fof(f32,axiom,
! [X0,X1] :
( inner_point(X0,X1)
| end_point(X0,X1)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',inner_point_defn_23) ).
fof(f33,axiom,
! [X2,X0,X1] :
( incident_c(X0,X1)
| ~ meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_24) ).
fof(f34,axiom,
! [X2,X0,X1] :
( incident_c(X0,X2)
| ~ meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_25) ).
fof(f35,axiom,
! [X2,X3,X0,X1] :
( end_point(X3,X1)
| ~ incident_c(X3,X2)
| ~ incident_c(X3,X1)
| ~ meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_26) ).
fof(f36,axiom,
! [X2,X3,X0,X1] :
( end_point(X3,X2)
| ~ incident_c(X3,X2)
| ~ incident_c(X3,X1)
| ~ meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_27) ).
fof(f37,axiom,
! [X2,X0,X1] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_28) ).
fof(f38,axiom,
! [X2,X0,X1] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X2)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_29) ).
fof(f39,axiom,
! [X2,X0,X1] :
( meet(X0,X1,X2)
| ~ end_point(ax0_sk5(X2,X1,X0),X2)
| ~ end_point(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',meet_defn_30) ).
fof(f40,axiom,
! [X0,X1] :
( ~ end_point(X1,X0)
| ~ closed(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',closed_defn_31) ).
fof(f41,axiom,
! [X0] :
( closed(X0)
| end_point(ax0_sk6(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',closed_defn_32) ).
fof(f42,axiom,
! [X0] :
( end_point(ax0_sk7(X0),X0)
| ~ open(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',open_defn_33) ).
fof(f43,axiom,
! [X0,X1] :
( open(X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',open_defn_34) ).
fof(f44,axiom,
! [X0,X1] :
( open(X0)
| X0 = X1
| ~ part_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c1_35) ).
fof(f45,axiom,
! [X2,X3,X0,X1,X4] :
( part_of(X3,X0)
| part_of(X0,X3)
| part_of(X2,X0)
| part_of(X0,X2)
| part_of(X3,X2)
| part_of(X2,X3)
| ~ end_point(X4,X3)
| ~ end_point(X4,X2)
| ~ end_point(X4,X0)
| ~ part_of(X3,X1)
| ~ part_of(X2,X1)
| ~ part_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c2_36) ).
fof(f46,axiom,
! [X0] : inner_point(ax0_sk8(X0),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c3_37) ).
fof(f47,axiom,
! [X0,X1] :
( meet(X0,ax0_sk9(X0,X1),ax0_sk10(X0,X1))
| ~ inner_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c4_38) ).
fof(f48,axiom,
! [X0,X1] :
( X1 = sum(ax0_sk9(X0,X1),ax0_sk10(X0,X1))
| ~ inner_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c4_39) ).
fof(f49,plain,
! [X0,X1] :
( sum(ax0_sk9(X0,X1),ax0_sk10(X0,X1)) = X1
| ~ inner_point(X0,X1) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,axiom,
! [X2,X3,X0,X1] :
( X2 = X3
| X0 = X3
| X0 = X2
| ~ end_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c5_40) ).
fof(f51,axiom,
! [X0,X1] :
( end_point(ax0_sk11(X0,X1),X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c6_41) ).
fof(f52,axiom,
! [X0,X1] :
( X0 != ax0_sk11(X0,X1)
| ~ end_point(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c6_42) ).
fof(f53,plain,
! [X0,X1] :
( ax0_sk11(X0,X1) != X0
| ~ end_point(X0,X1) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,axiom,
! [X2,X3,X0,X1,X4] :
( meet(X4,X2,X3)
| ~ end_point(X4,X2)
| X0 != sum(X2,X3)
| ~ meet(X1,X2,X3)
| ~ closed(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c7_43) ).
fof(f55,plain,
! [X2,X3,X0,X1,X4] :
( meet(X4,X2,X3)
| ~ end_point(X4,X2)
| sum(X2,X3) != X0
| ~ meet(X1,X2,X3)
| ~ closed(X0) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,axiom,
! [X2,X0,X1] :
( ax0_sk12(X2,X1) = sum(X1,X2)
| ~ meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c8_44) ).
fof(f57,plain,
! [X2,X0,X1] :
( sum(X1,X2) = ax0_sk12(X2,X1)
| ~ meet(X0,X1,X2) ),
inference(reorient_equations,[],[f56]) ).
fof(f58,axiom,
! [X0,X1] :
( X1 = X0
| incident_c(ax0_sk13(X0,X1),X0)
| incident_c(ax0_sk13(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c9_45) ).
fof(f59,plain,
! [X0,X1] :
( X0 = X1
| incident_c(ax0_sk13(X0,X1),X0)
| incident_c(ax0_sk13(X0,X1),X1) ),
inference(reorient_equations,[],[f58]) ).
fof(f64,axiom,
! [X0,X1] :
( X1 = X0
| ~ incident_c(ax0_sk13(X0,X1),X1)
| ~ incident_c(ax0_sk13(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-0.ax',c9_48) ).
fof(f65,plain,
! [X0,X1] :
( X0 = X1
| ~ incident_c(ax0_sk13(X0,X1),X1)
| ~ incident_c(ax0_sk13(X0,X1),X0) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,axiom,
! [X2,X3,X0,X1] :
( X1 != X3
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_1) ).
fof(f67,axiom,
! [X2,X3,X0,X1] :
( part_of(ax1_sk1(X3,X2,X1,X0),X0)
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_2) ).
fof(f68,axiom,
! [X2,X3,X0,X1] :
( end_point(X1,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_3) ).
fof(f69,axiom,
! [X2,X3,X0,X1] :
( end_point(X3,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_4) ).
fof(f70,axiom,
! [X2,X3,X0,X1] :
( inner_point(X2,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_5) ).
fof(f71,axiom,
! [X2,X3,X0,X1,X4] :
( between_c(X3,X0,X4,X1)
| ~ inner_point(X4,X2)
| ~ end_point(X1,X2)
| ~ end_point(X0,X2)
| ~ part_of(X2,X3)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004-1.ax',between_c_defn_6) ).
fof(f72,negated_conjecture,
between_c(sk15,sk16,sk17,sk18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_3_8_1_77) ).
fof(f73,negated_conjecture,
( sk16 = sk18
| sk17 = sk18
| sk16 = sk17
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk16,sk15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_3_8_1_78) ).
fof(f74,plain,
! [X2,X3,X1] :
( incident_c(X3,X2)
| incident_c(X3,X1)
| ~ incident_c(X3,sum(X1,X2)) ),
inference(equality_resolution,[],[f5]) ).
fof(f75,plain,
! [X2,X3,X1] :
( incident_c(X3,sum(X1,X2))
| ~ incident_c(X3,X1) ),
inference(equality_resolution,[],[f7]) ).
fof(f76,plain,
! [X2,X3,X1] :
( incident_c(X3,sum(X1,X2))
| ~ incident_c(X3,X2) ),
inference(equality_resolution,[],[f9]) ).
fof(f77,plain,
! [X2,X3,X1,X4] :
( meet(X4,X2,X3)
| ~ end_point(X4,X2)
| ~ meet(X1,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_resolution,[],[f55]) ).
fof(f78,plain,
! [X2,X3,X0] : ~ between_c(X0,X3,X2,X3),
inference(equality_resolution,[],[f66]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| incident_c(ax0_sk1(X0,X1),X0) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| ~ incident_c(ax0_sk1(X0,X1),X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X2)
| incident_c(X0,X1)
| ~ incident_c(X0,sum(X1,X2)) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,sum(X1,X2))
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,sum(X2,X1))
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(X1,X0,X2),X2)
| incident_c(ax0_sk2(X1,X0,X2),X1)
| incident_c(ax0_sk2(X1,X0,X2),X0)
| ( sum(X0,X1) = X2 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sum(X1,X0) = X2 )
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sum(X1,X0) = X2 )
| ~ incident_c(ax0_sk2(X0,X1,X2),X2)
| ~ incident_c(ax0_sk2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X2,X1)
| part_of(X1,X2)
| ~ end_point(X0,X3)
| ~ part_of(X2,X3)
| ~ part_of(X1,X3)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| part_of(ax0_sk3(X1,X0),X1)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| part_of(ax0_sk4(X1,X0),X1)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| incident_c(X0,ax0_sk3(X1,X0))
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| incident_c(X0,ax0_sk4(X1,X0))
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] :
( end_point(X1,X0)
| ~ incident_c(X1,X0)
| ~ part_of(ax0_sk3(X0,X1),ax0_sk4(X0,X1)) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i] :
( end_point(X1,X0)
| ~ incident_c(X1,X0)
| ~ part_of(ax0_sk4(X0,X1),ax0_sk3(X0,X1)) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] :
( ~ inner_point(X0,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] :
( inner_point(X0,X1)
| end_point(X0,X1)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X1)
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X2)
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X3,X1)
| ~ incident_c(X3,X2)
| ~ incident_c(X3,X1)
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X3,X2)
| ~ incident_c(X3,X2)
| ~ incident_c(X3,X1)
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X2)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X2,X1,X0)
| ~ incident_c(X2,X1)
| ~ incident_c(X2,X0)
| ~ end_point(ax0_sk5(X0,X1,X2),X1)
| ~ end_point(ax0_sk5(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] :
( ~ closed(X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_133,plain,
! [X0: $i] :
( closed(X0)
| end_point(ax0_sk6(X0),X0) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_134,plain,
! [X0: $i] :
( end_point(ax0_sk7(X0),X0)
| ~ open(X0) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i] :
( open(X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i] :
( open(X0)
| ( X0 = X1 )
| ~ part_of(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( part_of(X3,X2)
| part_of(X3,X0)
| part_of(X2,X3)
| part_of(X2,X0)
| part_of(X0,X3)
| part_of(X0,X2)
| ~ end_point(X4,X3)
| ~ end_point(X4,X2)
| ~ end_point(X4,X0)
| ~ part_of(X3,X1)
| ~ part_of(X2,X1)
| ~ part_of(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_138,plain,
! [X0: $i] : inner_point(ax0_sk8(X0),X0),
inference(cnf_transformation,[],[f46]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i] :
( meet(X0,ax0_sk9(X0,X1),ax0_sk10(X0,X1))
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i] :
( ( sum(ax0_sk9(X0,X1),ax0_sk10(X0,X1)) = X1 )
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X2 = X3 )
| ( X0 = X3 )
| ( X0 = X2 )
| ~ end_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] :
( end_point(ax0_sk11(X0,X1),X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i] :
( ~ end_point(X0,X1)
| ( ax0_sk11(X0,X1) != X0 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( meet(X3,X1,X2)
| ~ end_point(X3,X1)
| ~ closed(sum(X1,X2))
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sum(X1,X2) = ax0_sk12(X2,X1) )
| ~ meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk13(X0,X1),X1)
| incident_c(ax0_sk13(X0,X1),X0)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ incident_c(ax0_sk13(X0,X1),X1)
| ~ incident_c(ax0_sk13(X0,X1),X0) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] : ~ between_c(X0,X1,X2,X1),
inference(cnf_transformation,[],[f78]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(ax1_sk1(X3,X2,X1,X0),X0)
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X1,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X3,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( inner_point(X2,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( between_c(X1,X2,X4,X3)
| ( X2 = X3 )
| ~ inner_point(X4,X0)
| ~ end_point(X3,X0)
| ~ end_point(X2,X0)
| ~ part_of(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_154,negated_conjecture,
between_c(sk15,sk16,sk17,sk18),
inference(cnf_transformation,[],[f72]) ).
tcf(c_155,negated_conjecture,
( ( sk17 = sk18 )
| ( sk16 = sk18 )
| ( sk16 = sk17 )
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk16,sk15) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_869,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( inner_point(X2,ax1_sk1(X3,X2,X1,X0))
| ( X3 != sk18 )
| ( X2 != sk17 )
| ( X1 != sk16 )
| ( X0 != sk15 ) ),
inference(resolution_lifted,[status(thm)],[c_154,c_152]) ).
tcf(c_870,plain,
inner_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),
inference(unflattening,[status(thm)],[c_869]) ).
tcf(c_874,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X3,ax1_sk1(X3,X2,X1,X0))
| ( X3 != sk18 )
| ( X2 != sk17 )
| ( X1 != sk16 )
| ( X0 != sk15 ) ),
inference(resolution_lifted,[status(thm)],[c_154,c_151]) ).
tcf(c_875,plain,
end_point(sk18,ax1_sk1(sk18,sk17,sk16,sk15)),
inference(unflattening,[status(thm)],[c_874]) ).
tcf(c_879,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X1,ax1_sk1(X3,X2,X1,X0))
| ( X3 != sk18 )
| ( X2 != sk17 )
| ( X1 != sk16 )
| ( X0 != sk15 ) ),
inference(resolution_lifted,[status(thm)],[c_154,c_150]) ).
tcf(c_880,plain,
end_point(sk16,ax1_sk1(sk18,sk17,sk16,sk15)),
inference(unflattening,[status(thm)],[c_879]) ).
tcf(c_884,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(ax1_sk1(X3,X2,X1,X0),X0)
| ( X3 != sk18 )
| ( X2 != sk17 )
| ( X1 != sk16 )
| ( X0 != sk15 ) ),
inference(resolution_lifted,[status(thm)],[c_154,c_149]) ).
tcf(c_885,plain,
part_of(ax1_sk1(sk18,sk17,sk16,sk15),sk15),
inference(unflattening,[status(thm)],[c_884]) ).
tcf(c_889,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 != sk17 )
| ( X1 != sk18 )
| ( X1 != sk16 )
| ( X0 != sk15 ) ),
inference(resolution_lifted,[status(thm)],[c_154,c_148]) ).
tcf(c_890,plain,
sk16 != sk18,
inference(unflattening,[status(thm)],[c_889]) ).
tcf(c_981,plain,
( ( sk17 = sk18 )
| ( sk16 = sk17 )
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk16,sk15) ),
inference(backward_subsumption_resolution,[status(thm)],[c_155,c_890]) ).
tcf(c_1187,plain,
( ( sk17 = sk18 )
| ( sk16 = sk17 )
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk16,sk15) ),
inference(demodulation,[status(thm)],[c_981]) ).
tcf(c_1188,negated_conjecture,
between_c(sk15,sk16,sk17,sk18),
inference(demodulation,[status(thm)],[c_154]) ).
tcf(c_1978,plain,
! [X0: $i] :
( open(X0)
| closed(X0) ),
inference(superposition,[status(thm)],[c_133,c_135]) ).
tcf(c_1990,plain,
! [X0: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X0) ),
inference(superposition,[status(thm)],[c_133,c_114]) ).
tcf(c_2002,plain,
! [X0: $i] : incident_c(ax0_sk8(X0),X0),
inference(superposition,[status(thm)],[c_138,c_122]) ).
tcf(c_2012,plain,
! [X0: $i] :
( ~ open(X0)
| ~ closed(X0) ),
inference(superposition,[status(thm)],[c_134,c_132]) ).
tcf(c_2013,plain,
! [X0: $i] :
( incident_c(ax0_sk7(X0),X0)
| ~ open(X0) ),
inference(superposition,[status(thm)],[c_134,c_114]) ).
tcf(c_2041,plain,
! [X0: $i] :
( closed(X0)
| ~ inner_point(ax0_sk6(X0),X0) ),
inference(superposition,[status(thm)],[c_133,c_123]) ).
tcf(c_2042,plain,
! [X0: $i] :
( ~ open(X0)
| ~ inner_point(ax0_sk7(X0),X0) ),
inference(superposition,[status(thm)],[c_134,c_123]) ).
tcf(c_2069,plain,
! [X0: $i] : part_of(X0,X0),
inference(superposition,[status(thm)],[c_106,c_107]) ).
tcf(c_2075,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,sum(X1,X2))
| ~ incident_c(ax0_sk1(X0,sum(X1,X2)),X1) ),
inference(superposition,[status(thm)],[c_109,c_107]) ).
tcf(c_2083,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ between_c(X3,X0,X2,X1)
| ~ inner_point(X0,ax1_sk1(X1,X2,X0,X3)) ),
inference(superposition,[status(thm)],[c_150,c_123]) ).
tcf(c_2084,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ between_c(X3,X2,X1,X0)
| ~ closed(ax1_sk1(X0,X1,X2,X3)) ),
inference(superposition,[status(thm)],[c_150,c_132]) ).
tcf(c_2085,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(X1,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_150,c_114]) ).
tcf(c_2086,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( open(ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_150,c_135]) ).
tcf(c_2099,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,sum(X1,X2))
| ~ incident_c(ax0_sk1(X0,sum(X1,X2)),X2) ),
inference(superposition,[status(thm)],[c_110,c_107]) ).
tcf(c_2106,plain,
! [X0: $i,X1: $i] :
( ~ end_point(X0,X1)
| ~ inner_point(ax0_sk11(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_142,c_123]) ).
tcf(c_2108,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk11(X0,X1),X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_142,c_114]) ).
tcf(c_2122,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| inner_point(ax0_sk1(X0,X1),X0)
| end_point(ax0_sk1(X0,X1),X0) ),
inference(superposition,[status(thm)],[c_106,c_124]) ).
tcf(c_2123,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(X0,sum(X1,X2))
| end_point(X0,sum(X1,X2))
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_109,c_124]) ).
tcf(c_2124,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(X0,sum(X2,X1))
| end_point(X0,sum(X2,X1))
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_110,c_124]) ).
tcf(c_2126,plain,
! [X0: $i] :
( closed(X0)
| inner_point(ax0_sk6(X0),X0)
| end_point(ax0_sk6(X0),X0) ),
inference(superposition,[status(thm)],[c_1990,c_124]) ).
tcf(c_2147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( open(ax1_sk1(X3,X2,X1,X0))
| ( ax1_sk1(X3,X2,X1,X0) = X0 )
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_136]) ).
tcf(c_2169,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,X2)
| incident_c(ax0_sk1(X0,X2),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_106,c_105]) ).
tcf(c_2170,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(X3,X2)
| ~ incident_c(X3,X0)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_109,c_105]) ).
tcf(c_2171,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(X3,X2)
| ~ incident_c(X3,X1)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_110,c_105]) ).
tcf(c_2172,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(X0),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2002,c_105]) ).
tcf(c_2173,plain,
! [X0: $i,X1: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_1990,c_105]) ).
tcf(c_2174,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk7(X0),X1)
| ~ open(X0)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2013,c_105]) ).
tcf(c_2175,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk11(X2,X0),X1)
| ~ end_point(X2,X0)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2108,c_105]) ).
tcf(c_2203,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(X0),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2172,c_105]) ).
tcf(c_2204,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(X0),X1)
| end_point(ax0_sk8(X0),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2172,c_124]) ).
tcf(c_2217,plain,
! [X0: $i,X1: $i,X2: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2173,c_105]) ).
tcf(c_2218,plain,
! [X0: $i,X1: $i] :
( closed(X0)
| inner_point(ax0_sk6(X0),X1)
| end_point(ax0_sk6(X0),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2173,c_124]) ).
tcf(c_2237,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk7(X0),X2)
| ~ open(X0)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2174,c_105]) ).
tcf(c_2238,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk7(X0),X1)
| end_point(ax0_sk7(X0),X1)
| ~ open(X0)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2174,c_124]) ).
tcf(c_2253,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(sum(X0,X1),X2)
| incident_c(ax0_sk1(sum(X0,X1),X2),X1)
| incident_c(ax0_sk1(sum(X0,X1),X2),X0) ),
inference(superposition,[status(thm)],[c_106,c_108]) ).
tcf(c_2256,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),X1)
| incident_c(ax0_sk8(sum(X0,X1)),X0) ),
inference(superposition,[status(thm)],[c_2002,c_108]) ).
tcf(c_2257,plain,
! [X0: $i,X1: $i] :
( closed(sum(X0,X1))
| incident_c(ax0_sk6(sum(X0,X1)),X1)
| incident_c(ax0_sk6(sum(X0,X1)),X0) ),
inference(superposition,[status(thm)],[c_1990,c_108]) ).
tcf(c_2258,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk7(sum(X0,X1)),X1)
| incident_c(ax0_sk7(sum(X0,X1)),X0)
| ~ open(sum(X0,X1)) ),
inference(superposition,[status(thm)],[c_2013,c_108]) ).
tcf(c_2259,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk11(X0,sum(X1,X2)),X2)
| incident_c(ax0_sk11(X0,sum(X1,X2)),X1)
| ~ end_point(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2108,c_108]) ).
tcf(c_2260,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(X0),X2)
| incident_c(ax0_sk8(X0),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2172,c_108]) ).
tcf(c_2261,plain,
! [X0: $i,X1: $i,X2: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X2)
| incident_c(ax0_sk6(X0),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2173,c_108]) ).
tcf(c_2262,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk7(X0),X2)
| incident_c(ax0_sk7(X0),X1)
| ~ open(X0)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2174,c_108]) ).
tcf(c_2299,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| open(ax0_sk3(X1,X0))
| ( ax0_sk3(X1,X0) = X1 )
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_116,c_136]) ).
tcf(c_2311,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| open(ax0_sk4(X1,X0))
| ( ax0_sk4(X1,X0) = X1 )
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_117,c_136]) ).
tcf(c_2323,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X1,X0)
| incident_c(X1,X2)
| ~ incident_c(X1,X0)
| ~ part_of(ax0_sk3(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_118,c_105]) ).
tcf(c_2324,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| inner_point(X0,ax0_sk3(X1,X0))
| end_point(X0,ax0_sk3(X1,X0))
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_118,c_124]) ).
tcf(c_2338,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( incident_c(X2,X4)
| ~ between_c(X3,X2,X1,X0)
| ~ part_of(ax1_sk1(X0,X1,X2,X3),X4) ),
inference(superposition,[status(thm)],[c_2085,c_105]) ).
tcf(c_2349,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X1,X0)
| incident_c(X1,X2)
| ~ incident_c(X1,X0)
| ~ part_of(ax0_sk4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_119,c_105]) ).
tcf(c_2350,plain,
! [X0: $i,X1: $i] :
( end_point(X0,X1)
| inner_point(X0,ax0_sk4(X1,X0))
| end_point(X0,ax0_sk4(X1,X0))
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_119,c_124]) ).
tcf(c_2364,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,ax0_sk10(X0,X1))
| ~ inner_point(X0,X1) ),
inference(superposition,[status(thm)],[c_139,c_126]) ).
tcf(c_2365,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,ax0_sk9(X0,X1))
| ~ inner_point(X0,X1) ),
inference(superposition,[status(thm)],[c_139,c_125]) ).
tcf(c_2376,plain,
! [X0: $i,X1: $i] :
( ( sum(ax0_sk9(X0,X1),ax0_sk10(X0,X1)) = ax0_sk12(ax0_sk10(X0,X1),ax0_sk9(X0,X1)) )
| ~ inner_point(X0,X1) ),
inference(superposition,[status(thm)],[c_139,c_145]) ).
tcf(c_2384,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ between_c(X3,X2,X1,X0)
| ~ inner_point(X0,ax1_sk1(X0,X1,X2,X3)) ),
inference(superposition,[status(thm)],[c_151,c_123]) ).
tcf(c_2386,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(X3,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_151,c_114]) ).
tcf(c_2398,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X2)
| ~ inner_point(X0,X1)
| ~ part_of(ax0_sk10(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2364,c_105]) ).
tcf(c_2399,plain,
! [X0: $i,X1: $i] :
( inner_point(X0,ax0_sk10(X0,X1))
| end_point(X0,ax0_sk10(X0,X1))
| ~ inner_point(X0,X1) ),
inference(superposition,[status(thm)],[c_2364,c_124]) ).
tcf(c_2411,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(X0,X2)
| ~ inner_point(X0,X1)
| ~ part_of(ax0_sk9(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2365,c_105]) ).
tcf(c_2412,plain,
! [X0: $i,X1: $i] :
( inner_point(X0,ax0_sk9(X0,X1))
| end_point(X0,ax0_sk9(X0,X1))
| ~ inner_point(X0,X1) ),
inference(superposition,[status(thm)],[c_2365,c_124]) ).
tcf(c_2432,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X0,X3)
| incident_c(ax0_sk1(X0,X3),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2169,c_105]) ).
tcf(c_2433,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,X2)
| inner_point(ax0_sk1(X0,X2),X1)
| end_point(ax0_sk1(X0,X2),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2169,c_124]) ).
tcf(c_2435,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X0,X3)
| incident_c(ax0_sk1(X0,X3),X2)
| incident_c(ax0_sk1(X0,X3),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2169,c_108]) ).
tcf(c_2456,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( incident_c(ax0_sk8(ax1_sk1(X3,X2,X1,X0)),X4)
| ~ part_of(X0,X4)
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_2203]) ).
tcf(c_2457,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,X1)
| incident_c(ax0_sk8(ax0_sk3(X1,X0)),X2)
| ~ part_of(X1,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_116,c_2203]) ).
tcf(c_2458,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,X1)
| incident_c(ax0_sk8(ax0_sk4(X1,X0)),X2)
| ~ part_of(X1,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_117,c_2203]) ).
tcf(c_2488,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X2,X0)),X2)
| incident_c(ax0_sk8(sum(X2,X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2256,c_105]) ).
tcf(c_2489,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(sum(X0,X1)),X1)
| end_point(ax0_sk8(sum(X0,X1)),X1)
| incident_c(ax0_sk8(sum(X0,X1)),X0) ),
inference(superposition,[status(thm)],[c_2256,c_124]) ).
tcf(c_2490,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X0) ),
inference(superposition,[status(thm)],[c_2256,c_108]) ).
tcf(c_2491,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,X2)),X2)
| incident_c(ax0_sk8(sum(X0,X2)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2256,c_105]) ).
tcf(c_2492,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(sum(X0,X1)),X0)
| end_point(ax0_sk8(sum(X0,X1)),X0)
| incident_c(ax0_sk8(sum(X0,X1)),X1) ),
inference(superposition,[status(thm)],[c_2256,c_124]) ).
tcf(c_2493,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X0) ),
inference(superposition,[status(thm)],[c_2256,c_108]) ).
tcf(c_2494,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(X0,X0)),X0),
inference(equality_factoring,[status(thm)],[c_2256]) ).
tcf(c_2522,plain,
( incident_c(sk16,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ end_point(sk16,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_2527,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2494,c_105]) ).
tcf(c_2528,plain,
! [X0: $i] :
( inner_point(ax0_sk8(sum(X0,X0)),X0)
| end_point(ax0_sk8(sum(X0,X0)),X0) ),
inference(superposition,[status(thm)],[c_2494,c_124]) ).
tcf(c_2529,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X0) ),
inference(superposition,[status(thm)],[c_2494,c_108]) ).
tcf(c_2542,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2527,c_105]) ).
tcf(c_2543,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(sum(X0,X0)),X1)
| end_point(ax0_sk8(sum(X0,X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2527,c_124]) ).
tcf(c_2544,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),X2)
| incident_c(ax0_sk8(sum(X0,X0)),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2527,c_108]) ).
tcf(c_2563,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(X2,ax1_sk1(X3,X2,X1,X0))
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_152,c_122]) ).
tcf(c_2570,plain,
! [X0: $i,X1: $i] : part_of(X0,sum(X0,X1)),
inference(superposition,[status(thm)],[c_106,c_2075]) ).
tcf(c_2571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X0,sum(sum(X1,X2),X3))
| ~ incident_c(ax0_sk1(X0,sum(sum(X1,X2),X3)),X1) ),
inference(superposition,[status(thm)],[c_109,c_2075]) ).
tcf(c_2572,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X0,sum(sum(X1,X2),X3))
| ~ incident_c(ax0_sk1(X0,sum(sum(X1,X2),X3)),X2) ),
inference(superposition,[status(thm)],[c_110,c_2075]) ).
tcf(c_2573,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,sum(X1,X2))
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2169,c_2075]) ).
tcf(c_2587,plain,
( incident_c(sk18,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ end_point(sk18,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_2596,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( incident_c(X0,X4)
| ~ between_c(X3,X2,X1,X0)
| ~ part_of(ax1_sk1(X0,X1,X2,X3),X4) ),
inference(superposition,[status(thm)],[c_2386,c_105]) ).
tcf(c_2605,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sum(ax0_sk9(X2,ax1_sk1(X3,X2,X1,X0)),ax0_sk10(X2,ax1_sk1(X3,X2,X1,X0))) = ax1_sk1(X3,X2,X1,X0) )
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_152,c_140]) ).
tcf(c_2606,plain,
! [X0: $i] : sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)) = X0,
inference(superposition,[status(thm)],[c_138,c_140]) ).
tcf(c_2607,plain,
! [X0: $i,X1: $i] :
( end_point(ax0_sk8(X0),X1)
| ( sum(ax0_sk9(ax0_sk8(X0),X1),ax0_sk10(ax0_sk8(X0),X1)) = X1 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2204,c_140]) ).
tcf(c_2608,plain,
! [X0: $i] :
( end_point(ax0_sk8(sum(X0,X0)),X0)
| ( sum(ax0_sk9(ax0_sk8(sum(X0,X0)),X0),ax0_sk10(ax0_sk8(sum(X0,X0)),X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_2528,c_140]) ).
tcf(c_2623,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk13(X2,X0),X2)
| incident_c(ax0_sk13(X2,X0),X1)
| ( X0 = X2 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_146,c_105]) ).
tcf(c_2624,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk13(X0,X1),X1)
| end_point(ax0_sk13(X0,X1),X1)
| incident_c(ax0_sk13(X0,X1),X0)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_124]) ).
tcf(c_2625,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk13(X2,sum(X0,X1)),X2)
| incident_c(ax0_sk13(X2,sum(X0,X1)),X1)
| incident_c(ax0_sk13(X2,sum(X0,X1)),X0)
| ( sum(X0,X1) = X2 ) ),
inference(superposition,[status(thm)],[c_146,c_108]) ).
tcf(c_2626,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk13(X0,X2),X2)
| incident_c(ax0_sk13(X0,X2),X1)
| ( X0 = X2 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_146,c_105]) ).
tcf(c_2627,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk13(X0,X1),X0)
| end_point(ax0_sk13(X0,X1),X0)
| incident_c(ax0_sk13(X0,X1),X1)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_124]) ).
tcf(c_2628,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk13(sum(X0,X1),X2),X2)
| incident_c(ax0_sk13(sum(X0,X1),X2),X1)
| incident_c(ax0_sk13(sum(X0,X1),X2),X0)
| ( sum(X0,X1) = X2 ) ),
inference(superposition,[status(thm)],[c_146,c_108]) ).
tcf(c_2659,plain,
( incident_c(sk17,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ inner_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_2674,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(X0),X2)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2570,c_2203]) ).
tcf(c_2675,plain,
! [X0: $i,X1: $i] :
( open(X0)
| ( sum(X0,X1) = X0 ) ),
inference(superposition,[status(thm)],[c_2570,c_136]) ).
tcf(c_2689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(X3),X2)
| ~ part_of(X3,X0)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2573,c_2203]) ).
tcf(c_2690,plain,
! [X0: $i,X1: $i,X2: $i] :
( open(X0)
| ( sum(X1,X2) = X0 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2573,c_136]) ).
tcf(c_2702,plain,
! [X0: $i,X1: $i] : incident_c(ax0_sk8(X0),sum(X0,X1)),
inference(superposition,[status(thm)],[c_2069,c_2674]) ).
tcf(c_2703,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(X0),sum(X2,X3))
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2573,c_2674]) ).
tcf(c_2704,plain,
! [X0: $i,X1: $i,X2: $i] : incident_c(ax0_sk8(X0),sum(sum(X0,X1),X2)),
inference(superposition,[status(thm)],[c_2570,c_2674]) ).
tcf(c_2728,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(X0),sum(X0,X1))
| end_point(ax0_sk8(X0),sum(X0,X1)) ),
inference(superposition,[status(thm)],[c_2702,c_124]) ).
tcf(c_2733,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(X0),X3)
| ~ part_of(sum(sum(X0,X1),X2),X3) ),
inference(superposition,[status(thm)],[c_2704,c_105]) ).
tcf(c_2734,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(X0),sum(sum(X0,X1),X2))
| end_point(ax0_sk8(X0),sum(sum(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_2704,c_124]) ).
tcf(c_2741,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_2573]) ).
tcf(c_2742,plain,
! [X0: $i,X1: $i] :
( part_of(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))
| ~ incident_c(ax0_sk1(X0,X1),ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_2075]) ).
tcf(c_2743,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,ax0_sk10(ax0_sk8(X1),X1))
| incident_c(X0,ax0_sk9(ax0_sk8(X1),X1))
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_2606,c_108]) ).
tcf(c_2744,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_109]) ).
tcf(c_2745,plain,
! [X0: $i,X1: $i] : incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),sum(X0,X1)),
inference(superposition,[status(thm)],[c_2606,c_2704]) ).
tcf(c_2746,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X0),
inference(superposition,[status(thm)],[c_2606,c_2702]) ).
tcf(c_2747,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2606,c_2674]) ).
tcf(c_2748,plain,
! [X0: $i] : part_of(ax0_sk9(ax0_sk8(X0),X0),X0),
inference(superposition,[status(thm)],[c_2606,c_2570]) ).
tcf(c_2749,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax0_sk9(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0))),ax0_sk10(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2256]) ).
tcf(c_2750,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0))),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2256]) ).
tcf(c_2751,plain,
! [X0: $i,X1: $i] :
( incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_110]) ).
tcf(c_2765,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(X0),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(light_normalisation,[status(thm)],[c_2750,c_2606]) ).
tcf(c_2807,plain,
! [X0: $i] :
( open(ax0_sk9(ax0_sk8(X0),X0))
| ( ax0_sk9(ax0_sk8(X0),X0) = X0 ) ),
inference(superposition,[status(thm)],[c_2748,c_136]) ).
tcf(c_2812,plain,
! [X0: $i] :
( inner_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X0)
| end_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X0) ),
inference(superposition,[status(thm)],[c_2746,c_124]) ).
tcf(c_2813,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(sum(X0,X1)),sum(X0,X1))),X1)
| incident_c(ax0_sk8(ax0_sk9(ax0_sk8(sum(X0,X1)),sum(X0,X1))),X0) ),
inference(superposition,[status(thm)],[c_2746,c_108]) ).
tcf(c_2820,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),ax0_sk9(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_2606,c_2745]) ).
tcf(c_2821,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X2)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_2745,c_105]) ).
tcf(c_2822,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),sum(X0,X1))
| end_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),sum(X0,X1)) ),
inference(superposition,[status(thm)],[c_2745,c_124]) ).
tcf(c_2834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(ax1_sk1(X3,X2,X1,ax0_sk9(ax0_sk8(X0),X0)),X0)
| ~ between_c(ax0_sk9(ax0_sk8(X0),X0),X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_2741]) ).
tcf(c_2835,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk9(ax0_sk8(X1),X1))
| part_of(ax0_sk3(ax0_sk9(ax0_sk8(X1),X1),X0),X1)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_116,c_2741]) ).
tcf(c_2836,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk9(ax0_sk8(X1),X1))
| part_of(ax0_sk4(ax0_sk9(ax0_sk8(X1),X1),X0),X1)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_117,c_2741]) ).
tcf(c_2838,plain,
! [X0: $i] : part_of(ax0_sk9(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),ax0_sk9(ax0_sk8(X0),X0)),X0),
inference(superposition,[status(thm)],[c_2748,c_2741]) ).
tcf(c_2855,plain,
! [X0: $i,X1: $i] :
( part_of(ax0_sk9(ax0_sk8(X0),X0),X1)
| incident_c(ax0_sk1(ax0_sk9(ax0_sk8(X0),X0),X1),X0) ),
inference(superposition,[status(thm)],[c_106,c_2744]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk13(X1,ax0_sk9(ax0_sk8(X0),X0)),X1)
| incident_c(ax0_sk13(X1,ax0_sk9(ax0_sk8(X0),X0)),X0)
| ( ax0_sk9(ax0_sk8(X0),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_2744]) ).
tcf(c_2857,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk13(ax0_sk9(ax0_sk8(X0),X0),X1),X1)
| incident_c(ax0_sk13(ax0_sk9(ax0_sk8(X0),X0),X1),X0)
| ( ax0_sk9(ax0_sk8(X0),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_2744]) ).
tcf(c_2859,plain,
! [X0: $i] :
( closed(ax0_sk9(ax0_sk8(X0),X0))
| incident_c(ax0_sk6(ax0_sk9(ax0_sk8(X0),X0)),X0) ),
inference(superposition,[status(thm)],[c_1990,c_2744]) ).
tcf(c_2860,plain,
! [X0: $i] :
( incident_c(ax0_sk7(ax0_sk9(ax0_sk8(X0),X0)),X0)
| ~ open(ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2013,c_2744]) ).
tcf(c_2861,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk11(X0,ax0_sk9(ax0_sk8(X1),X1)),X1)
| ~ end_point(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2108,c_2744]) ).
tcf(c_2862,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,X2)
| incident_c(ax0_sk1(X0,X2),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2169,c_2744]) ).
tcf(c_2863,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(X0),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2172,c_2744]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2173,c_2744]) ).
tcf(c_2865,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk7(X0),X1)
| ~ open(X0)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2174,c_2744]) ).
tcf(c_2866,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),X1)),X1)
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),X1)),X0) ),
inference(superposition,[status(thm)],[c_2256,c_2744]) ).
tcf(c_2867,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,ax0_sk9(ax0_sk8(X1),X1))),X1)
| incident_c(ax0_sk8(sum(X0,ax0_sk9(ax0_sk8(X1),X1))),X0) ),
inference(superposition,[status(thm)],[c_2256,c_2744]) ).
tcf(c_2869,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk9(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_2494,c_2744]) ).
tcf(c_2870,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2527,c_2744]) ).
tcf(c_2915,plain,
sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) = ax1_sk1(sk18,sk17,sk16,sk15),
inference(superposition,[status(thm)],[c_1188,c_2605]) ).
tcf(c_2945,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,ax0_sk9(X1,X2))
| ~ inner_point(X1,X2)
| ~ incident_c(X0,ax0_sk10(X1,X2))
| ~ incident_c(X0,ax0_sk9(X1,X2)) ),
inference(superposition,[status(thm)],[c_139,c_127]) ).
tcf(c_2959,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,ax0_sk10(X1,X2))
| ~ inner_point(X1,X2)
| ~ incident_c(X0,ax0_sk10(X1,X2))
| ~ incident_c(X0,ax0_sk9(X1,X2)) ),
inference(superposition,[status(thm)],[c_139,c_128]) ).
tcf(c_2973,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sum(X1,X2) = X0 )
| ~ incident_c(ax0_sk13(X0,sum(X1,X2)),X1)
| ~ incident_c(ax0_sk13(X0,sum(X1,X2)),X0) ),
inference(superposition,[status(thm)],[c_109,c_147]) ).
tcf(c_2974,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sum(X1,X2) = X0 )
| ~ incident_c(ax0_sk13(X0,sum(X1,X2)),X2)
| ~ incident_c(ax0_sk13(X0,sum(X1,X2)),X0) ),
inference(superposition,[status(thm)],[c_110,c_147]) ).
tcf(c_2990,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X3)
| ~ part_of(X1,X3)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_129,c_105]) ).
tcf(c_2991,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X1,X2)
| inner_point(ax0_sk5(X2,X1,X0),X1)
| end_point(ax0_sk5(X2,X1,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_129,c_124]) ).
tcf(c_2992,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( meet(X0,sum(X1,X2),X3)
| incident_c(ax0_sk5(X3,sum(X1,X2),X0),X2)
| incident_c(ax0_sk5(X3,sum(X1,X2),X0),X1)
| ~ incident_c(X0,X3)
| ~ incident_c(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_129,c_108]) ).
tcf(c_2993,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,ax0_sk9(ax0_sk8(X1),X1),X2)
| incident_c(ax0_sk5(X2,ax0_sk9(ax0_sk8(X1),X1),X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_129,c_2744]) ).
tcf(c_3021,plain,
! [X0: $i,X1: $i] :
( part_of(ax0_sk10(ax0_sk8(X0),X0),X1)
| incident_c(ax0_sk1(ax0_sk10(ax0_sk8(X0),X0),X1),X0) ),
inference(superposition,[status(thm)],[c_106,c_2751]) ).
tcf(c_3022,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,ax0_sk10(ax0_sk8(X1),X1),X2)
| incident_c(ax0_sk5(X2,ax0_sk10(ax0_sk8(X1),X1),X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_129,c_2751]) ).
tcf(c_3023,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk13(X1,ax0_sk10(ax0_sk8(X0),X0)),X1)
| incident_c(ax0_sk13(X1,ax0_sk10(ax0_sk8(X0),X0)),X0)
| ( ax0_sk10(ax0_sk8(X0),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_2751]) ).
tcf(c_3024,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk13(ax0_sk10(ax0_sk8(X0),X0),X1),X1)
| incident_c(ax0_sk13(ax0_sk10(ax0_sk8(X0),X0),X1),X0)
| ( ax0_sk10(ax0_sk8(X0),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_146,c_2751]) ).
tcf(c_3025,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X0),
inference(superposition,[status(thm)],[c_2002,c_2751]) ).
tcf(c_3026,plain,
! [X0: $i] :
( closed(ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk6(ax0_sk10(ax0_sk8(X0),X0)),X0) ),
inference(superposition,[status(thm)],[c_1990,c_2751]) ).
tcf(c_3027,plain,
! [X0: $i] :
( incident_c(ax0_sk7(ax0_sk10(ax0_sk8(X0),X0)),X0)
| ~ open(ax0_sk10(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2013,c_2751]) ).
tcf(c_3028,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk11(X0,ax0_sk10(ax0_sk8(X1),X1)),X1)
| ~ end_point(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2108,c_2751]) ).
tcf(c_3029,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X0,X2)
| incident_c(ax0_sk1(X0,X2),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2169,c_2751]) ).
tcf(c_3030,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(X0),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2172,c_2751]) ).
tcf(c_3031,plain,
! [X0: $i,X1: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2173,c_2751]) ).
tcf(c_3032,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk7(X0),X1)
| ~ open(X0)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2174,c_2751]) ).
tcf(c_3033,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),X1)),X1)
| incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),X1)),X0) ),
inference(superposition,[status(thm)],[c_2256,c_2751]) ).
tcf(c_3034,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,ax0_sk10(ax0_sk8(X1),X1))),X1)
| incident_c(ax0_sk8(sum(X0,ax0_sk10(ax0_sk8(X1),X1))),X0) ),
inference(superposition,[status(thm)],[c_2256,c_2751]) ).
tcf(c_3036,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_2494,c_2751]) ).
tcf(c_3037,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2527,c_2751]) ).
tcf(c_3038,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),ax0_sk10(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_2746,c_2751]) ).
tcf(c_3124,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_3025,c_105]) ).
tcf(c_3125,plain,
! [X0: $i] :
( inner_point(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X0)
| end_point(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X0) ),
inference(superposition,[status(thm)],[c_3025,c_124]) ).
tcf(c_3126,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(sum(X0,X1)),sum(X0,X1))),X1)
| incident_c(ax0_sk8(ax0_sk10(ax0_sk8(sum(X0,X1)),sum(X0,X1))),X0) ),
inference(superposition,[status(thm)],[c_3025,c_108]) ).
tcf(c_3127,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk10(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),ax0_sk9(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_3025,c_2744]) ).
tcf(c_3128,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk10(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),ax0_sk10(ax0_sk8(X0),X0))),X0),
inference(superposition,[status(thm)],[c_3025,c_2751]) ).
tcf(c_3164,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2747,c_105]) ).
tcf(c_3165,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| end_point(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2747,c_124]) ).
tcf(c_3166,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X2)
| incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2747,c_108]) ).
tcf(c_3167,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2747,c_2744]) ).
tcf(c_3168,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2747,c_2751]) ).
tcf(c_3204,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(ax1_sk1(X3,X2,X1,ax0_sk9(ax0_sk8(X0),X0))),X0)
| ~ between_c(ax0_sk9(ax0_sk8(X0),X0),X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_2863]) ).
tcf(c_3205,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk9(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(ax0_sk3(ax0_sk9(ax0_sk8(X1),X1),X0)),X1)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_116,c_2863]) ).
tcf(c_3206,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk9(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(ax0_sk4(ax0_sk9(ax0_sk8(X1),X1),X0)),X1)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_117,c_2863]) ).
tcf(c_3243,plain,
! [X0: $i] :
( part_of(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2573]) ).
tcf(c_3244,plain,
! [X0: $i] :
( part_of(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))
| ~ incident_c(ax0_sk1(X0,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2075]) ).
tcf(c_3245,plain,
! [X0: $i] :
( incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2915,c_108]) ).
tcf(c_3246,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_109]) ).
tcf(c_3247,plain,
incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2915,c_2745]) ).
tcf(c_3248,plain,
! [X0: $i] : incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),
inference(superposition,[status(thm)],[c_2915,c_2704]) ).
tcf(c_3249,plain,
incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2915,c_2702]) ).
tcf(c_3250,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_2915,c_2674]) ).
tcf(c_3251,plain,
part_of(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2915,c_2570]) ).
tcf(c_3252,plain,
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2256]) ).
tcf(c_3253,plain,
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2256]) ).
tcf(c_3254,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_110]) ).
tcf(c_3266,plain,
! [X0: $i] :
( part_of(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(ax0_sk1(X0,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(light_normalisation,[status(thm)],[c_3244,c_2915]) ).
tcf(c_3269,plain,
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(light_normalisation,[status(thm)],[c_3253,c_2915]) ).
tcf(c_3295,plain,
! [X0: $i] :
( incident_c(sk16,X0)
| ~ incident_c(sk16,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_3300,plain,
( incident_c(sk16,sk15)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),sk15)
| ~ incident_c(sk16,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(instantiation,[status(thm)],[c_3295]) ).
tcf(c_3311,plain,
( open(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = ax1_sk1(sk18,sk17,sk16,sk15) ) ),
inference(superposition,[status(thm)],[c_3251,c_136]) ).
tcf(c_3315,plain,
( inner_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| end_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3249,c_124]) ).
tcf(c_3318,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| ~ part_of(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0),X1) ),
inference(superposition,[status(thm)],[c_3248,c_105]) ).
tcf(c_3319,plain,
! [X0: $i] :
( inner_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax1_sk1(sk18,sk17,sk16,sk15),X0))
| end_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)) ),
inference(superposition,[status(thm)],[c_3248,c_124]) ).
tcf(c_3352,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(ax1_sk1(X2,X1,X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ between_c(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1,X2) ),
inference(superposition,[status(thm)],[c_149,c_3243]) ).
tcf(c_3353,plain,
! [X0: $i] :
( end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| part_of(ax0_sk3(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_116,c_3243]) ).
tcf(c_3354,plain,
! [X0: $i] :
( end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| part_of(ax0_sk4(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_117,c_3243]) ).
tcf(c_3356,plain,
part_of(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2748,c_3243]) ).
tcf(c_3395,plain,
! [X0: $i] :
( part_of(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)
| incident_c(ax0_sk1(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_106,c_3246]) ).
tcf(c_3396,plain,
! [X0: $i,X1: $i] :
( meet(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)
| incident_c(ax0_sk5(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_129,c_3246]) ).
tcf(c_3397,plain,
! [X0: $i] :
( incident_c(ax0_sk13(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk13(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = X0 ) ),
inference(superposition,[status(thm)],[c_146,c_3246]) ).
tcf(c_3398,plain,
! [X0: $i] :
( incident_c(ax0_sk13(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X0)
| incident_c(ax0_sk13(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = X0 ) ),
inference(superposition,[status(thm)],[c_146,c_3246]) ).
tcf(c_3400,plain,
( closed(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk6(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_1990,c_3246]) ).
tcf(c_3401,plain,
( incident_c(ax0_sk7(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ open(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2013,c_3246]) ).
tcf(c_3402,plain,
! [X0: $i] :
( incident_c(ax0_sk11(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2108,c_3246]) ).
tcf(c_3403,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| incident_c(ax0_sk1(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2169,c_3246]) ).
tcf(c_3404,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2172,c_3246]) ).
tcf(c_3405,plain,
! [X0: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2173,c_3246]) ).
tcf(c_3406,plain,
! [X0: $i] :
( incident_c(ax0_sk7(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ open(X0)
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2174,c_3246]) ).
tcf(c_3407,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),X0)
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2256,c_3246]) ).
tcf(c_3408,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X0)
| incident_c(ax0_sk8(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2256,c_3246]) ).
tcf(c_3409,plain,
( incident_c(sk17,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ inner_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2365,c_3246]) ).
tcf(c_3410,plain,
incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2494,c_3246]) ).
tcf(c_3411,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2527,c_3246]) ).
tcf(c_3413,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2747,c_3246]) ).
tcf(c_3414,plain,
incident_c(ax0_sk8(ax0_sk10(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_3025,c_3246]) ).
tcf(c_3499,plain,
! [X0: $i] :
( part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)
| incident_c(ax0_sk1(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_106,c_3254]) ).
tcf(c_3500,plain,
! [X0: $i,X1: $i] :
( meet(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)
| incident_c(ax0_sk5(X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_129,c_3254]) ).
tcf(c_3501,plain,
! [X0: $i] :
( incident_c(ax0_sk13(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk13(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = X0 ) ),
inference(superposition,[status(thm)],[c_146,c_3254]) ).
tcf(c_3502,plain,
! [X0: $i] :
( incident_c(ax0_sk13(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X0)
| incident_c(ax0_sk13(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = X0 ) ),
inference(superposition,[status(thm)],[c_146,c_3254]) ).
tcf(c_3503,plain,
incident_c(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2002,c_3254]) ).
tcf(c_3504,plain,
( closed(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk6(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_1990,c_3254]) ).
tcf(c_3505,plain,
( incident_c(ax0_sk7(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ open(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2013,c_3254]) ).
tcf(c_3506,plain,
! [X0: $i] :
( incident_c(ax0_sk11(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ end_point(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2108,c_3254]) ).
tcf(c_3507,plain,
! [X0: $i,X1: $i] :
( part_of(X0,X1)
| incident_c(ax0_sk1(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2169,c_3254]) ).
tcf(c_3508,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2172,c_3254]) ).
tcf(c_3509,plain,
! [X0: $i] :
( closed(X0)
| incident_c(ax0_sk6(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2173,c_3254]) ).
tcf(c_3510,plain,
! [X0: $i] :
( incident_c(ax0_sk7(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ open(X0)
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2174,c_3254]) ).
tcf(c_3511,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),X0)
| incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2256,c_3254]) ).
tcf(c_3512,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X0)
| incident_c(ax0_sk8(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2256,c_3254]) ).
tcf(c_3514,plain,
incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2494,c_3254]) ).
tcf(c_3515,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2527,c_3254]) ).
tcf(c_3516,plain,
incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_2746,c_3254]) ).
tcf(c_3517,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(X0),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2747,c_3254]) ).
tcf(c_3518,plain,
incident_c(ax0_sk8(ax0_sk10(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_3025,c_3254]) ).
tcf(c_3627,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| ~ part_of(X0,X1)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_3250,c_105]) ).
tcf(c_3628,plain,
! [X0: $i] :
( inner_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| end_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_3250,c_124]) ).
tcf(c_3629,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),sum(X0,X1)) ),
inference(superposition,[status(thm)],[c_3250,c_108]) ).
tcf(c_3630,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_3250,c_2744]) ).
tcf(c_3631,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_3250,c_2751]) ).
tcf(c_3668,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),ax0_sk10(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_2490]) ).
tcf(c_3669,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2490]) ).
tcf(c_3670,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),ax0_sk9(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_2490]) ).
tcf(c_3671,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2490]) ).
tcf(c_3672,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),ax0_sk10(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),ax0_sk10(ax0_sk8(X1),X1)))),ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2606,c_2490]) ).
tcf(c_3673,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2490]) ).
tcf(c_3674,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(X2,sum(X3,X0))),X3)
| incident_c(ax0_sk8(sum(X2,sum(X3,X0))),X2)
| incident_c(ax0_sk8(sum(X2,sum(X3,X0))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2490,c_105]) ).
tcf(c_3675,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(X0,sum(X1,X2))),X2)
| end_point(ax0_sk8(sum(X0,sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_124]) ).
tcf(c_3676,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,sum(X2,X3)))),X3)
| incident_c(ax0_sk8(sum(X0,sum(X1,sum(X2,X3)))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,sum(X2,X3)))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,sum(X2,X3)))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_108]) ).
tcf(c_3677,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(ax0_sk8(X2),X2)))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(ax0_sk8(X2),X2)))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(ax0_sk8(X2),X2)))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2744]) ).
tcf(c_3678,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(ax0_sk8(X2),X2)))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(ax0_sk8(X2),X2)))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(ax0_sk8(X2),X2)))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2751]) ).
tcf(c_3679,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3246]) ).
tcf(c_3680,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3254]) ).
tcf(c_3681,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(X2,sum(X0,X3))),X3)
| incident_c(ax0_sk8(sum(X2,sum(X0,X3))),X2)
| incident_c(ax0_sk8(sum(X2,sum(X0,X3))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2490,c_105]) ).
tcf(c_3682,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(X0,sum(X1,X2))),X1)
| end_point(ax0_sk8(sum(X0,sum(X1,X2))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_124]) ).
tcf(c_3683,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(X0,sum(sum(X1,X2),X3))),X3)
| incident_c(ax0_sk8(sum(X0,sum(sum(X1,X2),X3))),X2)
| incident_c(ax0_sk8(sum(X0,sum(sum(X1,X2),X3))),X1)
| incident_c(ax0_sk8(sum(X0,sum(sum(X1,X2),X3))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_108]) ).
tcf(c_3684,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),X2))),X1)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(ax0_sk8(X1),X1),X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2744]) ).
tcf(c_3685,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(ax0_sk8(X1),X1),X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(ax0_sk8(X1),X1),X2))),X1)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(ax0_sk8(X1),X1),X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2751]) ).
tcf(c_3686,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),X1)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3246]) ).
tcf(c_3687,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),X1)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3254]) ).
tcf(c_3688,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X2,X3))),X3)
| incident_c(ax0_sk8(sum(X0,sum(X2,X3))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X2,X3))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2490,c_105]) ).
tcf(c_3689,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(X0,sum(X1,X2))),X0)
| end_point(ax0_sk8(sum(X0,sum(X1,X2))),X0)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(X0,sum(X1,X2))),X1) ),
inference(superposition,[status(thm)],[c_2490,c_124]) ).
tcf(c_3690,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),sum(X2,X3))),X3)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X2,X3))),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X2,X3))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X2,X3))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_108]) ).
tcf(c_3691,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),sum(X1,X2))),X1)
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),sum(X1,X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2744]) ).
tcf(c_3692,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),sum(X1,X2))),X2)
| incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),sum(X1,X2))),X1)
| incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),sum(X1,X2))),X0) ),
inference(superposition,[status(thm)],[c_2490,c_2751]) ).
tcf(c_3693,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),X0)
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3246]) ).
tcf(c_3694,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),X0)
| incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),sum(X0,X1))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2490,c_3254]) ).
tcf(c_3697,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,X1))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,X1))),X0) ),
inference(equality_factoring,[status(thm)],[c_2490]) ).
tcf(c_3699,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X1,X0))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X1,X0))),X0) ),
inference(equality_factoring,[status(thm)],[c_2490]) ).
tcf(c_3700,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(X0,sum(X0,X1))),X0) ),
inference(equality_factoring,[status(thm)],[c_2490]) ).
tcf(c_3788,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(light_normalisation,[status(thm)],[c_3673,c_2915]) ).
tcf(c_3820,plain,
! [X0: $i] :
( incident_c(sk18,X0)
| ~ incident_c(sk18,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_3825,plain,
( incident_c(sk18,sk15)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),sk15)
| ~ incident_c(sk18,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(instantiation,[status(thm)],[c_3820]) ).
tcf(c_3899,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( meet(X0,X1,X2)
| incident_c(ax0_sk5(X2,X1,X0),X3)
| ~ part_of(X2,X3)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_130,c_105]) ).
tcf(c_3900,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X1,X2)
| inner_point(ax0_sk5(X2,X1,X0),X2)
| end_point(ax0_sk5(X2,X1,X0),X2)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_130,c_124]) ).
tcf(c_3901,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( meet(X0,X3,sum(X1,X2))
| incident_c(ax0_sk5(sum(X1,X2),X3,X0),X2)
| incident_c(ax0_sk5(sum(X1,X2),X3,X0),X1)
| ~ incident_c(X0,X3)
| ~ incident_c(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_130,c_108]) ).
tcf(c_3902,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X2,ax0_sk9(ax0_sk8(X1),X1))
| incident_c(ax0_sk5(ax0_sk9(ax0_sk8(X1),X1),X2,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_130,c_2744]) ).
tcf(c_3903,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X0,X2,ax0_sk10(ax0_sk8(X1),X1))
| incident_c(ax0_sk5(ax0_sk10(ax0_sk8(X1),X1),X2,X0),X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_130,c_2751]) ).
tcf(c_3904,plain,
! [X0: $i,X1: $i] :
( meet(X0,X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk5(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1,X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_130,c_3246]) ).
tcf(c_3905,plain,
! [X0: $i,X1: $i] :
( meet(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk5(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1,X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,X1)
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_130,c_3254]) ).
tcf(c_3955,plain,
! [X0: $i,X1: $i,X2: $i] :
( meet(X2,ax0_sk9(X0,X1),ax0_sk10(X0,X1))
| ~ inner_point(X0,X1)
| ~ end_point(X2,ax0_sk9(X0,X1))
| ~ closed(sum(ax0_sk9(X0,X1),ax0_sk10(X0,X1))) ),
inference(superposition,[status(thm)],[c_139,c_144]) ).
tcf(c_3991,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sum(X1,X0) = sum(X2,X3) )
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X2)
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X1) ),
inference(superposition,[status(thm)],[c_109,c_112]) ).
tcf(c_3992,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sum(X1,X0) = sum(X2,X3) )
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X3)
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X1) ),
inference(superposition,[status(thm)],[c_110,c_112]) ).
tcf(c_4006,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sum(X1,X0) = sum(X2,X3) )
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X2)
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X0) ),
inference(superposition,[status(thm)],[c_109,c_113]) ).
tcf(c_4007,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sum(X1,X0) = sum(X2,X3) )
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X3)
| ~ incident_c(ax0_sk2(X0,X1,sum(X2,X3)),X0) ),
inference(superposition,[status(thm)],[c_110,c_113]) ).
tcf(c_4018,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(ax1_sk1(X3,X2,X1,ax0_sk10(ax0_sk8(X0),X0))),X0)
| ~ between_c(ax0_sk10(ax0_sk8(X0),X0),X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_3030]) ).
tcf(c_4019,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk10(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(ax0_sk3(ax0_sk10(ax0_sk8(X1),X1),X0)),X1)
| ~ incident_c(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_116,c_3030]) ).
tcf(c_4020,plain,
! [X0: $i,X1: $i] :
( end_point(X0,ax0_sk10(ax0_sk8(X1),X1))
| incident_c(ax0_sk8(ax0_sk4(ax0_sk10(ax0_sk8(X1),X1),X0)),X1)
| ~ incident_c(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_117,c_3030]) ).
tcf(c_4038,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X2)
| ~ part_of(X1,X2)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_3124,c_105]) ).
tcf(c_4039,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| end_point(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_3124,c_124]) ).
tcf(c_4040,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X2)
| incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_3124,c_108]) ).
tcf(c_4041,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_3124,c_2744]) ).
tcf(c_4042,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),X1)
| ~ part_of(X0,ax0_sk10(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_3124,c_2751]) ).
tcf(c_4043,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3124,c_3246]) ).
tcf(c_4044,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk10(ax0_sk8(X0),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3124,c_3254]) ).
tcf(c_4090,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( open(ax1_sk1(X3,X2,X1,X0))
| ( ax1_sk1(X3,X2,X1,X0) = sum(X0,X4) )
| ~ between_c(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_149,c_2690]) ).
tcf(c_4091,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,X1)
| open(ax0_sk3(X1,X0))
| ( sum(X1,X2) = ax0_sk3(X1,X0) )
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_116,c_2690]) ).
tcf(c_4092,plain,
! [X0: $i,X1: $i,X2: $i] :
( end_point(X0,X1)
| open(ax0_sk4(X1,X0))
| ( sum(X1,X2) = ax0_sk4(X1,X0) )
| ~ incident_c(X0,X1) ),
inference(superposition,[status(thm)],[c_117,c_2690]) ).
tcf(c_4094,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( open(X0)
| ( sum(sum(X1,X2),X3) = X0 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2573,c_2690]) ).
tcf(c_4095,plain,
! [X0: $i,X1: $i,X2: $i] :
( open(X0)
| ( sum(sum(X0,X1),X2) = X0 ) ),
inference(superposition,[status(thm)],[c_2570,c_2690]) ).
tcf(c_4096,plain,
! [X0: $i,X1: $i] :
( open(ax0_sk9(ax0_sk8(X0),X0))
| ( ax0_sk9(ax0_sk8(X0),X0) = sum(X0,X1) ) ),
inference(superposition,[status(thm)],[c_2748,c_2690]) ).
tcf(c_4097,plain,
! [X0: $i] :
( open(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( sum(ax1_sk1(sk18,sk17,sk16,sk15),X0) = ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) ) ),
inference(superposition,[status(thm)],[c_3251,c_2690]) ).
tcf(c_4185,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_3247,c_105]) ).
tcf(c_4186,plain,
( inner_point(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15))
| end_point(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3247,c_124]) ).
tcf(c_4204,plain,
! [X0: $i,X1: $i] :
( incident_c(X1,X0)
| incident_c(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ incident_c(X1,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) ),
inference(superposition,[status(thm)],[c_3245,c_105]) ).
tcf(c_4205,plain,
! [X0: $i] :
( inner_point(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| end_point(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_124]) ).
tcf(c_4206,plain,
! [X0: $i] :
( part_of(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk1(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ incident_c(ax0_sk1(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_107]) ).
tcf(c_4207,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = sum(X1,X0) )
| ~ incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_113]) ).
tcf(c_4208,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = sum(X1,X0) )
| ~ incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| ~ incident_c(ax0_sk2(X0,X1,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_112]) ).
tcf(c_4209,plain,
! [X0: $i] :
( incident_c(ax0_sk13(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = X0 )
| ~ incident_c(ax0_sk13(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ incident_c(ax0_sk13(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_147]) ).
tcf(c_4210,plain,
! [X0: $i,X1: $i] :
( part_of(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1))
| incident_c(ax0_sk1(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ incident_c(ax0_sk1(X0,sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3245,c_2075]) ).
tcf(c_4253,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),X0)
| incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) ),
inference(superposition,[status(thm)],[c_3269,c_105]) ).
tcf(c_4254,plain,
( inner_point(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| end_point(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3269,c_124]) ).
tcf(c_4255,plain,
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3269,c_3254]) ).
tcf(c_4289,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_3788,c_105]) ).
tcf(c_4290,plain,
! [X0: $i] :
( inner_point(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| end_point(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_124]) ).
tcf(c_4291,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_108]) ).
tcf(c_4292,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_2744]) ).
tcf(c_4293,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk10(ax0_sk8(X0),X0),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_2751]) ).
tcf(c_4294,plain,
( incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_3246]) ).
tcf(c_4296,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X1,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk8(sum(X1,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X1,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) ),
inference(superposition,[status(thm)],[c_3788,c_105]) ).
tcf(c_4297,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| inner_point(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| end_point(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_124]) ).
tcf(c_4298,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3788,c_3254]) ).
tcf(c_4299,plain,
( incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(equality_factoring,[status(thm)],[c_3788]) ).
tcf(c_4342,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_3503,c_105]) ).
tcf(c_4343,plain,
( inner_point(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| end_point(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_3503,c_124]) ).
tcf(c_4349,plain,
incident_c(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),
inference(global_subsumption_just,[status(thm)],[c_3409,c_870,c_2659]) ).
tcf(c_4351,plain,
! [X0: $i] :
( incident_c(sk17,X0)
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_4349,c_105]) ).
tcf(c_4352,plain,
( inner_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15))
| end_point(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_4349,c_124]) ).
tcf(c_4383,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax1_sk1(X2,X1,X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ between_c(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1,X2) ),
inference(superposition,[status(thm)],[c_149,c_3404]) ).
tcf(c_4384,plain,
! [X0: $i] :
( end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax0_sk3(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_116,c_3404]) ).
tcf(c_4385,plain,
! [X0: $i] :
( end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax0_sk4(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_117,c_3404]) ).
tcf(c_4405,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2493]) ).
tcf(c_4406,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2493]) ).
tcf(c_4407,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2493]) ).
tcf(c_4408,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2493]) ).
tcf(c_4409,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),ax0_sk9(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),X1)),ax0_sk10(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2493]) ).
tcf(c_4410,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2493]) ).
tcf(c_4411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(X2,X3),X0)),X3)
| incident_c(ax0_sk8(sum(sum(X2,X3),X0)),X2)
| incident_c(ax0_sk8(sum(sum(X2,X3),X0)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2493,c_105]) ).
tcf(c_4412,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X1),X2)),X2)
| end_point(ax0_sk8(sum(sum(X0,X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_124]) ).
tcf(c_4414,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(ax0_sk8(X2),X2))),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(ax0_sk8(X2),X2))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(ax0_sk8(X2),X2))),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2744]) ).
tcf(c_4415,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(ax0_sk8(X2),X2))),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(ax0_sk8(X2),X2))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(ax0_sk8(X2),X2))),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2751]) ).
tcf(c_4416,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X0)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3246]) ).
tcf(c_4417,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),X0)
| incident_c(ax0_sk8(sum(sum(X0,X1),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3254]) ).
tcf(c_4418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(X2,X0),X3)),X3)
| incident_c(ax0_sk8(sum(sum(X2,X0),X3)),X2)
| incident_c(ax0_sk8(sum(sum(X2,X0),X3)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2493,c_105]) ).
tcf(c_4419,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X1),X2)),X1)
| end_point(ax0_sk8(sum(sum(X0,X1),X2)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_124]) ).
tcf(c_4420,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),X3)),X3)
| incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),X3)),X2)
| incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),X3)),X1)
| incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),X3)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_108]) ).
tcf(c_4421,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(ax0_sk8(X1),X1)),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(ax0_sk8(X1),X1)),X2)),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(ax0_sk8(X1),X1)),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2744]) ).
tcf(c_4422,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(ax0_sk8(X1),X1)),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(ax0_sk8(X1),X1)),X2)),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(ax0_sk8(X1),X1)),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2751]) ).
tcf(c_4423,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),X0)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3246]) ).
tcf(c_4424,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),X0)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3254]) ).
tcf(c_4425,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X2),X3)),X3)
| incident_c(ax0_sk8(sum(sum(X0,X2),X3)),X2)
| incident_c(ax0_sk8(sum(sum(X0,X2),X3)),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2493,c_105]) ).
tcf(c_4426,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X1),X2)),X0)
| end_point(ax0_sk8(sum(sum(X0,X1),X2)),X0)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(X0,X1),X2)),X1) ),
inference(superposition,[status(thm)],[c_2493,c_124]) ).
tcf(c_4427,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),X3)),X3)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),X3)),X2)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),X3)),X1)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),X3)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_108]) ).
tcf(c_4428,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),X1),X2)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),X1),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2744]) ).
tcf(c_4429,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),X1),X2)),X2)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),X1),X2)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),X1),X2)),X0) ),
inference(superposition,[status(thm)],[c_2493,c_2751]) ).
tcf(c_4430,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3246]) ).
tcf(c_4431,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),X1)),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2493,c_3254]) ).
tcf(c_4434,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),X1)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),X1)),X0) ),
inference(equality_factoring,[status(thm)],[c_2493]) ).
tcf(c_4436,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X1),X0)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),X0)),X0) ),
inference(equality_factoring,[status(thm)],[c_2493]) ).
tcf(c_4437,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X0),X1)),X1)
| incident_c(ax0_sk8(sum(sum(X0,X0),X1)),X0) ),
inference(equality_factoring,[status(thm)],[c_2493]) ).
tcf(c_4494,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(X0,X1)),X1)
| incident_c(ax0_sk8(sum(X0,X1)),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(X0,X1)),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(light_normalisation,[status(thm)],[c_4409,c_2606]) ).
tcf(c_4518,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(light_normalisation,[status(thm)],[c_4410,c_2915]) ).
tcf(c_4648,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(X3,X2,X0),X3)
| incident_c(ax0_sk2(X3,X2,X0),X2)
| incident_c(ax0_sk2(X3,X2,X0),X1)
| ( sum(X2,X3) = X0 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_111,c_105]) ).
tcf(c_4649,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk2(X1,X0,X2),X2)
| end_point(ax0_sk2(X1,X0,X2),X2)
| incident_c(ax0_sk2(X1,X0,X2),X1)
| incident_c(ax0_sk2(X1,X0,X2),X0)
| ( sum(X0,X1) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_124]) ).
tcf(c_4652,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(X1,X0,sum(X2,X3)),X3)
| incident_c(ax0_sk2(X1,X0,sum(X2,X3)),X2)
| incident_c(ax0_sk2(X1,X0,sum(X2,X3)),X1)
| incident_c(ax0_sk2(X1,X0,sum(X2,X3)),X0)
| ( sum(X0,X1) = sum(X2,X3) ) ),
inference(superposition,[status(thm)],[c_111,c_108]) ).
tcf(c_4653,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(X2,X1,ax0_sk9(ax0_sk8(X0),X0)),X2)
| incident_c(ax0_sk2(X2,X1,ax0_sk9(ax0_sk8(X0),X0)),X1)
| incident_c(ax0_sk2(X2,X1,ax0_sk9(ax0_sk8(X0),X0)),X0)
| ( ax0_sk9(ax0_sk8(X0),X0) = sum(X1,X2) ) ),
inference(superposition,[status(thm)],[c_111,c_2744]) ).
tcf(c_4654,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(X2,X1,ax0_sk10(ax0_sk8(X0),X0)),X2)
| incident_c(ax0_sk2(X2,X1,ax0_sk10(ax0_sk8(X0),X0)),X1)
| incident_c(ax0_sk2(X2,X1,ax0_sk10(ax0_sk8(X0),X0)),X0)
| ( ax0_sk10(ax0_sk8(X0),X0) = sum(X1,X2) ) ),
inference(superposition,[status(thm)],[c_111,c_2751]) ).
tcf(c_4655,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X1,X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk2(X1,X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk2(X1,X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = sum(X0,X1) ) ),
inference(superposition,[status(thm)],[c_111,c_3246]) ).
tcf(c_4656,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X1,X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| incident_c(ax0_sk2(X1,X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk2(X1,X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| ( ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)) = sum(X0,X1) ) ),
inference(superposition,[status(thm)],[c_111,c_3254]) ).
tcf(c_4657,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(X0,X2,X3),X3)
| incident_c(ax0_sk2(X0,X2,X3),X2)
| incident_c(ax0_sk2(X0,X2,X3),X1)
| ( sum(X2,X0) = X3 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_111,c_105]) ).
tcf(c_4658,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk2(X1,X0,X2),X1)
| end_point(ax0_sk2(X1,X0,X2),X1)
| incident_c(ax0_sk2(X1,X0,X2),X2)
| incident_c(ax0_sk2(X1,X0,X2),X0)
| ( sum(X0,X1) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_124]) ).
tcf(c_4661,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(sum(X1,X2),X0,X3),X3)
| incident_c(ax0_sk2(sum(X1,X2),X0,X3),X2)
| incident_c(ax0_sk2(sum(X1,X2),X0,X3),X1)
| incident_c(ax0_sk2(sum(X1,X2),X0,X3),X0)
| ( sum(X0,sum(X1,X2)) = X3 ) ),
inference(superposition,[status(thm)],[c_111,c_108]) ).
tcf(c_4662,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(ax0_sk9(ax0_sk8(X1),X1),X0,X2),X2)
| incident_c(ax0_sk2(ax0_sk9(ax0_sk8(X1),X1),X0,X2),X1)
| incident_c(ax0_sk2(ax0_sk9(ax0_sk8(X1),X1),X0,X2),X0)
| ( sum(X0,ax0_sk9(ax0_sk8(X1),X1)) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_2744]) ).
tcf(c_4663,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(ax0_sk10(ax0_sk8(X1),X1),X0,X2),X2)
| incident_c(ax0_sk2(ax0_sk10(ax0_sk8(X1),X1),X0,X2),X1)
| incident_c(ax0_sk2(ax0_sk10(ax0_sk8(X1),X1),X0,X2),X0)
| ( sum(X0,ax0_sk10(ax0_sk8(X1),X1)) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_2751]) ).
tcf(c_4664,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),X1)
| incident_c(ax0_sk2(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),X0)
| incident_c(ax0_sk2(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) = X1 ) ),
inference(superposition,[status(thm)],[c_111,c_3246]) ).
tcf(c_4665,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),X1)
| incident_c(ax0_sk2(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),X0)
| incident_c(ax0_sk2(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) = X1 ) ),
inference(superposition,[status(thm)],[c_111,c_3254]) ).
tcf(c_4666,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(X2,X0,X3),X3)
| incident_c(ax0_sk2(X2,X0,X3),X2)
| incident_c(ax0_sk2(X2,X0,X3),X1)
| ( sum(X0,X2) = X3 )
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_111,c_105]) ).
tcf(c_4667,plain,
! [X0: $i,X1: $i,X2: $i] :
( inner_point(ax0_sk2(X1,X0,X2),X0)
| end_point(ax0_sk2(X1,X0,X2),X0)
| incident_c(ax0_sk2(X1,X0,X2),X2)
| incident_c(ax0_sk2(X1,X0,X2),X1)
| ( sum(X0,X1) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_124]) ).
tcf(c_4670,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident_c(ax0_sk2(X2,sum(X0,X1),X3),X3)
| incident_c(ax0_sk2(X2,sum(X0,X1),X3),X2)
| incident_c(ax0_sk2(X2,sum(X0,X1),X3),X1)
| incident_c(ax0_sk2(X2,sum(X0,X1),X3),X0)
| ( sum(sum(X0,X1),X2) = X3 ) ),
inference(superposition,[status(thm)],[c_111,c_108]) ).
tcf(c_4671,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(X1,ax0_sk9(ax0_sk8(X0),X0),X2),X2)
| incident_c(ax0_sk2(X1,ax0_sk9(ax0_sk8(X0),X0),X2),X1)
| incident_c(ax0_sk2(X1,ax0_sk9(ax0_sk8(X0),X0),X2),X0)
| ( sum(ax0_sk9(ax0_sk8(X0),X0),X1) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_2744]) ).
tcf(c_4672,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk2(X1,ax0_sk10(ax0_sk8(X0),X0),X2),X2)
| incident_c(ax0_sk2(X1,ax0_sk10(ax0_sk8(X0),X0),X2),X1)
| incident_c(ax0_sk2(X1,ax0_sk10(ax0_sk8(X0),X0),X2),X0)
| ( sum(ax0_sk10(ax0_sk8(X0),X0),X1) = X2 ) ),
inference(superposition,[status(thm)],[c_111,c_2751]) ).
tcf(c_4673,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),X1)
| incident_c(ax0_sk2(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),X0)
| incident_c(ax0_sk2(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_111,c_3246]) ).
tcf(c_4674,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),X1)
| incident_c(ax0_sk2(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),X0)
| incident_c(ax0_sk2(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) = X1 ) ),
inference(superposition,[status(thm)],[c_111,c_3254]) ).
tcf(c_4677,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X1,X0,X1),X1)
| incident_c(ax0_sk2(X1,X0,X1),X0)
| ( sum(X0,X1) = X1 ) ),
inference(equality_factoring,[status(thm)],[c_111]) ).
tcf(c_4679,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X1,X0,X0),X1)
| incident_c(ax0_sk2(X1,X0,X0),X0)
| ( sum(X0,X1) = X0 ) ),
inference(equality_factoring,[status(thm)],[c_111]) ).
tcf(c_4680,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk2(X0,X0,X1),X1)
| incident_c(ax0_sk2(X0,X0,X1),X0)
| ( sum(X0,X0) = X1 ) ),
inference(equality_factoring,[status(thm)],[c_111]) ).
tcf(c_4899,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X3 = X5 )
| ( X0 = X5 )
| ( X0 = X3 )
| ~ between_c(X4,X3,X2,X1)
| ~ end_point(X5,ax1_sk1(X1,X2,X3,X4))
| ~ end_point(X0,ax1_sk1(X1,X2,X3,X4)) ),
inference(superposition,[status(thm)],[c_150,c_141]) ).
tcf(c_4900,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X1 = X5 )
| ( X0 = X5 )
| ( X0 = X1 )
| ~ between_c(X4,X3,X2,X1)
| ~ end_point(X5,ax1_sk1(X1,X2,X3,X4))
| ~ end_point(X0,ax1_sk1(X1,X2,X3,X4)) ),
inference(superposition,[status(thm)],[c_151,c_141]) ).
tcf(c_4901,plain,
! [X0: $i,X1: $i,X2: $i] :
( closed(X1)
| ( X0 = X2 )
| ( ax0_sk6(X1) = X2 )
| ( ax0_sk6(X1) = X0 )
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_133,c_141]) ).
tcf(c_4902,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ( ax0_sk7(X1) = X2 )
| ( ax0_sk7(X1) = X0 )
| ~ open(X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_134,c_141]) ).
tcf(c_4903,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X2 = X3 )
| ( ax0_sk11(X0,X1) = X3 )
| ( ax0_sk11(X0,X1) = X2 )
| ~ end_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_142,c_141]) ).
tcf(c_4958,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( between_c(X4,X0,X6,X5)
| ( X0 = X5 )
| ~ between_c(X4,X3,X2,X1)
| ~ inner_point(X6,ax1_sk1(X1,X2,X3,X4))
| ~ end_point(X5,ax1_sk1(X1,X2,X3,X4))
| ~ end_point(X0,ax1_sk1(X1,X2,X3,X4)) ),
inference(superposition,[status(thm)],[c_149,c_153]) ).
tcf(c_4959,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( end_point(X2,X1)
| between_c(X1,X0,X4,X3)
| ( X0 = X3 )
| ~ incident_c(X2,X1)
| ~ inner_point(X4,ax0_sk3(X1,X2))
| ~ end_point(X3,ax0_sk3(X1,X2))
| ~ end_point(X0,ax0_sk3(X1,X2)) ),
inference(superposition,[status(thm)],[c_116,c_153]) ).
tcf(c_4960,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( end_point(X2,X1)
| between_c(X1,X0,X4,X3)
| ( X0 = X3 )
| ~ incident_c(X2,X1)
| ~ inner_point(X4,ax0_sk4(X1,X2))
| ~ end_point(X3,ax0_sk4(X1,X2))
| ~ end_point(X0,ax0_sk4(X1,X2)) ),
inference(superposition,[status(thm)],[c_117,c_153]) ).
tcf(c_4961,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between_c(X1,X0,X3,X2)
| ( X0 = X2 )
| ~ inner_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_2069,c_153]) ).
tcf(c_4962,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( between_c(sum(X1,X5),X2,X4,X3)
| ( X2 = X3 )
| ~ inner_point(X4,X0)
| ~ end_point(X3,X0)
| ~ end_point(X2,X0)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2573,c_153]) ).
tcf(c_4963,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( between_c(sum(X1,X4),X0,X3,X2)
| ( X0 = X2 )
| ~ inner_point(X3,X1)
| ~ end_point(X2,X1)
| ~ end_point(X0,X1) ),
inference(superposition,[status(thm)],[c_2570,c_153]) ).
tcf(c_4964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between_c(X1,X0,X3,X2)
| ( X0 = X2 )
| ~ inner_point(X3,ax0_sk9(ax0_sk8(X1),X1))
| ~ end_point(X2,ax0_sk9(ax0_sk8(X1),X1))
| ~ end_point(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2748,c_153]) ).
tcf(c_4965,plain,
! [X0: $i,X1: $i,X2: $i] :
( between_c(ax1_sk1(sk18,sk17,sk16,sk15),X0,X2,X1)
| ( X0 = X1 )
| ~ inner_point(X2,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ end_point(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3251,c_153]) ).
tcf(c_5043,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( part_of(X5,ax1_sk1(X1,X2,X3,X4))
| part_of(ax1_sk1(X1,X2,X3,X4),X5)
| ~ end_point(X0,X4)
| ~ part_of(X5,X4)
| ~ incident_c(X0,X5)
| ~ between_c(X4,X3,X2,X1)
| ~ incident_c(X0,ax1_sk1(X1,X2,X3,X4)) ),
inference(superposition,[status(thm)],[c_149,c_115]) ).
tcf(c_5044,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X2,X1)
| part_of(X3,ax0_sk3(X1,X2))
| part_of(ax0_sk3(X1,X2),X3)
| ~ end_point(X0,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X0,X3)
| ~ incident_c(X0,ax0_sk3(X1,X2)) ),
inference(superposition,[status(thm)],[c_116,c_115]) ).
tcf(c_5045,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( end_point(X2,X1)
| part_of(X3,ax0_sk4(X1,X2))
| part_of(ax0_sk4(X1,X2),X3)
| ~ end_point(X0,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X2,X1)
| ~ incident_c(X0,X3)
| ~ incident_c(X0,ax0_sk4(X1,X2)) ),
inference(superposition,[status(thm)],[c_117,c_115]) ).
tcf(c_5047,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( part_of(X4,X0)
| part_of(X0,X4)
| ~ part_of(X4,X1)
| ~ incident_c(X3,X4)
| ~ incident_c(X3,X0)
| ~ end_point(X3,sum(X1,X2))
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2573,c_115]) ).
tcf(c_5048,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X1,X0)
| part_of(X0,X1)
| ~ incident_c(X3,X1)
| ~ incident_c(X3,X0)
| ~ end_point(X3,sum(X1,X2))
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2570,c_115]) ).
tcf(c_5049,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X2,ax0_sk9(ax0_sk8(X1),X1))
| part_of(ax0_sk9(ax0_sk8(X1),X1),X2)
| ~ end_point(X0,X1)
| ~ part_of(X2,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2748,c_115]) ).
tcf(c_5050,plain,
! [X0: $i,X1: $i] :
( part_of(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| part_of(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)
| ~ incident_c(X0,X1)
| ~ end_point(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X1,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3251,c_115]) ).
tcf(c_5104,plain,
( incident_c(sk17,sk15)
| ~ between_c(sk15,sk16,sk17,sk18) ),
inference(superposition,[status(thm)],[c_149,c_4351]) ).
tcf(c_5106,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,sum(X0,X1))
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_2573,c_4351]) ).
tcf(c_5107,plain,
! [X0: $i] : incident_c(sk17,sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),
inference(superposition,[status(thm)],[c_2570,c_4351]) ).
tcf(c_5108,plain,
incident_c(sk17,sk15),
inference(forward_subsumption_resolution,[status(thm)],[c_5104,c_1188]) ).
tcf(c_5111,plain,
( ( sk17 = sk18 )
| ( sk16 = sk17 )
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk16,sk15) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1187,c_5108]) ).
tcf(c_5144,plain,
! [X0: $i] :
( incident_c(sk17,X0)
| ~ part_of(sk15,X0) ),
inference(superposition,[status(thm)],[c_5108,c_105]) ).
tcf(c_5145,plain,
( inner_point(sk17,sk15)
| end_point(sk17,sk15) ),
inference(superposition,[status(thm)],[c_5108,c_124]) ).
tcf(c_5154,plain,
( end_point(sk17,sk15)
| ( sum(ax0_sk9(sk17,sk15),ax0_sk10(sk17,sk15)) = sk15 ) ),
inference(superposition,[status(thm)],[c_5145,c_140]) ).
tcf(c_5163,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,sum(X0,X1))
| ~ part_of(sk15,X0) ),
inference(superposition,[status(thm)],[c_2573,c_5144]) ).
tcf(c_5164,plain,
! [X0: $i] : incident_c(sk17,sum(sk15,X0)),
inference(superposition,[status(thm)],[c_2570,c_5144]) ).
tcf(c_5189,plain,
( ( sk17 = sk18 )
| ( sk16 = sk17 ) ),
inference(global_subsumption_just,[status(thm)],[c_5111,c_875,c_880,c_885,c_2522,c_2587,c_3300,c_3825,c_5111]) ).
tcf(c_5195,plain,
! [X0: $i] :
( incident_c(sk17,X0)
| ( sk16 = sk17 )
| ~ part_of(ax1_sk1(sk17,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_5189,c_4351]) ).
tcf(c_5196,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3404]) ).
tcf(c_5197,plain,
( incident_c(sk17,ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_4349]) ).
tcf(c_5198,plain,
( incident_c(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3503]) ).
tcf(c_5199,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3788]) ).
tcf(c_5200,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk17,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3788]) ).
tcf(c_5201,plain,
( incident_c(ax0_sk8(ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3269]) ).
tcf(c_5202,plain,
! [X0: $i] :
( incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_5189,c_3245]) ).
tcf(c_5203,plain,
! [X0: $i] :
( part_of(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ incident_c(ax0_sk1(X0,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3266]) ).
tcf(c_5204,plain,
( incident_c(ax0_sk8(ax0_sk9(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3247]) ).
tcf(c_5205,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)
| ( sk16 = sk17 )
| ~ part_of(ax1_sk1(sk18,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_5189,c_3250]) ).
tcf(c_5206,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3254]) ).
tcf(c_5207,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3246]) ).
tcf(c_5208,plain,
! [X0: $i] :
( part_of(X0,ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3243]) ).
tcf(c_5209,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),sum(ax1_sk1(sk17,sk17,sk16,sk15),X0))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3248]) ).
tcf(c_5210,plain,
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3249]) ).
tcf(c_5211,plain,
( part_of(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_3251]) ).
tcf(c_5212,plain,
( ( sk16 = sk17 )
| ( sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) = ax1_sk1(sk17,sk17,sk16,sk15) ) ),
inference(superposition,[status(thm)],[c_5189,c_2915]) ).
tcf(c_5213,plain,
( between_c(sk15,sk16,sk17,sk17)
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_1188]) ).
tcf(c_5311,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk17,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2490]) ).
tcf(c_5312,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2490]) ).
tcf(c_5313,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2490]) ).
tcf(c_5314,plain,
! [X0: $i] :
( part_of(X0,ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ part_of(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5212,c_2573]) ).
tcf(c_5315,plain,
! [X0: $i] :
( part_of(X0,sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))
| ( sk16 = sk17 )
| ~ incident_c(ax0_sk1(X0,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5212,c_2075]) ).
tcf(c_5316,plain,
! [X0: $i] :
( incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax1_sk1(sk17,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_5212,c_108]) ).
tcf(c_5317,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5212,c_109]) ).
tcf(c_5318,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2493]) ).
tcf(c_5319,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2493]) ).
tcf(c_5320,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2493]) ).
tcf(c_5324,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)
| ( sk16 = sk17 )
| ~ part_of(ax1_sk1(sk17,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_5212,c_2674]) ).
tcf(c_5326,plain,
( incident_c(ax0_sk8(ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2256]) ).
tcf(c_5327,plain,
( incident_c(ax0_sk8(ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2256]) ).
tcf(c_5328,plain,
! [X0: $i] :
( incident_c(X0,ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5212,c_110]) ).
tcf(c_5433,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_4518]) ).
tcf(c_5434,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_4518]) ).
tcf(c_5436,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X1)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_4518,c_105]) ).
tcf(c_5437,plain,
! [X0: $i] :
( inner_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| end_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_124]) ).
tcf(c_5438,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),sum(X0,X1))),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),sum(X0,X1))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),sum(X0,X1))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_108]) ).
tcf(c_5439,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(ax0_sk8(X0),X0))),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(ax0_sk8(X0),X0))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(ax0_sk8(X0),X0))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_2744]) ).
tcf(c_5440,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(ax0_sk8(X0),X0))),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(ax0_sk8(X0),X0))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(ax0_sk8(X0),X0))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_2751]) ).
tcf(c_5441,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_3246]) ).
tcf(c_5443,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X1)),X1)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X1)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X1)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) ),
inference(superposition,[status(thm)],[c_4518,c_105]) ).
tcf(c_5444,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| inner_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| end_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_124]) ).
tcf(c_5445,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_4518,c_3254]) ).
tcf(c_5446,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(equality_factoring,[status(thm)],[c_4518]) ).
tcf(c_5512,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,X1)
| ~ part_of(sum(sk15,X0),X1) ),
inference(superposition,[status(thm)],[c_5164,c_105]) ).
tcf(c_5513,plain,
! [X0: $i] :
( inner_point(sk17,sum(sk15,X0))
| end_point(sk17,sum(sk15,X0)) ),
inference(superposition,[status(thm)],[c_5164,c_124]) ).
tcf(c_5528,plain,
! [X0: $i] :
( incident_c(sk17,X0)
| ~ part_of(sk15,ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_5163]) ).
tcf(c_5531,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(sk17,X2)
| ~ part_of(sk15,X0)
| ~ part_of(sum(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_5163,c_105]) ).
tcf(c_5532,plain,
! [X0: $i,X1: $i] :
( inner_point(sk17,sum(X0,X1))
| end_point(sk17,sum(X0,X1))
| ~ part_of(sk15,X0) ),
inference(superposition,[status(thm)],[c_5163,c_124]) ).
tcf(c_5558,plain,
( inner_point(sk17,ax1_sk1(sk17,sk17,sk16,sk15))
| end_point(sk17,ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5197,c_124]) ).
tcf(c_5582,plain,
! [X0: $i,X1: $i] :
( ( X1 = sk17 )
| ( X0 = sk17 )
| ( X0 = X1 )
| ( sum(ax0_sk9(sk17,sk15),ax0_sk10(sk17,sk15)) = sk15 )
| ~ end_point(X1,sk15)
| ~ end_point(X0,sk15) ),
inference(superposition,[status(thm)],[c_5154,c_141]) ).
tcf(c_5583,plain,
( ( sum(ax0_sk9(sk17,sk15),ax0_sk10(sk17,sk15)) = sk15 )
| ~ inner_point(sk17,sk15) ),
inference(superposition,[status(thm)],[c_5154,c_123]) ).
tcf(c_5584,plain,
( ( sum(ax0_sk9(sk17,sk15),ax0_sk10(sk17,sk15)) = sk15 )
| ~ closed(sk15) ),
inference(superposition,[status(thm)],[c_5154,c_132]) ).
tcf(c_5586,plain,
( open(sk15)
| ( sum(ax0_sk9(sk17,sk15),ax0_sk10(sk17,sk15)) = sk15 ) ),
inference(superposition,[status(thm)],[c_5154,c_135]) ).
tcf(c_5606,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)))),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2529]) ).
tcf(c_5607,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2529]) ).
tcf(c_5608,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2529]) ).
tcf(c_5612,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),ax0_sk9(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)))),ax0_sk10(ax0_sk8(X0),X0)) ),
inference(superposition,[status(thm)],[c_2606,c_2529]) ).
tcf(c_5613,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_2915,c_2529]) ).
tcf(c_5614,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),sum(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5212,c_2529]) ).
tcf(c_5615,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X2,X0),sum(X2,X0))),X2)
| incident_c(ax0_sk8(sum(sum(X2,X0),sum(X2,X0))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2529,c_105]) ).
tcf(c_5616,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X1)
| end_point(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X1)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_124]) ).
tcf(c_5617,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),sum(X0,sum(X1,X2)))),X2)
| incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),sum(X0,sum(X1,X2)))),X1)
| incident_c(ax0_sk8(sum(sum(X0,sum(X1,X2)),sum(X0,sum(X1,X2)))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_108]) ).
tcf(c_5618,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(ax0_sk8(X1),X1)),sum(X0,ax0_sk9(ax0_sk8(X1),X1)))),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(ax0_sk8(X1),X1)),sum(X0,ax0_sk9(ax0_sk8(X1),X1)))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_2744]) ).
tcf(c_5619,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(ax0_sk8(X1),X1)),sum(X0,ax0_sk10(ax0_sk8(X1),X1)))),X1)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(ax0_sk8(X1),X1)),sum(X0,ax0_sk10(ax0_sk8(X1),X1)))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_2751]) ).
tcf(c_5620,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2529,c_3246]) ).
tcf(c_5621,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),X0)
| incident_c(ax0_sk8(sum(sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2529,c_3254]) ).
tcf(c_5622,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X2),sum(X0,X2))),X2)
| incident_c(ax0_sk8(sum(sum(X0,X2),sum(X0,X2))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_2529,c_105]) ).
tcf(c_5623,plain,
! [X0: $i,X1: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X0)
| end_point(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X0)
| incident_c(ax0_sk8(sum(sum(X0,X1),sum(X0,X1))),X1) ),
inference(superposition,[status(thm)],[c_2529,c_124]) ).
tcf(c_5624,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),sum(sum(X0,X1),X2))),X2)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),sum(sum(X0,X1),X2))),X1)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),X2),sum(sum(X0,X1),X2))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_108]) ).
tcf(c_5625,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),X1),sum(ax0_sk9(ax0_sk8(X0),X0),X1))),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),X1),sum(ax0_sk9(ax0_sk8(X0),X0),X1))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_2744]) ).
tcf(c_5626,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),X1),sum(ax0_sk10(ax0_sk8(X0),X0),X1))),X1)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),X1),sum(ax0_sk10(ax0_sk8(X0),X0),X1))),X0) ),
inference(superposition,[status(thm)],[c_2529,c_2751]) ).
tcf(c_5627,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0))),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2529,c_3246]) ).
tcf(c_5628,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0))),X0)
| incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0),sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0))),ax1_sk1(sk18,sk17,sk16,sk15)) ),
inference(superposition,[status(thm)],[c_2529,c_3254]) ).
tcf(c_5629,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(sum(X0,X0),sum(X0,X0))),X0),
inference(equality_factoring,[status(thm)],[c_2529]) ).
tcf(c_5651,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(X0,X0)),ax0_sk10(ax0_sk8(X0),X0))
| incident_c(ax0_sk8(sum(X0,X0)),ax0_sk9(ax0_sk8(X0),X0)) ),
inference(light_normalisation,[status(thm)],[c_5612,c_2606]) ).
tcf(c_5669,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(light_normalisation,[status(thm)],[c_5613,c_2915]) ).
tcf(c_5795,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( part_of(X6,X5)
| part_of(X5,X6)
| part_of(X6,ax1_sk1(X1,X2,X3,X4))
| part_of(X5,ax1_sk1(X1,X2,X3,X4))
| part_of(ax1_sk1(X1,X2,X3,X4),X6)
| part_of(ax1_sk1(X1,X2,X3,X4),X5)
| ~ end_point(X0,X6)
| ~ end_point(X0,X5)
| ~ part_of(X6,X4)
| ~ part_of(X5,X4)
| ~ between_c(X4,X3,X2,X1)
| ~ end_point(X0,ax1_sk1(X1,X2,X3,X4)) ),
inference(superposition,[status(thm)],[c_149,c_137]) ).
tcf(c_5796,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( end_point(X2,X1)
| part_of(X4,X3)
| part_of(X3,X4)
| part_of(X4,ax0_sk3(X1,X2))
| part_of(X3,ax0_sk3(X1,X2))
| part_of(ax0_sk3(X1,X2),X4)
| part_of(ax0_sk3(X1,X2),X3)
| ~ end_point(X0,X4)
| ~ end_point(X0,X3)
| ~ part_of(X4,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X2,X1)
| ~ end_point(X0,ax0_sk3(X1,X2)) ),
inference(superposition,[status(thm)],[c_116,c_137]) ).
tcf(c_5797,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( end_point(X2,X1)
| part_of(X4,X3)
| part_of(X3,X4)
| part_of(X4,ax0_sk4(X1,X2))
| part_of(X3,ax0_sk4(X1,X2))
| part_of(ax0_sk4(X1,X2),X4)
| part_of(ax0_sk4(X1,X2),X3)
| ~ end_point(X0,X4)
| ~ end_point(X0,X3)
| ~ part_of(X4,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X2,X1)
| ~ end_point(X0,ax0_sk4(X1,X2)) ),
inference(superposition,[status(thm)],[c_117,c_137]) ).
tcf(c_5799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( part_of(X4,X3)
| part_of(X4,X0)
| part_of(X3,X4)
| part_of(X3,X0)
| part_of(X0,X4)
| part_of(X0,X3)
| ~ end_point(X5,X4)
| ~ end_point(X5,X3)
| ~ end_point(X5,X0)
| ~ part_of(X4,X1)
| ~ part_of(X3,sum(X1,X2))
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2573,c_137]) ).
tcf(c_5800,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( part_of(X3,X1)
| part_of(X3,X0)
| part_of(X1,X3)
| part_of(X1,X0)
| part_of(X0,X3)
| part_of(X0,X1)
| ~ end_point(X4,X3)
| ~ end_point(X4,X1)
| ~ end_point(X4,X0)
| ~ part_of(X3,sum(X1,X2))
| ~ part_of(X0,sum(X1,X2)) ),
inference(superposition,[status(thm)],[c_2570,c_137]) ).
tcf(c_5801,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( part_of(X3,X2)
| part_of(X2,X3)
| part_of(X3,ax0_sk9(ax0_sk8(X1),X1))
| part_of(X2,ax0_sk9(ax0_sk8(X1),X1))
| part_of(ax0_sk9(ax0_sk8(X1),X1),X3)
| part_of(ax0_sk9(ax0_sk8(X1),X1),X2)
| ~ end_point(X0,X3)
| ~ end_point(X0,X2)
| ~ part_of(X3,X1)
| ~ part_of(X2,X1)
| ~ end_point(X0,ax0_sk9(ax0_sk8(X1),X1)) ),
inference(superposition,[status(thm)],[c_2748,c_137]) ).
tcf(c_5802,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X2,X1)
| part_of(X1,X2)
| part_of(X2,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| part_of(X1,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| part_of(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X2)
| part_of(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X1)
| ~ end_point(X0,X2)
| ~ end_point(X0,X1)
| ~ part_of(X2,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ part_of(X1,ax1_sk1(sk18,sk17,sk16,sk15))
| ~ end_point(X0,ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_3251,c_137]) ).
tcf(c_5891,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(sk17,sum(X1,X2))
| ~ part_of(sum(sk15,X0),X1) ),
inference(superposition,[status(thm)],[c_2573,c_5512]) ).
tcf(c_5892,plain,
! [X0: $i,X1: $i] : incident_c(sk17,sum(sum(sk15,X0),X1)),
inference(superposition,[status(thm)],[c_2570,c_5512]) ).
tcf(c_5900,plain,
! [X0: $i] :
( end_point(sk17,sum(sk15,X0))
| ( sum(ax0_sk9(sk17,sum(sk15,X0)),ax0_sk10(sk17,sum(sk15,X0))) = sum(sk15,X0) ) ),
inference(superposition,[status(thm)],[c_5513,c_140]) ).
tcf(c_5905,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(sk17,X2)
| ~ part_of(sum(sum(sk15,X0),X1),X2) ),
inference(superposition,[status(thm)],[c_5892,c_105]) ).
tcf(c_5906,plain,
! [X0: $i,X1: $i] :
( inner_point(sk17,sum(sum(sk15,X0),X1))
| end_point(sk17,sum(sum(sk15,X0),X1)) ),
inference(superposition,[status(thm)],[c_5892,c_124]) ).
tcf(c_5913,plain,
! [X0: $i] :
( incident_c(sk17,sum(ax1_sk1(sk17,sk17,sk16,sk15),X0))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_5107]) ).
tcf(c_5914,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,X1)
| ~ part_of(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0),X1) ),
inference(superposition,[status(thm)],[c_5107,c_105]) ).
tcf(c_5915,plain,
! [X0: $i] :
( inner_point(sk17,sum(ax1_sk1(sk18,sk17,sk16,sk15),X0))
| end_point(sk17,sum(ax1_sk1(sk18,sk17,sk16,sk15),X0)) ),
inference(superposition,[status(thm)],[c_5107,c_124]) ).
tcf(c_5938,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(X0,X0),sum(X0,X0))),X1)
| ~ part_of(X0,X1) ),
inference(superposition,[status(thm)],[c_5629,c_105]) ).
tcf(c_5939,plain,
! [X0: $i] :
( inner_point(ax0_sk8(sum(sum(X0,X0),sum(X0,X0))),X0)
| end_point(ax0_sk8(sum(sum(X0,X0),sum(X0,X0))),X0) ),
inference(superposition,[status(thm)],[c_5629,c_124]) ).
tcf(c_5940,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(sum(sum(sum(X0,X1),sum(X0,X1)),sum(sum(X0,X1),sum(X0,X1)))),X1)
| incident_c(ax0_sk8(sum(sum(sum(X0,X1),sum(X0,X1)),sum(sum(X0,X1),sum(X0,X1)))),X0) ),
inference(superposition,[status(thm)],[c_5629,c_108]) ).
tcf(c_5941,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk9(ax0_sk8(X0),X0)),sum(ax0_sk9(ax0_sk8(X0),X0),ax0_sk9(ax0_sk8(X0),X0)))),X0),
inference(superposition,[status(thm)],[c_5629,c_2744]) ).
tcf(c_5942,plain,
! [X0: $i] : incident_c(ax0_sk8(sum(sum(ax0_sk10(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)),sum(ax0_sk10(ax0_sk8(X0),X0),ax0_sk10(ax0_sk8(X0),X0)))),X0),
inference(superposition,[status(thm)],[c_5629,c_2751]) ).
tcf(c_5943,plain,
incident_c(ax0_sk8(sum(sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_5629,c_3246]) ).
tcf(c_5944,plain,
incident_c(ax0_sk8(sum(sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))))),ax1_sk1(sk18,sk17,sk16,sk15)),
inference(superposition,[status(thm)],[c_5629,c_3254]) ).
tcf(c_5974,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk17,sk17,sk16,sk15),ax1_sk1(sk17,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5189,c_5669]) ).
tcf(c_5977,plain,
! [X0: $i] :
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),X0)
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| ~ part_of(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0) ),
inference(superposition,[status(thm)],[c_5669,c_105]) ).
tcf(c_5978,plain,
( inner_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| end_point(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5669,c_124]) ).
tcf(c_5979,plain,
( incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax1_sk1(sk18,sk17,sk16,sk15))
| incident_c(ax0_sk8(sum(ax1_sk1(sk18,sk17,sk16,sk15),ax1_sk1(sk18,sk17,sk16,sk15))),ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5669,c_3254]) ).
tcf(c_5994,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,X1)
| ( sk16 = sk17 )
| ~ part_of(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0),X1) ),
inference(superposition,[status(thm)],[c_5913,c_105]) ).
tcf(c_5995,plain,
! [X0: $i] :
( inner_point(sk17,sum(ax1_sk1(sk17,sk17,sk16,sk15),X0))
| end_point(sk17,sum(ax1_sk1(sk17,sk17,sk16,sk15),X0))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5913,c_124]) ).
tcf(c_6061,plain,
! [X0: $i,X1: $i] :
( incident_c(sk17,sum(X0,X1))
| ( sk16 = sk17 )
| ~ part_of(ax1_sk1(sk17,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_2573,c_5195]) ).
tcf(c_6070,plain,
! [X0: $i,X1: $i] :
( part_of(X1,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| part_of(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),X1)
| ( sk16 = sk17 )
| ~ incident_c(X0,X1)
| ~ end_point(X0,ax1_sk1(sk17,sk17,sk16,sk15))
| ~ part_of(X1,ax1_sk1(sk17,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5211,c_115]) ).
tcf(c_6071,plain,
! [X0: $i,X1: $i,X2: $i] :
( part_of(X2,X1)
| part_of(X1,X2)
| part_of(X2,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| part_of(X1,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| part_of(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),X2)
| part_of(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)),X1)
| ( sk16 = sk17 )
| ~ end_point(X0,X2)
| ~ end_point(X0,X1)
| ~ part_of(X2,ax1_sk1(sk17,sk17,sk16,sk15))
| ~ part_of(X1,ax1_sk1(sk17,sk17,sk16,sk15))
| ~ end_point(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5211,c_137]) ).
tcf(c_6072,plain,
! [X0: $i,X1: $i,X2: $i] :
( between_c(ax1_sk1(sk17,sk17,sk16,sk15),X0,X2,X1)
| ( sk16 = sk17 )
| ( X0 = X1 )
| ~ inner_point(X2,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ~ end_point(X1,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ~ end_point(X0,ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5211,c_153]) ).
tcf(c_6073,plain,
! [X0: $i] :
( open(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 )
| ( sum(ax1_sk1(sk17,sk17,sk16,sk15),X0) = ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)) ) ),
inference(superposition,[status(thm)],[c_5211,c_2690]) ).
tcf(c_6075,plain,
( open(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)))
| ( sk16 = sk17 )
| ( ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15)) = ax1_sk1(sk17,sk17,sk16,sk15) ) ),
inference(superposition,[status(thm)],[c_5211,c_136]) ).
tcf(c_6113,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax1_sk1(X2,X1,X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ between_c(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0,X1,X2) ),
inference(superposition,[status(thm)],[c_149,c_3508]) ).
tcf(c_6114,plain,
! [X0: $i] :
( end_point(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax0_sk3(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_116,c_3508]) ).
tcf(c_6115,plain,
! [X0: $i] :
( end_point(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)))
| incident_c(ax0_sk8(ax0_sk4(ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15)),X0)),ax1_sk1(sk18,sk17,sk16,sk15))
| ~ incident_c(X0,ax0_sk10(sk17,ax1_sk1(sk18,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_117,c_3508]) ).
tcf(c_6118,plain,
! [X0: $i] :
( incident_c(ax0_sk8(X0),ax1_sk1(sk18,sk17,sk16,sk15))
| ( sk16 = sk17 )
| ~ part_of(X0,ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))) ),
inference(superposition,[status(thm)],[c_5189,c_3508]) ).
tcf(c_6138,plain,
! [X0: $i] :
( incident_c(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),X0)
| ( sk16 = sk17 )
| ~ part_of(ax1_sk1(sk17,sk17,sk16,sk15),X0) ),
inference(superposition,[status(thm)],[c_5198,c_105]) ).
tcf(c_6139,plain,
( inner_point(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| end_point(ax0_sk8(ax0_sk10(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5198,c_124]) ).
tcf(c_6160,plain,
( inner_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| end_point(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk17,sk17,sk16,sk15))),ax1_sk1(sk17,sk17,sk16,sk15))
| ( sk16 = sk17 ) ),
inference(superposition,[status(thm)],[c_5210,c_124]) ).
tcf(c_6169,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(X1,X2))
| ~ part_of(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0),X1) ),
inference(superposition,[status(thm)],[c_2573,c_3318]) ).
tcf(c_6170,plain,
! [X0: $i,X1: $i] : incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),sum(sum(ax1_sk1(sk18,sk17,sk16,sk15),X0),X1)),
inference(superposition,[status(thm)],[c_2570,c_3318]) ).
tcf(c_6171,plain,
! [X0: $i,X1: $i] :
( incident_c(ax0_sk8(ax0_sk9(sk17,ax1_sk1(sk18,sk17,sk16,sk15))),X1)
| ( sk16 = sk17 )
| ~ part_of(sum(ax1_sk1(sk17,sk17,sk16,sk15),X0),X1) ),
inference(superposition,[status(thm)],[c_5189,c_3318]) ).
tcf(c_6213,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_6171,c_6170,c_6169,c_6160,c_6139,c_6138,c_6118,c_6115,c_6114,c_6113,c_6075,c_6073,c_6072,c_6071,c_6070,c_6061,c_5995,c_5994,c_5979,c_5978,c_5977,c_5974,c_5944,c_5943,c_5942,c_5941,c_5940,c_5939,c_5938,c_5915,c_5914,c_5913,c_5906,c_5905,c_5900,c_5892,c_5891,c_5802,c_5801,c_5800,c_5799,c_5797,c_5796,c_5795,c_5669,c_5651,c_5629,c_5628,c_5627,c_5626,c_5625,c_5624,c_5623,c_5622,c_5621,c_5620,c_5619,c_5618,c_5617,c_5616,c_5615,c_5614,c_5613,c_5612,c_5608,c_5607,c_5606,c_5586,c_5584,c_5583,c_5582,c_5558,c_5532,c_5531,c_5528,c_5513,c_5512,c_5446,c_5445,c_5444,c_5443,c_5441,c_5440,c_5439,c_5438,c_5437,c_5436,c_5434,c_5433,c_5328,c_5327,c_5326,c_5324,c_5320,c_5319,c_5318,c_5317,c_5316,c_5315,c_5314,c_5313,c_5312,c_5311,c_5213,c_5212,c_5211,c_5210,c_5209,c_5208,c_5207,c_5206,c_5205,c_5204,c_5203,c_5202,c_5201,c_5200,c_5199,c_5198,c_5197,c_5196,c_5195,c_5189,c_5164,c_5163,c_5154,c_5145,c_5144,c_5111,c_5108,c_5107,c_5106,c_5104,c_5050,c_5049,c_5048,c_5047,c_5045,c_5044,c_5043,c_4965,c_4964,c_4963,c_4962,c_4961,c_4960,c_4959,c_4958,c_4903,c_4902,c_4901,c_4900,c_4899,c_4680,c_4679,c_4677,c_4674,c_4673,c_4672,c_4671,c_4670,c_4667,c_4666,c_4665,c_4664,c_4663,c_4662,c_4661,c_4658,c_4657,c_4656,c_4655,c_4654,c_4653,c_4652,c_4649,c_4648,c_4518,c_4494,c_4437,c_4436,c_4434,c_4431,c_4430,c_4429,c_4428,c_4427,c_4426,c_4425,c_4424,c_4423,c_4422,c_4421,c_4420,c_4419,c_4418,c_4417,c_4416,c_4415,c_4414,c_4412,c_4411,c_4410,c_4409,c_4408,c_4407,c_4406,c_4405,c_4385,c_4384,c_4383,c_4352,c_4351,c_4349,c_4343,c_4342,c_4299,c_4298,c_4297,c_4296,c_4294,c_4293,c_4292,c_4291,c_4290,c_4289,c_4255,c_4254,c_4253,c_4210,c_4209,c_4208,c_4207,c_4206,c_4205,c_4204,c_4186,c_4185,c_4097,c_4096,c_4095,c_4094,c_4092,c_4091,c_4090,c_4044,c_4043,c_4042,c_4041,c_4040,c_4039,c_4038,c_4020,c_4019,c_4018,c_4007,c_4006,c_3992,c_3991,c_3955,c_3905,c_3904,c_3903,c_3902,c_3901,c_3900,c_3899,c_3788,c_3700,c_3699,c_3697,c_3694,c_3693,c_3692,c_3691,c_3690,c_3689,c_3688,c_3687,c_3686,c_3685,c_3684,c_3683,c_3682,c_3681,c_3680,c_3679,c_3678,c_3677,c_3676,c_3675,c_3674,c_3673,c_3672,c_3671,c_3670,c_3669,c_3668,c_3631,c_3630,c_3629,c_3628,c_3627,c_3518,c_3517,c_3516,c_3515,c_3514,c_3512,c_3511,c_3510,c_3509,c_3508,c_3507,c_3506,c_3505,c_3504,c_3503,c_3502,c_3501,c_3500,c_3499,c_3414,c_3413,c_3411,c_3410,c_3408,c_3407,c_3406,c_3405,c_3404,c_3403,c_3402,c_3401,c_3400,c_3398,c_3397,c_3396,c_3395,c_3356,c_3354,c_3353,c_3352,c_3319,c_3318,c_3315,c_3311,c_3269,c_3266,c_3254,c_3253,c_3252,c_3251,c_3250,c_3249,c_3248,c_3247,c_3246,c_3245,c_3244,c_3243,c_3206,c_3205,c_3204,c_3168,c_3167,c_3166,c_3165,c_3164,c_3128,c_3127,c_3126,c_3125,c_3124,c_3038,c_3037,c_3036,c_3034,c_3033,c_3032,c_3031,c_3030,c_3029,c_3028,c_3027,c_3026,c_3025,c_3024,c_3023,c_3022,c_3021,c_2993,c_2992,c_2991,c_2990,c_2974,c_2973,c_2959,c_2945,c_2915,c_2870,c_2869,c_2867,c_2866,c_2865,c_2864,c_2863,c_2862,c_2861,c_2860,c_2859,c_2857,c_2856,c_2855,c_2838,c_2836,c_2835,c_2834,c_2822,c_2821,c_2820,c_2813,c_2812,c_2807,c_2765,c_2751,c_2750,c_2749,c_2748,c_2747,c_2746,c_2745,c_2744,c_2743,c_2742,c_2741,c_2734,c_2733,c_2728,c_2704,c_2703,c_2702,c_2690,c_2689,c_2675,c_2674,c_3409,c_2628,c_2627,c_2626,c_2625,c_2624,c_2623,c_2608,c_2607,c_2596,c_2573,c_2572,c_2571,c_2570,c_2544,c_2543,c_2542,c_2529,c_2528,c_2527,c_2494,c_2493,c_2492,c_2491,c_2490,c_2489,c_2488,c_2458,c_2457,c_2456,c_2435,c_2433,c_2432,c_2412,c_2411,c_2399,c_2398,c_2386,c_2384,c_2376,c_2365,c_2364,c_2350,c_2349,c_2338,c_2324,c_2323,c_2311,c_2299,c_2262,c_2261,c_2260,c_2259,c_2258,c_2257,c_2256,c_2253,c_2238,c_2237,c_2218,c_2217,c_2204,c_2203,c_2175,c_2174,c_2173,c_2172,c_2171,c_2170,c_2169,c_2147,c_2126,c_2124,c_2123,c_2122,c_2108,c_2106,c_2099,c_2086,c_2085,c_2084,c_2083,c_2075,c_2069,c_2042,c_2041,c_2013,c_2012,c_1990,c_1978,c_2002,c_2606,c_2563,c_2605,c_1187,c_148,c_146,c_144,c_110,c_109,c_108,c_147,c_145,c_143,c_142,c_141,c_140,c_139,c_138,c_137,c_136,c_135,c_134,c_133,c_132,c_131,c_130,c_129,c_128,c_127,c_126,c_125,c_124,c_123,c_122,c_121,c_120,c_119,c_118,c_117,c_116,c_115,c_114,c_113,c_112,c_111,c_107,c_106,c_105,c_153,c_152,c_151,c_150,c_149,c_1188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO111-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Wed Sep 23 10:57:18 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.45 Running first-order theorem proving
% 0.12/0.45 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.46
% 0.12/0.46 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.46
% 0.12/0.47 % Detected problem language: tptp
% 0.20/0.48 % Proving...
% 8.32/1.93 % SZS status Started for theBenchmark.p
% 8.32/1.93 % SZS status Unsatisfiable for theBenchmark.p
% 8.32/1.93
% 8.32/1.93 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.32/1.93
% 8.32/1.93 % ------ iProver source info
% 8.32/1.93
% 8.32/1.93 % git: date: 2026-07-19 20:42:38 +0200
% 8.32/1.93 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.32/1.93 % git: non_committed_changes: false
% 8.32/1.93
% 8.32/1.93 % ------ Parsing...% successful
% 8.32/1.93
% 8.32/1.93
% 8.32/1.93 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.32/1.93
% 8.32/1.93 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 8.32/1.93
% 8.32/1.93 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.32/1.93
% 8.32/1.93 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.32/1.93 % ------ Proving...
% 8.32/1.93 % ------ Problem Properties
% 8.32/1.93
% 8.32/1.93 %
% 8.32/1.93 % clauses 51
% 8.32/1.93 % conjectures 1
% 8.32/1.93 % EPR 19
% 8.32/1.93 % Horn 33
% 8.32/1.93 % unary 3
% 8.32/1.93 % binary 22
% 8.32/1.93 % lits 154
% 8.32/1.93 % lits eq 15
% 8.32/1.93 % fd_pure 0
% 8.32/1.93 % fd_pseudo 0
% 8.32/1.93 % fd_cond 0
% 8.32/1.93 % fd_pseudo_cond 8
% 8.32/1.93 % AC symbols 0
% 8.32/1.93
% 8.32/1.93 % ------ Schedule dynamic 5 is on
% 8.32/1.93
% 8.32/1.93 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.32/1.93
% 8.32/1.93
% 8.32/1.93 % ------
% 8.32/1.93 % Current options:
% 8.32/1.93 % ------
% 8.32/1.93
% 8.32/1.93
% 8.32/1.93 %
% 8.32/1.93
% 8.32/1.93 % ------ Proving...
% 8.32/1.93 %
% 8.32/1.93
% 8.32/1.93 % SZS status Unsatisfiable for theBenchmark.p
% 8.32/1.93
% 8.32/1.93 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.32/1.96
% 8.32/1.96
%------------------------------------------------------------------------------