%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP409_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:39:35 AM UTC 2026
% Result : Theorem 1.60s 0.90s
% Output : Refutation 1.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP409_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 13:03:30 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.60/0.90 % (3553347)Will run a generic schedule for satisfiability detection.
% 1.60/0.90 % (3553372)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4191093555:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.60/0.90 % (3553368)% WARNING: option uhcvi not known.
% 1.60/0.90 % (3553368)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2832903975:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.60/0.90 % (3553370)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1154447143:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.60/0.90 % (3553367)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=184369218_2999 on theBenchmark for (2999ds/0Mi)
% 1.60/0.90 % (3553371)dis+10_1_sil=32000:sp=arity:random_seed=1217184733:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.60/0.90 % (3553373)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2661457765:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.60/0.90 % (3553374)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2218799988:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.60/0.90 % (3553372)Instruction limit reached!
% 1.60/0.90 % (3553372)------------------------------
% 1.60/0.90 % (3553372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553372)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553372)Termination reason: Instruction limit
% 1.60/0.90 % (3553372)Termination phase: Saturation
% 1.60/0.90 % (3553372)Time elapsed: 0.031 s
% 1.60/0.90 % (3553372)Peak memory usage: 13 MB
% 1.60/0.90 % (3553372)Instructions burned: 119 (million)
% 1.60/0.90 % (3553367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.60/0.90 % (3553367)Terminated due to inappropriate strategy.
% 1.60/0.90 % (3553367)------------------------------
% 1.60/0.90 % (3553367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553367)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553367)Termination reason: Inappropriate
% 1.60/0.90 % (3553367)Time elapsed: 0.034 s
% 1.60/0.90 % (3553367)Peak memory usage: 12 MB
% 1.60/0.90 % (3553367)Instructions burned: 74 (million)
% 1.60/0.90 % (3553367)------------------------------
% 1.60/0.90 % (3553367)------------------------------
% 1.60/0.90 % (3553397)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4161132907:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.60/0.90 % (3553371)Instruction limit reached!
% 1.60/0.90 % (3553371)------------------------------
% 1.60/0.90 % (3553371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553371)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553371)Termination reason: Instruction limit
% 1.60/0.90 % (3553371)Termination phase: Saturation
% 1.60/0.90 % (3553371)Time elapsed: 0.051 s
% 1.60/0.90 % (3553371)Peak memory usage: 13 MB
% 1.60/0.90 % (3553371)Instructions burned: 103 (million)
% 1.60/0.90 % (3553404)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=529876226:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.60/0.90 % (3553374)Instruction limit reached!
% 1.60/0.90 % (3553374)------------------------------
% 1.60/0.90 % (3553374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553374)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553374)Termination reason: Instruction limit
% 1.60/0.90 % (3553374)Termination phase: Saturation
% 1.60/0.90 % (3553374)Time elapsed: 0.070 s
% 1.60/0.90 % (3553374)Peak memory usage: 14 MB
% 1.60/0.90 % (3553374)Instructions burned: 159 (million)
% 1.60/0.90 % (3553373)Instruction limit reached!
% 1.60/0.90 % (3553373)------------------------------
% 1.60/0.90 % (3553373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553373)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553373)Termination reason: Instruction limit
% 1.60/0.90 % (3553373)Termination phase: Saturation
% 1.60/0.90 % (3553373)Time elapsed: 0.071 s
% 1.60/0.90 % (3553373)Peak memory usage: 14 MB
% 1.60/0.90 % (3553373)Instructions burned: 131 (million)
% 1.60/0.90 % (3553415)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2799442306:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.60/0.90 % (3553397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.60/0.90 % (3553397)Terminated due to inappropriate strategy.
% 1.60/0.90 % (3553397)------------------------------
% 1.60/0.90 % (3553397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553397)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553397)Termination reason: Inappropriate
% 1.60/0.90 % (3553397)Time elapsed: 0.036 s
% 1.60/0.90 % (3553397)Peak memory usage: 12 MB
% 1.60/0.90 % (3553397)Instructions burned: 67 (million)
% 1.60/0.90 % (3553397)------------------------------
% 1.60/0.90 % (3553397)------------------------------
% 1.60/0.90 % (3553426)ott-21_1_sil=16000:fs=off:random_seed=2406895282:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.60/0.90 % (3553428)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3247428645:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.60/0.90 % (3553432)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3029419441:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.60/0.90 % (3553404)Instruction limit reached!
% 1.60/0.90 % (3553404)------------------------------
% 1.60/0.90 % (3553404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553404)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553404)Termination reason: Instruction limit
% 1.60/0.90 % (3553404)Termination phase: Saturation
% 1.60/0.90 % (3553404)Time elapsed: 0.069 s
% 1.60/0.90 % (3553404)Peak memory usage: 14 MB
% 1.60/0.90 % (3553404)Instructions burned: 132 (million)
% 1.60/0.90 % (3553426)Instruction limit reached!
% 1.60/0.90 % (3553426)------------------------------
% 1.60/0.90 % (3553426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553426)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553426)Termination reason: Instruction limit
% 1.60/0.90 % (3553426)Termination phase: Saturation
% 1.60/0.90 % (3553426)Time elapsed: 0.045 s
% 1.60/0.90 % (3553426)Peak memory usage: 14 MB
% 1.60/0.90 % (3553426)Instructions burned: 184 (million)
% 1.60/0.90 % (3553443)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1731570937:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.60/0.90 % (3553432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.60/0.90 % (3553432)Terminated due to inappropriate strategy.
% 1.60/0.90 % (3553432)------------------------------
% 1.60/0.90 % (3553432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553432)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553432)Termination reason: Inappropriate
% 1.60/0.90 % (3553432)Time elapsed: 0.027 s
% 1.60/0.90 % (3553432)Peak memory usage: 11 MB
% 1.60/0.90 % (3553432)Instructions burned: 52 (million)
% 1.60/0.90 % (3553432)------------------------------
% 1.60/0.90 % (3553432)------------------------------
% 1.60/0.90 % (3553441)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=24570925:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.60/0.90 % (3553443)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.60/0.90 % (3553443)Terminated due to inappropriate strategy.
% 1.60/0.90 % (3553443)------------------------------
% 1.60/0.90 % (3553443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553443)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553443)Termination reason: Inappropriate
% 1.60/0.90 % (3553443)Time elapsed: 0.016 s
% 1.60/0.90 % (3553443)Peak memory usage: 12 MB
% 1.60/0.90 % (3553443)Instructions burned: 68 (million)
% 1.60/0.90 % (3553443)------------------------------
% 1.60/0.90 % (3553443)------------------------------
% 1.60/0.90 % (3553449)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1597442198:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 1.60/0.90 % (3553456)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3226704587:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 1.60/0.90 % (3553428)Instruction limit reached!
% 1.60/0.90 % (3553428)------------------------------
% 1.60/0.90 % (3553428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.90 % (3553428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.90 % (3553428)CaDiCaL version: 2.1.3
% 1.60/0.90 % (3553428)Termination reason: Instruction limit
% 1.60/0.90 % (3553428)Termination phase: Saturation
% 1.60/0.90 % (3553428)Time elapsed: 0.293 s
% 1.60/0.90 % (3553428)Peak memory usage: 15 MB
% 1.60/0.90 % (3553428)Instructions burned: 478 (million)
% 1.60/0.90 % (3553368) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3553347-3553368"...
% 1.60/0.90 % (3553478)fmb+10_1_sil=64000:random_seed=1742564864:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 1.60/0.90 % (3553368)...printing done.
% 1.60/0.90 % (3553368)Refutation found. Thanks to Tanya!
% 1.60/0.90 % SZS status Theorem for theBenchmark
% 1.60/0.90 % SZS output start Proof for theBenchmark
% 1.60/0.90 tff(type_def_5, type, 'Int_bool_fun$': $tType).
% 1.60/0.90 tff(type_def_6, type, 'Nat_nat_bool_fun_fun$': $tType).
% 1.60/0.90 tff(type_def_7, type, 'Int_int_fun$': $tType).
% 1.60/0.90 tff(type_def_8, type, 'Nat_nat_fun$': $tType).
% 1.60/0.90 tff(type_def_9, type, 'Int_nat_fun$': $tType).
% 1.60/0.90 tff(type_def_10, type, 'Nat$': $tType).
% 1.60/0.90 tff(type_def_11, type, tlbool: $tType).
% 1.60/0.90 tff(type_def_12, type, 'Int_int_bool_fun_fun$': $tType).
% 1.60/0.90 tff(type_def_13, type, 'Nat_bool_fun$': $tType).
% 1.60/0.90 tff(type_def_14, type, 'Nat_int_fun$': $tType).
% 1.60/0.90 tff(func_def_0, type, 'n_0$': 'Nat$').
% 1.60/0.90 tff(func_def_1, type, 'fun_app$d': ('Nat_nat_bool_fun_fun$' * 'Nat$') > 'Nat_bool_fun$').
% 1.60/0.90 tff(func_def_2, type, 'uu$': 'Int_int_bool_fun_fun$').
% 1.60/0.90 tff(func_def_3, type, 'zero$': 'Nat$').
% 1.60/0.90 tff(func_def_4, type, 'of_nat$a': 'Nat_nat_fun$').
% 1.60/0.90 tff(func_def_5, type, 'nat$': 'Int_nat_fun$').
% 1.60/0.90 tff(func_def_6, type, 'times$a': 'Nat$' > 'Nat_nat_fun$').
% 1.60/0.90 tff(func_def_7, type, 'of_nat$': 'Nat_int_fun$').
% 1.60/0.90 tff(func_def_8, type, 'fun_app$a': ('Int_int_bool_fun_fun$' * $int) > 'Int_bool_fun$').
% 1.60/0.90 tff(func_def_9, type, 'fun_app$f': ('Int_nat_fun$' * $int) > 'Nat$').
% 1.60/0.90 tff(func_def_10, type, 'of_int$': 'Int_int_fun$').
% 1.60/0.90 tff(func_def_11, type, 'times$': $int > 'Int_int_fun$').
% 1.60/0.90 tff(func_def_12, type, 'less$': 'Nat_nat_bool_fun_fun$').
% 1.60/0.90 tff(func_def_13, type, tltrue: tlbool).
% 1.60/0.90 tff(func_def_14, type, 'greatest$': 'Int_bool_fun$' > $int).
% 1.60/0.90 tff(func_def_15, type, 'one$': 'Nat$').
% 1.60/0.90 tff(func_def_16, type, 'fun_app$e': ('Nat_nat_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_17, type, 'fun_app$g': ('Int_int_fun$' * $int) > $int).
% 1.60/0.90 tff(func_def_18, type, 'less_eq$': 'Nat_nat_bool_fun_fun$').
% 1.60/0.90 tff(func_def_19, type, 'p$': 'Nat_bool_fun$').
% 1.60/0.90 tff(func_def_20, type, tlfalse: tlbool).
% 1.60/0.90 tff(func_def_21, type, 'greatest$a': 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_22, type, 'fun_app$b': ('Nat_int_fun$' * 'Nat$') > $int).
% 1.60/0.90 tff(func_def_28, type, sK0: 'Nat$').
% 1.60/0.90 tff(func_def_29, type, sK1: 'Nat$').
% 1.60/0.90 tff(func_def_30, type, sK2: 'Nat$').
% 1.60/0.90 tff(func_def_31, type, sK3: 'Nat$').
% 1.60/0.90 tff(func_def_32, type, sK4: 'Nat$').
% 1.60/0.90 tff(func_def_33, type, sK5: 'Nat$').
% 1.60/0.90 tff(func_def_34, type, sK6: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_35, type, sK7: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_36, type, sK8: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_37, type, sK9: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_38, type, sK10: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_39, type, sK11: $int > $int).
% 1.60/0.90 tff(func_def_40, type, sK12: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_41, type, sK13: $int > $int).
% 1.60/0.90 tff(func_def_42, type, sK14: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_43, type, sK15: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_44, type, sK16: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_45, type, sK17: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_46, type, sK18: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_47, type, sK19: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_48, type, sK20: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_49, type, sK21: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_50, type, sK22: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_51, type, sK23: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_52, type, sK24: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_53, type, sK25: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_54, type, sK26: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_55, type, sK27: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_56, type, sK28: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_57, type, sK29: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_58, type, sK30: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_59, type, sK31: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_60, type, sK32: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_61, type, sK33: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_62, type, sK34: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_63, type, sK35: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_64, type, sK36: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_65, type, sK37: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_66, type, sK38: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_67, type, sK39: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_68, type, sK40: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_69, type, sK41: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_70, type, sK42: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_71, type, sK43: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_72, type, sK44: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_73, type, sK45: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_74, type, sK46: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_75, type, sK47: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_76, type, sK48: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_77, type, sK49: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_78, type, sK50: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_79, type, sK51: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_80, type, sK52: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_81, type, sK53: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_82, type, sK54: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_83, type, sK55: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_84, type, sK56: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_85, type, sK57: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_86, type, sK58: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_87, type, sK59: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_88, type, sK60: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_89, type, sK61: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_90, type, sK62: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_91, type, sK63: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_92, type, sK64: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_93, type, sK65: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_94, type, sK66: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_95, type, sK67: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_96, type, sK68: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_97, type, sK69: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_98, type, sK70: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_99, type, sK71: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_100, type, sK72: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_101, type, sK73: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_102, type, sK74: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_103, type, sK75: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_104, type, sK76: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_105, type, sK77: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_106, type, sK78: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_107, type, sK79: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_108, type, sK80: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_109, type, sK81: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_110, type, sK82: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_111, type, sK83: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_112, type, sK84: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_113, type, sK85: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_114, type, sK86: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_115, type, sK87: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_116, type, sK88: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_117, type, sK89: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_118, type, sK90: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_119, type, sK91: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_120, type, sK92: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_121, type, sK93: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_122, type, sK94: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_123, type, sK95: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_124, type, sK96: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_125, type, sK97: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_126, type, sK98: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_127, type, sK99: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_128, type, sK100: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_129, type, sK101: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_130, type, sK102: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_131, type, sK103: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_132, type, sK104: ('Nat$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_133, type, sK105: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_134, type, sK106: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_135, type, sK107: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_136, type, sK108: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_137, type, sK109: ('Nat$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_138, type, sK110: ('Nat$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_139, type, sK111: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_140, type, sK112: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_141, type, sK113: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_142, type, sK114: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_143, type, sK115: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_144, type, sK116: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_145, type, sK117: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_146, type, sK118: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_147, type, sK119: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_148, type, sK120: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_149, type, sK121: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_150, type, sK122: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_151, type, sK123: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_152, type, sK124: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_153, type, sK125: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_154, type, sK126: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_155, type, sK127: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_156, type, sK128: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_157, type, sK129: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_158, type, sK130: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_159, type, sK131: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_160, type, sK132: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_161, type, sK133: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_162, type, sK134: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_163, type, sK135: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_164, type, sK136: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_165, type, sK137: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_166, type, sK138: 'Nat_int_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_167, type, sK139: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_168, type, sK140: 'Int_nat_fun$' > $int).
% 1.60/0.90 tff(func_def_169, type, sK141: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_170, type, sK142: 'Nat_nat_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_171, type, sK143: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_172, type, sK144: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_173, type, sK145: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_174, type, sK146: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_175, type, sK147: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_176, type, sK148: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_177, type, sK149: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_178, type, sK150: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_179, type, sK151: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_180, type, sK152: 'Int_int_bool_fun_fun$' > $int).
% 1.60/0.90 tff(func_def_181, type, sK158: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_182, type, sK159: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_183, type, sK160: ('Nat$' * 'Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_184, type, sK161: ('Nat$' * 'Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_185, type, sK162: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_186, type, sK163: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_187, type, sK164: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_188, type, sK165: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_189, type, sK166: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_190, type, sK167: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_191, type, sK168: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_192, type, sK169: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_193, type, sK170: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_194, type, sK171: ('Int_bool_fun$' * $int) > $int).
% 1.60/0.90 tff(func_def_195, type, sK172: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_196, type, sK173: ('Int_bool_fun$' * 'Int_bool_fun$') > $int).
% 1.60/0.90 tff(func_def_197, type, sK174: ('Int_bool_fun$' * $int) > $int).
% 1.60/0.90 tff(func_def_198, type, sK175: ('Nat_bool_fun$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_199, type, sK176: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_200, type, sK177: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_201, type, sK178: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_202, type, sK179: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_203, type, sK180: 'Int_int_fun$' > $int).
% 1.60/0.90 tff(func_def_204, type, sK181: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_205, type, sK182: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_206, type, sK183: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_207, type, sK184: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_208, type, sK185: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_209, type, sK186: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_210, type, sK187: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_211, type, sK188: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_212, type, sK189: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_213, type, sK190: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_214, type, sK191: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_215, type, sK192: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_216, type, sK193: 'Nat_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_217, type, sK194: ('Nat$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_218, type, sK195: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_219, type, sK196: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_220, type, sK197: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_221, type, sK198: 'Nat$' > 'Nat$').
% 1.60/0.90 tff(func_def_222, type, sK199: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_223, type, sK200: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 1.60/0.90 tff(func_def_224, type, sK201: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 1.60/0.90 tff(func_def_225, type, sK202: $int > 'Nat$').
% 1.60/0.90 tff(func_def_226, type, sK203: $int > 'Nat$').
% 1.60/0.90 tff(func_def_227, type, sK204: $int > 'Nat$').
% 1.60/0.90 tff(func_def_228, type, sK205: $int > 'Nat$').
% 1.60/0.90 tff(func_def_229, type, sK206: $int > 'Nat$').
% 1.60/0.90 tff(func_def_230, type, sK207: 'Int_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_231, type, sK208: 'Int_bool_fun$' > 'Nat$').
% 1.60/0.90 tff(func_def_232, type, sK209: $int > 'Nat$').
% 1.60/0.90 tff(func_def_233, type, sK210: $int > 'Nat$').
% 1.60/0.90 tff(func_def_234, type, sK211: $int > 'Nat$').
% 1.60/0.90 tff(func_def_235, type, sK212: $int > 'Nat$').
% 1.60/0.90 tff(func_def_236, type, sK213: $int > 'Nat$').
% 1.60/0.90 tff(func_def_237, type, sK214: $int > 'Nat$').
% 1.60/0.90 tff(func_def_238, type, sK215: $int > 'Nat$').
% 1.60/0.90 tff(func_def_239, type, sK216: ('Nat_bool_fun$' * $int) > 'Nat$').
% 1.60/0.90 tff(func_def_240, type, sK217: $int > 'Nat$').
% 1.60/0.90 tff(func_def_241, type, sK218: $int > 'Nat$').
% 1.60/0.90 tff(func_def_242, type, sK220: $int > 'Nat$').
% 1.60/0.90 tff(pred_def_1, type, 'fun_app$c': ('Nat_bool_fun$' * 'Nat$') > $o).
% 1.60/0.90 tff(pred_def_2, type, 'fun_app$': ('Int_bool_fun$' * $int) > $o).
% 1.60/0.90 tff(pred_def_3, type, 'antimono$': 'Nat_int_fun$' > $o).
% 1.60/0.90 tff(pred_def_4, type, 'antimono$a': 'Int_int_fun$' > $o).
% 1.60/0.90 tff(pred_def_7, type, sP153: ($int * $int * $int) > $o).
% 1.60/0.90 tff(pred_def_8, type, sP154: ($int * $int * $int) > $o).
% 1.60/0.90 tff(pred_def_9, type, sP155: ($int * $int * $int) > $o).
% 1.60/0.90 tff(pred_def_10, type, sP156: ($int * $int * $int) > $o).
% 1.60/0.90 tff(f2,conjecture,(
% 1.60/0.90 ! [X0 : 'Nat$'] : ($lesseq('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X0)) => 'fun_app$c'('p$',X0)) <=> ('fun_app$c'('p$','n_0$') & ! [X0 : 'Nat$'] : ($lesseq($sum('fun_app$b'('of_nat$','n_0$'),1),'fun_app$b'('of_nat$',X0)) => 'fun_app$c'('p$',X0)))),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture1)).
% 1.60/0.90 tff(f3,negated_conjecture,(
% 1.60/0.90 ~(! [X0 : 'Nat$'] : ($lesseq('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X0)) => 'fun_app$c'('p$',X0)) <=> ('fun_app$c'('p$','n_0$') & ! [X0 : 'Nat$'] : ($lesseq($sum('fun_app$b'('of_nat$','n_0$'),1),'fun_app$b'('of_nat$',X0)) => 'fun_app$c'('p$',X0))))),
% 1.60/0.90 inference(negated_conjecture,[status(cth)],[f2])).
% 1.60/0.90 tff(f6,axiom,(
% 1.60/0.90 ! [X0 : 'Nat$'] : ($lesseq('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X0)) => 'fun_app$c'('p$',X0)) <=> ! [X0 : 'Nat$'] : (('fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$','n_0$') | $less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X0))) => 'fun_app$c'('p$',X0))),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom4)).
% 1.60/0.90 tff(f95,axiom,(
% 1.60/0.90 ! [X0 : $int,X1 : $int] : ($less(X0,X1) => ~$less(X1,X0))),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom93)).
% 1.60/0.90 tff(f131,axiom,(
% 1.60/0.90 ! [X0 : $int,X1 : $int,X2 : $int] : (($less(X0,X1) & $lesseq(X1,X2)) => $less(X0,X2))),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom129)).
% 1.60/0.90 tff(f186,axiom,(
% 1.60/0.90 ! [X0 : 'Nat$',X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$',X1)) => ($less('fun_app$b'('of_nat$',X0),$sum('fun_app$b'('of_nat$',X1),1)) <=> 'fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$',X1)))),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom184)).
% 1.60/0.90 tff(f615,axiom,(
% 1.60/0.90 ! [X0 : 'Nat$'] : 'fun_app$f'('nat$','fun_app$b'('of_nat$',X0)) = X0),
% 1.60/0.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom613)).
% 1.60/0.90 tff(f619,plain,(
% 1.60/0.90 ~(! [X0 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) => 'fun_app$c'('p$',X0)) <=> ('fun_app$c'('p$','n_0$') & ! [X0 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),$sum('fun_app$b'('of_nat$','n_0$'),1)) => 'fun_app$c'('p$',X0))))),
% 1.60/0.90 inference(theory_normalization,[],[f3])).
% 1.60/0.90 tff(f621,plain,(
% 1.60/0.90 ! [X0 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) => 'fun_app$c'('p$',X0)) <=> ! [X0 : 'Nat$'] : (('fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$','n_0$') | $less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X0))) => 'fun_app$c'('p$',X0))),
% 1.60/0.90 inference(theory_normalization,[],[f6])).
% 1.60/0.90 tff(f645,plain,(
% 1.60/0.90 ! [X0 : $int,X1 : $int,X2 : $int] : (($less(X0,X1) & ~$less(X2,X1)) => $less(X0,X2))),
% 1.60/0.90 inference(theory_normalization,[],[f131])).
% 1.60/0.90 tff(f840,definition,(
% 1.60/0.90 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 1.60/0.90 introduced(theory,[tha_commutativity])).
% 1.60/0.90 tff(f845,definition,(
% 1.60/0.90 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 1.60/0.90 introduced(theory,[tha_non-reflexivity])).
% 1.60/0.90 tff(f847,definition,(
% 1.60/0.90 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 1.60/0.90 introduced(theory,[tha_order_totality])).
% 1.60/0.90 tff(f849,definition,(
% 1.60/0.90 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 1.60/0.90 introduced(theory,[tha_order_plus_one_dichotomy])).
% 1.60/0.90 tff(f858,plain,(
% 1.60/0.90 ~(! [X0 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) => 'fun_app$c'('p$',X0)) <=> ('fun_app$c'('p$','n_0$') & ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1)) => 'fun_app$c'('p$',X1))))),
% 1.60/0.90 inference(rectify,[],[f619])).
% 1.60/0.90 tff(f860,plain,(
% 1.60/0.90 ! [X0 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) => 'fun_app$c'('p$',X0)) <=> ! [X1 : 'Nat$'] : (('fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',X1) | $less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1))) => 'fun_app$c'('p$',X1))),
% 1.60/0.90 inference(rectify,[],[f621])).
% 1.60/0.90 tff(f884,plain,(
% 1.60/0.90 ! [X0 : 'Nat$'] : ('fun_app$c'('p$',X0) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$'))) <~> ('fun_app$c'('p$','n_0$') & ! [X1 : 'Nat$'] : ('fun_app$c'('p$',X1) | $less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1))))),
% 1.60/0.90 inference(ennf_transformation,[],[f858])).
% 1.60/0.90 tff(f886,plain,(
% 1.60/0.90 ! [X0 : 'Nat$'] : ('fun_app$c'('p$',X0) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$'))) <=> ! [X1 : 'Nat$'] : ('fun_app$c'('p$',X1) | ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) & ~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1))))),
% 1.60/0.90 inference(ennf_transformation,[],[f860])).
% 1.60/0.90 tff(f999,plain,(
% 1.60/0.90 ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | ~$less(X0,X1))),
% 1.60/0.90 inference(ennf_transformation,[],[f95])).
% 1.60/0.90 tff(f1052,plain,(
% 1.60/0.90 ! [X0 : $int,X1 : $int,X2 : $int] : ($less(X0,X2) | (~$less(X0,X1) | $less(X2,X1)))),
% 1.60/0.90 inference(ennf_transformation,[],[f645])).
% 1.60/0.90 tff(f1053,plain,(
% 1.60/0.90 ! [X0 : $int,X1 : $int,X2 : $int] : ($less(X0,X2) | ~$less(X0,X1) | $less(X2,X1))),
% 1.60/0.90 inference(flattening,[],[f1052])).
% 1.60/0.90 tff(f1098,plain,(
% 1.60/0.90 ! [X0 : 'Nat$',X1 : 'Nat$'] : (($less('fun_app$b'('of_nat$',X0),$sum('fun_app$b'('of_nat$',X1),1)) <=> 'fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$',X1)) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$',X1)))),
% 1.60/0.90 inference(ennf_transformation,[],[f186])).
% 1.60/0.90 tff(f1484,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | ~'fun_app$c'('p$','n_0$') | ~'fun_app$c'('p$',sK0)),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1485,plain,(
% 1.60/0.90 ~'fun_app$c'('p$',sK1) | ~'fun_app$c'('p$','n_0$') | ~'fun_app$c'('p$',sK0)),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1486,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | ~'fun_app$c'('p$','n_0$') | ~$less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1487,plain,(
% 1.60/0.90 ~'fun_app$c'('p$',sK1) | ~'fun_app$c'('p$','n_0$') | ~$less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1488,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$',X1 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | 'fun_app$c'('p$',X1) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) | 'fun_app$c'('p$',X0)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1489,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$'] : ('fun_app$c'('p$','n_0$') | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) | 'fun_app$c'('p$',X0)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f884])).
% 1.60/0.90 tff(f1500,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1)) | 'fun_app$c'('p$',X1) | ~$less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$'))) )),
% 1.60/0.90 inference(cnf_transformation,[],[f886])).
% 1.60/0.90 tff(f1501,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) | 'fun_app$c'('p$',X1) | ~$less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$'))) )),
% 1.60/0.90 inference(cnf_transformation,[],[f886])).
% 1.60/0.90 tff(f1502,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1)) | 'fun_app$c'('p$',X1) | ~'fun_app$c'('p$',sK4)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f886])).
% 1.60/0.90 tff(f1503,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) | 'fun_app$c'('p$',X1) | ~'fun_app$c'('p$',sK4)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f886])).
% 1.60/0.90 tff(f1638,plain,(
% 1.60/0.90 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f999])).
% 1.60/0.90 tff(f1691,plain,(
% 1.60/0.90 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less(X2,X1) | $less(X0,X2)) )),
% 1.60/0.90 inference(cnf_transformation,[],[f1053])).
% 1.60/0.90 tff(f1782,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$',X1 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$',X1)) | 'fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$',X1) | ~$less('fun_app$b'('of_nat$',X0),$sum('fun_app$b'('of_nat$',X1),1))) )),
% 1.60/0.90 inference(cnf_transformation,[],[f1098])).
% 1.60/0.90 tff(f2552,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$'] : ('fun_app$f'('nat$','fun_app$b'('of_nat$',X0)) = X0) )),
% 1.60/0.90 inference(cnf_transformation,[],[f615])).
% 1.60/0.90 tff(f2697,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$'] : (~'fun_app$c'('p$','n_0$') | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) | ~'fun_app$c'('p$',X0)) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1489])).
% 1.60/0.90 tff(f2698,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$',X1 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | ~'fun_app$c'('p$',X1) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) | ~'fun_app$c'('p$',X0)) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1488])).
% 1.60/0.90 tff(f2699,plain,(
% 1.60/0.90 'fun_app$c'('p$',sK1) | 'fun_app$c'('p$','n_0$') | ~$less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1487])).
% 1.60/0.90 tff(f2700,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | 'fun_app$c'('p$','n_0$') | ~$less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1486])).
% 1.60/0.90 tff(f2701,plain,(
% 1.60/0.90 'fun_app$c'('p$',sK1) | 'fun_app$c'('p$','n_0$') | 'fun_app$c'('p$',sK0)),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1485])).
% 1.60/0.90 tff(f2702,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | 'fun_app$c'('p$','n_0$') | 'fun_app$c'('p$',sK0)),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1484])).
% 1.60/0.90 tff(f2713,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) | ~'fun_app$c'('p$',X1) | 'fun_app$c'('p$',sK4)) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1503])).
% 1.60/0.90 tff(f2714,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1)) | ~'fun_app$c'('p$',X1) | 'fun_app$c'('p$',sK4)) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1502])).
% 1.60/0.90 tff(f2715,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) | ~'fun_app$c'('p$',X1) | ~$less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$'))) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1501])).
% 1.60/0.90 tff(f2716,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1)) | ~'fun_app$c'('p$',X1) | ~$less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$'))) )),
% 1.60/0.90 inference(consistent_polarity_flipping,[],[f1500])).
% 1.60/0.90 tff(f3157,definition,(
% 1.60/0.90 spl221_21 <=> ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_21])],[avatar_definition])).
% 1.60/0.90 tff(f3158,plain,(
% 1.60/0.90 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | ~$less(X0,X1)) ) | ~spl221_21),
% 1.60/0.90 inference(avatar_component_clause,[],[f3157])).
% 1.60/0.90 tff(f3164,plain,(
% 1.60/0.90 spl221_21),
% 1.60/0.90 inference(avatar_split_clause,[],[f1638,f3157])).
% 1.60/0.90 tff(f3167,definition,(
% 1.60/0.90 spl221_23 <=> $less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_23])],[avatar_definition])).
% 1.60/0.90 tff(f3171,definition,(
% 1.60/0.90 spl221_24 <=> ! [X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1)) | ~'fun_app$c'('p$',X1))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_24])],[avatar_definition])).
% 1.60/0.90 tff(f3172,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~'fun_app$c'('p$',X1) | ~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',X1))) ) | ~spl221_24),
% 1.60/0.90 inference(avatar_component_clause,[],[f3171])).
% 1.60/0.90 tff(f3173,plain,(
% 1.60/0.90 ~spl221_23 | spl221_24),
% 1.60/0.90 inference(avatar_split_clause,[],[f2716,f3171,f3167])).
% 1.60/0.90 tff(f3175,definition,(
% 1.60/0.90 spl221_25 <=> ! [X1 : 'Nat$'] : ('fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1) | ~'fun_app$c'('p$',X1))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_25])],[avatar_definition])).
% 1.60/0.90 tff(f3176,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : (~'fun_app$c'('p$',X1) | 'fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',X1)) ) | ~spl221_25),
% 1.60/0.90 inference(avatar_component_clause,[],[f3175])).
% 1.60/0.90 tff(f3177,plain,(
% 1.60/0.90 ~spl221_23 | spl221_25),
% 1.60/0.90 inference(avatar_split_clause,[],[f2715,f3175,f3167])).
% 1.60/0.90 tff(f3179,definition,(
% 1.60/0.90 spl221_26 <=> 'fun_app$c'('p$',sK4)),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_26])],[avatar_definition])).
% 1.60/0.90 tff(f3181,plain,(
% 1.60/0.90 'fun_app$c'('p$',sK4) | ~spl221_26),
% 1.60/0.90 inference(avatar_component_clause,[],[f3179])).
% 1.60/0.90 tff(f3182,plain,(
% 1.60/0.90 spl221_26 | spl221_24),
% 1.60/0.90 inference(avatar_split_clause,[],[f2714,f3171,f3179])).
% 1.60/0.90 tff(f3183,plain,(
% 1.60/0.90 spl221_26 | spl221_25),
% 1.60/0.90 inference(avatar_split_clause,[],[f2713,f3175,f3179])).
% 1.60/0.90 tff(f3185,definition,(
% 1.60/0.90 spl221_27 <=> ! [X0 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$')) | ~'fun_app$c'('p$',X0))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_27])],[avatar_definition])).
% 1.60/0.90 tff(f3186,plain,(
% 1.60/0.90 ( ! [X0 : 'Nat$'] : (~'fun_app$c'('p$',X0) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$','n_0$'))) ) | ~spl221_27),
% 1.60/0.90 inference(avatar_component_clause,[],[f3185])).
% 1.60/0.90 tff(f3207,definition,(
% 1.60/0.90 spl221_32 <=> 'fun_app$c'('p$','n_0$')),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_32])],[avatar_definition])).
% 1.60/0.90 tff(f3209,plain,(
% 1.60/0.90 'fun_app$c'('p$','n_0$') | ~spl221_32),
% 1.60/0.90 inference(avatar_component_clause,[],[f3207])).
% 1.60/0.90 tff(f3234,definition,(
% 1.60/0.90 spl221_37 <=> 'fun_app$c'('p$',sK0)),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_37])],[avatar_definition])).
% 1.60/0.90 tff(f3236,plain,(
% 1.60/0.90 'fun_app$c'('p$',sK0) | ~spl221_37),
% 1.60/0.90 inference(avatar_component_clause,[],[f3234])).
% 1.60/0.90 tff(f3238,definition,(
% 1.60/0.90 spl221_38 <=> $less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_38])],[avatar_definition])).
% 1.60/0.90 tff(f3240,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | spl221_38),
% 1.60/0.90 inference(avatar_component_clause,[],[f3238])).
% 1.60/0.90 tff(f3241,plain,(
% 1.60/0.90 spl221_37 | spl221_32 | ~spl221_38),
% 1.60/0.90 inference(avatar_split_clause,[],[f2702,f3238,f3207,f3234])).
% 1.60/0.90 tff(f3243,definition,(
% 1.60/0.90 spl221_39 <=> 'fun_app$c'('p$',sK1)),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_39])],[avatar_definition])).
% 1.60/0.90 tff(f3245,plain,(
% 1.60/0.90 'fun_app$c'('p$',sK1) | ~spl221_39),
% 1.60/0.90 inference(avatar_component_clause,[],[f3243])).
% 1.60/0.90 tff(f3246,plain,(
% 1.60/0.90 spl221_37 | spl221_32 | spl221_39),
% 1.60/0.90 inference(avatar_split_clause,[],[f2701,f3243,f3207,f3234])).
% 1.60/0.90 tff(f3248,definition,(
% 1.60/0.90 spl221_40 <=> $less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$'))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_40])],[avatar_definition])).
% 1.60/0.90 tff(f3250,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$')) | spl221_40),
% 1.60/0.90 inference(avatar_component_clause,[],[f3248])).
% 1.60/0.90 tff(f3251,plain,(
% 1.60/0.90 ~spl221_40 | spl221_32 | ~spl221_38),
% 1.60/0.90 inference(avatar_split_clause,[],[f2700,f3238,f3207,f3248])).
% 1.60/0.90 tff(f3252,plain,(
% 1.60/0.90 ~spl221_40 | spl221_32 | spl221_39),
% 1.60/0.90 inference(avatar_split_clause,[],[f2699,f3243,f3207,f3248])).
% 1.60/0.90 tff(f3254,definition,(
% 1.60/0.90 spl221_41 <=> ! [X1 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | ~'fun_app$c'('p$',X1))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_41])],[avatar_definition])).
% 1.60/0.90 tff(f3255,plain,(
% 1.60/0.90 ( ! [X1 : 'Nat$'] : ($less('fun_app$b'('of_nat$',X1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | ~'fun_app$c'('p$',X1)) ) | ~spl221_41),
% 1.60/0.90 inference(avatar_component_clause,[],[f3254])).
% 1.60/0.90 tff(f3256,plain,(
% 1.60/0.90 spl221_27 | spl221_41),
% 1.60/0.90 inference(avatar_split_clause,[],[f2698,f3254,f3185])).
% 1.60/0.90 tff(f3257,plain,(
% 1.60/0.90 spl221_27 | ~spl221_32),
% 1.60/0.90 inference(avatar_split_clause,[],[f2697,f3207,f3185])).
% 1.60/0.90 tff(f3362,plain,(
% 1.60/0.90 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 1.60/0.90 inference(resolution,[],[f849,f845])).
% 1.60/0.90 tff(f3401,plain,(
% 1.60/0.90 ( ! [X0 : $int] : (~$less($sum(X0,1),X0)) ) | ~spl221_21),
% 1.60/0.90 inference(resolution,[],[f3362,f3158])).
% 1.60/0.90 tff(f4490,plain,(
% 1.60/0.90 'fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$','n_0$') | (~spl221_25 | ~spl221_32)),
% 1.60/0.90 inference(resolution,[],[f3176,f3209])).
% 1.60/0.90 tff(f4497,plain,(
% 1.60/0.90 $false | (~spl221_25 | ~spl221_32)),
% 1.60/0.90 inference(trivial_inequality_removal,[],[f4490])).
% 1.60/0.90 tff(f4498,plain,(
% 1.60/0.90 ~spl221_25 | ~spl221_32),
% 1.60/0.90 inference(avatar_contradiction_clause,[],[f4497])).
% 1.60/0.90 tff(f4520,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',sK0)) | (~spl221_24 | ~spl221_37)),
% 1.60/0.90 inference(resolution,[],[f3236,f3172])).
% 1.60/0.90 tff(f4533,definition,(
% 1.60/0.90 spl221_50 <=> 'fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',sK0)),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_50])],[avatar_definition])).
% 1.60/0.90 tff(f4534,plain,(
% 1.60/0.90 'fun_app$b'('of_nat$','n_0$') != 'fun_app$b'('of_nat$',sK0) | spl221_50),
% 1.60/0.90 inference(avatar_component_clause,[],[f4533])).
% 1.60/0.90 tff(f4535,plain,(
% 1.60/0.90 'fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',sK0) | ~spl221_50),
% 1.60/0.90 inference(avatar_component_clause,[],[f4533])).
% 1.60/0.90 tff(f4537,definition,(
% 1.60/0.90 spl221_51 <=> $less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',sK0))),
% 1.60/0.90 introduced(definition,[new_symbols(definition,[spl221_51])],[avatar_definition])).
% 1.60/0.90 tff(f4542,plain,(
% 1.60/0.90 ~$less('fun_app$b'('of_nat$',sK1),$sum(1,'fun_app$b'('of_nat$','n_0$'))) | spl221_38),
% 1.60/0.90 inference(forward_demodulation,[],[f3240,f840])).
% 1.60/0.91 tff(f4567,plain,(
% 1.60/0.91 ~spl221_51 | ~spl221_24 | ~spl221_37),
% 1.60/0.91 inference(avatar_split_clause,[],[f4520,f3234,f3171,f4537])).
% 1.60/0.91 tff(f4569,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK1),'fun_app$b'('of_nat$','n_0$')) | (~spl221_27 | ~spl221_39)),
% 1.60/0.91 inference(resolution,[],[f3186,f3245])).
% 1.60/0.91 tff(f4571,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK4),'fun_app$b'('of_nat$','n_0$')) | (~spl221_26 | ~spl221_27)),
% 1.60/0.91 inference(resolution,[],[f3186,f3181])).
% 1.60/0.91 tff(f4706,plain,(
% 1.60/0.91 ( ! [X0 : $int] : ($less(X0,'fun_app$b'('of_nat$','n_0$')) | $less('fun_app$b'('of_nat$',sK1),X0)) ) | (~spl221_27 | ~spl221_39)),
% 1.60/0.91 inference(resolution,[],[f4569,f1691])).
% 1.60/0.91 tff(f4774,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$','n_0$'),'fun_app$b'('of_nat$',sK0)) | 'fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',sK0) | spl221_40),
% 1.60/0.91 inference(resolution,[],[f3250,f847])).
% 1.60/0.91 tff(f4822,plain,(
% 1.60/0.91 sK0 = 'fun_app$f'('nat$','fun_app$b'('of_nat$','n_0$')) | ~spl221_50),
% 1.60/0.91 inference(superposition,[],[f2552,f4535])).
% 1.60/0.91 tff(f4830,plain,(
% 1.60/0.91 'n_0$' = sK0 | ~spl221_50),
% 1.60/0.91 inference(forward_demodulation,[],[f4822,f2552])).
% 1.60/0.91 tff(f4851,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK1),$sum('fun_app$b'('of_nat$','n_0$'),1)) | (~spl221_21 | ~spl221_27 | ~spl221_39)),
% 1.60/0.91 inference(resolution,[],[f4706,f3401])).
% 1.60/0.91 tff(f4896,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK1),$sum(1,'fun_app$b'('of_nat$','n_0$'))) | (~spl221_21 | ~spl221_27 | ~spl221_39)),
% 1.60/0.91 inference(forward_demodulation,[],[f4851,f840])).
% 1.60/0.91 tff(f4898,plain,(
% 1.60/0.91 $false | (~spl221_21 | ~spl221_27 | spl221_38 | ~spl221_39)),
% 1.60/0.91 inference(forward_subsumption_resolution,[],[f4896,f4542])).
% 1.60/0.91 tff(f4899,plain,(
% 1.60/0.91 ~spl221_21 | ~spl221_27 | spl221_38 | ~spl221_39),
% 1.60/0.91 inference(avatar_contradiction_clause,[],[f4898])).
% 1.60/0.91 tff(f4900,plain,(
% 1.60/0.91 ( ! [X1 : 'Nat$'] : (~'fun_app$c'('p$',X1) | $less('fun_app$b'('of_nat$',X1),$sum(1,'fun_app$b'('of_nat$','n_0$')))) ) | ~spl221_41),
% 1.60/0.91 inference(forward_demodulation,[],[f3255,f840])).
% 1.60/0.91 tff(f4901,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK1),$sum(1,'fun_app$b'('of_nat$','n_0$'))) | (~spl221_39 | ~spl221_41)),
% 1.60/0.91 inference(resolution,[],[f4900,f3245])).
% 1.60/0.91 tff(f4909,plain,(
% 1.60/0.91 $false | (spl221_38 | ~spl221_39 | ~spl221_41)),
% 1.60/0.91 inference(forward_subsumption_resolution,[],[f4901,f4542])).
% 1.60/0.91 tff(f4910,plain,(
% 1.60/0.91 spl221_38 | ~spl221_39 | ~spl221_41),
% 1.60/0.91 inference(avatar_contradiction_clause,[],[f4909])).
% 1.60/0.91 tff(f4913,plain,(
% 1.60/0.91 spl221_23 | ~spl221_26 | ~spl221_27),
% 1.60/0.91 inference(avatar_split_clause,[],[f4571,f3185,f3179,f3167])).
% 1.60/0.91 tff(f4915,plain,(
% 1.60/0.91 'fun_app$c'('p$','n_0$') | (~spl221_37 | ~spl221_50)),
% 1.60/0.91 inference(forward_demodulation,[],[f3236,f4830])).
% 1.60/0.91 tff(f4917,plain,(
% 1.60/0.91 spl221_32 | ~spl221_37 | ~spl221_50),
% 1.60/0.91 inference(avatar_split_clause,[],[f4915,f4533,f3234,f3207])).
% 1.60/0.91 tff(f4921,plain,(
% 1.60/0.91 spl221_50 | spl221_51 | spl221_40),
% 1.60/0.91 inference(avatar_split_clause,[],[f4774,f3248,f4537,f4533])).
% 1.60/0.91 tff(f4930,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK0),$sum(1,'fun_app$b'('of_nat$','n_0$'))) | (~spl221_37 | ~spl221_41)),
% 1.60/0.91 inference(resolution,[],[f4900,f3236])).
% 1.60/0.91 tff(f14864,plain,(
% 1.60/0.91 ( ! [X0 : 'Nat$',X1 : 'Nat$'] : (~$less('fun_app$b'('of_nat$',X0),$sum(1,'fun_app$b'('of_nat$',X1))) | $less('fun_app$b'('of_nat$',X0),'fun_app$b'('of_nat$',X1)) | 'fun_app$b'('of_nat$',X0) = 'fun_app$b'('of_nat$',X1)) )),
% 1.60/0.91 inference(forward_demodulation,[],[f1782,f840])).
% 1.60/0.91 tff(f15245,plain,(
% 1.60/0.91 $less('fun_app$b'('of_nat$',sK0),'fun_app$b'('of_nat$','n_0$')) | 'fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',sK0) | (~spl221_37 | ~spl221_41)),
% 1.60/0.91 inference(resolution,[],[f14864,f4930])).
% 1.60/0.91 tff(f15331,plain,(
% 1.60/0.91 'fun_app$b'('of_nat$','n_0$') = 'fun_app$b'('of_nat$',sK0) | (~spl221_37 | spl221_40 | ~spl221_41)),
% 1.60/0.91 inference(forward_subsumption_resolution,[],[f15245,f3250])).
% 1.60/0.91 tff(f15333,plain,(
% 1.60/0.91 $false | (~spl221_37 | spl221_40 | ~spl221_41 | spl221_50)),
% 1.60/0.91 inference(forward_subsumption_resolution,[],[f15331,f4534])).
% 1.60/0.91 tff(f15334,plain,(
% 1.60/0.91 ~spl221_37 | spl221_40 | ~spl221_41 | spl221_50),
% 1.60/0.91 inference(avatar_contradiction_clause,[],[f15333])).
% 1.60/0.91 cnf(s21, plain, spl221_21, inference(sat_conversion,[],[f3164])).
% 1.60/0.91 cnf(s33, plain, ~spl221_23 | spl221_24, inference(sat_conversion,[],[f3173])).
% 1.60/0.91 cnf(s34, plain, ~spl221_23 | spl221_25, inference(sat_conversion,[],[f3177])).
% 1.60/0.91 cnf(s35, plain, spl221_24 | spl221_26, inference(sat_conversion,[],[f3182])).
% 1.60/0.91 cnf(s36, plain, spl221_25 | spl221_26, inference(sat_conversion,[],[f3183])).
% 1.60/0.91 cnf(s47, plain, spl221_32 | spl221_37 | ~spl221_38, inference(sat_conversion,[],[f3241])).
% 1.60/0.91 cnf(s48, plain, spl221_32 | spl221_37 | spl221_39, inference(sat_conversion,[],[f3246])).
% 1.60/0.91 cnf(s49, plain, spl221_32 | ~spl221_38 | ~spl221_40, inference(sat_conversion,[],[f3251])).
% 1.60/0.91 cnf(s50, plain, spl221_32 | spl221_39 | ~spl221_40, inference(sat_conversion,[],[f3252])).
% 1.60/0.91 cnf(s51, plain, spl221_27 | spl221_41, inference(sat_conversion,[],[f3256])).
% 1.60/0.91 cnf(s52, plain, spl221_27 | ~spl221_32, inference(sat_conversion,[],[f3257])).
% 1.60/0.91 cnf(s88, plain, ~spl221_25 | ~spl221_32, inference(sat_conversion,[],[f4498])).
% 1.60/0.91 cnf(s100, plain, ~spl221_24 | ~spl221_37 | ~spl221_51, inference(sat_conversion,[],[f4567])).
% 1.60/0.91 cnf(s122, plain, ~spl221_21 | ~spl221_27 | spl221_38 | ~spl221_39, inference(sat_conversion,[],[f4899])).
% 1.60/0.91 cnf(s123, plain, spl221_38 | ~spl221_39 | ~spl221_41, inference(sat_conversion,[],[f4910])).
% 1.60/0.91 cnf(s126, plain, spl221_23 | ~spl221_26 | ~spl221_27, inference(sat_conversion,[],[f4913])).
% 1.60/0.91 cnf(s128, plain, spl221_32 | ~spl221_37 | ~spl221_50, inference(sat_conversion,[],[f4917])).
% 1.60/0.91 cnf(s132, plain, spl221_40 | spl221_50 | spl221_51, inference(sat_conversion,[],[f4921])).
% 1.60/0.91 cnf(s552, plain, ~spl221_37 | spl221_40 | ~spl221_41 | spl221_50, inference(sat_conversion,[],[f15334])).
% 1.60/0.91 cnf(s559, plain, spl221_37 | spl221_27, inference(rat,[],[s123,s47,s48,s52,s51])).
% 1.60/0.91 cnf(s560, plain, spl221_27, inference(rat,[],[s123,s49,s50,s552,s128,s559,s51,s52])).
% 1.60/0.91 cnf(s561, plain, spl221_37 | spl221_32, inference(rat,[],[s122,s47,s48,s560,s21])).
% 1.60/0.91 cnf(s562, plain, ~spl221_40 | spl221_32, inference(rat,[],[s122,s49,s50,s560,s21])).
% 1.60/0.91 cnf(s563, plain, spl221_26, inference(rat,[],[s562,s132,s100,s128,s561,s88,s35,s36])).
% 1.60/0.91 cnf(s571, plain, spl221_23, inference(rat,[],[s126,s560,s563])).
% 1.60/0.91 cnf(s573, plain, spl221_25, inference(rat,[],[s34,s571])).
% 1.60/0.91 cnf(s574, plain, spl221_24, inference(rat,[],[s33,s571])).
% 1.60/0.91 cnf(s575, plain, ~spl221_32, inference(rat,[],[s88,s573])).
% 1.60/0.91 cnf(s577, plain, spl221_37, inference(rat,[],[s561,s575])).
% 1.60/0.91 cnf(s578, plain, ~spl221_40, inference(rat,[],[s562,s575])).
% 1.60/0.91 cnf(s579, plain, ~spl221_50, inference(rat,[],[s128,s575,s577])).
% 1.60/0.91 cnf(s580, plain, ~spl221_51, inference(rat,[],[s100,s574,s577])).
% 1.60/0.91 cnf(s582, plain, $false, inference(rat,[],[s132,s579,s578,s580])).
% 1.60/0.91 tff(f15335,plain,(
% 1.60/0.91 $false),
% 1.60/0.91 inference(avatar_sat_refutation,[],[s582])).
% 1.60/0.91 % SZS output end Proof for theBenchmark
% 1.60/0.91 % (3553368)------------------------------
% 1.60/0.91 % (3553368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.91 % (3553368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.91 % (3553368)CaDiCaL version: 2.1.3
% 1.60/0.91 % (3553368)Termination reason: Refutation
% 1.60/0.91 % (3553368)Time elapsed: 0.406 s
% 1.60/0.91 % (3553368)Peak memory usage: 19 MB
% 1.60/0.91 % (3553368)Instructions burned: 673 (million)
% 1.60/0.91 % (3553347)Success in time 0.485 s
% 1.60/0.91 % Vampire exiting
%------------------------------------------------------------------------------