%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT028+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 : n002.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:44 AM UTC 2026
% Result : Theorem 27.60s 4.88s
% Output : Refutation 28.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 35
% Syntax : Number of formulae : 273 ( 92 unt; 25 def)
% Number of atoms : 1097 ( 134 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1512 ( 688 ~; 681 |; 85 &)
% ( 6 <=>; 52 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 7 prp; 0-6 aty)
% Number of functors : 39 ( 39 usr; 27 con; 0-7 aty)
% Number of variables : 288 ( 0 sgn 272 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
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(f3901,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( 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)
& m2_cat_1(X4,X0,X1)
& m2_nattra_1(X5,X0,X1,X2,X3)
& m2_nattra_1(X6,X0,X1,X3,X4) )
=> m2_nattra_1(k8_nattra_1(X0,X1,X2,X3,X4,X5,X6),X0,X1,X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_nattra_1) ).
fof(f3948,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,X1,X2)
=> ! [X4] :
( m2_cat_1(X4,X1,X2)
=> ! [X5] :
( m2_cat_1(X5,X1,X2)
=> ! [X6] :
( m2_cat_1(X6,X2,X0)
=> ! [X7] :
( m2_nattra_1(X7,X1,X2,X3,X4)
=> ! [X8] :
( m2_nattra_1(X8,X1,X2,X4,X5)
=> ( ( r2_nattra_1(X1,X2,X3,X4)
& r2_nattra_1(X1,X2,X4,X5) )
=> r4_nattra_1(u1_cat_1(X1),u2_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),k6_isocat_1(X1,X2,X0,X3,X5,k8_nattra_1(X1,X2,X3,X4,X5,X7,X8),X6),k8_nattra_1(X1,X0,k2_isocat_1(X1,X2,X0,X3,X6),k2_isocat_1(X1,X2,X0,X4,X6),k2_isocat_1(X1,X2,X0,X5,X6),k6_isocat_1(X1,X2,X0,X3,X4,X7,X6),k6_isocat_1(X1,X2,X0,X4,X5,X8,X6))) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_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(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(f4067,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))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_cat_1(X5,X0,k11_cat_2(X1,X2))
=> ( ( r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& r2_nattra_1(X0,k11_cat_2(X1,X2),X4,X5) )
=> ! [X6] :
( m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
=> ! [X7] :
( m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
=> ( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4),k11_isocat_2(X0,X1,X2,X5),k13_isocat_2(X0,X1,X2,X3,X4,X6),k13_isocat_2(X0,X1,X2,X4,X5,X7)))
& r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k14_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4),k12_isocat_2(X0,X1,X2,X5),k14_isocat_2(X0,X1,X2,X3,X4,X6),k14_isocat_2(X0,X1,X2,X4,X5,X7))) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_isocat_2) ).
fof(f4068,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))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_cat_1(X5,X0,k11_cat_2(X1,X2))
=> ( ( r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& r2_nattra_1(X0,k11_cat_2(X1,X2),X4,X5) )
=> ! [X6] :
( m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
=> ! [X7] :
( m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
=> ( r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4),k11_isocat_2(X0,X1,X2,X5),k13_isocat_2(X0,X1,X2,X3,X4,X6),k13_isocat_2(X0,X1,X2,X4,X5,X7)))
& r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k14_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4),k12_isocat_2(X0,X1,X2,X5),k14_isocat_2(X0,X1,X2,X3,X4,X6),k14_isocat_2(X0,X1,X2,X4,X5,X7))) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f4067]) ).
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(ennf_transformation,[],[f3782]) ).
fof(f8262,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,[],[f8261]) ).
fof(f8475,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( m2_nattra_1(k8_nattra_1(X0,X1,X2,X3,X4,X5,X6),X0,X1,X2,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)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_nattra_1(X5,X0,X1,X2,X3)
| ~ m2_nattra_1(X6,X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f3901]) ).
fof(f8476,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( m2_nattra_1(k8_nattra_1(X0,X1,X2,X3,X4,X5,X6),X0,X1,X2,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)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_nattra_1(X5,X0,X1,X2,X3)
| ~ m2_nattra_1(X6,X0,X1,X3,X4) ),
inference(flattening,[],[f8475]) ).
fof(f8561,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( r4_nattra_1(u1_cat_1(X1),u2_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),k6_isocat_1(X1,X2,X0,X3,X5,k8_nattra_1(X1,X2,X3,X4,X5,X7,X8),X6),k8_nattra_1(X1,X0,k2_isocat_1(X1,X2,X0,X3,X6),k2_isocat_1(X1,X2,X0,X4,X6),k2_isocat_1(X1,X2,X0,X5,X6),k6_isocat_1(X1,X2,X0,X3,X4,X7,X6),k6_isocat_1(X1,X2,X0,X4,X5,X8,X6)))
| ~ r2_nattra_1(X1,X2,X3,X4)
| ~ r2_nattra_1(X1,X2,X4,X5)
| ~ m2_nattra_1(X8,X1,X2,X4,X5) )
| ~ m2_nattra_1(X7,X1,X2,X3,X4) )
| ~ m2_cat_1(X6,X2,X0) )
| ~ m2_cat_1(X5,X1,X2) )
| ~ m2_cat_1(X4,X1,X2) )
| ~ m2_cat_1(X3,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,[],[f3948]) ).
fof(f8562,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( r4_nattra_1(u1_cat_1(X1),u2_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),k6_isocat_1(X1,X2,X0,X3,X5,k8_nattra_1(X1,X2,X3,X4,X5,X7,X8),X6),k8_nattra_1(X1,X0,k2_isocat_1(X1,X2,X0,X3,X6),k2_isocat_1(X1,X2,X0,X4,X6),k2_isocat_1(X1,X2,X0,X5,X6),k6_isocat_1(X1,X2,X0,X3,X4,X7,X6),k6_isocat_1(X1,X2,X0,X4,X5,X8,X6)))
| ~ r2_nattra_1(X1,X2,X3,X4)
| ~ r2_nattra_1(X1,X2,X4,X5)
| ~ m2_nattra_1(X8,X1,X2,X4,X5) )
| ~ m2_nattra_1(X7,X1,X2,X3,X4) )
| ~ m2_cat_1(X6,X2,X0) )
| ~ m2_cat_1(X5,X1,X2) )
| ~ m2_cat_1(X4,X1,X2) )
| ~ m2_cat_1(X3,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,[],[f8561]) ).
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(ennf_transformation,[],[f4002]) ).
fof(f8666,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,[],[f8665]) ).
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(ennf_transformation,[],[f4004]) ).
fof(f8670,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,[],[f8669]) ).
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(ennf_transformation,[],[f4058]) ).
fof(f8770,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,[],[f8769]) ).
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(ennf_transformation,[],[f4059]) ).
fof(f8772,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,[],[f8771]) ).
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(ennf_transformation,[],[f4062]) ).
fof(f8778,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,[],[f8777]) ).
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(ennf_transformation,[],[f4063]) ).
fof(f8780,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,[],[f8779]) ).
fof(f8787,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ( ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4),k11_isocat_2(X0,X1,X2,X5),k13_isocat_2(X0,X1,X2,X3,X4,X6),k13_isocat_2(X0,X1,X2,X4,X5,X7)))
| ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k14_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4),k12_isocat_2(X0,X1,X2,X5),k14_isocat_2(X0,X1,X2,X3,X4,X6),k14_isocat_2(X0,X1,X2,X4,X5,X7))) )
& m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5) )
& m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4) )
& r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& r2_nattra_1(X0,k11_cat_2(X1,X2),X4,X5)
& m2_cat_1(X5,X0,k11_cat_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(ennf_transformation,[],[f4068]) ).
fof(f8788,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ( ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u2_cat_1(X1),k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4),k11_isocat_2(X0,X1,X2,X5),k13_isocat_2(X0,X1,X2,X3,X4,X6),k13_isocat_2(X0,X1,X2,X4,X5,X7)))
| ~ r4_nattra_1(u1_cat_1(X0),u2_cat_1(X2),u1_cat_1(X0),u2_cat_1(X2),k14_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)),k8_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4),k12_isocat_2(X0,X1,X2,X5),k14_isocat_2(X0,X1,X2,X3,X4,X6),k14_isocat_2(X0,X1,X2,X4,X5,X7))) )
& m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5) )
& m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4) )
& r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& r2_nattra_1(X0,k11_cat_2(X1,X2),X4,X5)
& m2_cat_1(X5,X0,k11_cat_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(flattening,[],[f8787]) ).
fof(f11186,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,k8_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515,sK1516,sK1517,sK1518)),k8_nattra_1(sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1515),k11_isocat_2(sK1511,sK1512,sK1513,sK1516),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518)))
| ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,k8_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515,sK1516,sK1517,sK1518)),k8_nattra_1(sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1515),k12_isocat_2(sK1511,sK1512,sK1513,sK1516),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518))) )
& m2_nattra_1(sK1518,sK1511,k11_cat_2(sK1512,sK1513),sK1515,sK1516)
& m2_nattra_1(sK1517,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515)
& r2_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515)
& r2_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1515,sK1516)
& m2_cat_1(sK1516,sK1511,k11_cat_2(sK1512,sK1513))
& m2_cat_1(sK1515,sK1511,k11_cat_2(sK1512,sK1513))
& 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,sK1515,sK1516,sK1517,sK1518]),skolemize(X0,sK1511),skolemize(X1,sK1512),skolemize(X2,sK1513),skolemize(X3,sK1514),skolemize(X4,sK1515),skolemize(X5,sK1516),skolemize(X6,sK1517),skolemize(X7,sK1518)],[f8788]) ).
fof(f18272,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,[],[f8262]) ).
fof(f18273,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,[],[f8262]) ).
fof(f18545,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( m2_nattra_1(k8_nattra_1(X0,X1,X2,X3,X4,X5,X6),X0,X1,X2,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)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_nattra_1(X5,X0,X1,X2,X3)
| ~ m2_nattra_1(X6,X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f8476]) ).
fof(f18622,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( r4_nattra_1(u1_cat_1(X1),u2_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),k6_isocat_1(X1,X2,X0,X3,X5,k8_nattra_1(X1,X2,X3,X4,X5,X7,X8),X6),k8_nattra_1(X1,X0,k2_isocat_1(X1,X2,X0,X3,X6),k2_isocat_1(X1,X2,X0,X4,X6),k2_isocat_1(X1,X2,X0,X5,X6),k6_isocat_1(X1,X2,X0,X3,X4,X7,X6),k6_isocat_1(X1,X2,X0,X4,X5,X8,X6)))
| ~ r2_nattra_1(X1,X2,X3,X4)
| ~ r2_nattra_1(X1,X2,X4,X5)
| ~ m2_nattra_1(X8,X1,X2,X4,X5)
| ~ m2_nattra_1(X7,X1,X2,X3,X4)
| ~ m2_cat_1(X6,X2,X0)
| ~ m2_cat_1(X5,X1,X2)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,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,[],[f8562]) ).
fof(f18692,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,[],[f8666]) ).
fof(f18694,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,[],[f8670]) ).
fof(f18782,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,[],[f8770]) ).
fof(f18783,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,[],[f8772]) ).
fof(f18787,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,[],[f8778]) ).
fof(f18788,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,[],[f8780]) ).
fof(f18794,plain,
l1_cat_1(sK1511),
inference(cnf_transformation,[],[f11186]) ).
fof(f18795,plain,
v2_cat_1(sK1511),
inference(cnf_transformation,[],[f11186]) ).
fof(f18796,plain,
l1_cat_1(sK1512),
inference(cnf_transformation,[],[f11186]) ).
fof(f18797,plain,
v2_cat_1(sK1512),
inference(cnf_transformation,[],[f11186]) ).
fof(f18798,plain,
l1_cat_1(sK1513),
inference(cnf_transformation,[],[f11186]) ).
fof(f18799,plain,
v2_cat_1(sK1513),
inference(cnf_transformation,[],[f11186]) ).
fof(f18800,plain,
m2_cat_1(sK1514,sK1511,k11_cat_2(sK1512,sK1513)),
inference(cnf_transformation,[],[f11186]) ).
fof(f18801,plain,
m2_cat_1(sK1515,sK1511,k11_cat_2(sK1512,sK1513)),
inference(cnf_transformation,[],[f11186]) ).
fof(f18802,plain,
m2_cat_1(sK1516,sK1511,k11_cat_2(sK1512,sK1513)),
inference(cnf_transformation,[],[f11186]) ).
fof(f18803,plain,
r2_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1515,sK1516),
inference(cnf_transformation,[],[f11186]) ).
fof(f18804,plain,
r2_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515),
inference(cnf_transformation,[],[f11186]) ).
fof(f18805,plain,
m2_nattra_1(sK1517,sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515),
inference(cnf_transformation,[],[f11186]) ).
fof(f18806,plain,
m2_nattra_1(sK1518,sK1511,k11_cat_2(sK1512,sK1513),sK1515,sK1516),
inference(cnf_transformation,[],[f11186]) ).
fof(f18807,plain,
( ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1512),u1_cat_1(sK1511),u2_cat_1(sK1512),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,k8_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515,sK1516,sK1517,sK1518)),k8_nattra_1(sK1511,sK1512,k11_isocat_2(sK1511,sK1512,sK1513,sK1514),k11_isocat_2(sK1511,sK1512,sK1513,sK1515),k11_isocat_2(sK1511,sK1512,sK1513,sK1516),k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518)))
| ~ r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(sK1513),u1_cat_1(sK1511),u2_cat_1(sK1513),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,k8_nattra_1(sK1511,k11_cat_2(sK1512,sK1513),sK1514,sK1515,sK1516,sK1517,sK1518)),k8_nattra_1(sK1511,sK1513,k12_isocat_2(sK1511,sK1512,sK1513,sK1514),k12_isocat_2(sK1511,sK1512,sK1513,sK1515),k12_isocat_2(sK1511,sK1512,sK1513,sK1516),k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518))) ),
inference(cnf_transformation,[],[f11186]) ).
fof(f22443,definition,
sF1519 = u1_cat_1(sK1511),
introduced(definition,[new_symbols(definition,[sF1519])],[function_definition]) ).
fof(f22444,plain,
u1_cat_1(sK1511) = sF1519,
inference(reorient_equations,[],[f22443]) ).
fof(f22445,definition,
sF1520 = u2_cat_1(sK1512),
introduced(definition,[new_symbols(definition,[sF1520])],[function_definition]) ).
fof(f22446,plain,
u2_cat_1(sK1512) = sF1520,
inference(reorient_equations,[],[f22445]) ).
fof(f22447,definition,
sF1521 = k11_cat_2(sK1512,sK1513),
introduced(definition,[new_symbols(definition,[sF1521])],[function_definition]) ).
fof(f22448,plain,
k11_cat_2(sK1512,sK1513) = sF1521,
inference(reorient_equations,[],[f22447]) ).
fof(f22449,definition,
sF1522 = k8_nattra_1(sK1511,sF1521,sK1514,sK1515,sK1516,sK1517,sK1518),
introduced(definition,[new_symbols(definition,[sF1522])],[function_definition]) ).
fof(f22450,plain,
k8_nattra_1(sK1511,sF1521,sK1514,sK1515,sK1516,sK1517,sK1518) = sF1522,
inference(reorient_equations,[],[f22449]) ).
fof(f22451,definition,
sF1523 = k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522),
introduced(definition,[new_symbols(definition,[sF1523])],[function_definition]) ).
fof(f22452,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = sF1523,
inference(reorient_equations,[],[f22451]) ).
fof(f22453,definition,
sF1524 = k11_isocat_2(sK1511,sK1512,sK1513,sK1514),
introduced(definition,[new_symbols(definition,[sF1524])],[function_definition]) ).
fof(f22454,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = sF1524,
inference(reorient_equations,[],[f22453]) ).
fof(f22455,definition,
sF1525 = k11_isocat_2(sK1511,sK1512,sK1513,sK1515),
introduced(definition,[new_symbols(definition,[sF1525])],[function_definition]) ).
fof(f22456,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1515) = sF1525,
inference(reorient_equations,[],[f22455]) ).
fof(f22457,definition,
sF1526 = k11_isocat_2(sK1511,sK1512,sK1513,sK1516),
introduced(definition,[new_symbols(definition,[sF1526])],[function_definition]) ).
fof(f22458,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1516) = sF1526,
inference(reorient_equations,[],[f22457]) ).
fof(f22459,definition,
sF1527 = k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),
introduced(definition,[new_symbols(definition,[sF1527])],[function_definition]) ).
fof(f22460,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = sF1527,
inference(reorient_equations,[],[f22459]) ).
fof(f22461,definition,
sF1528 = k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518),
introduced(definition,[new_symbols(definition,[sF1528])],[function_definition]) ).
fof(f22462,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = sF1528,
inference(reorient_equations,[],[f22461]) ).
fof(f22463,definition,
sF1529 = k8_nattra_1(sK1511,sK1512,sF1524,sF1525,sF1526,sF1527,sF1528),
introduced(definition,[new_symbols(definition,[sF1529])],[function_definition]) ).
fof(f22464,plain,
k8_nattra_1(sK1511,sK1512,sF1524,sF1525,sF1526,sF1527,sF1528) = sF1529,
inference(reorient_equations,[],[f22463]) ).
fof(f22465,definition,
sF1530 = u2_cat_1(sK1513),
introduced(definition,[new_symbols(definition,[sF1530])],[function_definition]) ).
fof(f22466,plain,
u2_cat_1(sK1513) = sF1530,
inference(reorient_equations,[],[f22465]) ).
fof(f22467,definition,
sF1531 = k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522),
introduced(definition,[new_symbols(definition,[sF1531])],[function_definition]) ).
fof(f22468,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = sF1531,
inference(reorient_equations,[],[f22467]) ).
fof(f22469,definition,
sF1532 = k12_isocat_2(sK1511,sK1512,sK1513,sK1514),
introduced(definition,[new_symbols(definition,[sF1532])],[function_definition]) ).
fof(f22470,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = sF1532,
inference(reorient_equations,[],[f22469]) ).
fof(f22471,definition,
sF1533 = k12_isocat_2(sK1511,sK1512,sK1513,sK1515),
introduced(definition,[new_symbols(definition,[sF1533])],[function_definition]) ).
fof(f22472,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1515) = sF1533,
inference(reorient_equations,[],[f22471]) ).
fof(f22473,definition,
sF1534 = k12_isocat_2(sK1511,sK1512,sK1513,sK1516),
introduced(definition,[new_symbols(definition,[sF1534])],[function_definition]) ).
fof(f22474,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1516) = sF1534,
inference(reorient_equations,[],[f22473]) ).
fof(f22475,definition,
sF1535 = k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517),
introduced(definition,[new_symbols(definition,[sF1535])],[function_definition]) ).
fof(f22476,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = sF1535,
inference(reorient_equations,[],[f22475]) ).
fof(f22477,definition,
sF1536 = k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518),
introduced(definition,[new_symbols(definition,[sF1536])],[function_definition]) ).
fof(f22478,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = sF1536,
inference(reorient_equations,[],[f22477]) ).
fof(f22479,definition,
sF1537 = k8_nattra_1(sK1511,sK1513,sF1532,sF1533,sF1534,sF1535,sF1536),
introduced(definition,[new_symbols(definition,[sF1537])],[function_definition]) ).
fof(f22480,plain,
k8_nattra_1(sK1511,sK1513,sF1532,sF1533,sF1534,sF1535,sF1536) = sF1537,
inference(reorient_equations,[],[f22479]) ).
fof(f22481,plain,
( ~ r4_nattra_1(sF1519,sF1520,sF1519,sF1520,sF1523,sF1529)
| ~ r4_nattra_1(sF1519,sF1530,sF1519,sF1530,sF1531,sF1537) ),
inference(definition_folding,[],[f18807,f22480,f22478,f22476,f22474,f22472,f22470,f22468,f22450,f22448,f22466,f22444,f22466,f22444,f22464,f22462,f22460,f22458,f22456,f22454,f22452,f22450,f22448,f22446,f22444,f22446,f22444]) ).
fof(f22482,plain,
m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516),
inference(definition_folding,[],[f18806,f22448]) ).
fof(f22483,plain,
m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515),
inference(definition_folding,[],[f18805,f22448]) ).
fof(f22484,plain,
r2_nattra_1(sK1511,sF1521,sK1514,sK1515),
inference(definition_folding,[],[f18804,f22448]) ).
fof(f22485,plain,
r2_nattra_1(sK1511,sF1521,sK1515,sK1516),
inference(definition_folding,[],[f18803,f22448]) ).
fof(f22486,plain,
m2_cat_1(sK1516,sK1511,sF1521),
inference(definition_folding,[],[f18802,f22448]) ).
fof(f22487,plain,
m2_cat_1(sK1515,sK1511,sF1521),
inference(definition_folding,[],[f18801,f22448]) ).
fof(f22488,plain,
m2_cat_1(sK1514,sK1511,sF1521),
inference(definition_folding,[],[f18800,f22448]) ).
fof(f22519,definition,
( spl1538_1
<=> r4_nattra_1(sF1519,sF1530,sF1519,sF1530,sF1531,sF1537) ),
introduced(definition,[new_symbols(definition,[spl1538_1])],[avatar_definition]) ).
fof(f22521,plain,
( ~ r4_nattra_1(sF1519,sF1530,sF1519,sF1530,sF1531,sF1537)
| spl1538_1 ),
inference(avatar_component_clause,[],[f22519]) ).
fof(f22523,definition,
( spl1538_2
<=> r4_nattra_1(sF1519,sF1520,sF1519,sF1520,sF1523,sF1529) ),
introduced(definition,[new_symbols(definition,[spl1538_2])],[avatar_definition]) ).
fof(f22526,plain,
( ~ spl1538_1
| ~ spl1538_2 ),
inference(avatar_split_clause,[],[f22481,f22523,f22519]) ).
fof(f26792,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f18782,f22448]) ).
fof(f26802,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f18783,f22448]) ).
fof(f26808,plain,
( l1_cat_1(sF1521)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18272,f22448]) ).
fof(f26809,plain,
( v2_cat_1(sF1521)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18273,f22448]) ).
fof(f26813,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(superposition,[],[f18545,f22450]) ).
fof(f26826,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ 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,[],[f18788,f22448]) ).
fof(f26829,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ 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,[],[f18787,f22448]) ).
fof(f26839,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ r2_nattra_1(sK1511,sF1521,sK1514,sK1515)
| ~ r2_nattra_1(sK1511,sF1521,sK1515,sK1516)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(superposition,[],[f18622,f22450]) ).
fof(f27002,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18694,f22448]) ).
fof(f27023,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(superposition,[],[f18692,f22448]) ).
fof(f27838,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f26792,f18799]) ).
fof(f27846,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f26802,f18799]) ).
fof(f27852,plain,
( l1_cat_1(sF1521)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26808,f18797]) ).
fof(f27853,plain,
( v2_cat_1(sF1521)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f26809,f18797]) ).
fof(f27854,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f26813,f18795]) ).
fof(f27867,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26826,f18799]) ).
fof(f27869,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f26829,f18799]) ).
fof(f27874,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ r2_nattra_1(sK1511,sF1521,sK1515,sK1516)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f26839,f22484]) ).
fof(f27999,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27002,f18797]) ).
fof(f28011,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27023,f18797]) ).
fof(f28375,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f27838,f18798]) ).
fof(f28383,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,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,[],[f27846,f18798]) ).
fof(f28389,plain,
( l1_cat_1(sF1521)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27852,f18796]) ).
fof(f28390,plain,
( v2_cat_1(sF1521)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27853,f18796]) ).
fof(f28391,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f27854,f18794]) ).
fof(f28399,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27867,f18798]) ).
fof(f28401,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ v2_cat_1(sK1512)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f27869,f18798]) ).
fof(f28406,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f27874,f22485]) ).
fof(f28531,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f27999,f18796]) ).
fof(f28543,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ v2_cat_1(sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f28011,f18796]) ).
fof(f28879,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28375,f18797]) ).
fof(f28885,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28383,f18797]) ).
fof(f28889,plain,
( l1_cat_1(sF1521)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f28389,f18799]) ).
fof(f28890,plain,
( v2_cat_1(sF1521)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f28390,f18799]) ).
fof(f28891,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f28391,f22488]) ).
fof(f28896,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28399,f18797]) ).
fof(f28897,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28401,f18797]) ).
fof(f28898,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f28406,f22482]) ).
fof(f28910,definition,
( spl1538_601
<=> l1_cat_1(sF1521) ),
introduced(definition,[new_symbols(definition,[spl1538_601])],[avatar_definition]) ).
fof(f28914,definition,
( spl1538_602
<=> v2_cat_1(sF1521) ),
introduced(definition,[new_symbols(definition,[spl1538_602])],[avatar_definition]) ).
fof(f28966,plain,
( m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f28531,f18799]) ).
fof(f28971,plain,
( m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ l1_cat_1(sK1513) ),
inference(forward_subsumption_resolution,[],[f28543,f18799]) ).
fof(f29174,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k11_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,sK1512,X0,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28879,f18796]) ).
fof(f29180,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,X1,sF1521)
| k12_isocat_2(X1,sK1512,sK1513,X0) = k2_isocat_1(X1,sF1521,sK1513,X0,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28885,f18796]) ).
fof(f29184,plain,
l1_cat_1(sF1521),
inference(forward_subsumption_resolution,[],[f28889,f18798]) ).
fof(f29185,plain,
v2_cat_1(sF1521),
inference(forward_subsumption_resolution,[],[f28890,f18798]) ).
fof(f29186,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f28891,f22487]) ).
fof(f29191,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k14_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1513,X2,X3,X0,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28896,f18796]) ).
fof(f29192,plain,
! [X2,X3,X0,X1] :
( ~ m2_nattra_1(X0,X1,sF1521,X2,X3)
| k13_isocat_2(X1,sK1512,sK1513,X2,X3,X0) = k6_isocat_1(X1,sF1521,sK1512,X2,X3,X0,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(X3,X1,sF1521)
| ~ m2_cat_1(X2,X1,sF1521)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f28897,f18796]) ).
fof(f29193,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f28898,f22483]) ).
fof(f29247,plain,
m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513),
inference(forward_subsumption_resolution,[],[f28966,f18798]) ).
fof(f29250,plain,
m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512),
inference(forward_subsumption_resolution,[],[f28971,f18798]) ).
fof(f29332,plain,
spl1538_601,
inference(avatar_split_clause,[],[f29184,f28910]) ).
fof(f29333,plain,
spl1538_602,
inference(avatar_split_clause,[],[f29185,f28914]) ).
fof(f29334,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_nattra_1(sK1517,sK1511,sF1521,sK1514,sK1515)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f29186,f22486]) ).
fof(f29393,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f29193,f22486]) ).
fof(f29527,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ m2_nattra_1(sK1518,sK1511,sF1521,sK1515,sK1516) ),
inference(forward_subsumption_resolution,[],[f29334,f22483]) ).
fof(f29528,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f29393,f22487]) ).
fof(f29698,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521) ),
inference(forward_subsumption_resolution,[],[f29527,f22482]) ).
fof(f29699,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f29528,f22488]) ).
fof(f29766,definition,
( spl1538_683
<=> m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516) ),
introduced(definition,[new_symbols(definition,[spl1538_683])],[avatar_definition]) ).
fof(f29768,plain,
( m2_nattra_1(sF1522,sK1511,sF1521,sK1514,sK1516)
| ~ spl1538_683 ),
inference(avatar_component_clause,[],[f29766]) ).
fof(f29769,plain,
( ~ spl1538_601
| ~ spl1538_602
| spl1538_683 ),
inference(avatar_split_clause,[],[f29698,f29766,f28914,f28910]) ).
fof(f29770,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ l1_cat_1(sK1511)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f29699,f18795]) ).
fof(f29828,plain,
! [X0,X1] :
( r4_nattra_1(u1_cat_1(sK1511),u2_cat_1(X0),u1_cat_1(sK1511),u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f29770,f18794]) ).
fof(f29880,plain,
! [X0,X1] :
( r4_nattra_1(sF1519,u2_cat_1(X0),sF1519,u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ m2_cat_1(X1,sF1521,X0)
| ~ v2_cat_1(sF1521)
| ~ l1_cat_1(sF1521)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_demodulation,[],[f29828,f22444]) ).
fof(f29939,definition,
( spl1538_686
<=> ! [X0,X1] :
( r4_nattra_1(sF1519,u2_cat_1(X0),sF1519,u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X1,sF1521,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1538_686])],[avatar_definition]) ).
fof(f29940,plain,
( ! [X0,X1] :
( r4_nattra_1(sF1519,u2_cat_1(X0),sF1519,u2_cat_1(X0),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1516,sF1522,X1),k8_nattra_1(sK1511,X0,k2_isocat_1(sK1511,sF1521,X0,sK1514,X1),k2_isocat_1(sK1511,sF1521,X0,sK1515,X1),k2_isocat_1(sK1511,sF1521,X0,sK1516,X1),k6_isocat_1(sK1511,sF1521,X0,sK1514,sK1515,sK1517,X1),k6_isocat_1(sK1511,sF1521,X0,sK1515,sK1516,sK1518,X1)))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m2_cat_1(X1,sF1521,X0) )
| ~ spl1538_686 ),
inference(avatar_component_clause,[],[f29939]) ).
fof(f29941,plain,
( ~ spl1538_601
| ~ spl1538_602
| spl1538_686 ),
inference(avatar_split_clause,[],[f29880,f29939,f28914,f28910]) ).
fof(f30396,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29174,f22486]) ).
fof(f30397,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29174,f22488]) ).
fof(f30398,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29174,f22487]) ).
fof(f30406,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30398,f18795]) ).
fof(f30407,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30397,f18795]) ).
fof(f30408,plain,
( k11_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30396,f18795]) ).
fof(f30420,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30406,f18794]) ).
fof(f30421,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30407,f18794]) ).
fof(f30422,plain,
k11_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30408,f18794]) ).
fof(f30434,plain,
sF1525 = k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30420,f22456]) ).
fof(f30435,plain,
sF1524 = k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30421,f22454]) ).
fof(f30436,plain,
sF1526 = k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30422,f22458]) ).
fof(f30456,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29180,f22486]) ).
fof(f30457,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29180,f22488]) ).
fof(f30458,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29180,f22487]) ).
fof(f30466,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30458,f18795]) ).
fof(f30467,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30457,f18795]) ).
fof(f30468,plain,
( k12_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f30456,f18795]) ).
fof(f30480,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1515) = k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30466,f18794]) ).
fof(f30481,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1514) = k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30467,f18794]) ).
fof(f30482,plain,
k12_isocat_2(sK1511,sK1512,sK1513,sK1516) = k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f30468,f18794]) ).
fof(f30494,plain,
sF1533 = k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30480,f22472]) ).
fof(f30495,plain,
sF1532 = k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30481,f22470]) ).
fof(f30496,plain,
sF1534 = k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f30482,f22474]) ).
fof(f31390,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29191,f22482]) ).
fof(f31391,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29191,f22483]) ).
fof(f31392,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(resolution,[],[f29191,f29768]) ).
fof(f31405,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31392,f22486]) ).
fof(f31406,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31391,f22487]) ).
fof(f31407,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31390,f22486]) ).
fof(f31412,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31405,f22488]) ).
fof(f31413,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31406,f22488]) ).
fof(f31414,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31407,f22487]) ).
fof(f31416,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31412,f18795]) ).
fof(f31417,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31413,f18795]) ).
fof(f31418,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31414,f18795]) ).
fof(f31420,plain,
( k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31416,f18794]) ).
fof(f31421,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f31417,f18794]) ).
fof(f31422,plain,
k14_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f31418,f18794]) ).
fof(f31423,plain,
( sF1531 = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1516,sF1522,k9_isocat_2(sK1512,sK1513))
| ~ spl1538_683 ),
inference(forward_demodulation,[],[f31420,f22468]) ).
fof(f31424,plain,
sF1535 = k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f31421,f22476]) ).
fof(f31425,plain,
sF1536 = k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f31422,f22478]) ).
fof(f31464,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29192,f22482]) ).
fof(f31465,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(resolution,[],[f29192,f22483]) ).
fof(f31466,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1516,sK1511,sF1521)
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(resolution,[],[f29192,f29768]) ).
fof(f31479,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31466,f22486]) ).
fof(f31480,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1514,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31465,f22487]) ).
fof(f31481,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513))
| ~ m2_cat_1(sK1515,sK1511,sF1521)
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31464,f22486]) ).
fof(f31486,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31479,f22488]) ).
fof(f31487,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31480,f22488]) ).
fof(f31488,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513))
| ~ v2_cat_1(sK1511)
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31481,f22487]) ).
fof(f31490,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511)
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31486,f18795]) ).
fof(f31491,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31487,f18795]) ).
fof(f31492,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513))
| ~ l1_cat_1(sK1511) ),
inference(forward_subsumption_resolution,[],[f31488,f18795]) ).
fof(f31494,plain,
( k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1516,sF1522) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ spl1538_683 ),
inference(forward_subsumption_resolution,[],[f31490,f18794]) ).
fof(f31495,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1514,sK1515,sK1517) = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f31491,f18794]) ).
fof(f31496,plain,
k13_isocat_2(sK1511,sK1512,sK1513,sK1515,sK1516,sK1518) = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513)),
inference(forward_subsumption_resolution,[],[f31492,f18794]) ).
fof(f31497,plain,
( sF1523 = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513))
| ~ spl1538_683 ),
inference(forward_demodulation,[],[f31494,f22452]) ).
fof(f31498,plain,
sF1527 = k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f31495,f22460]) ).
fof(f31499,plain,
sF1528 = k6_isocat_1(sK1511,sF1521,sK1512,sK1515,sK1516,sK1518,k8_isocat_2(sK1512,sK1513)),
inference(forward_demodulation,[],[f31496,f22462]) ).
fof(f34456,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))))
| ~ l1_cat_1(sK1513)
| ~ v2_cat_1(sK1513)
| ~ m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(superposition,[],[f29940,f31423]) ).
fof(f34465,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),sF1528))
| ~ l1_cat_1(sK1512)
| ~ v2_cat_1(sK1512)
| ~ m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ spl1538_686 ),
inference(superposition,[],[f29940,f31499]) ).
fof(f34470,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),sF1528))
| ~ v2_cat_1(sK1512)
| ~ m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34465,f18796]) ).
fof(f34479,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))))
| ~ v2_cat_1(sK1513)
| ~ m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34456,f18798]) ).
fof(f34486,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),sF1528))
| ~ m2_cat_1(k8_isocat_2(sK1512,sK1513),sF1521,sK1512)
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34470,f18797]) ).
fof(f34495,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))))
| ~ m2_cat_1(k9_isocat_2(sK1512,sK1513),sF1521,sK1513)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34479,f18799]) ).
fof(f34502,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1515,sK1517,k8_isocat_2(sK1512,sK1513)),sF1528))
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34486,f29250]) ).
fof(f34511,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1515,sK1516,sK1518,k9_isocat_2(sK1512,sK1513))))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34495,f29247]) ).
fof(f34514,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1516,k8_isocat_2(sK1512,sK1513)),sF1527,sF1528))
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34502,f31498]) ).
fof(f34523,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),k6_isocat_1(sK1511,sF1521,sK1513,sK1514,sK1515,sK1517,k9_isocat_2(sK1512,sK1513)),sF1536))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34511,f31425]) ).
fof(f34526,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1512,sK1515,k8_isocat_2(sK1512,sK1513)),sF1526,sF1527,sF1528))
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34514,f30436]) ).
fof(f34535,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1516,k9_isocat_2(sK1512,sK1513)),sF1535,sF1536))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34523,f31424]) ).
fof(f34538,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,k2_isocat_1(sK1511,sF1521,sK1512,sK1514,k8_isocat_2(sK1512,sK1513)),sF1525,sF1526,sF1527,sF1528))
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34526,f30434]) ).
fof(f34547,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),k2_isocat_1(sK1511,sF1521,sK1513,sK1515,k9_isocat_2(sK1512,sK1513)),sF1534,sF1535,sF1536))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34535,f30496]) ).
fof(f34550,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),k8_nattra_1(sK1511,sK1512,sF1524,sF1525,sF1526,sF1527,sF1528))
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34538,f30435]) ).
fof(f34559,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,k2_isocat_1(sK1511,sF1521,sK1513,sK1514,k9_isocat_2(sK1512,sK1513)),sF1533,sF1534,sF1535,sF1536))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34547,f30494]) ).
fof(f34562,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),k6_isocat_1(sK1511,sF1521,sK1512,sK1514,sK1516,sF1522,k8_isocat_2(sK1512,sK1513)),sF1529)
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34550,f22464]) ).
fof(f34571,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,k8_nattra_1(sK1511,sK1513,sF1532,sF1533,sF1534,sF1535,sF1536))
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34559,f30495]) ).
fof(f34574,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1512),sF1519,u2_cat_1(sK1512),sF1523,sF1529)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34562,f31497]) ).
fof(f34583,plain,
( r4_nattra_1(sF1519,u2_cat_1(sK1513),sF1519,u2_cat_1(sK1513),sF1531,sF1537)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34571,f22480]) ).
fof(f34586,plain,
( r4_nattra_1(sF1519,sF1520,sF1519,sF1520,sF1523,sF1529)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34574,f22446]) ).
fof(f34595,plain,
( r4_nattra_1(sF1519,sF1530,sF1519,sF1530,sF1531,sF1537)
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_demodulation,[],[f34583,f22466]) ).
fof(f34599,plain,
( spl1538_2
| ~ spl1538_683
| ~ spl1538_686 ),
inference(avatar_split_clause,[],[f34586,f29939,f29766,f22523]) ).
fof(f34608,plain,
( $false
| spl1538_1
| ~ spl1538_683
| ~ spl1538_686 ),
inference(forward_subsumption_resolution,[],[f34595,f22521]) ).
fof(f34609,plain,
( spl1538_1
| ~ spl1538_683
| ~ spl1538_686 ),
inference(avatar_contradiction_clause,[],[f34608]) ).
cnf(s1,plain,
( ~ spl1538_1
| ~ spl1538_2 ),
inference(sat_conversion,[],[f22526]) ).
cnf(s555,plain,
spl1538_601,
inference(sat_conversion,[],[f29332]) ).
cnf(s556,plain,
spl1538_602,
inference(sat_conversion,[],[f29333]) ).
cnf(s596,plain,
( ~ spl1538_601
| ~ spl1538_602
| spl1538_683 ),
inference(sat_conversion,[],[f29769]) ).
cnf(s605,plain,
( ~ spl1538_601
| ~ spl1538_602
| spl1538_686 ),
inference(sat_conversion,[],[f29941]) ).
cnf(s650,plain,
( spl1538_2
| ~ spl1538_683
| ~ spl1538_686 ),
inference(sat_conversion,[],[f34599]) ).
cnf(s659,plain,
( spl1538_1
| ~ spl1538_683
| ~ spl1538_686 ),
inference(sat_conversion,[],[f34609]) ).
cnf(s672,plain,
spl1538_686,
inference(rat,[],[s605,s556,s555]) ).
cnf(s675,plain,
spl1538_683,
inference(rat,[],[s596,s556,s555]) ).
cnf(s705,plain,
spl1538_1,
inference(rat,[],[s659,s672,s675]) ).
cnf(s706,plain,
spl1538_2,
inference(rat,[],[s650,s672,s675]) ).
cnf(s752,plain,
$false,
inference(rat,[],[s1,s706,s705]) ).
fof(f34610,plain,
$false,
inference(avatar_sat_refutation,[],[s752]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT028+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n002.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 21:21:38 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 Running first-order theorem proving
% 0.07/0.20 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
% 24.48/4.36 % (780797)Detected formulas, will run a generic FOF schedule.
% 24.48/4.36 % (780873)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=985215935:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 24.48/4.36 % (780876)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3475610409:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 24.48/4.36 % (780877)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1740958250:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 24.48/4.36 % (780874)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=3930201965:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 24.48/4.36 % (780875)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=2048919460:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 24.48/4.36 % (780876)Refutation not found, incomplete strategy
% 24.48/4.36 % (780876)------------------------------
% 24.48/4.36 % (780876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.48/4.36 % (780876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.36 % (780876)CaDiCaL version: 2.1.3
% 24.48/4.36 % (780876)Termination reason: Refutation not found, incomplete strategy
% 24.48/4.36 % (780876)Time elapsed: 0.040 s
% 24.48/4.36 % (780876)Peak memory usage: 93 MB
% 24.48/4.36 % (780876)Instructions burned: 33 (million)
% 24.48/4.36 % (780878)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=187635190:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 24.48/4.36 % (780879)dis-21_1_sil=8000:lcm=predicate:random_seed=4048888499:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 24.48/4.36 % (780877)Instruction limit reached!
% 24.48/4.36 % (780877)------------------------------
% 24.48/4.36 % (780877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.48/4.36 % (780877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.36 % (780877)CaDiCaL version: 2.1.3
% 24.48/4.36 % (780877)Termination reason: Instruction limit
% 24.48/4.36 % (780877)Termination phase: Saturation
% 24.48/4.36 % (780877)Time elapsed: 0.120 s
% 24.48/4.36 % (780877)Peak memory usage: 94 MB
% 24.48/4.36 % (780877)Instructions burned: 119 (million)
% 24.48/4.36 % (780878)Instruction limit reached!
% 24.48/4.36 % (780878)------------------------------
% 24.48/4.36 % (780878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.48/4.36 % (780878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.36 % (780878)CaDiCaL version: 2.1.3
% 24.48/4.36 % (780878)Termination reason: Instruction limit
% 24.48/4.36 % (780878)Termination phase: Preprocessing 3
% 24.48/4.36 % (780878)Time elapsed: 0.136 s
% 24.48/4.36 % (780878)Peak memory usage: 94 MB
% 24.48/4.36 % (780878)Instructions burned: 139 (million)
% 24.48/4.36 % (780879)Instruction limit reached!
% 24.48/4.36 % (780879)------------------------------
% 24.48/4.36 % (780879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.48/4.36 % (780879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.36 % (780879)CaDiCaL version: 2.1.3
% 24.48/4.36 % (780879)Termination reason: Instruction limit
% 24.48/4.36 % (780879)Termination phase: Preprocessing 3
% 24.48/4.36 % (780879)Time elapsed: 0.140 s
% 24.48/4.36 % (780879)Peak memory usage: 94 MB
% 24.48/4.36 % (780879)Instructions burned: 129 (million)
% 24.48/4.36 % (780893)lrs+10_1_sil=8000:sp=occurrence:random_seed=2221429876:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 24.48/4.36 % (780876)------------------------------
% 24.48/4.36 % (780876)------------------------------
% 24.48/4.36 % (780894)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1224279825:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 24.48/4.36 % (780895)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3079624326:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 24.48/4.36 % (780894)Instruction limit reached!
% 24.48/4.36 % (780894)------------------------------
% 24.48/4.36 % (780894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.48/4.36 % (780894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780894)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780894)Termination reason: Instruction limit
% 27.60/4.88 % (780894)Termination phase: Saturation
% 27.60/4.88 % (780894)Time elapsed: 0.125 s
% 27.60/4.88 % (780894)Peak memory usage: 94 MB
% 27.60/4.88 % (780894)Instructions burned: 157 (million)
% 27.60/4.88 % (780893)Instruction limit reached!
% 27.60/4.88 % (780893)------------------------------
% 27.60/4.88 % (780893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780893)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780893)Termination reason: Instruction limit
% 27.60/4.88 % (780893)Termination phase: Saturation
% 27.60/4.88 % (780893)Time elapsed: 0.290 s
% 27.60/4.88 % (780893)Peak memory usage: 97 MB
% 27.60/4.88 % (780893)Instructions burned: 285 (million)
% 27.60/4.88 % (780899)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=2003244191:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 27.60/4.88 % (780895)Instruction limit reached!
% 27.60/4.88 % (780895)------------------------------
% 27.60/4.88 % (780895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780895)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780895)Termination reason: Instruction limit
% 27.60/4.88 % (780895)Termination phase: Saturation
% 27.60/4.88 % (780895)Time elapsed: 0.299 s
% 27.60/4.88 % (780895)Peak memory usage: 96 MB
% 27.60/4.88 % (780895)Instructions burned: 325 (million)
% 27.60/4.88 % (780905)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3119345155:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 27.60/4.88 % (780904)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2048219181:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 27.60/4.88 % (780899)Instruction limit reached!
% 27.60/4.88 % (780899)------------------------------
% 27.60/4.88 % (780899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780899)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780899)Termination reason: Instruction limit
% 27.60/4.88 % (780899)Termination phase: Property scanning
% 27.60/4.88 % (780899)Time elapsed: 0.243 s
% 27.60/4.88 % (780899)Peak memory usage: 98 MB
% 27.60/4.88 % (780899)Instructions burned: 249 (million)
% 27.60/4.88 % (780909)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3354928424:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 27.60/4.88 % (780904)Instruction limit reached!
% 27.60/4.88 % (780904)------------------------------
% 27.60/4.88 % (780904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780904)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780904)Termination reason: Instruction limit
% 27.60/4.88 % (780904)Termination phase: Saturation
% 27.60/4.88 % (780904)Time elapsed: 0.284 s
% 27.60/4.88 % (780904)Peak memory usage: 97 MB
% 27.60/4.88 % (780904)Instructions burned: 294 (million)
% 27.60/4.88 % (780909)Instruction limit reached!
% 27.60/4.88 % (780909)------------------------------
% 27.60/4.88 % (780909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780909)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780909)Termination reason: Instruction limit
% 27.60/4.88 % (780909)Termination phase: Property scanning
% 27.60/4.88 % (780909)Time elapsed: 0.115 s
% 27.60/4.88 % (780909)Peak memory usage: 93 MB
% 27.60/4.88 % (780909)Instructions burned: 114 (million)
% 27.60/4.88 % (780912)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3841250536:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 27.60/4.88 % (780918)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=484527913:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 27.60/4.88 % (780912)Instruction limit reached!
% 27.60/4.88 % (780912)------------------------------
% 27.60/4.88 % (780912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780912)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780912)Termination reason: Instruction limit
% 27.60/4.88 % (780912)Termination phase: Preprocessing 3
% 27.60/4.88 % (780912)Time elapsed: 0.136 s
% 27.60/4.88 % (780912)Peak memory usage: 96 MB
% 27.60/4.88 % (780912)Instructions burned: 128 (million)
% 27.60/4.88 % (780918)Instruction limit reached!
% 27.60/4.88 % (780918)------------------------------
% 27.60/4.88 % (780918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780918)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780918)Termination reason: Instruction limit
% 27.60/4.88 % (780918)Termination phase: SInE selection
% 27.60/4.88 % (780918)Time elapsed: 0.094 s
% 27.60/4.88 % (780918)Peak memory usage: 89 MB
% 27.60/4.88 % (780918)Instructions burned: 114 (million)
% 27.60/4.88 % (780919)lrs+10_1_sil=8000:sp=occurrence:random_seed=36629685:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 27.60/4.88 % (780922)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3018779636:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 27.60/4.88 % (780923)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1719344996:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 27.60/4.88 % (780922)Instruction limit reached!
% 27.60/4.88 % (780922)------------------------------
% 27.60/4.88 % (780922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780922)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780922)Termination reason: Instruction limit
% 27.60/4.88 % (780922)Termination phase: Saturation
% 27.60/4.88 % (780922)Time elapsed: 0.410 s
% 27.60/4.88 % (780922)Peak memory usage: 97 MB
% 27.60/4.88 % (780922)Instructions burned: 437 (million)
% 27.60/4.88 % (780929)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1056941267:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 27.60/4.88 % (780919)Instruction limit reached!
% 27.60/4.88 % (780919)------------------------------
% 27.60/4.88 % (780919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780919)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780919)Termination reason: Instruction limit
% 27.60/4.88 % (780919)Termination phase: Saturation
% 27.60/4.88 % (780919)Time elapsed: 0.869 s
% 27.60/4.88 % (780919)Peak memory usage: 109 MB
% 27.60/4.88 % (780919)Instructions burned: 907 (million)
% 27.60/4.88 % (780929)Instruction limit reached!
% 27.60/4.88 % (780929)------------------------------
% 27.60/4.88 % (780929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780929)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780929)Termination reason: Instruction limit
% 27.60/4.88 % (780929)Termination phase: Saturation
% 27.60/4.88 % (780929)Time elapsed: 0.116 s
% 27.60/4.88 % (780929)Peak memory usage: 95 MB
% 27.60/4.88 % (780929)Instructions burned: 134 (million)
% 27.60/4.88 % (780931)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=798275223:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 27.60/4.88 % (780932)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3615343874:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 27.60/4.88 % (780931)Instruction limit reached!
% 27.60/4.88 % (780931)------------------------------
% 27.60/4.88 % (780931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780931)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780931)Termination reason: Instruction limit
% 27.60/4.88 % (780931)Termination phase: Saturation
% 27.60/4.88 % (780931)Time elapsed: 0.458 s
% 27.60/4.88 % (780931)Peak memory usage: 104 MB
% 27.60/4.88 % (780931)Instructions burned: 593 (million)
% 27.60/4.88 % (780905)Instruction limit reached!
% 27.60/4.88 % (780905)------------------------------
% 27.60/4.88 % (780905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780905)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780905)Termination reason: Instruction limit
% 27.60/4.88 % (780905)Termination phase: Saturation
% 27.60/4.88 % (780905)Time elapsed: 2.435 s
% 27.60/4.88 % (780905)Peak memory usage: 259 MB
% 27.60/4.88 % (780905)Instructions burned: 2351 (million)
% 27.60/4.88 % (780937)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=3027490640:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/125Mi)
% 27.60/4.88 % (780937)Instruction limit reached!
% 27.60/4.88 % (780937)------------------------------
% 27.60/4.88 % (780937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780937)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780937)Termination reason: Instruction limit
% 27.60/4.88 % (780937)Termination phase: Preprocessing 3
% 27.60/4.88 % (780937)Time elapsed: 0.128 s
% 27.60/4.88 % (780937)Peak memory usage: 92 MB
% 27.60/4.88 % (780937)Instructions burned: 125 (million)
% 27.60/4.88 % (780873)First to succeed.
% 27.60/4.88 % (780873)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-780797"
% 27.60/4.88 % (780938)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3780913878:i=134:gtgl=5:slsql=off:gtg=exists_sym_2962 on theBenchmark for (2962ds/134Mi)
% 27.60/4.88 % (780938)Instruction limit reached!
% 27.60/4.88 % (780938)------------------------------
% 27.60/4.88 % (780938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.60/4.88 % (780938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.60/4.88 % (780938)CaDiCaL version: 2.1.3
% 27.60/4.88 % (780938)Termination reason: Instruction limit
% 27.60/4.88 % (780938)Termination phase: Preprocessing 1
% 27.60/4.88 % (780938)Time elapsed: 0.123 s
% 27.60/4.88 % (780938)Peak memory usage: 90 MB
% 27.60/4.88 % (780938)Instructions burned: 135 (million)
% 27.60/4.88 % (780873)Refutation found. Thanks to Tanya!
% 27.60/4.88 % SZS status Theorem for theBenchmark
% 27.60/4.88 % SZS output start Proof for theBenchmark
% See solution above
% 28.96/5.19 % (780873)------------------------------
% 28.96/5.19 % (780873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/5.19 % (780873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/5.19 % (780873)CaDiCaL version: 2.1.3
% 28.96/5.19 % (780873)Termination reason: Refutation
% 28.96/5.19 % (780873)Time elapsed: 3.511 s
% 28.96/5.19 % (780873)Peak memory usage: 239 MB
% 28.96/5.19 % (780873)Instructions burned: 6847 (million)
% 28.96/5.19 % (780873)------------------------------
% 28.96/5.19 % (780873)------------------------------
% 28.96/5.19 % (780797)Success in time 4.191 s
% 28.96/5.19 % Vampire exiting
%------------------------------------------------------------------------------