%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI617_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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 09:34:58 AM UTC 2026
% Result : Theorem 3.77s 0.99s
% Output : Refutation 3.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ARI617_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.24 % Computer : n017.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 20:49:06 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.24/0.30 Running first-order model finding
% 0.24/0.30 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
% 3.77/0.99 % (4012264)Will run a generic schedule for satisfiability detection.
% 3.77/0.99 % (4012275)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3022510067:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 3.77/0.99 % (4012270)% WARNING: option uhcvi not known.
% 3.77/0.99 % (4012273)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3180856185:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 3.77/0.99 % (4012270)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3111052262:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 3.77/0.99 % (4012269)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=181079789_3000 on theBenchmark for (3000ds/0Mi)
% 3.77/0.99 % (4012272)dis+10_1_sil=32000:sp=arity:random_seed=2712199180:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 3.77/0.99 % (4012271)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4049195908:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 3.77/0.99 % (4012274)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1440910638:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 3.77/0.99 % (4012269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.77/0.99 % (4012269)Terminated due to inappropriate strategy.
% 3.77/0.99 % (4012269)------------------------------
% 3.77/0.99 % (4012269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012269)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012269)Termination reason: Inappropriate
% 3.77/0.99 % (4012269)Time elapsed: 0.001 s
% 3.77/0.99 % (4012269)Peak memory usage: 10 MB
% 3.77/0.99 % (4012269)------------------------------
% 3.77/0.99 % (4012269)------------------------------
% 3.77/0.99 % (4012283)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3665656903:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.77/0.99 % (4012283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.77/0.99 % (4012283)Terminated due to inappropriate strategy.
% 3.77/0.99 % (4012283)------------------------------
% 3.77/0.99 % (4012283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012283)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012283)Termination reason: Inappropriate
% 3.77/0.99 % (4012283)Time elapsed: 0.001 s
% 3.77/0.99 % (4012283)Peak memory usage: 10 MB
% 3.77/0.99 % (4012283)------------------------------
% 3.77/0.99 % (4012283)------------------------------
% 3.77/0.99 % (4012285)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3096663931:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.77/0.99 % (4012275)Instruction limit reached!
% 3.77/0.99 % (4012275)------------------------------
% 3.77/0.99 % (4012275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012275)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012275)Termination reason: Instruction limit
% 3.77/0.99 % (4012275)Termination phase: Saturation
% 3.77/0.99 % (4012275)Time elapsed: 0.097 s
% 3.77/0.99 % (4012275)Peak memory usage: 14 MB
% 3.77/0.99 % (4012275)Instructions burned: 160 (million)
% 3.77/0.99 % (4012272)Instruction limit reached!
% 3.77/0.99 % (4012272)------------------------------
% 3.77/0.99 % (4012272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012272)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012272)Termination reason: Instruction limit
% 3.77/0.99 % (4012272)Termination phase: Saturation
% 3.77/0.99 % (4012272)Time elapsed: 0.104 s
% 3.77/0.99 % (4012272)Peak memory usage: 12 MB
% 3.77/0.99 % (4012272)Instructions burned: 103 (million)
% 3.77/0.99 % (4012273)Instruction limit reached!
% 3.77/0.99 % (4012273)------------------------------
% 3.77/0.99 % (4012273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012273)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012273)Termination reason: Instruction limit
% 3.77/0.99 % (4012273)Termination phase: Saturation
% 3.77/0.99 % (4012273)Time elapsed: 0.112 s
% 3.77/0.99 % (4012273)Peak memory usage: 12 MB
% 3.77/0.99 % (4012273)Instructions burned: 116 (million)
% 3.77/0.99 % (4012287)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=489689983:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.77/0.99 % (4012274)Instruction limit reached!
% 3.77/0.99 % (4012274)------------------------------
% 3.77/0.99 % (4012274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012274)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012274)Termination reason: Instruction limit
% 3.77/0.99 % (4012274)Termination phase: Saturation
% 3.77/0.99 % (4012274)Time elapsed: 0.140 s
% 3.77/0.99 % (4012274)Peak memory usage: 13 MB
% 3.77/0.99 % (4012274)Instructions burned: 131 (million)
% 3.77/0.99 % (4012288)ott-21_1_sil=16000:fs=off:random_seed=2093527429:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.77/0.99 % (4012289)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3403913786:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.77/0.99 % (4012285)Instruction limit reached!
% 3.77/0.99 % (4012285)------------------------------
% 3.77/0.99 % (4012285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012285)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012285)Termination reason: Instruction limit
% 3.77/0.99 % (4012285)Termination phase: Saturation
% 3.77/0.99 % (4012285)Time elapsed: 0.088 s
% 3.77/0.99 % (4012285)Peak memory usage: 13 MB
% 3.77/0.99 % (4012285)Instructions burned: 131 (million)
% 3.77/0.99 % (4012294)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3475065795:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.77/0.99 % (4012292)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=395422284:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.77/0.99 % (4012292)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.77/0.99 % (4012292)Terminated due to inappropriate strategy.
% 3.77/0.99 % (4012292)------------------------------
% 3.77/0.99 % (4012292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012292)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012292)Termination reason: Inappropriate
% 3.77/0.99 % (4012292)Time elapsed: 0.001 s
% 3.77/0.99 % (4012292)Peak memory usage: 10 MB
% 3.77/0.99 % (4012292)------------------------------
% 3.77/0.99 % (4012292)------------------------------
% 3.77/0.99 % (4012297)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=796348396:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 3.77/0.99 % (4012297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.77/0.99 % (4012297)Terminated due to inappropriate strategy.
% 3.77/0.99 % (4012297)------------------------------
% 3.77/0.99 % (4012297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012297)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012297)Termination reason: Inappropriate
% 3.77/0.99 % (4012297)Time elapsed: 0.001 s
% 3.77/0.99 % (4012297)Peak memory usage: 10 MB
% 3.77/0.99 % (4012297)------------------------------
% 3.77/0.99 % (4012297)------------------------------
% 3.77/0.99 % (4012299)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=3769371073: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)
% 3.77/0.99 % (4012288)Instruction limit reached!
% 3.77/0.99 % (4012288)------------------------------
% 3.77/0.99 % (4012288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012288)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012288)Termination reason: Instruction limit
% 3.77/0.99 % (4012288)Termination phase: Saturation
% 3.77/0.99 % (4012288)Time elapsed: 0.146 s
% 3.77/0.99 % (4012288)Peak memory usage: 12 MB
% 3.77/0.99 % (4012288)Instructions burned: 181 (million)
% 3.77/0.99 % (4012301)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2079671288:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 3.77/0.99 % (4012287) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4012264-4012287"...
% 3.77/0.99 % (4012289)Instruction limit reached!
% 3.77/0.99 % (4012289)------------------------------
% 3.77/0.99 % (4012289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012289)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012289)Termination reason: Instruction limit
% 3.77/0.99 % (4012289)Termination phase: Saturation
% 3.77/0.99 % (4012289)Time elapsed: 0.488 s
% 3.77/0.99 % (4012289)Peak memory usage: 14 MB
% 3.77/0.99 % (4012289)Instructions burned: 478 (million)
% 3.77/0.99 % (4012287)...printing done.
% 3.77/0.99 % (4012287)Refutation found. Thanks to Tanya!
% 3.77/0.99 % SZS status Theorem for theBenchmark
% 3.77/0.99 % SZS output start Proof for theBenchmark
% 3.77/0.99 tff(func_def_0, type, f: $int > $int).
% 3.77/0.99 tff(func_def_1, type, g: $int > $int).
% 3.77/0.99 tff(func_def_6, type, sK0: $int).
% 3.77/0.99 tff(f1,conjecture,(
% 3.77/0.99 (! [X0 : $int] : ($lesseq(X0,f(X0)) & $lesseq($uminus(X0),f(X0)) & ($lesseq(f(X0),X0) | $lesseq(f(X0),$uminus(X0)))) & ! [X0 : $int] : ($lesseq(0,g(X0)) & (g(X0) = X0 | g(X0) = $uminus(X0)))) => ! [X0 : $int] : f(X0) = g(X0)),
% 3.77/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p',absolute_value_defs)).
% 3.77/0.99 tff(f2,negated_conjecture,(
% 3.77/0.99 ~((! [X0 : $int] : ($lesseq(X0,f(X0)) & $lesseq($uminus(X0),f(X0)) & ($lesseq(f(X0),X0) | $lesseq(f(X0),$uminus(X0)))) & ! [X0 : $int] : ($lesseq(0,g(X0)) & (g(X0) = X0 | g(X0) = $uminus(X0)))) => ! [X0 : $int] : f(X0) = g(X0))),
% 3.77/0.99 inference(negated_conjecture,[status(cth)],[f1])).
% 3.77/0.99 tff(f3,plain,(
% 3.77/0.99 ~((! [X0 : $int] : (~$less(f(X0),X0) & ~$less(f(X0),$uminus(X0)) & (~$less(X0,f(X0)) | ~$less($uminus(X0),f(X0)))) & ! [X0 : $int] : (~$less(g(X0),0) & (g(X0) = X0 | g(X0) = $uminus(X0)))) => ! [X0 : $int] : f(X0) = g(X0))),
% 3.77/0.99 inference(theory_normalization,[],[f2])).
% 3.77/0.99 tff(f4,definition,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 3.77/0.99 introduced(theory,[tha_commutativity])).
% 3.77/0.99 tff(f6,definition,(
% 3.77/0.99 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 3.77/0.99 introduced(theory,[tha_right_identity])).
% 3.77/0.99 tff(f8,definition,(
% 3.77/0.99 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 3.77/0.99 introduced(theory,[tha_inverse_op_unit])).
% 3.77/0.99 tff(f10,definition,(
% 3.77/0.99 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 3.77/0.99 introduced(theory,[tha_transitivity])).
% 3.77/0.99 tff(f11,definition,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 3.77/0.99 introduced(theory,[tha_order_totality])).
% 3.77/0.99 tff(f12,definition,(
% 3.77/0.99 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 3.77/0.99 introduced(theory,[tha_order_monotonicity])).
% 3.77/0.99 tff(f13,definition,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 3.77/0.99 introduced(theory,[tha_order_plus_one_dichotomy])).
% 3.77/0.99 tff(f14,definition,(
% 3.77/0.99 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 3.77/0.99 introduced(theory,[tha_minus_minus_x])).
% 3.77/0.99 tff(f15,definition,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 3.77/0.99 introduced(theory,[tha_extra_integer_ordering])).
% 3.77/0.99 tff(f16,plain,(
% 3.77/0.99 ~((! [X0 : $int] : (~$less(f(X0),X0) & ~$less(f(X0),$uminus(X0)) & (~$less(X0,f(X0)) | ~$less($uminus(X0),f(X0)))) & ! [X1 : $int] : (~$less(g(X1),0) & (g(X1) = X1 | $uminus(X1) = g(X1)))) => ! [X2 : $int] : f(X2) = g(X2))),
% 3.77/0.99 inference(rectify,[],[f3])).
% 3.77/0.99 tff(f17,plain,(
% 3.77/0.99 ? [X2 : $int] : f(X2) != g(X2) & (! [X0 : $int] : (~$less(f(X0),X0) & ~$less(f(X0),$uminus(X0)) & (~$less(X0,f(X0)) | ~$less($uminus(X0),f(X0)))) & ! [X1 : $int] : (~$less(g(X1),0) & (g(X1) = X1 | $uminus(X1) = g(X1))))),
% 3.77/0.99 inference(ennf_transformation,[],[f16])).
% 3.77/0.99 tff(f18,plain,(
% 3.77/0.99 ? [X2 : $int] : f(X2) != g(X2) & ! [X0 : $int] : (~$less(f(X0),X0) & ~$less(f(X0),$uminus(X0)) & (~$less(X0,f(X0)) | ~$less($uminus(X0),f(X0)))) & ! [X1 : $int] : (~$less(g(X1),0) & (g(X1) = X1 | $uminus(X1) = g(X1)))),
% 3.77/0.99 inference(flattening,[],[f17])).
% 3.77/0.99 tff(f19,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less($uminus(X0),f(X0)) | ~$less(X0,f(X0))) )),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f20,plain,(
% 3.77/0.99 ( ! [X1 : $int] : ($uminus(X1) = g(X1) | g(X1) = X1) )),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f21,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f(X0),$uminus(X0))) )),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f22,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f(X0),X0)) )),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f23,plain,(
% 3.77/0.99 ( ! [X1 : $int] : (~$less(g(X1),0)) )),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f24,plain,(
% 3.77/0.99 f(sK0) != g(sK0)),
% 3.77/0.99 inference(cnf_transformation,[],[f18])).
% 3.77/0.99 tff(f25,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less($uminus(X0),0) | g(X0) = X0) )),
% 3.77/0.99 inference(superposition,[],[f23,f20])).
% 3.77/0.99 tff(f26,plain,(
% 3.77/0.99 f(sK0) != $uminus(sK0) | sK0 = g(sK0)),
% 3.77/0.99 inference(superposition,[],[f24,f20])).
% 3.77/0.99 tff(f29,definition,(
% 3.77/0.99 spl1_1 <=> sK0 = g(sK0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition])).
% 3.77/0.99 tff(f30,plain,(
% 3.77/0.99 sK0 != g(sK0) | spl1_1),
% 3.77/0.99 inference(avatar_component_clause,[],[f29])).
% 3.77/0.99 tff(f31,plain,(
% 3.77/0.99 sK0 = g(sK0) | ~spl1_1),
% 3.77/0.99 inference(avatar_component_clause,[],[f29])).
% 3.77/0.99 tff(f33,definition,(
% 3.77/0.99 spl1_2 <=> f(sK0) = $uminus(sK0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition])).
% 3.77/0.99 tff(f35,plain,(
% 3.77/0.99 f(sK0) != $uminus(sK0) | spl1_2),
% 3.77/0.99 inference(avatar_component_clause,[],[f33])).
% 3.77/0.99 tff(f36,plain,(
% 3.77/0.99 spl1_1 | ~spl1_2),
% 3.77/0.99 inference(avatar_split_clause,[],[f26,f33,f29])).
% 3.77/0.99 tff(f38,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(X0,0) | $uminus(X0) = g($uminus(X0))) )),
% 3.77/0.99 inference(superposition,[],[f25,f14])).
% 3.77/0.99 tff(f40,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f($uminus(X0)),X0)) )),
% 3.77/0.99 inference(superposition,[],[f21,f14])).
% 3.77/0.99 tff(f44,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (0 = $sum($uminus(X0),X0)) )),
% 3.77/0.99 inference(superposition,[],[f8,f14])).
% 3.77/0.99 tff(f57,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f($sum(X0,1)))) )),
% 3.77/0.99 inference(resolution,[],[f13,f22])).
% 3.77/0.99 tff(f59,plain,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 3.77/0.99 inference(superposition,[],[f13,f4])).
% 3.77/0.99 tff(f61,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,0) | $less($uminus(1),X0)) )),
% 3.77/0.99 inference(superposition,[],[f13,f44])).
% 3.77/0.99 tff(f62,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,0) | $less(-1,X0)) )),
% 3.77/0.99 inference(evaluation,[],[f61])).
% 3.77/0.99 tff(f63,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f($sum(1,X0)))) )),
% 3.77/0.99 inference(superposition,[],[f57,f4])).
% 3.77/0.99 tff(f65,plain,(
% 3.77/0.99 $less($uminus(1),f(0))),
% 3.77/0.99 inference(superposition,[],[f57,f44])).
% 3.77/0.99 tff(f66,plain,(
% 3.77/0.99 $less(-1,f(0))),
% 3.77/0.99 inference(evaluation,[],[f65])).
% 3.77/0.99 tff(f67,plain,(
% 3.77/0.99 $less(0,f(1))),
% 3.77/0.99 inference(superposition,[],[f63,f6])).
% 3.77/0.99 tff(f93,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(-1,g(X0))) )),
% 3.77/0.99 inference(resolution,[],[f62,f23])).
% 3.77/0.99 tff(f96,plain,(
% 3.77/0.99 $less(0,0) | $uminus(-1) = g($uminus(-1))),
% 3.77/0.99 inference(resolution,[],[f62,f38])).
% 3.77/0.99 tff(f97,plain,(
% 3.77/0.99 1 = g(1)),
% 3.77/0.99 inference(evaluation,[],[f96])).
% 3.77/0.99 tff(f114,plain,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 3.77/0.99 inference(superposition,[],[f15,f4])).
% 3.77/0.99 tff(f116,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(X0,0) | ~$less($uminus(1),X0)) )),
% 3.77/0.99 inference(superposition,[],[f15,f44])).
% 3.77/0.99 tff(f117,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(-1,X0) | ~$less(X0,0)) )),
% 3.77/0.99 inference(evaluation,[],[f116])).
% 3.77/0.99 tff(f143,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,1) | $less(0,X0)) )),
% 3.77/0.99 inference(superposition,[],[f59,f6])).
% 3.77/0.99 tff(f164,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(0,X0) | ~$less(X0,1)) )),
% 3.77/0.99 inference(superposition,[],[f114,f6])).
% 3.77/0.99 tff(f185,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less($sum(1,X0),1) | $less(X0,0)) )),
% 3.77/0.99 inference(resolution,[],[f164,f59])).
% 3.77/0.99 tff(f243,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f(1)) | ~$less(X0,0)) )),
% 3.77/0.99 inference(resolution,[],[f10,f67])).
% 3.77/0.99 tff(f252,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f(0)) | ~$less(X0,-1)) )),
% 3.77/0.99 inference(resolution,[],[f10,f66])).
% 3.77/0.99 tff(f253,plain,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($less(X0,g(X1)) | ~$less(X0,-1)) )),
% 3.77/0.99 inference(resolution,[],[f10,f93])).
% 3.77/0.99 tff(f257,plain,(
% 3.77/0.99 ~$less(f(f(0)),-1)),
% 3.77/0.99 inference(resolution,[],[f252,f22])).
% 3.77/0.99 tff(f265,plain,(
% 3.77/0.99 ~$less(f($uminus(f(1))),0)),
% 3.77/0.99 inference(resolution,[],[f243,f40])).
% 3.77/0.99 tff(f266,plain,(
% 3.77/0.99 ~$less($uminus(1),0) | ~$less(1,f(1))),
% 3.77/0.99 inference(resolution,[],[f243,f19])).
% 3.77/0.99 tff(f270,plain,(
% 3.77/0.99 ~$less(1,f(1))),
% 3.77/0.99 inference(evaluation,[],[f266])).
% 3.77/0.99 tff(f280,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f(X0)) | f(X0) = X0) )),
% 3.77/0.99 inference(resolution,[],[f11,f22])).
% 3.77/0.99 tff(f282,plain,(
% 3.77/0.99 $less(-1,f(f(0))) | -1 = f(f(0))),
% 3.77/0.99 inference(resolution,[],[f11,f257])).
% 3.77/0.99 tff(f315,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(f(X0),$uminus(X0)) | f(X0) = $uminus(X0) | ~$less(X0,f(X0))) )),
% 3.77/0.99 inference(resolution,[],[f11,f19])).
% 3.77/0.99 tff(f319,plain,(
% 3.77/0.99 $less(f(1),1) | 1 = f(1)),
% 3.77/0.99 inference(resolution,[],[f11,f270])).
% 3.77/0.99 tff(f326,plain,(
% 3.77/0.99 1 = f(1)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f319,f22])).
% 3.77/0.99 tff(f328,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(X0,f(X0)) | f(X0) = $uminus(X0)) )),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f315,f21])).
% 3.77/0.99 tff(f348,definition,(
% 3.77/0.99 spl1_7 <=> -1 = f(f(0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition])).
% 3.77/0.99 tff(f350,plain,(
% 3.77/0.99 -1 = f(f(0)) | ~spl1_7),
% 3.77/0.99 inference(avatar_component_clause,[],[f348])).
% 3.77/0.99 tff(f352,definition,(
% 3.77/0.99 spl1_8 <=> $less(-1,f(f(0)))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition])).
% 3.77/0.99 tff(f354,plain,(
% 3.77/0.99 $less(-1,f(f(0))) | ~spl1_8),
% 3.77/0.99 inference(avatar_component_clause,[],[f352])).
% 3.77/0.99 tff(f361,plain,(
% 3.77/0.99 spl1_7 | spl1_8),
% 3.77/0.99 inference(avatar_split_clause,[],[f282,f352,f348])).
% 3.77/0.99 tff(f367,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(X0,0) | $less(X0,1)) )),
% 3.77/0.99 inference(superposition,[],[f243,f326])).
% 3.77/0.99 tff(f373,plain,(
% 3.77/0.99 sK0 != f(sK0) | ~spl1_1),
% 3.77/0.99 inference(superposition,[],[f24,f31])).
% 3.77/0.99 tff(f375,plain,(
% 3.77/0.99 ~$less(sK0,0) | ~spl1_1),
% 3.77/0.99 inference(superposition,[],[f23,f31])).
% 3.77/0.99 tff(f380,definition,(
% 3.77/0.99 spl1_9 <=> 0 = sK0),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition])).
% 3.77/0.99 tff(f381,plain,(
% 3.77/0.99 0 != sK0 | spl1_9),
% 3.77/0.99 inference(avatar_component_clause,[],[f380])).
% 3.77/0.99 tff(f382,plain,(
% 3.77/0.99 0 = sK0 | ~spl1_9),
% 3.77/0.99 inference(avatar_component_clause,[],[f380])).
% 3.77/0.99 tff(f384,definition,(
% 3.77/0.99 spl1_10 <=> $less(0,sK0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition])).
% 3.77/0.99 tff(f385,plain,(
% 3.77/0.99 ~$less(0,sK0) | spl1_10),
% 3.77/0.99 inference(avatar_component_clause,[],[f384])).
% 3.77/0.99 tff(f386,plain,(
% 3.77/0.99 $less(0,sK0) | ~spl1_10),
% 3.77/0.99 inference(avatar_component_clause,[],[f384])).
% 3.77/0.99 tff(f395,plain,(
% 3.77/0.99 0 != f(0) | (~spl1_1 | ~spl1_9)),
% 3.77/0.99 inference(forward_demodulation,[],[f373,f382])).
% 3.77/0.99 tff(f406,plain,(
% 3.77/0.99 ~$less(f($uminus(1)),0)),
% 3.77/0.99 inference(forward_demodulation,[],[f265,f326])).
% 3.77/0.99 tff(f407,plain,(
% 3.77/0.99 ~$less(f(-1),0)),
% 3.77/0.99 inference(evaluation,[],[f406])).
% 3.77/0.99 tff(f409,plain,(
% 3.77/0.99 ~$less(f(f(0)),0) | ~spl1_8),
% 3.77/0.99 inference(resolution,[],[f354,f117])).
% 3.77/0.99 tff(f412,plain,(
% 3.77/0.99 $less(0,f(f(0))) | 0 = f(f(0)) | ~spl1_8),
% 3.77/0.99 inference(resolution,[],[f409,f11])).
% 3.77/0.99 tff(f415,definition,(
% 3.77/0.99 spl1_11 <=> 0 = f(f(0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition])).
% 3.77/0.99 tff(f417,plain,(
% 3.77/0.99 0 = f(f(0)) | ~spl1_11),
% 3.77/0.99 inference(avatar_component_clause,[],[f415])).
% 3.77/0.99 tff(f419,definition,(
% 3.77/0.99 spl1_12 <=> $less(0,f(f(0)))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition])).
% 3.77/0.99 tff(f421,plain,(
% 3.77/0.99 $less(0,f(f(0))) | ~spl1_12),
% 3.77/0.99 inference(avatar_component_clause,[],[f419])).
% 3.77/0.99 tff(f423,plain,(
% 3.77/0.99 spl1_11 | spl1_12 | ~spl1_8),
% 3.77/0.99 inference(avatar_split_clause,[],[f412,f352,f419,f415])).
% 3.77/0.99 tff(f448,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,1) | $less(-1,X0)) )),
% 3.77/0.99 inference(resolution,[],[f367,f62])).
% 3.77/0.99 tff(f462,plain,(
% 3.77/0.99 ~$less(0,f(0)) | ~spl1_11),
% 3.77/0.99 inference(superposition,[],[f22,f417])).
% 3.77/0.99 tff(f465,plain,(
% 3.77/0.99 $less(f(0),0) | 0 = f(0) | ~spl1_11),
% 3.77/0.99 inference(resolution,[],[f462,f11])).
% 3.77/0.99 tff(f468,plain,(
% 3.77/0.99 0 = f(0) | ~spl1_11),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f465,f22])).
% 3.77/0.99 tff(f471,plain,(
% 3.77/0.99 $false | (~spl1_1 | ~spl1_9 | ~spl1_11)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f468,f395])).
% 3.77/0.99 tff(f472,plain,(
% 3.77/0.99 ~spl1_1 | ~spl1_9 | ~spl1_11),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f471])).
% 3.77/0.99 tff(f473,plain,(
% 3.77/0.99 ~$less(f(f(0)),1) | ~spl1_12),
% 3.77/0.99 inference(resolution,[],[f421,f164])).
% 3.77/0.99 tff(f482,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(-1,$sum(1,X0)) | $less(X0,0)) )),
% 3.77/0.99 inference(resolution,[],[f448,f185])).
% 3.77/0.99 tff(f498,plain,(
% 3.77/0.99 $less(1,f(f(0))) | 1 = f(f(0)) | ~spl1_12),
% 3.77/0.99 inference(resolution,[],[f473,f11])).
% 3.77/0.99 tff(f501,definition,(
% 3.77/0.99 spl1_13 <=> 1 = f(f(0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition])).
% 3.77/0.99 tff(f503,plain,(
% 3.77/0.99 1 = f(f(0)) | ~spl1_13),
% 3.77/0.99 inference(avatar_component_clause,[],[f501])).
% 3.77/0.99 tff(f505,definition,(
% 3.77/0.99 spl1_14 <=> $less(1,f(f(0)))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition])).
% 3.77/0.99 tff(f507,plain,(
% 3.77/0.99 $less(1,f(f(0))) | ~spl1_14),
% 3.77/0.99 inference(avatar_component_clause,[],[f505])).
% 3.77/0.99 tff(f509,plain,(
% 3.77/0.99 spl1_13 | spl1_14 | ~spl1_12),
% 3.77/0.99 inference(avatar_split_clause,[],[f498,f419,f505,f501])).
% 3.77/0.99 tff(f516,plain,(
% 3.77/0.99 ~$less($uminus(f(0)),1) | ~$less(f(0),1) | ~spl1_13),
% 3.77/0.99 inference(superposition,[],[f19,f503])).
% 3.77/0.99 tff(f517,plain,(
% 3.77/0.99 ~$less(1,$uminus(f(0))) | ~spl1_13),
% 3.77/0.99 inference(superposition,[],[f21,f503])).
% 3.77/0.99 tff(f520,definition,(
% 3.77/0.99 spl1_15 <=> $less(f(0),1)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition])).
% 3.77/0.99 tff(f522,plain,(
% 3.77/0.99 ~$less(f(0),1) | spl1_15),
% 3.77/0.99 inference(avatar_component_clause,[],[f520])).
% 3.77/0.99 tff(f524,definition,(
% 3.77/0.99 spl1_16 <=> $less($uminus(f(0)),1)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition])).
% 3.77/0.99 tff(f527,plain,(
% 3.77/0.99 ~spl1_15 | ~spl1_16 | ~spl1_13),
% 3.77/0.99 inference(avatar_split_clause,[],[f516,f501,f524,f520])).
% 3.77/0.99 tff(f532,definition,(
% 3.77/0.99 spl1_17 <=> 1 = f(0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_17])],[avatar_definition])).
% 3.77/0.99 tff(f534,plain,(
% 3.77/0.99 1 = f(0) | ~spl1_17),
% 3.77/0.99 inference(avatar_component_clause,[],[f532])).
% 3.77/0.99 tff(f538,plain,(
% 3.77/0.99 $less($uminus(f(0)),1) | 1 = $uminus(f(0)) | ~spl1_13),
% 3.77/0.99 inference(resolution,[],[f517,f11])).
% 3.77/0.99 tff(f541,definition,(
% 3.77/0.99 spl1_18 <=> 1 = $uminus(f(0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_18])],[avatar_definition])).
% 3.77/0.99 tff(f543,plain,(
% 3.77/0.99 1 = $uminus(f(0)) | ~spl1_18),
% 3.77/0.99 inference(avatar_component_clause,[],[f541])).
% 3.77/0.99 tff(f545,plain,(
% 3.77/0.99 spl1_18 | spl1_16 | ~spl1_13),
% 3.77/0.99 inference(avatar_split_clause,[],[f538,f501,f524,f541])).
% 3.77/0.99 tff(f556,plain,(
% 3.77/0.99 $uminus(1) = f(0) | ~spl1_18),
% 3.77/0.99 inference(superposition,[],[f14,f543])).
% 3.77/0.99 tff(f566,plain,(
% 3.77/0.99 -1 = f(0) | ~spl1_18),
% 3.77/0.99 inference(evaluation,[],[f556])).
% 3.77/0.99 tff(f576,plain,(
% 3.77/0.99 $less(-1,-1) | ~spl1_18),
% 3.77/0.99 inference(superposition,[],[f66,f566])).
% 3.77/0.99 tff(f601,plain,(
% 3.77/0.99 $false | ~spl1_18),
% 3.77/0.99 inference(evaluation,[],[f576])).
% 3.77/0.99 tff(f602,plain,(
% 3.77/0.99 ~spl1_18),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f601])).
% 3.77/0.99 tff(f608,plain,(
% 3.77/0.99 $less(0,f(0)) | spl1_15),
% 3.77/0.99 inference(resolution,[],[f522,f143])).
% 3.77/0.99 tff(f609,plain,(
% 3.77/0.99 $less(1,f(0)) | 1 = f(0) | spl1_15),
% 3.77/0.99 inference(resolution,[],[f522,f11])).
% 3.77/0.99 tff(f623,plain,(
% 3.77/0.99 ( ! [X0 : $int,X1 : $int] : ($less($sum(X0,$uminus(X1)),0) | ~$less(X0,X1)) )),
% 3.77/0.99 inference(superposition,[],[f12,f8])).
% 3.77/0.99 tff(f644,plain,(
% 3.77/0.99 ~$less($uminus(0),1) | ~$less(0,1) | ~spl1_17),
% 3.77/0.99 inference(superposition,[],[f19,f534])).
% 3.77/0.99 tff(f647,plain,(
% 3.77/0.99 $false | ~spl1_17),
% 3.77/0.99 inference(evaluation,[],[f644])).
% 3.77/0.99 tff(f648,plain,(
% 3.77/0.99 ~spl1_17),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f647])).
% 3.77/0.99 tff(f653,definition,(
% 3.77/0.99 spl1_20 <=> $less(1,f(0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_20])],[avatar_definition])).
% 3.77/0.99 tff(f655,plain,(
% 3.77/0.99 $less(1,f(0)) | ~spl1_20),
% 3.77/0.99 inference(avatar_component_clause,[],[f653])).
% 3.77/0.99 tff(f657,plain,(
% 3.77/0.99 spl1_17 | spl1_20 | spl1_15),
% 3.77/0.99 inference(avatar_split_clause,[],[f609,f520,f653,f532])).
% 3.77/0.99 tff(f667,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less(X0,f(0)) | ~$less(X0,1)) ) | ~spl1_20),
% 3.77/0.99 inference(resolution,[],[f655,f10])).
% 3.77/0.99 tff(f679,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f(g(X0)),-1)) )),
% 3.77/0.99 inference(resolution,[],[f253,f22])).
% 3.77/0.99 tff(f680,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f($uminus(g(X0))),-1)) )),
% 3.77/0.99 inference(resolution,[],[f253,f40])).
% 3.77/0.99 tff(f696,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f($uminus($uminus(X0))),-1) | g(X0) = X0) )),
% 3.77/0.99 inference(superposition,[],[f680,f20])).
% 3.77/0.99 tff(f699,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(f(X0),-1) | g(X0) = X0) )),
% 3.77/0.99 inference(evaluation,[],[f696])).
% 3.77/0.99 tff(f884,plain,(
% 3.77/0.99 0 = f(0) | ~$less(f(0),1)),
% 3.77/0.99 inference(resolution,[],[f280,f164])).
% 3.77/0.99 tff(f1019,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less($sum(1,X0),0) | $less(X0,0)) )),
% 3.77/0.99 inference(resolution,[],[f482,f117])).
% 3.77/0.99 tff(f1058,plain,(
% 3.77/0.99 ~$less($uminus(0),1) | ~$less(0,f(0)) | ~spl1_20),
% 3.77/0.99 inference(resolution,[],[f667,f19])).
% 3.77/0.99 tff(f1063,plain,(
% 3.77/0.99 ~$less(0,f(0)) | ~spl1_20),
% 3.77/0.99 inference(evaluation,[],[f1058])).
% 3.77/0.99 tff(f1064,plain,(
% 3.77/0.99 $false | (spl1_15 | ~spl1_20)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f1063,f608])).
% 3.77/0.99 tff(f1065,plain,(
% 3.77/0.99 spl1_15 | ~spl1_20),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f1064])).
% 3.77/0.99 tff(f1067,definition,(
% 3.77/0.99 spl1_41 <=> 0 = f(0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_41])],[avatar_definition])).
% 3.77/0.99 tff(f1069,plain,(
% 3.77/0.99 0 = f(0) | ~spl1_41),
% 3.77/0.99 inference(avatar_component_clause,[],[f1067])).
% 3.77/0.99 tff(f1070,plain,(
% 3.77/0.99 ~spl1_15 | spl1_41),
% 3.77/0.99 inference(avatar_split_clause,[],[f884,f1067,f520])).
% 3.77/0.99 tff(f1116,plain,(
% 3.77/0.99 -1 = f(0) | (~spl1_7 | ~spl1_41)),
% 3.77/0.99 inference(forward_demodulation,[],[f350,f1069])).
% 3.77/0.99 tff(f1117,plain,(
% 3.77/0.99 0 = -1 | (~spl1_7 | ~spl1_41)),
% 3.77/0.99 inference(forward_demodulation,[],[f1116,f1069])).
% 3.77/0.99 tff(f1118,plain,(
% 3.77/0.99 $false | (~spl1_7 | ~spl1_41)),
% 3.77/0.99 inference(evaluation,[],[f1117])).
% 3.77/0.99 tff(f1119,plain,(
% 3.77/0.99 ~spl1_7 | ~spl1_41),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f1118])).
% 3.77/0.99 tff(f1173,plain,(
% 3.77/0.99 $less(1,f(0)) | (~spl1_14 | ~spl1_41)),
% 3.77/0.99 inference(forward_demodulation,[],[f507,f1069])).
% 3.77/0.99 tff(f1174,plain,(
% 3.77/0.99 $less(1,0) | (~spl1_14 | ~spl1_41)),
% 3.77/0.99 inference(forward_demodulation,[],[f1173,f1069])).
% 3.77/0.99 tff(f1175,plain,(
% 3.77/0.99 $false | (~spl1_14 | ~spl1_41)),
% 3.77/0.99 inference(evaluation,[],[f1174])).
% 3.77/0.99 tff(f1176,plain,(
% 3.77/0.99 ~spl1_14 | ~spl1_41),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f1175])).
% 3.77/0.99 tff(f1333,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (f(X0) = $uminus(X0) | f(X0) = X0) )),
% 3.77/0.99 inference(resolution,[],[f328,f280])).
% 3.77/0.99 tff(f1345,plain,(
% 3.77/0.99 f(-1) = $uminus(-1) | $less(f(-1),0)),
% 3.77/0.99 inference(resolution,[],[f328,f62])).
% 3.77/0.99 tff(f1348,plain,(
% 3.77/0.99 1 = f(-1) | $less(f(-1),0)),
% 3.77/0.99 inference(evaluation,[],[f1345])).
% 3.77/0.99 tff(f1371,plain,(
% 3.77/0.99 1 = f(-1)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f1348,f407])).
% 3.77/0.99 tff(f3847,plain,(
% 3.77/0.99 ( ! [X0 : $int] : ($less($uminus(X0),0) | ~$less(1,X0)) )),
% 3.77/0.99 inference(resolution,[],[f623,f1019])).
% 3.77/0.99 tff(f3874,plain,(
% 3.77/0.99 ( ! [X0 : $int] : (~$less(1,X0) | g(X0) = X0) )),
% 3.77/0.99 inference(resolution,[],[f3847,f25])).
% 3.77/0.99 tff(f16162,plain,(
% 3.77/0.99 $uminus(sK0) != $uminus(sK0) | sK0 = f(sK0) | spl1_2),
% 3.77/0.99 inference(superposition,[],[f35,f1333])).
% 3.77/0.99 tff(f17167,plain,(
% 3.77/0.99 sK0 = f(sK0) | spl1_2),
% 3.77/0.99 inference(trivial_inequality_removal,[],[f16162])).
% 3.77/0.99 tff(f17915,plain,(
% 3.77/0.99 sK0 != $uminus(sK0) | spl1_2),
% 3.77/0.99 inference(superposition,[],[f35,f17167])).
% 3.77/0.99 tff(f17921,plain,(
% 3.77/0.99 ~$less(sK0,-1) | sK0 = g(sK0) | spl1_2),
% 3.77/0.99 inference(superposition,[],[f699,f17167])).
% 3.77/0.99 tff(f17940,plain,(
% 3.77/0.99 ~$less(sK0,-1) | (spl1_1 | spl1_2)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f17921,f30])).
% 3.77/0.99 tff(f17957,plain,(
% 3.77/0.99 $less(0,sK0) | 0 = sK0 | ~spl1_1),
% 3.77/0.99 inference(resolution,[],[f375,f11])).
% 3.77/0.99 tff(f17960,plain,(
% 3.77/0.99 spl1_9 | spl1_10 | ~spl1_1),
% 3.77/0.99 inference(avatar_split_clause,[],[f17957,f29,f384,f380])).
% 3.77/0.99 tff(f17965,plain,(
% 3.77/0.99 ~$less(sK0,1) | ~spl1_10),
% 3.77/0.99 inference(resolution,[],[f386,f164])).
% 3.77/0.99 tff(f17971,plain,(
% 3.77/0.99 $less(1,sK0) | 1 = sK0 | ~spl1_10),
% 3.77/0.99 inference(resolution,[],[f17965,f11])).
% 3.77/0.99 tff(f17974,definition,(
% 3.77/0.99 spl1_446 <=> 1 = sK0),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_446])],[avatar_definition])).
% 3.77/0.99 tff(f17975,plain,(
% 3.77/0.99 1 != sK0 | spl1_446),
% 3.77/0.99 inference(avatar_component_clause,[],[f17974])).
% 3.77/0.99 tff(f17976,plain,(
% 3.77/0.99 1 = sK0 | ~spl1_446),
% 3.77/0.99 inference(avatar_component_clause,[],[f17974])).
% 3.77/0.99 tff(f17978,definition,(
% 3.77/0.99 spl1_447 <=> $less(1,sK0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_447])],[avatar_definition])).
% 3.77/0.99 tff(f17980,plain,(
% 3.77/0.99 $less(1,sK0) | ~spl1_447),
% 3.77/0.99 inference(avatar_component_clause,[],[f17978])).
% 3.77/0.99 tff(f17982,plain,(
% 3.77/0.99 spl1_446 | spl1_447 | ~spl1_10),
% 3.77/0.99 inference(avatar_split_clause,[],[f17971,f384,f17978,f17974])).
% 3.77/0.99 tff(f17983,plain,(
% 3.77/0.99 f(1) != g(1) | ~spl1_446),
% 3.77/0.99 inference(superposition,[],[f24,f17976])).
% 3.77/0.99 tff(f17989,plain,(
% 3.77/0.99 1 != f(1) | ~spl1_446),
% 3.77/0.99 inference(forward_demodulation,[],[f17983,f97])).
% 3.77/0.99 tff(f17990,plain,(
% 3.77/0.99 $false | ~spl1_446),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f17989,f326])).
% 3.77/0.99 tff(f17991,plain,(
% 3.77/0.99 ~spl1_446),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f17990])).
% 3.77/0.99 tff(f18003,plain,(
% 3.77/0.99 ~$less(f(sK0),-1) | ~spl1_1),
% 3.77/0.99 inference(superposition,[],[f679,f31])).
% 3.77/0.99 tff(f18109,plain,(
% 3.77/0.99 ~$less($uminus(sK0),-1) | sK0 = f(sK0) | ~spl1_1),
% 3.77/0.99 inference(superposition,[],[f18003,f1333])).
% 3.77/0.99 tff(f18110,plain,(
% 3.77/0.99 ~$less($uminus(sK0),-1) | ~spl1_1),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18109,f373])).
% 3.77/0.99 tff(f18121,plain,(
% 3.77/0.99 $less(-1,$uminus(sK0)) | $uminus(sK0) = -1 | ~spl1_1),
% 3.77/0.99 inference(resolution,[],[f18110,f11])).
% 3.77/0.99 tff(f18124,definition,(
% 3.77/0.99 spl1_451 <=> $uminus(sK0) = -1),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_451])],[avatar_definition])).
% 3.77/0.99 tff(f18126,plain,(
% 3.77/0.99 $uminus(sK0) = -1 | ~spl1_451),
% 3.77/0.99 inference(avatar_component_clause,[],[f18124])).
% 3.77/0.99 tff(f18128,definition,(
% 3.77/0.99 spl1_452 <=> $less(-1,$uminus(sK0))),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_452])],[avatar_definition])).
% 3.77/0.99 tff(f18130,plain,(
% 3.77/0.99 $less(-1,$uminus(sK0)) | ~spl1_452),
% 3.77/0.99 inference(avatar_component_clause,[],[f18128])).
% 3.77/0.99 tff(f18132,plain,(
% 3.77/0.99 spl1_451 | spl1_452 | ~spl1_1),
% 3.77/0.99 inference(avatar_split_clause,[],[f18121,f29,f18128,f18124])).
% 3.77/0.99 tff(f18168,definition,(
% 3.77/0.99 spl1_453 <=> sK0 = -1),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_453])],[avatar_definition])).
% 3.77/0.99 tff(f18170,plain,(
% 3.77/0.99 sK0 = -1 | ~spl1_453),
% 3.77/0.99 inference(avatar_component_clause,[],[f18168])).
% 3.77/0.99 tff(f18192,plain,(
% 3.77/0.99 sK0 = $uminus(-1) | ~spl1_451),
% 3.77/0.99 inference(superposition,[],[f14,f18126])).
% 3.77/0.99 tff(f18229,plain,(
% 3.77/0.99 1 = sK0 | ~spl1_451),
% 3.77/0.99 inference(evaluation,[],[f18192])).
% 3.77/0.99 tff(f18244,plain,(
% 3.77/0.99 $false | (spl1_446 | ~spl1_451)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18229,f17975])).
% 3.77/0.99 tff(f18245,plain,(
% 3.77/0.99 spl1_446 | ~spl1_451),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18244])).
% 3.77/0.99 tff(f18253,plain,(
% 3.77/0.99 ~$less($uminus(sK0),0) | ~spl1_452),
% 3.77/0.99 inference(resolution,[],[f18130,f117])).
% 3.77/0.99 tff(f18272,plain,(
% 3.77/0.99 ~$less(1,sK0) | ~spl1_452),
% 3.77/0.99 inference(resolution,[],[f18253,f3847])).
% 3.77/0.99 tff(f18286,plain,(
% 3.77/0.99 $false | (~spl1_447 | ~spl1_452)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18272,f17980])).
% 3.77/0.99 tff(f18287,plain,(
% 3.77/0.99 ~spl1_447 | ~spl1_452),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18286])).
% 3.77/0.99 tff(f18290,plain,(
% 3.77/0.99 $less(sK0,0) | 0 = sK0 | spl1_10),
% 3.77/0.99 inference(resolution,[],[f385,f11])).
% 3.77/0.99 tff(f18291,plain,(
% 3.77/0.99 $less(sK0,0) | (spl1_9 | spl1_10)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18290,f381])).
% 3.77/0.99 tff(f18348,plain,(
% 3.77/0.99 $less(-1,sK0) | sK0 = -1 | (spl1_1 | spl1_2)),
% 3.77/0.99 inference(resolution,[],[f17940,f11])).
% 3.77/0.99 tff(f18351,definition,(
% 3.77/0.99 spl1_459 <=> $less(-1,sK0)),
% 3.77/0.99 introduced(definition,[new_symbols(definition,[spl1_459])],[avatar_definition])).
% 3.77/0.99 tff(f18353,plain,(
% 3.77/0.99 $less(-1,sK0) | ~spl1_459),
% 3.77/0.99 inference(avatar_component_clause,[],[f18351])).
% 3.77/0.99 tff(f18355,plain,(
% 3.77/0.99 spl1_453 | spl1_459 | spl1_1 | spl1_2),
% 3.77/0.99 inference(avatar_split_clause,[],[f18348,f33,f29,f18351,f18168])).
% 3.77/0.99 tff(f18356,plain,(
% 3.77/0.99 ~$less(sK0,0) | ~spl1_459),
% 3.77/0.99 inference(resolution,[],[f18353,f117])).
% 3.77/0.99 tff(f18360,plain,(
% 3.77/0.99 $false | (spl1_9 | spl1_10 | ~spl1_459)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18356,f18291])).
% 3.77/0.99 tff(f18361,plain,(
% 3.77/0.99 spl1_9 | spl1_10 | ~spl1_459),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18360])).
% 3.77/0.99 tff(f18366,plain,(
% 3.77/0.99 -1 = f(-1) | (spl1_2 | ~spl1_453)),
% 3.77/0.99 inference(superposition,[],[f17167,f18170])).
% 3.77/0.99 tff(f18382,plain,(
% 3.77/0.99 1 = -1 | (spl1_2 | ~spl1_453)),
% 3.77/0.99 inference(forward_demodulation,[],[f18366,f1371])).
% 3.77/0.99 tff(f18383,plain,(
% 3.77/0.99 $false | (spl1_2 | ~spl1_453)),
% 3.77/0.99 inference(evaluation,[],[f18382])).
% 3.77/0.99 tff(f18384,plain,(
% 3.77/0.99 spl1_2 | ~spl1_453),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18383])).
% 3.77/0.99 tff(f18396,plain,(
% 3.77/0.99 sK0 = g(sK0) | ~spl1_447),
% 3.77/0.99 inference(resolution,[],[f17980,f3874])).
% 3.77/0.99 tff(f18400,plain,(
% 3.77/0.99 $false | (spl1_1 | ~spl1_447)),
% 3.77/0.99 inference(forward_subsumption_resolution,[],[f18396,f30])).
% 3.77/0.99 tff(f18401,plain,(
% 3.77/0.99 spl1_1 | ~spl1_447),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18400])).
% 3.77/0.99 tff(f18405,plain,(
% 3.77/0.99 0 != $uminus(0) | (spl1_2 | ~spl1_9)),
% 3.77/0.99 inference(superposition,[],[f17915,f382])).
% 3.77/0.99 tff(f18414,plain,(
% 3.77/0.99 $false | (spl1_2 | ~spl1_9)),
% 3.77/0.99 inference(evaluation,[],[f18405])).
% 3.77/0.99 tff(f18415,plain,(
% 3.77/0.99 spl1_2 | ~spl1_9),
% 3.77/0.99 inference(avatar_contradiction_clause,[],[f18414])).
% 3.77/0.99 cnf(s1, plain, spl1_1 | ~spl1_2, inference(sat_conversion,[],[f36])).
% 3.77/0.99 cnf(s7, plain, spl1_7 | spl1_8, inference(sat_conversion,[],[f361])).
% 3.77/0.99 cnf(s11, plain, ~spl1_8 | spl1_11 | spl1_12, inference(sat_conversion,[],[f423])).
% 3.77/0.99 cnf(s13, plain, ~spl1_1 | ~spl1_9 | ~spl1_11, inference(sat_conversion,[],[f472])).
% 3.77/0.99 cnf(s15, plain, ~spl1_12 | spl1_13 | spl1_14, inference(sat_conversion,[],[f509])).
% 3.77/0.99 cnf(s16, plain, ~spl1_13 | ~spl1_15 | ~spl1_16, inference(sat_conversion,[],[f527])).
% 3.77/0.99 cnf(s20, plain, ~spl1_13 | spl1_16 | spl1_18, inference(sat_conversion,[],[f545])).
% 3.77/0.99 cnf(s24, plain, ~spl1_18, inference(sat_conversion,[],[f602])).
% 3.77/0.99 cnf(s25, plain, ~spl1_17, inference(sat_conversion,[],[f648])).
% 3.77/0.99 cnf(s27, plain, spl1_15 | spl1_17 | spl1_20, inference(sat_conversion,[],[f657])).
% 3.77/0.99 cnf(s47, plain, spl1_15 | ~spl1_20, inference(sat_conversion,[],[f1065])).
% 3.77/0.99 cnf(s48, plain, ~spl1_15 | spl1_41, inference(sat_conversion,[],[f1070])).
% 3.77/0.99 cnf(s49, plain, ~spl1_7 | ~spl1_41, inference(sat_conversion,[],[f1119])).
% 3.77/0.99 cnf(s58, plain, ~spl1_14 | ~spl1_41, inference(sat_conversion,[],[f1176])).
% 3.77/0.99 cnf(s1135, plain, ~spl1_1 | spl1_9 | spl1_10, inference(sat_conversion,[],[f17960])).
% 3.77/0.99 cnf(s1137, plain, ~spl1_10 | spl1_446 | spl1_447, inference(sat_conversion,[],[f17982])).
% 3.77/0.99 cnf(s1138, plain, ~spl1_446, inference(sat_conversion,[],[f17991])).
% 3.77/0.99 cnf(s1147, plain, ~spl1_1 | spl1_451 | spl1_452, inference(sat_conversion,[],[f18132])).
% 3.77/0.99 cnf(s1151, plain, spl1_446 | ~spl1_451, inference(sat_conversion,[],[f18245])).
% 3.77/0.99 cnf(s1158, plain, ~spl1_447 | ~spl1_452, inference(sat_conversion,[],[f18287])).
% 3.77/0.99 cnf(s1160, plain, spl1_1 | spl1_2 | spl1_453 | spl1_459, inference(sat_conversion,[],[f18355])).
% 3.77/0.99 cnf(s1161, plain, spl1_9 | spl1_10 | ~spl1_459, inference(sat_conversion,[],[f18361])).
% 3.77/0.99 cnf(s1164, plain, spl1_2 | ~spl1_453, inference(sat_conversion,[],[f18384])).
% 3.77/0.99 cnf(s1165, plain, spl1_1 | ~spl1_447, inference(sat_conversion,[],[f18401])).
% 3.77/0.99 cnf(s1167, plain, spl1_2 | ~spl1_9, inference(sat_conversion,[],[f18415])).
% 3.77/0.99 cnf(s1168, plain, ~spl1_451, inference(rat,[],[s1151,s1138])).
% 3.77/0.99 cnf(s1169, plain, ~spl1_10 | spl1_447, inference(rat,[],[s1137,s1138])).
% 3.77/0.99 cnf(s1513, plain, ~spl1_13 | spl1_16, inference(rat,[],[s20,s24])).
% 3.77/0.99 cnf(s1517, plain, spl1_1, inference(rat,[],[s1160,s1161,s1164,s1167,s1169,s1,s1165])).
% 3.77/0.99 cnf(s1519, plain, spl1_452, inference(rat,[],[s1147,s1168,s1517])).
% 3.77/0.99 cnf(s1522, plain, ~spl1_447, inference(rat,[],[s1158,s1519])).
% 3.77/0.99 cnf(s1523, plain, ~spl1_10, inference(rat,[],[s1169,s1522])).
% 3.77/0.99 cnf(s1524, plain, spl1_9, inference(rat,[],[s1135,s1517,s1523])).
% 3.77/0.99 cnf(s1527, plain, ~spl1_11, inference(rat,[],[s13,s1517,s1524])).
% 3.77/0.99 cnf(s1529, plain, spl1_15, inference(rat,[],[s27,s47,s25])).
% 3.77/0.99 cnf(s1530, plain, spl1_41, inference(rat,[],[s48,s1529])).
% 3.77/0.99 cnf(s1532, plain, ~spl1_14, inference(rat,[],[s58,s1530])).
% 3.77/0.99 cnf(s1533, plain, ~spl1_7, inference(rat,[],[s49,s1530])).
% 3.77/0.99 cnf(s1535, plain, spl1_8, inference(rat,[],[s7,s1533])).
% 3.77/0.99 cnf(s1537, plain, spl1_12, inference(rat,[],[s11,s1527,s1535])).
% 3.77/0.99 cnf(s1538, plain, spl1_13, inference(rat,[],[s15,s1532,s1537])).
% 3.77/0.99 cnf(s1539, plain, spl1_16, inference(rat,[],[s1513,s1538])).
% 3.77/0.99 cnf(s1540, plain, $false, inference(rat,[],[s16,s1529,s1539,s1538])).
% 3.77/0.99 tff(f18418,plain,(
% 3.77/0.99 $false),
% 3.77/0.99 inference(avatar_sat_refutation,[],[s1540])).
% 3.77/0.99 % SZS output end Proof for theBenchmark
% 3.77/0.99 % (4012287)------------------------------
% 3.77/0.99 % (4012287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.77/0.99 % (4012287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/0.99 % (4012287)CaDiCaL version: 2.1.3
% 3.77/0.99 % (4012287)Termination reason: Refutation
% 3.77/0.99 % (4012287)Time elapsed: 0.513 s
% 3.77/0.99 % (4012287)Peak memory usage: 18 MB
% 3.77/0.99 % (4012287)Instructions burned: 477 (million)
% 3.77/0.99 % (4012264)Success in time 0.681 s
% 3.77/0.99 % Vampire exiting
%------------------------------------------------------------------------------