%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT028+3 : 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 : n012.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 16.17s 5.84s
% Output : Refutation 34.83s
% 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(f8299,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_cat_2) ).
fof(f8397,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f10544,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(f11391,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(f11735,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f11737,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f11791,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f11792,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f11795,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_isocat_2) ).
fof(f11796,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ! [X5] :
( m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4)
=> k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_isocat_2) ).
fof(f11800,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(f11801,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)],[f11800]) ).
fof(f11958,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,[],[f11801]) ).
fof(f11959,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,[],[f11958]) ).
fof(f12002,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f8397]) ).
fof(f12003,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,[],[f12002]) ).
fof(f12020,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,[],[f11391]) ).
fof(f12021,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,[],[f12020]) ).
fof(f12022,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,[],[f10544]) ).
fof(f12023,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,[],[f12022]) ).
fof(f12040,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f11791]) ).
fof(f12041,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,[],[f12040]) ).
fof(f12046,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f11792]) ).
fof(f12047,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,[],[f12046]) ).
fof(f12054,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k13_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,X4,X5,k8_isocat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f11795]) ).
fof(f12055,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,[],[f12054]) ).
fof(f12056,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k14_isocat_2(X0,X1,X2,X3,X4,X5) = k6_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,X4,X5,k9_isocat_2(X1,X2))
| ~ m2_nattra_1(X5,X0,k11_cat_2(X1,X2),X3,X4) )
| ~ m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f11796]) ).
fof(f12057,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,[],[f12056]) ).
fof(f12864,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f11735]) ).
fof(f12865,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,[],[f12864]) ).
fof(f12868,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f11737]) ).
fof(f12869,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,[],[f12868]) ).
fof(f13685,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f8299]) ).
fof(f13686,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,[],[f13685]) ).
fof(f15116,plain,
( ( ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k11_isocat_2(sK58,sK59,sK60,sK61),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k12_isocat_2(sK58,sK59,sK60,sK61),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65))) )
& m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
& m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
& r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62)
& r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63)
& m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
& m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
& m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
& v2_cat_1(sK60)
& l1_cat_1(sK60)
& v2_cat_1(sK59)
& l1_cat_1(sK59)
& v2_cat_1(sK58)
& l1_cat_1(sK58) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58,sK59,sK60,sK61,sK62,sK63,sK64,sK65]),skolemize(X0,sK58),skolemize(X1,sK59),skolemize(X2,sK60),skolemize(X3,sK61),skolemize(X4,sK62),skolemize(X5,sK63),skolemize(X6,sK64),skolemize(X7,sK65)],[f11959]) ).
fof(f16002,plain,
l1_cat_1(sK58),
inference(cnf_transformation,[],[f15116]) ).
fof(f16003,plain,
v2_cat_1(sK58),
inference(cnf_transformation,[],[f15116]) ).
fof(f16004,plain,
l1_cat_1(sK59),
inference(cnf_transformation,[],[f15116]) ).
fof(f16005,plain,
v2_cat_1(sK59),
inference(cnf_transformation,[],[f15116]) ).
fof(f16006,plain,
l1_cat_1(sK60),
inference(cnf_transformation,[],[f15116]) ).
fof(f16007,plain,
v2_cat_1(sK60),
inference(cnf_transformation,[],[f15116]) ).
fof(f16008,plain,
m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60)),
inference(cnf_transformation,[],[f15116]) ).
fof(f16009,plain,
m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60)),
inference(cnf_transformation,[],[f15116]) ).
fof(f16010,plain,
m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60)),
inference(cnf_transformation,[],[f15116]) ).
fof(f16011,plain,
r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63),
inference(cnf_transformation,[],[f15116]) ).
fof(f16012,plain,
r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62),
inference(cnf_transformation,[],[f15116]) ).
fof(f16013,plain,
m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62),
inference(cnf_transformation,[],[f15116]) ).
fof(f16014,plain,
m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63),
inference(cnf_transformation,[],[f15116]) ).
fof(f16015,plain,
( ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k11_isocat_2(sK58,sK59,sK60,sK61),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k12_isocat_2(sK58,sK59,sK60,sK61),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65))) ),
inference(cnf_transformation,[],[f15116]) ).
fof(f16061,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,[],[f12003]) ).
fof(f16071,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,[],[f12021]) ).
fof(f16072,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,[],[f12023]) ).
fof(f16085,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,[],[f12041]) ).
fof(f16088,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,[],[f12047]) ).
fof(f16092,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,[],[f12055]) ).
fof(f16093,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,[],[f12057]) ).
fof(f17241,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,[],[f12865]) ).
fof(f17243,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,[],[f12869]) ).
fof(f18145,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,[],[f13686]) ).
fof(f21371,definition,
( spl606_13
<=> r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k12_isocat_2(sK58,sK59,sK60,sK61),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65))) ),
introduced(definition,[new_symbols(definition,[spl606_13])],[avatar_definition]) ).
fof(f21373,plain,
( ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k12_isocat_2(sK58,sK59,sK60,sK61),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| spl606_13 ),
inference(avatar_component_clause,[],[f21371]) ).
fof(f21375,definition,
( spl606_14
<=> r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k11_isocat_2(sK58,sK59,sK60,sK61),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65))) ),
introduced(definition,[new_symbols(definition,[spl606_14])],[avatar_definition]) ).
fof(f21377,plain,
( ~ r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k11_isocat_2(sK58,sK59,sK60,sK61),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| spl606_14 ),
inference(avatar_component_clause,[],[f21375]) ).
fof(f21378,plain,
( ~ spl606_13
| ~ spl606_14 ),
inference(avatar_split_clause,[],[f16015,f21375,f21371]) ).
fof(f21550,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16013,f16093]) ).
fof(f21551,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16013,f16092]) ).
fof(f21552,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16014,f16093]) ).
fof(f21553,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16014,f16092]) ).
fof(f21555,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,[],[f16072,f16092]) ).
fof(f21556,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,[],[f21555]) ).
fof(f21560,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16085,f16008]) ).
fof(f21561,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16085,f16010]) ).
fof(f21566,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16088,f16008]) ).
fof(f21567,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16088,f16010]) ).
fof(f21574,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16009,f16088]) ).
fof(f21575,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(resolution,[],[f16009,f16085]) ).
fof(f22158,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21551,f16009]) ).
fof(f22159,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21550,f16009]) ).
fof(f22160,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21553,f16010]) ).
fof(f22161,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21552,f16010]) ).
fof(f22162,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,[],[f21556,f18145]) ).
fof(f22164,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21561,f16007]) ).
fof(f22165,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21560,f16007]) ).
fof(f22168,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21567,f16007]) ).
fof(f22169,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21566,f16007]) ).
fof(f22174,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21575,f16007]) ).
fof(f22175,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f21574,f16007]) ).
fof(f22398,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22158,f16008]) ).
fof(f22399,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22159,f16008]) ).
fof(f22400,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22160,f16009]) ).
fof(f22401,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22161,f16009]) ).
fof(f22402,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,[],[f22162,f16061]) ).
fof(f22404,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22164,f16006]) ).
fof(f22405,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22165,f16006]) ).
fof(f22408,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22168,f16006]) ).
fof(f22409,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22169,f16006]) ).
fof(f22414,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22174,f16006]) ).
fof(f22415,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22175,f16006]) ).
fof(f22632,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22398,f16007]) ).
fof(f22633,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22399,f16007]) ).
fof(f22634,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22400,f16007]) ).
fof(f22635,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22401,f16007]) ).
fof(f22636,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22404,f16005]) ).
fof(f22637,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22405,f16005]) ).
fof(f22638,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22408,f16005]) ).
fof(f22639,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22409,f16005]) ).
fof(f22642,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22414,f16005]) ).
fof(f22643,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22415,f16005]) ).
fof(f22650,definition,
( spl606_16
<=> l1_cat_1(k11_cat_2(sK59,sK60)) ),
introduced(definition,[new_symbols(definition,[spl606_16])],[avatar_definition]) ).
fof(f22651,plain,
( l1_cat_1(k11_cat_2(sK59,sK60))
| ~ spl606_16 ),
inference(avatar_component_clause,[],[f22650]) ).
fof(f22652,plain,
( ~ l1_cat_1(k11_cat_2(sK59,sK60))
| spl606_16 ),
inference(avatar_component_clause,[],[f22650]) ).
fof(f22654,definition,
( spl606_17
<=> v2_cat_1(k11_cat_2(sK59,sK60)) ),
introduced(definition,[new_symbols(definition,[spl606_17])],[avatar_definition]) ).
fof(f22655,plain,
( v2_cat_1(k11_cat_2(sK59,sK60))
| ~ spl606_17 ),
inference(avatar_component_clause,[],[f22654]) ).
fof(f22656,plain,
( ~ v2_cat_1(k11_cat_2(sK59,sK60))
| spl606_17 ),
inference(avatar_component_clause,[],[f22654]) ).
fof(f22776,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22632,f16006]) ).
fof(f22777,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22633,f16006]) ).
fof(f22778,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22634,f16006]) ).
fof(f22779,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22635,f16006]) ).
fof(f22780,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22636,f16004]) ).
fof(f22781,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22637,f16004]) ).
fof(f22782,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22638,f16004]) ).
fof(f22783,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22639,f16004]) ).
fof(f22786,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22642,f16004]) ).
fof(f22787,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22643,f16004]) ).
fof(f22841,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22776,f16005]) ).
fof(f22842,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22777,f16005]) ).
fof(f22843,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22778,f16005]) ).
fof(f22844,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22779,f16005]) ).
fof(f22845,plain,
( k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22780,f16003]) ).
fof(f22846,plain,
( k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22781,f16003]) ).
fof(f22847,plain,
( k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22782,f16003]) ).
fof(f22848,plain,
( k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22783,f16003]) ).
fof(f22851,plain,
( k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22786,f16003]) ).
fof(f22852,plain,
( k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22787,f16003]) ).
fof(f22915,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22841,f16004]) ).
fof(f22916,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22842,f16004]) ).
fof(f22917,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22843,f16004]) ).
fof(f22918,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22844,f16004]) ).
fof(f22919,plain,
k11_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22845,f16002]) ).
fof(f22920,plain,
k11_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22846,f16002]) ).
fof(f22921,plain,
k12_isocat_2(sK58,sK59,sK60,sK63) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22847,f16002]) ).
fof(f22922,plain,
k12_isocat_2(sK58,sK59,sK60,sK61) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22848,f16002]) ).
fof(f22931,plain,
k11_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22851,f16002]) ).
fof(f22932,plain,
k12_isocat_2(sK58,sK59,sK60,sK62) = k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22852,f16002]) ).
fof(f22994,plain,
( k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22915,f16003]) ).
fof(f22995,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22916,f16003]) ).
fof(f22996,plain,
( k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22917,f16003]) ).
fof(f22997,plain,
( k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58) ),
inference(forward_subsumption_resolution,[],[f22918,f16003]) ).
fof(f22998,plain,
k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22994,f16002]) ).
fof(f22999,plain,
k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22995,f16002]) ).
fof(f23000,plain,
k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22996,f16002]) ).
fof(f23001,plain,
k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f22997,f16002]) ).
fof(f23002,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_16 ),
inference(resolution,[],[f22652,f16061]) ).
fof(f23003,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_16 ),
inference(forward_subsumption_resolution,[],[f23002,f16005]) ).
fof(f23004,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_16 ),
inference(forward_subsumption_resolution,[],[f23003,f16004]) ).
fof(f23005,plain,
( ~ l1_cat_1(sK60)
| spl606_16 ),
inference(forward_subsumption_resolution,[],[f23004,f16007]) ).
fof(f23006,plain,
( $false
| spl606_16 ),
inference(forward_subsumption_resolution,[],[f23005,f16006]) ).
fof(f23007,plain,
spl606_16,
inference(avatar_contradiction_clause,[],[f23006]) ).
fof(f23008,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_17 ),
inference(resolution,[],[f22656,f18145]) ).
fof(f23009,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_17 ),
inference(forward_subsumption_resolution,[],[f23008,f16005]) ).
fof(f23010,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_17 ),
inference(forward_subsumption_resolution,[],[f23009,f16004]) ).
fof(f23011,plain,
( ~ l1_cat_1(sK60)
| spl606_17 ),
inference(forward_subsumption_resolution,[],[f23010,f16007]) ).
fof(f23012,plain,
( $false
| spl606_17 ),
inference(forward_subsumption_resolution,[],[f23011,f16006]) ).
fof(f23013,plain,
spl606_17,
inference(avatar_contradiction_clause,[],[f23012]) ).
fof(f23349,definition,
( spl606_52
<=> m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59) ),
introduced(definition,[new_symbols(definition,[spl606_52])],[avatar_definition]) ).
fof(f23350,plain,
( m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ spl606_52 ),
inference(avatar_component_clause,[],[f23349]) ).
fof(f23351,plain,
( ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| spl606_52 ),
inference(avatar_component_clause,[],[f23349]) ).
fof(f23392,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_52 ),
inference(resolution,[],[f23351,f17241]) ).
fof(f23393,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_52 ),
inference(forward_subsumption_resolution,[],[f23392,f16005]) ).
fof(f23394,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_52 ),
inference(forward_subsumption_resolution,[],[f23393,f16004]) ).
fof(f23395,plain,
( ~ l1_cat_1(sK60)
| spl606_52 ),
inference(forward_subsumption_resolution,[],[f23394,f16007]) ).
fof(f23396,plain,
( $false
| spl606_52 ),
inference(forward_subsumption_resolution,[],[f23395,f16006]) ).
fof(f23397,plain,
spl606_52,
inference(avatar_contradiction_clause,[],[f23396]) ).
fof(f23572,definition,
( spl606_60
<=> m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60) ),
introduced(definition,[new_symbols(definition,[spl606_60])],[avatar_definition]) ).
fof(f23573,plain,
( m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ spl606_60 ),
inference(avatar_component_clause,[],[f23572]) ).
fof(f23574,plain,
( ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| spl606_60 ),
inference(avatar_component_clause,[],[f23572]) ).
fof(f23615,plain,
( ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_60 ),
inference(resolution,[],[f23574,f17243]) ).
fof(f23616,plain,
( ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_60 ),
inference(forward_subsumption_resolution,[],[f23615,f16005]) ).
fof(f23617,plain,
( ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| spl606_60 ),
inference(forward_subsumption_resolution,[],[f23616,f16004]) ).
fof(f23618,plain,
( ~ l1_cat_1(sK60)
| spl606_60 ),
inference(forward_subsumption_resolution,[],[f23617,f16007]) ).
fof(f23619,plain,
( $false
| spl606_60 ),
inference(forward_subsumption_resolution,[],[f23618,f16006]) ).
fof(f23620,plain,
spl606_60,
inference(avatar_contradiction_clause,[],[f23619]) ).
fof(f23717,plain,
! [X0,X1] :
( ~ l1_cat_1(sK58)
| ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| ~ v2_cat_1(sK58)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(resolution,[],[f22402,f16014]) ).
fof(f23739,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| ~ v2_cat_1(sK58)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23717,f16002]) ).
fof(f23748,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| ~ v2_cat_1(sK58)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23739,f16009]) ).
fof(f23750,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| ~ v2_cat_1(sK58)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23748,f16010]) ).
fof(f23752,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23750,f16003]) ).
fof(f23754,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23752,f16007]) ).
fof(f23756,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23754,f16006]) ).
fof(f23758,plain,
! [X0,X1] :
( ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65))
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f23756,f16005]) ).
fof(f23760,plain,
! [X0,X1] :
( ~ m2_nattra_1(X1,sK58,k11_cat_2(sK59,sK60),X0,sK62)
| ~ m2_cat_1(X0,sK58,k11_cat_2(sK59,sK60))
| k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65),k8_isocat_2(sK59,sK60)) = k13_isocat_2(sK58,sK59,sK60,X0,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),X0,sK62,sK63,X1,sK65)) ),
inference(forward_subsumption_resolution,[],[f23758,f16004]) ).
fof(f28484,plain,
( ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k8_isocat_2(sK59,sK60)) ),
inference(resolution,[],[f23760,f16013]) ).
fof(f28488,plain,
k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k8_isocat_2(sK59,sK60)),
inference(forward_subsumption_resolution,[],[f28484,f16008]) ).
fof(f28493,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(superposition,[],[f16071,f28488]) ).
fof(f28508,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f28493,f16012]) ).
fof(f28516,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f28508,f16011]) ).
fof(f28524,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f28516,f16014]) ).
fof(f28532,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_cat_1(k8_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK59)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59) ),
inference(forward_subsumption_resolution,[],[f28524,f16013]) ).
fof(f28540,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28532,f23350]) ).
fof(f28548,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28540,f16010]) ).
fof(f28556,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28548,f16009]) ).
fof(f28564,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28556,f16008]) ).
fof(f28572,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28564,f22655]) ).
fof(f28580,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28572,f22651]) ).
fof(f28583,definition,
( spl606_147
<=> m2_nattra_1(k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),sK58,k11_cat_2(sK59,sK60),sK61,sK63) ),
introduced(definition,[new_symbols(definition,[spl606_147])],[avatar_definition]) ).
fof(f28584,plain,
( m2_nattra_1(k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),sK58,k11_cat_2(sK59,sK60),sK61,sK63)
| ~ spl606_147 ),
inference(avatar_component_clause,[],[f28583]) ).
fof(f28585,plain,
( ~ m2_nattra_1(k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),sK58,k11_cat_2(sK59,sK60),sK61,sK63)
| spl606_147 ),
inference(avatar_component_clause,[],[f28583]) ).
fof(f28596,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28580,f16003]) ).
fof(f28607,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28596,f16002]) ).
fof(f28628,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ l1_cat_1(sK59)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28607,f16005]) ).
fof(f28629,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,sK63,sK65,k8_isocat_2(sK59,sK60))))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28628,f16004]) ).
fof(f28630,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,sK62,sK64,k8_isocat_2(sK59,sK60)),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_demodulation,[],[f28629,f23000]) ).
fof(f28631,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK63,k8_isocat_2(sK59,sK60)),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_demodulation,[],[f28630,f22998]) ).
fof(f28632,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK62,k8_isocat_2(sK59,sK60)),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_demodulation,[],[f28631,f22919]) ).
fof(f28633,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK59,sK61,k8_isocat_2(sK59,sK60)),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_demodulation,[],[f28632,f22931]) ).
fof(f28634,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK59),u1_cat_1(sK58),u2_cat_1(sK59),k13_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK59,k11_isocat_2(sK58,sK59,sK60,sK61),k11_isocat_2(sK58,sK59,sK60,sK62),k11_isocat_2(sK58,sK59,sK60,sK63),k13_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k13_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_demodulation,[],[f28633,f22920]) ).
fof(f28635,plain,
( $false
| spl606_14
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(forward_subsumption_resolution,[],[f28634,f21377]) ).
fof(f28636,plain,
( spl606_14
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(avatar_contradiction_clause,[],[f28635]) ).
fof(f28637,plain,
( ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| spl606_147 ),
inference(resolution,[],[f28585,f16072]) ).
fof(f28638,plain,
( ~ l1_cat_1(sK58)
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28637,f16003]) ).
fof(f28639,plain,
( ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28638,f16002]) ).
fof(f28640,plain,
( ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28639,f22655]) ).
fof(f28641,plain,
( ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28640,f22651]) ).
fof(f28642,plain,
( ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28641,f16008]) ).
fof(f28643,plain,
( ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28642,f16009]) ).
fof(f28644,plain,
( ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28643,f16010]) ).
fof(f28645,plain,
( ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28644,f16013]) ).
fof(f28646,plain,
( $false
| ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(forward_subsumption_resolution,[],[f28645,f16014]) ).
fof(f28647,plain,
( ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(avatar_contradiction_clause,[],[f28646]) ).
fof(f28652,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(resolution,[],[f28584,f16093]) ).
fof(f28676,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28652,f16010]) ).
fof(f28692,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28676,f16008]) ).
fof(f28708,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK60)
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28692,f16007]) ).
fof(f28724,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK59)
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28708,f16006]) ).
fof(f28740,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK59)
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28724,f16005]) ).
fof(f28756,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28740,f16004]) ).
fof(f28770,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ l1_cat_1(sK58)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28756,f16003]) ).
fof(f28775,plain,
( k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)) = k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65),k9_isocat_2(sK59,sK60))
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f28770,f16002]) ).
fof(f29300,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_147 ),
inference(superposition,[],[f16071,f28775]) ).
fof(f29315,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ r2_nattra_1(sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29300,f16012]) ).
fof(f29323,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_nattra_1(sK65,sK58,k11_cat_2(sK59,sK60),sK62,sK63)
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29315,f16011]) ).
fof(f29331,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_nattra_1(sK64,sK58,k11_cat_2(sK59,sK60),sK61,sK62)
| ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29323,f16014]) ).
fof(f29339,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_cat_1(k9_isocat_2(sK59,sK60),k11_cat_2(sK59,sK60),sK60)
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29331,f16013]) ).
fof(f29347,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK63,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29339,f23573]) ).
fof(f29355,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK62,sK58,k11_cat_2(sK59,sK60))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29347,f16010]) ).
fof(f29363,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ m2_cat_1(sK61,sK58,k11_cat_2(sK59,sK60))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29355,f16009]) ).
fof(f29371,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ v2_cat_1(k11_cat_2(sK59,sK60))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29363,f16008]) ).
fof(f29379,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ l1_cat_1(k11_cat_2(sK59,sK60))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29371,f22655]) ).
fof(f29387,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ v2_cat_1(sK58)
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29379,f22651]) ).
fof(f29395,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ l1_cat_1(sK58)
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29387,f16003]) ).
fof(f29402,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ v2_cat_1(sK60)
| ~ l1_cat_1(sK60)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29395,f16002]) ).
fof(f29408,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ l1_cat_1(sK60)
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29402,f16007]) ).
fof(f29409,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,sK63,sK65,k9_isocat_2(sK59,sK60))))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29408,f16006]) ).
fof(f29410,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k6_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,sK62,sK64,k9_isocat_2(sK59,sK60)),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_demodulation,[],[f29409,f23001]) ).
fof(f29411,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK63,k9_isocat_2(sK59,sK60)),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_demodulation,[],[f29410,f22999]) ).
fof(f29412,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK62,k9_isocat_2(sK59,sK60)),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_demodulation,[],[f29411,f22921]) ).
fof(f29413,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k2_isocat_1(sK58,k11_cat_2(sK59,sK60),sK60,sK61,k9_isocat_2(sK59,sK60)),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_demodulation,[],[f29412,f22932]) ).
fof(f29414,plain,
( r4_nattra_1(u1_cat_1(sK58),u2_cat_1(sK60),u1_cat_1(sK58),u2_cat_1(sK60),k14_isocat_2(sK58,sK59,sK60,sK61,sK63,k8_nattra_1(sK58,k11_cat_2(sK59,sK60),sK61,sK62,sK63,sK64,sK65)),k8_nattra_1(sK58,sK60,k12_isocat_2(sK58,sK59,sK60,sK61),k12_isocat_2(sK58,sK59,sK60,sK62),k12_isocat_2(sK58,sK59,sK60,sK63),k14_isocat_2(sK58,sK59,sK60,sK61,sK62,sK64),k14_isocat_2(sK58,sK59,sK60,sK62,sK63,sK65)))
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_demodulation,[],[f29413,f22922]) ).
fof(f29415,plain,
( $false
| spl606_13
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(forward_subsumption_resolution,[],[f29414,f21373]) ).
fof(f29416,plain,
( spl606_13
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(avatar_contradiction_clause,[],[f29415]) ).
cnf(s10,plain,
( ~ spl606_13
| ~ spl606_14 ),
inference(sat_conversion,[],[f21378]) ).
cnf(s53,plain,
spl606_16,
inference(sat_conversion,[],[f23007]) ).
cnf(s54,plain,
spl606_17,
inference(sat_conversion,[],[f23013]) ).
cnf(s62,plain,
spl606_52,
inference(sat_conversion,[],[f23397]) ).
cnf(s70,plain,
spl606_60,
inference(sat_conversion,[],[f23620]) ).
cnf(s152,plain,
( spl606_14
| ~ spl606_16
| ~ spl606_17
| ~ spl606_52 ),
inference(sat_conversion,[],[f28636]) ).
cnf(s153,plain,
( ~ spl606_16
| ~ spl606_17
| spl606_147 ),
inference(sat_conversion,[],[f28647]) ).
cnf(s170,plain,
( spl606_13
| ~ spl606_16
| ~ spl606_17
| ~ spl606_60
| ~ spl606_147 ),
inference(sat_conversion,[],[f29416]) ).
cnf(s228,plain,
spl606_147,
inference(rat,[],[s153,s54,s53]) ).
cnf(s229,plain,
spl606_14,
inference(rat,[],[s152,s62,s54,s53]) ).
cnf(s255,plain,
spl606_13,
inference(rat,[],[s170,s53,s70,s54,s228]) ).
cnf(s353,plain,
$false,
inference(rat,[],[s10,s229,s255]) ).
fof(f29417,plain,
$false,
inference(avatar_sat_refutation,[],[s353]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT028+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.15 % Computer : n012.cluster.edu
% 0.09/0.15 % Model : x86_64 x86_64
% 0.09/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.15 % Memory : 8046.5625MB
% 0.09/0.15 % OS : Linux 6.8.0-71-generic
% 0.09/0.15 % CPULimit : 300
% 0.09/0.15 % WCLimit : 300
% 0.09/0.15 % DateTime : Mon Sep 28 21:18:50 UTC 2026
% 0.09/0.15 % CPUTime :
% 0.09/0.15 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 Running first-order theorem proving
% 0.09/0.18 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
% 15.21/3.32 % (3778889)Detected formulas, will run a generic FOF schedule.
% 15.21/3.32 % (3778896)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=3594670723:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 15.21/3.32 % (3778897)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=1269870164:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 15.21/3.32 % (3778898)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=2716603743:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 15.21/3.32 % (3778900)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1760879094:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 15.21/3.32 % (3778899)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1559405310:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 15.21/3.32 % (3778902)dis-21_1_sil=8000:lcm=predicate:random_seed=3791538213:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 15.21/3.32 % (3778901)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1758006267:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 15.21/3.32 % (3778899)Refutation not found, incomplete strategy
% 15.21/3.32 % (3778899)------------------------------
% 15.21/3.32 % (3778899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/3.32 % (3778899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/3.32 % (3778899)CaDiCaL version: 2.1.3
% 15.21/3.32 % (3778899)Termination reason: Refutation not found, incomplete strategy
% 15.21/3.32 % (3778899)Time elapsed: 0.050 s
% 15.21/3.32 % (3778899)Peak memory usage: 105 MB
% 15.21/3.32 % (3778899)Instructions burned: 79 (million)
% 15.21/3.32 % (3778901)Instruction limit reached!
% 15.21/3.32 % (3778901)------------------------------
% 15.21/3.32 % (3778901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/3.32 % (3778901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/3.32 % (3778901)CaDiCaL version: 2.1.3
% 15.21/3.32 % (3778901)Termination reason: Instruction limit
% 15.21/3.32 % (3778901)Termination phase: Property scanning
% 15.21/3.32 % (3778901)Time elapsed: 0.062 s
% 15.21/3.32 % (3778901)Peak memory usage: 100 MB
% 15.21/3.32 % (3778901)Instructions burned: 140 (million)
% 15.21/3.32 % (3778900)Instruction limit reached!
% 15.21/3.32 % (3778900)------------------------------
% 15.21/3.32 % (3778900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/3.32 % (3778900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/3.32 % (3778900)CaDiCaL version: 2.1.3
% 15.21/3.32 % (3778900)Termination reason: Instruction limit
% 15.21/3.32 % (3778900)Termination phase: Saturation
% 15.21/3.32 % (3778900)Time elapsed: 0.072 s
% 15.21/3.32 % (3778900)Peak memory usage: 104 MB
% 15.21/3.32 % (3778900)Instructions burned: 121 (million)
% 15.21/3.32 % (3778902)Instruction limit reached!
% 15.21/3.32 % (3778902)------------------------------
% 15.21/3.32 % (3778902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/3.32 % (3778902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/3.32 % (3778902)CaDiCaL version: 2.1.3
% 15.21/3.32 % (3778902)Termination reason: Instruction limit
% 15.21/3.32 % (3778902)Termination phase: Preprocessing 1
% 15.21/3.32 % (3778902)Time elapsed: 0.084 s
% 15.21/3.32 % (3778902)Peak memory usage: 101 MB
% 15.21/3.32 % (3778902)Instructions burned: 129 (million)
% 15.21/3.32 % (3778899)------------------------------
% 15.21/3.32 % (3778899)------------------------------
% 15.21/3.32 % (3778911)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1841078476:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/157Mi)
% 15.21/3.32 % (3778910)lrs+10_1_sil=8000:sp=occurrence:random_seed=2478742641:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 15.21/3.32 % (3778912)lrs+1011_1_sil=32000:sp=occurrence:random_seed=501375498:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 15.21/3.32 % (3778911)Instruction limit reached!
% 15.21/3.32 % (3778911)------------------------------
% 15.21/3.32 % (3778911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778911)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778911)Termination reason: Instruction limit
% 23.61/4.36 % (3778911)Termination phase: SInE selection
% 23.61/4.36 % (3778911)Time elapsed: 0.066 s
% 23.61/4.36 % (3778911)Peak memory usage: 100 MB
% 23.61/4.36 % (3778911)Instructions burned: 157 (million)
% 23.61/4.36 % (3778910)Instruction limit reached!
% 23.61/4.36 % (3778910)------------------------------
% 23.61/4.36 % (3778910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778910)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778910)Termination reason: Instruction limit
% 23.61/4.36 % (3778910)Termination phase: Saturation
% 23.61/4.36 % (3778910)Time elapsed: 0.169 s
% 23.61/4.36 % (3778910)Peak memory usage: 107 MB
% 23.61/4.36 % (3778910)Instructions burned: 285 (million)
% 23.61/4.36 % (3778912)Instruction limit reached!
% 23.61/4.36 % (3778912)------------------------------
% 23.61/4.36 % (3778912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778912)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778912)Termination reason: Instruction limit
% 23.61/4.36 % (3778912)Termination phase: Saturation
% 23.61/4.36 % (3778912)Time elapsed: 0.176 s
% 23.61/4.36 % (3778912)Peak memory usage: 107 MB
% 23.61/4.36 % (3778912)Instructions burned: 327 (million)
% 23.61/4.36 % (3778915)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=1851866886:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 23.61/4.36 % (3778917)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3334356233:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 23.61/4.36 % (3778915)Instruction limit reached!
% 23.61/4.36 % (3778915)------------------------------
% 23.61/4.36 % (3778915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778915)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778915)Termination reason: Instruction limit
% 23.61/4.36 % (3778915)Termination phase: Preprocessing 1
% 23.61/4.36 % (3778915)Time elapsed: 0.131 s
% 23.61/4.36 % (3778915)Peak memory usage: 101 MB
% 23.61/4.36 % (3778915)Instructions burned: 248 (million)
% 23.61/4.36 % (3778918)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2254770332:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 23.61/4.36 % (3778919)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1597852295:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 23.61/4.36 % (3778917)Instruction limit reached!
% 23.61/4.36 % (3778917)------------------------------
% 23.61/4.36 % (3778917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778917)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778917)Termination reason: Instruction limit
% 23.61/4.36 % (3778917)Termination phase: Saturation
% 23.61/4.36 % (3778917)Time elapsed: 0.161 s
% 23.61/4.36 % (3778917)Peak memory usage: 108 MB
% 23.61/4.36 % (3778917)Instructions burned: 295 (million)
% 23.61/4.36 % (3778919)Instruction limit reached!
% 23.61/4.36 % (3778919)------------------------------
% 23.61/4.36 % (3778919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.61/4.36 % (3778919)CaDiCaL version: 2.1.3
% 23.61/4.36 % (3778919)Termination reason: Instruction limit
% 23.61/4.36 % (3778919)Termination phase: Preprocessing 3
% 23.61/4.36 % (3778919)Time elapsed: 0.085 s
% 23.61/4.36 % (3778919)Peak memory usage: 103 MB
% 23.61/4.36 % (3778919)Instructions burned: 114 (million)
% 23.61/4.36 % (3778922)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=292444252:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 23.61/4.36 % (3778922)Instruction limit reached!
% 23.61/4.36 % (3778922)------------------------------
% 23.61/4.36 % (3778922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.61/4.36 % (3778925)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=953246588:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 16.17/5.84 % (3778922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778922)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778922)Termination reason: Instruction limit
% 16.17/5.84 % (3778922)Termination phase: Preprocessing 2
% 16.17/5.84 % (3778922)Time elapsed: 0.093 s
% 16.17/5.84 % (3778922)Peak memory usage: 107 MB
% 16.17/5.84 % (3778922)Instructions burned: 127 (million)
% 16.17/5.84 % (3778925)Instruction limit reached!
% 16.17/5.84 % (3778925)------------------------------
% 16.17/5.84 % (3778925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778925)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778925)Termination reason: Instruction limit
% 16.17/5.84 % (3778925)Termination phase: Property scanning
% 16.17/5.84 % (3778925)Time elapsed: 0.048 s
% 16.17/5.84 % (3778925)Peak memory usage: 100 MB
% 16.17/5.84 % (3778925)Instructions burned: 116 (million)
% 16.17/5.84 % (3778926)lrs+10_1_sil=8000:sp=occurrence:random_seed=3649521103:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 16.17/5.84 % (3778930)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1115708826:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 16.17/5.84 % (3778929)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3158190086:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 16.17/5.84 % (3778929)Instruction limit reached!
% 16.17/5.84 % (3778929)------------------------------
% 16.17/5.84 % (3778929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778929)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778929)Termination reason: Instruction limit
% 16.17/5.84 % (3778929)Termination phase: Saturation
% 16.17/5.84 % (3778929)Time elapsed: 0.238 s
% 16.17/5.84 % (3778929)Peak memory usage: 107 MB
% 16.17/5.84 % (3778929)Instructions burned: 439 (million)
% 16.17/5.84 % (3778926)Instruction limit reached!
% 16.17/5.84 % (3778926)------------------------------
% 16.17/5.84 % (3778926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778926)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778926)Termination reason: Instruction limit
% 16.17/5.84 % (3778926)Termination phase: Saturation
% 16.17/5.84 % (3778926)Time elapsed: 0.481 s
% 16.17/5.84 % (3778926)Peak memory usage: 120 MB
% 16.17/5.84 % (3778926)Instructions burned: 908 (million)
% 16.17/5.84 % (3778934)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2483713359:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 16.17/5.84 % (3778934)Instruction limit reached!
% 16.17/5.84 % (3778934)------------------------------
% 16.17/5.84 % (3778934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778934)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778934)Termination reason: Instruction limit
% 16.17/5.84 % (3778934)Termination phase: Equality resolution with deletion
% 16.17/5.84 % (3778934)Time elapsed: 0.064 s
% 16.17/5.84 % (3778934)Peak memory usage: 104 MB
% 16.17/5.84 % (3778934)Instructions burned: 136 (million)
% 16.17/5.84 % (3778937)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=418041188:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 16.17/5.84 % (3778935)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3773336079:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 16.17/5.84 % (3778918)Instruction limit reached!
% 16.17/5.84 % (3778918)------------------------------
% 16.17/5.84 % (3778918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778918)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778918)Termination reason: Instruction limit
% 16.17/5.84 % (3778918)Termination phase: Saturation
% 16.17/5.84 % (3778918)Time elapsed: 1.394 s
% 16.17/5.84 % (3778918)Peak memory usage: 263 MB
% 16.17/5.84 % (3778918)Instructions burned: 2350 (million)
% 16.17/5.84 % (3778935)Instruction limit reached!
% 16.17/5.84 % (3778935)------------------------------
% 16.17/5.84 % (3778935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778935)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778935)Termination reason: Instruction limit
% 16.17/5.84 % (3778935)Termination phase: Function definition elimination
% 16.17/5.84 % (3778935)Time elapsed: 0.346 s
% 16.17/5.84 % (3778935)Peak memory usage: 118 MB
% 16.17/5.84 % (3778935)Instructions burned: 592 (million)
% 16.17/5.84 % (3778942)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=2160800762:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 16.17/5.84 % (3778943)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2673254526:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 16.17/5.84 % (3778942)Instruction limit reached!
% 16.17/5.84 % (3778942)------------------------------
% 16.17/5.84 % (3778942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778942)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778942)Termination reason: Instruction limit
% 16.17/5.84 % (3778942)Termination phase: Property scanning
% 16.17/5.84 % (3778942)Time elapsed: 0.057 s
% 16.17/5.84 % (3778942)Peak memory usage: 100 MB
% 16.17/5.84 % (3778942)Instructions burned: 127 (million)
% 16.17/5.84 % (3778943)Instruction limit reached!
% 16.17/5.84 % (3778943)------------------------------
% 16.17/5.84 % (3778943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778943)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778943)Termination reason: Instruction limit
% 16.17/5.84 % (3778943)Termination phase: Property scanning
% 16.17/5.84 % (3778943)Time elapsed: 0.061 s
% 16.17/5.84 % (3778943)Peak memory usage: 100 MB
% 16.17/5.84 % (3778943)Instructions burned: 134 (million)
% 16.17/5.84 % (3778946)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2393579306:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 16.17/5.84 % (3778947)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1229632734:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 16.17/5.84 % (3778946)Instruction limit reached!
% 16.17/5.84 % (3778946)------------------------------
% 16.17/5.84 % (3778946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778946)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778946)Termination reason: Instruction limit
% 16.17/5.84 % (3778946)Termination phase: Saturation
% 16.17/5.84 % (3778946)Time elapsed: 0.087 s
% 16.17/5.84 % (3778946)Peak memory usage: 105 MB
% 16.17/5.84 % (3778946)Instructions burned: 143 (million)
% 16.17/5.84 % (3778947)Instruction limit reached!
% 16.17/5.84 % (3778947)------------------------------
% 16.17/5.84 % (3778947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778947)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778947)Termination reason: Instruction limit
% 16.17/5.84 % (3778947)Termination phase: Saturation
% 16.17/5.84 % (3778947)Time elapsed: 0.230 s
% 16.17/5.84 % (3778947)Peak memory usage: 110 MB
% 16.17/5.84 % (3778947)Instructions burned: 431 (million)
% 16.17/5.84 % (3778952)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=1928395982:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 16.17/5.84 % (3778953)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=3701465430:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 16.17/5.84 % (3778953)Instruction limit reached!
% 16.17/5.84 % (3778953)------------------------------
% 16.17/5.84 % (3778953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778953)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778953)Termination reason: Instruction limit
% 16.17/5.84 % (3778953)Termination phase: Unused predicate definition removal
% 16.17/5.84 % (3778953)Time elapsed: 0.103 s
% 16.17/5.84 % (3778953)Peak memory usage: 102 MB
% 16.17/5.84 % (3778953)Instructions burned: 150 (million)
% 16.17/5.84 % (3778956)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2172929423:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 16.17/5.84 % (3778930)Instruction limit reached!
% 16.17/5.84 % (3778930)------------------------------
% 16.17/5.84 % (3778930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/5.84 % (3778930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/5.84 % (3778930)CaDiCaL version: 2.1.3
% 16.17/5.84 % (3778930)Termination reason: Instruction limit
% 16.17/5.84 % (3778930)Termination phase: Saturation
% 16.17/5.84 % (3778930)Time elapsed: 2.845 s
% 16.17/5.84 % (3778930)Peak memory usage: 271 MB
% 16.17/5.84 % (3778930)Instructions burned: 5203 (million)
% 16.17/5.84 % (3778958)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2432433461:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 16.17/5.84 % (3778937)First to succeed.
% 16.17/5.84 % (3778937)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3778889"
% 16.17/5.84 % (3778937)Refutation found. Thanks to Tanya!
% 16.17/5.84 % SZS status Theorem for theBenchmark
% 16.17/5.84 % SZS output start Proof for theBenchmark
% See solution above
% 34.83/6.07 % (3778937)------------------------------
% 34.83/6.07 % (3778937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.83/6.07 % (3778937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.83/6.07 % (3778937)CaDiCaL version: 2.1.3
% 34.83/6.07 % (3778937)Termination reason: Refutation
% 34.83/6.07 % (3778937)Time elapsed: 2.558 s
% 34.83/6.07 % (3778937)Peak memory usage: 194 MB
% 34.83/6.07 % (3778937)Instructions burned: 5036 (million)
% 34.83/6.07 % (3778937)------------------------------
% 34.83/6.07 % (3778937)------------------------------
% 34.83/6.07 % (3778889)Success in time 5.264 s
% 34.83/6.07 % Vampire exiting
%------------------------------------------------------------------------------