%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUN086+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:27:06 PM UTC 2026
% Result : Theorem 268.94s 38.50s
% Output : Refutation 268.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 16
% Syntax : Number of formulae : 138 ( 54 unt; 1 def)
% Number of atoms : 329 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 340 ( 149 ~; 138 |; 52 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 2 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-2 aty)
% Number of variables : 245 ( 0 sgn 220 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
? [X0] :
! [X1] :
( ( id(X1,X0)
& r1(X1) )
| ( ~ r1(X1)
& ~ id(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_1) ).
fof(f3,axiom,
! [X0,X1] :
? [X2] :
! [X3] :
( ( id(X3,X2)
& r3(X0,X1,X3) )
| ( ~ r3(X0,X1,X3)
& ~ id(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_3) ).
fof(f4,axiom,
! [X0,X1] :
? [X2] :
! [X3] :
( ( id(X3,X2)
& r4(X0,X1,X3) )
| ( ~ r4(X0,X1,X3)
& ~ id(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_4) ).
fof(f5,axiom,
! [X0] : id(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ id(X0,X1)
| id(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_6) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ~ id(X0,X1)
| id(X0,X2)
| ~ id(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_7) ).
fof(f8,axiom,
! [X0,X1] :
( ~ id(X0,X1)
| ( ~ r1(X0)
& ~ r1(X1) )
| ( r1(X0)
& r1(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_8) ).
fof(f9,axiom,
! [X0,X1,X2,X3] :
( ~ id(X0,X2)
| ~ id(X1,X3)
| ( ~ r2(X0,X1)
& ~ r2(X2,X3) )
| ( r2(X0,X1)
& r2(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_9) ).
fof(f10,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ~ id(X0,X3)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ( ~ r3(X0,X1,X2)
& ~ r3(X3,X4,X5) )
| ( r3(X0,X1,X2)
& r3(X3,X4,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_10) ).
fof(f11,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ~ id(X0,X3)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ( ~ r4(X0,X1,X2)
& ~ r4(X3,X4,X5) )
| ( r4(X0,X1,X2)
& r4(X3,X4,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_11) ).
fof(f13,axiom,
! [X0,X1] :
? [X2] :
( ? [X3] :
( id(X3,X2)
& ? [X4] :
( r2(X1,X4)
& r4(X0,X4,X3) ) )
& ? [X5] :
( r3(X5,X0,X2)
& r4(X0,X1,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_2a) ).
fof(f15,axiom,
! [X0] :
? [X1] :
( id(X1,X0)
& ? [X2] :
( r1(X2)
& r3(X0,X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_4a) ).
fof(f16,axiom,
! [X0] :
? [X1] :
( ? [X2] :
( r1(X2)
& r4(X0,X2,X1) )
& ? [X3] :
( id(X1,X3)
& r1(X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_5a) ).
fof(f17,axiom,
! [X0] :
( ? [X1] :
( id(X0,X1)
& r1(X1) )
| ? [X2,X3] :
( id(X0,X3)
& r2(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax',axiom_6a) ).
fof(f19,conjecture,
? [X0] :
( ? [X1] :
( ? [X2] :
( r1(X2)
& r2(X2,X1) )
& ? [X3] :
( r1(X3)
& r4(X3,X1,X0) ) )
& ? [X4] :
( id(X0,X4)
& r1(X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zerotimesoneidzero) ).
fof(f20,negated_conjecture,
~ ? [X0] :
( ? [X1] :
( ? [X2] :
( r1(X2)
& r2(X2,X1) )
& ? [X3] :
( r1(X3)
& r4(X3,X1,X0) ) )
& ? [X4] :
( id(X0,X4)
& r1(X4) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ r1(X2)
| ~ r2(X2,X1) )
| ! [X3] :
( ~ r1(X3)
| ~ r4(X3,X1,X0) ) )
| ! [X4] :
( ~ id(X0,X4)
| ~ r1(X4) ) ),
inference(ennf_transformation,[],[f20]) ).
fof(f22,plain,
! [X1] :
( ( id(X1,sK0)
& r1(X1) )
| ( ~ r1(X1)
& ~ id(X1,sK0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f1]) ).
fof(f24,plain,
! [X0,X1,X3] :
( ( id(X3,sK2(X0,X1))
& r3(X0,X1,X3) )
| ( ~ r3(X0,X1,X3)
& ~ id(X3,sK2(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X2,sK2(X0,X1))],[f3]) ).
fof(f25,plain,
! [X0,X1,X3] :
( ( id(X3,sK3(X0,X1))
& r4(X0,X1,X3) )
| ( ~ r4(X0,X1,X3)
& ~ id(X3,sK3(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f4]) ).
fof(f27,plain,
! [X0,X1] :
( id(sK9(X0,X1),sK8(X0,X1))
& r2(X1,sK10(X0,X1))
& r4(X0,sK10(X0,X1),sK9(X0,X1))
& r3(sK11(X0,X1),X0,sK8(X0,X1))
& r4(X0,X1,sK11(X0,X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11]),skolemize(X2,sK8(X0,X1)),skolemize(X3,sK9(X0,X1)),skolemize(X4,sK10(X0,X1)),skolemize(X5,sK11(X0,X1))],[f13]) ).
fof(f28,plain,
! [X0] :
( id(sK12(X0),X0)
& r1(sK13(X0))
& r3(X0,sK13(X0),sK12(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0))],[f15]) ).
fof(f29,plain,
! [X0] :
( r1(sK15(X0))
& r4(X0,sK15(X0),sK14(X0))
& id(sK14(X0),sK16(X0))
& r1(sK16(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X1,sK14(X0)),skolemize(X2,sK15(X0)),skolemize(X3,sK16(X0))],[f16]) ).
fof(f30,plain,
! [X0] :
( ( id(X0,sK17(X0))
& r1(sK17(X0)) )
| ( id(X0,sK19(X0))
& r2(sK18(X0),sK19(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X1,sK17(X0)),skolemize(X2,sK18(X0)),skolemize(X3,sK19(X0))],[f17]) ).
fof(f31,plain,
! [X1] :
( ~ id(X1,sK0)
| r1(X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f34,plain,
! [X1] :
( ~ r1(X1)
| id(X1,sK0) ),
inference(cnf_transformation,[],[f22]) ).
fof(f42,plain,
! [X3,X0,X1] :
( ~ r3(X0,X1,X3)
| id(X3,sK2(X0,X1)) ),
inference(cnf_transformation,[],[f24]) ).
fof(f46,plain,
! [X3,X0,X1] :
( ~ r4(X0,X1,X3)
| id(X3,sK3(X0,X1)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f47,plain,
! [X0] : id(X0,X0),
inference(cnf_transformation,[],[f5]) ).
fof(f48,plain,
! [X0,X1] :
( ~ id(X0,X1)
| id(X1,X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f49,plain,
! [X2,X0,X1] :
( ~ id(X1,X2)
| id(X0,X2)
| ~ id(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f51,plain,
! [X0,X1] :
( ~ id(X0,X1)
| ~ r1(X1)
| r1(X0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f52,plain,
! [X0,X1] :
( ~ id(X0,X1)
| ~ r1(X0)
| r1(X1) ),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X2,X3,X0,X1] :
( ~ r2(X2,X3)
| ~ id(X1,X3)
| ~ id(X0,X2)
| r2(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f59,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r3(X3,X4,X5)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ~ id(X0,X3)
| r3(X0,X1,X2) ),
inference(cnf_transformation,[],[f10]) ).
fof(f60,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r3(X0,X1,X2)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ~ id(X0,X3)
| r3(X3,X4,X5) ),
inference(cnf_transformation,[],[f10]) ).
fof(f63,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r4(X3,X4,X5)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ~ id(X0,X3)
| r4(X0,X1,X2) ),
inference(cnf_transformation,[],[f11]) ).
fof(f64,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r4(X0,X1,X2)
| ~ id(X1,X4)
| ~ id(X2,X5)
| ~ id(X0,X3)
| r4(X3,X4,X5) ),
inference(cnf_transformation,[],[f11]) ).
fof(f71,plain,
! [X0,X1] : r4(X0,X1,sK11(X0,X1)),
inference(cnf_transformation,[],[f27]) ).
fof(f72,plain,
! [X0,X1] : r3(sK11(X0,X1),X0,sK8(X0,X1)),
inference(cnf_transformation,[],[f27]) ).
fof(f73,plain,
! [X0,X1] : r4(X0,sK10(X0,X1),sK9(X0,X1)),
inference(cnf_transformation,[],[f27]) ).
fof(f74,plain,
! [X0,X1] : r2(X1,sK10(X0,X1)),
inference(cnf_transformation,[],[f27]) ).
fof(f75,plain,
! [X0,X1] : id(sK9(X0,X1),sK8(X0,X1)),
inference(cnf_transformation,[],[f27]) ).
fof(f77,plain,
! [X0] : r3(X0,sK13(X0),sK12(X0)),
inference(cnf_transformation,[],[f28]) ).
fof(f78,plain,
! [X0] : r1(sK13(X0)),
inference(cnf_transformation,[],[f28]) ).
fof(f79,plain,
! [X0] : id(sK12(X0),X0),
inference(cnf_transformation,[],[f28]) ).
fof(f80,plain,
! [X0] : r1(sK16(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f81,plain,
! [X0] : id(sK14(X0),sK16(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f82,plain,
! [X0] : r4(X0,sK15(X0),sK14(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f83,plain,
! [X0] : r1(sK15(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f85,plain,
! [X0] :
( id(X0,sK19(X0))
| r1(sK17(X0)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f87,plain,
! [X0] :
( id(X0,sK19(X0))
| id(X0,sK17(X0)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f89,plain,
! [X2,X3,X0,X1,X4] :
( ~ r4(X3,X1,X0)
| ~ r2(X2,X1)
| ~ r1(X3)
| ~ r1(X2)
| ~ id(X0,X4)
| ~ r1(X4) ),
inference(cnf_transformation,[],[f21]) ).
fof(f90,plain,
r1(sK0),
inference(resolution,[],[f31,f47]) ).
fof(f94,plain,
! [X0] : id(sK13(X0),sK0),
inference(resolution,[],[f34,f78]) ).
fof(f95,plain,
! [X0] : id(sK15(X0),sK0),
inference(resolution,[],[f34,f83]) ).
fof(f96,plain,
! [X0] : id(sK16(X0),sK0),
inference(resolution,[],[f34,f80]) ).
fof(f101,plain,
! [X0] : id(X0,sK12(X0)),
inference(resolution,[],[f48,f79]) ).
fof(f102,plain,
! [X0] : id(sK0,sK13(X0)),
inference(resolution,[],[f48,f94]) ).
fof(f103,plain,
! [X0] : id(sK0,sK15(X0)),
inference(resolution,[],[f48,f95]) ).
fof(f105,plain,
! [X0] : id(sK16(X0),sK14(X0)),
inference(resolution,[],[f48,f81]) ).
fof(f144,plain,
! [X0] :
( ~ r1(sK16(X0))
| r1(sK14(X0)) ),
inference(resolution,[],[f51,f81]) ).
fof(f146,plain,
! [X0] : r1(sK14(X0)),
inference(forward_subsumption_resolution,[],[f144,f80]) ).
fof(f299,plain,
! [X0,X1] : id(sK8(X0,X1),sK9(X0,X1)),
inference(resolution,[],[f75,f48]) ).
fof(f417,plain,
! [X2,X3,X0,X1] :
( ~ id(sK9(X1,X2),X3)
| ~ r1(X1)
| ~ r1(X0)
| ~ r2(X0,sK10(X1,X2))
| ~ r1(X3) ),
inference(resolution,[],[f73,f89]) ).
fof(f419,plain,
! [X2,X0,X1] :
( ~ r2(X1,sK10(X0,X2))
| ~ r1(X1)
| ~ r1(X0)
| ~ r1(sK8(X0,X2)) ),
inference(resolution,[],[f417,f75]) ).
fof(f513,plain,
! [X0,X1] : id(sK8(X0,X1),sK2(sK11(X0,X1),X0)),
inference(resolution,[],[f42,f72]) ).
fof(f592,plain,
! [X0,X1] : id(sK11(X0,X1),sK3(X0,X1)),
inference(resolution,[],[f46,f71]) ).
fof(f600,plain,
! [X0,X1] :
( ~ r1(sK3(X0,X1))
| r1(sK11(X0,X1)) ),
inference(resolution,[],[f592,f51]) ).
fof(f668,plain,
! [X0,X1] :
( ~ id(X0,sK12(X1))
| id(X0,X1) ),
inference(resolution,[],[f49,f79]) ).
fof(f747,plain,
! [X0,X1] :
( ~ id(X0,X1)
| id(X0,sK19(X1))
| id(X1,sK17(X1)) ),
inference(resolution,[],[f49,f87]) ).
fof(f748,plain,
! [X0,X1] :
( ~ id(X0,X1)
| id(X0,sK19(X1))
| r1(sK17(X1)) ),
inference(resolution,[],[f49,f85]) ).
fof(f774,plain,
! [X0] : id(sK12(sK12(X0)),X0),
inference(resolution,[],[f668,f79]) ).
fof(f779,plain,
! [X0] :
( ~ r1(X0)
| r1(sK12(sK12(X0))) ),
inference(resolution,[],[f774,f51]) ).
fof(f1042,plain,
! [X2,X3,X0,X1] :
( ~ id(X0,sK10(X1,X2))
| ~ id(X3,X2)
| r2(X3,X0) ),
inference(resolution,[],[f55,f74]) ).
fof(f1359,plain,
! [X2,X3,X0,X1] :
( ~ id(X2,sK12(X1))
| ~ id(X0,sK13(X1))
| ~ id(X3,X1)
| r3(X3,X0,X2) ),
inference(resolution,[],[f59,f77]) ).
fof(f1456,plain,
! [X2,X3,X0,X1] :
( ~ id(sK12(X0),X2)
| ~ id(sK13(X0),X1)
| ~ id(X0,X3)
| r3(X3,X1,X2) ),
inference(resolution,[],[f60,f77]) ).
fof(f1563,plain,
! [X2,X3,X0,X1] :
( ~ id(X2,sK14(X1))
| ~ id(X0,sK15(X1))
| ~ id(X3,X1)
| r4(X3,X0,X2) ),
inference(resolution,[],[f63,f82]) ).
fof(f1659,plain,
! [X2,X3,X0,X1] :
( ~ id(sK14(X0),X2)
| ~ id(sK15(X0),X1)
| ~ id(X0,X3)
| r4(X3,X1,X2) ),
inference(resolution,[],[f64,f82]) ).
fof(f2499,plain,
! [X2,X0,X1] :
( ~ id(X0,sK8(X1,X2))
| id(X0,sK2(sK11(X1,X2),X1)) ),
inference(resolution,[],[f513,f49]) ).
fof(f2967,plain,
! [X0,X1] :
( id(sK8(X0,X1),sK19(sK9(X0,X1)))
| r1(sK17(sK9(X0,X1))) ),
inference(resolution,[],[f748,f299]) ).
fof(f3633,plain,
! [X0,X1] :
( id(sK9(X0,X1),sK17(sK9(X0,X1)))
| id(sK8(X0,X1),sK19(sK9(X0,X1))) ),
inference(resolution,[],[f747,f299]) ).
fof(f4335,plain,
! [X2,X0,X1] :
( ~ id(X0,X1)
| r2(X0,sK10(X2,X1)) ),
inference(resolution,[],[f1042,f47]) ).
fof(f6840,plain,
! [X2,X0,X1] :
( ~ id(X0,sK13(X1))
| ~ id(X2,X1)
| r3(X2,X0,X1) ),
inference(resolution,[],[f1359,f101]) ).
fof(f7272,plain,
! [X2,X0,X1] :
( ~ id(sK13(X0),X1)
| ~ id(X0,X2)
| r3(X2,X1,X0) ),
inference(resolution,[],[f1456,f79]) ).
fof(f7772,plain,
! [X2,X0,X1] :
( ~ id(X0,sK15(X1))
| ~ id(X2,X1)
| r4(X2,X0,sK16(X1)) ),
inference(resolution,[],[f1563,f105]) ).
fof(f8096,plain,
! [X2,X0,X1] :
( ~ id(sK15(X0),X1)
| ~ id(X0,X2)
| r4(X2,X1,sK14(X0)) ),
inference(resolution,[],[f1659,f47]) ).
fof(f11393,plain,
! [X0,X1] : r2(sK12(sK12(X0)),sK10(X1,X0)),
inference(resolution,[],[f4335,f774]) ).
fof(f11445,plain,
! [X0,X1] : r2(sK16(X0),sK10(X1,sK0)),
inference(resolution,[],[f4335,f96]) ).
fof(f12582,plain,
! [X0,X1] :
( ~ r1(sK8(X1,X0))
| ~ r1(X1)
| ~ r1(sK12(sK12(X0))) ),
inference(resolution,[],[f11393,f419]) ).
fof(f28843,plain,
! [X0,X1] :
( ~ id(X0,X1)
| r3(X0,sK0,X1) ),
inference(resolution,[],[f6840,f102]) ).
fof(f29034,plain,
! [X0,X1] :
( ~ id(X0,X1)
| r3(X1,sK0,X0) ),
inference(resolution,[],[f7272,f94]) ).
fof(f36810,plain,
! [X0,X1] :
( ~ id(X0,X1)
| r4(X0,sK0,sK16(X1)) ),
inference(resolution,[],[f7772,f103]) ).
fof(f39725,plain,
! [X0,X1] :
( ~ id(X0,X1)
| r4(X1,sK0,sK14(X0)) ),
inference(resolution,[],[f8096,f95]) ).
fof(f69974,plain,
! [X2,X0,X1] :
( id(sK8(X0,X1),sK19(sK9(X0,X1)))
| ~ r1(X0)
| ~ r1(X2)
| ~ r2(X2,sK10(X0,X1))
| ~ r1(sK17(sK9(X0,X1))) ),
inference(resolution,[],[f3633,f417]) ).
fof(f70007,plain,
! [X2,X0,X1] :
( ~ r2(X2,sK10(X0,X1))
| ~ r1(X0)
| ~ r1(X2)
| id(sK8(X0,X1),sK19(sK9(X0,X1))) ),
inference(forward_subsumption_resolution,[],[f69974,f2967]) ).
fof(f110693,plain,
! [X0,X1] :
( ~ r1(X0)
| ~ r1(sK16(X1))
| id(sK8(X0,sK0),sK19(sK9(X0,sK0))) ),
inference(resolution,[],[f70007,f11445]) ).
fof(f110759,plain,
! [X0] :
( ~ r1(X0)
| id(sK8(X0,sK0),sK19(sK9(X0,sK0))) ),
inference(forward_subsumption_resolution,[],[f110693,f80]) ).
fof(f110807,plain,
id(sK8(sK0,sK0),sK19(sK9(sK0,sK0))),
inference(resolution,[],[f110759,f90]) ).
fof(f111069,plain,
id(sK19(sK9(sK0,sK0)),sK8(sK0,sK0)),
inference(resolution,[],[f110807,f48]) ).
fof(f111071,plain,
( ~ r1(sK19(sK9(sK0,sK0)))
| r1(sK8(sK0,sK0)) ),
inference(resolution,[],[f110807,f51]) ).
fof(f111124,plain,
id(sK19(sK9(sK0,sK0)),sK2(sK11(sK0,sK0),sK0)),
inference(resolution,[],[f111069,f2499]) ).
fof(f111290,definition,
( spl20_38
<=> r1(sK8(sK0,sK0)) ),
introduced(definition,[new_symbols(definition,[spl20_38])],[avatar_definition]) ).
fof(f111291,plain,
( r1(sK8(sK0,sK0))
| ~ spl20_38 ),
inference(avatar_component_clause,[],[f111290]) ).
fof(f111292,plain,
( ~ r1(sK8(sK0,sK0))
| spl20_38 ),
inference(avatar_component_clause,[],[f111290]) ).
fof(f111294,plain,
( ~ r1(sK19(sK9(sK0,sK0)))
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f111071,f111292]) ).
fof(f112990,plain,
( ~ r1(sK2(sK11(sK0,sK0),sK0))
| r1(sK19(sK9(sK0,sK0))) ),
inference(resolution,[],[f111124,f51]) ).
fof(f113031,plain,
( ~ r1(sK2(sK11(sK0,sK0),sK0))
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f112990,f111294]) ).
fof(f171896,plain,
r4(sK8(sK0,sK0),sK0,sK16(sK19(sK9(sK0,sK0)))),
inference(resolution,[],[f36810,f110807]) ).
fof(f172046,plain,
id(sK16(sK19(sK9(sK0,sK0))),sK3(sK8(sK0,sK0),sK0)),
inference(resolution,[],[f171896,f46]) ).
fof(f172081,plain,
( ~ r1(sK16(sK19(sK9(sK0,sK0))))
| r1(sK3(sK8(sK0,sK0),sK0)) ),
inference(resolution,[],[f172046,f52]) ).
fof(f172130,plain,
r1(sK3(sK8(sK0,sK0),sK0)),
inference(forward_subsumption_resolution,[],[f172081,f80]) ).
fof(f172133,plain,
id(sK3(sK8(sK0,sK0),sK0),sK0),
inference(resolution,[],[f172130,f34]) ).
fof(f172253,plain,
r3(sK0,sK0,sK3(sK8(sK0,sK0),sK0)),
inference(resolution,[],[f172133,f29034]) ).
fof(f177707,plain,
id(sK3(sK8(sK0,sK0),sK0),sK2(sK0,sK0)),
inference(resolution,[],[f172253,f42]) ).
fof(f184085,plain,
( ~ r1(sK3(sK8(sK0,sK0),sK0))
| r1(sK2(sK0,sK0)) ),
inference(resolution,[],[f177707,f52]) ).
fof(f184137,plain,
r1(sK2(sK0,sK0)),
inference(forward_subsumption_resolution,[],[f184085,f172130]) ).
fof(f184139,plain,
id(sK2(sK0,sK0),sK0),
inference(resolution,[],[f184137,f34]) ).
fof(f184262,plain,
r4(sK0,sK0,sK14(sK2(sK0,sK0))),
inference(resolution,[],[f184139,f39725]) ).
fof(f187599,plain,
id(sK14(sK2(sK0,sK0)),sK3(sK0,sK0)),
inference(resolution,[],[f184262,f46]) ).
fof(f201763,plain,
( ~ r1(sK14(sK2(sK0,sK0)))
| r1(sK3(sK0,sK0)) ),
inference(resolution,[],[f187599,f52]) ).
fof(f201815,plain,
r1(sK3(sK0,sK0)),
inference(forward_subsumption_resolution,[],[f201763,f146]) ).
fof(f201831,plain,
r1(sK11(sK0,sK0)),
inference(resolution,[],[f201815,f600]) ).
fof(f201866,plain,
id(sK11(sK0,sK0),sK0),
inference(resolution,[],[f201831,f34]) ).
fof(f202085,plain,
r3(sK11(sK0,sK0),sK0,sK0),
inference(resolution,[],[f201866,f28843]) ).
fof(f203434,plain,
id(sK0,sK2(sK11(sK0,sK0),sK0)),
inference(resolution,[],[f202085,f42]) ).
fof(f208314,plain,
( ~ r1(sK0)
| r1(sK2(sK11(sK0,sK0),sK0)) ),
inference(resolution,[],[f203434,f52]) ).
fof(f208366,plain,
r1(sK2(sK11(sK0,sK0),sK0)),
inference(forward_subsumption_resolution,[],[f208314,f90]) ).
fof(f208367,plain,
( $false
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f208366,f113031]) ).
fof(f208368,plain,
spl20_38,
inference(avatar_contradiction_clause,[],[f208367]) ).
fof(f208405,plain,
( ~ r1(sK0)
| ~ r1(sK12(sK12(sK0)))
| ~ spl20_38 ),
inference(resolution,[],[f111291,f12582]) ).
fof(f208444,plain,
( ~ r1(sK0)
| ~ spl20_38 ),
inference(forward_subsumption_resolution,[],[f208405,f779]) ).
fof(f208449,plain,
( $false
| ~ spl20_38 ),
inference(forward_subsumption_resolution,[],[f208444,f90]) ).
fof(f208450,plain,
~ spl20_38,
inference(avatar_contradiction_clause,[],[f208449]) ).
cnf(s87,plain,
spl20_38,
inference(sat_conversion,[],[f208368]) ).
cnf(s91,plain,
~ spl20_38,
inference(sat_conversion,[],[f208450]) ).
cnf(s92,plain,
$false,
inference(rat,[],[s87,s91]) ).
fof(f208451,plain,
$false,
inference(avatar_sat_refutation,[],[s92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN086+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n014.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 21:59:17 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/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
% 14.66/2.51 % (1211831)Will run a generic schedule for satisfiability detection.
% 14.66/2.51 % (1211842)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=815839578:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.66/2.51 % (1211837)% WARNING: option uhcvi not known.
% 14.66/2.51 % (1211839)dis+10_1_sil=32000:sp=arity:random_seed=359970356:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.66/2.51 % (1211836)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3069578435_2999 on theBenchmark for (2999ds/0Mi)
% 14.66/2.51 % (1211837)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4131226395:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.66/2.51 % (1211838)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1941947583:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.66/2.51 % (1211840)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3513501211:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.66/2.51 % (1211841)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2015114720:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.66/2.51 % TRYING [1]
% 14.66/2.51 % TRYING [2]
% 14.66/2.51 % TRYING [3]
% 14.66/2.51 % TRYING [4]
% 14.66/2.51 % TRYING [5]
% 14.66/2.51 % TRYING [6]
% 14.66/2.51 % (1211842)Instruction limit reached!
% 14.66/2.51 % (1211842)------------------------------
% 14.66/2.51 % (1211842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.66/2.51 % (1211842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.66/2.51 % (1211842)CaDiCaL version: 2.1.3
% 14.66/2.51 % (1211842)Termination reason: Instruction limit
% 14.66/2.51 % (1211842)Termination phase: Saturation
% 14.66/2.51 % (1211842)Time elapsed: 0.049 s
% 14.66/2.51 % (1211842)Peak memory usage: 14 MB
% 14.66/2.51 % (1211842)Instructions burned: 160 (million)
% 14.66/2.51 % (1211850)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2601116330:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.66/2.51 % TRYING [1]
% 14.66/2.51 % TRYING [2]
% 14.66/2.51 % TRYING [3]
% 14.66/2.51 % (1211840)Instruction limit reached!
% 14.66/2.51 % (1211840)------------------------------
% 14.66/2.51 % (1211840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.66/2.51 % (1211840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.66/2.51 % (1211840)CaDiCaL version: 2.1.3
% 14.66/2.51 % (1211840)Termination reason: Instruction limit
% 14.66/2.51 % (1211840)Termination phase: Saturation
% 14.66/2.51 % (1211840)Time elapsed: 0.061 s
% 14.66/2.51 % (1211840)Peak memory usage: 12 MB
% 14.66/2.51 % (1211840)Instructions burned: 117 (million)
% 14.66/2.51 % TRYING [4]
% 14.66/2.51 % (1211839)Instruction limit reached!
% 14.66/2.51 % (1211839)------------------------------
% 14.66/2.51 % (1211839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.66/2.51 % (1211839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.66/2.51 % (1211839)CaDiCaL version: 2.1.3
% 14.66/2.51 % (1211839)Termination reason: Instruction limit
% 14.66/2.51 % (1211839)Termination phase: Saturation
% 14.66/2.51 % (1211839)Time elapsed: 0.064 s
% 14.66/2.51 % (1211839)Peak memory usage: 12 MB
% 14.66/2.51 % (1211839)Instructions burned: 104 (million)
% 14.66/2.51 % (1211841)Instruction limit reached!
% 14.66/2.51 % (1211841)------------------------------
% 14.66/2.51 % (1211841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.66/2.51 % (1211841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.66/2.51 % (1211841)CaDiCaL version: 2.1.3
% 14.66/2.51 % (1211841)Termination reason: Instruction limit
% 14.66/2.51 % (1211841)Termination phase: Saturation
% 14.66/2.51 % (1211841)Time elapsed: 0.072 s
% 14.66/2.51 % (1211841)Peak memory usage: 13 MB
% 14.66/2.51 % (1211841)Instructions burned: 133 (million)
% 14.66/2.51 % TRYING [7]
% 14.66/2.51 % (1211852)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1435759711:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.66/2.51 % (1211853)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=1565174332:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 14.66/2.51 % TRYING [5]
% 14.66/2.51 % (1211854)ott-21_1_sil=16000:fs=off:random_seed=3595779472:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.66/2.51 % (1211852)Instruction limit reached!
% 14.66/2.51 % (1211852)------------------------------
% 14.66/2.51 % (1211852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211852)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211852)Termination reason: Instruction limit
% 48.71/7.36 % (1211852)Termination phase: Saturation
% 48.71/7.36 % (1211852)Time elapsed: 0.071 s
% 48.71/7.36 % (1211852)Peak memory usage: 13 MB
% 48.71/7.36 % (1211852)Instructions burned: 131 (million)
% 48.71/7.36 % TRYING [8]
% 48.71/7.36 % (1211858)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1793699151:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 48.71/7.36 % TRYING [6]
% 48.71/7.36 % (1211854)Instruction limit reached!
% 48.71/7.36 % (1211854)------------------------------
% 48.71/7.36 % (1211854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211854)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211854)Termination reason: Instruction limit
% 48.71/7.36 % (1211854)Termination phase: Saturation
% 48.71/7.36 % (1211854)Time elapsed: 0.098 s
% 48.71/7.36 % (1211854)Peak memory usage: 13 MB
% 48.71/7.36 % (1211854)Instructions burned: 181 (million)
% 48.71/7.36 % (1211850)Instruction limit reached!
% 48.71/7.36 % (1211850)------------------------------
% 48.71/7.36 % (1211850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211850)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211850)Termination reason: Instruction limit
% 48.71/7.36 % (1211850)Termination phase: Finite model building constraint generation
% 48.71/7.36 % (1211850)Time elapsed: 0.150 s
% 48.71/7.36 % (1211850)Peak memory usage: 40 MB
% 48.71/7.36 % (1211850)Instructions burned: 719 (million)
% 48.71/7.36 % (1211860)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3284990629:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 48.71/7.36 % TRYING [1]
% 48.71/7.36 % TRYING [2]
% 48.71/7.36 % TRYING [3]
% 48.71/7.36 % (1211861)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2601530679:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 48.71/7.36 % TRYING [4]
% 48.71/7.36 % TRYING [5]
% 48.71/7.36 % TRYING [6]
% 48.71/7.36 % TRYING [9]
% 48.71/7.36 % TRYING [7]
% 48.71/7.36 % TRYING [10]
% 48.71/7.36 % TRYING [8]
% 48.71/7.36 % (1211858)Instruction limit reached!
% 48.71/7.36 % (1211858)------------------------------
% 48.71/7.36 % (1211858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211858)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211858)Termination reason: Instruction limit
% 48.71/7.36 % (1211858)Termination phase: Saturation
% 48.71/7.36 % (1211858)Time elapsed: 0.305 s
% 48.71/7.36 % (1211858)Peak memory usage: 15 MB
% 48.71/7.36 % (1211858)Instructions burned: 478 (million)
% 48.71/7.36 % (1211853)Instruction limit reached!
% 48.71/7.36 % (1211853)------------------------------
% 48.71/7.36 % (1211853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211853)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211853)Termination reason: Instruction limit
% 48.71/7.36 % (1211853)Termination phase: Saturation
% 48.71/7.36 % (1211853)Time elapsed: 0.405 s
% 48.71/7.36 % (1211853)Peak memory usage: 19 MB
% 48.71/7.36 % (1211853)Instructions burned: 685 (million)
% 48.71/7.36 % (1211864)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2679750896:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 48.71/7.36 % (1211860)Instruction limit reached!
% 48.71/7.36 % (1211860)------------------------------
% 48.71/7.36 % (1211860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.71/7.36 % (1211860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.71/7.36 % (1211860)CaDiCaL version: 2.1.3
% 48.71/7.36 % (1211860)Termination reason: Instruction limit
% 48.71/7.36 % (1211860)Termination phase: Finite model building constraint generation
% 48.71/7.36 % (1211860)Time elapsed: 0.295 s
% 48.71/7.36 % (1211860)Peak memory usage: 20 MB
% 48.71/7.36 % (1211860)Instructions burned: 865 (million)
% 48.71/7.36 % (1211865)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=1400996755: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)
% 48.71/7.36 % (1211868)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1758757975:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 79.92/11.73 % TRYING [14]
% 79.92/11.73 % (1211861)Instruction limit reached!
% 79.92/11.73 % (1211861)------------------------------
% 79.92/11.73 % (1211861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211861)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211861)Termination reason: Instruction limit
% 79.92/11.73 % (1211861)Termination phase: Saturation
% 79.92/11.73 % (1211861)Time elapsed: 0.373 s
% 79.92/11.73 % (1211861)Peak memory usage: 20 MB
% 79.92/11.73 % (1211861)Instructions burned: 1181 (million)
% 79.92/11.73 % (1211870)fmb+10_1_sil=64000:random_seed=1900814627:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 79.92/11.73 % TRYING [1]
% 79.92/11.73 % TRYING [2]
% 79.92/11.73 % TRYING [3]
% 79.92/11.73 % TRYING [4]
% 79.92/11.73 % TRYING [5]
% 79.92/11.73 % TRYING [6]
% 79.92/11.73 % TRYING [11]
% 79.92/11.73 % (1211864)Instruction limit reached!
% 79.92/11.73 % (1211864)------------------------------
% 79.92/11.73 % (1211864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211864)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211864)Termination reason: Instruction limit
% 79.92/11.73 % (1211864)Termination phase: Finite model building constraint generation
% 79.92/11.73 % (1211864)Time elapsed: 0.320 s
% 79.92/11.73 % (1211864)Peak memory usage: 67 MB
% 79.92/11.73 % (1211864)Instructions burned: 890 (million)
% 79.92/11.73 % (1211872)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4097454526:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 79.92/11.73 % TRYING [20]
% 79.92/11.73 % (1211865)Instruction limit reached!
% 79.92/11.73 % (1211865)------------------------------
% 79.92/11.73 % (1211865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211865)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211865)Termination reason: Instruction limit
% 79.92/11.73 % (1211865)Termination phase: Saturation
% 79.92/11.73 % (1211865)Time elapsed: 0.451 s
% 79.92/11.73 % (1211865)Peak memory usage: 20 MB
% 79.92/11.73 % (1211865)Instructions burned: 692 (million)
% 79.92/11.73 % (1211874)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2932859638:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 79.92/11.73 % TRYING [8]
% 79.92/11.73 % (1211868)Instruction limit reached!
% 79.92/11.73 % (1211868)------------------------------
% 79.92/11.73 % (1211868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211868)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211868)Termination reason: Instruction limit
% 79.92/11.73 % (1211868)Termination phase: Saturation
% 79.92/11.73 % (1211868)Time elapsed: 0.475 s
% 79.92/11.73 % (1211868)Peak memory usage: 16 MB
% 79.92/11.73 % (1211868)Instructions burned: 880 (million)
% 79.92/11.73 % (1211876)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2075603157:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 79.92/11.73 % TRYING [7]
% 79.92/11.73 % TRYING [9]
% 79.92/11.73 % TRYING [12]
% 79.92/11.73 % TRYING [10]
% 79.92/11.73 % (1211874)Instruction limit reached!
% 79.92/11.73 % (1211874)------------------------------
% 79.92/11.73 % (1211874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211874)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211874)Termination reason: Instruction limit
% 79.92/11.73 % (1211874)Termination phase: Finite model building constraint generation
% 79.92/11.73 % (1211874)Time elapsed: 0.338 s
% 79.92/11.73 % (1211874)Peak memory usage: 44 MB
% 79.92/11.73 % (1211874)Instructions burned: 922 (million)
% 79.92/11.73 % (1211878)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1153810154:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 79.92/11.73 % TRYING [13]
% 79.92/11.73 % TRYING [8]
% 79.92/11.73 % (1211878)Instruction limit reached!
% 79.92/11.73 % (1211878)------------------------------
% 79.92/11.73 % (1211878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.92/11.73 % (1211878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.92/11.73 % (1211878)CaDiCaL version: 2.1.3
% 79.92/11.73 % (1211878)Termination reason: Instruction limit
% 79.92/11.73 % (1211878)Termination phase: Saturation
% 79.92/11.73 % (1211878)Time elapsed: 0.708 s
% 79.92/11.73 % (1211878)Peak memory usage: 26 MB
% 154.53/25.04 % (1211878)Instructions burned: 1473 (million)
% 154.53/25.04 % (1211880)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3322160085:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 154.53/25.04 % TRYING [77]
% 154.53/25.04 % TRYING [14]
% 154.53/25.04 % TRYING [15]
% 154.53/25.04 % (1211876)Instruction limit reached!
% 154.53/25.04 % (1211876)------------------------------
% 154.53/25.04 % (1211876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.53/25.04 % (1211876)CaDiCaL version: 2.1.3
% 154.53/25.04 % (1211876)Termination reason: Instruction limit
% 154.53/25.04 % (1211876)Termination phase: Saturation
% 154.53/25.04 % (1211876)Time elapsed: 2.738 s
% 154.53/25.04 % (1211876)Peak memory usage: 22 MB
% 154.53/25.04 % (1211876)Instructions burned: 5132 (million)
% 154.53/25.04 % (1211882)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1397655096:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 154.53/25.04 % TRYING [16]
% 154.53/25.04 % TRYING [9]
% 154.53/25.04 % (1211880)Instruction limit reached!
% 154.53/25.04 % (1211880)------------------------------
% 154.53/25.04 % (1211880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.53/25.04 % (1211880)CaDiCaL version: 2.1.3
% 154.53/25.04 % (1211880)Termination reason: Instruction limit
% 154.53/25.04 % (1211880)Termination phase: Finite model building constraint generation
% 154.53/25.04 % (1211880)Time elapsed: 2.191 s
% 154.53/25.04 % (1211880)Peak memory usage: 416 MB
% 154.53/25.04 % (1211880)Instructions burned: 6325 (million)
% 154.53/25.04 % (1211884)ott-2_1_sil=16000:newcnf=on:random_seed=829779047:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 154.53/25.04 % (1211882)Instruction limit reached!
% 154.53/25.04 % (1211882)------------------------------
% 154.53/25.04 % (1211882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.53/25.04 % (1211882)CaDiCaL version: 2.1.3
% 154.53/25.04 % (1211882)Termination reason: Instruction limit
% 154.53/25.04 % (1211882)Termination phase: Finite model building constraint generation
% 154.53/25.04 % (1211882)Time elapsed: 0.857 s
% 154.53/25.04 % (1211882)Peak memory usage: 164 MB
% 154.53/25.04 % (1211882)Instructions burned: 2177 (million)
% 154.53/25.04 % (1211886)ott+10_1_sil=32000:tgt=ground:random_seed=1478272816:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 154.53/25.04 % (1211884)Instruction limit reached!
% 154.53/25.04 % (1211884)------------------------------
% 154.53/25.04 % (1211884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.53/25.04 % (1211884)CaDiCaL version: 2.1.3
% 154.53/25.04 % (1211884)Termination reason: Instruction limit
% 154.53/25.04 % (1211884)Termination phase: Saturation
% 154.53/25.04 % (1211884)Time elapsed: 0.508 s
% 154.53/25.04 % (1211884)Peak memory usage: 15 MB
% 154.53/25.04 % (1211884)Instructions burned: 869 (million)
% 154.53/25.04 % (1211888)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3417712905:i=54282_2951 on theBenchmark for (2951ds/54282Mi)
% 154.53/25.04 % TRYING [1]
% 154.53/25.04 % TRYING [2]
% 154.53/25.04 % TRYING [3]
% 154.53/25.04 % TRYING [4]
% 154.53/25.04 % TRYING [5]
% 154.53/25.04 % TRYING [6]
% 154.53/25.04 % (1211872)Instruction limit reached!
% 154.53/25.04 % (1211872)------------------------------
% 154.53/25.04 % (1211872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.53/25.04 % (1211872)CaDiCaL version: 2.1.3
% 154.53/25.04 % (1211872)Termination reason: Instruction limit
% 154.53/25.04 % (1211872)Termination phase: Finite model building constraint generation
% 154.53/25.04 % (1211872)Time elapsed: 4.072 s
% 154.53/25.04 % (1211872)Peak memory usage: 627 MB
% 154.53/25.04 % (1211872)Instructions burned: 9517 (million)
% 154.53/25.04 % TRYING [7]
% 154.53/25.04 % (1211890)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=422081389:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 154.53/25.04 % TRYING [8]
% 154.53/25.04 % TRYING [16]
% 154.53/25.04 % TRYING [9]
% 154.53/25.04 % TRYING [10]
% 154.53/25.04 % TRYING [11]
% 154.53/25.04 % TRYING [12]
% 154.53/25.04 % TRYING [13]
% 154.53/25.04 % TRYING [17]
% 154.53/25.04 % (1211890)Instruction limit reached!
% 154.53/25.04 % (1211890)------------------------------
% 154.53/25.04 % (1211890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.53/25.04 % (1211890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.66/38.50 % (1211890)CaDiCaL version: 2.1.3
% 149.66/38.50 % (1211890)Termination reason: Instruction limit
% 149.66/38.50 % (1211890)Termination phase: Saturation
% 149.66/38.50 % (1211890)Time elapsed: 1.889 s
% 149.66/38.50 % (1211890)Peak memory usage: 21 MB
% 149.66/38.50 % (1211890)Instructions burned: 3512 (million)
% 149.66/38.50 % (1211892)dis+21_1_sil=32000:sas=cadical:random_seed=3605035940:i=3773:amm=off_2930 on theBenchmark for (2930ds/3773Mi)
% 149.66/38.50 % TRYING [14]
% 149.66/38.50 % (1211870)Instruction limit reached!
% 149.66/38.50 % (1211870)------------------------------
% 149.66/38.50 % (1211870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.66/38.50 % (1211870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.66/38.50 % (1211870)CaDiCaL version: 2.1.3
% 149.66/38.50 % (1211870)Termination reason: Instruction limit
% 149.66/38.50 % (1211870)Termination phase: Finite model building constraint generation
% 149.66/38.50 % (1211870)Time elapsed: 7.064 s
% 149.66/38.50 % (1211870)Peak memory usage: 534 MB
% 149.66/38.50 % (1211870)Instructions burned: 22063 (million)
% 149.66/38.50 % (1211894)ott+11_1_sil=16000:gs=on:random_seed=3997822209:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2922 on theBenchmark for (2922ds/2251Mi)
% 149.66/38.50 % (1211886)Instruction limit reached!
% 149.66/38.50 % (1211886)------------------------------
% 149.66/38.50 % (1211886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.66/38.50 % (1211886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.66/38.50 % (1211886)CaDiCaL version: 2.1.3
% 149.66/38.50 % (1211886)Termination reason: Instruction limit
% 149.66/38.50 % (1211886)Termination phase: Saturation
% 149.66/38.50 % (1211886)Time elapsed: 3.303 s
% 149.66/38.50 % (1211886)Peak memory usage: 39 MB
% 149.66/38.50 % (1211886)Instructions burned: 5114 (million)
% 149.66/38.50 % (1211896)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1542566743:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 149.66/38.50 % TRYING [7]
% 149.66/38.50 % TRYING [8]
% 149.66/38.50 % TRYING [9]
% 149.66/38.50 % TRYING [15]
% 149.66/38.50 % (1211894)Instruction limit reached!
% 149.66/38.50 % (1211894)------------------------------
% 149.66/38.50 % (1211894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.66/38.50 % (1211894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.66/38.50 % (1211894)CaDiCaL version: 2.1.3
% 149.66/38.50 % (1211894)Termination reason: Instruction limit
% 149.66/38.50 % (1211894)Termination phase: Saturation
% 149.66/38.50 % (1211894)Time elapsed: 0.796 s
% 149.66/38.50 % (1211894)Peak memory usage: 53 MB
% 149.66/38.50 % (1211894)Instructions burned: 2252 (million)
% 149.66/38.50 % (1211898)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1217541686:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2914 on theBenchmark for (2914ds/4591Mi)
% 149.66/38.50 % TRYING [10]
% 149.66/38.50 % TRYING [11]
% 149.66/38.50 % TRYING [18]
% 149.66/38.50 % (1211892)Instruction limit reached!
% 149.66/38.50 % (1211892)------------------------------
% 149.66/38.50 % (1211892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.66/38.50 % (1211892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.66/38.50 % (1211892)CaDiCaL version: 2.1.3
% 149.66/38.50 % (1211892)Termination reason: Instruction limit
% 149.66/38.50 % (1211892)Termination phase: Saturation
% 149.66/38.50 % (1211892)Time elapsed: 2.365 s
% 149.66/38.50 % (1211892)Peak memory usage: 37 MB
% 268.94/38.50 % (1211892)Instructions burned: 3774 (million)
% 268.94/38.50 % (1211900)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2551073617:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 268.94/38.50 % TRYING [12]
% 268.94/38.50 % (1211898)Instruction limit reached!
% 268.94/38.50 % (1211898)------------------------------
% 268.94/38.50 % (1211898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211898)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211898)Termination reason: Instruction limit
% 268.94/38.50 % (1211898)Termination phase: Saturation
% 268.94/38.50 % (1211898)Time elapsed: 1.331 s
% 268.94/38.50 % (1211898)Peak memory usage: 38 MB
% 268.94/38.50 % (1211898)Instructions burned: 4594 (million)
% 268.94/38.50 % (1211902)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2429950028:i=5211_2901 on theBenchmark for (2901ds/5211Mi)
% 268.94/38.50 % TRYING [16]
% 268.94/38.50 % TRYING [13]
% 268.94/38.50 % (1211902)Instruction limit reached!
% 268.94/38.50 % (1211902)------------------------------
% 268.94/38.50 % (1211902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211902)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211902)Termination reason: Instruction limit
% 268.94/38.50 % (1211902)Termination phase: Saturation
% 268.94/38.50 % (1211902)Time elapsed: 1.396 s
% 268.94/38.50 % (1211902)Peak memory usage: 25 MB
% 268.94/38.50 % (1211902)Instructions burned: 5214 (million)
% 268.94/38.50 % (1211904)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2036942760:i=5497:nm=2_2886 on theBenchmark for (2886ds/5497Mi)
% 268.94/38.50 % TRYING [17]
% 268.94/38.50 % TRYING [14]
% 268.94/38.50 % TRYING [17]
% 268.94/38.50 % TRYING [19]
% 268.94/38.50 % (1211904)Instruction limit reached!
% 268.94/38.50 % (1211904)------------------------------
% 268.94/38.50 % (1211904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211904)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211904)Termination reason: Instruction limit
% 268.94/38.50 % (1211904)Termination phase: Finite model building constraint generation
% 268.94/38.50 % (1211904)Time elapsed: 0.998 s
% 268.94/38.50 % (1211904)Peak memory usage: 301 MB
% 268.94/38.50 % (1211904)Instructions burned: 5498 (million)
% 268.94/38.50 % (1211906)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2415834748:fmbsr=2:i=46332_2876 on theBenchmark for (2876ds/46332Mi)
% 268.94/38.50 % TRYING [15]
% 268.94/38.50 % TRYING [16]
% 268.94/38.50 % TRYING [15]
% 268.94/38.50 % TRYING [17]
% 268.94/38.50 % TRYING [18]
% 268.94/38.50 % TRYING [18]
% 268.94/38.50 % TRYING [16]
% 268.94/38.50 % TRYING [20]
% 268.94/38.50 % TRYING [19]
% 268.94/38.50 % TRYING [19]
% 268.94/38.50 % TRYING [20]
% 268.94/38.50 % TRYING [17]
% 268.94/38.50 % TRYING [21]
% 268.94/38.50 % TRYING [21]
% 268.94/38.50 % TRYING [20]
% 268.94/38.50 % (1211906)Instruction limit reached!
% 268.94/38.50 % (1211906)------------------------------
% 268.94/38.50 % (1211906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211906)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211906)Termination reason: Instruction limit
% 268.94/38.50 % (1211906)Termination phase: Finite model building constraint generation
% 268.94/38.50 % (1211906)Time elapsed: 8.852 s
% 268.94/38.50 % (1211906)Peak memory usage: 528 MB
% 268.94/38.50 % (1211906)Instructions burned: 46334 (million)
% 268.94/38.50 % (1211908)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2182565684:i=14071_2787 on theBenchmark for (2787ds/14071Mi)
% 268.94/38.50 % TRYING [12]
% 268.94/38.50 % TRYING [18]
% 268.94/38.50 % TRYING [13]
% 268.94/38.50 % TRYING [14]
% 268.94/38.50 % TRYING [15]
% 268.94/38.50 % TRYING [16]
% 268.94/38.50 % (1211908)Instruction limit reached!
% 268.94/38.50 % (1211908)------------------------------
% 268.94/38.50 % (1211908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211908)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211908)Termination reason: Instruction limit
% 268.94/38.50 % (1211908)Termination phase: Finite model building constraint generation
% 268.94/38.50 % (1211908)Time elapsed: 2.849 s
% 268.94/38.50 % (1211908)Peak memory usage: 248 MB
% 268.94/38.50 % (1211908)Instructions burned: 14074 (million)
% 268.94/38.50 % (1211910)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1024247082:i=22565:add=on:rawr=on_2758 on theBenchmark for (2758ds/22565Mi)
% 268.94/38.50 % (1211888)Instruction limit reached!
% 268.94/38.50 % (1211888)------------------------------
% 268.94/38.50 % (1211888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211888)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211888)Termination reason: Instruction limit
% 268.94/38.50 % (1211888)Termination phase: Finite model building constraint generation
% 268.94/38.50 % (1211888)Time elapsed: 19.610 s
% 268.94/38.50 % (1211888)Peak memory usage: 729 MB
% 268.94/38.50 % (1211888)Instructions burned: 54282 (million)
% 268.94/38.50 % (1211900)Instruction limit reached!
% 268.94/38.50 % (1211900)------------------------------
% 268.94/38.50 % (1211900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211900)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211900)Termination reason: Instruction limit
% 268.94/38.50 % (1211900)Termination phase: Saturation
% 268.94/38.50 % (1211900)Time elapsed: 15.186 s
% 268.94/38.50 % (1211900)Peak memory usage: 409 MB
% 268.94/38.50 % (1211900)Instructions burned: 29341 (million)
% 268.94/38.50 % (1211912)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=452493322:i=8173:av=off_2754 on theBenchmark for (2754ds/8173Mi)
% 268.94/38.50 % (1211913)dis+10_16:1_sil=16000:random_seed=2306053231:i=9155:fsr=off_2753 on theBenchmark for (2753ds/9155Mi)
% 268.94/38.50 % TRYING [22]
% 268.94/38.50 % TRYING [19]
% 268.94/38.50 % (1211913)Instruction limit reached!
% 268.94/38.50 % (1211913)------------------------------
% 268.94/38.50 % (1211913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211913)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211913)Termination reason: Instruction limit
% 268.94/38.50 % (1211913)Termination phase: Saturation
% 268.94/38.50 % (1211913)Time elapsed: 5.188 s
% 268.94/38.50 % (1211913)Peak memory usage: 50 MB
% 268.94/38.50 % (1211913)Instructions burned: 9155 (million)
% 268.94/38.50 % (1211916)ott-3_8_sil=64000:random_seed=1564754267:i=20139:bs=on_2701 on theBenchmark for (2701ds/20139Mi)
% 268.94/38.50 % (1211912)Instruction limit reached!
% 268.94/38.50 % (1211912)------------------------------
% 268.94/38.50 % (1211912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211912)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211912)Termination reason: Instruction limit
% 268.94/38.50 % (1211912)Termination phase: Saturation
% 268.94/38.50 % (1211912)Time elapsed: 5.521 s
% 268.94/38.50 % (1211912)Peak memory usage: 68 MB
% 268.94/38.50 % (1211912)Instructions burned: 8173 (million)
% 268.94/38.50 % (1211918)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=362219569:fmbsr=2:i=32576_2698 on theBenchmark for (2698ds/32576Mi)
% 268.94/38.50 % TRYING [9]
% 268.94/38.50 % TRYING [10]
% 268.94/38.50 % TRYING [11]
% 268.94/38.50 % TRYING [12]
% 268.94/38.50 % TRYING [23]
% 268.94/38.50 % TRYING [20]
% 268.94/38.50 % TRYING [13]
% 268.94/38.50 % (1211910)Instruction limit reached!
% 268.94/38.50 % (1211910)------------------------------
% 268.94/38.50 % (1211910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211910)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211910)Termination reason: Instruction limit
% 268.94/38.50 % (1211910)Termination phase: Saturation
% 268.94/38.50 % (1211910)Time elapsed: 7.514 s
% 268.94/38.50 % (1211910)Peak memory usage: 198 MB
% 268.94/38.50 % (1211910)Instructions burned: 22566 (million)
% 268.94/38.50 % (1211920)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2179806683:i=11404_2683 on theBenchmark for (2683ds/11404Mi)
% 268.94/38.50 % TRYING [14]
% 268.94/38.50 % TRYING [15]
% 268.94/38.50 % (1211896)Instruction limit reached!
% 268.94/38.50 % (1211896)------------------------------
% 268.94/38.50 % (1211896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211896)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211896)Termination reason: Instruction limit
% 268.94/38.50 % (1211896)Termination phase: Finite model building constraint generation
% 268.94/38.50 % (1211896)Time elapsed: 25.724 s
% 268.94/38.50 % (1211896)Peak memory usage: 394 MB
% 268.94/38.50 % (1211896)Instructions burned: 67536 (million)
% 268.94/38.50 % (1211922)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=897609778:i=14134_2661 on theBenchmark for (2661ds/14134Mi)
% 268.94/38.50 % TRYING [16]
% 268.94/38.50 % (1211920)Instruction limit reached!
% 268.94/38.50 % (1211920)------------------------------
% 268.94/38.50 % (1211920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211920)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211920)Termination reason: Instruction limit
% 268.94/38.50 % (1211920)Termination phase: Saturation
% 268.94/38.50 % (1211920)Time elapsed: 4.593 s
% 268.94/38.50 % (1211920)Peak memory usage: 149 MB
% 268.94/38.50 % (1211920)Instructions burned: 11407 (million)
% 268.94/38.50 % (1211924)dis+33_16_sil=32000:sac=on:random_seed=1428034058:i=15851:nm=0_2637 on theBenchmark for (2637ds/15851Mi)
% 268.94/38.50 % TRYING [17]
% 268.94/38.50 % (1211924) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1211831-1211924"...
% 268.94/38.50 % (1211924)...printing done.
% 268.94/38.50 % (1211924)Refutation found. Thanks to Tanya!
% 268.94/38.50 % SZS status Theorem for theBenchmark
% 268.94/38.50 % SZS output start Proof for theBenchmark
% See solution above
% 268.94/38.50 % (1211924)------------------------------
% 268.94/38.50 % (1211924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.94/38.50 % (1211924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.94/38.50 % (1211924)CaDiCaL version: 2.1.3
% 268.94/38.50 % (1211924)Termination reason: Refutation
% 268.94/38.50 % (1211924)Time elapsed: 1.562 s
% 268.94/38.50 % (1211924)Peak memory usage: 74 MB
% 268.94/38.50 % (1211924)Instructions burned: 4817 (million)
% 268.94/38.50 % (1211831)Success in time 38.073 s
% 268.94/38.50 % Vampire exiting
%------------------------------------------------------------------------------