%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUN021^1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n016.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 : Wed Sep 30 08:19:53 AM UTC 2026 % Result : Satisfiable 0.20s 0.46s % Output : Saturation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUN021^1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.17 % Computer : n016.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Tue Sep 29 13:10:49 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.21 Running higher-order theorem proving % 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.40 % (315574)Detected a higher-order problem, will run a greedy HOL sequence. % 0.20/0.40 % (315585)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on % 0.20/0.40 % (315585)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on % 0.20/0.40 % (315580)lrs+10_16_si=on:nwc=1.5:random_seed=3338571715:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi) % 0.20/0.40 % (315583)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4212426888:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi) % 0.20/0.40 % (315585)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3215982227:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi) % 0.20/0.40 % (315580)Refutation not found, incomplete strategy % 0.20/0.40 % (315580)------------------------------ % 0.20/0.40 % (315580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.40 % (315580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.40 % (315580)CaDiCaL version: 2.1.3 % 0.20/0.40 % (315580)Termination reason: Refutation not found, incomplete strategy % 0.20/0.40 % (315580)Time elapsed: 0.002 s % 0.20/0.40 % (315580)Peak memory usage: 11 MB % 0.20/0.40 % (315580)Instructions burned: 2 (million) % 0.20/0.40 % (315585)Refutation not found, incomplete strategy % 0.20/0.40 % (315585)------------------------------ % 0.20/0.40 % (315585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.40 % (315585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.40 % (315585)CaDiCaL version: 2.1.3 % 0.20/0.40 % (315585)Termination reason: Refutation not found, incomplete strategy % 0.20/0.40 % (315585)Time elapsed: 0.002 s % 0.20/0.40 % (315585)Peak memory usage: 11 MB % 0.20/0.40 % (315585)Instructions burned: 2 (million) % 0.20/0.40 % (315580)------------------------------ % 0.20/0.40 % (315580)------------------------------ % 0.20/0.40 % (315585)------------------------------ % 0.20/0.40 % (315585)------------------------------ % 0.20/0.40 % (315583)Instruction limit reached! % 0.20/0.40 % (315583)------------------------------ % 0.20/0.40 % (315583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.40 % (315583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.40 % (315583)CaDiCaL version: 2.1.3 % 0.20/0.40 % (315583)Termination reason: Instruction limit % 0.20/0.40 % (315583)Termination phase: Saturation % 0.20/0.40 % (315583)Time elapsed: 0.022 s % 0.20/0.40 % (315583)Peak memory usage: 11 MB % 0.20/0.40 % (315583)Instructions burned: 24 (million) % 0.20/0.40 % (315589)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4287110659:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi) % 0.20/0.40 % (315590)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1405175261:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi) % 0.20/0.40 % (315589)Instruction limit reached! % 0.20/0.40 % (315589)------------------------------ % 0.20/0.40 % (315589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.40 % (315589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.40 % (315589)CaDiCaL version: 2.1.3 % 0.20/0.40 % (315589)Termination reason: Instruction limit % 0.20/0.40 % (315589)Termination phase: Saturation % 0.20/0.40 % (315589)Time elapsed: 0.002 s % 0.20/0.40 % (315589)Peak memory usage: 10 MB % 0.20/0.40 % (315589)Instructions burned: 2 (million) % 0.20/0.40 % (315590)Instruction limit reached! % 0.20/0.40 % (315590)------------------------------ % 0.20/0.40 % (315590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.40 % (315590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.40 % (315590)CaDiCaL version: 2.1.3 % 0.20/0.40 % (315590)Termination reason: Instruction limit % 0.20/0.40 % (315590)Termination phase: Saturation % 0.20/0.40 % (315590)Time elapsed: 0.006 s % 0.20/0.40 % (315590)Peak memory usage: 11 MB % 0.20/0.40 % (315590)Instructions burned: 5 (million) % 0.20/0.40 % (315582)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1977983337:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi) % 0.20/0.44 % (315591)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on % 0.20/0.44 % (315579)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4223992414:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi) % 0.20/0.44 % (315591)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4237784399:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi) % 0.20/0.44 % (315579)Refutation not found, incomplete strategy % 0.20/0.44 % (315579)------------------------------ % 0.20/0.44 % (315579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.44 % (315579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.44 % (315579)CaDiCaL version: 2.1.3 % 0.20/0.44 % (315579)Termination reason: Refutation not found, incomplete strategy % 0.20/0.44 % (315579)Time elapsed: 0.002 s % 0.20/0.44 % (315579)Peak memory usage: 11 MB % 0.20/0.44 % (315579)Instructions burned: 2 (million) % 0.20/0.44 % (315579)------------------------------ % 0.20/0.44 % (315579)------------------------------ % 0.20/0.44 % (315594)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1105935208:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi) % 0.20/0.44 % (315591)Refutation not found, incomplete strategy % 0.20/0.44 % (315591)------------------------------ % 0.20/0.44 % (315591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.44 % (315591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.44 % (315591)CaDiCaL version: 2.1.3 % 0.20/0.44 % (315591)Termination reason: Refutation not found, incomplete strategy % 0.20/0.44 % (315591)Time elapsed: 0.002 s % 0.20/0.44 % (315591)Peak memory usage: 11 MB % 0.20/0.44 % (315591)Instructions burned: 2 (million) % 0.20/0.44 % (315591)------------------------------ % 0.20/0.44 % (315591)------------------------------ % 0.20/0.44 % (315594)Refutation not found, incomplete strategy % 0.20/0.44 % (315594)------------------------------ % 0.20/0.44 % (315594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.44 % (315594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.44 % (315594)CaDiCaL version: 2.1.3 % 0.20/0.44 % (315594)Termination reason: Refutation not found, incomplete strategy % 0.20/0.44 % (315594)Time elapsed: 0.001 s % 0.20/0.44 % (315594)Peak memory usage: 11 MB % 0.20/0.44 % (315594)Instructions burned: 2 (million) % 0.20/0.44 % (315594)------------------------------ % 0.20/0.44 % (315594)------------------------------ % 0.20/0.44 % (315582)Refutation not found, incomplete strategy % 0.20/0.44 % (315582)------------------------------ % 0.20/0.44 % (315582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.44 % (315582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.44 % (315582)CaDiCaL version: 2.1.3 % 0.20/0.44 % (315582)Termination reason: Refutation not found, incomplete strategy % 0.20/0.44 % (315582)Time elapsed: 0.015 s % 0.20/0.44 % (315582)Peak memory usage: 12 MB % 0.20/0.44 % (315582)Instructions burned: 14 (million) % 0.20/0.44 % (315582)------------------------------ % 0.20/0.44 % (315582)------------------------------ % 0.20/0.44 % (315584)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1646033180:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi) % 0.20/0.44 % (315581)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1761118056:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi) % 0.20/0.44 % (315596)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on % 0.20/0.44 % (315596)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on % 0.20/0.44 % (315581)Refutation not found, incomplete strategy % 0.20/0.44 % (315581)------------------------------ % 0.20/0.44 % (315581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.44 % (315581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315581)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315581)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315581)Time elapsed: 0.005 s % 0.20/0.46 % (315581)Peak memory usage: 11 MB % 0.20/0.46 % (315581)Instructions burned: 2 (million) % 0.20/0.46 % (315581)------------------------------ % 0.20/0.46 % (315581)------------------------------ % 0.20/0.46 % (315584)Refutation not found, incomplete strategy % 0.20/0.46 % (315584)------------------------------ % 0.20/0.46 % (315584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315584)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315584)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315584)Time elapsed: 0.007 s % 0.20/0.46 % (315584)Peak memory usage: 11 MB % 0.20/0.46 % (315584)Instructions burned: 2 (million) % 0.20/0.46 % (315584)------------------------------ % 0.20/0.46 % (315584)------------------------------ % 0.20/0.46 % (315596)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3548880580:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi) % 0.20/0.46 % (315596)Refutation not found, incomplete strategy % 0.20/0.46 % (315596)------------------------------ % 0.20/0.46 % (315596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315596)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315596)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315596)Time elapsed: 0.002 s % 0.20/0.46 % (315596)Peak memory usage: 11 MB % 0.20/0.46 % (315596)Instructions burned: 2 (million) % 0.20/0.46 % (315596)------------------------------ % 0.20/0.46 % (315596)------------------------------ % 0.20/0.46 % (315601)lrs+10_1_si=on:cs=on:random_seed=748086894:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi) % 0.20/0.46 % (315601)Refutation not found, incomplete strategy % 0.20/0.46 % (315601)------------------------------ % 0.20/0.46 % (315601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315601)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315601)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315601)Time elapsed: 0.002 s % 0.20/0.46 % (315601)Peak memory usage: 11 MB % 0.20/0.46 % (315601)Instructions burned: 2 (million) % 0.20/0.46 % (315603)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1270988861:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi) % 0.20/0.46 % (315601)------------------------------ % 0.20/0.46 % (315601)------------------------------ % 0.20/0.46 % (315603)Refutation not found, incomplete strategy % 0.20/0.46 % (315603)------------------------------ % 0.20/0.46 % (315603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315603)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315603)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315603)Time elapsed: 0.002 s % 0.20/0.46 % (315603)Peak memory usage: 11 MB % 0.20/0.46 % (315603)Instructions burned: 1 (million) % 0.20/0.46 % (315603)------------------------------ % 0.20/0.46 % (315603)------------------------------ % 0.20/0.46 % (315602)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on % 0.20/0.46 % (315602)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=3251689924:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi) % 0.20/0.46 % (315602)Refutation not found, incomplete strategy % 0.20/0.46 % (315602)------------------------------ % 0.20/0.46 % (315602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315602)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315602)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315602)Time elapsed: 0.002 s % 0.20/0.46 % (315602)Peak memory usage: 11 MB % 0.20/0.46 % (315602)Instructions burned: 2 (million) % 0.20/0.46 % (315602)------------------------------ % 0.20/0.46 % (315602)------------------------------ % 0.20/0.46 % (315609)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=415915999:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi) % 0.20/0.46 % (315609)Refutation not found, incomplete strategy % 0.20/0.46 % (315609)------------------------------ % 0.20/0.46 % (315609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315609)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315609)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315609)Time elapsed: 0.002 s % 0.20/0.46 % (315609)Peak memory usage: 11 MB % 0.20/0.46 % (315609)Instructions burned: 2 (million) % 0.20/0.46 % (315609)------------------------------ % 0.20/0.46 % (315609)------------------------------ % 0.20/0.46 % (315613)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2580063355:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi) % 0.20/0.46 % (315613)Refutation not found, incomplete strategy % 0.20/0.46 % (315613)------------------------------ % 0.20/0.46 % (315613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315613)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315613)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315613)Time elapsed: 0.001 s % 0.20/0.46 % (315613)Peak memory usage: 11 MB % 0.20/0.46 % (315613)Instructions burned: 2 (million) % 0.20/0.46 % (315613)------------------------------ % 0.20/0.46 % (315613)------------------------------ % 0.20/0.46 % (315612)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3350395237:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi) % 0.20/0.46 % (315612)Refutation not found, incomplete strategy % 0.20/0.46 % (315612)------------------------------ % 0.20/0.46 % (315612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315612)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315612)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315612)Time elapsed: 0.002 s % 0.20/0.46 % (315612)Peak memory usage: 11 MB % 0.20/0.46 % (315612)Instructions burned: 2 (million) % 0.20/0.46 % (315600)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3696502581:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi) % 0.20/0.46 % (315612)------------------------------ % 0.20/0.46 % (315612)------------------------------ % 0.20/0.46 % (315606)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=75141276:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi) % 0.20/0.46 % (315600)Refutation not found, incomplete strategy % 0.20/0.46 % (315600)------------------------------ % 0.20/0.46 % (315600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315600)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315600)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315600)Time elapsed: 0.005 s % 0.20/0.46 % (315600)Peak memory usage: 11 MB % 0.20/0.46 % (315600)Instructions burned: 2 (million) % 0.20/0.46 % (315600)------------------------------ % 0.20/0.46 % (315600)------------------------------ % 0.20/0.46 % (315606)Refutation not found, incomplete strategy % 0.20/0.46 % (315606)------------------------------ % 0.20/0.46 % (315606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315606)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315606)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315606)Time elapsed: 0.002 s % 0.20/0.46 % (315606)Peak memory usage: 11 MB % 0.20/0.46 % (315606)Instructions burned: 1 (million) % 0.20/0.46 % (315606)------------------------------ % 0.20/0.46 % (315606)------------------------------ % 0.20/0.46 % (315608)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3917335331:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi) % 0.20/0.46 % (315608)Refutation not found, incomplete strategy % 0.20/0.46 % (315608)------------------------------ % 0.20/0.46 % (315608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315608)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315608)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315608)Time elapsed: 0.002 s % 0.20/0.46 % (315608)Peak memory usage: 11 MB % 0.20/0.46 % (315608)Instructions burned: 1 (million) % 0.20/0.46 % (315608)------------------------------ % 0.20/0.46 % (315608)------------------------------ % 0.20/0.46 % (315615)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=550413846:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi) % 0.20/0.46 % (315615)Refutation not found, incomplete strategy % 0.20/0.46 % (315615)------------------------------ % 0.20/0.46 % (315615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315615)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315615)Termination reason: Refutation not found, incomplete strategy % 0.20/0.46 % (315615)Time elapsed: 0.002 s % 0.20/0.46 % (315615)Peak memory usage: 11 MB % 0.20/0.46 % (315615)Instructions burned: 1 (million) % 0.20/0.46 % (315615)------------------------------ % 0.20/0.46 % (315615)------------------------------ % 0.20/0.46 % (315618)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3012057002:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi) % 0.20/0.46 % (315618) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-315574-315618"... % 0.20/0.46 % (315620)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3244745392:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi) % 0.20/0.46 % (315618)...printing done. % 0.20/0.46 % SZS status Satisfiable for theBenchmark % 0.20/0.46 % SZS output start Saturation. % 0.20/0.46 % SZS output end Saturation. % 0.20/0.46 % SZS output start Definitions and Model Updates. % 0.20/0.46 for all inputs, % 0.20/0.46 define mult := (^[Y0 : ($i > $i) > $i > $i]: ((^[Y1 : ($i > $i) > $i > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (Y0 @ (Y1 @ Y2) @ Y3)))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define plus := (^[Y0 : ($i > $i) > $i > $i]: ((^[Y1 : ($i > $i) > $i > $i]: ((^[Y2 : $i > $i]: ((^[Y3 : $i]: (Y0 @ Y2 @ (Y1 @ Y2 @ Y3))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define succ := (^[Y0 : ($i > $i) > $i > $i]: ((^[Y1 : $i > $i]: ((^[Y2 : $i]: (Y1 @ (Y0 @ Y1 @ Y2))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define ten := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1))))))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define nine := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1)))))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define eight := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1))))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define seven := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1)))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define six := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1))))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define five := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1)))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define four := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ (Y0 @ Y1))))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define three := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ (Y0 @ Y1)))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define two := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ (Y0 @ Y1))))) % 0.20/0.46 for all inputs, % 0.20/0.46 define one := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y0 @ Y1)))) % 0.20/0.46 for all inputs, % 0.20/0.46 define zero := (^[Y0 : $i > $i]: ((^[Y1 : $i]: (Y1)))) % 0.20/0.46 % SZS output end Definitions and Model Updates. % 0.20/0.46 % (315618)------------------------------ % 0.20/0.46 % (315618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 0.20/0.46 % (315618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 0.20/0.46 % (315618)CaDiCaL version: 2.1.3 % 0.20/0.46 % (315618)Termination reason: Satisfiable % 0.20/0.46 % (315618)Time elapsed: 0.003 s % 0.20/0.46 % (315618)Peak memory usage: 11 MB % 0.20/0.46 % (315618)Instructions burned: 2 (million) % 0.20/0.46 % (315574)Success in time 0.214 s % 0.20/0.46 % Vampire exiting %------------------------------------------------------------------------------