%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT031+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:46 AM UTC 2026
% Result : Theorem 22.68s 7.66s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 14
% Syntax : Number of formulae : 206 ( 47 unt; 3 def)
% Number of atoms : 1210 ( 114 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 1830 ( 826 ~; 815 |; 121 &)
% ( 3 <=>; 65 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 4 prp; 0-5 aty)
% Number of functors : 27 ( 27 usr; 10 con; 0-9 aty)
% Number of variables : 451 ( 0 sgn 431 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21083,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_cat_2) ).
fof(f21119,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( u1_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u1_cat_1(X0),u1_cat_1(X1))
& u2_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1))
& u3_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u3_cat_1(X0),u3_cat_1(X1))
& u4_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u4_cat_1(X0),u4_cat_1(X1))
& u5_cat_1(k11_cat_2(X0,X1)) = k10_cat_2(u2_cat_1(X0),u2_cat_1(X1),u5_cat_1(X0),u5_cat_1(X1))
& u6_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u1_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),u2_cat_1(X1),u6_cat_1(X0),u6_cat_1(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_cat_2) ).
fof(f21181,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f25728,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( m2_cat_1(X2,X0,X1)
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ( r1_nattra_1(X0,X1,X2,X3)
=> ! [X4] :
( m1_nattra_1(X4,X0,X1,X2,X3)
=> ! [X5] :
( m1_subset_1(X5,u1_cat_1(X0))
=> k5_nattra_1(X0,X1,X2,X3,X4,X5) = k8_funct_2(u1_cat_1(X0),u2_cat_1(X1),X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_nattra_1) ).
fof(f29043,axiom,
! [X0,X1,X2,X3,X4] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,X1)
& m2_cat_1(X4,X0,X2) )
=> m2_cat_1(k10_isocat_2(X0,X1,X2,X3,X4),X0,k11_cat_2(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_isocat_2) ).
fof(f29044,axiom,
! [X0,X1,X2,X3,X4] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,X1)
& m2_cat_1(X4,X0,X2) )
=> k10_isocat_2(X0,X1,X2,X3,X4) = k13_funct_3(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_isocat_2) ).
fof(f29049,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2)
& m2_cat_1(X3,X0,X1)
& m2_cat_1(X4,X0,X1)
& m2_cat_1(X5,X0,X2)
& m2_cat_1(X6,X0,X2)
& m1_nattra_1(X7,X0,X1,X3,X4)
& m1_nattra_1(X8,X0,X2,X5,X6) )
=> m1_nattra_1(k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_isocat_2) ).
fof(f29105,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ! [X5] :
( m2_cat_1(X5,X0,X2)
=> ! [X6] :
( m2_cat_1(X6,X0,X2)
=> ( ( r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6) )
=> ! [X7] :
( m1_nattra_1(X7,X0,X1,X3,X4)
=> ! [X8] :
( m1_nattra_1(X8,X0,X2,X5,X6)
=> ! [X9] :
( m1_subset_1(X9,u1_cat_1(X0))
=> k8_funct_2(u1_cat_1(X0),k2_zfmisc_1(u2_cat_1(X1),u2_cat_1(X2)),k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9)) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l54_isocat_2) ).
fof(f29109,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ! [X5] :
( m2_cat_1(X5,X0,X2)
=> ! [X6] :
( m2_cat_1(X6,X0,X2)
=> ( ( r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6) )
=> r1_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t44_isocat_2) ).
fof(f29110,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,X1)
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ! [X5] :
( m2_cat_1(X5,X0,X2)
=> ! [X6] :
( m2_cat_1(X6,X0,X2)
=> ( ( r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6) )
=> ! [X7] :
( m1_nattra_1(X7,X0,X1,X3,X4)
=> ! [X8] :
( m1_nattra_1(X8,X0,X2,X5,X6)
=> k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8) = k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_isocat_2) ).
fof(f29111,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,X1)
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ! [X5] :
( m2_cat_1(X5,X0,X2)
=> ! [X6] :
( m2_cat_1(X6,X0,X2)
=> ( ( r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6) )
=> ! [X7] :
( m1_nattra_1(X7,X0,X1,X3,X4)
=> ! [X8] :
( m1_nattra_1(X8,X0,X2,X5,X6)
=> ! [X9] :
( m1_subset_1(X9,u1_cat_1(X0))
=> k5_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6),k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9)) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t45_isocat_2) ).
fof(f29112,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,X1)
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ! [X5] :
( m2_cat_1(X5,X0,X2)
=> ! [X6] :
( m2_cat_1(X6,X0,X2)
=> ( ( r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6) )
=> ! [X7] :
( m1_nattra_1(X7,X0,X1,X3,X4)
=> ! [X8] :
( m1_nattra_1(X8,X0,X2,X5,X6)
=> ! [X9] :
( m1_subset_1(X9,u1_cat_1(X0))
=> k5_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6),k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9)) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f29111]) ).
fof(f29247,plain,
! [X0,X1,X2,X3,X4] :
( m2_cat_1(k10_isocat_2(X0,X1,X2,X3,X4),X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(ennf_transformation,[],[f29043]) ).
fof(f29248,plain,
! [X0,X1,X2,X3,X4] :
( m2_cat_1(k10_isocat_2(X0,X1,X2,X3,X4),X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(flattening,[],[f29247]) ).
fof(f29249,plain,
! [X0,X1,X2,X3,X4] :
( k10_isocat_2(X0,X1,X2,X3,X4) = k13_funct_3(X3,X4)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(ennf_transformation,[],[f29044]) ).
fof(f29250,plain,
! [X0,X1,X2,X3,X4] :
( k10_isocat_2(X0,X1,X2,X3,X4) = k13_funct_3(X3,X4)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(flattening,[],[f29249]) ).
fof(f29259,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( m1_nattra_1(k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X6,X0,X2)
| ~ m1_nattra_1(X7,X0,X1,X3,X4)
| ~ m1_nattra_1(X8,X0,X2,X5,X6) ),
inference(ennf_transformation,[],[f29049]) ).
fof(f29260,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( m1_nattra_1(k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X6,X0,X2)
| ~ m1_nattra_1(X7,X0,X1,X3,X4)
| ~ m1_nattra_1(X8,X0,X2,X5,X6) ),
inference(flattening,[],[f29259]) ).
fof(f29363,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( k8_funct_2(u1_cat_1(X0),k2_zfmisc_1(u2_cat_1(X1),u2_cat_1(X2)),k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9))
| ~ m1_subset_1(X9,u1_cat_1(X0)) )
| ~ m1_nattra_1(X8,X0,X2,X5,X6) )
| ~ m1_nattra_1(X7,X0,X1,X3,X4) )
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29105]) ).
fof(f29364,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( k8_funct_2(u1_cat_1(X0),k2_zfmisc_1(u2_cat_1(X1),u2_cat_1(X2)),k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9))
| ~ m1_subset_1(X9,u1_cat_1(X0)) )
| ~ m1_nattra_1(X8,X0,X2,X5,X6) )
| ~ m1_nattra_1(X7,X0,X1,X3,X4) )
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29363]) ).
fof(f29371,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( r1_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6))
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29109]) ).
fof(f29372,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( r1_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6))
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29371]) ).
fof(f29373,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8) = k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8)
| ~ m1_nattra_1(X8,X0,X2,X5,X6) )
| ~ m1_nattra_1(X7,X0,X1,X3,X4) )
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29110]) ).
fof(f29374,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8) = k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8)
| ~ m1_nattra_1(X8,X0,X2,X5,X6) )
| ~ m1_nattra_1(X7,X0,X1,X3,X4) )
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2) )
| ~ m2_cat_1(X5,X0,X2) )
| ~ m2_cat_1(X4,X0,X1) )
| ~ m2_cat_1(X3,X0,X1) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29373]) ).
fof(f29375,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9)) != k5_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6),k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X9)
& m1_subset_1(X9,u1_cat_1(X0)) )
& m1_nattra_1(X8,X0,X2,X5,X6) )
& m1_nattra_1(X7,X0,X1,X3,X4) )
& r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6)
& m2_cat_1(X6,X0,X2) )
& m2_cat_1(X5,X0,X2) )
& m2_cat_1(X4,X0,X1) )
& m2_cat_1(X3,X0,X1) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29112]) ).
fof(f29376,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9)) != k5_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6),k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X9)
& m1_subset_1(X9,u1_cat_1(X0)) )
& m1_nattra_1(X8,X0,X2,X5,X6) )
& m1_nattra_1(X7,X0,X1,X3,X4) )
& r1_nattra_1(X0,X1,X3,X4)
& r1_nattra_1(X0,X2,X5,X6)
& m2_cat_1(X6,X0,X2) )
& m2_cat_1(X5,X0,X2) )
& m2_cat_1(X4,X0,X1) )
& m2_cat_1(X3,X0,X1) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(flattening,[],[f29375]) ).
fof(f29428,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21181]) ).
fof(f29429,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,[],[f29428]) ).
fof(f29776,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k5_nattra_1(X0,X1,X2,X3,X4,X5) = k8_funct_2(u1_cat_1(X0),u2_cat_1(X1),X4,X5)
| ~ m1_subset_1(X5,u1_cat_1(X0)) )
| ~ m1_nattra_1(X4,X0,X1,X2,X3) )
| ~ r1_nattra_1(X0,X1,X2,X3)
| ~ m2_cat_1(X3,X0,X1) )
| ~ m2_cat_1(X2,X0,X1) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f25728]) ).
fof(f29777,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k5_nattra_1(X0,X1,X2,X3,X4,X5) = k8_funct_2(u1_cat_1(X0),u2_cat_1(X1),X4,X5)
| ~ m1_subset_1(X5,u1_cat_1(X0)) )
| ~ m1_nattra_1(X4,X0,X1,X2,X3) )
| ~ r1_nattra_1(X0,X1,X2,X3)
| ~ m2_cat_1(X3,X0,X1) )
| ~ m2_cat_1(X2,X0,X1) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29776]) ).
fof(f30197,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21083]) ).
fof(f30198,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,[],[f30197]) ).
fof(f30245,plain,
! [X0] :
( ! [X1] :
( ( u1_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u1_cat_1(X0),u1_cat_1(X1))
& u2_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1))
& u3_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u3_cat_1(X0),u3_cat_1(X1))
& u4_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u4_cat_1(X0),u4_cat_1(X1))
& u5_cat_1(k11_cat_2(X0,X1)) = k10_cat_2(u2_cat_1(X0),u2_cat_1(X1),u5_cat_1(X0),u5_cat_1(X1))
& u6_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u1_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),u2_cat_1(X1),u6_cat_1(X0),u6_cat_1(X1)) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f21119]) ).
fof(f30246,plain,
! [X0] :
( ! [X1] :
( ( u1_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u1_cat_1(X0),u1_cat_1(X1))
& u2_cat_1(k11_cat_2(X0,X1)) = k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1))
& u3_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u3_cat_1(X0),u3_cat_1(X1))
& u4_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u2_cat_1(X0),u2_cat_1(X1),u1_cat_1(X0),u1_cat_1(X1),u4_cat_1(X0),u4_cat_1(X1))
& u5_cat_1(k11_cat_2(X0,X1)) = k10_cat_2(u2_cat_1(X0),u2_cat_1(X1),u5_cat_1(X0),u5_cat_1(X1))
& u6_cat_1(k11_cat_2(X0,X1)) = k9_cat_2(u1_cat_1(X0),u1_cat_1(X1),u2_cat_1(X0),u2_cat_1(X1),u6_cat_1(X0),u6_cat_1(X1)) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f30245]) ).
fof(f36492,plain,
( k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68),k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK71)
& m1_subset_1(sK71,u1_cat_1(sK62))
& m1_nattra_1(sK70,sK62,sK64,sK67,sK68)
& m1_nattra_1(sK69,sK62,sK63,sK65,sK66)
& r1_nattra_1(sK62,sK63,sK65,sK66)
& r1_nattra_1(sK62,sK64,sK67,sK68)
& m2_cat_1(sK68,sK62,sK64)
& m2_cat_1(sK67,sK62,sK64)
& m2_cat_1(sK66,sK62,sK63)
& m2_cat_1(sK65,sK62,sK63)
& v2_cat_1(sK64)
& l1_cat_1(sK64)
& v2_cat_1(sK63)
& l1_cat_1(sK63)
& v2_cat_1(sK62)
& l1_cat_1(sK62) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70,sK71]),skolemize(X0,sK62),skolemize(X1,sK63),skolemize(X2,sK64),skolemize(X3,sK65),skolemize(X4,sK66),skolemize(X5,sK67),skolemize(X6,sK68),skolemize(X7,sK69),skolemize(X8,sK70),skolemize(X9,sK71)],[f29376]) ).
fof(f38533,plain,
! [X2,X3,X0,X1,X4] :
( m2_cat_1(k10_isocat_2(X0,X1,X2,X3,X4),X0,k11_cat_2(X1,X2))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(cnf_transformation,[],[f29248]) ).
fof(f38534,plain,
! [X2,X3,X0,X1,X4] :
( ~ v2_cat_1(X0)
| k13_funct_3(X3,X4) = k10_isocat_2(X0,X1,X2,X3,X4)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X2) ),
inference(cnf_transformation,[],[f29250]) ).
fof(f38539,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ m1_nattra_1(X8,X0,X2,X5,X6)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X6,X0,X2)
| ~ m1_nattra_1(X7,X0,X1,X3,X4)
| m1_nattra_1(k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8),X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6)) ),
inference(cnf_transformation,[],[f29260]) ).
fof(f38633,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ m1_subset_1(X9,u1_cat_1(X0))
| k8_funct_2(u1_cat_1(X0),k2_zfmisc_1(u2_cat_1(X1),u2_cat_1(X2)),k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8),X9) = k13_cat_2(X1,X2,k5_nattra_1(X0,X1,X3,X4,X7,X9),k5_nattra_1(X0,X2,X5,X6,X8,X9))
| ~ m1_nattra_1(X8,X0,X2,X5,X6)
| ~ m1_nattra_1(X7,X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X3,X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29364]) ).
fof(f38637,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( r1_nattra_1(X0,k11_cat_2(X1,X2),k10_isocat_2(X0,X1,X2,X3,X5),k10_isocat_2(X0,X1,X2,X4,X6))
| ~ r1_nattra_1(X0,X1,X3,X4)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X3,X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29372]) ).
fof(f38638,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1_nattra_1(X0,X1,X3,X4)
| ~ m1_nattra_1(X8,X0,X2,X5,X6)
| ~ m1_nattra_1(X7,X0,X1,X3,X4)
| k15_isocat_2(X0,X1,X2,X3,X4,X5,X6,X7,X8) = k14_funct_3(u1_cat_1(X0),u2_cat_1(X1),u2_cat_1(X2),X7,X8)
| ~ r1_nattra_1(X0,X2,X5,X6)
| ~ m2_cat_1(X6,X0,X2)
| ~ m2_cat_1(X5,X0,X2)
| ~ m2_cat_1(X4,X0,X1)
| ~ m2_cat_1(X3,X0,X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29374]) ).
fof(f38639,plain,
l1_cat_1(sK62),
inference(cnf_transformation,[],[f36492]) ).
fof(f38640,plain,
v2_cat_1(sK62),
inference(cnf_transformation,[],[f36492]) ).
fof(f38641,plain,
l1_cat_1(sK63),
inference(cnf_transformation,[],[f36492]) ).
fof(f38642,plain,
v2_cat_1(sK63),
inference(cnf_transformation,[],[f36492]) ).
fof(f38643,plain,
l1_cat_1(sK64),
inference(cnf_transformation,[],[f36492]) ).
fof(f38644,plain,
v2_cat_1(sK64),
inference(cnf_transformation,[],[f36492]) ).
fof(f38645,plain,
m2_cat_1(sK65,sK62,sK63),
inference(cnf_transformation,[],[f36492]) ).
fof(f38646,plain,
m2_cat_1(sK66,sK62,sK63),
inference(cnf_transformation,[],[f36492]) ).
fof(f38647,plain,
m2_cat_1(sK67,sK62,sK64),
inference(cnf_transformation,[],[f36492]) ).
fof(f38648,plain,
m2_cat_1(sK68,sK62,sK64),
inference(cnf_transformation,[],[f36492]) ).
fof(f38649,plain,
r1_nattra_1(sK62,sK64,sK67,sK68),
inference(cnf_transformation,[],[f36492]) ).
fof(f38650,plain,
r1_nattra_1(sK62,sK63,sK65,sK66),
inference(cnf_transformation,[],[f36492]) ).
fof(f38651,plain,
m1_nattra_1(sK69,sK62,sK63,sK65,sK66),
inference(cnf_transformation,[],[f36492]) ).
fof(f38652,plain,
m1_nattra_1(sK70,sK62,sK64,sK67,sK68),
inference(cnf_transformation,[],[f36492]) ).
fof(f38653,plain,
m1_subset_1(sK71,u1_cat_1(sK62)),
inference(cnf_transformation,[],[f36492]) ).
fof(f38654,plain,
k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68),k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK71),
inference(cnf_transformation,[],[f36492]) ).
fof(f38761,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,[],[f29429]) ).
fof(f39281,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v2_cat_1(X0)
| ~ m1_subset_1(X5,u1_cat_1(X0))
| ~ m1_nattra_1(X4,X0,X1,X2,X3)
| ~ r1_nattra_1(X0,X1,X2,X3)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| k8_funct_2(u1_cat_1(X0),u2_cat_1(X1),X4,X5) = k5_nattra_1(X0,X1,X2,X3,X4,X5)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29777]) ).
fof(f39832,plain,
! [X0,X1] :
( ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| v2_cat_1(k11_cat_2(X0,X1))
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f30198]) ).
fof(f39875,plain,
! [X0,X1] :
( ~ v2_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1)) = u2_cat_1(k11_cat_2(X0,X1))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f30246]) ).
fof(f52862,plain,
! [X0] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| v2_cat_1(k11_cat_2(X0,sK64))
| ~ l1_cat_1(sK64) ),
inference(resolution,[],[f38644,f39832]) ).
fof(f52869,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,u1_cat_1(sK62))
| ~ m1_nattra_1(X1,sK62,X2,X3,X4)
| ~ r1_nattra_1(sK62,X2,X3,X4)
| ~ m2_cat_1(X4,sK62,X2)
| ~ m2_cat_1(X3,sK62,X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| k8_funct_2(u1_cat_1(sK62),u2_cat_1(X2),X1,X0) = k5_nattra_1(sK62,X2,X3,X4,X1,X0)
| ~ l1_cat_1(sK62) ),
inference(resolution,[],[f38640,f39281]) ).
fof(f52872,plain,
! [X2,X3,X0,X1] :
( k13_funct_3(X0,X1) = k10_isocat_2(sK62,X2,X3,X0,X1)
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X3)
| ~ l1_cat_1(X3)
| ~ m2_cat_1(X0,sK62,X2)
| ~ m2_cat_1(X1,sK62,X3) ),
inference(resolution,[],[f38640,f38534]) ).
fof(f52873,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(X1),X2,X3),sK71) = k13_cat_2(X0,X1,k5_nattra_1(sK62,X0,X4,X5,X2,sK71),k5_nattra_1(sK62,X1,X6,X7,X3,sK71))
| ~ m1_nattra_1(X3,sK62,X1,X6,X7)
| ~ m1_nattra_1(X2,sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X1,X6,X7)
| ~ m2_cat_1(X7,sK62,X1)
| ~ m2_cat_1(X6,sK62,X1)
| ~ m2_cat_1(X5,sK62,X0)
| ~ m2_cat_1(X4,sK62,X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(resolution,[],[f38633,f38653]) ).
fof(f52884,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(resolution,[],[f38539,f38652]) ).
fof(f52885,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(resolution,[],[f38638,f38650]) ).
fof(f52895,plain,
! [X0] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(X0)) = u2_cat_1(k11_cat_2(sK63,X0))
| ~ l1_cat_1(sK63) ),
inference(resolution,[],[f39875,f38642]) ).
fof(f52953,plain,
! [X0] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| v2_cat_1(k11_cat_2(X0,sK64)) ),
inference(forward_subsumption_resolution,[],[f52862,f38643]) ).
fof(f52959,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X2)
| k13_funct_3(X0,X1) = k10_isocat_2(sK62,X2,X3,X0,X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X3)
| ~ l1_cat_1(X3)
| ~ m2_cat_1(X0,sK62,X2)
| ~ m2_cat_1(X1,sK62,X3) ),
inference(forward_subsumption_resolution,[],[f52872,f38639]) ).
fof(f52962,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,u1_cat_1(sK62))
| ~ m1_nattra_1(X1,sK62,X2,X3,X4)
| ~ r1_nattra_1(sK62,X2,X3,X4)
| ~ m2_cat_1(X4,sK62,X2)
| ~ m2_cat_1(X3,sK62,X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| k8_funct_2(u1_cat_1(sK62),u2_cat_1(X2),X1,X0) = k5_nattra_1(sK62,X2,X3,X4,X1,X0) ),
inference(forward_subsumption_resolution,[],[f52869,f38639]) ).
fof(f52963,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(X1),X2,X3),sK71) = k13_cat_2(X0,X1,k5_nattra_1(sK62,X0,X4,X5,X2,sK71),k5_nattra_1(sK62,X1,X6,X7,X3,sK71))
| ~ m1_nattra_1(X3,sK62,X1,X6,X7)
| ~ m1_nattra_1(X2,sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X1,X6,X7)
| ~ m2_cat_1(X7,sK62,X1)
| ~ m2_cat_1(X6,sK62,X1)
| ~ m2_cat_1(X5,sK62,X0)
| ~ m2_cat_1(X4,sK62,X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f52873,f38640]) ).
fof(f52973,plain,
! [X2,X3,X0,X1] :
( ~ l1_cat_1(sK62)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f52884,f38640]) ).
fof(f52976,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f52885,f38646]) ).
fof(f52982,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(X0)) = u2_cat_1(k11_cat_2(sK63,X0)) ),
inference(forward_subsumption_resolution,[],[f52895,f38641]) ).
fof(f53017,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ m1_nattra_1(X3,sK62,X1,X6,X7)
| k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(X1)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(X1),X2,X3),sK71) = k13_cat_2(X0,X1,k5_nattra_1(sK62,X0,X4,X5,X2,sK71),k5_nattra_1(sK62,X1,X6,X7,X3,sK71))
| ~ m1_nattra_1(X2,sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X0,X4,X5)
| ~ r1_nattra_1(sK62,X1,X6,X7)
| ~ m2_cat_1(X7,sK62,X1)
| ~ m2_cat_1(X6,sK62,X1)
| ~ m2_cat_1(X5,sK62,X0)
| ~ m2_cat_1(X4,sK62,X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f52963,f38639]) ).
fof(f53024,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f52973,f38639]) ).
fof(f53027,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f52976,f38645]) ).
fof(f53038,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f53024,f38644]) ).
fof(f53041,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f53027,f38642]) ).
fof(f53048,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f53038,f38643]) ).
fof(f53051,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f53041,f38641]) ).
fof(f53058,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f53048,f38647]) ).
fof(f53061,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f53051,f38640]) ).
fof(f53068,plain,
! [X2,X3,X0,X1] :
( ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m2_cat_1(X1,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ m1_nattra_1(X3,sK62,X0,X1,X2)
| m1_nattra_1(k15_isocat_2(sK62,X0,sK64,X1,X2,sK67,sK68,X3,sK70),sK62,k11_cat_2(X0,sK64),k10_isocat_2(sK62,X0,sK64,X1,sK67),k10_isocat_2(sK62,X0,sK64,X2,sK68)) ),
inference(forward_subsumption_resolution,[],[f53058,f38648]) ).
fof(f53071,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_nattra_1(X4,sK62,sK63,sK65,sK66)
| ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,X4,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),X4,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(forward_subsumption_resolution,[],[f53061,f38639]) ).
fof(f53103,plain,
! [X2,X0,X1] :
( k13_funct_3(X0,X1) = k10_isocat_2(sK62,sK63,X2,X0,X1)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(X1,sK62,X2) ),
inference(resolution,[],[f52959,f38642]) ).
fof(f53106,plain,
! [X2,X0,X1] :
( ~ v2_cat_1(X2)
| k13_funct_3(X0,X1) = k10_isocat_2(sK62,sK63,X2,X0,X1)
| ~ l1_cat_1(X2)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(X1,sK62,X2) ),
inference(forward_subsumption_resolution,[],[f53103,f38641]) ).
fof(f53108,plain,
! [X2,X3,X0,X1] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| k8_funct_2(u1_cat_1(sK62),u2_cat_1(X1),X0,sK71) = k5_nattra_1(sK62,X1,X2,X3,X0,sK71) ),
inference(resolution,[],[f52962,f38653]) ).
fof(f53112,plain,
( ~ r1_nattra_1(sK62,sK63,sK65,sK66)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71) ),
inference(resolution,[],[f53108,f38651]) ).
fof(f53113,plain,
( ~ r1_nattra_1(sK62,sK64,sK67,sK68)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71) ),
inference(resolution,[],[f53108,f38652]) ).
fof(f53114,plain,
( ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71) ),
inference(forward_subsumption_resolution,[],[f53113,f38649]) ).
fof(f53115,plain,
( ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71) ),
inference(forward_subsumption_resolution,[],[f53112,f38650]) ).
fof(f53116,plain,
( ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71) ),
inference(forward_subsumption_resolution,[],[f53114,f38648]) ).
fof(f53117,plain,
( ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71) ),
inference(forward_subsumption_resolution,[],[f53115,f38646]) ).
fof(f53118,plain,
( ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71) ),
inference(forward_subsumption_resolution,[],[f53116,f38647]) ).
fof(f53119,plain,
( ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71) ),
inference(forward_subsumption_resolution,[],[f53117,f38645]) ).
fof(f53120,plain,
( ~ l1_cat_1(sK64)
| k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71) ),
inference(forward_subsumption_resolution,[],[f53118,f38644]) ).
fof(f53121,plain,
( ~ l1_cat_1(sK63)
| k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71) ),
inference(forward_subsumption_resolution,[],[f53119,f38642]) ).
fof(f53122,plain,
k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71),
inference(forward_subsumption_resolution,[],[f53120,f38643]) ).
fof(f53123,plain,
k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),
inference(forward_subsumption_resolution,[],[f53121,f38641]) ).
fof(f53125,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,sK64,sK67,sK68)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(resolution,[],[f53017,f38652]) ).
fof(f53126,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f53125,f38649]) ).
fof(f53128,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f53126,f38648]) ).
fof(f53130,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f53128,f38647]) ).
fof(f53132,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f53130,f38644]) ).
fof(f53134,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71))
| ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_subsumption_resolution,[],[f53132,f38643]) ).
fof(f53136,plain,
! [X2,X3,X0,X1] :
( ~ m1_nattra_1(X1,sK62,X0,X2,X3)
| k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(X0),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(X0),u2_cat_1(sK64),X1,sK70),sK71) = k13_cat_2(X0,sK64,k5_nattra_1(sK62,X0,X2,X3,X1,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ r1_nattra_1(sK62,X0,X2,X3)
| ~ m2_cat_1(X3,sK62,X0)
| ~ m2_cat_1(X2,sK62,X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(forward_demodulation,[],[f53134,f53122]) ).
fof(f53138,plain,
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ r1_nattra_1(sK62,sK63,sK65,sK66)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63) ),
inference(resolution,[],[f53136,f38651]) ).
fof(f53141,plain,
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63) ),
inference(forward_subsumption_resolution,[],[f53138,f38650]) ).
fof(f53143,plain,
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63) ),
inference(forward_subsumption_resolution,[],[f53141,f38646]) ).
fof(f53145,plain,
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63) ),
inference(forward_subsumption_resolution,[],[f53143,f38645]) ).
fof(f53147,plain,
( k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71))
| ~ l1_cat_1(sK63) ),
inference(forward_subsumption_resolution,[],[f53145,f38642]) ).
fof(f53149,plain,
k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)),
inference(forward_subsumption_resolution,[],[f53147,f38641]) ).
fof(f53151,plain,
k8_funct_2(u1_cat_1(sK62),k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)),
inference(forward_demodulation,[],[f53149,f53123]) ).
fof(f53166,plain,
! [X2,X3,X0,X1] :
( ~ m1_nattra_1(X0,sK62,X1,X2,X3)
| k15_isocat_2(sK62,sK63,X1,sK65,sK66,X2,X3,sK69,X0) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(X1),sK69,X0)
| ~ r1_nattra_1(sK62,X1,X2,X3)
| ~ m2_cat_1(X3,sK62,X1)
| ~ m2_cat_1(X2,sK62,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(resolution,[],[f53071,f38651]) ).
fof(f53168,plain,
( k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70)
| ~ r1_nattra_1(sK62,sK64,sK67,sK68)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64) ),
inference(resolution,[],[f53166,f38652]) ).
fof(f53169,plain,
( k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70)
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64) ),
inference(forward_subsumption_resolution,[],[f53168,f38649]) ).
fof(f53171,plain,
( k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64) ),
inference(forward_subsumption_resolution,[],[f53169,f38648]) ).
fof(f53173,plain,
( k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64) ),
inference(forward_subsumption_resolution,[],[f53171,f38647]) ).
fof(f53175,plain,
( k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70)
| ~ l1_cat_1(sK64) ),
inference(forward_subsumption_resolution,[],[f53173,f38644]) ).
fof(f53177,plain,
k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70) = k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),
inference(forward_subsumption_resolution,[],[f53175,f38643]) ).
fof(f53179,plain,
k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k5_nattra_1(sK62,sK64,sK67,sK68,sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(superposition,[],[f38654,f53177]) ).
fof(f53180,plain,
k13_cat_2(sK63,sK64,k5_nattra_1(sK62,sK63,sK65,sK66,sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(forward_demodulation,[],[f53179,f53122]) ).
fof(f53181,plain,
k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(forward_demodulation,[],[f53180,f53123]) ).
fof(f53213,plain,
! [X0,X1] :
( k13_funct_3(X0,X1) = k10_isocat_2(sK62,sK63,sK64,X0,X1)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(X1,sK62,sK64) ),
inference(resolution,[],[f53106,f38644]) ).
fof(f53218,plain,
! [X0,X1] :
( ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| k13_funct_3(X0,X1) = k10_isocat_2(sK62,sK63,sK64,X0,X1) ),
inference(forward_subsumption_resolution,[],[f53213,f38643]) ).
fof(f53607,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(sK63)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(X1,sK62,sK63)
| ~ m1_nattra_1(X2,sK62,sK63,X0,X1)
| m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,X0,X1,sK67,sK68,X2,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,X0,sK67),k10_isocat_2(sK62,sK63,sK64,X1,sK68)) ),
inference(resolution,[],[f53068,f38642]) ).
fof(f53610,plain,
! [X2,X0,X1] :
( ~ m1_nattra_1(X2,sK62,sK63,X0,X1)
| ~ m2_cat_1(X1,sK62,sK63)
| ~ m2_cat_1(X0,sK62,sK63)
| m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,X0,X1,sK67,sK68,X2,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,X0,sK67),k10_isocat_2(sK62,sK63,sK64,X1,sK68)) ),
inference(forward_subsumption_resolution,[],[f53607,f38641]) ).
fof(f53667,plain,
( ~ l1_cat_1(sK63)
| v2_cat_1(k11_cat_2(sK63,sK64)) ),
inference(resolution,[],[f52953,f38642]) ).
fof(f53670,plain,
v2_cat_1(k11_cat_2(sK63,sK64)),
inference(forward_subsumption_resolution,[],[f53667,f38641]) ).
fof(f54120,plain,
! [X0] :
( ~ m2_cat_1(X0,sK62,sK63)
| k13_funct_3(X0,sK67) = k10_isocat_2(sK62,sK63,sK64,X0,sK67) ),
inference(resolution,[],[f53218,f38647]) ).
fof(f54121,plain,
! [X0] :
( ~ m2_cat_1(X0,sK62,sK63)
| k13_funct_3(X0,sK68) = k10_isocat_2(sK62,sK63,sK64,X0,sK68) ),
inference(resolution,[],[f53218,f38648]) ).
fof(f54133,plain,
k10_isocat_2(sK62,sK63,sK64,sK66,sK68) = k13_funct_3(sK66,sK68),
inference(resolution,[],[f54121,f38646]) ).
fof(f54144,plain,
k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(superposition,[],[f53181,f54133]) ).
fof(f54150,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(superposition,[],[f38533,f54133]) ).
fof(f54151,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54150,f38640]) ).
fof(f54157,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54151,f38639]) ).
fof(f54163,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54157,f38642]) ).
fof(f54169,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54163,f38641]) ).
fof(f54174,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54169,f38644]) ).
fof(f54179,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54174,f38643]) ).
fof(f54184,plain,
( m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ m2_cat_1(sK68,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54179,f38646]) ).
fof(f54189,plain,
m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64)),
inference(forward_subsumption_resolution,[],[f54184,f38648]) ).
fof(f54239,plain,
k10_isocat_2(sK62,sK63,sK64,sK65,sK67) = k13_funct_3(sK65,sK67),
inference(resolution,[],[f54120,f38645]) ).
fof(f54251,plain,
k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) != k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(superposition,[],[f54144,f54239]) ).
fof(f54257,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(sK67,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(superposition,[],[f38637,f54239]) ).
fof(f54258,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(superposition,[],[f38533,f54239]) ).
fof(f54259,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK62)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54258,f38640]) ).
fof(f54260,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54257,f38647]) ).
fof(f54266,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54259,f38639]) ).
fof(f54267,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54260,f38645]) ).
fof(f54272,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54266,f38642]) ).
fof(f54273,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ l1_cat_1(sK64)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54267,f38644]) ).
fof(f54278,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54272,f38641]) ).
fof(f54279,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54273,f38643]) ).
fof(f54284,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ l1_cat_1(sK64)
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54278,f38644]) ).
fof(f54285,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54279,f38642]) ).
fof(f54289,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ m2_cat_1(sK65,sK62,sK63)
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54284,f38643]) ).
fof(f54290,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ v2_cat_1(sK62)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54285,f38641]) ).
fof(f54294,plain,
( m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ m2_cat_1(sK67,sK62,sK64) ),
inference(forward_subsumption_resolution,[],[f54289,f38645]) ).
fof(f54295,plain,
! [X0,X1] :
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63)
| ~ l1_cat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f54290,f38640]) ).
fof(f54299,plain,
m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64)),
inference(forward_subsumption_resolution,[],[f54294,f38647]) ).
fof(f54300,plain,
! [X0,X1] :
( ~ r1_nattra_1(sK62,sK64,sK67,X1)
| ~ r1_nattra_1(sK62,sK63,sK65,X0)
| r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,X1))
| ~ m2_cat_1(X1,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63) ),
inference(forward_subsumption_resolution,[],[f54295,f38639]) ).
fof(f55102,plain,
( ~ m2_cat_1(sK66,sK62,sK63)
| ~ m2_cat_1(sK65,sK62,sK63)
| m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68)) ),
inference(resolution,[],[f53610,f38651]) ).
fof(f55103,plain,
( ~ m2_cat_1(sK65,sK62,sK63)
| m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68)) ),
inference(forward_subsumption_resolution,[],[f55102,f38646]) ).
fof(f55104,plain,
m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68)),
inference(forward_subsumption_resolution,[],[f55103,f38645]) ).
fof(f55105,plain,
m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK62,k11_cat_2(sK63,sK64),k10_isocat_2(sK62,sK63,sK64,sK65,sK67),k13_funct_3(sK66,sK68)),
inference(forward_demodulation,[],[f55104,f54133]) ).
fof(f55106,plain,
m1_nattra_1(k15_isocat_2(sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70),sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68)),
inference(forward_demodulation,[],[f55105,f54239]) ).
fof(f55107,plain,
m1_nattra_1(k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68)),
inference(forward_demodulation,[],[f55106,f53177]) ).
fof(f55110,plain,
( ~ r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68))
| ~ m2_cat_1(k13_funct_3(sK66,sK68),sK62,k11_cat_2(sK63,sK64))
| ~ m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(k11_cat_2(sK63,sK64))
| ~ l1_cat_1(k11_cat_2(sK63,sK64))
| k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) ),
inference(resolution,[],[f55107,f53108]) ).
fof(f55127,plain,
( ~ r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68))
| ~ m2_cat_1(k13_funct_3(sK65,sK67),sK62,k11_cat_2(sK63,sK64))
| ~ v2_cat_1(k11_cat_2(sK63,sK64))
| ~ l1_cat_1(k11_cat_2(sK63,sK64))
| k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) ),
inference(forward_subsumption_resolution,[],[f55110,f54189]) ).
fof(f55138,plain,
( ~ r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68))
| ~ v2_cat_1(k11_cat_2(sK63,sK64))
| ~ l1_cat_1(k11_cat_2(sK63,sK64))
| k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) ),
inference(forward_subsumption_resolution,[],[f55127,f54299]) ).
fof(f55149,plain,
( ~ r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68))
| ~ l1_cat_1(k11_cat_2(sK63,sK64))
| k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) ),
inference(forward_subsumption_resolution,[],[f55138,f53670]) ).
fof(f55157,definition,
( spl1486_188
<=> l1_cat_1(k11_cat_2(sK63,sK64)) ),
introduced(definition,[new_symbols(definition,[spl1486_188])],[avatar_definition]) ).
fof(f55158,plain,
( ~ l1_cat_1(k11_cat_2(sK63,sK64))
| spl1486_188 ),
inference(avatar_component_clause,[],[f55157]) ).
fof(f55160,definition,
( spl1486_189
<=> r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68)) ),
introduced(definition,[new_symbols(definition,[spl1486_189])],[avatar_definition]) ).
fof(f55161,plain,
( ~ r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68))
| spl1486_189 ),
inference(avatar_component_clause,[],[f55160]) ).
fof(f55179,definition,
( spl1486_194
<=> k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) ),
introduced(definition,[new_symbols(definition,[spl1486_194])],[avatar_definition]) ).
fof(f55180,plain,
( k5_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71)
| ~ spl1486_194 ),
inference(avatar_component_clause,[],[f55179]) ).
fof(f55181,plain,
( spl1486_194
| ~ spl1486_188
| ~ spl1486_189 ),
inference(avatar_split_clause,[],[f55149,f55160,f55157,f55179]) ).
fof(f55211,plain,
( ~ v2_cat_1(sK63)
| ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| spl1486_188 ),
inference(resolution,[],[f55158,f38761]) ).
fof(f55213,plain,
( ~ l1_cat_1(sK63)
| ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| spl1486_188 ),
inference(forward_subsumption_resolution,[],[f55211,f38642]) ).
fof(f55214,plain,
( ~ v2_cat_1(sK64)
| ~ l1_cat_1(sK64)
| spl1486_188 ),
inference(forward_subsumption_resolution,[],[f55213,f38641]) ).
fof(f55215,plain,
( ~ l1_cat_1(sK64)
| spl1486_188 ),
inference(forward_subsumption_resolution,[],[f55214,f38644]) ).
fof(f55216,plain,
( $false
| spl1486_188 ),
inference(forward_subsumption_resolution,[],[f55215,f38643]) ).
fof(f55217,plain,
spl1486_188,
inference(avatar_contradiction_clause,[],[f55216]) ).
fof(f55939,plain,
( ~ v2_cat_1(sK64)
| k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)) = u2_cat_1(k11_cat_2(sK63,sK64)) ),
inference(resolution,[],[f52982,f38643]) ).
fof(f55940,plain,
k2_zfmisc_1(u2_cat_1(sK63),u2_cat_1(sK64)) = u2_cat_1(k11_cat_2(sK63,sK64)),
inference(forward_subsumption_resolution,[],[f55939,f38644]) ).
fof(f56701,plain,
k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) = k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71),
inference(superposition,[],[f53151,f55940]) ).
fof(f57709,plain,
! [X0] :
( ~ r1_nattra_1(sK62,sK63,sK65,X0)
| r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,sK68))
| ~ m2_cat_1(sK68,sK62,sK64)
| ~ m2_cat_1(X0,sK62,sK63) ),
inference(resolution,[],[f54300,f38649]) ).
fof(f57710,plain,
! [X0] :
( ~ r1_nattra_1(sK62,sK63,sK65,X0)
| r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,X0,sK68))
| ~ m2_cat_1(X0,sK62,sK63) ),
inference(forward_subsumption_resolution,[],[f57709,f38648]) ).
fof(f57711,plain,
( r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68))
| ~ m2_cat_1(sK66,sK62,sK63) ),
inference(resolution,[],[f57710,f38650]) ).
fof(f57712,plain,
r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k10_isocat_2(sK62,sK63,sK64,sK66,sK68)),
inference(forward_subsumption_resolution,[],[f57711,f38646]) ).
fof(f57713,plain,
r1_nattra_1(sK62,k11_cat_2(sK63,sK64),k13_funct_3(sK65,sK67),k13_funct_3(sK66,sK68)),
inference(forward_demodulation,[],[f57712,f54133]) ).
fof(f57714,plain,
( $false
| spl1486_189 ),
inference(forward_subsumption_resolution,[],[f57713,f55161]) ).
fof(f57715,plain,
spl1486_189,
inference(avatar_contradiction_clause,[],[f57714]) ).
fof(f57727,plain,
( k13_cat_2(sK63,sK64,k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK63),sK69,sK71),k8_funct_2(u1_cat_1(sK62),u2_cat_1(sK64),sK70,sK71)) != k8_funct_2(u1_cat_1(sK62),u2_cat_1(k11_cat_2(sK63,sK64)),k14_funct_3(u1_cat_1(sK62),u2_cat_1(sK63),u2_cat_1(sK64),sK69,sK70),sK71)
| ~ spl1486_194 ),
inference(superposition,[],[f54251,f55180]) ).
fof(f57728,plain,
( $false
| ~ spl1486_194 ),
inference(forward_subsumption_resolution,[],[f57727,f56701]) ).
fof(f57729,plain,
~ spl1486_194,
inference(avatar_contradiction_clause,[],[f57728]) ).
cnf(s201,plain,
( ~ spl1486_188
| ~ spl1486_189
| spl1486_194 ),
inference(sat_conversion,[],[f55181]) ).
cnf(s209,plain,
spl1486_188,
inference(sat_conversion,[],[f55217]) ).
cnf(s489,plain,
spl1486_189,
inference(sat_conversion,[],[f57715]) ).
cnf(s491,plain,
~ spl1486_194,
inference(sat_conversion,[],[f57729]) ).
cnf(s681,plain,
$false,
inference(rat,[],[s201,s491,s489,s209]) ).
fof(f57730,plain,
$false,
inference(avatar_sat_refutation,[],[s681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT031+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n020.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 21:24:33 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.38/4.32 % (577624)Detected formulas, will run a generic FOF schedule.
% 15.38/4.32 % (577632)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2709668205:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi)
% 15.38/4.32 % (577629)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=449687280:i=141193_2982 on theBenchmark for (2982ds/141193Mi)
% 15.38/4.32 % (577630)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=2722250422:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi)
% 15.38/4.32 % (577631)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=3860681061:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi)
% 15.38/4.32 % (577632)Instruction limit reached!
% 15.38/4.32 % (577632)------------------------------
% 15.38/4.32 % (577632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.38/4.32 % (577632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/4.32 % (577632)CaDiCaL version: 2.1.3
% 15.38/4.32 % (577632)Termination reason: Instruction limit
% 15.38/4.32 % (577632)Termination phase: SInE selection
% 15.38/4.32 % (577632)Time elapsed: 0.050 s
% 15.38/4.32 % (577632)Peak memory usage: 127 MB
% 15.38/4.32 % (577632)Instructions burned: 110 (million)
% 15.38/4.32 % (577634)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=282120549:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi)
% 15.38/4.32 % (577633)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2401559894:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi)
% 15.38/4.32 % (577635)dis-21_1_sil=8000:lcm=predicate:random_seed=519223155:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2982 on theBenchmark for (2982ds/129Mi)
% 15.38/4.32 % (577634)Instruction limit reached!
% 15.38/4.32 % (577634)------------------------------
% 15.38/4.32 % (577634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.38/4.32 % (577634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/4.32 % (577634)CaDiCaL version: 2.1.3
% 15.38/4.32 % (577634)Termination reason: Instruction limit
% 15.38/4.32 % (577634)Termination phase: Property scanning
% 15.38/4.32 % (577634)Time elapsed: 0.062 s
% 15.38/4.32 % (577634)Peak memory usage: 127 MB
% 15.38/4.32 % (577634)Instructions burned: 139 (million)
% 15.38/4.32 % (577633)Instruction limit reached!
% 15.38/4.32 % (577633)------------------------------
% 15.38/4.32 % (577633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.38/4.32 % (577633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/4.32 % (577633)CaDiCaL version: 2.1.3
% 15.38/4.32 % (577633)Termination reason: Instruction limit
% 15.38/4.32 % (577633)Termination phase: SInE selection
% 15.38/4.32 % (577633)Time elapsed: 0.086 s
% 15.38/4.32 % (577633)Peak memory usage: 127 MB
% 15.38/4.32 % (577633)Instructions burned: 119 (million)
% 15.38/4.32 % (577635)Instruction limit reached!
% 15.38/4.32 % (577635)------------------------------
% 15.38/4.32 % (577635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.38/4.32 % (577635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/4.32 % (577635)CaDiCaL version: 2.1.3
% 15.38/4.32 % (577635)Termination reason: Instruction limit
% 15.38/4.32 % (577635)Termination phase: SInE selection
% 15.38/4.32 % (577635)Time elapsed: 0.088 s
% 15.38/4.32 % (577635)Peak memory usage: 127 MB
% 15.38/4.32 % (577635)Instructions burned: 130 (million)
% 15.38/4.32 % (577643)lrs+10_1_sil=8000:sp=occurrence:random_seed=2203136048:i=285:sd=3:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/285Mi)
% 15.38/4.32 % (577644)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1680752281:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/157Mi)
% 15.38/4.32 % (577643)Instruction limit reached!
% 15.38/4.32 % (577643)------------------------------
% 15.38/4.32 % (577643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.38/4.32 % (577643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/4.32 % (577643)CaDiCaL version: 2.1.3
% 15.38/4.32 % (577643)Termination reason: Instruction limit
% 15.38/4.32 % (577643)Termination phase: Saturation
% 23.09/5.45 % (577643)Time elapsed: 0.127 s
% 23.09/5.45 % (577643)Peak memory usage: 133 MB
% 23.09/5.45 % (577643)Instructions burned: 288 (million)
% 23.09/5.45 % (577645)lrs+1011_1_sil=32000:sp=occurrence:random_seed=616606116:i=325:sd=1:ss=axioms:sgt=32_2979 on theBenchmark for (2979ds/325Mi)
% 23.09/5.45 % (577646)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=2759842485:s2a=on:i=248:s2at=1.23:gtg=position_2979 on theBenchmark for (2979ds/248Mi)
% 23.09/5.45 % (577644)Instruction limit reached!
% 23.09/5.45 % (577644)------------------------------
% 23.09/5.45 % (577644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.09/5.45 % (577644)CaDiCaL version: 2.1.3
% 23.09/5.45 % (577644)Termination reason: Instruction limit
% 23.09/5.45 % (577644)Termination phase: Property scanning
% 23.09/5.45 % (577644)Time elapsed: 0.070 s
% 23.09/5.45 % (577644)Peak memory usage: 127 MB
% 23.09/5.45 % (577644)Instructions burned: 158 (million)
% 23.09/5.45 % (577646)Instruction limit reached!
% 23.09/5.45 % (577646)------------------------------
% 23.09/5.45 % (577646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.09/5.45 % (577646)CaDiCaL version: 2.1.3
% 23.09/5.45 % (577646)Termination reason: Instruction limit
% 23.09/5.45 % (577646)Termination phase: Property scanning
% 23.09/5.45 % (577646)Time elapsed: 0.110 s
% 23.09/5.45 % (577646)Peak memory usage: 127 MB
% 23.09/5.45 % (577646)Instructions burned: 250 (million)
% 23.09/5.45 % (577649)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=346988707:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2978 on theBenchmark for (2978ds/294Mi)
% 23.09/5.45 % (577652)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=170593220:i=2350_2977 on theBenchmark for (2977ds/2350Mi)
% 23.09/5.45 % (577649)Instruction limit reached!
% 23.09/5.45 % (577649)------------------------------
% 23.09/5.45 % (577649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.09/5.45 % (577649)CaDiCaL version: 2.1.3
% 23.09/5.45 % (577649)Termination reason: Instruction limit
% 23.09/5.45 % (577649)Termination phase: Preprocessing 3
% 23.09/5.45 % (577649)Time elapsed: 0.123 s
% 23.09/5.45 % (577649)Peak memory usage: 130 MB
% 23.09/5.45 % (577649)Instructions burned: 295 (million)
% 23.09/5.45 % (577645)Instruction limit reached!
% 23.09/5.45 % (577645)------------------------------
% 23.09/5.45 % (577645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.09/5.45 % (577645)CaDiCaL version: 2.1.3
% 23.09/5.45 % (577645)Termination reason: Instruction limit
% 23.09/5.45 % (577645)Termination phase: Saturation
% 23.09/5.45 % (577645)Time elapsed: 0.254 s
% 23.09/5.45 % (577645)Peak memory usage: 133 MB
% 23.09/5.45 % (577645)Instructions burned: 326 (million)
% 23.09/5.45 % (577654)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3493341654:cts=off:i=113:fsr=off:ss=included:sgt=4_2977 on theBenchmark for (2977ds/113Mi)
% 23.09/5.45 % (577654)Instruction limit reached!
% 23.09/5.45 % (577654)------------------------------
% 23.09/5.45 % (577654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.09/5.45 % (577654)CaDiCaL version: 2.1.3
% 23.09/5.45 % (577654)Termination reason: Instruction limit
% 23.09/5.45 % (577654)Termination phase: SInE selection
% 23.09/5.45 % (577654)Time elapsed: 0.087 s
% 23.09/5.45 % (577654)Peak memory usage: 127 MB
% 23.09/5.45 % (577654)Instructions burned: 113 (million)
% 23.09/5.45 % (577656)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3402199354:i=127:av=off:fsr=off:sup=off_2975 on theBenchmark for (2975ds/127Mi)
% 23.09/5.45 % (577657)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1709337548:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi)
% 23.09/5.45 % (577656)Instruction limit reached!
% 23.09/5.45 % (577656)------------------------------
% 23.09/5.45 % (577656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.09/5.45 % (577656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577656)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577656)Termination reason: Instruction limit
% 22.68/7.66 % (577656)Termination phase: Preprocessing 1
% 22.68/7.66 % (577656)Time elapsed: 0.056 s
% 22.68/7.66 % (577656)Peak memory usage: 128 MB
% 22.68/7.66 % (577656)Instructions burned: 128 (million)
% 22.68/7.66 % (577657)Instruction limit reached!
% 22.68/7.66 % (577657)------------------------------
% 22.68/7.66 % (577657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577657)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577657)Termination reason: Instruction limit
% 22.68/7.66 % (577657)Termination phase: Property scanning
% 22.68/7.66 % (577657)Time elapsed: 0.052 s
% 22.68/7.66 % (577657)Peak memory usage: 127 MB
% 22.68/7.66 % (577657)Instructions burned: 116 (million)
% 22.68/7.66 % (577660)lrs+10_1_sil=8000:sp=occurrence:random_seed=2335549396:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 22.68/7.66 % (577662)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1918014086:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi)
% 22.68/7.66 % (577663)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=137912985:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi)
% 22.68/7.66 % (577662)Instruction limit reached!
% 22.68/7.66 % (577662)------------------------------
% 22.68/7.66 % (577662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577662)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577662)Termination reason: Instruction limit
% 22.68/7.66 % (577662)Termination phase: Saturation
% 22.68/7.66 % (577662)Time elapsed: 0.165 s
% 22.68/7.66 % (577662)Peak memory usage: 135 MB
% 22.68/7.66 % (577662)Instructions burned: 439 (million)
% 22.68/7.66 % (577667)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2174629848:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2971 on theBenchmark for (2971ds/134Mi)
% 22.68/7.66 % (577667)Instruction limit reached!
% 22.68/7.66 % (577667)------------------------------
% 22.68/7.66 % (577667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577667)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577667)Termination reason: Instruction limit
% 22.68/7.66 % (577667)Termination phase: SInE selection
% 22.68/7.66 % (577667)Time elapsed: 0.058 s
% 22.68/7.66 % (577667)Peak memory usage: 127 MB
% 22.68/7.66 % (577667)Instructions burned: 134 (million)
% 22.68/7.66 % (577669)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=153695522:st=8:i=592:sd=3:ep=RST:ss=axioms_2969 on theBenchmark for (2969ds/592Mi)
% 22.68/7.66 % (577660)Instruction limit reached!
% 22.68/7.66 % (577660)------------------------------
% 22.68/7.66 % (577660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577660)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577660)Termination reason: Instruction limit
% 22.68/7.66 % (577660)Termination phase: Property scanning
% 22.68/7.66 % (577660)Time elapsed: 0.573 s
% 22.68/7.66 % (577660)Peak memory usage: 149 MB
% 22.68/7.66 % (577660)Instructions burned: 907 (million)
% 22.68/7.66 % (577671)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2947248747:st=3:i=13193:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/13193Mi)
% 22.68/7.66 % (577669)Instruction limit reached!
% 22.68/7.66 % (577669)------------------------------
% 22.68/7.66 % (577669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577669)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577669)Termination reason: Instruction limit
% 22.68/7.66 % (577669)Termination phase: Preprocessing 3
% 22.68/7.66 % (577669)Time elapsed: 0.270 s
% 22.68/7.66 % (577669)Peak memory usage: 146 MB
% 22.68/7.66 % (577669)Instructions burned: 593 (million)
% 22.68/7.66 % (577673)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=1059602934:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/125Mi)
% 22.68/7.66 % (577673)Instruction limit reached!
% 22.68/7.66 % (577673)------------------------------
% 22.68/7.66 % (577673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577673)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577673)Termination reason: Instruction limit
% 22.68/7.66 % (577673)Termination phase: Property scanning
% 22.68/7.66 % (577673)Time elapsed: 0.031 s
% 22.68/7.66 % (577673)Peak memory usage: 127 MB
% 22.68/7.66 % (577673)Instructions burned: 128 (million)
% 22.68/7.66 % (577675)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1777141036:i=134:gtgl=5:slsql=off:gtg=exists_sym_2963 on theBenchmark for (2963ds/134Mi)
% 22.68/7.66 % (577675)Instruction limit reached!
% 22.68/7.66 % (577675)------------------------------
% 22.68/7.66 % (577675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577675)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577675)Termination reason: Instruction limit
% 22.68/7.66 % (577675)Termination phase: Property scanning
% 22.68/7.66 % (577675)Time elapsed: 0.033 s
% 22.68/7.66 % (577675)Peak memory usage: 127 MB
% 22.68/7.66 % (577675)Instructions burned: 134 (million)
% 22.68/7.66 % (577652)Instruction limit reached!
% 22.68/7.66 % (577652)------------------------------
% 22.68/7.66 % (577652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577652)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577652)Termination reason: Instruction limit
% 22.68/7.66 % (577652)Termination phase: Property scanning
% 22.68/7.66 % (577652)Time elapsed: 1.459 s
% 22.68/7.66 % (577652)Peak memory usage: 208 MB
% 22.68/7.66 % (577652)Instructions burned: 2351 (million)
% 22.68/7.66 % (577677)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3952194007:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi)
% 22.68/7.66 % (577677)Instruction limit reached!
% 22.68/7.66 % (577677)------------------------------
% 22.68/7.66 % (577677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577677)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577677)Termination reason: Instruction limit
% 22.68/7.66 % (577677)Termination phase: SInE selection
% 22.68/7.66 % (577677)Time elapsed: 0.062 s
% 22.68/7.66 % (577677)Peak memory usage: 127 MB
% 22.68/7.66 % (577677)Instructions burned: 141 (million)
% 22.68/7.66 % (577678)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=736986984:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi)
% 22.68/7.66 % (577680)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=1560735646:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 22.68/7.66 % (577678)Refutation not found, incomplete strategy
% 22.68/7.66 % (577678)------------------------------
% 22.68/7.66 % (577678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577678)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577678)Termination reason: Refutation not found, incomplete strategy
% 22.68/7.66 % (577678)Time elapsed: 0.169 s
% 22.68/7.66 % (577678)Peak memory usage: 132 MB
% 22.68/7.66 % (577678)Instructions burned: 206 (million)
% 22.68/7.66 % (577678)------------------------------
% 22.68/7.66 % (577678)------------------------------
% 22.68/7.66 % (577683)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=3235837135:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2955 on theBenchmark for (2955ds/150Mi)
% 22.68/7.66 % (577683)Instruction limit reached!
% 22.68/7.66 % (577683)------------------------------
% 22.68/7.66 % (577683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577683)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577683)Termination reason: Instruction limit
% 22.68/7.66 % (577683)Termination phase: SInE selection
% 22.68/7.66 % (577683)Time elapsed: 0.123 s
% 22.68/7.66 % (577683)Peak memory usage: 127 MB
% 22.68/7.66 % (577683)Instructions burned: 151 (million)
% 22.68/7.66 % (577685)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3988595128:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 22.68/7.66 % (577680)Instruction limit reached!
% 22.68/7.66 % (577680)------------------------------
% 22.68/7.66 % (577680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577680)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577680)Termination reason: Instruction limit
% 22.68/7.66 % (577680)Termination phase: Property scanning
% 22.68/7.66 % (577680)Time elapsed: 1.996 s
% 22.68/7.66 % (577680)Peak memory usage: 227 MB
% 22.68/7.66 % (577680)Instructions burned: 6064 (million)
% 22.68/7.66 % (577687)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=381187836:i=667:av=off:fsr=off_2938 on theBenchmark for (2938ds/667Mi)
% 22.68/7.66 % (577687)Instruction limit reached!
% 22.68/7.66 % (577687)------------------------------
% 22.68/7.66 % (577687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577687)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577687)Termination reason: Instruction limit
% 22.68/7.66 % (577687)Termination phase: NewCNF
% 22.68/7.66 % (577687)Time elapsed: 0.315 s
% 22.68/7.66 % (577687)Peak memory usage: 172 MB
% 22.68/7.66 % (577687)Instructions burned: 669 (million)
% 22.68/7.66 % (577630)First to succeed.
% 22.68/7.66 % (577630)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-577624"
% 22.68/7.66 % (577689)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2193683858:s2a=on:i=185:s2at=1.8:fdi=4_2933 on theBenchmark for (2933ds/185Mi)
% 22.68/7.66 % (577663)Instruction limit reached!
% 22.68/7.66 % (577663)------------------------------
% 22.68/7.66 % (577663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577663)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577663)Termination reason: Instruction limit
% 22.68/7.66 % (577663)Termination phase: Saturation
% 22.68/7.66 % (577663)Time elapsed: 3.962 s
% 22.68/7.66 % (577663)Peak memory usage: 576 MB
% 22.68/7.66 % (577663)Instructions burned: 5202 (million)
% 22.68/7.66 % (577689)Instruction limit reached!
% 22.68/7.66 % (577689)------------------------------
% 22.68/7.66 % (577689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.68/7.66 % (577689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.68/7.66 % (577689)CaDiCaL version: 2.1.3
% 22.68/7.66 % (577689)Termination reason: Instruction limit
% 22.68/7.66 % (577689)Termination phase: SInE selection
% 22.68/7.66 % (577689)Time elapsed: 0.078 s
% 22.68/7.66 % (577689)Peak memory usage: 127 MB
% 22.68/7.66 % (577689)Instructions burned: 188 (million)
% 22.68/7.66 % (577630)Refutation found. Thanks to Tanya!
% 22.68/7.66 % SZS status Theorem for theBenchmark
% 22.68/7.66 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/7.90 % (577630)------------------------------
% 0.22/7.90 % (577630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.22/7.90 % (577630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/7.90 % (577630)CaDiCaL version: 2.1.3
% 0.22/7.90 % (577630)Termination reason: Refutation
% 0.22/7.90 % (577630)Time elapsed: 4.698 s
% 0.22/7.90 % (577630)Peak memory usage: 289 MB
% 0.22/7.90 % (577630)Instructions burned: 7740 (million)
% 0.22/7.90 % (577630)------------------------------
% 0.22/7.90 % (577630)------------------------------
% 0.22/7.90 % (577624)Success in time 6.982 s
% 0.22/7.90 % Vampire exiting
%------------------------------------------------------------------------------