%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT153^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 07:48:26 AM UTC 2026
% Result : Theorem 0.53s 0.43s
% Output : Refutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT153^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n020.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 18:03:04 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.22/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.42 % (1404375)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.53/0.42 % (1404381)lrs+10_16_si=on:nwc=1.5:random_seed=1855227016:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.53/0.42 % (1404386)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.53/0.42 % (1404386)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.53/0.42 % (1404381)Instruction limit reached!
% 0.53/0.42 % (1404381)------------------------------
% 0.53/0.42 % (1404381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404381)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404381)Termination reason: Instruction limit
% 0.53/0.42 % (1404381)Termination phase: Property scanning
% 0.53/0.42 % (1404381)Time elapsed: 0.005 s
% 0.53/0.42 % (1404381)Peak memory usage: 10 MB
% 0.53/0.42 % (1404381)Instructions burned: 21 (million)
% 0.53/0.42 % (1404382)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2876977952:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.53/0.42 % (1404380)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1890934633:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.53/0.42 % (1404385)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1488587041:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.53/0.42 % (1404384)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=703548085:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.53/0.42 % (1404383)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=1508062116: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.53/0.42 % (1404386)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=29365609:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.53/0.42 % (1404382)Instruction limit reached!
% 0.53/0.42 % (1404382)------------------------------
% 0.53/0.42 % (1404382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404382)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404382)Termination reason: Instruction limit
% 0.53/0.42 % (1404382)Termination phase: shuffling
% 0.53/0.42 % (1404382)Time elapsed: 0.003 s
% 0.53/0.42 % (1404382)Peak memory usage: 10 MB
% 0.53/0.42 % (1404382)Instructions burned: 6 (million)
% 0.53/0.42 % (1404384)Instruction limit reached!
% 0.53/0.42 % (1404384)------------------------------
% 0.53/0.42 % (1404384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404384)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404384)Termination reason: Instruction limit
% 0.53/0.42 % (1404384)Termination phase: Property scanning
% 0.53/0.42 % (1404384)Time elapsed: 0.011 s
% 0.53/0.42 % (1404384)Peak memory usage: 10 MB
% 0.53/0.42 % (1404384)Instructions burned: 24 (million)
% 0.53/0.42 % (1404388)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3496261596:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.53/0.42 % (1404388)Instruction limit reached!
% 0.53/0.42 % (1404388)------------------------------
% 0.53/0.42 % (1404388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404388)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404388)Termination reason: Instruction limit
% 0.53/0.42 % (1404388)Termination phase: shuffling
% 0.53/0.42 % (1404388)Time elapsed: 0.001 s
% 0.53/0.42 % (1404388)Peak memory usage: 10 MB
% 0.53/0.42 % (1404388)Instructions burned: 3 (million)
% 0.53/0.42 % (1404398)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=67556995:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.53/0.42 % (1404397)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.53/0.42 % (1404395)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3195064539:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.53/0.42 % (1404398)Instruction limit reached!
% 0.53/0.42 % (1404398)------------------------------
% 0.53/0.42 % (1404398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404398)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404398)Termination reason: Instruction limit
% 0.53/0.42 % (1404398)Termination phase: shuffling
% 0.53/0.42 % (1404398)Time elapsed: 0.003 s
% 0.53/0.42 % (1404398)Peak memory usage: 10 MB
% 0.53/0.42 % (1404398)Instructions burned: 13 (million)
% 0.53/0.42 % (1404397)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2552733870:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.53/0.42 % (1404395)Instruction limit reached!
% 0.53/0.42 % (1404395)------------------------------
% 0.53/0.42 % (1404395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404395)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404395)Termination reason: Instruction limit
% 0.53/0.42 % (1404395)Termination phase: shuffling
% 0.53/0.42 % (1404395)Time elapsed: 0.005 s
% 0.53/0.42 % (1404395)Peak memory usage: 10 MB
% 0.53/0.42 % (1404395)Instructions burned: 5 (million)
% 0.53/0.42 % (1404385)Instruction limit reached!
% 0.53/0.42 % (1404385)------------------------------
% 0.53/0.42 % (1404385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404385)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404385)Termination reason: Instruction limit
% 0.53/0.42 % (1404385)Termination phase: Property scanning
% 0.53/0.42 % (1404385)Time elapsed: 0.036 s
% 0.53/0.42 % (1404385)Peak memory usage: 12 MB
% 0.53/0.42 % (1404385)Instructions burned: 77 (million)
% 0.53/0.42 % (1404397)Instruction limit reached!
% 0.53/0.42 % (1404397)------------------------------
% 0.53/0.42 % (1404397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404397)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404397)Termination reason: Instruction limit
% 0.53/0.42 % (1404397)Termination phase: shuffling
% 0.53/0.42 % (1404397)Time elapsed: 0.004 s
% 0.53/0.42 % (1404397)Peak memory usage: 10 MB
% 0.53/0.42 % (1404397)Instructions burned: 8 (million)
% 0.53/0.42 % (1404401)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.53/0.42 % (1404401)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.53/0.42 % (1404401)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2942344053: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.53/0.42 % (1404380)Instruction limit reached!
% 0.53/0.42 % (1404380)------------------------------
% 0.53/0.42 % (1404380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404380)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404380)Termination reason: Instruction limit
% 0.53/0.42 % (1404380)Termination phase: Saturation
% 0.53/0.42 % (1404380)Time elapsed: 0.046 s
% 0.53/0.42 % (1404380)Peak memory usage: 12 MB
% 0.53/0.42 % (1404380)Instructions burned: 88 (million)
% 0.53/0.42 % (1404401)Instruction limit reached!
% 0.53/0.42 % (1404401)------------------------------
% 0.53/0.42 % (1404401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404401)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404401)Termination reason: Instruction limit
% 0.53/0.42 % (1404401)Termination phase: Property scanning
% 0.53/0.42 % (1404401)Time elapsed: 0.007 s
% 0.53/0.42 % (1404401)Peak memory usage: 10 MB
% 0.53/0.42 % (1404401)Instructions burned: 32 (million)
% 0.53/0.42 % (1404405)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.53/0.42 % (1404403)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=528657253:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.53/0.42 % (1404404)lrs+10_1_si=on:cs=on:random_seed=2610821121:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.53/0.42 % (1404405)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=4130935411:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.53/0.42 % (1404408)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1133090919:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.53/0.42 % (1404405)Instruction limit reached!
% 0.53/0.42 % (1404405)------------------------------
% 0.53/0.42 % (1404405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404405)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404405)Termination reason: Instruction limit
% 0.53/0.42 % (1404405)Termination phase: shuffling
% 0.53/0.42 % (1404405)Time elapsed: 0.003 s
% 0.53/0.42 % (1404405)Peak memory usage: 10 MB
% 0.53/0.42 % (1404405)Instructions burned: 6 (million)
% 0.53/0.42 % (1404404)Instruction limit reached!
% 0.53/0.42 % (1404404)------------------------------
% 0.53/0.42 % (1404404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.42 % (1404404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.42 % (1404404)CaDiCaL version: 2.1.3
% 0.53/0.42 % (1404404)Termination reason: Instruction limit
% 0.53/0.42 % (1404404)Termination phase: shuffling
% 0.53/0.42 % (1404404)Time elapsed: 0.004 s
% 0.53/0.42 % (1404404)Peak memory usage: 10 MB
% 0.53/0.42 % (1404404)Instructions burned: 8 (million)
% 0.53/0.43 % (1404407)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3852421176:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.53/0.43 % (1404386)Instruction limit reached!
% 0.53/0.43 % (1404386)------------------------------
% 0.53/0.43 % (1404386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404386)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404386)Termination reason: Instruction limit
% 0.53/0.43 % (1404386)Termination phase: Saturation
% 0.53/0.43 % (1404386)Time elapsed: 0.076 s
% 0.53/0.43 % (1404386)Peak memory usage: 14 MB
% 0.53/0.43 % (1404386)Instructions burned: 157 (million)
% 0.53/0.43 % (1404413)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1555755030:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.53/0.43 % (1404414)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3442550474:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.53/0.43 % (1404407)Instruction limit reached!
% 0.53/0.43 % (1404407)------------------------------
% 0.53/0.43 % (1404407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404407)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404407)Termination reason: Instruction limit
% 0.53/0.43 % (1404407)Termination phase: Property scanning
% 0.53/0.43 % (1404407)Time elapsed: 0.019 s
% 0.53/0.43 % (1404407)Peak memory usage: 11 MB
% 0.53/0.43 % (1404407)Instructions burned: 39 (million)
% 0.53/0.43 % (1404414)Instruction limit reached!
% 0.53/0.43 % (1404414)------------------------------
% 0.53/0.43 % (1404414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404414)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404414)Termination reason: Instruction limit
% 0.53/0.43 % (1404414)Termination phase: shuffling
% 0.53/0.43 % (1404414)Time elapsed: 0.007 s
% 0.53/0.43 % (1404414)Peak memory usage: 10 MB
% 0.53/0.43 % (1404414)Instructions burned: 14 (million)
% 0.53/0.43 % (1404383) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1404375-1404383"...
% 0.53/0.43 % (1404413)Instruction limit reached!
% 0.53/0.43 % (1404413)------------------------------
% 0.53/0.43 % (1404413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404413)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404413)Termination reason: Instruction limit
% 0.53/0.43 % (1404413)Termination phase: Property scanning
% 0.53/0.43 % (1404413)Time elapsed: 0.011 s
% 0.53/0.43 % (1404413)Peak memory usage: 10 MB
% 0.53/0.43 % (1404413)Instructions burned: 25 (million)
% 0.53/0.43 % (1404403)Instruction limit reached!
% 0.53/0.43 % (1404403)------------------------------
% 0.53/0.43 % (1404403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404403)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404403)Termination reason: Instruction limit
% 0.53/0.43 % (1404403)Termination phase: Function definition elimination
% 0.53/0.43 % (1404403)Time elapsed: 0.038 s
% 0.53/0.43 % (1404403)Peak memory usage: 11 MB
% 0.53/0.43 % (1404403)Instructions burned: 88 (million)
% 0.53/0.43 % (1404383)...printing done.
% 0.53/0.43 % (1404383)Refutation found. Thanks to Tanya!
% 0.53/0.43 % SZS status Theorem for theBenchmark
% 0.53/0.43 % SZS output start Proof for theBenchmark
% 0.53/0.43 thf(type_def_5, type, extended_enat: $tType).
% 0.53/0.43 thf(type_def_6, type, stream: $tType > $tType).
% 0.53/0.43 thf(type_def_7, type, set: $tType > $tType).
% 0.53/0.43 thf(type_def_8, type, nat: $tType).
% 0.53/0.43 thf(type_def_9, type, int: $tType).
% 0.53/0.43 thf(type_def_10, type, itself: $tType > $tType).
% 0.53/0.43 thf(type_def_11, type, a: $tType).
% 0.53/0.43 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 0.53/0.43 thf(func_def_0, type, zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_1, type, field: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_2, type, mult_zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_3, type, semiring_1: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_4, type, semiring_char_0: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_5, type, division_ring: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_6, type, semigroup_mult: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_7, type, comm_semiring_1: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_8, type, linordered_idom: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_9, type, linordered_ring: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_10, type, linordered_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_11, type, ab_semigroup_mult: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_12, type, linordered_semidom: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_13, type, linord581940658strict: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_14, type, archim1727834104eiling: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_15, type, semiri1193490041visors: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_16, type, linord20386208strict: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_17, type, archim1804426504_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_18, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_19, type, linord893533164strict: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_20, type, semiri1923998003cancel: !>[X0: $tType]:((itself @ X0 > $o))).
% 0.53/0.43 thf(func_def_21, type, archimedean_ceiling: !>[X0: $tType]:((X0 > int))).
% 0.53/0.43 thf(func_def_22, type, coindu1365464361scount: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > extended_enat))).
% 0.53/0.43 thf(func_def_23, type, coindu76177514sfirst: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > extended_enat))).
% 0.53/0.43 thf(func_def_24, type, extended_enat2: (nat > extended_enat)).
% 0.53/0.43 thf(func_def_25, type, extended_case_enat: !>[X0: $tType]:(((nat > X0) > X0 > extended_enat > X0))).
% 0.53/0.43 thf(func_def_26, type, extended_rec_enat: !>[X0: $tType]:(((nat > X0) > X0 > extended_enat > X0))).
% 0.53/0.43 thf(func_def_27, type, extended_size_enat: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_28, type, extend1396239628finity: !>[X0: $tType]:(X0)).
% 0.53/0.43 thf(func_def_29, type, extended_the_enat: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_30, type, inverse_inverse: !>[X0: $tType]:((X0 > X0))).
% 0.53/0.43 thf(func_def_31, type, finite_card: !>[X0: $tType]:((set @ X0 > nat))).
% 0.53/0.43 thf(func_def_32, type, times_times: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.53/0.43 thf(func_def_33, type, zero_zero: !>[X0: $tType]:(X0)).
% 0.53/0.43 thf(func_def_34, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 0.53/0.43 thf(func_def_35, type, nat2: (int > nat)).
% 0.53/0.43 thf(func_def_36, type, linear1341015445_UNTIL: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0 > $o))).
% 0.53/0.43 thf(func_def_37, type, linear1386806755on_alw: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > $o))).
% 0.53/0.43 thf(func_def_38, type, linear505997466_on_ev: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > $o))).
% 0.53/0.43 thf(func_def_39, type, linear1335279038n_wait: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0 > nat))).
% 0.53/0.43 thf(func_def_40, type, semiring_1_of_nat: !>[X0: $tType]:((nat > X0))).
% 0.53/0.43 thf(func_def_41, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 0.53/0.43 thf(func_def_42, type, nat_tr1645093318rphism: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > $o) > $o))).
% 0.53/0.43 thf(func_def_43, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.53/0.43 thf(func_def_44, type, type: !>[X0: $tType]:(itself @ X0)).
% 0.53/0.43 thf(func_def_45, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 0.53/0.43 thf(func_def_46, type, sdrop: !>[X0: $tType]:((nat > stream @ X0 > stream @ X0))).
% 0.53/0.43 thf(func_def_47, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 0.53/0.43 thf(func_def_48, type, p: (stream @ a > $o)).
% 0.53/0.43 thf(func_def_49, type, omega: stream @ a).
% 0.53/0.43 thf(func_def_51, type, db0: !>[X0: $tType]:(X0)).
% 0.53/0.43 thf(func_def_52, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.53/0.43 thf(func_def_55, type, vNOT: ($o > $o)).
% 0.53/0.43 thf(func_def_56, type, vIMP: ($o > $o > $o)).
% 0.53/0.43 thf(func_def_57, type, vOR: ($o > $o > $o)).
% 0.53/0.43 thf(func_def_58, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.53/0.43 thf(func_def_59, type, db2: !>[X0: $tType]:(X0)).
% 0.53/0.43 thf(func_def_60, type, db1: !>[X0: $tType]:(X0)).
% 0.53/0.43 thf(func_def_61, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.53/0.43 thf(func_def_62, type, vAND: ($o > $o > $o)).
% 0.53/0.43 thf(func_def_63, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.53/0.43 thf(func_def_64, type, sP0: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_65, type, sP1: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_66, type, sP2: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_67, type, sP3: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_68, type, sP4: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_69, type, sP5: (extended_enat > extended_enat > extended_enat > $o)).
% 0.53/0.43 thf(func_def_70, type, sK6: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.53/0.43 thf(func_def_71, type, sK7: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_72, type, sK8: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.53/0.43 thf(func_def_73, type, sK9: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.53/0.43 thf(func_def_74, type, sK10: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 0.53/0.43 thf(func_def_75, type, sK11: !>[X0: $tType]:((X0 > X0))).
% 0.53/0.43 thf(func_def_76, type, sK12: ((extended_enat > $o) > extended_enat)).
% 0.53/0.43 thf(func_def_77, type, sK13: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_78, type, sK14: ((extended_enat > $o) > nat)).
% 0.53/0.43 thf(func_def_79, type, sK15: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_80, type, sK16: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_81, type, sK17: (nat > extended_enat > nat)).
% 0.53/0.43 thf(func_def_82, type, sK18: !>[X0: $tType]:(((X0 > extended_enat) > nat > X0))).
% 0.53/0.43 thf(func_def_83, type, sK19: !>[X0: $tType]:(((X0 > extended_enat) > X0))).
% 0.53/0.43 thf(func_def_84, type, sK20: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_85, type, sK21: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_86, type, sK22: !>[X0: $tType]:((X0 > X0))).
% 0.53/0.43 thf(func_def_87, type, sK23: ((nat > $o) > nat)).
% 0.53/0.43 thf(func_def_88, type, sK24: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_89, type, sK25: ((nat > $o) > nat)).
% 0.53/0.43 thf(func_def_90, type, sK26: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_91, type, sK27: (int > nat)).
% 0.53/0.43 thf(func_def_92, type, sK28: !>[X0: $tType]:(((stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_93, type, sK29: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_94, type, sK30: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_95, type, sK31: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_96, type, sK32: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_97, type, sK33: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_98, type, sK34: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_99, type, sK35: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.53/0.43 thf(func_def_100, type, sK36: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.53/0.43 thf(func_def_101, type, sK37: !>[X0: $tType]:((X0 > nat))).
% 0.53/0.43 thf(func_def_102, type, sK38: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_103, type, sK39: !>[X0: $tType]:((X0 > nat))).
% 0.53/0.43 thf(func_def_104, type, sK40: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 0.53/0.43 thf(func_def_105, type, sK41: ((nat > $o) > nat)).
% 0.53/0.43 thf(func_def_106, type, sK42: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_107, type, sK43: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_108, type, sK44: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_109, type, sK45: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_110, type, sK46: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_111, type, sK47: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_112, type, sK48: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_113, type, sK49: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_114, type, sK50: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_115, type, sK51: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_116, type, sK52: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_117, type, sK53: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_118, type, sK54: (extended_enat > nat)).
% 0.53/0.43 thf(func_def_119, type, sK55: !>[X0: $tType]:((X0 > X0 > nat))).
% 0.53/0.43 thf(func_def_120, type, sK56: !>[X0: $tType]:(((stream @ X0 > $o) > (stream @ X0 > $o) > stream @ X0))).
% 0.53/0.43 thf(func_def_122, type, inv_extended_enat2_58: (extended_enat > nat)).
% 0.53/0.43 thf(f2,axiom,(
% 0.53/0.43 ! [X0 : $tType,X3 : stream @ X0,X2 : (stream @ X0 > $o),X1 : nat] : ((ord_less @ extended_enat @ (extended_enat2 @ X1) @ (coindu76177514sfirst @ X0 @ X2 @ X3)) => ~(X2 @ (sdrop @ X0 @ X1 @ X3)))),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_less__sfirstD)).
% 0.53/0.43 thf(f5,axiom,(
% 0.53/0.43 ! [X0 : $tType,X1 : stream @ X0] : (((sdrop @ X0 @ zero_zero @ nat @ X1)) = X1)),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_sdrop_Osimps_I1_J)).
% 0.53/0.43 thf(f14,axiom,(
% 0.53/0.43 ! [X0 : extended_enat] : (((ord_less @ extended_enat @ zero_zero @ extended_enat @ X0)) = (X0 != zero_zero @ extended_enat))),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_i0__less)).
% 0.53/0.43 thf(f19,axiom,(
% 0.53/0.43 ! [X0 : nat] : ((((extended_enat2 @ X0)) = zero_zero @ extended_enat) = (X0 = zero_zero @ nat))),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_enat__0__iff_I1_J)).
% 0.53/0.43 thf(f22,axiom,(
% 0.53/0.43 ! [X0 : $tType,X1 : (stream @ X0 > $o),X2 : stream @ X0] : (((X1 @ X2)) = (((coindu76177514sfirst @ X0 @ X1 @ X2)) = zero_zero @ extended_enat))),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_sfirst__eq__0)).
% 0.53/0.43 thf(f294,conjecture,(
% 0.53/0.43 (~(p @ (sdrop @ a @ zero_zero @ nat @ omega)) = ((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))))),
% 0.53/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.53/0.43 thf(f295,negated_conjecture,(
% 0.53/0.43 ~ (~(p @ (sdrop @ a @ zero_zero @ nat @ omega)) = ((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))))),
% 0.53/0.43 inference(negated_conjecture,[status(cth)],[f294])).
% 0.53/0.43 thf(f375,plain,(
% 0.53/0.43 ! [X0 : nat] : ((zero_zero @ nat = X0) <=> (((extended_enat2 @ X0)) = zero_zero @ extended_enat))),
% 0.53/0.43 inference(fool_elimination,[],[f19])).
% 0.53/0.43 thf(f406,plain,(
% 0.53/0.43 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o),X3 : nat] : ((ord_less @ extended_enat @ (extended_enat2 @ X3) @ (coindu76177514sfirst @ X0 @ X2 @ X1)) => ~(X2 @ (sdrop @ X0 @ X3 @ X1)))),
% 0.53/0.43 inference(rectify,[],[f2])).
% 0.53/0.43 thf(f407,plain,(
% 0.53/0.43 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o),X3 : nat] : (($true = ((ord_less @ extended_enat @ (extended_enat2 @ X3) @ (coindu76177514sfirst @ X0 @ X2 @ X1)))) => ~ (((X2 @ (sdrop @ X0 @ X3 @ X1))) = $true))),
% 0.53/0.43 inference(fool_elimination,[],[f406])).
% 0.53/0.43 thf(f558,plain,(
% 0.53/0.43 ~ (~(p @ (sdrop @ a @ zero_zero @ nat @ omega)) = ((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))))),
% 0.53/0.43 inference(rectify,[],[f295])).
% 0.53/0.43 thf(f559,plain,(
% 0.53/0.43 ~(~ (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) = $true) <=> (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true))),
% 0.53/0.43 inference(fool_elimination,[],[f558])).
% 0.53/0.43 thf(f713,plain,(
% 0.53/0.43 ! [X0 : extended_enat] : ((((ord_less @ extended_enat @ zero_zero @ extended_enat @ X0)) = $true) <=> (zero_zero @ extended_enat != X0))),
% 0.53/0.43 inference(fool_elimination,[],[f14])).
% 0.53/0.43 thf(f770,plain,(
% 0.53/0.43 ! [X0 : $tType,X1 : (stream @ X0 > $o),X2 : stream @ X0] : ((zero_zero @ extended_enat = ((coindu76177514sfirst @ X0 @ X1 @ X2))) <=> (((X1 @ X2)) = $true))),
% 0.53/0.43 inference(fool_elimination,[],[f22])).
% 0.53/0.43 thf(f793,plain,(
% 0.53/0.43 ! [X0 : $tType,X2 : (stream @ X0 > $o),X1 : stream @ X0,X3 : nat] : (($true = ((ord_less @ extended_enat @ (extended_enat2 @ X3) @ (coindu76177514sfirst @ X0 @ X2 @ X1)))) => (((X2 @ (sdrop @ X0 @ X3 @ X1))) != $true))),
% 0.53/0.43 inference(flattening,[],[f407])).
% 0.53/0.43 thf(f807,plain,(
% 0.53/0.43 ~((((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true) <=> (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) != $true))),
% 0.53/0.43 inference(flattening,[],[f559])).
% 0.53/0.43 thf(f889,plain,(
% 0.53/0.43 ! [X0 : $tType,X1 : stream @ X0,X2 : (stream @ X0 > $o),X3 : nat] : ((((X2 @ (sdrop @ X0 @ X3 @ X1))) != $true) | ($true != ((ord_less @ extended_enat @ (extended_enat2 @ X3) @ (coindu76177514sfirst @ X0 @ X2 @ X1)))))),
% 0.53/0.43 inference(ennf_transformation,[],[f793])).
% 0.53/0.43 thf(f906,plain,(
% 0.53/0.43 (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true) <~> (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) != $true)),
% 0.53/0.43 inference(ennf_transformation,[],[f807])).
% 0.53/0.43 thf(f1033,plain,(
% 0.53/0.43 ! [X0 : extended_enat] : (((((ord_less @ extended_enat @ zero_zero @ extended_enat @ X0)) = $true) | (zero_zero @ extended_enat = X0)) & ((zero_zero @ extended_enat != X0) | (((ord_less @ extended_enat @ zero_zero @ extended_enat @ X0)) != $true)))),
% 0.53/0.43 inference(nnf_transformation,[],[f713])).
% 0.53/0.43 thf(f1093,plain,(
% 0.53/0.43 ! [X0 : $tType,X1 : (stream @ X0 > $o),X2 : stream @ X0] : (((zero_zero @ extended_enat = ((coindu76177514sfirst @ X0 @ X1 @ X2))) | (((X1 @ X2)) != $true)) & ((((X1 @ X2)) = $true) | (zero_zero @ extended_enat != ((coindu76177514sfirst @ X0 @ X1 @ X2)))))),
% 0.53/0.43 inference(nnf_transformation,[],[f770])).
% 0.53/0.43 thf(f1117,plain,(
% 0.53/0.43 ! [X0 : nat] : (((zero_zero @ nat = X0) | (((extended_enat2 @ X0)) != zero_zero @ extended_enat)) & ((((extended_enat2 @ X0)) = zero_zero @ extended_enat) | (zero_zero @ nat != X0)))),
% 0.53/0.43 inference(nnf_transformation,[],[f375])).
% 0.53/0.43 thf(f1128,plain,(
% 0.53/0.43 ((((p @ (sdrop @ a @ zero_zero @ nat @ omega))) = $true) | (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) != $true)) & ((((p @ (sdrop @ a @ zero_zero @ nat @ omega))) != $true) | (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true))),
% 0.53/0.43 inference(nnf_transformation,[],[f906])).
% 0.53/0.43 thf(f1255,plain,(
% 0.53/0.43 ( ! [X0 : extended_enat] : ((((ord_less @ extended_enat @ zero_zero @ extended_enat @ X0)) = $true) | (zero_zero @ extended_enat = X0)) )),
% 0.53/0.43 inference(cnf_transformation,[],[f1033])).
% 0.53/0.43 thf(f1288,plain,(
% 0.53/0.43 ( ! [X0 : $tType,X1 : stream @ X0] : ((((sdrop @ X0 @ zero_zero @ nat @ X1)) = X1)) )),
% 0.53/0.43 inference(cnf_transformation,[],[f5])).
% 0.53/0.43 thf(f1363,plain,(
% 0.53/0.43 ( ! [X0 : $tType,X2 : stream @ X0,X1 : (stream @ X0 > $o)] : ((zero_zero @ extended_enat != ((coindu76177514sfirst @ X0 @ X1 @ X2))) | (((X1 @ X2)) = $true)) )),
% 0.53/0.43 inference(cnf_transformation,[],[f1093])).
% 0.53/0.43 thf(f1416,plain,(
% 0.53/0.43 ( ! [X0 : nat] : ((((extended_enat2 @ X0)) = zero_zero @ extended_enat) | (zero_zero @ nat != X0)) )),
% 0.53/0.43 inference(cnf_transformation,[],[f1117])).
% 0.53/0.43 thf(f1440,plain,(
% 0.53/0.43 (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) != $true) | (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true)),
% 0.53/0.43 inference(cnf_transformation,[],[f1128])).
% 0.53/0.43 thf(f1441,plain,(
% 0.53/0.43 (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) = $true) | (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) != $true)),
% 0.53/0.43 inference(cnf_transformation,[],[f1128])).
% 0.53/0.43 thf(f1487,plain,(
% 0.53/0.43 ( ! [X0 : $tType,X2 : (stream @ X0 > $o),X3 : nat,X1 : stream @ X0] : (($true != ((ord_less @ extended_enat @ (extended_enat2 @ X3) @ (coindu76177514sfirst @ X0 @ X2 @ X1)))) | (((X2 @ (sdrop @ X0 @ X3 @ X1))) != $true)) )),
% 0.53/0.43 inference(cnf_transformation,[],[f889])).
% 0.53/0.43 thf(f1742,plain,(
% 0.53/0.43 (zero_zero @ extended_enat = ((extended_enat2 @ zero_zero @ nat)))),
% 0.53/0.43 inference(equality_resolution,[],[f1416])).
% 0.53/0.43 thf(f1896,definition,(
% 0.53/0.43 spl57_17 <=> (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) = $true)),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_17])],[avatar_definition])).
% 0.53/0.43 thf(f1897,plain,(
% 0.53/0.43 (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) != $true) | spl57_17),
% 0.53/0.43 inference(avatar_component_clause,[],[f1896])).
% 0.53/0.43 thf(f1898,plain,(
% 0.53/0.43 (((p @ (sdrop @ a @ zero_zero @ nat @ omega))) = $true) | ~spl57_17),
% 0.53/0.43 inference(avatar_component_clause,[],[f1896])).
% 0.53/0.43 thf(f1900,definition,(
% 0.53/0.43 spl57_18 <=> (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true)),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_18])],[avatar_definition])).
% 0.53/0.43 thf(f1901,plain,(
% 0.53/0.43 (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) = $true) | ~spl57_18),
% 0.53/0.43 inference(avatar_component_clause,[],[f1900])).
% 0.53/0.43 thf(f1902,plain,(
% 0.53/0.43 (((ord_less @ extended_enat @ (extended_enat2 @ zero_zero @ nat) @ (coindu76177514sfirst @ a @ p @ omega))) != $true) | spl57_18),
% 0.53/0.43 inference(avatar_component_clause,[],[f1900])).
% 0.53/0.43 thf(f1903,plain,(
% 0.53/0.43 spl57_17 | ~spl57_18),
% 0.53/0.43 inference(avatar_split_clause,[],[f1441,f1900,f1896])).
% 0.53/0.43 thf(f1904,plain,(
% 0.53/0.43 spl57_18 | ~spl57_17),
% 0.53/0.43 inference(avatar_split_clause,[],[f1440,f1896,f1900])).
% 0.53/0.43 thf(f1906,definition,(
% 0.53/0.43 spl57_19 <=> (zero_zero @ extended_enat = ((extended_enat2 @ zero_zero @ nat)))),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_19])],[avatar_definition])).
% 0.53/0.43 thf(f1908,plain,(
% 0.53/0.43 (zero_zero @ extended_enat = ((extended_enat2 @ zero_zero @ nat))) | ~spl57_19),
% 0.53/0.43 inference(avatar_component_clause,[],[f1906])).
% 0.53/0.43 thf(f1909,plain,(
% 0.53/0.43 spl57_19),
% 0.53/0.43 inference(avatar_split_clause,[],[f1742,f1906])).
% 0.53/0.43 thf(f2208,plain,(
% 0.53/0.43 ($true != ((p @ omega))) | spl57_17),
% 0.53/0.43 inference(superposition,[],[f1897,f1288])).
% 0.53/0.43 thf(f2210,definition,(
% 0.53/0.43 spl57_79 <=> ($true = ((p @ omega)))),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_79])],[avatar_definition])).
% 0.53/0.43 thf(f2211,plain,(
% 0.53/0.43 ($true = ((p @ omega))) | ~spl57_79),
% 0.53/0.43 inference(avatar_component_clause,[],[f2210])).
% 0.53/0.43 thf(f2212,plain,(
% 0.53/0.43 ($true != ((p @ omega))) | spl57_79),
% 0.53/0.43 inference(avatar_component_clause,[],[f2210])).
% 0.53/0.43 thf(f2213,plain,(
% 0.53/0.43 ~spl57_79 | spl57_17),
% 0.53/0.43 inference(avatar_split_clause,[],[f2208,f1896,f2210])).
% 0.53/0.43 thf(f2248,plain,(
% 0.53/0.43 ($true != ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ a @ p @ omega)))) | (spl57_18 | ~spl57_19)),
% 0.53/0.43 inference(forward_demodulation,[],[f1902,f1908])).
% 0.53/0.43 thf(f2250,definition,(
% 0.53/0.43 spl57_83 <=> ($true = ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ a @ p @ omega))))),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_83])],[avatar_definition])).
% 0.53/0.43 thf(f2251,plain,(
% 0.53/0.43 ($true = ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ a @ p @ omega)))) | ~spl57_83),
% 0.53/0.43 inference(avatar_component_clause,[],[f2250])).
% 0.53/0.43 thf(f2252,plain,(
% 0.53/0.43 ($true != ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ a @ p @ omega)))) | spl57_83),
% 0.53/0.43 inference(avatar_component_clause,[],[f2250])).
% 0.53/0.43 thf(f2253,plain,(
% 0.53/0.43 ~spl57_83 | spl57_18 | ~spl57_19),
% 0.53/0.43 inference(avatar_split_clause,[],[f2248,f1906,f1900,f2250])).
% 0.53/0.43 thf(f2268,plain,(
% 0.53/0.43 (zero_zero @ extended_enat = ((coindu76177514sfirst @ a @ p @ omega))) | ($true != $true) | spl57_83),
% 0.53/0.43 inference(superposition,[],[f2252,f1255])).
% 0.53/0.43 thf(f2269,plain,(
% 0.53/0.43 (zero_zero @ extended_enat = ((coindu76177514sfirst @ a @ p @ omega))) | spl57_83),
% 0.53/0.43 inference(trivial_inequality_removal,[],[f2268])).
% 0.53/0.43 thf(f2406,definition,(
% 0.53/0.43 spl57_90 <=> (zero_zero @ extended_enat = ((coindu76177514sfirst @ a @ p @ omega)))),
% 0.53/0.43 introduced(definition,[new_symbols(definition,[spl57_90])],[avatar_definition])).
% 0.53/0.43 thf(f2408,plain,(
% 0.53/0.43 (zero_zero @ extended_enat = ((coindu76177514sfirst @ a @ p @ omega))) | ~spl57_90),
% 0.53/0.43 inference(avatar_component_clause,[],[f2406])).
% 0.53/0.43 thf(f2409,plain,(
% 0.53/0.43 spl57_90 | spl57_83),
% 0.53/0.43 inference(avatar_split_clause,[],[f2269,f2250,f2406])).
% 0.53/0.43 thf(f2415,plain,(
% 0.53/0.43 ($true = ((p @ omega))) | ~spl57_17),
% 0.53/0.43 inference(forward_demodulation,[],[f1898,f1288])).
% 0.53/0.43 thf(f2416,plain,(
% 0.53/0.43 ($true = ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ a @ p @ omega)))) | (~spl57_18 | ~spl57_19)),
% 0.53/0.43 inference(forward_demodulation,[],[f1901,f1908])).
% 0.53/0.43 thf(f2419,plain,(
% 0.53/0.43 spl57_83 | ~spl57_18 | ~spl57_19),
% 0.53/0.43 inference(avatar_split_clause,[],[f2416,f1906,f1900,f2250])).
% 0.53/0.43 thf(f2420,plain,(
% 0.53/0.43 spl57_79 | ~spl57_17),
% 0.53/0.43 inference(avatar_split_clause,[],[f2415,f1896,f2210])).
% 0.53/0.43 thf(f2557,plain,(
% 0.53/0.43 ( ! [X0 : $tType,X2 : stream @ X0,X1 : (stream @ X0 > $o)] : (($true != ((X1 @ (sdrop @ X0 @ zero_zero @ nat @ X2)))) | ($true != ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ X0 @ X1 @ X2))))) ) | ~spl57_19),
% 0.53/0.43 inference(superposition,[],[f1487,f1908])).
% 0.53/0.43 thf(f2561,plain,(
% 0.53/0.43 ( ! [X0 : $tType,X2 : stream @ X0,X1 : (stream @ X0 > $o)] : (($true != ((ord_less @ extended_enat @ zero_zero @ extended_enat @ (coindu76177514sfirst @ X0 @ X1 @ X2)))) | (((X1 @ X2)) != $true)) ) | ~spl57_19),
% 0.53/0.43 inference(forward_demodulation,[],[f2557,f1288])).
% 0.53/0.43 thf(f2562,plain,(
% 0.53/0.43 ($true != $true) | ($true != ((p @ omega))) | (~spl57_19 | ~spl57_83)),
% 0.53/0.43 inference(superposition,[],[f2561,f2251])).
% 0.53/0.43 thf(f2565,plain,(
% 0.53/0.43 ($true != ((p @ omega))) | (~spl57_19 | ~spl57_83)),
% 0.53/0.43 inference(trivial_inequality_removal,[],[f2562])).
% 0.53/0.43 thf(f2566,plain,(
% 0.53/0.43 $false | (~spl57_19 | ~spl57_79 | ~spl57_83)),
% 0.53/0.43 inference(forward_subsumption_resolution,[],[f2565,f2211])).
% 0.53/0.43 thf(f2567,plain,(
% 0.53/0.43 ~spl57_19 | ~spl57_79 | ~spl57_83),
% 0.53/0.43 inference(avatar_contradiction_clause,[],[f2566])).
% 0.53/0.43 thf(f2894,plain,(
% 0.53/0.43 ($true = ((p @ omega))) | (zero_zero @ extended_enat != zero_zero @ extended_enat) | ~spl57_90),
% 0.53/0.43 inference(superposition,[],[f1363,f2408])).
% 0.53/0.43 thf(f2895,plain,(
% 0.53/0.43 ($true = ((p @ omega))) | ~spl57_90),
% 0.53/0.43 inference(trivial_inequality_removal,[],[f2894])).
% 0.53/0.43 thf(f2896,plain,(
% 0.53/0.43 $false | (spl57_79 | ~spl57_90)),
% 0.53/0.43 inference(forward_subsumption_resolution,[],[f2895,f2212])).
% 0.53/0.43 thf(f2897,plain,(
% 0.53/0.43 spl57_79 | ~spl57_90),
% 0.53/0.43 inference(avatar_contradiction_clause,[],[f2896])).
% 0.53/0.43 cnf(s14, plain, spl57_17 | ~spl57_18, inference(sat_conversion,[],[f1903])).
% 0.53/0.43 cnf(s15, plain, ~spl57_17 | spl57_18, inference(sat_conversion,[],[f1904])).
% 0.53/0.43 cnf(s16, plain, spl57_19, inference(sat_conversion,[],[f1909])).
% 0.53/0.43 cnf(s85, plain, spl57_17 | ~spl57_79, inference(sat_conversion,[],[f2213])).
% 0.53/0.43 cnf(s89, plain, spl57_18 | ~spl57_19 | ~spl57_83, inference(sat_conversion,[],[f2253])).
% 0.53/0.43 cnf(s97, plain, spl57_83 | spl57_90, inference(sat_conversion,[],[f2409])).
% 0.53/0.43 cnf(s100, plain, ~spl57_18 | ~spl57_19 | spl57_83, inference(sat_conversion,[],[f2419])).
% 0.53/0.43 cnf(s101, plain, ~spl57_17 | spl57_79, inference(sat_conversion,[],[f2420])).
% 0.53/0.43 cnf(s120, plain, ~spl57_19 | ~spl57_79 | ~spl57_83, inference(sat_conversion,[],[f2567])).
% 0.53/0.43 cnf(s150, plain, spl57_79 | ~spl57_90, inference(sat_conversion,[],[f2897])).
% 0.53/0.43 cnf(s164, plain, spl57_17, inference(rat,[],[s97,s89,s150,s14,s85,s16])).
% 0.53/0.43 cnf(s165, plain, spl57_79, inference(rat,[],[s101,s164])).
% 0.53/0.43 cnf(s166, plain, spl57_18, inference(rat,[],[s15,s164])).
% 0.53/0.43 cnf(s167, plain, ~spl57_83, inference(rat,[],[s120,s16,s165])).
% 0.53/0.43 cnf(s168, plain, $false, inference(rat,[],[s100,s16,s167,s166])).
% 0.53/0.43 thf(f2898,plain,(
% 0.53/0.43 $false),
% 0.53/0.43 inference(avatar_sat_refutation,[],[s168])).
% 0.53/0.43 % SZS output end Proof for theBenchmark
% 0.53/0.43 % (1404383)------------------------------
% 0.53/0.43 % (1404383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.43 % (1404383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.43 % (1404383)CaDiCaL version: 2.1.3
% 0.53/0.43 % (1404383)Termination reason: Refutation
% 0.53/0.43 % (1404383)Time elapsed: 0.091 s
% 0.53/0.43 % (1404383)Peak memory usage: 15 MB
% 0.53/0.43 % (1404383)Instructions burned: 170 (million)
% 0.53/0.43 % (1404375)Success in time 0.149 s
% 0.53/0.43 % Vampire exiting
%------------------------------------------------------------------------------