%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CAT027+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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:01:14 PM UTC 2026
% Result : Theorem 177.58s 27.16s
% Output : CNFRefutation 177.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 33
% Syntax : Number of formulae : 289 ( 75 unt; 11 def)
% Number of atoms : 2078 ( 72 equ)
% Maximal formula atoms : 17 ( 7 avg)
% Number of connectives : 2495 (1160 ~;1161 |; 122 &)
% ( 1 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 24 ( 22 usr; 12 prp; 0-6 aty)
% Number of functors : 17 ( 17 usr; 4 con; 0-7 aty)
% Number of variables : 544 ( 0 sgn 536 !; 8 ?; 197 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3)),k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
& r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k7_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3)),k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_isocat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3)),k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
& r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k7_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3)),k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( ( m2_cat_1(X3,X0,X1)
& m2_cat_1(X2,X0,X1)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
=> ( m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_1(X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_nattra_1) ).
fof(f30,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f31,axiom,
! [X0,X1,X2] :
( ( m2_cat_1(X2,X0,X1)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m1_nattra_1(k4_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_nattra_1) ).
fof(f33,axiom,
! [X0,X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f34,axiom,
! [X0,X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f36,axiom,
! [X0,X1,X2,X3] :
( ( m2_cat_1(X3,X0,X1)
& m2_cat_1(X2,X0,X1)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X4] :
( m2_nattra_1(X4,X0,X1,X2,X3)
=> m1_nattra_1(X4,X0,X1,X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_nattra_1) ).
fof(f43,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( m1_relset_1(X5,X2,X3)
& v1_funct_2(X5,X2,X3)
& v1_funct_1(X5)
& m1_relset_1(X4,X0,X1)
& v1_funct_2(X4,X0,X1)
& v1_funct_1(X4)
& ~ v1_xboole_0(X3)
& ~ v1_xboole_0(X2)
& ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X0) )
=> ( r4_nattra_1(X0,X1,X2,X3,X4,X5)
=> r4_nattra_1(X0,X1,X2,X3,X5,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r4_nattra_1) ).
fof(f48,axiom,
! [X0,X1,X2] :
( ( m2_cat_1(X2,X0,X1)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> k7_nattra_1(X0,X1,X2) = k4_nattra_1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k7_nattra_1) ).
fof(f50,axiom,
! [X0,X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> ( l1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f51,axiom,
! [X0,X1,X2,X3] :
( ( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& l1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_isocat_2) ).
fof(f52,axiom,
! [X0,X1,X2,X3] :
( ( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& l1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k12_isocat_2) ).
fof(f53,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
& m2_cat_1(X4,X0,k11_cat_2(X1,X2))
& m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& l1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k13_isocat_2) ).
fof(f54,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
& m2_cat_1(X4,X0,k11_cat_2(X1,X2))
& m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& l1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k14_isocat_2) ).
fof(f57,axiom,
! [X0,X1,X2] :
( ( m2_cat_1(X2,X0,X1)
& l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_nattra_1) ).
fof(f60,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u1_cat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_cat_1) ).
fof(f61,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u2_cat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_cat_1) ).
fof(f62,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f63,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f64,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f65,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f66,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( ( l1_cat_1(X2)
& v2_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ! [X4] :
( m2_cat_1(X4,X1,X2)
=> r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_isocat_1) ).
fof(f69,plain,
? [X0] :
( l1_cat_1(X0)
& v2_cat_1(X0)
& ? [X1] :
( l1_cat_1(X1)
& v2_cat_1(X1)
& ? [X2] :
( l1_cat_1(X2)
& v2_cat_1(X2)
& ? [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& ( ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3)),k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k7_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3)),k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3))) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f70,plain,
? [X0] :
( l1_cat_1(X0)
& v2_cat_1(X0)
& ? [X1] :
( l1_cat_1(X1)
& v2_cat_1(X1)
& ? [X2] :
( l1_cat_1(X2)
& v2_cat_1(X2)
& ? [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& ( ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3)),k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k7_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3)),k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3))) ) ) ) ) ),
inference(flattening,[],[f69]) ).
fof(f78,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X4] :
( ~ m1_nattra_1(X4,X0,X1,X2,X3)
| ( m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_1(X4) ) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f79,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X4] :
( ~ m1_nattra_1(X4,X0,X1,X2,X3)
| ( m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& v1_funct_1(X4) ) ) ),
inference(flattening,[],[f78]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m1_nattra_1(k4_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(ennf_transformation,[],[f31]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m1_nattra_1(k4_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(flattening,[],[f97]) ).
fof(f101,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f102,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f104,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X4] :
( ~ m2_nattra_1(X4,X0,X1,X2,X3)
| m1_nattra_1(X4,X0,X1,X2,X3) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X4] :
( ~ m2_nattra_1(X4,X0,X1,X2,X3)
| m1_nattra_1(X4,X0,X1,X2,X3) ) ),
inference(flattening,[],[f105]) ).
fof(f111,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m1_relset_1(X5,X2,X3)
| ~ v1_funct_2(X5,X2,X3)
| ~ v1_funct_1(X5)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_2(X4,X0,X1)
| ~ v1_funct_1(X4)
| v1_xboole_0(X3)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| r4_nattra_1(X0,X1,X2,X3,X5,X4) ),
inference(ennf_transformation,[],[f43]) ).
fof(f112,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m1_relset_1(X5,X2,X3)
| ~ v1_funct_2(X5,X2,X3)
| ~ v1_funct_1(X5)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_2(X4,X0,X1)
| ~ v1_funct_1(X4)
| v1_xboole_0(X3)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| r4_nattra_1(X0,X1,X2,X3,X5,X4) ),
inference(flattening,[],[f111]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| k7_nattra_1(X0,X1,X2) = k4_nattra_1(X0,X1,X2) ),
inference(ennf_transformation,[],[f48]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| k7_nattra_1(X0,X1,X2) = k4_nattra_1(X0,X1,X2) ),
inference(flattening,[],[f119]) ).
fof(f123,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f124,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(ennf_transformation,[],[f51]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
inference(ennf_transformation,[],[f52]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4)) ),
inference(ennf_transformation,[],[f53]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4)) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ),
inference(ennf_transformation,[],[f54]) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ),
inference(flattening,[],[f131]) ).
fof(f137,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(ennf_transformation,[],[f57]) ).
fof(f138,plain,
! [X0,X1,X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(flattening,[],[f137]) ).
fof(f141,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u1_cat_1(X0)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f142,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u2_cat_1(X0)) ),
inference(ennf_transformation,[],[f61]) ).
fof(f143,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
inference(ennf_transformation,[],[f62]) ).
fof(f144,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
inference(flattening,[],[f143]) ).
fof(f145,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
inference(ennf_transformation,[],[f63]) ).
fof(f146,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
inference(flattening,[],[f145]) ).
fof(f147,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ! [X4] :
( ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ! [X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
inference(ennf_transformation,[],[f64]) ).
fof(f148,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ! [X4] :
( ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ! [X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
inference(flattening,[],[f147]) ).
fof(f149,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ! [X4] :
( ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ! [X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f150,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ! [X4] :
( ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ! [X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
inference(flattening,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,X1)
| ! [X4] :
( ~ m2_cat_1(X4,X1,X2)
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4))) ) ) ) ) ),
inference(ennf_transformation,[],[f66]) ).
fof(f152,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ! [X3] :
( ~ m2_cat_1(X3,X0,X1)
| ! [X4] :
( ~ m2_cat_1(X4,X1,X2)
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4))) ) ) ) ) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
( l1_cat_1(sK0)
& v2_cat_1(sK0)
& l1_cat_1(sK1)
& v2_cat_1(sK1)
& l1_cat_1(sK2)
& v2_cat_1(sK2)
& m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2))
& ( ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK2),u1_cat_1(sK0),u2_cat_1(sK2),k7_nattra_1(sK0,sK2,k12_isocat_2(sK0,sK1,sK2,sK3)),k14_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3)))
| ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK1),u1_cat_1(sK0),u2_cat_1(sK1),k7_nattra_1(sK0,sK1,k11_isocat_2(sK0,sK1,sK2,sK3)),k13_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f70]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) )
& ( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f167,plain,
l1_cat_1(sK0),
inference(cnf_transformation,[],[f153]) ).
fof(f168,plain,
v2_cat_1(sK0),
inference(cnf_transformation,[],[f153]) ).
fof(f169,plain,
l1_cat_1(sK1),
inference(cnf_transformation,[],[f153]) ).
fof(f170,plain,
v2_cat_1(sK1),
inference(cnf_transformation,[],[f153]) ).
fof(f171,plain,
l1_cat_1(sK2),
inference(cnf_transformation,[],[f153]) ).
fof(f172,plain,
v2_cat_1(sK2),
inference(cnf_transformation,[],[f153]) ).
fof(f173,plain,
m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)),
inference(cnf_transformation,[],[f153]) ).
fof(f174,plain,
( ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK2),u1_cat_1(sK0),u2_cat_1(sK2),k7_nattra_1(sK0,sK2,k12_isocat_2(sK0,sK1,sK2,sK3)),k14_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3)))
| ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK1),u1_cat_1(sK0),u2_cat_1(sK1),k7_nattra_1(sK0,sK1,k11_isocat_2(sK0,sK1,sK2,sK3)),k13_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3))) ),
inference(cnf_transformation,[],[f153]) ).
fof(f181,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_nattra_1(X4,X0,X1,X2,X3)
| m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f182,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_nattra_1(X4,X0,X1,X2,X3)
| v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f183,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_nattra_1(X4,X0,X1,X2,X3)
| v1_funct_1(X4) ),
inference(cnf_transformation,[],[f79]) ).
fof(f202,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f161]) ).
fof(f204,plain,
! [X2,X0,X1] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m1_nattra_1(k4_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(cnf_transformation,[],[f98]) ).
fof(f206,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f207,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f208,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m2_nattra_1(X4,X0,X1,X2,X3)
| m1_nattra_1(X4,X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f106]) ).
fof(f215,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X5,X2,X3)
| ~ v1_funct_2(X5,X2,X3)
| ~ v1_funct_1(X5)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_2(X4,X0,X1)
| ~ v1_funct_1(X4)
| v1_xboole_0(X3)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| r4_nattra_1(X0,X1,X2,X3,X5,X4) ),
inference(cnf_transformation,[],[f112]) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| k4_nattra_1(X0,X1,X2) = k7_nattra_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f223,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| l1_cat_1(k11_cat_2(X0,X1)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f224,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v2_cat_1(k11_cat_2(X0,X1)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f225,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f226,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f227,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f228,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ~ m2_cat_1(X2,X0,X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
inference(cnf_transformation,[],[f138]) ).
fof(f235,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u1_cat_1(X0)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f236,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u2_cat_1(X0)) ),
inference(cnf_transformation,[],[f142]) ).
fof(f237,plain,
! [X2,X3,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f238,plain,
! [X2,X3,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f239,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f240,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f241,plain,
! [X2,X3,X0,X1,X4] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X1,X2)
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4))) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_49,negated_conjecture,
( ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK2),u1_cat_1(sK0),u2_cat_1(sK2),k7_nattra_1(sK0,sK2,k12_isocat_2(sK0,sK1,sK2,sK3)),k14_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3)))
| ~ r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK1),u1_cat_1(sK0),u2_cat_1(sK1),k7_nattra_1(sK0,sK1,k11_isocat_2(sK0,sK1,sK2,sK3)),k13_isocat_2(sK0,sK1,sK2,sK3,sK3,k7_nattra_1(sK0,k11_cat_2(sK1,sK2),sK3))) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_50,negated_conjecture,
m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)),
inference(cnf_transformation,[],[f173]) ).
tcf(c_51,negated_conjecture,
v2_cat_1(sK2),
inference(cnf_transformation,[],[f172]) ).
tcf(c_52,negated_conjecture,
l1_cat_1(sK2),
inference(cnf_transformation,[],[f171]) ).
tcf(c_53,negated_conjecture,
v2_cat_1(sK1),
inference(cnf_transformation,[],[f170]) ).
tcf(c_54,negated_conjecture,
l1_cat_1(sK1),
inference(cnf_transformation,[],[f169]) ).
tcf(c_55,negated_conjecture,
v2_cat_1(sK0),
inference(cnf_transformation,[],[f168]) ).
tcf(c_56,negated_conjecture,
l1_cat_1(sK0),
inference(cnf_transformation,[],[f167]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_funct_1(X0)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ m1_nattra_1(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_funct_2(X0,u1_cat_1(X1),u2_cat_1(X2))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ m1_nattra_1(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m2_relset_1(X0,u1_cat_1(X1),u2_cat_1(X2))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ m1_nattra_1(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_nattra_1(k4_nattra_1(X1,X2,X0),X1,X2,X0,X0)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_nattra_1(X0,X1,X2,X3,X4)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ m2_nattra_1(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v1_xboole_0(X3)
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| r4_nattra_1(X0,X1,X2,X3,X5,X4)
| ~ v1_funct_1(X5)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X5,X2,X3)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_2(X5,X2,X3)
| ~ v1_funct_2(X4,X0,X1)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k7_nattra_1(X1,X2,X0) = k4_nattra_1(X1,X2,X0) )
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] :
( v2_cat_1(k11_cat_2(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( l1_cat_1(k11_cat_2(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m2_cat_1(k11_isocat_2(X1,X2,X3,X0),X1,X2)
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,k11_cat_2(X2,X3)) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m2_cat_1(k12_isocat_2(X1,X2,X3,X0),X1,X3)
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,k11_cat_2(X2,X3)) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m2_nattra_1(k13_isocat_2(X1,X2,X3,X4,X5,X0),X1,X2,k11_isocat_2(X1,X2,X3,X4),k11_isocat_2(X1,X2,X3,X5))
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m2_nattra_1(k14_isocat_2(X1,X2,X3,X4,X5,X0),X1,X3,k12_isocat_2(X1,X2,X3,X4),k12_isocat_2(X1,X2,X3,X5))
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_nattra_1(k7_nattra_1(X1,X2,X0),X1,X2,X0,X0)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_117,plain,
! [X0: $i] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u1_cat_1(X0)) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_118,plain,
! [X0: $i] :
( ~ l1_cat_1(X0)
| ~ v1_xboole_0(u2_cat_1(X0)) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_isocat_1(X1,k11_cat_2(X2,X3),X2,X0,k8_isocat_2(X2,X3)) = k11_isocat_2(X1,X2,X3,X0) )
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,k11_cat_2(X2,X3)) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_isocat_1(X1,k11_cat_2(X2,X3),X3,X0,k9_isocat_2(X2,X3)) = k12_isocat_2(X1,X2,X3,X0) )
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,k11_cat_2(X2,X3)) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( k6_isocat_1(X1,k11_cat_2(X2,X3),X2,X4,X5,X0,k8_isocat_2(X2,X3)) = k13_isocat_2(X1,X2,X3,X4,X5,X0) )
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( k6_isocat_1(X1,k11_cat_2(X2,X3),X3,X4,X5,X0,k9_isocat_2(X2,X3)) = k14_isocat_2(X1,X2,X3,X4,X5,X0) )
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r4_nattra_1(u1_cat_1(X1),u2_cat_1(X4),u1_cat_1(X1),u2_cat_1(X4),k6_isocat_1(X1,X2,X4,X0,X0,k7_nattra_1(X1,X2,X0),X3),k7_nattra_1(X1,X4,k2_isocat_1(X1,X2,X4,X0,X3)))
| ~ l1_cat_1(X4)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X4)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X2,X4)
| ~ m2_cat_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m2_relset_1(X0,X1,X2)
| m1_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_85]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_182]) ).
tcf(c_1746,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( m1_relset_1(X5,X1,X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X7,X0,X2)
| ~ m2_cat_1(X6,X0,X2)
| ~ m1_nattra_1(X4,X0,X2,X6,X7)
| ( X4 != X5 )
| ( u2_cat_1(X2) != X3 )
| ( u1_cat_1(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_183]) ).
tcf(c_1747,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_relset_1(X0,u1_cat_1(X1),u2_cat_1(X2))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ m1_nattra_1(X0,X1,X2,X3,X4) ),
inference(unflattening,[status(thm)],[c_1746]) ).
tcf(c_3689,definition,
iPr_def_10 = k11_cat_2(sK1,sK2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_3690,definition,
iPr_def_11 = u1_cat_1(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_3691,definition,
iPr_def_12 = u2_cat_1(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_3692,definition,
iPr_def_13 = k11_isocat_2(sK0,sK1,sK2,sK3),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_3693,definition,
iPr_def_14 = k7_nattra_1(sK0,sK1,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_3694,definition,
iPr_def_15 = k7_nattra_1(sK0,iPr_def_10,sK3),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_3695,definition,
iPr_def_16 = k13_isocat_2(sK0,sK1,sK2,sK3,sK3,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_3696,definition,
iPr_def_17 = u2_cat_1(sK2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_3697,definition,
iPr_def_18 = k12_isocat_2(sK0,sK1,sK2,sK3),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_3698,definition,
iPr_def_19 = k7_nattra_1(sK0,sK2,iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_3699,definition,
iPr_def_20 = k14_isocat_2(sK0,sK1,sK2,sK3,sK3,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_3700,negated_conjecture,
l1_cat_1(sK0),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_3701,negated_conjecture,
v2_cat_1(sK0),
inference(demodulation,[status(thm)],[c_55]) ).
tcf(c_3702,negated_conjecture,
l1_cat_1(sK1),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_3703,negated_conjecture,
v2_cat_1(sK1),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_3704,negated_conjecture,
l1_cat_1(sK2),
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_3705,negated_conjecture,
v2_cat_1(sK2),
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_3706,negated_conjecture,
m2_cat_1(sK3,sK0,iPr_def_10),
inference(demodulation,[status(thm)],[c_50,c_3689]) ).
tcf(c_3707,negated_conjecture,
( ~ r4_nattra_1(iPr_def_11,iPr_def_17,iPr_def_11,iPr_def_17,iPr_def_19,iPr_def_20)
| ~ r4_nattra_1(iPr_def_11,iPr_def_12,iPr_def_11,iPr_def_12,iPr_def_14,iPr_def_16) ),
inference(demodulation,[status(thm)],[c_49,c_3699,c_3697,c_3698,c_3696,c_3694,c_3695,c_3692,c_3693,c_3691,c_3690]) ).
tcf(c_7789,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(u2_cat_1(X2))
| v1_xboole_0(u1_cat_1(X0))
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ v1_funct_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)))
| ~ v1_funct_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ m1_relset_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2)) ),
inference(superposition,[status(thm)],[c_123,c_97]) ).
tcf(c_42752,plain,
( l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_106]) ).
tcf(c_42753,plain,
l1_cat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_42752,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_42850,plain,
( v2_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_105]) ).
tcf(c_42851,plain,
v2_cat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_42850,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_43213,plain,
( m2_cat_1(k8_isocat_2(sK1,sK2),iPr_def_10,sK1)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_88]) ).
tcf(c_43215,plain,
m2_cat_1(k8_isocat_2(sK1,sK2),iPr_def_10,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_43213,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_43233,plain,
( m2_cat_1(k9_isocat_2(sK1,sK2),iPr_def_10,sK2)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_89]) ).
tcf(c_43235,plain,
m2_cat_1(k9_isocat_2(sK1,sK2),iPr_def_10,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_43233,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_43381,plain,
( m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3)
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_3694,c_113]) ).
tcf(c_43386,plain,
m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_43381,c_42753,c_3700,c_42851,c_3701,c_3706]) ).
tcf(c_43560,plain,
( m2_cat_1(iPr_def_13,sK0,sK1)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_3692,c_107]) ).
tcf(c_43563,plain,
( m2_cat_1(iPr_def_13,sK0,sK1)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_43560,c_3689]) ).
tcf(c_43564,plain,
m2_cat_1(iPr_def_13,sK0,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_43563,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706]) ).
tcf(c_43597,plain,
( m2_cat_1(iPr_def_18,sK0,sK2)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_3697,c_108]) ).
tcf(c_43600,plain,
( m2_cat_1(iPr_def_18,sK0,sK2)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_43597,c_3689]) ).
tcf(c_43601,plain,
m2_cat_1(iPr_def_18,sK0,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_43600,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706]) ).
tcf(c_43618,plain,
( ( k7_nattra_1(sK0,sK1,iPr_def_13) = k4_nattra_1(sK0,sK1,iPr_def_13) )
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0) ),
inference(superposition,[status(thm)],[c_43564,c_102]) ).
tcf(c_43621,plain,
( ( k4_nattra_1(sK0,sK1,iPr_def_13) = iPr_def_14 )
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_43618,c_3693]) ).
tcf(c_43622,plain,
k4_nattra_1(sK0,sK1,iPr_def_13) = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_43621,c_3702,c_3700,c_3703,c_3701]) ).
tcf(c_43623,plain,
( ( k7_nattra_1(sK0,sK2,iPr_def_18) = k4_nattra_1(sK0,sK2,iPr_def_18) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0) ),
inference(superposition,[status(thm)],[c_43601,c_102]) ).
tcf(c_43626,plain,
( ( k4_nattra_1(sK0,sK2,iPr_def_18) = iPr_def_19 )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_43623,c_3698]) ).
tcf(c_43627,plain,
k4_nattra_1(sK0,sK2,iPr_def_18) = iPr_def_19,
inference(forward_subsumption_resolution,[status(thm)],[c_43626,c_3704,c_3700,c_3705,c_3701]) ).
tcf(c_43628,plain,
( m1_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_43622,c_86]) ).
tcf(c_43629,plain,
m1_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_43628,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_43630,plain,
( v1_funct_1(iPr_def_14)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_43629,c_63]) ).
tcf(c_43631,plain,
v1_funct_1(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_43630,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_43632,plain,
( m1_nattra_1(iPr_def_19,sK0,sK2,iPr_def_18,iPr_def_18)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_43627,c_86]) ).
tcf(c_43633,plain,
m1_nattra_1(iPr_def_19,sK0,sK2,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_43632,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_43634,plain,
( v1_funct_1(iPr_def_19)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_43633,c_63]) ).
tcf(c_43635,plain,
v1_funct_1(iPr_def_19),
inference(forward_subsumption_resolution,[status(thm)],[c_43634,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_43682,plain,
( v1_funct_2(iPr_def_14,u1_cat_1(sK0),u2_cat_1(sK1))
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_43629,c_64]) ).
tcf(c_43683,plain,
( v1_funct_2(iPr_def_19,u1_cat_1(sK0),u2_cat_1(sK2))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_43633,c_64]) ).
tcf(c_43684,plain,
( v1_funct_2(iPr_def_19,iPr_def_11,iPr_def_17)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(light_normalisation,[status(thm)],[c_43683,c_3690,c_3696]) ).
tcf(c_43685,plain,
v1_funct_2(iPr_def_19,iPr_def_11,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_43684,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_43686,plain,
( v1_funct_2(iPr_def_14,iPr_def_11,iPr_def_12)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(light_normalisation,[status(thm)],[c_43682,c_3690,c_3691]) ).
tcf(c_43687,plain,
v1_funct_2(iPr_def_14,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_43686,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_44110,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,k11_cat_2(sK1,sK2),sK1,X0,k8_isocat_2(sK1,sK2)) = k11_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(superposition,[status(thm)],[c_3689,c_119]) ).
tcf(c_44111,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,iPr_def_10,sK1,X0,k8_isocat_2(sK1,sK2)) = k11_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_44110,c_3689]) ).
tcf(c_44112,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,iPr_def_10,sK1,X0,k8_isocat_2(sK1,sK2)) = k11_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44111,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_44231,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,k11_cat_2(sK1,sK2),sK2,X0,k9_isocat_2(sK1,sK2)) = k12_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(superposition,[status(thm)],[c_3689,c_120]) ).
tcf(c_44232,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,iPr_def_10,sK2,X0,k9_isocat_2(sK1,sK2)) = k12_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_44231,c_3689]) ).
tcf(c_44233,plain,
! [X0: $i,X1: $i] :
( ( k2_isocat_1(X1,iPr_def_10,sK2,X0,k9_isocat_2(sK1,sK2)) = k12_isocat_2(X1,sK1,sK2,X0) )
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X0,X1,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44232,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_44571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(u2_cat_1(X2))
| v1_xboole_0(u1_cat_1(X0))
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ v1_funct_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)))
| ~ v1_funct_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ m1_relset_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2)) ),
inference(superposition,[status(thm)],[c_123,c_97]) ).
tcf(c_44669,plain,
( m2_nattra_1(iPr_def_16,sK0,sK1,k11_isocat_2(sK0,sK1,sK2,sK3),k11_isocat_2(sK0,sK1,sK2,sK3))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(iPr_def_15,sK0,k11_cat_2(sK1,sK2),sK3,sK3) ),
inference(superposition,[status(thm)],[c_3695,c_109]) ).
tcf(c_44673,plain,
( m2_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3) ),
inference(light_normalisation,[status(thm)],[c_44669,c_3689,c_3692]) ).
tcf(c_44674,plain,
m2_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_44673,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706,c_43386]) ).
tcf(c_44764,plain,
( m1_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_44674,c_90]) ).
tcf(c_44765,plain,
m1_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_44764,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_44766,plain,
( v1_funct_2(iPr_def_16,u1_cat_1(sK0),u2_cat_1(sK1))
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_44765,c_64]) ).
tcf(c_44767,plain,
( v1_funct_1(iPr_def_16)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_44765,c_63]) ).
tcf(c_44768,plain,
v1_funct_1(iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_44767,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_44769,plain,
( v1_funct_2(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(light_normalisation,[status(thm)],[c_44766,c_3690,c_3691]) ).
tcf(c_44770,plain,
v1_funct_2(iPr_def_16,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_44769,c_3702,c_3700,c_3703,c_3701,c_43564]) ).
tcf(c_44876,plain,
( m2_nattra_1(iPr_def_20,sK0,sK2,k12_isocat_2(sK0,sK1,sK2,sK3),k12_isocat_2(sK0,sK1,sK2,sK3))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(iPr_def_15,sK0,k11_cat_2(sK1,sK2),sK3,sK3) ),
inference(superposition,[status(thm)],[c_3699,c_110]) ).
tcf(c_44880,plain,
( m2_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3) ),
inference(light_normalisation,[status(thm)],[c_44876,c_3689,c_3697]) ).
tcf(c_44881,plain,
m2_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_44880,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706,c_43386]) ).
tcf(c_44928,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,k11_cat_2(sK1,sK2),sK1,X2,X3,X0,k8_isocat_2(sK1,sK2)) = k13_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,k11_cat_2(sK1,sK2))
| ~ m2_cat_1(X2,X1,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(superposition,[status(thm)],[c_3689,c_121]) ).
tcf(c_44929,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,iPr_def_10,sK1,X2,X3,X0,k8_isocat_2(sK1,sK2)) = k13_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,iPr_def_10)
| ~ m2_cat_1(X2,X1,iPr_def_10)
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(light_normalisation,[status(thm)],[c_44928,c_3689]) ).
tcf(c_44930,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,iPr_def_10,sK1,X2,X3,X0,k8_isocat_2(sK1,sK2)) = k13_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,iPr_def_10)
| ~ m2_cat_1(X2,X1,iPr_def_10)
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44929,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_45014,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,k11_cat_2(sK1,sK2),sK2,X2,X3,X0,k9_isocat_2(sK1,sK2)) = k14_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,k11_cat_2(sK1,sK2))
| ~ m2_cat_1(X2,X1,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(superposition,[status(thm)],[c_3689,c_122]) ).
tcf(c_45015,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,iPr_def_10,sK2,X2,X3,X0,k9_isocat_2(sK1,sK2)) = k14_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,iPr_def_10)
| ~ m2_cat_1(X2,X1,iPr_def_10)
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(light_normalisation,[status(thm)],[c_45014,c_3689]) ).
tcf(c_45016,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k6_isocat_1(X1,iPr_def_10,sK2,X2,X3,X0,k9_isocat_2(sK1,sK2)) = k14_isocat_2(X1,sK1,sK2,X2,X3,X0) )
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X3,X1,iPr_def_10)
| ~ m2_cat_1(X2,X1,iPr_def_10)
| ~ m2_nattra_1(X0,X1,iPr_def_10,X2,X3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_45015,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_45314,plain,
( m1_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_44881,c_90]) ).
tcf(c_45315,plain,
m1_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_45314,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_45316,plain,
( v1_funct_2(iPr_def_20,u1_cat_1(sK0),u2_cat_1(sK2))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_45315,c_64]) ).
tcf(c_45317,plain,
( v1_funct_1(iPr_def_20)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_45315,c_63]) ).
tcf(c_45318,plain,
v1_funct_1(iPr_def_20),
inference(forward_subsumption_resolution,[status(thm)],[c_45317,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_45319,plain,
( v1_funct_2(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(light_normalisation,[status(thm)],[c_45316,c_3690,c_3696]) ).
tcf(c_45320,plain,
v1_funct_2(iPr_def_20,iPr_def_11,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_45319,c_3704,c_3700,c_3705,c_3701,c_43601]) ).
tcf(c_45673,plain,
( ( k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2)) = k11_isocat_2(sK0,sK1,sK2,sK3) )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0) ),
inference(superposition,[status(thm)],[c_3706,c_44112]) ).
tcf(c_45674,plain,
( ( k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2)) = iPr_def_13 )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_45673,c_3692]) ).
tcf(c_45675,plain,
k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2)) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_45674,c_3700,c_3701]) ).
tcf(c_45742,plain,
( ( k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2)) = k12_isocat_2(sK0,sK1,sK2,sK3) )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0) ),
inference(superposition,[status(thm)],[c_3706,c_44233]) ).
tcf(c_45743,plain,
( ( k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2)) = iPr_def_18 )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_45742,c_3697]) ).
tcf(c_45744,plain,
k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2)) = iPr_def_18,
inference(forward_subsumption_resolution,[status(thm)],[c_45743,c_3700,c_3701]) ).
tcf(c_80236,plain,
( ( k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,iPr_def_15,k8_isocat_2(sK1,sK2)) = k13_isocat_2(sK0,sK1,sK2,sK3,sK3,iPr_def_15) )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_43386,c_44930]) ).
tcf(c_80237,plain,
( ( k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,iPr_def_15,k8_isocat_2(sK1,sK2)) = iPr_def_16 )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_80236,c_3695]) ).
tcf(c_80238,plain,
k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,iPr_def_15,k8_isocat_2(sK1,sK2)) = iPr_def_16,
inference(forward_subsumption_resolution,[status(thm)],[c_80237,c_3700,c_3701,c_3706]) ).
tcf(c_83677,plain,
( ( k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,iPr_def_15,k9_isocat_2(sK1,sK2)) = k14_isocat_2(sK0,sK1,sK2,sK3,sK3,iPr_def_15) )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_43386,c_45016]) ).
tcf(c_83678,plain,
( ( k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,iPr_def_15,k9_isocat_2(sK1,sK2)) = iPr_def_20 )
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_83677,c_3699]) ).
tcf(c_83679,plain,
k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,iPr_def_15,k9_isocat_2(sK1,sK2)) = iPr_def_20,
inference(forward_subsumption_resolution,[status(thm)],[c_83678,c_3700,c_3701,c_3706]) ).
tcf(c_108204,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(u2_cat_1(X2))
| ~ v1_funct_2(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ v1_funct_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)))
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X1,X2)
| ~ v2_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X2)
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4)) ),
inference(global_subsumption_just,[status(thm)],[c_44571,c_117,c_7789]) ).
tcf(c_108205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(u2_cat_1(X2))
| r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ v1_funct_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)))
| ~ v1_funct_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ m1_relset_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2)) ),
inference(renaming,[status(thm)],[c_108204]) ).
tcf(c_108223,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ v1_funct_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)))
| ~ v1_funct_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4))
| ~ m1_relset_1(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4)),u1_cat_1(X0),u2_cat_1(X2))
| ~ m1_relset_1(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2))
| ~ v1_funct_2(k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),u1_cat_1(X0),u2_cat_1(X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_108205,c_118]) ).
tcf(c_108276,plain,
( r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK1),u1_cat_1(sK0),u2_cat_1(sK1),k7_nattra_1(sK0,sK1,iPr_def_13),k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k8_isocat_2(sK1,sK2)))
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_cat_1(k8_isocat_2(sK1,sK2),iPr_def_10,sK1)
| ~ v1_funct_1(k7_nattra_1(sK0,sK1,k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2))))
| ~ v1_funct_1(k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k8_isocat_2(sK1,sK2)))
| ~ m1_relset_1(k7_nattra_1(sK0,sK1,k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2))),u1_cat_1(sK0),u2_cat_1(sK1))
| ~ v1_funct_2(k7_nattra_1(sK0,sK1,k2_isocat_1(sK0,iPr_def_10,sK1,sK3,k8_isocat_2(sK1,sK2))),u1_cat_1(sK0),u2_cat_1(sK1))
| ~ m1_relset_1(k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k8_isocat_2(sK1,sK2)),u1_cat_1(sK0),u2_cat_1(sK1))
| ~ v1_funct_2(k6_isocat_1(sK0,iPr_def_10,sK1,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k8_isocat_2(sK1,sK2)),u1_cat_1(sK0),u2_cat_1(sK1)) ),
inference(superposition,[status(thm)],[c_45675,c_108223]) ).
tcf(c_108277,plain,
( r4_nattra_1(u1_cat_1(sK0),u2_cat_1(sK2),u1_cat_1(sK0),u2_cat_1(sK2),k7_nattra_1(sK0,sK2,iPr_def_18),k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k9_isocat_2(sK1,sK2)))
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_cat_1(k9_isocat_2(sK1,sK2),iPr_def_10,sK2)
| ~ v1_funct_1(k7_nattra_1(sK0,sK2,k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2))))
| ~ v1_funct_1(k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k9_isocat_2(sK1,sK2)))
| ~ m1_relset_1(k7_nattra_1(sK0,sK2,k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2))),u1_cat_1(sK0),u2_cat_1(sK2))
| ~ v1_funct_2(k7_nattra_1(sK0,sK2,k2_isocat_1(sK0,iPr_def_10,sK2,sK3,k9_isocat_2(sK1,sK2))),u1_cat_1(sK0),u2_cat_1(sK2))
| ~ m1_relset_1(k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k9_isocat_2(sK1,sK2)),u1_cat_1(sK0),u2_cat_1(sK2))
| ~ v1_funct_2(k6_isocat_1(sK0,iPr_def_10,sK2,sK3,sK3,k7_nattra_1(sK0,iPr_def_10,sK3),k9_isocat_2(sK1,sK2)),u1_cat_1(sK0),u2_cat_1(sK2)) ),
inference(superposition,[status(thm)],[c_45744,c_108223]) ).
tcf(c_108399,plain,
( r4_nattra_1(iPr_def_11,iPr_def_17,iPr_def_11,iPr_def_17,iPr_def_19,iPr_def_20)
| ~ v1_funct_1(iPr_def_20)
| ~ v1_funct_1(iPr_def_19)
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m1_relset_1(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ m1_relset_1(iPr_def_19,iPr_def_11,iPr_def_17)
| ~ v1_funct_2(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ v1_funct_2(iPr_def_19,iPr_def_11,iPr_def_17)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_cat_1(k9_isocat_2(sK1,sK2),iPr_def_10,sK2) ),
inference(light_normalisation,[status(thm)],[c_108277,c_3690,c_3694,c_3696,c_3698,c_45744,c_83679]) ).
tcf(c_108400,plain,
( r4_nattra_1(iPr_def_11,iPr_def_17,iPr_def_11,iPr_def_17,iPr_def_19,iPr_def_20)
| ~ m1_relset_1(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ m1_relset_1(iPr_def_19,iPr_def_11,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_108399,c_45318,c_43635,c_42753,c_3704,c_3700,c_42851,c_3705,c_3701,c_45320,c_43685,c_3706,c_43235]) ).
tcf(c_108404,plain,
( r4_nattra_1(iPr_def_11,iPr_def_12,iPr_def_11,iPr_def_12,iPr_def_14,iPr_def_16)
| ~ v1_funct_1(iPr_def_16)
| ~ v1_funct_1(iPr_def_14)
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12)
| ~ v1_funct_2(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ v1_funct_2(iPr_def_14,iPr_def_11,iPr_def_12)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_cat_1(k8_isocat_2(sK1,sK2),iPr_def_10,sK1) ),
inference(light_normalisation,[status(thm)],[c_108276,c_3690,c_3691,c_3693,c_3694,c_45675,c_80238]) ).
tcf(c_108405,plain,
( r4_nattra_1(iPr_def_11,iPr_def_12,iPr_def_11,iPr_def_12,iPr_def_14,iPr_def_16)
| ~ m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_108404,c_44768,c_43631,c_42753,c_3702,c_3700,c_42851,c_3703,c_3701,c_44770,c_43687,c_3706,c_43215]) ).
tcf(c_112567,plain,
( ~ m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12)
| ~ r4_nattra_1(iPr_def_11,iPr_def_17,iPr_def_11,iPr_def_17,iPr_def_19,iPr_def_20) ),
inference(superposition,[status(thm)],[c_108405,c_3707]) ).
tcf(c_112581,plain,
( ~ m1_relset_1(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ m1_relset_1(iPr_def_19,iPr_def_11,iPr_def_17)
| ~ m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_108400,c_112567]) ).
tcf(c_312642,plain,
( l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_106]) ).
tcf(c_312643,plain,
( v2_cat_1(iPr_def_10)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1) ),
inference(superposition,[status(thm)],[c_3689,c_105]) ).
tcf(c_312648,plain,
v2_cat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_312643,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_312649,plain,
l1_cat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_312642,c_3704,c_3702,c_3705,c_3703]) ).
tcf(c_312684,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m1_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(superposition,[status(thm)],[c_109,c_90]) ).
tcf(c_312717,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m1_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4))
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
inference(superposition,[status(thm)],[c_110,c_90]) ).
tcf(c_313526,plain,
( m2_cat_1(iPr_def_13,sK0,sK1)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_3692,c_107]) ).
tcf(c_313529,plain,
( m2_cat_1(iPr_def_13,sK0,sK1)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_313526,c_3689]) ).
tcf(c_313530,plain,
m2_cat_1(iPr_def_13,sK0,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_313529,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706]) ).
tcf(c_313557,plain,
( m2_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_3693,c_113]) ).
tcf(c_313558,plain,
m2_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_313557,c_3702,c_3700,c_3703,c_3701,c_313530]) ).
tcf(c_313566,plain,
( m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3)
| ~ l1_cat_1(iPr_def_10)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(iPr_def_10)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_3694,c_113]) ).
tcf(c_313567,plain,
m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_313566,c_312649,c_3700,c_312648,c_3701,c_3706]) ).
tcf(c_313597,plain,
( m2_cat_1(iPr_def_18,sK0,sK2)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_3697,c_108]) ).
tcf(c_313600,plain,
( m2_cat_1(iPr_def_18,sK0,sK2)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_313597,c_3689]) ).
tcf(c_313601,plain,
m2_cat_1(iPr_def_18,sK0,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_313600,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706]) ).
tcf(c_313637,plain,
( ( k7_nattra_1(sK0,sK2,iPr_def_18) = k4_nattra_1(sK0,sK2,iPr_def_18) )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0) ),
inference(superposition,[status(thm)],[c_313601,c_102]) ).
tcf(c_313640,plain,
( ( k4_nattra_1(sK0,sK2,iPr_def_18) = iPr_def_19 )
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_313637,c_3698]) ).
tcf(c_313641,plain,
k4_nattra_1(sK0,sK2,iPr_def_18) = iPr_def_19,
inference(forward_subsumption_resolution,[status(thm)],[c_313640,c_3704,c_3700,c_3705,c_3701]) ).
tcf(c_313862,plain,
( m1_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_313558,c_90]) ).
tcf(c_313863,plain,
m1_nattra_1(iPr_def_14,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_313862,c_3702,c_3700,c_3703,c_3701,c_313530]) ).
tcf(c_313889,plain,
( m1_relset_1(iPr_def_14,u1_cat_1(sK0),u2_cat_1(sK1))
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_313863,c_1747]) ).
tcf(c_313895,plain,
( m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(light_normalisation,[status(thm)],[c_313889,c_3690,c_3691]) ).
tcf(c_313896,plain,
m1_relset_1(iPr_def_14,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_313895,c_3702,c_3700,c_3703,c_3701,c_313530]) ).
tcf(c_314798,plain,
( m1_nattra_1(iPr_def_19,sK0,sK2,iPr_def_18,iPr_def_18)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_313641,c_86]) ).
tcf(c_314800,plain,
m1_nattra_1(iPr_def_19,sK0,sK2,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_314798,c_3704,c_3700,c_3705,c_3701,c_313601]) ).
tcf(c_315101,plain,
( m1_relset_1(iPr_def_19,u1_cat_1(sK0),u2_cat_1(sK2))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_314800,c_1747]) ).
tcf(c_315104,plain,
( m1_relset_1(iPr_def_19,iPr_def_11,iPr_def_17)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(light_normalisation,[status(thm)],[c_315101,c_3690,c_3696]) ).
tcf(c_315105,plain,
m1_relset_1(iPr_def_19,iPr_def_11,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_315104,c_3704,c_3700,c_3705,c_3701,c_313601]) ).
tcf(c_316347,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m1_nattra_1(k13_isocat_2(X1,X2,X3,X4,X5,X0),X1,X2,k11_isocat_2(X1,X2,X3,X4),k11_isocat_2(X1,X2,X3,X5))
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_312684,c_107,c_107]) ).
tcf(c_316378,plain,
( m1_nattra_1(iPr_def_16,sK0,sK1,k11_isocat_2(sK0,sK1,sK2,sK3),k11_isocat_2(sK0,sK1,sK2,sK3))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(iPr_def_15,sK0,k11_cat_2(sK1,sK2),sK3,sK3) ),
inference(superposition,[status(thm)],[c_3695,c_316347]) ).
tcf(c_316384,plain,
( m1_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3) ),
inference(light_normalisation,[status(thm)],[c_316378,c_3689,c_3692]) ).
tcf(c_316385,plain,
m1_nattra_1(iPr_def_16,sK0,sK1,iPr_def_13,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_316384,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706,c_313567]) ).
tcf(c_316505,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m1_nattra_1(k14_isocat_2(X1,X2,X3,X4,X5,X0),X1,X3,k12_isocat_2(X1,X2,X3,X4),k12_isocat_2(X1,X2,X3,X5))
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X5,X1,k11_cat_2(X2,X3))
| ~ m2_cat_1(X4,X1,k11_cat_2(X2,X3))
| ~ m2_nattra_1(X0,X1,k11_cat_2(X2,X3),X4,X5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_312717,c_108,c_108]) ).
tcf(c_316536,plain,
( m1_nattra_1(iPr_def_20,sK0,sK2,k12_isocat_2(sK0,sK1,sK2,sK3),k12_isocat_2(sK0,sK1,sK2,sK3))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,k11_cat_2(sK1,sK2))
| ~ m2_nattra_1(iPr_def_15,sK0,k11_cat_2(sK1,sK2),sK3,sK3) ),
inference(superposition,[status(thm)],[c_3699,c_316505]) ).
tcf(c_316542,plain,
( m1_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(sK3,sK0,iPr_def_10)
| ~ m2_nattra_1(iPr_def_15,sK0,iPr_def_10,sK3,sK3) ),
inference(light_normalisation,[status(thm)],[c_316536,c_3689,c_3697]) ).
tcf(c_316543,plain,
m1_nattra_1(iPr_def_20,sK0,sK2,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_316542,c_3704,c_3702,c_3700,c_3705,c_3703,c_3701,c_3706,c_313567]) ).
tcf(c_316598,plain,
( m1_relset_1(iPr_def_16,u1_cat_1(sK0),u2_cat_1(sK1))
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(superposition,[status(thm)],[c_316385,c_1747]) ).
tcf(c_316604,plain,
( m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12)
| ~ l1_cat_1(sK1)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK1)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_13,sK0,sK1) ),
inference(light_normalisation,[status(thm)],[c_316598,c_3690,c_3691]) ).
tcf(c_316605,plain,
m1_relset_1(iPr_def_16,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_316604,c_3702,c_3700,c_3703,c_3701,c_313530]) ).
tcf(c_317864,plain,
( m1_relset_1(iPr_def_20,u1_cat_1(sK0),u2_cat_1(sK2))
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(superposition,[status(thm)],[c_316543,c_1747]) ).
tcf(c_317870,plain,
( m1_relset_1(iPr_def_20,iPr_def_11,iPr_def_17)
| ~ l1_cat_1(sK2)
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK2)
| ~ v2_cat_1(sK0)
| ~ m2_cat_1(iPr_def_18,sK0,sK2) ),
inference(light_normalisation,[status(thm)],[c_317864,c_3690,c_3696]) ).
tcf(c_317871,plain,
m1_relset_1(iPr_def_20,iPr_def_11,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_317870,c_3704,c_3700,c_3705,c_3701,c_313601]) ).
tcf(c_317872,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_317871,c_316605,c_315105,c_313896,c_112581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CAT027+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.41 % Computer : n009.cluster.edu
% 0.18/0.41 % Model : x86_64 x86_64
% 0.18/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.41 % Memory : 8046.5625MB
% 0.18/0.41 % OS : Linux 6.8.0-71-generic
% 0.18/0.41 % CPULimit : 300
% 0.18/0.41 % WCLimit : 300
% 0.18/0.41 % DateTime : Fri Sep 25 07:02:28 UTC 2026
% 0.18/0.42 % CPUTime :
% 0.18/0.42 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.46 Running first-order theorem proving
% 0.18/0.46 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.18/0.47
% 0.18/0.47 % ======== iProver multi-core TPTP/SMT =========
% 0.18/0.47
% 0.18/0.47 % Detected problem language: tptp
% 0.22/0.49 % Proving...
% 177.58/27.16 % SZS status Started for theBenchmark.p
% 177.58/27.16 % SZS status Theorem for theBenchmark.p
% 177.58/27.16
% 177.58/27.16 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 177.58/27.16
% 177.58/27.16 % ------ iProver source info
% 177.58/27.16
% 177.58/27.16 % git: date: 2026-07-19 20:42:38 +0200
% 177.58/27.16 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 177.58/27.16 % git: non_committed_changes: false
% 177.58/27.16
% 177.58/27.16 % ------ Parsing...
% 177.58/27.16 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 177.58/27.16
% 177.58/27.16 % ------ Preprocessing... sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 177.58/27.16
% 177.58/27.16 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 177.58/27.16
% 177.58/27.16 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 177.58/27.16 % ------ Proving...
% 177.58/27.16 % ------ Problem Properties
% 177.58/27.16
% 177.58/27.16 %
% 177.58/27.16 % clauses 81
% 177.58/27.16 % conjectures 8
% 177.58/27.16 % EPR 25
% 177.58/27.16 % Horn 74
% 177.58/27.16 % unary 29
% 177.58/27.16 % binary 10
% 177.58/27.16 % lits 346
% 177.58/27.16 % lits eq 22
% 177.58/27.16 % fd_pure 0
% 177.58/27.16 % fd_pseudo 0
% 177.58/27.16 % fd_cond 1
% 177.58/27.16 % fd_pseudo_cond 2
% 177.58/27.16 % AC symbols 0
% 177.58/27.16
% 177.58/27.16 % ------ Schedule dynamic 5 is on
% 177.58/27.16
% 177.58/27.16 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 % ------
% 177.58/27.16 % Current options:
% 177.58/27.16 % ------
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 %
% 177.58/27.16
% 177.58/27.16 % ------ Proving...
% 177.58/27.16 % Proof_search_loop: time out after: 5494 full_loop iterations
% 177.58/27.16
% 177.58/27.16 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 % ------
% 177.58/27.16 % Current options:
% 177.58/27.16 % ------
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 %
% 177.58/27.16
% 177.58/27.16 % ------ Proving...
% 177.58/27.16 % Proof_search_loop: time out after: 4883 full_loop iterations
% 177.58/27.16
% 177.58/27.16 % ------ Option_1: Negative Selections Time Limit: 35.
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 % ------
% 177.58/27.16 % Current options:
% 177.58/27.16 % ------
% 177.58/27.16
% 177.58/27.16
% 177.58/27.16 %
% 177.58/27.16
% 177.58/27.16 % ------ Proving...
% 177.58/27.16 %
% 177.58/27.16
% 177.58/27.16 % SZS status Theorem for theBenchmark.p
% 177.58/27.16
% 177.58/27.16 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 177.58/27.18
% 177.58/27.18
%------------------------------------------------------------------------------