%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO499+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n016.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:21:10 PM UTC 2026
% Result : Theorem 47.62s 11.23s
% Output : CNFRefutation 47.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 111
% Syntax : Number of formulae : 1053 ( 292 unt; 3 def)
% Number of atoms : 4058 ( 464 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 2407 (1079 ~;1288 |; 40 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 4 prp; 0-8 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-6 aty)
% Number of variables : 2194 ( 0 sgn2190 !; 4 ?;1258 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : s_e(X0,X1,X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA1) ).
fof(f2,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA2) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( s_e(X1,ext(X0,X1,X2,X3),X2,X3)
& s_t(X0,X1,ext(X0,X1,X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA4) ).
fof(f5,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( s_e(X4,X6,X5,X7)
| X0 = X1
| ~ s_t(X2,X3,X5)
| ~ s_t(X0,X1,X4)
| ~ s_e(X1,X6,X3,X7)
| ~ s_e(X0,X6,X2,X7)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA5) ).
fof(f6,axiom,
! [X0,X1] :
( X0 = X1
| ~ s_t(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA6) ).
fof(f7,axiom,
! [X0,X1,X2,X3,X4] :
( ( s_t(X4,ip(X0,X1,X2,X3,X4),X0)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) )
& ( s_t(X1,ip(X0,X1,X2,X3,X4),X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA7) ).
fof(f8,axiom,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO011+0.ax',aA8) ).
fof(f9,axiom,
! [X0,X1] : s_e(X0,X1,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_1) ).
fof(f10,axiom,
! [X0,X1,X2,X3] :
( s_e(X2,X3,X0,X1)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_2) ).
fof(f11,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X0,X1,X4,X5)
| ~ s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_3) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( s_e(X1,X0,X2,X3)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_4) ).
fof(f13,axiom,
! [X0,X1,X2,X3] :
( s_e(X0,X1,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_5) ).
fof(f14,axiom,
! [X0,X1] : s_e(X0,X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_8) ).
fof(f15,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X1,X3,X4)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_11) ).
fof(f16,axiom,
! [X0,X1,X2,X3,X4] :
( X2 = ext(X0,X1,X3,X4)
| ~ s_e(X1,X2,X3,X4)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_12) ).
fof(f17,axiom,
! [X0,X1,X2] :
( X0 = X1
| ~ s_e(X0,X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_13) ).
fof(f18,axiom,
! [X0,X1,X2,X3] :
( s_e(X1,X0,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_14) ).
fof(f19,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X3,X4)
| ~ s_e(X0,X1,X4,X5)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_15) ).
fof(f20,axiom,
! [X0,X1] : s_t(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_1) ).
fof(f21,axiom,
! [X0,X1,X2] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_2) ).
fof(f22,axiom,
! [X0,X1] : s_t(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_3) ).
fof(f23,axiom,
! [X0,X1,X2] :
( X0 = X1
| ~ s_t(X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_4) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X1,X3)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_5a) ).
fof(f25,axiom,
! [X0,X1,X2,X3] :
( s_t(X1,X2,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_6a) ).
fof(f26,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X2,X3)
| X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_7a) ).
fof(f27,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X3,X2)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_5b) ).
fof(f28,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X1,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_6b) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X1,X3)
| X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_7b) ).
fof(f30,axiom,
alpha != beta,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_13a) ).
fof(f31,axiom,
beta != gamma,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_13b) ).
fof(f32,axiom,
alpha != gamma,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_13c) ).
fof(f34,axiom,
! [X0,X1] : X0 != ext(X1,X0,alpha,gamma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_14b) ).
fof(f35,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( s_t(X1,crossbar(X0,X1,X2,X3,X4,X5),X4)
| ~ s_t(X0,X5,X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) )
& ( s_t(X5,crossbar(X0,X1,X2,X3,X4,X5),X2)
| ~ s_t(X0,X5,X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_17) ).
fof(f36,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( s_e(X1,X3,X5,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_2) ).
fof(f37,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X0,X1,X3,X4)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X2,X3,X5)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_3) ).
fof(f38,axiom,
! [X0,X1,X2,X3,X4] :
( ( s_e3(X0,X1,X2,X3,insert(X0,X1,X3,X4),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) )
& ( s_t(X3,insert(X0,X1,X3,X4),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_5) ).
fof(f39,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_t(X3,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_6) ).
fof(f40,axiom,
! [X0,X1,X2] :
( s_col(X1,X2,X0)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_11a) ).
fof(f41,axiom,
! [X0,X1,X2] :
( s_col(X2,X0,X1)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_11b) ).
fof(f42,axiom,
! [X0,X1,X2] :
( s_col(X2,X1,X0)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_11c) ).
fof(f43,axiom,
! [X0,X1,X2] :
( s_col(X1,X0,X2)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_11d) ).
fof(f44,axiom,
! [X0,X1,X2] :
( s_col(X0,X2,X1)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_11e) ).
fof(f45,axiom,
! [X0,X1] : s_col(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_12) ).
fof(f46,axiom,
! [X0,X1] : s_col(X0,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_12b) ).
fof(f47,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_col(X3,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_13) ).
fof(f48,axiom,
! [X0,X1,X2,X3,X4] :
( s_e3(X0,X1,X2,X3,X4,insert5(X0,X1,X2,X3,X4))
| ~ s_e(X0,X1,X3,X4)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_14) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( s_e(X2,X3,X6,X7)
| X0 = X1
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_16) ).
fof(f50,axiom,
! [X0,X1,X2,X3,X4] :
( s_e(X2,X3,X2,X4)
| ~ s_e(X1,X3,X1,X4)
| ~ s_e(X0,X3,X0,X4)
| ~ s_col(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_17) ).
fof(f51,axiom,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ s_e(X1,X2,X1,X3)
| ~ s_e(X0,X2,X0,X3)
| ~ s_col(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_18) ).
fof(f52,axiom,
! [X0,X1,X2,X3] :
( X1 = X3
| ~ s_e(X2,X1,X2,X3)
| ~ s_e(X0,X1,X0,X3)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_19) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X3,X2)
| s_t(X0,X2,X3)
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_1) ).
fof(f54,axiom,
! [X0,X1,X2,X3] :
( s_t(X1,X3,X2)
| s_t(X1,X2,X3)
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_2) ).
fof(f55,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X3,X1)
| s_t(X0,X1,X3)
| ~ s_t(X0,X3,X2)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_3) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( ins(X2,X3,X0,X1) = ext(X0,X1,insert(X0,X1,X2,X3),X3)
| ~ le(X0,X1,X2,X3) )
& ( s_e(X0,ins(X2,X3,X0,X1),X2,X3)
| ~ le(X0,X1,X2,X3) )
& ( s_t(X0,X1,ins(X2,X3,X0,X1))
| ~ le(X0,X1,X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_5a) ).
fof(f57,axiom,
! [X0,X1,X2,X3,X4] :
( ~ s_e(X0,X4,X2,X3)
| ~ s_t(X0,X1,X4)
| le(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_5b) ).
fof(f58,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( le(X4,X5,X6,X7)
| ~ s_e(X2,X3,X6,X7)
| ~ s_e(X0,X1,X4,X5)
| ~ le(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_6) ).
fof(f59,axiom,
! [X0,X1] : le(X0,X1,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_7) ).
fof(f60,axiom,
! [X0,X1,X2,X3,X4,X5] :
( le(X0,X1,X4,X5)
| ~ le(X2,X3,X4,X5)
| ~ le(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_8) ).
fof(f61,axiom,
! [X0,X1,X2,X3] :
( s_e(X0,X1,X2,X3)
| ~ le(X2,X3,X0,X1)
| ~ le(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_9) ).
fof(f62,axiom,
! [X0,X1,X2,X3] :
( le(X2,X3,X0,X1)
| le(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_10) ).
fof(f63,axiom,
! [X0,X1,X2] : le(X0,X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_11) ).
fof(f64,axiom,
! [X0,X1,X2] :
( le(X0,X1,X0,X2)
| ~ s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_12a1) ).
fof(f65,axiom,
! [X0,X1,X2] :
( le(X1,X2,X0,X2)
| ~ s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_12a2) ).
fof(f66,axiom,
! [X0,X1,X2] :
( X2 = X1
| ~ s_e(X0,X2,X0,X1)
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aNarbouxLemma1) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ~ le(X1,X2,X0,X2)
| ~ le(X0,X1,X0,X2)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz5_12b) ).
fof(f69,axiom,
! [X0,X1,X2,X3] :
( ~ sameside(X0,X1,X2)
| s_t(X2,X1,X3)
| ~ s_t(X0,X1,X3)
| X3 = X1
| X2 = X1
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_2b) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( s_t(X2,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) )
& ( s_t(X0,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) )
& ( c63(X0,X1,X2) != X1
| ~ sameside(X0,X1,X2) )
& ( X2 != X1
| ~ sameside(X0,X1,X2) )
& ( X0 != X1
| ~ sameside(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_3a) ).
fof(f71,axiom,
! [X0,X1,X2,X3] :
( ~ s_t(X2,X1,X3)
| ~ s_t(X0,X1,X3)
| X3 = X1
| X2 = X1
| X0 = X1
| sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_3b) ).
fof(f72,axiom,
! [X0,X1,X2] :
( ( ~ s_t(X0,X1,X2)
| ~ sameside(X0,X1,X2) )
& ( s_col(X0,X1,X2)
| ~ sameside(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_4a) ).
fof(f73,axiom,
! [X0,X1,X2] :
( s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2)
| sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_4b) ).
fof(f74,axiom,
! [X0,X1] :
( sameside(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_5) ).
fof(f75,axiom,
! [X0,X1,X2] :
( sameside(X2,X1,X0)
| ~ sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_6) ).
fof(f76,axiom,
! [X0,X1,X2,X3] :
( sameside(X0,X1,X3)
| ~ sameside(X2,X1,X3)
| ~ sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_7) ).
fof(f77,axiom,
! [X0,X1,X2,X3] :
( ( s_e(X1,insert(X2,X3,X1,X0),X2,X3)
| X2 = X3
| X0 = X1 )
& ( sameside(insert(X2,X3,X1,X0),X1,X0)
| X2 = X3
| X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_11a) ).
fof(f78,axiom,
! [X0,X1,X2,X3,X4,X5] :
( X4 = X5
| ~ s_e(X1,X5,X2,X3)
| ~ sameside(X5,X1,X0)
| ~ s_e(X1,X4,X2,X3)
| ~ sameside(X4,X1,X0)
| X2 = X3
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_11b) ).
fof(f79,axiom,
! [X0,X1,X2] :
( s_t(X1,X0,X2)
| ~ le(X1,X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_13a) ).
fof(f80,axiom,
! [X0,X1,X2] :
( ~ s_t(X1,X0,X2)
| le(X1,X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_13b) ).
fof(f81,axiom,
! [X0,X1,X2,X3] :
( sameside(X3,X0,X2)
| sameside(X3,X0,X1)
| X3 = X0
| ~ s_col(X3,X0,X1)
| ~ s_t(X1,X0,X2)
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_15a) ).
fof(f83,axiom,
! [X0,X1,X2,X3] :
( s_col(X3,X0,X1)
| ~ sameside(X3,X0,X2)
| ~ s_t(X1,X0,X2)
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_15c) ).
fof(f85,axiom,
! [X0,X1,X2,X3] :
( s_t(X2,X3,X1)
| s_t(X3,X2,X1)
| ~ s_t(X3,X0,X1)
| ~ s_t(X2,X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_16a) ).
fof(f86,axiom,
! [X0,X1,X2,X3] :
( s_col(X0,X2,X3)
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| X2 = X0
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_16b) ).
fof(f89,axiom,
! [X0,X1,X2,X3,X4] :
( s_col(X0,X1,X4)
| ~ s_col(X2,X3,X4)
| ~ s_col(X2,X3,X1)
| ~ s_col(X2,X3,X0)
| X2 = X3
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_18) ).
fof(f90,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( s_col(X2,X3,X6)
| ~ s_col(X0,X1,X6)
| X4 = X5
| ~ s_col(X2,X3,X5)
| ~ s_col(X0,X1,X5)
| ~ s_col(X2,X3,X4)
| ~ s_col(X0,X1,X4)
| X2 = X3
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_21) ).
fof(f91,axiom,
! [X0,X1] :
( ~ s_col(X0,X1,pointOffLine(X0,X1))
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_25) ).
fof(f92,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X1,X0,X4,X3)
| ~ sameside(X3,X4,X5)
| ~ sameside(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_28) ).
fof(f93,axiom,
! [X0,X1,X2] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_2) ).
fof(f94,axiom,
! [X0,X1] :
( X1 = X0
| ~ s_m(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_3a) ).
fof(f95,axiom,
! [X0,X1] :
( X1 != X0
| s_m(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_3b) ).
fof(f96,axiom,
! [X0,X1] : s_m(X0,X1,s(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_4a) ).
fof(f97,axiom,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ s_m(X0,X1,X3)
| ~ s_m(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_4b) ).
fof(f98,axiom,
! [X0,X1,X2] :
( X2 = s(X1,X0)
| ~ s_m(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_6) ).
fof(f99,axiom,
! [X0,X1] : s(X0,s(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_7) ).
fof(f101,axiom,
! [X0,X1,X2] :
( X1 = X2
| s(X0,X1) != s(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_9) ).
fof(f102,axiom,
! [X0,X1] :
( X1 = X0
| s(X0,X1) != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_10a) ).
fof(f103,axiom,
! [X0,X1] :
( X1 != X0
| s(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_10b) ).
fof(f104,axiom,
! [X0,X1,X2] : s_e(X0,X1,s(X2,X0),s(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_13) ).
fof(f105,axiom,
! [X0,X1,X2,X3] :
( s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| ~ s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_15a) ).
fof(f106,conjecture,
! [X0,X1,X2,X3] :
( ~ s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| s_t(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_15b) ).
fof(f107,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ~ s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| s_t(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f106]) ).
fof(f108,axiom,
! [X0,X1,X2,X3] : insert(X0,X1,X2,X3) = ext(ext(X3,X2,alpha,gamma),X2,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_insert) ).
fof(f110,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ s_e(X2,X3,X6,X7)
| ~ s_e(X0,X3,X4,X7)
| ~ s_e(X1,X2,X5,X6)
| ~ s_e(X0,X2,X4,X6)
| ~ s_t(X4,X5,X6)
| ~ s_t(X0,X1,X2) )
& ( s_e(X2,X3,X6,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_e(X0,X3,X4,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_e(X1,X2,X5,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_e(X0,X2,X4,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_t(X4,X5,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_t(X0,X1,X2)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn4_1) ).
fof(f111,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X2,X3,X5)
| ~ s_e(X0,X1,X3,X4) )
& ( s_e(X1,X2,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) )
& ( s_e(X0,X2,X3,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) )
& ( s_e(X0,X1,X3,X4)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn4_4) ).
fof(f112,axiom,
! [X0,X1,X2] :
( ( ~ s_t(X2,X0,X1)
| s_col(X0,X1,X2) )
& ( ~ s_t(X1,X2,X0)
| s_col(X0,X1,X2) )
& ( ~ s_t(X0,X1,X2)
| s_col(X0,X1,X2) )
& ( s_t(X2,X0,X1)
| s_t(X1,X2,X0)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn4_10) ).
fof(f113,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( s_fs(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ s_e(X1,X3,X5,X7)
| ~ s_e(X0,X3,X4,X7)
| ~ s_e3(X0,X1,X2,X4,X5,X6)
| ~ s_col(X0,X1,X2) )
& ( s_e(X1,X3,X5,X7)
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_e(X0,X3,X4,X7)
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_e3(X0,X1,X2,X4,X5,X6)
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) )
& ( s_col(X0,X1,X2)
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn4_15) ).
fof(f114,axiom,
! [X0,X1,X2,X3,X4] :
( ( le(X0,X1,X2,X3)
| ~ s_e(X0,X1,X2,X4)
| ~ s_t(X2,X4,X3) )
& ( s_e(X0,X1,X2,insert(X0,X1,X2,X3))
| ~ le(X0,X1,X2,X3) )
& ( s_t(X2,insert(X0,X1,X2,X3),X3)
| ~ le(X0,X1,X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn5_4) ).
fof(f115,axiom,
! [X0,X1,X2] :
( ( sameside(X0,X1,X2)
| X2 = X1
| X0 = X1
| ~ s_t(X1,X2,X0) )
& ( sameside(X0,X1,X2)
| xb = X1
| X0 = X1
| ~ s_t(X1,X0,X2) )
& ( s_t(X1,X2,X0)
| s_t(X1,X0,X2)
| ~ sameside(X0,X1,X2) )
& ( X2 != X1
| ~ sameside(X0,X1,X2) )
& ( X0 != X1
| ~ sameside(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn6_1) ).
fof(f116,axiom,
! [X0,X1,X2] :
( ( s_m(X0,X1,X2)
| ~ s_e(X1,X0,X1,X2)
| ~ s_t(X0,X1,X2) )
& ( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) )
& ( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn7_1) ).
fof(f118,plain,
? [X0,X1,X2,X3] :
( s_t(s(X3,X0),s(X3,X1),s(X3,X2))
& ~ s_t(X0,X1,X2) ),
inference(ennf_transformation,[],[f107]) ).
fof(f119,plain,
( s_t(s(sK3,sK0),s(sK3,sK1),s(sK3,sK2))
& ~ s_t(sK0,sK1,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f118]) ).
fof(f120,plain,
! [X0,X1] : s_e(X0,X1,X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f121,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f123,plain,
! [X2,X3,X0,X1] : s_e(X1,ext(X0,X1,X2,X3),X2,X3),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
! [X2,X3,X0,X1] : s_t(X0,X1,ext(X0,X1,X2,X3)),
inference(cnf_transformation,[],[f4]) ).
fof(f125,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X4,X6,X5,X7)
| X0 = X1
| ~ s_t(X2,X3,X5)
| ~ s_t(X0,X1,X4)
| ~ s_e(X1,X6,X3,X7)
| ~ s_e(X0,X6,X2,X7)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
! [X0,X1] :
( X0 = X1
| ~ s_t(X0,X1,X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f127,plain,
! [X2,X3,X0,X1,X4] :
( s_t(X4,ip(X0,X1,X2,X3,X4),X0)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f7]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4] :
( s_t(X1,ip(X0,X1,X2,X3,X4),X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f7]) ).
fof(f129,plain,
~ s_t(gamma,alpha,beta),
inference(cnf_transformation,[],[f8]) ).
fof(f130,plain,
~ s_t(beta,gamma,alpha),
inference(cnf_transformation,[],[f8]) ).
fof(f131,plain,
~ s_t(alpha,beta,gamma),
inference(cnf_transformation,[],[f8]) ).
fof(f132,plain,
! [X0,X1] : s_e(X0,X1,X0,X1),
inference(cnf_transformation,[],[f9]) ).
fof(f133,plain,
! [X2,X3,X0,X1] :
( s_e(X2,X3,X0,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f134,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X1,X4,X5)
| ~ s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f11]) ).
fof(f135,plain,
! [X2,X3,X0,X1] :
( s_e(X1,X0,X2,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f12]) ).
fof(f136,plain,
! [X2,X3,X0,X1] :
( s_e(X0,X1,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f13]) ).
fof(f137,plain,
! [X0,X1] : s_e(X0,X0,X1,X1),
inference(cnf_transformation,[],[f14]) ).
fof(f138,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X1,X3,X4)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f15]) ).
fof(f139,plain,
! [X2,X3,X0,X1,X4] :
( ext(X0,X1,X3,X4) = X2
| ~ s_e(X1,X2,X3,X4)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f16]) ).
fof(f140,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ s_e(X0,X1,X2,X2) ),
inference(cnf_transformation,[],[f17]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( s_e(X1,X0,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f18]) ).
fof(f142,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X3,X4)
| ~ s_e(X0,X1,X4,X5)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f19]) ).
fof(f143,plain,
! [X0,X1] : s_t(X0,X1,X1),
inference(cnf_transformation,[],[f20]) ).
fof(f144,plain,
! [X2,X0,X1] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f145,plain,
! [X0,X1] : s_t(X0,X0,X1),
inference(cnf_transformation,[],[f22]) ).
fof(f146,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ s_t(X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f23]) ).
fof(f147,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X1,X3)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f24]) ).
fof(f148,plain,
! [X2,X3,X0,X1] :
( s_t(X1,X2,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f149,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X2,X3)
| X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f150,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X3,X2)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f151,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X1,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f152,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X1,X3)
| X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
fof(f153,plain,
alpha != beta,
inference(cnf_transformation,[],[f30]) ).
fof(f154,plain,
beta != gamma,
inference(cnf_transformation,[],[f31]) ).
fof(f155,plain,
alpha != gamma,
inference(cnf_transformation,[],[f32]) ).
fof(f157,plain,
! [X0,X1] : ext(X1,X0,alpha,gamma) != X0,
inference(cnf_transformation,[],[f34]) ).
fof(f158,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X1,crossbar(X0,X1,X2,X3,X4,X5),X4)
| ~ s_t(X0,X5,X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f159,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X5,crossbar(X0,X1,X2,X3,X4,X5),X2)
| ~ s_t(X0,X5,X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f160,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X1,X3,X5,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f36]) ).
fof(f161,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X1,X3,X4)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X2,X3,X5)
| ~ s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f162,plain,
! [X2,X3,X0,X1,X4] :
( s_e3(X0,X1,X2,X3,insert(X0,X1,X3,X4),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f163,plain,
! [X2,X3,X0,X1,X4] :
( s_t(X3,insert(X0,X1,X3,X4),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f164,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X3,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f165,plain,
! [X2,X0,X1] :
( s_col(X1,X2,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f166,plain,
! [X2,X0,X1] :
( s_col(X2,X0,X1)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f41]) ).
fof(f167,plain,
! [X2,X0,X1] :
( s_col(X2,X1,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f168,plain,
! [X2,X0,X1] :
( s_col(X1,X0,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f169,plain,
! [X2,X0,X1] :
( s_col(X0,X2,X1)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f170,plain,
! [X0,X1] : s_col(X0,X0,X1),
inference(cnf_transformation,[],[f45]) ).
fof(f171,plain,
! [X0,X1] : s_col(X0,X1,X0),
inference(cnf_transformation,[],[f46]) ).
fof(f172,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_col(X3,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f47]) ).
fof(f173,plain,
! [X2,X3,X0,X1,X4] :
( s_e3(X0,X1,X2,X3,X4,insert5(X0,X1,X2,X3,X4))
| ~ s_e(X0,X1,X3,X4)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f48]) ).
fof(f174,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X2,X3,X6,X7)
| X0 = X1
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f49]) ).
fof(f175,plain,
! [X2,X3,X0,X1,X4] :
( s_e(X2,X3,X2,X4)
| ~ s_e(X1,X3,X1,X4)
| ~ s_e(X0,X3,X0,X4)
| ~ s_col(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f50]) ).
fof(f176,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ s_e(X1,X2,X1,X3)
| ~ s_e(X0,X2,X0,X3)
| ~ s_col(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f177,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| ~ s_e(X2,X1,X2,X3)
| ~ s_e(X0,X1,X0,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f52]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X3,X2)
| s_t(X0,X2,X3)
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f53]) ).
fof(f179,plain,
! [X2,X3,X0,X1] :
( s_t(X1,X3,X2)
| s_t(X1,X2,X3)
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f54]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X3,X1)
| s_t(X0,X1,X3)
| ~ s_t(X0,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f181,plain,
! [X2,X3,X0,X1] :
( ins(X2,X3,X0,X1) = ext(X0,X1,insert(X0,X1,X2,X3),X3)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f56]) ).
fof(f182,plain,
! [X2,X3,X0,X1] :
( s_e(X0,ins(X2,X3,X0,X1),X2,X3)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f56]) ).
fof(f183,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X1,ins(X2,X3,X0,X1))
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f56]) ).
fof(f184,plain,
! [X2,X3,X0,X1,X4] :
( ~ s_e(X0,X4,X2,X3)
| ~ s_t(X0,X1,X4)
| le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f57]) ).
fof(f185,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( le(X4,X5,X6,X7)
| ~ s_e(X2,X3,X6,X7)
| ~ s_e(X0,X1,X4,X5)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f58]) ).
fof(f186,plain,
! [X0,X1] : le(X0,X1,X0,X1),
inference(cnf_transformation,[],[f59]) ).
fof(f187,plain,
! [X2,X3,X0,X1,X4,X5] :
( le(X0,X1,X4,X5)
| ~ le(X2,X3,X4,X5)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f60]) ).
fof(f188,plain,
! [X2,X3,X0,X1] :
( s_e(X0,X1,X2,X3)
| ~ le(X2,X3,X0,X1)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f61]) ).
fof(f189,plain,
! [X2,X3,X0,X1] :
( le(X2,X3,X0,X1)
| le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f62]) ).
fof(f190,plain,
! [X2,X0,X1] : le(X0,X0,X1,X2),
inference(cnf_transformation,[],[f63]) ).
fof(f191,plain,
! [X2,X0,X1] :
( le(X0,X1,X0,X2)
| ~ s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f64]) ).
fof(f192,plain,
! [X2,X0,X1] :
( le(X1,X2,X0,X2)
| ~ s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f193,plain,
! [X2,X0,X1] :
( X1 = X2
| ~ s_e(X0,X2,X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ le(X1,X2,X0,X2)
| ~ le(X0,X1,X0,X2)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f67]) ).
fof(f196,plain,
! [X2,X3,X0,X1] :
( ~ sameside(X0,X1,X2)
| s_t(X2,X1,X3)
| ~ s_t(X0,X1,X3)
| X1 = X3
| X1 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f69]) ).
fof(f197,plain,
! [X2,X0,X1] :
( s_t(X2,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f198,plain,
! [X2,X0,X1] :
( s_t(X0,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f199,plain,
! [X2,X0,X1] :
( c63(X0,X1,X2) != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f70]) ).
fof(f202,plain,
! [X2,X3,X0,X1] :
( ~ s_t(X2,X1,X3)
| ~ s_t(X0,X1,X3)
| X1 = X3
| X1 = X2
| X0 = X1
| sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f71]) ).
fof(f203,plain,
! [X2,X0,X1] :
( ~ s_t(X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f72]) ).
fof(f204,plain,
! [X2,X0,X1] :
( s_col(X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f72]) ).
fof(f205,plain,
! [X2,X0,X1] :
( s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2)
| sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f206,plain,
! [X0,X1] :
( sameside(X0,X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f74]) ).
fof(f207,plain,
! [X2,X0,X1] :
( sameside(X2,X1,X0)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f75]) ).
fof(f208,plain,
! [X2,X3,X0,X1] :
( sameside(X0,X1,X3)
| ~ sameside(X2,X1,X3)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f76]) ).
fof(f210,plain,
! [X2,X3,X0,X1] :
( sameside(insert(X2,X3,X1,X0),X1,X0)
| X2 = X3
| X0 = X1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f211,plain,
! [X2,X3,X0,X1,X4,X5] :
( X4 = X5
| ~ s_e(X1,X5,X2,X3)
| ~ sameside(X5,X1,X0)
| ~ s_e(X1,X4,X2,X3)
| ~ sameside(X4,X1,X0)
| X2 = X3
| X0 = X1 ),
inference(cnf_transformation,[],[f78]) ).
fof(f212,plain,
! [X2,X0,X1] :
( s_t(X1,X0,X2)
| ~ le(X1,X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f79]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ s_t(X1,X0,X2)
| le(X1,X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f214,plain,
! [X2,X3,X0,X1] :
( sameside(X3,X0,X2)
| sameside(X3,X0,X1)
| X0 = X3
| ~ s_col(X3,X0,X1)
| ~ s_t(X1,X0,X2)
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f81]) ).
fof(f216,plain,
! [X2,X3,X0,X1] :
( s_col(X3,X0,X1)
| ~ sameside(X3,X0,X2)
| ~ s_t(X1,X0,X2)
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f218,plain,
! [X2,X3,X0,X1] :
( s_t(X2,X3,X1)
| s_t(X3,X2,X1)
| ~ s_t(X3,X0,X1)
| ~ s_t(X2,X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f85]) ).
fof(f219,plain,
! [X2,X3,X0,X1] :
( s_col(X0,X2,X3)
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f86]) ).
fof(f222,plain,
! [X2,X3,X0,X1,X4] :
( s_col(X0,X1,X4)
| ~ s_col(X2,X3,X4)
| ~ s_col(X2,X3,X1)
| ~ s_col(X2,X3,X0)
| X2 = X3
| X0 = X1 ),
inference(cnf_transformation,[],[f89]) ).
fof(f223,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( s_col(X2,X3,X6)
| ~ s_col(X0,X1,X6)
| X4 = X5
| ~ s_col(X2,X3,X5)
| ~ s_col(X0,X1,X5)
| ~ s_col(X2,X3,X4)
| ~ s_col(X0,X1,X4)
| X2 = X3
| X0 = X1 ),
inference(cnf_transformation,[],[f90]) ).
fof(f224,plain,
! [X0,X1] :
( ~ s_col(X0,X1,pointOffLine(X0,X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f91]) ).
fof(f225,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X1,X0,X4,X3)
| ~ sameside(X3,X4,X5)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f92]) ).
fof(f226,plain,
! [X2,X0,X1] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f227,plain,
! [X0,X1] :
( X0 = X1
| ~ s_m(X0,X1,X0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f228,plain,
! [X0,X1] :
( X0 != X1
| s_m(X0,X1,X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f229,plain,
! [X0,X1] : s_m(X0,X1,s(X1,X0)),
inference(cnf_transformation,[],[f96]) ).
fof(f230,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ s_m(X0,X1,X3)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f231,plain,
! [X2,X0,X1] :
( s(X1,X0) = X2
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f98]) ).
fof(f232,plain,
! [X0,X1] : s(X0,s(X0,X1)) = X1,
inference(cnf_transformation,[],[f99]) ).
fof(f234,plain,
! [X2,X0,X1] :
( X1 = X2
| s(X0,X1) != s(X0,X2) ),
inference(cnf_transformation,[],[f101]) ).
fof(f235,plain,
! [X0,X1] :
( X0 = X1
| s(X0,X1) != X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f236,plain,
! [X0,X1] :
( X0 != X1
| s(X0,X1) = X1 ),
inference(cnf_transformation,[],[f103]) ).
fof(f237,plain,
! [X2,X0,X1] : s_e(X0,X1,s(X2,X0),s(X2,X1)),
inference(cnf_transformation,[],[f104]) ).
fof(f238,plain,
! [X2,X3,X0,X1] :
( s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f239,plain,
s_t(s(sK3,sK0),s(sK3,sK1),s(sK3,sK2)),
inference(cnf_transformation,[],[f119]) ).
fof(f240,plain,
~ s_t(sK0,sK1,sK2),
inference(cnf_transformation,[],[f119]) ).
fof(f241,plain,
! [X2,X3,X0,X1] : insert(X0,X1,X2,X3) = ext(ext(X3,X2,alpha,gamma),X2,X0,X1),
inference(cnf_transformation,[],[f108]) ).
fof(f249,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ s_e(X2,X3,X6,X7)
| ~ s_e(X0,X3,X4,X7)
| ~ s_e(X1,X2,X5,X6)
| ~ s_e(X0,X2,X4,X6)
| ~ s_t(X4,X5,X6)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f256,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e3(X0,X1,X2,X3,X4,X5)
| ~ s_e(X1,X2,X4,X5)
| ~ s_e(X0,X2,X3,X5)
| ~ s_e(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f111]) ).
fof(f257,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X1,X2,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f258,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X2,X3,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f259,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X1,X3,X4)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f260,plain,
! [X2,X0,X1] :
( ~ s_t(X2,X0,X1)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f112]) ).
fof(f261,plain,
! [X2,X0,X1] :
( ~ s_t(X1,X2,X0)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f112]) ).
fof(f262,plain,
! [X2,X0,X1] :
( ~ s_t(X0,X1,X2)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f112]) ).
fof(f263,plain,
! [X2,X0,X1] :
( s_t(X2,X0,X1)
| s_t(X1,X2,X0)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f112]) ).
fof(f264,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_fs(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ s_e(X1,X3,X5,X7)
| ~ s_e(X0,X3,X4,X7)
| ~ s_e3(X0,X1,X2,X4,X5,X6)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f113]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X4] :
( le(X0,X1,X2,X3)
| ~ s_e(X0,X1,X2,X4)
| ~ s_t(X2,X4,X3) ),
inference(cnf_transformation,[],[f114]) ).
fof(f270,plain,
! [X2,X3,X0,X1] :
( s_e(X0,X1,X2,insert(X0,X1,X2,X3))
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f114]) ).
fof(f271,plain,
! [X2,X3,X0,X1] :
( s_t(X2,insert(X0,X1,X2,X3),X3)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f114]) ).
fof(f272,plain,
! [X2,X0,X1] :
( sameside(X0,X1,X2)
| X1 = X2
| X0 = X1
| ~ s_t(X1,X2,X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f273,plain,
! [X2,X0,X1] :
( sameside(X0,X1,X2)
| xb = X1
| X0 = X1
| ~ s_t(X1,X0,X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f274,plain,
! [X2,X0,X1] :
( s_t(X1,X2,X0)
| s_t(X1,X0,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f275,plain,
! [X2,X0,X1] :
( X1 != X2
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f276,plain,
! [X2,X0,X1] :
( X0 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f277,plain,
! [X2,X0,X1] :
( s_m(X0,X1,X2)
| ~ s_e(X1,X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f278,plain,
! [X2,X0,X1] :
( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f279,plain,
! [X2,X0,X1] :
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( s_t(X3,ext(ext(X4,X3,alpha,gamma),X3,X0,X1),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(definition_unfolding,[],[f163,f241]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X4] :
( s_e3(X0,X1,X2,X3,ext(ext(X4,X3,alpha,gamma),X3,X0,X1),X4)
| ~ s_e(X0,X2,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(definition_unfolding,[],[f162,f241]) ).
fof(f289,plain,
! [X2,X3,X0,X1] :
( ins(X2,X3,X0,X1) = ext(X0,X1,ext(ext(X3,X2,alpha,gamma),X2,X0,X1),X3)
| ~ le(X0,X1,X2,X3) ),
inference(definition_unfolding,[],[f181,f241]) ).
fof(f290,plain,
! [X2,X3,X0,X1] :
( sameside(ext(ext(X0,X1,alpha,gamma),X1,X2,X3),X1,X0)
| X2 = X3
| X0 = X1 ),
inference(definition_unfolding,[],[f210,f241]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( s_t(X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X1),X3)
| ~ le(X0,X1,X2,X3) ),
inference(definition_unfolding,[],[f271,f241]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( s_e(X0,X1,X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X1))
| ~ le(X0,X1,X2,X3) ),
inference(definition_unfolding,[],[f270,f241]) ).
fof(f297,plain,
! [X1] : s_m(X1,X1,X1),
inference(equality_resolution,[],[f228]) ).
fof(f299,plain,
! [X1] : s(X1,X1) = X1,
inference(equality_resolution,[],[f236]) ).
fof(f300,plain,
! [X2,X1] : ~ sameside(X1,X1,X2),
inference(equality_resolution,[],[f276]) ).
fof(f301,plain,
! [X2,X0] : ~ sameside(X0,X2,X2),
inference(equality_resolution,[],[f275]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,X1,X0),
inference(cnf_transformation,[],[f120]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_t(X0,X1,ext(X0,X1,X2,X3)),
inference(cnf_transformation,[],[f124]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_e(X0,ext(X1,X0,X2,X3),X2,X3),
inference(cnf_transformation,[],[f123]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_e(X6,X4,X7,X5)
| ( X0 = X1 )
| ~ s_t(X2,X3,X7)
| ~ s_t(X0,X1,X6)
| ~ s_e(X1,X6,X3,X7)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X4,X2,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_t(X0,X1,X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_t(X1,ip(X0,X1,X2,X3,X4),X3)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_t(X4,ip(X0,X1,X2,X3,X4),X0)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_58,plain,
~ s_t(alpha,beta,gamma),
inference(cnf_transformation,[],[f131]) ).
tcf(c_59,plain,
~ s_t(beta,gamma,alpha),
inference(cnf_transformation,[],[f130]) ).
tcf(c_60,plain,
~ s_t(gamma,alpha,beta),
inference(cnf_transformation,[],[f129]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,X0,X1),
inference(cnf_transformation,[],[f132]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X2,X3,X0,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X1,X4,X5)
| ~ s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X1,X0,X2,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,X1,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : s_e(X0,X0,X1,X1),
inference(cnf_transformation,[],[f137]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X4,X2,X5)
| ~ s_t(X2,X3,X5)
| ~ s_t(X0,X1,X4)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X0 = X4 )
| ( ext(X4,X0,X2,X3) = X1 )
| ~ s_t(X4,X0,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ~ s_e(X0,X1,X2,X2) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X1,X0,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X4,X5,X3)
| ~ s_t(X5,X2,X3)
| ~ s_t(X0,X1,X4)
| ~ s_e(X1,X4,X5,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] : s_t(X0,X1,X1),
inference(cnf_transformation,[],[f143]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] : s_t(X0,X0,X1),
inference(cnf_transformation,[],[f145]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ~ s_t(X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X1,X3)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X1,X2,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X2,X3)
| ( X1 = X2 )
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X3,X2)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X1,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X1,X3)
| ( X1 = X2 )
| ~ s_t(X1,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_82,plain,
alpha != beta,
inference(cnf_transformation,[],[f153]) ).
tcf(c_83,plain,
beta != gamma,
inference(cnf_transformation,[],[f154]) ).
tcf(c_84,plain,
alpha != gamma,
inference(cnf_transformation,[],[f155]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] : ext(X0,X1,alpha,gamma) != X1,
inference(cnf_transformation,[],[f157]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_t(X3,crossbar(X0,X1,X2,X4,X5,X3),X2)
| ~ s_t(X4,X5,X2)
| ~ s_t(X0,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_t(X1,crossbar(X0,X1,X2,X4,X5,X3),X5)
| ~ s_t(X4,X5,X2)
| ~ s_t(X0,X3,X4)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_e(X1,X3,X5,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X4,X2,X5)
| ~ s_t(X2,X5,X3)
| ~ s_t(X0,X4,X1)
| ~ s_e(X4,X1,X5,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_t(X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X4),X3)
| ~ s_t(X0,X4,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_e3(X0,X4,X1,X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X4),X3)
| ~ s_t(X0,X4,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_t(X3,X4,X5)
| ~ s_t(X0,X1,X2)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,X2,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X2,X0,X1)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X2,X1,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,X0,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X2,X1)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] : s_col(X0,X0,X1),
inference(cnf_transformation,[],[f170]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,X0),
inference(cnf_transformation,[],[f171]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_col(X3,X4,X5)
| ~ s_col(X0,X1,X2)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_e3(X0,X1,X4,X2,X3,insert5(X0,X1,X4,X2,X3))
| ~ s_col(X0,X1,X4)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_e(X2,X3,X6,X7)
| ( X0 = X1 )
| ~ s_fs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_e(X4,X1,X4,X2)
| ( X0 = X3 )
| ~ s_col(X0,X3,X4)
| ~ s_e(X3,X1,X3,X2)
| ~ s_e(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X2 )
| ( X0 = X3 )
| ~ s_col(X0,X3,X1)
| ~ s_e(X3,X1,X3,X2)
| ~ s_e(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X2 )
| ~ s_t(X0,X1,X3)
| ~ s_e(X3,X1,X3,X2)
| ~ s_e(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X3,X2)
| s_t(X0,X2,X3)
| ( X0 = X1 )
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X1,X3,X2)
| s_t(X1,X2,X3)
| ( X0 = X1 )
| ~ s_t(X0,X1,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X3,X1)
| s_t(X0,X1,X3)
| ~ s_t(X0,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X0,X1,ins(X2,X3,X0,X1))
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,ins(X2,X3,X0,X1),X2,X3)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ext(X0,X1,ext(ext(X3,X2,alpha,gamma),X2,X0,X1),X3) = ins(X2,X3,X0,X1) )
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( le(X0,X4,X2,X3)
| ~ s_t(X0,X4,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( le(X2,X3,X6,X7)
| ~ le(X0,X1,X4,X5)
| ~ s_e(X4,X5,X6,X7)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] : le(X0,X1,X0,X1),
inference(cnf_transformation,[],[f186]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( le(X0,X1,X4,X5)
| ~ le(X2,X3,X4,X5)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,X1,X2,X3)
| ~ le(X2,X3,X0,X1)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( le(X2,X3,X0,X1)
| le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] : le(X0,X0,X1,X2),
inference(cnf_transformation,[],[f190]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,X2)
| ~ s_col(X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X1,X2,X0,X2)
| ~ s_col(X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ s_t(X0,X2,X1)
| ~ s_e(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2)
| ~ le(X1,X2,X0,X2)
| ~ le(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X3,X1,X2)
| ( X1 = X3 )
| ( X1 = X2 )
| ( X0 = X1 )
| ~ sameside(X0,X1,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sameside(X0,X1,X2)
| ( c63(X0,X1,X2) != X1 ) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sameside(X0,X1,X3)
| ( X1 = X3 )
| ( X1 = X2 )
| ( X0 = X1 )
| ~ s_t(X3,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sameside(X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i] :
( sameside(X0,X1,X2)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i] :
( sameside(X0,X1,X0)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i] :
( sameside(X2,X1,X0)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sameside(X0,X1,X3)
| ~ sameside(X2,X1,X3)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sameside(ext(ext(X0,X1,alpha,gamma),X1,X2,X3),X1,X0)
| ( X2 = X3 )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X2 = X3 )
| ( X1 = X4 )
| ( X0 = X5 )
| ~ sameside(X4,X0,X5)
| ~ sameside(X1,X0,X5)
| ~ s_e(X0,X4,X2,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ sameside(X1,X0,X2)
| ~ le(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,X2)
| ~ sameside(X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sameside(X3,X1,X2)
| sameside(X3,X1,X0)
| ( X1 = X3 )
| ( X1 = X2 )
| ( X0 = X1 )
| ~ s_col(X3,X1,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_col(X3,X1,X0)
| ( X1 = X2 )
| ( X0 = X1 )
| ~ sameside(X3,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X3,X0,X2)
| s_t(X0,X3,X2)
| ( X1 = X2 )
| ~ s_t(X3,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_col(X0,X2,X3)
| ( X0 = X2 )
| ( X0 = X1 )
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_col(X2,X3,X4)
| ( X2 = X3 )
| ( X0 = X1 )
| ~ s_col(X0,X1,X4)
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( s_col(X5,X6,X4)
| ( X5 = X6 )
| ( X2 = X3 )
| ( X0 = X1 )
| ~ s_col(X5,X6,X3)
| ~ s_col(X5,X6,X2)
| ~ s_col(X0,X1,X4)
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_col(X0,X1,pointOffLine(X0,X1)) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X1,X4,X3,X5)
| ~ sameside(X3,X2,X5)
| ~ sameside(X1,X0,X4)
| ~ s_e(X0,X4,X2,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_m(X0,X1,X0) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_157,plain,
! [X0: $i] : s_m(X0,X0,X0),
inference(cnf_transformation,[],[f297]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] : s_m(X0,X1,s(X1,X0)),
inference(cnf_transformation,[],[f229]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X2 = X3 )
| ~ s_m(X0,X1,X3)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X1,X0) = X2 )
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] : s(X0,s(X0,X1)) = X1,
inference(cnf_transformation,[],[f232]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( s(X0,X1) != s(X0,X2) ) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_165,plain,
! [X0: $i] : s(X0,X0) = X0,
inference(cnf_transformation,[],[f299]) ).
tcf(c_166,plain,
! [X0: $i,X1: $i,X2: $i] : s_e(X0,X1,s(X2,X0),s(X2,X1)),
inference(cnf_transformation,[],[f237]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_168,negated_conjecture,
~ s_t(sK0,sK1,sK2),
inference(cnf_transformation,[],[f240]) ).
tcf(c_169,negated_conjecture,
s_t(s(sK3,sK0),s(sK3,sK1),s(sK3,sK2)),
inference(cnf_transformation,[],[f239]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_ifs(X0,X6,X1,X4,X2,X7,X3,X5)
| ~ s_t(X2,X7,X3)
| ~ s_t(X0,X6,X1)
| ~ s_e(X6,X1,X7,X3)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X4,X2,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X1,X3,X4)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X0,X2,X3,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e(X1,X2,X4,X5)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_e3(X0,X1,X4,X2,X3,X5)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X4,X2,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,X0,X1)
| s_t(X1,X2,X0)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X2,X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,X2,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_fs(X0,X1,X2,X6,X3,X4,X5,X7)
| ~ s_col(X0,X1,X2)
| ~ s_e(X1,X6,X4,X7)
| ~ s_e(X0,X6,X3,X7)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X1),X3)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,X1,X2,ext(ext(X3,X2,alpha,gamma),X2,X0,X1))
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( le(X0,X1,X2,X4)
| ~ s_t(X2,X3,X4)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] : ~ sameside(X0,X0,X1),
inference(cnf_transformation,[],[f300]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] : ~ sameside(X0,X1,X1),
inference(cnf_transformation,[],[f301]) ).
tcf(c_202,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X1,X2,X0)
| s_t(X1,X0,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i,X2: $i] :
( sameside(X1,X0,X2)
| ( X0 = xb )
| ( X0 = X1 )
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( sameside(X2,X0,X1)
| ( X0 = X2 )
| ( X0 = X1 )
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_m(X1,X0,X2)
| ~ s_t(X1,X0,X2)
| ~ s_e(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_142,c_189,c_120]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X1,X2,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_121,c_189,c_121]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_120,c_259]) ).
tcf(c_1908,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
( s_e(X4,X6,X12,X14)
| ( X0 = X2 )
| ~ s_col(X1,X3,X5)
| ~ s_e(X3,X7,X11,X15)
| ~ s_e(X1,X7,X9,X15)
| ~ s_e3(X1,X3,X5,X9,X11,X13)
| ( X14 != X15 )
| ( X12 != X13 )
| ( X10 != X11 )
| ( X8 != X9 )
| ( X6 != X7 )
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_103,c_196]) ).
tcf(c_1909,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_e(X2,X6,X5,X7)
| ( X0 = X1 )
| ~ s_col(X0,X1,X2)
| ~ s_e(X1,X6,X4,X7)
| ~ s_e(X0,X6,X3,X7)
| ~ s_e3(X0,X1,X2,X3,X4,X5) ),
inference(unflattening,[status(thm)],[c_1908]) ).
tcf(c_1970,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
( s_e(X2,X6,X10,X14)
| ~ s_t(X9,X11,X13)
| ~ s_t(X1,X3,X5)
| ~ s_e(X5,X7,X13,X15)
| ~ s_e(X3,X5,X11,X13)
| ~ s_e(X1,X7,X9,X15)
| ~ s_e(X1,X5,X9,X13)
| ( X14 != X15 )
| ( X12 != X13 )
| ( X10 != X11 )
| ( X8 != X9 )
| ( X6 != X7 )
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_183]) ).
tcf(c_1971,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( s_e(X6,X4,X7,X5)
| ~ s_t(X2,X7,X3)
| ~ s_t(X0,X6,X1)
| ~ s_e(X6,X1,X7,X3)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X4,X2,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(unflattening,[status(thm)],[c_1970]) ).
tcf(c_3890,definition,
iPr_def_10 = s(sK3,sK0),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_3891,definition,
iPr_def_11 = s(sK3,sK1),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_3892,definition,
iPr_def_12 = s(sK3,sK2),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_3893,negated_conjecture,
s_t(iPr_def_10,iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_169,c_3892,c_3891,c_3890]) ).
tcf(c_3894,negated_conjecture,
~ s_t(sK0,sK1,sK2),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_3895,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_3900,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_t(X0,X2,X4)
| ~ s_t(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_5516,plain,
! [X0: $i] :
( ( X0 = sK1 )
| ( s(sK3,X0) != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_3891,c_163]) ).
tcf(c_5522,plain,
s(sK3,iPr_def_12) = sK2,
inference(superposition,[status(thm)],[c_3892,c_161]) ).
tcf(c_5557,plain,
s(sK3,sK2) = iPr_def_12,
inference(superposition,[status(thm)],[c_5522,c_161]) ).
tcf(c_5619,plain,
s_t(iPr_def_12,iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_3893,c_73]) ).
tcf(c_5628,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,X1),
inference(superposition,[status(thm)],[c_100,c_94]) ).
tcf(c_5792,plain,
s_col(iPr_def_11,iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_3893,c_191]) ).
tcf(c_5794,plain,
s_col(iPr_def_11,iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_5619,c_191]) ).
tcf(c_6365,plain,
( ( sK1 = sK2 )
| ( iPr_def_11 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_5557,c_5516]) ).
tcf(c_6389,plain,
( sameside(iPr_def_11,iPr_def_12,iPr_def_10)
| s_t(iPr_def_11,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_5792,c_134]) ).
tcf(c_6390,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| s_t(iPr_def_11,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5794,c_134]) ).
tcf(c_6459,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(sK0,sK1,sK2)
| ~ s_t(X0,X1,X2)
| ( sK2 != X2 )
| ( sK1 != X1 )
| ( sK0 != X0 ) ),
inference(instantiation,[status(thm)],[c_3900]) ).
tcf(c_6633,plain,
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_3893,c_75]) ).
tcf(c_6635,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_5619,c_75]) ).
tcf(c_7761,plain,
! [X0: $i,X1: $i] : s_m(s(X0,X1),X0,X1),
inference(superposition,[status(thm)],[c_161,c_158]) ).
tcf(c_7787,plain,
s_m(sK0,sK3,iPr_def_10),
inference(superposition,[status(thm)],[c_3890,c_158]) ).
tcf(c_7788,plain,
s(sK3,iPr_def_10) = sK0,
inference(superposition,[status(thm)],[c_3890,c_161]) ).
tcf(c_7794,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X0,X2) = X1 )
| ( s(X0,X1) != X2 ) ),
inference(superposition,[status(thm)],[c_161,c_163]) ).
tcf(c_7795,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0,X1) != X0 ) ),
inference(superposition,[status(thm)],[c_165,c_163]) ).
tcf(c_7796,plain,
! [X0: $i] :
( ( X0 = sK0 )
| ( s(sK3,X0) != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_3890,c_163]) ).
tcf(c_7816,plain,
s_m(sK1,sK3,iPr_def_11),
inference(superposition,[status(thm)],[c_3891,c_158]) ).
tcf(c_7818,plain,
s(sK3,iPr_def_11) = sK1,
inference(superposition,[status(thm)],[c_3891,c_161]) ).
tcf(c_7819,plain,
! [X0: $i] :
( ( X0 = sK1 )
| ( s(sK3,X0) != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_3891,c_163]) ).
tcf(c_7939,plain,
s_m(sK2,sK3,iPr_def_12),
inference(superposition,[status(thm)],[c_3892,c_158]) ).
tcf(c_7941,plain,
s(sK3,iPr_def_12) = sK2,
inference(superposition,[status(thm)],[c_3892,c_161]) ).
tcf(c_7942,plain,
! [X0: $i] :
( ( X0 = sK2 )
| ( s(sK3,X0) != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_3892,c_163]) ).
tcf(c_8108,plain,
s_m(iPr_def_10,sK3,sK0),
inference(superposition,[status(thm)],[c_3890,c_7761]) ).
tcf(c_8109,plain,
s_m(iPr_def_11,sK3,sK1),
inference(superposition,[status(thm)],[c_3891,c_7761]) ).
tcf(c_8110,plain,
s_m(iPr_def_12,sK3,sK2),
inference(superposition,[status(thm)],[c_3892,c_7761]) ).
tcf(c_8122,plain,
s(sK3,sK0) = iPr_def_10,
inference(superposition,[status(thm)],[c_7788,c_161]) ).
tcf(c_8123,plain,
! [X0: $i] :
( ( X0 = iPr_def_10 )
| ( s(sK3,X0) != sK0 ) ),
inference(superposition,[status(thm)],[c_7788,c_163]) ).
tcf(c_8167,plain,
s(sK3,sK1) = iPr_def_11,
inference(superposition,[status(thm)],[c_7818,c_161]) ).
tcf(c_8168,plain,
! [X0: $i] :
( ( X0 = iPr_def_11 )
| ( s(sK3,X0) != sK1 ) ),
inference(superposition,[status(thm)],[c_7818,c_163]) ).
tcf(c_8248,plain,
s(sK3,sK2) = iPr_def_12,
inference(superposition,[status(thm)],[c_7941,c_161]) ).
tcf(c_8249,plain,
! [X0: $i] :
( ( X0 = iPr_def_12 )
| ( s(sK3,X0) != sK2 ) ),
inference(superposition,[status(thm)],[c_7941,c_163]) ).
tcf(c_8453,plain,
( ( sK0 = sK3 )
| ( sK0 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8122,c_164]) ).
tcf(c_8455,plain,
( ( sK1 = sK3 )
| ( sK1 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_8167,c_164]) ).
tcf(c_8457,plain,
( ( sK2 = sK3 )
| ( sK2 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8248,c_164]) ).
tcf(c_8459,plain,
( ( sK3 = iPr_def_10 )
| ( sK0 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_7788,c_164]) ).
tcf(c_8460,plain,
( ( sK3 = iPr_def_11 )
| ( sK1 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_7818,c_164]) ).
tcf(c_8461,plain,
( ( sK3 = iPr_def_12 )
| ( sK2 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_7941,c_164]) ).
tcf(c_8486,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_t(ext(X0,X1,X2,X3),X1,X0),
inference(superposition,[status(thm)],[c_52,c_73]) ).
tcf(c_8489,plain,
s_t(iPr_def_12,iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_3893,c_73]) ).
tcf(c_8766,plain,
! [X0: $i] :
( ( s(sK3,X0) = sK0 )
| ( X0 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8122,c_7794]) ).
tcf(c_8768,plain,
! [X0: $i] :
( ( s(sK3,X0) = sK1 )
| ( X0 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_8167,c_7794]) ).
tcf(c_8770,plain,
! [X0: $i] :
( ( s(sK3,X0) = sK2 )
| ( X0 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8248,c_7794]) ).
tcf(c_8772,plain,
! [X0: $i] :
( ( s(sK3,X0) = iPr_def_10 )
| ( X0 != sK0 ) ),
inference(superposition,[status(thm)],[c_7788,c_7794]) ).
tcf(c_8773,plain,
! [X0: $i] :
( ( s(sK3,X0) = iPr_def_11 )
| ( X0 != sK1 ) ),
inference(superposition,[status(thm)],[c_7818,c_7794]) ).
tcf(c_8774,plain,
! [X0: $i] :
( ( s(sK3,X0) = iPr_def_12 )
| ( X0 != sK2 ) ),
inference(superposition,[status(thm)],[c_7941,c_7794]) ).
tcf(c_8988,plain,
! [X0: $i,X1: $i] :
( s_t(sK0,sK1,sK2)
| ~ s_t(sK0,X0,X1)
| ( sK2 != X1 )
| ( sK1 != X0 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_6459]) ).
tcf(c_8989,plain,
sK0 = sK0,
inference(instantiation,[status(thm)],[c_3895]) ).
tcf(c_8992,plain,
! [X0: $i,X1: $i,X2: $i] : s_e(s(X0,X1),X2,X1,s(X0,X2)),
inference(superposition,[status(thm)],[c_161,c_166]) ).
tcf(c_8993,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,X0,s(X0,X1)),
inference(superposition,[status(thm)],[c_165,c_166]) ).
tcf(c_8994,plain,
! [X0: $i] : s_e(sK0,X0,iPr_def_10,s(sK3,X0)),
inference(superposition,[status(thm)],[c_8122,c_166]) ).
tcf(c_8996,plain,
! [X0: $i] : s_e(sK1,X0,iPr_def_11,s(sK3,X0)),
inference(superposition,[status(thm)],[c_8167,c_166]) ).
tcf(c_8998,plain,
! [X0: $i] : s_e(sK2,X0,iPr_def_12,s(sK3,X0)),
inference(superposition,[status(thm)],[c_8248,c_166]) ).
tcf(c_9000,plain,
! [X0: $i] : s_e(iPr_def_10,X0,sK0,s(sK3,X0)),
inference(superposition,[status(thm)],[c_7788,c_166]) ).
tcf(c_9001,plain,
! [X0: $i] : s_e(iPr_def_11,X0,sK1,s(sK3,X0)),
inference(superposition,[status(thm)],[c_7818,c_166]) ).
tcf(c_9002,plain,
! [X0: $i] : s_e(iPr_def_12,X0,sK2,s(sK3,X0)),
inference(superposition,[status(thm)],[c_7941,c_166]) ).
tcf(c_9003,plain,
! [X0: $i,X1: $i,X2: $i] : s_e(X0,s(X1,X2),s(X1,X0),X2),
inference(superposition,[status(thm)],[c_161,c_166]) ).
tcf(c_9004,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,s(X1,X0),X1),
inference(superposition,[status(thm)],[c_165,c_166]) ).
tcf(c_9005,plain,
! [X0: $i] : s_e(X0,sK0,s(sK3,X0),iPr_def_10),
inference(superposition,[status(thm)],[c_8122,c_166]) ).
tcf(c_9007,plain,
! [X0: $i] : s_e(X0,sK1,s(sK3,X0),iPr_def_11),
inference(superposition,[status(thm)],[c_8167,c_166]) ).
tcf(c_9009,plain,
! [X0: $i] : s_e(X0,sK2,s(sK3,X0),iPr_def_12),
inference(superposition,[status(thm)],[c_8248,c_166]) ).
tcf(c_9011,plain,
! [X0: $i] : s_e(X0,iPr_def_10,s(sK3,X0),sK0),
inference(superposition,[status(thm)],[c_7788,c_166]) ).
tcf(c_9012,plain,
! [X0: $i] : s_e(X0,iPr_def_11,s(sK3,X0),sK1),
inference(superposition,[status(thm)],[c_7818,c_166]) ).
tcf(c_9013,plain,
! [X0: $i] : s_e(X0,iPr_def_12,s(sK3,X0),sK2),
inference(superposition,[status(thm)],[c_7941,c_166]) ).
tcf(c_9179,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(X0,X1,ext(X0,X1,X2,X3)),
inference(superposition,[status(thm)],[c_52,c_189]) ).
tcf(c_9183,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(ext(X0,X1,X2,X3),X1,X0),
inference(superposition,[status(thm)],[c_8486,c_189]) ).
tcf(c_9353,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(ext(X0,X1,X2,X3),X0,X1),
inference(superposition,[status(thm)],[c_52,c_190]) ).
tcf(c_9356,plain,
s_col(iPr_def_12,iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_3893,c_190]) ).
tcf(c_9357,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(X0,ext(X0,X1,X2,X3),X1),
inference(superposition,[status(thm)],[c_8486,c_190]) ).
tcf(c_9363,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(X0,ext(X1,X0,X2,X3),X1),
inference(superposition,[status(thm)],[c_52,c_191]) ).
tcf(c_9367,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_col(X0,X1,ext(X1,X0,X2,X3)),
inference(superposition,[status(thm)],[c_8486,c_191]) ).
tcf(c_9368,plain,
s_col(iPr_def_11,iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_8489,c_191]) ).
tcf(c_9565,plain,
! [X0: $i,X1: $i] : s_e(X0,s(X0,X1),X0,X1),
inference(superposition,[status(thm)],[c_161,c_8993]) ).
tcf(c_9567,plain,
s_e(sK3,sK0,sK3,iPr_def_10),
inference(superposition,[status(thm)],[c_8122,c_8993]) ).
tcf(c_9569,plain,
s_e(sK3,sK1,sK3,iPr_def_11),
inference(superposition,[status(thm)],[c_8167,c_8993]) ).
tcf(c_9571,plain,
s_e(sK3,sK2,sK3,iPr_def_12),
inference(superposition,[status(thm)],[c_8248,c_8993]) ).
tcf(c_9573,plain,
s_e(sK3,iPr_def_10,sK3,sK0),
inference(superposition,[status(thm)],[c_7788,c_8993]) ).
tcf(c_9574,plain,
s_e(sK3,iPr_def_11,sK3,sK1),
inference(superposition,[status(thm)],[c_7818,c_8993]) ).
tcf(c_9575,plain,
s_e(sK3,iPr_def_12,sK3,sK2),
inference(superposition,[status(thm)],[c_7941,c_8993]) ).
tcf(c_9709,plain,
( ( sK0 = sK3 )
| ( sK3 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8122,c_7795]) ).
tcf(c_9711,plain,
( ( sK1 = sK3 )
| ( sK3 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_8167,c_7795]) ).
tcf(c_9713,plain,
( ( sK2 = sK3 )
| ( sK3 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8248,c_7795]) ).
tcf(c_9715,plain,
( ( sK3 = iPr_def_10 )
| ( sK0 != sK3 ) ),
inference(superposition,[status(thm)],[c_7788,c_7795]) ).
tcf(c_9716,plain,
( ( sK3 = iPr_def_11 )
| ( sK1 != sK3 ) ),
inference(superposition,[status(thm)],[c_7818,c_7795]) ).
tcf(c_9717,plain,
( ( sK3 = iPr_def_12 )
| ( sK2 != sK3 ) ),
inference(superposition,[status(thm)],[c_7941,c_7795]) ).
tcf(c_9862,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_11 )
| ( xb = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_3893,c_203]) ).
tcf(c_9864,plain,
( sameside(iPr_def_11,iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 )
| ( xb = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_5619,c_203]) ).
tcf(c_10062,plain,
! [X0: $i,X1: $i] : s_t(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_158,c_205]) ).
tcf(c_10063,plain,
! [X0: $i,X1: $i] : s_t(s(X0,X1),X0,X1),
inference(superposition,[status(thm)],[c_7761,c_205]) ).
tcf(c_10064,plain,
s_t(sK0,sK3,iPr_def_10),
inference(superposition,[status(thm)],[c_7787,c_205]) ).
tcf(c_10065,plain,
s_t(sK1,sK3,iPr_def_11),
inference(superposition,[status(thm)],[c_7816,c_205]) ).
tcf(c_10066,plain,
s_t(sK2,sK3,iPr_def_12),
inference(superposition,[status(thm)],[c_7939,c_205]) ).
tcf(c_10067,plain,
s_t(iPr_def_10,sK3,sK0),
inference(superposition,[status(thm)],[c_8108,c_205]) ).
tcf(c_10068,plain,
s_t(iPr_def_11,sK3,sK1),
inference(superposition,[status(thm)],[c_8109,c_205]) ).
tcf(c_10069,plain,
s_t(iPr_def_12,sK3,sK2),
inference(superposition,[status(thm)],[c_8110,c_205]) ).
tcf(c_10224,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_11 ) ),
inference(global_subsumption_just,[status(thm)],[c_9862,c_6390,c_6633]) ).
tcf(c_10252,plain,
( sameside(iPr_def_11,iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(global_subsumption_just,[status(thm)],[c_9864,c_6389,c_6635]) ).
tcf(c_10354,plain,
! [X0: $i,X1: $i,X2: $i] : ext(X0,X1,X2,X2) = X1,
inference(superposition,[status(thm)],[c_53,c_69]) ).
tcf(c_10374,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ sameside(X0,X1,ext(X0,X1,X2,X3)),
inference(superposition,[status(thm)],[c_52,c_133]) ).
tcf(c_10377,plain,
~ sameside(iPr_def_10,iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_3893,c_133]) ).
tcf(c_10378,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ sameside(ext(X0,X1,X2,X3),X1,X0),
inference(superposition,[status(thm)],[c_8486,c_133]) ).
tcf(c_10379,plain,
~ sameside(iPr_def_12,iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_8489,c_133]) ).
tcf(c_10561,plain,
~ sameside(sK0,sK3,iPr_def_10),
inference(superposition,[status(thm)],[c_10064,c_133]) ).
tcf(c_10562,plain,
s_col(sK3,iPr_def_10,sK0),
inference(superposition,[status(thm)],[c_10064,c_191]) ).
tcf(c_10563,plain,
s_col(iPr_def_10,sK0,sK3),
inference(superposition,[status(thm)],[c_10064,c_190]) ).
tcf(c_10582,plain,
~ sameside(sK1,sK3,iPr_def_11),
inference(superposition,[status(thm)],[c_10065,c_133]) ).
tcf(c_10583,plain,
s_col(sK3,iPr_def_11,sK1),
inference(superposition,[status(thm)],[c_10065,c_191]) ).
tcf(c_10584,plain,
s_col(iPr_def_11,sK1,sK3),
inference(superposition,[status(thm)],[c_10065,c_190]) ).
tcf(c_10587,plain,
~ sameside(sK2,sK3,iPr_def_12),
inference(superposition,[status(thm)],[c_10066,c_133]) ).
tcf(c_10588,plain,
s_col(sK3,iPr_def_12,sK2),
inference(superposition,[status(thm)],[c_10066,c_191]) ).
tcf(c_10589,plain,
s_col(iPr_def_12,sK2,sK3),
inference(superposition,[status(thm)],[c_10066,c_190]) ).
tcf(c_10843,plain,
~ sameside(iPr_def_10,sK3,sK0),
inference(superposition,[status(thm)],[c_10067,c_133]) ).
tcf(c_10844,plain,
s_col(sK3,sK0,iPr_def_10),
inference(superposition,[status(thm)],[c_10067,c_191]) ).
tcf(c_10845,plain,
s_col(sK0,iPr_def_10,sK3),
inference(superposition,[status(thm)],[c_10067,c_190]) ).
tcf(c_11045,plain,
~ sameside(iPr_def_11,sK3,sK1),
inference(superposition,[status(thm)],[c_10068,c_133]) ).
tcf(c_11046,plain,
s_col(sK3,sK1,iPr_def_11),
inference(superposition,[status(thm)],[c_10068,c_191]) ).
tcf(c_11047,plain,
s_col(sK1,iPr_def_11,sK3),
inference(superposition,[status(thm)],[c_10068,c_190]) ).
tcf(c_11050,plain,
~ sameside(iPr_def_12,sK3,sK2),
inference(superposition,[status(thm)],[c_10069,c_133]) ).
tcf(c_11051,plain,
s_col(sK3,sK2,iPr_def_12),
inference(superposition,[status(thm)],[c_10069,c_191]) ).
tcf(c_11052,plain,
s_col(sK2,iPr_def_12,sK3),
inference(superposition,[status(thm)],[c_10069,c_190]) ).
tcf(c_11103,plain,
! [X0: $i,X1: $i] : ~ sameside(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_10062,c_133]) ).
tcf(c_11104,plain,
! [X0: $i,X1: $i] : s_col(X0,s(X0,X1),X1),
inference(superposition,[status(thm)],[c_10062,c_191]) ).
tcf(c_11105,plain,
! [X0: $i,X1: $i] : s_col(s(X0,X1),X1,X0),
inference(superposition,[status(thm)],[c_10062,c_190]) ).
tcf(c_11363,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_m(X0,X1,X1) ),
inference(superposition,[status(thm)],[c_206,c_69]) ).
tcf(c_11379,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_e(X0,X1,X2,ext(X3,X2,X0,X1)),
inference(superposition,[status(thm)],[c_53,c_62]) ).
tcf(c_11382,plain,
! [X0: $i,X1: $i,X2: $i] : s_e(s(X0,X1),s(X0,X2),X1,X2),
inference(superposition,[status(thm)],[c_166,c_62]) ).
tcf(c_11383,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X1,X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_206,c_62]) ).
tcf(c_11510,plain,
! [X0: $i,X1: $i] : ~ sameside(s(X0,X1),X0,X1),
inference(superposition,[status(thm)],[c_10063,c_133]) ).
tcf(c_11511,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,s(X0,X1)),
inference(superposition,[status(thm)],[c_10063,c_191]) ).
tcf(c_11512,plain,
! [X0: $i,X1: $i] : s_col(X0,s(X1,X0),X1),
inference(superposition,[status(thm)],[c_10063,c_190]) ).
tcf(c_11520,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_e(ext(X0,X1,X2,X3),X1,X2,X3),
inference(superposition,[status(thm)],[c_53,c_64]) ).
tcf(c_11523,plain,
! [X0: $i,X1: $i,X2: $i] : s_e(X0,X1,s(X2,X1),s(X2,X0)),
inference(superposition,[status(thm)],[c_166,c_64]) ).
tcf(c_11524,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X0,X1,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_206,c_64]) ).
tcf(c_11525,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_8993,c_64]) ).
tcf(c_11526,plain,
s_e(sK0,sK3,sK3,iPr_def_10),
inference(superposition,[status(thm)],[c_9567,c_64]) ).
tcf(c_11527,plain,
s_e(sK1,sK3,sK3,iPr_def_11),
inference(superposition,[status(thm)],[c_9569,c_64]) ).
tcf(c_11528,plain,
s_e(sK2,sK3,sK3,iPr_def_12),
inference(superposition,[status(thm)],[c_9571,c_64]) ).
tcf(c_11529,plain,
s_e(iPr_def_10,sK3,sK3,sK0),
inference(superposition,[status(thm)],[c_9573,c_64]) ).
tcf(c_11530,plain,
s_e(iPr_def_11,sK3,sK3,sK1),
inference(superposition,[status(thm)],[c_9574,c_64]) ).
tcf(c_11752,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_e(X0,ext(X1,X0,X2,X3),X3,X2),
inference(superposition,[status(thm)],[c_53,c_65]) ).
tcf(c_11756,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X1,X0,X2,X1)
| ~ s_m(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_206,c_65]) ).
tcf(c_11757,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,s(X0,X1),X0),
inference(superposition,[status(thm)],[c_8993,c_65]) ).
tcf(c_11758,plain,
s_e(sK3,sK0,iPr_def_10,sK3),
inference(superposition,[status(thm)],[c_9567,c_65]) ).
tcf(c_11759,plain,
s_e(sK3,sK1,iPr_def_11,sK3),
inference(superposition,[status(thm)],[c_9569,c_65]) ).
tcf(c_11760,plain,
s_e(sK3,sK2,iPr_def_12,sK3),
inference(superposition,[status(thm)],[c_9571,c_65]) ).
tcf(c_11761,plain,
s_e(sK3,iPr_def_10,sK0,sK3),
inference(superposition,[status(thm)],[c_9573,c_65]) ).
tcf(c_11762,plain,
s_e(sK3,iPr_def_11,sK1,sK3),
inference(superposition,[status(thm)],[c_9574,c_65]) ).
tcf(c_11946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : s_e(ext(X0,X1,X2,X3),X1,X3,X2),
inference(superposition,[status(thm)],[c_53,c_70]) ).
tcf(c_11950,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X0,X1,X2,X1)
| ~ s_m(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_206,c_70]) ).
tcf(c_11952,plain,
s_e(sK0,sK3,iPr_def_10,sK3),
inference(superposition,[status(thm)],[c_9567,c_70]) ).
tcf(c_11953,plain,
s_e(sK1,sK3,iPr_def_11,sK3),
inference(superposition,[status(thm)],[c_9569,c_70]) ).
tcf(c_11954,plain,
s_e(sK2,sK3,iPr_def_12,sK3),
inference(superposition,[status(thm)],[c_9571,c_70]) ).
tcf(c_11955,plain,
s_e(iPr_def_10,sK3,sK0,sK3),
inference(superposition,[status(thm)],[c_9573,c_70]) ).
tcf(c_11956,plain,
s_e(iPr_def_11,sK3,sK1,sK3),
inference(superposition,[status(thm)],[c_9574,c_70]) ).
tcf(c_12202,plain,
s_e(iPr_def_12,sK3,sK2,sK3),
inference(superposition,[status(thm)],[c_9575,c_70]) ).
tcf(c_12203,plain,
s_e(sK3,iPr_def_12,sK2,sK3),
inference(superposition,[status(thm)],[c_9575,c_65]) ).
tcf(c_12204,plain,
s_e(iPr_def_12,sK3,sK3,sK2),
inference(superposition,[status(thm)],[c_9575,c_64]) ).
tcf(c_12252,plain,
( ( sK0 = sK1 )
| ( iPr_def_10 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_8167,c_7796]) ).
tcf(c_12254,plain,
( ( sK0 = sK2 )
| ( iPr_def_10 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8248,c_7796]) ).
tcf(c_12257,plain,
( ( sK0 = iPr_def_11 )
| ( sK1 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_7818,c_7796]) ).
tcf(c_12258,plain,
( ( sK0 = iPr_def_12 )
| ( sK2 != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_7941,c_7796]) ).
tcf(c_12461,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,c63(X0,X1,X2),X0)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_129,c_191]) ).
tcf(c_12462,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(c63(X0,X1,X2),X0,X1)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_129,c_190]) ).
tcf(c_12463,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_129,c_189]) ).
tcf(c_12464,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(c63(X0,X1,X2),X1,X0)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_129,c_73]) ).
tcf(c_12635,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,c63(X0,X1,X2),X2)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_130,c_191]) ).
tcf(c_12636,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(c63(X0,X1,X2),X2,X1)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_130,c_190]) ).
tcf(c_12637,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X2,X1,c63(X0,X1,X2))
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_130,c_189]) ).
tcf(c_12638,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(c63(X0,X1,X2),X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_130,c_73]) ).
tcf(c_12800,plain,
( ( sK1 = sK2 )
| ( iPr_def_11 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8248,c_7819]) ).
tcf(c_12802,plain,
( ( sK1 = iPr_def_10 )
| ( sK0 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_7788,c_7819]) ).
tcf(c_12804,plain,
( ( sK1 = iPr_def_12 )
| ( sK2 != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_7941,c_7819]) ).
tcf(c_12827,plain,
! [X0: $i,X1: $i] :
( sameside(X0,X1,X0)
| s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_100,c_134]) ).
tcf(c_12831,plain,
( sameside(iPr_def_12,iPr_def_10,iPr_def_11)
| s_t(iPr_def_12,iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_9356,c_134]) ).
tcf(c_12834,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| s_t(iPr_def_11,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9368,c_134]) ).
tcf(c_12835,plain,
( sameside(sK3,iPr_def_10,sK0)
| s_t(sK3,iPr_def_10,sK0) ),
inference(superposition,[status(thm)],[c_10562,c_134]) ).
tcf(c_12836,plain,
( sameside(iPr_def_10,sK0,sK3)
| s_t(iPr_def_10,sK0,sK3) ),
inference(superposition,[status(thm)],[c_10563,c_134]) ).
tcf(c_12838,plain,
( sameside(sK3,iPr_def_11,sK1)
| s_t(sK3,iPr_def_11,sK1) ),
inference(superposition,[status(thm)],[c_10583,c_134]) ).
tcf(c_12839,plain,
( sameside(iPr_def_11,sK1,sK3)
| s_t(iPr_def_11,sK1,sK3) ),
inference(superposition,[status(thm)],[c_10584,c_134]) ).
tcf(c_12841,plain,
( sameside(sK3,iPr_def_12,sK2)
| s_t(sK3,iPr_def_12,sK2) ),
inference(superposition,[status(thm)],[c_10588,c_134]) ).
tcf(c_12842,plain,
( sameside(iPr_def_12,sK2,sK3)
| s_t(iPr_def_12,sK2,sK3) ),
inference(superposition,[status(thm)],[c_10589,c_134]) ).
tcf(c_12844,plain,
( sameside(sK3,sK0,iPr_def_10)
| s_t(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_10844,c_134]) ).
tcf(c_12845,plain,
( sameside(sK0,iPr_def_10,sK3)
| s_t(sK0,iPr_def_10,sK3) ),
inference(superposition,[status(thm)],[c_10845,c_134]) ).
tcf(c_12847,plain,
( sameside(sK3,sK1,iPr_def_11)
| s_t(sK3,sK1,iPr_def_11) ),
inference(superposition,[status(thm)],[c_11046,c_134]) ).
tcf(c_12848,plain,
( sameside(sK1,iPr_def_11,sK3)
| s_t(sK1,iPr_def_11,sK3) ),
inference(superposition,[status(thm)],[c_11047,c_134]) ).
tcf(c_12850,plain,
( sameside(sK3,sK2,iPr_def_12)
| s_t(sK3,sK2,iPr_def_12) ),
inference(superposition,[status(thm)],[c_11051,c_134]) ).
tcf(c_12851,plain,
( sameside(sK2,iPr_def_12,sK3)
| s_t(sK2,iPr_def_12,sK3) ),
inference(superposition,[status(thm)],[c_11052,c_134]) ).
tcf(c_13513,plain,
! [X0: $i,X1: $i] :
( sameside(X0,s(X0,X1),X1)
| s_t(X0,s(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_11104,c_134]) ).
tcf(c_13615,plain,
( sameside(iPr_def_12,iPr_def_10,iPr_def_11)
| s_t(iPr_def_11,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_12834,c_136]) ).
tcf(c_13655,plain,
( ( sK2 = iPr_def_10 )
| ( sK0 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_7788,c_7942]) ).
tcf(c_13656,plain,
( ( sK2 = iPr_def_11 )
| ( sK1 != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_7818,c_7942]) ).
tcf(c_14058,plain,
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_3893,c_75]) ).
tcf(c_14060,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_8489,c_75]) ).
tcf(c_14061,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_t(X0,X1,s(X0,X1)) ),
inference(superposition,[status(thm)],[c_10062,c_75]) ).
tcf(c_14063,plain,
( ( sK0 = sK3 )
| ~ s_t(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_10064,c_75]) ).
tcf(c_14064,plain,
( ( sK1 = sK3 )
| ~ s_t(sK3,sK1,iPr_def_11) ),
inference(superposition,[status(thm)],[c_10065,c_75]) ).
tcf(c_14065,plain,
( ( sK2 = sK3 )
| ~ s_t(sK3,sK2,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10066,c_75]) ).
tcf(c_14066,plain,
( ( sK3 = iPr_def_10 )
| ~ s_t(sK3,iPr_def_10,sK0) ),
inference(superposition,[status(thm)],[c_10067,c_75]) ).
tcf(c_14067,plain,
( ( sK3 = iPr_def_11 )
| ~ s_t(sK3,iPr_def_11,sK1) ),
inference(superposition,[status(thm)],[c_10068,c_75]) ).
tcf(c_14068,plain,
( ( sK3 = iPr_def_12 )
| ~ s_t(sK3,iPr_def_12,sK2) ),
inference(superposition,[status(thm)],[c_10069,c_75]) ).
tcf(c_14188,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,X0,X1)
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_72,c_76]) ).
tcf(c_14193,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_t(ext(X2,X0,X3,X4),X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8486,c_76]) ).
tcf(c_14196,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(s(X0,X2),X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_10063,c_76]) ).
tcf(c_14201,plain,
! [X0: $i] :
( s_t(iPr_def_11,sK3,X0)
| ~ s_t(sK3,X0,sK1) ),
inference(superposition,[status(thm)],[c_10068,c_76]) ).
tcf(c_14202,plain,
! [X0: $i] :
( s_t(iPr_def_12,sK3,X0)
| ~ s_t(sK3,X0,sK2) ),
inference(superposition,[status(thm)],[c_10069,c_76]) ).
tcf(c_15090,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_12,X0)
| ~ s_t(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_3893,c_77]) ).
tcf(c_15092,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,X0)
| ~ s_t(iPr_def_12,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_8489,c_77]) ).
tcf(c_15094,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ s_t(s(X0,X1),X1,X2) ),
inference(superposition,[status(thm)],[c_10063,c_77]) ).
tcf(c_15095,plain,
! [X0: $i] :
( s_t(sK3,iPr_def_10,X0)
| ~ s_t(sK0,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_10064,c_77]) ).
tcf(c_15096,plain,
! [X0: $i] :
( s_t(sK3,iPr_def_11,X0)
| ~ s_t(sK1,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_10065,c_77]) ).
tcf(c_15097,plain,
! [X0: $i] :
( s_t(sK3,iPr_def_12,X0)
| ~ s_t(sK2,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_10066,c_77]) ).
tcf(c_15098,plain,
! [X0: $i] :
( s_t(sK3,sK0,X0)
| ~ s_t(iPr_def_10,sK0,X0) ),
inference(superposition,[status(thm)],[c_10067,c_77]) ).
tcf(c_15099,plain,
! [X0: $i] :
( s_t(sK3,sK1,X0)
| ~ s_t(iPr_def_11,sK1,X0) ),
inference(superposition,[status(thm)],[c_10068,c_77]) ).
tcf(c_15100,plain,
! [X0: $i] :
( s_t(sK3,sK2,X0)
| ~ s_t(iPr_def_12,sK2,X0) ),
inference(superposition,[status(thm)],[c_10069,c_77]) ).
tcf(c_15573,plain,
! [X0: $i,X1: $i] :
( sameside(s(X0,X1),X1,X0)
| s_t(s(X0,X1),X1,X0) ),
inference(superposition,[status(thm)],[c_11105,c_134]) ).
tcf(c_15609,plain,
! [X0: $i,X1: $i] :
( sameside(X0,X1,s(X0,X1))
| s_t(X0,X1,s(X0,X1)) ),
inference(superposition,[status(thm)],[c_11511,c_134]) ).
tcf(c_15628,plain,
! [X0: $i,X1: $i] :
( sameside(X0,s(X1,X0),X1)
| s_t(X0,s(X1,X0),X1) ),
inference(superposition,[status(thm)],[c_11512,c_134]) ).
tcf(c_15650,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_11,iPr_def_12,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_52,c_15090]) ).
tcf(c_15652,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_12,c63(iPr_def_10,iPr_def_12,X0))
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_129,c_15090]) ).
tcf(c_15653,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_12,c63(X0,iPr_def_12,iPr_def_10))
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_130,c_15090]) ).
tcf(c_15654,plain,
s_t(iPr_def_11,iPr_def_12,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_10062,c_15090]) ).
tcf(c_15685,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_12,iPr_def_11,s(iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_15654,c_75]) ).
tcf(c_15686,plain,
~ sameside(iPr_def_11,iPr_def_12,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_15654,c_133]) ).
tcf(c_15687,plain,
s_col(iPr_def_12,s(iPr_def_12,iPr_def_10),iPr_def_11),
inference(superposition,[status(thm)],[c_15654,c_191]) ).
tcf(c_15688,plain,
s_col(s(iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_15654,c_190]) ).
tcf(c_15690,plain,
s_t(s(iPr_def_12,iPr_def_10),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_15654,c_73]) ).
tcf(c_16108,plain,
! [X0: $i,X1: $i] : ~ sameside(iPr_def_11,iPr_def_12,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_15650,c_133]) ).
tcf(c_16109,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_12,ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11),
inference(superposition,[status(thm)],[c_15650,c_191]) ).
tcf(c_16112,plain,
! [X0: $i,X1: $i] : s_t(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_15650,c_73]) ).
tcf(c_16133,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_11,iPr_def_10,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_52,c_15092]) ).
tcf(c_16135,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,c63(iPr_def_12,iPr_def_10,X0))
| ~ sameside(iPr_def_12,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_129,c_15092]) ).
tcf(c_16136,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,c63(X0,iPr_def_10,iPr_def_12))
| ~ sameside(X0,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_130,c_15092]) ).
tcf(c_16137,plain,
s_t(iPr_def_11,iPr_def_10,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_10062,c_15092]) ).
tcf(c_16570,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_72,c_79]) ).
tcf(c_16578,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(s(X0,X2),X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_10063,c_79]) ).
tcf(c_16579,plain,
! [X0: $i] :
( s_t(sK0,X0,iPr_def_10)
| ~ s_t(sK3,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_10064,c_79]) ).
tcf(c_16580,plain,
! [X0: $i] :
( s_t(sK1,X0,iPr_def_11)
| ~ s_t(sK3,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_10065,c_79]) ).
tcf(c_16581,plain,
! [X0: $i] :
( s_t(sK2,X0,iPr_def_12)
| ~ s_t(sK3,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10066,c_79]) ).
tcf(c_16582,plain,
! [X0: $i] :
( s_t(iPr_def_10,X0,sK0)
| ~ s_t(sK3,X0,sK0) ),
inference(superposition,[status(thm)],[c_10067,c_79]) ).
tcf(c_16583,plain,
! [X0: $i] :
( s_t(iPr_def_11,X0,sK1)
| ~ s_t(sK3,X0,sK1) ),
inference(superposition,[status(thm)],[c_10068,c_79]) ).
tcf(c_16584,plain,
! [X0: $i] :
( s_t(iPr_def_12,X0,sK2)
| ~ s_t(sK3,X0,sK2) ),
inference(superposition,[status(thm)],[c_10069,c_79]) ).
tcf(c_16904,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ~ s_t(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_3893,c_80]) ).
tcf(c_16906,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ~ s_t(iPr_def_12,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_8489,c_80]) ).
tcf(c_16907,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ s_t(X0,s(X1,X0),X2) ),
inference(superposition,[status(thm)],[c_10062,c_80]) ).
tcf(c_16909,plain,
! [X0: $i] :
( s_t(sK0,sK3,X0)
| ~ s_t(sK0,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_10064,c_80]) ).
tcf(c_16910,plain,
! [X0: $i] :
( s_t(sK1,sK3,X0)
| ~ s_t(sK1,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_10065,c_80]) ).
tcf(c_16911,plain,
! [X0: $i] :
( s_t(sK2,sK3,X0)
| ~ s_t(sK2,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_10066,c_80]) ).
tcf(c_16912,plain,
! [X0: $i] :
( s_t(iPr_def_10,sK3,X0)
| ~ s_t(iPr_def_10,sK0,X0) ),
inference(superposition,[status(thm)],[c_10067,c_80]) ).
tcf(c_16913,plain,
! [X0: $i] :
( s_t(iPr_def_11,sK3,X0)
| ~ s_t(iPr_def_11,sK1,X0) ),
inference(superposition,[status(thm)],[c_10068,c_80]) ).
tcf(c_16914,plain,
! [X0: $i] :
( s_t(iPr_def_12,sK3,X0)
| ~ s_t(iPr_def_12,sK2,X0) ),
inference(superposition,[status(thm)],[c_10069,c_80]) ).
tcf(c_16916,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_12,X0)
| ~ s_t(iPr_def_11,s(iPr_def_12,iPr_def_10),X0) ),
inference(superposition,[status(thm)],[c_15654,c_80]) ).
tcf(c_18116,plain,
( sameside(iPr_def_12,s(iPr_def_12,iPr_def_10),iPr_def_11)
| s_t(iPr_def_12,s(iPr_def_12,iPr_def_10),iPr_def_11) ),
inference(superposition,[status(thm)],[c_15687,c_134]) ).
tcf(c_18117,plain,
s_col(iPr_def_12,iPr_def_11,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_15687,c_98]) ).
tcf(c_18119,plain,
s_col(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_12),
inference(superposition,[status(thm)],[c_15687,c_96]) ).
tcf(c_18131,plain,
( sameside(s(iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_12)
| s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_15688,c_134]) ).
tcf(c_18159,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_10,iPr_def_11,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_52,c_16904]) ).
tcf(c_18162,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,c63(iPr_def_10,iPr_def_12,X0))
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_129,c_16904]) ).
tcf(c_18163,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,c63(X0,iPr_def_12,iPr_def_10))
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_130,c_16904]) ).
tcf(c_18164,plain,
s_t(iPr_def_10,iPr_def_11,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_10062,c_16904]) ).
tcf(c_18569,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ~ s_t(iPr_def_10,s(iPr_def_12,iPr_def_10),X0) ),
inference(superposition,[status(thm)],[c_18164,c_80]) ).
tcf(c_18572,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,s(iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_18164,c_76]) ).
tcf(c_18573,plain,
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,s(iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_18164,c_75]) ).
tcf(c_18574,plain,
~ sameside(iPr_def_10,iPr_def_11,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_18164,c_133]) ).
tcf(c_18575,plain,
s_col(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_10),
inference(superposition,[status(thm)],[c_18164,c_191]) ).
tcf(c_18576,plain,
s_col(s(iPr_def_12,iPr_def_10),iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_18164,c_190]) ).
tcf(c_18578,plain,
s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_18164,c_73]) ).
tcf(c_18688,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,ext(iPr_def_10,iPr_def_12,X1,X2)) ),
inference(superposition,[status(thm)],[c_18159,c_76]) ).
tcf(c_18689,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,ext(iPr_def_10,iPr_def_12,X0,X1)) ),
inference(superposition,[status(thm)],[c_18159,c_75]) ).
tcf(c_18690,plain,
! [X0: $i,X1: $i] : ~ sameside(iPr_def_10,iPr_def_11,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_18159,c_133]) ).
tcf(c_18691,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_11,ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_10),
inference(superposition,[status(thm)],[c_18159,c_191]) ).
tcf(c_18694,plain,
! [X0: $i,X1: $i] : s_t(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_18159,c_73]) ).
tcf(c_19238,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_12,iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_52,c_16906]) ).
tcf(c_19241,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,c63(iPr_def_12,iPr_def_10,X0))
| ~ sameside(iPr_def_12,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_129,c_16906]) ).
tcf(c_19242,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,c63(X0,iPr_def_10,iPr_def_12))
| ~ sameside(X0,iPr_def_10,iPr_def_12) ),
inference(superposition,[status(thm)],[c_130,c_16906]) ).
tcf(c_19243,plain,
s_t(iPr_def_12,iPr_def_11,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_10062,c_16906]) ).
tcf(c_19424,plain,
! [X0: $i] :
( ~ sameside(iPr_def_10,iPr_def_12,X0)
| ~ sameside(iPr_def_11,iPr_def_12,c63(iPr_def_10,iPr_def_12,X0)) ),
inference(superposition,[status(thm)],[c_15652,c_133]) ).
tcf(c_19425,plain,
! [X0: $i] :
( s_col(iPr_def_12,c63(iPr_def_10,iPr_def_12,X0),iPr_def_11)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_15652,c_191]) ).
tcf(c_19426,plain,
! [X0: $i] :
( s_col(c63(iPr_def_10,iPr_def_12,X0),iPr_def_11,iPr_def_12)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_15652,c_190]) ).
tcf(c_19427,plain,
! [X0: $i] :
( s_col(iPr_def_11,iPr_def_12,c63(iPr_def_10,iPr_def_12,X0))
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_15652,c_189]) ).
tcf(c_19428,plain,
! [X0: $i] :
( s_t(c63(iPr_def_10,iPr_def_12,X0),iPr_def_12,iPr_def_11)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_15652,c_73]) ).
tcf(c_20074,plain,
! [X0: $i] :
( ~ sameside(X0,iPr_def_12,iPr_def_10)
| ~ sameside(iPr_def_11,iPr_def_12,c63(X0,iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_15653,c_133]) ).
tcf(c_20075,plain,
! [X0: $i] :
( s_col(iPr_def_12,c63(X0,iPr_def_12,iPr_def_10),iPr_def_11)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_15653,c_191]) ).
tcf(c_20076,plain,
! [X0: $i] :
( s_col(c63(X0,iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_12)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_15653,c_190]) ).
tcf(c_20077,plain,
! [X0: $i] :
( s_col(iPr_def_11,iPr_def_12,c63(X0,iPr_def_12,iPr_def_10))
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_15653,c_189]) ).
tcf(c_20078,plain,
! [X0: $i] :
( s_t(c63(X0,iPr_def_12,iPr_def_10),iPr_def_12,iPr_def_11)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_15653,c_73]) ).
tcf(c_20126,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ s_m(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_157,c_159]) ).
tcf(c_20128,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ s_m(s(X0,X1),X0,X2) ),
inference(superposition,[status(thm)],[c_7761,c_159]) ).
tcf(c_20129,plain,
! [X0: $i] :
( ( X0 = iPr_def_10 )
| ~ s_m(sK0,sK3,X0) ),
inference(superposition,[status(thm)],[c_7787,c_159]) ).
tcf(c_20130,plain,
! [X0: $i] :
( ( X0 = iPr_def_11 )
| ~ s_m(sK1,sK3,X0) ),
inference(superposition,[status(thm)],[c_7816,c_159]) ).
tcf(c_20131,plain,
! [X0: $i] :
( ( X0 = iPr_def_12 )
| ~ s_m(sK2,sK3,X0) ),
inference(superposition,[status(thm)],[c_7939,c_159]) ).
tcf(c_20132,plain,
! [X0: $i] :
( ( X0 = sK0 )
| ~ s_m(iPr_def_10,sK3,X0) ),
inference(superposition,[status(thm)],[c_8108,c_159]) ).
tcf(c_20133,plain,
! [X0: $i] :
( ( X0 = sK1 )
| ~ s_m(iPr_def_11,sK3,X0) ),
inference(superposition,[status(thm)],[c_8109,c_159]) ).
tcf(c_20134,plain,
! [X0: $i] :
( ( X0 = sK2 )
| ~ s_m(iPr_def_12,sK3,X0) ),
inference(superposition,[status(thm)],[c_8110,c_159]) ).
tcf(c_20643,plain,
! [X0: $i,X1: $i] :
( ( s(X0,X1) = X1 )
| ~ s_t(X0,s(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_8993,c_122]) ).
tcf(c_20644,plain,
( ( sK0 = iPr_def_10 )
| ~ s_t(sK3,iPr_def_10,sK0) ),
inference(superposition,[status(thm)],[c_9567,c_122]) ).
tcf(c_20645,plain,
( ( sK1 = iPr_def_11 )
| ~ s_t(sK3,iPr_def_11,sK1) ),
inference(superposition,[status(thm)],[c_9569,c_122]) ).
tcf(c_20646,plain,
( ( sK2 = iPr_def_12 )
| ~ s_t(sK3,iPr_def_12,sK2) ),
inference(superposition,[status(thm)],[c_9571,c_122]) ).
tcf(c_20647,plain,
( ( sK0 = iPr_def_10 )
| ~ s_t(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_9573,c_122]) ).
tcf(c_20648,plain,
( ( sK1 = iPr_def_11 )
| ~ s_t(sK3,sK1,iPr_def_11) ),
inference(superposition,[status(thm)],[c_9574,c_122]) ).
tcf(c_20649,plain,
( ( sK2 = iPr_def_12 )
| ~ s_t(sK3,sK2,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9575,c_122]) ).
tcf(c_20961,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),iPr_def_12,X0)
| ~ s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_15690,c_80]) ).
tcf(c_20962,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),X0,iPr_def_11)
| ~ s_t(iPr_def_12,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_15690,c_79]) ).
tcf(c_20963,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ~ s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_15690,c_77]) ).
tcf(c_20964,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),iPr_def_12,X0)
| ~ s_t(iPr_def_12,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_15690,c_76]) ).
tcf(c_20965,plain,
( ( s(iPr_def_12,iPr_def_10) = iPr_def_12 )
| ~ s_t(iPr_def_12,s(iPr_def_12,iPr_def_10),iPr_def_11) ),
inference(superposition,[status(thm)],[c_15690,c_75]) ).
tcf(c_20966,plain,
~ sameside(s(iPr_def_12,iPr_def_10),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_15690,c_133]) ).
tcf(c_21161,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,X0)
| ~ s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),X0) ),
inference(superposition,[status(thm)],[c_16137,c_80]) ).
tcf(c_21162,plain,
! [X0: $i] :
( s_t(iPr_def_11,X0,s(iPr_def_10,iPr_def_12))
| ~ s_t(iPr_def_10,X0,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_16137,c_79]) ).
tcf(c_21163,plain,
! [X0: $i] :
( s_t(iPr_def_10,s(iPr_def_10,iPr_def_12),X0)
| ~ s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),X0) ),
inference(superposition,[status(thm)],[c_16137,c_77]) ).
tcf(c_21164,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,X0)
| ~ s_t(iPr_def_10,X0,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_16137,c_76]) ).
tcf(c_21165,plain,
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_10,iPr_def_11,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_16137,c_75]) ).
tcf(c_21166,plain,
~ sameside(iPr_def_11,iPr_def_10,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_16137,c_133]) ).
tcf(c_21167,plain,
s_col(iPr_def_10,s(iPr_def_10,iPr_def_12),iPr_def_11),
inference(superposition,[status(thm)],[c_16137,c_191]) ).
tcf(c_21168,plain,
s_col(s(iPr_def_10,iPr_def_12),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_16137,c_190]) ).
tcf(c_21170,plain,
s_t(s(iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_16137,c_73]) ).
tcf(c_21519,plain,
( sameside(iPr_def_12,iPr_def_11,s(iPr_def_12,iPr_def_10))
| s_t(iPr_def_12,iPr_def_11,s(iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_18117,c_134]) ).
tcf(c_21542,plain,
! [X0: $i] :
( ~ sameside(iPr_def_10,iPr_def_12,X0)
| ~ sameside(iPr_def_10,iPr_def_11,c63(iPr_def_10,iPr_def_12,X0)) ),
inference(superposition,[status(thm)],[c_18162,c_133]) ).
tcf(c_21543,plain,
! [X0: $i] :
( s_col(iPr_def_11,c63(iPr_def_10,iPr_def_12,X0),iPr_def_10)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_18162,c_191]) ).
tcf(c_21544,plain,
! [X0: $i] :
( s_col(c63(iPr_def_10,iPr_def_12,X0),iPr_def_10,iPr_def_11)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_18162,c_190]) ).
tcf(c_21545,plain,
! [X0: $i] :
( s_col(iPr_def_10,iPr_def_11,c63(iPr_def_10,iPr_def_12,X0))
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_18162,c_189]) ).
tcf(c_21546,plain,
! [X0: $i] :
( s_t(c63(iPr_def_10,iPr_def_12,X0),iPr_def_11,iPr_def_10)
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_18162,c_73]) ).
tcf(c_21864,plain,
! [X0: $i] :
( ~ sameside(X0,iPr_def_12,iPr_def_10)
| ~ sameside(iPr_def_10,iPr_def_11,c63(X0,iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_18163,c_133]) ).
tcf(c_21865,plain,
! [X0: $i] :
( s_col(iPr_def_11,c63(X0,iPr_def_12,iPr_def_10),iPr_def_10)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18163,c_191]) ).
tcf(c_21866,plain,
! [X0: $i] :
( s_col(c63(X0,iPr_def_12,iPr_def_10),iPr_def_10,iPr_def_11)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18163,c_190]) ).
tcf(c_21867,plain,
! [X0: $i] :
( s_col(iPr_def_10,iPr_def_11,c63(X0,iPr_def_12,iPr_def_10))
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18163,c_189]) ).
tcf(c_21868,plain,
! [X0: $i] :
( s_t(c63(X0,iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_10)
| ~ sameside(X0,iPr_def_12,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18163,c_73]) ).
tcf(c_23384,plain,
( sameside(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_10)
| s_t(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_18575,c_134]) ).
tcf(c_23385,plain,
s_col(iPr_def_11,iPr_def_10,s(iPr_def_12,iPr_def_10)),
inference(superposition,[status(thm)],[c_18575,c_98]) ).
tcf(c_23387,plain,
s_col(iPr_def_10,s(iPr_def_12,iPr_def_10),iPr_def_11),
inference(superposition,[status(thm)],[c_18575,c_96]) ).
tcf(c_23392,plain,
( sameside(s(iPr_def_12,iPr_def_10),iPr_def_10,iPr_def_11)
| s_t(s(iPr_def_12,iPr_def_10),iPr_def_10,iPr_def_11) ),
inference(superposition,[status(thm)],[c_18576,c_134]) ).
tcf(c_23553,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,X0)
| ~ s_t(s(iPr_def_12,iPr_def_10),iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_18578,c_80]) ).
tcf(c_23554,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),X0,iPr_def_10)
| ~ s_t(iPr_def_11,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18578,c_79]) ).
tcf(c_23555,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_10,X0)
| ~ s_t(s(iPr_def_12,iPr_def_10),iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_18578,c_77]) ).
tcf(c_23556,plain,
! [X0: $i] :
( s_t(s(iPr_def_12,iPr_def_10),iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18578,c_76]) ).
tcf(c_23557,plain,
( ( s(iPr_def_12,iPr_def_10) = iPr_def_11 )
| ~ s_t(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_18578,c_75]) ).
tcf(c_23558,plain,
~ sameside(s(iPr_def_12,iPr_def_10),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_18578,c_133]) ).
tcf(c_23799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_col(X0,X1,ext(X2,X0,X3,X4))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14193,c_191]) ).
tcf(c_23800,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_col(X1,ext(X2,X0,X3,X4),X0)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14193,c_190]) ).
tcf(c_23801,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_col(ext(X2,X0,X3,X4),X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14193,c_189]) ).
tcf(c_23802,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_t(X1,X0,ext(X2,X0,X3,X4))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14193,c_73]) ).
tcf(c_24488,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,s(X0,X1),s(X0,X2))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_165,c_167]) ).
tcf(c_24489,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_10,s(sK3,X0),s(sK3,X1))
| ~ s_t(sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_8122,c_167]) ).
tcf(c_24491,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_11,s(sK3,X0),s(sK3,X1))
| ~ s_t(sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_8167,c_167]) ).
tcf(c_24493,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_12,s(sK3,X0),s(sK3,X1))
| ~ s_t(sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_8248,c_167]) ).
tcf(c_24495,plain,
! [X0: $i,X1: $i] :
( s_t(sK0,s(sK3,X0),s(sK3,X1))
| ~ s_t(iPr_def_10,X0,X1) ),
inference(superposition,[status(thm)],[c_7788,c_167]) ).
tcf(c_24496,plain,
! [X0: $i,X1: $i] :
( s_t(sK1,s(sK3,X0),s(sK3,X1))
| ~ s_t(iPr_def_11,X0,X1) ),
inference(superposition,[status(thm)],[c_7818,c_167]) ).
tcf(c_24497,plain,
! [X0: $i,X1: $i] :
( s_t(sK2,s(sK3,X0),s(sK3,X1))
| ~ s_t(iPr_def_12,X0,X1) ),
inference(superposition,[status(thm)],[c_7941,c_167]) ).
tcf(c_24499,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(s(X1,X0),X1,s(X1,X2))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_165,c_167]) ).
tcf(c_24500,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),iPr_def_10,s(sK3,X1))
| ~ s_t(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_8122,c_167]) ).
tcf(c_24502,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),iPr_def_11,s(sK3,X1))
| ~ s_t(X0,sK1,X1) ),
inference(superposition,[status(thm)],[c_8167,c_167]) ).
tcf(c_24504,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),iPr_def_12,s(sK3,X1))
| ~ s_t(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_8248,c_167]) ).
tcf(c_24506,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),sK0,s(sK3,X1))
| ~ s_t(X0,iPr_def_10,X1) ),
inference(superposition,[status(thm)],[c_7788,c_167]) ).
tcf(c_24507,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),sK1,s(sK3,X1))
| ~ s_t(X0,iPr_def_11,X1) ),
inference(superposition,[status(thm)],[c_7818,c_167]) ).
tcf(c_24508,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),sK2,s(sK3,X1))
| ~ s_t(X0,iPr_def_12,X1) ),
inference(superposition,[status(thm)],[c_7941,c_167]) ).
tcf(c_24510,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(s(X2,X0),s(X2,X1),X2)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_165,c_167]) ).
tcf(c_24511,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),iPr_def_10)
| ~ s_t(X0,X1,sK0) ),
inference(superposition,[status(thm)],[c_8122,c_167]) ).
tcf(c_24513,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),iPr_def_11)
| ~ s_t(X0,X1,sK1) ),
inference(superposition,[status(thm)],[c_8167,c_167]) ).
tcf(c_24515,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),iPr_def_12)
| ~ s_t(X0,X1,sK2) ),
inference(superposition,[status(thm)],[c_8248,c_167]) ).
tcf(c_24517,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),sK0)
| ~ s_t(X0,X1,iPr_def_10) ),
inference(superposition,[status(thm)],[c_7788,c_167]) ).
tcf(c_24518,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),sK1)
| ~ s_t(X0,X1,iPr_def_11) ),
inference(superposition,[status(thm)],[c_7818,c_167]) ).
tcf(c_24519,plain,
! [X0: $i,X1: $i] :
( s_t(s(sK3,X0),s(sK3,X1),sK2)
| ~ s_t(X0,X1,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7941,c_167]) ).
tcf(c_24520,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X2,s(X3,X0),s(X3,X1))
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_167,c_14188]) ).
tcf(c_24521,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2,X0) = s(X2,X1) )
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_167,c_55]) ).
tcf(c_25496,plain,
! [X0: $i,X1: $i] :
( s_m(X0,X1,X0)
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_61,c_207]) ).
tcf(c_25907,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X2,X0)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_49,c_113]) ).
tcf(c_25910,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X2,X2)
| ~ s_t(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_66,c_113]) ).
tcf(c_25914,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,s(X0,X2))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8993,c_113]) ).
tcf(c_25915,plain,
! [X0: $i] :
( le(sK3,X0,sK3,iPr_def_10)
| ~ s_t(sK3,X0,sK0) ),
inference(superposition,[status(thm)],[c_9567,c_113]) ).
tcf(c_25916,plain,
! [X0: $i] :
( le(sK3,X0,sK3,iPr_def_11)
| ~ s_t(sK3,X0,sK1) ),
inference(superposition,[status(thm)],[c_9569,c_113]) ).
tcf(c_25917,plain,
! [X0: $i] :
( le(sK3,X0,sK3,iPr_def_12)
| ~ s_t(sK3,X0,sK2) ),
inference(superposition,[status(thm)],[c_9571,c_113]) ).
tcf(c_25918,plain,
! [X0: $i] :
( le(sK3,X0,sK3,sK0)
| ~ s_t(sK3,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_9573,c_113]) ).
tcf(c_25919,plain,
! [X0: $i] :
( le(sK3,X0,sK3,sK1)
| ~ s_t(sK3,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_9574,c_113]) ).
tcf(c_25920,plain,
! [X0: $i] :
( le(sK3,X0,sK3,sK2)
| ~ s_t(sK3,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9575,c_113]) ).
tcf(c_25921,plain,
! [X0: $i] :
( le(sK0,X0,sK3,iPr_def_10)
| ~ s_t(sK0,X0,sK3) ),
inference(superposition,[status(thm)],[c_11526,c_113]) ).
tcf(c_25922,plain,
! [X0: $i] :
( le(sK1,X0,sK3,iPr_def_11)
| ~ s_t(sK1,X0,sK3) ),
inference(superposition,[status(thm)],[c_11527,c_113]) ).
tcf(c_25923,plain,
! [X0: $i] :
( le(sK2,X0,sK3,iPr_def_12)
| ~ s_t(sK2,X0,sK3) ),
inference(superposition,[status(thm)],[c_11528,c_113]) ).
tcf(c_25924,plain,
! [X0: $i] :
( le(iPr_def_10,X0,sK3,sK0)
| ~ s_t(iPr_def_10,X0,sK3) ),
inference(superposition,[status(thm)],[c_11529,c_113]) ).
tcf(c_25925,plain,
! [X0: $i] :
( le(iPr_def_11,X0,sK3,sK1)
| ~ s_t(iPr_def_11,X0,sK3) ),
inference(superposition,[status(thm)],[c_11530,c_113]) ).
tcf(c_25926,plain,
! [X0: $i] :
( le(sK3,X0,iPr_def_10,sK3)
| ~ s_t(sK3,X0,sK0) ),
inference(superposition,[status(thm)],[c_11758,c_113]) ).
tcf(c_25927,plain,
! [X0: $i] :
( le(sK3,X0,iPr_def_11,sK3)
| ~ s_t(sK3,X0,sK1) ),
inference(superposition,[status(thm)],[c_11759,c_113]) ).
tcf(c_25928,plain,
! [X0: $i] :
( le(sK3,X0,iPr_def_12,sK3)
| ~ s_t(sK3,X0,sK2) ),
inference(superposition,[status(thm)],[c_11760,c_113]) ).
tcf(c_25929,plain,
! [X0: $i] :
( le(sK3,X0,sK0,sK3)
| ~ s_t(sK3,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_11761,c_113]) ).
tcf(c_25930,plain,
! [X0: $i] :
( le(sK3,X0,sK1,sK3)
| ~ s_t(sK3,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_11762,c_113]) ).
tcf(c_25931,plain,
! [X0: $i] :
( le(sK0,X0,iPr_def_10,sK3)
| ~ s_t(sK0,X0,sK3) ),
inference(superposition,[status(thm)],[c_11952,c_113]) ).
tcf(c_25932,plain,
! [X0: $i] :
( le(sK1,X0,iPr_def_11,sK3)
| ~ s_t(sK1,X0,sK3) ),
inference(superposition,[status(thm)],[c_11953,c_113]) ).
tcf(c_25933,plain,
! [X0: $i] :
( le(sK2,X0,iPr_def_12,sK3)
| ~ s_t(sK2,X0,sK3) ),
inference(superposition,[status(thm)],[c_11954,c_113]) ).
tcf(c_25934,plain,
! [X0: $i] :
( le(iPr_def_10,X0,sK0,sK3)
| ~ s_t(iPr_def_10,X0,sK3) ),
inference(superposition,[status(thm)],[c_11955,c_113]) ).
tcf(c_25935,plain,
! [X0: $i] :
( le(iPr_def_11,X0,sK1,sK3)
| ~ s_t(iPr_def_11,X0,sK3) ),
inference(superposition,[status(thm)],[c_11956,c_113]) ).
tcf(c_25936,plain,
! [X0: $i] :
( le(iPr_def_12,X0,sK2,sK3)
| ~ s_t(iPr_def_12,X0,sK3) ),
inference(superposition,[status(thm)],[c_12202,c_113]) ).
tcf(c_25937,plain,
! [X0: $i] :
( le(sK3,X0,sK2,sK3)
| ~ s_t(sK3,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_12203,c_113]) ).
tcf(c_25938,plain,
! [X0: $i] :
( le(iPr_def_12,X0,sK3,sK2)
| ~ s_t(iPr_def_12,X0,sK3) ),
inference(superposition,[status(thm)],[c_12204,c_113]) ).
tcf(c_26825,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X1,X0,X0,X2)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_49,c_199]) ).
tcf(c_26832,plain,
! [X0: $i,X1: $i,X2: $i] :
( le(X0,X1,X0,X2)
| ~ s_t(X0,s(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_8993,c_199]) ).
tcf(c_26833,plain,
! [X0: $i] :
( le(sK3,sK0,sK3,X0)
| ~ s_t(sK3,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_9567,c_199]) ).
tcf(c_26834,plain,
! [X0: $i] :
( le(sK3,sK1,sK3,X0)
| ~ s_t(sK3,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_9569,c_199]) ).
tcf(c_26835,plain,
! [X0: $i] :
( le(sK3,sK2,sK3,X0)
| ~ s_t(sK3,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_9571,c_199]) ).
tcf(c_26836,plain,
! [X0: $i] :
( le(sK3,iPr_def_10,sK3,X0)
| ~ s_t(sK3,sK0,X0) ),
inference(superposition,[status(thm)],[c_9573,c_199]) ).
tcf(c_26837,plain,
! [X0: $i] :
( le(sK3,iPr_def_11,sK3,X0)
| ~ s_t(sK3,sK1,X0) ),
inference(superposition,[status(thm)],[c_9574,c_199]) ).
tcf(c_26838,plain,
! [X0: $i] :
( le(sK3,iPr_def_12,sK3,X0)
| ~ s_t(sK3,sK2,X0) ),
inference(superposition,[status(thm)],[c_9575,c_199]) ).
tcf(c_26839,plain,
! [X0: $i] :
( le(sK0,sK3,sK3,X0)
| ~ s_t(sK3,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_11526,c_199]) ).
tcf(c_26840,plain,
! [X0: $i] :
( le(sK1,sK3,sK3,X0)
| ~ s_t(sK3,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_11527,c_199]) ).
tcf(c_26841,plain,
! [X0: $i] :
( le(sK2,sK3,sK3,X0)
| ~ s_t(sK3,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_11528,c_199]) ).
tcf(c_26842,plain,
! [X0: $i] :
( le(iPr_def_10,sK3,sK3,X0)
| ~ s_t(sK3,sK0,X0) ),
inference(superposition,[status(thm)],[c_11529,c_199]) ).
tcf(c_26843,plain,
! [X0: $i] :
( le(iPr_def_11,sK3,sK3,X0)
| ~ s_t(sK3,sK1,X0) ),
inference(superposition,[status(thm)],[c_11530,c_199]) ).
tcf(c_26844,plain,
! [X0: $i] :
( le(sK3,sK0,iPr_def_10,X0)
| ~ s_t(iPr_def_10,sK3,X0) ),
inference(superposition,[status(thm)],[c_11758,c_199]) ).
tcf(c_26845,plain,
! [X0: $i] :
( le(sK3,sK1,iPr_def_11,X0)
| ~ s_t(iPr_def_11,sK3,X0) ),
inference(superposition,[status(thm)],[c_11759,c_199]) ).
tcf(c_26846,plain,
! [X0: $i] :
( le(sK3,sK2,iPr_def_12,X0)
| ~ s_t(iPr_def_12,sK3,X0) ),
inference(superposition,[status(thm)],[c_11760,c_199]) ).
tcf(c_26847,plain,
! [X0: $i] :
( le(sK3,iPr_def_10,sK0,X0)
| ~ s_t(sK0,sK3,X0) ),
inference(superposition,[status(thm)],[c_11761,c_199]) ).
tcf(c_26848,plain,
! [X0: $i] :
( le(sK3,iPr_def_11,sK1,X0)
| ~ s_t(sK1,sK3,X0) ),
inference(superposition,[status(thm)],[c_11762,c_199]) ).
tcf(c_26849,plain,
! [X0: $i] :
( le(sK0,sK3,iPr_def_10,X0)
| ~ s_t(iPr_def_10,sK3,X0) ),
inference(superposition,[status(thm)],[c_11952,c_199]) ).
tcf(c_26850,plain,
! [X0: $i] :
( le(sK1,sK3,iPr_def_11,X0)
| ~ s_t(iPr_def_11,sK3,X0) ),
inference(superposition,[status(thm)],[c_11953,c_199]) ).
tcf(c_26851,plain,
! [X0: $i] :
( le(sK2,sK3,iPr_def_12,X0)
| ~ s_t(iPr_def_12,sK3,X0) ),
inference(superposition,[status(thm)],[c_11954,c_199]) ).
tcf(c_26852,plain,
! [X0: $i] :
( le(iPr_def_10,sK3,sK0,X0)
| ~ s_t(sK0,sK3,X0) ),
inference(superposition,[status(thm)],[c_11955,c_199]) ).
tcf(c_26853,plain,
! [X0: $i] :
( le(iPr_def_11,sK3,sK1,X0)
| ~ s_t(sK1,sK3,X0) ),
inference(superposition,[status(thm)],[c_11956,c_199]) ).
tcf(c_26854,plain,
! [X0: $i] :
( le(iPr_def_12,sK3,sK2,X0)
| ~ s_t(sK2,sK3,X0) ),
inference(superposition,[status(thm)],[c_12202,c_199]) ).
tcf(c_26855,plain,
! [X0: $i] :
( le(sK3,iPr_def_12,sK2,X0)
| ~ s_t(sK2,sK3,X0) ),
inference(superposition,[status(thm)],[c_12203,c_199]) ).
tcf(c_26856,plain,
! [X0: $i] :
( le(iPr_def_12,sK3,sK3,X0)
| ~ s_t(sK3,sK2,X0) ),
inference(superposition,[status(thm)],[c_12204,c_199]) ).
tcf(c_27884,plain,
( sameside(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_12)
| s_t(iPr_def_11,s(iPr_def_12,iPr_def_10),iPr_def_12) ),
inference(superposition,[status(thm)],[c_18119,c_134]) ).
tcf(c_27892,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ~ s_t(iPr_def_12,s(iPr_def_10,iPr_def_12),X0) ),
inference(superposition,[status(thm)],[c_19243,c_80]) ).
tcf(c_27893,plain,
! [X0: $i] :
( s_t(iPr_def_12,X0,s(iPr_def_10,iPr_def_12))
| ~ s_t(iPr_def_11,X0,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_19243,c_79]) ).
tcf(c_27894,plain,
! [X0: $i] :
( s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),X0)
| ~ s_t(iPr_def_12,s(iPr_def_10,iPr_def_12),X0) ),
inference(superposition,[status(thm)],[c_19243,c_77]) ).
tcf(c_27895,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_19243,c_76]) ).
tcf(c_27896,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_19243,c_75]) ).
tcf(c_27897,plain,
~ sameside(iPr_def_12,iPr_def_11,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_19243,c_133]) ).
tcf(c_27898,plain,
s_col(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_12),
inference(superposition,[status(thm)],[c_19243,c_191]) ).
tcf(c_27899,plain,
s_col(s(iPr_def_10,iPr_def_12),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_19243,c_190]) ).
tcf(c_27901,plain,
s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_19243,c_73]) ).
tcf(c_28768,plain,
( sameside(iPr_def_10,s(iPr_def_10,iPr_def_12),iPr_def_11)
| s_t(iPr_def_10,s(iPr_def_10,iPr_def_12),iPr_def_11) ),
inference(superposition,[status(thm)],[c_21167,c_134]) ).
tcf(c_28769,plain,
s_col(iPr_def_10,iPr_def_11,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_21167,c_98]) ).
tcf(c_28771,plain,
s_col(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_10),
inference(superposition,[status(thm)],[c_21167,c_96]) ).
tcf(c_28853,plain,
( sameside(s(iPr_def_10,iPr_def_12),iPr_def_11,iPr_def_10)
| s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,iPr_def_10) ),
inference(superposition,[status(thm)],[c_21168,c_134]) ).
tcf(c_28862,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_12,iPr_def_11,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_16109,c_98]) ).
tcf(c_28863,plain,
! [X0: $i,X1: $i] : s_col(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_16109,c_97]) ).
tcf(c_28864,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_11,ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_12),
inference(superposition,[status(thm)],[c_16109,c_96]) ).
tcf(c_28884,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(ext(iPr_def_10,iPr_def_12,X1,X2),X0,iPr_def_11)
| ~ s_t(iPr_def_12,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_16112,c_79]) ).
tcf(c_28885,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_12,iPr_def_11,X2)
| ~ s_t(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11,X2) ),
inference(superposition,[status(thm)],[c_16112,c_77]) ).
tcf(c_28886,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(ext(iPr_def_10,iPr_def_12,X1,X2),iPr_def_12,X0)
| ~ s_t(iPr_def_12,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_16112,c_76]) ).
tcf(c_28888,plain,
! [X0: $i,X1: $i] : ~ sameside(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_16112,c_133]) ).
tcf(c_29489,plain,
s_t(sK0,sK2,sK2),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_29566,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_11,iPr_def_10,X2)
| ~ s_t(iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1),X2) ),
inference(superposition,[status(thm)],[c_16133,c_80]) ).
tcf(c_29569,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_11,iPr_def_10,X0)
| ~ s_t(iPr_def_10,X0,ext(iPr_def_12,iPr_def_10,X1,X2)) ),
inference(superposition,[status(thm)],[c_16133,c_76]) ).
tcf(c_29570,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_10,iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1)) ),
inference(superposition,[status(thm)],[c_16133,c_75]) ).
tcf(c_29571,plain,
! [X0: $i,X1: $i] : ~ sameside(iPr_def_11,iPr_def_10,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_16133,c_133]) ).
tcf(c_29572,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_10,ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_11),
inference(superposition,[status(thm)],[c_16133,c_191]) ).
tcf(c_29573,plain,
! [X0: $i,X1: $i] : s_col(ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_16133,c_190]) ).
tcf(c_29574,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_11,iPr_def_10,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_16133,c_189]) ).
tcf(c_29575,plain,
! [X0: $i,X1: $i] : s_t(ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_16133,c_73]) ).
tcf(c_29764,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_11,iPr_def_10,ext(iPr_def_10,iPr_def_12,X0,X1)),
inference(superposition,[status(thm)],[c_18691,c_98]) ).
tcf(c_29765,plain,
! [X0: $i,X1: $i] : s_col(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_18691,c_97]) ).
tcf(c_29766,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_10,ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11),
inference(superposition,[status(thm)],[c_18691,c_96]) ).
tcf(c_29861,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X3,X3,X1,X2)
| ~ s_e(X0,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_66,c_50]) ).
tcf(c_29865,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,s(X0,X1),X2,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_8993,c_50]) ).
tcf(c_29866,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_10,X0,X1)
| ~ s_e(sK3,sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_9567,c_50]) ).
tcf(c_29867,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_11,X0,X1)
| ~ s_e(sK3,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_9569,c_50]) ).
tcf(c_29868,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_12,X0,X1)
| ~ s_e(sK3,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_9571,c_50]) ).
tcf(c_29869,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK0,X0,X1)
| ~ s_e(sK3,iPr_def_10,X0,X1) ),
inference(superposition,[status(thm)],[c_9573,c_50]) ).
tcf(c_29870,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK1,X0,X1)
| ~ s_e(sK3,iPr_def_11,X0,X1) ),
inference(superposition,[status(thm)],[c_9574,c_50]) ).
tcf(c_29871,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK2,X0,X1)
| ~ s_e(sK3,iPr_def_12,X0,X1) ),
inference(superposition,[status(thm)],[c_9575,c_50]) ).
tcf(c_29872,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_10,X0,X1)
| ~ s_e(sK0,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11526,c_50]) ).
tcf(c_29873,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_11,X0,X1)
| ~ s_e(sK1,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11527,c_50]) ).
tcf(c_29874,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,iPr_def_12,X0,X1)
| ~ s_e(sK2,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11528,c_50]) ).
tcf(c_29875,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK0,X0,X1)
| ~ s_e(iPr_def_10,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11529,c_50]) ).
tcf(c_29876,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK1,X0,X1)
| ~ s_e(iPr_def_11,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11530,c_50]) ).
tcf(c_29877,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,sK3,X0,X1)
| ~ s_e(sK3,sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_11758,c_50]) ).
tcf(c_29878,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_11,sK3,X0,X1)
| ~ s_e(sK3,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_11759,c_50]) ).
tcf(c_29879,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_12,sK3,X0,X1)
| ~ s_e(sK3,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_11760,c_50]) ).
tcf(c_29880,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,sK3,X0,X1)
| ~ s_e(sK3,iPr_def_10,X0,X1) ),
inference(superposition,[status(thm)],[c_11761,c_50]) ).
tcf(c_29881,plain,
! [X0: $i,X1: $i] :
( s_e(sK1,sK3,X0,X1)
| ~ s_e(sK3,iPr_def_11,X0,X1) ),
inference(superposition,[status(thm)],[c_11762,c_50]) ).
tcf(c_29882,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,sK3,X0,X1)
| ~ s_e(sK0,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11952,c_50]) ).
tcf(c_29883,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_11,sK3,X0,X1)
| ~ s_e(sK1,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11953,c_50]) ).
tcf(c_29884,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_12,sK3,X0,X1)
| ~ s_e(sK2,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11954,c_50]) ).
tcf(c_29885,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,sK3,X0,X1)
| ~ s_e(iPr_def_10,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11955,c_50]) ).
tcf(c_29886,plain,
! [X0: $i,X1: $i] :
( s_e(sK1,sK3,X0,X1)
| ~ s_e(iPr_def_11,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_11956,c_50]) ).
tcf(c_29887,plain,
! [X0: $i,X1: $i] :
( s_e(sK2,sK3,X0,X1)
| ~ s_e(iPr_def_12,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_12202,c_50]) ).
tcf(c_29888,plain,
! [X0: $i,X1: $i] :
( s_e(sK2,sK3,X0,X1)
| ~ s_e(sK3,iPr_def_12,X0,X1) ),
inference(superposition,[status(thm)],[c_12203,c_50]) ).
tcf(c_29889,plain,
! [X0: $i,X1: $i] :
( s_e(sK3,sK2,X0,X1)
| ~ s_e(iPr_def_12,sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_12204,c_50]) ).
tcf(c_30138,plain,
! [X0: $i] :
( s_t(sK0,sK1,sK2)
| ~ s_t(sK0,X0,sK2)
| ( sK2 != sK2 )
| ( sK1 != X0 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_8988]) ).
tcf(c_30139,plain,
sK2 = sK2,
inference(instantiation,[status(thm)],[c_3895]) ).
tcf(c_31433,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_e(X0,X1,X2,X3)
| ~ s_e(X0,s(X0,X1),X2,X3) ),
inference(superposition,[status(thm)],[c_8993,c_63]) ).
tcf(c_32068,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),iPr_def_10,X0)
| ~ s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_21170,c_80]) ).
tcf(c_32069,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),X0,iPr_def_11)
| ~ s_t(iPr_def_10,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_21170,c_79]) ).
tcf(c_32070,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ~ s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_21170,c_77]) ).
tcf(c_32071,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),iPr_def_10,X0)
| ~ s_t(iPr_def_10,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_21170,c_76]) ).
tcf(c_32072,plain,
( ( s(iPr_def_10,iPr_def_12) = iPr_def_10 )
| ~ s_t(iPr_def_10,s(iPr_def_10,iPr_def_12),iPr_def_11) ),
inference(superposition,[status(thm)],[c_21170,c_75]) ).
tcf(c_32073,plain,
~ sameside(s(iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_21170,c_133]) ).
tcf(c_32088,plain,
( sameside(iPr_def_11,iPr_def_10,s(iPr_def_12,iPr_def_10))
| s_t(iPr_def_11,iPr_def_10,s(iPr_def_12,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_23385,c_134]) ).
tcf(c_32131,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(ext(iPr_def_10,iPr_def_12,X1,X2),X0,iPr_def_10)
| ~ s_t(iPr_def_11,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18694,c_79]) ).
tcf(c_32132,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_11,iPr_def_10,X2)
| ~ s_t(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_10,X2) ),
inference(superposition,[status(thm)],[c_18694,c_77]) ).
tcf(c_32133,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(ext(iPr_def_10,iPr_def_12,X1,X2),iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_18694,c_76]) ).
tcf(c_32135,plain,
! [X0: $i,X1: $i] : ~ sameside(ext(iPr_def_10,iPr_def_12,X0,X1),iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_18694,c_133]) ).
tcf(c_32210,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_12,iPr_def_11,X2)
| ~ s_t(iPr_def_12,ext(iPr_def_12,iPr_def_10,X0,X1),X2) ),
inference(superposition,[status(thm)],[c_19238,c_80]) ).
tcf(c_32213,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,ext(iPr_def_12,iPr_def_10,X1,X2)) ),
inference(superposition,[status(thm)],[c_19238,c_76]) ).
tcf(c_32214,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,ext(iPr_def_12,iPr_def_10,X0,X1)) ),
inference(superposition,[status(thm)],[c_19238,c_75]) ).
tcf(c_32215,plain,
! [X0: $i,X1: $i] : ~ sameside(iPr_def_12,iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_19238,c_133]) ).
tcf(c_32216,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_12),
inference(superposition,[status(thm)],[c_19238,c_191]) ).
tcf(c_32217,plain,
! [X0: $i,X1: $i] : s_col(ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_19238,c_190]) ).
tcf(c_32218,plain,
! [X0: $i,X1: $i] : s_col(iPr_def_12,iPr_def_11,ext(iPr_def_12,iPr_def_10,X0,X1)),
inference(superposition,[status(thm)],[c_19238,c_189]) ).
tcf(c_32219,plain,
! [X0: $i,X1: $i] : s_t(ext(iPr_def_12,iPr_def_10,X0,X1),iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_19238,c_73]) ).
tcf(c_32391,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X2,s(X0,X1),X0)
| ~ s_t(X0,s(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_14196,c_14188]) ).
tcf(c_32398,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ s_t(X0,X2,X1)
| ~ sameside(s(X0,X1),X0,X2) ),
inference(superposition,[status(thm)],[c_14196,c_133]) ).
tcf(c_32399,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,s(X0,X2))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14196,c_191]) ).
tcf(c_32400,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,s(X0,X2),X0)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14196,c_190]) ).
tcf(c_32401,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(s(X0,X2),X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14196,c_189]) ).
tcf(c_32402,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X1,X0,s(X0,X2))
| ~ s_t(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14196,c_73]) ).
tcf(c_33047,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X2,X2,X0,X1)
| ~ le(X0,X1,X2,X2) ),
inference(superposition,[status(thm)],[c_119,c_117]) ).
tcf(c_33430,plain,
! [X0: $i,X1: $i] :
( sameside(X1,X0,X1)
| ( X0 = xb )
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_72,c_203]) ).
tcf(c_33436,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_11 )
| ( xb = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_3893,c_203]) ).
tcf(c_33438,plain,
( sameside(iPr_def_11,iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 )
| ( xb = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_8489,c_203]) ).
tcf(c_33441,plain,
( sameside(sK3,sK0,iPr_def_10)
| ( sK0 = xb )
| ( sK0 = sK3 ) ),
inference(superposition,[status(thm)],[c_10064,c_203]) ).
tcf(c_33442,plain,
( sameside(sK3,sK1,iPr_def_11)
| ( sK1 = xb )
| ( sK1 = sK3 ) ),
inference(superposition,[status(thm)],[c_10065,c_203]) ).
tcf(c_33443,plain,
( sameside(sK3,sK2,iPr_def_12)
| ( sK2 = xb )
| ( sK2 = sK3 ) ),
inference(superposition,[status(thm)],[c_10066,c_203]) ).
tcf(c_33444,plain,
( sameside(sK3,iPr_def_10,sK0)
| ( xb = iPr_def_10 )
| ( sK3 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_10067,c_203]) ).
tcf(c_33445,plain,
( sameside(sK3,iPr_def_11,sK1)
| ( xb = iPr_def_11 )
| ( sK3 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_10068,c_203]) ).
tcf(c_33446,plain,
( sameside(sK3,iPr_def_12,sK2)
| ( xb = iPr_def_12 )
| ( sK3 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_10069,c_203]) ).
tcf(c_34596,plain,
( sameside(iPr_def_10,s(iPr_def_12,iPr_def_10),iPr_def_11)
| s_t(iPr_def_10,s(iPr_def_12,iPr_def_10),iPr_def_11) ),
inference(superposition,[status(thm)],[c_23387,c_134]) ).
tcf(c_34787,plain,
( sameside(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_12)
| s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_12) ),
inference(superposition,[status(thm)],[c_27898,c_134]) ).
tcf(c_34788,plain,
s_col(iPr_def_11,iPr_def_12,s(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_27898,c_98]) ).
tcf(c_34790,plain,
s_col(iPr_def_12,s(iPr_def_10,iPr_def_12),iPr_def_11),
inference(superposition,[status(thm)],[c_27898,c_96]) ).
tcf(c_34837,plain,
( sameside(s(iPr_def_10,iPr_def_12),iPr_def_12,iPr_def_11)
| s_t(s(iPr_def_10,iPr_def_12),iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_27899,c_134]) ).
tcf(c_34890,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_11 ) ),
inference(global_subsumption_just,[status(thm)],[c_33436,c_10224]) ).
tcf(c_34896,plain,
! [X0: $i] :
( sameside(iPr_def_11,iPr_def_10,X0)
| ( iPr_def_10 = iPr_def_11 )
| ~ sameside(iPr_def_12,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_34890,c_137]) ).
tcf(c_34898,plain,
( sameside(iPr_def_12,iPr_def_10,iPr_def_11)
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_34890,c_136]) ).
tcf(c_35139,plain,
! [X0: $i] :
( sameside(iPr_def_12,iPr_def_10,X0)
| ( iPr_def_10 = iPr_def_11 )
| ~ sameside(iPr_def_11,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_34898,c_137]) ).
tcf(c_35341,plain,
( sameside(iPr_def_11,iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(global_subsumption_just,[status(thm)],[c_33438,c_10252]) ).
tcf(c_35347,plain,
! [X0: $i] :
( sameside(iPr_def_11,iPr_def_12,X0)
| ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_35341,c_137]) ).
tcf(c_35349,plain,
( sameside(iPr_def_10,iPr_def_12,iPr_def_11)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_35341,c_136]) ).
tcf(c_35362,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_12 )
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_135,c_34896]) ).
tcf(c_35364,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_11)
| s_t(iPr_def_11,iPr_def_10,iPr_def_12)
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_13615,c_34896]) ).
tcf(c_35365,plain,
( sameside(iPr_def_11,iPr_def_10,iPr_def_11)
| s_t(iPr_def_12,iPr_def_10,iPr_def_11)
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_12831,c_34896]) ).
tcf(c_35598,plain,
! [X0: $i] :
( sameside(iPr_def_10,iPr_def_12,X0)
| ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_11,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_35349,c_137]) ).
tcf(c_35617,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_11,iPr_def_12,ext(iPr_def_11,s(iPr_def_12,iPr_def_10),X0,X1)),
inference(superposition,[status(thm)],[c_52,c_16916]) ).
tcf(c_35622,plain,
s_t(iPr_def_11,iPr_def_12,s(s(iPr_def_12,iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_10062,c_16916]) ).
tcf(c_35633,plain,
! [X0: $i,X1: $i] : s_t(iPr_def_10,iPr_def_11,ext(iPr_def_10,s(iPr_def_12,iPr_def_10),X0,X1)),
inference(superposition,[status(thm)],[c_52,c_18569]) ).
tcf(c_35638,plain,
s_t(iPr_def_10,iPr_def_11,s(s(iPr_def_12,iPr_def_10),iPr_def_10)),
inference(superposition,[status(thm)],[c_10062,c_18569]) ).
tcf(c_35887,plain,
! [X0: $i,X1: $i] :
( sameside(X1,X0,X1)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_72,c_204]) ).
tcf(c_35893,plain,
( sameside(iPr_def_12,iPr_def_10,iPr_def_11)
| ( iPr_def_10 = iPr_def_12 )
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_3893,c_204]) ).
tcf(c_35898,plain,
( sameside(iPr_def_10,sK0,sK3)
| ( sK0 = iPr_def_10 )
| ( sK0 = sK3 ) ),
inference(superposition,[status(thm)],[c_10064,c_204]) ).
tcf(c_35899,plain,
( sameside(iPr_def_11,sK1,sK3)
| ( sK1 = iPr_def_11 )
| ( sK1 = sK3 ) ),
inference(superposition,[status(thm)],[c_10065,c_204]) ).
tcf(c_35900,plain,
( sameside(iPr_def_12,sK2,sK3)
| ( sK2 = iPr_def_12 )
| ( sK2 = sK3 ) ),
inference(superposition,[status(thm)],[c_10066,c_204]) ).
tcf(c_35901,plain,
( sameside(sK0,iPr_def_10,sK3)
| ( sK3 = iPr_def_10 )
| ( sK0 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_10067,c_204]) ).
tcf(c_35902,plain,
( sameside(sK1,iPr_def_11,sK3)
| ( sK3 = iPr_def_11 )
| ( sK1 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_10068,c_204]) ).
tcf(c_35903,plain,
( sameside(sK2,iPr_def_12,sK3)
| ( sK3 = iPr_def_12 )
| ( sK2 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_10069,c_204]) ).
tcf(c_37604,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_12,X0)
| ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_3893,c_78]) ).
tcf(c_37606,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_10,X0)
| ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_8489,c_78]) ).
tcf(c_37609,plain,
! [X0: $i] :
( s_t(sK0,iPr_def_10,X0)
| ( sK3 = iPr_def_10 )
| ~ s_t(sK3,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_10064,c_78]) ).
tcf(c_37610,plain,
! [X0: $i] :
( s_t(sK1,iPr_def_11,X0)
| ( sK3 = iPr_def_11 )
| ~ s_t(sK3,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_10065,c_78]) ).
tcf(c_37611,plain,
! [X0: $i] :
( s_t(sK2,iPr_def_12,X0)
| ( sK3 = iPr_def_12 )
| ~ s_t(sK3,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_10066,c_78]) ).
tcf(c_37612,plain,
! [X0: $i] :
( s_t(iPr_def_10,sK0,X0)
| ( sK0 = sK3 )
| ~ s_t(sK3,sK0,X0) ),
inference(superposition,[status(thm)],[c_10067,c_78]) ).
tcf(c_37613,plain,
! [X0: $i] :
( s_t(iPr_def_11,sK1,X0)
| ( sK1 = sK3 )
| ~ s_t(sK3,sK1,X0) ),
inference(superposition,[status(thm)],[c_10068,c_78]) ).
tcf(c_37614,plain,
! [X0: $i] :
( s_t(iPr_def_12,sK2,X0)
| ( sK2 = sK3 )
| ~ s_t(sK3,sK2,X0) ),
inference(superposition,[status(thm)],[c_10069,c_78]) ).
tcf(c_38802,plain,
! [X0: $i] :
( s_t(iPr_def_10,iPr_def_11,X0)
| ( iPr_def_11 = iPr_def_12 )
| ~ s_t(iPr_def_11,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_3893,c_81]) ).
tcf(c_38804,plain,
! [X0: $i] :
( s_t(iPr_def_12,iPr_def_11,X0)
| ( iPr_def_10 = iPr_def_11 )
| ~ s_t(iPr_def_11,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_8489,c_81]) ).
tcf(c_38807,plain,
! [X0: $i] :
( s_t(sK0,sK3,X0)
| ( sK3 = iPr_def_10 )
| ~ s_t(sK3,iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_10064,c_81]) ).
tcf(c_38808,plain,
! [X0: $i] :
( s_t(sK1,sK3,X0)
| ( sK3 = iPr_def_11 )
| ~ s_t(sK3,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_10065,c_81]) ).
tcf(c_38809,plain,
! [X0: $i] :
( s_t(sK2,sK3,X0)
| ( sK3 = iPr_def_12 )
| ~ s_t(sK3,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_10066,c_81]) ).
tcf(c_38810,plain,
! [X0: $i] :
( s_t(iPr_def_10,sK3,X0)
| ( sK0 = sK3 )
| ~ s_t(sK3,sK0,X0) ),
inference(superposition,[status(thm)],[c_10067,c_81]) ).
tcf(c_38811,plain,
! [X0: $i] :
( s_t(iPr_def_11,sK3,X0)
| ( sK1 = sK3 )
| ~ s_t(sK3,sK1,X0) ),
inference(superposition,[status(thm)],[c_10068,c_81]) ).
tcf(c_38812,plain,
! [X0: $i] :
( s_t(iPr_def_12,sK3,X0)
| ( sK2 = sK3 )
| ~ s_t(sK3,sK2,X0) ),
inference(superposition,[status(thm)],[c_10069,c_81]) ).
tcf(c_40236,plain,
! [X0: $i] :
( s_t(sK0,sK3,X0)
| s_t(sK0,X0,sK3)
| ~ s_t(sK0,X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_10064,c_109]) ).
tcf(c_40237,plain,
! [X0: $i] :
( s_t(sK1,sK3,X0)
| s_t(sK1,X0,sK3)
| ~ s_t(sK1,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_10065,c_109]) ).
tcf(c_40238,plain,
! [X0: $i] :
( s_t(sK2,sK3,X0)
| s_t(sK2,X0,sK3)
| ~ s_t(sK2,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10066,c_109]) ).
tcf(c_40239,plain,
! [X0: $i] :
( s_t(iPr_def_10,sK3,X0)
| s_t(iPr_def_10,X0,sK3)
| ~ s_t(iPr_def_10,X0,sK0) ),
inference(superposition,[status(thm)],[c_10067,c_109]) ).
tcf(c_40240,plain,
! [X0: $i] :
( s_t(iPr_def_11,sK3,X0)
| s_t(iPr_def_11,X0,sK3)
| ~ s_t(iPr_def_11,X0,sK1) ),
inference(superposition,[status(thm)],[c_10068,c_109]) ).
tcf(c_40241,plain,
! [X0: $i] :
( s_t(iPr_def_12,sK3,X0)
| s_t(iPr_def_12,X0,sK3)
| ~ s_t(iPr_def_12,X0,sK2) ),
inference(superposition,[status(thm)],[c_10069,c_109]) ).
tcf(c_41861,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,X0)
| ~ s_t(s(iPr_def_10,iPr_def_12),iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_27901,c_80]) ).
tcf(c_41862,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),X0,iPr_def_12)
| ~ s_t(iPr_def_11,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_27901,c_79]) ).
tcf(c_41863,plain,
! [X0: $i] :
( s_t(iPr_def_11,iPr_def_12,X0)
| ~ s_t(s(iPr_def_10,iPr_def_12),iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_27901,c_77]) ).
tcf(c_41864,plain,
! [X0: $i] :
( s_t(s(iPr_def_10,iPr_def_12),iPr_def_11,X0)
| ~ s_t(iPr_def_11,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_27901,c_76]) ).
tcf(c_41865,plain,
( ( s(iPr_def_10,iPr_def_12) = iPr_def_11 )
| ~ s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_12) ),
inference(superposition,[status(thm)],[c_27901,c_75]) ).
tcf(c_41866,plain,
~ sameside(s(iPr_def_10,iPr_def_12),iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_27901,c_133]) ).
tcf(c_42521,plain,
( sameside(iPr_def_10,iPr_def_11,s(iPr_def_10,iPr_def_12))
| s_t(iPr_def_10,iPr_def_11,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_28769,c_134]) ).
tcf(c_42537,plain,
( sameside(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_10)
| s_t(iPr_def_11,s(iPr_def_10,iPr_def_12),iPr_def_10) ),
inference(superposition,[status(thm)],[c_28771,c_134]) ).
tcf(c_42553,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_10,iPr_def_12,ext(iPr_def_11,iPr_def_12,X0,X1))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_52,c_37604]) ).
tcf(c_42558,plain,
( s_t(iPr_def_10,iPr_def_12,s(iPr_def_12,iPr_def_11))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_10062,c_37604]) ).
tcf(c_43347,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_10,iPr_def_11,ext(iPr_def_11,iPr_def_12,X0,X1))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_52,c_38802]) ).
tcf(c_43352,plain,
( s_t(iPr_def_10,iPr_def_11,s(iPr_def_12,iPr_def_11))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_10062,c_38802]) ).
tcf(c_43403,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_10,iPr_def_12,s(iPr_def_12,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_42558,c_133]) ).
tcf(c_43404,plain,
( s_col(iPr_def_12,s(iPr_def_12,iPr_def_11),iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42558,c_191]) ).
tcf(c_43405,plain,
( s_col(s(iPr_def_12,iPr_def_11),iPr_def_10,iPr_def_12)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42558,c_190]) ).
tcf(c_43406,plain,
( s_col(iPr_def_10,iPr_def_12,s(iPr_def_12,iPr_def_11))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42558,c_189]) ).
tcf(c_43407,plain,
( s_t(s(iPr_def_12,iPr_def_11),iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42558,c_73]) ).
tcf(c_44242,plain,
( ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_10,iPr_def_11,s(iPr_def_12,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_43352,c_133]) ).
tcf(c_44243,plain,
( s_col(iPr_def_11,s(iPr_def_12,iPr_def_11),iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43352,c_191]) ).
tcf(c_44244,plain,
( s_col(s(iPr_def_12,iPr_def_11),iPr_def_10,iPr_def_11)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43352,c_190]) ).
tcf(c_44245,plain,
( s_col(iPr_def_10,iPr_def_11,s(iPr_def_12,iPr_def_11))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43352,c_189]) ).
tcf(c_44246,plain,
( s_t(s(iPr_def_12,iPr_def_11),iPr_def_11,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43352,c_73]) ).
tcf(c_45396,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_10,iPr_def_12,ext(iPr_def_11,iPr_def_12,X0,X1)) ),
inference(superposition,[status(thm)],[c_42553,c_133]) ).
tcf(c_45397,plain,
! [X0: $i,X1: $i] :
( s_col(iPr_def_12,ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42553,c_191]) ).
tcf(c_45398,plain,
! [X0: $i,X1: $i] :
( s_col(ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_10,iPr_def_12)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42553,c_190]) ).
tcf(c_45399,plain,
! [X0: $i,X1: $i] :
( s_col(iPr_def_10,iPr_def_12,ext(iPr_def_11,iPr_def_12,X0,X1))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42553,c_189]) ).
tcf(c_45400,plain,
! [X0: $i,X1: $i] :
( s_t(ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_12,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_42553,c_73]) ).
tcf(c_45610,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_11 = iPr_def_12 )
| ~ sameside(iPr_def_10,iPr_def_11,ext(iPr_def_11,iPr_def_12,X0,X1)) ),
inference(superposition,[status(thm)],[c_43347,c_133]) ).
tcf(c_45611,plain,
! [X0: $i,X1: $i] :
( s_col(iPr_def_11,ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43347,c_191]) ).
tcf(c_45612,plain,
! [X0: $i,X1: $i] :
( s_col(ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_10,iPr_def_11)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43347,c_190]) ).
tcf(c_45613,plain,
! [X0: $i,X1: $i] :
( s_col(iPr_def_10,iPr_def_11,ext(iPr_def_11,iPr_def_12,X0,X1))
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43347,c_189]) ).
tcf(c_45614,plain,
! [X0: $i,X1: $i] :
( s_t(ext(iPr_def_11,iPr_def_12,X0,X1),iPr_def_11,iPr_def_10)
| ( iPr_def_11 = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_43347,c_73]) ).
tcf(c_50654,plain,
( sameside(iPr_def_11,iPr_def_12,s(iPr_def_10,iPr_def_12))
| s_t(iPr_def_11,iPr_def_12,s(iPr_def_10,iPr_def_12)) ),
inference(superposition,[status(thm)],[c_34788,c_134]) ).
tcf(c_50670,plain,
( sameside(iPr_def_12,s(iPr_def_10,iPr_def_12),iPr_def_11)
| s_t(iPr_def_12,s(iPr_def_10,iPr_def_12),iPr_def_11) ),
inference(superposition,[status(thm)],[c_34790,c_134]) ).
tcf(c_50678,plain,
! [X0: $i] : s_e(sK0,s(sK3,X0),iPr_def_10,X0),
inference(superposition,[status(thm)],[c_161,c_8994]) ).
tcf(c_50682,plain,
s_e(sK0,sK1,iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_8167,c_8994]) ).
tcf(c_50684,plain,
s_e(sK0,sK2,iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_8248,c_8994]) ).
tcf(c_50687,plain,
s_e(sK0,iPr_def_11,iPr_def_10,sK1),
inference(superposition,[status(thm)],[c_7818,c_8994]) ).
tcf(c_50688,plain,
s_e(sK0,iPr_def_12,iPr_def_10,sK2),
inference(superposition,[status(thm)],[c_7941,c_8994]) ).
tcf(c_50689,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(sK0,X0,X1,X2)
| ~ s_e(iPr_def_10,s(sK3,X0),X1,X2) ),
inference(superposition,[status(thm)],[c_8994,c_63]) ).
tcf(c_50690,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(iPr_def_10,s(sK3,X0),X1,X2)
| ~ s_e(sK0,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8994,c_50]) ).
tcf(c_50691,plain,
! [X0: $i,X1: $i] :
( le(sK0,X0,iPr_def_10,X1)
| ~ s_t(iPr_def_10,s(sK3,X0),X1) ),
inference(superposition,[status(thm)],[c_8994,c_199]) ).
tcf(c_50692,plain,
! [X0: $i,X1: $i] :
( le(sK0,X0,iPr_def_10,s(sK3,X1))
| ~ s_t(sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_8994,c_113]) ).
tcf(c_50694,plain,
! [X0: $i] : s_e(sK0,X0,s(sK3,X0),iPr_def_10),
inference(superposition,[status(thm)],[c_8994,c_65]) ).
tcf(c_50695,plain,
! [X0: $i] : s_e(X0,sK0,iPr_def_10,s(sK3,X0)),
inference(superposition,[status(thm)],[c_8994,c_64]) ).
tcf(c_50696,plain,
! [X0: $i] : s_e(iPr_def_10,s(sK3,X0),sK0,X0),
inference(superposition,[status(thm)],[c_8994,c_62]) ).
tcf(c_51135,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_12,iPr_def_10,ext(iPr_def_11,iPr_def_10,X0,X1))
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_52,c_37606]) ).
tcf(c_51140,plain,
( s_t(iPr_def_12,iPr_def_10,s(iPr_def_10,iPr_def_11))
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_10062,c_37606]) ).
tcf(c_51384,plain,
! [X0: $i,X1: $i] :
( s_t(iPr_def_12,iPr_def_11,ext(iPr_def_11,iPr_def_10,X0,X1))
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_52,c_38804]) ).
tcf(c_51389,plain,
( s_t(iPr_def_12,iPr_def_11,s(iPr_def_10,iPr_def_11))
| ( iPr_def_10 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_10062,c_38804]) ).
tcf(c_56165,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,sK1,X0,X1)
| ~ s_e(iPr_def_10,iPr_def_11,X0,X1) ),
inference(superposition,[status(thm)],[c_50682,c_63]) ).
tcf(c_56166,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,iPr_def_11,X0,X1)
| ~ s_e(sK0,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_50682,c_50]) ).
tcf(c_56167,plain,
! [X0: $i] :
( le(sK0,sK1,iPr_def_10,X0)
| ~ s_t(iPr_def_10,iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_50682,c_199]) ).
tcf(c_56168,plain,
! [X0: $i] :
( le(sK0,X0,iPr_def_10,iPr_def_11)
| ~ s_t(sK0,X0,sK1) ),
inference(superposition,[status(thm)],[c_50682,c_113]) ).
tcf(c_56169,plain,
s_e(sK1,sK0,iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_50682,c_70]) ).
tcf(c_56170,plain,
s_e(sK0,sK1,iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_50682,c_65]) ).
tcf(c_56171,plain,
s_e(sK1,sK0,iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_50682,c_64]) ).
tcf(c_56172,plain,
s_e(iPr_def_10,iPr_def_11,sK0,sK1),
inference(superposition,[status(thm)],[c_50682,c_62]) ).
tcf(c_56764,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,sK2,X0,X1)
| ~ s_e(iPr_def_10,iPr_def_12,X0,X1) ),
inference(superposition,[status(thm)],[c_50684,c_63]) ).
tcf(c_56765,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,iPr_def_12,X0,X1)
| ~ s_e(sK0,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_50684,c_50]) ).
tcf(c_56766,plain,
! [X0: $i] :
( le(sK0,sK2,iPr_def_10,X0)
| ~ s_t(iPr_def_10,iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_50684,c_199]) ).
tcf(c_56767,plain,
! [X0: $i] :
( le(sK0,X0,iPr_def_10,iPr_def_12)
| ~ s_t(sK0,X0,sK2) ),
inference(superposition,[status(thm)],[c_50684,c_113]) ).
tcf(c_56768,plain,
s_e(sK2,sK0,iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_50684,c_70]) ).
tcf(c_56769,plain,
s_e(sK0,sK2,iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_50684,c_65]) ).
tcf(c_56770,plain,
s_e(sK2,sK0,iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_50684,c_64]) ).
tcf(c_56771,plain,
s_e(iPr_def_10,iPr_def_12,sK0,sK2),
inference(superposition,[status(thm)],[c_50684,c_62]) ).
tcf(c_57205,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,iPr_def_11,X0,X1)
| ~ s_e(iPr_def_10,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_50687,c_63]) ).
tcf(c_57206,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,sK1,X0,X1)
| ~ s_e(sK0,iPr_def_11,X0,X1) ),
inference(superposition,[status(thm)],[c_50687,c_50]) ).
tcf(c_57207,plain,
! [X0: $i] :
( le(sK0,iPr_def_11,iPr_def_10,X0)
| ~ s_t(iPr_def_10,sK1,X0) ),
inference(superposition,[status(thm)],[c_50687,c_199]) ).
tcf(c_57208,plain,
! [X0: $i] :
( le(sK0,X0,iPr_def_10,sK1)
| ~ s_t(sK0,X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_50687,c_113]) ).
tcf(c_57209,plain,
s_e(iPr_def_11,sK0,sK1,iPr_def_10),
inference(superposition,[status(thm)],[c_50687,c_70]) ).
tcf(c_57210,plain,
s_e(sK0,iPr_def_11,sK1,iPr_def_10),
inference(superposition,[status(thm)],[c_50687,c_65]) ).
tcf(c_57211,plain,
s_e(iPr_def_11,sK0,iPr_def_10,sK1),
inference(superposition,[status(thm)],[c_50687,c_64]) ).
tcf(c_57212,plain,
s_e(iPr_def_10,sK1,sK0,iPr_def_11),
inference(superposition,[status(thm)],[c_50687,c_62]) ).
tcf(c_57403,plain,
! [X0: $i,X1: $i] :
( s_e(sK0,iPr_def_12,X0,X1)
| ~ s_e(iPr_def_10,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_50688,c_63]) ).
tcf(c_57404,plain,
! [X0: $i,X1: $i] :
( s_e(iPr_def_10,sK2,X0,X1)
| ~ s_e(sK0,iPr_def_12,X0,X1) ),
inference(superposition,[status(thm)],[c_50688,c_50]) ).
tcf(c_57405,plain,
! [X0: $i] :
( le(sK0,iPr_def_12,iPr_def_10,X0)
| ~ s_t(iPr_def_10,sK2,X0) ),
inference(superposition,[status(thm)],[c_50688,c_199]) ).
tcf(c_57406,plain,
! [X0: $i] :
( le(sK0,X0,iPr_def_10,sK2)
| ~ s_t(sK0,X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_50688,c_113]) ).
tcf(c_57407,plain,
s_e(iPr_def_12,sK0,sK2,iPr_def_10),
inference(superposition,[status(thm)],[c_50688,c_70]) ).
tcf(c_57408,plain,
s_e(sK0,iPr_def_12,sK2,iPr_def_10),
inference(superposition,[status(thm)],[c_50688,c_65]) ).
tcf(c_57409,plain,
s_e(iPr_def_12,sK0,iPr_def_10,sK2),
inference(superposition,[status(thm)],[c_50688,c_64]) ).
tcf(c_57410,plain,
s_e(iPr_def_10,sK2,sK0,iPr_def_12),
inference(superposition,[status(thm)],[c_50688,c_62]) ).
tcf(c_94530,plain,
( s_t(sK0,sK1,sK2)
| ~ s_t(sK0,sK2,sK2)
| ( sK2 != sK2 )
| ( sK1 != sK2 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_30138]) ).
tcf(c_133606,plain,
iPr_def_11 != iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_12800,c_168,c_6365,c_8989,c_29489,c_30139,c_94530]) ).
tcf(c_198077,plain,
s(sK3,iPr_def_10) = sK0,
inference(unflattening,[status(thm)],[c_8766]) ).
tcf(c_198078,plain,
s(sK3,iPr_def_11) = sK1,
inference(unflattening,[status(thm)],[c_8768]) ).
tcf(c_198079,plain,
s(sK3,iPr_def_12) = sK2,
inference(unflattening,[status(thm)],[c_8770]) ).
tcf(c_198080,plain,
s(sK3,sK0) = iPr_def_10,
inference(unflattening,[status(thm)],[c_8772]) ).
tcf(c_198081,plain,
s(sK3,sK1) = iPr_def_11,
inference(unflattening,[status(thm)],[c_8773]) ).
tcf(c_198082,plain,
s(sK3,sK2) = iPr_def_12,
inference(unflattening,[status(thm)],[c_8774]) ).
tcf(c_198092,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_133606,c_57410,c_57409,c_57408,c_57407,c_57406,c_57405,c_57404,c_57403,c_57212,c_57211,c_57210,c_57209,c_57208,c_57207,c_57206,c_57205,c_56771,c_56770,c_56769,c_56768,c_56767,c_56766,c_56765,c_56764,c_56172,c_56171,c_56170,c_56169,c_56168,c_56167,c_56166,c_56165,c_51389,c_51384,c_51140,c_51135,c_50696,c_50695,c_50694,c_50692,c_50691,c_50690,c_50689,c_50678,c_50670,c_50654,c_45614,c_45613,c_45612,c_45611,c_45610,c_45400,c_45399,c_45398,c_45397,c_45396,c_44246,c_44245,c_44244,c_44243,c_44242,c_43407,c_43406,c_43405,c_43404,c_43403,c_42537,c_42521,c_41866,c_41865,c_41864,c_41863,c_41862,c_41861,c_40241,c_40240,c_40239,c_40238,c_40237,c_40236,c_38812,c_38811,c_38810,c_38809,c_38808,c_38807,c_37614,c_37613,c_37612,c_37611,c_37610,c_37609,c_35903,c_35902,c_35901,c_35900,c_35899,c_35898,c_35893,c_35887,c_35638,c_35633,c_35622,c_35617,c_35598,c_35365,c_35364,c_35362,c_35347,c_35139,c_34837,c_34787,c_34596,c_33446,c_33445,c_33444,c_33443,c_33442,c_33441,c_33438,c_33436,c_33430,c_33047,c_32402,c_32401,c_32400,c_32399,c_32398,c_32391,c_32219,c_32218,c_32217,c_32216,c_32215,c_32214,c_32213,c_32210,c_32135,c_32133,c_32132,c_32131,c_32088,c_32073,c_32072,c_32071,c_32070,c_32069,c_32068,c_31433,c_29889,c_29888,c_29887,c_29886,c_29885,c_29884,c_29883,c_29882,c_29881,c_29880,c_29879,c_29878,c_29877,c_29876,c_29875,c_29874,c_29873,c_29872,c_29871,c_29870,c_29869,c_29868,c_29867,c_29866,c_29865,c_29861,c_29766,c_29765,c_29764,c_29575,c_29574,c_29573,c_29572,c_29571,c_29570,c_29569,c_29566,c_28888,c_28886,c_28885,c_28884,c_28864,c_28863,c_28862,c_28853,c_28768,c_27897,c_27896,c_27895,c_27894,c_27893,c_27892,c_27884,c_26856,c_26855,c_26854,c_26853,c_26852,c_26851,c_26850,c_26849,c_26848,c_26847,c_26846,c_26845,c_26844,c_26843,c_26842,c_26841,c_26840,c_26839,c_26838,c_26837,c_26836,c_26835,c_26834,c_26833,c_26832,c_26825,c_25938,c_25937,c_25936,c_25935,c_25934,c_25933,c_25932,c_25931,c_25930,c_25929,c_25928,c_25927,c_25926,c_25925,c_25924,c_25923,c_25922,c_25921,c_25920,c_25919,c_25918,c_25917,c_25916,c_25915,c_25914,c_25910,c_25907,c_25496,c_24521,c_24520,c_24519,c_24518,c_24517,c_24515,c_24513,c_24511,c_24510,c_24508,c_24507,c_24506,c_24504,c_24502,c_24500,c_24499,c_24497,c_24496,c_24495,c_24493,c_24491,c_24489,c_24488,c_23802,c_23801,c_23800,c_23799,c_23558,c_23557,c_23556,c_23555,c_23554,c_23553,c_23392,c_23384,c_21868,c_21867,c_21866,c_21865,c_21864,c_21546,c_21545,c_21544,c_21543,c_21542,c_21519,c_21166,c_21165,c_21164,c_21163,c_21162,c_21161,c_20966,c_20965,c_20964,c_20963,c_20962,c_20961,c_20649,c_20648,c_20647,c_20646,c_20645,c_20644,c_20643,c_20134,c_20133,c_20132,c_20131,c_20130,c_20129,c_20128,c_20126,c_20078,c_20077,c_20076,c_20075,c_20074,c_19428,c_19427,c_19426,c_19425,c_19424,c_19242,c_19241,c_18690,c_18689,c_18688,c_18574,c_18573,c_18572,c_18131,c_18116,c_16914,c_16913,c_16912,c_16911,c_16910,c_16909,c_16907,c_16584,c_16583,c_16582,c_16581,c_16580,c_16579,c_16578,c_16570,c_16136,c_16135,c_16108,c_15686,c_15685,c_15628,c_15609,c_15573,c_15100,c_15099,c_15098,c_15097,c_15096,c_15095,c_15094,c_14202,c_14201,c_14068,c_14067,c_14066,c_14065,c_14064,c_14063,c_14061,c_14060,c_14058,c_13656,c_13655,c_13513,c_12851,c_12850,c_12848,c_12847,c_12845,c_12844,c_12842,c_12841,c_12839,c_12838,c_12836,c_12835,c_12827,c_12804,c_12802,c_12638,c_12637,c_12636,c_12635,c_12464,c_12463,c_12462,c_12461,c_12258,c_12257,c_12254,c_12252,c_11950,c_11946,c_11757,c_11756,c_11752,c_11525,c_11524,c_11523,c_11520,c_11510,c_11383,c_11382,c_11379,c_11363,c_11103,c_11050,c_11045,c_10843,c_10587,c_10582,c_10561,c_10379,c_10378,c_10377,c_10374,c_10354,c_9717,c_9716,c_9715,c_9713,c_9711,c_9709,c_9565,c_9367,c_9363,c_9357,c_9353,c_9183,c_9179,c_9013,c_9012,c_9011,c_9009,c_9007,c_9005,c_9004,c_9003,c_9002,c_9001,c_9000,c_8998,c_8996,c_8992,c_5628,c_8461,c_8460,c_8459,c_8457,c_8455,c_8453,c_198082,c_8249,c_198081,c_8168,c_198080,c_8123,c_198079,c_198078,c_198077,c_3893,c_3892,c_3891,c_3890,c_1971,c_1909,c_261,c_263,c_207,c_206,c_205,c_204,c_203,c_202,c_199,c_198,c_197,c_191,c_190,c_189,c_188,c_187,c_186,c_185,c_184,c_3894,c_167,c_166,c_165,c_164,c_163,c_161,c_160,c_159,c_158,c_157,c_156,c_155,c_154,c_153,c_152,c_151,c_148,c_147,c_145,c_143,c_141,c_140,c_138,c_137,c_136,c_135,c_134,c_133,c_132,c_130,c_129,c_128,c_201,c_200,c_125,c_131,c_123,c_122,c_119,c_118,c_117,c_116,c_115,c_114,c_113,c_112,c_111,c_110,c_109,c_108,c_107,c_106,c_105,c_104,c_102,c_101,c_100,c_99,c_98,c_97,c_96,c_95,c_94,c_93,c_92,c_91,c_90,c_88,c_87,c_86,c_84,c_83,c_82,c_81,c_80,c_79,c_78,c_77,c_76,c_75,c_74,c_73,c_72,c_71,c_70,c_68,c_67,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_54,c_53,c_52,c_69,c_50,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO499+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 12:18:41 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 47.62/11.23 % SZS status Started for theBenchmark.p
% 47.62/11.23 % SZS status Theorem for theBenchmark.p
% 47.62/11.23
% 47.62/11.23 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 47.62/11.23
% 47.62/11.23 % ------ iProver source info
% 47.62/11.23
% 47.62/11.23 % git: date: 2026-07-19 20:42:38 +0200
% 47.62/11.23 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 47.62/11.23 % git: non_committed_changes: false
% 47.62/11.23
% 47.62/11.23 % ------ Parsing...
% 47.62/11.23 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 47.62/11.23
% 47.62/11.23 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 47.62/11.23
% 47.62/11.23 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 47.62/11.23
% 47.62/11.23 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 47.62/11.23 % ------ Proving...
% 47.62/11.23 % ------ Problem Properties
% 47.62/11.23
% 47.62/11.23 %
% 47.62/11.23 % clauses 131
% 47.62/11.23 % conjectures 2
% 47.62/11.23 % EPR 99
% 47.62/11.23 % Horn 104
% 47.62/11.23 % unary 30
% 47.62/11.23 % binary 42
% 47.62/11.23 % lits 361
% 47.62/11.23 % lits eq 64
% 47.62/11.23 % fd_pure 0
% 47.62/11.23 % fd_pseudo 0
% 47.62/11.23 % fd_cond 0
% 47.62/11.23 % fd_pseudo_cond 33
% 47.62/11.23 % AC symbols 0
% 47.62/11.23
% 47.62/11.23 % ------ Schedule dynamic 5 is on
% 47.62/11.23
% 47.62/11.23 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 47.62/11.23
% 47.62/11.23
% 47.62/11.23 % ------
% 47.62/11.23 % Current options:
% 47.62/11.23 % ------
% 47.62/11.23
% 47.62/11.23
% 47.62/11.23 %
% 47.62/11.23
% 47.62/11.23 % ------ Proving...
% 47.62/11.23 % Proof_search_loop: time out after: 6054 full_loop iterations
% 47.62/11.23
% 47.62/11.23 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 47.62/11.23
% 47.62/11.23
% 47.62/11.23 % ------
% 47.62/11.23 % Current options:
% 47.62/11.23 % ------
% 47.62/11.23
% 47.62/11.23
% 47.62/11.23 %
% 47.62/11.23
% 47.62/11.23 % ------ Proving...
% 47.62/11.23 %
% 47.62/11.23
% 47.62/11.23 % SZS status Theorem for theBenchmark.p
% 47.62/11.23
% 47.62/11.23 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 47.62/11.24
% 47.62/11.24
%------------------------------------------------------------------------------