%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET016-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:42:37 PM UTC 2026
% Result : Unsatisfiable 126.24s 35.10s
% Output : Refutation 126.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 18
% Syntax : Number of formulae : 81 ( 23 unt; 8 def)
% Number of atoms : 163 ( 36 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 152 ( 70 ~; 74 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 22 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X2,X0,X1] :
( ~ member(X0,non_ordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair2) ).
fof(f7,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair3) ).
fof(f8,axiom,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair4) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',singleton_set) ).
fof(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair) ).
fof(f162,axiom,
little_set(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',little_set_a) ).
fof(f163,axiom,
little_set(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',little_set_b) ).
fof(f164,axiom,
ordered_pair(a,c) = ordered_pair(b,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_ordered_pairs) ).
fof(f165,negated_conjecture,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_first_components_equal) ).
fof(f167,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),
inference(definition_unfolding,[],[f10,f9]) ).
fof(f194,plain,
non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c)) = non_ordered_pair(non_ordered_pair(b,b),non_ordered_pair(b,d)),
inference(definition_unfolding,[],[f164,f167,f167]) ).
fof(f195,plain,
! [X2,X1] :
( member(X1,non_ordered_pair(X1,X2))
| ~ little_set(X1) ),
inference(equality_resolution,[],[f6]) ).
fof(f196,plain,
! [X2,X1] :
( member(X2,non_ordered_pair(X1,X2))
| ~ little_set(X2) ),
inference(equality_resolution,[],[f7]) ).
fof(f1581,plain,
( member(non_ordered_pair(b,b),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c)))
| ~ little_set(non_ordered_pair(b,b)) ),
inference(superposition,[],[f195,f194]) ).
fof(f1582,plain,
( member(non_ordered_pair(b,d),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c)))
| ~ little_set(non_ordered_pair(b,d)) ),
inference(superposition,[],[f196,f194]) ).
fof(f1591,definition,
( spl0_22
<=> little_set(non_ordered_pair(b,d)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1593,plain,
( ~ little_set(non_ordered_pair(b,d))
| spl0_22 ),
inference(avatar_component_clause,[],[f1591]) ).
fof(f1604,definition,
( spl0_25
<=> little_set(non_ordered_pair(b,b)) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f1606,plain,
( ~ little_set(non_ordered_pair(b,b))
| spl0_25 ),
inference(avatar_component_clause,[],[f1604]) ).
fof(f1614,definition,
( spl0_27
<=> member(non_ordered_pair(b,d),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c))) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f1616,plain,
( member(non_ordered_pair(b,d),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c)))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1617,plain,
( ~ spl0_22
| spl0_27 ),
inference(avatar_split_clause,[],[f1582,f1614,f1591]) ).
fof(f1619,definition,
( spl0_28
<=> member(non_ordered_pair(b,b),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1621,plain,
( member(non_ordered_pair(b,b),non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,c)))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1619]) ).
fof(f1622,plain,
( ~ spl0_25
| spl0_28 ),
inference(avatar_split_clause,[],[f1581,f1619,f1604]) ).
fof(f1653,plain,
( $false
| spl0_22 ),
inference(resolution,[],[f1593,f8]) ).
fof(f1654,plain,
spl0_22,
inference(avatar_contradiction_clause,[],[f1653]) ).
fof(f1823,plain,
( $false
| spl0_25 ),
inference(resolution,[],[f1606,f8]) ).
fof(f1824,plain,
spl0_25,
inference(avatar_contradiction_clause,[],[f1823]) ).
fof(f6828,plain,
( non_ordered_pair(a,a) = non_ordered_pair(b,d)
| non_ordered_pair(a,c) = non_ordered_pair(b,d)
| ~ spl0_27 ),
inference(resolution,[],[f1616,f5]) ).
fof(f6844,definition,
( spl0_67
<=> non_ordered_pair(a,c) = non_ordered_pair(b,d) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f6846,plain,
( non_ordered_pair(a,c) = non_ordered_pair(b,d)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f6844]) ).
fof(f6848,definition,
( spl0_68
<=> non_ordered_pair(a,a) = non_ordered_pair(b,d) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f6850,plain,
( non_ordered_pair(a,a) = non_ordered_pair(b,d)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f6848]) ).
fof(f6851,plain,
( spl0_67
| spl0_68
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f6828,f1614,f6848,f6844]) ).
fof(f6858,plain,
( non_ordered_pair(a,a) = non_ordered_pair(b,b)
| non_ordered_pair(a,c) = non_ordered_pair(b,b)
| ~ spl0_28 ),
inference(resolution,[],[f1621,f5]) ).
fof(f6865,definition,
( spl0_69
<=> non_ordered_pair(a,c) = non_ordered_pair(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f6867,plain,
( non_ordered_pair(a,c) = non_ordered_pair(b,b)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f6865]) ).
fof(f6869,definition,
( spl0_70
<=> non_ordered_pair(a,a) = non_ordered_pair(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f6871,plain,
( non_ordered_pair(a,a) = non_ordered_pair(b,b)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f6869]) ).
fof(f6872,plain,
( spl0_69
| spl0_70
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f6858,f1619,f6869,f6865]) ).
fof(f7305,plain,
( member(b,non_ordered_pair(a,c))
| ~ little_set(b)
| ~ spl0_67 ),
inference(superposition,[],[f195,f6846]) ).
fof(f7316,plain,
( member(b,non_ordered_pair(a,c))
| ~ spl0_67 ),
inference(global_subsumption,[],[f7305,f163]) ).
fof(f7327,plain,
( a = b
| b = c
| ~ spl0_67 ),
inference(resolution,[],[f7316,f5]) ).
fof(f7342,plain,
( b = c
| ~ spl0_67 ),
inference(global_subsumption,[],[f7327,f165]) ).
fof(f7376,plain,
( member(b,non_ordered_pair(a,a))
| ~ little_set(b)
| ~ spl0_68 ),
inference(superposition,[],[f195,f6850]) ).
fof(f7387,plain,
( member(b,non_ordered_pair(a,a))
| ~ spl0_68 ),
inference(global_subsumption,[],[f7376,f163]) ).
fof(f7396,plain,
( a = b
| a = b
| ~ spl0_68 ),
inference(resolution,[],[f7387,f5]) ).
fof(f7402,plain,
( a = b
| ~ spl0_68 ),
inference(duplicate_literal_removal,[],[f7396]) ).
fof(f7408,plain,
( $false
| ~ spl0_68 ),
inference(global_subsumption,[],[f7402,f165]) ).
fof(f7409,plain,
~ spl0_68,
inference(avatar_contradiction_clause,[],[f7408]) ).
fof(f7616,plain,
( member(b,non_ordered_pair(a,a))
| ~ little_set(b)
| ~ spl0_70 ),
inference(superposition,[],[f196,f6871]) ).
fof(f7639,plain,
( member(b,non_ordered_pair(a,a))
| ~ spl0_70 ),
inference(global_subsumption,[],[f7616,f163]) ).
fof(f7663,plain,
( non_ordered_pair(b,b) = non_ordered_pair(a,b)
| ~ spl0_67
| ~ spl0_69 ),
inference(forward_demodulation,[],[f6867,f7342]) ).
fof(f7979,plain,
( a = b
| a = b
| ~ spl0_70 ),
inference(resolution,[],[f7639,f5]) ).
fof(f7985,plain,
( a = b
| ~ spl0_70 ),
inference(duplicate_literal_removal,[],[f7979]) ).
fof(f7986,plain,
( $false
| ~ spl0_70 ),
inference(global_subsumption,[],[f7985,f165]) ).
fof(f7987,plain,
~ spl0_70,
inference(avatar_contradiction_clause,[],[f7986]) ).
fof(f8009,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(a,b))
| b = X0
| b = X0 )
| ~ spl0_67
| ~ spl0_69 ),
inference(superposition,[],[f5,f7663]) ).
fof(f8029,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(a,b))
| b = X0 )
| ~ spl0_67
| ~ spl0_69 ),
inference(duplicate_literal_removal,[],[f8009]) ).
fof(f9870,plain,
( a = b
| ~ little_set(a)
| ~ spl0_67
| ~ spl0_69 ),
inference(resolution,[],[f8029,f195]) ).
fof(f9959,plain,
( $false
| ~ spl0_67
| ~ spl0_69 ),
inference(global_subsumption,[],[f9870,f162,f165]) ).
fof(f9960,plain,
( ~ spl0_67
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f9959]) ).
cnf(s761,plain,
( ~ spl0_22
| spl0_27 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s763,plain,
( ~ spl0_25
| spl0_28 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s776,plain,
spl0_22,
inference(sat_conversion,[],[f1654]) ).
cnf(s855,plain,
spl0_25,
inference(sat_conversion,[],[f1824]) ).
cnf(s2072,plain,
( ~ spl0_27
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f6851]) ).
cnf(s2079,plain,
( ~ spl0_28
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f6872]) ).
cnf(s2230,plain,
~ spl0_68,
inference(sat_conversion,[],[f7409]) ).
cnf(s2487,plain,
~ spl0_70,
inference(sat_conversion,[],[f7987]) ).
cnf(s2992,plain,
( ~ spl0_67
| ~ spl0_69 ),
inference(sat_conversion,[],[f9960]) ).
cnf(s2994,plain,
( ~ spl0_28
| spl0_69 ),
inference(rat,[],[s2079,s2487]) ).
cnf(s2995,plain,
( ~ spl0_27
| spl0_67 ),
inference(rat,[],[s2072,s2230]) ).
cnf(s3003,plain,
spl0_28,
inference(rat,[],[s763,s855]) ).
cnf(s3004,plain,
spl0_69,
inference(rat,[],[s2994,s3003]) ).
cnf(s3005,plain,
~ spl0_67,
inference(rat,[],[s2992,s3004]) ).
cnf(s3006,plain,
~ spl0_27,
inference(rat,[],[s2995,s3005]) ).
cnf(s3007,plain,
$false,
inference(rat,[],[s761,s3006,s776]) ).
fof(f9961,plain,
$false,
inference(avatar_sat_refutation,[],[s3007]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET016-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 00:08:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 Running first-order model finding
% 0.13/0.39 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
% 6.87/1.46 % (3540681)Will run a generic schedule for satisfiability detection.
% 6.87/1.46 % (3540697)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1865316302:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.87/1.46 % (3540694)% WARNING: option uhcvi not known.
% 6.87/1.46 % (3540693)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=782316124_2999 on theBenchmark for (2999ds/0Mi)
% 6.87/1.46 % (3540696)dis+10_1_sil=32000:sp=arity:random_seed=2833871495:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.87/1.46 % (3540698)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2419647852:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.87/1.46 % (3540695)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2071710789:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.87/1.46 % (3540699)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2763639769:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.87/1.46 % (3540694)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4095720375:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.87/1.46 % TRYING [1]
% 6.87/1.46 % TRYING [2]
% 6.87/1.46 % (3540697)Instruction limit reached!
% 6.87/1.46 % (3540697)------------------------------
% 6.87/1.46 % (3540697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.46 % (3540697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.46 % (3540697)CaDiCaL version: 2.1.3
% 6.87/1.46 % (3540697)Termination reason: Instruction limit
% 6.87/1.46 % (3540697)Termination phase: Saturation
% 6.87/1.46 % (3540697)Time elapsed: 0.039 s
% 6.87/1.46 % (3540697)Peak memory usage: 13 MB
% 6.87/1.46 % (3540697)Instructions burned: 119 (million)
% 6.87/1.46 % TRYING [3]
% 6.87/1.46 % (3540725)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=444868409:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.87/1.46 % TRYING [1]
% 6.87/1.46 % TRYING [2]
% 6.87/1.46 % TRYING [3]
% 6.87/1.46 % (3540696)Instruction limit reached!
% 6.87/1.46 % (3540696)------------------------------
% 6.87/1.46 % (3540696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.46 % (3540696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.46 % (3540696)CaDiCaL version: 2.1.3
% 6.87/1.46 % (3540696)Termination reason: Instruction limit
% 6.87/1.46 % (3540696)Termination phase: Saturation
% 6.87/1.46 % (3540696)Time elapsed: 0.064 s
% 6.87/1.46 % (3540696)Peak memory usage: 12 MB
% 6.87/1.46 % (3540696)Instructions burned: 104 (million)
% 6.87/1.46 % (3540698)Instruction limit reached!
% 6.87/1.46 % (3540698)------------------------------
% 6.87/1.46 % (3540698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.46 % (3540698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.46 % (3540698)CaDiCaL version: 2.1.3
% 6.87/1.46 % (3540698)Termination reason: Instruction limit
% 6.87/1.46 % (3540698)Termination phase: Saturation
% 6.87/1.46 % (3540698)Time elapsed: 0.078 s
% 6.87/1.46 % (3540698)Peak memory usage: 13 MB
% 6.87/1.46 % (3540698)Instructions burned: 132 (million)
% 6.87/1.46 % (3540734)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2969473433:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.87/1.46 % (3540736)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=2307215004:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.87/1.46 % (3540699)Instruction limit reached!
% 6.87/1.46 % (3540699)------------------------------
% 6.87/1.46 % (3540699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.46 % (3540699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.46 % (3540699)CaDiCaL version: 2.1.3
% 6.87/1.46 % (3540699)Termination reason: Instruction limit
% 6.87/1.46 % (3540699)Termination phase: Saturation
% 6.87/1.46 % (3540699)Time elapsed: 0.107 s
% 6.87/1.46 % (3540699)Peak memory usage: 15 MB
% 6.87/1.46 % (3540699)Instructions burned: 159 (million)
% 6.87/1.46 % (3540751)ott-21_1_sil=16000:fs=off:random_seed=1109067187:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.87/1.46 % (3540734)Instruction limit reached!
% 6.87/1.46 % (3540734)------------------------------
% 6.87/1.46 % (3540734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.46 % (3540734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540734)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540734)Termination reason: Instruction limit
% 23.36/3.73 % (3540734)Termination phase: Saturation
% 23.36/3.73 % (3540734)Time elapsed: 0.083 s
% 23.36/3.73 % (3540734)Peak memory usage: 13 MB
% 23.36/3.73 % (3540734)Instructions burned: 132 (million)
% 23.36/3.73 % (3540725)Instruction limit reached!
% 23.36/3.73 % (3540725)------------------------------
% 23.36/3.73 % (3540725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.36/3.73 % (3540725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540725)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540725)Termination reason: Instruction limit
% 23.36/3.73 % (3540725)Termination phase: Finite model building constraint generation
% 23.36/3.73 % (3540725)Time elapsed: 0.137 s
% 23.36/3.73 % (3540725)Peak memory usage: 39 MB
% 23.36/3.73 % (3540725)Instructions burned: 718 (million)
% 23.36/3.73 % (3540784)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=744711455:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 23.36/3.73 % (3540792)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=197187113:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.36/3.73 % TRYING [1]
% 23.36/3.73 % TRYING [2]
% 23.36/3.73 % (3540751)Instruction limit reached!
% 23.36/3.73 % (3540751)------------------------------
% 23.36/3.73 % (3540751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.36/3.73 % (3540751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540751)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540751)Termination reason: Instruction limit
% 23.36/3.73 % (3540751)Termination phase: Saturation
% 23.36/3.73 % (3540751)Time elapsed: 0.100 s
% 23.36/3.73 % (3540751)Peak memory usage: 13 MB
% 23.36/3.73 % (3540751)Instructions burned: 180 (million)
% 23.36/3.73 % TRYING [3]
% 23.36/3.73 % (3540799)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1748455972:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 23.36/3.73 % TRYING [4]
% 23.36/3.73 % (3540792)Instruction limit reached!
% 23.36/3.73 % (3540792)------------------------------
% 23.36/3.73 % (3540792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.36/3.73 % (3540792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540792)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540792)Termination reason: Instruction limit
% 23.36/3.73 % (3540792)Termination phase: Finite model building SAT solving
% 23.36/3.73 % (3540792)Time elapsed: 0.183 s
% 23.36/3.73 % (3540792)Peak memory usage: 40 MB
% 23.36/3.73 % (3540792)Instructions burned: 866 (million)
% 23.36/3.73 % (3540801)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3278919045:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 23.36/3.73 % (3540801)Cannot represent all propositional literals internally
% 23.36/3.73 % (3540801)Refutation not found, incomplete strategy
% 23.36/3.73 % (3540801)------------------------------
% 23.36/3.73 % (3540801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.36/3.73 % (3540801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540801)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540801)Termination reason: Refutation not found, incomplete strategy
% 23.36/3.73 % (3540801)Time elapsed: 0.007 s
% 23.36/3.73 % (3540801)Peak memory usage: 10 MB
% 23.36/3.73 % (3540801)Instructions burned: 28 (million)
% 23.36/3.73 % (3540801)------------------------------
% 23.36/3.73 % (3540801)------------------------------
% 23.36/3.73 % (3540803)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=91671110:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 23.36/3.73 % (3540736)Instruction limit reached!
% 23.36/3.73 % (3540736)------------------------------
% 23.36/3.73 % (3540736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.36/3.73 % (3540736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.36/3.73 % (3540736)CaDiCaL version: 2.1.3
% 23.36/3.73 % (3540736)Termination reason: Instruction limit
% 23.36/3.73 % (3540736)Termination phase: Saturation
% 23.36/3.73 % (3540736)Time elapsed: 0.421 s
% 23.36/3.73 % (3540736)Peak memory usage: 21 MB
% 23.36/3.73 % (3540736)Instructions burned: 685 (million)
% 23.36/3.73 % (3540784)Instruction limit reached!
% 23.36/3.73 % (3540784)------------------------------
% 23.36/3.73 % (3540784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540784)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540784)Termination reason: Instruction limit
% 83.60/12.28 % (3540784)Termination phase: Saturation
% 83.60/12.28 % (3540784)Time elapsed: 0.338 s
% 83.60/12.28 % (3540784)Peak memory usage: 14 MB
% 83.60/12.28 % (3540784)Instructions burned: 478 (million)
% 83.60/12.28 % (3540805)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=304345097:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 83.60/12.28 % (3540806)fmb+10_1_sil=64000:random_seed=3238668643:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 83.60/12.28 % TRYING [1]
% 83.60/12.28 % TRYING [2]
% 83.60/12.28 % (3540803)Instruction limit reached!
% 83.60/12.28 % (3540803)------------------------------
% 83.60/12.28 % (3540803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540803)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540803)Termination reason: Instruction limit
% 83.60/12.28 % (3540803)Termination phase: Saturation
% 83.60/12.28 % (3540803)Time elapsed: 0.215 s
% 83.60/12.28 % (3540803)Peak memory usage: 24 MB
% 83.60/12.28 % (3540803)Instructions burned: 694 (million)
% 83.60/12.28 % TRYING [3]
% 83.60/12.28 % (3540809)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3899998113:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 83.60/12.28 % (3540809)Cannot represent all propositional literals internally
% 83.60/12.28 % (3540809)Refutation not found, incomplete strategy
% 83.60/12.28 % (3540809)------------------------------
% 83.60/12.28 % (3540809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540809)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540809)Termination reason: Refutation not found, incomplete strategy
% 83.60/12.28 % (3540809)Time elapsed: 0.008 s
% 83.60/12.28 % (3540809)Peak memory usage: 11 MB
% 83.60/12.28 % (3540809)Instructions burned: 30 (million)
% 83.60/12.28 % (3540809)------------------------------
% 83.60/12.28 % (3540809)------------------------------
% 83.60/12.28 % (3540811)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=291543111:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 83.60/12.28 % TRYING [8]
% 83.60/12.28 % (3540811)Instruction limit reached!
% 83.60/12.28 % (3540811)------------------------------
% 83.60/12.28 % (3540811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540811)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540811)Termination reason: Instruction limit
% 83.60/12.28 % (3540811)Termination phase: Finite model building constraint generation
% 83.60/12.28 % (3540811)Time elapsed: 0.181 s
% 83.60/12.28 % (3540811)Peak memory usage: 75 MB
% 83.60/12.28 % (3540811)Instructions burned: 925 (million)
% 83.60/12.28 % (3540813)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1677368679:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 83.60/12.28 % (3540799)Instruction limit reached!
% 83.60/12.28 % (3540799)------------------------------
% 83.60/12.28 % (3540799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540799)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540799)Termination reason: Instruction limit
% 83.60/12.28 % (3540799)Termination phase: Saturation
% 83.60/12.28 % (3540799)Time elapsed: 0.656 s
% 83.60/12.28 % (3540799)Peak memory usage: 26 MB
% 83.60/12.28 % (3540799)Instructions burned: 1180 (million)
% 83.60/12.28 % (3540815)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2395894820:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 83.60/12.28 % (3540805)Instruction limit reached!
% 83.60/12.28 % (3540805)------------------------------
% 83.60/12.28 % (3540805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.60/12.28 % (3540805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/12.28 % (3540805)CaDiCaL version: 2.1.3
% 83.60/12.28 % (3540805)Termination reason: Instruction limit
% 83.60/12.28 % (3540805)Termination phase: Saturation
% 83.60/12.28 % (3540805)Time elapsed: 0.459 s
% 83.60/12.28 % (3540805)Peak memory usage: 20 MB
% 83.60/12.28 % (3540805)Instructions burned: 880 (million)
% 83.60/12.28 % (3540817)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3030411288:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 142.72/20.64 % (3540817)Cannot represent all propositional literals internally
% 142.72/20.64 % (3540817)Refutation not found, incomplete strategy
% 142.72/20.64 % (3540817)------------------------------
% 142.72/20.64 % (3540817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540817)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540817)Termination reason: Refutation not found, incomplete strategy
% 142.72/20.64 % (3540817)Time elapsed: 0.016 s
% 142.72/20.64 % (3540817)Peak memory usage: 11 MB
% 142.72/20.64 % (3540817)Instructions burned: 31 (million)
% 142.72/20.64 % (3540817)------------------------------
% 142.72/20.64 % (3540817)------------------------------
% 142.72/20.64 % (3540819)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1032497174:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 142.72/20.64 % (3540819)Cannot represent all propositional literals internally
% 142.72/20.64 % (3540819)Refutation not found, incomplete strategy
% 142.72/20.64 % (3540819)------------------------------
% 142.72/20.64 % (3540819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540819)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540819)Termination reason: Refutation not found, incomplete strategy
% 142.72/20.64 % (3540819)Time elapsed: 0.089 s
% 142.72/20.64 % (3540819)Peak memory usage: 12 MB
% 142.72/20.64 % (3540819)Instructions burned: 182 (million)
% 142.72/20.64 % (3540819)------------------------------
% 142.72/20.64 % (3540819)------------------------------
% 142.72/20.64 % (3540821)ott-2_1_sil=16000:newcnf=on:random_seed=1882349116:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 142.72/20.64 % TRYING [4]
% 142.72/20.64 % (3540815)Instruction limit reached!
% 142.72/20.64 % (3540815)------------------------------
% 142.72/20.64 % (3540815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540815)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540815)Termination reason: Instruction limit
% 142.72/20.64 % (3540815)Termination phase: Saturation
% 142.72/20.64 % (3540815)Time elapsed: 0.607 s
% 142.72/20.64 % (3540815)Peak memory usage: 19 MB
% 142.72/20.64 % (3540815)Instructions burned: 1473 (million)
% 142.72/20.64 % (3540823)ott+10_1_sil=32000:tgt=ground:random_seed=2592743304:i=5114:av=off_2984 on theBenchmark for (2984ds/5114Mi)
% 142.72/20.64 % (3540821)Instruction limit reached!
% 142.72/20.64 % (3540821)------------------------------
% 142.72/20.64 % (3540821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540821)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540821)Termination reason: Instruction limit
% 142.72/20.64 % (3540821)Termination phase: Saturation
% 142.72/20.64 % (3540821)Time elapsed: 0.507 s
% 142.72/20.64 % (3540821)Peak memory usage: 22 MB
% 142.72/20.64 % (3540821)Instructions burned: 870 (million)
% 142.72/20.64 % (3540825)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2181057069:i=54282_2982 on theBenchmark for (2982ds/54282Mi)
% 142.72/20.64 % TRYING [1]
% 142.72/20.64 % TRYING [2]
% 142.72/20.64 % TRYING [3]
% 142.72/20.64 % TRYING [4]
% 142.72/20.64 % (3540813)Instruction limit reached!
% 142.72/20.64 % (3540813)------------------------------
% 142.72/20.64 % (3540813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540813)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540813)Termination reason: Instruction limit
% 142.72/20.64 % (3540813)Termination phase: Saturation
% 142.72/20.64 % (3540813)Time elapsed: 1.422 s
% 142.72/20.64 % (3540813)Peak memory usage: 50 MB
% 142.72/20.64 % (3540813)Instructions burned: 5133 (million)
% 142.72/20.64 % (3540827)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3046212691:i=3512:aac=none_2976 on theBenchmark for (2976ds/3512Mi)
% 142.72/20.64 % (3540827)Instruction limit reached!
% 142.72/20.64 % (3540827)------------------------------
% 142.72/20.64 % (3540827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.72/20.64 % (3540827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.72/20.64 % (3540827)CaDiCaL version: 2.1.3
% 142.72/20.64 % (3540827)Termination reason: Instruction limit
% 220.47/31.59 % (3540827)Termination phase: Saturation
% 220.47/31.59 % (3540827)Time elapsed: 1.0000 s
% 220.47/31.59 % (3540827)Peak memory usage: 39 MB
% 220.47/31.59 % (3540827)Instructions burned: 3512 (million)
% 220.47/31.59 % (3540829)dis+21_1_sil=32000:sas=cadical:random_seed=2462393534:i=3773:amm=off_2966 on theBenchmark for (2966ds/3773Mi)
% 220.47/31.59 % TRYING [5]
% 220.47/31.59 % (3540829)Instruction limit reached!
% 220.47/31.59 % (3540829)------------------------------
% 220.47/31.59 % (3540829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540829)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540829)Termination reason: Instruction limit
% 220.47/31.59 % (3540829)Termination phase: Saturation
% 220.47/31.59 % (3540829)Time elapsed: 1.115 s
% 220.47/31.59 % (3540829)Peak memory usage: 48 MB
% 220.47/31.59 % (3540829)Instructions burned: 3774 (million)
% 220.47/31.59 % (3540831)ott+11_1_sil=16000:gs=on:random_seed=3551487637:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2955 on theBenchmark for (2955ds/2251Mi)
% 220.47/31.59 % (3540823)Instruction limit reached!
% 220.47/31.59 % (3540823)------------------------------
% 220.47/31.59 % (3540823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540823)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540823)Termination reason: Instruction limit
% 220.47/31.59 % (3540823)Termination phase: Saturation
% 220.47/31.59 % (3540823)Time elapsed: 2.895 s
% 220.47/31.59 % (3540823)Peak memory usage: 77 MB
% 220.47/31.59 % (3540823)Instructions burned: 5114 (million)
% 220.47/31.59 % (3540833)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1086262584:fmbsr=1.6:i=67534_2955 on theBenchmark for (2955ds/67534Mi)
% 220.47/31.59 % (3540831)Instruction limit reached!
% 220.47/31.59 % (3540831)------------------------------
% 220.47/31.59 % (3540831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540831)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540831)Termination reason: Instruction limit
% 220.47/31.59 % (3540831)Termination phase: Saturation
% 220.47/31.59 % (3540831)Time elapsed: 0.712 s
% 220.47/31.59 % (3540831)Peak memory usage: 42 MB
% 220.47/31.59 % (3540831)Instructions burned: 2254 (million)
% 220.47/31.59 % (3540835)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1943541360:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2948 on theBenchmark for (2948ds/4591Mi)
% 220.47/31.59 % TRYING [5]
% 220.47/31.59 % (3540835)Instruction limit reached!
% 220.47/31.59 % (3540835)------------------------------
% 220.47/31.59 % (3540835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540835)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540835)Termination reason: Instruction limit
% 220.47/31.59 % (3540835)Termination phase: Saturation
% 220.47/31.59 % (3540835)Time elapsed: 1.099 s
% 220.47/31.59 % (3540835)Peak memory usage: 36 MB
% 220.47/31.59 % (3540835)Instructions burned: 4593 (million)
% 220.47/31.59 % (3540837)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3357116248:i=29340_2936 on theBenchmark for (2936ds/29340Mi)
% 220.47/31.59 % TRYING [7]
% 220.47/31.59 % (3540806)Instruction limit reached!
% 220.47/31.59 % (3540806)------------------------------
% 220.47/31.59 % (3540806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540806)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540806)Termination reason: Instruction limit
% 220.47/31.59 % (3540806)Termination phase: Finite model building constraint generation
% 220.47/31.59 % (3540806)Time elapsed: 8.878 s
% 220.47/31.59 % (3540806)Peak memory usage: 333 MB
% 220.47/31.59 % (3540806)Instructions burned: 22063 (million)
% 220.47/31.59 % (3540839)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3836776166:i=5211_2905 on theBenchmark for (2905ds/5211Mi)
% 220.47/31.59 % (3540839)Instruction limit reached!
% 220.47/31.59 % (3540839)------------------------------
% 220.47/31.59 % (3540839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.47/31.59 % (3540839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.47/31.59 % (3540839)CaDiCaL version: 2.1.3
% 220.47/31.59 % (3540839)Termination reason: Instruction limit
% 126.24/35.10 % (3540839)Termination phase: Saturation
% 126.24/35.10 % (3540839)Time elapsed: 2.363 s
% 126.24/35.10 % (3540839)Peak memory usage: 43 MB
% 126.24/35.10 % (3540839)Instructions burned: 5213 (million)
% 126.24/35.10 % (3540841)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2642746640:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 126.24/35.10 % (3540841)Cannot represent all propositional literals internally
% 126.24/35.10 % (3540841)Refutation not found, incomplete strategy
% 126.24/35.10 % (3540841)------------------------------
% 126.24/35.10 % (3540841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540841)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540841)Termination reason: Refutation not found, incomplete strategy
% 126.24/35.10 % (3540841)Time elapsed: 0.016 s
% 126.24/35.10 % (3540841)Peak memory usage: 11 MB
% 126.24/35.10 % (3540841)Instructions burned: 31 (million)
% 126.24/35.10 % (3540841)------------------------------
% 126.24/35.10 % (3540841)------------------------------
% 126.24/35.10 % (3540843)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=799835443:fmbsr=2:i=46332_2880 on theBenchmark for (2880ds/46332Mi)
% 126.24/35.10 % (3540843)Cannot represent all propositional literals internally
% 126.24/35.10 % (3540843)Refutation not found, incomplete strategy
% 126.24/35.10 % (3540843)------------------------------
% 126.24/35.10 % (3540843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540843)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540843)Termination reason: Refutation not found, incomplete strategy
% 126.24/35.10 % (3540843)Time elapsed: 0.016 s
% 126.24/35.10 % (3540843)Peak memory usage: 11 MB
% 126.24/35.10 % (3540843)Instructions burned: 33 (million)
% 126.24/35.10 % (3540843)------------------------------
% 126.24/35.10 % (3540843)------------------------------
% 126.24/35.10 % (3540845)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2908963609:i=14071_2880 on theBenchmark for (2880ds/14071Mi)
% 126.24/35.10 % TRYING [12]
% 126.24/35.10 % (3540837)Instruction limit reached!
% 126.24/35.10 % (3540837)------------------------------
% 126.24/35.10 % (3540837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540837)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540837)Termination reason: Instruction limit
% 126.24/35.10 % (3540837)Termination phase: Saturation
% 126.24/35.10 % (3540837)Time elapsed: 8.259 s
% 126.24/35.10 % (3540837)Peak memory usage: 559 MB
% 126.24/35.10 % (3540837)Instructions burned: 29342 (million)
% 126.24/35.10 % (3541056)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1236006450:i=22565:add=on:rawr=on_2853 on theBenchmark for (2853ds/22565Mi)
% 126.24/35.10 % (3540845)Instruction limit reached!
% 126.24/35.10 % (3540845)------------------------------
% 126.24/35.10 % (3540845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540845)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540845)Termination reason: Instruction limit
% 126.24/35.10 % (3540845)Termination phase: Finite model building constraint generation
% 126.24/35.10 % (3540845)Time elapsed: 5.131 s
% 126.24/35.10 % (3540845)Peak memory usage: 1035 MB
% 126.24/35.10 % (3540845)Instructions burned: 14071 (million)
% 126.24/35.10 % (3541268)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3176413790:i=8173:av=off_2827 on theBenchmark for (2827ds/8173Mi)
% 126.24/35.10 % (3540825)Instruction limit reached!
% 126.24/35.10 % (3540825)------------------------------
% 126.24/35.10 % (3540825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540825)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540825)Termination reason: Instruction limit
% 126.24/35.10 % (3540825)Termination phase: Finite model building constraint generation
% 126.24/35.10 % (3540825)Time elapsed: 17.799 s
% 126.24/35.10 % (3540825)Peak memory usage: 1594 MB
% 126.24/35.10 % (3540825)Instructions burned: 54282 (million)
% 126.24/35.10 % (3541270)dis+10_16:1_sil=16000:random_seed=1181503313:i=9155:fsr=off_2802 on theBenchmark for (2802ds/9155Mi)
% 126.24/35.10 % (3541056)Instruction limit reached!
% 126.24/35.10 % (3541056)------------------------------
% 126.24/35.10 % (3541056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541056)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541056)Termination reason: Instruction limit
% 126.24/35.10 % (3541056)Termination phase: Saturation
% 126.24/35.10 % (3541056)Time elapsed: 5.608 s
% 126.24/35.10 % (3541056)Peak memory usage: 26 MB
% 126.24/35.10 % (3541056)Instructions burned: 22566 (million)
% 126.24/35.10 % (3541272)ott-3_8_sil=64000:random_seed=3034170632:i=20139:bs=on_2797 on theBenchmark for (2797ds/20139Mi)
% 126.24/35.10 % (3541268)Instruction limit reached!
% 126.24/35.10 % (3541268)------------------------------
% 126.24/35.10 % (3541268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541268)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541268)Termination reason: Instruction limit
% 126.24/35.10 % (3541268)Termination phase: Saturation
% 126.24/35.10 % (3541268)Time elapsed: 4.676 s
% 126.24/35.10 % (3541268)Peak memory usage: 131 MB
% 126.24/35.10 % (3541268)Instructions burned: 8174 (million)
% 126.24/35.10 % (3541274)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3160952082:fmbsr=2:i=32576_2780 on theBenchmark for (2780ds/32576Mi)
% 126.24/35.10 % TRYING [9]
% 126.24/35.10 % (3541270)Instruction limit reached!
% 126.24/35.10 % (3541270)------------------------------
% 126.24/35.10 % (3541270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541270)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541270)Termination reason: Instruction limit
% 126.24/35.10 % (3541270)Termination phase: Saturation
% 126.24/35.10 % (3541270)Time elapsed: 4.784 s
% 126.24/35.10 % (3541270)Peak memory usage: 91 MB
% 126.24/35.10 % (3541270)Instructions burned: 9156 (million)
% 126.24/35.10 % (3541276)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=67774419:i=11404_2754 on theBenchmark for (2754ds/11404Mi)
% 126.24/35.10 % (3541272)Instruction limit reached!
% 126.24/35.10 % (3541272)------------------------------
% 126.24/35.10 % (3541272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541272)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541272)Termination reason: Instruction limit
% 126.24/35.10 % (3541272)Termination phase: Saturation
% 126.24/35.10 % (3541272)Time elapsed: 6.405 s
% 126.24/35.10 % (3541272)Peak memory usage: 92 MB
% 126.24/35.10 % (3541272)Instructions burned: 20142 (million)
% 126.24/35.10 % (3541278)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=484448020:i=14134_2733 on theBenchmark for (2733ds/14134Mi)
% 126.24/35.10 % (3540833)Instruction limit reached!
% 126.24/35.10 % (3540833)------------------------------
% 126.24/35.10 % (3540833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3540833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3540833)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3540833)Termination reason: Instruction limit
% 126.24/35.10 % (3540833)Termination phase: Finite model building constraint generation
% 126.24/35.10 % (3540833)Time elapsed: 22.788 s
% 126.24/35.10 % (3540833)Peak memory usage: 3225 MB
% 126.24/35.10 % (3540833)Instructions burned: 67537 (million)
% 126.24/35.10 % (3541280)dis+33_16_sil=32000:sac=on:random_seed=3672701268:i=15851:nm=0_2722 on theBenchmark for (2722ds/15851Mi)
% 126.24/35.10 % TRYING [6]
% 126.24/35.10 % (3541276)Instruction limit reached!
% 126.24/35.10 % (3541276)------------------------------
% 126.24/35.10 % (3541276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541276)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541276)Termination reason: Instruction limit
% 126.24/35.10 % (3541276)Termination phase: Saturation
% 126.24/35.10 % (3541276)Time elapsed: 6.469 s
% 126.24/35.10 % (3541276)Peak memory usage: 187 MB
% 126.24/35.10 % (3541276)Instructions burned: 11404 (million)
% 126.24/35.10 % (3541547)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=301503029:avsq=on:i=17627:add=on:amm=off_2689 on theBenchmark for (2689ds/17627Mi)
% 126.24/35.10 % (3541278)Instruction limit reached!
% 126.24/35.10 % (3541278)------------------------------
% 126.24/35.10 % (3541278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541278)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541278)Termination reason: Instruction limit
% 126.24/35.10 % (3541278)Termination phase: Saturation
% 126.24/35.10 % (3541278)Time elapsed: 4.514 s
% 126.24/35.10 % (3541278)Peak memory usage: 179 MB
% 126.24/35.10 % (3541278)Instructions burned: 14135 (million)
% 126.24/35.10 % (3541549)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4142895804:s2a=on:i=53295_2687 on theBenchmark for (2687ds/53295Mi)
% 126.24/35.10 % (3541274)Instruction limit reached!
% 126.24/35.10 % (3541274)------------------------------
% 126.24/35.10 % (3541274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541274)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541274)Termination reason: Instruction limit
% 126.24/35.10 % (3541274)Termination phase: Finite model building constraint generation
% 126.24/35.10 % (3541274)Time elapsed: 11.780 s
% 126.24/35.10 % (3541274)Peak memory usage: 2060 MB
% 126.24/35.10 % (3541274)Instructions burned: 32579 (million)
% 126.24/35.10 % (3541551)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1372855994:i=26857:ins=20_2660 on theBenchmark for (2660ds/26857Mi)
% 126.24/35.10 % (3541551)Cannot represent all propositional literals internally
% 126.24/35.10 % (3541551)Refutation not found, incomplete strategy
% 126.24/35.10 % (3541551)------------------------------
% 126.24/35.10 % (3541551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541551)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541551)Termination reason: Refutation not found, incomplete strategy
% 126.24/35.10 % (3541551)Time elapsed: 0.015 s
% 126.24/35.10 % (3541551)Peak memory usage: 11 MB
% 126.24/35.10 % (3541551)Instructions burned: 30 (million)
% 126.24/35.10 % (3541551)------------------------------
% 126.24/35.10 % (3541551)------------------------------
% 126.24/35.10 % (3541553)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1212105988:i=28120:bs=on:fsr=off_2659 on theBenchmark for (2659ds/28120Mi)
% 126.24/35.10 % (3541553) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3540681-3541553"...
% 126.24/35.10 % (3541553)...printing done.
% 126.24/35.10 % (3541553)Refutation found. Thanks to Tanya!
% 126.24/35.10 % SZS status Unsatisfiable for theBenchmark
% 126.24/35.10 % SZS output start Proof for theBenchmark
% See solution above
% 126.24/35.10 % (3541553)------------------------------
% 126.24/35.10 % (3541553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.24/35.10 % (3541553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.24/35.10 % (3541553)CaDiCaL version: 2.1.3
% 126.24/35.10 % (3541553)Termination reason: Refutation
% 126.24/35.10 % (3541553)Time elapsed: 0.319 s
% 126.24/35.10 % (3541553)Peak memory usage: 22 MB
% 126.24/35.10 % (3541553)Instructions burned: 506 (million)
% 126.24/35.10 % (3540681)Success in time 34.702 s
% 126.24/35.10 % Vampire exiting
%------------------------------------------------------------------------------