%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM174^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:46:23 AM UTC 2026
% Result : Theorem 20.04s 3.18s
% Output : Refutation 20.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM174^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n009.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % 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 17:48:30 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.21/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.59/0.42 % (131965)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.59/0.42 % (131975)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1393057917:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.59/0.42 % (131976)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.59/0.42 % (131976)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.59/0.42 % (131972)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4046993263:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.59/0.42 % (131971)lrs+10_16_si=on:nwc=1.5:random_seed=2669473690:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.59/0.42 % (131970)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4223357531:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.59/0.42 % (131974)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3719912846:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.59/0.42 % (131973)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=3605940970: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.59/0.42 % (131976)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=2456145147:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.59/0.42 % (131972)Instruction limit reached!
% 0.59/0.42 % (131972)------------------------------
% 0.59/0.42 % (131972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.42 % (131972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.42 % (131972)CaDiCaL version: 2.1.3
% 0.59/0.42 % (131972)Termination reason: Instruction limit
% 0.59/0.42 % (131972)Termination phase: shuffling
% 0.59/0.42 % (131972)Time elapsed: 0.002 s
% 0.59/0.42 % (131972)Peak memory usage: 10 MB
% 0.59/0.42 % (131972)Instructions burned: 4 (million)
% 0.59/0.42 % (131971)Instruction limit reached!
% 0.59/0.42 % (131971)------------------------------
% 0.59/0.42 % (131971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.42 % (131971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.42 % (131971)CaDiCaL version: 2.1.3
% 0.59/0.42 % (131971)Termination reason: Instruction limit
% 0.59/0.42 % (131971)Termination phase: Property scanning
% 0.59/0.42 % (131971)Time elapsed: 0.009 s
% 0.59/0.42 % (131971)Peak memory usage: 10 MB
% 0.59/0.42 % (131971)Instructions burned: 19 (million)
% 0.59/0.42 % (131975)Instruction limit reached!
% 0.59/0.42 % (131975)------------------------------
% 0.59/0.42 % (131975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.42 % (131975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.42 % (131975)CaDiCaL version: 2.1.3
% 0.59/0.42 % (131975)Termination reason: Instruction limit
% 0.59/0.42 % (131975)Termination phase: Property scanning
% 0.59/0.42 % (131975)Time elapsed: 0.019 s
% 0.59/0.42 % (131975)Peak memory usage: 12 MB
% 0.59/0.42 % (131975)Instructions burned: 76 (million)
% 0.59/0.42 % (131974)Instruction limit reached!
% 0.59/0.42 % (131974)------------------------------
% 0.59/0.42 % (131974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.42 % (131974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.42 % (131974)CaDiCaL version: 2.1.3
% 0.59/0.42 % (131974)Termination reason: Instruction limit
% 0.59/0.42 % (131974)Termination phase: Preprocessing 1
% 0.59/0.42 % (131974)Time elapsed: 0.012 s
% 0.59/0.42 % (131974)Peak memory usage: 10 MB
% 0.59/0.42 % (131974)Instructions burned: 26 (million)
% 0.59/0.42 % (131986)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.59/0.42 % (131984)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4177350821:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.59/0.42 % (131986)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2324608563:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.59/0.45 % (131984)Instruction limit reached!
% 0.59/0.45 % (131984)------------------------------
% 0.59/0.45 % (131984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.45 % (131984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.45 % (131984)CaDiCaL version: 2.1.3
% 0.59/0.45 % (131984)Termination reason: Instruction limit
% 0.59/0.45 % (131984)Termination phase: shuffling
% 0.59/0.45 % (131984)Time elapsed: 0.002 s
% 0.59/0.45 % (131984)Peak memory usage: 10 MB
% 0.59/0.45 % (131984)Instructions burned: 4 (million)
% 0.59/0.45 % (131986)Instruction limit reached!
% 0.59/0.45 % (131986)------------------------------
% 0.59/0.45 % (131986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.45 % (131986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.45 % (131986)CaDiCaL version: 2.1.3
% 0.59/0.45 % (131986)Termination reason: Instruction limit
% 0.59/0.45 % (131986)Termination phase: shuffling
% 0.59/0.45 % (131986)Time elapsed: 0.002 s
% 0.59/0.45 % (131986)Peak memory usage: 10 MB
% 0.59/0.45 % (131986)Instructions burned: 9 (million)
% 0.59/0.45 % (131985)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1825851193:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.59/0.45 % (131985)Instruction limit reached!
% 0.59/0.45 % (131985)------------------------------
% 0.59/0.45 % (131985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.45 % (131985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.45 % (131985)CaDiCaL version: 2.1.3
% 0.59/0.45 % (131985)Termination reason: Instruction limit
% 0.59/0.45 % (131985)Termination phase: shuffling
% 0.59/0.45 % (131985)Time elapsed: 0.003 s
% 0.59/0.45 % (131985)Peak memory usage: 10 MB
% 0.59/0.45 % (131985)Instructions burned: 5 (million)
% 0.59/0.45 % (131987)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1304237801:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.59/0.45 % (131991)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=2373059388:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.59/0.45 % (131987)Instruction limit reached!
% 0.59/0.45 % (131987)------------------------------
% 0.59/0.45 % (131987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.45 % (131987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.45 % (131987)CaDiCaL version: 2.1.3
% 0.59/0.45 % (131990)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.59/0.45 % (131987)Termination reason: Instruction limit
% 0.59/0.45 % (131987)Termination phase: shuffling
% 0.59/0.45 % (131987)Time elapsed: 0.007 s
% 0.59/0.45 % (131987)Peak memory usage: 10 MB
% 0.59/0.45 % (131987)Instructions burned: 13 (million)
% 0.59/0.45 % (131990)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.59/0.45 % (131990)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2396646876: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.59/0.45 % (131994)lrs+10_1_si=on:cs=on:random_seed=3035901231:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.59/0.45 % (131994)Instruction limit reached!
% 0.59/0.45 % (131994)------------------------------
% 0.59/0.45 % (131994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.45 % (131994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.45 % (131994)CaDiCaL version: 2.1.3
% 0.59/0.45 % (131994)Termination reason: Instruction limit
% 0.59/0.45 % (131994)Termination phase: shuffling
% 0.59/0.45 % (131994)Time elapsed: 0.004 s
% 0.59/0.45 % (131994)Peak memory usage: 10 MB
% 0.59/0.45 % (131994)Instructions burned: 8 (million)
% 0.59/0.45 % (131996)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.30/0.48 % (131990)Instruction limit reached!
% 1.30/0.48 % (131990)------------------------------
% 1.30/0.48 % (131990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (131990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (131990)CaDiCaL version: 2.1.3
% 1.30/0.48 % (131990)Termination reason: Instruction limit
% 1.30/0.48 % (131990)Termination phase: shuffling
% 1.30/0.48 % (131990)Time elapsed: 0.013 s
% 1.30/0.48 % (131990)Peak memory usage: 10 MB
% 1.30/0.48 % (131990)Instructions burned: 28 (million)
% 1.30/0.48 % (131991)Instruction limit reached!
% 1.30/0.48 % (131991)------------------------------
% 1.30/0.48 % (131991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (131991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (131991)CaDiCaL version: 2.1.3
% 1.30/0.48 % (131991)Termination reason: Instruction limit
% 1.30/0.48 % (131991)Termination phase: Preprocessing 3
% 1.30/0.48 % (131991)Time elapsed: 0.021 s
% 1.30/0.48 % (131991)Peak memory usage: 11 MB
% 1.30/0.48 % (131991)Instructions burned: 91 (million)
% 1.30/0.48 % (131996)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=1767539656:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.30/0.48 % (131996)Instruction limit reached!
% 1.30/0.48 % (131996)------------------------------
% 1.30/0.48 % (131996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (131996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (131996)CaDiCaL version: 2.1.3
% 1.30/0.48 % (131996)Termination reason: Instruction limit
% 1.30/0.48 % (131996)Termination phase: shuffling
% 1.30/0.48 % (131996)Time elapsed: 0.002 s
% 1.30/0.48 % (131996)Peak memory usage: 10 MB
% 1.30/0.48 % (131996)Instructions burned: 3 (million)
% 1.30/0.48 % (132001)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3772447364:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 1.30/0.48 % (131999)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2294362583:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.30/0.48 % (132001)Instruction limit reached!
% 1.30/0.48 % (132001)------------------------------
% 1.30/0.48 % (132001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (132001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (132001)CaDiCaL version: 2.1.3
% 1.30/0.48 % (132001)Termination reason: Instruction limit
% 1.30/0.48 % (132001)Termination phase: SInE selection
% 1.30/0.48 % (132001)Time elapsed: 0.006 s
% 1.30/0.48 % (132001)Peak memory usage: 11 MB
% 1.30/0.48 % (132001)Instructions burned: 26 (million)
% 1.30/0.48 % (132000)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1079022252:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.30/0.48 % (131976)Instruction limit reached!
% 1.30/0.48 % (131976)------------------------------
% 1.30/0.48 % (131976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (131976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (131976)CaDiCaL version: 2.1.3
% 1.30/0.48 % (131976)Termination reason: Instruction limit
% 1.30/0.48 % (131976)Termination phase: Saturation
% 1.30/0.48 % (131976)Time elapsed: 0.077 s
% 1.30/0.48 % (131976)Peak memory usage: 14 MB
% 1.30/0.48 % (131976)Instructions burned: 157 (million)
% 1.30/0.48 % (131970)Instruction limit reached!
% 1.30/0.48 % (131970)------------------------------
% 1.30/0.48 % (131970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.48 % (131970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.48 % (131970)CaDiCaL version: 2.1.3
% 1.30/0.48 % (131970)Termination reason: Instruction limit
% 1.30/0.48 % (131970)Termination phase: Property scanning
% 1.30/0.48 % (131970)Time elapsed: 0.080 s
% 1.30/0.48 % (131970)Peak memory usage: 12 MB
% 1.30/0.48 % (131970)Instructions burned: 92 (million)
% 1.30/0.48 % (132003)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4199706973:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.48 % (132003)Instruction limit reached!
% 1.30/0.48 % (132003)------------------------------
% 1.30/0.55 % (132003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.55 % (132003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.55 % (132003)CaDiCaL version: 2.1.3
% 1.30/0.55 % (132003)Termination reason: Instruction limit
% 1.30/0.55 % (132003)Termination phase: shuffling
% 1.30/0.55 % (132003)Time elapsed: 0.007 s
% 1.30/0.55 % (132003)Peak memory usage: 10 MB
% 1.30/0.55 % (132003)Instructions burned: 15 (million)
% 1.30/0.55 % (132010)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2031756634: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.30/0.55 % (132010)Instruction limit reached!
% 1.30/0.55 % (132010)------------------------------
% 1.30/0.55 % (132010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.55 % (132010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.55 % (132010)CaDiCaL version: 2.1.3
% 1.30/0.55 % (132010)Termination reason: Instruction limit
% 1.30/0.55 % (132010)Termination phase: shuffling
% 1.30/0.55 % (132010)Time elapsed: 0.001 s
% 1.30/0.55 % (132010)Peak memory usage: 10 MB
% 1.30/0.55 % (132010)Instructions burned: 4 (million)
% 1.30/0.55 % (131999)Instruction limit reached!
% 1.30/0.55 % (131999)------------------------------
% 1.30/0.55 % (131999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.55 % (131999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.55 % (131999)CaDiCaL version: 2.1.3
% 1.30/0.55 % (131999)Termination reason: Instruction limit
% 1.30/0.55 % (131999)Termination phase: Preprocessing 3
% 1.30/0.55 % (131999)Time elapsed: 0.018 s
% 1.30/0.55 % (131999)Peak memory usage: 11 MB
% 1.30/0.55 % (131999)Instructions burned: 38 (million)
% 1.30/0.55 % (132007)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1416341036:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.30/0.55 % (132008)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4239147320:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.30/0.55 % (132013)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3157130271:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.30/0.55 % (132008)Instruction limit reached!
% 1.30/0.55 % (132008)------------------------------
% 1.30/0.55 % (132008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.55 % (132008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.55 % (132008)CaDiCaL version: 2.1.3
% 1.30/0.55 % (132008)Termination reason: Instruction limit
% 1.30/0.55 % (132008)Termination phase: shuffling
% 1.30/0.55 % (132008)Time elapsed: 0.007 s
% 1.30/0.55 % (132008)Peak memory usage: 10 MB
% 1.30/0.55 % (132008)Instructions burned: 15 (million)
% 1.30/0.55 % (132011)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=782081840:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.30/0.55 % (132013)Instruction limit reached!
% 1.30/0.55 % (132013)------------------------------
% 1.30/0.55 % (132013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.55 % (132013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.55 % (132013)CaDiCaL version: 2.1.3
% 1.30/0.55 % (132013)Termination reason: Instruction limit
% 1.30/0.55 % (132013)Termination phase: Property scanning
% 1.30/0.55 % (132013)Time elapsed: 0.005 s
% 1.30/0.55 % (132013)Peak memory usage: 10 MB
% 1.30/0.55 % (132013)Instructions burned: 24 (million)
% 1.30/0.55 % (132015)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1194157284:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.30/0.55 % (132020)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.30/0.55 % (132020)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=3741587724:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.30/0.55 % (132018)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.96/0.62 % (132018)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.96/0.62 % (132011)Instruction limit reached!
% 1.96/0.62 % (132011)------------------------------
% 1.96/0.62 % (132011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132011)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132011)Termination reason: Instruction limit
% 1.96/0.62 % (132011)Termination phase: shuffling
% 1.96/0.62 % (132011)Time elapsed: 0.013 s
% 1.96/0.62 % (132011)Peak memory usage: 10 MB
% 1.96/0.62 % (132011)Instructions burned: 28 (million)
% 1.96/0.62 % (132020)Instruction limit reached!
% 1.96/0.62 % (132020)------------------------------
% 1.96/0.62 % (132020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132020)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132020)Termination reason: Instruction limit
% 1.96/0.62 % (132020)Termination phase: shuffling
% 1.96/0.62 % (132020)Time elapsed: 0.003 s
% 1.96/0.62 % (132020)Peak memory usage: 10 MB
% 1.96/0.62 % (132020)Instructions burned: 12 (million)
% 1.96/0.62 % (132018)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=992018866:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.96/0.62 % (132018)Instruction limit reached!
% 1.96/0.62 % (132018)------------------------------
% 1.96/0.62 % (132018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132018)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132018)Termination reason: Instruction limit
% 1.96/0.62 % (132018)Termination phase: shuffling
% 1.96/0.62 % (132018)Time elapsed: 0.007 s
% 1.96/0.62 % (132018)Peak memory usage: 10 MB
% 1.96/0.62 % (132018)Instructions burned: 14 (million)
% 1.96/0.62 % (132024)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3370310362:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.96/0.62 % (132024)Instruction limit reached!
% 1.96/0.62 % (132024)------------------------------
% 1.96/0.62 % (132024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132024)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132024)Termination reason: Instruction limit
% 1.96/0.62 % (132024)Termination phase: shuffling
% 1.96/0.62 % (132024)Time elapsed: 0.002 s
% 1.96/0.62 % (132024)Peak memory usage: 10 MB
% 1.96/0.62 % (132024)Instructions burned: 9 (million)
% 1.96/0.62 % (132023)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=60751062:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.96/0.62 % (132015)Instruction limit reached!
% 1.96/0.62 % (132015)------------------------------
% 1.96/0.62 % (132015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132015)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132015)Termination reason: Instruction limit
% 1.96/0.62 % (132015)Termination phase: Property scanning
% 1.96/0.62 % (132015)Time elapsed: 0.028 s
% 1.96/0.62 % (132015)Peak memory usage: 11 MB
% 1.96/0.62 % (132015)Instructions burned: 61 (million)
% 1.96/0.62 % (132028)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2552047328:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.96/0.62 % (132026)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4266760913:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.96/0.62 % (132028)Instruction limit reached!
% 1.96/0.62 % (132028)------------------------------
% 1.96/0.62 % (132028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (132028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (132028)CaDiCaL version: 2.1.3
% 1.96/0.62 % (132028)Termination reason: Instruction limit
% 1.96/0.62 % (132028)Termination phase: Property scanning
% 2.64/0.71 % (132028)Time elapsed: 0.005 s
% 2.64/0.71 % (132028)Peak memory usage: 10 MB
% 2.64/0.71 % (132028)Instructions burned: 22 (million)
% 2.64/0.71 % (132023)Instruction limit reached!
% 2.64/0.71 % (132023)------------------------------
% 2.64/0.71 % (132023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.71 % (132023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.71 % (132023)CaDiCaL version: 2.1.3
% 2.64/0.71 % (132023)Termination reason: Instruction limit
% 2.64/0.71 % (132023)Termination phase: shuffling
% 2.64/0.71 % (132023)Time elapsed: 0.015 s
% 2.64/0.71 % (132023)Peak memory usage: 10 MB
% 2.64/0.71 % (132023)Instructions burned: 32 (million)
% 2.64/0.71 % (132030)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=270314693:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.64/0.71 % (132026)Instruction limit reached!
% 2.64/0.71 % (132026)------------------------------
% 2.64/0.71 % (132026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.71 % (132026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.71 % (132026)CaDiCaL version: 2.1.3
% 2.64/0.71 % (132026)Termination reason: Instruction limit
% 2.64/0.71 % (132026)Termination phase: shuffling
% 2.64/0.71 % (132026)Time elapsed: 0.011 s
% 2.64/0.71 % (132026)Peak memory usage: 10 MB
% 2.64/0.71 % (132026)Instructions burned: 23 (million)
% 2.64/0.71 % (132033)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=753746398:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.64/0.71 % (132036)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=357089190:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.64/0.71 % (132034)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=780447282:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.64/0.71 % (132036)Instruction limit reached!
% 2.64/0.71 % (132036)------------------------------
% 2.64/0.71 % (132036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.71 % (132036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.71 % (132036)CaDiCaL version: 2.1.3
% 2.64/0.71 % (132036)Termination reason: Instruction limit
% 2.64/0.71 % (132036)Termination phase: Preprocessing 3
% 2.64/0.71 % (132036)Time elapsed: 0.011 s
% 2.64/0.71 % (132036)Peak memory usage: 11 MB
% 2.64/0.71 % (132036)Instructions burned: 43 (million)
% 2.64/0.71 % (132040)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.64/0.71 % (132040)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3859159252:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.64/0.71 % (132040)Instruction limit reached!
% 2.64/0.71 % (132040)------------------------------
% 2.64/0.71 % (132040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.71 % (132040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.71 % (132040)CaDiCaL version: 2.1.3
% 2.64/0.71 % (132040)Termination reason: Instruction limit
% 2.64/0.71 % (132040)Termination phase: shuffling
% 2.64/0.71 % (132040)Time elapsed: 0.002 s
% 2.64/0.71 % (132040)Peak memory usage: 10 MB
% 2.64/0.71 % (132040)Instructions burned: 8 (million)
% 2.64/0.71 % (132000)Instruction limit reached!
% 2.64/0.71 % (132000)------------------------------
% 2.64/0.71 % (132000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.71 % (132000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.71 % (132000)CaDiCaL version: 2.1.3
% 2.64/0.71 % (132000)Termination reason: Instruction limit
% 2.64/0.71 % (132000)Termination phase: Saturation
% 2.64/0.71 % (132000)Time elapsed: 0.130 s
% 2.64/0.71 % (132000)Peak memory usage: 14 MB
% 2.64/0.71 % (132000)Instructions burned: 249 (million)
% 2.64/0.71 % (132042)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2274257143:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.64/0.71 % (132044)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=244839550: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.64/0.78 % (132033)Instruction limit reached!
% 2.64/0.78 % (132033)------------------------------
% 2.64/0.78 % (132033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132033)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132033)Termination reason: Instruction limit
% 2.64/0.78 % (132033)Termination phase: Saturation
% 2.64/0.78 % (132033)Time elapsed: 0.085 s
% 2.64/0.78 % (132033)Peak memory usage: 14 MB
% 2.64/0.78 % (132033)Instructions burned: 145 (million)
% 2.64/0.78 % (132042)Instruction limit reached!
% 2.64/0.78 % (132042)------------------------------
% 2.64/0.78 % (132042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132042)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132042)Termination reason: Instruction limit
% 2.64/0.78 % (132042)Termination phase: Saturation
% 2.64/0.78 % (132042)Time elapsed: 0.052 s
% 2.64/0.78 % (132042)Peak memory usage: 14 MB
% 2.64/0.78 % (132042)Instructions burned: 184 (million)
% 2.64/0.78 % (132047)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=778869152:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.64/0.78 % (132046)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.64/0.78 % (132047)Instruction limit reached!
% 2.64/0.78 % (132047)------------------------------
% 2.64/0.78 % (132047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132047)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132047)Termination reason: Instruction limit
% 2.64/0.78 % (132047)Termination phase: Property scanning
% 2.64/0.78 % (132047)Time elapsed: 0.006 s
% 2.64/0.78 % (132047)Peak memory usage: 10 MB
% 2.64/0.78 % (132047)Instructions burned: 27 (million)
% 2.64/0.78 % (132046)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1369150920: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.64/0.78 % (132034)Instruction limit reached!
% 2.64/0.78 % (132034)------------------------------
% 2.64/0.78 % (132034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132034)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132034)Termination reason: Instruction limit
% 2.64/0.78 % (132034)Termination phase: Saturation
% 2.64/0.78 % (132034)Time elapsed: 0.104 s
% 2.64/0.78 % (132034)Peak memory usage: 14 MB
% 2.64/0.78 % (132034)Instructions burned: 194 (million)
% 2.64/0.78 % (132046)Instruction limit reached!
% 2.64/0.78 % (132046)------------------------------
% 2.64/0.78 % (132046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132046)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132046)Termination reason: Instruction limit
% 2.64/0.78 % (132046)Termination phase: shuffling
% 2.64/0.78 % (132046)Time elapsed: 0.003 s
% 2.64/0.78 % (132046)Peak memory usage: 10 MB
% 2.64/0.78 % (132046)Instructions burned: 6 (million)
% 2.64/0.78 % (132049)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3626077908:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.64/0.78 % (132049)Instruction limit reached!
% 2.64/0.78 % (132049)------------------------------
% 2.64/0.78 % (132049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132049)CaDiCaL version: 2.1.3
% 2.64/0.78 % (132049)Termination reason: Instruction limit
% 2.64/0.78 % (132049)Termination phase: shuffling
% 2.64/0.78 % (132049)Time elapsed: 0.005 s
% 2.64/0.78 % (132049)Peak memory usage: 10 MB
% 2.64/0.78 % (132049)Instructions burned: 22 (million)
% 2.64/0.78 % (132044)Refutation not found, incomplete strategy
% 2.64/0.78 % (132044)------------------------------
% 2.64/0.78 % (132044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.64/0.78 % (132044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.78 % (132044)CaDiCaL version: 2.1.3
% 3.23/0.88 % (132044)Termination reason: Refutation not found, incomplete strategy
% 3.23/0.88 % (132044)Time elapsed: 0.070 s
% 3.23/0.88 % (132044)Peak memory usage: 14 MB
% 3.23/0.88 % (132044)Instructions burned: 138 (million)
% 3.23/0.88 % (132051)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=916427814:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.23/0.88 % (132044)------------------------------
% 3.23/0.88 % (132044)------------------------------
% 3.23/0.88 % (132052)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=660024403: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.23/0.88 % (132054)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=1941019396: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.23/0.88 % (132054)Instruction limit reached!
% 3.23/0.88 % (132054)------------------------------
% 3.23/0.88 % (132054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.23/0.88 % (132054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/0.88 % (132054)CaDiCaL version: 2.1.3
% 3.23/0.88 % (132054)Termination reason: Instruction limit
% 3.23/0.88 % (132054)Termination phase: SInE selection
% 3.23/0.88 % (132054)Time elapsed: 0.011 s
% 3.23/0.88 % (132054)Peak memory usage: 11 MB
% 3.23/0.88 % (132054)Instructions burned: 49 (million)
% 3.23/0.88 % (132056)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3608953282:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.23/0.88 % (132059)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=850424715: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.23/0.88 % (132059)Instruction limit reached!
% 3.23/0.88 % (132059)------------------------------
% 3.23/0.88 % (132059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.23/0.88 % (132059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/0.88 % (132059)CaDiCaL version: 2.1.3
% 3.23/0.88 % (132059)Termination reason: Instruction limit
% 3.23/0.88 % (132059)Termination phase: Property scanning
% 3.23/0.88 % (132059)Time elapsed: 0.005 s
% 3.23/0.88 % (132059)Peak memory usage: 10 MB
% 3.23/0.88 % (132059)Instructions burned: 21 (million)
% 3.23/0.88 % (132062)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.23/0.88 % (132062)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3593505642:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.23/0.88 % (131973)Instruction limit reached!
% 3.23/0.88 % (131973)------------------------------
% 3.23/0.88 % (131973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.23/0.88 % (131973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/0.88 % (131973)CaDiCaL version: 2.1.3
% 3.23/0.88 % (131973)Termination reason: Instruction limit
% 3.23/0.88 % (131973)Termination phase: Saturation
% 3.23/0.88 % (131973)Time elapsed: 0.357 s
% 3.23/0.88 % (131973)Peak memory usage: 16 MB
% 3.23/0.88 % (131973)Instructions burned: 634 (million)
% 3.23/0.88 % (132007)Instruction limit reached!
% 3.23/0.88 % (132007)------------------------------
% 3.23/0.88 % (132007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.23/0.88 % (132007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/0.88 % (132007)CaDiCaL version: 2.1.3
% 3.23/0.88 % (132007)Termination reason: Instruction limit
% 3.23/0.88 % (132007)Termination phase: Saturation
% 3.23/0.88 % (132007)Time elapsed: 0.269 s
% 3.23/0.88 % (132007)Peak memory usage: 14 MB
% 3.23/0.88 % (132007)Instructions burned: 327 (million)
% 3.23/0.88 % (132064)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2211215654:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.23/0.88 % (132065)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=2761890771:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 5.25/1.06 % (132064)Instruction limit reached!
% 5.25/1.06 % (132064)------------------------------
% 5.25/1.06 % (132064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132064)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132064)Termination reason: Instruction limit
% 5.25/1.06 % (132064)Termination phase: shuffling
% 5.25/1.06 % (132064)Time elapsed: 0.007 s
% 5.25/1.06 % (132064)Peak memory usage: 10 MB
% 5.25/1.06 % (132064)Instructions burned: 15 (million)
% 5.25/1.06 % (132062)Instruction limit reached!
% 5.25/1.06 % (132062)------------------------------
% 5.25/1.06 % (132062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132062)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132062)Termination reason: Instruction limit
% 5.25/1.06 % (132062)Termination phase: Saturation
% 5.25/1.06 % (132062)Time elapsed: 0.051 s
% 5.25/1.06 % (132062)Peak memory usage: 14 MB
% 5.25/1.06 % (132062)Instructions burned: 202 (million)
% 5.25/1.06 % (132069)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1063569574:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 5.25/1.06 % (132068)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1227873781:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 5.25/1.06 % (132069)Instruction limit reached!
% 5.25/1.06 % (132069)------------------------------
% 5.25/1.06 % (132069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132069)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132069)Termination reason: Instruction limit
% 5.25/1.06 % (132069)Termination phase: Property scanning
% 5.25/1.06 % (132069)Time elapsed: 0.008 s
% 5.25/1.06 % (132069)Peak memory usage: 10 MB
% 5.25/1.06 % (132069)Instructions burned: 35 (million)
% 5.25/1.06 % (132065)Instruction limit reached!
% 5.25/1.06 % (132065)------------------------------
% 5.25/1.06 % (132065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132065)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132065)Termination reason: Instruction limit
% 5.25/1.06 % (132065)Termination phase: SInE selection
% 5.25/1.06 % (132065)Time elapsed: 0.029 s
% 5.25/1.06 % (132065)Peak memory usage: 11 MB
% 5.25/1.06 % (132065)Instructions burned: 66 (million)
% 5.25/1.06 % (132072)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=357868770:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.25/1.06 % (132068)Instruction limit reached!
% 5.25/1.06 % (132068)------------------------------
% 5.25/1.06 % (132068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132068)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132068)Termination reason: Instruction limit
% 5.25/1.06 % (132068)Termination phase: Preprocessing 3
% 5.25/1.06 % (132068)Time elapsed: 0.024 s
% 5.25/1.06 % (132068)Peak memory usage: 11 MB
% 5.25/1.06 % (132068)Instructions burned: 51 (million)
% 5.25/1.06 % (132073)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=309644430:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 5.25/1.06 % (132073)Instruction limit reached!
% 5.25/1.06 % (132073)------------------------------
% 5.25/1.06 % (132073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.06 % (132073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.06 % (132073)CaDiCaL version: 2.1.3
% 5.25/1.06 % (132073)Termination reason: Instruction limit
% 5.25/1.06 % (132073)Termination phase: shuffling
% 5.25/1.06 % (132073)Time elapsed: 0.015 s
% 5.25/1.06 % (132073)Peak memory usage: 10 MB
% 5.25/1.06 % (132073)Instructions burned: 34 (million)
% 5.25/1.06 % (132075)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1458833866:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.88/1.20 % (132072)Instruction limit reached!
% 5.88/1.20 % (132072)------------------------------
% 5.88/1.20 % (132072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132072)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132072)Termination reason: Instruction limit
% 5.88/1.20 % (132072)Termination phase: Saturation
% 5.88/1.20 % (132072)Time elapsed: 0.035 s
% 5.88/1.20 % (132072)Peak memory usage: 14 MB
% 5.88/1.20 % (132072)Instructions burned: 138 (million)
% 5.88/1.20 % (132078)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.88/1.20 % (132078)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2079475224:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.88/1.20 % (132079)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3796831223:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.88/1.20 % (132051)Instruction limit reached!
% 5.88/1.20 % (132051)------------------------------
% 5.88/1.20 % (132051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132051)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132051)Termination reason: Instruction limit
% 5.88/1.20 % (132051)Termination phase: Saturation
% 5.88/1.20 % (132051)Time elapsed: 0.171 s
% 5.88/1.20 % (132051)Peak memory usage: 16 MB
% 5.88/1.20 % (132051)Instructions burned: 317 (million)
% 5.88/1.20 % (132075)Instruction limit reached!
% 5.88/1.20 % (132075)------------------------------
% 5.88/1.20 % (132075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132075)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132075)Termination reason: Instruction limit
% 5.88/1.20 % (132075)Termination phase: Property scanning
% 5.88/1.20 % (132075)Time elapsed: 0.031 s
% 5.88/1.20 % (132075)Peak memory usage: 11 MB
% 5.88/1.20 % (132075)Instructions burned: 68 (million)
% 5.88/1.20 % (132082)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3665856932:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.88/1.20 % (132083)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1891190646:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.88/1.20 % (132082)Instruction limit reached!
% 5.88/1.20 % (132082)------------------------------
% 5.88/1.20 % (132082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132082)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132082)Termination reason: Instruction limit
% 5.88/1.20 % (132082)Termination phase: Saturation
% 5.88/1.20 % (132082)Time elapsed: 0.047 s
% 5.88/1.20 % (132082)Peak memory usage: 13 MB
% 5.88/1.20 % (132082)Instructions burned: 96 (million)
% 5.88/1.20 % (132079)Instruction limit reached!
% 5.88/1.20 % (132079)------------------------------
% 5.88/1.20 % (132079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132079)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132079)Termination reason: Instruction limit
% 5.88/1.20 % (132079)Termination phase: Saturation
% 5.88/1.20 % (132079)Time elapsed: 0.068 s
% 5.88/1.20 % (132079)Peak memory usage: 14 MB
% 5.88/1.20 % (132079)Instructions burned: 246 (million)
% 5.88/1.20 % (132078)Instruction limit reached!
% 5.88/1.20 % (132078)------------------------------
% 5.88/1.20 % (132078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.20 % (132078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.20 % (132078)CaDiCaL version: 2.1.3
% 5.88/1.20 % (132078)Termination reason: Instruction limit
% 5.88/1.20 % (132078)Termination phase: Saturation
% 5.88/1.20 % (132078)Time elapsed: 0.077 s
% 5.88/1.20 % (132078)Peak memory usage: 13 MB
% 5.88/1.20 % (132078)Instructions burned: 180 (million)
% 5.88/1.20 % (132087)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3727474741:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.88/1.20 % (132056)Instruction limit reached!
% 5.88/1.20 % (132056)------------------------------
% 6.13/1.29 % (132056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132056)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132056)Termination reason: Instruction limit
% 6.13/1.29 % (132056)Termination phase: Saturation
% 6.13/1.29 % (132056)Time elapsed: 0.234 s
% 6.13/1.29 % (132056)Peak memory usage: 17 MB
% 6.13/1.29 % (132056)Instructions burned: 480 (million)
% 6.13/1.29 % (132088)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2243947555:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 6.13/1.29 % (132086)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=854492365:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 6.13/1.29 % (132090)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2485424221:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 6.13/1.29 % (132090)Instruction limit reached!
% 6.13/1.29 % (132090)------------------------------
% 6.13/1.29 % (132090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132090)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132090)Termination reason: Instruction limit
% 6.13/1.29 % (132090)Termination phase: Property scanning
% 6.13/1.29 % (132090)Time elapsed: 0.020 s
% 6.13/1.29 % (132090)Peak memory usage: 10 MB
% 6.13/1.29 % (132090)Instructions burned: 45 (million)
% 6.13/1.29 % (132094)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=723392397:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 6.13/1.29 % (132088)Instruction limit reached!
% 6.13/1.29 % (132088)------------------------------
% 6.13/1.29 % (132088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132088)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132088)Termination reason: Instruction limit
% 6.13/1.29 % (132088)Termination phase: Saturation
% 6.13/1.29 % (132088)Time elapsed: 0.057 s
% 6.13/1.29 % (132088)Peak memory usage: 13 MB
% 6.13/1.29 % (132088)Instructions burned: 130 (million)
% 6.13/1.29 % (132096)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=172737029:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 6.13/1.29 % (132087)Instruction limit reached!
% 6.13/1.29 % (132087)------------------------------
% 6.13/1.29 % (132087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132087)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132087)Termination reason: Instruction limit
% 6.13/1.29 % (132087)Termination phase: Saturation
% 6.13/1.29 % (132087)Time elapsed: 0.139 s
% 6.13/1.29 % (132087)Peak memory usage: 16 MB
% 6.13/1.29 % (132087)Instructions burned: 516 (million)
% 6.13/1.29 % (132098)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=599931771:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.13/1.29 % (132098)Instruction limit reached!
% 6.13/1.29 % (132098)------------------------------
% 6.13/1.29 % (132098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132098)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132098)Termination reason: Instruction limit
% 6.13/1.29 % (132098)Termination phase: Saturation
% 6.13/1.29 % (132098)Time elapsed: 0.023 s
% 6.13/1.29 % (132098)Peak memory usage: 13 MB
% 6.13/1.29 % (132098)Instructions burned: 96 (million)
% 6.13/1.29 % (132083)Instruction limit reached!
% 6.13/1.29 % (132083)------------------------------
% 6.13/1.29 % (132083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.13/1.29 % (132083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.13/1.29 % (132083)CaDiCaL version: 2.1.3
% 6.13/1.29 % (132083)Termination reason: Instruction limit
% 6.13/1.29 % (132083)Termination phase: Saturation
% 6.13/1.29 % (132083)Time elapsed: 0.227 s
% 6.13/1.29 % (132083)Peak memory usage: 14 MB
% 6.13/1.29 % (132083)Instructions burned: 429 (million)
% 6.13/1.29 % (132100)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=3301224360:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.90/1.42 % (132101)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=1259672676: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_2992 on theBenchmark for (2992ds/105Mi)
% 6.90/1.42 % (132100)Instruction limit reached!
% 6.90/1.42 % (132100)------------------------------
% 6.90/1.42 % (132100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.90/1.42 % (132100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.90/1.42 % (132100)CaDiCaL version: 2.1.3
% 6.90/1.42 % (132100)Termination reason: Instruction limit
% 6.90/1.42 % (132100)Termination phase: SInE selection
% 6.90/1.42 % (132100)Time elapsed: 0.015 s
% 6.90/1.42 % (132100)Peak memory usage: 11 MB
% 6.90/1.42 % (132100)Instructions burned: 65 (million)
% 6.90/1.42 % (132052)Instruction limit reached!
% 6.90/1.42 % (132052)------------------------------
% 6.90/1.42 % (132052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.90/1.42 % (132052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.90/1.42 % (132052)CaDiCaL version: 2.1.3
% 6.90/1.42 % (132052)Termination reason: Instruction limit
% 6.90/1.42 % (132052)Termination phase: Saturation
% 6.90/1.42 % (132052)Time elapsed: 0.457 s
% 6.90/1.42 % (132052)Peak memory usage: 17 MB
% 6.90/1.42 % (132052)Instructions burned: 854 (million)
% 6.90/1.42 % (132104)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=2830870150:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.90/1.42 % (132105)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=179024330:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.90/1.42 % (132101)Instruction limit reached!
% 6.90/1.42 % (132101)------------------------------
% 6.90/1.42 % (132101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.90/1.42 % (132101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.90/1.42 % (132101)CaDiCaL version: 2.1.3
% 6.90/1.42 % (132101)Termination reason: Instruction limit
% 6.90/1.42 % (132101)Termination phase: Property scanning
% 6.90/1.42 % (132101)Time elapsed: 0.047 s
% 6.90/1.42 % (132101)Peak memory usage: 11 MB
% 6.90/1.42 % (132101)Instructions burned: 107 (million)
% 6.90/1.42 % (132108)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2651545427:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 6.90/1.42 % (132030)Instruction limit reached!
% 6.90/1.42 % (132030)------------------------------
% 6.90/1.42 % (132030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.90/1.42 % (132030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.90/1.42 % (132030)CaDiCaL version: 2.1.3
% 6.90/1.42 % (132030)Termination reason: Instruction limit
% 6.90/1.42 % (132030)Termination phase: Saturation
% 6.90/1.42 % (132030)Time elapsed: 0.656 s
% 6.90/1.42 % (132030)Peak memory usage: 18 MB
% 6.90/1.42 % (132030)Instructions burned: 1240 (million)
% 6.90/1.42 % (132110)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=1436288576:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 6.90/1.42 % (132110)Instruction limit reached!
% 6.90/1.42 % (132110)------------------------------
% 6.90/1.42 % (132110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.90/1.42 % (132110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.90/1.42 % (132110)CaDiCaL version: 2.1.3
% 6.90/1.42 % (132110)Termination reason: Instruction limit
% 6.90/1.42 % (132110)Termination phase: Property scanning
% 6.90/1.42 % (132110)Time elapsed: 0.016 s
% 6.90/1.42 % (132110)Peak memory usage: 10 MB
% 6.90/1.42 % (132110)Instructions burned: 35 (million)
% 6.90/1.42 % (132096)Instruction limit reached!
% 6.90/1.42 % (132096)------------------------------
% 6.90/1.42 % (132096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132096)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132096)Termination reason: Instruction limit
% 7.65/1.58 % (132096)Termination phase: Saturation
% 7.65/1.58 % (132096)Time elapsed: 0.231 s
% 7.65/1.58 % (132096)Peak memory usage: 14 MB
% 7.65/1.58 % (132096)Instructions burned: 450 (million)
% 7.65/1.58 % (132112)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2073750378:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 7.65/1.58 % (132114)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=973454692:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2990 on theBenchmark for (2990ds/66Mi)
% 7.65/1.58 % (132094)Instruction limit reached!
% 7.65/1.58 % (132094)------------------------------
% 7.65/1.58 % (132094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132094)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132094)Termination reason: Instruction limit
% 7.65/1.58 % (132094)Termination phase: Saturation
% 7.65/1.58 % (132094)Time elapsed: 0.299 s
% 7.65/1.58 % (132094)Peak memory usage: 16 MB
% 7.65/1.58 % (132094)Instructions burned: 573 (million)
% 7.65/1.58 % (132112)Instruction limit reached!
% 7.65/1.58 % (132112)------------------------------
% 7.65/1.58 % (132112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132112)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132112)Termination reason: Instruction limit
% 7.65/1.58 % (132112)Termination phase: Property scanning
% 7.65/1.58 % (132112)Time elapsed: 0.043 s
% 7.65/1.58 % (132112)Peak memory usage: 12 MB
% 7.65/1.58 % (132112)Instructions burned: 93 (million)
% 7.65/1.58 % (132114)Instruction limit reached!
% 7.65/1.58 % (132114)------------------------------
% 7.65/1.58 % (132114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132114)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132114)Termination reason: Instruction limit
% 7.65/1.58 % (132114)Termination phase: Property scanning
% 7.65/1.58 % (132114)Time elapsed: 0.031 s
% 7.65/1.58 % (132114)Peak memory usage: 12 MB
% 7.65/1.58 % (132114)Instructions burned: 68 (million)
% 7.65/1.58 % (132116)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2798778663:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2990 on theBenchmark for (2990ds/22Mi)
% 7.65/1.58 % (132117)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=3846106228:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.65/1.58 % (132116)Instruction limit reached!
% 7.65/1.58 % (132116)------------------------------
% 7.65/1.58 % (132116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132116)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132116)Termination reason: Instruction limit
% 7.65/1.58 % (132116)Termination phase: Property scanning
% 7.65/1.58 % (132116)Time elapsed: 0.010 s
% 7.65/1.58 % (132116)Peak memory usage: 10 MB
% 7.65/1.58 % (132116)Instructions burned: 22 (million)
% 7.65/1.58 % (132118)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3168754037:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/28Mi)
% 7.65/1.58 % (132118)Instruction limit reached!
% 7.65/1.58 % (132118)------------------------------
% 7.65/1.58 % (132118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.58 % (132118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.58 % (132118)CaDiCaL version: 2.1.3
% 7.65/1.58 % (132118)Termination reason: Instruction limit
% 7.65/1.58 % (132118)Termination phase: Property scanning
% 7.65/1.58 % (132118)Time elapsed: 0.013 s
% 7.65/1.58 % (132118)Peak memory usage: 10 MB
% 7.65/1.58 % (132118)Instructions burned: 28 (million)
% 7.65/1.58 % (132122)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.65/1.58 % (132122)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=395831542:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/137Mi)
% 8.83/1.74 % (132105)Instruction limit reached!
% 8.83/1.74 % (132105)------------------------------
% 8.83/1.74 % (132105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132105)CaDiCaL version: 2.1.3
% 8.83/1.74 % (132105)Termination reason: Instruction limit
% 8.83/1.74 % (132105)Termination phase: Saturation
% 8.83/1.74 % (132105)Time elapsed: 0.188 s
% 8.83/1.74 % (132105)Peak memory usage: 15 MB
% 8.83/1.74 % (132105)Instructions burned: 376 (million)
% 8.83/1.74 % (132123)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=547799984:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 8.83/1.74 % (132125)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=4283266621:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 8.83/1.74 % (132125)Refutation not found, incomplete strategy
% 8.83/1.74 % (132125)------------------------------
% 8.83/1.74 % (132125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132125)CaDiCaL version: 2.1.3
% 8.83/1.74 % (132125)Termination reason: Refutation not found, incomplete strategy
% 8.83/1.74 % (132125)Time elapsed: 0.025 s
% 8.83/1.74 % (132125)Peak memory usage: 13 MB
% 8.83/1.74 % (132125)Instructions burned: 50 (million)
% 8.83/1.74 % (132125)------------------------------
% 8.83/1.74 % (132125)------------------------------
% 8.83/1.74 % (132122)Instruction limit reached!
% 8.83/1.74 % (132122)------------------------------
% 8.83/1.74 % (132122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132122)CaDiCaL version: 2.1.3
% 8.83/1.74 % (132122)Termination reason: Instruction limit
% 8.83/1.74 % (132122)Termination phase: Saturation
% 8.83/1.74 % (132122)Time elapsed: 0.059 s
% 8.83/1.74 % (132122)Peak memory usage: 13 MB
% 8.83/1.74 % (132122)Instructions burned: 138 (million)
% 8.83/1.74 % (132128)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 8.83/1.74 % (132128)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1833612739:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 8.83/1.74 % (132129)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=555380404:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 8.83/1.74 % (132086)Instruction limit reached!
% 8.83/1.74 % (132086)------------------------------
% 8.83/1.74 % (132086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132086)CaDiCaL version: 2.1.3
% 8.83/1.74 % (132086)Termination reason: Instruction limit
% 8.83/1.74 % (132086)Termination phase: Saturation
% 8.83/1.74 % (132086)Time elapsed: 0.488 s
% 8.83/1.74 % (132086)Peak memory usage: 16 MB
% 8.83/1.74 % (132086)Instructions burned: 875 (million)
% 8.83/1.74 % (132132)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2501512578:i=575:rtra=on_2989 on theBenchmark for (2989ds/575Mi)
% 8.83/1.74 % (132108)Instruction limit reached!
% 8.83/1.74 % (132108)------------------------------
% 8.83/1.74 % (132108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132108)CaDiCaL version: 2.1.3
% 8.83/1.74 % (132108)Termination reason: Instruction limit
% 8.83/1.74 % (132108)Termination phase: Saturation
% 8.83/1.74 % (132108)Time elapsed: 0.263 s
% 8.83/1.74 % (132108)Peak memory usage: 16 MB
% 8.83/1.74 % (132108)Instructions burned: 495 (million)
% 8.83/1.74 % (132129)Instruction limit reached!
% 8.83/1.74 % (132129)------------------------------
% 8.83/1.74 % (132129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.83/1.74 % (132129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.83/1.74 % (132129)CaDiCaL version: 2.1.3
% 9.54/1.96 % (132129)Termination reason: Instruction limit
% 9.54/1.96 % (132129)Termination phase: Saturation
% 9.54/1.96 % (132129)Time elapsed: 0.053 s
% 9.54/1.96 % (132129)Peak memory usage: 13 MB
% 9.54/1.96 % (132129)Instructions burned: 117 (million)
% 9.54/1.96 % (132134)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1994599546:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2988 on theBenchmark for (2988ds/270Mi)
% 9.54/1.96 % (132135)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=489275295: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_2988 on theBenchmark for (2988ds/9840Mi)
% 9.54/1.96 % (132117)Instruction limit reached!
% 9.54/1.96 % (132117)------------------------------
% 9.54/1.96 % (132117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.54/1.96 % (132117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.96 % (132117)CaDiCaL version: 2.1.3
% 9.54/1.96 % (132117)Termination reason: Instruction limit
% 9.54/1.96 % (132117)Termination phase: Saturation
% 9.54/1.96 % (132117)Time elapsed: 0.178 s
% 9.54/1.96 % (132117)Peak memory usage: 17 MB
% 9.54/1.96 % (132117)Instructions burned: 339 (million)
% 9.54/1.96 % (132138)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3500639935:i=421:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/421Mi)
% 9.54/1.96 % (132123)Instruction limit reached!
% 9.54/1.96 % (132123)------------------------------
% 9.54/1.96 % (132123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.54/1.96 % (132123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.96 % (132123)CaDiCaL version: 2.1.3
% 9.54/1.96 % (132123)Termination reason: Instruction limit
% 9.54/1.96 % (132123)Termination phase: Saturation
% 9.54/1.96 % (132123)Time elapsed: 0.163 s
% 9.54/1.96 % (132123)Peak memory usage: 14 MB
% 9.54/1.96 % (132123)Instructions burned: 340 (million)
% 9.54/1.96 % (132140)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
% 9.54/1.96 % (132140)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=1490807179:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/270Mi)
% 9.54/1.96 % (132128)Instruction limit reached!
% 9.54/1.96 % (132128)------------------------------
% 9.54/1.96 % (132128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.54/1.96 % (132128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.96 % (132128)CaDiCaL version: 2.1.3
% 9.54/1.96 % (132128)Termination reason: Instruction limit
% 9.54/1.96 % (132128)Termination phase: Saturation
% 9.54/1.96 % (132128)Time elapsed: 0.189 s
% 9.54/1.96 % (132128)Peak memory usage: 13 MB
% 9.54/1.96 % (132128)Instructions burned: 374 (million)
% 9.54/1.96 % (132134)Instruction limit reached!
% 9.54/1.96 % (132134)------------------------------
% 9.54/1.96 % (132134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.54/1.96 % (132134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.96 % (132134)CaDiCaL version: 2.1.3
% 9.54/1.96 % (132134)Termination reason: Instruction limit
% 9.54/1.96 % (132134)Termination phase: Saturation
% 9.54/1.96 % (132134)Time elapsed: 0.134 s
% 9.54/1.96 % (132134)Peak memory usage: 14 MB
% 9.54/1.96 % (132134)Instructions burned: 271 (million)
% 9.54/1.96 % (132142)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2255176714:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 9.54/1.96 % (132143)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.54/1.96 % (132143)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
% 9.54/1.96 % (132143)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=4109103887:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2987 on theBenchmark for (2987ds/1440Mi)
% 13.07/2.16 % (132142)Instruction limit reached!
% 13.07/2.16 % (132142)------------------------------
% 13.07/2.16 % (132142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132142)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132142)Termination reason: Instruction limit
% 13.07/2.16 % (132142)Termination phase: shuffling
% 13.07/2.16 % (132142)Time elapsed: 0.015 s
% 13.07/2.16 % (132142)Peak memory usage: 10 MB
% 13.07/2.16 % (132142)Instructions burned: 33 (million)
% 13.07/2.16 % (132146)dis+10_2_sil=128000:si=on:random_seed=2916474643:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2987 on theBenchmark for (2987ds/339Mi)
% 13.07/2.16 % (132140)Instruction limit reached!
% 13.07/2.16 % (132140)------------------------------
% 13.07/2.16 % (132140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132140)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132140)Termination reason: Instruction limit
% 13.07/2.16 % (132140)Termination phase: Saturation
% 13.07/2.16 % (132140)Time elapsed: 0.139 s
% 13.07/2.16 % (132140)Peak memory usage: 14 MB
% 13.07/2.16 % (132140)Instructions burned: 270 (million)
% 13.07/2.16 % (132148)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2650546720:i=111:add=on:fgj=on:rtra=on:fdi=1024_2986 on theBenchmark for (2986ds/111Mi)
% 13.07/2.16 % (132138)Instruction limit reached!
% 13.07/2.16 % (132138)------------------------------
% 13.07/2.16 % (132138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132138)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132138)Termination reason: Instruction limit
% 13.07/2.16 % (132138)Termination phase: Saturation
% 13.07/2.16 % (132138)Time elapsed: 0.198 s
% 13.07/2.16 % (132138)Peak memory usage: 14 MB
% 13.07/2.16 % (132138)Instructions burned: 422 (million)
% 13.07/2.16 % (132150)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=3238229649:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/122Mi)
% 13.07/2.16 % (132132)Instruction limit reached!
% 13.07/2.16 % (132132)------------------------------
% 13.07/2.16 % (132132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132132)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132132)Termination reason: Instruction limit
% 13.07/2.16 % (132132)Termination phase: Saturation
% 13.07/2.16 % (132132)Time elapsed: 0.288 s
% 13.07/2.16 % (132132)Peak memory usage: 17 MB
% 13.07/2.16 % (132132)Instructions burned: 576 (million)
% 13.07/2.16 % (132148)Instruction limit reached!
% 13.07/2.16 % (132148)------------------------------
% 13.07/2.16 % (132148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132148)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132148)Termination reason: Instruction limit
% 13.07/2.16 % (132148)Termination phase: Saturation
% 13.07/2.16 % (132148)Time elapsed: 0.051 s
% 13.07/2.16 % (132148)Peak memory usage: 13 MB
% 13.07/2.16 % (132148)Instructions burned: 113 (million)
% 13.07/2.16 % (132152)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=2465534546:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/136Mi)
% 13.07/2.16 % (132153)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4199989682:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2985 on theBenchmark for (2985ds/232Mi)
% 13.07/2.16 % (132150)Instruction limit reached!
% 13.07/2.16 % (132150)------------------------------
% 13.07/2.16 % (132150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.16 % (132150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.16 % (132150)CaDiCaL version: 2.1.3
% 13.07/2.16 % (132150)Termination reason: Instruction limit
% 13.07/2.16 % (132150)Termination phase: Saturation
% 13.07/2.16 % (132150)Time elapsed: 0.060 s
% 13.07/2.16 % (132150)Peak memory usage: 14 MB
% 13.07/2.16 % (132150)Instructions burned: 122 (million)
% 14.03/2.34 % (132156)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=833433518:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/1254Mi)
% 14.03/2.34 % (132146)Instruction limit reached!
% 14.03/2.34 % (132146)------------------------------
% 14.03/2.34 % (132146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.34 % (132146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.34 % (132146)CaDiCaL version: 2.1.3
% 14.03/2.34 % (132146)Termination reason: Instruction limit
% 14.03/2.34 % (132146)Termination phase: Saturation
% 14.03/2.34 % (132146)Time elapsed: 0.157 s
% 14.03/2.34 % (132146)Peak memory usage: 14 MB
% 14.03/2.34 % (132146)Instructions burned: 340 (million)
% 14.03/2.34 % (132152)Instruction limit reached!
% 14.03/2.34 % (132152)------------------------------
% 14.03/2.34 % (132152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.34 % (132152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.34 % (132152)CaDiCaL version: 2.1.3
% 14.03/2.34 % (132152)Termination reason: Instruction limit
% 14.03/2.34 % (132152)Termination phase: Saturation
% 14.03/2.34 % (132152)Time elapsed: 0.065 s
% 14.03/2.34 % (132152)Peak memory usage: 13 MB
% 14.03/2.34 % (132152)Instructions burned: 137 (million)
% 14.03/2.34 % (132158)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 14.03/2.34 % (132158)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=1578275181:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2985 on theBenchmark for (2985ds/281Mi)
% 14.03/2.34 % (132159)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3612022639:i=619:add=on:rtra=on_2985 on theBenchmark for (2985ds/619Mi)
% 14.03/2.34 % (132153)Instruction limit reached!
% 14.03/2.34 % (132153)------------------------------
% 14.03/2.34 % (132153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.34 % (132153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.34 % (132153)CaDiCaL version: 2.1.3
% 14.03/2.34 % (132153)Termination reason: Instruction limit
% 14.03/2.34 % (132153)Termination phase: Saturation
% 14.03/2.34 % (132153)Time elapsed: 0.120 s
% 14.03/2.34 % (132153)Peak memory usage: 14 MB
% 14.03/2.34 % (132153)Instructions burned: 234 (million)
% 14.03/2.34 % (132162)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=3051864322:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/865Mi)
% 14.03/2.34 % (132156)Refutation not found, incomplete strategy
% 14.03/2.34 % (132156)------------------------------
% 14.03/2.34 % (132156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.34 % (132156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.34 % (132156)CaDiCaL version: 2.1.3
% 14.03/2.34 % (132156)Termination reason: Refutation not found, incomplete strategy
% 14.03/2.34 % (132156)Time elapsed: 0.109 s
% 14.03/2.34 % (132156)Peak memory usage: 15 MB
% 14.03/2.34 % (132156)Instructions burned: 243 (million)
% 14.03/2.34 % (132156)------------------------------
% 14.03/2.34 % (132156)------------------------------
% 14.03/2.34 % (132159)Refutation not found, incomplete strategy
% 14.03/2.34 % (132159)------------------------------
% 14.03/2.34 % (132159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.34 % (132159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.34 % (132159)CaDiCaL version: 2.1.3
% 14.03/2.34 % (132159)Termination reason: Refutation not found, incomplete strategy
% 14.03/2.34 % (132159)Time elapsed: 0.079 s
% 14.03/2.34 % (132159)Peak memory usage: 15 MB
% 14.03/2.34 % (132159)Instructions burned: 174 (million)
% 14.03/2.34 % (132159)------------------------------
% 14.03/2.34 % (132159)------------------------------
% 14.03/2.34 % (132164)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2153008372:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/212Mi)
% 14.03/2.34 % (132165)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2891653369:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/130Mi)
% 14.03/2.34 % (132165)Instruction limit reached!
% 15.23/2.67 % (132165)------------------------------
% 15.23/2.67 % (132165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132165)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132165)Termination reason: Instruction limit
% 15.23/2.67 % (132165)Termination phase: Saturation
% 15.23/2.67 % (132165)Time elapsed: 0.066 s
% 15.23/2.67 % (132165)Peak memory usage: 14 MB
% 15.23/2.67 % (132165)Instructions burned: 131 (million)
% 15.23/2.67 % (132168)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1685988725:st=1.5:i=346:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/346Mi)
% 15.23/2.67 % (132158)Instruction limit reached!
% 15.23/2.67 % (132158)------------------------------
% 15.23/2.67 % (132158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132158)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132158)Termination reason: Instruction limit
% 15.23/2.67 % (132158)Termination phase: Saturation
% 15.23/2.67 % (132158)Time elapsed: 0.203 s
% 15.23/2.67 % (132158)Peak memory usage: 14 MB
% 15.23/2.67 % (132158)Instructions burned: 281 (million)
% 15.23/2.67 % (132164)Instruction limit reached!
% 15.23/2.67 % (132164)------------------------------
% 15.23/2.67 % (132164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132164)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132164)Termination reason: Instruction limit
% 15.23/2.67 % (132164)Termination phase: Saturation
% 15.23/2.67 % (132164)Time elapsed: 0.103 s
% 15.23/2.67 % (132164)Peak memory usage: 14 MB
% 15.23/2.67 % (132164)Instructions burned: 214 (million)
% 15.23/2.67 % (132170)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3892309897:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/152Mi)
% 15.23/2.67 % (132171)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=509398527:i=75:ep=R:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/75Mi)
% 15.23/2.67 % (132171)Instruction limit reached!
% 15.23/2.67 % (132171)------------------------------
% 15.23/2.67 % (132171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132171)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132171)Termination reason: Instruction limit
% 15.23/2.67 % (132171)Termination phase: Preprocessing 1
% 15.23/2.67 % (132171)Time elapsed: 0.033 s
% 15.23/2.67 % (132171)Peak memory usage: 10 MB
% 15.23/2.67 % (132171)Instructions burned: 77 (million)
% 15.23/2.67 % (132174)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=1630451276:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/387Mi)
% 15.23/2.67 % (132170)Instruction limit reached!
% 15.23/2.67 % (132170)------------------------------
% 15.23/2.67 % (132170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132170)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132170)Termination reason: Instruction limit
% 15.23/2.67 % (132170)Termination phase: Saturation
% 15.23/2.67 % (132170)Time elapsed: 0.073 s
% 15.23/2.67 % (132170)Peak memory usage: 14 MB
% 15.23/2.67 % (132170)Instructions burned: 154 (million)
% 15.23/2.67 % (132176)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=4226037960:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2982 on theBenchmark for (2982ds/148Mi)
% 15.23/2.67 % (132168)Instruction limit reached!
% 15.23/2.67 % (132168)------------------------------
% 15.23/2.67 % (132168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.23/2.67 % (132168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.23/2.67 % (132168)CaDiCaL version: 2.1.3
% 15.23/2.67 % (132168)Termination reason: Instruction limit
% 15.23/2.67 % (132168)Termination phase: Saturation
% 15.23/2.67 % (132168)Time elapsed: 0.177 s
% 15.23/2.67 % (132168)Peak memory usage: 15 MB
% 15.23/2.67 % (132168)Instructions burned: 348 (million)
% 15.23/2.67 % (132176)Instruction limit reached!
% 15.23/2.67 % (132176)------------------------------
% 15.23/2.67 % (132176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132176)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132176)Termination reason: Instruction limit
% 17.09/2.81 % (132176)Termination phase: Saturation
% 17.09/2.81 % (132176)Time elapsed: 0.063 s
% 17.09/2.81 % (132176)Peak memory usage: 13 MB
% 17.09/2.81 % (132176)Instructions burned: 149 (million)
% 17.09/2.81 % (132178)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=2617899605:i=161:piset=and:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/161Mi)
% 17.09/2.81 % (132179)lrs+10_1_sil=128000:si=on:random_seed=1056822568:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/888Mi)
% 17.09/2.81 % (132143)Instruction limit reached!
% 17.09/2.81 % (132143)------------------------------
% 17.09/2.81 % (132143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132143)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132143)Termination reason: Instruction limit
% 17.09/2.81 % (132143)Termination phase: Saturation
% 17.09/2.81 % (132143)Time elapsed: 0.674 s
% 17.09/2.81 % (132143)Peak memory usage: 16 MB
% 17.09/2.81 % (132143)Instructions burned: 1440 (million)
% 17.09/2.81 % (132178)Instruction limit reached!
% 17.09/2.81 % (132178)------------------------------
% 17.09/2.81 % (132178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132178)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132178)Termination reason: Instruction limit
% 17.09/2.81 % (132178)Termination phase: Saturation
% 17.09/2.81 % (132178)Time elapsed: 0.078 s
% 17.09/2.81 % (132178)Peak memory usage: 14 MB
% 17.09/2.81 % (132178)Instructions burned: 164 (million)
% 17.09/2.81 % (132182)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=448456996:i=136:add=on:ins=4:rtra=on:sup=off_2980 on theBenchmark for (2980ds/136Mi)
% 17.09/2.81 % (132174)Instruction limit reached!
% 17.09/2.81 % (132174)------------------------------
% 17.09/2.81 % (132174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132174)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132174)Termination reason: Instruction limit
% 17.09/2.81 % (132174)Termination phase: Saturation
% 17.09/2.81 % (132174)Time elapsed: 0.212 s
% 17.09/2.81 % (132174)Peak memory usage: 15 MB
% 17.09/2.81 % (132174)Instructions burned: 388 (million)
% 17.09/2.81 % (132183)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=2624364473:i=88:s2at=3:nm=2:rtra=on:rawr=on_2980 on theBenchmark for (2980ds/88Mi)
% 17.09/2.81 % (132185)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=83165268:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2980 on theBenchmark for (2980ds/93Mi)
% 17.09/2.81 % (132183)Instruction limit reached!
% 17.09/2.81 % (132183)------------------------------
% 17.09/2.81 % (132183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132183)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132183)Termination reason: Instruction limit
% 17.09/2.81 % (132183)Termination phase: Preprocessing 1
% 17.09/2.81 % (132183)Time elapsed: 0.039 s
% 17.09/2.81 % (132183)Peak memory usage: 11 MB
% 17.09/2.81 % (132183)Instructions burned: 89 (million)
% 17.09/2.81 % (132185)Instruction limit reached!
% 17.09/2.81 % (132185)------------------------------
% 17.09/2.81 % (132185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/2.81 % (132185)CaDiCaL version: 2.1.3
% 17.09/2.81 % (132185)Termination reason: Instruction limit
% 17.09/2.81 % (132185)Termination phase: Preprocessing 3
% 17.09/2.81 % (132185)Time elapsed: 0.041 s
% 17.09/2.81 % (132185)Peak memory usage: 11 MB
% 17.09/2.81 % (132185)Instructions burned: 93 (million)
% 17.09/2.81 % (132162)Instruction limit reached!
% 17.09/2.81 % (132162)------------------------------
% 17.09/2.81 % (132162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.09/2.81 % (132162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132162)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132162)Termination reason: Instruction limit
% 17.29/2.99 % (132162)Termination phase: Saturation
% 17.29/2.99 % (132188)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1689032982:i=2186:rtra=on:ixr=off_2979 on theBenchmark for (2979ds/2186Mi)
% 17.29/2.99 % (132162)Time elapsed: 0.484 s
% 17.29/2.99 % (132162)Peak memory usage: 19 MB
% 17.29/2.99 % (132162)Instructions burned: 865 (million)
% 17.29/2.99 % (132182)Instruction limit reached!
% 17.29/2.99 % (132182)------------------------------
% 17.29/2.99 % (132182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.29/2.99 % (132182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132182)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132182)Termination reason: Instruction limit
% 17.29/2.99 % (132182)Termination phase: Saturation
% 17.29/2.99 % (132182)Time elapsed: 0.064 s
% 17.29/2.99 % (132182)Peak memory usage: 13 MB
% 17.29/2.99 % (132182)Instructions burned: 137 (million)
% 17.29/2.99 % (132192)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 17.29/2.99 % (132190)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1470784176:s2a=on:i=240:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/240Mi)
% 17.29/2.99 % (132191)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2447292399:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2979 on theBenchmark for (2979ds/805Mi)
% 17.29/2.99 % (132192)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=2802712708:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2979 on theBenchmark for (2979ds/391Mi)
% 17.29/2.99 % (132190)Instruction limit reached!
% 17.29/2.99 % (132190)------------------------------
% 17.29/2.99 % (132190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.29/2.99 % (132190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132190)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132190)Termination reason: Instruction limit
% 17.29/2.99 % (132190)Termination phase: Saturation
% 17.29/2.99 % (132190)Time elapsed: 0.119 s
% 17.29/2.99 % (132190)Peak memory usage: 15 MB
% 17.29/2.99 % (132190)Instructions burned: 241 (million)
% 17.29/2.99 % (132196)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=449385463:i=355:av=off:fsr=off:rtra=on:ixr=off_2978 on theBenchmark for (2978ds/355Mi)
% 17.29/2.99 % (132192)Instruction limit reached!
% 17.29/2.99 % (132192)------------------------------
% 17.29/2.99 % (132192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.29/2.99 % (132192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132192)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132192)Termination reason: Instruction limit
% 17.29/2.99 % (132192)Termination phase: Saturation
% 17.29/2.99 % (132192)Time elapsed: 0.188 s
% 17.29/2.99 % (132192)Peak memory usage: 15 MB
% 17.29/2.99 % (132192)Instructions burned: 391 (million)
% 17.29/2.99 % (132198)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=1805003716:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/314Mi)
% 17.29/2.99 % (132179)Instruction limit reached!
% 17.29/2.99 % (132179)------------------------------
% 17.29/2.99 % (132179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.29/2.99 % (132179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132179)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132179)Termination reason: Instruction limit
% 17.29/2.99 % (132179)Termination phase: Saturation
% 17.29/2.99 % (132179)Time elapsed: 0.484 s
% 17.29/2.99 % (132179)Peak memory usage: 19 MB
% 17.29/2.99 % (132179)Instructions burned: 888 (million)
% 17.29/2.99 % (132196)Instruction limit reached!
% 17.29/2.99 % (132196)------------------------------
% 17.29/2.99 % (132196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.29/2.99 % (132196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.29/2.99 % (132196)CaDiCaL version: 2.1.3
% 17.29/2.99 % (132196)Termination reason: Instruction limit
% 17.29/2.99 % (132196)Termination phase: Saturation
% 17.29/2.99 % (132196)Time elapsed: 0.179 s
% 17.29/2.99 % (132196)Peak memory usage: 14 MB
% 17.29/2.99 % (132196)Instructions burned: 356 (million)
% 20.04/3.17 % (132200)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=234504802:s2a=on:i=251:fsr=off:rtra=on_2976 on theBenchmark for (2976ds/251Mi)
% 20.04/3.17 % (132201)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=4192856635:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2976 on theBenchmark for (2976ds/2470Mi)
% 20.04/3.17 % (132104)Instruction limit reached!
% 20.04/3.17 % (132104)------------------------------
% 20.04/3.17 % (132104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.17 % (132104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.17 % (132104)CaDiCaL version: 2.1.3
% 20.04/3.17 % (132104)Termination reason: Instruction limit
% 20.04/3.17 % (132104)Termination phase: Saturation
% 20.04/3.17 % (132104)Time elapsed: 1.630 s
% 20.04/3.17 % (132104)Peak memory usage: 35 MB
% 20.04/3.17 % (132104)Instructions burned: 5757 (million)
% 20.04/3.18 % (132198)Instruction limit reached!
% 20.04/3.18 % (132198)------------------------------
% 20.04/3.18 % (132198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132198)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132198)Termination reason: Instruction limit
% 20.04/3.18 % (132198)Termination phase: Saturation
% 20.04/3.18 % (132198)Time elapsed: 0.159 s
% 20.04/3.18 % (132198)Peak memory usage: 14 MB
% 20.04/3.18 % (132198)Instructions burned: 315 (million)
% 20.04/3.18 % (132204)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=585441307:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2975 on theBenchmark for (2975ds/673Mi)
% 20.04/3.18 % (132205)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1174624954:i=116:ep=RSTC:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/116Mi)
% 20.04/3.18 % (132191)Instruction limit reached!
% 20.04/3.18 % (132191)------------------------------
% 20.04/3.18 % (132191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132191)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132191)Termination reason: Instruction limit
% 20.04/3.18 % (132191)Termination phase: Saturation
% 20.04/3.18 % (132191)Time elapsed: 0.399 s
% 20.04/3.18 % (132191)Peak memory usage: 17 MB
% 20.04/3.18 % (132191)Instructions burned: 805 (million)
% 20.04/3.18 % (132208)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2420494646:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2975 on theBenchmark for (2975ds/270Mi)
% 20.04/3.18 % (132200)Instruction limit reached!
% 20.04/3.18 % (132200)------------------------------
% 20.04/3.18 % (132200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132200)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132200)Termination reason: Instruction limit
% 20.04/3.18 % (132200)Termination phase: Saturation
% 20.04/3.18 % (132200)Time elapsed: 0.107 s
% 20.04/3.18 % (132200)Peak memory usage: 13 MB
% 20.04/3.18 % (132200)Instructions burned: 252 (million)
% 20.04/3.18 % (132205)Instruction limit reached!
% 20.04/3.18 % (132205)------------------------------
% 20.04/3.18 % (132205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132205)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132205)Termination reason: Instruction limit
% 20.04/3.18 % (132205)Termination phase: Saturation
% 20.04/3.18 % (132205)Time elapsed: 0.053 s
% 20.04/3.18 % (132205)Peak memory usage: 13 MB
% 20.04/3.18 % (132205)Instructions burned: 117 (million)
% 20.04/3.18 % (132211)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 20.04/3.18 % (132210)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=1694245503:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2974 on theBenchmark for (2974ds/30Mi)
% 20.04/3.18 % (132211)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2828118060:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2974 on theBenchmark for (2974ds/39Mi)
% 20.04/3.18 % (132210)Instruction limit reached!
% 20.04/3.18 % (132210)------------------------------
% 20.04/3.18 % (132210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132210)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132210)Termination reason: Instruction limit
% 20.04/3.18 % (132210)Termination phase: Property scanning
% 20.04/3.18 % (132210)Time elapsed: 0.014 s
% 20.04/3.18 % (132210)Peak memory usage: 10 MB
% 20.04/3.18 % (132210)Instructions burned: 31 (million)
% 20.04/3.18 % (132211)Instruction limit reached!
% 20.04/3.18 % (132211)------------------------------
% 20.04/3.18 % (132211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132211)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132211)Termination reason: Instruction limit
% 20.04/3.18 % (132211)Termination phase: Property scanning
% 20.04/3.18 % (132211)Time elapsed: 0.018 s
% 20.04/3.18 % (132211)Peak memory usage: 11 MB
% 20.04/3.18 % (132211)Instructions burned: 40 (million)
% 20.04/3.18 % (132214)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=947323598:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2974 on theBenchmark for (2974ds/365Mi)
% 20.04/3.18 % (132215)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1162696116:i=158:av=off:rtra=on_2974 on theBenchmark for (2974ds/158Mi)
% 20.04/3.18 % (132208)Instruction limit reached!
% 20.04/3.18 % (132208)------------------------------
% 20.04/3.18 % (132208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132208)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132208)Termination reason: Instruction limit
% 20.04/3.18 % (132208)Termination phase: Saturation
% 20.04/3.18 % (132208)Time elapsed: 0.135 s
% 20.04/3.18 % (132208)Peak memory usage: 14 MB
% 20.04/3.18 % (132208)Instructions burned: 271 (million)
% 20.04/3.18 % (132204)Instruction limit reached!
% 20.04/3.18 % (132204)------------------------------
% 20.04/3.18 % (132204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132204)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132204)Termination reason: Instruction limit
% 20.04/3.18 % (132204)Termination phase: Saturation
% 20.04/3.18 % (132204)Time elapsed: 0.192 s
% 20.04/3.18 % (132204)Peak memory usage: 15 MB
% 20.04/3.18 % (132204)Instructions burned: 675 (million)
% 20.04/3.18 % (132218)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
% 20.04/3.18 % (132218)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=3983448829:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2973 on theBenchmark for (2973ds/252Mi)
% 20.04/3.18 % (132215)Instruction limit reached!
% 20.04/3.18 % (132215)------------------------------
% 20.04/3.18 % (132215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132215)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132215)Termination reason: Instruction limit
% 20.04/3.18 % (132215)Termination phase: Saturation
% 20.04/3.18 % (132215)Time elapsed: 0.077 s
% 20.04/3.18 % (132215)Peak memory usage: 13 MB
% 20.04/3.18 % (132215)Instructions burned: 160 (million)
% 20.04/3.18 % (132219)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=369847611:i=213:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/213Mi)
% 20.04/3.18 % (132221)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=2882266045:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2973 on theBenchmark for (2973ds/160Mi)
% 20.04/3.18 % (132219)Refutation not found, incomplete strategy
% 20.04/3.18 % (132219)------------------------------
% 20.04/3.18 % (132219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132219)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132219)Termination reason: Refutation not found, incomplete strategy
% 20.04/3.18 % (132219)Time elapsed: 0.044 s
% 20.04/3.18 % (132219)Peak memory usage: 14 MB
% 20.04/3.18 % (132219)Instructions burned: 92 (million)
% 20.04/3.18 % (132219)------------------------------
% 20.04/3.18 % (132219)------------------------------
% 20.04/3.18 % (132224)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=4215656370:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2972 on theBenchmark for (2972ds/763Mi)
% 20.04/3.18 % (132214)Instruction limit reached!
% 20.04/3.18 % (132214)------------------------------
% 20.04/3.18 % (132214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132214)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132214)Termination reason: Instruction limit
% 20.04/3.18 % (132214)Termination phase: Saturation
% 20.04/3.18 % (132214)Time elapsed: 0.180 s
% 20.04/3.18 % (132214)Peak memory usage: 15 MB
% 20.04/3.18 % (132214)Instructions burned: 365 (million)
% 20.04/3.18 % (132221)Instruction limit reached!
% 20.04/3.18 % (132221)------------------------------
% 20.04/3.18 % (132221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132221)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132221)Termination reason: Instruction limit
% 20.04/3.18 % (132221)Termination phase: Saturation
% 20.04/3.18 % (132221)Time elapsed: 0.083 s
% 20.04/3.18 % (132221)Peak memory usage: 14 MB
% 20.04/3.18 % (132221)Instructions burned: 161 (million)
% 20.04/3.18 % (132226)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 20.04/3.18 % (132226)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=175500030:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2972 on theBenchmark for (2972ds/237Mi)
% 20.04/3.18 % (132227)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=1106563480:s2a=on:i=386:rtra=on:ntd=on_2972 on theBenchmark for (2972ds/386Mi)
% 20.04/3.18 % (132218)Instruction limit reached!
% 20.04/3.18 % (132218)------------------------------
% 20.04/3.18 % (132218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132218)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132218)Termination reason: Instruction limit
% 20.04/3.18 % (132218)Termination phase: Saturation
% 20.04/3.18 % (132218)Time elapsed: 0.130 s
% 20.04/3.18 % (132218)Peak memory usage: 14 MB
% 20.04/3.18 % (132218)Instructions burned: 252 (million)
% 20.04/3.18 % (132230)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=2247175003:i=300:piset=and:nm=32:rtra=on_2972 on theBenchmark for (2972ds/300Mi)
% 20.04/3.18 % (132226)Refutation not found, incomplete strategy
% 20.04/3.18 % (132226)------------------------------
% 20.04/3.18 % (132226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132226)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132226)Termination reason: Refutation not found, incomplete strategy
% 20.04/3.18 % (132226)Time elapsed: 0.054 s
% 20.04/3.18 % (132226)Peak memory usage: 14 MB
% 20.04/3.18 % (132226)Instructions burned: 109 (million)
% 20.04/3.18 % (132226)------------------------------
% 20.04/3.18 % (132226)------------------------------
% 20.04/3.18 % (132232)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=3194070941:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/567Mi)
% 20.04/3.18 % (132201) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-131965-132201"...
% 20.04/3.18 % (132201)...printing done.
% 20.04/3.18 % (132201)Refutation found. Thanks to Tanya!
% 20.04/3.18 % SZS status Theorem for theBenchmark
% 20.04/3.18 % SZS output start Proof for theBenchmark
% 20.04/3.18 thf(type_def_5, type, coinductive_llist: $tType > $tType).
% 20.04/3.18 thf(type_def_6, type, list: $tType > $tType).
% 20.04/3.18 thf(type_def_7, type, set: $tType > $tType).
% 20.04/3.18 thf(type_def_8, type, itself: $tType > $tType).
% 20.04/3.18 thf(type_def_9, type, a: $tType).
% 20.04/3.18 thf(type_def_10, type, sTfun: ($tType * $tType) > $tType).
% 20.04/3.18 thf(func_def_0, type, coindu328551480prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 20.04/3.18 thf(func_def_1, type, coinductive_lappend: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 20.04/3.18 thf(func_def_2, type, coinductive_lfinite: !>[X0: $tType]:((coinductive_llist @ X0 > $o))).
% 20.04/3.18 thf(func_def_3, type, coinductive_list_of: !>[X0: $tType]:((coinductive_llist @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_4, type, coindu1384447384of_aux: !>[X0: $tType]:((list @ X0 > coinductive_llist @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_5, type, coinductive_llast: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 20.04/3.18 thf(func_def_6, type, coinductive_LCons: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 20.04/3.18 thf(func_def_7, type, coinductive_LNil: !>[X0: $tType]:(coinductive_llist @ X0)).
% 20.04/3.18 thf(func_def_8, type, coinductive_lnull: !>[X0: $tType]:((coinductive_llist @ X0 > $o))).
% 20.04/3.18 thf(func_def_9, type, coinductive_lset: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0))).
% 20.04/3.18 thf(func_def_10, type, coinductive_llist_of: !>[X0: $tType]:((list @ X0 > coinductive_llist @ X0))).
% 20.04/3.18 thf(func_def_11, type, coindu1478340336prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 20.04/3.18 thf(func_def_12, type, undefined: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_13, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 20.04/3.18 thf(func_def_14, type, koenig793108494nected: !>[X0: $tType]:(((X0 > X0 > $o) > $o))).
% 20.04/3.18 thf(func_def_15, type, koenig916195507_paths: !>[X0: $tType]:(((X0 > X0 > $o) > set @ coinductive_llist @ X0))).
% 20.04/3.18 thf(func_def_16, type, append: !>[X0: $tType]:((list @ X0 > list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_17, type, bind: !>[X0: $tType, X1: $tType]:((list @ X0 > (X0 > list @ X1) > list @ X1))).
% 20.04/3.18 thf(func_def_18, type, butlast: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_19, type, can_select: !>[X0: $tType]:(((X0 > $o) > set @ X0 > $o))).
% 20.04/3.18 thf(func_def_20, type, insert: !>[X0: $tType]:((X0 > list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_21, type, last: !>[X0: $tType]:((list @ X0 > X0))).
% 20.04/3.18 thf(func_def_22, type, cons: !>[X0: $tType]:((X0 > list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_23, type, nil: !>[X0: $tType]:(list @ X0)).
% 20.04/3.18 thf(func_def_24, type, map: !>[X0: $tType, X1: $tType]:(((X0 > X1) > list @ X0 > list @ X1))).
% 20.04/3.18 thf(func_def_25, type, set2: !>[X0: $tType]:((list @ X0 > set @ X0))).
% 20.04/3.18 thf(func_def_26, type, list_ex1: !>[X0: $tType]:(((X0 > $o) > list @ X0 > $o))).
% 20.04/3.18 thf(func_def_27, type, map_tailrec: !>[X0: $tType, X1: $tType]:(((X0 > X1) > list @ X0 > list @ X1))).
% 20.04/3.18 thf(func_def_28, type, map_tailrec_rev: !>[X0: $tType, X1: $tType]:(((X0 > X1) > list @ X0 > list @ X1 > list @ X1))).
% 20.04/3.18 thf(func_def_29, type, maps: !>[X0: $tType, X1: $tType]:(((X0 > list @ X1) > list @ X0 > list @ X1))).
% 20.04/3.18 thf(func_def_30, type, product_lists: !>[X0: $tType]:((list @ list @ X0 > list @ list @ X0))).
% 20.04/3.18 thf(func_def_31, type, rev: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_32, type, rotate1: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_33, type, sublists: !>[X0: $tType]:((list @ X0 > list @ list @ X0))).
% 20.04/3.18 thf(func_def_34, type, type: !>[X0: $tType]:(itself @ X0)).
% 20.04/3.18 thf(func_def_35, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 20.04/3.18 thf(func_def_36, type, the_elem: !>[X0: $tType]:((set @ X0 > X0))).
% 20.04/3.18 thf(func_def_37, type, prefixes: !>[X0: $tType]:((list @ X0 > list @ list @ X0))).
% 20.04/3.18 thf(func_def_38, type, prefixes_rel: !>[X0: $tType]:((list @ X0 > list @ X0 > $o))).
% 20.04/3.18 thf(func_def_39, type, strict_suffix: !>[X0: $tType]:((list @ X0 > list @ X0 > $o))).
% 20.04/3.18 thf(func_def_40, type, accp: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > $o))).
% 20.04/3.18 thf(func_def_41, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 20.04/3.18 thf(func_def_42, type, xs: list @ a).
% 20.04/3.18 thf(func_def_43, type, graph: (a > a > $o)).
% 20.04/3.18 thf(func_def_44, type, n: a).
% 20.04/3.18 thf(func_def_45, type, x: a).
% 20.04/3.18 thf(func_def_46, type, xs2: coinductive_llist @ a).
% 20.04/3.18 thf(func_def_47, type, xs3: coinductive_llist @ a).
% 20.04/3.18 thf(func_def_48, type, xs4: coinductive_llist @ a).
% 20.04/3.18 thf(func_def_49, type, ys: list @ a).
% 20.04/3.18 thf(func_def_50, type, zs: list @ a).
% 20.04/3.18 thf(func_def_54, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 20.04/3.18 thf(func_def_55, type, vIMP: ($o > $o > $o)).
% 20.04/3.18 thf(func_def_56, type, db1: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_57, type, db3: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_58, type, db0: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_59, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 20.04/3.18 thf(func_def_60, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 20.04/3.18 thf(func_def_61, type, db2: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_62, type, vNOT: ($o > $o)).
% 20.04/3.18 thf(func_def_63, type, vAND: ($o > $o > $o)).
% 20.04/3.18 thf(func_def_64, type, db4: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_65, type, db5: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_66, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 20.04/3.18 thf(func_def_67, type, vOR: ($o > $o > $o)).
% 20.04/3.18 thf(func_def_68, type, db6: !>[X0: $tType]:(X0)).
% 20.04/3.18 thf(func_def_70, type, sK1: list @ a).
% 20.04/3.18 thf(func_def_71, type, sK2: list @ a).
% 20.04/3.18 thf(func_def_72, type, sK3: list @ a).
% 20.04/3.18 thf(func_def_73, type, sK4: list @ a).
% 20.04/3.18 thf(func_def_74, type, sK5: list @ a).
% 20.04/3.18 thf(func_def_75, type, sK6: coinductive_llist @ a).
% 20.04/3.18 thf(func_def_76, type, sK7: coinductive_llist @ a).
% 20.04/3.18 thf(func_def_77, type, sK8: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 20.04/3.18 thf(func_def_78, type, sK9: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 20.04/3.18 thf(func_def_79, type, sK10: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_80, type, sK11: !>[X0: $tType]:((list @ X0 > X0))).
% 20.04/3.18 thf(func_def_81, type, sK12: !>[X0: $tType]:((list @ X0 > X0))).
% 20.04/3.18 thf(func_def_82, type, sK13: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_83, type, sK14: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 20.04/3.18 thf(func_def_84, type, sK15: !>[X0: $tType]:((list @ X0 > X0))).
% 20.04/3.18 thf(f1,axiom,(
% 20.04/3.18 (xs4 = ((coinductive_llist_of @ a @ xs)))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_xs_H)).
% 20.04/3.18 thf(f4,axiom,(
% 20.04/3.18 (member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_path)).
% 20.04/3.18 thf(f5,axiom,(
% 20.04/3.18 (xs2 = ((coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_xs)).
% 20.04/3.18 thf(f6,axiom,(
% 20.04/3.18 (xs = ((append @ a @ ys @ (cons @ a @ n @ zs))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_XS_H)).
% 20.04/3.18 thf(f20,axiom,(
% 20.04/3.18 ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ X1)) = X1)),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_lappend__code_I1_J)).
% 20.04/3.18 thf(f22,axiom,(
% 20.04/3.18 ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0] : (((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X2) @ X3)) = ((coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X2 @ X3))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_lappend__code_I2_J)).
% 20.04/3.18 thf(f63,axiom,(
% 20.04/3.18 ! [X0 : $tType,X3 : coinductive_llist @ X0,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X1 @ X2) @ X3)) = ((coinductive_lappend @ X0 @ X1 @ (coinductive_lappend @ X0 @ X2 @ X3))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_lappend__assoc)).
% 20.04/3.18 thf(f65,axiom,(
% 20.04/3.18 ! [X0 : $tType,X1 : X0,X2 : list @ X0] : (((coinductive_llist_of @ X0 @ (cons @ X0 @ X1 @ X2))) = ((coinductive_LCons @ X0 @ X1 @ (coinductive_llist_of @ X0 @ X2))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_llist__of_Osimps_I2_J)).
% 20.04/3.18 thf(f66,axiom,(
% 20.04/3.18 ! [X0 : $tType,X2 : list @ X0,X1 : list @ X0] : (((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X1) @ (coinductive_llist_of @ X0 @ X2))) = ((coinductive_llist_of @ X0 @ (append @ X0 @ X1 @ X2))))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_lappend__llist__of__llist__of)).
% 20.04/3.18 thf(f146,axiom,(
% 20.04/3.18 ! [X0 : $tType] : (((coinductive_llist_of @ X0 @ nil @ X0)) = coinductive_LNil @ X0)),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_llist__of_Osimps_I1_J)).
% 20.04/3.18 thf(f258,conjecture,(
% 20.04/3.18 (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))),
% 20.04/3.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 20.04/3.18 thf(f259,negated_conjecture,(
% 20.04/3.18 ~(member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))),
% 20.04/3.18 inference(negated_conjecture,[status(cth)],[f258])).
% 20.04/3.18 thf(f265,plain,(
% 20.04/3.18 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ X2 @ (coinductive_lappend @ X0 @ X3 @ X1))) = ((coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X2 @ X3) @ X1)))),
% 20.04/3.18 inference(rectify,[],[f63])).
% 20.04/3.18 thf(f266,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y1 @ (coinductive_lappend @ X0 @ Y0 @ Y2)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y1 @ Y0) @ Y2))))))))) = $true)) )),
% 20.04/3.18 inference(fool_elimination,[],[f265])).
% 20.04/3.18 thf(f271,plain,(
% 20.04/3.18 (member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))),
% 20.04/3.18 inference(rectify,[],[f4])).
% 20.04/3.18 thf(f272,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) = $true)),
% 20.04/3.18 inference(fool_elimination,[],[f271])).
% 20.04/3.18 thf(f316,plain,(
% 20.04/3.18 (xs = ((append @ a @ ys @ (cons @ a @ n @ zs))))),
% 20.04/3.18 inference(fool_elimination,[],[f6])).
% 20.04/3.18 thf(f403,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ Y0) = Y0)))) = $true)) )),
% 20.04/3.18 inference(fool_elimination,[],[f20])).
% 20.04/3.18 thf(f454,plain,(
% 20.04/3.18 (xs2 = ((coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3))))),
% 20.04/3.18 inference(fool_elimination,[],[f5])).
% 20.04/3.18 thf(f524,plain,(
% 20.04/3.18 ~(member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))),
% 20.04/3.18 inference(rectify,[],[f259])).
% 20.04/3.18 thf(f525,plain,(
% 20.04/3.18 (((~ (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph)))) = $true)),
% 20.04/3.18 inference(fool_elimination,[],[f524])).
% 20.04/3.18 thf(f563,plain,(
% 20.04/3.18 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X3 : X0] : (((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X3 @ X1) @ X2)) = ((coinductive_LCons @ X0 @ X3 @ (coinductive_lappend @ X0 @ X1 @ X2))))),
% 20.04/3.18 inference(rectify,[],[f22])).
% 20.04/3.18 thf(f564,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : (($true = ((!! @ X0 @ (^[Y0 : X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ Y0 @ Y2) @ Y1) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_lappend @ X0 @ Y2 @ Y1)))))))))))) )),
% 20.04/3.18 inference(fool_elimination,[],[f563])).
% 20.04/3.18 thf(f627,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ X0 @ (^[Y1 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y1 @ Y0)) = (coinductive_LCons @ X0 @ Y1 @ (coinductive_llist_of @ X0 @ Y0)))))))) = $true)) )),
% 20.04/3.18 inference(fool_elimination,[],[f65])).
% 20.04/3.18 thf(f654,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((coinductive_LNil @ X0 = (coinductive_llist_of @ X0 @ nil @ X0))) = $true)) )),
% 20.04/3.18 inference(fool_elimination,[],[f146])).
% 20.04/3.18 thf(f659,plain,(
% 20.04/3.18 ! [X0 : $tType,X1 : list @ X0,X2 : list @ X0] : (((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X2) @ (coinductive_llist_of @ X0 @ X1))) = ((coinductive_llist_of @ X0 @ (append @ X0 @ X2 @ X1))))),
% 20.04/3.18 inference(rectify,[],[f66])).
% 20.04/3.18 thf(f660,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ list @ X0 @ (^[Y1 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ Y0) @ (coinductive_llist_of @ X0 @ Y1)) = (coinductive_llist_of @ X0 @ (append @ X0 @ Y0 @ Y1)))))))) = $true)) )),
% 20.04/3.18 inference(fool_elimination,[],[f659])).
% 20.04/3.18 thf(f678,plain,(
% 20.04/3.18 (xs4 = ((coinductive_llist_of @ a @ xs)))),
% 20.04/3.18 inference(fool_elimination,[],[f1])).
% 20.04/3.18 thf(f712,plain,(
% 20.04/3.18 ! [X0 : $tType] : (((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y1 @ (coinductive_lappend @ X0 @ Y0 @ Y2)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y1 @ Y0) @ Y2))))))))) = $true)),
% 20.04/3.18 inference(closure,[],[f266])).
% 20.04/3.18 thf(f789,plain,(
% 20.04/3.18 ! [X0 : $tType] : (((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ Y0) = Y0)))) = $true)),
% 20.04/3.18 inference(closure,[],[f403])).
% 20.04/3.18 thf(f876,plain,(
% 20.04/3.18 ! [X0 : $tType] : ($true = ((!! @ X0 @ (^[Y0 : X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ Y0 @ Y2) @ Y1) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_lappend @ X0 @ Y2 @ Y1)))))))))))),
% 20.04/3.18 inference(closure,[],[f564])).
% 20.04/3.18 thf(f914,plain,(
% 20.04/3.18 ! [X0 : $tType] : (((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ X0 @ (^[Y1 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y1 @ Y0)) = (coinductive_LCons @ X0 @ Y1 @ (coinductive_llist_of @ X0 @ Y0)))))))) = $true)),
% 20.04/3.18 inference(closure,[],[f627])).
% 20.04/3.18 thf(f930,plain,(
% 20.04/3.18 ! [X0 : $tType] : (((coinductive_LNil @ X0 = (coinductive_llist_of @ X0 @ nil @ X0))) = $true)),
% 20.04/3.18 inference(closure,[],[f654])).
% 20.04/3.18 thf(f933,plain,(
% 20.04/3.18 ! [X0 : $tType] : (((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ list @ X0 @ (^[Y1 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ Y0) @ (coinductive_llist_of @ X0 @ Y1)) = (coinductive_llist_of @ X0 @ (append @ X0 @ Y0 @ Y1)))))))) = $true)),
% 20.04/3.18 inference(closure,[],[f660])).
% 20.04/3.18 thf(f994,plain,(
% 20.04/3.18 (((~ (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph)))) = $true)),
% 20.04/3.18 inference(cnf_transformation,[],[f525])).
% 20.04/3.18 thf(f1004,plain,(
% 20.04/3.18 (xs2 = ((coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3))))),
% 20.04/3.18 inference(cnf_transformation,[],[f454])).
% 20.04/3.18 thf(f1027,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y1 @ (coinductive_lappend @ X0 @ Y0 @ Y2)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y1 @ Y0) @ Y2))))))))) = $true)) )),
% 20.04/3.18 inference(cnf_transformation,[],[f712])).
% 20.04/3.18 thf(f1038,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ list @ X0 @ (^[Y1 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ Y0) @ (coinductive_llist_of @ X0 @ Y1)) = (coinductive_llist_of @ X0 @ (append @ X0 @ Y0 @ Y1)))))))) = $true)) )),
% 20.04/3.18 inference(cnf_transformation,[],[f933])).
% 20.04/3.18 thf(f1119,plain,(
% 20.04/3.18 (xs4 = ((coinductive_llist_of @ a @ xs)))),
% 20.04/3.18 inference(cnf_transformation,[],[f678])).
% 20.04/3.18 thf(f1122,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ Y0) = Y0)))) = $true)) )),
% 20.04/3.18 inference(cnf_transformation,[],[f789])).
% 20.04/3.18 thf(f1129,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((!! @ list @ X0 @ (^[Y0 : list @ X0]: (!! @ X0 @ (^[Y1 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y1 @ Y0)) = (coinductive_LCons @ X0 @ Y1 @ (coinductive_llist_of @ X0 @ Y0)))))))) = $true)) )),
% 20.04/3.18 inference(cnf_transformation,[],[f914])).
% 20.04/3.18 thf(f1136,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) = $true)),
% 20.04/3.18 inference(cnf_transformation,[],[f272])).
% 20.04/3.18 thf(f1153,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : (($true = ((!! @ X0 @ (^[Y0 : X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ Y0 @ Y2) @ Y1) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_lappend @ X0 @ Y2 @ Y1)))))))))))) )),
% 20.04/3.18 inference(cnf_transformation,[],[f876])).
% 20.04/3.18 thf(f1171,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((((coinductive_LNil @ X0 = (coinductive_llist_of @ X0 @ nil @ X0))) = $true)) )),
% 20.04/3.18 inference(cnf_transformation,[],[f930])).
% 20.04/3.18 thf(f1234,plain,(
% 20.04/3.18 (xs = ((append @ a @ ys @ (cons @ a @ n @ zs))))),
% 20.04/3.18 inference(cnf_transformation,[],[f316])).
% 20.04/3.18 thf(f1236,definition,(
% 20.04/3.18 ($false != $true)),
% 20.04/3.18 introduced(theory,[fool_distinctness_axiom])).
% 20.04/3.18 thf(f1245,definition,(
% 20.04/3.18 spl0_1 <=> (xs4 = ((coinductive_llist_of @ a @ xs)))),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 20.04/3.18 thf(f1246,plain,(
% 20.04/3.18 (xs4 = ((coinductive_llist_of @ a @ xs))) | ~spl0_1),
% 20.04/3.18 inference(avatar_component_clause,[],[f1245])).
% 20.04/3.18 thf(f1247,plain,(
% 20.04/3.18 spl0_1),
% 20.04/3.18 inference(avatar_split_clause,[],[f1119,f1245])).
% 20.04/3.18 thf(f1249,definition,(
% 20.04/3.18 spl0_2 <=> ($false = $true)),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 20.04/3.18 thf(f1251,plain,(
% 20.04/3.18 ~spl0_2),
% 20.04/3.18 inference(avatar_split_clause,[],[f1236,f1249])).
% 20.04/3.18 thf(f1252,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))) = $false)),
% 20.04/3.18 inference(not_proxy_clausification,[],[f994])).
% 20.04/3.18 thf(f1268,plain,(
% 20.04/3.18 ( ! [X0 : $tType] : ((coinductive_LNil @ X0 = ((coinductive_llist_of @ X0 @ nil @ X0)))) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f1171])).
% 20.04/3.18 thf(f1276,definition,(
% 20.04/3.18 spl0_6 <=> (xs = ((append @ a @ ys @ (cons @ a @ n @ zs))))),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 20.04/3.18 thf(f1277,plain,(
% 20.04/3.18 (xs = ((append @ a @ ys @ (cons @ a @ n @ zs)))) | ~spl0_6),
% 20.04/3.18 inference(avatar_component_clause,[],[f1276])).
% 20.04/3.18 thf(f1278,plain,(
% 20.04/3.18 spl0_6),
% 20.04/3.18 inference(avatar_split_clause,[],[f1234,f1276])).
% 20.04/3.18 thf(f1289,definition,(
% 20.04/3.18 spl0_8 <=> (xs2 = ((coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3))))),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 20.04/3.18 thf(f1290,plain,(
% 20.04/3.18 (xs2 = ((coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3)))) | ~spl0_8),
% 20.04/3.18 inference(avatar_component_clause,[],[f1289])).
% 20.04/3.18 thf(f1291,plain,(
% 20.04/3.18 spl0_8),
% 20.04/3.18 inference(avatar_split_clause,[],[f1004,f1289])).
% 20.04/3.18 thf(f1298,definition,(
% 20.04/3.18 spl0_10 <=> (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) = $true)),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition])).
% 20.04/3.18 thf(f1300,plain,(
% 20.04/3.18 spl0_10),
% 20.04/3.18 inference(avatar_split_clause,[],[f1136,f1298])).
% 20.04/3.18 thf(f1327,definition,(
% 20.04/3.18 spl0_15 <=> (((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))) = $false)),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition])).
% 20.04/3.18 thf(f1328,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ ys)) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3)) @ (koenig916195507_paths @ a @ graph))) = $false) | ~spl0_15),
% 20.04/3.18 inference(avatar_component_clause,[],[f1327])).
% 20.04/3.18 thf(f1329,plain,(
% 20.04/3.18 spl0_15),
% 20.04/3.18 inference(avatar_split_clause,[],[f1252,f1327])).
% 20.04/3.18 thf(f1400,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((((^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ Y0) = Y0)) @ X1)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1122])).
% 20.04/3.18 thf(f1401,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((((coinductive_lappend @ X0 @ coinductive_LNil @ X0 @ X1) = X1)) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f1400])).
% 20.04/3.18 thf(f1402,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ nil @ X0) @ X1) = X1)) = $true)) )),
% 20.04/3.18 inference(forward_demodulation,[],[f1401,f1268])).
% 20.04/3.18 thf(f1403,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ nil @ X0) @ X1)) = X1)) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f1402])).
% 20.04/3.18 thf(f1591,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : list @ X0] : (($true = (((^[Y0 : list @ X0]: (!! @ X0 @ (^[Y1 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y1 @ Y0)) = (coinductive_LCons @ X0 @ Y1 @ (coinductive_llist_of @ X0 @ Y0)))))) @ X1)))) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1129])).
% 20.04/3.18 thf(f1592,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : list @ X0] : ((((!! @ X0 @ (^[Y0 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y0 @ X1)) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_llist_of @ X0 @ X1)))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f1591])).
% 20.04/3.18 thf(f1593,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : X0,X1 : list @ X0] : (((((^[Y0 : X0]: ((coinductive_llist_of @ X0 @ (cons @ X0 @ Y0 @ X1)) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_llist_of @ X0 @ X1)))) @ X2)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1592])).
% 20.04/3.18 thf(f1594,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : X0,X1 : list @ X0] : (((((coinductive_llist_of @ X0 @ (cons @ X0 @ X2 @ X1)) = (coinductive_LCons @ X0 @ X2 @ (coinductive_llist_of @ X0 @ X1)))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f1593])).
% 20.04/3.18 thf(f1595,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : X0,X1 : list @ X0] : ((((coinductive_llist_of @ X0 @ (cons @ X0 @ X2 @ X1))) = ((coinductive_LCons @ X0 @ X2 @ (coinductive_llist_of @ X0 @ X1))))) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f1594])).
% 20.04/3.18 thf(f1908,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : list @ X0] : (($true = (((^[Y0 : list @ X0]: (!! @ list @ X0 @ (^[Y1 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ Y0) @ (coinductive_llist_of @ X0 @ Y1)) = (coinductive_llist_of @ X0 @ (append @ X0 @ Y0 @ Y1)))))) @ X1)))) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1038])).
% 20.04/3.18 thf(f1909,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : list @ X0] : ((((!! @ list @ X0 @ (^[Y0 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X1) @ (coinductive_llist_of @ X0 @ Y0)) = (coinductive_llist_of @ X0 @ (append @ X0 @ X1 @ Y0)))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f1908])).
% 20.04/3.18 thf(f1931,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : list @ X0,X1 : list @ X0] : (((((^[Y0 : list @ X0]: ((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X1) @ (coinductive_llist_of @ X0 @ Y0)) = (coinductive_llist_of @ X0 @ (append @ X0 @ X1 @ Y0)))) @ X2)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1909])).
% 20.04/3.18 thf(f1932,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : list @ X0,X1 : list @ X0] : (((((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X1) @ (coinductive_llist_of @ X0 @ X2)) = (coinductive_llist_of @ X0 @ (append @ X0 @ X1 @ X2)))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f1931])).
% 20.04/3.18 thf(f1933,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : list @ X0,X1 : list @ X0] : ((((coinductive_lappend @ X0 @ (coinductive_llist_of @ X0 @ X1) @ (coinductive_llist_of @ X0 @ X2))) = ((coinductive_llist_of @ X0 @ (append @ X0 @ X1 @ X2))))) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f1932])).
% 20.04/3.18 thf(f1942,plain,(
% 20.04/3.18 (((coinductive_llist_of @ a @ xs)) = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_llist_of @ a @ (cons @ a @ n @ zs))))) | ~spl0_6),
% 20.04/3.18 inference(constrained_superposition,[],[f1933,f1277])).
% 20.04/3.18 thf(f1956,plain,(
% 20.04/3.18 (((coinductive_llist_of @ a @ xs)) = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ zs))))) | ~spl0_6),
% 20.04/3.18 inference(forward_demodulation,[],[f1942,f1595])).
% 20.04/3.18 thf(f1959,plain,(
% 20.04/3.18 (xs4 = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ zs))))) | (~spl0_1 | ~spl0_6)),
% 20.04/3.18 inference(forward_demodulation,[],[f1956,f1246])).
% 20.04/3.18 thf(f1963,definition,(
% 20.04/3.18 spl0_44 <=> (xs4 = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ zs)))))),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition])).
% 20.04/3.18 thf(f1964,plain,(
% 20.04/3.18 (xs4 = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ zs))))) | ~spl0_44),
% 20.04/3.18 inference(avatar_component_clause,[],[f1963])).
% 20.04/3.18 thf(f1965,plain,(
% 20.04/3.18 spl0_44 | ~spl0_1 | ~spl0_6),
% 20.04/3.18 inference(avatar_split_clause,[],[f1959,f1276,f1245,f1963])).
% 20.04/3.18 thf(f2440,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : X0] : (($true = (((^[Y0 : X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ Y0 @ Y2) @ Y1) = (coinductive_LCons @ X0 @ Y0 @ (coinductive_lappend @ X0 @ Y2 @ Y1)))))))) @ X1)))) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1153])).
% 20.04/3.18 thf(f2441,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : X0] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ Y1) @ Y0) = (coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ Y1 @ Y0)))))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2440])).
% 20.04/3.18 thf(f2445,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : X0] : (((((^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ Y1) @ Y0) = (coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ Y1 @ Y0)))))) @ X2)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f2441])).
% 20.04/3.18 thf(f2446,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : X0] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ Y0) @ X2) = (coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ Y0 @ X2)))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2445])).
% 20.04/3.18 thf(f2450,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0] : (($true = (((^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ Y0) @ X2) = (coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ Y0 @ X2)))) @ X3)))) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f2446])).
% 20.04/3.18 thf(f2451,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0] : (($true = (((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X3) @ X2) = (coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X3 @ X2)))))) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2450])).
% 20.04/3.18 thf(f2452,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0] : ((((coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X3 @ X2))) = ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X3) @ X2)))) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f2451])).
% 20.04/3.18 thf(f2458,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a))) @ xs3))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_15),
% 20.04/3.18 inference(constrained_superposition,[],[f1328,f2452])).
% 20.04/3.18 thf(f2464,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ coinductive_LNil @ a)) @ xs3)))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_15),
% 20.04/3.18 inference(forward_demodulation,[],[f2458,f2452])).
% 20.04/3.18 thf(f2468,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ (coinductive_llist_of @ a @ nil @ a))) @ xs3)))) @ (koenig916195507_paths @ a @ graph))) = $false) | ~spl0_15),
% 20.04/3.18 inference(forward_demodulation,[],[f2464,f1268])).
% 20.04/3.18 thf(f2470,definition,(
% 20.04/3.18 spl0_49 <=> (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ (coinductive_llist_of @ a @ nil @ a))) @ xs3)))) @ (koenig916195507_paths @ a @ graph))) = $false)),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition])).
% 20.04/3.18 thf(f2471,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ (coinductive_llist_of @ a @ nil @ a))) @ xs3)))) @ (koenig916195507_paths @ a @ graph))) = $false) | ~spl0_49),
% 20.04/3.18 inference(avatar_component_clause,[],[f2470])).
% 20.04/3.18 thf(f2474,plain,(
% 20.04/3.18 spl0_49 | ~spl0_15),
% 20.04/3.18 inference(avatar_split_clause,[],[f2468,f1327,f2470])).
% 20.04/3.18 thf(f2761,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((((^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y2 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y1 @ (coinductive_lappend @ X0 @ Y0 @ Y2)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y1 @ Y0) @ Y2))))))) @ X1)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f1027])).
% 20.04/3.18 thf(f2762,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y0 @ (coinductive_lappend @ X0 @ X1 @ Y1)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y0 @ X1) @ Y1))))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2761])).
% 20.04/3.18 thf(f2789,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (((((^[Y0 : coinductive_llist @ X0]: (!! @ coinductive_llist @ X0 @ (^[Y1 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ Y0 @ (coinductive_lappend @ X0 @ X1 @ Y1)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ Y0 @ X1) @ Y1))))) @ X2)) = $true)) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f2762])).
% 20.04/3.18 thf(f2790,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((((!! @ coinductive_llist @ X0 @ (^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ X2 @ (coinductive_lappend @ X0 @ X1 @ Y0)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X2 @ X1) @ Y0))))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2789])).
% 20.04/3.18 thf(f2811,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (($true = (((^[Y0 : coinductive_llist @ X0]: ((coinductive_lappend @ X0 @ X2 @ (coinductive_lappend @ X0 @ X1 @ Y0)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X2 @ X1) @ Y0))) @ X3)))) )),
% 20.04/3.18 inference(pi_proxy_clausification,[],[f2790])).
% 20.04/3.18 thf(f2812,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (((((coinductive_lappend @ X0 @ X2 @ (coinductive_lappend @ X0 @ X1 @ X3)) = (coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X2 @ X1) @ X3))) = $true)) )),
% 20.04/3.18 inference(beta-eta_normalization,[],[f2811])).
% 20.04/3.18 thf(f2813,plain,(
% 20.04/3.18 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((((coinductive_lappend @ X0 @ X2 @ (coinductive_lappend @ X0 @ X1 @ X3))) = ((coinductive_lappend @ X0 @ (coinductive_lappend @ X0 @ X2 @ X1) @ X3)))) )),
% 20.04/3.18 inference(equality_proxy_clausification,[],[f2812])).
% 20.04/3.18 thf(f2853,plain,(
% 20.04/3.18 ( ! [X0 : coinductive_llist @ a] : ((((coinductive_lappend @ a @ xs4 @ X0)) = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ n @ (coinductive_llist_of @ a @ zs)) @ X0))))) ) | ~spl0_44),
% 20.04/3.18 inference(constrained_superposition,[],[f2813,f1964])).
% 20.04/3.18 thf(f2864,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ x @ (coinductive_llist_of @ a @ nil @ a)) @ xs3))))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_49),
% 20.04/3.18 inference(constrained_superposition,[],[f2471,f2813])).
% 20.04/3.18 thf(f2872,plain,(
% 20.04/3.18 ( ! [X0 : coinductive_llist @ a] : ((((coinductive_lappend @ a @ xs4 @ X0)) = ((coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ X0)))))) ) | ~spl0_44),
% 20.04/3.18 inference(forward_demodulation,[],[f2853,f2452])).
% 20.04/3.18 thf(f2874,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ nil @ a) @ xs3)))))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_49),
% 20.04/3.18 inference(forward_demodulation,[],[f2864,f2452])).
% 20.04/3.18 thf(f2878,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ xs3))))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_49),
% 20.04/3.18 inference(forward_demodulation,[],[f2874,f1403])).
% 20.04/3.18 thf(f2881,definition,(
% 20.04/3.18 spl0_52 <=> ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ xs3))))) @ (koenig916195507_paths @ a @ graph))))),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition])).
% 20.04/3.18 thf(f2882,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ ys) @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ (coinductive_llist_of @ a @ zs) @ (coinductive_LCons @ a @ x @ xs3))))) @ (koenig916195507_paths @ a @ graph)))) | ~spl0_52),
% 20.04/3.18 inference(avatar_component_clause,[],[f2881])).
% 20.04/3.18 thf(f2883,plain,(
% 20.04/3.18 spl0_52 | ~spl0_49),
% 20.04/3.18 inference(avatar_split_clause,[],[f2878,f2470,f2881])).
% 20.04/3.18 thf(f2992,plain,(
% 20.04/3.18 ($false = ((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ (coinductive_lappend @ a @ xs4 @ (coinductive_LCons @ a @ x @ xs3))) @ (koenig916195507_paths @ a @ graph)))) | (~spl0_44 | ~spl0_52)),
% 20.04/3.18 inference(constrained_superposition,[],[f2882,f2872])).
% 20.04/3.18 thf(f2999,plain,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) = $false) | (~spl0_8 | ~spl0_44 | ~spl0_52)),
% 20.04/3.18 inference(forward_demodulation,[],[f2992,f1290])).
% 20.04/3.18 thf(f3002,definition,(
% 20.04/3.18 spl0_55 <=> (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) = $false)),
% 20.04/3.18 introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition])).
% 20.04/3.18 thf(f3004,plain,(
% 20.04/3.18 spl0_55 | ~spl0_8 | ~spl0_44 | ~spl0_52),
% 20.04/3.18 inference(avatar_split_clause,[],[f2999,f2881,f1963,f1289,f3002])).
% 20.04/3.18 thf(f3006,definition,(
% 20.04/3.18 (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) != $true) | (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ n @ xs2) @ (koenig916195507_paths @ a @ graph))) != $false) | ($false = $true)),
% 20.04/3.18 introduced(theory,[theory_tautology_sat_conflict])).
% 20.04/3.18 cnf(s1, plain, spl0_1, inference(sat_conversion,[],[f1247])).
% 20.04/3.18 cnf(s2, plain, ~spl0_2, inference(sat_conversion,[],[f1251])).
% 20.04/3.18 cnf(s6, plain, spl0_6, inference(sat_conversion,[],[f1278])).
% 20.04/3.18 cnf(s8, plain, spl0_8, inference(sat_conversion,[],[f1291])).
% 20.04/3.18 cnf(s10, plain, spl0_10, inference(sat_conversion,[],[f1300])).
% 20.04/3.18 cnf(s15, plain, spl0_15, inference(sat_conversion,[],[f1329])).
% 20.04/3.18 cnf(s42, plain, ~spl0_1 | ~spl0_6 | spl0_44, inference(sat_conversion,[],[f1965])).
% 20.04/3.18 cnf(s49, plain, ~spl0_15 | spl0_49, inference(sat_conversion,[],[f2474])).
% 20.04/3.18 cnf(s52, plain, ~spl0_49 | spl0_52, inference(sat_conversion,[],[f2883])).
% 20.04/3.18 cnf(s54, plain, ~spl0_8 | ~spl0_44 | ~spl0_52 | spl0_55, inference(sat_conversion,[],[f3004])).
% 20.04/3.18 cnf(s55, plain, spl0_2 | ~spl0_10 | ~spl0_55, inference(sat_conversion,[],[f3006])).
% 20.04/3.18 cnf(s62, plain, spl0_49, inference(rat,[],[s49,s15])).
% 20.04/3.18 cnf(s64, plain, spl0_52, inference(rat,[],[s52,s62])).
% 20.04/3.18 cnf(s73, plain, ~spl0_55, inference(rat,[],[s55,s10,s2])).
% 20.04/3.18 cnf(s74, plain, ~spl0_44, inference(rat,[],[s54,s8,s64,s73])).
% 20.04/3.18 cnf(s75, plain, ~spl0_1, inference(rat,[],[s42,s6,s74])).
% 20.04/3.18 cnf(s76, plain, $false, inference(rat,[],[s1,s75])).
% 20.04/3.18 thf(f3007,plain,(
% 20.04/3.18 $false),
% 20.04/3.18 inference(avatar_sat_refutation,[],[s76])).
% 20.04/3.18 % SZS output end Proof for theBenchmark
% 20.04/3.18 % (132201)------------------------------
% 20.04/3.18 % (132201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.18 % (132201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.18 % (132201)CaDiCaL version: 2.1.3
% 20.04/3.18 % (132201)Termination reason: Refutation
% 20.04/3.18 % (132201)Time elapsed: 0.475 s
% 20.04/3.18 % (132201)Peak memory usage: 17 MB
% 20.04/3.18 % (132201)Instructions burned: 1030 (million)
% 20.04/3.18 % (131965)Success in time 2.887 s
% 20.04/3.18 % Vampire exiting
%------------------------------------------------------------------------------