%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU447+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 : n014.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 12:49:09 PM UTC 2026
% Result : Theorem 49.86s 17.84s
% Output : Refutation 86.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 58
% Syntax : Number of formulae : 293 ( 72 unt; 42 def)
% Number of atoms : 726 ( 126 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 799 ( 366 ~; 362 |; 11 &)
% ( 36 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 34 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 15 con; 0-5 aty)
% Number of variables : 222 ( 0 sgn 216 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f493,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k3_subset_1(X0,X1) = k4_xboole_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f565,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f566,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k3_subset_1(X0,k3_subset_1(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f868,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t159_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1507,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_relset_1) ).
fof(f1508,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f30548,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( X1 = X2
<=> k3_subset_1(X0,X1) = k3_subset_1(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_fin_topo) ).
fof(f71075,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f71077,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) )
=> m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_relset_2) ).
fof(f71078,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) )
=> k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k9_relset_2) ).
fof(f71131,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_relset_2) ).
fof(f71132,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_relset_2) ).
fof(f71141,conjecture,
! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ! [X5] :
( m2_relset_1(X5,X1,X2)
=> k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) = k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5)))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_relset_2) ).
fof(f71142,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ! [X5] :
( m2_relset_1(X5,X1,X2)
=> k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) = k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5)))) ) ) ),
inference(negated_conjecture,[status(cth)],[f71141]) ).
fof(f71224,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f71075]) ).
fof(f71225,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f71224]) ).
fof(f71228,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(ennf_transformation,[],[f71077]) ).
fof(f71229,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(flattening,[],[f71228]) ).
fof(f71230,plain,
! [X0,X1,X2,X3,X4] :
( k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(ennf_transformation,[],[f71078]) ).
fof(f71231,plain,
! [X0,X1,X2,X3,X4] :
( k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(flattening,[],[f71230]) ).
fof(f71290,plain,
! [X0,X1,X2] :
( ! [X3] :
( k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71131]) ).
fof(f71291,plain,
! [X0,X1,X2] :
( ! [X3] :
( k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3))
| ~ m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71132]) ).
fof(f71300,plain,
? [X0,X1,X2,X3] :
( ? [X4] :
( ? [X5] :
( k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) != k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5))))
& m2_relset_1(X5,X1,X2) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71142]) ).
fof(f71401,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f71402,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f71488,plain,
! [X0,X1] :
( ! [X2] :
( k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0))
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f868]) ).
fof(f71856,plain,
! [X0,X1,X2,X3] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1508]) ).
fof(f71857,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1507]) ).
fof(f72137,plain,
! [X0,X1] :
( ! [X2] :
( ( X1 = X2
<=> k3_subset_1(X0,X1) = k3_subset_1(X0,X2) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f30548]) ).
fof(f72142,plain,
! [X0,X1] :
( k3_subset_1(X0,k3_subset_1(X0,X1)) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f566]) ).
fof(f72143,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f565]) ).
fof(f72172,plain,
! [X0,X1] :
( k3_subset_1(X0,X1) = k4_xboole_0(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f493]) ).
fof(f72370,plain,
( k8_relset_2(sK28,sK29,k10_relset_1(sK27,sK28,sK31,sK30),sK32) != k8_relset_2(sK27,sK29,sK30,k3_subset_1(k2_zfmisc_1(sK27,sK29),k9_relset_2(sK27,sK28,sK29,sK31,k3_subset_1(k2_zfmisc_1(sK28,sK29),sK32))))
& m2_relset_1(sK32,sK28,sK29)
& m2_relset_1(sK31,sK27,sK28)
& m1_subset_1(sK30,k1_zfmisc_1(sK27)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30,sK31,sK32]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29),skolemize(X3,sK30),skolemize(X4,sK31),skolemize(X5,sK32)],[f71300]) ).
fof(f72396,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f72715,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X1 = X2
| k3_subset_1(X0,X1) != k3_subset_1(X0,X2) )
& ( k3_subset_1(X0,X1) = k3_subset_1(X0,X2)
| X1 != X2 ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f72137]) ).
fof(f72789,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71225]) ).
fof(f72791,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f71229]) ).
fof(f72792,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| k5_relat_1(X3,X4) = k9_relset_2(X0,X1,X2,X3,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f71231]) ).
fof(f72870,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2) ),
inference(cnf_transformation,[],[f71290]) ).
fof(f72871,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m2_relset_1(X3,X0,X1)
| k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3)) ),
inference(cnf_transformation,[],[f71291]) ).
fof(f72886,plain,
m1_subset_1(sK30,k1_zfmisc_1(sK27)),
inference(cnf_transformation,[],[f72370]) ).
fof(f72887,plain,
m2_relset_1(sK31,sK27,sK28),
inference(cnf_transformation,[],[f72370]) ).
fof(f72888,plain,
m2_relset_1(sK32,sK28,sK29),
inference(cnf_transformation,[],[f72370]) ).
fof(f72889,plain,
k8_relset_2(sK28,sK29,k10_relset_1(sK27,sK28,sK31,sK30),sK32) != k8_relset_2(sK27,sK29,sK30,k3_subset_1(k2_zfmisc_1(sK27,sK29),k9_relset_2(sK27,sK28,sK29,sK31,k3_subset_1(k2_zfmisc_1(sK28,sK29),sK32)))),
inference(cnf_transformation,[],[f72370]) ).
fof(f73037,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72396]) ).
fof(f73052,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71401]) ).
fof(f73053,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71402]) ).
fof(f73139,plain,
! [X2,X0,X1] :
( k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0))
| ~ v1_relat_1(X2)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f71488]) ).
fof(f73732,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f71856]) ).
fof(f73733,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f71857]) ).
fof(f74213,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| k3_subset_1(X0,X1) != k3_subset_1(X0,X2)
| X1 = X2
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f72715]) ).
fof(f74218,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k3_subset_1(X0,k3_subset_1(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f72142]) ).
fof(f74219,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f72143]) ).
fof(f74247,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k4_xboole_0(X0,X1) = k3_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f72172]) ).
fof(f75262,definition,
sF306 = k10_relset_1(sK27,sK28,sK31,sK30),
introduced(definition,[new_symbols(definition,[sF306])],[function_definition]) ).
fof(f75263,plain,
k10_relset_1(sK27,sK28,sK31,sK30) = sF306,
inference(reorient_equations,[],[f75262]) ).
fof(f75264,definition,
sF307 = k8_relset_2(sK28,sK29,sF306,sK32),
introduced(definition,[new_symbols(definition,[sF307])],[function_definition]) ).
fof(f75265,plain,
k8_relset_2(sK28,sK29,sF306,sK32) = sF307,
inference(reorient_equations,[],[f75264]) ).
fof(f75266,definition,
sF308 = k2_zfmisc_1(sK27,sK29),
introduced(definition,[new_symbols(definition,[sF308])],[function_definition]) ).
fof(f75267,plain,
k2_zfmisc_1(sK27,sK29) = sF308,
inference(reorient_equations,[],[f75266]) ).
fof(f75268,definition,
sF309 = k2_zfmisc_1(sK28,sK29),
introduced(definition,[new_symbols(definition,[sF309])],[function_definition]) ).
fof(f75269,plain,
k2_zfmisc_1(sK28,sK29) = sF309,
inference(reorient_equations,[],[f75268]) ).
fof(f75270,definition,
sF310 = k3_subset_1(sF309,sK32),
introduced(definition,[new_symbols(definition,[sF310])],[function_definition]) ).
fof(f75271,plain,
k3_subset_1(sF309,sK32) = sF310,
inference(reorient_equations,[],[f75270]) ).
fof(f75272,definition,
sF311 = k9_relset_2(sK27,sK28,sK29,sK31,sF310),
introduced(definition,[new_symbols(definition,[sF311])],[function_definition]) ).
fof(f75273,plain,
k9_relset_2(sK27,sK28,sK29,sK31,sF310) = sF311,
inference(reorient_equations,[],[f75272]) ).
fof(f75274,definition,
sF312 = k3_subset_1(sF308,sF311),
introduced(definition,[new_symbols(definition,[sF312])],[function_definition]) ).
fof(f75275,plain,
k3_subset_1(sF308,sF311) = sF312,
inference(reorient_equations,[],[f75274]) ).
fof(f75276,definition,
sF313 = k8_relset_2(sK27,sK29,sK30,sF312),
introduced(definition,[new_symbols(definition,[sF313])],[function_definition]) ).
fof(f75277,plain,
k8_relset_2(sK27,sK29,sK30,sF312) = sF313,
inference(reorient_equations,[],[f75276]) ).
fof(f75278,plain,
sF307 != sF313,
inference(definition_folding,[],[f72889,f75277,f75275,f75273,f75271,f75269,f75267,f75265,f75263]) ).
fof(f75279,definition,
sF314 = k1_zfmisc_1(sK27),
introduced(definition,[new_symbols(definition,[sF314])],[function_definition]) ).
fof(f75280,plain,
k1_zfmisc_1(sK27) = sF314,
inference(reorient_equations,[],[f75279]) ).
fof(f75281,plain,
m1_subset_1(sK30,sF314),
inference(definition_folding,[],[f72886,f75280]) ).
fof(f75616,definition,
( spl315_46
<=> m1_subset_1(sK30,sF314) ),
introduced(definition,[new_symbols(definition,[spl315_46])],[avatar_definition]) ).
fof(f75618,plain,
( m1_subset_1(sK30,sF314)
| ~ spl315_46 ),
inference(avatar_component_clause,[],[f75616]) ).
fof(f75619,plain,
spl315_46,
inference(avatar_split_clause,[],[f75281,f75616]) ).
fof(f75621,definition,
( spl315_47
<=> m2_relset_1(sK31,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl315_47])],[avatar_definition]) ).
fof(f75623,plain,
( m2_relset_1(sK31,sK27,sK28)
| ~ spl315_47 ),
inference(avatar_component_clause,[],[f75621]) ).
fof(f75624,plain,
spl315_47,
inference(avatar_split_clause,[],[f72887,f75621]) ).
fof(f75626,definition,
( spl315_48
<=> m2_relset_1(sK32,sK28,sK29) ),
introduced(definition,[new_symbols(definition,[spl315_48])],[avatar_definition]) ).
fof(f75628,plain,
( m2_relset_1(sK32,sK28,sK29)
| ~ spl315_48 ),
inference(avatar_component_clause,[],[f75626]) ).
fof(f75629,plain,
spl315_48,
inference(avatar_split_clause,[],[f72888,f75626]) ).
fof(f75631,definition,
( spl315_49
<=> sF307 = sF313 ),
introduced(definition,[new_symbols(definition,[spl315_49])],[avatar_definition]) ).
fof(f75633,plain,
( sF307 != sF313
| spl315_49 ),
inference(avatar_component_clause,[],[f75631]) ).
fof(f75634,plain,
~ spl315_49,
inference(avatar_split_clause,[],[f75278,f75631]) ).
fof(f75649,definition,
( spl315_51
<=> k10_relset_1(sK27,sK28,sK31,sK30) = sF306 ),
introduced(definition,[new_symbols(definition,[spl315_51])],[avatar_definition]) ).
fof(f75651,plain,
( k10_relset_1(sK27,sK28,sK31,sK30) = sF306
| ~ spl315_51 ),
inference(avatar_component_clause,[],[f75649]) ).
fof(f75652,plain,
spl315_51,
inference(avatar_split_clause,[],[f75263,f75649]) ).
fof(f75654,definition,
( spl315_52
<=> k8_relset_2(sK28,sK29,sF306,sK32) = sF307 ),
introduced(definition,[new_symbols(definition,[spl315_52])],[avatar_definition]) ).
fof(f75656,plain,
( k8_relset_2(sK28,sK29,sF306,sK32) = sF307
| ~ spl315_52 ),
inference(avatar_component_clause,[],[f75654]) ).
fof(f75657,plain,
spl315_52,
inference(avatar_split_clause,[],[f75265,f75654]) ).
fof(f75659,definition,
( spl315_53
<=> k2_zfmisc_1(sK27,sK29) = sF308 ),
introduced(definition,[new_symbols(definition,[spl315_53])],[avatar_definition]) ).
fof(f75661,plain,
( k2_zfmisc_1(sK27,sK29) = sF308
| ~ spl315_53 ),
inference(avatar_component_clause,[],[f75659]) ).
fof(f75662,plain,
spl315_53,
inference(avatar_split_clause,[],[f75267,f75659]) ).
fof(f75664,definition,
( spl315_54
<=> k2_zfmisc_1(sK28,sK29) = sF309 ),
introduced(definition,[new_symbols(definition,[spl315_54])],[avatar_definition]) ).
fof(f75666,plain,
( k2_zfmisc_1(sK28,sK29) = sF309
| ~ spl315_54 ),
inference(avatar_component_clause,[],[f75664]) ).
fof(f75667,plain,
spl315_54,
inference(avatar_split_clause,[],[f75269,f75664]) ).
fof(f75669,definition,
( spl315_55
<=> k3_subset_1(sF309,sK32) = sF310 ),
introduced(definition,[new_symbols(definition,[spl315_55])],[avatar_definition]) ).
fof(f75671,plain,
( k3_subset_1(sF309,sK32) = sF310
| ~ spl315_55 ),
inference(avatar_component_clause,[],[f75669]) ).
fof(f75672,plain,
spl315_55,
inference(avatar_split_clause,[],[f75271,f75669]) ).
fof(f75674,definition,
( spl315_56
<=> k9_relset_2(sK27,sK28,sK29,sK31,sF310) = sF311 ),
introduced(definition,[new_symbols(definition,[spl315_56])],[avatar_definition]) ).
fof(f75676,plain,
( k9_relset_2(sK27,sK28,sK29,sK31,sF310) = sF311
| ~ spl315_56 ),
inference(avatar_component_clause,[],[f75674]) ).
fof(f75677,plain,
spl315_56,
inference(avatar_split_clause,[],[f75273,f75674]) ).
fof(f75679,definition,
( spl315_57
<=> k3_subset_1(sF308,sF311) = sF312 ),
introduced(definition,[new_symbols(definition,[spl315_57])],[avatar_definition]) ).
fof(f75681,plain,
( k3_subset_1(sF308,sF311) = sF312
| ~ spl315_57 ),
inference(avatar_component_clause,[],[f75679]) ).
fof(f75682,plain,
spl315_57,
inference(avatar_split_clause,[],[f75275,f75679]) ).
fof(f75684,definition,
( spl315_58
<=> k8_relset_2(sK27,sK29,sK30,sF312) = sF313 ),
introduced(definition,[new_symbols(definition,[spl315_58])],[avatar_definition]) ).
fof(f75686,plain,
( k8_relset_2(sK27,sK29,sK30,sF312) = sF313
| ~ spl315_58 ),
inference(avatar_component_clause,[],[f75684]) ).
fof(f75687,plain,
spl315_58,
inference(avatar_split_clause,[],[f75277,f75684]) ).
fof(f75689,definition,
( spl315_59
<=> k1_zfmisc_1(sK27) = sF314 ),
introduced(definition,[new_symbols(definition,[spl315_59])],[avatar_definition]) ).
fof(f75691,plain,
( k1_zfmisc_1(sK27) = sF314
| ~ spl315_59 ),
inference(avatar_component_clause,[],[f75689]) ).
fof(f75692,plain,
spl315_59,
inference(avatar_split_clause,[],[f75280,f75689]) ).
fof(f75793,plain,
( m1_subset_1(sK32,k1_zfmisc_1(k2_zfmisc_1(sK28,sK29)))
| ~ spl315_48 ),
inference(resolution,[],[f73052,f75628]) ).
fof(f75794,plain,
( m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl315_47 ),
inference(resolution,[],[f73052,f75623]) ).
fof(f75796,definition,
( spl315_64
<=> m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28))) ),
introduced(definition,[new_symbols(definition,[spl315_64])],[avatar_definition]) ).
fof(f75798,plain,
( m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl315_64 ),
inference(avatar_component_clause,[],[f75796]) ).
fof(f75799,plain,
( spl315_64
| ~ spl315_47 ),
inference(avatar_split_clause,[],[f75794,f75621,f75796]) ).
fof(f75800,plain,
( m1_subset_1(sK32,k1_zfmisc_1(sF309))
| ~ spl315_48
| ~ spl315_54 ),
inference(forward_demodulation,[],[f75793,f75666]) ).
fof(f75803,definition,
( spl315_65
<=> m1_subset_1(sK32,k1_zfmisc_1(sF309)) ),
introduced(definition,[new_symbols(definition,[spl315_65])],[avatar_definition]) ).
fof(f75805,plain,
( m1_subset_1(sK32,k1_zfmisc_1(sF309))
| ~ spl315_65 ),
inference(avatar_component_clause,[],[f75803]) ).
fof(f75806,plain,
( spl315_65
| ~ spl315_48
| ~ spl315_54 ),
inference(avatar_split_clause,[],[f75800,f75664,f75626,f75803]) ).
fof(f75832,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF314)
| ~ m2_relset_1(X1,sK27,X2)
| k3_subset_1(X2,k10_relset_1(sK27,X2,X1,X0)) = k8_relset_2(sK27,X2,X0,k3_subset_1(k2_zfmisc_1(sK27,X2),X1)) )
| ~ spl315_59 ),
inference(superposition,[],[f72871,f75691]) ).
fof(f75834,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X0,sK27,X1)
| k3_subset_1(X1,k10_relset_1(sK27,X1,X0,sK30)) = k8_relset_2(sK27,X1,sK30,k3_subset_1(k2_zfmisc_1(sK27,X1),X0)) )
| ~ spl315_46
| ~ spl315_59 ),
inference(resolution,[],[f75832,f75618]) ).
fof(f75876,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK28,X1)))
| k5_relat_1(sK31,X0) = k9_relset_2(sK27,sK28,X1,sK31,X0) )
| ~ spl315_64 ),
inference(resolution,[],[f75798,f72792]) ).
fof(f75877,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(sK28,X0)))
| m2_relset_1(k9_relset_2(sK27,sK28,X0,sK31,X1),sK27,X0) )
| ~ spl315_64 ),
inference(resolution,[],[f75798,f72791]) ).
fof(f75929,plain,
( v1_relat_1(sK31)
| ~ spl315_64 ),
inference(unit_resulting_resolution,[],[f73053,f75798]) ).
fof(f75931,definition,
( spl315_82
<=> v1_relat_1(sK31) ),
introduced(definition,[new_symbols(definition,[spl315_82])],[avatar_definition]) ).
fof(f75933,plain,
( v1_relat_1(sK31)
| ~ spl315_82 ),
inference(avatar_component_clause,[],[f75931]) ).
fof(f75934,plain,
( spl315_82
| ~ spl315_64 ),
inference(avatar_split_clause,[],[f75929,f75796,f75931]) ).
fof(f75952,plain,
( m1_subset_1(k3_subset_1(sF309,sK32),k1_zfmisc_1(sF309))
| ~ spl315_65 ),
inference(resolution,[],[f74219,f75805]) ).
fof(f75956,plain,
( m1_subset_1(sF310,k1_zfmisc_1(sF309))
| ~ spl315_55
| ~ spl315_65 ),
inference(forward_demodulation,[],[f75952,f75671]) ).
fof(f75965,definition,
( spl315_85
<=> m1_subset_1(sF310,k1_zfmisc_1(sF309)) ),
introduced(definition,[new_symbols(definition,[spl315_85])],[avatar_definition]) ).
fof(f75967,plain,
( m1_subset_1(sF310,k1_zfmisc_1(sF309))
| ~ spl315_85 ),
inference(avatar_component_clause,[],[f75965]) ).
fof(f75968,plain,
( spl315_85
| ~ spl315_55
| ~ spl315_65 ),
inference(avatar_split_clause,[],[f75956,f75803,f75669,f75965]) ).
fof(f76090,plain,
( m1_relset_1(sK31,sK27,sK28)
| ~ spl315_47 ),
inference(resolution,[],[f73037,f75623]) ).
fof(f76092,definition,
( spl315_97
<=> m1_relset_1(sK31,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl315_97])],[avatar_definition]) ).
fof(f76094,plain,
( m1_relset_1(sK31,sK27,sK28)
| ~ spl315_97 ),
inference(avatar_component_clause,[],[f76092]) ).
fof(f76095,plain,
( spl315_97
| ~ spl315_47 ),
inference(avatar_split_clause,[],[f76090,f75621,f76092]) ).
fof(f76103,plain,
( ! [X0] : k10_relset_1(sK27,sK28,sK31,X0) = k9_relat_1(sK31,X0)
| ~ spl315_97 ),
inference(resolution,[],[f76094,f73732]) ).
fof(f76104,plain,
( ! [X0] : m1_subset_1(k10_relset_1(sK27,sK28,sK31,X0),k1_zfmisc_1(sK28))
| ~ spl315_97 ),
inference(resolution,[],[f76094,f73733]) ).
fof(f76108,plain,
( sF306 = k9_relat_1(sK31,sK30)
| ~ spl315_51
| ~ spl315_97 ),
inference(superposition,[],[f75651,f76103]) ).
fof(f76118,definition,
( spl315_100
<=> sF306 = k9_relat_1(sK31,sK30) ),
introduced(definition,[new_symbols(definition,[spl315_100])],[avatar_definition]) ).
fof(f76120,plain,
( sF306 = k9_relat_1(sK31,sK30)
| ~ spl315_100 ),
inference(avatar_component_clause,[],[f76118]) ).
fof(f76121,plain,
( spl315_100
| ~ spl315_51
| ~ spl315_97 ),
inference(avatar_split_clause,[],[f76108,f76092,f75649,f76118]) ).
fof(f76130,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK28,X1)))
| k3_subset_1(X1,k8_relset_2(sK28,X1,k10_relset_1(sK27,sK28,sK31,X2),X0)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(sK28,X1),X0),k10_relset_1(sK27,sK28,sK31,X2)) )
| ~ spl315_97 ),
inference(resolution,[],[f76104,f72870]) ).
fof(f76137,plain,
( m1_subset_1(sF306,k1_zfmisc_1(sK28))
| ~ spl315_51
| ~ spl315_97 ),
inference(superposition,[],[f76104,f75651]) ).
fof(f76148,definition,
( spl315_102
<=> m1_subset_1(sF306,k1_zfmisc_1(sK28)) ),
introduced(definition,[new_symbols(definition,[spl315_102])],[avatar_definition]) ).
fof(f76150,plain,
( m1_subset_1(sF306,k1_zfmisc_1(sK28))
| ~ spl315_102 ),
inference(avatar_component_clause,[],[f76148]) ).
fof(f76151,plain,
( spl315_102
| ~ spl315_51
| ~ spl315_97 ),
inference(avatar_split_clause,[],[f76137,f76092,f75649,f76148]) ).
fof(f76158,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK28,X1)))
| k3_subset_1(X1,k8_relset_2(sK28,X1,k9_relat_1(sK31,X2),X0)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(sK28,X1),X0),k9_relat_1(sK31,X2)) )
| ~ spl315_97 ),
inference(forward_demodulation,[],[f76130,f76103]) ).
fof(f76181,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(sK28,X0)))
| m1_subset_1(k8_relset_2(sK28,X0,sF306,X1),k1_zfmisc_1(X0)) )
| ~ spl315_102 ),
inference(resolution,[],[f76150,f72789]) ).
fof(f76375,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF309))
| m1_subset_1(k8_relset_2(sK28,sK29,sF306,X0),k1_zfmisc_1(sK29)) )
| ~ spl315_54
| ~ spl315_102 ),
inference(superposition,[],[f76181,f75666]) ).
fof(f76540,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF309))
| k5_relat_1(sK31,X0) = k9_relset_2(sK27,sK28,sK29,sK31,X0) )
| ~ spl315_54
| ~ spl315_64 ),
inference(superposition,[],[f75876,f75666]) ).
fof(f76544,plain,
( k9_relset_2(sK27,sK28,sK29,sK31,sF310) = k5_relat_1(sK31,sF310)
| ~ spl315_54
| ~ spl315_64
| ~ spl315_85 ),
inference(resolution,[],[f76540,f75967]) ).
fof(f76545,plain,
( sF311 = k5_relat_1(sK31,sF310)
| ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85 ),
inference(forward_demodulation,[],[f76544,f75676]) ).
fof(f76553,definition,
( spl315_132
<=> sF311 = k5_relat_1(sK31,sF310) ),
introduced(definition,[new_symbols(definition,[spl315_132])],[avatar_definition]) ).
fof(f76555,plain,
( sF311 = k5_relat_1(sK31,sF310)
| ~ spl315_132 ),
inference(avatar_component_clause,[],[f76553]) ).
fof(f76556,plain,
( spl315_132
| ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85 ),
inference(avatar_split_clause,[],[f76545,f75965,f75796,f75674,f75664,f76553]) ).
fof(f76622,plain,
( m1_subset_1(k8_relset_2(sK28,sK29,sF306,sK32),k1_zfmisc_1(sK29))
| ~ spl315_54
| ~ spl315_65
| ~ spl315_102 ),
inference(resolution,[],[f76375,f75805]) ).
fof(f76625,plain,
( m1_subset_1(sF307,k1_zfmisc_1(sK29))
| ~ spl315_52
| ~ spl315_54
| ~ spl315_65
| ~ spl315_102 ),
inference(forward_demodulation,[],[f76622,f75656]) ).
fof(f76629,definition,
( spl315_141
<=> m1_subset_1(sF307,k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl315_141])],[avatar_definition]) ).
fof(f76631,plain,
( m1_subset_1(sF307,k1_zfmisc_1(sK29))
| ~ spl315_141 ),
inference(avatar_component_clause,[],[f76629]) ).
fof(f76632,plain,
( spl315_141
| ~ spl315_52
| ~ spl315_54
| ~ spl315_65
| ~ spl315_102 ),
inference(avatar_split_clause,[],[f76625,f76148,f75803,f75664,f75654,f76629]) ).
fof(f76647,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK29))
| sF307 = X0
| k3_subset_1(sK29,X0) != k3_subset_1(sK29,sF307) )
| ~ spl315_141 ),
inference(resolution,[],[f76631,f74213]) ).
fof(f76651,plain,
( k3_subset_1(sK29,sF307) = k4_xboole_0(sK29,sF307)
| ~ spl315_141 ),
inference(resolution,[],[f76631,f74247]) ).
fof(f76653,definition,
( spl315_142
<=> k3_subset_1(sK29,sF307) = k4_xboole_0(sK29,sF307) ),
introduced(definition,[new_symbols(definition,[spl315_142])],[avatar_definition]) ).
fof(f76655,plain,
( k3_subset_1(sK29,sF307) = k4_xboole_0(sK29,sF307)
| ~ spl315_142 ),
inference(avatar_component_clause,[],[f76653]) ).
fof(f76656,plain,
( spl315_142
| ~ spl315_141 ),
inference(avatar_split_clause,[],[f76651,f76629,f76653]) ).
fof(f77075,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF309))
| k3_subset_1(sK29,k8_relset_2(sK28,sK29,k9_relat_1(sK31,X1),X0)) = k9_relat_1(k3_subset_1(sF309,X0),k9_relat_1(sK31,X1)) )
| ~ spl315_54
| ~ spl315_97 ),
inference(superposition,[],[f76158,f75666]) ).
fof(f77078,plain,
( ! [X0] : k3_subset_1(sK29,k8_relset_2(sK28,sK29,k9_relat_1(sK31,X0),sK32)) = k9_relat_1(k3_subset_1(sF309,sK32),k9_relat_1(sK31,X0))
| ~ spl315_54
| ~ spl315_65
| ~ spl315_97 ),
inference(resolution,[],[f77075,f75805]) ).
fof(f77081,plain,
( ! [X0] : k3_subset_1(sK29,k8_relset_2(sK28,sK29,k9_relat_1(sK31,X0),sK32)) = k9_relat_1(sF310,k9_relat_1(sK31,X0))
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97 ),
inference(forward_demodulation,[],[f77078,f75671]) ).
fof(f77086,plain,
( k3_subset_1(sK29,k8_relset_2(sK28,sK29,sF306,sK32)) = k9_relat_1(sF310,sF306)
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97
| ~ spl315_100 ),
inference(superposition,[],[f77081,f76120]) ).
fof(f77095,plain,
( k3_subset_1(sK29,sF307) = k9_relat_1(sF310,sF306)
| ~ spl315_52
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97
| ~ spl315_100 ),
inference(forward_demodulation,[],[f77086,f75656]) ).
fof(f77096,plain,
( k4_xboole_0(sK29,sF307) = k9_relat_1(sF310,sF306)
| ~ spl315_52
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97
| ~ spl315_100
| ~ spl315_142 ),
inference(forward_demodulation,[],[f77095,f76655]) ).
fof(f77098,definition,
( spl315_188
<=> k4_xboole_0(sK29,sF307) = k9_relat_1(sF310,sF306) ),
introduced(definition,[new_symbols(definition,[spl315_188])],[avatar_definition]) ).
fof(f77100,plain,
( k4_xboole_0(sK29,sF307) = k9_relat_1(sF310,sF306)
| ~ spl315_188 ),
inference(avatar_component_clause,[],[f77098]) ).
fof(f77101,plain,
( spl315_188
| ~ spl315_52
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97
| ~ spl315_100
| ~ spl315_142 ),
inference(avatar_split_clause,[],[f77096,f76653,f76118,f76092,f75803,f75669,f75664,f75654,f77098]) ).
fof(f77568,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF309))
| m2_relset_1(k9_relset_2(sK27,sK28,sK29,sK31,X0),sK27,sK29) )
| ~ spl315_54
| ~ spl315_64 ),
inference(superposition,[],[f75877,f75666]) ).
fof(f78125,plain,
( m2_relset_1(k9_relset_2(sK27,sK28,sK29,sK31,sF310),sK27,sK29)
| ~ spl315_54
| ~ spl315_64
| ~ spl315_85 ),
inference(resolution,[],[f77568,f75967]) ).
fof(f78126,plain,
( m2_relset_1(sF311,sK27,sK29)
| ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85 ),
inference(forward_demodulation,[],[f78125,f75676]) ).
fof(f78131,definition,
( spl315_301
<=> m2_relset_1(sF311,sK27,sK29) ),
introduced(definition,[new_symbols(definition,[spl315_301])],[avatar_definition]) ).
fof(f78133,plain,
( m2_relset_1(sF311,sK27,sK29)
| ~ spl315_301 ),
inference(avatar_component_clause,[],[f78131]) ).
fof(f78134,plain,
( spl315_301
| ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85 ),
inference(avatar_split_clause,[],[f78126,f75965,f75796,f75674,f75664,f78131]) ).
fof(f78147,plain,
( k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30)) = k8_relset_2(sK27,sK29,sK30,k3_subset_1(k2_zfmisc_1(sK27,sK29),sF311))
| ~ spl315_46
| ~ spl315_59
| ~ spl315_301 ),
inference(resolution,[],[f78133,f75834]) ).
fof(f78152,plain,
( m1_relset_1(sF311,sK27,sK29)
| ~ spl315_301 ),
inference(resolution,[],[f78133,f73037]) ).
fof(f78162,definition,
( spl315_304
<=> m1_relset_1(sF311,sK27,sK29) ),
introduced(definition,[new_symbols(definition,[spl315_304])],[avatar_definition]) ).
fof(f78164,plain,
( m1_relset_1(sF311,sK27,sK29)
| ~ spl315_304 ),
inference(avatar_component_clause,[],[f78162]) ).
fof(f78165,plain,
( spl315_304
| ~ spl315_301 ),
inference(avatar_split_clause,[],[f78152,f78131,f78162]) ).
fof(f78171,plain,
( k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30)) = k8_relset_2(sK27,sK29,sK30,k3_subset_1(sF308,sF311))
| ~ spl315_46
| ~ spl315_53
| ~ spl315_59
| ~ spl315_301 ),
inference(forward_demodulation,[],[f78147,f75661]) ).
fof(f78182,plain,
( k8_relset_2(sK27,sK29,sK30,sF312) = k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30))
| ~ spl315_46
| ~ spl315_53
| ~ spl315_57
| ~ spl315_59
| ~ spl315_301 ),
inference(forward_demodulation,[],[f78171,f75681]) ).
fof(f78187,plain,
( sF313 = k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30))
| ~ spl315_46
| ~ spl315_53
| ~ spl315_57
| ~ spl315_58
| ~ spl315_59
| ~ spl315_301 ),
inference(forward_demodulation,[],[f78182,f75686]) ).
fof(f78191,definition,
( spl315_307
<=> sF313 = k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30)) ),
introduced(definition,[new_symbols(definition,[spl315_307])],[avatar_definition]) ).
fof(f78193,plain,
( sF313 = k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30))
| ~ spl315_307 ),
inference(avatar_component_clause,[],[f78191]) ).
fof(f78194,plain,
( spl315_307
| ~ spl315_46
| ~ spl315_53
| ~ spl315_57
| ~ spl315_58
| ~ spl315_59
| ~ spl315_301 ),
inference(avatar_split_clause,[],[f78187,f78131,f75689,f75684,f75679,f75659,f75616,f78191]) ).
fof(f78205,definition,
( spl315_309
<=> m1_subset_1(k10_relset_1(sK27,sK29,sF311,sK30),k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl315_309])],[avatar_definition]) ).
fof(f78206,plain,
( m1_subset_1(k10_relset_1(sK27,sK29,sF311,sK30),k1_zfmisc_1(sK29))
| ~ spl315_309 ),
inference(avatar_component_clause,[],[f78205]) ).
fof(f78207,plain,
( ~ m1_subset_1(k10_relset_1(sK27,sK29,sF311,sK30),k1_zfmisc_1(sK29))
| spl315_309 ),
inference(avatar_component_clause,[],[f78205]) ).
fof(f78216,plain,
( ~ m1_relset_1(sF311,sK27,sK29)
| spl315_309 ),
inference(unit_resulting_resolution,[],[f73733,f78207]) ).
fof(f78217,plain,
( $false
| ~ spl315_304
| spl315_309 ),
inference(forward_subsumption_resolution,[],[f78216,f78164]) ).
fof(f78218,plain,
( ~ spl315_304
| spl315_309 ),
inference(avatar_contradiction_clause,[],[f78217]) ).
fof(f78307,plain,
( ! [X0] : k10_relset_1(sK27,sK29,sF311,X0) = k9_relat_1(sF311,X0)
| ~ spl315_304 ),
inference(resolution,[],[f78164,f73732]) ).
fof(f78840,plain,
( k10_relset_1(sK27,sK29,sF311,sK30) = k3_subset_1(sK29,k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30)))
| ~ spl315_309 ),
inference(resolution,[],[f78206,f74218]) ).
fof(f78841,plain,
( m1_subset_1(k3_subset_1(sK29,k10_relset_1(sK27,sK29,sF311,sK30)),k1_zfmisc_1(sK29))
| ~ spl315_309 ),
inference(resolution,[],[f78206,f74219]) ).
fof(f78847,plain,
( m1_subset_1(sF313,k1_zfmisc_1(sK29))
| ~ spl315_307
| ~ spl315_309 ),
inference(forward_demodulation,[],[f78841,f78193]) ).
fof(f78848,plain,
( k10_relset_1(sK27,sK29,sF311,sK30) = k3_subset_1(sK29,sF313)
| ~ spl315_307
| ~ spl315_309 ),
inference(forward_demodulation,[],[f78840,f78193]) ).
fof(f78897,definition,
( spl315_361
<=> m1_subset_1(sF313,k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl315_361])],[avatar_definition]) ).
fof(f78899,plain,
( m1_subset_1(sF313,k1_zfmisc_1(sK29))
| ~ spl315_361 ),
inference(avatar_component_clause,[],[f78897]) ).
fof(f78900,plain,
( spl315_361
| ~ spl315_307
| ~ spl315_309 ),
inference(avatar_split_clause,[],[f78847,f78205,f78191,f78897]) ).
fof(f78901,plain,
( k9_relat_1(sF311,sK30) = k3_subset_1(sK29,sF313)
| ~ spl315_304
| ~ spl315_307
| ~ spl315_309 ),
inference(forward_demodulation,[],[f78848,f78307]) ).
fof(f78949,definition,
( spl315_363
<=> k9_relat_1(sF311,sK30) = k3_subset_1(sK29,sF313) ),
introduced(definition,[new_symbols(definition,[spl315_363])],[avatar_definition]) ).
fof(f78951,plain,
( k9_relat_1(sF311,sK30) = k3_subset_1(sK29,sF313)
| ~ spl315_363 ),
inference(avatar_component_clause,[],[f78949]) ).
fof(f78952,plain,
( spl315_363
| ~ spl315_304
| ~ spl315_307
| ~ spl315_309 ),
inference(avatar_split_clause,[],[f78901,f78205,f78191,f78162,f78949]) ).
fof(f79043,plain,
( k3_subset_1(sK29,sF307) != k3_subset_1(sK29,sF313)
| spl315_49
| ~ spl315_141
| ~ spl315_361 ),
inference(unit_resulting_resolution,[],[f76647,f75633,f78899]) ).
fof(f79111,plain,
( k3_subset_1(sK29,sF307) != k9_relat_1(sF311,sK30)
| spl315_49
| ~ spl315_141
| ~ spl315_361
| ~ spl315_363 ),
inference(forward_demodulation,[],[f79043,f78951]) ).
fof(f79163,plain,
( k4_xboole_0(sK29,sF307) != k9_relat_1(sF311,sK30)
| spl315_49
| ~ spl315_141
| ~ spl315_142
| ~ spl315_361
| ~ spl315_363 ),
inference(forward_demodulation,[],[f79111,f76655]) ).
fof(f79262,definition,
( spl315_394
<=> k4_xboole_0(sK29,sF307) = k9_relat_1(sF311,sK30) ),
introduced(definition,[new_symbols(definition,[spl315_394])],[avatar_definition]) ).
fof(f79264,plain,
( k4_xboole_0(sK29,sF307) != k9_relat_1(sF311,sK30)
| spl315_394 ),
inference(avatar_component_clause,[],[f79262]) ).
fof(f79265,plain,
( ~ spl315_394
| spl315_49
| ~ spl315_141
| ~ spl315_142
| ~ spl315_361
| ~ spl315_363 ),
inference(avatar_split_clause,[],[f79163,f78949,f78897,f76653,f76629,f75631,f79262]) ).
fof(f82519,plain,
( ! [X0] :
( k9_relat_1(sF310,k9_relat_1(sK31,X0)) = k9_relat_1(sF311,X0)
| ~ v1_relat_1(sF310)
| ~ v1_relat_1(sK31) )
| ~ spl315_132 ),
inference(superposition,[],[f73139,f76555]) ).
fof(f82520,plain,
( ! [X0] :
( k9_relat_1(sF310,k9_relat_1(sK31,X0)) = k9_relat_1(sF311,X0)
| ~ v1_relat_1(sF310) )
| ~ spl315_82
| ~ spl315_132 ),
inference(forward_subsumption_resolution,[],[f82519,f75933]) ).
fof(f82522,definition,
( spl315_669
<=> v1_relat_1(sF310) ),
introduced(definition,[new_symbols(definition,[spl315_669])],[avatar_definition]) ).
fof(f82524,plain,
( ~ v1_relat_1(sF310)
| spl315_669 ),
inference(avatar_component_clause,[],[f82522]) ).
fof(f82526,definition,
( spl315_670
<=> ! [X0] : k9_relat_1(sF310,k9_relat_1(sK31,X0)) = k9_relat_1(sF311,X0) ),
introduced(definition,[new_symbols(definition,[spl315_670])],[avatar_definition]) ).
fof(f82527,plain,
( ! [X0] : k9_relat_1(sF310,k9_relat_1(sK31,X0)) = k9_relat_1(sF311,X0)
| ~ spl315_670 ),
inference(avatar_component_clause,[],[f82526]) ).
fof(f82528,plain,
( ~ spl315_669
| spl315_670
| ~ spl315_82
| ~ spl315_132 ),
inference(avatar_split_clause,[],[f82520,f76553,f75931,f82526,f82522]) ).
fof(f82530,plain,
( ! [X0,X1] : ~ m1_subset_1(sF310,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| spl315_669 ),
inference(resolution,[],[f82524,f73053]) ).
fof(f82533,plain,
( ~ m1_subset_1(sF310,k1_zfmisc_1(sF309))
| ~ spl315_54
| spl315_669 ),
inference(superposition,[],[f82530,f75666]) ).
fof(f82536,plain,
( $false
| ~ spl315_54
| ~ spl315_85
| spl315_669 ),
inference(forward_subsumption_resolution,[],[f82533,f75967]) ).
fof(f82537,plain,
( ~ spl315_54
| ~ spl315_85
| spl315_669 ),
inference(avatar_contradiction_clause,[],[f82536]) ).
fof(f82541,plain,
( k9_relat_1(sF310,sF306) = k9_relat_1(sF311,sK30)
| ~ spl315_100
| ~ spl315_670 ),
inference(superposition,[],[f82527,f76120]) ).
fof(f82542,plain,
( k4_xboole_0(sK29,sF307) = k9_relat_1(sF311,sK30)
| ~ spl315_100
| ~ spl315_188
| ~ spl315_670 ),
inference(forward_demodulation,[],[f82541,f77100]) ).
fof(f82550,plain,
( $false
| ~ spl315_100
| ~ spl315_188
| spl315_394
| ~ spl315_670 ),
inference(forward_subsumption_resolution,[],[f82542,f79264]) ).
fof(f82551,plain,
( ~ spl315_100
| ~ spl315_188
| spl315_394
| ~ spl315_670 ),
inference(avatar_contradiction_clause,[],[f82550]) ).
cnf(s49,plain,
spl315_46,
inference(sat_conversion,[],[f75619]) ).
cnf(s50,plain,
spl315_47,
inference(sat_conversion,[],[f75624]) ).
cnf(s51,plain,
spl315_48,
inference(sat_conversion,[],[f75629]) ).
cnf(s52,plain,
~ spl315_49,
inference(sat_conversion,[],[f75634]) ).
cnf(s54,plain,
spl315_51,
inference(sat_conversion,[],[f75652]) ).
cnf(s55,plain,
spl315_52,
inference(sat_conversion,[],[f75657]) ).
cnf(s56,plain,
spl315_53,
inference(sat_conversion,[],[f75662]) ).
cnf(s57,plain,
spl315_54,
inference(sat_conversion,[],[f75667]) ).
cnf(s58,plain,
spl315_55,
inference(sat_conversion,[],[f75672]) ).
cnf(s59,plain,
spl315_56,
inference(sat_conversion,[],[f75677]) ).
cnf(s60,plain,
spl315_57,
inference(sat_conversion,[],[f75682]) ).
cnf(s61,plain,
spl315_58,
inference(sat_conversion,[],[f75687]) ).
cnf(s62,plain,
spl315_59,
inference(sat_conversion,[],[f75692]) ).
cnf(s68,plain,
( ~ spl315_47
| spl315_64 ),
inference(sat_conversion,[],[f75799]) ).
cnf(s70,plain,
( ~ spl315_48
| ~ spl315_54
| spl315_65 ),
inference(sat_conversion,[],[f75806]) ).
cnf(s89,plain,
( ~ spl315_64
| spl315_82 ),
inference(sat_conversion,[],[f75934]) ).
cnf(s92,plain,
( ~ spl315_55
| ~ spl315_65
| spl315_85 ),
inference(sat_conversion,[],[f75968]) ).
cnf(s116,plain,
( ~ spl315_47
| spl315_97 ),
inference(sat_conversion,[],[f76095]) ).
cnf(s121,plain,
( ~ spl315_51
| ~ spl315_97
| spl315_100 ),
inference(sat_conversion,[],[f76121]) ).
cnf(s127,plain,
( ~ spl315_51
| ~ spl315_97
| spl315_102 ),
inference(sat_conversion,[],[f76151]) ).
cnf(s169,plain,
( ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85
| spl315_132 ),
inference(sat_conversion,[],[f76556]) ).
cnf(s178,plain,
( ~ spl315_52
| ~ spl315_54
| ~ spl315_65
| ~ spl315_102
| spl315_141 ),
inference(sat_conversion,[],[f76632]) ).
cnf(s180,plain,
( ~ spl315_141
| spl315_142 ),
inference(sat_conversion,[],[f76656]) ).
cnf(s238,plain,
( ~ spl315_52
| ~ spl315_54
| ~ spl315_55
| ~ spl315_65
| ~ spl315_97
| ~ spl315_100
| ~ spl315_142
| spl315_188 ),
inference(sat_conversion,[],[f77101]) ).
cnf(s379,plain,
( ~ spl315_54
| ~ spl315_56
| ~ spl315_64
| ~ spl315_85
| spl315_301 ),
inference(sat_conversion,[],[f78134]) ).
cnf(s384,plain,
( ~ spl315_301
| spl315_304 ),
inference(sat_conversion,[],[f78165]) ).
cnf(s392,plain,
( ~ spl315_46
| ~ spl315_53
| ~ spl315_57
| ~ spl315_58
| ~ spl315_59
| ~ spl315_301
| spl315_307 ),
inference(sat_conversion,[],[f78194]) ).
cnf(s398,plain,
( ~ spl315_304
| spl315_309 ),
inference(sat_conversion,[],[f78218]) ).
cnf(s465,plain,
( ~ spl315_307
| ~ spl315_309
| spl315_361 ),
inference(sat_conversion,[],[f78900]) ).
cnf(s468,plain,
( ~ spl315_304
| ~ spl315_307
| ~ spl315_309
| spl315_363 ),
inference(sat_conversion,[],[f78952]) ).
cnf(s508,plain,
( spl315_49
| ~ spl315_141
| ~ spl315_142
| ~ spl315_361
| ~ spl315_363
| ~ spl315_394 ),
inference(sat_conversion,[],[f79265]) ).
cnf(s828,plain,
( ~ spl315_82
| ~ spl315_132
| ~ spl315_669
| spl315_670 ),
inference(sat_conversion,[],[f82528]) ).
cnf(s830,plain,
( ~ spl315_54
| ~ spl315_85
| spl315_669 ),
inference(sat_conversion,[],[f82537]) ).
cnf(s832,plain,
( ~ spl315_100
| ~ spl315_188
| spl315_394
| ~ spl315_670 ),
inference(sat_conversion,[],[f82551]) ).
cnf(s849,plain,
spl315_65,
inference(rat,[],[s70,s57,s51]) ).
cnf(s862,plain,
spl315_85,
inference(rat,[],[s92,s58,s849]) ).
cnf(s876,plain,
spl315_669,
inference(rat,[],[s830,s57,s862]) ).
cnf(s907,plain,
spl315_97,
inference(rat,[],[s116,s50]) ).
cnf(s910,plain,
spl315_64,
inference(rat,[],[s68,s50]) ).
cnf(s912,plain,
spl315_102,
inference(rat,[],[s127,s54,s907]) ).
cnf(s914,plain,
spl315_100,
inference(rat,[],[s121,s54,s907]) ).
cnf(s919,plain,
spl315_82,
inference(rat,[],[s89,s910]) ).
cnf(s922,plain,
spl315_301,
inference(rat,[],[s379,s862,s57,s59,s910]) ).
cnf(s923,plain,
spl315_132,
inference(rat,[],[s169,s862,s57,s59,s910]) ).
cnf(s938,plain,
spl315_141,
inference(rat,[],[s178,s849,s55,s57,s912]) ).
cnf(s959,plain,
spl315_304,
inference(rat,[],[s384,s922]) ).
cnf(s962,plain,
spl315_670,
inference(rat,[],[s828,s919,s876,s923]) ).
cnf(s988,plain,
spl315_142,
inference(rat,[],[s180,s938]) ).
cnf(s1012,plain,
spl315_309,
inference(rat,[],[s398,s959]) ).
cnf(s1039,plain,
spl315_188,
inference(rat,[],[s238,s914,s907,s849,s55,s57,s58,s988]) ).
cnf(s1080,plain,
spl315_394,
inference(rat,[],[s832,s962,s914,s1039]) ).
cnf(s1105,plain,
spl315_307,
inference(rat,[],[s392,s922,s56,s62,s61,s60,s49]) ).
cnf(s1132,plain,
spl315_363,
inference(rat,[],[s468,s1012,s959,s1105]) ).
cnf(s1134,plain,
spl315_361,
inference(rat,[],[s465,s1012,s1105]) ).
cnf(s1202,plain,
$false,
inference(rat,[],[s508,s1080,s988,s938,s52,s1132,s1134]) ).
fof(f82558,plain,
$false,
inference(avatar_sat_refutation,[],[s1202]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU447+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.10/0.43 % Computer : n014.cluster.edu
% 0.10/0.43 % Model : x86_64 x86_64
% 0.10/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.43 % Memory : 8046.5625MB
% 0.10/0.43 % OS : Linux 6.8.0-71-generic
% 0.10/0.43 % CPULimit : 300
% 0.10/0.43 % WCLimit : 300
% 0.10/0.43 % DateTime : Mon Sep 28 05:35:14 UTC 2026
% 0.10/0.43 % CPUTime :
% 0.10/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.47 Running first-order theorem proving
% 0.15/0.47 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
% 22.59/8.92 % (1482435)Detected formulas, will run a generic FOF schedule.
% 22.59/8.92 % (1482440)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=3344723142:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 22.59/8.92 % (1482441)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=2707064178:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 22.59/8.92 % (1482442)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=4062012664:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 22.59/8.92 % (1482443)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1746537337:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 22.59/8.92 % (1482446)dis-21_1_sil=8000:lcm=predicate:random_seed=2716225662:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 22.59/8.92 % (1482444)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4096110250:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 22.59/8.92 % (1482445)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1001870489:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 22.59/8.92 % (1482445)Instruction limit reached!
% 22.59/8.92 % (1482445)------------------------------
% 22.59/8.92 % (1482445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.59/8.92 % (1482445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/8.92 % (1482445)CaDiCaL version: 2.1.3
% 22.59/8.92 % (1482445)Termination reason: Instruction limit
% 22.59/8.92 % (1482445)Termination phase: Property scanning
% 22.59/8.92 % (1482445)Time elapsed: 0.068 s
% 22.59/8.92 % (1482445)Peak memory usage: 201 MB
% 22.59/8.92 % (1482445)Instructions burned: 140 (million)
% 22.59/8.92 % (1482443)Instruction limit reached!
% 22.59/8.92 % (1482443)------------------------------
% 22.59/8.92 % (1482443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.59/8.92 % (1482443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/8.92 % (1482443)CaDiCaL version: 2.1.3
% 22.59/8.92 % (1482443)Termination reason: Instruction limit
% 22.59/8.92 % (1482443)Termination phase: SInE selection
% 22.59/8.92 % (1482443)Time elapsed: 0.086 s
% 22.59/8.92 % (1482443)Peak memory usage: 201 MB
% 22.59/8.92 % (1482443)Instructions burned: 110 (million)
% 22.59/8.92 % (1482444)Instruction limit reached!
% 22.59/8.92 % (1482444)------------------------------
% 22.59/8.92 % (1482444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.59/8.92 % (1482444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/8.92 % (1482444)CaDiCaL version: 2.1.3
% 22.59/8.92 % (1482444)Termination reason: Instruction limit
% 22.59/8.92 % (1482444)Termination phase: SInE selection
% 22.59/8.92 % (1482444)Time elapsed: 0.087 s
% 22.59/8.92 % (1482444)Peak memory usage: 201 MB
% 22.59/8.92 % (1482444)Instructions burned: 119 (million)
% 22.59/8.92 % (1482446)Instruction limit reached!
% 22.59/8.92 % (1482446)------------------------------
% 22.59/8.92 % (1482446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.59/8.92 % (1482446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/8.92 % (1482446)CaDiCaL version: 2.1.3
% 22.59/8.92 % (1482446)Termination reason: Instruction limit
% 22.59/8.92 % (1482446)Termination phase: SInE selection
% 22.59/8.92 % (1482446)Time elapsed: 0.095 s
% 22.59/8.92 % (1482446)Peak memory usage: 201 MB
% 22.59/8.92 % (1482446)Instructions burned: 130 (million)
% 22.59/8.92 % (1482454)lrs+10_1_sil=8000:sp=occurrence:random_seed=1267876407:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 22.59/8.92 % (1482455)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3130228261:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/157Mi)
% 22.59/8.92 % (1482456)lrs+1011_1_sil=32000:sp=occurrence:random_seed=883076861:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 22.59/8.92 % (1482457)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=4283034763:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 22.59/8.92 % (1482455)Instruction limit reached!
% 29.79/10.01 % (1482455)------------------------------
% 29.79/10.01 % (1482455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482455)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482455)Termination reason: Instruction limit
% 29.79/10.01 % (1482455)Termination phase: Property scanning
% 29.79/10.01 % (1482455)Time elapsed: 0.074 s
% 29.79/10.01 % (1482455)Peak memory usage: 201 MB
% 29.79/10.01 % (1482455)Instructions burned: 158 (million)
% 29.79/10.01 % (1482457)Instruction limit reached!
% 29.79/10.01 % (1482457)------------------------------
% 29.79/10.01 % (1482457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482457)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482457)Termination reason: Instruction limit
% 29.79/10.01 % (1482457)Termination phase: Property scanning
% 29.79/10.01 % (1482457)Time elapsed: 0.112 s
% 29.79/10.01 % (1482457)Peak memory usage: 201 MB
% 29.79/10.01 % (1482457)Instructions burned: 249 (million)
% 29.79/10.01 % (1482454)Instruction limit reached!
% 29.79/10.01 % (1482454)------------------------------
% 29.79/10.01 % (1482454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482454)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482454)Termination reason: Instruction limit
% 29.79/10.01 % (1482454)Termination phase: SInE selection
% 29.79/10.01 % (1482454)Time elapsed: 0.222 s
% 29.79/10.01 % (1482454)Peak memory usage: 201 MB
% 29.79/10.01 % (1482454)Instructions burned: 286 (million)
% 29.79/10.01 % (1482462)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=518211602:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 29.79/10.01 % (1482456)Instruction limit reached!
% 29.79/10.01 % (1482456)------------------------------
% 29.79/10.01 % (1482456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482456)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482456)Termination reason: Instruction limit
% 29.79/10.01 % (1482456)Termination phase: SInE selection
% 29.79/10.01 % (1482456)Time elapsed: 0.239 s
% 29.79/10.01 % (1482456)Peak memory usage: 201 MB
% 29.79/10.01 % (1482456)Instructions burned: 325 (million)
% 29.79/10.01 % (1482463)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1224704518:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 29.79/10.01 % (1482464)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2699176853:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 29.79/10.01 % (1482466)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=729377817:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 29.79/10.01 % (1482462)Instruction limit reached!
% 29.79/10.01 % (1482462)------------------------------
% 29.79/10.01 % (1482462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482462)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482462)Termination reason: Instruction limit
% 29.79/10.01 % (1482462)Termination phase: SInE selection
% 29.79/10.01 % (1482462)Time elapsed: 0.228 s
% 29.79/10.01 % (1482462)Peak memory usage: 201 MB
% 29.79/10.01 % (1482462)Instructions burned: 294 (million)
% 29.79/10.01 % (1482464)Instruction limit reached!
% 29.79/10.01 % (1482464)------------------------------
% 29.79/10.01 % (1482464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482464)CaDiCaL version: 2.1.3
% 29.79/10.01 % (1482464)Termination reason: Instruction limit
% 29.79/10.01 % (1482464)Termination phase: SInE selection
% 29.79/10.01 % (1482464)Time elapsed: 0.092 s
% 29.79/10.01 % (1482464)Peak memory usage: 201 MB
% 29.79/10.01 % (1482464)Instructions burned: 113 (million)
% 29.79/10.01 % (1482466)Instruction limit reached!
% 29.79/10.01 % (1482466)------------------------------
% 29.79/10.01 % (1482466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/10.01 % (1482466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/10.01 % (1482466)CaDiCaL version: 2.1.3
% 77.35/16.50 % (1482466)Termination reason: Instruction limit
% 77.35/16.50 % (1482466)Termination phase: Preprocessing 1
% 77.35/16.50 % (1482466)Time elapsed: 0.101 s
% 77.35/16.50 % (1482466)Peak memory usage: 202 MB
% 77.35/16.50 % (1482466)Instructions burned: 127 (million)
% 77.35/16.50 % (1482471)lrs+10_1_sil=8000:sp=occurrence:random_seed=2326991303:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 77.35/16.50 % (1482470)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2197479314:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 77.35/16.50 % (1482470)Instruction limit reached!
% 77.35/16.50 % (1482470)------------------------------
% 77.35/16.50 % (1482470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.35/16.50 % (1482470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.35/16.50 % (1482470)CaDiCaL version: 2.1.3
% 77.35/16.50 % (1482470)Termination reason: Instruction limit
% 77.35/16.50 % (1482470)Termination phase: Property scanning
% 77.35/16.50 % (1482470)Time elapsed: 0.058 s
% 77.35/16.50 % (1482470)Peak memory usage: 201 MB
% 77.35/16.50 % (1482470)Instructions burned: 115 (million)
% 77.35/16.51 % (1482472)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2549933066:i=437:sd=1:aac=none:ss=included_2934 on theBenchmark for (2934ds/437Mi)
% 77.35/16.51 % (1482476)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1472709554:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 77.35/16.51 % (1482472)Instruction limit reached!
% 77.35/16.51 % (1482472)------------------------------
% 77.35/16.51 % (1482472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.35/16.51 % (1482472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.35/16.51 % (1482472)CaDiCaL version: 2.1.3
% 77.35/16.51 % (1482472)Termination reason: Instruction limit
% 77.35/16.51 % (1482472)Termination phase: SInE selection
% 77.35/16.51 % (1482472)Time elapsed: 0.330 s
% 77.35/16.51 % (1482472)Peak memory usage: 202 MB
% 77.35/16.51 % (1482472)Instructions burned: 438 (million)
% 77.35/16.51 % (1482478)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2880284278:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2929 on theBenchmark for (2929ds/134Mi)
% 77.35/16.51 % (1482471)Instruction limit reached!
% 77.35/16.51 % (1482471)------------------------------
% 77.35/16.51 % (1482471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.35/16.51 % (1482471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.35/16.51 % (1482471)CaDiCaL version: 2.1.3
% 77.35/16.51 % (1482471)Termination reason: Instruction limit
% 77.35/16.51 % (1482471)Termination phase: Preprocessing 1
% 77.35/16.51 % (1482471)Time elapsed: 0.650 s
% 77.35/16.51 % (1482471)Peak memory usage: 204 MB
% 77.35/16.51 % (1482471)Instructions burned: 908 (million)
% 77.35/16.51 % (1482478)Instruction limit reached!
% 77.35/16.51 % (1482478)------------------------------
% 77.35/16.51 % (1482478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.35/16.51 % (1482478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.35/16.51 % (1482478)CaDiCaL version: 2.1.3
% 77.35/16.51 % (1482478)Termination reason: Instruction limit
% 77.35/16.51 % (1482478)Termination phase: SInE selection
% 77.35/16.51 % (1482478)Time elapsed: 0.103 s
% 77.35/16.51 % (1482478)Peak memory usage: 201 MB
% 77.35/16.51 % (1482478)Instructions burned: 134 (million)
% 77.35/16.51 % (1482480)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3359073698:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 77.35/16.51 % (1482481)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=403901149:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 77.35/16.51 % (1482480)Instruction limit reached!
% 77.35/16.51 % (1482480)------------------------------
% 77.35/16.51 % (1482480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.35/16.51 % (1482480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.35/16.51 % (1482480)CaDiCaL version: 2.1.3
% 77.35/16.51 % (1482480)Termination reason: Instruction limit
% 77.35/16.51 % (1482480)Termination phase: SInE selection
% 77.35/16.51 % (1482480)Time elapsed: 0.396 s
% 77.35/16.51 % (1482480)Peak memory usage: 203 MB
% 77.35/16.51 % (1482480)Instructions burned: 592 (million)
% 77.35/16.51 % (1482484)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=1694765584:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2921 on theBenchmark for (2921ds/125Mi)
% 49.86/17.83 % (1482484)Instruction limit reached!
% 49.86/17.83 % (1482484)------------------------------
% 49.86/17.83 % (1482484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482484)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482484)Termination reason: Instruction limit
% 49.86/17.83 % (1482484)Termination phase: Property scanning
% 49.86/17.83 % (1482484)Time elapsed: 0.063 s
% 49.86/17.83 % (1482484)Peak memory usage: 201 MB
% 49.86/17.83 % (1482484)Instructions burned: 127 (million)
% 49.86/17.83 % (1482463)Instruction limit reached!
% 49.86/17.83 % (1482463)------------------------------
% 49.86/17.83 % (1482463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482463)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482463)Termination reason: Instruction limit
% 49.86/17.83 % (1482463)Termination phase: Preprocessing 3
% 49.86/17.83 % (1482463)Time elapsed: 1.851 s
% 49.86/17.83 % (1482463)Peak memory usage: 305 MB
% 49.86/17.83 % (1482463)Instructions burned: 2351 (million)
% 49.86/17.83 % (1482486)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4089949785:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 49.86/17.83 % (1482487)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1319621849:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2918 on theBenchmark for (2918ds/141Mi)
% 49.86/17.83 % (1482486)Instruction limit reached!
% 49.86/17.83 % (1482486)------------------------------
% 49.86/17.83 % (1482486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482486)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482486)Termination reason: Instruction limit
% 49.86/17.83 % (1482486)Termination phase: Property scanning
% 49.86/17.83 % (1482486)Time elapsed: 0.065 s
% 49.86/17.83 % (1482486)Peak memory usage: 201 MB
% 49.86/17.83 % (1482486)Instructions burned: 136 (million)
% 49.86/17.83 % (1482487)Instruction limit reached!
% 49.86/17.83 % (1482487)------------------------------
% 49.86/17.83 % (1482487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482487)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482487)Termination reason: Instruction limit
% 49.86/17.83 % (1482487)Termination phase: SInE selection
% 49.86/17.83 % (1482487)Time elapsed: 0.108 s
% 49.86/17.83 % (1482487)Peak memory usage: 201 MB
% 49.86/17.83 % (1482487)Instructions burned: 141 (million)
% 49.86/17.83 % (1482490)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1501827454:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2916 on theBenchmark for (2916ds/431Mi)
% 49.86/17.83 % (1482491)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=2344479456:i=6060:aac=none:ins=25_2915 on theBenchmark for (2915ds/6060Mi)
% 49.86/17.83 % (1482490)Instruction limit reached!
% 49.86/17.83 % (1482490)------------------------------
% 49.86/17.83 % (1482490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482490)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482490)Termination reason: Instruction limit
% 49.86/17.83 % (1482490)Termination phase: SInE selection
% 49.86/17.83 % (1482490)Time elapsed: 0.329 s
% 49.86/17.83 % (1482490)Peak memory usage: 202 MB
% 49.86/17.83 % (1482490)Instructions burned: 431 (million)
% 49.86/17.83 % (1482494)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=509551958:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2911 on theBenchmark for (2911ds/150Mi)
% 49.86/17.83 % (1482494)Instruction limit reached!
% 49.86/17.83 % (1482494)------------------------------
% 49.86/17.83 % (1482494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482494)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482494)Termination reason: Instruction limit
% 49.86/17.83 % (1482494)Termination phase: SInE selection
% 49.86/17.83 % (1482494)Time elapsed: 0.114 s
% 49.86/17.83 % (1482494)Peak memory usage: 201 MB
% 49.86/17.83 % (1482494)Instructions burned: 150 (million)
% 49.86/17.83 % (1482496)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3990785054:i=14155:bd=all_2908 on theBenchmark for (2908ds/14155Mi)
% 49.86/17.83 % (1482476)Instruction limit reached!
% 49.86/17.83 % (1482476)------------------------------
% 49.86/17.83 % (1482476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482476)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482476)Termination reason: Instruction limit
% 49.86/17.83 % (1482476)Termination phase: Saturation
% 49.86/17.83 % (1482476)Time elapsed: 3.571 s
% 49.86/17.83 % (1482476)Peak memory usage: 427 MB
% 49.86/17.83 % (1482476)Instructions burned: 5203 (million)
% 49.86/17.83 % (1482498)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3421584816:i=667:av=off:fsr=off_2895 on theBenchmark for (2895ds/667Mi)
% 49.86/17.83 % (1482498)Instruction limit reached!
% 49.86/17.83 % (1482498)------------------------------
% 49.86/17.83 % (1482498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482498)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482498)Termination reason: Instruction limit
% 49.86/17.83 % (1482498)Termination phase: Preprocessing 2
% 49.86/17.83 % (1482498)Time elapsed: 0.615 s
% 49.86/17.83 % (1482498)Peak memory usage: 218 MB
% 49.86/17.83 % (1482498)Instructions burned: 668 (million)
% 49.86/17.83 % (1482500)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=1956318804:s2a=on:i=185:s2at=1.8:fdi=4_2887 on theBenchmark for (2887ds/185Mi)
% 49.86/17.83 % (1482500)Instruction limit reached!
% 49.86/17.83 % (1482500)------------------------------
% 49.86/17.83 % (1482500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482500)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482500)Termination reason: Instruction limit
% 49.86/17.83 % (1482500)Termination phase: SInE selection
% 49.86/17.83 % (1482500)Time elapsed: 0.150 s
% 49.86/17.83 % (1482500)Peak memory usage: 201 MB
% 49.86/17.83 % (1482500)Instructions burned: 186 (million)
% 49.86/17.83 % (1482502)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2229333243:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2883 on theBenchmark for (2883ds/193Mi)
% 49.86/17.83 % (1482502)Instruction limit reached!
% 49.86/17.83 % (1482502)------------------------------
% 49.86/17.83 % (1482502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482502)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482502)Termination reason: Instruction limit
% 49.86/17.83 % (1482502)Termination phase: SInE selection
% 49.86/17.83 % (1482502)Time elapsed: 0.154 s
% 49.86/17.83 % (1482502)Peak memory usage: 201 MB
% 49.86/17.83 % (1482502)Instructions burned: 193 (million)
% 49.86/17.83 % (1482504)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1824065791:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2880 on theBenchmark for (2880ds/4850Mi)
% 49.86/17.83 % (1482491)Instruction limit reached!
% 49.86/17.83 % (1482491)------------------------------
% 49.86/17.83 % (1482491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.83 % (1482491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.83 % (1482491)CaDiCaL version: 2.1.3
% 49.86/17.83 % (1482491)Termination reason: Instruction limit
% 49.86/17.83 % (1482491)Termination phase: NewCNF
% 49.86/17.83 % (1482491)Time elapsed: 4.864 s
% 49.86/17.83 % (1482491)Peak memory usage: 381 MB
% 49.86/17.83 % (1482491)Instructions burned: 6060 (million)
% 49.86/17.83 % (1482506)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3770755806:i=12111:sd=1:ss=included_2865 on theBenchmark for (2865ds/12111Mi)
% 49.86/17.83 % (1482504)Instruction limit reached!
% 49.86/17.83 % (1482504)------------------------------
% 49.86/17.83 % (1482504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.84 % (1482504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.84 % (1482504)CaDiCaL version: 2.1.3
% 49.86/17.84 % (1482504)Termination reason: Instruction limit
% 49.86/17.84 % (1482504)Termination phase: Property scanning
% 49.86/17.84 % (1482504)Time elapsed: 3.473 s
% 49.86/17.84 % (1482504)Peak memory usage: 362 MB
% 49.86/17.84 % (1482504)Instructions burned: 4852 (million)
% 49.86/17.84 % (1482508)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1541834486:i=319:kws=precedence:fsr=off_2843 on theBenchmark for (2843ds/319Mi)
% 49.86/17.84 % (1482481)Instruction limit reached!
% 49.86/17.84 % (1482481)------------------------------
% 49.86/17.84 % (1482481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.84 % (1482481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.84 % (1482481)CaDiCaL version: 2.1.3
% 49.86/17.84 % (1482481)Termination reason: Instruction limit
% 49.86/17.84 % (1482481)Termination phase: Saturation
% 49.86/17.84 % (1482481)Time elapsed: 8.496 s
% 49.86/17.84 % (1482481)Peak memory usage: 608 MB
% 49.86/17.84 % (1482481)Instructions burned: 13194 (million)
% 49.86/17.84 % (1482508)Instruction limit reached!
% 49.86/17.84 % (1482508)------------------------------
% 49.86/17.84 % (1482508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.84 % (1482508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.84 % (1482508)CaDiCaL version: 2.1.3
% 49.86/17.84 % (1482508)Termination reason: Instruction limit
% 49.86/17.84 % (1482508)Termination phase: Preprocessing 1
% 49.86/17.84 % (1482508)Time elapsed: 0.232 s
% 49.86/17.84 % (1482508)Peak memory usage: 203 MB
% 49.86/17.84 % (1482508)Instructions burned: 319 (million)
% 49.86/17.84 % (1482510)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2954848583:i=2064:ep=RST_2839 on theBenchmark for (2839ds/2064Mi)
% 49.86/17.84 % (1482511)dis-1011_128_sil=32000:random_seed=1555751828:i=3706:ep=RST:av=off_2839 on theBenchmark for (2839ds/3706Mi)
% 49.86/17.84 % (1482496)Instruction limit reached!
% 49.86/17.84 % (1482496)------------------------------
% 49.86/17.84 % (1482496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.86/17.84 % (1482496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.86/17.84 % (1482496)CaDiCaL version: 2.1.3
% 49.86/17.84 % (1482496)Termination reason: Instruction limit
% 49.86/17.84 % (1482496)Termination phase: Property scanning
% 49.86/17.84 % (1482496)Time elapsed: 7.086 s
% 49.86/17.84 % (1482496)Peak memory usage: 447 MB
% 49.86/17.84 % (1482496)Instructions burned: 14156 (million)
% 49.86/17.84 % (1482506)First to succeed.
% 49.86/17.84 % (1482506)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1482435"
% 49.86/17.84 % (1482514)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=706707145:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2835 on theBenchmark for (2835ds/757Mi)
% 49.86/17.84 % (1482506)Refutation found. Thanks to Tanya!
% 49.86/17.84 % SZS status Theorem for theBenchmark
% 49.86/17.84 % SZS output start Proof for theBenchmark
% See solution above
% 86.09/17.99 % (1482506)------------------------------
% 86.09/17.99 % (1482506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.09/17.99 % (1482506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.09/17.99 % (1482506)CaDiCaL version: 2.1.3
% 86.09/17.99 % (1482506)Termination reason: Refutation
% 86.09/17.99 % (1482506)Time elapsed: 2.810 s
% 86.09/17.99 % (1482506)Peak memory usage: 291 MB
% 86.09/17.99 % (1482506)Instructions burned: 4105 (million)
% 86.09/17.99 % (1482506)------------------------------
% 86.09/17.99 % (1482506)------------------------------
% 86.09/17.99 % (1482435)Success in time 16.929 s
% 86.09/17.99 % Vampire exiting
%------------------------------------------------------------------------------