%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRA164-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n004.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:24:25 PM UTC 2026
% Result : Unsatisfiable 14.13s 2.70s
% Output : CNFRefutation 14.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 800 ( 25 unt; 0 def)
% Number of atoms : 2937 ( 323 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 4662 (2525 ~;2137 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 1420 ( 0 sgn1420 !; 0 ?;1407 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : s(X0) != z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snz) ).
fof(f2,axiom,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sinj) ).
fof(f4,axiom,
! [X0] : ~ b(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bi) ).
fof(f5,axiom,
! [X0,X1] :
( b(X0,X1)
| r(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rb) ).
fof(f6,axiom,
! [X2,X0,X1] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axr) ).
fof(f7,axiom,
! [X2,X3,X0,X1] :
( ~ b(X2,X3)
| ~ b(X0,X3)
| ~ b(X1,X2)
| ~ b(X0,X2)
| ~ b(X0,X1) ),
file('/export/starexec/sandbox2/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_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] :
( ~ 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(X2,X3)
| ~ b(X1,X2)
| ~ b(X0,X3)
| ~ 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_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_199,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(z) )
| ( s(z) != X1 )
| ( s(s(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_105]) ).
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] :
( ~ r(X0,z)
| ~ r(s(X1),z)
| ~ r(X0,s(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_225,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = X1 )
| ( X1 != s(X0) )
| ( s(X0) != s(X0) ) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(X0)))
| ~ r(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_228,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(z)))
| ~ r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,X1)
| ~ r(X2,s(X0))
| ~ r(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_233,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_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] :
( b(s(s(X0)),z)
| r(s(s(X0)),z)
| ( s(s(X0)) = z ) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_240,plain,
( b(s(s(z)),z)
| r(s(s(z)),z)
| ( s(s(z)) = z ) ),
inference(instantiation,[status(thm)],[c_239]) ).
tcf(c_242,plain,
! [X0: $i] :
( ( z = s(X0) )
| ( s(z) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_243,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0))
| ( z = s(X0) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_244,plain,
( b(z,s(z))
| r(z,s(z))
| ( z = s(z) ) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_245,plain,
( ( z = s(z) )
| ( s(z) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_242]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(X1) )
| ( s(X0) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_255,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] :
( ~ r(s(X1),s(z))
| ~ r(s(s(X0)),s(z))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_260,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X0,z)
| ~ b(X0,X2)
| ~ b(s(X1),z)
| ~ b(X2,s(X1))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_262,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X2,X1)
| ~ b(X3,s(X0))
| ~ b(X2,s(X0))
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X0) = X2 )
| ( X2 != s(X1) )
| ( s(X0) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_269,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_233]) ).
tcf(c_270,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_269]) ).
tcf(c_271,plain,
! [X0: $i] :
( b(s(z),s(X0))
| r(s(z),s(X0))
| ( s(z) = s(X0) ) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),s(X1))
| r(s(s(X0)),s(X1))
| ( s(s(X0)) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(X1) )
| ( s(X1) != s(X0) )
| ( s(X0) != s(X0) ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X0) = s(X2) )
| ( s(X2) != s(X1) )
| ( s(X0) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_319,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_233]) ).
tcf(c_320,plain,
( b(s(z),s(s(z)))
| r(s(z),s(s(z)))
| ( s(z) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_327,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_258]) ).
tcf(c_346,plain,
! [X0: $i] :
( ( s(z) = s(X0) )
| ( s(z) != s(z) )
| ( s(X0) != s(z) ) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(X1) )
| ( s(X1) != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_353,plain,
! [X0: $i] : s(s(X0)) != z,
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_354,plain,
s(s(z)) != z,
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(X1))
| ~ b(X3,s(X0))
| ~ b(s(X1),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_262]) ).
tcf(c_364,plain,
! [X0: $i] :
( b(z,s(s(X0)))
| r(z,s(s(X0)))
| ( z = s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_365,plain,
( b(z,s(s(z)))
| r(z,s(s(z)))
| ( z = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_364]) ).
tcf(c_366,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(X0))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(z)))
| ~ r(s(s(s(X0))),s(X1))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_377,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_376]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(z) )
| ( s(z) != s(X1) )
| ( s(s(X0)) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_385,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_271]) ).
tcf(c_389,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X0,X2)
| ~ r(X2,s(X1))
| ~ r(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_390,plain,
! [X0: $i,X1: $i] :
( b(X0,s(s(X1)))
| r(X0,s(s(X1)))
| ( X0 = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_391,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X1))
| ~ r(X2,s(X0))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_396,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_272]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X0)) = s(X2) )
| ( s(X2) != s(X1) )
| ( s(s(X0)) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_448,plain,
! [X0: $i] :
( ( s(z) = s(s(X0)) )
| ( s(z) != s(z) )
| ( s(s(X0)) != s(z) ) ),
inference(instantiation,[status(thm)],[c_346]) ).
tcf(c_456,plain,
! [X0: $i] :
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_457,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_456]) ).
tcf(c_485,plain,
! [X0: $i] :
( b(s(X0),z)
| r(s(X0),z) ),
inference(resolution,[status(thm)],[c_60,c_56]) ).
tcf(c_486,plain,
( b(s(z),z)
| r(s(z),z) ),
inference(instantiation,[status(thm)],[c_485]) ).
tcf(c_489,plain,
! [X0: $i] :
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_490,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(z))))
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_489]) ).
tcf(c_491,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(X0)))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_529,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(z)))
| ~ r(X1,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_391]) ).
tcf(c_533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X1),X3)
| ~ b(s(X2),s(X1))
| ~ b(s(X2),s(X0))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_539,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(s(s(X0)),z)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_389]) ).
tcf(c_540,plain,
( ~ r(z,s(z))
| ~ r(s(s(z)),z)
| ~ r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_539]) ).
tcf(c_543,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),z)
| ~ r(s(s(X0)),z)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_558,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(X1))
| r(s(X0),s(X1))
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_57,c_60]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(X0)))
| ~ r(s(z),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_391]) ).
tcf(c_565,plain,
! [X0: $i] :
( ~ r(z,s(z))
| ~ r(z,s(s(X0)))
| ~ r(s(z),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_566,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(z)))
| ~ r(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_565]) ).
tcf(c_587,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X0))
| ~ r(X2,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_391]) ).
tcf(c_598,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(X1) )
| ( s(s(X0)) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_604,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_396]) ).
tcf(c_605,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_604]) ).
tcf(c_624,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_625,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_105,c_103]) ).
tcf(c_648,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_390]) ).
tcf(c_649,plain,
( b(z,s(s(s(z))))
| r(z,s(s(s(z))))
| ( z = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_679,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X0)) = s(X2) )
| ( s(X2) != s(s(X1)) )
| ( s(s(X0)) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_713,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(s(z)) )
| ( s(s(s(s(X0)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_598]) ).
tcf(c_714,plain,
( ( s(s(s(z))) = s(s(z)) )
| ( s(s(s(s(z)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_716,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(X1) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_598]) ).
tcf(c_719,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(s(X1)) )
| ( s(s(X0)) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_598]) ).
tcf(c_720,plain,
( ( s(z) = s(s(z)) )
| ( s(s(z)) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_719]) ).
tcf(c_734,plain,
! [X0: $i] : s(s(s(X0))) = s(s(s(X0))),
inference(instantiation,[status(thm)],[c_237]) ).
tcf(c_735,plain,
s(s(s(z))) = s(s(s(z))),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_743,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(z,s(s(X0)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_491]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] :
( b(X0,s(s(s(X1))))
| r(X0,s(s(s(X1))))
| ( X0 = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_747,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(z)))
| ~ r(s(X1),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_529]) ).
tcf(c_748,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(z))))
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_747]) ).
tcf(c_755,plain,
! [X0: $i,X1: $i] :
( b(X1,X0)
| r(X1,X0)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_625,c_60]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(s(s(X0)),z)
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_539]) ).
tcf(c_760,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),z)
| ~ r(s(s(X0)),z)
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_543]) ).
tcf(c_812,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X1)))
| ~ r(X2,s(s(X0)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_587]) ).
tcf(c_825,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0)) ),
inference(resolution,[status(thm)],[c_755,c_56]) ).
tcf(c_826,plain,
( b(z,s(z))
| r(z,s(z)) ),
inference(instantiation,[status(thm)],[c_825]) ).
tcf(c_849,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),X2)
| ~ b(s(X1),s(z))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_533]) ).
tcf(c_851,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_533]) ).
tcf(c_853,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),z)
| ~ b(s(X0),z)
| ~ b(X2,s(X1))
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_857,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X1))
| ~ b(s(X0),z)
| ~ b(s(X1),X2)
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_262]) ).
tcf(c_859,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X1))
| ~ b(s(X1),X2)
| ~ b(s(X0),X3)
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_262]) ).
tcf(c_864,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X2,s(X1))
| ~ b(s(X1),X3)
| ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_867,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X0,X3)
| ~ b(X0,X2)
| ~ b(X2,s(X1))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_930,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X0)) = s(s(X2)) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(X0)) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_1051,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_396]) ).
tcf(c_1098,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),X2)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X1)),s(z))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_1133,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),z)
| ~ b(X2,s(X1))
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_1137,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X1))
| ~ b(s(X1),X2)
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_857]) ).
tcf(c_1148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(X0)),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_851]) ).
tcf(c_1159,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X1))
| ~ b(s(X1),X2)
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_859]) ).
tcf(c_1171,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(s(X1),z)
| ~ b(X0,z)
| ~ b(X0,X2)
| ~ b(X2,s(X1))
| ~ b(X0,s(X1)) ),
inference(resolution,[status(thm)],[c_62,c_485]) ).
tcf(c_1172,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r(s(X1),s(X2))
| ( X1 = X2 )
| ~ b(X0,X3)
| ~ b(X3,s(X1))
| ~ b(X0,s(X2))
| ~ b(X0,s(X1)) ),
inference(resolution,[status(thm)],[c_62,c_558]) ).
tcf(c_1177,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,X2)
| ~ b(z,s(X1))
| ~ b(s(X1),X2)
| ~ b(z,s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_864]) ).
tcf(c_1180,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(z))
| ~ b(X1,s(X2))
| ~ b(s(z),s(X2))
| ~ b(X1,s(s(X0)))
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_867]) ).
tcf(c_1182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X1)
| ~ b(X2,s(X3))
| ~ b(X2,s(X0))
| ~ b(X1,s(X3))
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_867]) ).
tcf(c_1185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X3,s(X0))
| ~ b(X2,s(X1))
| ~ b(X2,s(X0))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_867]) ).
tcf(c_1204,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(z)))
| ~ r(X1,s(s(s(X0))))
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_812]) ).
tcf(c_1205,plain,
! [X0: $i] :
( ~ r(s(s(z)),z)
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_760]) ).
tcf(c_1206,plain,
! [X0: $i] :
( ~ r(s(s(z)),z)
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_757]) ).
tcf(c_1207,plain,
! [X0: $i] :
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_1208,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_327]) ).
tcf(c_1209,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_1208]) ).
tcf(c_1210,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(z))))
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1207]) ).
tcf(c_1211,plain,
( ~ r(s(s(z)),z)
| ~ r(z,s(s(s(z))))
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_1212,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_1205]) ).
tcf(c_1223,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_746]) ).
tcf(c_1224,plain,
( b(s(z),s(s(s(z))))
| r(s(z),s(s(s(z))))
| ( s(z) = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_1223]) ).
tcf(c_1323,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = s(s(X2)) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_1364,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(z)))
| ~ r(s(X1),s(s(s(X0))))
| ~ r(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_1204]) ).
tcf(c_1365,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1364]) ).
tcf(c_1370,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(X2))
| ~ b(s(s(X1)),s(z))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1098]) ).
tcf(c_1383,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_624,c_60]) ).
tcf(c_1384,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_624,c_755]) ).
tcf(c_1386,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(X1))
| ~ b(z,s(s(X0)))
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1177]) ).
tcf(c_1409,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X0)))
| ~ r(X2,s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_812]) ).
tcf(c_1412,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X0)))
| ~ r(z,s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_1413,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(s(s(X1))),s(z))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_1414,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_1051]) ).
tcf(c_1452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1148]) ).
tcf(c_1454,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),X2)
| ~ b(X2,s(s(s(X1))))
| ~ b(s(s(X0)),s(s(z)))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1159]) ).
tcf(c_1455,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X0)),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_1159]) ).
tcf(c_1456,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X1))
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1159]) ).
tcf(c_1476,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_1383,c_57]) ).
tcf(c_1486,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(X2))
| ~ b(X1,s(s(z)))
| ~ b(s(s(z)),s(X2))
| ~ b(X1,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_1488,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(X1))
| ~ b(X3,s(s(X0)))
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_1489,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(X1))
| ~ b(X3,s(X0))
| ~ b(s(X1),s(X2))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_1493,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,X2)
| ~ b(X1,s(s(z)))
| ~ b(X2,s(s(s(X0))))
| ~ b(X1,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1185]) ).
tcf(c_1494,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X2,s(X1))
| ~ b(X3,s(s(X0)))
| ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1185]) ).
tcf(c_1497,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_389]) ).
tcf(c_1500,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),z)
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_1510,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),z)
| ~ b(s(s(X0)),z)
| ~ b(X2,s(s(X1)))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1133]) ).
tcf(c_1517,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(X1)))
| ~ b(s(s(X1)),z)
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1137]) ).
tcf(c_1520,plain,
! [X0: $i] :
( ( s(s(X0)) = z )
| ( z != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_1521,plain,
( ( s(s(z)) = z )
| ( z != s(s(z)) )
| ( s(s(z)) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_1520]) ).
tcf(c_1529,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X1))
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_389]) ).
tcf(c_1538,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),X2)
| ~ r(s(X0),X2)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1558,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = X1 )
| ( X1 != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1710,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(s(X1))))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1412]) ).
tcf(c_1714,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X0),z)
| ~ r(z,s(s(s(X1))))
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1497]) ).
tcf(c_1718,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X0),z)
| ~ r(s(s(s(X1))),z)
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1500]) ).
tcf(c_1765,plain,
! [X0: $i] :
( ~ b(z,s(s(z)))
| ~ b(s(s(z)),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_1766,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1765]) ).
tcf(c_1769,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(X1)))
| ~ b(s(s(X1)),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_1770,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_1409]) ).
tcf(c_1771,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(s(X1))))
| ~ r(X2,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_1789,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(s(X1))),X2)
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_1806,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_1414]) ).
tcf(c_1807,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_1806]) ).
tcf(c_1812,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(s(X1)) )
| ( s(s(s(X0))) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_1827,plain,
! [X0: $i] :
( b(s(s(s(z))),s(s(s(X0))))
| r(s(s(s(z))),s(s(s(X0))))
| ( s(s(s(z))) = s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_1414]) ).
tcf(c_1834,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_272]) ).
tcf(c_1835,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_1834]) ).
tcf(c_1837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1452]) ).
tcf(c_1868,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(z)))
| ~ b(z,s(s(X0)))
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1386]) ).
tcf(c_1869,plain,
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1868]) ).
tcf(c_1900,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(X1))))
| ~ b(s(s(s(X0))),X2)
| ~ 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_1454]) ).
tcf(c_1902,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(s(s(z)),s(X1))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(X1))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_1904,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_1918,plain,
! [X0: $i,X1: $i] :
( r(z,s(X1))
| r(s(X1),z)
| ~ b(X0,z)
| ~ b(X0,s(X1)) ),
inference(resolution,[status(thm)],[c_1171,c_825]) ).
tcf(c_1922,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),z)
| ~ b(X2,s(s(X1)))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1510]) ).
tcf(c_1931,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X0),X3)
| ~ b(s(X0),X2)
| ~ b(X3,s(s(X1)))
| ~ b(s(s(X1)),X2)
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_859]) ).
tcf(c_1934,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(X0))
| ~ b(X3,s(s(X1)))
| ~ b(s(s(X1)),X2)
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_1966,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(X2,s(s(X0)))
| ~ b(X2,s(s(s(X1))))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1493]) ).
tcf(c_1967,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(s(z)))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1493]) ).
tcf(c_1982,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1488]) ).
tcf(c_1983,plain,
( ~ b(s(z),s(s(z)))
| ~ 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_1982]) ).
tcf(c_1984,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(X3))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1488]) ).
tcf(c_1985,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(X1))
| ~ b(s(X3),s(s(X2)))
| ~ b(s(X3),s(s(X0)))
| ~ b(s(X1),s(s(X2)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1488]) ).
tcf(c_1994,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(X3,s(s(X0)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_2006,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(s(X1),X3)
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_2012,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X1)))
| ~ b(s(s(X1)),s(X2))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1456]) ).
tcf(c_2020,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),s(X2))
| ~ b(s(X2),s(s(z)))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(X1))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1489]) ).
tcf(c_2022,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(X3))
| ~ b(s(X1),s(X2))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1489]) ).
tcf(c_2023,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(X0))
| ~ b(s(X2),s(X3))
| ~ b(s(X2),s(X0))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1489]) ).
tcf(c_2061,plain,
! [X0: $i] :
( ~ r(z,s(z))
| ~ r(z,s(s(s(X0))))
| ~ r(s(z),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_565]) ).
tcf(c_2062,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(s(z))))
| ~ r(s(z),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2061]) ).
tcf(c_2065,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_491]) ).
tcf(c_2066,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(s(z))))
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_2065]) ).
tcf(c_2068,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(s(X0))))
| ~ r(s(z),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_2070,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X0))
| ~ r(X2,s(s(s(X1))))
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_587]) ).
tcf(c_2169,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(s(X2)))
| ~ b(s(s(X1)),s(z))
| ~ b(s(s(X0)),s(z))
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1370]) ).
tcf(c_2170,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(z))
| ~ b(X2,s(s(X1)))
| ~ b(X2,s(s(X0)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_1180]) ).
tcf(c_2173,plain,
! [X0: $i] :
( b(s(z),s(s(s(X0))))
| r(s(z),s(s(s(X0))))
| ( s(z) = s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_2205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X3,s(s(X0)))
| ~ b(X2,s(s(X1)))
| ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_2206,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(X0)))
| ~ b(s(s(X1)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_864]) ).
tcf(c_2211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X1)),X2)
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1159]) ).
tcf(c_2221,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X1))
| ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X0)))
| ~ b(s(X1),s(s(X2)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_1488]) ).
tcf(c_2257,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_239]) ).
tcf(c_2258,plain,
( b(s(s(s(z))),z)
| r(s(s(s(z))),z)
| ( s(s(s(z))) = z ) ),
inference(instantiation,[status(thm)],[c_2257]) ).
tcf(c_2405,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_1812]) ).
tcf(c_2406,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_2405]) ).
tcf(c_2407,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_1812]) ).
tcf(c_2416,plain,
! [X0: $i] :
( ( s(s(z)) = s(s(s(X0))) )
| ( s(s(s(z))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_1812]) ).
tcf(c_2417,plain,
( ( s(s(z)) = s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_2416]) ).
tcf(c_2501,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_1770]) ).
tcf(c_2512,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_2070]) ).
tcf(c_2514,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),X2)
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_2515,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X1))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1529]) ).
tcf(c_2516,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),z)
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1500]) ).
tcf(c_2517,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X1))
| ~ r(X2,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_391]) ).
tcf(c_2519,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_2516]) ).
tcf(c_2520,plain,
( ~ r(z,s(z))
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_2515]) ).
tcf(c_2529,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_1789]) ).
tcf(c_2555,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X1))),s(z))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1413]) ).
tcf(c_2568,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),X2)
| ~ b(s(s(s(X0))),X2)
| ~ 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_1837]) ).
tcf(c_2571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1837]) ).
tcf(c_2604,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(z)),s(s(X1)))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1902]) ).
tcf(c_2625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),X3)
| ~ b(X3,s(s(s(X1))))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_2629,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X0)),z)
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(s(X1))),z)
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1517]) ).
tcf(c_2632,plain,
( ~ b(s(s(z)),z)
| ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2629]) ).
tcf(c_2647,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X1))),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1837]) ).
tcf(c_2779,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_1384,c_57]) ).
tcf(c_2796,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1966]) ).
tcf(c_2797,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2796]) ).
tcf(c_2802,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(X1))
| ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_2898,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(X3),s(s(X1)))
| ~ b(s(X3),s(s(X0)))
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1985]) ).
tcf(c_2906,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(X3,s(s(s(X0))))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1994]) ).
tcf(c_2907,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(X3,s(s(X0)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1994]) ).
tcf(c_2912,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X2,s(s(X1)))
| ~ b(X3,s(s(s(X0))))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2205]) ).
tcf(c_2913,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X2,X3)
| ~ b(X3,s(s(X0)))
| ~ b(X2,s(s(X0)))
| ~ b(X2,s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2205]) ).
tcf(c_2919,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),s(X3))
| ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1984]) ).
tcf(c_2932,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),X3)
| ~ b(X3,s(s(X1)))
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2006]) ).
tcf(c_2957,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(X3))
| ~ b(s(X3),s(s(X0)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2023]) ).
tcf(c_2964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,X2)
| ~ b(X3,s(s(X0)))
| ~ b(X3,s(s(s(X1))))
| ~ b(s(s(s(X1))),X2)
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2206]) ).
tcf(c_2974,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2211]) ).
tcf(c_2975,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),X2)
| ~ b(X3,s(s(s(X1))))
| ~ b(s(s(s(X1))),X2)
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2211]) ).
tcf(c_2979,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(X0)))
| ~ b(s(s(X1)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2221]) ).
tcf(c_3060,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(z),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2068]) ).
tcf(c_3061,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(z),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3060]) ).
tcf(c_3129,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(s(z))))
| ~ r(X1,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1771]) ).
tcf(c_3130,plain,
! [X0: $i] :
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_3131,plain,
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3130]) ).
tcf(c_3341,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_1414]) ).
tcf(c_3342,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_3341]) ).
tcf(c_3367,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_1827]) ).
tcf(c_3368,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_3367]) ).
tcf(c_3406,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_648]) ).
tcf(c_3407,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_3406]) ).
tcf(c_3414,plain,
! [X0: $i] : s(s(s(s(X0)))) = s(s(s(s(X0)))),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_3415,plain,
s(s(s(s(z)))) = s(s(s(s(z)))),
inference(instantiation,[status(thm)],[c_3414]) ).
tcf(c_3470,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),s(s(s(s(X1)))))
| r(s(s(s(X0))),s(s(s(s(X1)))))
| ( s(s(s(X0))) = s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_1414]) ).
tcf(c_3559,plain,
! [X0: $i,X1: $i] :
( ~ 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_2512]) ).
tcf(c_3560,plain,
( ~ r(s(z),s(s(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_3559]) ).
tcf(c_3566,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2555]) ).
tcf(c_3567,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_3566]) ).
tcf(c_3584,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3060]) ).
tcf(c_3596,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(z))))
| ~ r(s(X1),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2501]) ).
tcf(c_3597,plain,
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3596]) ).
tcf(c_3604,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_2514]) ).
tcf(c_3612,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X1)))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2515]) ).
tcf(c_3634,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(z))))
| ~ r(s(s(X1)),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3129]) ).
tcf(c_3635,plain,
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3634]) ).
tcf(c_3638,plain,
! [X0: $i,X1: $i] :
( b(X0,s(s(s(s(X1)))))
| r(X0,s(s(s(s(X1)))))
| ( X0 = s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_3641,plain,
! [X0: $i] :
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3129]) ).
tcf(c_3672,plain,
! [X0: $i,X1: $i] :
( ~ 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_2529]) ).
tcf(c_3790,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(z)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2604]) ).
tcf(c_3944,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(s(X1))))
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2906]) ).
tcf(c_3951,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2907]) ).
tcf(c_3953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2912]) ).
tcf(c_3968,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2796]) ).
tcf(c_3976,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(X2))
| ~ 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_2802]) ).
tcf(c_4021,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,X2)
| ~ b(z,s(s(X0)))
| ~ b(X2,s(s(X0)))
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2913]) ).
tcf(c_4037,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,X2)
| ~ b(z,s(s(X0)))
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(s(X1))),X2)
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2964]) ).
tcf(c_4106,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(X1)))
| ~ b(s(s(X1)),X2)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2974]) ).
tcf(c_4114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(s(X1))),X3)
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2975]) ).
tcf(c_4124,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X1))),z)
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1718]) ).
tcf(c_4125,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(s(X1))))
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1714]) ).
tcf(c_4186,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(X3),s(s(X1)))
| ~ b(s(X3),s(s(s(X0))))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2898]) ).
tcf(c_4187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(X3),s(s(X0)))
| ~ b(s(X3),s(s(s(X1))))
| ~ b(s(s(X2)),s(s(X0)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2898]) ).
tcf(c_4216,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X2)),X3)
| ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2932]) ).
tcf(c_4243,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),s(X2))
| ~ b(s(X1),s(s(z)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2957]) ).
tcf(c_4247,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(X3))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X3),s(s(s(X0))))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2957]) ).
tcf(c_4248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(X3))
| ~ b(s(X3),s(s(X0)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2957]) ).
tcf(c_4254,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2979]) ).
tcf(c_4255,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X0)))
| ~ b(X3,s(s(s(X1))))
| ~ b(s(s(X2)),s(s(X0)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2979]) ).
tcf(c_4357,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_196]) ).
tcf(c_4358,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_4357]) ).
tcf(c_4364,plain,
! [X0: $i] :
( b(s(z),s(s(s(s(X0)))))
| r(s(z),s(s(s(s(X0)))))
| ( s(z) = s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_2173]) ).
tcf(c_4365,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_4364]) ).
tcf(c_4558,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),s(s(s(z))))
| ~ r(s(s(s(s(X1)))),s(s(s(z))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3634]) ).
tcf(c_4640,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(s(X1))))
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3612]) ).
tcf(c_4752,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_3638]) ).
tcf(c_4848,plain,
! [X0: $i,X1: $i] :
( ~ 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_2529]) ).
tcf(c_4849,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(s(z)))))
| ~ 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_2501]) ).
tcf(c_4850,plain,
! [X0: $i] :
( ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(s(X0))))),s(z))
| ~ r(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_2555]) ).
tcf(c_4851,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(s(z)))))
| ~ 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_2512]) ).
tcf(c_4855,plain,
( ~ r(s(z),s(s(s(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_4851]) ).
tcf(c_4856,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_4850]) ).
tcf(c_4857,plain,
( ~ r(s(z),s(s(s(s(z)))))
| ~ r(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_4849]) ).
tcf(c_4986,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_4124]) ).
tcf(c_4987,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),s(z))
| ~ r(s(z),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_3584]) ).
tcf(c_4988,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(s(X0)))),s(X1))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_4989,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(z))))
| ~ r(s(X1),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2501]) ).
tcf(c_4990,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2555]) ).
tcf(c_4991,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(X1),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_2512]) ).
tcf(c_4993,plain,
! [X0: $i] :
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_4994,plain,
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4993]) ).
tcf(c_4995,plain,
( ~ r(s(s(s(z))),s(z))
| ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_4991]) ).
tcf(c_4996,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_4990]) ).
tcf(c_4998,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_4986]) ).
tcf(c_5111,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(z)),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3790]) ).
tcf(c_5113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X1))),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2647]) ).
tcf(c_5114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2571]) ).
tcf(c_5115,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ 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_2568]) ).
tcf(c_5116,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),X2)
| ~ 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_1900]) ).
tcf(c_5117,plain,
( ~ b(z,s(s(s(z))))
| ~ b(s(s(s(s(z)))),z)
| ~ 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_5116]) ).
tcf(c_5118,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(z)))),z)
| ~ 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_5115]) ).
tcf(c_5120,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(z)),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_5111]) ).
tcf(c_5181,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),z)
| ~ r(z,s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_4125]) ).
tcf(c_5183,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),s(z))
| ~ r(s(z),s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3584]) ).
tcf(c_5184,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(s(X1)))),s(X2))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_5185,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(s(X0))))
| ~ r(s(X2),s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_2501]) ).
tcf(c_5188,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(s(X0))))
| ~ r(X2,s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1771]) ).
tcf(c_5189,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(s(X0))))
| ~ r(z,s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_5231,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(s(X0)))
| ~ b(z,s(s(s(X1))))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4021]) ).
tcf(c_5232,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(s(z),s(s(z)))
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5231]) ).
tcf(c_5236,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(s(X0)))
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4037]) ).
tcf(c_5237,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5236]) ).
tcf(c_5272,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3944]) ).
tcf(c_5278,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3951]) ).
tcf(c_5316,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3968]) ).
tcf(c_5317,plain,
( ~ b(s(s(z)),s(s(s(z))))
| ~ 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_5316]) ).
tcf(c_5358,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3976]) ).
tcf(c_5359,plain,
( ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),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_5358]) ).
tcf(c_5395,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(s(X1))))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3953]) ).
tcf(c_5418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(s(X1))))
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X3)))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4186]) ).
tcf(c_5447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(X3)))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4187]) ).
tcf(c_5448,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(X0)))
| ~ b(s(s(X2)),s(s(X3)))
| ~ b(s(s(X2)),s(s(X0)))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4187]) ).
tcf(c_5454,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(z)))
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_4243]) ).
tcf(c_5455,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4243]) ).
tcf(c_5505,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),X2)
| ~ b(X2,s(s(X1)))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(z)),s(s(X1)))
| ~ b(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_4216]) ).
tcf(c_5506,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_4216]) ).
tcf(c_5507,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(s(s(X0)),X3)
| ~ b(s(s(s(X1))),X3)
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4216]) ).
tcf(c_5532,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_4247]) ).
tcf(c_5533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(X3),s(s(s(X1))))
| ~ b(s(X3),s(s(s(X0))))
| ~ b(s(s(s(X1))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4247]) ).
tcf(c_5541,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(s(s(X0))),s(X3))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4248]) ).
tcf(c_5560,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(X2,s(s(s(X1))))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4255]) ).
tcf(c_5562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(X2))))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(s(X1)),s(s(s(X2))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_4255]) ).
tcf(c_5563,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(s(X1))))
| ~ b(X3,s(s(s(X0))))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4255]) ).
tcf(c_5757,plain,
! [X0: $i] :
( b(s(s(s(s(s(X0))))),z)
| r(s(s(s(s(s(X0))))),z)
| ( s(s(s(s(s(X0))))) = z ) ),
inference(instantiation,[status(thm)],[c_2257]) ).
tcf(c_5758,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_5757]) ).
tcf(c_5760,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_2257]) ).
tcf(c_5788,plain,
! [X0: $i,X1: $i] :
( ~ 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_4848]) ).
tcf(c_5789,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_5788]) ).
tcf(c_5792,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_1834]) ).
tcf(c_5793,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_5792]) ).
tcf(c_5800,plain,
! [X0: $i,X1: $i] :
( ~ 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_4851]) ).
tcf(c_5817,plain,
! [X0: $i] :
( b(z,s(s(s(s(s(X0))))))
| r(z,s(s(s(s(s(X0))))))
| ( z = s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_3406]) ).
tcf(c_5818,plain,
( b(z,s(s(s(s(s(z))))))
| r(z,s(s(s(s(s(z))))))
| ( z = s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_5817]) ).
tcf(c_5885,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ 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_4849]) ).
tcf(c_5891,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_1223]) ).
tcf(c_5892,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_5891]) ).
tcf(c_5942,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X0))),X2)
| ~ r(X2,s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_4640]) ).
tcf(c_6002,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(s(X1))))
| ~ 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_5454]) ).
tcf(c_6045,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),s(s(s(s(X1)))))
| r(s(s(X0)),s(s(s(s(X1)))))
| ( s(s(X0)) = s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_4752]) ).
tcf(c_6046,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_6045]) ).
tcf(c_6094,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_269]) ).
tcf(c_6095,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_6094]) ).
tcf(c_6134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X1))),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(X2))),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5113]) ).
tcf(c_6219,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(X2))),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5278]) ).
tcf(c_6331,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(X1))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(X1),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_3976]) ).
tcf(c_6332,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(X1)),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_3968]) ).
tcf(c_6345,plain,
( ~ b(s(s(s(z))),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(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_6332]) ).
tcf(c_6433,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),X2)
| ~ b(X2,s(s(s(X1))))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(z)),s(s(s(X1))))
| ~ b(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_5505]) ).
tcf(c_6565,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X0))),X3)
| ~ b(X3,s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3944]) ).
tcf(c_6569,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X2)),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_2571]) ).
tcf(c_6609,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_3470]) ).
tcf(c_6688,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X1)))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5455]) ).
tcf(c_6735,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5418]) ).
tcf(c_6760,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5532]) ).
tcf(c_6769,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5560]) ).
tcf(c_6787,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(X1)))
| ~ 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(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_5395]) ).
tcf(c_6797,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(X1)))
| ~ b(s(s(s(z))),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_5447]) ).
tcf(c_6805,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(X1)))
| ~ b(s(s(X3)),s(s(s(X2))))
| ~ b(s(s(X3)),s(s(s(X0))))
| ~ b(s(s(X1)),s(s(s(X2))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5448]) ).
tcf(c_6862,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X1)))
| ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(X0))),s(X3))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5506]) ).
tcf(c_6871,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(z)))
| ~ b(s(s(s(X1))),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5507]) ).
tcf(c_6876,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(s(s(s(X1))),X3)
| ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5507]) ).
tcf(c_6913,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(s(z))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_5533]) ).
tcf(c_6923,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(X3))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5541]) ).
tcf(c_6924,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(s(s(X0))),s(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_5541]) ).
tcf(c_6940,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(X1)))
| ~ b(z,s(s(s(X2))))
| ~ b(z,s(s(s(X0))))
| ~ b(s(s(X1)),s(s(s(X2))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5562]) ).
tcf(c_6960,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(s(X1))))
| ~ b(X3,s(s(s(s(X0)))))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5563]) ).
tcf(c_6988,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),s(s(s(X1))))
| ~ 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_5788]) ).
tcf(c_6989,plain,
( ~ r(s(s(s(s(z)))),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_6988]) ).
tcf(c_7004,plain,
! [X0: $i,X1: $i] :
( ~ 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_5800]) ).
tcf(c_7005,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_7004]) ).
tcf(c_7014,plain,
! [X0: $i,X1: $i] :
( ~ 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_5885]) ).
tcf(c_7015,plain,
( ~ 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_7014]) ).
tcf(c_7040,plain,
! [X0: $i] :
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6002]) ).
tcf(c_7043,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(s(X1))))
| ~ 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_6002]) ).
tcf(c_7062,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(s(X0))))),s(s(X1)))
| r(s(s(s(s(s(X0))))),s(s(X1)))
| ( s(s(s(s(s(X0))))) = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_5792]) ).
tcf(c_7063,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_7062]) ).
tcf(c_7277,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(s(X0)))) = s(s(X2)) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(s(s(X0)))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_1323]) ).
tcf(c_7280,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(X1) )
| ( s(s(s(s(X0)))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_7282,plain,
( ( s(s(s(z))) = s(z) )
| ( s(s(s(s(z)))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_7280]) ).
tcf(c_7344,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(s(X0))))),z)
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_4986]) ).
tcf(c_7345,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_7344]) ).
tcf(c_7409,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_1476,c_56]) ).
tcf(c_7531,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_5891]) ).
tcf(c_7532,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_7531]) ).
tcf(c_7645,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),s(X2))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(z)),s(s(s(X1))))
| ~ b(s(s(z)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_6433]) ).
tcf(c_7646,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(z)),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_7645]) ).
tcf(c_7734,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(z))),s(s(X2)))
| ~ b(s(s(s(X1))),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ 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_6735]) ).
tcf(c_7788,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(z))),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(s(z))),s(s(s(X0))))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6797]) ).
tcf(c_7848,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X2))),X3)
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(s(X1)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6134]) ).
tcf(c_7924,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6769]) ).
tcf(c_7933,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(s(z))))
| ~ b(X1,s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6787]) ).
tcf(c_7934,plain,
( ~ b(z,s(s(s(z))))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_7933]) ).
tcf(c_7982,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_2407]) ).
tcf(c_7988,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_6609]) ).
tcf(c_7989,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_7988]) ).
tcf(c_8036,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_6871]) ).
tcf(c_8054,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(X1)))
| ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6913]) ).
tcf(c_8055,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(z))))
| ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6913]) ).
tcf(c_8124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(s(s(X1)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(X2))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6219]) ).
tcf(c_8180,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(s(X2))))
| ~ b(s(s(X3)),s(s(s(X1))))
| ~ b(s(s(X3)),s(s(s(X0))))
| ~ b(s(s(s(X1))),s(s(s(X2))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_6805]) ).
tcf(c_8214,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(X3))
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6923]) ).
tcf(c_8237,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(X1)))
| ~ b(s(s(s(z))),X2)
| ~ b(s(s(s(s(X0)))),X2)
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_6876]) ).
tcf(c_8550,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ 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_5114]) ).
tcf(c_8551,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(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(s(z))))) ),
inference(instantiation,[status(thm)],[c_8550]) ).
tcf(c_8613,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ 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_5272]) ).
tcf(c_8627,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(s(s(s(s(X0)))),X3)
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5278]) ).
tcf(c_8632,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X0))),s(X3))
| ~ b(s(X3),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6565]) ).
tcf(c_8643,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(s(X0))),s(s(X2)))
| ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6569]) ).
tcf(c_8689,plain,
! [X0: $i] :
( ~ r(z,s(s(s(z))))
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4125]) ).
tcf(c_8699,plain,
( ~ r(z,s(s(s(z))))
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8689]) ).
tcf(c_8704,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X1)))),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_4558]) ).
tcf(c_8719,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(s(z))))
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3129]) ).
tcf(c_8720,plain,
( ~ r(z,s(s(s(z))))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8719]) ).
tcf(c_8732,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3559]) ).
tcf(c_8733,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_8732]) ).
tcf(c_8737,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(z))))
| ~ r(s(s(s(s(s(X0))))),s(X1))
| ~ r(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3559]) ).
tcf(c_8738,plain,
( ~ r(s(z),s(s(s(z))))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8737]) ).
tcf(c_8748,plain,
! [X0: $i] :
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3641]) ).
tcf(c_8749,plain,
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8748]) ).
tcf(c_8766,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3672]) ).
tcf(c_8767,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_8766]) ).
tcf(c_8779,plain,
! [X0: $i] :
( ( s(z) = s(s(s(X0))) )
| ( s(z) != s(z) )
| ( s(s(s(X0))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_448]) ).
tcf(c_8780,plain,
! [X0: $i] :
( ( s(s(X0)) = z )
| ( s(s(s(X0))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_8781,plain,
( ( s(s(z)) = z )
| ( s(s(s(z))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_8780]) ).
tcf(c_8802,plain,
! [X0: $i] :
( ( s(s(s(s(X0)))) = z )
| ( z != s(s(s(s(X0)))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_1558]) ).
tcf(c_8803,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_8802]) ).
tcf(c_8840,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(z) )
| ( s(z) != s(X1) )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_8841,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = X1 )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_8949,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(s(s(X1))) )
| ( s(X0) != s(s(s(s(X1)))) ) ),
inference(instantiation,[status(thm)],[c_254]) ).
tcf(c_8954,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = s(X1) )
| ( s(X1) != s(s(s(s(X0)))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_8955,plain,
( ( s(s(s(s(z)))) = s(z) )
| ( s(z) != s(s(s(s(z)))) )
| ( s(s(s(s(z)))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_8954]) ).
tcf(c_9016,plain,
! [X0: $i] :
( ( z = s(s(s(X0))) )
| ( s(z) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_242]) ).
tcf(c_9073,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X1))),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4124]) ).
tcf(c_9075,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(X2))
| ~ r(s(s(s(s(X0)))),s(X2))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_9076,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(s(X1))))
| ~ r(s(X2),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2501]) ).
tcf(c_9077,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X1))),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2555]) ).
tcf(c_9168,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(z),s(s(s(s(X1)))))
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3060]) ).
tcf(c_9169,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X0)))
| ~ r(z,s(s(s(s(X1)))))
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1412]) ).
tcf(c_9170,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X0)))
| ~ r(X2,s(s(s(s(X1)))))
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_9171,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(s(s(s(X1)))),s(z))
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1413]) ).
tcf(c_9172,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_9171]) ).
tcf(c_9174,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_9168]) ).
tcf(c_9240,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = s(s(X1)) )
| ( s(s(X1)) != s(s(s(s(X0)))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_7277]) ).
tcf(c_9241,plain,
( ( s(s(s(s(z)))) = s(s(z)) )
| ( s(s(z)) != s(s(s(s(z)))) )
| ( s(s(s(s(z)))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_9240]) ).
tcf(c_9329,plain,
! [X0: $i] :
( ~ r(z,s(s(s(z))))
| ~ r(s(s(s(s(s(X0))))),z)
| ~ r(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_8689]) ).
tcf(c_9330,plain,
( ~ r(z,s(s(s(z))))
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_9329]) ).
tcf(c_9341,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_1806]) ).
tcf(c_9342,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_9341]) ).
tcf(c_9360,plain,
! [X0: $i] :
( ( s(z) = s(s(s(s(X0)))) )
| ( s(z) != s(z) )
| ( s(s(s(s(X0)))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_8779]) ).
tcf(c_9461,plain,
! [X0: $i] :
( ( s(s(s(X0))) = z )
| ( s(s(s(s(X0)))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_8780]) ).
tcf(c_9462,plain,
( ( s(s(s(z))) = z )
| ( s(s(s(s(z)))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_9461]) ).
tcf(c_9475,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_1558]) ).
tcf(c_9476,plain,
( ( s(s(s(z))) = z )
| ( z != s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_9475]) ).
tcf(c_9486,plain,
! [X0: $i] :
( ( z = s(s(s(s(X0)))) )
| ( s(z) != s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_9016]) ).
tcf(c_9487,plain,
( ( z = s(s(s(s(z)))) )
| ( s(z) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_9486]) ).
tcf(c_9516,plain,
! [X0: $i] :
( ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_7043]) ).
tcf(c_9517,plain,
( ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(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(s(z))))) ),
inference(instantiation,[status(thm)],[c_9516]) ).
tcf(c_9833,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_7982]) ).
tcf(c_9834,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_9833]) ).
tcf(c_9881,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X0)))),s(s(s(z))))
| ~ r(s(s(s(s(s(X1))))),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_8704]) ).
tcf(c_9882,plain,
( ~ r(s(s(s(s(z)))),s(s(s(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_9881]) ).
tcf(c_9983,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(s(X1))))
| ~ r(s(s(s(s(X0)))),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_8766]) ).
tcf(c_10047,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(z) )
| ( s(z) != s(s(s(X0))) )
| ( s(s(s(X0))) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_8840]) ).
tcf(c_10048,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_10047]) ).
tcf(c_10209,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(s(s(s(X1)))) )
| ( s(X0) != s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_8949]) ).
tcf(c_10241,plain,
! [X0: $i] : s(s(s(X0))) != z,
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_10242,plain,
s(s(s(z))) != z,
inference(instantiation,[status(thm)],[c_10241]) ).
tcf(c_10406,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = X1 )
| ( s(s(s(s(X0)))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_8841]) ).
tcf(c_10506,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(s(X1))))),z)
| ~ r(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9073]) ).
tcf(c_10507,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_10506]) ).
tcf(c_10514,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(s(X1))))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9077]) ).
tcf(c_10515,plain,
( ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(s(z))))),s(z))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_10514]) ).
tcf(c_10527,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(z),s(s(s(s(s(X1))))))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9168]) ).
tcf(c_10528,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_10527]) ).
tcf(c_10535,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X0)))
| ~ r(z,s(s(s(s(s(X1))))))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10536,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_10535]) ).
tcf(c_10543,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),s(z))
| ~ r(s(s(s(s(s(X1))))),s(z))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9171]) ).
tcf(c_10544,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)))))) ),
inference(instantiation,[status(thm)],[c_10543]) ).
tcf(c_10747,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(s(s(X1))))
| ~ b(s(s(z)),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_8054]) ).
tcf(c_10748,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)))))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_10747]) ).
tcf(c_10922,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(X2)))
| ~ r(s(s(s(s(X0)))),s(s(X2)))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_9075]) ).
tcf(c_11596,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X2)),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_9076]) ).
tcf(c_11644,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X0)))
| ~ r(X2,s(s(s(s(s(X1))))))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_9170]) ).
tcf(c_11873,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,X2)
| ~ b(z,s(X0))
| ~ b(z,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1934]) ).
tcf(c_11878,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(s(X2))))
| ~ b(z,s(s(s(X1))))
| ~ b(z,s(s(s(s(X0)))))
| ~ b(s(s(s(X2))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_6940]) ).
tcf(c_11882,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),X2)
| ~ b(z,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_4106]) ).
tcf(c_11894,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),z)
| ~ b(z,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X1)))),z)
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1769]) ).
tcf(c_11952,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(X2))
| ~ b(X1,s(s(z)))
| ~ b(s(s(z)),s(X2))
| ~ b(X1,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1486]) ).
tcf(c_11953,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(s(s(z)),s(z))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_11952]) ).
tcf(c_11961,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(s(X0)))))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_4254]) ).
tcf(c_11963,plain,
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_11961]) ).
tcf(c_11970,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X0),X3)
| ~ b(s(X0),X2)
| ~ b(X3,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1931]) ).
tcf(c_12114,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X0)),z)
| ~ b(X1,s(s(X0)))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),X1)
| ~ b(s(s(s(s(z)))),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_1922]) ).
tcf(c_12117,plain,
( ~ b(z,s(s(z)))
| ~ 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_1765]) ).
tcf(c_12485,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),X1)
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5942]) ).
tcf(c_12487,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(s(s(z)))))
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5188]) ).
tcf(c_12488,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(s(s(z)))))
| ~ r(s(X1),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5185]) ).
tcf(c_12489,plain,
! [X0: $i] :
( ~ r(z,s(s(s(s(z)))))
| ~ r(z,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5189]) ).
tcf(c_12492,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),s(X1))
| ~ r(s(s(s(s(s(X0))))),s(X1))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5184]) ).
tcf(c_12493,plain,
! [X0: $i] :
( ~ r(s(s(s(s(z)))),z)
| ~ r(z,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5181]) ).
tcf(c_12494,plain,
! [X0: $i] :
( ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(z),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_5183]) ).
tcf(c_12495,plain,
( ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_12494]) ).
tcf(c_12496,plain,
( ~ r(s(s(s(s(z)))),z)
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_12493]) ).
tcf(c_12497,plain,
( ~ r(z,s(s(s(s(z)))))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_12489]) ).
tcf(c_12498,plain,
( ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_12488]) ).
tcf(c_12585,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X1,s(z))
| ~ b(X1,s(s(X2)))
| ~ b(s(z),s(s(X2)))
| ~ b(X1,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(z)) ),
inference(instantiation,[status(thm)],[c_2170]) ).
tcf(c_12588,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_12585]) ).
tcf(c_12600,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X0),s(z))
| ~ b(s(z),s(s(X2)))
| ~ b(s(X0),s(s(X2)))
| ~ b(s(s(s(X1))),s(z))
| ~ b(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1985]) ).
tcf(c_12637,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(z))
| ~ b(X2,s(X0))
| ~ b(X2,s(s(s(X1))))
| ~ b(s(s(s(X1))),s(z))
| ~ b(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1489]) ).
tcf(c_12642,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(z))))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_12637]) ).
tcf(c_12666,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(z))
| ~ b(s(X1),s(X2))
| ~ b(s(s(s(X0))),s(z))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2022]) ).
tcf(c_12703,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(z))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ 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_7734]) ).
tcf(c_12719,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(z))),s(s(X2)))
| ~ b(s(s(X2)),s(s(s(s(X0)))))
| ~ 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_7788]) ).
tcf(c_12831,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),s(s(X2)))
| ~ b(s(s(s(z))),s(X1))
| ~ b(s(s(s(z))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(X1))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_8237]) ).
tcf(c_12832,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(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_12831]) ).
tcf(c_12964,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_8613]) ).
tcf(c_12965,plain,
( ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(s(z)))),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_12964]) ).
tcf(c_13039,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X1)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5316]) ).
tcf(c_13049,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(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(s(X1))))) ),
inference(instantiation,[status(thm)],[c_5358]) ).
tcf(c_13551,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(z)))
| ~ b(s(X1),s(s(s(s(z)))))
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(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_7924]) ).
tcf(c_13552,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(z),s(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_13551]) ).
tcf(c_13645,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(z)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_5532]) ).
tcf(c_13647,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(s(X0)))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3953]) ).
tcf(c_13653,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_13647]) ).
tcf(c_13654,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(z)),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_13645]) ).
tcf(c_14406,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_8036]) ).
tcf(c_14407,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(z)))),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_14406]) ).
tcf(c_14424,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ 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_8055]) ).
tcf(c_14651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(s(X2))))
| ~ b(s(s(X3)),s(s(s(X1))))
| ~ b(s(s(X3)),s(s(s(s(X0)))))
| ~ b(s(s(s(X2))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_8180]) ).
tcf(c_14746,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ 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_8632]) ).
tcf(c_14755,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ 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_8643]) ).
tcf(c_14758,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(s(s(X1)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_8643]) ).
tcf(c_14896,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(s(X1)))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_4988]) ).
tcf(c_14897,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_14896]) ).
tcf(c_14915,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(z))))
| ~ r(s(s(X1)),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_4989]) ).
tcf(c_14916,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_14915]) ).
tcf(c_14920,plain,
! [X0: $i] :
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_4989]) ).
tcf(c_14925,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(X1)),s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_4991]) ).
tcf(c_14926,plain,
( ~ r(s(s(s(z))),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_14925]) ).
tcf(c_15342,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(s(X1)))
| ~ b(s(s(X2)),s(z))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6862]) ).
tcf(c_15343,plain,
( ~ b(s(z),s(s(z)))
| ~ 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_15342]) ).
tcf(c_15428,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(s(X0)))))
| ~ b(s(s(z)),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6760]) ).
tcf(c_15758,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X1)))
| ~ r(X2,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_812]) ).
tcf(c_15761,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(z,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_15762,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(z))
| ~ r(s(s(s(s(s(X0))))),s(z))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_15763,plain,
( ~ r(s(s(z)),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_15762]) ).
tcf(c_15764,plain,
( ~ r(z,s(s(z)))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_15761]) ).
tcf(c_15773,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(s(s(X0))))),s(s(X2)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1770]) ).
tcf(c_15774,plain,
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(s(s(s(z))))),s(s(z)))
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_15773]) ).
tcf(c_15778,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(X2))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3604]) ).
tcf(c_15782,plain,
( ~ r(s(z),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_15778]) ).
tcf(c_15837,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_7531]) ).
tcf(c_15838,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_15837]) ).
tcf(c_15986,plain,
! [X0: $i] : s(s(s(s(X0)))) != z,
inference(instantiation,[status(thm)],[c_10241]) ).
tcf(c_15987,plain,
s(s(s(s(z)))) != z,
inference(instantiation,[status(thm)],[c_15986]) ).
tcf(c_16029,plain,
! [X0: $i] :
( ( s(z) = s(s(s(s(s(X0))))) )
| ( s(z) != s(z) )
| ( s(s(s(s(s(X0))))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_9360]) ).
tcf(c_16030,plain,
( ( s(z) = s(s(s(s(s(z))))) )
| ( s(z) != s(z) )
| ( s(s(s(s(s(z))))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_16029]) ).
tcf(c_16081,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(s(s(s(X1)))) )
| ( s(s(X0)) != s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_10209]) ).
tcf(c_16082,plain,
( ( s(z) = s(s(s(s(z)))) )
| ( s(s(z)) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_16081]) ).
tcf(c_16148,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = X1 )
| ( s(s(s(s(s(X0))))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_10406]) ).
tcf(c_17527,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(s(s(X1)))))
| ~ r(s(s(s(s(X0)))),s(s(s(z))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_9983]) ).
tcf(c_18221,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),s(s(X1)))
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_12485]) ).
tcf(c_18222,plain,
( ~ r(s(s(s(s(z)))),s(s(z)))
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18221]) ).
tcf(c_18245,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(s(z)))))
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_12487]) ).
tcf(c_18246,plain,
( ~ r(s(s(z)),s(s(s(s(z)))))
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18245]) ).
tcf(c_18364,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),s(s(X1)))
| ~ 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_12492]) ).
tcf(c_18365,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_18364]) ).
tcf(c_18821,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),z)
| ~ b(X1,s(s(s(X0))))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),X1)
| ~ b(s(s(s(s(z)))),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_12114]) ).
tcf(c_18822,plain,
( ~ b(z,s(s(s(z))))
| ~ 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_18821]) ).
tcf(c_18840,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),s(s(X2)))
| ~ r(s(s(s(s(s(X0))))),s(s(X2)))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_10922]) ).
tcf(c_18841,plain,
( ~ r(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(z)))) ),
inference(instantiation,[status(thm)],[c_18840]) ).
tcf(c_18860,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(X0)))
| ~ r(s(z),s(s(s(s(s(X1))))))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_11644]) ).
tcf(c_18861,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18860]) ).
tcf(c_18874,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(X1)))
| ~ r(s(z),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_15758]) ).
tcf(c_18875,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_18874]) ).
tcf(c_19013,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X2)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_11596]) ).
tcf(c_19014,plain,
( ~ r(s(s(z)),s(s(s(z))))
| ~ r(s(s(z)),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_19013]) ).
tcf(c_19228,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(s(s(s(X1))))),s(X3))
| ~ b(s(s(X2)),s(s(s(s(s(X1))))))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_2919]) ).
tcf(c_19231,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X1))),X3)
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),X3)
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4114]) ).
tcf(c_19244,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ 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_2020]) ).
tcf(c_19245,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(X1))
| ~ b(X3,s(s(s(s(s(X0))))))
| ~ b(s(X2),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1489]) ).
tcf(c_19250,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(z)) ),
inference(instantiation,[status(thm)],[c_19245]) ).
tcf(c_19251,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(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_19244]) ).
tcf(c_19255,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),s(X3))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(X3),s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(s(X1))))),s(X2))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_2012]) ).
tcf(c_19259,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X0))),X3)
| ~ b(s(s(s(X0))),s(X2))
| ~ b(X3,s(s(s(s(s(X1))))))
| ~ 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_1904]) ).
tcf(c_19262,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(z),s(s(s(s(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_19255]) ).
tcf(c_19307,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X1)))
| ~ b(s(s(X2)),s(X3))
| ~ b(s(s(s(s(s(X0))))),s(X3))
| ~ b(s(s(s(s(s(X0))))),s(s(X2)))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6862]) ).
tcf(c_19308,plain,
( ~ b(s(z),s(s(z)))
| ~ 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_19307]) ).
tcf(c_19354,plain,
! [X0: $i] :
( ( s(s(s(s(s(X0))))) = z )
| ( z != s(s(s(s(s(X0))))) )
| ( s(s(s(s(s(X0))))) != s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_8802]) ).
tcf(c_19355,plain,
( ( s(s(s(s(s(z))))) = z )
| ( z != s(s(s(s(s(z))))) )
| ( s(s(s(s(s(z))))) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_19354]) ).
tcf(c_19396,plain,
! [X0: $i] :
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_7040]) ).
tcf(c_19397,plain,
( ~ b(s(s(z)),s(s(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_19396]) ).
tcf(c_19494,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_6332]) ).
tcf(c_19495,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(z)),s(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)))))) ),
inference(instantiation,[status(thm)],[c_19494]) ).
tcf(c_19621,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_760]) ).
tcf(c_19622,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_757]) ).
tcf(c_19623,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(z,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_19624,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_19625,plain,
( ~ r(s(s(z)),s(z))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_19624]) ).
tcf(c_19626,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_19623]) ).
tcf(c_19627,plain,
( ~ r(z,s(s(z)))
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_19622]) ).
tcf(c_19628,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_19621]) ).
tcf(c_19639,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(X2))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3604]) ).
tcf(c_19643,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(s(s(s(z)))),s(z))
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_19639]) ).
tcf(c_19735,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(s(s(X0))))))
| ~ b(s(s(z)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_15428]) ).
tcf(c_19736,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_19735]) ).
tcf(c_19809,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_713]) ).
tcf(c_19810,plain,
( ( s(s(s(s(z)))) = s(s(z)) )
| ( s(s(s(s(s(z))))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_19809]) ).
tcf(c_20053,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(z)),s(X2))
| ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5115]) ).
tcf(c_20054,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),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_20053]) ).
tcf(c_20089,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(X2))
| ~ b(z,s(X1))
| ~ b(z,s(s(s(s(X0)))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_11873]) ).
tcf(c_20090,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(s(z)))))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_20089]) ).
tcf(c_20263,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),X1)
| ~ b(s(s(s(s(s(X0))))),z)
| ~ 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_11882]) ).
tcf(c_20264,plain,
( ~ b(z,s(s(s(s(z)))))
| ~ 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_20263]) ).
tcf(c_20399,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(z),s(s(X2)))
| ~ b(s(s(s(X1))),s(z))
| ~ b(s(s(s(s(s(X0))))),s(z))
| ~ b(s(s(s(s(s(X0))))),s(s(X2)))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_12600]) ).
tcf(c_20400,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(s(z))))),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_20399]) ).
tcf(c_20468,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1)))
| ~ 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_12703]) ).
tcf(c_20469,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(s(z))))),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_20468]) ).
tcf(c_20483,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(X1)),s(s(s(s(s(X0))))))
| ~ 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_12719]) ).
tcf(c_20755,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14746]) ).
tcf(c_20756,plain,
( ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(z)))),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_20755]) ).
tcf(c_20930,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(X2))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(s(s(X0))))))
| ~ b(s(X2),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_13647]) ).
tcf(c_20986,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),s(z))
| ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(s(s(X1))))),s(z))
| ~ 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_12666]) ).
tcf(c_20987,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(z),s(s(s(s(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_20986]) ).
tcf(c_21058,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(X2)))
| ~ b(s(s(s(s(s(X1))))),s(s(z)))
| ~ b(s(s(X2)),s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_13039]) ).
tcf(c_21059,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(z)),s(s(s(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_21058]) ).
tcf(c_21065,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(X2),s(s(s(s(s(X1))))))
| ~ 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_13049]) ).
tcf(c_21066,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ 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_21065]) ).
tcf(c_21524,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(X1))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_6331]) ).
tcf(c_21525,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(z),s(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)))))) ),
inference(instantiation,[status(thm)],[c_21524]) ).
tcf(c_21532,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(s(z))))
| ~ b(s(X1),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_7933]) ).
tcf(c_21533,plain,
( ~ b(s(z),s(s(s(z))))
| ~ b(s(z),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_21532]) ).
tcf(c_21639,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),s(z))
| ~ r(s(z),s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_4987]) ).
tcf(c_21640,plain,
( ~ 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_21639]) ).
tcf(c_21646,plain,
! [X0: $i] :
( ~ r(s(z),s(s(s(z))))
| ~ r(s(z),s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_14920]) ).
tcf(c_21647,plain,
( ~ r(s(z),s(s(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_21646]) ).
tcf(c_21665,plain,
! [X0: $i,X1: $i] :
( ~ r(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(z)))) ),
inference(instantiation,[status(thm)],[c_3672]) ).
tcf(c_21666,plain,
( ~ r(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(z)))) ),
inference(instantiation,[status(thm)],[c_21665]) ).
tcf(c_21672,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(s(s(s(s(X0))))),s(X1))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_4988]) ).
tcf(c_21673,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_21672]) ).
tcf(c_21711,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(X1))
| ~ r(s(X1),s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_4991]) ).
tcf(c_22078,plain,
! [X0: $i] :
( ~ b(s(s(s(s(z)))),z)
| ~ b(z,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(z)))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_11894]) ).
tcf(c_22343,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X0),X3)
| ~ b(s(X0),X2)
| ~ b(X3,s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(s(X1))))),X2)
| ~ b(s(X0),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_11970]) ).
tcf(c_22392,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(z)))
| ~ r(s(X1),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_747]) ).
tcf(c_22393,plain,
( ~ r(s(z),s(s(z)))
| ~ r(s(z),s(s(s(s(z)))))
| ~ r(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_22392]) ).
tcf(c_22787,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(z)))),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(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_14424]) ).
tcf(c_22791,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_12703]) ).
tcf(c_22793,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(X1)))
| ~ b(s(s(s(s(z)))),X2)
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ 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_8627]) ).
tcf(c_22799,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(X2))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ 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_8214]) ).
tcf(c_22805,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(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_22799]) ).
tcf(c_22810,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(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_22793]) ).
tcf(c_22812,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))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_22791]) ).
tcf(c_22815,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(z)))),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(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_22787]) ).
tcf(c_22999,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(z)))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(X2),s(s(s(s(s(X1))))))
| ~ 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_6688]) ).
tcf(c_23000,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(z),s(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)))))) ),
inference(instantiation,[status(thm)],[c_22999]) ).
tcf(c_23705,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(z))
| ~ b(s(s(X0)),s(z))
| ~ b(s(z),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(X2)))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2169]) ).
tcf(c_23821,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X3),s(s(X2)))
| ~ b(s(s(s(X0))),s(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_6924]) ).
tcf(c_23822,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(z))),s(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_23821]) ).
tcf(c_23960,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(s(X1))))
| ~ b(X3,s(s(s(s(s(X0))))))
| ~ b(s(s(X2)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_6960]) ).
tcf(c_23961,plain,
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(z))))
| ~ b(z,s(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(z)))) ),
inference(instantiation,[status(thm)],[c_23960]) ).
tcf(c_23969,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),X2)
| ~ b(s(s(s(s(z)))),X2)
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_7848]) ).
tcf(c_23987,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),s(X2))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_14755]) ).
tcf(c_23988,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(z)))),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_23987]) ).
tcf(c_24100,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(z)))),X2)
| ~ b(X2,s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_8124]) ).
tcf(c_24434,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X3)),s(s(s(X2))))
| ~ b(s(s(X3)),s(s(s(X1))))
| ~ b(s(s(X3)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(X2))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_14651]) ).
tcf(c_24435,plain,
( ~ b(s(s(z)),s(s(s(z))))
| ~ b(s(s(z)),s(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(z)))) ),
inference(instantiation,[status(thm)],[c_24434]) ).
tcf(c_24524,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),s(X2))
| ~ b(s(s(s(s(z)))),s(X2))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_14758]) ).
tcf(c_24525,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ 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_24524]) ).
tcf(c_27457,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_7409,c_59]) ).
tcf(c_27467,plain,
! [X0: $i] : s(s(s(s(s(X0))))) != z,
inference(instantiation,[status(thm)],[c_15986]) ).
tcf(c_27468,plain,
s(s(s(s(s(z))))) != z,
inference(instantiation,[status(thm)],[c_27467]) ).
tcf(c_27591,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = s(X1) )
| ( s(s(s(s(s(X0))))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_16148]) ).
tcf(c_27592,plain,
( ( s(s(s(s(z)))) = s(z) )
| ( s(s(s(s(s(z))))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_27591]) ).
tcf(c_28121,plain,
! [X0: $i] :
( ~ b(s(s(s(s(z)))),z)
| ~ b(z,s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),z)
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_22078]) ).
tcf(c_28122,plain,
( ~ b(s(s(s(s(z)))),z)
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_28121]) ).
tcf(c_28270,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_16081]) ).
tcf(c_28271,plain,
( ( s(s(z)) = s(s(s(s(z)))) )
| ( s(s(s(z))) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_28270]) ).
tcf(c_28612,plain,
! [X0: $i] :
( b(s(z),s(s(X0)))
| r(s(z),s(s(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_27457,c_56,c_202,c_220,c_242,c_385]) ).
tcf(c_28614,plain,
( b(s(z),s(s(z)))
| r(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_28612]) ).
tcf(c_28626,plain,
! [X0: $i] :
( r(z,s(s(X0)))
| r(s(s(X0)),z)
| r(s(z),s(s(X0)))
| ~ b(s(z),z) ),
inference(resolution,[status(thm)],[c_28612,c_1918]) ).
tcf(c_28627,plain,
( r(z,s(s(z)))
| r(s(s(z)),z)
| r(s(z),s(s(z)))
| ~ b(s(z),z) ),
inference(instantiation,[status(thm)],[c_28626]) ).
tcf(c_28631,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(s(z),s(s(X1)))
| r(s(s(X1)),s(X2))
| ( s(X1) = X2 )
| ~ b(X0,s(z))
| ~ b(X0,s(X2))
| ~ b(X0,s(s(X1))) ),
inference(resolution,[status(thm)],[c_28612,c_1172]) ).
tcf(c_28632,plain,
( r(s(z),s(s(z)))
| r(s(s(z)),s(z))
| ( s(z) = z )
| ~ b(z,s(z))
| ~ b(z,s(s(z))) ),
inference(instantiation,[status(thm)],[c_28631]) ).
tcf(c_29061,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X0)))),s(s(s(z))))
| ~ r(s(s(s(z))),s(s(s(s(s(X1))))))
| ~ r(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_17527]) ).
tcf(c_29062,plain,
( ~ r(s(s(s(s(z)))),s(s(s(z))))
| ~ r(s(s(s(z))),s(s(s(s(s(z))))))
| ~ r(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_29061]) ).
tcf(c_29223,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_2779,c_56]) ).
tcf(c_29837,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(s(s(s(X0))))),s(s(X1)))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_21672]) ).
tcf(c_29838,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_29837]) ).
tcf(c_29923,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),s(s(X1)))
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_21711]) ).
tcf(c_29924,plain,
( ~ 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_29923]) ).
tcf(c_30251,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(s(s(X1)))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z))))
| ~ 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_20468]) ).
tcf(c_30252,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(s(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_30251]) ).
tcf(c_30255,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(s(s(z)))))
| ~ b(s(s(s(z))),s(s(s(s(X0)))))
| ~ b(s(s(s(z))),s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(s(X1))))),s(s(s(s(z)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_20483]) ).
tcf(c_30256,plain,
( ~ 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))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_30255]) ).
tcf(c_30681,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_29223,c_59]) ).
tcf(c_31101,plain,
! [X0: $i] :
( b(s(s(X0)),s(z))
| r(s(s(X0)),s(z)) ),
inference(global_subsumption_just,[status(thm)],[c_30681,c_56,c_190,c_196]) ).
tcf(c_31103,plain,
( b(s(s(z)),s(z))
| r(s(s(z)),s(z)) ),
inference(instantiation,[status(thm)],[c_31101]) ).
tcf(c_31116,plain,
! [X0: $i] :
( r(z,s(z))
| r(s(z),z)
| r(s(s(X0)),s(z))
| ~ b(s(s(X0)),z) ),
inference(resolution,[status(thm)],[c_31101,c_1918]) ).
tcf(c_31117,plain,
( r(z,s(z))
| r(s(z),z)
| r(s(s(z)),s(z))
| ~ b(s(s(z)),z) ),
inference(instantiation,[status(thm)],[c_31116]) ).
tcf(c_31126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(s(X0))),s(X3))
| ~ b(s(s(s(X0))),s(s(X2)))
| ~ b(s(s(s(s(s(X1))))),s(X3))
| ~ 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_19259]) ).
tcf(c_31127,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),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_31126]) ).
tcf(c_31251,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(z)))),s(X2))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ 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_19228]) ).
tcf(c_31258,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(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_31251]) ).
tcf(c_31753,plain,
! [X0: $i] : s(s(s(s(s(X0))))) = s(s(s(s(s(X0))))),
inference(instantiation,[status(thm)],[c_3414]) ).
tcf(c_31754,plain,
s(s(s(s(s(z))))) = s(s(s(s(s(z))))),
inference(instantiation,[status(thm)],[c_31753]) ).
tcf(c_32345,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X1))),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_23969]) ).
tcf(c_32346,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32345]) ).
tcf(c_32364,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(X3,s(s(X2)))
| ~ b(X3,s(s(X1)))
| ~ b(X3,s(s(s(s(s(X0))))))
| ~ b(s(s(X2)),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_20930]) ).
tcf(c_32365,plain,
( ~ b(z,s(s(z)))
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(s(z)),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_32364]) ).
tcf(c_32367,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(z),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(X1))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_24100]) ).
tcf(c_32368,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(z)))),s(s(s(z))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32367]) ).
tcf(c_32397,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(s(X0)),X3)
| ~ b(s(s(X0)),X2)
| ~ b(X3,s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(s(X1))))),X2)
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_22343]) ).
tcf(c_32398,plain,
( ~ b(s(s(z)),z)
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32397]) ).
tcf(c_32449,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X1))
| ~ r(X2,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2517]) ).
tcf(c_32454,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(s(s(z))))),s(z)) ),
inference(instantiation,[status(thm)],[c_32449]) ).
tcf(c_32773,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),s(X1))
| ~ b(s(s(s(s(z)))),X2)
| ~ b(s(s(s(s(z)))),s(X1))
| ~ b(s(s(s(s(z)))),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_1904]) ).
tcf(c_32775,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(z)),s(z))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_32773]) ).
tcf(c_32793,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X1)),s(z))
| ~ b(s(z),s(s(s(X0))))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(X1)))
| ~ b(s(s(s(s(z)))),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_23705]) ).
tcf(c_32801,plain,
( ~ b(s(s(z)),s(z))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(s(z)))),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_32793]) ).
tcf(c_32941,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(z)))
| ~ b(s(s(s(s(z)))),s(X1))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_19244]) ).
tcf(c_32942,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32941]) ).
tcf(c_32960,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(s(z)))),s(X2))
| ~ b(s(s(s(s(z)))),s(X1))
| ~ b(s(X2),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(X1))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_19255]) ).
tcf(c_32961,plain,
( ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_32960]) ).
tcf(c_33220,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(X0))))
| ~ b(s(s(s(s(z)))),X2)
| ~ b(s(s(s(X0))),s(X1))
| ~ b(s(s(s(s(z)))),s(X1))
| ~ b(s(s(s(s(z)))),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_2625]) ).
tcf(c_33221,plain,
( ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_33220]) ).
tcf(c_33673,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(z))))
| ~ b(s(s(s(z))),X1)
| ~ b(s(s(s(s(s(X0))))),X2)
| ~ b(s(s(s(s(s(X0))))),X1)
| ~ b(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_2975]) ).
tcf(c_33681,plain,
( ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_33673]) ).
tcf(c_33855,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(s(s(z))))
| ~ b(X2,s(s(s(s(s(X0))))))
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_20930]) ).
tcf(c_33856,plain,
! [X0: $i] :
( ~ b(s(s(s(s(z)))),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(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_22787]) ).
tcf(c_33858,plain,
( ~ 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(s(z))))),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_33856]) ).
tcf(c_33859,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(z))))
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_33855]) ).
tcf(c_33897,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(z,s(s(s(X2))))
| ~ b(z,s(s(s(X1))))
| ~ b(z,s(s(s(s(s(X0))))))
| ~ b(s(s(s(X2))),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_11878]) ).
tcf(c_33898,plain,
( ~ b(z,s(s(s(z))))
| ~ b(z,s(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(z)))) ),
inference(instantiation,[status(thm)],[c_33897]) ).
tcf(c_34188,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(X0))
| ~ r(X2,s(s(s(s(s(X1))))))
| ~ r(s(X0),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_2070]) ).
tcf(c_34191,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(z),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_34188]) ).
tcf(c_34259,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X1)),s(s(s(z))))
| ~ r(s(s(X1)),s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_14915]) ).
tcf(c_34260,plain,
( ~ r(s(s(z)),s(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_34259]) ).
tcf(c_34651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(X1))),s(X3))
| ~ b(s(s(s(s(s(X0))))),s(X3))
| ~ b(s(s(s(s(s(X0))))),s(X2))
| ~ b(s(s(s(s(s(X0))))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_19231]) ).
tcf(c_34652,plain,
( ~ b(s(z),s(s(s(z))))
| ~ b(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(z)))) ),
inference(instantiation,[status(thm)],[c_34651]) ).
tcf(c_34690,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_34652,c_34260,c_34191,c_33898,c_33859,c_33858,c_33681,c_33221,c_32961,c_32942,c_32801,c_32775,c_32454,c_32398,c_32368,c_32365,c_32346,c_31754,c_31258,c_31127,c_31117,c_31103,c_30256,c_30252,c_29924,c_29838,c_29062,c_28632,c_28627,c_28614,c_28271,c_28122,c_27592,c_27468,c_24525,c_24435,c_23988,c_23961,c_23822,c_23000,c_22815,c_22812,c_22810,c_22805,c_22393,c_21673,c_21666,c_21647,c_21640,c_21533,c_21525,c_21066,c_21059,c_20987,c_20756,c_20469,c_20400,c_20264,c_20090,c_20054,c_19810,c_19736,c_19643,c_19628,c_19627,c_19626,c_19625,c_19495,c_19397,c_19355,c_19308,c_19262,c_19251,c_19250,c_19014,c_18875,c_18861,c_18841,c_18822,c_18365,c_18246,c_18222,c_16082,c_16030,c_15987,c_15838,c_15782,c_15774,c_15764,c_15763,c_15343,c_14926,c_14916,c_14897,c_14407,c_13654,c_13653,c_13552,c_12965,c_12832,c_12642,c_12588,c_12498,c_12497,c_12496,c_12495,c_12117,c_11963,c_11953,c_10748,c_10544,c_10536,c_10528,c_10515,c_10507,c_10242,c_10048,c_9882,c_9834,c_9517,c_9487,c_9476,c_9462,c_9342,c_9330,c_9241,c_9174,c_9172,c_8955,c_8803,c_8781,c_8767,c_8749,c_8738,c_8733,c_8720,c_8699,c_8551,c_7989,c_7934,c_7646,c_7532,c_7345,c_7282,c_7063,c_7015,c_7005,c_6989,c_6345,c_6095,c_6046,c_5892,c_5818,c_5793,c_5789,c_5760,c_5758,c_5359,c_5317,c_5237,c_5232,c_5120,c_5118,c_5117,c_4998,c_4996,c_4995,c_4994,c_4857,c_4856,c_4855,c_4365,c_4358,c_3635,c_3597,c_3567,c_3560,c_3415,c_3407,c_3368,c_3342,c_3131,c_3061,c_2797,c_2632,c_2520,c_2519,c_2417,c_2406,c_2258,c_2066,c_2062,c_1983,c_1869,c_1835,c_1807,c_1766,c_1521,c_1365,c_1224,c_1212,c_1211,c_1210,c_1209,c_826,c_748,c_735,c_720,c_714,c_649,c_605,c_566,c_540,c_490,c_486,c_457,c_377,c_365,c_354,c_320,c_270,c_245,c_244,c_240,c_238,c_228,c_221,c_203,c_198,c_197,c_193,c_65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA164-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n004.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 13:06:23 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 14.13/2.70 % SZS status Started for theBenchmark.p
% 14.13/2.70 % SZS status Unsatisfiable for theBenchmark.p
% 14.13/2.70
% 14.13/2.70 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.13/2.70
% 14.13/2.70 % ------ iProver source info
% 14.13/2.70
% 14.13/2.70 % git: date: 2026-07-19 20:42:38 +0200
% 14.13/2.70 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.13/2.70 % git: non_committed_changes: false
% 14.13/2.70
% 14.13/2.70 % ------ Parsing...% successful
% 14.13/2.70
% 14.13/2.70
% 14.13/2.70 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.13/2.70
% 14.13/2.70 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 14.13/2.70
% 14.13/2.70 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 14.13/2.70
% 14.13/2.70 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 14.13/2.70 % ------ Proving...
% 14.13/2.70 % ------ Problem Properties
% 14.13/2.70
% 14.13/2.70 %
% 14.13/2.70 % clauses 7
% 14.13/2.70 % conjectures 0
% 14.13/2.70 % EPR 5
% 14.13/2.70 % Horn 6
% 14.13/2.70 % unary 3
% 14.13/2.70 % binary 1
% 14.13/2.70 % lits 16
% 14.13/2.70 % lits eq 4
% 14.13/2.70 % fd_pure 0
% 14.13/2.70 % fd_pseudo 0
% 14.13/2.70 % fd_cond 0
% 14.13/2.70 % fd_pseudo_cond 2
% 14.13/2.70 % AC symbols 0
% 14.13/2.70
% 14.13/2.70 % ------ Input Options Time Limit: Unbounded
% 14.13/2.70
% 14.13/2.70
% 14.13/2.70 % ------
% 14.13/2.70 % Current options:
% 14.13/2.70 % ------
% 14.13/2.70
% 14.13/2.70
% 14.13/2.70 %
% 14.13/2.70
% 14.13/2.70 % ------ Proving...
% 14.13/2.70 %
% 14.13/2.70
% 14.13/2.70 % SZS status Unsatisfiable for theBenchmark.p
% 14.13/2.70
% 14.13/2.70 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.13/2.72
% 14.13/2.72
%------------------------------------------------------------------------------