%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP631+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 10:18:18 AM UTC 2026
% Result : Theorem 31.07s 5.01s
% Output : Refutation 31.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 21
% Syntax : Number of formulae : 159 ( 60 unt; 6 def)
% Number of atoms : 482 ( 89 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 549 ( 226 ~; 233 |; 73 &)
% ( 1 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-6 aty)
% Number of variables : 176 ( 172 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),k6_autgroup(X0,X1)) = k6_autgroup(X0,X1)
& k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),k6_autgroup(X0,k2_group_1(X0))) = k6_autgroup(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_autgroup) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),k6_autgroup(X0,X1)) = k6_autgroup(X0,X1)
& k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),k6_autgroup(X0,k2_group_1(X0))) = k6_autgroup(X0,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f7,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> ( ( v1_funct_1(X2)
& v1_partfun1(X2,X0,X1) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_funct_2) ).
fof(f22,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f24,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_autgroup) ).
fof(f25,axiom,
! [X0] :
( v1_partfun1(k6_partfun1(X0),X0,X0)
& m2_relset_1(k6_partfun1(X0),X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_partfun1) ).
fof(f29,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f34,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
=> ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
fof(f47,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f50,axiom,
! [X0] :
( v1_relat_1(k6_relat_1(X0))
& v1_funct_1(k6_relat_1(X0))
& v1_relat_2(k6_relat_1(X0))
& v3_relat_2(k6_relat_1(X0))
& v4_relat_2(k6_relat_1(X0))
& v8_relat_2(k6_relat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_partfun1) ).
fof(f68,axiom,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f69,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f70,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( m1_relset_1(X4,X0,X1)
& m1_relset_1(X5,X2,X3) )
=> k7_relset_1(X0,X1,X2,X3,X4,X5) = k5_relat_1(X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_relset_1) ).
fof(f72,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(f75,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( k7_relset_1(X0,X0,X0,X1,k6_partfun1(X0),X2) = X2
& k7_relset_1(X0,X1,X1,X1,X2,k6_partfun1(X1)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_funct_2) ).
fof(f76,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_autgroup) ).
fof(f87,plain,
! [X0] :
( v1_relat_1(k6_relat_1(X0))
& v1_funct_1(k6_relat_1(X0))
& v1_relat_2(k6_relat_1(X0))
& v3_relat_2(k6_relat_1(X0))
& v8_relat_2(k6_relat_1(X0)) ),
inference(pure_predicate_removal,[],[f50]) ).
fof(f90,plain,
? [X0] :
( ? [X1] :
( ( k6_autgroup(X0,X1) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),k6_autgroup(X0,X1))
| k6_autgroup(X0,X1) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),k6_autgroup(X0,k2_group_1(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f91,plain,
? [X0] :
( ? [X1] :
( ( k6_autgroup(X0,X1) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),k6_autgroup(X0,X1))
| k6_autgroup(X0,X1) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),k6_autgroup(X0,k2_group_1(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f90]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f97]) ).
fof(f120,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f121,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f120]) ).
fof(f124,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f24]) ).
fof(f125,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f124]) ).
fof(f130,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f133,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f132]) ).
fof(f142,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f47]) ).
fof(f143,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f142]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4,X5] :
( k7_relset_1(X0,X1,X2,X3,X4,X5) = k5_relat_1(X4,X5)
| ~ m1_relset_1(X4,X0,X1)
| ~ m1_relset_1(X5,X2,X3) ),
inference(ennf_transformation,[],[f70]) ).
fof(f151,plain,
! [X0,X1,X2,X3,X4,X5] :
( k7_relset_1(X0,X1,X2,X3,X4,X5) = k5_relat_1(X4,X5)
| ~ m1_relset_1(X4,X0,X1)
| ~ m1_relset_1(X5,X2,X3) ),
inference(flattening,[],[f150]) ).
fof(f155,plain,
! [X0,X1,X2] :
( ( k7_relset_1(X0,X0,X0,X1,k6_partfun1(X0),X2) = X2
& k7_relset_1(X0,X1,X1,X1,X2,k6_partfun1(X1)) = X2 )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f75]) ).
fof(f156,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f76]) ).
fof(f157,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f156]) ).
fof(f167,plain,
( ( k6_autgroup(sK0,sK1) != k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),k6_autgroup(sK0,k2_group_1(sK0)),k6_autgroup(sK0,sK1))
| k6_autgroup(sK0,sK1) != k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),k6_autgroup(sK0,sK1),k6_autgroup(sK0,k2_group_1(sK0))) )
& m1_subset_1(sK1,u1_struct_0(sK0))
& ~ v3_struct_0(sK0)
& v1_group_1(sK0)
& v3_group_1(sK0)
& v4_group_1(sK0)
& l1_group_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f91]) ).
fof(f192,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,[],[f72]) ).
fof(f193,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f167]) ).
fof(f194,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f167]) ).
fof(f195,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f167]) ).
fof(f196,plain,
v1_group_1(sK0),
inference(cnf_transformation,[],[f167]) ).
fof(f197,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f167]) ).
fof(f198,plain,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f167]) ).
fof(f199,plain,
( k6_autgroup(sK0,sK1) != k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),k6_autgroup(sK0,k2_group_1(sK0)),k6_autgroup(sK0,sK1))
| k6_autgroup(sK0,sK1) != k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),k6_autgroup(sK0,sK1),k6_autgroup(sK0,k2_group_1(sK0))) ),
inference(cnf_transformation,[],[f167]) ).
fof(f205,plain,
! [X2,X0,X1] :
( ~ v1_partfun1(X2,X0,X1)
| ~ v1_funct_1(X2)
| v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f236,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f238,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f239,plain,
! [X0] : m2_relset_1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[],[f25]) ).
fof(f240,plain,
! [X0] : v1_partfun1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[],[f25]) ).
fof(f246,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f249,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| m2_relset_1(X3,X0,X1)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f250,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_funct_2(X3,X0,X1)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f251,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f267,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f274,plain,
! [X0] : v1_funct_1(k6_relat_1(X0)),
inference(cnf_transformation,[],[f87]) ).
fof(f328,plain,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
inference(cnf_transformation,[],[f68]) ).
fof(f329,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,X1,X2)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f149]) ).
fof(f330,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X5,X2,X3)
| ~ m1_relset_1(X4,X0,X1)
| k7_relset_1(X0,X1,X2,X3,X4,X5) = k5_relat_1(X4,X5) ),
inference(cnf_transformation,[],[f151]) ).
fof(f333,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
fof(f337,plain,
! [X2,X0,X1] :
( k7_relset_1(X0,X1,X1,X1,X2,k6_partfun1(X1)) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f155]) ).
fof(f338,plain,
! [X2,X0,X1] :
( k7_relset_1(X0,X0,X0,X1,k6_partfun1(X0),X2) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f155]) ).
fof(f339,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f347,plain,
! [X0] : v1_partfun1(k6_relat_1(X0),X0,X0),
inference(definition_unfolding,[],[f240,f328]) ).
fof(f348,plain,
! [X0] : m2_relset_1(k6_relat_1(X0),X0,X0),
inference(definition_unfolding,[],[f239,f328]) ).
fof(f349,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| k7_relset_1(X0,X0,X0,X1,k6_relat_1(X0),X2) = X2 ),
inference(definition_unfolding,[],[f338,f328]) ).
fof(f350,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| k7_relset_1(X0,X1,X1,X1,X2,k6_relat_1(X1)) = X2 ),
inference(definition_unfolding,[],[f337,f328]) ).
fof(f351,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k6_autgroup(X0,k2_group_1(X0)) = k6_relat_1(u1_struct_0(X0)) ),
inference(definition_unfolding,[],[f339,f328]) ).
fof(f352,definition,
sF25 = k6_autgroup(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f353,plain,
k6_autgroup(sK0,sK1) = sF25,
inference(reorient_equations,[],[f352]) ).
fof(f354,definition,
sF26 = u1_struct_0(sK0),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f355,plain,
u1_struct_0(sK0) = sF26,
inference(reorient_equations,[],[f354]) ).
fof(f356,definition,
sF27 = k2_group_1(sK0),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f357,plain,
k2_group_1(sK0) = sF27,
inference(reorient_equations,[],[f356]) ).
fof(f358,definition,
sF28 = k6_autgroup(sK0,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f359,plain,
k6_autgroup(sK0,sF27) = sF28,
inference(reorient_equations,[],[f358]) ).
fof(f360,definition,
sF29 = k7_funct_2(sF26,sF26,sF26,sF28,sF25),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f361,plain,
k7_funct_2(sF26,sF26,sF26,sF28,sF25) = sF29,
inference(reorient_equations,[],[f360]) ).
fof(f362,definition,
sF30 = k7_funct_2(sF26,sF26,sF26,sF25,sF28),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f363,plain,
k7_funct_2(sF26,sF26,sF26,sF25,sF28) = sF30,
inference(reorient_equations,[],[f362]) ).
fof(f364,plain,
( sF25 != sF30
| sF25 != sF29 ),
inference(definition_folding,[],[f199,f363,f359,f357,f353,f355,f355,f355,f353,f361,f353,f359,f357,f355,f355,f355,f353]) ).
fof(f365,plain,
m1_subset_1(sK1,sF26),
inference(definition_folding,[],[f198,f355]) ).
fof(f370,plain,
l1_struct_0(sK0),
inference(resolution,[],[f246,f193]) ).
fof(f397,plain,
( ~ v1_xboole_0(sF26)
| v3_struct_0(sK0)
| ~ l1_struct_0(sK0) ),
inference(superposition,[],[f267,f355]) ).
fof(f398,plain,
( ~ v1_xboole_0(sF26)
| ~ l1_struct_0(sK0) ),
inference(forward_subsumption_resolution,[],[f397,f197]) ).
fof(f399,plain,
~ v1_xboole_0(sF26),
inference(forward_subsumption_resolution,[],[f398,f370]) ).
fof(f439,plain,
! [X0] : m1_relset_1(k6_relat_1(X0),X0,X0),
inference(resolution,[],[f333,f348]) ).
fof(f513,plain,
! [X0] :
( ~ v1_funct_1(k6_relat_1(X0))
| v1_funct_2(k6_relat_1(X0),X0,X0)
| ~ m1_relset_1(k6_relat_1(X0),X0,X0) ),
inference(resolution,[],[f205,f347]) ).
fof(f514,plain,
! [X0] :
( v1_funct_2(k6_relat_1(X0),X0,X0)
| ~ m1_relset_1(k6_relat_1(X0),X0,X0) ),
inference(forward_subsumption_resolution,[],[f513,f274]) ).
fof(f516,plain,
! [X0] : v1_funct_2(k6_relat_1(X0),X0,X0),
inference(forward_subsumption_resolution,[],[f514,f439]) ).
fof(f596,plain,
( m1_fraenkel(k4_autgroup(sK0),sF26,sF26)
| v3_struct_0(sK0)
| ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f236,f355]) ).
fof(f597,plain,
( m1_fraenkel(k4_autgroup(sK0),sF26,sF26)
| ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f596,f197]) ).
fof(f598,plain,
( m1_fraenkel(k4_autgroup(sK0),sF26,sF26)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f597,f196]) ).
fof(f599,plain,
( m1_fraenkel(k4_autgroup(sK0),sF26,sF26)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f598,f195]) ).
fof(f600,plain,
( m1_fraenkel(k4_autgroup(sK0),sF26,sF26)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f599,f194]) ).
fof(f601,plain,
m1_fraenkel(k4_autgroup(sK0),sF26,sF26),
inference(forward_subsumption_resolution,[],[f600,f193]) ).
fof(f644,plain,
( v3_struct_0(sK0)
| ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(u1_struct_0(sK0)) ),
inference(resolution,[],[f351,f193]) ).
fof(f652,plain,
( ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f644,f197]) ).
fof(f655,plain,
( ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f652,f196]) ).
fof(f657,plain,
( ~ v4_group_1(sK0)
| k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f655,f195]) ).
fof(f659,plain,
k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(u1_struct_0(sK0)),
inference(forward_subsumption_resolution,[],[f657,f194]) ).
fof(f660,plain,
k6_autgroup(sK0,k2_group_1(sK0)) = k6_relat_1(sF26),
inference(forward_demodulation,[],[f659,f355]) ).
fof(f661,plain,
k6_autgroup(sK0,sF27) = k6_relat_1(sF26),
inference(forward_demodulation,[],[f660,f357]) ).
fof(f662,plain,
sF28 = k6_relat_1(sF26),
inference(forward_demodulation,[],[f661,f359]) ).
fof(f667,plain,
v1_funct_1(sF28),
inference(superposition,[],[f274,f662]) ).
fof(f671,plain,
m1_relset_1(sF28,sF26,sF26),
inference(superposition,[],[f439,f662]) ).
fof(f672,plain,
v1_funct_2(sF28,sF26,sF26),
inference(superposition,[],[f516,f662]) ).
fof(f722,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| v3_struct_0(sK0)
| ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(superposition,[],[f238,f353]) ).
fof(f727,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f722,f197]) ).
fof(f734,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v3_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f727,f196]) ).
fof(f737,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f734,f195]) ).
fof(f740,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f737,f194]) ).
fof(f743,plain,
( m2_fraenkel(sF25,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f740,f193]) ).
fof(f745,plain,
( m2_fraenkel(sF25,sF26,sF26,k4_autgroup(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f743,f355]) ).
fof(f747,plain,
( ~ m1_subset_1(sK1,sF26)
| m2_fraenkel(sF25,sF26,sF26,k4_autgroup(sK0)) ),
inference(forward_demodulation,[],[f745,f355]) ).
fof(f749,plain,
m2_fraenkel(sF25,sF26,sF26,k4_autgroup(sK0)),
inference(forward_subsumption_resolution,[],[f747,f365]) ).
fof(f760,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,X1,X2)
| k7_relset_1(X1,X2,sF26,sF26,X0,sF28) = k5_relat_1(X0,sF28) ),
inference(resolution,[],[f671,f330]) ).
fof(f856,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X2,X0)
| ~ m1_relset_1(X1,X2,X0)
| ~ v1_funct_1(k6_relat_1(X0))
| k7_funct_2(X2,X0,X0,X1,k6_relat_1(X0)) = k5_relat_1(X1,k6_relat_1(X0))
| ~ m1_relset_1(k6_relat_1(X0),X0,X0) ),
inference(resolution,[],[f329,f516]) ).
fof(f867,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X2,X0)
| ~ m1_relset_1(X1,X2,X0)
| k7_funct_2(X2,X0,X0,X1,k6_relat_1(X0)) = k5_relat_1(X1,k6_relat_1(X0))
| ~ m1_relset_1(k6_relat_1(X0),X0,X0) ),
inference(forward_subsumption_resolution,[],[f856,f274]) ).
fof(f873,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,X2,X0)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0)
| ~ m1_relset_1(X1,X2,X0)
| k7_funct_2(X2,X0,X0,X1,k6_relat_1(X0)) = k5_relat_1(X1,k6_relat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f867,f439]) ).
fof(f887,plain,
( v1_funct_2(sF25,sF26,sF26)
| v1_xboole_0(sF26)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(resolution,[],[f749,f250]) ).
fof(f888,plain,
( m2_relset_1(sF25,sF26,sF26)
| v1_xboole_0(sF26)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(resolution,[],[f749,f249]) ).
fof(f890,plain,
( v1_funct_1(sF25)
| v1_xboole_0(sF26)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(resolution,[],[f749,f251]) ).
fof(f891,plain,
( v1_funct_1(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(forward_subsumption_resolution,[],[f890,f399]) ).
fof(f893,plain,
( m2_relset_1(sF25,sF26,sF26)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(forward_subsumption_resolution,[],[f888,f399]) ).
fof(f894,plain,
( v1_funct_2(sF25,sF26,sF26)
| ~ m1_fraenkel(k4_autgroup(sK0),sF26,sF26) ),
inference(forward_subsumption_resolution,[],[f887,f399]) ).
fof(f895,plain,
v1_funct_1(sF25),
inference(forward_subsumption_resolution,[],[f891,f601]) ).
fof(f897,plain,
m2_relset_1(sF25,sF26,sF26),
inference(forward_subsumption_resolution,[],[f893,f601]) ).
fof(f898,plain,
v1_funct_2(sF25,sF26,sF26),
inference(forward_subsumption_resolution,[],[f894,f601]) ).
fof(f918,plain,
sF25 = k7_relset_1(sF26,sF26,sF26,sF26,sF25,k6_relat_1(sF26)),
inference(resolution,[],[f897,f350]) ).
fof(f919,plain,
sF25 = k7_relset_1(sF26,sF26,sF26,sF26,k6_relat_1(sF26),sF25),
inference(resolution,[],[f897,f349]) ).
fof(f920,plain,
m1_relset_1(sF25,sF26,sF26),
inference(resolution,[],[f897,f333]) ).
fof(f921,plain,
sF25 = k7_relset_1(sF26,sF26,sF26,sF26,sF28,sF25),
inference(forward_demodulation,[],[f919,f662]) ).
fof(f922,plain,
sF25 = k7_relset_1(sF26,sF26,sF26,sF26,sF25,sF28),
inference(forward_demodulation,[],[f918,f662]) ).
fof(f926,plain,
! [X0,X1] :
( v1_xboole_0(sF26)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,sF26)
| ~ m1_relset_1(X0,X1,sF26)
| ~ v1_funct_1(sF25)
| k7_funct_2(X1,sF26,sF26,X0,sF25) = k5_relat_1(X0,sF25)
| ~ m1_relset_1(sF25,sF26,sF26) ),
inference(resolution,[],[f898,f329]) ).
fof(f941,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,sF26)
| ~ m1_relset_1(X0,X1,sF26)
| ~ v1_funct_1(sF25)
| k7_funct_2(X1,sF26,sF26,X0,sF25) = k5_relat_1(X0,sF25)
| ~ m1_relset_1(sF25,sF26,sF26) ),
inference(forward_subsumption_resolution,[],[f926,f399]) ).
fof(f951,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,sF26)
| ~ m1_relset_1(X0,X1,sF26)
| k7_funct_2(X1,sF26,sF26,X0,sF25) = k5_relat_1(X0,sF25)
| ~ m1_relset_1(sF25,sF26,sF26) ),
inference(forward_subsumption_resolution,[],[f941,f895]) ).
fof(f958,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,X1,sF26)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,sF26)
| k7_funct_2(X1,sF26,sF26,X0,sF25) = k5_relat_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f951,f920]) ).
fof(f980,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,X1,X2)
| k5_relat_1(X0,sF25) = k7_relset_1(X1,X2,sF26,sF26,X0,sF25) ),
inference(resolution,[],[f920,f330]) ).
fof(f4680,plain,
( ~ v1_funct_1(sF25)
| v1_xboole_0(sF26)
| ~ m1_relset_1(sF25,sF26,sF26)
| k7_funct_2(sF26,sF26,sF26,sF25,k6_relat_1(sF26)) = k5_relat_1(sF25,k6_relat_1(sF26)) ),
inference(resolution,[],[f873,f898]) ).
fof(f4691,plain,
( v1_xboole_0(sF26)
| ~ m1_relset_1(sF25,sF26,sF26)
| k7_funct_2(sF26,sF26,sF26,sF25,k6_relat_1(sF26)) = k5_relat_1(sF25,k6_relat_1(sF26)) ),
inference(forward_subsumption_resolution,[],[f4680,f895]) ).
fof(f4711,plain,
( ~ m1_relset_1(sF25,sF26,sF26)
| k7_funct_2(sF26,sF26,sF26,sF25,k6_relat_1(sF26)) = k5_relat_1(sF25,k6_relat_1(sF26)) ),
inference(forward_subsumption_resolution,[],[f4691,f399]) ).
fof(f4730,plain,
k7_funct_2(sF26,sF26,sF26,sF25,k6_relat_1(sF26)) = k5_relat_1(sF25,k6_relat_1(sF26)),
inference(forward_subsumption_resolution,[],[f4711,f920]) ).
fof(f4741,plain,
k7_funct_2(sF26,sF26,sF26,sF25,sF28) = k5_relat_1(sF25,sF28),
inference(forward_demodulation,[],[f4730,f662]) ).
fof(f4748,plain,
sF30 = k5_relat_1(sF25,sF28),
inference(forward_demodulation,[],[f4741,f363]) ).
fof(f11278,plain,
k7_relset_1(sF26,sF26,sF26,sF26,sF25,sF28) = k5_relat_1(sF25,sF28),
inference(resolution,[],[f760,f920]) ).
fof(f11290,plain,
sF30 = k7_relset_1(sF26,sF26,sF26,sF26,sF25,sF28),
inference(forward_demodulation,[],[f11278,f4748]) ).
fof(f11299,plain,
sF25 = sF30,
inference(forward_demodulation,[],[f11290,f922]) ).
fof(f11303,plain,
( sF25 != sF25
| sF25 != sF29 ),
inference(superposition,[],[f364,f11299]) ).
fof(f11356,plain,
sF25 != sF29,
inference(trivial_inequality_removal,[],[f11303]) ).
fof(f13352,plain,
( ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF28,sF26,sF26)
| k7_funct_2(sF26,sF26,sF26,sF28,sF25) = k5_relat_1(sF28,sF25) ),
inference(resolution,[],[f958,f672]) ).
fof(f13360,plain,
( ~ m1_relset_1(sF28,sF26,sF26)
| k7_funct_2(sF26,sF26,sF26,sF28,sF25) = k5_relat_1(sF28,sF25) ),
inference(forward_subsumption_resolution,[],[f13352,f667]) ).
fof(f13385,plain,
k7_funct_2(sF26,sF26,sF26,sF28,sF25) = k5_relat_1(sF28,sF25),
inference(forward_subsumption_resolution,[],[f13360,f671]) ).
fof(f13406,plain,
sF29 = k5_relat_1(sF28,sF25),
inference(forward_demodulation,[],[f13385,f361]) ).
fof(f59594,plain,
k7_relset_1(sF26,sF26,sF26,sF26,sF28,sF25) = k5_relat_1(sF28,sF25),
inference(resolution,[],[f980,f671]) ).
fof(f59613,plain,
sF29 = k7_relset_1(sF26,sF26,sF26,sF26,sF28,sF25),
inference(forward_demodulation,[],[f59594,f13406]) ).
fof(f59619,plain,
sF25 = sF29,
inference(forward_demodulation,[],[f59613,f921]) ).
fof(f59622,plain,
$false,
inference(forward_subsumption_resolution,[],[f59619,f11356]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP631+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 10:15:30 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.43/1.81 % (2181842)Will run a generic schedule for satisfiability detection.
% 8.43/1.81 % (2181851)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=761901552:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.43/1.81 % (2181848)% WARNING: option uhcvi not known.
% 8.43/1.81 % (2181848)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2813970887:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.43/1.81 % (2181849)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=755813579:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.43/1.81 % (2181850)dis+10_1_sil=32000:sp=arity:random_seed=3139968447:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.43/1.81 % (2181847)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=574768062_2999 on theBenchmark for (2999ds/0Mi)
% 8.43/1.81 % (2181852)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4203365162:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.43/1.81 % TRYING [1]
% 8.43/1.81 % (2181853)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2112572663:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.43/1.81 % TRYING [2]
% 8.43/1.81 % TRYING [3]
% 8.43/1.81 % (2181851)Instruction limit reached!
% 8.43/1.81 % (2181851)------------------------------
% 8.43/1.81 % (2181851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.81 % (2181851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.81 % (2181851)CaDiCaL version: 2.1.3
% 8.43/1.81 % (2181851)Termination reason: Instruction limit
% 8.43/1.81 % (2181851)Termination phase: Saturation
% 8.43/1.81 % (2181851)Time elapsed: 0.039 s
% 8.43/1.81 % (2181851)Peak memory usage: 13 MB
% 8.43/1.81 % (2181851)Instructions burned: 116 (million)
% 8.43/1.81 % TRYING [4]
% 8.43/1.81 % (2181861)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1051640504:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.43/1.81 % TRYING [1]
% 8.43/1.81 % TRYING [2]
% 8.43/1.81 % TRYING [3]
% 8.43/1.81 % TRYING [4]
% 8.43/1.81 % (2181850)Instruction limit reached!
% 8.43/1.81 % (2181850)------------------------------
% 8.43/1.81 % (2181850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.81 % (2181850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.81 % (2181850)CaDiCaL version: 2.1.3
% 8.43/1.81 % (2181850)Termination reason: Instruction limit
% 8.43/1.81 % (2181850)Termination phase: Saturation
% 8.43/1.81 % (2181850)Time elapsed: 0.072 s
% 8.43/1.81 % (2181850)Peak memory usage: 13 MB
% 8.43/1.81 % (2181850)Instructions burned: 104 (million)
% 8.43/1.81 % (2181852)Instruction limit reached!
% 8.43/1.81 % (2181852)------------------------------
% 8.43/1.81 % (2181852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.81 % (2181852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.81 % (2181852)CaDiCaL version: 2.1.3
% 8.43/1.81 % (2181852)Termination reason: Instruction limit
% 8.43/1.81 % (2181852)Termination phase: Saturation
% 8.43/1.81 % (2181852)Time elapsed: 0.078 s
% 8.43/1.81 % (2181852)Peak memory usage: 13 MB
% 8.43/1.81 % (2181852)Instructions burned: 131 (million)
% 8.43/1.81 % (2181863)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2540865370:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.43/1.81 % (2181864)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1679997047:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.43/1.81 % (2181853)Instruction limit reached!
% 8.43/1.81 % (2181853)------------------------------
% 8.43/1.81 % (2181853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.81 % (2181853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.81 % (2181853)CaDiCaL version: 2.1.3
% 8.43/1.81 % (2181853)Termination reason: Instruction limit
% 8.43/1.81 % (2181853)Termination phase: Saturation
% 8.43/1.81 % (2181853)Time elapsed: 0.137 s
% 8.43/1.81 % (2181853)Peak memory usage: 13 MB
% 8.43/1.81 % (2181853)Instructions burned: 159 (million)
% 8.43/1.81 % (2181867)ott-21_1_sil=16000:fs=off:random_seed=2476995553:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.43/1.81 % (2181863)Instruction limit reached!
% 8.43/1.81 % (2181863)------------------------------
% 8.43/1.81 % (2181863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.81 % (2181863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181863)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181863)Termination reason: Instruction limit
% 31.07/5.01 % (2181863)Termination phase: Saturation
% 31.07/5.01 % (2181863)Time elapsed: 0.078 s
% 31.07/5.01 % (2181863)Peak memory usage: 13 MB
% 31.07/5.01 % (2181863)Instructions burned: 131 (million)
% 31.07/5.01 % (2181869)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=26655738:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 31.07/5.01 % TRYING [5]
% 31.07/5.01 % (2181861)Instruction limit reached!
% 31.07/5.01 % (2181861)------------------------------
% 31.07/5.01 % (2181861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181861)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181861)Termination reason: Instruction limit
% 31.07/5.01 % (2181861)Termination phase: Finite model building SAT solving
% 31.07/5.01 % (2181861)Time elapsed: 0.172 s
% 31.07/5.01 % (2181861)Peak memory usage: 40 MB
% 31.07/5.01 % (2181861)Instructions burned: 717 (million)
% 31.07/5.01 % (2181871)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=514148530:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 31.07/5.01 % TRYING [1]
% 31.07/5.01 % TRYING [2]
% 31.07/5.01 % TRYING [3]
% 31.07/5.01 % (2181867)Instruction limit reached!
% 31.07/5.01 % (2181867)------------------------------
% 31.07/5.01 % (2181867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181867)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181867)Termination reason: Instruction limit
% 31.07/5.01 % (2181867)Termination phase: Saturation
% 31.07/5.01 % (2181867)Time elapsed: 0.105 s
% 31.07/5.01 % (2181867)Peak memory usage: 13 MB
% 31.07/5.01 % (2181867)Instructions burned: 180 (million)
% 31.07/5.01 % TRYING [4]
% 31.07/5.01 % (2181873)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1749163635:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 31.07/5.01 % (2181871)Instruction limit reached!
% 31.07/5.01 % (2181871)------------------------------
% 31.07/5.01 % (2181871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181871)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181871)Termination reason: Instruction limit
% 31.07/5.01 % (2181871)Termination phase: Finite model building SAT solving
% 31.07/5.01 % (2181871)Time elapsed: 0.204 s
% 31.07/5.01 % (2181871)Peak memory usage: 33 MB
% 31.07/5.01 % (2181871)Instructions burned: 870 (million)
% 31.07/5.01 % (2181875)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=189341923:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 31.07/5.01 % (2181869)Instruction limit reached!
% 31.07/5.01 % (2181869)------------------------------
% 31.07/5.01 % (2181869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181869)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181869)Termination reason: Instruction limit
% 31.07/5.01 % (2181869)Termination phase: Saturation
% 31.07/5.01 % (2181869)Time elapsed: 0.333 s
% 31.07/5.01 % (2181869)Peak memory usage: 14 MB
% 31.07/5.01 % (2181869)Instructions burned: 478 (million)
% 31.07/5.01 % (2181864)Instruction limit reached!
% 31.07/5.01 % (2181864)------------------------------
% 31.07/5.01 % (2181864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181864)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181864)Termination reason: Instruction limit
% 31.07/5.01 % (2181864)Termination phase: Saturation
% 31.07/5.01 % (2181864)Time elapsed: 0.442 s
% 31.07/5.01 % (2181864)Peak memory usage: 18 MB
% 31.07/5.01 % (2181864)Instructions burned: 684 (million)
% 31.07/5.01 % (2181877)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2288942048:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 31.07/5.01 % (2181878)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2261922436:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 31.07/5.01 % (2181875)Instruction limit reached!
% 31.07/5.01 % (2181875)------------------------------
% 31.07/5.01 % (2181875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181875)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181875)Termination reason: Instruction limit
% 31.07/5.01 % (2181875)Termination phase: Finite model building constraint generation
% 31.07/5.01 % (2181875)Time elapsed: 0.239 s
% 31.07/5.01 % (2181875)Peak memory usage: 106 MB
% 31.07/5.01 % (2181875)Instructions burned: 893 (million)
% 31.07/5.01 % (2181881)fmb+10_1_sil=64000:random_seed=1325600338:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 31.07/5.01 % TRYING [1]
% 31.07/5.01 % TRYING [2]
% 31.07/5.01 % TRYING [3]
% 31.07/5.01 % TRYING [4]
% 31.07/5.01 % (2181877)Instruction limit reached!
% 31.07/5.01 % (2181877)------------------------------
% 31.07/5.01 % (2181877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181877)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181877)Termination reason: Instruction limit
% 31.07/5.01 % (2181877)Termination phase: Saturation
% 31.07/5.01 % (2181877)Time elapsed: 0.421 s
% 31.07/5.01 % (2181877)Peak memory usage: 24 MB
% 31.07/5.01 % (2181877)Instructions burned: 692 (million)
% 31.07/5.01 % (2181873)Instruction limit reached!
% 31.07/5.01 % (2181873)------------------------------
% 31.07/5.01 % (2181873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181873)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181873)Termination reason: Instruction limit
% 31.07/5.01 % (2181873)Termination phase: Saturation
% 31.07/5.01 % (2181873)Time elapsed: 0.686 s
% 31.07/5.01 % (2181873)Peak memory usage: 25 MB
% 31.07/5.01 % (2181873)Instructions burned: 1179 (million)
% 31.07/5.01 % (2181883)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3356702141:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 31.07/5.01 % (2181883)Cannot represent all propositional literals internally
% 31.07/5.01 % (2181883)Refutation not found, incomplete strategy
% 31.07/5.01 % (2181883)------------------------------
% 31.07/5.01 % (2181883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181883)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181883)Termination reason: Refutation not found, incomplete strategy
% 31.07/5.01 % (2181883)Time elapsed: 0.006 s
% 31.07/5.01 % (2181883)Peak memory usage: 10 MB
% 31.07/5.01 % (2181883)Instructions burned: 12 (million)
% 31.07/5.01 % (2181883)------------------------------
% 31.07/5.01 % (2181883)------------------------------
% 31.07/5.01 % TRYING [5]
% 31.07/5.01 % (2181884)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4111316128:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 31.07/5.01 % TRYING [8]
% 31.07/5.01 % (2181886)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=654692479:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 31.07/5.01 % (2181878)Instruction limit reached!
% 31.07/5.01 % (2181878)------------------------------
% 31.07/5.01 % (2181878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181878)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181878)Termination reason: Instruction limit
% 31.07/5.01 % (2181878)Termination phase: Saturation
% 31.07/5.01 % (2181878)Time elapsed: 0.537 s
% 31.07/5.01 % (2181878)Peak memory usage: 20 MB
% 31.07/5.01 % (2181878)Instructions burned: 879 (million)
% 31.07/5.01 % (2181889)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=839609690:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 31.07/5.01 % TRYING [6]
% 31.07/5.01 % (2181884)Instruction limit reached!
% 31.07/5.01 % (2181884)------------------------------
% 31.07/5.01 % (2181884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181884)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181884)Termination reason: Instruction limit
% 31.07/5.01 % (2181884)Termination phase: Finite model building constraint generation
% 31.07/5.01 % (2181884)Time elapsed: 0.306 s
% 31.07/5.01 % (2181884)Peak memory usage: 60 MB
% 31.07/5.01 % (2181884)Instructions burned: 921 (million)
% 31.07/5.01 % (2181891)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=851452179:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 31.07/5.01 % (2181891)Cannot represent all propositional literals internally
% 31.07/5.01 % (2181891)Refutation not found, incomplete strategy
% 31.07/5.01 % (2181891)------------------------------
% 31.07/5.01 % (2181891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181891)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181891)Termination reason: Refutation not found, incomplete strategy
% 31.07/5.01 % (2181891)Time elapsed: 0.007 s
% 31.07/5.01 % (2181891)Peak memory usage: 11 MB
% 31.07/5.01 % (2181891)Instructions burned: 12 (million)
% 31.07/5.01 % (2181891)------------------------------
% 31.07/5.01 % (2181891)------------------------------
% 31.07/5.01 % (2181893)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1165626029:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi)
% 31.07/5.01 % TRYING [16]
% 31.07/5.01 % (2181889)Instruction limit reached!
% 31.07/5.01 % (2181889)------------------------------
% 31.07/5.01 % (2181889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181889)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181889)Termination reason: Instruction limit
% 31.07/5.01 % (2181889)Termination phase: Saturation
% 31.07/5.01 % (2181889)Time elapsed: 0.742 s
% 31.07/5.01 % (2181889)Peak memory usage: 27 MB
% 31.07/5.01 % (2181889)Instructions burned: 1472 (million)
% 31.07/5.01 % (2181895)ott-2_1_sil=16000:newcnf=on:random_seed=3634237974:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 31.07/5.01 % (2181893)Instruction limit reached!
% 31.07/5.01 % (2181893)------------------------------
% 31.07/5.01 % (2181893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181893)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181893)Termination reason: Instruction limit
% 31.07/5.01 % (2181893)Termination phase: Finite model building constraint generation
% 31.07/5.01 % (2181893)Time elapsed: 0.725 s
% 31.07/5.01 % (2181893)Peak memory usage: 121 MB
% 31.07/5.01 % (2181893)Instructions burned: 2176 (million)
% 31.07/5.01 % (2181897)ott+10_1_sil=32000:tgt=ground:random_seed=156400758:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi)
% 31.07/5.01 % (2181895)Instruction limit reached!
% 31.07/5.01 % (2181895)------------------------------
% 31.07/5.01 % (2181895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181895)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181895)Termination reason: Instruction limit
% 31.07/5.01 % (2181895)Termination phase: Saturation
% 31.07/5.01 % (2181895)Time elapsed: 0.492 s
% 31.07/5.01 % (2181895)Peak memory usage: 19 MB
% 31.07/5.01 % (2181895)Instructions burned: 870 (million)
% 31.07/5.01 % (2181899)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=86117690:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 31.07/5.01 % TRYING [1]
% 31.07/5.01 % TRYING [2]
% 31.07/5.01 % TRYING [3]
% 31.07/5.01 % TRYING [6]
% 31.07/5.01 % TRYING [4]
% 31.07/5.01 % TRYING [5]
% 31.07/5.01 % TRYING [6]
% 31.07/5.01 % (2181886)Instruction limit reached!
% 31.07/5.01 % (2181886)------------------------------
% 31.07/5.01 % (2181886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181886)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181886)Termination reason: Instruction limit
% 31.07/5.01 % (2181886)Termination phase: Saturation
% 31.07/5.01 % (2181886)Time elapsed: 2.867 s
% 31.07/5.01 % (2181886)Peak memory usage: 34 MB
% 31.07/5.01 % (2181886)Instructions burned: 5131 (million)
% 31.07/5.01 % (2181901)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2106840347:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 31.07/5.01 % (2181897) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2181842-2181897"...
% 31.07/5.01 % (2181897)...printing done.
% 31.07/5.01 % (2181897)Refutation found. Thanks to Tanya!
% 31.07/5.01 % SZS status Theorem for theBenchmark
% 31.07/5.01 % SZS output start Proof for theBenchmark
% See solution above
% 31.07/5.01 % (2181897)------------------------------
% 31.07/5.01 % (2181897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.07/5.01 % (2181897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.07/5.01 % (2181897)CaDiCaL version: 2.1.3
% 31.07/5.01 % (2181897)Termination reason: Refutation
% 31.07/5.01 % (2181897)Time elapsed: 2.335 s
% 31.07/5.01 % (2181897)Peak memory usage: 47 MB
% 31.07/5.01 % (2181897)Instructions burned: 4042 (million)
% 31.07/5.01 % (2181842)Success in time 4.583 s
% 31.07/5.01 % Vampire exiting
%------------------------------------------------------------------------------