%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRA126-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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:23:51 PM UTC 2026
% Result : Unsatisfiable 14.30s 2.80s
% Output : CNFRefutation 14.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 635 ( 27 unt; 0 def)
% Number of atoms : 2161 ( 287 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 3304 (1778 ~;1526 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 1294 ( 0 sgn1294 !; 0 ?;1279 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : s(X0) != z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',snz) ).
fof(f2,axiom,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sinj) ).
fof(f3,axiom,
! [X0] : ~ r(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ri) ).
fof(f4,axiom,
! [X0] : ~ b(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bi) ).
fof(f5,axiom,
! [X0,X1] :
( b(X0,X1)
| r(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rb) ).
fof(f6,axiom,
! [X2,X3,X0,X1] :
( ~ r(X1,X3)
| ~ r(X0,X3)
| ~ r(X1,X2)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axr) ).
fof(f7,axiom,
! [X2,X3,X0,X1] :
( ~ b(X1,X3)
| ~ b(X0,X3)
| ~ b(X1,X2)
| ~ b(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axb) ).
tcf(c_56,plain,
! [X0: $i] : s(X0) != z,
inference(cnf_transformation,[],[f1]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0) != s(X1) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_58,plain,
! [X0: $i] : ~ r(X0,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_59,plain,
! [X0: $i] : ~ b(X0,X0),
inference(cnf_transformation,[],[f4]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( b(X0,X1)
| r(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X1,X3)
| ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X1,X3)
| ~ b(X1,X2)
| ~ b(X0,X2)
| ~ b(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_65,plain,
s(z) != z,
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_103,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_190,plain,
! [X0: $i] :
( ( s(X0) = z )
| ( s(s(X0)) != s(z) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_191,plain,
! [X0: $i] :
( b(s(X0),z)
| r(s(X0),z)
| ( s(X0) = z ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_192,plain,
( b(s(z),z)
| r(s(z),z)
| ( s(z) = z ) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_193,plain,
( ( s(z) = z )
| ( s(s(z)) != s(z) ) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = z )
| ( z != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_195,plain,
! [X0: $i] :
( ( s(s(X0)) = s(z) )
| ( s(s(s(X0))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_196,plain,
! [X0: $i] :
( b(s(s(X0)),s(z))
| r(s(s(X0)),s(z))
| ( s(s(X0)) = s(z) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_197,plain,
( b(s(s(z)),s(z))
| r(s(s(z)),s(z))
| ( s(s(z)) = s(z) ) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_198,plain,
( ( s(s(z)) = s(z) )
| ( s(s(s(z))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = X1 )
| ( s(s(X0)) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( b(s(X0),X1)
| r(s(X0),X1)
| ( s(X0) = X1 ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_202,plain,
! [X0: $i] :
( ( s(X0) = z )
| ( z != s(X0) )
| ( s(X0) != s(X0) ) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_203,plain,
( ( s(z) = z )
| ( z != s(z) )
| ( s(z) != s(z) ) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X0) = X2 )
| ( X2 != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,X1)
| ~ r(s(X0),z)
| ~ r(X2,s(X0))
| ~ r(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_220,plain,
! [X0: $i] : s(X0) = s(X0),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_221,plain,
s(z) = s(z),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,X1)
| ~ r(X2,s(s(X0)))
| ~ r(s(s(X0)),X1)
| ~ r(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,X1)
| ~ r(X3,s(X0))
| ~ r(s(X0),X2)
| ~ r(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_230,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),z)
| ~ r(s(z),X1)
| ~ r(s(s(X0)),X1)
| ~ r(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_231,plain,
( ~ r(s(z),z)
| ~ r(s(s(z)),z)
| ~ r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_230]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),z)
| ~ r(s(X1),X2)
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_237,plain,
! [X0: $i] : s(s(X0)) = s(s(X0)),
inference(instantiation,[status(thm)],[c_220]) ).
tcf(c_238,plain,
s(s(z)) = s(s(z)),
inference(instantiation,[status(thm)],[c_237]) ).
tcf(c_239,plain,
! [X0: $i] :
( ( z = s(X0) )
| ( s(z) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_240,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0))
| ( z = s(X0) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_241,plain,
( b(z,s(z))
| r(z,s(z))
| ( z = s(z) ) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_242,plain,
( ( z = s(z) )
| ( s(z) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_252,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),X1)
| r(s(s(X0)),X1)
| ( s(s(X0)) = X1 ) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_253,plain,
( b(s(s(z)),z)
| r(s(s(z)),z)
| ( s(s(z)) = z ) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_255,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(X1) )
| ( s(X0) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_256,plain,
! [X0: $i,X1: $i] :
( b(X0,s(X1))
| r(X0,s(X1))
| ( X0 = s(X1) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_258,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(X0) )
| ( X2 != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(X1)),X2)
| ~ r(s(s(X1)),s(z))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(X1))
| r(s(X0),s(X1))
| ( s(X0) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X1),X3)
| ~ r(s(X1),X2)
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_288,plain,
! [X0: $i] :
( b(s(s(X0)),z)
| r(s(s(X0)),z)
| ( s(s(X0)) = z ) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_316,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X0),s(z))
| ~ r(s(s(X1)),s(z))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_324,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(s(X0)) )
| ( X2 != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_326,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X0)) = X2 )
| ( X2 != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_327,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = z )
| ( z != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_329,plain,
! [X0: $i] :
( b(s(s(s(X0))),s(s(z)))
| r(s(s(s(X0))),s(s(z)))
| ( s(s(s(X0))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_330,plain,
( b(s(s(s(z))),s(s(z)))
| r(s(s(s(z))),s(s(z)))
| ( s(s(s(z))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_366,plain,
! [X0: $i] : ~ b(s(X0),s(X0)),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_367,plain,
~ b(s(z),s(z)),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(X0))
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,X2)
| ~ r(X1,z)
| ~ r(X1,X2)
| ~ r(z,s(X0)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_370,plain,
! [X0: $i] :
( b(z,s(s(X0)))
| r(z,s(s(X0)))
| ( z = s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_371,plain,
( b(z,s(s(z)))
| r(z,s(s(z)))
| ( z = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(X0))
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_377,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(X0))
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_379,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,X3)
| ~ r(X2,X0)
| ~ r(X0,X3)
| ~ r(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_381,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X1))
| ~ r(X3,s(X0))
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_394,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,X1)
| ~ b(s(X0),z)
| ~ b(X2,s(X0))
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_396,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X1)
| ~ b(X3,s(X0))
| ~ b(s(X0),X2)
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_410,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = X1 )
| ( X1 != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_326]) ).
tcf(c_411,plain,
( ( s(s(z)) = z )
| ( z != s(s(z)) )
| ( s(s(z)) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_410]) ).
tcf(c_419,plain,
! [X0: $i] :
( ( s(s(X0)) = z )
| ( z != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_428,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(X0))
| ~ r(s(X0),s(X2))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_431,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X0),X3)
| ~ b(s(X2),s(X0))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_368]) ).
tcf(c_437,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(X0)))
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_452,plain,
! [X0: $i] :
( b(s(z),s(X0))
| r(s(z),s(X0))
| ( s(z) = s(X0) ) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_456,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(s(X1)))
| r(s(X0),s(s(X1)))
| ( s(X0) = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X1))
| ~ r(X3,s(X0))
| ~ r(s(X0),s(X2))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_481,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X1))
| ~ r(X3,s(s(X0)))
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_493,plain,
! [X0: $i] :
( b(s(X0),z)
| r(s(X0),z) ),
inference(resolution,[status(thm)],[c_60,c_56]) ).
tcf(c_497,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),z)
| ~ b(s(X1),X2)
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,X0)
| ~ r(X3,s(X2))
| ~ r(X0,s(X2))
| ~ r(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X1,X2)
| ~ r(X1,s(X3))
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),X1) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_505,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X1),X3)
| ~ b(s(X1),X2)
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_536,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),X2)
| ~ r(s(s(z)),X1)
| ~ r(s(s(s(X0))),X1)
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),z)
| ~ r(s(s(z)),X1)
| ~ r(s(s(s(X0))),X1)
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_539,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_538]) ).
tcf(c_551,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(X2,X1)
| r(X2,X1)
| ( X2 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_105,c_60]) ).
tcf(c_552,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_105,c_103]) ).
tcf(c_556,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(z))
| ~ r(s(s(X0)),s(z))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_316]) ).
tcf(c_570,plain,
! [X0: $i] :
( b(s(s(s(X0))),z)
| r(s(s(s(X0))),z)
| ( s(s(s(X0))) = z ) ),
inference(instantiation,[status(thm)],[c_288]) ).
tcf(c_571,plain,
( b(s(s(s(z))),z)
| r(s(s(s(z))),z)
| ( s(s(s(z))) = z ) ),
inference(instantiation,[status(thm)],[c_570]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),X1)
| r(s(s(s(X0))),X1)
| ( s(s(s(X0))) = X1 ) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_635,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),X1)
| ~ r(s(s(z)),s(X2))
| ~ r(s(s(s(X0))),X1)
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X1))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_428]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(X0)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_437]) ).
tcf(c_645,plain,
! [X0: $i,X1: $i] :
( b(X1,X0)
| r(X1,X0)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_552,c_60]) ).
tcf(c_649,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X1),X2)
| ~ b(s(X1),s(X3))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_431]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),z)
| ~ b(s(X1),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_497]) ).
tcf(c_674,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0)) ),
inference(resolution,[status(thm)],[c_645,c_56]) ).
tcf(c_675,plain,
( b(z,s(z))
| r(z,s(z)) ),
inference(instantiation,[status(thm)],[c_674]) ).
tcf(c_679,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X2))
| ~ r(X3,s(X0))
| ~ r(s(X0),s(X2))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_683,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,s(X3))
| ~ r(X2,s(X1))
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_499]) ).
tcf(c_684,plain,
( ~ r(z,s(z))
| ~ r(s(s(z)),z)
| ~ r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_686,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),X2)
| ~ b(s(z),X1)
| ~ b(s(s(X0)),X1)
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_505]) ).
tcf(c_688,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X1),X3)
| ~ b(s(X1),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_505]) ).
tcf(c_697,plain,
! [X0: $i] :
( b(s(z),s(s(X0)))
| r(s(z),s(s(X0)))
| ( s(z) = s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_711,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(X1)),X3)
| ~ r(s(s(X1)),X2)
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_716,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X2))
| ~ r(X3,s(X0))
| ~ r(s(X0),s(X2))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_718,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),s(s(X1)))
| r(s(s(X0)),s(s(X1)))
| ( s(s(X0)) = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_456]) ).
tcf(c_816,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),s(X2))
| ~ r(s(s(z)),s(X1))
| ~ r(s(s(s(X0))),s(X1))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_635]) ).
tcf(c_817,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_855,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X2))
| ~ r(z,s(X1))
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_856,plain,
( ~ r(z,s(z))
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_855]) ).
tcf(c_868,plain,
! [X0: $i] :
( b(s(s(s(X0))),s(z))
| r(s(s(s(X0))),s(z))
| ( s(s(s(X0))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_869,plain,
( b(s(s(s(z))),s(z))
| r(s(s(s(z))),s(z))
| ( s(s(s(z))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_874,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),s(X1))
| r(s(s(s(X0))),s(X1))
| ( s(s(s(X0))) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_881,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X1,X2)
| ~ r(X1,s(X3))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),X1) ),
inference(instantiation,[status(thm)],[c_499]) ).
tcf(c_882,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X1))
| ~ r(X3,s(s(s(X0))))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_481]) ).
tcf(c_884,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,s(X3))
| ~ r(X2,s(X1))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_910,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(X1,X2)
| b(X0,X2)
| r(X1,X2)
| r(X0,X2)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_551,c_60]) ).
tcf(c_911,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(X2,X1)
| b(X0,X2)
| r(X2,X1)
| r(X0,X2)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_551,c_645]) ).
tcf(c_915,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X0))
| ~ r(s(X0),z)
| ~ r(z,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_377]) ).
tcf(c_918,plain,
! [X0: $i] :
( b(z,s(s(s(X0))))
| r(z,s(s(s(X0))))
| ( z = s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_256]) ).
tcf(c_919,plain,
( b(z,s(s(s(z))))
| r(z,s(s(s(z))))
| ( z = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_929,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_639]) ).
tcf(c_940,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,s(X0))
| ~ r(s(X0),X3)
| ~ r(X2,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),X3)
| ~ r(s(s(X0)),X3)
| ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_711]) ).
tcf(c_950,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(s(X1))),X3)
| ~ r(s(s(s(X1))),X2)
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_711]) ).
tcf(c_971,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(s(X0),z)
| ~ b(X2,X1)
| ~ b(X2,s(X0))
| ~ b(s(X0),X1) ),
inference(resolution,[status(thm)],[c_62,c_493]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(z,s(X2))
| ~ b(z,X1)
| ~ b(X0,z)
| ~ b(X0,X1) ),
inference(resolution,[status(thm)],[c_62,c_674]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),z)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_661]) ).
tcf(c_985,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X1)),s(z))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_1006,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),X3)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_688]) ).
tcf(c_1009,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X0))
| ~ r(X3,s(s(X2)))
| ~ r(s(X0),s(s(X2)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_1010,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X2))
| ~ r(X3,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_1021,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(X1) )
| ( s(s(X0)) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_1024,plain,
! [X0: $i] :
( b(s(s(z)),s(s(s(X0))))
| r(s(s(z)),s(s(s(X0))))
| ( s(s(z)) = s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_1025,plain,
( b(s(s(z)),s(s(s(z))))
| r(s(s(z)),s(s(s(z))))
| ( s(s(z)) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1024]) ).
tcf(c_1044,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(s(X0)) )
| ( s(X2) != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_324]) ).
tcf(c_1082,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(s(X1),X2)
| b(s(X0),X2)
| r(s(X1),X2)
| r(s(X0),X2)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_910,c_57]) ).
tcf(c_1087,plain,
! [X0: $i] : s(s(X0)) != z,
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_1088,plain,
s(s(z)) != z,
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_1105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X0)) = s(X2) )
| ( s(X2) != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_326]) ).
tcf(c_1132,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,X1)
| ~ r(z,s(X2))
| ~ r(s(X0),z)
| ~ r(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_369]) ).
tcf(c_1135,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X2))
| ~ r(z,s(X1))
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_1164,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X1,X2)
| ~ r(X1,s(X3))
| ~ r(s(X0),X2)
| ~ r(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_1195,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,X2)
| ~ b(X1,z)
| ~ b(X1,X2)
| ~ b(z,s(X0)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_1198,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,X1)
| ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),X1)
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_368]) ).
tcf(c_1199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(s(X0)))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_368]) ).
tcf(c_1215,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X2,X0)
| ~ b(X0,X3)
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_1376,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(s(z)) )
| ( s(s(s(s(X0)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1021]) ).
tcf(c_1377,plain,
( ( s(s(s(z))) = s(s(z)) )
| ( s(s(s(s(z)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1376]) ).
tcf(c_1378,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(X1) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_1021]) ).
tcf(c_1379,plain,
! [X0: $i] :
( ( s(z) = s(X0) )
| ( s(s(z)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_1021]) ).
tcf(c_1383,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(s(X1)) )
| ( s(s(X0)) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_1021]) ).
tcf(c_1384,plain,
( ( s(z) = s(s(z)) )
| ( s(s(z)) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1383]) ).
tcf(c_1517,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X0,z)
| ~ b(z,s(X2))
| ~ b(z,s(X1))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_1195]) ).
tcf(c_1524,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X1))),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(s(X1))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_881]) ).
tcf(c_1525,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(s(s(X0))),X3)
| ~ r(s(X2),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_1528,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(X1))
| ~ r(s(X2),s(s(X3)))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_884]) ).
tcf(c_1531,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X1))),s(X3))
| ~ r(s(s(s(X1))),s(X2))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_884]) ).
tcf(c_1540,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_915]) ).
tcf(c_1541,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(z))))
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1540]) ).
tcf(c_1547,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X2))
| ~ r(s(X1),z)
| ~ r(s(X1),s(X2))
| ~ r(z,s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_1550,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(s(s(X1))))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),X3)
| ~ r(s(X2),s(s(X1)))
| ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_1624,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(s(s(X1))))
| r(s(X0),s(s(s(X1))))
| ( s(X0) = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_456]) ).
tcf(c_1627,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X1))),X3)
| ~ r(s(s(s(X1))),X2)
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_950]) ).
tcf(c_1645,plain,
! [X0: $i,X1: $i] :
( ~ b(z,X1)
| ~ b(z,s(s(X0)))
| ~ b(s(s(X0)),X1)
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_1198]) ).
tcf(c_1648,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X3),s(s(X1)))
| ~ r(s(X3),s(s(X0)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_1829,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X3)))
| ~ r(s(X2),s(s(X1)))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1009]) ).
tcf(c_1834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),X3)
| ~ r(s(X0),X3)
| ~ r(s(X2),s(X0))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1164]) ).
tcf(c_1882,plain,
! [X0: $i] :
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_556]) ).
tcf(c_1884,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(z))),s(z))
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1882]) ).
tcf(c_1922,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),X1)
| ~ b(s(s(z)),s(z))
| ~ b(s(s(s(X0))),X1)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_985]) ).
tcf(c_1923,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),z)
| ~ b(s(s(z)),X1)
| ~ b(s(s(s(X0))),X1)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1924,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_1933,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),s(X2))
| ~ r(s(s(s(X1))),X3)
| ~ r(s(s(s(X1))),s(X2))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_950]) ).
tcf(c_1935,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X3)))
| ~ r(s(X2),s(s(X1)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1009]) ).
tcf(c_1942,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X1),X3)
| ~ r(s(X1),X2)
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_1944,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),z)
| ~ r(s(X1),X2)
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1950,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X1)),X2)
| ~ r(s(s(X1)),s(X3))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_881]) ).
tcf(c_1959,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X2))
| ~ r(X3,s(s(X0)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_1965,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(X3))
| ~ r(s(X2),s(X1))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_1986,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X1))
| ~ b(z,s(X0))
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_1988,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X1))
| ~ b(X3,s(X0))
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_396]) ).
tcf(c_2000,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(X2))
| ~ b(X1,s(s(z)))
| ~ b(s(s(s(X0))),X1)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1215]) ).
tcf(c_2003,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X1,X2)
| ~ b(X1,s(X3))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),X1) ),
inference(instantiation,[status(thm)],[c_1215]) ).
tcf(c_2004,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X0)
| ~ b(X3,s(X2))
| ~ b(X0,s(X2))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_1215]) ).
tcf(c_2030,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X2))
| ~ r(s(X0),z)
| ~ r(z,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1132]) ).
tcf(c_2141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X1,X2)
| ~ b(X1,s(X3))
| ~ b(s(X0),X2)
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_1215]) ).
tcf(c_2189,plain,
! [X0: $i] :
( b(s(s(s(s(X0)))),s(s(s(z))))
| r(s(s(s(s(X0)))),s(s(s(z))))
| ( s(s(s(s(X0)))) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_2190,plain,
( b(s(s(s(s(z)))),s(s(s(z))))
| r(s(s(s(s(z)))),s(s(s(z))))
| ( s(s(s(s(z)))) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_2189]) ).
tcf(c_2207,plain,
! [X0: $i] :
( ( s(z) = s(s(X0)) )
| ( s(s(z)) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_1379]) ).
tcf(c_2336,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(X2,s(X1))
| b(s(X0),X2)
| r(X2,s(X1))
| r(s(X0),X2)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_911,c_57]) ).
tcf(c_2364,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),s(s(s(X1))))
| r(s(s(X0)),s(s(s(X1))))
| ( s(s(X0)) = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_2378,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(z))
| ~ b(s(s(z)),s(X1))
| ~ b(s(s(s(X0))),s(X1))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1922]) ).
tcf(c_2379,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2378]) ).
tcf(c_2386,plain,
! [X0: $i] :
( ~ b(s(s(z)),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_2452,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(X1))
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_2481,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(z,s(s(X0)))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1645]) ).
tcf(c_2509,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),z)
| ~ r(z,s(s(X2)))
| ~ r(z,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2030]) ).
tcf(c_2556,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(X0))))
| ~ b(s(s(s(X0))),X1)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1986]) ).
tcf(c_2557,plain,
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2556]) ).
tcf(c_2623,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2000]) ).
tcf(c_2625,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X1)),s(s(z)))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2000]) ).
tcf(c_2651,plain,
! [X0: $i] : s(s(s(X0))) != z,
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_2652,plain,
s(s(s(z))) != z,
inference(instantiation,[status(thm)],[c_2651]) ).
tcf(c_2667,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X1))),s(X3))
| ~ r(s(s(s(X0))),s(X3))
| ~ r(s(s(s(X1))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1528]) ).
tcf(c_2681,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(s(s(X0))) )
| ( s(X2) != X1 )
| ( s(s(s(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_1044]) ).
tcf(c_2682,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = s(X2) )
| ( s(X2) != X1 )
| ( s(s(s(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_1105]) ).
tcf(c_2683,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = X2 )
| ( X2 != X1 )
| ( s(s(s(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_326]) ).
tcf(c_2702,plain,
! [X0: $i] :
( ( s(s(s(X0))) = z )
| ( z != s(s(s(X0))) )
| ( s(s(s(X0))) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_419]) ).
tcf(c_2703,plain,
( ( s(s(s(z))) = z )
| ( z != s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_2702]) ).
tcf(c_2745,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),X3)
| ~ r(s(X2),s(s(X0)))
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1618]) ).
tcf(c_2750,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(X3))
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1648]) ).
tcf(c_2778,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),X3)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1006]) ).
tcf(c_2781,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),z)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_2828,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X3)))
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1829]) ).
tcf(c_2841,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),X3)
| ~ r(s(s(X0)),X3)
| ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1834]) ).
tcf(c_2860,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X3)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1935]) ).
tcf(c_2895,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(X0)))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1199]) ).
tcf(c_2938,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(z,s(X2))
| r(z,s(X1))
| ~ b(X0,z)
| ~ b(X0,s(X1)) ),
inference(resolution,[status(thm)],[c_972,c_674]) ).
tcf(c_2941,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(X3))
| ~ r(s(X2),s(X1))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1965]) ).
tcf(c_2942,plain,
( ~ r(s(z),s(z))
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_2941]) ).
tcf(c_2953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X1),X3)
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1988]) ).
tcf(c_2959,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X1,X2)
| ~ b(X1,s(s(X3)))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),X1) ),
inference(instantiation,[status(thm)],[c_2003]) ).
tcf(c_2962,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,s(X3))
| ~ b(X2,s(X1))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_2004]) ).
tcf(c_2968,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2141]) ).
tcf(c_2970,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(X0)),X3)
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_2141]) ).
tcf(c_2993,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(z),s(s(X1)))
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_686]) ).
tcf(c_3257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X1),X3)
| ~ r(s(X0),X3)
| ~ r(s(X1),s(X2))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_1164]) ).
tcf(c_3455,plain,
! [X0: $i] : s(s(s(X0))) = s(s(s(X0))),
inference(instantiation,[status(thm)],[c_237]) ).
tcf(c_3456,plain,
s(s(s(z))) = s(s(s(z))),
inference(instantiation,[status(thm)],[c_3455]) ).
tcf(c_3655,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = s(X2) )
| ( s(X2) != s(X1) )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_2682]) ).
tcf(c_3785,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),s(s(s(X1))))
| r(s(s(s(X0))),s(s(s(X1))))
| ( s(s(s(X0))) = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_2364]) ).
tcf(c_3817,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X1)),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(X1)),s(s(s(X2))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1950]) ).
tcf(c_3843,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X3),s(X2))
| ~ r(s(X3),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1010]) ).
tcf(c_3871,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(s(X2)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2993]) ).
tcf(c_3897,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),X3)
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(X2),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1525]) ).
tcf(c_3968,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X3)),s(s(s(X1))))
| ~ r(s(s(X3)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2860]) ).
tcf(c_3971,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),s(s(X2)))
| ~ r(s(s(X2)),s(s(s(X3))))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2860]) ).
tcf(c_4339,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X1))),s(s(X3)))
| ~ r(s(s(s(X1))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1829]) ).
tcf(c_4439,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),s(s(X2)))
| ~ r(s(X1),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2828]) ).
tcf(c_4445,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),X2)
| ~ r(s(s(s(z))),X1)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_4446,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),s(X2))
| ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_4455,plain,
( ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4446]) ).
tcf(c_4456,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4445]) ).
tcf(c_4888,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(z))),s(s(X2)))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2667]) ).
tcf(c_4891,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2745]) ).
tcf(c_4899,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(X3))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2750]) ).
tcf(c_4902,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),s(X3))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2750]) ).
tcf(c_5031,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2841]) ).
tcf(c_5054,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2895]) ).
tcf(c_5065,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2953]) ).
tcf(c_5080,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),s(X3))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_5081,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),X3)
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_5083,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(X2)))
| ~ b(z,s(s(X1)))
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_5084,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,s(s(X3)))
| ~ b(X2,s(s(X1)))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_5089,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(z))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2962]) ).
tcf(c_5091,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),s(X3))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2962]) ).
tcf(c_5094,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(s(X3)))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_2962]) ).
tcf(c_5293,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X0),X2)
| ~ b(s(s(X1)),X3)
| ~ b(s(s(X1)),X2)
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_505]) ).
tcf(c_5333,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(z))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2970]) ).
tcf(c_5412,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),X3)
| ~ r(s(s(X0)),X3)
| ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3257]) ).
tcf(c_5529,plain,
! [X0: $i] :
( b(s(s(s(s(X0)))),s(z))
| r(s(s(s(s(X0)))),s(z))
| ( s(s(s(s(X0)))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_5530,plain,
( b(s(s(s(s(z)))),s(z))
| r(s(s(s(s(z)))),s(z))
| ( s(s(s(s(z)))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_5529]) ).
tcf(c_5673,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(X1) )
| ( s(X1) != s(s(s(X0))) )
| ( s(s(s(X0))) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_3655]) ).
tcf(c_5674,plain,
( ( s(s(s(z))) = s(z) )
| ( s(z) != s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_5673]) ).
tcf(c_5736,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),s(X1))
| r(s(s(s(s(X0)))),s(X1))
| ( s(s(s(s(X0)))) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_874]) ).
tcf(c_5824,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),z)
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(X1)),s(s(s(X2))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3817]) ).
tcf(c_5837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(s(s(X3))))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3971]) ).
tcf(c_5841,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X3)),s(s(s(X1))))
| ~ r(s(s(X3)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X2))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3971]) ).
tcf(c_5856,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),s(s(X1)))
| ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(z)))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4439]) ).
tcf(c_5877,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(s(X2)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(s(s(X0))),s(z))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3871]) ).
tcf(c_5878,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_5877]) ).
tcf(c_5911,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(z)))
| ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(s(X1))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3843]) ).
tcf(c_6000,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(z)))
| ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(s(z)))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4888]) ).
tcf(c_6001,plain,
( ~ r(s(s(s(z))),s(s(z)))
| ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6000]) ).
tcf(c_6049,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(X2)))
| ~ b(z,s(s(X1)))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5083]) ).
tcf(c_6160,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(s(s(s(X1)))))
| r(s(X0),s(s(s(s(X1)))))
| ( s(X0) = s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_1624]) ).
tcf(c_6161,plain,
( b(s(z),s(s(s(s(z)))))
| r(s(z),s(s(s(s(z)))))
| ( s(z) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6160]) ).
tcf(c_6344,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),X1)
| ~ b(s(s(s(s(X0)))),X1)
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2781]) ).
tcf(c_6347,plain,
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6344]) ).
tcf(c_6383,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(s(X1)) )
| ( s(s(s(X0))) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_1378]) ).
tcf(c_6399,plain,
! [X0: $i] :
( b(s(s(s(z))),s(s(s(s(X0)))))
| r(s(s(s(z))),s(s(s(s(X0)))))
| ( s(s(s(z))) = s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_3785]) ).
tcf(c_6400,plain,
( b(s(s(s(z))),s(s(s(s(z)))))
| r(s(s(s(z))),s(s(s(s(z)))))
| ( s(s(s(z))) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6399]) ).
tcf(c_6512,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(z))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5089]) ).
tcf(c_6592,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5412]) ).
tcf(c_6600,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(z))))
| ~ b(X2,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(X1))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5054]) ).
tcf(c_6619,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5065]) ).
tcf(c_6626,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(X0))),s(X3))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5080]) ).
tcf(c_6633,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5081]) ).
tcf(c_6640,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,s(s(X3)))
| ~ b(X2,s(s(X1)))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5084]) ).
tcf(c_6655,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(X3)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5094]) ).
tcf(c_6702,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),X3)
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5293]) ).
tcf(c_6770,plain,
! [X0: $i] :
( b(s(s(s(s(X0)))),s(s(z)))
| r(s(s(s(s(X0)))),s(s(z)))
| ( s(s(s(s(X0)))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_6771,plain,
( b(s(s(s(s(z)))),s(s(z)))
| r(s(s(s(s(z)))),s(s(z)))
| ( s(s(s(s(z)))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_6770]) ).
tcf(c_6905,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(X1))))
| ~ r(s(s(s(s(X0)))),s(s(z)))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5856]) ).
tcf(c_6906,plain,
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6905]) ).
tcf(c_6921,plain,
! [X0: $i] :
( b(s(s(z)),s(s(s(s(X0)))))
| r(s(s(z)),s(s(s(s(X0)))))
| ( s(s(z)) = s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_1024]) ).
tcf(c_6922,plain,
( b(s(s(z)),s(s(s(s(z)))))
| r(s(s(z)),s(s(s(s(z)))))
| ( s(s(z)) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6921]) ).
tcf(c_6966,plain,
! [X0: $i] :
( ( s(s(s(s(X0)))) = s(s(s(z))) )
| ( s(s(s(s(s(X0))))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6383]) ).
tcf(c_6967,plain,
( ( s(s(s(s(z)))) = s(s(s(z))) )
| ( s(s(s(s(s(z))))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6966]) ).
tcf(c_6968,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(s(X1)) )
| ( s(s(s(s(X0)))) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_6383]) ).
tcf(c_6977,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(s(s(X1))) )
| ( s(s(s(X0))) != s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_6383]) ).
tcf(c_6978,plain,
( ( s(s(z)) = s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_6977]) ).
tcf(c_7420,plain,
! [X0: $i] :
( b(z,s(s(s(s(X0)))))
| r(z,s(s(s(s(X0)))))
| ( z = s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_918]) ).
tcf(c_7421,plain,
( b(z,s(s(s(s(z)))))
| r(z,s(s(s(s(z)))))
| ( z = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_7420]) ).
tcf(c_7424,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(X1))
| ~ b(s(s(s(s(X0)))),s(X1))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6344]) ).
tcf(c_7430,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),X1)
| r(s(s(s(s(X0)))),X1)
| ( s(s(s(s(X0)))) = X1 ) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_7431,plain,
( b(s(s(s(s(z)))),z)
| r(s(s(s(s(z)))),z)
| ( s(s(s(s(z)))) = z ) ),
inference(instantiation,[status(thm)],[c_7430]) ).
tcf(c_7459,plain,
! [X0: $i] :
( b(s(s(s(s(X0)))),s(s(s(s(X0)))))
| r(s(s(s(s(X0)))),s(s(s(s(X0)))))
| ( s(s(s(s(X0)))) = s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_7460,plain,
( b(s(s(s(s(z)))),s(s(s(s(z)))))
| r(s(s(s(s(z)))),s(s(s(s(z)))))
| ( s(s(s(s(z)))) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_7459]) ).
tcf(c_7484,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),s(s(X1)))
| r(s(s(s(s(X0)))),s(s(X1)))
| ( s(s(s(s(X0)))) = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_7837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(s(s(X3))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(X2)),s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5837]) ).
tcf(c_7963,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(s(s(X1)))),s(s(z)))
| ~ r(s(s(s(s(X1)))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5911]) ).
tcf(c_7964,plain,
( ~ r(s(s(s(z))),s(s(z)))
| ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_7963]) ).
tcf(c_8228,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),X1)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_8229,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(s(X0)))),s(X2))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_8231,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(z))),X2)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1524]) ).
tcf(c_8232,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_8235,plain,
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_8232]) ).
tcf(c_8236,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_8231]) ).
tcf(c_8238,plain,
( ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_8229]) ).
tcf(c_8239,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_8228]) ).
tcf(c_8260,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(z))))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(z))),s(s(s(X1))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_5841]) ).
tcf(c_8307,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(z))))
| ~ b(X2,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6600]) ).
tcf(c_8512,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6592]) ).
tcf(c_8559,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(X1)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6626]) ).
tcf(c_8611,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(X3)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6655]) ).
tcf(c_8625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(X0))),X3)
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6702]) ).
tcf(c_8730,plain,
! [X0: $i] :
( b(s(s(s(s(s(X0))))),s(s(s(s(z)))))
| r(s(s(s(s(s(X0))))),s(s(s(s(z)))))
| ( s(s(s(s(s(X0))))) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_3785]) ).
tcf(c_8731,plain,
( b(s(s(s(s(s(z))))),s(s(s(s(z)))))
| r(s(s(s(s(s(z))))),s(s(s(s(z)))))
| ( s(s(s(s(s(z))))) = s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_8730]) ).
tcf(c_9170,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(z))))
| ~ r(s(s(X2)),s(s(s(s(X1)))))
| ~ r(s(s(s(z))),s(s(s(s(X1)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_8260]) ).
tcf(c_9171,plain,
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_9170]) ).
tcf(c_9247,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(s(X0)))) = X2 )
| ( X2 != X1 )
| ( s(s(s(s(X0)))) != X1 ) ),
inference(instantiation,[status(thm)],[c_2683]) ).
tcf(c_9249,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(s(s(s(X0)))) )
| ( s(X2) != X1 )
| ( s(s(s(s(X0)))) != X1 ) ),
inference(instantiation,[status(thm)],[c_2681]) ).
tcf(c_9443,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_7424]) ).
tcf(c_9499,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(X2))
| ~ r(s(X1),z)
| ~ r(s(X1),s(X2))
| ~ r(z,s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1547]) ).
tcf(c_9502,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_9505,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),z)
| ~ r(z,s(s(X2)))
| ~ r(s(X1),s(s(X2)))
| ~ r(z,s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2509]) ).
tcf(c_9617,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(s(s(X3))))
| ~ r(s(s(X2)),s(s(s(s(X1)))))
| ~ r(s(s(s(s(X0)))),s(s(X2)))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_7837]) ).
tcf(c_9645,plain,
! [X0: $i] : s(s(s(s(X0)))) != z,
inference(instantiation,[status(thm)],[c_2651]) ).
tcf(c_9646,plain,
s(s(s(s(z)))) != z,
inference(instantiation,[status(thm)],[c_9645]) ).
tcf(c_10021,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(s(z))))
| ~ b(X1,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8307]) ).
tcf(c_10060,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(X2))
| ~ r(X3,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(X2))
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1959]) ).
tcf(c_10078,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,s(X0))
| ~ r(s(X0),X3)
| ~ r(X2,s(s(s(s(X1)))))
| ~ r(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_10306,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(s(X2)))
| ~ b(s(s(s(z))),X1)
| ~ b(X1,s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6640]) ).
tcf(c_10307,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(s(z))),X2)
| ~ b(s(s(X1)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6633]) ).
tcf(c_10308,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(z))),s(X2))
| ~ b(s(s(X1)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6626]) ).
tcf(c_10309,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),X2)
| ~ b(s(s(s(z))),s(X1))
| ~ b(s(X1),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6619]) ).
tcf(c_10311,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(X1))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(s(X0)))),s(X1))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6512]) ).
tcf(c_10322,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),X1)
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),X1)
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2781]) ).
tcf(c_10325,plain,
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_10322]) ).
tcf(c_10329,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_10311]) ).
tcf(c_10330,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(z))),s(z))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_10309]) ).
tcf(c_10332,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_10307]) ).
tcf(c_10436,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(X1)))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8559]) ).
tcf(c_10465,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(s(X0)))),X3)
| ~ r(s(s(X2)),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_8512]) ).
tcf(c_10564,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(z) )
| ( s(s(s(s(X0)))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_10565,plain,
( ( s(s(s(z))) = s(z) )
| ( s(s(s(s(z)))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_10564]) ).
tcf(c_10682,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_8625]) ).
tcf(c_10684,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(X3)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_8611]) ).
tcf(c_10690,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6633]) ).
tcf(c_10691,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(s(X0)))),s(X3))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6626]) ).
tcf(c_10692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6619]) ).
tcf(c_10694,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(z))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6512]) ).
tcf(c_10698,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(X2)))
| ~ b(z,s(s(X1)))
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6049]) ).
tcf(c_10704,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X1)),X3)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2778]) ).
tcf(c_10705,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),z)
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2781]) ).
tcf(c_10708,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10705]) ).
tcf(c_10710,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10698]) ).
tcf(c_10712,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10694]) ).
tcf(c_10747,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),s(s(s(s(X1)))))
| r(s(s(s(s(X0)))),s(s(s(s(X1)))))
| ( s(s(s(s(X0)))) = s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_7484]) ).
tcf(c_10940,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(z))))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8307]) ).
tcf(c_10941,plain,
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_10940]) ).
tcf(c_10961,plain,
! [X0: $i] :
( ( z = s(s(s(X0))) )
| ( s(z) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_10962,plain,
( ( z = s(s(s(z))) )
| ( s(z) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_10961]) ).
tcf(c_10988,plain,
! [X0: $i] : ~ r(s(s(s(s(X0)))),s(s(s(s(X0))))),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_10989,plain,
~ r(s(s(s(s(z)))),s(s(s(s(z))))),
inference(instantiation,[status(thm)],[c_10988]) ).
tcf(c_11346,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(s(X0)))) = X2 )
| ( X2 != s(X1) )
| ( s(s(s(s(X0)))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_9247]) ).
tcf(c_11449,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(s(s(s(X0)))) )
| ( s(X2) != s(X1) )
| ( s(s(s(s(X0)))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_9249]) ).
tcf(c_11450,plain,
( ( s(z) = s(s(s(s(z)))) )
| ( s(z) != s(z) )
| ( s(s(s(s(z)))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_11449]) ).
tcf(c_11728,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_9443]) ).
tcf(c_11730,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X1)),s(s(s(z))))
| ~ b(s(s(X1)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_10021]) ).
tcf(c_11908,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(z,s(s(X1)))
| ~ r(s(s(s(X0))),z)
| ~ r(z,s(s(s(s(X2)))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_9499]) ).
tcf(c_12000,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6619]) ).
tcf(c_12068,plain,
! [X0: $i,X1: $i] :
( b(s(z),X1)
| r(s(z),X1)
| b(s(s(X0)),X1)
| r(s(s(X0)),X1) ),
inference(resolution,[status(thm)],[c_1082,c_56]) ).
tcf(c_12105,plain,
! [X0: $i] :
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_9502]) ).
tcf(c_12106,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_12105]) ).
tcf(c_12116,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),z)
| ~ r(z,s(s(s(s(X2)))))
| ~ r(z,s(s(s(s(X1)))))
| ~ r(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_9505]) ).
tcf(c_12192,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X1),X3)
| ~ r(s(X1),X2)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1942]) ).
tcf(c_12193,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),z)
| ~ r(s(X1),X2)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1944]) ).
tcf(c_12198,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_12193]) ).
tcf(c_12224,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X2,s(X3))
| ~ r(X2,s(X1))
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_884]) ).
tcf(c_12231,plain,
( ~ r(z,s(z))
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_12224]) ).
tcf(c_12232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),s(X2))
| ~ r(s(s(s(s(X1)))),X3)
| ~ r(s(s(s(s(X1)))),s(X2))
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1933]) ).
tcf(c_12233,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(s(s(X1)))),X3)
| ~ r(s(s(s(s(X1)))),X2)
| ~ r(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_950]) ).
tcf(c_12234,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_12232]) ).
tcf(c_12246,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(s(X0)))),X3)
| ~ r(s(s(X2)),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5031]) ).
tcf(c_12624,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(X1)))
| ~ b(s(s(X2)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_10308]) ).
tcf(c_13020,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(X1)),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_10306]) ).
tcf(c_13036,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(X1)),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_10309]) ).
tcf(c_13037,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_13036]) ).
tcf(c_13103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(s(X1)))
| ~ r(X3,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(X2))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_10060]) ).
tcf(c_13221,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X1,s(s(z)))
| ~ r(s(s(z)),X2)
| ~ r(X1,s(s(s(s(X0)))))
| ~ r(s(s(z)),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_10078]) ).
tcf(c_13267,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10436]) ).
tcf(c_13269,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_10436]) ).
tcf(c_13376,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X1)))),s(z))
| ~ b(s(s(s(s(X1)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10694]) ).
tcf(c_13377,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_13376]) ).
tcf(c_13398,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X1)))),z)
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10705]) ).
tcf(c_13399,plain,
( ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_13398]) ).
tcf(c_13648,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_10311]) ).
tcf(c_13751,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X2))),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(X2))),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5824]) ).
tcf(c_13882,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10682]) ).
tcf(c_14096,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(s(z)))))
| ~ r(s(s(X2)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_3968]) ).
tcf(c_14103,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),X2)
| ~ r(s(X1),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_3897]) ).
tcf(c_14104,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(X2))
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4902]) ).
tcf(c_14105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),s(X2))
| ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4899]) ).
tcf(c_14106,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),X2)
| ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4891]) ).
tcf(c_14112,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(z)))),s(s(X2)))
| ~ r(s(s(s(s(z)))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4339]) ).
tcf(c_14126,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(z)))),X2)
| ~ r(s(s(s(s(z)))),X1)
| ~ r(s(s(s(s(s(X0))))),X1)
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_14127,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(z)))),s(X2))
| ~ r(s(s(s(s(z)))),s(X1))
| ~ r(s(s(s(s(s(X0))))),s(X1))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_14136,plain,
( ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14127]) ).
tcf(c_14137,plain,
( ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14126]) ).
tcf(c_14145,plain,
( ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14112]) ).
tcf(c_14147,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14106]) ).
tcf(c_14148,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14105]) ).
tcf(c_14243,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),X2)
| ~ r(s(s(s(s(s(X0))))),X2)
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_10465]) ).
tcf(c_14248,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),s(s(s(X2))))
| ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_9617]) ).
tcf(c_14254,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14243]) ).
tcf(c_14372,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(s(s(X1))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_6968]) ).
tcf(c_14375,plain,
! [X0: $i] :
( b(s(s(s(s(z)))),s(s(s(s(s(X0))))))
| r(s(s(s(s(z)))),s(s(s(s(s(X0))))))
| ( s(s(s(s(z)))) = s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_10747]) ).
tcf(c_14376,plain,
( b(s(s(s(s(z)))),s(s(s(s(s(z))))))
| r(s(s(s(s(z)))),s(s(s(s(s(z))))))
| ( s(s(s(s(z)))) = s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_14375]) ).
tcf(c_14570,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10690]) ).
tcf(c_14581,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(s(X0)))),s(X3))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10691]) ).
tcf(c_14592,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10692]) ).
tcf(c_14644,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(s(X1)))),X3)
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_10704]) ).
tcf(c_15329,plain,
! [X0: $i] :
( b(s(s(s(s(s(X0))))),s(s(z)))
| r(s(s(s(s(s(X0))))),s(s(z)))
| ( s(s(s(s(s(X0))))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_6770]) ).
tcf(c_15330,plain,
( b(s(s(s(s(s(z))))),s(s(z)))
| r(s(s(s(s(s(z))))),s(s(z)))
| ( s(s(s(s(s(z))))) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_15329]) ).
tcf(c_15351,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = X1 )
| ( X1 != s(s(s(s(X0)))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_11346]) ).
tcf(c_15352,plain,
( ( s(s(s(s(z)))) = z )
| ( z != s(s(s(s(z)))) )
| ( s(s(s(s(z)))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_15351]) ).
tcf(c_15470,plain,
! [X0: $i] :
( ( s(s(s(z))) = s(s(s(s(X0)))) )
| ( s(s(s(s(z)))) != s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_14372]) ).
tcf(c_15471,plain,
( ( s(s(s(z))) = s(s(s(s(z)))) )
| ( s(s(s(s(z)))) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_15470]) ).
tcf(c_15665,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),X2)
| ~ r(s(s(z)),X1)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_12192]) ).
tcf(c_15666,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_15665]) ).
tcf(c_15769,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),s(s(s(z))))
| ~ b(s(s(s(s(X1)))),s(s(s(z))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_11730]) ).
tcf(c_15796,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X0))),z)
| ~ r(z,s(s(s(s(X2)))))
| ~ r(z,s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_11908]) ).
tcf(c_15797,plain,
( ~ r(s(s(s(z))),z)
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_15796]) ).
tcf(c_15865,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(X2))
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(z)) ),
inference(instantiation,[status(thm)],[c_12224]) ).
tcf(c_15973,plain,
! [X0: $i] :
( b(s(s(z)),s(s(s(s(s(X0))))))
| r(s(s(z)),s(s(s(s(s(X0))))))
| ( s(s(z)) = s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_6921]) ).
tcf(c_15974,plain,
( b(s(s(z)),s(s(s(s(s(z))))))
| r(s(s(z)),s(s(s(s(s(z))))))
| ( s(s(z)) = s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_15973]) ).
tcf(c_16027,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),X1)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(z)),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_12233]) ).
tcf(c_16028,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16027]) ).
tcf(c_16081,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),z)
| ~ r(z,s(s(s(s(X1)))))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(z)),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_12116]) ).
tcf(c_16082,plain,
( ~ r(s(s(z)),z)
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16081]) ).
tcf(c_16277,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(z))))
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_12624]) ).
tcf(c_16278,plain,
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16277]) ).
tcf(c_16368,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(z)),X2)
| ~ r(s(X1),s(s(z)))
| ~ r(s(X1),s(s(s(s(X0)))))
| ~ r(s(s(z)),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_13221]) ).
tcf(c_16369,plain,
( ~ r(s(s(z)),z)
| ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16368]) ).
tcf(c_16454,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(s(X2))))
| ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14248]) ).
tcf(c_16510,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_13648]) ).
tcf(c_16814,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(s(X0))))),X1)
| r(s(s(s(s(s(X0))))),X1)
| ( s(s(s(s(s(X0))))) = X1 ) ),
inference(instantiation,[status(thm)],[c_7430]) ).
tcf(c_16815,plain,
( b(s(s(s(s(s(z))))),z)
| r(s(s(s(s(s(z))))),z)
| ( s(s(s(s(s(z))))) = z ) ),
inference(instantiation,[status(thm)],[c_16814]) ).
tcf(c_17120,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(X1)))),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X1)))),s(s(s(X2))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_13751]) ).
tcf(c_17153,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_13020]) ).
tcf(c_17162,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_13036]) ).
tcf(c_17285,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_12000]) ).
tcf(c_17537,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(X2)))
| ~ r(s(s(s(X1))),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14096]) ).
tcf(c_17538,plain,
( ~ r(s(s(s(z))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(z))),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17537]) ).
tcf(c_17541,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),s(s(s(s(s(X1))))))
| r(s(s(X0)),s(s(s(s(s(X1))))))
| ( s(s(X0)) = s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_2364]) ).
tcf(c_17573,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(s(X0))))),X2)
| ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(X1))),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14103]) ).
tcf(c_17574,plain,
( ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(z))),s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17573]) ).
tcf(c_17633,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(s(X0))))),s(X2))
| ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(X1))),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14104]) ).
tcf(c_17634,plain,
( ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17633]) ).
tcf(c_17660,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),X2)
| ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14106]) ).
tcf(c_17661,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(z))))),s(s(s(z))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17660]) ).
tcf(c_17710,plain,
! [X0: $i] :
( b(s(z),s(s(X0)))
| r(s(z),s(s(X0)))
| r(s(s(X0)),s(s(X0))) ),
inference(resolution,[status(thm)],[c_12068,c_59]) ).
tcf(c_17717,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(s(X2),z)
| b(s(z),s(X2))
| r(s(z),s(X2))
| r(s(s(X0)),s(X2))
| ~ b(s(X2),X1)
| ~ b(s(s(X0)),X1) ),
inference(resolution,[status(thm)],[c_12068,c_971]) ).
tcf(c_17719,plain,
( r(s(z),z)
| b(s(z),s(z))
| r(s(z),s(z))
| r(s(s(z)),s(z))
| ~ b(s(z),z)
| ~ b(s(s(z)),z) ),
inference(instantiation,[status(thm)],[c_17717]) ).
tcf(c_18181,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(z)))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(X2)))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_4339]) ).
tcf(c_18195,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(z)))),X1)
| ~ r(s(s(s(s(s(X0))))),X2)
| ~ r(s(s(s(s(s(X0))))),X1)
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_18206,plain,
( ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18195]) ).
tcf(c_18214,plain,
( ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18181]) ).
tcf(c_18474,plain,
! [X0: $i] :
( b(s(z),s(s(X0)))
| r(s(z),s(s(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_17710,c_56,c_202,c_220,c_239,c_697]) ).
tcf(c_18476,plain,
( b(s(z),s(s(z)))
| r(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_18474]) ).
tcf(c_18524,plain,
! [X0: $i,X1: $i] :
( b(X1,s(z))
| r(X1,s(z))
| b(s(s(X0)),X1)
| r(s(s(X0)),X1) ),
inference(resolution,[status(thm)],[c_2336,c_56]) ).
tcf(c_18817,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_13376]) ).
tcf(c_18824,plain,
! [X0: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_11728]) ).
tcf(c_18825,plain,
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_18824]) ).
tcf(c_18831,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_18817]) ).
tcf(c_19062,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_13882]) ).
tcf(c_19256,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = X1 )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_19257,plain,
( ( s(s(z)) = z )
| ( s(s(s(z))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_19256]) ).
tcf(c_19321,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(s(s(X1))) )
| ( s(s(X0)) != s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_1383]) ).
tcf(c_19322,plain,
( ( s(z) = s(s(s(z))) )
| ( s(s(z)) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_19321]) ).
tcf(c_19377,plain,
! [X0: $i] :
( ( s(z) = s(s(s(X0))) )
| ( s(s(z)) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_2207]) ).
tcf(c_19426,plain,
! [X0: $i] :
( ( s(s(s(s(X0)))) = s(z) )
| ( s(s(s(s(s(X0))))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_10564]) ).
tcf(c_19427,plain,
( ( s(s(s(s(z)))) = s(z) )
| ( s(s(s(s(s(z))))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_19426]) ).
tcf(c_19589,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(s(X1)) )
| ( s(X0) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_20351,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14570]) ).
tcf(c_20352,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_20351]) ).
tcf(c_20374,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14581]) ).
tcf(c_20385,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),X2)
| ~ b(s(X1),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14592]) ).
tcf(c_20573,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(z)))),X2)
| ~ b(s(s(s(s(z)))),X1)
| ~ b(s(s(s(s(s(X0))))),X1)
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14644]) ).
tcf(c_20574,plain,
( ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_20573]) ).
tcf(c_21153,plain,
! [X0: $i] :
( b(s(s(s(s(s(X0))))),s(s(s(z))))
| r(s(s(s(s(s(X0))))),s(s(s(z))))
| ( s(s(s(s(s(X0))))) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_2189]) ).
tcf(c_21154,plain,
( b(s(s(s(s(s(z))))),s(s(s(z))))
| r(s(s(s(s(s(z))))),s(s(s(z))))
| ( s(s(s(s(s(z))))) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_21153]) ).
tcf(c_21900,plain,
! [X0: $i] :
( b(s(s(X0)),s(z))
| r(s(s(X0)),s(z))
| r(s(s(X0)),s(s(X0))) ),
inference(resolution,[status(thm)],[c_18524,c_59]) ).
tcf(c_22161,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(X1)))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_15769]) ).
tcf(c_22162,plain,
( ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_22161]) ).
tcf(c_22483,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(s(X0))))),s(X1))
| r(s(s(s(s(s(X0))))),s(X1))
| ( s(s(s(s(s(X0))))) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_22484,plain,
( b(s(s(s(s(s(z))))),s(z))
| r(s(s(s(s(s(z))))),s(z))
| ( s(s(s(s(s(z))))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_22483]) ).
tcf(c_23383,plain,
! [X0: $i] :
( ~ b(s(s(s(s(s(X0))))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16510]) ).
tcf(c_23384,plain,
( ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_23383]) ).
tcf(c_23394,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(X3))
| ~ r(s(s(s(s(X0)))),s(X3))
| ~ r(s(s(X2)),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_12246]) ).
tcf(c_23395,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_23394]) ).
tcf(c_23567,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(s(X1))))),z)
| ~ r(s(s(s(s(s(X1))))),s(s(s(X2))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_17120]) ).
tcf(c_23568,plain,
( ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(s(s(z))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_23567]) ).
tcf(c_24168,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(X3,s(s(X1)))
| ~ r(X3,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(X2))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_13103]) ).
tcf(c_24194,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),X2)
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2968]) ).
tcf(c_24201,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X1)),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2625]) ).
tcf(c_24206,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(z))
| ~ b(s(s(z)),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2378]) ).
tcf(c_24211,plain,
! [X0: $i] :
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(s(X0))))),z)
| ~ b(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2386]) ).
tcf(c_24214,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_24211]) ).
tcf(c_24215,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_24206]) ).
tcf(c_24220,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_24194]) ).
tcf(c_24299,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(s(s(X1))))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_2623]) ).
tcf(c_24300,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_24299]) ).
tcf(c_24367,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),s(s(z)))
| ~ b(s(X1),s(s(X2)))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10684]) ).
tcf(c_24382,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_24367]) ).
tcf(c_24506,plain,
! [X0: $i] :
( ( s(z) = s(s(s(s(X0)))) )
| ( s(s(z)) != s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_19377]) ).
tcf(c_24507,plain,
( ( s(z) = s(s(s(s(z)))) )
| ( s(s(z)) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_24506]) ).
tcf(c_24532,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(X2))
| ~ r(s(s(s(s(s(X0))))),X1)
| ~ r(s(s(s(s(s(X0))))),s(z)) ),
inference(instantiation,[status(thm)],[c_15865]) ).
tcf(c_24533,plain,
( ~ r(z,s(z))
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(z)) ),
inference(instantiation,[status(thm)],[c_24532]) ).
tcf(c_24756,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(s(s(z)))))
| ~ r(s(s(s(X1))),s(s(s(s(X2)))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16454]) ).
tcf(c_24757,plain,
( ~ r(s(s(s(z))),s(s(s(s(z)))))
| ~ r(s(s(s(s(s(z))))),s(s(s(z))))
| ~ r(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_24756]) ).
tcf(c_24909,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17153]) ).
tcf(c_24910,plain,
( ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_24909]) ).
tcf(c_24968,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(s(X0))))),X1)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_17162]) ).
tcf(c_24969,plain,
( ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_24968]) ).
tcf(c_25159,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),s(X2))
| ~ b(s(s(s(s(s(X1))))),s(X3))
| ~ b(s(s(s(s(s(X1))))),s(X2))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_5091]) ).
tcf(c_25161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(X2),s(s(s(s(s(X1))))))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_5065]) ).
tcf(c_25165,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),s(z))
| ~ b(s(s(s(s(s(X1))))),s(z))
| ~ b(s(s(s(s(s(X1))))),s(X2))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_5333]) ).
tcf(c_25182,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),X2)
| ~ b(s(s(s(s(s(X1))))),z)
| ~ b(s(s(s(s(s(X1))))),X2)
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_25188,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_25165]) ).
tcf(c_25195,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),s(s(s(s(s(X1))))))
| r(s(s(s(X0))),s(s(s(s(s(X1))))))
| ( s(s(s(X0))) = s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_17541]) ).
tcf(c_25196,plain,
( b(s(s(s(z))),s(s(s(s(s(z))))))
| r(s(s(s(z))),s(s(s(s(s(z))))))
| ( s(s(s(z))) = s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_25195]) ).
tcf(c_25209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X2)),s(s(X0)))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_5080]) ).
tcf(c_25239,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(X2)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_13269]) ).
tcf(c_25240,plain,
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_25239]) ).
tcf(c_25859,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),X1)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_17162]) ).
tcf(c_25860,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_17153]) ).
tcf(c_25886,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X1)),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_13267]) ).
tcf(c_25909,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_25860]) ).
tcf(c_25910,plain,
( ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_25859]) ).
tcf(c_25960,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(X1)),s(s(s(s(z)))))
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_19062]) ).
tcf(c_25961,plain,
( ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_25960]) ).
tcf(c_25970,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(s(s(s(s(X1))))))
| r(s(X0),s(s(s(s(s(X1))))))
| ( s(X0) = s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_6160]) ).
tcf(c_25971,plain,
( b(s(z),s(s(s(s(s(z))))))
| r(s(z),s(s(s(s(s(z))))))
| ( s(z) = s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_25970]) ).
tcf(c_26145,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(X1)),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_20385]) ).
tcf(c_26146,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_26145]) ).
tcf(c_27199,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(X1)))
| ~ b(s(s(X2)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_20374]) ).
tcf(c_27303,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(s(s(X1))))))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_17285]) ).
tcf(c_27304,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_27303]) ).
tcf(c_29241,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(s(X1))))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_24299]) ).
tcf(c_29242,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_29241]) ).
tcf(c_29447,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(X1))),s(s(s(s(z)))))
| ~ b(s(s(s(X1))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_25886]) ).
tcf(c_29448,plain,
( ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_29447]) ).
tcf(c_29710,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = X1 )
| ( s(s(s(s(s(X0))))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_19256]) ).
tcf(c_29717,plain,
( ( s(s(s(s(z)))) = z )
| ( s(s(s(s(s(z))))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_29710]) ).
tcf(c_30267,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),s(X3))
| ~ r(s(s(s(s(s(X0))))),s(X3))
| ~ r(s(s(X2)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_23394]) ).
tcf(c_30268,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_30267]) ).
tcf(c_30717,plain,
! [X0: $i] :
( ( s(s(s(s(X0)))) = s(s(z)) )
| ( s(s(s(s(s(X0))))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1376]) ).
tcf(c_30718,plain,
( ( s(s(s(s(z)))) = s(s(z)) )
| ( s(s(s(s(s(z))))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_30717]) ).
tcf(c_31654,plain,
! [X0: $i] : s(s(s(s(s(X0))))) != z,
inference(instantiation,[status(thm)],[c_9645]) ).
tcf(c_31655,plain,
s(s(s(s(s(z))))) != z,
inference(instantiation,[status(thm)],[c_31654]) ).
tcf(c_31691,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(s(s(s(X1)))) )
| ( s(X0) != s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_19589]) ).
tcf(c_31692,plain,
( ( z = s(s(s(s(z)))) )
| ( s(z) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_31691]) ).
tcf(c_31933,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_24201]) ).
tcf(c_31934,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_31933]) ).
tcf(c_32943,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(X2)),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_4891]) ).
tcf(c_32949,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(s(s(X1))))),s(s(X3)))
| ~ r(s(s(s(s(s(X1))))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_4339]) ).
tcf(c_32957,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X2),s(s(X3)))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(X2),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_2828]) ).
tcf(c_32963,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(s(s(X1))))),X3)
| ~ r(s(s(s(s(s(X1))))),X2)
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_32964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(s(s(X1))))),s(X3))
| ~ r(s(s(s(s(s(X1))))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_32966,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(s(X0))),X3)
| ~ r(s(s(s(s(s(X1))))),X3)
| ~ r(s(s(s(s(s(X1))))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_1524]) ).
tcf(c_32971,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32966]) ).
tcf(c_32972,plain,
( ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32964]) ).
tcf(c_32973,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32963]) ).
tcf(c_32976,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(s(s(z))),s(z))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32957]) ).
tcf(c_32981,plain,
( ~ r(s(s(s(z))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32949]) ).
tcf(c_32984,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(z))),s(s(z)))
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32943]) ).
tcf(c_33080,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X2)),X3)
| ~ r(s(s(s(X0))),X3)
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_8512]) ).
tcf(c_33089,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_33080]) ).
tcf(c_35869,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(X3),s(s(X1)))
| ~ r(s(X3),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(X2))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_24168]) ).
tcf(c_35870,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_35869]) ).
tcf(c_35966,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(s(s(s(X1)))) )
| ( s(s(s(X0))) != s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_6977]) ).
tcf(c_35967,plain,
( ( s(s(z)) = s(s(s(s(z)))) )
| ( s(s(s(z))) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_35966]) ).
tcf(c_36558,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(s(s(X1))))),z)
| ~ b(s(s(s(s(s(X1))))),X2)
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_25182]) ).
tcf(c_36559,plain,
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_36558]) ).
tcf(c_36630,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(s(s(X1))))),s(X3))
| ~ b(s(s(s(s(s(X1))))),s(X2))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_25159]) ).
tcf(c_36631,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_36630]) ).
tcf(c_36662,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(X2),s(s(s(s(s(X1))))))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_25161]) ).
tcf(c_36663,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(z))),s(z))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_36662]) ).
tcf(c_36920,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(X2)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_27199]) ).
tcf(c_36921,plain,
( ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_36920]) ).
tcf(c_36978,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(X0))),s(X3))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_25209]) ).
tcf(c_36979,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_36978]) ).
tcf(c_37765,plain,
! [X0: $i] :
( b(s(s(X0)),s(z))
| r(s(s(X0)),s(z)) ),
inference(global_subsumption_just,[status(thm)],[c_21900,c_56,c_190,c_196]) ).
tcf(c_37767,plain,
( b(s(s(z)),s(z))
| r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_37765]) ).
tcf(c_37786,plain,
! [X0: $i,X1: $i] :
( r(z,s(z))
| r(z,s(X1))
| r(s(s(X0)),s(z))
| ~ b(s(s(X0)),z) ),
inference(resolution,[status(thm)],[c_37765,c_2938]) ).
tcf(c_37787,plain,
( r(z,s(z))
| r(s(s(z)),s(z))
| ~ b(s(s(z)),z) ),
inference(instantiation,[status(thm)],[c_37786]) ).
tcf(c_38789,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2623]) ).
tcf(c_38790,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_38789]) ).
tcf(c_38791,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(s(X1)))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_2623]) ).
tcf(c_38792,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_38791]) ).
tcf(c_39561,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),s(z))
| ~ b(s(s(s(X1))),s(z))
| ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5333]) ).
tcf(c_39578,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),X2)
| ~ b(s(s(s(X1))),z)
| ~ b(s(s(s(X1))),X2)
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_39579,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_39578]) ).
tcf(c_39585,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_39561]) ).
tcf(c_39778,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r(s(s(X0)),X2)
| ~ r(s(s(s(X1))),X3)
| ~ r(s(s(s(X1))),X2)
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1942]) ).
tcf(c_39779,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_39778]) ).
tcf(c_40161,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(X1))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2452]) ).
tcf(c_40162,plain,
( ~ b(z,s(z))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_40161]) ).
tcf(c_40168,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(z,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(z))
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2481]) ).
tcf(c_40169,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_40168]) ).
tcf(c_40642,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2004]) ).
tcf(c_40644,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_40642]) ).
tcf(c_41730,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_40644,c_40169,c_40162,c_39779,c_39585,c_39579,c_38792,c_38790,c_37787,c_37767,c_36979,c_36921,c_36663,c_36631,c_36559,c_35967,c_35870,c_33089,c_32984,c_32981,c_32976,c_32973,c_32972,c_32971,c_31934,c_31692,c_31655,c_30718,c_30268,c_29717,c_29448,c_29242,c_27304,c_26146,c_25971,c_25961,c_25910,c_25909,c_25240,c_25196,c_25188,c_24969,c_24910,c_24757,c_24533,c_24507,c_24382,c_24300,c_24220,c_24215,c_24214,c_23568,c_23395,c_23384,c_22484,c_22162,c_21154,c_20574,c_20352,c_19427,c_19322,c_19257,c_18831,c_18825,c_18476,c_18214,c_18206,c_17719,c_17661,c_17634,c_17574,c_17538,c_16815,c_16369,c_16278,c_16082,c_16028,c_15974,c_15797,c_15666,c_15471,c_15352,c_15330,c_14376,c_14254,c_14148,c_14147,c_14145,c_14137,c_14136,c_13399,c_13377,c_13037,c_12234,c_12231,c_12198,c_12106,c_11450,c_10989,c_10962,c_10941,c_10712,c_10710,c_10708,c_10565,c_10332,c_10330,c_10329,c_10325,c_9646,c_9171,c_8731,c_8239,c_8238,c_8236,c_8235,c_7964,c_7460,c_7431,c_7421,c_6978,c_6967,c_6922,c_6906,c_6771,c_6400,c_6347,c_6161,c_6001,c_5878,c_5674,c_5530,c_4456,c_4455,c_3456,c_2942,c_2703,c_2652,c_2557,c_2379,c_2190,c_1924,c_1884,c_1541,c_1384,c_1377,c_1088,c_1025,c_919,c_869,c_856,c_817,c_684,c_675,c_571,c_539,c_411,c_371,c_367,c_330,c_253,c_242,c_241,c_238,c_231,c_221,c_203,c_198,c_197,c_193,c_192,c_65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA126-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Wed Sep 23 12:53:56 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.43
% 0.12/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.43
% 0.12/0.43 % Detected problem language: tptp
% 0.12/0.44 % Proving...
% 14.30/2.80 % SZS status Started for theBenchmark.p
% 14.30/2.80 % SZS status Unsatisfiable for theBenchmark.p
% 14.30/2.80
% 14.30/2.80 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.30/2.80
% 14.30/2.80 % ------ iProver source info
% 14.30/2.80
% 14.30/2.80 % git: date: 2026-07-19 20:42:38 +0200
% 14.30/2.80 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.30/2.80 % git: non_committed_changes: false
% 14.30/2.80
% 14.30/2.80 % ------ Parsing...% successful
% 14.30/2.80
% 14.30/2.80
% 14.30/2.80 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.30/2.80
% 14.30/2.80 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 14.30/2.80
% 14.30/2.80 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 14.30/2.80
% 14.30/2.80 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 14.30/2.80 % ------ Proving...
% 14.30/2.80 % ------ Problem Properties
% 14.30/2.80
% 14.30/2.80 %
% 14.30/2.80 % clauses 7
% 14.30/2.80 % conjectures 0
% 14.30/2.80 % EPR 5
% 14.30/2.80 % Horn 6
% 14.30/2.80 % unary 3
% 14.30/2.80 % binary 1
% 14.30/2.80 % lits 16
% 14.30/2.80 % lits eq 4
% 14.30/2.80 % fd_pure 0
% 14.30/2.80 % fd_pseudo 0
% 14.30/2.80 % fd_cond 0
% 14.30/2.80 % fd_pseudo_cond 2
% 14.30/2.80 % AC symbols 0
% 14.30/2.80
% 14.30/2.80 % ------ Input Options Time Limit: Unbounded
% 14.30/2.80
% 14.30/2.80
% 14.30/2.80 % ------
% 14.30/2.80 % Current options:
% 14.30/2.80 % ------
% 14.30/2.80
% 14.30/2.80
% 14.30/2.80 %
% 14.30/2.80
% 14.30/2.80 % ------ Proving...
% 14.30/2.80 %
% 14.30/2.80
% 14.30/2.80 % SZS status Unsatisfiable for theBenchmark.p
% 14.30/2.80
% 14.30/2.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.30/2.81
% 14.30/2.81
%------------------------------------------------------------------------------