%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500^1.007 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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.66s 0.48s
% Output : Refutation 1.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.007 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 % Computer : n018.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 17:13:26 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.66/0.48 % (364787)Will run a generic schedule for satisfiability detection.
% 1.66/0.48 % (364795)dis+10_1_sil=32000:sp=arity:random_seed=2269993531:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.66/0.48 % (364793)% WARNING: option uhcvi not known.
% 1.66/0.48 % (364792)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=809256430_2999 on theBenchmark for (2999ds/0Mi)
% 1.66/0.48 % (364793)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3576034338:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.66/0.48 % (364794)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1048830163:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.66/0.48 % Exception at run slice level
% 1.66/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.66/0.48 % (364796)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3241404834:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.66/0.48 % (364793)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.66/0.48 % (364793)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.66/0.48 % (364796)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.66/0.48 % (364797)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=670377095:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.66/0.48 % (364798)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=126645324:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.66/0.48 % (364804)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=716048675:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.66/0.48 % Exception at run slice level
% 1.66/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.66/0.48 % (364795)Instruction limit reached!
% 1.66/0.48 % (364795)------------------------------
% 1.66/0.48 % (364795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364795)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364795)Termination reason: Instruction limit
% 1.66/0.48 % (364795)Termination phase: Saturation
% 1.66/0.48 % (364795)Time elapsed: 0.028 s
% 1.66/0.48 % (364795)Peak memory usage: 12 MB
% 1.66/0.48 % (364795)Instructions burned: 105 (million)
% 1.66/0.48 % (364809)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=1405319405:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.66/0.48 % (364809)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.66/0.48 % (364809)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.66/0.48 % (364808)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4272194207:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.66/0.48 % (364796)Instruction limit reached!
% 1.66/0.48 % (364796)------------------------------
% 1.66/0.48 % (364796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364796)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364796)Termination reason: Instruction limit
% 1.66/0.48 % (364796)Termination phase: Saturation
% 1.66/0.48 % (364796)Time elapsed: 0.057 s
% 1.66/0.48 % (364796)Peak memory usage: 12 MB
% 1.66/0.48 % (364796)Instructions burned: 117 (million)
% 1.66/0.48 % (364797)Instruction limit reached!
% 1.66/0.48 % (364797)------------------------------
% 1.66/0.48 % (364797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364797)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364797)Termination reason: Instruction limit
% 1.66/0.48 % (364797)Termination phase: Saturation
% 1.66/0.48 % (364797)Time elapsed: 0.064 s
% 1.66/0.48 % (364797)Peak memory usage: 12 MB
% 1.66/0.48 % (364797)Instructions burned: 133 (million)
% 1.66/0.48 % (364812)ott-21_1_sil=16000:fs=off:random_seed=3884479205:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.66/0.48 % (364813)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3018471141:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.66/0.48 % (364808)Instruction limit reached!
% 1.66/0.48 % (364808)------------------------------
% 1.66/0.48 % (364808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364808)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364808)Termination reason: Instruction limit
% 1.66/0.48 % (364808)Termination phase: Saturation
% 1.66/0.48 % (364808)Time elapsed: 0.068 s
% 1.66/0.48 % (364808)Peak memory usage: 12 MB
% 1.66/0.48 % (364808)Instructions burned: 132 (million)
% 1.66/0.48 % (364816)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2254424159:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.66/0.48 % Exception at run slice level
% 1.66/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.66/0.48 % (364818)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1840543728:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.66/0.48 % (364812)Instruction limit reached!
% 1.66/0.48 % (364812)------------------------------
% 1.66/0.48 % (364812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364812)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364812)Termination reason: Instruction limit
% 1.66/0.48 % (364812)Termination phase: Saturation
% 1.66/0.48 % (364812)Time elapsed: 0.071 s
% 1.66/0.48 % (364812)Peak memory usage: 11 MB
% 1.66/0.48 % (364812)Instructions burned: 182 (million)
% 1.66/0.48 % (364798)Instruction limit reached!
% 1.66/0.48 % (364798)------------------------------
% 1.66/0.48 % (364798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364798)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364798)Termination reason: Instruction limit
% 1.66/0.48 % (364798)Termination phase: Saturation
% 1.66/0.48 % (364798)Time elapsed: 0.142 s
% 1.66/0.48 % (364798)Peak memory usage: 12 MB
% 1.66/0.48 % (364798)Instructions burned: 159 (million)
% 1.66/0.48 % (364820)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2094444202:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.66/0.48 % Exception at run slice level
% 1.66/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.66/0.48 % (364821)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=2661308291: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.66/0.48 % (364821)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.66/0.48 % (364823)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2890478577:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 1.66/0.48 % (364823)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.66/0.48 % (364818) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-364787-364818"...
% 1.66/0.48 % (364809)Instruction limit reached!
% 1.66/0.48 % (364809)------------------------------
% 1.66/0.48 % (364809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.48 % (364809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.48 % (364809)CaDiCaL version: 2.1.3
% 1.66/0.48 % (364809)Termination reason: Instruction limit
% 1.66/0.48 % (364809)Termination phase: Saturation
% 1.66/0.48 % (364809)Time elapsed: 0.175 s
% 1.66/0.48 % (364809)Peak memory usage: 14 MB
% 1.66/0.48 % (364809)Instructions burned: 684 (million)
% 1.66/0.48 % (364818)...printing done.
% 1.66/0.48 % (364818)Refutation found. Thanks to Tanya!
% 1.66/0.48 % SZS status Theorem for theBenchmark
% 1.66/0.48 % SZS output start Proof for theBenchmark
% 1.66/0.48 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.66/0.48 thf(func_def_0, type, x: $o).
% 1.66/0.48 thf(func_def_1, type, f0: ($o > $o)).
% 1.66/0.48 thf(func_def_2, type, f1: ($o > $o)).
% 1.66/0.48 thf(func_def_3, type, f2: ($o > $o)).
% 1.66/0.48 thf(func_def_4, type, f3: ($o > $o)).
% 1.66/0.48 thf(func_def_5, type, f4: ($o > $o)).
% 1.66/0.48 thf(func_def_6, type, f5: ($o > $o)).
% 1.66/0.48 thf(func_def_7, type, f6: ($o > $o)).
% 1.66/0.48 thf(func_def_11, type, sF0: $o).
% 1.66/0.48 thf(func_def_12, type, sF1: $o).
% 1.66/0.48 thf(func_def_13, type, sF2: $o).
% 1.66/0.48 thf(func_def_14, type, sF3: $o).
% 1.66/0.48 thf(func_def_15, type, sF4: $o).
% 1.66/0.48 thf(func_def_16, type, sF5: $o).
% 1.66/0.48 thf(func_def_17, type, sF6: $o).
% 1.66/0.48 thf(func_def_18, type, sF7: $o).
% 1.66/0.48 thf(func_def_19, type, sF8: $o).
% 1.66/0.48 thf(func_def_20, type, sF9: $o).
% 1.66/0.48 thf(func_def_21, type, sF10: $o).
% 1.66/0.48 thf(func_def_22, type, sF11: $o).
% 1.66/0.48 thf(func_def_23, type, sF12: $o).
% 1.66/0.48 thf(func_def_24, type, sF13: $o).
% 1.66/0.48 thf(func_def_25, type, sF14: $o).
% 1.66/0.48 thf(func_def_26, type, sF15: $o).
% 1.66/0.48 thf(func_def_27, type, sF16: $o).
% 1.66/0.48 thf(func_def_28, type, sF17: $o).
% 1.66/0.48 thf(func_def_29, type, sF18: $o).
% 1.66/0.48 thf(func_def_30, type, sF19: $o).
% 1.66/0.48 thf(func_def_31, type, sF20: $o).
% 1.66/0.48 thf(func_def_32, type, sF21: $o).
% 1.66/0.48 thf(func_def_33, type, sF22: $o).
% 1.66/0.48 thf(func_def_34, type, sF23: $o).
% 1.66/0.48 thf(func_def_35, type, sF24: $o).
% 1.66/0.48 thf(func_def_36, type, sF25: $o).
% 1.66/0.48 thf(func_def_37, type, sF26: $o).
% 1.66/0.48 thf(func_def_38, type, vNOT: ($o > $o)).
% 1.66/0.48 thf(f1,conjecture,(
% 1.66/0.48 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 1.66/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski7)).
% 1.66/0.48 thf(f2,negated_conjecture,(
% 1.66/0.48 ~ (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 1.66/0.48 inference(negated_conjecture,[status(cth)],[f1])).
% 1.66/0.48 thf(f3,plain,(
% 1.66/0.48 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 1.66/0.48 inference(flattening,[],[f2])).
% 1.66/0.48 thf(f4,plain,(
% 1.66/0.48 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 1.66/0.48 inference(cnf_transformation,[],[f3])).
% 1.66/0.48 thf(f6,definition,(
% 1.66/0.48 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.66/0.48 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.66/0.48 thf(f7,definition,(
% 1.66/0.48 (sF0 = ((f6 @ x)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 1.66/0.48 thf(f8,plain,(
% 1.66/0.48 (((f6 @ x)) = sF0)),
% 1.66/0.48 inference(reorient_equations,[],[f7])).
% 1.66/0.48 thf(f9,definition,(
% 1.66/0.48 (sF1 = ((f5 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 1.66/0.48 thf(f10,plain,(
% 1.66/0.48 (((f5 @ sF0)) = sF1)),
% 1.66/0.48 inference(reorient_equations,[],[f9])).
% 1.66/0.48 thf(f11,definition,(
% 1.66/0.48 (sF2 = ((f5 @ sF1)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 1.66/0.48 thf(f12,plain,(
% 1.66/0.48 (((f5 @ sF1)) = sF2)),
% 1.66/0.48 inference(reorient_equations,[],[f11])).
% 1.66/0.48 thf(f13,definition,(
% 1.66/0.48 (sF3 = ((f5 @ sF2)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 1.66/0.48 thf(f14,plain,(
% 1.66/0.48 (((f5 @ sF2)) = sF3)),
% 1.66/0.48 inference(reorient_equations,[],[f13])).
% 1.66/0.48 thf(f15,definition,(
% 1.66/0.48 (sF4 = ((f4 @ sF3)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 1.66/0.48 thf(f16,plain,(
% 1.66/0.48 (((f4 @ sF3)) = sF4)),
% 1.66/0.48 inference(reorient_equations,[],[f15])).
% 1.66/0.48 thf(f17,definition,(
% 1.66/0.48 (sF5 = ((f3 @ sF4)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 1.66/0.48 thf(f18,plain,(
% 1.66/0.48 (((f3 @ sF4)) = sF5)),
% 1.66/0.48 inference(reorient_equations,[],[f17])).
% 1.66/0.48 thf(f19,definition,(
% 1.66/0.48 (sF6 = ((f3 @ sF5)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 1.66/0.48 thf(f20,plain,(
% 1.66/0.48 (((f3 @ sF5)) = sF6)),
% 1.66/0.48 inference(reorient_equations,[],[f19])).
% 1.66/0.48 thf(f21,definition,(
% 1.66/0.48 (sF7 = ((f3 @ sF6)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 1.66/0.48 thf(f22,plain,(
% 1.66/0.48 (((f3 @ sF6)) = sF7)),
% 1.66/0.48 inference(reorient_equations,[],[f21])).
% 1.66/0.48 thf(f23,definition,(
% 1.66/0.48 (sF8 = ((f2 @ sF7)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 1.66/0.48 thf(f24,plain,(
% 1.66/0.48 (((f2 @ sF7)) = sF8)),
% 1.66/0.48 inference(reorient_equations,[],[f23])).
% 1.66/0.48 thf(f25,definition,(
% 1.66/0.48 (sF9 = ((f1 @ sF8)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 1.66/0.48 thf(f26,plain,(
% 1.66/0.48 (((f1 @ sF8)) = sF9)),
% 1.66/0.48 inference(reorient_equations,[],[f25])).
% 1.66/0.48 thf(f27,definition,(
% 1.66/0.48 (sF10 = ((f1 @ sF9)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 1.66/0.48 thf(f28,plain,(
% 1.66/0.48 (((f1 @ sF9)) = sF10)),
% 1.66/0.48 inference(reorient_equations,[],[f27])).
% 1.66/0.48 thf(f29,definition,(
% 1.66/0.48 (sF11 = ((f1 @ sF10)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 1.66/0.48 thf(f30,plain,(
% 1.66/0.48 (((f1 @ sF10)) = sF11)),
% 1.66/0.48 inference(reorient_equations,[],[f29])).
% 1.66/0.48 thf(f31,definition,(
% 1.66/0.48 (sF12 = ((f0 @ sF11)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 1.66/0.48 thf(f32,plain,(
% 1.66/0.48 (((f0 @ sF11)) = sF12)),
% 1.66/0.48 inference(reorient_equations,[],[f31])).
% 1.66/0.48 thf(f33,definition,(
% 1.66/0.48 (sF13 = ((f6 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 1.66/0.48 thf(f34,plain,(
% 1.66/0.48 (((f6 @ sF0)) = sF13)),
% 1.66/0.48 inference(reorient_equations,[],[f33])).
% 1.66/0.48 thf(f35,definition,(
% 1.66/0.48 (sF14 = ((f6 @ sF13)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 1.66/0.48 thf(f36,plain,(
% 1.66/0.48 (((f6 @ sF13)) = sF14)),
% 1.66/0.48 inference(reorient_equations,[],[f35])).
% 1.66/0.48 thf(f37,definition,(
% 1.66/0.48 (sF15 = ((f5 @ sF14)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 1.66/0.48 thf(f38,plain,(
% 1.66/0.48 (((f5 @ sF14)) = sF15)),
% 1.66/0.48 inference(reorient_equations,[],[f37])).
% 1.66/0.48 thf(f39,definition,(
% 1.66/0.48 (sF16 = ((f4 @ sF15)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 1.66/0.48 thf(f40,plain,(
% 1.66/0.48 (((f4 @ sF15)) = sF16)),
% 1.66/0.48 inference(reorient_equations,[],[f39])).
% 1.66/0.48 thf(f41,definition,(
% 1.66/0.48 (sF17 = ((f4 @ sF16)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 1.66/0.48 thf(f42,plain,(
% 1.66/0.48 (((f4 @ sF16)) = sF17)),
% 1.66/0.48 inference(reorient_equations,[],[f41])).
% 1.66/0.48 thf(f43,definition,(
% 1.66/0.48 (sF18 = ((f4 @ sF17)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 1.66/0.48 thf(f44,plain,(
% 1.66/0.48 (((f4 @ sF17)) = sF18)),
% 1.66/0.48 inference(reorient_equations,[],[f43])).
% 1.66/0.48 thf(f45,definition,(
% 1.66/0.48 (sF19 = ((f3 @ sF18)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 1.66/0.48 thf(f46,plain,(
% 1.66/0.48 (((f3 @ sF18)) = sF19)),
% 1.66/0.48 inference(reorient_equations,[],[f45])).
% 1.66/0.48 thf(f47,definition,(
% 1.66/0.48 (sF20 = ((f2 @ sF19)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 1.66/0.48 thf(f48,plain,(
% 1.66/0.48 (((f2 @ sF19)) = sF20)),
% 1.66/0.48 inference(reorient_equations,[],[f47])).
% 1.66/0.48 thf(f49,definition,(
% 1.66/0.48 (sF21 = ((f2 @ sF20)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 1.66/0.48 thf(f50,plain,(
% 1.66/0.48 (((f2 @ sF20)) = sF21)),
% 1.66/0.48 inference(reorient_equations,[],[f49])).
% 1.66/0.48 thf(f51,definition,(
% 1.66/0.48 (sF22 = ((f2 @ sF21)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 1.66/0.48 thf(f52,plain,(
% 1.66/0.48 (((f2 @ sF21)) = sF22)),
% 1.66/0.48 inference(reorient_equations,[],[f51])).
% 1.66/0.48 thf(f53,definition,(
% 1.66/0.48 (sF23 = ((f1 @ sF22)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 1.66/0.48 thf(f54,plain,(
% 1.66/0.48 (((f1 @ sF22)) = sF23)),
% 1.66/0.48 inference(reorient_equations,[],[f53])).
% 1.66/0.48 thf(f55,definition,(
% 1.66/0.48 (sF24 = ((f0 @ sF23)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 1.66/0.48 thf(f56,plain,(
% 1.66/0.48 (((f0 @ sF23)) = sF24)),
% 1.66/0.48 inference(reorient_equations,[],[f55])).
% 1.66/0.48 thf(f57,definition,(
% 1.66/0.48 (sF25 = ((f0 @ sF24)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 1.66/0.48 thf(f58,plain,(
% 1.66/0.48 (((f0 @ sF24)) = sF25)),
% 1.66/0.48 inference(reorient_equations,[],[f57])).
% 1.66/0.48 thf(f59,definition,(
% 1.66/0.48 (sF26 = ((f0 @ sF25)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 1.66/0.48 thf(f60,plain,(
% 1.66/0.48 (((f0 @ sF25)) = sF26)),
% 1.66/0.48 inference(reorient_equations,[],[f59])).
% 1.66/0.48 thf(f61,plain,(
% 1.66/0.48 (sF12 != sF26)),
% 1.66/0.48 inference(definition_folding,[],[f4,f60,f58,f56,f54,f52,f50,f48,f46,f44,f42,f40,f38,f36,f34,f8,f32,f30,f28,f26,f24,f22,f20,f18,f16,f14,f12,f10,f8])).
% 1.66/0.48 thf(f62,plain,(
% 1.66/0.48 ($true = sF12) | ($true = sF26)),
% 1.66/0.48 inference(xor_proxy_clausification,[],[f61])).
% 1.66/0.48 thf(f63,plain,(
% 1.66/0.48 ($false = sF12) | ($false = sF26)),
% 1.66/0.48 inference(xor_proxy_clausification,[],[f61])).
% 1.66/0.48 thf(f64,plain,(
% 1.66/0.48 (((f6 @ x)) = $true) | ($false = sF0)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f8])).
% 1.66/0.48 thf(f65,plain,(
% 1.66/0.48 (((f6 @ x)) = $false) | ($true = sF0)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f8])).
% 1.66/0.48 thf(f66,plain,(
% 1.66/0.48 ($true = ((f5 @ sF0))) | ($false = sF1)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f10])).
% 1.66/0.48 thf(f67,plain,(
% 1.66/0.48 ($false = ((f5 @ sF0))) | ($true = sF1)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f10])).
% 1.66/0.48 thf(f68,plain,(
% 1.66/0.48 ($true = ((f5 @ sF1))) | ($false = sF2)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f12])).
% 1.66/0.48 thf(f69,plain,(
% 1.66/0.48 ($false = ((f5 @ sF1))) | ($true = sF2)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f12])).
% 1.66/0.48 thf(f70,plain,(
% 1.66/0.48 ($true = ((f5 @ sF2))) | ($false = sF3)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f14])).
% 1.66/0.48 thf(f71,plain,(
% 1.66/0.48 ($false = ((f5 @ sF2))) | ($true = sF3)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f14])).
% 1.66/0.48 thf(f72,plain,(
% 1.66/0.48 ($true = ((f4 @ sF3))) | ($false = sF4)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f16])).
% 1.66/0.48 thf(f73,plain,(
% 1.66/0.48 ($false = ((f4 @ sF3))) | ($true = sF4)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f16])).
% 1.66/0.48 thf(f74,plain,(
% 1.66/0.48 ($true = ((f3 @ sF4))) | ($false = sF5)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f18])).
% 1.66/0.48 thf(f75,plain,(
% 1.66/0.48 ($false = ((f3 @ sF4))) | ($true = sF5)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f18])).
% 1.66/0.48 thf(f76,plain,(
% 1.66/0.48 ($true = ((f3 @ sF5))) | ($false = sF6)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f20])).
% 1.66/0.48 thf(f77,plain,(
% 1.66/0.48 ($false = ((f3 @ sF5))) | ($true = sF6)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f20])).
% 1.66/0.48 thf(f78,plain,(
% 1.66/0.48 ($true = ((f3 @ sF6))) | ($false = sF7)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f22])).
% 1.66/0.48 thf(f79,plain,(
% 1.66/0.48 ($false = ((f3 @ sF6))) | ($true = sF7)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f22])).
% 1.66/0.48 thf(f80,plain,(
% 1.66/0.48 ($true = ((f2 @ sF7))) | ($false = sF8)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f24])).
% 1.66/0.48 thf(f81,plain,(
% 1.66/0.48 ($false = ((f2 @ sF7))) | ($true = sF8)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f24])).
% 1.66/0.48 thf(f82,plain,(
% 1.66/0.48 ($true = ((f1 @ sF8))) | ($false = sF9)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f26])).
% 1.66/0.48 thf(f83,plain,(
% 1.66/0.48 ($false = ((f1 @ sF8))) | ($true = sF9)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f26])).
% 1.66/0.48 thf(f84,plain,(
% 1.66/0.48 ($true = ((f1 @ sF9))) | ($false = sF10)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f28])).
% 1.66/0.48 thf(f85,plain,(
% 1.66/0.48 ($false = ((f1 @ sF9))) | ($true = sF10)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f28])).
% 1.66/0.48 thf(f86,plain,(
% 1.66/0.48 ($true = ((f1 @ sF10))) | ($false = sF11)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f30])).
% 1.66/0.48 thf(f87,plain,(
% 1.66/0.48 ($false = ((f1 @ sF10))) | ($true = sF11)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f30])).
% 1.66/0.48 thf(f88,plain,(
% 1.66/0.48 ($true = ((f0 @ sF11))) | ($false = sF12)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f32])).
% 1.66/0.48 thf(f89,plain,(
% 1.66/0.48 ($false = ((f0 @ sF11))) | ($true = sF12)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f32])).
% 1.66/0.48 thf(f90,plain,(
% 1.66/0.48 ($true = ((f6 @ sF0))) | ($false = sF13)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f34])).
% 1.66/0.48 thf(f91,plain,(
% 1.66/0.48 ($false = ((f6 @ sF0))) | ($true = sF13)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f34])).
% 1.66/0.48 thf(f92,plain,(
% 1.66/0.48 ($true = ((f6 @ sF13))) | ($false = sF14)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f36])).
% 1.66/0.48 thf(f93,plain,(
% 1.66/0.48 ($false = ((f6 @ sF13))) | ($true = sF14)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f36])).
% 1.66/0.48 thf(f94,plain,(
% 1.66/0.48 ($true = ((f5 @ sF14))) | ($false = sF15)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f38])).
% 1.66/0.48 thf(f95,plain,(
% 1.66/0.48 ($false = ((f5 @ sF14))) | ($true = sF15)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f38])).
% 1.66/0.48 thf(f96,plain,(
% 1.66/0.48 ($true = ((f4 @ sF15))) | ($false = sF16)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f40])).
% 1.66/0.48 thf(f97,plain,(
% 1.66/0.48 ($false = ((f4 @ sF15))) | ($true = sF16)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f40])).
% 1.66/0.48 thf(f98,plain,(
% 1.66/0.48 ($true = ((f4 @ sF16))) | ($false = sF17)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f42])).
% 1.66/0.48 thf(f99,plain,(
% 1.66/0.48 ($false = ((f4 @ sF16))) | ($true = sF17)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f42])).
% 1.66/0.48 thf(f100,plain,(
% 1.66/0.48 ($true = ((f4 @ sF17))) | ($false = sF18)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f44])).
% 1.66/0.48 thf(f101,plain,(
% 1.66/0.48 ($false = ((f4 @ sF17))) | ($true = sF18)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f44])).
% 1.66/0.48 thf(f102,plain,(
% 1.66/0.48 ($true = ((f3 @ sF18))) | ($false = sF19)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f46])).
% 1.66/0.48 thf(f103,plain,(
% 1.66/0.48 ($false = ((f3 @ sF18))) | ($true = sF19)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f46])).
% 1.66/0.48 thf(f104,plain,(
% 1.66/0.48 ($true = ((f2 @ sF19))) | ($false = sF20)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f48])).
% 1.66/0.48 thf(f105,plain,(
% 1.66/0.48 ($false = ((f2 @ sF19))) | ($true = sF20)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f48])).
% 1.66/0.48 thf(f106,plain,(
% 1.66/0.48 ($true = ((f2 @ sF20))) | ($false = sF21)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f50])).
% 1.66/0.48 thf(f107,plain,(
% 1.66/0.48 ($false = ((f2 @ sF20))) | ($true = sF21)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f50])).
% 1.66/0.48 thf(f108,plain,(
% 1.66/0.48 ($true = ((f2 @ sF21))) | ($false = sF22)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f52])).
% 1.66/0.48 thf(f109,plain,(
% 1.66/0.48 ($false = ((f2 @ sF21))) | ($true = sF22)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f52])).
% 1.66/0.48 thf(f110,plain,(
% 1.66/0.48 ($true = ((f1 @ sF22))) | ($false = sF23)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f54])).
% 1.66/0.48 thf(f111,plain,(
% 1.66/0.48 ($false = ((f1 @ sF22))) | ($true = sF23)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f54])).
% 1.66/0.48 thf(f112,plain,(
% 1.66/0.48 ($true = ((f0 @ sF23))) | ($false = sF24)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f56])).
% 1.66/0.48 thf(f113,plain,(
% 1.66/0.48 ($false = ((f0 @ sF23))) | ($true = sF24)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f56])).
% 1.66/0.48 thf(f114,plain,(
% 1.66/0.48 ($true = ((f0 @ sF24))) | ($false = sF25)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f58])).
% 1.66/0.48 thf(f115,plain,(
% 1.66/0.48 ($false = ((f0 @ sF24))) | ($true = sF25)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f58])).
% 1.66/0.48 thf(f116,plain,(
% 1.66/0.48 ($true = ((f0 @ sF25))) | ($false = sF26)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f60])).
% 1.66/0.48 thf(f117,plain,(
% 1.66/0.48 ($false = ((f0 @ sF25))) | ($true = sF26)),
% 1.66/0.48 inference(iff_proxy_clausification,[],[f60])).
% 1.66/0.48 thf(f119,definition,(
% 1.66/0.48 spl27_1 <=> ($false = sF26)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition])).
% 1.66/0.48 thf(f121,plain,(
% 1.66/0.48 ($false = sF26) | ~spl27_1),
% 1.66/0.48 inference(avatar_component_clause,[],[f119])).
% 1.66/0.48 thf(f123,definition,(
% 1.66/0.48 spl27_2 <=> ($false = sF12)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition])).
% 1.66/0.48 thf(f125,plain,(
% 1.66/0.48 ($false = sF12) | ~spl27_2),
% 1.66/0.48 inference(avatar_component_clause,[],[f123])).
% 1.66/0.48 thf(f126,plain,(
% 1.66/0.48 spl27_1 | spl27_2),
% 1.66/0.48 inference(avatar_split_clause,[],[f63,f123,f119])).
% 1.66/0.48 thf(f128,definition,(
% 1.66/0.48 spl27_3 <=> ($true = sF26)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition])).
% 1.66/0.48 thf(f130,plain,(
% 1.66/0.48 ($true = sF26) | ~spl27_3),
% 1.66/0.48 inference(avatar_component_clause,[],[f128])).
% 1.66/0.48 thf(f132,definition,(
% 1.66/0.48 spl27_4 <=> ($true = sF12)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition])).
% 1.66/0.48 thf(f134,plain,(
% 1.66/0.48 ($true = sF12) | ~spl27_4),
% 1.66/0.48 inference(avatar_component_clause,[],[f132])).
% 1.66/0.48 thf(f135,plain,(
% 1.66/0.48 spl27_3 | spl27_4),
% 1.66/0.48 inference(avatar_split_clause,[],[f62,f132,f128])).
% 1.66/0.48 thf(f137,definition,(
% 1.66/0.48 spl27_5 <=> ($true = sF0)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition])).
% 1.66/0.48 thf(f138,plain,(
% 1.66/0.48 ($true != sF0) | spl27_5),
% 1.66/0.48 inference(avatar_component_clause,[],[f137])).
% 1.66/0.48 thf(f139,plain,(
% 1.66/0.48 ($true = sF0) | ~spl27_5),
% 1.66/0.48 inference(avatar_component_clause,[],[f137])).
% 1.66/0.48 thf(f141,definition,(
% 1.66/0.48 spl27_6 <=> (((f6 @ x)) = $false)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition])).
% 1.66/0.48 thf(f143,plain,(
% 1.66/0.48 (((f6 @ x)) = $false) | ~spl27_6),
% 1.66/0.48 inference(avatar_component_clause,[],[f141])).
% 1.66/0.48 thf(f144,plain,(
% 1.66/0.48 spl27_5 | spl27_6),
% 1.66/0.48 inference(avatar_split_clause,[],[f65,f141,f137])).
% 1.66/0.48 thf(f146,definition,(
% 1.66/0.48 spl27_7 <=> ($false = sF0)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition])).
% 1.66/0.48 thf(f147,plain,(
% 1.66/0.48 ($false != sF0) | spl27_7),
% 1.66/0.48 inference(avatar_component_clause,[],[f146])).
% 1.66/0.48 thf(f148,plain,(
% 1.66/0.48 ($false = sF0) | ~spl27_7),
% 1.66/0.48 inference(avatar_component_clause,[],[f146])).
% 1.66/0.48 thf(f150,definition,(
% 1.66/0.48 spl27_8 <=> (((f6 @ x)) = $true)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition])).
% 1.66/0.48 thf(f152,plain,(
% 1.66/0.48 (((f6 @ x)) = $true) | ~spl27_8),
% 1.66/0.48 inference(avatar_component_clause,[],[f150])).
% 1.66/0.48 thf(f153,plain,(
% 1.66/0.48 spl27_7 | spl27_8),
% 1.66/0.48 inference(avatar_split_clause,[],[f64,f150,f146])).
% 1.66/0.48 thf(f155,definition,(
% 1.66/0.48 spl27_9 <=> ($true = sF1)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition])).
% 1.66/0.48 thf(f156,plain,(
% 1.66/0.48 ($true != sF1) | spl27_9),
% 1.66/0.48 inference(avatar_component_clause,[],[f155])).
% 1.66/0.48 thf(f157,plain,(
% 1.66/0.48 ($true = sF1) | ~spl27_9),
% 1.66/0.48 inference(avatar_component_clause,[],[f155])).
% 1.66/0.48 thf(f159,definition,(
% 1.66/0.48 spl27_10 <=> ($false = ((f5 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition])).
% 1.66/0.48 thf(f160,plain,(
% 1.66/0.48 ($false != ((f5 @ sF0))) | spl27_10),
% 1.66/0.48 inference(avatar_component_clause,[],[f159])).
% 1.66/0.48 thf(f161,plain,(
% 1.66/0.48 ($false = ((f5 @ sF0))) | ~spl27_10),
% 1.66/0.48 inference(avatar_component_clause,[],[f159])).
% 1.66/0.48 thf(f162,plain,(
% 1.66/0.48 spl27_9 | spl27_10),
% 1.66/0.48 inference(avatar_split_clause,[],[f67,f159,f155])).
% 1.66/0.48 thf(f164,definition,(
% 1.66/0.48 spl27_11 <=> ($false = sF1)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition])).
% 1.66/0.48 thf(f166,plain,(
% 1.66/0.48 ($false = sF1) | ~spl27_11),
% 1.66/0.48 inference(avatar_component_clause,[],[f164])).
% 1.66/0.48 thf(f168,definition,(
% 1.66/0.48 spl27_12 <=> ($true = ((f5 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition])).
% 1.66/0.48 thf(f169,plain,(
% 1.66/0.48 ($true != ((f5 @ sF0))) | spl27_12),
% 1.66/0.48 inference(avatar_component_clause,[],[f168])).
% 1.66/0.48 thf(f170,plain,(
% 1.66/0.48 ($true = ((f5 @ sF0))) | ~spl27_12),
% 1.66/0.48 inference(avatar_component_clause,[],[f168])).
% 1.66/0.48 thf(f171,plain,(
% 1.66/0.48 spl27_11 | spl27_12),
% 1.66/0.48 inference(avatar_split_clause,[],[f66,f168,f164])).
% 1.66/0.48 thf(f173,definition,(
% 1.66/0.48 spl27_13 <=> ($true = sF2)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition])).
% 1.66/0.48 thf(f175,plain,(
% 1.66/0.48 ($true = sF2) | ~spl27_13),
% 1.66/0.48 inference(avatar_component_clause,[],[f173])).
% 1.66/0.48 thf(f177,definition,(
% 1.66/0.48 spl27_14 <=> ($false = ((f5 @ sF1)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition])).
% 1.66/0.48 thf(f179,plain,(
% 1.66/0.48 ($false = ((f5 @ sF1))) | ~spl27_14),
% 1.66/0.48 inference(avatar_component_clause,[],[f177])).
% 1.66/0.48 thf(f180,plain,(
% 1.66/0.48 spl27_13 | spl27_14),
% 1.66/0.48 inference(avatar_split_clause,[],[f69,f177,f173])).
% 1.66/0.48 thf(f182,definition,(
% 1.66/0.48 spl27_15 <=> ($false = sF2)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_15])],[avatar_definition])).
% 1.66/0.48 thf(f184,plain,(
% 1.66/0.48 ($false = sF2) | ~spl27_15),
% 1.66/0.48 inference(avatar_component_clause,[],[f182])).
% 1.66/0.48 thf(f186,definition,(
% 1.66/0.48 spl27_16 <=> ($true = ((f5 @ sF1)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_16])],[avatar_definition])).
% 1.66/0.48 thf(f187,plain,(
% 1.66/0.48 ($true != ((f5 @ sF1))) | spl27_16),
% 1.66/0.48 inference(avatar_component_clause,[],[f186])).
% 1.66/0.48 thf(f188,plain,(
% 1.66/0.48 ($true = ((f5 @ sF1))) | ~spl27_16),
% 1.66/0.48 inference(avatar_component_clause,[],[f186])).
% 1.66/0.48 thf(f189,plain,(
% 1.66/0.48 spl27_15 | spl27_16),
% 1.66/0.48 inference(avatar_split_clause,[],[f68,f186,f182])).
% 1.66/0.48 thf(f191,definition,(
% 1.66/0.48 spl27_17 <=> ($true = sF3)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_17])],[avatar_definition])).
% 1.66/0.48 thf(f192,plain,(
% 1.66/0.48 ($true != sF3) | spl27_17),
% 1.66/0.48 inference(avatar_component_clause,[],[f191])).
% 1.66/0.48 thf(f193,plain,(
% 1.66/0.48 ($true = sF3) | ~spl27_17),
% 1.66/0.48 inference(avatar_component_clause,[],[f191])).
% 1.66/0.48 thf(f195,definition,(
% 1.66/0.48 spl27_18 <=> ($false = ((f5 @ sF2)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition])).
% 1.66/0.48 thf(f196,plain,(
% 1.66/0.48 ($false != ((f5 @ sF2))) | spl27_18),
% 1.66/0.48 inference(avatar_component_clause,[],[f195])).
% 1.66/0.48 thf(f197,plain,(
% 1.66/0.48 ($false = ((f5 @ sF2))) | ~spl27_18),
% 1.66/0.48 inference(avatar_component_clause,[],[f195])).
% 1.66/0.48 thf(f198,plain,(
% 1.66/0.48 spl27_17 | spl27_18),
% 1.66/0.48 inference(avatar_split_clause,[],[f71,f195,f191])).
% 1.66/0.48 thf(f200,definition,(
% 1.66/0.48 spl27_19 <=> ($false = sF3)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_19])],[avatar_definition])).
% 1.66/0.48 thf(f201,plain,(
% 1.66/0.48 ($false != sF3) | spl27_19),
% 1.66/0.48 inference(avatar_component_clause,[],[f200])).
% 1.66/0.48 thf(f202,plain,(
% 1.66/0.48 ($false = sF3) | ~spl27_19),
% 1.66/0.48 inference(avatar_component_clause,[],[f200])).
% 1.66/0.48 thf(f204,definition,(
% 1.66/0.48 spl27_20 <=> ($true = ((f5 @ sF2)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition])).
% 1.66/0.48 thf(f206,plain,(
% 1.66/0.48 ($true = ((f5 @ sF2))) | ~spl27_20),
% 1.66/0.48 inference(avatar_component_clause,[],[f204])).
% 1.66/0.48 thf(f207,plain,(
% 1.66/0.48 spl27_19 | spl27_20),
% 1.66/0.48 inference(avatar_split_clause,[],[f70,f204,f200])).
% 1.66/0.48 thf(f209,definition,(
% 1.66/0.48 spl27_21 <=> ($true = sF4)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition])).
% 1.66/0.48 thf(f210,plain,(
% 1.66/0.48 ($true != sF4) | spl27_21),
% 1.66/0.48 inference(avatar_component_clause,[],[f209])).
% 1.66/0.48 thf(f211,plain,(
% 1.66/0.48 ($true = sF4) | ~spl27_21),
% 1.66/0.48 inference(avatar_component_clause,[],[f209])).
% 1.66/0.48 thf(f213,definition,(
% 1.66/0.48 spl27_22 <=> ($false = ((f4 @ sF3)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_22])],[avatar_definition])).
% 1.66/0.48 thf(f214,plain,(
% 1.66/0.48 ($false != ((f4 @ sF3))) | spl27_22),
% 1.66/0.48 inference(avatar_component_clause,[],[f213])).
% 1.66/0.48 thf(f215,plain,(
% 1.66/0.48 ($false = ((f4 @ sF3))) | ~spl27_22),
% 1.66/0.48 inference(avatar_component_clause,[],[f213])).
% 1.66/0.48 thf(f216,plain,(
% 1.66/0.48 spl27_21 | spl27_22),
% 1.66/0.48 inference(avatar_split_clause,[],[f73,f213,f209])).
% 1.66/0.48 thf(f218,definition,(
% 1.66/0.48 spl27_23 <=> ($false = sF4)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_23])],[avatar_definition])).
% 1.66/0.48 thf(f220,plain,(
% 1.66/0.48 ($false = sF4) | ~spl27_23),
% 1.66/0.48 inference(avatar_component_clause,[],[f218])).
% 1.66/0.48 thf(f222,definition,(
% 1.66/0.48 spl27_24 <=> ($true = ((f4 @ sF3)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_24])],[avatar_definition])).
% 1.66/0.48 thf(f224,plain,(
% 1.66/0.48 ($true = ((f4 @ sF3))) | ~spl27_24),
% 1.66/0.48 inference(avatar_component_clause,[],[f222])).
% 1.66/0.48 thf(f225,plain,(
% 1.66/0.48 spl27_23 | spl27_24),
% 1.66/0.48 inference(avatar_split_clause,[],[f72,f222,f218])).
% 1.66/0.48 thf(f227,definition,(
% 1.66/0.48 spl27_25 <=> ($true = sF5)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_25])],[avatar_definition])).
% 1.66/0.48 thf(f228,plain,(
% 1.66/0.48 ($true != sF5) | spl27_25),
% 1.66/0.48 inference(avatar_component_clause,[],[f227])).
% 1.66/0.48 thf(f229,plain,(
% 1.66/0.48 ($true = sF5) | ~spl27_25),
% 1.66/0.48 inference(avatar_component_clause,[],[f227])).
% 1.66/0.48 thf(f231,definition,(
% 1.66/0.48 spl27_26 <=> ($false = ((f3 @ sF4)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_26])],[avatar_definition])).
% 1.66/0.48 thf(f233,plain,(
% 1.66/0.48 ($false = ((f3 @ sF4))) | ~spl27_26),
% 1.66/0.48 inference(avatar_component_clause,[],[f231])).
% 1.66/0.48 thf(f234,plain,(
% 1.66/0.48 spl27_25 | spl27_26),
% 1.66/0.48 inference(avatar_split_clause,[],[f75,f231,f227])).
% 1.66/0.48 thf(f236,definition,(
% 1.66/0.48 spl27_27 <=> ($false = sF5)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_27])],[avatar_definition])).
% 1.66/0.48 thf(f238,plain,(
% 1.66/0.48 ($false = sF5) | ~spl27_27),
% 1.66/0.48 inference(avatar_component_clause,[],[f236])).
% 1.66/0.48 thf(f240,definition,(
% 1.66/0.48 spl27_28 <=> ($true = ((f3 @ sF4)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_28])],[avatar_definition])).
% 1.66/0.48 thf(f242,plain,(
% 1.66/0.48 ($true = ((f3 @ sF4))) | ~spl27_28),
% 1.66/0.48 inference(avatar_component_clause,[],[f240])).
% 1.66/0.48 thf(f243,plain,(
% 1.66/0.48 spl27_27 | spl27_28),
% 1.66/0.48 inference(avatar_split_clause,[],[f74,f240,f236])).
% 1.66/0.48 thf(f245,definition,(
% 1.66/0.48 spl27_29 <=> ($true = sF6)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition])).
% 1.66/0.48 thf(f246,plain,(
% 1.66/0.48 ($true != sF6) | spl27_29),
% 1.66/0.48 inference(avatar_component_clause,[],[f245])).
% 1.66/0.48 thf(f247,plain,(
% 1.66/0.48 ($true = sF6) | ~spl27_29),
% 1.66/0.48 inference(avatar_component_clause,[],[f245])).
% 1.66/0.48 thf(f249,definition,(
% 1.66/0.48 spl27_30 <=> ($false = ((f3 @ sF5)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition])).
% 1.66/0.48 thf(f251,plain,(
% 1.66/0.48 ($false = ((f3 @ sF5))) | ~spl27_30),
% 1.66/0.48 inference(avatar_component_clause,[],[f249])).
% 1.66/0.48 thf(f252,plain,(
% 1.66/0.48 spl27_29 | spl27_30),
% 1.66/0.48 inference(avatar_split_clause,[],[f77,f249,f245])).
% 1.66/0.48 thf(f254,definition,(
% 1.66/0.48 spl27_31 <=> ($false = sF6)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_31])],[avatar_definition])).
% 1.66/0.48 thf(f255,plain,(
% 1.66/0.48 ($false != sF6) | spl27_31),
% 1.66/0.48 inference(avatar_component_clause,[],[f254])).
% 1.66/0.48 thf(f256,plain,(
% 1.66/0.48 ($false = sF6) | ~spl27_31),
% 1.66/0.48 inference(avatar_component_clause,[],[f254])).
% 1.66/0.48 thf(f258,definition,(
% 1.66/0.48 spl27_32 <=> ($true = ((f3 @ sF5)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_32])],[avatar_definition])).
% 1.66/0.48 thf(f260,plain,(
% 1.66/0.48 ($true = ((f3 @ sF5))) | ~spl27_32),
% 1.66/0.48 inference(avatar_component_clause,[],[f258])).
% 1.66/0.48 thf(f261,plain,(
% 1.66/0.48 spl27_31 | spl27_32),
% 1.66/0.48 inference(avatar_split_clause,[],[f76,f258,f254])).
% 1.66/0.48 thf(f263,definition,(
% 1.66/0.48 spl27_33 <=> ($true = sF7)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_33])],[avatar_definition])).
% 1.66/0.48 thf(f265,plain,(
% 1.66/0.48 ($true = sF7) | ~spl27_33),
% 1.66/0.48 inference(avatar_component_clause,[],[f263])).
% 1.66/0.48 thf(f267,definition,(
% 1.66/0.48 spl27_34 <=> ($false = ((f3 @ sF6)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition])).
% 1.66/0.48 thf(f268,plain,(
% 1.66/0.48 ($false != ((f3 @ sF6))) | spl27_34),
% 1.66/0.48 inference(avatar_component_clause,[],[f267])).
% 1.66/0.48 thf(f269,plain,(
% 1.66/0.48 ($false = ((f3 @ sF6))) | ~spl27_34),
% 1.66/0.48 inference(avatar_component_clause,[],[f267])).
% 1.66/0.48 thf(f270,plain,(
% 1.66/0.48 spl27_33 | spl27_34),
% 1.66/0.48 inference(avatar_split_clause,[],[f79,f267,f263])).
% 1.66/0.48 thf(f272,definition,(
% 1.66/0.48 spl27_35 <=> ($false = sF7)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition])).
% 1.66/0.48 thf(f274,plain,(
% 1.66/0.48 ($false = sF7) | ~spl27_35),
% 1.66/0.48 inference(avatar_component_clause,[],[f272])).
% 1.66/0.48 thf(f276,definition,(
% 1.66/0.48 spl27_36 <=> ($true = ((f3 @ sF6)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_36])],[avatar_definition])).
% 1.66/0.48 thf(f277,plain,(
% 1.66/0.48 ($true != ((f3 @ sF6))) | spl27_36),
% 1.66/0.48 inference(avatar_component_clause,[],[f276])).
% 1.66/0.48 thf(f278,plain,(
% 1.66/0.48 ($true = ((f3 @ sF6))) | ~spl27_36),
% 1.66/0.48 inference(avatar_component_clause,[],[f276])).
% 1.66/0.48 thf(f279,plain,(
% 1.66/0.48 spl27_35 | spl27_36),
% 1.66/0.48 inference(avatar_split_clause,[],[f78,f276,f272])).
% 1.66/0.48 thf(f281,definition,(
% 1.66/0.48 spl27_37 <=> ($true = sF8)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_37])],[avatar_definition])).
% 1.66/0.48 thf(f282,plain,(
% 1.66/0.48 ($true != sF8) | spl27_37),
% 1.66/0.48 inference(avatar_component_clause,[],[f281])).
% 1.66/0.48 thf(f283,plain,(
% 1.66/0.48 ($true = sF8) | ~spl27_37),
% 1.66/0.48 inference(avatar_component_clause,[],[f281])).
% 1.66/0.48 thf(f285,definition,(
% 1.66/0.48 spl27_38 <=> ($false = ((f2 @ sF7)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_38])],[avatar_definition])).
% 1.66/0.48 thf(f286,plain,(
% 1.66/0.48 ($false != ((f2 @ sF7))) | spl27_38),
% 1.66/0.48 inference(avatar_component_clause,[],[f285])).
% 1.66/0.48 thf(f287,plain,(
% 1.66/0.48 ($false = ((f2 @ sF7))) | ~spl27_38),
% 1.66/0.48 inference(avatar_component_clause,[],[f285])).
% 1.66/0.48 thf(f288,plain,(
% 1.66/0.48 spl27_37 | spl27_38),
% 1.66/0.48 inference(avatar_split_clause,[],[f81,f285,f281])).
% 1.66/0.48 thf(f290,definition,(
% 1.66/0.48 spl27_39 <=> ($false = sF8)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_39])],[avatar_definition])).
% 1.66/0.48 thf(f292,plain,(
% 1.66/0.48 ($false = sF8) | ~spl27_39),
% 1.66/0.48 inference(avatar_component_clause,[],[f290])).
% 1.66/0.48 thf(f294,definition,(
% 1.66/0.48 spl27_40 <=> ($true = ((f2 @ sF7)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_40])],[avatar_definition])).
% 1.66/0.48 thf(f295,plain,(
% 1.66/0.48 ($true != ((f2 @ sF7))) | spl27_40),
% 1.66/0.48 inference(avatar_component_clause,[],[f294])).
% 1.66/0.48 thf(f296,plain,(
% 1.66/0.48 ($true = ((f2 @ sF7))) | ~spl27_40),
% 1.66/0.48 inference(avatar_component_clause,[],[f294])).
% 1.66/0.48 thf(f297,plain,(
% 1.66/0.48 spl27_39 | spl27_40),
% 1.66/0.48 inference(avatar_split_clause,[],[f80,f294,f290])).
% 1.66/0.48 thf(f299,definition,(
% 1.66/0.48 spl27_41 <=> ($true = sF9)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_41])],[avatar_definition])).
% 1.66/0.48 thf(f300,plain,(
% 1.66/0.48 ($true != sF9) | spl27_41),
% 1.66/0.48 inference(avatar_component_clause,[],[f299])).
% 1.66/0.48 thf(f301,plain,(
% 1.66/0.48 ($true = sF9) | ~spl27_41),
% 1.66/0.48 inference(avatar_component_clause,[],[f299])).
% 1.66/0.48 thf(f303,definition,(
% 1.66/0.48 spl27_42 <=> ($false = ((f1 @ sF8)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_42])],[avatar_definition])).
% 1.66/0.48 thf(f304,plain,(
% 1.66/0.48 ($false != ((f1 @ sF8))) | spl27_42),
% 1.66/0.48 inference(avatar_component_clause,[],[f303])).
% 1.66/0.48 thf(f305,plain,(
% 1.66/0.48 ($false = ((f1 @ sF8))) | ~spl27_42),
% 1.66/0.48 inference(avatar_component_clause,[],[f303])).
% 1.66/0.48 thf(f306,plain,(
% 1.66/0.48 spl27_41 | spl27_42),
% 1.66/0.48 inference(avatar_split_clause,[],[f83,f303,f299])).
% 1.66/0.48 thf(f308,definition,(
% 1.66/0.48 spl27_43 <=> ($false = sF9)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_43])],[avatar_definition])).
% 1.66/0.48 thf(f310,plain,(
% 1.66/0.48 ($false = sF9) | ~spl27_43),
% 1.66/0.48 inference(avatar_component_clause,[],[f308])).
% 1.66/0.48 thf(f312,definition,(
% 1.66/0.48 spl27_44 <=> ($true = ((f1 @ sF8)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_44])],[avatar_definition])).
% 1.66/0.48 thf(f313,plain,(
% 1.66/0.48 ($true != ((f1 @ sF8))) | spl27_44),
% 1.66/0.48 inference(avatar_component_clause,[],[f312])).
% 1.66/0.48 thf(f314,plain,(
% 1.66/0.48 ($true = ((f1 @ sF8))) | ~spl27_44),
% 1.66/0.48 inference(avatar_component_clause,[],[f312])).
% 1.66/0.48 thf(f315,plain,(
% 1.66/0.48 spl27_43 | spl27_44),
% 1.66/0.48 inference(avatar_split_clause,[],[f82,f312,f308])).
% 1.66/0.48 thf(f317,definition,(
% 1.66/0.48 spl27_45 <=> ($true = sF10)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition])).
% 1.66/0.48 thf(f318,plain,(
% 1.66/0.48 ($true != sF10) | spl27_45),
% 1.66/0.48 inference(avatar_component_clause,[],[f317])).
% 1.66/0.48 thf(f319,plain,(
% 1.66/0.48 ($true = sF10) | ~spl27_45),
% 1.66/0.48 inference(avatar_component_clause,[],[f317])).
% 1.66/0.48 thf(f321,definition,(
% 1.66/0.48 spl27_46 <=> ($false = ((f1 @ sF9)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition])).
% 1.66/0.48 thf(f322,plain,(
% 1.66/0.48 ($false != ((f1 @ sF9))) | spl27_46),
% 1.66/0.48 inference(avatar_component_clause,[],[f321])).
% 1.66/0.48 thf(f323,plain,(
% 1.66/0.48 ($false = ((f1 @ sF9))) | ~spl27_46),
% 1.66/0.48 inference(avatar_component_clause,[],[f321])).
% 1.66/0.48 thf(f324,plain,(
% 1.66/0.48 spl27_45 | spl27_46),
% 1.66/0.48 inference(avatar_split_clause,[],[f85,f321,f317])).
% 1.66/0.48 thf(f326,definition,(
% 1.66/0.48 spl27_47 <=> ($false = sF10)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_47])],[avatar_definition])).
% 1.66/0.48 thf(f328,plain,(
% 1.66/0.48 ($false = sF10) | ~spl27_47),
% 1.66/0.48 inference(avatar_component_clause,[],[f326])).
% 1.66/0.48 thf(f330,definition,(
% 1.66/0.48 spl27_48 <=> ($true = ((f1 @ sF9)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition])).
% 1.66/0.48 thf(f332,plain,(
% 1.66/0.48 ($true = ((f1 @ sF9))) | ~spl27_48),
% 1.66/0.48 inference(avatar_component_clause,[],[f330])).
% 1.66/0.48 thf(f333,plain,(
% 1.66/0.48 spl27_47 | spl27_48),
% 1.66/0.48 inference(avatar_split_clause,[],[f84,f330,f326])).
% 1.66/0.48 thf(f335,definition,(
% 1.66/0.48 spl27_49 <=> ($true = sF11)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_49])],[avatar_definition])).
% 1.66/0.48 thf(f337,plain,(
% 1.66/0.48 ($true = sF11) | ~spl27_49),
% 1.66/0.48 inference(avatar_component_clause,[],[f335])).
% 1.66/0.48 thf(f339,definition,(
% 1.66/0.48 spl27_50 <=> ($false = ((f1 @ sF10)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_50])],[avatar_definition])).
% 1.66/0.48 thf(f341,plain,(
% 1.66/0.48 ($false = ((f1 @ sF10))) | ~spl27_50),
% 1.66/0.48 inference(avatar_component_clause,[],[f339])).
% 1.66/0.48 thf(f342,plain,(
% 1.66/0.48 spl27_49 | spl27_50),
% 1.66/0.48 inference(avatar_split_clause,[],[f87,f339,f335])).
% 1.66/0.48 thf(f344,definition,(
% 1.66/0.48 spl27_51 <=> ($false = sF11)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_51])],[avatar_definition])).
% 1.66/0.48 thf(f346,plain,(
% 1.66/0.48 ($false = sF11) | ~spl27_51),
% 1.66/0.48 inference(avatar_component_clause,[],[f344])).
% 1.66/0.48 thf(f348,definition,(
% 1.66/0.48 spl27_52 <=> ($true = ((f1 @ sF10)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_52])],[avatar_definition])).
% 1.66/0.48 thf(f350,plain,(
% 1.66/0.48 ($true = ((f1 @ sF10))) | ~spl27_52),
% 1.66/0.48 inference(avatar_component_clause,[],[f348])).
% 1.66/0.48 thf(f351,plain,(
% 1.66/0.48 spl27_51 | spl27_52),
% 1.66/0.48 inference(avatar_split_clause,[],[f86,f348,f344])).
% 1.66/0.48 thf(f353,definition,(
% 1.66/0.48 spl27_53 <=> ($false = ((f0 @ sF11)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_53])],[avatar_definition])).
% 1.66/0.48 thf(f355,plain,(
% 1.66/0.48 ($false = ((f0 @ sF11))) | ~spl27_53),
% 1.66/0.48 inference(avatar_component_clause,[],[f353])).
% 1.66/0.48 thf(f356,plain,(
% 1.66/0.48 spl27_4 | spl27_53),
% 1.66/0.48 inference(avatar_split_clause,[],[f89,f353,f132])).
% 1.66/0.48 thf(f358,definition,(
% 1.66/0.48 spl27_54 <=> ($true = ((f0 @ sF11)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_54])],[avatar_definition])).
% 1.66/0.48 thf(f360,plain,(
% 1.66/0.48 ($true = ((f0 @ sF11))) | ~spl27_54),
% 1.66/0.48 inference(avatar_component_clause,[],[f358])).
% 1.66/0.48 thf(f361,plain,(
% 1.66/0.48 spl27_2 | spl27_54),
% 1.66/0.48 inference(avatar_split_clause,[],[f88,f358,f123])).
% 1.66/0.48 thf(f363,definition,(
% 1.66/0.48 spl27_55 <=> ($true = sF13)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_55])],[avatar_definition])).
% 1.66/0.48 thf(f365,plain,(
% 1.66/0.48 ($true = sF13) | ~spl27_55),
% 1.66/0.48 inference(avatar_component_clause,[],[f363])).
% 1.66/0.48 thf(f367,definition,(
% 1.66/0.48 spl27_56 <=> ($false = ((f6 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_56])],[avatar_definition])).
% 1.66/0.48 thf(f368,plain,(
% 1.66/0.48 ($false != ((f6 @ sF0))) | spl27_56),
% 1.66/0.48 inference(avatar_component_clause,[],[f367])).
% 1.66/0.48 thf(f369,plain,(
% 1.66/0.48 ($false = ((f6 @ sF0))) | ~spl27_56),
% 1.66/0.48 inference(avatar_component_clause,[],[f367])).
% 1.66/0.48 thf(f370,plain,(
% 1.66/0.48 spl27_55 | spl27_56),
% 1.66/0.48 inference(avatar_split_clause,[],[f91,f367,f363])).
% 1.66/0.48 thf(f372,definition,(
% 1.66/0.48 spl27_57 <=> ($false = sF13)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_57])],[avatar_definition])).
% 1.66/0.48 thf(f374,plain,(
% 1.66/0.48 ($false = sF13) | ~spl27_57),
% 1.66/0.48 inference(avatar_component_clause,[],[f372])).
% 1.66/0.48 thf(f376,definition,(
% 1.66/0.48 spl27_58 <=> ($true = ((f6 @ sF0)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_58])],[avatar_definition])).
% 1.66/0.48 thf(f378,plain,(
% 1.66/0.48 ($true = ((f6 @ sF0))) | ~spl27_58),
% 1.66/0.48 inference(avatar_component_clause,[],[f376])).
% 1.66/0.48 thf(f379,plain,(
% 1.66/0.48 spl27_57 | spl27_58),
% 1.66/0.48 inference(avatar_split_clause,[],[f90,f376,f372])).
% 1.66/0.48 thf(f381,definition,(
% 1.66/0.48 spl27_59 <=> ($true = sF14)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_59])],[avatar_definition])).
% 1.66/0.48 thf(f382,plain,(
% 1.66/0.48 ($true != sF14) | spl27_59),
% 1.66/0.48 inference(avatar_component_clause,[],[f381])).
% 1.66/0.48 thf(f383,plain,(
% 1.66/0.48 ($true = sF14) | ~spl27_59),
% 1.66/0.48 inference(avatar_component_clause,[],[f381])).
% 1.66/0.48 thf(f385,definition,(
% 1.66/0.48 spl27_60 <=> ($false = ((f6 @ sF13)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_60])],[avatar_definition])).
% 1.66/0.48 thf(f387,plain,(
% 1.66/0.48 ($false = ((f6 @ sF13))) | ~spl27_60),
% 1.66/0.48 inference(avatar_component_clause,[],[f385])).
% 1.66/0.48 thf(f388,plain,(
% 1.66/0.48 spl27_59 | spl27_60),
% 1.66/0.48 inference(avatar_split_clause,[],[f93,f385,f381])).
% 1.66/0.48 thf(f390,definition,(
% 1.66/0.48 spl27_61 <=> ($false = sF14)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_61])],[avatar_definition])).
% 1.66/0.48 thf(f392,plain,(
% 1.66/0.48 ($false = sF14) | ~spl27_61),
% 1.66/0.48 inference(avatar_component_clause,[],[f390])).
% 1.66/0.48 thf(f394,definition,(
% 1.66/0.48 spl27_62 <=> ($true = ((f6 @ sF13)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_62])],[avatar_definition])).
% 1.66/0.48 thf(f395,plain,(
% 1.66/0.48 ($true != ((f6 @ sF13))) | spl27_62),
% 1.66/0.48 inference(avatar_component_clause,[],[f394])).
% 1.66/0.48 thf(f396,plain,(
% 1.66/0.48 ($true = ((f6 @ sF13))) | ~spl27_62),
% 1.66/0.48 inference(avatar_component_clause,[],[f394])).
% 1.66/0.48 thf(f397,plain,(
% 1.66/0.48 spl27_61 | spl27_62),
% 1.66/0.48 inference(avatar_split_clause,[],[f92,f394,f390])).
% 1.66/0.48 thf(f399,definition,(
% 1.66/0.48 spl27_63 <=> ($true = sF15)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_63])],[avatar_definition])).
% 1.66/0.48 thf(f401,plain,(
% 1.66/0.48 ($true = sF15) | ~spl27_63),
% 1.66/0.48 inference(avatar_component_clause,[],[f399])).
% 1.66/0.48 thf(f403,definition,(
% 1.66/0.48 spl27_64 <=> ($false = ((f5 @ sF14)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_64])],[avatar_definition])).
% 1.66/0.48 thf(f404,plain,(
% 1.66/0.48 ($false != ((f5 @ sF14))) | spl27_64),
% 1.66/0.48 inference(avatar_component_clause,[],[f403])).
% 1.66/0.48 thf(f405,plain,(
% 1.66/0.48 ($false = ((f5 @ sF14))) | ~spl27_64),
% 1.66/0.48 inference(avatar_component_clause,[],[f403])).
% 1.66/0.48 thf(f406,plain,(
% 1.66/0.48 spl27_63 | spl27_64),
% 1.66/0.48 inference(avatar_split_clause,[],[f95,f403,f399])).
% 1.66/0.48 thf(f408,definition,(
% 1.66/0.48 spl27_65 <=> ($false = sF15)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_65])],[avatar_definition])).
% 1.66/0.48 thf(f410,plain,(
% 1.66/0.48 ($false = sF15) | ~spl27_65),
% 1.66/0.48 inference(avatar_component_clause,[],[f408])).
% 1.66/0.48 thf(f412,definition,(
% 1.66/0.48 spl27_66 <=> ($true = ((f5 @ sF14)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_66])],[avatar_definition])).
% 1.66/0.48 thf(f413,plain,(
% 1.66/0.48 ($true != ((f5 @ sF14))) | spl27_66),
% 1.66/0.48 inference(avatar_component_clause,[],[f412])).
% 1.66/0.48 thf(f414,plain,(
% 1.66/0.48 ($true = ((f5 @ sF14))) | ~spl27_66),
% 1.66/0.48 inference(avatar_component_clause,[],[f412])).
% 1.66/0.48 thf(f415,plain,(
% 1.66/0.48 spl27_65 | spl27_66),
% 1.66/0.48 inference(avatar_split_clause,[],[f94,f412,f408])).
% 1.66/0.48 thf(f417,definition,(
% 1.66/0.48 spl27_67 <=> ($true = sF16)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_67])],[avatar_definition])).
% 1.66/0.48 thf(f418,plain,(
% 1.66/0.48 ($true != sF16) | spl27_67),
% 1.66/0.48 inference(avatar_component_clause,[],[f417])).
% 1.66/0.48 thf(f419,plain,(
% 1.66/0.48 ($true = sF16) | ~spl27_67),
% 1.66/0.48 inference(avatar_component_clause,[],[f417])).
% 1.66/0.48 thf(f421,definition,(
% 1.66/0.48 spl27_68 <=> ($false = ((f4 @ sF15)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_68])],[avatar_definition])).
% 1.66/0.48 thf(f423,plain,(
% 1.66/0.48 ($false = ((f4 @ sF15))) | ~spl27_68),
% 1.66/0.48 inference(avatar_component_clause,[],[f421])).
% 1.66/0.48 thf(f424,plain,(
% 1.66/0.48 spl27_67 | spl27_68),
% 1.66/0.48 inference(avatar_split_clause,[],[f97,f421,f417])).
% 1.66/0.48 thf(f426,definition,(
% 1.66/0.48 spl27_69 <=> ($false = sF16)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_69])],[avatar_definition])).
% 1.66/0.48 thf(f428,plain,(
% 1.66/0.48 ($false = sF16) | ~spl27_69),
% 1.66/0.48 inference(avatar_component_clause,[],[f426])).
% 1.66/0.48 thf(f430,definition,(
% 1.66/0.48 spl27_70 <=> ($true = ((f4 @ sF15)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_70])],[avatar_definition])).
% 1.66/0.48 thf(f431,plain,(
% 1.66/0.48 ($true != ((f4 @ sF15))) | spl27_70),
% 1.66/0.48 inference(avatar_component_clause,[],[f430])).
% 1.66/0.48 thf(f432,plain,(
% 1.66/0.48 ($true = ((f4 @ sF15))) | ~spl27_70),
% 1.66/0.48 inference(avatar_component_clause,[],[f430])).
% 1.66/0.48 thf(f433,plain,(
% 1.66/0.48 spl27_69 | spl27_70),
% 1.66/0.48 inference(avatar_split_clause,[],[f96,f430,f426])).
% 1.66/0.48 thf(f435,definition,(
% 1.66/0.48 spl27_71 <=> ($true = sF17)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_71])],[avatar_definition])).
% 1.66/0.48 thf(f436,plain,(
% 1.66/0.48 ($true != sF17) | spl27_71),
% 1.66/0.48 inference(avatar_component_clause,[],[f435])).
% 1.66/0.48 thf(f437,plain,(
% 1.66/0.48 ($true = sF17) | ~spl27_71),
% 1.66/0.48 inference(avatar_component_clause,[],[f435])).
% 1.66/0.48 thf(f439,definition,(
% 1.66/0.48 spl27_72 <=> ($false = ((f4 @ sF16)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_72])],[avatar_definition])).
% 1.66/0.48 thf(f440,plain,(
% 1.66/0.48 ($false != ((f4 @ sF16))) | spl27_72),
% 1.66/0.48 inference(avatar_component_clause,[],[f439])).
% 1.66/0.48 thf(f441,plain,(
% 1.66/0.48 ($false = ((f4 @ sF16))) | ~spl27_72),
% 1.66/0.48 inference(avatar_component_clause,[],[f439])).
% 1.66/0.48 thf(f442,plain,(
% 1.66/0.48 spl27_71 | spl27_72),
% 1.66/0.48 inference(avatar_split_clause,[],[f99,f439,f435])).
% 1.66/0.48 thf(f444,definition,(
% 1.66/0.48 spl27_73 <=> ($false = sF17)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_73])],[avatar_definition])).
% 1.66/0.48 thf(f446,plain,(
% 1.66/0.48 ($false = sF17) | ~spl27_73),
% 1.66/0.48 inference(avatar_component_clause,[],[f444])).
% 1.66/0.48 thf(f448,definition,(
% 1.66/0.48 spl27_74 <=> ($true = ((f4 @ sF16)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_74])],[avatar_definition])).
% 1.66/0.48 thf(f449,plain,(
% 1.66/0.48 ($true != ((f4 @ sF16))) | spl27_74),
% 1.66/0.48 inference(avatar_component_clause,[],[f448])).
% 1.66/0.48 thf(f450,plain,(
% 1.66/0.48 ($true = ((f4 @ sF16))) | ~spl27_74),
% 1.66/0.48 inference(avatar_component_clause,[],[f448])).
% 1.66/0.48 thf(f451,plain,(
% 1.66/0.48 spl27_73 | spl27_74),
% 1.66/0.48 inference(avatar_split_clause,[],[f98,f448,f444])).
% 1.66/0.48 thf(f453,definition,(
% 1.66/0.48 spl27_75 <=> ($true = sF18)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_75])],[avatar_definition])).
% 1.66/0.48 thf(f455,plain,(
% 1.66/0.48 ($true = sF18) | ~spl27_75),
% 1.66/0.48 inference(avatar_component_clause,[],[f453])).
% 1.66/0.48 thf(f457,definition,(
% 1.66/0.48 spl27_76 <=> ($false = ((f4 @ sF17)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_76])],[avatar_definition])).
% 1.66/0.48 thf(f458,plain,(
% 1.66/0.48 ($false != ((f4 @ sF17))) | spl27_76),
% 1.66/0.48 inference(avatar_component_clause,[],[f457])).
% 1.66/0.48 thf(f459,plain,(
% 1.66/0.48 ($false = ((f4 @ sF17))) | ~spl27_76),
% 1.66/0.48 inference(avatar_component_clause,[],[f457])).
% 1.66/0.48 thf(f460,plain,(
% 1.66/0.48 spl27_75 | spl27_76),
% 1.66/0.48 inference(avatar_split_clause,[],[f101,f457,f453])).
% 1.66/0.48 thf(f462,definition,(
% 1.66/0.48 spl27_77 <=> ($false = sF18)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_77])],[avatar_definition])).
% 1.66/0.48 thf(f464,plain,(
% 1.66/0.48 ($false = sF18) | ~spl27_77),
% 1.66/0.48 inference(avatar_component_clause,[],[f462])).
% 1.66/0.48 thf(f466,definition,(
% 1.66/0.48 spl27_78 <=> ($true = ((f4 @ sF17)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_78])],[avatar_definition])).
% 1.66/0.48 thf(f467,plain,(
% 1.66/0.48 ($true != ((f4 @ sF17))) | spl27_78),
% 1.66/0.48 inference(avatar_component_clause,[],[f466])).
% 1.66/0.48 thf(f468,plain,(
% 1.66/0.48 ($true = ((f4 @ sF17))) | ~spl27_78),
% 1.66/0.48 inference(avatar_component_clause,[],[f466])).
% 1.66/0.48 thf(f469,plain,(
% 1.66/0.48 spl27_77 | spl27_78),
% 1.66/0.48 inference(avatar_split_clause,[],[f100,f466,f462])).
% 1.66/0.48 thf(f471,definition,(
% 1.66/0.48 spl27_79 <=> ($true = sF19)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_79])],[avatar_definition])).
% 1.66/0.48 thf(f473,plain,(
% 1.66/0.48 ($true = sF19) | ~spl27_79),
% 1.66/0.48 inference(avatar_component_clause,[],[f471])).
% 1.66/0.48 thf(f475,definition,(
% 1.66/0.48 spl27_80 <=> ($false = ((f3 @ sF18)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_80])],[avatar_definition])).
% 1.66/0.48 thf(f476,plain,(
% 1.66/0.48 ($false != ((f3 @ sF18))) | spl27_80),
% 1.66/0.48 inference(avatar_component_clause,[],[f475])).
% 1.66/0.48 thf(f477,plain,(
% 1.66/0.48 ($false = ((f3 @ sF18))) | ~spl27_80),
% 1.66/0.48 inference(avatar_component_clause,[],[f475])).
% 1.66/0.48 thf(f478,plain,(
% 1.66/0.48 spl27_79 | spl27_80),
% 1.66/0.48 inference(avatar_split_clause,[],[f103,f475,f471])).
% 1.66/0.48 thf(f480,definition,(
% 1.66/0.48 spl27_81 <=> ($false = sF19)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_81])],[avatar_definition])).
% 1.66/0.48 thf(f482,plain,(
% 1.66/0.48 ($false = sF19) | ~spl27_81),
% 1.66/0.48 inference(avatar_component_clause,[],[f480])).
% 1.66/0.48 thf(f484,definition,(
% 1.66/0.48 spl27_82 <=> ($true = ((f3 @ sF18)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_82])],[avatar_definition])).
% 1.66/0.48 thf(f486,plain,(
% 1.66/0.48 ($true = ((f3 @ sF18))) | ~spl27_82),
% 1.66/0.48 inference(avatar_component_clause,[],[f484])).
% 1.66/0.48 thf(f487,plain,(
% 1.66/0.48 spl27_81 | spl27_82),
% 1.66/0.48 inference(avatar_split_clause,[],[f102,f484,f480])).
% 1.66/0.48 thf(f489,definition,(
% 1.66/0.48 spl27_83 <=> ($true = sF20)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_83])],[avatar_definition])).
% 1.66/0.48 thf(f490,plain,(
% 1.66/0.48 ($true != sF20) | spl27_83),
% 1.66/0.48 inference(avatar_component_clause,[],[f489])).
% 1.66/0.48 thf(f491,plain,(
% 1.66/0.48 ($true = sF20) | ~spl27_83),
% 1.66/0.48 inference(avatar_component_clause,[],[f489])).
% 1.66/0.48 thf(f493,definition,(
% 1.66/0.48 spl27_84 <=> ($false = ((f2 @ sF19)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_84])],[avatar_definition])).
% 1.66/0.48 thf(f494,plain,(
% 1.66/0.48 ($false != ((f2 @ sF19))) | spl27_84),
% 1.66/0.48 inference(avatar_component_clause,[],[f493])).
% 1.66/0.48 thf(f495,plain,(
% 1.66/0.48 ($false = ((f2 @ sF19))) | ~spl27_84),
% 1.66/0.48 inference(avatar_component_clause,[],[f493])).
% 1.66/0.48 thf(f496,plain,(
% 1.66/0.48 spl27_83 | spl27_84),
% 1.66/0.48 inference(avatar_split_clause,[],[f105,f493,f489])).
% 1.66/0.48 thf(f498,definition,(
% 1.66/0.48 spl27_85 <=> ($false = sF20)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_85])],[avatar_definition])).
% 1.66/0.48 thf(f500,plain,(
% 1.66/0.48 ($false = sF20) | ~spl27_85),
% 1.66/0.48 inference(avatar_component_clause,[],[f498])).
% 1.66/0.48 thf(f502,definition,(
% 1.66/0.48 spl27_86 <=> ($true = ((f2 @ sF19)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_86])],[avatar_definition])).
% 1.66/0.48 thf(f504,plain,(
% 1.66/0.48 ($true = ((f2 @ sF19))) | ~spl27_86),
% 1.66/0.48 inference(avatar_component_clause,[],[f502])).
% 1.66/0.48 thf(f505,plain,(
% 1.66/0.48 spl27_85 | spl27_86),
% 1.66/0.48 inference(avatar_split_clause,[],[f104,f502,f498])).
% 1.66/0.48 thf(f507,definition,(
% 1.66/0.48 spl27_87 <=> ($true = sF21)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_87])],[avatar_definition])).
% 1.66/0.48 thf(f508,plain,(
% 1.66/0.48 ($true != sF21) | spl27_87),
% 1.66/0.48 inference(avatar_component_clause,[],[f507])).
% 1.66/0.48 thf(f509,plain,(
% 1.66/0.48 ($true = sF21) | ~spl27_87),
% 1.66/0.48 inference(avatar_component_clause,[],[f507])).
% 1.66/0.48 thf(f511,definition,(
% 1.66/0.48 spl27_88 <=> ($false = ((f2 @ sF20)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_88])],[avatar_definition])).
% 1.66/0.48 thf(f512,plain,(
% 1.66/0.48 ($false != ((f2 @ sF20))) | spl27_88),
% 1.66/0.48 inference(avatar_component_clause,[],[f511])).
% 1.66/0.48 thf(f513,plain,(
% 1.66/0.48 ($false = ((f2 @ sF20))) | ~spl27_88),
% 1.66/0.48 inference(avatar_component_clause,[],[f511])).
% 1.66/0.48 thf(f514,plain,(
% 1.66/0.48 spl27_87 | spl27_88),
% 1.66/0.48 inference(avatar_split_clause,[],[f107,f511,f507])).
% 1.66/0.48 thf(f516,definition,(
% 1.66/0.48 spl27_89 <=> ($false = sF21)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_89])],[avatar_definition])).
% 1.66/0.48 thf(f518,plain,(
% 1.66/0.48 ($false = sF21) | ~spl27_89),
% 1.66/0.48 inference(avatar_component_clause,[],[f516])).
% 1.66/0.48 thf(f520,definition,(
% 1.66/0.48 spl27_90 <=> ($true = ((f2 @ sF20)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_90])],[avatar_definition])).
% 1.66/0.48 thf(f522,plain,(
% 1.66/0.48 ($true = ((f2 @ sF20))) | ~spl27_90),
% 1.66/0.48 inference(avatar_component_clause,[],[f520])).
% 1.66/0.48 thf(f523,plain,(
% 1.66/0.48 spl27_89 | spl27_90),
% 1.66/0.48 inference(avatar_split_clause,[],[f106,f520,f516])).
% 1.66/0.48 thf(f525,definition,(
% 1.66/0.48 spl27_91 <=> ($true = sF22)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_91])],[avatar_definition])).
% 1.66/0.48 thf(f527,plain,(
% 1.66/0.48 ($true = sF22) | ~spl27_91),
% 1.66/0.48 inference(avatar_component_clause,[],[f525])).
% 1.66/0.48 thf(f529,definition,(
% 1.66/0.48 spl27_92 <=> ($false = ((f2 @ sF21)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_92])],[avatar_definition])).
% 1.66/0.48 thf(f531,plain,(
% 1.66/0.48 ($false = ((f2 @ sF21))) | ~spl27_92),
% 1.66/0.48 inference(avatar_component_clause,[],[f529])).
% 1.66/0.48 thf(f532,plain,(
% 1.66/0.48 spl27_91 | spl27_92),
% 1.66/0.48 inference(avatar_split_clause,[],[f109,f529,f525])).
% 1.66/0.48 thf(f534,definition,(
% 1.66/0.48 spl27_93 <=> ($false = sF22)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_93])],[avatar_definition])).
% 1.66/0.48 thf(f536,plain,(
% 1.66/0.48 ($false = sF22) | ~spl27_93),
% 1.66/0.48 inference(avatar_component_clause,[],[f534])).
% 1.66/0.48 thf(f538,definition,(
% 1.66/0.48 spl27_94 <=> ($true = ((f2 @ sF21)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_94])],[avatar_definition])).
% 1.66/0.48 thf(f539,plain,(
% 1.66/0.48 ($true != ((f2 @ sF21))) | spl27_94),
% 1.66/0.48 inference(avatar_component_clause,[],[f538])).
% 1.66/0.48 thf(f540,plain,(
% 1.66/0.48 ($true = ((f2 @ sF21))) | ~spl27_94),
% 1.66/0.48 inference(avatar_component_clause,[],[f538])).
% 1.66/0.48 thf(f541,plain,(
% 1.66/0.48 spl27_93 | spl27_94),
% 1.66/0.48 inference(avatar_split_clause,[],[f108,f538,f534])).
% 1.66/0.48 thf(f543,definition,(
% 1.66/0.48 spl27_95 <=> ($true = sF23)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_95])],[avatar_definition])).
% 1.66/0.48 thf(f544,plain,(
% 1.66/0.48 ($true != sF23) | spl27_95),
% 1.66/0.48 inference(avatar_component_clause,[],[f543])).
% 1.66/0.48 thf(f545,plain,(
% 1.66/0.48 ($true = sF23) | ~spl27_95),
% 1.66/0.48 inference(avatar_component_clause,[],[f543])).
% 1.66/0.48 thf(f547,definition,(
% 1.66/0.48 spl27_96 <=> ($false = ((f1 @ sF22)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_96])],[avatar_definition])).
% 1.66/0.48 thf(f548,plain,(
% 1.66/0.48 ($false != ((f1 @ sF22))) | spl27_96),
% 1.66/0.48 inference(avatar_component_clause,[],[f547])).
% 1.66/0.48 thf(f549,plain,(
% 1.66/0.48 ($false = ((f1 @ sF22))) | ~spl27_96),
% 1.66/0.48 inference(avatar_component_clause,[],[f547])).
% 1.66/0.48 thf(f550,plain,(
% 1.66/0.48 spl27_95 | spl27_96),
% 1.66/0.48 inference(avatar_split_clause,[],[f111,f547,f543])).
% 1.66/0.48 thf(f552,definition,(
% 1.66/0.48 spl27_97 <=> ($false = sF23)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_97])],[avatar_definition])).
% 1.66/0.48 thf(f553,plain,(
% 1.66/0.48 ($false != sF23) | spl27_97),
% 1.66/0.48 inference(avatar_component_clause,[],[f552])).
% 1.66/0.48 thf(f554,plain,(
% 1.66/0.48 ($false = sF23) | ~spl27_97),
% 1.66/0.48 inference(avatar_component_clause,[],[f552])).
% 1.66/0.48 thf(f556,definition,(
% 1.66/0.48 spl27_98 <=> ($true = ((f1 @ sF22)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_98])],[avatar_definition])).
% 1.66/0.48 thf(f557,plain,(
% 1.66/0.48 ($true != ((f1 @ sF22))) | spl27_98),
% 1.66/0.48 inference(avatar_component_clause,[],[f556])).
% 1.66/0.48 thf(f558,plain,(
% 1.66/0.48 ($true = ((f1 @ sF22))) | ~spl27_98),
% 1.66/0.48 inference(avatar_component_clause,[],[f556])).
% 1.66/0.48 thf(f559,plain,(
% 1.66/0.48 spl27_97 | spl27_98),
% 1.66/0.48 inference(avatar_split_clause,[],[f110,f556,f552])).
% 1.66/0.48 thf(f561,definition,(
% 1.66/0.48 spl27_99 <=> ($true = sF24)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_99])],[avatar_definition])).
% 1.66/0.48 thf(f563,plain,(
% 1.66/0.48 ($true = sF24) | ~spl27_99),
% 1.66/0.48 inference(avatar_component_clause,[],[f561])).
% 1.66/0.48 thf(f565,definition,(
% 1.66/0.48 spl27_100 <=> ($false = ((f0 @ sF23)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_100])],[avatar_definition])).
% 1.66/0.48 thf(f566,plain,(
% 1.66/0.48 ($false != ((f0 @ sF23))) | spl27_100),
% 1.66/0.48 inference(avatar_component_clause,[],[f565])).
% 1.66/0.48 thf(f567,plain,(
% 1.66/0.48 ($false = ((f0 @ sF23))) | ~spl27_100),
% 1.66/0.48 inference(avatar_component_clause,[],[f565])).
% 1.66/0.48 thf(f568,plain,(
% 1.66/0.48 spl27_99 | spl27_100),
% 1.66/0.48 inference(avatar_split_clause,[],[f113,f565,f561])).
% 1.66/0.48 thf(f570,definition,(
% 1.66/0.48 spl27_101 <=> ($false = sF24)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_101])],[avatar_definition])).
% 1.66/0.48 thf(f572,plain,(
% 1.66/0.48 ($false = sF24) | ~spl27_101),
% 1.66/0.48 inference(avatar_component_clause,[],[f570])).
% 1.66/0.48 thf(f574,definition,(
% 1.66/0.48 spl27_102 <=> ($true = ((f0 @ sF23)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_102])],[avatar_definition])).
% 1.66/0.48 thf(f576,plain,(
% 1.66/0.48 ($true = ((f0 @ sF23))) | ~spl27_102),
% 1.66/0.48 inference(avatar_component_clause,[],[f574])).
% 1.66/0.48 thf(f577,plain,(
% 1.66/0.48 spl27_101 | spl27_102),
% 1.66/0.48 inference(avatar_split_clause,[],[f112,f574,f570])).
% 1.66/0.48 thf(f579,definition,(
% 1.66/0.48 spl27_103 <=> ($true = sF25)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_103])],[avatar_definition])).
% 1.66/0.48 thf(f580,plain,(
% 1.66/0.48 ($true != sF25) | spl27_103),
% 1.66/0.48 inference(avatar_component_clause,[],[f579])).
% 1.66/0.48 thf(f581,plain,(
% 1.66/0.48 ($true = sF25) | ~spl27_103),
% 1.66/0.48 inference(avatar_component_clause,[],[f579])).
% 1.66/0.48 thf(f583,definition,(
% 1.66/0.48 spl27_104 <=> ($false = ((f0 @ sF24)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_104])],[avatar_definition])).
% 1.66/0.48 thf(f585,plain,(
% 1.66/0.48 ($false = ((f0 @ sF24))) | ~spl27_104),
% 1.66/0.48 inference(avatar_component_clause,[],[f583])).
% 1.66/0.48 thf(f586,plain,(
% 1.66/0.48 spl27_103 | spl27_104),
% 1.66/0.48 inference(avatar_split_clause,[],[f115,f583,f579])).
% 1.66/0.48 thf(f588,definition,(
% 1.66/0.48 spl27_105 <=> ($false = sF25)),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_105])],[avatar_definition])).
% 1.66/0.48 thf(f590,plain,(
% 1.66/0.48 ($false = sF25) | ~spl27_105),
% 1.66/0.48 inference(avatar_component_clause,[],[f588])).
% 1.66/0.48 thf(f592,definition,(
% 1.66/0.48 spl27_106 <=> ($true = ((f0 @ sF24)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_106])],[avatar_definition])).
% 1.66/0.48 thf(f593,plain,(
% 1.66/0.48 ($true != ((f0 @ sF24))) | spl27_106),
% 1.66/0.48 inference(avatar_component_clause,[],[f592])).
% 1.66/0.48 thf(f594,plain,(
% 1.66/0.48 ($true = ((f0 @ sF24))) | ~spl27_106),
% 1.66/0.48 inference(avatar_component_clause,[],[f592])).
% 1.66/0.48 thf(f595,plain,(
% 1.66/0.48 spl27_105 | spl27_106),
% 1.66/0.48 inference(avatar_split_clause,[],[f114,f592,f588])).
% 1.66/0.48 thf(f597,definition,(
% 1.66/0.48 spl27_107 <=> ($false = ((f0 @ sF25)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_107])],[avatar_definition])).
% 1.66/0.48 thf(f599,plain,(
% 1.66/0.48 ($false = ((f0 @ sF25))) | ~spl27_107),
% 1.66/0.48 inference(avatar_component_clause,[],[f597])).
% 1.66/0.48 thf(f600,plain,(
% 1.66/0.48 spl27_3 | spl27_107),
% 1.66/0.48 inference(avatar_split_clause,[],[f117,f597,f128])).
% 1.66/0.48 thf(f602,definition,(
% 1.66/0.48 spl27_108 <=> ($true = ((f0 @ sF25)))),
% 1.66/0.48 introduced(definition,[new_symbols(definition,[spl27_108])],[avatar_definition])).
% 1.66/0.48 thf(f603,plain,(
% 1.66/0.48 ($true != ((f0 @ sF25))) | spl27_108),
% 1.66/0.48 inference(avatar_component_clause,[],[f602])).
% 1.66/0.48 thf(f604,plain,(
% 1.66/0.48 ($true = ((f0 @ sF25))) | ~spl27_108),
% 1.66/0.48 inference(avatar_component_clause,[],[f602])).
% 1.66/0.48 thf(f605,plain,(
% 1.66/0.48 spl27_1 | spl27_108),
% 1.66/0.48 inference(avatar_split_clause,[],[f116,f602,f119])).
% 1.66/0.48 thf(f606,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_2 | ~spl27_4)),
% 1.66/0.48 inference(forward_demodulation,[],[f134,f125])).
% 1.66/0.48 thf(f607,plain,(
% 1.66/0.48 $false | (~spl27_2 | ~spl27_4)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f606])).
% 1.66/0.48 thf(f608,plain,(
% 1.66/0.48 ~spl27_2 | ~spl27_4),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f607])).
% 1.66/0.48 thf(f609,plain,(
% 1.66/0.48 ($true = ((f0 @ $true))) | (~spl27_103 | ~spl27_108)),
% 1.66/0.48 inference(forward_demodulation,[],[f604,f581])).
% 1.66/0.48 thf(f611,plain,(
% 1.66/0.48 ($false = ((f0 @ $true))) | (~spl27_49 | ~spl27_53)),
% 1.66/0.48 inference(forward_demodulation,[],[f355,f337])).
% 1.66/0.48 thf(f622,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_5 | ~spl27_7)),
% 1.66/0.48 inference(constrained_superposition,[],[f148,f139])).
% 1.66/0.48 thf(f626,plain,(
% 1.66/0.48 $false | (~spl27_5 | ~spl27_7)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f622])).
% 1.66/0.48 thf(f627,plain,(
% 1.66/0.48 ~spl27_5 | ~spl27_7),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f626])).
% 1.66/0.48 thf(f631,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_9 | ~spl27_11)),
% 1.66/0.48 inference(constrained_superposition,[],[f166,f157])).
% 1.66/0.48 thf(f635,plain,(
% 1.66/0.48 $false | (~spl27_9 | ~spl27_11)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f631])).
% 1.66/0.48 thf(f636,plain,(
% 1.66/0.48 ~spl27_9 | ~spl27_11),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f635])).
% 1.66/0.48 thf(f641,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_13 | ~spl27_15)),
% 1.66/0.48 inference(constrained_superposition,[],[f184,f175])).
% 1.66/0.48 thf(f645,plain,(
% 1.66/0.48 $false | (~spl27_13 | ~spl27_15)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f641])).
% 1.66/0.48 thf(f646,plain,(
% 1.66/0.48 ~spl27_13 | ~spl27_15),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f645])).
% 1.66/0.48 thf(f649,plain,(
% 1.66/0.48 ($false = ((f5 @ $true))) | (~spl27_9 | ~spl27_14)),
% 1.66/0.48 inference(forward_demodulation,[],[f179,f157])).
% 1.66/0.48 thf(f651,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_17 | ~spl27_19)),
% 1.66/0.48 inference(constrained_superposition,[],[f202,f193])).
% 1.66/0.48 thf(f655,plain,(
% 1.66/0.48 $false | (~spl27_17 | ~spl27_19)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f651])).
% 1.66/0.48 thf(f656,plain,(
% 1.66/0.48 ~spl27_17 | ~spl27_19),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f655])).
% 1.66/0.48 thf(f659,plain,(
% 1.66/0.48 ($false = ((f5 @ $false))) | (~spl27_15 | ~spl27_18)),
% 1.66/0.48 inference(forward_demodulation,[],[f197,f184])).
% 1.66/0.48 thf(f661,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_21 | ~spl27_23)),
% 1.66/0.48 inference(constrained_superposition,[],[f220,f211])).
% 1.66/0.48 thf(f665,plain,(
% 1.66/0.48 $false | (~spl27_21 | ~spl27_23)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f661])).
% 1.66/0.48 thf(f666,plain,(
% 1.66/0.48 ~spl27_21 | ~spl27_23),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f665])).
% 1.66/0.48 thf(f669,plain,(
% 1.66/0.48 ($false = ((f4 @ $false))) | (~spl27_19 | ~spl27_22)),
% 1.66/0.48 inference(forward_demodulation,[],[f215,f202])).
% 1.66/0.48 thf(f671,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_25 | ~spl27_27)),
% 1.66/0.48 inference(constrained_superposition,[],[f238,f229])).
% 1.66/0.48 thf(f675,plain,(
% 1.66/0.48 $false | (~spl27_25 | ~spl27_27)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f671])).
% 1.66/0.48 thf(f676,plain,(
% 1.66/0.48 ~spl27_25 | ~spl27_27),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f675])).
% 1.66/0.48 thf(f679,plain,(
% 1.66/0.48 ($false = ((f3 @ $false))) | (~spl27_23 | ~spl27_26)),
% 1.66/0.48 inference(forward_demodulation,[],[f233,f220])).
% 1.66/0.48 thf(f681,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_29 | ~spl27_31)),
% 1.66/0.48 inference(constrained_superposition,[],[f256,f247])).
% 1.66/0.48 thf(f685,plain,(
% 1.66/0.48 $false | (~spl27_29 | ~spl27_31)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f681])).
% 1.66/0.48 thf(f686,plain,(
% 1.66/0.48 ~spl27_29 | ~spl27_31),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f685])).
% 1.66/0.48 thf(f689,plain,(
% 1.66/0.48 ($false = ((f3 @ $false))) | (~spl27_27 | ~spl27_30)),
% 1.66/0.48 inference(forward_demodulation,[],[f251,f238])).
% 1.66/0.48 thf(f701,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_37 | ~spl27_39)),
% 1.66/0.48 inference(constrained_superposition,[],[f292,f283])).
% 1.66/0.48 thf(f705,plain,(
% 1.66/0.48 $false | (~spl27_37 | ~spl27_39)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f701])).
% 1.66/0.48 thf(f706,plain,(
% 1.66/0.48 ~spl27_37 | ~spl27_39),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f705])).
% 1.66/0.48 thf(f709,plain,(
% 1.66/0.48 ($false = ((f2 @ $false))) | (~spl27_35 | ~spl27_38)),
% 1.66/0.48 inference(forward_demodulation,[],[f287,f274])).
% 1.66/0.48 thf(f711,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_41 | ~spl27_43)),
% 1.66/0.48 inference(constrained_superposition,[],[f310,f301])).
% 1.66/0.48 thf(f715,plain,(
% 1.66/0.48 $false | (~spl27_41 | ~spl27_43)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f711])).
% 1.66/0.48 thf(f716,plain,(
% 1.66/0.48 ~spl27_41 | ~spl27_43),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f715])).
% 1.66/0.48 thf(f719,plain,(
% 1.66/0.48 ($false = ((f1 @ $false))) | (~spl27_39 | ~spl27_42)),
% 1.66/0.48 inference(forward_demodulation,[],[f305,f292])).
% 1.66/0.48 thf(f729,plain,(
% 1.66/0.48 ($false = ((f1 @ $false))) | (~spl27_43 | ~spl27_46)),
% 1.66/0.48 inference(forward_demodulation,[],[f323,f310])).
% 1.66/0.48 thf(f739,plain,(
% 1.66/0.48 ($false = ((f1 @ $false))) | (~spl27_47 | ~spl27_50)),
% 1.66/0.48 inference(forward_demodulation,[],[f341,f328])).
% 1.66/0.48 thf(f740,plain,(
% 1.66/0.48 ($false = ((f0 @ $false))) | (~spl27_51 | ~spl27_53)),
% 1.66/0.48 inference(forward_demodulation,[],[f355,f346])).
% 1.66/0.48 thf(f742,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_55 | ~spl27_57)),
% 1.66/0.48 inference(constrained_superposition,[],[f374,f365])).
% 1.66/0.48 thf(f746,plain,(
% 1.66/0.48 $false | (~spl27_55 | ~spl27_57)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f742])).
% 1.66/0.48 thf(f747,plain,(
% 1.66/0.48 ~spl27_55 | ~spl27_57),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f746])).
% 1.66/0.48 thf(f750,plain,(
% 1.66/0.48 ($false = ((f6 @ $true))) | (~spl27_5 | ~spl27_56)),
% 1.66/0.48 inference(forward_demodulation,[],[f369,f139])).
% 1.66/0.48 thf(f752,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_59 | ~spl27_61)),
% 1.66/0.48 inference(constrained_superposition,[],[f392,f383])).
% 1.66/0.48 thf(f756,plain,(
% 1.66/0.48 $false | (~spl27_59 | ~spl27_61)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f752])).
% 1.66/0.48 thf(f757,plain,(
% 1.66/0.48 ~spl27_59 | ~spl27_61),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f756])).
% 1.66/0.48 thf(f760,plain,(
% 1.66/0.48 ($false = ((f6 @ $false))) | (~spl27_57 | ~spl27_60)),
% 1.66/0.48 inference(forward_demodulation,[],[f387,f374])).
% 1.66/0.48 thf(f800,plain,(
% 1.66/0.48 ($false = ((f4 @ $false))) | (~spl27_73 | ~spl27_76)),
% 1.66/0.48 inference(forward_demodulation,[],[f459,f446])).
% 1.66/0.48 thf(f810,plain,(
% 1.66/0.48 ($false = ((f3 @ $false))) | (~spl27_77 | ~spl27_80)),
% 1.66/0.48 inference(forward_demodulation,[],[f477,f464])).
% 1.66/0.48 thf(f820,plain,(
% 1.66/0.48 ($false = ((f2 @ $false))) | (~spl27_81 | ~spl27_84)),
% 1.66/0.48 inference(forward_demodulation,[],[f495,f482])).
% 1.66/0.48 thf(f822,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_87 | ~spl27_89)),
% 1.66/0.48 inference(constrained_superposition,[],[f518,f509])).
% 1.66/0.48 thf(f826,plain,(
% 1.66/0.48 $false | (~spl27_87 | ~spl27_89)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f822])).
% 1.66/0.48 thf(f827,plain,(
% 1.66/0.48 ~spl27_87 | ~spl27_89),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f826])).
% 1.66/0.48 thf(f830,plain,(
% 1.66/0.48 ($false = ((f2 @ $false))) | (~spl27_85 | ~spl27_88)),
% 1.66/0.48 inference(forward_demodulation,[],[f513,f500])).
% 1.66/0.48 thf(f842,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_95 | ~spl27_97)),
% 1.66/0.48 inference(constrained_superposition,[],[f554,f545])).
% 1.66/0.48 thf(f846,plain,(
% 1.66/0.48 $false | (~spl27_95 | ~spl27_97)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f842])).
% 1.66/0.48 thf(f847,plain,(
% 1.66/0.48 ~spl27_95 | ~spl27_97),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f846])).
% 1.66/0.48 thf(f850,plain,(
% 1.66/0.48 ($false = ((f1 @ $false))) | (~spl27_93 | ~spl27_96)),
% 1.66/0.48 inference(forward_demodulation,[],[f549,f536])).
% 1.66/0.48 thf(f860,plain,(
% 1.66/0.48 ($false = ((f0 @ $false))) | (~spl27_97 | ~spl27_100)),
% 1.66/0.48 inference(forward_demodulation,[],[f567,f554])).
% 1.66/0.48 thf(f870,plain,(
% 1.66/0.48 ($false = ((f0 @ $false))) | (~spl27_101 | ~spl27_104)),
% 1.66/0.48 inference(forward_demodulation,[],[f585,f572])).
% 1.66/0.48 thf(f871,plain,(
% 1.66/0.48 ($true = ((f0 @ $false))) | (~spl27_105 | ~spl27_108)),
% 1.66/0.48 inference(forward_demodulation,[],[f604,f590])).
% 1.66/0.48 thf(f872,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_51 | ~spl27_53 | ~spl27_105 | ~spl27_108)),
% 1.66/0.48 inference(forward_demodulation,[],[f871,f740])).
% 1.66/0.48 thf(f873,plain,(
% 1.66/0.48 $false | (~spl27_51 | ~spl27_53 | ~spl27_105 | ~spl27_108)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f872])).
% 1.66/0.48 thf(f874,plain,(
% 1.66/0.48 ~spl27_51 | ~spl27_53 | ~spl27_105 | ~spl27_108),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f873])).
% 1.66/0.48 thf(f875,plain,(
% 1.66/0.48 ($true = ((f1 @ $false))) | (~spl27_47 | ~spl27_52)),
% 1.66/0.48 inference(forward_demodulation,[],[f350,f328])).
% 1.66/0.48 thf(f879,plain,(
% 1.66/0.48 ($true = $false) | (~spl27_39 | ~spl27_42 | ~spl27_47 | ~spl27_52)),
% 1.66/0.48 inference(forward_demodulation,[],[f875,f719])).
% 1.66/0.48 thf(f880,plain,(
% 1.66/0.48 $false | (~spl27_39 | ~spl27_42 | ~spl27_47 | ~spl27_52)),
% 1.66/0.48 inference(trivial_inequality_removal,[],[f879])).
% 1.66/0.48 thf(f881,plain,(
% 1.66/0.48 ~spl27_39 | ~spl27_42 | ~spl27_47 | ~spl27_52),
% 1.66/0.48 inference(avatar_contradiction_clause,[],[f880])).
% 1.66/0.48 thf(f882,plain,(
% 1.66/0.48 ($true = ((f2 @ $false))) | (~spl27_35 | ~spl27_40)),
% 1.66/0.48 inference(forward_demodulation,[],[f296,f274])).
% 1.66/0.48 thf(f883,plain,(
% 1.66/0.48 ($true = ((f1 @ $false))) | (~spl27_93 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f558,f536])).
% 1.66/0.49 thf(f884,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_101 | ~spl27_104 | ~spl27_105 | ~spl27_108)),
% 1.66/0.49 inference(forward_demodulation,[],[f871,f870])).
% 1.66/0.49 thf(f885,plain,(
% 1.66/0.49 $false | (~spl27_101 | ~spl27_104 | ~spl27_105 | ~spl27_108)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f884])).
% 1.66/0.49 thf(f886,plain,(
% 1.66/0.49 ~spl27_101 | ~spl27_104 | ~spl27_105 | ~spl27_108),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f885])).
% 1.66/0.49 thf(f887,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_43 | ~spl27_46 | ~spl27_47 | ~spl27_52)),
% 1.66/0.49 inference(forward_demodulation,[],[f875,f729])).
% 1.66/0.49 thf(f888,plain,(
% 1.66/0.49 $false | (~spl27_43 | ~spl27_46 | ~spl27_47 | ~spl27_52)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f887])).
% 1.66/0.49 thf(f889,plain,(
% 1.66/0.49 ~spl27_43 | ~spl27_46 | ~spl27_47 | ~spl27_52),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f888])).
% 1.66/0.49 thf(f893,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_43 | ~spl27_46 | ~spl27_93 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f883,f729])).
% 1.66/0.49 thf(f894,plain,(
% 1.66/0.49 $false | (~spl27_43 | ~spl27_46 | ~spl27_93 | ~spl27_98)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f893])).
% 1.66/0.49 thf(f895,plain,(
% 1.66/0.49 ~spl27_43 | ~spl27_46 | ~spl27_93 | ~spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f894])).
% 1.66/0.49 thf(f899,plain,(
% 1.66/0.49 ($true = ((f1 @ $false))) | (~spl27_39 | ~spl27_44)),
% 1.66/0.49 inference(forward_demodulation,[],[f314,f292])).
% 1.66/0.49 thf(f900,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_100 | ~spl27_102)),
% 1.66/0.49 inference(forward_demodulation,[],[f576,f567])).
% 1.66/0.49 thf(f901,plain,(
% 1.66/0.49 $false | (~spl27_100 | ~spl27_102)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f900])).
% 1.66/0.49 thf(f902,plain,(
% 1.66/0.49 ~spl27_100 | ~spl27_102),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f901])).
% 1.66/0.49 thf(f903,plain,(
% 1.66/0.49 ($false = ((f1 @ $true))) | (~spl27_41 | ~spl27_46)),
% 1.66/0.49 inference(forward_demodulation,[],[f323,f301])).
% 1.66/0.49 thf(f907,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_47 | ~spl27_50 | ~spl27_93 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f883,f739])).
% 1.66/0.49 thf(f908,plain,(
% 1.66/0.49 $false | (~spl27_47 | ~spl27_50 | ~spl27_93 | ~spl27_98)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f907])).
% 1.66/0.49 thf(f909,plain,(
% 1.66/0.49 ~spl27_47 | ~spl27_50 | ~spl27_93 | ~spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f908])).
% 1.66/0.49 thf(f913,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_39 | ~spl27_44 | ~spl27_47 | ~spl27_50)),
% 1.66/0.49 inference(forward_demodulation,[],[f899,f739])).
% 1.66/0.49 thf(f914,plain,(
% 1.66/0.49 $false | (~spl27_39 | ~spl27_44 | ~spl27_47 | ~spl27_50)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f913])).
% 1.66/0.49 thf(f915,plain,(
% 1.66/0.49 ~spl27_39 | ~spl27_44 | ~spl27_47 | ~spl27_50),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f914])).
% 1.66/0.49 thf(f925,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_39 | ~spl27_44 | ~spl27_93 | ~spl27_96)),
% 1.66/0.49 inference(forward_demodulation,[],[f899,f850])).
% 1.66/0.49 thf(f926,plain,(
% 1.66/0.49 $false | (~spl27_39 | ~spl27_44 | ~spl27_93 | ~spl27_96)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f925])).
% 1.66/0.49 thf(f927,plain,(
% 1.66/0.49 ~spl27_39 | ~spl27_44 | ~spl27_93 | ~spl27_96),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f926])).
% 1.66/0.49 thf(f933,plain,(
% 1.66/0.49 ($true = ((f2 @ $false))) | (~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f540,f518])).
% 1.66/0.49 thf(f934,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_96 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f558,f549])).
% 1.66/0.49 thf(f935,plain,(
% 1.66/0.49 $false | (~spl27_96 | ~spl27_98)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f934])).
% 1.66/0.49 thf(f936,plain,(
% 1.66/0.49 ~spl27_96 | ~spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f935])).
% 1.66/0.49 thf(f937,plain,(
% 1.66/0.49 ($true = ((f1 @ $true))) | (~spl27_45 | ~spl27_52)),
% 1.66/0.49 inference(forward_demodulation,[],[f350,f319])).
% 1.66/0.49 thf(f940,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_35 | ~spl27_38 | ~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f933,f709])).
% 1.66/0.49 thf(f941,plain,(
% 1.66/0.49 $false | (~spl27_35 | ~spl27_38 | ~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f940])).
% 1.66/0.49 thf(f942,plain,(
% 1.66/0.49 ~spl27_35 | ~spl27_38 | ~spl27_89 | ~spl27_94),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f941])).
% 1.66/0.49 thf(f943,plain,(
% 1.66/0.49 ($true = ((f2 @ $false))) | (~spl27_85 | ~spl27_90)),
% 1.66/0.49 inference(forward_demodulation,[],[f522,f500])).
% 1.66/0.49 thf(f944,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_92 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f540,f531])).
% 1.66/0.49 thf(f945,plain,(
% 1.66/0.49 $false | (~spl27_92 | ~spl27_94)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f944])).
% 1.66/0.49 thf(f946,plain,(
% 1.66/0.49 ~spl27_92 | ~spl27_94),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f945])).
% 1.66/0.49 thf(f947,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_35 | ~spl27_38 | ~spl27_85 | ~spl27_90)),
% 1.66/0.49 inference(forward_demodulation,[],[f943,f709])).
% 1.66/0.49 thf(f948,plain,(
% 1.66/0.49 $false | (~spl27_35 | ~spl27_38 | ~spl27_85 | ~spl27_90)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f947])).
% 1.66/0.49 thf(f949,plain,(
% 1.66/0.49 ~spl27_35 | ~spl27_38 | ~spl27_85 | ~spl27_90),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f948])).
% 1.66/0.49 thf(f950,plain,(
% 1.66/0.49 ($true = ((f2 @ $false))) | (~spl27_81 | ~spl27_86)),
% 1.66/0.49 inference(forward_demodulation,[],[f504,f482])).
% 1.66/0.49 thf(f951,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_88 | ~spl27_90)),
% 1.66/0.49 inference(forward_demodulation,[],[f522,f513])).
% 1.66/0.49 thf(f952,plain,(
% 1.66/0.49 $false | (~spl27_88 | ~spl27_90)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f951])).
% 1.66/0.49 thf(f953,plain,(
% 1.66/0.49 ~spl27_88 | ~spl27_90),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f952])).
% 1.66/0.49 thf(f954,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_35 | ~spl27_38 | ~spl27_81 | ~spl27_86)),
% 1.66/0.49 inference(forward_demodulation,[],[f950,f709])).
% 1.66/0.49 thf(f955,plain,(
% 1.66/0.49 $false | (~spl27_35 | ~spl27_38 | ~spl27_81 | ~spl27_86)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f954])).
% 1.66/0.49 thf(f956,plain,(
% 1.66/0.49 ~spl27_35 | ~spl27_38 | ~spl27_81 | ~spl27_86),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f955])).
% 1.66/0.49 thf(f957,plain,(
% 1.66/0.49 ($true = ((f3 @ $false))) | (~spl27_77 | ~spl27_82)),
% 1.66/0.49 inference(forward_demodulation,[],[f486,f464])).
% 1.66/0.49 thf(f961,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_23 | ~spl27_26 | ~spl27_77 | ~spl27_82)),
% 1.66/0.49 inference(forward_demodulation,[],[f957,f679])).
% 1.66/0.49 thf(f962,plain,(
% 1.66/0.49 $false | (~spl27_23 | ~spl27_26 | ~spl27_77 | ~spl27_82)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f961])).
% 1.66/0.49 thf(f963,plain,(
% 1.66/0.49 ~spl27_23 | ~spl27_26 | ~spl27_77 | ~spl27_82),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f962])).
% 1.66/0.49 thf(f964,plain,(
% 1.66/0.49 ($true = ((f4 @ $false))) | (~spl27_73 | ~spl27_78)),
% 1.66/0.49 inference(forward_demodulation,[],[f468,f446])).
% 1.66/0.49 thf(f965,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_80 | ~spl27_82)),
% 1.66/0.49 inference(forward_demodulation,[],[f486,f477])).
% 1.66/0.49 thf(f966,plain,(
% 1.66/0.49 $false | (~spl27_80 | ~spl27_82)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f965])).
% 1.66/0.49 thf(f967,plain,(
% 1.66/0.49 ~spl27_80 | ~spl27_82),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f966])).
% 1.66/0.49 thf(f968,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_19 | ~spl27_22 | ~spl27_73 | ~spl27_78)),
% 1.66/0.49 inference(forward_demodulation,[],[f964,f669])).
% 1.66/0.49 thf(f969,plain,(
% 1.66/0.49 $false | (~spl27_19 | ~spl27_22 | ~spl27_73 | ~spl27_78)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f968])).
% 1.66/0.49 thf(f970,plain,(
% 1.66/0.49 ~spl27_19 | ~spl27_22 | ~spl27_73 | ~spl27_78),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f969])).
% 1.66/0.49 thf(f971,plain,(
% 1.66/0.49 ($true = ((f4 @ $false))) | (~spl27_69 | ~spl27_74)),
% 1.66/0.49 inference(forward_demodulation,[],[f450,f428])).
% 1.66/0.49 thf(f972,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_76 | ~spl27_78)),
% 1.66/0.49 inference(forward_demodulation,[],[f468,f459])).
% 1.66/0.49 thf(f973,plain,(
% 1.66/0.49 $false | (~spl27_76 | ~spl27_78)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f972])).
% 1.66/0.49 thf(f974,plain,(
% 1.66/0.49 ~spl27_76 | ~spl27_78),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f973])).
% 1.66/0.49 thf(f978,plain,(
% 1.66/0.49 ($true = ((f4 @ $false))) | (~spl27_65 | ~spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f432,f410])).
% 1.66/0.49 thf(f979,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_72 | ~spl27_74)),
% 1.66/0.49 inference(forward_demodulation,[],[f450,f441])).
% 1.66/0.49 thf(f980,plain,(
% 1.66/0.49 $false | (~spl27_72 | ~spl27_74)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f979])).
% 1.66/0.49 thf(f981,plain,(
% 1.66/0.49 ~spl27_72 | ~spl27_74),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f980])).
% 1.66/0.49 thf(f982,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_19 | ~spl27_22 | ~spl27_65 | ~spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f978,f669])).
% 1.66/0.49 thf(f983,plain,(
% 1.66/0.49 $false | (~spl27_19 | ~spl27_22 | ~spl27_65 | ~spl27_70)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f982])).
% 1.66/0.49 thf(f984,plain,(
% 1.66/0.49 ~spl27_19 | ~spl27_22 | ~spl27_65 | ~spl27_70),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f983])).
% 1.66/0.49 thf(f985,plain,(
% 1.66/0.49 ($true = ((f5 @ $false))) | (~spl27_61 | ~spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f414,f392])).
% 1.66/0.49 thf(f986,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_68 | ~spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f432,f423])).
% 1.66/0.49 thf(f987,plain,(
% 1.66/0.49 $false | (~spl27_68 | ~spl27_70)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f986])).
% 1.66/0.49 thf(f988,plain,(
% 1.66/0.49 ~spl27_68 | ~spl27_70),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f987])).
% 1.66/0.49 thf(f989,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_15 | ~spl27_18 | ~spl27_61 | ~spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f985,f659])).
% 1.66/0.49 thf(f990,plain,(
% 1.66/0.49 $false | (~spl27_15 | ~spl27_18 | ~spl27_61 | ~spl27_66)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f989])).
% 1.66/0.49 thf(f991,plain,(
% 1.66/0.49 ~spl27_15 | ~spl27_18 | ~spl27_61 | ~spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f990])).
% 1.66/0.49 thf(f993,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_64 | ~spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f414,f405])).
% 1.66/0.49 thf(f994,plain,(
% 1.66/0.49 $false | (~spl27_64 | ~spl27_66)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f993])).
% 1.66/0.49 thf(f995,plain,(
% 1.66/0.49 ~spl27_64 | ~spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f994])).
% 1.66/0.49 thf(f1004,plain,(
% 1.66/0.49 ($true != ((f4 @ $false))) | (~spl27_69 | spl27_74)),
% 1.66/0.49 inference(forward_demodulation,[],[f449,f428])).
% 1.66/0.49 thf(f1014,plain,(
% 1.66/0.49 ($true != ((f2 @ $false))) | (~spl27_89 | spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f539,f518])).
% 1.66/0.49 thf(f1023,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF8) | spl27_37),
% 1.66/0.49 inference(constrained_superposition,[],[f282,f6])).
% 1.66/0.49 thf(f1024,plain,(
% 1.66/0.49 ($false = sF8) | spl27_37),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1023])).
% 1.66/0.49 thf(f1032,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF14) | spl27_59),
% 1.66/0.49 inference(constrained_superposition,[],[f382,f6])).
% 1.66/0.49 thf(f1033,plain,(
% 1.66/0.49 ($false = sF14) | spl27_59),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1032])).
% 1.66/0.49 thf(f1042,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF16) | spl27_67),
% 1.66/0.49 inference(constrained_superposition,[],[f418,f6])).
% 1.66/0.49 thf(f1043,plain,(
% 1.66/0.49 ($false = sF16) | spl27_67),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1042])).
% 1.66/0.49 thf(f1047,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF17) | spl27_71),
% 1.66/0.49 inference(constrained_superposition,[],[f436,f6])).
% 1.66/0.49 thf(f1048,plain,(
% 1.66/0.49 ($false = sF17) | spl27_71),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1047])).
% 1.66/0.49 thf(f1062,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF20) | spl27_83),
% 1.66/0.49 inference(constrained_superposition,[],[f490,f6])).
% 1.66/0.49 thf(f1063,plain,(
% 1.66/0.49 ($false = sF20) | spl27_83),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1062])).
% 1.66/0.49 thf(f1067,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF21) | spl27_87),
% 1.66/0.49 inference(constrained_superposition,[],[f508,f6])).
% 1.66/0.49 thf(f1068,plain,(
% 1.66/0.49 ($false = sF21) | spl27_87),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1067])).
% 1.66/0.49 thf(f1081,plain,(
% 1.66/0.49 ($true = ((f6 @ $true))) | (x = $false) | ~spl27_8),
% 1.66/0.49 inference(constrained_superposition,[],[f152,f6])).
% 1.66/0.49 thf(f1082,plain,(
% 1.66/0.49 ($true = $false) | (x = $false) | (~spl27_5 | ~spl27_8 | ~spl27_56)),
% 1.66/0.49 inference(forward_demodulation,[],[f1081,f750])).
% 1.66/0.49 thf(f1083,plain,(
% 1.66/0.49 (x = $false) | (~spl27_5 | ~spl27_8 | ~spl27_56)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1082])).
% 1.66/0.49 thf(f1085,plain,(
% 1.66/0.49 ($true = ((f6 @ $false))) | (~spl27_5 | ~spl27_8 | ~spl27_56)),
% 1.66/0.49 inference(constrained_superposition,[],[f152,f1083])).
% 1.66/0.49 thf(f1087,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_5 | ~spl27_8 | ~spl27_56 | ~spl27_57 | ~spl27_60)),
% 1.66/0.49 inference(forward_demodulation,[],[f1085,f760])).
% 1.66/0.49 thf(f1088,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_8 | ~spl27_56 | ~spl27_57 | ~spl27_60)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1087])).
% 1.66/0.49 thf(f1089,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_8 | ~spl27_56 | ~spl27_57 | ~spl27_60),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1088])).
% 1.66/0.49 thf(f1090,plain,(
% 1.66/0.49 ($true = ((f5 @ $false))) | (~spl27_7 | ~spl27_12)),
% 1.66/0.49 inference(forward_demodulation,[],[f170,f148])).
% 1.66/0.49 thf(f1091,plain,(
% 1.66/0.49 ($false = ((f6 @ $false))) | (~spl27_7 | ~spl27_56)),
% 1.66/0.49 inference(forward_demodulation,[],[f369,f148])).
% 1.66/0.49 thf(f1095,plain,(
% 1.66/0.49 ($false = ((f5 @ $false))) | (~spl27_7 | ~spl27_10)),
% 1.66/0.49 inference(forward_demodulation,[],[f161,f148])).
% 1.66/0.49 thf(f1096,plain,(
% 1.66/0.49 ($true != ((f5 @ $false))) | (~spl27_7 | spl27_12)),
% 1.66/0.49 inference(forward_demodulation,[],[f169,f148])).
% 1.66/0.49 thf(f1099,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF0) | spl27_5),
% 1.66/0.49 inference(constrained_superposition,[],[f138,f6])).
% 1.66/0.49 thf(f1100,plain,(
% 1.66/0.49 ($false = sF0) | spl27_5),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1099])).
% 1.66/0.49 thf(f1104,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF1) | spl27_9),
% 1.66/0.49 inference(constrained_superposition,[],[f156,f6])).
% 1.66/0.49 thf(f1105,plain,(
% 1.66/0.49 ($false = sF1) | spl27_9),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1104])).
% 1.66/0.49 thf(f1109,plain,(
% 1.66/0.49 ($false = ((f6 @ $true))) | (x = $false) | ~spl27_6),
% 1.66/0.49 inference(constrained_superposition,[],[f143,f6])).
% 1.66/0.49 thf(f1113,definition,(
% 1.66/0.49 spl27_109 <=> (x = $false)),
% 1.66/0.49 introduced(definition,[new_symbols(definition,[spl27_109])],[avatar_definition])).
% 1.66/0.49 thf(f1115,plain,(
% 1.66/0.49 (x = $false) | ~spl27_109),
% 1.66/0.49 inference(avatar_component_clause,[],[f1113])).
% 1.66/0.49 thf(f1117,definition,(
% 1.66/0.49 spl27_110 <=> ($false = ((f6 @ $true)))),
% 1.66/0.49 introduced(definition,[new_symbols(definition,[spl27_110])],[avatar_definition])).
% 1.66/0.49 thf(f1119,plain,(
% 1.66/0.49 ($false = ((f6 @ $true))) | ~spl27_110),
% 1.66/0.49 inference(avatar_component_clause,[],[f1117])).
% 1.66/0.49 thf(f1120,plain,(
% 1.66/0.49 spl27_109 | spl27_110 | ~spl27_6),
% 1.66/0.49 inference(avatar_split_clause,[],[f1109,f141,f1117,f1113])).
% 1.66/0.49 thf(f1135,plain,(
% 1.66/0.49 ($false != ((f0 @ $true))) | ($false = sF23) | spl27_100),
% 1.66/0.49 inference(constrained_superposition,[],[f566,f6])).
% 1.66/0.49 thf(f1136,plain,(
% 1.66/0.49 ($false != ((f0 @ $true))) | (~spl27_95 | spl27_100)),
% 1.66/0.49 inference(constrained_superposition,[],[f566,f545])).
% 1.66/0.49 thf(f1140,plain,(
% 1.66/0.49 ($false = sF23) | (~spl27_49 | ~spl27_53 | spl27_100)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1135,f611])).
% 1.66/0.49 thf(f1141,plain,(
% 1.66/0.49 $false | (~spl27_49 | ~spl27_53 | spl27_97 | spl27_100)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1140,f553])).
% 1.66/0.49 thf(f1142,plain,(
% 1.66/0.49 ~spl27_49 | ~spl27_53 | spl27_97 | spl27_100),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1141])).
% 1.66/0.49 thf(f1143,plain,(
% 1.66/0.49 ($false = ((f0 @ $true))) | (~spl27_95 | ~spl27_100)),
% 1.66/0.49 inference(forward_demodulation,[],[f567,f545])).
% 1.66/0.49 thf(f1145,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_104 | ~spl27_106)),
% 1.66/0.49 inference(forward_demodulation,[],[f594,f585])).
% 1.66/0.49 thf(f1146,plain,(
% 1.66/0.49 $false | (~spl27_104 | ~spl27_106)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1145])).
% 1.66/0.49 thf(f1147,plain,(
% 1.66/0.49 ~spl27_104 | ~spl27_106),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1146])).
% 1.66/0.49 thf(f1149,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_49 | ~spl27_53 | ~spl27_103 | ~spl27_108)),
% 1.66/0.49 inference(forward_demodulation,[],[f609,f611])).
% 1.66/0.49 thf(f1150,plain,(
% 1.66/0.49 $false | (~spl27_49 | ~spl27_53 | ~spl27_103 | ~spl27_108)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1149])).
% 1.66/0.49 thf(f1151,plain,(
% 1.66/0.49 ~spl27_49 | ~spl27_53 | ~spl27_103 | ~spl27_108),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1150])).
% 1.66/0.49 thf(f1155,plain,(
% 1.66/0.49 ($true = ((f0 @ $true))) | (~spl27_49 | ~spl27_54)),
% 1.66/0.49 inference(forward_demodulation,[],[f360,f337])).
% 1.66/0.49 thf(f1162,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_49 | ~spl27_54 | ~spl27_95 | ~spl27_100)),
% 1.66/0.49 inference(forward_demodulation,[],[f1155,f1143])).
% 1.66/0.49 thf(f1163,plain,(
% 1.66/0.49 $false | (~spl27_49 | ~spl27_54 | ~spl27_95 | ~spl27_100)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1162])).
% 1.66/0.49 thf(f1164,plain,(
% 1.66/0.49 ~spl27_49 | ~spl27_54 | ~spl27_95 | ~spl27_100),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1163])).
% 1.66/0.49 thf(f1169,plain,(
% 1.66/0.49 ($true = ((f0 @ $true))) | (~spl27_99 | ~spl27_106)),
% 1.66/0.49 inference(forward_demodulation,[],[f594,f563])).
% 1.66/0.49 thf(f1171,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_1 | ~spl27_3)),
% 1.66/0.49 inference(constrained_superposition,[],[f121,f130])).
% 1.66/0.49 thf(f1175,plain,(
% 1.66/0.49 $false | (~spl27_1 | ~spl27_3)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1171])).
% 1.66/0.49 thf(f1176,plain,(
% 1.66/0.49 ~spl27_1 | ~spl27_3),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1175])).
% 1.66/0.49 thf(f1179,plain,(
% 1.66/0.49 ($false = ((f0 @ $true))) | (~spl27_103 | ~spl27_107)),
% 1.66/0.49 inference(forward_demodulation,[],[f599,f581])).
% 1.66/0.49 thf(f1180,plain,(
% 1.66/0.49 $false | (~spl27_95 | spl27_100 | ~spl27_103 | ~spl27_107)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1179,f1136])).
% 1.66/0.49 thf(f1181,plain,(
% 1.66/0.49 ~spl27_95 | spl27_100 | ~spl27_103 | ~spl27_107),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1180])).
% 1.66/0.49 thf(f1182,plain,(
% 1.66/0.49 ($false != ((f2 @ $false))) | (~spl27_35 | spl27_38)),
% 1.66/0.49 inference(forward_demodulation,[],[f286,f274])).
% 1.66/0.49 thf(f1187,plain,(
% 1.66/0.49 ($false != ((f0 @ $false))) | (~spl27_97 | spl27_100)),
% 1.66/0.49 inference(forward_demodulation,[],[f566,f554])).
% 1.66/0.49 thf(f1192,plain,(
% 1.66/0.49 ($true = ((f1 @ $true))) | (~spl27_37 | ~spl27_44)),
% 1.66/0.49 inference(forward_demodulation,[],[f314,f283])).
% 1.66/0.49 thf(f1197,plain,(
% 1.66/0.49 $false | (~spl27_35 | ~spl27_40 | ~spl27_89 | spl27_94)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1014,f882])).
% 1.66/0.49 thf(f1198,plain,(
% 1.66/0.49 ~spl27_35 | ~spl27_40 | ~spl27_89 | spl27_94),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1197])).
% 1.66/0.49 thf(f1199,plain,(
% 1.66/0.49 $false | (~spl27_35 | spl27_38 | ~spl27_81 | ~spl27_84)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1182,f820])).
% 1.66/0.49 thf(f1200,plain,(
% 1.66/0.49 ~spl27_35 | spl27_38 | ~spl27_81 | ~spl27_84),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1199])).
% 1.66/0.49 thf(f1203,plain,(
% 1.66/0.49 spl27_39 | spl27_37),
% 1.66/0.49 inference(avatar_split_clause,[],[f1024,f281,f290])).
% 1.66/0.49 thf(f1209,plain,(
% 1.66/0.49 ($true = ((f1 @ $false))) | (~spl27_43 | ~spl27_48)),
% 1.66/0.49 inference(forward_demodulation,[],[f332,f310])).
% 1.66/0.49 thf(f1210,plain,(
% 1.66/0.49 ($false != ((f1 @ $false))) | (~spl27_43 | spl27_46)),
% 1.66/0.49 inference(forward_demodulation,[],[f322,f310])).
% 1.66/0.49 thf(f1221,plain,(
% 1.66/0.49 ($true = ((f3 @ $false))) | (~spl27_31 | ~spl27_36)),
% 1.66/0.49 inference(forward_demodulation,[],[f278,f256])).
% 1.66/0.49 thf(f1225,plain,(
% 1.66/0.49 ($false = ((f1 @ $true))) | (~spl27_37 | ~spl27_42)),
% 1.66/0.49 inference(forward_demodulation,[],[f305,f283])).
% 1.66/0.49 thf(f1226,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_23 | ~spl27_26 | ~spl27_31 | ~spl27_36)),
% 1.66/0.49 inference(forward_demodulation,[],[f1221,f679])).
% 1.66/0.49 thf(f1227,plain,(
% 1.66/0.49 $false | (~spl27_23 | ~spl27_26 | ~spl27_31 | ~spl27_36)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1226])).
% 1.66/0.49 thf(f1228,plain,(
% 1.66/0.49 ~spl27_23 | ~spl27_26 | ~spl27_31 | ~spl27_36),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1227])).
% 1.66/0.49 thf(f1231,plain,(
% 1.66/0.49 ($true = ((f3 @ $false))) | (~spl27_27 | ~spl27_32)),
% 1.66/0.49 inference(forward_demodulation,[],[f260,f238])).
% 1.66/0.49 thf(f1232,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_34 | ~spl27_36)),
% 1.66/0.49 inference(forward_demodulation,[],[f278,f269])).
% 1.66/0.49 thf(f1233,plain,(
% 1.66/0.49 $false | (~spl27_34 | ~spl27_36)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1232])).
% 1.66/0.49 thf(f1234,plain,(
% 1.66/0.49 ~spl27_34 | ~spl27_36),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1233])).
% 1.66/0.49 thf(f1235,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_23 | ~spl27_26 | ~spl27_27 | ~spl27_32)),
% 1.66/0.49 inference(forward_demodulation,[],[f1231,f679])).
% 1.66/0.49 thf(f1236,plain,(
% 1.66/0.49 $false | (~spl27_23 | ~spl27_26 | ~spl27_27 | ~spl27_32)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1235])).
% 1.66/0.49 thf(f1237,plain,(
% 1.66/0.49 ~spl27_23 | ~spl27_26 | ~spl27_27 | ~spl27_32),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1236])).
% 1.66/0.49 thf(f1239,plain,(
% 1.66/0.49 ($true = ((f3 @ $false))) | (~spl27_23 | ~spl27_28)),
% 1.66/0.49 inference(forward_demodulation,[],[f242,f220])).
% 1.66/0.49 thf(f1240,plain,(
% 1.66/0.49 ($false = ((f3 @ $true))) | (~spl27_25 | ~spl27_30)),
% 1.66/0.49 inference(forward_demodulation,[],[f251,f229])).
% 1.66/0.49 thf(f1241,plain,(
% 1.66/0.49 ($true = ((f3 @ $true))) | (~spl27_25 | ~spl27_32)),
% 1.66/0.49 inference(forward_demodulation,[],[f260,f229])).
% 1.66/0.49 thf(f1243,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_23 | ~spl27_28 | ~spl27_77 | ~spl27_80)),
% 1.66/0.49 inference(forward_demodulation,[],[f1239,f810])).
% 1.66/0.49 thf(f1244,plain,(
% 1.66/0.49 $false | (~spl27_23 | ~spl27_28 | ~spl27_77 | ~spl27_80)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1243])).
% 1.66/0.49 thf(f1245,plain,(
% 1.66/0.49 ~spl27_23 | ~spl27_28 | ~spl27_77 | ~spl27_80),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1244])).
% 1.66/0.49 thf(f1249,plain,(
% 1.66/0.49 ($true = ((f5 @ $false))) | (~spl27_15 | ~spl27_20)),
% 1.66/0.49 inference(forward_demodulation,[],[f206,f184])).
% 1.66/0.49 thf(f1254,plain,(
% 1.66/0.49 ($false = ((f3 @ $true))) | (~spl27_75 | ~spl27_80)),
% 1.66/0.49 inference(forward_demodulation,[],[f477,f455])).
% 1.66/0.49 thf(f1258,plain,(
% 1.66/0.49 $false | (~spl27_69 | ~spl27_73 | spl27_74 | ~spl27_78)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1004,f964])).
% 1.66/0.49 thf(f1259,plain,(
% 1.66/0.49 ~spl27_69 | ~spl27_73 | spl27_74 | ~spl27_78),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1258])).
% 1.66/0.49 thf(f1268,plain,(
% 1.66/0.49 ($false != ((f5 @ $false))) | (~spl27_15 | spl27_18)),
% 1.66/0.49 inference(forward_demodulation,[],[f196,f184])).
% 1.66/0.49 thf(f1272,plain,(
% 1.66/0.49 ($false != ((f3 @ $true))) | (~spl27_75 | spl27_80)),
% 1.66/0.49 inference(forward_demodulation,[],[f476,f455])).
% 1.66/0.49 thf(f1274,plain,(
% 1.66/0.49 ($true = ((f3 @ $true))) | (~spl27_75 | ~spl27_82)),
% 1.66/0.49 inference(forward_demodulation,[],[f486,f455])).
% 1.66/0.49 thf(f1275,plain,(
% 1.66/0.49 ($false = ((f2 @ $true))) | (~spl27_79 | ~spl27_84)),
% 1.66/0.49 inference(forward_demodulation,[],[f495,f473])).
% 1.66/0.49 thf(f1279,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | (~spl27_67 | ~spl27_72)),
% 1.66/0.49 inference(forward_demodulation,[],[f441,f419])).
% 1.66/0.49 thf(f1296,plain,(
% 1.66/0.49 ($true = ((f4 @ $true))) | (~spl27_63 | ~spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f432,f401])).
% 1.66/0.49 thf(f1297,plain,(
% 1.66/0.49 $false | (~spl27_7 | spl27_12 | ~spl27_61 | ~spl27_66)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1096,f985])).
% 1.66/0.49 thf(f1298,plain,(
% 1.66/0.49 ~spl27_7 | spl27_12 | ~spl27_61 | ~spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1297])).
% 1.66/0.49 thf(f1305,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_63 | ~spl27_67 | ~spl27_70 | ~spl27_72)),
% 1.66/0.49 inference(forward_demodulation,[],[f1296,f1279])).
% 1.66/0.49 thf(f1306,plain,(
% 1.66/0.49 $false | (~spl27_63 | ~spl27_67 | ~spl27_70 | ~spl27_72)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1305])).
% 1.66/0.49 thf(f1307,plain,(
% 1.66/0.49 ~spl27_63 | ~spl27_67 | ~spl27_70 | ~spl27_72),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1306])).
% 1.66/0.49 thf(f1308,plain,(
% 1.66/0.49 ($true = ((f5 @ $false))) | (~spl27_11 | ~spl27_16)),
% 1.66/0.49 inference(forward_demodulation,[],[f188,f166])).
% 1.66/0.49 thf(f1312,plain,(
% 1.66/0.49 ($true != ((f5 @ $false))) | (~spl27_61 | spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f413,f392])).
% 1.66/0.49 thf(f1317,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_7 | ~spl27_10 | ~spl27_11 | ~spl27_16)),
% 1.66/0.49 inference(forward_demodulation,[],[f1308,f1095])).
% 1.66/0.49 thf(f1318,plain,(
% 1.66/0.49 $false | (~spl27_7 | ~spl27_10 | ~spl27_11 | ~spl27_16)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1317])).
% 1.66/0.49 thf(f1319,plain,(
% 1.66/0.49 ~spl27_7 | ~spl27_10 | ~spl27_11 | ~spl27_16),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1318])).
% 1.66/0.49 thf(f1325,plain,(
% 1.66/0.49 ($true = ((f5 @ $true))) | (~spl27_9 | ~spl27_16)),
% 1.66/0.49 inference(forward_demodulation,[],[f188,f157])).
% 1.66/0.49 thf(f1326,plain,(
% 1.66/0.49 $false | (~spl27_7 | ~spl27_12 | ~spl27_61 | spl27_66)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1312,f1090])).
% 1.66/0.49 thf(f1327,plain,(
% 1.66/0.49 ~spl27_7 | ~spl27_12 | ~spl27_61 | spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1326])).
% 1.66/0.49 thf(f1337,plain,(
% 1.66/0.49 spl27_69 | spl27_67),
% 1.66/0.49 inference(avatar_split_clause,[],[f1043,f417,f426])).
% 1.66/0.49 thf(f1343,plain,(
% 1.66/0.49 ($false != ((f4 @ $true))) | (~spl27_71 | spl27_76)),
% 1.66/0.49 inference(forward_demodulation,[],[f458,f437])).
% 1.66/0.49 thf(f1355,plain,(
% 1.66/0.49 ($true = ((f6 @ $false))) | (~spl27_7 | ~spl27_58)),
% 1.66/0.49 inference(forward_demodulation,[],[f378,f148])).
% 1.66/0.49 thf(f1360,plain,(
% 1.66/0.49 ($true != ((f4 @ $false))) | (~spl27_65 | spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f431,f410])).
% 1.66/0.49 thf(f1363,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_7 | ~spl27_56 | ~spl27_58)),
% 1.66/0.49 inference(forward_demodulation,[],[f1355,f1091])).
% 1.66/0.49 thf(f1364,plain,(
% 1.66/0.49 $false | (~spl27_7 | ~spl27_56 | ~spl27_58)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1363])).
% 1.66/0.49 thf(f1365,plain,(
% 1.66/0.49 ~spl27_7 | ~spl27_56 | ~spl27_58),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1364])).
% 1.66/0.49 thf(f1366,plain,(
% 1.66/0.49 $false | (~spl27_65 | ~spl27_69 | spl27_70 | ~spl27_74)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1360,f971])).
% 1.66/0.49 thf(f1367,plain,(
% 1.66/0.49 ~spl27_65 | ~spl27_69 | spl27_70 | ~spl27_74),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1366])).
% 1.66/0.49 thf(f1368,plain,(
% 1.66/0.49 ($false != ((f6 @ $false))) | (~spl27_7 | spl27_56)),
% 1.66/0.49 inference(forward_demodulation,[],[f368,f148])).
% 1.66/0.49 thf(f1373,plain,(
% 1.66/0.49 ($true = ((f4 @ $true))) | (~spl27_67 | ~spl27_74)),
% 1.66/0.49 inference(forward_demodulation,[],[f450,f419])).
% 1.66/0.49 thf(f1385,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF9) | spl27_41),
% 1.66/0.49 inference(constrained_superposition,[],[f300,f6])).
% 1.66/0.49 thf(f1386,plain,(
% 1.66/0.49 ($false = sF9) | spl27_41),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1385])).
% 1.66/0.49 thf(f1389,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_43 | ~spl27_46 | ~spl27_48)),
% 1.66/0.49 inference(forward_demodulation,[],[f1209,f729])).
% 1.66/0.49 thf(f1390,plain,(
% 1.66/0.49 $false | (~spl27_43 | ~spl27_46 | ~spl27_48)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1389])).
% 1.66/0.49 thf(f1391,plain,(
% 1.66/0.49 ~spl27_43 | ~spl27_46 | ~spl27_48),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1390])).
% 1.66/0.49 thf(f1394,plain,(
% 1.66/0.49 ($true = ((f2 @ $false))) | (~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f540,f518])).
% 1.66/0.49 thf(f1398,plain,(
% 1.66/0.49 ($false = ((f1 @ $true))) | (~spl27_91 | ~spl27_96)),
% 1.66/0.49 inference(forward_demodulation,[],[f549,f527])).
% 1.66/0.49 thf(f1399,plain,(
% 1.66/0.49 ($true != ((f1 @ $true))) | (~spl27_91 | spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f557,f527])).
% 1.66/0.49 thf(f1402,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_85 | ~spl27_88 | ~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f1394,f830])).
% 1.66/0.49 thf(f1403,plain,(
% 1.66/0.49 $false | (~spl27_85 | ~spl27_88 | ~spl27_89 | ~spl27_94)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1402])).
% 1.66/0.49 thf(f1404,plain,(
% 1.66/0.49 ~spl27_85 | ~spl27_88 | ~spl27_89 | ~spl27_94),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1403])).
% 1.66/0.49 thf(f1405,plain,(
% 1.66/0.49 $false | (~spl27_37 | ~spl27_44 | ~spl27_91 | spl27_98)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1399,f1192])).
% 1.66/0.49 thf(f1406,plain,(
% 1.66/0.49 ~spl27_37 | ~spl27_44 | ~spl27_91 | spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1405])).
% 1.66/0.49 thf(f1416,plain,(
% 1.66/0.49 ($true != ((f1 @ $false))) | (~spl27_93 | spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f557,f536])).
% 1.66/0.49 thf(f1418,plain,(
% 1.66/0.49 $false | (~spl27_47 | ~spl27_52 | ~spl27_93 | spl27_98)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1416,f875])).
% 1.66/0.49 thf(f1419,plain,(
% 1.66/0.49 ~spl27_47 | ~spl27_52 | ~spl27_93 | spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1418])).
% 1.66/0.49 thf(f1423,plain,(
% 1.66/0.49 ($false != ((f1 @ $true))) | (~spl27_41 | spl27_46)),
% 1.66/0.49 inference(forward_demodulation,[],[f322,f301])).
% 1.66/0.49 thf(f1445,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF23) | spl27_95),
% 1.66/0.49 inference(constrained_superposition,[],[f544,f6])).
% 1.66/0.49 thf(f1446,plain,(
% 1.66/0.49 ($false = sF23) | spl27_95),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1445])).
% 1.66/0.49 thf(f1453,plain,(
% 1.66/0.49 ($true = ((f5 @ $true))) | (~spl27_13 | ~spl27_20)),
% 1.66/0.49 inference(constrained_superposition,[],[f206,f175])).
% 1.66/0.49 thf(f1454,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | ($false = sF3) | ~spl27_22),
% 1.66/0.49 inference(constrained_superposition,[],[f215,f6])).
% 1.66/0.49 thf(f1455,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | (~spl27_17 | ~spl27_22)),
% 1.66/0.49 inference(constrained_superposition,[],[f215,f193])).
% 1.66/0.49 thf(f1458,plain,(
% 1.66/0.49 $false | (~spl27_17 | ~spl27_22 | ~spl27_71 | spl27_76)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1455,f1343])).
% 1.66/0.49 thf(f1459,plain,(
% 1.66/0.49 ~spl27_17 | ~spl27_22 | ~spl27_71 | spl27_76),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1458])).
% 1.66/0.49 thf(f1460,plain,(
% 1.66/0.49 ($false = sF3) | (~spl27_22 | ~spl27_71 | spl27_76)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1454,f1343])).
% 1.66/0.49 thf(f1461,plain,(
% 1.66/0.49 $false | (spl27_19 | ~spl27_22 | ~spl27_71 | spl27_76)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1460,f201])).
% 1.66/0.49 thf(f1462,plain,(
% 1.66/0.49 spl27_19 | ~spl27_22 | ~spl27_71 | spl27_76),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1461])).
% 1.66/0.49 thf(f1463,plain,(
% 1.66/0.49 ($false != ((f4 @ $true))) | (~spl27_17 | spl27_22)),
% 1.66/0.49 inference(forward_demodulation,[],[f214,f193])).
% 1.66/0.49 thf(f1465,plain,(
% 1.66/0.49 ($true = ((f4 @ $true))) | (~spl27_17 | ~spl27_24)),
% 1.66/0.49 inference(forward_demodulation,[],[f224,f193])).
% 1.66/0.49 thf(f1466,plain,(
% 1.66/0.49 ($true = ((f3 @ $true))) | (~spl27_21 | ~spl27_28)),
% 1.66/0.49 inference(forward_demodulation,[],[f242,f211])).
% 1.66/0.49 thf(f1467,plain,(
% 1.66/0.49 ($false != ((f3 @ $true))) | ($false = sF6) | spl27_34),
% 1.66/0.49 inference(constrained_superposition,[],[f268,f6])).
% 1.66/0.49 thf(f1471,plain,(
% 1.66/0.49 ($false != ((f3 @ $true))) | (spl27_31 | spl27_34)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1467,f255])).
% 1.66/0.49 thf(f1481,plain,(
% 1.66/0.49 ($true = ((f2 @ $true))) | (~spl27_33 | ~spl27_40)),
% 1.66/0.49 inference(constrained_superposition,[],[f296,f265])).
% 1.66/0.49 thf(f1482,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_38 | ~spl27_40)),
% 1.66/0.49 inference(constrained_superposition,[],[f296,f287])).
% 1.66/0.49 thf(f1486,plain,(
% 1.66/0.49 $false | (~spl27_38 | ~spl27_40)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1482])).
% 1.66/0.49 thf(f1487,plain,(
% 1.66/0.49 ~spl27_38 | ~spl27_40),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1486])).
% 1.66/0.49 thf(f1488,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_33 | ~spl27_40 | ~spl27_79 | ~spl27_84)),
% 1.66/0.49 inference(forward_demodulation,[],[f1481,f1275])).
% 1.66/0.49 thf(f1489,plain,(
% 1.66/0.49 $false | (~spl27_33 | ~spl27_40 | ~spl27_79 | ~spl27_84)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1488])).
% 1.66/0.49 thf(f1490,plain,(
% 1.66/0.49 ~spl27_33 | ~spl27_40 | ~spl27_79 | ~spl27_84),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1489])).
% 1.66/0.49 thf(f1496,plain,(
% 1.66/0.49 ($true != ((f3 @ $true))) | (~spl27_29 | spl27_36)),
% 1.66/0.49 inference(forward_demodulation,[],[f277,f247])).
% 1.66/0.49 thf(f1501,plain,(
% 1.66/0.49 ($false = ((f2 @ $true))) | (~spl27_87 | ~spl27_92)),
% 1.66/0.49 inference(forward_demodulation,[],[f531,f509])).
% 1.66/0.49 thf(f1503,plain,(
% 1.66/0.49 $false | (~spl27_25 | ~spl27_29 | ~spl27_32 | spl27_36)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1496,f1241])).
% 1.66/0.49 thf(f1504,plain,(
% 1.66/0.49 ~spl27_25 | ~spl27_29 | ~spl27_32 | spl27_36),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1503])).
% 1.66/0.49 thf(f1511,plain,(
% 1.66/0.49 ($false != ((f2 @ $true))) | (~spl27_79 | spl27_84)),
% 1.66/0.49 inference(forward_demodulation,[],[f494,f473])).
% 1.66/0.49 thf(f1514,plain,(
% 1.66/0.49 ($false != ((f2 @ $true))) | (~spl27_83 | spl27_88)),
% 1.66/0.49 inference(forward_demodulation,[],[f512,f491])).
% 1.66/0.49 thf(f1515,plain,(
% 1.66/0.49 ($true = ((f2 @ $true))) | (~spl27_83 | ~spl27_90)),
% 1.66/0.49 inference(forward_demodulation,[],[f522,f491])).
% 1.66/0.49 thf(f1519,plain,(
% 1.66/0.49 $false | (~spl27_79 | spl27_84 | ~spl27_87 | ~spl27_92)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1511,f1501])).
% 1.66/0.49 thf(f1520,plain,(
% 1.66/0.49 ~spl27_79 | spl27_84 | ~spl27_87 | ~spl27_92),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1519])).
% 1.66/0.49 thf(f1521,plain,(
% 1.66/0.49 $false | (~spl27_83 | ~spl27_87 | spl27_88 | ~spl27_92)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1514,f1501])).
% 1.66/0.49 thf(f1522,plain,(
% 1.66/0.49 ~spl27_83 | ~spl27_87 | spl27_88 | ~spl27_92),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1521])).
% 1.66/0.49 thf(f1523,plain,(
% 1.66/0.49 spl27_89 | spl27_87),
% 1.66/0.49 inference(avatar_split_clause,[],[f1068,f507,f516])).
% 1.66/0.49 thf(f1524,plain,(
% 1.66/0.49 ($false = ((f2 @ $true))) | (~spl27_83 | ~spl27_88)),
% 1.66/0.49 inference(forward_demodulation,[],[f513,f491])).
% 1.66/0.49 thf(f1538,plain,(
% 1.66/0.49 spl27_85 | spl27_83),
% 1.66/0.49 inference(avatar_split_clause,[],[f1063,f489,f498])).
% 1.66/0.49 thf(f1550,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_25 | ~spl27_30 | ~spl27_75 | ~spl27_82)),
% 1.66/0.49 inference(forward_demodulation,[],[f1274,f1240])).
% 1.66/0.49 thf(f1551,plain,(
% 1.66/0.49 $false | (~spl27_25 | ~spl27_30 | ~spl27_75 | ~spl27_82)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1550])).
% 1.66/0.49 thf(f1552,plain,(
% 1.66/0.49 ~spl27_25 | ~spl27_30 | ~spl27_75 | ~spl27_82),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1551])).
% 1.66/0.49 thf(f1567,plain,(
% 1.66/0.49 ($true != ((f2 @ $true))) | (~spl27_33 | spl27_40)),
% 1.66/0.49 inference(forward_demodulation,[],[f295,f265])).
% 1.66/0.49 thf(f1571,plain,(
% 1.66/0.49 ($true = ((f2 @ $true))) | (~spl27_87 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f540,f509])).
% 1.66/0.49 thf(f1577,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_45 | ~spl27_52 | ~spl27_91 | ~spl27_96)),
% 1.66/0.49 inference(forward_demodulation,[],[f937,f1398])).
% 1.66/0.49 thf(f1578,plain,(
% 1.66/0.49 $false | (~spl27_45 | ~spl27_52 | ~spl27_91 | ~spl27_96)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1577])).
% 1.66/0.49 thf(f1579,plain,(
% 1.66/0.49 ~spl27_45 | ~spl27_52 | ~spl27_91 | ~spl27_96),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1578])).
% 1.66/0.49 thf(f1585,plain,(
% 1.66/0.49 $false | (~spl27_41 | spl27_46 | ~spl27_91 | ~spl27_96)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1423,f1398])).
% 1.66/0.49 thf(f1586,plain,(
% 1.66/0.49 ~spl27_41 | spl27_46 | ~spl27_91 | ~spl27_96),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1585])).
% 1.66/0.49 thf(f1595,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_79 | ~spl27_84 | ~spl27_87 | ~spl27_94)),
% 1.66/0.49 inference(forward_demodulation,[],[f1571,f1275])).
% 1.66/0.49 thf(f1596,plain,(
% 1.66/0.49 $false | (~spl27_79 | ~spl27_84 | ~spl27_87 | ~spl27_94)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1595])).
% 1.66/0.49 thf(f1597,plain,(
% 1.66/0.49 ~spl27_79 | ~spl27_84 | ~spl27_87 | ~spl27_94),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1596])).
% 1.66/0.49 thf(f1603,plain,(
% 1.66/0.49 ($false != ((f2 @ $true))) | (~spl27_79 | spl27_84)),
% 1.66/0.49 inference(forward_demodulation,[],[f494,f473])).
% 1.66/0.49 thf(f1605,plain,(
% 1.66/0.49 ($true = ((f2 @ $true))) | (~spl27_79 | ~spl27_86)),
% 1.66/0.49 inference(forward_demodulation,[],[f504,f473])).
% 1.66/0.49 thf(f1612,plain,(
% 1.66/0.49 $false | (~spl27_33 | spl27_40 | ~spl27_83 | ~spl27_90)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1567,f1515])).
% 1.66/0.49 thf(f1613,plain,(
% 1.66/0.49 ~spl27_33 | spl27_40 | ~spl27_83 | ~spl27_90),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1612])).
% 1.66/0.49 thf(f1624,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_79 | ~spl27_83 | ~spl27_86 | ~spl27_88)),
% 1.66/0.49 inference(forward_demodulation,[],[f1605,f1524])).
% 1.66/0.49 thf(f1625,plain,(
% 1.66/0.49 $false | (~spl27_79 | ~spl27_83 | ~spl27_86 | ~spl27_88)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1624])).
% 1.66/0.49 thf(f1626,plain,(
% 1.66/0.49 ~spl27_79 | ~spl27_83 | ~spl27_86 | ~spl27_88),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1625])).
% 1.66/0.49 thf(f1629,plain,(
% 1.66/0.49 $false | (~spl27_79 | ~spl27_83 | spl27_84 | ~spl27_88)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1603,f1524])).
% 1.66/0.49 thf(f1630,plain,(
% 1.66/0.49 ~spl27_79 | ~spl27_83 | spl27_84 | ~spl27_88),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1629])).
% 1.66/0.49 thf(f1644,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_21 | ~spl27_28 | ~spl27_75 | ~spl27_80)),
% 1.66/0.49 inference(forward_demodulation,[],[f1466,f1254])).
% 1.66/0.49 thf(f1645,plain,(
% 1.66/0.49 $false | (~spl27_21 | ~spl27_28 | ~spl27_75 | ~spl27_80)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1644])).
% 1.66/0.49 thf(f1646,plain,(
% 1.66/0.49 ~spl27_21 | ~spl27_28 | ~spl27_75 | ~spl27_80),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1645])).
% 1.66/0.49 thf(f1651,plain,(
% 1.66/0.49 spl27_73 | spl27_71),
% 1.66/0.49 inference(avatar_split_clause,[],[f1048,f435,f444])).
% 1.66/0.49 thf(f1661,plain,(
% 1.66/0.49 ($false = ((f5 @ $true))) | (~spl27_13 | ~spl27_18)),
% 1.66/0.49 inference(forward_demodulation,[],[f197,f175])).
% 1.66/0.49 thf(f1664,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF3) | spl27_17),
% 1.66/0.49 inference(constrained_superposition,[],[f192,f6])).
% 1.66/0.49 thf(f1665,plain,(
% 1.66/0.49 ($false = sF3) | spl27_17),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1664])).
% 1.66/0.49 thf(f1668,plain,(
% 1.66/0.49 ($false != ((f5 @ $true))) | (~spl27_59 | spl27_64)),
% 1.66/0.49 inference(forward_demodulation,[],[f404,f383])).
% 1.66/0.49 thf(f1671,plain,(
% 1.66/0.49 ($false != ((f4 @ $true))) | (~spl27_67 | spl27_72)),
% 1.66/0.49 inference(forward_demodulation,[],[f440,f419])).
% 1.66/0.49 thf(f1678,plain,(
% 1.66/0.49 $false | (~spl27_13 | ~spl27_18 | ~spl27_59 | spl27_64)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1668,f1661])).
% 1.66/0.49 thf(f1679,plain,(
% 1.66/0.49 ~spl27_13 | ~spl27_18 | ~spl27_59 | spl27_64),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1678])).
% 1.66/0.49 thf(f1680,plain,(
% 1.66/0.49 spl27_61 | spl27_59),
% 1.66/0.49 inference(avatar_split_clause,[],[f1033,f381,f390])).
% 1.66/0.49 thf(f1689,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF4) | spl27_21),
% 1.66/0.49 inference(constrained_superposition,[],[f210,f6])).
% 1.66/0.49 thf(f1690,plain,(
% 1.66/0.49 ($false = sF4) | spl27_21),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1689])).
% 1.66/0.49 thf(f1696,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF5) | spl27_25),
% 1.66/0.49 inference(constrained_superposition,[],[f228,f6])).
% 1.66/0.49 thf(f1697,plain,(
% 1.66/0.49 ($false = sF5) | spl27_25),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1696])).
% 1.66/0.49 thf(f1701,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF6) | spl27_29),
% 1.66/0.49 inference(constrained_superposition,[],[f246,f6])).
% 1.66/0.49 thf(f1702,plain,(
% 1.66/0.49 ($false = sF6) | spl27_29),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1701])).
% 1.66/0.49 thf(f1711,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF10) | spl27_45),
% 1.66/0.49 inference(constrained_superposition,[],[f318,f6])).
% 1.66/0.49 thf(f1712,plain,(
% 1.66/0.49 ($false = sF10) | spl27_45),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1711])).
% 1.66/0.49 thf(f1737,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_22 | ~spl27_24)),
% 1.66/0.49 inference(constrained_superposition,[],[f224,f215])).
% 1.66/0.49 thf(f1741,plain,(
% 1.66/0.49 $false | (~spl27_22 | ~spl27_24)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1737])).
% 1.66/0.49 thf(f1742,plain,(
% 1.66/0.49 ~spl27_22 | ~spl27_24),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1741])).
% 1.66/0.49 thf(f1748,plain,(
% 1.66/0.49 ($false = ((f3 @ $true))) | (~spl27_21 | ~spl27_26)),
% 1.66/0.49 inference(constrained_superposition,[],[f233,f211])).
% 1.66/0.49 thf(f1767,plain,(
% 1.66/0.49 ($true = ((f6 @ $true))) | (~spl27_55 | ~spl27_62)),
% 1.66/0.49 inference(constrained_superposition,[],[f396,f365])).
% 1.66/0.49 thf(f1768,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_60 | ~spl27_62)),
% 1.66/0.49 inference(constrained_superposition,[],[f396,f387])).
% 1.66/0.49 thf(f1772,plain,(
% 1.66/0.49 $false | (~spl27_60 | ~spl27_62)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1768])).
% 1.66/0.49 thf(f1773,plain,(
% 1.66/0.49 ~spl27_60 | ~spl27_62),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1772])).
% 1.66/0.49 thf(f1774,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_55 | ~spl27_62 | ~spl27_110)),
% 1.66/0.49 inference(forward_demodulation,[],[f1767,f1119])).
% 1.66/0.49 thf(f1775,plain,(
% 1.66/0.49 $false | (~spl27_55 | ~spl27_62 | ~spl27_110)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1774])).
% 1.66/0.49 thf(f1776,plain,(
% 1.66/0.49 ~spl27_55 | ~spl27_62 | ~spl27_110),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1775])).
% 1.66/0.49 thf(f1792,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_103 | ~spl27_107 | ~spl27_108)),
% 1.66/0.49 inference(constrained_superposition,[],[f1179,f609])).
% 1.66/0.49 thf(f1796,plain,(
% 1.66/0.49 $false | (~spl27_103 | ~spl27_107 | ~spl27_108)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1792])).
% 1.66/0.49 thf(f1797,plain,(
% 1.66/0.49 ~spl27_103 | ~spl27_107 | ~spl27_108),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1796])).
% 1.66/0.49 thf(f1800,plain,(
% 1.66/0.49 ($true != ((f0 @ $true))) | (~spl27_99 | spl27_106)),
% 1.66/0.49 inference(forward_demodulation,[],[f593,f563])).
% 1.66/0.49 thf(f1801,plain,(
% 1.66/0.49 ($false = ((f0 @ $false))) | (~spl27_105 | ~spl27_107)),
% 1.66/0.49 inference(forward_demodulation,[],[f599,f590])).
% 1.66/0.49 thf(f1803,plain,(
% 1.66/0.49 $false | (~spl27_49 | ~spl27_54 | ~spl27_99 | spl27_106)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1800,f1155])).
% 1.66/0.49 thf(f1804,plain,(
% 1.66/0.49 ~spl27_49 | ~spl27_54 | ~spl27_99 | spl27_106),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1803])).
% 1.66/0.49 thf(f1805,plain,(
% 1.66/0.49 $false | (~spl27_97 | spl27_100 | ~spl27_105 | ~spl27_107)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1801,f1187])).
% 1.66/0.49 thf(f1806,plain,(
% 1.66/0.49 ~spl27_97 | spl27_100 | ~spl27_105 | ~spl27_107),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1805])).
% 1.66/0.49 thf(f1817,plain,(
% 1.66/0.49 ($true != $true) | ($false = sF25) | spl27_103),
% 1.66/0.49 inference(constrained_superposition,[],[f580,f6])).
% 1.66/0.49 thf(f1818,plain,(
% 1.66/0.49 ($false = sF25) | spl27_103),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1817])).
% 1.66/0.49 thf(f1825,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_27 | ~spl27_30 | ~spl27_31 | ~spl27_36)),
% 1.66/0.49 inference(constrained_superposition,[],[f1221,f689])).
% 1.66/0.49 thf(f1829,plain,(
% 1.66/0.49 $false | (~spl27_27 | ~spl27_30 | ~spl27_31 | ~spl27_36)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1825])).
% 1.66/0.49 thf(f1830,plain,(
% 1.66/0.49 ~spl27_27 | ~spl27_30 | ~spl27_31 | ~spl27_36),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1829])).
% 1.66/0.49 thf(f1831,plain,(
% 1.66/0.49 spl27_23 | spl27_21),
% 1.66/0.49 inference(avatar_split_clause,[],[f1690,f209,f218])).
% 1.66/0.49 thf(f1839,plain,(
% 1.66/0.49 ($true != ((f3 @ $false))) | (~spl27_31 | spl27_36)),
% 1.66/0.49 inference(forward_demodulation,[],[f277,f256])).
% 1.66/0.49 thf(f1875,plain,(
% 1.66/0.49 spl27_27 | spl27_25),
% 1.66/0.49 inference(avatar_split_clause,[],[f1697,f227,f236])).
% 1.66/0.49 thf(f1877,plain,(
% 1.66/0.49 $false | (~spl27_23 | ~spl27_28 | ~spl27_31 | spl27_36)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1839,f1239])).
% 1.66/0.49 thf(f1878,plain,(
% 1.66/0.49 ~spl27_23 | ~spl27_28 | ~spl27_31 | spl27_36),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1877])).
% 1.66/0.49 thf(f1951,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_9 | ~spl27_13 | ~spl27_16 | ~spl27_18)),
% 1.66/0.49 inference(constrained_superposition,[],[f1661,f1325])).
% 1.66/0.49 thf(f1955,plain,(
% 1.66/0.49 $false | (~spl27_9 | ~spl27_13 | ~spl27_16 | ~spl27_18)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1951])).
% 1.66/0.49 thf(f1956,plain,(
% 1.66/0.49 ~spl27_9 | ~spl27_13 | ~spl27_16 | ~spl27_18),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1955])).
% 1.66/0.49 thf(f1958,plain,(
% 1.66/0.49 spl27_11 | spl27_9),
% 1.66/0.49 inference(avatar_split_clause,[],[f1105,f155,f164])).
% 1.66/0.49 thf(f1966,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_14 | ~spl27_16)),
% 1.66/0.49 inference(forward_demodulation,[],[f188,f179])).
% 1.66/0.49 thf(f1967,plain,(
% 1.66/0.49 $false | (~spl27_14 | ~spl27_16)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f1966])).
% 1.66/0.49 thf(f1968,plain,(
% 1.66/0.49 ~spl27_14 | ~spl27_16),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f1967])).
% 1.66/0.49 thf(f1979,plain,(
% 1.66/0.49 ($true != ((f6 @ $true))) | (~spl27_55 | spl27_62)),
% 1.66/0.49 inference(forward_demodulation,[],[f395,f365])).
% 1.66/0.49 thf(f2007,plain,(
% 1.66/0.49 ($false = ((f5 @ $true))) | (~spl27_5 | ~spl27_10)),
% 1.66/0.49 inference(constrained_superposition,[],[f161,f139])).
% 1.66/0.49 thf(f2014,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_10 | ~spl27_12)),
% 1.66/0.49 inference(constrained_superposition,[],[f170,f161])).
% 1.66/0.49 thf(f2018,plain,(
% 1.66/0.49 $false | (~spl27_10 | ~spl27_12)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2014])).
% 1.66/0.49 thf(f2019,plain,(
% 1.66/0.49 ~spl27_10 | ~spl27_12),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2018])).
% 1.66/0.49 thf(f2024,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_18 | ~spl27_20)),
% 1.66/0.49 inference(constrained_superposition,[],[f197,f206])).
% 1.66/0.49 thf(f2028,plain,(
% 1.66/0.49 $false | (~spl27_18 | ~spl27_20)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2024])).
% 1.66/0.49 thf(f2029,plain,(
% 1.66/0.49 ~spl27_18 | ~spl27_20),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2028])).
% 1.66/0.49 thf(f2032,plain,(
% 1.66/0.49 ($true = ((f6 @ $true))) | ($false = sF0) | ~spl27_58),
% 1.66/0.49 inference(constrained_superposition,[],[f378,f6])).
% 1.66/0.49 thf(f2033,plain,(
% 1.66/0.49 ($true = ((f6 @ $true))) | (~spl27_5 | ~spl27_58)),
% 1.66/0.49 inference(constrained_superposition,[],[f378,f139])).
% 1.66/0.49 thf(f2036,plain,(
% 1.66/0.49 ($false = sF0) | (~spl27_55 | ~spl27_58 | spl27_62)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2032,f1979])).
% 1.66/0.49 thf(f2037,plain,(
% 1.66/0.49 $false | (spl27_7 | ~spl27_55 | ~spl27_58 | spl27_62)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2036,f147])).
% 1.66/0.49 thf(f2038,plain,(
% 1.66/0.49 spl27_7 | ~spl27_55 | ~spl27_58 | spl27_62),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2037])).
% 1.66/0.49 thf(f2043,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_5 | ~spl27_58 | ~spl27_110)),
% 1.66/0.49 inference(forward_demodulation,[],[f2033,f1119])).
% 1.66/0.49 thf(f2044,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_58 | ~spl27_110)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2043])).
% 1.66/0.49 thf(f2045,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_58 | ~spl27_110),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2044])).
% 1.66/0.49 thf(f2054,plain,(
% 1.66/0.49 ($false != ((f5 @ $true))) | (~spl27_13 | spl27_18)),
% 1.66/0.49 inference(forward_demodulation,[],[f196,f175])).
% 1.66/0.49 thf(f2063,plain,(
% 1.66/0.49 ($true != ((f5 @ $true))) | (~spl27_59 | spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f413,f383])).
% 1.66/0.49 thf(f2076,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_10 | ~spl27_13 | spl27_18)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2054,f2007])).
% 1.66/0.49 thf(f2077,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_10 | ~spl27_13 | spl27_18),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2076])).
% 1.66/0.49 thf(f2078,plain,(
% 1.66/0.49 $false | (~spl27_13 | ~spl27_20 | ~spl27_59 | spl27_66)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2063,f1453])).
% 1.66/0.49 thf(f2079,plain,(
% 1.66/0.49 ~spl27_13 | ~spl27_20 | ~spl27_59 | spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2078])).
% 1.66/0.49 thf(f2084,plain,(
% 1.66/0.49 spl27_7 | spl27_5),
% 1.66/0.49 inference(avatar_split_clause,[],[f1100,f137,f146])).
% 1.66/0.49 thf(f2085,plain,(
% 1.66/0.49 ($false = ((f6 @ $false))) | (~spl27_6 | ~spl27_109)),
% 1.66/0.49 inference(forward_demodulation,[],[f143,f1115])).
% 1.66/0.49 thf(f2097,plain,(
% 1.66/0.49 $false | (~spl27_6 | ~spl27_7 | spl27_56 | ~spl27_109)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2085,f1368])).
% 1.66/0.49 thf(f2098,plain,(
% 1.66/0.49 ~spl27_6 | ~spl27_7 | spl27_56 | ~spl27_109),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2097])).
% 1.66/0.49 thf(f2111,plain,(
% 1.66/0.49 ($true = ((f6 @ $false))) | (~spl27_57 | ~spl27_62)),
% 1.66/0.49 inference(forward_demodulation,[],[f396,f374])).
% 1.66/0.49 thf(f2115,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_7 | ~spl27_56 | ~spl27_57 | ~spl27_62)),
% 1.66/0.49 inference(forward_demodulation,[],[f2111,f1091])).
% 1.66/0.49 thf(f2116,plain,(
% 1.66/0.49 $false | (~spl27_7 | ~spl27_56 | ~spl27_57 | ~spl27_62)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2115])).
% 1.66/0.49 thf(f2117,plain,(
% 1.66/0.49 ~spl27_7 | ~spl27_56 | ~spl27_57 | ~spl27_62),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2116])).
% 1.66/0.49 thf(f2121,plain,(
% 1.66/0.49 spl27_19 | spl27_17),
% 1.66/0.49 inference(avatar_split_clause,[],[f1665,f191,f200])).
% 1.66/0.49 thf(f2126,plain,(
% 1.66/0.49 $false | (~spl27_21 | ~spl27_26 | ~spl27_75 | spl27_80)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f1748,f1272])).
% 1.66/0.49 thf(f2127,plain,(
% 1.66/0.49 ~spl27_21 | ~spl27_26 | ~spl27_75 | spl27_80),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2126])).
% 1.66/0.49 thf(f2130,plain,(
% 1.66/0.49 ($true = ((f4 @ $false))) | (~spl27_19 | ~spl27_24)),
% 1.66/0.49 inference(forward_demodulation,[],[f224,f202])).
% 1.66/0.49 thf(f2143,plain,(
% 1.66/0.49 ($false = ((f5 @ $false))) | (~spl27_11 | ~spl27_14)),
% 1.66/0.49 inference(forward_demodulation,[],[f179,f166])).
% 1.66/0.49 thf(f2144,plain,(
% 1.66/0.49 ($true != ((f5 @ $false))) | (~spl27_11 | spl27_16)),
% 1.66/0.49 inference(forward_demodulation,[],[f187,f166])).
% 1.66/0.49 thf(f2176,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_19 | ~spl27_24 | ~spl27_73 | ~spl27_76)),
% 1.66/0.49 inference(forward_demodulation,[],[f2130,f800])).
% 1.66/0.49 thf(f2177,plain,(
% 1.66/0.49 $false | (~spl27_19 | ~spl27_24 | ~spl27_73 | ~spl27_76)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2176])).
% 1.66/0.49 thf(f2178,plain,(
% 1.66/0.49 ~spl27_19 | ~spl27_24 | ~spl27_73 | ~spl27_76),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2177])).
% 1.66/0.49 thf(f2191,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | (~spl27_71 | ~spl27_76)),
% 1.66/0.49 inference(forward_demodulation,[],[f459,f437])).
% 1.66/0.49 thf(f2192,plain,(
% 1.66/0.49 ($true != ((f4 @ $true))) | (~spl27_71 | spl27_78)),
% 1.66/0.49 inference(forward_demodulation,[],[f467,f437])).
% 1.66/0.49 thf(f2193,plain,(
% 1.66/0.49 $false | (~spl27_67 | ~spl27_71 | spl27_72 | ~spl27_76)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2191,f1671])).
% 1.66/0.49 thf(f2194,plain,(
% 1.66/0.49 ~spl27_67 | ~spl27_71 | spl27_72 | ~spl27_76),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2193])).
% 1.66/0.49 thf(f2195,plain,(
% 1.66/0.49 $false | (~spl27_67 | ~spl27_71 | ~spl27_74 | spl27_78)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2192,f1373])).
% 1.66/0.49 thf(f2196,plain,(
% 1.66/0.49 ~spl27_67 | ~spl27_71 | ~spl27_74 | spl27_78),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2195])).
% 1.66/0.49 thf(f2204,plain,(
% 1.66/0.49 ($false = ((f3 @ $true))) | (~spl27_75 | ~spl27_80)),
% 1.66/0.49 inference(forward_demodulation,[],[f477,f455])).
% 1.66/0.49 thf(f2224,plain,(
% 1.66/0.49 $false | (spl27_31 | spl27_34 | ~spl27_75 | ~spl27_80)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2204,f1471])).
% 1.66/0.49 thf(f2225,plain,(
% 1.66/0.49 spl27_31 | spl27_34 | ~spl27_75 | ~spl27_80),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2224])).
% 1.66/0.49 thf(f2233,plain,(
% 1.66/0.49 spl27_110 | ~spl27_5 | ~spl27_56),
% 1.66/0.49 inference(avatar_split_clause,[],[f750,f367,f137,f1117])).
% 1.66/0.49 thf(f2244,plain,(
% 1.66/0.49 spl27_31 | spl27_29),
% 1.66/0.49 inference(avatar_split_clause,[],[f1702,f245,f254])).
% 1.66/0.49 thf(f2289,plain,(
% 1.66/0.49 $false | (~spl27_11 | ~spl27_14 | ~spl27_15 | spl27_18)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2143,f1268])).
% 1.66/0.49 thf(f2290,plain,(
% 1.66/0.49 ~spl27_11 | ~spl27_14 | ~spl27_15 | spl27_18),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2289])).
% 1.66/0.49 thf(f2291,plain,(
% 1.66/0.49 $false | (~spl27_11 | ~spl27_15 | spl27_16 | ~spl27_20)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2144,f1249])).
% 1.66/0.49 thf(f2292,plain,(
% 1.66/0.49 ~spl27_11 | ~spl27_15 | spl27_16 | ~spl27_20),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2291])).
% 1.66/0.49 thf(f2305,plain,(
% 1.66/0.49 ($false != ((f5 @ $true))) | (~spl27_5 | spl27_10)),
% 1.66/0.49 inference(forward_demodulation,[],[f160,f139])).
% 1.66/0.49 thf(f2307,plain,(
% 1.66/0.49 ($true = ((f5 @ $true))) | (~spl27_5 | ~spl27_12)),
% 1.66/0.49 inference(forward_demodulation,[],[f170,f139])).
% 1.66/0.49 thf(f2318,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_9 | spl27_10 | ~spl27_14)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2305,f649])).
% 1.66/0.49 thf(f2319,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_9 | spl27_10 | ~spl27_14),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2318])).
% 1.66/0.49 thf(f2320,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_5 | ~spl27_9 | ~spl27_12 | ~spl27_14)),
% 1.66/0.49 inference(forward_demodulation,[],[f2307,f649])).
% 1.66/0.49 thf(f2321,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_9 | ~spl27_12 | ~spl27_14)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2320])).
% 1.66/0.49 thf(f2322,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_9 | ~spl27_12 | ~spl27_14),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2321])).
% 1.66/0.49 thf(f2336,plain,(
% 1.66/0.49 ($true = ((f5 @ $true))) | (~spl27_59 | ~spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f414,f383])).
% 1.66/0.49 thf(f2355,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_5 | ~spl27_10 | ~spl27_59 | ~spl27_66)),
% 1.66/0.49 inference(forward_demodulation,[],[f2336,f2007])).
% 1.66/0.49 thf(f2356,plain,(
% 1.66/0.49 $false | (~spl27_5 | ~spl27_10 | ~spl27_59 | ~spl27_66)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2355])).
% 1.66/0.49 thf(f2357,plain,(
% 1.66/0.49 ~spl27_5 | ~spl27_10 | ~spl27_59 | ~spl27_66),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2356])).
% 1.66/0.49 thf(f2386,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | (~spl27_63 | ~spl27_68)),
% 1.66/0.49 inference(forward_demodulation,[],[f423,f401])).
% 1.66/0.49 thf(f2390,plain,(
% 1.66/0.49 ($true != ((f4 @ $true))) | (~spl27_63 | spl27_70)),
% 1.66/0.49 inference(forward_demodulation,[],[f431,f401])).
% 1.66/0.49 thf(f2393,plain,(
% 1.66/0.49 ($false = ((f4 @ $true))) | (~spl27_71 | ~spl27_76)),
% 1.66/0.49 inference(forward_demodulation,[],[f459,f437])).
% 1.66/0.49 thf(f2421,plain,(
% 1.66/0.49 $false | (~spl27_17 | spl27_22 | ~spl27_63 | ~spl27_68)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2386,f1463])).
% 1.66/0.49 thf(f2422,plain,(
% 1.66/0.49 ~spl27_17 | spl27_22 | ~spl27_63 | ~spl27_68),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2421])).
% 1.66/0.49 thf(f2423,plain,(
% 1.66/0.49 $false | (~spl27_17 | ~spl27_24 | ~spl27_63 | spl27_70)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2390,f1465])).
% 1.66/0.49 thf(f2424,plain,(
% 1.66/0.49 ~spl27_17 | ~spl27_24 | ~spl27_63 | spl27_70),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2423])).
% 1.66/0.49 thf(f2425,plain,(
% 1.66/0.49 $false | (~spl27_17 | spl27_22 | ~spl27_71 | ~spl27_76)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2393,f1463])).
% 1.66/0.49 thf(f2426,plain,(
% 1.66/0.49 ~spl27_17 | spl27_22 | ~spl27_71 | ~spl27_76),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2425])).
% 1.66/0.49 thf(f2462,plain,(
% 1.66/0.49 spl27_43 | spl27_41),
% 1.66/0.49 inference(avatar_split_clause,[],[f1386,f299,f308])).
% 1.66/0.49 thf(f2463,plain,(
% 1.66/0.49 ($false = ((f1 @ $false))) | (~spl27_39 | ~spl27_42)),
% 1.66/0.49 inference(forward_demodulation,[],[f305,f292])).
% 1.66/0.49 thf(f2464,plain,(
% 1.66/0.49 ($true != ((f1 @ $false))) | (~spl27_39 | spl27_44)),
% 1.66/0.49 inference(forward_demodulation,[],[f313,f292])).
% 1.66/0.49 thf(f2465,plain,(
% 1.66/0.49 spl27_47 | spl27_45),
% 1.66/0.49 inference(avatar_split_clause,[],[f1712,f317,f326])).
% 1.66/0.49 thf(f2508,plain,(
% 1.66/0.49 ($true = ((f0 @ $false))) | (~spl27_101 | ~spl27_106)),
% 1.66/0.49 inference(forward_demodulation,[],[f594,f572])).
% 1.66/0.49 thf(f2533,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_51 | ~spl27_53 | ~spl27_101 | ~spl27_106)),
% 1.66/0.49 inference(forward_demodulation,[],[f2508,f740])).
% 1.66/0.49 thf(f2534,plain,(
% 1.66/0.49 $false | (~spl27_51 | ~spl27_53 | ~spl27_101 | ~spl27_106)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2533])).
% 1.66/0.49 thf(f2535,plain,(
% 1.66/0.49 ~spl27_51 | ~spl27_53 | ~spl27_101 | ~spl27_106),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2534])).
% 1.66/0.49 thf(f2545,plain,(
% 1.66/0.49 ($true = ((f0 @ $false))) | (~spl27_97 | ~spl27_102)),
% 1.66/0.49 inference(forward_demodulation,[],[f576,f554])).
% 1.66/0.49 thf(f2553,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_51 | ~spl27_53 | ~spl27_97 | ~spl27_102)),
% 1.66/0.49 inference(forward_demodulation,[],[f2545,f740])).
% 1.66/0.49 thf(f2554,plain,(
% 1.66/0.49 $false | (~spl27_51 | ~spl27_53 | ~spl27_97 | ~spl27_102)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2553])).
% 1.66/0.49 thf(f2555,plain,(
% 1.66/0.49 ~spl27_51 | ~spl27_53 | ~spl27_97 | ~spl27_102),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2554])).
% 1.66/0.49 thf(f2572,plain,(
% 1.66/0.49 $false | (~spl27_39 | ~spl27_42 | ~spl27_43 | spl27_46)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2463,f1210])).
% 1.66/0.49 thf(f2573,plain,(
% 1.66/0.49 ~spl27_39 | ~spl27_42 | ~spl27_43 | spl27_46),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2572])).
% 1.66/0.49 thf(f2574,plain,(
% 1.66/0.49 $false | (~spl27_39 | ~spl27_43 | spl27_44 | ~spl27_48)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2464,f1209])).
% 1.66/0.49 thf(f2575,plain,(
% 1.66/0.49 ~spl27_39 | ~spl27_43 | spl27_44 | ~spl27_48),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2574])).
% 1.66/0.49 thf(f2576,plain,(
% 1.66/0.49 ($false = ((f1 @ $true))) | (~spl27_45 | ~spl27_50)),
% 1.66/0.49 inference(forward_demodulation,[],[f341,f319])).
% 1.66/0.49 thf(f2597,plain,(
% 1.66/0.49 ($false != ((f1 @ $true))) | (~spl27_41 | spl27_46)),
% 1.66/0.49 inference(forward_demodulation,[],[f322,f301])).
% 1.66/0.49 thf(f2598,plain,(
% 1.66/0.49 ($true = ((f1 @ $true))) | (~spl27_41 | ~spl27_48)),
% 1.66/0.49 inference(forward_demodulation,[],[f332,f301])).
% 1.66/0.49 thf(f2601,plain,(
% 1.66/0.49 $false | (~spl27_41 | ~spl27_45 | spl27_46 | ~spl27_50)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2597,f2576])).
% 1.66/0.49 thf(f2602,plain,(
% 1.66/0.49 ~spl27_41 | ~spl27_45 | spl27_46 | ~spl27_50),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2601])).
% 1.66/0.49 thf(f2603,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_41 | ~spl27_45 | ~spl27_48 | ~spl27_50)),
% 1.66/0.49 inference(forward_demodulation,[],[f2598,f2576])).
% 1.66/0.49 thf(f2604,plain,(
% 1.66/0.49 $false | (~spl27_41 | ~spl27_45 | ~spl27_48 | ~spl27_50)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2603])).
% 1.66/0.49 thf(f2605,plain,(
% 1.66/0.49 ~spl27_41 | ~spl27_45 | ~spl27_48 | ~spl27_50),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2604])).
% 1.66/0.49 thf(f2616,plain,(
% 1.66/0.49 ($true = ((f0 @ $false))) | (~spl27_51 | ~spl27_54)),
% 1.66/0.49 inference(forward_demodulation,[],[f360,f346])).
% 1.66/0.49 thf(f2617,plain,(
% 1.66/0.49 spl27_97 | spl27_95),
% 1.66/0.49 inference(avatar_split_clause,[],[f1446,f543,f552])).
% 1.66/0.49 thf(f2626,plain,(
% 1.66/0.49 spl27_105 | spl27_103),
% 1.66/0.49 inference(avatar_split_clause,[],[f1818,f579,f588])).
% 1.66/0.49 thf(f2637,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_51 | ~spl27_54 | ~spl27_97 | ~spl27_100)),
% 1.66/0.49 inference(forward_demodulation,[],[f2616,f860])).
% 1.66/0.49 thf(f2638,plain,(
% 1.66/0.49 $false | (~spl27_51 | ~spl27_54 | ~spl27_97 | ~spl27_100)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2637])).
% 1.66/0.49 thf(f2639,plain,(
% 1.66/0.49 ~spl27_51 | ~spl27_54 | ~spl27_97 | ~spl27_100),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2638])).
% 1.66/0.49 thf(f2654,plain,(
% 1.66/0.49 ($true != ((f0 @ $true))) | (~spl27_103 | spl27_108)),
% 1.66/0.49 inference(forward_demodulation,[],[f603,f581])).
% 1.66/0.49 thf(f2657,plain,(
% 1.66/0.49 $false | (~spl27_99 | ~spl27_103 | ~spl27_106 | spl27_108)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2654,f1169])).
% 1.66/0.49 thf(f2658,plain,(
% 1.66/0.49 ~spl27_99 | ~spl27_103 | ~spl27_106 | spl27_108),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2657])).
% 1.66/0.49 thf(f2680,plain,(
% 1.66/0.49 ($false != ((f1 @ $true))) | (~spl27_91 | spl27_96)),
% 1.66/0.49 inference(forward_demodulation,[],[f548,f527])).
% 1.66/0.49 thf(f2682,plain,(
% 1.66/0.49 ($true = ((f1 @ $true))) | (~spl27_91 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f558,f527])).
% 1.66/0.49 thf(f2699,plain,(
% 1.66/0.49 $false | (~spl27_37 | ~spl27_42 | ~spl27_91 | spl27_96)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2680,f1225])).
% 1.66/0.49 thf(f2700,plain,(
% 1.66/0.49 ~spl27_37 | ~spl27_42 | ~spl27_91 | spl27_96),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2699])).
% 1.66/0.49 thf(f2701,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_37 | ~spl27_42 | ~spl27_91 | ~spl27_98)),
% 1.66/0.49 inference(forward_demodulation,[],[f2682,f1225])).
% 1.66/0.49 thf(f2702,plain,(
% 1.66/0.49 $false | (~spl27_37 | ~spl27_42 | ~spl27_91 | ~spl27_98)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2701])).
% 1.66/0.49 thf(f2703,plain,(
% 1.66/0.49 ~spl27_37 | ~spl27_42 | ~spl27_91 | ~spl27_98),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2702])).
% 1.66/0.49 thf(f2708,plain,(
% 1.66/0.49 ($false != ((f1 @ $true))) | (~spl27_37 | spl27_42)),
% 1.66/0.49 inference(forward_demodulation,[],[f304,f283])).
% 1.66/0.49 thf(f2716,plain,(
% 1.66/0.49 ($true = ((f1 @ $true))) | (~spl27_37 | ~spl27_44)),
% 1.66/0.49 inference(forward_demodulation,[],[f314,f283])).
% 1.66/0.49 thf(f2729,plain,(
% 1.66/0.49 $false | (~spl27_37 | ~spl27_41 | spl27_42 | ~spl27_46)),
% 1.66/0.49 inference(forward_subsumption_resolution,[],[f2708,f903])).
% 1.66/0.49 thf(f2730,plain,(
% 1.66/0.49 ~spl27_37 | ~spl27_41 | spl27_42 | ~spl27_46),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2729])).
% 1.66/0.49 thf(f2731,plain,(
% 1.66/0.49 ($true = $false) | (~spl27_37 | ~spl27_41 | ~spl27_44 | ~spl27_46)),
% 1.66/0.49 inference(forward_demodulation,[],[f2716,f903])).
% 1.66/0.49 thf(f2732,plain,(
% 1.66/0.49 $false | (~spl27_37 | ~spl27_41 | ~spl27_44 | ~spl27_46)),
% 1.66/0.49 inference(trivial_inequality_removal,[],[f2731])).
% 1.66/0.49 thf(f2733,plain,(
% 1.66/0.49 ~spl27_37 | ~spl27_41 | ~spl27_44 | ~spl27_46),
% 1.66/0.49 inference(avatar_contradiction_clause,[],[f2732])).
% 1.66/0.49 cnf(s1, plain, spl27_1 | spl27_2, inference(sat_conversion,[],[f126])).
% 1.66/0.49 cnf(s2, plain, spl27_3 | spl27_4, inference(sat_conversion,[],[f135])).
% 1.66/0.49 cnf(s3, plain, spl27_5 | spl27_6, inference(sat_conversion,[],[f144])).
% 1.66/0.49 cnf(s4, plain, spl27_7 | spl27_8, inference(sat_conversion,[],[f153])).
% 1.66/0.49 cnf(s5, plain, spl27_9 | spl27_10, inference(sat_conversion,[],[f162])).
% 1.66/0.49 cnf(s6, plain, spl27_11 | spl27_12, inference(sat_conversion,[],[f171])).
% 1.66/0.49 cnf(s7, plain, spl27_13 | spl27_14, inference(sat_conversion,[],[f180])).
% 1.66/0.49 cnf(s8, plain, spl27_15 | spl27_16, inference(sat_conversion,[],[f189])).
% 1.66/0.49 cnf(s9, plain, spl27_17 | spl27_18, inference(sat_conversion,[],[f198])).
% 1.66/0.49 cnf(s10, plain, spl27_19 | spl27_20, inference(sat_conversion,[],[f207])).
% 1.66/0.49 cnf(s11, plain, spl27_21 | spl27_22, inference(sat_conversion,[],[f216])).
% 1.66/0.49 cnf(s12, plain, spl27_23 | spl27_24, inference(sat_conversion,[],[f225])).
% 1.66/0.49 cnf(s13, plain, spl27_25 | spl27_26, inference(sat_conversion,[],[f234])).
% 1.66/0.49 cnf(s14, plain, spl27_27 | spl27_28, inference(sat_conversion,[],[f243])).
% 1.66/0.49 cnf(s15, plain, spl27_29 | spl27_30, inference(sat_conversion,[],[f252])).
% 1.66/0.49 cnf(s16, plain, spl27_31 | spl27_32, inference(sat_conversion,[],[f261])).
% 1.66/0.49 cnf(s17, plain, spl27_33 | spl27_34, inference(sat_conversion,[],[f270])).
% 1.66/0.49 cnf(s18, plain, spl27_35 | spl27_36, inference(sat_conversion,[],[f279])).
% 1.66/0.49 cnf(s19, plain, spl27_37 | spl27_38, inference(sat_conversion,[],[f288])).
% 1.66/0.49 cnf(s20, plain, spl27_39 | spl27_40, inference(sat_conversion,[],[f297])).
% 1.66/0.49 cnf(s21, plain, spl27_41 | spl27_42, inference(sat_conversion,[],[f306])).
% 1.66/0.49 cnf(s22, plain, spl27_43 | spl27_44, inference(sat_conversion,[],[f315])).
% 1.66/0.49 cnf(s23, plain, spl27_45 | spl27_46, inference(sat_conversion,[],[f324])).
% 1.66/0.49 cnf(s24, plain, spl27_47 | spl27_48, inference(sat_conversion,[],[f333])).
% 1.66/0.49 cnf(s25, plain, spl27_49 | spl27_50, inference(sat_conversion,[],[f342])).
% 1.66/0.49 cnf(s26, plain, spl27_51 | spl27_52, inference(sat_conversion,[],[f351])).
% 1.66/0.49 cnf(s27, plain, spl27_4 | spl27_53, inference(sat_conversion,[],[f356])).
% 1.66/0.49 cnf(s28, plain, spl27_2 | spl27_54, inference(sat_conversion,[],[f361])).
% 1.66/0.49 cnf(s29, plain, spl27_55 | spl27_56, inference(sat_conversion,[],[f370])).
% 1.66/0.49 cnf(s30, plain, spl27_57 | spl27_58, inference(sat_conversion,[],[f379])).
% 1.66/0.49 cnf(s31, plain, spl27_59 | spl27_60, inference(sat_conversion,[],[f388])).
% 1.66/0.49 cnf(s32, plain, spl27_61 | spl27_62, inference(sat_conversion,[],[f397])).
% 1.66/0.49 cnf(s33, plain, spl27_63 | spl27_64, inference(sat_conversion,[],[f406])).
% 1.66/0.49 cnf(s34, plain, spl27_65 | spl27_66, inference(sat_conversion,[],[f415])).
% 1.66/0.49 cnf(s35, plain, spl27_67 | spl27_68, inference(sat_conversion,[],[f424])).
% 1.66/0.49 cnf(s36, plain, spl27_69 | spl27_70, inference(sat_conversion,[],[f433])).
% 1.66/0.49 cnf(s37, plain, spl27_71 | spl27_72, inference(sat_conversion,[],[f442])).
% 1.66/0.49 cnf(s38, plain, spl27_73 | spl27_74, inference(sat_conversion,[],[f451])).
% 1.66/0.49 cnf(s39, plain, spl27_75 | spl27_76, inference(sat_conversion,[],[f460])).
% 1.66/0.49 cnf(s40, plain, spl27_77 | spl27_78, inference(sat_conversion,[],[f469])).
% 1.66/0.49 cnf(s41, plain, spl27_79 | spl27_80, inference(sat_conversion,[],[f478])).
% 1.66/0.49 cnf(s42, plain, spl27_81 | spl27_82, inference(sat_conversion,[],[f487])).
% 1.66/0.49 cnf(s43, plain, spl27_83 | spl27_84, inference(sat_conversion,[],[f496])).
% 1.66/0.49 cnf(s44, plain, spl27_85 | spl27_86, inference(sat_conversion,[],[f505])).
% 1.66/0.49 cnf(s45, plain, spl27_87 | spl27_88, inference(sat_conversion,[],[f514])).
% 1.66/0.49 cnf(s46, plain, spl27_89 | spl27_90, inference(sat_conversion,[],[f523])).
% 1.66/0.49 cnf(s47, plain, spl27_91 | spl27_92, inference(sat_conversion,[],[f532])).
% 1.66/0.49 cnf(s48, plain, spl27_93 | spl27_94, inference(sat_conversion,[],[f541])).
% 1.66/0.49 cnf(s49, plain, spl27_95 | spl27_96, inference(sat_conversion,[],[f550])).
% 1.66/0.49 cnf(s50, plain, spl27_97 | spl27_98, inference(sat_conversion,[],[f559])).
% 1.66/0.49 cnf(s51, plain, spl27_99 | spl27_100, inference(sat_conversion,[],[f568])).
% 1.66/0.49 cnf(s52, plain, spl27_101 | spl27_102, inference(sat_conversion,[],[f577])).
% 1.66/0.49 cnf(s53, plain, spl27_103 | spl27_104, inference(sat_conversion,[],[f586])).
% 1.66/0.49 cnf(s54, plain, spl27_105 | spl27_106, inference(sat_conversion,[],[f595])).
% 1.66/0.49 cnf(s55, plain, spl27_3 | spl27_107, inference(sat_conversion,[],[f600])).
% 1.66/0.49 cnf(s56, plain, spl27_1 | spl27_108, inference(sat_conversion,[],[f605])).
% 1.66/0.49 cnf(s57, plain, ~spl27_2 | ~spl27_4, inference(sat_conversion,[],[f608])).
% 1.66/0.49 cnf(s59, plain, ~spl27_5 | ~spl27_7, inference(sat_conversion,[],[f627])).
% 1.66/0.49 cnf(s61, plain, ~spl27_9 | ~spl27_11, inference(sat_conversion,[],[f636])).
% 1.66/0.49 cnf(s63, plain, ~spl27_13 | ~spl27_15, inference(sat_conversion,[],[f646])).
% 1.66/0.49 cnf(s65, plain, ~spl27_17 | ~spl27_19, inference(sat_conversion,[],[f656])).
% 1.66/0.49 cnf(s67, plain, ~spl27_21 | ~spl27_23, inference(sat_conversion,[],[f666])).
% 1.66/0.49 cnf(s69, plain, ~spl27_25 | ~spl27_27, inference(sat_conversion,[],[f676])).
% 1.66/0.49 cnf(s71, plain, ~spl27_29 | ~spl27_31, inference(sat_conversion,[],[f686])).
% 1.66/0.49 cnf(s75, plain, ~spl27_37 | ~spl27_39, inference(sat_conversion,[],[f706])).
% 1.66/0.49 cnf(s77, plain, ~spl27_41 | ~spl27_43, inference(sat_conversion,[],[f716])).
% 1.66/0.49 cnf(s83, plain, ~spl27_55 | ~spl27_57, inference(sat_conversion,[],[f747])).
% 1.66/0.49 cnf(s85, plain, ~spl27_59 | ~spl27_61, inference(sat_conversion,[],[f757])).
% 1.66/0.49 cnf(s99, plain, ~spl27_87 | ~spl27_89, inference(sat_conversion,[],[f827])).
% 1.66/0.49 cnf(s103, plain, ~spl27_95 | ~spl27_97, inference(sat_conversion,[],[f847])).
% 1.66/0.49 cnf(s108, plain, ~spl27_51 | ~spl27_53 | ~spl27_105 | ~spl27_108, inference(sat_conversion,[],[f874])).
% 1.66/0.49 cnf(s110, plain, ~spl27_39 | ~spl27_42 | ~spl27_47 | ~spl27_52, inference(sat_conversion,[],[f881])).
% 1.66/0.49 cnf(s111, plain, ~spl27_101 | ~spl27_104 | ~spl27_105 | ~spl27_108, inference(sat_conversion,[],[f886])).
% 1.66/0.49 cnf(s112, plain, ~spl27_43 | ~spl27_46 | ~spl27_47 | ~spl27_52, inference(sat_conversion,[],[f889])).
% 1.66/0.49 cnf(s114, plain, ~spl27_43 | ~spl27_46 | ~spl27_93 | ~spl27_98, inference(sat_conversion,[],[f895])).
% 1.66/0.49 cnf(s115, plain, ~spl27_100 | ~spl27_102, inference(sat_conversion,[],[f902])).
% 1.66/0.49 cnf(s117, plain, ~spl27_47 | ~spl27_50 | ~spl27_93 | ~spl27_98, inference(sat_conversion,[],[f909])).
% 1.66/0.49 cnf(s119, plain, ~spl27_39 | ~spl27_44 | ~spl27_47 | ~spl27_50, inference(sat_conversion,[],[f915])).
% 1.66/0.49 cnf(s123, plain, ~spl27_39 | ~spl27_44 | ~spl27_93 | ~spl27_96, inference(sat_conversion,[],[f927])).
% 1.66/0.49 cnf(s125, plain, ~spl27_96 | ~spl27_98, inference(sat_conversion,[],[f936])).
% 1.66/0.49 cnf(s126, plain, ~spl27_35 | ~spl27_38 | ~spl27_89 | ~spl27_94, inference(sat_conversion,[],[f942])).
% 1.66/0.49 cnf(s127, plain, ~spl27_92 | ~spl27_94, inference(sat_conversion,[],[f946])).
% 1.66/0.49 cnf(s128, plain, ~spl27_35 | ~spl27_38 | ~spl27_85 | ~spl27_90, inference(sat_conversion,[],[f949])).
% 1.66/0.49 cnf(s129, plain, ~spl27_88 | ~spl27_90, inference(sat_conversion,[],[f953])).
% 1.66/0.49 cnf(s130, plain, ~spl27_35 | ~spl27_38 | ~spl27_81 | ~spl27_86, inference(sat_conversion,[],[f956])).
% 1.66/0.49 cnf(s132, plain, ~spl27_23 | ~spl27_26 | ~spl27_77 | ~spl27_82, inference(sat_conversion,[],[f963])).
% 1.66/0.49 cnf(s133, plain, ~spl27_80 | ~spl27_82, inference(sat_conversion,[],[f967])).
% 1.66/0.49 cnf(s134, plain, ~spl27_19 | ~spl27_22 | ~spl27_73 | ~spl27_78, inference(sat_conversion,[],[f970])).
% 1.66/0.49 cnf(s135, plain, ~spl27_76 | ~spl27_78, inference(sat_conversion,[],[f974])).
% 1.66/0.49 cnf(s137, plain, ~spl27_72 | ~spl27_74, inference(sat_conversion,[],[f981])).
% 1.66/0.49 cnf(s138, plain, ~spl27_19 | ~spl27_22 | ~spl27_65 | ~spl27_70, inference(sat_conversion,[],[f984])).
% 1.66/0.49 cnf(s139, plain, ~spl27_68 | ~spl27_70, inference(sat_conversion,[],[f988])).
% 1.66/0.49 cnf(s140, plain, ~spl27_15 | ~spl27_18 | ~spl27_61 | ~spl27_66, inference(sat_conversion,[],[f991])).
% 1.66/0.49 cnf(s141, plain, ~spl27_64 | ~spl27_66, inference(sat_conversion,[],[f995])).
% 1.66/0.49 cnf(s143, plain, ~spl27_5 | ~spl27_8 | ~spl27_56 | ~spl27_57 | ~spl27_60, inference(sat_conversion,[],[f1089])).
% 1.66/0.49 cnf(s145, plain, ~spl27_6 | spl27_109 | spl27_110, inference(sat_conversion,[],[f1120])).
% 1.66/0.49 cnf(s147, plain, ~spl27_49 | ~spl27_53 | spl27_97 | spl27_100, inference(sat_conversion,[],[f1142])).
% 1.66/0.49 cnf(s148, plain, ~spl27_104 | ~spl27_106, inference(sat_conversion,[],[f1147])).
% 1.66/0.49 cnf(s149, plain, ~spl27_49 | ~spl27_53 | ~spl27_103 | ~spl27_108, inference(sat_conversion,[],[f1151])).
% 1.66/0.49 cnf(s152, plain, ~spl27_49 | ~spl27_54 | ~spl27_95 | ~spl27_100, inference(sat_conversion,[],[f1164])).
% 1.66/0.49 cnf(s154, plain, ~spl27_1 | ~spl27_3, inference(sat_conversion,[],[f1176])).
% 1.66/0.49 cnf(s155, plain, ~spl27_95 | spl27_100 | ~spl27_103 | ~spl27_107, inference(sat_conversion,[],[f1181])).
% 1.66/0.49 cnf(s158, plain, ~spl27_35 | ~spl27_40 | ~spl27_89 | spl27_94, inference(sat_conversion,[],[f1198])).
% 1.66/0.49 cnf(s159, plain, ~spl27_35 | spl27_38 | ~spl27_81 | ~spl27_84, inference(sat_conversion,[],[f1200])).
% 1.66/0.49 cnf(s160, plain, spl27_37 | spl27_39, inference(sat_conversion,[],[f1203])).
% 1.66/0.49 cnf(s163, plain, ~spl27_23 | ~spl27_26 | ~spl27_31 | ~spl27_36, inference(sat_conversion,[],[f1228])).
% 1.66/0.49 cnf(s165, plain, ~spl27_34 | ~spl27_36, inference(sat_conversion,[],[f1234])).
% 1.66/0.49 cnf(s166, plain, ~spl27_23 | ~spl27_26 | ~spl27_27 | ~spl27_32, inference(sat_conversion,[],[f1237])).
% 1.66/0.49 cnf(s167, plain, ~spl27_23 | ~spl27_28 | ~spl27_77 | ~spl27_80, inference(sat_conversion,[],[f1245])).
% 1.66/0.49 cnf(s170, plain, ~spl27_69 | ~spl27_73 | spl27_74 | ~spl27_78, inference(sat_conversion,[],[f1259])).
% 1.66/0.49 cnf(s176, plain, ~spl27_7 | spl27_12 | ~spl27_61 | ~spl27_66, inference(sat_conversion,[],[f1298])).
% 1.66/0.49 cnf(s180, plain, ~spl27_63 | ~spl27_67 | ~spl27_70 | ~spl27_72, inference(sat_conversion,[],[f1307])).
% 1.66/0.49 cnf(s182, plain, ~spl27_7 | ~spl27_10 | ~spl27_11 | ~spl27_16, inference(sat_conversion,[],[f1319])).
% 1.66/0.49 cnf(s183, plain, ~spl27_7 | ~spl27_12 | ~spl27_61 | spl27_66, inference(sat_conversion,[],[f1327])).
% 1.66/0.49 cnf(s185, plain, spl27_67 | spl27_69, inference(sat_conversion,[],[f1337])).
% 1.66/0.49 cnf(s191, plain, ~spl27_7 | ~spl27_56 | ~spl27_58, inference(sat_conversion,[],[f1365])).
% 1.66/0.49 cnf(s192, plain, ~spl27_65 | ~spl27_69 | spl27_70 | ~spl27_74, inference(sat_conversion,[],[f1367])).
% 1.66/0.49 cnf(s194, plain, ~spl27_43 | ~spl27_46 | ~spl27_48, inference(sat_conversion,[],[f1391])).
% 1.66/0.49 cnf(s197, plain, ~spl27_85 | ~spl27_88 | ~spl27_89 | ~spl27_94, inference(sat_conversion,[],[f1404])).
% 1.66/0.49 cnf(s198, plain, ~spl27_37 | ~spl27_44 | ~spl27_91 | spl27_98, inference(sat_conversion,[],[f1406])).
% 1.66/0.49 cnf(s201, plain, ~spl27_47 | ~spl27_52 | ~spl27_93 | spl27_98, inference(sat_conversion,[],[f1419])).
% 1.66/0.49 cnf(s202, plain, ~spl27_17 | ~spl27_22 | ~spl27_71 | spl27_76, inference(sat_conversion,[],[f1459])).
% 1.66/0.49 cnf(s203, plain, spl27_19 | ~spl27_22 | ~spl27_71 | spl27_76, inference(sat_conversion,[],[f1462])).
% 1.66/0.49 cnf(s205, plain, ~spl27_38 | ~spl27_40, inference(sat_conversion,[],[f1487])).
% 1.66/0.49 cnf(s206, plain, ~spl27_33 | ~spl27_40 | ~spl27_79 | ~spl27_84, inference(sat_conversion,[],[f1490])).
% 1.66/0.49 cnf(s208, plain, ~spl27_25 | ~spl27_29 | ~spl27_32 | spl27_36, inference(sat_conversion,[],[f1504])).
% 1.66/0.49 cnf(s210, plain, ~spl27_79 | spl27_84 | ~spl27_87 | ~spl27_92, inference(sat_conversion,[],[f1520])).
% 1.66/0.49 cnf(s211, plain, ~spl27_83 | ~spl27_87 | spl27_88 | ~spl27_92, inference(sat_conversion,[],[f1522])).
% 1.66/0.49 cnf(s212, plain, spl27_87 | spl27_89, inference(sat_conversion,[],[f1523])).
% 1.66/0.49 cnf(s214, plain, spl27_83 | spl27_85, inference(sat_conversion,[],[f1538])).
% 1.66/0.49 cnf(s216, plain, ~spl27_25 | ~spl27_30 | ~spl27_75 | ~spl27_82, inference(sat_conversion,[],[f1552])).
% 1.66/0.49 cnf(s220, plain, ~spl27_45 | ~spl27_52 | ~spl27_91 | ~spl27_96, inference(sat_conversion,[],[f1579])).
% 1.66/0.49 cnf(s223, plain, ~spl27_41 | spl27_46 | ~spl27_91 | ~spl27_96, inference(sat_conversion,[],[f1586])).
% 1.66/0.49 cnf(s226, plain, ~spl27_79 | ~spl27_84 | ~spl27_87 | ~spl27_94, inference(sat_conversion,[],[f1597])).
% 1.66/0.49 cnf(s229, plain, ~spl27_33 | spl27_40 | ~spl27_83 | ~spl27_90, inference(sat_conversion,[],[f1613])).
% 1.66/0.49 cnf(s232, plain, ~spl27_79 | ~spl27_83 | ~spl27_86 | ~spl27_88, inference(sat_conversion,[],[f1626])).
% 1.66/0.49 cnf(s234, plain, ~spl27_79 | ~spl27_83 | spl27_84 | ~spl27_88, inference(sat_conversion,[],[f1630])).
% 1.66/0.49 cnf(s236, plain, ~spl27_21 | ~spl27_28 | ~spl27_75 | ~spl27_80, inference(sat_conversion,[],[f1646])).
% 1.66/0.49 cnf(s237, plain, spl27_71 | spl27_73, inference(sat_conversion,[],[f1651])).
% 1.66/0.49 cnf(s240, plain, ~spl27_13 | ~spl27_18 | ~spl27_59 | spl27_64, inference(sat_conversion,[],[f1679])).
% 1.66/0.49 cnf(s241, plain, spl27_59 | spl27_61, inference(sat_conversion,[],[f1680])).
% 1.66/0.49 cnf(s244, plain, ~spl27_22 | ~spl27_24, inference(sat_conversion,[],[f1742])).
% 1.66/0.49 cnf(s247, plain, ~spl27_60 | ~spl27_62, inference(sat_conversion,[],[f1773])).
% 1.66/0.49 cnf(s248, plain, ~spl27_55 | ~spl27_62 | ~spl27_110, inference(sat_conversion,[],[f1776])).
% 1.66/0.49 cnf(s251, plain, ~spl27_103 | ~spl27_107 | ~spl27_108, inference(sat_conversion,[],[f1797])).
% 1.66/0.49 cnf(s252, plain, ~spl27_49 | ~spl27_54 | ~spl27_99 | spl27_106, inference(sat_conversion,[],[f1804])).
% 1.66/0.49 cnf(s253, plain, ~spl27_97 | spl27_100 | ~spl27_105 | ~spl27_107, inference(sat_conversion,[],[f1806])).
% 1.66/0.49 cnf(s255, plain, ~spl27_27 | ~spl27_30 | ~spl27_31 | ~spl27_36, inference(sat_conversion,[],[f1830])).
% 1.66/0.49 cnf(s256, plain, spl27_21 | spl27_23, inference(sat_conversion,[],[f1831])).
% 1.66/0.49 cnf(s262, plain, spl27_25 | spl27_27, inference(sat_conversion,[],[f1875])).
% 1.66/0.49 cnf(s263, plain, ~spl27_23 | ~spl27_28 | ~spl27_31 | spl27_36, inference(sat_conversion,[],[f1878])).
% 1.66/0.49 cnf(s266, plain, ~spl27_9 | ~spl27_13 | ~spl27_16 | ~spl27_18, inference(sat_conversion,[],[f1956])).
% 1.66/0.49 cnf(s267, plain, spl27_9 | spl27_11, inference(sat_conversion,[],[f1958])).
% 1.66/0.49 cnf(s268, plain, ~spl27_14 | ~spl27_16, inference(sat_conversion,[],[f1968])).
% 1.66/0.49 cnf(s276, plain, ~spl27_10 | ~spl27_12, inference(sat_conversion,[],[f2019])).
% 1.66/0.49 cnf(s278, plain, ~spl27_18 | ~spl27_20, inference(sat_conversion,[],[f2029])).
% 1.66/0.49 cnf(s280, plain, spl27_7 | ~spl27_55 | ~spl27_58 | spl27_62, inference(sat_conversion,[],[f2038])).
% 1.66/0.49 cnf(s281, plain, ~spl27_5 | ~spl27_58 | ~spl27_110, inference(sat_conversion,[],[f2045])).
% 1.66/0.49 cnf(s288, plain, ~spl27_5 | ~spl27_10 | ~spl27_13 | spl27_18, inference(sat_conversion,[],[f2077])).
% 1.66/0.49 cnf(s289, plain, ~spl27_13 | ~spl27_20 | ~spl27_59 | spl27_66, inference(sat_conversion,[],[f2079])).
% 1.66/0.49 cnf(s290, plain, spl27_5 | spl27_7, inference(sat_conversion,[],[f2084])).
% 1.66/0.49 cnf(s291, plain, ~spl27_6 | ~spl27_7 | spl27_56 | ~spl27_109, inference(sat_conversion,[],[f2098])).
% 1.66/0.49 cnf(s295, plain, ~spl27_7 | ~spl27_56 | ~spl27_57 | ~spl27_62, inference(sat_conversion,[],[f2117])).
% 1.66/0.49 cnf(s298, plain, spl27_17 | spl27_19, inference(sat_conversion,[],[f2121])).
% 1.66/0.49 cnf(s300, plain, ~spl27_21 | ~spl27_26 | ~spl27_75 | spl27_80, inference(sat_conversion,[],[f2127])).
% 1.66/0.49 cnf(s311, plain, ~spl27_19 | ~spl27_24 | ~spl27_73 | ~spl27_76, inference(sat_conversion,[],[f2178])).
% 1.66/0.49 cnf(s312, plain, ~spl27_67 | ~spl27_71 | spl27_72 | ~spl27_76, inference(sat_conversion,[],[f2194])).
% 1.66/0.49 cnf(s313, plain, ~spl27_67 | ~spl27_71 | ~spl27_74 | spl27_78, inference(sat_conversion,[],[f2196])).
% 1.66/0.49 cnf(s321, plain, spl27_31 | spl27_34 | ~spl27_75 | ~spl27_80, inference(sat_conversion,[],[f2225])).
% 1.66/0.49 cnf(s323, plain, ~spl27_5 | ~spl27_56 | spl27_110, inference(sat_conversion,[],[f2233])).
% 1.66/0.49 cnf(s327, plain, spl27_29 | spl27_31, inference(sat_conversion,[],[f2244])).
% 1.66/0.49 cnf(s331, plain, ~spl27_11 | ~spl27_14 | ~spl27_15 | spl27_18, inference(sat_conversion,[],[f2290])).
% 1.66/0.49 cnf(s332, plain, ~spl27_11 | ~spl27_15 | spl27_16 | ~spl27_20, inference(sat_conversion,[],[f2292])).
% 1.66/0.49 cnf(s335, plain, ~spl27_5 | ~spl27_9 | spl27_10 | ~spl27_14, inference(sat_conversion,[],[f2319])).
% 1.66/0.49 cnf(s336, plain, ~spl27_5 | ~spl27_9 | ~spl27_12 | ~spl27_14, inference(sat_conversion,[],[f2322])).
% 1.66/0.49 cnf(s343, plain, ~spl27_5 | ~spl27_10 | ~spl27_59 | ~spl27_66, inference(sat_conversion,[],[f2357])).
% 1.66/0.49 cnf(s357, plain, ~spl27_17 | spl27_22 | ~spl27_63 | ~spl27_68, inference(sat_conversion,[],[f2422])).
% 1.66/0.49 cnf(s358, plain, ~spl27_17 | ~spl27_24 | ~spl27_63 | spl27_70, inference(sat_conversion,[],[f2424])).
% 1.66/0.49 cnf(s359, plain, ~spl27_17 | spl27_22 | ~spl27_71 | ~spl27_76, inference(sat_conversion,[],[f2426])).
% 1.66/0.49 cnf(s368, plain, spl27_41 | spl27_43, inference(sat_conversion,[],[f2462])).
% 1.66/0.49 cnf(s369, plain, spl27_45 | spl27_47, inference(sat_conversion,[],[f2465])).
% 1.66/0.49 cnf(s378, plain, ~spl27_51 | ~spl27_53 | ~spl27_101 | ~spl27_106, inference(sat_conversion,[],[f2535])).
% 1.66/0.49 cnf(s382, plain, ~spl27_51 | ~spl27_53 | ~spl27_97 | ~spl27_102, inference(sat_conversion,[],[f2555])).
% 1.66/0.49 cnf(s386, plain, ~spl27_39 | ~spl27_42 | ~spl27_43 | spl27_46, inference(sat_conversion,[],[f2573])).
% 1.66/0.49 cnf(s387, plain, ~spl27_39 | ~spl27_43 | spl27_44 | ~spl27_48, inference(sat_conversion,[],[f2575])).
% 1.66/0.49 cnf(s394, plain, ~spl27_41 | ~spl27_45 | spl27_46 | ~spl27_50, inference(sat_conversion,[],[f2602])).
% 1.66/0.49 cnf(s395, plain, ~spl27_41 | ~spl27_45 | ~spl27_48 | ~spl27_50, inference(sat_conversion,[],[f2605])).
% 1.66/0.49 cnf(s398, plain, spl27_95 | spl27_97, inference(sat_conversion,[],[f2617])).
% 1.66/0.49 cnf(s399, plain, spl27_103 | spl27_105, inference(sat_conversion,[],[f2626])).
% 1.66/0.49 cnf(s401, plain, ~spl27_51 | ~spl27_54 | ~spl27_97 | ~spl27_100, inference(sat_conversion,[],[f2639])).
% 1.66/0.49 cnf(s404, plain, ~spl27_99 | ~spl27_103 | ~spl27_106 | spl27_108, inference(sat_conversion,[],[f2658])).
% 1.66/0.49 cnf(s409, plain, ~spl27_37 | ~spl27_42 | ~spl27_91 | spl27_96, inference(sat_conversion,[],[f2700])).
% 1.66/0.49 cnf(s410, plain, ~spl27_37 | ~spl27_42 | ~spl27_91 | ~spl27_98, inference(sat_conversion,[],[f2703])).
% 1.66/0.49 cnf(s417, plain, ~spl27_37 | ~spl27_41 | spl27_42 | ~spl27_46, inference(sat_conversion,[],[f2730])).
% 1.66/0.49 cnf(s418, plain, ~spl27_37 | ~spl27_41 | ~spl27_44 | ~spl27_46, inference(sat_conversion,[],[f2733])).
% 1.66/0.49 cnf(s419, plain, ~spl27_56 | ~spl27_62 | ~spl27_7, inference(rat,[],[s30,s191,s295])).
% 1.66/0.49 cnf(s420, plain, ~spl27_62 | spl27_5, inference(rat,[],[s145,s248,s291,s29,s419,s290,s3])).
% 1.66/0.49 cnf(s421, plain, spl27_41 | ~spl27_93 | ~spl27_39 | spl27_1, inference(rat,[],[s378,s52,s54,s382,s108,s26,s110,s50,s24,s114,s194,s386,s21,s368,s56,s27,s57,s1])).
% 1.66/0.49 cnf(s423, plain, ~spl27_49 | spl27_97 | spl27_1, inference(rat,[],[s52,s111,s115,s53,s399,s147,s149,s56,s27,s57,s1])).
% 1.66/0.49 cnf(s424, plain, ~spl27_93 | ~spl27_39 | spl27_1, inference(rat,[],[s395,s24,s369,s119,s25,s423,s103,s49,s123,s22,s77,s421])).
% 1.66/0.49 cnf(s425, plain, spl27_37 | ~spl27_35 | ~spl27_81 | spl27_1, inference(rat,[],[s424,s48,s126,s46,s128,s44,s130,s19,s160])).
% 1.66/0.49 cnf(s426, plain, ~spl27_51 | ~spl27_97 | spl27_1, inference(rat,[],[s378,s52,s54,s382,s108,s56,s27,s57,s1])).
% 1.66/0.49 cnf(s427, plain, spl27_41 | ~spl27_91 | ~spl27_37 | spl27_1, inference(rat,[],[s112,s23,s369,s220,s26,s426,s50,s409,s410,s21,s368])).
% 1.66/0.49 cnf(s428, plain, ~spl27_91 | ~spl27_37 | spl27_1, inference(rat,[],[s423,s103,s25,s49,s394,s223,s23,s418,s22,s77,s427])).
% 1.66/0.49 cnf(s429, plain, ~spl27_35 | ~spl27_81 | spl27_1, inference(rat,[],[s129,s211,s46,s212,s158,s127,s47,s428,s43,s159,s205,s20,s75,s425])).
% 1.66/0.49 cnf(s430, plain, spl27_25 | ~spl27_77 | ~spl27_23 | spl27_1, inference(rat,[],[s429,s18,s163,s42,s16,s132,s166,s13,s262])).
% 1.66/0.49 cnf(s431, plain, spl27_36 | ~spl27_25 | ~spl27_23, inference(rat,[],[s208,s16,s327,s263,s14,s69])).
% 1.66/0.49 cnf(s432, plain, spl27_89 | ~spl27_94 | spl27_40 | ~spl27_33 | ~spl27_79, inference(rat,[],[s43,s229,s226,s46,s212])).
% 1.66/0.49 cnf(s433, plain, ~spl27_94 | spl27_40 | ~spl27_79 | ~spl27_33, inference(rat,[],[s232,s44,s214,s197,s45,s99,s432])).
% 1.66/0.49 cnf(s434, plain, spl27_37 | ~spl27_33 | ~spl27_79 | spl27_1, inference(rat,[],[s433,s48,s205,s424,s19,s160])).
% 1.66/0.49 cnf(s435, plain, ~spl27_92 | spl27_84 | ~spl27_79, inference(rat,[],[s234,s45,s43,s210])).
% 1.66/0.49 cnf(s436, plain, ~spl27_33 | ~spl27_79 | spl27_1, inference(rat,[],[s435,s206,s47,s20,s428,s75,s434])).
% 1.66/0.49 cnf(s437, plain, ~spl27_77 | ~spl27_23 | spl27_1, inference(rat,[],[s436,s17,s165,s431,s41,s167,s14,s69,s430])).
% 1.66/0.49 cnf(s438, plain, spl27_21 | ~spl27_65 | ~spl27_19 | spl27_1, inference(rat,[],[s437,s40,s170,s38,s192,s36,s138,s11,s256])).
% 1.66/0.49 cnf(s439, plain, ~spl27_75 | ~spl27_82 | spl27_36 | ~spl27_21, inference(rat,[],[s16,s208,s71,s15,s216,s13,s300,s133])).
% 1.66/0.49 cnf(s440, plain, ~spl27_76 | ~spl27_24 | ~spl27_65 | ~spl27_19, inference(rat,[],[s139,s192,s35,s185,s313,s38,s237,s311,s135])).
% 1.66/0.49 cnf(s441, plain, spl27_36 | ~spl27_75 | ~spl27_21 | spl27_1, inference(rat,[],[s42,s429,s439,s18])).
% 1.66/0.49 cnf(s442, plain, ~spl27_75 | ~spl27_21 | spl27_1, inference(rat,[],[s15,s255,s71,s14,s321,s236,s41,s436,s17,s165,s441])).
% 1.66/0.49 cnf(s443, plain, ~spl27_65 | ~spl27_19 | spl27_1, inference(rat,[],[s442,s39,s440,s12,s67,s438])).
% 1.66/0.49 cnf(s444, plain, spl27_9 | spl27_5 | spl27_1, inference(rat,[],[s443,s34,s176,s10,s332,s8,s182,s276,s5,s267,s290,s32,s420])).
% 1.66/0.49 cnf(s445, plain, ~spl27_18 | ~spl27_66 | ~spl27_9 | ~spl27_61, inference(rat,[],[s7,s266,s268,s8,s140])).
% 1.66/0.49 cnf(s446, plain, ~spl27_23 | spl27_5 | spl27_1, inference(rat,[],[s180,s36,s185,s170,s137,s37,s237,s202,s135,s40,s11,s437,s67,s33,s141,s9,s445,s183,s6,s61,s290,s444,s32,s420])).
% 1.66/0.49 cnf(s447, plain, spl27_5 | spl27_1, inference(rat,[],[s180,s37,s35,s359,s357,s39,s358,s244,s442,s12,s256,s446,s9,s445,s33,s141,s183,s6,s61,s444,s32,s420,s290])).
% 1.66/0.49 cnf(s448, plain, ~spl27_56 | ~spl27_60 | ~spl27_5, inference(rat,[],[s30,s281,s143,s323,s4,s59])).
% 1.66/0.49 cnf(s449, plain, ~spl27_60 | ~spl27_5, inference(rat,[],[s30,s280,s83,s29,s448,s247,s59])).
% 1.66/0.49 cnf(s450, plain, ~spl27_19 | spl27_1, inference(rat,[],[s7,s335,s5,s240,s343,s141,s34,s9,s443,s65,s31,s449,s447])).
% 1.66/0.49 cnf(s451, plain, ~spl27_14 | spl27_1, inference(rat,[],[s336,s6,s267,s332,s8,s268,s447,s10,s450])).
% 1.66/0.49 cnf(s452, plain, ~spl27_23 | spl27_1, inference(rat,[],[s180,s36,s185,s170,s137,s37,s237,s203,s135,s40,s11,s437,s67,s33,s141,s289,s7,s451,s10,s450,s31,s449,s447])).
% 1.66/0.49 cnf(s453, plain, spl27_1, inference(rat,[],[s180,s37,s35,s359,s357,s39,s358,s244,s442,s12,s256,s452,s33,s141,s289,s7,s451,s10,s298,s450,s31,s449,s447])).
% 1.66/0.49 cnf(s454, plain, ~spl27_3, inference(rat,[],[s154,s453])).
% 1.66/0.49 cnf(s455, plain, spl27_107, inference(rat,[],[s55,s454])).
% 1.66/0.49 cnf(s456, plain, spl27_4, inference(rat,[],[s2,s454])).
% 1.66/0.49 cnf(s457, plain, ~spl27_2, inference(rat,[],[s57,s456])).
% 1.66/0.49 cnf(s458, plain, spl27_54, inference(rat,[],[s28,s457])).
% 1.66/0.49 cnf(s459, plain, ~spl27_78 | ~spl27_22 | spl27_19 | ~spl27_63, inference(rat,[],[s180,s36,s185,s170,s137,s37,s237,s203,s135])).
% 1.66/0.49 cnf(s460, plain, ~spl27_70 | ~spl27_76 | ~spl27_63, inference(rat,[],[s312,s37,s180,s35,s139])).
% 1.66/0.49 cnf(s461, plain, spl27_41 | ~spl27_98 | ~spl27_93 | ~spl27_39, inference(rat,[],[s386,s114,s21,s368])).
% 1.66/0.49 cnf(s462, plain, ~spl27_49 | ~spl27_95, inference(rat,[],[s148,s252,s53,s51,s155,s152,s455,s458])).
% 1.66/0.49 cnf(s463, plain, spl27_97 | ~spl27_93 | ~spl27_39, inference(rat,[],[s395,s24,s369,s117,s25,s462,s461,s50,s398])).
% 1.66/0.49 cnf(s464, plain, ~spl27_103 | ~spl27_99 | ~spl27_106, inference(rat,[],[s251,s404,s455])).
% 1.66/0.49 cnf(s465, plain, spl27_100 | ~spl27_97, inference(rat,[],[s464,s54,s399,s51,s253,s455])).
% 1.66/0.49 cnf(s466, plain, ~spl27_51 | ~spl27_97, inference(rat,[],[s465,s401,s458])).
% 1.66/0.49 cnf(s467, plain, ~spl27_93 | ~spl27_39, inference(rat,[],[s466,s26,s201,s24,s387,s22,s123,s125,s49,s103,s463])).
% 1.66/0.49 cnf(s468, plain, spl27_37 | ~spl27_81 | ~spl27_35, inference(rat,[],[s467,s48,s126,s46,s128,s44,s130,s19,s160])).
% 1.66/0.49 cnf(s469, plain, spl27_42 | ~spl27_50 | ~spl27_37, inference(rat,[],[s394,s23,s417,s21])).
% 1.66/0.49 cnf(s470, plain, ~spl27_92 | ~spl27_83 | ~spl27_40 | ~spl27_35, inference(rat,[],[s129,s211,s46,s212,s158,s127])).
% 1.66/0.49 cnf(s471, plain, spl27_97 | ~spl27_91 | ~spl27_37, inference(rat,[],[s469,s25,s410,s462,s50,s398])).
% 1.66/0.49 cnf(s472, plain, ~spl27_91 | ~spl27_37, inference(rat,[],[s112,s22,s23,s369,s198,s220,s125,s26,s49,s466,s103,s471])).
% 1.66/0.49 cnf(s473, plain, ~spl27_81 | ~spl27_35, inference(rat,[],[s472,s47,s470,s43,s159,s205,s20,s75,s468])).
% 1.66/0.49 cnf(s474, plain, spl27_36 | ~spl27_77 | ~spl27_23, inference(rat,[],[s473,s42,s132,s13,s431,s18])).
% 1.66/0.49 cnf(s475, plain, ~spl27_27 | ~spl27_36 | ~spl27_23, inference(rat,[],[s16,s163,s166,s13,s69])).
% 1.66/0.49 cnf(s476, plain, spl27_37 | ~spl27_79 | ~spl27_33, inference(rat,[],[s433,s48,s205,s467,s19,s160])).
% 1.66/0.49 cnf(s477, plain, ~spl27_79 | ~spl27_33, inference(rat,[],[s435,s206,s47,s20,s472,s75,s476])).
% 1.66/0.49 cnf(s478, plain, ~spl27_77 | ~spl27_23, inference(rat,[],[s477,s41,s167,s14,s475,s17,s165,s474])).
% 1.66/0.49 cnf(s479, plain, ~spl27_23 | spl27_19 | ~spl27_63, inference(rat,[],[s478,s40,s459,s11,s67])).
% 1.66/0.49 cnf(s480, plain, spl27_36 | ~spl27_75 | ~spl27_21, inference(rat,[],[s42,s473,s439,s18])).
% 1.66/0.49 cnf(s481, plain, ~spl27_75 | ~spl27_21, inference(rat,[],[s15,s255,s71,s14,s321,s236,s41,s477,s17,s165,s480])).
% 1.66/0.49 cnf(s482, plain, ~spl27_17 | ~spl27_63, inference(rat,[],[s481,s39,s460,s358,s12,s256,s479,s65])).
% 1.66/0.49 cnf(s483, plain, spl27_61 | ~spl27_10 | ~spl27_66, inference(rat,[],[s420,s343,s32,s241])).
% 1.66/0.49 cnf(s484, plain, ~spl27_10 | ~spl27_66, inference(rat,[],[s449,s290,s31,s176,s85,s483,s276])).
% 1.66/0.49 cnf(s485, plain, ~spl27_66, inference(rat,[],[s336,s7,s420,s240,s32,s241,s6,s445,s61,s5,s484,s9,s482,s33,s141])).
% 1.66/0.49 cnf(s486, plain, spl27_65, inference(rat,[],[s34,s485])).
% 1.66/0.49 cnf(s489, plain, ~spl27_19 | ~spl27_23, inference(rat,[],[s192,s38,s36,s134,s138,s11,s67,s40,s478,s486])).
% 1.66/0.49 cnf(s490, plain, ~spl27_14 | ~spl27_11 | spl27_18, inference(rat,[],[s8,s331,s268])).
% 1.66/0.49 cnf(s491, plain, spl27_9 | spl27_18, inference(rat,[],[s182,s290,s8,s288,s63,s7,s490,s5,s267])).
% 1.66/0.49 cnf(s492, plain, spl27_5 | ~spl27_12, inference(rat,[],[s32,s183,s420,s290,s485])).
% 1.66/0.49 cnf(s493, plain, ~spl27_20, inference(rat,[],[s289,s7,s31,s336,s449,s492,s6,s61,s491,s278,s485])).
% 1.66/0.49 cnf(s494, plain, spl27_19, inference(rat,[],[s10,s493])).
% 1.66/0.49 cnf(s496, plain, ~spl27_23, inference(rat,[],[s489,s494])).
% 1.66/0.49 cnf(s498, plain, spl27_21, inference(rat,[],[s256,s496])).
% 1.66/0.49 cnf(s499, plain, spl27_24, inference(rat,[],[s12,s496])).
% 1.66/0.49 cnf(s500, plain, ~spl27_75, inference(rat,[],[s481,s498])).
% 1.66/0.49 cnf(s502, plain, ~spl27_76, inference(rat,[],[s440,s494,s486,s499])).
% 1.66/0.49 cnf(s504, plain, $false, inference(rat,[],[s39,s502,s500])).
% 1.66/0.49 thf(f2735,plain,(
% 1.66/0.49 $false),
% 1.66/0.49 inference(avatar_sat_refutation,[],[s504])).
% 1.66/0.49 % SZS output end Proof for theBenchmark
% 1.66/0.49 % (364818)------------------------------
% 1.66/0.49 % (364818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.66/0.49 % (364818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.49 % (364818)CaDiCaL version: 2.1.3
% 1.66/0.49 % (364818)Termination reason: Refutation
% 1.66/0.49 % (364818)Time elapsed: 0.060 s
% 1.66/0.49 % (364818)Peak memory usage: 13 MB
% 1.66/0.49 % (364818)Instructions burned: 114 (million)
% 1.66/0.49 % (364787)Success in time 0.246 s
% 1.66/0.49 % Vampire exiting
%------------------------------------------------------------------------------