%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500^1.005 : 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 : n011.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:19 AM UTC 2026
% Result : Theorem 0.75s 0.49s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.005 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n011.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 17:11:01 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 0.75/0.49 % (375133)Will run a generic schedule for satisfiability detection.
% 0.75/0.49 % (375139)% WARNING: option uhcvi not known.
% 0.75/0.49 % (375143)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2500959028:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.75/0.49 % (375139)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1432311681:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.75/0.49 % (375138)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1649339322_2999 on theBenchmark for (2999ds/0Mi)
% 0.75/0.49 % (375141)dis+10_1_sil=32000:sp=arity:random_seed=2380146408:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.75/0.49 % (375140)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1917925472:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.75/0.49 % (375139)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.75/0.49 % (375139)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.75/0.49 % Exception at run slice level
% 0.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.75/0.49 % (375144)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3896394107:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.75/0.49 % (375150)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=563245999:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.75/0.49 % Exception at run slice level
% 0.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.75/0.49 % (375142)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1395132657:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.75/0.49 % (375142)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.75/0.49 % (375154)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=821838909:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.75/0.49 % (375141)Instruction limit reached!
% 0.75/0.49 % (375141)------------------------------
% 0.75/0.49 % (375141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (375141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (375141)CaDiCaL version: 2.1.3
% 0.75/0.49 % (375141)Termination reason: Instruction limit
% 0.75/0.49 % (375141)Termination phase: Saturation
% 0.75/0.49 % (375141)Time elapsed: 0.052 s
% 0.75/0.49 % (375141)Peak memory usage: 12 MB
% 0.75/0.49 % (375141)Instructions burned: 104 (million)
% 0.75/0.49 % (375143)Instruction limit reached!
% 0.75/0.49 % (375143)------------------------------
% 0.75/0.49 % (375143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (375143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (375143)CaDiCaL version: 2.1.3
% 0.75/0.49 % (375143)Termination reason: Instruction limit
% 0.75/0.49 % (375143)Termination phase: Saturation
% 0.75/0.49 % (375143)Time elapsed: 0.060 s
% 0.75/0.49 % (375143)Peak memory usage: 12 MB
% 0.75/0.49 % (375143)Instructions burned: 131 (million)
% 0.75/0.49 % (375156)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=2751932263:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.75/0.49 % (375156)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.75/0.49 % (375156)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.75/0.49 % (375157)ott-21_1_sil=16000:fs=off:random_seed=3736420904:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.75/0.49 % (375154)Instruction limit reached!
% 0.75/0.49 % (375154)------------------------------
% 0.75/0.49 % (375154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (375154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (375154)CaDiCaL version: 2.1.3
% 0.75/0.49 % (375154)Termination reason: Instruction limit
% 0.75/0.49 % (375154)Termination phase: Saturation
% 0.75/0.49 % (375154)Time elapsed: 0.068 s
% 0.75/0.49 % (375154)Peak memory usage: 13 MB
% 0.75/0.49 % (375154)Instructions burned: 131 (million)
% 0.75/0.49 % (375160)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3416081181:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.75/0.49 % (375144)Instruction limit reached!
% 0.75/0.49 % (375144)------------------------------
% 0.75/0.49 % (375144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (375144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (375144)CaDiCaL version: 2.1.3
% 0.75/0.49 % (375144)Termination reason: Instruction limit
% 0.75/0.49 % (375144)Termination phase: Saturation
% 0.75/0.49 % (375144)Time elapsed: 0.115 s
% 0.75/0.49 % (375144)Peak memory usage: 12 MB
% 0.75/0.49 % (375144)Instructions burned: 159 (million)
% 0.75/0.49 % (375142)Instruction limit reached!
% 0.75/0.49 % (375142)------------------------------
% 0.75/0.49 % (375142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (375142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (375142)CaDiCaL version: 2.1.3
% 0.75/0.49 % (375142)Termination reason: Instruction limit
% 0.75/0.49 % (375142)Termination phase: Saturation
% 0.75/0.49 % (375142)Time elapsed: 0.125 s
% 0.75/0.49 % (375142)Peak memory usage: 12 MB
% 0.75/0.49 % (375142)Instructions burned: 116 (million)
% 0.75/0.49 % (375163)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2669010352:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.75/0.49 % (375162)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3913275895:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 0.75/0.49 % Exception at run slice level
% 0.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.75/0.49 % (375166)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1417833534:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 0.75/0.49 % Exception at run slice level
% 0.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.75/0.49 % (375163) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-375133-375163"...
% 0.75/0.49 % (375163)...printing done.
% 0.75/0.49 % (375163)Refutation found. Thanks to Tanya!
% 0.75/0.49 % SZS status Theorem for theBenchmark
% 0.75/0.49 % SZS output start Proof for theBenchmark
% 0.75/0.49 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.75/0.49 thf(func_def_0, type, x: $o).
% 0.75/0.49 thf(func_def_1, type, f0: ($o > $o)).
% 0.75/0.49 thf(func_def_2, type, f1: ($o > $o)).
% 0.75/0.49 thf(func_def_3, type, f2: ($o > $o)).
% 0.75/0.49 thf(func_def_4, type, f3: ($o > $o)).
% 0.75/0.49 thf(func_def_5, type, f4: ($o > $o)).
% 0.75/0.49 thf(func_def_9, type, sF0: $o).
% 0.75/0.49 thf(func_def_10, type, sF1: $o).
% 0.75/0.49 thf(func_def_11, type, sF2: $o).
% 0.75/0.49 thf(func_def_12, type, sF3: $o).
% 0.75/0.49 thf(func_def_13, type, sF4: $o).
% 0.75/0.49 thf(func_def_14, type, sF5: $o).
% 0.75/0.49 thf(func_def_15, type, sF6: $o).
% 0.75/0.49 thf(func_def_16, type, sF7: $o).
% 0.75/0.49 thf(func_def_17, type, sF8: $o).
% 0.75/0.49 thf(func_def_18, type, sF9: $o).
% 0.75/0.49 thf(func_def_19, type, sF10: $o).
% 0.75/0.49 thf(func_def_20, type, sF11: $o).
% 0.75/0.49 thf(func_def_21, type, sF12: $o).
% 0.75/0.49 thf(func_def_22, type, sF13: $o).
% 0.75/0.49 thf(func_def_23, type, sF14: $o).
% 0.75/0.49 thf(func_def_24, type, sF15: $o).
% 0.75/0.49 thf(func_def_25, type, sF16: $o).
% 0.75/0.49 thf(func_def_26, type, sF17: $o).
% 0.75/0.49 thf(func_def_27, type, sF18: $o).
% 0.75/0.49 thf(func_def_28, type, vNOT: ($o > $o)).
% 0.75/0.49 thf(f1,conjecture,(
% 0.75/0.49 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.75/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski5)).
% 0.75/0.49 thf(f2,negated_conjecture,(
% 0.75/0.49 ~ (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.75/0.49 inference(negated_conjecture,[status(cth)],[f1])).
% 0.75/0.49 thf(f3,plain,(
% 0.75/0.49 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.75/0.49 inference(flattening,[],[f2])).
% 0.75/0.49 thf(f4,plain,(
% 0.75/0.49 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.75/0.49 inference(cnf_transformation,[],[f3])).
% 0.75/0.49 thf(f6,definition,(
% 0.75/0.49 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.75/0.49 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.75/0.49 thf(f7,definition,(
% 0.75/0.49 (sF0 = ((f4 @ x)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.75/0.49 thf(f8,plain,(
% 0.75/0.49 (((f4 @ x)) = sF0)),
% 0.75/0.49 inference(reorient_equations,[],[f7])).
% 0.75/0.49 thf(f9,definition,(
% 0.75/0.49 (sF1 = ((f3 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.75/0.49 thf(f10,plain,(
% 0.75/0.49 (((f3 @ sF0)) = sF1)),
% 0.75/0.49 inference(reorient_equations,[],[f9])).
% 0.75/0.49 thf(f11,definition,(
% 0.75/0.49 (sF2 = ((f3 @ sF1)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.75/0.49 thf(f12,plain,(
% 0.75/0.49 (((f3 @ sF1)) = sF2)),
% 0.75/0.49 inference(reorient_equations,[],[f11])).
% 0.75/0.49 thf(f13,definition,(
% 0.75/0.49 (sF3 = ((f3 @ sF2)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.75/0.49 thf(f14,plain,(
% 0.75/0.49 (((f3 @ sF2)) = sF3)),
% 0.75/0.49 inference(reorient_equations,[],[f13])).
% 0.75/0.49 thf(f15,definition,(
% 0.75/0.49 (sF4 = ((f2 @ sF3)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.75/0.49 thf(f16,plain,(
% 0.75/0.49 (((f2 @ sF3)) = sF4)),
% 0.75/0.49 inference(reorient_equations,[],[f15])).
% 0.75/0.49 thf(f17,definition,(
% 0.75/0.49 (sF5 = ((f1 @ sF4)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 0.75/0.49 thf(f18,plain,(
% 0.75/0.49 (((f1 @ sF4)) = sF5)),
% 0.75/0.49 inference(reorient_equations,[],[f17])).
% 0.75/0.49 thf(f19,definition,(
% 0.75/0.49 (sF6 = ((f1 @ sF5)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.75/0.49 thf(f20,plain,(
% 0.75/0.49 (((f1 @ sF5)) = sF6)),
% 0.75/0.49 inference(reorient_equations,[],[f19])).
% 0.75/0.49 thf(f21,definition,(
% 0.75/0.49 (sF7 = ((f1 @ sF6)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 0.75/0.49 thf(f22,plain,(
% 0.75/0.49 (((f1 @ sF6)) = sF7)),
% 0.75/0.49 inference(reorient_equations,[],[f21])).
% 0.75/0.49 thf(f23,definition,(
% 0.75/0.49 (sF8 = ((f0 @ sF7)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 0.75/0.49 thf(f24,plain,(
% 0.75/0.49 (((f0 @ sF7)) = sF8)),
% 0.75/0.49 inference(reorient_equations,[],[f23])).
% 0.75/0.49 thf(f25,definition,(
% 0.75/0.49 (sF9 = ((f4 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.75/0.49 thf(f26,plain,(
% 0.75/0.49 (((f4 @ sF0)) = sF9)),
% 0.75/0.49 inference(reorient_equations,[],[f25])).
% 0.75/0.49 thf(f27,definition,(
% 0.75/0.49 (sF10 = ((f4 @ sF9)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.75/0.49 thf(f28,plain,(
% 0.75/0.49 (((f4 @ sF9)) = sF10)),
% 0.75/0.49 inference(reorient_equations,[],[f27])).
% 0.75/0.49 thf(f29,definition,(
% 0.75/0.49 (sF11 = ((f3 @ sF10)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 0.75/0.49 thf(f30,plain,(
% 0.75/0.49 (((f3 @ sF10)) = sF11)),
% 0.75/0.49 inference(reorient_equations,[],[f29])).
% 0.75/0.49 thf(f31,definition,(
% 0.75/0.49 (sF12 = ((f2 @ sF11)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.75/0.49 thf(f32,plain,(
% 0.75/0.49 (((f2 @ sF11)) = sF12)),
% 0.75/0.49 inference(reorient_equations,[],[f31])).
% 0.75/0.49 thf(f33,definition,(
% 0.75/0.49 (sF13 = ((f2 @ sF12)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.75/0.49 thf(f34,plain,(
% 0.75/0.49 (((f2 @ sF12)) = sF13)),
% 0.75/0.49 inference(reorient_equations,[],[f33])).
% 0.75/0.49 thf(f35,definition,(
% 0.75/0.49 (sF14 = ((f2 @ sF13)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.75/0.49 thf(f36,plain,(
% 0.75/0.49 (((f2 @ sF13)) = sF14)),
% 0.75/0.49 inference(reorient_equations,[],[f35])).
% 0.75/0.49 thf(f37,definition,(
% 0.75/0.49 (sF15 = ((f1 @ sF14)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 0.75/0.49 thf(f38,plain,(
% 0.75/0.49 (((f1 @ sF14)) = sF15)),
% 0.75/0.49 inference(reorient_equations,[],[f37])).
% 0.75/0.49 thf(f39,definition,(
% 0.75/0.49 (sF16 = ((f0 @ sF15)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 0.75/0.49 thf(f40,plain,(
% 0.75/0.49 (((f0 @ sF15)) = sF16)),
% 0.75/0.49 inference(reorient_equations,[],[f39])).
% 0.75/0.49 thf(f41,definition,(
% 0.75/0.49 (sF17 = ((f0 @ sF16)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 0.75/0.49 thf(f42,plain,(
% 0.75/0.49 (((f0 @ sF16)) = sF17)),
% 0.75/0.49 inference(reorient_equations,[],[f41])).
% 0.75/0.49 thf(f43,definition,(
% 0.75/0.49 (sF18 = ((f0 @ sF17)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 0.75/0.49 thf(f44,plain,(
% 0.75/0.49 (((f0 @ sF17)) = sF18)),
% 0.75/0.49 inference(reorient_equations,[],[f43])).
% 0.75/0.49 thf(f45,plain,(
% 0.75/0.49 (sF8 != sF18)),
% 0.75/0.49 inference(definition_folding,[],[f4,f44,f42,f40,f38,f36,f34,f32,f30,f28,f26,f8,f24,f22,f20,f18,f16,f14,f12,f10,f8])).
% 0.75/0.49 thf(f46,plain,(
% 0.75/0.49 ($true = sF8) | ($true = sF18)),
% 0.75/0.49 inference(xor_proxy_clausification,[],[f45])).
% 0.75/0.49 thf(f47,plain,(
% 0.75/0.49 ($false = sF8) | ($false = sF18)),
% 0.75/0.49 inference(xor_proxy_clausification,[],[f45])).
% 0.75/0.49 thf(f48,plain,(
% 0.75/0.49 (((f4 @ x)) = $true) | ($false = sF0)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f8])).
% 0.75/0.49 thf(f49,plain,(
% 0.75/0.49 (((f4 @ x)) = $false) | ($true = sF0)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f8])).
% 0.75/0.49 thf(f50,plain,(
% 0.75/0.49 ($true = ((f3 @ sF0))) | ($false = sF1)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f10])).
% 0.75/0.49 thf(f51,plain,(
% 0.75/0.49 ($false = ((f3 @ sF0))) | ($true = sF1)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f10])).
% 0.75/0.49 thf(f52,plain,(
% 0.75/0.49 ($true = ((f3 @ sF1))) | ($false = sF2)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f12])).
% 0.75/0.49 thf(f53,plain,(
% 0.75/0.49 ($false = ((f3 @ sF1))) | ($true = sF2)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f12])).
% 0.75/0.49 thf(f54,plain,(
% 0.75/0.49 ($true = ((f3 @ sF2))) | ($false = sF3)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f14])).
% 0.75/0.49 thf(f55,plain,(
% 0.75/0.49 ($false = ((f3 @ sF2))) | ($true = sF3)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f14])).
% 0.75/0.49 thf(f56,plain,(
% 0.75/0.49 ($true = ((f2 @ sF3))) | ($false = sF4)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f16])).
% 0.75/0.49 thf(f57,plain,(
% 0.75/0.49 ($false = ((f2 @ sF3))) | ($true = sF4)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f16])).
% 0.75/0.49 thf(f58,plain,(
% 0.75/0.49 ($true = ((f1 @ sF4))) | ($false = sF5)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f18])).
% 0.75/0.49 thf(f59,plain,(
% 0.75/0.49 ($false = ((f1 @ sF4))) | ($true = sF5)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f18])).
% 0.75/0.49 thf(f60,plain,(
% 0.75/0.49 ($true = ((f1 @ sF5))) | ($false = sF6)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f20])).
% 0.75/0.49 thf(f61,plain,(
% 0.75/0.49 ($false = ((f1 @ sF5))) | ($true = sF6)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f20])).
% 0.75/0.49 thf(f62,plain,(
% 0.75/0.49 ($true = ((f1 @ sF6))) | ($false = sF7)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f22])).
% 0.75/0.49 thf(f63,plain,(
% 0.75/0.49 ($false = ((f1 @ sF6))) | ($true = sF7)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f22])).
% 0.75/0.49 thf(f64,plain,(
% 0.75/0.49 ($true = ((f0 @ sF7))) | ($false = sF8)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f24])).
% 0.75/0.49 thf(f65,plain,(
% 0.75/0.49 ($false = ((f0 @ sF7))) | ($true = sF8)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f24])).
% 0.75/0.49 thf(f66,plain,(
% 0.75/0.49 ($true = ((f4 @ sF0))) | ($false = sF9)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f26])).
% 0.75/0.49 thf(f67,plain,(
% 0.75/0.49 ($false = ((f4 @ sF0))) | ($true = sF9)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f26])).
% 0.75/0.49 thf(f68,plain,(
% 0.75/0.49 ($true = ((f4 @ sF9))) | ($false = sF10)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f28])).
% 0.75/0.49 thf(f69,plain,(
% 0.75/0.49 ($false = ((f4 @ sF9))) | ($true = sF10)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f28])).
% 0.75/0.49 thf(f70,plain,(
% 0.75/0.49 ($true = ((f3 @ sF10))) | ($false = sF11)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f30])).
% 0.75/0.49 thf(f71,plain,(
% 0.75/0.49 ($false = ((f3 @ sF10))) | ($true = sF11)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f30])).
% 0.75/0.49 thf(f72,plain,(
% 0.75/0.49 ($true = ((f2 @ sF11))) | ($false = sF12)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f32])).
% 0.75/0.49 thf(f73,plain,(
% 0.75/0.49 ($false = ((f2 @ sF11))) | ($true = sF12)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f32])).
% 0.75/0.49 thf(f74,plain,(
% 0.75/0.49 ($true = ((f2 @ sF12))) | ($false = sF13)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f34])).
% 0.75/0.49 thf(f75,plain,(
% 0.75/0.49 ($false = ((f2 @ sF12))) | ($true = sF13)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f34])).
% 0.75/0.49 thf(f76,plain,(
% 0.75/0.49 ($true = ((f2 @ sF13))) | ($false = sF14)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f36])).
% 0.75/0.49 thf(f77,plain,(
% 0.75/0.49 ($false = ((f2 @ sF13))) | ($true = sF14)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f36])).
% 0.75/0.49 thf(f78,plain,(
% 0.75/0.49 ($true = ((f1 @ sF14))) | ($false = sF15)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f38])).
% 0.75/0.49 thf(f79,plain,(
% 0.75/0.49 ($false = ((f1 @ sF14))) | ($true = sF15)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f38])).
% 0.75/0.49 thf(f80,plain,(
% 0.75/0.49 ($true = ((f0 @ sF15))) | ($false = sF16)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f40])).
% 0.75/0.49 thf(f81,plain,(
% 0.75/0.49 ($false = ((f0 @ sF15))) | ($true = sF16)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f40])).
% 0.75/0.49 thf(f82,plain,(
% 0.75/0.49 ($true = ((f0 @ sF16))) | ($false = sF17)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f42])).
% 0.75/0.49 thf(f83,plain,(
% 0.75/0.49 ($false = ((f0 @ sF16))) | ($true = sF17)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f42])).
% 0.75/0.49 thf(f84,plain,(
% 0.75/0.49 ($true = ((f0 @ sF17))) | ($false = sF18)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f44])).
% 0.75/0.49 thf(f85,plain,(
% 0.75/0.49 ($false = ((f0 @ sF17))) | ($true = sF18)),
% 0.75/0.49 inference(iff_proxy_clausification,[],[f44])).
% 0.75/0.49 thf(f87,definition,(
% 0.75/0.49 spl19_1 <=> ($false = sF18)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition])).
% 0.75/0.49 thf(f89,plain,(
% 0.75/0.49 ($false = sF18) | ~spl19_1),
% 0.75/0.49 inference(avatar_component_clause,[],[f87])).
% 0.75/0.49 thf(f91,definition,(
% 0.75/0.49 spl19_2 <=> ($false = sF8)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition])).
% 0.75/0.49 thf(f93,plain,(
% 0.75/0.49 ($false = sF8) | ~spl19_2),
% 0.75/0.49 inference(avatar_component_clause,[],[f91])).
% 0.75/0.49 thf(f94,plain,(
% 0.75/0.49 spl19_1 | spl19_2),
% 0.75/0.49 inference(avatar_split_clause,[],[f47,f91,f87])).
% 0.75/0.49 thf(f96,definition,(
% 0.75/0.49 spl19_3 <=> ($true = sF18)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition])).
% 0.75/0.49 thf(f98,plain,(
% 0.75/0.49 ($true = sF18) | ~spl19_3),
% 0.75/0.49 inference(avatar_component_clause,[],[f96])).
% 0.75/0.49 thf(f100,definition,(
% 0.75/0.49 spl19_4 <=> ($true = sF8)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition])).
% 0.75/0.49 thf(f102,plain,(
% 0.75/0.49 ($true = sF8) | ~spl19_4),
% 0.75/0.49 inference(avatar_component_clause,[],[f100])).
% 0.75/0.49 thf(f103,plain,(
% 0.75/0.49 spl19_3 | spl19_4),
% 0.75/0.49 inference(avatar_split_clause,[],[f46,f100,f96])).
% 0.75/0.49 thf(f105,definition,(
% 0.75/0.49 spl19_5 <=> ($true = sF0)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition])).
% 0.75/0.49 thf(f106,plain,(
% 0.75/0.49 ($true != sF0) | spl19_5),
% 0.75/0.49 inference(avatar_component_clause,[],[f105])).
% 0.75/0.49 thf(f107,plain,(
% 0.75/0.49 ($true = sF0) | ~spl19_5),
% 0.75/0.49 inference(avatar_component_clause,[],[f105])).
% 0.75/0.49 thf(f109,definition,(
% 0.75/0.49 spl19_6 <=> (((f4 @ x)) = $false)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition])).
% 0.75/0.49 thf(f110,plain,(
% 0.75/0.49 (((f4 @ x)) != $false) | spl19_6),
% 0.75/0.49 inference(avatar_component_clause,[],[f109])).
% 0.75/0.49 thf(f111,plain,(
% 0.75/0.49 (((f4 @ x)) = $false) | ~spl19_6),
% 0.75/0.49 inference(avatar_component_clause,[],[f109])).
% 0.75/0.49 thf(f112,plain,(
% 0.75/0.49 spl19_5 | spl19_6),
% 0.75/0.49 inference(avatar_split_clause,[],[f49,f109,f105])).
% 0.75/0.49 thf(f114,definition,(
% 0.75/0.49 spl19_7 <=> ($false = sF0)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition])).
% 0.75/0.49 thf(f116,plain,(
% 0.75/0.49 ($false = sF0) | ~spl19_7),
% 0.75/0.49 inference(avatar_component_clause,[],[f114])).
% 0.75/0.49 thf(f118,definition,(
% 0.75/0.49 spl19_8 <=> (((f4 @ x)) = $true)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition])).
% 0.75/0.49 thf(f120,plain,(
% 0.75/0.49 (((f4 @ x)) = $true) | ~spl19_8),
% 0.75/0.49 inference(avatar_component_clause,[],[f118])).
% 0.75/0.49 thf(f121,plain,(
% 0.75/0.49 spl19_7 | spl19_8),
% 0.75/0.49 inference(avatar_split_clause,[],[f48,f118,f114])).
% 0.75/0.49 thf(f123,definition,(
% 0.75/0.49 spl19_9 <=> ($true = sF1)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition])).
% 0.75/0.49 thf(f124,plain,(
% 0.75/0.49 ($true != sF1) | spl19_9),
% 0.75/0.49 inference(avatar_component_clause,[],[f123])).
% 0.75/0.49 thf(f125,plain,(
% 0.75/0.49 ($true = sF1) | ~spl19_9),
% 0.75/0.49 inference(avatar_component_clause,[],[f123])).
% 0.75/0.49 thf(f127,definition,(
% 0.75/0.49 spl19_10 <=> ($false = ((f3 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition])).
% 0.75/0.49 thf(f128,plain,(
% 0.75/0.49 ($false != ((f3 @ sF0))) | spl19_10),
% 0.75/0.49 inference(avatar_component_clause,[],[f127])).
% 0.75/0.49 thf(f129,plain,(
% 0.75/0.49 ($false = ((f3 @ sF0))) | ~spl19_10),
% 0.75/0.49 inference(avatar_component_clause,[],[f127])).
% 0.75/0.49 thf(f130,plain,(
% 0.75/0.49 spl19_9 | spl19_10),
% 0.75/0.49 inference(avatar_split_clause,[],[f51,f127,f123])).
% 0.75/0.49 thf(f132,definition,(
% 0.75/0.49 spl19_11 <=> ($false = sF1)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition])).
% 0.75/0.49 thf(f134,plain,(
% 0.75/0.49 ($false = sF1) | ~spl19_11),
% 0.75/0.49 inference(avatar_component_clause,[],[f132])).
% 0.75/0.49 thf(f136,definition,(
% 0.75/0.49 spl19_12 <=> ($true = ((f3 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition])).
% 0.75/0.49 thf(f138,plain,(
% 0.75/0.49 ($true = ((f3 @ sF0))) | ~spl19_12),
% 0.75/0.49 inference(avatar_component_clause,[],[f136])).
% 0.75/0.49 thf(f139,plain,(
% 0.75/0.49 spl19_11 | spl19_12),
% 0.75/0.49 inference(avatar_split_clause,[],[f50,f136,f132])).
% 0.75/0.49 thf(f141,definition,(
% 0.75/0.49 spl19_13 <=> ($true = sF2)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition])).
% 0.75/0.49 thf(f142,plain,(
% 0.75/0.49 ($true != sF2) | spl19_13),
% 0.75/0.49 inference(avatar_component_clause,[],[f141])).
% 0.75/0.49 thf(f143,plain,(
% 0.75/0.49 ($true = sF2) | ~spl19_13),
% 0.75/0.49 inference(avatar_component_clause,[],[f141])).
% 0.75/0.49 thf(f145,definition,(
% 0.75/0.49 spl19_14 <=> ($false = ((f3 @ sF1)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition])).
% 0.75/0.49 thf(f146,plain,(
% 0.75/0.49 ($false != ((f3 @ sF1))) | spl19_14),
% 0.75/0.49 inference(avatar_component_clause,[],[f145])).
% 0.75/0.49 thf(f147,plain,(
% 0.75/0.49 ($false = ((f3 @ sF1))) | ~spl19_14),
% 0.75/0.49 inference(avatar_component_clause,[],[f145])).
% 0.75/0.49 thf(f148,plain,(
% 0.75/0.49 spl19_13 | spl19_14),
% 0.75/0.49 inference(avatar_split_clause,[],[f53,f145,f141])).
% 0.75/0.49 thf(f150,definition,(
% 0.75/0.49 spl19_15 <=> ($false = sF2)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition])).
% 0.75/0.49 thf(f152,plain,(
% 0.75/0.49 ($false = sF2) | ~spl19_15),
% 0.75/0.49 inference(avatar_component_clause,[],[f150])).
% 0.75/0.49 thf(f154,definition,(
% 0.75/0.49 spl19_16 <=> ($true = ((f3 @ sF1)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition])).
% 0.75/0.49 thf(f156,plain,(
% 0.75/0.49 ($true = ((f3 @ sF1))) | ~spl19_16),
% 0.75/0.49 inference(avatar_component_clause,[],[f154])).
% 0.75/0.49 thf(f157,plain,(
% 0.75/0.49 spl19_15 | spl19_16),
% 0.75/0.49 inference(avatar_split_clause,[],[f52,f154,f150])).
% 0.75/0.49 thf(f159,definition,(
% 0.75/0.49 spl19_17 <=> ($true = sF3)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition])).
% 0.75/0.49 thf(f160,plain,(
% 0.75/0.49 ($true != sF3) | spl19_17),
% 0.75/0.49 inference(avatar_component_clause,[],[f159])).
% 0.75/0.49 thf(f161,plain,(
% 0.75/0.49 ($true = sF3) | ~spl19_17),
% 0.75/0.49 inference(avatar_component_clause,[],[f159])).
% 0.75/0.49 thf(f163,definition,(
% 0.75/0.49 spl19_18 <=> ($false = ((f3 @ sF2)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition])).
% 0.75/0.49 thf(f164,plain,(
% 0.75/0.49 ($false != ((f3 @ sF2))) | spl19_18),
% 0.75/0.49 inference(avatar_component_clause,[],[f163])).
% 0.75/0.49 thf(f165,plain,(
% 0.75/0.49 ($false = ((f3 @ sF2))) | ~spl19_18),
% 0.75/0.49 inference(avatar_component_clause,[],[f163])).
% 0.75/0.49 thf(f166,plain,(
% 0.75/0.49 spl19_17 | spl19_18),
% 0.75/0.49 inference(avatar_split_clause,[],[f55,f163,f159])).
% 0.75/0.49 thf(f168,definition,(
% 0.75/0.49 spl19_19 <=> ($false = sF3)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition])).
% 0.75/0.49 thf(f170,plain,(
% 0.75/0.49 ($false = sF3) | ~spl19_19),
% 0.75/0.49 inference(avatar_component_clause,[],[f168])).
% 0.75/0.49 thf(f172,definition,(
% 0.75/0.49 spl19_20 <=> ($true = ((f3 @ sF2)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition])).
% 0.75/0.49 thf(f173,plain,(
% 0.75/0.49 ($true != ((f3 @ sF2))) | spl19_20),
% 0.75/0.49 inference(avatar_component_clause,[],[f172])).
% 0.75/0.49 thf(f174,plain,(
% 0.75/0.49 ($true = ((f3 @ sF2))) | ~spl19_20),
% 0.75/0.49 inference(avatar_component_clause,[],[f172])).
% 0.75/0.49 thf(f175,plain,(
% 0.75/0.49 spl19_19 | spl19_20),
% 0.75/0.49 inference(avatar_split_clause,[],[f54,f172,f168])).
% 0.75/0.49 thf(f177,definition,(
% 0.75/0.49 spl19_21 <=> ($true = sF4)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition])).
% 0.75/0.49 thf(f178,plain,(
% 0.75/0.49 ($true != sF4) | spl19_21),
% 0.75/0.49 inference(avatar_component_clause,[],[f177])).
% 0.75/0.49 thf(f179,plain,(
% 0.75/0.49 ($true = sF4) | ~spl19_21),
% 0.75/0.49 inference(avatar_component_clause,[],[f177])).
% 0.75/0.49 thf(f181,definition,(
% 0.75/0.49 spl19_22 <=> ($false = ((f2 @ sF3)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition])).
% 0.75/0.49 thf(f182,plain,(
% 0.75/0.49 ($false != ((f2 @ sF3))) | spl19_22),
% 0.75/0.49 inference(avatar_component_clause,[],[f181])).
% 0.75/0.49 thf(f183,plain,(
% 0.75/0.49 ($false = ((f2 @ sF3))) | ~spl19_22),
% 0.75/0.49 inference(avatar_component_clause,[],[f181])).
% 0.75/0.49 thf(f184,plain,(
% 0.75/0.49 spl19_21 | spl19_22),
% 0.75/0.49 inference(avatar_split_clause,[],[f57,f181,f177])).
% 0.75/0.49 thf(f186,definition,(
% 0.75/0.49 spl19_23 <=> ($false = sF4)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition])).
% 0.75/0.49 thf(f188,plain,(
% 0.75/0.49 ($false = sF4) | ~spl19_23),
% 0.75/0.49 inference(avatar_component_clause,[],[f186])).
% 0.75/0.49 thf(f190,definition,(
% 0.75/0.49 spl19_24 <=> ($true = ((f2 @ sF3)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition])).
% 0.75/0.49 thf(f192,plain,(
% 0.75/0.49 ($true = ((f2 @ sF3))) | ~spl19_24),
% 0.75/0.49 inference(avatar_component_clause,[],[f190])).
% 0.75/0.49 thf(f193,plain,(
% 0.75/0.49 spl19_23 | spl19_24),
% 0.75/0.49 inference(avatar_split_clause,[],[f56,f190,f186])).
% 0.75/0.49 thf(f195,definition,(
% 0.75/0.49 spl19_25 <=> ($true = sF5)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition])).
% 0.75/0.49 thf(f197,plain,(
% 0.75/0.49 ($true = sF5) | ~spl19_25),
% 0.75/0.49 inference(avatar_component_clause,[],[f195])).
% 0.75/0.49 thf(f199,definition,(
% 0.75/0.49 spl19_26 <=> ($false = ((f1 @ sF4)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition])).
% 0.75/0.49 thf(f200,plain,(
% 0.75/0.49 ($false != ((f1 @ sF4))) | spl19_26),
% 0.75/0.49 inference(avatar_component_clause,[],[f199])).
% 0.75/0.49 thf(f201,plain,(
% 0.75/0.49 ($false = ((f1 @ sF4))) | ~spl19_26),
% 0.75/0.49 inference(avatar_component_clause,[],[f199])).
% 0.75/0.49 thf(f202,plain,(
% 0.75/0.49 spl19_25 | spl19_26),
% 0.75/0.49 inference(avatar_split_clause,[],[f59,f199,f195])).
% 0.75/0.49 thf(f204,definition,(
% 0.75/0.49 spl19_27 <=> ($false = sF5)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition])).
% 0.75/0.49 thf(f206,plain,(
% 0.75/0.49 ($false = sF5) | ~spl19_27),
% 0.75/0.49 inference(avatar_component_clause,[],[f204])).
% 0.75/0.49 thf(f208,definition,(
% 0.75/0.49 spl19_28 <=> ($true = ((f1 @ sF4)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition])).
% 0.75/0.49 thf(f210,plain,(
% 0.75/0.49 ($true = ((f1 @ sF4))) | ~spl19_28),
% 0.75/0.49 inference(avatar_component_clause,[],[f208])).
% 0.75/0.49 thf(f211,plain,(
% 0.75/0.49 spl19_27 | spl19_28),
% 0.75/0.49 inference(avatar_split_clause,[],[f58,f208,f204])).
% 0.75/0.49 thf(f213,definition,(
% 0.75/0.49 spl19_29 <=> ($true = sF6)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition])).
% 0.75/0.49 thf(f214,plain,(
% 0.75/0.49 ($true != sF6) | spl19_29),
% 0.75/0.49 inference(avatar_component_clause,[],[f213])).
% 0.75/0.49 thf(f215,plain,(
% 0.75/0.49 ($true = sF6) | ~spl19_29),
% 0.75/0.49 inference(avatar_component_clause,[],[f213])).
% 0.75/0.49 thf(f217,definition,(
% 0.75/0.49 spl19_30 <=> ($false = ((f1 @ sF5)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_30])],[avatar_definition])).
% 0.75/0.49 thf(f218,plain,(
% 0.75/0.49 ($false != ((f1 @ sF5))) | spl19_30),
% 0.75/0.49 inference(avatar_component_clause,[],[f217])).
% 0.75/0.49 thf(f219,plain,(
% 0.75/0.49 ($false = ((f1 @ sF5))) | ~spl19_30),
% 0.75/0.49 inference(avatar_component_clause,[],[f217])).
% 0.75/0.49 thf(f220,plain,(
% 0.75/0.49 spl19_29 | spl19_30),
% 0.75/0.49 inference(avatar_split_clause,[],[f61,f217,f213])).
% 0.75/0.49 thf(f222,definition,(
% 0.75/0.49 spl19_31 <=> ($false = sF6)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_31])],[avatar_definition])).
% 0.75/0.49 thf(f224,plain,(
% 0.75/0.49 ($false = sF6) | ~spl19_31),
% 0.75/0.49 inference(avatar_component_clause,[],[f222])).
% 0.75/0.49 thf(f226,definition,(
% 0.75/0.49 spl19_32 <=> ($true = ((f1 @ sF5)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_32])],[avatar_definition])).
% 0.75/0.49 thf(f228,plain,(
% 0.75/0.49 ($true = ((f1 @ sF5))) | ~spl19_32),
% 0.75/0.49 inference(avatar_component_clause,[],[f226])).
% 0.75/0.49 thf(f229,plain,(
% 0.75/0.49 spl19_31 | spl19_32),
% 0.75/0.49 inference(avatar_split_clause,[],[f60,f226,f222])).
% 0.75/0.49 thf(f231,definition,(
% 0.75/0.49 spl19_33 <=> ($true = sF7)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition])).
% 0.75/0.49 thf(f233,plain,(
% 0.75/0.49 ($true = sF7) | ~spl19_33),
% 0.75/0.49 inference(avatar_component_clause,[],[f231])).
% 0.75/0.49 thf(f235,definition,(
% 0.75/0.49 spl19_34 <=> ($false = ((f1 @ sF6)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_34])],[avatar_definition])).
% 0.75/0.49 thf(f236,plain,(
% 0.75/0.49 ($false != ((f1 @ sF6))) | spl19_34),
% 0.75/0.49 inference(avatar_component_clause,[],[f235])).
% 0.75/0.49 thf(f237,plain,(
% 0.75/0.49 ($false = ((f1 @ sF6))) | ~spl19_34),
% 0.75/0.49 inference(avatar_component_clause,[],[f235])).
% 0.75/0.49 thf(f238,plain,(
% 0.75/0.49 spl19_33 | spl19_34),
% 0.75/0.49 inference(avatar_split_clause,[],[f63,f235,f231])).
% 0.75/0.49 thf(f240,definition,(
% 0.75/0.49 spl19_35 <=> ($false = sF7)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_35])],[avatar_definition])).
% 0.75/0.49 thf(f242,plain,(
% 0.75/0.49 ($false = sF7) | ~spl19_35),
% 0.75/0.49 inference(avatar_component_clause,[],[f240])).
% 0.75/0.49 thf(f244,definition,(
% 0.75/0.49 spl19_36 <=> ($true = ((f1 @ sF6)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_36])],[avatar_definition])).
% 0.75/0.49 thf(f246,plain,(
% 0.75/0.49 ($true = ((f1 @ sF6))) | ~spl19_36),
% 0.75/0.49 inference(avatar_component_clause,[],[f244])).
% 0.75/0.49 thf(f247,plain,(
% 0.75/0.49 spl19_35 | spl19_36),
% 0.75/0.49 inference(avatar_split_clause,[],[f62,f244,f240])).
% 0.75/0.49 thf(f249,definition,(
% 0.75/0.49 spl19_37 <=> ($false = ((f0 @ sF7)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_37])],[avatar_definition])).
% 0.75/0.49 thf(f251,plain,(
% 0.75/0.49 ($false = ((f0 @ sF7))) | ~spl19_37),
% 0.75/0.49 inference(avatar_component_clause,[],[f249])).
% 0.75/0.49 thf(f252,plain,(
% 0.75/0.49 spl19_4 | spl19_37),
% 0.75/0.49 inference(avatar_split_clause,[],[f65,f249,f100])).
% 0.75/0.49 thf(f254,definition,(
% 0.75/0.49 spl19_38 <=> ($true = ((f0 @ sF7)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_38])],[avatar_definition])).
% 0.75/0.49 thf(f256,plain,(
% 0.75/0.49 ($true = ((f0 @ sF7))) | ~spl19_38),
% 0.75/0.49 inference(avatar_component_clause,[],[f254])).
% 0.75/0.49 thf(f257,plain,(
% 0.75/0.49 spl19_2 | spl19_38),
% 0.75/0.49 inference(avatar_split_clause,[],[f64,f254,f91])).
% 0.75/0.49 thf(f259,definition,(
% 0.75/0.49 spl19_39 <=> ($true = sF9)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_39])],[avatar_definition])).
% 0.75/0.49 thf(f260,plain,(
% 0.75/0.49 ($true != sF9) | spl19_39),
% 0.75/0.49 inference(avatar_component_clause,[],[f259])).
% 0.75/0.49 thf(f261,plain,(
% 0.75/0.49 ($true = sF9) | ~spl19_39),
% 0.75/0.49 inference(avatar_component_clause,[],[f259])).
% 0.75/0.49 thf(f263,definition,(
% 0.75/0.49 spl19_40 <=> ($false = ((f4 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_40])],[avatar_definition])).
% 0.75/0.49 thf(f264,plain,(
% 0.75/0.49 ($false != ((f4 @ sF0))) | spl19_40),
% 0.75/0.49 inference(avatar_component_clause,[],[f263])).
% 0.75/0.49 thf(f265,plain,(
% 0.75/0.49 ($false = ((f4 @ sF0))) | ~spl19_40),
% 0.75/0.49 inference(avatar_component_clause,[],[f263])).
% 0.75/0.49 thf(f266,plain,(
% 0.75/0.49 spl19_39 | spl19_40),
% 0.75/0.49 inference(avatar_split_clause,[],[f67,f263,f259])).
% 0.75/0.49 thf(f268,definition,(
% 0.75/0.49 spl19_41 <=> ($false = sF9)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_41])],[avatar_definition])).
% 0.75/0.49 thf(f270,plain,(
% 0.75/0.49 ($false = sF9) | ~spl19_41),
% 0.75/0.49 inference(avatar_component_clause,[],[f268])).
% 0.75/0.49 thf(f272,definition,(
% 0.75/0.49 spl19_42 <=> ($true = ((f4 @ sF0)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_42])],[avatar_definition])).
% 0.75/0.49 thf(f274,plain,(
% 0.75/0.49 ($true = ((f4 @ sF0))) | ~spl19_42),
% 0.75/0.49 inference(avatar_component_clause,[],[f272])).
% 0.75/0.49 thf(f275,plain,(
% 0.75/0.49 spl19_41 | spl19_42),
% 0.75/0.49 inference(avatar_split_clause,[],[f66,f272,f268])).
% 0.75/0.49 thf(f277,definition,(
% 0.75/0.49 spl19_43 <=> ($true = sF10)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_43])],[avatar_definition])).
% 0.75/0.49 thf(f279,plain,(
% 0.75/0.49 ($true = sF10) | ~spl19_43),
% 0.75/0.49 inference(avatar_component_clause,[],[f277])).
% 0.75/0.49 thf(f281,definition,(
% 0.75/0.49 spl19_44 <=> ($false = ((f4 @ sF9)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_44])],[avatar_definition])).
% 0.75/0.49 thf(f283,plain,(
% 0.75/0.49 ($false = ((f4 @ sF9))) | ~spl19_44),
% 0.75/0.49 inference(avatar_component_clause,[],[f281])).
% 0.75/0.49 thf(f284,plain,(
% 0.75/0.49 spl19_43 | spl19_44),
% 0.75/0.49 inference(avatar_split_clause,[],[f69,f281,f277])).
% 0.75/0.49 thf(f286,definition,(
% 0.75/0.49 spl19_45 <=> ($false = sF10)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_45])],[avatar_definition])).
% 0.75/0.49 thf(f288,plain,(
% 0.75/0.49 ($false = sF10) | ~spl19_45),
% 0.75/0.49 inference(avatar_component_clause,[],[f286])).
% 0.75/0.49 thf(f290,definition,(
% 0.75/0.49 spl19_46 <=> ($true = ((f4 @ sF9)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_46])],[avatar_definition])).
% 0.75/0.49 thf(f292,plain,(
% 0.75/0.49 ($true = ((f4 @ sF9))) | ~spl19_46),
% 0.75/0.49 inference(avatar_component_clause,[],[f290])).
% 0.75/0.49 thf(f293,plain,(
% 0.75/0.49 spl19_45 | spl19_46),
% 0.75/0.49 inference(avatar_split_clause,[],[f68,f290,f286])).
% 0.75/0.49 thf(f295,definition,(
% 0.75/0.49 spl19_47 <=> ($true = sF11)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_47])],[avatar_definition])).
% 0.75/0.49 thf(f296,plain,(
% 0.75/0.49 ($true != sF11) | spl19_47),
% 0.75/0.49 inference(avatar_component_clause,[],[f295])).
% 0.75/0.49 thf(f297,plain,(
% 0.75/0.49 ($true = sF11) | ~spl19_47),
% 0.75/0.49 inference(avatar_component_clause,[],[f295])).
% 0.75/0.49 thf(f299,definition,(
% 0.75/0.49 spl19_48 <=> ($false = ((f3 @ sF10)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_48])],[avatar_definition])).
% 0.75/0.49 thf(f300,plain,(
% 0.75/0.49 ($false != ((f3 @ sF10))) | spl19_48),
% 0.75/0.49 inference(avatar_component_clause,[],[f299])).
% 0.75/0.49 thf(f301,plain,(
% 0.75/0.49 ($false = ((f3 @ sF10))) | ~spl19_48),
% 0.75/0.49 inference(avatar_component_clause,[],[f299])).
% 0.75/0.49 thf(f302,plain,(
% 0.75/0.49 spl19_47 | spl19_48),
% 0.75/0.49 inference(avatar_split_clause,[],[f71,f299,f295])).
% 0.75/0.49 thf(f304,definition,(
% 0.75/0.49 spl19_49 <=> ($false = sF11)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_49])],[avatar_definition])).
% 0.75/0.49 thf(f306,plain,(
% 0.75/0.49 ($false = sF11) | ~spl19_49),
% 0.75/0.49 inference(avatar_component_clause,[],[f304])).
% 0.75/0.49 thf(f308,definition,(
% 0.75/0.49 spl19_50 <=> ($true = ((f3 @ sF10)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_50])],[avatar_definition])).
% 0.75/0.49 thf(f309,plain,(
% 0.75/0.49 ($true != ((f3 @ sF10))) | spl19_50),
% 0.75/0.49 inference(avatar_component_clause,[],[f308])).
% 0.75/0.49 thf(f310,plain,(
% 0.75/0.49 ($true = ((f3 @ sF10))) | ~spl19_50),
% 0.75/0.49 inference(avatar_component_clause,[],[f308])).
% 0.75/0.49 thf(f311,plain,(
% 0.75/0.49 spl19_49 | spl19_50),
% 0.75/0.49 inference(avatar_split_clause,[],[f70,f308,f304])).
% 0.75/0.49 thf(f313,definition,(
% 0.75/0.49 spl19_51 <=> ($true = sF12)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_51])],[avatar_definition])).
% 0.75/0.49 thf(f315,plain,(
% 0.75/0.49 ($true = sF12) | ~spl19_51),
% 0.75/0.49 inference(avatar_component_clause,[],[f313])).
% 0.75/0.49 thf(f317,definition,(
% 0.75/0.49 spl19_52 <=> ($false = ((f2 @ sF11)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_52])],[avatar_definition])).
% 0.75/0.49 thf(f319,plain,(
% 0.75/0.49 ($false = ((f2 @ sF11))) | ~spl19_52),
% 0.75/0.49 inference(avatar_component_clause,[],[f317])).
% 0.75/0.49 thf(f320,plain,(
% 0.75/0.49 spl19_51 | spl19_52),
% 0.75/0.49 inference(avatar_split_clause,[],[f73,f317,f313])).
% 0.75/0.49 thf(f322,definition,(
% 0.75/0.49 spl19_53 <=> ($false = sF12)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_53])],[avatar_definition])).
% 0.75/0.49 thf(f324,plain,(
% 0.75/0.49 ($false = sF12) | ~spl19_53),
% 0.75/0.49 inference(avatar_component_clause,[],[f322])).
% 0.75/0.49 thf(f326,definition,(
% 0.75/0.49 spl19_54 <=> ($true = ((f2 @ sF11)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_54])],[avatar_definition])).
% 0.75/0.49 thf(f327,plain,(
% 0.75/0.49 ($true != ((f2 @ sF11))) | spl19_54),
% 0.75/0.49 inference(avatar_component_clause,[],[f326])).
% 0.75/0.49 thf(f328,plain,(
% 0.75/0.49 ($true = ((f2 @ sF11))) | ~spl19_54),
% 0.75/0.49 inference(avatar_component_clause,[],[f326])).
% 0.75/0.49 thf(f329,plain,(
% 0.75/0.49 spl19_53 | spl19_54),
% 0.75/0.49 inference(avatar_split_clause,[],[f72,f326,f322])).
% 0.75/0.49 thf(f331,definition,(
% 0.75/0.49 spl19_55 <=> ($true = sF13)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_55])],[avatar_definition])).
% 0.75/0.49 thf(f332,plain,(
% 0.75/0.49 ($true != sF13) | spl19_55),
% 0.75/0.49 inference(avatar_component_clause,[],[f331])).
% 0.75/0.49 thf(f333,plain,(
% 0.75/0.49 ($true = sF13) | ~spl19_55),
% 0.75/0.49 inference(avatar_component_clause,[],[f331])).
% 0.75/0.49 thf(f335,definition,(
% 0.75/0.49 spl19_56 <=> ($false = ((f2 @ sF12)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_56])],[avatar_definition])).
% 0.75/0.49 thf(f336,plain,(
% 0.75/0.49 ($false != ((f2 @ sF12))) | spl19_56),
% 0.75/0.49 inference(avatar_component_clause,[],[f335])).
% 0.75/0.49 thf(f337,plain,(
% 0.75/0.49 ($false = ((f2 @ sF12))) | ~spl19_56),
% 0.75/0.49 inference(avatar_component_clause,[],[f335])).
% 0.75/0.49 thf(f338,plain,(
% 0.75/0.49 spl19_55 | spl19_56),
% 0.75/0.49 inference(avatar_split_clause,[],[f75,f335,f331])).
% 0.75/0.49 thf(f340,definition,(
% 0.75/0.49 spl19_57 <=> ($false = sF13)),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_57])],[avatar_definition])).
% 0.75/0.49 thf(f342,plain,(
% 0.75/0.49 ($false = sF13) | ~spl19_57),
% 0.75/0.49 inference(avatar_component_clause,[],[f340])).
% 0.75/0.49 thf(f344,definition,(
% 0.75/0.49 spl19_58 <=> ($true = ((f2 @ sF12)))),
% 0.75/0.49 introduced(definition,[new_symbols(definition,[spl19_58])],[avatar_definition])).
% 0.75/0.49 thf(f345,plain,(
% 0.75/0.49 ($true != ((f2 @ sF12))) | spl19_58),
% 0.75/0.49 inference(avatar_component_clause,[],[f344])).
% 0.75/0.49 thf(f346,plain,(
% 0.75/0.50 ($true = ((f2 @ sF12))) | ~spl19_58),
% 0.75/0.50 inference(avatar_component_clause,[],[f344])).
% 0.75/0.50 thf(f347,plain,(
% 0.75/0.50 spl19_57 | spl19_58),
% 0.75/0.50 inference(avatar_split_clause,[],[f74,f344,f340])).
% 0.75/0.50 thf(f349,definition,(
% 0.75/0.50 spl19_59 <=> ($true = sF14)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_59])],[avatar_definition])).
% 0.75/0.50 thf(f351,plain,(
% 0.75/0.50 ($true = sF14) | ~spl19_59),
% 0.75/0.50 inference(avatar_component_clause,[],[f349])).
% 0.75/0.50 thf(f353,definition,(
% 0.75/0.50 spl19_60 <=> ($false = ((f2 @ sF13)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_60])],[avatar_definition])).
% 0.75/0.50 thf(f355,plain,(
% 0.75/0.50 ($false = ((f2 @ sF13))) | ~spl19_60),
% 0.75/0.50 inference(avatar_component_clause,[],[f353])).
% 0.75/0.50 thf(f356,plain,(
% 0.75/0.50 spl19_59 | spl19_60),
% 0.75/0.50 inference(avatar_split_clause,[],[f77,f353,f349])).
% 0.75/0.50 thf(f358,definition,(
% 0.75/0.50 spl19_61 <=> ($false = sF14)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_61])],[avatar_definition])).
% 0.75/0.50 thf(f360,plain,(
% 0.75/0.50 ($false = sF14) | ~spl19_61),
% 0.75/0.50 inference(avatar_component_clause,[],[f358])).
% 0.75/0.50 thf(f362,definition,(
% 0.75/0.50 spl19_62 <=> ($true = ((f2 @ sF13)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_62])],[avatar_definition])).
% 0.75/0.50 thf(f363,plain,(
% 0.75/0.50 ($true != ((f2 @ sF13))) | spl19_62),
% 0.75/0.50 inference(avatar_component_clause,[],[f362])).
% 0.75/0.50 thf(f364,plain,(
% 0.75/0.50 ($true = ((f2 @ sF13))) | ~spl19_62),
% 0.75/0.50 inference(avatar_component_clause,[],[f362])).
% 0.75/0.50 thf(f365,plain,(
% 0.75/0.50 spl19_61 | spl19_62),
% 0.75/0.50 inference(avatar_split_clause,[],[f76,f362,f358])).
% 0.75/0.50 thf(f367,definition,(
% 0.75/0.50 spl19_63 <=> ($true = sF15)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_63])],[avatar_definition])).
% 0.75/0.50 thf(f369,plain,(
% 0.75/0.50 ($true = sF15) | ~spl19_63),
% 0.75/0.50 inference(avatar_component_clause,[],[f367])).
% 0.75/0.50 thf(f371,definition,(
% 0.75/0.50 spl19_64 <=> ($false = ((f1 @ sF14)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_64])],[avatar_definition])).
% 0.75/0.50 thf(f372,plain,(
% 0.75/0.50 ($false != ((f1 @ sF14))) | spl19_64),
% 0.75/0.50 inference(avatar_component_clause,[],[f371])).
% 0.75/0.50 thf(f373,plain,(
% 0.75/0.50 ($false = ((f1 @ sF14))) | ~spl19_64),
% 0.75/0.50 inference(avatar_component_clause,[],[f371])).
% 0.75/0.50 thf(f374,plain,(
% 0.75/0.50 spl19_63 | spl19_64),
% 0.75/0.50 inference(avatar_split_clause,[],[f79,f371,f367])).
% 0.75/0.50 thf(f376,definition,(
% 0.75/0.50 spl19_65 <=> ($false = sF15)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_65])],[avatar_definition])).
% 0.75/0.50 thf(f378,plain,(
% 0.75/0.50 ($false = sF15) | ~spl19_65),
% 0.75/0.50 inference(avatar_component_clause,[],[f376])).
% 0.75/0.50 thf(f380,definition,(
% 0.75/0.50 spl19_66 <=> ($true = ((f1 @ sF14)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_66])],[avatar_definition])).
% 0.75/0.50 thf(f381,plain,(
% 0.75/0.50 ($true != ((f1 @ sF14))) | spl19_66),
% 0.75/0.50 inference(avatar_component_clause,[],[f380])).
% 0.75/0.50 thf(f382,plain,(
% 0.75/0.50 ($true = ((f1 @ sF14))) | ~spl19_66),
% 0.75/0.50 inference(avatar_component_clause,[],[f380])).
% 0.75/0.50 thf(f383,plain,(
% 0.75/0.50 spl19_65 | spl19_66),
% 0.75/0.50 inference(avatar_split_clause,[],[f78,f380,f376])).
% 0.75/0.50 thf(f385,definition,(
% 0.75/0.50 spl19_67 <=> ($true = sF16)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_67])],[avatar_definition])).
% 0.75/0.50 thf(f386,plain,(
% 0.75/0.50 ($true != sF16) | spl19_67),
% 0.75/0.50 inference(avatar_component_clause,[],[f385])).
% 0.75/0.50 thf(f387,plain,(
% 0.75/0.50 ($true = sF16) | ~spl19_67),
% 0.75/0.50 inference(avatar_component_clause,[],[f385])).
% 0.75/0.50 thf(f389,definition,(
% 0.75/0.50 spl19_68 <=> ($false = ((f0 @ sF15)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_68])],[avatar_definition])).
% 0.75/0.50 thf(f391,plain,(
% 0.75/0.50 ($false = ((f0 @ sF15))) | ~spl19_68),
% 0.75/0.50 inference(avatar_component_clause,[],[f389])).
% 0.75/0.50 thf(f392,plain,(
% 0.75/0.50 spl19_67 | spl19_68),
% 0.75/0.50 inference(avatar_split_clause,[],[f81,f389,f385])).
% 0.75/0.50 thf(f394,definition,(
% 0.75/0.50 spl19_69 <=> ($false = sF16)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_69])],[avatar_definition])).
% 0.75/0.50 thf(f396,plain,(
% 0.75/0.50 ($false = sF16) | ~spl19_69),
% 0.75/0.50 inference(avatar_component_clause,[],[f394])).
% 0.75/0.50 thf(f398,definition,(
% 0.75/0.50 spl19_70 <=> ($true = ((f0 @ sF15)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_70])],[avatar_definition])).
% 0.75/0.50 thf(f399,plain,(
% 0.75/0.50 ($true != ((f0 @ sF15))) | spl19_70),
% 0.75/0.50 inference(avatar_component_clause,[],[f398])).
% 0.75/0.50 thf(f400,plain,(
% 0.75/0.50 ($true = ((f0 @ sF15))) | ~spl19_70),
% 0.75/0.50 inference(avatar_component_clause,[],[f398])).
% 0.75/0.50 thf(f401,plain,(
% 0.75/0.50 spl19_69 | spl19_70),
% 0.75/0.50 inference(avatar_split_clause,[],[f80,f398,f394])).
% 0.75/0.50 thf(f403,definition,(
% 0.75/0.50 spl19_71 <=> ($true = sF17)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_71])],[avatar_definition])).
% 0.75/0.50 thf(f405,plain,(
% 0.75/0.50 ($true = sF17) | ~spl19_71),
% 0.75/0.50 inference(avatar_component_clause,[],[f403])).
% 0.75/0.50 thf(f407,definition,(
% 0.75/0.50 spl19_72 <=> ($false = ((f0 @ sF16)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_72])],[avatar_definition])).
% 0.75/0.50 thf(f408,plain,(
% 0.75/0.50 ($false != ((f0 @ sF16))) | spl19_72),
% 0.75/0.50 inference(avatar_component_clause,[],[f407])).
% 0.75/0.50 thf(f409,plain,(
% 0.75/0.50 ($false = ((f0 @ sF16))) | ~spl19_72),
% 0.75/0.50 inference(avatar_component_clause,[],[f407])).
% 0.75/0.50 thf(f410,plain,(
% 0.75/0.50 spl19_71 | spl19_72),
% 0.75/0.50 inference(avatar_split_clause,[],[f83,f407,f403])).
% 0.75/0.50 thf(f412,definition,(
% 0.75/0.50 spl19_73 <=> ($false = sF17)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_73])],[avatar_definition])).
% 0.75/0.50 thf(f414,plain,(
% 0.75/0.50 ($false = sF17) | ~spl19_73),
% 0.75/0.50 inference(avatar_component_clause,[],[f412])).
% 0.75/0.50 thf(f416,definition,(
% 0.75/0.50 spl19_74 <=> ($true = ((f0 @ sF16)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_74])],[avatar_definition])).
% 0.75/0.50 thf(f418,plain,(
% 0.75/0.50 ($true = ((f0 @ sF16))) | ~spl19_74),
% 0.75/0.50 inference(avatar_component_clause,[],[f416])).
% 0.75/0.50 thf(f419,plain,(
% 0.75/0.50 spl19_73 | spl19_74),
% 0.75/0.50 inference(avatar_split_clause,[],[f82,f416,f412])).
% 0.75/0.50 thf(f421,definition,(
% 0.75/0.50 spl19_75 <=> ($false = ((f0 @ sF17)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_75])],[avatar_definition])).
% 0.75/0.50 thf(f423,plain,(
% 0.75/0.50 ($false = ((f0 @ sF17))) | ~spl19_75),
% 0.75/0.50 inference(avatar_component_clause,[],[f421])).
% 0.75/0.50 thf(f424,plain,(
% 0.75/0.50 spl19_3 | spl19_75),
% 0.75/0.50 inference(avatar_split_clause,[],[f85,f421,f96])).
% 0.75/0.50 thf(f426,definition,(
% 0.75/0.50 spl19_76 <=> ($true = ((f0 @ sF17)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_76])],[avatar_definition])).
% 0.75/0.50 thf(f428,plain,(
% 0.75/0.50 ($true = ((f0 @ sF17))) | ~spl19_76),
% 0.75/0.50 inference(avatar_component_clause,[],[f426])).
% 0.75/0.50 thf(f429,plain,(
% 0.75/0.50 spl19_1 | spl19_76),
% 0.75/0.50 inference(avatar_split_clause,[],[f84,f426,f87])).
% 0.75/0.50 thf(f430,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_2 | ~spl19_4)),
% 0.75/0.50 inference(forward_demodulation,[],[f102,f93])).
% 0.75/0.50 thf(f431,plain,(
% 0.75/0.50 $false | (~spl19_2 | ~spl19_4)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f430])).
% 0.75/0.50 thf(f432,plain,(
% 0.75/0.50 ~spl19_2 | ~spl19_4),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f431])).
% 0.75/0.50 thf(f433,plain,(
% 0.75/0.50 ($true = ((f0 @ $true))) | (~spl19_71 | ~spl19_76)),
% 0.75/0.50 inference(forward_demodulation,[],[f428,f405])).
% 0.75/0.50 thf(f435,plain,(
% 0.75/0.50 ($false = ((f0 @ $true))) | (~spl19_33 | ~spl19_37)),
% 0.75/0.50 inference(forward_demodulation,[],[f251,f233])).
% 0.75/0.50 thf(f446,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_5 | ~spl19_7)),
% 0.75/0.50 inference(constrained_superposition,[],[f116,f107])).
% 0.75/0.50 thf(f450,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_7)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f446])).
% 0.75/0.50 thf(f451,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_7),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f450])).
% 0.75/0.50 thf(f455,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_9 | ~spl19_11)),
% 0.75/0.50 inference(constrained_superposition,[],[f134,f125])).
% 0.75/0.50 thf(f459,plain,(
% 0.75/0.50 $false | (~spl19_9 | ~spl19_11)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f455])).
% 0.75/0.50 thf(f460,plain,(
% 0.75/0.50 ~spl19_9 | ~spl19_11),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f459])).
% 0.75/0.50 thf(f463,plain,(
% 0.75/0.50 ($true = ((f3 @ $true))) | (~spl19_5 | ~spl19_12)),
% 0.75/0.50 inference(forward_demodulation,[],[f138,f107])).
% 0.75/0.50 thf(f473,plain,(
% 0.75/0.50 ($false = ((f3 @ $true))) | (~spl19_9 | ~spl19_14)),
% 0.75/0.50 inference(forward_demodulation,[],[f147,f125])).
% 0.75/0.50 thf(f475,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_17 | ~spl19_19)),
% 0.75/0.50 inference(constrained_superposition,[],[f170,f161])).
% 0.75/0.50 thf(f479,plain,(
% 0.75/0.50 $false | (~spl19_17 | ~spl19_19)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f475])).
% 0.75/0.50 thf(f480,plain,(
% 0.75/0.50 ~spl19_17 | ~spl19_19),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f479])).
% 0.75/0.50 thf(f483,plain,(
% 0.75/0.50 ($false = ((f3 @ $false))) | (~spl19_15 | ~spl19_18)),
% 0.75/0.50 inference(forward_demodulation,[],[f165,f152])).
% 0.75/0.50 thf(f485,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_21 | ~spl19_23)),
% 0.75/0.50 inference(constrained_superposition,[],[f188,f179])).
% 0.75/0.50 thf(f489,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_23)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f485])).
% 0.75/0.50 thf(f490,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_23),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f489])).
% 0.75/0.50 thf(f493,plain,(
% 0.75/0.50 ($false = ((f2 @ $false))) | (~spl19_19 | ~spl19_22)),
% 0.75/0.50 inference(forward_demodulation,[],[f183,f170])).
% 0.75/0.50 thf(f495,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_25 | ~spl19_27)),
% 0.75/0.50 inference(constrained_superposition,[],[f206,f197])).
% 0.75/0.50 thf(f499,plain,(
% 0.75/0.50 $false | (~spl19_25 | ~spl19_27)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f495])).
% 0.75/0.50 thf(f500,plain,(
% 0.75/0.50 ~spl19_25 | ~spl19_27),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f499])).
% 0.75/0.50 thf(f503,plain,(
% 0.75/0.50 ($false = ((f1 @ $false))) | (~spl19_23 | ~spl19_26)),
% 0.75/0.50 inference(forward_demodulation,[],[f201,f188])).
% 0.75/0.50 thf(f513,plain,(
% 0.75/0.50 ($false = ((f1 @ $false))) | (~spl19_27 | ~spl19_30)),
% 0.75/0.50 inference(forward_demodulation,[],[f219,f206])).
% 0.75/0.50 thf(f523,plain,(
% 0.75/0.50 ($false = ((f1 @ $false))) | (~spl19_31 | ~spl19_34)),
% 0.75/0.50 inference(forward_demodulation,[],[f237,f224])).
% 0.75/0.50 thf(f524,plain,(
% 0.75/0.50 ($false = ((f0 @ $false))) | (~spl19_35 | ~spl19_37)),
% 0.75/0.50 inference(forward_demodulation,[],[f251,f242])).
% 0.75/0.50 thf(f526,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_39 | ~spl19_41)),
% 0.75/0.50 inference(constrained_superposition,[],[f270,f261])).
% 0.75/0.50 thf(f530,plain,(
% 0.75/0.50 $false | (~spl19_39 | ~spl19_41)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f526])).
% 0.75/0.50 thf(f531,plain,(
% 0.75/0.50 ~spl19_39 | ~spl19_41),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f530])).
% 0.75/0.50 thf(f534,plain,(
% 0.75/0.50 ($false = ((f4 @ $true))) | (~spl19_5 | ~spl19_40)),
% 0.75/0.50 inference(forward_demodulation,[],[f265,f107])).
% 0.75/0.50 thf(f544,plain,(
% 0.75/0.50 ($false = ((f4 @ $false))) | (~spl19_41 | ~spl19_44)),
% 0.75/0.50 inference(forward_demodulation,[],[f283,f270])).
% 0.75/0.50 thf(f546,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_47 | ~spl19_49)),
% 0.75/0.50 inference(constrained_superposition,[],[f306,f297])).
% 0.75/0.50 thf(f550,plain,(
% 0.75/0.50 $false | (~spl19_47 | ~spl19_49)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f546])).
% 0.75/0.50 thf(f551,plain,(
% 0.75/0.50 ~spl19_47 | ~spl19_49),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f550])).
% 0.75/0.50 thf(f554,plain,(
% 0.75/0.50 ($false = ((f3 @ $false))) | (~spl19_45 | ~spl19_48)),
% 0.75/0.50 inference(forward_demodulation,[],[f301,f288])).
% 0.75/0.50 thf(f584,plain,(
% 0.75/0.50 ($false = ((f2 @ $false))) | (~spl19_57 | ~spl19_60)),
% 0.75/0.50 inference(forward_demodulation,[],[f355,f342])).
% 0.75/0.50 thf(f594,plain,(
% 0.75/0.50 ($false = ((f1 @ $false))) | (~spl19_61 | ~spl19_64)),
% 0.75/0.50 inference(forward_demodulation,[],[f373,f360])).
% 0.75/0.50 thf(f614,plain,(
% 0.75/0.50 ($false = ((f0 @ $false))) | (~spl19_69 | ~spl19_72)),
% 0.75/0.50 inference(forward_demodulation,[],[f409,f396])).
% 0.75/0.50 thf(f615,plain,(
% 0.75/0.50 ($true = ((f0 @ $false))) | (~spl19_73 | ~spl19_76)),
% 0.75/0.50 inference(forward_demodulation,[],[f428,f414])).
% 0.75/0.50 thf(f616,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_35 | ~spl19_37 | ~spl19_73 | ~spl19_76)),
% 0.75/0.50 inference(forward_demodulation,[],[f615,f524])).
% 0.75/0.50 thf(f617,plain,(
% 0.75/0.50 $false | (~spl19_35 | ~spl19_37 | ~spl19_73 | ~spl19_76)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f616])).
% 0.75/0.50 thf(f618,plain,(
% 0.75/0.50 ~spl19_35 | ~spl19_37 | ~spl19_73 | ~spl19_76),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f617])).
% 0.75/0.50 thf(f619,plain,(
% 0.75/0.50 ($true = ((f1 @ $false))) | (~spl19_31 | ~spl19_36)),
% 0.75/0.50 inference(forward_demodulation,[],[f246,f224])).
% 0.75/0.50 thf(f623,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_23 | ~spl19_26 | ~spl19_31 | ~spl19_36)),
% 0.75/0.50 inference(forward_demodulation,[],[f619,f503])).
% 0.75/0.50 thf(f624,plain,(
% 0.75/0.50 $false | (~spl19_23 | ~spl19_26 | ~spl19_31 | ~spl19_36)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f623])).
% 0.75/0.50 thf(f625,plain,(
% 0.75/0.50 ~spl19_23 | ~spl19_26 | ~spl19_31 | ~spl19_36),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f624])).
% 0.75/0.50 thf(f626,plain,(
% 0.75/0.50 ($true = ((f1 @ $false))) | (~spl19_27 | ~spl19_32)),
% 0.75/0.50 inference(forward_demodulation,[],[f228,f206])).
% 0.75/0.50 thf(f627,plain,(
% 0.75/0.50 ($true = ((f1 @ $false))) | (~spl19_61 | ~spl19_66)),
% 0.75/0.50 inference(forward_demodulation,[],[f382,f360])).
% 0.75/0.50 thf(f628,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_69 | ~spl19_72 | ~spl19_73 | ~spl19_76)),
% 0.75/0.50 inference(forward_demodulation,[],[f615,f614])).
% 0.75/0.50 thf(f629,plain,(
% 0.75/0.50 $false | (~spl19_69 | ~spl19_72 | ~spl19_73 | ~spl19_76)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f628])).
% 0.75/0.50 thf(f630,plain,(
% 0.75/0.50 ~spl19_69 | ~spl19_72 | ~spl19_73 | ~spl19_76),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f629])).
% 0.75/0.50 thf(f631,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_34 | ~spl19_36)),
% 0.75/0.50 inference(forward_demodulation,[],[f246,f237])).
% 0.75/0.50 thf(f632,plain,(
% 0.75/0.50 $false | (~spl19_34 | ~spl19_36)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f631])).
% 0.75/0.50 thf(f633,plain,(
% 0.75/0.50 ~spl19_34 | ~spl19_36),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f632])).
% 0.75/0.50 thf(f634,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_23 | ~spl19_26 | ~spl19_27 | ~spl19_32)),
% 0.75/0.50 inference(forward_demodulation,[],[f626,f503])).
% 0.75/0.50 thf(f635,plain,(
% 0.75/0.50 $false | (~spl19_23 | ~spl19_26 | ~spl19_27 | ~spl19_32)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f634])).
% 0.75/0.50 thf(f636,plain,(
% 0.75/0.50 ~spl19_23 | ~spl19_26 | ~spl19_27 | ~spl19_32),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f635])).
% 0.75/0.50 thf(f637,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_23 | ~spl19_26 | ~spl19_61 | ~spl19_66)),
% 0.75/0.50 inference(forward_demodulation,[],[f627,f503])).
% 0.75/0.50 thf(f638,plain,(
% 0.75/0.50 $false | (~spl19_23 | ~spl19_26 | ~spl19_61 | ~spl19_66)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f637])).
% 0.75/0.50 thf(f639,plain,(
% 0.75/0.50 ~spl19_23 | ~spl19_26 | ~spl19_61 | ~spl19_66),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f638])).
% 0.75/0.50 thf(f642,plain,(
% 0.75/0.50 ($true = ((f2 @ $false))) | (~spl19_57 | ~spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f364,f342])).
% 0.75/0.50 thf(f643,plain,(
% 0.75/0.50 ($true = ((f0 @ $false))) | (~spl19_69 | ~spl19_74)),
% 0.75/0.50 inference(forward_demodulation,[],[f418,f396])).
% 0.75/0.50 thf(f644,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_64 | ~spl19_66)),
% 0.75/0.50 inference(forward_demodulation,[],[f382,f373])).
% 0.75/0.50 thf(f645,plain,(
% 0.75/0.50 $false | (~spl19_64 | ~spl19_66)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f644])).
% 0.75/0.50 thf(f646,plain,(
% 0.75/0.50 ~spl19_64 | ~spl19_66),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f645])).
% 0.75/0.50 thf(f648,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_19 | ~spl19_22 | ~spl19_57 | ~spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f642,f493])).
% 0.75/0.50 thf(f649,plain,(
% 0.75/0.50 $false | (~spl19_19 | ~spl19_22 | ~spl19_57 | ~spl19_62)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f648])).
% 0.75/0.50 thf(f650,plain,(
% 0.75/0.50 ~spl19_19 | ~spl19_22 | ~spl19_57 | ~spl19_62),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f649])).
% 0.75/0.50 thf(f654,plain,(
% 0.75/0.50 ($true = ((f2 @ $false))) | (~spl19_53 | ~spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f346,f324])).
% 0.75/0.50 thf(f655,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_68 | ~spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f400,f391])).
% 0.75/0.50 thf(f656,plain,(
% 0.75/0.50 $false | (~spl19_68 | ~spl19_70)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f655])).
% 0.75/0.50 thf(f657,plain,(
% 0.75/0.50 ~spl19_68 | ~spl19_70),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f656])).
% 0.75/0.50 thf(f658,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_72 | ~spl19_74)),
% 0.75/0.50 inference(forward_demodulation,[],[f418,f409])).
% 0.75/0.50 thf(f659,plain,(
% 0.75/0.50 $false | (~spl19_72 | ~spl19_74)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f658])).
% 0.75/0.50 thf(f660,plain,(
% 0.75/0.50 ~spl19_72 | ~spl19_74),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f659])).
% 0.75/0.50 thf(f661,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_60 | ~spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f364,f355])).
% 0.75/0.50 thf(f662,plain,(
% 0.75/0.50 $false | (~spl19_60 | ~spl19_62)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f661])).
% 0.75/0.50 thf(f663,plain,(
% 0.75/0.50 ~spl19_60 | ~spl19_62),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f662])).
% 0.75/0.50 thf(f664,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_19 | ~spl19_22 | ~spl19_53 | ~spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f654,f493])).
% 0.75/0.50 thf(f665,plain,(
% 0.75/0.50 $false | (~spl19_19 | ~spl19_22 | ~spl19_53 | ~spl19_58)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f664])).
% 0.75/0.50 thf(f666,plain,(
% 0.75/0.50 ~spl19_19 | ~spl19_22 | ~spl19_53 | ~spl19_58),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f665])).
% 0.75/0.50 thf(f667,plain,(
% 0.75/0.50 ($true = ((f2 @ $false))) | (~spl19_49 | ~spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f328,f306])).
% 0.75/0.50 thf(f669,plain,(
% 0.75/0.50 ($false != ((f0 @ $true))) | (~spl19_67 | spl19_72)),
% 0.75/0.50 inference(forward_demodulation,[],[f408,f387])).
% 0.75/0.50 thf(f672,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_56 | ~spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f346,f337])).
% 0.75/0.50 thf(f673,plain,(
% 0.75/0.50 $false | (~spl19_56 | ~spl19_58)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f672])).
% 0.75/0.50 thf(f674,plain,(
% 0.75/0.50 ~spl19_56 | ~spl19_58),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f673])).
% 0.75/0.50 thf(f675,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_19 | ~spl19_22 | ~spl19_49 | ~spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f667,f493])).
% 0.75/0.50 thf(f676,plain,(
% 0.75/0.50 $false | (~spl19_19 | ~spl19_22 | ~spl19_49 | ~spl19_54)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f675])).
% 0.75/0.50 thf(f677,plain,(
% 0.75/0.50 ~spl19_19 | ~spl19_22 | ~spl19_49 | ~spl19_54),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f676])).
% 0.75/0.50 thf(f680,plain,(
% 0.75/0.50 ($true = ((f3 @ $false))) | (~spl19_45 | ~spl19_50)),
% 0.75/0.50 inference(forward_demodulation,[],[f310,f288])).
% 0.75/0.50 thf(f681,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_52 | ~spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f328,f319])).
% 0.75/0.50 thf(f682,plain,(
% 0.75/0.50 $false | (~spl19_52 | ~spl19_54)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f681])).
% 0.75/0.50 thf(f683,plain,(
% 0.75/0.50 ~spl19_52 | ~spl19_54),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f682])).
% 0.75/0.50 thf(f684,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_15 | ~spl19_18 | ~spl19_45 | ~spl19_50)),
% 0.75/0.50 inference(forward_demodulation,[],[f680,f483])).
% 0.75/0.50 thf(f685,plain,(
% 0.75/0.50 $false | (~spl19_15 | ~spl19_18 | ~spl19_45 | ~spl19_50)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f684])).
% 0.75/0.50 thf(f686,plain,(
% 0.75/0.50 ~spl19_15 | ~spl19_18 | ~spl19_45 | ~spl19_50),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f685])).
% 0.75/0.50 thf(f688,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_48 | ~spl19_50)),
% 0.75/0.50 inference(forward_demodulation,[],[f310,f301])).
% 0.75/0.50 thf(f689,plain,(
% 0.75/0.50 $false | (~spl19_48 | ~spl19_50)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f688])).
% 0.75/0.50 thf(f690,plain,(
% 0.75/0.50 ~spl19_48 | ~spl19_50),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f689])).
% 0.75/0.50 thf(f695,plain,(
% 0.75/0.50 ($false != ((f3 @ $true))) | (~spl19_43 | spl19_48)),
% 0.75/0.50 inference(forward_demodulation,[],[f300,f279])).
% 0.75/0.50 thf(f701,plain,(
% 0.75/0.50 ($true != ((f3 @ $true))) | (~spl19_43 | spl19_50)),
% 0.75/0.50 inference(forward_demodulation,[],[f309,f279])).
% 0.75/0.50 thf(f711,plain,(
% 0.75/0.50 ($true = ((f0 @ $false))) | (~spl19_65 | ~spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f400,f378])).
% 0.75/0.50 thf(f712,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_12 | ~spl19_43 | spl19_50)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f701,f463])).
% 0.75/0.50 thf(f713,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_12 | ~spl19_43 | spl19_50),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f712])).
% 0.75/0.50 thf(f720,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_35 | ~spl19_37 | ~spl19_65 | ~spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f711,f524])).
% 0.75/0.50 thf(f721,plain,(
% 0.75/0.50 $false | (~spl19_35 | ~spl19_37 | ~spl19_65 | ~spl19_70)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f720])).
% 0.75/0.50 thf(f722,plain,(
% 0.75/0.50 ~spl19_35 | ~spl19_37 | ~spl19_65 | ~spl19_70),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f721])).
% 0.75/0.50 thf(f723,plain,(
% 0.75/0.50 ($false = ((f3 @ $true))) | (~spl19_5 | ~spl19_10)),
% 0.75/0.50 inference(forward_demodulation,[],[f129,f107])).
% 0.75/0.50 thf(f724,plain,(
% 0.75/0.50 ($false != ((f3 @ $true))) | (~spl19_43 | spl19_48)),
% 0.75/0.50 inference(forward_demodulation,[],[f300,f279])).
% 0.75/0.50 thf(f731,plain,(
% 0.75/0.50 ($false != ((f2 @ $true))) | (~spl19_51 | spl19_56)),
% 0.75/0.50 inference(forward_demodulation,[],[f336,f315])).
% 0.75/0.50 thf(f733,plain,(
% 0.75/0.50 ($true = ((f2 @ $true))) | (~spl19_51 | ~spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f346,f315])).
% 0.75/0.50 thf(f738,plain,(
% 0.75/0.50 ($false != ((f1 @ $true))) | (~spl19_59 | spl19_64)),
% 0.75/0.50 inference(forward_demodulation,[],[f372,f351])).
% 0.75/0.50 thf(f742,plain,(
% 0.75/0.50 ($true = ((f0 @ $true))) | (~spl19_63 | ~spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f400,f369])).
% 0.75/0.50 thf(f743,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_10 | ~spl19_43 | spl19_48)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f724,f723])).
% 0.75/0.50 thf(f744,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_10 | ~spl19_43 | spl19_48),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f743])).
% 0.75/0.50 thf(f746,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF0) | spl19_5),
% 0.75/0.50 inference(constrained_superposition,[],[f106,f6])).
% 0.75/0.50 thf(f747,plain,(
% 0.75/0.50 ($false = sF0) | spl19_5),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f746])).
% 0.75/0.50 thf(f753,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF1) | spl19_9),
% 0.75/0.50 inference(constrained_superposition,[],[f124,f6])).
% 0.75/0.50 thf(f754,plain,(
% 0.75/0.50 ($false = sF1) | spl19_9),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f753])).
% 0.75/0.50 thf(f760,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF6) | spl19_29),
% 0.75/0.50 inference(constrained_superposition,[],[f214,f6])).
% 0.75/0.50 thf(f761,plain,(
% 0.75/0.50 ($false = sF6) | spl19_29),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f760])).
% 0.75/0.50 thf(f776,plain,(
% 0.75/0.50 ($false = ((f4 @ $true))) | (x = $false) | ~spl19_6),
% 0.75/0.50 inference(constrained_superposition,[],[f111,f6])).
% 0.75/0.50 thf(f780,definition,(
% 0.75/0.50 spl19_77 <=> (x = $false)),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_77])],[avatar_definition])).
% 0.75/0.50 thf(f781,plain,(
% 0.75/0.50 (x != $false) | spl19_77),
% 0.75/0.50 inference(avatar_component_clause,[],[f780])).
% 0.75/0.50 thf(f782,plain,(
% 0.75/0.50 (x = $false) | ~spl19_77),
% 0.75/0.50 inference(avatar_component_clause,[],[f780])).
% 0.75/0.50 thf(f784,definition,(
% 0.75/0.50 spl19_78 <=> ($false = ((f4 @ $true)))),
% 0.75/0.50 introduced(definition,[new_symbols(definition,[spl19_78])],[avatar_definition])).
% 0.75/0.50 thf(f786,plain,(
% 0.75/0.50 ($false = ((f4 @ $true))) | ~spl19_78),
% 0.75/0.50 inference(avatar_component_clause,[],[f784])).
% 0.75/0.50 thf(f787,plain,(
% 0.75/0.50 spl19_77 | spl19_78 | ~spl19_6),
% 0.75/0.50 inference(avatar_split_clause,[],[f776,f109,f784,f780])).
% 0.75/0.50 thf(f788,plain,(
% 0.75/0.50 spl19_78 | ~spl19_5 | ~spl19_40),
% 0.75/0.50 inference(avatar_split_clause,[],[f534,f263,f105,f784])).
% 0.75/0.50 thf(f795,plain,(
% 0.75/0.50 ($true = ((f3 @ $true))) | (~spl19_9 | ~spl19_16)),
% 0.75/0.50 inference(forward_demodulation,[],[f156,f125])).
% 0.75/0.50 thf(f796,plain,(
% 0.75/0.50 ($false = ((f3 @ $true))) | (~spl19_13 | ~spl19_18)),
% 0.75/0.50 inference(forward_demodulation,[],[f165,f143])).
% 0.75/0.50 thf(f797,plain,(
% 0.75/0.50 $false | (~spl19_13 | ~spl19_18 | ~spl19_43 | spl19_48)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f796,f695])).
% 0.75/0.50 thf(f798,plain,(
% 0.75/0.50 ~spl19_13 | ~spl19_18 | ~spl19_43 | spl19_48),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f797])).
% 0.75/0.50 thf(f799,plain,(
% 0.75/0.50 spl19_11 | spl19_9),
% 0.75/0.50 inference(avatar_split_clause,[],[f754,f123,f132])).
% 0.75/0.50 thf(f802,plain,(
% 0.75/0.50 ($false = ((f3 @ $false))) | (~spl19_11 | ~spl19_14)),
% 0.75/0.50 inference(forward_demodulation,[],[f147,f134])).
% 0.75/0.50 thf(f813,plain,(
% 0.75/0.50 ($true = ((f3 @ $false))) | (~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(forward_demodulation,[],[f156,f134])).
% 0.75/0.50 thf(f830,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF2) | spl19_13),
% 0.75/0.50 inference(constrained_superposition,[],[f142,f6])).
% 0.75/0.50 thf(f831,plain,(
% 0.75/0.50 ($false = sF2) | spl19_13),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f830])).
% 0.75/0.50 thf(f835,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF3) | spl19_17),
% 0.75/0.50 inference(constrained_superposition,[],[f160,f6])).
% 0.75/0.50 thf(f836,plain,(
% 0.75/0.50 ($false = sF3) | spl19_17),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f835])).
% 0.75/0.50 thf(f841,plain,(
% 0.75/0.50 ($true = ((f2 @ $false))) | (~spl19_19 | ~spl19_24)),
% 0.75/0.50 inference(forward_demodulation,[],[f192,f170])).
% 0.75/0.50 thf(f842,plain,(
% 0.75/0.50 ($false = ((f1 @ $true))) | (~spl19_21 | ~spl19_26)),
% 0.75/0.50 inference(forward_demodulation,[],[f201,f179])).
% 0.75/0.50 thf(f845,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_26 | ~spl19_59 | spl19_64)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f842,f738])).
% 0.75/0.50 thf(f846,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_26 | ~spl19_59 | spl19_64),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f845])).
% 0.75/0.50 thf(f847,plain,(
% 0.75/0.50 ($false != ((f1 @ $true))) | (~spl19_21 | spl19_26)),
% 0.75/0.50 inference(forward_demodulation,[],[f200,f179])).
% 0.75/0.50 thf(f849,plain,(
% 0.75/0.50 ($true = ((f1 @ $true))) | (~spl19_21 | ~spl19_28)),
% 0.75/0.50 inference(forward_demodulation,[],[f210,f179])).
% 0.75/0.50 thf(f850,plain,(
% 0.75/0.50 ($false = ((f1 @ $true))) | (~spl19_25 | ~spl19_30)),
% 0.75/0.50 inference(forward_demodulation,[],[f219,f197])).
% 0.75/0.50 thf(f858,plain,(
% 0.75/0.50 ($true = ((f1 @ $true))) | (~spl19_25 | ~spl19_32)),
% 0.75/0.50 inference(forward_demodulation,[],[f228,f197])).
% 0.75/0.50 thf(f862,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF11) | spl19_47),
% 0.75/0.50 inference(constrained_superposition,[],[f296,f6])).
% 0.75/0.50 thf(f863,plain,(
% 0.75/0.50 ($false = sF11) | spl19_47),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f862])).
% 0.75/0.50 thf(f873,plain,(
% 0.75/0.50 ($true = ((f3 @ $false))) | (~spl19_15 | ~spl19_20)),
% 0.75/0.50 inference(constrained_superposition,[],[f174,f152])).
% 0.75/0.50 thf(f874,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_18 | ~spl19_20)),
% 0.75/0.50 inference(constrained_superposition,[],[f174,f165])).
% 0.75/0.50 thf(f878,plain,(
% 0.75/0.50 $false | (~spl19_18 | ~spl19_20)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f874])).
% 0.75/0.50 thf(f879,plain,(
% 0.75/0.50 ~spl19_18 | ~spl19_20),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f878])).
% 0.75/0.50 thf(f880,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_11 | ~spl19_14 | ~spl19_15 | ~spl19_20)),
% 0.75/0.50 inference(forward_demodulation,[],[f873,f802])).
% 0.75/0.50 thf(f881,plain,(
% 0.75/0.50 $false | (~spl19_11 | ~spl19_14 | ~spl19_15 | ~spl19_20)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f880])).
% 0.75/0.50 thf(f882,plain,(
% 0.75/0.50 ~spl19_11 | ~spl19_14 | ~spl19_15 | ~spl19_20),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f881])).
% 0.75/0.50 thf(f885,plain,(
% 0.75/0.50 ($false = ((f1 @ $true))) | (~spl19_29 | ~spl19_34)),
% 0.75/0.50 inference(constrained_superposition,[],[f237,f215])).
% 0.75/0.50 thf(f907,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_33 | ~spl19_37 | ~spl19_71 | ~spl19_76)),
% 0.75/0.50 inference(constrained_superposition,[],[f435,f433])).
% 0.75/0.50 thf(f911,plain,(
% 0.75/0.50 $false | (~spl19_33 | ~spl19_37 | ~spl19_71 | ~spl19_76)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f907])).
% 0.75/0.50 thf(f912,plain,(
% 0.75/0.50 ~spl19_33 | ~spl19_37 | ~spl19_71 | ~spl19_76),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f911])).
% 0.75/0.50 thf(f927,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_33 | ~spl19_37 | ~spl19_63 | ~spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f742,f435])).
% 0.75/0.50 thf(f928,plain,(
% 0.75/0.50 $false | (~spl19_33 | ~spl19_37 | ~spl19_63 | ~spl19_70)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f927])).
% 0.75/0.50 thf(f929,plain,(
% 0.75/0.50 ~spl19_33 | ~spl19_37 | ~spl19_63 | ~spl19_70),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f928])).
% 0.75/0.50 thf(f932,plain,(
% 0.75/0.50 ($true = ((f0 @ $true))) | (~spl19_33 | ~spl19_38)),
% 0.75/0.50 inference(forward_demodulation,[],[f256,f233])).
% 0.75/0.50 thf(f937,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_1 | ~spl19_3)),
% 0.75/0.50 inference(constrained_superposition,[],[f89,f98])).
% 0.75/0.50 thf(f941,plain,(
% 0.75/0.50 $false | (~spl19_1 | ~spl19_3)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f937])).
% 0.75/0.50 thf(f942,plain,(
% 0.75/0.50 ~spl19_1 | ~spl19_3),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f941])).
% 0.75/0.50 thf(f945,plain,(
% 0.75/0.50 ($false = ((f0 @ $true))) | (~spl19_71 | ~spl19_75)),
% 0.75/0.50 inference(forward_demodulation,[],[f423,f405])).
% 0.75/0.50 thf(f946,plain,(
% 0.75/0.50 $false | (~spl19_67 | ~spl19_71 | spl19_72 | ~spl19_75)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f945,f669])).
% 0.75/0.50 thf(f947,plain,(
% 0.75/0.50 ~spl19_67 | ~spl19_71 | spl19_72 | ~spl19_75),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f946])).
% 0.75/0.50 thf(f948,plain,(
% 0.75/0.50 ($false = ((f0 @ $true))) | (~spl19_67 | ~spl19_72)),
% 0.75/0.50 inference(forward_demodulation,[],[f409,f387])).
% 0.75/0.50 thf(f954,plain,(
% 0.75/0.50 ($false = ((f0 @ $false))) | (~spl19_73 | ~spl19_75)),
% 0.75/0.50 inference(forward_demodulation,[],[f423,f414])).
% 0.75/0.50 thf(f960,plain,(
% 0.75/0.50 ($true != ((f1 @ $true))) | (~spl19_59 | spl19_66)),
% 0.75/0.50 inference(forward_demodulation,[],[f381,f351])).
% 0.75/0.50 thf(f966,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_33 | ~spl19_38 | ~spl19_67 | ~spl19_72)),
% 0.75/0.50 inference(forward_demodulation,[],[f932,f948])).
% 0.75/0.50 thf(f967,plain,(
% 0.75/0.50 $false | (~spl19_33 | ~spl19_38 | ~spl19_67 | ~spl19_72)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f966])).
% 0.75/0.50 thf(f968,plain,(
% 0.75/0.50 ~spl19_33 | ~spl19_38 | ~spl19_67 | ~spl19_72),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f967])).
% 0.75/0.50 thf(f972,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_28 | ~spl19_59 | spl19_66)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f960,f849])).
% 0.75/0.50 thf(f973,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_28 | ~spl19_59 | spl19_66),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f972])).
% 0.75/0.50 thf(f981,plain,(
% 0.75/0.50 ($true != ((f0 @ $true))) | (~spl19_63 | spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f399,f369])).
% 0.75/0.50 thf(f987,plain,(
% 0.75/0.50 $false | (~spl19_33 | ~spl19_38 | ~spl19_63 | spl19_70)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f981,f932])).
% 0.75/0.50 thf(f988,plain,(
% 0.75/0.50 ~spl19_33 | ~spl19_38 | ~spl19_63 | spl19_70),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f987])).
% 0.75/0.50 thf(f991,plain,(
% 0.75/0.50 spl19_31 | spl19_29),
% 0.75/0.50 inference(avatar_split_clause,[],[f761,f213,f222])).
% 0.75/0.50 thf(f995,plain,(
% 0.75/0.50 ($false = ((f2 @ $true))) | (~spl19_55 | ~spl19_60)),
% 0.75/0.50 inference(forward_demodulation,[],[f355,f333])).
% 0.75/0.50 thf(f996,plain,(
% 0.75/0.50 ($true != ((f2 @ $true))) | (~spl19_55 | spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f363,f333])).
% 0.75/0.50 thf(f1000,plain,(
% 0.75/0.50 ($true = ((f0 @ $false))) | (~spl19_35 | ~spl19_38)),
% 0.75/0.50 inference(forward_demodulation,[],[f256,f242])).
% 0.75/0.50 thf(f1002,plain,(
% 0.75/0.50 $false | (~spl19_51 | ~spl19_55 | spl19_56 | ~spl19_60)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f995,f731])).
% 0.75/0.50 thf(f1003,plain,(
% 0.75/0.50 ~spl19_51 | ~spl19_55 | spl19_56 | ~spl19_60),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1002])).
% 0.75/0.50 thf(f1004,plain,(
% 0.75/0.50 $false | (~spl19_51 | ~spl19_55 | ~spl19_58 | spl19_62)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f996,f733])).
% 0.75/0.50 thf(f1005,plain,(
% 0.75/0.50 ~spl19_51 | ~spl19_55 | ~spl19_58 | spl19_62),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1004])).
% 0.75/0.50 thf(f1009,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_35 | ~spl19_38 | ~spl19_73 | ~spl19_75)),
% 0.75/0.50 inference(forward_demodulation,[],[f1000,f954])).
% 0.75/0.50 thf(f1010,plain,(
% 0.75/0.50 $false | (~spl19_35 | ~spl19_38 | ~spl19_73 | ~spl19_75)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1009])).
% 0.75/0.50 thf(f1011,plain,(
% 0.75/0.50 ~spl19_35 | ~spl19_38 | ~spl19_73 | ~spl19_75),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1010])).
% 0.75/0.50 thf(f1035,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_19 | ~spl19_24 | ~spl19_57 | ~spl19_60)),
% 0.75/0.50 inference(forward_demodulation,[],[f841,f584])).
% 0.75/0.50 thf(f1036,plain,(
% 0.75/0.50 $false | (~spl19_19 | ~spl19_24 | ~spl19_57 | ~spl19_60)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1035])).
% 0.75/0.50 thf(f1037,plain,(
% 0.75/0.50 ~spl19_19 | ~spl19_24 | ~spl19_57 | ~spl19_60),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1036])).
% 0.75/0.50 thf(f1041,plain,(
% 0.75/0.50 ($true != ((f2 @ $false))) | (~spl19_53 | spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f345,f324])).
% 0.75/0.50 thf(f1046,plain,(
% 0.75/0.50 ($false != ((f1 @ $false))) | (~spl19_23 | spl19_26)),
% 0.75/0.50 inference(forward_demodulation,[],[f200,f188])).
% 0.75/0.50 thf(f1052,plain,(
% 0.75/0.50 $false | (~spl19_23 | spl19_26 | ~spl19_31 | ~spl19_34)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1046,f523])).
% 0.75/0.50 thf(f1053,plain,(
% 0.75/0.50 ~spl19_23 | spl19_26 | ~spl19_31 | ~spl19_34),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1052])).
% 0.75/0.50 thf(f1054,plain,(
% 0.75/0.50 ($false != ((f1 @ $true))) | (~spl19_25 | spl19_30)),
% 0.75/0.50 inference(forward_demodulation,[],[f218,f197])).
% 0.75/0.50 thf(f1059,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_25 | ~spl19_29 | ~spl19_32 | ~spl19_34)),
% 0.75/0.50 inference(forward_demodulation,[],[f858,f885])).
% 0.75/0.50 thf(f1060,plain,(
% 0.75/0.50 $false | (~spl19_25 | ~spl19_29 | ~spl19_32 | ~spl19_34)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1059])).
% 0.75/0.50 thf(f1061,plain,(
% 0.75/0.50 ~spl19_25 | ~spl19_29 | ~spl19_32 | ~spl19_34),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1060])).
% 0.75/0.50 thf(f1062,plain,(
% 0.75/0.50 $false | (~spl19_25 | ~spl19_29 | spl19_30 | ~spl19_34)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1054,f885])).
% 0.75/0.50 thf(f1063,plain,(
% 0.75/0.50 ~spl19_25 | ~spl19_29 | spl19_30 | ~spl19_34),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1062])).
% 0.75/0.50 thf(f1072,plain,(
% 0.75/0.50 ($true = ((f2 @ $true))) | (~spl19_17 | ~spl19_24)),
% 0.75/0.50 inference(forward_demodulation,[],[f192,f161])).
% 0.75/0.50 thf(f1076,plain,(
% 0.75/0.50 ($false = ((f4 @ $true))) | (~spl19_39 | ~spl19_44)),
% 0.75/0.50 inference(forward_demodulation,[],[f283,f261])).
% 0.75/0.50 thf(f1078,plain,(
% 0.75/0.50 ($false = ((f2 @ $true))) | (~spl19_17 | ~spl19_22)),
% 0.75/0.50 inference(forward_demodulation,[],[f183,f161])).
% 0.75/0.50 thf(f1086,plain,(
% 0.75/0.50 spl19_78 | ~spl19_39 | ~spl19_44),
% 0.75/0.50 inference(avatar_split_clause,[],[f1076,f281,f259,f784])).
% 0.75/0.50 thf(f1088,plain,(
% 0.75/0.50 spl19_7 | spl19_5),
% 0.75/0.50 inference(avatar_split_clause,[],[f747,f105,f114])).
% 0.75/0.50 thf(f1089,plain,(
% 0.75/0.50 ($false = ((f4 @ $false))) | (~spl19_7 | ~spl19_40)),
% 0.75/0.50 inference(forward_demodulation,[],[f265,f116])).
% 0.75/0.50 thf(f1090,plain,(
% 0.75/0.50 ($false = ((f3 @ $false))) | (~spl19_7 | ~spl19_10)),
% 0.75/0.50 inference(forward_demodulation,[],[f129,f116])).
% 0.75/0.50 thf(f1091,plain,(
% 0.75/0.50 ($true = ((f4 @ $false))) | (~spl19_7 | ~spl19_42)),
% 0.75/0.50 inference(forward_demodulation,[],[f274,f116])).
% 0.75/0.50 thf(f1092,plain,(
% 0.75/0.50 ($true = ((f3 @ $false))) | (~spl19_7 | ~spl19_12)),
% 0.75/0.50 inference(forward_demodulation,[],[f138,f116])).
% 0.75/0.50 thf(f1094,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_40 | ~spl19_42)),
% 0.75/0.50 inference(forward_demodulation,[],[f1091,f1089])).
% 0.75/0.50 thf(f1095,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_40 | ~spl19_42)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1094])).
% 0.75/0.50 thf(f1096,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_40 | ~spl19_42),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1095])).
% 0.75/0.50 thf(f1107,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF4) | spl19_21),
% 0.75/0.50 inference(constrained_superposition,[],[f178,f6])).
% 0.75/0.50 thf(f1108,plain,(
% 0.75/0.50 ($false = sF4) | spl19_21),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1107])).
% 0.75/0.50 thf(f1111,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_25 | spl19_26 | ~spl19_30)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f847,f850])).
% 0.75/0.50 thf(f1112,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_25 | spl19_26 | ~spl19_30),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1111])).
% 0.75/0.50 thf(f1116,plain,(
% 0.75/0.50 spl19_23 | spl19_21),
% 0.75/0.50 inference(avatar_split_clause,[],[f1108,f177,f186])).
% 0.75/0.50 thf(f1128,plain,(
% 0.75/0.50 ($true != ((f0 @ $false))) | (~spl19_65 | spl19_70)),
% 0.75/0.50 inference(forward_demodulation,[],[f399,f378])).
% 0.75/0.50 thf(f1137,plain,(
% 0.75/0.50 $false | (~spl19_53 | ~spl19_57 | spl19_58 | ~spl19_62)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1041,f642])).
% 0.75/0.50 thf(f1138,plain,(
% 0.75/0.50 ~spl19_53 | ~spl19_57 | spl19_58 | ~spl19_62),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1137])).
% 0.75/0.50 thf(f1142,plain,(
% 0.75/0.50 $false | (~spl19_65 | ~spl19_69 | spl19_70 | ~spl19_74)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1128,f643])).
% 0.75/0.50 thf(f1143,plain,(
% 0.75/0.50 ~spl19_65 | ~spl19_69 | spl19_70 | ~spl19_74),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1142])).
% 0.75/0.50 thf(f1162,plain,(
% 0.75/0.50 ($true != ((f2 @ $true))) | (~spl19_51 | spl19_58)),
% 0.75/0.50 inference(forward_demodulation,[],[f345,f315])).
% 0.75/0.50 thf(f1168,plain,(
% 0.75/0.50 $false | (~spl19_17 | ~spl19_24 | ~spl19_51 | spl19_58)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1162,f1072])).
% 0.75/0.50 thf(f1169,plain,(
% 0.75/0.50 ~spl19_17 | ~spl19_24 | ~spl19_51 | spl19_58),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1168])).
% 0.75/0.50 thf(f1184,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF9) | spl19_39),
% 0.75/0.50 inference(constrained_superposition,[],[f260,f6])).
% 0.75/0.50 thf(f1185,plain,(
% 0.75/0.50 ($false = sF9) | spl19_39),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1184])).
% 0.75/0.50 thf(f1194,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF13) | spl19_55),
% 0.75/0.50 inference(constrained_superposition,[],[f332,f6])).
% 0.75/0.50 thf(f1195,plain,(
% 0.75/0.50 ($false = sF13) | spl19_55),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1194])).
% 0.75/0.50 thf(f1204,plain,(
% 0.75/0.50 ($true != $true) | ($false = sF16) | spl19_67),
% 0.75/0.50 inference(constrained_superposition,[],[f386,f6])).
% 0.75/0.50 thf(f1205,plain,(
% 0.75/0.50 ($false = sF16) | spl19_67),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1204])).
% 0.75/0.50 thf(f1216,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_6 | ~spl19_8)),
% 0.75/0.50 inference(constrained_superposition,[],[f111,f120])).
% 0.75/0.50 thf(f1220,plain,(
% 0.75/0.50 $false | (~spl19_6 | ~spl19_8)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1216])).
% 0.75/0.50 thf(f1221,plain,(
% 0.75/0.50 ~spl19_6 | ~spl19_8),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1220])).
% 0.75/0.50 thf(f1225,plain,(
% 0.75/0.50 ($false = ((f4 @ $false))) | (~spl19_6 | ~spl19_77)),
% 0.75/0.50 inference(constrained_superposition,[],[f111,f782])).
% 0.75/0.50 thf(f1260,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_10 | ~spl19_15 | ~spl19_20)),
% 0.75/0.50 inference(constrained_superposition,[],[f873,f1090])).
% 0.75/0.50 thf(f1264,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_10 | ~spl19_15 | ~spl19_20)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1260])).
% 0.75/0.50 thf(f1265,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_10 | ~spl19_15 | ~spl19_20),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1264])).
% 0.75/0.50 thf(f1272,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_10 | ~spl19_12)),
% 0.75/0.50 inference(forward_demodulation,[],[f1092,f1090])).
% 0.75/0.50 thf(f1273,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_10 | ~spl19_12)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1272])).
% 0.75/0.50 thf(f1274,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_10 | ~spl19_12),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1273])).
% 0.75/0.50 thf(f1278,plain,(
% 0.75/0.50 ($false != ((f3 @ $false))) | (~spl19_7 | spl19_10)),
% 0.75/0.50 inference(forward_demodulation,[],[f128,f116])).
% 0.75/0.50 thf(f1282,plain,(
% 0.75/0.50 $false | (~spl19_7 | spl19_10 | ~spl19_45 | ~spl19_48)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1278,f554])).
% 0.75/0.50 thf(f1283,plain,(
% 0.75/0.50 ~spl19_7 | spl19_10 | ~spl19_45 | ~spl19_48),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1282])).
% 0.75/0.50 thf(f1285,plain,(
% 0.75/0.50 ($false != ((f4 @ $false))) | (~spl19_7 | spl19_40)),
% 0.75/0.50 inference(forward_demodulation,[],[f264,f116])).
% 0.75/0.50 thf(f1294,plain,(
% 0.75/0.50 $false | (~spl19_6 | ~spl19_7 | spl19_40 | ~spl19_77)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1285,f1225])).
% 0.75/0.50 thf(f1295,plain,(
% 0.75/0.50 ~spl19_6 | ~spl19_7 | spl19_40 | ~spl19_77),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1294])).
% 0.75/0.50 thf(f1296,plain,(
% 0.75/0.50 spl19_41 | spl19_39),
% 0.75/0.50 inference(avatar_split_clause,[],[f1185,f259,f268])).
% 0.75/0.50 thf(f1308,plain,(
% 0.75/0.50 ($true = ((f4 @ $false))) | (~spl19_41 | ~spl19_46)),
% 0.75/0.50 inference(forward_demodulation,[],[f292,f270])).
% 0.75/0.50 thf(f1324,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_40 | ~spl19_41 | ~spl19_46)),
% 0.75/0.50 inference(forward_demodulation,[],[f1308,f1089])).
% 0.75/0.50 thf(f1325,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_40 | ~spl19_41 | ~spl19_46)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1324])).
% 0.75/0.50 thf(f1326,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_40 | ~spl19_41 | ~spl19_46),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1325])).
% 0.75/0.50 thf(f1336,plain,(
% 0.75/0.50 ($true = ((f4 @ $true))) | (~spl19_39 | ~spl19_46)),
% 0.75/0.50 inference(forward_demodulation,[],[f292,f261])).
% 0.75/0.50 thf(f1339,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_39 | ~spl19_46 | ~spl19_78)),
% 0.75/0.50 inference(forward_demodulation,[],[f1336,f786])).
% 0.75/0.50 thf(f1340,plain,(
% 0.75/0.50 $false | (~spl19_39 | ~spl19_46 | ~spl19_78)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1339])).
% 0.75/0.50 thf(f1341,plain,(
% 0.75/0.50 ~spl19_39 | ~spl19_46 | ~spl19_78),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1340])).
% 0.75/0.50 thf(f1354,plain,(
% 0.75/0.50 ($true = ((f2 @ $true))) | (~spl19_47 | ~spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f328,f297])).
% 0.75/0.50 thf(f1359,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_17 | ~spl19_22 | ~spl19_47 | ~spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f1354,f1078])).
% 0.75/0.50 thf(f1360,plain,(
% 0.75/0.50 $false | (~spl19_17 | ~spl19_22 | ~spl19_47 | ~spl19_54)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1359])).
% 0.75/0.50 thf(f1361,plain,(
% 0.75/0.50 ~spl19_17 | ~spl19_22 | ~spl19_47 | ~spl19_54),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1360])).
% 0.75/0.50 thf(f1362,plain,(
% 0.75/0.50 ($false = ((f2 @ $true))) | (~spl19_47 | ~spl19_52)),
% 0.75/0.50 inference(forward_demodulation,[],[f319,f297])).
% 0.75/0.50 thf(f1373,plain,(
% 0.75/0.50 ($true = ((f2 @ $true))) | (~spl19_55 | ~spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f364,f333])).
% 0.75/0.50 thf(f1378,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_17 | ~spl19_22 | ~spl19_55 | ~spl19_62)),
% 0.75/0.50 inference(forward_demodulation,[],[f1373,f1078])).
% 0.75/0.50 thf(f1379,plain,(
% 0.75/0.50 $false | (~spl19_17 | ~spl19_22 | ~spl19_55 | ~spl19_62)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1378])).
% 0.75/0.50 thf(f1380,plain,(
% 0.75/0.50 ~spl19_17 | ~spl19_22 | ~spl19_55 | ~spl19_62),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1379])).
% 0.75/0.50 thf(f1382,plain,(
% 0.75/0.50 ($false != ((f2 @ $true))) | (~spl19_17 | spl19_22)),
% 0.75/0.50 inference(forward_demodulation,[],[f182,f161])).
% 0.75/0.50 thf(f1405,plain,(
% 0.75/0.50 ($true = ((f1 @ $true))) | (~spl19_29 | ~spl19_36)),
% 0.75/0.50 inference(forward_demodulation,[],[f246,f215])).
% 0.75/0.50 thf(f1413,plain,(
% 0.75/0.50 $false | (~spl19_17 | spl19_22 | ~spl19_47 | ~spl19_52)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1382,f1362])).
% 0.75/0.50 thf(f1414,plain,(
% 0.75/0.50 ~spl19_17 | spl19_22 | ~spl19_47 | ~spl19_52),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1413])).
% 0.75/0.50 thf(f1420,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_21 | ~spl19_26 | ~spl19_29 | ~spl19_36)),
% 0.75/0.50 inference(forward_demodulation,[],[f1405,f842])).
% 0.75/0.50 thf(f1421,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_26 | ~spl19_29 | ~spl19_36)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1420])).
% 0.75/0.50 thf(f1422,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_26 | ~spl19_29 | ~spl19_36),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1421])).
% 0.75/0.50 thf(f1436,plain,(
% 0.75/0.50 ($false != ((f1 @ $false))) | (~spl19_31 | spl19_34)),
% 0.75/0.50 inference(forward_demodulation,[],[f236,f224])).
% 0.75/0.50 thf(f1440,plain,(
% 0.75/0.50 $false | (~spl19_27 | ~spl19_30 | ~spl19_31 | spl19_34)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1436,f513])).
% 0.75/0.50 thf(f1441,plain,(
% 0.75/0.50 ~spl19_27 | ~spl19_30 | ~spl19_31 | spl19_34),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1440])).
% 0.75/0.50 thf(f1451,plain,(
% 0.75/0.50 ($true = ((f1 @ $false))) | (~spl19_23 | ~spl19_28)),
% 0.75/0.50 inference(forward_demodulation,[],[f210,f188])).
% 0.75/0.50 thf(f1471,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_23 | ~spl19_26 | ~spl19_28)),
% 0.75/0.50 inference(forward_demodulation,[],[f1451,f503])).
% 0.75/0.50 thf(f1472,plain,(
% 0.75/0.50 $false | (~spl19_23 | ~spl19_26 | ~spl19_28)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1471])).
% 0.75/0.50 thf(f1473,plain,(
% 0.75/0.50 ~spl19_23 | ~spl19_26 | ~spl19_28),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1472])).
% 0.75/0.50 thf(f1497,plain,(
% 0.75/0.50 spl19_49 | spl19_47),
% 0.75/0.50 inference(avatar_split_clause,[],[f863,f295,f304])).
% 0.75/0.50 thf(f1502,plain,(
% 0.75/0.50 spl19_57 | spl19_55),
% 0.75/0.50 inference(avatar_split_clause,[],[f1195,f331,f340])).
% 0.75/0.50 thf(f1515,plain,(
% 0.75/0.50 ($true = ((f1 @ $true))) | (~spl19_21 | ~spl19_28)),
% 0.75/0.50 inference(forward_demodulation,[],[f210,f179])).
% 0.75/0.50 thf(f1522,plain,(
% 0.75/0.50 ($false != ((f3 @ $true))) | (~spl19_5 | spl19_10)),
% 0.75/0.50 inference(forward_demodulation,[],[f128,f107])).
% 0.75/0.50 thf(f1523,plain,(
% 0.75/0.50 ($true = ((f4 @ $true))) | (~spl19_5 | ~spl19_42)),
% 0.75/0.50 inference(forward_demodulation,[],[f274,f107])).
% 0.75/0.50 thf(f1531,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_21 | ~spl19_26 | ~spl19_28)),
% 0.75/0.50 inference(forward_demodulation,[],[f1515,f842])).
% 0.75/0.50 thf(f1532,plain,(
% 0.75/0.50 $false | (~spl19_21 | ~spl19_26 | ~spl19_28)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1531])).
% 0.75/0.50 thf(f1533,plain,(
% 0.75/0.50 ~spl19_21 | ~spl19_26 | ~spl19_28),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1532])).
% 0.75/0.50 thf(f1537,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_9 | spl19_10 | ~spl19_14)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1522,f473])).
% 0.75/0.50 thf(f1538,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_9 | spl19_10 | ~spl19_14),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1537])).
% 0.75/0.50 thf(f1539,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_5 | ~spl19_42 | ~spl19_78)),
% 0.75/0.50 inference(forward_demodulation,[],[f1523,f786])).
% 0.75/0.50 thf(f1540,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_42 | ~spl19_78)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1539])).
% 0.75/0.50 thf(f1541,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_42 | ~spl19_78),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1540])).
% 0.75/0.50 thf(f1554,plain,(
% 0.75/0.50 spl19_69 | spl19_67),
% 0.75/0.50 inference(avatar_split_clause,[],[f1205,f385,f394])).
% 0.75/0.50 thf(f1623,plain,(
% 0.75/0.50 ($false != ((f4 @ $true))) | (x = $false) | spl19_6),
% 0.75/0.50 inference(constrained_superposition,[],[f110,f6])).
% 0.75/0.50 thf(f1625,plain,(
% 0.75/0.50 (x = $false) | (spl19_6 | ~spl19_78)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1623,f786])).
% 0.75/0.50 thf(f1626,plain,(
% 0.75/0.50 $false | (spl19_6 | spl19_77 | ~spl19_78)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1625,f781])).
% 0.75/0.50 thf(f1627,plain,(
% 0.75/0.50 spl19_6 | spl19_77 | ~spl19_78),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1626])).
% 0.75/0.50 thf(f1629,plain,(
% 0.75/0.50 ($false != ((f4 @ $false))) | (spl19_6 | ~spl19_77)),
% 0.75/0.50 inference(constrained_superposition,[],[f110,f782])).
% 0.75/0.50 thf(f1631,plain,(
% 0.75/0.50 $false | (spl19_6 | ~spl19_41 | ~spl19_44 | ~spl19_77)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1629,f544])).
% 0.75/0.50 thf(f1632,plain,(
% 0.75/0.50 spl19_6 | ~spl19_41 | ~spl19_44 | ~spl19_77),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1631])).
% 0.75/0.50 thf(f1656,plain,(
% 0.75/0.50 ($false != ((f3 @ $true))) | ($false = sF2) | spl19_18),
% 0.75/0.50 inference(constrained_superposition,[],[f164,f6])).
% 0.75/0.50 thf(f1657,plain,(
% 0.75/0.50 ($false != ((f3 @ $true))) | (~spl19_13 | spl19_18)),
% 0.75/0.50 inference(constrained_superposition,[],[f164,f143])).
% 0.75/0.50 thf(f1659,plain,(
% 0.75/0.50 $false | (~spl19_5 | ~spl19_10 | ~spl19_13 | spl19_18)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1657,f723])).
% 0.75/0.50 thf(f1660,plain,(
% 0.75/0.50 ~spl19_5 | ~spl19_10 | ~spl19_13 | spl19_18),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1659])).
% 0.75/0.50 thf(f1661,plain,(
% 0.75/0.50 ($false = sF2) | (~spl19_5 | ~spl19_10 | spl19_18)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1656,f723])).
% 0.75/0.50 thf(f1662,plain,(
% 0.75/0.50 spl19_15 | ~spl19_5 | ~spl19_10 | spl19_18),
% 0.75/0.50 inference(avatar_split_clause,[],[f1661,f163,f127,f105,f150])).
% 0.75/0.50 thf(f1698,plain,(
% 0.75/0.50 ($false != ((f1 @ $false))) | (~spl19_23 | spl19_26)),
% 0.75/0.50 inference(forward_demodulation,[],[f200,f188])).
% 0.75/0.50 thf(f1710,plain,(
% 0.75/0.50 $false | (~spl19_23 | spl19_26 | ~spl19_61 | ~spl19_64)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1698,f594])).
% 0.75/0.50 thf(f1711,plain,(
% 0.75/0.50 ~spl19_23 | spl19_26 | ~spl19_61 | ~spl19_64),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1710])).
% 0.75/0.50 thf(f1719,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(forward_demodulation,[],[f813,f1090])).
% 0.75/0.50 thf(f1720,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1719])).
% 0.75/0.50 thf(f1721,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1720])).
% 0.75/0.50 thf(f1726,plain,(
% 0.75/0.50 ($true = ((f2 @ $true))) | (~spl19_17 | ~spl19_24)),
% 0.75/0.50 inference(forward_demodulation,[],[f192,f161])).
% 0.75/0.50 thf(f1752,plain,(
% 0.75/0.50 ($true != ((f2 @ $false))) | (~spl19_49 | spl19_54)),
% 0.75/0.50 inference(forward_demodulation,[],[f327,f306])).
% 0.75/0.50 thf(f1755,plain,(
% 0.75/0.50 ($false != ((f3 @ $false))) | (~spl19_11 | spl19_14)),
% 0.75/0.50 inference(forward_demodulation,[],[f146,f134])).
% 0.75/0.50 thf(f1756,plain,(
% 0.75/0.50 ($true = ((f3 @ $false))) | (~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(forward_demodulation,[],[f156,f134])).
% 0.75/0.50 thf(f1761,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_17 | ~spl19_22 | ~spl19_24)),
% 0.75/0.50 inference(forward_demodulation,[],[f1726,f1078])).
% 0.75/0.50 thf(f1762,plain,(
% 0.75/0.50 $false | (~spl19_17 | ~spl19_22 | ~spl19_24)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1761])).
% 0.75/0.50 thf(f1763,plain,(
% 0.75/0.50 ~spl19_17 | ~spl19_22 | ~spl19_24),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1762])).
% 0.75/0.50 thf(f1769,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_10 | ~spl19_11 | spl19_14)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1755,f1090])).
% 0.75/0.50 thf(f1770,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_10 | ~spl19_11 | spl19_14),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1769])).
% 0.75/0.50 thf(f1771,plain,(
% 0.75/0.50 ($true = $false) | (~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(forward_demodulation,[],[f1756,f1090])).
% 0.75/0.50 thf(f1772,plain,(
% 0.75/0.50 $false | (~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16)),
% 0.75/0.50 inference(trivial_inequality_removal,[],[f1771])).
% 0.75/0.50 thf(f1773,plain,(
% 0.75/0.50 ~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1772])).
% 0.75/0.50 thf(f1775,plain,(
% 0.75/0.50 spl19_15 | spl19_13),
% 0.75/0.50 inference(avatar_split_clause,[],[f831,f141,f150])).
% 0.75/0.50 thf(f1779,plain,(
% 0.75/0.50 spl19_19 | spl19_17),
% 0.75/0.50 inference(avatar_split_clause,[],[f836,f159,f168])).
% 0.75/0.50 thf(f1800,plain,(
% 0.75/0.50 $false | (~spl19_19 | ~spl19_24 | ~spl19_49 | spl19_54)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1752,f841])).
% 0.75/0.50 thf(f1801,plain,(
% 0.75/0.50 ~spl19_19 | ~spl19_24 | ~spl19_49 | spl19_54),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1800])).
% 0.75/0.50 thf(f1823,plain,(
% 0.75/0.50 ($true != ((f3 @ $true))) | (~spl19_13 | spl19_20)),
% 0.75/0.50 inference(forward_demodulation,[],[f173,f143])).
% 0.75/0.50 thf(f1827,plain,(
% 0.75/0.50 $false | (~spl19_9 | ~spl19_13 | ~spl19_16 | spl19_20)),
% 0.75/0.50 inference(forward_subsumption_resolution,[],[f1823,f795])).
% 0.75/0.50 thf(f1828,plain,(
% 0.75/0.50 ~spl19_9 | ~spl19_13 | ~spl19_16 | spl19_20),
% 0.75/0.50 inference(avatar_contradiction_clause,[],[f1827])).
% 0.75/0.50 cnf(s1, plain, spl19_1 | spl19_2, inference(sat_conversion,[],[f94])).
% 0.75/0.50 cnf(s2, plain, spl19_3 | spl19_4, inference(sat_conversion,[],[f103])).
% 0.75/0.50 cnf(s3, plain, spl19_5 | spl19_6, inference(sat_conversion,[],[f112])).
% 0.75/0.50 cnf(s4, plain, spl19_7 | spl19_8, inference(sat_conversion,[],[f121])).
% 0.75/0.50 cnf(s5, plain, spl19_9 | spl19_10, inference(sat_conversion,[],[f130])).
% 0.75/0.50 cnf(s6, plain, spl19_11 | spl19_12, inference(sat_conversion,[],[f139])).
% 0.75/0.50 cnf(s7, plain, spl19_13 | spl19_14, inference(sat_conversion,[],[f148])).
% 0.75/0.50 cnf(s8, plain, spl19_15 | spl19_16, inference(sat_conversion,[],[f157])).
% 0.75/0.50 cnf(s9, plain, spl19_17 | spl19_18, inference(sat_conversion,[],[f166])).
% 0.75/0.50 cnf(s10, plain, spl19_19 | spl19_20, inference(sat_conversion,[],[f175])).
% 0.75/0.50 cnf(s11, plain, spl19_21 | spl19_22, inference(sat_conversion,[],[f184])).
% 0.75/0.50 cnf(s12, plain, spl19_23 | spl19_24, inference(sat_conversion,[],[f193])).
% 0.75/0.50 cnf(s13, plain, spl19_25 | spl19_26, inference(sat_conversion,[],[f202])).
% 0.75/0.50 cnf(s14, plain, spl19_27 | spl19_28, inference(sat_conversion,[],[f211])).
% 0.75/0.50 cnf(s15, plain, spl19_29 | spl19_30, inference(sat_conversion,[],[f220])).
% 0.75/0.50 cnf(s16, plain, spl19_31 | spl19_32, inference(sat_conversion,[],[f229])).
% 0.75/0.50 cnf(s17, plain, spl19_33 | spl19_34, inference(sat_conversion,[],[f238])).
% 0.75/0.50 cnf(s18, plain, spl19_35 | spl19_36, inference(sat_conversion,[],[f247])).
% 0.75/0.50 cnf(s19, plain, spl19_4 | spl19_37, inference(sat_conversion,[],[f252])).
% 0.75/0.50 cnf(s20, plain, spl19_2 | spl19_38, inference(sat_conversion,[],[f257])).
% 0.75/0.50 cnf(s21, plain, spl19_39 | spl19_40, inference(sat_conversion,[],[f266])).
% 0.75/0.50 cnf(s22, plain, spl19_41 | spl19_42, inference(sat_conversion,[],[f275])).
% 0.75/0.50 cnf(s23, plain, spl19_43 | spl19_44, inference(sat_conversion,[],[f284])).
% 0.75/0.50 cnf(s24, plain, spl19_45 | spl19_46, inference(sat_conversion,[],[f293])).
% 0.75/0.50 cnf(s25, plain, spl19_47 | spl19_48, inference(sat_conversion,[],[f302])).
% 0.75/0.50 cnf(s26, plain, spl19_49 | spl19_50, inference(sat_conversion,[],[f311])).
% 0.75/0.50 cnf(s27, plain, spl19_51 | spl19_52, inference(sat_conversion,[],[f320])).
% 0.75/0.50 cnf(s28, plain, spl19_53 | spl19_54, inference(sat_conversion,[],[f329])).
% 0.75/0.50 cnf(s29, plain, spl19_55 | spl19_56, inference(sat_conversion,[],[f338])).
% 0.75/0.50 cnf(s30, plain, spl19_57 | spl19_58, inference(sat_conversion,[],[f347])).
% 0.75/0.50 cnf(s31, plain, spl19_59 | spl19_60, inference(sat_conversion,[],[f356])).
% 0.75/0.50 cnf(s32, plain, spl19_61 | spl19_62, inference(sat_conversion,[],[f365])).
% 0.75/0.50 cnf(s33, plain, spl19_63 | spl19_64, inference(sat_conversion,[],[f374])).
% 0.75/0.50 cnf(s34, plain, spl19_65 | spl19_66, inference(sat_conversion,[],[f383])).
% 0.75/0.50 cnf(s35, plain, spl19_67 | spl19_68, inference(sat_conversion,[],[f392])).
% 0.75/0.50 cnf(s36, plain, spl19_69 | spl19_70, inference(sat_conversion,[],[f401])).
% 0.75/0.50 cnf(s37, plain, spl19_71 | spl19_72, inference(sat_conversion,[],[f410])).
% 0.75/0.50 cnf(s38, plain, spl19_73 | spl19_74, inference(sat_conversion,[],[f419])).
% 0.75/0.50 cnf(s39, plain, spl19_3 | spl19_75, inference(sat_conversion,[],[f424])).
% 0.75/0.50 cnf(s40, plain, spl19_1 | spl19_76, inference(sat_conversion,[],[f429])).
% 0.75/0.50 cnf(s41, plain, ~spl19_2 | ~spl19_4, inference(sat_conversion,[],[f432])).
% 0.75/0.50 cnf(s43, plain, ~spl19_5 | ~spl19_7, inference(sat_conversion,[],[f451])).
% 0.75/0.50 cnf(s45, plain, ~spl19_9 | ~spl19_11, inference(sat_conversion,[],[f460])).
% 0.75/0.50 cnf(s49, plain, ~spl19_17 | ~spl19_19, inference(sat_conversion,[],[f480])).
% 0.75/0.50 cnf(s51, plain, ~spl19_21 | ~spl19_23, inference(sat_conversion,[],[f490])).
% 0.75/0.50 cnf(s53, plain, ~spl19_25 | ~spl19_27, inference(sat_conversion,[],[f500])).
% 0.75/0.50 cnf(s59, plain, ~spl19_39 | ~spl19_41, inference(sat_conversion,[],[f531])).
% 0.75/0.50 cnf(s63, plain, ~spl19_47 | ~spl19_49, inference(sat_conversion,[],[f551])).
% 0.75/0.50 cnf(s76, plain, ~spl19_35 | ~spl19_37 | ~spl19_73 | ~spl19_76, inference(sat_conversion,[],[f618])).
% 0.75/0.50 cnf(s78, plain, ~spl19_23 | ~spl19_26 | ~spl19_31 | ~spl19_36, inference(sat_conversion,[],[f625])).
% 0.75/0.50 cnf(s79, plain, ~spl19_69 | ~spl19_72 | ~spl19_73 | ~spl19_76, inference(sat_conversion,[],[f630])).
% 0.75/0.50 cnf(s80, plain, ~spl19_34 | ~spl19_36, inference(sat_conversion,[],[f633])).
% 0.75/0.50 cnf(s81, plain, ~spl19_23 | ~spl19_26 | ~spl19_27 | ~spl19_32, inference(sat_conversion,[],[f636])).
% 0.75/0.50 cnf(s82, plain, ~spl19_23 | ~spl19_26 | ~spl19_61 | ~spl19_66, inference(sat_conversion,[],[f639])).
% 0.75/0.50 cnf(s83, plain, ~spl19_64 | ~spl19_66, inference(sat_conversion,[],[f646])).
% 0.75/0.50 cnf(s84, plain, ~spl19_19 | ~spl19_22 | ~spl19_57 | ~spl19_62, inference(sat_conversion,[],[f650])).
% 0.75/0.50 cnf(s86, plain, ~spl19_68 | ~spl19_70, inference(sat_conversion,[],[f657])).
% 0.75/0.50 cnf(s87, plain, ~spl19_72 | ~spl19_74, inference(sat_conversion,[],[f660])).
% 0.75/0.50 cnf(s88, plain, ~spl19_60 | ~spl19_62, inference(sat_conversion,[],[f663])).
% 0.75/0.50 cnf(s89, plain, ~spl19_19 | ~spl19_22 | ~spl19_53 | ~spl19_58, inference(sat_conversion,[],[f666])).
% 0.75/0.50 cnf(s90, plain, ~spl19_56 | ~spl19_58, inference(sat_conversion,[],[f674])).
% 0.75/0.50 cnf(s91, plain, ~spl19_19 | ~spl19_22 | ~spl19_49 | ~spl19_54, inference(sat_conversion,[],[f677])).
% 0.75/0.50 cnf(s92, plain, ~spl19_52 | ~spl19_54, inference(sat_conversion,[],[f683])).
% 0.75/0.50 cnf(s93, plain, ~spl19_15 | ~spl19_18 | ~spl19_45 | ~spl19_50, inference(sat_conversion,[],[f686])).
% 0.75/0.50 cnf(s94, plain, ~spl19_48 | ~spl19_50, inference(sat_conversion,[],[f690])).
% 0.75/0.50 cnf(s97, plain, ~spl19_5 | ~spl19_12 | ~spl19_43 | spl19_50, inference(sat_conversion,[],[f713])).
% 0.75/0.50 cnf(s99, plain, ~spl19_35 | ~spl19_37 | ~spl19_65 | ~spl19_70, inference(sat_conversion,[],[f722])).
% 0.75/0.50 cnf(s100, plain, ~spl19_5 | ~spl19_10 | ~spl19_43 | spl19_48, inference(sat_conversion,[],[f744])).
% 0.75/0.50 cnf(s103, plain, ~spl19_6 | spl19_77 | spl19_78, inference(sat_conversion,[],[f787])).
% 0.75/0.50 cnf(s104, plain, ~spl19_5 | ~spl19_40 | spl19_78, inference(sat_conversion,[],[f788])).
% 0.75/0.50 cnf(s105, plain, ~spl19_13 | ~spl19_18 | ~spl19_43 | spl19_48, inference(sat_conversion,[],[f798])).
% 0.75/0.50 cnf(s106, plain, spl19_9 | spl19_11, inference(sat_conversion,[],[f799])).
% 0.75/0.50 cnf(s110, plain, ~spl19_21 | ~spl19_26 | ~spl19_59 | spl19_64, inference(sat_conversion,[],[f846])).
% 0.75/0.50 cnf(s114, plain, ~spl19_18 | ~spl19_20, inference(sat_conversion,[],[f879])).
% 0.75/0.50 cnf(s115, plain, ~spl19_11 | ~spl19_14 | ~spl19_15 | ~spl19_20, inference(sat_conversion,[],[f882])).
% 0.75/0.50 cnf(s119, plain, ~spl19_33 | ~spl19_37 | ~spl19_71 | ~spl19_76, inference(sat_conversion,[],[f912])).
% 0.75/0.50 cnf(s125, plain, ~spl19_33 | ~spl19_37 | ~spl19_63 | ~spl19_70, inference(sat_conversion,[],[f929])).
% 0.75/0.50 cnf(s128, plain, ~spl19_1 | ~spl19_3, inference(sat_conversion,[],[f942])).
% 0.75/0.50 cnf(s129, plain, ~spl19_67 | ~spl19_71 | spl19_72 | ~spl19_75, inference(sat_conversion,[],[f947])).
% 0.75/0.50 cnf(s132, plain, ~spl19_33 | ~spl19_38 | ~spl19_67 | ~spl19_72, inference(sat_conversion,[],[f968])).
% 0.75/0.50 cnf(s134, plain, ~spl19_21 | ~spl19_28 | ~spl19_59 | spl19_66, inference(sat_conversion,[],[f973])).
% 0.75/0.50 cnf(s136, plain, ~spl19_33 | ~spl19_38 | ~spl19_63 | spl19_70, inference(sat_conversion,[],[f988])).
% 0.75/0.50 cnf(s137, plain, spl19_29 | spl19_31, inference(sat_conversion,[],[f991])).
% 0.75/0.50 cnf(s139, plain, ~spl19_51 | ~spl19_55 | spl19_56 | ~spl19_60, inference(sat_conversion,[],[f1003])).
% 0.75/0.50 cnf(s140, plain, ~spl19_51 | ~spl19_55 | ~spl19_58 | spl19_62, inference(sat_conversion,[],[f1005])).
% 0.75/0.50 cnf(s142, plain, ~spl19_35 | ~spl19_38 | ~spl19_73 | ~spl19_75, inference(sat_conversion,[],[f1011])).
% 0.75/0.50 cnf(s146, plain, ~spl19_19 | ~spl19_24 | ~spl19_57 | ~spl19_60, inference(sat_conversion,[],[f1037])).
% 0.75/0.50 cnf(s148, plain, ~spl19_23 | spl19_26 | ~spl19_31 | ~spl19_34, inference(sat_conversion,[],[f1053])).
% 0.75/0.50 cnf(s150, plain, ~spl19_25 | ~spl19_29 | ~spl19_32 | ~spl19_34, inference(sat_conversion,[],[f1061])).
% 0.75/0.50 cnf(s151, plain, ~spl19_25 | ~spl19_29 | spl19_30 | ~spl19_34, inference(sat_conversion,[],[f1063])).
% 0.75/0.50 cnf(s155, plain, ~spl19_39 | ~spl19_44 | spl19_78, inference(sat_conversion,[],[f1086])).
% 0.75/0.50 cnf(s156, plain, spl19_5 | spl19_7, inference(sat_conversion,[],[f1088])).
% 0.75/0.50 cnf(s157, plain, ~spl19_7 | ~spl19_40 | ~spl19_42, inference(sat_conversion,[],[f1096])).
% 0.75/0.50 cnf(s159, plain, ~spl19_21 | ~spl19_25 | spl19_26 | ~spl19_30, inference(sat_conversion,[],[f1112])).
% 0.75/0.50 cnf(s161, plain, spl19_21 | spl19_23, inference(sat_conversion,[],[f1116])).
% 0.75/0.50 cnf(s166, plain, ~spl19_53 | ~spl19_57 | spl19_58 | ~spl19_62, inference(sat_conversion,[],[f1138])).
% 0.75/0.50 cnf(s168, plain, ~spl19_65 | ~spl19_69 | spl19_70 | ~spl19_74, inference(sat_conversion,[],[f1143])).
% 0.75/0.50 cnf(s170, plain, ~spl19_17 | ~spl19_24 | ~spl19_51 | spl19_58, inference(sat_conversion,[],[f1169])).
% 0.75/0.50 cnf(s172, plain, ~spl19_6 | ~spl19_8, inference(sat_conversion,[],[f1221])).
% 0.75/0.50 cnf(s174, plain, ~spl19_7 | ~spl19_10 | ~spl19_15 | ~spl19_20, inference(sat_conversion,[],[f1265])).
% 0.75/0.50 cnf(s177, plain, ~spl19_7 | ~spl19_10 | ~spl19_12, inference(sat_conversion,[],[f1274])).
% 0.75/0.50 cnf(s179, plain, ~spl19_7 | spl19_10 | ~spl19_45 | ~spl19_48, inference(sat_conversion,[],[f1283])).
% 0.75/0.50 cnf(s183, plain, ~spl19_6 | ~spl19_7 | spl19_40 | ~spl19_77, inference(sat_conversion,[],[f1295])).
% 0.75/0.50 cnf(s184, plain, spl19_39 | spl19_41, inference(sat_conversion,[],[f1296])).
% 0.75/0.50 cnf(s192, plain, ~spl19_7 | ~spl19_40 | ~spl19_41 | ~spl19_46, inference(sat_conversion,[],[f1326])).
% 0.75/0.50 cnf(s196, plain, ~spl19_39 | ~spl19_46 | ~spl19_78, inference(sat_conversion,[],[f1341])).
% 0.75/0.50 cnf(s201, plain, ~spl19_17 | ~spl19_22 | ~spl19_47 | ~spl19_54, inference(sat_conversion,[],[f1361])).
% 0.75/0.50 cnf(s205, plain, ~spl19_17 | ~spl19_22 | ~spl19_55 | ~spl19_62, inference(sat_conversion,[],[f1380])).
% 0.75/0.50 cnf(s210, plain, ~spl19_17 | spl19_22 | ~spl19_47 | ~spl19_52, inference(sat_conversion,[],[f1414])).
% 0.75/0.50 cnf(s212, plain, ~spl19_21 | ~spl19_26 | ~spl19_29 | ~spl19_36, inference(sat_conversion,[],[f1422])).
% 0.75/0.50 cnf(s216, plain, ~spl19_27 | ~spl19_30 | ~spl19_31 | spl19_34, inference(sat_conversion,[],[f1441])).
% 0.75/0.50 cnf(s221, plain, ~spl19_23 | ~spl19_26 | ~spl19_28, inference(sat_conversion,[],[f1473])).
% 0.75/0.50 cnf(s228, plain, spl19_47 | spl19_49, inference(sat_conversion,[],[f1497])).
% 0.75/0.50 cnf(s229, plain, spl19_55 | spl19_57, inference(sat_conversion,[],[f1502])).
% 0.75/0.50 cnf(s234, plain, ~spl19_21 | ~spl19_26 | ~spl19_28, inference(sat_conversion,[],[f1533])).
% 0.75/0.50 cnf(s236, plain, ~spl19_5 | ~spl19_9 | spl19_10 | ~spl19_14, inference(sat_conversion,[],[f1538])).
% 0.75/0.50 cnf(s237, plain, ~spl19_5 | ~spl19_42 | ~spl19_78, inference(sat_conversion,[],[f1541])).
% 0.75/0.50 cnf(s240, plain, spl19_67 | spl19_69, inference(sat_conversion,[],[f1554])).
% 0.75/0.50 cnf(s242, plain, spl19_6 | spl19_77 | ~spl19_78, inference(sat_conversion,[],[f1627])).
% 0.75/0.50 cnf(s243, plain, spl19_6 | ~spl19_41 | ~spl19_44 | ~spl19_77, inference(sat_conversion,[],[f1632])).
% 0.75/0.50 cnf(s246, plain, ~spl19_5 | ~spl19_10 | ~spl19_13 | spl19_18, inference(sat_conversion,[],[f1660])).
% 0.75/0.50 cnf(s247, plain, ~spl19_5 | ~spl19_10 | spl19_15 | spl19_18, inference(sat_conversion,[],[f1662])).
% 0.75/0.50 cnf(s255, plain, ~spl19_23 | spl19_26 | ~spl19_61 | ~spl19_64, inference(sat_conversion,[],[f1711])).
% 0.75/0.50 cnf(s261, plain, ~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16, inference(sat_conversion,[],[f1721])).
% 0.75/0.50 cnf(s268, plain, ~spl19_17 | ~spl19_22 | ~spl19_24, inference(sat_conversion,[],[f1763])).
% 0.75/0.50 cnf(s269, plain, ~spl19_7 | ~spl19_10 | ~spl19_11 | spl19_14, inference(sat_conversion,[],[f1770])).
% 0.75/0.50 cnf(s270, plain, ~spl19_7 | ~spl19_10 | ~spl19_11 | ~spl19_16, inference(sat_conversion,[],[f1773])).
% 0.75/0.50 cnf(s271, plain, spl19_13 | spl19_15, inference(sat_conversion,[],[f1775])).
% 0.75/0.50 cnf(s272, plain, spl19_17 | spl19_19, inference(sat_conversion,[],[f1779])).
% 0.75/0.50 cnf(s278, plain, ~spl19_19 | ~spl19_24 | ~spl19_49 | spl19_54, inference(sat_conversion,[],[f1801])).
% 0.75/0.50 cnf(s280, plain, ~spl19_9 | ~spl19_13 | ~spl19_16 | spl19_20, inference(sat_conversion,[],[f1828])).
% 0.75/0.50 cnf(s281, plain, ~spl19_65 | ~spl19_74 | ~spl19_35 | ~spl19_37, inference(rat,[],[s168,s36,s99])).
% 0.75/0.50 cnf(s282, plain, spl19_39 | ~spl19_46 | ~spl19_7, inference(rat,[],[s192,s21,s184])).
% 0.75/0.50 cnf(s283, plain, ~spl19_46 | spl19_5, inference(rat,[],[s183,s157,s103,s22,s196,s59,s282,s156,s3])).
% 0.75/0.50 cnf(s284, plain, ~spl19_26 | ~spl19_61 | ~spl19_23 | spl19_1, inference(rat,[],[s38,s281,s76,s18,s78,s16,s81,s34,s14,s82,s221,s40,s19,s41,s1])).
% 0.75/0.50 cnf(s285, plain, ~spl19_33 | ~spl19_63 | spl19_1, inference(rat,[],[s38,s79,s87,s37,s36,s119,s125,s40,s19,s41,s1])).
% 0.75/0.50 cnf(s286, plain, ~spl19_61 | ~spl19_23 | spl19_1, inference(rat,[],[s150,s16,s137,s148,s17,s285,s33,s13,s255,s284])).
% 0.75/0.50 cnf(s287, plain, ~spl19_23 | ~spl19_49 | ~spl19_19 | spl19_1, inference(rat,[],[s286,s32,s166,s30,s89,s28,s91,s11,s51])).
% 0.75/0.50 cnf(s288, plain, ~spl19_35 | ~spl19_65 | spl19_1, inference(rat,[],[s38,s281,s76,s40,s19,s41,s1])).
% 0.75/0.50 cnf(s289, plain, ~spl19_26 | ~spl19_59 | ~spl19_21 | spl19_1, inference(rat,[],[s216,s15,s137,s212,s80,s18,s288,s34,s83,s14,s110,s234])).
% 0.75/0.50 cnf(s290, plain, ~spl19_59 | ~spl19_21 | spl19_1, inference(rat,[],[s33,s285,s83,s17,s134,s151,s14,s15,s53,s159,s13,s289])).
% 0.75/0.50 cnf(s291, plain, ~spl19_49 | ~spl19_19 | spl19_1, inference(rat,[],[s140,s30,s229,s146,s88,s31,s290,s27,s92,s278,s12,s161,s287])).
% 0.75/0.50 cnf(s292, plain, spl19_9 | spl19_5 | spl19_1, inference(rat,[],[s291,s26,s93,s9,s49,s10,s115,s8,s269,s270,s5,s106,s156,s24,s283])).
% 0.75/0.50 cnf(s293, plain, ~spl19_18 | ~spl19_50 | ~spl19_9 | ~spl19_45, inference(rat,[],[s280,s8,s271,s93,s114])).
% 0.75/0.50 cnf(s294, plain, ~spl19_23 | spl19_5 | spl19_1, inference(rat,[],[s90,s166,s29,s229,s28,s205,s201,s32,s11,s286,s51,s9,s293,s26,s63,s25,s179,s177,s6,s45,s156,s292,s24,s283])).
% 0.75/0.50 cnf(s295, plain, spl19_5 | spl19_1, inference(rat,[],[s29,s140,s90,s170,s27,s88,s210,s31,s268,s290,s12,s161,s294,s9,s293,s26,s63,s25,s179,s177,s6,s45,s292,s24,s283,s156])).
% 0.75/0.50 cnf(s296, plain, ~spl19_43 | ~spl19_18 | spl19_48 | ~spl19_5, inference(rat,[],[s7,s236,s5,s105,s100])).
% 0.75/0.50 cnf(s297, plain, spl19_39 | ~spl19_44 | ~spl19_5, inference(rat,[],[s242,s104,s243,s21,s184,s172,s4,s43])).
% 0.75/0.50 cnf(s298, plain, ~spl19_44 | ~spl19_5, inference(rat,[],[s237,s22,s155,s59,s297])).
% 0.75/0.50 cnf(s299, plain, spl19_49 | ~spl19_62 | ~spl19_22 | ~spl19_5, inference(rat,[],[s90,s166,s29,s229,s28,s205,s201,s9,s296,s94,s26,s228,s23,s298])).
% 0.75/0.50 cnf(s300, plain, ~spl19_49 | spl19_1, inference(rat,[],[s7,s115,s246,s247,s5,s45,s6,s97,s114,s94,s10,s25,s291,s63,s23,s298,s295])).
% 0.75/0.50 cnf(s301, plain, ~spl19_23 | spl19_1, inference(rat,[],[s299,s32,s11,s286,s51,s295,s300])).
% 0.75/0.50 cnf(s302, plain, spl19_1, inference(rat,[],[s29,s140,s90,s170,s27,s88,s210,s31,s268,s290,s12,s161,s301,s9,s296,s94,s26,s228,s300,s23,s298,s295])).
% 0.75/0.50 cnf(s303, plain, ~spl19_3, inference(rat,[],[s128,s302])).
% 0.75/0.50 cnf(s304, plain, spl19_75, inference(rat,[],[s39,s303])).
% 0.75/0.50 cnf(s305, plain, spl19_4, inference(rat,[],[s2,s303])).
% 0.75/0.50 cnf(s306, plain, ~spl19_2, inference(rat,[],[s41,s305])).
% 0.75/0.50 cnf(s307, plain, spl19_38, inference(rat,[],[s20,s306])).
% 0.75/0.50 cnf(s308, plain, ~spl19_18 | ~spl19_50 | spl19_5, inference(rat,[],[s261,s5,s106,s8,s293,s93,s156,s24,s283])).
% 0.75/0.50 cnf(s309, plain, ~spl19_62 | ~spl19_53 | ~spl19_22 | ~spl19_17, inference(rat,[],[s90,s166,s29,s229,s205])).
% 0.75/0.50 cnf(s310, plain, spl19_9 | ~spl19_20 | ~spl19_7, inference(rat,[],[s8,s174,s270,s5,s106])).
% 0.75/0.50 cnf(s311, plain, ~spl19_26 | ~spl19_61 | ~spl19_23, inference(rat,[],[s86,s168,s35,s240,s129,s37,s87,s38,s142,s18,s78,s16,s81,s34,s14,s82,s221,s304,s307])).
% 0.75/0.50 cnf(s312, plain, ~spl19_67 | spl19_72, inference(rat,[],[s37,s129,s304])).
% 0.75/0.50 cnf(s313, plain, ~spl19_67 | ~spl19_33, inference(rat,[],[s312,s132,s307])).
% 0.75/0.50 cnf(s314, plain, ~spl19_33 | ~spl19_63, inference(rat,[],[s313,s35,s86,s136,s307])).
% 0.75/0.50 cnf(s315, plain, spl19_26 | ~spl19_61 | ~spl19_23, inference(rat,[],[s150,s16,s137,s148,s17,s314,s33,s13,s255])).
% 0.75/0.50 cnf(s316, plain, ~spl19_61 | ~spl19_23, inference(rat,[],[s315,s311])).
% 0.75/0.50 cnf(s317, plain, ~spl19_23 | ~spl19_17 | ~spl19_47, inference(rat,[],[s316,s32,s309,s28,s201,s11,s51])).
% 0.75/0.50 cnf(s318, plain, ~spl19_74 | ~spl19_65, inference(rat,[],[s86,s168,s35,s240,s312,s87])).
% 0.75/0.50 cnf(s319, plain, ~spl19_26 | ~spl19_59 | ~spl19_21, inference(rat,[],[s216,s15,s137,s212,s80,s18,s142,s38,s318,s34,s83,s14,s110,s234,s307,s304])).
% 0.75/0.50 cnf(s320, plain, ~spl19_59 | ~spl19_21, inference(rat,[],[s33,s314,s83,s17,s134,s151,s14,s15,s53,s159,s13,s319])).
% 0.75/0.50 cnf(s321, plain, ~spl19_17 | ~spl19_47, inference(rat,[],[s320,s31,s139,s29,s90,s170,s27,s210,s268,s12,s161,s317])).
% 0.75/0.50 cnf(s322, plain, spl19_49 | spl19_5, inference(rat,[],[s321,s9,s308,s26,s228])).
% 0.75/0.50 cnf(s323, plain, ~spl19_23 | spl19_5, inference(rat,[],[s89,s30,s28,s84,s91,s32,s11,s316,s51,s10,s310,s45,s6,s177,s179,s25,s63,s322,s24,s283,s156])).
% 0.75/0.50 cnf(s324, plain, spl19_5, inference(rat,[],[s140,s30,s229,s27,s146,s88,s92,s31,s278,s320,s12,s161,s323,s10,s310,s45,s6,s177,s179,s25,s63,s322,s24,s283,s156])).
% 0.75/0.50 cnf(s326, plain, ~spl19_44, inference(rat,[],[s298,s324])).
% 0.75/0.50 cnf(s328, plain, spl19_43, inference(rat,[],[s23,s326])).
% 0.75/0.50 cnf(s332, plain, ~spl19_19 | ~spl19_23, inference(rat,[],[s89,s30,s28,s84,s91,s299,s32,s316,s11,s51,s324])).
% 0.75/0.50 cnf(s333, plain, ~spl19_23, inference(rat,[],[s7,s115,s246,s247,s114,s10,s332,s5,s45,s6,s97,s94,s25,s63,s299,s32,s11,s316,s51,s324,s328])).
% 0.75/0.50 cnf(s334, plain, spl19_21, inference(rat,[],[s161,s333])).
% 0.75/0.50 cnf(s335, plain, spl19_24, inference(rat,[],[s12,s333])).
% 0.75/0.50 cnf(s336, plain, ~spl19_59, inference(rat,[],[s320,s334])).
% 0.75/0.50 cnf(s337, plain, spl19_60, inference(rat,[],[s31,s336])).
% 0.75/0.50 cnf(s338, plain, ~spl19_62, inference(rat,[],[s88,s337])).
% 0.75/0.50 cnf(s340, plain, spl19_17, inference(rat,[],[s92,s278,s27,s26,s140,s94,s30,s229,s296,s146,s9,s272,s335,s338,s328,s324,s337])).
% 0.75/0.50 cnf(s341, plain, ~spl19_19, inference(rat,[],[s49,s340])).
% 0.75/0.50 cnf(s342, plain, ~spl19_47, inference(rat,[],[s321,s340])).
% 0.75/0.50 cnf(s344, plain, spl19_20, inference(rat,[],[s10,s341])).
% 0.75/0.50 cnf(s346, plain, spl19_48, inference(rat,[],[s25,s342])).
% 0.75/0.50 cnf(s347, plain, ~spl19_18, inference(rat,[],[s114,s344])).
% 0.75/0.50 cnf(s348, plain, ~spl19_50, inference(rat,[],[s94,s346])).
% 0.75/0.50 cnf(s349, plain, ~spl19_12, inference(rat,[],[s97,s328,s324,s348])).
% 0.75/0.50 cnf(s350, plain, spl19_11, inference(rat,[],[s6,s349])).
% 0.75/0.50 cnf(s351, plain, ~spl19_9, inference(rat,[],[s45,s350])).
% 0.75/0.50 cnf(s352, plain, spl19_10, inference(rat,[],[s5,s351])).
% 0.75/0.50 cnf(s353, plain, spl19_15, inference(rat,[],[s247,s347,s324,s352])).
% 0.75/0.50 cnf(s354, plain, ~spl19_13, inference(rat,[],[s246,s347,s324,s352])).
% 0.75/0.50 cnf(s355, plain, ~spl19_14, inference(rat,[],[s115,s350,s344,s353])).
% 0.75/0.50 cnf(s356, plain, $false, inference(rat,[],[s7,s355,s354])).
% 0.75/0.50 thf(f1829,plain,(
% 0.75/0.50 $false),
% 0.75/0.50 inference(avatar_sat_refutation,[],[s356])).
% 0.75/0.50 % SZS output end Proof for theBenchmark
% 0.75/0.50 % (375163)------------------------------
% 0.75/0.50 % (375163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.50 % (375163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.50 % (375163)CaDiCaL version: 2.1.3
% 0.75/0.50 % (375163)Termination reason: Refutation
% 0.75/0.50 % (375163)Time elapsed: 0.038 s
% 0.75/0.50 % (375163)Peak memory usage: 13 MB
% 0.75/0.50 % (375163)Instructions burned: 68 (million)
% 0.75/0.50 % (375133)Success in time 0.239 s
% 0.75/0.50 % Vampire exiting
%------------------------------------------------------------------------------