%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.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 9.71s 2.29s
% Output : CNFRefutation 9.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 421 ( 20 unt; 0 def)
% Number of atoms : 2048 (1109 equ)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 2214 ( 587 ~;1627 |; 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 : 605 ( 0 sgn 605 !; 0 ?; 583 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rsym) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rn3cl) ).
fof(f3,axiom,
! [X0,X1,X2] :
( r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rn3acl) ).
fof(f4,axiom,
! [X0] : f(X0) != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pfnc) ).
fof(f5,axiom,
! [X0,X1] :
( X0 = X1
| f(X0) != f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pfinj) ).
fof(f6,plain,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f7,plain,
! [X2,X0,X1] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f8,plain,
! [X2,X0,X1] :
( r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f9,plain,
! [X0] : f(X0) != c,
inference(cnf_transformation,[],[f4]) ).
fof(f10,plain,
! [X0,X1] :
( X0 = X1
| f(X0) != f(X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_50,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,[],[f7]) ).
tcf(c_51,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,[],[f8]) ).
tcf(c_52,plain,
! [X0: $i] : f(X0) != c,
inference(cnf_transformation,[],[f9]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( f(X0) != f(X1) ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_54,plain,
f(c) != c,
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_95,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_186,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_50]) ).
tcf(c_187,plain,
! [X0: $i] :
( ( f(X0) = c )
| ( f(f(X0)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_188,plain,
( ( f(c) = c )
| ( f(f(c)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = c )
| ( c != X1 )
| ( f(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_190,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_50]) ).
tcf(c_191,plain,
! [X0: $i] :
( ( f(f(X0)) = f(c) )
| ( f(f(f(X0))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_192,plain,
( ( f(f(c)) = f(c) )
| ( f(f(f(c))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_193,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_190]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(c) != X1 )
| ( f(f(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_195,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_50]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = X1 )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_197,plain,
! [X0: $i] :
( ( f(X0) = c )
| ( c != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_198,plain,
( ( f(c) = c )
| ( c != f(c) )
| ( f(c) != f(c) ) ),
inference(instantiation,[status(thm)],[c_197]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(X0) = X2 )
| ( X2 != X1 )
| ( f(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_214,plain,
! [X0: $i] : f(X0) = f(X0),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_215,plain,
f(c) = f(c),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = X1 )
| ( X1 != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_221,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_51]) ).
tcf(c_224,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_51]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i] :
( r(f(X1),X0)
| ~ r(X0,f(X1)) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_229,plain,
! [X0: $i] : f(f(X0)) = f(f(X0)),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_230,plain,
f(f(c)) = f(f(c)),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_231,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_186]) ).
tcf(c_232,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_50]) ).
tcf(c_233,plain,
! [X0: $i] :
( ( c = f(X0) )
| ( f(c) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_234,plain,
( ( c = f(c) )
| ( f(c) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_242,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_50]) ).
tcf(c_262,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_221]) ).
tcf(c_263,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_51]) ).
tcf(c_265,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_224]) ).
tcf(c_266,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_224]) ).
tcf(c_267,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_224]) ).
tcf(c_268,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_224]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(c) )
| ( f(c) != f(X1) )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_324,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_262]) ).
tcf(c_374,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_232]) ).
tcf(c_385,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_265]) ).
tcf(c_386,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_385]) ).
tcf(c_393,plain,
! [X0: $i] :
( ( f(c) = f(X0) )
| ( f(c) != f(c) )
| ( f(X0) != f(c) ) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_427,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_267]) ).
tcf(c_428,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_427]) ).
tcf(c_446,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_263]) ).
tcf(c_454,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_266]) ).
tcf(c_457,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_266]) ).
tcf(c_458,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(X1) )
| ( f(X1) != f(X0) )
| ( f(X0) != f(X0) ) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_460,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_266]) ).
tcf(c_548,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_231]) ).
tcf(c_549,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_548]) ).
tcf(c_554,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_231]) ).
tcf(c_556,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_231]) ).
tcf(c_557,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_231]) ).
tcf(c_560,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_231]) ).
tcf(c_562,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_195]) ).
tcf(c_563,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_195]) ).
tcf(c_564,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_195]) ).
tcf(c_579,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_242]) ).
tcf(c_702,plain,
! [X0: $i] :
( ( f(c) = f(f(X0)) )
| ( f(c) != f(c) )
| ( f(f(X0)) != f(c) ) ),
inference(instantiation,[status(thm)],[c_393]) ).
tcf(c_788,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_458]) ).
tcf(c_825,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_556]) ).
tcf(c_831,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_324]) ).
tcf(c_841,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_374]) ).
tcf(c_852,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_385]) ).
tcf(c_877,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_268]) ).
tcf(c_878,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_557]) ).
tcf(c_880,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(X0))
| ~ r(f(X0),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_884,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_446]) ).
tcf(c_1014,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_446]) ).
tcf(c_1022,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_562]) ).
tcf(c_1025,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_562]) ).
tcf(c_1030,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_562]) ).
tcf(c_1035,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_563]) ).
tcf(c_1063,plain,
! [X0: $i] : f(f(X0)) != c,
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_1064,plain,
f(f(c)) != c,
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_1073,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(X0)) = X2 )
| ( X2 != X1 )
| ( f(f(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1075,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_190]) ).
tcf(c_1092,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_564]) ).
tcf(c_1094,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_564]) ).
tcf(c_1099,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_564]) ).
tcf(c_1155,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_579]) ).
tcf(c_1165,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_460]) ).
tcf(c_1409,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(X0)) = X2 )
| ( X2 != f(X1) )
| ( f(f(X0)) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_1073]) ).
tcf(c_1448,plain,
! [X0: $i,X1: $i] :
( r(f(X1),f(f(X0)))
| ~ r(f(f(X0)),f(X1)) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1452,plain,
! [X0: $i] :
( r(f(f(X0)),c)
| ~ r(c,f(f(X0))) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1569,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_878]) ).
tcf(c_1589,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_268]) ).
tcf(c_1591,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_268]) ).
tcf(c_1608,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_1014]) ).
tcf(c_1642,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_457]) ).
tcf(c_1688,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_446]) ).
tcf(c_1689,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_1688]) ).
tcf(c_1690,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_446]) ).
tcf(c_1714,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_1094]) ).
tcf(c_1715,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_1094]) ).
tcf(c_1752,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_454]) ).
tcf(c_1760,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_557]) ).
tcf(c_1840,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_1014]) ).
tcf(c_1844,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_884]) ).
tcf(c_1867,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_1035]) ).
tcf(c_1875,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(X1) )
| ( f(f(X0)) != f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1882,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_1035]) ).
tcf(c_1884,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_788]) ).
tcf(c_2106,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_1099]) ).
tcf(c_2107,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_1099]) ).
tcf(c_2229,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_1155]) ).
tcf(c_2280,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_1030]) ).
tcf(c_2287,plain,
! [X0: $i] :
( r(f(f(f(X0))),c)
| ~ r(c,f(f(f(X0)))) ),
inference(instantiation,[status(thm)],[c_1452]) ).
tcf(c_2288,plain,
( r(f(f(f(c))),c)
| ~ r(c,f(f(f(c)))) ),
inference(instantiation,[status(thm)],[c_2287]) ).
tcf(c_2365,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_1884]) ).
tcf(c_2410,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_324]) ).
tcf(c_2414,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_2410]) ).
tcf(c_2418,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_852]) ).
tcf(c_2419,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_831]) ).
tcf(c_2421,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_2419]) ).
tcf(c_2422,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_2418]) ).
tcf(c_2441,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_457]) ).
tcf(c_2442,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_2441]) ).
tcf(c_2447,plain,
! [X0: $i] :
( r(f(f(c)),f(f(f(X0))))
| ~ r(f(f(f(X0))),f(f(c))) ),
inference(instantiation,[status(thm)],[c_880]) ).
tcf(c_2449,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_884]) ).
tcf(c_2588,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = X1 )
| ( X1 != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_2589,plain,
( ( f(f(c)) = c )
| ( c != f(f(c)) )
| ( f(f(c)) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_2588]) ).
tcf(c_2646,plain,
! [X0: $i] :
( ( f(f(f(X0))) = f(f(c)) )
| ( f(f(f(f(X0)))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2647,plain,
( ( f(f(f(c))) = f(f(c)) )
| ( f(f(f(f(c)))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2646]) ).
tcf(c_2648,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(X1) )
| ( f(f(f(X0))) != f(f(X1)) ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2649,plain,
! [X0: $i] :
( ( f(c) = f(X0) )
| ( f(f(c)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2655,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(f(X1)) )
| ( f(f(X0)) != f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2656,plain,
( ( f(c) = f(f(c)) )
| ( f(f(c)) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_2655]) ).
tcf(c_2766,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( f(f(f(X0))) = X2 )
| ( X2 != X1 )
| ( f(f(f(X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_1073]) ).
tcf(c_2804,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_1844]) ).
tcf(c_2818,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_457]) ).
tcf(c_2820,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_1014]) ).
tcf(c_2822,plain,
! [X0: $i,X1: $i] :
( r(f(f(X1)),f(f(X0)))
| ~ r(f(f(X0)),f(f(X1))) ),
inference(instantiation,[status(thm)],[c_1448]) ).
tcf(c_2825,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_884]) ).
tcf(c_2826,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_877]) ).
tcf(c_2838,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_1608]) ).
tcf(c_3002,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_1591]) ).
tcf(c_3044,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_1642]) ).
tcf(c_3166,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_1714]) ).
tcf(c_3167,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_3166]) ).
tcf(c_3180,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_1752]) ).
tcf(c_3207,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_1760]) ).
tcf(c_3208,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_3207]) ).
tcf(c_3282,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_1690]) ).
tcf(c_3384,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_2106]) ).
tcf(c_3541,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_2107]) ).
tcf(c_3560,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_2107]) ).
tcf(c_3585,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_2229]) ).
tcf(c_3796,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_2107]) ).
tcf(c_3800,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_1760]) ).
tcf(c_3919,plain,
! [X0: $i] :
( ( f(c) = f(f(X0)) )
| ( f(f(c)) != f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_2649]) ).
tcf(c_4126,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_1035]) ).
tcf(c_4191,plain,
! [X0: $i] :
( ( f(f(X0)) = c )
| ( c != f(f(X0)) )
| ( f(f(X0)) != f(f(X0)) ) ),
inference(instantiation,[status(thm)],[c_2588]) ).
tcf(c_4238,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_2766]) ).
tcf(c_4271,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_454]) ).
tcf(c_4276,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_1094]) ).
tcf(c_4297,plain,
! [X0: $i] :
( ( c = f(f(X0)) )
| ( f(c) != f(f(f(X0))) ) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_4298,plain,
( ( c = f(f(c)) )
| ( f(c) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_4297]) ).
tcf(c_4729,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_1165]) ).
tcf(c_5159,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_2449]) ).
tcf(c_5342,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),X0)
| ~ r(X0,f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_5450,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_2280]) ).
tcf(c_5477,plain,
! [X0: $i,X1: $i] :
( ( f(f(X0)) = f(f(X1)) )
| ( f(f(f(X0))) != f(f(f(X1))) ) ),
inference(instantiation,[status(thm)],[c_2648]) ).
tcf(c_5509,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_2820]) ).
tcf(c_5510,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_5509]) ).
tcf(c_5660,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_2818]) ).
tcf(c_5661,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_5660]) ).
tcf(c_5662,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_2818]) ).
tcf(c_5672,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_2818]) ).
tcf(c_5731,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_2825]) ).
tcf(c_5732,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_5731]) ).
tcf(c_5743,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_2825]) ).
tcf(c_5769,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_2826]) ).
tcf(c_5809,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_3180]) ).
tcf(c_6011,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_3541]) ).
tcf(c_6051,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_3002]) ).
tcf(c_6052,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_6051]) ).
tcf(c_6062,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_3002]) ).
tcf(c_6063,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_6062]) ).
tcf(c_6088,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_3282]) ).
tcf(c_6110,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_3560]) ).
tcf(c_6168,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_3585]) ).
tcf(c_6546,plain,
! [X0: $i,X1: $i] :
( r(f(f(f(X1))),f(X0))
| ~ r(f(X0),f(f(f(X1)))) ),
inference(instantiation,[status(thm)],[c_5342]) ).
tcf(c_6597,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_5477]) ).
tcf(c_6598,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_6597]) ).
tcf(c_6599,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_5477]) ).
tcf(c_6608,plain,
! [X0: $i] :
( ( f(f(c)) = f(f(f(X0))) )
| ( f(f(f(c))) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_5477]) ).
tcf(c_6609,plain,
( ( f(f(c)) = f(f(f(c))) )
| ( f(f(f(c))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_6608]) ).
tcf(c_6929,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_4238]) ).
tcf(c_6930,plain,
( ( f(f(f(c))) = c )
| ( c != f(f(f(c))) )
| ( f(f(f(c))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_6929]) ).
tcf(c_7529,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_2365]) ).
tcf(c_7530,plain,
! [X0: $i] :
( ( f(f(f(X0))) = f(c) )
| ( f(f(f(f(X0)))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_7532,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_7529]) ).
tcf(c_7666,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_5159]) ).
tcf(c_7737,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_3796]) ).
tcf(c_7746,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_702]) ).
tcf(c_7747,plain,
! [X0: $i] :
( ( f(f(f(X0))) = c )
| ( f(f(f(f(X0)))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_7748,plain,
( ( f(f(f(c))) = c )
| ( f(f(f(f(c)))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_7747]) ).
tcf(c_7923,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_3800]) ).
tcf(c_8167,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_5450]) ).
tcf(c_8215,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_4276]) ).
tcf(c_8366,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_5731]) ).
tcf(c_8371,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_5731]) ).
tcf(c_8372,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_8371]) ).
tcf(c_8378,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_1409]) ).
tcf(c_8383,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_322]) ).
tcf(c_8384,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(X0))) = X1 )
| ( f(f(f(f(X0)))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_8608,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_5662]) ).
tcf(c_8677,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_6011]) ).
tcf(c_8784,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_6088]) ).
tcf(c_8785,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_8784]) ).
tcf(c_8866,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_6110]) ).
tcf(c_9027,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_6168]) ).
tcf(c_9133,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_5672]) ).
tcf(c_9385,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_6599]) ).
tcf(c_9386,plain,
( ( f(f(f(c))) = f(f(f(c))) )
| ( f(f(f(f(c)))) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_9385]) ).
tcf(c_9829,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_8383]) ).
tcf(c_9830,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_9829]) ).
tcf(c_10062,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_1591]) ).
tcf(c_10072,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_5769]) ).
tcf(c_10075,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_5743]) ).
tcf(c_10165,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_5809]) ).
tcf(c_10166,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_2804]) ).
tcf(c_10795,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_8378]) ).
tcf(c_10796,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_10795]) ).
tcf(c_10931,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_1715]) ).
tcf(c_10932,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_10931]) ).
tcf(c_11011,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_1075]) ).
tcf(c_11015,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_4126]) ).
tcf(c_11016,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_11015]) ).
tcf(c_11162,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_8215]) ).
tcf(c_11163,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_11162]) ).
tcf(c_11199,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_8215]) ).
tcf(c_11531,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_7737]) ).
tcf(c_11568,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_7737]) ).
tcf(c_11651,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_7666]) ).
tcf(c_11652,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_11651]) ).
tcf(c_11688,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_7666]) ).
tcf(c_11716,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_7923]) ).
tcf(c_11717,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_11716]) ).
tcf(c_11753,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_7923]) ).
tcf(c_11792,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_8167]) ).
tcf(c_11827,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_8167]) ).
tcf(c_12167,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_8677]) ).
tcf(c_12269,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_8866]) ).
tcf(c_12270,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_12269]) ).
tcf(c_12416,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_9027]) ).
tcf(c_12417,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_12416]) ).
tcf(c_12453,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_9027]) ).
tcf(c_13197,plain,
! [X0: $i] : f(f(f(f(X0)))) = f(f(f(f(X0)))),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_13198,plain,
f(f(f(f(c)))) = f(f(f(f(c)))),
inference(instantiation,[status(thm)],[c_13197]) ).
tcf(c_13362,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_3384]) ).
tcf(c_13363,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_3166]) ).
tcf(c_13367,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_13362]) ).
tcf(c_14445,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_10795]) ).
tcf(c_14694,plain,
! [X0: $i,X1: $i] :
( ( f(X0) = f(f(f(X1))) )
| ( f(f(X0)) != f(f(f(f(X1)))) ) ),
inference(instantiation,[status(thm)],[c_2655]) ).
tcf(c_14695,plain,
( ( f(c) = f(f(f(c))) )
| ( f(f(c)) != f(f(f(f(c)))) ) ),
inference(instantiation,[status(thm)],[c_14694]) ).
tcf(c_14789,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_2447]) ).
tcf(c_14790,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_1867]) ).
tcf(c_14793,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_1092]) ).
tcf(c_14794,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_14793]) ).
tcf(c_15225,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_10072]) ).
tcf(c_15395,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_2838]) ).
tcf(c_15397,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_1840]) ).
tcf(c_15400,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_15397]) ).
tcf(c_15402,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_15395]) ).
tcf(c_15903,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_10075]) ).
tcf(c_16086,plain,
! [X0: $i] : f(f(f(f(X0)))) != c,
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_16087,plain,
f(f(f(f(c)))) != c,
inference(instantiation,[status(thm)],[c_16086]) ).
tcf(c_16419,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_2822]) ).
tcf(c_16439,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_10931]) ).
tcf(c_17239,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_10165]) ).
tcf(c_17339,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_11199]) ).
tcf(c_17717,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_11531]) ).
tcf(c_17719,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_11531]) ).
tcf(c_17721,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_11531]) ).
tcf(c_17829,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_11568]) ).
tcf(c_18123,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_11688]) ).
tcf(c_20832,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_9133]) ).
tcf(c_20834,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_8608]) ).
tcf(c_20836,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_4729]) ).
tcf(c_20837,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_4271]) ).
tcf(c_20839,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_3044]) ).
tcf(c_20844,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_20839]) ).
tcf(c_20846,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_20837]) ).
tcf(c_21528,plain,
! [X0: $i] :
( ( f(c) = f(f(f(X0))) )
| ( f(f(c)) != f(f(f(f(X0)))) ) ),
inference(instantiation,[status(thm)],[c_14694]) ).
tcf(c_24327,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_15225]) ).
tcf(c_24359,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_15903]) ).
tcf(c_24611,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_10166]) ).
tcf(c_24940,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_5672]) ).
tcf(c_24943,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_2441]) ).
tcf(c_24945,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_1589]) ).
tcf(c_24946,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_454]) ).
tcf(c_24967,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_10062]) ).
tcf(c_26136,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_6546]) ).
tcf(c_26154,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_11568]) ).
tcf(c_26272,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_6599]) ).
tcf(c_26273,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_17239]) ).
tcf(c_26274,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_26273]) ).
tcf(c_26478,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_17339]) ).
tcf(c_26612,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_17717]) ).
tcf(c_26807,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_17829]) ).
tcf(c_30714,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_26272]) ).
tcf(c_30715,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_30714]) ).
tcf(c_31546,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_20832]) ).
tcf(c_32771,plain,
! [X0: $i] :
( ( f(f(f(f(X0)))) = f(c) )
| ( f(f(f(f(f(X0))))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_7530]) ).
tcf(c_32773,plain,
( ( f(f(f(f(c)))) = f(c) )
| ( f(f(f(f(f(c))))) != f(f(c)) ) ),
inference(instantiation,[status(thm)],[c_32771]) ).
tcf(c_32864,plain,
! [X0: $i] :
( ( f(c) = f(f(f(f(X0)))) )
| ( f(f(c)) != f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_3919]) ).
tcf(c_32867,plain,
( ( f(c) = f(f(f(f(c)))) )
| ( f(f(c)) != f(f(f(f(f(c))))) ) ),
inference(instantiation,[status(thm)],[c_32864]) ).
tcf(c_33266,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_24943]) ).
tcf(c_33267,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_33266]) ).
tcf(c_33357,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_24611]) ).
tcf(c_33581,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_24945]) ).
tcf(c_33582,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_33581]) ).
tcf(c_33621,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_24946]) ).
tcf(c_33622,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_33621]) ).
tcf(c_33837,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_24967]) ).
tcf(c_34533,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_26154]) ).
tcf(c_35040,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_26478]) ).
tcf(c_35151,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_26612]) ).
tcf(c_36089,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_24940]) ).
tcf(c_37388,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_26612]) ).
tcf(c_37389,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_26478]) ).
tcf(c_37391,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_26807]) ).
tcf(c_37397,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_24359]) ).
tcf(c_37398,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_24327]) ).
tcf(c_37400,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_18123]) ).
tcf(c_37401,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_17239]) ).
tcf(c_37402,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_37401]) ).
tcf(c_37411,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_37391]) ).
tcf(c_37417,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_24611]) ).
tcf(c_40453,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_31546]) ).
tcf(c_40496,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_31546]) ).
tcf(c_41651,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_11827]) ).
tcf(c_41652,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_11753]) ).
tcf(c_41654,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_11792]) ).
tcf(c_41655,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_11716]) ).
tcf(c_41659,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_41654]) ).
tcf(c_41715,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_20839]) ).
tcf(c_41723,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_41715]) ).
tcf(c_41934,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_2646]) ).
tcf(c_41935,plain,
( ( f(f(f(f(c)))) = f(f(c)) )
| ( f(f(f(f(f(c))))) != f(f(f(c))) ) ),
inference(instantiation,[status(thm)],[c_41934]) ).
tcf(c_42167,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_11651]) ).
tcf(c_42168,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_8366]) ).
tcf(c_42174,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_8371]) ).
tcf(c_42175,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_5731]) ).
tcf(c_42180,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_42175]) ).
tcf(c_42184,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_42167]) ).
tcf(c_42321,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_26136]) ).
tcf(c_42906,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_34533]) ).
tcf(c_43050,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_16419]) ).
tcf(c_43747,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_36089]) ).
tcf(c_43748,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_43747]) ).
tcf(c_44013,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_33837]) ).
tcf(c_44014,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_44013]) ).
tcf(c_46126,plain,
! [X0: $i,X1: $i] :
( ( f(f(f(f(X0)))) = X1 )
| ( f(f(f(f(f(X0))))) != f(X1) ) ),
inference(instantiation,[status(thm)],[c_8384]) ).
tcf(c_46130,plain,
( ( f(f(f(f(c)))) = c )
| ( f(f(f(f(f(c))))) != f(c) ) ),
inference(instantiation,[status(thm)],[c_46126]) ).
tcf(c_46507,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_42321]) ).
tcf(c_46705,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_43050]) ).
tcf(c_46706,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_46705]) ).
tcf(c_47011,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_37397]) ).
tcf(c_47076,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_37398]) ).
tcf(c_47094,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_37398]) ).
tcf(c_47095,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_47094]) ).
tcf(c_47342,plain,
! [X0: $i] : f(f(f(f(f(X0))))) != c,
inference(instantiation,[status(thm)],[c_16086]) ).
tcf(c_47343,plain,
f(f(f(f(f(c))))) != c,
inference(instantiation,[status(thm)],[c_47342]) ).
tcf(c_47471,plain,
! [X0: $i] :
( ( c = f(f(f(f(X0)))) )
| ( f(c) != f(f(f(f(f(X0))))) ) ),
inference(instantiation,[status(thm)],[c_4297]) ).
tcf(c_48122,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_7746]) ).
tcf(c_48301,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_12453]) ).
tcf(c_48303,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_48301]) ).
tcf(c_48314,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_1882]) ).
tcf(c_48336,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_13363]) ).
tcf(c_48419,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_1022]) ).
tcf(c_48421,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_554]) ).
tcf(c_48467,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_14790]) ).
tcf(c_48468,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_11011]) ).
tcf(c_48470,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_14789]) ).
tcf(c_48472,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_48468]) ).
tcf(c_49168,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_17719]) ).
tcf(c_49169,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_49168]) ).
tcf(c_51880,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_1569]) ).
tcf(c_51881,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_51880]) ).
tcf(c_53314,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_20834]) ).
tcf(c_53315,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_53314]) ).
tcf(c_53335,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_20836]) ).
tcf(c_54726,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_16439]) ).
tcf(c_54727,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_54726]) ).
tcf(c_54873,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_17721]) ).
tcf(c_57537,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_825]) ).
tcf(c_57538,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_57537]) ).
tcf(c_58352,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_12167]) ).
tcf(c_58583,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_12269]) ).
tcf(c_60801,plain,
f(f(f(c))) != c,
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_60811,plain,
! [X0: $i] : f(f(f(X0))) != c,
inference(instantiation,[status(thm)],[c_1063]) ).
tcf(c_63860,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_560]) ).
tcf(c_63861,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_63860]) ).
tcf(c_64654,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_841]) ).
tcf(c_64655,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_64654]) ).
tcf(c_64723,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_1025]) ).
tcf(c_64724,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_64723]) ).
tcf(c_65227,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_41651]) ).
tcf(c_65228,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_65227]) ).
tcf(c_65609,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_41652]) ).
tcf(c_65610,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_65609]) ).
tcf(c_69995,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_65610,c_65228,c_64724,c_64655,c_63861,c_60811,c_60801,c_58583,c_58352,c_57538,c_54873,c_54727,c_54726,c_53335,c_53315,c_51881,c_49169,c_48467,c_48472,c_48470,c_48419,c_48421,c_48336,c_48314,c_48303,c_48122,c_47471,c_47343,c_47342,c_47095,c_47094,c_47076,c_47011,c_46706,c_46507,c_46130,c_44014,c_43748,c_42906,c_42184,c_42168,c_42174,c_42180,c_41935,c_41934,c_41723,c_41715,c_41659,c_41654,c_41655,c_40496,c_40453,c_37417,c_37388,c_37389,c_37411,c_37400,c_37402,c_35151,c_35040,c_33622,c_33582,c_33357,c_33267,c_32867,c_32864,c_32773,c_32771,c_30715,c_30714,c_26274,c_21528,c_20846,c_20844,c_16087,c_16086,c_15402,c_15400,c_14794,c_14695,c_14445,c_13367,c_13198,c_13197,c_12417,c_12270,c_11717,c_11652,c_11163,c_11016,c_10932,c_10796,c_9830,c_9829,c_9386,c_8785,c_8372,c_7748,c_7747,c_7532,c_7529,c_6930,c_6609,c_6608,c_6598,c_6597,c_6063,c_6052,c_5732,c_5661,c_5510,c_4298,c_4297,c_4191,c_3919,c_3208,c_3167,c_2656,c_2647,c_2646,c_2589,c_2442,c_2422,c_2421,c_2414,c_2288,c_1689,c_1064,c_1063,c_549,c_428,c_386,c_234,c_233,c_230,c_229,c_215,c_214,c_198,c_197,c_193,c_192,c_191,c_188,c_187,c_54,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA118+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.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 12:52:48 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 9.71/2.29 % SZS status Started for theBenchmark.p
% 9.71/2.29 % SZS status Unsatisfiable for theBenchmark.p
% 9.71/2.29
% 9.71/2.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.71/2.29
% 9.71/2.29 % ------ iProver source info
% 9.71/2.29
% 9.71/2.29 % git: date: 2026-07-19 20:42:38 +0200
% 9.71/2.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.71/2.29 % git: non_committed_changes: false
% 9.71/2.29
% 9.71/2.29 % ------ Parsing...
% 9.71/2.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 9.71/2.29
% 9.71/2.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 9.71/2.29
% 9.71/2.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 9.71/2.29
% 9.71/2.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 9.71/2.29 % ------ Proving...
% 9.71/2.29 % ------ Problem Properties
% 9.71/2.29
% 9.71/2.29 %
% 9.71/2.29 % clauses 5
% 9.71/2.29 % conjectures 0
% 9.71/2.29 % EPR 3
% 9.71/2.29 % Horn 3
% 9.71/2.29 % unary 1
% 9.71/2.29 % binary 2
% 9.71/2.29 % lits 17
% 9.71/2.29 % lits eq 9
% 9.71/2.29 % fd_pure 0
% 9.71/2.29 % fd_pseudo 0
% 9.71/2.29 % fd_cond 0
% 9.71/2.29 % fd_pseudo_cond 3
% 9.71/2.29 % AC symbols 0
% 9.71/2.29
% 9.71/2.29 % ------ Input Options Time Limit: Unbounded
% 9.71/2.29
% 9.71/2.29
% 9.71/2.29 % ------
% 9.71/2.29 % Current options:
% 9.71/2.29 % ------
% 9.71/2.29
% 9.71/2.29
% 9.71/2.29 %
% 9.71/2.29
% 9.71/2.29 % ------ Proving...
% 9.71/2.29 %
% 9.71/2.29
% 9.71/2.29 % SZS status Unsatisfiable for theBenchmark.p
% 9.71/2.29
% 9.71/2.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.75/2.30
% 9.75/2.30
%------------------------------------------------------------------------------