%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL024-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:57:26 AM UTC 2026
% Result : Unsatisfiable 133.53s 19.37s
% Output : Refutation 133.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 3
% Syntax : Number of formulae : 26 ( 23 unt; 0 def)
% Number of atoms : 31 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 27 ( 22 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 85 ( 85 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xgk) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_pyo) ).
fof(f4,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(X4,X2)),equivalent(X4,X3))))),equivalent(X1,X0))),
inference(unit_resulting_resolution,[],[f1,f2,f2]) ).
fof(f5,plain,
! [X2,X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1))),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a)))),
inference(unit_resulting_resolution,[],[f1,f3,f2]) ).
fof(f7,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f8,plain,
! [X2,X3,X0,X1,X4,X5] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1))),equivalent(equivalent(X3,equivalent(equivalent(X4,equivalent(X5,X3)),equivalent(X5,X4))),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))))),
inference(unit_resulting_resolution,[],[f1,f2,f5]) ).
fof(f10,plain,
! [X0] : ~ is_a_theorem(equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X0)),X0)),
inference(unit_resulting_resolution,[],[f1,f2,f8]) ).
fof(f11,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1))),equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X3)),X3))),
inference(unit_resulting_resolution,[],[f1,f2,f10]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X6,X4,X5] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X2,X1))),equivalent(equivalent(X3,equivalent(equivalent(X4,equivalent(X5,X3)),equivalent(X5,X4))),equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X6)),X6)))),
inference(unit_resulting_resolution,[],[f1,f2,f11]) ).
fof(f16,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X0)),X1)),X1)),
inference(unit_resulting_resolution,[],[f1,f2,f13]) ).
fof(f258,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(X0)
| is_a_theorem(equivalent(X2,X1)) ),
inference(resolution,[],[f7,f1]) ).
fof(f416,plain,
! [X2,X3,X0,X1,X4] : ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X1)),X0)),equivalent(X2,equivalent(equivalent(X3,equivalent(X4,X2)),equivalent(X4,X3)))))),
inference(unit_resulting_resolution,[],[f1,f16,f4]) ).
fof(f518,plain,
! [X2,X3,X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X1,X0)),equivalent(X2,X3)),X3)),
inference(unit_resulting_resolution,[],[f1,f2,f4]) ).
fof(f519,plain,
! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X1)),equivalent(X3,X2))),equivalent(X0,equivalent(X4,equivalent(equivalent(X5,equivalent(X6,X4)),equivalent(X6,X5))))))),
inference(unit_resulting_resolution,[],[f1,f4,f4]) ).
fof(f638,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(b,a),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),X0)),X1)),equivalent(X2,equivalent(equivalent(X3,equivalent(X4,X2)),equivalent(X4,X3)))),equivalent(X1,equivalent(X5,equivalent(equivalent(X6,equivalent(X7,X5)),equivalent(X7,X6)))))),
inference(unit_resulting_resolution,[],[f1,f4,f416]) ).
fof(f708,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a)))),equivalent(X1,X0))),
inference(unit_resulting_resolution,[],[f7,f638]) ).
fof(f2330,plain,
! [X2,X3,X0,X1,X4] : ~ is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X1,X0)),equivalent(X2,equivalent(equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a)))),equivalent(X4,X3))))),
inference(unit_resulting_resolution,[],[f1,f708,f518]) ).
fof(f2384,plain,
! [X0] : is_a_theorem(equivalent(X0,X0)),
inference(unit_resulting_resolution,[],[f1,f518,f518]) ).
fof(f3458,plain,
! [X0] : ~ is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))))),
inference(unit_resulting_resolution,[],[f7,f2330]) ).
fof(f3470,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),equivalent(X0,equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X1)),equivalent(X3,X2)))))),
inference(unit_resulting_resolution,[],[f258,f2,f3458]) ).
fof(f3491,plain,
! [X0,X1] : ~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(equivalent(X0,equivalent(X1,equivalent(b,a))),equivalent(X1,X0)))),
inference(unit_resulting_resolution,[],[f258,f518,f3470]) ).
fof(f21928,plain,
! [X2,X0,X1] : ~ is_a_theorem(equivalent(equivalent(X0,X0),equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(equivalent(X1,equivalent(X2,equivalent(b,a))),equivalent(X2,X1))))),
inference(unit_resulting_resolution,[],[f1,f3491,f2384]) ).
fof(f26276,plain,
! [X2,X0,X1] : ~ is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(equivalent(X1,equivalent(X2,equivalent(b,a))),equivalent(X2,X1)))))),
inference(unit_resulting_resolution,[],[f258,f2,f21928]) ).
fof(f26812,plain,
! [X0] : ~ is_a_theorem(equivalent(X0,equivalent(equivalent(b,a),equivalent(X0,equivalent(equivalent(a,equivalent(b,c)),c))))),
inference(unit_resulting_resolution,[],[f258,f518,f26276]) ).
fof(f26832,plain,
$false,
inference(unit_resulting_resolution,[],[f258,f2384,f519,f26812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL024-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.18/0.46 % Computer : n003.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Sun Sep 27 15:19:26 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.51 Running first-order model finding
% 0.24/0.51 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.31/4.57 % (686754)Will run a generic schedule for satisfiability detection.
% 28.31/4.57 % (686763)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4144953738:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 28.31/4.57 % (686760)% WARNING: option uhcvi not known.
% 28.31/4.57 % (686761)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3906747717:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 28.31/4.57 % (686764)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1423682052:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 28.31/4.57 % (686760)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4122759665:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 28.31/4.57 % (686765)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1856081856:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 28.31/4.57 % (686762)dis+10_1_sil=32000:sp=arity:random_seed=812661584:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 28.31/4.57 % (686759)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3322504305_3000 on theBenchmark for (3000ds/0Mi)
% 28.31/4.57 % TRYING [1]
% 28.31/4.57 % TRYING [2]
% 28.31/4.57 % TRYING [3]
% 28.31/4.57 % TRYING [4]
% 28.31/4.57 % (686763)Instruction limit reached!
% 28.31/4.57 % (686763)------------------------------
% 28.31/4.57 % (686763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.31/4.57 % (686763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.31/4.57 % (686763)CaDiCaL version: 2.1.3
% 28.31/4.57 % (686763)Termination reason: Instruction limit
% 28.31/4.57 % (686763)Termination phase: Saturation
% 28.31/4.57 % (686763)Time elapsed: 0.058 s
% 28.31/4.57 % (686763)Peak memory usage: 12 MB
% 28.31/4.57 % (686763)Instructions burned: 117 (million)
% 28.31/4.57 % (686773)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=668641801:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 28.31/4.57 % TRYING [1]
% 28.31/4.57 % TRYING [2]
% 28.31/4.57 % TRYING [3]
% 28.31/4.57 % TRYING [4]
% 28.31/4.57 % (686762)Instruction limit reached!
% 28.31/4.57 % (686762)------------------------------
% 28.31/4.57 % (686762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.31/4.57 % (686762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.31/4.57 % (686762)CaDiCaL version: 2.1.3
% 28.31/4.57 % (686762)Termination reason: Instruction limit
% 28.31/4.57 % (686762)Termination phase: Saturation
% 28.31/4.57 % (686762)Time elapsed: 0.102 s
% 28.31/4.57 % (686762)Peak memory usage: 11 MB
% 28.31/4.57 % (686762)Instructions burned: 103 (million)
% 28.31/4.57 % (686764)Instruction limit reached!
% 28.31/4.57 % (686764)------------------------------
% 28.31/4.57 % (686764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.31/4.57 % (686764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.31/4.57 % (686764)CaDiCaL version: 2.1.3
% 28.31/4.57 % (686764)Termination reason: Instruction limit
% 28.31/4.57 % (686764)Termination phase: Saturation
% 28.31/4.57 % (686764)Time elapsed: 0.125 s
% 28.31/4.57 % (686764)Peak memory usage: 12 MB
% 28.31/4.57 % (686764)Instructions burned: 131 (million)
% 28.31/4.57 % (686775)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2876914671:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.31/4.57 % (686765)Instruction limit reached!
% 28.31/4.57 % (686765)------------------------------
% 28.31/4.57 % (686765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.31/4.57 % (686765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.31/4.57 % (686765)CaDiCaL version: 2.1.3
% 28.31/4.57 % (686765)Termination reason: Instruction limit
% 28.31/4.57 % (686765)Termination phase: Saturation
% 28.31/4.57 % (686765)Time elapsed: 0.163 s
% 28.31/4.57 % (686765)Peak memory usage: 13 MB
% 28.31/4.57 % (686765)Instructions burned: 160 (million)
% 28.31/4.57 % (686776)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=723983221:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.31/4.57 % (686778)ott-21_1_sil=16000:fs=off:random_seed=673975783:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 28.31/4.57 % (686775)Instruction limit reached!
% 28.31/4.57 % (686775)------------------------------
% 28.31/4.57 % (686775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.31/4.57 % (686775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686775)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686775)Termination reason: Instruction limit
% 66.70/10.04 % (686775)Termination phase: Saturation
% 66.70/10.04 % (686775)Time elapsed: 0.101 s
% 66.70/10.04 % (686775)Peak memory usage: 12 MB
% 66.70/10.04 % (686775)Instructions burned: 131 (million)
% 66.70/10.04 % (686781)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3524153024:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 66.70/10.04 % TRYING [5]
% 66.70/10.04 % (686778)Instruction limit reached!
% 66.70/10.04 % (686778)------------------------------
% 66.70/10.04 % (686778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686778)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686778)Termination reason: Instruction limit
% 66.70/10.04 % (686778)Termination phase: Saturation
% 66.70/10.04 % (686778)Time elapsed: 0.159 s
% 66.70/10.04 % (686778)Peak memory usage: 13 MB
% 66.70/10.04 % (686778)Instructions burned: 181 (million)
% 66.70/10.04 % (686783)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1827471079:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 66.70/10.04 % TRYING [1]
% 66.70/10.04 % TRYING [2]
% 66.70/10.04 % TRYING [3]
% 66.70/10.04 % (686773)Instruction limit reached!
% 66.70/10.04 % (686773)------------------------------
% 66.70/10.04 % (686773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686773)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686773)Termination reason: Instruction limit
% 66.70/10.04 % (686773)Termination phase: Finite model building SAT solving
% 66.70/10.04 % (686773)Time elapsed: 0.337 s
% 66.70/10.04 % (686773)Peak memory usage: 13 MB
% 66.70/10.04 % (686773)Instructions burned: 714 (million)
% 66.70/10.04 % TRYING [4]
% 66.70/10.04 % (686785)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2631742706:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 66.70/10.04 % TRYING [5]
% 66.70/10.04 % TRYING [5]
% 66.70/10.04 % (686781)Instruction limit reached!
% 66.70/10.04 % (686781)------------------------------
% 66.70/10.04 % (686781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686781)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686781)Termination reason: Instruction limit
% 66.70/10.04 % (686781)Termination phase: Saturation
% 66.70/10.04 % (686781)Time elapsed: 0.465 s
% 66.70/10.04 % (686781)Peak memory usage: 13 MB
% 66.70/10.04 % (686781)Instructions burned: 478 (million)
% 66.70/10.04 % (686788)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2271024110:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 66.70/10.04 % (686776)Instruction limit reached!
% 66.70/10.04 % (686776)------------------------------
% 66.70/10.04 % (686776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686776)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686776)Termination reason: Instruction limit
% 66.70/10.04 % (686776)Termination phase: Saturation
% 66.70/10.04 % (686776)Time elapsed: 0.664 s
% 66.70/10.04 % (686776)Peak memory usage: 17 MB
% 66.70/10.04 % (686776)Instructions burned: 684 (million)
% 66.70/10.04 % TRYING [14]
% 66.70/10.04 % (686791)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=4153877075:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 66.70/10.04 % (686785)Instruction limit reached!
% 66.70/10.04 % (686785)------------------------------
% 66.70/10.04 % (686785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.70/10.04 % (686785)CaDiCaL version: 2.1.3
% 66.70/10.04 % (686785)Termination reason: Instruction limit
% 66.70/10.04 % (686785)Termination phase: Saturation
% 66.70/10.04 % (686785)Time elapsed: 0.597 s
% 66.70/10.04 % (686785)Peak memory usage: 20 MB
% 66.70/10.04 % (686785)Instructions burned: 1180 (million)
% 66.70/10.04 % (686793)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1061190135:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 66.70/10.04 % (686783)Instruction limit reached!
% 66.70/10.04 % (686783)------------------------------
% 66.70/10.04 % (686783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.70/10.04 % (686783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686783)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686783)Termination reason: Instruction limit
% 133.53/19.37 % (686783)Termination phase: Finite model building SAT solving
% 133.53/19.37 % (686783)Time elapsed: 0.767 s
% 133.53/19.37 % (686783)Peak memory usage: 13 MB
% 133.53/19.37 % (686783)Instructions burned: 866 (million)
% 133.53/19.37 % (686795)fmb+10_1_sil=64000:random_seed=3878768217:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 133.53/19.37 % TRYING [1]
% 133.53/19.37 % TRYING [2]
% 133.53/19.37 % TRYING [3]
% 133.53/19.37 % TRYING [4]
% 133.53/19.37 % TRYING [5]
% 133.53/19.37 % (686788)Instruction limit reached!
% 133.53/19.37 % (686788)------------------------------
% 133.53/19.37 % (686788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686788)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686788)Termination reason: Instruction limit
% 133.53/19.37 % (686788)Termination phase: Finite model building constraint generation
% 133.53/19.37 % (686788)Time elapsed: 0.650 s
% 133.53/19.37 % (686788)Peak memory usage: 63 MB
% 133.53/19.37 % (686788)Instructions burned: 889 (million)
% 133.53/19.37 % (686793)Instruction limit reached!
% 133.53/19.37 % (686793)------------------------------
% 133.53/19.37 % (686793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686793)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686793)Termination reason: Instruction limit
% 133.53/19.37 % (686793)Termination phase: Saturation
% 133.53/19.37 % (686793)Time elapsed: 0.419 s
% 133.53/19.37 % (686793)Peak memory usage: 19 MB
% 133.53/19.37 % (686793)Instructions burned: 881 (million)
% 133.53/19.37 % (686797)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1325566994:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 133.53/19.37 % (686798)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2712198198:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 133.53/19.37 % TRYING [8]
% 133.53/19.37 % TRYING [20]
% 133.53/19.37 % (686791)Instruction limit reached!
% 133.53/19.37 % (686791)------------------------------
% 133.53/19.37 % (686791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686791)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686791)Termination reason: Instruction limit
% 133.53/19.37 % (686791)Termination phase: Saturation
% 133.53/19.37 % (686791)Time elapsed: 0.759 s
% 133.53/19.37 % (686791)Peak memory usage: 20 MB
% 133.53/19.37 % (686791)Instructions burned: 693 (million)
% 133.53/19.37 % (686801)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3426001144:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 133.53/19.37 % (686798)Instruction limit reached!
% 133.53/19.37 % (686798)------------------------------
% 133.53/19.37 % (686798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686798)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686798)Termination reason: Instruction limit
% 133.53/19.37 % (686798)Termination phase: Finite model building SAT solving
% 133.53/19.37 % (686798)Time elapsed: 0.436 s
% 133.53/19.37 % (686798)Peak memory usage: 32 MB
% 133.53/19.37 % (686798)Instructions burned: 921 (million)
% 133.53/19.37 % (686803)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=444340356:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 133.53/19.37 % (686803)Instruction limit reached!
% 133.53/19.37 % (686803)------------------------------
% 133.53/19.37 % (686803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686803)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686803)Termination reason: Instruction limit
% 133.53/19.37 % (686803)Termination phase: Saturation
% 133.53/19.37 % (686803)Time elapsed: 1.323 s
% 133.53/19.37 % (686803)Peak memory usage: 24 MB
% 133.53/19.37 % (686803)Instructions burned: 1472 (million)
% 133.53/19.37 % (686805)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=10669607:i=6324_2966 on theBenchmark for (2966ds/6324Mi)
% 133.53/19.37 % TRYING [77]
% 133.53/19.37 % (686801)Instruction limit reached!
% 133.53/19.37 % (686801)------------------------------
% 133.53/19.37 % (686801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686801)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686801)Termination reason: Instruction limit
% 133.53/19.37 % (686801)Termination phase: Saturation
% 133.53/19.37 % (686801)Time elapsed: 2.353 s
% 133.53/19.37 % (686801)Peak memory usage: 25 MB
% 133.53/19.37 % (686801)Instructions burned: 5134 (million)
% 133.53/19.37 % (686807)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2542906558:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 133.53/19.37 % TRYING [16]
% 133.53/19.37 % (686807)Instruction limit reached!
% 133.53/19.37 % (686807)------------------------------
% 133.53/19.37 % (686807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686807)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686807)Termination reason: Instruction limit
% 133.53/19.37 % (686807)Termination phase: Finite model building constraint generation
% 133.53/19.37 % (686807)Time elapsed: 0.835 s
% 133.53/19.37 % (686807)Peak memory usage: 155 MB
% 133.53/19.37 % (686807)Instructions burned: 2176 (million)
% 133.53/19.37 % (686811)ott-2_1_sil=16000:newcnf=on:random_seed=3366298472:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2950 on theBenchmark for (2950ds/869Mi)
% 133.53/19.37 % (686811)Instruction limit reached!
% 133.53/19.37 % (686811)------------------------------
% 133.53/19.37 % (686811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686811)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686811)Termination reason: Instruction limit
% 133.53/19.37 % (686811)Termination phase: Saturation
% 133.53/19.37 % (686811)Time elapsed: 0.409 s
% 133.53/19.37 % (686811)Peak memory usage: 14 MB
% 133.53/19.37 % (686811)Instructions burned: 870 (million)
% 133.53/19.37 % (686813)ott+10_1_sil=32000:tgt=ground:random_seed=2353259462:i=5114:av=off_2946 on theBenchmark for (2946ds/5114Mi)
% 133.53/19.37 % (686805)Instruction limit reached!
% 133.53/19.37 % (686805)------------------------------
% 133.53/19.37 % (686805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686805)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686805)Termination reason: Instruction limit
% 133.53/19.37 % (686805)Termination phase: Finite model building constraint generation
% 133.53/19.37 % (686805)Time elapsed: 4.554 s
% 133.53/19.37 % (686805)Peak memory usage: 430 MB
% 133.53/19.37 % (686805)Instructions burned: 6326 (million)
% 133.53/19.37 % (686819)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3177484347:i=54282_2920 on theBenchmark for (2920ds/54282Mi)
% 133.53/19.37 % TRYING [1]
% 133.53/19.37 % TRYING [2]
% 133.53/19.37 % TRYING [3]
% 133.53/19.37 % (686813)Instruction limit reached!
% 133.53/19.37 % (686813)------------------------------
% 133.53/19.37 % (686813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686813)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686813)Termination reason: Instruction limit
% 133.53/19.37 % (686813)Termination phase: Saturation
% 133.53/19.37 % (686813)Time elapsed: 2.656 s
% 133.53/19.37 % (686813)Peak memory usage: 21 MB
% 133.53/19.37 % (686813)Instructions burned: 5116 (million)
% 133.53/19.37 % TRYING [4]
% 133.53/19.37 % (686821)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3755061472:i=3512:aac=none_2919 on theBenchmark for (2919ds/3512Mi)
% 133.53/19.37 % TRYING [5]
% 133.53/19.37 % (686797)Instruction limit reached!
% 133.53/19.37 % (686797)------------------------------
% 133.53/19.37 % (686797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686797)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686797)Termination reason: Instruction limit
% 133.53/19.37 % (686797)Termination phase: Finite model building constraint generation
% 133.53/19.37 % (686797)Time elapsed: 7.679 s
% 133.53/19.37 % (686797)Peak memory usage: 592 MB
% 133.53/19.37 % (686797)Instructions burned: 9515 (million)
% 133.53/19.37 % (686823)dis+21_1_sil=32000:sas=cadical:random_seed=3835288922:i=3773:amm=off_2906 on theBenchmark for (2906ds/3773Mi)
% 133.53/19.37 % (686821)Instruction limit reached!
% 133.53/19.37 % (686821)------------------------------
% 133.53/19.37 % (686821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686821)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686821)Termination reason: Instruction limit
% 133.53/19.37 % (686821)Termination phase: Saturation
% 133.53/19.37 % (686821)Time elapsed: 1.445 s
% 133.53/19.37 % (686821)Peak memory usage: 22 MB
% 133.53/19.37 % (686821)Instructions burned: 3514 (million)
% 133.53/19.37 % (686825)ott+11_1_sil=16000:gs=on:random_seed=2495895385:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2904 on theBenchmark for (2904ds/2251Mi)
% 133.53/19.37 % TRYING [6]
% 133.53/19.37 % (686825)Instruction limit reached!
% 133.53/19.37 % (686825)------------------------------
% 133.53/19.37 % (686825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686825)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686825)Termination reason: Instruction limit
% 133.53/19.37 % (686825)Termination phase: Saturation
% 133.53/19.37 % (686825)Time elapsed: 0.999 s
% 133.53/19.37 % (686825)Peak memory usage: 30 MB
% 133.53/19.37 % (686825)Instructions burned: 2252 (million)
% 133.53/19.37 % (686827)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1733661122:fmbsr=1.6:i=67534_2894 on theBenchmark for (2894ds/67534Mi)
% 133.53/19.37 % TRYING [7]
% 133.53/19.37 % (686823)Instruction limit reached!
% 133.53/19.37 % (686823)------------------------------
% 133.53/19.37 % (686823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686823)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686823)Termination reason: Instruction limit
% 133.53/19.37 % (686823)Termination phase: Saturation
% 133.53/19.37 % (686823)Time elapsed: 3.430 s
% 133.53/19.37 % (686823)Peak memory usage: 24 MB
% 133.53/19.37 % (686823)Instructions burned: 3773 (million)
% 133.53/19.37 % (686829)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3417972212:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2871 on theBenchmark for (2871ds/4591Mi)
% 133.53/19.37 % TRYING [6]
% 133.53/19.37 % (686829)Instruction limit reached!
% 133.53/19.37 % (686829)------------------------------
% 133.53/19.37 % (686829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686829)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686829)Termination reason: Instruction limit
% 133.53/19.37 % (686829)Termination phase: Saturation
% 133.53/19.37 % (686829)Time elapsed: 3.614 s
% 133.53/19.37 % (686829)Peak memory usage: 47 MB
% 133.53/19.37 % (686829)Instructions burned: 4591 (million)
% 133.53/19.37 % (686833)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=625368734:i=29340_2835 on theBenchmark for (2835ds/29340Mi)
% 133.53/19.37 % TRYING [6]
% 133.53/19.37 % (686833) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-686754-686833"...
% 133.53/19.37 % (686833)...printing done.
% 133.53/19.37 % (686833)Refutation found. Thanks to Tanya!
% 133.53/19.37 % SZS status Unsatisfiable for theBenchmark
% 133.53/19.37 % SZS output start Proof for theBenchmark
% See solution above
% 133.53/19.37 % (686833)------------------------------
% 133.53/19.37 % (686833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.53/19.37 % (686833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.53/19.37 % (686833)CaDiCaL version: 2.1.3
% 133.53/19.37 % (686833)Termination reason: Refutation
% 133.53/19.37 % (686833)Time elapsed: 2.284 s
% 133.53/19.37 % (686833)Peak memory usage: 24 MB
% 133.53/19.37 % (686833)Instructions burned: 2641 (million)
% 133.53/19.37 % (686754)Success in time 18.849 s
% 133.53/19.37 % Vampire exiting
%------------------------------------------------------------------------------