%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT028+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 11.21s 5.07s
% Output : Refutation 28.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 18
% Syntax : Number of formulae : 273 ( 37 unt; 7 def)
% Number of atoms : 1510 ( 118 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 2323 (1086 ~;1086 |; 91 &)
% ( 7 <=>; 53 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 8 prp; 0-6 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-7 aty)
% Number of variables : 258 ( 0 sgn 242 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21083,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_cat_2) ).
fof(f21181,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f25804,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(f27611,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(f29039,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f29041,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f29095,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f29096,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f29099,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f29100,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f29104,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(f29105,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)],[f29104]) ).
fof(f29275,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,[],[f29105]) ).
fof(f29276,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,[],[f29275]) ).
fof(f29323,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21181]) ).
fof(f29324,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,[],[f29323]) ).
fof(f29341,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,[],[f27611]) ).
fof(f29342,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,[],[f29341]) ).
fof(f29343,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,[],[f25804]) ).
fof(f29344,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,[],[f29343]) ).
fof(f29361,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29095]) ).
fof(f29362,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,[],[f29361]) ).
fof(f29367,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29096]) ).
fof(f29368,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,[],[f29367]) ).
fof(f29375,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29099]) ).
fof(f29376,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,[],[f29375]) ).
fof(f29377,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29100]) ).
fof(f29378,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,[],[f29377]) ).
fof(f30247,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29039]) ).
fof(f30248,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,[],[f30247]) ).
fof(f30251,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29041]) ).
fof(f30252,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,[],[f30251]) ).
fof(f31958,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21083]) ).
fof(f31959,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f31958]) ).
fof(f33438,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k11_isocat_2(sK98,sK99,sK100,sK101),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k12_isocat_2(sK98,sK99,sK100,sK101),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105))) )
& m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
& m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
& r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102)
& r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103)
& m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
& m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
& m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
& v2_cat_1(sK100)
& l1_cat_1(sK100)
& v2_cat_1(sK99)
& l1_cat_1(sK99)
& v2_cat_1(sK98)
& l1_cat_1(sK98) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK98,sK99,sK100,sK101,sK102,sK103,sK104,sK105]),skolemize(X0,sK98),skolemize(X1,sK99),skolemize(X2,sK100),skolemize(X3,sK101),skolemize(X4,sK102),skolemize(X5,sK103),skolemize(X6,sK104),skolemize(X7,sK105)],[f29276]) ).
fof(f34714,plain,
l1_cat_1(sK98),
inference(cnf_transformation,[],[f33438]) ).
fof(f34715,plain,
v2_cat_1(sK98),
inference(cnf_transformation,[],[f33438]) ).
fof(f34716,plain,
l1_cat_1(sK99),
inference(cnf_transformation,[],[f33438]) ).
fof(f34717,plain,
v2_cat_1(sK99),
inference(cnf_transformation,[],[f33438]) ).
fof(f34718,plain,
l1_cat_1(sK100),
inference(cnf_transformation,[],[f33438]) ).
fof(f34719,plain,
v2_cat_1(sK100),
inference(cnf_transformation,[],[f33438]) ).
fof(f34720,plain,
m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100)),
inference(cnf_transformation,[],[f33438]) ).
fof(f34721,plain,
m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100)),
inference(cnf_transformation,[],[f33438]) ).
fof(f34722,plain,
m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100)),
inference(cnf_transformation,[],[f33438]) ).
fof(f34723,plain,
r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103),
inference(cnf_transformation,[],[f33438]) ).
fof(f34724,plain,
r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102),
inference(cnf_transformation,[],[f33438]) ).
fof(f34725,plain,
m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102),
inference(cnf_transformation,[],[f33438]) ).
fof(f34726,plain,
m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103),
inference(cnf_transformation,[],[f33438]) ).
fof(f34727,plain,
( ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k11_isocat_2(sK98,sK99,sK100,sK101),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k12_isocat_2(sK98,sK99,sK100,sK101),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105))) ),
inference(cnf_transformation,[],[f33438]) ).
fof(f34775,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,[],[f29324]) ).
fof(f34785,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,[],[f29342]) ).
fof(f34786,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,[],[f29344]) ).
fof(f34799,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,[],[f29362]) ).
fof(f34802,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,[],[f29368]) ).
fof(f34806,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,[],[f29376]) ).
fof(f34807,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,[],[f29378]) ).
fof(f36174,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,[],[f30248]) ).
fof(f36176,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,[],[f30252]) ).
fof(f38324,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,[],[f31959]) ).
fof(f42711,definition,
( spl921_19
<=> r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k12_isocat_2(sK98,sK99,sK100,sK101),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105))) ),
introduced(definition,[new_symbols(definition,[spl921_19])],[avatar_definition]) ).
fof(f42713,plain,
( ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k12_isocat_2(sK98,sK99,sK100,sK101),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| spl921_19 ),
inference(avatar_component_clause,[],[f42711]) ).
fof(f42715,definition,
( spl921_20
<=> r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k11_isocat_2(sK98,sK99,sK100,sK101),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105))) ),
introduced(definition,[new_symbols(definition,[spl921_20])],[avatar_definition]) ).
fof(f42717,plain,
( ~ r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k11_isocat_2(sK98,sK99,sK100,sK101),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| spl921_20 ),
inference(avatar_component_clause,[],[f42715]) ).
fof(f42718,plain,
( ~ spl921_19
| ~ spl921_20 ),
inference(avatar_split_clause,[],[f34727,f42715,f42711]) ).
fof(f43003,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34725,f34806]) ).
fof(f43004,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34725,f34807]) ).
fof(f43005,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34726,f34806]) ).
fof(f43006,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34726,f34807]) ).
fof(f43007,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X5,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
| k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7),k8_isocat_2(X1,X2))
| ~ m2_cat_1(X5,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(resolution,[],[f34786,f34806]) ).
fof(f43010,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(k11_cat_2(X1,X2))
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X5,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
| k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7),k8_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(duplicate_literal_removal,[],[f43007]) ).
fof(f43015,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34802,f34720]) ).
fof(f43016,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34802,f34722]) ).
fof(f43017,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34802,f34721]) ).
fof(f43022,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34799,f34720]) ).
fof(f43023,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34799,f34722]) ).
fof(f43024,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(resolution,[],[f34799,f34721]) ).
fof(f43625,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43004,f34721]) ).
fof(f43626,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43003,f34721]) ).
fof(f43627,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43006,f34722]) ).
fof(f43628,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43005,f34722]) ).
fof(f43630,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ l1_cat_1(k11_cat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X5,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
| ~ m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
| k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7),k8_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f43010,f38324]) ).
fof(f43635,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43017,f34719]) ).
fof(f43636,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43016,f34719]) ).
fof(f43637,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43015,f34719]) ).
fof(f43640,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43024,f34719]) ).
fof(f43641,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43023,f34719]) ).
fof(f43642,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43022,f34719]) ).
fof(f43866,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43625,f34720]) ).
fof(f43867,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43626,f34720]) ).
fof(f43868,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43627,f34721]) ).
fof(f43869,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43628,f34721]) ).
fof(f43871,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ m2_nattra_1(X7,X0,k11_cat_2(X1,X2),X4,X5)
| ~ l1_cat_1(X0)
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2))
| ~ m2_cat_1(X5,X0,k11_cat_2(X1,X2))
| ~ m2_nattra_1(X6,X0,k11_cat_2(X1,X2),X3,X4)
| ~ v2_cat_1(X0)
| k13_isocat_2(X0,X1,X2,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7)) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X5,k8_nattra_1(X0,k11_cat_2(X1,X2),X3,X4,X5,X6,X7),k8_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f43630,f34775]) ).
fof(f43876,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43635,f34718]) ).
fof(f43877,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43636,f34718]) ).
fof(f43878,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43637,f34718]) ).
fof(f43881,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43640,f34718]) ).
fof(f43882,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43641,f34718]) ).
fof(f43883,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43642,f34718]) ).
fof(f44100,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43866,f34719]) ).
fof(f44101,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43867,f34719]) ).
fof(f44102,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43868,f34719]) ).
fof(f44103,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43869,f34719]) ).
fof(f44106,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43876,f34717]) ).
fof(f44107,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43877,f34717]) ).
fof(f44108,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43878,f34717]) ).
fof(f44109,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43881,f34717]) ).
fof(f44110,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43882,f34717]) ).
fof(f44111,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f43883,f34717]) ).
fof(f44118,definition,
( spl921_27
<=> l1_cat_1(k11_cat_2(sK99,sK100)) ),
introduced(definition,[new_symbols(definition,[spl921_27])],[avatar_definition]) ).
fof(f44119,plain,
( l1_cat_1(k11_cat_2(sK99,sK100))
| ~ spl921_27 ),
inference(avatar_component_clause,[],[f44118]) ).
fof(f44120,plain,
( ~ l1_cat_1(k11_cat_2(sK99,sK100))
| spl921_27 ),
inference(avatar_component_clause,[],[f44118]) ).
fof(f44122,definition,
( spl921_28
<=> v2_cat_1(k11_cat_2(sK99,sK100)) ),
introduced(definition,[new_symbols(definition,[spl921_28])],[avatar_definition]) ).
fof(f44123,plain,
( v2_cat_1(k11_cat_2(sK99,sK100))
| ~ spl921_28 ),
inference(avatar_component_clause,[],[f44122]) ).
fof(f44124,plain,
( ~ v2_cat_1(k11_cat_2(sK99,sK100))
| spl921_28 ),
inference(avatar_component_clause,[],[f44122]) ).
fof(f44248,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44100,f34718]) ).
fof(f44249,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44101,f34718]) ).
fof(f44250,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44102,f34718]) ).
fof(f44251,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44103,f34718]) ).
fof(f44254,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44106,f34716]) ).
fof(f44255,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44107,f34716]) ).
fof(f44256,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44108,f34716]) ).
fof(f44257,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44109,f34716]) ).
fof(f44258,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44110,f34716]) ).
fof(f44259,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44111,f34716]) ).
fof(f44322,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44248,f34717]) ).
fof(f44323,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44249,f34717]) ).
fof(f44324,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44250,f34717]) ).
fof(f44325,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44251,f34717]) ).
fof(f44328,plain,
( k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44254,f34715]) ).
fof(f44329,plain,
( k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44255,f34715]) ).
fof(f44330,plain,
( k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44256,f34715]) ).
fof(f44331,plain,
( k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44257,f34715]) ).
fof(f44332,plain,
( k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44258,f34715]) ).
fof(f44333,plain,
( k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44259,f34715]) ).
fof(f44399,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44322,f34716]) ).
fof(f44400,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44323,f34716]) ).
fof(f44401,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44324,f34716]) ).
fof(f44402,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44325,f34716]) ).
fof(f44411,plain,
k12_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44328,f34714]) ).
fof(f44412,plain,
k12_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44329,f34714]) ).
fof(f44413,plain,
k12_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44330,f34714]) ).
fof(f44414,plain,
k11_isocat_2(sK98,sK99,sK100,sK102) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44331,f34714]) ).
fof(f44415,plain,
k11_isocat_2(sK98,sK99,sK100,sK103) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44332,f34714]) ).
fof(f44416,plain,
k11_isocat_2(sK98,sK99,sK100,sK101) = k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44333,f34714]) ).
fof(f44479,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44399,f34715]) ).
fof(f44480,plain,
( k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44400,f34715]) ).
fof(f44481,plain,
( k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44401,f34715]) ).
fof(f44482,plain,
( k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98) ),
inference(forward_subsumption_resolution,[],[f44402,f34715]) ).
fof(f44483,plain,
k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44479,f34714]) ).
fof(f44484,plain,
k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44480,f34714]) ).
fof(f44485,plain,
k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44481,f34714]) ).
fof(f44486,plain,
k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f44482,f34714]) ).
fof(f44487,plain,
( ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_27 ),
inference(resolution,[],[f44120,f34775]) ).
fof(f44488,plain,
( ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_27 ),
inference(forward_subsumption_resolution,[],[f44487,f34717]) ).
fof(f44489,plain,
( ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_27 ),
inference(forward_subsumption_resolution,[],[f44488,f34716]) ).
fof(f44490,plain,
( ~ l1_cat_1(sK100)
| spl921_27 ),
inference(forward_subsumption_resolution,[],[f44489,f34719]) ).
fof(f44491,plain,
( $false
| spl921_27 ),
inference(forward_subsumption_resolution,[],[f44490,f34718]) ).
fof(f44492,plain,
spl921_27,
inference(avatar_contradiction_clause,[],[f44491]) ).
fof(f44493,plain,
( ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_28 ),
inference(resolution,[],[f44124,f38324]) ).
fof(f44494,plain,
( ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_28 ),
inference(forward_subsumption_resolution,[],[f44493,f34717]) ).
fof(f44495,plain,
( ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_28 ),
inference(forward_subsumption_resolution,[],[f44494,f34716]) ).
fof(f44496,plain,
( ~ l1_cat_1(sK100)
| spl921_28 ),
inference(forward_subsumption_resolution,[],[f44495,f34719]) ).
fof(f44497,plain,
( $false
| spl921_28 ),
inference(forward_subsumption_resolution,[],[f44496,f34718]) ).
fof(f44498,plain,
spl921_28,
inference(avatar_contradiction_clause,[],[f44497]) ).
fof(f44778,definition,
( spl921_63
<=> m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99) ),
introduced(definition,[new_symbols(definition,[spl921_63])],[avatar_definition]) ).
fof(f44779,plain,
( m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ spl921_63 ),
inference(avatar_component_clause,[],[f44778]) ).
fof(f44780,plain,
( ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| spl921_63 ),
inference(avatar_component_clause,[],[f44778]) ).
fof(f44821,plain,
( ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_63 ),
inference(resolution,[],[f44780,f36174]) ).
fof(f44822,plain,
( ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_63 ),
inference(forward_subsumption_resolution,[],[f44821,f34717]) ).
fof(f44823,plain,
( ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_63 ),
inference(forward_subsumption_resolution,[],[f44822,f34716]) ).
fof(f44824,plain,
( ~ l1_cat_1(sK100)
| spl921_63 ),
inference(forward_subsumption_resolution,[],[f44823,f34719]) ).
fof(f44825,plain,
( $false
| spl921_63 ),
inference(forward_subsumption_resolution,[],[f44824,f34718]) ).
fof(f44826,plain,
spl921_63,
inference(avatar_contradiction_clause,[],[f44825]) ).
fof(f45057,definition,
( spl921_71
<=> m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100) ),
introduced(definition,[new_symbols(definition,[spl921_71])],[avatar_definition]) ).
fof(f45058,plain,
( m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ spl921_71 ),
inference(avatar_component_clause,[],[f45057]) ).
fof(f45059,plain,
( ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| spl921_71 ),
inference(avatar_component_clause,[],[f45057]) ).
fof(f45100,plain,
( ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_71 ),
inference(resolution,[],[f45059,f36176]) ).
fof(f45101,plain,
( ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_71 ),
inference(forward_subsumption_resolution,[],[f45100,f34717]) ).
fof(f45102,plain,
( ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| spl921_71 ),
inference(forward_subsumption_resolution,[],[f45101,f34716]) ).
fof(f45103,plain,
( ~ l1_cat_1(sK100)
| spl921_71 ),
inference(forward_subsumption_resolution,[],[f45102,f34719]) ).
fof(f45104,plain,
( $false
| spl921_71 ),
inference(forward_subsumption_resolution,[],[f45103,f34718]) ).
fof(f45105,plain,
spl921_71,
inference(avatar_contradiction_clause,[],[f45104]) ).
fof(f45252,plain,
! [X0,X1] :
( ~ l1_cat_1(sK98)
| ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| ~ v2_cat_1(sK98)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(resolution,[],[f43871,f34726]) ).
fof(f45274,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| ~ v2_cat_1(sK98)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45252,f34714]) ).
fof(f45283,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| ~ v2_cat_1(sK98)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45274,f34721]) ).
fof(f45287,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| ~ v2_cat_1(sK98)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45283,f34722]) ).
fof(f45291,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45287,f34715]) ).
fof(f45293,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45291,f34719]) ).
fof(f45295,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45293,f34718]) ).
fof(f45297,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105))
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f45295,f34717]) ).
fof(f45299,plain,
! [X0,X1] :
( ~ m2_nattra_1(X1,sK98,k11_cat_2(sK99,sK100),X0,sK102)
| ~ m2_cat_1(X0,sK98,k11_cat_2(sK99,sK100))
| k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105),k8_isocat_2(sK99,sK100)) = k13_isocat_2(sK98,sK99,sK100,X0,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),X0,sK102,sK103,X1,sK105)) ),
inference(forward_subsumption_resolution,[],[f45297,f34716]) ).
fof(f49123,plain,
( ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k8_isocat_2(sK99,sK100)) ),
inference(resolution,[],[f45299,f34725]) ).
fof(f49127,plain,
k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k8_isocat_2(sK99,sK100)),
inference(forward_subsumption_resolution,[],[f49123,f34720]) ).
fof(f49132,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(superposition,[],[f34785,f49127]) ).
fof(f49147,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f49132,f34724]) ).
fof(f49155,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f49147,f34723]) ).
fof(f49163,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f49155,f34726]) ).
fof(f49171,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_cat_1(k8_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK99)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99) ),
inference(forward_subsumption_resolution,[],[f49163,f34725]) ).
fof(f49179,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49171,f44779]) ).
fof(f49187,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49179,f34722]) ).
fof(f49195,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49187,f34721]) ).
fof(f49203,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49195,f34720]) ).
fof(f49211,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49203,f44123]) ).
fof(f49219,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49211,f44119]) ).
fof(f49222,definition,
( spl921_158
<=> m2_nattra_1(k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),sK98,k11_cat_2(sK99,sK100),sK101,sK103) ),
introduced(definition,[new_symbols(definition,[spl921_158])],[avatar_definition]) ).
fof(f49223,plain,
( m2_nattra_1(k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),sK98,k11_cat_2(sK99,sK100),sK101,sK103)
| ~ spl921_158 ),
inference(avatar_component_clause,[],[f49222]) ).
fof(f49224,plain,
( ~ m2_nattra_1(k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),sK98,k11_cat_2(sK99,sK100),sK101,sK103)
| spl921_158 ),
inference(avatar_component_clause,[],[f49222]) ).
fof(f49235,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49219,f34715]) ).
fof(f49246,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49235,f34714]) ).
fof(f49267,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ l1_cat_1(sK99)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49246,f34717]) ).
fof(f49268,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,sK103,sK105,k8_isocat_2(sK99,sK100))))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49267,f34716]) ).
fof(f49269,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,sK102,sK104,k8_isocat_2(sK99,sK100)),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_demodulation,[],[f49268,f44486]) ).
fof(f49270,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK103,k8_isocat_2(sK99,sK100)),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_demodulation,[],[f49269,f44484]) ).
fof(f49271,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK102,k8_isocat_2(sK99,sK100)),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_demodulation,[],[f49270,f44415]) ).
fof(f49272,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK99,sK101,k8_isocat_2(sK99,sK100)),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_demodulation,[],[f49271,f44414]) ).
fof(f49273,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK99),u1_cat_1(sK98),u2_cat_1(sK99),k13_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK99,k11_isocat_2(sK98,sK99,sK100,sK101),k11_isocat_2(sK98,sK99,sK100,sK102),k11_isocat_2(sK98,sK99,sK100,sK103),k13_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k13_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_demodulation,[],[f49272,f44416]) ).
fof(f49274,plain,
( $false
| spl921_20
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(forward_subsumption_resolution,[],[f49273,f42717]) ).
fof(f49275,plain,
( spl921_20
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(avatar_contradiction_clause,[],[f49274]) ).
fof(f49276,plain,
( ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| spl921_158 ),
inference(resolution,[],[f49224,f34786]) ).
fof(f49277,plain,
( ~ l1_cat_1(sK98)
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49276,f34715]) ).
fof(f49278,plain,
( ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49277,f34714]) ).
fof(f49279,plain,
( ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49278,f44123]) ).
fof(f49280,plain,
( ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49279,f44119]) ).
fof(f49281,plain,
( ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49280,f34720]) ).
fof(f49282,plain,
( ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49281,f34721]) ).
fof(f49283,plain,
( ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49282,f34722]) ).
fof(f49284,plain,
( ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49283,f34725]) ).
fof(f49285,plain,
( $false
| ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(forward_subsumption_resolution,[],[f49284,f34726]) ).
fof(f49286,plain,
( ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(avatar_contradiction_clause,[],[f49285]) ).
fof(f49292,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(resolution,[],[f49223,f34807]) ).
fof(f49315,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49292,f34722]) ).
fof(f49331,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49315,f34720]) ).
fof(f49347,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK100)
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49331,f34719]) ).
fof(f49363,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK99)
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49347,f34718]) ).
fof(f49379,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK99)
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49363,f34717]) ).
fof(f49395,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49379,f34716]) ).
fof(f49409,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ l1_cat_1(sK98)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49395,f34715]) ).
fof(f49414,plain,
( k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)) = k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105),k9_isocat_2(sK99,sK100))
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49409,f34714]) ).
fof(f49817,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_158 ),
inference(superposition,[],[f34785,f49414]) ).
fof(f49832,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ r2_nattra_1(sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49817,f34724]) ).
fof(f49840,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_nattra_1(sK105,sK98,k11_cat_2(sK99,sK100),sK102,sK103)
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49832,f34723]) ).
fof(f49848,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_nattra_1(sK104,sK98,k11_cat_2(sK99,sK100),sK101,sK102)
| ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49840,f34726]) ).
fof(f49856,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_cat_1(k9_isocat_2(sK99,sK100),k11_cat_2(sK99,sK100),sK100)
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49848,f34725]) ).
fof(f49864,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK103,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49856,f45058]) ).
fof(f49872,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK102,sK98,k11_cat_2(sK99,sK100))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49864,f34722]) ).
fof(f49880,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ m2_cat_1(sK101,sK98,k11_cat_2(sK99,sK100))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49872,f34721]) ).
fof(f49888,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ v2_cat_1(k11_cat_2(sK99,sK100))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49880,f34720]) ).
fof(f49896,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ l1_cat_1(k11_cat_2(sK99,sK100))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49888,f44123]) ).
fof(f49904,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ v2_cat_1(sK98)
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49896,f44119]) ).
fof(f49912,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ l1_cat_1(sK98)
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49904,f34715]) ).
fof(f49919,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ v2_cat_1(sK100)
| ~ l1_cat_1(sK100)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49912,f34714]) ).
fof(f49925,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ l1_cat_1(sK100)
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49919,f34719]) ).
fof(f49926,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,sK103,sK105,k9_isocat_2(sK99,sK100))))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49925,f34718]) ).
fof(f49927,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k6_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,sK102,sK104,k9_isocat_2(sK99,sK100)),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_demodulation,[],[f49926,f44485]) ).
fof(f49928,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK103,k9_isocat_2(sK99,sK100)),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_demodulation,[],[f49927,f44483]) ).
fof(f49929,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK102,k9_isocat_2(sK99,sK100)),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_demodulation,[],[f49928,f44412]) ).
fof(f49930,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k2_isocat_1(sK98,k11_cat_2(sK99,sK100),sK100,sK101,k9_isocat_2(sK99,sK100)),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_demodulation,[],[f49929,f44411]) ).
fof(f49931,plain,
( r4_nattra_1(u1_cat_1(sK98),u2_cat_1(sK100),u1_cat_1(sK98),u2_cat_1(sK100),k14_isocat_2(sK98,sK99,sK100,sK101,sK103,k8_nattra_1(sK98,k11_cat_2(sK99,sK100),sK101,sK102,sK103,sK104,sK105)),k8_nattra_1(sK98,sK100,k12_isocat_2(sK98,sK99,sK100,sK101),k12_isocat_2(sK98,sK99,sK100,sK102),k12_isocat_2(sK98,sK99,sK100,sK103),k14_isocat_2(sK98,sK99,sK100,sK101,sK102,sK104),k14_isocat_2(sK98,sK99,sK100,sK102,sK103,sK105)))
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_demodulation,[],[f49930,f44413]) ).
fof(f49932,plain,
( $false
| spl921_19
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(forward_subsumption_resolution,[],[f49931,f42713]) ).
fof(f49933,plain,
( spl921_19
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(avatar_contradiction_clause,[],[f49932]) ).
cnf(s19,plain,
( ~ spl921_19
| ~ spl921_20 ),
inference(sat_conversion,[],[f42718]) ).
cnf(s66,plain,
spl921_27,
inference(sat_conversion,[],[f44492]) ).
cnf(s67,plain,
spl921_28,
inference(sat_conversion,[],[f44498]) ).
cnf(s75,plain,
spl921_63,
inference(sat_conversion,[],[f44826]) ).
cnf(s83,plain,
spl921_71,
inference(sat_conversion,[],[f45105]) ).
cnf(s146,plain,
( spl921_20
| ~ spl921_27
| ~ spl921_28
| ~ spl921_63 ),
inference(sat_conversion,[],[f49275]) ).
cnf(s147,plain,
( ~ spl921_27
| ~ spl921_28
| spl921_158 ),
inference(sat_conversion,[],[f49286]) ).
cnf(s159,plain,
( spl921_19
| ~ spl921_27
| ~ spl921_28
| ~ spl921_71
| ~ spl921_158 ),
inference(sat_conversion,[],[f49933]) ).
cnf(s214,plain,
spl921_158,
inference(rat,[],[s147,s67,s66]) ).
cnf(s215,plain,
spl921_20,
inference(rat,[],[s146,s75,s67,s66]) ).
cnf(s233,plain,
spl921_19,
inference(rat,[],[s159,s66,s83,s67,s214]) ).
cnf(s325,plain,
$false,
inference(rat,[],[s19,s215,s233]) ).
fof(f49934,plain,
$false,
inference(avatar_sat_refutation,[],[s325]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT028+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n007.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 21:17:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 11.63/2.89 % (2842873)Detected formulas, will run a generic FOF schedule.
% 11.63/2.89 % (2842884)dis-21_1_sil=8000:lcm=predicate:random_seed=759375048:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 11.63/2.89 % (2842878)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=1594031073:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 11.63/2.89 % (2842883)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1971242061:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 11.63/2.89 % (2842882)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2796721170:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 11.63/2.89 % (2842881)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=130841839:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 11.63/2.89 % (2842879)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=227655992:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 11.63/2.89 % (2842880)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=1900536986:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 11.63/2.89 % (2842884)Instruction limit reached!
% 11.63/2.89 % (2842884)------------------------------
% 11.63/2.89 % (2842884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.89 % (2842884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.89 % (2842884)CaDiCaL version: 2.1.3
% 11.63/2.89 % (2842884)Termination reason: Instruction limit
% 11.63/2.89 % (2842884)Termination phase: SInE selection
% 11.63/2.89 % (2842884)Time elapsed: 0.055 s
% 11.63/2.89 % (2842884)Peak memory usage: 127 MB
% 11.63/2.89 % (2842884)Instructions burned: 132 (million)
% 11.63/2.89 % (2842883)Instruction limit reached!
% 11.63/2.89 % (2842883)------------------------------
% 11.63/2.89 % (2842883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.89 % (2842883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.89 % (2842883)CaDiCaL version: 2.1.3
% 11.63/2.89 % (2842883)Termination reason: Instruction limit
% 11.63/2.89 % (2842883)Termination phase: Property scanning
% 11.63/2.89 % (2842883)Time elapsed: 0.059 s
% 11.63/2.89 % (2842883)Peak memory usage: 127 MB
% 11.63/2.89 % (2842883)Instructions burned: 139 (million)
% 11.63/2.89 % (2842881)Instruction limit reached!
% 11.63/2.89 % (2842881)------------------------------
% 11.63/2.89 % (2842881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.89 % (2842881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.89 % (2842881)CaDiCaL version: 2.1.3
% 11.63/2.89 % (2842881)Termination reason: Instruction limit
% 11.63/2.89 % (2842881)Termination phase: SInE selection
% 11.63/2.89 % (2842881)Time elapsed: 0.081 s
% 11.63/2.89 % (2842881)Peak memory usage: 126 MB
% 11.63/2.89 % (2842881)Instructions burned: 109 (million)
% 11.63/2.89 % (2842882)Instruction limit reached!
% 11.63/2.89 % (2842882)------------------------------
% 11.63/2.89 % (2842882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.89 % (2842882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.89 % (2842882)CaDiCaL version: 2.1.3
% 11.63/2.89 % (2842882)Termination reason: Instruction limit
% 11.63/2.89 % (2842882)Termination phase: SInE selection
% 11.63/2.89 % (2842882)Time elapsed: 0.088 s
% 11.63/2.89 % (2842882)Peak memory usage: 126 MB
% 11.63/2.89 % (2842882)Instructions burned: 119 (million)
% 11.63/2.89 % (2842892)lrs+10_1_sil=8000:sp=occurrence:random_seed=141515854:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 11.63/2.89 % (2842893)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3681290000:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 11.63/2.89 % (2842894)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2322289998:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 11.63/2.89 % (2842895)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=2025384440:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 11.63/2.89 % (2842893)Instruction limit reached!
% 19.77/3.96 % (2842893)------------------------------
% 19.77/3.96 % (2842893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842893)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842893)Termination reason: Instruction limit
% 19.77/3.96 % (2842893)Termination phase: Property scanning
% 19.77/3.96 % (2842893)Time elapsed: 0.069 s
% 19.77/3.96 % (2842893)Peak memory usage: 127 MB
% 19.77/3.96 % (2842893)Instructions burned: 159 (million)
% 19.77/3.96 % (2842892)Instruction limit reached!
% 19.77/3.96 % (2842892)------------------------------
% 19.77/3.96 % (2842892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842892)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842892)Termination reason: Instruction limit
% 19.77/3.96 % (2842892)Termination phase: Saturation
% 19.77/3.96 % (2842892)Time elapsed: 0.122 s
% 19.77/3.96 % (2842892)Peak memory usage: 133 MB
% 19.77/3.96 % (2842892)Instructions burned: 286 (million)
% 19.77/3.96 % (2842895)Instruction limit reached!
% 19.77/3.96 % (2842895)------------------------------
% 19.77/3.96 % (2842895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842895)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842895)Termination reason: Instruction limit
% 19.77/3.96 % (2842895)Termination phase: Property scanning
% 19.77/3.96 % (2842895)Time elapsed: 0.107 s
% 19.77/3.96 % (2842895)Peak memory usage: 127 MB
% 19.77/3.96 % (2842895)Instructions burned: 249 (million)
% 19.77/3.96 % (2842901)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1742850356:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 19.77/3.96 % (2842900)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3103353057:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 19.77/3.96 % (2842894)Instruction limit reached!
% 19.77/3.96 % (2842894)------------------------------
% 19.77/3.96 % (2842894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842894)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842894)Termination reason: Instruction limit
% 19.77/3.96 % (2842894)Termination phase: Saturation
% 19.77/3.96 % (2842894)Time elapsed: 0.246 s
% 19.77/3.96 % (2842894)Peak memory usage: 133 MB
% 19.77/3.96 % (2842894)Instructions burned: 325 (million)
% 19.77/3.96 % (2842902)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1134982735:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.77/3.96 % (2842902)Instruction limit reached!
% 19.77/3.96 % (2842902)------------------------------
% 19.77/3.96 % (2842902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842902)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842902)Termination reason: Instruction limit
% 19.77/3.96 % (2842902)Termination phase: SInE selection
% 19.77/3.96 % (2842902)Time elapsed: 0.089 s
% 19.77/3.96 % (2842902)Peak memory usage: 127 MB
% 19.77/3.96 % (2842902)Instructions burned: 114 (million)
% 19.77/3.96 % (2842900)Instruction limit reached!
% 19.77/3.96 % (2842900)------------------------------
% 19.77/3.96 % (2842900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842900)CaDiCaL version: 2.1.3
% 19.77/3.96 % (2842900)Termination reason: Instruction limit
% 19.77/3.96 % (2842900)Termination phase: Preprocessing 3
% 19.77/3.96 % (2842900)Time elapsed: 0.216 s
% 19.77/3.96 % (2842900)Peak memory usage: 130 MB
% 19.77/3.96 % (2842900)Instructions burned: 294 (million)
% 19.77/3.96 % (2842905)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3696296727:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 19.77/3.96 % (2842905)Instruction limit reached!
% 19.77/3.96 % (2842905)------------------------------
% 19.77/3.96 % (2842905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.77/3.96 % (2842905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.77/3.96 % (2842905)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842905)Termination reason: Instruction limit
% 11.21/5.07 % (2842905)Termination phase: Preprocessing 1
% 11.21/5.07 % (2842905)Time elapsed: 0.095 s
% 11.21/5.07 % (2842905)Peak memory usage: 128 MB
% 11.21/5.07 % (2842905)Instructions burned: 128 (million)
% 11.21/5.07 % (2842907)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=686769746:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 11.21/5.07 % (2842909)lrs+10_1_sil=8000:sp=occurrence:random_seed=1308449048:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 11.21/5.07 % (2842907)Instruction limit reached!
% 11.21/5.07 % (2842907)------------------------------
% 11.21/5.07 % (2842907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842907)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842907)Termination reason: Instruction limit
% 11.21/5.07 % (2842907)Termination phase: Property scanning
% 11.21/5.07 % (2842907)Time elapsed: 0.052 s
% 11.21/5.07 % (2842907)Peak memory usage: 127 MB
% 11.21/5.07 % (2842907)Instructions burned: 114 (million)
% 11.21/5.07 % (2842910)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3567625619:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 11.21/5.07 % (2842913)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=734191857:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 11.21/5.07 % (2842901)Instruction limit reached!
% 11.21/5.07 % (2842901)------------------------------
% 11.21/5.07 % (2842901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842901)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842901)Termination reason: Instruction limit
% 11.21/5.07 % (2842901)Termination phase: Property scanning
% 11.21/5.07 % (2842901)Time elapsed: 0.787 s
% 11.21/5.07 % (2842901)Peak memory usage: 208 MB
% 11.21/5.07 % (2842901)Instructions burned: 2354 (million)
% 11.21/5.07 % (2842910)Instruction limit reached!
% 11.21/5.07 % (2842910)------------------------------
% 11.21/5.07 % (2842910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842910)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842910)Termination reason: Instruction limit
% 11.21/5.07 % (2842910)Termination phase: Saturation
% 11.21/5.07 % (2842910)Time elapsed: 0.293 s
% 11.21/5.07 % (2842910)Peak memory usage: 134 MB
% 11.21/5.07 % (2842910)Instructions burned: 438 (million)
% 11.21/5.07 % (2842916)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=939966318:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 11.21/5.07 % (2842916)Instruction limit reached!
% 11.21/5.07 % (2842916)------------------------------
% 11.21/5.07 % (2842916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842916)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842916)Termination reason: Instruction limit
% 11.21/5.07 % (2842916)Termination phase: SInE selection
% 11.21/5.07 % (2842916)Time elapsed: 0.059 s
% 11.21/5.07 % (2842916)Peak memory usage: 127 MB
% 11.21/5.07 % (2842916)Instructions burned: 135 (million)
% 11.21/5.07 % (2842909)Instruction limit reached!
% 11.21/5.07 % (2842909)------------------------------
% 11.21/5.07 % (2842909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842909)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842909)Termination reason: Instruction limit
% 11.21/5.07 % (2842909)Termination phase: Equality resolution with deletion
% 11.21/5.07 % (2842909)Time elapsed: 0.576 s
% 11.21/5.07 % (2842909)Peak memory usage: 149 MB
% 11.21/5.07 % (2842909)Instructions burned: 908 (million)
% 11.21/5.07 % (2842917)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=958604931:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 11.21/5.07 % (2842919)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=653681825:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 11.21/5.07 % (2842921)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=2901409165:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 11.21/5.07 % (2842921)Instruction limit reached!
% 11.21/5.07 % (2842921)------------------------------
% 11.21/5.07 % (2842921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842921)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842921)Termination reason: Instruction limit
% 11.21/5.07 % (2842921)Termination phase: Property scanning
% 11.21/5.07 % (2842921)Time elapsed: 0.057 s
% 11.21/5.07 % (2842921)Peak memory usage: 127 MB
% 11.21/5.07 % (2842921)Instructions burned: 127 (million)
% 11.21/5.07 % (2842924)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=830793733:i=134:gtgl=5:slsql=off:gtg=exists_sym_2974 on theBenchmark for (2974ds/134Mi)
% 11.21/5.07 % (2842924)Instruction limit reached!
% 11.21/5.07 % (2842924)------------------------------
% 11.21/5.07 % (2842924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842924)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842924)Termination reason: Instruction limit
% 11.21/5.07 % (2842924)Termination phase: Property scanning
% 11.21/5.07 % (2842924)Time elapsed: 0.060 s
% 11.21/5.07 % (2842924)Peak memory usage: 127 MB
% 11.21/5.07 % (2842924)Instructions burned: 134 (million)
% 11.21/5.07 % (2842917)Instruction limit reached!
% 11.21/5.07 % (2842917)------------------------------
% 11.21/5.07 % (2842917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842917)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842917)Termination reason: Instruction limit
% 11.21/5.07 % (2842917)Termination phase: Preprocessing 3
% 11.21/5.07 % (2842917)Time elapsed: 0.467 s
% 11.21/5.07 % (2842917)Peak memory usage: 146 MB
% 11.21/5.07 % (2842917)Instructions burned: 592 (million)
% 11.21/5.07 % (2842927)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2966106899:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 11.21/5.07 % (2842926)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1018751506:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 11.21/5.07 % (2842926)Instruction limit reached!
% 11.21/5.07 % (2842926)------------------------------
% 11.21/5.07 % (2842926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842926)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842926)Termination reason: Instruction limit
% 11.21/5.07 % (2842926)Termination phase: SInE selection
% 11.21/5.07 % (2842926)Time elapsed: 0.105 s
% 11.21/5.07 % (2842926)Peak memory usage: 126 MB
% 11.21/5.07 % (2842926)Instructions burned: 142 (million)
% 11.21/5.07 % (2842930)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2873507772:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 11.21/5.07 % (2842927)Instruction limit reached!
% 11.21/5.07 % (2842927)------------------------------
% 11.21/5.07 % (2842927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842927)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842927)Termination reason: Instruction limit
% 11.21/5.07 % (2842927)Termination phase: Saturation
% 11.21/5.07 % (2842927)Time elapsed: 0.297 s
% 11.21/5.07 % (2842927)Peak memory usage: 135 MB
% 11.21/5.07 % (2842927)Instructions burned: 432 (million)
% 11.21/5.07 % (2842932)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4053165427:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 11.21/5.07 % (2842932)Instruction limit reached!
% 11.21/5.07 % (2842932)------------------------------
% 11.21/5.07 % (2842932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/5.07 % (2842932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/5.07 % (2842932)CaDiCaL version: 2.1.3
% 11.21/5.07 % (2842932)Termination reason: Instruction limit
% 11.21/5.07 % (2842932)Termination phase: SInE selection
% 11.21/5.07 % (2842932)Time elapsed: 0.119 s
% 11.21/5.07 % (2842932)Peak memory usage: 127 MB
% 11.21/5.07 % (2842932)Instructions burned: 151 (million)
% 11.21/5.07 % (2842934)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2569197651:i=14155:bd=all_2964 on theBenchmark for (2964ds/14155Mi)
% 11.21/5.07 % (2842919)First to succeed.
% 11.21/5.07 % (2842919)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2842873"
% 11.21/5.07 % (2842919)Refutation found. Thanks to Tanya!
% 11.21/5.07 % SZS status Theorem for theBenchmark
% 11.21/5.07 % SZS output start Proof for theBenchmark
% See solution above
% 28.70/5.18 % (2842919)------------------------------
% 28.70/5.18 % (2842919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.70/5.18 % (2842919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.70/5.18 % (2842919)CaDiCaL version: 2.1.3
% 28.70/5.18 % (2842919)Termination reason: Refutation
% 28.70/5.18 % (2842919)Time elapsed: 1.994 s
% 28.70/5.18 % (2842919)Peak memory usage: 253 MB
% 28.70/5.18 % (2842919)Instructions burned: 5973 (million)
% 28.70/5.18 % (2842919)------------------------------
% 28.70/5.18 % (2842919)------------------------------
% 28.70/5.18 % (2842873)Success in time 4.634 s
% 28.70/5.18 % Vampire exiting
%------------------------------------------------------------------------------