%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT182^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 07:48:29 AM UTC 2026
% Result : Theorem 22.30s 3.64s
% Output : Refutation 22.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT182^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n002.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 18:09:08 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.21/0.28 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.50/0.43 % (1651082)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.50/0.43 % (1651091)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1864055206:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.50/0.43 % (1651093)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.50/0.43 % (1651093)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.50/0.43 % (1651089)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3829738955:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.50/0.43 % (1651088)lrs+10_16_si=on:nwc=1.5:random_seed=1860456850:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.50/0.43 % (1651090)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=2605159079: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.50/0.43 % (1651091)Instruction limit reached!
% 0.50/0.43 % (1651091)------------------------------
% 0.50/0.43 % (1651091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.43 % (1651091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.43 % (1651091)CaDiCaL version: 2.1.3
% 0.50/0.43 % (1651091)Termination reason: Instruction limit
% 0.50/0.43 % (1651091)Termination phase: Property scanning
% 0.50/0.43 % (1651091)Time elapsed: 0.007 s
% 0.50/0.43 % (1651091)Peak memory usage: 10 MB
% 0.50/0.43 % (1651091)Instructions burned: 25 (million)
% 0.50/0.43 % (1651093)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=718579042:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.50/0.43 % (1651092)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=602344446:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.50/0.43 % (1651089)Instruction limit reached!
% 0.50/0.43 % (1651089)------------------------------
% 0.50/0.43 % (1651089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.43 % (1651089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.43 % (1651089)CaDiCaL version: 2.1.3
% 0.50/0.43 % (1651089)Termination reason: Instruction limit
% 0.50/0.43 % (1651089)Termination phase: shuffling
% 0.50/0.43 % (1651089)Time elapsed: 0.004 s
% 0.50/0.43 % (1651089)Peak memory usage: 10 MB
% 0.50/0.43 % (1651089)Instructions burned: 6 (million)
% 0.50/0.43 % (1651087)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1673884314:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.50/0.43 % (1651088)Instruction limit reached!
% 0.50/0.43 % (1651088)------------------------------
% 0.50/0.43 % (1651088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.43 % (1651088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.43 % (1651088)CaDiCaL version: 2.1.3
% 0.50/0.43 % (1651088)Termination reason: Instruction limit
% 0.50/0.43 % (1651088)Termination phase: Property scanning
% 0.50/0.43 % (1651088)Time elapsed: 0.010 s
% 0.50/0.43 % (1651088)Peak memory usage: 10 MB
% 0.50/0.43 % (1651088)Instructions burned: 20 (million)
% 0.50/0.43 % (1651100)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3990907933:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.50/0.43 % (1651100)Instruction limit reached!
% 0.50/0.43 % (1651100)------------------------------
% 0.50/0.43 % (1651100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.43 % (1651100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.43 % (1651100)CaDiCaL version: 2.1.3
% 0.50/0.43 % (1651100)Termination reason: Instruction limit
% 0.50/0.43 % (1651100)Termination phase: shuffling
% 0.50/0.43 % (1651100)Time elapsed: 0.003 s
% 0.50/0.43 % (1651100)Peak memory usage: 10 MB
% 0.50/0.43 % (1651100)Instructions burned: 11 (million)
% 0.50/0.43 % (1651103)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.47 % (1651103)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2145773335:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.50/0.47 % (1651105)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=208582215:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.50/0.47 % (1651103)Instruction limit reached!
% 0.50/0.47 % (1651103)------------------------------
% 0.50/0.47 % (1651103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.47 % (1651103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.47 % (1651103)CaDiCaL version: 2.1.3
% 0.50/0.47 % (1651103)Termination reason: Instruction limit
% 0.50/0.47 % (1651103)Termination phase: shuffling
% 0.50/0.47 % (1651103)Time elapsed: 0.004 s
% 0.50/0.47 % (1651103)Peak memory usage: 10 MB
% 0.50/0.47 % (1651103)Instructions burned: 7 (million)
% 0.50/0.47 % (1651105)Instruction limit reached!
% 0.50/0.47 % (1651105)------------------------------
% 0.50/0.47 % (1651105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.47 % (1651105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.47 % (1651105)CaDiCaL version: 2.1.3
% 0.50/0.47 % (1651105)Termination reason: Instruction limit
% 0.50/0.47 % (1651105)Termination phase: shuffling
% 0.50/0.47 % (1651105)Time elapsed: 0.004 s
% 0.50/0.47 % (1651105)Peak memory usage: 10 MB
% 0.50/0.47 % (1651105)Instructions burned: 14 (million)
% 0.50/0.47 % (1651092)Instruction limit reached!
% 0.50/0.47 % (1651092)------------------------------
% 0.50/0.47 % (1651092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.47 % (1651092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.47 % (1651092)CaDiCaL version: 2.1.3
% 0.50/0.47 % (1651092)Termination reason: Instruction limit
% 0.50/0.47 % (1651092)Termination phase: Equality resolution with deletion
% 0.50/0.47 % (1651092)Time elapsed: 0.038 s
% 0.50/0.47 % (1651092)Peak memory usage: 12 MB
% 0.50/0.47 % (1651092)Instructions burned: 76 (million)
% 0.50/0.47 % (1651101)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1658612685:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.50/0.47 % (1651101)Instruction limit reached!
% 0.50/0.47 % (1651101)------------------------------
% 0.50/0.47 % (1651101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.47 % (1651101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.47 % (1651101)CaDiCaL version: 2.1.3
% 0.50/0.47 % (1651101)Termination reason: Instruction limit
% 0.50/0.47 % (1651101)Termination phase: shuffling
% 0.50/0.47 % (1651101)Time elapsed: 0.004 s
% 0.50/0.47 % (1651101)Peak memory usage: 10 MB
% 0.50/0.47 % (1651101)Instructions burned: 6 (million)
% 0.50/0.47 % (1651109)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=3975809326:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.50/0.47 % (1651087)Instruction limit reached!
% 0.50/0.47 % (1651087)------------------------------
% 0.50/0.47 % (1651087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.47 % (1651087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.47 % (1651087)CaDiCaL version: 2.1.3
% 0.50/0.47 % (1651087)Termination reason: Instruction limit
% 0.50/0.47 % (1651087)Termination phase: Property scanning
% 0.50/0.47 % (1651087)Time elapsed: 0.043 s
% 0.50/0.47 % (1651087)Peak memory usage: 12 MB
% 0.50/0.47 % (1651087)Instructions burned: 91 (million)
% 0.50/0.47 % (1651108)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.50/0.47 % (1651108)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.47 % (1651108)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1384761440: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.50/0.47 % (1651111)lrs+10_1_si=on:cs=on:random_seed=1583754315:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.11/0.49 % (1651112)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.11/0.49 % (1651112)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=1224403756:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.11/0.49 % (1651111)Instruction limit reached!
% 1.11/0.49 % (1651111)------------------------------
% 1.11/0.49 % (1651111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651111)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651111)Termination reason: Instruction limit
% 1.11/0.49 % (1651111)Termination phase: shuffling
% 1.11/0.49 % (1651111)Time elapsed: 0.004 s
% 1.11/0.49 % (1651111)Peak memory usage: 10 MB
% 1.11/0.49 % (1651111)Instructions burned: 8 (million)
% 1.11/0.49 % (1651112)Instruction limit reached!
% 1.11/0.49 % (1651112)------------------------------
% 1.11/0.49 % (1651112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651112)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651112)Termination reason: Instruction limit
% 1.11/0.49 % (1651112)Termination phase: shuffling
% 1.11/0.49 % (1651112)Time elapsed: 0.001 s
% 1.11/0.49 % (1651112)Peak memory usage: 10 MB
% 1.11/0.49 % (1651112)Instructions burned: 2 (million)
% 1.11/0.49 % (1651109)Instruction limit reached!
% 1.11/0.49 % (1651109)------------------------------
% 1.11/0.49 % (1651109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651109)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651109)Termination reason: Instruction limit
% 1.11/0.49 % (1651109)Termination phase: Property scanning
% 1.11/0.49 % (1651109)Time elapsed: 0.021 s
% 1.11/0.49 % (1651109)Peak memory usage: 11 MB
% 1.11/0.49 % (1651109)Instructions burned: 89 (million)
% 1.11/0.49 % (1651114)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4075827625:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.11/0.49 % (1651108)Instruction limit reached!
% 1.11/0.49 % (1651108)------------------------------
% 1.11/0.49 % (1651108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651108)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651108)Termination reason: Instruction limit
% 1.11/0.49 % (1651108)Termination phase: shuffling
% 1.11/0.49 % (1651108)Time elapsed: 0.014 s
% 1.11/0.49 % (1651108)Peak memory usage: 10 MB
% 1.11/0.49 % (1651108)Instructions burned: 29 (million)
% 1.11/0.49 % (1651120)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1511924099:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.11/0.49 % (1651118)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3562672062:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.11/0.49 % (1651120)Instruction limit reached!
% 1.11/0.49 % (1651120)------------------------------
% 1.11/0.49 % (1651120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651120)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651120)Termination reason: Instruction limit
% 1.11/0.49 % (1651120)Termination phase: shuffling
% 1.11/0.49 % (1651120)Time elapsed: 0.004 s
% 1.11/0.49 % (1651120)Peak memory usage: 10 MB
% 1.11/0.49 % (1651120)Instructions burned: 16 (million)
% 1.11/0.49 % (1651119)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2587505785:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.11/0.49 % (1651114)Instruction limit reached!
% 1.11/0.49 % (1651114)------------------------------
% 1.11/0.49 % (1651114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.49 % (1651114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.49 % (1651114)CaDiCaL version: 2.1.3
% 1.11/0.49 % (1651114)Termination reason: Instruction limit
% 1.11/0.49 % (1651114)Termination phase: Preprocessing 3
% 1.11/0.54 % (1651114)Time elapsed: 0.019 s
% 1.11/0.54 % (1651114)Peak memory usage: 11 MB
% 1.11/0.54 % (1651114)Instructions burned: 39 (million)
% 1.11/0.54 % (1651122)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1582655507:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.11/0.54 % (1651125)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2599042417:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.11/0.54 % (1651119)Instruction limit reached!
% 1.11/0.54 % (1651119)------------------------------
% 1.11/0.54 % (1651119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.54 % (1651119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.54 % (1651119)CaDiCaL version: 2.1.3
% 1.11/0.54 % (1651119)Termination reason: Instruction limit
% 1.11/0.54 % (1651119)Termination phase: Property scanning
% 1.11/0.54 % (1651119)Time elapsed: 0.013 s
% 1.11/0.54 % (1651119)Peak memory usage: 10 MB
% 1.11/0.54 % (1651119)Instructions burned: 25 (million)
% 1.11/0.54 % (1651125)Instruction limit reached!
% 1.11/0.54 % (1651125)------------------------------
% 1.11/0.54 % (1651125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.54 % (1651125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.54 % (1651125)CaDiCaL version: 2.1.3
% 1.11/0.54 % (1651125)Termination reason: Instruction limit
% 1.11/0.54 % (1651125)Termination phase: shuffling
% 1.11/0.54 % (1651125)Time elapsed: 0.004 s
% 1.11/0.54 % (1651125)Peak memory usage: 10 MB
% 1.11/0.54 % (1651125)Instructions burned: 14 (million)
% 1.11/0.54 % (1651093)Instruction limit reached!
% 1.11/0.54 % (1651093)------------------------------
% 1.11/0.54 % (1651093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.54 % (1651093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.54 % (1651093)CaDiCaL version: 2.1.3
% 1.11/0.54 % (1651093)Termination reason: Instruction limit
% 1.11/0.54 % (1651093)Termination phase: Saturation
% 1.11/0.54 % (1651093)Time elapsed: 0.102 s
% 1.11/0.54 % (1651093)Peak memory usage: 14 MB
% 1.11/0.54 % (1651093)Instructions burned: 157 (million)
% 1.11/0.54 % (1651118)Refutation not found, incomplete strategy
% 1.11/0.54 % (1651118)------------------------------
% 1.11/0.54 % (1651118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.54 % (1651118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.54 % (1651118)CaDiCaL version: 2.1.3
% 1.11/0.54 % (1651118)Termination reason: Refutation not found, incomplete strategy
% 1.11/0.54 % (1651118)Time elapsed: 0.023 s
% 1.11/0.54 % (1651118)Peak memory usage: 13 MB
% 1.11/0.54 % (1651118)Instructions burned: 48 (million)
% 1.11/0.54 % (1651118)------------------------------
% 1.11/0.54 % (1651118)------------------------------
% 1.11/0.54 % (1651128)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3118354994: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)
% 1.11/0.54 % (1651128)Instruction limit reached!
% 1.11/0.54 % (1651128)------------------------------
% 1.11/0.54 % (1651128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.54 % (1651128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.54 % (1651128)CaDiCaL version: 2.1.3
% 1.11/0.54 % (1651128)Termination reason: Instruction limit
% 1.11/0.54 % (1651128)Termination phase: shuffling
% 1.11/0.54 % (1651128)Time elapsed: 0.002 s
% 1.11/0.54 % (1651128)Peak memory usage: 10 MB
% 1.11/0.54 % (1651128)Instructions burned: 3 (million)
% 1.11/0.54 % (1651130)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1372159959:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.11/0.54 % (1651132)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=108056193:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.11/0.54 % (1651131)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2395035908:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.11/0.54 % (1651134)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) 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
% 1.80/0.61 % (1651134)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.80/0.61 % (1651135)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.80/0.61 % (1651135)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1312726735:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.80/0.61 % (1651134)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=2663859228:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.80/0.61 % (1651131)Instruction limit reached!
% 1.80/0.61 % (1651131)------------------------------
% 1.80/0.61 % (1651131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.80/0.61 % (1651131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.61 % (1651131)CaDiCaL version: 2.1.3
% 1.80/0.61 % (1651131)Termination reason: Instruction limit
% 1.80/0.61 % (1651131)Termination phase: Property scanning
% 1.80/0.61 % (1651131)Time elapsed: 0.012 s
% 1.80/0.61 % (1651131)Peak memory usage: 10 MB
% 1.80/0.61 % (1651131)Instructions burned: 24 (million)
% 1.80/0.61 % (1651130)Instruction limit reached!
% 1.80/0.61 % (1651130)------------------------------
% 1.80/0.61 % (1651130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.80/0.61 % (1651130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.61 % (1651130)CaDiCaL version: 2.1.3
% 1.80/0.61 % (1651130)Termination reason: Instruction limit
% 1.80/0.61 % (1651130)Termination phase: shuffling
% 1.80/0.61 % (1651130)Time elapsed: 0.013 s
% 1.80/0.61 % (1651130)Peak memory usage: 10 MB
% 1.80/0.61 % (1651130)Instructions burned: 26 (million)
% 1.80/0.61 % (1651135)Instruction limit reached!
% 1.80/0.61 % (1651135)------------------------------
% 1.80/0.61 % (1651135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.80/0.61 % (1651135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.61 % (1651135)CaDiCaL version: 2.1.3
% 1.80/0.61 % (1651135)Termination reason: Instruction limit
% 1.80/0.61 % (1651135)Termination phase: shuffling
% 1.80/0.61 % (1651135)Time elapsed: 0.003 s
% 1.80/0.61 % (1651135)Peak memory usage: 10 MB
% 1.80/0.61 % (1651135)Instructions burned: 10 (million)
% 1.80/0.61 % (1651134)Instruction limit reached!
% 1.80/0.61 % (1651134)------------------------------
% 1.80/0.61 % (1651134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.80/0.61 % (1651134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.61 % (1651134)CaDiCaL version: 2.1.3
% 1.80/0.61 % (1651134)Termination reason: Instruction limit
% 1.80/0.61 % (1651134)Termination phase: shuffling
% 1.80/0.61 % (1651134)Time elapsed: 0.007 s
% 1.80/0.61 % (1651134)Peak memory usage: 10 MB
% 1.80/0.61 % (1651134)Instructions burned: 14 (million)
% 1.80/0.61 % (1651132)Instruction limit reached!
% 1.80/0.61 % (1651132)------------------------------
% 1.80/0.61 % (1651132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.80/0.61 % (1651132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/0.61 % (1651132)CaDiCaL version: 2.1.3
% 1.80/0.61 % (1651132)Termination reason: Instruction limit
% 1.80/0.61 % (1651132)Termination phase: Property scanning
% 1.80/0.61 % (1651132)Time elapsed: 0.029 s
% 1.80/0.61 % (1651132)Peak memory usage: 11 MB
% 1.80/0.61 % (1651132)Instructions burned: 61 (million)
% 1.80/0.61 % (1651141)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=262496867:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.80/0.61 % (1651142)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1652695124:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.80/0.61 % (1651143)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=296977021:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.80/0.61 % (1651142)Instruction limit reached!
% 1.80/0.61 % (1651142)------------------------------
% 1.80/0.61 % (1651142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651142)CaDiCaL version: 2.1.3
% 2.28/0.68 % (1651142)Termination reason: Instruction limit
% 2.28/0.68 % (1651142)Termination phase: shuffling
% 2.28/0.68 % (1651142)Time elapsed: 0.004 s
% 2.28/0.68 % (1651142)Peak memory usage: 10 MB
% 2.28/0.68 % (1651142)Instructions burned: 8 (million)
% 2.28/0.68 % (1651147)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4027866049:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.28/0.68 % (1651143)Instruction limit reached!
% 2.28/0.68 % (1651143)------------------------------
% 2.28/0.68 % (1651143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651143)CaDiCaL version: 2.1.3
% 2.28/0.68 % (1651143)Termination reason: Instruction limit
% 2.28/0.68 % (1651143)Termination phase: shuffling
% 2.28/0.68 % (1651143)Time elapsed: 0.010 s
% 2.28/0.68 % (1651143)Peak memory usage: 10 MB
% 2.28/0.68 % (1651143)Instructions burned: 23 (million)
% 2.28/0.68 % (1651141)Instruction limit reached!
% 2.28/0.68 % (1651141)------------------------------
% 2.28/0.68 % (1651141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651141)CaDiCaL version: 2.1.3
% 2.28/0.68 % (1651141)Termination reason: Instruction limit
% 2.28/0.68 % (1651141)Termination phase: Property scanning
% 2.28/0.68 % (1651141)Time elapsed: 0.015 s
% 2.28/0.68 % (1651141)Peak memory usage: 10 MB
% 2.28/0.68 % (1651141)Instructions burned: 32 (million)
% 2.28/0.68 % (1651147)Instruction limit reached!
% 2.28/0.68 % (1651147)------------------------------
% 2.28/0.68 % (1651147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651147)CaDiCaL version: 2.1.3
% 2.28/0.68 % (1651147)Termination reason: Instruction limit
% 2.28/0.68 % (1651147)Termination phase: Property scanning
% 2.28/0.68 % (1651147)Time elapsed: 0.010 s
% 2.28/0.68 % (1651147)Peak memory usage: 10 MB
% 2.28/0.68 % (1651147)Instructions burned: 20 (million)
% 2.28/0.68 % (1651151)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=192598821:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.28/0.68 % (1651157)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3595349107:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.28/0.68 % (1651160)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=324539490:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.28/0.68 % (1651163)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.28/0.68 % (1651161)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1793441852:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.28/0.68 % (1651163)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3532889423:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.28/0.68 % (1651163)Instruction limit reached!
% 2.28/0.68 % (1651163)------------------------------
% 2.28/0.68 % (1651163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651163)CaDiCaL version: 2.1.3
% 2.28/0.68 % (1651163)Termination reason: Instruction limit
% 2.28/0.68 % (1651163)Termination phase: shuffling
% 2.28/0.68 % (1651163)Time elapsed: 0.004 s
% 2.28/0.68 % (1651163)Peak memory usage: 10 MB
% 2.28/0.68 % (1651163)Instructions burned: 8 (million)
% 2.28/0.68 % (1651173)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3674891530:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.28/0.68 % (1651161)Instruction limit reached!
% 2.28/0.68 % (1651161)------------------------------
% 2.28/0.68 % (1651161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.68 % (1651161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.68 % (1651161)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651161)Termination reason: Instruction limit
% 2.51/0.78 % (1651161)Termination phase: Preprocessing 3
% 2.51/0.78 % (1651161)Time elapsed: 0.020 s
% 2.51/0.78 % (1651161)Peak memory usage: 11 MB
% 2.51/0.78 % (1651161)Instructions burned: 43 (million)
% 2.51/0.78 % (1651179)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=2065629010:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.51/0.78 % (1651157)Instruction limit reached!
% 2.51/0.78 % (1651157)------------------------------
% 2.51/0.78 % (1651157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.78 % (1651157)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651157)Termination reason: Instruction limit
% 2.51/0.78 % (1651157)Termination phase: Saturation
% 2.51/0.78 % (1651157)Time elapsed: 0.066 s
% 2.51/0.78 % (1651157)Peak memory usage: 13 MB
% 2.51/0.78 % (1651157)Instructions burned: 143 (million)
% 2.51/0.78 % (1651122)Instruction limit reached!
% 2.51/0.78 % (1651122)------------------------------
% 2.51/0.78 % (1651122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.78 % (1651122)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651122)Termination reason: Instruction limit
% 2.51/0.78 % (1651122)Termination phase: Saturation
% 2.51/0.78 % (1651122)Time elapsed: 0.161 s
% 2.51/0.78 % (1651122)Peak memory usage: 14 MB
% 2.51/0.78 % (1651122)Instructions burned: 327 (million)
% 2.51/0.78 % (1651173)Instruction limit reached!
% 2.51/0.78 % (1651173)------------------------------
% 2.51/0.78 % (1651173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.78 % (1651173)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651173)Termination reason: Instruction limit
% 2.51/0.78 % (1651173)Termination phase: Saturation
% 2.51/0.78 % (1651173)Time elapsed: 0.053 s
% 2.51/0.78 % (1651173)Peak memory usage: 14 MB
% 2.51/0.78 % (1651173)Instructions burned: 181 (million)
% 2.51/0.78 % (1651193)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.51/0.78 % (1651193)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4127231384:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.51/0.78 % (1651193)Instruction limit reached!
% 2.51/0.78 % (1651193)------------------------------
% 2.51/0.78 % (1651193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.78 % (1651193)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651193)Termination reason: Instruction limit
% 2.51/0.78 % (1651193)Termination phase: shuffling
% 2.51/0.78 % (1651193)Time elapsed: 0.003 s
% 2.51/0.78 % (1651193)Peak memory usage: 10 MB
% 2.51/0.78 % (1651193)Instructions burned: 6 (million)
% 2.51/0.78 % (1651199)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3905188607:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.51/0.78 % (1651196)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2181596811:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.51/0.78 % (1651199)Instruction limit reached!
% 2.51/0.78 % (1651199)------------------------------
% 2.51/0.78 % (1651199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.78 % (1651199)CaDiCaL version: 2.1.3
% 2.51/0.78 % (1651199)Termination reason: Instruction limit
% 2.51/0.78 % (1651199)Termination phase: shuffling
% 2.51/0.78 % (1651199)Time elapsed: 0.005 s
% 2.51/0.78 % (1651199)Peak memory usage: 10 MB
% 2.51/0.78 % (1651199)Instructions burned: 21 (million)
% 2.51/0.78 % (1651179)Refutation not found, incomplete strategy
% 2.51/0.78 % (1651179)------------------------------
% 2.51/0.78 % (1651179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.78 % (1651179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.88 % (1651179)CaDiCaL version: 2.1.3
% 3.08/0.88 % (1651179)Termination reason: Refutation not found, incomplete strategy
% 3.08/0.88 % (1651179)Time elapsed: 0.052 s
% 3.08/0.88 % (1651179)Peak memory usage: 14 MB
% 3.08/0.88 % (1651179)Instructions burned: 105 (million)
% 3.08/0.88 % (1651179)------------------------------
% 3.08/0.88 % (1651179)------------------------------
% 3.08/0.88 % (1651160)Instruction limit reached!
% 3.08/0.88 % (1651160)------------------------------
% 3.08/0.88 % (1651160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.08/0.88 % (1651160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.88 % (1651160)CaDiCaL version: 2.1.3
% 3.08/0.88 % (1651160)Termination reason: Instruction limit
% 3.08/0.88 % (1651160)Termination phase: Saturation
% 3.08/0.88 % (1651160)Time elapsed: 0.098 s
% 3.08/0.88 % (1651160)Peak memory usage: 14 MB
% 3.08/0.88 % (1651160)Instructions burned: 193 (million)
% 3.08/0.88 % (1651196)Instruction limit reached!
% 3.08/0.88 % (1651196)------------------------------
% 3.08/0.88 % (1651196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.08/0.88 % (1651196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.88 % (1651196)CaDiCaL version: 2.1.3
% 3.08/0.88 % (1651196)Termination reason: Instruction limit
% 3.08/0.88 % (1651196)Termination phase: Property scanning
% 3.08/0.88 % (1651196)Time elapsed: 0.010 s
% 3.08/0.88 % (1651196)Peak memory usage: 10 MB
% 3.08/0.88 % (1651196)Instructions burned: 22 (million)
% 3.08/0.88 % (1651209)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3875200879:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.08/0.88 % (1651206)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=994238244:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.08/0.88 % (1651213)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=813587547:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.08/0.88 % (1651214)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=973849913:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.08/0.88 % (1651216)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2505774368:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.08/0.88 % (1651216)Instruction limit reached!
% 3.08/0.88 % (1651216)------------------------------
% 3.08/0.88 % (1651216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.08/0.88 % (1651216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.88 % (1651216)CaDiCaL version: 2.1.3
% 3.08/0.88 % (1651216)Termination reason: Instruction limit
% 3.08/0.88 % (1651216)Termination phase: Property scanning
% 3.08/0.88 % (1651216)Time elapsed: 0.011 s
% 3.08/0.88 % (1651216)Peak memory usage: 10 MB
% 3.08/0.88 % (1651216)Instructions burned: 21 (million)
% 3.08/0.88 % (1651213)Instruction limit reached!
% 3.08/0.88 % (1651213)------------------------------
% 3.08/0.88 % (1651213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.08/0.88 % (1651213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.88 % (1651213)CaDiCaL version: 2.1.3
% 3.08/0.88 % (1651213)Termination reason: Instruction limit
% 3.08/0.88 % (1651213)Termination phase: Preprocessing 1
% 3.08/0.88 % (1651213)Time elapsed: 0.021 s
% 3.08/0.88 % (1651213)Peak memory usage: 11 MB
% 3.08/0.88 % (1651213)Instructions burned: 45 (million)
% 3.08/0.88 % (1651237)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.08/0.88 % (1651237)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=271306862:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.08/0.88 % (1651090)Instruction limit reached!
% 3.08/0.88 % (1651090)------------------------------
% 3.08/0.88 % (1651090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651090)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651090)Termination reason: Instruction limit
% 5.49/1.09 % (1651090)Termination phase: Saturation
% 5.49/1.09 % (1651090)Time elapsed: 0.341 s
% 5.49/1.09 % (1651090)Peak memory usage: 15 MB
% 5.49/1.09 % (1651090)Instructions burned: 635 (million)
% 5.49/1.09 % (1651240)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1052480960:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 5.49/1.09 % (1651240)Instruction limit reached!
% 5.49/1.09 % (1651240)------------------------------
% 5.49/1.09 % (1651240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651240)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651240)Termination reason: Instruction limit
% 5.49/1.09 % (1651240)Termination phase: shuffling
% 5.49/1.09 % (1651240)Time elapsed: 0.010 s
% 5.49/1.09 % (1651240)Peak memory usage: 10 MB
% 5.49/1.09 % (1651240)Instructions burned: 13 (million)
% 5.49/1.09 % (1651249)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1275320178:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 5.49/1.09 % (1651250)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=325717333:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 5.49/1.09 % (1651249)Instruction limit reached!
% 5.49/1.09 % (1651249)------------------------------
% 5.49/1.09 % (1651249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651249)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651249)Termination reason: Instruction limit
% 5.49/1.09 % (1651249)Termination phase: SInE selection
% 5.49/1.09 % (1651249)Time elapsed: 0.031 s
% 5.49/1.09 % (1651249)Peak memory usage: 11 MB
% 5.49/1.09 % (1651249)Instructions burned: 67 (million)
% 5.49/1.09 % (1651250)Instruction limit reached!
% 5.49/1.09 % (1651250)------------------------------
% 5.49/1.09 % (1651250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651250)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651250)Termination reason: Instruction limit
% 5.49/1.09 % (1651250)Termination phase: Property scanning
% 5.49/1.09 % (1651250)Time elapsed: 0.024 s
% 5.49/1.09 % (1651250)Peak memory usage: 11 MB
% 5.49/1.09 % (1651250)Instructions burned: 51 (million)
% 5.49/1.09 % (1651264)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2484793052:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 5.49/1.09 % (1651266)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2680207748:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.49/1.09 % (1651237)Instruction limit reached!
% 5.49/1.09 % (1651237)------------------------------
% 5.49/1.09 % (1651237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651237)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651237)Termination reason: Instruction limit
% 5.49/1.09 % (1651237)Termination phase: Saturation
% 5.49/1.09 % (1651237)Time elapsed: 0.089 s
% 5.49/1.09 % (1651237)Peak memory usage: 13 MB
% 5.49/1.09 % (1651237)Instructions burned: 200 (million)
% 5.49/1.09 % (1651264)Instruction limit reached!
% 5.49/1.09 % (1651264)------------------------------
% 5.49/1.09 % (1651264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.09 % (1651264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.09 % (1651264)CaDiCaL version: 2.1.3
% 5.49/1.09 % (1651264)Termination reason: Instruction limit
% 5.49/1.09 % (1651264)Termination phase: Property scanning
% 5.49/1.09 % (1651264)Time elapsed: 0.015 s
% 5.49/1.09 % (1651264)Peak memory usage: 10 MB
% 5.49/1.09 % (1651264)Instructions burned: 32 (million)
% 5.49/1.09 % (1651274)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=789335000:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 6.80/1.32 % (1651275)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2619986765:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 6.80/1.32 % (1651206)Instruction limit reached!
% 6.80/1.32 % (1651206)------------------------------
% 6.80/1.32 % (1651206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651206)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651206)Termination reason: Instruction limit
% 6.80/1.32 % (1651206)Termination phase: Saturation
% 6.80/1.32 % (1651206)Time elapsed: 0.164 s
% 6.80/1.32 % (1651206)Peak memory usage: 16 MB
% 6.80/1.32 % (1651206)Instructions burned: 316 (million)
% 6.80/1.32 % (1651274)Instruction limit reached!
% 6.80/1.32 % (1651274)------------------------------
% 6.80/1.32 % (1651274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651274)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651274)Termination reason: Instruction limit
% 6.80/1.32 % (1651274)Termination phase: Property scanning
% 6.80/1.32 % (1651274)Time elapsed: 0.016 s
% 6.80/1.32 % (1651274)Peak memory usage: 10 MB
% 6.80/1.32 % (1651274)Instructions burned: 36 (million)
% 6.80/1.32 % (1651288)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.80/1.32 % (1651288)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=524012661:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 6.80/1.32 % (1651292)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1553868483:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 6.80/1.32 % (1651275)Instruction limit reached!
% 6.80/1.32 % (1651275)------------------------------
% 6.80/1.32 % (1651275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651275)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651275)Termination reason: Instruction limit
% 6.80/1.32 % (1651275)Termination phase: Equality resolution with deletion
% 6.80/1.32 % (1651275)Time elapsed: 0.034 s
% 6.80/1.32 % (1651275)Peak memory usage: 12 MB
% 6.80/1.32 % (1651275)Instructions burned: 69 (million)
% 6.80/1.32 % (1651266)Instruction limit reached!
% 6.80/1.32 % (1651266)------------------------------
% 6.80/1.32 % (1651266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651266)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651266)Termination reason: Instruction limit
% 6.80/1.32 % (1651266)Termination phase: Saturation
% 6.80/1.32 % (1651266)Time elapsed: 0.075 s
% 6.80/1.32 % (1651266)Peak memory usage: 14 MB
% 6.80/1.32 % (1651266)Instructions burned: 137 (million)
% 6.80/1.32 % (1651298)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4152809334:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 6.80/1.32 % (1651299)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2696118484:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 6.80/1.32 % (1651214)Instruction limit reached!
% 6.80/1.32 % (1651214)------------------------------
% 6.80/1.32 % (1651214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651214)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651214)Termination reason: Instruction limit
% 6.80/1.32 % (1651214)Termination phase: Saturation
% 6.80/1.32 % (1651214)Time elapsed: 0.238 s
% 6.80/1.32 % (1651214)Peak memory usage: 16 MB
% 6.80/1.32 % (1651214)Instructions burned: 481 (million)
% 6.80/1.32 % (1651209)Instruction limit reached!
% 6.80/1.32 % (1651209)------------------------------
% 6.80/1.32 % (1651209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.32 % (1651209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.32 % (1651209)CaDiCaL version: 2.1.3
% 6.80/1.32 % (1651209)Termination reason: Instruction limit
% 6.80/1.32 % (1651209)Termination phase: Saturation
% 6.80/1.32 % (1651209)Time elapsed: 0.256 s
% 6.80/1.32 % (1651209)Peak memory usage: 16 MB
% 6.80/1.32 % (1651209)Instructions burned: 854 (million)
% 7.06/1.45 % (1651313)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=533394087:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 7.06/1.45 % (1651288)Instruction limit reached!
% 7.06/1.45 % (1651288)------------------------------
% 7.06/1.45 % (1651288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.45 % (1651288)CaDiCaL version: 2.1.3
% 7.06/1.45 % (1651288)Termination reason: Instruction limit
% 7.06/1.45 % (1651288)Termination phase: Saturation
% 7.06/1.45 % (1651288)Time elapsed: 0.078 s
% 7.06/1.45 % (1651288)Peak memory usage: 13 MB
% 7.06/1.45 % (1651288)Instructions burned: 181 (million)
% 7.06/1.45 % (1651298)Instruction limit reached!
% 7.06/1.45 % (1651298)------------------------------
% 7.06/1.45 % (1651298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.45 % (1651298)CaDiCaL version: 2.1.3
% 7.06/1.45 % (1651298)Termination reason: Instruction limit
% 7.06/1.45 % (1651298)Termination phase: Saturation
% 7.06/1.45 % (1651298)Time elapsed: 0.055 s
% 7.06/1.45 % (1651298)Peak memory usage: 13 MB
% 7.06/1.45 % (1651298)Instructions burned: 97 (million)
% 7.06/1.45 % (1651314)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=248023857:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 7.06/1.45 % (1651319)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3615429065:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 7.06/1.45 % (1651321)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1529660498:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 7.06/1.45 % (1651292)Instruction limit reached!
% 7.06/1.45 % (1651292)------------------------------
% 7.06/1.45 % (1651292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.45 % (1651292)CaDiCaL version: 2.1.3
% 7.06/1.45 % (1651292)Termination reason: Instruction limit
% 7.06/1.45 % (1651292)Termination phase: Saturation
% 7.06/1.45 % (1651292)Time elapsed: 0.124 s
% 7.06/1.45 % (1651292)Peak memory usage: 14 MB
% 7.06/1.45 % (1651292)Instructions burned: 247 (million)
% 7.06/1.45 % (1651321)Instruction limit reached!
% 7.06/1.45 % (1651321)------------------------------
% 7.06/1.45 % (1651321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.45 % (1651321)CaDiCaL version: 2.1.3
% 7.06/1.45 % (1651321)Termination reason: Instruction limit
% 7.06/1.45 % (1651321)Termination phase: Property scanning
% 7.06/1.45 % (1651321)Time elapsed: 0.038 s
% 7.06/1.45 % (1651321)Peak memory usage: 10 MB
% 7.06/1.45 % (1651321)Instructions burned: 45 (million)
% 7.06/1.45 % (1651340)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2468773940:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 7.06/1.45 % (1651319)Instruction limit reached!
% 7.06/1.45 % (1651319)------------------------------
% 7.06/1.45 % (1651319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.45 % (1651319)CaDiCaL version: 2.1.3
% 7.06/1.45 % (1651319)Termination reason: Instruction limit
% 7.06/1.45 % (1651319)Termination phase: Saturation
% 7.06/1.45 % (1651319)Time elapsed: 0.067 s
% 7.06/1.45 % (1651319)Peak memory usage: 13 MB
% 7.06/1.45 % (1651319)Instructions burned: 130 (million)
% 7.06/1.45 % (1651342)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1749741577:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 7.06/1.45 % (1651351)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2661345246:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 7.06/1.45 % (1651351)Instruction limit reached!
% 7.06/1.45 % (1651351)------------------------------
% 7.06/1.45 % (1651351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/1.45 % (1651351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651351)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651351)Termination reason: Instruction limit
% 7.90/1.68 % (1651351)Termination phase: Saturation
% 7.90/1.68 % (1651351)Time elapsed: 0.079 s
% 7.90/1.68 % (1651351)Peak memory usage: 13 MB
% 7.90/1.68 % (1651351)Instructions burned: 96 (million)
% 7.90/1.68 % (1651364)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=4191485266:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2991 on theBenchmark for (2991ds/65Mi)
% 7.90/1.68 % (1651299)Instruction limit reached!
% 7.90/1.68 % (1651299)------------------------------
% 7.90/1.68 % (1651299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.90/1.68 % (1651299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651299)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651299)Termination reason: Instruction limit
% 7.90/1.68 % (1651299)Termination phase: Saturation
% 7.90/1.68 % (1651299)Time elapsed: 0.296 s
% 7.90/1.68 % (1651299)Peak memory usage: 16 MB
% 7.90/1.68 % (1651299)Instructions burned: 429 (million)
% 7.90/1.68 % (1651313)Instruction limit reached!
% 7.90/1.68 % (1651313)------------------------------
% 7.90/1.68 % (1651313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.90/1.68 % (1651313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651313)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651313)Termination reason: Instruction limit
% 7.90/1.68 % (1651313)Termination phase: Saturation
% 7.90/1.68 % (1651313)Time elapsed: 0.281 s
% 7.90/1.68 % (1651313)Peak memory usage: 16 MB
% 7.90/1.68 % (1651313)Instructions burned: 876 (million)
% 7.90/1.68 % (1651374)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=134967535:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2991 on theBenchmark for (2991ds/105Mi)
% 7.90/1.68 % (1651364)Instruction limit reached!
% 7.90/1.68 % (1651364)------------------------------
% 7.90/1.68 % (1651364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.90/1.68 % (1651364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651364)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651364)Termination reason: Instruction limit
% 7.90/1.68 % (1651364)Termination phase: SInE selection
% 7.90/1.68 % (1651364)Time elapsed: 0.054 s
% 7.90/1.68 % (1651364)Peak memory usage: 11 MB
% 7.90/1.68 % (1651364)Instructions burned: 65 (million)
% 7.90/1.68 % (1651376)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=3183854411:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 7.90/1.68 % (1651379)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=924246651:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/375Mi)
% 7.90/1.68 % (1651374)Instruction limit reached!
% 7.90/1.68 % (1651374)------------------------------
% 7.90/1.68 % (1651374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.90/1.68 % (1651374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651374)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651374)Termination reason: Instruction limit
% 7.90/1.68 % (1651374)Termination phase: Property scanning
% 7.90/1.68 % (1651374)Time elapsed: 0.083 s
% 7.90/1.68 % (1651374)Peak memory usage: 11 MB
% 7.90/1.68 % (1651374)Instructions burned: 105 (million)
% 7.90/1.68 % (1651384)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2975400062:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/495Mi)
% 7.90/1.68 % (1651314)Instruction limit reached!
% 7.90/1.68 % (1651314)------------------------------
% 7.90/1.68 % (1651314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.90/1.68 % (1651314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.68 % (1651314)CaDiCaL version: 2.1.3
% 7.90/1.68 % (1651314)Termination reason: Instruction limit
% 7.90/1.68 % (1651314)Termination phase: Saturation
% 7.90/1.68 % (1651314)Time elapsed: 0.402 s
% 7.90/1.68 % (1651314)Peak memory usage: 16 MB
% 7.90/1.68 % (1651314)Instructions burned: 515 (million)
% 7.90/1.68 % (1651151)Instruction limit reached!
% 9.31/1.92 % (1651151)------------------------------
% 9.31/1.92 % (1651151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651151)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651151)Termination reason: Instruction limit
% 9.31/1.92 % (1651151)Termination phase: Saturation
% 9.31/1.92 % (1651151)Time elapsed: 0.813 s
% 9.31/1.92 % (1651151)Peak memory usage: 19 MB
% 9.31/1.92 % (1651151)Instructions burned: 1241 (million)
% 9.31/1.92 % (1651389)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3658168792:cond=on:i=34:hud=10:nm=10:rtra=on_2989 on theBenchmark for (2989ds/34Mi)
% 9.31/1.92 % (1651390)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3097346731:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/91Mi)
% 9.31/1.92 % (1651342)Instruction limit reached!
% 9.31/1.92 % (1651342)------------------------------
% 9.31/1.92 % (1651342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651342)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651342)Termination reason: Instruction limit
% 9.31/1.92 % (1651342)Termination phase: Saturation
% 9.31/1.92 % (1651342)Time elapsed: 0.374 s
% 9.31/1.92 % (1651342)Peak memory usage: 15 MB
% 9.31/1.92 % (1651342)Instructions burned: 451 (million)
% 9.31/1.92 % (1651389)Instruction limit reached!
% 9.31/1.92 % (1651389)------------------------------
% 9.31/1.92 % (1651389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651389)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651389)Termination reason: Instruction limit
% 9.31/1.92 % (1651389)Termination phase: Property scanning
% 9.31/1.92 % (1651389)Time elapsed: 0.029 s
% 9.31/1.92 % (1651389)Peak memory usage: 10 MB
% 9.31/1.92 % (1651389)Instructions burned: 34 (million)
% 9.31/1.92 % (1651393)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=4031003239:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 9.31/1.92 % (1651394)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2467275896:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2989 on theBenchmark for (2989ds/22Mi)
% 9.31/1.92 % (1651393)Instruction limit reached!
% 9.31/1.92 % (1651393)------------------------------
% 9.31/1.92 % (1651393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651393)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651393)Termination reason: Instruction limit
% 9.31/1.92 % (1651393)Termination phase: Saturation
% 9.31/1.92 % (1651393)Time elapsed: 0.034 s
% 9.31/1.92 % (1651393)Peak memory usage: 13 MB
% 9.31/1.92 % (1651393)Instructions burned: 66 (million)
% 9.31/1.92 % (1651394)Instruction limit reached!
% 9.31/1.92 % (1651394)------------------------------
% 9.31/1.92 % (1651394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651394)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651394)Termination reason: Instruction limit
% 9.31/1.92 % (1651394)Termination phase: Property scanning
% 9.31/1.92 % (1651394)Time elapsed: 0.020 s
% 9.31/1.92 % (1651394)Peak memory usage: 10 MB
% 9.31/1.92 % (1651394)Instructions burned: 22 (million)
% 9.31/1.92 % (1651340)Instruction limit reached!
% 9.31/1.92 % (1651340)------------------------------
% 9.31/1.92 % (1651340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.31/1.92 % (1651340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.31/1.92 % (1651340)CaDiCaL version: 2.1.3
% 9.31/1.92 % (1651340)Termination reason: Instruction limit
% 9.31/1.92 % (1651340)Termination phase: Saturation
% 9.31/1.92 % (1651340)Time elapsed: 0.465 s
% 9.31/1.92 % (1651340)Peak memory usage: 16 MB
% 9.31/1.92 % (1651340)Instructions burned: 572 (million)
% 9.31/1.92 % (1651399)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=2633477013:i=338:bd=all:ins=4:rtra=on_2988 on theBenchmark for (2988ds/338Mi)
% 9.31/1.92 % (1651390)Instruction limit reached!
% 12.90/2.17 % (1651390)------------------------------
% 12.90/2.17 % (1651390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.90/2.17 % (1651390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.17 % (1651390)CaDiCaL version: 2.1.3
% 12.90/2.17 % (1651390)Termination reason: Instruction limit
% 12.90/2.17 % (1651390)Termination phase: Property scanning
% 12.90/2.17 % (1651390)Time elapsed: 0.084 s
% 12.90/2.17 % (1651390)Peak memory usage: 12 MB
% 12.90/2.17 % (1651390)Instructions burned: 91 (million)
% 12.90/2.17 % (1651400)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2336241968:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/28Mi)
% 12.90/2.17 % (1651401)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 12.90/2.17 % (1651401)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3012086199:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/137Mi)
% 12.90/2.17 % (1651403)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=2485654841:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/340Mi)
% 12.90/2.17 % (1651400)Instruction limit reached!
% 12.90/2.17 % (1651400)------------------------------
% 12.90/2.17 % (1651400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.90/2.17 % (1651400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.17 % (1651400)CaDiCaL version: 2.1.3
% 12.90/2.17 % (1651400)Termination reason: Instruction limit
% 12.90/2.17 % (1651400)Termination phase: Property scanning
% 12.90/2.17 % (1651400)Time elapsed: 0.025 s
% 12.90/2.17 % (1651400)Peak memory usage: 10 MB
% 12.90/2.17 % (1651400)Instructions burned: 29 (million)
% 12.90/2.17 % (1651407)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=431922575:i=227:sd=1:bd=all:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/227Mi)
% 12.90/2.17 % (1651379)Instruction limit reached!
% 12.90/2.17 % (1651379)------------------------------
% 12.90/2.17 % (1651379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.90/2.17 % (1651379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.17 % (1651379)CaDiCaL version: 2.1.3
% 12.90/2.17 % (1651379)Termination reason: Instruction limit
% 12.90/2.17 % (1651379)Termination phase: Saturation
% 12.90/2.17 % (1651379)Time elapsed: 0.330 s
% 12.90/2.17 % (1651379)Peak memory usage: 15 MB
% 12.90/2.17 % (1651379)Instructions burned: 376 (million)
% 12.90/2.17 % (1651401)Instruction limit reached!
% 12.90/2.17 % (1651401)------------------------------
% 12.90/2.17 % (1651401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.90/2.17 % (1651401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.17 % (1651401)CaDiCaL version: 2.1.3
% 12.90/2.17 % (1651401)Termination reason: Instruction limit
% 12.90/2.17 % (1651401)Termination phase: Saturation
% 12.90/2.17 % (1651401)Time elapsed: 0.111 s
% 12.90/2.17 % (1651401)Peak memory usage: 13 MB
% 12.90/2.17 % (1651401)Instructions burned: 137 (million)
% 12.90/2.17 % (1651409)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 12.90/2.17 % (1651409)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3214134011:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/373Mi)
% 12.90/2.17 % (1651410)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2912542697:i=116:ep=RSTC:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/116Mi)
% 12.90/2.17 % (1651410)Instruction limit reached!
% 12.90/2.17 % (1651410)------------------------------
% 12.90/2.17 % (1651410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.90/2.17 % (1651410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.17 % (1651410)CaDiCaL version: 2.1.3
% 12.90/2.17 % (1651410)Termination reason: Instruction limit
% 12.90/2.17 % (1651410)Termination phase: Saturation
% 12.90/2.17 % (1651410)Time elapsed: 0.059 s
% 12.90/2.17 % (1651410)Peak memory usage: 13 MB
% 12.90/2.17 % (1651410)Instructions burned: 116 (million)
% 12.90/2.17 % (1651416)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2318351820:i=575:rtra=on_2986 on theBenchmark for (2986ds/575Mi)
% 14.26/2.42 % (1651403)Instruction limit reached!
% 14.26/2.42 % (1651403)------------------------------
% 14.26/2.42 % (1651403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.26/2.42 % (1651403)CaDiCaL version: 2.1.3
% 14.26/2.42 % (1651403)Termination reason: Instruction limit
% 14.26/2.42 % (1651403)Termination phase: Saturation
% 14.26/2.42 % (1651403)Time elapsed: 0.230 s
% 14.26/2.42 % (1651403)Peak memory usage: 15 MB
% 14.26/2.42 % (1651403)Instructions burned: 340 (million)
% 14.26/2.42 % (1651407)Instruction limit reached!
% 14.26/2.42 % (1651407)------------------------------
% 14.26/2.42 % (1651407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.26/2.42 % (1651407)CaDiCaL version: 2.1.3
% 14.26/2.42 % (1651407)Termination reason: Instruction limit
% 14.26/2.42 % (1651407)Termination phase: Saturation
% 14.26/2.42 % (1651407)Time elapsed: 0.198 s
% 14.26/2.42 % (1651407)Peak memory usage: 14 MB
% 14.26/2.42 % (1651407)Instructions burned: 227 (million)
% 14.26/2.42 % (1651420)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=911504014:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2985 on theBenchmark for (2985ds/270Mi)
% 14.26/2.42 % (1651384)Instruction limit reached!
% 14.26/2.42 % (1651384)------------------------------
% 14.26/2.42 % (1651384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.26/2.42 % (1651384)CaDiCaL version: 2.1.3
% 14.26/2.42 % (1651384)Termination reason: Instruction limit
% 14.26/2.42 % (1651384)Termination phase: Saturation
% 14.26/2.42 % (1651384)Time elapsed: 0.452 s
% 14.26/2.42 % (1651384)Peak memory usage: 16 MB
% 14.26/2.42 % (1651384)Instructions burned: 495 (million)
% 14.26/2.42 % (1651421)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=1551555217:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2985 on theBenchmark for (2985ds/9840Mi)
% 14.26/2.42 % (1651399)Instruction limit reached!
% 14.26/2.42 % (1651399)------------------------------
% 14.26/2.42 % (1651399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.26/2.42 % (1651399)CaDiCaL version: 2.1.3
% 14.26/2.42 % (1651399)Termination reason: Instruction limit
% 14.26/2.42 % (1651399)Termination phase: Saturation
% 14.26/2.42 % (1651399)Time elapsed: 0.309 s
% 14.26/2.42 % (1651399)Peak memory usage: 17 MB
% 14.26/2.42 % (1651399)Instructions burned: 338 (million)
% 14.26/2.42 % (1651425)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2004098588:i=421:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/421Mi)
% 14.26/2.42 % (1651427)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 14.26/2.42 % (1651427)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=3369784887:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/270Mi)
% 14.26/2.42 % (1651409)Instruction limit reached!
% 14.26/2.42 % (1651409)------------------------------
% 14.26/2.42 % (1651409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.26/2.42 % (1651409)CaDiCaL version: 2.1.3
% 14.26/2.42 % (1651409)Termination reason: Instruction limit
% 14.26/2.42 % (1651409)Termination phase: Saturation
% 14.26/2.42 % (1651409)Time elapsed: 0.325 s
% 14.26/2.42 % (1651409)Peak memory usage: 13 MB
% 14.26/2.42 % (1651409)Instructions burned: 374 (million)
% 14.26/2.42 % (1651420)Instruction limit reached!
% 14.26/2.42 % (1651420)------------------------------
% 14.26/2.42 % (1651420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.26/2.42 % (1651420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651420)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651420)Termination reason: Instruction limit
% 16.22/2.73 % (1651420)Termination phase: Saturation
% 16.22/2.73 % (1651420)Time elapsed: 0.186 s
% 16.22/2.73 % (1651420)Peak memory usage: 13 MB
% 16.22/2.73 % (1651420)Instructions burned: 270 (million)
% 16.22/2.73 % (1651435)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1320435306:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/31Mi)
% 16.22/2.73 % (1651437)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 16.22/2.73 % (1651437)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
% 16.22/2.73 % (1651435)Instruction limit reached!
% 16.22/2.73 % (1651435)------------------------------
% 16.22/2.73 % (1651435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.22/2.73 % (1651435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651435)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651435)Termination reason: Instruction limit
% 16.22/2.73 % (1651435)Termination phase: Property scanning
% 16.22/2.73 % (1651435)Time elapsed: 0.016 s
% 16.22/2.73 % (1651435)Peak memory usage: 10 MB
% 16.22/2.73 % (1651435)Instructions burned: 32 (million)
% 16.22/2.73 % (1651437)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=3005384445:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2983 on theBenchmark for (2983ds/1440Mi)
% 16.22/2.73 % (1651440)dis+10_2_sil=128000:si=on:random_seed=2275953652:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2983 on theBenchmark for (2983ds/339Mi)
% 16.22/2.73 % (1651427)Instruction limit reached!
% 16.22/2.73 % (1651427)------------------------------
% 16.22/2.73 % (1651427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.22/2.73 % (1651427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651427)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651427)Termination reason: Instruction limit
% 16.22/2.73 % (1651427)Termination phase: Saturation
% 16.22/2.73 % (1651427)Time elapsed: 0.251 s
% 16.22/2.73 % (1651427)Peak memory usage: 15 MB
% 16.22/2.73 % (1651427)Instructions burned: 270 (million)
% 16.22/2.73 % (1651445)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2700619524:i=111:add=on:fgj=on:rtra=on:fdi=1024_2982 on theBenchmark for (2982ds/111Mi)
% 16.22/2.73 % (1651425)Instruction limit reached!
% 16.22/2.73 % (1651425)------------------------------
% 16.22/2.73 % (1651425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.22/2.73 % (1651425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651425)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651425)Termination reason: Instruction limit
% 16.22/2.73 % (1651425)Termination phase: Saturation
% 16.22/2.73 % (1651425)Time elapsed: 0.328 s
% 16.22/2.73 % (1651425)Peak memory usage: 16 MB
% 16.22/2.73 % (1651425)Instructions burned: 422 (million)
% 16.22/2.73 % (1651447)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=269595189:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2981 on theBenchmark for (2981ds/122Mi)
% 16.22/2.73 % (1651445)Instruction limit reached!
% 16.22/2.73 % (1651445)------------------------------
% 16.22/2.73 % (1651445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.22/2.73 % (1651445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651445)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651445)Termination reason: Instruction limit
% 16.22/2.73 % (1651445)Termination phase: Saturation
% 16.22/2.73 % (1651445)Time elapsed: 0.094 s
% 16.22/2.73 % (1651445)Peak memory usage: 13 MB
% 16.22/2.73 % (1651445)Instructions burned: 111 (million)
% 16.22/2.73 % (1651416)Instruction limit reached!
% 16.22/2.73 % (1651416)------------------------------
% 16.22/2.73 % (1651416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.22/2.73 % (1651416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/2.73 % (1651416)CaDiCaL version: 2.1.3
% 16.22/2.73 % (1651416)Termination reason: Instruction limit
% 16.22/2.73 % (1651416)Termination phase: Saturation
% 19.96/3.16 % (1651416)Time elapsed: 0.496 s
% 19.96/3.16 % (1651416)Peak memory usage: 16 MB
% 19.96/3.16 % (1651416)Instructions burned: 576 (million)
% 19.96/3.16 % (1651449)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3637858807:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/136Mi)
% 19.96/3.16 % (1651447)Refutation not found, incomplete strategy
% 19.96/3.16 % (1651447)------------------------------
% 19.96/3.16 % (1651447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.96/3.16 % (1651447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.96/3.16 % (1651447)CaDiCaL version: 2.1.3
% 19.96/3.16 % (1651447)Termination reason: Refutation not found, incomplete strategy
% 19.96/3.16 % (1651447)Time elapsed: 0.073 s
% 19.96/3.16 % (1651447)Peak memory usage: 14 MB
% 19.96/3.16 % (1651447)Instructions burned: 106 (million)
% 19.96/3.16 % (1651447)------------------------------
% 19.96/3.16 % (1651447)------------------------------
% 19.96/3.16 % (1651440)Instruction limit reached!
% 19.96/3.16 % (1651440)------------------------------
% 19.96/3.16 % (1651440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.96/3.16 % (1651440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.96/3.16 % (1651440)CaDiCaL version: 2.1.3
% 19.96/3.16 % (1651440)Termination reason: Instruction limit
% 19.96/3.16 % (1651440)Termination phase: Saturation
% 19.96/3.16 % (1651440)Time elapsed: 0.238 s
% 19.96/3.16 % (1651440)Peak memory usage: 14 MB
% 19.96/3.16 % (1651440)Instructions burned: 340 (million)
% 19.96/3.16 % (1651451)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1388047777:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2981 on theBenchmark for (2981ds/232Mi)
% 19.96/3.16 % (1651453)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=61838051:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2980 on theBenchmark for (2980ds/1254Mi)
% 19.96/3.16 % (1651456)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 19.96/3.16 % (1651456)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=356927146:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2980 on theBenchmark for (2980ds/281Mi)
% 19.96/3.16 % (1651449)Instruction limit reached!
% 19.96/3.16 % (1651449)------------------------------
% 19.96/3.16 % (1651449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.96/3.16 % (1651449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.96/3.16 % (1651449)CaDiCaL version: 2.1.3
% 19.96/3.16 % (1651449)Termination reason: Instruction limit
% 19.96/3.16 % (1651449)Termination phase: Saturation
% 19.96/3.16 % (1651449)Time elapsed: 0.113 s
% 19.96/3.16 % (1651449)Peak memory usage: 14 MB
% 19.96/3.16 % (1651449)Instructions burned: 137 (million)
% 19.96/3.16 % (1651461)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1453175924:i=619:add=on:rtra=on_2979 on theBenchmark for (2979ds/619Mi)
% 19.96/3.16 % (1651456)Instruction limit reached!
% 19.96/3.16 % (1651456)------------------------------
% 19.96/3.16 % (1651456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.96/3.16 % (1651456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.96/3.16 % (1651456)CaDiCaL version: 2.1.3
% 19.96/3.16 % (1651456)Termination reason: Instruction limit
% 19.96/3.16 % (1651456)Termination phase: Saturation
% 19.96/3.16 % (1651456)Time elapsed: 0.143 s
% 19.96/3.16 % (1651456)Peak memory usage: 14 MB
% 19.96/3.16 % (1651456)Instructions burned: 282 (million)
% 19.96/3.16 % (1651465)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3336072525:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/865Mi)
% 19.96/3.16 % (1651451)Instruction limit reached!
% 19.96/3.16 % (1651451)------------------------------
% 19.96/3.16 % (1651451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.96/3.16 % (1651451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.96/3.16 % (1651451)CaDiCaL version: 2.1.3
% 19.96/3.16 % (1651451)Termination reason: Instruction limit
% 21.66/3.55 % (1651451)Termination phase: Saturation
% 21.66/3.55 % (1651451)Time elapsed: 0.208 s
% 21.66/3.55 % (1651451)Peak memory usage: 14 MB
% 21.66/3.55 % (1651451)Instructions burned: 232 (million)
% 21.66/3.55 % (1651453)Refutation not found, incomplete strategy
% 21.66/3.55 % (1651453)------------------------------
% 21.66/3.55 % (1651453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651453)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651453)Termination reason: Refutation not found, incomplete strategy
% 21.66/3.55 % (1651453)Time elapsed: 0.205 s
% 21.66/3.55 % (1651453)Peak memory usage: 15 MB
% 21.66/3.55 % (1651453)Instructions burned: 245 (million)
% 21.66/3.55 % (1651453)------------------------------
% 21.66/3.55 % (1651453)------------------------------
% 21.66/3.55 % (1651467)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3893457042:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/212Mi)
% 21.66/3.55 % (1651468)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2601821076:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/130Mi)
% 21.66/3.55 % (1651461)Refutation not found, incomplete strategy
% 21.66/3.55 % (1651461)------------------------------
% 21.66/3.55 % (1651461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651461)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651461)Termination reason: Refutation not found, incomplete strategy
% 21.66/3.55 % (1651461)Time elapsed: 0.143 s
% 21.66/3.55 % (1651461)Peak memory usage: 15 MB
% 21.66/3.55 % (1651461)Instructions burned: 170 (million)
% 21.66/3.55 % (1651461)------------------------------
% 21.66/3.55 % (1651461)------------------------------
% 21.66/3.55 % (1651471)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2429675201:st=1.5:i=346:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/346Mi)
% 21.66/3.55 % (1651468)Instruction limit reached!
% 21.66/3.55 % (1651468)------------------------------
% 21.66/3.55 % (1651468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651468)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651468)Termination reason: Instruction limit
% 21.66/3.55 % (1651468)Termination phase: Saturation
% 21.66/3.55 % (1651468)Time elapsed: 0.104 s
% 21.66/3.55 % (1651468)Peak memory usage: 13 MB
% 21.66/3.55 % (1651468)Instructions burned: 130 (million)
% 21.66/3.55 % (1651473)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=4258965426:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2977 on theBenchmark for (2977ds/152Mi)
% 21.66/3.55 % (1651467)Instruction limit reached!
% 21.66/3.55 % (1651467)------------------------------
% 21.66/3.55 % (1651467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651467)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651467)Termination reason: Instruction limit
% 21.66/3.55 % (1651467)Termination phase: Saturation
% 21.66/3.55 % (1651467)Time elapsed: 0.192 s
% 21.66/3.55 % (1651467)Peak memory usage: 14 MB
% 21.66/3.55 % (1651467)Instructions burned: 212 (million)
% 21.66/3.55 % (1651475)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3674500831:i=75:ep=R:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/75Mi)
% 21.66/3.55 % (1651473)Instruction limit reached!
% 21.66/3.55 % (1651473)------------------------------
% 21.66/3.55 % (1651473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651473)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651473)Termination reason: Instruction limit
% 21.66/3.55 % (1651473)Termination phase: Saturation
% 21.66/3.55 % (1651473)Time elapsed: 0.127 s
% 21.66/3.55 % (1651473)Peak memory usage: 14 MB
% 21.66/3.55 % (1651473)Instructions burned: 152 (million)
% 21.66/3.55 % (1651475)Instruction limit reached!
% 21.66/3.55 % (1651475)------------------------------
% 21.66/3.55 % (1651475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.66/3.55 % (1651475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/3.55 % (1651475)CaDiCaL version: 2.1.3
% 21.66/3.55 % (1651475)Termination reason: Instruction limit
% 22.30/3.63 % (1651475)Termination phase: Preprocessing 1
% 22.30/3.63 % (1651475)Time elapsed: 0.062 s
% 22.30/3.63 % (1651475)Peak memory usage: 10 MB
% 22.30/3.63 % (1651475)Instructions burned: 75 (million)
% 22.30/3.63 % (1651480)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=818133163:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2975 on theBenchmark for (2975ds/148Mi)
% 22.30/3.63 % (1651479)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=4121832149:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/387Mi)
% 22.30/3.63 % (1651471)Instruction limit reached!
% 22.30/3.63 % (1651471)------------------------------
% 22.30/3.63 % (1651471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.63 % (1651471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.63 % (1651471)CaDiCaL version: 2.1.3
% 22.30/3.63 % (1651471)Termination reason: Instruction limit
% 22.30/3.63 % (1651471)Termination phase: Saturation
% 22.30/3.63 % (1651471)Time elapsed: 0.303 s
% 22.30/3.64 % (1651471)Peak memory usage: 14 MB
% 22.30/3.64 % (1651471)Instructions burned: 347 (million)
% 22.30/3.64 % (1651480)Instruction limit reached!
% 22.30/3.64 % (1651480)------------------------------
% 22.30/3.64 % (1651480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651480)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651480)Termination reason: Instruction limit
% 22.30/3.64 % (1651480)Termination phase: Saturation
% 22.30/3.64 % (1651480)Time elapsed: 0.088 s
% 22.30/3.64 % (1651480)Peak memory usage: 13 MB
% 22.30/3.64 % (1651480)Instructions burned: 148 (million)
% 22.30/3.64 % (1651483)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1963023549:i=161:piset=and:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/161Mi)
% 22.30/3.64 % (1651484)lrs+10_1_sil=128000:si=on:random_seed=3055929021:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/888Mi)
% 22.30/3.64 % (1651483)Instruction limit reached!
% 22.30/3.64 % (1651483)------------------------------
% 22.30/3.64 % (1651483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651483)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651483)Termination reason: Instruction limit
% 22.30/3.64 % (1651483)Termination phase: Saturation
% 22.30/3.64 % (1651483)Time elapsed: 0.144 s
% 22.30/3.64 % (1651483)Peak memory usage: 14 MB
% 22.30/3.64 % (1651483)Instructions burned: 161 (million)
% 22.30/3.64 % (1651487)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=2881657400:i=136:add=on:ins=4:rtra=on:sup=off_2972 on theBenchmark for (2972ds/136Mi)
% 22.30/3.64 % (1651479)Instruction limit reached!
% 22.30/3.64 % (1651479)------------------------------
% 22.30/3.64 % (1651479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651479)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651479)Termination reason: Instruction limit
% 22.30/3.64 % (1651479)Termination phase: Saturation
% 22.30/3.64 % (1651479)Time elapsed: 0.345 s
% 22.30/3.64 % (1651479)Peak memory usage: 14 MB
% 22.30/3.64 % (1651479)Instructions burned: 388 (million)
% 22.30/3.64 % (1651437)Instruction limit reached!
% 22.30/3.64 % (1651437)------------------------------
% 22.30/3.64 % (1651437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651437)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651437)Termination reason: Instruction limit
% 22.30/3.64 % (1651437)Termination phase: Saturation
% 22.30/3.64 % (1651437)Time elapsed: 1.167 s
% 22.30/3.64 % (1651437)Peak memory usage: 16 MB
% 22.30/3.64 % (1651437)Instructions burned: 1441 (million)
% 22.30/3.64 % (1651491)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1352094707:i=88:s2at=3:nm=2:rtra=on:rawr=on_2971 on theBenchmark for (2971ds/88Mi)
% 22.30/3.64 % (1651492)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=1902660981:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2971 on theBenchmark for (2971ds/93Mi)
% 22.30/3.64 % (1651487)Instruction limit reached!
% 22.30/3.64 % (1651487)------------------------------
% 22.30/3.64 % (1651487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651487)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651487)Termination reason: Instruction limit
% 22.30/3.64 % (1651487)Termination phase: Saturation
% 22.30/3.64 % (1651487)Time elapsed: 0.128 s
% 22.30/3.64 % (1651487)Peak memory usage: 13 MB
% 22.30/3.64 % (1651487)Instructions burned: 137 (million)
% 22.30/3.64 % (1651495)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2238158291:i=2186:rtra=on:ixr=off_2971 on theBenchmark for (2971ds/2186Mi)
% 22.30/3.64 % (1651465)Instruction limit reached!
% 22.30/3.64 % (1651465)------------------------------
% 22.30/3.64 % (1651465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651465)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651465)Termination reason: Instruction limit
% 22.30/3.64 % (1651465)Termination phase: Saturation
% 22.30/3.64 % (1651465)Time elapsed: 0.803 s
% 22.30/3.64 % (1651465)Peak memory usage: 23 MB
% 22.30/3.64 % (1651465)Instructions burned: 866 (million)
% 22.30/3.64 % (1651491)Instruction limit reached!
% 22.30/3.64 % (1651491)------------------------------
% 22.30/3.64 % (1651491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651491)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651491)Termination reason: Instruction limit
% 22.30/3.64 % (1651491)Termination phase: Preprocessing 3
% 22.30/3.64 % (1651491)Time elapsed: 0.072 s
% 22.30/3.64 % (1651491)Peak memory usage: 11 MB
% 22.30/3.64 % (1651491)Instructions burned: 89 (million)
% 22.30/3.64 % (1651498)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=366266288:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2970 on theBenchmark for (2970ds/805Mi)
% 22.30/3.64 % (1651492)Instruction limit reached!
% 22.30/3.64 % (1651492)------------------------------
% 22.30/3.64 % (1651492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651492)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651492)Termination reason: Instruction limit
% 22.30/3.64 % (1651492)Termination phase: Preprocessing 3
% 22.30/3.64 % (1651492)Time elapsed: 0.075 s
% 22.30/3.64 % (1651492)Peak memory usage: 11 MB
% 22.30/3.64 % (1651492)Instructions burned: 93 (million)
% 22.30/3.64 % (1651497)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2165328493:s2a=on:i=240:rtra=on:ntd=on_2970 on theBenchmark for (2970ds/240Mi)
% 22.30/3.64 % (1651500)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 22.30/3.64 % (1651500)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2298188017:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2970 on theBenchmark for (2970ds/391Mi)
% 22.30/3.64 % (1651497)Instruction limit reached!
% 22.30/3.64 % (1651497)------------------------------
% 22.30/3.64 % (1651497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651497)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651497)Termination reason: Instruction limit
% 22.30/3.64 % (1651497)Termination phase: Saturation
% 22.30/3.64 % (1651497)Time elapsed: 0.222 s
% 22.30/3.64 % (1651497)Peak memory usage: 15 MB
% 22.30/3.64 % (1651497)Instructions burned: 240 (million)
% 22.30/3.64 % (1651503)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=2503253093:i=355:av=off:fsr=off:rtra=on:ixr=off_2968 on theBenchmark for (2968ds/355Mi)
% 22.30/3.64 % (1651500)Instruction limit reached!
% 22.30/3.64 % (1651500)------------------------------
% 22.30/3.64 % (1651500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651500)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651500)Termination reason: Instruction limit
% 22.30/3.64 % (1651500)Termination phase: Saturation
% 22.30/3.64 % (1651500)Time elapsed: 0.297 s
% 22.30/3.64 % (1651500)Peak memory usage: 14 MB
% 22.30/3.64 % (1651500)Instructions burned: 392 (million)
% 22.30/3.64 % (1651505)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2168941910:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2967 on theBenchmark for (2967ds/314Mi)
% 22.30/3.64 % (1651421) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1651082-1651421"...
% 22.30/3.64 % (1651421)...printing done.
% 22.30/3.64 % (1651421)Refutation found. Thanks to Tanya!
% 22.30/3.64 % SZS status Theorem for theBenchmark
% 22.30/3.64 % SZS output start Proof for theBenchmark
% 22.30/3.64 thf(type_def_5, type, coinductive_llist: $tType > $tType).
% 22.30/3.64 thf(type_def_6, type, set: $tType > $tType).
% 22.30/3.64 thf(type_def_7, type, nat: $tType).
% 22.30/3.64 thf(type_def_8, type, itself: $tType > $tType).
% 22.30/3.64 thf(type_def_9, type, a: $tType).
% 22.30/3.64 thf(type_def_10, type, sTfun: ($tType * $tType) > $tType).
% 22.30/3.64 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_1, type, ord: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_2, type, top: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_3, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_4, type, no_bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_5, type, no_top: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_6, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_7, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_8, type, order_top: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_9, type, wellorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_10, type, dense_order: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_11, type, dense_linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_12, type, condit1656338222tinuum: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_13, type, condit1037483654norder: !>[X0: $tType]:((itself @ X0 > $o))).
% 22.30/3.64 thf(func_def_14, type, coindu328551480prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 22.30/3.64 thf(func_def_15, type, coinductive_lappend: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_16, type, coinductive_LCons: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_17, type, coinductive_LNil: !>[X0: $tType]:(coinductive_llist @ X0)).
% 22.30/3.64 thf(func_def_18, type, coindu1478340336prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 22.30/3.64 thf(func_def_19, type, lList21511617539llstsp: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > $o))).
% 22.30/3.64 thf(func_def_20, type, lList2236698231inlsts: !>[X0: $tType]:((set @ X0 > set @ coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_21, type, lList21916056377ts_rec: !>[X0: $tType, X1: $tType]:((X0 > (X1 > coinductive_llist @ X1 > X0 > X0) > coinductive_llist @ X1 > X0))).
% 22.30/3.64 thf(func_def_22, type, lList2860480441nlstsp: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > $o))).
% 22.30/3.64 thf(func_def_23, type, lList22096119349pslsts: !>[X0: $tType]:((set @ X0 > set @ coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_24, type, lList2370560421utlast: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_25, type, lList2508575361_ldrop: !>[X0: $tType]:((coinductive_llist @ X0 > nat > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_26, type, lList2170638824_llast: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 22.30/3.64 thf(func_def_27, type, lList21232602520length: !>[X0: $tType]:((coinductive_llist @ X0 > nat))).
% 22.30/3.64 thf(func_def_28, type, lList2281150353e_lrev: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_29, type, lList22119844313_ltake: !>[X0: $tType]:((coinductive_llist @ X0 > nat > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_30, type, lList21148268032oslsts: !>[X0: $tType]:((set @ X0 > set @ coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_31, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 22.30/3.64 thf(func_def_32, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 22.30/3.64 thf(func_def_33, type, ordering_top: !>[X0: $tType]:(((X0 > X0 > $o) > (X0 > X0 > $o) > X0 > $o))).
% 22.30/3.64 thf(func_def_34, type, top_top: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_35, type, type2: !>[X0: $tType]:(itself @ X0)).
% 22.30/3.64 thf(func_def_36, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 22.30/3.64 thf(func_def_37, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 22.30/3.64 thf(func_def_38, type, a2: a).
% 22.30/3.64 thf(func_def_39, type, l: coinductive_llist @ a).
% 22.30/3.64 thf(func_def_43, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 22.30/3.64 thf(func_def_44, type, db1: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_45, type, db0: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_46, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 22.30/3.64 thf(func_def_47, type, vAND: ($o > $o > $o)).
% 22.30/3.64 thf(func_def_48, type, vNOT: ($o > $o)).
% 22.30/3.64 thf(func_def_49, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 22.30/3.64 thf(func_def_50, type, vIMP: ($o > $o > $o)).
% 22.30/3.64 thf(func_def_51, type, db2: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_52, type, vOR: ($o > $o > $o)).
% 22.30/3.64 thf(func_def_53, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 22.30/3.64 thf(func_def_54, type, db3: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_55, type, sP0: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 22.30/3.64 thf(func_def_56, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 22.30/3.64 thf(func_def_57, type, sK2: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_58, type, sK3: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_59, type, sK4: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_60, type, sK5: !>[X0: $tType]:((X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_61, type, sK6: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_62, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_63, type, sK8: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_64, type, sK9: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_65, type, sK10: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_66, type, sK11: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_67, type, sK12: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > X0))).
% 22.30/3.64 thf(func_def_68, type, sK13: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_69, type, sK14: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_70, type, sK15: !>[X0: $tType]:((X0 > X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_71, type, sK16: !>[X0: $tType]:((set @ X0 > coinductive_llist @ X0 > X0))).
% 22.30/3.64 thf(func_def_72, type, sK17: !>[X0: $tType]:((set @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_73, type, sK18: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_74, type, sK19: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_75, type, sK20: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_76, type, sK21: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_77, type, sK22: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_78, type, sK23: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_79, type, sK24: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_80, type, sK25: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_81, type, sK26: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_82, type, sK27: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_83, type, sK28: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_84, type, sK29: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_85, type, sK30: !>[X0: $tType]:((set @ X0 > X0))).
% 22.30/3.64 thf(func_def_86, type, sK31: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_87, type, sK32: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_88, type, sK33: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_89, type, sK34: !>[X0: $tType, X1: $tType]:((X1 > X0))).
% 22.30/3.64 thf(func_def_90, type, sK35: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_91, type, sK36: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > (X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_92, type, sK37: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_93, type, sK38: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > set @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_94, type, sK39: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_95, type, sK40: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_96, type, sK41: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_97, type, sK42: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_98, type, sK43: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_99, type, sK44: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > set @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_100, type, sK45: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_101, type, sK46: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_102, type, sK47: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_103, type, sK48: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_104, type, sK49: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_105, type, sK50: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_106, type, sK51: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_107, type, sK52: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_108, type, sK53: !>[X0: $tType]:((set @ X0 > (coinductive_llist @ X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_109, type, sK54: !>[X0: $tType]:((set @ X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_110, type, sK55: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_111, type, sK56: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_112, type, sK57: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_113, type, sK58: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_114, type, sK59: !>[X0: $tType]:((X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_115, type, sK60: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_116, type, sK61: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_117, type, sK62: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_118, type, sK63: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_119, type, sK64: !>[X0: $tType]:((X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_120, type, sK65: !>[X0: $tType]:((X0 > X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_121, type, sK66: !>[X0: $tType]:((set @ X0 > (coinductive_llist @ X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_122, type, sK67: !>[X0: $tType]:((set @ X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_123, type, sK68: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_124, type, sK69: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_125, type, sK70: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_126, type, sK71: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_127, type, sK72: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_128, type, sK73: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_129, type, sK74: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_130, type, sK75: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_131, type, sK76: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_132, type, sK77: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_133, type, sK78: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_134, type, sK79: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_135, type, sK80: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 22.30/3.64 thf(func_def_136, type, sK81: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_137, type, sK82: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_138, type, sK83: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_139, type, sK84: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_140, type, sK85: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_141, type, sK86: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_142, type, sK87: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_143, type, sK88: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_144, type, sK89: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_145, type, sK90: !>[X0: $tType]:(((X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_146, type, sK91: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_147, type, sK92: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 22.30/3.64 thf(func_def_148, type, sK93: !>[X0: $tType]:(X0)).
% 22.30/3.64 thf(func_def_149, type, sK94: !>[X0: $tType]:(((X0 > $o) > X0 > X0 > X0))).
% 22.30/3.64 thf(func_def_150, type, sK95: !>[X0: $tType]:((X0 > (X0 > $o) > X0 > X0))).
% 22.30/3.64 thf(func_def_151, type, sK96: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_152, type, sK97: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 22.30/3.64 thf(func_def_153, type, sK98: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_154, type, sK99: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_155, type, sK100: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 22.30/3.64 thf(func_def_156, type, sK101: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > (X0 > $o) > coinductive_llist @ X0))).
% 22.30/3.64 thf(func_def_157, type, sK102: !>[X0: $tType]:((X0 > X0))).
% 22.30/3.64 thf(func_def_158, type, sK103: !>[X0: $tType, X1: $tType]:((X0 > X1))).
% 22.30/3.64 thf(func_def_159, type, sK104: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_160, type, sK105: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_161, type, sK106: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_162, type, sK107: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 22.30/3.64 thf(func_def_163, type, sK108: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 22.30/3.64 thf(func_def_165, type, sK110: (coinductive_llist @ a > coinductive_llist @ a > coinductive_llist @ a)).
% 22.30/3.64 thf(f4,axiom,(
% 22.30/3.64 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : X0] : (coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X1 @ X2)))),
% 22.30/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_llist_Odistinct_I1_J)).
% 22.30/3.64 thf(f7,axiom,(
% 22.30/3.64 ((^[X0 : coinductive_llist @ a, X1 : coinductive_llist @ a] : (? [X2 : coinductive_llist @ a] : (X1 = ((coinductive_lappend @ a @ X0 @ X2))))) = ord_less_eq @ coinductive_llist @ a)),
% 22.30/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_llist__le__def)).
% 22.30/3.64 thf(f16,axiom,(
% 22.30/3.64 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0] : ((X1 = coinductive_LNil @ X0) & (X2 = coinductive_LNil @ X0) = (coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))))),
% 22.30/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_LNil__eq__lappend__iff)).
% 22.30/3.64 thf(f280,conjecture,(
% 22.30/3.64 ~(ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)),
% 22.30/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 22.30/3.64 thf(f281,negated_conjecture,(
% 22.30/3.64 ~ ~(ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)),
% 22.30/3.64 inference(negated_conjecture,[status(cth)],[f280])).
% 22.30/3.64 thf(f300,plain,(
% 22.30/3.64 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)) <=> (coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))))),
% 22.30/3.64 inference(fool_elimination,[],[f16])).
% 22.30/3.64 thf(f557,plain,(
% 22.30/3.64 (ord_less_eq @ coinductive_llist @ a = (^[Y0 : coinductive_llist @ a]: ((^[Y1 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y2 : coinductive_llist @ a]: ((coinductive_lappend @ a @ Y0 @ Y2) = Y1)))))))),
% 22.30/3.64 inference(fool_elimination,[],[f7])).
% 22.30/3.64 thf(f722,plain,(
% 22.30/3.64 ~ ~(ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)),
% 22.30/3.64 inference(rectify,[],[f281])).
% 22.30/3.64 thf(f723,plain,(
% 22.30/3.64 ~ ~ (((ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)) = $true)),
% 22.30/3.64 inference(fool_elimination,[],[f722])).
% 22.30/3.64 thf(f831,plain,(
% 22.30/3.64 (((ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)) = $true)),
% 22.30/3.64 inference(flattening,[],[f723])).
% 22.30/3.64 thf(f1194,plain,(
% 22.30/3.64 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X1 @ X2)))) & ((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))) | ((coinductive_LNil @ X0 != X1) | (coinductive_LNil @ X0 != X2))))),
% 22.30/3.64 inference(nnf_transformation,[],[f300])).
% 22.30/3.64 thf(f1195,plain,(
% 22.30/3.64 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X1 @ X2)))) & ((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))) | (coinductive_LNil @ X0 != X1) | (coinductive_LNil @ X0 != X2)))),
% 22.30/3.64 inference(flattening,[],[f1194])).
% 22.30/3.64 thf(f1196,plain,(
% 22.30/3.64 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0] : ((((coinductive_LNil @ X0 = X2) & (coinductive_LNil @ X0 = X1)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X2 @ X1)))) & ((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X2 @ X1))) | (coinductive_LNil @ X0 != X2) | (coinductive_LNil @ X0 != X1)))),
% 22.30/3.64 inference(rectify,[],[f1195])).
% 22.30/3.64 thf(f1361,plain,(
% 22.30/3.64 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : X0] : (coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X2 @ X1)))),
% 22.30/3.64 inference(rectify,[],[f4])).
% 22.30/3.64 thf(f1526,plain,(
% 22.30/3.64 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X2 @ X1))) | (coinductive_LNil @ X0 = X2)) )),
% 22.30/3.64 inference(cnf_transformation,[],[f1196])).
% 22.30/3.64 thf(f1792,plain,(
% 22.30/3.64 (((ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)) = $true)),
% 22.30/3.64 inference(cnf_transformation,[],[f831])).
% 22.30/3.64 thf(f1826,plain,(
% 22.30/3.64 ( ! [X0 : $tType,X2 : X0,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X2 @ X1)))) )),
% 22.30/3.64 inference(cnf_transformation,[],[f1361])).
% 22.30/3.64 thf(f1856,plain,(
% 22.30/3.64 (ord_less_eq @ coinductive_llist @ a = (^[Y0 : coinductive_llist @ a]: ((^[Y1 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y2 : coinductive_llist @ a]: ((coinductive_lappend @ a @ Y0 @ Y2) = Y1)))))))),
% 22.30/3.64 inference(cnf_transformation,[],[f557])).
% 22.30/3.64 thf(f2115,definition,(
% 22.30/3.64 spl109_4 <=> (ord_less_eq @ coinductive_llist @ a = (^[Y0 : coinductive_llist @ a]: ((^[Y1 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y2 : coinductive_llist @ a]: ((coinductive_lappend @ a @ Y0 @ Y2) = Y1)))))))),
% 22.30/3.64 introduced(definition,[new_symbols(definition,[spl109_4])],[avatar_definition])).
% 22.30/3.64 thf(f2117,plain,(
% 22.30/3.64 (ord_less_eq @ coinductive_llist @ a = (^[Y0 : coinductive_llist @ a]: ((^[Y1 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y2 : coinductive_llist @ a]: ((coinductive_lappend @ a @ Y0 @ Y2) = Y1))))))) | ~spl109_4),
% 22.30/3.64 inference(avatar_component_clause,[],[f2115])).
% 22.30/3.64 thf(f2118,plain,(
% 22.30/3.64 spl109_4),
% 22.30/3.64 inference(avatar_split_clause,[],[f1856,f2115])).
% 22.30/3.64 thf(f2175,definition,(
% 22.30/3.64 spl109_16 <=> (((ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)) = $true)),
% 22.30/3.64 introduced(definition,[new_symbols(definition,[spl109_16])],[avatar_definition])).
% 22.30/3.64 thf(f2177,plain,(
% 22.30/3.64 (((ord_less_eq @ coinductive_llist @ a @ (coinductive_LCons @ a @ a2 @ l) @ coinductive_LNil @ a)) = $true) | ~spl109_16),
% 22.30/3.64 inference(avatar_component_clause,[],[f2175])).
% 22.30/3.64 thf(f2178,plain,(
% 22.30/3.64 spl109_16),
% 22.30/3.64 inference(avatar_split_clause,[],[f1792,f2175])).
% 22.30/3.64 thf(f3269,plain,(
% 22.30/3.64 ( ! [X1 : coinductive_llist @ a] : (((((^[Y0 : coinductive_llist @ a]: ((^[Y1 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y2 : coinductive_llist @ a]: ((coinductive_lappend @ a @ Y0 @ Y2) = Y1)))))) @ X1)) = ((ord_less_eq @ coinductive_llist @ a @ X1)))) ) | ~spl109_4),
% 22.30/3.64 inference(argument_congruence,[],[f2117])).
% 22.30/3.64 thf(f3270,plain,(
% 22.30/3.64 ( ! [X1 : coinductive_llist @ a] : ((((ord_less_eq @ coinductive_llist @ a @ X1)) = (^[Y0 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y1 : coinductive_llist @ a]: ((coinductive_lappend @ a @ X1 @ Y1) = Y0)))))) ) | ~spl109_4),
% 22.30/3.64 inference(beta-eta_normalization,[],[f3269])).
% 22.30/3.64 thf(f11142,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (((((^[Y0 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y1 : coinductive_llist @ a]: ((coinductive_lappend @ a @ X1 @ Y1) = Y0)))) @ X2)) = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(argument_congruence,[],[f3270])).
% 22.30/3.64 thf(f11143,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (($true = (((^[Y0 : coinductive_llist @ a]: (?? @ coinductive_llist @ a @ (^[Y1 : coinductive_llist @ a]: ((coinductive_lappend @ a @ X1 @ Y1) = Y0)))) @ X2))) | ($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(iff_proxy_clausification,[],[f11142])).
% 22.30/3.64 thf(f11149,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (($true = ((?? @ coinductive_llist @ a @ (^[Y0 : coinductive_llist @ a]: ((coinductive_lappend @ a @ X1 @ Y0) = X2))))) | ($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(beta-eta_normalization,[],[f11143])).
% 22.30/3.64 thf(f11150,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (($true = (((^[Y0 : coinductive_llist @ a]: ((coinductive_lappend @ a @ X1 @ Y0) = X2)) @ (sK110 @ X1 @ X2)))) | ($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(sigma_proxy_clausification,[],[f11149])).
% 22.30/3.64 thf(f11151,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2))) | ($true = (((coinductive_lappend @ a @ X1 @ (sK110 @ X1 @ X2)) = X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(beta-eta_normalization,[],[f11150])).
% 22.30/3.64 thf(f11152,plain,(
% 22.30/3.64 ( ! [X2 : coinductive_llist @ a,X1 : coinductive_llist @ a] : ((((coinductive_lappend @ a @ X1 @ (sK110 @ X1 @ X2))) = X2) | ($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X2)))) ) | ~spl109_4),
% 22.30/3.64 inference(equality_proxy_clausification,[],[f11151])).
% 22.30/3.64 thf(f11607,plain,(
% 22.30/3.64 ( ! [X0 : coinductive_llist @ a,X1 : coinductive_llist @ a] : (($false = ((ord_less_eq @ coinductive_llist @ a @ X1 @ X0))) | (coinductive_LNil @ a != X0) | (coinductive_LNil @ a = X1)) ) | ~spl109_4),
% 22.30/3.64 inference(superposition,[],[f1526,f11152])).
% 22.30/3.64 thf(f12664,plain,(
% 22.30/3.64 ($true = $false) | (coinductive_LNil @ a != coinductive_LNil @ a) | (((coinductive_LCons @ a @ a2 @ l)) = coinductive_LNil @ a) | (~spl109_4 | ~spl109_16)),
% 22.30/3.64 inference(superposition,[],[f11607,f2177])).
% 22.30/3.64 thf(f12715,plain,(
% 22.30/3.64 (((coinductive_LCons @ a @ a2 @ l)) = coinductive_LNil @ a) | (~spl109_4 | ~spl109_16)),
% 22.30/3.64 inference(trivial_inequality_removal,[],[f12664])).
% 22.30/3.64 thf(f12732,plain,(
% 22.30/3.64 $false | (~spl109_4 | ~spl109_16)),
% 22.30/3.64 inference(forward_subsumption_resolution,[],[f12715,f1826])).
% 22.30/3.64 thf(f12733,plain,(
% 22.30/3.64 ~spl109_4 | ~spl109_16),
% 22.30/3.64 inference(avatar_contradiction_clause,[],[f12732])).
% 22.30/3.64 cnf(s5, plain, spl109_4, inference(sat_conversion,[],[f2118])).
% 22.30/3.64 cnf(s19, plain, spl109_16, inference(sat_conversion,[],[f2178])).
% 22.30/3.64 cnf(s101, plain, ~spl109_4 | ~spl109_16, inference(sat_conversion,[],[f12733])).
% 22.30/3.64 cnf(s107, plain, ~spl109_4, inference(rat,[],[s101,s19])).
% 22.30/3.64 cnf(s118, plain, $false, inference(rat,[],[s5,s107])).
% 22.30/3.64 thf(f12734,plain,(
% 22.30/3.64 $false),
% 22.30/3.64 inference(avatar_sat_refutation,[],[s118])).
% 22.30/3.64 % SZS output end Proof for theBenchmark
% 22.30/3.64 % (1651421)------------------------------
% 22.30/3.64 % (1651421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.64 % (1651421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.64 % (1651421)CaDiCaL version: 2.1.3
% 22.30/3.64 % (1651421)Termination reason: Refutation
% 22.30/3.64 % (1651421)Time elapsed: 1.878 s
% 22.30/3.64 % (1651421)Peak memory usage: 20 MB
% 22.30/3.64 % (1651421)Instructions burned: 2099 (million)
% 22.30/3.64 % (1651082)Success in time 3.35 s
% 22.30/3.64 % Vampire exiting
%------------------------------------------------------------------------------