%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRA172-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:24:29 PM UTC 2026
% Result : Unsatisfiable 6.63s 13.00s
% Output : CNFRefutation 6.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 521 ( 21 unt; 0 def)
% Number of atoms : 1482 ( 315 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 2085 (1124 ~; 961 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 767 ( 0 sgn 767 !; 0 ?; 756 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : s(X0) != z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',snz) ).
fof(f2,axiom,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sinj) ).
fof(f5,axiom,
! [X0,X1] :
( b(X0,X1)
| r(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rb) ).
fof(f6,axiom,
! [X2,X0,X1] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axr) ).
fof(f7,axiom,
! [X2,X0,X1] :
( ~ b(X1,X2)
| ~ b(X0,X2)
| ~ b(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axb) ).
tcf(c_56,plain,
! [X0: $i] : s(X0) != z,
inference(cnf_transformation,[],[f1]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0) != s(X1) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_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] :
( ~ b(X1,X2)
| ~ b(X0,X2)
| ~ b(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_65,plain,
s(z) != z,
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_99,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_178,plain,
! [X0: $i] :
( ( s(X0) = z )
| ( s(s(X0)) != s(z) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_179,plain,
! [X0: $i] :
( b(s(X0),z)
| r(s(X0),z)
| ( s(X0) = z ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_180,plain,
( b(s(z),z)
| r(s(z),z)
| ( s(z) = z ) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_181,plain,
( ( s(z) = z )
| ( s(s(z)) != s(z) ) ),
inference(instantiation,[status(thm)],[c_178]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = z )
| ( z != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_183,plain,
! [X0: $i] :
( ( s(s(X0)) = s(z) )
| ( s(s(s(X0))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_184,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_186,plain,
( ( s(s(z)) = s(z) )
| ( s(s(s(z))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = X1 )
| ( s(s(X0)) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i] :
( b(s(X0),X1)
| r(s(X0),X1)
| ( s(X0) = X1 ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_190,plain,
! [X0: $i] :
( ( s(X0) = z )
| ( z != s(X0) )
| ( s(X0) != s(X0) ) ),
inference(instantiation,[status(thm)],[c_182]) ).
tcf(c_191,plain,
( ( s(z) = z )
| ( z != s(z) )
| ( s(z) != s(z) ) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_192,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X0) = X2 )
| ( X2 != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i] :
( ~ r(X0,z)
| ~ r(s(X1),z)
| ~ r(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_208,plain,
! [X0: $i] : s(X0) = s(X0),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_209,plain,
s(z) = s(z),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = X1 )
| ( X1 != s(X0) )
| ( s(X0) != s(X0) ) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_215,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_218,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_219,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),z)
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_225,plain,
! [X0: $i] : s(s(X0)) = s(s(X0)),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_226,plain,
s(s(z)) = s(s(z)),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_227,plain,
! [X0: $i] :
( ( z = s(X0) )
| ( s(z) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_228,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0))
| ( z = s(X0) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_229,plain,
( b(z,s(z))
| r(z,s(z))
| ( z = s(z) ) ),
inference(instantiation,[status(thm)],[c_228]) ).
tcf(c_230,plain,
( ( z = s(z) )
| ( s(z) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_237,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_215]) ).
tcf(c_243,plain,
! [X0: $i,X1: $i] :
( b(s(X0),s(X1))
| r(s(X0),s(X1))
| ( s(X0) = s(X1) ) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(X1) )
| ( s(X0) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_246,plain,
! [X0: $i,X1: $i] :
( b(X0,s(X1))
| r(X0,s(X1))
| ( X0 = s(X1) ) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(X0) )
| ( X2 != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_252,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_218]) ).
tcf(c_280,plain,
! [X0: $i] :
( b(s(s(X0)),z)
| r(s(s(X0)),z)
| ( s(s(X0)) = z ) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_281,plain,
( b(s(s(z)),z)
| r(s(s(z)),z)
| ( s(s(z)) = z ) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_301,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),X1)
| ~ r(s(s(X0)),X1)
| ~ r(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_304,plain,
! [X0: $i,X1: $i] :
( ~ r(X0,z)
| ~ r(z,s(X1))
| ~ r(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(z,s(X0))
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_311,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(X0) )
| ( X2 != s(X1) )
| ( s(X0) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_315,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_243]) ).
tcf(c_316,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_315]) ).
tcf(c_318,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_243]) ).
tcf(c_321,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_243]) ).
tcf(c_322,plain,
( b(s(z),s(s(z)))
| r(s(z),s(s(z)))
| ( s(z) = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_340,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_341,plain,
! [X0: $i,X1: $i] :
( b(X0,s(s(X1)))
| r(X0,s(s(X1)))
| ( X0 = s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_246]) ).
tcf(c_342,plain,
( b(z,s(s(z)))
| r(z,s(s(z)))
| ( z = s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_343,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_218]) ).
tcf(c_349,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(X0) )
| ( s(X2) != s(X1) )
| ( s(X0) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_373,plain,
! [X0: $i,X1: $i] :
( b(s(s(X0)),X1)
| r(s(s(X0)),X1)
| ( s(s(X0)) = X1 ) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_374,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(X1))
| ~ r(s(s(X0)),s(z))
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_301]) ).
tcf(c_378,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(s(X0),z)
| ~ r(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_304]) ).
tcf(c_413,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_340]) ).
tcf(c_433,plain,
! [X0: $i] : s(s(X0)) != z,
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_434,plain,
s(s(z)) != z,
inference(instantiation,[status(thm)],[c_433]) ).
tcf(c_450,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_343]) ).
tcf(c_452,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),X1)
| ~ r(s(s(s(X0))),X1)
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_453,plain,
! [X0: $i] :
( ~ r(s(s(z)),z)
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_454,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_469,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(z))
| ~ b(X1,s(s(X0)))
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_489,plain,
! [X0: $i] :
( b(s(X0),z)
| r(s(X0),z) ),
inference(resolution,[status(thm)],[c_60,c_56]) ).
tcf(c_490,plain,
( b(s(z),z)
| r(s(z),z) ),
inference(instantiation,[status(thm)],[c_489]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_500,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_343]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(X1)),X2)
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_503,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X0),z)
| ~ r(s(s(X1)),z)
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_504,plain,
( ~ r(s(z),z)
| ~ r(s(s(z)),z)
| ~ r(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_506,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_321]) ).
tcf(c_525,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_349]) ).
tcf(c_579,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_341]) ).
tcf(c_580,plain,
( b(z,s(s(s(z))))
| r(z,s(s(s(z))))
| ( z = s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_579]) ).
tcf(c_618,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_341]) ).
tcf(c_619,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_450]) ).
tcf(c_620,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_619]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),s(s(X1)))
| ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_644,plain,
! [X0: $i,X1: $i] :
( r(s(X1),z)
| ~ b(X0,z)
| ~ b(X0,s(X1)) ),
inference(resolution,[status(thm)],[c_62,c_489]) ).
tcf(c_646,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(X2,s(s(X1)))
| ~ r(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_413]) ).
tcf(c_647,plain,
( ~ r(s(z),z)
| ~ r(z,s(s(z)))
| ~ r(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_646]) ).
tcf(c_651,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_500]) ).
tcf(c_659,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(X2),s(s(X0)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_668,plain,
! [X0: $i,X1: $i,X2: $i] :
( b(X2,X1)
| r(X2,X1)
| ( X2 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_101,c_60]) ).
tcf(c_669,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_101,c_99]) ).
tcf(c_670,plain,
! [X0: $i,X1: $i] :
( ~ b(X0,z)
| ~ b(s(X1),z)
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_673,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_503]) ).
tcf(c_674,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_378]) ).
tcf(c_681,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_280]) ).
tcf(c_682,plain,
( b(s(s(s(z))),z)
| r(s(s(s(z))),z)
| ( s(s(s(z))) = z ) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_697,plain,
! [X0: $i,X1: $i] :
( ~ b(X0,z)
| ~ b(z,s(X1))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,X1)
| ~ b(X2,s(X0))
| ~ b(s(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_718,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X0,X2)
| ~ b(X2,s(X1))
| ~ b(X0,s(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_734,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X1)),X2)
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(X0))),X1)
| r(s(s(s(X0))),X1)
| ( s(s(s(X0))) = X1 ) ),
inference(instantiation,[status(thm)],[c_373]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(X1) )
| ( s(s(X0)) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_188]) ).
tcf(c_749,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_506]) ).
tcf(c_750,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_749]) ).
tcf(c_776,plain,
! [X0: $i,X1: $i] :
( b(X1,X0)
| r(X1,X0)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_669,c_60]) ).
tcf(c_839,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_525]) ).
tcf(c_852,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(s(z)) )
| ( s(s(s(s(X0)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_853,plain,
( ( s(s(s(z))) = s(s(z)) )
| ( s(s(s(s(z)))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_852]) ).
tcf(c_855,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(X1) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_858,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = s(s(X1)) )
| ( s(s(X0)) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_859,plain,
( ( s(z) = s(s(z)) )
| ( s(s(z)) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_858]) ).
tcf(c_872,plain,
! [X0: $i] :
( b(z,s(X0))
| r(z,s(X0)) ),
inference(resolution,[status(thm)],[c_776,c_56]) ).
tcf(c_873,plain,
( b(z,s(z))
| r(z,s(z)) ),
inference(instantiation,[status(thm)],[c_872]) ).
tcf(c_906,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),z)
| ~ b(s(X0),z)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_670]) ).
tcf(c_907,plain,
( ~ b(s(z),z)
| ~ b(s(z),s(z)) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_912,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_674]) ).
tcf(c_914,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(s(X0),z)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_921,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(X2,s(s(X1)))
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_646]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X1),X2)
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(z,s(X0))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_960,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(X0))
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_980,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_618]) ).
tcf(c_981,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_980]) ).
tcf(c_995,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(s(X0),X2)
| ~ b(s(X0),s(X1)) ),
inference(instantiation,[status(thm)],[c_718]) ).
tcf(c_1004,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X0)),X2)
| ~ r(s(s(s(X1))),X2)
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_1005,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_1004]) ).
tcf(c_1036,plain,
! [X0: $i] :
( b(s(s(s(X0))),s(z))
| r(s(s(s(X0))),s(z))
| ( s(s(s(X0))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_184]) ).
tcf(c_1037,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_1036]) ).
tcf(c_1045,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_506]) ).
tcf(c_1046,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_1045]) ).
tcf(c_1090,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_839]) ).
tcf(c_1154,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_506]) ).
tcf(c_1166,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_1169,plain,
! [X0: $i] :
( ~ b(s(s(z)),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_1170,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1169]) ).
tcf(c_1176,plain,
! [X0: $i] :
( ~ b(z,s(s(z)))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_1177,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1176]) ).
tcf(c_1178,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(s(s(X0)),z)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_1192,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_318]) ).
tcf(c_1213,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(X1)))
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(s(X1))),X2)
| ~ r(s(s(s(X0))),X2)
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_1234,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(X1)))
| ~ r(s(s(X0)),s(s(X2)))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_921]) ).
tcf(c_1238,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_921]) ).
tcf(c_1239,plain,
( ~ r(z,s(s(z)))
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1238]) ).
tcf(c_1251,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_668,c_60]) ).
tcf(c_1259,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(X1)))
| ~ r(s(s(X0)),s(z))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_374]) ).
tcf(c_1314,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(z)))
| ~ b(X1,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_960]) ).
tcf(c_1318,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(z)))
| ~ b(s(s(s(X0))),X1)
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_995]) ).
tcf(c_1320,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(s(s(X0)),X2)
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_995]) ).
tcf(c_1351,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_659]) ).
tcf(c_1357,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_1351]) ).
tcf(c_1362,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_632]) ).
tcf(c_1385,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(s(X0)),s(X2))
| ~ r(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_1388,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_305]) ).
tcf(c_1389,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),X2)
| ~ r(s(s(X0)),X2)
| ~ r(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_1390,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_219]) ).
tcf(c_1402,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X0)),s(X2))
| ~ r(s(s(s(X1))),s(X2))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_1439,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X1)),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_955]) ).
tcf(c_1533,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_1090]) ).
tcf(c_1537,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X2)) = s(s(s(X0))) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_1090]) ).
tcf(c_1563,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_1251,c_57]) ).
tcf(c_1614,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(X1)))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1259]) ).
tcf(c_1615,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_1614]) ).
tcf(c_1622,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X1))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1318]) ).
tcf(c_1626,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X2)),s(s(s(X0))))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1213]) ).
tcf(c_1633,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_1402]) ).
tcf(c_1636,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_1238]) ).
tcf(c_1643,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_1388]) ).
tcf(c_1644,plain,
( ~ r(z,s(z))
| ~ r(z,s(s(s(z))))
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_1643]) ).
tcf(c_1646,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_1390]) ).
tcf(c_1647,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_1646]) ).
tcf(c_1650,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X0)),s(s(X2)))
| ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1234]) ).
tcf(c_1654,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X0)),s(X2))
| ~ r(s(X2),s(s(s(X1))))
| ~ r(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1385]) ).
tcf(c_1779,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(s(X1)))
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_912]) ).
tcf(c_1796,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(s(X0))))
| ~ r(s(s(s(X0))),s(z)) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_1798,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_378]) ).
tcf(c_1799,plain,
( ~ r(s(z),z)
| ~ r(z,s(s(s(z))))
| ~ r(s(z),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1798]) ).
tcf(c_1804,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_503]) ).
tcf(c_1805,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(z))),z)
| ~ r(s(z),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1804]) ).
tcf(c_1818,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_502]) ).
tcf(c_1822,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(X2,s(s(s(X1))))
| ~ r(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_646]) ).
tcf(c_1844,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_659]) ).
tcf(c_1845,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_651]) ).
tcf(c_1846,plain,
! [X0: $i] :
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_673]) ).
tcf(c_1848,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_237]) ).
tcf(c_1849,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_1848]) ).
tcf(c_1851,plain,
( ~ r(s(s(s(z))),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1846]) ).
tcf(c_1863,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),X1)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_1876,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_659]) ).
tcf(c_1887,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_1154]) ).
tcf(c_1920,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_1389]) ).
tcf(c_1937,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X1)),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1439]) ).
tcf(c_1939,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_1439]) ).
tcf(c_1965,plain,
! [X0: $i] :
( ( s(s(X0)) = z )
| ( z != s(s(X0)) )
| ( s(s(X0)) != s(s(X0)) ) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_1966,plain,
( ( s(s(z)) = z )
| ( z != s(s(z)) )
| ( s(s(z)) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_1965]) ).
tcf(c_2012,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),X1)
| ~ r(s(s(s(X0))),X1)
| ~ r(s(s(s(X0))),s(z)) ),
inference(instantiation,[status(thm)],[c_301]) ).
tcf(c_2019,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),X1)
| ~ b(s(s(X0)),X1)
| ~ b(s(s(X0)),s(z)) ),
inference(instantiation,[status(thm)],[c_955]) ).
tcf(c_2045,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_674]) ).
tcf(c_2052,plain,
! [X0: $i] :
( ~ b(z,s(z))
| ~ b(z,s(s(X0)))
| ~ b(s(z),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_958]) ).
tcf(c_2053,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(z,s(s(X0)))
| ~ b(s(z),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_2054,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(s(s(X0)),z)
| ~ b(s(z),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_2056,plain,
( ~ b(s(z),z)
| ~ b(z,s(s(z)))
| ~ b(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2053]) ).
tcf(c_2057,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(z)))
| ~ b(s(z),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2052]) ).
tcf(c_2060,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(X1))
| ~ b(s(z),s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_492]) ).
tcf(c_2130,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(z,s(s(X1)))
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_2131,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(s(s(X1)),z)
| ~ b(s(X0),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_906]) ).
tcf(c_2134,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(X1))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_492]) ).
tcf(c_2135,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(s(X0)),s(X2))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1320]) ).
tcf(c_2226,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = X1 )
| ( X1 != s(s(s(X0))) )
| ( s(s(s(X0))) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_2227,plain,
( ( s(s(s(z))) = z )
| ( z != s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_2226]) ).
tcf(c_2248,plain,
! [X0: $i] : s(s(s(X0))) != z,
inference(instantiation,[status(thm)],[c_433]) ).
tcf(c_2249,plain,
s(s(s(z))) != z,
inference(instantiation,[status(thm)],[c_2248]) ).
tcf(c_2278,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(s(s(X0))) )
| ( X2 != X1 )
| ( s(s(s(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_2280,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = X2 )
| ( X2 != X1 )
| ( s(s(s(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_2410,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = s(X1) )
| ( s(X1) != s(s(s(X0))) )
| ( s(s(s(X0))) != s(s(s(X0))) ) ),
inference(instantiation,[status(thm)],[c_2226]) ).
tcf(c_2411,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_2410]) ).
tcf(c_2462,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_1036]) ).
tcf(c_2463,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_2462]) ).
tcf(c_2520,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = X2 )
| ( X2 != s(X1) )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_2280]) ).
tcf(c_2585,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_1614]) ).
tcf(c_2677,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_1863]) ).
tcf(c_2691,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(s(z))))
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_1636]) ).
tcf(c_2692,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_2691]) ).
tcf(c_2700,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_980]) ).
tcf(c_2701,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_2700]) ).
tcf(c_2703,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_1844]) ).
tcf(c_2727,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(X1))
| ~ r(s(s(s(X0))),s(z))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2012]) ).
tcf(c_2742,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_1654]) ).
tcf(c_2755,plain,
! [X0: $i] :
( ~ b(z,s(z))
| ~ b(z,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(z)) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_2756,plain,
( ~ b(z,s(z))
| ~ b(z,s(s(s(z))))
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_2755]) ).
tcf(c_2758,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X0)),z)
| ~ b(z,s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1320]) ).
tcf(c_2771,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_492]) ).
tcf(c_2793,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(z)))
| ~ b(s(X1),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_1314]) ).
tcf(c_2794,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(z))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2793]) ).
tcf(c_2805,plain,
! [X0: $i] :
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(X0))),s(z))
| ~ b(s(s(s(X0))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2019]) ).
tcf(c_2881,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2060]) ).
tcf(c_2897,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(z,s(s(s(X1))))
| ~ b(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2130]) ).
tcf(c_2919,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(X0))),s(s(X2)))
| ~ r(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1650]) ).
tcf(c_2929,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_1876]) ).
tcf(c_2963,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = s(s(X1)) )
| ( s(s(s(X0))) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_855]) ).
tcf(c_2971,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_1887]) ).
tcf(c_2972,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_2971]) ).
tcf(c_3011,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),s(X2))
| ~ r(s(s(s(X0))),s(X2))
| ~ r(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1920]) ).
tcf(c_3037,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_1939]) ).
tcf(c_3070,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(z),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_2054]) ).
tcf(c_3072,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(z)) ),
inference(instantiation,[status(thm)],[c_1166]) ).
tcf(c_3073,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_3072]) ).
tcf(c_3074,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(z))),z)
| ~ b(s(z),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3070]) ).
tcf(c_3079,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(s(s(s(X1))),z)
| ~ b(s(X0),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2131]) ).
tcf(c_3080,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X1))),z)
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1937]) ).
tcf(c_3108,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X1))),X2)
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_1439]) ).
tcf(c_3145,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(X1)))
| ~ b(s(X2),s(s(X0)))
| ~ b(s(s(X0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2134]) ).
tcf(c_3154,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X0)),s(X2))
| ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2135]) ).
tcf(c_3422,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_2963]) ).
tcf(c_3423,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_3422]) ).
tcf(c_3424,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_2963]) ).
tcf(c_3428,plain,
! [X0: $i] :
( ( s(s(z)) = s(s(s(X0))) )
| ( s(s(s(z))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_2963]) ).
tcf(c_3429,plain,
( ( s(s(z)) = s(s(s(z))) )
| ( s(s(s(z))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_3428]) ).
tcf(c_3475,plain,
! [X0: $i] : s(s(s(s(X0)))) = s(s(s(s(X0)))),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_3476,plain,
s(s(s(s(z)))) = s(s(s(s(z)))),
inference(instantiation,[status(thm)],[c_3475]) ).
tcf(c_3585,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_2677]) ).
tcf(c_3586,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_3585]) ).
tcf(c_3637,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = s(X2) )
| ( s(X2) != s(X1) )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_2520]) ).
tcf(c_3706,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(X1))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2727]) ).
tcf(c_3707,plain,
( ~ r(s(z),s(z))
| ~ r(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_3706]) ).
tcf(c_3722,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(s(X1))))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2758]) ).
tcf(c_3757,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_2700]) ).
tcf(c_3758,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_3757]) ).
tcf(c_3855,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X0)))
| ~ b(s(z),s(s(s(X1))))
| ~ b(s(s(X0)),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2881]) ).
tcf(c_3858,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2881]) ).
tcf(c_3883,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(X1)))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2771]) ).
tcf(c_3977,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_2929]) ).
tcf(c_4006,plain,
! [X0: $i] :
( ( s(s(X0)) = z )
| ( s(s(s(X0))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_178]) ).
tcf(c_4007,plain,
( ( s(s(z)) = z )
| ( s(s(s(z))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_4006]) ).
tcf(c_4072,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_3011]) ).
tcf(c_4129,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(X1)))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3037]) ).
tcf(c_4131,plain,
! [X0: $i] :
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3080]) ).
tcf(c_4133,plain,
! [X0: $i] :
( ~ 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_1622]) ).
tcf(c_4134,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4133]) ).
tcf(c_4136,plain,
( ~ b(s(s(s(z))),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4131]) ).
tcf(c_4150,plain,
! [X0: $i,X1: $i] :
( ( s(s(X0)) = X1 )
| ( s(s(s(X0))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_188]) ).
tcf(c_4267,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),X1)
| ~ b(s(s(s(s(X0)))),X1)
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_3108]) ).
tcf(c_4316,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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_3145]) ).
tcf(c_4351,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(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3154]) ).
tcf(c_4426,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_1887]) ).
tcf(c_4427,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_4426]) ).
tcf(c_4718,plain,
! [X0: $i] :
( b(s(s(s(s(X0)))),z)
| r(s(s(s(s(X0)))),z)
| ( s(s(s(s(X0)))) = z ) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_4719,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_4718]) ).
tcf(c_4721,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_579]) ).
tcf(c_4725,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_315]) ).
tcf(c_4726,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_4725]) ).
tcf(c_4747,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(s(s(X0))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_3424]) ).
tcf(c_4748,plain,
( ( s(s(s(z))) = s(s(s(z))) )
| ( s(s(s(s(z)))) != s(s(s(s(z)))) ) ),
inference(instantiation,[status(thm)],[c_4747]) ).
tcf(c_4758,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),s(s(s(X1))))
| r(s(s(s(s(X0)))),s(s(s(X1))))
| ( s(s(s(s(X0)))) = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_1887]) ).
tcf(c_4887,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(X1)))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3706]) ).
tcf(c_4888,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_4887]) ).
tcf(c_4930,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(X0))) = s(X2) )
| ( s(X2) != s(s(X1)) )
| ( s(s(s(X0))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_3637]) ).
tcf(c_4989,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_4072]) ).
tcf(c_4990,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_4989]) ).
tcf(c_4996,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),s(s(s(X1))))
| ~ 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_4129]) ).
tcf(c_5017,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(s(s(X1))))
| ~ b(X2,s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_3883]) ).
tcf(c_5140,plain,
! [X0: $i] :
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4267]) ).
tcf(c_5141,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)))) ),
inference(instantiation,[status(thm)],[c_5140]) ).
tcf(c_5148,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(X0)))),X1)
| r(s(s(s(s(X0)))),X1)
| ( s(s(s(s(X0)))) = X1 ) ),
inference(instantiation,[status(thm)],[c_737]) ).
tcf(c_5238,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(z))),X1)
| ~ b(s(s(s(s(X0)))),X1)
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_3108]) ).
tcf(c_5243,plain,
! [X0: $i] :
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1622]) ).
tcf(c_5244,plain,
( ~ b(s(s(s(z))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_5243]) ).
tcf(c_5293,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_2585]) ).
tcf(c_5354,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(X2),s(s(s(X0))))
| ~ b(s(s(s(X0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4316]) ).
tcf(c_5488,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(s(z))))
| ~ b(s(s(s(s(X0)))),s(X1))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_4351]) ).
tcf(c_5489,plain,
( ~ b(s(z),s(s(s(z))))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5488]) ).
tcf(c_6054,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_4989]) ).
tcf(c_6063,plain,
! [X0: $i,X1: $i] :
( ~ 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_4996]) ).
tcf(c_6111,plain,
! [X0: $i] :
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_5238]) ).
tcf(c_6112,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_6111]) ).
tcf(c_6144,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(s(z))))
| ~ b(X1,s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5017]) ).
tcf(c_6179,plain,
! [X0: $i,X1: $i] :
( ~ r(z,s(X1))
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_2045]) ).
tcf(c_6180,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_1779]) ).
tcf(c_6182,plain,
! [X0: $i] :
( ~ r(s(s(z)),z)
| ~ r(s(s(s(s(X0)))),z)
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_6183,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_6182]) ).
tcf(c_6185,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_6180]) ).
tcf(c_6186,plain,
( ~ r(z,s(z))
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_6179]) ).
tcf(c_6188,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(X0)),z)
| ~ r(s(s(s(s(X1)))),z)
| ~ r(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1004]) ).
tcf(c_6389,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(s(s(s(X0)))),s(X2))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_4351]) ).
tcf(c_6402,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_4758]) ).
tcf(c_6482,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(s(z))))
| ~ b(s(X1),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_5354]) ).
tcf(c_6484,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))))) ),
inference(instantiation,[status(thm)],[c_5354]) ).
tcf(c_6485,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))))) ),
inference(instantiation,[status(thm)],[c_6484]) ).
tcf(c_6486,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(X1))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_5354]) ).
tcf(c_6540,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_2742]) ).
tcf(c_6541,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_1633]) ).
tcf(c_6570,plain,
! [X0: $i] :
( ( s(s(s(X0))) = s(z) )
| ( s(s(s(s(X0)))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_6571,plain,
( ( s(s(s(z))) = s(z) )
| ( s(s(s(s(z)))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_6570]) ).
tcf(c_6657,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),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_5354]) ).
tcf(c_6661,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),z)
| ~ b(z,s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3722]) ).
tcf(c_6662,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(s(X1)))),X2)
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3108]) ).
tcf(c_6667,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(X0))),s(s(z)))
| ~ b(s(s(s(s(X1)))),s(s(z)))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1622]) ).
tcf(c_6837,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(s(s(X0)))) = s(X2) )
| ( s(X2) != s(s(X1)) )
| ( s(s(s(s(X0)))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_4930]) ).
tcf(c_6839,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X2)) = s(s(s(s(X0)))) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(s(s(X0)))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_1537]) ).
tcf(c_6841,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_1533]) ).
tcf(c_6903,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(s(s(s(s(X1)))),X2)
| ~ r(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1818]) ).
tcf(c_6905,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(z),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_6903]) ).
tcf(c_6910,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X1),X2)
| ~ r(s(s(s(s(X0)))),X2)
| ~ r(s(s(s(s(X0)))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1920]) ).
tcf(c_6912,plain,
( ~ r(s(z),z)
| ~ r(s(s(s(s(z)))),z)
| ~ r(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_6910]) ).
tcf(c_7100,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_6837]) ).
tcf(c_7101,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_7100]) ).
tcf(c_7152,plain,
! [X0: $i] :
( b(s(s(s(s(s(X0))))),s(z))
| r(s(s(s(s(s(X0))))),s(z))
| ( s(s(s(s(s(X0))))) = s(z) ) ),
inference(instantiation,[status(thm)],[c_2462]) ).
tcf(c_7153,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_7152]) ).
tcf(c_7201,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X1)))),s(z))
| ~ r(s(s(s(s(X0)))),s(z))
| ~ r(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6054]) ).
tcf(c_7279,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_6841]) ).
tcf(c_7280,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_7279]) ).
tcf(c_7446,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),z)
| ~ r(s(s(s(s(X1)))),z)
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6188]) ).
tcf(c_7447,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_7446]) ).
tcf(c_7522,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(z)) ),
inference(instantiation,[status(thm)],[c_1796]) ).
tcf(c_7535,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(X2,s(s(s(s(X1)))))
| ~ r(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1822]) ).
tcf(c_7602,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_3424]) ).
tcf(c_7607,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_6402]) ).
tcf(c_7608,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_7607]) ).
tcf(c_7627,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_6540]) ).
tcf(c_7630,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_1192]) ).
tcf(c_7649,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_6541]) ).
tcf(c_7669,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(s(X0))))),X1)
| r(s(s(s(s(s(X0))))),X1)
| ( s(s(s(s(s(X0))))) = X1 ) ),
inference(instantiation,[status(thm)],[c_5148]) ).
tcf(c_7670,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_7669]) ).
tcf(c_7709,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_2700]) ).
tcf(c_7710,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_7709]) ).
tcf(c_7729,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(X1)))
| ~ r(s(X2),s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_6903]) ).
tcf(c_7730,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_7729]) ).
tcf(c_7852,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X2)),s(s(s(X1))))
| ~ r(s(s(s(s(X0)))),s(s(X2)))
| ~ r(s(s(s(s(X0)))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_2919]) ).
tcf(c_7853,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_7852]) ).
tcf(c_7921,plain,
! [X0: $i,X1: $i] :
( ~ 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_6667]) ).
tcf(c_8061,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(X2,s(X1))
| ~ b(s(s(s(X0))),X2)
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1320]) ).
tcf(c_8062,plain,
( ~ b(z,s(z))
| ~ b(s(s(s(z))),z)
| ~ b(s(s(s(z))),s(z)) ),
inference(instantiation,[status(thm)],[c_8061]) ).
tcf(c_8235,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(X2)),s(s(s(X0))))
| ~ b(s(s(X2)),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6657]) ).
tcf(c_8236,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(s(X0))))
| ~ b(s(z),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6657]) ).
tcf(c_8283,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),s(X2))
| ~ b(s(s(s(s(X1)))),s(X2))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6662]) ).
tcf(c_8402,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(z)))
| ~ r(X1,s(s(s(s(X0)))))
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_450]) ).
tcf(c_8440,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),X1)
| ~ r(s(s(s(s(X0)))),X1)
| ~ r(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_8458,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(z)),s(s(s(s(X1)))))
| ~ r(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_1362]) ).
tcf(c_8598,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(X1))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_1178]) ).
tcf(c_9044,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(X0))) = X1 )
| ( s(s(s(s(X0)))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_4150]) ).
tcf(c_9051,plain,
( ( s(s(s(z))) = z )
| ( s(s(s(s(z)))) != s(z) ) ),
inference(instantiation,[status(thm)],[c_9044]) ).
tcf(c_9135,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_7602]) ).
tcf(c_9136,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_9135]) ).
tcf(c_9615,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_7627]) ).
tcf(c_9616,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_9615]) ).
tcf(c_9713,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_7649]) ).
tcf(c_9714,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_9713]) ).
tcf(c_10029,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(s(s(X1)))))
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6661]) ).
tcf(c_10134,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(z))
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(z)) ),
inference(instantiation,[status(thm)],[c_7522]) ).
tcf(c_10135,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_10134]) ).
tcf(c_10136,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_7201]) ).
tcf(c_10137,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_10136]) ).
tcf(c_10196,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(z)))),s(X1))
| ~ 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_2742]) ).
tcf(c_10198,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_1636]) ).
tcf(c_10199,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_1626]) ).
tcf(c_10203,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_10199]) ).
tcf(c_10204,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_10198]) ).
tcf(c_10205,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_10196]) ).
tcf(c_10302,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_7630]) ).
tcf(c_10303,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_10302]) ).
tcf(c_10418,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_7709]) ).
tcf(c_10419,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_10418]) ).
tcf(c_10466,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X0),X2)
| ~ r(X2,s(s(s(s(s(X1))))))
| ~ r(s(X0),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_7535]) ).
tcf(c_10467,plain,
( ~ r(s(z),z)
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(z),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_10466]) ).
tcf(c_10473,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(X2),s(s(s(X0))))
| ~ r(s(X2),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_3977]) ).
tcf(c_10474,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_10473]) ).
tcf(c_10491,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_2703]) ).
tcf(c_10492,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_10491]) ).
tcf(c_10665,plain,
! [X0: $i,X1: $i] :
( b(s(s(s(s(s(X0))))),s(s(s(X1))))
| r(s(s(s(s(s(X0))))),s(s(s(X1))))
| ( s(s(s(s(s(X0))))) = s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_4758]) ).
tcf(c_10666,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_10665]) ).
tcf(c_10706,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_1563,c_56]) ).
tcf(c_10767,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_3585]) ).
tcf(c_10786,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),s(z))
| ~ r(s(z),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_5293]) ).
tcf(c_10787,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_10786]) ).
tcf(c_10800,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(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6389]) ).
tcf(c_10925,plain,
! [X0: $i,X1: $i] :
( ~ r(X1,s(s(z)))
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_8402]) ).
tcf(c_10926,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_10925]) ).
tcf(c_10955,plain,
! [X0: $i] :
( ~ b(s(z),z)
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),s(z)) ),
inference(instantiation,[status(thm)],[c_3072]) ).
tcf(c_10956,plain,
! [X0: $i] :
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(s(X0)))),s(z))
| ~ b(s(s(s(s(X0)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_2805]) ).
tcf(c_10962,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(s(s(s(z)))),s(z))
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10956]) ).
tcf(c_10963,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(z)) ),
inference(instantiation,[status(thm)],[c_10955]) ).
tcf(c_11022,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(s(s(s(s(X1)))),z)
| ~ b(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3079]) ).
tcf(c_11023,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(z,s(s(s(s(X1)))))
| ~ b(s(X0),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_2897]) ).
tcf(c_11124,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),X1)
| ~ r(X1,s(s(s(s(X0)))))
| ~ r(s(s(s(z))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_1636]) ).
tcf(c_11155,plain,
! [X0: $i] :
( b(s(s(s(z))),s(s(s(s(s(X0))))))
| r(s(s(s(z))),s(s(s(s(s(X0))))))
| ( s(s(s(z))) = s(s(s(s(s(X0))))) ) ),
inference(instantiation,[status(thm)],[c_2971]) ).
tcf(c_11156,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_11155]) ).
tcf(c_11177,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(z)),X1)
| ~ r(s(s(s(s(s(X0))))),X1)
| ~ r(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_8440]) ).
tcf(c_11178,plain,
( ~ r(s(s(z)),z)
| ~ r(s(s(s(s(s(z))))),z)
| ~ r(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_11177]) ).
tcf(c_11194,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(X0))),s(s(z)))
| ~ r(s(s(z)),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_8458]) ).
tcf(c_11218,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(X1)))
| ~ b(s(s(s(X0))),z)
| ~ b(s(s(s(X0))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_8598]) ).
tcf(c_11407,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(X2),s(s(s(s(X1)))))
| ~ b(s(X2),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_6486]) ).
tcf(c_11489,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_1965]) ).
tcf(c_11490,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_11489]) ).
tcf(c_11537,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = X1 )
| ( X1 != s(s(s(s(X0)))) )
| ( s(s(s(s(X0)))) != s(s(s(s(X0)))) ) ),
inference(instantiation,[status(thm)],[c_2226]) ).
tcf(c_11638,plain,
! [X0: $i] :
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(X0))))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_7921]) ).
tcf(c_11640,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(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_6063]) ).
tcf(c_11641,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(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_11640]) ).
tcf(c_11643,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_11638]) ).
tcf(c_11713,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(s(s(s(s(X0))))) )
| ( X2 != X1 )
| ( s(s(s(s(s(X0))))) != X1 ) ),
inference(instantiation,[status(thm)],[c_2278]) ).
tcf(c_11752,plain,
! [X0: $i,X1: $i] :
( ( X0 = s(s(s(s(X1)))) )
| ( s(X0) != s(s(s(s(s(X1))))) ) ),
inference(instantiation,[status(thm)],[c_245]) ).
tcf(c_11753,plain,
( ( z = s(s(s(s(z)))) )
| ( s(z) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_11752]) ).
tcf(c_11810,plain,
! [X0: $i] : s(s(s(s(X0)))) != z,
inference(instantiation,[status(thm)],[c_2248]) ).
tcf(c_11811,plain,
s(s(s(s(z)))) != z,
inference(instantiation,[status(thm)],[c_11810]) ).
tcf(c_12358,plain,
! [X0: $i] :
( ~ 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_7921]) ).
tcf(c_12363,plain,
( ~ b(s(s(s(s(z)))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(z)))
| ~ b(s(s(s(s(s(z))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_12358]) ).
tcf(c_13329,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(s(X1)))))
| ~ b(s(s(s(X0))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_8235]) ).
tcf(c_13558,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(s(s(X1)))))
| ~ b(s(z),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_8236]) ).
tcf(c_13562,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(s(X0)))))
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_3858]) ).
tcf(c_13576,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X0)))
| ~ b(s(z),s(s(s(s(X1)))))
| ~ b(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_3855]) ).
tcf(c_14743,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = s(s(s(s(s(X0))))) )
| ( X2 != s(X1) )
| ( s(s(s(s(s(X0))))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_11713]) ).
tcf(c_14772,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_11752]) ).
tcf(c_14773,plain,
( ( s(z) = s(s(s(s(z)))) )
| ( s(s(z)) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_14772]) ).
tcf(c_15376,plain,
! [X0: $i] :
( ~ b(s(s(s(s(z)))),z)
| ~ b(z,s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_10029]) ).
tcf(c_15377,plain,
( ~ b(s(s(s(s(z)))),z)
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(s(s(s(z)))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_15376]) ).
tcf(c_15747,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_10767]) ).
tcf(c_15898,plain,
! [X0: $i,X1: $i] :
( ~ r(s(X1),s(s(z)))
| ~ r(s(X1),s(s(s(s(s(X0))))))
| ~ r(s(s(s(s(s(X0))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_10925]) ).
tcf(c_15899,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_15898]) ).
tcf(c_16024,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(X0)),z)
| ~ b(s(s(s(s(X1)))),z)
| ~ b(s(s(X0)),s(s(s(s(X1))))) ),
inference(instantiation,[status(thm)],[c_11022]) ).
tcf(c_16025,plain,
( ~ b(s(s(z)),z)
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(z)),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_16024]) ).
tcf(c_16099,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r(s(s(X0)),X2)
| ~ r(X2,s(s(s(s(s(X1))))))
| ~ r(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_10466]) ).
tcf(c_16100,plain,
( ~ r(s(s(z)),z)
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(z)),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_16099]) ).
tcf(c_16103,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),X1)
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(z),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_10466]) ).
tcf(c_16115,plain,
! [X0: $i,X1: $i] :
( ~ r(s(z),s(s(s(X0))))
| ~ r(s(z),s(s(s(s(s(X1))))))
| ~ r(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_10473]) ).
tcf(c_16165,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(s(X0)))),s(s(z)))
| ~ r(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_11194]) ).
tcf(c_16166,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_16165]) ).
tcf(c_16488,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(z,s(s(s(s(s(X1))))))
| ~ b(s(X0),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_11023]) ).
tcf(c_16489,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X0),z)
| ~ b(s(s(s(s(s(X1))))),z)
| ~ b(s(X0),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_11022]) ).
tcf(c_16492,plain,
( ~ b(s(z),z)
| ~ b(s(s(s(s(s(z))))),z)
| ~ b(s(z),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_16489]) ).
tcf(c_16493,plain,
( ~ b(s(z),z)
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(z),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_16488]) ).
tcf(c_16569,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_1845]) ).
tcf(c_16570,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_16569]) ).
tcf(c_17373,plain,
! [X0: $i,X1: $i] :
( ~ b(z,s(s(X1)))
| ~ b(s(s(s(s(X0)))),z)
| ~ b(s(s(s(s(X0)))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_11218]) ).
tcf(c_17374,plain,
( ~ b(z,s(s(z)))
| ~ b(s(s(s(s(z)))),z)
| ~ b(s(s(s(s(z)))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_17373]) ).
tcf(c_17809,plain,
! [X0: $i,X1: $i] :
( r(s(X1),z)
| b(s(z),s(X1))
| r(s(z),s(X1))
| r(s(s(X0)),s(X1))
| ~ b(s(s(X0)),z) ),
inference(resolution,[status(thm)],[c_10706,c_644]) ).
tcf(c_17812,plain,
( r(s(z),z)
| b(s(z),s(z))
| r(s(z),s(z))
| r(s(s(z)),s(z))
| ~ b(s(s(z)),z) ),
inference(instantiation,[status(thm)],[c_17809]) ).
tcf(c_17976,plain,
! [X0: $i] : s(s(s(s(s(X0))))) != z,
inference(instantiation,[status(thm)],[c_11810]) ).
tcf(c_17977,plain,
s(s(s(s(s(z))))) != z,
inference(instantiation,[status(thm)],[c_17976]) ).
tcf(c_18052,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_11537]) ).
tcf(c_18053,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_18052]) ).
tcf(c_18093,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(z)),s(s(s(X0))))
| ~ b(s(s(z)),s(s(s(s(s(X1))))))
| ~ b(s(s(s(X0))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_13329]) ).
tcf(c_18094,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)))))) ),
inference(instantiation,[status(thm)],[c_18093]) ).
tcf(c_18100,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(s(s(X0)))))
| ~ b(s(z),s(s(s(s(s(X1))))))
| ~ b(s(s(s(s(X0)))),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_13558]) ).
tcf(c_18101,plain,
( ~ b(s(z),s(s(s(s(z)))))
| ~ b(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_18100]) ).
tcf(c_18113,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X1)))
| ~ b(s(z),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_13562]) ).
tcf(c_18114,plain,
( ~ b(s(z),s(s(z)))
| ~ b(s(z),s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(z))) ),
inference(instantiation,[status(thm)],[c_18113]) ).
tcf(c_18233,plain,
! [X0: $i,X1: $i] :
( ~ b(s(z),s(s(X0)))
| ~ b(s(z),s(s(s(s(s(X1))))))
| ~ b(s(s(X0)),s(s(s(s(s(X1)))))) ),
inference(instantiation,[status(thm)],[c_13576]) ).
tcf(c_18234,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)))))) ),
inference(instantiation,[status(thm)],[c_18233]) ).
tcf(c_18796,plain,
! [X0: $i,X1: $i] :
( ~ r(s(s(s(z))),X1)
| ~ r(X1,s(s(s(s(s(X0))))))
| ~ r(s(s(s(z))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_11124]) ).
tcf(c_18801,plain,
( ~ r(s(s(s(z))),z)
| ~ r(z,s(s(s(s(s(z))))))
| ~ r(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_18796]) ).
tcf(c_19111,plain,
! [X0: $i,X1: $i] :
( ~ b(s(s(s(s(z)))),s(X1))
| ~ b(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_10800]) ).
tcf(c_19112,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(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_19111]) ).
tcf(c_19594,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(s(s(z)))))
| ~ b(s(X1),s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(s(z))))) ),
inference(instantiation,[status(thm)],[c_11407]) ).
tcf(c_19595,plain,
( ~ b(s(z),s(s(s(s(z)))))
| ~ b(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_19594]) ).
tcf(c_20456,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(s(X2)) = s(s(s(s(s(X0))))) )
| ( s(s(X2)) != s(s(X1)) )
| ( s(s(s(s(s(X0))))) != s(s(X1)) ) ),
inference(instantiation,[status(thm)],[c_6839]) ).
tcf(c_20461,plain,
( ( s(s(z)) = s(s(s(s(s(z))))) )
| ( s(s(z)) != s(s(z)) )
| ( s(s(s(s(s(z))))) != s(s(z)) ) ),
inference(instantiation,[status(thm)],[c_20456]) ).
tcf(c_20967,plain,
! [X0: $i,X1: $i] :
( ( s(s(s(s(X0)))) = s(s(X1)) )
| ( s(s(s(s(s(X0))))) != s(s(s(X1))) ) ),
inference(instantiation,[status(thm)],[c_3424]) ).
tcf(c_20968,plain,
( ( s(s(s(s(z)))) = s(s(z)) )
| ( s(s(s(s(s(z))))) != s(s(s(z))) ) ),
inference(instantiation,[status(thm)],[c_20967]) ).
tcf(c_21162,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_4721]) ).
tcf(c_21163,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_21162]) ).
tcf(c_21514,plain,
! [X0: $i] : s(s(s(s(s(X0))))) = s(s(s(s(s(X0))))),
inference(instantiation,[status(thm)],[c_3475]) ).
tcf(c_21515,plain,
s(s(s(s(s(z))))) = s(s(s(s(s(z))))),
inference(instantiation,[status(thm)],[c_21514]) ).
tcf(c_21892,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_14772]) ).
tcf(c_21893,plain,
( ( s(s(z)) = s(s(s(s(z)))) )
| ( s(s(s(z))) != s(s(s(s(s(z))))) ) ),
inference(instantiation,[status(thm)],[c_21892]) ).
tcf(c_22525,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s(X2) = s(s(s(s(s(X0))))) )
| ( s(X2) != s(X1) )
| ( s(s(s(s(s(X0))))) != s(X1) ) ),
inference(instantiation,[status(thm)],[c_14743]) ).
tcf(c_22526,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_22525]) ).
tcf(c_22652,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_15747]) ).
tcf(c_22653,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_22652]) ).
tcf(c_22857,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_16103]) ).
tcf(c_22858,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_22857]) ).
tcf(c_23765,plain,
! [X0: $i,X1: $i] :
( ~ b(X1,s(s(s(z))))
| ~ b(X1,s(s(s(s(s(X0))))))
| ~ b(s(s(s(s(s(X0))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_6144]) ).
tcf(c_23766,plain,
( ~ b(z,s(s(s(z))))
| ~ b(z,s(s(s(s(s(z))))))
| ~ b(s(s(s(s(s(z))))),s(s(s(z)))) ),
inference(instantiation,[status(thm)],[c_23765]) ).
tcf(c_23769,plain,
! [X0: $i,X1: $i] :
( ~ b(s(X1),s(s(s(z))))
| ~ 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_6482]) ).
tcf(c_23770,plain,
( ~ 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(s(z)))) ),
inference(instantiation,[status(thm)],[c_23769]) ).
tcf(c_24092,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ b(s(s(s(X0))),s(X2))
| ~ 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_8283]) ).
tcf(c_24093,plain,
( ~ b(s(s(s(z))),s(z))
| ~ b(s(s(s(s(s(z))))),s(z))
| ~ b(s(s(s(z))),s(s(s(s(s(z)))))) ),
inference(instantiation,[status(thm)],[c_24092]) ).
tcf(c_24294,plain,
! [X0: $i] :
( ~ r(s(z),s(s(s(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_16115]) ).
tcf(c_24295,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_24294]) ).
tcf(c_24315,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_24295,c_24093,c_23770,c_23766,c_22858,c_22653,c_22526,c_21893,c_21515,c_21163,c_20968,c_20461,c_19595,c_19112,c_18801,c_18234,c_18114,c_18101,c_18094,c_18053,c_17977,c_17812,c_17374,c_16570,c_16493,c_16492,c_16166,c_16100,c_16025,c_15899,c_15377,c_14773,c_12363,c_11811,c_11753,c_11643,c_11641,c_11490,c_11178,c_11156,c_10963,c_10962,c_10926,c_10787,c_10666,c_10492,c_10474,c_10467,c_10419,c_10303,c_10205,c_10204,c_10203,c_10137,c_10135,c_9714,c_9616,c_9136,c_9051,c_8062,c_7853,c_7730,c_7710,c_7670,c_7608,c_7447,c_7280,c_7153,c_7101,c_6912,c_6905,c_6571,c_6485,c_6186,c_6185,c_6183,c_6112,c_5489,c_5244,c_5141,c_4990,c_4888,c_4748,c_4726,c_4719,c_4427,c_4136,c_4134,c_4007,c_3758,c_3707,c_3586,c_3476,c_3429,c_3423,c_3074,c_3073,c_2972,c_2794,c_2756,c_2701,c_2692,c_2463,c_2411,c_2249,c_2227,c_2057,c_2056,c_1966,c_1851,c_1849,c_1805,c_1799,c_1647,c_1644,c_1615,c_1357,c_1239,c_1177,c_1170,c_1046,c_1037,c_1005,c_981,c_907,c_873,c_859,c_853,c_750,c_682,c_647,c_620,c_580,c_504,c_490,c_454,c_434,c_342,c_322,c_316,c_281,c_230,c_229,c_226,c_209,c_191,c_186,c_181,c_180,c_65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA172-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/11.63 % Computer : n013.cluster.edu
% 0.10/11.63 % Model : x86_64 x86_64
% 0.10/11.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/11.63 % Memory : 8046.5625MB
% 0.10/11.63 % OS : Linux 6.8.0-71-generic
% 0.10/11.63 % CPULimit : 300
% 0.10/11.63 % WCLimit : 300
% 0.10/11.63 % DateTime : Wed Sep 23 13:08:06 UTC 2026
% 0.10/11.63 % CPUTime :
% 0.10/11.63 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/11.67 Running first-order theorem proving
% 0.10/11.67 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/11.68
% 0.10/11.68 % ======== iProver multi-core TPTP/SMT =========
% 0.10/11.68
% 0.10/11.68 % Detected problem language: tptp
% 0.10/11.70 % Proving...
% 6.63/13.00 % SZS status Started for theBenchmark.p
% 6.63/13.00 % SZS status Unsatisfiable for theBenchmark.p
% 6.63/13.00
% 6.63/13.00 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.63/13.00
% 6.63/13.00 % ------ iProver source info
% 6.63/13.00
% 6.63/13.00 % git: date: 2026-07-19 20:42:38 +0200
% 6.63/13.00 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.63/13.00 % git: non_committed_changes: false
% 6.63/13.00
% 6.63/13.00 % ------ Parsing...% successful
% 6.63/13.00
% 6.63/13.00
% 6.63/13.00 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.63/13.00
% 6.63/13.00 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 6.63/13.00
% 6.63/13.00 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.63/13.00
% 6.63/13.00 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 6.63/13.00 % ------ Proving...
% 6.63/13.00 % ------ Problem Properties
% 6.63/13.00
% 6.63/13.00 %
% 6.63/13.00 % clauses 7
% 6.63/13.00 % conjectures 0
% 6.63/13.00 % EPR 5
% 6.63/13.00 % Horn 6
% 6.63/13.00 % unary 3
% 6.63/13.00 % binary 1
% 6.63/13.00 % lits 14
% 6.63/13.00 % lits eq 4
% 6.63/13.00 % fd_pure 0
% 6.63/13.00 % fd_pseudo 0
% 6.63/13.00 % fd_cond 0
% 6.63/13.00 % fd_pseudo_cond 2
% 6.63/13.00 % AC symbols 0
% 6.63/13.00
% 6.63/13.00 % ------ Input Options Time Limit: Unbounded
% 6.63/13.00
% 6.63/13.00
% 6.63/13.00 % ------
% 6.63/13.00 % Current options:
% 6.63/13.00 % ------
% 6.63/13.00
% 6.63/13.00
% 6.63/13.00 %
% 6.63/13.00
% 6.63/13.00 % ------ Proving...
% 6.63/13.00 %
% 6.63/13.00
% 6.63/13.00 % SZS status Unsatisfiable for theBenchmark.p
% 6.63/13.00
% 6.63/13.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.63/13.01
% 6.63/13.01
%------------------------------------------------------------------------------