%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT026+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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:36:43 AM UTC 2026
% Result : Theorem 13.56s 6.32s
% Output : Refutation 29.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 17
% Syntax : Number of formulae : 177 ( 27 unt; 8 def)
% Number of atoms : 889 ( 36 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 1317 ( 605 ~; 603 |; 68 &)
% ( 8 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-5 aty)
% Number of variables : 178 ( 0 sgn 168 !; 10 ?)
% 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(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(f25789,axiom,
! [X0,X1,X2,X3] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& m2_cat_1(X2,X0,X1)
& m2_cat_1(X3,X0,X1) )
=> r2_nattra_1(X0,X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r2_nattra_1) ).
fof(f27604,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,X1,X2)
=> ! [X6] :
( m2_cat_1(X6,X1,X2)
=> ( ( r2_nattra_1(X0,X1,X3,X4)
& r2_nattra_1(X1,X2,X5,X6) )
=> r2_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X5),k2_isocat_1(X0,X1,X2,X4,X6)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_isocat_1) ).
fof(f29039,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_isocat_2) ).
fof(f29041,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_isocat_2) ).
fof(f29095,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_isocat_2) ).
fof(f29096,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_isocat_2) ).
fof(f29101,conjecture,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ( r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
=> ( r2_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4))
& r2_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_isocat_2) ).
fof(f29102,negated_conjecture,
~ ! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> ! [X3] :
( m2_cat_1(X3,X0,k11_cat_2(X1,X2))
=> ! [X4] :
( m2_cat_1(X4,X0,k11_cat_2(X1,X2))
=> ( r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
=> ( r2_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4))
& r2_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f29101]) ).
fof(f29258,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( ~ r2_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4))
| ~ r2_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) )
& r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29102]) ).
fof(f29259,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( ~ r2_nattra_1(X0,X1,k11_isocat_2(X0,X1,X2,X3),k11_isocat_2(X0,X1,X2,X4))
| ~ r2_nattra_1(X0,X2,k12_isocat_2(X0,X1,X2,X3),k12_isocat_2(X0,X1,X2,X4)) )
& r2_nattra_1(X0,k11_cat_2(X1,X2),X3,X4)
& m2_cat_1(X4,X0,k11_cat_2(X1,X2)) )
& m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(flattening,[],[f29258]) ).
fof(f29280,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( r2_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X5),k2_isocat_1(X0,X1,X2,X4,X6))
| ~ r2_nattra_1(X0,X1,X3,X4)
| ~ r2_nattra_1(X1,X2,X5,X6)
| ~ m2_cat_1(X6,X1,X2) )
| ~ m2_cat_1(X5,X1,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,[],[f27604]) ).
fof(f29281,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( r2_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X5),k2_isocat_1(X0,X1,X2,X4,X6))
| ~ r2_nattra_1(X0,X1,X3,X4)
| ~ r2_nattra_1(X1,X2,X5,X6)
| ~ m2_cat_1(X6,X1,X2) )
| ~ m2_cat_1(X5,X1,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,[],[f29280]) ).
fof(f29282,plain,
! [X0,X1,X2,X3] :
( r2_nattra_1(X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f25789]) ).
fof(f29283,plain,
! [X0,X1,X2,X3] :
( r2_nattra_1(X0,X1,X2,X2)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1) ),
inference(flattening,[],[f29282]) ).
fof(f29286,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(f29287,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,[],[f29286]) ).
fof(f29296,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29095]) ).
fof(f29297,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29296]) ).
fof(f29302,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29096]) ).
fof(f29303,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2)) )
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29302]) ).
fof(f29883,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29039]) ).
fof(f29884,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f29883]) ).
fof(f29889,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f29041]) ).
fof(f29890,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f29889]) ).
fof(f32362,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(f32363,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,[],[f32362]) ).
fof(f32934,plain,
( ( ~ r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99))
| ~ r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99)) )
& r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
& m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
& m2_cat_1(sK98,sK95,k11_cat_2(sK96,sK97))
& v2_cat_1(sK97)
& l1_cat_1(sK97)
& v2_cat_1(sK96)
& l1_cat_1(sK96)
& v2_cat_1(sK95)
& l1_cat_1(sK95) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95,sK96,sK97,sK98,sK99]),skolemize(X0,sK95),skolemize(X1,sK96),skolemize(X2,sK97),skolemize(X3,sK98),skolemize(X4,sK99)],[f29259]) ).
fof(f34084,plain,
l1_cat_1(sK95),
inference(cnf_transformation,[],[f32934]) ).
fof(f34085,plain,
v2_cat_1(sK95),
inference(cnf_transformation,[],[f32934]) ).
fof(f34086,plain,
l1_cat_1(sK96),
inference(cnf_transformation,[],[f32934]) ).
fof(f34087,plain,
v2_cat_1(sK96),
inference(cnf_transformation,[],[f32934]) ).
fof(f34088,plain,
l1_cat_1(sK97),
inference(cnf_transformation,[],[f32934]) ).
fof(f34089,plain,
v2_cat_1(sK97),
inference(cnf_transformation,[],[f32934]) ).
fof(f34090,plain,
m2_cat_1(sK98,sK95,k11_cat_2(sK96,sK97)),
inference(cnf_transformation,[],[f32934]) ).
fof(f34091,plain,
m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97)),
inference(cnf_transformation,[],[f32934]) ).
fof(f34092,plain,
r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99),
inference(cnf_transformation,[],[f32934]) ).
fof(f34093,plain,
( ~ r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99))
| ~ r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99)) ),
inference(cnf_transformation,[],[f32934]) ).
fof(f34118,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( r2_nattra_1(X0,X2,k2_isocat_1(X0,X1,X2,X3,X5),k2_isocat_1(X0,X1,X2,X4,X6))
| ~ r2_nattra_1(X0,X1,X3,X4)
| ~ r2_nattra_1(X1,X2,X5,X6)
| ~ m2_cat_1(X6,X1,X2)
| ~ m2_cat_1(X5,X1,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,[],[f29281]) ).
fof(f34119,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| r2_nattra_1(X0,X1,X2,X2) ),
inference(cnf_transformation,[],[f29283]) ).
fof(f34121,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,[],[f29287]) ).
fof(f34128,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k11_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X1,X3,k8_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29297]) ).
fof(f34131,plain,
! [X2,X3,X0,X1] :
( ~ m2_cat_1(X3,X0,k11_cat_2(X1,X2))
| k12_isocat_2(X0,X1,X2,X3) = k2_isocat_1(X0,k11_cat_2(X1,X2),X2,X3,k9_isocat_2(X1,X2))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29303]) ).
fof(f34949,plain,
! [X0,X1] :
( m2_cat_1(k8_isocat_2(X0,X1),k11_cat_2(X0,X1),X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29884]) ).
fof(f34952,plain,
! [X0,X1] :
( m2_cat_1(k9_isocat_2(X0,X1),k11_cat_2(X0,X1),X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29890]) ).
fof(f38198,plain,
! [X0,X1] :
( v2_cat_1(k11_cat_2(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f32363]) ).
fof(f41262,definition,
( spl862_19
<=> r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99)) ),
introduced(definition,[new_symbols(definition,[spl862_19])],[avatar_definition]) ).
fof(f41266,definition,
( spl862_20
<=> r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99)) ),
introduced(definition,[new_symbols(definition,[spl862_20])],[avatar_definition]) ).
fof(f41268,plain,
( ~ r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99))
| spl862_20 ),
inference(avatar_component_clause,[],[f41266]) ).
fof(f41269,plain,
( ~ spl862_19
| ~ spl862_20 ),
inference(avatar_split_clause,[],[f34093,f41266,f41262]) ).
fof(f41476,definition,
( spl862_26
<=> l1_cat_1(k11_cat_2(sK96,sK97)) ),
introduced(definition,[new_symbols(definition,[spl862_26])],[avatar_definition]) ).
fof(f41477,plain,
( l1_cat_1(k11_cat_2(sK96,sK97))
| ~ spl862_26 ),
inference(avatar_component_clause,[],[f41476]) ).
fof(f41478,plain,
( ~ l1_cat_1(k11_cat_2(sK96,sK97))
| spl862_26 ),
inference(avatar_component_clause,[],[f41476]) ).
fof(f41480,definition,
( spl862_27
<=> v2_cat_1(k11_cat_2(sK96,sK97)) ),
introduced(definition,[new_symbols(definition,[spl862_27])],[avatar_definition]) ).
fof(f41481,plain,
( v2_cat_1(k11_cat_2(sK96,sK97))
| ~ spl862_27 ),
inference(avatar_component_clause,[],[f41480]) ).
fof(f41482,plain,
( ~ v2_cat_1(k11_cat_2(sK96,sK97))
| spl862_27 ),
inference(avatar_component_clause,[],[f41480]) ).
fof(f41493,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_26 ),
inference(resolution,[],[f34121,f41478]) ).
fof(f41494,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_26 ),
inference(forward_subsumption_resolution,[],[f41493,f34087]) ).
fof(f41495,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_26 ),
inference(forward_subsumption_resolution,[],[f41494,f34086]) ).
fof(f41496,plain,
( ~ l1_cat_1(sK97)
| spl862_26 ),
inference(forward_subsumption_resolution,[],[f41495,f34089]) ).
fof(f41497,plain,
( $false
| spl862_26 ),
inference(forward_subsumption_resolution,[],[f41496,f34088]) ).
fof(f41498,plain,
spl862_26,
inference(avatar_contradiction_clause,[],[f41497]) ).
fof(f41499,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(resolution,[],[f34131,f34090]) ).
fof(f41500,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(resolution,[],[f34131,f34091]) ).
fof(f41507,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41500,f34089]) ).
fof(f41508,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41499,f34089]) ).
fof(f41511,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41507,f34088]) ).
fof(f41512,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41508,f34088]) ).
fof(f41513,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41511,f34087]) ).
fof(f41514,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41512,f34087]) ).
fof(f41515,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41513,f34086]) ).
fof(f41516,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41514,f34086]) ).
fof(f41517,plain,
( k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41515,f34085]) ).
fof(f41518,plain,
( k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41516,f34085]) ).
fof(f41519,plain,
k12_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK99,k9_isocat_2(sK96,sK97)),
inference(forward_subsumption_resolution,[],[f41517,f34084]) ).
fof(f41520,plain,
k12_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,sK98,k9_isocat_2(sK96,sK97)),
inference(forward_subsumption_resolution,[],[f41518,f34084]) ).
fof(f41521,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(resolution,[],[f34128,f34090]) ).
fof(f41522,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(resolution,[],[f34128,f34091]) ).
fof(f41529,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41522,f34089]) ).
fof(f41530,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41521,f34089]) ).
fof(f41533,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41529,f34088]) ).
fof(f41534,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41530,f34088]) ).
fof(f41535,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41533,f34087]) ).
fof(f41536,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41534,f34087]) ).
fof(f41537,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41535,f34086]) ).
fof(f41538,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41536,f34086]) ).
fof(f41539,plain,
( k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41537,f34085]) ).
fof(f41540,plain,
( k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97))
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41538,f34085]) ).
fof(f41541,plain,
k11_isocat_2(sK95,sK96,sK97,sK99) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK99,k8_isocat_2(sK96,sK97)),
inference(forward_subsumption_resolution,[],[f41539,f34084]) ).
fof(f41542,plain,
k11_isocat_2(sK95,sK96,sK97,sK98) = k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,sK98,k8_isocat_2(sK96,sK97)),
inference(forward_subsumption_resolution,[],[f41540,f34084]) ).
fof(f41544,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(sK98,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(superposition,[],[f34118,f41520]) ).
fof(f41546,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(sK98,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(superposition,[],[f34118,f41542]) ).
fof(f41555,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_27 ),
inference(resolution,[],[f38198,f41482]) ).
fof(f41556,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_27 ),
inference(forward_subsumption_resolution,[],[f41555,f34087]) ).
fof(f41557,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_27 ),
inference(forward_subsumption_resolution,[],[f41556,f34086]) ).
fof(f41558,plain,
( ~ l1_cat_1(sK97)
| spl862_27 ),
inference(forward_subsumption_resolution,[],[f41557,f34089]) ).
fof(f41559,plain,
( $false
| spl862_27 ),
inference(forward_subsumption_resolution,[],[f41558,f34088]) ).
fof(f41560,plain,
spl862_27,
inference(avatar_contradiction_clause,[],[f41559]) ).
fof(f41568,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41546,f34090]) ).
fof(f41570,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41544,f34090]) ).
fof(f41578,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41568,f34087]) ).
fof(f41580,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(sK97)
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41570,f34089]) ).
fof(f41588,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41578,f34086]) ).
fof(f41590,plain,
! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) ),
inference(forward_subsumption_resolution,[],[f41580,f34088]) ).
fof(f41598,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) )
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41588,f41481]) ).
fof(f41600,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) )
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41590,f41481]) ).
fof(f41606,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41598,f41477]) ).
fof(f41608,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK95)
| ~ l1_cat_1(sK95) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41600,f41477]) ).
fof(f41614,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(sK95) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41606,f34085]) ).
fof(f41616,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ l1_cat_1(sK95) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41608,f34085]) ).
fof(f41622,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97)) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41614,f34084]) ).
fof(f41624,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97)) )
| ~ spl862_26
| ~ spl862_27 ),
inference(forward_subsumption_resolution,[],[f41616,f34084]) ).
fof(f41626,definition,
( spl862_29
<=> m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96) ),
introduced(definition,[new_symbols(definition,[spl862_29])],[avatar_definition]) ).
fof(f41627,plain,
( m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ spl862_29 ),
inference(avatar_component_clause,[],[f41626]) ).
fof(f41628,plain,
( ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| spl862_29 ),
inference(avatar_component_clause,[],[f41626]) ).
fof(f41638,definition,
( spl862_32
<=> m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97) ),
introduced(definition,[new_symbols(definition,[spl862_32])],[avatar_definition]) ).
fof(f41639,plain,
( m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ spl862_32 ),
inference(avatar_component_clause,[],[f41638]) ).
fof(f41640,plain,
( ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| spl862_32 ),
inference(avatar_component_clause,[],[f41638]) ).
fof(f41654,definition,
( spl862_36
<=> ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0) ) ),
introduced(definition,[new_symbols(definition,[spl862_36])],[avatar_definition]) ).
fof(f41655,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK96,X0,X1))
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),X1)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0) )
| ~ spl862_36 ),
inference(avatar_component_clause,[],[f41654]) ).
fof(f41656,plain,
( ~ spl862_29
| spl862_36
| ~ spl862_26
| ~ spl862_27 ),
inference(avatar_split_clause,[],[f41622,f41480,f41476,f41654,f41626]) ).
fof(f41662,definition,
( spl862_38
<=> ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0) ) ),
introduced(definition,[new_symbols(definition,[spl862_38])],[avatar_definition]) ).
fof(f41663,plain,
( ! [X0,X1] :
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k2_isocat_1(sK95,k11_cat_2(sK96,sK97),sK97,X0,X1))
| ~ m2_cat_1(X0,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(X1,k11_cat_2(sK96,sK97),sK97)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),X1)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,X0) )
| ~ spl862_38 ),
inference(avatar_component_clause,[],[f41662]) ).
fof(f41664,plain,
( ~ spl862_32
| spl862_38
| ~ spl862_26
| ~ spl862_27 ),
inference(avatar_split_clause,[],[f41624,f41480,f41476,f41662,f41638]) ).
fof(f41669,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_32 ),
inference(resolution,[],[f34952,f41640]) ).
fof(f41677,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_32 ),
inference(forward_subsumption_resolution,[],[f41669,f34087]) ).
fof(f41681,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_32 ),
inference(forward_subsumption_resolution,[],[f41677,f34086]) ).
fof(f41684,plain,
( ~ l1_cat_1(sK97)
| spl862_32 ),
inference(forward_subsumption_resolution,[],[f41681,f34089]) ).
fof(f41685,plain,
( $false
| spl862_32 ),
inference(forward_subsumption_resolution,[],[f41684,f34088]) ).
fof(f41686,plain,
spl862_32,
inference(avatar_contradiction_clause,[],[f41685]) ).
fof(f41687,plain,
( ! [X0] :
( ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK97)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK97,X0,X0) )
| ~ spl862_32 ),
inference(resolution,[],[f41639,f34119]) ).
fof(f41688,plain,
( ! [X0] :
( ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK97)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK97,X0,X0) )
| ~ spl862_27
| ~ spl862_32 ),
inference(forward_subsumption_resolution,[],[f41687,f41481]) ).
fof(f41689,plain,
( ! [X0] :
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK97)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK97,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32 ),
inference(forward_subsumption_resolution,[],[f41688,f41477]) ).
fof(f41690,plain,
( ! [X0] :
( ~ l1_cat_1(sK97)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK97)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK97,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32 ),
inference(forward_subsumption_resolution,[],[f41689,f34089]) ).
fof(f41691,plain,
( ! [X0] :
( ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK97)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK97,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32 ),
inference(forward_subsumption_resolution,[],[f41690,f34088]) ).
fof(f41692,plain,
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_29 ),
inference(resolution,[],[f34949,f41628]) ).
fof(f41700,plain,
( ~ l1_cat_1(sK96)
| ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_29 ),
inference(forward_subsumption_resolution,[],[f41692,f34087]) ).
fof(f41704,plain,
( ~ v2_cat_1(sK97)
| ~ l1_cat_1(sK97)
| spl862_29 ),
inference(forward_subsumption_resolution,[],[f41700,f34086]) ).
fof(f41707,plain,
( ~ l1_cat_1(sK97)
| spl862_29 ),
inference(forward_subsumption_resolution,[],[f41704,f34089]) ).
fof(f41708,plain,
( $false
| spl862_29 ),
inference(forward_subsumption_resolution,[],[f41707,f34088]) ).
fof(f41709,plain,
spl862_29,
inference(avatar_contradiction_clause,[],[f41708]) ).
fof(f41710,plain,
( ! [X0] :
( ~ v2_cat_1(k11_cat_2(sK96,sK97))
| ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK96)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK96,X0,X0) )
| ~ spl862_29 ),
inference(resolution,[],[f41627,f34119]) ).
fof(f41711,plain,
( ! [X0] :
( ~ l1_cat_1(k11_cat_2(sK96,sK97))
| ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK96)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK96,X0,X0) )
| ~ spl862_27
| ~ spl862_29 ),
inference(forward_subsumption_resolution,[],[f41710,f41481]) ).
fof(f41712,plain,
( ! [X0] :
( ~ v2_cat_1(sK96)
| ~ l1_cat_1(sK96)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK96)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK96,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29 ),
inference(forward_subsumption_resolution,[],[f41711,f41477]) ).
fof(f41713,plain,
( ! [X0] :
( ~ l1_cat_1(sK96)
| ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK96)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK96,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29 ),
inference(forward_subsumption_resolution,[],[f41712,f34087]) ).
fof(f41714,plain,
( ! [X0] :
( ~ m2_cat_1(X0,k11_cat_2(sK96,sK97),sK96)
| r2_nattra_1(k11_cat_2(sK96,sK97),sK96,X0,X0) )
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29 ),
inference(forward_subsumption_resolution,[],[f41713,f34086]) ).
fof(f41717,plain,
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99))
| ~ m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK97,k9_isocat_2(sK96,sK97),k9_isocat_2(sK96,sK97))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_38 ),
inference(superposition,[],[f41663,f41519]) ).
fof(f41718,plain,
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99))
| ~ m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(forward_subsumption_resolution,[],[f41717,f41691]) ).
fof(f41721,plain,
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99))
| ~ m2_cat_1(k9_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK97)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(forward_subsumption_resolution,[],[f41718,f34091]) ).
fof(f41724,plain,
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(forward_subsumption_resolution,[],[f41721,f41639]) ).
fof(f41727,plain,
( r2_nattra_1(sK95,sK97,k12_isocat_2(sK95,sK96,sK97,sK98),k12_isocat_2(sK95,sK96,sK97,sK99))
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(forward_subsumption_resolution,[],[f41724,f34092]) ).
fof(f41738,plain,
( spl862_19
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(avatar_split_clause,[],[f41727,f41662,f41638,f41480,f41476,f41262]) ).
fof(f41815,plain,
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99))
| ~ m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(k11_cat_2(sK96,sK97),sK96,k8_isocat_2(sK96,sK97),k8_isocat_2(sK96,sK97))
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_36 ),
inference(superposition,[],[f41655,f41541]) ).
fof(f41816,plain,
( r2_nattra_1(sK95,sK96,k11_isocat_2(sK95,sK96,sK97,sK98),k11_isocat_2(sK95,sK96,sK97,sK99))
| ~ m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(forward_subsumption_resolution,[],[f41815,f41714]) ).
fof(f41818,plain,
( ~ m2_cat_1(sK99,sK95,k11_cat_2(sK96,sK97))
| ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(forward_subsumption_resolution,[],[f41816,f41268]) ).
fof(f41819,plain,
( ~ m2_cat_1(k8_isocat_2(sK96,sK97),k11_cat_2(sK96,sK97),sK96)
| ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(forward_subsumption_resolution,[],[f41818,f34091]) ).
fof(f41820,plain,
( ~ r2_nattra_1(sK95,k11_cat_2(sK96,sK97),sK98,sK99)
| spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(forward_subsumption_resolution,[],[f41819,f41627]) ).
fof(f41821,plain,
( $false
| spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(forward_subsumption_resolution,[],[f41820,f34092]) ).
fof(f41822,plain,
( spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(avatar_contradiction_clause,[],[f41821]) ).
cnf(s19,plain,
( ~ spl862_19
| ~ spl862_20 ),
inference(sat_conversion,[],[f41269]) ).
cnf(s25,plain,
spl862_26,
inference(sat_conversion,[],[f41498]) ).
cnf(s26,plain,
spl862_27,
inference(sat_conversion,[],[f41560]) ).
cnf(s32,plain,
( ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| spl862_36 ),
inference(sat_conversion,[],[f41656]) ).
cnf(s34,plain,
( ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| spl862_38 ),
inference(sat_conversion,[],[f41664]) ).
cnf(s35,plain,
spl862_32,
inference(sat_conversion,[],[f41686]) ).
cnf(s36,plain,
spl862_29,
inference(sat_conversion,[],[f41709]) ).
cnf(s38,plain,
( spl862_19
| ~ spl862_26
| ~ spl862_27
| ~ spl862_32
| ~ spl862_38 ),
inference(sat_conversion,[],[f41738]) ).
cnf(s44,plain,
( spl862_20
| ~ spl862_26
| ~ spl862_27
| ~ spl862_29
| ~ spl862_36 ),
inference(sat_conversion,[],[f41822]) ).
cnf(s45,plain,
( ~ spl862_26
| ~ spl862_27
| spl862_38 ),
inference(rat,[],[s34,s35]) ).
cnf(s47,plain,
( ~ spl862_26
| ~ spl862_27
| spl862_36 ),
inference(rat,[],[s32,s36]) ).
cnf(s53,plain,
spl862_38,
inference(rat,[],[s45,s26,s25]) ).
cnf(s55,plain,
spl862_36,
inference(rat,[],[s47,s26,s25]) ).
cnf(s61,plain,
spl862_19,
inference(rat,[],[s38,s25,s35,s26,s53]) ).
cnf(s62,plain,
spl862_20,
inference(rat,[],[s44,s25,s36,s26,s55]) ).
cnf(s64,plain,
$false,
inference(rat,[],[s19,s62,s61]) ).
fof(f41823,plain,
$false,
inference(avatar_sat_refutation,[],[s64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT026+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n002.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 21:21:13 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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
% 16.20/4.49 % (779549)Detected formulas, will run a generic FOF schedule.
% 16.20/4.49 % (779555)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=1917074426:i=141193_2982 on theBenchmark for (2982ds/141193Mi)
% 16.20/4.49 % (779556)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=2766000082:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi)
% 16.20/4.49 % (779557)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=156819686:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi)
% 16.20/4.49 % (779561)dis-21_1_sil=8000:lcm=predicate:random_seed=1576507625: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)
% 16.20/4.49 % (779559)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2246040952:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi)
% 16.20/4.49 % (779558)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2138796854:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi)
% 16.20/4.49 % (779560)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3376640779:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi)
% 16.20/4.49 % (779560)Instruction limit reached!
% 16.20/4.49 % (779560)------------------------------
% 16.20/4.49 % (779560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/4.49 % (779560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/4.49 % (779560)CaDiCaL version: 2.1.3
% 16.20/4.49 % (779560)Termination reason: Instruction limit
% 16.20/4.49 % (779560)Termination phase: Property scanning
% 16.20/4.49 % (779560)Time elapsed: 0.062 s
% 16.20/4.49 % (779560)Peak memory usage: 127 MB
% 16.20/4.49 % (779560)Instructions burned: 140 (million)
% 16.20/4.49 % (779558)Instruction limit reached!
% 16.20/4.49 % (779558)------------------------------
% 16.20/4.49 % (779558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/4.49 % (779558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/4.49 % (779558)CaDiCaL version: 2.1.3
% 16.20/4.49 % (779558)Termination reason: Instruction limit
% 16.20/4.49 % (779558)Termination phase: SInE selection
% 16.20/4.49 % (779558)Time elapsed: 0.082 s
% 16.20/4.49 % (779558)Peak memory usage: 127 MB
% 16.20/4.49 % (779558)Instructions burned: 110 (million)
% 16.20/4.49 % (779561)Instruction limit reached!
% 16.20/4.49 % (779561)------------------------------
% 16.20/4.49 % (779561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/4.49 % (779561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/4.49 % (779561)CaDiCaL version: 2.1.3
% 16.20/4.49 % (779561)Termination reason: Instruction limit
% 16.20/4.49 % (779561)Termination phase: SInE selection
% 16.20/4.49 % (779561)Time elapsed: 0.090 s
% 16.20/4.49 % (779561)Peak memory usage: 127 MB
% 16.20/4.49 % (779561)Instructions burned: 129 (million)
% 16.20/4.49 % (779559)Instruction limit reached!
% 16.20/4.49 % (779559)------------------------------
% 16.20/4.49 % (779559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/4.49 % (779559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/4.49 % (779559)CaDiCaL version: 2.1.3
% 16.20/4.49 % (779559)Termination reason: Instruction limit
% 16.20/4.49 % (779559)Termination phase: SInE selection
% 16.20/4.49 % (779559)Time elapsed: 0.090 s
% 16.20/4.49 % (779559)Peak memory usage: 127 MB
% 16.20/4.49 % (779559)Instructions burned: 119 (million)
% 16.20/4.49 % (779570)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2497160064:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/157Mi)
% 16.20/4.49 % (779569)lrs+10_1_sil=8000:sp=occurrence:random_seed=670639139:i=285:sd=3:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/285Mi)
% 16.20/4.49 % (779571)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2958539292:i=325:sd=1:ss=axioms:sgt=32_2979 on theBenchmark for (2979ds/325Mi)
% 16.20/4.49 % (779572)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=562299414:s2a=on:i=248:s2at=1.23:gtg=position_2979 on theBenchmark for (2979ds/248Mi)
% 16.20/4.49 % (779570)Instruction limit reached!
% 16.20/4.49 % (779570)------------------------------
% 23.95/5.56 % (779570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779570)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779570)Termination reason: Instruction limit
% 23.95/5.56 % (779570)Termination phase: Property scanning
% 23.95/5.56 % (779570)Time elapsed: 0.069 s
% 23.95/5.56 % (779570)Peak memory usage: 127 MB
% 23.95/5.56 % (779570)Instructions burned: 159 (million)
% 23.95/5.56 % (779572)Instruction limit reached!
% 23.95/5.56 % (779572)------------------------------
% 23.95/5.56 % (779572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779572)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779572)Termination reason: Instruction limit
% 23.95/5.56 % (779572)Termination phase: Property scanning
% 23.95/5.56 % (779572)Time elapsed: 0.108 s
% 23.95/5.56 % (779572)Peak memory usage: 127 MB
% 23.95/5.56 % (779572)Instructions burned: 249 (million)
% 23.95/5.56 % (779577)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=461103324:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2977 on theBenchmark for (2977ds/294Mi)
% 23.95/5.56 % (779569)Instruction limit reached!
% 23.95/5.56 % (779569)------------------------------
% 23.95/5.56 % (779569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779569)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779569)Termination reason: Instruction limit
% 23.95/5.56 % (779569)Termination phase: Saturation
% 23.95/5.56 % (779569)Time elapsed: 0.228 s
% 23.95/5.56 % (779569)Peak memory usage: 133 MB
% 23.95/5.56 % (779569)Instructions burned: 285 (million)
% 23.95/5.56 % (779571)Instruction limit reached!
% 23.95/5.56 % (779571)------------------------------
% 23.95/5.56 % (779571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779571)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779571)Termination reason: Instruction limit
% 23.95/5.56 % (779571)Termination phase: Saturation
% 23.95/5.56 % (779571)Time elapsed: 0.214 s
% 23.95/5.56 % (779571)Peak memory usage: 132 MB
% 23.95/5.56 % (779571)Instructions burned: 327 (million)
% 23.95/5.56 % (779578)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3266859021:i=2350_2977 on theBenchmark for (2977ds/2350Mi)
% 23.95/5.56 % (779580)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3314766107:cts=off:i=113:fsr=off:ss=included:sgt=4_2976 on theBenchmark for (2976ds/113Mi)
% 23.95/5.56 % (779581)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=437373709:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi)
% 23.95/5.56 % (779577)Instruction limit reached!
% 23.95/5.56 % (779577)------------------------------
% 23.95/5.56 % (779577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779577)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779577)Termination reason: Instruction limit
% 23.95/5.56 % (779577)Termination phase: Clausification
% 23.95/5.56 % (779577)Time elapsed: 0.214 s
% 23.95/5.56 % (779577)Peak memory usage: 130 MB
% 23.95/5.56 % (779577)Instructions burned: 296 (million)
% 23.95/5.56 % (779580)Instruction limit reached!
% 23.95/5.56 % (779580)------------------------------
% 23.95/5.56 % (779580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779580)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779580)Termination reason: Instruction limit
% 23.95/5.56 % (779580)Termination phase: SInE selection
% 23.95/5.56 % (779580)Time elapsed: 0.091 s
% 23.95/5.56 % (779580)Peak memory usage: 127 MB
% 23.95/5.56 % (779580)Instructions burned: 114 (million)
% 23.95/5.56 % (779581)Instruction limit reached!
% 23.95/5.56 % (779581)------------------------------
% 23.95/5.56 % (779581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.95/5.56 % (779581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.95/5.56 % (779581)CaDiCaL version: 2.1.3
% 23.95/5.56 % (779581)Termination reason: Instruction limit
% 23.95/5.56 % (779581)Termination phase: Preprocessing 1
% 23.95/5.56 % (779581)Time elapsed: 0.097 s
% 13.56/6.32 % (779581)Peak memory usage: 128 MB
% 13.56/6.32 % (779581)Instructions burned: 127 (million)
% 13.56/6.32 % (779585)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1986855548:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2974 on theBenchmark for (2974ds/114Mi)
% 13.56/6.32 % (779587)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=979185692:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi)
% 13.56/6.32 % (779586)lrs+10_1_sil=8000:sp=occurrence:random_seed=1882602854:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 13.56/6.32 % (779585)Instruction limit reached!
% 13.56/6.32 % (779585)------------------------------
% 13.56/6.32 % (779585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779585)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779585)Termination reason: Instruction limit
% 13.56/6.32 % (779585)Termination phase: Property scanning
% 13.56/6.32 % (779585)Time elapsed: 0.052 s
% 13.56/6.32 % (779585)Peak memory usage: 127 MB
% 13.56/6.32 % (779585)Instructions burned: 114 (million)
% 13.56/6.32 % (779591)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3603638764:i=5202:ss=axioms:sgt=16_2972 on theBenchmark for (2972ds/5202Mi)
% 13.56/6.32 % (779587)Instruction limit reached!
% 13.56/6.32 % (779587)------------------------------
% 13.56/6.32 % (779587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779587)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779587)Termination reason: Instruction limit
% 13.56/6.32 % (779587)Termination phase: Saturation
% 13.56/6.32 % (779587)Time elapsed: 0.287 s
% 13.56/6.32 % (779587)Peak memory usage: 134 MB
% 13.56/6.32 % (779587)Instructions burned: 437 (million)
% 13.56/6.32 % (779593)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4153165301:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2969 on theBenchmark for (2969ds/134Mi)
% 13.56/6.32 % (779593)Instruction limit reached!
% 13.56/6.32 % (779593)------------------------------
% 13.56/6.32 % (779593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779593)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779593)Termination reason: Instruction limit
% 13.56/6.32 % (779593)Termination phase: SInE selection
% 13.56/6.32 % (779593)Time elapsed: 0.101 s
% 13.56/6.32 % (779593)Peak memory usage: 127 MB
% 13.56/6.32 % (779593)Instructions burned: 134 (million)
% 13.56/6.32 % (779586)Instruction limit reached!
% 13.56/6.32 % (779586)------------------------------
% 13.56/6.32 % (779586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779586)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779586)Termination reason: Instruction limit
% 13.56/6.32 % (779586)Termination phase: Property scanning
% 13.56/6.32 % (779586)Time elapsed: 0.587 s
% 13.56/6.32 % (779586)Peak memory usage: 149 MB
% 13.56/6.32 % (779586)Instructions burned: 908 (million)
% 13.56/6.32 % (779595)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1872732916:st=8:i=592:sd=3:ep=RST:ss=axioms_2967 on theBenchmark for (2967ds/592Mi)
% 13.56/6.32 % (779596)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1897865168:st=3:i=13193:sd=3:ss=axioms_2966 on theBenchmark for (2966ds/13193Mi)
% 13.56/6.32 % (779595)Instruction limit reached!
% 13.56/6.32 % (779595)------------------------------
% 13.56/6.32 % (779595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779595)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779595)Termination reason: Instruction limit
% 13.56/6.32 % (779595)Termination phase: Preprocessing 3
% 13.56/6.32 % (779595)Time elapsed: 0.453 s
% 13.56/6.32 % (779595)Peak memory usage: 146 MB
% 13.56/6.32 % (779595)Instructions burned: 593 (million)
% 13.56/6.32 % (779578)Instruction limit reached!
% 13.56/6.32 % (779578)------------------------------
% 13.56/6.32 % (779578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779578)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779578)Termination reason: Instruction limit
% 13.56/6.32 % (779578)Termination phase: Property scanning
% 13.56/6.32 % (779578)Time elapsed: 1.434 s
% 13.56/6.32 % (779578)Peak memory usage: 208 MB
% 13.56/6.32 % (779578)Instructions burned: 2351 (million)
% 13.56/6.32 % (779599)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=4079620516:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/125Mi)
% 13.56/6.32 % (779600)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1890549148:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi)
% 13.56/6.32 % (779599)Instruction limit reached!
% 13.56/6.32 % (779599)------------------------------
% 13.56/6.32 % (779599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779599)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779599)Termination reason: Instruction limit
% 13.56/6.32 % (779599)Termination phase: Property scanning
% 13.56/6.32 % (779599)Time elapsed: 0.057 s
% 13.56/6.32 % (779599)Peak memory usage: 127 MB
% 13.56/6.32 % (779599)Instructions burned: 127 (million)
% 13.56/6.32 % (779600)Instruction limit reached!
% 13.56/6.32 % (779600)------------------------------
% 13.56/6.32 % (779600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779600)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779600)Termination reason: Instruction limit
% 13.56/6.32 % (779600)Termination phase: Property scanning
% 13.56/6.32 % (779600)Time elapsed: 0.059 s
% 13.56/6.32 % (779600)Peak memory usage: 127 MB
% 13.56/6.32 % (779600)Instructions burned: 135 (million)
% 13.56/6.32 % (779603)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4212884282:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/141Mi)
% 13.56/6.32 % (779604)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4293201283:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi)
% 13.56/6.32 % (779603)Instruction limit reached!
% 13.56/6.32 % (779603)------------------------------
% 13.56/6.32 % (779603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779603)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779603)Termination reason: Instruction limit
% 13.56/6.32 % (779603)Termination phase: SInE selection
% 13.56/6.32 % (779603)Time elapsed: 0.114 s
% 13.56/6.32 % (779603)Peak memory usage: 127 MB
% 13.56/6.32 % (779603)Instructions burned: 141 (million)
% 13.56/6.32 % (779607)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=2541119389:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi)
% 13.56/6.32 % (779604)Instruction limit reached!
% 13.56/6.32 % (779604)------------------------------
% 13.56/6.32 % (779604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779604)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779604)Termination reason: Instruction limit
% 13.56/6.32 % (779604)Termination phase: Saturation
% 13.56/6.32 % (779604)Time elapsed: 0.285 s
% 13.56/6.32 % (779604)Peak memory usage: 133 MB
% 13.56/6.32 % (779604)Instructions burned: 433 (million)
% 13.56/6.32 % (779609)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=2456567107:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2955 on theBenchmark for (2955ds/150Mi)
% 13.56/6.32 % (779609)Instruction limit reached!
% 13.56/6.32 % (779609)------------------------------
% 13.56/6.32 % (779609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/6.32 % (779609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/6.32 % (779609)CaDiCaL version: 2.1.3
% 13.56/6.32 % (779609)Termination reason: Instruction limit
% 13.56/6.32 % (779609)Termination phase: SInE selection
% 13.56/6.32 % (779609)Time elapsed: 0.127 s
% 13.56/6.32 % (779609)Peak memory usage: 127 MB
% 13.56/6.32 % (779609)Instructions burned: 150 (million)
% 13.56/6.32 % (779611)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2728136286:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 13.56/6.32 % (779596)First to succeed.
% 13.56/6.32 % (779596)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-779549"
% 13.56/6.32 % (779596)Refutation found. Thanks to Tanya!
% 13.56/6.32 % SZS status Theorem for theBenchmark
% 13.56/6.32 % SZS output start Proof for theBenchmark
% See solution above
% 29.45/6.43 % (779596)------------------------------
% 29.45/6.43 % (779596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.45/6.43 % (779596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.45/6.43 % (779596)CaDiCaL version: 2.1.3
% 29.45/6.43 % (779596)Termination reason: Refutation
% 29.45/6.43 % (779596)Time elapsed: 1.915 s
% 29.45/6.43 % (779596)Peak memory usage: 246 MB
% 29.45/6.43 % (779596)Instructions burned: 3969 (million)
% 29.45/6.43 % (779596)------------------------------
% 29.45/6.43 % (779596)------------------------------
% 29.45/6.43 % (779549)Success in time 5.668 s
% 29.45/6.43 % Vampire exiting
%------------------------------------------------------------------------------