%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRA120+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 : n015.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:50 PM UTC 2026
% Result : Unsatisfiable 14.79s 2.90s
% Output : CNFRefutation 14.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 41
% Syntax : Number of formulae : 727 ( 111 unt; 0 def)
% Number of atoms : 5992 (3059 equ)
% Maximal formula atoms : 12 ( 8 avg)
% Number of connectives : 5997 ( 732 ~;5265 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 9 avg)
% Maximal term depth : 1 ( 1 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 : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 277 ( 0 sgn 277 !; 0 ?; 259 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',rno3cl) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( r(X2,X3)
| r(X1,X3)
| r(X0,X3)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| X2 = X3
| X1 = X3
| X0 = X3
| X1 = X2
| X0 = X2
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rno4acl) ).
fof(f4,axiom,
v0 != v1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv1) ).
fof(f5,axiom,
v0 != v2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv2) ).
fof(f6,axiom,
v1 != v2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv2) ).
fof(f7,axiom,
v0 != v3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv3) ).
fof(f8,axiom,
v1 != v3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv3) ).
fof(f9,axiom,
v2 != v3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv3) ).
fof(f10,axiom,
v0 != v4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv4) ).
fof(f11,axiom,
v1 != v4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv4) ).
fof(f12,axiom,
v2 != v4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv4) ).
fof(f13,axiom,
v3 != v4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3nv4) ).
fof(f14,axiom,
v0 != v5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv5) ).
fof(f15,axiom,
v1 != v5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv5) ).
fof(f16,axiom,
v2 != v5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv5) ).
fof(f17,axiom,
v3 != v5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3nv5) ).
fof(f18,axiom,
v4 != v5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4nv5) ).
fof(f19,axiom,
v0 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv6) ).
fof(f20,axiom,
v1 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv6) ).
fof(f21,axiom,
v2 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv6) ).
fof(f22,axiom,
v3 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3nv6) ).
fof(f23,axiom,
v4 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4nv6) ).
fof(f24,axiom,
v5 != v6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v5nv6) ).
fof(f25,axiom,
v0 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv7) ).
fof(f26,axiom,
v1 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv7) ).
fof(f27,axiom,
v2 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv7) ).
fof(f28,axiom,
v3 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3nv7) ).
fof(f29,axiom,
v4 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4nv7) ).
fof(f30,axiom,
v5 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v5nv7) ).
fof(f31,axiom,
v6 != v7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v6nv7) ).
fof(f32,axiom,
v0 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v0nv8) ).
fof(f33,axiom,
v1 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1nv8) ).
fof(f34,axiom,
v2 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v2nv8) ).
fof(f35,axiom,
v3 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3nv8) ).
fof(f36,axiom,
v4 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4nv8) ).
fof(f37,axiom,
v5 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v5nv8) ).
fof(f38,axiom,
v6 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v6nv8) ).
fof(f39,axiom,
v7 != v8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v7nv8) ).
fof(f40,plain,
! [X0,X1] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f41,plain,
! [X2,X0,X1] :
( ~ r(X1,X2)
| ~ r(X0,X2)
| ~ r(X0,X1)
| X1 = X2
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
! [X2,X3,X0,X1] :
( r(X2,X3)
| r(X1,X3)
| r(X0,X3)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| X2 = X3
| X1 = X3
| X0 = X3
| X1 = X2
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f43,plain,
v0 != v1,
inference(cnf_transformation,[],[f4]) ).
fof(f44,plain,
v0 != v2,
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
v1 != v2,
inference(cnf_transformation,[],[f6]) ).
fof(f46,plain,
v0 != v3,
inference(cnf_transformation,[],[f7]) ).
fof(f47,plain,
v1 != v3,
inference(cnf_transformation,[],[f8]) ).
fof(f48,plain,
v2 != v3,
inference(cnf_transformation,[],[f9]) ).
fof(f49,plain,
v0 != v4,
inference(cnf_transformation,[],[f10]) ).
fof(f50,plain,
v1 != v4,
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
v2 != v4,
inference(cnf_transformation,[],[f12]) ).
fof(f52,plain,
v3 != v4,
inference(cnf_transformation,[],[f13]) ).
fof(f53,plain,
v0 != v5,
inference(cnf_transformation,[],[f14]) ).
fof(f54,plain,
v1 != v5,
inference(cnf_transformation,[],[f15]) ).
fof(f55,plain,
v2 != v5,
inference(cnf_transformation,[],[f16]) ).
fof(f56,plain,
v3 != v5,
inference(cnf_transformation,[],[f17]) ).
fof(f57,plain,
v4 != v5,
inference(cnf_transformation,[],[f18]) ).
fof(f58,plain,
v0 != v6,
inference(cnf_transformation,[],[f19]) ).
fof(f59,plain,
v1 != v6,
inference(cnf_transformation,[],[f20]) ).
fof(f60,plain,
v2 != v6,
inference(cnf_transformation,[],[f21]) ).
fof(f61,plain,
v3 != v6,
inference(cnf_transformation,[],[f22]) ).
fof(f62,plain,
v4 != v6,
inference(cnf_transformation,[],[f23]) ).
fof(f63,plain,
v5 != v6,
inference(cnf_transformation,[],[f24]) ).
fof(f64,plain,
v0 != v7,
inference(cnf_transformation,[],[f25]) ).
fof(f65,plain,
v1 != v7,
inference(cnf_transformation,[],[f26]) ).
fof(f66,plain,
v2 != v7,
inference(cnf_transformation,[],[f27]) ).
fof(f67,plain,
v3 != v7,
inference(cnf_transformation,[],[f28]) ).
fof(f68,plain,
v4 != v7,
inference(cnf_transformation,[],[f29]) ).
fof(f69,plain,
v5 != v7,
inference(cnf_transformation,[],[f30]) ).
fof(f70,plain,
v6 != v7,
inference(cnf_transformation,[],[f31]) ).
fof(f71,plain,
v0 != v8,
inference(cnf_transformation,[],[f32]) ).
fof(f72,plain,
v1 != v8,
inference(cnf_transformation,[],[f33]) ).
fof(f73,plain,
v2 != v8,
inference(cnf_transformation,[],[f34]) ).
fof(f74,plain,
v3 != v8,
inference(cnf_transformation,[],[f35]) ).
fof(f75,plain,
v4 != v8,
inference(cnf_transformation,[],[f36]) ).
fof(f76,plain,
v5 != v8,
inference(cnf_transformation,[],[f37]) ).
fof(f77,plain,
v6 != v8,
inference(cnf_transformation,[],[f38]) ).
fof(f78,plain,
v7 != v8,
inference(cnf_transformation,[],[f39]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( r(X1,X0)
| ~ r(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
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,[],[f41]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r(X2,X3)
| r(X1,X3)
| r(X1,X2)
| r(X0,X3)
| r(X0,X2)
| r(X0,X1)
| ( X2 = X3 )
| ( X1 = X3 )
| ( X1 = X2 )
| ( X0 = X3 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_52,plain,
v0 != v1,
inference(cnf_transformation,[],[f43]) ).
tcf(c_53,plain,
v0 != v2,
inference(cnf_transformation,[],[f44]) ).
tcf(c_54,plain,
v1 != v2,
inference(cnf_transformation,[],[f45]) ).
tcf(c_55,plain,
v0 != v3,
inference(cnf_transformation,[],[f46]) ).
tcf(c_56,plain,
v1 != v3,
inference(cnf_transformation,[],[f47]) ).
tcf(c_57,plain,
v2 != v3,
inference(cnf_transformation,[],[f48]) ).
tcf(c_58,plain,
v0 != v4,
inference(cnf_transformation,[],[f49]) ).
tcf(c_59,plain,
v1 != v4,
inference(cnf_transformation,[],[f50]) ).
tcf(c_60,plain,
v2 != v4,
inference(cnf_transformation,[],[f51]) ).
tcf(c_61,plain,
v3 != v4,
inference(cnf_transformation,[],[f52]) ).
tcf(c_62,plain,
v0 != v5,
inference(cnf_transformation,[],[f53]) ).
tcf(c_63,plain,
v1 != v5,
inference(cnf_transformation,[],[f54]) ).
tcf(c_64,plain,
v2 != v5,
inference(cnf_transformation,[],[f55]) ).
tcf(c_65,plain,
v3 != v5,
inference(cnf_transformation,[],[f56]) ).
tcf(c_66,plain,
v4 != v5,
inference(cnf_transformation,[],[f57]) ).
tcf(c_67,plain,
v0 != v6,
inference(cnf_transformation,[],[f58]) ).
tcf(c_68,plain,
v1 != v6,
inference(cnf_transformation,[],[f59]) ).
tcf(c_69,plain,
v2 != v6,
inference(cnf_transformation,[],[f60]) ).
tcf(c_70,plain,
v3 != v6,
inference(cnf_transformation,[],[f61]) ).
tcf(c_71,plain,
v4 != v6,
inference(cnf_transformation,[],[f62]) ).
tcf(c_72,plain,
v5 != v6,
inference(cnf_transformation,[],[f63]) ).
tcf(c_73,plain,
v0 != v7,
inference(cnf_transformation,[],[f64]) ).
tcf(c_74,plain,
v1 != v7,
inference(cnf_transformation,[],[f65]) ).
tcf(c_75,plain,
v2 != v7,
inference(cnf_transformation,[],[f66]) ).
tcf(c_76,plain,
v3 != v7,
inference(cnf_transformation,[],[f67]) ).
tcf(c_77,plain,
v4 != v7,
inference(cnf_transformation,[],[f68]) ).
tcf(c_78,plain,
v5 != v7,
inference(cnf_transformation,[],[f69]) ).
tcf(c_79,plain,
v6 != v7,
inference(cnf_transformation,[],[f70]) ).
tcf(c_80,plain,
v0 != v8,
inference(cnf_transformation,[],[f71]) ).
tcf(c_81,plain,
v1 != v8,
inference(cnf_transformation,[],[f72]) ).
tcf(c_82,plain,
v2 != v8,
inference(cnf_transformation,[],[f73]) ).
tcf(c_83,plain,
v3 != v8,
inference(cnf_transformation,[],[f74]) ).
tcf(c_84,plain,
v4 != v8,
inference(cnf_transformation,[],[f75]) ).
tcf(c_85,plain,
v5 != v8,
inference(cnf_transformation,[],[f76]) ).
tcf(c_86,plain,
v6 != v8,
inference(cnf_transformation,[],[f77]) ).
tcf(c_87,plain,
v7 != v8,
inference(cnf_transformation,[],[f78]) ).
tcf(c_205,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_208,plain,
v0 = v0,
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_453,plain,
! [X0: $i] :
( ( v1 = X0 )
| ( v0 = v1 )
| ( v0 = X0 )
| ~ r(v0,v1)
| ~ r(v1,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_454,plain,
! [X0: $i] :
( ( v0 = v1 )
| ( v1 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_455,plain,
( ( v0 = v1 )
| ( v1 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_457,plain,
! [X0: $i] :
( ( v2 = X0 )
| ( v0 = v2 )
| ( v0 = X0 )
| ~ r(v0,v2)
| ~ r(v2,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_458,plain,
! [X0: $i] :
( ( v0 = v2 )
| ( v2 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_459,plain,
( ( v0 = v2 )
| ( v2 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_458]) ).
tcf(c_460,plain,
! [X0: $i,X1: $i] :
( r(v1,v2)
| r(v2,X1)
| r(v2,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v2 = X1 )
| ( v2 = X0 )
| ( v1 = v2 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_461,plain,
! [X0: $i] :
( ( v2 = X0 )
| ( v1 = v2 )
| ( v1 = X0 )
| ~ r(v1,v2)
| ~ r(v2,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_462,plain,
( ( v2 = v0 )
| ( v1 = v2 )
| ( v1 = v0 )
| ~ r(v2,v0)
| ~ r(v1,v2)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_466,plain,
! [X0: $i] :
( ( v3 = X0 )
| ( v0 = v3 )
| ( v0 = X0 )
| ~ r(v0,v3)
| ~ r(v3,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_467,plain,
! [X0: $i] :
( ( v0 = v3 )
| ( v3 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_468,plain,
( ( v0 = v3 )
| ( v3 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_469,plain,
! [X0: $i,X1: $i] :
( r(v1,v3)
| r(v3,X1)
| r(v3,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v3 = X1 )
| ( v3 = X0 )
| ( v1 = v3 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_470,plain,
! [X0: $i] :
( ( v3 = X0 )
| ( v1 = v3 )
| ( v1 = X0 )
| ~ r(v1,v3)
| ~ r(v3,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_471,plain,
( ( v3 = v0 )
| ( v1 = v3 )
| ( v1 = v0 )
| ~ r(v3,v0)
| ~ r(v1,v3)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_470]) ).
tcf(c_474,plain,
! [X0: $i,X1: $i] :
( r(v2,v3)
| r(v3,X1)
| r(v3,X0)
| r(v2,X1)
| r(v2,X0)
| r(X0,X1)
| ( v3 = X1 )
| ( v3 = X0 )
| ( v2 = v3 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_475,plain,
! [X0: $i] :
( ( v3 = X0 )
| ( v2 = v3 )
| ( v2 = X0 )
| ~ r(v2,v3)
| ~ r(v3,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_476,plain,
( ( v3 = v0 )
| ( v2 = v3 )
| ( v2 = v0 )
| ~ r(v3,v0)
| ~ r(v2,v3)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_475]) ).
tcf(c_480,plain,
! [X0: $i] :
( ( v4 = X0 )
| ( v0 = v4 )
| ( v0 = X0 )
| ~ r(v0,v4)
| ~ r(v4,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_481,plain,
! [X0: $i] :
( ( v0 = v4 )
| ( v4 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_482,plain,
( ( v0 = v4 )
| ( v4 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_481]) ).
tcf(c_483,plain,
! [X0: $i,X1: $i] :
( r(v1,v4)
| r(v4,X1)
| r(v4,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v4 = X1 )
| ( v4 = X0 )
| ( v1 = v4 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_484,plain,
! [X0: $i] :
( ( v4 = X0 )
| ( v1 = v4 )
| ( v1 = X0 )
| ~ r(v1,v4)
| ~ r(v4,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_485,plain,
( ( v4 = v0 )
| ( v1 = v4 )
| ( v1 = v0 )
| ~ r(v4,v0)
| ~ r(v1,v4)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_484]) ).
tcf(c_488,plain,
! [X0: $i,X1: $i] :
( r(v2,v4)
| r(v4,X1)
| r(v4,X0)
| r(v2,X1)
| r(v2,X0)
| r(X0,X1)
| ( v4 = X1 )
| ( v4 = X0 )
| ( v2 = v4 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_489,plain,
! [X0: $i] :
( ( v4 = X0 )
| ( v2 = v4 )
| ( v2 = X0 )
| ~ r(v2,v4)
| ~ r(v4,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_490,plain,
( ( v4 = v0 )
| ( v2 = v4 )
| ( v2 = v0 )
| ~ r(v4,v0)
| ~ r(v2,v4)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_489]) ).
tcf(c_493,plain,
! [X0: $i,X1: $i] :
( r(v3,v4)
| r(v4,X1)
| r(v4,X0)
| r(v3,X1)
| r(v3,X0)
| r(X0,X1)
| ( v4 = X1 )
| ( v4 = X0 )
| ( v3 = v4 )
| ( v3 = X1 )
| ( v3 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_494,plain,
! [X0: $i] :
( ( v4 = X0 )
| ( v3 = v4 )
| ( v3 = X0 )
| ~ r(v3,v4)
| ~ r(v4,X0)
| ~ r(v3,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_495,plain,
( ( v4 = v0 )
| ( v3 = v4 )
| ( v3 = v0 )
| ~ r(v4,v0)
| ~ r(v3,v4)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_500,plain,
! [X0: $i] :
( ( v0 = v5 )
| ( v5 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_501,plain,
( ( v0 = v5 )
| ( v5 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i] :
( r(v1,v5)
| r(v5,X1)
| r(v5,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v5 = X1 )
| ( v5 = X0 )
| ( v1 = v5 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_503,plain,
! [X0: $i] :
( ( v5 = X0 )
| ( v1 = v5 )
| ( v1 = X0 )
| ~ r(v1,v5)
| ~ r(v5,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_504,plain,
( ( v5 = v0 )
| ( v1 = v5 )
| ( v1 = v0 )
| ~ r(v5,v0)
| ~ r(v1,v5)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_503]) ).
tcf(c_507,plain,
! [X0: $i,X1: $i] :
( r(v2,v5)
| r(v5,X1)
| r(v5,X0)
| r(v2,X1)
| r(v2,X0)
| r(X0,X1)
| ( v5 = X1 )
| ( v5 = X0 )
| ( v2 = v5 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_508,plain,
! [X0: $i] :
( ( v5 = X0 )
| ( v2 = v5 )
| ( v2 = X0 )
| ~ r(v2,v5)
| ~ r(v5,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_509,plain,
( ( v5 = v0 )
| ( v2 = v5 )
| ( v2 = v0 )
| ~ r(v5,v0)
| ~ r(v2,v5)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_508]) ).
tcf(c_512,plain,
! [X0: $i,X1: $i] :
( r(v3,v5)
| r(v5,X1)
| r(v5,X0)
| r(v3,X1)
| r(v3,X0)
| r(X0,X1)
| ( v5 = X1 )
| ( v5 = X0 )
| ( v3 = v5 )
| ( v3 = X1 )
| ( v3 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_513,plain,
! [X0: $i] :
( ( v5 = X0 )
| ( v3 = v5 )
| ( v3 = X0 )
| ~ r(v3,v5)
| ~ r(v5,X0)
| ~ r(v3,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_514,plain,
( ( v5 = v0 )
| ( v3 = v5 )
| ( v3 = v0 )
| ~ r(v5,v0)
| ~ r(v3,v5)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_517,plain,
! [X0: $i,X1: $i] :
( r(v4,v5)
| r(v5,X1)
| r(v5,X0)
| r(v4,X1)
| r(v4,X0)
| r(X0,X1)
| ( v5 = X1 )
| ( v5 = X0 )
| ( v4 = v5 )
| ( v4 = X1 )
| ( v4 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_518,plain,
! [X0: $i] :
( ( v5 = X0 )
| ( v4 = v5 )
| ( v4 = X0 )
| ~ r(v4,v5)
| ~ r(v5,X0)
| ~ r(v4,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_519,plain,
( ( v5 = v0 )
| ( v4 = v5 )
| ( v4 = v0 )
| ~ r(v5,v0)
| ~ r(v4,v5)
| ~ r(v4,v0) ),
inference(instantiation,[status(thm)],[c_518]) ).
tcf(c_520,plain,
! [X0: $i] :
( ( v4 = v5 )
| ( v5 != X0 )
| ( v4 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_523,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v0 = v6 )
| ( v0 = X0 )
| ~ r(v0,v6)
| ~ r(v6,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_524,plain,
! [X0: $i] :
( ( v0 = v6 )
| ( v6 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_525,plain,
( ( v0 = v6 )
| ( v6 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_524]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i] :
( r(v1,v6)
| r(v6,X1)
| r(v6,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v6 = X1 )
| ( v6 = X0 )
| ( v1 = v6 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_527,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v1 = v6 )
| ( v1 = X0 )
| ~ r(v1,v6)
| ~ r(v6,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_528,plain,
( ( v6 = v0 )
| ( v1 = v6 )
| ( v1 = v0 )
| ~ r(v6,v0)
| ~ r(v1,v6)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_531,plain,
! [X0: $i,X1: $i] :
( r(v2,v6)
| r(v6,X1)
| r(v6,X0)
| r(v2,X1)
| r(v2,X0)
| r(X0,X1)
| ( v6 = X1 )
| ( v6 = X0 )
| ( v2 = v6 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_532,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v2 = v6 )
| ( v2 = X0 )
| ~ r(v2,v6)
| ~ r(v6,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_533,plain,
( ( v6 = v0 )
| ( v2 = v6 )
| ( v2 = v0 )
| ~ r(v6,v0)
| ~ r(v2,v6)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_532]) ).
tcf(c_536,plain,
! [X0: $i,X1: $i] :
( r(v3,v6)
| r(v6,X1)
| r(v6,X0)
| r(v3,X1)
| r(v3,X0)
| r(X0,X1)
| ( v6 = X1 )
| ( v6 = X0 )
| ( v3 = v6 )
| ( v3 = X1 )
| ( v3 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_537,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v3 = v6 )
| ( v3 = X0 )
| ~ r(v3,v6)
| ~ r(v6,X0)
| ~ r(v3,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_538,plain,
( ( v6 = v0 )
| ( v3 = v6 )
| ( v3 = v0 )
| ~ r(v6,v0)
| ~ r(v3,v6)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_541,plain,
! [X0: $i,X1: $i] :
( r(v4,v6)
| r(v6,X1)
| r(v6,X0)
| r(v4,X1)
| r(v4,X0)
| r(X0,X1)
| ( v6 = X1 )
| ( v6 = X0 )
| ( v4 = v6 )
| ( v4 = X1 )
| ( v4 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_542,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v4 = v6 )
| ( v4 = X0 )
| ~ r(v4,v6)
| ~ r(v6,X0)
| ~ r(v4,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_543,plain,
( ( v6 = v0 )
| ( v4 = v6 )
| ( v4 = v0 )
| ~ r(v6,v0)
| ~ r(v4,v6)
| ~ r(v4,v0) ),
inference(instantiation,[status(thm)],[c_542]) ).
tcf(c_546,plain,
! [X0: $i,X1: $i] :
( r(v5,v6)
| r(v6,X1)
| r(v6,X0)
| r(v5,X1)
| r(v5,X0)
| r(X0,X1)
| ( v6 = X1 )
| ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X1 )
| ( v5 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_547,plain,
! [X0: $i] :
( ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X0 )
| ~ r(v5,v6)
| ~ r(v6,X0)
| ~ r(v5,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_548,plain,
( ( v6 = v0 )
| ( v5 = v6 )
| ( v5 = v0 )
| ~ r(v6,v0)
| ~ r(v5,v6)
| ~ r(v5,v0) ),
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_552,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v0 = v7 )
| ( v0 = X0 )
| ~ r(v0,v7)
| ~ r(v7,X0)
| ~ r(v0,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_553,plain,
! [X0: $i] :
( ( v0 = v7 )
| ( v7 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_554,plain,
( ( v0 = v7 )
| ( v7 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_553]) ).
tcf(c_555,plain,
! [X0: $i,X1: $i] :
( r(v1,v7)
| r(v7,X1)
| r(v7,X0)
| r(v1,X1)
| r(v1,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v1 = v7 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_556,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v1 = v7 )
| ( v1 = X0 )
| ~ r(v1,v7)
| ~ r(v7,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_557,plain,
( ( v7 = v0 )
| ( v1 = v7 )
| ( v1 = v0 )
| ~ r(v7,v0)
| ~ r(v1,v7)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_556]) ).
tcf(c_560,plain,
! [X0: $i,X1: $i] :
( r(v2,v7)
| r(v7,X1)
| r(v7,X0)
| r(v2,X1)
| r(v2,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v2 = v7 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_561,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v2 = v7 )
| ( v2 = X0 )
| ~ r(v2,v7)
| ~ r(v7,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_562,plain,
( ( v7 = v0 )
| ( v2 = v7 )
| ( v2 = v0 )
| ~ r(v7,v0)
| ~ r(v2,v7)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_565,plain,
! [X0: $i,X1: $i] :
( r(v3,v7)
| r(v7,X1)
| r(v7,X0)
| r(v3,X1)
| r(v3,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v3 = v7 )
| ( v3 = X1 )
| ( v3 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_566,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v3 = v7 )
| ( v3 = X0 )
| ~ r(v3,v7)
| ~ r(v7,X0)
| ~ r(v3,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_567,plain,
( ( v7 = v0 )
| ( v3 = v7 )
| ( v3 = v0 )
| ~ r(v7,v0)
| ~ r(v3,v7)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_566]) ).
tcf(c_570,plain,
! [X0: $i,X1: $i] :
( r(v4,v7)
| r(v7,X1)
| r(v7,X0)
| r(v4,X1)
| r(v4,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v4 = v7 )
| ( v4 = X1 )
| ( v4 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_571,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v4 = v7 )
| ( v4 = X0 )
| ~ r(v4,v7)
| ~ r(v7,X0)
| ~ r(v4,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_572,plain,
( ( v7 = v0 )
| ( v4 = v7 )
| ( v4 = v0 )
| ~ r(v7,v0)
| ~ r(v4,v7)
| ~ r(v4,v0) ),
inference(instantiation,[status(thm)],[c_571]) ).
tcf(c_575,plain,
! [X0: $i,X1: $i] :
( r(v5,v7)
| r(v7,X1)
| r(v7,X0)
| r(v5,X1)
| r(v5,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X1 )
| ( v5 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_576,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X0 )
| ~ r(v5,v7)
| ~ r(v7,X0)
| ~ r(v5,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_577,plain,
( ( v7 = v0 )
| ( v5 = v7 )
| ( v5 = v0 )
| ~ r(v7,v0)
| ~ r(v5,v7)
| ~ r(v5,v0) ),
inference(instantiation,[status(thm)],[c_576]) ).
tcf(c_580,plain,
! [X0: $i,X1: $i] :
( r(v6,v7)
| r(v7,X1)
| r(v7,X0)
| r(v6,X1)
| r(v6,X0)
| r(X0,X1)
| ( v7 = X1 )
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X1 )
| ( v6 = X0 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_581,plain,
! [X0: $i] :
( ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ~ r(v6,v7)
| ~ r(v7,X0)
| ~ r(v6,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_582,plain,
( ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ~ r(v7,v0)
| ~ r(v6,v7)
| ~ r(v6,v0) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_587,plain,
! [X0: $i] :
( ( v0 = v8 )
| ( v8 != X0 )
| ( v0 != X0 ) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_588,plain,
( ( v0 = v8 )
| ( v8 != v0 )
| ( v0 != v0 ) ),
inference(instantiation,[status(thm)],[c_587]) ).
tcf(c_590,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v1 = v8 )
| ( v1 = X0 )
| ~ r(v1,v8)
| ~ r(v8,X0)
| ~ r(v1,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_591,plain,
( ( v8 = v0 )
| ( v1 = v8 )
| ( v1 = v0 )
| ~ r(v8,v0)
| ~ r(v1,v8)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_590]) ).
tcf(c_595,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v2 = v8 )
| ( v2 = X0 )
| ~ r(v2,v8)
| ~ r(v8,X0)
| ~ r(v2,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_596,plain,
( ( v8 = v0 )
| ( v2 = v8 )
| ( v2 = v0 )
| ~ r(v8,v0)
| ~ r(v2,v8)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_595]) ).
tcf(c_600,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v3 = v8 )
| ( v3 = X0 )
| ~ r(v3,v8)
| ~ r(v8,X0)
| ~ r(v3,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_601,plain,
( ( v8 = v0 )
| ( v3 = v8 )
| ( v3 = v0 )
| ~ r(v8,v0)
| ~ r(v3,v8)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_600]) ).
tcf(c_605,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v4 = v8 )
| ( v4 = X0 )
| ~ r(v4,v8)
| ~ r(v8,X0)
| ~ r(v4,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_606,plain,
( ( v8 = v0 )
| ( v4 = v8 )
| ( v4 = v0 )
| ~ r(v8,v0)
| ~ r(v4,v8)
| ~ r(v4,v0) ),
inference(instantiation,[status(thm)],[c_605]) ).
tcf(c_610,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v5 = v8 )
| ( v5 = X0 )
| ~ r(v5,v8)
| ~ r(v8,X0)
| ~ r(v5,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_611,plain,
( ( v8 = v0 )
| ( v5 = v8 )
| ( v5 = v0 )
| ~ r(v8,v0)
| ~ r(v5,v8)
| ~ r(v5,v0) ),
inference(instantiation,[status(thm)],[c_610]) ).
tcf(c_615,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ~ r(v6,v8)
| ~ r(v8,X0)
| ~ r(v6,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_616,plain,
( ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ~ r(v8,v0)
| ~ r(v6,v8)
| ~ r(v6,v0) ),
inference(instantiation,[status(thm)],[c_615]) ).
tcf(c_620,plain,
! [X0: $i] :
( ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ~ r(v7,v8)
| ~ r(v8,X0)
| ~ r(v7,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_621,plain,
( ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ~ r(v8,v0)
| ~ r(v7,v8)
| ~ r(v7,v0) ),
inference(instantiation,[status(thm)],[c_620]) ).
tcf(c_624,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v1,X2)
| r(v1,X1)
| r(v1,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v1 = X2 )
| ( v1 = X1 )
| ( v1 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_625,plain,
! [X0: $i,X1: $i] :
( ( v1 = X1 )
| ( v1 = X0 )
| ( X0 = X1 )
| ~ r(v1,X1)
| ~ r(v1,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_628,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v2,X2)
| r(v2,X1)
| r(v2,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v2 = X2 )
| ( v2 = X1 )
| ( v2 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_629,plain,
! [X0: $i,X1: $i] :
( ( v2 = X1 )
| ( v2 = X0 )
| ( X0 = X1 )
| ~ r(v2,X1)
| ~ r(v2,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_636,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v3,X2)
| r(v3,X1)
| r(v3,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v3 = X2 )
| ( v3 = X1 )
| ( v3 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i] :
( ( v3 = X1 )
| ( v3 = X0 )
| ( X0 = X1 )
| ~ r(v3,X1)
| ~ r(v3,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_648,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v4,X2)
| r(v4,X1)
| r(v4,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v4 = X2 )
| ( v4 = X1 )
| ( v4 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_649,plain,
! [X0: $i,X1: $i] :
( ( v4 = X1 )
| ( v4 = X0 )
| ( X0 = X1 )
| ~ r(v4,X1)
| ~ r(v4,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_664,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v5,X2)
| r(v5,X1)
| r(v5,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v5 = X2 )
| ( v5 = X1 )
| ( v5 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_665,plain,
! [X0: $i,X1: $i] :
( ( v5 = X1 )
| ( v5 = X0 )
| ( X0 = X1 )
| ~ r(v5,X1)
| ~ r(v5,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_684,plain,
! [X0: $i,X1: $i,X2: $i] :
( r(v6,X2)
| r(v6,X1)
| r(v6,X0)
| r(X1,X2)
| r(X0,X2)
| r(X0,X1)
| ( v6 = X2 )
| ( v6 = X1 )
| ( v6 = X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_685,plain,
! [X0: $i,X1: $i] :
( ( v6 = X1 )
| ( v6 = X0 )
| ( X0 = X1 )
| ~ r(v6,X1)
| ~ r(v6,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_709,plain,
! [X0: $i,X1: $i] :
( ( v7 = X1 )
| ( v7 = X0 )
| ( X0 = X1 )
| ~ r(v7,X1)
| ~ r(v7,X0)
| ~ r(X0,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_776,plain,
( r(v0,v1)
| ~ r(v1,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_827,plain,
( r(v0,v2)
| ~ r(v2,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_829,plain,
( r(v0,v3)
| ~ r(v3,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_832,plain,
( r(v0,v4)
| ~ r(v4,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_839,plain,
( r(v2,v3)
| r(v2,v0)
| r(v1,v3)
| r(v1,v2)
| r(v1,v0)
| r(v0,v3)
| ( v2 = v3 )
| ( v2 = v0 )
| ( v1 = v3 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_842,plain,
( r(v2,v4)
| r(v2,v0)
| r(v1,v4)
| r(v1,v2)
| r(v1,v0)
| r(v0,v4)
| ( v2 = v4 )
| ( v2 = v0 )
| ( v1 = v4 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_845,plain,
( r(v3,v4)
| r(v2,v4)
| r(v2,v3)
| r(v1,v4)
| r(v1,v3)
| r(v1,v2)
| ( v3 = v4 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_846,plain,
( r(v2,v5)
| r(v2,v0)
| r(v1,v5)
| r(v1,v2)
| r(v1,v0)
| r(v0,v5)
| ( v2 = v5 )
| ( v2 = v0 )
| ( v1 = v5 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_849,plain,
( r(v3,v5)
| r(v2,v5)
| r(v2,v3)
| r(v1,v5)
| r(v1,v3)
| r(v1,v2)
| ( v3 = v5 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_850,plain,
( r(v4,v5)
| r(v2,v5)
| r(v2,v4)
| r(v1,v5)
| r(v1,v4)
| r(v1,v2)
| ( v4 = v5 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_851,plain,
( r(v2,v6)
| r(v2,v0)
| r(v1,v6)
| r(v1,v2)
| r(v1,v0)
| r(v0,v6)
| ( v2 = v6 )
| ( v2 = v0 )
| ( v1 = v6 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_854,plain,
( r(v3,v6)
| r(v2,v6)
| r(v2,v3)
| r(v1,v6)
| r(v1,v3)
| r(v1,v2)
| ( v3 = v6 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_855,plain,
( r(v4,v6)
| r(v2,v6)
| r(v2,v4)
| r(v1,v6)
| r(v1,v4)
| r(v1,v2)
| ( v4 = v6 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_856,plain,
( r(v5,v6)
| r(v2,v6)
| r(v2,v5)
| r(v1,v6)
| r(v1,v5)
| r(v1,v2)
| ( v5 = v6 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_857,plain,
( r(v2,v7)
| r(v2,v0)
| r(v1,v7)
| r(v1,v2)
| r(v1,v0)
| r(v0,v7)
| ( v2 = v7 )
| ( v2 = v0 )
| ( v1 = v7 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_860,plain,
( r(v3,v7)
| r(v2,v7)
| r(v2,v3)
| r(v1,v7)
| r(v1,v3)
| r(v1,v2)
| ( v3 = v7 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_861,plain,
( r(v4,v7)
| r(v2,v7)
| r(v2,v4)
| r(v1,v7)
| r(v1,v4)
| r(v1,v2)
| ( v4 = v7 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_862,plain,
( r(v5,v7)
| r(v2,v7)
| r(v2,v5)
| r(v1,v7)
| r(v1,v5)
| r(v1,v2)
| ( v5 = v7 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_863,plain,
( r(v6,v7)
| r(v2,v7)
| r(v2,v6)
| r(v1,v7)
| r(v1,v6)
| r(v1,v2)
| ( v6 = v7 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_864,plain,
( r(v2,v8)
| r(v2,v0)
| r(v1,v8)
| r(v1,v2)
| r(v1,v0)
| r(v0,v8)
| ( v2 = v8 )
| ( v2 = v0 )
| ( v1 = v8 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_867,plain,
( r(v3,v8)
| r(v2,v8)
| r(v2,v3)
| r(v1,v8)
| r(v1,v3)
| r(v1,v2)
| ( v3 = v8 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_868,plain,
( r(v4,v8)
| r(v2,v8)
| r(v2,v4)
| r(v1,v8)
| r(v1,v4)
| r(v1,v2)
| ( v4 = v8 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_869,plain,
( r(v5,v8)
| r(v2,v8)
| r(v2,v5)
| r(v1,v8)
| r(v1,v5)
| r(v1,v2)
| ( v5 = v8 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_870,plain,
( r(v6,v8)
| r(v2,v8)
| r(v2,v6)
| r(v1,v8)
| r(v1,v6)
| r(v1,v2)
| ( v6 = v8 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_871,plain,
( r(v7,v8)
| r(v2,v8)
| r(v2,v7)
| r(v1,v8)
| r(v1,v7)
| r(v1,v2)
| ( v7 = v8 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v2 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_876,plain,
! [X0: $i] :
( r(v2,v3)
| r(v1,v3)
| r(v1,v2)
| r(v3,X0)
| r(v2,X0)
| r(v1,X0)
| ( v3 = X0 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( v1 = v3 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_877,plain,
( r(v3,v0)
| r(v2,v3)
| r(v2,v0)
| r(v1,v3)
| r(v1,v2)
| r(v1,v0)
| ( v3 = v0 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v1 = v3 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_876]) ).
tcf(c_878,plain,
! [X0: $i] :
( r(v2,v4)
| r(v1,v4)
| r(v1,v2)
| r(v4,X0)
| r(v2,X0)
| r(v1,X0)
| ( v4 = X0 )
| ( v2 = v4 )
| ( v2 = X0 )
| ( v1 = v4 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_879,plain,
( r(v4,v0)
| r(v2,v4)
| r(v2,v0)
| r(v1,v4)
| r(v1,v2)
| r(v1,v0)
| ( v4 = v0 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v1 = v4 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_878]) ).
tcf(c_880,plain,
! [X0: $i] :
( r(v2,v5)
| r(v1,v5)
| r(v1,v2)
| r(v5,X0)
| r(v2,X0)
| r(v1,X0)
| ( v5 = X0 )
| ( v2 = v5 )
| ( v2 = X0 )
| ( v1 = v5 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_881,plain,
( r(v5,v0)
| r(v2,v5)
| r(v2,v0)
| r(v1,v5)
| r(v1,v2)
| r(v1,v0)
| ( v5 = v0 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v1 = v5 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_880]) ).
tcf(c_882,plain,
! [X0: $i] :
( r(v2,v6)
| r(v1,v6)
| r(v1,v2)
| r(v6,X0)
| r(v2,X0)
| r(v1,X0)
| ( v6 = X0 )
| ( v2 = v6 )
| ( v2 = X0 )
| ( v1 = v6 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_883,plain,
( r(v6,v0)
| r(v2,v6)
| r(v2,v0)
| r(v1,v6)
| r(v1,v2)
| r(v1,v0)
| ( v6 = v0 )
| ( v2 = v6 )
| ( v2 = v0 )
| ( v1 = v6 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_884,plain,
! [X0: $i] :
( r(v2,v7)
| r(v1,v7)
| r(v1,v2)
| r(v7,X0)
| r(v2,X0)
| r(v1,X0)
| ( v7 = X0 )
| ( v2 = v7 )
| ( v2 = X0 )
| ( v1 = v7 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_885,plain,
( r(v7,v0)
| r(v2,v7)
| r(v2,v0)
| r(v1,v7)
| r(v1,v2)
| r(v1,v0)
| ( v7 = v0 )
| ( v2 = v7 )
| ( v2 = v0 )
| ( v1 = v7 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_884]) ).
tcf(c_886,plain,
! [X0: $i] :
( r(v2,v8)
| r(v1,v8)
| r(v1,v2)
| r(v8,X0)
| r(v2,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v2 = v8 )
| ( v2 = X0 )
| ( v1 = v8 )
| ( v1 = v2 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_887,plain,
( r(v8,v0)
| r(v2,v8)
| r(v2,v0)
| r(v1,v8)
| r(v1,v2)
| r(v1,v0)
| ( v8 = v0 )
| ( v2 = v8 )
| ( v2 = v0 )
| ( v1 = v8 )
| ( v1 = v2 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_886]) ).
tcf(c_986,plain,
( r(v3,v4)
| r(v3,v0)
| r(v1,v4)
| r(v1,v3)
| r(v1,v0)
| r(v0,v4)
| ( v3 = v4 )
| ( v3 = v0 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_990,plain,
( r(v3,v5)
| r(v3,v0)
| r(v1,v5)
| r(v1,v3)
| r(v1,v0)
| r(v0,v5)
| ( v3 = v5 )
| ( v3 = v0 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_994,plain,
( r(v4,v5)
| r(v3,v5)
| r(v3,v4)
| r(v1,v5)
| r(v1,v4)
| r(v1,v3)
| ( v4 = v5 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_995,plain,
( r(v3,v6)
| r(v3,v0)
| r(v1,v6)
| r(v1,v3)
| r(v1,v0)
| r(v0,v6)
| ( v3 = v6 )
| ( v3 = v0 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_999,plain,
( r(v4,v6)
| r(v3,v6)
| r(v3,v4)
| r(v1,v6)
| r(v1,v4)
| r(v1,v3)
| ( v4 = v6 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1000,plain,
( r(v5,v6)
| r(v3,v6)
| r(v3,v5)
| r(v1,v6)
| r(v1,v5)
| r(v1,v3)
| ( v5 = v6 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1001,plain,
( r(v3,v7)
| r(v3,v0)
| r(v1,v7)
| r(v1,v3)
| r(v1,v0)
| r(v0,v7)
| ( v3 = v7 )
| ( v3 = v0 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1005,plain,
( r(v4,v7)
| r(v3,v7)
| r(v3,v4)
| r(v1,v7)
| r(v1,v4)
| r(v1,v3)
| ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1006,plain,
( r(v5,v7)
| r(v3,v7)
| r(v3,v5)
| r(v1,v7)
| r(v1,v5)
| r(v1,v3)
| ( v5 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1007,plain,
( r(v6,v7)
| r(v3,v7)
| r(v3,v6)
| r(v1,v7)
| r(v1,v6)
| r(v1,v3)
| ( v6 = v7 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1008,plain,
( r(v3,v8)
| r(v3,v0)
| r(v1,v8)
| r(v1,v3)
| r(v1,v0)
| r(v0,v8)
| ( v3 = v8 )
| ( v3 = v0 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1012,plain,
( r(v4,v8)
| r(v3,v8)
| r(v3,v4)
| r(v1,v8)
| r(v1,v4)
| r(v1,v3)
| ( v4 = v8 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1013,plain,
( r(v5,v8)
| r(v3,v8)
| r(v3,v5)
| r(v1,v8)
| r(v1,v5)
| r(v1,v3)
| ( v5 = v8 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1014,plain,
( r(v6,v8)
| r(v3,v8)
| r(v3,v6)
| r(v1,v8)
| r(v1,v6)
| r(v1,v3)
| ( v6 = v8 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1015,plain,
( r(v7,v8)
| r(v3,v8)
| r(v3,v7)
| r(v1,v8)
| r(v1,v7)
| r(v1,v3)
| ( v7 = v8 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v3 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1022,plain,
! [X0: $i] :
( r(v3,v4)
| r(v1,v4)
| r(v1,v3)
| r(v4,X0)
| r(v3,X0)
| r(v1,X0)
| ( v4 = X0 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1023,plain,
( r(v4,v0)
| r(v3,v4)
| r(v3,v0)
| r(v1,v4)
| r(v1,v3)
| r(v1,v0)
| ( v4 = v0 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1022]) ).
tcf(c_1024,plain,
! [X0: $i] :
( r(v3,v5)
| r(v1,v5)
| r(v1,v3)
| r(v5,X0)
| r(v3,X0)
| r(v1,X0)
| ( v5 = X0 )
| ( v3 = v5 )
| ( v3 = X0 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1025,plain,
( r(v5,v0)
| r(v3,v5)
| r(v3,v0)
| r(v1,v5)
| r(v1,v3)
| r(v1,v0)
| ( v5 = v0 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1024]) ).
tcf(c_1026,plain,
! [X0: $i] :
( r(v3,v6)
| r(v1,v6)
| r(v1,v3)
| r(v6,X0)
| r(v3,X0)
| r(v1,X0)
| ( v6 = X0 )
| ( v3 = v6 )
| ( v3 = X0 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1027,plain,
( r(v6,v0)
| r(v3,v6)
| r(v3,v0)
| r(v1,v6)
| r(v1,v3)
| r(v1,v0)
| ( v6 = v0 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1026]) ).
tcf(c_1028,plain,
! [X0: $i] :
( r(v3,v7)
| r(v1,v7)
| r(v1,v3)
| r(v7,X0)
| r(v3,X0)
| r(v1,X0)
| ( v7 = X0 )
| ( v3 = v7 )
| ( v3 = X0 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1029,plain,
( r(v7,v0)
| r(v3,v7)
| r(v3,v0)
| r(v1,v7)
| r(v1,v3)
| r(v1,v0)
| ( v7 = v0 )
| ( v3 = v7 )
| ( v3 = v0 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1028]) ).
tcf(c_1030,plain,
! [X0: $i] :
( r(v3,v8)
| r(v1,v8)
| r(v1,v3)
| r(v8,X0)
| r(v3,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v3 = v8 )
| ( v3 = X0 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1031,plain,
( r(v8,v0)
| r(v3,v8)
| r(v3,v0)
| r(v1,v8)
| r(v1,v3)
| r(v1,v0)
| ( v8 = v0 )
| ( v3 = v8 )
| ( v3 = v0 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_1122,plain,
( r(v3,v4)
| r(v3,v0)
| r(v2,v4)
| r(v2,v3)
| r(v2,v0)
| r(v0,v4)
| ( v3 = v4 )
| ( v3 = v0 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1126,plain,
( r(v3,v5)
| r(v3,v0)
| r(v2,v5)
| r(v2,v3)
| r(v2,v0)
| r(v0,v5)
| ( v3 = v5 )
| ( v3 = v0 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1130,plain,
( r(v4,v5)
| r(v3,v5)
| r(v3,v4)
| r(v2,v5)
| r(v2,v4)
| r(v2,v3)
| ( v4 = v5 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1131,plain,
( r(v3,v6)
| r(v3,v0)
| r(v2,v6)
| r(v2,v3)
| r(v2,v0)
| r(v0,v6)
| ( v3 = v6 )
| ( v3 = v0 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1135,plain,
( r(v4,v6)
| r(v3,v6)
| r(v3,v4)
| r(v2,v6)
| r(v2,v4)
| r(v2,v3)
| ( v4 = v6 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1136,plain,
( r(v5,v6)
| r(v3,v6)
| r(v3,v5)
| r(v2,v6)
| r(v2,v5)
| r(v2,v3)
| ( v5 = v6 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1137,plain,
( r(v3,v7)
| r(v3,v0)
| r(v2,v7)
| r(v2,v3)
| r(v2,v0)
| r(v0,v7)
| ( v3 = v7 )
| ( v3 = v0 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1141,plain,
( r(v4,v7)
| r(v3,v7)
| r(v3,v4)
| r(v2,v7)
| r(v2,v4)
| r(v2,v3)
| ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1142,plain,
( r(v5,v7)
| r(v3,v7)
| r(v3,v5)
| r(v2,v7)
| r(v2,v5)
| r(v2,v3)
| ( v5 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1143,plain,
( r(v6,v7)
| r(v3,v7)
| r(v3,v6)
| r(v2,v7)
| r(v2,v6)
| r(v2,v3)
| ( v6 = v7 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1144,plain,
( r(v3,v8)
| r(v3,v0)
| r(v2,v8)
| r(v2,v3)
| r(v2,v0)
| r(v0,v8)
| ( v3 = v8 )
| ( v3 = v0 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1148,plain,
( r(v4,v8)
| r(v3,v8)
| r(v3,v4)
| r(v2,v8)
| r(v2,v4)
| r(v2,v3)
| ( v4 = v8 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1149,plain,
( r(v5,v8)
| r(v3,v8)
| r(v3,v5)
| r(v2,v8)
| r(v2,v5)
| r(v2,v3)
| ( v5 = v8 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1150,plain,
( r(v6,v8)
| r(v3,v8)
| r(v3,v6)
| r(v2,v8)
| r(v2,v6)
| r(v2,v3)
| ( v6 = v8 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1151,plain,
( r(v7,v8)
| r(v3,v8)
| r(v3,v7)
| r(v2,v8)
| r(v2,v7)
| r(v2,v3)
| ( v7 = v8 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v3 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1158,plain,
! [X0: $i] :
( r(v3,v4)
| r(v2,v4)
| r(v2,v3)
| r(v4,X0)
| r(v3,X0)
| r(v2,X0)
| ( v4 = X0 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1159,plain,
( r(v4,v0)
| r(v3,v4)
| r(v3,v0)
| r(v2,v4)
| r(v2,v3)
| r(v2,v0)
| ( v4 = v0 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1158]) ).
tcf(c_1160,plain,
! [X0: $i] :
( r(v3,v5)
| r(v2,v5)
| r(v2,v3)
| r(v5,X0)
| r(v3,X0)
| r(v2,X0)
| ( v5 = X0 )
| ( v3 = v5 )
| ( v3 = X0 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1161,plain,
( r(v5,v0)
| r(v3,v5)
| r(v3,v0)
| r(v2,v5)
| r(v2,v3)
| r(v2,v0)
| ( v5 = v0 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1160]) ).
tcf(c_1162,plain,
! [X0: $i] :
( r(v3,v6)
| r(v2,v6)
| r(v2,v3)
| r(v6,X0)
| r(v3,X0)
| r(v2,X0)
| ( v6 = X0 )
| ( v3 = v6 )
| ( v3 = X0 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1163,plain,
( r(v6,v0)
| r(v3,v6)
| r(v3,v0)
| r(v2,v6)
| r(v2,v3)
| r(v2,v0)
| ( v6 = v0 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1162]) ).
tcf(c_1164,plain,
! [X0: $i] :
( r(v3,v7)
| r(v2,v7)
| r(v2,v3)
| r(v7,X0)
| r(v3,X0)
| r(v2,X0)
| ( v7 = X0 )
| ( v3 = v7 )
| ( v3 = X0 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1165,plain,
( r(v7,v0)
| r(v3,v7)
| r(v3,v0)
| r(v2,v7)
| r(v2,v3)
| r(v2,v0)
| ( v7 = v0 )
| ( v3 = v7 )
| ( v3 = v0 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1164]) ).
tcf(c_1166,plain,
! [X0: $i] :
( r(v3,v8)
| r(v2,v8)
| r(v2,v3)
| r(v8,X0)
| r(v3,X0)
| r(v2,X0)
| ( v8 = X0 )
| ( v3 = v8 )
| ( v3 = X0 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_474]) ).
tcf(c_1167,plain,
( r(v8,v0)
| r(v3,v8)
| r(v3,v0)
| r(v2,v8)
| r(v2,v3)
| r(v2,v0)
| ( v8 = v0 )
| ( v3 = v8 )
| ( v3 = v0 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1166]) ).
tcf(c_1338,plain,
( r(v0,v5)
| ~ r(v5,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1709,plain,
( r(v4,v5)
| ~ r(v5,v4) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1710,plain,
( r(v0,v6)
| ~ r(v6,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1731,plain,
( r(v4,v5)
| r(v4,v0)
| r(v1,v5)
| r(v1,v4)
| r(v1,v0)
| r(v0,v5)
| ( v4 = v5 )
| ( v4 = v0 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1736,plain,
( r(v4,v6)
| r(v4,v0)
| r(v1,v6)
| r(v1,v4)
| r(v1,v0)
| r(v0,v6)
| ( v4 = v6 )
| ( v4 = v0 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1741,plain,
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v1,v6)
| r(v1,v5)
| r(v1,v4)
| ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1742,plain,
( r(v4,v7)
| r(v4,v0)
| r(v1,v7)
| r(v1,v4)
| r(v1,v0)
| r(v0,v7)
| ( v4 = v7 )
| ( v4 = v0 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1746,plain,
( r(v4,v7)
| r(v4,v4)
| r(v1,v7)
| r(v1,v4)
| ( v4 = v7 )
| ( v4 = v4 )
| ( v1 = v7 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1747,plain,
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v1,v7)
| r(v1,v5)
| r(v1,v4)
| ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1748,plain,
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v1,v7)
| r(v1,v6)
| r(v1,v4)
| ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1749,plain,
( r(v4,v8)
| r(v4,v0)
| r(v1,v8)
| r(v1,v4)
| r(v1,v0)
| r(v0,v8)
| ( v4 = v8 )
| ( v4 = v0 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1754,plain,
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v1,v8)
| r(v1,v5)
| r(v1,v4)
| ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1755,plain,
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v1,v8)
| r(v1,v6)
| r(v1,v4)
| ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1756,plain,
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v1,v8)
| r(v1,v7)
| r(v1,v4)
| ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v4 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1765,plain,
! [X0: $i] :
( r(v4,v5)
| r(v1,v5)
| r(v1,v4)
| r(v5,X0)
| r(v4,X0)
| r(v1,X0)
| ( v5 = X0 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1766,plain,
( r(v5,v0)
| r(v4,v5)
| r(v4,v0)
| r(v1,v5)
| r(v1,v4)
| r(v1,v0)
| ( v5 = v0 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1765]) ).
tcf(c_1767,plain,
! [X0: $i] :
( r(v4,v6)
| r(v1,v6)
| r(v1,v4)
| r(v6,X0)
| r(v4,X0)
| r(v1,X0)
| ( v6 = X0 )
| ( v4 = v6 )
| ( v4 = X0 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1768,plain,
( r(v6,v0)
| r(v4,v6)
| r(v4,v0)
| r(v1,v6)
| r(v1,v4)
| r(v1,v0)
| ( v6 = v0 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1767]) ).
tcf(c_1769,plain,
! [X0: $i] :
( r(v4,v7)
| r(v1,v7)
| r(v1,v4)
| r(v7,X0)
| r(v4,X0)
| r(v1,X0)
| ( v7 = X0 )
| ( v4 = v7 )
| ( v4 = X0 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1770,plain,
( r(v7,v0)
| r(v4,v7)
| r(v4,v0)
| r(v1,v7)
| r(v1,v4)
| r(v1,v0)
| ( v7 = v0 )
| ( v4 = v7 )
| ( v4 = v0 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1769]) ).
tcf(c_1771,plain,
! [X0: $i] :
( r(v4,v8)
| r(v1,v8)
| r(v1,v4)
| r(v8,X0)
| r(v4,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v4 = v8 )
| ( v4 = X0 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_483]) ).
tcf(c_1772,plain,
( r(v8,v0)
| r(v4,v8)
| r(v4,v0)
| r(v1,v8)
| r(v1,v4)
| r(v1,v0)
| ( v8 = v0 )
| ( v4 = v8 )
| ( v4 = v0 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1771]) ).
tcf(c_1783,plain,
( r(v4,v5)
| r(v4,v0)
| r(v2,v5)
| r(v2,v4)
| r(v2,v0)
| r(v0,v5)
| ( v4 = v5 )
| ( v4 = v0 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1788,plain,
( r(v4,v6)
| r(v4,v0)
| r(v2,v6)
| r(v2,v4)
| r(v2,v0)
| r(v0,v6)
| ( v4 = v6 )
| ( v4 = v0 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1793,plain,
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v2,v6)
| r(v2,v5)
| r(v2,v4)
| ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1794,plain,
( r(v4,v7)
| r(v4,v0)
| r(v2,v7)
| r(v2,v4)
| r(v2,v0)
| r(v0,v7)
| ( v4 = v7 )
| ( v4 = v0 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1799,plain,
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v2,v7)
| r(v2,v5)
| r(v2,v4)
| ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1800,plain,
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v2,v7)
| r(v2,v6)
| r(v2,v4)
| ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1801,plain,
( r(v4,v8)
| r(v4,v0)
| r(v2,v8)
| r(v2,v4)
| r(v2,v0)
| r(v0,v8)
| ( v4 = v8 )
| ( v4 = v0 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1806,plain,
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v2,v8)
| r(v2,v5)
| r(v2,v4)
| ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1807,plain,
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v2,v8)
| r(v2,v6)
| r(v2,v4)
| ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1808,plain,
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v2,v8)
| r(v2,v7)
| r(v2,v4)
| ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v4 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1817,plain,
! [X0: $i] :
( r(v4,v5)
| r(v2,v5)
| r(v2,v4)
| r(v5,X0)
| r(v4,X0)
| r(v2,X0)
| ( v5 = X0 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1818,plain,
( r(v5,v0)
| r(v4,v5)
| r(v4,v0)
| r(v2,v5)
| r(v2,v4)
| r(v2,v0)
| ( v5 = v0 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1817]) ).
tcf(c_1819,plain,
! [X0: $i] :
( r(v4,v6)
| r(v2,v6)
| r(v2,v4)
| r(v6,X0)
| r(v4,X0)
| r(v2,X0)
| ( v6 = X0 )
| ( v4 = v6 )
| ( v4 = X0 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1820,plain,
( r(v6,v0)
| r(v4,v6)
| r(v4,v0)
| r(v2,v6)
| r(v2,v4)
| r(v2,v0)
| ( v6 = v0 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1819]) ).
tcf(c_1821,plain,
! [X0: $i] :
( r(v4,v7)
| r(v2,v7)
| r(v2,v4)
| r(v7,X0)
| r(v4,X0)
| r(v2,X0)
| ( v7 = X0 )
| ( v4 = v7 )
| ( v4 = X0 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1822,plain,
( r(v7,v0)
| r(v4,v7)
| r(v4,v0)
| r(v2,v7)
| r(v2,v4)
| r(v2,v0)
| ( v7 = v0 )
| ( v4 = v7 )
| ( v4 = v0 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1821]) ).
tcf(c_1823,plain,
! [X0: $i] :
( r(v4,v8)
| r(v2,v8)
| r(v2,v4)
| r(v8,X0)
| r(v4,X0)
| r(v2,X0)
| ( v8 = X0 )
| ( v4 = v8 )
| ( v4 = X0 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_1824,plain,
( r(v8,v0)
| r(v4,v8)
| r(v4,v0)
| r(v2,v8)
| r(v2,v4)
| r(v2,v0)
| ( v8 = v0 )
| ( v4 = v8 )
| ( v4 = v0 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1823]) ).
tcf(c_1835,plain,
( r(v4,v5)
| r(v4,v0)
| r(v3,v5)
| r(v3,v4)
| r(v3,v0)
| r(v0,v5)
| ( v4 = v5 )
| ( v4 = v0 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1840,plain,
( r(v4,v6)
| r(v4,v0)
| r(v3,v6)
| r(v3,v4)
| r(v3,v0)
| r(v0,v6)
| ( v4 = v6 )
| ( v4 = v0 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1845,plain,
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v3,v6)
| r(v3,v5)
| r(v3,v4)
| ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1846,plain,
( r(v4,v7)
| r(v4,v0)
| r(v3,v7)
| r(v3,v4)
| r(v3,v0)
| r(v0,v7)
| ( v4 = v7 )
| ( v4 = v0 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1851,plain,
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v3,v7)
| r(v3,v5)
| r(v3,v4)
| ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1852,plain,
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v3,v7)
| r(v3,v6)
| r(v3,v4)
| ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1853,plain,
( r(v4,v8)
| r(v4,v0)
| r(v3,v8)
| r(v3,v4)
| r(v3,v0)
| r(v0,v8)
| ( v4 = v8 )
| ( v4 = v0 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1858,plain,
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v3,v8)
| r(v3,v5)
| r(v3,v4)
| ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1859,plain,
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v3,v8)
| r(v3,v6)
| r(v3,v4)
| ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1860,plain,
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v3,v8)
| r(v3,v7)
| r(v3,v4)
| ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1869,plain,
! [X0: $i] :
( r(v4,v5)
| r(v3,v5)
| r(v3,v4)
| r(v5,X0)
| r(v4,X0)
| r(v3,X0)
| ( v5 = X0 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1870,plain,
( r(v5,v0)
| r(v4,v5)
| r(v4,v0)
| r(v3,v5)
| r(v3,v4)
| r(v3,v0)
| ( v5 = v0 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_1869]) ).
tcf(c_1871,plain,
! [X0: $i] :
( r(v4,v6)
| r(v3,v6)
| r(v3,v4)
| r(v6,X0)
| r(v4,X0)
| r(v3,X0)
| ( v6 = X0 )
| ( v4 = v6 )
| ( v4 = X0 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1872,plain,
( r(v6,v0)
| r(v4,v6)
| r(v4,v0)
| r(v3,v6)
| r(v3,v4)
| r(v3,v0)
| ( v6 = v0 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_1871]) ).
tcf(c_1873,plain,
! [X0: $i] :
( r(v4,v7)
| r(v3,v7)
| r(v3,v4)
| r(v7,X0)
| r(v4,X0)
| r(v3,X0)
| ( v7 = X0 )
| ( v4 = v7 )
| ( v4 = X0 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1874,plain,
( r(v7,v0)
| r(v4,v7)
| r(v4,v0)
| r(v3,v7)
| r(v3,v4)
| r(v3,v0)
| ( v7 = v0 )
| ( v4 = v7 )
| ( v4 = v0 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_1873]) ).
tcf(c_1875,plain,
! [X0: $i] :
( r(v4,v8)
| r(v3,v8)
| r(v3,v4)
| r(v8,X0)
| r(v4,X0)
| r(v3,X0)
| ( v8 = X0 )
| ( v4 = v8 )
| ( v4 = X0 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_493]) ).
tcf(c_1876,plain,
( r(v8,v0)
| r(v4,v8)
| r(v4,v0)
| r(v3,v8)
| r(v3,v4)
| r(v3,v0)
| ( v8 = v0 )
| ( v4 = v8 )
| ( v4 = v0 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_1880,plain,
( r(v0,v7)
| ~ r(v7,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1908,plain,
( r(v5,v6)
| r(v5,v0)
| r(v1,v6)
| r(v1,v5)
| r(v1,v0)
| r(v0,v6)
| ( v5 = v6 )
| ( v5 = v0 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1914,plain,
( r(v5,v7)
| r(v5,v0)
| r(v1,v7)
| r(v1,v5)
| r(v1,v0)
| r(v0,v7)
| ( v5 = v7 )
| ( v5 = v0 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1920,plain,
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v1,v7)
| r(v1,v6)
| r(v1,v5)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v5 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1921,plain,
( r(v5,v8)
| r(v5,v0)
| r(v1,v8)
| r(v1,v5)
| r(v1,v0)
| r(v0,v8)
| ( v5 = v8 )
| ( v5 = v0 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1927,plain,
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v1,v8)
| r(v1,v6)
| r(v1,v5)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v5 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1928,plain,
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v1,v8)
| r(v1,v7)
| r(v1,v5)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v5 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1935,plain,
! [X0: $i] :
( r(v5,v4)
| r(v1,v5)
| r(v1,v4)
| r(v5,X0)
| r(v4,X0)
| r(v1,X0)
| ( v5 = v4 )
| ( v5 = X0 )
| ( v4 = X0 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1936,plain,
( r(v5,v4)
| r(v5,v0)
| r(v4,v0)
| r(v1,v5)
| r(v1,v4)
| r(v1,v0)
| ( v5 = v4 )
| ( v5 = v0 )
| ( v4 = v0 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1935]) ).
tcf(c_1939,plain,
! [X0: $i] :
( r(v5,v6)
| r(v1,v6)
| r(v1,v5)
| r(v6,X0)
| r(v5,X0)
| r(v1,X0)
| ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1940,plain,
( r(v6,v0)
| r(v5,v6)
| r(v5,v0)
| r(v1,v6)
| r(v1,v5)
| r(v1,v0)
| ( v6 = v0 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1939]) ).
tcf(c_1941,plain,
! [X0: $i] :
( r(v5,v7)
| r(v1,v7)
| r(v1,v5)
| r(v7,X0)
| r(v5,X0)
| r(v1,X0)
| ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X0 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1942,plain,
( r(v7,v0)
| r(v5,v7)
| r(v5,v0)
| r(v1,v7)
| r(v1,v5)
| r(v1,v0)
| ( v7 = v0 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1941]) ).
tcf(c_1943,plain,
! [X0: $i] :
( r(v5,v8)
| r(v1,v8)
| r(v1,v5)
| r(v8,X0)
| r(v5,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v5 = v8 )
| ( v5 = X0 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_1944,plain,
( r(v8,v0)
| r(v5,v8)
| r(v5,v0)
| r(v1,v8)
| r(v1,v5)
| r(v1,v0)
| ( v8 = v0 )
| ( v5 = v8 )
| ( v5 = v0 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_1960,plain,
( r(v5,v6)
| r(v5,v0)
| r(v2,v6)
| r(v2,v5)
| r(v2,v0)
| r(v0,v6)
| ( v5 = v6 )
| ( v5 = v0 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1966,plain,
( r(v5,v7)
| r(v5,v0)
| r(v2,v7)
| r(v2,v5)
| r(v2,v0)
| r(v0,v7)
| ( v5 = v7 )
| ( v5 = v0 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1972,plain,
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v2,v7)
| r(v2,v6)
| r(v2,v5)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v5 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1973,plain,
( r(v5,v8)
| r(v5,v0)
| r(v2,v8)
| r(v2,v5)
| r(v2,v0)
| r(v0,v8)
| ( v5 = v8 )
| ( v5 = v0 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1979,plain,
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v2,v8)
| r(v2,v6)
| r(v2,v5)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v5 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1980,plain,
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v2,v8)
| r(v2,v7)
| r(v2,v5)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v5 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1991,plain,
! [X0: $i] :
( r(v5,v6)
| r(v2,v6)
| r(v2,v5)
| r(v6,X0)
| r(v5,X0)
| r(v2,X0)
| ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1992,plain,
( r(v6,v0)
| r(v5,v6)
| r(v5,v0)
| r(v2,v6)
| r(v2,v5)
| r(v2,v0)
| ( v6 = v0 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1991]) ).
tcf(c_1993,plain,
! [X0: $i] :
( r(v5,v7)
| r(v2,v7)
| r(v2,v5)
| r(v7,X0)
| r(v5,X0)
| r(v2,X0)
| ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X0 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1994,plain,
( r(v7,v0)
| r(v5,v7)
| r(v5,v0)
| r(v2,v7)
| r(v2,v5)
| r(v2,v0)
| ( v7 = v0 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1993]) ).
tcf(c_1995,plain,
! [X0: $i] :
( r(v5,v8)
| r(v2,v8)
| r(v2,v5)
| r(v8,X0)
| r(v5,X0)
| r(v2,X0)
| ( v8 = X0 )
| ( v5 = v8 )
| ( v5 = X0 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_507]) ).
tcf(c_1996,plain,
( r(v8,v0)
| r(v5,v8)
| r(v5,v0)
| r(v2,v8)
| r(v2,v5)
| r(v2,v0)
| ( v8 = v0 )
| ( v5 = v8 )
| ( v5 = v0 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_1995]) ).
tcf(c_2012,plain,
( r(v5,v6)
| r(v5,v0)
| r(v3,v6)
| r(v3,v5)
| r(v3,v0)
| r(v0,v6)
| ( v5 = v6 )
| ( v5 = v0 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2018,plain,
( r(v5,v7)
| r(v5,v0)
| r(v3,v7)
| r(v3,v5)
| r(v3,v0)
| r(v0,v7)
| ( v5 = v7 )
| ( v5 = v0 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2022,plain,
( r(v5,v7)
| r(v5,v4)
| r(v4,v7)
| r(v3,v7)
| r(v3,v5)
| r(v3,v4)
| ( v5 = v7 )
| ( v5 = v4 )
| ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = v4 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2024,plain,
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v3,v7)
| r(v3,v6)
| r(v3,v5)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = v5 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2025,plain,
( r(v5,v8)
| r(v5,v0)
| r(v3,v8)
| r(v3,v5)
| r(v3,v0)
| r(v0,v8)
| ( v5 = v8 )
| ( v5 = v0 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2031,plain,
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v3,v8)
| r(v3,v6)
| r(v3,v5)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = v5 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2032,plain,
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v3,v8)
| r(v3,v7)
| r(v3,v5)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v5 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2039,plain,
! [X0: $i] :
( r(v5,v4)
| r(v3,v5)
| r(v3,v4)
| r(v5,X0)
| r(v4,X0)
| r(v3,X0)
| ( v5 = v4 )
| ( v5 = X0 )
| ( v4 = X0 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2040,plain,
( r(v5,v4)
| r(v5,v0)
| r(v4,v0)
| r(v3,v5)
| r(v3,v4)
| r(v3,v0)
| ( v5 = v4 )
| ( v5 = v0 )
| ( v4 = v0 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_2039]) ).
tcf(c_2043,plain,
! [X0: $i] :
( r(v5,v6)
| r(v3,v6)
| r(v3,v5)
| r(v6,X0)
| r(v5,X0)
| r(v3,X0)
| ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2044,plain,
( r(v6,v0)
| r(v5,v6)
| r(v5,v0)
| r(v3,v6)
| r(v3,v5)
| r(v3,v0)
| ( v6 = v0 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_2043]) ).
tcf(c_2045,plain,
! [X0: $i] :
( r(v5,v7)
| r(v3,v7)
| r(v3,v5)
| r(v7,X0)
| r(v5,X0)
| r(v3,X0)
| ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X0 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2046,plain,
( r(v7,v0)
| r(v5,v7)
| r(v5,v0)
| r(v3,v7)
| r(v3,v5)
| r(v3,v0)
| ( v7 = v0 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_2045]) ).
tcf(c_2047,plain,
! [X0: $i] :
( r(v5,v8)
| r(v3,v8)
| r(v3,v5)
| r(v8,X0)
| r(v5,X0)
| r(v3,X0)
| ( v8 = X0 )
| ( v5 = v8 )
| ( v5 = X0 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_2048,plain,
( r(v8,v0)
| r(v5,v8)
| r(v5,v0)
| r(v3,v8)
| r(v3,v5)
| r(v3,v0)
| ( v8 = v0 )
| ( v5 = v8 )
| ( v5 = v0 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_2047]) ).
tcf(c_2135,plain,
( r(v0,v8)
| ~ r(v8,v0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2198,plain,
( r(v5,v6)
| r(v5,v0)
| r(v4,v6)
| r(v4,v5)
| r(v4,v0)
| r(v0,v6)
| ( v5 = v6 )
| ( v5 = v0 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2204,plain,
( r(v5,v7)
| r(v5,v0)
| r(v4,v7)
| r(v4,v5)
| r(v4,v0)
| r(v0,v7)
| ( v5 = v7 )
| ( v5 = v0 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2210,plain,
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v4,v7)
| r(v4,v6)
| r(v4,v5)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = v5 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2211,plain,
( r(v5,v8)
| r(v5,v0)
| r(v4,v8)
| r(v4,v5)
| r(v4,v0)
| r(v0,v8)
| ( v5 = v8 )
| ( v5 = v0 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2217,plain,
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v4,v8)
| r(v4,v6)
| r(v4,v5)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = v5 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2218,plain,
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v4,v8)
| r(v4,v7)
| r(v4,v5)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = v5 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2229,plain,
! [X0: $i] :
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v6,X0)
| r(v5,X0)
| r(v4,X0)
| ( v6 = X0 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2230,plain,
( r(v6,v0)
| r(v5,v6)
| r(v5,v0)
| r(v4,v6)
| r(v4,v5)
| r(v4,v0)
| ( v6 = v0 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_2229]) ).
tcf(c_2231,plain,
! [X0: $i] :
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v7,X0)
| r(v5,X0)
| r(v4,X0)
| ( v7 = X0 )
| ( v5 = v7 )
| ( v5 = X0 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2232,plain,
( r(v7,v0)
| r(v5,v7)
| r(v5,v0)
| r(v4,v7)
| r(v4,v5)
| r(v4,v0)
| ( v7 = v0 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_2231]) ).
tcf(c_2233,plain,
! [X0: $i] :
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v8,X0)
| r(v5,X0)
| r(v4,X0)
| ( v8 = X0 )
| ( v5 = v8 )
| ( v5 = X0 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_517]) ).
tcf(c_2234,plain,
( r(v8,v0)
| r(v5,v8)
| r(v5,v0)
| r(v4,v8)
| r(v4,v5)
| r(v4,v0)
| ( v8 = v0 )
| ( v5 = v8 )
| ( v5 = v0 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_2233]) ).
tcf(c_2558,plain,
( r(v6,v7)
| r(v6,v0)
| r(v1,v7)
| r(v1,v6)
| r(v1,v0)
| r(v0,v7)
| ( v6 = v7 )
| ( v6 = v0 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2565,plain,
( r(v6,v8)
| r(v6,v0)
| r(v1,v8)
| r(v1,v6)
| r(v1,v0)
| r(v0,v8)
| ( v6 = v8 )
| ( v6 = v0 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2572,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v1,v8)
| r(v1,v7)
| r(v1,v6)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v6 ) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2585,plain,
! [X0: $i] :
( r(v6,v7)
| r(v1,v7)
| r(v1,v6)
| r(v7,X0)
| r(v6,X0)
| r(v1,X0)
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2586,plain,
( r(v7,v0)
| r(v6,v7)
| r(v6,v0)
| r(v1,v7)
| r(v1,v6)
| r(v1,v0)
| ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_2585]) ).
tcf(c_2587,plain,
! [X0: $i] :
( r(v6,v8)
| r(v1,v8)
| r(v1,v6)
| r(v8,X0)
| r(v6,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_2588,plain,
( r(v8,v0)
| r(v6,v8)
| r(v6,v0)
| r(v1,v8)
| r(v1,v6)
| r(v1,v0)
| ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_2587]) ).
tcf(c_3120,plain,
( r(v6,v7)
| r(v6,v0)
| r(v2,v7)
| r(v2,v6)
| r(v2,v0)
| r(v0,v7)
| ( v6 = v7 )
| ( v6 = v0 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_3127,plain,
( r(v6,v8)
| r(v6,v0)
| r(v2,v8)
| r(v2,v6)
| r(v2,v0)
| r(v0,v8)
| ( v6 = v8 )
| ( v6 = v0 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_3134,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v2,v8)
| r(v2,v7)
| r(v2,v6)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v6 ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_3147,plain,
! [X0: $i] :
( r(v6,v7)
| r(v2,v7)
| r(v2,v6)
| r(v7,X0)
| r(v6,X0)
| r(v2,X0)
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_3148,plain,
( r(v7,v0)
| r(v6,v7)
| r(v6,v0)
| r(v2,v7)
| r(v2,v6)
| r(v2,v0)
| ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_3147]) ).
tcf(c_3149,plain,
! [X0: $i] :
( r(v6,v8)
| r(v2,v8)
| r(v2,v6)
| r(v8,X0)
| r(v6,X0)
| r(v2,X0)
| ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_3150,plain,
( r(v8,v0)
| r(v6,v8)
| r(v6,v0)
| r(v2,v8)
| r(v2,v6)
| r(v2,v0)
| ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_3149]) ).
tcf(c_3174,plain,
( r(v6,v7)
| r(v6,v0)
| r(v3,v7)
| r(v3,v6)
| r(v3,v0)
| r(v0,v7)
| ( v6 = v7 )
| ( v6 = v0 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_3181,plain,
( r(v6,v8)
| r(v6,v0)
| r(v3,v8)
| r(v3,v6)
| r(v3,v0)
| r(v0,v8)
| ( v6 = v8 )
| ( v6 = v0 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_3188,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v3,v8)
| r(v3,v7)
| r(v3,v6)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v6 ) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_3201,plain,
! [X0: $i] :
( r(v6,v7)
| r(v3,v7)
| r(v3,v6)
| r(v7,X0)
| r(v6,X0)
| r(v3,X0)
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_3202,plain,
( r(v7,v0)
| r(v6,v7)
| r(v6,v0)
| r(v3,v7)
| r(v3,v6)
| r(v3,v0)
| ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_3201]) ).
tcf(c_3203,plain,
! [X0: $i] :
( r(v6,v8)
| r(v3,v8)
| r(v3,v6)
| r(v8,X0)
| r(v6,X0)
| r(v3,X0)
| ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_3204,plain,
( r(v8,v0)
| r(v6,v8)
| r(v6,v0)
| r(v3,v8)
| r(v3,v6)
| r(v3,v0)
| ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_3203]) ).
tcf(c_3226,plain,
( r(v6,v7)
| r(v6,v0)
| r(v4,v7)
| r(v4,v6)
| r(v4,v0)
| r(v0,v7)
| ( v6 = v7 )
| ( v6 = v0 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_3233,plain,
( r(v6,v8)
| r(v6,v0)
| r(v4,v8)
| r(v4,v6)
| r(v4,v0)
| r(v0,v8)
| ( v6 = v8 )
| ( v6 = v0 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_3240,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v4,v8)
| r(v4,v7)
| r(v4,v6)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = v6 ) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_3253,plain,
! [X0: $i] :
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v7,X0)
| r(v6,X0)
| r(v4,X0)
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_3254,plain,
( r(v7,v0)
| r(v6,v7)
| r(v6,v0)
| r(v4,v7)
| r(v4,v6)
| r(v4,v0)
| ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_3253]) ).
tcf(c_3255,plain,
! [X0: $i] :
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v8,X0)
| r(v6,X0)
| r(v4,X0)
| ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_541]) ).
tcf(c_3256,plain,
( r(v8,v0)
| r(v6,v8)
| r(v6,v0)
| r(v4,v8)
| r(v4,v6)
| r(v4,v0)
| ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_3255]) ).
tcf(c_3278,plain,
( r(v6,v7)
| r(v6,v0)
| r(v5,v7)
| r(v5,v6)
| r(v5,v0)
| r(v0,v7)
| ( v6 = v7 )
| ( v6 = v0 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_3285,plain,
( r(v6,v8)
| r(v6,v0)
| r(v5,v8)
| r(v5,v6)
| r(v5,v0)
| r(v0,v8)
| ( v6 = v8 )
| ( v6 = v0 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_3292,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v5,v8)
| r(v5,v7)
| r(v5,v6)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = v6 ) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_3305,plain,
! [X0: $i] :
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v7,X0)
| r(v6,X0)
| r(v5,X0)
| ( v7 = X0 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v5 = X0 ) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_3306,plain,
( r(v7,v0)
| r(v6,v7)
| r(v6,v0)
| r(v5,v7)
| r(v5,v6)
| r(v5,v0)
| ( v7 = v0 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v5 = v0 ) ),
inference(instantiation,[status(thm)],[c_3305]) ).
tcf(c_3307,plain,
! [X0: $i] :
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v8,X0)
| r(v6,X0)
| r(v5,X0)
| ( v8 = X0 )
| ( v6 = v8 )
| ( v6 = X0 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v5 = X0 ) ),
inference(instantiation,[status(thm)],[c_546]) ).
tcf(c_3308,plain,
( r(v8,v0)
| r(v6,v8)
| r(v6,v0)
| r(v5,v8)
| r(v5,v6)
| r(v5,v0)
| ( v8 = v0 )
| ( v6 = v8 )
| ( v6 = v0 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v5 = v0 ) ),
inference(instantiation,[status(thm)],[c_3307]) ).
tcf(c_3345,plain,
( r(v7,v8)
| r(v7,v0)
| r(v1,v8)
| r(v1,v7)
| r(v1,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_555]) ).
tcf(c_3367,plain,
! [X0: $i] :
( r(v7,v8)
| r(v1,v8)
| r(v1,v7)
| r(v8,X0)
| r(v7,X0)
| r(v1,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = X0 ) ),
inference(instantiation,[status(thm)],[c_555]) ).
tcf(c_3368,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v1,v8)
| r(v1,v7)
| r(v1,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v0 ) ),
inference(instantiation,[status(thm)],[c_3367]) ).
tcf(c_4447,plain,
( r(v7,v8)
| r(v7,v0)
| r(v2,v8)
| r(v2,v7)
| r(v2,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_560]) ).
tcf(c_4469,plain,
! [X0: $i] :
( r(v7,v8)
| r(v2,v8)
| r(v2,v7)
| r(v8,X0)
| r(v7,X0)
| r(v2,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = X0 ) ),
inference(instantiation,[status(thm)],[c_560]) ).
tcf(c_4470,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v2,v8)
| r(v2,v7)
| r(v2,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v0 ) ),
inference(instantiation,[status(thm)],[c_4469]) ).
tcf(c_5273,plain,
( r(v7,v8)
| r(v7,v0)
| r(v3,v8)
| r(v3,v7)
| r(v3,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_565]) ).
tcf(c_5295,plain,
! [X0: $i] :
( r(v7,v8)
| r(v3,v8)
| r(v3,v7)
| r(v8,X0)
| r(v7,X0)
| r(v3,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = X0 ) ),
inference(instantiation,[status(thm)],[c_565]) ).
tcf(c_5296,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v3,v8)
| r(v3,v7)
| r(v3,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v0 ) ),
inference(instantiation,[status(thm)],[c_5295]) ).
tcf(c_5325,plain,
( r(v7,v8)
| r(v7,v0)
| r(v4,v8)
| r(v4,v7)
| r(v4,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_570]) ).
tcf(c_5347,plain,
! [X0: $i] :
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v8,X0)
| r(v7,X0)
| r(v4,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = X0 ) ),
inference(instantiation,[status(thm)],[c_570]) ).
tcf(c_5348,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v4,v8)
| r(v4,v7)
| r(v4,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = v0 ) ),
inference(instantiation,[status(thm)],[c_5347]) ).
tcf(c_5377,plain,
( r(v7,v8)
| r(v7,v0)
| r(v5,v8)
| r(v5,v7)
| r(v5,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_575]) ).
tcf(c_5399,plain,
! [X0: $i] :
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v8,X0)
| r(v7,X0)
| r(v5,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = X0 ) ),
inference(instantiation,[status(thm)],[c_575]) ).
tcf(c_5400,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v5,v8)
| r(v5,v7)
| r(v5,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = v0 ) ),
inference(instantiation,[status(thm)],[c_5399]) ).
tcf(c_5429,plain,
( r(v7,v8)
| r(v7,v0)
| r(v6,v8)
| r(v6,v7)
| r(v6,v0)
| r(v0,v8)
| ( v7 = v8 )
| ( v7 = v0 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v0 = v8 ) ),
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_5451,plain,
! [X0: $i] :
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v8,X0)
| r(v7,X0)
| r(v6,X0)
| ( v8 = X0 )
| ( v7 = v8 )
| ( v7 = X0 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v6 = X0 ) ),
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_5452,plain,
( r(v8,v0)
| r(v7,v8)
| r(v7,v0)
| r(v6,v8)
| r(v6,v7)
| r(v6,v0)
| ( v8 = v0 )
| ( v7 = v8 )
| ( v7 = v0 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v6 = v0 ) ),
inference(instantiation,[status(thm)],[c_5451]) ).
tcf(c_5454,plain,
( r(v2,v0)
| ~ r(v0,v2) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5456,plain,
( r(v3,v0)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5459,plain,
( r(v4,v0)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5563,plain,
( r(v5,v0)
| ~ r(v0,v5) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5567,plain,
( r(v5,v4)
| ~ r(v4,v5) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5568,plain,
( r(v6,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5674,plain,
( r(v7,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5685,plain,
! [X0: $i] :
( r(v2,v3)
| r(v1,v3)
| r(v1,v2)
| r(v1,X0)
| r(X0,v3)
| r(X0,v2)
| ( v2 = v3 )
| ( v1 = v3 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v3 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5686,plain,
( r(v2,v3)
| r(v1,v3)
| r(v1,v2)
| r(v1,v0)
| r(v0,v3)
| r(v0,v2)
| ( v2 = v3 )
| ( v1 = v3 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v3 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5685]) ).
tcf(c_5690,plain,
! [X0: $i] :
( r(v2,v4)
| r(v1,v4)
| r(v1,v2)
| r(v1,X0)
| r(X0,v4)
| r(X0,v2)
| ( v2 = v4 )
| ( v1 = v4 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v4 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5691,plain,
( r(v2,v4)
| r(v1,v4)
| r(v1,v2)
| r(v1,v0)
| r(v0,v4)
| r(v0,v2)
| ( v2 = v4 )
| ( v1 = v4 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v4 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5690]) ).
tcf(c_5692,plain,
! [X0: $i] :
( r(v3,v4)
| r(v1,v4)
| r(v1,v3)
| r(v1,X0)
| r(X0,v4)
| r(X0,v3)
| ( v3 = v4 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v4 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5693,plain,
( r(v3,v4)
| r(v1,v4)
| r(v1,v3)
| r(v1,v0)
| r(v0,v4)
| r(v0,v3)
| ( v3 = v4 )
| ( v1 = v4 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v4 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5692]) ).
tcf(c_5697,plain,
! [X0: $i] :
( r(v2,v5)
| r(v1,v5)
| r(v1,v2)
| r(v1,X0)
| r(X0,v5)
| r(X0,v2)
| ( v2 = v5 )
| ( v1 = v5 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v5 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5698,plain,
( r(v2,v5)
| r(v1,v5)
| r(v1,v2)
| r(v1,v0)
| r(v0,v5)
| r(v0,v2)
| ( v2 = v5 )
| ( v1 = v5 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v5 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5697]) ).
tcf(c_5699,plain,
! [X0: $i] :
( r(v3,v5)
| r(v1,v5)
| r(v1,v3)
| r(v1,X0)
| r(X0,v5)
| r(X0,v3)
| ( v3 = v5 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v5 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5700,plain,
( r(v3,v5)
| r(v1,v5)
| r(v1,v3)
| r(v1,v0)
| r(v0,v5)
| r(v0,v3)
| ( v3 = v5 )
| ( v1 = v5 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v5 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5699]) ).
tcf(c_5701,plain,
! [X0: $i] :
( r(v4,v5)
| r(v1,v5)
| r(v1,v4)
| r(v1,X0)
| r(X0,v5)
| r(X0,v4)
| ( v4 = v5 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = X0 )
| ( X0 = v5 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5702,plain,
( r(v4,v5)
| r(v1,v5)
| r(v1,v4)
| r(v1,v0)
| r(v0,v5)
| r(v0,v4)
| ( v4 = v5 )
| ( v1 = v5 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v5 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5701]) ).
tcf(c_5706,plain,
! [X0: $i] :
( r(v2,v6)
| r(v1,v6)
| r(v1,v2)
| r(v1,X0)
| r(X0,v6)
| r(X0,v2)
| ( v2 = v6 )
| ( v1 = v6 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v6 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5707,plain,
( r(v2,v6)
| r(v1,v6)
| r(v1,v2)
| r(v1,v0)
| r(v0,v6)
| r(v0,v2)
| ( v2 = v6 )
| ( v1 = v6 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v6 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5706]) ).
tcf(c_5708,plain,
! [X0: $i] :
( r(v3,v6)
| r(v1,v6)
| r(v1,v3)
| r(v1,X0)
| r(X0,v6)
| r(X0,v3)
| ( v3 = v6 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v6 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5709,plain,
( r(v3,v6)
| r(v1,v6)
| r(v1,v3)
| r(v1,v0)
| r(v0,v6)
| r(v0,v3)
| ( v3 = v6 )
| ( v1 = v6 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v6 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5708]) ).
tcf(c_5710,plain,
! [X0: $i] :
( r(v4,v6)
| r(v1,v6)
| r(v1,v4)
| r(v1,X0)
| r(X0,v6)
| r(X0,v4)
| ( v4 = v6 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = X0 )
| ( X0 = v6 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5711,plain,
( r(v4,v6)
| r(v1,v6)
| r(v1,v4)
| r(v1,v0)
| r(v0,v6)
| r(v0,v4)
| ( v4 = v6 )
| ( v1 = v6 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v6 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5710]) ).
tcf(c_5712,plain,
! [X0: $i] :
( r(v5,v6)
| r(v1,v6)
| r(v1,v5)
| r(v1,X0)
| r(X0,v6)
| r(X0,v5)
| ( v5 = v6 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = X0 )
| ( X0 = v6 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5713,plain,
( r(v5,v6)
| r(v1,v6)
| r(v1,v5)
| r(v1,v0)
| r(v0,v6)
| r(v0,v5)
| ( v5 = v6 )
| ( v1 = v6 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v6 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5712]) ).
tcf(c_5717,plain,
! [X0: $i] :
( r(v2,v7)
| r(v1,v7)
| r(v1,v2)
| r(v1,X0)
| r(X0,v7)
| r(X0,v2)
| ( v2 = v7 )
| ( v1 = v7 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v7 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5718,plain,
( r(v2,v7)
| r(v1,v7)
| r(v1,v2)
| r(v1,v0)
| r(v0,v7)
| r(v0,v2)
| ( v2 = v7 )
| ( v1 = v7 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v7 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5717]) ).
tcf(c_5719,plain,
! [X0: $i] :
( r(v3,v7)
| r(v1,v7)
| r(v1,v3)
| r(v1,X0)
| r(X0,v7)
| r(X0,v3)
| ( v3 = v7 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v7 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5720,plain,
( r(v3,v7)
| r(v1,v7)
| r(v1,v3)
| r(v1,v0)
| r(v0,v7)
| r(v0,v3)
| ( v3 = v7 )
| ( v1 = v7 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v7 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5719]) ).
tcf(c_5721,plain,
! [X0: $i] :
( r(v4,v7)
| r(v1,v7)
| r(v1,v4)
| r(v1,X0)
| r(X0,v7)
| r(X0,v4)
| ( v4 = v7 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = X0 )
| ( X0 = v7 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5722,plain,
( r(v4,v7)
| r(v1,v7)
| r(v1,v4)
| r(v1,v0)
| r(v0,v7)
| r(v0,v4)
| ( v4 = v7 )
| ( v1 = v7 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v7 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5721]) ).
tcf(c_5723,plain,
! [X0: $i] :
( r(v5,v7)
| r(v1,v7)
| r(v1,v5)
| r(v1,X0)
| r(X0,v7)
| r(X0,v5)
| ( v5 = v7 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = X0 )
| ( X0 = v7 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5724,plain,
( r(v5,v7)
| r(v1,v7)
| r(v1,v5)
| r(v1,v0)
| r(v0,v7)
| r(v0,v5)
| ( v5 = v7 )
| ( v1 = v7 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v7 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5723]) ).
tcf(c_5725,plain,
! [X0: $i] :
( r(v6,v7)
| r(v1,v7)
| r(v1,v6)
| r(v1,X0)
| r(X0,v7)
| r(X0,v6)
| ( v6 = v7 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = X0 )
| ( X0 = v7 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5726,plain,
( r(v6,v7)
| r(v1,v7)
| r(v1,v6)
| r(v1,v0)
| r(v0,v7)
| r(v0,v6)
| ( v6 = v7 )
| ( v1 = v7 )
| ( v1 = v6 )
| ( v1 = v0 )
| ( v0 = v7 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_5725]) ).
tcf(c_5730,plain,
! [X0: $i] :
( r(v2,v8)
| r(v1,v8)
| r(v1,v2)
| r(v1,X0)
| r(X0,v8)
| r(X0,v2)
| ( v2 = v8 )
| ( v1 = v8 )
| ( v1 = v2 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v2 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5731,plain,
( r(v2,v8)
| r(v1,v8)
| r(v1,v2)
| r(v1,v0)
| r(v0,v8)
| r(v0,v2)
| ( v2 = v8 )
| ( v1 = v8 )
| ( v1 = v2 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v2 ) ),
inference(instantiation,[status(thm)],[c_5730]) ).
tcf(c_5732,plain,
! [X0: $i] :
( r(v3,v8)
| r(v1,v8)
| r(v1,v3)
| r(v1,X0)
| r(X0,v8)
| r(X0,v3)
| ( v3 = v8 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5733,plain,
( r(v3,v8)
| r(v1,v8)
| r(v1,v3)
| r(v1,v0)
| r(v0,v8)
| r(v0,v3)
| ( v3 = v8 )
| ( v1 = v8 )
| ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5732]) ).
tcf(c_5734,plain,
! [X0: $i] :
( r(v4,v8)
| r(v1,v8)
| r(v1,v4)
| r(v1,X0)
| r(X0,v8)
| r(X0,v4)
| ( v4 = v8 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5735,plain,
( r(v4,v8)
| r(v1,v8)
| r(v1,v4)
| r(v1,v0)
| r(v0,v8)
| r(v0,v4)
| ( v4 = v8 )
| ( v1 = v8 )
| ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5734]) ).
tcf(c_5736,plain,
! [X0: $i] :
( r(v5,v8)
| r(v1,v8)
| r(v1,v5)
| r(v1,X0)
| r(X0,v8)
| r(X0,v5)
| ( v5 = v8 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5737,plain,
( r(v5,v8)
| r(v1,v8)
| r(v1,v5)
| r(v1,v0)
| r(v0,v8)
| r(v0,v5)
| ( v5 = v8 )
| ( v1 = v8 )
| ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_5738,plain,
! [X0: $i] :
( r(v6,v8)
| r(v1,v8)
| r(v1,v6)
| r(v1,X0)
| r(X0,v8)
| r(X0,v6)
| ( v6 = v8 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5739,plain,
( r(v6,v8)
| r(v1,v8)
| r(v1,v6)
| r(v1,v0)
| r(v0,v8)
| r(v0,v6)
| ( v6 = v8 )
| ( v1 = v8 )
| ( v1 = v6 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_5738]) ).
tcf(c_5740,plain,
! [X0: $i] :
( r(v7,v8)
| r(v1,v8)
| r(v1,v7)
| r(v1,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_5741,plain,
( r(v7,v8)
| r(v1,v8)
| r(v1,v7)
| r(v1,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v1 = v8 )
| ( v1 = v7 )
| ( v1 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_5740]) ).
tcf(c_5773,plain,
! [X0: $i] :
( r(v3,v4)
| r(v2,v4)
| r(v2,v3)
| r(v2,X0)
| r(X0,v4)
| r(X0,v3)
| ( v3 = v4 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( X0 = v4 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5774,plain,
( r(v3,v4)
| r(v2,v4)
| r(v2,v3)
| r(v2,v0)
| r(v0,v4)
| r(v0,v3)
| ( v3 = v4 )
| ( v2 = v4 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v4 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5773]) ).
tcf(c_5780,plain,
! [X0: $i] :
( r(v3,v5)
| r(v2,v5)
| r(v2,v3)
| r(v2,X0)
| r(X0,v5)
| r(X0,v3)
| ( v3 = v5 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( X0 = v5 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5781,plain,
( r(v3,v5)
| r(v2,v5)
| r(v2,v3)
| r(v2,v0)
| r(v0,v5)
| r(v0,v3)
| ( v3 = v5 )
| ( v2 = v5 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v5 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5780]) ).
tcf(c_5782,plain,
! [X0: $i] :
( r(v4,v5)
| r(v2,v5)
| r(v2,v4)
| r(v2,X0)
| r(X0,v5)
| r(X0,v4)
| ( v4 = v5 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = X0 )
| ( X0 = v5 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5783,plain,
( r(v4,v5)
| r(v2,v5)
| r(v2,v4)
| r(v2,v0)
| r(v0,v5)
| r(v0,v4)
| ( v4 = v5 )
| ( v2 = v5 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v5 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5782]) ).
tcf(c_5789,plain,
! [X0: $i] :
( r(v3,v6)
| r(v2,v6)
| r(v2,v3)
| r(v2,X0)
| r(X0,v6)
| r(X0,v3)
| ( v3 = v6 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( X0 = v6 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5790,plain,
( r(v3,v6)
| r(v2,v6)
| r(v2,v3)
| r(v2,v0)
| r(v0,v6)
| r(v0,v3)
| ( v3 = v6 )
| ( v2 = v6 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v6 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5789]) ).
tcf(c_5791,plain,
! [X0: $i] :
( r(v4,v6)
| r(v2,v6)
| r(v2,v4)
| r(v2,X0)
| r(X0,v6)
| r(X0,v4)
| ( v4 = v6 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = X0 )
| ( X0 = v6 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5792,plain,
( r(v4,v6)
| r(v2,v6)
| r(v2,v4)
| r(v2,v0)
| r(v0,v6)
| r(v0,v4)
| ( v4 = v6 )
| ( v2 = v6 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v6 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5791]) ).
tcf(c_5793,plain,
! [X0: $i] :
( r(v5,v6)
| r(v2,v6)
| r(v2,v5)
| r(v2,X0)
| r(X0,v6)
| r(X0,v5)
| ( v5 = v6 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = X0 )
| ( X0 = v6 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5794,plain,
( r(v5,v6)
| r(v2,v6)
| r(v2,v5)
| r(v2,v0)
| r(v0,v6)
| r(v0,v5)
| ( v5 = v6 )
| ( v2 = v6 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v6 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5793]) ).
tcf(c_5800,plain,
! [X0: $i] :
( r(v3,v7)
| r(v2,v7)
| r(v2,v3)
| r(v2,X0)
| r(X0,v7)
| r(X0,v3)
| ( v3 = v7 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( X0 = v7 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5801,plain,
( r(v3,v7)
| r(v2,v7)
| r(v2,v3)
| r(v2,v0)
| r(v0,v7)
| r(v0,v3)
| ( v3 = v7 )
| ( v2 = v7 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v7 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5800]) ).
tcf(c_5802,plain,
! [X0: $i] :
( r(v4,v7)
| r(v2,v7)
| r(v2,v4)
| r(v2,X0)
| r(X0,v7)
| r(X0,v4)
| ( v4 = v7 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = X0 )
| ( X0 = v7 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5803,plain,
( r(v4,v7)
| r(v2,v7)
| r(v2,v4)
| r(v2,v0)
| r(v0,v7)
| r(v0,v4)
| ( v4 = v7 )
| ( v2 = v7 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v7 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5802]) ).
tcf(c_5804,plain,
! [X0: $i] :
( r(v5,v7)
| r(v2,v7)
| r(v2,v5)
| r(v2,X0)
| r(X0,v7)
| r(X0,v5)
| ( v5 = v7 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = X0 )
| ( X0 = v7 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5805,plain,
( r(v5,v7)
| r(v2,v7)
| r(v2,v5)
| r(v2,v0)
| r(v0,v7)
| r(v0,v5)
| ( v5 = v7 )
| ( v2 = v7 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v7 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5804]) ).
tcf(c_5806,plain,
! [X0: $i] :
( r(v6,v7)
| r(v2,v7)
| r(v2,v6)
| r(v2,X0)
| r(X0,v7)
| r(X0,v6)
| ( v6 = v7 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = X0 )
| ( X0 = v7 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5807,plain,
( r(v6,v7)
| r(v2,v7)
| r(v2,v6)
| r(v2,v0)
| r(v0,v7)
| r(v0,v6)
| ( v6 = v7 )
| ( v2 = v7 )
| ( v2 = v6 )
| ( v2 = v0 )
| ( v0 = v7 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_5806]) ).
tcf(c_5813,plain,
! [X0: $i] :
( r(v3,v8)
| r(v2,v8)
| r(v2,v3)
| r(v2,X0)
| r(X0,v8)
| r(X0,v3)
| ( v3 = v8 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v2 = X0 )
| ( X0 = v8 )
| ( X0 = v3 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5814,plain,
( r(v3,v8)
| r(v2,v8)
| r(v2,v3)
| r(v2,v0)
| r(v0,v8)
| r(v0,v3)
| ( v3 = v8 )
| ( v2 = v8 )
| ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v8 )
| ( v0 = v3 ) ),
inference(instantiation,[status(thm)],[c_5813]) ).
tcf(c_5815,plain,
! [X0: $i] :
( r(v4,v8)
| r(v2,v8)
| r(v2,v4)
| r(v2,X0)
| r(X0,v8)
| r(X0,v4)
| ( v4 = v8 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = X0 )
| ( X0 = v8 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5816,plain,
( r(v4,v8)
| r(v2,v8)
| r(v2,v4)
| r(v2,v0)
| r(v0,v8)
| r(v0,v4)
| ( v4 = v8 )
| ( v2 = v8 )
| ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v8 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_5815]) ).
tcf(c_5817,plain,
! [X0: $i] :
( r(v5,v8)
| r(v2,v8)
| r(v2,v5)
| r(v2,X0)
| r(X0,v8)
| r(X0,v5)
| ( v5 = v8 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = X0 )
| ( X0 = v8 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5818,plain,
( r(v5,v8)
| r(v2,v8)
| r(v2,v5)
| r(v2,v0)
| r(v0,v8)
| r(v0,v5)
| ( v5 = v8 )
| ( v2 = v8 )
| ( v2 = v5 )
| ( v2 = v0 )
| ( v0 = v8 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_5817]) ).
tcf(c_5819,plain,
! [X0: $i] :
( r(v6,v8)
| r(v2,v8)
| r(v2,v6)
| r(v2,X0)
| r(X0,v8)
| r(X0,v6)
| ( v6 = v8 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = X0 )
| ( X0 = v8 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5820,plain,
( r(v6,v8)
| r(v2,v8)
| r(v2,v6)
| r(v2,v0)
| r(v0,v8)
| r(v0,v6)
| ( v6 = v8 )
| ( v2 = v8 )
| ( v2 = v6 )
| ( v2 = v0 )
| ( v0 = v8 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_5819]) ).
tcf(c_5821,plain,
! [X0: $i] :
( r(v7,v8)
| r(v2,v8)
| r(v2,v7)
| r(v2,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_5822,plain,
( r(v7,v8)
| r(v2,v8)
| r(v2,v7)
| r(v2,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v2 = v8 )
| ( v2 = v7 )
| ( v2 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_5821]) ).
tcf(c_6070,plain,
( r(v8,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_6100,plain,
! [X0: $i] :
( r(v4,v5)
| r(v3,v5)
| r(v3,v4)
| r(v3,X0)
| r(X0,v5)
| r(X0,v4)
| ( v4 = v5 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( X0 = v5 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6101,plain,
( r(v4,v5)
| r(v3,v5)
| r(v3,v4)
| r(v3,v0)
| r(v0,v5)
| r(v0,v4)
| ( v4 = v5 )
| ( v3 = v5 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v5 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_6100]) ).
tcf(c_6109,plain,
! [X0: $i] :
( r(v4,v6)
| r(v3,v6)
| r(v3,v4)
| r(v3,X0)
| r(X0,v6)
| r(X0,v4)
| ( v4 = v6 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( X0 = v6 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6110,plain,
( r(v4,v6)
| r(v3,v6)
| r(v3,v4)
| r(v3,v0)
| r(v0,v6)
| r(v0,v4)
| ( v4 = v6 )
| ( v3 = v6 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v6 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_6109]) ).
tcf(c_6111,plain,
! [X0: $i] :
( r(v5,v6)
| r(v3,v6)
| r(v3,v5)
| r(v3,X0)
| r(X0,v6)
| r(X0,v5)
| ( v5 = v6 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = X0 )
| ( X0 = v6 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6112,plain,
( r(v5,v6)
| r(v3,v6)
| r(v3,v5)
| r(v3,v0)
| r(v0,v6)
| r(v0,v5)
| ( v5 = v6 )
| ( v3 = v6 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v6 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6111]) ).
tcf(c_6120,plain,
! [X0: $i] :
( r(v4,v7)
| r(v3,v7)
| r(v3,v4)
| r(v3,X0)
| r(X0,v7)
| r(X0,v4)
| ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( X0 = v7 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6121,plain,
( r(v4,v7)
| r(v3,v7)
| r(v3,v4)
| r(v3,v0)
| r(v0,v7)
| r(v0,v4)
| ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v7 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_6120]) ).
tcf(c_6122,plain,
! [X0: $i] :
( r(v5,v7)
| r(v3,v7)
| r(v3,v5)
| r(v3,X0)
| r(X0,v7)
| r(X0,v5)
| ( v5 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = X0 )
| ( X0 = v7 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6123,plain,
( r(v5,v7)
| r(v3,v7)
| r(v3,v5)
| r(v3,v0)
| r(v0,v7)
| r(v0,v5)
| ( v5 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v7 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6122]) ).
tcf(c_6124,plain,
! [X0: $i] :
( r(v6,v7)
| r(v3,v7)
| r(v3,v6)
| r(v3,X0)
| r(X0,v7)
| r(X0,v6)
| ( v6 = v7 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = X0 )
| ( X0 = v7 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6125,plain,
( r(v6,v7)
| r(v3,v7)
| r(v3,v6)
| r(v3,v0)
| r(v0,v7)
| r(v0,v6)
| ( v6 = v7 )
| ( v3 = v7 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v0 = v7 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6124]) ).
tcf(c_6133,plain,
! [X0: $i] :
( r(v4,v8)
| r(v3,v8)
| r(v3,v4)
| r(v3,X0)
| r(X0,v8)
| r(X0,v4)
| ( v4 = v8 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v3 = X0 )
| ( X0 = v8 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6134,plain,
( r(v4,v8)
| r(v3,v8)
| r(v3,v4)
| r(v3,v0)
| r(v0,v8)
| r(v0,v4)
| ( v4 = v8 )
| ( v3 = v8 )
| ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v8 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_6133]) ).
tcf(c_6135,plain,
! [X0: $i] :
( r(v5,v8)
| r(v3,v8)
| r(v3,v5)
| r(v3,X0)
| r(X0,v8)
| r(X0,v5)
| ( v5 = v8 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = X0 )
| ( X0 = v8 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6136,plain,
( r(v5,v8)
| r(v3,v8)
| r(v3,v5)
| r(v3,v0)
| r(v0,v8)
| r(v0,v5)
| ( v5 = v8 )
| ( v3 = v8 )
| ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v8 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6135]) ).
tcf(c_6137,plain,
! [X0: $i] :
( r(v6,v8)
| r(v3,v8)
| r(v3,v6)
| r(v3,X0)
| r(X0,v8)
| r(X0,v6)
| ( v6 = v8 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = X0 )
| ( X0 = v8 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6138,plain,
( r(v6,v8)
| r(v3,v8)
| r(v3,v6)
| r(v3,v0)
| r(v0,v8)
| r(v0,v6)
| ( v6 = v8 )
| ( v3 = v8 )
| ( v3 = v6 )
| ( v3 = v0 )
| ( v0 = v8 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6137]) ).
tcf(c_6139,plain,
! [X0: $i] :
( r(v7,v8)
| r(v3,v8)
| r(v3,v7)
| r(v3,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_6140,plain,
( r(v7,v8)
| r(v3,v8)
| r(v3,v7)
| r(v3,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v3 = v8 )
| ( v3 = v7 )
| ( v3 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_6139]) ).
tcf(c_6203,plain,
! [X0: $i] :
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v4,X0)
| r(X0,v6)
| r(X0,v5)
| ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( X0 = v6 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6204,plain,
( r(v5,v6)
| r(v4,v6)
| r(v4,v5)
| r(v4,v0)
| r(v0,v6)
| r(v0,v5)
| ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v6 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6203]) ).
tcf(c_6214,plain,
! [X0: $i] :
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v4,X0)
| r(X0,v7)
| r(X0,v5)
| ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( X0 = v7 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6215,plain,
( r(v5,v7)
| r(v4,v7)
| r(v4,v5)
| r(v4,v0)
| r(v0,v7)
| r(v0,v5)
| ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v7 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6214]) ).
tcf(c_6216,plain,
! [X0: $i] :
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v4,X0)
| r(X0,v7)
| r(X0,v6)
| ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = X0 )
| ( X0 = v7 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6217,plain,
( r(v6,v7)
| r(v4,v7)
| r(v4,v6)
| r(v4,v0)
| r(v0,v7)
| r(v0,v6)
| ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v0 = v7 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6216]) ).
tcf(c_6227,plain,
! [X0: $i] :
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v4,X0)
| r(X0,v8)
| r(X0,v5)
| ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v4 = X0 )
| ( X0 = v8 )
| ( X0 = v5 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6228,plain,
( r(v5,v8)
| r(v4,v8)
| r(v4,v5)
| r(v4,v0)
| r(v0,v8)
| r(v0,v5)
| ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v8 )
| ( v0 = v5 ) ),
inference(instantiation,[status(thm)],[c_6227]) ).
tcf(c_6229,plain,
! [X0: $i] :
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v4,X0)
| r(X0,v8)
| r(X0,v6)
| ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = X0 )
| ( X0 = v8 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6230,plain,
( r(v6,v8)
| r(v4,v8)
| r(v4,v6)
| r(v4,v0)
| r(v0,v8)
| r(v0,v6)
| ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ( v4 = v0 )
| ( v0 = v8 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6229]) ).
tcf(c_6231,plain,
! [X0: $i] :
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v4,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_6232,plain,
( r(v7,v8)
| r(v4,v8)
| r(v4,v7)
| r(v4,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ( v4 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_6231]) ).
tcf(c_6290,plain,
! [X0: $i] :
( r(v5,v6)
| r(v5,v4)
| r(v4,v6)
| r(v5,X0)
| r(X0,v6)
| r(X0,v4)
| ( v5 = v6 )
| ( v5 = v4 )
| ( v5 = X0 )
| ( v4 = v6 )
| ( X0 = v6 )
| ( X0 = v4 ) ),
inference(instantiation,[status(thm)],[c_664]) ).
tcf(c_6291,plain,
( r(v5,v6)
| r(v5,v4)
| r(v5,v0)
| r(v4,v6)
| r(v0,v6)
| r(v0,v4)
| ( v5 = v6 )
| ( v5 = v4 )
| ( v5 = v0 )
| ( v4 = v6 )
| ( v0 = v6 )
| ( v0 = v4 ) ),
inference(instantiation,[status(thm)],[c_6290]) ).
tcf(c_6305,plain,
! [X0: $i] :
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v5,X0)
| r(X0,v7)
| r(X0,v6)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( X0 = v7 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_664]) ).
tcf(c_6306,plain,
( r(v6,v7)
| r(v5,v7)
| r(v5,v6)
| r(v5,v0)
| r(v0,v7)
| r(v0,v6)
| ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v0 = v7 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6305]) ).
tcf(c_6318,plain,
! [X0: $i] :
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v5,X0)
| r(X0,v8)
| r(X0,v6)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v5 = X0 )
| ( X0 = v8 )
| ( X0 = v6 ) ),
inference(instantiation,[status(thm)],[c_664]) ).
tcf(c_6319,plain,
( r(v6,v8)
| r(v5,v8)
| r(v5,v6)
| r(v5,v0)
| r(v0,v8)
| r(v0,v6)
| ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ( v5 = v0 )
| ( v0 = v8 )
| ( v0 = v6 ) ),
inference(instantiation,[status(thm)],[c_6318]) ).
tcf(c_6320,plain,
! [X0: $i] :
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v5,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_664]) ).
tcf(c_6321,plain,
( r(v7,v8)
| r(v5,v8)
| r(v5,v7)
| r(v5,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ( v5 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_6320]) ).
tcf(c_6400,plain,
! [X0: $i] :
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v6,X0)
| r(X0,v8)
| r(X0,v7)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v6 = X0 )
| ( X0 = v8 )
| ( X0 = v7 ) ),
inference(instantiation,[status(thm)],[c_684]) ).
tcf(c_6401,plain,
( r(v7,v8)
| r(v6,v8)
| r(v6,v7)
| r(v6,v0)
| r(v0,v8)
| r(v0,v7)
| ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ( v6 = v0 )
| ( v0 = v8 )
| ( v0 = v7 ) ),
inference(instantiation,[status(thm)],[c_6400]) ).
tcf(c_6460,plain,
( ( v7 = v8 )
| ( v7 = v0 )
| ( v0 = v8 )
| ~ r(v7,v8)
| ~ r(v7,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_709]) ).
tcf(c_6491,plain,
( ( v2 = v7 )
| ( v2 = v0 )
| ( v0 = v7 )
| ~ r(v2,v7)
| ~ r(v2,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_6492,plain,
( ( v2 = v7 )
| ( v0 = v7 )
| ( v0 = v2 )
| ~ r(v2,v7)
| ~ r(v0,v7)
| ~ r(v0,v2) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_6493,plain,
( ( v5 = v7 )
| ( v2 = v7 )
| ( v2 = v5 )
| ~ r(v5,v7)
| ~ r(v2,v7)
| ~ r(v2,v5) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_6494,plain,
! [X0: $i] :
( ( v5 = v7 )
| ( v5 = X0 )
| ( X0 = v7 )
| ~ r(v5,v7)
| ~ r(v5,X0)
| ~ r(X0,v7) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_6495,plain,
( ( v5 = v7 )
| ( v5 = v0 )
| ( v0 = v7 )
| ~ r(v5,v7)
| ~ r(v5,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_6494]) ).
tcf(c_6496,plain,
( ( v6 = v7 )
| ( v2 = v7 )
| ( v2 = v6 )
| ~ r(v6,v7)
| ~ r(v2,v7)
| ~ r(v2,v6) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_6497,plain,
! [X0: $i] :
( ( v6 = v7 )
| ( v6 = X0 )
| ( X0 = v7 )
| ~ r(v6,v7)
| ~ r(v6,X0)
| ~ r(X0,v7) ),
inference(instantiation,[status(thm)],[c_685]) ).
tcf(c_6498,plain,
( ( v6 = v7 )
| ( v6 = v0 )
| ( v0 = v7 )
| ~ r(v6,v7)
| ~ r(v6,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_6497]) ).
tcf(c_7605,plain,
( ( v6 = v8 )
| ( v2 = v8 )
| ( v2 = v6 )
| ~ r(v6,v8)
| ~ r(v2,v8)
| ~ r(v2,v6) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_7606,plain,
! [X0: $i] :
( ( v6 = v8 )
| ( v6 = X0 )
| ( X0 = v8 )
| ~ r(v6,v8)
| ~ r(v6,X0)
| ~ r(X0,v8) ),
inference(instantiation,[status(thm)],[c_685]) ).
tcf(c_7607,plain,
( ( v6 = v8 )
| ( v6 = v0 )
| ( v0 = v8 )
| ~ r(v6,v8)
| ~ r(v6,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_7606]) ).
tcf(c_8346,plain,
( ( v3 = v4 )
| ( v2 = v4 )
| ( v2 = v3 )
| ~ r(v3,v4)
| ~ r(v2,v4)
| ~ r(v2,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_8348,plain,
! [X0: $i] :
( ( v3 = v4 )
| ( v3 = X0 )
| ( X0 = v4 )
| ~ r(v3,v4)
| ~ r(v3,X0)
| ~ r(X0,v4) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_8349,plain,
( ( v3 = v4 )
| ( v3 = v0 )
| ( v0 = v4 )
| ~ r(v3,v4)
| ~ r(v3,v0)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_8348]) ).
tcf(c_8524,plain,
( ( v3 = v5 )
| ( v2 = v5 )
| ( v2 = v3 )
| ~ r(v3,v5)
| ~ r(v2,v5)
| ~ r(v2,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_8526,plain,
! [X0: $i] :
( ( v3 = v5 )
| ( v3 = X0 )
| ( X0 = v5 )
| ~ r(v3,v5)
| ~ r(v3,X0)
| ~ r(X0,v5) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_8527,plain,
( ( v3 = v5 )
| ( v3 = v0 )
| ( v0 = v5 )
| ~ r(v3,v5)
| ~ r(v3,v0)
| ~ r(v0,v5) ),
inference(instantiation,[status(thm)],[c_8526]) ).
tcf(c_8839,plain,
( ( v3 = v6 )
| ( v2 = v6 )
| ( v2 = v3 )
| ~ r(v3,v6)
| ~ r(v2,v6)
| ~ r(v2,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_8841,plain,
! [X0: $i] :
( ( v3 = v6 )
| ( v3 = X0 )
| ( X0 = v6 )
| ~ r(v3,v6)
| ~ r(v3,X0)
| ~ r(X0,v6) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_8842,plain,
( ( v3 = v6 )
| ( v3 = v0 )
| ( v0 = v6 )
| ~ r(v3,v6)
| ~ r(v3,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_8841]) ).
tcf(c_9363,plain,
( ( v5 = v7 )
| ( v3 = v7 )
| ( v3 = v5 )
| ~ r(v5,v7)
| ~ r(v3,v7)
| ~ r(v3,v5) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_9392,plain,
( ( v2 = v3 )
| ( v1 = v3 )
| ( v1 = v2 )
| ~ r(v2,v3)
| ~ r(v1,v3)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_9393,plain,
! [X0: $i] :
( ( v1 = v3 )
| ( v1 = X0 )
| ( X0 = v3 )
| ~ r(v1,v3)
| ~ r(v1,X0)
| ~ r(X0,v3) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9394,plain,
( ( v1 = v3 )
| ( v1 = v0 )
| ( v0 = v3 )
| ~ r(v1,v3)
| ~ r(v1,v0)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_9393]) ).
tcf(c_9430,plain,
( ( v6 = v7 )
| ( v3 = v7 )
| ( v3 = v6 )
| ~ r(v6,v7)
| ~ r(v3,v7)
| ~ r(v3,v6) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_9431,plain,
( ( v6 = v8 )
| ( v3 = v8 )
| ( v3 = v6 )
| ~ r(v6,v8)
| ~ r(v3,v8)
| ~ r(v3,v6) ),
inference(instantiation,[status(thm)],[c_537]) ).
tcf(c_9450,plain,
( ( v7 = v8 )
| ( v0 = v8 )
| ( v0 = v7 )
| ~ r(v7,v8)
| ~ r(v0,v8)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_552]) ).
tcf(c_9476,plain,
( ( v7 = v8 )
| ( v6 = v8 )
| ( v6 = v7 )
| ~ r(v7,v8)
| ~ r(v6,v8)
| ~ r(v6,v7) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_9507,plain,
( ( v4 = v5 )
| ( v2 = v5 )
| ( v2 = v4 )
| ~ r(v4,v5)
| ~ r(v2,v5)
| ~ r(v2,v4) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_9508,plain,
( ( v4 = v5 )
| ( v3 = v5 )
| ( v3 = v4 )
| ~ r(v4,v5)
| ~ r(v3,v5)
| ~ r(v3,v4) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_9510,plain,
! [X0: $i] :
( ( v4 = v5 )
| ( v4 = X0 )
| ( X0 = v5 )
| ~ r(v4,v5)
| ~ r(v4,X0)
| ~ r(X0,v5) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_9511,plain,
( ( v4 = v5 )
| ( v4 = v0 )
| ( v0 = v5 )
| ~ r(v4,v5)
| ~ r(v4,v0)
| ~ r(v0,v5) ),
inference(instantiation,[status(thm)],[c_9510]) ).
tcf(c_9512,plain,
( ( v4 = v6 )
| ( v2 = v6 )
| ( v2 = v4 )
| ~ r(v4,v6)
| ~ r(v2,v6)
| ~ r(v2,v4) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_9513,plain,
( ( v4 = v6 )
| ( v3 = v6 )
| ( v3 = v4 )
| ~ r(v4,v6)
| ~ r(v3,v6)
| ~ r(v3,v4) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_9515,plain,
! [X0: $i] :
( ( v4 = v6 )
| ( v4 = X0 )
| ( X0 = v6 )
| ~ r(v4,v6)
| ~ r(v4,X0)
| ~ r(X0,v6) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_9516,plain,
( ( v4 = v6 )
| ( v4 = v0 )
| ( v0 = v6 )
| ~ r(v4,v6)
| ~ r(v4,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_9515]) ).
tcf(c_9537,plain,
( ( v5 = v7 )
| ( v4 = v7 )
| ( v4 = v5 )
| ~ r(v5,v7)
| ~ r(v4,v7)
| ~ r(v4,v5) ),
inference(instantiation,[status(thm)],[c_518]) ).
tcf(c_9539,plain,
( ( v3 = v4 )
| ( v1 = v4 )
| ( v1 = v3 )
| ~ r(v3,v4)
| ~ r(v1,v4)
| ~ r(v1,v3) ),
inference(instantiation,[status(thm)],[c_470]) ).
tcf(c_9540,plain,
( ( v2 = v4 )
| ( v1 = v4 )
| ( v1 = v2 )
| ~ r(v2,v4)
| ~ r(v1,v4)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_9541,plain,
! [X0: $i] :
( ( v1 = v4 )
| ( v1 = X0 )
| ( X0 = v4 )
| ~ r(v1,v4)
| ~ r(v1,X0)
| ~ r(X0,v4) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9542,plain,
( ( v1 = v4 )
| ( v1 = v0 )
| ( v0 = v4 )
| ~ r(v1,v4)
| ~ r(v1,v0)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_9541]) ).
tcf(c_9576,plain,
( ( v4 = v5 )
| ( v1 = v5 )
| ( v1 = v4 )
| ~ r(v4,v5)
| ~ r(v1,v5)
| ~ r(v1,v4) ),
inference(instantiation,[status(thm)],[c_484]) ).
tcf(c_9577,plain,
( ( v4 = v6 )
| ( v1 = v6 )
| ( v1 = v4 )
| ~ r(v4,v6)
| ~ r(v1,v6)
| ~ r(v1,v4) ),
inference(instantiation,[status(thm)],[c_484]) ).
tcf(c_9945,plain,
( ( v4 = v5 )
| ( v5 != v4 )
| ( v4 != v4 ) ),
inference(instantiation,[status(thm)],[c_520]) ).
tcf(c_9967,plain,
( ( v4 = v7 )
| ( v2 = v7 )
| ( v2 = v4 )
| ~ r(v4,v7)
| ~ r(v2,v7)
| ~ r(v2,v4) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_9968,plain,
( ( v6 = v7 )
| ( v4 = v7 )
| ( v4 = v6 )
| ~ r(v6,v7)
| ~ r(v4,v7)
| ~ r(v4,v6) ),
inference(instantiation,[status(thm)],[c_542]) ).
tcf(c_9969,plain,
( ( v4 = v7 )
| ( v1 = v7 )
| ( v1 = v4 )
| ~ r(v4,v7)
| ~ r(v1,v7)
| ~ r(v1,v4) ),
inference(instantiation,[status(thm)],[c_484]) ).
tcf(c_9970,plain,
( ( v4 = v7 )
| ( v3 = v7 )
| ( v3 = v4 )
| ~ r(v4,v7)
| ~ r(v3,v7)
| ~ r(v3,v4) ),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_9972,plain,
! [X0: $i] :
( ( v4 = v7 )
| ( v4 = X0 )
| ( X0 = v7 )
| ~ r(v4,v7)
| ~ r(v4,X0)
| ~ r(X0,v7) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_9973,plain,
( ( v4 = v7 )
| ( v4 = v0 )
| ( v0 = v7 )
| ~ r(v4,v7)
| ~ r(v4,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_9972]) ).
tcf(c_9991,plain,
( ( v1 = v5 )
| ( v1 = v0 )
| ( v0 = v5 )
| ~ r(v1,v5)
| ~ r(v1,v0)
| ~ r(v0,v5) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9993,plain,
( ( v2 = v5 )
| ( v1 = v5 )
| ( v1 = v2 )
| ~ r(v2,v5)
| ~ r(v1,v5)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9994,plain,
( ( v3 = v5 )
| ( v1 = v5 )
| ( v1 = v3 )
| ~ r(v3,v5)
| ~ r(v1,v5)
| ~ r(v1,v3) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9996,plain,
( ( v1 = v6 )
| ( v1 = v0 )
| ( v0 = v6 )
| ~ r(v1,v6)
| ~ r(v1,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9998,plain,
( ( v2 = v6 )
| ( v1 = v6 )
| ( v1 = v2 )
| ~ r(v2,v6)
| ~ r(v1,v6)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_9999,plain,
( ( v3 = v6 )
| ( v1 = v6 )
| ( v1 = v3 )
| ~ r(v3,v6)
| ~ r(v1,v6)
| ~ r(v1,v3) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10001,plain,
( ( v5 = v6 )
| ( v1 = v6 )
| ( v1 = v5 )
| ~ r(v5,v6)
| ~ r(v1,v6)
| ~ r(v1,v5) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10002,plain,
( ( v1 = v7 )
| ( v1 = v0 )
| ( v0 = v7 )
| ~ r(v1,v7)
| ~ r(v1,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10004,plain,
( ( v2 = v7 )
| ( v1 = v7 )
| ( v1 = v2 )
| ~ r(v2,v7)
| ~ r(v1,v7)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10005,plain,
( ( v3 = v7 )
| ( v1 = v7 )
| ( v1 = v3 )
| ~ r(v3,v7)
| ~ r(v1,v7)
| ~ r(v1,v3) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10007,plain,
( ( v5 = v7 )
| ( v1 = v7 )
| ( v1 = v5 )
| ~ r(v5,v7)
| ~ r(v1,v7)
| ~ r(v1,v5) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10008,plain,
( ( v6 = v7 )
| ( v1 = v7 )
| ( v1 = v6 )
| ~ r(v6,v7)
| ~ r(v1,v7)
| ~ r(v1,v6) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10009,plain,
( ( v1 = v8 )
| ( v1 = v0 )
| ( v0 = v8 )
| ~ r(v1,v8)
| ~ r(v1,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10011,plain,
( ( v2 = v8 )
| ( v1 = v8 )
| ( v1 = v2 )
| ~ r(v2,v8)
| ~ r(v1,v8)
| ~ r(v1,v2) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10012,plain,
( ( v3 = v8 )
| ( v1 = v8 )
| ( v1 = v3 )
| ~ r(v3,v8)
| ~ r(v1,v8)
| ~ r(v1,v3) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10013,plain,
( ( v4 = v8 )
| ( v1 = v8 )
| ( v1 = v4 )
| ~ r(v4,v8)
| ~ r(v1,v8)
| ~ r(v1,v4) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10014,plain,
( ( v5 = v8 )
| ( v1 = v8 )
| ( v1 = v5 )
| ~ r(v5,v8)
| ~ r(v1,v8)
| ~ r(v1,v5) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10015,plain,
( ( v6 = v8 )
| ( v1 = v8 )
| ( v1 = v6 )
| ~ r(v6,v8)
| ~ r(v1,v8)
| ~ r(v1,v6) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10016,plain,
( ( v7 = v8 )
| ( v1 = v8 )
| ( v1 = v7 )
| ~ r(v7,v8)
| ~ r(v1,v8)
| ~ r(v1,v7) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_10138,plain,
( ( v2 = v6 )
| ( v2 = v0 )
| ( v0 = v6 )
| ~ r(v2,v6)
| ~ r(v2,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_10139,plain,
( ( v2 = v6 )
| ( v0 = v6 )
| ( v0 = v2 )
| ~ r(v2,v6)
| ~ r(v0,v6)
| ~ r(v0,v2) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_10147,plain,
( ( v5 = v6 )
| ( v2 = v6 )
| ( v2 = v5 )
| ~ r(v5,v6)
| ~ r(v2,v6)
| ~ r(v2,v5) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_10148,plain,
( ( v5 = v6 )
| ( v4 = v6 )
| ( v4 = v5 )
| ~ r(v5,v6)
| ~ r(v4,v6)
| ~ r(v4,v5) ),
inference(instantiation,[status(thm)],[c_518]) ).
tcf(c_10150,plain,
( ( v5 = v6 )
| ( v3 = v6 )
| ( v3 = v5 )
| ~ r(v5,v6)
| ~ r(v3,v6)
| ~ r(v3,v5) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_10152,plain,
! [X0: $i] :
( ( v5 = v6 )
| ( v5 = X0 )
| ( X0 = v6 )
| ~ r(v5,v6)
| ~ r(v5,X0)
| ~ r(X0,v6) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_10153,plain,
( ( v5 = v6 )
| ( v5 = v0 )
| ( v0 = v6 )
| ~ r(v5,v6)
| ~ r(v5,v0)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_10152]) ).
tcf(c_10181,plain,
( ( v6 = v7 )
| ( v0 = v7 )
| ( v0 = v6 )
| ~ r(v6,v7)
| ~ r(v0,v7)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_523]) ).
tcf(c_10182,plain,
( ( v6 = v8 )
| ( v0 = v8 )
| ( v0 = v6 )
| ~ r(v6,v8)
| ~ r(v0,v8)
| ~ r(v0,v6) ),
inference(instantiation,[status(thm)],[c_523]) ).
tcf(c_10210,plain,
( ( v1 = v6 )
| ( v0 = v6 )
| ( v0 = v1 )
| ~ r(v1,v6)
| ~ r(v0,v6)
| ~ r(v0,v1) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_10211,plain,
( ( v1 = v7 )
| ( v0 = v7 )
| ( v0 = v1 )
| ~ r(v1,v7)
| ~ r(v0,v7)
| ~ r(v0,v1) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_10212,plain,
( ( v1 = v8 )
| ( v0 = v8 )
| ( v0 = v1 )
| ~ r(v1,v8)
| ~ r(v0,v8)
| ~ r(v0,v1) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_10295,plain,
( ( v6 = v7 )
| ( v5 = v7 )
| ( v5 = v6 )
| ~ r(v6,v7)
| ~ r(v5,v7)
| ~ r(v5,v6) ),
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_10743,plain,
( ( v3 = v7 )
| ( v2 = v7 )
| ( v2 = v3 )
| ~ r(v3,v7)
| ~ r(v2,v7)
| ~ r(v2,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_10751,plain,
( ( v3 = v8 )
| ( v2 = v8 )
| ( v2 = v3 )
| ~ r(v3,v8)
| ~ r(v2,v8)
| ~ r(v2,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_10774,plain,
( ( v3 = v7 )
| ( v3 = v0 )
| ( v0 = v7 )
| ~ r(v3,v7)
| ~ r(v3,v0)
| ~ r(v0,v7) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_10781,plain,
( ( v3 = v8 )
| ( v3 = v0 )
| ( v0 = v8 )
| ~ r(v3,v8)
| ~ r(v3,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_10785,plain,
( ( v4 = v8 )
| ( v3 = v8 )
| ( v3 = v4 )
| ~ r(v4,v8)
| ~ r(v3,v8)
| ~ r(v3,v4) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_10786,plain,
( ( v5 = v8 )
| ( v3 = v8 )
| ( v3 = v5 )
| ~ r(v5,v8)
| ~ r(v3,v8)
| ~ r(v3,v5) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_10788,plain,
( ( v7 = v8 )
| ( v3 = v8 )
| ( v3 = v7 )
| ~ r(v7,v8)
| ~ r(v3,v8)
| ~ r(v3,v7) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_10816,plain,
( ( v2 = v3 )
| ( v2 = v0 )
| ( v0 = v3 )
| ~ r(v2,v3)
| ~ r(v2,v0)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_10817,plain,
( ( v2 = v3 )
| ( v0 = v3 )
| ( v0 = v2 )
| ~ r(v2,v3)
| ~ r(v0,v3)
| ~ r(v0,v2) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_10822,plain,
( ( v3 = v4 )
| ( v0 = v4 )
| ( v0 = v3 )
| ~ r(v3,v4)
| ~ r(v0,v4)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_10823,plain,
( ( v3 = v5 )
| ( v0 = v5 )
| ( v0 = v3 )
| ~ r(v3,v5)
| ~ r(v0,v5)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_10824,plain,
( ( v3 = v6 )
| ( v0 = v6 )
| ( v0 = v3 )
| ~ r(v3,v6)
| ~ r(v0,v6)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_10825,plain,
( ( v3 = v7 )
| ( v0 = v7 )
| ( v0 = v3 )
| ~ r(v3,v7)
| ~ r(v0,v7)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_10826,plain,
( ( v3 = v8 )
| ( v0 = v8 )
| ( v0 = v3 )
| ~ r(v3,v8)
| ~ r(v0,v8)
| ~ r(v0,v3) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_11019,plain,
( ( v2 = v4 )
| ( v2 = v0 )
| ( v0 = v4 )
| ~ r(v2,v4)
| ~ r(v2,v0)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_11020,plain,
( ( v2 = v4 )
| ( v0 = v4 )
| ( v0 = v2 )
| ~ r(v2,v4)
| ~ r(v0,v4)
| ~ r(v0,v2) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_11026,plain,
( ( v4 = v5 )
| ( v0 = v5 )
| ( v0 = v4 )
| ~ r(v4,v5)
| ~ r(v0,v5)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_11027,plain,
( ( v4 = v6 )
| ( v0 = v6 )
| ( v0 = v4 )
| ~ r(v4,v6)
| ~ r(v0,v6)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_11028,plain,
( ( v4 = v7 )
| ( v0 = v7 )
| ( v0 = v4 )
| ~ r(v4,v7)
| ~ r(v0,v7)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_11029,plain,
( ( v4 = v8 )
| ( v0 = v8 )
| ( v0 = v4 )
| ~ r(v4,v8)
| ~ r(v0,v8)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_11058,plain,
( ( v4 = v8 )
| ( v4 = v0 )
| ( v0 = v8 )
| ~ r(v4,v8)
| ~ r(v4,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_11062,plain,
( ( v4 = v8 )
| ( v4 = v4 )
| ~ r(v4,v8)
| ~ r(v4,v4) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_11063,plain,
( ( v5 = v8 )
| ( v4 = v8 )
| ( v4 = v5 )
| ~ r(v5,v8)
| ~ r(v4,v8)
| ~ r(v4,v5) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_11064,plain,
( ( v6 = v8 )
| ( v4 = v8 )
| ( v4 = v6 )
| ~ r(v6,v8)
| ~ r(v4,v8)
| ~ r(v4,v6) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_11065,plain,
( ( v7 = v8 )
| ( v4 = v8 )
| ( v4 = v7 )
| ~ r(v7,v8)
| ~ r(v4,v8)
| ~ r(v4,v7) ),
inference(instantiation,[status(thm)],[c_649]) ).
tcf(c_11101,plain,
( ( v4 = v8 )
| ( v2 = v8 )
| ( v2 = v4 )
| ~ r(v4,v8)
| ~ r(v2,v8)
| ~ r(v2,v4) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_11123,plain,
( ( v5 = v8 )
| ( v2 = v8 )
| ( v2 = v5 )
| ~ r(v5,v8)
| ~ r(v2,v8)
| ~ r(v2,v5) ),
inference(instantiation,[status(thm)],[c_629]) ).
tcf(c_11124,plain,
( ( v6 = v8 )
| ( v5 = v8 )
| ( v5 = v6 )
| ~ r(v6,v8)
| ~ r(v5,v8)
| ~ r(v5,v6) ),
inference(instantiation,[status(thm)],[c_547]) ).
tcf(c_11127,plain,
( ( v7 = v8 )
| ( v5 = v8 )
| ( v5 = v7 )
| ~ r(v7,v8)
| ~ r(v5,v8)
| ~ r(v5,v7) ),
inference(instantiation,[status(thm)],[c_576]) ).
tcf(c_11130,plain,
! [X0: $i] :
( ( v5 = v8 )
| ( v5 = X0 )
| ( X0 = v8 )
| ~ r(v5,v8)
| ~ r(v5,X0)
| ~ r(X0,v8) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_11131,plain,
( ( v5 = v8 )
| ( v5 = v0 )
| ( v0 = v8 )
| ~ r(v5,v8)
| ~ r(v5,v0)
| ~ r(v0,v8) ),
inference(instantiation,[status(thm)],[c_11130]) ).
tcf(c_11492,plain,
( ( v5 = v4 )
| ( v3 = v5 )
| ( v3 = v4 )
| ~ r(v5,v4)
| ~ r(v3,v5)
| ~ r(v3,v4) ),
inference(instantiation,[status(thm)],[c_513]) ).
tcf(c_11494,plain,
! [X0: $i] :
( ( v5 = v4 )
| ( v5 = X0 )
| ( X0 = v4 )
| ~ r(v5,v4)
| ~ r(v5,X0)
| ~ r(X0,v4) ),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_11495,plain,
( ( v5 = v4 )
| ( v5 = v0 )
| ( v0 = v4 )
| ~ r(v5,v4)
| ~ r(v5,v0)
| ~ r(v0,v4) ),
inference(instantiation,[status(thm)],[c_11494]) ).
tcf(c_11644,plain,
( ( v7 = v8 )
| ( v2 = v8 )
| ( v2 = v7 )
| ~ r(v7,v8)
| ~ r(v2,v8)
| ~ r(v2,v7) ),
inference(instantiation,[status(thm)],[c_561]) ).
tcf(c_12012,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_11644,c_11495,c_11492,c_11131,c_11124,c_11127,c_11123,c_11101,c_11065,c_11064,c_11063,c_11062,c_11058,c_11029,c_11028,c_11027,c_11026,c_11020,c_11019,c_10826,c_10825,c_10824,c_10823,c_10822,c_10817,c_10816,c_10788,c_10786,c_10785,c_10781,c_10774,c_10751,c_10743,c_10295,c_10212,c_10211,c_10210,c_10182,c_10181,c_10153,c_10148,c_10150,c_10147,c_10139,c_10138,c_10016,c_10015,c_10014,c_10013,c_10012,c_10011,c_10009,c_10008,c_10007,c_10005,c_10004,c_10002,c_10001,c_9999,c_9998,c_9996,c_9994,c_9993,c_9991,c_9973,c_9968,c_9969,c_9970,c_9967,c_9945,c_9577,c_9576,c_9542,c_9539,c_9540,c_9537,c_9516,c_9513,c_9512,c_9511,c_9508,c_9507,c_9476,c_9450,c_9431,c_9430,c_9394,c_9392,c_9363,c_8842,c_8839,c_8527,c_8524,c_8349,c_8346,c_7607,c_7605,c_6498,c_6496,c_6495,c_6493,c_6492,c_6491,c_6460,c_6401,c_6321,c_6319,c_6306,c_6291,c_6232,c_6230,c_6228,c_6217,c_6215,c_6204,c_6140,c_6138,c_6136,c_6134,c_6125,c_6123,c_6121,c_6112,c_6110,c_6101,c_6070,c_5822,c_5820,c_5818,c_5816,c_5814,c_5807,c_5805,c_5803,c_5801,c_5794,c_5792,c_5790,c_5783,c_5781,c_5774,c_5741,c_5739,c_5737,c_5735,c_5733,c_5731,c_5726,c_5724,c_5722,c_5720,c_5718,c_5713,c_5711,c_5709,c_5707,c_5702,c_5700,c_5698,c_5693,c_5691,c_5686,c_5674,c_5568,c_5567,c_5563,c_5459,c_5456,c_5454,c_5452,c_5429,c_5400,c_5377,c_5348,c_5325,c_5296,c_5273,c_4470,c_4447,c_3368,c_3345,c_3308,c_3306,c_3292,c_3285,c_3278,c_3256,c_3254,c_3240,c_3233,c_3226,c_3204,c_3202,c_3188,c_3181,c_3174,c_3150,c_3148,c_3134,c_3127,c_3120,c_2588,c_2586,c_2572,c_2565,c_2558,c_2234,c_2232,c_2230,c_2218,c_2217,c_2211,c_2210,c_2204,c_2198,c_2135,c_2048,c_2046,c_2044,c_2040,c_2032,c_2031,c_2025,c_2024,c_2022,c_2018,c_2012,c_1996,c_1994,c_1992,c_1980,c_1979,c_1973,c_1972,c_1966,c_1960,c_1944,c_1942,c_1940,c_1936,c_1928,c_1927,c_1921,c_1920,c_1914,c_1908,c_1880,c_1876,c_1874,c_1872,c_1870,c_1860,c_1859,c_1858,c_1853,c_1852,c_1851,c_1846,c_1845,c_1840,c_1835,c_1824,c_1822,c_1820,c_1818,c_1808,c_1807,c_1806,c_1801,c_1800,c_1799,c_1794,c_1793,c_1788,c_1783,c_1772,c_1770,c_1768,c_1766,c_1756,c_1755,c_1754,c_1749,c_1748,c_1747,c_1746,c_1742,c_1741,c_1736,c_1731,c_1710,c_1709,c_1338,c_1167,c_1165,c_1163,c_1161,c_1159,c_1151,c_1150,c_1149,c_1148,c_1144,c_1143,c_1142,c_1141,c_1137,c_1136,c_1135,c_1131,c_1130,c_1126,c_1122,c_1031,c_1029,c_1027,c_1025,c_1023,c_1015,c_1014,c_1013,c_1012,c_1008,c_1007,c_1006,c_1005,c_1001,c_1000,c_999,c_995,c_994,c_990,c_986,c_887,c_885,c_883,c_881,c_879,c_877,c_871,c_870,c_869,c_868,c_867,c_864,c_863,c_862,c_861,c_860,c_857,c_856,c_855,c_854,c_851,c_850,c_849,c_846,c_845,c_842,c_839,c_832,c_829,c_827,c_776,c_621,c_616,c_611,c_606,c_601,c_596,c_591,c_588,c_582,c_577,c_572,c_567,c_562,c_557,c_554,c_548,c_543,c_538,c_533,c_528,c_525,c_519,c_514,c_509,c_504,c_501,c_495,c_490,c_485,c_482,c_476,c_471,c_468,c_462,c_459,c_455,c_208,c_52,c_53,c_54,c_55,c_56,c_57,c_58,c_59,c_60,c_61,c_62,c_63,c_64,c_65,c_66,c_67,c_68,c_69,c_70,c_71,c_72,c_73,c_74,c_75,c_76,c_77,c_78,c_79,c_80,c_81,c_82,c_83,c_84,c_85,c_86,c_87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA120+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 12:55:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 14.79/2.90 % SZS status Started for theBenchmark.p
% 14.79/2.90 % SZS status Unsatisfiable for theBenchmark.p
% 14.79/2.90
% 14.79/2.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.79/2.90
% 14.79/2.90 % ------ iProver source info
% 14.79/2.90
% 14.79/2.90 % git: date: 2026-07-19 20:42:38 +0200
% 14.79/2.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.79/2.90 % git: non_committed_changes: false
% 14.79/2.90
% 14.79/2.90 % ------ Parsing...
% 14.79/2.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.79/2.90
% 14.79/2.90 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 14.79/2.90
% 14.79/2.90 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 14.79/2.90
% 14.79/2.90 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 14.79/2.90 % ------ Proving...
% 14.79/2.90 % ------ Problem Properties
% 14.79/2.90
% 14.79/2.90 %
% 14.79/2.90 % clauses 39
% 14.79/2.90 % conjectures 0
% 14.79/2.90 % EPR 39
% 14.79/2.90 % Horn 37
% 14.79/2.90 % unary 36
% 14.79/2.90 % binary 1
% 14.79/2.90 % lits 56
% 14.79/2.90 % lits eq 45
% 14.79/2.90 % fd_pure 0
% 14.79/2.90 % fd_pseudo 0
% 14.79/2.90 % fd_cond 0
% 14.79/2.90 % fd_pseudo_cond 2
% 14.79/2.90 % AC symbols 0
% 14.79/2.90
% 14.79/2.90 % ------ Input Options Time Limit: Unbounded
% 14.79/2.90
% 14.79/2.90
% 14.79/2.90 % ------
% 14.79/2.90 % Current options:
% 14.79/2.90 % ------
% 14.79/2.90
% 14.79/2.90
% 14.79/2.90 %
% 14.79/2.90
% 14.79/2.90 % ------ Proving...
% 14.79/2.90 %
% 14.79/2.90
% 14.79/2.90 % SZS status Unsatisfiable for theBenchmark.p
% 14.79/2.90
% 14.79/2.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.79/2.93
% 14.79/2.93
%------------------------------------------------------------------------------