%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL385-1 : TPTP v9.3.1. Released v2.3.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 11:58:31 AM UTC 2026
% Result : Unsatisfiable 254.86s 36.56s
% Output : Refutation 254.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 5
% Syntax : Number of formulae : 69 ( 49 unt; 0 def)
% Number of atoms : 90 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 43 ( 22 ~; 21 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 184 ( 184 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
fof(f3,axiom,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_2) ).
fof(f4,axiom,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
fof(f5,negated_conjecture,
~ is_a_theorem(implies(implies(x,not(y)),implies(y,not(x)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_47) ).
fof(f6,plain,
! [X0] :
( ~ is_a_theorem(implies(not(X0),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f1,f3]) ).
fof(f7,plain,
! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[],[f1,f4]) ).
fof(f34,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(implies(X1,X2),implies(X0,X2))) ),
inference(resolution,[],[f2,f1]) ).
fof(f36,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))),
inference(resolution,[],[f34,f3]) ).
fof(f37,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))),
inference(resolution,[],[f34,f2]) ).
fof(f38,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))),
inference(resolution,[],[f34,f4]) ).
fof(f41,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X1),X2),implies(implies(X0,X1),X2))),
inference(resolution,[],[f36,f34]) ).
fof(f44,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(implies(not(X0),X3),X1),X2))),
inference(resolution,[],[f38,f34]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(not(X0),X1),X2))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f38,f1]) ).
fof(f66,plain,
! [X0] : is_a_theorem(implies(X0,X0)),
inference(resolution,[],[f45,f3]) ).
fof(f75,plain,
! [X0,X1] : is_a_theorem(implies(not(implies(X0,X0)),X1)),
inference(resolution,[],[f66,f7]) ).
fof(f79,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1))),
inference(resolution,[],[f75,f34]) ).
fof(f143,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3))
| is_a_theorem(implies(implies(X2,X0),X3)) ),
inference(resolution,[],[f37,f1]) ).
fof(f163,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))),
inference(resolution,[],[f79,f45]) ).
fof(f173,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(not(implies(X0,X0)),X1),X2),implies(X3,X2))),
inference(resolution,[],[f163,f34]) ).
fof(f387,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(not(implies(X0,X0)),X1),X2))
| is_a_theorem(implies(X3,X2)) ),
inference(resolution,[],[f173,f1]) ).
fof(f393,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))),
inference(resolution,[],[f387,f3]) ).
fof(f413,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[],[f393,f34]) ).
fof(f441,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f413,f1]) ).
fof(f451,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))),
inference(resolution,[],[f441,f36]) ).
fof(f499,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),implies(X2,X1))),
inference(resolution,[],[f451,f34]) ).
fof(f738,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(not(X0),X0),X1),X2))
| is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(resolution,[],[f41,f1]) ).
fof(f779,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(not(X0),X0),X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f499,f1]) ).
fof(f955,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(not(not(X1)),X2),X1),X1))),
inference(resolution,[],[f44,f779]) ).
fof(f976,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(not(not(X0)),X1),X0),X0)),
inference(resolution,[],[f955,f6]) ).
fof(f985,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(not(not(X0)),X1),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f976,f1]) ).
fof(f1368,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X1)))),
inference(resolution,[],[f143,f413]) ).
fof(f1369,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X2,implies(X0,X1)))),
inference(resolution,[],[f143,f499]) ).
fof(f1412,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(not(X0),X2)))),
inference(resolution,[],[f1368,f45]) ).
fof(f1437,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(not(X1),X2)),X3),implies(X1,X3))),
inference(resolution,[],[f1412,f34]) ).
fof(f2047,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(not(X1),X2)),X3))
| is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f1437,f1]) ).
fof(f2174,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(X2,implies(implies(X1,X0),X0)))),
inference(resolution,[],[f1369,f143]) ).
fof(f2178,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),X1)))
| is_a_theorem(implies(X2,implies(X0,X1))) ),
inference(resolution,[],[f1369,f1]) ).
fof(f2273,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X0)))),
inference(resolution,[],[f2047,f1369]) ).
fof(f2344,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X3),implies(X2,X3))),
inference(resolution,[],[f2273,f34]) ).
fof(f2754,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f2344,f779]) ).
fof(f2774,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(resolution,[],[f2754,f985]) ).
fof(f2818,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(resolution,[],[f2774,f34]) ).
fof(f3109,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f2818,f1]) ).
fof(f6988,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(X0,X2),X2)))),
inference(resolution,[],[f2174,f3109]) ).
fof(f11315,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(X1,X2),X2)))),
inference(resolution,[],[f2178,f6988]) ).
fof(f11384,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[],[f11315,f985]) ).
fof(f11478,plain,
! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[],[f11384,f1]) ).
fof(f11479,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),
inference(resolution,[],[f11384,f34]) ).
fof(f11512,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1)),
inference(resolution,[],[f11478,f3]) ).
fof(f11584,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(not(X0),X1)),X2),X2)),
inference(resolution,[],[f11478,f4]) ).
fof(f12353,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))),
inference(resolution,[],[f11512,f143]) ).
fof(f12413,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(not(X0),X1)),X2))
| is_a_theorem(X2) ),
inference(resolution,[],[f11584,f1]) ).
fof(f12770,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))),
inference(resolution,[],[f12353,f143]) ).
fof(f13241,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| is_a_theorem(implies(implies(X1,X0),X0)) ),
inference(resolution,[],[f12770,f1]) ).
fof(f15353,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(resolution,[],[f11479,f143]) ).
fof(f15358,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X0,X1),X1),X2))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f11479,f1]) ).
fof(f16061,plain,
! [X0,X1] : is_a_theorem(implies(not(X0),implies(X0,X1))),
inference(resolution,[],[f15353,f12413]) ).
fof(f16075,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X1,implies(X0,X2))) ),
inference(resolution,[],[f15353,f1]) ).
fof(f16115,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),X0)),
inference(resolution,[],[f16061,f13241]) ).
fof(f73835,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(resolution,[],[f15358,f37]) ).
fof(f96697,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(implies(X2,X0),implies(X2,X1))) ),
inference(resolution,[],[f73835,f1]) ).
fof(f102772,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(implies(X1,X2),X1)),implies(X0,X1))),
inference(resolution,[],[f96697,f16115]) ).
fof(f125689,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),X0))),
inference(resolution,[],[f102772,f143]) ).
fof(f160050,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X1,X2),X0),X1))),
inference(resolution,[],[f125689,f16075]) ).
fof(f242021,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X2),not(X0)),X1))),
inference(resolution,[],[f160050,f45]) ).
fof(f242256,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(X2)),implies(X2,X0))),
inference(resolution,[],[f242021,f16075]) ).
fof(f242573,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,not(X1)),implies(X1,not(X0)))),
inference(resolution,[],[f242256,f738]) ).
fof(f242735,plain,
$false,
inference(resolution,[],[f242573,f5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL385-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.32 % Computer : n012.cluster.edu
% 0.04/0.32 % Model : x86_64 x86_64
% 0.04/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.32 % Memory : 8046.5625MB
% 0.04/0.32 % OS : Linux 6.8.0-71-generic
% 0.04/0.32 % CPULimit : 300
% 0.04/0.32 % WCLimit : 300
% 0.04/0.32 % DateTime : Sun Sep 27 15:38:20 UTC 2026
% 0.04/0.32 % CPUTime :
% 0.04/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.34 Running first-order model finding
% 0.07/0.34 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
% 15.12/2.52 % (2531427)Will run a generic schedule for satisfiability detection.
% 15.12/2.52 % (2531433)% WARNING: option uhcvi not known.
% 15.12/2.52 % (2531433)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1294000416:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.12/2.52 % (2531434)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1711504704:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.12/2.52 % (2531432)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1538621678_2999 on theBenchmark for (2999ds/0Mi)
% 15.12/2.52 % (2531435)dis+10_1_sil=32000:sp=arity:random_seed=1183995147:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.12/2.52 % (2531436)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3571056745:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.12/2.52 % (2531437)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=49645369:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.12/2.52 % (2531438)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3400136396:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.12/2.52 % TRYING [1]
% 15.12/2.52 % TRYING [2]
% 15.12/2.52 % TRYING [3]
% 15.12/2.52 % TRYING [4]
% 15.12/2.52 % (2531435)Instruction limit reached!
% 15.12/2.52 % (2531435)------------------------------
% 15.12/2.52 % (2531435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/2.52 % (2531435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/2.52 % (2531435)CaDiCaL version: 2.1.3
% 15.12/2.52 % (2531435)Termination reason: Instruction limit
% 15.12/2.52 % (2531435)Termination phase: Saturation
% 15.12/2.52 % (2531435)Time elapsed: 0.035 s
% 15.12/2.52 % (2531435)Peak memory usage: 11 MB
% 15.12/2.52 % (2531435)Instructions burned: 103 (million)
% 15.12/2.52 % (2531436)Instruction limit reached!
% 15.12/2.52 % (2531436)------------------------------
% 15.12/2.52 % (2531436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/2.52 % (2531436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/2.52 % (2531436)CaDiCaL version: 2.1.3
% 15.12/2.52 % (2531436)Termination reason: Instruction limit
% 15.12/2.52 % (2531436)Termination phase: Saturation
% 15.12/2.52 % (2531436)Time elapsed: 0.039 s
% 15.12/2.52 % (2531436)Peak memory usage: 11 MB
% 15.12/2.52 % (2531436)Instructions burned: 117 (million)
% 15.12/2.52 % (2531437)Instruction limit reached!
% 15.12/2.52 % (2531437)------------------------------
% 15.12/2.52 % (2531437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/2.52 % (2531437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/2.52 % (2531437)CaDiCaL version: 2.1.3
% 15.12/2.52 % (2531437)Termination reason: Instruction limit
% 15.12/2.52 % (2531437)Termination phase: Saturation
% 15.12/2.52 % (2531437)Time elapsed: 0.045 s
% 15.12/2.52 % (2531437)Peak memory usage: 13 MB
% 15.12/2.52 % (2531437)Instructions burned: 131 (million)
% 15.12/2.52 % (2531446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3259737654:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.12/2.52 % TRYING [1]
% 15.12/2.52 % TRYING [2]
% 15.12/2.52 % TRYING [3]
% 15.12/2.52 % (2531447)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3436053730:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.12/2.52 % TRYING [4]
% 15.12/2.52 % (2531438)Instruction limit reached!
% 15.12/2.52 % (2531438)------------------------------
% 15.12/2.52 % (2531438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/2.52 % (2531438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/2.52 % (2531438)CaDiCaL version: 2.1.3
% 15.12/2.52 % (2531438)Termination reason: Instruction limit
% 15.12/2.52 % (2531438)Termination phase: Saturation
% 15.12/2.52 % (2531438)Time elapsed: 0.055 s
% 15.12/2.52 % (2531438)Peak memory usage: 12 MB
% 15.12/2.52 % (2531438)Instructions burned: 161 (million)
% 15.12/2.52 % (2531448)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=1961602243:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.12/2.52 % TRYING [5]
% 15.12/2.52 % (2531451)ott-21_1_sil=16000:fs=off:random_seed=2210674824:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 15.12/2.52 % (2531447)Instruction limit reached!
% 15.12/2.52 % (2531447)------------------------------
% 15.12/2.52 % (2531447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531447)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531447)Termination reason: Instruction limit
% 31.13/4.89 % (2531447)Termination phase: Saturation
% 31.13/4.89 % (2531447)Time elapsed: 0.043 s
% 31.13/4.89 % (2531447)Peak memory usage: 12 MB
% 31.13/4.89 % (2531447)Instructions burned: 133 (million)
% 31.13/4.89 % (2531454)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=978649194:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 31.13/4.89 % TRYING [5]
% 31.13/4.89 % (2531451)Instruction limit reached!
% 31.13/4.89 % (2531451)------------------------------
% 31.13/4.89 % (2531451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531451)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531451)Termination reason: Instruction limit
% 31.13/4.89 % (2531451)Termination phase: Saturation
% 31.13/4.89 % (2531451)Time elapsed: 0.051 s
% 31.13/4.89 % (2531451)Peak memory usage: 13 MB
% 31.13/4.89 % (2531451)Instructions burned: 183 (million)
% 31.13/4.89 % (2531456)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3295545557:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 31.13/4.89 % TRYING [1]
% 31.13/4.89 % TRYING [2]
% 31.13/4.89 % TRYING [3]
% 31.13/4.89 % TRYING [4]
% 31.13/4.89 % TRYING [5]
% 31.13/4.89 % (2531454)Instruction limit reached!
% 31.13/4.89 % (2531454)------------------------------
% 31.13/4.89 % (2531454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531454)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531454)Termination reason: Instruction limit
% 31.13/4.89 % (2531454)Termination phase: Saturation
% 31.13/4.89 % (2531454)Time elapsed: 0.155 s
% 31.13/4.89 % (2531454)Peak memory usage: 12 MB
% 31.13/4.89 % (2531454)Instructions burned: 478 (million)
% 31.13/4.89 % (2531448)Instruction limit reached!
% 31.13/4.89 % (2531448)------------------------------
% 31.13/4.89 % (2531448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531448)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531448)Termination reason: Instruction limit
% 31.13/4.89 % (2531448)Termination phase: Saturation
% 31.13/4.89 % (2531448)Time elapsed: 0.215 s
% 31.13/4.89 % (2531448)Peak memory usage: 16 MB
% 31.13/4.89 % (2531448)Instructions burned: 685 (million)
% 31.13/4.89 % (2531458)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1457334477:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 31.13/4.89 % (2531446)Instruction limit reached!
% 31.13/4.89 % (2531446)------------------------------
% 31.13/4.89 % (2531446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531446)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531446)Termination reason: Instruction limit
% 31.13/4.89 % (2531446)Termination phase: Finite model building SAT solving
% 31.13/4.89 % (2531446)Time elapsed: 0.228 s
% 31.13/4.89 % (2531446)Peak memory usage: 13 MB
% 31.13/4.89 % (2531446)Instructions burned: 717 (million)
% 31.13/4.89 % (2531459)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=12716027:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 31.13/4.89 % (2531461)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=831873710:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 31.13/4.89 % TRYING [14]
% 31.13/4.89 % (2531456)Instruction limit reached!
% 31.13/4.89 % (2531456)------------------------------
% 31.13/4.89 % (2531456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.13/4.89 % (2531456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.13/4.89 % (2531456)CaDiCaL version: 2.1.3
% 31.13/4.89 % (2531456)Termination reason: Instruction limit
% 31.13/4.89 % (2531456)Termination phase: Finite model building SAT solving
% 31.13/4.89 % (2531456)Time elapsed: 0.286 s
% 31.13/4.89 % (2531456)Peak memory usage: 13 MB
% 31.13/4.89 % (2531456)Instructions burned: 867 (million)
% 31.13/4.89 % (2531464)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4124028349:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 31.13/4.89 % (2531459)Instruction limit reached!
% 31.13/4.89 % (2531459)------------------------------
% 65.85/9.71 % (2531459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531459)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531459)Termination reason: Instruction limit
% 65.85/9.71 % (2531459)Termination phase: Finite model building constraint generation
% 65.85/9.71 % (2531459)Time elapsed: 0.175 s
% 65.85/9.71 % (2531459)Peak memory usage: 63 MB
% 65.85/9.71 % (2531459)Instructions burned: 890 (million)
% 65.85/9.71 % (2531466)fmb+10_1_sil=64000:random_seed=3171616473:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 65.85/9.71 % TRYING [1]
% 65.85/9.71 % TRYING [2]
% 65.85/9.71 % TRYING [3]
% 65.85/9.71 % TRYING [4]
% 65.85/9.71 % (2531461)Instruction limit reached!
% 65.85/9.71 % (2531461)------------------------------
% 65.85/9.71 % (2531461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531461)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531461)Termination reason: Instruction limit
% 65.85/9.71 % (2531461)Termination phase: Saturation
% 65.85/9.71 % (2531461)Time elapsed: 0.214 s
% 65.85/9.71 % (2531461)Peak memory usage: 61 MB
% 65.85/9.71 % (2531461)Instructions burned: 695 (million)
% 65.85/9.71 % TRYING [5]
% 65.85/9.71 % (2531468)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2401175425:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 65.85/9.71 % TRYING [20]
% 65.85/9.71 % TRYING [6]
% 65.85/9.71 % (2531458)Instruction limit reached!
% 65.85/9.71 % (2531458)------------------------------
% 65.85/9.71 % (2531458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531458)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531458)Termination reason: Instruction limit
% 65.85/9.71 % (2531458)Termination phase: Saturation
% 65.85/9.71 % (2531458)Time elapsed: 0.406 s
% 65.85/9.71 % (2531458)Peak memory usage: 24 MB
% 65.85/9.71 % (2531458)Instructions burned: 1182 (million)
% 65.85/9.71 % (2531464)Instruction limit reached!
% 65.85/9.71 % (2531464)------------------------------
% 65.85/9.71 % (2531464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531464)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531464)Termination reason: Instruction limit
% 65.85/9.71 % (2531464)Termination phase: Saturation
% 65.85/9.71 % (2531464)Time elapsed: 0.255 s
% 65.85/9.71 % (2531464)Peak memory usage: 16 MB
% 65.85/9.71 % (2531464)Instructions burned: 881 (million)
% 65.85/9.71 % (2531471)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=723928400:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 65.85/9.71 % (2531470)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=916789644:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 65.85/9.71 % TRYING [8]
% 65.85/9.71 % TRYING [6]
% 65.85/9.71 % (2531470)Instruction limit reached!
% 65.85/9.71 % (2531470)------------------------------
% 65.85/9.71 % (2531470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531470)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531470)Termination reason: Instruction limit
% 65.85/9.71 % (2531470)Termination phase: Finite model building SAT solving
% 65.85/9.71 % (2531470)Time elapsed: 0.279 s
% 65.85/9.71 % (2531470)Peak memory usage: 32 MB
% 65.85/9.71 % (2531470)Instructions burned: 921 (million)
% 65.85/9.71 % (2531474)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1522248272:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 65.85/9.71 % (2531474)Instruction limit reached!
% 65.85/9.71 % (2531474)------------------------------
% 65.85/9.71 % (2531474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.85/9.71 % (2531474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.85/9.71 % (2531474)CaDiCaL version: 2.1.3
% 65.85/9.71 % (2531474)Termination reason: Instruction limit
% 65.85/9.71 % (2531474)Termination phase: Saturation
% 65.85/9.71 % (2531474)Time elapsed: 0.471 s
% 65.85/9.71 % (2531474)Peak memory usage: 21 MB
% 65.85/9.71 % (2531474)Instructions burned: 1472 (million)
% 65.85/9.71 % (2531476)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=943149931:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 65.85/9.71 % TRYING [77]
% 65.85/9.71 % (2531471)Instruction limit reached!
% 207.58/29.83 % (2531471)------------------------------
% 207.58/29.83 % (2531471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531471)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531471)Termination reason: Instruction limit
% 207.58/29.83 % (2531471)Termination phase: Saturation
% 207.58/29.83 % (2531471)Time elapsed: 1.457 s
% 207.58/29.83 % (2531471)Peak memory usage: 23 MB
% 207.58/29.83 % (2531471)Instructions burned: 5135 (million)
% 207.58/29.83 % (2531478)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1676778999:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 207.58/29.83 % TRYING [16]
% 207.58/29.83 % (2531478)Instruction limit reached!
% 207.58/29.83 % (2531478)------------------------------
% 207.58/29.83 % (2531478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531478)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531478)Termination reason: Instruction limit
% 207.58/29.83 % (2531478)Termination phase: Finite model building constraint generation
% 207.58/29.83 % (2531478)Time elapsed: 0.477 s
% 207.58/29.83 % (2531478)Peak memory usage: 156 MB
% 207.58/29.83 % (2531478)Instructions burned: 2175 (million)
% 207.58/29.83 % (2531480)ott-2_1_sil=16000:newcnf=on:random_seed=41858417:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi)
% 207.58/29.83 % (2531476)Instruction limit reached!
% 207.58/29.83 % (2531476)------------------------------
% 207.58/29.83 % (2531476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531476)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531476)Termination reason: Instruction limit
% 207.58/29.83 % (2531476)Termination phase: Finite model building constraint generation
% 207.58/29.83 % (2531476)Time elapsed: 1.243 s
% 207.58/29.83 % (2531476)Peak memory usage: 416 MB
% 207.58/29.83 % (2531476)Instructions burned: 6325 (million)
% 207.58/29.83 % (2531482)ott+10_1_sil=32000:tgt=ground:random_seed=447554351:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 207.58/29.83 % (2531468)Instruction limit reached!
% 207.58/29.83 % (2531468)------------------------------
% 207.58/29.83 % (2531468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531468)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531468)Termination reason: Instruction limit
% 207.58/29.83 % (2531468)Termination phase: Finite model building constraint generation
% 207.58/29.83 % (2531468)Time elapsed: 2.317 s
% 207.58/29.83 % (2531468)Peak memory usage: 596 MB
% 207.58/29.83 % (2531468)Instructions burned: 9518 (million)
% 207.58/29.83 % (2531484)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2377158023:i=54282_2970 on theBenchmark for (2970ds/54282Mi)
% 207.58/29.83 % TRYING [1]
% 207.58/29.83 % TRYING [2]
% 207.58/29.83 % TRYING [3]
% 207.58/29.83 % TRYING [4]
% 207.58/29.83 % (2531480)Instruction limit reached!
% 207.58/29.83 % (2531480)------------------------------
% 207.58/29.83 % (2531480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531480)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531480)Termination reason: Instruction limit
% 207.58/29.83 % (2531480)Termination phase: Saturation
% 207.58/29.83 % (2531480)Time elapsed: 0.268 s
% 207.58/29.83 % (2531480)Peak memory usage: 15 MB
% 207.58/29.83 % (2531480)Instructions burned: 869 (million)
% 207.58/29.83 % (2531486)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3821822471:i=3512:aac=none_2970 on theBenchmark for (2970ds/3512Mi)
% 207.58/29.83 % TRYING [5]
% 207.58/29.83 % TRYING [6]
% 207.58/29.83 % (2531486)Instruction limit reached!
% 207.58/29.83 % (2531486)------------------------------
% 207.58/29.83 % (2531486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.58/29.83 % (2531486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.58/29.83 % (2531486)CaDiCaL version: 2.1.3
% 207.58/29.83 % (2531486)Termination reason: Instruction limit
% 207.58/29.83 % (2531486)Termination phase: Saturation
% 207.58/29.83 % (2531486)Time elapsed: 1.278 s
% 207.58/29.83 % (2531486)Peak memory usage: 27 MB
% 207.58/29.83 % (2531486)Instructions burned: 3512 (million)
% 207.58/29.83 % (2531488)dis+21_1_sil=32000:sas=cadical:random_seed=4251730752:i=3773:amm=off_2957 on theBenchmark for (2957ds/3773Mi)
% 207.58/29.83 % (2531482)Instruction limit reached!
% 254.86/36.56 % (2531482)------------------------------
% 254.86/36.56 % (2531482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531482)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531482)Termination reason: Instruction limit
% 254.86/36.56 % (2531482)Termination phase: Saturation
% 254.86/36.56 % (2531482)Time elapsed: 1.767 s
% 254.86/36.56 % (2531482)Peak memory usage: 33 MB
% 254.86/36.56 % (2531482)Instructions burned: 5114 (million)
% 254.86/36.56 % (2531490)ott+11_1_sil=16000:gs=on:random_seed=1352574934:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2954 on theBenchmark for (2954ds/2251Mi)
% 254.86/36.56 % (2531490)Instruction limit reached!
% 254.86/36.56 % (2531490)------------------------------
% 254.86/36.56 % (2531490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531490)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531490)Termination reason: Instruction limit
% 254.86/36.56 % (2531490)Termination phase: Saturation
% 254.86/36.56 % (2531490)Time elapsed: 0.739 s
% 254.86/36.56 % (2531490)Peak memory usage: 29 MB
% 254.86/36.56 % (2531490)Instructions burned: 2251 (million)
% 254.86/36.56 % (2531492)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2602718286:fmbsr=1.6:i=67534_2946 on theBenchmark for (2946ds/67534Mi)
% 254.86/36.56 % TRYING [7]
% 254.86/36.56 % (2531488)Instruction limit reached!
% 254.86/36.56 % (2531488)------------------------------
% 254.86/36.56 % (2531488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531488)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531488)Termination reason: Instruction limit
% 254.86/36.56 % (2531488)Termination phase: Saturation
% 254.86/36.56 % (2531488)Time elapsed: 1.228 s
% 254.86/36.56 % (2531488)Peak memory usage: 36 MB
% 254.86/36.56 % (2531488)Instructions burned: 3774 (million)
% 254.86/36.56 % (2531494)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3512682220:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2945 on theBenchmark for (2945ds/4591Mi)
% 254.86/36.56 % TRYING [7]
% 254.86/36.56 % TRYING [7]
% 254.86/36.56 % (2531494)Instruction limit reached!
% 254.86/36.56 % (2531494)------------------------------
% 254.86/36.56 % (2531494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531494)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531494)Termination reason: Instruction limit
% 254.86/36.56 % (2531494)Termination phase: Saturation
% 254.86/36.56 % (2531494)Time elapsed: 1.295 s
% 254.86/36.56 % (2531494)Peak memory usage: 42 MB
% 254.86/36.56 % (2531494)Instructions burned: 4591 (million)
% 254.86/36.56 % (2531496)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1227640869:i=29340_2931 on theBenchmark for (2931ds/29340Mi)
% 254.86/36.56 % (2531466)Instruction limit reached!
% 254.86/36.56 % (2531466)------------------------------
% 254.86/36.56 % (2531466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531466)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531466)Termination reason: Instruction limit
% 254.86/36.56 % (2531466)Termination phase: Finite model building SAT solving
% 254.86/36.56 % (2531466)Time elapsed: 7.362 s
% 254.86/36.56 % (2531466)Peak memory usage: 20 MB
% 254.86/36.56 % (2531466)Instructions burned: 22063 (million)
% 254.86/36.56 % (2531498)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=348167025:i=5211_2921 on theBenchmark for (2921ds/5211Mi)
% 254.86/36.56 % TRYING [7]
% 254.86/36.56 % (2531498)Instruction limit reached!
% 254.86/36.56 % (2531498)------------------------------
% 254.86/36.56 % (2531498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531498)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531498)Termination reason: Instruction limit
% 254.86/36.56 % (2531498)Termination phase: Saturation
% 254.86/36.56 % (2531498)Time elapsed: 1.477 s
% 254.86/36.56 % (2531498)Peak memory usage: 29 MB
% 254.86/36.56 % (2531498)Instructions burned: 5213 (million)
% 254.86/36.56 % (2531500)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3963638349:i=5497:nm=2_2906 on theBenchmark for (2906ds/5497Mi)
% 254.86/36.56 % TRYING [17]
% 254.86/36.56 % (2531500)Instruction limit reached!
% 254.86/36.56 % (2531500)------------------------------
% 254.86/36.56 % (2531500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531500)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531500)Termination reason: Instruction limit
% 254.86/36.56 % (2531500)Termination phase: Finite model building constraint generation
% 254.86/36.56 % (2531500)Time elapsed: 1.333 s
% 254.86/36.56 % (2531500)Peak memory usage: 372 MB
% 254.86/36.56 % (2531500)Instructions burned: 5498 (million)
% 254.86/36.56 % (2531502)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2511974566:fmbsr=2:i=46332_2892 on theBenchmark for (2892ds/46332Mi)
% 254.86/36.56 % TRYING [15]
% 254.86/36.56 % (2531496)Instruction limit reached!
% 254.86/36.56 % (2531496)------------------------------
% 254.86/36.56 % (2531496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531496)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531496)Termination reason: Instruction limit
% 254.86/36.56 % (2531496)Termination phase: Saturation
% 254.86/36.56 % (2531496)Time elapsed: 10.015 s
% 254.86/36.56 % (2531496)Peak memory usage: 241 MB
% 254.86/36.56 % (2531496)Instructions burned: 29341 (million)
% 254.86/36.56 % (2531797)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2689049918:i=14071_2831 on theBenchmark for (2831ds/14071Mi)
% 254.86/36.56 % TRYING [12]
% 254.86/36.56 % (2531484)Instruction limit reached!
% 254.86/36.56 % (2531484)------------------------------
% 254.86/36.56 % (2531484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531484)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531484)Termination reason: Instruction limit
% 254.86/36.56 % (2531484)Termination phase: Finite model building SAT solving
% 254.86/36.56 % (2531484)Time elapsed: 18.776 s
% 254.86/36.56 % (2531484)Peak memory usage: 32 MB
% 254.86/36.56 % (2531484)Instructions burned: 54282 (million)
% 254.86/36.56 % (2531943)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1555635010:i=22565:add=on:rawr=on_2783 on theBenchmark for (2783ds/22565Mi)
% 254.86/36.56 % (2531797)Instruction limit reached!
% 254.86/36.56 % (2531797)------------------------------
% 254.86/36.56 % (2531797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531797)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531797)Termination reason: Instruction limit
% 254.86/36.56 % (2531797)Termination phase: Finite model building SAT solving
% 254.86/36.56 % (2531797)Time elapsed: 5.813 s
% 254.86/36.56 % (2531797)Peak memory usage: 140 MB
% 254.86/36.56 % (2531797)Instructions burned: 14073 (million)
% 254.86/36.56 % (2531945)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3175364688:i=8173:av=off_2773 on theBenchmark for (2773ds/8173Mi)
% 254.86/36.56 % (2531945)Instruction limit reached!
% 254.86/36.56 % (2531945)------------------------------
% 254.86/36.56 % (2531945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531945)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531945)Termination reason: Instruction limit
% 254.86/36.56 % (2531945)Termination phase: Saturation
% 254.86/36.56 % (2531945)Time elapsed: 2.793 s
% 254.86/36.56 % (2531945)Peak memory usage: 67 MB
% 254.86/36.56 % (2531945)Instructions burned: 8175 (million)
% 254.86/36.56 % (2531947)dis+10_16:1_sil=16000:random_seed=3085921561:i=9155:fsr=off_2744 on theBenchmark for (2744ds/9155Mi)
% 254.86/36.56 % (2531947)Instruction limit reached!
% 254.86/36.56 % (2531947)------------------------------
% 254.86/36.56 % (2531947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531947)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531947)Termination reason: Instruction limit
% 254.86/36.56 % (2531947)Termination phase: Saturation
% 254.86/36.56 % (2531947)Time elapsed: 3.004 s
% 254.86/36.56 % (2531947)Peak memory usage: 58 MB
% 254.86/36.56 % (2531947)Instructions burned: 9155 (million)
% 254.86/36.56 % (2531949)ott-3_8_sil=64000:random_seed=3031446429:i=20139:bs=on_2714 on theBenchmark for (2714ds/20139Mi)
% 254.86/36.56 % (2531943)Instruction limit reached!
% 254.86/36.56 % (2531943)------------------------------
% 254.86/36.56 % (2531943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531943)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531943)Termination reason: Instruction limit
% 254.86/36.56 % (2531943)Termination phase: Saturation
% 254.86/36.56 % (2531943)Time elapsed: 7.777 s
% 254.86/36.56 % (2531943)Peak memory usage: 257 MB
% 254.86/36.56 % (2531943)Instructions burned: 22568 (million)
% 254.86/36.56 % (2532083)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=62422022:fmbsr=2:i=32576_2704 on theBenchmark for (2704ds/32576Mi)
% 254.86/36.56 % TRYING [9]
% 254.86/36.56 % (2531492)Instruction limit reached!
% 254.86/36.56 % (2531492)------------------------------
% 254.86/36.56 % (2531492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531492)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531492)Termination reason: Instruction limit
% 254.86/36.56 % (2531492)Termination phase: Finite model building SAT solving
% 254.86/36.56 % (2531492)Time elapsed: 25.717 s
% 254.86/36.56 % (2531492)Peak memory usage: 39 MB
% 254.86/36.56 % (2531492)Instructions burned: 67535 (million)
% 254.86/36.56 % (2532224)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2697734211:i=11404_2689 on theBenchmark for (2689ds/11404Mi)
% 254.86/36.56 % (2531434)Instruction limit reached!
% 254.86/36.56 % (2531434)------------------------------
% 254.86/36.56 % (2531434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531434)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531434)Termination reason: Instruction limit
% 254.86/36.56 % (2531434)Termination phase: Saturation
% 254.86/36.56 % (2531434)Time elapsed: 33.076 s
% 254.86/36.56 % (2531434)Peak memory usage: 574 MB
% 254.86/36.56 % (2531434)Instructions burned: 88024 (million)
% 254.86/36.56 % (2532255)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=372004957:i=14134_2668 on theBenchmark for (2668ds/14134Mi)
% 254.86/36.56 % (2531502)Instruction limit reached!
% 254.86/36.56 % (2531502)------------------------------
% 254.86/36.56 % (2531502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2531502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2531502)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2531502)Termination reason: Instruction limit
% 254.86/36.56 % (2531502)Termination phase: Finite model building SAT solving
% 254.86/36.56 % (2531502)Time elapsed: 23.401 s
% 254.86/36.56 % (2531502)Peak memory usage: 377 MB
% 254.86/36.56 % (2531502)Instructions burned: 46334 (million)
% 254.86/36.56 % (2532341)dis+33_16_sil=32000:sac=on:random_seed=269276278:i=15851:nm=0_2658 on theBenchmark for (2658ds/15851Mi)
% 254.86/36.56 % (2532341) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2531427-2532341"...
% 254.86/36.56 % (2532341)...printing done.
% 254.86/36.56 % (2532341)Refutation found. Thanks to Tanya!
% 254.86/36.56 % SZS status Unsatisfiable for theBenchmark
% 254.86/36.56 % SZS output start Proof for theBenchmark
% See solution above
% 254.86/36.56 % (2532341)------------------------------
% 254.86/36.56 % (2532341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 254.86/36.56 % (2532341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 254.86/36.56 % (2532341)CaDiCaL version: 2.1.3
% 254.86/36.56 % (2532341)Termination reason: Refutation
% 254.86/36.56 % (2532341)Time elapsed: 1.986 s
% 254.86/36.56 % (2532341)Peak memory usage: 92 MB
% 254.86/36.56 % (2532341)Instructions burned: 5706 (million)
% 254.86/36.56 % (2531427)Success in time 36.218 s
% 254.86/36.56 % Vampire exiting
%------------------------------------------------------------------------------