%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX002_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 : Tue Sep 29 01:45:39 PM UTC 2026
% Result : Theorem 7.62s 1.46s
% Output : Refutation 7.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWX002_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 14:50:49 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.43/0.87 % (3432955)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.43/0.87 % (3432962)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1593223819:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.43/0.87 % Exception at run slice level
% 3.43/0.87 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 3.43/0.87 % (3432960)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2231141468:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.43/0.87 % (3432961)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=943394462:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.43/0.87 % (3432963)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3527684263:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.43/0.87 % (3432964)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4064820045:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.43/0.87 % Exception at run slice level% Exception at run slice level
% 3.43/0.87
% 3.43/0.87 User error: User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 3.43/0.87
% 3.43/0.87 % Exception at run slice level
% 3.43/0.87 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 3.43/0.87 % Exception at run slice level
% 3.43/0.87 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 3.43/0.87 % (3432965)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1433042025:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.43/0.87 % (3432966)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2448944418:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.43/0.87 % Exception at run slice level% Exception at run slice level
% 3.43/0.87
% 3.43/0.87 User error: User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 3.43/0.87
% 3.43/0.87 % (3432973)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=4103847504:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2999 on theBenchmark for (2999ds/29Mi)
% 3.43/0.87 % Exception at run slice level
% 3.43/0.87 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 3.43/0.87 % (3432972)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3238701552:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2999 on theBenchmark for (2999ds/14Mi)
% 3.43/0.87 % (3432974)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2693426961:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2999 on theBenchmark for (2999ds/16Mi)
% 3.43/0.87 % Exception at run slice level% Exception at run slice level
% 3.43/0.87
% 3.43/0.87 User error: User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 3.43/0.87
% 3.43/0.87 % (3432976)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=2977381059:i=27:canc=cautious:fsr=off:rtra=on_2999 on theBenchmark for (2999ds/27Mi)
% 3.43/0.87 % (3432975)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1057905833:i=24:canc=force:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 3.43/0.87 % Exception at run slice level% Exception at run slice level
% 3.43/0.87
% 3.43/0.87 User error: User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 3.43/0.87
% 3.43/0.87 % (3432979)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1880426417:i=85:gtgl=4:rtra=on:gtg=exists_sym_2998 on theBenchmark for (2998ds/85Mi)
% 3.43/0.87 % (3432980)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3610737099:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2998 on theBenchmark for (2998ds/2Mi)
% 5.07/1.04 % Exception at run slice level% Exception at run slice level
% 5.07/1.04
% 5.07/1.04 User error: User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04
% 5.07/1.04 % (3432982)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1387192716:i=181:rtra=on:ss=axioms:ev=cautious_2998 on theBenchmark for (2998ds/181Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.07/1.04 % (3432989)lrs+10_1_thi=all:si=on:fd=off:random_seed=4054008064:i=53:rtra=on:gtg=all_2998 on theBenchmark for (2998ds/53Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04 % (3432987)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3635057360:i=4:ep=RST:ins=2:rtra=on_2998 on theBenchmark for (2998ds/4Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.07/1.04 % (3432990)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2301600882:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2998 on theBenchmark for (2998ds/8Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04 % (3432988)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4027958594:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2998 on theBenchmark for (2998ds/66Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.07/1.04 % (3432994)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=332258631:i=2:doe=on:canc=force:asg=cautious:rtra=on_2997 on theBenchmark for (2997ds/2Mi)
% 5.07/1.04 % (3432993)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=224746590:st=3:i=2:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/2Mi)
% 5.07/1.04 % Exception at run slice level% Exception at run slice level
% 5.07/1.04
% 5.07/1.04 User error: User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04
% 5.07/1.04 % (3432996)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2115463615:i=127:doe=on:rtra=on_2997 on theBenchmark for (2997ds/127Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.07/1.04 % (3432998)dis+10_1_si=on:random_seed=4040884860:i=10:ep=R:rtra=on_2997 on theBenchmark for (2997ds/10Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04 % (3433000)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4259555234:i=26:canc=cautious:av=off:rtra=on_2997 on theBenchmark for (2997ds/26Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.07/1.04 % (3433002)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1345530441:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2997 on theBenchmark for (2997ds/35Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04 % (3433004)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3487115582:i=2:fsr=off:rtra=on:inst=on_2997 on theBenchmark for (2997ds/2Mi)
% 5.07/1.04 % Exception at run slice level
% 5.07/1.04 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.07/1.04 % (3433007)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1681813740:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2997 on theBenchmark for (2997ds/8Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433008)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=542915694:i=370:ep=RS:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/370Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433010)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1639790899:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2996 on theBenchmark for (2996ds/13Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433012)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1531378867:i=226:rtra=on:gtg=position:ss=axioms_2996 on theBenchmark for (2996ds/226Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433014)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=130404465:i=10:rtra=on_2996 on theBenchmark for (2996ds/10Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433016)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1523602095:i=71:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/71Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433022)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4100715742:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2996 on theBenchmark for (2996ds/130Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433018)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=2555468877:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2996 on theBenchmark for (2996ds/75Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433021)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=1821700621:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/294Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433024)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3132280252:i=131:rtra=on_2995 on theBenchmark for (2995ds/131Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 5.92/1.20 % (3433026)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=314819131:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2995 on theBenchmark for (2995ds/40Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433028)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=472720088:i=307:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/307Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 5.92/1.20 % (3433034)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=4014444732:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2995 on theBenchmark for (2995ds/259Mi)
% 5.92/1.20 % Exception at run slice level
% 5.92/1.20 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % (3433036)dis+10_1_si=on:random_seed=2524785446:s2a=on:i=1000:rtra=on:gtg=exists_all_2995 on theBenchmark for (2995ds/1000Mi)
% 6.54/1.36 % (3433030)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=253709364:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/598Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % (3433033)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3319300875:i=131:canc=cautious:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/131Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433038)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1985105566:i=383:fsr=off:rtra=on:ev=force_2994 on theBenchmark for (2994ds/383Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433040)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3278365810:i=141:doe=on:rtra=on_2994 on theBenchmark for (2994ds/141Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % (3433042)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2245523100:i=65:nm=16:rtra=on_2994 on theBenchmark for (2994ds/65Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433047)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1524903247:s2a=on:i=128:s2at=5:ins=3:rtra=on_2994 on theBenchmark for (2994ds/128Mi)
% 6.54/1.36 % (3433050)dis+1010_1_to=kbo:si=on:random_seed=2454771068:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/175Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: % Exception at run slice levelImmediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433048)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=736059322:i=39:ins=3:rtra=on_2994 on theBenchmark for (2994ds/39Mi)
% 6.54/1.36 % (3433046)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3812144697:i=121:nm=16:rtra=on_2994 on theBenchmark for (2994ds/121Mi)
% 6.54/1.36 % Exception at run slice level% Exception at run slice level
% 6.54/1.36 User error:
% 6.54/1.36 Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433052)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3783913965:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/329Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433054)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=625533666:s2a=on:i=483:doe=on:nm=32:rtra=on_2993 on theBenchmark for (2993ds/483Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433061)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=280336852:i=349:rtra=on_2993 on theBenchmark for (2993ds/349Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433056)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3847371160:thitd=on:i=215:nm=0:rtra=on:ev=force_2993 on theBenchmark for (2993ds/215Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433064)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2659878999:i=281:gtgl=2:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/281Mi)
% 6.54/1.36 % (3433062)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=961211772:st=2:i=295:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/295Mi)
% 6.54/1.36 % Exception at run slice level% Exception at run slice level
% 6.54/1.36
% 6.54/1.36 User error: User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36
% 6.54/1.36 % (3433063)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2734939850:i=328:kws=inv_frequency:nm=20:rtra=on_2993 on theBenchmark for (2993ds/328Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % (3433066)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=956204049:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/484Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 6.54/1.36 % (3433068)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2363256202:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2992 on theBenchmark for (2992ds/321Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433074)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3766367183:i=471:thf=on:kws=precedence:rtra=on_2992 on theBenchmark for (2992ds/471Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433070)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3532580425:i=416:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/416Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433075)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1151279144:avsq=on:i=276:avsqr=1,2:rtra=on_2992 on theBenchmark for (2992ds/276Mi)
% 6.54/1.36 % (3433077)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3296658974:i=375:kws=inv_arity_squared:rtra=on_2992 on theBenchmark for (2992ds/375Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433080)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=485844804:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2992 on theBenchmark for (2992ds/513Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433078)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1054497085:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/387Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 6.54/1.36 % (3433075)First to succeed.
% 6.54/1.36 % (3433075)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3432955"
% 6.54/1.36 % (3433082)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3003312376:i=334:rtra=on_2991 on theBenchmark for (2991ds/334Mi)
% 6.54/1.36 % Exception at run slice level
% 6.54/1.36 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433084)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1618890085:i=359:rtra=on:gtg=exists_top:ss=axioms_2991 on theBenchmark for (2991ds/359Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433086)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2453399554:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2991 on theBenchmark for (2991ds/341Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433092)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2579777720:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2991 on theBenchmark for (2991ds/235Mi)
% 7.62/1.46 % (3433090)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1182537487:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/261Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 % Exception at run slice levelUser error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433093)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3028790808:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2991 on theBenchmark for (2991ds/273Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 7.62/1.46 % (3433097)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2366747398:i=4428:doe=on:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/4428Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433095)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1104827581:i=146:doe=on:rtra=on_2990 on theBenchmark for (2990ds/146Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 7.62/1.46 % (3433099)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1205572321:avsq=on:i=276:avsqr=1,2:rtra=on_2990 on theBenchmark for (2990ds/276Mi)
% 7.62/1.46 % (3433103)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2112636219:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2990 on theBenchmark for (2990ds/655Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 7.62/1.46 % (3433102)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=706916202:i=1052:rtra=on_2990 on theBenchmark for (2990ds/1052Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal (iG5 = lG3) have different types/not well-typed!
% 7.62/1.46 % (3433105)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=235379670:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2990 on theBenchmark for (2990ds/1054Mi)
% 7.62/1.46 % Exception at run slice level
% 7.62/1.46 User error: Immediate (shared) subterms of term/literal lG3 = iG5 have different types/not well-typed!
% 7.62/1.46 % (3433099)Also succeeded, but the first one will report.
% 7.62/1.46 % (3433075)Refutation found. Thanks to Tanya!
% 7.62/1.46 % SZS status Theorem for theBenchmark
% 7.62/1.46 % SZS output start Proof for theBenchmark
% 7.62/1.46 tff(type_def_5, type, array_int_int: $tType).
% 7.62/1.46 tff(func_def_0, type, select_int_int: (array_int_int * $int) > $int).
% 7.62/1.46 tff(func_def_1, type, store_int_int: (array_int_int * $int * $int) > array_int_int).
% 7.62/1.46 tff(func_def_2, type, a: array_int_int).
% 7.62/1.46 tff(func_def_3, type, i: $int).
% 7.62/1.46 tff(func_def_4, type, max: $int).
% 7.62/1.46 tff(func_def_5, type, n: $int).
% 7.62/1.46 tff(func_def_7, type, max1: $int).
% 7.62/1.46 tff(func_def_8, type, i2: $int).
% 7.62/1.46 tff(func_def_14, type, sK3: (array_int_int * array_int_int) > $int).
% 7.62/1.46 tff(func_def_15, type, sK4: $int).
% 7.62/1.46 tff(func_def_17, type, '$inst6': $int).
% 7.62/1.46 tff(func_def_19, type, '$inst7': $int).
% 7.62/1.46 tff(pred_def_6, type, ':=': !>[X0: $tType]:((X0 * X0) > $o)).
% 7.62/1.46 tff(f5,axiom,(
% 7.62/1.46 ! [X0 : $int] : (($less(X0,i) & $greatereq(X0,0)) => $greatereq(max,select_int_int(a,X0)))),
% 7.62/1.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',voogie_precondition_5)).
% 7.62/1.46 tff(f6,conjecture,(
% 7.62/1.46 $let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (! [X0 : $int] : (($greatereq(X0,0) & $less(X0,i2)) => $greatereq(max1,select_int_int(a,X0))) | bad0)))),
% 7.62/1.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',voogie_conjecture)).
% 7.62/1.46 tff(f7,negated_conjecture,(
% 7.62/1.46 ~$let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (! [X0 : $int] : (($greatereq(X0,0) & $less(X0,i2)) => $greatereq(max1,select_int_int(a,X0))) | bad0)))),
% 7.62/1.46 inference(negated_conjecture,[status(cth)],[f6])).
% 7.62/1.46 tff(f8,plain,(
% 7.62/1.46 ! [X0 : $int] : (($less(X0,i) & ~$less(X0,0)) => ~$less(max,select_int_int(a,X0)))),
% 7.62/1.46 inference(theory_normalization,[],[f5])).
% 7.62/1.46 tff(f10,plain,(
% 7.62/1.46 ~$let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (bad0 | ! [X0 : $int] : (($less(X0,i2) & ~$less(X0,0)) => ~$less(max1,select_int_int(a,X0))))))),
% 7.62/1.46 inference(theory_normalization,[],[f7])).
% 7.62/1.46 tff(f18,plain,(
% 7.62/1.46 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | X0 = X1 | $less(X0,X1)) )),
% 7.62/1.46 introduced(definition,[],[tha_order_totality])).
% 7.62/1.46 tff(f26,plain,(
% 7.62/1.46 ~$let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (bad0 | ! [X0 : $int] : (($less(X0,i2) & ~$less(X0,0)) => ~$less(max1,select_int_int(a,X0))))))),
% 7.62/1.46 inference(rectify,[],[f10])).
% 7.62/1.46 tff(f27,plain,(
% 7.62/1.46 ! [X0 : $int] : (~$less(max,select_int_int(a,X0)) | (~$less(X0,i) | $less(X0,0)))),
% 7.62/1.46 inference(ennf_transformation,[],[f8])).
% 7.62/1.46 tff(f28,plain,(
% 7.62/1.46 ! [X0 : $int] : (~$less(X0,i) | ~$less(max,select_int_int(a,X0)) | $less(X0,0))),
% 7.62/1.46 inference(flattening,[],[f27])).
% 7.62/1.46 tff(f32,plain,(
% 7.62/1.46 $let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (~bad0 & ? [X0 : $int] : ($less(max1,select_int_int(a,X0)) & ($less(X0,i2) & ~$less(X0,0))))))),
% 7.62/1.46 inference(ennf_transformation,[],[f26])).
% 7.62/1.46 tff(f33,plain,(
% 7.62/1.46 $let(n: $int, n := $ite(~$less(i,n), ($true,bad), ($let(max1: $int, max1 := $ite($less(max,select_int_int(a,i)), (select_int_int(a,i),max), ($let(i2: $int, i2 := $sum(i,1), (? [X0 : $int] : ($less(max1,select_int_int(a,X0)) & $less(X0,i2) & ~$less(X0,0)) & ~bad0)))),
% 7.62/1.46 inference(flattening,[],[f32])).
% 7.62/1.46 tff(f38,plain,(
% 7.62/1.46 ( ! [X0 : $int] : (~$less(X0,i) | ~$less(max,select_int_int(a,X0)) | $less(X0,0)) )),
% 7.62/1.46 inference(cnf_transformation,[],[f28])).
% 7.62/1.46 tff(f39,plain,(
% 7.62/1.46 ~$less(max,select_int_int(a,i)) | $less(select_int_int(a,i),select_int_int(a,sK4))),
% 7.62/1.46 inference(cnf_transformation,[],[f33])).
% 7.62/1.46 tff(f40,plain,(
% 7.62/1.46 $less(max,select_int_int(a,sK4)) | $less(max,select_int_int(a,i))),
% 7.62/1.46 inference(cnf_transformation,[],[f33])).
% 7.62/1.46 tff(f41,plain,(
% 7.62/1.46 ~$less(sK4,0)),
% 7.62/1.46 inference(cnf_transformation,[],[f33])).
% 7.62/1.46 tff(f42,plain,(
% 7.62/1.46 $less(sK4,$sum(i,1))),
% 7.62/1.46 inference(cnf_transformation,[],[f33])).
% 7.62/1.46 tff(f51,definition,(
% 7.62/1.46 spl5_2 <=> $less(sK4,0)),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 7.62/1.46 tff(f53,plain,(
% 7.62/1.46 ~$less(sK4,0) | spl5_2),
% 7.62/1.46 inference(avatar_component_clause,[],[f51])).
% 7.62/1.46 tff(f54,plain,(
% 7.62/1.46 ~spl5_2),
% 7.62/1.46 inference(avatar_split_clause,[],[f41,f51])).
% 7.62/1.46 tff(f61,definition,(
% 7.62/1.46 spl5_4 <=> $less(sK4,$sum(i,1))),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 7.62/1.46 tff(f64,plain,(
% 7.62/1.46 spl5_4),
% 7.62/1.46 inference(avatar_split_clause,[],[f42,f61])).
% 7.62/1.46 tff(f66,definition,(
% 7.62/1.46 spl5_5 <=> $less(max,select_int_int(a,sK4))),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 7.62/1.46 tff(f68,plain,(
% 7.62/1.46 $less(max,select_int_int(a,sK4)) | ~spl5_5),
% 7.62/1.46 inference(avatar_component_clause,[],[f66])).
% 7.62/1.46 tff(f70,definition,(
% 7.62/1.46 spl5_6 <=> $less(max,select_int_int(a,i))),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 7.62/1.46 tff(f73,plain,(
% 7.62/1.46 spl5_5 | spl5_6),
% 7.62/1.46 inference(avatar_split_clause,[],[f40,f70,f66])).
% 7.62/1.46 tff(f75,definition,(
% 7.62/1.46 spl5_7 <=> $less(select_int_int(a,i),select_int_int(a,sK4))),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 7.62/1.46 tff(f78,plain,(
% 7.62/1.46 spl5_7 | ~spl5_6),
% 7.62/1.46 inference(avatar_split_clause,[],[f39,f70,f75])).
% 7.62/1.46 tff(f104,plain,(
% 7.62/1.46 ( ! [X0 : $int] : (~$less(max,select_int_int(a,X0)) | i = X0 | $less(X0,0) | $less(i,X0)) )),
% 7.62/1.46 inference(resolution,[],[f38,f18])).
% 7.62/1.46 tff(f193,plain,(
% 7.62/1.46 $less(sK4,0) | i = sK4 | $less(i,sK4) | ~spl5_5),
% 7.62/1.46 inference(resolution,[],[f104,f68])).
% 7.62/1.46 tff(f196,plain,(
% 7.62/1.46 i = sK4 | $less(i,sK4) | (spl5_2 | ~spl5_5)),
% 7.62/1.46 inference(forward_subsumption_resolution,[],[f193,f53])).
% 7.62/1.46 tff(f198,definition,(
% 7.62/1.46 spl5_22 <=> i = sK4),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition])).
% 7.62/1.46 tff(f202,definition,(
% 7.62/1.46 spl5_23 <=> $less(i,sK4)),
% 7.62/1.46 introduced(definition,[new_symbols(definition,[spl5_23])],[avatar_definition])).
% 7.62/1.46 tff(f205,plain,(
% 7.62/1.46 spl5_22 | spl5_23 | spl5_2 | ~spl5_5),
% 7.62/1.46 inference(avatar_split_clause,[],[f196,f66,f51,f202,f198])).
% 7.62/1.46 tff(f206,plain,(
% 7.62/1.46 $false),
% 7.62/1.46 inference(avatar_smt_refutation,[],[f205,f78,f73,f64,f54])).
% 7.62/1.46 % SZS output end Proof for theBenchmark
% 7.62/1.46 % (3433075)------------------------------
% 7.62/1.46 % (3433075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.62/1.46 % (3433075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.62/1.46 % (3433075)CaDiCaL version: 2.1.3
% 7.62/1.46 % (3433075)Termination reason: Refutation
% 7.62/1.46 % (3433075)Time elapsed: 0.046 s
% 7.62/1.46 % (3433075)Peak memory usage: 134 MB
% 7.62/1.46 % (3433075)Instructions burned: 35 (million)
% 7.62/1.46 % (3433075)------------------------------
% 7.62/1.46 % (3433075)------------------------------
% 7.62/1.46 % (3432955)Success in time 1.062 s
% 7.62/1.46 % Vampire exiting
%------------------------------------------------------------------------------