%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP107^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:08:22 AM UTC 2026
% Result : Theorem 0.30s 0.45s
% Output : Refutation 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP107^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:55:09 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.21/0.29 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.30/0.44 % (3651361)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.30/0.44 % (3651368)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2865139962:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.30/0.44 % (3651368)Instruction limit reached!
% 0.30/0.44 % (3651368)------------------------------
% 0.30/0.44 % (3651368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.44 % (3651368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.44 % (3651368)CaDiCaL version: 2.1.3
% 0.30/0.44 % (3651368)Termination reason: Instruction limit
% 0.30/0.44 % (3651368)Termination phase: shuffling
% 0.30/0.44 % (3651368)Time elapsed: 0.002 s
% 0.30/0.44 % (3651368)Peak memory usage: 10 MB
% 0.30/0.44 % (3651368)Instructions burned: 9 (million)
% 0.30/0.44 % (3651372)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.30/0.44 % (3651372)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.30/0.44 % (3651366)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4169157335:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.30/0.44 % (3651367)lrs+10_16_si=on:nwc=1.5:random_seed=3994299526:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.30/0.44 % (3651370)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3986684403:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.30/0.44 % (3651372)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=1022286868:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.30/0.44 % (3651369)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=997372232: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.30/0.44 % (3651371)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4082129441:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.30/0.44 % (3651374)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2821925279:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.30/0.44 % (3651374)Instruction limit reached!
% 0.30/0.44 % (3651374)------------------------------
% 0.30/0.44 % (3651374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.44 % (3651374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.44 % (3651374)CaDiCaL version: 2.1.3
% 0.30/0.44 % (3651374)Termination reason: Instruction limit
% 0.30/0.44 % (3651374)Termination phase: shuffling
% 0.30/0.44 % (3651374)Time elapsed: 0.001 s
% 0.30/0.44 % (3651374)Peak memory usage: 10 MB
% 0.30/0.44 % (3651374)Instructions burned: 4 (million)
% 0.30/0.44 % (3651367)Instruction limit reached!
% 0.30/0.44 % (3651367)------------------------------
% 0.30/0.44 % (3651367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.44 % (3651367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.44 % (3651367)CaDiCaL version: 2.1.3
% 0.30/0.44 % (3651367)Termination reason: Instruction limit
% 0.30/0.44 % (3651367)Termination phase: shuffling
% 0.30/0.44 % (3651367)Time elapsed: 0.009 s
% 0.30/0.44 % (3651367)Peak memory usage: 10 MB
% 0.30/0.44 % (3651367)Instructions burned: 19 (million)
% 0.30/0.44 % (3651370)Instruction limit reached!
% 0.30/0.44 % (3651370)------------------------------
% 0.30/0.44 % (3651370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.44 % (3651370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.44 % (3651370)CaDiCaL version: 2.1.3
% 0.30/0.44 % (3651370)Termination reason: Instruction limit
% 0.30/0.44 % (3651370)Termination phase: shuffling
% 0.30/0.44 % (3651370)Time elapsed: 0.011 s
% 0.30/0.44 % (3651370)Peak memory usage: 10 MB
% 0.30/0.44 % (3651370)Instructions burned: 24 (million)
% 0.30/0.44 % (3651382)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=965992761:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.30/0.45 % (3651382)Instruction limit reached!
% 0.30/0.45 % (3651382)------------------------------
% 0.30/0.45 % (3651382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651382)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651382)Termination reason: Instruction limit
% 0.30/0.45 % (3651382)Termination phase: shuffling
% 0.30/0.45 % (3651382)Time elapsed: 0.002 s
% 0.30/0.45 % (3651382)Peak memory usage: 10 MB
% 0.30/0.45 % (3651382)Instructions burned: 8 (million)
% 0.30/0.45 % (3651383)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.30/0.45 % (3651386)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.30/0.45 % (3651386)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.30/0.45 % (3651383)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1871755270:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.30/0.45 % (3651386)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4037170637: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.30/0.45 % (3651384)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2860260583:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.30/0.45 % (3651383)Instruction limit reached!
% 0.30/0.45 % (3651383)------------------------------
% 0.30/0.45 % (3651383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651383)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651383)Termination reason: Instruction limit
% 0.30/0.45 % (3651383)Termination phase: shuffling
% 0.30/0.45 % (3651383)Time elapsed: 0.004 s
% 0.30/0.45 % (3651383)Peak memory usage: 10 MB
% 0.30/0.45 % (3651383)Instructions burned: 8 (million)
% 0.30/0.45 % (3651371)Instruction limit reached!
% 0.30/0.45 % (3651371)------------------------------
% 0.30/0.45 % (3651371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651371)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651371)Termination reason: Instruction limit
% 0.30/0.45 % (3651371)Termination phase: Preprocessing 3
% 0.30/0.45 % (3651371)Time elapsed: 0.035 s
% 0.30/0.45 % (3651371)Peak memory usage: 11 MB
% 0.30/0.45 % (3651371)Instructions burned: 76 (million)
% 0.30/0.45 % (3651384)Instruction limit reached!
% 0.30/0.45 % (3651384)------------------------------
% 0.30/0.45 % (3651384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651384)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651384)Termination reason: Instruction limit
% 0.30/0.45 % (3651384)Termination phase: shuffling
% 0.30/0.45 % (3651384)Time elapsed: 0.006 s
% 0.30/0.45 % (3651384)Peak memory usage: 10 MB
% 0.30/0.45 % (3651384)Instructions burned: 13 (million)
% 0.30/0.45 % (3651386)Instruction limit reached!
% 0.30/0.45 % (3651386)------------------------------
% 0.30/0.45 % (3651386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651386)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651386)Termination reason: Instruction limit
% 0.30/0.45 % (3651386)Termination phase: shuffling
% 0.30/0.45 % (3651386)Time elapsed: 0.007 s
% 0.30/0.45 % (3651386)Peak memory usage: 10 MB
% 0.30/0.45 % (3651386)Instructions burned: 31 (million)
% 0.30/0.45 % (3651366)Instruction limit reached!
% 0.30/0.45 % (3651366)------------------------------
% 0.30/0.45 % (3651366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651366)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651366)Termination reason: Instruction limit
% 0.30/0.45 % (3651366)Termination phase: Property scanning
% 0.30/0.45 % (3651366)Time elapsed: 0.040 s
% 0.30/0.45 % (3651366)Peak memory usage: 12 MB
% 0.30/0.45 % (3651366)Instructions burned: 87 (million)
% 0.30/0.45 % (3651390)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=2258021340:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.30/0.45 % (3651392)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.30/0.45 % (3651391)lrs+10_1_si=on:cs=on:random_seed=4269433057:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.30/0.45 % (3651392)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=1022306538:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.30/0.45 % (3651393)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3171947406:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.30/0.45 % (3651394)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1319966648:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.30/0.45 % (3651392)Instruction limit reached!
% 0.30/0.45 % (3651392)------------------------------
% 0.30/0.45 % (3651392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651392)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651392)Termination reason: Instruction limit
% 0.30/0.45 % (3651392)Termination phase: shuffling
% 0.30/0.45 % (3651392)Time elapsed: 0.002 s
% 0.30/0.45 % (3651392)Peak memory usage: 10 MB
% 0.30/0.45 % (3651392)Instructions burned: 3 (million)
% 0.30/0.45 % (3651391)Instruction limit reached!
% 0.30/0.45 % (3651391)------------------------------
% 0.30/0.45 % (3651391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651391)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651391)Termination reason: Instruction limit
% 0.30/0.45 % (3651391)Termination phase: shuffling
% 0.30/0.45 % (3651391)Time elapsed: 0.004 s
% 0.30/0.45 % (3651391)Peak memory usage: 10 MB
% 0.30/0.45 % (3651391)Instructions burned: 8 (million)
% 0.30/0.45 % (3651372)Instruction limit reached!
% 0.30/0.45 % (3651372)------------------------------
% 0.30/0.45 % (3651372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651372)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651372)Termination reason: Instruction limit
% 0.30/0.45 % (3651372)Termination phase: Property scanning
% 0.30/0.45 % (3651372)Time elapsed: 0.066 s
% 0.30/0.45 % (3651372)Peak memory usage: 12 MB
% 0.30/0.45 % (3651372)Instructions burned: 157 (million)
% 0.30/0.45 % (3651393)Instruction limit reached!
% 0.30/0.45 % (3651393)------------------------------
% 0.30/0.45 % (3651393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651393)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651393)Termination reason: Instruction limit
% 0.30/0.45 % (3651393)Termination phase: Property scanning
% 0.30/0.45 % (3651393)Time elapsed: 0.017 s
% 0.30/0.45 % (3651393)Peak memory usage: 10 MB
% 0.30/0.45 % (3651393)Instructions burned: 40 (million)
% 0.30/0.45 % (3651400)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3746292251:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.30/0.45 % (3651401)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3031987021:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.30/0.45 % (3651402)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1837802325:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.30/0.45 % (3651401)Instruction limit reached!
% 0.30/0.45 % (3651401)------------------------------
% 0.30/0.45 % (3651401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651401)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651401)Termination reason: Instruction limit
% 0.30/0.45 % (3651401)Termination phase: shuffling
% 0.30/0.45 % (3651401)Time elapsed: 0.007 s
% 0.30/0.45 % (3651401)Peak memory usage: 10 MB
% 0.30/0.45 % (3651401)Instructions burned: 16 (million)
% 0.30/0.45 % (3651390)Instruction limit reached!
% 0.30/0.45 % (3651390)------------------------------
% 0.30/0.45 % (3651390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651390)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651390)Termination reason: Instruction limit
% 0.30/0.45 % (3651390)Termination phase: Property scanning
% 0.30/0.45 % (3651390)Time elapsed: 0.034 s
% 0.30/0.45 % (3651390)Peak memory usage: 11 MB
% 0.30/0.45 % (3651390)Instructions burned: 88 (million)
% 0.30/0.45 % (3651400)Instruction limit reached!
% 0.30/0.45 % (3651400)------------------------------
% 0.30/0.45 % (3651400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651400)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651400)Termination reason: Instruction limit
% 0.30/0.45 % (3651400)Termination phase: shuffling
% 0.30/0.45 % (3651400)Time elapsed: 0.012 s
% 0.30/0.45 % (3651400)Peak memory usage: 10 MB
% 0.30/0.45 % (3651400)Instructions burned: 27 (million)
% 0.30/0.45 % (3651369) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3651361-3651369"...
% 0.30/0.45 % (3651394)Refutation not found, incomplete strategy
% 0.30/0.45 % (3651394)------------------------------
% 0.30/0.45 % (3651394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651403)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2767102478:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.30/0.45 % (3651394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651394)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651394)Termination reason: Refutation not found, incomplete strategy
% 0.30/0.45 % (3651394)Time elapsed: 0.034 s
% 0.30/0.45 % (3651394)Peak memory usage: 13 MB
% 0.30/0.45 % (3651394)Instructions burned: 74 (million)
% 0.30/0.45 % (3651369)...printing done.
% 0.30/0.45 % (3651394)------------------------------
% 0.30/0.45 % (3651394)------------------------------
% 0.30/0.45 % (3651369)Refutation found. Thanks to Tanya!
% 0.30/0.45 % SZS status Theorem for theBenchmark
% 0.30/0.45 % SZS output start Proof for theBenchmark
% 0.30/0.45 thf(type_def_5, type, partia539144763t_unit: $tType).
% 0.30/0.45 thf(type_def_6, type, partia1993116613t_unit: $tType).
% 0.30/0.45 thf(type_def_7, type, partia1833973666xt_a_b: $tType).
% 0.30/0.45 thf(type_def_8, type, partia96731725t_unit: $tType).
% 0.30/0.45 thf(type_def_9, type, set_se1596668135od_a_a: $tType).
% 0.30/0.45 thf(type_def_10, type, set_Product_prod_a_a: $tType).
% 0.30/0.45 thf(type_def_11, type, product_prod_a_a: $tType).
% 0.30/0.45 thf(type_def_12, type, set_set_a: $tType).
% 0.30/0.45 thf(type_def_13, type, set_a: $tType).
% 0.30/0.45 thf(type_def_14, type, nat: $tType).
% 0.30/0.45 thf(type_def_15, type, int: $tType).
% 0.30/0.45 thf(type_def_16, type, a: $tType).
% 0.30/0.45 thf(type_def_17, type, sTfun: ($tType * $tType) > $tType).
% 0.30/0.45 thf(func_def_0, type, a_RCOSETS_a_b: (partia1833973666xt_a_b > set_a > set_set_a)).
% 0.30/0.45 thf(func_def_1, type, a_l_coset_a_b: (partia1833973666xt_a_b > a > set_a > set_a)).
% 0.30/0.45 thf(func_def_2, type, a_r_coset_a_b: (partia1833973666xt_a_b > set_a > a > set_a)).
% 0.30/0.45 thf(func_def_3, type, additi2104487374up_a_b: (set_a > partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_4, type, set_add_a_b: (partia1833973666xt_a_b > set_a > set_a > set_a)).
% 0.30/0.45 thf(func_def_5, type, equiva2136214035t_unit: (partia1993116613t_unit > $o)).
% 0.30/0.45 thf(func_def_6, type, partia206007992t_unit: (partia1993116613t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_7, type, partia616129906t_unit: (partia539144763t_unit > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_8, type, partia1955795460t_unit: (partia96731725t_unit > set_a)).
% 0.30/0.45 thf(func_def_9, type, partia1066395285xt_a_b: (partia1833973666xt_a_b > set_a)).
% 0.30/0.45 thf(func_def_10, type, units_1734235042t_unit: (partia539144763t_unit > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_11, type, units_a_Product_unit: (partia96731725t_unit > set_a)).
% 0.30/0.45 thf(func_def_12, type, units_a_ring_ext_a_b: (partia1833973666xt_a_b > set_a)).
% 0.30/0.45 thf(func_def_13, type, group_52730354t_unit: (partia539144763t_unit > $o)).
% 0.30/0.45 thf(func_def_14, type, group_a_Product_unit: (partia96731725t_unit > $o)).
% 0.30/0.45 thf(func_def_15, type, group_a_ring_ext_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_16, type, monoid1242292471t_unit: (partia539144763t_unit > $o)).
% 0.30/0.45 thf(func_def_17, type, monoid1447254976t_unit: (partia96731725t_unit > $o)).
% 0.30/0.45 thf(func_def_18, type, monoid1022105667xt_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_19, type, mult_s977248631t_unit: (partia539144763t_unit > set_Product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_20, type, mult_a_Product_unit: (partia96731725t_unit > a > a > a)).
% 0.30/0.45 thf(func_def_21, type, mult_a_ring_ext_a_b: (partia1833973666xt_a_b > a > a > a)).
% 0.30/0.45 thf(func_def_22, type, one_se1488596747t_unit: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_23, type, one_a_Product_unit: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_24, type, one_a_ring_ext_a_b: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_25, type, units_390215097t_unit: (partia539144763t_unit > partia539144763t_unit)).
% 0.30/0.45 thf(func_def_26, type, units_1411277569xt_a_b: (partia1833973666xt_a_b > partia96731725t_unit)).
% 0.30/0.45 thf(func_def_27, type, minus_minus_set_a: (set_a > set_a > set_a)).
% 0.30/0.45 thf(func_def_28, type, locali1170246543t_unit: (partia1993116613t_unit > a > a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_29, type, locali1648887798ac_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.30/0.45 thf(func_def_30, type, locali1944243560ac_a_b: (partia1833973666xt_a_b > set_a > partia539144763t_unit)).
% 0.30/0.45 thf(func_def_31, type, locali807230110ng_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.30/0.45 thf(func_def_32, type, locali880295127ng_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.30/0.45 thf(func_def_33, type, locali1538946157t_unit: (partia1993116613t_unit > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_34, type, locali1488796916t_unit: (partia539144763t_unit > set_se1596668135od_a_a > $o)).
% 0.30/0.45 thf(func_def_35, type, locali425460998xt_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.30/0.45 thf(func_def_36, type, bot_bo2131659635od_a_a: set_Product_prod_a_a).
% 0.30/0.45 thf(func_def_37, type, bot_bo1424703315od_a_a: set_se1596668135od_a_a).
% 0.30/0.45 thf(func_def_38, type, bot_bot_set_set_a: set_set_a).
% 0.30/0.45 thf(func_def_39, type, bot_bot_set_a: set_a).
% 0.30/0.45 thf(func_def_40, type, ord_le1824328871od_a_a: (set_Product_prod_a_a > set_Product_prod_a_a > $o)).
% 0.30/0.45 thf(func_def_41, type, ord_le391835783od_a_a: (set_se1596668135od_a_a > set_se1596668135od_a_a > $o)).
% 0.30/0.45 thf(func_def_42, type, ord_le318720350_set_a: (set_set_a > set_set_a > $o)).
% 0.30/0.45 thf(func_def_43, type, ord_less_eq_set_a: (set_a > set_a > $o)).
% 0.30/0.45 thf(func_def_44, type, product_Pair_a_a: (a > a > product_prod_a_a)).
% 0.30/0.45 thf(func_def_45, type, abelian_monoid_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_46, type, add_pow_a_b_int: (partia1833973666xt_a_b > int > a > a)).
% 0.30/0.45 thf(func_def_47, type, add_pow_a_b_nat: (partia1833973666xt_a_b > nat > a > a)).
% 0.30/0.45 thf(func_def_48, type, field_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_49, type, ring_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_50, type, zero_a_b: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_51, type, semiring_a_b: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_52, type, collec645855634od_a_a: ((product_prod_a_a > $o) > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_53, type, collec183727474od_a_a: ((set_Product_prod_a_a > $o) > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_54, type, collect_set_a: ((set_a > $o) > set_set_a)).
% 0.30/0.45 thf(func_def_55, type, collect_a: ((a > $o) > set_a)).
% 0.30/0.45 thf(func_def_56, type, pow_a: (set_a > set_set_a)).
% 0.30/0.45 thf(func_def_57, type, insert1116662519od_a_a: (product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_58, type, insert1738756823od_a_a: (set_Product_prod_a_a > set_se1596668135od_a_a > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_59, type, insert_set_a: (set_a > set_set_a > set_set_a)).
% 0.30/0.45 thf(func_def_60, type, insert_a: (a > set_a > set_a)).
% 0.30/0.45 thf(func_def_61, type, member449909584od_a_a: (product_prod_a_a > set_Product_prod_a_a > $o)).
% 0.30/0.45 thf(func_def_62, type, member1838126896od_a_a: (set_Product_prod_a_a > set_se1596668135od_a_a > $o)).
% 0.30/0.45 thf(func_def_63, type, member_set_a: (set_a > set_set_a > $o)).
% 0.30/0.45 thf(func_def_64, type, member_a: (a > set_a > $o)).
% 0.30/0.45 thf(func_def_65, type, r: partia1833973666xt_a_b).
% 0.30/0.45 thf(func_def_66, type, s: set_a).
% 0.30/0.45 thf(func_def_67, type, r2: a).
% 0.30/0.45 thf(func_def_68, type, r3: a).
% 0.30/0.45 thf(func_def_69, type, rel: partia1993116613t_unit).
% 0.30/0.45 thf(func_def_70, type, s2: a).
% 0.30/0.45 thf(func_def_71, type, s3: a).
% 0.30/0.45 thf(func_def_75, type, db0: !>[X0: $tType]:(X0)).
% 0.30/0.45 thf(func_def_76, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.30/0.45 thf(func_def_77, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.30/0.45 thf(func_def_78, type, vIMP: ($o > $o > $o)).
% 0.30/0.45 thf(func_def_79, type, db2: !>[X0: $tType]:(X0)).
% 0.30/0.45 thf(func_def_80, type, db1: !>[X0: $tType]:(X0)).
% 0.30/0.45 thf(func_def_81, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.30/0.45 thf(func_def_82, type, vAND: ($o > $o > $o)).
% 0.30/0.45 thf(func_def_83, type, db3: !>[X0: $tType]:(X0)).
% 0.30/0.45 thf(func_def_84, type, sP0: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_85, type, sP1: (partia539144763t_unit > $o)).
% 0.30/0.45 thf(func_def_86, type, sP2: (partia539144763t_unit > $o)).
% 0.30/0.45 thf(func_def_87, type, sP3: (partia96731725t_unit > $o)).
% 0.30/0.45 thf(func_def_88, type, sP4: (partia539144763t_unit > $o)).
% 0.30/0.45 thf(func_def_89, type, sP5: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_90, type, sP6: (partia1833973666xt_a_b > $o)).
% 0.30/0.45 thf(func_def_91, type, sK7: (set_se1596668135od_a_a > set_se1596668135od_a_a > set_Product_prod_a_a > set_Product_prod_a_a > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_92, type, sK8: (a > a)).
% 0.30/0.45 thf(func_def_93, type, sK9: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_94, type, sK10: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_95, type, sK11: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_96, type, sK12: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_97, type, sK13: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_98, type, sK14: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_99, type, sK15: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_100, type, sK16: (set_a > a > set_a)).
% 0.30/0.45 thf(func_def_101, type, sK17: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_102, type, sK18: (set_a > a)).
% 0.30/0.45 thf(func_def_103, type, sK19: (set_Product_prod_a_a > product_prod_a_a)).
% 0.30/0.45 thf(func_def_104, type, sK20: (set_se1596668135od_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_105, type, sK21: ((a > $o) > (a > $o) > a)).
% 0.30/0.45 thf(func_def_106, type, sK22: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_107, type, sK23: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_108, type, sK24: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_109, type, sK25: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_110, type, sK26: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_111, type, sK27: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_112, type, sK28: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_113, type, sK29: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_114, type, sK30: (a > partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_115, type, sK31: (set_Product_prod_a_a > set_se1596668135od_a_a > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_116, type, sK32: (set_Product_prod_a_a > product_prod_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_117, type, sK33: (set_Product_prod_a_a > partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_118, type, sK34: ((a > $o) > a)).
% 0.30/0.45 thf(func_def_119, type, sK35: (a > a)).
% 0.30/0.45 thf(func_def_120, type, sK36: ((set_a > $o) > (set_a > $o) > set_a)).
% 0.30/0.45 thf(func_def_121, type, sK37: (set_set_a > set_a)).
% 0.30/0.45 thf(func_def_122, type, sK38: ((product_prod_a_a > $o) > product_prod_a_a)).
% 0.30/0.45 thf(func_def_123, type, sK39: (set_Product_prod_a_a > product_prod_a_a)).
% 0.30/0.45 thf(func_def_124, type, sK40: a).
% 0.30/0.45 thf(func_def_125, type, sK41: (set_a > a)).
% 0.30/0.45 thf(func_def_126, type, sK42: ((product_prod_a_a > $o) > a)).
% 0.30/0.45 thf(func_def_127, type, sK43: ((product_prod_a_a > $o) > a)).
% 0.30/0.45 thf(func_def_128, type, sK44: (set_Product_prod_a_a > partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_129, type, sK45: (product_prod_a_a > product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_130, type, sK46: ((a > $o) > a)).
% 0.30/0.45 thf(func_def_131, type, sK47: ((a > $o) > (a > $o) > a)).
% 0.30/0.45 thf(func_def_132, type, sK48: (a > partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_133, type, sK49: (set_a > set_a > set_set_a > set_set_a > set_set_a)).
% 0.30/0.45 thf(func_def_134, type, sK50: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_135, type, sK51: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_136, type, sK52: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_137, type, sK53: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_138, type, sK54: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_139, type, sK55: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_140, type, sK56: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_141, type, sK57: (partia1833973666xt_a_b > a > a)).
% 0.30/0.45 thf(func_def_142, type, sK58: (set_Product_prod_a_a > set_se1596668135od_a_a > set_se1596668135od_a_a)).
% 0.30/0.45 thf(func_def_143, type, sK59: a).
% 0.30/0.45 thf(func_def_144, type, sK60: (set_Product_prod_a_a > partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_145, type, sK61: (set_a > set_set_a > set_set_a)).
% 0.30/0.45 thf(func_def_146, type, sK62: (set_a > a)).
% 0.30/0.45 thf(func_def_147, type, sK63: (set_Product_prod_a_a > partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_148, type, sK64: (a > partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_149, type, sK65: (set_se1596668135od_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_150, type, sK66: (set_set_a > set_set_a > set_a)).
% 0.30/0.45 thf(func_def_151, type, sK67: (set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a)).
% 0.30/0.45 thf(func_def_152, type, sK68: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_153, type, sK69: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_154, type, sK70: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_155, type, sK71: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_156, type, sK72: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_157, type, sK73: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_158, type, sK74: (partia96731725t_unit > a)).
% 0.30/0.45 thf(func_def_159, type, sK75: (set_a > a > set_a)).
% 0.30/0.45 thf(func_def_160, type, sK76: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_161, type, sK77: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_162, type, sK78: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_163, type, sK79: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_164, type, sK80: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_165, type, sK81: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_166, type, sK82: (partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_167, type, sK83: (product_prod_a_a > a)).
% 0.30/0.45 thf(func_def_168, type, sK84: (product_prod_a_a > a)).
% 0.30/0.45 thf(func_def_169, type, sK85: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_170, type, sK86: (product_prod_a_a > a)).
% 0.30/0.45 thf(func_def_171, type, sK87: (product_prod_a_a > a)).
% 0.30/0.45 thf(func_def_172, type, sK88: ((set_a > $o) > (set_a > $o) > set_a)).
% 0.30/0.45 thf(func_def_173, type, sK89: (set_set_a > set_a > set_set_a)).
% 0.30/0.45 thf(func_def_174, type, sK90: (a > a)).
% 0.30/0.45 thf(func_def_175, type, sK91: (set_se1596668135od_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_176, type, sK92: (set_Product_prod_a_a > product_prod_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_177, type, sK93: ((product_prod_a_a > $o) > a)).
% 0.30/0.45 thf(func_def_178, type, sK94: ((product_prod_a_a > $o) > a)).
% 0.30/0.45 thf(func_def_179, type, sK95: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_180, type, sK96: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_181, type, sK97: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_182, type, sK98: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_183, type, sK99: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_184, type, sK100: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_185, type, sK101: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_186, type, sK102: (set_se1596668135od_a_a > set_se1596668135od_a_a > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_187, type, sK103: ((product_prod_a_a > $o) > product_prod_a_a)).
% 0.30/0.45 thf(func_def_188, type, sK104: a).
% 0.30/0.45 thf(func_def_189, type, sK105: (partia1833973666xt_a_b > a > a)).
% 0.30/0.45 thf(func_def_190, type, sK106: (set_Product_prod_a_a > product_prod_a_a)).
% 0.30/0.45 thf(func_def_191, type, sK107: (set_Product_prod_a_a > partia539144763t_unit > set_Product_prod_a_a)).
% 0.30/0.45 thf(func_def_192, type, sK108: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_193, type, sK109: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_194, type, sK110: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_195, type, sK111: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_196, type, sK112: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_197, type, sK113: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_198, type, sK114: (partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_199, type, sK115: (a > partia1833973666xt_a_b > a)).
% 0.30/0.45 thf(func_def_200, type, sK116: (partia1833973666xt_a_b > a > a)).
% 0.30/0.45 thf(func_def_201, type, sK117: (set_set_a > set_a)).
% 0.30/0.45 thf(func_def_202, type, sK118: (a > set_a > set_a > a > set_a)).
% 0.30/0.45 thf(func_def_203, type, sK119: (set_a > set_a > a)).
% 0.30/0.45 thf(func_def_204, type, sK120: (set_set_a > set_a)).
% 0.30/0.45 thf(func_def_205, type, vNOT: ($o > $o)).
% 0.30/0.45 thf(f1,axiom,(
% 0.30/0.45 (((mult_a_ring_ext_a_b @ r @ r2 @ r3)) = ((mult_a_ring_ext_a_b @ r @ r3 @ r2)))),
% 0.30/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_f3)).
% 0.30/0.45 thf(f2,axiom,(
% 0.30/0.45 (((mult_a_ring_ext_a_b @ r @ s2 @ s3)) = ((mult_a_ring_ext_a_b @ r @ s3 @ s2)))),
% 0.30/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_f4)).
% 0.30/0.45 thf(f4,axiom,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r2 @ r3) @ (mult_a_ring_ext_a_b @ r @ s2 @ s3))))),
% 0.30/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_f1)).
% 0.30/0.45 thf(f5,axiom,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r3 @ r2) @ (mult_a_ring_ext_a_b @ r @ s3 @ s2))))),
% 0.30/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_f2)).
% 0.30/0.45 thf(f356,conjecture,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 0.30/0.45 thf(f357,negated_conjecture,(
% 0.30/0.45 ~ (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 inference(negated_conjecture,[status(cth)],[f356])).
% 0.30/0.45 thf(f1013,plain,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) != ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 inference(flattening,[],[f357])).
% 0.30/0.45 thf(f1867,plain,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r3 @ r2) @ (mult_a_ring_ext_a_b @ r @ s3 @ s2))))),
% 0.30/0.45 inference(cnf_transformation,[],[f5])).
% 0.30/0.45 thf(f1915,plain,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r2 @ r3) @ (mult_a_ring_ext_a_b @ r @ s2 @ s3))))),
% 0.30/0.45 inference(cnf_transformation,[],[f4])).
% 0.30/0.45 thf(f2153,plain,(
% 0.30/0.45 (((mult_a_ring_ext_a_b @ r @ s2 @ s3)) = ((mult_a_ring_ext_a_b @ r @ s3 @ s2)))),
% 0.30/0.45 inference(cnf_transformation,[],[f2])).
% 0.30/0.45 thf(f2156,plain,(
% 0.30/0.45 (((mult_a_ring_ext_a_b @ r @ r2 @ r3)) = ((mult_a_ring_ext_a_b @ r @ r3 @ r2)))),
% 0.30/0.45 inference(cnf_transformation,[],[f1])).
% 0.30/0.45 thf(f2178,plain,(
% 0.30/0.45 (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) != ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 inference(cnf_transformation,[],[f1013])).
% 0.30/0.45 thf(f2602,definition,(
% 0.30/0.45 spl121_13 <=> (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 introduced(definition,[new_symbols(definition,[spl121_13])],[avatar_definition])).
% 0.30/0.45 thf(f2605,plain,(
% 0.30/0.45 ~spl121_13),
% 0.30/0.45 inference(avatar_split_clause,[],[f2178,f2602])).
% 0.30/0.45 thf(f2637,definition,(
% 0.30/0.45 spl121_20 <=> (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r2 @ r3) @ (mult_a_ring_ext_a_b @ r @ s2 @ s3))))),
% 0.30/0.45 introduced(definition,[new_symbols(definition,[spl121_20])],[avatar_definition])).
% 0.30/0.45 thf(f2640,plain,(
% 0.30/0.45 spl121_20),
% 0.30/0.45 inference(avatar_split_clause,[],[f1915,f2637])).
% 0.30/0.45 thf(f2657,definition,(
% 0.30/0.45 spl121_24 <=> (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))) = ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r3 @ r2) @ (mult_a_ring_ext_a_b @ r @ s3 @ s2))))),
% 0.30/0.45 introduced(definition,[new_symbols(definition,[spl121_24])],[avatar_definition])).
% 0.30/0.45 thf(f2660,plain,(
% 0.30/0.45 spl121_24),
% 0.30/0.45 inference(avatar_split_clause,[],[f1867,f2657])).
% 0.30/0.45 thf(f2683,definition,(
% 0.30/0.45 spl121_29 <=> (((mult_a_ring_ext_a_b @ r @ r2 @ r3)) = ((mult_a_ring_ext_a_b @ r @ r3 @ r2)))),
% 0.30/0.45 introduced(definition,[new_symbols(definition,[spl121_29])],[avatar_definition])).
% 0.30/0.45 thf(f2686,plain,(
% 0.30/0.45 spl121_29),
% 0.30/0.45 inference(avatar_split_clause,[],[f2156,f2683])).
% 0.30/0.45 thf(f2736,definition,(
% 0.30/0.45 spl121_40 <=> (((mult_a_ring_ext_a_b @ r @ s2 @ s3)) = ((mult_a_ring_ext_a_b @ r @ s3 @ s2)))),
% 0.30/0.45 introduced(definition,[new_symbols(definition,[spl121_40])],[avatar_definition])).
% 0.30/0.45 thf(f2739,plain,(
% 0.30/0.45 spl121_40),
% 0.30/0.45 inference(avatar_split_clause,[],[f2153,f2736])).
% 0.30/0.45 thf(f2792,definition,(
% 0.30/0.45 (((mult_a_ring_ext_a_b @ r @ r2 @ r3)) != ((mult_a_ring_ext_a_b @ r @ r3 @ r2))) | (((mult_a_ring_ext_a_b @ r @ s2 @ s3)) != ((mult_a_ring_ext_a_b @ r @ s3 @ s2))) | (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))) != ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r3 @ r2) @ (mult_a_ring_ext_a_b @ r @ s3 @ s2)))) | (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) != ((locali1170246543t_unit @ rel @ (mult_a_ring_ext_a_b @ r @ r2 @ r3) @ (mult_a_ring_ext_a_b @ r @ s2 @ s3)))) | (((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r2 @ s2) @ (locali1170246543t_unit @ rel @ r3 @ s3))) = ((mult_s977248631t_unit @ (locali1944243560ac_a_b @ r @ s) @ (locali1170246543t_unit @ rel @ r3 @ s3) @ (locali1170246543t_unit @ rel @ r2 @ s2))))),
% 0.30/0.45 introduced(theory,[theory_tautology_sat_conflict])).
% 0.30/0.45 cnf(s10, plain, ~spl121_13, inference(sat_conversion,[],[f2605])).
% 0.30/0.45 cnf(s17, plain, spl121_20, inference(sat_conversion,[],[f2640])).
% 0.30/0.45 cnf(s21, plain, spl121_24, inference(sat_conversion,[],[f2660])).
% 0.30/0.45 cnf(s29, plain, spl121_29, inference(sat_conversion,[],[f2686])).
% 0.30/0.45 cnf(s40, plain, spl121_40, inference(sat_conversion,[],[f2739])).
% 0.30/0.45 cnf(s56, plain, spl121_13 | ~spl121_20 | ~spl121_24 | ~spl121_29 | ~spl121_40, inference(sat_conversion,[],[f2792])).
% 0.30/0.45 cnf(s57, plain, spl121_13, inference(rat,[],[s56,s40,s29,s21,s17])).
% 0.30/0.45 cnf(s58, plain, $false, inference(rat,[],[s10,s57])).
% 0.30/0.45 thf(f2793,plain,(
% 0.30/0.45 $false),
% 0.30/0.45 inference(avatar_sat_refutation,[],[s58])).
% 0.30/0.45 % SZS output end Proof for theBenchmark
% 0.30/0.45 % (3651369)------------------------------
% 0.30/0.45 % (3651369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.45 % (3651369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.45 % (3651369)CaDiCaL version: 2.1.3
% 0.30/0.45 % (3651369)Termination reason: Refutation
% 0.30/0.45 % (3651369)Time elapsed: 0.092 s
% 0.30/0.45 % (3651369)Peak memory usage: 14 MB
% 0.30/0.45 % (3651369)Instructions burned: 201 (million)
% 0.30/0.45 % (3651361)Success in time 0.146 s
% 0.30/0.45 % Vampire exiting
%------------------------------------------------------------------------------