%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU998^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:07 AM UTC 2026
% Result : Theorem 1.00s 0.37s
% Output : Refutation 1.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU998^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n001.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Tue Sep 29 15:03:21 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 Running higher-order theorem proving
% 0.06/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.33 % (1354721)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.18/0.33 % (1354728)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1846449286:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.18/0.33 % (1354728)Instruction limit reached!
% 0.18/0.33 % (1354728)------------------------------
% 0.18/0.33 % (1354728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (1354728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (1354728)CaDiCaL version: 2.1.3
% 0.18/0.33 % (1354728)Termination reason: Instruction limit
% 0.18/0.33 % (1354728)Termination phase: Saturation
% 0.18/0.33 % (1354728)Time elapsed: 0.003 s
% 0.18/0.33 % (1354728)Peak memory usage: 12 MB
% 0.18/0.33 % (1354728)Instructions burned: 12 (million)
% 0.18/0.33 % (1354732)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.18/0.33 % (1354732)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.18/0.33 % (1354726)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=394738249:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.18/0.33 % (1354727)lrs+10_16_si=on:nwc=1.5:random_seed=1723492374:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.18/0.33 % (1354729)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=1464714721: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.18/0.33 % (1354730)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3543289629:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.18/0.33 % (1354732)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=849308894:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.18/0.33 % (1354731)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=761617078:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.18/0.33 % (1354734)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1450743969:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.18/0.33 % (1354727)Instruction limit reached!
% 0.18/0.33 % (1354727)------------------------------
% 0.18/0.33 % (1354727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (1354727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (1354727)CaDiCaL version: 2.1.3
% 0.18/0.33 % (1354727)Termination reason: Instruction limit
% 0.18/0.33 % (1354727)Termination phase: Saturation
% 0.18/0.33 % (1354727)Time elapsed: 0.009 s
% 0.18/0.33 % (1354727)Peak memory usage: 12 MB
% 0.18/0.33 % (1354727)Instructions burned: 19 (million)
% 0.18/0.33 % (1354734)Instruction limit reached!
% 0.18/0.33 % (1354734)------------------------------
% 0.18/0.33 % (1354734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (1354734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (1354734)CaDiCaL version: 2.1.3
% 0.18/0.33 % (1354734)Termination reason: Instruction limit
% 0.18/0.33 % (1354734)Termination phase: Saturation
% 0.18/0.33 % (1354734)Time elapsed: 0.003 s
% 0.18/0.33 % (1354734)Peak memory usage: 12 MB
% 0.18/0.33 % (1354734)Instructions burned: 11 (million)
% 0.18/0.33 % (1354730)Instruction limit reached!
% 0.18/0.33 % (1354730)------------------------------
% 0.18/0.33 % (1354730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.33 % (1354730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.33 % (1354730)CaDiCaL version: 2.1.3
% 0.18/0.33 % (1354730)Termination reason: Instruction limit
% 0.18/0.33 % (1354730)Termination phase: Saturation
% 0.18/0.33 % (1354730)Time elapsed: 0.013 s
% 0.18/0.33 % (1354730)Peak memory usage: 12 MB
% 0.18/0.33 % (1354730)Instructions burned: 25 (million)
% 0.18/0.33 % (1354742)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1630435873:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.00/0.36 % (1354742)Instruction limit reached!
% 1.00/0.36 % (1354742)------------------------------
% 1.00/0.36 % (1354742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354742)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354742)Termination reason: Instruction limit
% 1.00/0.36 % (1354742)Termination phase: Saturation
% 1.00/0.36 % (1354742)Time elapsed: 0.002 s
% 1.00/0.36 % (1354742)Peak memory usage: 12 MB
% 1.00/0.36 % (1354742)Instructions burned: 7 (million)
% 1.00/0.36 % (1354743)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.00/0.36 % (1354743)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=233888024:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.00/0.36 % (1354746)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
% 1.00/0.36 % (1354746)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.00/0.36 % (1354744)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1674376063:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.00/0.36 % (1354746)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1265356628:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.00/0.36 % (1354743)Instruction limit reached!
% 1.00/0.36 % (1354743)------------------------------
% 1.00/0.36 % (1354743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354743)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354743)Termination reason: Instruction limit
% 1.00/0.36 % (1354743)Termination phase: Saturation
% 1.00/0.36 % (1354743)Time elapsed: 0.004 s
% 1.00/0.36 % (1354743)Peak memory usage: 11 MB
% 1.00/0.36 % (1354743)Instructions burned: 8 (million)
% 1.00/0.36 % (1354744)Instruction limit reached!
% 1.00/0.36 % (1354744)------------------------------
% 1.00/0.36 % (1354744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354744)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354744)Termination reason: Instruction limit
% 1.00/0.36 % (1354744)Termination phase: Saturation
% 1.00/0.36 % (1354744)Time elapsed: 0.006 s
% 1.00/0.36 % (1354744)Peak memory usage: 12 MB
% 1.00/0.36 % (1354744)Instructions burned: 12 (million)
% 1.00/0.36 % (1354731)Instruction limit reached!
% 1.00/0.36 % (1354731)------------------------------
% 1.00/0.36 % (1354731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354731)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354731)Termination reason: Instruction limit
% 1.00/0.36 % (1354731)Termination phase: Saturation
% 1.00/0.36 % (1354731)Time elapsed: 0.038 s
% 1.00/0.36 % (1354731)Peak memory usage: 12 MB
% 1.00/0.36 % (1354731)Instructions burned: 76 (million)
% 1.00/0.36 % (1354746)Instruction limit reached!
% 1.00/0.36 % (1354746)------------------------------
% 1.00/0.36 % (1354746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354746)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354746)Termination reason: Instruction limit
% 1.00/0.36 % (1354746)Termination phase: Saturation
% 1.00/0.36 % (1354746)Time elapsed: 0.007 s
% 1.00/0.36 % (1354746)Peak memory usage: 12 MB
% 1.00/0.36 % (1354746)Instructions burned: 33 (million)
% 1.00/0.36 % (1354726)Instruction limit reached!
% 1.00/0.36 % (1354726)------------------------------
% 1.00/0.36 % (1354726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354726)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354726)Termination reason: Instruction limit
% 1.00/0.36 % (1354726)Termination phase: Saturation
% 1.00/0.36 % (1354726)Time elapsed: 0.046 s
% 1.00/0.36 % (1354726)Peak memory usage: 12 MB
% 1.00/0.36 % (1354726)Instructions burned: 89 (million)
% 1.00/0.36 % (1354753)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2300628194:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.00/0.36 % (1354750)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=3357822710:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.00/0.36 % (1354753)Refutation not found, incomplete strategy
% 1.00/0.36 % (1354753)------------------------------
% 1.00/0.36 % (1354753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354753)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354753)Termination reason: Refutation not found, incomplete strategy
% 1.00/0.36 % (1354753)Time elapsed: 0.002 s
% 1.00/0.36 % (1354753)Peak memory usage: 12 MB
% 1.00/0.36 % (1354753)Instructions burned: 7 (million)
% 1.00/0.36 % (1354752)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.00/0.36 % (1354753)------------------------------
% 1.00/0.36 % (1354753)------------------------------
% 1.00/0.36 % (1354751)lrs+10_1_si=on:cs=on:random_seed=3080030445:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.00/0.36 % (1354752)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=1996564172:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.00/0.36 % (1354752)Instruction limit reached!
% 1.00/0.36 % (1354752)------------------------------
% 1.00/0.36 % (1354752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354752)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354752)Termination reason: Instruction limit
% 1.00/0.36 % (1354752)Termination phase: shuffling
% 1.00/0.36 % (1354752)Time elapsed: 0.001 s
% 1.00/0.36 % (1354752)Peak memory usage: 9 MB
% 1.00/0.36 % (1354752)Instructions burned: 2 (million)
% 1.00/0.36 % (1354751)Instruction limit reached!
% 1.00/0.36 % (1354751)------------------------------
% 1.00/0.36 % (1354751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354751)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354751)Termination reason: Instruction limit
% 1.00/0.36 % (1354751)Termination phase: Saturation
% 1.00/0.36 % (1354751)Time elapsed: 0.004 s
% 1.00/0.36 % (1354751)Peak memory usage: 12 MB
% 1.00/0.36 % (1354751)Instructions burned: 8 (million)
% 1.00/0.36 % (1354754)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4168769660:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.00/0.36 % (1354757)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1984756963:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 1.00/0.36 % (1354757)Instruction limit reached!
% 1.00/0.36 % (1354757)------------------------------
% 1.00/0.36 % (1354757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.36 % (1354757)CaDiCaL version: 2.1.3
% 1.00/0.36 % (1354757)Termination reason: Instruction limit
% 1.00/0.36 % (1354757)Termination phase: Saturation
% 1.00/0.36 % (1354757)Time elapsed: 0.007 s
% 1.00/0.36 % (1354757)Peak memory usage: 12 MB
% 1.00/0.36 % (1354757)Instructions burned: 27 (million)
% 1.00/0.36 % (1354760)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3061065922:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 1.00/0.36 % (1354761)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2088681771:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.00/0.36 % (1354732)Instruction limit reached!
% 1.00/0.36 % (1354732)------------------------------
% 1.00/0.36 % (1354732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.36 % (1354732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354732)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354732)Termination reason: Instruction limit
% 1.00/0.37 % (1354732)Termination phase: Saturation
% 1.00/0.37 % (1354732)Time elapsed: 0.080 s
% 1.00/0.37 % (1354732)Peak memory usage: 13 MB
% 1.00/0.37 % (1354732)Instructions burned: 157 (million)
% 1.00/0.37 % (1354764)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=781736299:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.00/0.37 % (1354760)Instruction limit reached!
% 1.00/0.37 % (1354760)------------------------------
% 1.00/0.37 % (1354760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354760)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354760)Termination reason: Instruction limit
% 1.00/0.37 % (1354760)Termination phase: Saturation
% 1.00/0.37 % (1354760)Time elapsed: 0.008 s
% 1.00/0.37 % (1354760)Peak memory usage: 12 MB
% 1.00/0.37 % (1354760)Instructions burned: 14 (million)
% 1.00/0.37 % (1354764)Instruction limit reached!
% 1.00/0.37 % (1354764)------------------------------
% 1.00/0.37 % (1354764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354764)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354764)Termination reason: Instruction limit
% 1.00/0.37 % (1354764)Termination phase: Saturation
% 1.00/0.37 % (1354764)Time elapsed: 0.004 s
% 1.00/0.37 % (1354764)Peak memory usage: 12 MB
% 1.00/0.37 % (1354764)Instructions burned: 17 (million)
% 1.00/0.37 % (1354750)Instruction limit reached!
% 1.00/0.37 % (1354750)------------------------------
% 1.00/0.37 % (1354750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354750)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354750)Termination reason: Instruction limit
% 1.00/0.37 % (1354750)Termination phase: Saturation
% 1.00/0.37 % (1354750)Time elapsed: 0.044 s
% 1.00/0.37 % (1354750)Peak memory usage: 12 MB
% 1.00/0.37 % (1354750)Instructions burned: 86 (million)
% 1.00/0.37 % (1354770)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=743188073:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.00/0.37 % (1354767)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4292112921: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.00/0.37 % (1354767)Instruction limit reached!
% 1.00/0.37 % (1354767)------------------------------
% 1.00/0.37 % (1354767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354767)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354767)Termination reason: Instruction limit
% 1.00/0.37 % (1354767)Termination phase: Saturation
% 1.00/0.37 % (1354767)Time elapsed: 0.003 s
% 1.00/0.37 % (1354767)Peak memory usage: 12 MB
% 1.00/0.37 % (1354767)Instructions burned: 6 (million)
% 1.00/0.37 % (1354769)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3226054694:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.00/0.37 % (1354770)Instruction limit reached!
% 1.00/0.37 % (1354770)------------------------------
% 1.00/0.37 % (1354770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354770)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354770)Termination reason: Instruction limit
% 1.00/0.37 % (1354770)Termination phase: Saturation
% 1.00/0.37 % (1354770)Time elapsed: 0.006 s
% 1.00/0.37 % (1354770)Peak memory usage: 12 MB
% 1.00/0.37 % (1354770)Instructions burned: 27 (million)
% 1.00/0.37 % (1354729) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1354721-1354729"...
% 1.00/0.37 % (1354729)...printing done.
% 1.00/0.37 % (1354776)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.00/0.37 % (1354729)Refutation found. Thanks to Tanya!
% 1.00/0.37 % SZS status Theorem for theBenchmark
% 1.00/0.37 % SZS output start Proof for theBenchmark
% 1.00/0.37 thf(type_def_5, type, a: $tType).
% 1.00/0.37 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 1.00/0.37 thf(func_def_1, type, sK0: (a > a > a)).
% 1.00/0.37 thf(func_def_2, type, sK1: (a > a > a)).
% 1.00/0.37 thf(func_def_3, type, sK2: a).
% 1.00/0.37 thf(func_def_4, type, sK3: a).
% 1.00/0.37 thf(func_def_5, type, sK4: a).
% 1.00/0.37 thf(func_def_6, type, sK5: a).
% 1.00/0.37 thf(func_def_7, type, sK6: a).
% 1.00/0.37 thf(f1,conjecture,(
% 1.00/0.37 ! [X1 : (a > a > a),X0 : (a > a > a)] : ((! [X3 : a,X2 : a] : (((X1 @ X2 @ X3)) = ((X1 @ X3 @ X2))) & ! [X2 : a,X4 : a,X3 : a] : (((X1 @ (X1 @ X2 @ X3) @ X4)) = ((X1 @ X2 @ (X1 @ X3 @ X4)))) & ! [X2 : a,X3 : a] : (((X0 @ (X1 @ X2 @ X3) @ X3)) = X3) & ! [X2 : a] : (((X1 @ X2 @ X2)) = X2) & ! [X3 : a,X2 : a] : (((X0 @ X2 @ X3)) = ((X0 @ X3 @ X2))) & ! [X2 : a,X3 : a] : (((X1 @ (X0 @ X2 @ X3) @ X3)) = X3) & ! [X2 : a,X4 : a,X3 : a] : (((X0 @ (X0 @ X2 @ X3) @ X4)) = ((X0 @ X2 @ (X0 @ X3 @ X4)))) & ! [X2 : a] : (((X0 @ X2 @ X2)) = X2)) => (? [X6 : a,X3 : a,X2 : a,X7 : a,X5 : a] : ((X6 != X2) & (((X0 @ X5 @ X3)) = X5) & (((X1 @ X5 @ X7)) = X3) & (((X1 @ X2 @ X6)) = X6) & (((X1 @ X7 @ X3)) = X3) & (X6 != X7) & (X5 != X6) & (((X1 @ X6 @ X7)) = X3) & (((X0 @ X2 @ X3)) = X2) & (X5 != X7) & (((X0 @ X6 @ X3)) = X6) & (((X0 @ X6 @ X7)) = X2) & (((X0 @ X2 @ X7)) = X2) & (X7 != X3) & (((X1 @ X6 @ X3)) = X3) & (X5 != X2) & (((X1 @ X5 @ X3)) = X3) & (((X1 @ X2 @ X7)) = X7) & (X5 != X3) & (((X1 @ X2 @ X3)) = X3) & (((X0 @ X2 @ X6)) = X2) & (((X0 @ X5 @ X6)) = X2) & (((X1 @ X2 @ X5)) = X5) & (X7 != X2) & (((X0 @ X2 @ X5)) = X2) & (X2 != X3) & (((X0 @ X7 @ X3)) = X7) & (((X0 @ X5 @ X7)) = X2) & (((X1 @ X5 @ X6)) = X3) & (X6 != X3)) => ~ ! [X4 : a,X3 : a,X2 : a] : (((X1 @ X2 @ (X0 @ X3 @ X4))) = ((X0 @ (X1 @ X2 @ X3) @ (X1 @ X2 @ X4))))))),
% 1.00/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p',c3_DIAMOND_THM_pme)).
% 1.00/0.37 thf(f2,negated_conjecture,(
% 1.00/0.37 ~ ! [X1 : (a > a > a),X0 : (a > a > a)] : ((! [X3 : a,X2 : a] : (((X1 @ X2 @ X3)) = ((X1 @ X3 @ X2))) & ! [X2 : a,X4 : a,X3 : a] : (((X1 @ (X1 @ X2 @ X3) @ X4)) = ((X1 @ X2 @ (X1 @ X3 @ X4)))) & ! [X2 : a,X3 : a] : (((X0 @ (X1 @ X2 @ X3) @ X3)) = X3) & ! [X2 : a] : (((X1 @ X2 @ X2)) = X2) & ! [X3 : a,X2 : a] : (((X0 @ X2 @ X3)) = ((X0 @ X3 @ X2))) & ! [X2 : a,X3 : a] : (((X1 @ (X0 @ X2 @ X3) @ X3)) = X3) & ! [X2 : a,X4 : a,X3 : a] : (((X0 @ (X0 @ X2 @ X3) @ X4)) = ((X0 @ X2 @ (X0 @ X3 @ X4)))) & ! [X2 : a] : (((X0 @ X2 @ X2)) = X2)) => (? [X6 : a,X3 : a,X2 : a,X7 : a,X5 : a] : ((X6 != X2) & (((X0 @ X5 @ X3)) = X5) & (((X1 @ X5 @ X7)) = X3) & (((X1 @ X2 @ X6)) = X6) & (((X1 @ X7 @ X3)) = X3) & (X6 != X7) & (X5 != X6) & (((X1 @ X6 @ X7)) = X3) & (((X0 @ X2 @ X3)) = X2) & (X5 != X7) & (((X0 @ X6 @ X3)) = X6) & (((X0 @ X6 @ X7)) = X2) & (((X0 @ X2 @ X7)) = X2) & (X7 != X3) & (((X1 @ X6 @ X3)) = X3) & (X5 != X2) & (((X1 @ X5 @ X3)) = X3) & (((X1 @ X2 @ X7)) = X7) & (X5 != X3) & (((X1 @ X2 @ X3)) = X3) & (((X0 @ X2 @ X6)) = X2) & (((X0 @ X5 @ X6)) = X2) & (((X1 @ X2 @ X5)) = X5) & (X7 != X2) & (((X0 @ X2 @ X5)) = X2) & (X2 != X3) & (((X0 @ X7 @ X3)) = X7) & (((X0 @ X5 @ X7)) = X2) & (((X1 @ X5 @ X6)) = X3) & (X6 != X3)) => ~ ! [X4 : a,X3 : a,X2 : a] : (((X1 @ X2 @ (X0 @ X3 @ X4))) = ((X0 @ (X1 @ X2 @ X3) @ (X1 @ X2 @ X4))))))),
% 1.00/0.37 inference(negated_conjecture,[status(cth)],[f1])).
% 1.00/0.37 thf(f3,plain,(
% 1.00/0.37 ~ ! [X1 : (a > a > a),X0 : (a > a > a)] : ((! [X8 : a,X7 : a] : (((X1 @ (X0 @ X7 @ X8) @ X8)) = X8) & ! [X11 : a,X10 : a] : (((X1 @ X11 @ X10)) = ((X1 @ X10 @ X11))) & ! [X9 : a] : (((X0 @ X9 @ X9)) = X9) & ! [X6 : a,X4 : a,X5 : a] : (((X0 @ (X0 @ X4 @ X6) @ X5)) = ((X0 @ X4 @ (X0 @ X6 @ X5)))) & ! [X2 : a,X3 : a] : (((X0 @ X2 @ X3)) = ((X0 @ X3 @ X2))) & ! [X15 : a,X14 : a,X16 : a] : (((X1 @ (X1 @ X14 @ X16) @ X15)) = ((X1 @ X14 @ (X1 @ X16 @ X15)))) & ! [X12 : a,X13 : a] : (((X0 @ (X1 @ X12 @ X13) @ X13)) = X13) & ! [X17 : a] : (((X1 @ X17 @ X17)) = X17)) => (? [X20 : a,X19 : a,X18 : a,X22 : a,X21 : a] : ((((X0 @ X20 @ X19)) = X19) & (((X1 @ X22 @ X18)) = X20) & (X20 != X22) & (((X1 @ X21 @ X19)) = X21) & (((X0 @ X20 @ X18)) = X18) & (X18 != X22) & (((X1 @ X20 @ X18)) = X20) & (((X1 @ X18 @ X19)) = X18) & (((X0 @ X20 @ X22)) = X22) & (((X0 @ X18 @ X21)) = X19) & (((X0 @ X22 @ X18)) = X19) & (((X1 @ X20 @ X19)) = X20) & (((X1 @ X22 @ X19)) = X22) & (X18 != X19) & (X18 != X20) & (((X1 @ X20 @ X21)) = X20) & (((X0 @ X18 @ X19)) = X19) & (X20 != X21) & (((X1 @ X22 @ X21)) = X20) & (X21 != X22) & (X18 != X21) & (X19 != X22) & (X19 != X21) & (((X0 @ X20 @ X21)) = X21) & (((X0 @ X21 @ X19)) = X19) & (((X1 @ X20 @ X22)) = X20) & (((X0 @ X22 @ X21)) = X19) & (X19 != X20) & (((X1 @ X18 @ X21)) = X20) & (((X0 @ X22 @ X19)) = X19)) => ~ ! [X24 : a,X25 : a,X23 : a] : (((X1 @ (X0 @ X25 @ X24) @ (X0 @ X25 @ X23))) = ((X0 @ X25 @ (X1 @ X24 @ X23))))))),
% 1.00/0.37 inference(rectify,[],[f2])).
% 1.00/0.37 thf(f4,plain,(
% 1.00/0.37 ? [X1 : (a > a > a),X0 : (a > a > a)] : ((! [X24 : a,X25 : a,X23 : a] : (((X1 @ (X0 @ X25 @ X24) @ (X0 @ X25 @ X23))) = ((X0 @ X25 @ (X1 @ X24 @ X23)))) & ? [X20 : a,X19 : a,X18 : a,X22 : a,X21 : a] : ((((X0 @ X20 @ X19)) = X19) & (((X1 @ X22 @ X18)) = X20) & (X20 != X22) & (((X1 @ X21 @ X19)) = X21) & (((X0 @ X20 @ X18)) = X18) & (X18 != X22) & (((X1 @ X20 @ X18)) = X20) & (((X1 @ X18 @ X19)) = X18) & (((X0 @ X20 @ X22)) = X22) & (((X0 @ X18 @ X21)) = X19) & (((X0 @ X22 @ X18)) = X19) & (((X1 @ X20 @ X19)) = X20) & (((X1 @ X22 @ X19)) = X22) & (X18 != X19) & (X18 != X20) & (((X1 @ X20 @ X21)) = X20) & (((X0 @ X18 @ X19)) = X19) & (X20 != X21) & (((X1 @ X22 @ X21)) = X20) & (X21 != X22) & (X18 != X21) & (X19 != X22) & (X19 != X21) & (((X0 @ X20 @ X21)) = X21) & (((X0 @ X21 @ X19)) = X19) & (((X1 @ X20 @ X22)) = X20) & (((X0 @ X22 @ X21)) = X19) & (X19 != X20) & (((X1 @ X18 @ X21)) = X20) & (((X0 @ X22 @ X19)) = X19))) & (! [X8 : a,X7 : a] : (((X1 @ (X0 @ X7 @ X8) @ X8)) = X8) & ! [X11 : a,X10 : a] : (((X1 @ X11 @ X10)) = ((X1 @ X10 @ X11))) & ! [X9 : a] : (((X0 @ X9 @ X9)) = X9) & ! [X6 : a,X4 : a,X5 : a] : (((X0 @ (X0 @ X4 @ X6) @ X5)) = ((X0 @ X4 @ (X0 @ X6 @ X5)))) & ! [X2 : a,X3 : a] : (((X0 @ X2 @ X3)) = ((X0 @ X3 @ X2))) & ! [X15 : a,X14 : a,X16 : a] : (((X1 @ (X1 @ X14 @ X16) @ X15)) = ((X1 @ X14 @ (X1 @ X16 @ X15)))) & ! [X12 : a,X13 : a] : (((X0 @ (X1 @ X12 @ X13) @ X13)) = X13) & ! [X17 : a] : (((X1 @ X17 @ X17)) = X17)))),
% 1.00/0.37 inference(ennf_transformation,[],[f3])).
% 1.00/0.37 thf(f5,plain,(
% 1.00/0.37 ? [X0 : (a > a > a),X1 : (a > a > a)] : (! [X8 : a,X7 : a] : (((X1 @ (X0 @ X7 @ X8) @ X8)) = X8) & ! [X6 : a,X4 : a,X5 : a] : (((X0 @ (X0 @ X4 @ X6) @ X5)) = ((X0 @ X4 @ (X0 @ X6 @ X5)))) & ! [X11 : a,X10 : a] : (((X1 @ X11 @ X10)) = ((X1 @ X10 @ X11))) & ! [X9 : a] : (((X0 @ X9 @ X9)) = X9) & ! [X12 : a,X13 : a] : (((X0 @ (X1 @ X12 @ X13) @ X13)) = X13) & ! [X2 : a,X3 : a] : (((X0 @ X2 @ X3)) = ((X0 @ X3 @ X2))) & ! [X17 : a] : (((X1 @ X17 @ X17)) = X17) & ! [X24 : a,X25 : a,X23 : a] : (((X1 @ (X0 @ X25 @ X24) @ (X0 @ X25 @ X23))) = ((X0 @ X25 @ (X1 @ X24 @ X23)))) & ! [X15 : a,X14 : a,X16 : a] : (((X1 @ (X1 @ X14 @ X16) @ X15)) = ((X1 @ X14 @ (X1 @ X16 @ X15)))) & ? [X20 : a,X19 : a,X18 : a,X22 : a,X21 : a] : ((((X0 @ X20 @ X19)) = X19) & (((X1 @ X22 @ X18)) = X20) & (X20 != X22) & (((X1 @ X21 @ X19)) = X21) & (((X0 @ X20 @ X18)) = X18) & (X18 != X22) & (((X1 @ X20 @ X18)) = X20) & (((X1 @ X18 @ X19)) = X18) & (((X0 @ X20 @ X22)) = X22) & (((X0 @ X18 @ X21)) = X19) & (((X0 @ X22 @ X18)) = X19) & (((X1 @ X20 @ X19)) = X20) & (((X1 @ X22 @ X19)) = X22) & (X18 != X19) & (X18 != X20) & (((X1 @ X20 @ X21)) = X20) & (((X0 @ X18 @ X19)) = X19) & (X20 != X21) & (((X1 @ X22 @ X21)) = X20) & (X21 != X22) & (X18 != X21) & (X19 != X22) & (X19 != X21) & (((X0 @ X20 @ X21)) = X21) & (((X0 @ X21 @ X19)) = X19) & (((X1 @ X20 @ X22)) = X20) & (((X0 @ X22 @ X21)) = X19) & (X19 != X20) & (((X1 @ X18 @ X21)) = X20) & (((X0 @ X22 @ X19)) = X19)))),
% 1.00/0.37 inference(flattening,[],[f4])).
% 1.00/0.37 thf(f6,plain,(
% 1.00/0.37 ? [X0 : (a > a > a),X1 : (a > a > a)] : (! [X2 : a,X3 : a] : (((X1 @ (X0 @ X3 @ X2) @ X2)) = X2) & ! [X4 : a,X5 : a,X6 : a] : (((X0 @ (X0 @ X5 @ X4) @ X6)) = ((X0 @ X5 @ (X0 @ X4 @ X6)))) & ! [X7 : a,X8 : a] : (((X1 @ X7 @ X8)) = ((X1 @ X8 @ X7))) & ! [X9 : a] : (((X0 @ X9 @ X9)) = X9) & ! [X10 : a,X11 : a] : (((X0 @ (X1 @ X10 @ X11) @ X11)) = X11) & ! [X12 : a,X13 : a] : (((X0 @ X13 @ X12)) = ((X0 @ X12 @ X13))) & ! [X14 : a] : (((X1 @ X14 @ X14)) = X14) & ! [X15 : a,X16 : a,X17 : a] : (((X1 @ (X0 @ X16 @ X15) @ (X0 @ X16 @ X17))) = ((X0 @ X16 @ (X1 @ X15 @ X17)))) & ! [X18 : a,X19 : a,X20 : a] : (((X1 @ X19 @ (X1 @ X20 @ X18))) = ((X1 @ (X1 @ X19 @ X20) @ X18))) & ? [X21 : a,X22 : a,X23 : a,X24 : a,X25 : a] : ((((X0 @ X21 @ X22)) = X22) & (((X1 @ X24 @ X23)) = X21) & (X21 != X24) & (((X1 @ X25 @ X22)) = X25) & (((X0 @ X21 @ X23)) = X23) & (X23 != X24) & (((X1 @ X21 @ X23)) = X21) & (((X1 @ X23 @ X22)) = X23) & (((X0 @ X21 @ X24)) = X24) & (((X0 @ X23 @ X25)) = X22) & (((X0 @ X24 @ X23)) = X22) & (((X1 @ X21 @ X22)) = X21) & (((X1 @ X24 @ X22)) = X24) & (X22 != X23) & (X21 != X23) & (((X1 @ X21 @ X25)) = X21) & (((X0 @ X23 @ X22)) = X22) & (X21 != X25) & (((X1 @ X24 @ X25)) = X21) & (X24 != X25) & (X23 != X25) & (X22 != X24) & (X22 != X25) & (((X0 @ X21 @ X25)) = X25) & (((X0 @ X25 @ X22)) = X22) & (((X1 @ X21 @ X24)) = X21) & (((X0 @ X24 @ X25)) = X22) & (X21 != X22) & (((X1 @ X23 @ X25)) = X21) & (((X0 @ X24 @ X22)) = X22)))),
% 1.00/0.37 inference(rectify,[],[f5])).
% 1.00/0.37 thf(f7,plain,(
% 1.00/0.37 ! [X2 : a,X3 : a] : (((sK1 @ (sK0 @ X3 @ X2) @ X2)) = X2) & ! [X4 : a,X5 : a,X6 : a] : (((sK0 @ (sK0 @ X5 @ X4) @ X6)) = ((sK0 @ X5 @ (sK0 @ X4 @ X6)))) & ! [X7 : a,X8 : a] : (((sK1 @ X8 @ X7)) = ((sK1 @ X7 @ X8))) & ! [X9 : a] : (((sK0 @ X9 @ X9)) = X9) & ! [X10 : a,X11 : a] : (((sK0 @ (sK1 @ X10 @ X11) @ X11)) = X11) & ! [X12 : a,X13 : a] : (((sK0 @ X12 @ X13)) = ((sK0 @ X13 @ X12))) & ! [X14 : a] : (((sK1 @ X14 @ X14)) = X14) & ! [X15 : a,X16 : a,X17 : a] : (((sK0 @ X16 @ (sK1 @ X15 @ X17))) = ((sK1 @ (sK0 @ X16 @ X15) @ (sK0 @ X16 @ X17)))) & ! [X18 : a,X19 : a,X20 : a] : (((sK1 @ X19 @ (sK1 @ X20 @ X18))) = ((sK1 @ (sK1 @ X19 @ X20) @ X18))) & ((((sK0 @ sK2 @ sK3)) = sK3) & (sK2 = ((sK1 @ sK5 @ sK4))) & (sK2 != sK5) & (((sK1 @ sK6 @ sK3)) = sK6) & (sK4 = ((sK0 @ sK2 @ sK4))) & (sK4 != sK5) & (sK2 = ((sK1 @ sK2 @ sK4))) & (sK4 = ((sK1 @ sK4 @ sK3))) & (((sK0 @ sK2 @ sK5)) = sK5) & (sK3 = ((sK0 @ sK4 @ sK6))) & (((sK0 @ sK5 @ sK4)) = sK3) & (((sK1 @ sK2 @ sK3)) = sK2) & (((sK1 @ sK5 @ sK3)) = sK5) & (sK4 != sK3) & (sK2 != sK4) & (sK2 = ((sK1 @ sK2 @ sK6))) & (sK3 = ((sK0 @ sK4 @ sK3))) & (sK2 != sK6) & (sK2 = ((sK1 @ sK5 @ sK6))) & (sK5 != sK6) & (sK4 != sK6) & (sK3 != sK5) & (sK3 != sK6) & (((sK0 @ sK2 @ sK6)) = sK6) & (((sK0 @ sK6 @ sK3)) = sK3) & (((sK1 @ sK2 @ sK5)) = sK2) & (sK3 = ((sK0 @ sK5 @ sK6))) & (sK2 != sK3) & (sK2 = ((sK1 @ sK4 @ sK6))) & (sK3 = ((sK0 @ sK5 @ sK3))))),
% 1.00/0.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X21,sK2),skolemize(X22,sK3),skolemize(X23,sK4),skolemize(X24,sK5),skolemize(X25,sK6)],[f6])).
% 1.00/0.37 thf(f19,plain,(
% 1.00/0.37 (sK2 = ((sK1 @ sK5 @ sK6)))),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f24,plain,(
% 1.00/0.37 (sK4 != sK3)),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f27,plain,(
% 1.00/0.37 (((sK0 @ sK5 @ sK4)) = sK3)),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f28,plain,(
% 1.00/0.37 (sK3 = ((sK0 @ sK4 @ sK6)))),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f36,plain,(
% 1.00/0.37 (sK2 = ((sK1 @ sK5 @ sK4)))),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f39,plain,(
% 1.00/0.37 ( ! [X16 : a,X17 : a,X15 : a] : ((((sK0 @ X16 @ (sK1 @ X15 @ X17))) = ((sK1 @ (sK0 @ X16 @ X15) @ (sK0 @ X16 @ X17))))) )),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f40,plain,(
% 1.00/0.37 ( ! [X14 : a] : ((((sK1 @ X14 @ X14)) = X14)) )),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f41,plain,(
% 1.00/0.37 ( ! [X12 : a,X13 : a] : ((((sK0 @ X12 @ X13)) = ((sK0 @ X13 @ X12)))) )),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f42,plain,(
% 1.00/0.37 ( ! [X10 : a,X11 : a] : ((((sK0 @ (sK1 @ X10 @ X11) @ X11)) = X11)) )),
% 1.00/0.37 inference(cnf_transformation,[],[f7])).
% 1.00/0.37 thf(f73,definition,(
% 1.00/0.37 spl7_6 <=> (sK2 = ((sK1 @ sK5 @ sK4)))),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition])).
% 1.00/0.37 thf(f75,plain,(
% 1.00/0.37 (sK2 = ((sK1 @ sK5 @ sK4))) | ~spl7_6),
% 1.00/0.37 inference(avatar_component_clause,[],[f73])).
% 1.00/0.37 thf(f76,plain,(
% 1.00/0.37 spl7_6),
% 1.00/0.37 inference(avatar_split_clause,[],[f36,f73])).
% 1.00/0.37 thf(f83,definition,(
% 1.00/0.37 spl7_8 <=> (((sK0 @ sK5 @ sK4)) = sK3)),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition])).
% 1.00/0.37 thf(f85,plain,(
% 1.00/0.37 (((sK0 @ sK5 @ sK4)) = sK3) | ~spl7_8),
% 1.00/0.37 inference(avatar_component_clause,[],[f83])).
% 1.00/0.37 thf(f86,plain,(
% 1.00/0.37 spl7_8),
% 1.00/0.37 inference(avatar_split_clause,[],[f27,f83])).
% 1.00/0.37 thf(f113,definition,(
% 1.00/0.37 spl7_14 <=> (sK3 = ((sK0 @ sK4 @ sK6)))),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_14])],[avatar_definition])).
% 1.00/0.37 thf(f115,plain,(
% 1.00/0.37 (sK3 = ((sK0 @ sK4 @ sK6))) | ~spl7_14),
% 1.00/0.37 inference(avatar_component_clause,[],[f113])).
% 1.00/0.37 thf(f116,plain,(
% 1.00/0.37 spl7_14),
% 1.00/0.37 inference(avatar_split_clause,[],[f28,f113])).
% 1.00/0.37 thf(f163,definition,(
% 1.00/0.37 spl7_24 <=> (sK4 = sK3)),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_24])],[avatar_definition])).
% 1.00/0.37 thf(f166,plain,(
% 1.00/0.37 ~spl7_24),
% 1.00/0.37 inference(avatar_split_clause,[],[f24,f163])).
% 1.00/0.37 thf(f178,definition,(
% 1.00/0.37 spl7_27 <=> (sK2 = ((sK1 @ sK5 @ sK6)))),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_27])],[avatar_definition])).
% 1.00/0.37 thf(f180,plain,(
% 1.00/0.37 (sK2 = ((sK1 @ sK5 @ sK6))) | ~spl7_27),
% 1.00/0.37 inference(avatar_component_clause,[],[f178])).
% 1.00/0.37 thf(f181,plain,(
% 1.00/0.37 spl7_27),
% 1.00/0.37 inference(avatar_split_clause,[],[f19,f178])).
% 1.00/0.37 thf(f206,plain,(
% 1.00/0.37 (sK3 = ((sK0 @ sK4 @ sK5))) | ~spl7_8),
% 1.00/0.37 inference(superposition,[],[f41,f85])).
% 1.00/0.37 thf(f237,definition,(
% 1.00/0.37 spl7_34 <=> (sK3 = ((sK0 @ sK4 @ sK5)))),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_34])],[avatar_definition])).
% 1.00/0.37 thf(f239,plain,(
% 1.00/0.37 (sK3 = ((sK0 @ sK4 @ sK5))) | ~spl7_34),
% 1.00/0.37 inference(avatar_component_clause,[],[f237])).
% 1.00/0.37 thf(f240,plain,(
% 1.00/0.37 spl7_34 | ~spl7_8),
% 1.00/0.37 inference(avatar_split_clause,[],[f206,f83,f237])).
% 1.00/0.37 thf(f262,plain,(
% 1.00/0.37 ( ! [X0 : a,X1 : a] : ((((sK0 @ X0 @ (sK1 @ X1 @ X0))) = X0)) )),
% 1.00/0.37 inference(superposition,[],[f42,f41])).
% 1.00/0.37 thf(f412,plain,(
% 1.00/0.37 ( ! [X0 : a] : ((((sK0 @ sK4 @ (sK1 @ X0 @ sK6))) = ((sK1 @ (sK0 @ sK4 @ X0) @ sK3)))) ) | ~spl7_14),
% 1.00/0.37 inference(superposition,[],[f39,f115])).
% 1.00/0.37 thf(f498,plain,(
% 1.00/0.37 (sK4 = ((sK0 @ sK4 @ sK2))) | ~spl7_6),
% 1.00/0.37 inference(superposition,[],[f262,f75])).
% 1.00/0.37 thf(f525,definition,(
% 1.00/0.37 spl7_45 <=> (sK4 = ((sK0 @ sK4 @ sK2)))),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_45])],[avatar_definition])).
% 1.00/0.37 thf(f530,plain,(
% 1.00/0.37 spl7_45 | ~spl7_6),
% 1.00/0.37 inference(avatar_split_clause,[],[f498,f73,f525])).
% 1.00/0.37 thf(f3196,plain,(
% 1.00/0.37 (((sK0 @ sK4 @ (sK1 @ sK5 @ sK6))) = ((sK1 @ sK3 @ sK3))) | (~spl7_14 | ~spl7_34)),
% 1.00/0.37 inference(superposition,[],[f412,f239])).
% 1.00/0.37 thf(f3230,plain,(
% 1.00/0.37 (sK3 = ((sK0 @ sK4 @ (sK1 @ sK5 @ sK6)))) | (~spl7_14 | ~spl7_34)),
% 1.00/0.37 inference(forward_demodulation,[],[f3196,f40])).
% 1.00/0.37 thf(f3247,plain,(
% 1.00/0.37 (((sK0 @ sK4 @ sK2)) = sK3) | (~spl7_14 | ~spl7_27 | ~spl7_34)),
% 1.00/0.37 inference(forward_demodulation,[],[f3230,f180])).
% 1.00/0.37 thf(f3254,definition,(
% 1.00/0.37 spl7_51 <=> (((sK0 @ sK4 @ sK2)) = sK3)),
% 1.00/0.37 introduced(definition,[new_symbols(definition,[spl7_51])],[avatar_definition])).
% 1.00/0.37 thf(f3257,plain,(
% 1.00/0.37 spl7_51 | ~spl7_14 | ~spl7_27 | ~spl7_34),
% 1.00/0.37 inference(avatar_split_clause,[],[f3247,f237,f178,f113,f3254])).
% 1.00/0.37 thf(f3266,definition,(
% 1.00/0.37 (sK4 != ((sK0 @ sK4 @ sK2))) | (((sK0 @ sK4 @ sK2)) != sK3) | (sK4 = sK3)),
% 1.00/0.37 introduced(theory,[theory_tautology_sat_conflict])).
% 1.00/0.37 cnf(s6, plain, spl7_6, inference(sat_conversion,[],[f76])).
% 1.00/0.37 cnf(s8, plain, spl7_8, inference(sat_conversion,[],[f86])).
% 1.00/0.37 cnf(s14, plain, spl7_14, inference(sat_conversion,[],[f116])).
% 1.00/0.37 cnf(s24, plain, ~spl7_24, inference(sat_conversion,[],[f166])).
% 1.00/0.37 cnf(s27, plain, spl7_27, inference(sat_conversion,[],[f181])).
% 1.00/0.37 cnf(s34, plain, ~spl7_8 | spl7_34, inference(sat_conversion,[],[f240])).
% 1.00/0.37 cnf(s95, plain, ~spl7_6 | spl7_45, inference(sat_conversion,[],[f530])).
% 1.00/0.37 cnf(s109, plain, ~spl7_14 | ~spl7_27 | ~spl7_34 | spl7_51, inference(sat_conversion,[],[f3257])).
% 1.00/0.37 cnf(s117, plain, spl7_24 | ~spl7_45 | ~spl7_51, inference(sat_conversion,[],[f3266])).
% 1.00/0.37 cnf(s135, plain, spl7_34, inference(rat,[],[s34,s8])).
% 1.00/0.37 cnf(s136, plain, spl7_51, inference(rat,[],[s109,s14,s27,s135])).
% 1.00/0.37 cnf(s137, plain, ~spl7_45, inference(rat,[],[s117,s24,s136])).
% 1.00/0.37 cnf(s138, plain, ~spl7_6, inference(rat,[],[s95,s137])).
% 1.00/0.37 cnf(s140, plain, $false, inference(rat,[],[s6,s138])).
% 1.00/0.37 thf(f3269,plain,(
% 1.00/0.37 $false),
% 1.00/0.37 inference(avatar_sat_refutation,[],[s140])).
% 1.00/0.37 % SZS output end Proof for theBenchmark
% 1.00/0.37 % (1354729)------------------------------
% 1.00/0.37 % (1354729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.00/0.37 % (1354729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.00/0.37 % (1354729)CaDiCaL version: 2.1.3
% 1.00/0.37 % (1354729)Termination reason: Refutation
% 1.00/0.37 % (1354729)Time elapsed: 0.112 s
% 1.00/0.37 % (1354729)Peak memory usage: 14 MB
% 1.00/0.37 % (1354729)Instructions burned: 221 (million)
% 1.00/0.37 % (1354721)Success in time 0.149 s
% 1.00/0.37 % Vampire exiting
%------------------------------------------------------------------------------