%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV024^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:37:29 AM UTC 2026
% Result : Theorem 19.81s 3.14s
% Output : Refutation 19.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV024^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n007.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 14:59:11 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.25 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.81/0.38 % (3471076)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.81/0.38 % (3471085)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2855315925:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.81/0.38 % (3471087)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.81/0.38 % (3471087)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.81/0.38 % (3471082)lrs+10_16_si=on:nwc=1.5:random_seed=532104658:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.81/0.38 % (3471086)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3193955910:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.81/0.38 % (3471081)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=280177366:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.81/0.38 % (3471083)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=544905180:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.81/0.38 % (3471084)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=2909039100: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.81/0.38 % (3471085)Instruction limit reached!
% 0.81/0.38 % (3471085)------------------------------
% 0.81/0.38 % (3471085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (3471085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (3471085)CaDiCaL version: 2.1.3
% 0.81/0.38 % (3471085)Termination reason: Instruction limit
% 0.81/0.38 % (3471085)Termination phase: Saturation
% 0.81/0.38 % (3471085)Time elapsed: 0.008 s
% 0.81/0.38 % (3471085)Peak memory usage: 12 MB
% 0.81/0.38 % (3471085)Instructions burned: 26 (million)
% 0.81/0.38 % (3471087)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=161584374:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.81/0.38 % (3471083)Instruction limit reached!
% 0.81/0.38 % (3471083)------------------------------
% 0.81/0.38 % (3471083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (3471083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (3471083)CaDiCaL version: 2.1.3
% 0.81/0.38 % (3471083)Termination reason: Instruction limit
% 0.81/0.38 % (3471083)Termination phase: Saturation
% 0.81/0.38 % (3471083)Time elapsed: 0.002 s
% 0.81/0.38 % (3471083)Peak memory usage: 11 MB
% 0.81/0.38 % (3471083)Instructions burned: 4 (million)
% 0.81/0.38 % (3471082)Instruction limit reached!
% 0.81/0.38 % (3471082)------------------------------
% 0.81/0.38 % (3471082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (3471082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (3471082)CaDiCaL version: 2.1.3
% 0.81/0.38 % (3471082)Termination reason: Instruction limit
% 0.81/0.38 % (3471082)Termination phase: Saturation
% 0.81/0.38 % (3471082)Time elapsed: 0.011 s
% 0.81/0.38 % (3471082)Peak memory usage: 12 MB
% 0.81/0.38 % (3471082)Instructions burned: 20 (million)
% 0.81/0.38 % (3471095)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2020857734:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.81/0.38 % (3471095)Instruction limit reached!
% 0.81/0.38 % (3471095)------------------------------
% 0.81/0.38 % (3471095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (3471095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (3471095)CaDiCaL version: 2.1.3
% 0.81/0.38 % (3471095)Termination reason: Instruction limit
% 0.81/0.38 % (3471095)Termination phase: Saturation
% 0.81/0.38 % (3471095)Time elapsed: 0.001 s
% 0.81/0.38 % (3471095)Peak memory usage: 11 MB
% 0.81/0.38 % (3471095)Instructions burned: 3 (million)
% 0.81/0.38 % (3471096)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4066242827:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.81/0.42 % (3471099)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1101476107:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.81/0.42 % (3471097)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.42 % (3471096)Instruction limit reached!
% 0.81/0.42 % (3471096)------------------------------
% 0.81/0.42 % (3471096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.42 % (3471096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.42 % (3471096)CaDiCaL version: 2.1.3
% 0.81/0.42 % (3471096)Termination reason: Instruction limit
% 0.81/0.42 % (3471096)Termination phase: Saturation
% 0.81/0.42 % (3471096)Time elapsed: 0.004 s
% 0.81/0.42 % (3471096)Peak memory usage: 12 MB
% 0.81/0.42 % (3471096)Instructions burned: 6 (million)
% 0.81/0.42 % (3471099)Instruction limit reached!
% 0.81/0.42 % (3471099)------------------------------
% 0.81/0.42 % (3471099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.42 % (3471099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.42 % (3471099)CaDiCaL version: 2.1.3
% 0.81/0.42 % (3471099)Termination reason: Instruction limit
% 0.81/0.42 % (3471099)Termination phase: Saturation
% 0.81/0.42 % (3471099)Time elapsed: 0.005 s
% 0.81/0.42 % (3471099)Peak memory usage: 12 MB
% 0.81/0.42 % (3471099)Instructions burned: 15 (million)
% 0.81/0.42 % (3471097)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1785095160:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.81/0.42 % (3471097)Instruction limit reached!
% 0.81/0.42 % (3471097)------------------------------
% 0.81/0.42 % (3471097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.42 % (3471097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.42 % (3471097)CaDiCaL version: 2.1.3
% 0.81/0.42 % (3471097)Termination reason: Instruction limit
% 0.81/0.42 % (3471097)Termination phase: Saturation
% 0.81/0.42 % (3471097)Time elapsed: 0.005 s
% 0.81/0.42 % (3471097)Peak memory usage: 12 MB
% 0.81/0.42 % (3471097)Instructions burned: 9 (million)
% 0.81/0.42 % (3471086)Instruction limit reached!
% 0.81/0.42 % (3471086)------------------------------
% 0.81/0.42 % (3471086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.42 % (3471086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.42 % (3471086)CaDiCaL version: 2.1.3
% 0.81/0.42 % (3471086)Termination reason: Instruction limit
% 0.81/0.42 % (3471086)Termination phase: Saturation
% 0.81/0.42 % (3471086)Time elapsed: 0.038 s
% 0.81/0.42 % (3471086)Peak memory usage: 13 MB
% 0.81/0.42 % (3471086)Instructions burned: 78 (million)
% 0.81/0.42 % (3471103)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=3338348664:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.81/0.42 % (3471102)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.81/0.42 % (3471102)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.42 % (3471102)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1836058850: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.81/0.42 % (3471106)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.81/0.42 % (3471105)lrs+10_1_si=on:cs=on:random_seed=2985442038:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.81/0.42 % (3471106)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=1936310939:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.81/0.42 % (3471081)Instruction limit reached!
% 0.81/0.42 % (3471081)------------------------------
% 0.81/0.42 % (3471081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.42 % (3471081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471081)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471081)Termination reason: Instruction limit
% 0.81/0.46 % (3471081)Termination phase: Saturation
% 0.81/0.46 % (3471081)Time elapsed: 0.058 s
% 0.81/0.46 % (3471081)Peak memory usage: 13 MB
% 0.81/0.46 % (3471081)Instructions burned: 88 (million)
% 0.81/0.46 % (3471106)Instruction limit reached!
% 0.81/0.46 % (3471106)------------------------------
% 0.81/0.46 % (3471106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471106)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471106)Termination reason: Instruction limit
% 0.81/0.46 % (3471106)Termination phase: Saturation
% 0.81/0.46 % (3471106)Time elapsed: 0.002 s
% 0.81/0.46 % (3471106)Peak memory usage: 11 MB
% 0.81/0.46 % (3471105)Instruction limit reached!
% 0.81/0.46 % (3471105)------------------------------
% 0.81/0.46 % (3471105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471106)Instructions burned: 3 (million)
% 0.81/0.46 % (3471105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471105)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471105)Termination reason: Instruction limit
% 0.81/0.46 % (3471105)Termination phase: Saturation
% 0.81/0.46 % (3471105)Time elapsed: 0.004 s
% 0.81/0.46 % (3471105)Peak memory usage: 12 MB
% 0.81/0.46 % (3471105)Instructions burned: 8 (million)
% 0.81/0.46 % (3471103)Instruction limit reached!
% 0.81/0.46 % (3471103)------------------------------
% 0.81/0.46 % (3471103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471103)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471103)Termination reason: Instruction limit
% 0.81/0.46 % (3471103)Termination phase: Saturation
% 0.81/0.46 % (3471103)Time elapsed: 0.022 s
% 0.81/0.46 % (3471103)Peak memory usage: 12 MB
% 0.81/0.46 % (3471103)Instructions burned: 89 (million)
% 0.81/0.46 % (3471102)Instruction limit reached!
% 0.81/0.46 % (3471102)------------------------------
% 0.81/0.46 % (3471102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471102)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471102)Termination reason: Instruction limit
% 0.81/0.46 % (3471102)Termination phase: Saturation
% 0.81/0.46 % (3471102)Time elapsed: 0.017 s
% 0.81/0.46 % (3471102)Peak memory usage: 12 MB
% 0.81/0.46 % (3471102)Instructions burned: 31 (million)
% 0.81/0.46 % (3471114)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3390525563:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.81/0.46 % (3471112)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1067203879:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.81/0.46 % (3471114)Instruction limit reached!
% 0.81/0.46 % (3471114)------------------------------
% 0.81/0.46 % (3471114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471114)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471114)Termination reason: Instruction limit
% 0.81/0.46 % (3471114)Termination phase: Saturation
% 0.81/0.46 % (3471114)Time elapsed: 0.004 s
% 0.81/0.46 % (3471114)Peak memory usage: 12 MB
% 0.81/0.46 % (3471114)Instructions burned: 14 (million)
% 0.81/0.46 % (3471113)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=578517240:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.81/0.46 % (3471087)Instruction limit reached!
% 0.81/0.46 % (3471087)------------------------------
% 0.81/0.46 % (3471087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.46 % (3471087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.46 % (3471087)CaDiCaL version: 2.1.3
% 0.81/0.46 % (3471087)Termination reason: Instruction limit
% 0.81/0.46 % (3471087)Termination phase: Saturation
% 0.81/0.46 % (3471087)Time elapsed: 0.081 s
% 0.81/0.46 % (3471087)Peak memory usage: 12 MB
% 0.81/0.46 % (3471087)Instructions burned: 157 (million)
% 0.81/0.46 % (3471115)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3145645182:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.54/0.53 % (3471111)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=6134646:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.54/0.53 % (3471119)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2579943865:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.54/0.53 % (3471113)Instruction limit reached!
% 1.54/0.53 % (3471113)------------------------------
% 1.54/0.53 % (3471113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (3471113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (3471113)CaDiCaL version: 2.1.3
% 1.54/0.53 % (3471113)Termination reason: Instruction limit
% 1.54/0.53 % (3471113)Termination phase: Saturation
% 1.54/0.53 % (3471113)Time elapsed: 0.014 s
% 1.54/0.53 % (3471113)Peak memory usage: 12 MB
% 1.54/0.53 % (3471113)Instructions burned: 26 (million)
% 1.54/0.53 % (3471119)Instruction limit reached!
% 1.54/0.53 % (3471119)------------------------------
% 1.54/0.53 % (3471119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (3471119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (3471119)CaDiCaL version: 2.1.3
% 1.54/0.53 % (3471119)Termination reason: Instruction limit
% 1.54/0.53 % (3471119)Termination phase: Saturation
% 1.54/0.53 % (3471119)Time elapsed: 0.004 s
% 1.54/0.53 % (3471119)Peak memory usage: 12 MB
% 1.54/0.53 % (3471119)Instructions burned: 14 (million)
% 1.54/0.53 % (3471120)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2336577965: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.54/0.53 % (3471120)Instruction limit reached!
% 1.54/0.53 % (3471120)------------------------------
% 1.54/0.53 % (3471120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (3471120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (3471120)CaDiCaL version: 2.1.3
% 1.54/0.53 % (3471120)Termination reason: Instruction limit
% 1.54/0.53 % (3471120)Termination phase: Saturation
% 1.54/0.53 % (3471120)Time elapsed: 0.002 s
% 1.54/0.53 % (3471120)Peak memory usage: 11 MB
% 1.54/0.53 % (3471120)Instructions burned: 3 (million)
% 1.54/0.53 % (3471125)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1612819787:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.54/0.53 % (3471124)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=167894840:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.54/0.53 % (3471125)Instruction limit reached!
% 1.54/0.53 % (3471125)------------------------------
% 1.54/0.53 % (3471125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (3471125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (3471125)CaDiCaL version: 2.1.3
% 1.54/0.53 % (3471125)Termination reason: Instruction limit
% 1.54/0.53 % (3471125)Termination phase: Saturation
% 1.54/0.53 % (3471125)Time elapsed: 0.007 s
% 1.54/0.53 % (3471125)Peak memory usage: 11 MB
% 1.54/0.53 % (3471125)Instructions burned: 24 (million)
% 1.54/0.53 % (3471127)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2728225726:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.54/0.53 % (3471130)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.54/0.53 % (3471130)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.54/0.53 % (3471130)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=2457575322:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.54/0.53 % (3471124)Instruction limit reached!
% 1.54/0.53 % (3471124)------------------------------
% 1.54/0.53 % (3471124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (3471124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.57 % (3471124)CaDiCaL version: 2.1.3
% 1.54/0.57 % (3471124)Termination reason: Instruction limit
% 1.54/0.57 % (3471124)Termination phase: Saturation
% 1.54/0.57 % (3471124)Time elapsed: 0.014 s
% 1.54/0.57 % (3471124)Peak memory usage: 12 MB
% 1.54/0.57 % (3471124)Instructions burned: 28 (million)
% 1.54/0.57 % (3471111)Instruction limit reached!
% 1.54/0.57 % (3471111)------------------------------
% 1.54/0.57 % (3471111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.57 % (3471111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.57 % (3471111)CaDiCaL version: 2.1.3
% 1.54/0.57 % (3471111)Termination reason: Instruction limit
% 1.54/0.57 % (3471111)Termination phase: Saturation
% 1.54/0.57 % (3471111)Time elapsed: 0.035 s
% 1.54/0.57 % (3471111)Peak memory usage: 12 MB
% 1.54/0.57 % (3471111)Instructions burned: 38 (million)
% 1.54/0.57 % (3471130)Instruction limit reached!
% 1.54/0.57 % (3471130)------------------------------
% 1.54/0.57 % (3471130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.57 % (3471130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.57 % (3471130)CaDiCaL version: 2.1.3
% 1.54/0.57 % (3471130)Termination reason: Instruction limit
% 1.54/0.57 % (3471130)Termination phase: Saturation
% 1.54/0.57 % (3471130)Time elapsed: 0.004 s
% 1.54/0.57 % (3471130)Peak memory usage: 12 MB
% 1.54/0.57 % (3471130)Instructions burned: 14 (million)
% 1.54/0.57 % (3471135)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1675153484:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.54/0.57 % (3471133)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.54/0.57 % (3471135)Instruction limit reached!
% 1.54/0.57 % (3471135)------------------------------
% 1.54/0.57 % (3471135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.57 % (3471135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.57 % (3471135)CaDiCaL version: 2.1.3
% 1.54/0.57 % (3471135)Termination reason: Instruction limit
% 1.54/0.57 % (3471135)Termination phase: Saturation
% 1.54/0.57 % (3471135)Time elapsed: 0.003 s
% 1.54/0.57 % (3471135)Peak memory usage: 12 MB
% 1.54/0.57 % (3471135)Instructions burned: 10 (million)
% 1.54/0.57 % (3471133)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=1928234587:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.54/0.57 % (3471134)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=2746628408:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.54/0.57 % (3471133)Instruction limit reached!
% 1.54/0.57 % (3471133)------------------------------
% 1.54/0.57 % (3471133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.57 % (3471133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.57 % (3471133)CaDiCaL version: 2.1.3
% 1.54/0.57 % (3471133)Termination reason: Instruction limit
% 1.54/0.57 % (3471133)Termination phase: Saturation
% 1.54/0.57 % (3471133)Time elapsed: 0.005 s
% 1.54/0.57 % (3471133)Peak memory usage: 12 MB
% 1.54/0.57 % (3471133)Instructions burned: 9 (million)
% 1.54/0.58 % (3471137)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3995709622:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.54/0.58 % (3471137)Instruction limit reached!
% 1.54/0.58 % (3471137)------------------------------
% 1.54/0.58 % (3471137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.58 % (3471137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.58 % (3471137)CaDiCaL version: 2.1.3
% 1.54/0.58 % (3471137)Termination reason: Instruction limit
% 1.54/0.58 % (3471137)Termination phase: Saturation
% 1.54/0.58 % (3471137)Time elapsed: 0.006 s
% 1.54/0.58 % (3471137)Peak memory usage: 11 MB
% 1.54/0.58 % (3471137)Instructions burned: 27 (million)
% 1.54/0.58 % (3471134)Instruction limit reached!
% 1.54/0.58 % (3471134)------------------------------
% 1.54/0.58 % (3471134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.58 % (3471134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.58 % (3471134)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471134)Termination reason: Instruction limit
% 2.51/0.65 % (3471134)Termination phase: Saturation
% 2.51/0.65 % (3471134)Time elapsed: 0.016 s
% 2.51/0.65 % (3471134)Peak memory usage: 12 MB
% 2.51/0.65 % (3471134)Instructions burned: 33 (million)
% 2.51/0.65 % (3471127)Instruction limit reached!
% 2.51/0.65 % (3471127)------------------------------
% 2.51/0.65 % (3471127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (3471127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (3471127)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471127)Termination reason: Instruction limit
% 2.51/0.65 % (3471127)Termination phase: Saturation
% 2.51/0.65 % (3471127)Time elapsed: 0.045 s
% 2.51/0.65 % (3471127)Peak memory usage: 12 MB
% 2.51/0.65 % (3471127)Instructions burned: 60 (million)
% 2.51/0.65 % (3471140)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2153824454:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.51/0.65 % (3471142)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=886974428:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.51/0.65 % (3471144)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=487997235:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.51/0.65 % (3471140)Instruction limit reached!
% 2.51/0.65 % (3471140)------------------------------
% 2.51/0.65 % (3471140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (3471140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (3471140)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471140)Termination reason: Instruction limit
% 2.51/0.65 % (3471140)Termination phase: Saturation
% 2.51/0.65 % (3471140)Time elapsed: 0.011 s
% 2.51/0.65 % (3471140)Peak memory usage: 12 MB
% 2.51/0.65 % (3471140)Instructions burned: 21 (million)
% 2.51/0.65 % (3471143)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2357726919:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.51/0.65 % (3471149)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=615235793:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.51/0.65 % (3471112)Instruction limit reached!
% 2.51/0.65 % (3471112)------------------------------
% 2.51/0.65 % (3471112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (3471112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (3471112)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471112)Termination reason: Instruction limit
% 2.51/0.65 % (3471112)Termination phase: Saturation
% 2.51/0.65 % (3471112)Time elapsed: 0.131 s
% 2.51/0.65 % (3471112)Peak memory usage: 13 MB
% 2.51/0.65 % (3471112)Instructions burned: 249 (million)
% 2.51/0.65 % (3471149)Instruction limit reached!
% 2.51/0.65 % (3471149)------------------------------
% 2.51/0.65 % (3471149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (3471149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (3471149)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471149)Termination reason: Instruction limit
% 2.51/0.65 % (3471149)Termination phase: Saturation
% 2.51/0.65 % (3471149)Time elapsed: 0.021 s
% 2.51/0.65 % (3471149)Peak memory usage: 12 MB
% 2.51/0.65 % (3471149)Instructions burned: 42 (million)
% 2.51/0.65 % (3471151)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.51/0.65 % (3471151)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4169654989:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.51/0.65 % (3471151)Instruction limit reached!
% 2.51/0.65 % (3471151)------------------------------
% 2.51/0.65 % (3471151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (3471151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (3471151)CaDiCaL version: 2.1.3
% 2.51/0.65 % (3471151)Termination reason: Instruction limit
% 2.51/0.65 % (3471151)Termination phase: Saturation
% 2.51/0.65 % (3471151)Time elapsed: 0.004 s
% 2.51/0.65 % (3471151)Peak memory usage: 12 MB
% 2.51/0.65 % (3471151)Instructions burned: 7 (million)
% 2.51/0.65 % (3471144)Instruction limit reached!
% 2.51/0.65 % (3471144)------------------------------
% 2.51/0.65 % (3471144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.76 % (3471144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.76 % (3471144)CaDiCaL version: 2.1.3
% 2.61/0.76 % (3471144)Termination reason: Instruction limit
% 2.61/0.76 % (3471144)Termination phase: Saturation
% 2.61/0.76 % (3471144)Time elapsed: 0.055 s
% 2.61/0.76 % (3471144)Peak memory usage: 13 MB
% 2.61/0.76 % (3471144)Instructions burned: 194 (million)
% 2.61/0.76 % (3471152)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2422372832:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.61/0.76 % (3471155)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.61/0.76 % (3471155)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3277407701: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.61/0.76 % (3471155)Instruction limit reached!
% 2.61/0.76 % (3471155)------------------------------
% 2.61/0.76 % (3471155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.76 % (3471155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.76 % (3471155)CaDiCaL version: 2.1.3
% 2.61/0.76 % (3471155)Termination reason: Instruction limit
% 2.61/0.76 % (3471155)Termination phase: Saturation
% 2.61/0.76 % (3471155)Time elapsed: 0.002 s
% 2.61/0.76 % (3471155)Peak memory usage: 12 MB
% 2.61/0.76 % (3471155)Instructions burned: 7 (million)
% 2.61/0.76 % (3471115)Instruction limit reached!
% 2.61/0.76 % (3471115)------------------------------
% 2.61/0.76 % (3471115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.76 % (3471115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.76 % (3471115)CaDiCaL version: 2.1.3
% 2.61/0.76 % (3471115)Termination reason: Instruction limit
% 2.61/0.76 % (3471115)Termination phase: Saturation
% 2.61/0.76 % (3471115)Time elapsed: 0.162 s
% 2.61/0.76 % (3471115)Peak memory usage: 13 MB
% 2.61/0.76 % (3471115)Instructions burned: 331 (million)
% 2.61/0.76 % (3471154)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=1525233934: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.61/0.76 % (3471143)Instruction limit reached!
% 2.61/0.76 % (3471143)------------------------------
% 2.61/0.76 % (3471143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.76 % (3471143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.76 % (3471143)CaDiCaL version: 2.1.3
% 2.61/0.76 % (3471143)Termination reason: Instruction limit
% 2.61/0.76 % (3471143)Termination phase: Saturation
% 2.61/0.76 % (3471143)Time elapsed: 0.076 s
% 2.61/0.76 % (3471143)Peak memory usage: 13 MB
% 2.61/0.76 % (3471143)Instructions burned: 144 (million)
% 2.61/0.76 % (3471158)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3626580269:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.61/0.76 % (3471158)Instruction limit reached!
% 2.61/0.76 % (3471158)------------------------------
% 2.61/0.76 % (3471158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.61/0.76 % (3471158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.61/0.76 % (3471158)CaDiCaL version: 2.1.3
% 2.61/0.76 % (3471158)Termination reason: Instruction limit
% 2.61/0.76 % (3471158)Termination phase: Saturation
% 2.61/0.76 % (3471158)Time elapsed: 0.006 s
% 2.61/0.76 % (3471158)Peak memory usage: 12 MB
% 2.61/0.76 % (3471158)Instructions burned: 26 (million)
% 2.61/0.76 % (3471160)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1042238730:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.61/0.76 % (3471163)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=1136690440: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)
% 2.61/0.76 % (3471162)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=1587144226:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.50/0.82 % (3471160)Instruction limit reached!
% 3.50/0.82 % (3471160)------------------------------
% 3.50/0.82 % (3471160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/0.82 % (3471160)CaDiCaL version: 2.1.3
% 3.50/0.82 % (3471160)Termination reason: Instruction limit
% 3.50/0.82 % (3471160)Termination phase: Saturation
% 3.50/0.82 % (3471160)Time elapsed: 0.010 s
% 3.50/0.82 % (3471160)Peak memory usage: 12 MB
% 3.50/0.82 % (3471160)Instructions burned: 19 (million)
% 3.50/0.82 % (3471084)Instruction limit reached!
% 3.50/0.82 % (3471084)------------------------------
% 3.50/0.82 % (3471084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/0.82 % (3471084)CaDiCaL version: 2.1.3
% 3.50/0.82 % (3471084)Termination reason: Instruction limit
% 3.50/0.82 % (3471084)Termination phase: Saturation
% 3.50/0.82 % (3471084)Time elapsed: 0.300 s
% 3.50/0.82 % (3471084)Peak memory usage: 13 MB
% 3.50/0.82 % (3471084)Instructions burned: 636 (million)
% 3.50/0.82 % (3471167)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=3269526501: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.50/0.82 % (3471169)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3971233947:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.50/0.82 % (3471167)Instruction limit reached!
% 3.50/0.82 % (3471167)------------------------------
% 3.50/0.82 % (3471167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/0.82 % (3471167)CaDiCaL version: 2.1.3
% 3.50/0.82 % (3471167)Termination reason: Instruction limit
% 3.50/0.82 % (3471167)Termination phase: Saturation
% 3.50/0.82 % (3471167)Time elapsed: 0.024 s
% 3.50/0.82 % (3471167)Peak memory usage: 12 MB
% 3.50/0.82 % (3471167)Instructions burned: 47 (million)
% 3.50/0.82 % (3471152)Instruction limit reached!
% 3.50/0.82 % (3471152)------------------------------
% 3.50/0.82 % (3471152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/0.82 % (3471152)CaDiCaL version: 2.1.3
% 3.50/0.82 % (3471152)Termination reason: Instruction limit
% 3.50/0.82 % (3471152)Termination phase: Saturation
% 3.50/0.82 % (3471152)Time elapsed: 0.094 s
% 3.50/0.82 % (3471152)Peak memory usage: 13 MB
% 3.50/0.82 % (3471152)Instructions burned: 182 (million)
% 3.50/0.82 % (3471154)Instruction limit reached!
% 3.50/0.82 % (3471154)------------------------------
% 3.50/0.82 % (3471154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/0.82 % (3471154)CaDiCaL version: 2.1.3
% 3.50/0.82 % (3471154)Termination reason: Instruction limit
% 3.50/0.82 % (3471154)Termination phase: Saturation
% 3.50/0.82 % (3471154)Time elapsed: 0.087 s
% 3.50/0.82 % (3471154)Peak memory usage: 13 MB
% 3.50/0.82 % (3471154)Instructions burned: 171 (million)
% 3.50/0.82 % (3471171)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3209560856: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.50/0.82 % (3471172)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.50/0.82 % (3471172)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1883147345:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.50/0.82 % (3471173)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1248122469:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.50/0.82 % (3471171)Instruction limit reached!
% 3.50/0.82 % (3471171)------------------------------
% 3.50/0.82 % (3471171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.50/0.82 % (3471171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471171)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471171)Termination reason: Instruction limit
% 4.06/0.96 % (3471171)Termination phase: Saturation
% 4.06/0.96 % (3471171)Time elapsed: 0.013 s
% 4.06/0.96 % (3471171)Peak memory usage: 12 MB
% 4.06/0.96 % (3471171)Instructions burned: 25 (million)
% 4.06/0.96 % (3471173)Instruction limit reached!
% 4.06/0.96 % (3471173)------------------------------
% 4.06/0.96 % (3471173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471173)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471173)Termination reason: Instruction limit
% 4.06/0.96 % (3471173)Termination phase: Saturation
% 4.06/0.96 % (3471173)Time elapsed: 0.008 s
% 4.06/0.96 % (3471173)Peak memory usage: 12 MB
% 4.06/0.96 % (3471173)Instructions burned: 15 (million)
% 4.06/0.96 % (3471177)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=1043712346:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 4.06/0.96 % (3471178)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2045361030:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 4.06/0.96 % (3471178)Instruction limit reached!
% 4.06/0.96 % (3471178)------------------------------
% 4.06/0.96 % (3471178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471178)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471178)Termination reason: Instruction limit
% 4.06/0.96 % (3471178)Termination phase: Saturation
% 4.06/0.96 % (3471178)Time elapsed: 0.026 s
% 4.06/0.96 % (3471178)Peak memory usage: 12 MB
% 4.06/0.96 % (3471178)Instructions burned: 53 (million)
% 4.06/0.96 % (3471177)Instruction limit reached!
% 4.06/0.96 % (3471177)------------------------------
% 4.06/0.96 % (3471177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471177)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471177)Termination reason: Instruction limit
% 4.06/0.96 % (3471177)Termination phase: Saturation
% 4.06/0.96 % (3471177)Time elapsed: 0.035 s
% 4.06/0.96 % (3471177)Peak memory usage: 13 MB
% 4.06/0.96 % (3471177)Instructions burned: 66 (million)
% 4.06/0.96 % (3471181)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1412235639:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 4.06/0.96 % (3471182)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1565799133:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 4.06/0.96 % (3471172)Instruction limit reached!
% 4.06/0.96 % (3471172)------------------------------
% 4.06/0.96 % (3471172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471172)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471172)Termination reason: Instruction limit
% 4.06/0.96 % (3471172)Termination phase: Saturation
% 4.06/0.96 % (3471172)Time elapsed: 0.088 s
% 4.06/0.96 % (3471172)Peak memory usage: 12 MB
% 4.06/0.96 % (3471172)Instructions burned: 201 (million)
% 4.06/0.96 % (3471181)Instruction limit reached!
% 4.06/0.96 % (3471181)------------------------------
% 4.06/0.96 % (3471181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.06/0.96 % (3471181)CaDiCaL version: 2.1.3
% 4.06/0.96 % (3471181)Termination reason: Instruction limit
% 4.06/0.96 % (3471181)Termination phase: Saturation
% 4.06/0.96 % (3471181)Time elapsed: 0.016 s
% 4.06/0.96 % (3471181)Peak memory usage: 12 MB
% 4.06/0.96 % (3471181)Instructions burned: 31 (million)
% 4.06/0.96 % (3471185)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=463602632:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 4.06/0.96 % (3471163)Instruction limit reached!
% 4.06/0.96 % (3471163)------------------------------
% 4.06/0.96 % (3471163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.06/0.96 % (3471163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471163)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471163)Termination reason: Instruction limit
% 5.56/1.08 % (3471163)Termination phase: Saturation
% 5.56/1.08 % (3471163)Time elapsed: 0.186 s
% 5.56/1.08 % (3471163)Peak memory usage: 12 MB
% 5.56/1.08 % (3471163)Instructions burned: 855 (million)
% 5.56/1.08 % (3471162)Instruction limit reached!
% 5.56/1.08 % (3471162)------------------------------
% 5.56/1.08 % (3471162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.08 % (3471162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471162)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471162)Termination reason: Instruction limit
% 5.56/1.08 % (3471162)Termination phase: Saturation
% 5.56/1.08 % (3471162)Time elapsed: 0.183 s
% 5.56/1.08 % (3471162)Peak memory usage: 12 MB
% 5.56/1.08 % (3471162)Instructions burned: 317 (million)
% 5.56/1.08 % (3471188)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.56/1.08 % (3471186)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3936394402:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.56/1.08 % (3471188)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=385591099:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.56/1.08 % (3471185)Instruction limit reached!
% 5.56/1.08 % (3471185)------------------------------
% 5.56/1.08 % (3471185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.08 % (3471185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471185)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471185)Termination reason: Instruction limit
% 5.56/1.08 % (3471185)Termination phase: Saturation
% 5.56/1.08 % (3471185)Time elapsed: 0.017 s
% 5.56/1.08 % (3471185)Peak memory usage: 12 MB
% 5.56/1.08 % (3471185)Instructions burned: 35 (million)
% 5.56/1.08 % (3471189)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3406705218:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.56/1.08 % (3471192)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2947668492:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.56/1.08 % (3471182)Instruction limit reached!
% 5.56/1.08 % (3471182)------------------------------
% 5.56/1.08 % (3471182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.08 % (3471182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471182)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471182)Termination reason: Instruction limit
% 5.56/1.08 % (3471182)Termination phase: Saturation
% 5.56/1.08 % (3471182)Time elapsed: 0.069 s
% 5.56/1.08 % (3471182)Peak memory usage: 12 MB
% 5.56/1.08 % (3471182)Instructions burned: 138 (million)
% 5.56/1.08 % (3471186)Instruction limit reached!
% 5.56/1.08 % (3471186)------------------------------
% 5.56/1.08 % (3471186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.08 % (3471186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471186)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471186)Termination reason: Instruction limit
% 5.56/1.08 % (3471186)Termination phase: Saturation
% 5.56/1.08 % (3471186)Time elapsed: 0.036 s
% 5.56/1.08 % (3471186)Peak memory usage: 12 MB
% 5.56/1.08 % (3471186)Instructions burned: 68 (million)
% 5.56/1.08 % (3471188)Instruction limit reached!
% 5.56/1.08 % (3471188)------------------------------
% 5.56/1.08 % (3471188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.08 % (3471188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.08 % (3471188)CaDiCaL version: 2.1.3
% 5.56/1.08 % (3471188)Termination reason: Instruction limit
% 5.56/1.08 % (3471188)Termination phase: Saturation
% 5.56/1.08 % (3471188)Time elapsed: 0.043 s
% 5.56/1.08 % (3471188)Peak memory usage: 13 MB
% 5.56/1.08 % (3471188)Instructions burned: 181 (million)
% 5.56/1.08 % (3471195)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=831394769:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.56/1.08 % (3471197)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4177901717:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.56/1.08 % (3471196)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=958179867:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.96/1.16 % (3471192)Instruction limit reached!
% 5.96/1.16 % (3471192)------------------------------
% 5.96/1.16 % (3471192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471192)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471192)Termination reason: Instruction limit
% 5.96/1.16 % (3471192)Termination phase: Saturation
% 5.96/1.16 % (3471192)Time elapsed: 0.052 s
% 5.96/1.16 % (3471192)Peak memory usage: 12 MB
% 5.96/1.16 % (3471192)Instructions burned: 98 (million)
% 5.96/1.16 % (3471169)Instruction limit reached!
% 5.96/1.16 % (3471169)------------------------------
% 5.96/1.16 % (3471169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471169)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471169)Termination reason: Instruction limit
% 5.96/1.16 % (3471169)Termination phase: Saturation
% 5.96/1.16 % (3471169)Time elapsed: 0.244 s
% 5.96/1.16 % (3471169)Peak memory usage: 14 MB
% 5.96/1.16 % (3471169)Instructions burned: 482 (million)
% 5.96/1.16 % (3471201)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2768167770:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.96/1.16 % (3471202)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2685926574:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 5.96/1.16 % (3471202)Instruction limit reached!
% 5.96/1.16 % (3471202)------------------------------
% 5.96/1.16 % (3471202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471202)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471202)Termination reason: Instruction limit
% 5.96/1.16 % (3471202)Termination phase: Saturation
% 5.96/1.16 % (3471202)Time elapsed: 0.021 s
% 5.96/1.16 % (3471202)Peak memory usage: 12 MB
% 5.96/1.16 % (3471202)Instructions burned: 44 (million)
% 5.96/1.16 % (3471205)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2909347136:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 5.96/1.16 % (3471201)Instruction limit reached!
% 5.96/1.16 % (3471201)------------------------------
% 5.96/1.16 % (3471201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471201)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471201)Termination reason: Instruction limit
% 5.96/1.16 % (3471201)Termination phase: Saturation
% 5.96/1.16 % (3471201)Time elapsed: 0.067 s
% 5.96/1.16 % (3471201)Peak memory usage: 13 MB
% 5.96/1.16 % (3471201)Instructions burned: 131 (million)
% 5.96/1.16 % (3471189)Instruction limit reached!
% 5.96/1.16 % (3471189)------------------------------
% 5.96/1.16 % (3471189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471189)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471189)Termination reason: Instruction limit
% 5.96/1.16 % (3471189)Termination phase: Saturation
% 5.96/1.16 % (3471189)Time elapsed: 0.146 s
% 5.96/1.16 % (3471189)Peak memory usage: 13 MB
% 5.96/1.16 % (3471189)Instructions burned: 247 (million)
% 5.96/1.16 % (3471197)Instruction limit reached!
% 5.96/1.16 % (3471197)------------------------------
% 5.96/1.16 % (3471197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.96/1.16 % (3471197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.96/1.16 % (3471197)CaDiCaL version: 2.1.3
% 5.96/1.16 % (3471197)Termination reason: Instruction limit
% 5.96/1.16 % (3471197)Termination phase: Saturation
% 5.96/1.16 % (3471197)Time elapsed: 0.120 s
% 5.96/1.16 % (3471197)Peak memory usage: 14 MB
% 5.96/1.16 % (3471197)Instructions burned: 516 (million)
% 5.96/1.16 % (3471207)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=64021154:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.96/1.16 % (3471209)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=3235864530:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.96/1.16 % (3471208)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1587196087:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 6.33/1.23 % (3471209)Instruction limit reached!
% 6.33/1.23 % (3471209)------------------------------
% 6.33/1.23 % (3471209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.23 % (3471209)CaDiCaL version: 2.1.3
% 6.33/1.23 % (3471209)Termination reason: Instruction limit
% 6.33/1.23 % (3471209)Termination phase: Saturation
% 6.33/1.23 % (3471209)Time elapsed: 0.017 s
% 6.33/1.23 % (3471209)Peak memory usage: 12 MB
% 6.33/1.23 % (3471209)Instructions burned: 65 (million)
% 6.33/1.23 % (3471213)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=206061406: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.33/1.23 % (3471208)Instruction limit reached!
% 6.33/1.23 % (3471208)------------------------------
% 6.33/1.23 % (3471208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.23 % (3471208)CaDiCaL version: 2.1.3
% 6.33/1.23 % (3471208)Termination reason: Instruction limit
% 6.33/1.23 % (3471208)Termination phase: Saturation
% 6.33/1.23 % (3471208)Time elapsed: 0.051 s
% 6.33/1.23 % (3471208)Peak memory usage: 12 MB
% 6.33/1.23 % (3471208)Instructions burned: 102 (million)
% 6.33/1.23 % (3471213)Instruction limit reached!
% 6.33/1.23 % (3471213)------------------------------
% 6.33/1.23 % (3471213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.23 % (3471213)CaDiCaL version: 2.1.3
% 6.33/1.23 % (3471213)Termination reason: Instruction limit
% 6.33/1.23 % (3471213)Termination phase: Saturation
% 6.33/1.23 % (3471213)Time elapsed: 0.027 s
% 6.33/1.23 % (3471213)Peak memory usage: 13 MB
% 6.33/1.23 % (3471213)Instructions burned: 105 (million)
% 6.33/1.23 % (3471215)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=3498444686: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.33/1.23 % (3471215)Refutation not found, incomplete strategy
% 6.33/1.23 % (3471215)------------------------------
% 6.33/1.23 % (3471215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.23 % (3471215)CaDiCaL version: 2.1.3
% 6.33/1.23 % (3471215)Termination reason: Refutation not found, incomplete strategy
% 6.33/1.23 % (3471215)Time elapsed: 0.006 s
% 6.33/1.23 % (3471215)Peak memory usage: 13 MB
% 6.33/1.23 % (3471215)Instructions burned: 18 (million)
% 6.33/1.23 % (3471215)------------------------------
% 6.33/1.23 % (3471215)------------------------------
% 6.33/1.23 % (3471216)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1673908064:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.33/1.23 % (3471218)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=436382739:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.33/1.23 % (3471205)Refutation not found, incomplete strategy
% 6.33/1.23 % (3471205)------------------------------
% 6.33/1.23 % (3471205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.23 % (3471205)CaDiCaL version: 2.1.3
% 6.33/1.23 % (3471205)Termination reason: Refutation not found, incomplete strategy
% 6.33/1.23 % (3471205)Time elapsed: 0.164 s
% 6.33/1.23 % (3471205)Peak memory usage: 14 MB
% 6.33/1.23 % (3471205)Instructions burned: 338 (million)
% 6.33/1.23 % (3471205)------------------------------
% 6.33/1.23 % (3471205)------------------------------
% 6.33/1.23 % (3471142)Instruction limit reached!
% 6.33/1.23 % (3471142)------------------------------
% 6.33/1.23 % (3471142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.33/1.23 % (3471142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471142)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471142)Termination reason: Instruction limit
% 6.82/1.36 % (3471142)Termination phase: Saturation
% 6.82/1.36 % (3471142)Time elapsed: 0.615 s
% 6.82/1.36 % (3471142)Peak memory usage: 14 MB
% 6.82/1.36 % (3471142)Instructions burned: 1242 (million)
% 6.82/1.36 % (3471195)Instruction limit reached!
% 6.82/1.36 % (3471195)------------------------------
% 6.82/1.36 % (3471195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471195)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471195)Termination reason: Instruction limit
% 6.82/1.36 % (3471195)Termination phase: Saturation
% 6.82/1.36 % (3471195)Time elapsed: 0.284 s
% 6.82/1.36 % (3471195)Peak memory usage: 13 MB
% 6.82/1.36 % (3471195)Instructions burned: 427 (million)
% 6.82/1.36 % (3471221)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=2276634202:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 6.82/1.36 % (3471222)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2812777550:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.82/1.36 % (3471221)Instruction limit reached!
% 6.82/1.36 % (3471221)------------------------------
% 6.82/1.36 % (3471221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471221)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471223)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=260953186:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.82/1.36 % (3471221)Termination reason: Instruction limit
% 6.82/1.36 % (3471221)Termination phase: Saturation
% 6.82/1.36 % (3471221)Time elapsed: 0.017 s
% 6.82/1.36 % (3471221)Peak memory usage: 12 MB
% 6.82/1.36 % (3471221)Instructions burned: 34 (million)
% 6.82/1.36 % (3471227)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=429221175:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.82/1.36 % (3471222)Instruction limit reached!
% 6.82/1.36 % (3471222)------------------------------
% 6.82/1.36 % (3471222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471222)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471222)Termination reason: Instruction limit
% 6.82/1.36 % (3471222)Termination phase: Saturation
% 6.82/1.36 % (3471222)Time elapsed: 0.047 s
% 6.82/1.36 % (3471222)Peak memory usage: 12 MB
% 6.82/1.36 % (3471222)Instructions burned: 92 (million)
% 6.82/1.36 % (3471227)Instruction limit reached!
% 6.82/1.36 % (3471227)------------------------------
% 6.82/1.36 % (3471227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471227)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471227)Termination reason: Instruction limit
% 6.82/1.36 % (3471227)Termination phase: Saturation
% 6.82/1.36 % (3471227)Time elapsed: 0.011 s
% 6.82/1.36 % (3471227)Peak memory usage: 12 MB
% 6.82/1.36 % (3471227)Instructions burned: 24 (million)
% 6.82/1.36 % (3471218)Instruction limit reached!
% 6.82/1.36 % (3471218)------------------------------
% 6.82/1.36 % (3471218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471218)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471218)Termination reason: Instruction limit
% 6.82/1.36 % (3471218)Termination phase: Saturation
% 6.82/1.36 % (3471218)Time elapsed: 0.119 s
% 6.82/1.36 % (3471218)Peak memory usage: 16 MB
% 6.82/1.36 % (3471218)Instructions burned: 497 (million)
% 6.82/1.36 % (3471207)Instruction limit reached!
% 6.82/1.36 % (3471207)------------------------------
% 6.82/1.36 % (3471207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.82/1.36 % (3471207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.36 % (3471207)CaDiCaL version: 2.1.3
% 6.82/1.36 % (3471207)Termination reason: Instruction limit
% 6.82/1.36 % (3471207)Termination phase: Saturation
% 6.82/1.36 % (3471207)Time elapsed: 0.208 s
% 7.77/1.53 % (3471207)Peak memory usage: 13 MB
% 7.77/1.53 % (3471207)Instructions burned: 450 (million)
% 7.77/1.53 % (3471223)Instruction limit reached!
% 7.77/1.53 % (3471223)------------------------------
% 7.77/1.53 % (3471223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.77/1.53 % (3471223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.53 % (3471223)CaDiCaL version: 2.1.3
% 7.77/1.53 % (3471223)Termination reason: Instruction limit
% 7.77/1.53 % (3471223)Termination phase: Saturation
% 7.77/1.53 % (3471223)Time elapsed: 0.038 s
% 7.77/1.53 % (3471223)Peak memory usage: 13 MB
% 7.77/1.53 % (3471223)Instructions burned: 66 (million)
% 7.77/1.53 % (3471231)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.77/1.53 % (3471231)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3356789330: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)
% 7.77/1.53 % (3471229)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=1806559790:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 7.77/1.53 % (3471230)lrs+10_1_sil=128000:si=on:urr=on:random_seed=4281642568:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 7.77/1.53 % (3471232)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=941334196:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 7.77/1.53 % (3471233)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2609312619:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 7.77/1.53 % (3471230)Instruction limit reached!
% 7.77/1.53 % (3471230)------------------------------
% 7.77/1.53 % (3471230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.77/1.53 % (3471230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.53 % (3471230)CaDiCaL version: 2.1.3
% 7.77/1.53 % (3471230)Termination reason: Instruction limit
% 7.77/1.53 % (3471230)Termination phase: Saturation
% 7.77/1.53 % (3471230)Time elapsed: 0.016 s
% 7.77/1.53 % (3471230)Peak memory usage: 12 MB
% 7.77/1.53 % (3471230)Instructions burned: 29 (million)
% 7.77/1.53 % (3471239)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.77/1.53 % (3471231)Instruction limit reached!
% 7.77/1.53 % (3471231)------------------------------
% 7.77/1.53 % (3471231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.77/1.53 % (3471231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.53 % (3471231)CaDiCaL version: 2.1.3
% 7.77/1.53 % (3471231)Termination reason: Instruction limit
% 7.77/1.53 % (3471231)Termination phase: Saturation
% 7.77/1.53 % (3471231)Time elapsed: 0.037 s
% 7.77/1.53 % (3471231)Peak memory usage: 13 MB
% 7.77/1.53 % (3471231)Instructions burned: 139 (million)
% 7.77/1.53 % (3471239)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1387747676:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.77/1.53 % (3471240)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3145934376:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.77/1.53 % (3471216)Instruction limit reached!
% 7.77/1.53 % (3471216)------------------------------
% 7.77/1.53 % (3471216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.77/1.53 % (3471216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.53 % (3471216)CaDiCaL version: 2.1.3
% 7.77/1.53 % (3471216)Termination reason: Instruction limit
% 7.77/1.53 % (3471216)Termination phase: Saturation
% 7.77/1.53 % (3471216)Time elapsed: 0.199 s
% 7.77/1.53 % (3471216)Peak memory usage: 14 MB
% 7.77/1.53 % (3471216)Instructions burned: 376 (million)
% 7.77/1.53 % (3471196)Instruction limit reached!
% 7.77/1.53 % (3471196)------------------------------
% 7.77/1.53 % (3471196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.77/1.53 % (3471196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.70 % (3471196)CaDiCaL version: 2.1.3
% 8.97/1.70 % (3471196)Termination reason: Instruction limit
% 8.97/1.70 % (3471196)Termination phase: Saturation
% 8.97/1.70 % (3471196)Time elapsed: 0.412 s
% 8.97/1.70 % (3471196)Peak memory usage: 14 MB
% 8.97/1.70 % (3471196)Instructions burned: 876 (million)
% 8.97/1.70 % (3471243)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2921223814:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 8.97/1.70 % (3471240)Instruction limit reached!
% 8.97/1.70 % (3471240)------------------------------
% 8.97/1.70 % (3471240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.97/1.70 % (3471240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.70 % (3471240)CaDiCaL version: 2.1.3
% 8.97/1.70 % (3471240)Termination reason: Instruction limit
% 8.97/1.70 % (3471240)Termination phase: Saturation
% 8.97/1.70 % (3471240)Time elapsed: 0.034 s
% 8.97/1.70 % (3471240)Peak memory usage: 12 MB
% 8.97/1.70 % (3471240)Instructions burned: 117 (million)
% 8.97/1.70 % (3471244)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3184281836:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2990 on theBenchmark for (2990ds/270Mi)
% 8.97/1.70 % (3471246)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=1639617347: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_2990 on theBenchmark for (2990ds/9840Mi)
% 8.97/1.70 % (3471233)Instruction limit reached!
% 8.97/1.70 % (3471233)------------------------------
% 8.97/1.70 % (3471233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.97/1.70 % (3471233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.70 % (3471233)CaDiCaL version: 2.1.3
% 8.97/1.70 % (3471233)Termination reason: Instruction limit
% 8.97/1.70 % (3471233)Termination phase: Saturation
% 8.97/1.70 % (3471233)Time elapsed: 0.107 s
% 8.97/1.70 % (3471233)Peak memory usage: 13 MB
% 8.97/1.70 % (3471233)Instructions burned: 228 (million)
% 8.97/1.70 % (3471249)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=704151135:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 8.97/1.70 % (3471229)Instruction limit reached!
% 8.97/1.70 % (3471229)------------------------------
% 8.97/1.70 % (3471229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.97/1.70 % (3471229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.70 % (3471229)CaDiCaL version: 2.1.3
% 8.97/1.70 % (3471229)Termination reason: Instruction limit
% 8.97/1.70 % (3471229)Termination phase: Saturation
% 8.97/1.70 % (3471229)Time elapsed: 0.143 s
% 8.97/1.70 % (3471229)Peak memory usage: 13 MB
% 8.97/1.70 % (3471229)Instructions burned: 339 (million)
% 8.97/1.70 % (3471232)Instruction limit reached!
% 8.97/1.70 % (3471232)------------------------------
% 8.97/1.70 % (3471232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.97/1.70 % (3471232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.70 % (3471232)CaDiCaL version: 2.1.3
% 8.97/1.70 % (3471232)Termination reason: Instruction limit
% 8.97/1.70 % (3471232)Termination phase: Saturation
% 8.97/1.70 % (3471232)Time elapsed: 0.146 s
% 8.97/1.70 % (3471232)Peak memory usage: 13 MB
% 8.97/1.70 % (3471232)Instructions burned: 342 (million)
% 8.97/1.70 % (3471251)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
% 8.97/1.70 % (3471251)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=671401862:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.97/1.70 % (3471252)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2741104708:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 8.97/1.70 % (3471252)Instruction limit reached!
% 8.97/1.70 % (3471252)------------------------------
% 8.97/1.70 % (3471252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.97/1.70 % (3471252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471252)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471252)Termination reason: Instruction limit
% 9.34/1.98 % (3471252)Termination phase: Saturation
% 9.34/1.98 % (3471252)Time elapsed: 0.016 s
% 9.34/1.98 % (3471252)Peak memory usage: 12 MB
% 9.34/1.98 % (3471252)Instructions burned: 31 (million)
% 9.34/1.98 % (3471255)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.34/1.98 % (3471255)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.34/1.98 % (3471255)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=181652900:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2988 on theBenchmark for (2988ds/1440Mi)
% 9.34/1.98 % (3471244)Instruction limit reached!
% 9.34/1.98 % (3471244)------------------------------
% 9.34/1.98 % (3471244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.34/1.98 % (3471244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471244)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471244)Termination reason: Instruction limit
% 9.34/1.98 % (3471244)Termination phase: Saturation
% 9.34/1.98 % (3471244)Time elapsed: 0.127 s
% 9.34/1.98 % (3471244)Peak memory usage: 13 MB
% 9.34/1.98 % (3471244)Instructions burned: 270 (million)
% 9.34/1.98 % (3471239)Instruction limit reached!
% 9.34/1.98 % (3471239)------------------------------
% 9.34/1.98 % (3471239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.34/1.98 % (3471239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471239)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471239)Termination reason: Instruction limit
% 9.34/1.98 % (3471239)Termination phase: Saturation
% 9.34/1.98 % (3471239)Time elapsed: 0.174 s
% 9.34/1.98 % (3471239)Peak memory usage: 15 MB
% 9.34/1.98 % (3471239)Instructions burned: 373 (million)
% 9.34/1.98 % (3471258)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1293101553:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 9.34/1.98 % (3471257)dis+10_2_sil=128000:si=on:random_seed=3296719814:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 9.34/1.98 % (3471258)Instruction limit reached!
% 9.34/1.98 % (3471258)------------------------------
% 9.34/1.98 % (3471258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.34/1.98 % (3471258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471258)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471258)Termination reason: Instruction limit
% 9.34/1.98 % (3471258)Termination phase: Saturation
% 9.34/1.98 % (3471258)Time elapsed: 0.058 s
% 9.34/1.98 % (3471258)Peak memory usage: 12 MB
% 9.34/1.98 % (3471258)Instructions burned: 112 (million)
% 9.34/1.98 % (3471251)Instruction limit reached!
% 9.34/1.98 % (3471251)------------------------------
% 9.34/1.98 % (3471251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.34/1.98 % (3471251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471251)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471251)Termination reason: Instruction limit
% 9.34/1.98 % (3471251)Termination phase: Saturation
% 9.34/1.98 % (3471251)Time elapsed: 0.131 s
% 9.34/1.98 % (3471251)Peak memory usage: 14 MB
% 9.34/1.98 % (3471251)Instructions burned: 272 (million)
% 9.34/1.98 % (3471261)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=2695938596:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/122Mi)
% 9.34/1.98 % (3471262)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=3250099747:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/136Mi)
% 9.34/1.98 % (3471243)Instruction limit reached!
% 9.34/1.98 % (3471243)------------------------------
% 9.34/1.98 % (3471243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.34/1.98 % (3471243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/1.98 % (3471243)CaDiCaL version: 2.1.3
% 9.34/1.98 % (3471243)Termination reason: Instruction limit
% 12.70/2.12 % (3471243)Termination phase: Saturation
% 12.70/2.12 % (3471243)Time elapsed: 0.284 s
% 12.70/2.12 % (3471243)Peak memory usage: 14 MB
% 12.70/2.12 % (3471243)Instructions burned: 576 (million)
% 12.70/2.12 % (3471261)Instruction limit reached!
% 12.70/2.12 % (3471261)------------------------------
% 12.70/2.12 % (3471261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.70/2.12 % (3471261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.12 % (3471261)CaDiCaL version: 2.1.3
% 12.70/2.12 % (3471261)Termination reason: Instruction limit
% 12.70/2.12 % (3471261)Termination phase: Saturation
% 12.70/2.12 % (3471261)Time elapsed: 0.065 s
% 12.70/2.12 % (3471261)Peak memory usage: 13 MB
% 12.70/2.12 % (3471261)Instructions burned: 124 (million)
% 12.70/2.12 % (3471249)Instruction limit reached!
% 12.70/2.12 % (3471249)------------------------------
% 12.70/2.12 % (3471249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.70/2.12 % (3471249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.12 % (3471249)CaDiCaL version: 2.1.3
% 12.70/2.12 % (3471249)Termination reason: Instruction limit
% 12.70/2.12 % (3471249)Termination phase: Saturation
% 12.70/2.12 % (3471249)Time elapsed: 0.233 s
% 12.70/2.12 % (3471249)Peak memory usage: 13 MB
% 12.70/2.12 % (3471249)Instructions burned: 422 (million)
% 12.70/2.12 % (3471262)Instruction limit reached!
% 12.70/2.12 % (3471262)------------------------------
% 12.70/2.12 % (3471262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.70/2.12 % (3471262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.12 % (3471262)CaDiCaL version: 2.1.3
% 12.70/2.12 % (3471262)Termination reason: Instruction limit
% 12.70/2.12 % (3471262)Termination phase: Saturation
% 12.70/2.12 % (3471262)Time elapsed: 0.062 s
% 12.70/2.12 % (3471262)Peak memory usage: 12 MB
% 12.70/2.12 % (3471262)Instructions burned: 137 (million)
% 12.70/2.12 % (3471265)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2204509920:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 12.70/2.12 % (3471267)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.70/2.12 % (3471266)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=907453496:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2987 on theBenchmark for (2987ds/1254Mi)
% 12.70/2.12 % (3471267)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=2225494723:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2987 on theBenchmark for (2987ds/281Mi)
% 12.70/2.12 % (3471268)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=320786653:i=619:add=on:rtra=on_2987 on theBenchmark for (2987ds/619Mi)
% 12.70/2.12 % (3471265)Instruction limit reached!
% 12.70/2.12 % (3471265)------------------------------
% 12.70/2.12 % (3471265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.70/2.12 % (3471265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.12 % (3471265)CaDiCaL version: 2.1.3
% 12.70/2.12 % (3471265)Termination reason: Instruction limit
% 12.70/2.12 % (3471265)Termination phase: Saturation
% 12.70/2.12 % (3471265)Time elapsed: 0.118 s
% 12.70/2.12 % (3471265)Peak memory usage: 12 MB
% 12.70/2.12 % (3471265)Instructions burned: 232 (million)
% 12.70/2.12 % (3471257)Instruction limit reached!
% 12.70/2.12 % (3471257)------------------------------
% 12.70/2.12 % (3471257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.70/2.12 % (3471257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.12 % (3471257)CaDiCaL version: 2.1.3
% 12.70/2.12 % (3471257)Termination reason: Instruction limit
% 12.70/2.12 % (3471257)Termination phase: Saturation
% 12.70/2.12 % (3471257)Time elapsed: 0.270 s
% 12.70/2.12 % (3471257)Peak memory usage: 12 MB
% 12.70/2.12 % (3471257)Instructions burned: 340 (million)
% 12.70/2.12 % (3471273)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=3114369526:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/865Mi)
% 12.70/2.12 % (3471274)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3710486778:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/212Mi)
% 13.36/2.26 % (3471267)Instruction limit reached!
% 13.36/2.26 % (3471267)------------------------------
% 13.36/2.26 % (3471267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471267)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471267)Termination reason: Instruction limit
% 13.36/2.26 % (3471267)Termination phase: Saturation
% 13.36/2.26 % (3471267)Time elapsed: 0.142 s
% 13.36/2.26 % (3471267)Peak memory usage: 13 MB
% 13.36/2.26 % (3471267)Instructions burned: 282 (million)
% 13.36/2.26 % (3471277)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3541299880:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/130Mi)
% 13.36/2.26 % (3471277)Instruction limit reached!
% 13.36/2.26 % (3471277)------------------------------
% 13.36/2.26 % (3471277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471277)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471277)Termination reason: Instruction limit
% 13.36/2.26 % (3471277)Termination phase: Saturation
% 13.36/2.26 % (3471277)Time elapsed: 0.060 s
% 13.36/2.26 % (3471277)Peak memory usage: 12 MB
% 13.36/2.26 % (3471277)Instructions burned: 132 (million)
% 13.36/2.26 % (3471279)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3987638390:st=1.5:i=346:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/346Mi)
% 13.36/2.26 % (3471274)Instruction limit reached!
% 13.36/2.26 % (3471274)------------------------------
% 13.36/2.26 % (3471274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471274)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471274)Termination reason: Instruction limit
% 13.36/2.26 % (3471274)Termination phase: Saturation
% 13.36/2.26 % (3471274)Time elapsed: 0.109 s
% 13.36/2.26 % (3471274)Peak memory usage: 13 MB
% 13.36/2.26 % (3471274)Instructions burned: 213 (million)
% 13.36/2.26 % (3471281)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=1141602459:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/152Mi)
% 13.36/2.26 % (3471268)Instruction limit reached!
% 13.36/2.26 % (3471268)------------------------------
% 13.36/2.26 % (3471268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471268)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471268)Termination reason: Instruction limit
% 13.36/2.26 % (3471268)Termination phase: Saturation
% 13.36/2.26 % (3471268)Time elapsed: 0.335 s
% 13.36/2.26 % (3471268)Peak memory usage: 15 MB
% 13.36/2.26 % (3471268)Instructions burned: 620 (million)
% 13.36/2.26 % (3471281)Instruction limit reached!
% 13.36/2.26 % (3471281)------------------------------
% 13.36/2.26 % (3471281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471281)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471281)Termination reason: Instruction limit
% 13.36/2.26 % (3471281)Termination phase: Saturation
% 13.36/2.26 % (3471281)Time elapsed: 0.081 s
% 13.36/2.26 % (3471281)Peak memory usage: 13 MB
% 13.36/2.26 % (3471281)Instructions burned: 153 (million)
% 13.36/2.26 % (3471283)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3245161318:i=75:ep=R:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/75Mi)
% 13.36/2.26 % (3471284)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=321535145:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/387Mi)
% 13.36/2.26 % (3471283)Instruction limit reached!
% 13.36/2.26 % (3471283)------------------------------
% 13.36/2.26 % (3471283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.36/2.26 % (3471283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.26 % (3471283)CaDiCaL version: 2.1.3
% 13.36/2.26 % (3471283)Termination reason: Instruction limit
% 13.36/2.26 % (3471283)Termination phase: Saturation
% 13.36/2.26 % (3471283)Time elapsed: 0.035 s
% 13.36/2.26 % (3471283)Peak memory usage: 12 MB
% 13.36/2.26 % (3471283)Instructions burned: 76 (million)
% 13.36/2.26 % (3471287)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=2399195114:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2982 on theBenchmark for (2982ds/148Mi)
% 14.35/2.47 % (3471279)Instruction limit reached!
% 14.35/2.47 % (3471279)------------------------------
% 14.35/2.47 % (3471279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471279)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471279)Termination reason: Instruction limit
% 14.35/2.47 % (3471279)Termination phase: Saturation
% 14.35/2.47 % (3471279)Time elapsed: 0.184 s
% 14.35/2.47 % (3471279)Peak memory usage: 13 MB
% 14.35/2.47 % (3471279)Instructions burned: 346 (million)
% 14.35/2.47 % (3471289)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=2146215205:i=161:piset=and:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/161Mi)
% 14.35/2.47 % (3471287)Instruction limit reached!
% 14.35/2.47 % (3471287)------------------------------
% 14.35/2.47 % (3471287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471287)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471287)Termination reason: Instruction limit
% 14.35/2.47 % (3471287)Termination phase: Saturation
% 14.35/2.47 % (3471287)Time elapsed: 0.073 s
% 14.35/2.47 % (3471287)Peak memory usage: 12 MB
% 14.35/2.47 % (3471287)Instructions burned: 150 (million)
% 14.35/2.47 % (3471273)Instruction limit reached!
% 14.35/2.47 % (3471273)------------------------------
% 14.35/2.47 % (3471273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471273)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471273)Termination reason: Instruction limit
% 14.35/2.47 % (3471273)Termination phase: Saturation
% 14.35/2.47 % (3471273)Time elapsed: 0.373 s
% 14.35/2.47 % (3471273)Peak memory usage: 13 MB
% 14.35/2.47 % (3471273)Instructions burned: 866 (million)
% 14.35/2.47 % (3471291)lrs+10_1_sil=128000:si=on:random_seed=1127033537:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/888Mi)
% 14.35/2.47 % (3471292)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=1366415269:i=136:add=on:ins=4:rtra=on:sup=off_2981 on theBenchmark for (2981ds/136Mi)
% 14.35/2.47 % (3471292)Refutation not found, incomplete strategy
% 14.35/2.47 % (3471292)------------------------------
% 14.35/2.47 % (3471292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471292)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471292)Termination reason: Refutation not found, incomplete strategy
% 14.35/2.47 % (3471292)Time elapsed: 0.017 s
% 14.35/2.47 % (3471292)Peak memory usage: 12 MB
% 14.35/2.47 % (3471292)Instructions burned: 31 (million)
% 14.35/2.47 % (3471289)Instruction limit reached!
% 14.35/2.47 % (3471289)------------------------------
% 14.35/2.47 % (3471289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471289)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471289)Termination reason: Instruction limit
% 14.35/2.47 % (3471289)Termination phase: Saturation
% 14.35/2.47 % (3471289)Time elapsed: 0.083 s
% 14.35/2.47 % (3471289)Peak memory usage: 12 MB
% 14.35/2.47 % (3471289)Instructions burned: 163 (million)
% 14.35/2.47 % (3471292)------------------------------
% 14.35/2.47 % (3471292)------------------------------
% 14.35/2.47 % (3471266)Instruction limit reached!
% 14.35/2.47 % (3471266)------------------------------
% 14.35/2.47 % (3471266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.35/2.47 % (3471266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/2.47 % (3471266)CaDiCaL version: 2.1.3
% 14.35/2.47 % (3471266)Termination reason: Instruction limit
% 14.35/2.47 % (3471266)Termination phase: Saturation
% 14.35/2.47 % (3471266)Time elapsed: 0.536 s
% 14.35/2.47 % (3471266)Peak memory usage: 13 MB
% 14.35/2.47 % (3471266)Instructions burned: 1254 (million)
% 14.35/2.47 % (3471296)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=215225327:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2981 on theBenchmark for (2981ds/93Mi)
% 14.35/2.47 % (3471295)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=1999805679:i=88:s2at=3:nm=2:rtra=on:rawr=on_2981 on theBenchmark for (2981ds/88Mi)
% 15.50/2.64 % (3471297)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3111689411:i=2186:rtra=on:ixr=off_2981 on theBenchmark for (2981ds/2186Mi)
% 15.50/2.64 % (3471255)Instruction limit reached!
% 15.50/2.64 % (3471255)------------------------------
% 15.50/2.64 % (3471255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/2.64 % (3471255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/2.64 % (3471255)CaDiCaL version: 2.1.3
% 15.50/2.64 % (3471255)Termination reason: Instruction limit
% 15.50/2.64 % (3471255)Termination phase: Saturation
% 15.50/2.64 % (3471255)Time elapsed: 0.742 s
% 15.50/2.64 % (3471255)Peak memory usage: 15 MB
% 15.50/2.64 % (3471255)Instructions burned: 1441 (million)
% 15.50/2.64 % (3471301)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=791103810:s2a=on:i=240:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/240Mi)
% 15.50/2.64 % (3471284)Instruction limit reached!
% 15.50/2.64 % (3471284)------------------------------
% 15.50/2.64 % (3471284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/2.64 % (3471284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/2.64 % (3471284)CaDiCaL version: 2.1.3
% 15.50/2.64 % (3471284)Termination reason: Instruction limit
% 15.50/2.64 % (3471284)Termination phase: Saturation
% 15.50/2.64 % (3471284)Time elapsed: 0.220 s
% 15.50/2.64 % (3471284)Peak memory usage: 13 MB
% 15.50/2.64 % (3471284)Instructions burned: 387 (million)
% 15.50/2.64 % (3471295)Instruction limit reached!
% 15.50/2.64 % (3471295)------------------------------
% 15.50/2.64 % (3471295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/2.64 % (3471295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/2.64 % (3471295)CaDiCaL version: 2.1.3
% 15.50/2.64 % (3471295)Termination reason: Instruction limit
% 15.50/2.64 % (3471295)Termination phase: Saturation
% 15.50/2.64 % (3471295)Time elapsed: 0.046 s
% 15.50/2.64 % (3471295)Peak memory usage: 13 MB
% 15.50/2.64 % (3471295)Instructions burned: 88 (million)
% 15.50/2.64 % (3471296)Instruction limit reached!
% 15.50/2.64 % (3471296)------------------------------
% 15.50/2.64 % (3471296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/2.64 % (3471296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/2.64 % (3471296)CaDiCaL version: 2.1.3
% 15.50/2.64 % (3471296)Termination reason: Instruction limit
% 15.50/2.64 % (3471296)Termination phase: Saturation
% 15.50/2.64 % (3471296)Time elapsed: 0.048 s
% 15.50/2.64 % (3471296)Peak memory usage: 12 MB
% 15.50/2.64 % (3471296)Instructions burned: 94 (million)
% 15.50/2.64 % (3471303)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=1651660679:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2981 on theBenchmark for (2981ds/805Mi)
% 15.50/2.64 % (3471304)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 15.50/2.64 % (3471304)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=3359743857:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2980 on theBenchmark for (2980ds/391Mi)
% 15.50/2.64 % (3471305)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=838971394:i=355:av=off:fsr=off:rtra=on:ixr=off_2980 on theBenchmark for (2980ds/355Mi)
% 15.50/2.64 % (3471303)Refutation not found, incomplete strategy
% 15.50/2.64 % (3471303)------------------------------
% 15.50/2.64 % (3471303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.50/2.64 % (3471303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.50/2.64 % (3471303)CaDiCaL version: 2.1.3
% 15.50/2.64 % (3471303)Termination reason: Refutation not found, incomplete strategy
% 15.50/2.64 % (3471303)Time elapsed: 0.083 s
% 15.50/2.64 % (3471303)Peak memory usage: 13 MB
% 15.50/2.64 % (3471303)Instructions burned: 157 (million)
% 15.50/2.64 % (3471303)------------------------------
% 15.50/2.64 % (3471303)------------------------------
% 15.50/2.64 % (3471301)Instruction limit reached!
% 15.50/2.64 % (3471301)------------------------------
% 15.50/2.64 % (3471301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471301)CaDiCaL version: 2.1.3
% 15.73/2.79 % (3471301)Termination reason: Instruction limit
% 15.73/2.79 % (3471301)Termination phase: Saturation
% 15.73/2.79 % (3471301)Time elapsed: 0.120 s
% 15.73/2.79 % (3471301)Peak memory usage: 13 MB
% 15.73/2.79 % (3471301)Instructions burned: 240 (million)
% 15.73/2.79 % (3471309)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=3419816404:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/314Mi)
% 15.73/2.79 % (3471310)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=27646350:s2a=on:i=251:fsr=off:rtra=on_2979 on theBenchmark for (2979ds/251Mi)
% 15.73/2.79 % (3471305)Instruction limit reached!
% 15.73/2.79 % (3471305)------------------------------
% 15.73/2.79 % (3471305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471305)CaDiCaL version: 2.1.3
% 15.73/2.79 % (3471305)Termination reason: Instruction limit
% 15.73/2.79 % (3471305)Termination phase: Saturation
% 15.73/2.79 % (3471305)Time elapsed: 0.167 s
% 15.73/2.79 % (3471305)Peak memory usage: 13 MB
% 15.73/2.79 % (3471305)Instructions burned: 355 (million)
% 15.73/2.79 % (3471313)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=2666401861: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_2979 on theBenchmark for (2979ds/2470Mi)
% 15.73/2.79 % (3471304)Instruction limit reached!
% 15.73/2.79 % (3471304)------------------------------
% 15.73/2.79 % (3471304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471304)CaDiCaL version: 2.1.3
% 15.73/2.79 % (3471304)Termination reason: Instruction limit
% 15.73/2.79 % (3471304)Termination phase: Saturation
% 15.73/2.79 % (3471304)Time elapsed: 0.199 s
% 15.73/2.79 % (3471304)Peak memory usage: 13 MB
% 15.73/2.79 % (3471304)Instructions burned: 392 (million)
% 15.73/2.79 % (3471310)Instruction limit reached!
% 15.73/2.79 % (3471310)------------------------------
% 15.73/2.79 % (3471310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471310)CaDiCaL version: 2.1.3
% 15.73/2.79 % (3471310)Termination reason: Instruction limit
% 15.73/2.79 % (3471310)Termination phase: Saturation
% 15.73/2.79 % (3471310)Time elapsed: 0.103 s
% 15.73/2.79 % (3471310)Peak memory usage: 12 MB
% 15.73/2.79 % (3471310)Instructions burned: 253 (million)
% 15.73/2.79 % (3471315)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=3717924420:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2978 on theBenchmark for (2978ds/673Mi)
% 15.73/2.79 % (3471316)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=958028763:i=116:ep=RSTC:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/116Mi)
% 15.73/2.79 % (3471309)Instruction limit reached!
% 15.73/2.79 % (3471309)------------------------------
% 15.73/2.79 % (3471309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471309)CaDiCaL version: 2.1.3
% 15.73/2.79 % (3471309)Termination reason: Instruction limit
% 15.73/2.79 % (3471309)Termination phase: Saturation
% 15.73/2.79 % (3471309)Time elapsed: 0.150 s
% 15.73/2.79 % (3471309)Peak memory usage: 13 MB
% 15.73/2.79 % (3471309)Instructions burned: 315 (million)
% 15.73/2.79 % (3471320)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3611345052:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2978 on theBenchmark for (2978ds/270Mi)
% 15.73/2.79 % (3471316)Instruction limit reached!
% 15.73/2.79 % (3471316)------------------------------
% 15.73/2.79 % (3471316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.73/2.79 % (3471316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/2.79 % (3471316)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471316)Termination reason: Instruction limit
% 19.81/3.14 % (3471316)Termination phase: Saturation
% 19.81/3.14 % (3471316)Time elapsed: 0.067 s
% 19.81/3.14 % (3471316)Peak memory usage: 12 MB
% 19.81/3.14 % (3471316)Instructions burned: 118 (million)
% 19.81/3.14 % (3471322)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=4005000168: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_2977 on theBenchmark for (2977ds/30Mi)
% 19.81/3.14 % (3471322)Instruction limit reached!
% 19.81/3.14 % (3471322)------------------------------
% 19.81/3.14 % (3471322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471322)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471322)Termination reason: Instruction limit
% 19.81/3.14 % (3471322)Termination phase: Saturation
% 19.81/3.14 % (3471322)Time elapsed: 0.017 s
% 19.81/3.14 % (3471322)Peak memory usage: 12 MB
% 19.81/3.14 % (3471322)Instructions burned: 31 (million)
% 19.81/3.14 % (3471291)Instruction limit reached!
% 19.81/3.14 % (3471291)------------------------------
% 19.81/3.14 % (3471291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471291)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471291)Termination reason: Instruction limit
% 19.81/3.14 % (3471291)Termination phase: Saturation
% 19.81/3.14 % (3471291)Time elapsed: 0.441 s
% 19.81/3.14 % (3471291)Peak memory usage: 15 MB
% 19.81/3.14 % (3471291)Instructions burned: 889 (million)
% 19.81/3.14 % (3471324)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 19.81/3.14 % (3471324)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=3469531594:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 19.81/3.14 % (3471325)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1572912963:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2977 on theBenchmark for (2977ds/365Mi)
% 19.81/3.14 % (3471324)Instruction limit reached!
% 19.81/3.14 % (3471324)------------------------------
% 19.81/3.14 % (3471324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471324)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471324)Termination reason: Instruction limit
% 19.81/3.14 % (3471324)Termination phase: Saturation
% 19.81/3.14 % (3471324)Time elapsed: 0.020 s
% 19.81/3.14 % (3471324)Peak memory usage: 12 MB
% 19.81/3.14 % (3471324)Instructions burned: 40 (million)
% 19.81/3.14 % (3471328)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1461465000:i=158:av=off:rtra=on_2977 on theBenchmark for (2977ds/158Mi)
% 19.81/3.14 % (3471320)Instruction limit reached!
% 19.81/3.14 % (3471320)------------------------------
% 19.81/3.14 % (3471320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471320)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471320)Termination reason: Instruction limit
% 19.81/3.14 % (3471320)Termination phase: Saturation
% 19.81/3.14 % (3471320)Time elapsed: 0.126 s
% 19.81/3.14 % (3471320)Peak memory usage: 13 MB
% 19.81/3.14 % (3471320)Instructions burned: 270 (million)
% 19.81/3.14 % (3471330)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
% 19.81/3.14 % (3471330)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=944703791:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/252Mi)
% 19.81/3.14 % (3471328)Instruction limit reached!
% 19.81/3.14 % (3471328)------------------------------
% 19.81/3.14 % (3471328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471328)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471328)Termination reason: Instruction limit
% 19.81/3.14 % (3471328)Termination phase: Saturation
% 19.81/3.14 % (3471328)Time elapsed: 0.078 s
% 19.81/3.14 % (3471328)Peak memory usage: 12 MB
% 19.81/3.14 % (3471328)Instructions burned: 160 (million)
% 19.81/3.14 % (3471332)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2227867326:i=213:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/213Mi)
% 19.81/3.14 % (3471330)Instruction limit reached!
% 19.81/3.14 % (3471330)------------------------------
% 19.81/3.14 % (3471330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471330)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471330)Termination reason: Instruction limit
% 19.81/3.14 % (3471330)Termination phase: Saturation
% 19.81/3.14 % (3471330)Time elapsed: 0.121 s
% 19.81/3.14 % (3471330)Peak memory usage: 13 MB
% 19.81/3.14 % (3471330)Instructions burned: 253 (million)
% 19.81/3.14 % (3471315)Instruction limit reached!
% 19.81/3.14 % (3471315)------------------------------
% 19.81/3.14 % (3471315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471315)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471315)Termination reason: Instruction limit
% 19.81/3.14 % (3471315)Termination phase: Saturation
% 19.81/3.14 % (3471315)Time elapsed: 0.326 s
% 19.81/3.14 % (3471315)Peak memory usage: 14 MB
% 19.81/3.14 % (3471315)Instructions burned: 675 (million)
% 19.81/3.14 % (3471334)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=1760592440:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2975 on theBenchmark for (2975ds/160Mi)
% 19.81/3.14 % (3471335)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=922150730:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/763Mi)
% 19.81/3.14 % (3471325)Instruction limit reached!
% 19.81/3.14 % (3471325)------------------------------
% 19.81/3.14 % (3471325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471325)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471325)Termination reason: Instruction limit
% 19.81/3.14 % (3471325)Termination phase: Saturation
% 19.81/3.14 % (3471325)Time elapsed: 0.217 s
% 19.81/3.14 % (3471325)Peak memory usage: 14 MB
% 19.81/3.14 % (3471325)Instructions burned: 367 (million)
% 19.81/3.14 % (3471335)Refutation not found, incomplete strategy
% 19.81/3.14 % (3471335)------------------------------
% 19.81/3.14 % (3471335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471335)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471335)Termination reason: Refutation not found, incomplete strategy
% 19.81/3.14 % (3471335)Time elapsed: 0.007 s
% 19.81/3.14 % (3471335)Peak memory usage: 12 MB
% 19.81/3.14 % (3471335)Instructions burned: 12 (million)
% 19.81/3.14 % (3471335)------------------------------
% 19.81/3.14 % (3471335)------------------------------
% 19.81/3.14 % (3471338)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 19.81/3.14 % (3471332)Instruction limit reached!
% 19.81/3.14 % (3471332)------------------------------
% 19.81/3.14 % (3471332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471332)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471332)Termination reason: Instruction limit
% 19.81/3.14 % (3471332)Termination phase: Saturation
% 19.81/3.14 % (3471332)Time elapsed: 0.106 s
% 19.81/3.14 % (3471332)Peak memory usage: 13 MB
% 19.81/3.14 % (3471332)Instructions burned: 213 (million)
% 19.81/3.14 % (3471338)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=1653957007:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2975 on theBenchmark for (2975ds/237Mi)
% 19.81/3.14 % (3471339)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=523221199:s2a=on:i=386:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/386Mi)
% 19.81/3.14 % (3471341)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=2089637919:i=300:piset=and:nm=32:rtra=on_2974 on theBenchmark for (2974ds/300Mi)
% 19.81/3.14 % (3471334)Instruction limit reached!
% 19.81/3.14 % (3471334)------------------------------
% 19.81/3.14 % (3471334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471334)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471334)Termination reason: Instruction limit
% 19.81/3.14 % (3471334)Termination phase: Saturation
% 19.81/3.14 % (3471334)Time elapsed: 0.083 s
% 19.81/3.14 % (3471334)Peak memory usage: 13 MB
% 19.81/3.14 % (3471334)Instructions burned: 161 (million)
% 19.81/3.14 % (3471344)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=731486308:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/567Mi)
% 19.81/3.14 % (3471341)Instruction limit reached!
% 19.81/3.14 % (3471341)------------------------------
% 19.81/3.14 % (3471341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471341)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471341)Termination reason: Instruction limit
% 19.81/3.14 % (3471341)Termination phase: Saturation
% 19.81/3.14 % (3471341)Time elapsed: 0.135 s
% 19.81/3.14 % (3471341)Peak memory usage: 12 MB
% 19.81/3.14 % (3471341)Instructions burned: 302 (million)
% 19.81/3.14 % (3471346)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=3899102805:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2973 on theBenchmark for (2973ds/379Mi)
% 19.81/3.14 % (3471339)Instruction limit reached!
% 19.81/3.14 % (3471339)------------------------------
% 19.81/3.14 % (3471339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471339)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471339)Termination reason: Instruction limit
% 19.81/3.14 % (3471339)Termination phase: Saturation
% 19.81/3.14 % (3471339)Time elapsed: 0.185 s
% 19.81/3.14 % (3471339)Peak memory usage: 12 MB
% 19.81/3.14 % (3471339)Instructions burned: 387 (million)
% 19.81/3.14 % (3471338)Instruction limit reached!
% 19.81/3.14 % (3471338)------------------------------
% 19.81/3.14 % (3471338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471338)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471338)Termination reason: Instruction limit
% 19.81/3.14 % (3471338)Termination phase: Saturation
% 19.81/3.14 % (3471338)Time elapsed: 0.191 s
% 19.81/3.14 % (3471338)Peak memory usage: 13 MB
% 19.81/3.14 % (3471338)Instructions burned: 238 (million)
% 19.81/3.14 % (3471348)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=3241866815:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2972 on theBenchmark for (2972ds/429Mi)
% 19.81/3.14 % (3471349)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=3739384245:i=478:bd=all:rtra=on_2972 on theBenchmark for (2972ds/478Mi)
% 19.81/3.14 % (3471348) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3471076-3471348"...
% 19.81/3.14 % (3471346)Instruction limit reached!
% 19.81/3.14 % (3471346)------------------------------
% 19.81/3.14 % (3471346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471346)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471346)Termination reason: Instruction limit
% 19.81/3.14 % (3471346)Termination phase: Saturation
% 19.81/3.14 % (3471346)Time elapsed: 0.186 s
% 19.81/3.14 % (3471346)Peak memory usage: 14 MB
% 19.81/3.14 % (3471346)Instructions burned: 380 (million)
% 19.81/3.14 % (3471348)...printing done.
% 19.81/3.14 % (3471348)Refutation found. Thanks to Tanya!
% 19.81/3.14 % SZS status Theorem for theBenchmark
% 19.81/3.14 % SZS output start Proof for theBenchmark
% 19.81/3.14 thf(type_def_5, type, a: $tType).
% 19.81/3.14 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 19.81/3.14 thf(func_def_3, type, vAND: ($o > $o > $o)).
% 19.81/3.14 thf(func_def_4, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 19.81/3.14 thf(func_def_5, type, db1: !>[X0: $tType]:(X0)).
% 19.81/3.14 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 19.81/3.14 thf(func_def_7, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 19.81/3.14 thf(func_def_8, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 19.81/3.14 thf(func_def_9, type, vIMP: ($o > $o > $o)).
% 19.81/3.14 thf(func_def_10, type, vIFF: ($o > $o > $o)).
% 19.81/3.14 thf(func_def_11, type, db2: !>[X0: $tType]:(X0)).
% 19.81/3.14 thf(func_def_12, type, vEPSILON: !>[X0: $tType]:(((X0 > $o) > X0))).
% 19.81/3.14 thf(func_def_13, type, sK0: ((a > $o) > $o)).
% 19.81/3.14 thf(func_def_14, type, sK1: ((a > $o) > a)).
% 19.81/3.14 thf(func_def_15, type, sK2: (a > a > $o)).
% 19.81/3.14 thf(func_def_16, type, sK3: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_17, type, sK4: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_18, type, sK5: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_19, type, sK6: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_20, type, sK7: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_21, type, sK8: ((a > a > $o) > a)).
% 19.81/3.14 thf(func_def_23, type, sK10: (a > $o)).
% 19.81/3.14 thf(func_def_24, type, sK11: a).
% 19.81/3.14 thf(func_def_25, type, sK12: a).
% 19.81/3.14 thf(func_def_26, type, sK13: a).
% 19.81/3.14 thf(func_def_27, type, sK14: (a > $o)).
% 19.81/3.14 thf(func_def_28, type, sK15: a).
% 19.81/3.14 thf(func_def_29, type, sK16: a).
% 19.81/3.14 thf(func_def_30, type, sK17: a).
% 19.81/3.14 thf(func_def_31, type, sK18: ((a > $o) > a)).
% 19.81/3.14 thf(func_def_32, type, sK19: ((a > $o) > a)).
% 19.81/3.14 thf(func_def_33, type, sK20: ((a > $o) > a)).
% 19.81/3.14 thf(func_def_34, type, sK21: (a > $o)).
% 19.81/3.14 thf(func_def_35, type, sK22: a).
% 19.81/3.14 thf(func_def_36, type, sK23: a).
% 19.81/3.14 thf(func_def_37, type, sK24: a).
% 19.81/3.14 thf(func_def_38, type, sK25: a).
% 19.81/3.14 thf(func_def_39, type, sK26: a).
% 19.81/3.14 thf(func_def_40, type, sK27: a).
% 19.81/3.14 thf(func_def_41, type, sK28: a).
% 19.81/3.14 thf(func_def_42, type, sK29: a).
% 19.81/3.14 thf(func_def_43, type, sK30: a).
% 19.81/3.14 thf(f1,conjecture,(
% 19.81/3.14 ! [X0 : ((a > $o) > $o)] : ((! [X1 : (a > $o)] : ((X0 @ X1) => ? [X2 : a] : (X1 @ X2)) & ! [X3 : a] : ? [X1 : (a > $o)] : ((X1 @ X3) & ! [X4 : (a > $o)] : (((X4 @ X3) & (X0 @ X4)) => (X4 = X1)) & (X0 @ X1))) => ? [X5 : (a > a > $o)] : (! [X3 : a] : (X5 @ X3 @ X3) & ! [X6 : a,X3 : a] : ((X5 @ X3 @ X6) => (X5 @ X6 @ X3)) & (X0 = (^[X7 : (a > $o)] : (! [X3 : a] : ((X7 @ X3) => ! [X6 : a] : ((X7 @ X6) <=> (X5 @ X3 @ X6))) & ? [X2 : a] : (X7 @ X2)))) & ! [X6 : a,X3 : a,X2 : a] : (((X5 @ X3 @ X6) & (X5 @ X6 @ X2)) => (X5 @ X3 @ X2))))),
% 19.81/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM262_pme)).
% 19.81/3.14 thf(f2,negated_conjecture,(
% 19.81/3.14 ~ ! [X0 : ((a > $o) > $o)] : ((! [X1 : (a > $o)] : ((X0 @ X1) => ? [X2 : a] : (X1 @ X2)) & ! [X3 : a] : ? [X1 : (a > $o)] : ((X1 @ X3) & ! [X4 : (a > $o)] : (((X4 @ X3) & (X0 @ X4)) => (X4 = X1)) & (X0 @ X1))) => ? [X5 : (a > a > $o)] : (! [X3 : a] : (X5 @ X3 @ X3) & ! [X6 : a,X3 : a] : ((X5 @ X3 @ X6) => (X5 @ X6 @ X3)) & (X0 = (^[X7 : (a > $o)] : (! [X3 : a] : ((X7 @ X3) => ! [X6 : a] : ((X7 @ X6) <=> (X5 @ X3 @ X6))) & ? [X2 : a] : (X7 @ X2)))) & ! [X6 : a,X3 : a,X2 : a] : (((X5 @ X3 @ X6) & (X5 @ X6 @ X2)) => (X5 @ X3 @ X2))))),
% 19.81/3.14 inference(negated_conjecture,[status(cth)],[f1])).
% 19.81/3.14 thf(f3,plain,(
% 19.81/3.14 ~ ! [X0 : ((a > $o) > $o)] : ((! [X1 : (a > $o)] : ((X0 @ X1) => ? [X2 : a] : (X1 @ X2)) & ! [X3 : a] : ? [X4 : (a > $o)] : ((X4 @ X3) & ! [X5 : (a > $o)] : (((X5 @ X3) & (X0 @ X5)) => (X4 = X5)) & (X0 @ X4))) => ? [X6 : (a > a > $o)] : (! [X7 : a] : (X6 @ X7 @ X7) & ! [X8 : a,X9 : a] : ((X6 @ X9 @ X8) => (X6 @ X8 @ X9)) & (X0 = (^[X10 : (a > $o)] : (! [X11 : a] : ((X10 @ X11) => ! [X12 : a] : ((X10 @ X12) <=> (X6 @ X11 @ X12))) & ? [X13 : a] : (X10 @ X13)))) & ! [X14 : a,X15 : a,X16 : a] : (((X6 @ X15 @ X14) & (X6 @ X14 @ X16)) => (X6 @ X15 @ X16))))),
% 19.81/3.14 inference(rectify,[],[f2])).
% 19.81/3.14 thf(f4,plain,(
% 19.81/3.14 ~ ! [X0 : ((a > $o) > $o)] : ((! [X1 : (a > $o)] : ((((X0 @ X1)) = $true) => ? [X2 : a] : (((X1 @ X2)) = $true)) & ! [X3 : a] : ? [X4 : (a > $o)] : ((((X4 @ X3)) = $true) & ! [X5 : (a > $o)] : ((($true = ((X0 @ X5))) & ($true = ((X5 @ X3)))) => (X4 = X5)) & (((X0 @ X4)) = $true))) => ? [X6 : (a > a > $o)] : (! [X7 : a] : ($true = ((X6 @ X7 @ X7))) & ! [X8 : a,X9 : a] : (($true = ((X6 @ X9 @ X8))) => (((X6 @ X8 @ X9)) = $true)) & ((^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))) = X0) & ! [X14 : a,X15 : a,X16 : a] : ((($true = ((X6 @ X15 @ X14))) & (((X6 @ X14 @ X16)) = $true)) => (((X6 @ X15 @ X16)) = $true))))),
% 19.81/3.14 inference(fool_elimination,[],[f3])).
% 19.81/3.14 thf(f6,plain,(
% 19.81/3.14 ~ ! [X0 : ((a > $o) > $o)] : ((! [X1 : (a > $o)] : ((((X0 @ X1)) = $true) => ? [X2 : a] : (((X1 @ X2)) = $true)) & ! [X3 : a] : ? [X4 : (a > $o)] : ((((X4 @ X3)) = $true) & ! [X5 : (a > $o)] : ((($true = ((X0 @ X5))) & ($true = ((X5 @ X3)))) => (X4 = X5)) & (((X0 @ X4)) = $true))) => ? [X6 : (a > a > $o)] : (! [X12 : a,X10 : a,X11 : a] : (((((X6 @ X10 @ X12)) = $true) & ($true = ((X6 @ X11 @ X10)))) => ($true = ((X6 @ X11 @ X12)))) & ((^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))) = X0) & ! [X7 : a] : ($true = ((X6 @ X7 @ X7))) & ! [X8 : a,X9 : a] : (($true = ((X6 @ X9 @ X8))) => (((X6 @ X8 @ X9)) = $true))))),
% 19.81/3.14 inference(rectify,[],[f4])).
% 19.81/3.14 thf(f7,plain,(
% 19.81/3.14 ? [X0 : ((a > $o) > $o)] : (! [X6 : (a > a > $o)] : (? [X12 : a,X10 : a,X11 : a] : (($true != ((X6 @ X11 @ X12))) & ((((X6 @ X10 @ X12)) = $true) & ($true = ((X6 @ X11 @ X10))))) | ((^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))) != X0) | ? [X7 : a] : ($true != ((X6 @ X7 @ X7))) | ? [X8 : a,X9 : a] : (($true = ((X6 @ X9 @ X8))) & (((X6 @ X8 @ X9)) != $true))) & (! [X1 : (a > $o)] : ((((X0 @ X1)) != $true) | ? [X2 : a] : (((X1 @ X2)) = $true)) & ! [X3 : a] : ? [X4 : (a > $o)] : ((((X4 @ X3)) = $true) & ! [X5 : (a > $o)] : ((X4 = X5) | (($true != ((X0 @ X5))) | ($true != ((X5 @ X3))))) & (((X0 @ X4)) = $true))))),
% 19.81/3.14 inference(ennf_transformation,[],[f6])).
% 19.81/3.14 thf(f8,plain,(
% 19.81/3.14 ? [X0 : ((a > $o) > $o)] : (! [X1 : (a > $o)] : ((((X0 @ X1)) != $true) | ? [X2 : a] : (((X1 @ X2)) = $true)) & ! [X3 : a] : ? [X4 : (a > $o)] : (! [X5 : (a > $o)] : ((X4 = X5) | ($true != ((X5 @ X3))) | ($true != ((X0 @ X5)))) & (((X0 @ X4)) = $true) & (((X4 @ X3)) = $true)) & ! [X6 : (a > a > $o)] : (? [X8 : a,X9 : a] : (($true = ((X6 @ X9 @ X8))) & (((X6 @ X8 @ X9)) != $true)) | ? [X11 : a,X12 : a,X10 : a] : (($true = ((X6 @ X11 @ X10))) & (((X6 @ X10 @ X12)) = $true) & ($true != ((X6 @ X11 @ X12)))) | ((^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))) != X0) | ? [X7 : a] : ($true != ((X6 @ X7 @ X7)))))),
% 19.81/3.14 inference(flattening,[],[f7])).
% 19.81/3.14 thf(f9,plain,(
% 19.81/3.14 ? [X0 : ((a > $o) > $o)] : (! [X1 : (a > $o)] : ((((X0 @ X1)) != $true) | ? [X2 : a] : (((X1 @ X2)) = $true)) & ! [X3 : a] : ? [X4 : (a > $o)] : (! [X5 : (a > $o)] : ((X4 = X5) | ($true != ((X5 @ X3))) | ($true != ((X0 @ X5)))) & (((X0 @ X4)) = $true) & (((X4 @ X3)) = $true)) & ! [X6 : (a > a > $o)] : (? [X7 : a,X8 : a] : (($true = ((X6 @ X8 @ X7))) & ($true != ((X6 @ X7 @ X8)))) | ? [X9 : a,X10 : a,X11 : a] : (($true = ((X6 @ X9 @ X11))) & ($true = ((X6 @ X11 @ X10))) & (((X6 @ X9 @ X10)) != $true)) | ((^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))) != X0) | ? [X12 : a] : ($true != ((X6 @ X12 @ X12)))))),
% 19.81/3.14 inference(rectify,[],[f8])).
% 19.81/3.14 thf(f10,plain,(
% 19.81/3.14 ! [X1 : (a > $o)] : ((((sK0 @ X1)) != $true) | (((X1 @ (sK1 @ X1))) = $true)) & ! [X3 : a] : (! [X5 : (a > $o)] : ((((sK2 @ X3)) = X5) | ($true != ((X5 @ X3))) | ($true != ((sK0 @ X5)))) & ($true = ((sK0 @ (sK2 @ X3)))) & (((sK2 @ X3 @ X3)) = $true)) & ! [X6 : (a > a > $o)] : ((($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6)))) & ($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6))))) | (($true = ((X6 @ (sK5 @ X6) @ (sK7 @ X6)))) & ($true = ((X6 @ (sK7 @ X6) @ (sK6 @ X6)))) & (((X6 @ (sK5 @ X6) @ (sK6 @ X6))) != $true)) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true))),
% 19.81/3.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X0,sK0),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6),skolemize(X12,sK8 @ X6)],[f9])).
% 19.81/3.14 thf(f11,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : (($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6)))) | (((X6 @ (sK5 @ X6) @ (sK6 @ X6))) != $true) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f12,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | ($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6)))) | ($true = ((X6 @ (sK7 @ X6) @ (sK6 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f13,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : (($true = ((X6 @ (sK5 @ X6) @ (sK7 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | ($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f14,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK5 @ X6) @ (sK6 @ X6))) != $true) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f15,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | ($true = ((X6 @ (sK7 @ X6) @ (sK6 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f16,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : (($true = ((X6 @ (sK5 @ X6) @ (sK7 @ X6)))) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: (Y0 @ Y1))) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f17,plain,(
% 19.81/3.14 ( ! [X3 : a] : ((((sK2 @ X3 @ X3)) = $true)) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f18,plain,(
% 19.81/3.14 ( ! [X3 : a] : (($true = ((sK0 @ (sK2 @ X3))))) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f19,plain,(
% 19.81/3.14 ( ! [X3 : a,X5 : (a > $o)] : (($true != ((X5 @ X3))) | ($true != ((sK0 @ X5))) | (((sK2 @ X3)) = X5)) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f20,plain,(
% 19.81/3.14 ( ! [X1 : (a > $o)] : ((((sK0 @ X1)) != $true) | (((X1 @ (sK1 @ X1))) = $true)) )),
% 19.81/3.14 inference(cnf_transformation,[],[f10])).
% 19.81/3.14 thf(f22,definition,(
% 19.81/3.14 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 19.81/3.14 introduced(theory,[fool_exhaustiveness_axiom])).
% 19.81/3.14 thf(f23,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6)))) | ($true = ((X6 @ (sK7 @ X6) @ (sK6 @ X6))))) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f12])).
% 19.81/3.14 thf(f24,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | ($true = ((X6 @ (sK5 @ X6) @ (sK7 @ X6)))) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))))) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f16])).
% 19.81/3.14 thf(f25,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : (($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true = ((X6 @ (sK5 @ X6) @ (sK7 @ X6)))) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true)) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f13])).
% 19.81/3.14 thf(f26,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true = ((X6 @ (sK7 @ X6) @ (sK6 @ X6)))) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6))))) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f15])).
% 19.81/3.14 thf(f27,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK5 @ X6) @ (sK6 @ X6))) != $true) | ($true != ((X6 @ (sK3 @ X6) @ (sK4 @ X6)))) | (((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2))))))))))) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f11])).
% 19.81/3.14 thf(f28,plain,(
% 19.81/3.14 ( ! [X6 : (a > a > $o)] : ((((X6 @ (sK8 @ X6) @ (sK8 @ X6))) != $true) | (((X6 @ (sK5 @ X6) @ (sK6 @ X6))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (X6 @ Y1 @ Y2)))))))))) | ($true = ((X6 @ (sK4 @ X6) @ (sK3 @ X6))))) )),
% 19.81/3.14 inference(beta-eta_normalization,[],[f14])).
% 19.81/3.14 thf(f36,plain,(
% 19.81/3.14 ( ! [X0 : a] : (($true != $true) | ($true = ((sK2 @ X0 @ (sK1 @ (sK2 @ X0)))))) )),
% 19.81/3.14 inference(constrained_superposition,[],[f20,f18])).
% 19.81/3.14 thf(f37,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((X0 @ (sK1 @ X0)))) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(constrained_superposition,[],[f20,f22])).
% 19.81/3.14 thf(f38,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : (($true = ((X0 @ (sK1 @ X0)))) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f37])).
% 19.81/3.14 thf(f39,plain,(
% 19.81/3.14 ( ! [X0 : a] : (($true = ((sK2 @ X0 @ (sK1 @ (sK2 @ X0)))))) )),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f36])).
% 19.81/3.14 thf(f41,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o),X1 : a] : (($true != ((sK0 @ X0))) | (((X0 @ X1)) = $false) | ($true != $true) | (((sK2 @ X1)) = X0)) )),
% 19.81/3.14 inference(constrained_superposition,[],[f19,f22])).
% 19.81/3.14 thf(f44,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o),X1 : a] : (($true != ((sK0 @ X0))) | (((sK2 @ X1)) = X0) | (((X0 @ X1)) = $false)) )),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f41])).
% 19.81/3.14 thf(f60,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : (($true != ((sK0 @ X0))) | ($true != $true) | (((sK0 @ X0)) = $false) | (((sK2 @ (sK1 @ X0))) = X0)) )),
% 19.81/3.14 inference(constrained_superposition,[],[f19,f38])).
% 19.81/3.14 thf(f61,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : ((((sK2 @ (sK1 @ X0))) = X0) | (((sK0 @ X0)) = $false) | ($true != ((sK0 @ X0)))) )),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f60])).
% 19.81/3.14 thf(f62,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : ((((sK2 @ (sK1 @ X0))) = X0) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f61,f22])).
% 19.81/3.14 thf(f64,plain,(
% 19.81/3.14 ($true != $true) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))))),
% 19.81/3.14 inference(constrained_superposition,[],[f23,f17])).
% 19.81/3.14 thf(f67,plain,(
% 19.81/3.14 (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))))),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f64])).
% 19.81/3.14 thf(f71,definition,(
% 19.81/3.14 spl9_3 <=> (sK0 = (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition])).
% 19.81/3.14 thf(f72,plain,(
% 19.81/3.14 (sK0 = (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ~spl9_3),
% 19.81/3.14 inference(avatar_component_clause,[],[f71])).
% 19.81/3.14 thf(f73,plain,(
% 19.81/3.14 (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | spl9_3),
% 19.81/3.14 inference(avatar_component_clause,[],[f71])).
% 19.81/3.14 thf(f75,definition,(
% 19.81/3.14 spl9_4 <=> ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition])).
% 19.81/3.14 thf(f77,plain,(
% 19.81/3.14 ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2)))) | ~spl9_4),
% 19.81/3.14 inference(avatar_component_clause,[],[f75])).
% 19.81/3.14 thf(f79,definition,(
% 19.81/3.14 spl9_5 <=> ($true = ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2))))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition])).
% 19.81/3.14 thf(f81,plain,(
% 19.81/3.14 ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | spl9_5),
% 19.81/3.14 inference(avatar_component_clause,[],[f79])).
% 19.81/3.14 thf(f82,plain,(
% 19.81/3.14 ~spl9_3 | spl9_4 | ~spl9_5),
% 19.81/3.14 inference(avatar_split_clause,[],[f67,f79,f75,f71])).
% 19.81/3.14 thf(f86,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o),X1 : a] : ((((sK2 @ (sK1 @ X0) @ X1)) = ((X0 @ X1))) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(argument_congruence,[],[f62])).
% 19.81/3.14 thf(f90,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o),X1 : a] : ((((sK2 @ (sK1 @ X0) @ X1)) = $false) | ($true = ((X0 @ X1))) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f86])).
% 19.81/3.14 thf(f98,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | ($true != $true)),
% 19.81/3.14 inference(constrained_superposition,[],[f24,f17])).
% 19.81/3.14 thf(f102,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f98])).
% 19.81/3.14 thf(f105,definition,(
% 19.81/3.14 spl9_6 <=> (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition])).
% 19.81/3.14 thf(f107,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | ~spl9_6),
% 19.81/3.14 inference(avatar_component_clause,[],[f105])).
% 19.81/3.14 thf(f109,definition,(
% 19.81/3.14 spl9_7 <=> (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition])).
% 19.81/3.14 thf(f111,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | ~spl9_7),
% 19.81/3.14 inference(avatar_component_clause,[],[f109])).
% 19.81/3.14 thf(f112,plain,(
% 19.81/3.14 spl9_6 | spl9_7 | ~spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f102,f71,f109,f105])).
% 19.81/3.14 thf(f190,plain,(
% 19.81/3.14 ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2)))) | ($true != $true) | (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))))),
% 19.81/3.14 inference(constrained_superposition,[],[f26,f17])).
% 19.81/3.14 thf(f193,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | ($true = ((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))))),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f190])).
% 19.81/3.14 thf(f197,plain,(
% 19.81/3.14 ~spl9_3 | spl9_7 | spl9_4),
% 19.81/3.14 inference(avatar_split_clause,[],[f193,f75,f109,f71])).
% 19.81/3.14 thf(f204,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((X0 @ (sK1 @ (sK2 @ (sK1 @ X0)))))) | ($true = $false)) )),
% 19.81/3.14 inference(constrained_superposition,[],[f39,f90])).
% 19.81/3.14 thf(f208,plain,(
% 19.81/3.14 ( ! [X0 : (a > $o)] : (($true = ((X0 @ (sK1 @ (sK2 @ (sK1 @ X0)))))) | (((sK0 @ X0)) = $false)) )),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f204])).
% 19.81/3.14 thf(f289,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) != $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true != $true) | (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true)),
% 19.81/3.14 inference(constrained_superposition,[],[f28,f17])).
% 19.81/3.14 thf(f294,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) != $true) | (((sK2 @ (sK4 @ sK2) @ (sK3 @ sK2))) = $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))))),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f289])).
% 19.81/3.14 thf(f297,definition,(
% 19.81/3.14 spl9_8 <=> (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition])).
% 19.81/3.14 thf(f299,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) != $true) | spl9_8),
% 19.81/3.14 inference(avatar_component_clause,[],[f297])).
% 19.81/3.14 thf(f300,plain,(
% 19.81/3.14 ~spl9_3 | ~spl9_8 | spl9_7),
% 19.81/3.14 inference(avatar_split_clause,[],[f294,f109,f297,f71])).
% 19.81/3.14 thf(f815,plain,(
% 19.81/3.14 ($true != $true) | (((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2))) = $false) | spl9_5),
% 19.81/3.14 inference(constrained_superposition,[],[f81,f22])).
% 19.81/3.14 thf(f816,plain,(
% 19.81/3.14 (((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2))) = $false) | spl9_5),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f815])).
% 19.81/3.14 thf(f825,plain,(
% 19.81/3.14 ($true != $true) | (((sK2 @ (sK3 @ sK2))) = ((sK2 @ (sK4 @ sK2)))) | ($true != ((sK0 @ (sK2 @ (sK4 @ sK2))))) | ~spl9_7),
% 19.81/3.14 inference(constrained_superposition,[],[f19,f111])).
% 19.81/3.14 thf(f826,plain,(
% 19.81/3.14 (((sK2 @ (sK3 @ sK2))) = ((sK2 @ (sK4 @ sK2)))) | ($true != ((sK0 @ (sK2 @ (sK4 @ sK2))))) | ~spl9_7),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f825])).
% 19.81/3.14 thf(f829,plain,(
% 19.81/3.14 (((sK2 @ (sK3 @ sK2))) = ((sK2 @ (sK4 @ sK2)))) | ~spl9_7),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f826,f18])).
% 19.81/3.14 thf(f980,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK2 @ (sK4 @ sK2) @ X1)) = ((sK2 @ (sK3 @ sK2) @ X1)))) ) | ~spl9_7),
% 19.81/3.14 inference(argument_congruence,[],[f829])).
% 19.81/3.14 thf(f987,plain,(
% 19.81/3.14 ( ! [X1 : a] : (($true = ((sK2 @ (sK3 @ sK2) @ X1))) | (((sK2 @ (sK4 @ sK2) @ X1)) = $false)) ) | ~spl9_7),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f980])).
% 19.81/3.14 thf(f1749,plain,(
% 19.81/3.14 ($true = $false) | (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(constrained_superposition,[],[f987,f816])).
% 19.81/3.14 thf(f1756,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | ($true = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(constrained_superposition,[],[f816,f987])).
% 19.81/3.14 thf(f1757,plain,(
% 19.81/3.14 ($true != $true) | (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true != ((sK2 @ (sK8 @ sK2) @ (sK8 @ sK2)))) | (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | ~spl9_7),
% 19.81/3.14 inference(constrained_superposition,[],[f25,f987])).
% 19.81/3.14 thf(f1766,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | ($true != ((sK2 @ (sK8 @ sK2) @ (sK8 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | ~spl9_7),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1757])).
% 19.81/3.14 thf(f1771,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1756])).
% 19.81/3.14 thf(f1776,plain,(
% 19.81/3.14 (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1749])).
% 19.81/3.14 thf(f1779,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | ~spl9_7),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f1766,f17])).
% 19.81/3.14 thf(f1782,plain,(
% 19.81/3.14 ($true = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(forward_demodulation,[],[f1771,f17])).
% 19.81/3.14 thf(f1783,plain,(
% 19.81/3.14 $false | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1782])).
% 19.81/3.14 thf(f1784,plain,(
% 19.81/3.14 spl9_5 | ~spl9_7),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f1783])).
% 19.81/3.14 thf(f1787,plain,(
% 19.81/3.14 ($true = $false) | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(forward_demodulation,[],[f1776,f17])).
% 19.81/3.14 thf(f1788,plain,(
% 19.81/3.14 $false | (spl9_5 | ~spl9_7)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1787])).
% 19.81/3.14 thf(f1789,plain,(
% 19.81/3.14 spl9_5 | ~spl9_7),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f1788])).
% 19.81/3.14 thf(f1791,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | (((sK2 @ (sK4 @ sK2) @ (sK4 @ sK2))) = $false) | (~spl9_3 | ~spl9_7)),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f1779,f72])).
% 19.81/3.14 thf(f1793,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | ($true = $false) | (~spl9_3 | ~spl9_7)),
% 19.81/3.14 inference(forward_demodulation,[],[f1791,f17])).
% 19.81/3.14 thf(f1794,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK7 @ sK2))) = $true) | (~spl9_3 | ~spl9_7)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1793])).
% 19.81/3.14 thf(f1795,plain,(
% 19.81/3.14 spl9_6 | ~spl9_3 | ~spl9_7),
% 19.81/3.14 inference(avatar_split_clause,[],[f1794,f109,f71,f105])).
% 19.81/3.14 thf(f1815,plain,(
% 19.81/3.14 ($true != ((sK0 @ (sK2 @ (sK5 @ sK2))))) | ($true != $true) | (((sK2 @ (sK5 @ sK2))) = ((sK2 @ (sK7 @ sK2)))) | ~spl9_6),
% 19.81/3.14 inference(constrained_superposition,[],[f19,f107])).
% 19.81/3.14 thf(f1817,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2))) = ((sK2 @ (sK7 @ sK2)))) | ($true != ((sK0 @ (sK2 @ (sK5 @ sK2))))) | ~spl9_6),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1815])).
% 19.81/3.14 thf(f1823,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2))) = ((sK2 @ (sK7 @ sK2)))) | ~spl9_6),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f1817,f18])).
% 19.81/3.14 thf(f1832,plain,(
% 19.81/3.14 ($true != $true) | (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) = $false) | spl9_8),
% 19.81/3.14 inference(constrained_superposition,[],[f299,f22])).
% 19.81/3.14 thf(f1833,plain,(
% 19.81/3.14 (((sK2 @ (sK5 @ sK2) @ (sK6 @ sK2))) = $false) | spl9_8),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1832])).
% 19.81/3.14 thf(f1857,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK2 @ (sK5 @ sK2) @ X1)) = ((sK2 @ (sK7 @ sK2) @ X1)))) ) | ~spl9_6),
% 19.81/3.14 inference(argument_congruence,[],[f1823])).
% 19.81/3.14 thf(f1869,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK2 @ (sK5 @ sK2) @ X1)) = $true) | (((sK2 @ (sK7 @ sK2) @ X1)) = $false)) ) | ~spl9_6),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f1857])).
% 19.81/3.14 thf(f1998,plain,(
% 19.81/3.14 (((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))) = $false) | ($true = $false) | (~spl9_6 | spl9_8)),
% 19.81/3.14 inference(constrained_superposition,[],[f1869,f1833])).
% 19.81/3.14 thf(f2004,plain,(
% 19.81/3.14 ($true != ((sK2 @ (sK8 @ sK2) @ (sK8 @ sK2)))) | (((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))) = $false) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true != $true) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | ~spl9_6),
% 19.81/3.14 inference(constrained_superposition,[],[f27,f1869])).
% 19.81/3.14 thf(f2020,plain,(
% 19.81/3.14 (((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))) = $false) | ($true != ((sK2 @ (sK8 @ sK2) @ (sK8 @ sK2)))) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ~spl9_6),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f2004])).
% 19.81/3.14 thf(f2021,plain,(
% 19.81/3.14 (((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))) = $false) | (~spl9_6 | spl9_8)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f1998])).
% 19.81/3.14 thf(f2033,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_4 | ~spl9_6 | spl9_8)),
% 19.81/3.14 inference(forward_demodulation,[],[f2021,f77])).
% 19.81/3.14 thf(f2034,plain,(
% 19.81/3.14 $false | (~spl9_4 | ~spl9_6 | spl9_8)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f2033])).
% 19.81/3.14 thf(f2035,plain,(
% 19.81/3.14 ~spl9_4 | ~spl9_6 | spl9_8),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f2034])).
% 19.81/3.14 thf(f2043,plain,(
% 19.81/3.14 (((sK2 @ (sK7 @ sK2) @ (sK6 @ sK2))) = $false) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ~spl9_6),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f2020,f17])).
% 19.81/3.14 thf(f2044,plain,(
% 19.81/3.14 ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true = $false) | (~spl9_4 | ~spl9_6)),
% 19.81/3.14 inference(forward_demodulation,[],[f2043,f77])).
% 19.81/3.14 thf(f2045,plain,(
% 19.81/3.14 (sK0 != (^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2)))))))))) | ($true != ((sK2 @ (sK3 @ sK2) @ (sK4 @ sK2)))) | (~spl9_4 | ~spl9_6)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f2044])).
% 19.81/3.14 thf(f2110,plain,(
% 19.81/3.14 ((((^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))) @ sK21)) != ((sK0 @ sK21))) | spl9_3),
% 19.81/3.14 inference(negative_extensionality,[],[f73])).
% 19.81/3.14 thf(f2111,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | ((((^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))) @ sK21)) = $true) | spl9_3),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f2110])).
% 19.81/3.14 thf(f2112,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | ((((^[Y0 : a > $o]: ((?? @ a @ Y0) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) = (sK2 @ Y1 @ Y2))))))))) @ sK21)) = $false) | spl9_3),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f2110])).
% 19.81/3.14 thf(f2113,plain,(
% 19.81/3.14 ((((?? @ a @ sK21) & (!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1))))))))) = $false) | (((sK0 @ sK21)) = $false) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2112])).
% 19.81/3.14 thf(f2114,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | (((!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1)))))))) = $false) | (((?? @ a @ sK21)) = $false) | spl9_3),
% 19.81/3.14 inference(and_proxy_clausification,[],[f2113])).
% 19.81/3.14 thf(f2115,plain,(
% 19.81/3.14 ((((^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1)))))) @ sK22)) = $false) | (((?? @ a @ sK21)) = $false) | (((sK0 @ sK21)) = $false) | spl9_3),
% 19.81/3.14 inference(sigma_proxy_clausification,[],[f2114])).
% 19.81/3.14 thf(f2116,plain,(
% 19.81/3.14 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1)))))) @ sK22)) = $false) | (((sK21 @ X1)) = $false) | (((sK0 @ sK21)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(pi_proxy_clausification,[],[f2115])).
% 19.81/3.14 thf(f2117,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ X1)) = $false) | ((((sK21 @ sK22) => (!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ sK22 @ Y0)))))) = $false) | (((sK0 @ sK21)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2116])).
% 19.81/3.14 thf(f2118,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK0 @ sK21)) = $false) | (((sK21 @ X1)) = $false) | (((!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ sK22 @ Y0))))) = $false)) ) | spl9_3),
% 19.81/3.14 inference(imp_proxy_clausification,[],[f2117])).
% 19.81/3.14 thf(f2119,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ sK22)) = $true) | (((sK21 @ X1)) = $false) | (((sK0 @ sK21)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(imp_proxy_clausification,[],[f2117])).
% 19.81/3.14 thf(f2120,plain,(
% 19.81/3.14 ( ! [X1 : a] : (((((^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ sK22 @ Y0))) @ sK23)) = $false) | (((sK0 @ sK21)) = $false) | (((sK21 @ X1)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(sigma_proxy_clausification,[],[f2118])).
% 19.81/3.14 thf(f2121,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ X1)) = $false) | ((((sK21 @ sK23) = (sK2 @ sK22 @ sK23))) = $false) | (((sK0 @ sK21)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2120])).
% 19.81/3.14 thf(f2122,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK2 @ sK22 @ sK23)) != ((sK21 @ sK23))) | (((sK0 @ sK21)) = $false) | (((sK21 @ X1)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f2121])).
% 19.81/3.14 thf(f2123,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK2 @ sK22 @ sK23)) = $true) | (((sK21 @ X1)) = $false) | ($true = ((sK21 @ sK23))) | (((sK0 @ sK21)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f2122])).
% 19.81/3.14 thf(f2124,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ sK23)) = $false) | (((sK0 @ sK21)) = $false) | (((sK2 @ sK22 @ sK23)) = $false) | (((sK21 @ X1)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f2122])).
% 19.81/3.14 thf(f2125,plain,(
% 19.81/3.14 ((((?? @ a @ sK21) & (!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1))))))))) = $true) | ($true = ((sK0 @ sK21))) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2111])).
% 19.81/3.14 thf(f2126,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | (((!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1)))))))) = $true) | spl9_3),
% 19.81/3.14 inference(and_proxy_clausification,[],[f2125])).
% 19.81/3.14 thf(f2127,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | ($true = ((?? @ a @ sK21))) | spl9_3),
% 19.81/3.14 inference(and_proxy_clausification,[],[f2125])).
% 19.81/3.14 thf(f2128,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | (((sK21 @ sK24)) = $true) | spl9_3),
% 19.81/3.14 inference(sigma_proxy_clausification,[],[f2127])).
% 19.81/3.14 thf(f2129,plain,(
% 19.81/3.14 ( ! [X1 : a] : (($true = ((sK0 @ sK21))) | ((((^[Y0 : a]: ((sK21 @ Y0) => (!! @ a @ (^[Y1 : a]: ((sK21 @ Y1) = (sK2 @ Y0 @ Y1)))))) @ X1)) = $true)) ) | spl9_3),
% 19.81/3.14 inference(pi_proxy_clausification,[],[f2126])).
% 19.81/3.14 thf(f2130,plain,(
% 19.81/3.14 ( ! [X1 : a] : (($true = (((sK21 @ X1) => (!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ X1 @ Y0))))))) | ($true = ((sK0 @ sK21)))) ) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2129])).
% 19.81/3.14 thf(f2131,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ X1)) = $false) | (((!! @ a @ (^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ X1 @ Y0))))) = $true) | ($true = ((sK0 @ sK21)))) ) | spl9_3),
% 19.81/3.14 inference(imp_proxy_clausification,[],[f2130])).
% 19.81/3.14 thf(f2132,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : ((((sK21 @ X1)) = $false) | ($true = ((sK0 @ sK21))) | ((((^[Y0 : a]: ((sK21 @ Y0) = (sK2 @ X1 @ Y0))) @ X2)) = $true)) ) | spl9_3),
% 19.81/3.14 inference(pi_proxy_clausification,[],[f2131])).
% 19.81/3.14 thf(f2133,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : (($true = ((sK0 @ sK21))) | ($true = (((sK21 @ X2) = (sK2 @ X1 @ X2)))) | (((sK21 @ X1)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(beta-eta_normalization,[],[f2132])).
% 19.81/3.14 thf(f2134,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : ((((sK21 @ X2)) = ((sK2 @ X1 @ X2))) | ($true = ((sK0 @ sK21))) | (((sK21 @ X1)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f2133])).
% 19.81/3.14 thf(f2135,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : ((((sK21 @ X2)) = $true) | (((sK21 @ X1)) = $false) | (((sK2 @ X1 @ X2)) = $false) | ($true = ((sK0 @ sK21)))) ) | spl9_3),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f2134])).
% 19.81/3.14 thf(f2136,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : ((((sK21 @ X1)) = $false) | ($true = ((sK2 @ X1 @ X2))) | ($true = ((sK0 @ sK21))) | (((sK21 @ X2)) = $false)) ) | spl9_3),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f2134])).
% 19.81/3.14 thf(f2138,definition,(
% 19.81/3.14 spl9_39 <=> ! [X1 : a] : (((sK21 @ X1)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_39])],[avatar_definition])).
% 19.81/3.14 thf(f2139,plain,(
% 19.81/3.14 ( ! [X1 : a] : ((((sK21 @ X1)) = $false)) ) | ~spl9_39),
% 19.81/3.14 inference(avatar_component_clause,[],[f2138])).
% 19.81/3.14 thf(f2141,definition,(
% 19.81/3.14 spl9_40 <=> (((sK0 @ sK21)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_40])],[avatar_definition])).
% 19.81/3.14 thf(f2143,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | ~spl9_40),
% 19.81/3.14 inference(avatar_component_clause,[],[f2141])).
% 19.81/3.14 thf(f2145,definition,(
% 19.81/3.14 spl9_41 <=> (((sK21 @ sK22)) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_41])],[avatar_definition])).
% 19.81/3.14 thf(f2147,plain,(
% 19.81/3.14 (((sK21 @ sK22)) = $true) | ~spl9_41),
% 19.81/3.14 inference(avatar_component_clause,[],[f2145])).
% 19.81/3.14 thf(f2148,plain,(
% 19.81/3.14 spl9_39 | spl9_40 | spl9_41 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2119,f71,f2145,f2141,f2138])).
% 19.81/3.14 thf(f2150,definition,(
% 19.81/3.14 spl9_42 <=> (((sK2 @ sK22 @ sK23)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_42])],[avatar_definition])).
% 19.81/3.14 thf(f2152,plain,(
% 19.81/3.14 (((sK2 @ sK22 @ sK23)) = $false) | ~spl9_42),
% 19.81/3.14 inference(avatar_component_clause,[],[f2150])).
% 19.81/3.14 thf(f2154,definition,(
% 19.81/3.14 spl9_43 <=> (((sK21 @ sK23)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_43])],[avatar_definition])).
% 19.81/3.14 thf(f2155,plain,(
% 19.81/3.14 (((sK21 @ sK23)) != $false) | spl9_43),
% 19.81/3.14 inference(avatar_component_clause,[],[f2154])).
% 19.81/3.14 thf(f2156,plain,(
% 19.81/3.14 (((sK21 @ sK23)) = $false) | ~spl9_43),
% 19.81/3.14 inference(avatar_component_clause,[],[f2154])).
% 19.81/3.14 thf(f2157,plain,(
% 19.81/3.14 spl9_42 | spl9_43 | spl9_40 | spl9_39 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2124,f71,f2138,f2141,f2154,f2150])).
% 19.81/3.14 thf(f2159,definition,(
% 19.81/3.14 spl9_44 <=> (((sK2 @ sK22 @ sK23)) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_44])],[avatar_definition])).
% 19.81/3.14 thf(f2161,plain,(
% 19.81/3.14 (((sK2 @ sK22 @ sK23)) = $true) | ~spl9_44),
% 19.81/3.14 inference(avatar_component_clause,[],[f2159])).
% 19.81/3.14 thf(f2163,definition,(
% 19.81/3.14 spl9_45 <=> ($true = ((sK21 @ sK23)))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_45])],[avatar_definition])).
% 19.81/3.14 thf(f2165,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK23))) | ~spl9_45),
% 19.81/3.14 inference(avatar_component_clause,[],[f2163])).
% 19.81/3.14 thf(f2166,plain,(
% 19.81/3.14 spl9_44 | spl9_39 | spl9_40 | spl9_45 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2123,f71,f2163,f2141,f2138,f2159])).
% 19.81/3.14 thf(f2168,definition,(
% 19.81/3.14 spl9_46 <=> ($true = ((sK0 @ sK21)))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_46])],[avatar_definition])).
% 19.81/3.14 thf(f2169,plain,(
% 19.81/3.14 ($true != ((sK0 @ sK21))) | spl9_46),
% 19.81/3.14 inference(avatar_component_clause,[],[f2168])).
% 19.81/3.14 thf(f2170,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | ~spl9_46),
% 19.81/3.14 inference(avatar_component_clause,[],[f2168])).
% 19.81/3.14 thf(f2172,definition,(
% 19.81/3.14 spl9_47 <=> (((sK21 @ sK24)) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_47])],[avatar_definition])).
% 19.81/3.14 thf(f2174,plain,(
% 19.81/3.14 (((sK21 @ sK24)) = $true) | ~spl9_47),
% 19.81/3.14 inference(avatar_component_clause,[],[f2172])).
% 19.81/3.14 thf(f2175,plain,(
% 19.81/3.14 spl9_46 | spl9_47 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2128,f71,f2172,f2168])).
% 19.81/3.14 thf(f2177,definition,(
% 19.81/3.14 spl9_48 <=> ! [X2 : a,X1 : a] : ((((sK21 @ X1)) = $false) | (((sK21 @ X2)) = $false) | ($true = ((sK2 @ X1 @ X2))))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_48])],[avatar_definition])).
% 19.81/3.14 thf(f2178,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : (($true = ((sK2 @ X1 @ X2))) | (((sK21 @ X2)) = $false) | (((sK21 @ X1)) = $false)) ) | ~spl9_48),
% 19.81/3.14 inference(avatar_component_clause,[],[f2177])).
% 19.81/3.14 thf(f2179,plain,(
% 19.81/3.14 spl9_48 | spl9_46 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2136,f71,f2168,f2177])).
% 19.81/3.14 thf(f2181,definition,(
% 19.81/3.14 spl9_49 <=> ! [X2 : a,X1 : a] : ((((sK21 @ X2)) = $true) | (((sK21 @ X1)) = $false) | (((sK2 @ X1 @ X2)) = $false))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_49])],[avatar_definition])).
% 19.81/3.14 thf(f2182,plain,(
% 19.81/3.14 ( ! [X2 : a,X1 : a] : ((((sK2 @ X1 @ X2)) = $false) | (((sK21 @ X2)) = $true) | (((sK21 @ X1)) = $false)) ) | ~spl9_49),
% 19.81/3.14 inference(avatar_component_clause,[],[f2181])).
% 19.81/3.14 thf(f2183,plain,(
% 19.81/3.14 spl9_46 | spl9_49 | spl9_3),
% 19.81/3.14 inference(avatar_split_clause,[],[f2135,f71,f2181,f2168])).
% 19.81/3.14 thf(f2192,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | ($true = $false) | ~spl9_39),
% 19.81/3.14 inference(constrained_superposition,[],[f208,f2139])).
% 19.81/3.14 thf(f2195,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | ~spl9_39),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f2192])).
% 19.81/3.14 thf(f2203,plain,(
% 19.81/3.14 spl9_40 | ~spl9_39),
% 19.81/3.14 inference(avatar_split_clause,[],[f2195,f2138,f2141])).
% 19.81/3.14 thf(f2225,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_40 | ~spl9_46)),
% 19.81/3.14 inference(forward_demodulation,[],[f2170,f2143])).
% 19.81/3.14 thf(f2226,plain,(
% 19.81/3.14 $false | (~spl9_40 | ~spl9_46)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f2225])).
% 19.81/3.14 thf(f2227,plain,(
% 19.81/3.14 ~spl9_40 | ~spl9_46),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f2226])).
% 19.81/3.14 thf(f4043,definition,(
% 19.81/3.14 spl9_114 <=> (sK21 = ((sK2 @ sK24)))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_114])],[avatar_definition])).
% 19.81/3.14 thf(f4044,plain,(
% 19.81/3.14 (sK21 != ((sK2 @ sK24))) | spl9_114),
% 19.81/3.14 inference(avatar_component_clause,[],[f4043])).
% 19.81/3.14 thf(f4045,plain,(
% 19.81/3.14 (sK21 = ((sK2 @ sK24))) | ~spl9_114),
% 19.81/3.14 inference(avatar_component_clause,[],[f4043])).
% 19.81/3.14 thf(f4064,plain,(
% 19.81/3.14 ( ! [X0 : a] : ((((sK21 @ X0)) = $false) | ($true != $true) | (((sK2 @ X0)) = sK21)) ) | ~spl9_46),
% 19.81/3.14 inference(constrained_superposition,[],[f44,f2170])).
% 19.81/3.14 thf(f4066,plain,(
% 19.81/3.14 ( ! [X0 : a] : ((((sK2 @ X0)) = sK21) | (((sK21 @ X0)) = $false)) ) | ~spl9_46),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4064])).
% 19.81/3.14 thf(f4077,plain,(
% 19.81/3.14 ($true = ((sK0 @ sK21))) | ~spl9_114),
% 19.81/3.14 inference(constrained_superposition,[],[f18,f4045])).
% 19.81/3.14 thf(f4187,plain,(
% 19.81/3.14 ( ! [X0 : a,X1 : a] : ((((sK21 @ X0)) = $false) | (((sK2 @ X0 @ X1)) = ((sK21 @ X1)))) ) | ~spl9_46),
% 19.81/3.14 inference(argument_congruence,[],[f4066])).
% 19.81/3.14 thf(f4220,plain,(
% 19.81/3.14 ( ! [X0 : a,X1 : a] : ((((sK21 @ X1)) = $false) | (((sK21 @ X0)) = $false) | ($true = ((sK2 @ X0 @ X1)))) ) | ~spl9_46),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f4187])).
% 19.81/3.14 thf(f4221,plain,(
% 19.81/3.14 ( ! [X0 : a,X1 : a] : ((((sK21 @ X0)) = $false) | ($true = ((sK21 @ X1))) | (((sK2 @ X0 @ X1)) = $false)) ) | ~spl9_46),
% 19.81/3.14 inference(iff_proxy_clausification,[],[f4187])).
% 19.81/3.14 thf(f4230,plain,(
% 19.81/3.14 spl9_49 | ~spl9_46),
% 19.81/3.14 inference(avatar_split_clause,[],[f4221,f2168,f2181])).
% 19.81/3.14 thf(f4231,plain,(
% 19.81/3.14 spl9_48 | ~spl9_46),
% 19.81/3.14 inference(avatar_split_clause,[],[f4220,f2168,f2177])).
% 19.81/3.14 thf(f4233,plain,(
% 19.81/3.14 spl9_46 | ~spl9_114),
% 19.81/3.14 inference(avatar_split_clause,[],[f4077,f4043,f2168])).
% 19.81/3.14 thf(f4241,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | ($true != $true) | spl9_46),
% 19.81/3.14 inference(constrained_superposition,[],[f2169,f22])).
% 19.81/3.14 thf(f4242,plain,(
% 19.81/3.14 (((sK0 @ sK21)) = $false) | spl9_46),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4241])).
% 19.81/3.14 thf(f4245,plain,(
% 19.81/3.14 spl9_40 | spl9_46),
% 19.81/3.14 inference(avatar_split_clause,[],[f4242,f2168,f2141])).
% 19.81/3.14 thf(f4252,plain,(
% 19.81/3.14 (((sK2 @ sK24 @ sK28)) != ((sK21 @ sK28))) | spl9_114),
% 19.81/3.14 inference(negative_extensionality,[],[f4044])).
% 19.81/3.14 thf(f4253,plain,(
% 19.81/3.14 (((sK2 @ sK24 @ sK28)) = $true) | ($true = ((sK21 @ sK28))) | spl9_114),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f4252])).
% 19.81/3.14 thf(f4254,plain,(
% 19.81/3.14 (((sK21 @ sK28)) = $false) | (((sK2 @ sK24 @ sK28)) = $false) | spl9_114),
% 19.81/3.14 inference(xor_proxy_clausification,[],[f4252])).
% 19.81/3.14 thf(f4256,definition,(
% 19.81/3.14 spl9_123 <=> (((sK2 @ sK24 @ sK28)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_123])],[avatar_definition])).
% 19.81/3.14 thf(f4257,plain,(
% 19.81/3.14 (((sK2 @ sK24 @ sK28)) != $false) | spl9_123),
% 19.81/3.14 inference(avatar_component_clause,[],[f4256])).
% 19.81/3.14 thf(f4258,plain,(
% 19.81/3.14 (((sK2 @ sK24 @ sK28)) = $false) | ~spl9_123),
% 19.81/3.14 inference(avatar_component_clause,[],[f4256])).
% 19.81/3.14 thf(f4260,definition,(
% 19.81/3.14 spl9_124 <=> (((sK21 @ sK28)) = $false)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_124])],[avatar_definition])).
% 19.81/3.14 thf(f4262,plain,(
% 19.81/3.14 (((sK21 @ sK28)) = $false) | ~spl9_124),
% 19.81/3.14 inference(avatar_component_clause,[],[f4260])).
% 19.81/3.14 thf(f4263,plain,(
% 19.81/3.14 spl9_123 | spl9_124 | spl9_114),
% 19.81/3.14 inference(avatar_split_clause,[],[f4254,f4043,f4260,f4256])).
% 19.81/3.14 thf(f4265,definition,(
% 19.81/3.14 spl9_125 <=> ($true = ((sK21 @ sK28)))),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_125])],[avatar_definition])).
% 19.81/3.14 thf(f4267,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK28))) | ~spl9_125),
% 19.81/3.14 inference(avatar_component_clause,[],[f4265])).
% 19.81/3.14 thf(f4269,definition,(
% 19.81/3.14 spl9_126 <=> (((sK2 @ sK24 @ sK28)) = $true)),
% 19.81/3.14 introduced(definition,[new_symbols(definition,[spl9_126])],[avatar_definition])).
% 19.81/3.14 thf(f4271,plain,(
% 19.81/3.14 (((sK2 @ sK24 @ sK28)) = $true) | ~spl9_126),
% 19.81/3.14 inference(avatar_component_clause,[],[f4269])).
% 19.81/3.14 thf(f4272,plain,(
% 19.81/3.14 spl9_125 | spl9_126 | spl9_114),
% 19.81/3.14 inference(avatar_split_clause,[],[f4253,f4043,f4269,f4265])).
% 19.81/3.14 thf(f4334,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_123 | ~spl9_126)),
% 19.81/3.14 inference(forward_demodulation,[],[f4271,f4258])).
% 19.81/3.14 thf(f4335,plain,(
% 19.81/3.14 $false | (~spl9_123 | ~spl9_126)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4334])).
% 19.81/3.14 thf(f4336,plain,(
% 19.81/3.14 ~spl9_123 | ~spl9_126),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4335])).
% 19.81/3.14 thf(f4367,plain,(
% 19.81/3.14 (((sK21 @ sK24)) = $false) | ($true = $false) | (((sK21 @ sK28)) = $false) | (~spl9_48 | ~spl9_123)),
% 19.81/3.14 inference(constrained_superposition,[],[f4258,f2178])).
% 19.81/3.14 thf(f4372,plain,(
% 19.81/3.14 (((sK21 @ sK28)) = $false) | (((sK21 @ sK24)) = $false) | (~spl9_48 | ~spl9_123)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4367])).
% 19.81/3.14 thf(f4408,plain,(
% 19.81/3.14 ($true = $false) | (((sK21 @ sK28)) = $false) | (~spl9_47 | ~spl9_48 | ~spl9_123)),
% 19.81/3.14 inference(forward_demodulation,[],[f4372,f2174])).
% 19.81/3.14 thf(f4409,plain,(
% 19.81/3.14 (((sK21 @ sK28)) = $false) | (~spl9_47 | ~spl9_48 | ~spl9_123)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4408])).
% 19.81/3.14 thf(f4419,plain,(
% 19.81/3.14 spl9_124 | ~spl9_47 | ~spl9_48 | ~spl9_123),
% 19.81/3.14 inference(avatar_split_clause,[],[f4409,f4256,f2177,f2172,f4260])).
% 19.81/3.14 thf(f4423,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_124 | ~spl9_125)),
% 19.81/3.14 inference(forward_demodulation,[],[f4267,f4262])).
% 19.81/3.14 thf(f4424,plain,(
% 19.81/3.14 $false | (~spl9_124 | ~spl9_125)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4423])).
% 19.81/3.14 thf(f4425,plain,(
% 19.81/3.14 ~spl9_124 | ~spl9_125),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4424])).
% 19.81/3.14 thf(f4449,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK23))) | ($true = $false) | (((sK21 @ sK22)) = $false) | (~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(constrained_superposition,[],[f2182,f2161])).
% 19.81/3.14 thf(f4477,plain,(
% 19.81/3.14 (((sK21 @ sK24)) = $false) | ($true = ((sK21 @ sK28))) | ($false != $false) | (~spl9_49 | spl9_123)),
% 19.81/3.14 inference(constrained_superposition,[],[f4257,f2182])).
% 19.81/3.14 thf(f4516,plain,(
% 19.81/3.14 (((sK21 @ sK24)) = $false) | ($true = ((sK21 @ sK28))) | (~spl9_49 | spl9_123)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4477])).
% 19.81/3.14 thf(f4525,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK23))) | (((sK21 @ sK22)) = $false) | (~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4449])).
% 19.81/3.14 thf(f4541,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK28))) | ($true = $false) | (~spl9_47 | ~spl9_49 | spl9_123)),
% 19.81/3.14 inference(forward_demodulation,[],[f4516,f2174])).
% 19.81/3.14 thf(f4542,plain,(
% 19.81/3.14 ($true = ((sK21 @ sK28))) | (~spl9_47 | ~spl9_49 | spl9_123)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4541])).
% 19.81/3.14 thf(f4545,plain,(
% 19.81/3.14 (((sK21 @ sK22)) = $false) | ($true = $false) | (~spl9_43 | ~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(forward_demodulation,[],[f4525,f2156])).
% 19.81/3.14 thf(f4546,plain,(
% 19.81/3.14 (((sK21 @ sK22)) = $false) | (~spl9_43 | ~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4545])).
% 19.81/3.14 thf(f4552,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_47 | ~spl9_49 | spl9_123 | ~spl9_124)),
% 19.81/3.14 inference(forward_demodulation,[],[f4542,f4262])).
% 19.81/3.14 thf(f4553,plain,(
% 19.81/3.14 $false | (~spl9_47 | ~spl9_49 | spl9_123 | ~spl9_124)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4552])).
% 19.81/3.14 thf(f4554,plain,(
% 19.81/3.14 ~spl9_47 | ~spl9_49 | spl9_123 | ~spl9_124),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4553])).
% 19.81/3.14 thf(f4555,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_41 | ~spl9_43 | ~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(forward_demodulation,[],[f4546,f2147])).
% 19.81/3.14 thf(f4556,plain,(
% 19.81/3.14 $false | (~spl9_41 | ~spl9_43 | ~spl9_44 | ~spl9_49)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4555])).
% 19.81/3.14 thf(f4557,plain,(
% 19.81/3.14 ~spl9_41 | ~spl9_43 | ~spl9_44 | ~spl9_49),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4556])).
% 19.81/3.14 thf(f4558,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_43 | ~spl9_45)),
% 19.81/3.14 inference(forward_demodulation,[],[f2165,f2156])).
% 19.81/3.14 thf(f4559,plain,(
% 19.81/3.14 $false | (~spl9_43 | ~spl9_45)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4558])).
% 19.81/3.14 thf(f4560,plain,(
% 19.81/3.14 ~spl9_43 | ~spl9_45),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4559])).
% 19.81/3.14 thf(f4603,plain,(
% 19.81/3.14 ($true = $false) | (((sK21 @ sK22)) = $false) | (((sK21 @ sK23)) = $false) | (~spl9_42 | ~spl9_48)),
% 19.81/3.14 inference(constrained_superposition,[],[f2152,f2178])).
% 19.81/3.14 thf(f4613,plain,(
% 19.81/3.14 (((sK21 @ sK23)) = $false) | (((sK21 @ sK22)) = $false) | (~spl9_42 | ~spl9_48)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4603])).
% 19.81/3.14 thf(f4619,plain,(
% 19.81/3.14 (((sK21 @ sK22)) = $false) | (~spl9_42 | spl9_43 | ~spl9_48)),
% 19.81/3.14 inference(forward_subsumption_resolution,[],[f4613,f2155])).
% 19.81/3.14 thf(f4624,plain,(
% 19.81/3.14 ($true = $false) | (~spl9_41 | ~spl9_42 | spl9_43 | ~spl9_48)),
% 19.81/3.14 inference(forward_demodulation,[],[f4619,f2147])).
% 19.81/3.14 thf(f4625,plain,(
% 19.81/3.14 $false | (~spl9_41 | ~spl9_42 | spl9_43 | ~spl9_48)),
% 19.81/3.14 inference(trivial_inequality_removal,[],[f4624])).
% 19.81/3.14 thf(f4626,plain,(
% 19.81/3.14 ~spl9_41 | ~spl9_42 | spl9_43 | ~spl9_48),
% 19.81/3.14 inference(avatar_contradiction_clause,[],[f4625])).
% 19.81/3.14 thf(f4628,plain,(
% 19.81/3.14 ~spl9_5 | ~spl9_3 | ~spl9_4 | ~spl9_6),
% 19.81/3.14 inference(avatar_split_clause,[],[f2045,f105,f75,f71,f79])).
% 19.81/3.14 cnf(s2, plain, ~spl9_3 | spl9_4 | ~spl9_5, inference(sat_conversion,[],[f82])).
% 19.81/3.14 cnf(s3, plain, ~spl9_3 | spl9_6 | spl9_7, inference(sat_conversion,[],[f112])).
% 19.81/3.14 cnf(s4, plain, ~spl9_3 | spl9_4 | spl9_7, inference(sat_conversion,[],[f197])).
% 19.81/3.14 cnf(s5, plain, ~spl9_3 | spl9_7 | ~spl9_8, inference(sat_conversion,[],[f300])).
% 19.81/3.14 cnf(s47, plain, spl9_5 | ~spl9_7, inference(sat_conversion,[],[f1784])).
% 19.81/3.14 cnf(s48, plain, spl9_5 | ~spl9_7, inference(sat_conversion,[],[f1789])).
% 19.81/3.14 cnf(s49, plain, ~spl9_3 | spl9_6 | ~spl9_7, inference(sat_conversion,[],[f1795])).
% 19.81/3.14 cnf(s51, plain, ~spl9_4 | ~spl9_6 | spl9_8, inference(sat_conversion,[],[f2035])).
% 19.81/3.14 cnf(s60, plain, spl9_3 | spl9_39 | spl9_40 | spl9_41, inference(sat_conversion,[],[f2148])).
% 19.81/3.14 cnf(s61, plain, spl9_3 | spl9_39 | spl9_40 | spl9_42 | spl9_43, inference(sat_conversion,[],[f2157])).
% 19.81/3.14 cnf(s62, plain, spl9_3 | spl9_39 | spl9_40 | spl9_44 | spl9_45, inference(sat_conversion,[],[f2166])).
% 19.81/3.14 cnf(s63, plain, spl9_3 | spl9_46 | spl9_47, inference(sat_conversion,[],[f2175])).
% 19.81/3.14 cnf(s64, plain, spl9_3 | spl9_46 | spl9_48, inference(sat_conversion,[],[f2179])).
% 19.81/3.14 cnf(s65, plain, spl9_3 | spl9_46 | spl9_49, inference(sat_conversion,[],[f2183])).
% 19.81/3.14 cnf(s66, plain, ~spl9_39 | spl9_40, inference(sat_conversion,[],[f2203])).
% 19.81/3.14 cnf(s73, plain, ~spl9_40 | ~spl9_46, inference(sat_conversion,[],[f2227])).
% 19.81/3.14 cnf(s280, plain, ~spl9_46 | spl9_49, inference(sat_conversion,[],[f4230])).
% 19.81/3.14 cnf(s281, plain, ~spl9_46 | spl9_48, inference(sat_conversion,[],[f4231])).
% 19.81/3.14 cnf(s282, plain, spl9_46 | ~spl9_114, inference(sat_conversion,[],[f4233])).
% 19.81/3.14 cnf(s288, plain, spl9_40 | spl9_46, inference(sat_conversion,[],[f4245])).
% 19.81/3.14 cnf(s289, plain, spl9_114 | spl9_123 | spl9_124, inference(sat_conversion,[],[f4263])).
% 19.81/3.14 cnf(s290, plain, spl9_114 | spl9_125 | spl9_126, inference(sat_conversion,[],[f4272])).
% 19.81/3.14 cnf(s297, plain, ~spl9_123 | ~spl9_126, inference(sat_conversion,[],[f4336])).
% 19.81/3.14 cnf(s300, plain, ~spl9_47 | ~spl9_48 | ~spl9_123 | spl9_124, inference(sat_conversion,[],[f4419])).
% 19.81/3.14 cnf(s302, plain, ~spl9_124 | ~spl9_125, inference(sat_conversion,[],[f4425])).
% 19.81/3.14 cnf(s306, plain, ~spl9_47 | ~spl9_49 | spl9_123 | ~spl9_124, inference(sat_conversion,[],[f4554])).
% 19.81/3.14 cnf(s307, plain, ~spl9_41 | ~spl9_43 | ~spl9_44 | ~spl9_49, inference(sat_conversion,[],[f4557])).
% 19.81/3.14 cnf(s308, plain, ~spl9_43 | ~spl9_45, inference(sat_conversion,[],[f4560])).
% 19.81/3.14 cnf(s319, plain, ~spl9_41 | ~spl9_42 | spl9_43 | ~spl9_48, inference(sat_conversion,[],[f4626])).
% 19.81/3.14 cnf(s321, plain, ~spl9_3 | ~spl9_4 | ~spl9_5 | ~spl9_6, inference(sat_conversion,[],[f4628])).
% 19.81/3.14 cnf(s332, plain, ~spl9_43 | spl9_40 | spl9_39 | spl9_3, inference(rat,[],[s62,s307,s308,s60,s280,s288])).
% 19.81/3.14 cnf(s333, plain, spl9_40 | spl9_39 | spl9_3, inference(rat,[],[s319,s61,s332,s281,s60,s288])).
% 19.81/3.14 cnf(s338, plain, spl9_123 | ~spl9_47 | ~spl9_49 | spl9_114, inference(rat,[],[s306,s289])).
% 19.81/3.14 cnf(s339, plain, spl9_46 | spl9_3, inference(rat,[],[s302,s290,s300,s297,s338,s63,s64,s65,s282])).
% 19.81/3.14 cnf(s340, plain, spl9_3, inference(rat,[],[s333,s66,s73,s339])).
% 19.81/3.14 cnf(s341, plain, spl9_4, inference(rat,[],[s47,s2,s4,s340])).
% 19.81/3.14 cnf(s342, plain, spl9_7, inference(rat,[],[s51,s3,s5,s341,s340])).
% 19.81/3.14 cnf(s343, plain, spl9_5, inference(rat,[],[s48,s342])).
% 19.81/3.14 cnf(s344, plain, spl9_6, inference(rat,[],[s49,s340,s342])).
% 19.81/3.14 cnf(s346, plain, $false, inference(rat,[],[s321,s341,s340,s343,s344])).
% 19.81/3.14 thf(f4641,plain,(
% 19.81/3.14 $false),
% 19.81/3.14 inference(avatar_sat_refutation,[],[s346])).
% 19.81/3.14 % SZS output end Proof for theBenchmark
% 19.81/3.14 % (3471348)------------------------------
% 19.81/3.14 % (3471348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.81/3.14 % (3471348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.14 % (3471348)CaDiCaL version: 2.1.3
% 19.81/3.14 % (3471348)Termination reason: Refutation
% 19.81/3.14 % (3471348)Time elapsed: 0.151 s
% 19.81/3.14 % (3471348)Peak memory usage: 14 MB
% 19.81/3.14 % (3471348)Instructions burned: 275 (million)
% 19.81/3.14 % (3471076)Success in time 2.881 s
% 19.81/3.14 % Vampire exiting
%------------------------------------------------------------------------------