%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP131^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 : n015.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:29 AM UTC 2026
% Result : ContradictoryAxioms 1.97s 0.60s
% Output : Refutation 1.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP131^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.19 % Computer : n015.cluster.edu
% 0.12/0.19 % Model : x86_64 x86_64
% 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.19 % Memory : 8046.5625MB
% 0.12/0.19 % OS : Linux 6.8.0-71-generic
% 0.12/0.20 % CPULimit : 300
% 0.12/0.20 % WCLimit : 300
% 0.12/0.20 % DateTime : Tue Sep 29 20:01:34 UTC 2026
% 0.12/0.20 % CPUTime :
% 0.12/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.25 Running higher-order theorem proving
% 0.12/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.80/0.48 % (4039960)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.80/0.48 % (4039973)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.80/0.48 % (4039973)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.80/0.48 % (4039973)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=781823438:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.80/0.48 % (4039967)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2899028656:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.80/0.48 % (4039968)lrs+10_16_si=on:nwc=1.5:random_seed=2579010789:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.80/0.48 % (4039971)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1120458830:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.80/0.48 % (4039970)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=2291474355: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.80/0.48 % (4039969)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=650752314:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.80/0.48 % (4039969)Instruction limit reached!
% 0.80/0.48 % (4039969)------------------------------
% 0.80/0.48 % (4039969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.48 % (4039969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.48 % (4039969)CaDiCaL version: 2.1.3
% 0.80/0.48 % (4039969)Termination reason: Instruction limit
% 0.80/0.48 % (4039969)Termination phase: shuffling
% 0.80/0.48 % (4039969)Time elapsed: 0.003 s
% 0.80/0.48 % (4039969)Peak memory usage: 10 MB
% 0.80/0.48 % (4039969)Instructions burned: 3 (million)
% 0.80/0.48 % (4039972)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=662564988:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.80/0.48 % (4039968)Instruction limit reached!
% 0.80/0.48 % (4039968)------------------------------
% 0.80/0.48 % (4039968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.48 % (4039968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.48 % (4039968)CaDiCaL version: 2.1.3
% 0.80/0.48 % (4039968)Termination reason: Instruction limit
% 0.80/0.48 % (4039968)Termination phase: Preprocessing 1
% 0.80/0.48 % (4039968)Time elapsed: 0.015 s
% 0.80/0.48 % (4039968)Peak memory usage: 10 MB
% 0.80/0.48 % (4039968)Instructions burned: 19 (million)
% 0.80/0.48 % (4039971)Instruction limit reached!
% 0.80/0.48 % (4039971)------------------------------
% 0.80/0.48 % (4039971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.48 % (4039971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.48 % (4039971)CaDiCaL version: 2.1.3
% 0.80/0.48 % (4039971)Termination reason: Instruction limit
% 0.80/0.48 % (4039971)Termination phase: Property scanning
% 0.80/0.48 % (4039971)Time elapsed: 0.021 s
% 0.80/0.48 % (4039971)Peak memory usage: 11 MB
% 0.80/0.48 % (4039971)Instructions burned: 25 (million)
% 0.80/0.48 % (4039982)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2885869830:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.80/0.48 % (4039982)Instruction limit reached!
% 0.80/0.48 % (4039982)------------------------------
% 0.80/0.48 % (4039982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.48 % (4039982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.48 % (4039982)CaDiCaL version: 2.1.3
% 0.80/0.48 % (4039982)Termination reason: Instruction limit
% 0.80/0.48 % (4039982)Termination phase: shuffling
% 0.80/0.48 % (4039982)Time elapsed: 0.002 s
% 0.80/0.48 % (4039982)Peak memory usage: 10 MB
% 0.80/0.48 % (4039982)Instructions burned: 2 (million)
% 0.80/0.48 % (4039984)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1759822622:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.51/0.52 % (4039985)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.51/0.52 % (4039984)Instruction limit reached!
% 1.51/0.52 % (4039984)------------------------------
% 1.51/0.52 % (4039984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039984)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039984)Termination reason: Instruction limit
% 1.51/0.52 % (4039984)Termination phase: shuffling
% 1.51/0.52 % (4039984)Time elapsed: 0.005 s
% 1.51/0.52 % (4039984)Peak memory usage: 10 MB
% 1.51/0.52 % (4039984)Instructions burned: 5 (million)
% 1.51/0.52 % (4039985)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4239143949:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.51/0.52 % (4039973)Instruction limit reached!
% 1.51/0.52 % (4039973)------------------------------
% 1.51/0.52 % (4039973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039973)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039973)Termination reason: Instruction limit
% 1.51/0.52 % (4039973)Termination phase: Saturation
% 1.51/0.52 % (4039973)Time elapsed: 0.068 s
% 1.51/0.52 % (4039973)Peak memory usage: 13 MB
% 1.51/0.52 % (4039973)Instructions burned: 158 (million)
% 1.51/0.52 % (4039985)Instruction limit reached!
% 1.51/0.52 % (4039985)------------------------------
% 1.51/0.52 % (4039985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039985)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039985)Termination reason: Instruction limit
% 1.51/0.52 % (4039985)Termination phase: shuffling
% 1.51/0.52 % (4039985)Time elapsed: 0.006 s
% 1.51/0.52 % (4039985)Peak memory usage: 10 MB
% 1.51/0.52 % (4039985)Instructions burned: 7 (million)
% 1.51/0.52 % (4039967)Instruction limit reached!
% 1.51/0.52 % (4039967)------------------------------
% 1.51/0.52 % (4039967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039967)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039967)Termination reason: Instruction limit
% 1.51/0.52 % (4039967)Termination phase: Saturation
% 1.51/0.52 % (4039967)Time elapsed: 0.070 s
% 1.51/0.52 % (4039967)Peak memory usage: 12 MB
% 1.51/0.52 % (4039967)Instructions burned: 88 (million)
% 1.51/0.52 % (4039991)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.51/0.52 % (4039991)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.51/0.52 % (4039988)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2784596005:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.51/0.52 % (4039991)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3050156405:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.51/0.52 % (4039988)Instruction limit reached!
% 1.51/0.52 % (4039988)------------------------------
% 1.51/0.52 % (4039988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039988)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039988)Termination reason: Instruction limit
% 1.51/0.52 % (4039988)Termination phase: Property scanning
% 1.51/0.52 % (4039988)Time elapsed: 0.011 s
% 1.51/0.52 % (4039988)Peak memory usage: 10 MB
% 1.51/0.52 % (4039988)Instructions burned: 12 (million)
% 1.51/0.52 % (4039972)Instruction limit reached!
% 1.51/0.52 % (4039972)------------------------------
% 1.51/0.52 % (4039972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.52 % (4039972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.52 % (4039972)CaDiCaL version: 2.1.3
% 1.51/0.52 % (4039972)Termination reason: Instruction limit
% 1.51/0.56 % (4039972)Termination phase: Saturation
% 1.51/0.56 % (4039972)Time elapsed: 0.077 s
% 1.51/0.56 % (4039972)Peak memory usage: 13 MB
% 1.51/0.56 % (4039972)Instructions burned: 75 (million)
% 1.51/0.56 % (4039991)Instruction limit reached!
% 1.51/0.56 % (4039991)------------------------------
% 1.51/0.56 % (4039991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.56 % (4039991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.56 % (4039991)CaDiCaL version: 2.1.3
% 1.51/0.56 % (4039991)Termination reason: Instruction limit
% 1.51/0.56 % (4039991)Termination phase: Property scanning
% 1.51/0.56 % (4039991)Time elapsed: 0.012 s
% 1.51/0.56 % (4039991)Peak memory usage: 10 MB
% 1.51/0.56 % (4039991)Instructions burned: 29 (million)
% 1.51/0.56 % (4039992)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=1708214084:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.51/0.56 % (4039993)lrs+10_1_si=on:cs=on:random_seed=935325601:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.51/0.56 % (4039995)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.51/0.56 % (4039993)Instruction limit reached!
% 1.51/0.56 % (4039993)------------------------------
% 1.51/0.56 % (4039993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.56 % (4039993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.56 % (4039993)CaDiCaL version: 2.1.3
% 1.51/0.56 % (4039993)Termination reason: Instruction limit
% 1.51/0.56 % (4039993)Termination phase: shuffling
% 1.51/0.56 % (4039993)Time elapsed: 0.007 s
% 1.51/0.56 % (4039993)Peak memory usage: 10 MB
% 1.51/0.56 % (4039993)Instructions burned: 8 (million)
% 1.51/0.56 % (4039995)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=538220121:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.51/0.56 % (4039995)Instruction limit reached!
% 1.51/0.56 % (4039995)------------------------------
% 1.51/0.56 % (4039995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.56 % (4039995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.56 % (4039995)CaDiCaL version: 2.1.3
% 1.51/0.56 % (4039995)Termination reason: Instruction limit
% 1.51/0.56 % (4039995)Termination phase: shuffling
% 1.51/0.56 % (4039995)Time elapsed: 0.002 s
% 1.51/0.56 % (4039995)Peak memory usage: 10 MB
% 1.51/0.56 % (4039995)Instructions burned: 2 (million)
% 1.51/0.56 % (4040000)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=333577671:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.51/0.56 % (4040000)Refutation not found, incomplete strategy
% 1.51/0.56 % (4040000)------------------------------
% 1.51/0.56 % (4040000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.56 % (4040000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.56 % (4040000)CaDiCaL version: 2.1.3
% 1.51/0.56 % (4040000)Termination reason: Refutation not found, incomplete strategy
% 1.51/0.56 % (4040000)Time elapsed: 0.009 s
% 1.51/0.56 % (4040000)Peak memory usage: 11 MB
% 1.51/0.56 % (4040000)Instructions burned: 22 (million)
% 1.51/0.56 % (4040000)------------------------------
% 1.51/0.56 % (4040000)------------------------------
% 1.51/0.56 % (4039998)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3948103571:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.51/0.56 % (4040002)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3525886522:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.51/0.56 % (4040004)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1569247627:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.51/0.56 % (4039998)Refutation not found, incomplete strategy
% 1.51/0.56 % (4039998)------------------------------
% 1.51/0.56 % (4039998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.56 % (4039998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.56 % (4040009)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1359293757:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.97/0.60 % (4040006)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=337974390:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.97/0.60 % (4039998)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4039998)Termination reason: Refutation not found, incomplete strategy
% 1.97/0.60 % (4039998)Time elapsed: 0.017 s
% 1.97/0.60 % (4039998)Peak memory usage: 11 MB
% 1.97/0.60 % (4039998)Instructions burned: 19 (million)
% 1.97/0.60 % (4039998)------------------------------
% 1.97/0.60 % (4039998)------------------------------
% 1.97/0.60 % (4040002)Refutation not found, incomplete strategy
% 1.97/0.60 % (4040002)------------------------------
% 1.97/0.60 % (4040002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040002)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040002)Termination reason: Refutation not found, incomplete strategy
% 1.97/0.60 % (4040002)Time elapsed: 0.018 s
% 1.97/0.60 % (4040002)Peak memory usage: 12 MB
% 1.97/0.60 % (4040002)Instructions burned: 20 (million)
% 1.97/0.60 % (4040002)------------------------------
% 1.97/0.60 % (4040002)------------------------------
% 1.97/0.60 % (4040009)Instruction limit reached!
% 1.97/0.60 % (4040009)------------------------------
% 1.97/0.60 % (4040009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040009)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040009)Termination reason: Instruction limit
% 1.97/0.60 % (4040009)Termination phase: Property scanning
% 1.97/0.60 % (4040009)Time elapsed: 0.007 s
% 1.97/0.60 % (4040009)Peak memory usage: 10 MB
% 1.97/0.60 % (4040009)Instructions burned: 18 (million)
% 1.97/0.60 % (4040004)Instruction limit reached!
% 1.97/0.60 % (4040004)------------------------------
% 1.97/0.60 % (4040004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040004)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040004)Termination reason: Instruction limit
% 1.97/0.60 % (4040004)Termination phase: Property scanning
% 1.97/0.60 % (4040004)Time elapsed: 0.012 s
% 1.97/0.60 % (4040004)Peak memory usage: 10 MB
% 1.97/0.60 % (4040004)Instructions burned: 14 (million)
% 1.97/0.60 % (4040006)Refutation not found, incomplete strategy
% 1.97/0.60 % (4040006)------------------------------
% 1.97/0.60 % (4040006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040006)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040006)Termination reason: Refutation not found, incomplete strategy
% 1.97/0.60 % (4040006)Time elapsed: 0.020 s
% 1.97/0.60 % (4040006)Peak memory usage: 12 MB
% 1.97/0.60 % (4040006)Instructions burned: 24 (million)
% 1.97/0.60 % (4040006)------------------------------
% 1.97/0.60 % (4040006)------------------------------
% 1.97/0.60 % (4040016)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=476193190:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.97/0.60 % (4039992)Instruction limit reached!
% 1.97/0.60 % (4039992)------------------------------
% 1.97/0.60 % (4039992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4039992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4039992)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4039992)Termination reason: Instruction limit
% 1.97/0.60 % (4039992)Termination phase: Saturation
% 1.97/0.60 % (4039992)Time elapsed: 0.072 s
% 1.97/0.60 % (4039992)Peak memory usage: 12 MB
% 1.97/0.60 % (4039992)Instructions burned: 90 (million)
% 1.97/0.60 % (4040014)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4064622159: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.97/0.60 % (4040016)Instruction limit reached!
% 1.97/0.60 % (4040016)------------------------------
% 1.97/0.60 % (4040016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040016)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040016)Termination reason: Instruction limit
% 1.97/0.60 % (4040016)Termination phase: Preprocessing 3
% 1.97/0.60 % (4040016)Time elapsed: 0.010 s
% 1.97/0.60 % (4040016)Peak memory usage: 11 MB
% 1.97/0.60 % (4040016)Instructions burned: 23 (million)
% 1.97/0.60 % (4040014)Instruction limit reached!
% 1.97/0.60 % (4040014)------------------------------
% 1.97/0.60 % (4040014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040014)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040014)Termination reason: Instruction limit
% 1.97/0.60 % (4040014)Termination phase: shuffling
% 1.97/0.60 % (4040014)Time elapsed: 0.003 s
% 1.97/0.60 % (4040014)Peak memory usage: 10 MB
% 1.97/0.60 % (4040014)Instructions burned: 3 (million)
% 1.97/0.60 % (4040015)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=313021580:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.97/0.60 % (4040017)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3717597300:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.97/0.60 % (4040018)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.97/0.60 % (4040018)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.97/0.60 % (4040020)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.97/0.60 % (4040018)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3618406673:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 1.97/0.60 % (4040022)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1165205779:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 1.97/0.60 % (4040020)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=2307301656:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 1.97/0.60 % (4040015)Instruction limit reached!
% 1.97/0.60 % (4040015)------------------------------
% 1.97/0.60 % (4040015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040015)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040015)Termination reason: Instruction limit
% 1.97/0.60 % (4040015)Termination phase: Property scanning
% 1.97/0.60 % (4040015)Time elapsed: 0.022 s
% 1.97/0.60 % (4040015)Peak memory usage: 10 MB
% 1.97/0.60 % (4040015)Instructions burned: 26 (million)
% 1.97/0.60 % (4040020)Instruction limit reached!
% 1.97/0.60 % (4040020)------------------------------
% 1.97/0.60 % (4040020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040020)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040020)Termination reason: Instruction limit
% 1.97/0.60 % (4040020)Termination phase: shuffling
% 1.97/0.60 % (4040020)Time elapsed: 0.007 s
% 1.97/0.60 % (4040020)Peak memory usage: 10 MB
% 1.97/0.60 % (4040020)Instructions burned: 8 (million)
% 1.97/0.60 % (4040018)Instruction limit reached!
% 1.97/0.60 % (4040018)------------------------------
% 1.97/0.60 % (4040018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040018)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040018)Termination reason: Instruction limit
% 1.97/0.60 % (4040018)Termination phase: shuffling
% 1.97/0.60 % (4040018)Time elapsed: 0.012 s
% 1.97/0.60 % (4040018)Peak memory usage: 10 MB
% 1.97/0.60 % (4040018)Instructions burned: 15 (million)
% 1.97/0.60 % (4040024)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2366526348:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 1.97/0.60 % (4040022)Instruction limit reached!
% 1.97/0.60 % (4040022)------------------------------
% 1.97/0.60 % (4040022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040022)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040022)Termination reason: Instruction limit
% 1.97/0.60 % (4040022)Termination phase: Property scanning
% 1.97/0.60 % (4040022)Time elapsed: 0.015 s
% 1.97/0.60 % (4040022)Peak memory usage: 10 MB
% 1.97/0.60 % (4040022)Instructions burned: 31 (million)
% 1.97/0.60 % (4040024)Instruction limit reached!
% 1.97/0.60 % (4040024)------------------------------
% 1.97/0.60 % (4040024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040024)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040024)Termination reason: Instruction limit
% 1.97/0.60 % (4040024)Termination phase: shuffling
% 1.97/0.60 % (4040024)Time elapsed: 0.007 s
% 1.97/0.60 % (4040024)Peak memory usage: 10 MB
% 1.97/0.60 % (4040024)Instructions burned: 8 (million)
% 1.97/0.60 % (4040033)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=733631723:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 1.97/0.60 % (4040017)Instruction limit reached!
% 1.97/0.60 % (4040017)------------------------------
% 1.97/0.60 % (4040017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4040017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4040017)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4040017)Termination reason: Instruction limit
% 1.97/0.60 % (4040017)Termination phase: Saturation
% 1.97/0.60 % (4040017)Time elapsed: 0.050 s
% 1.97/0.60 % (4040017)Peak memory usage: 12 MB
% 1.97/0.60 % (4040017)Instructions burned: 60 (million)
% 1.97/0.60 % (4040029)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2108979381:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 1.97/0.60 % (4040030)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3043169258:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 1.97/0.60 % (4040031)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2328950067:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 1.97/0.60 % (4039970) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4039960-4039970"...
% 1.97/0.60 % (4039970)...printing done.
% 1.97/0.60 % (4039970)Refutation found. Thanks to Tanya!
% 1.97/0.60 % SZS status ContradictoryAxioms for theBenchmark
% 1.97/0.60 % SZS output start Proof for theBenchmark
% 1.97/0.60 thf(type_def_5, type, nat: $tType).
% 1.97/0.60 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 1.97/0.60 thf(func_def_0, type, minus_minus_nat: (nat > nat > nat)).
% 1.97/0.60 thf(func_def_1, type, plus_plus_nat: (nat > nat > nat)).
% 1.97/0.60 thf(func_def_2, type, times_times_nat: (nat > nat > nat)).
% 1.97/0.60 thf(func_def_3, type, zero_zero_nat: nat).
% 1.97/0.60 thf(func_def_4, type, number1551313001itions: ((nat > nat) > nat > $o)).
% 1.97/0.60 thf(func_def_5, type, ord_less_nat: (nat > nat > $o)).
% 1.97/0.60 thf(func_def_6, type, ord_less_eq_nat: (nat > nat > $o)).
% 1.97/0.60 thf(func_def_7, type, i: nat).
% 1.97/0.60 thf(func_def_8, type, k: nat).
% 1.97/0.60 thf(func_def_9, type, n: nat).
% 1.97/0.60 thf(func_def_10, type, p: (nat > nat)).
% 1.97/0.60 thf(func_def_14, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.97/0.60 thf(func_def_15, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.97/0.60 thf(func_def_16, type, db2: !>[X0: $tType]:(X0)).
% 1.97/0.60 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 1.97/0.60 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 1.97/0.60 thf(func_def_19, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.97/0.60 thf(func_def_20, type, vOR: ($o > $o > $o)).
% 1.97/0.60 thf(func_def_21, type, vAND: ($o > $o > $o)).
% 1.97/0.60 thf(func_def_22, type, vNOT: ($o > $o)).
% 1.97/0.60 thf(func_def_23, type, sK0: ((nat > $o) > nat)).
% 1.97/0.60 thf(func_def_24, type, sK1: ((nat > $o) > nat)).
% 1.97/0.60 thf(func_def_25, type, sK2: (nat > nat > nat)).
% 1.97/0.60 thf(func_def_26, type, sK3: ((nat > nat) > nat)).
% 1.97/0.60 thf(func_def_27, type, sK4: ((nat > nat) > nat)).
% 1.97/0.60 thf(func_def_28, type, sK5: ((nat > $o) > nat)).
% 1.97/0.60 thf(func_def_29, type, sK6: (nat > (nat > $o) > nat > nat)).
% 1.97/0.60 thf(func_def_30, type, sK7: ((nat > $o) > nat > nat > nat)).
% 1.97/0.60 thf(func_def_31, type, sK8: (nat > (nat > $o) > nat)).
% 1.97/0.60 thf(func_def_32, type, sK9: ((nat > $o) > nat)).
% 1.97/0.60 thf(func_def_34, type, inv_plus_plus_nat_11: (nat > nat > nat)).
% 1.97/0.60 thf(func_def_35, type, inv_plus_plus_nat_12: (nat > nat > nat)).
% 1.97/0.60 thf(f3,axiom,(
% 1.97/0.60 (ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)),
% 1.97/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_upper__bound)).
% 1.97/0.60 thf(f4,axiom,(
% 1.97/0.60 (ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))),
% 1.97/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_lower__bound)).
% 1.97/0.60 thf(f163,axiom,(
% 1.97/0.60 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) => ~ ! [X2 : nat] : (X1 != ((plus_plus_nat @ X0 @ X2))))),
% 1.97/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_less__eqE)).
% 1.97/0.60 thf(f203,axiom,(
% 1.97/0.60 ! [X1 : nat,X0 : nat] : ~(ord_less_nat @ (plus_plus_nat @ X0 @ X1) @ X0)),
% 1.97/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_not__add__less1)).
% 1.97/0.60 thf(f255,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) => ~ ! [X2 : nat] : (((plus_plus_nat @ X1 @ X2)) != X0))),
% 1.97/0.60 inference(rectify,[],[f163])).
% 1.97/0.60 thf(f256,plain,(
% 1.97/0.60 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) => ~ ! [X2 : nat] : (((plus_plus_nat @ X1 @ X2)) != X0))),
% 1.97/0.60 inference(fool_elimination,[],[f255])).
% 1.97/0.60 thf(f257,plain,(
% 1.97/0.60 (ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))),
% 1.97/0.60 inference(rectify,[],[f4])).
% 1.97/0.60 thf(f258,plain,(
% 1.97/0.60 (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) = $true)),
% 1.97/0.60 inference(fool_elimination,[],[f257])).
% 1.97/0.60 thf(f438,plain,(
% 1.97/0.60 (ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)),
% 1.97/0.60 inference(rectify,[],[f3])).
% 1.97/0.60 thf(f439,plain,(
% 1.97/0.60 (((ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)) = $true)),
% 1.97/0.60 inference(fool_elimination,[],[f438])).
% 1.97/0.60 thf(f489,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : ~(ord_less_nat @ (plus_plus_nat @ X1 @ X0) @ X1)),
% 1.97/0.60 inference(rectify,[],[f203])).
% 1.97/0.60 thf(f490,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : ~ ($true = ((ord_less_nat @ (plus_plus_nat @ X1 @ X0) @ X1)))),
% 1.97/0.60 inference(fool_elimination,[],[f489])).
% 1.97/0.60 thf(f547,plain,(
% 1.97/0.60 ! [X1 : nat,X0 : nat] : ($true != ((ord_less_nat @ (plus_plus_nat @ X1 @ X0) @ X1)))),
% 1.97/0.60 inference(flattening,[],[f490])).
% 1.97/0.60 thf(f594,plain,(
% 1.97/0.60 ! [X1 : nat,X0 : nat] : (? [X2 : nat] : (((plus_plus_nat @ X1 @ X2)) = X0) | (((ord_less_eq_nat @ X1 @ X0)) != $true))),
% 1.97/0.60 inference(ennf_transformation,[],[f256])).
% 1.97/0.60 thf(f725,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : (? [X2 : nat] : (((plus_plus_nat @ X0 @ X2)) = X1) | (((ord_less_eq_nat @ X0 @ X1)) != $true))),
% 1.97/0.60 inference(rectify,[],[f594])).
% 1.97/0.60 thf(f726,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : ((((plus_plus_nat @ X0 @ (sK2 @ X1 @ X0))) = X1) | (((ord_less_eq_nat @ X0 @ X1)) != $true))),
% 1.97/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X0)],[f725])).
% 1.97/0.60 thf(f841,plain,(
% 1.97/0.60 ! [X0 : nat,X1 : nat] : (((ord_less_nat @ (plus_plus_nat @ X0 @ X1) @ X0)) != $true)),
% 1.97/0.60 inference(rectify,[],[f547])).
% 1.97/0.60 thf(f932,plain,(
% 1.97/0.60 ( ! [X0 : nat,X1 : nat] : ((((plus_plus_nat @ X0 @ (sK2 @ X1 @ X0))) = X1) | (((ord_less_eq_nat @ X0 @ X1)) != $true)) )),
% 1.97/0.60 inference(cnf_transformation,[],[f726])).
% 1.97/0.60 thf(f1030,plain,(
% 1.97/0.60 (((ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)) = $true)),
% 1.97/0.60 inference(cnf_transformation,[],[f439])).
% 1.97/0.60 thf(f1045,plain,(
% 1.97/0.60 (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) = $true)),
% 1.97/0.60 inference(cnf_transformation,[],[f258])).
% 1.97/0.60 thf(f1114,plain,(
% 1.97/0.60 ( ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ (plus_plus_nat @ X0 @ X1) @ X0)) != $true)) )),
% 1.97/0.60 inference(cnf_transformation,[],[f841])).
% 1.97/0.60 thf(f1283,definition,(
% 1.97/0.60 spl10_6 <=> (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) = $true)),
% 1.97/0.60 introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition])).
% 1.97/0.60 thf(f1285,plain,(
% 1.97/0.60 (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) = $true) | ~spl10_6),
% 1.97/0.60 inference(avatar_component_clause,[],[f1283])).
% 1.97/0.60 thf(f1286,plain,(
% 1.97/0.60 spl10_6),
% 1.97/0.60 inference(avatar_split_clause,[],[f1045,f1283])).
% 1.97/0.60 thf(f1318,definition,(
% 1.97/0.60 spl10_13 <=> (((ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)) = $true)),
% 1.97/0.60 introduced(definition,[new_symbols(definition,[spl10_13])],[avatar_definition])).
% 1.97/0.60 thf(f1320,plain,(
% 1.97/0.60 (((ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)) @ n)) = $true) | ~spl10_13),
% 1.97/0.60 inference(avatar_component_clause,[],[f1318])).
% 1.97/0.60 thf(f1321,plain,(
% 1.97/0.60 spl10_13),
% 1.97/0.60 inference(avatar_split_clause,[],[f1030,f1318])).
% 1.97/0.60 thf(f1617,plain,(
% 1.97/0.60 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_nat @ X0 @ X1)) != $true)) )),
% 1.97/0.60 inference(superposition,[],[f1114,f932])).
% 1.97/0.60 thf(f3463,plain,(
% 1.97/0.60 (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) != $true) | ($true != $true) | ~spl10_13),
% 1.97/0.60 inference(superposition,[],[f1617,f1320])).
% 1.97/0.60 thf(f3464,plain,(
% 1.97/0.60 (((ord_less_nat @ n @ (plus_plus_nat @ (times_times_nat @ (p @ i) @ i) @ (times_times_nat @ (p @ k) @ k)))) != $true) | ~spl10_13),
% 1.97/0.60 inference(trivial_inequality_removal,[],[f3463])).
% 1.97/0.60 thf(f3466,plain,(
% 1.97/0.60 $false | (~spl10_6 | ~spl10_13)),
% 1.97/0.60 inference(forward_subsumption_resolution,[],[f3464,f1285])).
% 1.97/0.60 thf(f3467,plain,(
% 1.97/0.60 ~spl10_6 | ~spl10_13),
% 1.97/0.60 inference(avatar_contradiction_clause,[],[f3466])).
% 1.97/0.60 cnf(s7, plain, spl10_6, inference(sat_conversion,[],[f1286])).
% 1.97/0.60 cnf(s19, plain, spl10_13, inference(sat_conversion,[],[f1321])).
% 1.97/0.60 cnf(s87, plain, ~spl10_6 | ~spl10_13, inference(sat_conversion,[],[f3467])).
% 1.97/0.60 cnf(s92, plain, ~spl10_6, inference(rat,[],[s87,s19])).
% 1.97/0.60 cnf(s97, plain, $false, inference(rat,[],[s7,s92])).
% 1.97/0.60 thf(f3482,plain,(
% 1.97/0.60 $false),
% 1.97/0.60 inference(avatar_sat_refutation,[],[s97])).
% 1.97/0.60 % SZS output end Proof for theBenchmark
% 1.97/0.60 % (4039970)------------------------------
% 1.97/0.60 % (4039970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.60 % (4039970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.60 % (4039970)CaDiCaL version: 2.1.3
% 1.97/0.60 % (4039970)Termination reason: Refutation
% 1.97/0.60 % (4039970)Time elapsed: 0.242 s
% 1.97/0.60 % (4039970)Peak memory usage: 14 MB
% 1.97/0.60 % (4039970)Instructions burned: 270 (million)
% 1.97/0.60 % (4039960)Success in time 0.297 s
% 1.97/0.60 % Vampire exiting
%------------------------------------------------------------------------------