%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRA118-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:23:49 PM UTC 2026
% Result : Unsatisfiable 3.96s 2.00s
% Output : CNFRefutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 416 ( 19 unt; 0 def)
% Number of atoms : 2031 (1100 equ)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 2196 ( 581 ~;1615 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 7 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 : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 594 ( 0 sgn 594 !; 0 ?; 583 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rsym) ).
fof(f2,axiom,
! [X2,X0,X1] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rn3cl) ).
fof(f3,axiom,
! [X2,X0,X1] :
( r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rn3acl) ).
fof(f4,axiom,
! [X0] : f(X0) != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pfnc) ).
fof(f5,axiom,
! [X0,X1] :
( X0 = X1
| f(X0) != f(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pfinj) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 )
| ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_57,plain,
! [X0: $i] : f(X0) != c,
inference(cnf_transformation,[],[f4]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( f(X0) != f(X1) ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_59,plain,
f(c) != c,
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_100,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_191,plain,
! [X0: $i,X1: $i] :
( ( c = X1 )
| ( f(X0) = c )
| ( f(X0) = X1 )
| ~ r(c,X1)
| ~ r(f(X0),c)
| ~ r(f(X0),X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_192,plain,
! [X0: $i] :
( ( f(X0) = c )
| ( f(f(X0)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_193,plain,
( ( f(c) = c )
| ( f(f(c)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = c )
| ( c != X1 )
| ( f(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i] :
( ( f(c) = X1 )
| ( f(f(X0)) = X1 )
| ( f(f(X0)) = f(c) )
| ~ r(f(c),X1)
| ~ r(f(f(X0)),X1)
| ~ r(f(f(X0)),f(c)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_196,plain,
! [X0: $i] :
( ( f(f(X0)) = f(c) )
| ( f(f(f(X0))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_197,plain,
( ( f(f(c)) = f(c) )
| ( f(f(f(c))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_198,plain,
( ( f(c) = c )
| ( f(f(c)) = c )
| ( f(f(c)) = f(c) )
| ~ r(f(c),c)
| ~ r(f(f(c)),c)
| ~ r(f(f(c)),f(c)) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(c) != X1 )
| ( f(f(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( f(X0) = X2 )
| ( f(X0) = X1 )
| ~ r(X1,X2)
| ~ r(f(X0),X2)
| ~ r(f(X0),X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = X1 )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_202,plain,
! [X0: $i] :
( ( f(X0) = c )
| ( c != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_203,plain,
( ( f(c) = c )
| ( c != f(c) )
| ( f(c) != f(c) ) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X0) = X2 )
| ( X2 != X1 )
| ( f(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_219,plain,
! [X0: $i] : f(X0) = f(X0),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_220,plain,
f(c) = f(c),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_224,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = X1 )
| ( X1 != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_226,plain,
! [X0: $i,X1: $i] :
( r(X0,X1)
| r(f(c),X1)
| r(f(c),X0)
| ( X0 = X1 )
| ( f(c) = X1 )
| ( f(c) = X0 ) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X1,X2)
| r(f(X0),X2)
| r(f(X0),X1)
| ( X1 = X2 )
| ( f(X0) = X2 )
| ( f(X0) = X1 ) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_230,plain,
! [X0: $i,X1: $i] :
( r(f(X1),X0)
| ~ r(X0,f(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_234,plain,
! [X0: $i] : f(f(X0)) = f(f(X0)),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_235,plain,
f(f(c)) = f(f(c)),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_236,plain,
! [X0: $i,X1: $i] :
( ( c = f(X1) )
| ( f(X0) = c )
| ( f(X0) = f(X1) )
| ~ r(c,f(X1))
| ~ r(f(X0),c)
| ~ r(f(X0),f(X1)) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_237,plain,
! [X0: $i,X1: $i] :
( ( c = X1 )
| ( c = f(X0) )
| ( f(X0) = X1 )
| ~ r(c,X1)
| ~ r(c,f(X0))
| ~ r(f(X0),X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_238,plain,
! [X0: $i] :
( ( c = f(X0) )
| ( f(c) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_239,plain,
( ( c = f(c) )
| ( f(c) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X1 )
| ( X2 = f(X0) )
| ( f(X0) = X1 )
| ~ r(X2,X1)
| ~ r(X2,f(X0))
| ~ r(f(X0),X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(X1,f(X0))
| r(f(c),f(X0))
| ( X1 = f(X0) )
| ( f(c) = X1 )
| ( f(c) = f(X0) ) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_268,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,X1)
| r(X2,f(X0))
| r(f(X0),X1)
| ( X2 = X1 )
| ( X2 = f(X0) )
| ( f(X0) = X1 ) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(f(X0),X1)
| r(f(X0),f(c))
| ( f(c) = X1 )
| ( f(X0) = X1 )
| ( f(X0) = f(c) ) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X1),X2)
| r(f(X0),X2)
| r(f(X0),f(X1))
| ( f(X1) = X2 )
| ( f(X0) = X2 )
| ( f(X0) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] :
( r(X1,f(c))
| r(f(X0),X1)
| r(f(X0),f(c))
| ( X1 = f(c) )
| ( f(X0) = X1 )
| ( f(X0) = f(c) ) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(f(X0),X2)
| r(f(X0),f(X1))
| ( X2 = f(X1) )
| ( f(X0) = X2 )
| ( f(X0) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_327,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(c) != f(X1) )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(X1,f(f(X0)))
| r(f(c),f(f(X0)))
| ( X1 = f(f(X0)) )
| ( f(c) = X1 )
| ( f(c) = f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_379,plain,
! [X0: $i,X1: $i] :
( ( c = f(X1) )
| ( c = f(X0) )
| ( f(X0) = f(X1) )
| ~ r(c,f(X1))
| ~ r(c,f(X0))
| ~ r(f(X0),f(X1)) ),
inference(instantiation,[status(thm)],[c_237]) ).
tcf(c_390,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(f(f(X0)),X1)
| r(f(f(X0)),f(c))
| ( f(c) = X1 )
| ( f(f(X0)) = X1 )
| ( f(f(X0)) = f(c) ) ),
inference(instantiation,[status(thm)],[c_270]) ).
tcf(c_391,plain,
( r(f(c),c)
| r(f(f(c)),c)
| r(f(f(c)),f(c))
| ( f(c) = c )
| ( f(f(c)) = c )
| ( f(f(c)) = f(c) ) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_398,plain,
! [X0: $i] :
( ( f(c) = f(X0) )
| ( f(c) != f(c) )
| ( f(X0) != f(c) ) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_432,plain,
! [X0: $i,X1: $i] :
( r(X1,f(c))
| r(f(f(X0)),X1)
| r(f(f(X0)),f(c))
| ( X1 = f(c) )
| ( f(f(X0)) = X1 )
| ( f(f(X0)) = f(c) ) ),
inference(instantiation,[status(thm)],[c_272]) ).
tcf(c_433,plain,
( r(c,f(c))
| r(f(f(c)),c)
| r(f(f(c)),f(c))
| ( c = f(c) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(c) ) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_451,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(X2,f(X0))
| r(f(X0),f(X1))
| ( X2 = f(X1) )
| ( X2 = f(X0) )
| ( f(X0) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_268]) ).
tcf(c_459,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),X1)
| r(f(f(f(X0))),X1)
| r(f(f(f(X0))),f(f(c)))
| ( f(f(c)) = X1 )
| ( f(f(f(X0))) = X1 )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_462,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X1),X2)
| r(f(f(X0)),X2)
| r(f(f(X0)),f(X1))
| ( f(X1) = X2 )
| ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(X1) )
| ( f(X1) != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_465,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),X1)
| r(f(f(X0)),X1)
| r(f(X2),f(f(X0)))
| ( f(X2) = X1 )
| ( f(X2) = f(f(X0)) )
| ( f(f(X0)) = X1 ) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_553,plain,
! [X0: $i] :
( ( c = f(c) )
| ( f(f(X0)) = c )
| ( f(f(X0)) = f(c) )
| ~ r(c,f(c))
| ~ r(f(f(X0)),c)
| ~ r(f(f(X0)),f(c)) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_554,plain,
( ( c = f(c) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(c) )
| ~ r(c,f(c))
| ~ r(f(f(c)),c)
| ~ r(f(f(c)),f(c)) ),
inference(instantiation,[status(thm)],[c_553]) ).
tcf(c_559,plain,
! [X0: $i] :
( ( c = f(f(c)) )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(c,f(f(c)))
| ~ r(f(f(f(X0))),c)
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_561,plain,
! [X0: $i] :
( ( c = f(X0) )
| ( f(c) = c )
| ( f(c) = f(X0) )
| ~ r(f(c),c)
| ~ r(c,f(X0))
| ~ r(f(c),f(X0)) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i] :
( ( c = f(X1) )
| ( f(f(X0)) = c )
| ( f(f(X0)) = f(X1) )
| ~ r(c,f(X1))
| ~ r(f(f(X0)),c)
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_565,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(X1)) )
| ( f(X0) = c )
| ( f(X0) = f(f(X1)) )
| ~ r(f(X0),c)
| ~ r(c,f(f(X1)))
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_236]) ).
tcf(c_567,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = c )
| ( f(X0) = c )
| ( f(X0) = f(X1) )
| ~ r(f(X1),c)
| ~ r(f(X0),c)
| ~ r(f(X0),f(X1)) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_568,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(c) )
| ( f(X0) = f(f(X1)) )
| ( f(f(X1)) = f(c) )
| ~ r(f(X0),f(c))
| ~ r(f(f(X1)),f(c))
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_569,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X1) = X2 )
| ( f(X0) = X2 )
| ( f(X0) = f(X1) )
| ~ r(f(X1),X2)
| ~ r(f(X0),X2)
| ~ r(f(X0),f(X1)) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_584,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = f(X1) )
| ( X2 = f(X0) )
| ( f(X0) = f(X1) )
| ~ r(X2,f(X1))
| ~ r(X2,f(X0))
| ~ r(f(X0),f(X1)) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_707,plain,
! [X0: $i] :
( ( f(c) = f(f(X0)) )
| ( f(c) != f(c) )
| ( f(f(X0)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_793,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(X1) )
| ( f(X1) != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_463]) ).
tcf(c_830,plain,
! [X0: $i] :
( ( c = f(f(X0)) )
| ( f(c) = c )
| ( f(c) = f(f(X0)) )
| ~ r(f(c),c)
| ~ r(c,f(f(X0)))
| ~ r(f(c),f(f(X0))) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_836,plain,
! [X0: $i,X1: $i] :
( r(f(c),f(f(X1)))
| r(f(c),f(f(X0)))
| r(f(f(X0)),f(f(X1)))
| ( f(c) = f(f(X1)) )
| ( f(c) = f(f(X0)) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_846,plain,
! [X0: $i,X1: $i] :
( ( c = f(X1) )
| ( c = f(f(X0)) )
| ( f(f(X0)) = f(X1) )
| ~ r(c,f(X1))
| ~ r(c,f(f(X0)))
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_857,plain,
! [X0: $i,X1: $i] :
( r(f(c),f(f(X1)))
| r(f(f(X0)),f(c))
| r(f(f(X0)),f(f(X1)))
| ( f(c) = f(f(X1)) )
| ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_882,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),f(X1))
| r(f(f(X0)),f(X2))
| r(f(f(X0)),f(X1))
| ( f(X2) = f(X1) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_883,plain,
! [X0: $i] :
( ( c = f(X0) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(X0) )
| ~ r(c,f(X0))
| ~ r(f(f(c)),c)
| ~ r(f(f(c)),f(X0)) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_885,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(X0))
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_230]) ).
tcf(c_889,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X1),f(X2))
| r(f(f(X0)),f(X2))
| r(f(f(X0)),f(X1))
| ( f(X1) = f(X2) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_1019,plain,
! [X0: $i,X1: $i] :
( r(c,f(X0))
| r(c,f(f(X1)))
| r(f(X0),f(f(X1)))
| ( c = f(X0) )
| ( c = f(f(X1)) )
| ( f(X0) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_1027,plain,
! [X0: $i] :
( ( f(f(c)) = c )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(f(c)),c)
| ~ r(f(f(f(X0))),c)
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_567]) ).
tcf(c_1030,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = c )
| ( f(f(X0)) = c )
| ( f(f(X0)) = f(X1) )
| ~ r(f(X1),c)
| ~ r(f(f(X0)),c)
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_567]) ).
tcf(c_1035,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = c )
| ( f(X0) = f(f(X1)) )
| ( f(f(X1)) = c )
| ~ r(f(X0),c)
| ~ r(f(f(X1)),c)
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_567]) ).
tcf(c_1040,plain,
! [X0: $i,X1: $i] :
( ( f(f(X1)) = f(c) )
| ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(f(X1)),f(c))
| ~ r(f(f(X0)),f(c))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_568]) ).
tcf(c_1068,plain,
! [X0: $i] : f(f(X0)) != c,
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_1069,plain,
f(f(c)) != c,
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_1078,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(X0)) = X2 )
| ( X2 != X1 )
| ( f(f(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_1080,plain,
! [X0: $i] :
( ( f(c) = f(f(c)) )
| ( f(f(f(X0))) = f(c) )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(f(f(X0))),f(c))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_1097,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = X1 )
| ( f(f(f(X0))) = X1 )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(f(c)),X1)
| ~ r(f(f(f(X0))),X1)
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_1099,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X1) = X2 )
| ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(X1) )
| ~ r(f(X1),X2)
| ~ r(f(f(X0)),X2)
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_1104,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X0) = X2 )
| ( f(X0) = f(f(X1)) )
| ( f(f(X1)) = X2 )
| ~ r(f(X0),X2)
| ~ r(f(f(X1)),X2)
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_1160,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = f(X0) )
| ( X2 = f(f(X1)) )
| ( f(X0) = f(f(X1)) )
| ~ r(X2,f(X0))
| ~ r(X2,f(f(X1)))
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_584]) ).
tcf(c_1170,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(X0)),c)
| r(f(f(c)),f(f(X0)))
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(X0)) )
| ( f(f(X0)) = c ) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_1414,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(X0)) = X2 )
| ( X2 != f(X1) )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_1078]) ).
tcf(c_1453,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(X0)))
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_230]) ).
tcf(c_1457,plain,
! [X0: $i] :
( r(f(f(X0)),c)
| ~ r(c,f(f(X0))) ),
inference(instantiation,[status(thm)],[c_230]) ).
tcf(c_1574,plain,
! [X0: $i] :
( ( c = f(f(X0)) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(X0)) )
| ~ r(f(f(c)),c)
| ~ r(c,f(f(X0)))
| ~ r(f(f(c)),f(f(X0))) ),
inference(instantiation,[status(thm)],[c_883]) ).
tcf(c_1594,plain,
! [X0: $i,X1: $i] :
( r(X1,f(f(c)))
| r(f(f(f(X0))),X1)
| r(f(f(f(X0))),f(f(c)))
| ( X1 = f(f(c)) )
| ( f(f(f(X0))) = X1 )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1596,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(f(f(X0)),X2)
| r(f(f(X0)),f(X1))
| ( X2 = f(X1) )
| ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1613,plain,
! [X0: $i] :
( r(c,f(c))
| r(c,f(f(X0)))
| r(f(c),f(f(X0)))
| ( c = f(c) )
| ( c = f(f(X0)) )
| ( f(c) = f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_1019]) ).
tcf(c_1647,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(f(f(f(X0))),X1)
| r(f(f(f(X0))),f(c))
| ( f(c) = X1 )
| ( f(f(f(X0))) = X1 )
| ( f(f(f(X0))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_1693,plain,
! [X0: $i,X1: $i] :
( r(X1,f(f(c)))
| r(X1,f(f(f(X0))))
| r(f(f(f(X0))),f(f(c)))
| ( X1 = f(f(c)) )
| ( X1 = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_1694,plain,
( r(c,f(f(c)))
| r(c,f(f(f(c))))
| r(f(f(f(c))),f(f(c)))
| ( c = f(f(c)) )
| ( c = f(f(f(c))) )
| ( f(f(f(c))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_1693]) ).
tcf(c_1695,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(X2,f(f(X0)))
| r(f(f(X0)),f(X1))
| ( X2 = f(X1) )
| ( X2 = f(f(X0)) )
| ( f(f(X0)) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_1719,plain,
! [X0: $i,X1: $i] :
( ( f(c) = f(f(X1)) )
| ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(c),f(f(X1)))
| ~ r(f(f(X0)),f(c))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1099]) ).
tcf(c_1720,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(X1)) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(X2),f(f(X1)))
| ~ r(f(f(X0)),f(X2))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1099]) ).
tcf(c_1757,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(X1))
| r(f(f(f(X0))),f(X1))
| r(f(f(f(X0))),f(f(c)))
| ( f(f(c)) = f(X1) )
| ( f(f(f(X0))) = f(X1) )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_459]) ).
tcf(c_1765,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(X1)) )
| ( f(f(X0)) = c )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(c,f(f(X1)))
| ~ r(f(f(X0)),c)
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_1845,plain,
! [X0: $i] :
( r(c,f(f(c)))
| r(c,f(f(f(X0))))
| r(f(f(f(X0))),f(f(c)))
| ( c = f(f(c)) )
| ( c = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_1019]) ).
tcf(c_1849,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(c)))
| r(f(f(f(X0))),f(X1))
| r(f(f(f(X0))),f(f(c)))
| ( f(X1) = f(f(c)) )
| ( f(f(f(X0))) = f(X1) )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_1872,plain,
! [X0: $i] :
( ( f(f(c)) = f(c) )
| ( f(f(f(X0))) = f(c) )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(X0))),f(c))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_1040]) ).
tcf(c_1880,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(X1) )
| ( f(f(X0)) != f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_1887,plain,
! [X0: $i] :
( ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(c) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(X0))),f(c))
| ~ r(f(f(c)),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_1040]) ).
tcf(c_1889,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(f(X1)) )
| ( f(f(X1)) != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_793]) ).
tcf(c_2111,plain,
! [X0: $i,X1: $i] :
( ( f(c) = f(f(X1)) )
| ( f(c) = f(f(X0)) )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(c),f(f(X1)))
| ~ r(f(c),f(f(X0)))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1104]) ).
tcf(c_2112,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(X1)) )
| ( f(X2) = f(f(X0)) )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(X2),f(f(X1)))
| ~ r(f(X2),f(f(X0)))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1104]) ).
tcf(c_2234,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(X0)) )
| ( f(f(c)) = f(X1) )
| ( f(f(c)) = f(f(X0)) )
| ~ r(f(f(c)),f(X1))
| ~ r(f(X1),f(f(X0)))
| ~ r(f(f(c)),f(f(X0))) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_2285,plain,
! [X0: $i,X1: $i] :
( ( f(f(X1)) = c )
| ( f(f(X0)) = c )
| ( f(f(X0)) = f(f(X1)) )
| ~ r(f(f(X1)),c)
| ~ r(f(f(X0)),c)
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1035]) ).
tcf(c_2292,plain,
! [X0: $i] :
( r(f(f(f(X0))),c)
| ~ r(c,f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_2293,plain,
( r(f(f(f(c))),c)
| ~ r(c,f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_2292]) ).
tcf(c_2370,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(X0))) )
| ( f(f(c)) != f(f(c)) )
| ( f(f(f(X0))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_1889]) ).
tcf(c_2415,plain,
! [X0: $i,X1: $i] :
( r(f(c),X1)
| r(X1,f(f(f(X0))))
| r(f(c),f(f(f(X0))))
| ( X1 = f(f(f(X0))) )
| ( f(c) = X1 )
| ( f(c) = f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_2419,plain,
( r(f(c),c)
| r(c,f(f(f(c))))
| r(f(c),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( f(c) = c )
| ( f(c) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2415]) ).
tcf(c_2423,plain,
! [X0: $i,X1: $i] :
( r(f(f(X0)),f(c))
| r(f(c),f(f(f(X1))))
| r(f(f(X0)),f(f(f(X1))))
| ( f(c) = f(f(f(X1))) )
| ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_857]) ).
tcf(c_2424,plain,
! [X0: $i,X1: $i] :
( r(f(c),f(f(X0)))
| r(f(c),f(f(f(X1))))
| r(f(f(X0)),f(f(f(X1))))
| ( f(c) = f(f(X0)) )
| ( f(c) = f(f(f(X1))) )
| ( f(f(X0)) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_836]) ).
tcf(c_2426,plain,
( r(f(c),f(f(c)))
| r(f(c),f(f(f(c))))
| r(f(f(c)),f(f(f(c))))
| ( f(c) = f(f(c)) )
| ( f(c) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2424]) ).
tcf(c_2427,plain,
( r(f(f(c)),f(c))
| r(f(c),f(f(f(c))))
| r(f(f(c)),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2423]) ).
tcf(c_2446,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),X1)
| r(f(f(f(X0))),X1)
| r(f(f(c)),f(f(f(X0))))
| ( f(f(c)) = X1 )
| ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(X0))) = X1 ) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_2447,plain,
( r(f(f(c)),c)
| r(f(f(f(c))),c)
| r(f(f(c)),f(f(f(c))))
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(c))) = c ) ),
inference(instantiation,[status(thm)],[c_2446]) ).
tcf(c_2452,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_885]) ).
tcf(c_2454,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(X1))
| r(f(X1),f(f(f(X0))))
| r(f(f(c)),f(f(f(X0))))
| ( f(X1) = f(f(f(X0))) )
| ( f(f(c)) = f(X1) )
| ( f(f(c)) = f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_2593,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = X1 )
| ( X1 != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_1414]) ).
tcf(c_2594,plain,
( ( f(f(c)) = c )
| ( c != f(f(c)) )
| ( f(f(c)) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_2593]) ).
tcf(c_2651,plain,
! [X0: $i] :
( ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(f(X0)))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_2652,plain,
( ( f(f(f(c))) = f(f(c)) )
| ( f(f(f(f(c)))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2651]) ).
tcf(c_2653,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(X1) )
| ( f(f(f(X0))) != f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_2654,plain,
! [X0: $i] :
( ( f(c) = f(X0) )
| ( f(f(c)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_2660,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(f(X1)) )
| ( f(f(X0)) != f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_2661,plain,
( ( f(c) = f(f(c)) )
| ( f(f(c)) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2660]) ).
tcf(c_2771,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X0))) = X2 )
| ( X2 != X1 )
| ( f(f(f(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_1078]) ).
tcf(c_2809,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),f(f(c)))
| r(f(f(f(X0))),f(f(c)))
| r(f(f(f(X0))),f(f(f(X1))))
| ( f(f(f(X1))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_1849]) ).
tcf(c_2823,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X1)),X2)
| r(f(f(X0)),X2)
| r(f(f(X0)),f(f(X1)))
| ( f(f(X1)) = X2 )
| ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_2825,plain,
! [X0: $i,X1: $i] :
( r(c,f(f(X1)))
| r(c,f(f(X0)))
| r(f(f(X0)),f(f(X1)))
| ( c = f(f(X1)) )
| ( c = f(f(X0)) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1019]) ).
tcf(c_2827,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(f(X0)))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1453]) ).
tcf(c_2830,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),f(f(X1)))
| r(f(f(X0)),f(X2))
| r(f(f(X0)),f(f(X1)))
| ( f(X2) = f(f(X1)) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_2831,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X1)),f(X2))
| r(f(f(X0)),f(X2))
| r(f(f(X0)),f(f(X1)))
| ( f(f(X1)) = f(X2) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_2843,plain,
! [X0: $i] :
( r(c,f(c))
| r(c,f(f(f(X0))))
| r(f(c),f(f(f(X0))))
| ( c = f(c) )
| ( c = f(f(f(X0))) )
| ( f(c) = f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_1613]) ).
tcf(c_3007,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(f(X1)))
| r(f(f(X0)),X2)
| r(f(f(X0)),f(f(X1)))
| ( X2 = f(f(X1)) )
| ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_3049,plain,
! [X0: $i] :
( r(f(c),c)
| r(f(f(f(X0))),c)
| r(f(f(f(X0))),f(c))
| ( f(c) = c )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_1647]) ).
tcf(c_3171,plain,
! [X0: $i] :
( ( f(c) = f(f(f(X0))) )
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(X0))) )
| ~ r(f(f(c)),f(c))
| ~ r(f(c),f(f(f(X0))))
| ~ r(f(f(c)),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_1719]) ).
tcf(c_3172,plain,
( ( f(c) = f(f(f(c))) )
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(c))) )
| ~ r(f(f(c)),f(c))
| ~ r(f(c),f(f(f(c))))
| ~ r(f(f(c)),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_3171]) ).
tcf(c_3185,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(X1)))
| r(f(f(f(X0))),f(f(c)))
| r(f(f(f(X0))),f(f(X1)))
| ( f(f(c)) = f(f(X1)) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1757]) ).
tcf(c_3212,plain,
! [X0: $i] :
( ( c = f(f(f(X0))) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(X0))) )
| ~ r(f(f(c)),c)
| ~ r(c,f(f(f(X0))))
| ~ r(f(f(c)),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_1765]) ).
tcf(c_3213,plain,
( ( c = f(f(f(c))) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(c))) )
| ~ r(f(f(c)),c)
| ~ r(c,f(f(f(c))))
| ~ r(f(f(c)),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_3212]) ).
tcf(c_3287,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(f(X1)))
| r(X2,f(f(X0)))
| r(f(f(X0)),f(f(X1)))
| ( X2 = f(f(X1)) )
| ( X2 = f(f(X0)) )
| ( f(f(X0)) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1695]) ).
tcf(c_3389,plain,
! [X0: $i] :
( ( f(c) = f(f(c)) )
| ( f(c) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(c),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_2111]) ).
tcf(c_3546,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(c)) )
| ( f(X1) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(c)) )
| ~ r(f(X1),f(f(c)))
| ~ r(f(X1),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_2112]) ).
tcf(c_3565,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(c)) )
| ( f(X1) = f(f(f(X0))) )
| ( f(f(c)) = f(f(f(X0))) )
| ~ r(f(X1),f(f(c)))
| ~ r(f(X1),f(f(f(X0))))
| ~ r(f(f(c)),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_2112]) ).
tcf(c_3590,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(f(X0))) )
| ( f(f(c)) = f(X1) )
| ( f(f(c)) = f(f(f(X0))) )
| ~ r(f(f(c)),f(X1))
| ~ r(f(X1),f(f(f(X0))))
| ~ r(f(f(c)),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_2234]) ).
tcf(c_3801,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(X1)) )
| ( f(X2) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(X1)) )
| ~ r(f(X2),f(f(X1)))
| ~ r(f(X2),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_2112]) ).
tcf(c_3805,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(X1)) )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(X1)) )
| ~ r(c,f(f(X1)))
| ~ r(f(f(f(X0))),c)
| ~ r(f(f(f(X0))),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1765]) ).
tcf(c_3924,plain,
! [X0: $i] :
( ( f(c) = f(f(X0)) )
| ( f(f(c)) != f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_2654]) ).
tcf(c_4131,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(f(X1))) )
| ( f(f(f(X1))) = f(c) )
| ~ r(f(f(X0)),f(c))
| ~ r(f(f(f(X1))),f(c))
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_1040]) ).
tcf(c_4196,plain,
! [X0: $i] :
( ( f(f(X0)) = c )
| ( c != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_2593]) ).
tcf(c_4243,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X0))) = X2 )
| ( X2 != f(X1) )
| ( f(f(f(X0))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_2771]) ).
tcf(c_4276,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(f(X0))),c)
| r(f(f(f(X0))),f(f(c)))
| ( f(f(c)) = c )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_459]) ).
tcf(c_4281,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(X0)) = X2 )
| ( f(f(X0)) = f(f(f(X1))) )
| ( f(f(f(X1))) = X2 )
| ~ r(f(f(X0)),X2)
| ~ r(f(f(f(X1))),X2)
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_1099]) ).
tcf(c_4302,plain,
! [X0: $i] :
( ( c = f(f(X0)) )
| ( f(c) != f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_4303,plain,
( ( c = f(f(c)) )
| ( f(c) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_4302]) ).
tcf(c_4734,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(f(X0))),c)
| r(f(f(c)),f(f(f(X0))))
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(X0))) = c ) ),
inference(instantiation,[status(thm)],[c_1170]) ).
tcf(c_5164,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(X0)))
| r(f(f(c)),f(f(f(X1))))
| r(f(f(X0)),f(f(f(X1))))
| ( f(f(c)) = f(f(X0)) )
| ( f(f(c)) = f(f(f(X1))) )
| ( f(f(X0)) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_2454]) ).
tcf(c_5347,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),X0)
| ~ r(X0,f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_230]) ).
tcf(c_5455,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = c )
| ( f(f(X0)) = f(f(f(X1))) )
| ( f(f(f(X1))) = c )
| ~ r(f(f(X0)),c)
| ~ r(f(f(f(X1))),c)
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_2285]) ).
tcf(c_5482,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(f(X1)) )
| ( f(f(f(X0))) != f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_2653]) ).
tcf(c_5514,plain,
! [X0: $i] :
( r(c,f(f(f(c))))
| r(c,f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( c = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2825]) ).
tcf(c_5515,plain,
( r(c,f(f(f(c))))
| r(c,f(f(f(f(c)))))
| r(f(f(f(f(c)))),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( c = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5514]) ).
tcf(c_5665,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(c))),X1)
| r(f(f(f(f(X0)))),X1)
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(f(f(c))) = X1 )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2823]) ).
tcf(c_5666,plain,
( r(f(f(f(c))),c)
| r(f(f(f(f(c)))),c)
| r(f(f(f(f(c)))),f(f(f(c))))
| ( f(f(f(c))) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5665]) ).
tcf(c_5667,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X1)),X2)
| r(f(f(f(X0))),X2)
| r(f(f(f(X0))),f(f(X1)))
| ( f(f(X1)) = X2 )
| ( f(f(f(X0))) = X2 )
| ( f(f(f(X0))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_2823]) ).
tcf(c_5677,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X2)),X1)
| r(f(f(f(X0))),X1)
| r(f(f(X2)),f(f(f(X0))))
| ( f(f(X2)) = X1 )
| ( f(f(X2)) = f(f(f(X0))) )
| ( f(f(f(X0))) = X1 ) ),
inference(instantiation,[status(thm)],[c_2823]) ).
tcf(c_5736,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(f(c))))
| r(f(f(f(f(X0)))),f(X1))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(X1) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(X1) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2830]) ).
tcf(c_5737,plain,
( r(f(c),f(f(f(c))))
| r(f(f(f(f(c)))),f(c))
| r(f(f(f(f(c)))),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_5748,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X0)),f(X2))
| r(f(X2),f(f(f(X1))))
| r(f(f(X0)),f(f(f(X1))))
| ( f(X2) = f(f(f(X1))) )
| ( f(f(X0)) = f(X2) )
| ( f(f(X0)) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_2830]) ).
tcf(c_5774,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X1)),f(X2))
| r(f(f(f(X0))),f(X2))
| r(f(f(f(X0))),f(f(X1)))
| ( f(f(X1)) = f(X2) )
| ( f(f(f(X0))) = f(X2) )
| ( f(f(f(X0))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_2831]) ).
tcf(c_5814,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(f(X1))))
| r(f(f(f(X0))),f(f(c)))
| r(f(f(f(X0))),f(f(f(X1))))
| ( f(f(c)) = f(f(f(X1))) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_3185]) ).
tcf(c_6016,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(f(c)) )
| ( f(f(X0)) = f(f(f(X1))) )
| ( f(f(f(X1))) = f(f(c)) )
| ~ r(f(f(X0)),f(f(c)))
| ~ r(f(f(f(X1))),f(f(c)))
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_3546]) ).
tcf(c_6056,plain,
! [X0: $i,X1: $i] :
( r(X1,f(f(f(c))))
| r(f(f(f(f(X0)))),X1)
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( X1 = f(f(f(c))) )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_3007]) ).
tcf(c_6057,plain,
( r(c,f(f(f(c))))
| r(f(f(f(f(c)))),c)
| r(f(f(f(f(c)))),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_6056]) ).
tcf(c_6067,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),X1)
| r(X1,f(f(f(X0))))
| r(f(f(c)),f(f(f(X0))))
| ( X1 = f(f(f(X0))) )
| ( f(f(c)) = X1 )
| ( f(f(c)) = f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_3007]) ).
tcf(c_6068,plain,
( r(f(f(c)),c)
| r(c,f(f(f(c))))
| r(f(f(c)),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_6067]) ).
tcf(c_6093,plain,
! [X0: $i,X1: $i] :
( r(X1,f(f(f(c))))
| r(X1,f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( X1 = f(f(f(c))) )
| ( X1 = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_3287]) ).
tcf(c_6115,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(f(X1))) )
| ( f(f(X0)) = f(f(c)) )
| ( f(f(X0)) = f(f(f(X1))) )
| ~ r(f(f(X0)),f(f(c)))
| ~ r(f(f(c)),f(f(f(X1))))
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_3565]) ).
tcf(c_6173,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(X0)) )
| ( f(f(c)) = f(f(f(X1))) )
| ( f(f(X0)) = f(f(f(X1))) )
| ~ r(f(f(c)),f(f(X0)))
| ~ r(f(f(c)),f(f(f(X1))))
| ~ r(f(f(X0)),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_3590]) ).
tcf(c_6551,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),f(X0))
| ~ r(f(X0),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_5347]) ).
tcf(c_6602,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_5482]) ).
tcf(c_6603,plain,
( ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(f(c))))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_6602]) ).
tcf(c_6604,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = f(f(X1)) )
| ( f(f(f(f(X0)))) != f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_5482]) ).
tcf(c_6613,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(c))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_5482]) ).
tcf(c_6614,plain,
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(c))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_6613]) ).
tcf(c_6934,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = X1 )
| ( X1 != f(f(f(X0))) )
| ( f(f(f(X0))) != f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_4243]) ).
tcf(c_6935,plain,
( ( f(f(f(c))) = c )
| ( c != f(f(f(c))) )
| ( f(f(f(c))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_6934]) ).
tcf(c_7534,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(c)) != f(f(c)) )
| ( f(f(f(f(X0)))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_2370]) ).
tcf(c_7535,plain,
! [X0: $i] :
( ( f(f(f(X0))) = f(c) )
| ( f(f(f(f(X0)))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_7537,plain,
( ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(c)) != f(f(c)) )
| ( f(f(f(f(c)))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_7534]) ).
tcf(c_7671,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(f(X1))))
| r(f(f(c)),f(f(f(X0))))
| r(f(f(f(X0))),f(f(f(X1))))
| ( f(f(c)) = f(f(f(X1))) )
| ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_5164]) ).
tcf(c_7742,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(f(X1))) )
| ( f(X2) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(X2),f(f(f(X1))))
| ~ r(f(X2),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_3801]) ).
tcf(c_7751,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(X0)))) )
| ( f(c) != f(c) )
| ( f(f(f(f(X0)))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_707]) ).
tcf(c_7752,plain,
! [X0: $i] :
( ( f(f(f(X0))) = c )
| ( f(f(f(f(X0)))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_7753,plain,
( ( f(f(f(c))) = c )
| ( f(f(f(f(c)))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_7752]) ).
tcf(c_7928,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(f(X1))) )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(c,f(f(f(X1))))
| ~ r(f(f(f(X0))),c)
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_3805]) ).
tcf(c_8172,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X1))) = c )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),c)
| ~ r(f(f(f(X0))),c)
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_5455]) ).
tcf(c_8220,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X1))) = X2 )
| ( f(f(f(X0))) = X2 )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),X2)
| ~ r(f(f(f(X0))),X2)
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_4281]) ).
tcf(c_8371,plain,
! [X0: $i] :
( r(f(c),f(f(f(c))))
| r(f(f(f(f(X0)))),f(c))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_8376,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(c))))
| r(f(f(f(f(X0)))),f(f(c)))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_8377,plain,
( r(f(f(c)),f(f(f(c))))
| r(f(f(f(f(c)))),f(f(c)))
| r(f(f(f(f(c)))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_8376]) ).
tcf(c_8383,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(f(X0)))) = X2 )
| ( X2 != f(X1) )
| ( f(f(f(f(X0)))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_1414]) ).
tcf(c_8388,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X0)))) = f(c) )
| ( f(c) != f(X1) )
| ( f(f(f(f(X0)))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_327]) ).
tcf(c_8389,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = X1 )
| ( f(f(f(f(X0)))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_8613,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),c)
| r(f(f(f(X0))),c)
| r(f(f(f(X0))),f(f(X1)))
| ( f(f(X1)) = c )
| ( f(f(f(X0))) = c )
| ( f(f(f(X0))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_5667]) ).
tcf(c_8682,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X1))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),f(f(c)))
| ~ r(f(f(f(X0))),f(f(c)))
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_6016]) ).
tcf(c_8789,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(f(c))))
| r(f(X1),f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(X1) = f(f(f(c))) )
| ( f(X1) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_6093]) ).
tcf(c_8790,plain,
( r(f(c),f(f(f(c))))
| r(f(c),f(f(f(f(c)))))
| r(f(f(f(f(c)))),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(c) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_8789]) ).
tcf(c_8871,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(f(X1))) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(f(c)),f(f(f(X1))))
| ~ r(f(f(f(X0))),f(f(c)))
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_6115]) ).
tcf(c_9032,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(f(X1))) )
| ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(X0))) = f(f(f(X1))) )
| ~ r(f(f(c)),f(f(f(X1))))
| ~ r(f(f(c)),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_6173]) ).
tcf(c_9138,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),c)
| r(f(f(f(X0))),c)
| r(f(f(X1)),f(f(f(X0))))
| ( f(f(X1)) = c )
| ( f(f(X1)) = f(f(f(X0))) )
| ( f(f(f(X0))) = c ) ),
inference(instantiation,[status(thm)],[c_5677]) ).
tcf(c_9390,plain,
! [X0: $i] :
( ( f(f(f(X0))) = f(f(f(X0))) )
| ( f(f(f(f(X0)))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_6604]) ).
tcf(c_9391,plain,
( ( f(f(f(c))) = f(f(f(c))) )
| ( f(f(f(f(c)))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_9390]) ).
tcf(c_9834,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = f(c) )
| ( f(c) != f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_8388]) ).
tcf(c_9835,plain,
( ( f(f(f(f(c)))) = f(c) )
| ( f(c) != f(f(f(f(c)))) )
| ( f(f(f(f(c)))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_9834]) ).
tcf(c_10067,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(f(f(f(X0))),X2)
| r(f(f(f(X0))),f(X1))
| ( X2 = f(X1) )
| ( f(f(f(X0))) = X2 )
| ( f(f(f(X0))) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_10077,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(f(X1))),f(X2))
| r(f(f(f(X0))),f(X2))
| r(f(f(f(X0))),f(f(f(X1))))
| ( f(f(f(X1))) = f(X2) )
| ( f(f(f(X0))) = f(X2) )
| ( f(f(f(X0))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_5774]) ).
tcf(c_10080,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),f(f(f(X1))))
| r(f(f(f(X0))),f(X2))
| r(f(f(f(X0))),f(f(f(X1))))
| ( f(X2) = f(f(f(X1))) )
| ( f(f(f(X0))) = f(X2) )
| ( f(f(f(X0))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_5748]) ).
tcf(c_10170,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X0))),f(f(c)))
| r(f(f(c)),f(f(f(f(X1)))))
| r(f(f(f(X0))),f(f(f(f(X1)))))
| ( f(f(c)) = f(f(f(f(X1)))) )
| ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(X0))) = f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_5814]) ).
tcf(c_10171,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),f(f(c)))
| r(f(f(f(f(X0)))),f(f(c)))
| r(f(f(f(X1))),f(f(f(f(X0)))))
| ( f(f(f(X1))) = f(f(c)) )
| ( f(f(f(X1))) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_2809]) ).
tcf(c_10800,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X0)))) = X1 )
| ( X1 != f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_8383]) ).
tcf(c_10801,plain,
( ( f(f(f(f(c)))) = c )
| ( c != f(f(f(f(c)))) )
| ( f(f(f(f(c)))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_10800]) ).
tcf(c_10936,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(X1) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(X1),f(f(f(c))))
| ~ r(f(f(f(f(X0)))),f(X1))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_1720]) ).
tcf(c_10937,plain,
( ( f(c) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(f(f(f(c)))),f(c))
| ~ r(f(f(f(f(c)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_10936]) ).
tcf(c_11016,plain,
! [X0: $i] :
( ( f(c) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(f(f(f(X0)))),f(c))
| ~ r(f(f(f(f(X0)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_1080]) ).
tcf(c_11020,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(f(X0)) = f(f(f(f(X1)))) )
| ( f(f(f(f(X1)))) = f(c) )
| ~ r(f(f(X0)),f(c))
| ~ r(f(f(f(f(X1)))),f(c))
| ~ r(f(f(X0)),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_4131]) ).
tcf(c_11021,plain,
( ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(c) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(f(c)))),f(c))
| ~ r(f(f(c)),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_11020]) ).
tcf(c_11167,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(c))) = X1 )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(f(c))),X1)
| ~ r(f(f(f(f(X0)))),X1)
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_8220]) ).
tcf(c_11168,plain,
( ( f(f(f(c))) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ~ r(f(f(f(c))),c)
| ~ r(f(f(f(f(c)))),c)
| ~ r(f(f(f(f(c)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11167]) ).
tcf(c_11204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X1))) = X2 )
| ( f(f(f(f(X0)))) = X2 )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),X2)
| ~ r(f(f(f(f(X0)))),X2)
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_8220]) ).
tcf(c_11536,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(f(c))) )
| ( f(X1) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(X1),f(f(f(c))))
| ~ r(f(X1),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_7742]) ).
tcf(c_11573,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(f(X1))) )
| ( f(X2) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(X2),f(f(f(X1))))
| ~ r(f(X2),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_7742]) ).
tcf(c_11656,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(c))))
| r(f(f(c)),f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_7671]) ).
tcf(c_11657,plain,
( r(f(f(c)),f(f(f(c))))
| r(f(f(c)),f(f(f(f(c)))))
| r(f(f(f(f(c)))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_11656]) ).
tcf(c_11693,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(f(X1))))
| r(f(f(c)),f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(X1))))
| ( f(f(c)) = f(f(f(X1))) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_7671]) ).
tcf(c_11721,plain,
! [X0: $i] :
( ( c = f(f(f(c))) )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(c,f(f(f(c))))
| ~ r(f(f(f(f(X0)))),c)
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_7928]) ).
tcf(c_11722,plain,
( ( c = f(f(f(c))) )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ~ r(c,f(f(f(c))))
| ~ r(f(f(f(f(c)))),c)
| ~ r(f(f(f(f(c)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11721]) ).
tcf(c_11758,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(f(X1))) )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(c,f(f(f(X1))))
| ~ r(f(f(f(f(X0)))),c)
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_7928]) ).
tcf(c_11797,plain,
! [X0: $i] :
( ( f(f(f(c))) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(f(c))),c)
| ~ r(f(f(f(f(X0)))),c)
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_8172]) ).
tcf(c_11832,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X1))) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),c)
| ~ r(f(f(f(f(X0)))),c)
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_8172]) ).
tcf(c_12172,plain,
! [X0: $i] :
( ( f(f(f(c))) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(f(c))),f(f(c)))
| ~ r(f(f(f(f(X0)))),f(f(c)))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_8682]) ).
tcf(c_12274,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(f(f(X0)))),f(f(c)))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_8871]) ).
tcf(c_12275,plain,
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(f(f(c)))),f(f(c)))
| ~ r(f(f(f(f(c)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_12274]) ).
tcf(c_12421,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(c)),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_9032]) ).
tcf(c_12422,plain,
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(c)),f(f(f(f(c)))))
| ~ r(f(f(f(f(c)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_12421]) ).
tcf(c_12458,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(f(X1))) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(f(c)),f(f(f(X1))))
| ~ r(f(f(c)),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_9032]) ).
tcf(c_13202,plain,
! [X0: $i] : f(f(f(f(X0)))) = f(f(f(f(X0)))),
inference(instantiation,[status(thm)],[c_234]) ).
tcf(c_13203,plain,
f(f(f(f(c)))) = f(f(f(f(c)))),
inference(instantiation,[status(thm)],[c_13202]) ).
tcf(c_13367,plain,
! [X0: $i] :
( ( f(c) = f(f(c)) )
| ( f(c) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(c),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_3389]) ).
tcf(c_13368,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(X0)))) )
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ~ r(f(f(c)),f(c))
| ~ r(f(c),f(f(f(f(X0)))))
| ~ r(f(f(c)),f(f(f(f(X0))))) ),
inference(instantiation,[status(thm)],[c_3171]) ).
tcf(c_13372,plain,
( ( f(c) = f(f(c)) )
| ( f(c) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(c),f(f(f(f(c)))))
| ~ r(f(f(f(f(c)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_13367]) ).
tcf(c_14450,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = c )
| ( c != f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_10800]) ).
tcf(c_14699,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(f(f(X1))) )
| ( f(f(X0)) != f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_2660]) ).
tcf(c_14700,plain,
( ( f(c) = f(f(f(c))) )
| ( f(f(c)) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_14699]) ).
tcf(c_14794,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_2452]) ).
tcf(c_14795,plain,
! [X0: $i] :
( ( f(f(c)) = f(c) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(f(X0)))),f(c))
| ~ r(f(f(f(f(X0)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_1872]) ).
tcf(c_14798,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = X1 )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ~ r(f(f(c)),X1)
| ~ r(f(f(f(f(X0)))),X1)
| ~ r(f(f(f(f(X0)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_1097]) ).
tcf(c_14799,plain,
( ( f(f(c)) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(c)) )
| ~ r(f(f(c)),c)
| ~ r(f(f(f(f(c)))),c)
| ~ r(f(f(f(f(c)))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_14798]) ).
tcf(c_15230,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(f(X1))),f(X2))
| r(f(f(f(f(X0)))),f(X2))
| r(f(f(f(f(X0)))),f(f(f(X1))))
| ( f(f(f(X1))) = f(X2) )
| ( f(f(f(f(X0)))) = f(X2) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_10077]) ).
tcf(c_15400,plain,
! [X0: $i] :
( r(c,f(c))
| r(c,f(f(f(f(X0)))))
| r(f(c),f(f(f(f(X0)))))
| ( c = f(c) )
| ( c = f(f(f(f(X0)))) )
| ( f(c) = f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_2843]) ).
tcf(c_15402,plain,
! [X0: $i] :
( r(c,f(f(c)))
| r(c,f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(c)))
| ( c = f(f(c)) )
| ( c = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_1845]) ).
tcf(c_15405,plain,
( r(c,f(f(c)))
| r(c,f(f(f(f(c)))))
| r(f(f(f(f(c)))),f(f(c)))
| ( c = f(f(c)) )
| ( c = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_15402]) ).
tcf(c_15407,plain,
( r(c,f(c))
| r(c,f(f(f(f(c)))))
| r(f(c),f(f(f(f(c)))))
| ( c = f(c) )
| ( c = f(f(f(f(c)))) )
| ( f(c) = f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_15400]) ).
tcf(c_15908,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),f(f(f(X1))))
| r(f(f(f(f(X0)))),f(X2))
| r(f(f(f(f(X0)))),f(f(f(X1))))
| ( f(X2) = f(f(f(X1))) )
| ( f(f(f(f(X0)))) = f(X2) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_10080]) ).
tcf(c_16091,plain,
! [X0: $i] : f(f(f(f(X0)))) != c,
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_16092,plain,
f(f(f(f(c)))) != c,
inference(instantiation,[status(thm)],[c_16091]) ).
tcf(c_16424,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(X1)))),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_2827]) ).
tcf(c_16444,plain,
! [X0: $i] :
( ( f(c) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(f(f(f(X0)))),f(c))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_10936]) ).
tcf(c_17244,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(f(f(X1)))))
| r(f(f(f(f(X0)))),f(f(c)))
| r(f(f(f(f(X0)))),f(f(f(f(X1)))))
| ( f(f(c)) = f(f(f(f(X1)))) )
| ( f(f(f(f(X0)))) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_10170]) ).
tcf(c_17344,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X1))) = f(c) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),f(c))
| ~ r(f(f(f(f(X0)))),f(c))
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_11204]) ).
tcf(c_17722,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = f(f(f(c))) )
| ( f(f(f(X0))) = f(f(f(f(X1)))) )
| ( f(f(f(f(X1)))) = f(f(f(c))) )
| ~ r(f(f(f(X0))),f(f(f(c))))
| ~ r(f(f(f(f(X1)))),f(f(f(c))))
| ~ r(f(f(f(X0))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_11536]) ).
tcf(c_17724,plain,
! [X0: $i,X1: $i] :
( ( f(f(X1)) = f(f(f(c))) )
| ( f(f(X1)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(f(X1)),f(f(f(c))))
| ~ r(f(f(X1)),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11536]) ).
tcf(c_17726,plain,
! [X0: $i] :
( ( f(c) = f(f(f(c))) )
| ( f(c) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(c),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11536]) ).
tcf(c_17834,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X2))) = f(f(f(X1))) )
| ( f(f(f(X2))) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(X1))) )
| ~ r(f(f(f(X2))),f(f(f(X1))))
| ~ r(f(f(f(X2))),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_11573]) ).
tcf(c_18128,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),f(f(f(f(X1)))))
| r(f(f(c)),f(f(f(f(X0)))))
| r(f(f(f(f(X0)))),f(f(f(f(X1)))))
| ( f(f(c)) = f(f(f(f(X1)))) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_11693]) ).
tcf(c_20837,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(X1)),f(f(f(f(X0)))))
| ( f(f(X1)) = c )
| ( f(f(X1)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = c ) ),
inference(instantiation,[status(thm)],[c_9138]) ).
tcf(c_20839,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(f(f(X0)))),f(f(X1)))
| ( f(f(X1)) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_8613]) ).
tcf(c_20841,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(c)),f(f(f(f(X0)))))
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = c ) ),
inference(instantiation,[status(thm)],[c_4734]) ).
tcf(c_20842,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(f(f(X0)))),f(f(c)))
| ( f(f(c)) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_4276]) ).
tcf(c_20844,plain,
! [X0: $i] :
( r(f(c),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(f(f(X0)))),f(c))
| ( f(c) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_3049]) ).
tcf(c_20849,plain,
( r(f(c),c)
| r(f(f(f(f(c)))),c)
| r(f(f(f(f(c)))),f(c))
| ( f(c) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_20844]) ).
tcf(c_20851,plain,
( r(f(f(c)),c)
| r(f(f(f(f(c)))),c)
| r(f(f(f(f(c)))),f(f(c)))
| ( f(f(c)) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_20842]) ).
tcf(c_21533,plain,
! [X0: $i] :
( ( f(c) = f(f(f(X0))) )
| ( f(f(c)) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_14699]) ).
tcf(c_24332,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(f(f(X1)))),f(X2))
| r(f(f(f(f(X0)))),f(X2))
| r(f(f(f(f(X0)))),f(f(f(f(X1)))))
| ( f(f(f(f(X1)))) = f(X2) )
| ( f(f(f(f(X0)))) = f(X2) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_15230]) ).
tcf(c_24364,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(X2),f(f(f(f(X1)))))
| r(f(f(f(f(X0)))),f(X2))
| r(f(f(f(f(X0)))),f(f(f(f(X1)))))
| ( f(X2) = f(f(f(f(X1)))) )
| ( f(f(f(f(X0)))) = f(X2) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_15908]) ).
tcf(c_24616,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(X1)))),f(f(c)))
| r(f(f(f(f(X0)))),f(f(c)))
| r(f(f(f(f(X1)))),f(f(f(f(X0)))))
| ( f(f(f(f(X1)))) = f(f(c)) )
| ( f(f(f(f(X1)))) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_10171]) ).
tcf(c_24945,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(f(f(X2)),X1)
| r(f(f(f(f(X0)))),X1)
| r(f(f(X2)),f(f(f(f(X0)))))
| ( f(f(X2)) = X1 )
| ( f(f(X2)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = X1 ) ),
inference(instantiation,[status(thm)],[c_5677]) ).
tcf(c_24948,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),X1)
| r(f(f(f(f(X0)))),X1)
| r(f(f(c)),f(f(f(f(X0)))))
| ( f(f(c)) = X1 )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = X1 ) ),
inference(instantiation,[status(thm)],[c_2446]) ).
tcf(c_24950,plain,
! [X0: $i,X1: $i] :
( r(X1,f(f(c)))
| r(f(f(f(f(X0)))),X1)
| r(f(f(f(f(X0)))),f(f(c)))
| ( X1 = f(f(c)) )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_1594]) ).
tcf(c_24951,plain,
! [X0: $i,X1: $i] :
( r(f(f(c)),X1)
| r(f(f(f(f(X0)))),X1)
| r(f(f(f(f(X0)))),f(f(c)))
| ( f(f(c)) = X1 )
| ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_459]) ).
tcf(c_24972,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(X1))
| r(f(f(f(f(X0)))),X2)
| r(f(f(f(f(X0)))),f(X1))
| ( X2 = f(X1) )
| ( f(f(f(f(X0)))) = X2 )
| ( f(f(f(f(X0)))) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_10067]) ).
tcf(c_26141,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(X1)))),f(X0))
| ~ r(f(X0),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_6551]) ).
tcf(c_26159,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X2) = f(f(f(f(X1)))) )
| ( f(X2) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) )
| ~ r(f(X2),f(f(f(f(X1)))))
| ~ r(f(X2),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_11573]) ).
tcf(c_26277,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = f(f(f(X1))) )
| ( f(f(f(f(X0)))) != f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_6604]) ).
tcf(c_26278,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(f(c)))))
| r(f(f(f(f(f(X0))))),f(f(c)))
| r(f(f(f(f(f(X0))))),f(f(f(f(c)))))
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_17244]) ).
tcf(c_26279,plain,
( r(f(f(c)),f(f(f(f(c)))))
| r(f(f(f(f(f(c))))),f(f(c)))
| r(f(f(f(f(f(c))))),f(f(f(f(c)))))
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(f(c))))) = f(f(c)) )
| ( f(f(f(f(f(c))))) = f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_26278]) ).
tcf(c_26483,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X1)))) = f(c) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) )
| ~ r(f(f(f(f(X1)))),f(c))
| ~ r(f(f(f(f(X0)))),f(c))
| ~ r(f(f(f(f(X0)))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_17344]) ).
tcf(c_26617,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X1)))) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(f(f(c))) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) )
| ~ r(f(f(f(f(X1)))),f(f(f(c))))
| ~ r(f(f(f(f(X0)))),f(f(f(c))))
| ~ r(f(f(f(f(X0)))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_17722]) ).
tcf(c_26812,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(f(X1)))) = f(f(f(X2))) )
| ( f(f(f(f(X0)))) = f(f(f(X2))) )
| ( f(f(f(f(X0)))) = f(f(f(f(X1)))) )
| ~ r(f(f(f(f(X1)))),f(f(f(X2))))
| ~ r(f(f(f(f(X0)))),f(f(f(X2))))
| ~ r(f(f(f(f(X0)))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_17834]) ).
tcf(c_30719,plain,
! [X0: $i] :
( ( f(f(f(c))) = f(f(f(f(X0)))) )
| ( f(f(f(f(c)))) != f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_26277]) ).
tcf(c_30720,plain,
( ( f(f(f(c))) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) != f(f(f(f(f(c))))) ) ),
inference(instantiation,[status(thm)],[c_30719]) ).
tcf(c_31551,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(X1)))),c)
| r(f(f(f(f(X0)))),c)
| r(f(f(f(f(X1)))),f(f(f(f(X0)))))
| ( f(f(f(f(X1)))) = c )
| ( f(f(f(f(X1)))) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = c ) ),
inference(instantiation,[status(thm)],[c_20837]) ).
tcf(c_32776,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(f(X0))))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_7535]) ).
tcf(c_32778,plain,
( ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(f(c))))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_32776]) ).
tcf(c_32869,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(X0)))) )
| ( f(f(c)) != f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_3924]) ).
tcf(c_32872,plain,
( ( f(c) = f(f(f(f(c)))) )
| ( f(f(c)) != f(f(f(f(f(c))))) ) ),
inference(instantiation,[status(thm)],[c_32869]) ).
tcf(c_33271,plain,
! [X0: $i] :
( r(f(f(c)),f(c))
| r(f(f(f(f(X0)))),f(c))
| r(f(f(c)),f(f(f(f(X0)))))
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_24948]) ).
tcf(c_33272,plain,
( r(f(f(c)),f(c))
| r(f(f(f(f(c)))),f(c))
| r(f(f(c)),f(f(f(f(c)))))
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_33271]) ).
tcf(c_33362,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(f(c)))
| r(f(f(f(f(f(X0))))),f(f(c)))
| r(f(f(f(f(f(X0))))),f(f(f(f(c)))))
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_24616]) ).
tcf(c_33586,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(c)))
| r(f(f(f(f(X0)))),f(X1))
| r(f(f(f(f(X0)))),f(f(c)))
| ( f(X1) = f(f(c)) )
| ( f(f(f(f(X0)))) = f(X1) )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_24950]) ).
tcf(c_33587,plain,
( r(f(c),f(f(c)))
| r(f(f(f(f(c)))),f(c))
| r(f(f(f(f(c)))),f(f(c)))
| ( f(c) = f(f(c)) )
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_33586]) ).
tcf(c_33626,plain,
! [X0: $i] :
( r(f(f(c)),f(c))
| r(f(f(f(f(X0)))),f(c))
| r(f(f(f(f(X0)))),f(f(c)))
| ( f(f(c)) = f(c) )
| ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(X0)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_24951]) ).
tcf(c_33627,plain,
( r(f(f(c)),f(c))
| r(f(f(f(f(c)))),f(c))
| r(f(f(f(f(c)))),f(f(c)))
| ( f(f(c)) = f(c) )
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_33626]) ).
tcf(c_33842,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(f(f(X1))))
| r(f(f(f(f(X0)))),X2)
| r(f(f(f(f(X0)))),f(f(f(X1))))
| ( X2 = f(f(f(X1))) )
| ( f(f(f(f(X0)))) = X2 )
| ( f(f(f(f(X0)))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_24972]) ).
tcf(c_34538,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = f(f(f(f(c)))) )
| ( f(X1) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) )
| ~ r(f(X1),f(f(f(f(c)))))
| ~ r(f(X1),f(f(f(f(f(X0))))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_26159]) ).
tcf(c_35045,plain,
! [X0: $i] :
( ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) )
| ~ r(f(f(f(f(c)))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_26483]) ).
tcf(c_35156,plain,
! [X0: $i] :
( ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) )
| ~ r(f(f(f(f(c)))),f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_26617]) ).
tcf(c_36094,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(c))
| r(f(f(f(f(X0)))),f(c))
| r(f(f(X1)),f(f(f(f(X0)))))
| ( f(f(X1)) = f(c) )
| ( f(f(X1)) = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_24945]) ).
tcf(c_37393,plain,
! [X0: $i] :
( ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(f(f(f(c)))),f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c))))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_26617]) ).
tcf(c_37394,plain,
! [X0: $i] :
( ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ~ r(f(f(f(f(c)))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_26483]) ).
tcf(c_37396,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(c)))) = f(f(f(X1))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(X1))) )
| ~ r(f(f(f(f(c)))),f(f(f(X1))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(X1))))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_26812]) ).
tcf(c_37402,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(c)))),f(X1))
| r(f(X1),f(f(f(f(f(X0))))))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(X1) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(c)))) = f(X1) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_24364]) ).
tcf(c_37403,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(c)))),f(X1))
| r(f(f(f(f(f(X0))))),f(X1))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(f(f(c)))) = f(X1) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(X1) ) ),
inference(instantiation,[status(thm)],[c_24332]) ).
tcf(c_37405,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(f(c)))))
| r(f(f(c)),f(f(f(f(f(X0))))))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_18128]) ).
tcf(c_37406,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(f(c)))
| r(f(f(c)),f(f(f(f(f(X0))))))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_17244]) ).
tcf(c_37407,plain,
( r(f(f(f(f(c)))),f(f(c)))
| r(f(f(c)),f(f(f(f(f(c))))))
| r(f(f(f(f(c)))),f(f(f(f(f(c))))))
| ( f(f(c)) = f(f(f(f(f(c))))) )
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(c)))) = f(f(f(f(f(c))))) ) ),
inference(instantiation,[status(thm)],[c_37406]) ).
tcf(c_37416,plain,
( ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(c))))) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) )
| ~ r(f(f(f(f(c)))),f(f(f(c))))
| ~ r(f(f(f(f(f(c))))),f(f(f(c))))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(c)))))) ),
inference(instantiation,[status(thm)],[c_37396]) ).
tcf(c_37422,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(f(c)))
| r(f(f(f(f(f(X0))))),f(f(c)))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_24616]) ).
tcf(c_40458,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),c)
| r(f(f(f(f(f(X0))))),c)
| r(f(f(f(f(f(X0))))),f(f(f(f(c)))))
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_31551]) ).
tcf(c_40501,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),c)
| r(f(f(f(f(f(X0))))),c)
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = c ) ),
inference(instantiation,[status(thm)],[c_31551]) ).
tcf(c_41656,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X1))) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(X1))) )
| ~ r(f(f(f(X1))),c)
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_11832]) ).
tcf(c_41657,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(f(X1))) )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(X1))) )
| ~ r(c,f(f(f(X1))))
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_11758]) ).
tcf(c_41659,plain,
! [X0: $i] :
( ( f(f(f(c))) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(f(f(c))),c)
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11797]) ).
tcf(c_41660,plain,
! [X0: $i] :
( ( c = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(c,f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_11721]) ).
tcf(c_41664,plain,
( ( f(f(f(c))) = c )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(f(f(c))) )
| ~ r(f(f(f(c))),c)
| ~ r(f(f(f(f(f(c))))),c)
| ~ r(f(f(f(f(f(c))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_41659]) ).
tcf(c_41720,plain,
! [X0: $i] :
( r(f(c),c)
| r(f(f(f(f(f(X0))))),c)
| r(f(f(f(f(f(X0))))),f(c))
| ( f(c) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_20844]) ).
tcf(c_41728,plain,
( r(f(c),c)
| r(f(f(f(f(f(c))))),c)
| r(f(f(f(f(f(c))))),f(c))
| ( f(c) = c )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_41720]) ).
tcf(c_41939,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2651]) ).
tcf(c_41940,plain,
( ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(f(c))))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_41939]) ).
tcf(c_42172,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(c))))
| r(f(f(c)),f(f(f(f(f(X0))))))
| r(f(f(f(f(f(X0))))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_11656]) ).
tcf(c_42173,plain,
! [X0: $i] :
( r(f(c),f(f(f(c))))
| r(f(f(f(f(f(X0))))),f(c))
| r(f(f(f(f(f(X0))))),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_8371]) ).
tcf(c_42179,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(c))))
| r(f(f(f(f(f(X0))))),f(f(c)))
| r(f(f(f(f(f(X0))))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_8376]) ).
tcf(c_42180,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(f(c))))
| r(f(f(f(f(f(X0))))),f(X1))
| r(f(f(f(f(f(X0))))),f(f(f(c))))
| ( f(X1) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(X1) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_42185,plain,
( r(f(c),f(f(f(c))))
| r(f(f(f(f(f(c))))),f(c))
| r(f(f(f(f(f(c))))),f(f(f(c))))
| ( f(c) = f(f(f(c))) )
| ( f(f(f(f(f(c))))) = f(c) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_42180]) ).
tcf(c_42189,plain,
( r(f(f(c)),f(f(f(c))))
| r(f(f(c)),f(f(f(f(f(c))))))
| r(f(f(f(f(f(c))))),f(f(f(c))))
| ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(f(c))))) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_42172]) ).
tcf(c_42326,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(f(X1))))),f(X0))
| ~ r(f(X0),f(f(f(f(f(X1)))))) ),
inference(instantiation,[status(thm)],[c_26141]) ).
tcf(c_42911,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(f(c)))) )
| ~ r(f(f(c)),f(f(f(f(c)))))
| ~ r(f(f(c)),f(f(f(f(f(X0))))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_34538]) ).
tcf(c_43055,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(f(X1))))),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(f(f(f(X1)))))) ),
inference(instantiation,[status(thm)],[c_16424]) ).
tcf(c_43752,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(c))
| r(f(f(f(f(f(X0))))),f(c))
| r(f(f(X1)),f(f(f(f(f(X0))))))
| ( f(f(X1)) = f(c) )
| ( f(f(X1)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_36094]) ).
tcf(c_43753,plain,
( r(f(f(c)),f(c))
| r(f(f(f(f(f(c))))),f(c))
| r(f(f(c)),f(f(f(f(f(c))))))
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(f(c))))) )
| ( f(f(f(f(f(c))))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_43752]) ).
tcf(c_44018,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(X2,f(f(f(X1))))
| r(f(f(f(f(f(X0))))),X2)
| r(f(f(f(f(f(X0))))),f(f(f(X1))))
| ( X2 = f(f(f(X1))) )
| ( f(f(f(f(f(X0))))) = X2 )
| ( f(f(f(f(f(X0))))) = f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_33842]) ).
tcf(c_44019,plain,
( r(c,f(f(f(c))))
| r(f(f(f(f(f(c))))),c)
| r(f(f(f(f(f(c))))),f(f(f(c))))
| ( c = f(f(f(c))) )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_44018]) ).
tcf(c_46131,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(f(X0))))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_8389]) ).
tcf(c_46135,plain,
( ( f(f(f(f(c)))) = c )
| ( f(f(f(f(f(c))))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_46131]) ).
tcf(c_46512,plain,
! [X0: $i] :
( r(f(f(f(f(f(X0))))),f(f(c)))
| ~ r(f(f(c)),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_42326]) ).
tcf(c_46710,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(f(f(X1))))),f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(f(f(f(f(X1)))))) ),
inference(instantiation,[status(thm)],[c_43055]) ).
tcf(c_46711,plain,
( r(f(f(f(f(f(c))))),f(f(f(f(c)))))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(c)))))) ),
inference(instantiation,[status(thm)],[c_46710]) ).
tcf(c_47016,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(c))
| r(f(c),f(f(f(f(f(X0))))))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(c) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_37402]) ).
tcf(c_47081,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(c))
| r(f(f(f(f(f(X0))))),f(c))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(c) ) ),
inference(instantiation,[status(thm)],[c_37403]) ).
tcf(c_47099,plain,
! [X0: $i] :
( r(f(f(f(f(c)))),f(f(f(c))))
| r(f(f(f(f(f(X0))))),f(f(f(c))))
| r(f(f(f(f(c)))),f(f(f(f(f(X0))))))
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_37403]) ).
tcf(c_47100,plain,
( r(f(f(f(f(c)))),f(f(f(c))))
| r(f(f(f(f(f(c))))),f(f(f(c))))
| r(f(f(f(f(c)))),f(f(f(f(f(c))))))
| ( f(f(f(f(c)))) = f(f(f(c))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(c))))) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_47099]) ).
tcf(c_47347,plain,
! [X0: $i] : f(f(f(f(f(X0))))) != c,
inference(instantiation,[status(thm)],[c_16091]) ).
tcf(c_47348,plain,
f(f(f(f(f(c))))) != c,
inference(instantiation,[status(thm)],[c_47347]) ).
tcf(c_47476,plain,
! [X0: $i] :
( ( c = f(f(f(f(X0)))) )
| ( f(c) != f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_4302]) ).
tcf(c_48127,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(f(X0))))) )
| ( f(c) != f(c) )
| ( f(f(f(f(f(X0))))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_7751]) ).
tcf(c_48306,plain,
! [X0: $i,X1: $i] :
( ( f(f(c)) = f(f(f(f(X0)))) )
| ( f(f(c)) = f(f(f(f(f(X1))))) )
| ( f(f(f(f(X0)))) = f(f(f(f(f(X1))))) )
| ~ r(f(f(c)),f(f(f(f(X0)))))
| ~ r(f(f(c)),f(f(f(f(f(X1))))))
| ~ r(f(f(f(f(X0)))),f(f(f(f(f(X1)))))) ),
inference(instantiation,[status(thm)],[c_12458]) ).
tcf(c_48308,plain,
( ( f(f(c)) = f(f(f(f(c)))) )
| ( f(f(c)) = f(f(f(f(f(c))))) )
| ( f(f(f(f(c)))) = f(f(f(f(f(c))))) )
| ~ r(f(f(c)),f(f(f(f(c)))))
| ~ r(f(f(c)),f(f(f(f(f(c))))))
| ~ r(f(f(f(f(c)))),f(f(f(f(f(c)))))) ),
inference(instantiation,[status(thm)],[c_48306]) ).
tcf(c_48319,plain,
! [X0: $i] :
( ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(c)),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_1887]) ).
tcf(c_48341,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(f(X0))))) )
| ( f(f(c)) = f(c) )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ~ r(f(f(c)),f(c))
| ~ r(f(c),f(f(f(f(f(X0))))))
| ~ r(f(f(c)),f(f(f(f(f(X0)))))) ),
inference(instantiation,[status(thm)],[c_13368]) ).
tcf(c_48424,plain,
! [X0: $i] :
( ( f(f(c)) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ~ r(f(f(c)),c)
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_1027]) ).
tcf(c_48426,plain,
! [X0: $i] :
( ( c = f(f(c)) )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ~ r(c,f(f(c)))
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_559]) ).
tcf(c_48472,plain,
! [X0: $i] :
( ( f(f(c)) = f(c) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ~ r(f(f(c)),f(c))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_14795]) ).
tcf(c_48473,plain,
! [X0: $i] :
( ( f(c) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_11016]) ).
tcf(c_48475,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(f(f(X0))))))
| ~ r(f(f(f(f(f(X0))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_14794]) ).
tcf(c_48477,plain,
( ( f(c) = f(f(c)) )
| ( f(f(f(f(f(c))))) = f(c) )
| ( f(f(f(f(f(c))))) = f(f(c)) )
| ~ r(f(c),f(f(c)))
| ~ r(f(f(f(f(f(c))))),f(c))
| ~ r(f(f(f(f(f(c))))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_48473]) ).
tcf(c_49173,plain,
! [X0: $i,X1: $i] :
( ( f(f(X1)) = f(f(f(c))) )
| ( f(f(X1)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(f(X1)),f(f(f(c))))
| ~ r(f(f(X1)),f(f(f(f(f(X0))))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_17724]) ).
tcf(c_49174,plain,
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(c)) = f(f(f(f(f(c))))) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(c)),f(f(f(f(f(c))))))
| ~ r(f(f(f(f(f(c))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_49173]) ).
tcf(c_51885,plain,
! [X0: $i] :
( ( c = f(f(f(f(X0)))) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(f(X0)))) )
| ~ r(f(f(c)),c)
| ~ r(c,f(f(f(f(X0)))))
| ~ r(f(f(c)),f(f(f(f(X0))))) ),
inference(instantiation,[status(thm)],[c_1574]) ).
tcf(c_51886,plain,
( ( c = f(f(f(f(c)))) )
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(f(c)))) )
| ~ r(f(f(c)),c)
| ~ r(c,f(f(f(f(c)))))
| ~ r(f(f(c)),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_51885]) ).
tcf(c_53319,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),c)
| r(f(f(f(f(f(X0))))),c)
| r(f(f(f(f(f(X0))))),f(f(X1)))
| ( f(f(X1)) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_20839]) ).
tcf(c_53320,plain,
( r(f(f(c)),c)
| r(f(f(f(f(f(c))))),c)
| r(f(f(f(f(f(c))))),f(f(c)))
| ( f(f(c)) = c )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_53319]) ).
tcf(c_53340,plain,
! [X0: $i] :
( r(f(f(c)),c)
| r(f(f(f(f(f(X0))))),c)
| r(f(f(c)),f(f(f(f(f(X0))))))
| ( f(f(c)) = c )
| ( f(f(c)) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = c ) ),
inference(instantiation,[status(thm)],[c_20841]) ).
tcf(c_54731,plain,
! [X0: $i] :
( ( f(c) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(c) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),f(c))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_16444]) ).
tcf(c_54732,plain,
( ( f(c) = f(f(f(c))) )
| ( f(f(f(f(f(c))))) = f(c) )
| ( f(f(f(f(f(c))))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(f(f(f(f(c))))),f(c))
| ~ r(f(f(f(f(f(c))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_54731]) ).
tcf(c_54878,plain,
! [X0: $i] :
( ( f(c) = f(f(f(c))) )
| ( f(c) = f(f(f(f(f(X0))))) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(c),f(f(f(c))))
| ~ r(f(c),f(f(f(f(f(X0))))))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_17726]) ).
tcf(c_57542,plain,
! [X0: $i] :
( ( c = f(f(f(X0))) )
| ( f(c) = c )
| ( f(c) = f(f(f(X0))) )
| ~ r(f(c),c)
| ~ r(c,f(f(f(X0))))
| ~ r(f(c),f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_830]) ).
tcf(c_57543,plain,
( ( c = f(f(f(c))) )
| ( f(c) = c )
| ( f(c) = f(f(f(c))) )
| ~ r(f(c),c)
| ~ r(c,f(f(f(c))))
| ~ r(f(c),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_57542]) ).
tcf(c_58357,plain,
! [X0: $i] :
( ( f(f(f(c))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(f(f(c))),f(f(c)))
| ~ r(f(f(f(f(f(X0))))),f(f(c)))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_12172]) ).
tcf(c_58588,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(f(f(X0))))) = f(f(c)) )
| ( f(f(f(f(f(X0))))) = f(f(f(c))) )
| ~ r(f(f(c)),f(f(f(c))))
| ~ r(f(f(f(f(f(X0))))),f(f(c)))
| ~ r(f(f(f(f(f(X0))))),f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_12274]) ).
tcf(c_60806,plain,
f(f(f(c))) != c,
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_60816,plain,
! [X0: $i] : f(f(f(X0))) != c,
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_63865,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(f(f(X1)))) )
| ( f(X0) = c )
| ( f(X0) = f(f(f(f(X1)))) )
| ~ r(f(X0),c)
| ~ r(c,f(f(f(f(X1)))))
| ~ r(f(X0),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_565]) ).
tcf(c_63866,plain,
( ( c = f(f(f(f(c)))) )
| ( f(c) = c )
| ( f(c) = f(f(f(f(c)))) )
| ~ r(f(c),c)
| ~ r(c,f(f(f(f(c)))))
| ~ r(f(c),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_63865]) ).
tcf(c_64659,plain,
! [X0: $i,X1: $i] :
( ( c = f(X1) )
| ( c = f(f(f(f(X0)))) )
| ( f(f(f(f(X0)))) = f(X1) )
| ~ r(c,f(X1))
| ~ r(c,f(f(f(f(X0)))))
| ~ r(f(f(f(f(X0)))),f(X1)) ),
inference(instantiation,[status(thm)],[c_846]) ).
tcf(c_64660,plain,
( ( c = f(c) )
| ( c = f(f(f(f(c)))) )
| ( f(f(f(f(c)))) = f(c) )
| ~ r(c,f(c))
| ~ r(c,f(f(f(f(c)))))
| ~ r(f(f(f(f(c)))),f(c)) ),
inference(instantiation,[status(thm)],[c_64659]) ).
tcf(c_64728,plain,
! [X0: $i,X1: $i] :
( ( f(X1) = c )
| ( f(f(f(f(X0)))) = c )
| ( f(f(f(f(X0)))) = f(X1) )
| ~ r(f(X1),c)
| ~ r(f(f(f(f(X0)))),c)
| ~ r(f(f(f(f(X0)))),f(X1)) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_64729,plain,
( ( f(c) = c )
| ( f(f(f(f(c)))) = c )
| ( f(f(f(f(c)))) = f(c) )
| ~ r(f(c),c)
| ~ r(f(f(f(f(c)))),c)
| ~ r(f(f(f(f(c)))),f(c)) ),
inference(instantiation,[status(thm)],[c_64728]) ).
tcf(c_65232,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X1)))) = c )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(f(X1)))) )
| ~ r(f(f(f(f(X1)))),c)
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_41656]) ).
tcf(c_65233,plain,
( ( f(f(f(f(c)))) = c )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(f(f(f(c)))) )
| ~ r(f(f(f(f(c)))),c)
| ~ r(f(f(f(f(f(c))))),c)
| ~ r(f(f(f(f(f(c))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_65232]) ).
tcf(c_65614,plain,
! [X0: $i,X1: $i] :
( ( c = f(f(f(f(X1)))) )
| ( f(f(f(f(f(X0))))) = c )
| ( f(f(f(f(f(X0))))) = f(f(f(f(X1)))) )
| ~ r(c,f(f(f(f(X1)))))
| ~ r(f(f(f(f(f(X0))))),c)
| ~ r(f(f(f(f(f(X0))))),f(f(f(f(X1))))) ),
inference(instantiation,[status(thm)],[c_41657]) ).
tcf(c_65615,plain,
( ( c = f(f(f(f(c)))) )
| ( f(f(f(f(f(c))))) = c )
| ( f(f(f(f(f(c))))) = f(f(f(f(c)))) )
| ~ r(c,f(f(f(f(c)))))
| ~ r(f(f(f(f(f(c))))),c)
| ~ r(f(f(f(f(f(c))))),f(f(f(f(c))))) ),
inference(instantiation,[status(thm)],[c_65614]) ).
tcf(c_70000,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_65615,c_65233,c_64729,c_64660,c_63866,c_60816,c_60806,c_58588,c_58357,c_57543,c_54878,c_54732,c_54731,c_53340,c_53320,c_51886,c_49174,c_48472,c_48477,c_48475,c_48424,c_48426,c_48341,c_48319,c_48308,c_48127,c_47476,c_47348,c_47347,c_47100,c_47099,c_47081,c_47016,c_46711,c_46512,c_46135,c_44019,c_43753,c_42911,c_42189,c_42173,c_42179,c_42185,c_41940,c_41939,c_41728,c_41720,c_41664,c_41659,c_41660,c_40501,c_40458,c_37422,c_37393,c_37394,c_37416,c_37405,c_37407,c_35156,c_35045,c_33627,c_33587,c_33362,c_33272,c_32872,c_32869,c_32778,c_32776,c_30720,c_30719,c_26279,c_21533,c_20851,c_20849,c_16092,c_16091,c_15407,c_15405,c_14799,c_14700,c_14450,c_13372,c_13203,c_13202,c_12422,c_12275,c_11722,c_11657,c_11168,c_11021,c_10937,c_10801,c_9835,c_9834,c_9391,c_8790,c_8377,c_7753,c_7752,c_7537,c_7534,c_6935,c_6614,c_6613,c_6603,c_6602,c_6068,c_6057,c_5737,c_5666,c_5515,c_4303,c_4302,c_4196,c_3924,c_3213,c_3172,c_2661,c_2652,c_2651,c_2594,c_2447,c_2427,c_2426,c_2419,c_2293,c_1694,c_1069,c_1068,c_554,c_433,c_391,c_239,c_238,c_235,c_234,c_220,c_219,c_203,c_202,c_198,c_197,c_196,c_193,c_192,c_59,c_57]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRA118-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Wed Sep 23 12:52:21 UTC 2026
% 0.04/0.29 % CPUTime :
% 0.04/0.29 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.31 Running first-order theorem proving
% 0.04/0.31 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.04/0.32
% 0.04/0.32 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.32
% 0.04/0.32 % Detected problem language: tptp
% 0.06/0.33 % Proving...
% 3.96/2.00 % SZS status Started for theBenchmark.p
% 3.96/2.00 % SZS status Unsatisfiable for theBenchmark.p
% 3.96/2.00
% 3.96/2.00 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.96/2.00
% 3.96/2.00 % ------ iProver source info
% 3.96/2.00
% 3.96/2.00 % git: date: 2026-07-19 20:42:38 +0200
% 3.96/2.00 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.96/2.00 % git: non_committed_changes: false
% 3.96/2.00
% 3.96/2.00 % ------ Parsing...% successful
% 3.96/2.00
% 3.96/2.00
% 3.96/2.00 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.96/2.00
% 3.96/2.00 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 3.96/2.00
% 3.96/2.00 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.96/2.00
% 3.96/2.00 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.96/2.00 % ------ Proving...
% 3.96/2.00 % ------ Problem Properties
% 3.96/2.00
% 3.96/2.00 %
% 3.96/2.00 % clauses 5
% 3.96/2.00 % conjectures 0
% 3.96/2.00 % EPR 3
% 3.96/2.00 % Horn 3
% 3.96/2.00 % unary 1
% 3.96/2.00 % binary 2
% 3.96/2.00 % lits 17
% 3.96/2.00 % lits eq 9
% 3.96/2.00 % fd_pure 0
% 3.96/2.00 % fd_pseudo 0
% 3.96/2.00 % fd_cond 0
% 3.96/2.00 % fd_pseudo_cond 3
% 3.96/2.00 % AC symbols 0
% 3.96/2.00
% 3.96/2.00 % ------ Input Options Time Limit: Unbounded
% 3.96/2.00
% 3.96/2.00
% 3.96/2.00 % ------
% 3.96/2.00 % Current options:
% 3.96/2.00 % ------
% 3.96/2.00
% 3.96/2.00
% 3.96/2.00 %
% 3.96/2.00
% 3.96/2.00 % ------ Proving...
% 3.96/2.00 %
% 3.96/2.00
% 3.96/2.00 % SZS status Unsatisfiable for theBenchmark.p
% 3.96/2.00
% 3.96/2.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.96/2.01
% 3.96/2.01
%------------------------------------------------------------------------------