%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG226+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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:29:52 AM UTC 2026
% Result : Theorem 106.66s 28.06s
% Output : Refutation 106.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 17
% Syntax : Number of formulae : 154 ( 28 unt; 3 def)
% Number of atoms : 576 ( 154 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 700 ( 278 ~; 296 |; 85 &)
% ( 18 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 4 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 219 ( 0 sgn 201 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( v2_relat_1(X1)
& m1_pboole(X1,X0) )
=> ! [X2] :
( ( v2_relat_1(X2)
& m1_pboole(X2,X0) )
=> ( ( k1_closure3(X0,X1) = k1_closure3(X0,X2)
& k7_relat_1(X1,k1_closure3(X0,X1)) = k7_relat_1(X2,k1_closure3(X0,X2)) )
=> r6_pboole(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_closure3) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( v2_relat_1(X1)
& m1_pboole(X1,X0) )
=> ! [X2] :
( ( v2_relat_1(X2)
& m1_pboole(X2,X0) )
=> ( ( k1_closure3(X0,X1) = k1_closure3(X0,X2)
& k7_relat_1(X1,k1_closure3(X0,X1)) = k7_relat_1(X2,k1_closure3(X0,X2)) )
=> r6_pboole(X0,X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f11,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f12,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ( v2_relat_1(X1)
<=> ! [X2] :
~ ( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_pboole) ).
fof(f13,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( X2 = k1_closure3(X0,X1)
<=> X2 = a_2_0_closure3(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_closure3) ).
fof(f14,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pboole) ).
fof(f15,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f22,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ( v1_relat_1(X1)
& v1_funct_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_pboole) ).
fof(f28,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f31,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_pboole(X2,X1) )
=> ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_2_0_closure3) ).
fof(f46,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_pboole(X2,X0) )
=> ( r6_pboole(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r6_pboole) ).
fof(f49,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f54,axiom,
! [X0,X1,X2] :
( ( v1_relat_1(X2)
& v1_funct_1(X2) )
=> ( r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
=> k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_funct_1) ).
fof(f57,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> k1_relat_1(k7_relat_1(X1,X0)) = k3_xboole_0(k1_relat_1(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t90_relat_1) ).
fof(f58,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( ( k1_relat_1(X0) = k1_relat_1(X1)
& ! [X2] :
( r2_hidden(X2,k1_relat_1(X0))
=> k1_funct_1(X0,X2) = k1_funct_1(X1,X2) ) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_funct_1) ).
fof(f66,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r6_pboole(X0,X1,X2)
& k1_closure3(X0,X1) = k1_closure3(X0,X2)
& k7_relat_1(X1,k1_closure3(X0,X1)) = k7_relat_1(X2,k1_closure3(X0,X2))
& v2_relat_1(X2)
& m1_pboole(X2,X0) )
& v2_relat_1(X1)
& m1_pboole(X1,X0) )
& ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f67,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r6_pboole(X0,X1,X2)
& k1_closure3(X0,X1) = k1_closure3(X0,X2)
& k7_relat_1(X1,k1_closure3(X0,X1)) = k7_relat_1(X2,k1_closure3(X0,X2))
& v2_relat_1(X2)
& m1_pboole(X2,X0) )
& v2_relat_1(X1)
& m1_pboole(X1,X0) )
& ~ v1_xboole_0(X0) ),
inference(flattening,[],[f66]) ).
fof(f77,plain,
! [X0,X1] :
( ( v2_relat_1(X1)
<=> ! [X2] :
( ~ r2_hidden(X2,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X2)) ) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f78,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = k1_closure3(X0,X1)
<=> X2 = a_2_0_closure3(X0,X1) )
| ~ m1_pboole(X1,X0) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f79,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f14]) ).
fof(f80,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f79]) ).
fof(f82,plain,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f89,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(flattening,[],[f89]) ).
fof(f93,plain,
! [X0,X1,X2] :
( ( r6_pboole(X0,X1,X2)
<=> X1 = X2 )
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f94,plain,
! [X0,X1,X2] :
( ( r6_pboole(X0,X1,X2)
<=> X1 = X2 )
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(flattening,[],[f93]) ).
fof(f99,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0,X1,X2] :
( k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f105,plain,
! [X0,X1,X2] :
( k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(flattening,[],[f104]) ).
fof(f108,plain,
! [X0,X1] :
( k1_relat_1(k7_relat_1(X1,X0)) = k3_xboole_0(k1_relat_1(X1),X0)
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f57]) ).
fof(f109,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| k1_relat_1(X1) != k1_relat_1(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != k1_funct_1(X0,X2)
& r2_hidden(X2,k1_relat_1(X0)) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f110,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| k1_relat_1(X1) != k1_relat_1(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != k1_funct_1(X0,X2)
& r2_hidden(X2,k1_relat_1(X0)) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
( ~ r6_pboole(sK0,sK1,sK2)
& k1_closure3(sK0,sK1) = k1_closure3(sK0,sK2)
& k7_relat_1(sK1,k1_closure3(sK0,sK1)) = k7_relat_1(sK2,k1_closure3(sK0,sK2))
& v2_relat_1(sK2)
& m1_pboole(sK2,sK0)
& v2_relat_1(sK1)
& m1_pboole(sK1,sK0)
& ~ v1_xboole_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f67]) ).
fof(f112,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ? [X2] :
( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) )
& ( ! [X2] :
( ~ r2_hidden(X2,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X2)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(nnf_transformation,[],[f77]) ).
fof(f113,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ? [X2] :
( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) )
& ( ! [X3] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X3)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(rectify,[],[f112]) ).
fof(f114,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ( r2_hidden(sK3(X0,X1),X0)
& v1_xboole_0(k1_funct_1(X1,sK3(X0,X1))) ) )
& ( ! [X3] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X3)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f113]) ).
fof(f115,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_closure3(X0,X1)
| a_2_0_closure3(X0,X1) != X2 )
& ( X2 = a_2_0_closure3(X0,X1)
| k1_closure3(X0,X1) != X2 ) )
| ~ m1_pboole(X1,X0) )
| v1_xboole_0(X0) ),
inference(nnf_transformation,[],[f78]) ).
fof(f116,plain,
! [X0,X1] :
( ( ( m1_pboole(X1,X0)
| k1_relat_1(X1) != X0 )
& ( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(nnf_transformation,[],[f80]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f117]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK4(X0,X1,X2),X0)
| ~ r2_hidden(sK4(X0,X1,X2),X1)
| ~ r2_hidden(sK4(X0,X1,X2),X2) )
& ( ( r2_hidden(sK4(X0,X1,X2),X0)
& r2_hidden(sK4(X0,X1,X2),X1) )
| r2_hidden(sK4(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f119]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(nnf_transformation,[],[f90]) ).
fof(f124,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ? [X4] :
( m1_subset_1(X4,X1)
& X0 = X4
& k1_xboole_0 != k1_funct_1(X2,X4) )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(rectify,[],[f123]) ).
fof(f125,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ( m1_subset_1(sK7(X0,X1,X2),X1)
& sK7(X0,X1,X2) = X0
& k1_xboole_0 != k1_funct_1(X2,sK7(X0,X1,X2)) )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X4,sK7(X0,X1,X2))],[f124]) ).
fof(f141,plain,
! [X0,X1,X2] :
( ( ( r6_pboole(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r6_pboole(X0,X1,X2) ) )
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(nnf_transformation,[],[f94]) ).
fof(f144,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| k1_relat_1(X1) != k1_relat_1(X0)
| ( k1_funct_1(X1,sK22(X0,X1)) != k1_funct_1(X0,sK22(X0,X1))
& r2_hidden(sK22(X0,X1),k1_relat_1(X0)) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X2,sK22(X0,X1))],[f110]) ).
fof(f145,plain,
~ v1_xboole_0(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f146,plain,
m1_pboole(sK1,sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f147,plain,
v2_relat_1(sK1),
inference(cnf_transformation,[],[f111]) ).
fof(f148,plain,
m1_pboole(sK2,sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f150,plain,
k7_relat_1(sK1,k1_closure3(sK0,sK1)) = k7_relat_1(sK2,k1_closure3(sK0,sK2)),
inference(cnf_transformation,[],[f111]) ).
fof(f151,plain,
k1_closure3(sK0,sK1) = k1_closure3(sK0,sK2),
inference(cnf_transformation,[],[f111]) ).
fof(f152,plain,
~ r6_pboole(sK0,sK1,sK2),
inference(cnf_transformation,[],[f111]) ).
fof(f160,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f161,plain,
! [X3,X0,X1] :
( ~ v1_xboole_0(k1_funct_1(X1,X3))
| ~ r2_hidden(X3,X0)
| ~ v2_relat_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f165,plain,
! [X2,X0,X1] :
( k1_closure3(X0,X1) = X2
| a_2_0_closure3(X0,X1) != X2
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f166,plain,
! [X0,X1] :
( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f116]) ).
fof(f170,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f120]) ).
fof(f175,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| v1_funct_1(X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f176,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| v1_relat_1(X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f181,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f28]) ).
fof(f188,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3)
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f227,plain,
! [X2,X0,X1] :
( r6_pboole(X0,X1,X2)
| X1 != X2
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f230,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X1,k1_relat_1(k7_relat_1(X2,X0)))
| k1_funct_1(k7_relat_1(X2,X0),X1) = k1_funct_1(X2,X1)
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f239,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| k1_relat_1(k7_relat_1(X1,X0)) = k3_xboole_0(k1_relat_1(X1),X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f240,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| k1_relat_1(X1) != k1_relat_1(X0)
| r2_hidden(sK22(X0,X1),k1_relat_1(X0))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f144]) ).
fof(f241,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| k1_relat_1(X1) != k1_relat_1(X0)
| k1_funct_1(X1,sK22(X0,X1)) != k1_funct_1(X0,sK22(X0,X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f144]) ).
fof(f242,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| k1_closure3(X0,X1) = a_2_0_closure3(X0,X1)
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f165]) ).
fof(f245,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,k3_xboole_0(X0,X1)) ),
inference(equality_resolution,[],[f170]) ).
fof(f248,plain,
! [X2,X3,X1] :
( ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,X1)
| k1_xboole_0 = k1_funct_1(X2,X3)
| v1_xboole_0(X1)
| r2_hidden(X3,a_2_0_closure3(X1,X2)) ),
inference(equality_resolution,[],[f188]) ).
fof(f250,plain,
! [X2,X0] :
( r6_pboole(X0,X2,X2)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X2,X0) ),
inference(equality_resolution,[],[f227]) ).
fof(f251,plain,
! [X2,X0] :
( ~ m1_pboole(X2,X0)
| r6_pboole(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f250]) ).
fof(f252,plain,
k7_relat_1(sK1,k1_closure3(sK0,sK1)) = k7_relat_1(sK2,k1_closure3(sK0,sK1)),
inference(forward_demodulation,[],[f150,f151]) ).
fof(f261,plain,
v1_funct_1(sK1),
inference(resolution,[],[f175,f146]) ).
fof(f262,plain,
v1_funct_1(sK2),
inference(resolution,[],[f175,f148]) ).
fof(f266,plain,
v1_relat_1(sK1),
inference(resolution,[],[f176,f146]) ).
fof(f267,plain,
v1_relat_1(sK2),
inference(resolution,[],[f176,f148]) ).
fof(f453,plain,
r6_pboole(sK0,sK1,sK1),
inference(resolution,[],[f251,f146]) ).
fof(f1088,plain,
! [X0,X1] :
( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0)
| ~ v1_funct_1(X1) ),
inference(forward_subsumption_resolution,[],[f166,f176]) ).
fof(f1089,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| k1_relat_1(X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1088,f175]) ).
fof(f1196,plain,
sK0 = k1_relat_1(sK1),
inference(resolution,[],[f1089,f146]) ).
fof(f1197,plain,
sK0 = k1_relat_1(sK2),
inference(resolution,[],[f1089,f148]) ).
fof(f1368,plain,
! [X0] : k1_relat_1(k7_relat_1(sK1,X0)) = k3_xboole_0(k1_relat_1(sK1),X0),
inference(resolution,[],[f239,f266]) ).
fof(f1383,plain,
! [X0] : k1_relat_1(k7_relat_1(sK1,X0)) = k3_xboole_0(sK0,X0),
inference(forward_demodulation,[],[f1368,f1196]) ).
fof(f1650,plain,
( k1_closure3(sK0,sK1) = a_2_0_closure3(sK0,sK1)
| v1_xboole_0(sK0) ),
inference(resolution,[],[f242,f146]) ).
fof(f1657,plain,
k1_closure3(sK0,sK1) = a_2_0_closure3(sK0,sK1),
inference(forward_subsumption_resolution,[],[f1650,f145]) ).
fof(f3951,plain,
! [X0] :
( ~ m1_subset_1(X0,sK0)
| k1_xboole_0 = k1_funct_1(sK1,X0)
| v1_xboole_0(sK0)
| r2_hidden(X0,a_2_0_closure3(sK0,sK1)) ),
inference(resolution,[],[f248,f146]) ).
fof(f3962,plain,
! [X0] :
( ~ m1_subset_1(X0,sK0)
| k1_xboole_0 = k1_funct_1(sK1,X0)
| r2_hidden(X0,a_2_0_closure3(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3951,f145]) ).
fof(f3972,plain,
! [X0] :
( ~ m1_subset_1(X0,sK0)
| r2_hidden(X0,k1_closure3(sK0,sK1))
| k1_xboole_0 = k1_funct_1(sK1,X0) ),
inference(forward_demodulation,[],[f3962,f1657]) ).
fof(f4045,plain,
! [X0] :
( ~ r2_hidden(X0,k1_relat_1(k7_relat_1(sK1,k1_closure3(sK0,sK1))))
| k1_funct_1(sK2,X0) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),X0)
| ~ v1_relat_1(sK2)
| ~ v1_funct_1(sK2) ),
inference(superposition,[],[f236,f252]) ).
fof(f4049,plain,
! [X0,X1] :
( ~ r2_hidden(X1,k3_xboole_0(sK0,X0))
| k1_funct_1(k7_relat_1(sK1,X0),X1) = k1_funct_1(sK1,X1)
| ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1) ),
inference(superposition,[],[f236,f1383]) ).
fof(f4066,plain,
! [X0,X1] :
( ~ r2_hidden(X1,k3_xboole_0(sK0,X0))
| k1_funct_1(k7_relat_1(sK1,X0),X1) = k1_funct_1(sK1,X1)
| ~ v1_funct_1(sK1) ),
inference(forward_subsumption_resolution,[],[f4049,f266]) ).
fof(f4070,plain,
! [X0] :
( ~ r2_hidden(X0,k1_relat_1(k7_relat_1(sK1,k1_closure3(sK0,sK1))))
| k1_funct_1(sK2,X0) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),X0)
| ~ v1_funct_1(sK2) ),
inference(forward_subsumption_resolution,[],[f4045,f267]) ).
fof(f4087,plain,
! [X0,X1] :
( ~ r2_hidden(X1,k3_xboole_0(sK0,X0))
| k1_funct_1(k7_relat_1(sK1,X0),X1) = k1_funct_1(sK1,X1) ),
inference(forward_subsumption_resolution,[],[f4066,f261]) ).
fof(f4091,plain,
! [X0] :
( ~ r2_hidden(X0,k1_relat_1(k7_relat_1(sK1,k1_closure3(sK0,sK1))))
| k1_funct_1(sK2,X0) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),X0) ),
inference(forward_subsumption_resolution,[],[f4070,f262]) ).
fof(f4100,plain,
! [X0] :
( ~ r2_hidden(X0,k3_xboole_0(sK0,k1_closure3(sK0,sK1)))
| k1_funct_1(sK2,X0) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),X0) ),
inference(forward_demodulation,[],[f4091,f1383]) ).
fof(f4420,plain,
! [X0] :
( k1_relat_1(X0) != k1_relat_1(sK2)
| r2_hidden(sK22(sK2,X0),k1_relat_1(sK2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(sK2)
| sK2 = X0 ),
inference(resolution,[],[f240,f262]) ).
fof(f4443,plain,
! [X0] :
( k1_relat_1(X0) != k1_relat_1(sK2)
| r2_hidden(sK22(sK2,X0),k1_relat_1(sK2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| sK2 = X0 ),
inference(forward_subsumption_resolution,[],[f4420,f267]) ).
fof(f4497,plain,
! [X0] :
( k1_relat_1(X0) != sK0
| r2_hidden(sK22(sK2,X0),k1_relat_1(sK2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| sK2 = X0 ),
inference(forward_demodulation,[],[f4443,f1197]) ).
fof(f4508,plain,
! [X0] :
( k1_relat_1(X0) != sK0
| r2_hidden(sK22(sK2,X0),sK0)
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| sK2 = X0 ),
inference(forward_demodulation,[],[f4497,f1197]) ).
fof(f4719,plain,
! [X0] :
( k1_relat_1(X0) != k1_relat_1(sK2)
| k1_funct_1(X0,sK22(sK2,X0)) != k1_funct_1(sK2,sK22(sK2,X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(sK2)
| sK2 = X0 ),
inference(resolution,[],[f241,f262]) ).
fof(f4742,plain,
! [X0] :
( k1_relat_1(X0) != k1_relat_1(sK2)
| k1_funct_1(X0,sK22(sK2,X0)) != k1_funct_1(sK2,sK22(sK2,X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| sK2 = X0 ),
inference(forward_subsumption_resolution,[],[f4719,f267]) ).
fof(f4796,plain,
! [X0] :
( k1_relat_1(X0) != sK0
| k1_funct_1(X0,sK22(sK2,X0)) != k1_funct_1(sK2,sK22(sK2,X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| sK2 = X0 ),
inference(forward_demodulation,[],[f4742,f1197]) ).
fof(f26635,definition,
( spl23_54
<=> r2_hidden(sK22(sK2,sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition]) ).
fof(f26636,plain,
( ~ r2_hidden(sK22(sK2,sK1),sK0)
| spl23_54 ),
inference(avatar_component_clause,[],[f26635]) ).
fof(f26637,plain,
( r2_hidden(sK22(sK2,sK1),sK0)
| ~ spl23_54 ),
inference(avatar_component_clause,[],[f26635]) ).
fof(f26639,definition,
( spl23_55
<=> sK1 = sK2 ),
introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition]) ).
fof(f26640,plain,
( sK1 != sK2
| spl23_55 ),
inference(avatar_component_clause,[],[f26639]) ).
fof(f26641,plain,
( sK1 = sK2
| ~ spl23_55 ),
inference(avatar_component_clause,[],[f26639]) ).
fof(f27791,plain,
( ~ r6_pboole(sK0,sK1,sK1)
| ~ spl23_55 ),
inference(superposition,[],[f152,f26641]) ).
fof(f28248,plain,
( $false
| ~ spl23_55 ),
inference(forward_subsumption_resolution,[],[f27791,f453]) ).
fof(f28249,plain,
~ spl23_55,
inference(avatar_contradiction_clause,[],[f28248]) ).
fof(f28265,plain,
( m1_subset_1(sK22(sK2,sK1),sK0)
| ~ spl23_54 ),
inference(resolution,[],[f26637,f230]) ).
fof(f28539,definition,
( spl23_65
<=> k1_xboole_0 = k1_funct_1(sK1,sK22(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition]) ).
fof(f28540,plain,
( k1_xboole_0 != k1_funct_1(sK1,sK22(sK2,sK1))
| spl23_65 ),
inference(avatar_component_clause,[],[f28539]) ).
fof(f28541,plain,
( k1_xboole_0 = k1_funct_1(sK1,sK22(sK2,sK1))
| ~ spl23_65 ),
inference(avatar_component_clause,[],[f28539]) ).
fof(f58184,plain,
( sK0 != sK0
| r2_hidden(sK22(sK2,sK1),sK0)
| ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1)
| sK1 = sK2 ),
inference(superposition,[],[f4508,f1196]) ).
fof(f58188,plain,
( r2_hidden(sK22(sK2,sK1),sK0)
| ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1)
| sK1 = sK2 ),
inference(trivial_inequality_removal,[],[f58184]) ).
fof(f58192,plain,
( ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1)
| sK1 = sK2
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f58188,f26636]) ).
fof(f58216,plain,
( ~ v1_funct_1(sK1)
| sK1 = sK2
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f58192,f266]) ).
fof(f58237,plain,
( sK1 = sK2
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f58216,f261]) ).
fof(f58238,plain,
( $false
| spl23_54
| spl23_55 ),
inference(forward_subsumption_resolution,[],[f58237,f26640]) ).
fof(f58239,plain,
( spl23_54
| spl23_55 ),
inference(avatar_contradiction_clause,[],[f58238]) ).
fof(f58245,plain,
( ! [X0] :
( ~ r2_hidden(sK22(sK2,sK1),X0)
| r2_hidden(sK22(sK2,sK1),k3_xboole_0(X0,sK0)) )
| ~ spl23_54 ),
inference(resolution,[],[f26637,f245]) ).
fof(f58252,plain,
( r2_hidden(sK22(sK2,sK1),k1_closure3(sK0,sK1))
| k1_xboole_0 = k1_funct_1(sK1,sK22(sK2,sK1))
| ~ spl23_54 ),
inference(resolution,[],[f28265,f3972]) ).
fof(f58655,plain,
( sK0 != sK0
| k1_funct_1(sK2,sK22(sK2,sK1)) != k1_funct_1(sK1,sK22(sK2,sK1))
| ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1)
| sK1 = sK2 ),
inference(superposition,[],[f4796,f1196]) ).
fof(f58659,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) != k1_funct_1(sK1,sK22(sK2,sK1))
| ~ v1_relat_1(sK1)
| ~ v1_funct_1(sK1)
| sK1 = sK2 ),
inference(trivial_inequality_removal,[],[f58655]) ).
fof(f58663,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) != k1_funct_1(sK1,sK22(sK2,sK1))
| ~ v1_funct_1(sK1)
| sK1 = sK2 ),
inference(forward_subsumption_resolution,[],[f58659,f266]) ).
fof(f58687,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) != k1_funct_1(sK1,sK22(sK2,sK1))
| sK1 = sK2 ),
inference(forward_subsumption_resolution,[],[f58663,f261]) ).
fof(f58708,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) != k1_funct_1(sK1,sK22(sK2,sK1))
| spl23_55 ),
inference(forward_subsumption_resolution,[],[f58687,f26640]) ).
fof(f59593,plain,
( r2_hidden(sK22(sK2,sK1),k1_closure3(sK0,sK1))
| ~ spl23_54
| spl23_65 ),
inference(forward_subsumption_resolution,[],[f58252,f28540]) ).
fof(f59677,plain,
( r2_hidden(sK22(sK2,sK1),k3_xboole_0(k1_closure3(sK0,sK1),sK0))
| ~ spl23_54
| spl23_65 ),
inference(resolution,[],[f59593,f58245]) ).
fof(f59686,plain,
( r2_hidden(sK22(sK2,sK1),k3_xboole_0(sK0,k1_closure3(sK0,sK1)))
| ~ spl23_54
| spl23_65 ),
inference(forward_demodulation,[],[f59677,f160]) ).
fof(f59753,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),sK22(sK2,sK1))
| ~ spl23_54
| spl23_65 ),
inference(resolution,[],[f59686,f4100]) ).
fof(f59755,plain,
( k1_funct_1(sK1,sK22(sK2,sK1)) = k1_funct_1(k7_relat_1(sK1,k1_closure3(sK0,sK1)),sK22(sK2,sK1))
| ~ spl23_54
| spl23_65 ),
inference(resolution,[],[f59686,f4087]) ).
fof(f62595,plain,
( k1_funct_1(sK2,sK22(sK2,sK1)) = k1_funct_1(sK1,sK22(sK2,sK1))
| ~ spl23_54
| spl23_65 ),
inference(superposition,[],[f59755,f59753]) ).
fof(f62601,plain,
( $false
| ~ spl23_54
| spl23_55
| spl23_65 ),
inference(forward_subsumption_resolution,[],[f62595,f58708]) ).
fof(f62602,plain,
( ~ spl23_54
| spl23_55
| spl23_65 ),
inference(avatar_contradiction_clause,[],[f62601]) ).
fof(f62605,plain,
( ! [X0] :
( ~ v1_xboole_0(k1_xboole_0)
| ~ r2_hidden(sK22(sK2,sK1),X0)
| ~ v2_relat_1(sK1)
| ~ m1_pboole(sK1,X0) )
| ~ spl23_65 ),
inference(superposition,[],[f161,f28541]) ).
fof(f62606,plain,
( ! [X0] :
( ~ r2_hidden(sK22(sK2,sK1),X0)
| ~ v2_relat_1(sK1)
| ~ m1_pboole(sK1,X0) )
| ~ spl23_65 ),
inference(forward_subsumption_resolution,[],[f62605,f181]) ).
fof(f62608,plain,
( ! [X0] :
( ~ r2_hidden(sK22(sK2,sK1),X0)
| ~ m1_pboole(sK1,X0) )
| ~ spl23_65 ),
inference(forward_subsumption_resolution,[],[f62606,f147]) ).
fof(f62636,plain,
( ~ m1_pboole(sK1,sK0)
| ~ spl23_54
| ~ spl23_65 ),
inference(resolution,[],[f62608,f26637]) ).
fof(f62637,plain,
( $false
| ~ spl23_54
| ~ spl23_65 ),
inference(forward_subsumption_resolution,[],[f62636,f146]) ).
fof(f62638,plain,
( ~ spl23_54
| ~ spl23_65 ),
inference(avatar_contradiction_clause,[],[f62637]) ).
cnf(s141,plain,
~ spl23_55,
inference(sat_conversion,[],[f28249]) ).
cnf(s151,plain,
( spl23_54
| spl23_55 ),
inference(sat_conversion,[],[f58239]) ).
cnf(s162,plain,
( ~ spl23_54
| spl23_55
| spl23_65 ),
inference(sat_conversion,[],[f62602]) ).
cnf(s163,plain,
( ~ spl23_54
| ~ spl23_65 ),
inference(sat_conversion,[],[f62638]) ).
cnf(s166,plain,
spl23_54,
inference(rat,[],[s151,s141]) ).
cnf(s167,plain,
~ spl23_65,
inference(rat,[],[s163,s166]) ).
cnf(s168,plain,
$false,
inference(rat,[],[s162,s141,s167,s166]) ).
fof(f62639,plain,
$false,
inference(avatar_sat_refutation,[],[s168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG226+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.12 % Computer : n012.cluster.edu
% 0.05/0.12 % Model : x86_64 x86_64
% 0.05/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.12 % Memory : 8046.5625MB
% 0.05/0.12 % OS : Linux 6.8.0-71-generic
% 0.05/0.12 % CPULimit : 300
% 0.05/0.12 % WCLimit : 300
% 0.05/0.12 % DateTime : Mon Sep 28 19:50:19 UTC 2026
% 0.05/0.12 % CPUTime :
% 0.05/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.05/0.13 Running first-order model finding
% 0.05/0.14 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.74/1.40 % (3674155)Will run a generic schedule for satisfiability detection.
% 8.74/1.40 % (3674161)% WARNING: option uhcvi not known.
% 8.74/1.40 % (3674161)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1659871342:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.74/1.40 % (3674162)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4083703278:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.74/1.40 % (3674160)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=466661816_2999 on theBenchmark for (2999ds/0Mi)
% 8.74/1.40 % (3674164)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3181330002:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.74/1.40 % (3674163)dis+10_1_sil=32000:sp=arity:random_seed=1482886924:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.74/1.40 % (3674165)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3177735866:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.74/1.40 % (3674166)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1848597320:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.74/1.40 % TRYING [1]
% 8.74/1.40 % TRYING [2]
% 8.74/1.40 % TRYING [3]
% 8.74/1.40 % TRYING [4]
% 8.74/1.40 % TRYING [5]
% 8.74/1.40 % (3674163)Instruction limit reached!
% 8.74/1.40 % (3674163)------------------------------
% 8.74/1.40 % (3674163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.74/1.40 % (3674163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/1.40 % (3674163)CaDiCaL version: 2.1.3
% 8.74/1.40 % (3674163)Termination reason: Instruction limit
% 8.74/1.40 % (3674163)Termination phase: Saturation
% 8.74/1.40 % (3674163)Time elapsed: 0.035 s
% 8.74/1.40 % (3674163)Peak memory usage: 12 MB
% 8.74/1.40 % (3674163)Instructions burned: 104 (million)
% 8.74/1.40 % (3674164)Instruction limit reached!
% 8.74/1.40 % (3674164)------------------------------
% 8.74/1.40 % (3674164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.74/1.40 % (3674164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/1.40 % (3674164)CaDiCaL version: 2.1.3
% 8.74/1.40 % (3674164)Termination reason: Instruction limit
% 8.74/1.40 % (3674164)Termination phase: Saturation
% 8.74/1.40 % (3674164)Time elapsed: 0.037 s
% 8.74/1.40 % (3674164)Peak memory usage: 13 MB
% 8.74/1.40 % (3674164)Instructions burned: 116 (million)
% 8.74/1.40 % (3674165)Instruction limit reached!
% 8.74/1.40 % (3674165)------------------------------
% 8.74/1.40 % (3674165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.74/1.40 % (3674165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/1.40 % (3674165)CaDiCaL version: 2.1.3
% 8.74/1.40 % (3674165)Termination reason: Instruction limit
% 8.74/1.40 % (3674165)Termination phase: Saturation
% 8.74/1.40 % (3674165)Time elapsed: 0.041 s
% 8.74/1.40 % (3674165)Peak memory usage: 13 MB
% 8.74/1.40 % (3674165)Instructions burned: 131 (million)
% 8.74/1.40 % (3674174)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3753776211:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.74/1.40 % (3674175)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3957240332:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.74/1.40 % TRYING [1]
% 8.74/1.40 % TRYING [2]
% 8.74/1.40 % TRYING [3]
% 8.74/1.40 % (3674176)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=2463504906:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 8.74/1.40 % (3674166)Instruction limit reached!
% 8.74/1.40 % (3674166)------------------------------
% 8.74/1.40 % (3674166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.74/1.40 % (3674166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/1.40 % (3674166)CaDiCaL version: 2.1.3
% 8.74/1.40 % (3674166)Termination reason: Instruction limit
% 8.74/1.40 % (3674166)Termination phase: Saturation
% 8.74/1.40 % (3674166)Time elapsed: 0.054 s
% 8.74/1.40 % (3674166)Peak memory usage: 14 MB
% 8.74/1.40 % (3674166)Instructions burned: 159 (million)
% 8.74/1.40 % TRYING [6]
% 8.74/1.40 % TRYING [4]
% 8.74/1.40 % (3674180)ott-21_1_sil=16000:fs=off:random_seed=2313179342:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 8.74/1.40 % TRYING [5]
% 8.74/1.40 % TRYING [6]
% 8.74/1.40 % (3674175)Instruction limit reached!
% 8.74/1.40 % (3674175)------------------------------
% 8.74/1.40 % (3674175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674175)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674175)Termination reason: Instruction limit
% 28.46/4.21 % (3674175)Termination phase: Saturation
% 28.46/4.21 % (3674175)Time elapsed: 0.047 s
% 28.46/4.21 % (3674175)Peak memory usage: 13 MB
% 28.46/4.21 % (3674175)Instructions burned: 132 (million)
% 28.46/4.21 % (3674182)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=94386046:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 28.46/4.21 % (3674180)Instruction limit reached!
% 28.46/4.21 % (3674180)------------------------------
% 28.46/4.21 % (3674180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674180)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674180)Termination reason: Instruction limit
% 28.46/4.21 % (3674180)Termination phase: Saturation
% 28.46/4.21 % (3674180)Time elapsed: 0.053 s
% 28.46/4.21 % (3674180)Peak memory usage: 13 MB
% 28.46/4.21 % (3674180)Instructions burned: 183 (million)
% 28.46/4.21 % (3674184)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2127894347:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 28.46/4.21 % TRYING [1]
% 28.46/4.21 % TRYING [2]
% 28.46/4.21 % TRYING [3]
% 28.46/4.21 % TRYING [4]
% 28.46/4.21 % TRYING [7]
% 28.46/4.21 % TRYING [7]
% 28.46/4.21 % TRYING [5]
% 28.46/4.21 % (3674174)Instruction limit reached!
% 28.46/4.21 % (3674174)------------------------------
% 28.46/4.21 % (3674174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674174)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674174)Termination reason: Instruction limit
% 28.46/4.21 % (3674174)Termination phase: Finite model building constraint generation
% 28.46/4.21 % (3674174)Time elapsed: 0.155 s
% 28.46/4.21 % (3674174)Peak memory usage: 28 MB
% 28.46/4.21 % (3674174)Instructions burned: 718 (million)
% 28.46/4.21 % (3674186)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=400567490:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 28.46/4.21 % TRYING [6]
% 28.46/4.21 % (3674176)Instruction limit reached!
% 28.46/4.21 % (3674176)------------------------------
% 28.46/4.21 % (3674176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674176)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674176)Termination reason: Instruction limit
% 28.46/4.21 % (3674176)Termination phase: Saturation
% 28.46/4.21 % (3674176)Time elapsed: 0.225 s
% 28.46/4.21 % (3674176)Peak memory usage: 18 MB
% 28.46/4.21 % (3674176)Instructions burned: 685 (million)
% 28.46/4.21 % (3674182)Instruction limit reached!
% 28.46/4.21 % (3674182)------------------------------
% 28.46/4.21 % (3674182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674182)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674182)Termination reason: Instruction limit
% 28.46/4.21 % (3674182)Termination phase: Saturation
% 28.46/4.21 % (3674182)Time elapsed: 0.180 s
% 28.46/4.21 % (3674182)Peak memory usage: 14 MB
% 28.46/4.21 % (3674182)Instructions burned: 478 (million)
% 28.46/4.21 % (3674188)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=52017674:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 28.46/4.21 % (3674190)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=354408511:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 28.46/4.21 % (3674184)Instruction limit reached!
% 28.46/4.21 % (3674184)------------------------------
% 28.46/4.21 % (3674184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.46/4.21 % (3674184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/4.21 % (3674184)CaDiCaL version: 2.1.3
% 28.46/4.21 % (3674184)Termination reason: Instruction limit
% 28.46/4.21 % (3674184)Termination phase: Finite model building SAT solving
% 28.46/4.21 % (3674184)Time elapsed: 0.200 s
% 28.46/4.21 % (3674184)Peak memory usage: 23 MB
% 28.46/4.21 % (3674184)Instructions burned: 867 (million)
% 28.46/4.21 % TRYING [14]
% 28.46/4.21 % (3674192)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1442925899:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 54.53/7.94 % TRYING [8]
% 54.53/7.94 % (3674188)Instruction limit reached!
% 54.53/7.94 % (3674188)------------------------------
% 54.53/7.94 % (3674188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674188)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674188)Termination reason: Instruction limit
% 54.53/7.94 % (3674188)Termination phase: Finite model building constraint generation
% 54.53/7.94 % (3674188)Time elapsed: 0.176 s
% 54.53/7.94 % (3674188)Peak memory usage: 71 MB
% 54.53/7.94 % (3674188)Instructions burned: 892 (million)
% 54.53/7.94 % (3674194)fmb+10_1_sil=64000:random_seed=2755496213:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 54.53/7.94 % TRYING [1]
% 54.53/7.94 % TRYING [2]
% 54.53/7.94 % TRYING [3]
% 54.53/7.94 % TRYING [4]
% 54.53/7.94 % TRYING [5]
% 54.53/7.94 % (3674190)Instruction limit reached!
% 54.53/7.94 % (3674190)------------------------------
% 54.53/7.94 % (3674190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674190)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674190)Termination reason: Instruction limit
% 54.53/7.94 % (3674190)Termination phase: Saturation
% 54.53/7.94 % (3674190)Time elapsed: 0.222 s
% 54.53/7.94 % (3674190)Peak memory usage: 18 MB
% 54.53/7.94 % (3674190)Instructions burned: 693 (million)
% 54.53/7.94 % (3674196)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2094475184:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 54.53/7.94 % TRYING [20]
% 54.53/7.94 % TRYING [6]
% 54.53/7.94 % (3674186)Instruction limit reached!
% 54.53/7.94 % (3674186)------------------------------
% 54.53/7.94 % (3674186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674186)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674186)Termination reason: Instruction limit
% 54.53/7.94 % (3674186)Termination phase: Saturation
% 54.53/7.94 % (3674186)Time elapsed: 0.349 s
% 54.53/7.94 % (3674186)Peak memory usage: 20 MB
% 54.53/7.94 % (3674186)Instructions burned: 1181 (million)
% 54.53/7.94 % (3674198)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3560042418:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 54.53/7.94 % TRYING [8]
% 54.53/7.94 % (3674192)Instruction limit reached!
% 54.53/7.94 % (3674192)------------------------------
% 54.53/7.94 % (3674192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674192)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674192)Termination reason: Instruction limit
% 54.53/7.94 % (3674192)Termination phase: Saturation
% 54.53/7.94 % (3674192)Time elapsed: 0.276 s
% 54.53/7.94 % (3674192)Peak memory usage: 19 MB
% 54.53/7.94 % (3674192)Instructions burned: 880 (million)
% 54.53/7.94 % (3674200)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=731223779:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 54.53/7.94 % TRYING [7]
% 54.53/7.94 % TRYING [9]
% 54.53/7.94 % (3674198)Instruction limit reached!
% 54.53/7.94 % (3674198)------------------------------
% 54.53/7.94 % (3674198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674198)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674198)Termination reason: Instruction limit
% 54.53/7.94 % (3674198)Termination phase: Finite model building SAT solving
% 54.53/7.94 % (3674198)Time elapsed: 0.264 s
% 54.53/7.94 % (3674198)Peak memory usage: 62 MB
% 54.53/7.94 % (3674198)Instructions burned: 921 (million)
% 54.53/7.94 % (3674202)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=784057310:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 54.53/7.94 % TRYING [8]
% 54.53/7.94 % (3674202)Instruction limit reached!
% 54.53/7.94 % (3674202)------------------------------
% 54.53/7.94 % (3674202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.53/7.94 % (3674202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.53/7.94 % (3674202)CaDiCaL version: 2.1.3
% 54.53/7.94 % (3674202)Termination reason: Instruction limit
% 54.53/7.94 % (3674202)Termination phase: Saturation
% 54.53/7.94 % (3674202)Time elapsed: 0.354 s
% 54.53/7.94 % (3674202)Peak memory usage: 19 MB
% 54.53/7.94 % (3674202)Instructions burned: 1475 (million)
% 54.53/7.94 % (3674204)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2506732049:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 154.81/22.13 % TRYING [77]
% 154.81/22.13 % TRYING [9]
% 154.81/22.13 % (3674200)Instruction limit reached!
% 154.81/22.13 % (3674200)------------------------------
% 154.81/22.13 % (3674200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674200)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674200)Termination reason: Instruction limit
% 154.81/22.13 % (3674200)Termination phase: Saturation
% 154.81/22.13 % (3674200)Time elapsed: 1.475 s
% 154.81/22.13 % (3674200)Peak memory usage: 36 MB
% 154.81/22.13 % (3674200)Instructions burned: 5134 (million)
% 154.81/22.13 % (3674206)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=769891443:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 154.81/22.13 % TRYING [16]
% 154.81/22.13 % TRYING [10]
% 154.81/22.13 % (3674204)Instruction limit reached!
% 154.81/22.13 % (3674204)------------------------------
% 154.81/22.13 % (3674204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674204)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674204)Termination reason: Instruction limit
% 154.81/22.13 % (3674204)Termination phase: Finite model building constraint generation
% 154.81/22.13 % (3674204)Time elapsed: 1.251 s
% 154.81/22.13 % (3674204)Peak memory usage: 452 MB
% 154.81/22.13 % (3674204)Instructions burned: 6325 (million)
% 154.81/22.13 % (3674208)ott-2_1_sil=16000:newcnf=on:random_seed=3542208828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 154.81/22.13 % (3674206)Instruction limit reached!
% 154.81/22.13 % (3674206)------------------------------
% 154.81/22.13 % (3674206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674206)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674206)Termination reason: Instruction limit
% 154.81/22.13 % (3674206)Termination phase: Finite model building constraint generation
% 154.81/22.13 % (3674206)Time elapsed: 0.405 s
% 154.81/22.13 % (3674206)Peak memory usage: 132 MB
% 154.81/22.13 % (3674206)Instructions burned: 2177 (million)
% 154.81/22.13 % (3674210)ott+10_1_sil=32000:tgt=ground:random_seed=518428063:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 154.81/22.13 % (3674208)Instruction limit reached!
% 154.81/22.13 % (3674208)------------------------------
% 154.81/22.13 % (3674208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674208)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674208)Termination reason: Instruction limit
% 154.81/22.13 % (3674208)Termination phase: Saturation
% 154.81/22.13 % (3674208)Time elapsed: 0.254 s
% 154.81/22.13 % (3674208)Peak memory usage: 18 MB
% 154.81/22.13 % (3674208)Instructions burned: 871 (million)
% 154.81/22.13 % (3674212)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2915678046:i=54282_2971 on theBenchmark for (2971ds/54282Mi)
% 154.81/22.13 % TRYING [1]
% 154.81/22.13 % TRYING [2]
% 154.81/22.13 % TRYING [3]
% 154.81/22.13 % TRYING [4]
% 154.81/22.13 % TRYING [5]
% 154.81/22.13 % TRYING [6]
% 154.81/22.13 % TRYING [7]
% 154.81/22.13 % (3674196)Instruction limit reached!
% 154.81/22.13 % (3674196)------------------------------
% 154.81/22.13 % (3674196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674196)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674196)Termination reason: Instruction limit
% 154.81/22.13 % (3674196)Termination phase: Finite model building constraint generation
% 154.81/22.13 % (3674196)Time elapsed: 2.452 s
% 154.81/22.13 % (3674196)Peak memory usage: 801 MB
% 154.81/22.13 % (3674196)Instructions burned: 9516 (million)
% 154.81/22.13 % (3674214)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2988404136:i=3512:aac=none_2969 on theBenchmark for (2969ds/3512Mi)
% 154.81/22.13 % TRYING [8]
% 154.81/22.13 % TRYING [9]
% 154.81/22.13 % TRYING [10]
% 154.81/22.13 % (3674210)Instruction limit reached!
% 154.81/22.13 % (3674210)------------------------------
% 154.81/22.13 % (3674210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.81/22.13 % (3674210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.81/22.13 % (3674210)CaDiCaL version: 2.1.3
% 154.81/22.13 % (3674210)Termination reason: Instruction limit
% 154.81/22.13 % (3674210)Termination phase: Saturation
% 154.81/22.13 % (3674210)Time elapsed: 1.485 s
% 154.81/22.13 % (3674210)Peak memory usage: 44 MB
% 106.66/28.06 % (3674210)Instructions burned: 5116 (million)
% 106.66/28.06 % (3674214)Instruction limit reached!
% 106.66/28.06 % (3674214)------------------------------
% 106.66/28.06 % (3674214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674214)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674214)Termination reason: Instruction limit
% 106.66/28.06 % (3674214)Termination phase: Saturation
% 106.66/28.06 % (3674214)Time elapsed: 0.990 s
% 106.66/28.06 % (3674214)Peak memory usage: 29 MB
% 106.66/28.06 % (3674214)Instructions burned: 3517 (million)
% 106.66/28.06 % (3674216)dis+21_1_sil=32000:sas=cadical:random_seed=2321902922:i=3773:amm=off_2959 on theBenchmark for (2959ds/3773Mi)
% 106.66/28.06 % (3674218)ott+11_1_sil=16000:gs=on:random_seed=4252079258:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2959 on theBenchmark for (2959ds/2251Mi)
% 106.66/28.06 % (3674218)Instruction limit reached!
% 106.66/28.06 % (3674218)------------------------------
% 106.66/28.06 % (3674218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674218)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674218)Termination reason: Instruction limit
% 106.66/28.06 % (3674218)Termination phase: Saturation
% 106.66/28.06 % (3674218)Time elapsed: 0.792 s
% 106.66/28.06 % (3674218)Peak memory usage: 34 MB
% 106.66/28.06 % (3674218)Instructions burned: 2251 (million)
% 106.66/28.06 % (3674220)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1237056346:fmbsr=1.6:i=67534_2951 on theBenchmark for (2951ds/67534Mi)
% 106.66/28.06 % TRYING [7]
% 106.66/28.06 % (3674216)Instruction limit reached!
% 106.66/28.06 % (3674216)------------------------------
% 106.66/28.06 % (3674216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674216)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674216)Termination reason: Instruction limit
% 106.66/28.06 % (3674216)Termination phase: Saturation
% 106.66/28.06 % (3674216)Time elapsed: 1.099 s
% 106.66/28.06 % (3674216)Peak memory usage: 34 MB
% 106.66/28.06 % (3674216)Instructions burned: 3773 (million)
% 106.66/28.06 % (3674222)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2809426063:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2948 on theBenchmark for (2948ds/4591Mi)
% 106.66/28.06 % TRYING [8]
% 106.66/28.06 % TRYING [9]
% 106.66/28.06 % (3674194)Instruction limit reached!
% 106.66/28.06 % (3674194)------------------------------
% 106.66/28.06 % (3674194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674194)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674194)Termination reason: Instruction limit
% 106.66/28.06 % (3674194)Termination phase: Finite model building SAT solving
% 106.66/28.06 % (3674194)Time elapsed: 5.749 s
% 106.66/28.06 % (3674194)Peak memory usage: 94 MB
% 106.66/28.06 % (3674194)Instructions burned: 22064 (million)
% 106.66/28.06 % (3674224)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1589137685:i=29340_2937 on theBenchmark for (2937ds/29340Mi)
% 106.66/28.06 % (3674222)Instruction limit reached!
% 106.66/28.06 % (3674222)------------------------------
% 106.66/28.06 % (3674222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674222)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674222)Termination reason: Instruction limit
% 106.66/28.06 % (3674222)Termination phase: Saturation
% 106.66/28.06 % (3674222)Time elapsed: 1.197 s
% 106.66/28.06 % (3674222)Peak memory usage: 41 MB
% 106.66/28.06 % (3674222)Instructions burned: 4594 (million)
% 106.66/28.06 % (3674226)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=274176444:i=5211_2936 on theBenchmark for (2936ds/5211Mi)
% 106.66/28.06 % TRYING [10]
% 106.66/28.06 % TRYING [10]
% 106.66/28.06 % (3674226)Instruction limit reached!
% 106.66/28.06 % (3674226)------------------------------
% 106.66/28.06 % (3674226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674226)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674226)Termination reason: Instruction limit
% 106.66/28.06 % (3674226)Termination phase: Saturation
% 106.66/28.06 % (3674226)Time elapsed: 1.388 s
% 106.66/28.06 % (3674226)Peak memory usage: 46 MB
% 106.66/28.06 % (3674226)Instructions burned: 5212 (million)
% 106.66/28.06 % (3674228)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2520262435:i=5497:nm=2_2921 on theBenchmark for (2921ds/5497Mi)
% 106.66/28.06 % TRYING [17]
% 106.66/28.06 % (3674228)Instruction limit reached!
% 106.66/28.06 % (3674228)------------------------------
% 106.66/28.06 % (3674228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674228)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674228)Termination reason: Instruction limit
% 106.66/28.06 % (3674228)Termination phase: Finite model building constraint generation
% 106.66/28.06 % (3674228)Time elapsed: 1.620 s
% 106.66/28.06 % (3674228)Peak memory usage: 449 MB
% 106.66/28.06 % (3674228)Instructions burned: 5499 (million)
% 106.66/28.06 % (3674230)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=965302217:fmbsr=2:i=46332_2905 on theBenchmark for (2905ds/46332Mi)
% 106.66/28.06 % TRYING [15]
% 106.66/28.06 % (3674224)Instruction limit reached!
% 106.66/28.06 % (3674224)------------------------------
% 106.66/28.06 % (3674224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674224)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674224)Termination reason: Instruction limit
% 106.66/28.06 % (3674224)Termination phase: Saturation
% 106.66/28.06 % (3674224)Time elapsed: 8.054 s
% 106.66/28.06 % (3674224)Peak memory usage: 183 MB
% 106.66/28.06 % (3674224)Instructions burned: 29340 (million)
% 106.66/28.06 % (3674232)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1625476720:i=14071_2856 on theBenchmark for (2856ds/14071Mi)
% 106.66/28.06 % TRYING [12]
% 106.66/28.06 % TRYING [11]
% 106.66/28.06 % TRYING [11]
% 106.66/28.06 % TRYING [11]
% 106.66/28.06 % (3674212)Instruction limit reached!
% 106.66/28.06 % (3674212)------------------------------
% 106.66/28.06 % (3674212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674212)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674212)Termination reason: Instruction limit
% 106.66/28.06 % (3674212)Termination phase: Finite model building SAT solving
% 106.66/28.06 % (3674212)Time elapsed: 16.324 s
% 106.66/28.06 % (3674212)Peak memory usage: 170 MB
% 106.66/28.06 % (3674212)Instructions burned: 54282 (million)
% 106.66/28.06 % (3674234)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1090487677:i=22565:add=on:rawr=on_2808 on theBenchmark for (2808ds/22565Mi)
% 106.66/28.06 % (3674162)Instruction limit reached!
% 106.66/28.06 % (3674162)------------------------------
% 106.66/28.06 % (3674162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674162)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674162)Termination reason: Instruction limit
% 106.66/28.06 % (3674162)Termination phase: Saturation
% 106.66/28.06 % (3674162)Time elapsed: 19.426 s
% 106.66/28.06 % (3674162)Peak memory usage: 51 MB
% 106.66/28.06 % (3674162)Instructions burned: 88024 (million)
% 106.66/28.06 % (3674236)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=176868428:i=8173:av=off_2805 on theBenchmark for (2805ds/8173Mi)
% 106.66/28.06 % (3674232)Instruction limit reached!
% 106.66/28.06 % (3674232)------------------------------
% 106.66/28.06 % (3674232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674232)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674232)Termination reason: Instruction limit
% 106.66/28.06 % (3674232)Termination phase: Finite model building SAT solving
% 106.66/28.06 % (3674232)Time elapsed: 5.202 s
% 106.66/28.06 % (3674232)Peak memory usage: 312 MB
% 106.66/28.06 % (3674232)Instructions burned: 14075 (million)
% 106.66/28.06 % (3674238)dis+10_16:1_sil=16000:random_seed=344527777:i=9155:fsr=off_2804 on theBenchmark for (2804ds/9155Mi)
% 106.66/28.06 % (3674236)Instruction limit reached!
% 106.66/28.06 % (3674236)------------------------------
% 106.66/28.06 % (3674236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674236)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674236)Termination reason: Instruction limit
% 106.66/28.06 % (3674236)Termination phase: Saturation
% 106.66/28.06 % (3674236)Time elapsed: 2.516 s
% 106.66/28.06 % (3674236)Peak memory usage: 83 MB
% 106.66/28.06 % (3674236)Instructions burned: 8173 (million)
% 106.66/28.06 % (3674240)ott-3_8_sil=64000:random_seed=3360615921:i=20139:bs=on_2780 on theBenchmark for (2780ds/20139Mi)
% 106.66/28.06 % (3674238)Instruction limit reached!
% 106.66/28.06 % (3674238)------------------------------
% 106.66/28.06 % (3674238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674238)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674238)Termination reason: Instruction limit
% 106.66/28.06 % (3674238)Termination phase: Saturation
% 106.66/28.06 % (3674238)Time elapsed: 2.611 s
% 106.66/28.06 % (3674238)Peak memory usage: 64 MB
% 106.66/28.06 % (3674238)Instructions burned: 9156 (million)
% 106.66/28.06 % (3674242)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1182931033:fmbsr=2:i=32576_2777 on theBenchmark for (2777ds/32576Mi)
% 106.66/28.06 % TRYING [9]
% 106.66/28.06 % (3674220)Instruction limit reached!
% 106.66/28.06 % (3674220)------------------------------
% 106.66/28.06 % (3674220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674220)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674220)Termination reason: Instruction limit
% 106.66/28.06 % (3674220)Termination phase: Finite model building SAT solving
% 106.66/28.06 % (3674220)Time elapsed: 18.514 s
% 106.66/28.06 % (3674220)Peak memory usage: 162 MB
% 106.66/28.06 % (3674220)Instructions burned: 67537 (million)
% 106.66/28.06 % (3674244)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1584386243:i=11404_2765 on theBenchmark for (2765ds/11404Mi)
% 106.66/28.06 % (3674234)Instruction limit reached!
% 106.66/28.06 % (3674234)------------------------------
% 106.66/28.06 % (3674234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674234)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674234)Termination reason: Instruction limit
% 106.66/28.06 % (3674234)Termination phase: Saturation
% 106.66/28.06 % (3674234)Time elapsed: 5.113 s
% 106.66/28.06 % (3674234)Peak memory usage: 31 MB
% 106.66/28.06 % (3674234)Instructions burned: 22569 (million)
% 106.66/28.06 % (3674246)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=365368664:i=14134_2757 on theBenchmark for (2757ds/14134Mi)
% 106.66/28.06 % TRYING [10]
% 106.66/28.06 % (3674244)Instruction limit reached!
% 106.66/28.06 % (3674244)------------------------------
% 106.66/28.06 % (3674244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674244)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674244)Termination reason: Instruction limit
% 106.66/28.06 % (3674244)Termination phase: Saturation
% 106.66/28.06 % (3674244)Time elapsed: 3.543 s
% 106.66/28.06 % (3674244)Peak memory usage: 86 MB
% 106.66/28.06 % (3674244)Instructions burned: 11406 (million)
% 106.66/28.06 % (3674248)dis+33_16_sil=32000:sac=on:random_seed=429336143:i=15851:nm=0_2729 on theBenchmark for (2729ds/15851Mi)
% 106.66/28.06 % (3674248) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3674155-3674248"...
% 106.66/28.06 % (3674248)...printing done.
% 106.66/28.06 % (3674248)Refutation found. Thanks to Tanya!
% 106.66/28.06 % SZS status Theorem for theBenchmark
% 106.66/28.06 % SZS output start Proof for theBenchmark
% See solution above
% 106.66/28.06 % (3674248)------------------------------
% 106.66/28.06 % (3674248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.66/28.06 % (3674248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.66/28.06 % (3674248)CaDiCaL version: 2.1.3
% 106.66/28.06 % (3674248)Termination reason: Refutation
% 106.66/28.06 % (3674248)Time elapsed: 0.830 s
% 106.66/28.06 % (3674248)Peak memory usage: 32 MB
% 106.66/28.06 % (3674248)Instructions burned: 2884 (million)
% 106.66/28.06 % (3674155)Success in time 27.92 s
% 106.66/28.06 % Vampire exiting
%------------------------------------------------------------------------------