%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP105^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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:22 AM UTC 2026
% Result : Theorem 0.43s 0.40s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP105^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n019.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Tue Sep 29 19:54:18 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.18/0.28 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.43/0.40 % (1270146)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.43/0.40 % (1270151)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1347228630:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.43/0.40 % (1270157)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.43/0.40 % (1270157)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.43/0.40 % (1270153)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3469134779:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.43/0.40 % (1270154)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=386117599: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.43/0.40 % (1270155)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1962655429:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.43/0.40 % (1270156)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2302840083:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.43/0.40 % (1270157)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=1118989037:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.43/0.40 % (1270152)lrs+10_16_si=on:nwc=1.5:random_seed=2707358238:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.43/0.40 % (1270153)Instruction limit reached!
% 0.43/0.40 % (1270153)------------------------------
% 0.43/0.40 % (1270153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270153)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270153)Termination reason: Instruction limit
% 0.43/0.40 % (1270153)Termination phase: shuffling
% 0.43/0.40 % (1270153)Time elapsed: 0.003 s
% 0.43/0.40 % (1270153)Peak memory usage: 10 MB
% 0.43/0.40 % (1270153)Instructions burned: 5 (million)
% 0.43/0.40 % (1270152)Instruction limit reached!
% 0.43/0.40 % (1270152)------------------------------
% 0.43/0.40 % (1270152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270152)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270152)Termination reason: Instruction limit
% 0.43/0.40 % (1270152)Termination phase: Property scanning
% 0.43/0.40 % (1270152)Time elapsed: 0.009 s
% 0.43/0.40 % (1270152)Peak memory usage: 10 MB
% 0.43/0.40 % (1270152)Instructions burned: 18 (million)
% 0.43/0.40 % (1270155)Instruction limit reached!
% 0.43/0.40 % (1270155)------------------------------
% 0.43/0.40 % (1270155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270155)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270155)Termination reason: Instruction limit
% 0.43/0.40 % (1270155)Termination phase: Property scanning
% 0.43/0.40 % (1270155)Time elapsed: 0.011 s
% 0.43/0.40 % (1270155)Peak memory usage: 10 MB
% 0.43/0.40 % (1270155)Instructions burned: 24 (million)
% 0.43/0.40 % (1270151)Instruction limit reached!
% 0.43/0.40 % (1270151)------------------------------
% 0.43/0.40 % (1270151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270151)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270151)Termination reason: Instruction limit
% 0.43/0.40 % (1270151)Termination phase: Property scanning
% 0.43/0.40 % (1270151)Time elapsed: 0.021 s
% 0.43/0.40 % (1270151)Peak memory usage: 12 MB
% 0.43/0.40 % (1270151)Instructions burned: 90 (million)
% 0.43/0.40 % (1270165)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3946277619:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.43/0.40 % (1270168)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3295156935:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.43/0.40 % (1270165)Instruction limit reached!
% 0.43/0.40 % (1270165)------------------------------
% 0.43/0.40 % (1270165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270165)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270165)Termination reason: Instruction limit
% 0.43/0.40 % (1270165)Termination phase: shuffling
% 0.43/0.40 % (1270165)Time elapsed: 0.002 s
% 0.43/0.40 % (1270165)Peak memory usage: 10 MB
% 0.43/0.40 % (1270165)Instructions burned: 3 (million)
% 0.43/0.40 % (1270168)Instruction limit reached!
% 0.43/0.40 % (1270168)------------------------------
% 0.43/0.40 % (1270168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270167)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.43/0.40 % (1270168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270168)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270168)Termination reason: Instruction limit
% 0.43/0.40 % (1270168)Termination phase: shuffling
% 0.43/0.40 % (1270168)Time elapsed: 0.003 s
% 0.43/0.40 % (1270168)Peak memory usage: 10 MB
% 0.43/0.40 % (1270168)Instructions burned: 13 (million)
% 0.43/0.40 % (1270166)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2221126920:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.43/0.40 % (1270167)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=526341098:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.43/0.40 % (1270166)Instruction limit reached!
% 0.43/0.40 % (1270166)------------------------------
% 0.43/0.40 % (1270166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270166)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270166)Termination reason: Instruction limit
% 0.43/0.40 % (1270166)Termination phase: shuffling
% 0.43/0.40 % (1270166)Time elapsed: 0.003 s
% 0.43/0.40 % (1270166)Peak memory usage: 10 MB
% 0.43/0.40 % (1270166)Instructions burned: 6 (million)
% 0.43/0.40 % (1270156)Instruction limit reached!
% 0.43/0.40 % (1270156)------------------------------
% 0.43/0.40 % (1270156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270156)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270156)Termination reason: Instruction limit
% 0.43/0.40 % (1270156)Termination phase: Property scanning
% 0.43/0.40 % (1270156)Time elapsed: 0.034 s
% 0.43/0.40 % (1270156)Peak memory usage: 12 MB
% 0.43/0.40 % (1270156)Instructions burned: 75 (million)
% 0.43/0.40 % (1270167)Instruction limit reached!
% 0.43/0.40 % (1270167)------------------------------
% 0.43/0.40 % (1270167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270167)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270167)Termination reason: Instruction limit
% 0.43/0.40 % (1270167)Termination phase: shuffling
% 0.43/0.40 % (1270167)Time elapsed: 0.004 s
% 0.43/0.40 % (1270167)Peak memory usage: 10 MB
% 0.43/0.40 % (1270167)Instructions burned: 9 (million)
% 0.43/0.40 % (1270172)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=3964809713:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.43/0.40 % (1270171)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.43/0.40 % (1270171)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.43/0.40 % (1270171)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=885655352: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.43/0.40 % (1270176)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.43/0.40 % (1270175)lrs+10_1_si=on:cs=on:random_seed=366433626:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.43/0.40 % (1270176)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=1565837117:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.43/0.40 % (1270177)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3539625279:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.43/0.40 % (1270175)Instruction limit reached!
% 0.43/0.40 % (1270175)------------------------------
% 0.43/0.40 % (1270175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270175)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270175)Termination reason: Instruction limit
% 0.43/0.40 % (1270175)Termination phase: shuffling
% 0.43/0.40 % (1270175)Time elapsed: 0.004 s
% 0.43/0.40 % (1270175)Peak memory usage: 10 MB
% 0.43/0.40 % (1270175)Instructions burned: 8 (million)
% 0.43/0.40 % (1270176)Instruction limit reached!
% 0.43/0.40 % (1270176)------------------------------
% 0.43/0.40 % (1270176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270176)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270176)Termination reason: Instruction limit
% 0.43/0.40 % (1270176)Termination phase: shuffling
% 0.43/0.40 % (1270176)Time elapsed: 0.002 s
% 0.43/0.40 % (1270176)Peak memory usage: 10 MB
% 0.43/0.40 % (1270176)Instructions burned: 4 (million)
% 0.43/0.40 % (1270172)Instruction limit reached!
% 0.43/0.40 % (1270172)------------------------------
% 0.43/0.40 % (1270172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270172)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270172)Termination reason: Instruction limit
% 0.43/0.40 % (1270172)Termination phase: Function definition elimination
% 0.43/0.40 % (1270172)Time elapsed: 0.019 s
% 0.43/0.40 % (1270172)Peak memory usage: 11 MB
% 0.43/0.40 % (1270172)Instructions burned: 86 (million)
% 0.43/0.40 % (1270171)Instruction limit reached!
% 0.43/0.40 % (1270171)------------------------------
% 0.43/0.40 % (1270171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.40 % (1270171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.40 % (1270171)CaDiCaL version: 2.1.3
% 0.43/0.40 % (1270171)Termination reason: Instruction limit
% 0.43/0.40 % (1270171)Termination phase: Property scanning
% 0.43/0.40 % (1270171)Time elapsed: 0.013 s
% 0.43/0.40 % (1270171)Peak memory usage: 10 MB
% 0.43/0.40 % (1270171)Instructions burned: 29 (million)
% 0.43/0.40 % (1270154) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1270146-1270154"...
% 0.43/0.40 % (1270154)...printing done.
% 0.43/0.40 % (1270154)Refutation found. Thanks to Tanya!
% 0.43/0.40 % SZS status Theorem for theBenchmark
% 0.43/0.40 % SZS output start Proof for theBenchmark
% 0.43/0.40 thf(type_def_5, type, list_l2071841302list_a: $tType).
% 0.43/0.40 thf(type_def_6, type, option_list_list_a: $tType).
% 0.43/0.40 thf(type_def_7, type, list_list_list_a: $tType).
% 0.43/0.40 thf(type_def_8, type, option_list_a: $tType).
% 0.43/0.40 thf(type_def_9, type, list_list_a: $tType).
% 0.43/0.40 thf(type_def_10, type, set_real: $tType).
% 0.43/0.40 thf(type_def_11, type, set_nat: $tType).
% 0.43/0.40 thf(type_def_12, type, option_a: $tType).
% 0.43/0.40 thf(type_def_13, type, list_a: $tType).
% 0.43/0.40 thf(type_def_14, type, real: $tType).
% 0.43/0.40 thf(type_def_15, type, nat: $tType).
% 0.43/0.40 thf(type_def_16, type, int: $tType).
% 0.43/0.40 thf(type_def_17, type, a: $tType).
% 0.43/0.40 thf(type_def_18, type, sTfun: ($tType * $tType) > $tType).
% 0.43/0.40 thf(func_def_0, type, inverse_inverse_real: (real > real)).
% 0.43/0.40 thf(func_def_1, type, zero_zero_int: int).
% 0.43/0.40 thf(func_def_2, type, zero_zero_nat: nat).
% 0.43/0.40 thf(func_def_3, type, zero_zero_real: real).
% 0.43/0.40 thf(func_def_4, type, if_nat: ($o > nat > nat > nat)).
% 0.43/0.40 thf(func_def_5, type, listSl162220270list_a: (list_list_a > nat > list_list_list_a)).
% 0.43/0.40 thf(func_def_6, type, listSl97544552lice_a: (list_a > nat > list_list_a)).
% 0.43/0.40 thf(func_def_7, type, listSl856612276list_a: (list_list_a > nat > nat > list_list_list_a)).
% 0.43/0.40 thf(func_def_8, type, listSl1495374126_aux_a: (list_a > nat > nat > list_list_a)).
% 0.43/0.40 thf(func_def_9, type, bind_l311701255list_a: (list_list_list_a > (list_list_a > list_list_list_a) > list_list_list_a)).
% 0.43/0.40 thf(func_def_10, type, bind_l94945665list_a: (list_list_list_a > (list_list_a > list_list_a) > list_list_a)).
% 0.43/0.40 thf(func_def_11, type, bind_list_list_a_a: (list_list_list_a > (list_list_a > list_a) > list_a)).
% 0.43/0.40 thf(func_def_12, type, bind_l971853709list_a: (list_list_a > (list_a > list_list_list_a) > list_list_list_a)).
% 0.43/0.40 thf(func_def_13, type, bind_list_a_list_a: (list_list_a > (list_a > list_list_a) > list_list_a)).
% 0.43/0.40 thf(func_def_14, type, bind_list_a_a: (list_list_a > (list_a > list_a) > list_a)).
% 0.43/0.40 thf(func_def_15, type, bind_a_list_list_a: (list_a > (a > list_list_list_a) > list_list_list_a)).
% 0.43/0.40 thf(func_def_16, type, bind_a_list_a: (list_a > (a > list_list_a) > list_list_a)).
% 0.43/0.40 thf(func_def_17, type, bind_a_a: (list_a > (a > list_a) > list_a)).
% 0.43/0.40 thf(func_def_18, type, concat_list_list_a: (list_l2071841302list_a > list_list_list_a)).
% 0.43/0.40 thf(func_def_19, type, concat_list_a: (list_list_list_a > list_list_a)).
% 0.43/0.40 thf(func_def_20, type, concat_a: (list_list_a > list_a)).
% 0.43/0.40 thf(func_def_21, type, count_429956358list_a: (list_list_list_a > list_list_a > nat)).
% 0.43/0.40 thf(func_def_22, type, count_list_list_a: (list_list_a > list_a > nat)).
% 0.43/0.40 thf(func_def_23, type, count_list_a: (list_a > a > nat)).
% 0.43/0.40 thf(func_def_24, type, gen_le840878749list_a: (nat > list_list_list_a > nat)).
% 0.43/0.40 thf(func_def_25, type, gen_length_list_a: (nat > list_list_a > nat)).
% 0.43/0.40 thf(func_def_26, type, gen_length_a: (nat > list_a > nat)).
% 0.43/0.40 thf(func_def_27, type, nil_list_list_list_a: list_l2071841302list_a).
% 0.43/0.40 thf(func_def_28, type, nil_list_list_a: list_list_list_a).
% 0.43/0.40 thf(func_def_29, type, nil_list_a: list_list_a).
% 0.43/0.40 thf(func_def_30, type, nil_a: list_a).
% 0.43/0.40 thf(func_def_31, type, list_ex1_list_list_a: ((list_list_a > $o) > list_list_list_a > $o)).
% 0.43/0.40 thf(func_def_32, type, list_ex1_list_a: ((list_a > $o) > list_list_a > $o)).
% 0.43/0.40 thf(func_def_33, type, list_ex1_a: ((a > $o) > list_a > $o)).
% 0.43/0.40 thf(func_def_34, type, map_fi824137674list_a: ((list_list_a > option_list_list_a) > list_list_list_a > list_list_list_a)).
% 0.43/0.40 thf(func_def_35, type, map_fi213215172list_a: ((list_list_a > option_list_a) > list_list_list_a > list_list_a)).
% 0.43/0.40 thf(func_def_36, type, map_fi1574988606st_a_a: ((list_list_a > option_a) > list_list_list_a > list_a)).
% 0.43/0.40 thf(func_def_37, type, map_fi1090123216list_a: ((list_a > option_list_list_a) > list_list_a > list_list_list_a)).
% 0.43/0.40 thf(func_def_38, type, map_fi461586634list_a: ((list_a > option_list_a) > list_list_a > list_list_a)).
% 0.43/0.40 thf(func_def_39, type, map_filter_list_a_a: ((list_a > option_a) > list_list_a > list_a)).
% 0.43/0.40 thf(func_def_40, type, map_fi2089402454list_a: ((a > option_list_list_a) > list_a > list_list_list_a)).
% 0.43/0.40 thf(func_def_41, type, map_filter_a_list_a: ((a > option_list_a) > list_a > list_list_a)).
% 0.43/0.40 thf(func_def_42, type, map_filter_a_a: ((a > option_a) > list_a > list_a)).
% 0.43/0.40 thf(func_def_43, type, maps_l57963201list_a: ((list_list_a > list_list_list_a) > list_list_list_a > list_list_list_a)).
% 0.43/0.40 thf(func_def_44, type, maps_l2025957947list_a: ((list_list_a > list_list_a) > list_list_list_a > list_list_a)).
% 0.43/0.41 thf(func_def_45, type, maps_list_list_a_a: ((list_list_a > list_a) > list_list_list_a > list_a)).
% 0.43/0.41 thf(func_def_46, type, maps_l755382343list_a: ((list_a > list_list_list_a) > list_list_a > list_list_list_a)).
% 0.43/0.41 thf(func_def_47, type, maps_list_a_list_a: ((list_a > list_list_a) > list_list_a > list_list_a)).
% 0.43/0.41 thf(func_def_48, type, maps_list_a_a: ((list_a > list_a) > list_list_a > list_a)).
% 0.43/0.41 thf(func_def_49, type, maps_a_list_list_a: ((a > list_list_list_a) > list_a > list_list_list_a)).
% 0.43/0.41 thf(func_def_50, type, maps_a_list_a: ((a > list_list_a) > list_a > list_list_a)).
% 0.43/0.41 thf(func_def_51, type, maps_a_a: ((a > list_a) > list_a > list_a)).
% 0.43/0.41 thf(func_def_52, type, member_list_list_a: (list_list_list_a > list_list_a > $o)).
% 0.43/0.41 thf(func_def_53, type, member_list_a: (list_list_a > list_a > $o)).
% 0.43/0.41 thf(func_def_54, type, member_a: (list_a > a > $o)).
% 0.43/0.41 thf(func_def_55, type, null_list_list_a: (list_list_list_a > $o)).
% 0.43/0.41 thf(func_def_56, type, null_list_a: (list_list_a > $o)).
% 0.43/0.41 thf(func_def_57, type, null_a: (list_a > $o)).
% 0.43/0.41 thf(func_def_58, type, semiri2019852685at_int: (nat > int)).
% 0.43/0.41 thf(func_def_59, type, semiri1382578993at_nat: (nat > nat)).
% 0.43/0.41 thf(func_def_60, type, semiri2110766477t_real: (nat > real)).
% 0.43/0.41 thf(func_def_61, type, size_s575106428list_a: (list_list_list_a > nat)).
% 0.43/0.41 thf(func_def_62, type, size_s1427607542list_a: (list_list_a > nat)).
% 0.43/0.41 thf(func_def_63, type, size_size_list_a: (list_a > nat)).
% 0.43/0.41 thf(func_def_64, type, ord_less_int: (int > int > $o)).
% 0.43/0.41 thf(func_def_65, type, ord_less_nat: (nat > nat > $o)).
% 0.43/0.41 thf(func_def_66, type, ord_less_real: (real > real > $o)).
% 0.43/0.41 thf(func_def_67, type, ord_less_eq_int: (int > int > $o)).
% 0.43/0.41 thf(func_def_68, type, ord_less_eq_nat: (nat > nat > $o)).
% 0.43/0.41 thf(func_def_69, type, ord_less_eq_real: (real > real > $o)).
% 0.43/0.41 thf(func_def_70, type, power_power_int: (int > nat > int)).
% 0.43/0.41 thf(func_def_71, type, power_power_nat: (nat > nat > nat)).
% 0.43/0.41 thf(func_def_72, type, power_power_real: (real > nat > real)).
% 0.43/0.41 thf(func_def_73, type, divide_divide_int: (int > int > int)).
% 0.43/0.41 thf(func_def_74, type, divide_divide_nat: (nat > nat > nat)).
% 0.43/0.41 thf(func_def_75, type, divide_divide_real: (real > real > real)).
% 0.43/0.41 thf(func_def_76, type, collect_nat: ((nat > $o) > set_nat)).
% 0.43/0.41 thf(func_def_77, type, collect_real: ((real > $o) > set_real)).
% 0.43/0.41 thf(func_def_78, type, member_nat: (nat > set_nat > $o)).
% 0.43/0.41 thf(func_def_79, type, member_real: (real > set_real > $o)).
% 0.43/0.41 thf(func_def_80, type, k: nat).
% 0.43/0.41 thf(func_def_84, type, db1: !>[X0: $tType]:(X0)).
% 0.43/0.41 thf(func_def_85, type, db0: !>[X0: $tType]:(X0)).
% 0.43/0.41 thf(func_def_86, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.43/0.41 thf(func_def_87, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.43/0.41 thf(func_def_88, type, vIMP: ($o > $o > $o)).
% 0.43/0.41 thf(func_def_89, type, db2: !>[X0: $tType]:(X0)).
% 0.43/0.41 thf(func_def_90, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.43/0.41 thf(func_def_91, type, vNOT: ($o > $o)).
% 0.43/0.41 thf(func_def_92, type, vOR: ($o > $o > $o)).
% 0.43/0.41 thf(func_def_93, type, vAND: ($o > $o > $o)).
% 0.43/0.41 thf(func_def_94, type, sK0: (real > nat)).
% 0.43/0.41 thf(func_def_95, type, sK1: (real > real)).
% 0.43/0.41 thf(func_def_96, type, sK2: (real > nat)).
% 0.43/0.41 thf(func_def_97, type, sK3: ((nat > $o) > nat)).
% 0.43/0.41 thf(func_def_98, type, sK4: ((list_a > $o) > list_a)).
% 0.43/0.41 thf(func_def_99, type, sK5: ((nat > nat) > nat)).
% 0.43/0.41 thf(func_def_100, type, sK6: ((nat > nat) > nat)).
% 0.43/0.41 thf(func_def_101, type, sK7: (int > nat)).
% 0.43/0.41 thf(func_def_102, type, sK8: (real > real > real)).
% 0.43/0.41 thf(func_def_103, type, sK9: (real > nat)).
% 0.43/0.41 thf(func_def_104, type, sK10: (real > nat)).
% 0.43/0.41 thf(func_def_105, type, sK11: ((nat > $o) > nat)).
% 0.43/0.41 thf(func_def_106, type, sK12: (int > nat)).
% 0.43/0.41 thf(func_def_107, type, sK13: ((nat > $o) > set_nat > nat)).
% 0.43/0.41 thf(func_def_108, type, sK14: ((nat > $o) > nat)).
% 0.43/0.41 thf(func_def_109, type, sK15: (nat > (nat > $o) > nat)).
% 0.43/0.41 thf(func_def_110, type, sK16: (set_nat > (nat > $o) > nat)).
% 0.43/0.41 thf(func_def_111, type, sK17: (real > real)).
% 0.43/0.41 thf(func_def_112, type, sK18: (nat > list_a)).
% 0.43/0.41 thf(func_def_113, type, sK19: (nat > real > real)).
% 0.43/0.41 thf(func_def_114, type, sK20: ((real > $o) > real)).
% 0.43/0.41 thf(func_def_115, type, sK21: ((real > $o) > real)).
% 0.43/0.41 thf(func_def_116, type, sK22: ((real > $o) > nat)).
% 0.43/0.41 thf(func_def_117, type, sK23: ((nat > $o) > nat)).
% 0.43/0.41 thf(func_def_118, type, sK24: ((nat > $o) > set_nat > nat)).
% 0.43/0.41 thf(func_def_119, type, sK25: (set_real > real)).
% 0.43/0.41 thf(func_def_120, type, sK26: (real > set_real > real)).
% 0.43/0.41 thf(func_def_121, type, sK27: (real > set_real > real)).
% 0.43/0.41 thf(func_def_122, type, sK28: (int > nat)).
% 0.43/0.41 thf(func_def_123, type, sK29: (nat > real > real)).
% 0.43/0.41 thf(func_def_124, type, sK30: (int > nat)).
% 0.43/0.41 thf(func_def_125, type, sK31: ((nat > $o) > nat > nat)).
% 0.43/0.41 thf(func_def_126, type, sK32: (set_nat > (nat > $o) > nat)).
% 0.43/0.41 thf(f2,axiom,(
% 0.43/0.41 ! [X0 : list_a] : (((listSl97544552lice_a @ X0 @ zero_zero_nat)) = nil_list_a)),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_list__slice__0)).
% 0.43/0.41 thf(f10,axiom,(
% 0.43/0.41 ! [X0 : list_a,X1 : nat] : ((ord_less_nat @ (size_size_list_a @ X0) @ X1) => (((listSl97544552lice_a @ X0 @ X1)) = nil_list_a))),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_list__slice__less)).
% 0.43/0.41 thf(f50,axiom,(
% 0.43/0.41 ! [X0 : list_list_a] : ((((size_s1427607542list_a @ X0)) = zero_zero_nat) = (X0 = nil_list_a))),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_length__0__conv)).
% 0.43/0.41 thf(f52,axiom,(
% 0.43/0.41 ! [X0 : list_a] : ((((size_size_list_a @ X0)) = zero_zero_nat) = (X0 = nil_a))),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_length__0__conv)).
% 0.43/0.41 thf(f55,axiom,(
% 0.43/0.41 ! [X0 : list_a] : (((ord_less_nat @ zero_zero_nat @ (size_size_list_a @ X0))) = (X0 != nil_a))),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_length__greater__0__conv)).
% 0.43/0.41 thf(f56,axiom,(
% 0.43/0.41 (((size_s1427607542list_a @ nil_list_a)) = zero_zero_nat)),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_list_Osize_I3_J)).
% 0.43/0.41 thf(f62,axiom,(
% 0.43/0.41 ! [X0 : nat] : ? [X1 : list_a] : (((size_size_list_a @ X1)) = X0)),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_Ex__list__of__length)).
% 0.43/0.41 thf(f258,axiom,(
% 0.43/0.41 ! [X1 : nat,X0 : list_a] : (((size_s1427607542list_a @ (listSl97544552lice_a @ X0 @ X1))) = ((divide_divide_nat @ (size_size_list_a @ X0) @ X1)))),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_257_list__slice__length)).
% 0.43/0.41 thf(f350,conjecture,(
% 0.43/0.41 (((listSl97544552lice_a @ nil_a @ k)) = nil_list_a)),
% 0.43/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 0.43/0.41 thf(f351,negated_conjecture,(
% 0.43/0.41 ~ (((listSl97544552lice_a @ nil_a @ k)) = nil_list_a)),
% 0.43/0.41 inference(negated_conjecture,[status(cth)],[f350])).
% 0.43/0.41 thf(f370,plain,(
% 0.43/0.41 ! [X0 : list_a] : ((zero_zero_nat = ((size_size_list_a @ X0))) <=> (nil_a = X0))),
% 0.43/0.41 inference(fool_elimination,[],[f52])).
% 0.43/0.41 thf(f487,plain,(
% 0.43/0.41 ! [X0 : list_a] : ((((ord_less_nat @ zero_zero_nat @ (size_size_list_a @ X0))) = $true) <=> (nil_a != X0))),
% 0.43/0.41 inference(fool_elimination,[],[f55])).
% 0.43/0.41 thf(f631,plain,(
% 0.43/0.41 ! [X0 : list_list_a] : ((zero_zero_nat = ((size_s1427607542list_a @ X0))) <=> (nil_list_a = X0))),
% 0.43/0.41 inference(fool_elimination,[],[f50])).
% 0.43/0.41 thf(f726,plain,(
% 0.43/0.41 ! [X0 : list_a,X1 : nat] : ((ord_less_nat @ (size_size_list_a @ X0) @ X1) => (((listSl97544552lice_a @ X0 @ X1)) = nil_list_a))),
% 0.43/0.41 inference(rectify,[],[f10])).
% 0.43/0.41 thf(f727,plain,(
% 0.43/0.41 ! [X1 : nat,X0 : list_a] : ((((ord_less_nat @ (size_size_list_a @ X0) @ X1)) = $true) => (nil_list_a = ((listSl97544552lice_a @ X0 @ X1))))),
% 0.43/0.41 inference(fool_elimination,[],[f726])).
% 0.43/0.41 thf(f827,plain,(
% 0.43/0.41 ! [X0 : nat,X1 : list_a] : (((divide_divide_nat @ (size_size_list_a @ X1) @ X0)) = ((size_s1427607542list_a @ (listSl97544552lice_a @ X1 @ X0))))),
% 0.43/0.41 inference(rectify,[],[f258])).
% 0.43/0.41 thf(f836,plain,(
% 0.43/0.41 (nil_list_a != ((listSl97544552lice_a @ nil_a @ k)))),
% 0.43/0.41 inference(flattening,[],[f351])).
% 0.43/0.41 thf(f920,plain,(
% 0.43/0.41 ! [X0 : list_a,X1 : nat] : ((((ord_less_nat @ (size_size_list_a @ X0) @ X1)) != $true) | (nil_list_a = ((listSl97544552lice_a @ X0 @ X1))))),
% 0.43/0.41 inference(ennf_transformation,[],[f727])).
% 0.43/0.41 thf(f1193,plain,(
% 0.43/0.41 ! [X0 : nat] : (((size_size_list_a @ (sK18 @ X0))) = X0)),
% 0.43/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK0 @ X0)],[f62])).
% 0.43/0.41 thf(f1243,plain,(
% 0.43/0.41 ! [X0 : list_a] : (((((ord_less_nat @ zero_zero_nat @ (size_size_list_a @ X0))) = $true) | (nil_a = X0)) & ((nil_a != X0) | (((ord_less_nat @ zero_zero_nat @ (size_size_list_a @ X0))) != $true)))),
% 0.43/0.41 inference(nnf_transformation,[],[f487])).
% 0.43/0.41 thf(f1253,plain,(
% 0.43/0.41 ! [X0 : list_a] : (((zero_zero_nat = ((size_size_list_a @ X0))) | (nil_a != X0)) & ((nil_a = X0) | (zero_zero_nat != ((size_size_list_a @ X0)))))),
% 0.43/0.41 inference(nnf_transformation,[],[f370])).
% 0.43/0.41 thf(f1254,plain,(
% 0.43/0.41 ! [X0 : list_list_a] : (((zero_zero_nat = ((size_s1427607542list_a @ X0))) | (nil_list_a != X0)) & ((nil_list_a = X0) | (zero_zero_nat != ((size_s1427607542list_a @ X0)))))),
% 0.43/0.41 inference(nnf_transformation,[],[f631])).
% 0.43/0.41 thf(f1287,plain,(
% 0.43/0.41 ( ! [X0 : nat,X1 : list_a] : ((((divide_divide_nat @ (size_size_list_a @ X1) @ X0)) = ((size_s1427607542list_a @ (listSl97544552lice_a @ X1 @ X0))))) )),
% 0.43/0.41 inference(cnf_transformation,[],[f827])).
% 0.43/0.41 thf(f1332,plain,(
% 0.43/0.41 ( ! [X0 : list_a] : ((((listSl97544552lice_a @ X0 @ zero_zero_nat)) = nil_list_a)) )),
% 0.43/0.41 inference(cnf_transformation,[],[f2])).
% 0.43/0.41 thf(f1420,plain,(
% 0.43/0.41 (nil_list_a != ((listSl97544552lice_a @ nil_a @ k)))),
% 0.43/0.41 inference(cnf_transformation,[],[f836])).
% 0.43/0.41 thf(f1585,plain,(
% 0.43/0.41 (zero_zero_nat = ((size_s1427607542list_a @ nil_list_a)))),
% 0.43/0.41 inference(cnf_transformation,[],[f56])).
% 0.43/0.41 thf(f1594,plain,(
% 0.43/0.41 ( ! [X0 : list_a,X1 : nat] : ((((ord_less_nat @ (size_size_list_a @ X0) @ X1)) != $true) | (nil_list_a = ((listSl97544552lice_a @ X0 @ X1)))) )),
% 0.43/0.41 inference(cnf_transformation,[],[f920])).
% 0.43/0.41 thf(f1597,plain,(
% 0.43/0.41 ( ! [X0 : nat] : ((((size_size_list_a @ (sK18 @ X0))) = X0)) )),
% 0.43/0.41 inference(cnf_transformation,[],[f1193])).
% 0.43/0.41 thf(f1704,plain,(
% 0.43/0.41 ( ! [X0 : list_a] : ((((ord_less_nat @ zero_zero_nat @ (size_size_list_a @ X0))) = $true) | (nil_a = X0)) )),
% 0.43/0.41 inference(cnf_transformation,[],[f1243])).
% 0.43/0.41 thf(f1724,plain,(
% 0.43/0.41 ( ! [X0 : list_a] : ((zero_zero_nat = ((size_size_list_a @ X0))) | (nil_a != X0)) )),
% 0.43/0.41 inference(cnf_transformation,[],[f1253])).
% 0.43/0.41 thf(f1725,plain,(
% 0.43/0.41 ( ! [X0 : list_list_a] : ((zero_zero_nat != ((size_s1427607542list_a @ X0))) | (nil_list_a = X0)) )),
% 0.43/0.41 inference(cnf_transformation,[],[f1254])).
% 0.43/0.41 thf(f1856,plain,(
% 0.43/0.41 (zero_zero_nat = ((size_size_list_a @ nil_a)))),
% 0.43/0.41 inference(equality_resolution,[],[f1724])).
% 0.43/0.41 thf(f1968,definition,(
% 0.43/0.41 spl33_4 <=> (zero_zero_nat = ((size_s1427607542list_a @ nil_list_a)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_4])],[avatar_definition])).
% 0.43/0.41 thf(f1970,plain,(
% 0.43/0.41 (zero_zero_nat = ((size_s1427607542list_a @ nil_list_a))) | ~spl33_4),
% 0.43/0.41 inference(avatar_component_clause,[],[f1968])).
% 0.43/0.41 thf(f1971,plain,(
% 0.43/0.41 spl33_4),
% 0.43/0.41 inference(avatar_split_clause,[],[f1585,f1968])).
% 0.43/0.41 thf(f2008,definition,(
% 0.43/0.41 spl33_12 <=> (zero_zero_nat = ((size_size_list_a @ nil_a)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_12])],[avatar_definition])).
% 0.43/0.41 thf(f2010,plain,(
% 0.43/0.41 (zero_zero_nat = ((size_size_list_a @ nil_a))) | ~spl33_12),
% 0.43/0.41 inference(avatar_component_clause,[],[f2008])).
% 0.43/0.41 thf(f2011,plain,(
% 0.43/0.41 spl33_12),
% 0.43/0.41 inference(avatar_split_clause,[],[f1856,f2008])).
% 0.43/0.41 thf(f2078,definition,(
% 0.43/0.41 spl33_26 <=> (nil_list_a = ((listSl97544552lice_a @ nil_a @ k)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_26])],[avatar_definition])).
% 0.43/0.41 thf(f2080,plain,(
% 0.43/0.41 (nil_list_a != ((listSl97544552lice_a @ nil_a @ k))) | spl33_26),
% 0.43/0.41 inference(avatar_component_clause,[],[f2078])).
% 0.43/0.41 thf(f2081,plain,(
% 0.43/0.41 ~spl33_26),
% 0.43/0.41 inference(avatar_split_clause,[],[f1420,f2078])).
% 0.43/0.41 thf(f2191,plain,(
% 0.43/0.41 ( ! [X0 : nat] : ((nil_list_a = ((listSl97544552lice_a @ nil_a @ X0))) | (((ord_less_nat @ zero_zero_nat @ X0)) != $true)) ) | ~spl33_12),
% 0.43/0.41 inference(superposition,[],[f1594,f2010])).
% 0.43/0.41 thf(f2192,plain,(
% 0.43/0.41 ( ! [X0 : list_a] : ((((size_s1427607542list_a @ nil_list_a)) = ((divide_divide_nat @ (size_size_list_a @ X0) @ zero_zero_nat)))) )),
% 0.43/0.41 inference(superposition,[],[f1287,f1332])).
% 0.43/0.41 thf(f2194,plain,(
% 0.43/0.41 ( ! [X0 : list_a,X1 : nat] : ((zero_zero_nat != ((divide_divide_nat @ (size_size_list_a @ X0) @ X1))) | (nil_list_a = ((listSl97544552lice_a @ X0 @ X1)))) )),
% 0.43/0.41 inference(superposition,[],[f1725,f1287])).
% 0.43/0.41 thf(f2195,plain,(
% 0.43/0.41 ( ! [X0 : list_a] : ((zero_zero_nat = ((divide_divide_nat @ (size_size_list_a @ X0) @ zero_zero_nat)))) ) | ~spl33_4),
% 0.43/0.41 inference(forward_demodulation,[],[f2192,f1970])).
% 0.43/0.41 thf(f2196,plain,(
% 0.43/0.41 (zero_zero_nat = ((divide_divide_nat @ zero_zero_nat @ zero_zero_nat))) | (~spl33_4 | ~spl33_12)),
% 0.43/0.41 inference(superposition,[],[f2195,f2010])).
% 0.43/0.41 thf(f2198,definition,(
% 0.43/0.41 spl33_48 <=> (zero_zero_nat = ((divide_divide_nat @ zero_zero_nat @ zero_zero_nat)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_48])],[avatar_definition])).
% 0.43/0.41 thf(f2201,plain,(
% 0.43/0.41 spl33_48 | ~spl33_4 | ~spl33_12),
% 0.43/0.41 inference(avatar_split_clause,[],[f2196,f2008,f1968,f2198])).
% 0.43/0.41 thf(f2205,plain,(
% 0.43/0.41 (nil_list_a != nil_list_a) | ($true != ((ord_less_nat @ zero_zero_nat @ k))) | (~spl33_12 | spl33_26)),
% 0.43/0.41 inference(superposition,[],[f2080,f2191])).
% 0.43/0.41 thf(f2206,plain,(
% 0.43/0.41 ($true != ((ord_less_nat @ zero_zero_nat @ k))) | (~spl33_12 | spl33_26)),
% 0.43/0.41 inference(trivial_inequality_removal,[],[f2205])).
% 0.43/0.41 thf(f2209,definition,(
% 0.43/0.41 spl33_49 <=> ($true = ((ord_less_nat @ zero_zero_nat @ k)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_49])],[avatar_definition])).
% 0.43/0.41 thf(f2211,plain,(
% 0.43/0.41 ($true != ((ord_less_nat @ zero_zero_nat @ k))) | spl33_49),
% 0.43/0.41 inference(avatar_component_clause,[],[f2209])).
% 0.43/0.41 thf(f2212,plain,(
% 0.43/0.41 ~spl33_49 | ~spl33_12 | spl33_26),
% 0.43/0.41 inference(avatar_split_clause,[],[f2206,f2078,f2008,f2209])).
% 0.43/0.41 thf(f2214,plain,(
% 0.43/0.41 ( ! [X0 : nat] : ((nil_list_a = ((listSl97544552lice_a @ nil_a @ X0))) | (zero_zero_nat != ((divide_divide_nat @ zero_zero_nat @ X0)))) ) | ~spl33_12),
% 0.43/0.41 inference(superposition,[],[f2194,f2010])).
% 0.43/0.41 thf(f2223,plain,(
% 0.43/0.41 ( ! [X0 : nat] : ((((ord_less_nat @ zero_zero_nat @ X0)) = $true) | (nil_a = ((sK18 @ X0)))) )),
% 0.43/0.41 inference(superposition,[],[f1704,f1597])).
% 0.43/0.41 thf(f2253,plain,(
% 0.43/0.41 (nil_a = ((sK18 @ k))) | ($true != $true) | spl33_49),
% 0.43/0.41 inference(superposition,[],[f2211,f2223])).
% 0.43/0.41 thf(f2254,plain,(
% 0.43/0.41 (nil_a = ((sK18 @ k))) | spl33_49),
% 0.43/0.41 inference(trivial_inequality_removal,[],[f2253])).
% 0.43/0.41 thf(f2258,definition,(
% 0.43/0.41 spl33_50 <=> (nil_a = ((sK18 @ k)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_50])],[avatar_definition])).
% 0.43/0.41 thf(f2260,plain,(
% 0.43/0.41 (nil_a = ((sK18 @ k))) | ~spl33_50),
% 0.43/0.41 inference(avatar_component_clause,[],[f2258])).
% 0.43/0.41 thf(f2261,plain,(
% 0.43/0.41 spl33_50 | spl33_49),
% 0.43/0.41 inference(avatar_split_clause,[],[f2254,f2209,f2258])).
% 0.43/0.41 thf(f2270,plain,(
% 0.43/0.41 (zero_zero_nat != ((divide_divide_nat @ zero_zero_nat @ k))) | (nil_list_a != nil_list_a) | (~spl33_12 | spl33_26)),
% 0.43/0.41 inference(superposition,[],[f2080,f2214])).
% 0.43/0.41 thf(f2271,plain,(
% 0.43/0.41 (zero_zero_nat != ((divide_divide_nat @ zero_zero_nat @ k))) | (~spl33_12 | spl33_26)),
% 0.43/0.41 inference(trivial_inequality_removal,[],[f2270])).
% 0.43/0.41 thf(f2273,definition,(
% 0.43/0.41 spl33_52 <=> (zero_zero_nat = ((divide_divide_nat @ zero_zero_nat @ k)))),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_52])],[avatar_definition])).
% 0.43/0.41 thf(f2276,plain,(
% 0.43/0.41 ~spl33_52 | ~spl33_12 | spl33_26),
% 0.43/0.41 inference(avatar_split_clause,[],[f2271,f2078,f2008,f2273])).
% 0.43/0.41 thf(f2284,plain,(
% 0.43/0.41 (((size_size_list_a @ nil_a)) = k) | ~spl33_50),
% 0.43/0.41 inference(superposition,[],[f1597,f2260])).
% 0.43/0.41 thf(f2285,plain,(
% 0.43/0.41 (zero_zero_nat = k) | (~spl33_12 | ~spl33_50)),
% 0.43/0.41 inference(forward_demodulation,[],[f2284,f2010])).
% 0.43/0.41 thf(f2287,definition,(
% 0.43/0.41 spl33_53 <=> (zero_zero_nat = k)),
% 0.43/0.41 introduced(definition,[new_symbols(definition,[spl33_53])],[avatar_definition])).
% 0.43/0.41 thf(f2290,plain,(
% 0.43/0.41 spl33_53 | ~spl33_12 | ~spl33_50),
% 0.43/0.41 inference(avatar_split_clause,[],[f2285,f2258,f2008,f2287])).
% 0.43/0.41 thf(f2291,definition,(
% 0.43/0.41 (zero_zero_nat != k) | (zero_zero_nat != ((divide_divide_nat @ zero_zero_nat @ zero_zero_nat))) | (zero_zero_nat = ((divide_divide_nat @ zero_zero_nat @ k)))),
% 0.43/0.41 introduced(theory,[theory_tautology_sat_conflict])).
% 0.43/0.41 cnf(s4, plain, spl33_4, inference(sat_conversion,[],[f1971])).
% 0.43/0.41 cnf(s13, plain, spl33_12, inference(sat_conversion,[],[f2011])).
% 0.43/0.41 cnf(s34, plain, ~spl33_26, inference(sat_conversion,[],[f2081])).
% 0.43/0.41 cnf(s73, plain, ~spl33_4 | ~spl33_12 | spl33_48, inference(sat_conversion,[],[f2201])).
% 0.43/0.41 cnf(s74, plain, ~spl33_12 | spl33_26 | ~spl33_49, inference(sat_conversion,[],[f2212])).
% 0.43/0.41 cnf(s75, plain, spl33_49 | spl33_50, inference(sat_conversion,[],[f2261])).
% 0.43/0.41 cnf(s78, plain, ~spl33_12 | spl33_26 | ~spl33_52, inference(sat_conversion,[],[f2276])).
% 0.43/0.41 cnf(s79, plain, ~spl33_12 | ~spl33_50 | spl33_53, inference(sat_conversion,[],[f2290])).
% 0.43/0.41 cnf(s80, plain, ~spl33_48 | spl33_52 | ~spl33_53, inference(sat_conversion,[],[f2291])).
% 0.43/0.41 cnf(s81, plain, ~spl33_52, inference(rat,[],[s78,s34,s13])).
% 0.43/0.41 cnf(s82, plain, ~spl33_49, inference(rat,[],[s74,s34,s13])).
% 0.43/0.41 cnf(s83, plain, spl33_50, inference(rat,[],[s75,s82])).
% 0.43/0.41 cnf(s84, plain, spl33_53, inference(rat,[],[s79,s13,s83])).
% 0.43/0.41 cnf(s85, plain, ~spl33_48, inference(rat,[],[s80,s81,s84])).
% 0.43/0.41 cnf(s86, plain, ~spl33_4, inference(rat,[],[s73,s13,s85])).
% 0.43/0.41 cnf(s87, plain, $false, inference(rat,[],[s4,s86])).
% 0.43/0.41 thf(f2292,plain,(
% 0.43/0.41 $false),
% 0.43/0.41 inference(avatar_sat_refutation,[],[s87])).
% 0.43/0.41 % SZS output end Proof for theBenchmark
% 0.43/0.41 % (1270154)------------------------------
% 0.43/0.41 % (1270154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.41 % (1270154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.41 % (1270154)CaDiCaL version: 2.1.3
% 0.43/0.41 % (1270154)Termination reason: Refutation
% 0.43/0.41 % (1270154)Time elapsed: 0.060 s
% 0.43/0.41 % (1270154)Peak memory usage: 14 MB
% 0.43/0.41 % (1270154)Instructions burned: 119 (million)
% 0.43/0.41 % (1270146)Success in time 0.114 s
% 0.43/0.41 % Vampire exiting
%------------------------------------------------------------------------------