%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU445+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 : n003.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:08 PM UTC 2026
% Result : Theorem 19.76s 8.46s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 29
% Syntax : Number of formulae : 169 ( 21 unt; 14 def)
% Number of atoms : 414 ( 87 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 447 ( 202 ~; 198 |; 16 &)
% ( 15 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 15 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-5 aty)
% Number of variables : 145 ( 0 sgn 142 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f740,axiom,
! [X0] :
( v1_relat_1(X0)
=> ( k2_relat_1(X0) = k1_relat_1(k4_relat_1(X0))
& k1_relat_1(X0) = k2_relat_1(k4_relat_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_relat_1) ).
fof(f855,axiom,
! [X0] :
( v1_relat_1(X0)
=> k9_relat_1(X0,k1_relat_1(X0)) = k2_relat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t146_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/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1461,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( k10_relset_1(X0,X1,X2,X0) = k5_relset_1(X0,X1,X2)
& k11_relset_1(X0,X1,X2,X1) = k4_relset_1(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_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/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1498,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f1500,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_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/sandbox/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f6128,axiom,
! [X0] :
( v1_relat_1(X0)
=> ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_funct_5) ).
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/sandbox/benchmark/theBenchmark.p',dt_k9_relset_2) ).
fof(f71133,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_relset_2) ).
fof(f71135,axiom,
! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_relset_2) ).
fof(f71138,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k10_relset_1(X1,X0,X2,X1)) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k2_funct_5(X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_relset_2) ).
fof(f71139,conjecture,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) = k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t57_relset_2) ).
fof(f71140,negated_conjecture,
~ ! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) = k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1) ),
inference(negated_conjecture,[status(cth)],[f71139]) ).
fof(f71226,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(f71227,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,[],[f71226]) ).
fof(f71290,plain,
! [X0,X1,X2] :
( ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f71133]) ).
fof(f71292,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) )
| ~ m2_relset_1(X4,X1,X2) )
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f71135]) ).
fof(f71295,plain,
! [X0,X1,X2] :
( ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k10_relset_1(X1,X0,X2,X1)) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k2_funct_5(X2)) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f71138]) ).
fof(f71296,plain,
? [X0,X1,X2] :
( k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) != k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1)
& m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f71140]) ).
fof(f71397,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(f71398,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(f71500,plain,
! [X0] :
( k9_relat_1(X0,k1_relat_1(X0)) = k2_relat_1(X0)
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f855]) ).
fof(f71852,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(f71931,plain,
! [X0,X1,X2] :
( ( k10_relset_1(X0,X1,X2,X0) = k5_relset_1(X0,X1,X2)
& k11_relset_1(X0,X1,X2,X1) = k4_relset_1(X0,X1,X2) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1461]) ).
fof(f72283,plain,
! [X0] :
( ( k2_relat_1(X0) = k1_relat_1(k4_relat_1(X0))
& k1_relat_1(X0) = k2_relat_1(k4_relat_1(X0)) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f740]) ).
fof(f72299,plain,
! [X0] :
( ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f6128]) ).
fof(f72308,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1500]) ).
fof(f72310,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1498]) ).
fof(f72339,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) != k10_relset_1(sK11,sK11,k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11)
& m2_relset_1(sK12,sK11,sK10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12)],[f71296]) ).
fof(f72365,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(f72733,plain,
! [X2,X3,X0,X1,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(cnf_transformation,[],[f71227]) ).
fof(f72814,plain,
! [X2,X0,X1] :
( k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f71290]) ).
fof(f72819,plain,
! [X2,X3,X0,X1,X4] :
( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
| ~ m2_relset_1(X4,X1,X2)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f71292]) ).
fof(f72824,plain,
! [X2,X0,X1] :
( k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k10_relset_1(X1,X0,X2,X1)) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k2_funct_5(X2))
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f71295]) ).
fof(f72825,plain,
! [X2,X0,X1] :
( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f71295]) ).
fof(f72826,plain,
m2_relset_1(sK12,sK11,sK10),
inference(cnf_transformation,[],[f72339]) ).
fof(f72827,plain,
k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) != k10_relset_1(sK11,sK11,k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11),
inference(cnf_transformation,[],[f72339]) ).
fof(f72975,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72365]) ).
fof(f72990,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71397]) ).
fof(f72991,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71398]) ).
fof(f73088,plain,
! [X0] :
( k2_relat_1(X0) = k9_relat_1(X0,k1_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f71500]) ).
fof(f73673,plain,
! [X2,X3,X0,X1] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71852]) ).
fof(f73847,plain,
! [X2,X0,X1] :
( k5_relset_1(X0,X1,X2) = k10_relset_1(X0,X1,X2,X0)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71931]) ).
fof(f74321,plain,
! [X0] :
( k1_relat_1(X0) = k2_relat_1(k4_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72283]) ).
fof(f74322,plain,
! [X0] :
( k2_relat_1(X0) = k1_relat_1(k4_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72283]) ).
fof(f74360,plain,
! [X0] :
( k2_relat_1(X0) = k2_funct_5(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72299]) ).
fof(f74361,plain,
! [X0] :
( k1_relat_1(X0) = k1_funct_5(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72299]) ).
fof(f74402,plain,
! [X2,X0,X1] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72308]) ).
fof(f74404,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72310]) ).
fof(f75772,definition,
( spl542_1
<=> k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) = k10_relset_1(sK11,sK11,k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11) ),
introduced(definition,[new_symbols(definition,[spl542_1])],[avatar_definition]) ).
fof(f75774,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) != k10_relset_1(sK11,sK11,k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11)
| spl542_1 ),
inference(avatar_component_clause,[],[f75772]) ).
fof(f75775,plain,
~ spl542_1,
inference(avatar_split_clause,[],[f72827,f75772]) ).
fof(f75777,definition,
( spl542_2
<=> m2_relset_1(sK12,sK11,sK10) ),
introduced(definition,[new_symbols(definition,[spl542_2])],[avatar_definition]) ).
fof(f75779,plain,
( m2_relset_1(sK12,sK11,sK10)
| ~ spl542_2 ),
inference(avatar_component_clause,[],[f75777]) ).
fof(f75780,plain,
spl542_2,
inference(avatar_split_clause,[],[f72826,f75777]) ).
fof(f75801,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k10_relset_1(sK11,sK10,sK12,sK11)) = k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| ~ spl542_2 ),
inference(resolution,[],[f75779,f72824]) ).
fof(f75802,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) = k1_funct_5(sK12)
| ~ spl542_2 ),
inference(resolution,[],[f75779,f72825]) ).
fof(f75803,plain,
( m1_relset_1(sK12,sK11,sK10)
| ~ spl542_2 ),
inference(resolution,[],[f75779,f72975]) ).
fof(f75804,plain,
( m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK11,sK10)))
| ~ spl542_2 ),
inference(resolution,[],[f75779,f72990]) ).
fof(f75847,plain,
( k10_relset_1(sK11,sK10,sK12,sK11) = k5_relset_1(sK11,sK10,sK12)
| ~ spl542_2 ),
inference(resolution,[],[f75779,f73847]) ).
fof(f75918,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) = k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12))
| ~ spl542_2 ),
inference(forward_demodulation,[],[f75801,f75847]) ).
fof(f75931,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),sK10) != k2_funct_5(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)))
| ~ m2_relset_1(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11,sK11)
| spl542_1 ),
inference(superposition,[],[f75774,f72814]) ).
fof(f75934,plain,
( k1_funct_5(sK12) != k2_funct_5(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)))
| ~ m2_relset_1(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11,sK11)
| spl542_1
| ~ spl542_2 ),
inference(forward_demodulation,[],[f75931,f75802]) ).
fof(f75959,definition,
( spl542_4
<=> k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) = k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12)) ),
introduced(definition,[new_symbols(definition,[spl542_4])],[avatar_definition]) ).
fof(f75961,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) = k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12))
| ~ spl542_4 ),
inference(avatar_component_clause,[],[f75959]) ).
fof(f75962,plain,
( spl542_4
| ~ spl542_2 ),
inference(avatar_split_clause,[],[f75918,f75777,f75959]) ).
fof(f75964,definition,
( spl542_5
<=> m2_relset_1(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11,sK11) ),
introduced(definition,[new_symbols(definition,[spl542_5])],[avatar_definition]) ).
fof(f75966,plain,
( ~ m2_relset_1(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)),sK11,sK11)
| spl542_5 ),
inference(avatar_component_clause,[],[f75964]) ).
fof(f75968,definition,
( spl542_6
<=> k1_funct_5(sK12) = k2_funct_5(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12))) ),
introduced(definition,[new_symbols(definition,[spl542_6])],[avatar_definition]) ).
fof(f75970,plain,
( k1_funct_5(sK12) != k2_funct_5(k9_relset_2(sK11,sK10,sK11,sK12,k6_relset_1(sK11,sK10,sK12)))
| spl542_6 ),
inference(avatar_component_clause,[],[f75968]) ).
fof(f75971,plain,
( ~ spl542_5
| ~ spl542_6
| spl542_1
| ~ spl542_2 ),
inference(avatar_split_clause,[],[f75934,f75777,f75772,f75968,f75964]) ).
fof(f75972,plain,
( ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK11,sK10)))
| ~ m1_subset_1(k6_relset_1(sK11,sK10,sK12),k1_zfmisc_1(k2_zfmisc_1(sK10,sK11)))
| spl542_5 ),
inference(resolution,[],[f75966,f72733]) ).
fof(f75995,plain,
( ~ m1_subset_1(k6_relset_1(sK11,sK10,sK12),k1_zfmisc_1(k2_zfmisc_1(sK10,sK11)))
| ~ spl542_2
| spl542_5 ),
inference(forward_subsumption_resolution,[],[f75972,f75804]) ).
fof(f75997,definition,
( spl542_7
<=> m1_subset_1(k6_relset_1(sK11,sK10,sK12),k1_zfmisc_1(k2_zfmisc_1(sK10,sK11))) ),
introduced(definition,[new_symbols(definition,[spl542_7])],[avatar_definition]) ).
fof(f75998,plain,
( m1_subset_1(k6_relset_1(sK11,sK10,sK12),k1_zfmisc_1(k2_zfmisc_1(sK10,sK11)))
| ~ spl542_7 ),
inference(avatar_component_clause,[],[f75997]) ).
fof(f75999,plain,
( ~ m1_subset_1(k6_relset_1(sK11,sK10,sK12),k1_zfmisc_1(k2_zfmisc_1(sK10,sK11)))
| spl542_7 ),
inference(avatar_component_clause,[],[f75997]) ).
fof(f76000,plain,
( ~ spl542_7
| ~ spl542_2
| spl542_5 ),
inference(avatar_split_clause,[],[f75995,f75964,f75777,f75997]) ).
fof(f76001,plain,
( ~ m2_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| spl542_7 ),
inference(resolution,[],[f75999,f72990]) ).
fof(f76045,definition,
( spl542_8
<=> m2_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11) ),
introduced(definition,[new_symbols(definition,[spl542_8])],[avatar_definition]) ).
fof(f76046,plain,
( m2_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| ~ spl542_8 ),
inference(avatar_component_clause,[],[f76045]) ).
fof(f76047,plain,
( ~ m2_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| spl542_8 ),
inference(avatar_component_clause,[],[f76045]) ).
fof(f76048,plain,
( ~ spl542_8
| spl542_7 ),
inference(avatar_split_clause,[],[f76001,f75997,f76045]) ).
fof(f76049,plain,
( ~ m1_relset_1(sK12,sK11,sK10)
| spl542_8 ),
inference(resolution,[],[f76047,f74404]) ).
fof(f76070,plain,
( $false
| ~ spl542_2
| spl542_8 ),
inference(forward_subsumption_resolution,[],[f76049,f75803]) ).
fof(f76071,plain,
( ~ spl542_2
| spl542_8 ),
inference(avatar_contradiction_clause,[],[f76070]) ).
fof(f76338,plain,
( m1_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| ~ spl542_8 ),
inference(resolution,[],[f76046,f72975]) ).
fof(f76540,plain,
( k1_funct_5(sK12) != k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| ~ m2_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| ~ m2_relset_1(sK12,sK11,sK10)
| spl542_6 ),
inference(superposition,[],[f75970,f72819]) ).
fof(f76550,plain,
( k1_funct_5(sK12) != k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| ~ m2_relset_1(sK12,sK11,sK10)
| spl542_6
| ~ spl542_8 ),
inference(forward_subsumption_resolution,[],[f76540,f76046]) ).
fof(f76554,plain,
( k1_funct_5(sK12) != k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| ~ spl542_2
| spl542_6
| ~ spl542_8 ),
inference(forward_subsumption_resolution,[],[f76550,f75779]) ).
fof(f76641,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) = k9_relat_1(k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12))
| ~ m1_relset_1(k6_relset_1(sK11,sK10,sK12),sK10,sK11)
| ~ spl542_4 ),
inference(superposition,[],[f73673,f75961]) ).
fof(f76653,plain,
( k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) = k9_relat_1(k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12))
| ~ spl542_4
| ~ spl542_8 ),
inference(forward_subsumption_resolution,[],[f76641,f76338]) ).
fof(f76726,definition,
( spl542_18
<=> m1_relset_1(sK12,sK11,sK10) ),
introduced(definition,[new_symbols(definition,[spl542_18])],[avatar_definition]) ).
fof(f76728,plain,
( m1_relset_1(sK12,sK11,sK10)
| ~ spl542_18 ),
inference(avatar_component_clause,[],[f76726]) ).
fof(f76729,plain,
( spl542_18
| ~ spl542_2 ),
inference(avatar_split_clause,[],[f75803,f75777,f76726]) ).
fof(f76736,plain,
( ! [X0] : k10_relset_1(sK11,sK10,sK12,X0) = k9_relat_1(sK12,X0)
| ~ spl542_18 ),
inference(resolution,[],[f76728,f73673]) ).
fof(f76740,plain,
( k6_relset_1(sK11,sK10,sK12) = k4_relat_1(sK12)
| ~ spl542_18 ),
inference(resolution,[],[f76728,f74402]) ).
fof(f76745,definition,
( spl542_19
<=> ! [X0] : k10_relset_1(sK11,sK10,sK12,X0) = k9_relat_1(sK12,X0) ),
introduced(definition,[new_symbols(definition,[spl542_19])],[avatar_definition]) ).
fof(f76746,plain,
( ! [X0] : k10_relset_1(sK11,sK10,sK12,X0) = k9_relat_1(sK12,X0)
| ~ spl542_19 ),
inference(avatar_component_clause,[],[f76745]) ).
fof(f76747,plain,
( spl542_19
| ~ spl542_18 ),
inference(avatar_split_clause,[],[f76736,f76726,f76745]) ).
fof(f76752,plain,
( k9_relat_1(sK12,sK11) = k5_relset_1(sK11,sK10,sK12)
| ~ m2_relset_1(sK12,sK11,sK10)
| ~ spl542_19 ),
inference(superposition,[],[f73847,f76746]) ).
fof(f76755,plain,
( k2_funct_5(sK12) = k9_relat_1(sK12,sK11)
| ~ m2_relset_1(sK12,sK11,sK10)
| ~ spl542_19 ),
inference(superposition,[],[f72814,f76746]) ).
fof(f76780,plain,
( k2_funct_5(sK12) = k9_relat_1(sK12,sK11)
| ~ spl542_2
| ~ spl542_19 ),
inference(forward_subsumption_resolution,[],[f76755,f75779]) ).
fof(f76783,plain,
( k9_relat_1(sK12,sK11) = k5_relset_1(sK11,sK10,sK12)
| ~ spl542_2
| ~ spl542_19 ),
inference(forward_subsumption_resolution,[],[f76752,f75779]) ).
fof(f76798,plain,
( k2_funct_5(sK12) = k5_relset_1(sK11,sK10,sK12)
| ~ spl542_2
| ~ spl542_19 ),
inference(forward_demodulation,[],[f76783,f76780]) ).
fof(f76811,definition,
( spl542_20
<=> k6_relset_1(sK11,sK10,sK12) = k4_relat_1(sK12) ),
introduced(definition,[new_symbols(definition,[spl542_20])],[avatar_definition]) ).
fof(f76813,plain,
( k6_relset_1(sK11,sK10,sK12) = k4_relat_1(sK12)
| ~ spl542_20 ),
inference(avatar_component_clause,[],[f76811]) ).
fof(f76814,plain,
( spl542_20
| ~ spl542_18 ),
inference(avatar_split_clause,[],[f76740,f76726,f76811]) ).
fof(f76984,plain,
( v1_relat_1(k6_relset_1(sK11,sK10,sK12))
| ~ spl542_7 ),
inference(resolution,[],[f75998,f72991]) ).
fof(f77585,plain,
( v1_relat_1(k4_relat_1(sK12))
| ~ spl542_7
| ~ spl542_20 ),
inference(forward_demodulation,[],[f76984,f76813]) ).
fof(f78802,definition,
( spl542_28
<=> m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK11,sK10))) ),
introduced(definition,[new_symbols(definition,[spl542_28])],[avatar_definition]) ).
fof(f78804,plain,
( m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK11,sK10)))
| ~ spl542_28 ),
inference(avatar_component_clause,[],[f78802]) ).
fof(f78805,plain,
( spl542_28
| ~ spl542_2 ),
inference(avatar_split_clause,[],[f75804,f75777,f78802]) ).
fof(f78835,plain,
( v1_relat_1(sK12)
| ~ spl542_28 ),
inference(resolution,[],[f78804,f72991]) ).
fof(f79456,definition,
( spl542_29
<=> v1_relat_1(sK12) ),
introduced(definition,[new_symbols(definition,[spl542_29])],[avatar_definition]) ).
fof(f79458,plain,
( v1_relat_1(sK12)
| ~ spl542_29 ),
inference(avatar_component_clause,[],[f79456]) ).
fof(f79459,plain,
( spl542_29
| ~ spl542_28 ),
inference(avatar_split_clause,[],[f78835,f78802,f79456]) ).
fof(f79839,plain,
( k1_relat_1(sK12) = k2_relat_1(k4_relat_1(sK12))
| ~ spl542_29 ),
inference(resolution,[],[f79458,f74321]) ).
fof(f79840,plain,
( k2_relat_1(sK12) = k1_relat_1(k4_relat_1(sK12))
| ~ spl542_29 ),
inference(resolution,[],[f79458,f74322]) ).
fof(f79843,plain,
( k2_funct_5(sK12) = k2_relat_1(sK12)
| ~ spl542_29 ),
inference(resolution,[],[f79458,f74360]) ).
fof(f79844,plain,
( k1_funct_5(sK12) = k1_relat_1(sK12)
| ~ spl542_29 ),
inference(resolution,[],[f79458,f74361]) ).
fof(f80613,definition,
( spl542_40
<=> k1_funct_5(sK12) = k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12)) ),
introduced(definition,[new_symbols(definition,[spl542_40])],[avatar_definition]) ).
fof(f80615,plain,
( k1_funct_5(sK12) != k10_relset_1(sK10,sK11,k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| spl542_40 ),
inference(avatar_component_clause,[],[f80613]) ).
fof(f80616,plain,
( ~ spl542_40
| ~ spl542_2
| spl542_6
| ~ spl542_8 ),
inference(avatar_split_clause,[],[f76554,f76045,f75968,f75777,f80613]) ).
fof(f80617,plain,
( k1_funct_5(sK12) != k9_relat_1(k6_relset_1(sK11,sK10,sK12),k5_relset_1(sK11,sK10,sK12))
| ~ spl542_4
| ~ spl542_8
| spl542_40 ),
inference(forward_demodulation,[],[f80615,f76653]) ).
fof(f80618,plain,
( k1_funct_5(sK12) != k9_relat_1(k6_relset_1(sK11,sK10,sK12),k2_funct_5(sK12))
| ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| spl542_40 ),
inference(forward_demodulation,[],[f80617,f76798]) ).
fof(f80619,plain,
( k1_funct_5(sK12) != k9_relat_1(k6_relset_1(sK11,sK10,sK12),k2_relat_1(sK12))
| ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_29
| spl542_40 ),
inference(forward_demodulation,[],[f80618,f79843]) ).
fof(f80620,plain,
( k1_funct_5(sK12) != k9_relat_1(k4_relat_1(sK12),k2_relat_1(sK12))
| ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_20
| ~ spl542_29
| spl542_40 ),
inference(forward_demodulation,[],[f80619,f76813]) ).
fof(f80621,plain,
( k1_relat_1(sK12) != k9_relat_1(k4_relat_1(sK12),k2_relat_1(sK12))
| ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_20
| ~ spl542_29
| spl542_40 ),
inference(forward_demodulation,[],[f80620,f79844]) ).
fof(f80869,definition,
( spl542_47
<=> v1_relat_1(k4_relat_1(sK12)) ),
introduced(definition,[new_symbols(definition,[spl542_47])],[avatar_definition]) ).
fof(f80871,plain,
( v1_relat_1(k4_relat_1(sK12))
| ~ spl542_47 ),
inference(avatar_component_clause,[],[f80869]) ).
fof(f80872,plain,
( spl542_47
| ~ spl542_7
| ~ spl542_20 ),
inference(avatar_split_clause,[],[f77585,f76811,f75997,f80869]) ).
fof(f80943,plain,
( k2_relat_1(k4_relat_1(sK12)) = k9_relat_1(k4_relat_1(sK12),k1_relat_1(k4_relat_1(sK12)))
| ~ spl542_47 ),
inference(resolution,[],[f80871,f73088]) ).
fof(f81910,plain,
( k2_relat_1(k4_relat_1(sK12)) = k9_relat_1(k4_relat_1(sK12),k2_relat_1(sK12))
| ~ spl542_29
| ~ spl542_47 ),
inference(forward_demodulation,[],[f80943,f79840]) ).
fof(f82129,plain,
( k1_relat_1(sK12) = k9_relat_1(k4_relat_1(sK12),k2_relat_1(sK12))
| ~ spl542_29
| ~ spl542_47 ),
inference(forward_demodulation,[],[f81910,f79839]) ).
fof(f82198,plain,
( $false
| ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_20
| ~ spl542_29
| spl542_40
| ~ spl542_47 ),
inference(forward_subsumption_resolution,[],[f82129,f80621]) ).
fof(f82199,plain,
( ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_20
| ~ spl542_29
| spl542_40
| ~ spl542_47 ),
inference(avatar_contradiction_clause,[],[f82198]) ).
cnf(s1,plain,
~ spl542_1,
inference(sat_conversion,[],[f75775]) ).
cnf(s2,plain,
spl542_2,
inference(sat_conversion,[],[f75780]) ).
cnf(s4,plain,
( ~ spl542_2
| spl542_4 ),
inference(sat_conversion,[],[f75962]) ).
cnf(s5,plain,
( spl542_1
| ~ spl542_2
| ~ spl542_5
| ~ spl542_6 ),
inference(sat_conversion,[],[f75971]) ).
cnf(s6,plain,
( ~ spl542_2
| spl542_5
| ~ spl542_7 ),
inference(sat_conversion,[],[f76000]) ).
cnf(s7,plain,
( spl542_7
| ~ spl542_8 ),
inference(sat_conversion,[],[f76048]) ).
cnf(s8,plain,
( ~ spl542_2
| spl542_8 ),
inference(sat_conversion,[],[f76071]) ).
cnf(s18,plain,
( ~ spl542_2
| spl542_18 ),
inference(sat_conversion,[],[f76729]) ).
cnf(s19,plain,
( ~ spl542_18
| spl542_19 ),
inference(sat_conversion,[],[f76747]) ).
cnf(s20,plain,
( ~ spl542_18
| spl542_20 ),
inference(sat_conversion,[],[f76814]) ).
cnf(s28,plain,
( ~ spl542_2
| spl542_28 ),
inference(sat_conversion,[],[f78805]) ).
cnf(s29,plain,
( ~ spl542_28
| spl542_29 ),
inference(sat_conversion,[],[f79459]) ).
cnf(s40,plain,
( ~ spl542_2
| spl542_6
| ~ spl542_8
| ~ spl542_40 ),
inference(sat_conversion,[],[f80616]) ).
cnf(s47,plain,
( ~ spl542_7
| ~ spl542_20
| spl542_47 ),
inference(sat_conversion,[],[f80872]) ).
cnf(s48,plain,
( ~ spl542_2
| ~ spl542_4
| ~ spl542_8
| ~ spl542_19
| ~ spl542_20
| ~ spl542_29
| spl542_40
| ~ spl542_47 ),
inference(sat_conversion,[],[f82199]) ).
cnf(s53,plain,
spl542_28,
inference(rat,[],[s28,s2]) ).
cnf(s56,plain,
spl542_18,
inference(rat,[],[s18,s2]) ).
cnf(s57,plain,
spl542_8,
inference(rat,[],[s8,s2]) ).
cnf(s58,plain,
spl542_4,
inference(rat,[],[s4,s2]) ).
cnf(s61,plain,
spl542_29,
inference(rat,[],[s29,s53]) ).
cnf(s64,plain,
spl542_20,
inference(rat,[],[s20,s56]) ).
cnf(s65,plain,
spl542_19,
inference(rat,[],[s19,s56]) ).
cnf(s67,plain,
spl542_7,
inference(rat,[],[s7,s57]) ).
cnf(s70,plain,
spl542_47,
inference(rat,[],[s47,s64,s67]) ).
cnf(s71,plain,
spl542_5,
inference(rat,[],[s6,s2,s67]) ).
cnf(s73,plain,
spl542_40,
inference(rat,[],[s48,s58,s57,s61,s64,s65,s2,s70]) ).
cnf(s79,plain,
spl542_6,
inference(rat,[],[s40,s57,s2,s73]) ).
cnf(s80,plain,
spl542_1,
inference(rat,[],[s5,s71,s2,s79]) ).
cnf(s81,plain,
$false,
inference(rat,[],[s1,s80]) ).
fof(f82226,plain,
$false,
inference(avatar_sat_refutation,[],[s81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU445+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 05:38:04 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 19.76/8.46 % (1263830)Detected formulas, will run a generic FOF schedule.
% 19.76/8.46 % (1263837)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=3444480869:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 19.76/8.46 % (1263836)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=3067709189:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 19.76/8.46 % (1263835)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=2299161469:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 19.76/8.46 % (1263838)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1944774044:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 19.76/8.46 % (1263839)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2898095786:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 19.76/8.46 % (1263840)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2198418865:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 19.76/8.46 % (1263841)dis-21_1_sil=8000:lcm=predicate:random_seed=585415391: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)
% 19.76/8.46 % (1263838)Instruction limit reached!
% 19.76/8.46 % (1263838)------------------------------
% 19.76/8.46 % (1263838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263838)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263838)Termination reason: Instruction limit
% 19.76/8.46 % (1263838)Termination phase: SInE selection
% 19.76/8.46 % (1263838)Time elapsed: 0.082 s
% 19.76/8.46 % (1263838)Peak memory usage: 201 MB
% 19.76/8.46 % (1263838)Instructions burned: 109 (million)
% 19.76/8.46 % (1263840)Instruction limit reached!
% 19.76/8.46 % (1263840)------------------------------
% 19.76/8.46 % (1263840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263840)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263840)Termination reason: Instruction limit
% 19.76/8.46 % (1263840)Termination phase: Property scanning
% 19.76/8.46 % (1263840)Time elapsed: 0.069 s
% 19.76/8.46 % (1263840)Peak memory usage: 201 MB
% 19.76/8.46 % (1263840)Instructions burned: 141 (million)
% 19.76/8.46 % (1263839)Instruction limit reached!
% 19.76/8.46 % (1263839)------------------------------
% 19.76/8.46 % (1263839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263839)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263839)Termination reason: Instruction limit
% 19.76/8.46 % (1263839)Termination phase: SInE selection
% 19.76/8.46 % (1263839)Time elapsed: 0.095 s
% 19.76/8.46 % (1263839)Peak memory usage: 201 MB
% 19.76/8.46 % (1263839)Instructions burned: 119 (million)
% 19.76/8.46 % (1263841)Instruction limit reached!
% 19.76/8.46 % (1263841)------------------------------
% 19.76/8.46 % (1263841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263841)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263841)Termination reason: Instruction limit
% 19.76/8.46 % (1263841)Termination phase: SInE selection
% 19.76/8.46 % (1263841)Time elapsed: 0.103 s
% 19.76/8.46 % (1263841)Peak memory usage: 201 MB
% 19.76/8.46 % (1263841)Instructions burned: 130 (million)
% 19.76/8.46 % (1263849)lrs+10_1_sil=8000:sp=occurrence:random_seed=1692109694:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 19.76/8.46 % (1263850)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1258895658:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 19.76/8.46 % (1263851)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2926690323:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 19.76/8.46 % (1263852)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=1797656635:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 19.76/8.46 % (1263850)Instruction limit reached!
% 19.76/8.46 % (1263850)------------------------------
% 19.76/8.46 % (1263850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263850)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263850)Termination reason: Instruction limit
% 19.76/8.46 % (1263850)Termination phase: Property scanning
% 19.76/8.46 % (1263850)Time elapsed: 0.074 s
% 19.76/8.46 % (1263850)Peak memory usage: 201 MB
% 19.76/8.46 % (1263850)Instructions burned: 157 (million)
% 19.76/8.46 % (1263852)Instruction limit reached!
% 19.76/8.46 % (1263852)------------------------------
% 19.76/8.46 % (1263852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263852)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263852)Termination reason: Instruction limit
% 19.76/8.46 % (1263852)Termination phase: Property scanning
% 19.76/8.46 % (1263852)Time elapsed: 0.113 s
% 19.76/8.46 % (1263852)Peak memory usage: 201 MB
% 19.76/8.46 % (1263852)Instructions burned: 250 (million)
% 19.76/8.46 % (1263849)Instruction limit reached!
% 19.76/8.46 % (1263849)------------------------------
% 19.76/8.46 % (1263849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263849)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263849)Termination reason: Instruction limit
% 19.76/8.46 % (1263849)Termination phase: SInE selection
% 19.76/8.46 % (1263849)Time elapsed: 0.221 s
% 19.76/8.46 % (1263849)Peak memory usage: 201 MB
% 19.76/8.46 % (1263849)Instructions burned: 286 (million)
% 19.76/8.46 % (1263857)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2257179743:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 19.76/8.46 % (1263851)Instruction limit reached!
% 19.76/8.46 % (1263851)------------------------------
% 19.76/8.46 % (1263851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263851)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263851)Termination reason: Instruction limit
% 19.76/8.46 % (1263851)Termination phase: SInE selection
% 19.76/8.46 % (1263851)Time elapsed: 0.240 s
% 19.76/8.46 % (1263851)Peak memory usage: 201 MB
% 19.76/8.46 % (1263851)Instructions burned: 326 (million)
% 19.76/8.46 % (1263859)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1800257010:i=2350_2938 on theBenchmark for (2938ds/2350Mi)
% 19.76/8.46 % (1263860)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=151045188:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 19.76/8.46 % (1263862)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=737056805:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 19.76/8.46 % (1263857)Instruction limit reached!
% 19.76/8.46 % (1263857)------------------------------
% 19.76/8.46 % (1263857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263857)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263857)Termination reason: Instruction limit
% 19.76/8.46 % (1263857)Termination phase: SInE selection
% 19.76/8.46 % (1263857)Time elapsed: 0.218 s
% 19.76/8.46 % (1263857)Peak memory usage: 201 MB
% 19.76/8.46 % (1263857)Instructions burned: 296 (million)
% 19.76/8.46 % (1263860)Instruction limit reached!
% 19.76/8.46 % (1263860)------------------------------
% 19.76/8.46 % (1263860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263860)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263860)Termination reason: Instruction limit
% 19.76/8.46 % (1263860)Termination phase: SInE selection
% 19.76/8.46 % (1263860)Time elapsed: 0.087 s
% 19.76/8.46 % (1263860)Peak memory usage: 201 MB
% 19.76/8.46 % (1263860)Instructions burned: 114 (million)
% 19.76/8.46 % (1263862)Instruction limit reached!
% 19.76/8.46 % (1263862)------------------------------
% 19.76/8.46 % (1263862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263862)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263862)Termination reason: Instruction limit
% 19.76/8.46 % (1263862)Termination phase: Preprocessing 1
% 19.76/8.46 % (1263862)Time elapsed: 0.099 s
% 19.76/8.46 % (1263862)Peak memory usage: 202 MB
% 19.76/8.46 % (1263862)Instructions burned: 127 (million)
% 19.76/8.46 % (1263866)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4008476834:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 19.76/8.46 % (1263867)lrs+10_1_sil=8000:sp=occurrence:random_seed=1602598443:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 19.76/8.46 % (1263866)Instruction limit reached!
% 19.76/8.46 % (1263866)------------------------------
% 19.76/8.46 % (1263866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263866)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263866)Termination reason: Instruction limit
% 19.76/8.46 % (1263866)Termination phase: Property scanning
% 19.76/8.46 % (1263866)Time elapsed: 0.057 s
% 19.76/8.46 % (1263866)Peak memory usage: 201 MB
% 19.76/8.46 % (1263866)Instructions burned: 116 (million)
% 19.76/8.46 % (1263868)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2497623326:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 19.76/8.46 % (1263871)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2643585178:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 19.76/8.46 % (1263868)Instruction limit reached!
% 19.76/8.46 % (1263868)------------------------------
% 19.76/8.46 % (1263868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263868)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263868)Termination reason: Instruction limit
% 19.76/8.46 % (1263868)Termination phase: SInE selection
% 19.76/8.46 % (1263868)Time elapsed: 0.326 s
% 19.76/8.46 % (1263868)Peak memory usage: 202 MB
% 19.76/8.46 % (1263868)Instructions burned: 437 (million)
% 19.76/8.46 % (1263874)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1501479761:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2929 on theBenchmark for (2929ds/134Mi)
% 19.76/8.46 % (1263867)Instruction limit reached!
% 19.76/8.46 % (1263867)------------------------------
% 19.76/8.46 % (1263867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263867)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263867)Termination reason: Instruction limit
% 19.76/8.46 % (1263867)Termination phase: Preprocessing 1
% 19.76/8.46 % (1263867)Time elapsed: 0.644 s
% 19.76/8.46 % (1263867)Peak memory usage: 204 MB
% 19.76/8.46 % (1263867)Instructions burned: 907 (million)
% 19.76/8.46 % (1263874)Instruction limit reached!
% 19.76/8.46 % (1263874)------------------------------
% 19.76/8.46 % (1263874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.76/8.46 % (1263874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.76/8.46 % (1263874)CaDiCaL version: 2.1.3
% 19.76/8.46 % (1263874)Termination reason: Instruction limit
% 19.76/8.46 % (1263874)Termination phase: SInE selection
% 19.76/8.46 % (1263874)Time elapsed: 0.106 s
% 19.76/8.46 % (1263874)Peak memory usage: 201 MB
% 19.76/8.46 % (1263874)Instructions burned: 135 (million)
% 19.76/8.46 % (1263837)First to succeed.
% 19.76/8.46 % (1263837)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1263830"
% 19.76/8.46 % (1263876)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1120049456:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 19.76/8.46 % (1263877)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3116474338:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 19.76/8.46 % (1263837)Refutation found. Thanks to Tanya!
% 19.76/8.46 % SZS status Theorem for theBenchmark
% 19.76/8.46 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/8.71 % (1263837)------------------------------
% 0.17/8.71 % (1263837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/8.71 % (1263837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/8.71 % (1263837)CaDiCaL version: 2.1.3
% 0.17/8.71 % (1263837)Termination reason: Refutation
% 0.17/8.71 % (1263837)Time elapsed: 1.712 s
% 0.17/8.71 % (1263837)Peak memory usage: 292 MB
% 0.17/8.71 % (1263837)Instructions burned: 4381 (million)
% 0.17/8.71 % (1263837)------------------------------
% 0.17/8.71 % (1263837)------------------------------
% 0.17/8.71 % (1263830)Success in time 7.608 s
% 0.17/8.71 % Vampire exiting
%------------------------------------------------------------------------------