%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU997^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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:32:06 AM UTC 2026
% Result : Theorem 0.78s 0.49s
% Output : Refutation 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU997^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.10/0.19 % Computer : n009.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 14:57:30 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running higher-order theorem proving
% 0.10/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.78/0.39 % (4107166)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.78/0.39 % (4107177)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.78/0.39 % (4107177)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.78/0.39 % (4107172)lrs+10_16_si=on:nwc=1.5:random_seed=811751515:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.78/0.39 % (4107175)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=403774398:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.78/0.39 % (4107173)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3960006330:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.78/0.39 % (4107176)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=819206610:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.78/0.39 % (4107171)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2758682742:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.78/0.39 % (4107174)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=1106038131: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.78/0.39 % (4107177)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=2508195735:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.78/0.39 % (4107173)Instruction limit reached!
% 0.78/0.39 % (4107173)------------------------------
% 0.78/0.39 % (4107173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (4107173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (4107173)CaDiCaL version: 2.1.3
% 0.78/0.39 % (4107173)Termination reason: Instruction limit
% 0.78/0.39 % (4107173)Termination phase: Saturation
% 0.78/0.39 % (4107173)Time elapsed: 0.002 s
% 0.78/0.39 % (4107173)Peak memory usage: 11 MB
% 0.78/0.39 % (4107173)Instructions burned: 3 (million)
% 0.78/0.39 % (4107172)Instruction limit reached!
% 0.78/0.39 % (4107172)------------------------------
% 0.78/0.39 % (4107172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (4107172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (4107172)CaDiCaL version: 2.1.3
% 0.78/0.39 % (4107172)Termination reason: Instruction limit
% 0.78/0.39 % (4107172)Termination phase: Saturation
% 0.78/0.39 % (4107172)Time elapsed: 0.010 s
% 0.78/0.39 % (4107172)Peak memory usage: 12 MB
% 0.78/0.39 % (4107172)Instructions burned: 18 (million)
% 0.78/0.39 % (4107175)Instruction limit reached!
% 0.78/0.39 % (4107175)------------------------------
% 0.78/0.39 % (4107175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (4107175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (4107175)CaDiCaL version: 2.1.3
% 0.78/0.39 % (4107175)Termination reason: Instruction limit
% 0.78/0.39 % (4107175)Termination phase: Saturation
% 0.78/0.39 % (4107175)Time elapsed: 0.013 s
% 0.78/0.39 % (4107175)Peak memory usage: 11 MB
% 0.78/0.39 % (4107175)Instructions burned: 24 (million)
% 0.78/0.39 % (4107185)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3858481972:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.78/0.39 % (4107185)Instruction limit reached!
% 0.78/0.39 % (4107185)------------------------------
% 0.78/0.39 % (4107185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.39 % (4107185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.39 % (4107185)CaDiCaL version: 2.1.3
% 0.78/0.39 % (4107185)Termination reason: Instruction limit
% 0.78/0.39 % (4107185)Termination phase: Saturation
% 0.78/0.39 % (4107185)Time elapsed: 0.002 s
% 0.78/0.39 % (4107185)Peak memory usage: 12 MB
% 0.78/0.39 % (4107185)Instructions burned: 3 (million)
% 0.78/0.39 % (4107187)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.78/0.43 % (4107186)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1963253737:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.78/0.43 % (4107187)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=586320593:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.78/0.43 % (4107186)Instruction limit reached!
% 0.78/0.43 % (4107186)------------------------------
% 0.78/0.43 % (4107186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.43 % (4107186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.43 % (4107186)CaDiCaL version: 2.1.3
% 0.78/0.43 % (4107186)Termination reason: Instruction limit
% 0.78/0.43 % (4107186)Termination phase: Saturation
% 0.78/0.43 % (4107186)Time elapsed: 0.004 s
% 0.78/0.43 % (4107186)Peak memory usage: 12 MB
% 0.78/0.43 % (4107186)Instructions burned: 6 (million)
% 0.78/0.43 % (4107187)Instruction limit reached!
% 0.78/0.43 % (4107187)------------------------------
% 0.78/0.43 % (4107187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.43 % (4107187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.43 % (4107187)CaDiCaL version: 2.1.3
% 0.78/0.43 % (4107187)Termination reason: Instruction limit
% 0.78/0.43 % (4107187)Termination phase: Saturation
% 0.78/0.43 % (4107187)Time elapsed: 0.004 s
% 0.78/0.43 % (4107187)Peak memory usage: 12 MB
% 0.78/0.43 % (4107187)Instructions burned: 9 (million)
% 0.78/0.43 % (4107176)Instruction limit reached!
% 0.78/0.43 % (4107176)------------------------------
% 0.78/0.43 % (4107176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.43 % (4107176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.43 % (4107176)CaDiCaL version: 2.1.3
% 0.78/0.43 % (4107176)Termination reason: Instruction limit
% 0.78/0.43 % (4107176)Termination phase: Saturation
% 0.78/0.43 % (4107176)Time elapsed: 0.039 s
% 0.78/0.43 % (4107176)Peak memory usage: 12 MB
% 0.78/0.43 % (4107176)Instructions burned: 75 (million)
% 0.78/0.43 % (4107189)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2663360754:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.78/0.43 % (4107171)Instruction limit reached!
% 0.78/0.43 % (4107171)------------------------------
% 0.78/0.43 % (4107171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.43 % (4107171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.43 % (4107171)CaDiCaL version: 2.1.3
% 0.78/0.43 % (4107171)Termination reason: Instruction limit
% 0.78/0.43 % (4107171)Termination phase: Saturation
% 0.78/0.43 % (4107171)Time elapsed: 0.045 s
% 0.78/0.43 % (4107171)Peak memory usage: 12 MB
% 0.78/0.43 % (4107171)Instructions burned: 89 (million)
% 0.78/0.43 % (4107189)Instruction limit reached!
% 0.78/0.43 % (4107189)------------------------------
% 0.78/0.43 % (4107189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.43 % (4107189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.43 % (4107189)CaDiCaL version: 2.1.3
% 0.78/0.43 % (4107189)Termination reason: Instruction limit
% 0.78/0.43 % (4107189)Termination phase: Saturation
% 0.78/0.43 % (4107189)Time elapsed: 0.008 s
% 0.78/0.43 % (4107189)Peak memory usage: 12 MB
% 0.78/0.43 % (4107189)Instructions burned: 14 (million)
% 0.78/0.43 % (4107193)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=1514023209:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.78/0.43 % (4107194)lrs+10_1_si=on:cs=on:random_seed=2045488814:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.78/0.43 % (4107192)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.78/0.43 % (4107192)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.78/0.43 % (4107196)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.78/0.43 % (4107194)Instruction limit reached!
% 0.78/0.43 % (4107194)------------------------------
% 0.78/0.43 % (4107194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107194)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107194)Termination reason: Instruction limit
% 0.78/0.46 % (4107194)Termination phase: Saturation
% 0.78/0.46 % (4107194)Time elapsed: 0.005 s
% 0.78/0.46 % (4107194)Peak memory usage: 12 MB
% 0.78/0.46 % (4107194)Instructions burned: 10 (million)
% 0.78/0.46 % (4107196)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=867628584:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.78/0.46 % (4107192)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2366660302: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.78/0.46 % (4107196)Instruction limit reached!
% 0.78/0.46 % (4107196)------------------------------
% 0.78/0.46 % (4107196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107196)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107196)Termination reason: Instruction limit
% 0.78/0.46 % (4107196)Termination phase: Saturation
% 0.78/0.46 % (4107196)Time elapsed: 0.003 s
% 0.78/0.46 % (4107196)Peak memory usage: 11 MB
% 0.78/0.46 % (4107196)Instructions burned: 5 (million)
% 0.78/0.46 % (4107197)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2666228772:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.78/0.46 % (4107197)Refutation not found, incomplete strategy
% 0.78/0.46 % (4107197)------------------------------
% 0.78/0.46 % (4107197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107197)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107197)Termination reason: Refutation not found, incomplete strategy
% 0.78/0.46 % (4107197)Time elapsed: 0.003 s
% 0.78/0.46 % (4107197)Peak memory usage: 12 MB
% 0.78/0.46 % (4107197)Instructions burned: 5 (million)
% 0.78/0.46 % (4107197)------------------------------
% 0.78/0.46 % (4107197)------------------------------
% 0.78/0.46 % (4107201)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=535566613:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.78/0.46 % (4107177)Instruction limit reached!
% 0.78/0.46 % (4107177)------------------------------
% 0.78/0.46 % (4107177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107177)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107177)Termination reason: Instruction limit
% 0.78/0.46 % (4107177)Termination phase: Saturation
% 0.78/0.46 % (4107177)Time elapsed: 0.083 s
% 0.78/0.46 % (4107177)Peak memory usage: 13 MB
% 0.78/0.46 % (4107177)Instructions burned: 157 (million)
% 0.78/0.46 % (4107203)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=584574709:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.78/0.46 % (4107192)Instruction limit reached!
% 0.78/0.46 % (4107192)------------------------------
% 0.78/0.46 % (4107192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107192)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107192)Termination reason: Instruction limit
% 0.78/0.46 % (4107192)Termination phase: Saturation
% 0.78/0.46 % (4107192)Time elapsed: 0.023 s
% 0.78/0.46 % (4107192)Peak memory usage: 11 MB
% 0.78/0.46 % (4107192)Instructions burned: 29 (million)
% 0.78/0.46 % (4107205)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2639028270:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.78/0.46 % (4107193)Instruction limit reached!
% 0.78/0.46 % (4107193)------------------------------
% 0.78/0.46 % (4107193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.46 % (4107193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.46 % (4107193)CaDiCaL version: 2.1.3
% 0.78/0.46 % (4107193)Termination reason: Instruction limit
% 0.78/0.49 % (4107193)Termination phase: Saturation
% 0.78/0.49 % (4107193)Time elapsed: 0.042 s
% 0.78/0.49 % (4107193)Peak memory usage: 13 MB
% 0.78/0.49 % (4107193)Instructions burned: 87 (million)
% 0.78/0.49 % (4107203)Instruction limit reached!
% 0.78/0.49 % (4107203)------------------------------
% 0.78/0.49 % (4107203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107203)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107203)Termination reason: Instruction limit
% 0.78/0.49 % (4107203)Termination phase: Saturation
% 0.78/0.49 % (4107203)Time elapsed: 0.013 s
% 0.78/0.49 % (4107203)Peak memory usage: 12 MB
% 0.78/0.49 % (4107203)Instructions burned: 25 (million)
% 0.78/0.49 % (4107205)Instruction limit reached!
% 0.78/0.49 % (4107205)------------------------------
% 0.78/0.49 % (4107205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107205)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107205)Termination reason: Instruction limit
% 0.78/0.49 % (4107205)Termination phase: Saturation
% 0.78/0.49 % (4107205)Time elapsed: 0.009 s
% 0.78/0.49 % (4107205)Peak memory usage: 12 MB
% 0.78/0.49 % (4107205)Instructions burned: 16 (million)
% 0.78/0.49 % (4107209)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1230217963:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.78/0.49 % (4107208)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2914005455:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.78/0.49 % (4107211)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1942196948:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.78/0.49 % (4107209)Instruction limit reached!
% 0.78/0.49 % (4107209)------------------------------
% 0.78/0.49 % (4107209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107209)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107209)Termination reason: Instruction limit
% 0.78/0.49 % (4107209)Termination phase: Saturation
% 0.78/0.49 % (4107209)Time elapsed: 0.007 s
% 0.78/0.49 % (4107209)Peak memory usage: 12 MB
% 0.78/0.49 % (4107209)Instructions burned: 14 (million)
% 0.78/0.49 % (4107212)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=720368204:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.78/0.49 % (4107211)Instruction limit reached!
% 0.78/0.49 % (4107211)------------------------------
% 0.78/0.49 % (4107211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107211)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107211)Termination reason: Instruction limit
% 0.78/0.49 % (4107211)Termination phase: Saturation
% 0.78/0.49 % (4107211)Time elapsed: 0.002 s
% 0.78/0.49 % (4107211)Peak memory usage: 11 MB
% 0.78/0.49 % (4107211)Instructions burned: 3 (million)
% 0.78/0.49 % (4107213)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3875727101:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.78/0.49 % (4107212)Instruction limit reached!
% 0.78/0.49 % (4107212)------------------------------
% 0.78/0.49 % (4107212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107212)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107212)Termination reason: Instruction limit
% 0.78/0.49 % (4107212)Termination phase: Saturation
% 0.78/0.49 % (4107212)Time elapsed: 0.012 s
% 0.78/0.49 % (4107212)Peak memory usage: 12 MB
% 0.78/0.49 % (4107212)Instructions burned: 26 (million)
% 0.78/0.49 % (4107219)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
% 0.78/0.49 % (4107219)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.78/0.49 % (4107213)Instruction limit reached!
% 0.78/0.49 % (4107213)------------------------------
% 0.78/0.49 % (4107213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107213)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107213)Termination reason: Instruction limit
% 0.78/0.49 % (4107213)Termination phase: Saturation
% 0.78/0.49 % (4107213)Time elapsed: 0.012 s
% 0.78/0.49 % (4107213)Peak memory usage: 12 MB
% 0.78/0.49 % (4107213)Instructions burned: 24 (million)
% 0.78/0.49 % (4107217)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3991454243:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.78/0.49 % (4107219)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=29337695:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.78/0.49 % (4107219)Instruction limit reached!
% 0.78/0.49 % (4107219)------------------------------
% 0.78/0.49 % (4107219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107219)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107219)Termination reason: Instruction limit
% 0.78/0.49 % (4107219)Termination phase: Saturation
% 0.78/0.49 % (4107219)Time elapsed: 0.007 s
% 0.78/0.49 % (4107219)Peak memory usage: 12 MB
% 0.78/0.49 % (4107219)Instructions burned: 14 (million)
% 0.78/0.49 % (4107221)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.78/0.49 % (4107221)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=1356524537:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.78/0.49 % (4107222)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=1538359388:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.78/0.49 % (4107221)Instruction limit reached!
% 0.78/0.49 % (4107221)------------------------------
% 0.78/0.49 % (4107221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107221)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107221)Termination reason: Instruction limit
% 0.78/0.49 % (4107221)Termination phase: Saturation
% 0.78/0.49 % (4107221)Time elapsed: 0.005 s
% 0.78/0.49 % (4107221)Peak memory usage: 12 MB
% 0.78/0.49 % (4107221)Instructions burned: 9 (million)
% 0.78/0.49 % (4107225)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2132824424:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.78/0.49 % (4107217)Instruction limit reached!
% 0.78/0.49 % (4107217)------------------------------
% 0.78/0.49 % (4107217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107217)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107217)Termination reason: Instruction limit
% 0.78/0.49 % (4107217)Termination phase: Saturation
% 0.78/0.49 % (4107217)Time elapsed: 0.030 s
% 0.78/0.49 % (4107217)Peak memory usage: 12 MB
% 0.78/0.49 % (4107217)Instructions burned: 60 (million)
% 0.78/0.49 % (4107222)Instruction limit reached!
% 0.78/0.49 % (4107222)------------------------------
% 0.78/0.49 % (4107222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107222)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107222)Termination reason: Instruction limit
% 0.78/0.49 % (4107222)Termination phase: Saturation
% 0.78/0.49 % (4107222)Time elapsed: 0.015 s
% 0.78/0.49 % (4107222)Peak memory usage: 12 MB
% 0.78/0.49 % (4107222)Instructions burned: 31 (million)
% 0.78/0.49 % (4107225)Instruction limit reached!
% 0.78/0.49 % (4107225)------------------------------
% 0.78/0.49 % (4107225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107225)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107225)Termination reason: Instruction limit
% 0.78/0.49 % (4107225)Termination phase: Saturation
% 0.78/0.49 % (4107225)Time elapsed: 0.004 s
% 0.78/0.49 % (4107225)Peak memory usage: 12 MB
% 0.78/0.49 % (4107225)Instructions burned: 7 (million)
% 0.78/0.49 % (4107228)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2292694809:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.78/0.49 % (4107201) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4107166-4107201"...
% 0.78/0.49 % (4107230)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3953268929:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 0.78/0.49 % (4107228)Instruction limit reached!
% 0.78/0.49 % (4107228)------------------------------
% 0.78/0.49 % (4107228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107228)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107228)Termination reason: Instruction limit
% 0.78/0.49 % (4107228)Termination phase: Saturation
% 0.78/0.49 % (4107228)Time elapsed: 0.010 s
% 0.78/0.49 % (4107228)Peak memory usage: 11 MB
% 0.78/0.49 % (4107228)Instructions burned: 25 (million)
% 0.78/0.49 % (4107232)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3153321896:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 0.78/0.49 % (4107231)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=150791900:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 0.78/0.49 % (4107201)...printing done.
% 0.78/0.49 % (4107201)Refutation found. Thanks to Tanya!
% 0.78/0.49 % SZS status Theorem for theBenchmark
% 0.78/0.49 % SZS output start Proof for theBenchmark
% 0.78/0.49 thf(type_def_5, type, a: $tType).
% 0.78/0.49 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.78/0.49 thf(func_def_1, type, sK0: a).
% 0.78/0.49 thf(func_def_2, type, sK1: a).
% 0.78/0.49 thf(func_def_3, type, sK2: (a > a > a)).
% 0.78/0.49 thf(func_def_4, type, sK3: (a > a > a)).
% 0.78/0.49 thf(func_def_5, type, sK4: a).
% 0.78/0.49 thf(func_def_6, type, sK5: a).
% 0.78/0.49 thf(func_def_7, type, sK6: a).
% 0.78/0.49 thf(func_def_8, type, sK7: (a > a)).
% 0.78/0.49 thf(f1,conjecture,(
% 0.78/0.49 ! [X1 : (a > a > a),X2 : a,X0 : (a > a > a),X3 : a] : ((! [X4 : a,X5 : a,X6 : a] : (((X1 @ (X1 @ X4 @ X5) @ X6)) = ((X1 @ X4 @ (X1 @ X5 @ X6)))) & ! [X4 : a] : ? [X5 : a] : ((((X0 @ X4 @ X5)) = X2) & (((X1 @ X4 @ X5)) = X3)) & ! [X6 : a,X5 : a,X4 : a] : (((X0 @ X4 @ (X1 @ X5 @ X6))) = ((X1 @ (X0 @ X4 @ X5) @ (X0 @ X4 @ X6)))) & ! [X4 : a,X5 : a] : (((X0 @ (X1 @ X4 @ X5) @ X5)) = X5) & ! [X5 : a,X4 : a] : (((X0 @ X4 @ X5)) = ((X0 @ X5 @ X4))) & ! [X4 : a] : (((X0 @ X3 @ X4)) = X4) & ! [X4 : a] : (((X0 @ X4 @ X4)) = X4) & ! [X4 : a,X5 : a,X6 : a] : (((X1 @ X4 @ (X0 @ X5 @ X6))) = ((X0 @ (X1 @ X4 @ X5) @ (X1 @ X4 @ X6)))) & ! [X5 : a,X4 : a] : (((X1 @ (X0 @ X4 @ X5) @ X5)) = X5) & ! [X5 : a,X4 : a] : (((X1 @ X4 @ X5)) = ((X1 @ X5 @ X4))) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X4 @ X5) @ X6)) = ((X0 @ X4 @ (X0 @ X5 @ X6)))) & ! [X4 : a] : (((X1 @ X4 @ X4)) = X4) & ! [X4 : a] : (((X0 @ X2 @ X4)) = X2) & ! [X4 : a] : (((X1 @ X3 @ X4)) = X3) & ! [X4 : a] : (((X1 @ X2 @ X4)) = X4)) => ! [X6 : a,X5 : a,X4 : a] : (((((X1 @ X4 @ X6)) = X3) & (((X0 @ X4 @ X5)) = X2) & (((X1 @ X4 @ X5)) = X3) & (((X0 @ X4 @ X6)) = X2)) => (X5 = X6)))),
% 0.78/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cCD_LATTICE_THM_pme)).
% 0.78/0.49 thf(f2,negated_conjecture,(
% 0.78/0.49 ~ ! [X1 : (a > a > a),X2 : a,X0 : (a > a > a),X3 : a] : ((! [X4 : a,X5 : a,X6 : a] : (((X1 @ (X1 @ X4 @ X5) @ X6)) = ((X1 @ X4 @ (X1 @ X5 @ X6)))) & ! [X4 : a] : ? [X5 : a] : ((((X0 @ X4 @ X5)) = X2) & (((X1 @ X4 @ X5)) = X3)) & ! [X6 : a,X5 : a,X4 : a] : (((X0 @ X4 @ (X1 @ X5 @ X6))) = ((X1 @ (X0 @ X4 @ X5) @ (X0 @ X4 @ X6)))) & ! [X4 : a,X5 : a] : (((X0 @ (X1 @ X4 @ X5) @ X5)) = X5) & ! [X5 : a,X4 : a] : (((X0 @ X4 @ X5)) = ((X0 @ X5 @ X4))) & ! [X4 : a] : (((X0 @ X3 @ X4)) = X4) & ! [X4 : a] : (((X0 @ X4 @ X4)) = X4) & ! [X4 : a,X5 : a,X6 : a] : (((X1 @ X4 @ (X0 @ X5 @ X6))) = ((X0 @ (X1 @ X4 @ X5) @ (X1 @ X4 @ X6)))) & ! [X5 : a,X4 : a] : (((X1 @ (X0 @ X4 @ X5) @ X5)) = X5) & ! [X5 : a,X4 : a] : (((X1 @ X4 @ X5)) = ((X1 @ X5 @ X4))) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X4 @ X5) @ X6)) = ((X0 @ X4 @ (X0 @ X5 @ X6)))) & ! [X4 : a] : (((X1 @ X4 @ X4)) = X4) & ! [X4 : a] : (((X0 @ X2 @ X4)) = X2) & ! [X4 : a] : (((X1 @ X3 @ X4)) = X3) & ! [X4 : a] : (((X1 @ X2 @ X4)) = X4)) => ! [X6 : a,X5 : a,X4 : a] : (((((X1 @ X4 @ X6)) = X3) & (((X0 @ X4 @ X5)) = X2) & (((X1 @ X4 @ X5)) = X3) & (((X0 @ X4 @ X6)) = X2)) => (X5 = X6)))),
% 0.78/0.49 inference(negated_conjecture,[status(cth)],[f1])).
% 0.78/0.49 thf(f3,plain,(
% 0.78/0.49 ~ ! [X2 : (a > a > a),X0 : (a > a > a),X1 : a,X3 : a] : ((! [X22 : a,X21 : a] : (((X0 @ (X2 @ X22 @ X21) @ X21)) = X21) & ! [X28 : a] : (((X0 @ X28 @ X28)) = X28) & ! [X10 : a,X11 : a,X9 : a] : (((X0 @ (X2 @ X11 @ X10) @ (X2 @ X11 @ X9))) = ((X2 @ X11 @ (X0 @ X10 @ X9)))) & ! [X26 : a,X25 : a,X27 : a] : (((X2 @ (X2 @ X25 @ X26) @ X27)) = ((X2 @ X25 @ (X2 @ X26 @ X27)))) & ! [X17 : a] : (((X2 @ X17 @ X17)) = X17) & ! [X7 : a] : ? [X8 : a] : ((((X2 @ X7 @ X8)) = X1) & (((X0 @ X7 @ X8)) = X3)) & ! [X30 : a] : (((X0 @ X3 @ X30)) = X3) & ! [X23 : a,X24 : a] : (((X0 @ X23 @ X24)) = ((X0 @ X24 @ X23))) & ! [X18 : a,X19 : a,X20 : a] : (((X2 @ (X0 @ X18 @ X19) @ (X0 @ X18 @ X20))) = ((X0 @ X18 @ (X2 @ X19 @ X20)))) & ! [X12 : a,X13 : a] : (((X2 @ (X0 @ X12 @ X13) @ X13)) = X13) & ! [X14 : a,X15 : a] : (((X2 @ X14 @ X15)) = ((X2 @ X15 @ X14))) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X4 @ X5) @ X6)) = ((X0 @ X4 @ (X0 @ X5 @ X6)))) & ! [X31 : a] : (((X0 @ X1 @ X31)) = X31) & ! [X16 : a] : (((X2 @ X3 @ X16)) = X16) & ! [X29 : a] : (((X2 @ X1 @ X29)) = X1)) => ! [X32 : a,X33 : a,X34 : a] : (((((X2 @ X34 @ X32)) = X1) & (((X0 @ X34 @ X33)) = X3) & (((X0 @ X34 @ X32)) = X3) & (((X2 @ X34 @ X33)) = X1)) => (X32 = X33)))),
% 0.78/0.49 inference(rectify,[],[f2])).
% 0.78/0.49 thf(f4,plain,(
% 0.78/0.49 ? [X2 : (a > a > a),X0 : (a > a > a),X1 : a,X3 : a] : (? [X32 : a,X33 : a,X34 : a] : ((X32 != X33) & ((((X2 @ X34 @ X32)) = X1) & (((X0 @ X34 @ X33)) = X3) & (((X0 @ X34 @ X32)) = X3) & (((X2 @ X34 @ X33)) = X1))) & (! [X22 : a,X21 : a] : (((X0 @ (X2 @ X22 @ X21) @ X21)) = X21) & ! [X28 : a] : (((X0 @ X28 @ X28)) = X28) & ! [X10 : a,X11 : a,X9 : a] : (((X0 @ (X2 @ X11 @ X10) @ (X2 @ X11 @ X9))) = ((X2 @ X11 @ (X0 @ X10 @ X9)))) & ! [X26 : a,X25 : a,X27 : a] : (((X2 @ (X2 @ X25 @ X26) @ X27)) = ((X2 @ X25 @ (X2 @ X26 @ X27)))) & ! [X17 : a] : (((X2 @ X17 @ X17)) = X17) & ! [X7 : a] : ? [X8 : a] : ((((X2 @ X7 @ X8)) = X1) & (((X0 @ X7 @ X8)) = X3)) & ! [X30 : a] : (((X0 @ X3 @ X30)) = X3) & ! [X23 : a,X24 : a] : (((X0 @ X23 @ X24)) = ((X0 @ X24 @ X23))) & ! [X18 : a,X19 : a,X20 : a] : (((X2 @ (X0 @ X18 @ X19) @ (X0 @ X18 @ X20))) = ((X0 @ X18 @ (X2 @ X19 @ X20)))) & ! [X12 : a,X13 : a] : (((X2 @ (X0 @ X12 @ X13) @ X13)) = X13) & ! [X14 : a,X15 : a] : (((X2 @ X14 @ X15)) = ((X2 @ X15 @ X14))) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X4 @ X5) @ X6)) = ((X0 @ X4 @ (X0 @ X5 @ X6)))) & ! [X31 : a] : (((X0 @ X1 @ X31)) = X31) & ! [X16 : a] : (((X2 @ X3 @ X16)) = X16) & ! [X29 : a] : (((X2 @ X1 @ X29)) = X1)))),
% 0.78/0.49 inference(ennf_transformation,[],[f3])).
% 0.78/0.49 thf(f5,plain,(
% 0.78/0.49 ? [X3 : a,X1 : a,X2 : (a > a > a),X0 : (a > a > a)] : (? [X32 : a,X34 : a,X33 : a] : ((((X2 @ X34 @ X32)) = X1) & (((X0 @ X34 @ X32)) = X3) & (((X2 @ X34 @ X33)) = X1) & (((X0 @ X34 @ X33)) = X3) & (X32 != X33)) & ! [X22 : a,X21 : a] : (((X0 @ (X2 @ X22 @ X21) @ X21)) = X21) & ! [X16 : a] : (((X2 @ X3 @ X16)) = X16) & ! [X23 : a,X24 : a] : (((X0 @ X23 @ X24)) = ((X0 @ X24 @ X23))) & ! [X17 : a] : (((X2 @ X17 @ X17)) = X17) & ! [X28 : a] : (((X0 @ X28 @ X28)) = X28) & ! [X12 : a,X13 : a] : (((X2 @ (X0 @ X12 @ X13) @ X13)) = X13) & ! [X14 : a,X15 : a] : (((X2 @ X14 @ X15)) = ((X2 @ X15 @ X14))) & ! [X29 : a] : (((X2 @ X1 @ X29)) = X1) & ! [X26 : a,X25 : a,X27 : a] : (((X2 @ (X2 @ X25 @ X26) @ X27)) = ((X2 @ X25 @ (X2 @ X26 @ X27)))) & ! [X18 : a,X19 : a,X20 : a] : (((X2 @ (X0 @ X18 @ X19) @ (X0 @ X18 @ X20))) = ((X0 @ X18 @ (X2 @ X19 @ X20)))) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X4 @ X5) @ X6)) = ((X0 @ X4 @ (X0 @ X5 @ X6)))) & ! [X31 : a] : (((X0 @ X1 @ X31)) = X31) & ! [X30 : a] : (((X0 @ X3 @ X30)) = X3) & ! [X7 : a] : ? [X8 : a] : ((((X2 @ X7 @ X8)) = X1) & (((X0 @ X7 @ X8)) = X3)) & ! [X10 : a,X11 : a,X9 : a] : (((X0 @ (X2 @ X11 @ X10) @ (X2 @ X11 @ X9))) = ((X2 @ X11 @ (X0 @ X10 @ X9)))))),
% 0.78/0.49 inference(flattening,[],[f4])).
% 0.78/0.49 thf(f6,plain,(
% 0.78/0.49 ? [X0 : a,X1 : a,X2 : (a > a > a),X3 : (a > a > a)] : (? [X4 : a,X5 : a,X6 : a] : ((((X2 @ X5 @ X4)) = X1) & (((X3 @ X5 @ X4)) = X0) & (((X2 @ X5 @ X6)) = X1) & (((X3 @ X5 @ X6)) = X0) & (X4 != X6)) & ! [X7 : a,X8 : a] : (((X3 @ (X2 @ X7 @ X8) @ X8)) = X8) & ! [X9 : a] : (((X2 @ X0 @ X9)) = X9) & ! [X10 : a,X11 : a] : (((X3 @ X10 @ X11)) = ((X3 @ X11 @ X10))) & ! [X12 : a] : (((X2 @ X12 @ X12)) = X12) & ! [X13 : a] : (((X3 @ X13 @ X13)) = X13) & ! [X14 : a,X15 : a] : (((X2 @ (X3 @ X14 @ X15) @ X15)) = X15) & ! [X16 : a,X17 : a] : (((X2 @ X17 @ X16)) = ((X2 @ X16 @ X17))) & ! [X18 : a] : (((X2 @ X1 @ X18)) = X1) & ! [X19 : a,X20 : a,X21 : a] : (((X2 @ (X2 @ X20 @ X19) @ X21)) = ((X2 @ X20 @ (X2 @ X19 @ X21)))) & ! [X22 : a,X23 : a,X24 : a] : (((X2 @ (X3 @ X22 @ X23) @ (X3 @ X22 @ X24))) = ((X3 @ X22 @ (X2 @ X23 @ X24)))) & ! [X25 : a,X26 : a,X27 : a] : (((X3 @ X25 @ (X3 @ X26 @ X27))) = ((X3 @ (X3 @ X25 @ X26) @ X27))) & ! [X28 : a] : (((X3 @ X1 @ X28)) = X28) & ! [X29 : a] : (((X3 @ X0 @ X29)) = X0) & ! [X30 : a] : ? [X31 : a] : ((((X2 @ X30 @ X31)) = X1) & (((X3 @ X30 @ X31)) = X0)) & ! [X32 : a,X33 : a,X34 : a] : (((X2 @ X33 @ (X3 @ X32 @ X34))) = ((X3 @ (X2 @ X33 @ X32) @ (X2 @ X33 @ X34)))))),
% 0.78/0.49 inference(rectify,[],[f5])).
% 0.78/0.49 thf(f7,plain,(
% 0.78/0.49 ((sK1 = ((sK2 @ sK5 @ sK4))) & (sK0 = ((sK3 @ sK5 @ sK4))) & (((sK2 @ sK5 @ sK6)) = sK1) & (sK0 = ((sK3 @ sK5 @ sK6))) & (sK4 != sK6)) & ! [X7 : a,X8 : a] : (((sK3 @ (sK2 @ X7 @ X8) @ X8)) = X8) & ! [X9 : a] : (((sK2 @ sK0 @ X9)) = X9) & ! [X10 : a,X11 : a] : (((sK3 @ X10 @ X11)) = ((sK3 @ X11 @ X10))) & ! [X12 : a] : (((sK2 @ X12 @ X12)) = X12) & ! [X13 : a] : (((sK3 @ X13 @ X13)) = X13) & ! [X14 : a,X15 : a] : (((sK2 @ (sK3 @ X14 @ X15) @ X15)) = X15) & ! [X16 : a,X17 : a] : (((sK2 @ X16 @ X17)) = ((sK2 @ X17 @ X16))) & ! [X18 : a] : (sK1 = ((sK2 @ sK1 @ X18))) & ! [X19 : a,X20 : a,X21 : a] : (((sK2 @ X20 @ (sK2 @ X19 @ X21))) = ((sK2 @ (sK2 @ X20 @ X19) @ X21))) & ! [X22 : a,X23 : a,X24 : a] : (((sK2 @ (sK3 @ X22 @ X23) @ (sK3 @ X22 @ X24))) = ((sK3 @ X22 @ (sK2 @ X23 @ X24)))) & ! [X25 : a,X26 : a,X27 : a] : (((sK3 @ (sK3 @ X25 @ X26) @ X27)) = ((sK3 @ X25 @ (sK3 @ X26 @ X27)))) & ! [X28 : a] : (((sK3 @ sK1 @ X28)) = X28) & ! [X29 : a] : (sK0 = ((sK3 @ sK0 @ X29))) & ! [X30 : a] : ((sK1 = ((sK2 @ X30 @ (sK7 @ X30)))) & (((sK3 @ X30 @ (sK7 @ X30))) = sK0)) & ! [X32 : a,X33 : a,X34 : a] : (((sK2 @ X33 @ (sK3 @ X32 @ X34))) = ((sK3 @ (sK2 @ X33 @ X32) @ (sK2 @ X33 @ X34))))),
% 0.78/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X31,sK7 @ X30)],[f6])).
% 0.78/0.49 thf(f8,plain,(
% 0.78/0.49 ( ! [X34 : a,X32 : a,X33 : a] : ((((sK2 @ X33 @ (sK3 @ X32 @ X34))) = ((sK3 @ (sK2 @ X33 @ X32) @ (sK2 @ X33 @ X34))))) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f9,plain,(
% 0.78/0.49 ( ! [X30 : a] : ((((sK3 @ X30 @ (sK7 @ X30))) = sK0)) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f10,plain,(
% 0.78/0.49 ( ! [X30 : a] : ((sK1 = ((sK2 @ X30 @ (sK7 @ X30))))) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f12,plain,(
% 0.78/0.49 ( ! [X28 : a] : ((((sK3 @ sK1 @ X28)) = X28)) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f14,plain,(
% 0.78/0.49 ( ! [X24 : a,X22 : a,X23 : a] : ((((sK2 @ (sK3 @ X22 @ X23) @ (sK3 @ X22 @ X24))) = ((sK3 @ X22 @ (sK2 @ X23 @ X24))))) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f17,plain,(
% 0.78/0.49 ( ! [X16 : a,X17 : a] : ((((sK2 @ X16 @ X17)) = ((sK2 @ X17 @ X16)))) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f18,plain,(
% 0.78/0.49 ( ! [X14 : a,X15 : a] : ((((sK2 @ (sK3 @ X14 @ X15) @ X15)) = X15)) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f21,plain,(
% 0.78/0.49 ( ! [X10 : a,X11 : a] : ((((sK3 @ X10 @ X11)) = ((sK3 @ X11 @ X10)))) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f22,plain,(
% 0.78/0.49 ( ! [X9 : a] : ((((sK2 @ sK0 @ X9)) = X9)) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f23,plain,(
% 0.78/0.49 ( ! [X8 : a,X7 : a] : ((((sK3 @ (sK2 @ X7 @ X8) @ X8)) = X8)) )),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f24,plain,(
% 0.78/0.49 (sK4 != sK6)),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f25,plain,(
% 0.78/0.49 (sK0 = ((sK3 @ sK5 @ sK6)))),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f26,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ sK6)) = sK1)),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f27,plain,(
% 0.78/0.49 (sK0 = ((sK3 @ sK5 @ sK4)))),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f28,plain,(
% 0.78/0.49 (sK1 = ((sK2 @ sK5 @ sK4)))),
% 0.78/0.49 inference(cnf_transformation,[],[f7])).
% 0.78/0.49 thf(f38,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ X0 @ sK0)) = X0)) )),
% 0.78/0.49 inference(superposition,[],[f17,f22])).
% 0.78/0.49 thf(f66,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ X0 @ sK1)) = X0)) )),
% 0.78/0.49 inference(superposition,[],[f21,f12])).
% 0.78/0.49 thf(f236,plain,(
% 0.78/0.49 ( ! [X0 : a,X1 : a] : ((((sK3 @ sK1 @ (sK2 @ X0 @ X1))) = ((sK2 @ X0 @ (sK3 @ (sK7 @ X0) @ X1))))) )),
% 0.78/0.49 inference(superposition,[],[f8,f10])).
% 0.78/0.49 thf(f241,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ sK1 @ (sK2 @ sK5 @ X0))) = ((sK2 @ sK5 @ (sK3 @ sK4 @ X0))))) )),
% 0.78/0.49 inference(superposition,[],[f8,f28])).
% 0.78/0.49 thf(f242,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ sK1 @ (sK2 @ sK5 @ X0))) = ((sK2 @ sK5 @ (sK3 @ sK6 @ X0))))) )),
% 0.78/0.49 inference(superposition,[],[f8,f26])).
% 0.78/0.49 thf(f260,plain,(
% 0.78/0.49 ( ! [X0 : a,X1 : a] : ((((sK2 @ X0 @ (sK3 @ (sK7 @ X0) @ X1))) = ((sK2 @ X0 @ X1)))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f236,f12])).
% 0.78/0.49 thf(f267,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ sK5 @ X0)) = ((sK2 @ sK5 @ (sK3 @ sK4 @ X0))))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f241,f12])).
% 0.78/0.49 thf(f269,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ sK5 @ (sK3 @ sK6 @ X0))) = ((sK2 @ sK5 @ X0)))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f242,f12])).
% 0.78/0.49 thf(f348,plain,(
% 0.78/0.49 ( ! [X0 : a,X1 : a] : ((((sK2 @ sK0 @ (sK3 @ X0 @ X1))) = ((sK3 @ X0 @ (sK2 @ (sK7 @ X0) @ X1))))) )),
% 0.78/0.49 inference(superposition,[],[f14,f9])).
% 0.78/0.49 thf(f353,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ sK0 @ (sK3 @ sK5 @ X0))) = ((sK3 @ sK5 @ (sK2 @ sK4 @ X0))))) )),
% 0.78/0.49 inference(superposition,[],[f14,f27])).
% 0.78/0.49 thf(f354,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ sK0 @ (sK3 @ sK5 @ X0))) = ((sK3 @ sK5 @ (sK2 @ sK6 @ X0))))) )),
% 0.78/0.49 inference(superposition,[],[f14,f25])).
% 0.78/0.49 thf(f384,plain,(
% 0.78/0.49 ( ! [X0 : a,X1 : a] : ((((sK3 @ X0 @ (sK2 @ (sK7 @ X0) @ X1))) = ((sK3 @ X0 @ X1)))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f348,f22])).
% 0.78/0.49 thf(f393,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ sK5 @ (sK2 @ sK6 @ X0))) = ((sK3 @ sK5 @ X0)))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f354,f22])).
% 0.78/0.49 thf(f394,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ sK5 @ (sK2 @ sK4 @ X0))) = ((sK3 @ sK5 @ X0)))) )),
% 0.78/0.49 inference(forward_demodulation,[],[f353,f22])).
% 0.78/0.49 thf(f994,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ sK0)) = ((sK2 @ sK5 @ (sK7 @ sK4))))),
% 0.78/0.49 inference(superposition,[],[f267,f9])).
% 0.78/0.49 thf(f1024,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ (sK7 @ sK4))) = ((sK2 @ sK0 @ sK5)))),
% 0.78/0.49 inference(forward_demodulation,[],[f994,f17])).
% 0.78/0.49 thf(f1031,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ (sK7 @ sK4))) = sK5)),
% 0.78/0.49 inference(forward_demodulation,[],[f1024,f22])).
% 0.78/0.49 thf(f1048,plain,(
% 0.78/0.49 (((sK3 @ sK5 @ (sK7 @ sK4))) = ((sK7 @ sK4)))),
% 0.78/0.49 inference(superposition,[],[f23,f1031])).
% 0.78/0.49 thf(f1060,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ sK0)) = ((sK2 @ sK5 @ (sK7 @ sK6))))),
% 0.78/0.49 inference(superposition,[],[f269,f9])).
% 0.78/0.49 thf(f1085,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ (sK7 @ sK6))) = ((sK2 @ sK0 @ sK5)))),
% 0.78/0.49 inference(forward_demodulation,[],[f1060,f17])).
% 0.78/0.49 thf(f1094,plain,(
% 0.78/0.49 (((sK2 @ sK5 @ (sK7 @ sK6))) = sK5)),
% 0.78/0.49 inference(forward_demodulation,[],[f1085,f22])).
% 0.78/0.49 thf(f1115,plain,(
% 0.78/0.49 (((sK7 @ sK6)) = ((sK3 @ sK5 @ (sK7 @ sK6))))),
% 0.78/0.49 inference(superposition,[],[f23,f1094])).
% 0.78/0.49 thf(f1404,plain,(
% 0.78/0.49 (((sK3 @ sK5 @ sK1)) = ((sK3 @ sK5 @ (sK7 @ sK6))))),
% 0.78/0.49 inference(superposition,[],[f393,f10])).
% 0.78/0.49 thf(f1426,plain,(
% 0.78/0.49 (((sK3 @ sK1 @ sK5)) = ((sK3 @ sK5 @ (sK7 @ sK6))))),
% 0.78/0.49 inference(forward_demodulation,[],[f1404,f21])).
% 0.78/0.49 thf(f1440,plain,(
% 0.78/0.49 (sK5 = ((sK3 @ sK5 @ (sK7 @ sK6))))),
% 0.78/0.49 inference(forward_demodulation,[],[f1426,f12])).
% 0.78/0.49 thf(f1443,plain,(
% 0.78/0.49 (((sK7 @ sK6)) = sK5)),
% 0.78/0.49 inference(superposition,[],[f1440,f1115])).
% 0.78/0.49 thf(f1463,plain,(
% 0.78/0.49 (((sK3 @ sK5 @ (sK7 @ sK4))) = ((sK3 @ sK5 @ sK1)))),
% 0.78/0.49 inference(superposition,[],[f394,f10])).
% 0.78/0.49 thf(f1486,plain,(
% 0.78/0.49 (((sK3 @ sK5 @ (sK7 @ sK4))) = ((sK3 @ sK1 @ sK5)))),
% 0.78/0.49 inference(forward_demodulation,[],[f1463,f21])).
% 0.78/0.49 thf(f1498,plain,(
% 0.78/0.49 (((sK3 @ sK5 @ (sK7 @ sK4))) = sK5)),
% 0.78/0.49 inference(forward_demodulation,[],[f1486,f12])).
% 0.78/0.49 thf(f1545,plain,(
% 0.78/0.49 (((sK7 @ sK4)) = sK5)),
% 0.78/0.49 inference(superposition,[],[f1048,f1498])).
% 0.78/0.49 thf(f1943,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ X0 @ (sK7 @ (sK7 @ X0)))) = ((sK2 @ X0 @ sK0)))) )),
% 0.78/0.49 inference(superposition,[],[f260,f9])).
% 0.78/0.49 thf(f1986,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ X0 @ (sK7 @ (sK7 @ X0)))) = X0)) )),
% 0.78/0.49 inference(forward_demodulation,[],[f1943,f38])).
% 0.78/0.49 thf(f2187,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ X0 @ sK1)) = ((sK3 @ X0 @ (sK7 @ (sK7 @ X0)))))) )),
% 0.78/0.49 inference(superposition,[],[f384,f10])).
% 0.78/0.49 thf(f2247,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK3 @ X0 @ (sK7 @ (sK7 @ X0)))) = X0)) )),
% 0.78/0.49 inference(forward_demodulation,[],[f2187,f66])).
% 0.78/0.49 thf(f2377,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK2 @ X0 @ (sK7 @ (sK7 @ X0)))) = ((sK7 @ (sK7 @ X0))))) )),
% 0.78/0.49 inference(superposition,[],[f18,f2247])).
% 0.78/0.49 thf(f2387,plain,(
% 0.78/0.49 ( ! [X0 : a] : ((((sK7 @ (sK7 @ X0))) = X0)) )),
% 0.78/0.49 inference(forward_demodulation,[],[f2377,f1986])).
% 0.78/0.49 thf(f2585,plain,(
% 0.78/0.49 (((sK7 @ sK5)) = sK4)),
% 0.78/0.49 inference(superposition,[],[f2387,f1545])).
% 0.78/0.49 thf(f2586,plain,(
% 0.78/0.49 (((sK7 @ sK5)) = sK6)),
% 0.78/0.49 inference(superposition,[],[f2387,f1443])).
% 0.78/0.49 thf(f2998,plain,(
% 0.78/0.49 (sK4 = sK6)),
% 0.78/0.49 inference(superposition,[],[f2585,f2586])).
% 0.78/0.49 thf(f3015,plain,(
% 0.78/0.49 $false),
% 0.78/0.49 inference(forward_subsumption_resolution,[],[f2998,f24])).
% 0.78/0.49 % SZS output end Proof for theBenchmark
% 0.78/0.49 % (4107201)------------------------------
% 0.78/0.49 % (4107201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.49 % (4107201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.49 % (4107201)CaDiCaL version: 2.1.3
% 0.78/0.49 % (4107201)Termination reason: Refutation
% 0.78/0.49 % (4107201)Time elapsed: 0.105 s
% 0.78/0.49 % (4107201)Peak memory usage: 13 MB
% 0.78/0.49 % (4107201)Instructions burned: 207 (million)
% 0.78/0.49 % (4107166)Success in time 0.233 s
% 0.78/0.49 % Vampire exiting
%------------------------------------------------------------------------------