%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT027+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 16.90s 3.63s
% Output : Refutation 20.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 48
% Syntax : Number of formulae : 492 ( 66 unt; 28 def)
% Number of atoms : 2321 ( 78 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 3463 (1634 ~;1648 |; 114 &)
% ( 18 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 18 prp; 0-6 aty)
% Number of functors : 27 ( 27 usr; 15 con; 0-7 aty)
% Number of variables : 407 ( 0 sgn 399 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1161,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f3672,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_cat_1) ).
fof(f3673,axiom,
! [X0] :
( l1_cat_1(X0)
=> ~ v1_xboole_0(u2_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_cat_1) ).
fof(f3782,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f3877,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1)
& m2_cat_1(X3,X0,X1) )
=> ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
=> ( v1_funct_1(X4)
& v1_funct_2(X4,u1_cat_1(X0),u2_cat_1(X1))
& m2_relset_1(X4,u1_cat_1(X0),u2_cat_1(X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_nattra_1) ).
fof(f3879,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1)
& m2_cat_1(X3,X0,X1) )
=> ! [X4] :
( m2_nattra_1(X4,X0,X1,X2,X3)
=> m1_nattra_1(X4,X0,X1,X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_nattra_1) ).
fof(f3888,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X2)
& ~ v1_xboole_0(X3)
& v1_funct_1(X4)
& v1_funct_2(X4,X0,X1)
& m1_relset_1(X4,X0,X1)
& v1_funct_1(X5)
& v1_funct_2(X5,X2,X3)
& m1_relset_1(X5,X2,X3) )
=> ( r4_nattra_1(X0,X1,X2,X3,X4,X5)
=> r4_nattra_1(X0,X1,X2,X3,X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r4_nattra_1) ).
fof(f3899,axiom,
! [X0,X1,X2] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1) )
=> m2_nattra_1(k7_nattra_1(X0,X1,X2),X0,X1,X2,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_nattra_1) ).
fof(f3954,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ! [X4] :
( m2_cat_1(X4,X1,X2)
=> r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k6_isocat_1(X0,X1,X2,X3,X3,k7_nattra_1(X0,X1,X3),X4),k7_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X4))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_isocat_1) ).
fof(f4002,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f4004,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f4008,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
=> m2_cat_1(k11_isocat_2(X0,X1,X2,X3),X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_isocat_2) ).
fof(f4009,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
=> m2_cat_1(k12_isocat_2(X0,X1,X2,X3),X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_isocat_2) ).
fof(f4010,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& m2_cat_1(X4,X0,k11_cat_2(X1,X2))
& m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
=> m2_nattra_1(k13_isocat_2(X0,X1,X2,X3,X4,X5),X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k13_isocat_2) ).
fof(f4011,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,k11_cat_2(X1,X2))
& m2_cat_1(X4,X0,k11_cat_2(X1,X2))
& m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
=> m2_nattra_1(k14_isocat_2(X0,X1,X2,X3,X4,X5),X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k14_isocat_2) ).
fof(f4058,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f4059,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f4062,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f4063,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f4066,conjecture,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k7_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3)),k13_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3)))
& r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k7_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3)),k14_isocat_2(X0,X1,X2,X3,X3,k7_nattra_1(X0,k11_cat_2(X1,X2),X3))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_isocat_2) ).
fof(f4067,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)],[f4066]) ).
fof(f8073,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f3672]) ).
fof(f8074,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f3673]) ).
fof(f8260,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,[],[f3782]) ).
fof(f8261,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,[],[f8260]) ).
fof(f8426,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,[],[f3877]) ).
fof(f8427,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,[],[f8426]) ).
fof(f8430,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,[],[f3879]) ).
fof(f8431,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,[],[f8430]) ).
fof(f8448,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,[],[f3888]) ).
fof(f8449,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,[],[f8448]) ).
fof(f8470,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,[],[f3899]) ).
fof(f8471,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,[],[f8470]) ).
fof(f8572,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,[],[f3954]) ).
fof(f8573,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,[],[f8572]) ).
fof(f8664,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,[],[f4002]) ).
fof(f8665,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,[],[f8664]) ).
fof(f8668,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,[],[f4004]) ).
fof(f8669,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,[],[f8668]) ).
fof(f8676,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,[],[f4008]) ).
fof(f8677,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,[],[f8676]) ).
fof(f8678,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,[],[f4009]) ).
fof(f8679,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,[],[f8678]) ).
fof(f8680,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,[],[f4010]) ).
fof(f8681,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,[],[f8680]) ).
fof(f8682,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,[],[f4011]) ).
fof(f8683,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,[],[f8682]) ).
fof(f8768,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,[],[f4058]) ).
fof(f8769,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,[],[f8768]) ).
fof(f8770,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,[],[f4059]) ).
fof(f8771,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,[],[f8770]) ).
fof(f8776,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,[],[f4062]) ).
fof(f8777,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,[],[f8776]) ).
fof(f8778,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,[],[f4063]) ).
fof(f8779,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,[],[f8778]) ).
fof(f8784,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,[],[f4067]) ).
fof(f8785,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,[],[f8784]) ).
fof(f9540,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,[],[f1161]) ).
fof(f11183,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k7_nattra_1(sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514)),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514)))
| ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k7_nattra_1(sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514)),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514))) )
& m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
& v2_cat_1(sK1513)
& l1_cat_1(sK1513)
& v2_cat_1(sK1512)
& l1_cat_1(sK1512)
& v2_cat_1(sK1511)
& l1_cat_1(sK1511) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1511,sK1512,sK1513,sK1514]),skolemize(X0,sK1511),skolemize(X1,sK1512),skolemize(X2,sK1513),skolemize(X3,sK1514)],[f8785]) ).
fof(f12837,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f9540]) ).
fof(f18079,plain,
! [X0] :
( ~ v1_xboole_0(u1_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f8073]) ).
fof(f18080,plain,
! [X0] :
( ~ v1_xboole_0(u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f8074]) ).
fof(f18269,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,[],[f8261]) ).
fof(f18270,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,[],[f8261]) ).
fof(f18512,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,[],[f8427]) ).
fof(f18513,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,[],[f8427]) ).
fof(f18514,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,[],[f8427]) ).
fof(f18516,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,[],[f8431]) ).
fof(f18525,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,[],[f8449]) ).
fof(f18540,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,[],[f8471]) ).
fof(f18625,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,[],[f8573]) ).
fof(f18689,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,[],[f8665]) ).
fof(f18691,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,[],[f8669]) ).
fof(f18695,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,[],[f8677]) ).
fof(f18696,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,[],[f8679]) ).
fof(f18697,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,[],[f8681]) ).
fof(f18698,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,[],[f8683]) ).
fof(f18779,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,[],[f8769]) ).
fof(f18780,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,[],[f8771]) ).
fof(f18784,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,[],[f8777]) ).
fof(f18785,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,[],[f8779]) ).
fof(f18789,plain,
l1_cat_1(sK1511),
inference(cnf_transformation,[],[f11183]) ).
fof(f18790,plain,
v2_cat_1(sK1511),
inference(cnf_transformation,[],[f11183]) ).
fof(f18791,plain,
l1_cat_1(sK1512),
inference(cnf_transformation,[],[f11183]) ).
fof(f18792,plain,
v2_cat_1(sK1512),
inference(cnf_transformation,[],[f11183]) ).
fof(f18793,plain,
l1_cat_1(sK1513),
inference(cnf_transformation,[],[f11183]) ).
fof(f18794,plain,
v2_cat_1(sK1513),
inference(cnf_transformation,[],[f11183]) ).
fof(f18795,plain,
m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)),
inference(cnf_transformation,[],[f11183]) ).
fof(f18796,plain,
( ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k7_nattra_1(sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514)),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514)))
| ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k7_nattra_1(sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514)),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514))) ),
inference(cnf_transformation,[],[f11183]) ).
fof(f22432,definition,
sF1515 = u1_cat_1(sK1511),
introduced(definition,[new_symbols(definition,[sF1515])],[function_definition]) ).
fof(f22433,plain,
u1_cat_1(sK1511) = sF1515,
inference(reorient_equations,[],[f22432]) ).
fof(f22434,definition,
sF1516 = u2_cat_1(sK1512),
introduced(definition,[new_symbols(definition,[sF1516])],[function_definition]) ).
fof(f22435,plain,
u2_cat_1(sK1512) = sF1516,
inference(reorient_equations,[],[f22434]) ).
fof(f22436,definition,
sF1517 = k11_isocat_2(sK1511,sK1512,sK1513,sK1514),
introduced(definition,[new_symbols(definition,[sF1517])],[function_definition]) ).
fof(f22437,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = sF1517,
inference(reorient_equations,[],[f22436]) ).
fof(f22438,definition,
sF1518 = k7_nattra_1(sK1511,sK1512,sF1517),
introduced(definition,[new_symbols(definition,[sF1518])],[function_definition]) ).
fof(f22439,plain,
k7_nattra_1(sK1511,sK1512,sF1517) = sF1518,
inference(reorient_equations,[],[f22438]) ).
fof(f22440,definition,
sF1519 = k11_cat_2(sK1512,sK1513),
introduced(definition,[new_symbols(definition,[sF1519])],[function_definition]) ).
fof(f22441,plain,
k11_cat_2(sK1512,sK1513) = sF1519,
inference(reorient_equations,[],[f22440]) ).
fof(f22442,definition,
sF1520 = k7_nattra_1(sK1511,sF1519,sK1514),
introduced(definition,[new_symbols(definition,[sF1520])],[function_definition]) ).
fof(f22443,plain,
k7_nattra_1(sK1511,sF1519,sK1514) = sF1520,
inference(reorient_equations,[],[f22442]) ).
fof(f22444,definition,
sF1521 = k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520),
introduced(definition,[new_symbols(definition,[sF1521])],[function_definition]) ).
fof(f22445,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = sF1521,
inference(reorient_equations,[],[f22444]) ).
fof(f22446,definition,
sF1522 = u2_cat_1(sK1513),
introduced(definition,[new_symbols(definition,[sF1522])],[function_definition]) ).
fof(f22447,plain,
u2_cat_1(sK1513) = sF1522,
inference(reorient_equations,[],[f22446]) ).
fof(f22448,definition,
sF1523 = k12_isocat_2(sK1511,sK1512,sK1513,sK1514),
introduced(definition,[new_symbols(definition,[sF1523])],[function_definition]) ).
fof(f22449,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = sF1523,
inference(reorient_equations,[],[f22448]) ).
fof(f22450,definition,
sF1524 = k7_nattra_1(sK1511,sK1513,sF1523),
introduced(definition,[new_symbols(definition,[sF1524])],[function_definition]) ).
fof(f22451,plain,
k7_nattra_1(sK1511,sK1513,sF1523) = sF1524,
inference(reorient_equations,[],[f22450]) ).
fof(f22452,definition,
sF1525 = k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520),
introduced(definition,[new_symbols(definition,[sF1525])],[function_definition]) ).
fof(f22453,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = sF1525,
inference(reorient_equations,[],[f22452]) ).
fof(f22454,plain,
( ~ r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1518,sF1521)
| ~ r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1524,sF1525) ),
inference(definition_folding,[],[f18796,f22453,f22443,f22441,f22451,f22449,f22447,f22433,f22447,f22433,f22445,f22443,f22441,f22439,f22437,f22435,f22433,f22435,f22433]) ).
fof(f22455,plain,
m2_cat_1(sK1514,sK1511,sF1519),
inference(definition_folding,[],[f18795,f22441]) ).
fof(f22486,definition,
( spl1526_1
<=> r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1524,sF1525) ),
introduced(definition,[new_symbols(definition,[spl1526_1])],[avatar_definition]) ).
fof(f22488,plain,
( ~ r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1524,sF1525)
| spl1526_1 ),
inference(avatar_component_clause,[],[f22486]) ).
fof(f22490,definition,
( spl1526_2
<=> r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1518,sF1521) ),
introduced(definition,[new_symbols(definition,[spl1526_2])],[avatar_definition]) ).
fof(f22492,plain,
( ~ r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1518,sF1521)
| spl1526_2 ),
inference(avatar_component_clause,[],[f22490]) ).
fof(f22493,plain,
( ~ spl1526_1
| ~ spl1526_2 ),
inference(avatar_split_clause,[],[f22454,f22490,f22486]) ).
fof(f26759,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(superposition,[],[f18779,f22441]) ).
fof(f26764,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(superposition,[],[f18780,f22441]) ).
fof(f26767,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(superposition,[],[f18696,f22449]) ).
fof(f26768,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(superposition,[],[f18695,f22437]) ).
fof(f26771,plain,
( m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ m2_cat_1(sK1514,sK1511,sF1519) ),
inference(superposition,[],[f18540,f22443]) ).
fof(f26772,plain,
( l1_cat_1(sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18269,f22441]) ).
fof(f26773,plain,
( v2_cat_1(sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18270,f22441]) ).
fof(f26790,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18691,f22441]) ).
fof(f26795,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18689,f22441]) ).
fof(f26824,plain,
( ~ v1_xboole_0(sF1515)
| ~ l1_cat_1(sK1511) ),
inference(superposition,[],[f18079,f22433]) ).
fof(f26828,plain,
~ v1_xboole_0(sF1515),
inference(forward_subsumption_resolution,[],[f26824,f18789]) ).
fof(f26837,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(superposition,[],[f18784,f22441]) ).
fof(f26839,plain,
( ~ v1_xboole_0(sF1522)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18080,f22447]) ).
fof(f26840,plain,
( ~ v1_xboole_0(sF1516)
| ~ l1_cat_1(sK1512) ),
inference(superposition,[],[f18080,f22435]) ).
fof(f26841,plain,
~ v1_xboole_0(sF1516),
inference(forward_subsumption_resolution,[],[f26840,f18791]) ).
fof(f26842,plain,
~ v1_xboole_0(sF1522),
inference(forward_subsumption_resolution,[],[f26839,f18793]) ).
fof(f26844,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(superposition,[],[f18785,f22441]) ).
fof(f27001,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,[],[f18516,f18540]) ).
fof(f27002,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,[],[f27001]) ).
fof(f27103,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(superposition,[],[f18698,f22453]) ).
fof(f27106,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(duplicate_literal_removal,[],[f27103]) ).
fof(f27161,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(superposition,[],[f18697,f22445]) ).
fof(f27164,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(duplicate_literal_removal,[],[f27161]) ).
fof(f27559,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26759,f18794]) ).
fof(f27562,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26764,f18794]) ).
fof(f27565,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f26767,f18790]) ).
fof(f27566,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f26768,f18790]) ).
fof(f27567,plain,
( m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ m2_cat_1(sK1514,sK1511,sF1519) ),
inference(forward_subsumption_resolution,[],[f26771,f18790]) ).
fof(f27570,plain,
( l1_cat_1(sF1519)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26772,f18792]) ).
fof(f27571,plain,
( v2_cat_1(sF1519)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26773,f18792]) ).
fof(f27581,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26790,f18792]) ).
fof(f27585,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26795,f18792]) ).
fof(f27615,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26837,f18794]) ).
fof(f27617,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26844,f18794]) ).
fof(f27756,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f27106,f18790]) ).
fof(f27782,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f27164,f18790]) ).
fof(f27907,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27559,f18793]) ).
fof(f27910,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27562,f18793]) ).
fof(f27913,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f27565,f18789]) ).
fof(f27914,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f27566,f18789]) ).
fof(f27915,plain,
( m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ m2_cat_1(sK1514,sK1511,sF1519) ),
inference(forward_subsumption_resolution,[],[f27567,f18789]) ).
fof(f27918,plain,
( l1_cat_1(sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27570,f18791]) ).
fof(f27919,plain,
( v2_cat_1(sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27571,f18791]) ).
fof(f27924,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27581,f18791]) ).
fof(f27928,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27585,f18791]) ).
fof(f27958,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27615,f18793]) ).
fof(f27960,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27617,f18793]) ).
fof(f28099,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f27756,f18789]) ).
fof(f28125,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f27782,f18789]) ).
fof(f28233,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27907,f18792]) ).
fof(f28234,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27910,f18792]) ).
fof(f28235,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f27913,f18792]) ).
fof(f28236,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f27914,f18792]) ).
fof(f28237,plain,
( m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519) ),
inference(forward_subsumption_resolution,[],[f27915,f22455]) ).
fof(f28240,plain,
( l1_cat_1(sF1519)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27918,f18794]) ).
fof(f28241,plain,
( v2_cat_1(sF1519)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27919,f18794]) ).
fof(f28243,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27924,f18794]) ).
fof(f28246,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27928,f18794]) ).
fof(f28259,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27958,f18792]) ).
fof(f28260,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27960,f18792]) ).
fof(f28266,definition,
( spl1526_600
<=> l1_cat_1(sF1519) ),
introduced(definition,[new_symbols(definition,[spl1526_600])],[avatar_definition]) ).
fof(f28267,plain,
( l1_cat_1(sF1519)
| ~ spl1526_600 ),
inference(avatar_component_clause,[],[f28266]) ).
fof(f28270,definition,
( spl1526_601
<=> v2_cat_1(sF1519) ),
introduced(definition,[new_symbols(definition,[spl1526_601])],[avatar_definition]) ).
fof(f28271,plain,
( v2_cat_1(sF1519)
| ~ spl1526_601 ),
inference(avatar_component_clause,[],[f28270]) ).
fof(f28342,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28099,f18792]) ).
fof(f28359,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28125,f18792]) ).
fof(f28396,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28233,f18791]) ).
fof(f28397,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1519)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1519,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28234,f18791]) ).
fof(f28398,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28235,f18791]) ).
fof(f28399,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28236,f18791]) ).
fof(f28401,definition,
( spl1526_616
<=> m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514) ),
introduced(definition,[new_symbols(definition,[spl1526_616])],[avatar_definition]) ).
fof(f28403,plain,
( m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| ~ spl1526_616 ),
inference(avatar_component_clause,[],[f28401]) ).
fof(f28404,plain,
( ~ spl1526_600
| ~ spl1526_601
| spl1526_616 ),
inference(avatar_split_clause,[],[f28237,f28401,f28270,f28266]) ).
fof(f28407,plain,
l1_cat_1(sF1519),
inference(forward_subsumption_resolution,[],[f28240,f18793]) ).
fof(f28408,plain,
v2_cat_1(sF1519),
inference(forward_subsumption_resolution,[],[f28241,f18793]) ).
fof(f28414,plain,
m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513),
inference(forward_subsumption_resolution,[],[f28243,f18793]) ).
fof(f28415,plain,
m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512),
inference(forward_subsumption_resolution,[],[f28246,f18793]) ).
fof(f28428,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28259,f18791]) ).
fof(f28429,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1519,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1519,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1519)
| ~ m2_cat_1(X2,X1,sF1519)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28260,f18791]) ).
fof(f28468,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28342,f18791]) ).
fof(f28475,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28359,f18791]) ).
fof(f28489,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28398,f18794]) ).
fof(f28490,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28399,f18794]) ).
fof(f28492,definition,
( spl1526_620
<=> m2_cat_1(sF1523,sK1511,sK1513) ),
introduced(definition,[new_symbols(definition,[spl1526_620])],[avatar_definition]) ).
fof(f28493,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620 ),
inference(avatar_component_clause,[],[f28492]) ).
fof(f28501,definition,
( spl1526_622
<=> m2_cat_1(sF1517,sK1511,sK1512) ),
introduced(definition,[new_symbols(definition,[spl1526_622])],[avatar_definition]) ).
fof(f28502,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622 ),
inference(avatar_component_clause,[],[f28501]) ).
fof(f28509,plain,
spl1526_600,
inference(avatar_split_clause,[],[f28407,f28266]) ).
fof(f28510,plain,
spl1526_601,
inference(avatar_split_clause,[],[f28408,f28270]) ).
fof(f28540,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28468,f18794]) ).
fof(f28543,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28475,f18794]) ).
fof(f28550,plain,
( m2_cat_1(sF1523,sK1511,sK1513)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28489,f18793]) ).
fof(f28551,plain,
( m2_cat_1(sF1517,sK1511,sK1512)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)) ),
inference(forward_subsumption_resolution,[],[f28490,f18793]) ).
fof(f28579,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28540,f18793]) ).
fof(f28582,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1514))
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28543,f18793]) ).
fof(f28585,plain,
( ~ m2_cat_1(sK1514,sK1511,sF1519)
| m2_cat_1(sF1523,sK1511,sK1513) ),
inference(forward_demodulation,[],[f28550,f22441]) ).
fof(f28586,plain,
( ~ m2_cat_1(sK1514,sK1511,sF1519)
| m2_cat_1(sF1517,sK1511,sK1512) ),
inference(forward_demodulation,[],[f28551,f22441]) ).
fof(f28595,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_demodulation,[],[f28579,f22449]) ).
fof(f28598,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513))
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_demodulation,[],[f28582,f22437]) ).
fof(f28599,plain,
m2_cat_1(sF1523,sK1511,sK1513),
inference(forward_subsumption_resolution,[],[f28585,f22455]) ).
fof(f28600,plain,
m2_cat_1(sF1517,sK1511,sK1512),
inference(forward_subsumption_resolution,[],[f28586,f22455]) ).
fof(f28609,plain,
( ~ m2_cat_1(sK1514,sK1511,sF1519)
| m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_demodulation,[],[f28595,f22441]) ).
fof(f28612,plain,
( ~ m2_cat_1(sK1514,sK1511,sF1519)
| m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_demodulation,[],[f28598,f22441]) ).
fof(f28613,plain,
spl1526_620,
inference(avatar_split_clause,[],[f28599,f28492]) ).
fof(f28614,plain,
spl1526_622,
inference(avatar_split_clause,[],[f28600,f28501]) ).
fof(f28623,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28609,f22455]) ).
fof(f28626,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ m2_nattra_1(sF1520,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1514) ),
inference(forward_subsumption_resolution,[],[f28612,f22455]) ).
fof(f28635,plain,
( ~ m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523) ),
inference(forward_demodulation,[],[f28623,f22441]) ).
fof(f28638,plain,
( ~ m2_nattra_1(sF1520,sK1511,sF1519,sK1514,sK1514)
| m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517) ),
inference(forward_demodulation,[],[f28626,f22441]) ).
fof(f28642,definition,
( spl1526_632
<=> m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523) ),
introduced(definition,[new_symbols(definition,[spl1526_632])],[avatar_definition]) ).
fof(f28644,plain,
( m2_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ spl1526_632 ),
inference(avatar_component_clause,[],[f28642]) ).
fof(f28645,plain,
( spl1526_632
| ~ spl1526_616 ),
inference(avatar_split_clause,[],[f28635,f28401,f28642]) ).
fof(f28647,definition,
( spl1526_633
<=> m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517) ),
introduced(definition,[new_symbols(definition,[spl1526_633])],[avatar_definition]) ).
fof(f28649,plain,
( m2_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ spl1526_633 ),
inference(avatar_component_clause,[],[f28647]) ).
fof(f28650,plain,
( spl1526_633
| ~ spl1526_616 ),
inference(avatar_split_clause,[],[f28638,f28401,f28647]) ).
fof(f28669,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1513,sK1514,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f28397,f22455]) ).
fof(f28678,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1513,sK1514,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28669,f18790]) ).
fof(f28693,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f28678,f18789]) ).
fof(f28708,plain,
sF1523 = k2_isocat_1(sK1511,sF1519,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f28693,f22449]) ).
fof(f28735,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1512,sK1514,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f28396,f22455]) ).
fof(f28744,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1512,sK1514,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28735,f18790]) ).
fof(f28759,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1519,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f28744,f18789]) ).
fof(f28774,plain,
sF1517 = k2_isocat_1(sK1511,sF1519,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f28759,f22437]) ).
fof(f28930,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1519,sK1512)
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(superposition,[],[f18625,f28774]) ).
fof(f28931,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28930,f28415]) ).
fof(f28936,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28931,f22455]) ).
fof(f28941,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28936,f18792]) ).
fof(f28946,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f28941,f18791]) ).
fof(f28951,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f28946,f28271]) ).
fof(f28956,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f28951,f28267]) ).
fof(f28961,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ l1_cat_1(sK1511)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f28956,f18790]) ).
fof(f28966,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1512,sF1517))
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f28961,f18789]) ).
fof(f28971,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k8_isocat_2(sK1512,sK1513)),sF1518)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f28966,f22439]) ).
fof(f28976,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513)),sF1518)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f28971,f22443]) ).
fof(f28978,plain,
( r4_nattra_1(u1_cat_1(sK1511),sF1516,u1_cat_1(sK1511),sF1516,k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513)),sF1518)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f28976,f22435]) ).
fof(f28980,plain,
( r4_nattra_1(sF1515,sF1516,sF1515,sF1516,k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513)),sF1518)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f28978,f22433]) ).
fof(f28990,definition,
( spl1526_636
<=> m1_relset_1(sF1518,sF1515,sF1516) ),
introduced(definition,[new_symbols(definition,[spl1526_636])],[avatar_definition]) ).
fof(f28991,plain,
( m1_relset_1(sF1518,sF1515,sF1516)
| ~ spl1526_636 ),
inference(avatar_component_clause,[],[f28990]) ).
fof(f28992,plain,
( ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_636 ),
inference(avatar_component_clause,[],[f28990]) ).
fof(f28994,definition,
( spl1526_637
<=> v1_funct_2(sF1518,sF1515,sF1516) ),
introduced(definition,[new_symbols(definition,[spl1526_637])],[avatar_definition]) ).
fof(f28995,plain,
( v1_funct_2(sF1518,sF1515,sF1516)
| ~ spl1526_637 ),
inference(avatar_component_clause,[],[f28994]) ).
fof(f28998,definition,
( spl1526_638
<=> v1_funct_1(sF1518) ),
introduced(definition,[new_symbols(definition,[spl1526_638])],[avatar_definition]) ).
fof(f28999,plain,
( v1_funct_1(sF1518)
| ~ spl1526_638 ),
inference(avatar_component_clause,[],[f28998]) ).
fof(f29000,plain,
( ~ v1_funct_1(sF1518)
| spl1526_638 ),
inference(avatar_component_clause,[],[f28998]) ).
fof(f29032,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1519,sK1513)
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(superposition,[],[f18625,f28708]) ).
fof(f29033,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29032,f28414]) ).
fof(f29038,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29033,f22455]) ).
fof(f29043,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29038,f18794]) ).
fof(f29048,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ v2_cat_1(sF1519)
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29043,f18793]) ).
fof(f29053,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ l1_cat_1(sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f29048,f28271]) ).
fof(f29058,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f29053,f28267]) ).
fof(f29063,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ l1_cat_1(sK1511)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f29058,f18790]) ).
fof(f29068,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),k7_nattra_1(sK1511,sK1513,sF1523))
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_subsumption_resolution,[],[f29063,f18789]) ).
fof(f29073,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,k7_nattra_1(sK1511,sF1519,sK1514),k9_isocat_2(sK1512,sK1513)),sF1524)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f29068,f22451]) ).
fof(f29078,plain,
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513)),sF1524)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f29073,f22443]) ).
fof(f29080,plain,
( r4_nattra_1(u1_cat_1(sK1511),sF1522,u1_cat_1(sK1511),sF1522,k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513)),sF1524)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f29078,f22447]) ).
fof(f29082,plain,
( r4_nattra_1(sF1515,sF1522,sF1515,sF1522,k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513)),sF1524)
| ~ spl1526_600
| ~ spl1526_601 ),
inference(forward_demodulation,[],[f29080,f22433]) ).
fof(f29092,definition,
( spl1526_644
<=> m1_relset_1(sF1524,sF1515,sF1522) ),
introduced(definition,[new_symbols(definition,[spl1526_644])],[avatar_definition]) ).
fof(f29093,plain,
( m1_relset_1(sF1524,sF1515,sF1522)
| ~ spl1526_644 ),
inference(avatar_component_clause,[],[f29092]) ).
fof(f29094,plain,
( ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_644 ),
inference(avatar_component_clause,[],[f29092]) ).
fof(f29096,definition,
( spl1526_645
<=> v1_funct_2(sF1524,sF1515,sF1522) ),
introduced(definition,[new_symbols(definition,[spl1526_645])],[avatar_definition]) ).
fof(f29097,plain,
( v1_funct_2(sF1524,sF1515,sF1522)
| ~ spl1526_645 ),
inference(avatar_component_clause,[],[f29096]) ).
fof(f29100,definition,
( spl1526_646
<=> v1_funct_1(sF1524) ),
introduced(definition,[new_symbols(definition,[spl1526_646])],[avatar_definition]) ).
fof(f29101,plain,
( v1_funct_1(sF1524)
| ~ spl1526_646 ),
inference(avatar_component_clause,[],[f29100]) ).
fof(f29102,plain,
( ~ v1_funct_1(sF1524)
| spl1526_646 ),
inference(avatar_component_clause,[],[f29100]) ).
fof(f29475,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(resolution,[],[f28644,f18516]) ).
fof(f29476,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(duplicate_literal_removal,[],[f29475]) ).
fof(f29477,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f29476,f18790]) ).
fof(f29478,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f29477,f18789]) ).
fof(f29479,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f29478,f18794]) ).
fof(f29480,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f29479,f18793]) ).
fof(f29481,plain,
( m1_nattra_1(sF1525,sK1511,sK1513,sF1523,sF1523)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f29480,f28493]) ).
fof(f29482,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_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) ),
inference(resolution,[],[f27002,f18514]) ).
fof(f29483,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,[],[f27002,f18512]) ).
fof(f29484,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,[],[f27002,f18513]) ).
fof(f29490,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,[],[f29484]) ).
fof(f29491,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,[],[f29483]) ).
fof(f29492,plain,
! [X2,X0,X1] :
( v1_funct_1(k7_nattra_1(X0,X1,X2))
| ~ 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,[],[f29482]) ).
fof(f29508,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(resolution,[],[f28649,f18516]) ).
fof(f29509,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(duplicate_literal_removal,[],[f29508]) ).
fof(f29510,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f29509,f18790]) ).
fof(f29511,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f29510,f18789]) ).
fof(f29512,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f29511,f18792]) ).
fof(f29513,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f29512,f18791]) ).
fof(f29514,plain,
( m1_nattra_1(sF1521,sK1511,sK1512,sF1517,sF1517)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f29513,f28502]) ).
fof(f29516,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29490,f22439]) ).
fof(f29517,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29490,f22451]) ).
fof(f29526,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29517,f18789]) ).
fof(f29527,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29516,f18789]) ).
fof(f29533,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29526,f18794]) ).
fof(f29534,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29527,f18792]) ).
fof(f29537,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29533,f18793]) ).
fof(f29538,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29534,f18791]) ).
fof(f29541,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ spl1526_620 ),
inference(forward_subsumption_resolution,[],[f29537,f28493]) ).
fof(f29542,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ spl1526_622 ),
inference(forward_subsumption_resolution,[],[f29538,f28502]) ).
fof(f29544,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ spl1526_620 ),
inference(forward_subsumption_resolution,[],[f29541,f18790]) ).
fof(f29545,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ spl1526_622 ),
inference(forward_subsumption_resolution,[],[f29542,f18790]) ).
fof(f29547,plain,
( v1_funct_2(sF1524,u1_cat_1(sK1511),sF1522)
| ~ spl1526_620 ),
inference(forward_demodulation,[],[f29544,f22447]) ).
fof(f29548,plain,
( v1_funct_2(sF1518,u1_cat_1(sK1511),sF1516)
| ~ spl1526_622 ),
inference(forward_demodulation,[],[f29545,f22435]) ).
fof(f29549,plain,
( v1_funct_2(sF1524,sF1515,sF1522)
| ~ spl1526_620 ),
inference(forward_demodulation,[],[f29547,f22433]) ).
fof(f29550,plain,
( v1_funct_2(sF1518,sF1515,sF1516)
| ~ spl1526_622 ),
inference(forward_demodulation,[],[f29548,f22433]) ).
fof(f29551,plain,
( spl1526_645
| ~ spl1526_620 ),
inference(avatar_split_clause,[],[f29549,f28492,f29096]) ).
fof(f29552,plain,
( spl1526_637
| ~ spl1526_622 ),
inference(avatar_split_clause,[],[f29550,f28501,f28994]) ).
fof(f29769,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29491,f22439]) ).
fof(f29770,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29491,f22451]) ).
fof(f29780,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29770,f18789]) ).
fof(f29781,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29769,f18789]) ).
fof(f29786,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29780,f18794]) ).
fof(f29787,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29781,f18792]) ).
fof(f29789,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29786,f18793]) ).
fof(f29790,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f29787,f18791]) ).
fof(f29792,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ spl1526_620 ),
inference(forward_subsumption_resolution,[],[f29789,f28493]) ).
fof(f29793,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ spl1526_622 ),
inference(forward_subsumption_resolution,[],[f29790,f28502]) ).
fof(f29795,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ spl1526_620 ),
inference(forward_subsumption_resolution,[],[f29792,f18790]) ).
fof(f29796,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ spl1526_622 ),
inference(forward_subsumption_resolution,[],[f29793,f18790]) ).
fof(f29798,plain,
( m2_relset_1(sF1524,u1_cat_1(sK1511),sF1522)
| ~ spl1526_620 ),
inference(forward_demodulation,[],[f29795,f22447]) ).
fof(f29799,plain,
( m2_relset_1(sF1518,u1_cat_1(sK1511),sF1516)
| ~ spl1526_622 ),
inference(forward_demodulation,[],[f29796,f22435]) ).
fof(f29800,plain,
( m2_relset_1(sF1524,sF1515,sF1522)
| ~ spl1526_620 ),
inference(forward_demodulation,[],[f29798,f22433]) ).
fof(f29801,plain,
( m2_relset_1(sF1518,sF1515,sF1516)
| ~ spl1526_622 ),
inference(forward_demodulation,[],[f29799,f22433]) ).
fof(f29802,plain,
( m1_relset_1(sF1518,sF1515,sF1516)
| ~ spl1526_622 ),
inference(resolution,[],[f29801,f12837]) ).
fof(f29803,plain,
( $false
| ~ spl1526_622
| spl1526_636 ),
inference(forward_subsumption_resolution,[],[f29802,f28992]) ).
fof(f29804,plain,
( ~ spl1526_622
| spl1526_636 ),
inference(avatar_contradiction_clause,[],[f29803]) ).
fof(f29805,plain,
( m1_relset_1(sF1524,sF1515,sF1522)
| ~ spl1526_620 ),
inference(resolution,[],[f29800,f12837]) ).
fof(f29806,plain,
( $false
| ~ spl1526_620
| spl1526_644 ),
inference(forward_subsumption_resolution,[],[f29805,f29094]) ).
fof(f29807,plain,
( ~ spl1526_620
| spl1526_644 ),
inference(avatar_contradiction_clause,[],[f29806]) ).
fof(f31158,plain,
( v1_funct_1(sF1525)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(resolution,[],[f29481,f18514]) ).
fof(f31159,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(resolution,[],[f29481,f18512]) ).
fof(f31160,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(resolution,[],[f29481,f18513]) ).
fof(f31162,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(duplicate_literal_removal,[],[f31160]) ).
fof(f31163,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(duplicate_literal_removal,[],[f31159]) ).
fof(f31164,plain,
( v1_funct_1(sF1525)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(duplicate_literal_removal,[],[f31158]) ).
fof(f31165,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31162,f18790]) ).
fof(f31166,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31163,f18790]) ).
fof(f31167,plain,
( v1_funct_1(sF1525)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31164,f18790]) ).
fof(f31168,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31165,f18789]) ).
fof(f31169,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31166,f18789]) ).
fof(f31170,plain,
( v1_funct_1(sF1525)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31167,f18789]) ).
fof(f31171,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31168,f18794]) ).
fof(f31172,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31169,f18794]) ).
fof(f31173,plain,
( v1_funct_1(sF1525)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31170,f18794]) ).
fof(f31174,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31171,f18793]) ).
fof(f31175,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31172,f18793]) ).
fof(f31176,plain,
( v1_funct_1(sF1525)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31173,f18793]) ).
fof(f31177,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31174,f28493]) ).
fof(f31178,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),u2_cat_1(sK1513))
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31175,f28493]) ).
fof(f31179,plain,
( v1_funct_1(sF1525)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f31176,f28493]) ).
fof(f31180,plain,
( v1_funct_2(sF1525,u1_cat_1(sK1511),sF1522)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_demodulation,[],[f31177,f22447]) ).
fof(f31181,plain,
( m2_relset_1(sF1525,u1_cat_1(sK1511),sF1522)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_demodulation,[],[f31178,f22447]) ).
fof(f31182,plain,
( v1_funct_2(sF1525,sF1515,sF1522)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_demodulation,[],[f31180,f22433]) ).
fof(f31183,plain,
( m2_relset_1(sF1525,sF1515,sF1522)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_demodulation,[],[f31181,f22433]) ).
fof(f31189,definition,
( spl1526_903
<=> m1_relset_1(sF1525,sF1515,sF1522) ),
introduced(definition,[new_symbols(definition,[spl1526_903])],[avatar_definition]) ).
fof(f31190,plain,
( m1_relset_1(sF1525,sF1515,sF1522)
| ~ spl1526_903 ),
inference(avatar_component_clause,[],[f31189]) ).
fof(f31191,plain,
( ~ m1_relset_1(sF1525,sF1515,sF1522)
| spl1526_903 ),
inference(avatar_component_clause,[],[f31189]) ).
fof(f31196,plain,
( m1_relset_1(sF1525,sF1515,sF1522)
| ~ spl1526_620
| ~ spl1526_632 ),
inference(resolution,[],[f31183,f12837]) ).
fof(f31197,plain,
( $false
| ~ spl1526_620
| ~ spl1526_632
| spl1526_903 ),
inference(forward_subsumption_resolution,[],[f31196,f31191]) ).
fof(f31198,plain,
( ~ spl1526_620
| ~ spl1526_632
| spl1526_903 ),
inference(avatar_contradiction_clause,[],[f31197]) ).
fof(f31212,plain,
( v1_funct_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(resolution,[],[f29514,f18514]) ).
fof(f31213,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(resolution,[],[f29514,f18512]) ).
fof(f31214,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(resolution,[],[f29514,f18513]) ).
fof(f31216,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(duplicate_literal_removal,[],[f31214]) ).
fof(f31217,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(duplicate_literal_removal,[],[f31213]) ).
fof(f31218,plain,
( v1_funct_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(duplicate_literal_removal,[],[f31212]) ).
fof(f31219,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31216,f18790]) ).
fof(f31220,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31217,f18790]) ).
fof(f31221,plain,
( v1_funct_1(sF1521)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31218,f18790]) ).
fof(f31222,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31219,f18789]) ).
fof(f31223,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31220,f18789]) ).
fof(f31224,plain,
( v1_funct_1(sF1521)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31221,f18789]) ).
fof(f31225,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31222,f18792]) ).
fof(f31226,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31223,f18792]) ).
fof(f31227,plain,
( v1_funct_1(sF1521)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31224,f18792]) ).
fof(f31228,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31225,f18791]) ).
fof(f31229,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31226,f18791]) ).
fof(f31230,plain,
( v1_funct_1(sF1521)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31227,f18791]) ).
fof(f31231,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31228,f28502]) ).
fof(f31232,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),u2_cat_1(sK1512))
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31229,f28502]) ).
fof(f31233,plain,
( v1_funct_1(sF1521)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f31230,f28502]) ).
fof(f31234,plain,
( v1_funct_2(sF1521,u1_cat_1(sK1511),sF1516)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_demodulation,[],[f31231,f22435]) ).
fof(f31235,plain,
( m2_relset_1(sF1521,u1_cat_1(sK1511),sF1516)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_demodulation,[],[f31232,f22435]) ).
fof(f31236,plain,
( v1_funct_2(sF1521,sF1515,sF1516)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_demodulation,[],[f31234,f22433]) ).
fof(f31237,plain,
( m2_relset_1(sF1521,sF1515,sF1516)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_demodulation,[],[f31235,f22433]) ).
fof(f31243,definition,
( spl1526_905
<=> m1_relset_1(sF1521,sF1515,sF1516) ),
introduced(definition,[new_symbols(definition,[spl1526_905])],[avatar_definition]) ).
fof(f31244,plain,
( m1_relset_1(sF1521,sF1515,sF1516)
| ~ spl1526_905 ),
inference(avatar_component_clause,[],[f31243]) ).
fof(f31245,plain,
( ~ m1_relset_1(sF1521,sF1515,sF1516)
| spl1526_905 ),
inference(avatar_component_clause,[],[f31243]) ).
fof(f31250,plain,
( m1_relset_1(sF1521,sF1515,sF1516)
| ~ spl1526_622
| ~ spl1526_633 ),
inference(resolution,[],[f31237,f12837]) ).
fof(f31251,plain,
( $false
| ~ spl1526_622
| ~ spl1526_633
| spl1526_905 ),
inference(forward_subsumption_resolution,[],[f31250,f31245]) ).
fof(f31252,plain,
( ~ spl1526_622
| ~ spl1526_633
| spl1526_905 ),
inference(avatar_contradiction_clause,[],[f31251]) ).
fof(f31299,plain,
( v1_funct_1(sF1518)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29492,f22439]) ).
fof(f31300,plain,
( v1_funct_1(sF1524)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511) ),
inference(superposition,[],[f29492,f22451]) ).
fof(f31303,plain,
( ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511)
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31300,f29102]) ).
fof(f31304,plain,
( ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511)
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31299,f29000]) ).
fof(f31306,plain,
( ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511)
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31303,f18789]) ).
fof(f31307,plain,
( ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511)
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31304,f18789]) ).
fof(f31309,plain,
( ~ l1_cat_1(sK1513)
| ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511)
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31306,f18794]) ).
fof(f31310,plain,
( ~ l1_cat_1(sK1512)
| ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511)
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31307,f18792]) ).
fof(f31312,plain,
( ~ m2_cat_1(sF1523,sK1511,sK1513)
| ~ v2_cat_1(sK1511)
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31309,f18793]) ).
fof(f31313,plain,
( ~ m2_cat_1(sF1517,sK1511,sK1512)
| ~ v2_cat_1(sK1511)
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31310,f18791]) ).
fof(f31315,plain,
( ~ v2_cat_1(sK1511)
| ~ spl1526_620
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31312,f28493]) ).
fof(f31316,plain,
( ~ v2_cat_1(sK1511)
| ~ spl1526_622
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31313,f28502]) ).
fof(f31319,plain,
( $false
| ~ spl1526_620
| spl1526_646 ),
inference(forward_subsumption_resolution,[],[f31315,f18790]) ).
fof(f31320,plain,
( ~ spl1526_620
| spl1526_646 ),
inference(avatar_contradiction_clause,[],[f31319]) ).
fof(f31321,plain,
( $false
| ~ spl1526_622
| spl1526_638 ),
inference(forward_subsumption_resolution,[],[f31316,f18790]) ).
fof(f31322,plain,
( ~ spl1526_622
| spl1526_638 ),
inference(avatar_contradiction_clause,[],[f31321]) ).
fof(f35028,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(resolution,[],[f28403,f28428]) ).
fof(f35029,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(resolution,[],[f28403,f28429]) ).
fof(f35032,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(duplicate_literal_removal,[],[f35029]) ).
fof(f35033,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1519)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(duplicate_literal_removal,[],[f35028]) ).
fof(f35034,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35032,f22455]) ).
fof(f35035,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35033,f22455]) ).
fof(f35036,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35034,f18790]) ).
fof(f35037,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511)
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35035,f18790]) ).
fof(f35038,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35036,f18789]) ).
fof(f35039,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1514,sF1520) = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35037,f18789]) ).
fof(f35040,plain,
( sF1525 = k6_isocat_1(sK1511,sF1519,sK1513,sK1514,sK1514,sF1520,k9_isocat_2(sK1512,sK1513))
| ~ spl1526_616 ),
inference(forward_demodulation,[],[f35038,f22453]) ).
fof(f35041,plain,
( sF1521 = k6_isocat_1(sK1511,sF1519,sK1512,sK1514,sK1514,sF1520,k8_isocat_2(sK1512,sK1513))
| ~ spl1526_616 ),
inference(forward_demodulation,[],[f35039,f22445]) ).
fof(f35042,plain,
( r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1525,sF1524)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(superposition,[],[f29082,f35040]) ).
fof(f35069,plain,
( r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1524,sF1525)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1522)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1522)
| ~ v1_funct_1(sF1525)
| ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(resolution,[],[f35042,f18525]) ).
fof(f35070,plain,
( r4_nattra_1(sF1515,sF1522,sF1515,sF1522,sF1524,sF1525)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1522)
| ~ v1_funct_1(sF1525)
| ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(duplicate_literal_removal,[],[f35069]) ).
fof(f35072,plain,
( v1_xboole_0(sF1515)
| v1_xboole_0(sF1522)
| ~ v1_funct_1(sF1525)
| ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35070,f22488]) ).
fof(f35074,plain,
( v1_xboole_0(sF1522)
| ~ v1_funct_1(sF1525)
| ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35072,f26828]) ).
fof(f35076,plain,
( ~ v1_funct_1(sF1525)
| ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35074,f26842]) ).
fof(f35078,plain,
( ~ v1_funct_2(sF1525,sF1515,sF1522)
| ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f35076,f31179]) ).
fof(f35080,plain,
( ~ m1_relset_1(sF1525,sF1515,sF1522)
| ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632 ),
inference(forward_subsumption_resolution,[],[f35078,f31182]) ).
fof(f35082,plain,
( ~ v1_funct_1(sF1524)
| ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_903 ),
inference(forward_subsumption_resolution,[],[f35080,f31190]) ).
fof(f35084,plain,
( ~ v1_funct_2(sF1524,sF1515,sF1522)
| ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_646
| ~ spl1526_903 ),
inference(forward_subsumption_resolution,[],[f35082,f29101]) ).
fof(f35086,plain,
( ~ m1_relset_1(sF1524,sF1515,sF1522)
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_645
| ~ spl1526_646
| ~ spl1526_903 ),
inference(forward_subsumption_resolution,[],[f35084,f29097]) ).
fof(f35088,plain,
( $false
| spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_644
| ~ spl1526_645
| ~ spl1526_646
| ~ spl1526_903 ),
inference(forward_subsumption_resolution,[],[f35086,f29093]) ).
fof(f35089,plain,
( spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_644
| ~ spl1526_645
| ~ spl1526_646
| ~ spl1526_903 ),
inference(avatar_contradiction_clause,[],[f35088]) ).
fof(f35106,plain,
( r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1521,sF1518)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(superposition,[],[f28980,f35041]) ).
fof(f35133,plain,
( r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1518,sF1521)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1516)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1516)
| ~ v1_funct_1(sF1521)
| ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(resolution,[],[f35106,f18525]) ).
fof(f35134,plain,
( r4_nattra_1(sF1515,sF1516,sF1515,sF1516,sF1518,sF1521)
| v1_xboole_0(sF1515)
| v1_xboole_0(sF1516)
| ~ v1_funct_1(sF1521)
| ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(duplicate_literal_removal,[],[f35133]) ).
fof(f35136,plain,
( v1_xboole_0(sF1515)
| v1_xboole_0(sF1516)
| ~ v1_funct_1(sF1521)
| ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35134,f22492]) ).
fof(f35138,plain,
( v1_xboole_0(sF1516)
| ~ v1_funct_1(sF1521)
| ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35136,f26828]) ).
fof(f35140,plain,
( ~ v1_funct_1(sF1521)
| ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616 ),
inference(forward_subsumption_resolution,[],[f35138,f26841]) ).
fof(f35142,plain,
( ~ v1_funct_2(sF1521,sF1515,sF1516)
| ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f35140,f31233]) ).
fof(f35144,plain,
( ~ m1_relset_1(sF1521,sF1515,sF1516)
| ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633 ),
inference(forward_subsumption_resolution,[],[f35142,f31236]) ).
fof(f35146,plain,
( ~ v1_funct_1(sF1518)
| ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_905 ),
inference(forward_subsumption_resolution,[],[f35144,f31244]) ).
fof(f35148,plain,
( ~ v1_funct_2(sF1518,sF1515,sF1516)
| ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_638
| ~ spl1526_905 ),
inference(forward_subsumption_resolution,[],[f35146,f28999]) ).
fof(f35150,plain,
( ~ m1_relset_1(sF1518,sF1515,sF1516)
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_637
| ~ spl1526_638
| ~ spl1526_905 ),
inference(forward_subsumption_resolution,[],[f35148,f28995]) ).
fof(f35152,plain,
( $false
| spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_636
| ~ spl1526_637
| ~ spl1526_638
| ~ spl1526_905 ),
inference(forward_subsumption_resolution,[],[f35150,f28991]) ).
fof(f35153,plain,
( spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_636
| ~ spl1526_637
| ~ spl1526_638
| ~ spl1526_905 ),
inference(avatar_contradiction_clause,[],[f35152]) ).
cnf(s1,plain,
( ~ spl1526_1
| ~ spl1526_2 ),
inference(sat_conversion,[],[f22493]) ).
cnf(s537,plain,
( ~ spl1526_600
| ~ spl1526_601
| spl1526_616 ),
inference(sat_conversion,[],[f28404]) ).
cnf(s543,plain,
spl1526_600,
inference(sat_conversion,[],[f28509]) ).
cnf(s544,plain,
spl1526_601,
inference(sat_conversion,[],[f28510]) ).
cnf(s553,plain,
spl1526_620,
inference(sat_conversion,[],[f28613]) ).
cnf(s554,plain,
spl1526_622,
inference(sat_conversion,[],[f28614]) ).
cnf(s555,plain,
( ~ spl1526_616
| spl1526_632 ),
inference(sat_conversion,[],[f28645]) ).
cnf(s556,plain,
( ~ spl1526_616
| spl1526_633 ),
inference(sat_conversion,[],[f28650]) ).
cnf(s565,plain,
( ~ spl1526_620
| spl1526_645 ),
inference(sat_conversion,[],[f29551]) ).
cnf(s566,plain,
( ~ spl1526_622
| spl1526_637 ),
inference(sat_conversion,[],[f29552]) ).
cnf(s603,plain,
( ~ spl1526_622
| spl1526_636 ),
inference(sat_conversion,[],[f29804]) ).
cnf(s604,plain,
( ~ spl1526_620
| spl1526_644 ),
inference(sat_conversion,[],[f29807]) ).
cnf(s804,plain,
( ~ spl1526_620
| ~ spl1526_632
| spl1526_903 ),
inference(sat_conversion,[],[f31198]) ).
cnf(s806,plain,
( ~ spl1526_622
| ~ spl1526_633
| spl1526_905 ),
inference(sat_conversion,[],[f31252]) ).
cnf(s812,plain,
( ~ spl1526_620
| spl1526_646 ),
inference(sat_conversion,[],[f31320]) ).
cnf(s813,plain,
( ~ spl1526_622
| spl1526_638 ),
inference(sat_conversion,[],[f31322]) ).
cnf(s958,plain,
( spl1526_1
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_620
| ~ spl1526_632
| ~ spl1526_644
| ~ spl1526_645
| ~ spl1526_646
| ~ spl1526_903 ),
inference(sat_conversion,[],[f35089]) ).
cnf(s959,plain,
( spl1526_2
| ~ spl1526_600
| ~ spl1526_601
| ~ spl1526_616
| ~ spl1526_622
| ~ spl1526_633
| ~ spl1526_636
| ~ spl1526_637
| ~ spl1526_638
| ~ spl1526_905 ),
inference(sat_conversion,[],[f35153]) ).
cnf(s1181,plain,
spl1526_638,
inference(rat,[],[s813,s554]) ).
cnf(s1182,plain,
spl1526_636,
inference(rat,[],[s603,s554]) ).
cnf(s1183,plain,
spl1526_637,
inference(rat,[],[s566,s554]) ).
cnf(s1184,plain,
spl1526_646,
inference(rat,[],[s812,s553]) ).
cnf(s1185,plain,
spl1526_644,
inference(rat,[],[s604,s553]) ).
cnf(s1186,plain,
spl1526_645,
inference(rat,[],[s565,s553]) ).
cnf(s1219,plain,
spl1526_616,
inference(rat,[],[s537,s544,s543]) ).
cnf(s1220,plain,
spl1526_633,
inference(rat,[],[s556,s1219]) ).
cnf(s1221,plain,
spl1526_632,
inference(rat,[],[s555,s1219]) ).
cnf(s1222,plain,
spl1526_905,
inference(rat,[],[s806,s554,s1220]) ).
cnf(s1223,plain,
spl1526_903,
inference(rat,[],[s804,s553,s1221]) ).
cnf(s1225,plain,
spl1526_2,
inference(rat,[],[s959,s1219,s1181,s1183,s1182,s1220,s554,s543,s544,s1222]) ).
cnf(s1227,plain,
spl1526_1,
inference(rat,[],[s958,s1219,s1184,s1186,s1185,s1221,s553,s543,s544,s1223]) ).
cnf(s1256,plain,
$false,
inference(rat,[],[s1,s1225,s1227]) ).
fof(f35154,plain,
$false,
inference(avatar_sat_refutation,[],[s1256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT027+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n010.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 21:21:13 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running first-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.87/2.87 % (2355272)Detected formulas, will run a generic FOF schedule.
% 13.87/2.87 % (2355634)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=804688983:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 13.87/2.87 % (2355631)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2049244187:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 13.87/2.87 % (2355629)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=3224204056:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 13.87/2.87 % (2355632)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3416976596:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 13.87/2.87 % (2355627)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=2383704916:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 13.87/2.87 % (2355625)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=844782000:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 13.87/2.87 % (2355634)Instruction limit reached!
% 13.87/2.87 % (2355634)------------------------------
% 13.87/2.87 % (2355634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.87 % (2355634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.87 % (2355634)CaDiCaL version: 2.1.3
% 13.87/2.87 % (2355634)Termination reason: Instruction limit
% 13.87/2.87 % (2355634)Termination phase: Preprocessing 3
% 13.87/2.87 % (2355634)Time elapsed: 0.052 s
% 13.87/2.87 % (2355634)Peak memory usage: 94 MB
% 13.87/2.87 % (2355634)Instructions burned: 140 (million)
% 13.87/2.87 % (2355636)dis-21_1_sil=8000:lcm=predicate:random_seed=3888664316:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 13.87/2.87 % (2355631)Refutation not found, incomplete strategy
% 13.87/2.87 % (2355631)------------------------------
% 13.87/2.87 % (2355631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.87 % (2355631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.87 % (2355631)CaDiCaL version: 2.1.3
% 13.87/2.87 % (2355631)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.87 % (2355631)Time elapsed: 0.024 s
% 13.87/2.87 % (2355631)Peak memory usage: 93 MB
% 13.87/2.87 % (2355631)Instructions burned: 28 (million)
% 13.87/2.87 % (2355632)Instruction limit reached!
% 13.87/2.87 % (2355632)------------------------------
% 13.87/2.87 % (2355632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.87 % (2355632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.87 % (2355632)CaDiCaL version: 2.1.3
% 13.87/2.87 % (2355632)Termination reason: Instruction limit
% 13.87/2.87 % (2355632)Termination phase: Saturation
% 13.87/2.87 % (2355632)Time elapsed: 0.073 s
% 13.87/2.87 % (2355632)Peak memory usage: 95 MB
% 13.87/2.87 % (2355632)Instructions burned: 119 (million)
% 13.87/2.87 % (2355636)Instruction limit reached!
% 13.87/2.87 % (2355636)------------------------------
% 13.87/2.87 % (2355636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.87 % (2355636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.87 % (2355636)CaDiCaL version: 2.1.3
% 13.87/2.87 % (2355636)Termination reason: Instruction limit
% 13.87/2.87 % (2355636)Termination phase: Preprocessing 3
% 13.87/2.87 % (2355636)Time elapsed: 0.093 s
% 13.87/2.87 % (2355636)Peak memory usage: 95 MB
% 13.87/2.87 % (2355636)Instructions burned: 130 (million)
% 13.87/2.87 % (2355728)lrs+10_1_sil=8000:sp=occurrence:random_seed=3004939176:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 13.87/2.87 % (2355761)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2143180123:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.87/2.87 % (2355728)Instruction limit reached!
% 13.87/2.87 % (2355728)------------------------------
% 13.87/2.87 % (2355728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.87 % (2355728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.87 % (2355728)CaDiCaL version: 2.1.3
% 13.87/2.87 % (2355728)Termination reason: Instruction limit
% 16.90/3.63 % (2355728)Termination phase: Saturation
% 16.90/3.63 % (2355728)Time elapsed: 0.104 s
% 16.90/3.63 % (2355728)Peak memory usage: 97 MB
% 16.90/3.63 % (2355728)Instructions burned: 287 (million)
% 16.90/3.63 % (2355631)------------------------------
% 16.90/3.63 % (2355631)------------------------------
% 16.90/3.63 % (2355786)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2247684650:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 16.90/3.63 % (2355761)Instruction limit reached!
% 16.90/3.63 % (2355761)------------------------------
% 16.90/3.63 % (2355761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355761)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355761)Termination reason: Instruction limit
% 16.90/3.63 % (2355761)Termination phase: Saturation
% 16.90/3.63 % (2355761)Time elapsed: 0.087 s
% 16.90/3.63 % (2355761)Peak memory usage: 95 MB
% 16.90/3.63 % (2355761)Instructions burned: 158 (million)
% 16.90/3.63 % (2355851)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=2838902241:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 16.90/3.63 % (2355851)Instruction limit reached!
% 16.90/3.63 % (2355851)------------------------------
% 16.90/3.63 % (2355851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355851)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355851)Termination reason: Instruction limit
% 16.90/3.63 % (2355851)Termination phase: Property scanning
% 16.90/3.63 % (2355851)Time elapsed: 0.082 s
% 16.90/3.63 % (2355851)Peak memory usage: 99 MB
% 16.90/3.63 % (2355851)Instructions burned: 251 (million)
% 16.90/3.63 % (2355871)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3805432655:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 16.90/3.63 % (2355894)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2909876548:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 16.90/3.63 % (2355786)Instruction limit reached!
% 16.90/3.63 % (2355786)------------------------------
% 16.90/3.63 % (2355786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355786)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355786)Termination reason: Instruction limit
% 16.90/3.63 % (2355786)Termination phase: Saturation
% 16.90/3.63 % (2355786)Time elapsed: 0.216 s
% 16.90/3.63 % (2355786)Peak memory usage: 97 MB
% 16.90/3.63 % (2355786)Instructions burned: 326 (million)
% 16.90/3.63 % (2355958)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=7769571:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 16.90/3.63 % (2355958)Instruction limit reached!
% 16.90/3.63 % (2355958)------------------------------
% 16.90/3.63 % (2355958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355958)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355958)Termination reason: Instruction limit
% 16.90/3.63 % (2355958)Termination phase: Property scanning
% 16.90/3.63 % (2355958)Time elapsed: 0.035 s
% 16.90/3.63 % (2355958)Peak memory usage: 93 MB
% 16.90/3.63 % (2355958)Instructions burned: 113 (million)
% 16.90/3.63 % (2355871)Instruction limit reached!
% 16.90/3.63 % (2355871)------------------------------
% 16.90/3.63 % (2355871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355871)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355871)Termination reason: Instruction limit
% 16.90/3.63 % (2355871)Termination phase: Saturation
% 16.90/3.63 % (2355871)Time elapsed: 0.172 s
% 16.90/3.63 % (2355871)Peak memory usage: 97 MB
% 16.90/3.63 % (2355871)Instructions burned: 295 (million)
% 16.90/3.63 % (2355997)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=190003466:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 16.90/3.63 % (2356038)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4259210770:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 16.90/3.63 % (2356038)Instruction limit reached!
% 16.90/3.63 % (2356038)------------------------------
% 16.90/3.63 % (2356038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356038)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356038)Termination reason: Instruction limit
% 16.90/3.63 % (2356038)Termination phase: SInE selection
% 16.90/3.63 % (2356038)Time elapsed: 0.028 s
% 16.90/3.63 % (2356038)Peak memory usage: 90 MB
% 16.90/3.63 % (2356038)Instructions burned: 115 (million)
% 16.90/3.63 % (2355997)Instruction limit reached!
% 16.90/3.63 % (2355997)------------------------------
% 16.90/3.63 % (2355997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355997)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355997)Termination reason: Instruction limit
% 16.90/3.63 % (2355997)Termination phase: Preprocessing 3
% 16.90/3.63 % (2355997)Time elapsed: 0.086 s
% 16.90/3.63 % (2355997)Peak memory usage: 97 MB
% 16.90/3.63 % (2355997)Instructions burned: 128 (million)
% 16.90/3.63 % (2356054)lrs+10_1_sil=8000:sp=occurrence:random_seed=3640487657:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 16.90/3.63 % (2356114)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2714463216:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 16.90/3.63 % (2356125)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3134753010:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 16.90/3.63 % (2356114)Instruction limit reached!
% 16.90/3.63 % (2356114)------------------------------
% 16.90/3.63 % (2356114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356114)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356114)Termination reason: Instruction limit
% 16.90/3.63 % (2356114)Termination phase: Saturation
% 16.90/3.63 % (2356114)Time elapsed: 0.198 s
% 16.90/3.63 % (2356114)Peak memory usage: 98 MB
% 16.90/3.63 % (2356114)Instructions burned: 438 (million)
% 16.90/3.63 % (2356278)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3732357596:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 16.90/3.63 % (2356278)Instruction limit reached!
% 16.90/3.63 % (2356278)------------------------------
% 16.90/3.63 % (2356278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356278)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356278)Termination reason: Instruction limit
% 16.90/3.63 % (2356278)Termination phase: Saturation
% 16.90/3.63 % (2356278)Time elapsed: 0.080 s
% 16.90/3.63 % (2356278)Peak memory usage: 96 MB
% 16.90/3.63 % (2356278)Instructions burned: 135 (million)
% 16.90/3.63 % (2356054)Instruction limit reached!
% 16.90/3.63 % (2356054)------------------------------
% 16.90/3.63 % (2356054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356054)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356054)Termination reason: Instruction limit
% 16.90/3.63 % (2356054)Termination phase: Saturation
% 16.90/3.63 % (2356054)Time elapsed: 0.542 s
% 16.90/3.63 % (2356054)Peak memory usage: 108 MB
% 16.90/3.63 % (2356054)Instructions burned: 907 (million)
% 16.90/3.63 % (2356403)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1084291221:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 16.90/3.63 % (2356424)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2411624129:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 16.90/3.63 % (2356403)Instruction limit reached!
% 16.90/3.63 % (2356403)------------------------------
% 16.90/3.63 % (2356403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356403)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356403)Termination reason: Instruction limit
% 16.90/3.63 % (2356403)Termination phase: Saturation
% 16.90/3.63 % (2356403)Time elapsed: 0.294 s
% 16.90/3.63 % (2356403)Peak memory usage: 104 MB
% 16.90/3.63 % (2356403)Instructions burned: 592 (million)
% 16.90/3.63 % (2356637)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=2133636107:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 16.90/3.63 % (2355894)Instruction limit reached!
% 16.90/3.63 % (2355894)------------------------------
% 16.90/3.63 % (2355894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2355894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2355894)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2355894)Termination reason: Instruction limit
% 16.90/3.63 % (2355894)Termination phase: Saturation
% 16.90/3.63 % (2355894)Time elapsed: 1.443 s
% 16.90/3.63 % (2355894)Peak memory usage: 194 MB
% 16.90/3.63 % (2355894)Instructions burned: 2350 (million)
% 16.90/3.63 % (2356637)Instruction limit reached!
% 16.90/3.63 % (2356637)------------------------------
% 16.90/3.63 % (2356637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356637)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356637)Termination reason: Instruction limit
% 16.90/3.63 % (2356637)Termination phase: Preprocessing 3
% 16.90/3.63 % (2356637)Time elapsed: 0.083 s
% 16.90/3.63 % (2356637)Peak memory usage: 92 MB
% 16.90/3.63 % (2356637)Instructions burned: 125 (million)
% 16.90/3.63 % (2356746)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3785341008:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 16.90/3.63 % (2356770)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2545498979:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 16.90/3.63 % (2356746)Instruction limit reached!
% 16.90/3.63 % (2356746)------------------------------
% 16.90/3.63 % (2356746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356746)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356746)Termination reason: Instruction limit
% 16.90/3.63 % (2356746)Termination phase: Preprocessing 1
% 16.90/3.63 % (2356746)Time elapsed: 0.067 s
% 16.90/3.63 % (2356746)Peak memory usage: 90 MB
% 16.90/3.63 % (2356746)Instructions burned: 135 (million)
% 16.90/3.63 % (2356770)Instruction limit reached!
% 16.90/3.63 % (2356770)------------------------------
% 16.90/3.63 % (2356770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356770)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356770)Termination reason: Instruction limit
% 16.90/3.63 % (2356770)Termination phase: Saturation
% 16.90/3.63 % (2356770)Time elapsed: 0.076 s
% 16.90/3.63 % (2356770)Peak memory usage: 95 MB
% 16.90/3.63 % (2356770)Instructions burned: 142 (million)
% 16.90/3.63 % (2356841)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4175383110:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 16.90/3.63 % (2356841)Refutation not found, incomplete strategy
% 16.90/3.63 % (2356841)------------------------------
% 16.90/3.63 % (2356841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.90/3.63 % (2356841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.63 % (2356841)CaDiCaL version: 2.1.3
% 16.90/3.63 % (2356841)Termination reason: Refutation not found, incomplete strategy
% 16.90/3.63 % (2356841)Time elapsed: 0.026 s
% 16.90/3.63 % (2356841)Peak memory usage: 93 MB
% 16.90/3.63 % (2356841)Instructions burned: 35 (million)
% 16.90/3.63 % (2356842)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=2512070759:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 16.90/3.63 % (2355625)First to succeed.
% 16.90/3.63 % (2355625)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2355272"
% 16.90/3.63 % (2356841)------------------------------
% 16.90/3.63 % (2356841)------------------------------
% 16.90/3.63 % (2355625)Refutation found. Thanks to Tanya!
% 16.90/3.63 % SZS status Theorem for theBenchmark
% 16.90/3.63 % SZS output start Proof for theBenchmark
% See solution above
% 20.47/3.83 % (2355625)------------------------------
% 20.47/3.83 % (2355625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.47/3.83 % (2355625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.47/3.83 % (2355625)CaDiCaL version: 2.1.3
% 20.47/3.83 % (2355625)Termination reason: Refutation
% 20.47/3.83 % (2355625)Time elapsed: 2.443 s
% 20.47/3.83 % (2355625)Peak memory usage: 222 MB
% 20.47/3.83 % (2355625)Instructions burned: 6422 (million)
% 20.47/3.83 % (2355625)------------------------------
% 20.47/3.83 % (2355625)------------------------------
% 20.47/3.83 % (2355272)Success in time 2.969 s
% 20.47/3.83 % Vampire exiting
%------------------------------------------------------------------------------