%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500^1.006 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:50:20 AM UTC 2026
% Result : Theorem 1.14s 0.47s
% Output : Refutation 1.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.006 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n019.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 17:11:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.14/0.47 % (1094376)Will run a generic schedule for satisfiability detection.
% 1.14/0.47 % (1094383)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2855007648:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.14/0.47 % (1094385)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3075623588:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.14/0.47 % (1094384)dis+10_1_sil=32000:sp=arity:random_seed=44121913:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.14/0.47 % (1094385)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.14/0.47 % (1094381)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=629288297_2999 on theBenchmark for (2999ds/0Mi)
% 1.14/0.47 % Exception at run slice level
% 1.14/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.14/0.47 % (1094382)% WARNING: option uhcvi not known.
% 1.14/0.47 % (1094387)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2940060957:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.14/0.47 % (1094382)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2190601891:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.14/0.47 % (1094382)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.14/0.47 % (1094382)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.14/0.47 % (1094386)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1973069861:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.14/0.47 % (1094392)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1059183503:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.14/0.47 % Exception at run slice level
% 1.14/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.14/0.47 % (1094397)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3729099754:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.14/0.47 % (1094387)Instruction limit reached!
% 1.14/0.47 % (1094387)------------------------------
% 1.14/0.47 % (1094387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094387)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094387)Termination reason: Instruction limit
% 1.14/0.47 % (1094387)Termination phase: Saturation
% 1.14/0.47 % (1094387)Time elapsed: 0.043 s
% 1.14/0.47 % (1094387)Peak memory usage: 12 MB
% 1.14/0.47 % (1094387)Instructions burned: 163 (million)
% 1.14/0.47 % (1094384)Instruction limit reached!
% 1.14/0.47 % (1094384)------------------------------
% 1.14/0.47 % (1094384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094384)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094384)Termination reason: Instruction limit
% 1.14/0.47 % (1094384)Termination phase: Saturation
% 1.14/0.47 % (1094384)Time elapsed: 0.051 s
% 1.14/0.47 % (1094384)Peak memory usage: 12 MB
% 1.14/0.47 % (1094384)Instructions burned: 104 (million)
% 1.14/0.47 % (1094385)Instruction limit reached!
% 1.14/0.47 % (1094385)------------------------------
% 1.14/0.47 % (1094385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094385)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094385)Termination reason: Instruction limit
% 1.14/0.47 % (1094385)Termination phase: Saturation
% 1.14/0.47 % (1094385)Time elapsed: 0.054 s
% 1.14/0.47 % (1094385)Peak memory usage: 12 MB
% 1.14/0.47 % (1094385)Instructions burned: 117 (million)
% 1.14/0.47 % (1094399)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=3812570951:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.14/0.47 % (1094399)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.14/0.47 % (1094399)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.14/0.47 % (1094400)ott-21_1_sil=16000:fs=off:random_seed=2339345844:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.14/0.47 % (1094401)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1164476555:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.14/0.47 % (1094397)Instruction limit reached!
% 1.14/0.47 % (1094397)------------------------------
% 1.14/0.47 % (1094397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094397)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094397)Termination reason: Instruction limit
% 1.14/0.47 % (1094397)Termination phase: Saturation
% 1.14/0.47 % (1094397)Time elapsed: 0.067 s
% 1.14/0.47 % (1094397)Peak memory usage: 12 MB
% 1.14/0.47 % (1094397)Instructions burned: 132 (million)
% 1.14/0.47 % (1094386)Instruction limit reached!
% 1.14/0.47 % (1094386)------------------------------
% 1.14/0.47 % (1094386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094386)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094386)Termination reason: Instruction limit
% 1.14/0.47 % (1094386)Termination phase: Saturation
% 1.14/0.47 % (1094386)Time elapsed: 0.104 s
% 1.14/0.47 % (1094386)Peak memory usage: 12 MB
% 1.14/0.47 % (1094386)Instructions burned: 132 (million)
% 1.14/0.47 % (1094406)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3433697413:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.14/0.47 % (1094405)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1321466174:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.14/0.47 % Exception at run slice level
% 1.14/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.14/0.47 % (1094400)Instruction limit reached!
% 1.14/0.47 % (1094400)------------------------------
% 1.14/0.47 % (1094400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.47 % (1094400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.47 % (1094400)CaDiCaL version: 2.1.3
% 1.14/0.47 % (1094400)Termination reason: Instruction limit
% 1.14/0.47 % (1094400)Termination phase: Saturation
% 1.14/0.47 % (1094400)Time elapsed: 0.071 s
% 1.14/0.47 % (1094400)Peak memory usage: 11 MB
% 1.14/0.47 % (1094400)Instructions burned: 180 (million)
% 1.14/0.47 % (1094409)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=153209587:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.14/0.47 % Exception at run slice level
% 1.14/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.14/0.47 % (1094410)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1391210453:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.14/0.47 % (1094410)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.14/0.47 % (1094406) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1094376-1094406"...
% 1.14/0.47 % (1094413)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1232112179:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 1.14/0.47 % (1094413)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.14/0.47 % (1094406)...printing done.
% 1.14/0.47 % (1094406)Refutation found. Thanks to Tanya!
% 1.14/0.47 % SZS status Theorem for theBenchmark
% 1.14/0.47 % SZS output start Proof for theBenchmark
% 1.14/0.47 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.14/0.47 thf(func_def_0, type, x: $o).
% 1.14/0.47 thf(func_def_1, type, f0: ($o > $o)).
% 1.14/0.47 thf(func_def_2, type, f1: ($o > $o)).
% 1.14/0.47 thf(func_def_3, type, f2: ($o > $o)).
% 1.14/0.47 thf(func_def_4, type, f3: ($o > $o)).
% 1.14/0.47 thf(func_def_5, type, f4: ($o > $o)).
% 1.14/0.47 thf(func_def_6, type, f5: ($o > $o)).
% 1.14/0.47 thf(func_def_10, type, sF0: $o).
% 1.14/0.47 thf(func_def_11, type, sF1: $o).
% 1.14/0.47 thf(func_def_12, type, sF2: $o).
% 1.14/0.47 thf(func_def_13, type, sF3: $o).
% 1.14/0.47 thf(func_def_14, type, sF4: $o).
% 1.14/0.47 thf(func_def_15, type, sF5: $o).
% 1.14/0.47 thf(func_def_16, type, sF6: $o).
% 1.14/0.47 thf(func_def_17, type, sF7: $o).
% 1.14/0.47 thf(func_def_18, type, sF8: $o).
% 1.14/0.47 thf(func_def_19, type, sF9: $o).
% 1.14/0.47 thf(func_def_20, type, sF10: $o).
% 1.14/0.47 thf(func_def_21, type, sF11: $o).
% 1.14/0.47 thf(func_def_22, type, sF12: $o).
% 1.14/0.47 thf(func_def_23, type, sF13: $o).
% 1.14/0.47 thf(func_def_24, type, sF14: $o).
% 1.14/0.47 thf(func_def_25, type, sF15: $o).
% 1.14/0.47 thf(func_def_26, type, sF16: $o).
% 1.14/0.47 thf(func_def_27, type, sF17: $o).
% 1.14/0.47 thf(func_def_28, type, sF18: $o).
% 1.14/0.47 thf(func_def_29, type, sF19: $o).
% 1.14/0.47 thf(func_def_30, type, sF20: $o).
% 1.14/0.47 thf(func_def_31, type, sF21: $o).
% 1.14/0.47 thf(func_def_32, type, sF22: $o).
% 1.14/0.47 thf(func_def_33, type, vNOT: ($o > $o)).
% 1.14/0.47 thf(f1,conjecture,(
% 1.14/0.47 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 1.14/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski6)).
% 1.14/0.47 thf(f2,negated_conjecture,(
% 1.14/0.47 ~ (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 1.14/0.47 inference(negated_conjecture,[status(cth)],[f1])).
% 1.14/0.47 thf(f3,plain,(
% 1.14/0.47 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 1.14/0.47 inference(flattening,[],[f2])).
% 1.14/0.47 thf(f4,plain,(
% 1.14/0.47 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 1.14/0.47 inference(cnf_transformation,[],[f3])).
% 1.14/0.47 thf(f6,definition,(
% 1.14/0.47 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.14/0.47 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.14/0.47 thf(f7,definition,(
% 1.14/0.47 (sF0 = ((f5 @ x)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 1.14/0.47 thf(f8,plain,(
% 1.14/0.47 (((f5 @ x)) = sF0)),
% 1.14/0.47 inference(reorient_equations,[],[f7])).
% 1.14/0.47 thf(f9,definition,(
% 1.14/0.47 (sF1 = ((f4 @ sF0)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 1.14/0.47 thf(f10,plain,(
% 1.14/0.47 (((f4 @ sF0)) = sF1)),
% 1.14/0.47 inference(reorient_equations,[],[f9])).
% 1.14/0.47 thf(f11,definition,(
% 1.14/0.47 (sF2 = ((f4 @ sF1)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 1.14/0.47 thf(f12,plain,(
% 1.14/0.47 (((f4 @ sF1)) = sF2)),
% 1.14/0.47 inference(reorient_equations,[],[f11])).
% 1.14/0.47 thf(f13,definition,(
% 1.14/0.47 (sF3 = ((f4 @ sF2)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 1.14/0.47 thf(f14,plain,(
% 1.14/0.47 (((f4 @ sF2)) = sF3)),
% 1.14/0.47 inference(reorient_equations,[],[f13])).
% 1.14/0.47 thf(f15,definition,(
% 1.14/0.47 (sF4 = ((f3 @ sF3)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 1.14/0.47 thf(f16,plain,(
% 1.14/0.47 (((f3 @ sF3)) = sF4)),
% 1.14/0.47 inference(reorient_equations,[],[f15])).
% 1.14/0.47 thf(f17,definition,(
% 1.14/0.47 (sF5 = ((f2 @ sF4)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 1.14/0.47 thf(f18,plain,(
% 1.14/0.47 (((f2 @ sF4)) = sF5)),
% 1.14/0.47 inference(reorient_equations,[],[f17])).
% 1.14/0.47 thf(f19,definition,(
% 1.14/0.47 (sF6 = ((f2 @ sF5)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 1.14/0.47 thf(f20,plain,(
% 1.14/0.47 (((f2 @ sF5)) = sF6)),
% 1.14/0.47 inference(reorient_equations,[],[f19])).
% 1.14/0.47 thf(f21,definition,(
% 1.14/0.47 (sF7 = ((f2 @ sF6)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 1.14/0.47 thf(f22,plain,(
% 1.14/0.47 (((f2 @ sF6)) = sF7)),
% 1.14/0.47 inference(reorient_equations,[],[f21])).
% 1.14/0.47 thf(f23,definition,(
% 1.14/0.47 (sF8 = ((f1 @ sF7)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 1.14/0.47 thf(f24,plain,(
% 1.14/0.47 (((f1 @ sF7)) = sF8)),
% 1.14/0.47 inference(reorient_equations,[],[f23])).
% 1.14/0.47 thf(f25,definition,(
% 1.14/0.47 (sF9 = ((f0 @ sF8)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 1.14/0.47 thf(f26,plain,(
% 1.14/0.47 (((f0 @ sF8)) = sF9)),
% 1.14/0.47 inference(reorient_equations,[],[f25])).
% 1.14/0.47 thf(f27,definition,(
% 1.14/0.47 (sF10 = ((f0 @ sF9)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 1.14/0.47 thf(f28,plain,(
% 1.14/0.47 (((f0 @ sF9)) = sF10)),
% 1.14/0.47 inference(reorient_equations,[],[f27])).
% 1.14/0.47 thf(f29,definition,(
% 1.14/0.47 (sF11 = ((f0 @ sF10)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 1.14/0.47 thf(f30,plain,(
% 1.14/0.47 (((f0 @ sF10)) = sF11)),
% 1.14/0.47 inference(reorient_equations,[],[f29])).
% 1.14/0.47 thf(f31,definition,(
% 1.14/0.47 (sF12 = ((f5 @ sF0)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 1.14/0.47 thf(f32,plain,(
% 1.14/0.47 (((f5 @ sF0)) = sF12)),
% 1.14/0.47 inference(reorient_equations,[],[f31])).
% 1.14/0.47 thf(f33,definition,(
% 1.14/0.47 (sF13 = ((f5 @ sF12)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 1.14/0.47 thf(f34,plain,(
% 1.14/0.47 (((f5 @ sF12)) = sF13)),
% 1.14/0.47 inference(reorient_equations,[],[f33])).
% 1.14/0.47 thf(f35,definition,(
% 1.14/0.47 (sF14 = ((f4 @ sF13)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 1.14/0.47 thf(f36,plain,(
% 1.14/0.47 (((f4 @ sF13)) = sF14)),
% 1.14/0.47 inference(reorient_equations,[],[f35])).
% 1.14/0.47 thf(f37,definition,(
% 1.14/0.47 (sF15 = ((f3 @ sF14)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 1.14/0.47 thf(f38,plain,(
% 1.14/0.47 (((f3 @ sF14)) = sF15)),
% 1.14/0.47 inference(reorient_equations,[],[f37])).
% 1.14/0.47 thf(f39,definition,(
% 1.14/0.47 (sF16 = ((f3 @ sF15)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 1.14/0.47 thf(f40,plain,(
% 1.14/0.47 (((f3 @ sF15)) = sF16)),
% 1.14/0.47 inference(reorient_equations,[],[f39])).
% 1.14/0.47 thf(f41,definition,(
% 1.14/0.47 (sF17 = ((f3 @ sF16)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 1.14/0.47 thf(f42,plain,(
% 1.14/0.47 (((f3 @ sF16)) = sF17)),
% 1.14/0.47 inference(reorient_equations,[],[f41])).
% 1.14/0.47 thf(f43,definition,(
% 1.14/0.47 (sF18 = ((f2 @ sF17)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 1.14/0.47 thf(f44,plain,(
% 1.14/0.47 (((f2 @ sF17)) = sF18)),
% 1.14/0.47 inference(reorient_equations,[],[f43])).
% 1.14/0.47 thf(f45,definition,(
% 1.14/0.47 (sF19 = ((f1 @ sF18)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 1.14/0.47 thf(f46,plain,(
% 1.14/0.47 (((f1 @ sF18)) = sF19)),
% 1.14/0.47 inference(reorient_equations,[],[f45])).
% 1.14/0.47 thf(f47,definition,(
% 1.14/0.47 (sF20 = ((f1 @ sF19)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 1.14/0.47 thf(f48,plain,(
% 1.14/0.47 (((f1 @ sF19)) = sF20)),
% 1.14/0.47 inference(reorient_equations,[],[f47])).
% 1.14/0.47 thf(f49,definition,(
% 1.14/0.47 (sF21 = ((f1 @ sF20)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 1.14/0.47 thf(f50,plain,(
% 1.14/0.47 (((f1 @ sF20)) = sF21)),
% 1.14/0.47 inference(reorient_equations,[],[f49])).
% 1.14/0.47 thf(f51,definition,(
% 1.14/0.47 (sF22 = ((f0 @ sF21)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 1.14/0.47 thf(f52,plain,(
% 1.14/0.47 (((f0 @ sF21)) = sF22)),
% 1.14/0.47 inference(reorient_equations,[],[f51])).
% 1.14/0.47 thf(f53,plain,(
% 1.14/0.47 (sF11 != sF22)),
% 1.14/0.47 inference(definition_folding,[],[f4,f52,f50,f48,f46,f44,f42,f40,f38,f36,f34,f32,f8,f30,f28,f26,f24,f22,f20,f18,f16,f14,f12,f10,f8])).
% 1.14/0.47 thf(f54,plain,(
% 1.14/0.47 ($true = sF11) | ($true = sF22)),
% 1.14/0.47 inference(xor_proxy_clausification,[],[f53])).
% 1.14/0.47 thf(f55,plain,(
% 1.14/0.47 ($false = sF11) | ($false = sF22)),
% 1.14/0.47 inference(xor_proxy_clausification,[],[f53])).
% 1.14/0.47 thf(f56,plain,(
% 1.14/0.47 (((f5 @ x)) = $true) | ($false = sF0)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f8])).
% 1.14/0.47 thf(f57,plain,(
% 1.14/0.47 (((f5 @ x)) = $false) | ($true = sF0)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f8])).
% 1.14/0.47 thf(f58,plain,(
% 1.14/0.47 ($true = ((f4 @ sF0))) | ($false = sF1)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f10])).
% 1.14/0.47 thf(f59,plain,(
% 1.14/0.47 ($false = ((f4 @ sF0))) | ($true = sF1)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f10])).
% 1.14/0.47 thf(f60,plain,(
% 1.14/0.47 ($true = ((f4 @ sF1))) | ($false = sF2)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f12])).
% 1.14/0.47 thf(f61,plain,(
% 1.14/0.47 ($false = ((f4 @ sF1))) | ($true = sF2)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f12])).
% 1.14/0.47 thf(f62,plain,(
% 1.14/0.47 ($true = ((f4 @ sF2))) | ($false = sF3)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f14])).
% 1.14/0.47 thf(f63,plain,(
% 1.14/0.47 ($false = ((f4 @ sF2))) | ($true = sF3)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f14])).
% 1.14/0.47 thf(f64,plain,(
% 1.14/0.47 ($true = ((f3 @ sF3))) | ($false = sF4)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f16])).
% 1.14/0.47 thf(f65,plain,(
% 1.14/0.47 ($false = ((f3 @ sF3))) | ($true = sF4)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f16])).
% 1.14/0.47 thf(f66,plain,(
% 1.14/0.47 ($true = ((f2 @ sF4))) | ($false = sF5)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f18])).
% 1.14/0.47 thf(f67,plain,(
% 1.14/0.47 ($false = ((f2 @ sF4))) | ($true = sF5)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f18])).
% 1.14/0.47 thf(f68,plain,(
% 1.14/0.47 ($true = ((f2 @ sF5))) | ($false = sF6)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f20])).
% 1.14/0.47 thf(f69,plain,(
% 1.14/0.47 ($false = ((f2 @ sF5))) | ($true = sF6)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f20])).
% 1.14/0.47 thf(f70,plain,(
% 1.14/0.47 ($true = ((f2 @ sF6))) | ($false = sF7)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f22])).
% 1.14/0.47 thf(f71,plain,(
% 1.14/0.47 ($false = ((f2 @ sF6))) | ($true = sF7)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f22])).
% 1.14/0.47 thf(f72,plain,(
% 1.14/0.47 ($true = ((f1 @ sF7))) | ($false = sF8)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f24])).
% 1.14/0.47 thf(f73,plain,(
% 1.14/0.47 ($false = ((f1 @ sF7))) | ($true = sF8)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f24])).
% 1.14/0.47 thf(f74,plain,(
% 1.14/0.47 ($true = ((f0 @ sF8))) | ($false = sF9)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f26])).
% 1.14/0.47 thf(f75,plain,(
% 1.14/0.47 ($false = ((f0 @ sF8))) | ($true = sF9)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f26])).
% 1.14/0.47 thf(f76,plain,(
% 1.14/0.47 ($true = ((f0 @ sF9))) | ($false = sF10)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f28])).
% 1.14/0.47 thf(f77,plain,(
% 1.14/0.47 ($false = ((f0 @ sF9))) | ($true = sF10)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f28])).
% 1.14/0.47 thf(f78,plain,(
% 1.14/0.47 ($true = ((f0 @ sF10))) | ($false = sF11)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f30])).
% 1.14/0.47 thf(f79,plain,(
% 1.14/0.47 ($false = ((f0 @ sF10))) | ($true = sF11)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f30])).
% 1.14/0.47 thf(f80,plain,(
% 1.14/0.47 ($true = ((f5 @ sF0))) | ($false = sF12)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f32])).
% 1.14/0.47 thf(f81,plain,(
% 1.14/0.47 ($false = ((f5 @ sF0))) | ($true = sF12)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f32])).
% 1.14/0.47 thf(f82,plain,(
% 1.14/0.47 ($true = ((f5 @ sF12))) | ($false = sF13)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f34])).
% 1.14/0.47 thf(f83,plain,(
% 1.14/0.47 ($false = ((f5 @ sF12))) | ($true = sF13)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f34])).
% 1.14/0.47 thf(f84,plain,(
% 1.14/0.47 ($true = ((f4 @ sF13))) | ($false = sF14)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f36])).
% 1.14/0.47 thf(f85,plain,(
% 1.14/0.47 ($false = ((f4 @ sF13))) | ($true = sF14)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f36])).
% 1.14/0.47 thf(f86,plain,(
% 1.14/0.47 ($true = ((f3 @ sF14))) | ($false = sF15)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f38])).
% 1.14/0.47 thf(f87,plain,(
% 1.14/0.47 ($false = ((f3 @ sF14))) | ($true = sF15)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f38])).
% 1.14/0.47 thf(f88,plain,(
% 1.14/0.47 ($true = ((f3 @ sF15))) | ($false = sF16)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f40])).
% 1.14/0.47 thf(f89,plain,(
% 1.14/0.47 ($false = ((f3 @ sF15))) | ($true = sF16)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f40])).
% 1.14/0.47 thf(f90,plain,(
% 1.14/0.47 ($true = ((f3 @ sF16))) | ($false = sF17)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f42])).
% 1.14/0.47 thf(f91,plain,(
% 1.14/0.47 ($false = ((f3 @ sF16))) | ($true = sF17)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f42])).
% 1.14/0.47 thf(f92,plain,(
% 1.14/0.47 ($true = ((f2 @ sF17))) | ($false = sF18)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f44])).
% 1.14/0.47 thf(f93,plain,(
% 1.14/0.47 ($false = ((f2 @ sF17))) | ($true = sF18)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f44])).
% 1.14/0.47 thf(f94,plain,(
% 1.14/0.47 ($true = ((f1 @ sF18))) | ($false = sF19)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f46])).
% 1.14/0.47 thf(f95,plain,(
% 1.14/0.47 ($false = ((f1 @ sF18))) | ($true = sF19)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f46])).
% 1.14/0.47 thf(f96,plain,(
% 1.14/0.47 ($true = ((f1 @ sF19))) | ($false = sF20)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f48])).
% 1.14/0.47 thf(f97,plain,(
% 1.14/0.47 ($false = ((f1 @ sF19))) | ($true = sF20)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f48])).
% 1.14/0.47 thf(f98,plain,(
% 1.14/0.47 ($true = ((f1 @ sF20))) | ($false = sF21)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f50])).
% 1.14/0.47 thf(f99,plain,(
% 1.14/0.47 ($false = ((f1 @ sF20))) | ($true = sF21)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f50])).
% 1.14/0.47 thf(f100,plain,(
% 1.14/0.47 ($true = ((f0 @ sF21))) | ($false = sF22)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f52])).
% 1.14/0.47 thf(f101,plain,(
% 1.14/0.47 ($false = ((f0 @ sF21))) | ($true = sF22)),
% 1.14/0.47 inference(iff_proxy_clausification,[],[f52])).
% 1.14/0.47 thf(f103,definition,(
% 1.14/0.47 spl23_1 <=> ($false = sF22)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition])).
% 1.14/0.47 thf(f105,plain,(
% 1.14/0.47 ($false = sF22) | ~spl23_1),
% 1.14/0.47 inference(avatar_component_clause,[],[f103])).
% 1.14/0.47 thf(f107,definition,(
% 1.14/0.47 spl23_2 <=> ($false = sF11)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition])).
% 1.14/0.47 thf(f109,plain,(
% 1.14/0.47 ($false = sF11) | ~spl23_2),
% 1.14/0.47 inference(avatar_component_clause,[],[f107])).
% 1.14/0.47 thf(f110,plain,(
% 1.14/0.47 spl23_1 | spl23_2),
% 1.14/0.47 inference(avatar_split_clause,[],[f55,f107,f103])).
% 1.14/0.47 thf(f112,definition,(
% 1.14/0.47 spl23_3 <=> ($true = sF22)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition])).
% 1.14/0.47 thf(f114,plain,(
% 1.14/0.47 ($true = sF22) | ~spl23_3),
% 1.14/0.47 inference(avatar_component_clause,[],[f112])).
% 1.14/0.47 thf(f116,definition,(
% 1.14/0.47 spl23_4 <=> ($true = sF11)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_4])],[avatar_definition])).
% 1.14/0.47 thf(f118,plain,(
% 1.14/0.47 ($true = sF11) | ~spl23_4),
% 1.14/0.47 inference(avatar_component_clause,[],[f116])).
% 1.14/0.47 thf(f119,plain,(
% 1.14/0.47 spl23_3 | spl23_4),
% 1.14/0.47 inference(avatar_split_clause,[],[f54,f116,f112])).
% 1.14/0.47 thf(f121,definition,(
% 1.14/0.47 spl23_5 <=> ($true = sF0)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition])).
% 1.14/0.47 thf(f122,plain,(
% 1.14/0.47 ($true != sF0) | spl23_5),
% 1.14/0.47 inference(avatar_component_clause,[],[f121])).
% 1.14/0.47 thf(f123,plain,(
% 1.14/0.47 ($true = sF0) | ~spl23_5),
% 1.14/0.47 inference(avatar_component_clause,[],[f121])).
% 1.14/0.47 thf(f125,definition,(
% 1.14/0.47 spl23_6 <=> (((f5 @ x)) = $false)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition])).
% 1.14/0.47 thf(f126,plain,(
% 1.14/0.47 (((f5 @ x)) != $false) | spl23_6),
% 1.14/0.47 inference(avatar_component_clause,[],[f125])).
% 1.14/0.47 thf(f127,plain,(
% 1.14/0.47 (((f5 @ x)) = $false) | ~spl23_6),
% 1.14/0.47 inference(avatar_component_clause,[],[f125])).
% 1.14/0.47 thf(f128,plain,(
% 1.14/0.47 spl23_5 | spl23_6),
% 1.14/0.47 inference(avatar_split_clause,[],[f57,f125,f121])).
% 1.14/0.47 thf(f130,definition,(
% 1.14/0.47 spl23_7 <=> ($false = sF0)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition])).
% 1.14/0.47 thf(f132,plain,(
% 1.14/0.47 ($false = sF0) | ~spl23_7),
% 1.14/0.47 inference(avatar_component_clause,[],[f130])).
% 1.14/0.47 thf(f134,definition,(
% 1.14/0.47 spl23_8 <=> (((f5 @ x)) = $true)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition])).
% 1.14/0.47 thf(f136,plain,(
% 1.14/0.47 (((f5 @ x)) = $true) | ~spl23_8),
% 1.14/0.47 inference(avatar_component_clause,[],[f134])).
% 1.14/0.47 thf(f137,plain,(
% 1.14/0.47 spl23_7 | spl23_8),
% 1.14/0.47 inference(avatar_split_clause,[],[f56,f134,f130])).
% 1.14/0.47 thf(f139,definition,(
% 1.14/0.47 spl23_9 <=> ($true = sF1)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition])).
% 1.14/0.47 thf(f140,plain,(
% 1.14/0.47 ($true != sF1) | spl23_9),
% 1.14/0.47 inference(avatar_component_clause,[],[f139])).
% 1.14/0.47 thf(f141,plain,(
% 1.14/0.47 ($true = sF1) | ~spl23_9),
% 1.14/0.47 inference(avatar_component_clause,[],[f139])).
% 1.14/0.47 thf(f143,definition,(
% 1.14/0.47 spl23_10 <=> ($false = ((f4 @ sF0)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition])).
% 1.14/0.47 thf(f144,plain,(
% 1.14/0.47 ($false != ((f4 @ sF0))) | spl23_10),
% 1.14/0.47 inference(avatar_component_clause,[],[f143])).
% 1.14/0.47 thf(f145,plain,(
% 1.14/0.47 ($false = ((f4 @ sF0))) | ~spl23_10),
% 1.14/0.47 inference(avatar_component_clause,[],[f143])).
% 1.14/0.47 thf(f146,plain,(
% 1.14/0.47 spl23_9 | spl23_10),
% 1.14/0.47 inference(avatar_split_clause,[],[f59,f143,f139])).
% 1.14/0.47 thf(f148,definition,(
% 1.14/0.47 spl23_11 <=> ($false = sF1)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition])).
% 1.14/0.47 thf(f150,plain,(
% 1.14/0.47 ($false = sF1) | ~spl23_11),
% 1.14/0.47 inference(avatar_component_clause,[],[f148])).
% 1.14/0.47 thf(f152,definition,(
% 1.14/0.47 spl23_12 <=> ($true = ((f4 @ sF0)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition])).
% 1.14/0.47 thf(f154,plain,(
% 1.14/0.47 ($true = ((f4 @ sF0))) | ~spl23_12),
% 1.14/0.47 inference(avatar_component_clause,[],[f152])).
% 1.14/0.47 thf(f155,plain,(
% 1.14/0.47 spl23_11 | spl23_12),
% 1.14/0.47 inference(avatar_split_clause,[],[f58,f152,f148])).
% 1.14/0.47 thf(f157,definition,(
% 1.14/0.47 spl23_13 <=> ($true = sF2)),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition])).
% 1.14/0.47 thf(f158,plain,(
% 1.14/0.47 ($true != sF2) | spl23_13),
% 1.14/0.47 inference(avatar_component_clause,[],[f157])).
% 1.14/0.47 thf(f159,plain,(
% 1.14/0.47 ($true = sF2) | ~spl23_13),
% 1.14/0.47 inference(avatar_component_clause,[],[f157])).
% 1.14/0.47 thf(f161,definition,(
% 1.14/0.47 spl23_14 <=> ($false = ((f4 @ sF1)))),
% 1.14/0.47 introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition])).
% 1.14/0.47 thf(f162,plain,(
% 1.14/0.47 ($false != ((f4 @ sF1))) | spl23_14),
% 1.14/0.47 inference(avatar_component_clause,[],[f161])).
% 1.14/0.47 thf(f163,plain,(
% 1.14/0.47 ($false = ((f4 @ sF1))) | ~spl23_14),
% 1.14/0.47 inference(avatar_component_clause,[],[f161])).
% 1.14/0.47 thf(f164,plain,(
% 1.14/0.47 spl23_13 | spl23_14),
% 1.14/0.47 inference(avatar_split_clause,[],[f61,f161,f157])).
% 1.14/0.47 thf(f166,definition,(
% 1.14/0.47 spl23_15 <=> ($false = sF2)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition])).
% 1.14/0.48 thf(f168,plain,(
% 1.14/0.48 ($false = sF2) | ~spl23_15),
% 1.14/0.48 inference(avatar_component_clause,[],[f166])).
% 1.14/0.48 thf(f170,definition,(
% 1.14/0.48 spl23_16 <=> ($true = ((f4 @ sF1)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition])).
% 1.14/0.48 thf(f172,plain,(
% 1.14/0.48 ($true = ((f4 @ sF1))) | ~spl23_16),
% 1.14/0.48 inference(avatar_component_clause,[],[f170])).
% 1.14/0.48 thf(f173,plain,(
% 1.14/0.48 spl23_15 | spl23_16),
% 1.14/0.48 inference(avatar_split_clause,[],[f60,f170,f166])).
% 1.14/0.48 thf(f175,definition,(
% 1.14/0.48 spl23_17 <=> ($true = sF3)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition])).
% 1.14/0.48 thf(f176,plain,(
% 1.14/0.48 ($true != sF3) | spl23_17),
% 1.14/0.48 inference(avatar_component_clause,[],[f175])).
% 1.14/0.48 thf(f177,plain,(
% 1.14/0.48 ($true = sF3) | ~spl23_17),
% 1.14/0.48 inference(avatar_component_clause,[],[f175])).
% 1.14/0.48 thf(f179,definition,(
% 1.14/0.48 spl23_18 <=> ($false = ((f4 @ sF2)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition])).
% 1.14/0.48 thf(f181,plain,(
% 1.14/0.48 ($false = ((f4 @ sF2))) | ~spl23_18),
% 1.14/0.48 inference(avatar_component_clause,[],[f179])).
% 1.14/0.48 thf(f182,plain,(
% 1.14/0.48 spl23_17 | spl23_18),
% 1.14/0.48 inference(avatar_split_clause,[],[f63,f179,f175])).
% 1.14/0.48 thf(f184,definition,(
% 1.14/0.48 spl23_19 <=> ($false = sF3)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition])).
% 1.14/0.48 thf(f186,plain,(
% 1.14/0.48 ($false = sF3) | ~spl23_19),
% 1.14/0.48 inference(avatar_component_clause,[],[f184])).
% 1.14/0.48 thf(f188,definition,(
% 1.14/0.48 spl23_20 <=> ($true = ((f4 @ sF2)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition])).
% 1.14/0.48 thf(f189,plain,(
% 1.14/0.48 ($true != ((f4 @ sF2))) | spl23_20),
% 1.14/0.48 inference(avatar_component_clause,[],[f188])).
% 1.14/0.48 thf(f190,plain,(
% 1.14/0.48 ($true = ((f4 @ sF2))) | ~spl23_20),
% 1.14/0.48 inference(avatar_component_clause,[],[f188])).
% 1.14/0.48 thf(f191,plain,(
% 1.14/0.48 spl23_19 | spl23_20),
% 1.14/0.48 inference(avatar_split_clause,[],[f62,f188,f184])).
% 1.14/0.48 thf(f193,definition,(
% 1.14/0.48 spl23_21 <=> ($true = sF4)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition])).
% 1.14/0.48 thf(f194,plain,(
% 1.14/0.48 ($true != sF4) | spl23_21),
% 1.14/0.48 inference(avatar_component_clause,[],[f193])).
% 1.14/0.48 thf(f195,plain,(
% 1.14/0.48 ($true = sF4) | ~spl23_21),
% 1.14/0.48 inference(avatar_component_clause,[],[f193])).
% 1.14/0.48 thf(f197,definition,(
% 1.14/0.48 spl23_22 <=> ($false = ((f3 @ sF3)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition])).
% 1.14/0.48 thf(f198,plain,(
% 1.14/0.48 ($false != ((f3 @ sF3))) | spl23_22),
% 1.14/0.48 inference(avatar_component_clause,[],[f197])).
% 1.14/0.48 thf(f199,plain,(
% 1.14/0.48 ($false = ((f3 @ sF3))) | ~spl23_22),
% 1.14/0.48 inference(avatar_component_clause,[],[f197])).
% 1.14/0.48 thf(f200,plain,(
% 1.14/0.48 spl23_21 | spl23_22),
% 1.14/0.48 inference(avatar_split_clause,[],[f65,f197,f193])).
% 1.14/0.48 thf(f202,definition,(
% 1.14/0.48 spl23_23 <=> ($false = sF4)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_23])],[avatar_definition])).
% 1.14/0.48 thf(f204,plain,(
% 1.14/0.48 ($false = sF4) | ~spl23_23),
% 1.14/0.48 inference(avatar_component_clause,[],[f202])).
% 1.14/0.48 thf(f206,definition,(
% 1.14/0.48 spl23_24 <=> ($true = ((f3 @ sF3)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_24])],[avatar_definition])).
% 1.14/0.48 thf(f207,plain,(
% 1.14/0.48 ($true != ((f3 @ sF3))) | spl23_24),
% 1.14/0.48 inference(avatar_component_clause,[],[f206])).
% 1.14/0.48 thf(f208,plain,(
% 1.14/0.48 ($true = ((f3 @ sF3))) | ~spl23_24),
% 1.14/0.48 inference(avatar_component_clause,[],[f206])).
% 1.14/0.48 thf(f209,plain,(
% 1.14/0.48 spl23_23 | spl23_24),
% 1.14/0.48 inference(avatar_split_clause,[],[f64,f206,f202])).
% 1.14/0.48 thf(f211,definition,(
% 1.14/0.48 spl23_25 <=> ($true = sF5)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition])).
% 1.14/0.48 thf(f213,plain,(
% 1.14/0.48 ($true = sF5) | ~spl23_25),
% 1.14/0.48 inference(avatar_component_clause,[],[f211])).
% 1.14/0.48 thf(f215,definition,(
% 1.14/0.48 spl23_26 <=> ($false = ((f2 @ sF4)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition])).
% 1.14/0.48 thf(f216,plain,(
% 1.14/0.48 ($false != ((f2 @ sF4))) | spl23_26),
% 1.14/0.48 inference(avatar_component_clause,[],[f215])).
% 1.14/0.48 thf(f217,plain,(
% 1.14/0.48 ($false = ((f2 @ sF4))) | ~spl23_26),
% 1.14/0.48 inference(avatar_component_clause,[],[f215])).
% 1.14/0.48 thf(f218,plain,(
% 1.14/0.48 spl23_25 | spl23_26),
% 1.14/0.48 inference(avatar_split_clause,[],[f67,f215,f211])).
% 1.14/0.48 thf(f220,definition,(
% 1.14/0.48 spl23_27 <=> ($false = sF5)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_27])],[avatar_definition])).
% 1.14/0.48 thf(f222,plain,(
% 1.14/0.48 ($false = sF5) | ~spl23_27),
% 1.14/0.48 inference(avatar_component_clause,[],[f220])).
% 1.14/0.48 thf(f224,definition,(
% 1.14/0.48 spl23_28 <=> ($true = ((f2 @ sF4)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition])).
% 1.14/0.48 thf(f226,plain,(
% 1.14/0.48 ($true = ((f2 @ sF4))) | ~spl23_28),
% 1.14/0.48 inference(avatar_component_clause,[],[f224])).
% 1.14/0.48 thf(f227,plain,(
% 1.14/0.48 spl23_27 | spl23_28),
% 1.14/0.48 inference(avatar_split_clause,[],[f66,f224,f220])).
% 1.14/0.48 thf(f229,definition,(
% 1.14/0.48 spl23_29 <=> ($true = sF6)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_29])],[avatar_definition])).
% 1.14/0.48 thf(f230,plain,(
% 1.14/0.48 ($true != sF6) | spl23_29),
% 1.14/0.48 inference(avatar_component_clause,[],[f229])).
% 1.14/0.48 thf(f231,plain,(
% 1.14/0.48 ($true = sF6) | ~spl23_29),
% 1.14/0.48 inference(avatar_component_clause,[],[f229])).
% 1.14/0.48 thf(f233,definition,(
% 1.14/0.48 spl23_30 <=> ($false = ((f2 @ sF5)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_30])],[avatar_definition])).
% 1.14/0.48 thf(f235,plain,(
% 1.14/0.48 ($false = ((f2 @ sF5))) | ~spl23_30),
% 1.14/0.48 inference(avatar_component_clause,[],[f233])).
% 1.14/0.48 thf(f236,plain,(
% 1.14/0.48 spl23_29 | spl23_30),
% 1.14/0.48 inference(avatar_split_clause,[],[f69,f233,f229])).
% 1.14/0.48 thf(f238,definition,(
% 1.14/0.48 spl23_31 <=> ($false = sF6)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_31])],[avatar_definition])).
% 1.14/0.48 thf(f239,plain,(
% 1.14/0.48 ($false != sF6) | spl23_31),
% 1.14/0.48 inference(avatar_component_clause,[],[f238])).
% 1.14/0.48 thf(f240,plain,(
% 1.14/0.48 ($false = sF6) | ~spl23_31),
% 1.14/0.48 inference(avatar_component_clause,[],[f238])).
% 1.14/0.48 thf(f242,definition,(
% 1.14/0.48 spl23_32 <=> ($true = ((f2 @ sF5)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition])).
% 1.14/0.48 thf(f244,plain,(
% 1.14/0.48 ($true = ((f2 @ sF5))) | ~spl23_32),
% 1.14/0.48 inference(avatar_component_clause,[],[f242])).
% 1.14/0.48 thf(f245,plain,(
% 1.14/0.48 spl23_31 | spl23_32),
% 1.14/0.48 inference(avatar_split_clause,[],[f68,f242,f238])).
% 1.14/0.48 thf(f247,definition,(
% 1.14/0.48 spl23_33 <=> ($true = sF7)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition])).
% 1.14/0.48 thf(f248,plain,(
% 1.14/0.48 ($true != sF7) | spl23_33),
% 1.14/0.48 inference(avatar_component_clause,[],[f247])).
% 1.14/0.48 thf(f249,plain,(
% 1.14/0.48 ($true = sF7) | ~spl23_33),
% 1.14/0.48 inference(avatar_component_clause,[],[f247])).
% 1.14/0.48 thf(f251,definition,(
% 1.14/0.48 spl23_34 <=> ($false = ((f2 @ sF6)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_34])],[avatar_definition])).
% 1.14/0.48 thf(f252,plain,(
% 1.14/0.48 ($false != ((f2 @ sF6))) | spl23_34),
% 1.14/0.48 inference(avatar_component_clause,[],[f251])).
% 1.14/0.48 thf(f253,plain,(
% 1.14/0.48 ($false = ((f2 @ sF6))) | ~spl23_34),
% 1.14/0.48 inference(avatar_component_clause,[],[f251])).
% 1.14/0.48 thf(f254,plain,(
% 1.14/0.48 spl23_33 | spl23_34),
% 1.14/0.48 inference(avatar_split_clause,[],[f71,f251,f247])).
% 1.14/0.48 thf(f256,definition,(
% 1.14/0.48 spl23_35 <=> ($false = sF7)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_35])],[avatar_definition])).
% 1.14/0.48 thf(f258,plain,(
% 1.14/0.48 ($false = sF7) | ~spl23_35),
% 1.14/0.48 inference(avatar_component_clause,[],[f256])).
% 1.14/0.48 thf(f260,definition,(
% 1.14/0.48 spl23_36 <=> ($true = ((f2 @ sF6)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition])).
% 1.14/0.48 thf(f262,plain,(
% 1.14/0.48 ($true = ((f2 @ sF6))) | ~spl23_36),
% 1.14/0.48 inference(avatar_component_clause,[],[f260])).
% 1.14/0.48 thf(f263,plain,(
% 1.14/0.48 spl23_35 | spl23_36),
% 1.14/0.48 inference(avatar_split_clause,[],[f70,f260,f256])).
% 1.14/0.48 thf(f265,definition,(
% 1.14/0.48 spl23_37 <=> ($true = sF8)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_37])],[avatar_definition])).
% 1.14/0.48 thf(f266,plain,(
% 1.14/0.48 ($true != sF8) | spl23_37),
% 1.14/0.48 inference(avatar_component_clause,[],[f265])).
% 1.14/0.48 thf(f267,plain,(
% 1.14/0.48 ($true = sF8) | ~spl23_37),
% 1.14/0.48 inference(avatar_component_clause,[],[f265])).
% 1.14/0.48 thf(f269,definition,(
% 1.14/0.48 spl23_38 <=> ($false = ((f1 @ sF7)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_38])],[avatar_definition])).
% 1.14/0.48 thf(f270,plain,(
% 1.14/0.48 ($false != ((f1 @ sF7))) | spl23_38),
% 1.14/0.48 inference(avatar_component_clause,[],[f269])).
% 1.14/0.48 thf(f271,plain,(
% 1.14/0.48 ($false = ((f1 @ sF7))) | ~spl23_38),
% 1.14/0.48 inference(avatar_component_clause,[],[f269])).
% 1.14/0.48 thf(f272,plain,(
% 1.14/0.48 spl23_37 | spl23_38),
% 1.14/0.48 inference(avatar_split_clause,[],[f73,f269,f265])).
% 1.14/0.48 thf(f274,definition,(
% 1.14/0.48 spl23_39 <=> ($false = sF8)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition])).
% 1.14/0.48 thf(f276,plain,(
% 1.14/0.48 ($false = sF8) | ~spl23_39),
% 1.14/0.48 inference(avatar_component_clause,[],[f274])).
% 1.14/0.48 thf(f278,definition,(
% 1.14/0.48 spl23_40 <=> ($true = ((f1 @ sF7)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition])).
% 1.14/0.48 thf(f279,plain,(
% 1.14/0.48 ($true != ((f1 @ sF7))) | spl23_40),
% 1.14/0.48 inference(avatar_component_clause,[],[f278])).
% 1.14/0.48 thf(f280,plain,(
% 1.14/0.48 ($true = ((f1 @ sF7))) | ~spl23_40),
% 1.14/0.48 inference(avatar_component_clause,[],[f278])).
% 1.14/0.48 thf(f281,plain,(
% 1.14/0.48 spl23_39 | spl23_40),
% 1.14/0.48 inference(avatar_split_clause,[],[f72,f278,f274])).
% 1.14/0.48 thf(f283,definition,(
% 1.14/0.48 spl23_41 <=> ($true = sF9)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_41])],[avatar_definition])).
% 1.14/0.48 thf(f285,plain,(
% 1.14/0.48 ($true = sF9) | ~spl23_41),
% 1.14/0.48 inference(avatar_component_clause,[],[f283])).
% 1.14/0.48 thf(f287,definition,(
% 1.14/0.48 spl23_42 <=> ($false = ((f0 @ sF8)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_42])],[avatar_definition])).
% 1.14/0.48 thf(f288,plain,(
% 1.14/0.48 ($false != ((f0 @ sF8))) | spl23_42),
% 1.14/0.48 inference(avatar_component_clause,[],[f287])).
% 1.14/0.48 thf(f289,plain,(
% 1.14/0.48 ($false = ((f0 @ sF8))) | ~spl23_42),
% 1.14/0.48 inference(avatar_component_clause,[],[f287])).
% 1.14/0.48 thf(f290,plain,(
% 1.14/0.48 spl23_41 | spl23_42),
% 1.14/0.48 inference(avatar_split_clause,[],[f75,f287,f283])).
% 1.14/0.48 thf(f292,definition,(
% 1.14/0.48 spl23_43 <=> ($false = sF9)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_43])],[avatar_definition])).
% 1.14/0.48 thf(f294,plain,(
% 1.14/0.48 ($false = sF9) | ~spl23_43),
% 1.14/0.48 inference(avatar_component_clause,[],[f292])).
% 1.14/0.48 thf(f296,definition,(
% 1.14/0.48 spl23_44 <=> ($true = ((f0 @ sF8)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_44])],[avatar_definition])).
% 1.14/0.48 thf(f298,plain,(
% 1.14/0.48 ($true = ((f0 @ sF8))) | ~spl23_44),
% 1.14/0.48 inference(avatar_component_clause,[],[f296])).
% 1.14/0.48 thf(f299,plain,(
% 1.14/0.48 spl23_43 | spl23_44),
% 1.14/0.48 inference(avatar_split_clause,[],[f74,f296,f292])).
% 1.14/0.48 thf(f301,definition,(
% 1.14/0.48 spl23_45 <=> ($true = sF10)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_45])],[avatar_definition])).
% 1.14/0.48 thf(f302,plain,(
% 1.14/0.48 ($true != sF10) | spl23_45),
% 1.14/0.48 inference(avatar_component_clause,[],[f301])).
% 1.14/0.48 thf(f303,plain,(
% 1.14/0.48 ($true = sF10) | ~spl23_45),
% 1.14/0.48 inference(avatar_component_clause,[],[f301])).
% 1.14/0.48 thf(f305,definition,(
% 1.14/0.48 spl23_46 <=> ($false = ((f0 @ sF9)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition])).
% 1.14/0.48 thf(f306,plain,(
% 1.14/0.48 ($false != ((f0 @ sF9))) | spl23_46),
% 1.14/0.48 inference(avatar_component_clause,[],[f305])).
% 1.14/0.48 thf(f307,plain,(
% 1.14/0.48 ($false = ((f0 @ sF9))) | ~spl23_46),
% 1.14/0.48 inference(avatar_component_clause,[],[f305])).
% 1.14/0.48 thf(f308,plain,(
% 1.14/0.48 spl23_45 | spl23_46),
% 1.14/0.48 inference(avatar_split_clause,[],[f77,f305,f301])).
% 1.14/0.48 thf(f310,definition,(
% 1.14/0.48 spl23_47 <=> ($false = sF10)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_47])],[avatar_definition])).
% 1.14/0.48 thf(f312,plain,(
% 1.14/0.48 ($false = sF10) | ~spl23_47),
% 1.14/0.48 inference(avatar_component_clause,[],[f310])).
% 1.14/0.48 thf(f314,definition,(
% 1.14/0.48 spl23_48 <=> ($true = ((f0 @ sF9)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_48])],[avatar_definition])).
% 1.14/0.48 thf(f316,plain,(
% 1.14/0.48 ($true = ((f0 @ sF9))) | ~spl23_48),
% 1.14/0.48 inference(avatar_component_clause,[],[f314])).
% 1.14/0.48 thf(f317,plain,(
% 1.14/0.48 spl23_47 | spl23_48),
% 1.14/0.48 inference(avatar_split_clause,[],[f76,f314,f310])).
% 1.14/0.48 thf(f319,definition,(
% 1.14/0.48 spl23_49 <=> ($false = ((f0 @ sF10)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_49])],[avatar_definition])).
% 1.14/0.48 thf(f321,plain,(
% 1.14/0.48 ($false = ((f0 @ sF10))) | ~spl23_49),
% 1.14/0.48 inference(avatar_component_clause,[],[f319])).
% 1.14/0.48 thf(f322,plain,(
% 1.14/0.48 spl23_4 | spl23_49),
% 1.14/0.48 inference(avatar_split_clause,[],[f79,f319,f116])).
% 1.14/0.48 thf(f324,definition,(
% 1.14/0.48 spl23_50 <=> ($true = ((f0 @ sF10)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition])).
% 1.14/0.48 thf(f326,plain,(
% 1.14/0.48 ($true = ((f0 @ sF10))) | ~spl23_50),
% 1.14/0.48 inference(avatar_component_clause,[],[f324])).
% 1.14/0.48 thf(f327,plain,(
% 1.14/0.48 spl23_2 | spl23_50),
% 1.14/0.48 inference(avatar_split_clause,[],[f78,f324,f107])).
% 1.14/0.48 thf(f329,definition,(
% 1.14/0.48 spl23_51 <=> ($true = sF12)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_51])],[avatar_definition])).
% 1.14/0.48 thf(f331,plain,(
% 1.14/0.48 ($true = sF12) | ~spl23_51),
% 1.14/0.48 inference(avatar_component_clause,[],[f329])).
% 1.14/0.48 thf(f333,definition,(
% 1.14/0.48 spl23_52 <=> ($false = ((f5 @ sF0)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_52])],[avatar_definition])).
% 1.14/0.48 thf(f334,plain,(
% 1.14/0.48 ($false != ((f5 @ sF0))) | spl23_52),
% 1.14/0.48 inference(avatar_component_clause,[],[f333])).
% 1.14/0.48 thf(f335,plain,(
% 1.14/0.48 ($false = ((f5 @ sF0))) | ~spl23_52),
% 1.14/0.48 inference(avatar_component_clause,[],[f333])).
% 1.14/0.48 thf(f336,plain,(
% 1.14/0.48 spl23_51 | spl23_52),
% 1.14/0.48 inference(avatar_split_clause,[],[f81,f333,f329])).
% 1.14/0.48 thf(f338,definition,(
% 1.14/0.48 spl23_53 <=> ($false = sF12)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_53])],[avatar_definition])).
% 1.14/0.48 thf(f340,plain,(
% 1.14/0.48 ($false = sF12) | ~spl23_53),
% 1.14/0.48 inference(avatar_component_clause,[],[f338])).
% 1.14/0.48 thf(f342,definition,(
% 1.14/0.48 spl23_54 <=> ($true = ((f5 @ sF0)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition])).
% 1.14/0.48 thf(f343,plain,(
% 1.14/0.48 ($true != ((f5 @ sF0))) | spl23_54),
% 1.14/0.48 inference(avatar_component_clause,[],[f342])).
% 1.14/0.48 thf(f344,plain,(
% 1.14/0.48 ($true = ((f5 @ sF0))) | ~spl23_54),
% 1.14/0.48 inference(avatar_component_clause,[],[f342])).
% 1.14/0.48 thf(f345,plain,(
% 1.14/0.48 spl23_53 | spl23_54),
% 1.14/0.48 inference(avatar_split_clause,[],[f80,f342,f338])).
% 1.14/0.48 thf(f347,definition,(
% 1.14/0.48 spl23_55 <=> ($true = sF13)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition])).
% 1.14/0.48 thf(f349,plain,(
% 1.14/0.48 ($true = sF13) | ~spl23_55),
% 1.14/0.48 inference(avatar_component_clause,[],[f347])).
% 1.14/0.48 thf(f351,definition,(
% 1.14/0.48 spl23_56 <=> ($false = ((f5 @ sF12)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_56])],[avatar_definition])).
% 1.14/0.48 thf(f352,plain,(
% 1.14/0.48 ($false != ((f5 @ sF12))) | spl23_56),
% 1.14/0.48 inference(avatar_component_clause,[],[f351])).
% 1.14/0.48 thf(f353,plain,(
% 1.14/0.48 ($false = ((f5 @ sF12))) | ~spl23_56),
% 1.14/0.48 inference(avatar_component_clause,[],[f351])).
% 1.14/0.48 thf(f354,plain,(
% 1.14/0.48 spl23_55 | spl23_56),
% 1.14/0.48 inference(avatar_split_clause,[],[f83,f351,f347])).
% 1.14/0.48 thf(f356,definition,(
% 1.14/0.48 spl23_57 <=> ($false = sF13)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_57])],[avatar_definition])).
% 1.14/0.48 thf(f358,plain,(
% 1.14/0.48 ($false = sF13) | ~spl23_57),
% 1.14/0.48 inference(avatar_component_clause,[],[f356])).
% 1.14/0.48 thf(f360,definition,(
% 1.14/0.48 spl23_58 <=> ($true = ((f5 @ sF12)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_58])],[avatar_definition])).
% 1.14/0.48 thf(f361,plain,(
% 1.14/0.48 ($true != ((f5 @ sF12))) | spl23_58),
% 1.14/0.48 inference(avatar_component_clause,[],[f360])).
% 1.14/0.48 thf(f362,plain,(
% 1.14/0.48 ($true = ((f5 @ sF12))) | ~spl23_58),
% 1.14/0.48 inference(avatar_component_clause,[],[f360])).
% 1.14/0.48 thf(f363,plain,(
% 1.14/0.48 spl23_57 | spl23_58),
% 1.14/0.48 inference(avatar_split_clause,[],[f82,f360,f356])).
% 1.14/0.48 thf(f365,definition,(
% 1.14/0.48 spl23_59 <=> ($true = sF14)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition])).
% 1.14/0.48 thf(f367,plain,(
% 1.14/0.48 ($true = sF14) | ~spl23_59),
% 1.14/0.48 inference(avatar_component_clause,[],[f365])).
% 1.14/0.48 thf(f369,definition,(
% 1.14/0.48 spl23_60 <=> ($false = ((f4 @ sF13)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_60])],[avatar_definition])).
% 1.14/0.48 thf(f371,plain,(
% 1.14/0.48 ($false = ((f4 @ sF13))) | ~spl23_60),
% 1.14/0.48 inference(avatar_component_clause,[],[f369])).
% 1.14/0.48 thf(f372,plain,(
% 1.14/0.48 spl23_59 | spl23_60),
% 1.14/0.48 inference(avatar_split_clause,[],[f85,f369,f365])).
% 1.14/0.48 thf(f374,definition,(
% 1.14/0.48 spl23_61 <=> ($false = sF14)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_61])],[avatar_definition])).
% 1.14/0.48 thf(f376,plain,(
% 1.14/0.48 ($false = sF14) | ~spl23_61),
% 1.14/0.48 inference(avatar_component_clause,[],[f374])).
% 1.14/0.48 thf(f378,definition,(
% 1.14/0.48 spl23_62 <=> ($true = ((f4 @ sF13)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_62])],[avatar_definition])).
% 1.14/0.48 thf(f379,plain,(
% 1.14/0.48 ($true != ((f4 @ sF13))) | spl23_62),
% 1.14/0.48 inference(avatar_component_clause,[],[f378])).
% 1.14/0.48 thf(f380,plain,(
% 1.14/0.48 ($true = ((f4 @ sF13))) | ~spl23_62),
% 1.14/0.48 inference(avatar_component_clause,[],[f378])).
% 1.14/0.48 thf(f381,plain,(
% 1.14/0.48 spl23_61 | spl23_62),
% 1.14/0.48 inference(avatar_split_clause,[],[f84,f378,f374])).
% 1.14/0.48 thf(f383,definition,(
% 1.14/0.48 spl23_63 <=> ($true = sF15)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_63])],[avatar_definition])).
% 1.14/0.48 thf(f384,plain,(
% 1.14/0.48 ($true != sF15) | spl23_63),
% 1.14/0.48 inference(avatar_component_clause,[],[f383])).
% 1.14/0.48 thf(f385,plain,(
% 1.14/0.48 ($true = sF15) | ~spl23_63),
% 1.14/0.48 inference(avatar_component_clause,[],[f383])).
% 1.14/0.48 thf(f387,definition,(
% 1.14/0.48 spl23_64 <=> ($false = ((f3 @ sF14)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_64])],[avatar_definition])).
% 1.14/0.48 thf(f388,plain,(
% 1.14/0.48 ($false != ((f3 @ sF14))) | spl23_64),
% 1.14/0.48 inference(avatar_component_clause,[],[f387])).
% 1.14/0.48 thf(f389,plain,(
% 1.14/0.48 ($false = ((f3 @ sF14))) | ~spl23_64),
% 1.14/0.48 inference(avatar_component_clause,[],[f387])).
% 1.14/0.48 thf(f390,plain,(
% 1.14/0.48 spl23_63 | spl23_64),
% 1.14/0.48 inference(avatar_split_clause,[],[f87,f387,f383])).
% 1.14/0.48 thf(f392,definition,(
% 1.14/0.48 spl23_65 <=> ($false = sF15)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition])).
% 1.14/0.48 thf(f394,plain,(
% 1.14/0.48 ($false = sF15) | ~spl23_65),
% 1.14/0.48 inference(avatar_component_clause,[],[f392])).
% 1.14/0.48 thf(f396,definition,(
% 1.14/0.48 spl23_66 <=> ($true = ((f3 @ sF14)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_66])],[avatar_definition])).
% 1.14/0.48 thf(f397,plain,(
% 1.14/0.48 ($true != ((f3 @ sF14))) | spl23_66),
% 1.14/0.48 inference(avatar_component_clause,[],[f396])).
% 1.14/0.48 thf(f398,plain,(
% 1.14/0.48 ($true = ((f3 @ sF14))) | ~spl23_66),
% 1.14/0.48 inference(avatar_component_clause,[],[f396])).
% 1.14/0.48 thf(f399,plain,(
% 1.14/0.48 spl23_65 | spl23_66),
% 1.14/0.48 inference(avatar_split_clause,[],[f86,f396,f392])).
% 1.14/0.48 thf(f401,definition,(
% 1.14/0.48 spl23_67 <=> ($true = sF16)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_67])],[avatar_definition])).
% 1.14/0.48 thf(f403,plain,(
% 1.14/0.48 ($true = sF16) | ~spl23_67),
% 1.14/0.48 inference(avatar_component_clause,[],[f401])).
% 1.14/0.48 thf(f405,definition,(
% 1.14/0.48 spl23_68 <=> ($false = ((f3 @ sF15)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_68])],[avatar_definition])).
% 1.14/0.48 thf(f406,plain,(
% 1.14/0.48 ($false != ((f3 @ sF15))) | spl23_68),
% 1.14/0.48 inference(avatar_component_clause,[],[f405])).
% 1.14/0.48 thf(f407,plain,(
% 1.14/0.48 ($false = ((f3 @ sF15))) | ~spl23_68),
% 1.14/0.48 inference(avatar_component_clause,[],[f405])).
% 1.14/0.48 thf(f408,plain,(
% 1.14/0.48 spl23_67 | spl23_68),
% 1.14/0.48 inference(avatar_split_clause,[],[f89,f405,f401])).
% 1.14/0.48 thf(f410,definition,(
% 1.14/0.48 spl23_69 <=> ($false = sF16)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_69])],[avatar_definition])).
% 1.14/0.48 thf(f411,plain,(
% 1.14/0.48 ($false != sF16) | spl23_69),
% 1.14/0.48 inference(avatar_component_clause,[],[f410])).
% 1.14/0.48 thf(f412,plain,(
% 1.14/0.48 ($false = sF16) | ~spl23_69),
% 1.14/0.48 inference(avatar_component_clause,[],[f410])).
% 1.14/0.48 thf(f414,definition,(
% 1.14/0.48 spl23_70 <=> ($true = ((f3 @ sF15)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_70])],[avatar_definition])).
% 1.14/0.48 thf(f415,plain,(
% 1.14/0.48 ($true != ((f3 @ sF15))) | spl23_70),
% 1.14/0.48 inference(avatar_component_clause,[],[f414])).
% 1.14/0.48 thf(f416,plain,(
% 1.14/0.48 ($true = ((f3 @ sF15))) | ~spl23_70),
% 1.14/0.48 inference(avatar_component_clause,[],[f414])).
% 1.14/0.48 thf(f417,plain,(
% 1.14/0.48 spl23_69 | spl23_70),
% 1.14/0.48 inference(avatar_split_clause,[],[f88,f414,f410])).
% 1.14/0.48 thf(f419,definition,(
% 1.14/0.48 spl23_71 <=> ($true = sF17)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_71])],[avatar_definition])).
% 1.14/0.48 thf(f421,plain,(
% 1.14/0.48 ($true = sF17) | ~spl23_71),
% 1.14/0.48 inference(avatar_component_clause,[],[f419])).
% 1.14/0.48 thf(f423,definition,(
% 1.14/0.48 spl23_72 <=> ($false = ((f3 @ sF16)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_72])],[avatar_definition])).
% 1.14/0.48 thf(f425,plain,(
% 1.14/0.48 ($false = ((f3 @ sF16))) | ~spl23_72),
% 1.14/0.48 inference(avatar_component_clause,[],[f423])).
% 1.14/0.48 thf(f426,plain,(
% 1.14/0.48 spl23_71 | spl23_72),
% 1.14/0.48 inference(avatar_split_clause,[],[f91,f423,f419])).
% 1.14/0.48 thf(f428,definition,(
% 1.14/0.48 spl23_73 <=> ($false = sF17)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_73])],[avatar_definition])).
% 1.14/0.48 thf(f430,plain,(
% 1.14/0.48 ($false = sF17) | ~spl23_73),
% 1.14/0.48 inference(avatar_component_clause,[],[f428])).
% 1.14/0.48 thf(f432,definition,(
% 1.14/0.48 spl23_74 <=> ($true = ((f3 @ sF16)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_74])],[avatar_definition])).
% 1.14/0.48 thf(f434,plain,(
% 1.14/0.48 ($true = ((f3 @ sF16))) | ~spl23_74),
% 1.14/0.48 inference(avatar_component_clause,[],[f432])).
% 1.14/0.48 thf(f435,plain,(
% 1.14/0.48 spl23_73 | spl23_74),
% 1.14/0.48 inference(avatar_split_clause,[],[f90,f432,f428])).
% 1.14/0.48 thf(f437,definition,(
% 1.14/0.48 spl23_75 <=> ($true = sF18)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_75])],[avatar_definition])).
% 1.14/0.48 thf(f439,plain,(
% 1.14/0.48 ($true = sF18) | ~spl23_75),
% 1.14/0.48 inference(avatar_component_clause,[],[f437])).
% 1.14/0.48 thf(f441,definition,(
% 1.14/0.48 spl23_76 <=> ($false = ((f2 @ sF17)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_76])],[avatar_definition])).
% 1.14/0.48 thf(f442,plain,(
% 1.14/0.48 ($false != ((f2 @ sF17))) | spl23_76),
% 1.14/0.48 inference(avatar_component_clause,[],[f441])).
% 1.14/0.48 thf(f443,plain,(
% 1.14/0.48 ($false = ((f2 @ sF17))) | ~spl23_76),
% 1.14/0.48 inference(avatar_component_clause,[],[f441])).
% 1.14/0.48 thf(f444,plain,(
% 1.14/0.48 spl23_75 | spl23_76),
% 1.14/0.48 inference(avatar_split_clause,[],[f93,f441,f437])).
% 1.14/0.48 thf(f446,definition,(
% 1.14/0.48 spl23_77 <=> ($false = sF18)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_77])],[avatar_definition])).
% 1.14/0.48 thf(f448,plain,(
% 1.14/0.48 ($false = sF18) | ~spl23_77),
% 1.14/0.48 inference(avatar_component_clause,[],[f446])).
% 1.14/0.48 thf(f450,definition,(
% 1.14/0.48 spl23_78 <=> ($true = ((f2 @ sF17)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_78])],[avatar_definition])).
% 1.14/0.48 thf(f451,plain,(
% 1.14/0.48 ($true != ((f2 @ sF17))) | spl23_78),
% 1.14/0.48 inference(avatar_component_clause,[],[f450])).
% 1.14/0.48 thf(f452,plain,(
% 1.14/0.48 ($true = ((f2 @ sF17))) | ~spl23_78),
% 1.14/0.48 inference(avatar_component_clause,[],[f450])).
% 1.14/0.48 thf(f453,plain,(
% 1.14/0.48 spl23_77 | spl23_78),
% 1.14/0.48 inference(avatar_split_clause,[],[f92,f450,f446])).
% 1.14/0.48 thf(f455,definition,(
% 1.14/0.48 spl23_79 <=> ($true = sF19)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_79])],[avatar_definition])).
% 1.14/0.48 thf(f456,plain,(
% 1.14/0.48 ($true != sF19) | spl23_79),
% 1.14/0.48 inference(avatar_component_clause,[],[f455])).
% 1.14/0.48 thf(f457,plain,(
% 1.14/0.48 ($true = sF19) | ~spl23_79),
% 1.14/0.48 inference(avatar_component_clause,[],[f455])).
% 1.14/0.48 thf(f459,definition,(
% 1.14/0.48 spl23_80 <=> ($false = ((f1 @ sF18)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_80])],[avatar_definition])).
% 1.14/0.48 thf(f460,plain,(
% 1.14/0.48 ($false != ((f1 @ sF18))) | spl23_80),
% 1.14/0.48 inference(avatar_component_clause,[],[f459])).
% 1.14/0.48 thf(f461,plain,(
% 1.14/0.48 ($false = ((f1 @ sF18))) | ~spl23_80),
% 1.14/0.48 inference(avatar_component_clause,[],[f459])).
% 1.14/0.48 thf(f462,plain,(
% 1.14/0.48 spl23_79 | spl23_80),
% 1.14/0.48 inference(avatar_split_clause,[],[f95,f459,f455])).
% 1.14/0.48 thf(f464,definition,(
% 1.14/0.48 spl23_81 <=> ($false = sF19)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_81])],[avatar_definition])).
% 1.14/0.48 thf(f466,plain,(
% 1.14/0.48 ($false = sF19) | ~spl23_81),
% 1.14/0.48 inference(avatar_component_clause,[],[f464])).
% 1.14/0.48 thf(f468,definition,(
% 1.14/0.48 spl23_82 <=> ($true = ((f1 @ sF18)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_82])],[avatar_definition])).
% 1.14/0.48 thf(f470,plain,(
% 1.14/0.48 ($true = ((f1 @ sF18))) | ~spl23_82),
% 1.14/0.48 inference(avatar_component_clause,[],[f468])).
% 1.14/0.48 thf(f471,plain,(
% 1.14/0.48 spl23_81 | spl23_82),
% 1.14/0.48 inference(avatar_split_clause,[],[f94,f468,f464])).
% 1.14/0.48 thf(f473,definition,(
% 1.14/0.48 spl23_83 <=> ($true = sF20)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_83])],[avatar_definition])).
% 1.14/0.48 thf(f475,plain,(
% 1.14/0.48 ($true = sF20) | ~spl23_83),
% 1.14/0.48 inference(avatar_component_clause,[],[f473])).
% 1.14/0.48 thf(f477,definition,(
% 1.14/0.48 spl23_84 <=> ($false = ((f1 @ sF19)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_84])],[avatar_definition])).
% 1.14/0.48 thf(f479,plain,(
% 1.14/0.48 ($false = ((f1 @ sF19))) | ~spl23_84),
% 1.14/0.48 inference(avatar_component_clause,[],[f477])).
% 1.14/0.48 thf(f480,plain,(
% 1.14/0.48 spl23_83 | spl23_84),
% 1.14/0.48 inference(avatar_split_clause,[],[f97,f477,f473])).
% 1.14/0.48 thf(f482,definition,(
% 1.14/0.48 spl23_85 <=> ($false = sF20)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_85])],[avatar_definition])).
% 1.14/0.48 thf(f484,plain,(
% 1.14/0.48 ($false = sF20) | ~spl23_85),
% 1.14/0.48 inference(avatar_component_clause,[],[f482])).
% 1.14/0.48 thf(f486,definition,(
% 1.14/0.48 spl23_86 <=> ($true = ((f1 @ sF19)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_86])],[avatar_definition])).
% 1.14/0.48 thf(f488,plain,(
% 1.14/0.48 ($true = ((f1 @ sF19))) | ~spl23_86),
% 1.14/0.48 inference(avatar_component_clause,[],[f486])).
% 1.14/0.48 thf(f489,plain,(
% 1.14/0.48 spl23_85 | spl23_86),
% 1.14/0.48 inference(avatar_split_clause,[],[f96,f486,f482])).
% 1.14/0.48 thf(f491,definition,(
% 1.14/0.48 spl23_87 <=> ($true = sF21)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_87])],[avatar_definition])).
% 1.14/0.48 thf(f493,plain,(
% 1.14/0.48 ($true = sF21) | ~spl23_87),
% 1.14/0.48 inference(avatar_component_clause,[],[f491])).
% 1.14/0.48 thf(f495,definition,(
% 1.14/0.48 spl23_88 <=> ($false = ((f1 @ sF20)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_88])],[avatar_definition])).
% 1.14/0.48 thf(f496,plain,(
% 1.14/0.48 ($false != ((f1 @ sF20))) | spl23_88),
% 1.14/0.48 inference(avatar_component_clause,[],[f495])).
% 1.14/0.48 thf(f497,plain,(
% 1.14/0.48 ($false = ((f1 @ sF20))) | ~spl23_88),
% 1.14/0.48 inference(avatar_component_clause,[],[f495])).
% 1.14/0.48 thf(f498,plain,(
% 1.14/0.48 spl23_87 | spl23_88),
% 1.14/0.48 inference(avatar_split_clause,[],[f99,f495,f491])).
% 1.14/0.48 thf(f500,definition,(
% 1.14/0.48 spl23_89 <=> ($false = sF21)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_89])],[avatar_definition])).
% 1.14/0.48 thf(f502,plain,(
% 1.14/0.48 ($false = sF21) | ~spl23_89),
% 1.14/0.48 inference(avatar_component_clause,[],[f500])).
% 1.14/0.48 thf(f504,definition,(
% 1.14/0.48 spl23_90 <=> ($true = ((f1 @ sF20)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_90])],[avatar_definition])).
% 1.14/0.48 thf(f505,plain,(
% 1.14/0.48 ($true != ((f1 @ sF20))) | spl23_90),
% 1.14/0.48 inference(avatar_component_clause,[],[f504])).
% 1.14/0.48 thf(f506,plain,(
% 1.14/0.48 ($true = ((f1 @ sF20))) | ~spl23_90),
% 1.14/0.48 inference(avatar_component_clause,[],[f504])).
% 1.14/0.48 thf(f507,plain,(
% 1.14/0.48 spl23_89 | spl23_90),
% 1.14/0.48 inference(avatar_split_clause,[],[f98,f504,f500])).
% 1.14/0.48 thf(f509,definition,(
% 1.14/0.48 spl23_91 <=> ($false = ((f0 @ sF21)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_91])],[avatar_definition])).
% 1.14/0.48 thf(f510,plain,(
% 1.14/0.48 ($false != ((f0 @ sF21))) | spl23_91),
% 1.14/0.48 inference(avatar_component_clause,[],[f509])).
% 1.14/0.48 thf(f511,plain,(
% 1.14/0.48 ($false = ((f0 @ sF21))) | ~spl23_91),
% 1.14/0.48 inference(avatar_component_clause,[],[f509])).
% 1.14/0.48 thf(f512,plain,(
% 1.14/0.48 spl23_3 | spl23_91),
% 1.14/0.48 inference(avatar_split_clause,[],[f101,f509,f112])).
% 1.14/0.48 thf(f514,definition,(
% 1.14/0.48 spl23_92 <=> ($true = ((f0 @ sF21)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_92])],[avatar_definition])).
% 1.14/0.48 thf(f515,plain,(
% 1.14/0.48 ($true != ((f0 @ sF21))) | spl23_92),
% 1.14/0.48 inference(avatar_component_clause,[],[f514])).
% 1.14/0.48 thf(f516,plain,(
% 1.14/0.48 ($true = ((f0 @ sF21))) | ~spl23_92),
% 1.14/0.48 inference(avatar_component_clause,[],[f514])).
% 1.14/0.48 thf(f517,plain,(
% 1.14/0.48 spl23_1 | spl23_92),
% 1.14/0.48 inference(avatar_split_clause,[],[f100,f514,f103])).
% 1.14/0.48 thf(f518,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_2 | ~spl23_4)),
% 1.14/0.48 inference(forward_demodulation,[],[f118,f109])).
% 1.14/0.48 thf(f519,plain,(
% 1.14/0.48 $false | (~spl23_2 | ~spl23_4)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f518])).
% 1.14/0.48 thf(f520,plain,(
% 1.14/0.48 ~spl23_2 | ~spl23_4),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f519])).
% 1.14/0.48 thf(f521,plain,(
% 1.14/0.48 ($true = ((f0 @ $true))) | (~spl23_87 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f516,f493])).
% 1.14/0.48 thf(f523,plain,(
% 1.14/0.48 ($false = ((f0 @ $true))) | (~spl23_45 | ~spl23_49)),
% 1.14/0.48 inference(forward_demodulation,[],[f321,f303])).
% 1.14/0.48 thf(f534,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_5 | ~spl23_7)),
% 1.14/0.48 inference(constrained_superposition,[],[f132,f123])).
% 1.14/0.48 thf(f538,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_7)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f534])).
% 1.14/0.48 thf(f539,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_7),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f538])).
% 1.14/0.48 thf(f543,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_9 | ~spl23_11)),
% 1.14/0.48 inference(constrained_superposition,[],[f150,f141])).
% 1.14/0.48 thf(f547,plain,(
% 1.14/0.48 $false | (~spl23_9 | ~spl23_11)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f543])).
% 1.14/0.48 thf(f548,plain,(
% 1.14/0.48 ~spl23_9 | ~spl23_11),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f547])).
% 1.14/0.48 thf(f551,plain,(
% 1.14/0.48 ($true = ((f4 @ $true))) | (~spl23_5 | ~spl23_12)),
% 1.14/0.48 inference(forward_demodulation,[],[f154,f123])).
% 1.14/0.48 thf(f561,plain,(
% 1.14/0.48 ($false = ((f4 @ $true))) | (~spl23_9 | ~spl23_14)),
% 1.14/0.48 inference(forward_demodulation,[],[f163,f141])).
% 1.14/0.48 thf(f563,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_17 | ~spl23_19)),
% 1.14/0.48 inference(constrained_superposition,[],[f186,f177])).
% 1.14/0.48 thf(f567,plain,(
% 1.14/0.48 $false | (~spl23_17 | ~spl23_19)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f563])).
% 1.14/0.48 thf(f568,plain,(
% 1.14/0.48 ~spl23_17 | ~spl23_19),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f567])).
% 1.14/0.48 thf(f571,plain,(
% 1.14/0.48 ($false = ((f4 @ $false))) | (~spl23_15 | ~spl23_18)),
% 1.14/0.48 inference(forward_demodulation,[],[f181,f168])).
% 1.14/0.48 thf(f573,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_21 | ~spl23_23)),
% 1.14/0.48 inference(constrained_superposition,[],[f204,f195])).
% 1.14/0.48 thf(f577,plain,(
% 1.14/0.48 $false | (~spl23_21 | ~spl23_23)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f573])).
% 1.14/0.48 thf(f578,plain,(
% 1.14/0.48 ~spl23_21 | ~spl23_23),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f577])).
% 1.14/0.48 thf(f581,plain,(
% 1.14/0.48 ($false = ((f3 @ $false))) | (~spl23_19 | ~spl23_22)),
% 1.14/0.48 inference(forward_demodulation,[],[f199,f186])).
% 1.14/0.48 thf(f591,plain,(
% 1.14/0.48 ($false = ((f2 @ $false))) | (~spl23_23 | ~spl23_26)),
% 1.14/0.48 inference(forward_demodulation,[],[f217,f204])).
% 1.14/0.48 thf(f601,plain,(
% 1.14/0.48 ($false = ((f2 @ $false))) | (~spl23_27 | ~spl23_30)),
% 1.14/0.48 inference(forward_demodulation,[],[f235,f222])).
% 1.14/0.48 thf(f603,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_33 | ~spl23_35)),
% 1.14/0.48 inference(constrained_superposition,[],[f258,f249])).
% 1.14/0.48 thf(f607,plain,(
% 1.14/0.48 $false | (~spl23_33 | ~spl23_35)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f603])).
% 1.14/0.48 thf(f608,plain,(
% 1.14/0.48 ~spl23_33 | ~spl23_35),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f607])).
% 1.14/0.48 thf(f611,plain,(
% 1.14/0.48 ($false = ((f2 @ $false))) | (~spl23_31 | ~spl23_34)),
% 1.14/0.48 inference(forward_demodulation,[],[f253,f240])).
% 1.14/0.48 thf(f613,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_37 | ~spl23_39)),
% 1.14/0.48 inference(constrained_superposition,[],[f276,f267])).
% 1.14/0.48 thf(f617,plain,(
% 1.14/0.48 $false | (~spl23_37 | ~spl23_39)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f613])).
% 1.14/0.48 thf(f618,plain,(
% 1.14/0.48 ~spl23_37 | ~spl23_39),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f617])).
% 1.14/0.48 thf(f621,plain,(
% 1.14/0.48 ($false = ((f1 @ $false))) | (~spl23_35 | ~spl23_38)),
% 1.14/0.48 inference(forward_demodulation,[],[f271,f258])).
% 1.14/0.48 thf(f631,plain,(
% 1.14/0.48 ($false = ((f0 @ $false))) | (~spl23_39 | ~spl23_42)),
% 1.14/0.48 inference(forward_demodulation,[],[f289,f276])).
% 1.14/0.48 thf(f641,plain,(
% 1.14/0.48 ($false = ((f0 @ $false))) | (~spl23_43 | ~spl23_46)),
% 1.14/0.48 inference(forward_demodulation,[],[f307,f294])).
% 1.14/0.48 thf(f642,plain,(
% 1.14/0.48 ($false = ((f0 @ $false))) | (~spl23_47 | ~spl23_49)),
% 1.14/0.48 inference(forward_demodulation,[],[f321,f312])).
% 1.14/0.48 thf(f644,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_51 | ~spl23_53)),
% 1.14/0.48 inference(constrained_superposition,[],[f340,f331])).
% 1.14/0.48 thf(f648,plain,(
% 1.14/0.48 $false | (~spl23_51 | ~spl23_53)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f644])).
% 1.14/0.48 thf(f649,plain,(
% 1.14/0.48 ~spl23_51 | ~spl23_53),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f648])).
% 1.14/0.48 thf(f652,plain,(
% 1.14/0.48 ($false = ((f5 @ $true))) | (~spl23_5 | ~spl23_52)),
% 1.14/0.48 inference(forward_demodulation,[],[f335,f123])).
% 1.14/0.48 thf(f672,plain,(
% 1.14/0.48 ($false = ((f4 @ $false))) | (~spl23_57 | ~spl23_60)),
% 1.14/0.48 inference(forward_demodulation,[],[f371,f358])).
% 1.14/0.48 thf(f682,plain,(
% 1.14/0.48 ($false = ((f3 @ $false))) | (~spl23_61 | ~spl23_64)),
% 1.14/0.48 inference(forward_demodulation,[],[f389,f376])).
% 1.14/0.48 thf(f692,plain,(
% 1.14/0.48 ($false = ((f3 @ $false))) | (~spl23_65 | ~spl23_68)),
% 1.14/0.48 inference(forward_demodulation,[],[f407,f394])).
% 1.14/0.48 thf(f702,plain,(
% 1.14/0.48 ($false = ((f3 @ $false))) | (~spl23_69 | ~spl23_72)),
% 1.14/0.48 inference(forward_demodulation,[],[f425,f412])).
% 1.14/0.48 thf(f712,plain,(
% 1.14/0.48 ($false = ((f2 @ $false))) | (~spl23_73 | ~spl23_76)),
% 1.14/0.48 inference(forward_demodulation,[],[f443,f430])).
% 1.14/0.48 thf(f722,plain,(
% 1.14/0.48 ($false = ((f1 @ $false))) | (~spl23_77 | ~spl23_80)),
% 1.14/0.48 inference(forward_demodulation,[],[f461,f448])).
% 1.14/0.48 thf(f732,plain,(
% 1.14/0.48 ($false = ((f1 @ $false))) | (~spl23_81 | ~spl23_84)),
% 1.14/0.48 inference(forward_demodulation,[],[f479,f466])).
% 1.14/0.48 thf(f742,plain,(
% 1.14/0.48 ($false = ((f1 @ $false))) | (~spl23_85 | ~spl23_88)),
% 1.14/0.48 inference(forward_demodulation,[],[f497,f484])).
% 1.14/0.48 thf(f743,plain,(
% 1.14/0.48 ($true = ((f0 @ $false))) | (~spl23_89 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f516,f502])).
% 1.14/0.48 thf(f744,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_39 | ~spl23_42 | ~spl23_89 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f743,f631])).
% 1.14/0.48 thf(f745,plain,(
% 1.14/0.48 $false | (~spl23_39 | ~spl23_42 | ~spl23_89 | ~spl23_92)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f744])).
% 1.14/0.48 thf(f746,plain,(
% 1.14/0.48 ~spl23_39 | ~spl23_42 | ~spl23_89 | ~spl23_92),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f745])).
% 1.14/0.48 thf(f754,plain,(
% 1.14/0.48 ($true = ((f2 @ $false))) | (~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_demodulation,[],[f262,f240])).
% 1.14/0.48 thf(f755,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_42 | ~spl23_44)),
% 1.14/0.48 inference(forward_demodulation,[],[f298,f289])).
% 1.14/0.48 thf(f756,plain,(
% 1.14/0.48 $false | (~spl23_42 | ~spl23_44)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f755])).
% 1.14/0.48 thf(f757,plain,(
% 1.14/0.48 ~spl23_42 | ~spl23_44),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f756])).
% 1.14/0.48 thf(f758,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_47 | ~spl23_49 | ~spl23_89 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f743,f642])).
% 1.14/0.48 thf(f759,plain,(
% 1.14/0.48 $false | (~spl23_47 | ~spl23_49 | ~spl23_89 | ~spl23_92)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f758])).
% 1.14/0.48 thf(f760,plain,(
% 1.14/0.48 ~spl23_47 | ~spl23_49 | ~spl23_89 | ~spl23_92),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f759])).
% 1.14/0.48 thf(f761,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_38 | ~spl23_40)),
% 1.14/0.48 inference(forward_demodulation,[],[f280,f271])).
% 1.14/0.48 thf(f762,plain,(
% 1.14/0.48 $false | (~spl23_38 | ~spl23_40)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f761])).
% 1.14/0.48 thf(f763,plain,(
% 1.14/0.48 ~spl23_38 | ~spl23_40),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f762])).
% 1.14/0.48 thf(f764,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_23 | ~spl23_26 | ~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_demodulation,[],[f754,f591])).
% 1.14/0.48 thf(f765,plain,(
% 1.14/0.48 $false | (~spl23_23 | ~spl23_26 | ~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f764])).
% 1.14/0.48 thf(f766,plain,(
% 1.14/0.48 ~spl23_23 | ~spl23_26 | ~spl23_31 | ~spl23_36),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f765])).
% 1.14/0.48 thf(f772,plain,(
% 1.14/0.48 ($false != ((f0 @ $true))) | (~spl23_37 | spl23_42)),
% 1.14/0.48 inference(forward_demodulation,[],[f288,f267])).
% 1.14/0.48 thf(f776,plain,(
% 1.14/0.48 ($true = ((f0 @ $true))) | (~spl23_37 | ~spl23_44)),
% 1.14/0.48 inference(forward_demodulation,[],[f298,f267])).
% 1.14/0.48 thf(f777,plain,(
% 1.14/0.48 ($true = ((f1 @ $false))) | (~spl23_35 | ~spl23_40)),
% 1.14/0.48 inference(forward_demodulation,[],[f280,f258])).
% 1.14/0.48 thf(f781,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_35 | ~spl23_40 | ~spl23_77 | ~spl23_80)),
% 1.14/0.48 inference(forward_demodulation,[],[f777,f722])).
% 1.14/0.48 thf(f782,plain,(
% 1.14/0.48 $false | (~spl23_35 | ~spl23_40 | ~spl23_77 | ~spl23_80)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f781])).
% 1.14/0.48 thf(f783,plain,(
% 1.14/0.48 ~spl23_35 | ~spl23_40 | ~spl23_77 | ~spl23_80),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f782])).
% 1.14/0.48 thf(f784,plain,(
% 1.14/0.48 $false | (~spl23_37 | spl23_42 | ~spl23_45 | ~spl23_49)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f523,f772])).
% 1.14/0.48 thf(f785,plain,(
% 1.14/0.48 ~spl23_37 | spl23_42 | ~spl23_45 | ~spl23_49),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f784])).
% 1.14/0.48 thf(f787,plain,(
% 1.14/0.48 ($true = ((f2 @ $false))) | (~spl23_73 | ~spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f452,f430])).
% 1.14/0.48 thf(f797,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_23 | ~spl23_26 | ~spl23_73 | ~spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f787,f591])).
% 1.14/0.48 thf(f798,plain,(
% 1.14/0.48 $false | (~spl23_23 | ~spl23_26 | ~spl23_73 | ~spl23_78)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f797])).
% 1.14/0.48 thf(f799,plain,(
% 1.14/0.48 ~spl23_23 | ~spl23_26 | ~spl23_73 | ~spl23_78),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f798])).
% 1.14/0.48 thf(f800,plain,(
% 1.14/0.48 ($false = ((f0 @ $true))) | (~spl23_41 | ~spl23_46)),
% 1.14/0.48 inference(forward_demodulation,[],[f307,f285])).
% 1.14/0.48 thf(f802,plain,(
% 1.14/0.48 ($true = ((f3 @ $false))) | (~spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(forward_demodulation,[],[f434,f412])).
% 1.14/0.48 thf(f812,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_35 | ~spl23_40 | ~spl23_85 | ~spl23_88)),
% 1.14/0.48 inference(forward_demodulation,[],[f777,f742])).
% 1.14/0.48 thf(f813,plain,(
% 1.14/0.48 $false | (~spl23_35 | ~spl23_40 | ~spl23_85 | ~spl23_88)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f812])).
% 1.14/0.48 thf(f814,plain,(
% 1.14/0.48 ~spl23_35 | ~spl23_40 | ~spl23_85 | ~spl23_88),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f813])).
% 1.14/0.48 thf(f815,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_76 | ~spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f452,f443])).
% 1.14/0.48 thf(f816,plain,(
% 1.14/0.48 $false | (~spl23_76 | ~spl23_78)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f815])).
% 1.14/0.48 thf(f817,plain,(
% 1.14/0.48 ~spl23_76 | ~spl23_78),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f816])).
% 1.14/0.48 thf(f822,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_19 | ~spl23_22 | ~spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(forward_demodulation,[],[f802,f581])).
% 1.14/0.48 thf(f823,plain,(
% 1.14/0.48 $false | (~spl23_19 | ~spl23_22 | ~spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f822])).
% 1.14/0.48 thf(f824,plain,(
% 1.14/0.48 ~spl23_19 | ~spl23_22 | ~spl23_69 | ~spl23_74),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f823])).
% 1.14/0.48 thf(f832,plain,(
% 1.14/0.48 ($false != ((f1 @ $false))) | (~spl23_77 | spl23_80)),
% 1.14/0.48 inference(forward_demodulation,[],[f460,f448])).
% 1.14/0.48 thf(f833,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_84 | ~spl23_86)),
% 1.14/0.48 inference(forward_demodulation,[],[f488,f479])).
% 1.14/0.48 thf(f834,plain,(
% 1.14/0.48 $false | (~spl23_84 | ~spl23_86)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f833])).
% 1.14/0.48 thf(f835,plain,(
% 1.14/0.48 ~spl23_84 | ~spl23_86),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f834])).
% 1.14/0.48 thf(f836,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_88 | ~spl23_90)),
% 1.14/0.48 inference(forward_demodulation,[],[f506,f497])).
% 1.14/0.48 thf(f837,plain,(
% 1.14/0.48 $false | (~spl23_88 | ~spl23_90)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f836])).
% 1.14/0.48 thf(f838,plain,(
% 1.14/0.48 ~spl23_88 | ~spl23_90),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f837])).
% 1.14/0.48 thf(f839,plain,(
% 1.14/0.48 ($true = ((f1 @ $false))) | (~spl23_77 | ~spl23_82)),
% 1.14/0.48 inference(forward_demodulation,[],[f470,f448])).
% 1.14/0.48 thf(f840,plain,(
% 1.14/0.48 ($false != ((f0 @ $false))) | (~spl23_39 | spl23_42)),
% 1.14/0.48 inference(forward_demodulation,[],[f288,f276])).
% 1.14/0.48 thf(f845,plain,(
% 1.14/0.48 $false | (~spl23_35 | ~spl23_38 | ~spl23_77 | spl23_80)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f832,f621])).
% 1.14/0.48 thf(f846,plain,(
% 1.14/0.48 ~spl23_35 | ~spl23_38 | ~spl23_77 | spl23_80),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f845])).
% 1.14/0.48 thf(f847,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_35 | ~spl23_38 | ~spl23_77 | ~spl23_82)),
% 1.14/0.48 inference(forward_demodulation,[],[f839,f621])).
% 1.14/0.48 thf(f848,plain,(
% 1.14/0.48 $false | (~spl23_35 | ~spl23_38 | ~spl23_77 | ~spl23_82)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f847])).
% 1.14/0.48 thf(f849,plain,(
% 1.14/0.48 ~spl23_35 | ~spl23_38 | ~spl23_77 | ~spl23_82),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f848])).
% 1.14/0.48 thf(f856,plain,(
% 1.14/0.48 ($true = ((f0 @ $false))) | (~spl23_47 | ~spl23_50)),
% 1.14/0.48 inference(forward_demodulation,[],[f326,f312])).
% 1.14/0.48 thf(f863,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_41 | ~spl23_46 | ~spl23_87 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f521,f800])).
% 1.14/0.48 thf(f864,plain,(
% 1.14/0.48 $false | (~spl23_41 | ~spl23_46 | ~spl23_87 | ~spl23_92)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f863])).
% 1.14/0.48 thf(f865,plain,(
% 1.14/0.48 ~spl23_41 | ~spl23_46 | ~spl23_87 | ~spl23_92),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f864])).
% 1.14/0.48 thf(f866,plain,(
% 1.14/0.48 ($false != ((f1 @ $false))) | (~spl23_85 | spl23_88)),
% 1.14/0.48 inference(forward_demodulation,[],[f496,f484])).
% 1.14/0.48 thf(f867,plain,(
% 1.14/0.48 ($true = ((f1 @ $false))) | (~spl23_85 | ~spl23_90)),
% 1.14/0.48 inference(forward_demodulation,[],[f506,f484])).
% 1.14/0.48 thf(f871,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_35 | ~spl23_38 | ~spl23_85 | ~spl23_90)),
% 1.14/0.48 inference(forward_demodulation,[],[f867,f621])).
% 1.14/0.48 thf(f872,plain,(
% 1.14/0.48 $false | (~spl23_35 | ~spl23_38 | ~spl23_85 | ~spl23_90)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f871])).
% 1.14/0.48 thf(f873,plain,(
% 1.14/0.48 ~spl23_35 | ~spl23_38 | ~spl23_85 | ~spl23_90),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f872])).
% 1.14/0.48 thf(f878,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_1 | ~spl23_3)),
% 1.14/0.48 inference(constrained_superposition,[],[f105,f114])).
% 1.14/0.48 thf(f882,plain,(
% 1.14/0.48 $false | (~spl23_1 | ~spl23_3)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f878])).
% 1.14/0.48 thf(f883,plain,(
% 1.14/0.48 ~spl23_1 | ~spl23_3),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f882])).
% 1.14/0.48 thf(f886,plain,(
% 1.14/0.48 ($false = ((f0 @ $false))) | (~spl23_89 | ~spl23_91)),
% 1.14/0.48 inference(forward_demodulation,[],[f511,f502])).
% 1.14/0.48 thf(f887,plain,(
% 1.14/0.48 $false | (~spl23_39 | spl23_42 | ~spl23_89 | ~spl23_91)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f886,f840])).
% 1.14/0.48 thf(f888,plain,(
% 1.14/0.48 ~spl23_39 | spl23_42 | ~spl23_89 | ~spl23_91),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f887])).
% 1.14/0.48 thf(f889,plain,(
% 1.14/0.48 ($true = ((f2 @ $false))) | (~spl23_27 | ~spl23_32)),
% 1.14/0.48 inference(forward_demodulation,[],[f244,f222])).
% 1.14/0.48 thf(f894,plain,(
% 1.14/0.48 ($false = ((f0 @ $true))) | (~spl23_87 | ~spl23_91)),
% 1.14/0.48 inference(forward_demodulation,[],[f511,f493])).
% 1.14/0.48 thf(f898,plain,(
% 1.14/0.48 $false | (~spl23_81 | ~spl23_84 | ~spl23_85 | spl23_88)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f732,f866])).
% 1.14/0.48 thf(f899,plain,(
% 1.14/0.48 ~spl23_81 | ~spl23_84 | ~spl23_85 | spl23_88),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f898])).
% 1.14/0.48 thf(f904,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_23 | ~spl23_26 | ~spl23_27 | ~spl23_32)),
% 1.14/0.48 inference(forward_demodulation,[],[f889,f591])).
% 1.14/0.48 thf(f905,plain,(
% 1.14/0.48 $false | (~spl23_23 | ~spl23_26 | ~spl23_27 | ~spl23_32)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f904])).
% 1.14/0.48 thf(f906,plain,(
% 1.14/0.48 ~spl23_23 | ~spl23_26 | ~spl23_27 | ~spl23_32),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f905])).
% 1.14/0.48 thf(f908,plain,(
% 1.14/0.48 ($true = ((f2 @ $false))) | (~spl23_23 | ~spl23_28)),
% 1.14/0.48 inference(forward_demodulation,[],[f226,f204])).
% 1.14/0.48 thf(f911,plain,(
% 1.14/0.48 ($true = ((f1 @ $false))) | (~spl23_81 | ~spl23_86)),
% 1.14/0.48 inference(forward_demodulation,[],[f488,f466])).
% 1.14/0.48 thf(f913,plain,(
% 1.14/0.48 ($true = ((f1 @ $true))) | (~spl23_83 | ~spl23_90)),
% 1.14/0.48 inference(forward_demodulation,[],[f506,f475])).
% 1.14/0.48 thf(f923,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_77 | ~spl23_80 | ~spl23_81 | ~spl23_86)),
% 1.14/0.48 inference(forward_demodulation,[],[f911,f722])).
% 1.14/0.48 thf(f924,plain,(
% 1.14/0.48 $false | (~spl23_77 | ~spl23_80 | ~spl23_81 | ~spl23_86)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f923])).
% 1.14/0.48 thf(f925,plain,(
% 1.14/0.48 ~spl23_77 | ~spl23_80 | ~spl23_81 | ~spl23_86),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f924])).
% 1.14/0.48 thf(f926,plain,(
% 1.14/0.48 ($true = ((f3 @ $false))) | (~spl23_19 | ~spl23_24)),
% 1.14/0.48 inference(forward_demodulation,[],[f208,f186])).
% 1.14/0.48 thf(f932,plain,(
% 1.14/0.48 ($true = ((f1 @ $true))) | (~spl23_79 | ~spl23_86)),
% 1.14/0.48 inference(forward_demodulation,[],[f488,f457])).
% 1.14/0.48 thf(f939,plain,(
% 1.14/0.48 ($true = ((f4 @ $false))) | (~spl23_15 | ~spl23_20)),
% 1.14/0.48 inference(forward_demodulation,[],[f190,f168])).
% 1.14/0.48 thf(f942,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_22 | ~spl23_24)),
% 1.14/0.48 inference(forward_demodulation,[],[f208,f199])).
% 1.14/0.48 thf(f943,plain,(
% 1.14/0.48 $false | (~spl23_22 | ~spl23_24)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f942])).
% 1.14/0.48 thf(f944,plain,(
% 1.14/0.48 ~spl23_22 | ~spl23_24),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f943])).
% 1.14/0.48 thf(f945,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_15 | ~spl23_18 | ~spl23_20)),
% 1.14/0.48 inference(forward_demodulation,[],[f939,f571])).
% 1.14/0.48 thf(f946,plain,(
% 1.14/0.48 $false | (~spl23_15 | ~spl23_18 | ~spl23_20)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f945])).
% 1.14/0.48 thf(f947,plain,(
% 1.14/0.48 ~spl23_15 | ~spl23_18 | ~spl23_20),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f946])).
% 1.14/0.48 thf(f949,plain,(
% 1.14/0.48 ($false != ((f3 @ $true))) | (~spl23_17 | spl23_22)),
% 1.14/0.48 inference(forward_demodulation,[],[f198,f177])).
% 1.14/0.48 thf(f950,plain,(
% 1.14/0.48 ($true = ((f3 @ $true))) | (~spl23_17 | ~spl23_24)),
% 1.14/0.48 inference(forward_demodulation,[],[f208,f177])).
% 1.14/0.48 thf(f951,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_15 | ~spl23_20 | ~spl23_57 | ~spl23_60)),
% 1.14/0.48 inference(forward_demodulation,[],[f939,f672])).
% 1.14/0.48 thf(f952,plain,(
% 1.14/0.48 $false | (~spl23_15 | ~spl23_20 | ~spl23_57 | ~spl23_60)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f951])).
% 1.14/0.48 thf(f953,plain,(
% 1.14/0.48 ~spl23_15 | ~spl23_20 | ~spl23_57 | ~spl23_60),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f952])).
% 1.14/0.48 thf(f956,plain,(
% 1.14/0.48 ($true = ((f5 @ $false))) | (~spl23_53 | ~spl23_58)),
% 1.14/0.48 inference(forward_demodulation,[],[f362,f340])).
% 1.14/0.48 thf(f961,plain,(
% 1.14/0.48 ($true = ((f5 @ $true))) | (~spl23_5 | ~spl23_54)),
% 1.14/0.48 inference(forward_demodulation,[],[f344,f123])).
% 1.14/0.48 thf(f962,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_56 | ~spl23_58)),
% 1.14/0.48 inference(forward_demodulation,[],[f362,f353])).
% 1.14/0.48 thf(f963,plain,(
% 1.14/0.48 $false | (~spl23_56 | ~spl23_58)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f962])).
% 1.14/0.48 thf(f964,plain,(
% 1.14/0.48 ~spl23_56 | ~spl23_58),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f963])).
% 1.14/0.48 thf(f968,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_52 | ~spl23_54)),
% 1.14/0.48 inference(forward_demodulation,[],[f344,f335])).
% 1.14/0.48 thf(f969,plain,(
% 1.14/0.48 $false | (~spl23_52 | ~spl23_54)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f968])).
% 1.14/0.48 thf(f970,plain,(
% 1.14/0.48 ~spl23_52 | ~spl23_54),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f969])).
% 1.14/0.48 thf(f973,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF0) | spl23_5),
% 1.14/0.48 inference(constrained_superposition,[],[f122,f6])).
% 1.14/0.48 thf(f974,plain,(
% 1.14/0.48 ($false = sF0) | spl23_5),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f973])).
% 1.14/0.48 thf(f991,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF7) | spl23_33),
% 1.14/0.48 inference(constrained_superposition,[],[f248,f6])).
% 1.14/0.48 thf(f992,plain,(
% 1.14/0.48 ($false = sF7) | spl23_33),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f991])).
% 1.14/0.48 thf(f997,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF8) | spl23_37),
% 1.14/0.48 inference(constrained_superposition,[],[f266,f6])).
% 1.14/0.48 thf(f998,plain,(
% 1.14/0.48 ($false = sF8) | spl23_37),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f997])).
% 1.14/0.48 thf(f1004,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF10) | spl23_45),
% 1.14/0.48 inference(constrained_superposition,[],[f302,f6])).
% 1.14/0.48 thf(f1005,plain,(
% 1.14/0.48 ($false = sF10) | spl23_45),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1004])).
% 1.14/0.48 thf(f1024,plain,(
% 1.14/0.48 ($false = ((f5 @ $true))) | (x = $false) | ~spl23_6),
% 1.14/0.48 inference(constrained_superposition,[],[f127,f6])).
% 1.14/0.48 thf(f1028,definition,(
% 1.14/0.48 spl23_93 <=> (x = $false)),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_93])],[avatar_definition])).
% 1.14/0.48 thf(f1030,plain,(
% 1.14/0.48 (x = $false) | ~spl23_93),
% 1.14/0.48 inference(avatar_component_clause,[],[f1028])).
% 1.14/0.48 thf(f1032,definition,(
% 1.14/0.48 spl23_94 <=> ($false = ((f5 @ $true)))),
% 1.14/0.48 introduced(definition,[new_symbols(definition,[spl23_94])],[avatar_definition])).
% 1.14/0.48 thf(f1034,plain,(
% 1.14/0.48 ($false = ((f5 @ $true))) | ~spl23_94),
% 1.14/0.48 inference(avatar_component_clause,[],[f1032])).
% 1.14/0.48 thf(f1035,plain,(
% 1.14/0.48 spl23_93 | spl23_94 | ~spl23_6),
% 1.14/0.48 inference(avatar_split_clause,[],[f1024,f125,f1032,f1028])).
% 1.14/0.48 thf(f1036,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_5 | ~spl23_9 | ~spl23_12 | ~spl23_14)),
% 1.14/0.48 inference(forward_demodulation,[],[f551,f561])).
% 1.14/0.48 thf(f1037,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_9 | ~spl23_12 | ~spl23_14)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1036])).
% 1.14/0.48 thf(f1038,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_9 | ~spl23_12 | ~spl23_14),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1037])).
% 1.14/0.48 thf(f1041,plain,(
% 1.14/0.48 spl23_7 | spl23_5),
% 1.14/0.48 inference(avatar_split_clause,[],[f974,f121,f130])).
% 1.14/0.48 thf(f1051,plain,(
% 1.14/0.48 ($false = ((f5 @ $false))) | (~spl23_6 | ~spl23_93)),
% 1.14/0.48 inference(constrained_superposition,[],[f127,f1030])).
% 1.14/0.48 thf(f1055,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_6 | ~spl23_8)),
% 1.14/0.48 inference(constrained_superposition,[],[f136,f127])).
% 1.14/0.48 thf(f1059,plain,(
% 1.14/0.48 $false | (~spl23_6 | ~spl23_8)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1055])).
% 1.14/0.48 thf(f1060,plain,(
% 1.14/0.48 ~spl23_6 | ~spl23_8),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1059])).
% 1.14/0.48 thf(f1066,plain,(
% 1.14/0.48 ($true = ((f4 @ $false))) | (~spl23_7 | ~spl23_12)),
% 1.14/0.48 inference(constrained_superposition,[],[f154,f132])).
% 1.14/0.48 thf(f1068,plain,(
% 1.14/0.48 ($false = ((f2 @ $true))) | (~spl23_21 | ~spl23_26)),
% 1.14/0.48 inference(constrained_superposition,[],[f217,f195])).
% 1.14/0.48 thf(f1072,plain,(
% 1.14/0.48 ($false = ((f2 @ $true))) | (~spl23_29 | ~spl23_34)),
% 1.14/0.48 inference(constrained_superposition,[],[f253,f231])).
% 1.14/0.48 thf(f1075,plain,(
% 1.14/0.48 ($true = ((f2 @ $true))) | ($false = sF6) | ~spl23_36),
% 1.14/0.48 inference(constrained_superposition,[],[f262,f6])).
% 1.14/0.48 thf(f1077,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_34 | ~spl23_36)),
% 1.14/0.48 inference(constrained_superposition,[],[f262,f253])).
% 1.14/0.48 thf(f1081,plain,(
% 1.14/0.48 $false | (~spl23_34 | ~spl23_36)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1077])).
% 1.14/0.48 thf(f1082,plain,(
% 1.14/0.48 ~spl23_34 | ~spl23_36),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1081])).
% 1.14/0.48 thf(f1086,plain,(
% 1.14/0.48 ($true = ((f2 @ $true))) | (spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1075,f239])).
% 1.14/0.48 thf(f1087,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_21 | ~spl23_26 | spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_demodulation,[],[f1086,f1068])).
% 1.14/0.48 thf(f1088,plain,(
% 1.14/0.48 $false | (~spl23_21 | ~spl23_26 | spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1087])).
% 1.14/0.48 thf(f1089,plain,(
% 1.14/0.48 ~spl23_21 | ~spl23_26 | spl23_31 | ~spl23_36),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1088])).
% 1.14/0.48 thf(f1090,plain,(
% 1.14/0.48 spl23_35 | spl23_33),
% 1.14/0.48 inference(avatar_split_clause,[],[f992,f247,f256])).
% 1.14/0.48 thf(f1095,plain,(
% 1.14/0.48 ($false = ((f0 @ $true))) | (~spl23_37 | ~spl23_42)),
% 1.14/0.48 inference(forward_demodulation,[],[f289,f267])).
% 1.14/0.48 thf(f1101,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_43 | ~spl23_46 | ~spl23_47 | ~spl23_50)),
% 1.14/0.48 inference(forward_demodulation,[],[f856,f641])).
% 1.14/0.48 thf(f1102,plain,(
% 1.14/0.48 $false | (~spl23_43 | ~spl23_46 | ~spl23_47 | ~spl23_50)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1101])).
% 1.14/0.48 thf(f1103,plain,(
% 1.14/0.48 ~spl23_43 | ~spl23_46 | ~spl23_47 | ~spl23_50),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1102])).
% 1.14/0.48 thf(f1108,plain,(
% 1.14/0.48 ($true = ((f0 @ $true))) | (~spl23_87 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f516,f493])).
% 1.14/0.48 thf(f1114,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_87 | ~spl23_91 | ~spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f1108,f894])).
% 1.14/0.48 thf(f1115,plain,(
% 1.14/0.48 $false | (~spl23_87 | ~spl23_91 | ~spl23_92)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1114])).
% 1.14/0.48 thf(f1116,plain,(
% 1.14/0.48 ~spl23_87 | ~spl23_91 | ~spl23_92),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1115])).
% 1.14/0.48 thf(f1117,plain,(
% 1.14/0.48 ($false != ((f0 @ $true))) | (~spl23_87 | spl23_91)),
% 1.14/0.48 inference(forward_demodulation,[],[f510,f493])).
% 1.14/0.48 thf(f1125,plain,(
% 1.14/0.48 $false | (~spl23_37 | ~spl23_42 | ~spl23_87 | spl23_91)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1117,f1095])).
% 1.14/0.48 thf(f1126,plain,(
% 1.14/0.48 ~spl23_37 | ~spl23_42 | ~spl23_87 | spl23_91),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1125])).
% 1.14/0.48 thf(f1127,plain,(
% 1.14/0.48 ($false != ((f0 @ $false))) | (~spl23_43 | spl23_46)),
% 1.14/0.48 inference(forward_demodulation,[],[f306,f294])).
% 1.14/0.48 thf(f1129,plain,(
% 1.14/0.48 ($true = ((f0 @ $false))) | (~spl23_43 | ~spl23_48)),
% 1.14/0.48 inference(forward_demodulation,[],[f316,f294])).
% 1.14/0.48 thf(f1131,plain,(
% 1.14/0.48 ($true != ((f1 @ $true))) | (~spl23_83 | spl23_90)),
% 1.14/0.48 inference(forward_demodulation,[],[f505,f475])).
% 1.14/0.48 thf(f1138,plain,(
% 1.14/0.48 $false | (~spl23_79 | ~spl23_83 | ~spl23_86 | spl23_90)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1131,f932])).
% 1.14/0.48 thf(f1139,plain,(
% 1.14/0.48 ~spl23_79 | ~spl23_83 | ~spl23_86 | spl23_90),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1138])).
% 1.14/0.48 thf(f1149,plain,(
% 1.14/0.48 ($true = ((f2 @ $false))) | (~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_demodulation,[],[f262,f240])).
% 1.14/0.48 thf(f1150,plain,(
% 1.14/0.48 ($false = ((f1 @ $true))) | (~spl23_79 | ~spl23_84)),
% 1.14/0.48 inference(forward_demodulation,[],[f479,f457])).
% 1.14/0.48 thf(f1160,plain,(
% 1.14/0.48 ($false != ((f1 @ $true))) | (~spl23_33 | spl23_38)),
% 1.14/0.48 inference(forward_demodulation,[],[f270,f249])).
% 1.14/0.48 thf(f1165,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_27 | ~spl23_30 | ~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(forward_demodulation,[],[f1149,f601])).
% 1.14/0.48 thf(f1166,plain,(
% 1.14/0.48 $false | (~spl23_27 | ~spl23_30 | ~spl23_31 | ~spl23_36)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1165])).
% 1.14/0.48 thf(f1167,plain,(
% 1.14/0.48 ~spl23_27 | ~spl23_30 | ~spl23_31 | ~spl23_36),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1166])).
% 1.14/0.48 thf(f1178,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_26 | ~spl23_28)),
% 1.14/0.48 inference(forward_demodulation,[],[f226,f217])).
% 1.14/0.48 thf(f1179,plain,(
% 1.14/0.48 $false | (~spl23_26 | ~spl23_28)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1178])).
% 1.14/0.48 thf(f1180,plain,(
% 1.14/0.48 ~spl23_26 | ~spl23_28),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1179])).
% 1.14/0.48 thf(f1203,plain,(
% 1.14/0.48 ($true = ((f2 @ $true))) | (~spl23_71 | ~spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f452,f421])).
% 1.14/0.48 thf(f1218,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_21 | ~spl23_26 | ~spl23_71 | ~spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f1203,f1068])).
% 1.14/0.48 thf(f1219,plain,(
% 1.14/0.48 $false | (~spl23_21 | ~spl23_26 | ~spl23_71 | ~spl23_78)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1218])).
% 1.14/0.48 thf(f1220,plain,(
% 1.14/0.48 ~spl23_21 | ~spl23_26 | ~spl23_71 | ~spl23_78),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1219])).
% 1.14/0.48 thf(f1237,plain,(
% 1.14/0.48 ($true != ((f3 @ $true))) | (~spl23_17 | spl23_24)),
% 1.14/0.48 inference(forward_demodulation,[],[f207,f177])).
% 1.14/0.48 thf(f1246,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF4) | spl23_21),
% 1.14/0.48 inference(constrained_superposition,[],[f194,f6])).
% 1.14/0.48 thf(f1247,plain,(
% 1.14/0.48 ($false = sF4) | spl23_21),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1246])).
% 1.14/0.48 thf(f1255,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF6) | spl23_29),
% 1.14/0.48 inference(constrained_superposition,[],[f230,f6])).
% 1.14/0.48 thf(f1256,plain,(
% 1.14/0.48 ($false = sF6) | spl23_29),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1255])).
% 1.14/0.48 thf(f1270,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF19) | spl23_79),
% 1.14/0.48 inference(constrained_superposition,[],[f456,f6])).
% 1.14/0.48 thf(f1271,plain,(
% 1.14/0.48 ($false = sF19) | spl23_79),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1270])).
% 1.14/0.48 thf(f1285,plain,(
% 1.14/0.48 ($false != ((f5 @ $false))) | (~spl23_7 | spl23_52)),
% 1.14/0.48 inference(constrained_superposition,[],[f334,f132])).
% 1.14/0.48 thf(f1287,plain,(
% 1.14/0.48 $false | (~spl23_6 | ~spl23_7 | spl23_52 | ~spl23_93)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1285,f1051])).
% 1.14/0.48 thf(f1288,plain,(
% 1.14/0.48 ~spl23_6 | ~spl23_7 | spl23_52 | ~spl23_93),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1287])).
% 1.14/0.48 thf(f1294,plain,(
% 1.14/0.48 ($false != ((f5 @ $true))) | (~spl23_51 | spl23_56)),
% 1.14/0.48 inference(constrained_superposition,[],[f352,f331])).
% 1.14/0.48 thf(f1296,plain,(
% 1.14/0.48 $false | (~spl23_51 | spl23_56 | ~spl23_94)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1294,f1034])).
% 1.14/0.48 thf(f1297,plain,(
% 1.14/0.48 ~spl23_51 | spl23_56 | ~spl23_94),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1296])).
% 1.14/0.48 thf(f1302,plain,(
% 1.14/0.48 ($true != ((f5 @ $false))) | (~spl23_7 | spl23_54)),
% 1.14/0.48 inference(forward_demodulation,[],[f343,f132])).
% 1.14/0.48 thf(f1303,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_53 | spl23_54 | ~spl23_58)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1302,f956])).
% 1.14/0.48 thf(f1304,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_53 | spl23_54 | ~spl23_58),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1303])).
% 1.14/0.48 thf(f1305,plain,(
% 1.14/0.48 spl23_94 | ~spl23_5 | ~spl23_52),
% 1.14/0.48 inference(avatar_split_clause,[],[f652,f333,f121,f1032])).
% 1.14/0.48 thf(f1307,plain,(
% 1.14/0.48 ($false = ((f4 @ $true))) | (~spl23_5 | ~spl23_10)),
% 1.14/0.48 inference(forward_demodulation,[],[f145,f123])).
% 1.14/0.48 thf(f1308,plain,(
% 1.14/0.48 ($false = ((f4 @ $false))) | (~spl23_11 | ~spl23_14)),
% 1.14/0.48 inference(forward_demodulation,[],[f163,f150])).
% 1.14/0.48 thf(f1311,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF1) | spl23_9),
% 1.14/0.48 inference(constrained_superposition,[],[f140,f6])).
% 1.14/0.48 thf(f1312,plain,(
% 1.14/0.48 ($false = sF1) | spl23_9),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1311])).
% 1.14/0.48 thf(f1323,plain,(
% 1.14/0.48 ($false != ((f5 @ $true))) | (x = $false) | spl23_6),
% 1.14/0.48 inference(constrained_superposition,[],[f126,f6])).
% 1.14/0.48 thf(f1325,plain,(
% 1.14/0.48 (x = $false) | (spl23_6 | ~spl23_94)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1323,f1034])).
% 1.14/0.48 thf(f1326,plain,(
% 1.14/0.48 spl23_93 | spl23_6 | ~spl23_94),
% 1.14/0.48 inference(avatar_split_clause,[],[f1325,f1032,f125,f1028])).
% 1.14/0.48 thf(f1328,plain,(
% 1.14/0.48 ($false != ((f5 @ $false))) | (spl23_6 | ~spl23_93)),
% 1.14/0.48 inference(constrained_superposition,[],[f126,f1030])).
% 1.14/0.48 thf(f1338,plain,(
% 1.14/0.48 ($false = ((f4 @ $true))) | (~spl23_55 | ~spl23_60)),
% 1.14/0.48 inference(constrained_superposition,[],[f371,f349])).
% 1.14/0.48 thf(f1353,plain,(
% 1.14/0.48 ($true = ((f3 @ $false))) | (~spl23_61 | ~spl23_66)),
% 1.14/0.48 inference(forward_demodulation,[],[f398,f376])).
% 1.14/0.48 thf(f1380,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20)),
% 1.14/0.48 inference(constrained_superposition,[],[f1308,f939])).
% 1.14/0.48 thf(f1381,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20)),
% 1.14/0.48 inference(constrained_superposition,[],[f939,f1308])).
% 1.14/0.48 thf(f1382,plain,(
% 1.14/0.48 $false | (~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1381])).
% 1.14/0.48 thf(f1383,plain,(
% 1.14/0.48 ~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1382])).
% 1.14/0.48 thf(f1384,plain,(
% 1.14/0.48 $false | (~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1380])).
% 1.14/0.48 thf(f1385,plain,(
% 1.14/0.48 ~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1384])).
% 1.14/0.48 thf(f1390,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_19 | ~spl23_22 | ~spl23_61 | ~spl23_66)),
% 1.14/0.48 inference(forward_demodulation,[],[f1353,f581])).
% 1.14/0.48 thf(f1391,plain,(
% 1.14/0.48 $false | (~spl23_19 | ~spl23_22 | ~spl23_61 | ~spl23_66)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1390])).
% 1.14/0.48 thf(f1392,plain,(
% 1.14/0.48 ~spl23_19 | ~spl23_22 | ~spl23_61 | ~spl23_66),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1391])).
% 1.14/0.48 thf(f1403,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_60 | ~spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f380,f371])).
% 1.14/0.48 thf(f1404,plain,(
% 1.14/0.48 $false | (~spl23_60 | ~spl23_62)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1403])).
% 1.14/0.48 thf(f1405,plain,(
% 1.14/0.48 ~spl23_60 | ~spl23_62),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1404])).
% 1.14/0.48 thf(f1406,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_68 | ~spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f416,f407])).
% 1.14/0.48 thf(f1407,plain,(
% 1.14/0.48 $false | (~spl23_68 | ~spl23_70)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1406])).
% 1.14/0.48 thf(f1408,plain,(
% 1.14/0.48 ~spl23_68 | ~spl23_70),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1407])).
% 1.14/0.48 thf(f1409,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_64 | ~spl23_66)),
% 1.14/0.48 inference(forward_demodulation,[],[f398,f389])).
% 1.14/0.48 thf(f1410,plain,(
% 1.14/0.48 $false | (~spl23_64 | ~spl23_66)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1409])).
% 1.14/0.48 thf(f1411,plain,(
% 1.14/0.48 ~spl23_64 | ~spl23_66),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1410])).
% 1.14/0.48 thf(f1414,plain,(
% 1.14/0.48 ($false != ((f3 @ $false))) | (~spl23_65 | spl23_68)),
% 1.14/0.48 inference(forward_demodulation,[],[f406,f394])).
% 1.14/0.48 thf(f1415,plain,(
% 1.14/0.48 ($true = ((f3 @ $false))) | (~spl23_65 | ~spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f416,f394])).
% 1.14/0.48 thf(f1416,plain,(
% 1.14/0.48 $false | (~spl23_19 | ~spl23_22 | ~spl23_65 | spl23_68)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1414,f581])).
% 1.14/0.48 thf(f1417,plain,(
% 1.14/0.48 ~spl23_19 | ~spl23_22 | ~spl23_65 | spl23_68),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1416])).
% 1.14/0.48 thf(f1418,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_19 | ~spl23_22 | ~spl23_65 | ~spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f1415,f581])).
% 1.14/0.48 thf(f1419,plain,(
% 1.14/0.48 $false | (~spl23_19 | ~spl23_22 | ~spl23_65 | ~spl23_70)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1418])).
% 1.14/0.48 thf(f1420,plain,(
% 1.14/0.48 ~spl23_19 | ~spl23_22 | ~spl23_65 | ~spl23_70),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1419])).
% 1.14/0.48 thf(f1425,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_61 | ~spl23_64 | ~spl23_65 | ~spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f1415,f682])).
% 1.14/0.48 thf(f1426,plain,(
% 1.14/0.48 $false | (~spl23_61 | ~spl23_64 | ~spl23_65 | ~spl23_70)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1425])).
% 1.14/0.48 thf(f1427,plain,(
% 1.14/0.48 ~spl23_61 | ~spl23_64 | ~spl23_65 | ~spl23_70),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1426])).
% 1.14/0.48 thf(f1437,plain,(
% 1.14/0.48 ($true = ((f4 @ $true))) | (~spl23_55 | ~spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f380,f349])).
% 1.14/0.48 thf(f1440,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_14 | ~spl23_16)),
% 1.14/0.48 inference(forward_demodulation,[],[f172,f163])).
% 1.14/0.48 thf(f1441,plain,(
% 1.14/0.48 $false | (~spl23_14 | ~spl23_16)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1440])).
% 1.14/0.48 thf(f1442,plain,(
% 1.14/0.48 ~spl23_14 | ~spl23_16),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1441])).
% 1.14/0.48 thf(f1448,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_5 | ~spl23_10 | ~spl23_55 | ~spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f1437,f1307])).
% 1.14/0.48 thf(f1449,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_10 | ~spl23_55 | ~spl23_62)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1448])).
% 1.14/0.48 thf(f1450,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_10 | ~spl23_55 | ~spl23_62),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1449])).
% 1.14/0.48 thf(f1460,plain,(
% 1.14/0.48 ($true = ((f4 @ $false))) | (~spl23_57 | ~spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f380,f358])).
% 1.14/0.48 thf(f1461,plain,(
% 1.14/0.48 ($false = ((f4 @ $false))) | (~spl23_7 | ~spl23_10)),
% 1.14/0.48 inference(forward_demodulation,[],[f145,f132])).
% 1.14/0.48 thf(f1476,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF2) | spl23_13),
% 1.14/0.48 inference(constrained_superposition,[],[f158,f6])).
% 1.14/0.48 thf(f1477,plain,(
% 1.14/0.48 ($false = sF2) | spl23_13),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1476])).
% 1.14/0.48 thf(f1488,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF15) | spl23_63),
% 1.14/0.48 inference(constrained_superposition,[],[f384,f6])).
% 1.14/0.48 thf(f1489,plain,(
% 1.14/0.48 ($false = sF15) | spl23_63),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1488])).
% 1.14/0.48 thf(f1509,plain,(
% 1.14/0.48 ($true = ((f3 @ $true))) | ($false = sF16) | ~spl23_74),
% 1.14/0.48 inference(constrained_superposition,[],[f434,f6])).
% 1.14/0.48 thf(f1510,plain,(
% 1.14/0.48 ($true = ((f3 @ $true))) | (~spl23_67 | ~spl23_74)),
% 1.14/0.48 inference(constrained_superposition,[],[f434,f403])).
% 1.14/0.48 thf(f1511,plain,(
% 1.14/0.48 $false | (~spl23_17 | spl23_24 | ~spl23_67 | ~spl23_74)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1510,f1237])).
% 1.14/0.48 thf(f1512,plain,(
% 1.14/0.48 ~spl23_17 | spl23_24 | ~spl23_67 | ~spl23_74),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1511])).
% 1.14/0.48 thf(f1513,plain,(
% 1.14/0.48 ($false = sF16) | (~spl23_17 | spl23_24 | ~spl23_74)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1509,f1237])).
% 1.14/0.48 thf(f1514,plain,(
% 1.14/0.48 $false | (~spl23_17 | spl23_24 | spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1513,f411])).
% 1.14/0.48 thf(f1515,plain,(
% 1.14/0.48 ~spl23_17 | spl23_24 | spl23_69 | ~spl23_74),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1514])).
% 1.14/0.48 thf(f1517,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_65 | ~spl23_68 | ~spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(forward_demodulation,[],[f802,f692])).
% 1.14/0.48 thf(f1518,plain,(
% 1.14/0.48 $false | (~spl23_65 | ~spl23_68 | ~spl23_69 | ~spl23_74)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1517])).
% 1.14/0.48 thf(f1519,plain,(
% 1.14/0.48 ~spl23_65 | ~spl23_68 | ~spl23_69 | ~spl23_74),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1518])).
% 1.14/0.48 thf(f1524,plain,(
% 1.14/0.48 ($false != ((f3 @ $true))) | (~spl23_59 | spl23_64)),
% 1.14/0.48 inference(forward_demodulation,[],[f388,f367])).
% 1.14/0.48 thf(f1526,plain,(
% 1.14/0.48 ($true = ((f3 @ $true))) | (~spl23_59 | ~spl23_66)),
% 1.14/0.48 inference(forward_demodulation,[],[f398,f367])).
% 1.14/0.48 thf(f1532,plain,(
% 1.14/0.48 $false | (~spl23_17 | spl23_24 | ~spl23_59 | ~spl23_66)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1526,f1237])).
% 1.14/0.48 thf(f1533,plain,(
% 1.14/0.48 ~spl23_17 | spl23_24 | ~spl23_59 | ~spl23_66),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1532])).
% 1.14/0.48 thf(f1536,plain,(
% 1.14/0.48 ($true != ((f4 @ $false))) | (~spl23_15 | spl23_20)),
% 1.14/0.48 inference(forward_demodulation,[],[f189,f168])).
% 1.14/0.48 thf(f1539,plain,(
% 1.14/0.48 ($false != ((f3 @ $true))) | (~spl23_63 | spl23_68)),
% 1.14/0.48 inference(forward_demodulation,[],[f406,f385])).
% 1.14/0.48 thf(f1541,plain,(
% 1.14/0.48 ($true = ((f3 @ $true))) | (~spl23_63 | ~spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f416,f385])).
% 1.14/0.48 thf(f1543,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_12 | ~spl23_15 | spl23_20)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1536,f1066])).
% 1.14/0.48 thf(f1544,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_12 | ~spl23_15 | spl23_20),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1543])).
% 1.14/0.48 thf(f1546,plain,(
% 1.14/0.48 spl23_11 | spl23_9),
% 1.14/0.48 inference(avatar_split_clause,[],[f1312,f139,f148])).
% 1.14/0.48 thf(f1550,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_7 | ~spl23_10 | ~spl23_57 | ~spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f1460,f1461])).
% 1.14/0.48 thf(f1551,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_10 | ~spl23_57 | ~spl23_62)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1550])).
% 1.14/0.48 thf(f1552,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_10 | ~spl23_57 | ~spl23_62),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1551])).
% 1.14/0.48 thf(f1565,plain,(
% 1.14/0.48 ($false = ((f3 @ $true))) | (~spl23_67 | ~spl23_72)),
% 1.14/0.48 inference(forward_demodulation,[],[f425,f403])).
% 1.14/0.48 thf(f1582,plain,(
% 1.14/0.48 ($true != $true) | ($false = sF3) | spl23_17),
% 1.14/0.48 inference(constrained_superposition,[],[f176,f6])).
% 1.14/0.48 thf(f1583,plain,(
% 1.14/0.48 ($false = sF3) | spl23_17),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1582])).
% 1.14/0.48 thf(f1626,plain,(
% 1.14/0.48 $false | (~spl23_63 | ~spl23_67 | spl23_68 | ~spl23_72)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1539,f1565])).
% 1.14/0.48 thf(f1627,plain,(
% 1.14/0.48 ~spl23_63 | ~spl23_67 | spl23_68 | ~spl23_72),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1626])).
% 1.14/0.48 thf(f1628,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_63 | ~spl23_67 | ~spl23_70 | ~spl23_72)),
% 1.14/0.48 inference(forward_demodulation,[],[f1541,f1565])).
% 1.14/0.48 thf(f1629,plain,(
% 1.14/0.48 $false | (~spl23_63 | ~spl23_67 | ~spl23_70 | ~spl23_72)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1628])).
% 1.14/0.48 thf(f1630,plain,(
% 1.14/0.48 ~spl23_63 | ~spl23_67 | ~spl23_70 | ~spl23_72),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1629])).
% 1.14/0.48 thf(f1632,plain,(
% 1.14/0.48 spl23_65 | spl23_63),
% 1.14/0.48 inference(avatar_split_clause,[],[f1489,f383,f392])).
% 1.14/0.48 thf(f1636,plain,(
% 1.14/0.48 ($true != ((f3 @ $false))) | (~spl23_61 | spl23_66)),
% 1.14/0.48 inference(forward_demodulation,[],[f397,f376])).
% 1.14/0.48 thf(f1643,plain,(
% 1.14/0.48 $false | (~spl23_19 | ~spl23_24 | ~spl23_61 | spl23_66)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1636,f926])).
% 1.14/0.48 thf(f1644,plain,(
% 1.14/0.48 ~spl23_19 | ~spl23_24 | ~spl23_61 | spl23_66),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1643])).
% 1.14/0.48 thf(f1653,plain,(
% 1.14/0.48 ($false != ((f4 @ $true))) | (~spl23_5 | spl23_10)),
% 1.14/0.48 inference(forward_demodulation,[],[f144,f123])).
% 1.14/0.48 thf(f1656,plain,(
% 1.14/0.48 ($false != ((f4 @ $true))) | (~spl23_9 | spl23_14)),
% 1.14/0.48 inference(forward_demodulation,[],[f162,f141])).
% 1.14/0.48 thf(f1660,plain,(
% 1.14/0.48 ($true = ((f4 @ $true))) | (~spl23_13 | ~spl23_20)),
% 1.14/0.48 inference(forward_demodulation,[],[f190,f159])).
% 1.14/0.48 thf(f1665,plain,(
% 1.14/0.48 ($true != ((f4 @ $true))) | (~spl23_55 | spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f379,f349])).
% 1.14/0.48 thf(f1675,plain,(
% 1.14/0.48 $false | (~spl23_5 | spl23_10 | ~spl23_55 | ~spl23_60)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1653,f1338])).
% 1.14/0.48 thf(f1676,plain,(
% 1.14/0.48 ~spl23_5 | spl23_10 | ~spl23_55 | ~spl23_60),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1675])).
% 1.14/0.48 thf(f1679,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_12 | ~spl23_55 | spl23_62)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1665,f551])).
% 1.14/0.48 thf(f1680,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_12 | ~spl23_55 | spl23_62),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1679])).
% 1.14/0.48 thf(f1683,plain,(
% 1.14/0.48 ($false = ((f5 @ $false))) | (~spl23_53 | ~spl23_56)),
% 1.14/0.48 inference(forward_demodulation,[],[f353,f340])).
% 1.14/0.48 thf(f1696,plain,(
% 1.14/0.48 $false | (spl23_6 | ~spl23_53 | ~spl23_56 | ~spl23_93)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1683,f1328])).
% 1.14/0.48 thf(f1697,plain,(
% 1.14/0.48 spl23_6 | ~spl23_53 | ~spl23_56 | ~spl23_93),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1696])).
% 1.14/0.48 thf(f1706,plain,(
% 1.14/0.48 ($true != ((f5 @ $true))) | (~spl23_51 | spl23_58)),
% 1.14/0.48 inference(forward_demodulation,[],[f361,f331])).
% 1.14/0.48 thf(f1709,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_51 | ~spl23_54 | spl23_58)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1706,f961])).
% 1.14/0.48 thf(f1710,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_51 | ~spl23_54 | spl23_58),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1709])).
% 1.14/0.48 thf(f1721,plain,(
% 1.14/0.48 ($false = ((f3 @ $true))) | (~spl23_59 | ~spl23_64)),
% 1.14/0.48 inference(forward_demodulation,[],[f389,f367])).
% 1.14/0.48 thf(f1729,plain,(
% 1.14/0.48 $false | (~spl23_17 | spl23_22 | ~spl23_59 | ~spl23_64)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1721,f949])).
% 1.14/0.48 thf(f1730,plain,(
% 1.14/0.48 ~spl23_17 | spl23_22 | ~spl23_59 | ~spl23_64),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1729])).
% 1.14/0.48 thf(f1733,plain,(
% 1.14/0.48 spl23_19 | spl23_17),
% 1.14/0.48 inference(avatar_split_clause,[],[f1583,f175,f184])).
% 1.14/0.48 thf(f1734,plain,(
% 1.14/0.48 ($false = ((f4 @ $true))) | (~spl23_13 | ~spl23_18)),
% 1.14/0.48 inference(forward_demodulation,[],[f181,f159])).
% 1.14/0.48 thf(f1778,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_5 | ~spl23_12 | ~spl23_13 | ~spl23_18)),
% 1.14/0.48 inference(constrained_superposition,[],[f1734,f551])).
% 1.14/0.48 thf(f1782,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_12 | ~spl23_13 | ~spl23_18)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1778])).
% 1.14/0.48 thf(f1783,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_12 | ~spl23_13 | ~spl23_18),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1782])).
% 1.14/0.48 thf(f1816,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_5 | ~spl23_10 | ~spl23_13 | ~spl23_20)),
% 1.14/0.48 inference(forward_demodulation,[],[f1660,f1307])).
% 1.14/0.48 thf(f1817,plain,(
% 1.14/0.48 $false | (~spl23_5 | ~spl23_10 | ~spl23_13 | ~spl23_20)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1816])).
% 1.14/0.48 thf(f1818,plain,(
% 1.14/0.48 ~spl23_5 | ~spl23_10 | ~spl23_13 | ~spl23_20),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1817])).
% 1.14/0.48 thf(f1838,plain,(
% 1.14/0.48 ($false = ((f3 @ $true))) | (~spl23_63 | ~spl23_68)),
% 1.14/0.48 inference(forward_demodulation,[],[f407,f385])).
% 1.14/0.48 thf(f1839,plain,(
% 1.14/0.48 ($true != ((f3 @ $true))) | (~spl23_63 | spl23_70)),
% 1.14/0.48 inference(forward_demodulation,[],[f415,f385])).
% 1.14/0.48 thf(f1847,plain,(
% 1.14/0.48 $false | (~spl23_17 | ~spl23_24 | ~spl23_63 | spl23_70)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1839,f950])).
% 1.14/0.48 thf(f1848,plain,(
% 1.14/0.48 ~spl23_17 | ~spl23_24 | ~spl23_63 | spl23_70),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1847])).
% 1.14/0.48 thf(f1850,plain,(
% 1.14/0.48 spl23_23 | spl23_21),
% 1.14/0.48 inference(avatar_split_clause,[],[f1247,f193,f202])).
% 1.14/0.48 thf(f1854,plain,(
% 1.14/0.48 spl23_31 | spl23_29),
% 1.14/0.48 inference(avatar_split_clause,[],[f1256,f229,f238])).
% 1.14/0.48 thf(f1869,plain,(
% 1.14/0.48 ($true != ((f4 @ $false))) | (~spl23_57 | spl23_62)),
% 1.14/0.48 inference(forward_demodulation,[],[f379,f358])).
% 1.14/0.48 thf(f1884,plain,(
% 1.14/0.48 ($false != ((f4 @ $false))) | (~spl23_7 | spl23_10)),
% 1.14/0.48 inference(forward_demodulation,[],[f144,f132])).
% 1.14/0.48 thf(f1888,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_12 | ~spl23_57 | spl23_62)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1869,f1066])).
% 1.14/0.48 thf(f1889,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_12 | ~spl23_57 | spl23_62),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1888])).
% 1.14/0.48 thf(f1893,plain,(
% 1.14/0.48 $false | (~spl23_7 | spl23_10 | ~spl23_57 | ~spl23_60)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1884,f672])).
% 1.14/0.48 thf(f1894,plain,(
% 1.14/0.48 ~spl23_7 | spl23_10 | ~spl23_57 | ~spl23_60),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1893])).
% 1.14/0.48 thf(f1895,plain,(
% 1.14/0.48 ($false = ((f4 @ $true))) | (~spl23_13 | ~spl23_18)),
% 1.14/0.48 inference(forward_demodulation,[],[f181,f159])).
% 1.14/0.48 thf(f1901,plain,(
% 1.14/0.48 ($false != ((f3 @ $false))) | (~spl23_19 | spl23_22)),
% 1.14/0.48 inference(forward_demodulation,[],[f198,f186])).
% 1.14/0.48 thf(f1928,plain,(
% 1.14/0.48 $false | (~spl23_59 | ~spl23_63 | spl23_64 | ~spl23_68)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1838,f1524])).
% 1.14/0.48 thf(f1929,plain,(
% 1.14/0.48 ~spl23_59 | ~spl23_63 | spl23_64 | ~spl23_68),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1928])).
% 1.14/0.48 thf(f1930,plain,(
% 1.14/0.48 $false | (~spl23_9 | ~spl23_13 | spl23_14 | ~spl23_18)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1895,f1656])).
% 1.14/0.48 thf(f1931,plain,(
% 1.14/0.48 ~spl23_9 | ~spl23_13 | spl23_14 | ~spl23_18),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1930])).
% 1.14/0.48 thf(f1934,plain,(
% 1.14/0.48 $false | (~spl23_19 | spl23_22 | ~spl23_69 | ~spl23_72)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1901,f702])).
% 1.14/0.48 thf(f1935,plain,(
% 1.14/0.48 ~spl23_19 | spl23_22 | ~spl23_69 | ~spl23_72),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1934])).
% 1.14/0.48 thf(f1976,plain,(
% 1.14/0.48 ($false != ((f4 @ $false))) | (~spl23_11 | spl23_14)),
% 1.14/0.48 inference(forward_demodulation,[],[f162,f150])).
% 1.14/0.48 thf(f1977,plain,(
% 1.14/0.48 ($true = ((f4 @ $false))) | (~spl23_11 | ~spl23_16)),
% 1.14/0.48 inference(forward_demodulation,[],[f172,f150])).
% 1.14/0.48 thf(f1984,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_10 | ~spl23_11 | spl23_14)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1976,f1461])).
% 1.14/0.48 thf(f1985,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_10 | ~spl23_11 | spl23_14),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1984])).
% 1.14/0.48 thf(f1986,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_7 | ~spl23_10 | ~spl23_11 | ~spl23_16)),
% 1.14/0.48 inference(forward_demodulation,[],[f1977,f1461])).
% 1.14/0.48 thf(f1987,plain,(
% 1.14/0.48 $false | (~spl23_7 | ~spl23_10 | ~spl23_11 | ~spl23_16)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f1986])).
% 1.14/0.48 thf(f1988,plain,(
% 1.14/0.48 ~spl23_7 | ~spl23_10 | ~spl23_11 | ~spl23_16),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f1987])).
% 1.14/0.48 thf(f1990,plain,(
% 1.14/0.48 spl23_15 | spl23_13),
% 1.14/0.48 inference(avatar_split_clause,[],[f1477,f157,f166])).
% 1.14/0.48 thf(f1998,plain,(
% 1.14/0.48 spl23_39 | spl23_37),
% 1.14/0.48 inference(avatar_split_clause,[],[f998,f265,f274])).
% 1.14/0.48 thf(f2019,plain,(
% 1.14/0.48 ($true != ((f2 @ $false))) | (~spl23_73 | spl23_78)),
% 1.14/0.48 inference(forward_demodulation,[],[f451,f430])).
% 1.14/0.48 thf(f2027,plain,(
% 1.14/0.48 $false | (~spl23_39 | ~spl23_42 | ~spl23_43 | spl23_46)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f1127,f631])).
% 1.14/0.48 thf(f2028,plain,(
% 1.14/0.48 ~spl23_39 | ~spl23_42 | ~spl23_43 | spl23_46),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2027])).
% 1.14/0.48 thf(f2029,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_39 | ~spl23_42 | ~spl23_43 | ~spl23_48)),
% 1.14/0.48 inference(forward_demodulation,[],[f1129,f631])).
% 1.14/0.48 thf(f2030,plain,(
% 1.14/0.48 $false | (~spl23_39 | ~spl23_42 | ~spl23_43 | ~spl23_48)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f2029])).
% 1.14/0.48 thf(f2031,plain,(
% 1.14/0.48 ~spl23_39 | ~spl23_42 | ~spl23_43 | ~spl23_48),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2030])).
% 1.14/0.48 thf(f2072,plain,(
% 1.14/0.48 ($true = ((f0 @ $true))) | (~spl23_41 | ~spl23_48)),
% 1.14/0.48 inference(forward_demodulation,[],[f316,f285])).
% 1.14/0.48 thf(f2076,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_41 | ~spl23_45 | ~spl23_48 | ~spl23_49)),
% 1.14/0.48 inference(forward_demodulation,[],[f2072,f523])).
% 1.14/0.48 thf(f2077,plain,(
% 1.14/0.48 $false | (~spl23_41 | ~spl23_45 | ~spl23_48 | ~spl23_49)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f2076])).
% 1.14/0.48 thf(f2078,plain,(
% 1.14/0.48 ~spl23_41 | ~spl23_45 | ~spl23_48 | ~spl23_49),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2077])).
% 1.14/0.48 thf(f2084,plain,(
% 1.14/0.48 ($true = ((f0 @ $true))) | (~spl23_45 | ~spl23_50)),
% 1.14/0.48 inference(forward_demodulation,[],[f326,f303])).
% 1.14/0.48 thf(f2096,plain,(
% 1.14/0.48 ($false = ((f0 @ $true))) | (~spl23_87 | ~spl23_91)),
% 1.14/0.48 inference(forward_demodulation,[],[f511,f493])).
% 1.14/0.48 thf(f2097,plain,(
% 1.14/0.48 ($true != ((f0 @ $true))) | (~spl23_87 | spl23_92)),
% 1.14/0.48 inference(forward_demodulation,[],[f515,f493])).
% 1.14/0.48 thf(f2102,plain,(
% 1.14/0.48 $false | (~spl23_37 | spl23_42 | ~spl23_87 | ~spl23_91)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f2096,f772])).
% 1.14/0.48 thf(f2103,plain,(
% 1.14/0.48 ~spl23_37 | spl23_42 | ~spl23_87 | ~spl23_91),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2102])).
% 1.14/0.48 thf(f2104,plain,(
% 1.14/0.48 $false | (~spl23_37 | ~spl23_44 | ~spl23_87 | spl23_92)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f2097,f776])).
% 1.14/0.48 thf(f2105,plain,(
% 1.14/0.48 ~spl23_37 | ~spl23_44 | ~spl23_87 | spl23_92),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2104])).
% 1.14/0.48 thf(f2115,plain,(
% 1.14/0.48 ($true = $false) | (~spl23_37 | ~spl23_42 | ~spl23_45 | ~spl23_50)),
% 1.14/0.48 inference(forward_demodulation,[],[f2084,f1095])).
% 1.14/0.48 thf(f2116,plain,(
% 1.14/0.48 $false | (~spl23_37 | ~spl23_42 | ~spl23_45 | ~spl23_50)),
% 1.14/0.48 inference(trivial_inequality_removal,[],[f2115])).
% 1.14/0.48 thf(f2117,plain,(
% 1.14/0.48 ~spl23_37 | ~spl23_42 | ~spl23_45 | ~spl23_50),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2116])).
% 1.14/0.48 thf(f2125,plain,(
% 1.14/0.48 ($false != ((f2 @ $false))) | (~spl23_23 | spl23_26)),
% 1.14/0.48 inference(forward_demodulation,[],[f216,f204])).
% 1.14/0.48 thf(f2128,plain,(
% 1.14/0.48 ($false != ((f2 @ $false))) | (~spl23_31 | spl23_34)),
% 1.14/0.48 inference(forward_demodulation,[],[f252,f240])).
% 1.14/0.48 thf(f2134,plain,(
% 1.14/0.48 ($true != ((f1 @ $true))) | (~spl23_33 | spl23_40)),
% 1.14/0.48 inference(forward_demodulation,[],[f279,f249])).
% 1.14/0.48 thf(f2135,plain,(
% 1.14/0.48 spl23_47 | spl23_45),
% 1.14/0.48 inference(avatar_split_clause,[],[f1005,f301,f310])).
% 1.14/0.48 thf(f2146,plain,(
% 1.14/0.48 ($false = ((f2 @ $true))) | (~spl23_25 | ~spl23_30)),
% 1.14/0.48 inference(forward_demodulation,[],[f235,f213])).
% 1.14/0.48 thf(f2148,plain,(
% 1.14/0.48 $false | (~spl23_23 | ~spl23_28 | ~spl23_73 | spl23_78)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f2019,f908])).
% 1.14/0.48 thf(f2149,plain,(
% 1.14/0.48 ~spl23_23 | ~spl23_28 | ~spl23_73 | spl23_78),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2148])).
% 1.14/0.48 thf(f2150,plain,(
% 1.14/0.48 $false | (~spl23_23 | spl23_26 | ~spl23_73 | ~spl23_76)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f2125,f712])).
% 1.14/0.48 thf(f2151,plain,(
% 1.14/0.48 ~spl23_23 | spl23_26 | ~spl23_73 | ~spl23_76),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2150])).
% 1.14/0.48 thf(f2152,plain,(
% 1.14/0.48 $false | (~spl23_31 | spl23_34 | ~spl23_73 | ~spl23_76)),
% 1.14/0.48 inference(forward_subsumption_resolution,[],[f2128,f712])).
% 1.14/0.48 thf(f2153,plain,(
% 1.14/0.48 ~spl23_31 | spl23_34 | ~spl23_73 | ~spl23_76),
% 1.14/0.48 inference(avatar_contradiction_clause,[],[f2152])).
% 1.14/0.48 thf(f2186,plain,(
% 1.14/0.48 ($false = ((f2 @ $true))) | (~spl23_71 | ~spl23_76)),
% 1.14/0.48 inference(forward_demodulation,[],[f443,f421])).
% 1.14/0.48 thf(f2188,plain,(
% 1.14/0.48 ($false != ((f2 @ $true))) | (~spl23_29 | spl23_34)),
% 1.14/0.49 inference(forward_demodulation,[],[f252,f231])).
% 1.14/0.49 thf(f2190,plain,(
% 1.14/0.49 ($false != ((f2 @ $true))) | (~spl23_21 | spl23_26)),
% 1.14/0.49 inference(forward_demodulation,[],[f216,f195])).
% 1.14/0.49 thf(f2195,plain,(
% 1.14/0.49 $false | (~spl23_29 | spl23_34 | ~spl23_71 | ~spl23_76)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2188,f2186])).
% 1.14/0.49 thf(f2196,plain,(
% 1.14/0.49 ~spl23_29 | spl23_34 | ~spl23_71 | ~spl23_76),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2195])).
% 1.14/0.49 thf(f2197,plain,(
% 1.14/0.49 $false | (~spl23_21 | spl23_26 | ~spl23_71 | ~spl23_76)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2190,f2186])).
% 1.14/0.49 thf(f2198,plain,(
% 1.14/0.49 ~spl23_21 | spl23_26 | ~spl23_71 | ~spl23_76),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2197])).
% 1.14/0.49 thf(f2215,plain,(
% 1.14/0.49 ($true = ((f2 @ $true))) | (~spl23_71 | ~spl23_78)),
% 1.14/0.49 inference(forward_demodulation,[],[f452,f421])).
% 1.14/0.49 thf(f2220,plain,(
% 1.14/0.49 ($false != ((f1 @ $true))) | (~spl23_75 | spl23_80)),
% 1.14/0.49 inference(forward_demodulation,[],[f460,f439])).
% 1.14/0.49 thf(f2221,plain,(
% 1.14/0.49 ($true = ((f1 @ $true))) | (~spl23_75 | ~spl23_82)),
% 1.14/0.49 inference(forward_demodulation,[],[f470,f439])).
% 1.14/0.49 thf(f2222,plain,(
% 1.14/0.49 $false | (~spl23_21 | ~spl23_25 | spl23_26 | ~spl23_30)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2190,f2146])).
% 1.14/0.49 thf(f2223,plain,(
% 1.14/0.49 ~spl23_21 | ~spl23_25 | spl23_26 | ~spl23_30),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2222])).
% 1.14/0.49 thf(f2242,plain,(
% 1.14/0.49 $false | (~spl23_75 | ~spl23_79 | spl23_80 | ~spl23_84)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2220,f1150])).
% 1.14/0.49 thf(f2243,plain,(
% 1.14/0.49 ~spl23_75 | ~spl23_79 | spl23_80 | ~spl23_84),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2242])).
% 1.14/0.49 thf(f2244,plain,(
% 1.14/0.49 ($true = $false) | (~spl23_75 | ~spl23_79 | ~spl23_82 | ~spl23_84)),
% 1.14/0.49 inference(forward_demodulation,[],[f2221,f1150])).
% 1.14/0.49 thf(f2245,plain,(
% 1.14/0.49 $false | (~spl23_75 | ~spl23_79 | ~spl23_82 | ~spl23_84)),
% 1.14/0.49 inference(trivial_inequality_removal,[],[f2244])).
% 1.14/0.49 thf(f2246,plain,(
% 1.14/0.49 ~spl23_75 | ~spl23_79 | ~spl23_82 | ~spl23_84),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2245])).
% 1.14/0.49 thf(f2253,plain,(
% 1.14/0.49 ($true = ((f2 @ $true))) | (~spl23_25 | ~spl23_32)),
% 1.14/0.49 inference(forward_demodulation,[],[f244,f213])).
% 1.14/0.49 thf(f2261,plain,(
% 1.14/0.49 $false | (~spl23_33 | spl23_40 | ~spl23_83 | ~spl23_90)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2134,f913])).
% 1.14/0.49 thf(f2262,plain,(
% 1.14/0.49 ~spl23_33 | spl23_40 | ~spl23_83 | ~spl23_90),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2261])).
% 1.14/0.49 thf(f2293,plain,(
% 1.14/0.49 ($true = $false) | (~spl23_29 | ~spl23_34 | ~spl23_71 | ~spl23_78)),
% 1.14/0.49 inference(forward_demodulation,[],[f2215,f1072])).
% 1.14/0.49 thf(f2294,plain,(
% 1.14/0.49 $false | (~spl23_29 | ~spl23_34 | ~spl23_71 | ~spl23_78)),
% 1.14/0.49 inference(trivial_inequality_removal,[],[f2293])).
% 1.14/0.49 thf(f2295,plain,(
% 1.14/0.49 ~spl23_29 | ~spl23_34 | ~spl23_71 | ~spl23_78),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2294])).
% 1.14/0.49 thf(f2298,plain,(
% 1.14/0.49 ($true = $false) | (~spl23_25 | ~spl23_29 | ~spl23_32 | ~spl23_34)),
% 1.14/0.49 inference(forward_demodulation,[],[f2253,f1072])).
% 1.14/0.49 thf(f2299,plain,(
% 1.14/0.49 $false | (~spl23_25 | ~spl23_29 | ~spl23_32 | ~spl23_34)),
% 1.14/0.49 inference(trivial_inequality_removal,[],[f2298])).
% 1.14/0.49 thf(f2300,plain,(
% 1.14/0.49 ~spl23_25 | ~spl23_29 | ~spl23_32 | ~spl23_34),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2299])).
% 1.14/0.49 thf(f2318,plain,(
% 1.14/0.49 spl23_81 | spl23_79),
% 1.14/0.49 inference(avatar_split_clause,[],[f1271,f455,f464])).
% 1.14/0.49 thf(f2319,plain,(
% 1.14/0.49 ($false = ((f1 @ $true))) | (~spl23_75 | ~spl23_80)),
% 1.14/0.49 inference(forward_demodulation,[],[f461,f439])).
% 1.14/0.49 thf(f2326,plain,(
% 1.14/0.49 ($false = ((f1 @ $true))) | (~spl23_83 | ~spl23_88)),
% 1.14/0.49 inference(forward_demodulation,[],[f497,f475])).
% 1.14/0.49 thf(f2342,plain,(
% 1.14/0.49 $false | (~spl23_33 | spl23_38 | ~spl23_75 | ~spl23_80)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2319,f1160])).
% 1.14/0.49 thf(f2343,plain,(
% 1.14/0.49 ~spl23_33 | spl23_38 | ~spl23_75 | ~spl23_80),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2342])).
% 1.14/0.49 thf(f2346,plain,(
% 1.14/0.49 $false | (~spl23_33 | spl23_38 | ~spl23_83 | ~spl23_88)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2326,f1160])).
% 1.14/0.49 thf(f2347,plain,(
% 1.14/0.49 ~spl23_33 | spl23_38 | ~spl23_83 | ~spl23_88),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2346])).
% 1.14/0.49 thf(f2412,plain,(
% 1.14/0.49 ($false != ((f2 @ $false))) | (~spl23_73 | spl23_76)),
% 1.14/0.49 inference(forward_demodulation,[],[f442,f430])).
% 1.14/0.49 thf(f2431,plain,(
% 1.14/0.49 $false | (~spl23_31 | ~spl23_34 | ~spl23_73 | spl23_76)),
% 1.14/0.49 inference(forward_subsumption_resolution,[],[f2412,f611])).
% 1.14/0.49 thf(f2432,plain,(
% 1.14/0.49 ~spl23_31 | ~spl23_34 | ~spl23_73 | spl23_76),
% 1.14/0.49 inference(avatar_contradiction_clause,[],[f2431])).
% 1.14/0.49 cnf(s1, plain, spl23_1 | spl23_2, inference(sat_conversion,[],[f110])).
% 1.14/0.49 cnf(s2, plain, spl23_3 | spl23_4, inference(sat_conversion,[],[f119])).
% 1.14/0.49 cnf(s3, plain, spl23_5 | spl23_6, inference(sat_conversion,[],[f128])).
% 1.14/0.49 cnf(s4, plain, spl23_7 | spl23_8, inference(sat_conversion,[],[f137])).
% 1.14/0.49 cnf(s5, plain, spl23_9 | spl23_10, inference(sat_conversion,[],[f146])).
% 1.14/0.49 cnf(s6, plain, spl23_11 | spl23_12, inference(sat_conversion,[],[f155])).
% 1.14/0.49 cnf(s7, plain, spl23_13 | spl23_14, inference(sat_conversion,[],[f164])).
% 1.14/0.49 cnf(s8, plain, spl23_15 | spl23_16, inference(sat_conversion,[],[f173])).
% 1.14/0.49 cnf(s9, plain, spl23_17 | spl23_18, inference(sat_conversion,[],[f182])).
% 1.14/0.49 cnf(s10, plain, spl23_19 | spl23_20, inference(sat_conversion,[],[f191])).
% 1.14/0.49 cnf(s11, plain, spl23_21 | spl23_22, inference(sat_conversion,[],[f200])).
% 1.14/0.49 cnf(s12, plain, spl23_23 | spl23_24, inference(sat_conversion,[],[f209])).
% 1.14/0.49 cnf(s13, plain, spl23_25 | spl23_26, inference(sat_conversion,[],[f218])).
% 1.14/0.49 cnf(s14, plain, spl23_27 | spl23_28, inference(sat_conversion,[],[f227])).
% 1.14/0.49 cnf(s15, plain, spl23_29 | spl23_30, inference(sat_conversion,[],[f236])).
% 1.14/0.49 cnf(s16, plain, spl23_31 | spl23_32, inference(sat_conversion,[],[f245])).
% 1.14/0.49 cnf(s17, plain, spl23_33 | spl23_34, inference(sat_conversion,[],[f254])).
% 1.14/0.49 cnf(s18, plain, spl23_35 | spl23_36, inference(sat_conversion,[],[f263])).
% 1.14/0.49 cnf(s19, plain, spl23_37 | spl23_38, inference(sat_conversion,[],[f272])).
% 1.14/0.49 cnf(s20, plain, spl23_39 | spl23_40, inference(sat_conversion,[],[f281])).
% 1.14/0.49 cnf(s21, plain, spl23_41 | spl23_42, inference(sat_conversion,[],[f290])).
% 1.14/0.49 cnf(s22, plain, spl23_43 | spl23_44, inference(sat_conversion,[],[f299])).
% 1.14/0.49 cnf(s23, plain, spl23_45 | spl23_46, inference(sat_conversion,[],[f308])).
% 1.14/0.49 cnf(s24, plain, spl23_47 | spl23_48, inference(sat_conversion,[],[f317])).
% 1.14/0.49 cnf(s25, plain, spl23_4 | spl23_49, inference(sat_conversion,[],[f322])).
% 1.14/0.49 cnf(s26, plain, spl23_2 | spl23_50, inference(sat_conversion,[],[f327])).
% 1.14/0.49 cnf(s27, plain, spl23_51 | spl23_52, inference(sat_conversion,[],[f336])).
% 1.14/0.49 cnf(s28, plain, spl23_53 | spl23_54, inference(sat_conversion,[],[f345])).
% 1.14/0.49 cnf(s29, plain, spl23_55 | spl23_56, inference(sat_conversion,[],[f354])).
% 1.14/0.49 cnf(s30, plain, spl23_57 | spl23_58, inference(sat_conversion,[],[f363])).
% 1.14/0.49 cnf(s31, plain, spl23_59 | spl23_60, inference(sat_conversion,[],[f372])).
% 1.14/0.49 cnf(s32, plain, spl23_61 | spl23_62, inference(sat_conversion,[],[f381])).
% 1.14/0.49 cnf(s33, plain, spl23_63 | spl23_64, inference(sat_conversion,[],[f390])).
% 1.14/0.49 cnf(s34, plain, spl23_65 | spl23_66, inference(sat_conversion,[],[f399])).
% 1.14/0.49 cnf(s35, plain, spl23_67 | spl23_68, inference(sat_conversion,[],[f408])).
% 1.14/0.49 cnf(s36, plain, spl23_69 | spl23_70, inference(sat_conversion,[],[f417])).
% 1.14/0.49 cnf(s37, plain, spl23_71 | spl23_72, inference(sat_conversion,[],[f426])).
% 1.14/0.49 cnf(s38, plain, spl23_73 | spl23_74, inference(sat_conversion,[],[f435])).
% 1.14/0.49 cnf(s39, plain, spl23_75 | spl23_76, inference(sat_conversion,[],[f444])).
% 1.14/0.49 cnf(s40, plain, spl23_77 | spl23_78, inference(sat_conversion,[],[f453])).
% 1.14/0.49 cnf(s41, plain, spl23_79 | spl23_80, inference(sat_conversion,[],[f462])).
% 1.14/0.49 cnf(s42, plain, spl23_81 | spl23_82, inference(sat_conversion,[],[f471])).
% 1.14/0.49 cnf(s43, plain, spl23_83 | spl23_84, inference(sat_conversion,[],[f480])).
% 1.14/0.49 cnf(s44, plain, spl23_85 | spl23_86, inference(sat_conversion,[],[f489])).
% 1.14/0.49 cnf(s45, plain, spl23_87 | spl23_88, inference(sat_conversion,[],[f498])).
% 1.14/0.49 cnf(s46, plain, spl23_89 | spl23_90, inference(sat_conversion,[],[f507])).
% 1.14/0.49 cnf(s47, plain, spl23_3 | spl23_91, inference(sat_conversion,[],[f512])).
% 1.14/0.49 cnf(s48, plain, spl23_1 | spl23_92, inference(sat_conversion,[],[f517])).
% 1.14/0.49 cnf(s49, plain, ~spl23_2 | ~spl23_4, inference(sat_conversion,[],[f520])).
% 1.14/0.49 cnf(s51, plain, ~spl23_5 | ~spl23_7, inference(sat_conversion,[],[f539])).
% 1.14/0.49 cnf(s53, plain, ~spl23_9 | ~spl23_11, inference(sat_conversion,[],[f548])).
% 1.14/0.49 cnf(s57, plain, ~spl23_17 | ~spl23_19, inference(sat_conversion,[],[f568])).
% 1.14/0.49 cnf(s59, plain, ~spl23_21 | ~spl23_23, inference(sat_conversion,[],[f578])).
% 1.14/0.49 cnf(s65, plain, ~spl23_33 | ~spl23_35, inference(sat_conversion,[],[f608])).
% 1.14/0.49 cnf(s67, plain, ~spl23_37 | ~spl23_39, inference(sat_conversion,[],[f618])).
% 1.14/0.49 cnf(s73, plain, ~spl23_51 | ~spl23_53, inference(sat_conversion,[],[f649])).
% 1.14/0.49 cnf(s92, plain, ~spl23_39 | ~spl23_42 | ~spl23_89 | ~spl23_92, inference(sat_conversion,[],[f746])).
% 1.14/0.49 cnf(s95, plain, ~spl23_42 | ~spl23_44, inference(sat_conversion,[],[f757])).
% 1.14/0.49 cnf(s96, plain, ~spl23_47 | ~spl23_49 | ~spl23_89 | ~spl23_92, inference(sat_conversion,[],[f760])).
% 1.14/0.49 cnf(s97, plain, ~spl23_38 | ~spl23_40, inference(sat_conversion,[],[f763])).
% 1.14/0.49 cnf(s98, plain, ~spl23_23 | ~spl23_26 | ~spl23_31 | ~spl23_36, inference(sat_conversion,[],[f766])).
% 1.14/0.49 cnf(s102, plain, ~spl23_35 | ~spl23_40 | ~spl23_77 | ~spl23_80, inference(sat_conversion,[],[f783])).
% 1.14/0.49 cnf(s103, plain, ~spl23_37 | spl23_42 | ~spl23_45 | ~spl23_49, inference(sat_conversion,[],[f785])).
% 1.14/0.49 cnf(s107, plain, ~spl23_23 | ~spl23_26 | ~spl23_73 | ~spl23_78, inference(sat_conversion,[],[f799])).
% 1.14/0.49 cnf(s111, plain, ~spl23_35 | ~spl23_40 | ~spl23_85 | ~spl23_88, inference(sat_conversion,[],[f814])).
% 1.14/0.49 cnf(s112, plain, ~spl23_76 | ~spl23_78, inference(sat_conversion,[],[f817])).
% 1.14/0.49 cnf(s115, plain, ~spl23_19 | ~spl23_22 | ~spl23_69 | ~spl23_74, inference(sat_conversion,[],[f824])).
% 1.14/0.49 cnf(s117, plain, ~spl23_84 | ~spl23_86, inference(sat_conversion,[],[f835])).
% 1.14/0.49 cnf(s118, plain, ~spl23_88 | ~spl23_90, inference(sat_conversion,[],[f838])).
% 1.14/0.49 cnf(s119, plain, ~spl23_35 | ~spl23_38 | ~spl23_77 | spl23_80, inference(sat_conversion,[],[f846])).
% 1.14/0.49 cnf(s120, plain, ~spl23_35 | ~spl23_38 | ~spl23_77 | ~spl23_82, inference(sat_conversion,[],[f849])).
% 1.14/0.49 cnf(s124, plain, ~spl23_41 | ~spl23_46 | ~spl23_87 | ~spl23_92, inference(sat_conversion,[],[f865])).
% 1.14/0.49 cnf(s126, plain, ~spl23_35 | ~spl23_38 | ~spl23_85 | ~spl23_90, inference(sat_conversion,[],[f873])).
% 1.14/0.49 cnf(s128, plain, ~spl23_1 | ~spl23_3, inference(sat_conversion,[],[f883])).
% 1.14/0.49 cnf(s129, plain, ~spl23_39 | spl23_42 | ~spl23_89 | ~spl23_91, inference(sat_conversion,[],[f888])).
% 1.14/0.49 cnf(s131, plain, ~spl23_81 | ~spl23_84 | ~spl23_85 | spl23_88, inference(sat_conversion,[],[f899])).
% 1.14/0.49 cnf(s134, plain, ~spl23_23 | ~spl23_26 | ~spl23_27 | ~spl23_32, inference(sat_conversion,[],[f906])).
% 1.14/0.49 cnf(s138, plain, ~spl23_77 | ~spl23_80 | ~spl23_81 | ~spl23_86, inference(sat_conversion,[],[f925])).
% 1.14/0.49 cnf(s141, plain, ~spl23_22 | ~spl23_24, inference(sat_conversion,[],[f944])).
% 1.14/0.49 cnf(s142, plain, ~spl23_15 | ~spl23_18 | ~spl23_20, inference(sat_conversion,[],[f947])).
% 1.14/0.49 cnf(s143, plain, ~spl23_15 | ~spl23_20 | ~spl23_57 | ~spl23_60, inference(sat_conversion,[],[f953])).
% 1.14/0.49 cnf(s146, plain, ~spl23_56 | ~spl23_58, inference(sat_conversion,[],[f964])).
% 1.14/0.49 cnf(s148, plain, ~spl23_52 | ~spl23_54, inference(sat_conversion,[],[f970])).
% 1.14/0.49 cnf(s152, plain, ~spl23_6 | spl23_93 | spl23_94, inference(sat_conversion,[],[f1035])).
% 1.14/0.49 cnf(s153, plain, ~spl23_5 | ~spl23_9 | ~spl23_12 | ~spl23_14, inference(sat_conversion,[],[f1038])).
% 1.14/0.49 cnf(s154, plain, spl23_5 | spl23_7, inference(sat_conversion,[],[f1041])).
% 1.14/0.49 cnf(s156, plain, ~spl23_6 | ~spl23_8, inference(sat_conversion,[],[f1060])).
% 1.14/0.49 cnf(s159, plain, ~spl23_34 | ~spl23_36, inference(sat_conversion,[],[f1082])).
% 1.14/0.49 cnf(s161, plain, ~spl23_21 | ~spl23_26 | spl23_31 | ~spl23_36, inference(sat_conversion,[],[f1089])).
% 1.14/0.49 cnf(s162, plain, spl23_33 | spl23_35, inference(sat_conversion,[],[f1090])).
% 1.14/0.49 cnf(s164, plain, ~spl23_43 | ~spl23_46 | ~spl23_47 | ~spl23_50, inference(sat_conversion,[],[f1103])).
% 1.14/0.49 cnf(s166, plain, ~spl23_87 | ~spl23_91 | ~spl23_92, inference(sat_conversion,[],[f1116])).
% 1.14/0.49 cnf(s169, plain, ~spl23_37 | ~spl23_42 | ~spl23_87 | spl23_91, inference(sat_conversion,[],[f1126])).
% 1.14/0.49 cnf(s170, plain, ~spl23_79 | ~spl23_83 | ~spl23_86 | spl23_90, inference(sat_conversion,[],[f1139])).
% 1.14/0.49 cnf(s176, plain, ~spl23_27 | ~spl23_30 | ~spl23_31 | ~spl23_36, inference(sat_conversion,[],[f1167])).
% 1.14/0.49 cnf(s181, plain, ~spl23_26 | ~spl23_28, inference(sat_conversion,[],[f1180])).
% 1.14/0.49 cnf(s185, plain, ~spl23_21 | ~spl23_26 | ~spl23_71 | ~spl23_78, inference(sat_conversion,[],[f1220])).
% 1.14/0.49 cnf(s190, plain, ~spl23_6 | ~spl23_7 | spl23_52 | ~spl23_93, inference(sat_conversion,[],[f1288])).
% 1.14/0.49 cnf(s191, plain, ~spl23_51 | spl23_56 | ~spl23_94, inference(sat_conversion,[],[f1297])).
% 1.14/0.49 cnf(s193, plain, ~spl23_7 | ~spl23_53 | spl23_54 | ~spl23_58, inference(sat_conversion,[],[f1304])).
% 1.14/0.49 cnf(s194, plain, ~spl23_5 | ~spl23_52 | spl23_94, inference(sat_conversion,[],[f1305])).
% 1.14/0.49 cnf(s196, plain, spl23_6 | spl23_93 | ~spl23_94, inference(sat_conversion,[],[f1326])).
% 1.14/0.49 cnf(s200, plain, ~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20, inference(sat_conversion,[],[f1383])).
% 1.14/0.49 cnf(s201, plain, ~spl23_11 | ~spl23_14 | ~spl23_15 | ~spl23_20, inference(sat_conversion,[],[f1385])).
% 1.14/0.49 cnf(s202, plain, ~spl23_19 | ~spl23_22 | ~spl23_61 | ~spl23_66, inference(sat_conversion,[],[f1392])).
% 1.14/0.49 cnf(s205, plain, ~spl23_60 | ~spl23_62, inference(sat_conversion,[],[f1405])).
% 1.14/0.49 cnf(s206, plain, ~spl23_68 | ~spl23_70, inference(sat_conversion,[],[f1408])).
% 1.14/0.49 cnf(s207, plain, ~spl23_64 | ~spl23_66, inference(sat_conversion,[],[f1411])).
% 1.14/0.49 cnf(s208, plain, ~spl23_19 | ~spl23_22 | ~spl23_65 | spl23_68, inference(sat_conversion,[],[f1417])).
% 1.14/0.49 cnf(s209, plain, ~spl23_19 | ~spl23_22 | ~spl23_65 | ~spl23_70, inference(sat_conversion,[],[f1420])).
% 1.14/0.49 cnf(s211, plain, ~spl23_61 | ~spl23_64 | ~spl23_65 | ~spl23_70, inference(sat_conversion,[],[f1427])).
% 1.14/0.49 cnf(s215, plain, ~spl23_14 | ~spl23_16, inference(sat_conversion,[],[f1442])).
% 1.14/0.49 cnf(s218, plain, ~spl23_5 | ~spl23_10 | ~spl23_55 | ~spl23_62, inference(sat_conversion,[],[f1450])).
% 1.14/0.49 cnf(s221, plain, ~spl23_17 | spl23_24 | ~spl23_67 | ~spl23_74, inference(sat_conversion,[],[f1512])).
% 1.14/0.49 cnf(s222, plain, ~spl23_17 | spl23_24 | spl23_69 | ~spl23_74, inference(sat_conversion,[],[f1515])).
% 1.14/0.49 cnf(s223, plain, ~spl23_65 | ~spl23_68 | ~spl23_69 | ~spl23_74, inference(sat_conversion,[],[f1519])).
% 1.14/0.49 cnf(s226, plain, ~spl23_17 | spl23_24 | ~spl23_59 | ~spl23_66, inference(sat_conversion,[],[f1533])).
% 1.14/0.49 cnf(s228, plain, ~spl23_7 | ~spl23_12 | ~spl23_15 | spl23_20, inference(sat_conversion,[],[f1544])).
% 1.14/0.49 cnf(s229, plain, spl23_9 | spl23_11, inference(sat_conversion,[],[f1546])).
% 1.14/0.49 cnf(s231, plain, ~spl23_7 | ~spl23_10 | ~spl23_57 | ~spl23_62, inference(sat_conversion,[],[f1552])).
% 1.14/0.49 cnf(s236, plain, ~spl23_63 | ~spl23_67 | spl23_68 | ~spl23_72, inference(sat_conversion,[],[f1627])).
% 1.14/0.49 cnf(s237, plain, ~spl23_63 | ~spl23_67 | ~spl23_70 | ~spl23_72, inference(sat_conversion,[],[f1630])).
% 1.14/0.49 cnf(s238, plain, spl23_63 | spl23_65, inference(sat_conversion,[],[f1632])).
% 1.14/0.49 cnf(s241, plain, ~spl23_19 | ~spl23_24 | ~spl23_61 | spl23_66, inference(sat_conversion,[],[f1644])).
% 1.14/0.49 cnf(s244, plain, ~spl23_5 | spl23_10 | ~spl23_55 | ~spl23_60, inference(sat_conversion,[],[f1676])).
% 1.14/0.49 cnf(s246, plain, ~spl23_5 | ~spl23_12 | ~spl23_55 | spl23_62, inference(sat_conversion,[],[f1680])).
% 1.14/0.49 cnf(s251, plain, spl23_6 | ~spl23_53 | ~spl23_56 | ~spl23_93, inference(sat_conversion,[],[f1697])).
% 1.14/0.49 cnf(s254, plain, ~spl23_5 | ~spl23_51 | ~spl23_54 | spl23_58, inference(sat_conversion,[],[f1710])).
% 1.14/0.49 cnf(s256, plain, ~spl23_17 | spl23_22 | ~spl23_59 | ~spl23_64, inference(sat_conversion,[],[f1730])).
% 1.14/0.49 cnf(s258, plain, spl23_17 | spl23_19, inference(sat_conversion,[],[f1733])).
% 1.14/0.49 cnf(s260, plain, ~spl23_5 | ~spl23_12 | ~spl23_13 | ~spl23_18, inference(sat_conversion,[],[f1783])).
% 1.14/0.49 cnf(s265, plain, ~spl23_5 | ~spl23_10 | ~spl23_13 | ~spl23_20, inference(sat_conversion,[],[f1818])).
% 1.14/0.49 cnf(s271, plain, ~spl23_17 | ~spl23_24 | ~spl23_63 | spl23_70, inference(sat_conversion,[],[f1848])).
% 1.14/0.49 cnf(s275, plain, spl23_21 | spl23_23, inference(sat_conversion,[],[f1850])).
% 1.14/0.49 cnf(s276, plain, spl23_29 | spl23_31, inference(sat_conversion,[],[f1854])).
% 1.14/0.49 cnf(s282, plain, ~spl23_7 | ~spl23_12 | ~spl23_57 | spl23_62, inference(sat_conversion,[],[f1889])).
% 1.14/0.49 cnf(s283, plain, ~spl23_7 | spl23_10 | ~spl23_57 | ~spl23_60, inference(sat_conversion,[],[f1894])).
% 1.14/0.49 cnf(s293, plain, ~spl23_59 | ~spl23_63 | spl23_64 | ~spl23_68, inference(sat_conversion,[],[f1929])).
% 1.14/0.49 cnf(s294, plain, ~spl23_9 | ~spl23_13 | spl23_14 | ~spl23_18, inference(sat_conversion,[],[f1931])).
% 1.14/0.49 cnf(s296, plain, ~spl23_19 | spl23_22 | ~spl23_69 | ~spl23_72, inference(sat_conversion,[],[f1935])).
% 1.14/0.49 cnf(s304, plain, ~spl23_7 | ~spl23_10 | ~spl23_11 | spl23_14, inference(sat_conversion,[],[f1985])).
% 1.14/0.49 cnf(s305, plain, ~spl23_7 | ~spl23_10 | ~spl23_11 | ~spl23_16, inference(sat_conversion,[],[f1988])).
% 1.14/0.49 cnf(s306, plain, spl23_13 | spl23_15, inference(sat_conversion,[],[f1990])).
% 1.14/0.49 cnf(s309, plain, spl23_37 | spl23_39, inference(sat_conversion,[],[f1998])).
% 1.14/0.49 cnf(s315, plain, ~spl23_39 | ~spl23_42 | ~spl23_43 | spl23_46, inference(sat_conversion,[],[f2028])).
% 1.14/0.49 cnf(s316, plain, ~spl23_39 | ~spl23_42 | ~spl23_43 | ~spl23_48, inference(sat_conversion,[],[f2031])).
% 1.14/0.49 cnf(s321, plain, ~spl23_41 | ~spl23_45 | ~spl23_48 | ~spl23_49, inference(sat_conversion,[],[f2078])).
% 1.14/0.49 cnf(s324, plain, ~spl23_37 | spl23_42 | ~spl23_87 | ~spl23_91, inference(sat_conversion,[],[f2103])).
% 1.14/0.49 cnf(s325, plain, ~spl23_37 | ~spl23_44 | ~spl23_87 | spl23_92, inference(sat_conversion,[],[f2105])).
% 1.14/0.49 cnf(s328, plain, ~spl23_37 | ~spl23_42 | ~spl23_45 | ~spl23_50, inference(sat_conversion,[],[f2117])).
% 1.14/0.49 cnf(s331, plain, spl23_45 | spl23_47, inference(sat_conversion,[],[f2135])).
% 1.14/0.49 cnf(s332, plain, ~spl23_23 | ~spl23_28 | ~spl23_73 | spl23_78, inference(sat_conversion,[],[f2149])).
% 1.14/0.49 cnf(s333, plain, ~spl23_23 | spl23_26 | ~spl23_73 | ~spl23_76, inference(sat_conversion,[],[f2151])).
% 1.14/0.49 cnf(s334, plain, ~spl23_31 | spl23_34 | ~spl23_73 | ~spl23_76, inference(sat_conversion,[],[f2153])).
% 1.14/0.49 cnf(s336, plain, ~spl23_29 | spl23_34 | ~spl23_71 | ~spl23_76, inference(sat_conversion,[],[f2196])).
% 1.14/0.49 cnf(s337, plain, ~spl23_21 | spl23_26 | ~spl23_71 | ~spl23_76, inference(sat_conversion,[],[f2198])).
% 1.14/0.49 cnf(s341, plain, ~spl23_21 | ~spl23_25 | spl23_26 | ~spl23_30, inference(sat_conversion,[],[f2223])).
% 1.14/0.49 cnf(s345, plain, ~spl23_75 | ~spl23_79 | spl23_80 | ~spl23_84, inference(sat_conversion,[],[f2243])).
% 1.14/0.49 cnf(s346, plain, ~spl23_75 | ~spl23_79 | ~spl23_82 | ~spl23_84, inference(sat_conversion,[],[f2246])).
% 1.14/0.49 cnf(s348, plain, ~spl23_33 | spl23_40 | ~spl23_83 | ~spl23_90, inference(sat_conversion,[],[f2262])).
% 1.14/0.49 cnf(s358, plain, ~spl23_29 | ~spl23_34 | ~spl23_71 | ~spl23_78, inference(sat_conversion,[],[f2295])).
% 1.14/0.49 cnf(s360, plain, ~spl23_25 | ~spl23_29 | ~spl23_32 | ~spl23_34, inference(sat_conversion,[],[f2300])).
% 1.14/0.49 cnf(s361, plain, spl23_79 | spl23_81, inference(sat_conversion,[],[f2318])).
% 1.14/0.49 cnf(s368, plain, ~spl23_33 | spl23_38 | ~spl23_75 | ~spl23_80, inference(sat_conversion,[],[f2343])).
% 1.14/0.49 cnf(s370, plain, ~spl23_33 | spl23_38 | ~spl23_83 | ~spl23_88, inference(sat_conversion,[],[f2347])).
% 1.14/0.49 cnf(s395, plain, ~spl23_31 | ~spl23_34 | ~spl23_73 | spl23_76, inference(sat_conversion,[],[f2432])).
% 1.14/0.49 cnf(s397, plain, ~spl23_77 | ~spl23_86 | ~spl23_38 | ~spl23_35, inference(rat,[],[s138,s42,s119,s120])).
% 1.14/0.49 cnf(s398, plain, spl23_54 | ~spl23_58 | ~spl23_7, inference(rat,[],[s193,s28])).
% 1.14/0.49 cnf(s399, plain, ~spl23_58 | spl23_5, inference(rat,[],[s152,s191,s190,s27,s148,s398,s146,s154,s3])).
% 1.14/0.49 cnf(s400, plain, spl23_37 | ~spl23_35 | ~spl23_77 | spl23_1, inference(rat,[],[s321,s21,s24,s331,s92,s96,s46,s126,s44,s397,s19,s309,s48,s25,s49,s1])).
% 1.14/0.49 cnf(s401, plain, ~spl23_87 | ~spl23_37 | spl23_1, inference(rat,[],[s23,s124,s103,s21,s169,s166,s48,s25,s49,s1])).
% 1.14/0.49 cnf(s402, plain, ~spl23_35 | ~spl23_77 | spl23_1, inference(rat,[],[s43,s170,s117,s44,s111,s118,s45,s401,s41,s102,s20,s67,s400])).
% 1.14/0.49 cnf(s403, plain, ~spl23_26 | ~spl23_73 | ~spl23_23 | spl23_1, inference(rat,[],[s402,s18,s98,s16,s134,s40,s14,s107,s181])).
% 1.14/0.49 cnf(s404, plain, ~spl23_34 | ~spl23_25 | spl23_76 | ~spl23_73, inference(rat,[],[s360,s16,s276,s395])).
% 1.14/0.49 cnf(s405, plain, ~spl23_90 | spl23_40 | ~spl23_33 | ~spl23_75, inference(rat,[],[s346,s42,s361,s131,s44,s117,s43,s348,s118])).
% 1.14/0.49 cnf(s406, plain, spl23_37 | ~spl23_33 | ~spl23_75 | spl23_1, inference(rat,[],[s321,s21,s24,s331,s92,s96,s46,s405,s97,s19,s309,s48,s25,s49,s1])).
% 1.14/0.49 cnf(s407, plain, ~spl23_33 | ~spl23_75 | spl23_1, inference(rat,[],[s345,s41,s43,s368,s370,s97,s45,s20,s401,s67,s406])).
% 1.14/0.49 cnf(s408, plain, ~spl23_73 | ~spl23_23 | spl23_1, inference(rat,[],[s407,s17,s404,s39,s13,s333,s403])).
% 1.14/0.49 cnf(s409, plain, ~spl23_23 | ~spl23_61 | ~spl23_19 | spl23_1, inference(rat,[],[s408,s38,s223,s36,s208,s209,s34,s202,s11,s59])).
% 1.14/0.49 cnf(s410, plain, spl23_33 | ~spl23_71 | ~spl23_21 | spl23_1, inference(rat,[],[s15,s341,s13,s358,s185,s40,s402,s17,s162])).
% 1.14/0.49 cnf(s411, plain, ~spl23_71 | ~spl23_21 | spl23_1, inference(rat,[],[s176,s14,s15,s161,s181,s336,s337,s159,s39,s18,s407,s65,s410])).
% 1.14/0.49 cnf(s412, plain, ~spl23_61 | ~spl23_19 | spl23_1, inference(rat,[],[s35,s237,s206,s36,s296,s37,s411,s33,s207,s141,s241,s12,s275,s409])).
% 1.14/0.49 cnf(s413, plain, spl23_9 | spl23_5 | spl23_1, inference(rat,[],[s412,s32,s231,s10,s201,s8,s304,s305,s5,s229,s154,s30,s399])).
% 1.14/0.49 cnf(s414, plain, ~spl23_15 | ~spl23_18 | ~spl23_12 | ~spl23_7, inference(rat,[],[s142,s228])).
% 1.14/0.49 cnf(s415, plain, ~spl23_18 | ~spl23_9 | ~spl23_7, inference(rat,[],[s215,s294,s8,s306,s414,s6,s53])).
% 1.14/0.49 cnf(s416, plain, ~spl23_23 | spl23_5 | spl23_1, inference(rat,[],[s223,s35,s34,s221,s222,s226,s141,s38,s11,s408,s59,s31,s205,s282,s6,s53,s30,s399,s9,s415,s413,s154])).
% 1.14/0.49 cnf(s417, plain, spl23_5 | spl23_1, inference(rat,[],[s236,s35,s293,s33,s256,s37,s141,s411,s12,s275,s416,s9,s415,s31,s205,s282,s6,s53,s413,s30,s399,s154])).
% 1.14/0.49 cnf(s418, plain, ~spl23_52 | ~spl23_56 | ~spl23_5, inference(rat,[],[s251,s28,s196,s148,s194,s156,s4,s51])).
% 1.14/0.49 cnf(s419, plain, ~spl23_56 | ~spl23_5, inference(rat,[],[s28,s254,s73,s27,s418,s146])).
% 1.14/0.49 cnf(s420, plain, ~spl23_19 | spl23_1, inference(rat,[],[s7,s260,s153,s6,s53,s5,s218,s32,s9,s412,s57,s29,s419,s417])).
% 1.14/0.49 cnf(s421, plain, ~spl23_60 | spl23_1, inference(rat,[],[s200,s7,s306,s6,s265,s246,s244,s205,s29,s419,s417,s10,s420])).
% 1.14/0.49 cnf(s422, plain, ~spl23_23 | spl23_1, inference(rat,[],[s223,s34,s35,s226,s221,s222,s141,s38,s11,s408,s59,s258,s420,s31,s421])).
% 1.14/0.49 cnf(s423, plain, spl23_1, inference(rat,[],[s236,s35,s293,s33,s256,s37,s141,s411,s12,s275,s422,s31,s421,s258,s420])).
% 1.14/0.49 cnf(s424, plain, ~spl23_3, inference(rat,[],[s128,s423])).
% 1.14/0.49 cnf(s425, plain, spl23_91, inference(rat,[],[s47,s424])).
% 1.14/0.49 cnf(s426, plain, spl23_4, inference(rat,[],[s2,s424])).
% 1.14/0.49 cnf(s427, plain, ~spl23_2, inference(rat,[],[s49,s426])).
% 1.14/0.49 cnf(s428, plain, spl23_50, inference(rat,[],[s26,s427])).
% 1.14/0.49 cnf(s429, plain, ~spl23_74 | ~spl23_65 | ~spl23_17 | spl23_24, inference(rat,[],[s35,s223,s221,s222])).
% 1.14/0.49 cnf(s430, plain, ~spl23_43 | ~spl23_42 | ~spl23_39, inference(rat,[],[s24,s316,s164,s315,s428])).
% 1.14/0.49 cnf(s431, plain, ~spl23_89 | ~spl23_39, inference(rat,[],[s430,s22,s95,s129,s425])).
% 1.14/0.49 cnf(s432, plain, spl23_37 | ~spl23_77 | ~spl23_35, inference(rat,[],[s431,s46,s126,s44,s397,s19,s309])).
% 1.14/0.49 cnf(s433, plain, ~spl23_87 | spl23_92 | ~spl23_37, inference(rat,[],[s164,s23,s331,s328,s22,s324,s325,s425,s428])).
% 1.14/0.49 cnf(s434, plain, ~spl23_87 | ~spl23_37, inference(rat,[],[s433,s166,s425])).
% 1.14/0.49 cnf(s435, plain, ~spl23_77 | ~spl23_35, inference(rat,[],[s43,s170,s117,s44,s111,s118,s45,s434,s41,s102,s20,s67,s432])).
% 1.14/0.49 cnf(s436, plain, spl23_33 | ~spl23_73 | ~spl23_23, inference(rat,[],[s13,s404,s107,s112,s40,s435,s17,s162])).
% 1.14/0.49 cnf(s437, plain, spl23_37 | ~spl23_75 | ~spl23_33, inference(rat,[],[s405,s46,s97,s431,s19,s309])).
% 1.14/0.49 cnf(s438, plain, ~spl23_75 | ~spl23_33, inference(rat,[],[s345,s41,s43,s368,s370,s97,s45,s20,s434,s67,s437])).
% 1.14/0.49 cnf(s439, plain, ~spl23_73 | ~spl23_23, inference(rat,[],[s134,s14,s16,s332,s334,s333,s112,s39,s438,s159,s18,s65,s436])).
% 1.14/0.49 cnf(s440, plain, spl23_17 | ~spl23_23 | spl23_5, inference(rat,[],[s202,s32,s34,s231,s209,s5,s36,s415,s115,s9,s258,s154,s30,s399,s11,s59,s38,s439])).
% 1.14/0.49 cnf(s441, plain, ~spl23_23 | spl23_5, inference(rat,[],[s305,s6,s8,s282,s143,s283,s205,s31,s226,s34,s10,s429,s57,s440,s38,s439,s141,s11,s59,s154,s30,s399])).
% 1.14/0.49 cnf(s442, plain, spl23_33 | ~spl23_71 | ~spl23_21, inference(rat,[],[s15,s341,s13,s358,s185,s40,s435,s17,s162])).
% 1.14/0.49 cnf(s443, plain, ~spl23_71 | ~spl23_21, inference(rat,[],[s176,s14,s15,s161,s181,s336,s337,s159,s39,s18,s438,s65,s442])).
% 1.14/0.49 cnf(s445, plain, spl23_17 | spl23_5, inference(rat,[],[s207,s33,s241,s237,s32,s35,s231,s206,s5,s36,s415,s296,s9,s258,s154,s30,s399,s141,s12,s37,s443,s275,s441])).
% 1.14/0.49 cnf(s446, plain, ~spl23_59 | spl23_5, inference(rat,[],[s35,s237,s271,s293,s33,s256,s141,s12,s37,s443,s275,s441,s445])).
% 1.14/0.49 cnf(s447, plain, spl23_5, inference(rat,[],[s305,s6,s8,s282,s143,s283,s205,s31,s446,s10,s57,s445,s30,s399,s154])).
% 1.14/0.49 cnf(s449, plain, ~spl23_56, inference(rat,[],[s419,s447])).
% 1.14/0.49 cnf(s451, plain, spl23_55, inference(rat,[],[s29,s449])).
% 1.14/0.49 cnf(s455, plain, spl23_17 | ~spl23_23, inference(rat,[],[s7,s260,s153,s6,s53,s5,s218,s32,s202,s34,s209,s36,s115,s9,s258,s11,s59,s38,s439,s447,s451])).
% 1.14/0.49 cnf(s456, plain, ~spl23_23, inference(rat,[],[s200,s7,s306,s6,s265,s246,s244,s205,s31,s226,s34,s10,s429,s57,s455,s141,s38,s11,s439,s59,s447,s451])).
% 1.14/0.49 cnf(s457, plain, spl23_21, inference(rat,[],[s275,s456])).
% 1.14/0.49 cnf(s458, plain, spl23_24, inference(rat,[],[s12,s456])).
% 1.14/0.49 cnf(s460, plain, ~spl23_71, inference(rat,[],[s443,s457])).
% 1.14/0.49 cnf(s461, plain, ~spl23_22, inference(rat,[],[s141,s458])).
% 1.14/0.49 cnf(s463, plain, spl23_72, inference(rat,[],[s37,s460])).
% 1.14/0.49 cnf(s464, plain, spl23_17, inference(rat,[],[s7,s260,s153,s6,s53,s5,s218,s32,s211,s33,s238,s237,s35,s206,s36,s296,s9,s258,s447,s451,s463,s461])).
% 1.14/0.49 cnf(s465, plain, ~spl23_19, inference(rat,[],[s57,s464])).
% 1.14/0.49 cnf(s466, plain, spl23_20, inference(rat,[],[s10,s465])).
% 1.14/0.49 cnf(s467, plain, spl23_64 | ~spl23_59 | ~spl23_63, inference(rat,[],[s35,s237,s271,s293,s458,s464,s463])).
% 1.14/0.49 cnf(s468, plain, ~spl23_59, inference(rat,[],[s467,s33,s256,s464,s461])).
% 1.14/0.49 cnf(s470, plain, spl23_60, inference(rat,[],[s31,s468])).
% 1.14/0.49 cnf(s471, plain, ~spl23_62, inference(rat,[],[s205,s470])).
% 1.14/0.49 cnf(s472, plain, spl23_10, inference(rat,[],[s244,s451,s447,s470])).
% 1.14/0.49 cnf(s473, plain, ~spl23_12, inference(rat,[],[s246,s451,s447,s471])).
% 1.14/0.49 cnf(s474, plain, ~spl23_13, inference(rat,[],[s265,s466,s447,s472])).
% 1.14/0.49 cnf(s475, plain, spl23_11, inference(rat,[],[s6,s473])).
% 1.14/0.49 cnf(s476, plain, spl23_15, inference(rat,[],[s306,s474])).
% 1.14/0.49 cnf(s477, plain, spl23_14, inference(rat,[],[s7,s474])).
% 1.14/0.49 cnf(s479, plain, $false, inference(rat,[],[s200,s477,s466,s475,s476])).
% 1.14/0.49 thf(f2435,plain,(
% 1.14/0.49 $false),
% 1.14/0.49 inference(avatar_sat_refutation,[],[s479])).
% 1.14/0.49 % SZS output end Proof for theBenchmark
% 1.14/0.49 % (1094406)------------------------------
% 1.14/0.49 % (1094406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.14/0.49 % (1094406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.14/0.49 % (1094406)CaDiCaL version: 2.1.3
% 1.14/0.49 % (1094406)Termination reason: Refutation
% 1.14/0.49 % (1094406)Time elapsed: 0.054 s
% 1.14/0.49 % (1094406)Peak memory usage: 13 MB
% 1.14/0.49 % (1094406)Instructions burned: 100 (million)
% 1.14/0.49 % (1094376)Success in time 0.238 s
% 1.14/0.49 % Vampire exiting
%------------------------------------------------------------------------------