%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL119-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:51:16 AM UTC 2026
% Result : Unsatisfiable 96.76s 22.91s
% Output : Refutation 155.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 5
% Syntax : Number of formulae : 69 ( 9 unt; 2 def)
% Number of atoms : 164 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 193 ( 98 ~; 93 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 3 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 171 ( 0 sgn 171 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(equivalent(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(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X1,X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xgj) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,equivalent(b,c)),equivalent(c,equivalent(b,a)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_wo) ).
fof(f4,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f5,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(X0)
| is_a_theorem(equivalent(X1,X2)) ),
inference(resolution,[],[f4,f1]) ).
fof(f6,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X2,equivalent(X0,equivalent(X1,X2))))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(resolution,[],[f5,f2]) ).
fof(f8,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(X2,X0)) ),
inference(resolution,[],[f6,f5]) ).
fof(f10,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),equivalent(X2,X3)),X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(resolution,[],[f8,f2]) ).
fof(f11,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(equivalent(X2,equivalent(X3,X1)),X0))
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X2,X3)) ),
inference(resolution,[],[f8,f6]) ).
fof(f21,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X3,X1)))
| ~ is_a_theorem(equivalent(X2,X3))
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(X0) ),
inference(resolution,[],[f11,f1]) ).
fof(f46,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X2,X0))))
| ~ is_a_theorem(equivalent(X3,equivalent(X1,X2)))
| is_a_theorem(X3) ),
inference(resolution,[],[f21,f2]) ).
fof(f61,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X2)),X1)))
| is_a_theorem(X0) ),
inference(resolution,[],[f46,f2]) ).
fof(f66,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X1,X0),equivalent(X2,X2)),X1))
| is_a_theorem(X0) ),
inference(resolution,[],[f61,f6]) ).
fof(f68,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X1)),equivalent(X0,X2)))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f61,f4]) ).
fof(f70,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X3,equivalent(X4,X4)),X3),X2))
| is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X0,X1))) ),
inference(resolution,[],[f61,f10]) ).
fof(f73,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X0)
| is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)) ),
inference(resolution,[],[f68,f5]) ).
fof(f78,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)) ),
inference(duplicate_literal_removal,[],[f73]) ).
fof(f80,definition,
( spl0_7
<=> ! [X2,X1] : is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f81,plain,
( ! [X2,X1] : is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f80]) ).
fof(f83,definition,
( spl0_8
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f84,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f85,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f78,f83,f80]) ).
fof(f90,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X1)),X0),equivalent(X2,X2)))
| ~ spl0_7 ),
inference(resolution,[],[f81,f61]) ).
fof(f95,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X1)),X0))
| is_a_theorem(equivalent(X2,X2)) )
| ~ spl0_7 ),
inference(resolution,[],[f90,f1]) ).
fof(f96,plain,
( ! [X2] : is_a_theorem(equivalent(X2,X2))
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f95,f81]) ).
fof(f97,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(X1,X0)) )
| ~ spl0_7 ),
inference(resolution,[],[f96,f8]) ).
fof(f102,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X0,X1)),X2))
| ~ spl0_7 ),
inference(resolution,[],[f97,f2]) ).
fof(f103,plain,
( ! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),X2))
| ~ is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f97,f6]) ).
fof(f109,plain,
( ! [X0,X1] : is_a_theorem(equivalent(X0,equivalent(X0,equivalent(X1,X1))))
| ~ spl0_7 ),
inference(resolution,[],[f97,f81]) ).
fof(f122,plain,
( ! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,X0),equivalent(X1,X1)))
| ~ spl0_7 ),
inference(resolution,[],[f109,f61]) ).
fof(f127,plain,
( ! [X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,X1),X0))
| ~ is_a_theorem(X0) )
| ~ spl0_7 ),
inference(resolution,[],[f122,f5]) ).
fof(f206,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X0),X1))
| is_a_theorem(X0) )
| ~ spl0_7 ),
inference(resolution,[],[f66,f103]) ).
fof(f220,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),X2))
| is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f206,f10]) ).
fof(f221,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,X1))
| is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(X2,X0)) )
| ~ spl0_7 ),
inference(resolution,[],[f206,f11]) ).
fof(f229,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X0))
| is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f221,f81]) ).
fof(f237,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X1,X2))))
| ~ is_a_theorem(equivalent(X3,X0)) )
| ~ spl0_7 ),
inference(resolution,[],[f221,f2]) ).
fof(f282,plain,
( ! [X0,X1] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X1,X0))))
| ~ spl0_7 ),
inference(resolution,[],[f229,f102]) ).
fof(f284,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X2))
| is_a_theorem(equivalent(X0,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f229,f11]) ).
fof(f301,plain,
( ! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X0,X1)),X1))
| ~ spl0_7 ),
inference(resolution,[],[f282,f97]) ).
fof(f312,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X0,X1)))
| is_a_theorem(X1) )
| ~ spl0_7 ),
inference(resolution,[],[f301,f1]) ).
fof(f340,plain,
( ! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X1),X0))
| is_a_theorem(X0) )
| ~ spl0_7 ),
inference(resolution,[],[f312,f127]) ).
fof(f358,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(X2,X2))),equivalent(X0,X1)))
| ~ spl0_7 ),
inference(resolution,[],[f340,f2]) ).
fof(f372,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X2,equivalent(X3,X3)))))
| is_a_theorem(equivalent(equivalent(X1,X2),X0)) )
| ~ spl0_7 ),
inference(resolution,[],[f358,f8]) ).
fof(f436,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(X1,X1),X2)),X0),X2))
| ~ spl0_7 ),
inference(resolution,[],[f372,f2]) ).
fof(f463,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X2),X1)),X0))
| ~ spl0_7 ),
inference(resolution,[],[f436,f220]) ).
fof(f586,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X2),X1)))
| is_a_theorem(X0) )
| ~ spl0_7 ),
inference(resolution,[],[f463,f1]) ).
fof(f780,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X1,X2))))
| is_a_theorem(equivalent(X0,X2)) )
| ~ spl0_7 ),
inference(resolution,[],[f284,f282]) ).
fof(f1854,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(X2,X0),X2))))
| is_a_theorem(X1) )
| ~ spl0_7 ),
inference(resolution,[],[f237,f586]) ).
fof(f2185,plain,
( ! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X0,X2)))
| ~ is_a_theorem(equivalent(X2,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f1854,f237]) ).
fof(f2212,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X2,X0))))
| is_a_theorem(equivalent(X2,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f2185,f220]) ).
fof(f2235,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),X2))
| is_a_theorem(equivalent(equivalent(X0,X2),X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f2185,f780]) ).
fof(f2251,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X3,X1)))
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(equivalent(X3,X0),X2)) )
| ~ spl0_7 ),
inference(resolution,[],[f2185,f8]) ).
fof(f3829,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| is_a_theorem(equivalent(equivalent(X3,X0),X2))
| ~ is_a_theorem(equivalent(X3,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f2251,f6]) ).
fof(f4023,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X2,equivalent(X3,X1))))
| is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X3))) )
| ~ spl0_7 ),
inference(resolution,[],[f3829,f2]) ).
fof(f4085,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,equivalent(X1,X0)),X2)))
| ~ spl0_7 ),
inference(resolution,[],[f4023,f2]) ).
fof(f4169,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X2,X1))))
| ~ spl0_7 ),
inference(resolution,[],[f4085,f2212]) ).
fof(f4335,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X3,X2))))
| is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X3))) )
| ~ spl0_7 ),
inference(resolution,[],[f4169,f3829]) ).
fof(f4357,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(X2,X0))),equivalent(X2,X1)))
| ~ spl0_7 ),
inference(resolution,[],[f4335,f2]) ).
fof(f4440,plain,
( ! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X2,equivalent(X1,X0))))
| ~ spl0_7 ),
inference(resolution,[],[f4357,f2235]) ).
fof(f4483,plain,
( $false
| ~ spl0_7 ),
inference(resolution,[],[f4440,f3]) ).
fof(f4539,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f4483]) ).
fof(f4559,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,equivalent(X5,X5)),X4))),equivalent(X2,X3)))),equivalent(X0,X1))),
inference(resolution,[],[f70,f2]) ).
fof(f4562,plain,
( $false
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f4559,f84]) ).
fof(f4563,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f4562]) ).
cnf(s4,plain,
( spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f85]) ).
cnf(s5,plain,
~ spl0_7,
inference(sat_conversion,[],[f4539]) ).
cnf(s6,plain,
~ spl0_8,
inference(sat_conversion,[],[f4563]) ).
cnf(s7,plain,
$false,
inference(rat,[],[s4,s6,s5]) ).
fof(f4564,plain,
$false,
inference(avatar_sat_refutation,[],[s7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL119-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 % Computer : n004.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 15:22:52 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.00/3.62 % (3659822)Input is clausal, will run a generic CNF schedule.
% 18.00/3.62 % (3659841)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=121902247:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 18.00/3.62 % (3659840)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2927378726:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 18.00/3.62 % (3659843)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1836476143:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 18.00/3.62 % (3659842)lrs+10_1_sil=8000:sp=occurrence:random_seed=647562505:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 18.00/3.62 % (3659844)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=623650590:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 18.00/3.62 % (3659845)dis-21_1_sil=8000:lcm=predicate:random_seed=1596362204:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 18.00/3.62 % (3659839)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4093466711:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 18.00/3.62 % (3659842)Instruction limit reached!
% 18.00/3.62 % (3659842)------------------------------
% 18.00/3.62 % (3659842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.62 % (3659842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.62 % (3659842)CaDiCaL version: 2.1.3
% 18.00/3.62 % (3659842)Termination reason: Instruction limit
% 18.00/3.62 % (3659842)Termination phase: Saturation
% 18.00/3.62 % (3659842)Time elapsed: 0.104 s
% 18.00/3.62 % (3659842)Peak memory usage: 88 MB
% 18.00/3.62 % (3659842)Instructions burned: 108 (million)
% 18.00/3.62 % (3659843)Instruction limit reached!
% 18.00/3.62 % (3659843)------------------------------
% 18.00/3.62 % (3659843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.62 % (3659843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.62 % (3659843)CaDiCaL version: 2.1.3
% 18.00/3.62 % (3659843)Termination reason: Instruction limit
% 18.00/3.62 % (3659843)Termination phase: Saturation
% 18.00/3.62 % (3659843)Time elapsed: 0.113 s
% 18.00/3.62 % (3659843)Peak memory usage: 88 MB
% 18.00/3.62 % (3659843)Instructions burned: 115 (million)
% 18.00/3.62 % (3659845)Instruction limit reached!
% 18.00/3.62 % (3659845)------------------------------
% 18.00/3.62 % (3659845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.62 % (3659845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.62 % (3659845)CaDiCaL version: 2.1.3
% 18.00/3.62 % (3659845)Termination reason: Instruction limit
% 18.00/3.62 % (3659845)Termination phase: Saturation
% 18.00/3.62 % (3659845)Time elapsed: 0.114 s
% 18.00/3.62 % (3659845)Peak memory usage: 88 MB
% 18.00/3.62 % (3659845)Instructions burned: 117 (million)
% 18.00/3.62 % (3659844)Instruction limit reached!
% 18.00/3.62 % (3659844)------------------------------
% 18.00/3.62 % (3659844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.62 % (3659844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.62 % (3659844)CaDiCaL version: 2.1.3
% 18.00/3.62 % (3659844)Termination reason: Instruction limit
% 18.00/3.62 % (3659844)Termination phase: Saturation
% 18.00/3.62 % (3659844)Time elapsed: 0.167 s
% 18.00/3.62 % (3659844)Peak memory usage: 89 MB
% 18.00/3.62 % (3659844)Instructions burned: 181 (million)
% 18.00/3.62 % (3659856)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2791191852:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 18.00/3.62 % (3659855)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3814571616:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.00/3.62 % (3659855)Refutation not found, incomplete strategy
% 18.00/3.62 % (3659855)------------------------------
% 18.00/3.62 % (3659855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.62 % (3659855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.62 % (3659855)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659855)Termination reason: Refutation not found, incomplete strategy
% 36.73/6.27 % (3659855)Time elapsed: 0.001 s
% 36.73/6.27 % (3659855)Peak memory usage: 87 MB
% 36.73/6.27 % (3659857)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3329794922:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 36.73/6.27 % (3659857)Refutation not found, incomplete strategy
% 36.73/6.27 % (3659857)------------------------------
% 36.73/6.27 % (3659857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.73/6.27 % (3659857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.73/6.27 % (3659857)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659857)Termination reason: Refutation not found, incomplete strategy
% 36.73/6.27 % (3659857)Time elapsed: 0.001 s
% 36.73/6.27 % (3659857)Peak memory usage: 87 MB
% 36.73/6.27 % (3659860)lrs+10_64_to=lpo:sil=8000:random_seed=4192687218:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 36.73/6.27 % (3659856)Instruction limit reached!
% 36.73/6.27 % (3659856)------------------------------
% 36.73/6.27 % (3659856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.73/6.27 % (3659856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.73/6.27 % (3659856)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659856)Termination reason: Instruction limit
% 36.73/6.27 % (3659856)Termination phase: Saturation
% 36.73/6.27 % (3659856)Time elapsed: 0.114 s
% 36.73/6.27 % (3659856)Peak memory usage: 88 MB
% 36.73/6.27 % (3659856)Instructions burned: 190 (million)
% 36.73/6.27 % (3659860)Instruction limit reached!
% 36.73/6.27 % (3659860)------------------------------
% 36.73/6.27 % (3659860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.73/6.27 % (3659860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.73/6.27 % (3659860)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659860)Termination reason: Instruction limit
% 36.73/6.27 % (3659860)Termination phase: Saturation
% 36.73/6.27 % (3659860)Time elapsed: 0.124 s
% 36.73/6.27 % (3659860)Peak memory usage: 88 MB
% 36.73/6.27 % (3659860)Instructions burned: 126 (million)
% 36.73/6.27 % (3659865)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1239245606:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 36.73/6.27 % (3659855)------------------------------
% 36.73/6.27 % (3659855)------------------------------
% 36.73/6.27 % (3659857)------------------------------
% 36.73/6.27 % (3659857)------------------------------
% 36.73/6.27 % (3659866)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3349108363:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 36.73/6.27 % (3659865)Instruction limit reached!
% 36.73/6.27 % (3659865)------------------------------
% 36.73/6.27 % (3659865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.73/6.27 % (3659865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.73/6.27 % (3659865)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659865)Termination reason: Instruction limit
% 36.73/6.27 % (3659865)Termination phase: Saturation
% 36.73/6.27 % (3659865)Time elapsed: 0.208 s
% 36.73/6.27 % (3659865)Peak memory usage: 89 MB
% 36.73/6.27 % (3659865)Instructions burned: 194 (million)
% 36.73/6.27 % (3659866)Instruction limit reached!
% 36.73/6.27 % (3659866)------------------------------
% 36.73/6.27 % (3659866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.73/6.27 % (3659866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.73/6.27 % (3659866)CaDiCaL version: 2.1.3
% 36.73/6.27 % (3659866)Termination reason: Instruction limit
% 36.73/6.27 % (3659866)Termination phase: Saturation
% 36.73/6.27 % (3659866)Time elapsed: 0.164 s
% 36.73/6.27 % (3659866)Peak memory usage: 90 MB
% 36.73/6.27 % (3659866)Instructions burned: 157 (million)
% 36.73/6.27 % (3659870)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1904192317:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 36.73/6.27 % (3659871)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=418139905:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 36.73/6.27 % (3659873)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2498474786:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 36.73/6.27 % (3659873)Refutation not found, incomplete strategy
% 36.73/6.27 % (3659873)------------------------------
% 53.85/8.71 % (3659873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659873)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659873)Termination reason: Refutation not found, incomplete strategy
% 53.85/8.71 % (3659873)Time elapsed: 0.001 s
% 53.85/8.71 % (3659873)Peak memory usage: 87 MB
% 53.85/8.71 % (3659871)Instruction limit reached!
% 53.85/8.71 % (3659871)------------------------------
% 53.85/8.71 % (3659871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659871)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659871)Termination reason: Instruction limit
% 53.85/8.71 % (3659871)Termination phase: Saturation
% 53.85/8.71 % (3659871)Time elapsed: 0.098 s
% 53.85/8.71 % (3659871)Peak memory usage: 88 MB
% 53.85/8.71 % (3659871)Instructions burned: 106 (million)
% 53.85/8.71 % (3659874)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1311822079:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 53.85/8.71 % (3659878)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=443503439:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 53.85/8.71 % (3659874)Instruction limit reached!
% 53.85/8.71 % (3659874)------------------------------
% 53.85/8.71 % (3659874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659874)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659874)Termination reason: Instruction limit
% 53.85/8.71 % (3659874)Termination phase: Saturation
% 53.85/8.71 % (3659874)Time elapsed: 0.205 s
% 53.85/8.71 % (3659874)Peak memory usage: 89 MB
% 53.85/8.71 % (3659874)Instructions burned: 243 (million)
% 53.85/8.71 % (3659873)------------------------------
% 53.85/8.71 % (3659873)------------------------------
% 53.85/8.71 % (3659881)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=216488594:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 53.85/8.71 % (3659882)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2923902320:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 53.85/8.71 % (3659881)Instruction limit reached!
% 53.85/8.71 % (3659881)------------------------------
% 53.85/8.71 % (3659881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659881)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659881)Termination reason: Instruction limit
% 53.85/8.71 % (3659881)Termination phase: Saturation
% 53.85/8.71 % (3659881)Time elapsed: 0.149 s
% 53.85/8.71 % (3659881)Peak memory usage: 89 MB
% 53.85/8.71 % (3659881)Instructions burned: 134 (million)
% 53.85/8.71 % (3659885)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2596406723:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 53.85/8.71 % (3659882)Instruction limit reached!
% 53.85/8.71 % (3659882)------------------------------
% 53.85/8.71 % (3659882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659882)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659882)Termination reason: Instruction limit
% 53.85/8.71 % (3659882)Termination phase: Saturation
% 53.85/8.71 % (3659882)Time elapsed: 0.444 s
% 53.85/8.71 % (3659882)Peak memory usage: 91 MB
% 53.85/8.71 % (3659882)Instructions burned: 500 (million)
% 53.85/8.71 % (3659885)Instruction limit reached!
% 53.85/8.71 % (3659885)------------------------------
% 53.85/8.71 % (3659885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.85/8.71 % (3659885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.85/8.71 % (3659885)CaDiCaL version: 2.1.3
% 53.85/8.71 % (3659885)Termination reason: Instruction limit
% 53.85/8.71 % (3659885)Termination phase: Saturation
% 53.85/8.71 % (3659885)Time elapsed: 0.192 s
% 53.85/8.71 % (3659885)Peak memory usage: 89 MB
% 53.85/8.71 % (3659885)Instructions burned: 191 (million)
% 53.85/8.71 % (3659890)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2031732765:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 96.32/14.68 % (3659889)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2756122342:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 96.32/14.68 % (3659890)Instruction limit reached!
% 96.32/14.68 % (3659890)------------------------------
% 96.32/14.68 % (3659890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.32/14.68 % (3659890)CaDiCaL version: 2.1.3
% 96.32/14.68 % (3659890)Termination reason: Instruction limit
% 96.32/14.68 % (3659890)Termination phase: Saturation
% 96.32/14.68 % (3659890)Time elapsed: 0.139 s
% 96.32/14.68 % (3659890)Peak memory usage: 89 MB
% 96.32/14.68 % (3659890)Instructions burned: 157 (million)
% 96.32/14.68 % (3659889)Instruction limit reached!
% 96.32/14.68 % (3659889)------------------------------
% 96.32/14.68 % (3659889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.32/14.68 % (3659889)CaDiCaL version: 2.1.3
% 96.32/14.68 % (3659889)Termination reason: Instruction limit
% 96.32/14.68 % (3659889)Termination phase: Saturation
% 96.32/14.68 % (3659889)Time elapsed: 0.259 s
% 96.32/14.68 % (3659889)Peak memory usage: 91 MB
% 96.32/14.68 % (3659889)Instructions burned: 264 (million)
% 96.32/14.68 % (3659893)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3309854313:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 96.32/14.68 % (3659894)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3290057026:i=537:av=off:ss=included_2972 on theBenchmark for (2972ds/537Mi)
% 96.32/14.68 % (3659894)Instruction limit reached!
% 96.32/14.68 % (3659894)------------------------------
% 96.32/14.68 % (3659894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.32/14.68 % (3659894)CaDiCaL version: 2.1.3
% 96.32/14.68 % (3659894)Termination reason: Instruction limit
% 96.32/14.68 % (3659894)Termination phase: Saturation
% 96.32/14.68 % (3659894)Time elapsed: 0.527 s
% 96.32/14.68 % (3659894)Peak memory usage: 91 MB
% 96.32/14.68 % (3659894)Instructions burned: 537 (million)
% 96.32/14.68 % (3659897)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3575913596:i=180:bd=preordered:av=off_2964 on theBenchmark for (2964ds/180Mi)
% 96.32/14.68 % (3659897)Instruction limit reached!
% 96.32/14.68 % (3659897)------------------------------
% 96.32/14.68 % (3659897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.32/14.68 % (3659897)CaDiCaL version: 2.1.3
% 96.32/14.68 % (3659897)Termination reason: Instruction limit
% 96.32/14.68 % (3659897)Termination phase: Saturation
% 96.32/14.68 % (3659897)Time elapsed: 0.163 s
% 96.32/14.68 % (3659897)Peak memory usage: 88 MB
% 96.32/14.68 % (3659897)Instructions burned: 180 (million)
% 96.32/14.68 % (3659899)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3670727097:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2960 on theBenchmark for (2960ds/10307Mi)
% 96.32/14.68 % (3659870)Instruction limit reached!
% 96.32/14.68 % (3659870)------------------------------
% 96.32/14.68 % (3659870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.32/14.68 % (3659870)CaDiCaL version: 2.1.3
% 96.32/14.68 % (3659870)Termination reason: Instruction limit
% 96.32/14.68 % (3659870)Termination phase: Saturation
% 96.32/14.68 % (3659870)Time elapsed: 3.363 s
% 96.32/14.68 % (3659870)Peak memory usage: 146 MB
% 96.32/14.68 % (3659870)Instructions burned: 3396 (million)
% 96.32/14.68 % (3659903)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=66490959:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 96.32/14.68 % (3659903)Instruction limit reached!
% 96.32/14.68 % (3659903)------------------------------
% 96.32/14.68 % (3659903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.32/14.68 % (3659903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659903)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659903)Termination reason: Instruction limit
% 126.08/18.97 % (3659903)Termination phase: Saturation
% 126.08/18.97 % (3659903)Time elapsed: 0.427 s
% 126.08/18.97 % (3659903)Peak memory usage: 94 MB
% 126.08/18.97 % (3659903)Instructions burned: 413 (million)
% 126.08/18.97 % (3659905)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3192234419:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 126.08/18.97 % (3659893)Instruction limit reached!
% 126.08/18.97 % (3659893)------------------------------
% 126.08/18.97 % (3659893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.08/18.97 % (3659893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659893)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659893)Termination reason: Instruction limit
% 126.08/18.97 % (3659893)Termination phase: Saturation
% 126.08/18.97 % (3659893)Time elapsed: 3.113 s
% 126.08/18.97 % (3659893)Peak memory usage: 147 MB
% 126.08/18.97 % (3659893)Instructions burned: 3256 (million)
% 126.08/18.97 % (3659907)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=4095049720:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2939 on theBenchmark for (2939ds/303Mi)
% 126.08/18.97 % (3659907)Instruction limit reached!
% 126.08/18.97 % (3659907)------------------------------
% 126.08/18.97 % (3659907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.08/18.97 % (3659907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659907)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659907)Termination reason: Instruction limit
% 126.08/18.97 % (3659907)Termination phase: Saturation
% 126.08/18.97 % (3659907)Time elapsed: 0.261 s
% 126.08/18.97 % (3659907)Peak memory usage: 90 MB
% 126.08/18.97 % (3659907)Instructions burned: 303 (million)
% 126.08/18.97 % (3659878)Instruction limit reached!
% 126.08/18.97 % (3659878)------------------------------
% 126.08/18.97 % (3659878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.08/18.97 % (3659878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659878)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659878)Termination reason: Instruction limit
% 126.08/18.97 % (3659878)Termination phase: Saturation
% 126.08/18.97 % (3659878)Time elapsed: 5.219 s
% 126.08/18.97 % (3659878)Peak memory usage: 157 MB
% 126.08/18.97 % (3659878)Instructions burned: 5208 (million)
% 126.08/18.97 % (3659911)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1948887469:st=4:i=720:sd=3:fsr=off:ss=axioms_2935 on theBenchmark for (2935ds/720Mi)
% 126.08/18.97 % (3659913)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=237376662:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi)
% 126.08/18.97 % (3659911)Instruction limit reached!
% 126.08/18.97 % (3659911)------------------------------
% 126.08/18.97 % (3659911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.08/18.97 % (3659911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659911)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659911)Termination reason: Instruction limit
% 126.08/18.97 % (3659911)Termination phase: Saturation
% 126.08/18.97 % (3659911)Time elapsed: 0.594 s
% 126.08/18.97 % (3659911)Peak memory usage: 88 MB
% 126.08/18.97 % (3659911)Instructions burned: 721 (million)
% 126.08/18.97 % (3659913)Instruction limit reached!
% 126.08/18.97 % (3659913)------------------------------
% 126.08/18.97 % (3659913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.08/18.97 % (3659913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.08/18.97 % (3659913)CaDiCaL version: 2.1.3
% 126.08/18.97 % (3659913)Termination reason: Instruction limit
% 126.08/18.97 % (3659913)Termination phase: Saturation
% 126.08/18.97 % (3659913)Time elapsed: 0.579 s
% 126.08/18.97 % (3659913)Peak memory usage: 94 MB
% 126.08/18.97 % (3659913)Instructions burned: 599 (million)
% 126.08/18.97 % (3659920)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=907907566:i=2989:sd=3:ss=axioms:sgt=60_2927 on theBenchmark for (2927ds/2989Mi)
% 126.08/18.97 % (3659922)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1070379136:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 96.76/22.91 % (3659922)Instruction limit reached!
% 96.76/22.91 % (3659922)------------------------------
% 96.76/22.91 % (3659922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659922)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659922)Termination reason: Instruction limit
% 96.76/22.91 % (3659922)Termination phase: Saturation
% 96.76/22.91 % (3659922)Time elapsed: 2.251 s
% 96.76/22.91 % (3659922)Peak memory usage: 136 MB
% 96.76/22.91 % (3659922)Instructions burned: 1997 (million)
% 96.76/22.91 % (3659925)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1058397930:i=2088:bd=preordered:av=off_2901 on theBenchmark for (2901ds/2088Mi)
% 96.76/22.91 % (3659920)Instruction limit reached!
% 96.76/22.91 % (3659920)------------------------------
% 96.76/22.91 % (3659920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659920)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659920)Termination reason: Instruction limit
% 96.76/22.91 % (3659920)Termination phase: Saturation
% 96.76/22.91 % (3659920)Time elapsed: 3.032 s
% 96.76/22.91 % (3659920)Peak memory usage: 144 MB
% 96.76/22.91 % (3659920)Instructions burned: 2989 (million)
% 96.76/22.91 % (3659929)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1712405800:i=1098:nicw=on_2894 on theBenchmark for (2894ds/1098Mi)
% 96.76/22.91 % (3659929)Instruction limit reached!
% 96.76/22.91 % (3659929)------------------------------
% 96.76/22.91 % (3659929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659929)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659929)Termination reason: Instruction limit
% 96.76/22.91 % (3659929)Termination phase: Saturation
% 96.76/22.91 % (3659929)Time elapsed: 0.973 s
% 96.76/22.91 % (3659929)Peak memory usage: 94 MB
% 96.76/22.91 % (3659929)Instructions burned: 1099 (million)
% 96.76/22.91 % (3659933)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1032830945:i=433:bd=preordered_2882 on theBenchmark for (2882ds/433Mi)
% 96.76/22.91 % (3659925)Instruction limit reached!
% 96.76/22.91 % (3659925)------------------------------
% 96.76/22.91 % (3659925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659925)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659925)Termination reason: Instruction limit
% 96.76/22.91 % (3659925)Termination phase: Saturation
% 96.76/22.91 % (3659925)Time elapsed: 2.109 s
% 96.76/22.91 % (3659925)Peak memory usage: 135 MB
% 96.76/22.91 % (3659925)Instructions burned: 2088 (million)
% 96.76/22.91 % (3659933)Instruction limit reached!
% 96.76/22.91 % (3659933)------------------------------
% 96.76/22.91 % (3659933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659933)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659933)Termination reason: Instruction limit
% 96.76/22.91 % (3659933)Termination phase: Saturation
% 96.76/22.91 % (3659933)Time elapsed: 0.450 s
% 96.76/22.91 % (3659933)Peak memory usage: 93 MB
% 96.76/22.91 % (3659933)Instructions burned: 433 (million)
% 96.76/22.91 % (3659935)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1763115035:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2877 on theBenchmark for (2877ds/2942Mi)
% 96.76/22.91 % (3659936)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=960501267:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2875 on theBenchmark for (2875ds/6922Mi)
% 96.76/22.91 % (3659899)Instruction limit reached!
% 96.76/22.91 % (3659899)------------------------------
% 96.76/22.91 % (3659899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659899)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659899)Termination reason: Instruction limit
% 96.76/22.91 % (3659899)Termination phase: Saturation
% 96.76/22.91 % (3659899)Time elapsed: 9.482 s
% 96.76/22.91 % (3659899)Peak memory usage: 159 MB
% 96.76/22.91 % (3659899)Instructions burned: 10307 (million)
% 96.76/22.91 % (3659905)Instruction limit reached!
% 96.76/22.91 % (3659905)------------------------------
% 96.76/22.91 % (3659905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659905)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659905)Termination reason: Instruction limit
% 96.76/22.91 % (3659905)Termination phase: Saturation
% 96.76/22.91 % (3659905)Time elapsed: 8.330 s
% 96.76/22.91 % (3659905)Peak memory usage: 191 MB
% 96.76/22.91 % (3659905)Instructions burned: 8479 (million)
% 96.76/22.91 % (3659941)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1974779071:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2864 on theBenchmark for (2864ds/596Mi)
% 96.76/22.91 % (3659942)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=33997337:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2862 on theBenchmark for (2862ds/4123Mi)
% 96.76/22.91 % (3659941)Instruction limit reached!
% 96.76/22.91 % (3659941)------------------------------
% 96.76/22.91 % (3659941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659941)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659941)Termination reason: Instruction limit
% 96.76/22.91 % (3659941)Termination phase: Saturation
% 96.76/22.91 % (3659941)Time elapsed: 0.502 s
% 96.76/22.91 % (3659941)Peak memory usage: 95 MB
% 96.76/22.91 % (3659941)Instructions burned: 597 (million)
% 96.76/22.91 % (3659947)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1572645563:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2856 on theBenchmark for (2856ds/16411Mi)
% 96.76/22.91 % (3659935)Instruction limit reached!
% 96.76/22.91 % (3659935)------------------------------
% 96.76/22.91 % (3659935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659935)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659935)Termination reason: Instruction limit
% 96.76/22.91 % (3659935)Termination phase: Saturation
% 96.76/22.91 % (3659935)Time elapsed: 2.832 s
% 96.76/22.91 % (3659935)Peak memory usage: 139 MB
% 96.76/22.91 % (3659935)Instructions burned: 2942 (million)
% 96.76/22.91 % (3659949)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=327686045:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2847 on theBenchmark for (2847ds/1670Mi)
% 96.76/22.91 % (3659949)Instruction limit reached!
% 96.76/22.91 % (3659949)------------------------------
% 96.76/22.91 % (3659949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659949)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659949)Termination reason: Instruction limit
% 96.76/22.91 % (3659949)Termination phase: Saturation
% 96.76/22.91 % (3659949)Time elapsed: 1.638 s
% 96.76/22.91 % (3659949)Peak memory usage: 135 MB
% 96.76/22.91 % (3659949)Instructions burned: 1670 (million)
% 96.76/22.91 % (3659953)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3393189062:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2828 on theBenchmark for (2828ds/1722Mi)
% 96.76/22.91 % (3659942)Instruction limit reached!
% 96.76/22.91 % (3659942)------------------------------
% 96.76/22.91 % (3659942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659942)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659942)Termination reason: Instruction limit
% 96.76/22.91 % (3659942)Termination phase: Saturation
% 96.76/22.91 % (3659942)Time elapsed: 3.656 s
% 96.76/22.91 % (3659942)Peak memory usage: 165 MB
% 96.76/22.91 % (3659942)Instructions burned: 4123 (million)
% 96.76/22.91 % (3659956)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=321056018:cts=off:cond=on:i=9530:bs=on:fsd=on_2823 on theBenchmark for (2823ds/9530Mi)
% 96.76/22.91 % (3659953)Instruction limit reached!
% 96.76/22.91 % (3659953)------------------------------
% 96.76/22.91 % (3659953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659953)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659953)Termination reason: Instruction limit
% 96.76/22.91 % (3659953)Termination phase: Saturation
% 96.76/22.91 % (3659953)Time elapsed: 1.819 s
% 96.76/22.91 % (3659953)Peak memory usage: 135 MB
% 96.76/22.91 % (3659953)Instructions burned: 1722 (million)
% 96.76/22.91 % (3659936)Instruction limit reached!
% 96.76/22.91 % (3659936)------------------------------
% 96.76/22.91 % (3659936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.76/22.91 % (3659936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.76/22.91 % (3659936)CaDiCaL version: 2.1.3
% 96.76/22.91 % (3659936)Termination reason: Instruction limit
% 96.76/22.91 % (3659936)Termination phase: Saturation
% 96.76/22.91 % (3659936)Time elapsed: 6.593 s
% 96.76/22.91 % (3659936)Peak memory usage: 171 MB
% 96.76/22.91 % (3659936)Instructions burned: 6922 (million)
% 96.76/22.91 % (3659958)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1880278142:st=2:i=4495:sd=10:ss=included_2808 on theBenchmark for (2808ds/4495Mi)
% 96.76/22.91 % (3659959)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=23487902:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2807 on theBenchmark for (2807ds/4920Mi)
% 96.76/22.91 % (3659958)First to succeed.
% 96.76/22.91 % (3659958)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3659822"
% 96.76/22.91 % (3659958)Refutation found. Thanks to Tanya!
% 96.76/22.91 % SZS status Unsatisfiable for theBenchmark
% 96.76/22.91 % SZS output start Proof for theBenchmark
% See solution above
% 155.17/23.12 % (3659958)------------------------------
% 155.17/23.12 % (3659958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.17/23.12 % (3659958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.17/23.12 % (3659958)CaDiCaL version: 2.1.3
% 155.17/23.12 % (3659958)Termination reason: Refutation
% 155.17/23.12 % (3659958)Time elapsed: 1.888 s
% 155.17/23.12 % (3659958)Peak memory usage: 136 MB
% 155.17/23.12 % (3659958)Instructions burned: 1774 (million)
% 155.17/23.12 % (3659958)------------------------------
% 155.17/23.12 % (3659958)------------------------------
% 155.17/23.12 % (3659822)Success in time 21.804 s
% 155.17/23.12 % Vampire exiting
%------------------------------------------------------------------------------