%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT034+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:48 AM UTC 2026
% Result : Theorem 71.57s 22.26s
% Output : Refutation 130.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 23
% Syntax : Number of formulae : 138 ( 25 unt; 12 def)
% Number of atoms : 558 ( 47 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 696 ( 276 ~; 267 |; 82 &)
% ( 19 <=>; 52 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 13 prp; 0-5 aty)
% Number of functors : 22 ( 22 usr; 2 con; 0-7 aty)
% Number of variables : 156 ( 0 sgn 142 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f17911,axiom,
! [X0,X1] :
( ( l1_cat_1(X0)
& m1_subset_1(X1,u2_cat_1(X0)) )
=> m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_cat_1) ).
fof(f17912,axiom,
! [X0,X1] :
( ( l1_cat_1(X0)
& m1_subset_1(X1,u2_cat_1(X0)) )
=> m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_cat_1) ).
fof(f25756,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)
=> ! [X4] :
( m2_nattra_1(X4,X0,X1,X2,X3)
=> ( r2_nattra_1(X0,X1,X2,X3)
<=> r2_hidden(k4_tarski(k4_tarski(X2,X3),X4),k11_nattra_1(X0,X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_nattra_1) ).
fof(f25757,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X2) )
=> ( X2 = k12_nattra_1(X0,X1)
<=> ( u1_cat_1(X2) = k7_cat_2(X0,X1)
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& ! [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
=> ( k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3))
& k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3)) ) )
& ! [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
=> ! [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
=> ( k2_cat_1(X2,X4) = k3_cat_1(X2,X3)
=> r2_hidden(k13_cat_2(X2,X2,X4,X3),k1_relat_1(u5_cat_1(X2))) ) ) )
& ! [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
=> ! [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
=> ~ ( r2_hidden(k13_cat_2(X2,X2,X4,X3),k1_relat_1(u5_cat_1(X2)))
& ! [X5] :
( m2_cat_1(X5,X0,X1)
=> ! [X6] :
( m2_cat_1(X6,X0,X1)
=> ! [X7] :
( m2_cat_1(X7,X0,X1)
=> ! [X8] :
( m2_nattra_1(X8,X0,X1,X5,X6)
=> ! [X9] :
( m2_nattra_1(X9,X0,X1,X6,X7)
=> ~ ( X3 = k4_tarski(k4_tarski(X5,X6),X8)
& X4 = k4_tarski(k4_tarski(X6,X7),X9)
& k1_funct_1(u5_cat_1(X2),k13_cat_2(X2,X2,X4,X3)) = k4_tarski(k4_tarski(X5,X7),k8_nattra_1(X0,X1,X5,X6,X7,X8,X9)) ) ) ) ) ) ) ) ) )
& ! [X3] :
( m1_subset_1(X3,u1_cat_1(X2))
=> ! [X4] :
( m2_cat_1(X4,X0,X1)
=> ( X4 = X3
=> k10_cat_1(X2,X3) = k4_tarski(k4_tarski(X4,X4),k7_nattra_1(X0,X1,X4)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d18_nattra_1) ).
fof(f25808,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_nattra_1) ).
fof(f42641,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ( v2_cat_1(k1_yoneda_1(X0))
& l1_cat_1(k1_yoneda_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yoneda_1) ).
fof(f42642,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& m1_subset_1(X1,u1_cat_1(X0)) )
=> m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yoneda_1) ).
fof(f42643,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& m1_subset_1(X1,u2_cat_1(X0)) )
=> m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yoneda_1) ).
fof(f42650,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_yoneda_1) ).
fof(f42652,conjecture,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_yoneda_1) ).
fof(f42653,negated_conjecture,
~ ! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f42652]) ).
fof(f42659,plain,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v1_cat_1(X2)
& v2_cat_1(X2)
& l1_cat_1(X2) )
=> ( X2 = k12_nattra_1(X0,X1)
<=> ( u1_cat_1(X2) = k7_cat_2(X0,X1)
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& ! [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
=> ( k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3))
& k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3)) ) )
& ! [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
=> ! [X5] :
( m1_subset_1(X5,u2_cat_1(X2))
=> ( k3_cat_1(X2,X4) = k2_cat_1(X2,X5)
=> r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) ) )
& ! [X6] :
( m1_subset_1(X6,u2_cat_1(X2))
=> ! [X7] :
( m1_subset_1(X7,u2_cat_1(X2))
=> ~ ( r2_hidden(k13_cat_2(X2,X2,X7,X6),k1_relat_1(u5_cat_1(X2)))
& ! [X8] :
( m2_cat_1(X8,X0,X1)
=> ! [X9] :
( m2_cat_1(X9,X0,X1)
=> ! [X10] :
( m2_cat_1(X10,X0,X1)
=> ! [X11] :
( m2_nattra_1(X11,X0,X1,X8,X9)
=> ! [X12] :
( m2_nattra_1(X12,X0,X1,X9,X10)
=> ~ ( k4_tarski(k4_tarski(X8,X9),X11) = X6
& k4_tarski(k4_tarski(X9,X10),X12) = X7
& k1_funct_1(u5_cat_1(X2),k13_cat_2(X2,X2,X7,X6)) = k4_tarski(k4_tarski(X8,X10),k8_nattra_1(X0,X1,X8,X9,X10,X11,X12)) ) ) ) ) ) ) ) ) )
& ! [X13] :
( m1_subset_1(X13,u1_cat_1(X2))
=> ! [X14] :
( m2_cat_1(X14,X0,X1)
=> ( X13 = X14
=> k10_cat_1(X2,X13) = k4_tarski(k4_tarski(X14,X14),k7_nattra_1(X0,X1,X14)) ) ) ) ) ) ) ) ),
inference(rectify,[],[f25757]) ).
fof(f42697,plain,
? [X0] :
( ? [X1] :
( ~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0))))
& m1_subset_1(X1,u2_cat_1(X0)) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(ennf_transformation,[],[f42653]) ).
fof(f42698,plain,
? [X0] :
( ? [X1] :
( ~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0))))
& m1_subset_1(X1,u2_cat_1(X0)) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(flattening,[],[f42697]) ).
fof(f42759,plain,
! [X0,X1] :
( m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(ennf_transformation,[],[f17911]) ).
fof(f42760,plain,
! [X0,X1] :
( m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(flattening,[],[f42759]) ).
fof(f42763,plain,
! [X0,X1] :
( m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(ennf_transformation,[],[f17912]) ).
fof(f42764,plain,
! [X0,X1] :
( m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(flattening,[],[f42763]) ).
fof(f42819,plain,
! [X0,X1] :
( ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f25808]) ).
fof(f42820,plain,
! [X0,X1] :
( ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f42819]) ).
fof(f42831,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k12_nattra_1(X0,X1)
<=> ( u1_cat_1(X2) = k7_cat_2(X0,X1)
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& ! [X3] :
( ( k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3))
& k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3)) )
| ~ m1_subset_1(X3,u2_cat_1(X2)) )
& ! [X4] :
( ! [X5] :
( r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2)))
| k3_cat_1(X2,X4) != k2_cat_1(X2,X5)
| ~ m1_subset_1(X5,u2_cat_1(X2)) )
| ~ m1_subset_1(X4,u2_cat_1(X2)) )
& ! [X6] :
( ! [X7] :
( ~ r2_hidden(k13_cat_2(X2,X2,X7,X6),k1_relat_1(u5_cat_1(X2)))
| ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ? [X12] :
( k4_tarski(k4_tarski(X8,X9),X11) = X6
& k4_tarski(k4_tarski(X9,X10),X12) = X7
& k1_funct_1(u5_cat_1(X2),k13_cat_2(X2,X2,X7,X6)) = k4_tarski(k4_tarski(X8,X10),k8_nattra_1(X0,X1,X8,X9,X10,X11,X12))
& m2_nattra_1(X12,X0,X1,X9,X10) )
& m2_nattra_1(X11,X0,X1,X8,X9) )
& m2_cat_1(X10,X0,X1) )
& m2_cat_1(X9,X0,X1) )
& m2_cat_1(X8,X0,X1) )
| ~ m1_subset_1(X7,u2_cat_1(X2)) )
| ~ m1_subset_1(X6,u2_cat_1(X2)) )
& ! [X13] :
( ! [X14] :
( k10_cat_1(X2,X13) = k4_tarski(k4_tarski(X14,X14),k7_nattra_1(X0,X1,X14))
| X13 != X14
| ~ m2_cat_1(X14,X0,X1) )
| ~ m1_subset_1(X13,u1_cat_1(X2)) ) ) )
| ~ v1_cat_1(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,[],[f42659]) ).
fof(f42832,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k12_nattra_1(X0,X1)
<=> ( u1_cat_1(X2) = k7_cat_2(X0,X1)
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& ! [X3] :
( ( k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3))
& k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3)) )
| ~ m1_subset_1(X3,u2_cat_1(X2)) )
& ! [X4] :
( ! [X5] :
( r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2)))
| k3_cat_1(X2,X4) != k2_cat_1(X2,X5)
| ~ m1_subset_1(X5,u2_cat_1(X2)) )
| ~ m1_subset_1(X4,u2_cat_1(X2)) )
& ! [X6] :
( ! [X7] :
( ~ r2_hidden(k13_cat_2(X2,X2,X7,X6),k1_relat_1(u5_cat_1(X2)))
| ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ? [X12] :
( k4_tarski(k4_tarski(X8,X9),X11) = X6
& k4_tarski(k4_tarski(X9,X10),X12) = X7
& k1_funct_1(u5_cat_1(X2),k13_cat_2(X2,X2,X7,X6)) = k4_tarski(k4_tarski(X8,X10),k8_nattra_1(X0,X1,X8,X9,X10,X11,X12))
& m2_nattra_1(X12,X0,X1,X9,X10) )
& m2_nattra_1(X11,X0,X1,X8,X9) )
& m2_cat_1(X10,X0,X1) )
& m2_cat_1(X9,X0,X1) )
& m2_cat_1(X8,X0,X1) )
| ~ m1_subset_1(X7,u2_cat_1(X2)) )
| ~ m1_subset_1(X6,u2_cat_1(X2)) )
& ! [X13] :
( ! [X14] :
( k10_cat_1(X2,X13) = k4_tarski(k4_tarski(X14,X14),k7_nattra_1(X0,X1,X14))
| X13 != X14
| ~ m2_cat_1(X14,X0,X1) )
| ~ m1_subset_1(X13,u1_cat_1(X2)) ) ) )
| ~ v1_cat_1(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,[],[f42831]) ).
fof(f42835,plain,
! [X0] :
( ! [X1] :
( r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ m1_subset_1(X1,u2_cat_1(X0)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f42650]) ).
fof(f42836,plain,
! [X0] :
( ! [X1] :
( r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ m1_subset_1(X1,u2_cat_1(X0)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f42835]) ).
fof(f42843,plain,
! [X0,X1] :
( m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(ennf_transformation,[],[f42643]) ).
fof(f42844,plain,
! [X0,X1] :
( m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(flattening,[],[f42843]) ).
fof(f42845,plain,
! [X0,X1] :
( m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u1_cat_1(X0)) ),
inference(ennf_transformation,[],[f42642]) ).
fof(f42846,plain,
! [X0,X1] :
( m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u1_cat_1(X0)) ),
inference(flattening,[],[f42845]) ).
fof(f42847,plain,
! [X0] :
( ( v2_cat_1(k1_yoneda_1(X0))
& l1_cat_1(k1_yoneda_1(X0)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f42641]) ).
fof(f42848,plain,
! [X0] :
( ( v2_cat_1(k1_yoneda_1(X0))
& l1_cat_1(k1_yoneda_1(X0)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f42847]) ).
fof(f42857,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f43486,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r2_nattra_1(X0,X1,X2,X3)
<=> r2_hidden(k4_tarski(k4_tarski(X2,X3),X4),k11_nattra_1(X0,X1)) )
| ~ m2_nattra_1(X4,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,[],[f25756]) ).
fof(f43487,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r2_nattra_1(X0,X1,X2,X3)
<=> r2_hidden(k4_tarski(k4_tarski(X2,X3),X4),k11_nattra_1(X0,X1)) )
| ~ m2_nattra_1(X4,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,[],[f43486]) ).
fof(f43629,plain,
m1_subset_1(sK1,u2_cat_1(sK0)),
inference(cnf_transformation,[],[f42698]) ).
fof(f43630,plain,
~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),u2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))),
inference(cnf_transformation,[],[f42698]) ).
fof(f43631,plain,
l1_cat_1(sK0),
inference(cnf_transformation,[],[f42698]) ).
fof(f43632,plain,
v2_cat_1(sK0),
inference(cnf_transformation,[],[f42698]) ).
fof(f43771,plain,
! [X0,X1] :
( m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(cnf_transformation,[],[f42760]) ).
fof(f43776,plain,
! [X0,X1] :
( m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(cnf_transformation,[],[f42764]) ).
fof(f43839,plain,
! [X0,X1] :
( l1_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f42820]) ).
fof(f43840,plain,
! [X0,X1] :
( v2_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f42820]) ).
fof(f43841,plain,
! [X0,X1] :
( v1_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f42820]) ).
fof(f43893,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ v1_cat_1(X2)
| u2_cat_1(X2) = k11_nattra_1(X0,X1)
| k12_nattra_1(X0,X1) != X2 ),
inference(cnf_transformation,[],[f42832]) ).
fof(f43898,plain,
! [X0,X1] :
( r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ v2_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f42836]) ).
fof(f43902,plain,
! [X0,X1] :
( m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1)))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0)) ),
inference(cnf_transformation,[],[f42844]) ).
fof(f43903,plain,
! [X0,X1] :
( m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_subset_1(X1,u1_cat_1(X0)) ),
inference(cnf_transformation,[],[f42846]) ).
fof(f43904,plain,
! [X0] :
( l1_cat_1(k1_yoneda_1(X0))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f42848]) ).
fof(f43905,plain,
! [X0] :
( v2_cat_1(k1_yoneda_1(X0))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f42848]) ).
fof(f43912,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f42857]) ).
fof(f44711,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(k4_tarski(k4_tarski(X2,X3),X4),k11_nattra_1(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ m2_cat_1(X3,X0,X1)
| ~ m2_nattra_1(X4,X0,X1,X2,X3)
| ~ l1_cat_1(X0)
| ~ r2_nattra_1(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f43487]) ).
fof(f45056,plain,
! [X0,X1] :
( k11_nattra_1(X0,X1) = u2_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(k12_nattra_1(X0,X1))
| ~ v1_cat_1(k12_nattra_1(X0,X1))
| ~ l1_cat_1(X0) ),
inference(equality_resolution,[],[f43893]) ).
fof(f45148,plain,
~ r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),u2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))),
inference(resolution,[],[f43630,f43912]) ).
fof(f45158,definition,
( spl261_1
<=> v2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0))) ),
introduced(definition,[new_symbols(definition,[spl261_1])],[avatar_definition]) ).
fof(f45160,plain,
( ~ v2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| spl261_1 ),
inference(avatar_component_clause,[],[f45158]) ).
fof(f45162,definition,
( spl261_2
<=> l1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0))) ),
introduced(definition,[new_symbols(definition,[spl261_2])],[avatar_definition]) ).
fof(f45164,plain,
( ~ l1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| spl261_2 ),
inference(avatar_component_clause,[],[f45162]) ).
fof(f45186,definition,
( spl261_6
<=> v1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0))) ),
introduced(definition,[new_symbols(definition,[spl261_6])],[avatar_definition]) ).
fof(f45188,plain,
( ~ v1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| spl261_6 ),
inference(avatar_component_clause,[],[f45186]) ).
fof(f45190,definition,
( spl261_7
<=> v2_cat_1(k1_yoneda_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_7])],[avatar_definition]) ).
fof(f45192,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| spl261_7 ),
inference(avatar_component_clause,[],[f45190]) ).
fof(f45194,definition,
( spl261_8
<=> l1_cat_1(k1_yoneda_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_8])],[avatar_definition]) ).
fof(f45196,plain,
( ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_8 ),
inference(avatar_component_clause,[],[f45194]) ).
fof(f45203,definition,
( spl261_10
<=> m1_subset_1(k2_cat_1(sK0,sK1),u1_cat_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_10])],[avatar_definition]) ).
fof(f45205,plain,
( ~ m1_subset_1(k2_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_10 ),
inference(avatar_component_clause,[],[f45203]) ).
fof(f45221,definition,
( spl261_14
<=> m1_subset_1(k3_cat_1(sK0,sK1),u1_cat_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_14])],[avatar_definition]) ).
fof(f45223,plain,
( ~ m1_subset_1(k3_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_14 ),
inference(avatar_component_clause,[],[f45221]) ).
fof(f45234,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_1 ),
inference(resolution,[],[f45160,f43840]) ).
fof(f45235,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_1 ),
inference(global_subsumption,[],[f45234,f43632,f43631]) ).
fof(f45236,plain,
( ~ spl261_8
| ~ spl261_7
| spl261_1 ),
inference(avatar_split_clause,[],[f45235,f45158,f45190,f45194]) ).
fof(f45237,plain,
( ~ v2_cat_1(sK0)
| ~ l1_cat_1(sK0)
| spl261_7 ),
inference(resolution,[],[f45192,f43905]) ).
fof(f45238,plain,
( $false
| spl261_7 ),
inference(global_subsumption,[],[f45237,f43632,f43631]) ).
fof(f45239,plain,
spl261_7,
inference(avatar_contradiction_clause,[],[f45238]) ).
fof(f45240,plain,
( ~ v2_cat_1(sK0)
| ~ l1_cat_1(sK0)
| spl261_8 ),
inference(resolution,[],[f45196,f43904]) ).
fof(f45241,plain,
( $false
| spl261_8 ),
inference(global_subsumption,[],[f45240,f43632,f43631]) ).
fof(f45242,plain,
spl261_8,
inference(avatar_contradiction_clause,[],[f45241]) ).
fof(f45243,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_2 ),
inference(resolution,[],[f45164,f43839]) ).
fof(f45244,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_2 ),
inference(global_subsumption,[],[f45243,f43632,f43631]) ).
fof(f45245,plain,
( ~ spl261_8
| ~ spl261_7
| spl261_2 ),
inference(avatar_split_clause,[],[f45244,f45162,f45190,f45194]) ).
fof(f45246,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_6 ),
inference(resolution,[],[f45188,f43841]) ).
fof(f45247,plain,
( ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k1_yoneda_1(sK0))
| spl261_6 ),
inference(global_subsumption,[],[f45246,f43632,f43631]) ).
fof(f45248,plain,
( ~ spl261_8
| ~ spl261_7
| spl261_6 ),
inference(avatar_split_clause,[],[f45247,f45186,f45190,f45194]) ).
fof(f45249,plain,
( ~ l1_cat_1(sK0)
| ~ m1_subset_1(sK1,u2_cat_1(sK0))
| spl261_10 ),
inference(resolution,[],[f45205,f43771]) ).
fof(f45269,plain,
( $false
| spl261_10 ),
inference(global_subsumption,[],[f45249,f43631,f43629]) ).
fof(f45270,plain,
spl261_10,
inference(avatar_contradiction_clause,[],[f45269]) ).
fof(f45271,plain,
( ~ l1_cat_1(sK0)
| ~ m1_subset_1(sK1,u2_cat_1(sK0))
| spl261_14 ),
inference(resolution,[],[f45223,f43776]) ).
fof(f45288,plain,
( $false
| spl261_14 ),
inference(global_subsumption,[],[f45271,f43631,f43629]) ).
fof(f45289,plain,
spl261_14,
inference(avatar_contradiction_clause,[],[f45288]) ).
fof(f45403,plain,
( ~ r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),k11_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v2_cat_1(sK0)
| ~ l1_cat_1(k1_yoneda_1(sK0))
| ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ l1_cat_1(sK0) ),
inference(superposition,[],[f45148,f45056]) ).
fof(f45411,plain,
( ~ r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),k11_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ l1_cat_1(k1_yoneda_1(sK0))
| ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0))) ),
inference(global_subsumption,[],[f45403,f43632,f43631]) ).
fof(f45425,definition,
( spl261_37
<=> r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),k11_nattra_1(sK0,k1_yoneda_1(sK0))) ),
introduced(definition,[new_symbols(definition,[spl261_37])],[avatar_definition]) ).
fof(f45427,plain,
( ~ r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),k11_nattra_1(sK0,k1_yoneda_1(sK0)))
| spl261_37 ),
inference(avatar_component_clause,[],[f45425]) ).
fof(f45476,plain,
( ~ r2_hidden(k4_tarski(k4_tarski(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))),k3_yoneda_1(sK0,sK1)),k11_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ l1_cat_1(k1_yoneda_1(sK0))
| ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ l1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v2_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0)))
| ~ v1_cat_1(k12_nattra_1(sK0,k1_yoneda_1(sK0))) ),
inference(global_subsumption,[],[f45411]) ).
fof(f45482,plain,
( ~ spl261_6
| ~ spl261_1
| ~ spl261_2
| ~ spl261_7
| ~ spl261_8
| ~ spl261_37 ),
inference(avatar_split_clause,[],[f45476,f45425,f45194,f45190,f45162,f45158,f45186]) ).
fof(f45580,definition,
( spl261_55
<=> r2_nattra_1(sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl261_55])],[avatar_definition]) ).
fof(f45582,plain,
( ~ r2_nattra_1(sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| spl261_55 ),
inference(avatar_component_clause,[],[f45580]) ).
fof(f45584,definition,
( spl261_56
<=> m2_nattra_1(k3_yoneda_1(sK0,sK1),sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl261_56])],[avatar_definition]) ).
fof(f45586,plain,
( ~ m2_nattra_1(k3_yoneda_1(sK0,sK1),sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| spl261_56 ),
inference(avatar_component_clause,[],[f45584]) ).
fof(f45588,definition,
( spl261_57
<=> m2_cat_1(k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_57])],[avatar_definition]) ).
fof(f45590,plain,
( ~ m2_cat_1(k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| spl261_57 ),
inference(avatar_component_clause,[],[f45588]) ).
fof(f45592,definition,
( spl261_58
<=> m2_cat_1(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl261_58])],[avatar_definition]) ).
fof(f45594,plain,
( ~ m2_cat_1(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| spl261_58 ),
inference(avatar_component_clause,[],[f45592]) ).
fof(f45686,plain,
( ~ v2_cat_1(sK0)
| ~ m1_subset_1(sK1,u2_cat_1(sK0))
| ~ l1_cat_1(sK0)
| spl261_55 ),
inference(resolution,[],[f45582,f43898]) ).
fof(f45708,plain,
( $false
| spl261_55 ),
inference(global_subsumption,[],[f45686,f43632,f43631,f43629]) ).
fof(f45709,plain,
spl261_55,
inference(avatar_contradiction_clause,[],[f45708]) ).
fof(f45738,plain,
( ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m1_subset_1(sK1,u2_cat_1(sK0))
| spl261_56 ),
inference(resolution,[],[f45586,f43902]) ).
fof(f45756,plain,
( $false
| spl261_56 ),
inference(global_subsumption,[],[f45738,f43632,f43631,f43629]) ).
fof(f45757,plain,
spl261_56,
inference(avatar_contradiction_clause,[],[f45756]) ).
fof(f45782,plain,
( ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m1_subset_1(k2_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_57 ),
inference(resolution,[],[f45590,f43903]) ).
fof(f45787,plain,
( ~ m1_subset_1(k2_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_57 ),
inference(global_subsumption,[],[f45782,f43632,f43631]) ).
fof(f45794,plain,
( ~ spl261_10
| spl261_57 ),
inference(avatar_split_clause,[],[f45787,f45588,f45203]) ).
fof(f45796,plain,
( ~ v2_cat_1(sK0)
| ~ l1_cat_1(k1_yoneda_1(sK0))
| ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ m2_cat_1(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| ~ m2_cat_1(k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| ~ m2_nattra_1(k3_yoneda_1(sK0,sK1),sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| ~ l1_cat_1(sK0)
| ~ r2_nattra_1(sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| spl261_37 ),
inference(resolution,[],[f45427,f44711]) ).
fof(f45809,plain,
( ~ l1_cat_1(k1_yoneda_1(sK0))
| ~ v2_cat_1(k1_yoneda_1(sK0))
| ~ r2_nattra_1(sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| ~ m2_nattra_1(k3_yoneda_1(sK0,sK1),sK0,k1_yoneda_1(sK0),k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)))
| ~ m2_cat_1(k2_yoneda_1(sK0,k2_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| ~ m2_cat_1(k2_yoneda_1(sK0,k3_cat_1(sK0,sK1)),sK0,k1_yoneda_1(sK0))
| spl261_37 ),
inference(global_subsumption,[],[f45796,f43632,f43631]) ).
fof(f45815,plain,
( ~ spl261_58
| ~ spl261_57
| ~ spl261_56
| ~ spl261_55
| ~ spl261_7
| ~ spl261_8
| spl261_37 ),
inference(avatar_split_clause,[],[f45809,f45425,f45194,f45190,f45580,f45584,f45588,f45592]) ).
fof(f45816,plain,
( ~ l1_cat_1(sK0)
| ~ v2_cat_1(sK0)
| ~ m1_subset_1(k3_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_58 ),
inference(resolution,[],[f45594,f43903]) ).
fof(f45822,plain,
( ~ m1_subset_1(k3_cat_1(sK0,sK1),u1_cat_1(sK0))
| spl261_58 ),
inference(global_subsumption,[],[f45816,f43632,f43631]) ).
fof(f45829,plain,
( ~ spl261_14
| spl261_58 ),
inference(avatar_split_clause,[],[f45822,f45592,f45221]) ).
cnf(s38,plain,
( spl261_1
| ~ spl261_7
| ~ spl261_8 ),
inference(sat_conversion,[],[f45236]) ).
cnf(s41,plain,
spl261_7,
inference(sat_conversion,[],[f45239]) ).
cnf(s45,plain,
spl261_8,
inference(sat_conversion,[],[f45242]) ).
cnf(s51,plain,
( spl261_2
| ~ spl261_7
| ~ spl261_8 ),
inference(sat_conversion,[],[f45245]) ).
cnf(s57,plain,
( spl261_6
| ~ spl261_7
| ~ spl261_8 ),
inference(sat_conversion,[],[f45248]) ).
cnf(s70,plain,
spl261_10,
inference(sat_conversion,[],[f45270]) ).
cnf(s84,plain,
spl261_14,
inference(sat_conversion,[],[f45289]) ).
cnf(s194,plain,
( ~ spl261_1
| ~ spl261_2
| ~ spl261_6
| ~ spl261_7
| ~ spl261_8
| ~ spl261_37 ),
inference(sat_conversion,[],[f45482]) ).
cnf(s351,plain,
spl261_55,
inference(sat_conversion,[],[f45709]) ).
cnf(s386,plain,
spl261_56,
inference(sat_conversion,[],[f45757]) ).
cnf(s413,plain,
( ~ spl261_10
| spl261_57 ),
inference(sat_conversion,[],[f45794]) ).
cnf(s438,plain,
( ~ spl261_7
| ~ spl261_8
| spl261_37
| ~ spl261_55
| ~ spl261_56
| ~ spl261_57
| ~ spl261_58 ),
inference(sat_conversion,[],[f45815]) ).
cnf(s447,plain,
( ~ spl261_14
| spl261_58 ),
inference(sat_conversion,[],[f45829]) ).
cnf(s454,plain,
spl261_58,
inference(rat,[],[s447,s84]) ).
cnf(s456,plain,
spl261_57,
inference(rat,[],[s413,s70]) ).
cnf(s458,plain,
spl261_37,
inference(rat,[],[s438,s454,s456,s386,s351,s45,s41]) ).
cnf(s460,plain,
spl261_6,
inference(rat,[],[s57,s45,s41]) ).
cnf(s461,plain,
spl261_2,
inference(rat,[],[s51,s45,s41]) ).
cnf(s462,plain,
~ spl261_1,
inference(rat,[],[s194,s458,s45,s41,s460,s461]) ).
cnf(s463,plain,
$false,
inference(rat,[],[s38,s45,s41,s462]) ).
fof(f45830,plain,
$false,
inference(avatar_sat_refutation,[],[s463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CAT034+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.27 % Computer : n026.cluster.edu
% 0.24/0.27 % Model : x86_64 x86_64
% 0.24/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.27 % Memory : 8046.5625MB
% 0.24/0.27 % OS : Linux 6.8.0-71-generic
% 0.24/0.27 % CPULimit : 300
% 0.24/0.27 % WCLimit : 300
% 0.24/0.27 % DateTime : Mon Sep 28 21:26:48 UTC 2026
% 0.24/0.28 % CPUTime :
% 0.24/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.32 Running first-order theorem proving
% 0.24/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.80/7.37 % (90812)Detected formulas, will run a generic FOF schedule.
% 24.80/7.37 % (90831)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=1668014273:i=141193_2964 on theBenchmark for (2964ds/141193Mi)
% 24.80/7.37 % (90837)dis-21_1_sil=8000:lcm=predicate:random_seed=715535688:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2964 on theBenchmark for (2964ds/129Mi)
% 24.80/7.37 % (90832)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=287716553:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2964 on theBenchmark for (2964ds/134677Mi)
% 24.80/7.37 % (90833)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=410045317:i=141695:sd=1:nm=32:gsp=on:ss=included_2964 on theBenchmark for (2964ds/141695Mi)
% 24.80/7.37 % (90834)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4043359235:i=109:sd=1:ins=1:gsp=on:ss=axioms_2964 on theBenchmark for (2964ds/109Mi)
% 24.80/7.37 % (90835)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=487026113:i=119:av=off:ss=axioms_2964 on theBenchmark for (2964ds/119Mi)
% 24.80/7.37 % (90836)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3427353196:s2a=on:i=139:gtg=position_2964 on theBenchmark for (2964ds/139Mi)
% 24.80/7.37 % (90837)Instruction limit reached!
% 24.80/7.37 % (90837)------------------------------
% 24.80/7.37 % (90837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/7.37 % (90837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/7.37 % (90837)CaDiCaL version: 2.1.3
% 24.80/7.37 % (90837)Termination reason: Instruction limit
% 24.80/7.37 % (90837)Termination phase: SInE selection
% 24.80/7.37 % (90837)Time elapsed: 0.089 s
% 24.80/7.37 % (90837)Peak memory usage: 148 MB
% 24.80/7.37 % (90837)Instructions burned: 129 (million)
% 24.80/7.37 % (90834)Instruction limit reached!
% 24.80/7.37 % (90834)------------------------------
% 24.80/7.37 % (90834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/7.37 % (90834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/7.37 % (90834)CaDiCaL version: 2.1.3
% 24.80/7.37 % (90834)Termination reason: Instruction limit
% 24.80/7.37 % (90834)Termination phase: SInE selection
% 24.80/7.37 % (90834)Time elapsed: 0.118 s
% 24.80/7.37 % (90834)Peak memory usage: 148 MB
% 24.80/7.37 % (90834)Instructions burned: 109 (million)
% 24.80/7.37 % (90835)Instruction limit reached!
% 24.80/7.37 % (90835)------------------------------
% 24.80/7.37 % (90835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/7.37 % (90835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/7.37 % (90835)CaDiCaL version: 2.1.3
% 24.80/7.37 % (90835)Termination reason: Instruction limit
% 24.80/7.37 % (90835)Termination phase: SInE selection
% 24.80/7.37 % (90835)Time elapsed: 0.128 s
% 24.80/7.37 % (90835)Peak memory usage: 148 MB
% 24.80/7.37 % (90835)Instructions burned: 119 (million)
% 24.80/7.37 % (90836)Instruction limit reached!
% 24.80/7.37 % (90836)------------------------------
% 24.80/7.37 % (90836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.80/7.37 % (90836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.80/7.37 % (90836)CaDiCaL version: 2.1.3
% 24.80/7.37 % (90836)Termination reason: Instruction limit
% 24.80/7.37 % (90836)Termination phase: Property scanning
% 24.80/7.37 % (90836)Time elapsed: 0.116 s
% 24.80/7.37 % (90836)Peak memory usage: 149 MB
% 24.80/7.37 % (90836)Instructions burned: 139 (million)
% 24.80/7.37 % (90845)lrs+10_1_sil=8000:sp=occurrence:random_seed=2025634174:i=285:sd=3:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/285Mi)
% 24.80/7.37 % (90846)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3137849024:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/157Mi)
% 24.80/7.37 % (90847)lrs+1011_1_sil=32000:sp=occurrence:random_seed=137627721:i=325:sd=1:ss=axioms:sgt=32_2960 on theBenchmark for (2960ds/325Mi)
% 24.80/7.37 % (90848)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=2559770972:s2a=on:i=248:s2at=1.23:gtg=position_2960 on theBenchmark for (2960ds/248Mi)
% 24.80/7.37 % (90845)Instruction limit reached!
% 24.80/7.37 % (90845)------------------------------
% 24.80/7.37 % (90845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90845)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90845)Termination reason: Instruction limit
% 51.44/11.09 % (90845)Termination phase: SInE selection
% 51.44/11.09 % (90845)Time elapsed: 0.184 s
% 51.44/11.09 % (90845)Peak memory usage: 149 MB
% 51.44/11.09 % (90845)Instructions burned: 285 (million)
% 51.44/11.09 % (90846)Instruction limit reached!
% 51.44/11.09 % (90846)------------------------------
% 51.44/11.09 % (90846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90846)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90846)Termination reason: Instruction limit
% 51.44/11.09 % (90846)Termination phase: Property scanning
% 51.44/11.09 % (90846)Time elapsed: 0.132 s
% 51.44/11.09 % (90846)Peak memory usage: 149 MB
% 51.44/11.09 % (90846)Instructions burned: 157 (million)
% 51.44/11.09 % (90853)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1284371781:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2957 on theBenchmark for (2957ds/294Mi)
% 51.44/11.09 % (90848)Instruction limit reached!
% 51.44/11.09 % (90848)------------------------------
% 51.44/11.09 % (90848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90848)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90848)Termination reason: Instruction limit
% 51.44/11.09 % (90848)Termination phase: Property scanning
% 51.44/11.09 % (90848)Time elapsed: 0.205 s
% 51.44/11.09 % (90848)Peak memory usage: 149 MB
% 51.44/11.09 % (90848)Instructions burned: 249 (million)
% 51.44/11.09 % (90854)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1055512244:i=2350_2956 on theBenchmark for (2956ds/2350Mi)
% 51.44/11.09 % (90853)Instruction limit reached!
% 51.44/11.09 % (90853)------------------------------
% 51.44/11.09 % (90853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90853)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90853)Termination reason: Instruction limit
% 51.44/11.09 % (90853)Termination phase: SInE selection
% 51.44/11.09 % (90853)Time elapsed: 0.171 s
% 51.44/11.09 % (90853)Peak memory usage: 149 MB
% 51.44/11.09 % (90853)Instructions burned: 294 (million)
% 51.44/11.09 % (90847)Instruction limit reached!
% 51.44/11.09 % (90847)------------------------------
% 51.44/11.09 % (90847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90847)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90847)Termination reason: Instruction limit
% 51.44/11.09 % (90847)Termination phase: Saturation
% 51.44/11.09 % (90847)Time elapsed: 0.391 s
% 51.44/11.09 % (90847)Peak memory usage: 154 MB
% 51.44/11.09 % (90847)Instructions burned: 325 (million)
% 51.44/11.09 % (90856)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1562290074:cts=off:i=113:fsr=off:ss=included:sgt=4_2955 on theBenchmark for (2955ds/113Mi)
% 51.44/11.09 % (90856)Instruction limit reached!
% 51.44/11.09 % (90856)------------------------------
% 51.44/11.09 % (90856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.44/11.09 % (90856)CaDiCaL version: 2.1.3
% 51.44/11.09 % (90856)Termination reason: Instruction limit
% 51.44/11.09 % (90856)Termination phase: SInE selection
% 51.44/11.09 % (90856)Time elapsed: 0.079 s
% 51.44/11.09 % (90856)Peak memory usage: 148 MB
% 51.44/11.09 % (90856)Instructions burned: 114 (million)
% 51.44/11.09 % (90858)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3727811722:i=127:av=off:fsr=off:sup=off_2954 on theBenchmark for (2954ds/127Mi)
% 51.44/11.09 % (90859)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=308643063:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2954 on theBenchmark for (2954ds/114Mi)
% 51.44/11.09 % (90861)lrs+10_1_sil=8000:sp=occurrence:random_seed=363001856:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2952 on theBenchmark for (2952ds/907Mi)
% 51.44/11.09 % (90858)Instruction limit reached!
% 51.44/11.09 % (90858)------------------------------
% 51.44/11.09 % (90858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.44/11.09 % (90858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90858)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90858)Termination reason: Instruction limit
% 102.41/18.28 % (90858)Termination phase: Preprocessing 1
% 102.41/18.28 % (90858)Time elapsed: 0.155 s
% 102.41/18.28 % (90858)Peak memory usage: 150 MB
% 102.41/18.28 % (90858)Instructions burned: 127 (million)
% 102.41/18.28 % (90859)Instruction limit reached!
% 102.41/18.28 % (90859)------------------------------
% 102.41/18.28 % (90859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90859)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90859)Termination reason: Instruction limit
% 102.41/18.28 % (90859)Termination phase: Property scanning
% 102.41/18.28 % (90859)Time elapsed: 0.099 s
% 102.41/18.28 % (90859)Peak memory usage: 149 MB
% 102.41/18.28 % (90859)Instructions burned: 115 (million)
% 102.41/18.28 % (90865)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1185912389:i=437:sd=1:aac=none:ss=included_2950 on theBenchmark for (2950ds/437Mi)
% 102.41/18.28 % (90866)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3391749688:i=5202:ss=axioms:sgt=16_2950 on theBenchmark for (2950ds/5202Mi)
% 102.41/18.28 % (90861)Instruction limit reached!
% 102.41/18.28 % (90861)------------------------------
% 102.41/18.28 % (90861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90861)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90861)Termination reason: Instruction limit
% 102.41/18.28 % (90861)Termination phase: Property scanning
% 102.41/18.28 % (90861)Time elapsed: 0.577 s
% 102.41/18.28 % (90861)Peak memory usage: 168 MB
% 102.41/18.28 % (90861)Instructions burned: 908 (million)
% 102.41/18.28 % (90865)Refutation not found, incomplete strategy
% 102.41/18.28 % (90865)------------------------------
% 102.41/18.28 % (90865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90865)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90865)Termination reason: Refutation not found, incomplete strategy
% 102.41/18.28 % (90865)Time elapsed: 0.413 s
% 102.41/18.28 % (90865)Peak memory usage: 154 MB
% 102.41/18.28 % (90865)Instructions burned: 353 (million)
% 102.41/18.28 % (90869)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2889245621:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2945 on theBenchmark for (2945ds/134Mi)
% 102.41/18.28 % (90869)Instruction limit reached!
% 102.41/18.28 % (90869)------------------------------
% 102.41/18.28 % (90869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90869)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90869)Termination reason: Instruction limit
% 102.41/18.28 % (90869)Termination phase: SInE selection
% 102.41/18.28 % (90869)Time elapsed: 0.155 s
% 102.41/18.28 % (90869)Peak memory usage: 148 MB
% 102.41/18.28 % (90869)Instructions burned: 134 (million)
% 102.41/18.28 % (90865)------------------------------
% 102.41/18.28 % (90865)------------------------------
% 102.41/18.28 % (90871)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=624925403:st=8:i=592:sd=3:ep=RST:ss=axioms_2941 on theBenchmark for (2941ds/592Mi)
% 102.41/18.28 % (90872)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1969853719:st=3:i=13193:sd=3:ss=axioms_2940 on theBenchmark for (2940ds/13193Mi)
% 102.41/18.28 % (90871)Instruction limit reached!
% 102.41/18.28 % (90871)------------------------------
% 102.41/18.28 % (90871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.41/18.28 % (90871)CaDiCaL version: 2.1.3
% 102.41/18.28 % (90871)Termination reason: Instruction limit
% 102.41/18.28 % (90871)Termination phase: Preprocessing 1
% 102.41/18.28 % (90871)Time elapsed: 0.382 s
% 102.41/18.28 % (90871)Peak memory usage: 151 MB
% 102.41/18.28 % (90871)Instructions burned: 592 (million)
% 102.41/18.28 % (90875)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=2517164363:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2936 on theBenchmark for (2936ds/125Mi)
% 102.41/18.28 % (90875)Instruction limit reached!
% 102.41/18.28 % (90875)------------------------------
% 102.41/18.28 % (90875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.41/18.28 % (90875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90875)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90875)Termination reason: Instruction limit
% 71.57/22.26 % (90875)Termination phase: Property scanning
% 71.57/22.26 % (90875)Time elapsed: 0.060 s
% 71.57/22.26 % (90875)Peak memory usage: 149 MB
% 71.57/22.26 % (90875)Instructions burned: 126 (million)
% 71.57/22.26 % (90877)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1965316433:i=134:gtgl=5:slsql=off:gtg=exists_sym_2934 on theBenchmark for (2934ds/134Mi)
% 71.57/22.26 % (90877)Instruction limit reached!
% 71.57/22.26 % (90877)------------------------------
% 71.57/22.26 % (90877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90877)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90877)Termination reason: Instruction limit
% 71.57/22.26 % (90877)Termination phase: Property scanning
% 71.57/22.26 % (90877)Time elapsed: 0.063 s
% 71.57/22.26 % (90877)Peak memory usage: 148 MB
% 71.57/22.26 % (90877)Instructions burned: 135 (million)
% 71.57/22.26 % (90881)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3171114514:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2931 on theBenchmark for (2931ds/141Mi)
% 71.57/22.26 % (90881)Instruction limit reached!
% 71.57/22.26 % (90881)------------------------------
% 71.57/22.26 % (90881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90881)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90881)Termination reason: Instruction limit
% 71.57/22.26 % (90881)Termination phase: SInE selection
% 71.57/22.26 % (90881)Time elapsed: 0.077 s
% 71.57/22.26 % (90881)Peak memory usage: 148 MB
% 71.57/22.26 % (90881)Instructions burned: 141 (million)
% 71.57/22.26 % (90854)Instruction limit reached!
% 71.57/22.26 % (90854)------------------------------
% 71.57/22.26 % (90854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90854)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90854)Termination reason: Instruction limit
% 71.57/22.26 % (90854)Termination phase: Preprocessing 3
% 71.57/22.26 % (90854)Time elapsed: 2.664 s
% 71.57/22.26 % (90854)Peak memory usage: 249 MB
% 71.57/22.26 % (90854)Instructions burned: 2350 (million)
% 71.57/22.26 % (90884)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=654045104:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2929 on theBenchmark for (2929ds/431Mi)
% 71.57/22.26 % (90887)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=940562923:i=6060:aac=none:ins=25_2928 on theBenchmark for (2928ds/6060Mi)
% 71.57/22.26 % (90884)Instruction limit reached!
% 71.57/22.26 % (90884)------------------------------
% 71.57/22.26 % (90884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90884)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90884)Termination reason: Instruction limit
% 71.57/22.26 % (90884)Termination phase: Saturation
% 71.57/22.26 % (90884)Time elapsed: 0.504 s
% 71.57/22.26 % (90884)Peak memory usage: 156 MB
% 71.57/22.26 % (90884)Instructions burned: 431 (million)
% 71.57/22.26 % (90893)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=2938751319:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2921 on theBenchmark for (2921ds/150Mi)
% 71.57/22.26 % (90893)Instruction limit reached!
% 71.57/22.26 % (90893)------------------------------
% 71.57/22.26 % (90893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90893)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90893)Termination reason: Instruction limit
% 71.57/22.26 % (90893)Termination phase: SInE selection
% 71.57/22.26 % (90893)Time elapsed: 0.174 s
% 71.57/22.26 % (90893)Peak memory usage: 148 MB
% 71.57/22.26 % (90893)Instructions burned: 150 (million)
% 71.57/22.26 % (90895)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1232038533:i=14155:bd=all_2917 on theBenchmark for (2917ds/14155Mi)
% 71.57/22.26 % (90866)Instruction limit reached!
% 71.57/22.26 % (90866)------------------------------
% 71.57/22.26 % (90866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90866)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90866)Termination reason: Instruction limit
% 71.57/22.26 % (90866)Termination phase: Saturation
% 71.57/22.26 % (90866)Time elapsed: 5.166 s
% 71.57/22.26 % (90866)Peak memory usage: 256 MB
% 71.57/22.26 % (90866)Instructions burned: 5202 (million)
% 71.57/22.26 % (90899)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2943396803:i=667:av=off:fsr=off_2896 on theBenchmark for (2896ds/667Mi)
% 71.57/22.26 % (90899)Instruction limit reached!
% 71.57/22.26 % (90899)------------------------------
% 71.57/22.26 % (90899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90899)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90899)Termination reason: Instruction limit
% 71.57/22.26 % (90899)Termination phase: NewCNF
% 71.57/22.26 % (90899)Time elapsed: 0.879 s
% 71.57/22.26 % (90899)Peak memory usage: 205 MB
% 71.57/22.26 % (90899)Instructions burned: 667 (million)
% 71.57/22.26 % (90907)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=1097533260:s2a=on:i=185:s2at=1.8:fdi=4_2885 on theBenchmark for (2885ds/185Mi)
% 71.57/22.26 % (90907)Instruction limit reached!
% 71.57/22.26 % (90907)------------------------------
% 71.57/22.26 % (90907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90907)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90907)Termination reason: Instruction limit
% 71.57/22.26 % (90907)Termination phase: SInE selection
% 71.57/22.26 % (90907)Time elapsed: 0.205 s
% 71.57/22.26 % (90907)Peak memory usage: 148 MB
% 71.57/22.26 % (90907)Instructions burned: 185 (million)
% 71.57/22.26 % (90909)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3060094326:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2881 on theBenchmark for (2881ds/193Mi)
% 71.57/22.26 % (90909)Instruction limit reached!
% 71.57/22.26 % (90909)------------------------------
% 71.57/22.26 % (90909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90909)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90909)Termination reason: Instruction limit
% 71.57/22.26 % (90909)Termination phase: SInE selection
% 71.57/22.26 % (90909)Time elapsed: 0.225 s
% 71.57/22.26 % (90909)Peak memory usage: 149 MB
% 71.57/22.26 % (90909)Instructions burned: 194 (million)
% 71.57/22.26 % (90911)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1366342976:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2877 on theBenchmark for (2877ds/4850Mi)
% 71.57/22.26 % (90887)Instruction limit reached!
% 71.57/22.26 % (90887)------------------------------
% 71.57/22.26 % (90887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90887)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90887)Termination reason: Instruction limit
% 71.57/22.26 % (90887)Termination phase: Property scanning
% 71.57/22.26 % (90887)Time elapsed: 6.611 s
% 71.57/22.26 % (90887)Peak memory usage: 288 MB
% 71.57/22.26 % (90887)Instructions burned: 6060 (million)
% 71.57/22.26 % (90915)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=648216322:i=12111:sd=1:ss=included_2859 on theBenchmark for (2859ds/12111Mi)
% 71.57/22.26 % (90911)Instruction limit reached!
% 71.57/22.26 % (90911)------------------------------
% 71.57/22.26 % (90911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90911)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90911)Termination reason: Instruction limit
% 71.57/22.26 % (90911)Termination phase: Property scanning
% 71.57/22.26 % (90911)Time elapsed: 4.361 s
% 71.57/22.26 % (90911)Peak memory usage: 238 MB
% 71.57/22.26 % (90911)Instructions burned: 4851 (million)
% 71.57/22.26 % (90925)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2920092298:i=319:kws=precedence:fsr=off_2831 on theBenchmark for (2831ds/319Mi)
% 71.57/22.26 % (90925)Instruction limit reached!
% 71.57/22.26 % (90925)------------------------------
% 71.57/22.26 % (90925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90925)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90925)Termination reason: Instruction limit
% 71.57/22.26 % (90925)Termination phase: Preprocessing 1
% 71.57/22.26 % (90925)Time elapsed: 0.373 s
% 71.57/22.26 % (90925)Peak memory usage: 150 MB
% 71.57/22.26 % (90925)Instructions burned: 319 (million)
% 71.57/22.26 % (90931)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1664667528:i=2064:ep=RST_2824 on theBenchmark for (2824ds/2064Mi)
% 71.57/22.26 % (90872)Instruction limit reached!
% 71.57/22.26 % (90872)------------------------------
% 71.57/22.26 % (90872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90872)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90872)Termination reason: Instruction limit
% 71.57/22.26 % (90872)Termination phase: Saturation
% 71.57/22.26 % (90872)Time elapsed: 13.196 s
% 71.57/22.26 % (90872)Peak memory usage: 311 MB
% 71.57/22.26 % (90872)Instructions burned: 13193 (million)
% 71.57/22.26 % (90938)dis-1011_128_sil=32000:random_seed=2561199549:i=3706:ep=RST:av=off_2806 on theBenchmark for (2806ds/3706Mi)
% 71.57/22.26 % (90931)Instruction limit reached!
% 71.57/22.26 % (90931)------------------------------
% 71.57/22.26 % (90931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.57/22.26 % (90931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.57/22.26 % (90931)CaDiCaL version: 2.1.3
% 71.57/22.26 % (90931)Termination reason: Instruction limit
% 71.57/22.26 % (90931)Termination phase: Preprocessing 3
% 71.57/22.26 % (90931)Time elapsed: 2.291 s
% 71.57/22.26 % (90931)Peak memory usage: 249 MB
% 71.57/22.26 % (90931)Instructions burned: 2064 (million)
% 71.57/22.26 % (90941)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3168596076:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2799 on theBenchmark for (2799ds/757Mi)
% 71.57/22.26 % (90941)First to succeed.
% 71.57/22.26 % (90941)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-90812"
% 71.57/22.26 % (90941)Refutation found. Thanks to Tanya!
% 71.57/22.26 % SZS status Theorem for theBenchmark
% 71.57/22.26 % SZS output start Proof for theBenchmark
% See solution above
% 130.76/22.54 % (90941)------------------------------
% 130.76/22.54 % (90941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.76/22.54 % (90941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.76/22.54 % (90941)CaDiCaL version: 2.1.3
% 130.76/22.54 % (90941)Termination reason: Refutation
% 130.76/22.54 % (90941)Time elapsed: 0.542 s
% 130.76/22.54 % (90941)Peak memory usage: 158 MB
% 130.76/22.54 % (90941)Instructions burned: 469 (million)
% 130.76/22.54 % (90941)------------------------------
% 130.76/22.54 % (90941)------------------------------
% 130.76/22.54 % (90812)Success in time 21.482 s
% 130.76/22.54 % Vampire exiting
%------------------------------------------------------------------------------