%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX107_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 01:46:30 PM UTC 2026
% Result : Theorem 1.02s 0.39s
% Output : Refutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX107_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n008.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:02:25 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.02/0.39 % (2314502)Will run a generic schedule for satisfiability detection.
% 1.02/0.39 % (2314507)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1073950062_2999 on theBenchmark for (2999ds/0Mi)
% 1.02/0.39 % (2314507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.02/0.39 % (2314507)Terminated due to inappropriate strategy.
% 1.02/0.39 % (2314507)------------------------------
% 1.02/0.39 % (2314507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314507)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314507)Termination reason: Inappropriate
% 1.02/0.39 % (2314507)Time elapsed: 0.001 s
% 1.02/0.39 % (2314507)Peak memory usage: 11 MB
% 1.02/0.39 % (2314507)Instructions burned: 3 (million)
% 1.02/0.39 % (2314507)------------------------------
% 1.02/0.39 % (2314507)------------------------------
% 1.02/0.39 % (2314508)% WARNING: option uhcvi not known.
% 1.02/0.39 % (2314509)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3744758297:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.02/0.39 % (2314508)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=637470085:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.02/0.39 % (2314510)dis+10_1_sil=32000:sp=arity:random_seed=952986568:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.02/0.39 % (2314512)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=977594011:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.39 % (2314511)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1971639459:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.02/0.39 % (2314513)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=302245846:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.02/0.39 % (2314515)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1828766441:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.02/0.39 % (2314515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.02/0.39 % (2314515)Terminated due to inappropriate strategy.
% 1.02/0.39 % (2314515)------------------------------
% 1.02/0.39 % (2314515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314515)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314515)Termination reason: Inappropriate
% 1.02/0.39 % (2314515)Time elapsed: 0.001 s
% 1.02/0.39 % (2314515)Peak memory usage: 11 MB
% 1.02/0.39 % (2314515)Instructions burned: 2 (million)
% 1.02/0.39 % (2314515)------------------------------
% 1.02/0.39 % (2314515)------------------------------
% 1.02/0.39 % (2314523)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1412846149:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.02/0.39 % (2314523)Instruction limit reached!
% 1.02/0.39 % (2314523)------------------------------
% 1.02/0.39 % (2314523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314523)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314523)Termination reason: Instruction limit
% 1.02/0.39 % (2314523)Termination phase: Saturation
% 1.02/0.39 % (2314523)Time elapsed: 0.050 s
% 1.02/0.39 % (2314523)Peak memory usage: 13 MB
% 1.02/0.39 % (2314523)Instructions burned: 133 (million)
% 1.02/0.39 % (2314510)Instruction limit reached!
% 1.02/0.39 % (2314510)------------------------------
% 1.02/0.39 % (2314510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314510)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314510)Termination reason: Instruction limit
% 1.02/0.39 % (2314510)Termination phase: Saturation
% 1.02/0.39 % (2314510)Time elapsed: 0.067 s
% 1.02/0.39 % (2314510)Peak memory usage: 13 MB
% 1.02/0.39 % (2314510)Instructions burned: 104 (million)
% 1.02/0.39 % (2314511)Instruction limit reached!
% 1.02/0.39 % (2314511)------------------------------
% 1.02/0.39 % (2314511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314511)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314511)Termination reason: Instruction limit
% 1.02/0.39 % (2314511)Termination phase: Saturation
% 1.02/0.39 % (2314511)Time elapsed: 0.076 s
% 1.02/0.39 % (2314511)Peak memory usage: 13 MB
% 1.02/0.39 % (2314511)Instructions burned: 119 (million)
% 1.02/0.39 % (2314525)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=3301748824:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.02/0.39 % (2314512)Instruction limit reached!
% 1.02/0.39 % (2314512)------------------------------
% 1.02/0.39 % (2314512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314512)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314512)Termination reason: Instruction limit
% 1.02/0.39 % (2314512)Termination phase: Saturation
% 1.02/0.39 % (2314512)Time elapsed: 0.083 s
% 1.02/0.39 % (2314512)Peak memory usage: 13 MB
% 1.02/0.39 % (2314512)Instructions burned: 132 (million)
% 1.02/0.39 % (2314526)ott-21_1_sil=16000:fs=off:random_seed=1115296218:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.02/0.39 % (2314527)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=29663432:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.02/0.39 % (2314529)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3262243224:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.02/0.39 % (2314529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.02/0.39 % (2314529)Terminated due to inappropriate strategy.
% 1.02/0.39 % (2314529)------------------------------
% 1.02/0.39 % (2314529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314529)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314529)Termination reason: Inappropriate
% 1.02/0.39 % (2314529)Time elapsed: 0.001 s
% 1.02/0.39 % (2314529)Peak memory usage: 10 MB
% 1.02/0.39 % (2314529)Instructions burned: 2 (million)
% 1.02/0.39 % (2314529)------------------------------
% 1.02/0.39 % (2314529)------------------------------
% 1.02/0.39 % (2314513)Instruction limit reached!
% 1.02/0.39 % (2314513)------------------------------
% 1.02/0.39 % (2314513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.39 % (2314513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.39 % (2314513)CaDiCaL version: 2.1.3
% 1.02/0.39 % (2314513)Termination reason: Instruction limit
% 1.02/0.39 % (2314513)Termination phase: Saturation
% 1.02/0.39 % (2314513)Time elapsed: 0.113 s
% 1.02/0.39 % (2314513)Peak memory usage: 13 MB
% 1.02/0.39 % (2314513)Instructions burned: 160 (million)
% 1.02/0.39 % (2314508) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2314502-2314508"...
% 1.02/0.39 % (2314533)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2858638988:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.02/0.39 % (2314508)...printing done.
% 1.02/0.39 % (2314508)Refutation found. Thanks to Tanya!
% 1.02/0.39 % SZS status Theorem for theBenchmark
% 1.02/0.39 % SZS output start Proof for theBenchmark
% 1.02/0.39 tff(type_def_5, type, general: $tType).
% 1.02/0.39 tff(type_def_6, type, symbol: $tType).
% 1.02/0.39 tff(func_def_0, type, f__integer__: $int > general).
% 1.02/0.39 tff(func_def_1, type, f__symbolic__: symbol > general).
% 1.02/0.39 tff(func_def_2, type, c__infimum__: general).
% 1.02/0.39 tff(func_def_3, type, c__supremum__: general).
% 1.02/0.39 tff(func_def_9, type, sK0: general > $int).
% 1.02/0.39 tff(func_def_10, type, sK1: general > symbol).
% 1.02/0.39 tff(func_def_11, type, sK2: general).
% 1.02/0.39 tff(func_def_12, type, sK3: general).
% 1.02/0.39 tff(func_def_13, type, sK4: general).
% 1.02/0.39 tff(func_def_14, type, sK5: general).
% 1.02/0.39 tff(func_def_15, type, sK6: general).
% 1.02/0.39 tff(func_def_16, type, sK7: general).
% 1.02/0.39 tff(func_def_17, type, sK8: general).
% 1.02/0.39 tff(func_def_18, type, sK9: general).
% 1.02/0.39 tff(func_def_19, type, sK10: general).
% 1.02/0.39 tff(func_def_20, type, sK11: general).
% 1.02/0.39 tff(func_def_21, type, sK12: general).
% 1.02/0.39 tff(func_def_22, type, sK13: $int).
% 1.02/0.39 tff(func_def_23, type, sK14: $int).
% 1.02/0.39 tff(func_def_24, type, sK15: $int).
% 1.02/0.39 tff(func_def_25, type, sK16: $int).
% 1.02/0.39 tff(func_def_26, type, sK17: $int).
% 1.02/0.39 tff(func_def_27, type, sK18: $int).
% 1.02/0.39 tff(func_def_28, type, sK19: $int).
% 1.02/0.39 tff(func_def_29, type, sK20: $int).
% 1.02/0.39 tff(func_def_30, type, sK21: $int).
% 1.02/0.39 tff(func_def_31, type, sK22: $int).
% 1.02/0.39 tff(pred_def_1, type, p__is_integer__: general > $o).
% 1.02/0.39 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 1.02/0.39 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 1.02/0.39 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 1.02/0.39 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 1.02/0.39 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 1.02/0.39 tff(pred_def_8, type, hp: general > $o).
% 1.02/0.39 tff(pred_def_9, type, tp: general > $o).
% 1.02/0.39 tff(pred_def_11, type, sP23: ($int * $int * general * general) > $o).
% 1.02/0.39 tff(pred_def_12, type, sP24: ($int * $int * $int * general) > $o).
% 1.02/0.39 tff(f4,axiom,(
% 1.02/0.39 ! [X0 : $int,X1 : $int] : (f__integer__(X0) = f__integer__(X1) <=> X0 = X1)),
% 1.02/0.39 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',f__integer__def_ax)).
% 1.02/0.39 tff(f16,axiom,(
% 1.02/0.39 ! [X0 : general] : (hp(X0) => tp(X0))),
% 1.02/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_0_transition_axiom_0)).
% 1.02/0.39 tff(f17,axiom,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = 0 & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => hp(X0)) & ((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = 0 & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => tp(X0)))),
% 1.02/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1_left_0)).
% 1.02/0.39 tff(f18,conjecture,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => hp(X0)) & ((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => tp(X0)))),
% 1.02/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_right_0)).
% 1.02/0.39 tff(f19,negated_conjecture,(
% 1.02/0.39 ~ ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => hp(X0)) & ((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & $lesseq(X5,X7) & $lesseq(X7,X6)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => tp(X0)))),
% 1.02/0.39 inference(negated_conjecture,[status(cth)],[f18])).
% 1.02/0.39 tff(f21,plain,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = 0 & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => hp(X0)) & ((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = 0 & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => tp(X0)))),
% 1.02/0.39 inference(theory_normalization,[],[f17])).
% 1.02/0.39 tff(f22,plain,(
% 1.02/0.39 ~ ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => hp(X0)) & ((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X3 : general,X4 : general] : (X3 = X2 & ? [X5 : $int,X6 : $int] : (X4 = f__integer__($product(X5,X6)) & f__integer__(X5) = X1 & f__integer__(X6) = X1) & X3 = X4)) => tp(X0)))),
% 1.02/0.39 inference(theory_normalization,[],[f19])).
% 1.02/0.39 tff(f30,definition,(
% 1.02/0.39 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 1.02/0.39 introduced(theory,[tha_order_totality])).
% 1.02/0.39 tff(f36,definition,(
% 1.02/0.39 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 1.02/0.39 introduced(theory,[tha_right_identity])).
% 1.02/0.39 tff(f40,definition,(
% 1.02/0.39 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(X0,1))) )),
% 1.02/0.39 introduced(theory,[tha_extra_integer_ordering])).
% 1.02/0.39 tff(f41,plain,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = 0 & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X8 : general,X9 : general] : (X2 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) = X9 & f__integer__(X10) = X1 & f__integer__(X11) = X1) & X8 = X9)) => hp(X0)) & ((X0 = X2 & ? [X12 : general,X13 : general] : (X1 = X12 & ? [X14 : $int,X15 : $int,X16 : $int] : (0 = X14 & 1 = X15 & f__integer__(X16) = X13 & ~$less(X16,X14) & ~$less(X15,X16)) & X12 = X13) & ? [X17 : general,X18 : general] : (X2 = X17 & ? [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) = X18 & f__integer__(X19) = X1 & f__integer__(X20) = X1) & X17 = X18)) => tp(X0)))),
% 1.02/0.39 inference(rectify,[],[f21])).
% 1.02/0.39 tff(f42,plain,(
% 1.02/0.39 ~ ! [X0 : general,X1 : general,X2 : general] : (((X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X8 : general,X9 : general] : (X2 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) = X9 & f__integer__(X10) = X1 & f__integer__(X11) = X1) & X8 = X9)) => hp(X0)) & ((X0 = X2 & ? [X12 : general,X13 : general] : (X1 = X12 & ? [X14 : $int,X15 : $int,X16 : $int] : ($uminus(1) = X14 & 1 = X15 & f__integer__(X16) = X13 & ~$less(X16,X14) & ~$less(X15,X16)) & X12 = X13) & ? [X17 : general,X18 : general] : (X2 = X17 & ? [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) = X18 & f__integer__(X19) = X1 & f__integer__(X20) = X1) & X17 = X18)) => tp(X0)))),
% 1.02/0.39 inference(rectify,[],[f22])).
% 1.02/0.39 tff(f53,plain,(
% 1.02/0.39 ! [X0 : general] : (tp(X0) | ~hp(X0))),
% 1.02/0.39 inference(ennf_transformation,[],[f16])).
% 1.02/0.39 tff(f54,plain,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : ((hp(X0) | (X0 != X2 | ! [X3 : general,X4 : general] : (X1 != X3 | ! [X5 : $int,X6 : $int,X7 : $int] : (0 != X5 | 1 != X6 | f__integer__(X7) != X4 | $less(X7,X5) | $less(X6,X7)) | X3 != X4) | ! [X8 : general,X9 : general] : (X2 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) != X9 | f__integer__(X10) != X1 | f__integer__(X11) != X1) | X8 != X9))) & (tp(X0) | (X0 != X2 | ! [X12 : general,X13 : general] : (X1 != X12 | ! [X14 : $int,X15 : $int,X16 : $int] : (0 != X14 | 1 != X15 | f__integer__(X16) != X13 | $less(X16,X14) | $less(X15,X16)) | X12 != X13) | ! [X17 : general,X18 : general] : (X2 != X17 | ! [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) != X18 | f__integer__(X19) != X1 | f__integer__(X20) != X1) | X17 != X18))))),
% 1.02/0.39 inference(ennf_transformation,[],[f41])).
% 1.02/0.39 tff(f55,plain,(
% 1.02/0.39 ! [X0 : general,X1 : general,X2 : general] : ((hp(X0) | X0 != X2 | ! [X3 : general,X4 : general] : (X1 != X3 | ! [X5 : $int,X6 : $int,X7 : $int] : (0 != X5 | 1 != X6 | f__integer__(X7) != X4 | $less(X7,X5) | $less(X6,X7)) | X3 != X4) | ! [X8 : general,X9 : general] : (X2 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) != X9 | f__integer__(X10) != X1 | f__integer__(X11) != X1) | X8 != X9)) & (tp(X0) | X0 != X2 | ! [X12 : general,X13 : general] : (X1 != X12 | ! [X14 : $int,X15 : $int,X16 : $int] : (0 != X14 | 1 != X15 | f__integer__(X16) != X13 | $less(X16,X14) | $less(X15,X16)) | X12 != X13) | ! [X17 : general,X18 : general] : (X2 != X17 | ! [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) != X18 | f__integer__(X19) != X1 | f__integer__(X20) != X1) | X17 != X18)))),
% 1.02/0.39 inference(flattening,[],[f54])).
% 1.02/0.39 tff(f56,plain,(
% 1.02/0.39 ? [X0 : general,X1 : general,X2 : general] : ((~hp(X0) & (X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X8 : general,X9 : general] : (X2 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) = X9 & f__integer__(X10) = X1 & f__integer__(X11) = X1) & X8 = X9))) | (~tp(X0) & (X0 = X2 & ? [X12 : general,X13 : general] : (X1 = X12 & ? [X14 : $int,X15 : $int,X16 : $int] : ($uminus(1) = X14 & 1 = X15 & f__integer__(X16) = X13 & ~$less(X16,X14) & ~$less(X15,X16)) & X12 = X13) & ? [X17 : general,X18 : general] : (X2 = X17 & ? [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) = X18 & f__integer__(X19) = X1 & f__integer__(X20) = X1) & X17 = X18))))),
% 1.02/0.39 inference(ennf_transformation,[],[f42])).
% 1.02/0.39 tff(f57,plain,(
% 1.02/0.39 ? [X0 : general,X1 : general,X2 : general] : ((~hp(X0) & X0 = X2 & ? [X3 : general,X4 : general] : (X3 = X1 & ? [X5 : $int,X6 : $int,X7 : $int] : (X5 = $uminus(1) & X6 = 1 & X4 = f__integer__(X7) & ~$less(X7,X5) & ~$less(X6,X7)) & X3 = X4) & ? [X8 : general,X9 : general] : (X2 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($product(X10,X11)) = X9 & f__integer__(X10) = X1 & f__integer__(X11) = X1) & X8 = X9)) | (~tp(X0) & X0 = X2 & ? [X12 : general,X13 : general] : (X1 = X12 & ? [X14 : $int,X15 : $int,X16 : $int] : ($uminus(1) = X14 & 1 = X15 & f__integer__(X16) = X13 & ~$less(X16,X14) & ~$less(X15,X16)) & X12 = X13) & ? [X17 : general,X18 : general] : (X2 = X17 & ? [X19 : $int,X20 : $int] : (f__integer__($product(X19,X20)) = X18 & f__integer__(X19) = X1 & f__integer__(X20) = X1) & X17 = X18)))),
% 1.02/0.39 inference(flattening,[],[f56])).
% 1.02/0.39 tff(f62,plain,(
% 1.02/0.39 ( ! [X0 : $int,X1 : $int] : (f__integer__(X1) != f__integer__(X0) | X0 = X1) )),
% 1.02/0.39 inference(cnf_transformation,[],[f4])).
% 1.02/0.39 tff(f75,plain,(
% 1.02/0.39 ( ! [X0 : general] : (~hp(X0) | tp(X0)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f53])).
% 1.02/0.39 tff(f76,plain,(
% 1.02/0.39 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X1 : general,X8 : general,X6 : $int,X9 : general,X7 : $int,X4 : general,X5 : $int] : (X8 != X9 | f__integer__(X11) != X1 | f__integer__(X10) != X1 | f__integer__($product(X10,X11)) != X9 | X2 != X8 | X3 != X4 | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | X1 != X3 | X0 != X2 | hp(X0)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f55])).
% 1.02/0.39 tff(f77,plain,(
% 1.02/0.39 ( ! [X2 : general,X0 : general,X18 : general,X1 : general,X19 : $int,X16 : $int,X14 : $int,X17 : general,X15 : $int,X12 : general,X13 : general,X20 : $int] : (X17 != X18 | f__integer__(X20) != X1 | f__integer__(X19) != X1 | f__integer__($product(X19,X20)) != X18 | X2 != X17 | X12 != X13 | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | X1 != X12 | X0 != X2 | tp(X0)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f55])).
% 1.02/0.39 tff(f78,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : (~sP24(X7,X6,X5,X4) | ~$less(X6,X7)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f79,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : (~sP24(X7,X6,X5,X4) | ~$less(X7,X5)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f80,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : (~sP24(X7,X6,X5,X4) | f__integer__(X7) = X4) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f81,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : (~sP24(X7,X6,X5,X4) | 1 = X6) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f82,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : ($uminus(1) = X5 | ~sP24(X7,X6,X5,X4)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f83,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (f__integer__(X11) = X1 | ~sP23(X11,X10,X9,X1)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f84,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (f__integer__(X10) = X1 | ~sP23(X11,X10,X9,X1)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f85,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (f__integer__($product(X10,X11)) = X9 | ~sP23(X11,X10,X9,X1)) )),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f96,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f97,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f98,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f99,plain,(
% 1.02/0.39 1 = sK16 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f100,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f101,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f102,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f103,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f104,plain,(
% 1.02/0.39 1 = sK16 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f105,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f106,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f107,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f108,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f109,plain,(
% 1.02/0.39 1 = sK16 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f110,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f111,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f112,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f113,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f114,plain,(
% 1.02/0.39 1 = sK16 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f115,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f116,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f117,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f118,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f119,plain,(
% 1.02/0.39 1 = sK16 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f120,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f121,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f122,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f123,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f124,plain,(
% 1.02/0.39 1 = sK16 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f125,plain,(
% 1.02/0.39 $uminus(1) = sK15 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f132,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f133,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f134,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f135,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f136,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f137,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f138,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f139,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f140,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f141,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f142,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f143,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f144,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f145,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f146,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f147,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f148,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f149,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f153,plain,(
% 1.02/0.39 ~tp(sK2) | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f154,plain,(
% 1.02/0.39 ~tp(sK2) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f155,plain,(
% 1.02/0.39 ~tp(sK2) | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f156,plain,(
% 1.02/0.39 sK4 = sK5 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f157,plain,(
% 1.02/0.39 sK4 = sK5 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f158,plain,(
% 1.02/0.39 sK4 = sK5 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f159,plain,(
% 1.02/0.39 sK5 = sK6 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f160,plain,(
% 1.02/0.39 sK5 = sK6 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f161,plain,(
% 1.02/0.39 sK5 = sK6 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f162,plain,(
% 1.02/0.39 sK3 = sK7 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f163,plain,(
% 1.02/0.39 sK3 = sK7 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f164,plain,(
% 1.02/0.39 sK3 = sK7 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f165,plain,(
% 1.02/0.39 sK7 = sK8 | sK11 = sK12),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f166,plain,(
% 1.02/0.39 sK7 = sK8 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f167,plain,(
% 1.02/0.39 sK7 = sK8 | sK3 = sK11),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f171,plain,(
% 1.02/0.39 ~tp(sK2) | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f172,plain,(
% 1.02/0.39 ~tp(sK2) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f173,plain,(
% 1.02/0.39 ~tp(sK2) | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f174,plain,(
% 1.02/0.39 sK4 = sK5 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f175,plain,(
% 1.02/0.39 sK4 = sK5 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f176,plain,(
% 1.02/0.39 sK4 = sK5 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f177,plain,(
% 1.02/0.39 sK5 = sK6 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f178,plain,(
% 1.02/0.39 sK5 = sK6 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f179,plain,(
% 1.02/0.39 sK5 = sK6 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f180,plain,(
% 1.02/0.39 sK3 = sK7 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f181,plain,(
% 1.02/0.39 sK3 = sK7 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f182,plain,(
% 1.02/0.39 sK3 = sK7 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f183,plain,(
% 1.02/0.39 sK7 = sK8 | sK9 = sK10),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f184,plain,(
% 1.02/0.39 sK7 = sK8 | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f185,plain,(
% 1.02/0.39 sK7 = sK8 | sK4 = sK9),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f195,plain,(
% 1.02/0.39 ~tp(sK2) | ~hp(sK2)),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f196,plain,(
% 1.02/0.39 sK2 = sK4),
% 1.02/0.39 inference(cnf_transformation,[],[f57])).
% 1.02/0.39 tff(f199,plain,(
% 1.02/0.39 ~tp(sK4) | ~hp(sK4)),
% 1.02/0.39 inference(definition_unfolding,[],[f195,f196,f196])).
% 1.02/0.39 tff(f209,plain,(
% 1.02/0.39 ~tp(sK4) | sK4 = sK9),
% 1.02/0.39 inference(definition_unfolding,[],[f173,f196])).
% 1.02/0.39 tff(f210,plain,(
% 1.02/0.39 ~tp(sK4) | sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(definition_unfolding,[],[f172,f196])).
% 1.02/0.39 tff(f211,plain,(
% 1.02/0.39 ~tp(sK4) | sK9 = sK10),
% 1.02/0.39 inference(definition_unfolding,[],[f171,f196])).
% 1.02/0.39 tff(f215,plain,(
% 1.02/0.39 ~tp(sK4) | sK3 = sK11),
% 1.02/0.39 inference(definition_unfolding,[],[f155,f196])).
% 1.02/0.39 tff(f216,plain,(
% 1.02/0.39 ~tp(sK4) | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(definition_unfolding,[],[f154,f196])).
% 1.02/0.39 tff(f217,plain,(
% 1.02/0.39 ~tp(sK4) | sK11 = sK12),
% 1.02/0.39 inference(definition_unfolding,[],[f153,f196])).
% 1.02/0.39 tff(f241,plain,(
% 1.02/0.39 ( ! [X2 : general,X0 : general,X1 : general,X18 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X12 : general,X13 : general,X20 : $int] : (f__integer__(X20) != X1 | f__integer__(X19) != X1 | f__integer__($product(X19,X20)) != X18 | X2 != X18 | X12 != X13 | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | X1 != X12 | X0 != X2 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f77])).
% 1.02/0.39 tff(f242,plain,(
% 1.02/0.39 ( ! [X2 : general,X0 : general,X18 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X12 : general,X13 : general,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | f__integer__($product(X19,X20)) != X18 | X2 != X18 | X12 != X13 | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | f__integer__(X20) != X12 | X0 != X2 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f241])).
% 1.02/0.39 tff(f243,plain,(
% 1.02/0.39 ( ! [X2 : general,X0 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X12 : general,X13 : general,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | f__integer__($product(X19,X20)) != X2 | X12 != X13 | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | f__integer__(X20) != X12 | X0 != X2 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f242])).
% 1.02/0.39 tff(f244,plain,(
% 1.02/0.39 ( ! [X0 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X12 : general,X13 : general,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | X12 != X13 | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | f__integer__(X20) != X12 | f__integer__($product(X19,X20)) != X0 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f243])).
% 1.02/0.39 tff(f245,plain,(
% 1.02/0.39 ( ! [X0 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X13 : general,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | $less(X15,X16) | $less(X16,X14) | f__integer__(X16) != X13 | 1 != X15 | 0 != X14 | f__integer__(X20) != X13 | f__integer__($product(X19,X20)) != X0 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f244])).
% 1.02/0.39 tff(f246,plain,(
% 1.02/0.39 ( ! [X0 : general,X19 : $int,X16 : $int,X14 : $int,X15 : $int,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | $less(X15,X16) | $less(X16,X14) | 1 != X15 | 0 != X14 | f__integer__(X16) != f__integer__(X20) | f__integer__($product(X19,X20)) != X0 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f245])).
% 1.02/0.39 tff(f247,plain,(
% 1.02/0.39 ( ! [X0 : general,X19 : $int,X16 : $int,X14 : $int,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | $less(1,X16) | $less(X16,X14) | 0 != X14 | f__integer__(X16) != f__integer__(X20) | f__integer__($product(X19,X20)) != X0 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f246])).
% 1.02/0.39 tff(f248,plain,(
% 1.02/0.39 ( ! [X0 : general,X19 : $int,X16 : $int,X20 : $int] : (f__integer__(X19) != f__integer__(X20) | $less(1,X16) | $less(X16,0) | f__integer__(X16) != f__integer__(X20) | f__integer__($product(X19,X20)) != X0 | tp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f247])).
% 1.02/0.39 tff(f249,plain,(
% 1.02/0.39 ( ! [X19 : $int,X16 : $int,X20 : $int] : (tp(f__integer__($product(X19,X20))) | $less(1,X16) | $less(X16,0) | f__integer__(X16) != f__integer__(X20) | f__integer__(X19) != f__integer__(X20)) )),
% 1.02/0.39 inference(equality_resolution,[],[f248])).
% 1.02/0.39 tff(f250,plain,(
% 1.02/0.39 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X1 : general,X6 : $int,X9 : general,X7 : $int,X4 : general,X5 : $int] : (f__integer__(X11) != X1 | f__integer__(X10) != X1 | f__integer__($product(X10,X11)) != X9 | X2 != X9 | X3 != X4 | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | X1 != X3 | X0 != X2 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f76])).
% 1.02/0.39 tff(f251,plain,(
% 1.02/0.39 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X6 : $int,X9 : general,X7 : $int,X4 : general,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | f__integer__($product(X10,X11)) != X9 | X2 != X9 | X3 != X4 | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | f__integer__(X11) != X3 | X0 != X2 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f250])).
% 1.02/0.39 tff(f252,plain,(
% 1.02/0.39 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X6 : $int,X7 : $int,X4 : general,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | f__integer__($product(X10,X11)) != X2 | X3 != X4 | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | f__integer__(X11) != X3 | X0 != X2 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f251])).
% 1.02/0.39 tff(f253,plain,(
% 1.02/0.39 ( ! [X3 : general,X10 : $int,X0 : general,X11 : $int,X6 : $int,X7 : $int,X4 : general,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | X3 != X4 | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | f__integer__(X11) != X3 | f__integer__($product(X10,X11)) != X0 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f252])).
% 1.02/0.39 tff(f254,plain,(
% 1.02/0.39 ( ! [X10 : $int,X0 : general,X11 : $int,X6 : $int,X7 : $int,X4 : general,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | $less(X6,X7) | $less(X7,X5) | f__integer__(X7) != X4 | 1 != X6 | 0 != X5 | f__integer__(X11) != X4 | f__integer__($product(X10,X11)) != X0 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f253])).
% 1.02/0.39 tff(f255,plain,(
% 1.02/0.39 ( ! [X10 : $int,X0 : general,X11 : $int,X6 : $int,X7 : $int,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | $less(X6,X7) | $less(X7,X5) | 1 != X6 | 0 != X5 | f__integer__(X7) != f__integer__(X11) | f__integer__($product(X10,X11)) != X0 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f254])).
% 1.02/0.39 tff(f256,plain,(
% 1.02/0.39 ( ! [X10 : $int,X0 : general,X11 : $int,X7 : $int,X5 : $int] : (f__integer__(X10) != f__integer__(X11) | $less(1,X7) | $less(X7,X5) | 0 != X5 | f__integer__(X7) != f__integer__(X11) | f__integer__($product(X10,X11)) != X0 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f255])).
% 1.02/0.39 tff(f257,plain,(
% 1.02/0.39 ( ! [X10 : $int,X0 : general,X11 : $int,X7 : $int] : (f__integer__(X10) != f__integer__(X11) | $less(1,X7) | $less(X7,0) | f__integer__(X7) != f__integer__(X11) | f__integer__($product(X10,X11)) != X0 | hp(X0)) )),
% 1.02/0.39 inference(equality_resolution,[],[f256])).
% 1.02/0.39 tff(f258,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X7 : $int] : (f__integer__(X10) != f__integer__(X11) | $less(1,X7) | $less(X7,0) | f__integer__(X7) != f__integer__(X11) | hp(f__integer__($product(X10,X11)))) )),
% 1.02/0.39 inference(equality_resolution,[],[f257])).
% 1.02/0.39 tff(f271,plain,(
% 1.02/0.39 ( ! [X0 : general] : (tp(X0) | hp(X0)) )),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f75])).
% 1.02/0.39 tff(f272,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X7 : $int] : (~hp(f__integer__($product(X10,X11))) | $less(1,X7) | $less(X7,0) | f__integer__(X7) != f__integer__(X11) | f__integer__(X10) != f__integer__(X11)) )),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f258])).
% 1.02/0.39 tff(f274,plain,(
% 1.02/0.39 ~tp(sK4) | hp(sK4)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f199])).
% 1.02/0.39 tff(f279,plain,(
% 1.02/0.39 sK7 = sK8 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f184])).
% 1.02/0.39 tff(f280,plain,(
% 1.02/0.39 sK3 = sK7 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f181])).
% 1.02/0.39 tff(f281,plain,(
% 1.02/0.39 sK5 = sK6 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f178])).
% 1.02/0.39 tff(f282,plain,(
% 1.02/0.39 sK4 = sK5 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f175])).
% 1.02/0.39 tff(f283,plain,(
% 1.02/0.39 ~tp(sK4) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f210])).
% 1.02/0.39 tff(f285,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f137])).
% 1.02/0.39 tff(f286,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f136])).
% 1.02/0.39 tff(f287,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f135])).
% 1.02/0.39 tff(f291,plain,(
% 1.02/0.39 $uminus(1) = sK15 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f105])).
% 1.02/0.39 tff(f292,plain,(
% 1.02/0.39 1 = sK16 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f104])).
% 1.02/0.39 tff(f293,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f103])).
% 1.02/0.39 tff(f294,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f102])).
% 1.02/0.39 tff(f295,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f101])).
% 1.02/0.39 tff(f301,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (sP23(X11,X10,X9,X1) | f__integer__($product(X10,X11)) = X9) )),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f85])).
% 1.02/0.39 tff(f302,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (sP23(X11,X10,X9,X1) | f__integer__(X10) = X1) )),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f84])).
% 1.02/0.39 tff(f303,plain,(
% 1.02/0.39 ( ! [X10 : $int,X11 : $int,X1 : general,X9 : general] : (sP23(X11,X10,X9,X1) | f__integer__(X11) = X1) )),
% 1.02/0.39 inference(consistent_polarity_flipping,[],[f83])).
% 1.02/0.39 tff(f304,plain,(
% 1.02/0.39 ( ! [X6 : $int,X7 : $int,X4 : general,X5 : $int] : (~sP24(X7,X6,X5,X4) | -1 = X5) )),
% 1.02/0.39 inference(evaluation,[],[f82])).
% 1.02/0.39 tff(f306,plain,(
% 1.02/0.39 sK15 = -1 | sK4 = sK9),
% 1.02/0.39 inference(evaluation,[],[f100])).
% 1.02/0.39 tff(f307,plain,(
% 1.02/0.39 sK15 = -1 | ~sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 inference(evaluation,[],[f291])).
% 1.02/0.39 tff(f308,plain,(
% 1.02/0.39 sK15 = -1 | sK9 = sK10),
% 1.02/0.39 inference(evaluation,[],[f110])).
% 1.02/0.39 tff(f309,plain,(
% 1.02/0.39 sK15 = -1 | sK3 = sK11),
% 1.02/0.39 inference(evaluation,[],[f115])).
% 1.02/0.39 tff(f310,plain,(
% 1.02/0.39 sK15 = -1 | sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 inference(evaluation,[],[f120])).
% 1.02/0.39 tff(f311,plain,(
% 1.02/0.39 sK15 = -1 | sK11 = sK12),
% 1.02/0.39 inference(evaluation,[],[f125])).
% 1.02/0.39 tff(f313,definition,(
% 1.02/0.39 spl25_1 <=> hp(sK4)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition])).
% 1.02/0.39 tff(f315,plain,(
% 1.02/0.39 hp(sK4) | ~spl25_1),
% 1.02/0.39 inference(avatar_component_clause,[],[f313])).
% 1.02/0.39 tff(f317,definition,(
% 1.02/0.39 spl25_2 <=> $less(sK16,sK17)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition])).
% 1.02/0.39 tff(f319,plain,(
% 1.02/0.39 ~$less(sK16,sK17) | spl25_2),
% 1.02/0.39 inference(avatar_component_clause,[],[f317])).
% 1.02/0.39 tff(f322,definition,(
% 1.02/0.39 spl25_3 <=> $less(sK17,sK15)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition])).
% 1.02/0.39 tff(f324,plain,(
% 1.02/0.39 ~$less(sK17,sK15) | spl25_3),
% 1.02/0.39 inference(avatar_component_clause,[],[f322])).
% 1.02/0.39 tff(f327,definition,(
% 1.02/0.39 spl25_4 <=> sK8 = f__integer__(sK17)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition])).
% 1.02/0.39 tff(f329,plain,(
% 1.02/0.39 sK8 = f__integer__(sK17) | ~spl25_4),
% 1.02/0.39 inference(avatar_component_clause,[],[f327])).
% 1.02/0.39 tff(f332,definition,(
% 1.02/0.39 spl25_5 <=> 1 = sK16),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition])).
% 1.02/0.39 tff(f334,plain,(
% 1.02/0.39 1 = sK16 | ~spl25_5),
% 1.02/0.39 inference(avatar_component_clause,[],[f332])).
% 1.02/0.39 tff(f337,definition,(
% 1.02/0.39 spl25_6 <=> sK15 = -1),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition])).
% 1.02/0.39 tff(f339,plain,(
% 1.02/0.39 sK15 = -1 | ~spl25_6),
% 1.02/0.39 inference(avatar_component_clause,[],[f337])).
% 1.02/0.39 tff(f342,definition,(
% 1.02/0.39 spl25_7 <=> sK4 = sK9),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition])).
% 1.02/0.39 tff(f344,plain,(
% 1.02/0.39 sK4 = sK9 | ~spl25_7),
% 1.02/0.39 inference(avatar_component_clause,[],[f342])).
% 1.02/0.39 tff(f345,plain,(
% 1.02/0.39 spl25_7 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f96,f317,f342])).
% 1.02/0.39 tff(f346,plain,(
% 1.02/0.39 spl25_7 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f97,f322,f342])).
% 1.02/0.39 tff(f347,plain,(
% 1.02/0.39 spl25_7 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f98,f327,f342])).
% 1.02/0.39 tff(f348,plain,(
% 1.02/0.39 spl25_7 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f99,f332,f342])).
% 1.02/0.39 tff(f349,plain,(
% 1.02/0.39 spl25_7 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f306,f337,f342])).
% 1.02/0.39 tff(f351,definition,(
% 1.02/0.39 spl25_8 <=> sP23(sK19,sK18,sK10,sK3)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition])).
% 1.02/0.39 tff(f353,plain,(
% 1.02/0.39 ~sP23(sK19,sK18,sK10,sK3) | spl25_8),
% 1.02/0.39 inference(avatar_component_clause,[],[f351])).
% 1.02/0.39 tff(f354,plain,(
% 1.02/0.39 ~spl25_8 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f295,f317,f351])).
% 1.02/0.39 tff(f355,plain,(
% 1.02/0.39 ~spl25_8 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f294,f322,f351])).
% 1.02/0.39 tff(f356,plain,(
% 1.02/0.39 ~spl25_8 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f293,f327,f351])).
% 1.02/0.39 tff(f357,plain,(
% 1.02/0.39 ~spl25_8 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f292,f332,f351])).
% 1.02/0.39 tff(f358,plain,(
% 1.02/0.39 ~spl25_8 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f307,f337,f351])).
% 1.02/0.39 tff(f360,definition,(
% 1.02/0.39 spl25_9 <=> sK9 = sK10),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition])).
% 1.02/0.39 tff(f362,plain,(
% 1.02/0.39 sK9 = sK10 | ~spl25_9),
% 1.02/0.39 inference(avatar_component_clause,[],[f360])).
% 1.02/0.39 tff(f363,plain,(
% 1.02/0.39 spl25_9 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f106,f317,f360])).
% 1.02/0.39 tff(f364,plain,(
% 1.02/0.39 spl25_9 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f107,f322,f360])).
% 1.02/0.39 tff(f365,plain,(
% 1.02/0.39 spl25_9 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f108,f327,f360])).
% 1.02/0.39 tff(f366,plain,(
% 1.02/0.39 spl25_9 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f109,f332,f360])).
% 1.02/0.39 tff(f367,plain,(
% 1.02/0.39 spl25_9 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f308,f337,f360])).
% 1.02/0.39 tff(f369,definition,(
% 1.02/0.39 spl25_10 <=> sK3 = sK11),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition])).
% 1.02/0.39 tff(f371,plain,(
% 1.02/0.39 sK3 = sK11 | ~spl25_10),
% 1.02/0.39 inference(avatar_component_clause,[],[f369])).
% 1.02/0.39 tff(f372,plain,(
% 1.02/0.39 spl25_10 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f111,f317,f369])).
% 1.02/0.39 tff(f373,plain,(
% 1.02/0.39 spl25_10 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f112,f322,f369])).
% 1.02/0.39 tff(f374,plain,(
% 1.02/0.39 spl25_10 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f113,f327,f369])).
% 1.02/0.39 tff(f375,plain,(
% 1.02/0.39 spl25_10 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f114,f332,f369])).
% 1.02/0.39 tff(f376,plain,(
% 1.02/0.39 spl25_10 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f309,f337,f369])).
% 1.02/0.39 tff(f378,definition,(
% 1.02/0.39 spl25_11 <=> sP24(sK22,sK21,sK20,sK12)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition])).
% 1.02/0.39 tff(f380,plain,(
% 1.02/0.39 sP24(sK22,sK21,sK20,sK12) | ~spl25_11),
% 1.02/0.39 inference(avatar_component_clause,[],[f378])).
% 1.02/0.39 tff(f381,plain,(
% 1.02/0.39 spl25_11 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f116,f317,f378])).
% 1.02/0.39 tff(f382,plain,(
% 1.02/0.39 spl25_11 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f117,f322,f378])).
% 1.02/0.39 tff(f383,plain,(
% 1.02/0.39 spl25_11 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f118,f327,f378])).
% 1.02/0.39 tff(f384,plain,(
% 1.02/0.39 spl25_11 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f119,f332,f378])).
% 1.02/0.39 tff(f385,plain,(
% 1.02/0.39 spl25_11 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f310,f337,f378])).
% 1.02/0.39 tff(f387,definition,(
% 1.02/0.39 spl25_12 <=> sK11 = sK12),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition])).
% 1.02/0.39 tff(f389,plain,(
% 1.02/0.39 sK11 = sK12 | ~spl25_12),
% 1.02/0.39 inference(avatar_component_clause,[],[f387])).
% 1.02/0.39 tff(f390,plain,(
% 1.02/0.39 spl25_12 | ~spl25_2),
% 1.02/0.39 inference(avatar_split_clause,[],[f121,f317,f387])).
% 1.02/0.39 tff(f391,plain,(
% 1.02/0.39 spl25_12 | ~spl25_3),
% 1.02/0.39 inference(avatar_split_clause,[],[f122,f322,f387])).
% 1.02/0.39 tff(f392,plain,(
% 1.02/0.39 spl25_12 | spl25_4),
% 1.02/0.39 inference(avatar_split_clause,[],[f123,f327,f387])).
% 1.02/0.39 tff(f393,plain,(
% 1.02/0.39 spl25_12 | spl25_5),
% 1.02/0.39 inference(avatar_split_clause,[],[f124,f332,f387])).
% 1.02/0.39 tff(f394,plain,(
% 1.02/0.39 spl25_12 | spl25_6),
% 1.02/0.39 inference(avatar_split_clause,[],[f311,f337,f387])).
% 1.02/0.39 tff(f396,definition,(
% 1.02/0.39 spl25_13 <=> sK3 = f__integer__(sK14)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition])).
% 1.02/0.39 tff(f398,plain,(
% 1.02/0.39 sK3 = f__integer__(sK14) | ~spl25_13),
% 1.02/0.39 inference(avatar_component_clause,[],[f396])).
% 1.02/0.39 tff(f401,definition,(
% 1.02/0.39 spl25_14 <=> sK3 = f__integer__(sK13)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_14])],[avatar_definition])).
% 1.02/0.39 tff(f403,plain,(
% 1.02/0.39 sK3 = f__integer__(sK13) | ~spl25_14),
% 1.02/0.39 inference(avatar_component_clause,[],[f401])).
% 1.02/0.39 tff(f406,definition,(
% 1.02/0.39 spl25_15 <=> sK6 = f__integer__($product(sK13,sK14))),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition])).
% 1.02/0.39 tff(f408,plain,(
% 1.02/0.39 sK6 = f__integer__($product(sK13,sK14)) | ~spl25_15),
% 1.02/0.39 inference(avatar_component_clause,[],[f406])).
% 1.02/0.39 tff(f410,plain,(
% 1.02/0.39 spl25_7 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f132,f396,f342])).
% 1.02/0.39 tff(f411,plain,(
% 1.02/0.39 spl25_7 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f133,f401,f342])).
% 1.02/0.39 tff(f412,plain,(
% 1.02/0.39 spl25_7 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f134,f406,f342])).
% 1.02/0.39 tff(f413,plain,(
% 1.02/0.39 ~spl25_8 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f287,f396,f351])).
% 1.02/0.39 tff(f414,plain,(
% 1.02/0.39 ~spl25_8 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f286,f401,f351])).
% 1.02/0.39 tff(f415,plain,(
% 1.02/0.39 ~spl25_8 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f285,f406,f351])).
% 1.02/0.39 tff(f416,plain,(
% 1.02/0.39 spl25_9 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f138,f396,f360])).
% 1.02/0.39 tff(f417,plain,(
% 1.02/0.39 spl25_9 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f139,f401,f360])).
% 1.02/0.39 tff(f418,plain,(
% 1.02/0.39 spl25_9 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f140,f406,f360])).
% 1.02/0.39 tff(f419,plain,(
% 1.02/0.39 spl25_10 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f141,f396,f369])).
% 1.02/0.39 tff(f420,plain,(
% 1.02/0.39 spl25_10 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f142,f401,f369])).
% 1.02/0.39 tff(f421,plain,(
% 1.02/0.39 spl25_10 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f143,f406,f369])).
% 1.02/0.39 tff(f422,plain,(
% 1.02/0.39 spl25_11 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f144,f396,f378])).
% 1.02/0.39 tff(f423,plain,(
% 1.02/0.39 spl25_11 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f145,f401,f378])).
% 1.02/0.39 tff(f424,plain,(
% 1.02/0.39 spl25_11 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f146,f406,f378])).
% 1.02/0.39 tff(f425,plain,(
% 1.02/0.39 spl25_12 | spl25_13),
% 1.02/0.39 inference(avatar_split_clause,[],[f147,f396,f387])).
% 1.02/0.39 tff(f426,plain,(
% 1.02/0.39 spl25_12 | spl25_14),
% 1.02/0.39 inference(avatar_split_clause,[],[f148,f401,f387])).
% 1.02/0.39 tff(f427,plain,(
% 1.02/0.39 spl25_12 | spl25_15),
% 1.02/0.39 inference(avatar_split_clause,[],[f149,f406,f387])).
% 1.02/0.39 tff(f429,definition,(
% 1.02/0.39 spl25_16 <=> tp(sK4)),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_16])],[avatar_definition])).
% 1.02/0.39 tff(f431,plain,(
% 1.02/0.39 ~tp(sK4) | spl25_16),
% 1.02/0.39 inference(avatar_component_clause,[],[f429])).
% 1.02/0.39 tff(f432,plain,(
% 1.02/0.39 spl25_12 | ~spl25_16),
% 1.02/0.39 inference(avatar_split_clause,[],[f217,f429,f387])).
% 1.02/0.39 tff(f433,plain,(
% 1.02/0.39 spl25_11 | ~spl25_16),
% 1.02/0.39 inference(avatar_split_clause,[],[f216,f429,f378])).
% 1.02/0.39 tff(f434,plain,(
% 1.02/0.39 spl25_10 | ~spl25_16),
% 1.02/0.39 inference(avatar_split_clause,[],[f215,f429,f369])).
% 1.02/0.39 tff(f436,definition,(
% 1.02/0.39 spl25_17 <=> sK4 = sK5),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_17])],[avatar_definition])).
% 1.02/0.39 tff(f438,plain,(
% 1.02/0.39 sK4 = sK5 | ~spl25_17),
% 1.02/0.39 inference(avatar_component_clause,[],[f436])).
% 1.02/0.39 tff(f439,plain,(
% 1.02/0.39 spl25_12 | spl25_17),
% 1.02/0.39 inference(avatar_split_clause,[],[f156,f436,f387])).
% 1.02/0.39 tff(f440,plain,(
% 1.02/0.39 spl25_11 | spl25_17),
% 1.02/0.39 inference(avatar_split_clause,[],[f157,f436,f378])).
% 1.02/0.39 tff(f441,plain,(
% 1.02/0.39 spl25_10 | spl25_17),
% 1.02/0.39 inference(avatar_split_clause,[],[f158,f436,f369])).
% 1.02/0.39 tff(f443,definition,(
% 1.02/0.39 spl25_18 <=> sK5 = sK6),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition])).
% 1.02/0.39 tff(f445,plain,(
% 1.02/0.39 sK5 = sK6 | ~spl25_18),
% 1.02/0.39 inference(avatar_component_clause,[],[f443])).
% 1.02/0.39 tff(f446,plain,(
% 1.02/0.39 spl25_12 | spl25_18),
% 1.02/0.39 inference(avatar_split_clause,[],[f159,f443,f387])).
% 1.02/0.39 tff(f447,plain,(
% 1.02/0.39 spl25_11 | spl25_18),
% 1.02/0.39 inference(avatar_split_clause,[],[f160,f443,f378])).
% 1.02/0.39 tff(f448,plain,(
% 1.02/0.39 spl25_10 | spl25_18),
% 1.02/0.39 inference(avatar_split_clause,[],[f161,f443,f369])).
% 1.02/0.39 tff(f450,definition,(
% 1.02/0.39 spl25_19 <=> sK3 = sK7),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition])).
% 1.02/0.39 tff(f452,plain,(
% 1.02/0.39 sK3 = sK7 | ~spl25_19),
% 1.02/0.39 inference(avatar_component_clause,[],[f450])).
% 1.02/0.39 tff(f453,plain,(
% 1.02/0.39 spl25_12 | spl25_19),
% 1.02/0.39 inference(avatar_split_clause,[],[f162,f450,f387])).
% 1.02/0.39 tff(f454,plain,(
% 1.02/0.39 spl25_11 | spl25_19),
% 1.02/0.39 inference(avatar_split_clause,[],[f163,f450,f378])).
% 1.02/0.39 tff(f455,plain,(
% 1.02/0.39 spl25_10 | spl25_19),
% 1.02/0.39 inference(avatar_split_clause,[],[f164,f450,f369])).
% 1.02/0.39 tff(f457,definition,(
% 1.02/0.39 spl25_20 <=> sK7 = sK8),
% 1.02/0.39 introduced(definition,[new_symbols(definition,[spl25_20])],[avatar_definition])).
% 1.02/0.39 tff(f459,plain,(
% 1.02/0.39 sK7 = sK8 | ~spl25_20),
% 1.02/0.39 inference(avatar_component_clause,[],[f457])).
% 1.02/0.39 tff(f460,plain,(
% 1.02/0.39 spl25_12 | spl25_20),
% 1.02/0.39 inference(avatar_split_clause,[],[f165,f457,f387])).
% 1.02/0.40 tff(f461,plain,(
% 1.02/0.40 spl25_11 | spl25_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f166,f457,f378])).
% 1.02/0.40 tff(f462,plain,(
% 1.02/0.40 spl25_10 | spl25_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f167,f457,f369])).
% 1.02/0.40 tff(f463,plain,(
% 1.02/0.40 spl25_9 | ~spl25_16),
% 1.02/0.40 inference(avatar_split_clause,[],[f211,f429,f360])).
% 1.02/0.40 tff(f464,plain,(
% 1.02/0.40 ~spl25_8 | ~spl25_16),
% 1.02/0.40 inference(avatar_split_clause,[],[f283,f429,f351])).
% 1.02/0.40 tff(f465,plain,(
% 1.02/0.40 spl25_7 | ~spl25_16),
% 1.02/0.40 inference(avatar_split_clause,[],[f209,f429,f342])).
% 1.02/0.40 tff(f466,plain,(
% 1.02/0.40 spl25_9 | spl25_17),
% 1.02/0.40 inference(avatar_split_clause,[],[f174,f436,f360])).
% 1.02/0.40 tff(f467,plain,(
% 1.02/0.40 ~spl25_8 | spl25_17),
% 1.02/0.40 inference(avatar_split_clause,[],[f282,f436,f351])).
% 1.02/0.40 tff(f468,plain,(
% 1.02/0.40 spl25_7 | spl25_17),
% 1.02/0.40 inference(avatar_split_clause,[],[f176,f436,f342])).
% 1.02/0.40 tff(f469,plain,(
% 1.02/0.40 spl25_9 | spl25_18),
% 1.02/0.40 inference(avatar_split_clause,[],[f177,f443,f360])).
% 1.02/0.40 tff(f470,plain,(
% 1.02/0.40 ~spl25_8 | spl25_18),
% 1.02/0.40 inference(avatar_split_clause,[],[f281,f443,f351])).
% 1.02/0.40 tff(f471,plain,(
% 1.02/0.40 spl25_7 | spl25_18),
% 1.02/0.40 inference(avatar_split_clause,[],[f179,f443,f342])).
% 1.02/0.40 tff(f472,plain,(
% 1.02/0.40 spl25_9 | spl25_19),
% 1.02/0.40 inference(avatar_split_clause,[],[f180,f450,f360])).
% 1.02/0.40 tff(f473,plain,(
% 1.02/0.40 ~spl25_8 | spl25_19),
% 1.02/0.40 inference(avatar_split_clause,[],[f280,f450,f351])).
% 1.02/0.40 tff(f474,plain,(
% 1.02/0.40 spl25_7 | spl25_19),
% 1.02/0.40 inference(avatar_split_clause,[],[f182,f450,f342])).
% 1.02/0.40 tff(f475,plain,(
% 1.02/0.40 spl25_9 | spl25_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f183,f457,f360])).
% 1.02/0.40 tff(f476,plain,(
% 1.02/0.40 ~spl25_8 | spl25_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f279,f457,f351])).
% 1.02/0.40 tff(f477,plain,(
% 1.02/0.40 spl25_7 | spl25_20),
% 1.02/0.40 inference(avatar_split_clause,[],[f185,f457,f342])).
% 1.02/0.40 tff(f482,plain,(
% 1.02/0.40 spl25_1 | ~spl25_16),
% 1.02/0.40 inference(avatar_split_clause,[],[f274,f429,f313])).
% 1.02/0.40 tff(f484,plain,(
% 1.02/0.40 ~$less(sK17,-1) | (spl25_3 | ~spl25_6)),
% 1.02/0.40 inference(superposition,[],[f324,f339])).
% 1.02/0.40 tff(f485,plain,(
% 1.02/0.40 sK4 = sK6 | (~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_demodulation,[],[f445,f438])).
% 1.02/0.40 tff(f486,plain,(
% 1.02/0.40 sK3 = sK8 | (~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(forward_demodulation,[],[f459,f452])).
% 1.02/0.40 tff(f487,plain,(
% 1.02/0.40 sK3 = f__integer__(sK17) | (~spl25_4 | ~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(forward_demodulation,[],[f329,f486])).
% 1.02/0.40 tff(f488,plain,(
% 1.02/0.40 sK4 = f__integer__($product(sK13,sK14)) | (~spl25_15 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_demodulation,[],[f408,f485])).
% 1.02/0.40 tff(f489,plain,(
% 1.02/0.40 sK3 = f__integer__(sK18) | spl25_8),
% 1.02/0.40 inference(resolution,[],[f302,f353])).
% 1.02/0.40 tff(f490,plain,(
% 1.02/0.40 sK3 = f__integer__(sK19) | spl25_8),
% 1.02/0.40 inference(resolution,[],[f303,f353])).
% 1.02/0.40 tff(f491,plain,(
% 1.02/0.40 sK10 = f__integer__($product(sK18,sK19)) | spl25_8),
% 1.02/0.40 inference(resolution,[],[f301,f353])).
% 1.02/0.40 tff(f499,plain,(
% 1.02/0.40 hp(sK4) | spl25_16),
% 1.02/0.40 inference(resolution,[],[f271,f431])).
% 1.02/0.40 tff(f500,plain,(
% 1.02/0.40 spl25_1 | spl25_16),
% 1.02/0.40 inference(avatar_split_clause,[],[f499,f429,f313])).
% 1.02/0.40 tff(f527,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | sK13 = X0) ) | ~spl25_14),
% 1.02/0.40 inference(superposition,[],[f62,f403])).
% 1.02/0.40 tff(f528,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | sK14 = X0) ) | ~spl25_13),
% 1.02/0.40 inference(superposition,[],[f62,f398])).
% 1.02/0.40 tff(f530,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | sK18 = X0) ) | spl25_8),
% 1.02/0.40 inference(superposition,[],[f62,f489])).
% 1.02/0.40 tff(f569,definition,(
% 1.02/0.40 spl25_21 <=> sK17 = -1),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition])).
% 1.02/0.40 tff(f571,plain,(
% 1.02/0.40 sK17 = -1 | ~spl25_21),
% 1.02/0.40 inference(avatar_component_clause,[],[f569])).
% 1.02/0.40 tff(f573,definition,(
% 1.02/0.40 spl25_22 <=> $less(-1,sK17)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition])).
% 1.02/0.40 tff(f575,plain,(
% 1.02/0.40 $less(-1,sK17) | ~spl25_22),
% 1.02/0.40 inference(avatar_component_clause,[],[f573])).
% 1.02/0.40 tff(f593,plain,(
% 1.02/0.40 sK4 = sK10 | (~spl25_7 | ~spl25_9)),
% 1.02/0.40 inference(forward_demodulation,[],[f362,f344])).
% 1.02/0.40 tff(f594,plain,(
% 1.02/0.40 sK3 = sK12 | (~spl25_10 | ~spl25_12)),
% 1.02/0.40 inference(forward_demodulation,[],[f389,f371])).
% 1.02/0.40 tff(f602,plain,(
% 1.02/0.40 ~sP23(sK19,sK18,sK4,sK3) | (~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(superposition,[],[f353,f593])).
% 1.02/0.40 tff(f615,plain,(
% 1.02/0.40 sP24(sK22,sK21,sK20,sK3) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(forward_demodulation,[],[f380,f594])).
% 1.02/0.40 tff(f626,plain,(
% 1.02/0.40 sK3 = f__integer__(sK22) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f615,f80])).
% 1.02/0.40 tff(f627,plain,(
% 1.02/0.40 sK20 = -1 | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f615,f304])).
% 1.02/0.40 tff(f628,plain,(
% 1.02/0.40 1 = sK21 | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f615,f81])).
% 1.02/0.40 tff(f629,plain,(
% 1.02/0.40 ~$less(sK22,sK20) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f615,f79])).
% 1.02/0.40 tff(f630,plain,(
% 1.02/0.40 ~$less(sK21,sK22) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f615,f78])).
% 1.02/0.40 tff(f678,plain,(
% 1.02/0.40 ~$less(sK22,-1) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(forward_demodulation,[],[f629,f627])).
% 1.02/0.40 tff(f679,plain,(
% 1.02/0.40 ~$less(1,sK22) | (~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(forward_demodulation,[],[f630,f628])).
% 1.02/0.40 tff(f730,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (tp(sK4) | $less(1,X0) | $less(X0,0) | f__integer__(X0) != f__integer__(sK14) | f__integer__(sK14) != f__integer__(sK13)) ) | (~spl25_15 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(superposition,[],[f249,f488])).
% 1.02/0.40 tff(f733,plain,(
% 1.02/0.40 ( ! [X0 : $int] : ($less(1,X0) | $less(X0,0) | f__integer__(X0) != f__integer__(sK14) | f__integer__(sK14) != f__integer__(sK13)) ) | (~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f730,f431])).
% 1.02/0.40 tff(f746,definition,(
% 1.02/0.40 spl25_30 <=> ! [X1 : $int] : ($less(1,X1) | f__integer__(X1) != f__integer__(1) | $less(X1,0))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_30])],[avatar_definition])).
% 1.02/0.40 tff(f747,plain,(
% 1.02/0.40 ( ! [X1 : $int] : (f__integer__(X1) != f__integer__(1) | $less(1,X1) | $less(X1,0)) ) | ~spl25_30),
% 1.02/0.40 inference(avatar_component_clause,[],[f746])).
% 1.02/0.40 tff(f753,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0) | f__integer__(sK14) != f__integer__(sK13)) ) | (~spl25_13 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_demodulation,[],[f733,f398])).
% 1.02/0.40 tff(f755,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (sK3 != f__integer__(sK14) | f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0)) ) | (~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_demodulation,[],[f753,f403])).
% 1.02/0.40 tff(f757,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0)) ) | (~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f755,f398])).
% 1.02/0.40 tff(f759,plain,(
% 1.02/0.40 ( ! [X0 : $int,X1 : $int] : (~hp(f__integer__(X0)) | $less(1,X1) | $less(X1,0) | f__integer__(X1) != f__integer__(1) | f__integer__(X0) != f__integer__(1)) )),
% 1.02/0.40 inference(superposition,[],[f272,f36])).
% 1.02/0.40 tff(f774,definition,(
% 1.02/0.40 spl25_33 <=> ! [X0 : $int] : (~hp(f__integer__(X0)) | f__integer__(X0) != f__integer__(1))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_33])],[avatar_definition])).
% 1.02/0.40 tff(f775,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (~hp(f__integer__(X0)) | f__integer__(X0) != f__integer__(1)) ) | ~spl25_33),
% 1.02/0.40 inference(avatar_component_clause,[],[f774])).
% 1.02/0.40 tff(f776,plain,(
% 1.02/0.40 spl25_30 | spl25_33),
% 1.02/0.40 inference(avatar_split_clause,[],[f759,f774,f746])).
% 1.02/0.40 tff(f791,definition,(
% 1.02/0.40 spl25_35 <=> $less(-1,sK22)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_35])],[avatar_definition])).
% 1.02/0.40 tff(f792,plain,(
% 1.02/0.40 ~$less(-1,sK22) | spl25_35),
% 1.02/0.40 inference(avatar_component_clause,[],[f791])).
% 1.02/0.40 tff(f793,plain,(
% 1.02/0.40 $less(-1,sK22) | ~spl25_35),
% 1.02/0.40 inference(avatar_component_clause,[],[f791])).
% 1.02/0.40 tff(f805,plain,(
% 1.02/0.40 sK4 = f__integer__($product(sK18,sK19)) | (~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(resolution,[],[f602,f301])).
% 1.02/0.40 tff(f825,plain,(
% 1.02/0.40 sK3 != sK3 | sK13 = sK17 | (~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(superposition,[],[f527,f487])).
% 1.02/0.40 tff(f832,plain,(
% 1.02/0.40 sK13 = sK17 | (~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f825])).
% 1.02/0.40 tff(f869,plain,(
% 1.02/0.40 sK3 != sK3 | sK14 = sK17 | (~spl25_4 | ~spl25_13 | ~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(superposition,[],[f528,f487])).
% 1.02/0.40 tff(f876,plain,(
% 1.02/0.40 sK14 = sK17 | (~spl25_4 | ~spl25_13 | ~spl25_19 | ~spl25_20)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f869])).
% 1.02/0.40 tff(f1140,plain,(
% 1.02/0.40 sK3 != sK3 | $less(1,sK13) | $less(sK13,0) | (~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(superposition,[],[f757,f403])).
% 1.02/0.40 tff(f1149,plain,(
% 1.02/0.40 $less(1,sK13) | $less(sK13,0) | (~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f1140])).
% 1.02/0.40 tff(f1256,plain,(
% 1.02/0.40 ~hp(sK4) | sK4 != f__integer__(1) | (~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_33)),
% 1.02/0.40 inference(superposition,[],[f775,f488])).
% 1.02/0.40 tff(f1257,plain,(
% 1.02/0.40 ~hp(sK10) | sK10 != f__integer__(1) | (spl25_8 | ~spl25_33)),
% 1.02/0.40 inference(superposition,[],[f775,f491])).
% 1.02/0.40 tff(f1272,plain,(
% 1.02/0.40 ~hp(sK4) | sK10 != f__integer__(1) | (~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_33)),
% 1.02/0.40 inference(forward_demodulation,[],[f1257,f593])).
% 1.02/0.40 tff(f1273,plain,(
% 1.02/0.40 sK4 != f__integer__(1) | (~spl25_1 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_33)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f1256,f315])).
% 1.02/0.40 tff(f1274,plain,(
% 1.02/0.40 sK10 != f__integer__(1) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_33)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f1272,f315])).
% 1.02/0.40 tff(f1275,plain,(
% 1.02/0.40 sK4 != f__integer__(1) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_33)),
% 1.02/0.40 inference(forward_demodulation,[],[f1274,f593])).
% 1.02/0.40 tff(f2895,plain,(
% 1.02/0.40 $less(1,1) | $less(1,0) | ~spl25_30),
% 1.02/0.40 inference(equality_resolution,[],[f747])).
% 1.02/0.40 tff(f2896,plain,(
% 1.02/0.40 $false | ~spl25_30),
% 1.02/0.40 inference(evaluation,[],[f2895])).
% 1.02/0.40 tff(f2897,plain,(
% 1.02/0.40 ~spl25_30),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f2896])).
% 1.02/0.40 tff(f2913,definition,(
% 1.02/0.40 spl25_60 <=> sK4 = f__integer__(1)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_60])],[avatar_definition])).
% 1.02/0.40 tff(f2915,plain,(
% 1.02/0.40 sK4 != f__integer__(1) | spl25_60),
% 1.02/0.40 inference(avatar_component_clause,[],[f2913])).
% 1.02/0.40 tff(f2923,definition,(
% 1.02/0.40 spl25_61 <=> ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(X0,0) | $less(1,X0))),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_61])],[avatar_definition])).
% 1.02/0.40 tff(f2924,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(X0,0) | $less(1,X0)) ) | ~spl25_61),
% 1.02/0.40 inference(avatar_component_clause,[],[f2923])).
% 1.02/0.40 tff(f2934,plain,(
% 1.02/0.40 ~spl25_60 | ~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_33),
% 1.02/0.40 inference(avatar_split_clause,[],[f1275,f774,f360,f351,f342,f313,f2913])).
% 1.02/0.40 tff(f2942,plain,(
% 1.02/0.40 ~$less(sK22,$sum(-1,1)) | ~spl25_35),
% 1.02/0.40 inference(resolution,[],[f793,f40])).
% 1.02/0.40 tff(f3001,definition,(
% 1.02/0.40 spl25_62 <=> sK14 = -1),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_62])],[avatar_definition])).
% 1.02/0.40 tff(f3002,plain,(
% 1.02/0.40 sK14 != -1 | spl25_62),
% 1.02/0.40 inference(avatar_component_clause,[],[f3001])).
% 1.02/0.40 tff(f3003,plain,(
% 1.02/0.40 sK14 = -1 | ~spl25_62),
% 1.02/0.40 inference(avatar_component_clause,[],[f3001])).
% 1.02/0.40 tff(f3099,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (~hp(sK4) | $less(1,X0) | $less(X0,0) | f__integer__(X0) != f__integer__(sK19) | f__integer__(sK18) != f__integer__(sK19)) ) | (~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(superposition,[],[f272,f805])).
% 1.02/0.40 tff(f3114,plain,(
% 1.02/0.40 ( ! [X0 : $int] : ($less(1,X0) | $less(X0,0) | f__integer__(X0) != f__integer__(sK19) | f__integer__(sK18) != f__integer__(sK19)) ) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f3099,f315])).
% 1.02/0.40 tff(f3116,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0) | f__integer__(sK18) != f__integer__(sK19)) ) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(forward_demodulation,[],[f3114,f490])).
% 1.02/0.40 tff(f3118,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (sK3 != f__integer__(sK18) | f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0)) ) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(forward_demodulation,[],[f3116,f490])).
% 1.02/0.40 tff(f3120,plain,(
% 1.02/0.40 ( ! [X0 : $int] : (f__integer__(X0) != sK3 | $less(1,X0) | $less(X0,0)) ) | (~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f3118,f489])).
% 1.02/0.40 tff(f3122,plain,(
% 1.02/0.40 spl25_61 | ~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9),
% 1.02/0.40 inference(avatar_split_clause,[],[f3120,f360,f351,f342,f313,f2923])).
% 1.02/0.40 tff(f3126,plain,(
% 1.02/0.40 sK3 != sK3 | sK18 = sK19 | spl25_8),
% 1.02/0.40 inference(superposition,[],[f530,f490])).
% 1.02/0.40 tff(f3127,plain,(
% 1.02/0.40 sK3 != sK3 | sK18 = sK22 | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(superposition,[],[f530,f626])).
% 1.02/0.40 tff(f3128,plain,(
% 1.02/0.40 sK18 = sK22 | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f3127])).
% 1.02/0.40 tff(f3129,plain,(
% 1.02/0.40 sK18 = sK19 | spl25_8),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f3126])).
% 1.02/0.40 tff(f3221,plain,(
% 1.02/0.40 ~$less(sK18,-1) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(superposition,[],[f678,f3128])).
% 1.02/0.40 tff(f3222,plain,(
% 1.02/0.40 ~$less(1,sK18) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(superposition,[],[f679,f3128])).
% 1.02/0.40 tff(f3256,plain,(
% 1.02/0.40 $less(-1,sK18) | sK18 = -1 | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12)),
% 1.02/0.40 inference(resolution,[],[f3221,f30])).
% 1.02/0.40 tff(f3259,definition,(
% 1.02/0.40 spl25_70 <=> sK18 = -1),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_70])],[avatar_definition])).
% 1.02/0.40 tff(f3261,plain,(
% 1.02/0.40 sK18 = -1 | ~spl25_70),
% 1.02/0.40 inference(avatar_component_clause,[],[f3259])).
% 1.02/0.40 tff(f3263,definition,(
% 1.02/0.40 spl25_71 <=> $less(-1,sK18)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_71])],[avatar_definition])).
% 1.02/0.40 tff(f3267,plain,(
% 1.02/0.40 spl25_70 | spl25_71 | spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12),
% 1.02/0.40 inference(avatar_split_clause,[],[f3256,f387,f378,f369,f351,f3263,f3259])).
% 1.02/0.40 tff(f3366,plain,(
% 1.02/0.40 ~$less(-1,sK18) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | spl25_35)),
% 1.02/0.40 inference(forward_demodulation,[],[f792,f3128])).
% 1.02/0.40 tff(f3368,plain,(
% 1.02/0.40 ~spl25_71 | spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | spl25_35),
% 1.02/0.40 inference(avatar_split_clause,[],[f3366,f791,f387,f378,f369,f351,f3263])).
% 1.02/0.40 tff(f3370,plain,(
% 1.02/0.40 ~$less(sK22,0) | ~spl25_35),
% 1.02/0.40 inference(evaluation,[],[f2942])).
% 1.02/0.40 tff(f3377,plain,(
% 1.02/0.40 ~$less(sK18,0) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35)),
% 1.02/0.40 inference(forward_demodulation,[],[f3370,f3128])).
% 1.02/0.40 tff(f4026,plain,(
% 1.02/0.40 sK10 = f__integer__($product(-1,sK19)) | (spl25_8 | ~spl25_70)),
% 1.02/0.40 inference(superposition,[],[f491,f3261])).
% 1.02/0.40 tff(f4032,plain,(
% 1.02/0.40 sK10 = f__integer__($uminus(sK19)) | (spl25_8 | ~spl25_70)),
% 1.02/0.40 inference(evaluation,[],[f4026])).
% 1.02/0.40 tff(f4035,plain,(
% 1.02/0.40 sK10 = f__integer__($uminus(sK18)) | (spl25_8 | ~spl25_70)),
% 1.02/0.40 inference(forward_demodulation,[],[f4032,f3129])).
% 1.02/0.40 tff(f4041,plain,(
% 1.02/0.40 sK10 = f__integer__($uminus(-1)) | (spl25_8 | ~spl25_70)),
% 1.02/0.40 inference(forward_demodulation,[],[f4035,f3261])).
% 1.02/0.40 tff(f4042,plain,(
% 1.02/0.40 sK10 = f__integer__(1) | (spl25_8 | ~spl25_70)),
% 1.02/0.40 inference(evaluation,[],[f4041])).
% 1.02/0.40 tff(f4047,plain,(
% 1.02/0.40 sK4 = f__integer__(1) | (~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_70)),
% 1.02/0.40 inference(forward_demodulation,[],[f4042,f593])).
% 1.02/0.40 tff(f4049,plain,(
% 1.02/0.40 $false | (~spl25_7 | spl25_8 | ~spl25_9 | spl25_60 | ~spl25_70)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f4047,f2915])).
% 1.02/0.40 tff(f4050,plain,(
% 1.02/0.40 ~spl25_7 | spl25_8 | ~spl25_9 | spl25_60 | ~spl25_70),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f4049])).
% 1.02/0.40 tff(f4317,plain,(
% 1.02/0.40 sK3 != sK3 | $less(sK19,0) | $less(1,sK19) | (spl25_8 | ~spl25_61)),
% 1.02/0.40 inference(superposition,[],[f2924,f490])).
% 1.02/0.40 tff(f4320,plain,(
% 1.02/0.40 $less(sK19,0) | $less(1,sK19) | (spl25_8 | ~spl25_61)),
% 1.02/0.40 inference(trivial_inequality_removal,[],[f4317])).
% 1.02/0.40 tff(f4323,plain,(
% 1.02/0.40 $less(sK18,0) | $less(1,sK19) | (spl25_8 | ~spl25_61)),
% 1.02/0.40 inference(forward_demodulation,[],[f4320,f3129])).
% 1.02/0.40 tff(f4327,plain,(
% 1.02/0.40 $less(1,sK19) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35 | ~spl25_61)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f4323,f3377])).
% 1.02/0.40 tff(f4332,plain,(
% 1.02/0.40 $less(1,sK18) | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35 | ~spl25_61)),
% 1.02/0.40 inference(forward_demodulation,[],[f4327,f3129])).
% 1.02/0.40 tff(f4333,plain,(
% 1.02/0.40 $false | (spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35 | ~spl25_61)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f4332,f3222])).
% 1.02/0.40 tff(f4334,plain,(
% 1.02/0.40 spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35 | ~spl25_61),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f4333])).
% 1.02/0.40 tff(f4395,definition,(
% 1.02/0.40 spl25_83 <=> $less(sK13,0)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_83])],[avatar_definition])).
% 1.02/0.40 tff(f4397,plain,(
% 1.02/0.40 $less(sK13,0) | ~spl25_83),
% 1.02/0.40 inference(avatar_component_clause,[],[f4395])).
% 1.02/0.40 tff(f4399,definition,(
% 1.02/0.40 spl25_84 <=> $less(1,sK13)),
% 1.02/0.40 introduced(definition,[new_symbols(definition,[spl25_84])],[avatar_definition])).
% 1.02/0.40 tff(f4401,plain,(
% 1.02/0.40 $less(1,sK13) | ~spl25_84),
% 1.02/0.40 inference(avatar_component_clause,[],[f4399])).
% 1.02/0.40 tff(f4405,plain,(
% 1.02/0.40 spl25_83 | spl25_84 | ~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18),
% 1.02/0.40 inference(avatar_split_clause,[],[f1149,f443,f436,f429,f406,f401,f396,f4399,f4395])).
% 1.02/0.40 tff(f4533,plain,(
% 1.02/0.40 ~$less(1,sK17) | (spl25_2 | ~spl25_5)),
% 1.02/0.40 inference(forward_demodulation,[],[f319,f334])).
% 1.02/0.40 tff(f4627,plain,(
% 1.02/0.40 $less(-1,sK17) | sK17 = -1 | (spl25_3 | ~spl25_6)),
% 1.02/0.40 inference(resolution,[],[f484,f30])).
% 1.02/0.40 tff(f4630,plain,(
% 1.02/0.40 spl25_21 | spl25_22 | spl25_3 | ~spl25_6),
% 1.02/0.40 inference(avatar_split_clause,[],[f4627,f337,f322,f573,f569])).
% 1.02/0.40 tff(f4790,plain,(
% 1.02/0.40 ~$less(sK17,$sum(-1,1)) | ~spl25_22),
% 1.02/0.40 inference(resolution,[],[f575,f40])).
% 1.02/0.40 tff(f4791,plain,(
% 1.02/0.40 ~$less(sK17,0) | ~spl25_22),
% 1.02/0.40 inference(evaluation,[],[f4790])).
% 1.02/0.40 tff(f4874,plain,(
% 1.02/0.40 sK17 != -1 | (~spl25_4 | ~spl25_13 | ~spl25_19 | ~spl25_20 | spl25_62)),
% 1.02/0.40 inference(superposition,[],[f3002,f876])).
% 1.02/0.40 tff(f4887,plain,(
% 1.02/0.40 $less(1,sK17) | (~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_84)),
% 1.02/0.40 inference(forward_demodulation,[],[f4401,f832])).
% 1.02/0.40 tff(f4888,plain,(
% 1.02/0.40 $false | (spl25_2 | ~spl25_4 | ~spl25_5 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_84)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f4887,f4533])).
% 1.02/0.40 tff(f4889,plain,(
% 1.02/0.40 spl25_2 | ~spl25_4 | ~spl25_5 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_84),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f4888])).
% 1.02/0.40 tff(f4890,plain,(
% 1.02/0.40 $less(sK17,0) | (~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_83)),
% 1.02/0.40 inference(forward_demodulation,[],[f4397,f832])).
% 1.02/0.40 tff(f5101,plain,(
% 1.02/0.40 $false | (~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_22 | ~spl25_83)),
% 1.02/0.40 inference(forward_subsumption_resolution,[],[f4791,f4890])).
% 1.02/0.40 tff(f5102,plain,(
% 1.02/0.40 ~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_22 | ~spl25_83),
% 1.02/0.40 inference(avatar_contradiction_clause,[],[f5101])).
% 1.02/0.40 tff(f5104,plain,(
% 1.02/0.40 ~spl25_21 | ~spl25_4 | ~spl25_13 | ~spl25_19 | ~spl25_20 | spl25_62),
% 1.02/0.40 inference(avatar_split_clause,[],[f4874,f3001,f457,f450,f396,f327,f569])).
% 1.02/0.40 tff(f5233,plain,(
% 1.02/0.40 sK4 = f__integer__($product(sK13,-1)) | (~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_62)),
% 1.02/0.40 inference(superposition,[],[f488,f3003])).
% 1.02/0.40 tff(f5235,plain,(
% 1.02/0.40 sK4 = f__integer__($uminus(sK13)) | (~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_62)),
% 1.02/0.40 inference(evaluation,[],[f5233])).
% 1.02/0.40 tff(f5236,plain,(
% 1.02/0.40 sK4 = f__integer__($uminus(sK17)) | (~spl25_4 | ~spl25_14 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_19 | ~spl25_20 | ~spl25_62)),
% 1.02/0.40 inference(forward_demodulation,[],[f5235,f832])).
% 1.02/0.40 tff(f5237,plain,(
% 1.02/0.40 sK4 = f__integer__($uminus(-1)) | (~spl25_4 | ~spl25_14 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_19 | ~spl25_20 | ~spl25_21 | ~spl25_62)),
% 1.02/0.40 inference(forward_demodulation,[],[f5236,f571])).
% 1.02/0.40 tff(f5238,plain,(
% 1.02/0.40 sK4 = f__integer__(1) | (~spl25_4 | ~spl25_14 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_19 | ~spl25_20 | ~spl25_21 | ~spl25_62)),
% 1.02/0.40 inference(evaluation,[],[f5237])).
% 1.02/0.40 tff(f5245,plain,(
% 1.02/0.40 ~spl25_60 | ~spl25_1 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_33),
% 1.02/0.40 inference(avatar_split_clause,[],[f1273,f774,f443,f436,f406,f313,f2913])).
% 1.02/0.40 tff(f5248,plain,(
% 1.02/0.40 spl25_60 | ~spl25_4 | ~spl25_14 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_19 | ~spl25_20 | ~spl25_21 | ~spl25_62),
% 1.02/0.40 inference(avatar_split_clause,[],[f5238,f3001,f569,f457,f450,f443,f436,f406,f401,f327,f2913])).
% 1.02/0.40 cnf(s6, plain, ~spl25_2 | spl25_7, inference(sat_conversion,[],[f345])).
% 1.02/0.40 cnf(s7, plain, ~spl25_3 | spl25_7, inference(sat_conversion,[],[f346])).
% 1.02/0.40 cnf(s8, plain, spl25_4 | spl25_7, inference(sat_conversion,[],[f347])).
% 1.02/0.40 cnf(s9, plain, spl25_5 | spl25_7, inference(sat_conversion,[],[f348])).
% 1.02/0.40 cnf(s10, plain, spl25_6 | spl25_7, inference(sat_conversion,[],[f349])).
% 1.02/0.40 cnf(s11, plain, ~spl25_2 | ~spl25_8, inference(sat_conversion,[],[f354])).
% 1.02/0.40 cnf(s12, plain, ~spl25_3 | ~spl25_8, inference(sat_conversion,[],[f355])).
% 1.02/0.40 cnf(s13, plain, spl25_4 | ~spl25_8, inference(sat_conversion,[],[f356])).
% 1.02/0.40 cnf(s14, plain, spl25_5 | ~spl25_8, inference(sat_conversion,[],[f357])).
% 1.02/0.40 cnf(s15, plain, spl25_6 | ~spl25_8, inference(sat_conversion,[],[f358])).
% 1.02/0.40 cnf(s16, plain, ~spl25_2 | spl25_9, inference(sat_conversion,[],[f363])).
% 1.02/0.40 cnf(s17, plain, ~spl25_3 | spl25_9, inference(sat_conversion,[],[f364])).
% 1.02/0.40 cnf(s18, plain, spl25_4 | spl25_9, inference(sat_conversion,[],[f365])).
% 1.02/0.40 cnf(s19, plain, spl25_5 | spl25_9, inference(sat_conversion,[],[f366])).
% 1.02/0.40 cnf(s20, plain, spl25_6 | spl25_9, inference(sat_conversion,[],[f367])).
% 1.02/0.40 cnf(s21, plain, ~spl25_2 | spl25_10, inference(sat_conversion,[],[f372])).
% 1.02/0.40 cnf(s22, plain, ~spl25_3 | spl25_10, inference(sat_conversion,[],[f373])).
% 1.02/0.40 cnf(s23, plain, spl25_4 | spl25_10, inference(sat_conversion,[],[f374])).
% 1.02/0.40 cnf(s24, plain, spl25_5 | spl25_10, inference(sat_conversion,[],[f375])).
% 1.02/0.40 cnf(s25, plain, spl25_6 | spl25_10, inference(sat_conversion,[],[f376])).
% 1.02/0.40 cnf(s26, plain, ~spl25_2 | spl25_11, inference(sat_conversion,[],[f381])).
% 1.02/0.40 cnf(s27, plain, ~spl25_3 | spl25_11, inference(sat_conversion,[],[f382])).
% 1.02/0.40 cnf(s28, plain, spl25_4 | spl25_11, inference(sat_conversion,[],[f383])).
% 1.02/0.40 cnf(s29, plain, spl25_5 | spl25_11, inference(sat_conversion,[],[f384])).
% 1.02/0.40 cnf(s30, plain, spl25_6 | spl25_11, inference(sat_conversion,[],[f385])).
% 1.02/0.40 cnf(s31, plain, ~spl25_2 | spl25_12, inference(sat_conversion,[],[f390])).
% 1.02/0.40 cnf(s32, plain, ~spl25_3 | spl25_12, inference(sat_conversion,[],[f391])).
% 1.02/0.40 cnf(s33, plain, spl25_4 | spl25_12, inference(sat_conversion,[],[f392])).
% 1.02/0.40 cnf(s34, plain, spl25_5 | spl25_12, inference(sat_conversion,[],[f393])).
% 1.02/0.40 cnf(s35, plain, spl25_6 | spl25_12, inference(sat_conversion,[],[f394])).
% 1.02/0.40 cnf(s39, plain, spl25_7 | spl25_13, inference(sat_conversion,[],[f410])).
% 1.02/0.40 cnf(s40, plain, spl25_7 | spl25_14, inference(sat_conversion,[],[f411])).
% 1.02/0.40 cnf(s41, plain, spl25_7 | spl25_15, inference(sat_conversion,[],[f412])).
% 1.02/0.40 cnf(s42, plain, ~spl25_8 | spl25_13, inference(sat_conversion,[],[f413])).
% 1.02/0.40 cnf(s43, plain, ~spl25_8 | spl25_14, inference(sat_conversion,[],[f414])).
% 1.02/0.40 cnf(s44, plain, ~spl25_8 | spl25_15, inference(sat_conversion,[],[f415])).
% 1.02/0.40 cnf(s45, plain, spl25_9 | spl25_13, inference(sat_conversion,[],[f416])).
% 1.02/0.40 cnf(s46, plain, spl25_9 | spl25_14, inference(sat_conversion,[],[f417])).
% 1.02/0.40 cnf(s47, plain, spl25_9 | spl25_15, inference(sat_conversion,[],[f418])).
% 1.02/0.40 cnf(s48, plain, spl25_10 | spl25_13, inference(sat_conversion,[],[f419])).
% 1.02/0.40 cnf(s49, plain, spl25_10 | spl25_14, inference(sat_conversion,[],[f420])).
% 1.02/0.40 cnf(s50, plain, spl25_10 | spl25_15, inference(sat_conversion,[],[f421])).
% 1.02/0.40 cnf(s51, plain, spl25_11 | spl25_13, inference(sat_conversion,[],[f422])).
% 1.02/0.40 cnf(s52, plain, spl25_11 | spl25_14, inference(sat_conversion,[],[f423])).
% 1.02/0.40 cnf(s53, plain, spl25_11 | spl25_15, inference(sat_conversion,[],[f424])).
% 1.02/0.40 cnf(s54, plain, spl25_12 | spl25_13, inference(sat_conversion,[],[f425])).
% 1.02/0.40 cnf(s55, plain, spl25_12 | spl25_14, inference(sat_conversion,[],[f426])).
% 1.02/0.40 cnf(s56, plain, spl25_12 | spl25_15, inference(sat_conversion,[],[f427])).
% 1.02/0.40 cnf(s57, plain, spl25_12 | ~spl25_16, inference(sat_conversion,[],[f432])).
% 1.02/0.40 cnf(s58, plain, spl25_11 | ~spl25_16, inference(sat_conversion,[],[f433])).
% 1.02/0.40 cnf(s59, plain, spl25_10 | ~spl25_16, inference(sat_conversion,[],[f434])).
% 1.02/0.40 cnf(s60, plain, spl25_12 | spl25_17, inference(sat_conversion,[],[f439])).
% 1.02/0.40 cnf(s61, plain, spl25_11 | spl25_17, inference(sat_conversion,[],[f440])).
% 1.02/0.40 cnf(s62, plain, spl25_10 | spl25_17, inference(sat_conversion,[],[f441])).
% 1.02/0.40 cnf(s63, plain, spl25_12 | spl25_18, inference(sat_conversion,[],[f446])).
% 1.02/0.40 cnf(s64, plain, spl25_11 | spl25_18, inference(sat_conversion,[],[f447])).
% 1.02/0.40 cnf(s65, plain, spl25_10 | spl25_18, inference(sat_conversion,[],[f448])).
% 1.02/0.40 cnf(s66, plain, spl25_12 | spl25_19, inference(sat_conversion,[],[f453])).
% 1.02/0.40 cnf(s67, plain, spl25_11 | spl25_19, inference(sat_conversion,[],[f454])).
% 1.02/0.40 cnf(s68, plain, spl25_10 | spl25_19, inference(sat_conversion,[],[f455])).
% 1.02/0.40 cnf(s69, plain, spl25_12 | spl25_20, inference(sat_conversion,[],[f460])).
% 1.02/0.40 cnf(s70, plain, spl25_11 | spl25_20, inference(sat_conversion,[],[f461])).
% 1.02/0.40 cnf(s71, plain, spl25_10 | spl25_20, inference(sat_conversion,[],[f462])).
% 1.02/0.40 cnf(s72, plain, spl25_9 | ~spl25_16, inference(sat_conversion,[],[f463])).
% 1.02/0.40 cnf(s73, plain, ~spl25_8 | ~spl25_16, inference(sat_conversion,[],[f464])).
% 1.02/0.40 cnf(s74, plain, spl25_7 | ~spl25_16, inference(sat_conversion,[],[f465])).
% 1.02/0.40 cnf(s75, plain, spl25_9 | spl25_17, inference(sat_conversion,[],[f466])).
% 1.02/0.40 cnf(s76, plain, ~spl25_8 | spl25_17, inference(sat_conversion,[],[f467])).
% 1.02/0.40 cnf(s77, plain, spl25_7 | spl25_17, inference(sat_conversion,[],[f468])).
% 1.02/0.40 cnf(s78, plain, spl25_9 | spl25_18, inference(sat_conversion,[],[f469])).
% 1.02/0.40 cnf(s79, plain, ~spl25_8 | spl25_18, inference(sat_conversion,[],[f470])).
% 1.02/0.40 cnf(s80, plain, spl25_7 | spl25_18, inference(sat_conversion,[],[f471])).
% 1.02/0.40 cnf(s81, plain, spl25_9 | spl25_19, inference(sat_conversion,[],[f472])).
% 1.02/0.40 cnf(s82, plain, ~spl25_8 | spl25_19, inference(sat_conversion,[],[f473])).
% 1.02/0.40 cnf(s83, plain, spl25_7 | spl25_19, inference(sat_conversion,[],[f474])).
% 1.02/0.40 cnf(s84, plain, spl25_9 | spl25_20, inference(sat_conversion,[],[f475])).
% 1.02/0.40 cnf(s85, plain, ~spl25_8 | spl25_20, inference(sat_conversion,[],[f476])).
% 1.02/0.40 cnf(s86, plain, spl25_7 | spl25_20, inference(sat_conversion,[],[f477])).
% 1.02/0.40 cnf(s91, plain, spl25_1 | ~spl25_16, inference(sat_conversion,[],[f482])).
% 1.02/0.40 cnf(s92, plain, spl25_1 | spl25_16, inference(sat_conversion,[],[f500])).
% 1.02/0.40 cnf(s104, plain, spl25_30 | spl25_33, inference(sat_conversion,[],[f776])).
% 1.02/0.40 cnf(s156, plain, ~spl25_30, inference(sat_conversion,[],[f2897])).
% 1.02/0.40 cnf(s161, plain, ~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9 | ~spl25_33 | ~spl25_60, inference(sat_conversion,[],[f2934])).
% 1.02/0.40 cnf(s175, plain, ~spl25_1 | ~spl25_7 | spl25_8 | ~spl25_9 | spl25_61, inference(sat_conversion,[],[f3122])).
% 1.02/0.40 cnf(s180, plain, spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | spl25_70 | spl25_71, inference(sat_conversion,[],[f3267])).
% 1.02/0.40 cnf(s188, plain, spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | spl25_35 | ~spl25_71, inference(sat_conversion,[],[f3368])).
% 1.02/0.40 cnf(s255, plain, ~spl25_7 | spl25_8 | ~spl25_9 | spl25_60 | ~spl25_70, inference(sat_conversion,[],[f4050])).
% 1.02/0.40 cnf(s301, plain, spl25_8 | ~spl25_10 | ~spl25_11 | ~spl25_12 | ~spl25_35 | ~spl25_61, inference(sat_conversion,[],[f4334])).
% 1.02/0.40 cnf(s305, plain, ~spl25_13 | ~spl25_14 | ~spl25_15 | spl25_16 | ~spl25_17 | ~spl25_18 | spl25_83 | spl25_84, inference(sat_conversion,[],[f4405])).
% 1.02/0.40 cnf(s352, plain, spl25_3 | ~spl25_6 | spl25_21 | spl25_22, inference(sat_conversion,[],[f4630])).
% 1.02/0.40 cnf(s415, plain, spl25_2 | ~spl25_4 | ~spl25_5 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_84, inference(sat_conversion,[],[f4889])).
% 1.02/0.40 cnf(s436, plain, ~spl25_4 | ~spl25_14 | ~spl25_19 | ~spl25_20 | ~spl25_22 | ~spl25_83, inference(sat_conversion,[],[f5102])).
% 1.02/0.40 cnf(s437, plain, ~spl25_4 | ~spl25_13 | ~spl25_19 | ~spl25_20 | ~spl25_21 | spl25_62, inference(sat_conversion,[],[f5104])).
% 1.02/0.40 cnf(s447, plain, ~spl25_1 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_33 | ~spl25_60, inference(sat_conversion,[],[f5245])).
% 1.02/0.40 cnf(s448, plain, ~spl25_4 | ~spl25_14 | ~spl25_15 | ~spl25_17 | ~spl25_18 | ~spl25_19 | ~spl25_20 | ~spl25_21 | spl25_60 | ~spl25_62, inference(sat_conversion,[],[f5248])).
% 1.02/0.40 cnf(s454, plain, spl25_33, inference(rat,[],[s104,s156])).
% 1.02/0.40 cnf(s458, plain, spl25_1, inference(rat,[],[s91,s92])).
% 1.02/0.40 cnf(s459, plain, spl25_4, inference(rat,[],[s180,s188,s255,s301,s161,s175,s8,s13,s18,s23,s28,s33,s458,s454])).
% 1.02/0.40 cnf(s460, plain, ~spl25_12 | ~spl25_11 | ~spl25_10 | spl25_70 | ~spl25_61 | spl25_8, inference(rat,[],[s188,s180,s301])).
% 1.02/0.40 cnf(s461, plain, spl25_12 | spl25_60 | ~spl25_6 | ~spl25_5 | spl25_3 | spl25_2, inference(rat,[],[s448,s437,s352,s436,s305,s415,s54,s55,s56,s57,s60,s63,s66,s69,s459])).
% 1.02/0.40 cnf(s462, plain, spl25_11 | spl25_60 | ~spl25_6 | ~spl25_5 | spl25_3 | spl25_2, inference(rat,[],[s448,s437,s352,s436,s305,s415,s51,s52,s53,s58,s61,s64,s67,s70,s459])).
% 1.02/0.40 cnf(s463, plain, ~spl25_9 | spl25_8 | ~spl25_7 | ~spl25_6 | ~spl25_5 | spl25_3 | spl25_2, inference(rat,[],[s448,s437,s352,s436,s305,s415,s48,s49,s50,s59,s62,s65,s68,s71,s460,s462,s461,s255,s161,s175,s459,s458,s454])).
% 1.02/0.40 cnf(s464, plain, spl25_9 | ~spl25_6 | ~spl25_5 | spl25_3 | spl25_2, inference(rat,[],[s448,s437,s352,s436,s305,s415,s447,s45,s46,s47,s72,s75,s78,s81,s84,s459,s458,s454])).
% 1.02/0.40 cnf(s465, plain, ~spl25_8 | ~spl25_6 | ~spl25_5 | spl25_3 | spl25_2, inference(rat,[],[s448,s437,s352,s436,s305,s415,s447,s42,s43,s44,s73,s76,s79,s82,s85,s459,s458,s454])).
% 1.02/0.40 cnf(s466, plain, spl25_8 | ~spl25_9 | spl25_2 | ~spl25_6 | ~spl25_5 | spl25_3, inference(rat,[],[s448,s437,s352,s436,s305,s415,s447,s39,s40,s41,s74,s77,s80,s83,s86,s463,s454,s458,s459])).
% 1.02/0.40 cnf(s467, plain, ~spl25_6 | ~spl25_5 | spl25_2 | spl25_3, inference(rat,[],[s466,s465,s464])).
% 1.02/0.40 cnf(s468, plain, spl25_6, inference(rat,[],[s255,s460,s161,s175,s10,s15,s20,s25,s30,s35,s458,s454])).
% 1.02/0.40 cnf(s469, plain, spl25_5, inference(rat,[],[s255,s460,s161,s175,s9,s14,s19,s24,s29,s34,s458,s454])).
% 1.02/0.40 cnf(s470, plain, ~spl25_3, inference(rat,[],[s255,s460,s161,s175,s7,s12,s17,s22,s27,s32,s458,s454])).
% 1.02/0.40 cnf(s471, plain, spl25_2, inference(rat,[],[s467,s468,s469,s470])).
% 1.02/0.40 cnf(s472, plain, spl25_12, inference(rat,[],[s31,s471])).
% 1.02/0.40 cnf(s473, plain, spl25_11, inference(rat,[],[s26,s471])).
% 1.02/0.40 cnf(s474, plain, spl25_10, inference(rat,[],[s21,s471])).
% 1.02/0.40 cnf(s475, plain, spl25_9, inference(rat,[],[s16,s471])).
% 1.02/0.40 cnf(s476, plain, ~spl25_8, inference(rat,[],[s11,s471])).
% 1.02/0.40 cnf(s477, plain, spl25_7, inference(rat,[],[s6,s471])).
% 1.02/0.40 cnf(s480, plain, spl25_61, inference(rat,[],[s175,s477,s475,s458,s476])).
% 1.02/0.40 cnf(s481, plain, ~spl25_60, inference(rat,[],[s161,s477,s454,s475,s458,s476])).
% 1.02/0.40 cnf(s486, plain, spl25_70, inference(rat,[],[s460,s476,s474,s473,s472,s480])).
% 1.02/0.40 cnf(s488, plain, $false, inference(rat,[],[s255,s477,s476,s475,s486,s481])).
% 1.02/0.40 tff(f5249,plain,(
% 1.02/0.40 $false),
% 1.02/0.40 inference(avatar_sat_refutation,[],[s488])).
% 1.02/0.40 % SZS output end Proof for theBenchmark
% 1.02/0.40 % (2314508)------------------------------
% 1.02/0.40 % (2314508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.40 % (2314508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.40 % (2314508)CaDiCaL version: 2.1.3
% 1.02/0.40 % (2314508)Termination reason: Refutation
% 1.02/0.40 % (2314508)Time elapsed: 0.127 s
% 1.02/0.40 % (2314508)Peak memory usage: 15 MB
% 1.02/0.40 % (2314508)Instructions burned: 205 (million)
% 1.02/0.40 % (2314502)Success in time 0.165 s
% 1.02/0.40 % Vampire exiting
%------------------------------------------------------------------------------