%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT027+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 21.96s 4.30s
% Output : Refutation 22.62s
% 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(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f6631,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u1_cat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_cat_1) ).
fof(f6632,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u2_cat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_cat_1) ).
fof(f8299,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/sandbox2/benchmark/theBenchmark.p',fc2_cat_2) ).
fof(f8397,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/sandbox2/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f10520,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/sandbox2/benchmark/theBenchmark.p',dt_m1_nattra_1) ).
fof(f10522,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/sandbox2/benchmark/theBenchmark.p',dt_m2_nattra_1) ).
fof(f10531,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/sandbox2/benchmark/theBenchmark.p',symmetry_r4_nattra_1) ).
fof(f10542,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/sandbox2/benchmark/theBenchmark.p',dt_k7_nattra_1) ).
fof(f11397,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/sandbox2/benchmark/theBenchmark.p',t38_isocat_1) ).
fof(f11429,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/sandbox2/benchmark/theBenchmark.p',dt_k2_isocat_1) ).
fof(f11735,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/sandbox2/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f11737,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/sandbox2/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f11741,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/sandbox2/benchmark/theBenchmark.p',dt_k11_isocat_2) ).
fof(f11742,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/sandbox2/benchmark/theBenchmark.p',dt_k12_isocat_2) ).
fof(f11743,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/sandbox2/benchmark/theBenchmark.p',dt_k13_isocat_2) ).
fof(f11744,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/sandbox2/benchmark/theBenchmark.p',dt_k14_isocat_2) ).
fof(f11791,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/sandbox2/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f11792,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/sandbox2/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f11795,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/sandbox2/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f11796,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/sandbox2/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f11799,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/sandbox2/benchmark/theBenchmark.p',t40_isocat_2) ).
fof(f11800,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)],[f11799]) ).
fof(f11960,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,[],[f11800]) ).
fof(f11961,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,[],[f11960]) ).
fof(f11962,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f6632]) ).
fof(f11963,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f6631]) ).
fof(f11978,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,[],[f10531]) ).
fof(f11979,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,[],[f11978]) ).
fof(f11986,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,[],[f8397]) ).
fof(f11987,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,[],[f11986]) ).
fof(f12004,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,[],[f11397]) ).
fof(f12005,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,[],[f12004]) ).
fof(f12010,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,[],[f10542]) ).
fof(f12011,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,[],[f12010]) ).
fof(f12024,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,[],[f11791]) ).
fof(f12025,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,[],[f12024]) ).
fof(f12026,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,[],[f11743]) ).
fof(f12027,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,[],[f12026]) ).
fof(f12028,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,[],[f11741]) ).
fof(f12029,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,[],[f12028]) ).
fof(f12030,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,[],[f11792]) ).
fof(f12031,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,[],[f12030]) ).
fof(f12032,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,[],[f11744]) ).
fof(f12033,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,[],[f12032]) ).
fof(f12034,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,[],[f11742]) ).
fof(f12035,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,[],[f12034]) ).
fof(f12038,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,[],[f11795]) ).
fof(f12039,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,[],[f12038]) ).
fof(f12040,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,[],[f11796]) ).
fof(f12041,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,[],[f12040]) ).
fof(f12384,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,[],[f10522]) ).
fof(f12385,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,[],[f12384]) ).
fof(f12795,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,[],[f11429]) ).
fof(f12796,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,[],[f12795]) ).
fof(f12829,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,[],[f10520]) ).
fof(f12830,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,[],[f12829]) ).
fof(f12853,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,[],[f11735]) ).
fof(f12854,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,[],[f12853]) ).
fof(f12857,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,[],[f11737]) ).
fof(f12858,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,[],[f12857]) ).
fof(f14587,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,[],[f8299]) ).
fof(f14588,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,[],[f14587]) ).
fof(f15158,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| ~ r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) )
& m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
& v2_cat_1(sK61)
& l1_cat_1(sK61)
& v2_cat_1(sK60)
& l1_cat_1(sK60)
& v2_cat_1(sK59)
& l1_cat_1(sK59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59,sK60,sK61,sK62]),skolemize(X0,sK59),skolemize(X1,sK60),skolemize(X2,sK61),skolemize(X3,sK62)],[f11961]) ).
fof(f15289,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,[],[f1394]) ).
fof(f16066,plain,
l1_cat_1(sK59),
inference(cnf_transformation,[],[f15158]) ).
fof(f16067,plain,
v2_cat_1(sK59),
inference(cnf_transformation,[],[f15158]) ).
fof(f16068,plain,
l1_cat_1(sK60),
inference(cnf_transformation,[],[f15158]) ).
fof(f16069,plain,
v2_cat_1(sK60),
inference(cnf_transformation,[],[f15158]) ).
fof(f16070,plain,
l1_cat_1(sK61),
inference(cnf_transformation,[],[f15158]) ).
fof(f16071,plain,
v2_cat_1(sK61),
inference(cnf_transformation,[],[f15158]) ).
fof(f16072,plain,
m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61)),
inference(cnf_transformation,[],[f15158]) ).
fof(f16073,plain,
( ~ r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| ~ r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) ),
inference(cnf_transformation,[],[f15158]) ).
fof(f16074,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f11962]) ).
fof(f16075,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f11963]) ).
fof(f16090,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,[],[f11979]) ).
fof(f16098,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,[],[f11987]) ).
fof(f16108,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,[],[f12005]) ).
fof(f16111,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,[],[f12011]) ).
fof(f16121,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,[],[f12025]) ).
fof(f16122,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,[],[f12027]) ).
fof(f16123,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,[],[f12029]) ).
fof(f16124,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,[],[f12031]) ).
fof(f16125,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,[],[f12033]) ).
fof(f16126,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,[],[f12035]) ).
fof(f16128,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,[],[f12039]) ).
fof(f16129,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,[],[f12041]) ).
fof(f16632,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,[],[f12385]) ).
fof(f16687,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f15289]) ).
fof(f17234,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,[],[f12796]) ).
fof(f17281,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,[],[f12830]) ).
fof(f17282,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,[],[f12830]) ).
fof(f17283,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,[],[f12830]) ).
fof(f17298,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,[],[f12854]) ).
fof(f17300,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,[],[f12858]) ).
fof(f19343,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,[],[f14588]) ).
fof(f21385,definition,
( spl615_8
<=> r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_8])],[avatar_definition]) ).
fof(f21389,definition,
( spl615_9
<=> r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_9])],[avatar_definition]) ).
fof(f21391,plain,
( ~ r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| spl615_9 ),
inference(avatar_component_clause,[],[f21389]) ).
fof(f21392,plain,
( ~ spl615_8
| ~ spl615_9 ),
inference(avatar_split_clause,[],[f16073,f21389,f21385]) ).
fof(f21519,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(resolution,[],[f16121,f16072]) ).
fof(f21526,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21519,f16071]) ).
fof(f21529,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21526,f16070]) ).
fof(f21530,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21529,f16069]) ).
fof(f21531,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21530,f16068]) ).
fof(f21532,plain,
( k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21531,f16067]) ).
fof(f21533,plain,
k11_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,k8_isocat_2(sK60,sK61)),
inference(forward_subsumption_resolution,[],[f21532,f16066]) ).
fof(f21534,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(resolution,[],[f16124,f16072]) ).
fof(f21541,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21534,f16071]) ).
fof(f21544,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21541,f16070]) ).
fof(f21545,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21544,f16069]) ).
fof(f21546,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21545,f16068]) ).
fof(f21547,plain,
( k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21546,f16067]) ).
fof(f21548,plain,
k12_isocat_2(sK59,sK60,sK61,sK62) = k2_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,k9_isocat_2(sK60,sK61)),
inference(forward_subsumption_resolution,[],[f21547,f16066]) ).
fof(f21549,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(superposition,[],[f16108,f21533]) ).
fof(f21550,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(superposition,[],[f16108,f21548]) ).
fof(f21551,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21550,f16072]) ).
fof(f21552,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21549,f16072]) ).
fof(f21553,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21551,f16071]) ).
fof(f21554,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21552,f16069]) ).
fof(f21555,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21553,f16070]) ).
fof(f21556,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21554,f16068]) ).
fof(f21557,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21555,f16067]) ).
fof(f21558,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21556,f16067]) ).
fof(f21559,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61)) ),
inference(forward_subsumption_resolution,[],[f21557,f16066]) ).
fof(f21560,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61)) ),
inference(forward_subsumption_resolution,[],[f21558,f16066]) ).
fof(f21562,definition,
( spl615_14
<=> l1_cat_1(k11_cat_2(sK60,sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_14])],[avatar_definition]) ).
fof(f21563,plain,
( l1_cat_1(k11_cat_2(sK60,sK61))
| ~ spl615_14 ),
inference(avatar_component_clause,[],[f21562]) ).
fof(f21564,plain,
( ~ l1_cat_1(k11_cat_2(sK60,sK61))
| spl615_14 ),
inference(avatar_component_clause,[],[f21562]) ).
fof(f21566,definition,
( spl615_15
<=> v2_cat_1(k11_cat_2(sK60,sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_15])],[avatar_definition]) ).
fof(f21567,plain,
( v2_cat_1(k11_cat_2(sK60,sK61))
| ~ spl615_15 ),
inference(avatar_component_clause,[],[f21566]) ).
fof(f21568,plain,
( ~ v2_cat_1(k11_cat_2(sK60,sK61))
| spl615_15 ),
inference(avatar_component_clause,[],[f21566]) ).
fof(f21570,definition,
( spl615_16
<=> m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61) ),
introduced(definition,[new_symbols(definition,[spl615_16])],[avatar_definition]) ).
fof(f21571,plain,
( m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_16 ),
inference(avatar_component_clause,[],[f21570]) ).
fof(f21572,plain,
( ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| spl615_16 ),
inference(avatar_component_clause,[],[f21570]) ).
fof(f21574,definition,
( spl615_17
<=> r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_17])],[avatar_definition]) ).
fof(f21576,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ spl615_17 ),
inference(avatar_component_clause,[],[f21574]) ).
fof(f21577,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_17 ),
inference(avatar_split_clause,[],[f21559,f21574,f21570,f21566,f21562]) ).
fof(f21579,definition,
( spl615_18
<=> m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60) ),
introduced(definition,[new_symbols(definition,[spl615_18])],[avatar_definition]) ).
fof(f21580,plain,
( m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_18 ),
inference(avatar_component_clause,[],[f21579]) ).
fof(f21581,plain,
( ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| spl615_18 ),
inference(avatar_component_clause,[],[f21579]) ).
fof(f21583,definition,
( spl615_19
<=> r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_19])],[avatar_definition]) ).
fof(f21585,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ spl615_19 ),
inference(avatar_component_clause,[],[f21583]) ).
fof(f21586,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_19 ),
inference(avatar_split_clause,[],[f21560,f21583,f21579,f21566,f21562]) ).
fof(f21587,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_14 ),
inference(resolution,[],[f21564,f16098]) ).
fof(f21588,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_14 ),
inference(forward_subsumption_resolution,[],[f21587,f16069]) ).
fof(f21589,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_14 ),
inference(forward_subsumption_resolution,[],[f21588,f16068]) ).
fof(f21590,plain,
( ~ l1_cat_1(sK61)
| spl615_14 ),
inference(forward_subsumption_resolution,[],[f21589,f16071]) ).
fof(f21591,plain,
( $false
| spl615_14 ),
inference(forward_subsumption_resolution,[],[f21590,f16070]) ).
fof(f21592,plain,
spl615_14,
inference(avatar_contradiction_clause,[],[f21591]) ).
fof(f21593,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_15 ),
inference(resolution,[],[f21568,f19343]) ).
fof(f21594,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_15 ),
inference(forward_subsumption_resolution,[],[f21593,f16069]) ).
fof(f21595,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_15 ),
inference(forward_subsumption_resolution,[],[f21594,f16068]) ).
fof(f21596,plain,
( ~ l1_cat_1(sK61)
| spl615_15 ),
inference(forward_subsumption_resolution,[],[f21595,f16071]) ).
fof(f21597,plain,
( $false
| spl615_15 ),
inference(forward_subsumption_resolution,[],[f21596,f16070]) ).
fof(f21598,plain,
spl615_15,
inference(avatar_contradiction_clause,[],[f21597]) ).
fof(f21599,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,[],[f16128,f16111]) ).
fof(f21600,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,[],[f21599]) ).
fof(f21601,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,[],[f21600,f16098]) ).
fof(f21602,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,[],[f21601,f19343]) ).
fof(f21603,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_16 ),
inference(resolution,[],[f17300,f21572]) ).
fof(f21608,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_16 ),
inference(forward_subsumption_resolution,[],[f21603,f16069]) ).
fof(f21611,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_16 ),
inference(forward_subsumption_resolution,[],[f21608,f16068]) ).
fof(f21614,plain,
( ~ l1_cat_1(sK61)
| spl615_16 ),
inference(forward_subsumption_resolution,[],[f21611,f16071]) ).
fof(f21615,plain,
( $false
| spl615_16 ),
inference(forward_subsumption_resolution,[],[f21614,f16070]) ).
fof(f21616,plain,
spl615_16,
inference(avatar_contradiction_clause,[],[f21615]) ).
fof(f21617,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,[],[f16129,f16111]) ).
fof(f21618,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,[],[f21617]) ).
fof(f21619,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,[],[f21618,f16098]) ).
fof(f21620,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,[],[f21619,f19343]) ).
fof(f21621,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_18 ),
inference(resolution,[],[f17298,f21581]) ).
fof(f21626,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_18 ),
inference(forward_subsumption_resolution,[],[f21621,f16069]) ).
fof(f21629,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| spl615_18 ),
inference(forward_subsumption_resolution,[],[f21626,f16068]) ).
fof(f21632,plain,
( ~ l1_cat_1(sK61)
| spl615_18 ),
inference(forward_subsumption_resolution,[],[f21629,f16071]) ).
fof(f21633,plain,
( $false
| spl615_18 ),
inference(forward_subsumption_resolution,[],[f21632,f16070]) ).
fof(f21634,plain,
spl615_18,
inference(avatar_contradiction_clause,[],[f21633]) ).
fof(f21657,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(resolution,[],[f21602,f16072]) ).
fof(f21660,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21657,f16071]) ).
fof(f21665,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21660,f16070]) ).
fof(f21670,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21665,f16069]) ).
fof(f21671,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21670,f16068]) ).
fof(f21672,plain,
( k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21671,f16067]) ).
fof(f21673,plain,
k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),
inference(forward_subsumption_resolution,[],[f21672,f16066]) ).
fof(f21728,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(resolution,[],[f21620,f16072]) ).
fof(f21731,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21728,f16071]) ).
fof(f21736,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21731,f16070]) ).
fof(f21741,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21736,f16069]) ).
fof(f21742,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21741,f16068]) ).
fof(f21743,plain,
( k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f21742,f16067]) ).
fof(f21744,plain,
k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)) = k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),
inference(forward_subsumption_resolution,[],[f21743,f16066]) ).
fof(f21861,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,[],[f16632,f16111]) ).
fof(f21862,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,[],[f16632,f16122]) ).
fof(f21863,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,[],[f16632,f16125]) ).
fof(f21864,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,[],[f21863]) ).
fof(f21865,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,[],[f21862]) ).
fof(f21866,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,[],[f21861]) ).
fof(f21867,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,[],[f21864,f16126]) ).
fof(f21868,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,[],[f21865,f16123]) ).
fof(f21869,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,[],[f21867,f16126]) ).
fof(f21870,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,[],[f21868,f16123]) ).
fof(f21871,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,[],[f21866,f17282]) ).
fof(f21872,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,[],[f21866,f17281]) ).
fof(f21873,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,[],[f21872]) ).
fof(f21874,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,[],[f21871]) ).
fof(f21875,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,[],[f21870,f17282]) ).
fof(f21876,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,[],[f21870,f17281]) ).
fof(f21877,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,[],[f21876]) ).
fof(f21878,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,[],[f21875]) ).
fof(f21879,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,[],[f21877,f16123]) ).
fof(f21880,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,[],[f21878,f16123]) ).
fof(f21881,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,[],[f21879,f16123]) ).
fof(f21882,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,[],[f21880,f16123]) ).
fof(f21883,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,[],[f21869,f17282]) ).
fof(f21884,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,[],[f21869,f17281]) ).
fof(f21885,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,[],[f21884]) ).
fof(f21886,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,[],[f21883]) ).
fof(f21887,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,[],[f21885,f16126]) ).
fof(f21888,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,[],[f21886,f16126]) ).
fof(f21889,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,[],[f21887,f16126]) ).
fof(f21890,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,[],[f21888,f16126]) ).
fof(f22010,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,[],[f17283,f21866]) ).
fof(f22011,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,[],[f17283,f21870]) ).
fof(f22012,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,[],[f17283,f21869]) ).
fof(f22013,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,[],[f22012]) ).
fof(f22014,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,[],[f22011]) ).
fof(f22015,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,[],[f22010]) ).
fof(f22016,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,[],[f22013,f16126]) ).
fof(f22017,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,[],[f22014,f16123]) ).
fof(f22018,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,[],[f22016,f16126]) ).
fof(f22019,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,[],[f22017,f16123]) ).
fof(f22156,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,[],[f22018,f16111]) ).
fof(f22161,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,[],[f22156]) ).
fof(f22164,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,[],[f22161,f16098]) ).
fof(f22167,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,[],[f22164,f19343]) ).
fof(f22168,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,[],[f22019,f16111]) ).
fof(f22173,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,[],[f22168]) ).
fof(f22176,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,[],[f22173,f16098]) ).
fof(f22179,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,[],[f22176,f19343]) ).
fof(f22255,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60) ),
inference(superposition,[],[f17234,f21533]) ).
fof(f22256,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61) ),
inference(superposition,[],[f17234,f21548]) ).
fof(f22269,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61) ),
inference(forward_subsumption_resolution,[],[f22256,f16067]) ).
fof(f22270,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60) ),
inference(forward_subsumption_resolution,[],[f22255,f16067]) ).
fof(f22280,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61) ),
inference(forward_subsumption_resolution,[],[f22269,f16066]) ).
fof(f22281,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60) ),
inference(forward_subsumption_resolution,[],[f22270,f16066]) ).
fof(f22291,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22280,f21567]) ).
fof(f22292,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22281,f21567]) ).
fof(f22296,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22291,f21563]) ).
fof(f22297,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22292,f21563]) ).
fof(f22301,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22296,f16071]) ).
fof(f22302,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22297,f16069]) ).
fof(f22303,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22301,f16070]) ).
fof(f22304,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22302,f16068]) ).
fof(f22305,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ m2_cat_1(k9_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK61)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22303,f16072]) ).
fof(f22306,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ m2_cat_1(k8_isocat_2(sK60,sK61),k11_cat_2(sK60,sK61),sK60)
| ~ spl615_14
| ~ spl615_15 ),
inference(forward_subsumption_resolution,[],[f22304,f16072]) ).
fof(f22307,plain,
( m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16 ),
inference(forward_subsumption_resolution,[],[f22305,f21571]) ).
fof(f22308,plain,
( m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18 ),
inference(forward_subsumption_resolution,[],[f22306,f21580]) ).
fof(f23545,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ spl615_19 ),
inference(resolution,[],[f16090,f21585]) ).
fof(f23551,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(resolution,[],[f16090,f21576]) ).
fof(f23562,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(duplicate_literal_removal,[],[f23551]) ).
fof(f23568,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ spl615_19 ),
inference(duplicate_literal_removal,[],[f23545]) ).
fof(f23615,definition,
( spl615_79
<=> v1_xboole_0(u2_cat_1(sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_79])],[avatar_definition]) ).
fof(f23617,plain,
( v1_xboole_0(u2_cat_1(sK61))
| ~ spl615_79 ),
inference(avatar_component_clause,[],[f23615]) ).
fof(f23673,definition,
( spl615_93
<=> m1_relset_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_93])],[avatar_definition]) ).
fof(f23675,plain,
( ~ m1_relset_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| spl615_93 ),
inference(avatar_component_clause,[],[f23673]) ).
fof(f23677,definition,
( spl615_94
<=> v1_funct_2(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_94])],[avatar_definition]) ).
fof(f23679,plain,
( ~ v1_funct_2(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| spl615_94 ),
inference(avatar_component_clause,[],[f23677]) ).
fof(f23681,definition,
( spl615_95
<=> v1_funct_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_95])],[avatar_definition]) ).
fof(f23683,plain,
( ~ v1_funct_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| spl615_95 ),
inference(avatar_component_clause,[],[f23681]) ).
fof(f23685,definition,
( spl615_96
<=> v1_xboole_0(u1_cat_1(sK59)) ),
introduced(definition,[new_symbols(definition,[spl615_96])],[avatar_definition]) ).
fof(f23687,plain,
( v1_xboole_0(u1_cat_1(sK59))
| ~ spl615_96 ),
inference(avatar_component_clause,[],[f23685]) ).
fof(f23694,definition,
( spl615_98
<=> m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_98])],[avatar_definition]) ).
fof(f23696,plain,
( ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| spl615_98 ),
inference(avatar_component_clause,[],[f23694]) ).
fof(f23698,definition,
( spl615_99
<=> v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61)) ),
introduced(definition,[new_symbols(definition,[spl615_99])],[avatar_definition]) ).
fof(f23700,plain,
( ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| spl615_99 ),
inference(avatar_component_clause,[],[f23698]) ).
fof(f23702,definition,
( spl615_100
<=> v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_100])],[avatar_definition]) ).
fof(f23704,plain,
( ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| spl615_100 ),
inference(avatar_component_clause,[],[f23702]) ).
fof(f23723,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(forward_demodulation,[],[f23562,f21744]) ).
fof(f23749,definition,
( spl615_111
<=> v1_xboole_0(u2_cat_1(sK60)) ),
introduced(definition,[new_symbols(definition,[spl615_111])],[avatar_definition]) ).
fof(f23751,plain,
( v1_xboole_0(u2_cat_1(sK60))
| ~ spl615_111 ),
inference(avatar_component_clause,[],[f23749]) ).
fof(f23799,definition,
( spl615_123
<=> m1_relset_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60)) ),
introduced(definition,[new_symbols(definition,[spl615_123])],[avatar_definition]) ).
fof(f23801,plain,
( ~ m1_relset_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_123 ),
inference(avatar_component_clause,[],[f23799]) ).
fof(f23803,definition,
( spl615_124
<=> v1_funct_2(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60)) ),
introduced(definition,[new_symbols(definition,[spl615_124])],[avatar_definition]) ).
fof(f23805,plain,
( ~ v1_funct_2(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_124 ),
inference(avatar_component_clause,[],[f23803]) ).
fof(f23807,definition,
( spl615_125
<=> v1_funct_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_125])],[avatar_definition]) ).
fof(f23809,plain,
( ~ v1_funct_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| spl615_125 ),
inference(avatar_component_clause,[],[f23807]) ).
fof(f23817,definition,
( spl615_127
<=> m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60)) ),
introduced(definition,[new_symbols(definition,[spl615_127])],[avatar_definition]) ).
fof(f23819,plain,
( ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_127 ),
inference(avatar_component_clause,[],[f23817]) ).
fof(f23821,definition,
( spl615_128
<=> v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60)) ),
introduced(definition,[new_symbols(definition,[spl615_128])],[avatar_definition]) ).
fof(f23823,plain,
( ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_128 ),
inference(avatar_component_clause,[],[f23821]) ).
fof(f23825,definition,
( spl615_129
<=> v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62))) ),
introduced(definition,[new_symbols(definition,[spl615_129])],[avatar_definition]) ).
fof(f23827,plain,
( ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| spl615_129 ),
inference(avatar_component_clause,[],[f23825]) ).
fof(f23845,plain,
( r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK60),u1_cat_1(sK59),u2_cat_1(sK60),k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ spl615_19 ),
inference(forward_demodulation,[],[f23568,f21673]) ).
fof(f23942,plain,
( ~ v1_funct_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(forward_demodulation,[],[f23723,f21744]) ).
fof(f23944,plain,
( v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_9
| ~ spl615_19 ),
inference(forward_subsumption_resolution,[],[f23845,f21391]) ).
fof(f23961,plain,
( ~ v1_funct_2(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k9_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(forward_demodulation,[],[f23942,f21744]) ).
fof(f23962,plain,
( ~ v1_funct_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_2(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_9
| ~ spl615_19 ),
inference(forward_demodulation,[],[f23944,f21673]) ).
fof(f23967,plain,
( ~ m1_relset_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_2(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ v1_funct_1(k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| r4_nattra_1(u1_cat_1(sK59),u2_cat_1(sK61),u1_cat_1(sK59),u2_cat_1(sK61),k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),k14_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK61))
| ~ v1_funct_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ m1_relset_1(k7_nattra_1(sK59,sK61,k12_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK61))
| ~ spl615_17 ),
inference(forward_demodulation,[],[f23961,f21744]) ).
fof(f23968,plain,
( ~ v1_funct_2(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ m1_relset_1(k6_isocat_1(sK59,k11_cat_2(sK60,sK61),sK60,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),k8_isocat_2(sK60,sK61)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_9
| ~ spl615_19 ),
inference(forward_demodulation,[],[f23962,f21673]) ).
fof(f23973,plain,
( ~ spl615_98
| ~ spl615_99
| ~ spl615_100
| spl615_79
| spl615_96
| spl615_8
| ~ spl615_95
| ~ spl615_94
| ~ spl615_93
| ~ spl615_17 ),
inference(avatar_split_clause,[],[f23967,f21574,f23673,f23677,f23681,f21385,f23685,f23615,f23702,f23698,f23694]) ).
fof(f23974,plain,
( ~ m1_relset_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_2(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ v1_funct_1(k13_isocat_2(sK59,sK60,sK61,sK62,sK62,k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62)))
| v1_xboole_0(u1_cat_1(sK59))
| v1_xboole_0(u2_cat_1(sK60))
| ~ v1_funct_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)))
| ~ v1_funct_2(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| ~ m1_relset_1(k7_nattra_1(sK59,sK60,k11_isocat_2(sK59,sK60,sK61,sK62)),u1_cat_1(sK59),u2_cat_1(sK60))
| spl615_9
| ~ spl615_19 ),
inference(forward_demodulation,[],[f23968,f21673]) ).
fof(f23976,plain,
( ~ spl615_127
| ~ spl615_128
| ~ spl615_129
| spl615_111
| spl615_96
| ~ spl615_125
| ~ spl615_124
| ~ spl615_123
| spl615_9
| ~ spl615_19 ),
inference(avatar_split_clause,[],[f23974,f21583,f21389,f23799,f23803,f23807,f23685,f23749,f23825,f23821,f23817]) ).
fof(f23978,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| spl615_129 ),
inference(resolution,[],[f23827,f22015]) ).
fof(f23979,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| spl615_129 ),
inference(forward_subsumption_resolution,[],[f23978,f16067]) ).
fof(f23980,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| spl615_129 ),
inference(forward_subsumption_resolution,[],[f23979,f16066]) ).
fof(f23981,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| spl615_129 ),
inference(forward_subsumption_resolution,[],[f23980,f16069]) ).
fof(f23982,plain,
( ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| spl615_129 ),
inference(forward_subsumption_resolution,[],[f23981,f16068]) ).
fof(f23983,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_129 ),
inference(forward_subsumption_resolution,[],[f23982,f22308]) ).
fof(f23984,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_129 ),
inference(avatar_contradiction_clause,[],[f23983]) ).
fof(f23985,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| spl615_100 ),
inference(resolution,[],[f23704,f22015]) ).
fof(f23986,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| spl615_100 ),
inference(forward_subsumption_resolution,[],[f23985,f16067]) ).
fof(f23987,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| spl615_100 ),
inference(forward_subsumption_resolution,[],[f23986,f16066]) ).
fof(f23988,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| spl615_100 ),
inference(forward_subsumption_resolution,[],[f23987,f16071]) ).
fof(f23989,plain,
( ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| spl615_100 ),
inference(forward_subsumption_resolution,[],[f23988,f16070]) ).
fof(f23990,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_100 ),
inference(forward_subsumption_resolution,[],[f23989,f22307]) ).
fof(f23991,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_100 ),
inference(avatar_contradiction_clause,[],[f23990]) ).
fof(f24235,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,[],[f16687,f21873]) ).
fof(f24236,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,[],[f16687,f21881]) ).
fof(f24237,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,[],[f16687,f21889]) ).
fof(f24239,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_127 ),
inference(resolution,[],[f24235,f23819]) ).
fof(f24240,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_98 ),
inference(resolution,[],[f24235,f23696]) ).
fof(f24241,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_98 ),
inference(forward_subsumption_resolution,[],[f24240,f16066]) ).
fof(f24242,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_127 ),
inference(forward_subsumption_resolution,[],[f24239,f16066]) ).
fof(f24243,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_98 ),
inference(forward_subsumption_resolution,[],[f24241,f16071]) ).
fof(f24244,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_127 ),
inference(forward_subsumption_resolution,[],[f24242,f16069]) ).
fof(f24245,plain,
( ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_98 ),
inference(forward_subsumption_resolution,[],[f24243,f16070]) ).
fof(f24246,plain,
( ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_127 ),
inference(forward_subsumption_resolution,[],[f24244,f16068]) ).
fof(f24247,plain,
( ~ v2_cat_1(sK59)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_98 ),
inference(forward_subsumption_resolution,[],[f24245,f22307]) ).
fof(f24248,plain,
( ~ v2_cat_1(sK59)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_127 ),
inference(forward_subsumption_resolution,[],[f24246,f22308]) ).
fof(f24249,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_98 ),
inference(forward_subsumption_resolution,[],[f24247,f16067]) ).
fof(f24250,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_98 ),
inference(avatar_contradiction_clause,[],[f24249]) ).
fof(f24251,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_127 ),
inference(forward_subsumption_resolution,[],[f24248,f16067]) ).
fof(f24252,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_127 ),
inference(avatar_contradiction_clause,[],[f24251]) ).
fof(f24253,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(resolution,[],[f24236,f23801]) ).
fof(f24254,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(duplicate_literal_removal,[],[f24253]) ).
fof(f24255,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24254,f16066]) ).
fof(f24256,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24255,f16069]) ).
fof(f24257,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24256,f16068]) ).
fof(f24258,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24257,f16071]) ).
fof(f24259,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24258,f16070]) ).
fof(f24260,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24259,f16072]) ).
fof(f24261,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24260,f16067]) ).
fof(f24262,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_123 ),
inference(resolution,[],[f24261,f16111]) ).
fof(f24263,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24262,f16067]) ).
fof(f24264,plain,
( ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24263,f16066]) ).
fof(f24265,plain,
( ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_15
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24264,f21567]) ).
fof(f24266,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_14
| ~ spl615_15
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24265,f21563]) ).
fof(f24267,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| spl615_123 ),
inference(forward_subsumption_resolution,[],[f24266,f16072]) ).
fof(f24268,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_123 ),
inference(avatar_contradiction_clause,[],[f24267]) ).
fof(f24269,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(resolution,[],[f24237,f23675]) ).
fof(f24270,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(duplicate_literal_removal,[],[f24269]) ).
fof(f24271,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24270,f16066]) ).
fof(f24272,plain,
( ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24271,f16071]) ).
fof(f24273,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24272,f16070]) ).
fof(f24274,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24273,f16069]) ).
fof(f24275,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24274,f16068]) ).
fof(f24276,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24275,f16072]) ).
fof(f24277,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24276,f16067]) ).
fof(f24278,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_93 ),
inference(resolution,[],[f24277,f16111]) ).
fof(f24279,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24278,f16067]) ).
fof(f24280,plain,
( ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24279,f16066]) ).
fof(f24281,plain,
( ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_15
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24280,f21567]) ).
fof(f24282,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_14
| ~ spl615_15
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24281,f21563]) ).
fof(f24283,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| spl615_93 ),
inference(forward_subsumption_resolution,[],[f24282,f16072]) ).
fof(f24284,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_93 ),
inference(avatar_contradiction_clause,[],[f24283]) ).
fof(f24285,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_99 ),
inference(resolution,[],[f23700,f21874]) ).
fof(f24286,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_99 ),
inference(forward_subsumption_resolution,[],[f24285,f16066]) ).
fof(f24287,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_99 ),
inference(forward_subsumption_resolution,[],[f24286,f16071]) ).
fof(f24288,plain,
( ~ m2_cat_1(k12_isocat_2(sK59,sK60,sK61,sK62),sK59,sK61)
| ~ v2_cat_1(sK59)
| spl615_99 ),
inference(forward_subsumption_resolution,[],[f24287,f16070]) ).
fof(f24289,plain,
( ~ v2_cat_1(sK59)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_99 ),
inference(forward_subsumption_resolution,[],[f24288,f22307]) ).
fof(f24290,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_99 ),
inference(forward_subsumption_resolution,[],[f24289,f16067]) ).
fof(f24291,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_99 ),
inference(avatar_contradiction_clause,[],[f24290]) ).
fof(f24299,plain,
( ~ l1_cat_1(sK61)
| ~ spl615_79 ),
inference(resolution,[],[f23617,f16074]) ).
fof(f24300,plain,
( $false
| ~ spl615_79 ),
inference(forward_subsumption_resolution,[],[f24299,f16070]) ).
fof(f24301,plain,
~ spl615_79,
inference(avatar_contradiction_clause,[],[f24300]) ).
fof(f24302,plain,
( ~ l1_cat_1(sK59)
| ~ spl615_96 ),
inference(resolution,[],[f23687,f16075]) ).
fof(f24303,plain,
( $false
| ~ spl615_96 ),
inference(forward_subsumption_resolution,[],[f24302,f16066]) ).
fof(f24304,plain,
~ spl615_96,
inference(avatar_contradiction_clause,[],[f24303]) ).
fof(f24406,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(resolution,[],[f23805,f21882]) ).
fof(f24407,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(duplicate_literal_removal,[],[f24406]) ).
fof(f24408,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24407,f16066]) ).
fof(f24409,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24408,f16069]) ).
fof(f24410,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24409,f16068]) ).
fof(f24411,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24410,f16071]) ).
fof(f24412,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24411,f16070]) ).
fof(f24413,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24412,f16072]) ).
fof(f24414,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24413,f16067]) ).
fof(f24415,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_124 ),
inference(resolution,[],[f24414,f16111]) ).
fof(f24416,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24415,f16067]) ).
fof(f24417,plain,
( ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24416,f16066]) ).
fof(f24418,plain,
( ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_15
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24417,f21567]) ).
fof(f24419,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_14
| ~ spl615_15
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24418,f21563]) ).
fof(f24420,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| spl615_124 ),
inference(forward_subsumption_resolution,[],[f24419,f16072]) ).
fof(f24421,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_124 ),
inference(avatar_contradiction_clause,[],[f24420]) ).
fof(f24423,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(resolution,[],[f23809,f22179]) ).
fof(f24424,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24423,f16066]) ).
fof(f24425,plain,
( ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24424,f16069]) ).
fof(f24426,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24425,f16068]) ).
fof(f24427,plain,
( ~ l1_cat_1(sK61)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24426,f16071]) ).
fof(f24428,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24427,f16070]) ).
fof(f24429,plain,
( ~ v2_cat_1(sK59)
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24428,f16072]) ).
fof(f24430,plain,
( $false
| spl615_125 ),
inference(forward_subsumption_resolution,[],[f24429,f16067]) ).
fof(f24431,plain,
spl615_125,
inference(avatar_contradiction_clause,[],[f24430]) ).
fof(f24439,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_128 ),
inference(resolution,[],[f23823,f21874]) ).
fof(f24440,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_128 ),
inference(forward_subsumption_resolution,[],[f24439,f16066]) ).
fof(f24441,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_128 ),
inference(forward_subsumption_resolution,[],[f24440,f16069]) ).
fof(f24442,plain,
( ~ m2_cat_1(k11_isocat_2(sK59,sK60,sK61,sK62),sK59,sK60)
| ~ v2_cat_1(sK59)
| spl615_128 ),
inference(forward_subsumption_resolution,[],[f24441,f16068]) ).
fof(f24443,plain,
( ~ v2_cat_1(sK59)
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_128 ),
inference(forward_subsumption_resolution,[],[f24442,f22308]) ).
fof(f24444,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_128 ),
inference(forward_subsumption_resolution,[],[f24443,f16067]) ).
fof(f24445,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_128 ),
inference(avatar_contradiction_clause,[],[f24444]) ).
fof(f24447,plain,
( ~ l1_cat_1(sK60)
| ~ spl615_111 ),
inference(resolution,[],[f23751,f16074]) ).
fof(f24448,plain,
( $false
| ~ spl615_111 ),
inference(forward_subsumption_resolution,[],[f24447,f16068]) ).
fof(f24449,plain,
~ spl615_111,
inference(avatar_contradiction_clause,[],[f24448]) ).
fof(f24457,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(resolution,[],[f23679,f21890]) ).
fof(f24458,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(duplicate_literal_removal,[],[f24457]) ).
fof(f24459,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24458,f16066]) ).
fof(f24460,plain,
( ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24459,f16071]) ).
fof(f24461,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24460,f16070]) ).
fof(f24462,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24461,f16069]) ).
fof(f24463,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24462,f16068]) ).
fof(f24464,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| ~ v2_cat_1(sK59)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24463,f16072]) ).
fof(f24465,plain,
( ~ m2_nattra_1(k7_nattra_1(sK59,k11_cat_2(sK60,sK61),sK62),sK59,k11_cat_2(sK60,sK61),sK62,sK62)
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24464,f16067]) ).
fof(f24466,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_94 ),
inference(resolution,[],[f24465,f16111]) ).
fof(f24467,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24466,f16067]) ).
fof(f24468,plain,
( ~ v2_cat_1(k11_cat_2(sK60,sK61))
| ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24467,f16066]) ).
fof(f24469,plain,
( ~ l1_cat_1(k11_cat_2(sK60,sK61))
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_15
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24468,f21567]) ).
fof(f24470,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ spl615_14
| ~ spl615_15
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24469,f21563]) ).
fof(f24471,plain,
( $false
| ~ spl615_14
| ~ spl615_15
| spl615_94 ),
inference(forward_subsumption_resolution,[],[f24470,f16072]) ).
fof(f24472,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_94 ),
inference(avatar_contradiction_clause,[],[f24471]) ).
fof(f24474,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(resolution,[],[f23683,f22167]) ).
fof(f24475,plain,
( ~ v2_cat_1(sK61)
| ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24474,f16066]) ).
fof(f24476,plain,
( ~ l1_cat_1(sK61)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24475,f16071]) ).
fof(f24477,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24476,f16070]) ).
fof(f24478,plain,
( ~ l1_cat_1(sK60)
| ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24477,f16069]) ).
fof(f24479,plain,
( ~ m2_cat_1(sK62,sK59,k11_cat_2(sK60,sK61))
| ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24478,f16068]) ).
fof(f24480,plain,
( ~ v2_cat_1(sK59)
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24479,f16072]) ).
fof(f24481,plain,
( $false
| spl615_95 ),
inference(forward_subsumption_resolution,[],[f24480,f16067]) ).
fof(f24482,plain,
spl615_95,
inference(avatar_contradiction_clause,[],[f24481]) ).
cnf(s5,plain,
( ~ spl615_8
| ~ spl615_9 ),
inference(sat_conversion,[],[f21392]) ).
cnf(s9,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_17 ),
inference(sat_conversion,[],[f21577]) ).
cnf(s10,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_19 ),
inference(sat_conversion,[],[f21586]) ).
cnf(s11,plain,
spl615_14,
inference(sat_conversion,[],[f21592]) ).
cnf(s12,plain,
spl615_15,
inference(sat_conversion,[],[f21598]) ).
cnf(s13,plain,
spl615_16,
inference(sat_conversion,[],[f21616]) ).
cnf(s14,plain,
spl615_18,
inference(sat_conversion,[],[f21634]) ).
cnf(s75,plain,
( spl615_8
| ~ spl615_17
| spl615_79
| ~ spl615_93
| ~ spl615_94
| ~ spl615_95
| spl615_96
| ~ spl615_98
| ~ spl615_99
| ~ spl615_100 ),
inference(sat_conversion,[],[f23973]) ).
cnf(s76,plain,
( spl615_9
| ~ spl615_19
| spl615_96
| spl615_111
| ~ spl615_123
| ~ spl615_124
| ~ spl615_125
| ~ spl615_127
| ~ spl615_128
| ~ spl615_129 ),
inference(sat_conversion,[],[f23976]) ).
cnf(s77,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_129 ),
inference(sat_conversion,[],[f23984]) ).
cnf(s78,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_100 ),
inference(sat_conversion,[],[f23991]) ).
cnf(s88,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_98 ),
inference(sat_conversion,[],[f24250]) ).
cnf(s89,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_127 ),
inference(sat_conversion,[],[f24252]) ).
cnf(s90,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_123 ),
inference(sat_conversion,[],[f24268]) ).
cnf(s91,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_93 ),
inference(sat_conversion,[],[f24284]) ).
cnf(s92,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_16
| spl615_99 ),
inference(sat_conversion,[],[f24291]) ).
cnf(s94,plain,
~ spl615_79,
inference(sat_conversion,[],[f24301]) ).
cnf(s95,plain,
~ spl615_96,
inference(sat_conversion,[],[f24304]) ).
cnf(s106,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_124 ),
inference(sat_conversion,[],[f24421]) ).
cnf(s107,plain,
spl615_125,
inference(sat_conversion,[],[f24431]) ).
cnf(s109,plain,
( ~ spl615_14
| ~ spl615_15
| ~ spl615_18
| spl615_128 ),
inference(sat_conversion,[],[f24445]) ).
cnf(s110,plain,
~ spl615_111,
inference(sat_conversion,[],[f24449]) ).
cnf(s111,plain,
( ~ spl615_14
| ~ spl615_15
| spl615_94 ),
inference(sat_conversion,[],[f24472]) ).
cnf(s112,plain,
spl615_95,
inference(sat_conversion,[],[f24482]) ).
cnf(s116,plain,
( spl615_9
| ~ spl615_19
| ~ spl615_123
| ~ spl615_124
| ~ spl615_127
| ~ spl615_128
| ~ spl615_129 ),
inference(rat,[],[s76,s107,s110,s95]) ).
cnf(s117,plain,
( spl615_8
| ~ spl615_17
| ~ spl615_93
| ~ spl615_94
| ~ spl615_98
| ~ spl615_99
| ~ spl615_100 ),
inference(rat,[],[s75,s95,s112,s94]) ).
cnf(s134,plain,
spl615_94,
inference(rat,[],[s111,s12,s11]) ).
cnf(s135,plain,
spl615_128,
inference(rat,[],[s109,s12,s14,s11]) ).
cnf(s136,plain,
spl615_124,
inference(rat,[],[s106,s12,s11]) ).
cnf(s143,plain,
spl615_99,
inference(rat,[],[s92,s12,s13,s11]) ).
cnf(s144,plain,
spl615_93,
inference(rat,[],[s91,s12,s11]) ).
cnf(s145,plain,
spl615_123,
inference(rat,[],[s90,s12,s11]) ).
cnf(s146,plain,
spl615_127,
inference(rat,[],[s89,s12,s14,s11]) ).
cnf(s147,plain,
spl615_98,
inference(rat,[],[s88,s12,s13,s11]) ).
cnf(s156,plain,
spl615_100,
inference(rat,[],[s78,s12,s13,s11]) ).
cnf(s157,plain,
spl615_129,
inference(rat,[],[s77,s12,s14,s11]) ).
cnf(s191,plain,
spl615_19,
inference(rat,[],[s10,s14,s12,s11]) ).
cnf(s192,plain,
spl615_9,
inference(rat,[],[s116,s157,s135,s146,s136,s145,s191]) ).
cnf(s193,plain,
spl615_17,
inference(rat,[],[s9,s13,s12,s11]) ).
cnf(s194,plain,
spl615_8,
inference(rat,[],[s117,s156,s143,s147,s134,s144,s193]) ).
cnf(s195,plain,
$false,
inference(rat,[],[s5,s192,s194]) ).
fof(f24483,plain,
$false,
inference(avatar_sat_refutation,[],[s195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT027+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n019.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 21:18:50 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.13/2.89 % (291283)Detected formulas, will run a generic FOF schedule.
% 11.13/2.89 % (291291)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3089699260:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 11.13/2.89 % (291290)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=2520411967:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 11.13/2.89 % (291288)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=3994459394:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 11.13/2.89 % (291289)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=2177563968:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 11.13/2.89 % (291291)Refutation not found, incomplete strategy
% 11.13/2.89 % (291291)------------------------------
% 11.13/2.89 % (291291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.89 % (291291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.89 % (291291)CaDiCaL version: 2.1.3
% 11.13/2.89 % (291291)Termination reason: Refutation not found, incomplete strategy
% 11.13/2.89 % (291291)Time elapsed: 0.038 s
% 11.13/2.89 % (291291)Peak memory usage: 104 MB
% 11.13/2.89 % (291291)Instructions burned: 75 (million)
% 11.13/2.89 % (291293)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1539605268:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 11.13/2.89 % (291292)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4020076704:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 11.13/2.89 % (291294)dis-21_1_sil=8000:lcm=predicate:random_seed=3220859358:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 11.13/2.89 % (291293)Instruction limit reached!
% 11.13/2.89 % (291293)------------------------------
% 11.13/2.89 % (291293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.89 % (291293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.89 % (291293)CaDiCaL version: 2.1.3
% 11.13/2.89 % (291293)Termination reason: Instruction limit
% 11.13/2.89 % (291293)Termination phase: Property scanning
% 11.13/2.89 % (291293)Time elapsed: 0.059 s
% 11.13/2.89 % (291293)Peak memory usage: 100 MB
% 11.13/2.89 % (291293)Instructions burned: 140 (million)
% 11.13/2.89 % (291292)Instruction limit reached!
% 11.13/2.89 % (291292)------------------------------
% 11.13/2.89 % (291292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.89 % (291292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.89 % (291292)CaDiCaL version: 2.1.3
% 11.13/2.89 % (291292)Termination reason: Instruction limit
% 11.13/2.89 % (291292)Termination phase: Clausification
% 11.13/2.89 % (291292)Time elapsed: 0.092 s
% 11.13/2.89 % (291292)Peak memory usage: 103 MB
% 11.13/2.89 % (291292)Instructions burned: 119 (million)
% 11.13/2.89 % (291294)Instruction limit reached!
% 11.13/2.89 % (291294)------------------------------
% 11.13/2.89 % (291294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.89 % (291294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.89 % (291294)CaDiCaL version: 2.1.3
% 11.13/2.89 % (291294)Termination reason: Instruction limit
% 11.13/2.89 % (291294)Termination phase: Preprocessing 1
% 11.13/2.89 % (291294)Time elapsed: 0.096 s
% 11.13/2.89 % (291294)Peak memory usage: 101 MB
% 11.13/2.89 % (291294)Instructions burned: 130 (million)
% 11.13/2.89 % (291291)------------------------------
% 11.13/2.89 % (291291)------------------------------
% 11.13/2.89 % (291302)lrs+10_1_sil=8000:sp=occurrence:random_seed=1607859342:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 11.13/2.89 % (291305)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=1092711335:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 11.13/2.89 % (291304)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3804153835:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 11.13/2.89 % (291303)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2293005840:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 18.46/3.83 % (291303)Instruction limit reached!
% 18.46/3.83 % (291303)------------------------------
% 18.46/3.83 % (291303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291303)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291303)Termination reason: Instruction limit
% 18.46/3.83 % (291303)Termination phase: SInE selection
% 18.46/3.83 % (291303)Time elapsed: 0.069 s
% 18.46/3.83 % (291303)Peak memory usage: 100 MB
% 18.46/3.83 % (291303)Instructions burned: 157 (million)
% 18.46/3.83 % (291305)Instruction limit reached!
% 18.46/3.83 % (291305)------------------------------
% 18.46/3.83 % (291305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291305)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291305)Termination reason: Instruction limit
% 18.46/3.83 % (291305)Termination phase: Preprocessing 1
% 18.46/3.83 % (291305)Time elapsed: 0.075 s
% 18.46/3.83 % (291305)Peak memory usage: 101 MB
% 18.46/3.83 % (291305)Instructions burned: 249 (million)
% 18.46/3.83 % (291311)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2866072720:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 18.46/3.83 % (291302)Instruction limit reached!
% 18.46/3.83 % (291302)------------------------------
% 18.46/3.83 % (291302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291302)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291302)Termination reason: Instruction limit
% 18.46/3.83 % (291302)Termination phase: Saturation
% 18.46/3.83 % (291302)Time elapsed: 0.201 s
% 18.46/3.83 % (291302)Peak memory usage: 107 MB
% 18.46/3.83 % (291302)Instructions burned: 285 (million)
% 18.46/3.83 % (291310)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2492368318:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 18.46/3.83 % (291304)Instruction limit reached!
% 18.46/3.83 % (291304)------------------------------
% 18.46/3.83 % (291304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291304)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291304)Termination reason: Instruction limit
% 18.46/3.83 % (291304)Termination phase: Saturation
% 18.46/3.83 % (291304)Time elapsed: 0.224 s
% 18.46/3.83 % (291304)Peak memory usage: 107 MB
% 18.46/3.83 % (291304)Instructions burned: 326 (million)
% 18.46/3.83 % (291313)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3793467362:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 18.46/3.83 % (291315)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=81393290:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 18.46/3.83 % (291310)Instruction limit reached!
% 18.46/3.83 % (291310)------------------------------
% 18.46/3.83 % (291310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291310)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291310)Termination reason: Instruction limit
% 18.46/3.83 % (291310)Termination phase: Saturation
% 18.46/3.83 % (291310)Time elapsed: 0.184 s
% 18.46/3.83 % (291310)Peak memory usage: 108 MB
% 18.46/3.83 % (291310)Instructions burned: 296 (million)
% 18.46/3.83 % (291313)Instruction limit reached!
% 18.46/3.83 % (291313)------------------------------
% 18.46/3.83 % (291313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291313)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291313)Termination reason: Instruction limit
% 18.46/3.83 % (291313)Termination phase: Preprocessing 3
% 18.46/3.83 % (291313)Time elapsed: 0.095 s
% 18.46/3.83 % (291313)Peak memory usage: 103 MB
% 18.46/3.83 % (291313)Instructions burned: 115 (million)
% 18.46/3.83 % (291315)Instruction limit reached!
% 18.46/3.83 % (291315)------------------------------
% 18.46/3.83 % (291315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.46/3.83 % (291315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.46/3.83 % (291315)CaDiCaL version: 2.1.3
% 18.46/3.83 % (291315)Termination reason: Instruction limit
% 18.46/3.83 % (291315)Termination phase: Preprocessing 2
% 21.96/4.30 % (291315)Time elapsed: 0.109 s
% 21.96/4.30 % (291315)Peak memory usage: 107 MB
% 21.96/4.30 % (291315)Instructions burned: 127 (million)
% 21.96/4.30 % (291319)lrs+10_1_sil=8000:sp=occurrence:random_seed=2569331605:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 21.96/4.30 % (291318)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2703612526:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 21.96/4.30 % (291318)Instruction limit reached!
% 21.96/4.30 % (291318)------------------------------
% 21.96/4.30 % (291318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291318)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291318)Termination reason: Instruction limit
% 21.96/4.30 % (291318)Termination phase: Property scanning
% 21.96/4.30 % (291318)Time elapsed: 0.049 s
% 21.96/4.30 % (291318)Peak memory usage: 100 MB
% 21.96/4.30 % (291318)Instructions burned: 115 (million)
% 21.96/4.30 % (291320)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3579778618:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 21.96/4.30 % (291323)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2939837078:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 21.96/4.30 % (291320)Instruction limit reached!
% 21.96/4.30 % (291320)------------------------------
% 21.96/4.30 % (291320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291320)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291320)Termination reason: Instruction limit
% 21.96/4.30 % (291320)Termination phase: Saturation
% 21.96/4.30 % (291320)Time elapsed: 0.266 s
% 21.96/4.30 % (291320)Peak memory usage: 108 MB
% 21.96/4.30 % (291320)Instructions burned: 438 (million)
% 21.96/4.30 % (291319)Instruction limit reached!
% 21.96/4.30 % (291319)------------------------------
% 21.96/4.30 % (291319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291319)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291319)Termination reason: Instruction limit
% 21.96/4.30 % (291319)Termination phase: Saturation
% 21.96/4.30 % (291319)Time elapsed: 0.494 s
% 21.96/4.30 % (291319)Peak memory usage: 120 MB
% 21.96/4.30 % (291319)Instructions burned: 907 (million)
% 21.96/4.30 % (291326)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2943028312:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 21.96/4.30 % (291311)Instruction limit reached!
% 21.96/4.30 % (291311)------------------------------
% 21.96/4.30 % (291311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291311)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291311)Termination reason: Instruction limit
% 21.96/4.30 % (291311)Termination phase: Saturation
% 21.96/4.30 % (291311)Time elapsed: 0.904 s
% 21.96/4.30 % (291311)Peak memory usage: 260 MB
% 21.96/4.30 % (291311)Instructions burned: 2351 (million)
% 21.96/4.30 % (291326)Instruction limit reached!
% 21.96/4.30 % (291326)------------------------------
% 21.96/4.30 % (291326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291326)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291326)Termination reason: Instruction limit
% 21.96/4.30 % (291326)Termination phase: Equality resolution with deletion
% 21.96/4.30 % (291326)Time elapsed: 0.103 s
% 21.96/4.30 % (291326)Peak memory usage: 104 MB
% 21.96/4.30 % (291326)Instructions burned: 134 (million)
% 21.96/4.30 % (291328)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2982575686:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 21.96/4.30 % (291329)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=894112882:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 21.96/4.30 % (291330)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=1111838753:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 21.96/4.30 % (291330)Instruction limit reached!
% 21.96/4.30 % (291330)------------------------------
% 21.96/4.30 % (291330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291330)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291330)Termination reason: Instruction limit
% 21.96/4.30 % (291330)Termination phase: Property scanning
% 21.96/4.30 % (291330)Time elapsed: 0.055 s
% 21.96/4.30 % (291330)Peak memory usage: 100 MB
% 21.96/4.30 % (291330)Instructions burned: 126 (million)
% 21.96/4.30 % (291334)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3792695535:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 21.96/4.30 % (291328)Instruction limit reached!
% 21.96/4.30 % (291328)------------------------------
% 21.96/4.30 % (291328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291328)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291328)Termination reason: Instruction limit
% 21.96/4.30 % (291328)Termination phase: Function definition elimination
% 21.96/4.30 % (291328)Time elapsed: 0.370 s
% 21.96/4.30 % (291328)Peak memory usage: 117 MB
% 21.96/4.30 % (291328)Instructions burned: 592 (million)
% 21.96/4.30 % (291334)Instruction limit reached!
% 21.96/4.30 % (291334)------------------------------
% 21.96/4.30 % (291334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291334)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291334)Termination reason: Instruction limit
% 21.96/4.30 % (291334)Termination phase: Property scanning
% 21.96/4.30 % (291334)Time elapsed: 0.057 s
% 21.96/4.30 % (291334)Peak memory usage: 100 MB
% 21.96/4.30 % (291334)Instructions burned: 135 (million)
% 21.96/4.30 % (291337)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2888358214:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 21.96/4.30 % (291336)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2863566477:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 21.96/4.30 % (291337)Refutation not found, incomplete strategy
% 21.96/4.30 % (291337)------------------------------
% 21.96/4.30 % (291337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291337)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291337)Termination reason: Refutation not found, incomplete strategy
% 21.96/4.30 % (291337)Time elapsed: 0.064 s
% 21.96/4.30 % (291337)Peak memory usage: 104 MB
% 21.96/4.30 % (291337)Instructions burned: 80 (million)
% 21.96/4.30 % (291336)Instruction limit reached!
% 21.96/4.30 % (291336)------------------------------
% 21.96/4.30 % (291336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291336)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291336)Termination reason: Instruction limit
% 21.96/4.30 % (291336)Termination phase: Saturation
% 21.96/4.30 % (291336)Time elapsed: 0.093 s
% 21.96/4.30 % (291336)Peak memory usage: 105 MB
% 21.96/4.30 % (291336)Instructions burned: 143 (million)
% 21.96/4.30 % (291340)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=3496828113:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 21.96/4.30 % (291337)------------------------------
% 21.96/4.30 % (291337)------------------------------
% 21.96/4.30 % (291342)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=1140550686:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 21.96/4.30 % (291342)Instruction limit reached!
% 21.96/4.30 % (291342)------------------------------
% 21.96/4.30 % (291342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.96/4.30 % (291342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/4.30 % (291342)CaDiCaL version: 2.1.3
% 21.96/4.30 % (291342)Termination reason: Instruction limit
% 21.96/4.30 % (291342)Termination phase: Unused predicate definition removal
% 21.96/4.30 % (291342)Time elapsed: 0.116 s
% 21.96/4.30 % (291342)Peak memory usage: 102 MB
% 21.96/4.30 % (291342)Instructions burned: 150 (million)
% 21.96/4.30 % (291344)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2934585068:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 21.96/4.30 % (291329)First to succeed.
% 21.96/4.30 % (291329)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-291283"
% 21.96/4.30 % (291329)Refutation found. Thanks to Tanya!
% 21.96/4.30 % SZS status Theorem for theBenchmark
% 21.96/4.30 % SZS output start Proof for theBenchmark
% See solution above
% 22.62/4.49 % (291329)------------------------------
% 22.62/4.49 % (291329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.62/4.49 % (291329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.62/4.49 % (291329)CaDiCaL version: 2.1.3
% 22.62/4.49 % (291329)Termination reason: Refutation
% 22.62/4.49 % (291329)Time elapsed: 1.306 s
% 22.62/4.49 % (291329)Peak memory usage: 190 MB
% 22.62/4.49 % (291329)Instructions burned: 3709 (million)
% 22.62/4.49 % (291329)------------------------------
% 22.62/4.49 % (291329)------------------------------
% 22.62/4.49 % (291283)Success in time 3.62 s
% 22.62/4.49 % Vampire exiting
%------------------------------------------------------------------------------