%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT027+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 : Tue Sep 29 09:36:43 AM UTC 2026
% Result : Theorem 41.61s 11.23s
% Output : Refutation 61.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 45
% Syntax : Number of formulae : 479 ( 45 unt; 23 def)
% Number of atoms : 2684 ( 52 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 4168 (1963 ~;2003 |; 127 &)
% ( 24 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 24 prp; 0-6 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-7 aty)
% Number of variables : 644 ( 0 sgn 636 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f17929,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_cat_1) ).
fof(f17930,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u2_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_cat_1) ).
fof(f21083,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_cat_2) ).
fof(f21181,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f25780,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1)
& m2_cat_1(X3,X0,X1) )
=> ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
=> ( v1_funct_1(X4)
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_nattra_1) ).
fof(f25782,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1)
& m2_cat_1(X3,X0,X1) )
=> ! [X4] :
( m2_nattra_1(X4,X0,X1,X2,X3)
=> m1_nattra_1(X4,X0,X1,X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_nattra_1) ).
fof(f25791,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X2)
& ~ v1_xboole_0(X3)
& v1_funct_1(X4)
& v1_funct_2(X4,X0,X1)
& m1_relset_1(X4,X0,X1)
& v1_funct_1(X5)
& v1_funct_2(X5,X2,X3)
& m1_relset_1(X5,X2,X3) )
=> ( r4_nattra_1(X0,X1,X2,X3,X4,X5)
=> r4_nattra_1(X0,X1,X2,X3,X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r4_nattra_1) ).
fof(f25802,axiom,
! [X0,X1,X2] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1) )
=> m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_nattra_1) ).
fof(f27617,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_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/sandbox/benchmark/theBenchmark.p',t38_isocat_1) ).
fof(f27649,axiom,
! [X0,X1,X2,X3,X4] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,X1)
& m2_cat_1(X4,X1,X2) )
=> m2_cat_1(k2_isocat_1(X0,X1,X2,X3,X4),X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_isocat_1) ).
fof(f29039,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f29041,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f29045,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
=> m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_isocat_2) ).
fof(f29046,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
=> m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_isocat_2) ).
fof(f29047,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_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) )
=> 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/sandbox/benchmark/theBenchmark.p',dt_k13_isocat_2) ).
fof(f29048,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_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) )
=> 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/sandbox/benchmark/theBenchmark.p',dt_k14_isocat_2) ).
fof(f29095,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_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/sandbox/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f29096,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_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/sandbox/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f29099,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_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/sandbox/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f29100,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_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/sandbox/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f29103,conjecture,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ( 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)))
& 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))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_isocat_2) ).
fof(f29104,negated_conjecture,
~ ! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ( 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)))
& 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))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f29103]) ).
fof(f29276,plain,
? [X0] :
( ? [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)))
| ~ 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))) )
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29104]) ).
fof(f29277,plain,
? [X0] :
( ? [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)))
| ~ 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))) )
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(flattening,[],[f29276]) ).
fof(f29278,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f17930]) ).
fof(f29279,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f17929]) ).
fof(f29298,plain,
! [X0,X1,X2,X3,X4,X5] :
( r4_nattra_1(X0,X1,X2,X3,X5,X4)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| v1_xboole_0(X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X0,X1)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,X2,X3)
| ~ m1_relset_1(X5,X2,X3) ),
inference(ennf_transformation,[],[f25791]) ).
fof(f29299,plain,
! [X0,X1,X2,X3,X4,X5] :
( r4_nattra_1(X0,X1,X2,X3,X5,X4)
| ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| v1_xboole_0(X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X0,X1)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,X2,X3)
| ~ m1_relset_1(X5,X2,X3) ),
inference(flattening,[],[f29298]) ).
fof(f29306,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21181]) ).
fof(f29307,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f29306]) ).
fof(f29324,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( 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)))
| ~ m2_cat_1(X4,X1,X2) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f27617]) ).
fof(f29325,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( 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)))
| ~ m2_cat_1(X4,X1,X2) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29324]) ).
fof(f29330,plain,
! [X0,X1,X2] :
( m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f25802]) ).
fof(f29331,plain,
! [X0,X1,X2] :
( m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(flattening,[],[f29330]) ).
fof(f29344,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29095]) ).
fof(f29345,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29344]) ).
fof(f29346,plain,
! [X0,X1,X2,X3,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(ennf_transformation,[],[f29047]) ).
fof(f29347,plain,
! [X0,X1,X2,X3,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(flattening,[],[f29346]) ).
fof(f29348,plain,
! [X0,X1,X2,X3] :
( m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(ennf_transformation,[],[f29045]) ).
fof(f29349,plain,
! [X0,X1,X2,X3] :
( m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(flattening,[],[f29348]) ).
fof(f29350,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29096]) ).
fof(f29351,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29350]) ).
fof(f29352,plain,
! [X0,X1,X2,X3,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(ennf_transformation,[],[f29048]) ).
fof(f29353,plain,
! [X0,X1,X2,X3,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(flattening,[],[f29352]) ).
fof(f29354,plain,
! [X0,X1,X2,X3] :
( m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(ennf_transformation,[],[f29046]) ).
fof(f29355,plain,
! [X0,X1,X2,X3] :
( m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(flattening,[],[f29354]) ).
fof(f29358,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( 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))
| ~ 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)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29099]) ).
fof(f29359,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( 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))
| ~ 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)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29358]) ).
fof(f29360,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( 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))
| ~ 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)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29100]) ).
fof(f29361,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( 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))
| ~ 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)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29360]) ).
fof(f29712,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
| ~ m2_nattra_1(X4,X0,X1,X2,X3) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f25782]) ).
fof(f29713,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
| ~ m2_nattra_1(X4,X0,X1,X2,X3) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(flattening,[],[f29712]) ).
fof(f30167,plain,
! [X0,X1,X2,X3,X4] :
( m2_cat_1(k2_isocat_1(X0,X1,X2,X3,X4),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f27649]) ).
fof(f30168,plain,
! [X0,X1,X2,X3,X4] :
( m2_cat_1(k2_isocat_1(X0,X1,X2,X3,X4),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X1,X2) ),
inference(flattening,[],[f30167]) ).
fof(f30201,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1)) )
| ~ m1_nattra_1(X4,X0,X1,X2,X3) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f25780]) ).
fof(f30202,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1)) )
| ~ m1_nattra_1(X4,X0,X1,X2,X3) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(flattening,[],[f30201]) ).
fof(f30225,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29039]) ).
fof(f30226,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f30225]) ).
fof(f30229,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29041]) ).
fof(f30230,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f30229]) ).
fof(f32757,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21083]) ).
fof(f32758,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f32757]) ).
fof(f33461,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| ~ r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) )
& m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
& v2_cat_1(sK98)
& l1_cat_1(sK98)
& v2_cat_1(sK97)
& l1_cat_1(sK97)
& v2_cat_1(sK96)
& l1_cat_1(sK96) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96,sK97,sK98,sK99]),skolemize(X0,sK96),skolemize(X1,sK97),skolemize(X2,sK98),skolemize(X3,sK99)],[f29277]) ).
fof(f33617,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,[],[f1483]) ).
fof(f34739,plain,
l1_cat_1(sK96),
inference(cnf_transformation,[],[f33461]) ).
fof(f34740,plain,
v2_cat_1(sK96),
inference(cnf_transformation,[],[f33461]) ).
fof(f34741,plain,
l1_cat_1(sK97),
inference(cnf_transformation,[],[f33461]) ).
fof(f34742,plain,
v2_cat_1(sK97),
inference(cnf_transformation,[],[f33461]) ).
fof(f34743,plain,
l1_cat_1(sK98),
inference(cnf_transformation,[],[f33461]) ).
fof(f34744,plain,
v2_cat_1(sK98),
inference(cnf_transformation,[],[f33461]) ).
fof(f34745,plain,
m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98)),
inference(cnf_transformation,[],[f33461]) ).
fof(f34746,plain,
( ~ r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| ~ r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) ),
inference(cnf_transformation,[],[f33461]) ).
fof(f34747,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29278]) ).
fof(f34748,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29279]) ).
fof(f34765,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r4_nattra_1(X0,X1,X2,X3,X4,X5)
| r4_nattra_1(X0,X1,X2,X3,X5,X4)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| v1_xboole_0(X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X0,X1)
| ~ m1_relset_1(X4,X0,X1)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,X2,X3)
| ~ m1_relset_1(X5,X2,X3) ),
inference(cnf_transformation,[],[f29299]) ).
fof(f34773,plain,
! [X0,X1] :
( l1_cat_1(k11_cat_2(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29307]) ).
fof(f34783,plain,
! [X2,X3,X0,X1,X4] :
( 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)))
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29325]) ).
fof(f34786,plain,
! [X2,X0,X1] :
( m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f29331]) ).
fof(f34796,plain,
! [X2,X3,X0,X1] :
( ~ 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))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29345]) ).
fof(f34797,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(cnf_transformation,[],[f29347]) ).
fof(f34798,plain,
! [X2,X3,X0,X1] :
( m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(cnf_transformation,[],[f29349]) ).
fof(f34799,plain,
! [X2,X3,X0,X1] :
( ~ 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))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29351]) ).
fof(f34800,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(cnf_transformation,[],[f29353]) ).
fof(f34801,plain,
! [X2,X3,X0,X1] :
( m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(cnf_transformation,[],[f29355]) ).
fof(f34803,plain,
! [X2,X3,X0,X1,X4,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))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29359]) ).
fof(f34804,plain,
! [X2,X3,X0,X1,X4,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))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29361]) ).
fof(f35346,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_nattra_1(X4,X0,X1,X2,X3)
| m1_nattra_1(X4,X0,X1,X2,X3)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f29713]) ).
fof(f35415,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f33617]) ).
fof(f36069,plain,
! [X2,X3,X0,X1,X4] :
( m2_cat_1(k2_isocat_1(X0,X1,X2,X3,X4),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f30168]) ).
fof(f36116,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X4,X0,X1,X2,X3)
| m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f30202]) ).
fof(f36117,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X4,X0,X1,X2,X3)
| v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f30202]) ).
fof(f36118,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X4,X0,X1,X2,X3)
| v1_funct_1(X4)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f30202]) ).
fof(f36133,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f30226]) ).
fof(f36135,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f30230]) ).
fof(f39271,plain,
! [X0,X1] :
( v2_cat_1(k11_cat_2(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f32758]) ).
fof(f42629,definition,
( spl916_20
<=> r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_20])],[avatar_definition]) ).
fof(f42633,definition,
( spl916_21
<=> r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_21])],[avatar_definition]) ).
fof(f42635,plain,
( ~ r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| spl916_21 ),
inference(avatar_component_clause,[],[f42633]) ).
fof(f42636,plain,
( ~ spl916_20
| ~ spl916_21 ),
inference(avatar_split_clause,[],[f34746,f42633,f42629]) ).
fof(f42846,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(resolution,[],[f34799,f34745]) ).
fof(f42853,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42846,f34744]) ).
fof(f42856,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42853,f34743]) ).
fof(f42857,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42856,f34742]) ).
fof(f42858,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42857,f34741]) ).
fof(f42859,plain,
( k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42858,f34740]) ).
fof(f42860,plain,
k12_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,k9_isocat_2(sK97,sK98)),
inference(forward_subsumption_resolution,[],[f42859,f34739]) ).
fof(f42861,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(resolution,[],[f34796,f34745]) ).
fof(f42868,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42861,f34744]) ).
fof(f42871,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42868,f34743]) ).
fof(f42872,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42871,f34742]) ).
fof(f42873,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42872,f34741]) ).
fof(f42874,plain,
( k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42873,f34740]) ).
fof(f42875,plain,
k11_isocat_2(sK96,sK97,sK98,sK99) = k2_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,k8_isocat_2(sK97,sK98)),
inference(forward_subsumption_resolution,[],[f42874,f34739]) ).
fof(f42876,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(superposition,[],[f34783,f42860]) ).
fof(f42877,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(superposition,[],[f34783,f42875]) ).
fof(f42878,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42877,f34745]) ).
fof(f42879,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42876,f34745]) ).
fof(f42880,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42878,f34742]) ).
fof(f42881,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42879,f34744]) ).
fof(f42882,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42880,f34741]) ).
fof(f42883,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42881,f34743]) ).
fof(f42884,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42882,f34740]) ).
fof(f42885,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f42883,f34740]) ).
fof(f42886,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98)) ),
inference(forward_subsumption_resolution,[],[f42884,f34739]) ).
fof(f42887,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98)) ),
inference(forward_subsumption_resolution,[],[f42885,f34739]) ).
fof(f42889,definition,
( spl916_27
<=> l1_cat_1(k11_cat_2(sK97,sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_27])],[avatar_definition]) ).
fof(f42890,plain,
( l1_cat_1(k11_cat_2(sK97,sK98))
| ~ spl916_27 ),
inference(avatar_component_clause,[],[f42889]) ).
fof(f42891,plain,
( ~ l1_cat_1(k11_cat_2(sK97,sK98))
| spl916_27 ),
inference(avatar_component_clause,[],[f42889]) ).
fof(f42893,definition,
( spl916_28
<=> v2_cat_1(k11_cat_2(sK97,sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_28])],[avatar_definition]) ).
fof(f42894,plain,
( v2_cat_1(k11_cat_2(sK97,sK98))
| ~ spl916_28 ),
inference(avatar_component_clause,[],[f42893]) ).
fof(f42895,plain,
( ~ v2_cat_1(k11_cat_2(sK97,sK98))
| spl916_28 ),
inference(avatar_component_clause,[],[f42893]) ).
fof(f42897,definition,
( spl916_29
<=> m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97) ),
introduced(definition,[new_symbols(definition,[spl916_29])],[avatar_definition]) ).
fof(f42898,plain,
( m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_29 ),
inference(avatar_component_clause,[],[f42897]) ).
fof(f42899,plain,
( ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| spl916_29 ),
inference(avatar_component_clause,[],[f42897]) ).
fof(f42901,definition,
( spl916_30
<=> r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_30])],[avatar_definition]) ).
fof(f42903,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ spl916_30 ),
inference(avatar_component_clause,[],[f42901]) ).
fof(f42904,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_30 ),
inference(avatar_split_clause,[],[f42886,f42901,f42897,f42893,f42889]) ).
fof(f42906,definition,
( spl916_31
<=> m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98) ),
introduced(definition,[new_symbols(definition,[spl916_31])],[avatar_definition]) ).
fof(f42907,plain,
( m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_31 ),
inference(avatar_component_clause,[],[f42906]) ).
fof(f42908,plain,
( ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| spl916_31 ),
inference(avatar_component_clause,[],[f42906]) ).
fof(f42910,definition,
( spl916_32
<=> r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_32])],[avatar_definition]) ).
fof(f42912,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ spl916_32 ),
inference(avatar_component_clause,[],[f42910]) ).
fof(f42913,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_32 ),
inference(avatar_split_clause,[],[f42887,f42910,f42906,f42893,f42889]) ).
fof(f42914,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_27 ),
inference(resolution,[],[f42891,f34773]) ).
fof(f42915,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_27 ),
inference(forward_subsumption_resolution,[],[f42914,f34742]) ).
fof(f42916,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_27 ),
inference(forward_subsumption_resolution,[],[f42915,f34741]) ).
fof(f42917,plain,
( ~ l1_cat_1(sK98)
| spl916_27 ),
inference(forward_subsumption_resolution,[],[f42916,f34744]) ).
fof(f42918,plain,
( $false
| spl916_27 ),
inference(forward_subsumption_resolution,[],[f42917,f34743]) ).
fof(f42919,plain,
spl916_27,
inference(avatar_contradiction_clause,[],[f42918]) ).
fof(f42920,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_28 ),
inference(resolution,[],[f42895,f39271]) ).
fof(f42921,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_28 ),
inference(forward_subsumption_resolution,[],[f42920,f34742]) ).
fof(f42922,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_28 ),
inference(forward_subsumption_resolution,[],[f42921,f34741]) ).
fof(f42923,plain,
( ~ l1_cat_1(sK98)
| spl916_28 ),
inference(forward_subsumption_resolution,[],[f42922,f34744]) ).
fof(f42924,plain,
( $false
| spl916_28 ),
inference(forward_subsumption_resolution,[],[f42923,f34743]) ).
fof(f42925,plain,
spl916_28,
inference(avatar_contradiction_clause,[],[f42924]) ).
fof(f42926,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_29 ),
inference(resolution,[],[f36133,f42899]) ).
fof(f42931,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_29 ),
inference(forward_subsumption_resolution,[],[f42926,f34742]) ).
fof(f42934,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_29 ),
inference(forward_subsumption_resolution,[],[f42931,f34741]) ).
fof(f42937,plain,
( ~ l1_cat_1(sK98)
| spl916_29 ),
inference(forward_subsumption_resolution,[],[f42934,f34744]) ).
fof(f42938,plain,
( $false
| spl916_29 ),
inference(forward_subsumption_resolution,[],[f42937,f34743]) ).
fof(f42939,plain,
spl916_29,
inference(avatar_contradiction_clause,[],[f42938]) ).
fof(f42940,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_31 ),
inference(resolution,[],[f36135,f42908]) ).
fof(f42945,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_31 ),
inference(forward_subsumption_resolution,[],[f42940,f34742]) ).
fof(f42948,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| spl916_31 ),
inference(forward_subsumption_resolution,[],[f42945,f34741]) ).
fof(f42951,plain,
( ~ l1_cat_1(sK98)
| spl916_31 ),
inference(forward_subsumption_resolution,[],[f42948,f34744]) ).
fof(f42952,plain,
( $false
| spl916_31 ),
inference(forward_subsumption_resolution,[],[f42951,f34743]) ).
fof(f42953,plain,
spl916_31,
inference(avatar_contradiction_clause,[],[f42952]) ).
fof(f42954,plain,
! [X2,X3,X0,X1] :
( k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(resolution,[],[f34803,f34786]) ).
fof(f42955,plain,
! [X2,X3,X0,X1] :
( k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2)) ),
inference(duplicate_literal_removal,[],[f42954]) ).
fof(f42956,plain,
! [X2,X3,X0,X1] :
( k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f42955,f34773]) ).
fof(f42957,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k8_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f42956,f39271]) ).
fof(f42958,plain,
! [X2,X3,X0,X1] :
( k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(resolution,[],[f34804,f34786]) ).
fof(f42959,plain,
! [X2,X3,X0,X1] :
( k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2)) ),
inference(duplicate_literal_removal,[],[f42958]) ).
fof(f42960,plain,
! [X2,X3,X0,X1] :
( k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f42959,f34773]) ).
fof(f42961,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3),k9_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f42960,f39271]) ).
fof(f43068,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(resolution,[],[f42957,f34745]) ).
fof(f43071,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43068,f34744]) ).
fof(f43076,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43071,f34743]) ).
fof(f43081,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43076,f34742]) ).
fof(f43082,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43081,f34741]) ).
fof(f43083,plain,
( k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43082,f34740]) ).
fof(f43084,plain,
k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),
inference(forward_subsumption_resolution,[],[f43083,f34739]) ).
fof(f43128,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(resolution,[],[f42961,f34745]) ).
fof(f43131,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43128,f34744]) ).
fof(f43136,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43131,f34743]) ).
fof(f43141,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43136,f34742]) ).
fof(f43142,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43141,f34741]) ).
fof(f43143,plain,
( k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98))
| ~ l1_cat_1(sK96) ),
inference(forward_subsumption_resolution,[],[f43142,f34740]) ).
fof(f43144,plain,
k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)) = k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),
inference(forward_subsumption_resolution,[],[f43143,f34739]) ).
fof(f43510,plain,
! [X2,X0,X1] :
( m1_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(resolution,[],[f35346,f34786]) ).
fof(f43511,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(resolution,[],[f35346,f34797]) ).
fof(f43512,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(resolution,[],[f35346,f34800]) ).
fof(f43513,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(duplicate_literal_removal,[],[f43512]) ).
fof(f43514,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(duplicate_literal_removal,[],[f43511]) ).
fof(f43515,plain,
! [X2,X0,X1] :
( m1_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(duplicate_literal_removal,[],[f43510]) ).
fof(f43516,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(forward_subsumption_resolution,[],[f43513,f34801]) ).
fof(f43517,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(forward_subsumption_resolution,[],[f43514,f34798]) ).
fof(f43518,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(forward_subsumption_resolution,[],[f43516,f34801]) ).
fof(f43519,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(forward_subsumption_resolution,[],[f43517,f34798]) ).
fof(f43520,plain,
! [X2,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| v1_funct_2(k7_nattra_1(X0,X1,X2),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(resolution,[],[f43515,f36117]) ).
fof(f43521,plain,
! [X2,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| m2_relset_1(k7_nattra_1(X0,X1,X2),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(resolution,[],[f43515,f36116]) ).
fof(f43522,plain,
! [X2,X0,X1] :
( m2_relset_1(k7_nattra_1(X0,X1,X2),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X0) ),
inference(duplicate_literal_removal,[],[f43521]) ).
fof(f43523,plain,
! [X2,X0,X1] :
( v1_funct_2(k7_nattra_1(X0,X1,X2),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X0) ),
inference(duplicate_literal_removal,[],[f43520]) ).
fof(f43524,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| v1_funct_2(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1) ),
inference(resolution,[],[f43519,f36117]) ).
fof(f43525,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| m2_relset_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1) ),
inference(resolution,[],[f43519,f36116]) ).
fof(f43526,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| m2_relset_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1) ),
inference(duplicate_literal_removal,[],[f43525]) ).
fof(f43527,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| v1_funct_2(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1) ),
inference(duplicate_literal_removal,[],[f43524]) ).
fof(f43528,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| m2_relset_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(forward_subsumption_resolution,[],[f43526,f34798]) ).
fof(f43529,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| v1_funct_2(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
inference(forward_subsumption_resolution,[],[f43527,f34798]) ).
fof(f43530,plain,
! [X2,X3,X0,X1,X4,X5] :
( m2_relset_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43528,f34798]) ).
fof(f43531,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_2(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43529,f34798]) ).
fof(f43532,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| v1_funct_2(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X3),X0,X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(resolution,[],[f43518,f36117]) ).
fof(f43533,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| m2_relset_1(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X3),X0,X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(resolution,[],[f43518,f36116]) ).
fof(f43534,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| m2_relset_1(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X3),X0,X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(duplicate_literal_removal,[],[f43533]) ).
fof(f43535,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| v1_funct_2(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X3),X0,X1)
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(duplicate_literal_removal,[],[f43532]) ).
fof(f43536,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| m2_relset_1(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(forward_subsumption_resolution,[],[f43534,f34801]) ).
fof(f43537,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| v1_funct_2(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ m2_cat_1(k12_isocat_2(X0,X2,X1,X4),X0,X1) ),
inference(forward_subsumption_resolution,[],[f43535,f34801]) ).
fof(f43538,plain,
! [X2,X3,X0,X1,X4,X5] :
( m2_relset_1(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43536,f34801]) ).
fof(f43539,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_2(k14_isocat_2(X0,X2,X1,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X4,X0,k11_cat_2(X2,X1))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X2,X1),X3,X4)
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43537,f34801]) ).
fof(f43573,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98) ),
inference(superposition,[],[f36069,f42860]) ).
fof(f43574,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97) ),
inference(superposition,[],[f36069,f42875]) ).
fof(f43587,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97) ),
inference(forward_subsumption_resolution,[],[f43574,f34740]) ).
fof(f43588,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98) ),
inference(forward_subsumption_resolution,[],[f43573,f34740]) ).
fof(f43598,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97) ),
inference(forward_subsumption_resolution,[],[f43587,f34739]) ).
fof(f43599,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98) ),
inference(forward_subsumption_resolution,[],[f43588,f34739]) ).
fof(f43609,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43598,f42894]) ).
fof(f43610,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43599,f42894]) ).
fof(f43614,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43609,f42890]) ).
fof(f43615,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43610,f42890]) ).
fof(f43619,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43614,f34742]) ).
fof(f43620,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43615,f34744]) ).
fof(f43621,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43619,f34741]) ).
fof(f43622,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43620,f34743]) ).
fof(f43623,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ m2_cat_1(k8_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK97)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43621,f34745]) ).
fof(f43624,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ m2_cat_1(k9_isocat_2(sK97,sK98),k11_cat_2(sK97,sK98),sK98)
| ~ spl916_27
| ~ spl916_28 ),
inference(forward_subsumption_resolution,[],[f43622,f34745]) ).
fof(f43625,plain,
( m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29 ),
inference(forward_subsumption_resolution,[],[f43623,f42898]) ).
fof(f43626,plain,
( m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31 ),
inference(forward_subsumption_resolution,[],[f43624,f42907]) ).
fof(f43918,plain,
! [X2,X0,X1] :
( v1_funct_1(k7_nattra_1(X0,X1,X2))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(resolution,[],[f36118,f43515]) ).
fof(f43919,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(resolution,[],[f36118,f43519]) ).
fof(f43920,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k14_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(resolution,[],[f36118,f43518]) ).
fof(f43921,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k14_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(duplicate_literal_removal,[],[f43920]) ).
fof(f43922,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X4),X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(duplicate_literal_removal,[],[f43919]) ).
fof(f43923,plain,
! [X2,X0,X1] :
( v1_funct_1(k7_nattra_1(X0,X1,X2))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1) ),
inference(duplicate_literal_removal,[],[f43918]) ).
fof(f43924,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k14_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(k12_isocat_2(X0,X1,X2,X4),X0,X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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) ),
inference(forward_subsumption_resolution,[],[f43921,f34801]) ).
fof(f43925,plain,
! [X2,X3,X0,X1,X4,X5] :
( v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X4,X5))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_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) ),
inference(forward_subsumption_resolution,[],[f43922,f34798]) ).
fof(f43926,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| v1_funct_1(k14_isocat_2(X0,X1,X2,X3,X4,X5)) ),
inference(forward_subsumption_resolution,[],[f43924,f34801]) ).
fof(f43927,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X4,X5)) ),
inference(forward_subsumption_resolution,[],[f43925,f34798]) ).
fof(f43928,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) ),
inference(resolution,[],[f43927,f34786]) ).
fof(f43933,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2)) ),
inference(duplicate_literal_removal,[],[f43928]) ).
fof(f43936,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ v2_cat_1(k11_cat_2(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f43933,f34773]) ).
fof(f43939,plain,
! [X2,X3,X0,X1] :
( v1_funct_1(k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43936,f39271]) ).
fof(f43940,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| v1_funct_1(k14_isocat_2(X0,X2,X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X2,X1),X3)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X2,X1))
| ~ l1_cat_1(k11_cat_2(X2,X1))
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1)) ),
inference(resolution,[],[f43926,f34786]) ).
fof(f43945,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| v1_funct_1(k14_isocat_2(X0,X2,X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X2,X1),X3)))
| ~ v2_cat_1(k11_cat_2(X2,X1))
| ~ l1_cat_1(k11_cat_2(X2,X1)) ),
inference(duplicate_literal_removal,[],[f43940]) ).
fof(f43948,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| v1_funct_1(k14_isocat_2(X0,X2,X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X2,X1),X3)))
| ~ v2_cat_1(k11_cat_2(X2,X1)) ),
inference(forward_subsumption_resolution,[],[f43945,f34773]) ).
fof(f43951,plain,
! [X2,X3,X0,X1] :
( v1_funct_1(k14_isocat_2(X0,X2,X1,X3,X3,k7_nattra_1(X0,k11_cat_2(X2,X1),X3)))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,k11_cat_2(X2,X1))
| ~ v2_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f43948,f39271]) ).
fof(f44418,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ spl916_30 ),
inference(resolution,[],[f34765,f42903]) ).
fof(f44424,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(resolution,[],[f34765,f42912]) ).
fof(f44435,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(duplicate_literal_removal,[],[f44424]) ).
fof(f44441,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ spl916_30 ),
inference(duplicate_literal_removal,[],[f44418]) ).
fof(f44486,definition,
( spl916_74
<=> v1_xboole_0(u2_cat_1(sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_74])],[avatar_definition]) ).
fof(f44488,plain,
( v1_xboole_0(u2_cat_1(sK98))
| ~ spl916_74 ),
inference(avatar_component_clause,[],[f44486]) ).
fof(f44528,definition,
( spl916_84
<=> m1_relset_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_84])],[avatar_definition]) ).
fof(f44530,plain,
( ~ m1_relset_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| spl916_84 ),
inference(avatar_component_clause,[],[f44528]) ).
fof(f44532,definition,
( spl916_85
<=> v1_funct_2(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_85])],[avatar_definition]) ).
fof(f44534,plain,
( ~ v1_funct_2(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| spl916_85 ),
inference(avatar_component_clause,[],[f44532]) ).
fof(f44536,definition,
( spl916_86
<=> v1_funct_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_86])],[avatar_definition]) ).
fof(f44538,plain,
( ~ v1_funct_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| spl916_86 ),
inference(avatar_component_clause,[],[f44536]) ).
fof(f44540,definition,
( spl916_87
<=> v1_xboole_0(u1_cat_1(sK96)) ),
introduced(definition,[new_symbols(definition,[spl916_87])],[avatar_definition]) ).
fof(f44542,plain,
( v1_xboole_0(u1_cat_1(sK96))
| ~ spl916_87 ),
inference(avatar_component_clause,[],[f44540]) ).
fof(f44549,definition,
( spl916_89
<=> m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_89])],[avatar_definition]) ).
fof(f44551,plain,
( ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| spl916_89 ),
inference(avatar_component_clause,[],[f44549]) ).
fof(f44553,definition,
( spl916_90
<=> v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98)) ),
introduced(definition,[new_symbols(definition,[spl916_90])],[avatar_definition]) ).
fof(f44555,plain,
( ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| spl916_90 ),
inference(avatar_component_clause,[],[f44553]) ).
fof(f44557,definition,
( spl916_91
<=> v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_91])],[avatar_definition]) ).
fof(f44559,plain,
( ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| spl916_91 ),
inference(avatar_component_clause,[],[f44557]) ).
fof(f44578,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(forward_demodulation,[],[f44435,f43144]) ).
fof(f44604,definition,
( spl916_102
<=> v1_xboole_0(u2_cat_1(sK97)) ),
introduced(definition,[new_symbols(definition,[spl916_102])],[avatar_definition]) ).
fof(f44606,plain,
( v1_xboole_0(u2_cat_1(sK97))
| ~ spl916_102 ),
inference(avatar_component_clause,[],[f44604]) ).
fof(f44642,definition,
( spl916_111
<=> m1_relset_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97)) ),
introduced(definition,[new_symbols(definition,[spl916_111])],[avatar_definition]) ).
fof(f44644,plain,
( ~ m1_relset_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_111 ),
inference(avatar_component_clause,[],[f44642]) ).
fof(f44646,definition,
( spl916_112
<=> v1_funct_2(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97)) ),
introduced(definition,[new_symbols(definition,[spl916_112])],[avatar_definition]) ).
fof(f44648,plain,
( ~ v1_funct_2(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_112 ),
inference(avatar_component_clause,[],[f44646]) ).
fof(f44650,definition,
( spl916_113
<=> v1_funct_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_113])],[avatar_definition]) ).
fof(f44652,plain,
( ~ v1_funct_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| spl916_113 ),
inference(avatar_component_clause,[],[f44650]) ).
fof(f44660,definition,
( spl916_115
<=> m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97)) ),
introduced(definition,[new_symbols(definition,[spl916_115])],[avatar_definition]) ).
fof(f44662,plain,
( ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_115 ),
inference(avatar_component_clause,[],[f44660]) ).
fof(f44664,definition,
( spl916_116
<=> v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97)) ),
introduced(definition,[new_symbols(definition,[spl916_116])],[avatar_definition]) ).
fof(f44666,plain,
( ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_116 ),
inference(avatar_component_clause,[],[f44664]) ).
fof(f44668,definition,
( spl916_117
<=> v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99))) ),
introduced(definition,[new_symbols(definition,[spl916_117])],[avatar_definition]) ).
fof(f44670,plain,
( ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| spl916_117 ),
inference(avatar_component_clause,[],[f44668]) ).
fof(f44688,plain,
( r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK97),u1_cat_1(sK96),u2_cat_1(sK97),k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ spl916_30 ),
inference(forward_demodulation,[],[f44441,f43084]) ).
fof(f44755,plain,
( ~ v1_funct_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(forward_demodulation,[],[f44578,f43144]) ).
fof(f44757,plain,
( v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_21
| ~ spl916_30 ),
inference(forward_subsumption_resolution,[],[f44688,f42635]) ).
fof(f44774,plain,
( ~ v1_funct_2(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k9_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(forward_demodulation,[],[f44755,f43144]) ).
fof(f44775,plain,
( ~ v1_funct_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_2(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_21
| ~ spl916_30 ),
inference(forward_demodulation,[],[f44757,f43084]) ).
fof(f44780,plain,
( ~ m1_relset_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_2(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ v1_funct_1(k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| r4_nattra_1(u1_cat_1(sK96),u2_cat_1(sK98),u1_cat_1(sK96),u2_cat_1(sK98),k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),k14_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK98))
| ~ v1_funct_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ m1_relset_1(k7_nattra_1(sK96,sK98,k12_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK98))
| ~ spl916_32 ),
inference(forward_demodulation,[],[f44774,f43144]) ).
fof(f44781,plain,
( ~ v1_funct_2(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ m1_relset_1(k6_isocat_1(sK96,k11_cat_2(sK97,sK98),sK97,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),k8_isocat_2(sK97,sK98)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_21
| ~ spl916_30 ),
inference(forward_demodulation,[],[f44775,f43084]) ).
fof(f44786,plain,
( ~ spl916_89
| ~ spl916_90
| ~ spl916_91
| spl916_74
| spl916_87
| spl916_20
| ~ spl916_86
| ~ spl916_85
| ~ spl916_84
| ~ spl916_32 ),
inference(avatar_split_clause,[],[f44780,f42910,f44528,f44532,f44536,f42629,f44540,f44486,f44557,f44553,f44549]) ).
fof(f44787,plain,
( ~ m1_relset_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_2(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ v1_funct_1(k13_isocat_2(sK96,sK97,sK98,sK99,sK99,k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99)))
| v1_xboole_0(u1_cat_1(sK96))
| v1_xboole_0(u2_cat_1(sK97))
| ~ v1_funct_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)))
| ~ v1_funct_2(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| ~ m1_relset_1(k7_nattra_1(sK96,sK97,k11_isocat_2(sK96,sK97,sK98,sK99)),u1_cat_1(sK96),u2_cat_1(sK97))
| spl916_21
| ~ spl916_30 ),
inference(forward_demodulation,[],[f44781,f43084]) ).
fof(f44789,plain,
( ~ spl916_115
| ~ spl916_116
| ~ spl916_117
| spl916_102
| spl916_87
| ~ spl916_113
| ~ spl916_112
| ~ spl916_111
| spl916_21
| ~ spl916_30 ),
inference(avatar_split_clause,[],[f44787,f42901,f42633,f44642,f44646,f44650,f44540,f44604,f44668,f44664,f44660]) ).
fof(f44791,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| spl916_117 ),
inference(resolution,[],[f44670,f43923]) ).
fof(f44792,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| spl916_117 ),
inference(forward_subsumption_resolution,[],[f44791,f34740]) ).
fof(f44793,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| spl916_117 ),
inference(forward_subsumption_resolution,[],[f44792,f34739]) ).
fof(f44794,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| spl916_117 ),
inference(forward_subsumption_resolution,[],[f44793,f34742]) ).
fof(f44795,plain,
( ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| spl916_117 ),
inference(forward_subsumption_resolution,[],[f44794,f34741]) ).
fof(f44796,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_117 ),
inference(forward_subsumption_resolution,[],[f44795,f43625]) ).
fof(f44797,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_117 ),
inference(avatar_contradiction_clause,[],[f44796]) ).
fof(f44923,plain,
! [X2,X0,X1] :
( m1_relset_1(k7_nattra_1(X0,X1,X2),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X0) ),
inference(resolution,[],[f35415,f43522]) ).
fof(f44924,plain,
! [X2,X3,X0,X1,X4,X5] :
( m1_relset_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X1))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_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)
| ~ v2_cat_1(X0) ),
inference(resolution,[],[f35415,f43530]) ).
fof(f44925,plain,
! [X2,X3,X0,X1,X4,X5] :
( m1_relset_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),u1_cat_1(X0),u2_cat_1(X2))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ 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)
| ~ v2_cat_1(X0) ),
inference(resolution,[],[f35415,f43538]) ).
fof(f44927,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(resolution,[],[f44924,f44644]) ).
fof(f44928,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(duplicate_literal_removal,[],[f44927]) ).
fof(f44929,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44928,f34739]) ).
fof(f44930,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44929,f34742]) ).
fof(f44931,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44930,f34741]) ).
fof(f44932,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44931,f34744]) ).
fof(f44933,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44932,f34743]) ).
fof(f44934,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44933,f34745]) ).
fof(f44935,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44934,f34740]) ).
fof(f44936,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_111 ),
inference(resolution,[],[f44935,f34786]) ).
fof(f44937,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44936,f34740]) ).
fof(f44938,plain,
( ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44937,f34739]) ).
fof(f44939,plain,
( ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_28
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44938,f42894]) ).
fof(f44940,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_27
| ~ spl916_28
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44939,f42890]) ).
fof(f44941,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| spl916_111 ),
inference(forward_subsumption_resolution,[],[f44940,f34745]) ).
fof(f44942,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_111 ),
inference(avatar_contradiction_clause,[],[f44941]) ).
fof(f44943,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_115 ),
inference(resolution,[],[f44923,f44662]) ).
fof(f44944,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_89 ),
inference(resolution,[],[f44923,f44551]) ).
fof(f44945,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_89 ),
inference(forward_subsumption_resolution,[],[f44944,f34739]) ).
fof(f44946,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_115 ),
inference(forward_subsumption_resolution,[],[f44943,f34739]) ).
fof(f44947,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_89 ),
inference(forward_subsumption_resolution,[],[f44945,f34744]) ).
fof(f44948,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_115 ),
inference(forward_subsumption_resolution,[],[f44946,f34742]) ).
fof(f44949,plain,
( ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_89 ),
inference(forward_subsumption_resolution,[],[f44947,f34743]) ).
fof(f44950,plain,
( ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_115 ),
inference(forward_subsumption_resolution,[],[f44948,f34741]) ).
fof(f44951,plain,
( ~ v2_cat_1(sK96)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_89 ),
inference(forward_subsumption_resolution,[],[f44949,f43626]) ).
fof(f44952,plain,
( ~ v2_cat_1(sK96)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_115 ),
inference(forward_subsumption_resolution,[],[f44950,f43625]) ).
fof(f44953,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_89 ),
inference(forward_subsumption_resolution,[],[f44951,f34740]) ).
fof(f44954,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_89 ),
inference(avatar_contradiction_clause,[],[f44953]) ).
fof(f44955,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_115 ),
inference(forward_subsumption_resolution,[],[f44952,f34740]) ).
fof(f44956,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_115 ),
inference(avatar_contradiction_clause,[],[f44955]) ).
fof(f44957,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_116 ),
inference(resolution,[],[f44666,f43523]) ).
fof(f44958,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_116 ),
inference(forward_subsumption_resolution,[],[f44957,f34739]) ).
fof(f44959,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_116 ),
inference(forward_subsumption_resolution,[],[f44958,f34742]) ).
fof(f44960,plain,
( ~ m2_cat_1(k11_isocat_2(sK96,sK97,sK98,sK99),sK96,sK97)
| ~ v2_cat_1(sK96)
| spl916_116 ),
inference(forward_subsumption_resolution,[],[f44959,f34741]) ).
fof(f44961,plain,
( ~ v2_cat_1(sK96)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_116 ),
inference(forward_subsumption_resolution,[],[f44960,f43625]) ).
fof(f44962,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_116 ),
inference(forward_subsumption_resolution,[],[f44961,f34740]) ).
fof(f44963,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_116 ),
inference(avatar_contradiction_clause,[],[f44962]) ).
fof(f44964,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_90 ),
inference(resolution,[],[f44555,f43523]) ).
fof(f44965,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_90 ),
inference(forward_subsumption_resolution,[],[f44964,f34739]) ).
fof(f44966,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_90 ),
inference(forward_subsumption_resolution,[],[f44965,f34744]) ).
fof(f44967,plain,
( ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| ~ v2_cat_1(sK96)
| spl916_90 ),
inference(forward_subsumption_resolution,[],[f44966,f34743]) ).
fof(f44968,plain,
( ~ v2_cat_1(sK96)
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_90 ),
inference(forward_subsumption_resolution,[],[f44967,f43626]) ).
fof(f44969,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_90 ),
inference(forward_subsumption_resolution,[],[f44968,f34740]) ).
fof(f44970,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_90 ),
inference(avatar_contradiction_clause,[],[f44969]) ).
fof(f44971,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| spl916_91 ),
inference(resolution,[],[f44559,f43923]) ).
fof(f44972,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| spl916_91 ),
inference(forward_subsumption_resolution,[],[f44971,f34740]) ).
fof(f44973,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| spl916_91 ),
inference(forward_subsumption_resolution,[],[f44972,f34739]) ).
fof(f44974,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| spl916_91 ),
inference(forward_subsumption_resolution,[],[f44973,f34744]) ).
fof(f44975,plain,
( ~ m2_cat_1(k12_isocat_2(sK96,sK97,sK98,sK99),sK96,sK98)
| spl916_91 ),
inference(forward_subsumption_resolution,[],[f44974,f34743]) ).
fof(f44976,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_91 ),
inference(forward_subsumption_resolution,[],[f44975,f43626]) ).
fof(f44977,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_91 ),
inference(avatar_contradiction_clause,[],[f44976]) ).
fof(f45020,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(resolution,[],[f44648,f43531]) ).
fof(f45021,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(duplicate_literal_removal,[],[f45020]) ).
fof(f45022,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45021,f34739]) ).
fof(f45023,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45022,f34742]) ).
fof(f45024,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45023,f34741]) ).
fof(f45025,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45024,f34744]) ).
fof(f45026,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45025,f34743]) ).
fof(f45027,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45026,f34745]) ).
fof(f45028,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45027,f34740]) ).
fof(f45029,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_112 ),
inference(resolution,[],[f45028,f34786]) ).
fof(f45030,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45029,f34740]) ).
fof(f45031,plain,
( ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45030,f34739]) ).
fof(f45032,plain,
( ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_28
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45031,f42894]) ).
fof(f45033,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_27
| ~ spl916_28
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45032,f42890]) ).
fof(f45034,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| spl916_112 ),
inference(forward_subsumption_resolution,[],[f45033,f34745]) ).
fof(f45035,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_112 ),
inference(avatar_contradiction_clause,[],[f45034]) ).
fof(f45036,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(resolution,[],[f44652,f43939]) ).
fof(f45037,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45036,f34739]) ).
fof(f45038,plain,
( ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45037,f34742]) ).
fof(f45039,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45038,f34741]) ).
fof(f45040,plain,
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45039,f34744]) ).
fof(f45041,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45040,f34743]) ).
fof(f45042,plain,
( ~ v2_cat_1(sK96)
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45041,f34745]) ).
fof(f45043,plain,
( $false
| spl916_113 ),
inference(forward_subsumption_resolution,[],[f45042,f34740]) ).
fof(f45044,plain,
spl916_113,
inference(avatar_contradiction_clause,[],[f45043]) ).
fof(f45047,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(resolution,[],[f44530,f44925]) ).
fof(f45048,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(duplicate_literal_removal,[],[f45047]) ).
fof(f45049,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45048,f34739]) ).
fof(f45050,plain,
( ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45049,f34744]) ).
fof(f45051,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45050,f34743]) ).
fof(f45052,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45051,f34742]) ).
fof(f45053,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45052,f34741]) ).
fof(f45054,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45053,f34745]) ).
fof(f45055,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45054,f34740]) ).
fof(f45056,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_84 ),
inference(resolution,[],[f45055,f34786]) ).
fof(f45057,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45056,f34740]) ).
fof(f45058,plain,
( ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45057,f34739]) ).
fof(f45059,plain,
( ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_28
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45058,f42894]) ).
fof(f45060,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_27
| ~ spl916_28
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45059,f42890]) ).
fof(f45061,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| spl916_84 ),
inference(forward_subsumption_resolution,[],[f45060,f34745]) ).
fof(f45062,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_84 ),
inference(avatar_contradiction_clause,[],[f45061]) ).
fof(f45063,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(resolution,[],[f44534,f43539]) ).
fof(f45064,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(duplicate_literal_removal,[],[f45063]) ).
fof(f45065,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45064,f34739]) ).
fof(f45066,plain,
( ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45065,f34744]) ).
fof(f45067,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45066,f34743]) ).
fof(f45068,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45067,f34742]) ).
fof(f45069,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45068,f34741]) ).
fof(f45070,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| ~ v2_cat_1(sK96)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45069,f34745]) ).
fof(f45071,plain,
( ~ m2_nattra_1(k7_nattra_1(sK96,k11_cat_2(sK97,sK98),sK99),sK96,k11_cat_2(sK97,sK98),sK99,sK99)
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45070,f34740]) ).
fof(f45072,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_85 ),
inference(resolution,[],[f45071,f34786]) ).
fof(f45073,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45072,f34740]) ).
fof(f45074,plain,
( ~ v2_cat_1(k11_cat_2(sK97,sK98))
| ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45073,f34739]) ).
fof(f45075,plain,
( ~ l1_cat_1(k11_cat_2(sK97,sK98))
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_28
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45074,f42894]) ).
fof(f45076,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ spl916_27
| ~ spl916_28
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45075,f42890]) ).
fof(f45077,plain,
( $false
| ~ spl916_27
| ~ spl916_28
| spl916_85 ),
inference(forward_subsumption_resolution,[],[f45076,f34745]) ).
fof(f45078,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_85 ),
inference(avatar_contradiction_clause,[],[f45077]) ).
fof(f45079,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(resolution,[],[f44538,f43951]) ).
fof(f45080,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45079,f34739]) ).
fof(f45081,plain,
( ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45080,f34744]) ).
fof(f45082,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45081,f34743]) ).
fof(f45083,plain,
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45082,f34742]) ).
fof(f45084,plain,
( ~ m2_cat_1(sK99,sK96,k11_cat_2(sK97,sK98))
| ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45083,f34741]) ).
fof(f45085,plain,
( ~ v2_cat_1(sK96)
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45084,f34745]) ).
fof(f45086,plain,
( $false
| spl916_86 ),
inference(forward_subsumption_resolution,[],[f45085,f34740]) ).
fof(f45087,plain,
spl916_86,
inference(avatar_contradiction_clause,[],[f45086]) ).
fof(f45088,plain,
( ~ l1_cat_1(sK98)
| ~ spl916_74 ),
inference(resolution,[],[f44488,f34747]) ).
fof(f45089,plain,
( $false
| ~ spl916_74 ),
inference(forward_subsumption_resolution,[],[f45088,f34743]) ).
fof(f45090,plain,
~ spl916_74,
inference(avatar_contradiction_clause,[],[f45089]) ).
fof(f45430,plain,
( ~ l1_cat_1(sK96)
| ~ spl916_87 ),
inference(resolution,[],[f34748,f44542]) ).
fof(f45431,plain,
( $false
| ~ spl916_87 ),
inference(forward_subsumption_resolution,[],[f45430,f34739]) ).
fof(f45432,plain,
~ spl916_87,
inference(avatar_contradiction_clause,[],[f45431]) ).
fof(f45435,plain,
( ~ l1_cat_1(sK97)
| ~ spl916_102 ),
inference(resolution,[],[f44606,f34747]) ).
fof(f45436,plain,
( $false
| ~ spl916_102 ),
inference(forward_subsumption_resolution,[],[f45435,f34741]) ).
fof(f45437,plain,
~ spl916_102,
inference(avatar_contradiction_clause,[],[f45436]) ).
cnf(s20,plain,
( ~ spl916_20
| ~ spl916_21 ),
inference(sat_conversion,[],[f42636]) ).
cnf(s25,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_30 ),
inference(sat_conversion,[],[f42904]) ).
cnf(s26,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_32 ),
inference(sat_conversion,[],[f42913]) ).
cnf(s27,plain,
spl916_27,
inference(sat_conversion,[],[f42919]) ).
cnf(s28,plain,
spl916_28,
inference(sat_conversion,[],[f42925]) ).
cnf(s29,plain,
spl916_29,
inference(sat_conversion,[],[f42939]) ).
cnf(s30,plain,
spl916_31,
inference(sat_conversion,[],[f42953]) ).
cnf(s66,plain,
( spl916_20
| ~ spl916_32
| spl916_74
| ~ spl916_84
| ~ spl916_85
| ~ spl916_86
| spl916_87
| ~ spl916_89
| ~ spl916_90
| ~ spl916_91 ),
inference(sat_conversion,[],[f44786]) ).
cnf(s67,plain,
( spl916_21
| ~ spl916_30
| spl916_87
| spl916_102
| ~ spl916_111
| ~ spl916_112
| ~ spl916_113
| ~ spl916_115
| ~ spl916_116
| ~ spl916_117 ),
inference(sat_conversion,[],[f44789]) ).
cnf(s68,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_117 ),
inference(sat_conversion,[],[f44797]) ).
cnf(s69,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_111 ),
inference(sat_conversion,[],[f44942]) ).
cnf(s70,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_89 ),
inference(sat_conversion,[],[f44954]) ).
cnf(s71,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_115 ),
inference(sat_conversion,[],[f44956]) ).
cnf(s72,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_29
| spl916_116 ),
inference(sat_conversion,[],[f44963]) ).
cnf(s73,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_90 ),
inference(sat_conversion,[],[f44970]) ).
cnf(s74,plain,
( ~ spl916_27
| ~ spl916_28
| ~ spl916_31
| spl916_91 ),
inference(sat_conversion,[],[f44977]) ).
cnf(s81,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_112 ),
inference(sat_conversion,[],[f45035]) ).
cnf(s82,plain,
spl916_113,
inference(sat_conversion,[],[f45044]) ).
cnf(s83,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_84 ),
inference(sat_conversion,[],[f45062]) ).
cnf(s84,plain,
( ~ spl916_27
| ~ spl916_28
| spl916_85 ),
inference(sat_conversion,[],[f45078]) ).
cnf(s85,plain,
spl916_86,
inference(sat_conversion,[],[f45087]) ).
cnf(s86,plain,
~ spl916_74,
inference(sat_conversion,[],[f45090]) ).
cnf(s98,plain,
~ spl916_87,
inference(sat_conversion,[],[f45432]) ).
cnf(s99,plain,
~ spl916_102,
inference(sat_conversion,[],[f45437]) ).
cnf(s100,plain,
( spl916_21
| ~ spl916_30
| ~ spl916_111
| ~ spl916_112
| ~ spl916_115
| ~ spl916_116
| ~ spl916_117 ),
inference(rat,[],[s67,s82,s99,s98]) ).
cnf(s101,plain,
( spl916_20
| ~ spl916_32
| ~ spl916_84
| ~ spl916_85
| ~ spl916_89
| ~ spl916_90
| ~ spl916_91 ),
inference(rat,[],[s66,s98,s85,s86]) ).
cnf(s112,plain,
spl916_85,
inference(rat,[],[s84,s28,s27]) ).
cnf(s113,plain,
spl916_84,
inference(rat,[],[s83,s28,s27]) ).
cnf(s114,plain,
spl916_112,
inference(rat,[],[s81,s28,s27]) ).
cnf(s121,plain,
spl916_91,
inference(rat,[],[s74,s28,s30,s27]) ).
cnf(s122,plain,
spl916_90,
inference(rat,[],[s73,s28,s30,s27]) ).
cnf(s123,plain,
spl916_116,
inference(rat,[],[s72,s28,s29,s27]) ).
cnf(s124,plain,
spl916_115,
inference(rat,[],[s71,s28,s29,s27]) ).
cnf(s125,plain,
spl916_89,
inference(rat,[],[s70,s28,s30,s27]) ).
cnf(s126,plain,
spl916_111,
inference(rat,[],[s69,s28,s27]) ).
cnf(s127,plain,
spl916_117,
inference(rat,[],[s68,s28,s29,s27]) ).
cnf(s136,plain,
spl916_32,
inference(rat,[],[s26,s30,s28,s27]) ).
cnf(s137,plain,
spl916_20,
inference(rat,[],[s101,s121,s122,s125,s112,s113,s136]) ).
cnf(s138,plain,
spl916_30,
inference(rat,[],[s25,s29,s28,s27]) ).
cnf(s139,plain,
spl916_21,
inference(rat,[],[s100,s127,s123,s124,s114,s126,s138]) ).
cnf(s140,plain,
$false,
inference(rat,[],[s20,s139,s137]) ).
fof(f45438,plain,
$false,
inference(avatar_sat_refutation,[],[s140]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CAT027+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.27 % Computer : n005.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 21:18:35 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.32 Running first-order theorem proving
% 0.26/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.85/6.40 % (1188181)Detected formulas, will run a generic FOF schedule.
% 27.85/6.40 % (1188188)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3644826189:i=141193_2979 on theBenchmark for (2979ds/141193Mi)
% 27.85/6.40 % (1188190)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1751519352:i=141695:sd=1:nm=32:gsp=on:ss=included_2979 on theBenchmark for (2979ds/141695Mi)
% 27.85/6.40 % (1188189)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1918196857:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2979 on theBenchmark for (2979ds/134677Mi)
% 27.85/6.40 % (1188194)dis-21_1_sil=8000:lcm=predicate:random_seed=431969313:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2979 on theBenchmark for (2979ds/129Mi)
% 27.85/6.40 % (1188191)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3368491155:i=109:sd=1:ins=1:gsp=on:ss=axioms_2979 on theBenchmark for (2979ds/109Mi)
% 27.85/6.40 % (1188193)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1810094775:s2a=on:i=139:gtg=position_2979 on theBenchmark for (2979ds/139Mi)
% 27.85/6.40 % (1188192)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1886894051:i=119:av=off:ss=axioms_2979 on theBenchmark for (2979ds/119Mi)
% 27.85/6.40 % (1188191)Instruction limit reached!
% 27.85/6.40 % (1188191)------------------------------
% 27.85/6.40 % (1188191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/6.40 % (1188191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/6.40 % (1188191)CaDiCaL version: 2.1.3
% 27.85/6.40 % (1188191)Termination reason: Instruction limit
% 27.85/6.40 % (1188191)Termination phase: SInE selection
% 27.85/6.40 % (1188191)Time elapsed: 0.116 s
% 27.85/6.40 % (1188191)Peak memory usage: 126 MB
% 27.85/6.40 % (1188191)Instructions burned: 110 (million)
% 27.85/6.40 % (1188194)Instruction limit reached!
% 27.85/6.40 % (1188194)------------------------------
% 27.85/6.40 % (1188194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/6.40 % (1188194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/6.40 % (1188194)CaDiCaL version: 2.1.3
% 27.85/6.40 % (1188194)Termination reason: Instruction limit
% 27.85/6.40 % (1188194)Termination phase: SInE selection
% 27.85/6.40 % (1188194)Time elapsed: 0.132 s
% 27.85/6.40 % (1188194)Peak memory usage: 127 MB
% 27.85/6.40 % (1188194)Instructions burned: 131 (million)
% 27.85/6.40 % (1188193)Instruction limit reached!
% 27.85/6.40 % (1188193)------------------------------
% 27.85/6.40 % (1188193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/6.40 % (1188193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/6.40 % (1188193)CaDiCaL version: 2.1.3
% 27.85/6.40 % (1188193)Termination reason: Instruction limit
% 27.85/6.40 % (1188193)Termination phase: Property scanning
% 27.85/6.40 % (1188193)Time elapsed: 0.117 s
% 27.85/6.40 % (1188193)Peak memory usage: 127 MB
% 27.85/6.40 % (1188193)Instructions burned: 139 (million)
% 27.85/6.40 % (1188192)Instruction limit reached!
% 27.85/6.40 % (1188192)------------------------------
% 27.85/6.40 % (1188192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/6.41 % (1188192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/6.41 % (1188192)CaDiCaL version: 2.1.3
% 27.85/6.41 % (1188192)Termination reason: Instruction limit
% 27.85/6.41 % (1188192)Termination phase: SInE selection
% 27.85/6.41 % (1188192)Time elapsed: 0.140 s
% 27.85/6.41 % (1188192)Peak memory usage: 127 MB
% 27.85/6.41 % (1188192)Instructions burned: 119 (million)
% 27.85/6.41 % (1188202)lrs+10_1_sil=8000:sp=occurrence:random_seed=2595293357:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 27.85/6.41 % (1188203)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2500459647:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 27.85/6.41 % (1188204)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1252694021:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 27.85/6.41 % (1188205)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1545049894:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 27.85/6.41 % (1188203)Instruction limit reached!
% 40.58/8.24 % (1188203)------------------------------
% 40.58/8.24 % (1188203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188203)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188203)Termination reason: Instruction limit
% 40.58/8.24 % (1188203)Termination phase: Property scanning
% 40.58/8.24 % (1188203)Time elapsed: 0.131 s
% 40.58/8.24 % (1188203)Peak memory usage: 127 MB
% 40.58/8.24 % (1188203)Instructions burned: 157 (million)
% 40.58/8.24 % (1188205)Instruction limit reached!
% 40.58/8.24 % (1188205)------------------------------
% 40.58/8.24 % (1188205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188205)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188205)Termination reason: Instruction limit
% 40.58/8.24 % (1188205)Termination phase: Property scanning
% 40.58/8.24 % (1188205)Time elapsed: 0.206 s
% 40.58/8.24 % (1188205)Peak memory usage: 127 MB
% 40.58/8.24 % (1188205)Instructions burned: 248 (million)
% 40.58/8.24 % (1188202)Instruction limit reached!
% 40.58/8.24 % (1188202)------------------------------
% 40.58/8.24 % (1188202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188202)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188202)Termination reason: Instruction limit
% 40.58/8.24 % (1188202)Termination phase: Saturation
% 40.58/8.24 % (1188202)Time elapsed: 0.327 s
% 40.58/8.24 % (1188202)Peak memory usage: 133 MB
% 40.58/8.24 % (1188202)Instructions burned: 285 (million)
% 40.58/8.24 % (1188204)Instruction limit reached!
% 40.58/8.24 % (1188204)------------------------------
% 40.58/8.24 % (1188204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188204)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188204)Termination reason: Instruction limit
% 40.58/8.24 % (1188204)Termination phase: Saturation
% 40.58/8.24 % (1188204)Time elapsed: 0.398 s
% 40.58/8.24 % (1188204)Peak memory usage: 133 MB
% 40.58/8.24 % (1188204)Instructions burned: 325 (million)
% 40.58/8.24 % (1188210)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1209476785:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2971 on theBenchmark for (2971ds/294Mi)
% 40.58/8.24 % (1188211)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1838249944:i=2350_2970 on theBenchmark for (2970ds/2350Mi)
% 40.58/8.24 % (1188212)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2380736718:cts=off:i=113:fsr=off:ss=included:sgt=4_2969 on theBenchmark for (2969ds/113Mi)
% 40.58/8.24 % (1188213)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=126483379:i=127:av=off:fsr=off:sup=off_2968 on theBenchmark for (2968ds/127Mi)
% 40.58/8.24 % (1188212)Instruction limit reached!
% 40.58/8.24 % (1188212)------------------------------
% 40.58/8.24 % (1188212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188212)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188212)Termination reason: Instruction limit
% 40.58/8.24 % (1188212)Termination phase: SInE selection
% 40.58/8.24 % (1188212)Time elapsed: 0.127 s
% 40.58/8.24 % (1188212)Peak memory usage: 126 MB
% 40.58/8.24 % (1188212)Instructions burned: 114 (million)
% 40.58/8.24 % (1188210)Instruction limit reached!
% 40.58/8.24 % (1188210)------------------------------
% 40.58/8.24 % (1188210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188210)CaDiCaL version: 2.1.3
% 40.58/8.24 % (1188210)Termination reason: Instruction limit
% 40.58/8.24 % (1188210)Termination phase: Preprocessing 3
% 40.58/8.24 % (1188210)Time elapsed: 0.335 s
% 40.58/8.24 % (1188210)Peak memory usage: 130 MB
% 40.58/8.24 % (1188210)Instructions burned: 294 (million)
% 40.58/8.24 % (1188213)Instruction limit reached!
% 40.58/8.24 % (1188213)------------------------------
% 40.58/8.24 % (1188213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/8.24 % (1188213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/8.24 % (1188213)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188213)Termination reason: Instruction limit
% 41.61/11.23 % (1188213)Termination phase: Preprocessing 1
% 41.61/11.23 % (1188213)Time elapsed: 0.151 s
% 41.61/11.23 % (1188213)Peak memory usage: 128 MB
% 41.61/11.23 % (1188213)Instructions burned: 127 (million)
% 41.61/11.23 % (1188218)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2601963172:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2965 on theBenchmark for (2965ds/114Mi)
% 41.61/11.23 % (1188219)lrs+10_1_sil=8000:sp=occurrence:random_seed=3687264417:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2965 on theBenchmark for (2965ds/907Mi)
% 41.61/11.23 % (1188218)Instruction limit reached!
% 41.61/11.23 % (1188218)------------------------------
% 41.61/11.23 % (1188218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188218)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188218)Termination reason: Instruction limit
% 41.61/11.23 % (1188218)Termination phase: Property scanning
% 41.61/11.23 % (1188218)Time elapsed: 0.098 s
% 41.61/11.23 % (1188218)Peak memory usage: 127 MB
% 41.61/11.23 % (1188218)Instructions burned: 114 (million)
% 41.61/11.23 % (1188220)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3274926826:i=437:sd=1:aac=none:ss=included_2964 on theBenchmark for (2964ds/437Mi)
% 41.61/11.23 % (1188223)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2572404515:i=5202:ss=axioms:sgt=16_2962 on theBenchmark for (2962ds/5202Mi)
% 41.61/11.23 % (1188220)Instruction limit reached!
% 41.61/11.23 % (1188220)------------------------------
% 41.61/11.23 % (1188220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188220)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188220)Termination reason: Instruction limit
% 41.61/11.23 % (1188220)Termination phase: Saturation
% 41.61/11.23 % (1188220)Time elapsed: 0.485 s
% 41.61/11.23 % (1188220)Peak memory usage: 134 MB
% 41.61/11.23 % (1188220)Instructions burned: 437 (million)
% 41.61/11.23 % (1188226)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3960045641:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2956 on theBenchmark for (2956ds/134Mi)
% 41.61/11.23 % (1188219)Instruction limit reached!
% 41.61/11.23 % (1188219)------------------------------
% 41.61/11.23 % (1188219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188219)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188219)Termination reason: Instruction limit
% 41.61/11.23 % (1188219)Termination phase: Equality resolution with deletion
% 41.61/11.23 % (1188219)Time elapsed: 0.927 s
% 41.61/11.23 % (1188219)Peak memory usage: 149 MB
% 41.61/11.23 % (1188219)Instructions burned: 907 (million)
% 41.61/11.23 % (1188226)Instruction limit reached!
% 41.61/11.23 % (1188226)------------------------------
% 41.61/11.23 % (1188226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188226)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188226)Termination reason: Instruction limit
% 41.61/11.23 % (1188226)Termination phase: SInE selection
% 41.61/11.23 % (1188226)Time elapsed: 0.158 s
% 41.61/11.23 % (1188226)Peak memory usage: 127 MB
% 41.61/11.23 % (1188226)Instructions burned: 134 (million)
% 41.61/11.23 % (1188228)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2247578098:st=8:i=592:sd=3:ep=RST:ss=axioms_2953 on theBenchmark for (2953ds/592Mi)
% 41.61/11.23 % (1188229)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=207192119:st=3:i=13193:sd=3:ss=axioms_2952 on theBenchmark for (2952ds/13193Mi)
% 41.61/11.23 % (1188211)Instruction limit reached!
% 41.61/11.23 % (1188211)------------------------------
% 41.61/11.23 % (1188211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188211)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188211)Termination reason: Instruction limit
% 41.61/11.23 % (1188211)Termination phase: Property scanning
% 41.61/11.23 % (1188211)Time elapsed: 2.358 s
% 41.61/11.23 % (1188211)Peak memory usage: 208 MB
% 41.61/11.23 % (1188211)Instructions burned: 2351 (million)
% 41.61/11.23 % (1188228)Instruction limit reached!
% 41.61/11.23 % (1188228)------------------------------
% 41.61/11.23 % (1188228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188228)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188228)Termination reason: Instruction limit
% 41.61/11.23 % (1188228)Termination phase: Preprocessing 3
% 41.61/11.23 % (1188228)Time elapsed: 0.687 s
% 41.61/11.23 % (1188228)Peak memory usage: 146 MB
% 41.61/11.23 % (1188228)Instructions burned: 592 (million)
% 41.61/11.23 % (1188232)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2289066482:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2943 on theBenchmark for (2943ds/125Mi)
% 41.61/11.23 % (1188233)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1790694688:i=134:gtgl=5:slsql=off:gtg=exists_sym_2943 on theBenchmark for (2943ds/134Mi)
% 41.61/11.23 % (1188232)Instruction limit reached!
% 41.61/11.23 % (1188232)------------------------------
% 41.61/11.23 % (1188232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188232)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188232)Termination reason: Instruction limit
% 41.61/11.23 % (1188232)Termination phase: Property scanning
% 41.61/11.23 % (1188232)Time elapsed: 0.106 s
% 41.61/11.23 % (1188232)Peak memory usage: 127 MB
% 41.61/11.23 % (1188232)Instructions burned: 126 (million)
% 41.61/11.23 % (1188233)Instruction limit reached!
% 41.61/11.23 % (1188233)------------------------------
% 41.61/11.23 % (1188233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188233)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188233)Termination reason: Instruction limit
% 41.61/11.23 % (1188233)Termination phase: Property scanning
% 41.61/11.23 % (1188233)Time elapsed: 0.113 s
% 41.61/11.23 % (1188233)Peak memory usage: 126 MB
% 41.61/11.23 % (1188233)Instructions burned: 134 (million)
% 41.61/11.23 % (1188236)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3115439083:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2939 on theBenchmark for (2939ds/141Mi)
% 41.61/11.23 % (1188237)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2136044955:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2939 on theBenchmark for (2939ds/431Mi)
% 41.61/11.23 % (1188236)Instruction limit reached!
% 41.61/11.23 % (1188236)------------------------------
% 41.61/11.23 % (1188236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188236)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188236)Termination reason: Instruction limit
% 41.61/11.23 % (1188236)Termination phase: SInE selection
% 41.61/11.23 % (1188236)Time elapsed: 0.157 s
% 41.61/11.23 % (1188236)Peak memory usage: 127 MB
% 41.61/11.23 % (1188236)Instructions burned: 142 (million)
% 41.61/11.23 % (1188237)Refutation not found, incomplete strategy
% 41.61/11.23 % (1188237)------------------------------
% 41.61/11.23 % (1188237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188237)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188237)Termination reason: Refutation not found, incomplete strategy
% 41.61/11.23 % (1188237)Time elapsed: 0.230 s
% 41.61/11.23 % (1188237)Peak memory usage: 132 MB
% 41.61/11.23 % (1188237)Instructions burned: 197 (million)
% 41.61/11.23 % (1188240)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=364386887:i=6060:aac=none:ins=25_2935 on theBenchmark for (2935ds/6060Mi)
% 41.61/11.23 % (1188237)------------------------------
% 41.61/11.23 % (1188237)------------------------------
% 41.61/11.23 % (1188242)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3392003024:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2930 on theBenchmark for (2930ds/150Mi)
% 41.61/11.23 % (1188242)Instruction limit reached!
% 41.61/11.23 % (1188242)------------------------------
% 41.61/11.23 % (1188242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188242)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188242)Termination reason: Instruction limit
% 41.61/11.23 % (1188242)Termination phase: SInE selection
% 41.61/11.23 % (1188242)Time elapsed: 0.178 s
% 41.61/11.23 % (1188242)Peak memory usage: 127 MB
% 41.61/11.23 % (1188242)Instructions burned: 151 (million)
% 41.61/11.23 % (1188244)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=735982997:i=14155:bd=all_2925 on theBenchmark for (2925ds/14155Mi)
% 41.61/11.23 % (1188240)Instruction limit reached!
% 41.61/11.23 % (1188240)------------------------------
% 41.61/11.23 % (1188240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188240)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188240)Termination reason: Instruction limit
% 41.61/11.23 % (1188240)Termination phase: Property scanning
% 41.61/11.23 % (1188240)Time elapsed: 3.005 s
% 41.61/11.23 % (1188240)Peak memory usage: 227 MB
% 41.61/11.23 % (1188240)Instructions burned: 6061 (million)
% 41.61/11.23 % (1188229)First to succeed.
% 41.61/11.23 % (1188229)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1188181"
% 41.61/11.23 % (1188246)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1033973014:i=667:av=off:fsr=off_2902 on theBenchmark for (2902ds/667Mi)
% 41.61/11.23 % (1188223)Instruction limit reached!
% 41.61/11.23 % (1188223)------------------------------
% 41.61/11.23 % (1188223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/11.23 % (1188223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/11.23 % (1188223)CaDiCaL version: 2.1.3
% 41.61/11.23 % (1188223)Termination reason: Instruction limit
% 41.61/11.23 % (1188223)Termination phase: Saturation
% 41.61/11.23 % (1188223)Time elapsed: 6.109 s
% 41.61/11.23 % (1188223)Peak memory usage: 627 MB
% 41.61/11.23 % (1188223)Instructions burned: 5202 (million)
% 41.61/11.23 % (1188229)Refutation found. Thanks to Tanya!
% 41.61/11.23 % SZS status Theorem for theBenchmark
% 41.61/11.23 % SZS output start Proof for theBenchmark
% See solution above
% 61.50/11.45 % (1188229)------------------------------
% 61.50/11.45 % (1188229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/11.45 % (1188229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/11.45 % (1188229)CaDiCaL version: 2.1.3
% 61.50/11.45 % (1188229)Termination reason: Refutation
% 61.50/11.45 % (1188229)Time elapsed: 4.740 s
% 61.50/11.45 % (1188229)Peak memory usage: 269 MB
% 61.50/11.45 % (1188229)Instructions burned: 4726 (million)
% 61.50/11.45 % (1188229)------------------------------
% 61.50/11.45 % (1188229)------------------------------
% 61.50/11.45 % (1188181)Success in time 10.453 s
% 61.50/11.45 % Vampire exiting
%------------------------------------------------------------------------------