%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO500^1.004 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:50:19 AM UTC 2026
% Result : Theorem 1.05s 0.44s
% Output : Refutation 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.004 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n008.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:11:39 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/0.44 % (3447925)Will run a generic schedule for satisfiability detection.
% 1.05/0.44 % (3447930)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2461463079_2999 on theBenchmark for (2999ds/0Mi)
% 1.05/0.44 % Exception at run slice level
% 1.05/0.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.05/0.44 % (3447933)dis+10_1_sil=32000:sp=arity:random_seed=4130672011:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.05/0.44 % (3447935)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2781114606:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.05/0.44 % (3447934)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2389977879:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.05/0.44 % (3447934)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.05/0.44 % (3447938)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=855834495:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.05/0.44 % Exception at run slice level
% 1.05/0.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.05/0.44 % (3447931)% WARNING: option uhcvi not known.
% 1.05/0.44 % (3447936)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4072884426:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.05/0.44 % (3447943)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1895756864:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.05/0.44 % (3447931)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1797015554:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.05/0.44 % (3447931)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.05/0.44 % (3447931)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.05/0.44 % (3447932)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2295320192:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.05/0.44 % (3447933)Instruction limit reached!
% 1.05/0.44 % (3447933)------------------------------
% 1.05/0.44 % (3447933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447933)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447933)Termination reason: Instruction limit
% 1.05/0.44 % (3447933)Termination phase: Saturation
% 1.05/0.44 % (3447933)Time elapsed: 0.055 s
% 1.05/0.44 % (3447933)Peak memory usage: 12 MB
% 1.05/0.44 % (3447933)Instructions burned: 104 (million)
% 1.05/0.44 % (3447943)Instruction limit reached!
% 1.05/0.44 % (3447943)------------------------------
% 1.05/0.44 % (3447943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447943)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447943)Termination reason: Instruction limit
% 1.05/0.44 % (3447943)Termination phase: Saturation
% 1.05/0.44 % (3447943)Time elapsed: 0.040 s
% 1.05/0.44 % (3447943)Peak memory usage: 12 MB
% 1.05/0.44 % (3447943)Instructions burned: 133 (million)
% 1.05/0.44 % (3447935)Instruction limit reached!
% 1.05/0.44 % (3447935)------------------------------
% 1.05/0.44 % (3447935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447935)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447935)Termination reason: Instruction limit
% 1.05/0.44 % (3447935)Termination phase: Saturation
% 1.05/0.44 % (3447935)Time elapsed: 0.063 s
% 1.05/0.44 % (3447935)Peak memory usage: 12 MB
% 1.05/0.44 % (3447935)Instructions burned: 132 (million)
% 1.05/0.44 % (3447949)ott-21_1_sil=16000:fs=off:random_seed=3877270027:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.05/0.44 % (3447934)Instruction limit reached!
% 1.05/0.44 % (3447934)------------------------------
% 1.05/0.44 % (3447934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447934)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447934)Termination reason: Instruction limit
% 1.05/0.44 % (3447934)Termination phase: Saturation
% 1.05/0.44 % (3447934)Time elapsed: 0.071 s
% 1.05/0.44 % (3447934)Peak memory usage: 12 MB
% 1.05/0.44 % (3447934)Instructions burned: 119 (million)
% 1.05/0.44 % (3447948)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=2017355724:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.05/0.44 % (3447948)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.05/0.44 % (3447948)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.05/0.44 % (3447950)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4204126571:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.05/0.44 % (3447952)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3184758291:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.05/0.44 % Exception at run slice level
% 1.05/0.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.05/0.44 % (3447949)Instruction limit reached!
% 1.05/0.44 % (3447949)------------------------------
% 1.05/0.44 % (3447949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447949)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447949)Termination reason: Instruction limit
% 1.05/0.44 % (3447949)Termination phase: Saturation
% 1.05/0.44 % (3447949)Time elapsed: 0.038 s
% 1.05/0.44 % (3447949)Peak memory usage: 11 MB
% 1.05/0.44 % (3447949)Instructions burned: 180 (million)
% 1.05/0.44 % (3447957)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2508679532:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.05/0.44 % Exception at run slice level
% 1.05/0.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.05/0.44 % (3447956)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3192061704:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.05/0.44 % (3447959)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1825136923:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.05/0.44 % (3447959)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.05/0.44 % (3447936)Instruction limit reached!
% 1.05/0.44 % (3447936)------------------------------
% 1.05/0.44 % (3447936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.44 % (3447936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.44 % (3447936)CaDiCaL version: 2.1.3
% 1.05/0.44 % (3447936)Termination reason: Instruction limit
% 1.05/0.44 % (3447936)Termination phase: Saturation
% 1.05/0.44 % (3447936)Time elapsed: 0.144 s
% 1.05/0.44 % (3447936)Peak memory usage: 12 MB
% 1.05/0.44 % (3447936)Instructions burned: 159 (million)
% 1.05/0.44 % (3447956) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3447925-3447956"...
% 1.05/0.44 % (3447956)...printing done.
% 1.05/0.44 % (3447956)Refutation found. Thanks to Tanya!
% 1.05/0.44 % SZS status Theorem for theBenchmark
% 1.05/0.44 % SZS output start Proof for theBenchmark
% 1.05/0.44 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.05/0.44 thf(func_def_0, type, x: $o).
% 1.05/0.44 thf(func_def_1, type, f0: ($o > $o)).
% 1.05/0.44 thf(func_def_2, type, f1: ($o > $o)).
% 1.05/0.44 thf(func_def_3, type, f2: ($o > $o)).
% 1.05/0.44 thf(func_def_4, type, f3: ($o > $o)).
% 1.05/0.44 thf(func_def_8, type, sF0: $o).
% 1.05/0.44 thf(func_def_9, type, sF1: $o).
% 1.05/0.44 thf(func_def_10, type, sF2: $o).
% 1.05/0.44 thf(func_def_11, type, sF3: $o).
% 1.05/0.44 thf(func_def_12, type, sF4: $o).
% 1.05/0.44 thf(func_def_13, type, sF5: $o).
% 1.05/0.44 thf(func_def_14, type, sF6: $o).
% 1.05/0.44 thf(func_def_15, type, sF7: $o).
% 1.05/0.44 thf(func_def_16, type, sF8: $o).
% 1.05/0.44 thf(func_def_17, type, sF9: $o).
% 1.05/0.44 thf(func_def_18, type, sF10: $o).
% 1.05/0.44 thf(func_def_19, type, sF11: $o).
% 1.05/0.44 thf(func_def_20, type, sF12: $o).
% 1.05/0.44 thf(func_def_21, type, sF13: $o).
% 1.05/0.44 thf(func_def_22, type, sF14: $o).
% 1.05/0.44 thf(func_def_23, type, vNOT: ($o > $o)).
% 1.05/0.44 thf(f1,conjecture,(
% 1.05/0.44 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 1.05/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski4)).
% 1.05/0.44 thf(f2,negated_conjecture,(
% 1.05/0.44 ~ (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 1.05/0.44 inference(negated_conjecture,[status(cth)],[f1])).
% 1.05/0.44 thf(f3,plain,(
% 1.05/0.44 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 1.05/0.44 inference(flattening,[],[f2])).
% 1.05/0.44 thf(f4,plain,(
% 1.05/0.44 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 1.05/0.44 inference(cnf_transformation,[],[f3])).
% 1.05/0.44 thf(f6,definition,(
% 1.05/0.44 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.05/0.44 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.05/0.44 thf(f7,definition,(
% 1.05/0.44 (sF0 = ((f3 @ x)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 1.05/0.44 thf(f8,plain,(
% 1.05/0.44 (((f3 @ x)) = sF0)),
% 1.05/0.44 inference(reorient_equations,[],[f7])).
% 1.05/0.44 thf(f9,definition,(
% 1.05/0.44 (sF1 = ((f2 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 1.05/0.44 thf(f10,plain,(
% 1.05/0.44 (((f2 @ sF0)) = sF1)),
% 1.05/0.44 inference(reorient_equations,[],[f9])).
% 1.05/0.44 thf(f11,definition,(
% 1.05/0.44 (sF2 = ((f2 @ sF1)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 1.05/0.44 thf(f12,plain,(
% 1.05/0.44 (((f2 @ sF1)) = sF2)),
% 1.05/0.44 inference(reorient_equations,[],[f11])).
% 1.05/0.44 thf(f13,definition,(
% 1.05/0.44 (sF3 = ((f2 @ sF2)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 1.05/0.44 thf(f14,plain,(
% 1.05/0.44 (((f2 @ sF2)) = sF3)),
% 1.05/0.44 inference(reorient_equations,[],[f13])).
% 1.05/0.44 thf(f15,definition,(
% 1.05/0.44 (sF4 = ((f1 @ sF3)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 1.05/0.44 thf(f16,plain,(
% 1.05/0.44 (((f1 @ sF3)) = sF4)),
% 1.05/0.44 inference(reorient_equations,[],[f15])).
% 1.05/0.44 thf(f17,definition,(
% 1.05/0.44 (sF5 = ((f0 @ sF4)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 1.05/0.44 thf(f18,plain,(
% 1.05/0.44 (((f0 @ sF4)) = sF5)),
% 1.05/0.44 inference(reorient_equations,[],[f17])).
% 1.05/0.44 thf(f19,definition,(
% 1.05/0.44 (sF6 = ((f0 @ sF5)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 1.05/0.44 thf(f20,plain,(
% 1.05/0.44 (((f0 @ sF5)) = sF6)),
% 1.05/0.44 inference(reorient_equations,[],[f19])).
% 1.05/0.44 thf(f21,definition,(
% 1.05/0.44 (sF7 = ((f0 @ sF6)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 1.05/0.44 thf(f22,plain,(
% 1.05/0.44 (((f0 @ sF6)) = sF7)),
% 1.05/0.44 inference(reorient_equations,[],[f21])).
% 1.05/0.44 thf(f23,definition,(
% 1.05/0.44 (sF8 = ((f3 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 1.05/0.44 thf(f24,plain,(
% 1.05/0.44 (((f3 @ sF0)) = sF8)),
% 1.05/0.44 inference(reorient_equations,[],[f23])).
% 1.05/0.44 thf(f25,definition,(
% 1.05/0.44 (sF9 = ((f3 @ sF8)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 1.05/0.44 thf(f26,plain,(
% 1.05/0.44 (((f3 @ sF8)) = sF9)),
% 1.05/0.44 inference(reorient_equations,[],[f25])).
% 1.05/0.44 thf(f27,definition,(
% 1.05/0.44 (sF10 = ((f2 @ sF9)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 1.05/0.44 thf(f28,plain,(
% 1.05/0.44 (((f2 @ sF9)) = sF10)),
% 1.05/0.44 inference(reorient_equations,[],[f27])).
% 1.05/0.44 thf(f29,definition,(
% 1.05/0.44 (sF11 = ((f1 @ sF10)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 1.05/0.44 thf(f30,plain,(
% 1.05/0.44 (((f1 @ sF10)) = sF11)),
% 1.05/0.44 inference(reorient_equations,[],[f29])).
% 1.05/0.44 thf(f31,definition,(
% 1.05/0.44 (sF12 = ((f1 @ sF11)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 1.05/0.44 thf(f32,plain,(
% 1.05/0.44 (((f1 @ sF11)) = sF12)),
% 1.05/0.44 inference(reorient_equations,[],[f31])).
% 1.05/0.44 thf(f33,definition,(
% 1.05/0.44 (sF13 = ((f1 @ sF12)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 1.05/0.44 thf(f34,plain,(
% 1.05/0.44 (((f1 @ sF12)) = sF13)),
% 1.05/0.44 inference(reorient_equations,[],[f33])).
% 1.05/0.44 thf(f35,definition,(
% 1.05/0.44 (sF14 = ((f0 @ sF13)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 1.05/0.44 thf(f36,plain,(
% 1.05/0.44 (((f0 @ sF13)) = sF14)),
% 1.05/0.44 inference(reorient_equations,[],[f35])).
% 1.05/0.44 thf(f37,plain,(
% 1.05/0.44 (sF7 != sF14)),
% 1.05/0.44 inference(definition_folding,[],[f4,f36,f34,f32,f30,f28,f26,f24,f8,f22,f20,f18,f16,f14,f12,f10,f8])).
% 1.05/0.44 thf(f38,plain,(
% 1.05/0.44 ($true = sF7) | ($true = sF14)),
% 1.05/0.44 inference(xor_proxy_clausification,[],[f37])).
% 1.05/0.44 thf(f39,plain,(
% 1.05/0.44 ($false = sF7) | ($false = sF14)),
% 1.05/0.44 inference(xor_proxy_clausification,[],[f37])).
% 1.05/0.44 thf(f40,plain,(
% 1.05/0.44 (((f3 @ x)) = $true) | ($false = sF0)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f8])).
% 1.05/0.44 thf(f41,plain,(
% 1.05/0.44 (((f3 @ x)) = $false) | ($true = sF0)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f8])).
% 1.05/0.44 thf(f42,plain,(
% 1.05/0.44 ($true = ((f2 @ sF0))) | ($false = sF1)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f10])).
% 1.05/0.44 thf(f43,plain,(
% 1.05/0.44 ($false = ((f2 @ sF0))) | ($true = sF1)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f10])).
% 1.05/0.44 thf(f44,plain,(
% 1.05/0.44 ($true = ((f2 @ sF1))) | ($false = sF2)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f12])).
% 1.05/0.44 thf(f45,plain,(
% 1.05/0.44 ($false = ((f2 @ sF1))) | ($true = sF2)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f12])).
% 1.05/0.44 thf(f46,plain,(
% 1.05/0.44 ($true = ((f2 @ sF2))) | ($false = sF3)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f14])).
% 1.05/0.44 thf(f47,plain,(
% 1.05/0.44 ($false = ((f2 @ sF2))) | ($true = sF3)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f14])).
% 1.05/0.44 thf(f48,plain,(
% 1.05/0.44 ($true = ((f1 @ sF3))) | ($false = sF4)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f16])).
% 1.05/0.44 thf(f49,plain,(
% 1.05/0.44 ($false = ((f1 @ sF3))) | ($true = sF4)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f16])).
% 1.05/0.44 thf(f50,plain,(
% 1.05/0.44 ($true = ((f0 @ sF4))) | ($false = sF5)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f18])).
% 1.05/0.44 thf(f51,plain,(
% 1.05/0.44 ($false = ((f0 @ sF4))) | ($true = sF5)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f18])).
% 1.05/0.44 thf(f52,plain,(
% 1.05/0.44 ($true = ((f0 @ sF5))) | ($false = sF6)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f20])).
% 1.05/0.44 thf(f53,plain,(
% 1.05/0.44 ($false = ((f0 @ sF5))) | ($true = sF6)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f20])).
% 1.05/0.44 thf(f54,plain,(
% 1.05/0.44 ($true = ((f0 @ sF6))) | ($false = sF7)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f22])).
% 1.05/0.44 thf(f55,plain,(
% 1.05/0.44 ($false = ((f0 @ sF6))) | ($true = sF7)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f22])).
% 1.05/0.44 thf(f56,plain,(
% 1.05/0.44 ($true = ((f3 @ sF0))) | ($false = sF8)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f24])).
% 1.05/0.44 thf(f57,plain,(
% 1.05/0.44 ($false = ((f3 @ sF0))) | ($true = sF8)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f24])).
% 1.05/0.44 thf(f58,plain,(
% 1.05/0.44 ($true = ((f3 @ sF8))) | ($false = sF9)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f26])).
% 1.05/0.44 thf(f59,plain,(
% 1.05/0.44 ($false = ((f3 @ sF8))) | ($true = sF9)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f26])).
% 1.05/0.44 thf(f60,plain,(
% 1.05/0.44 ($true = ((f2 @ sF9))) | ($false = sF10)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f28])).
% 1.05/0.44 thf(f61,plain,(
% 1.05/0.44 ($false = ((f2 @ sF9))) | ($true = sF10)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f28])).
% 1.05/0.44 thf(f62,plain,(
% 1.05/0.44 ($true = ((f1 @ sF10))) | ($false = sF11)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f30])).
% 1.05/0.44 thf(f63,plain,(
% 1.05/0.44 ($false = ((f1 @ sF10))) | ($true = sF11)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f30])).
% 1.05/0.44 thf(f64,plain,(
% 1.05/0.44 ($true = ((f1 @ sF11))) | ($false = sF12)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f32])).
% 1.05/0.44 thf(f65,plain,(
% 1.05/0.44 ($false = ((f1 @ sF11))) | ($true = sF12)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f32])).
% 1.05/0.44 thf(f66,plain,(
% 1.05/0.44 ($true = ((f1 @ sF12))) | ($false = sF13)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f34])).
% 1.05/0.44 thf(f67,plain,(
% 1.05/0.44 ($false = ((f1 @ sF12))) | ($true = sF13)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f34])).
% 1.05/0.44 thf(f68,plain,(
% 1.05/0.44 ($true = ((f0 @ sF13))) | ($false = sF14)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f36])).
% 1.05/0.44 thf(f69,plain,(
% 1.05/0.44 ($false = ((f0 @ sF13))) | ($true = sF14)),
% 1.05/0.44 inference(iff_proxy_clausification,[],[f36])).
% 1.05/0.44 thf(f71,definition,(
% 1.05/0.44 spl15_1 <=> ($false = sF14)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition])).
% 1.05/0.44 thf(f73,plain,(
% 1.05/0.44 ($false = sF14) | ~spl15_1),
% 1.05/0.44 inference(avatar_component_clause,[],[f71])).
% 1.05/0.44 thf(f75,definition,(
% 1.05/0.44 spl15_2 <=> ($false = sF7)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition])).
% 1.05/0.44 thf(f77,plain,(
% 1.05/0.44 ($false = sF7) | ~spl15_2),
% 1.05/0.44 inference(avatar_component_clause,[],[f75])).
% 1.05/0.44 thf(f78,plain,(
% 1.05/0.44 spl15_1 | spl15_2),
% 1.05/0.44 inference(avatar_split_clause,[],[f39,f75,f71])).
% 1.05/0.44 thf(f80,definition,(
% 1.05/0.44 spl15_3 <=> ($true = sF14)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition])).
% 1.05/0.44 thf(f82,plain,(
% 1.05/0.44 ($true = sF14) | ~spl15_3),
% 1.05/0.44 inference(avatar_component_clause,[],[f80])).
% 1.05/0.44 thf(f84,definition,(
% 1.05/0.44 spl15_4 <=> ($true = sF7)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition])).
% 1.05/0.44 thf(f86,plain,(
% 1.05/0.44 ($true = sF7) | ~spl15_4),
% 1.05/0.44 inference(avatar_component_clause,[],[f84])).
% 1.05/0.44 thf(f87,plain,(
% 1.05/0.44 spl15_3 | spl15_4),
% 1.05/0.44 inference(avatar_split_clause,[],[f38,f84,f80])).
% 1.05/0.44 thf(f89,definition,(
% 1.05/0.44 spl15_5 <=> ($true = sF0)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition])).
% 1.05/0.44 thf(f90,plain,(
% 1.05/0.44 ($true != sF0) | spl15_5),
% 1.05/0.44 inference(avatar_component_clause,[],[f89])).
% 1.05/0.44 thf(f91,plain,(
% 1.05/0.44 ($true = sF0) | ~spl15_5),
% 1.05/0.44 inference(avatar_component_clause,[],[f89])).
% 1.05/0.44 thf(f93,definition,(
% 1.05/0.44 spl15_6 <=> (((f3 @ x)) = $false)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition])).
% 1.05/0.44 thf(f95,plain,(
% 1.05/0.44 (((f3 @ x)) = $false) | ~spl15_6),
% 1.05/0.44 inference(avatar_component_clause,[],[f93])).
% 1.05/0.44 thf(f96,plain,(
% 1.05/0.44 spl15_5 | spl15_6),
% 1.05/0.44 inference(avatar_split_clause,[],[f41,f93,f89])).
% 1.05/0.44 thf(f98,definition,(
% 1.05/0.44 spl15_7 <=> ($false = sF0)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition])).
% 1.05/0.44 thf(f100,plain,(
% 1.05/0.44 ($false = sF0) | ~spl15_7),
% 1.05/0.44 inference(avatar_component_clause,[],[f98])).
% 1.05/0.44 thf(f102,definition,(
% 1.05/0.44 spl15_8 <=> (((f3 @ x)) = $true)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition])).
% 1.05/0.44 thf(f104,plain,(
% 1.05/0.44 (((f3 @ x)) = $true) | ~spl15_8),
% 1.05/0.44 inference(avatar_component_clause,[],[f102])).
% 1.05/0.44 thf(f105,plain,(
% 1.05/0.44 spl15_7 | spl15_8),
% 1.05/0.44 inference(avatar_split_clause,[],[f40,f102,f98])).
% 1.05/0.44 thf(f107,definition,(
% 1.05/0.44 spl15_9 <=> ($true = sF1)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition])).
% 1.05/0.44 thf(f108,plain,(
% 1.05/0.44 ($true != sF1) | spl15_9),
% 1.05/0.44 inference(avatar_component_clause,[],[f107])).
% 1.05/0.44 thf(f109,plain,(
% 1.05/0.44 ($true = sF1) | ~spl15_9),
% 1.05/0.44 inference(avatar_component_clause,[],[f107])).
% 1.05/0.44 thf(f111,definition,(
% 1.05/0.44 spl15_10 <=> ($false = ((f2 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition])).
% 1.05/0.44 thf(f112,plain,(
% 1.05/0.44 ($false != ((f2 @ sF0))) | spl15_10),
% 1.05/0.44 inference(avatar_component_clause,[],[f111])).
% 1.05/0.44 thf(f113,plain,(
% 1.05/0.44 ($false = ((f2 @ sF0))) | ~spl15_10),
% 1.05/0.44 inference(avatar_component_clause,[],[f111])).
% 1.05/0.44 thf(f114,plain,(
% 1.05/0.44 spl15_9 | spl15_10),
% 1.05/0.44 inference(avatar_split_clause,[],[f43,f111,f107])).
% 1.05/0.44 thf(f116,definition,(
% 1.05/0.44 spl15_11 <=> ($false = sF1)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition])).
% 1.05/0.44 thf(f118,plain,(
% 1.05/0.44 ($false = sF1) | ~spl15_11),
% 1.05/0.44 inference(avatar_component_clause,[],[f116])).
% 1.05/0.44 thf(f120,definition,(
% 1.05/0.44 spl15_12 <=> ($true = ((f2 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition])).
% 1.05/0.44 thf(f122,plain,(
% 1.05/0.44 ($true = ((f2 @ sF0))) | ~spl15_12),
% 1.05/0.44 inference(avatar_component_clause,[],[f120])).
% 1.05/0.44 thf(f123,plain,(
% 1.05/0.44 spl15_11 | spl15_12),
% 1.05/0.44 inference(avatar_split_clause,[],[f42,f120,f116])).
% 1.05/0.44 thf(f125,definition,(
% 1.05/0.44 spl15_13 <=> ($true = sF2)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition])).
% 1.05/0.44 thf(f126,plain,(
% 1.05/0.44 ($true != sF2) | spl15_13),
% 1.05/0.44 inference(avatar_component_clause,[],[f125])).
% 1.05/0.44 thf(f127,plain,(
% 1.05/0.44 ($true = sF2) | ~spl15_13),
% 1.05/0.44 inference(avatar_component_clause,[],[f125])).
% 1.05/0.44 thf(f129,definition,(
% 1.05/0.44 spl15_14 <=> ($false = ((f2 @ sF1)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition])).
% 1.05/0.44 thf(f130,plain,(
% 1.05/0.44 ($false != ((f2 @ sF1))) | spl15_14),
% 1.05/0.44 inference(avatar_component_clause,[],[f129])).
% 1.05/0.44 thf(f131,plain,(
% 1.05/0.44 ($false = ((f2 @ sF1))) | ~spl15_14),
% 1.05/0.44 inference(avatar_component_clause,[],[f129])).
% 1.05/0.44 thf(f132,plain,(
% 1.05/0.44 spl15_13 | spl15_14),
% 1.05/0.44 inference(avatar_split_clause,[],[f45,f129,f125])).
% 1.05/0.44 thf(f134,definition,(
% 1.05/0.44 spl15_15 <=> ($false = sF2)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition])).
% 1.05/0.44 thf(f136,plain,(
% 1.05/0.44 ($false = sF2) | ~spl15_15),
% 1.05/0.44 inference(avatar_component_clause,[],[f134])).
% 1.05/0.44 thf(f138,definition,(
% 1.05/0.44 spl15_16 <=> ($true = ((f2 @ sF1)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition])).
% 1.05/0.44 thf(f140,plain,(
% 1.05/0.44 ($true = ((f2 @ sF1))) | ~spl15_16),
% 1.05/0.44 inference(avatar_component_clause,[],[f138])).
% 1.05/0.44 thf(f141,plain,(
% 1.05/0.44 spl15_15 | spl15_16),
% 1.05/0.44 inference(avatar_split_clause,[],[f44,f138,f134])).
% 1.05/0.44 thf(f143,definition,(
% 1.05/0.44 spl15_17 <=> ($true = sF3)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition])).
% 1.05/0.44 thf(f144,plain,(
% 1.05/0.44 ($true != sF3) | spl15_17),
% 1.05/0.44 inference(avatar_component_clause,[],[f143])).
% 1.05/0.44 thf(f145,plain,(
% 1.05/0.44 ($true = sF3) | ~spl15_17),
% 1.05/0.44 inference(avatar_component_clause,[],[f143])).
% 1.05/0.44 thf(f147,definition,(
% 1.05/0.44 spl15_18 <=> ($false = ((f2 @ sF2)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition])).
% 1.05/0.44 thf(f148,plain,(
% 1.05/0.44 ($false != ((f2 @ sF2))) | spl15_18),
% 1.05/0.44 inference(avatar_component_clause,[],[f147])).
% 1.05/0.44 thf(f149,plain,(
% 1.05/0.44 ($false = ((f2 @ sF2))) | ~spl15_18),
% 1.05/0.44 inference(avatar_component_clause,[],[f147])).
% 1.05/0.44 thf(f150,plain,(
% 1.05/0.44 spl15_17 | spl15_18),
% 1.05/0.44 inference(avatar_split_clause,[],[f47,f147,f143])).
% 1.05/0.44 thf(f152,definition,(
% 1.05/0.44 spl15_19 <=> ($false = sF3)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition])).
% 1.05/0.44 thf(f154,plain,(
% 1.05/0.44 ($false = sF3) | ~spl15_19),
% 1.05/0.44 inference(avatar_component_clause,[],[f152])).
% 1.05/0.44 thf(f156,definition,(
% 1.05/0.44 spl15_20 <=> ($true = ((f2 @ sF2)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition])).
% 1.05/0.44 thf(f157,plain,(
% 1.05/0.44 ($true != ((f2 @ sF2))) | spl15_20),
% 1.05/0.44 inference(avatar_component_clause,[],[f156])).
% 1.05/0.44 thf(f158,plain,(
% 1.05/0.44 ($true = ((f2 @ sF2))) | ~spl15_20),
% 1.05/0.44 inference(avatar_component_clause,[],[f156])).
% 1.05/0.44 thf(f159,plain,(
% 1.05/0.44 spl15_19 | spl15_20),
% 1.05/0.44 inference(avatar_split_clause,[],[f46,f156,f152])).
% 1.05/0.44 thf(f161,definition,(
% 1.05/0.44 spl15_21 <=> ($true = sF4)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition])).
% 1.05/0.44 thf(f163,plain,(
% 1.05/0.44 ($true = sF4) | ~spl15_21),
% 1.05/0.44 inference(avatar_component_clause,[],[f161])).
% 1.05/0.44 thf(f165,definition,(
% 1.05/0.44 spl15_22 <=> ($false = ((f1 @ sF3)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition])).
% 1.05/0.44 thf(f166,plain,(
% 1.05/0.44 ($false != ((f1 @ sF3))) | spl15_22),
% 1.05/0.44 inference(avatar_component_clause,[],[f165])).
% 1.05/0.44 thf(f167,plain,(
% 1.05/0.44 ($false = ((f1 @ sF3))) | ~spl15_22),
% 1.05/0.44 inference(avatar_component_clause,[],[f165])).
% 1.05/0.44 thf(f168,plain,(
% 1.05/0.44 spl15_21 | spl15_22),
% 1.05/0.44 inference(avatar_split_clause,[],[f49,f165,f161])).
% 1.05/0.44 thf(f170,definition,(
% 1.05/0.44 spl15_23 <=> ($false = sF4)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_23])],[avatar_definition])).
% 1.05/0.44 thf(f172,plain,(
% 1.05/0.44 ($false = sF4) | ~spl15_23),
% 1.05/0.44 inference(avatar_component_clause,[],[f170])).
% 1.05/0.44 thf(f174,definition,(
% 1.05/0.44 spl15_24 <=> ($true = ((f1 @ sF3)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_24])],[avatar_definition])).
% 1.05/0.44 thf(f176,plain,(
% 1.05/0.44 ($true = ((f1 @ sF3))) | ~spl15_24),
% 1.05/0.44 inference(avatar_component_clause,[],[f174])).
% 1.05/0.44 thf(f177,plain,(
% 1.05/0.44 spl15_23 | spl15_24),
% 1.05/0.44 inference(avatar_split_clause,[],[f48,f174,f170])).
% 1.05/0.44 thf(f179,definition,(
% 1.05/0.44 spl15_25 <=> ($true = sF5)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition])).
% 1.05/0.44 thf(f181,plain,(
% 1.05/0.44 ($true = sF5) | ~spl15_25),
% 1.05/0.44 inference(avatar_component_clause,[],[f179])).
% 1.05/0.44 thf(f183,definition,(
% 1.05/0.44 spl15_26 <=> ($false = ((f0 @ sF4)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition])).
% 1.05/0.44 thf(f184,plain,(
% 1.05/0.44 ($false != ((f0 @ sF4))) | spl15_26),
% 1.05/0.44 inference(avatar_component_clause,[],[f183])).
% 1.05/0.44 thf(f185,plain,(
% 1.05/0.44 ($false = ((f0 @ sF4))) | ~spl15_26),
% 1.05/0.44 inference(avatar_component_clause,[],[f183])).
% 1.05/0.44 thf(f186,plain,(
% 1.05/0.44 spl15_25 | spl15_26),
% 1.05/0.44 inference(avatar_split_clause,[],[f51,f183,f179])).
% 1.05/0.44 thf(f188,definition,(
% 1.05/0.44 spl15_27 <=> ($false = sF5)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_27])],[avatar_definition])).
% 1.05/0.44 thf(f190,plain,(
% 1.05/0.44 ($false = sF5) | ~spl15_27),
% 1.05/0.44 inference(avatar_component_clause,[],[f188])).
% 1.05/0.44 thf(f192,definition,(
% 1.05/0.44 spl15_28 <=> ($true = ((f0 @ sF4)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition])).
% 1.05/0.44 thf(f194,plain,(
% 1.05/0.44 ($true = ((f0 @ sF4))) | ~spl15_28),
% 1.05/0.44 inference(avatar_component_clause,[],[f192])).
% 1.05/0.44 thf(f195,plain,(
% 1.05/0.44 spl15_27 | spl15_28),
% 1.05/0.44 inference(avatar_split_clause,[],[f50,f192,f188])).
% 1.05/0.44 thf(f197,definition,(
% 1.05/0.44 spl15_29 <=> ($true = sF6)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_29])],[avatar_definition])).
% 1.05/0.44 thf(f198,plain,(
% 1.05/0.44 ($true != sF6) | spl15_29),
% 1.05/0.44 inference(avatar_component_clause,[],[f197])).
% 1.05/0.44 thf(f199,plain,(
% 1.05/0.44 ($true = sF6) | ~spl15_29),
% 1.05/0.44 inference(avatar_component_clause,[],[f197])).
% 1.05/0.44 thf(f201,definition,(
% 1.05/0.44 spl15_30 <=> ($false = ((f0 @ sF5)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_30])],[avatar_definition])).
% 1.05/0.44 thf(f202,plain,(
% 1.05/0.44 ($false != ((f0 @ sF5))) | spl15_30),
% 1.05/0.44 inference(avatar_component_clause,[],[f201])).
% 1.05/0.44 thf(f203,plain,(
% 1.05/0.44 ($false = ((f0 @ sF5))) | ~spl15_30),
% 1.05/0.44 inference(avatar_component_clause,[],[f201])).
% 1.05/0.44 thf(f204,plain,(
% 1.05/0.44 spl15_29 | spl15_30),
% 1.05/0.44 inference(avatar_split_clause,[],[f53,f201,f197])).
% 1.05/0.44 thf(f206,definition,(
% 1.05/0.44 spl15_31 <=> ($false = sF6)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition])).
% 1.05/0.44 thf(f208,plain,(
% 1.05/0.44 ($false = sF6) | ~spl15_31),
% 1.05/0.44 inference(avatar_component_clause,[],[f206])).
% 1.05/0.44 thf(f210,definition,(
% 1.05/0.44 spl15_32 <=> ($true = ((f0 @ sF5)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_32])],[avatar_definition])).
% 1.05/0.44 thf(f212,plain,(
% 1.05/0.44 ($true = ((f0 @ sF5))) | ~spl15_32),
% 1.05/0.44 inference(avatar_component_clause,[],[f210])).
% 1.05/0.44 thf(f213,plain,(
% 1.05/0.44 spl15_31 | spl15_32),
% 1.05/0.44 inference(avatar_split_clause,[],[f52,f210,f206])).
% 1.05/0.44 thf(f215,definition,(
% 1.05/0.44 spl15_33 <=> ($false = ((f0 @ sF6)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_33])],[avatar_definition])).
% 1.05/0.44 thf(f217,plain,(
% 1.05/0.44 ($false = ((f0 @ sF6))) | ~spl15_33),
% 1.05/0.44 inference(avatar_component_clause,[],[f215])).
% 1.05/0.44 thf(f218,plain,(
% 1.05/0.44 spl15_4 | spl15_33),
% 1.05/0.44 inference(avatar_split_clause,[],[f55,f215,f84])).
% 1.05/0.44 thf(f220,definition,(
% 1.05/0.44 spl15_34 <=> ($true = ((f0 @ sF6)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition])).
% 1.05/0.44 thf(f222,plain,(
% 1.05/0.44 ($true = ((f0 @ sF6))) | ~spl15_34),
% 1.05/0.44 inference(avatar_component_clause,[],[f220])).
% 1.05/0.44 thf(f223,plain,(
% 1.05/0.44 spl15_2 | spl15_34),
% 1.05/0.44 inference(avatar_split_clause,[],[f54,f220,f75])).
% 1.05/0.44 thf(f225,definition,(
% 1.05/0.44 spl15_35 <=> ($true = sF8)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition])).
% 1.05/0.44 thf(f226,plain,(
% 1.05/0.44 ($true != sF8) | spl15_35),
% 1.05/0.44 inference(avatar_component_clause,[],[f225])).
% 1.05/0.44 thf(f227,plain,(
% 1.05/0.44 ($true = sF8) | ~spl15_35),
% 1.05/0.44 inference(avatar_component_clause,[],[f225])).
% 1.05/0.44 thf(f229,definition,(
% 1.05/0.44 spl15_36 <=> ($false = ((f3 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_36])],[avatar_definition])).
% 1.05/0.44 thf(f230,plain,(
% 1.05/0.44 ($false != ((f3 @ sF0))) | spl15_36),
% 1.05/0.44 inference(avatar_component_clause,[],[f229])).
% 1.05/0.44 thf(f231,plain,(
% 1.05/0.44 ($false = ((f3 @ sF0))) | ~spl15_36),
% 1.05/0.44 inference(avatar_component_clause,[],[f229])).
% 1.05/0.44 thf(f232,plain,(
% 1.05/0.44 spl15_35 | spl15_36),
% 1.05/0.44 inference(avatar_split_clause,[],[f57,f229,f225])).
% 1.05/0.44 thf(f234,definition,(
% 1.05/0.44 spl15_37 <=> ($false = sF8)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_37])],[avatar_definition])).
% 1.05/0.44 thf(f236,plain,(
% 1.05/0.44 ($false = sF8) | ~spl15_37),
% 1.05/0.44 inference(avatar_component_clause,[],[f234])).
% 1.05/0.44 thf(f238,definition,(
% 1.05/0.44 spl15_38 <=> ($true = ((f3 @ sF0)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_38])],[avatar_definition])).
% 1.05/0.44 thf(f240,plain,(
% 1.05/0.44 ($true = ((f3 @ sF0))) | ~spl15_38),
% 1.05/0.44 inference(avatar_component_clause,[],[f238])).
% 1.05/0.44 thf(f241,plain,(
% 1.05/0.44 spl15_37 | spl15_38),
% 1.05/0.44 inference(avatar_split_clause,[],[f56,f238,f234])).
% 1.05/0.44 thf(f243,definition,(
% 1.05/0.44 spl15_39 <=> ($true = sF9)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_39])],[avatar_definition])).
% 1.05/0.44 thf(f245,plain,(
% 1.05/0.44 ($true = sF9) | ~spl15_39),
% 1.05/0.44 inference(avatar_component_clause,[],[f243])).
% 1.05/0.44 thf(f247,definition,(
% 1.05/0.44 spl15_40 <=> ($false = ((f3 @ sF8)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_40])],[avatar_definition])).
% 1.05/0.44 thf(f248,plain,(
% 1.05/0.44 ($false != ((f3 @ sF8))) | spl15_40),
% 1.05/0.44 inference(avatar_component_clause,[],[f247])).
% 1.05/0.44 thf(f249,plain,(
% 1.05/0.44 ($false = ((f3 @ sF8))) | ~spl15_40),
% 1.05/0.44 inference(avatar_component_clause,[],[f247])).
% 1.05/0.44 thf(f250,plain,(
% 1.05/0.44 spl15_39 | spl15_40),
% 1.05/0.44 inference(avatar_split_clause,[],[f59,f247,f243])).
% 1.05/0.44 thf(f252,definition,(
% 1.05/0.44 spl15_41 <=> ($false = sF9)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_41])],[avatar_definition])).
% 1.05/0.44 thf(f254,plain,(
% 1.05/0.44 ($false = sF9) | ~spl15_41),
% 1.05/0.44 inference(avatar_component_clause,[],[f252])).
% 1.05/0.44 thf(f256,definition,(
% 1.05/0.44 spl15_42 <=> ($true = ((f3 @ sF8)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_42])],[avatar_definition])).
% 1.05/0.44 thf(f258,plain,(
% 1.05/0.44 ($true = ((f3 @ sF8))) | ~spl15_42),
% 1.05/0.44 inference(avatar_component_clause,[],[f256])).
% 1.05/0.44 thf(f259,plain,(
% 1.05/0.44 spl15_41 | spl15_42),
% 1.05/0.44 inference(avatar_split_clause,[],[f58,f256,f252])).
% 1.05/0.44 thf(f261,definition,(
% 1.05/0.44 spl15_43 <=> ($true = sF10)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_43])],[avatar_definition])).
% 1.05/0.44 thf(f263,plain,(
% 1.05/0.44 ($true = sF10) | ~spl15_43),
% 1.05/0.44 inference(avatar_component_clause,[],[f261])).
% 1.05/0.44 thf(f265,definition,(
% 1.05/0.44 spl15_44 <=> ($false = ((f2 @ sF9)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_44])],[avatar_definition])).
% 1.05/0.44 thf(f266,plain,(
% 1.05/0.44 ($false != ((f2 @ sF9))) | spl15_44),
% 1.05/0.44 inference(avatar_component_clause,[],[f265])).
% 1.05/0.44 thf(f267,plain,(
% 1.05/0.44 ($false = ((f2 @ sF9))) | ~spl15_44),
% 1.05/0.44 inference(avatar_component_clause,[],[f265])).
% 1.05/0.44 thf(f268,plain,(
% 1.05/0.44 spl15_43 | spl15_44),
% 1.05/0.44 inference(avatar_split_clause,[],[f61,f265,f261])).
% 1.05/0.44 thf(f270,definition,(
% 1.05/0.44 spl15_45 <=> ($false = sF10)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_45])],[avatar_definition])).
% 1.05/0.44 thf(f272,plain,(
% 1.05/0.44 ($false = sF10) | ~spl15_45),
% 1.05/0.44 inference(avatar_component_clause,[],[f270])).
% 1.05/0.44 thf(f274,definition,(
% 1.05/0.44 spl15_46 <=> ($true = ((f2 @ sF9)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_46])],[avatar_definition])).
% 1.05/0.44 thf(f276,plain,(
% 1.05/0.44 ($true = ((f2 @ sF9))) | ~spl15_46),
% 1.05/0.44 inference(avatar_component_clause,[],[f274])).
% 1.05/0.44 thf(f277,plain,(
% 1.05/0.44 spl15_45 | spl15_46),
% 1.05/0.44 inference(avatar_split_clause,[],[f60,f274,f270])).
% 1.05/0.44 thf(f279,definition,(
% 1.05/0.44 spl15_47 <=> ($true = sF11)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_47])],[avatar_definition])).
% 1.05/0.44 thf(f281,plain,(
% 1.05/0.44 ($true = sF11) | ~spl15_47),
% 1.05/0.44 inference(avatar_component_clause,[],[f279])).
% 1.05/0.44 thf(f283,definition,(
% 1.05/0.44 spl15_48 <=> ($false = ((f1 @ sF10)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_48])],[avatar_definition])).
% 1.05/0.44 thf(f284,plain,(
% 1.05/0.44 ($false != ((f1 @ sF10))) | spl15_48),
% 1.05/0.44 inference(avatar_component_clause,[],[f283])).
% 1.05/0.44 thf(f285,plain,(
% 1.05/0.44 ($false = ((f1 @ sF10))) | ~spl15_48),
% 1.05/0.44 inference(avatar_component_clause,[],[f283])).
% 1.05/0.44 thf(f286,plain,(
% 1.05/0.44 spl15_47 | spl15_48),
% 1.05/0.44 inference(avatar_split_clause,[],[f63,f283,f279])).
% 1.05/0.44 thf(f288,definition,(
% 1.05/0.44 spl15_49 <=> ($false = sF11)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_49])],[avatar_definition])).
% 1.05/0.44 thf(f290,plain,(
% 1.05/0.44 ($false = sF11) | ~spl15_49),
% 1.05/0.44 inference(avatar_component_clause,[],[f288])).
% 1.05/0.44 thf(f292,definition,(
% 1.05/0.44 spl15_50 <=> ($true = ((f1 @ sF10)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_50])],[avatar_definition])).
% 1.05/0.44 thf(f294,plain,(
% 1.05/0.44 ($true = ((f1 @ sF10))) | ~spl15_50),
% 1.05/0.44 inference(avatar_component_clause,[],[f292])).
% 1.05/0.44 thf(f295,plain,(
% 1.05/0.44 spl15_49 | spl15_50),
% 1.05/0.44 inference(avatar_split_clause,[],[f62,f292,f288])).
% 1.05/0.44 thf(f297,definition,(
% 1.05/0.44 spl15_51 <=> ($true = sF12)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_51])],[avatar_definition])).
% 1.05/0.44 thf(f299,plain,(
% 1.05/0.44 ($true = sF12) | ~spl15_51),
% 1.05/0.44 inference(avatar_component_clause,[],[f297])).
% 1.05/0.44 thf(f301,definition,(
% 1.05/0.44 spl15_52 <=> ($false = ((f1 @ sF11)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_52])],[avatar_definition])).
% 1.05/0.44 thf(f302,plain,(
% 1.05/0.44 ($false != ((f1 @ sF11))) | spl15_52),
% 1.05/0.44 inference(avatar_component_clause,[],[f301])).
% 1.05/0.44 thf(f303,plain,(
% 1.05/0.44 ($false = ((f1 @ sF11))) | ~spl15_52),
% 1.05/0.44 inference(avatar_component_clause,[],[f301])).
% 1.05/0.44 thf(f304,plain,(
% 1.05/0.44 spl15_51 | spl15_52),
% 1.05/0.44 inference(avatar_split_clause,[],[f65,f301,f297])).
% 1.05/0.44 thf(f306,definition,(
% 1.05/0.44 spl15_53 <=> ($false = sF12)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition])).
% 1.05/0.44 thf(f307,plain,(
% 1.05/0.44 ($false != sF12) | spl15_53),
% 1.05/0.44 inference(avatar_component_clause,[],[f306])).
% 1.05/0.44 thf(f308,plain,(
% 1.05/0.44 ($false = sF12) | ~spl15_53),
% 1.05/0.44 inference(avatar_component_clause,[],[f306])).
% 1.05/0.44 thf(f310,definition,(
% 1.05/0.44 spl15_54 <=> ($true = ((f1 @ sF11)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_54])],[avatar_definition])).
% 1.05/0.44 thf(f311,plain,(
% 1.05/0.44 ($true != ((f1 @ sF11))) | spl15_54),
% 1.05/0.44 inference(avatar_component_clause,[],[f310])).
% 1.05/0.44 thf(f312,plain,(
% 1.05/0.44 ($true = ((f1 @ sF11))) | ~spl15_54),
% 1.05/0.44 inference(avatar_component_clause,[],[f310])).
% 1.05/0.44 thf(f313,plain,(
% 1.05/0.44 spl15_53 | spl15_54),
% 1.05/0.44 inference(avatar_split_clause,[],[f64,f310,f306])).
% 1.05/0.44 thf(f315,definition,(
% 1.05/0.44 spl15_55 <=> ($true = sF13)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_55])],[avatar_definition])).
% 1.05/0.44 thf(f317,plain,(
% 1.05/0.44 ($true = sF13) | ~spl15_55),
% 1.05/0.44 inference(avatar_component_clause,[],[f315])).
% 1.05/0.44 thf(f319,definition,(
% 1.05/0.44 spl15_56 <=> ($false = ((f1 @ sF12)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_56])],[avatar_definition])).
% 1.05/0.44 thf(f321,plain,(
% 1.05/0.44 ($false = ((f1 @ sF12))) | ~spl15_56),
% 1.05/0.44 inference(avatar_component_clause,[],[f319])).
% 1.05/0.44 thf(f322,plain,(
% 1.05/0.44 spl15_55 | spl15_56),
% 1.05/0.44 inference(avatar_split_clause,[],[f67,f319,f315])).
% 1.05/0.44 thf(f324,definition,(
% 1.05/0.44 spl15_57 <=> ($false = sF13)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_57])],[avatar_definition])).
% 1.05/0.44 thf(f326,plain,(
% 1.05/0.44 ($false = sF13) | ~spl15_57),
% 1.05/0.44 inference(avatar_component_clause,[],[f324])).
% 1.05/0.44 thf(f328,definition,(
% 1.05/0.44 spl15_58 <=> ($true = ((f1 @ sF12)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition])).
% 1.05/0.44 thf(f329,plain,(
% 1.05/0.44 ($true != ((f1 @ sF12))) | spl15_58),
% 1.05/0.44 inference(avatar_component_clause,[],[f328])).
% 1.05/0.44 thf(f330,plain,(
% 1.05/0.44 ($true = ((f1 @ sF12))) | ~spl15_58),
% 1.05/0.44 inference(avatar_component_clause,[],[f328])).
% 1.05/0.44 thf(f331,plain,(
% 1.05/0.44 spl15_57 | spl15_58),
% 1.05/0.44 inference(avatar_split_clause,[],[f66,f328,f324])).
% 1.05/0.44 thf(f333,definition,(
% 1.05/0.44 spl15_59 <=> ($false = ((f0 @ sF13)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_59])],[avatar_definition])).
% 1.05/0.44 thf(f335,plain,(
% 1.05/0.44 ($false = ((f0 @ sF13))) | ~spl15_59),
% 1.05/0.44 inference(avatar_component_clause,[],[f333])).
% 1.05/0.44 thf(f336,plain,(
% 1.05/0.44 spl15_3 | spl15_59),
% 1.05/0.44 inference(avatar_split_clause,[],[f69,f333,f80])).
% 1.05/0.44 thf(f338,definition,(
% 1.05/0.44 spl15_60 <=> ($true = ((f0 @ sF13)))),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition])).
% 1.05/0.44 thf(f340,plain,(
% 1.05/0.44 ($true = ((f0 @ sF13))) | ~spl15_60),
% 1.05/0.44 inference(avatar_component_clause,[],[f338])).
% 1.05/0.44 thf(f341,plain,(
% 1.05/0.44 spl15_1 | spl15_60),
% 1.05/0.44 inference(avatar_split_clause,[],[f68,f338,f71])).
% 1.05/0.44 thf(f342,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_2 | ~spl15_4)),
% 1.05/0.44 inference(forward_demodulation,[],[f86,f77])).
% 1.05/0.44 thf(f343,plain,(
% 1.05/0.44 $false | (~spl15_2 | ~spl15_4)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f342])).
% 1.05/0.44 thf(f344,plain,(
% 1.05/0.44 ~spl15_2 | ~spl15_4),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f343])).
% 1.05/0.44 thf(f345,plain,(
% 1.05/0.44 ($true = ((f0 @ $true))) | (~spl15_55 | ~spl15_60)),
% 1.05/0.44 inference(forward_demodulation,[],[f340,f317])).
% 1.05/0.44 thf(f347,plain,(
% 1.05/0.44 ($false = ((f0 @ $true))) | (~spl15_29 | ~spl15_33)),
% 1.05/0.44 inference(forward_demodulation,[],[f217,f199])).
% 1.05/0.44 thf(f358,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_5 | ~spl15_7)),
% 1.05/0.44 inference(constrained_superposition,[],[f100,f91])).
% 1.05/0.44 thf(f362,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_7)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f358])).
% 1.05/0.44 thf(f363,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_7),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f362])).
% 1.05/0.44 thf(f367,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_9 | ~spl15_11)),
% 1.05/0.44 inference(constrained_superposition,[],[f118,f109])).
% 1.05/0.44 thf(f371,plain,(
% 1.05/0.44 $false | (~spl15_9 | ~spl15_11)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f367])).
% 1.05/0.44 thf(f372,plain,(
% 1.05/0.44 ~spl15_9 | ~spl15_11),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f371])).
% 1.05/0.44 thf(f375,plain,(
% 1.05/0.44 ($true = ((f2 @ $true))) | (~spl15_5 | ~spl15_12)),
% 1.05/0.44 inference(forward_demodulation,[],[f122,f91])).
% 1.05/0.44 thf(f385,plain,(
% 1.05/0.44 ($false = ((f2 @ $true))) | (~spl15_9 | ~spl15_14)),
% 1.05/0.44 inference(forward_demodulation,[],[f131,f109])).
% 1.05/0.44 thf(f397,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_21 | ~spl15_23)),
% 1.05/0.44 inference(constrained_superposition,[],[f172,f163])).
% 1.05/0.44 thf(f401,plain,(
% 1.05/0.44 $false | (~spl15_21 | ~spl15_23)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f397])).
% 1.05/0.44 thf(f402,plain,(
% 1.05/0.44 ~spl15_21 | ~spl15_23),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f401])).
% 1.05/0.44 thf(f405,plain,(
% 1.05/0.44 ($false = ((f1 @ $false))) | (~spl15_19 | ~spl15_22)),
% 1.05/0.44 inference(forward_demodulation,[],[f167,f154])).
% 1.05/0.44 thf(f415,plain,(
% 1.05/0.44 ($false = ((f0 @ $false))) | (~spl15_23 | ~spl15_26)),
% 1.05/0.44 inference(forward_demodulation,[],[f185,f172])).
% 1.05/0.44 thf(f425,plain,(
% 1.05/0.44 ($false = ((f0 @ $false))) | (~spl15_27 | ~spl15_30)),
% 1.05/0.44 inference(forward_demodulation,[],[f203,f190])).
% 1.05/0.44 thf(f426,plain,(
% 1.05/0.44 ($false = ((f0 @ $false))) | (~spl15_31 | ~spl15_33)),
% 1.05/0.44 inference(forward_demodulation,[],[f217,f208])).
% 1.05/0.44 thf(f428,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_35 | ~spl15_37)),
% 1.05/0.44 inference(constrained_superposition,[],[f236,f227])).
% 1.05/0.44 thf(f432,plain,(
% 1.05/0.44 $false | (~spl15_35 | ~spl15_37)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f428])).
% 1.05/0.44 thf(f433,plain,(
% 1.05/0.44 ~spl15_35 | ~spl15_37),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f432])).
% 1.05/0.44 thf(f436,plain,(
% 1.05/0.44 ($false = ((f3 @ $true))) | (~spl15_5 | ~spl15_36)),
% 1.05/0.44 inference(forward_demodulation,[],[f231,f91])).
% 1.05/0.44 thf(f446,plain,(
% 1.05/0.44 ($false = ((f3 @ $false))) | (~spl15_37 | ~spl15_40)),
% 1.05/0.44 inference(forward_demodulation,[],[f249,f236])).
% 1.05/0.44 thf(f448,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_43 | ~spl15_45)),
% 1.05/0.44 inference(constrained_superposition,[],[f272,f263])).
% 1.05/0.44 thf(f452,plain,(
% 1.05/0.44 $false | (~spl15_43 | ~spl15_45)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f448])).
% 1.05/0.44 thf(f453,plain,(
% 1.05/0.44 ~spl15_43 | ~spl15_45),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f452])).
% 1.05/0.44 thf(f456,plain,(
% 1.05/0.44 ($false = ((f2 @ $false))) | (~spl15_41 | ~spl15_44)),
% 1.05/0.44 inference(forward_demodulation,[],[f267,f254])).
% 1.05/0.44 thf(f458,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_47 | ~spl15_49)),
% 1.05/0.44 inference(constrained_superposition,[],[f290,f281])).
% 1.05/0.44 thf(f462,plain,(
% 1.05/0.44 $false | (~spl15_47 | ~spl15_49)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f458])).
% 1.05/0.44 thf(f463,plain,(
% 1.05/0.44 ~spl15_47 | ~spl15_49),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f462])).
% 1.05/0.44 thf(f466,plain,(
% 1.05/0.44 ($false = ((f1 @ $false))) | (~spl15_45 | ~spl15_48)),
% 1.05/0.44 inference(forward_demodulation,[],[f285,f272])).
% 1.05/0.44 thf(f476,plain,(
% 1.05/0.44 ($false = ((f1 @ $false))) | (~spl15_49 | ~spl15_52)),
% 1.05/0.44 inference(forward_demodulation,[],[f303,f290])).
% 1.05/0.44 thf(f487,plain,(
% 1.05/0.44 ($true = ((f0 @ $false))) | (~spl15_57 | ~spl15_60)),
% 1.05/0.44 inference(forward_demodulation,[],[f340,f326])).
% 1.05/0.44 thf(f488,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_23 | ~spl15_26 | ~spl15_57 | ~spl15_60)),
% 1.05/0.44 inference(forward_demodulation,[],[f487,f415])).
% 1.05/0.44 thf(f489,plain,(
% 1.05/0.44 $false | (~spl15_23 | ~spl15_26 | ~spl15_57 | ~spl15_60)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f488])).
% 1.05/0.44 thf(f490,plain,(
% 1.05/0.44 ~spl15_23 | ~spl15_26 | ~spl15_57 | ~spl15_60),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f489])).
% 1.05/0.44 thf(f491,plain,(
% 1.05/0.44 ($false != ((f0 @ $false))) | (~spl15_23 | spl15_26)),
% 1.05/0.44 inference(forward_demodulation,[],[f184,f172])).
% 1.05/0.44 thf(f493,plain,(
% 1.05/0.44 ($true = ((f0 @ $false))) | (~spl15_23 | ~spl15_28)),
% 1.05/0.44 inference(forward_demodulation,[],[f194,f172])).
% 1.05/0.44 thf(f494,plain,(
% 1.05/0.44 ($false = ((f0 @ $true))) | (~spl15_25 | ~spl15_30)),
% 1.05/0.44 inference(forward_demodulation,[],[f203,f181])).
% 1.05/0.44 thf(f495,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_31 | ~spl15_33 | ~spl15_57 | ~spl15_60)),
% 1.05/0.44 inference(forward_demodulation,[],[f487,f426])).
% 1.05/0.44 thf(f496,plain,(
% 1.05/0.44 $false | (~spl15_31 | ~spl15_33 | ~spl15_57 | ~spl15_60)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f495])).
% 1.05/0.44 thf(f497,plain,(
% 1.05/0.44 ~spl15_31 | ~spl15_33 | ~spl15_57 | ~spl15_60),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f496])).
% 1.05/0.44 thf(f498,plain,(
% 1.05/0.44 $false | (~spl15_23 | spl15_26 | ~spl15_31 | ~spl15_33)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f491,f426])).
% 1.05/0.44 thf(f499,plain,(
% 1.05/0.44 ~spl15_23 | spl15_26 | ~spl15_31 | ~spl15_33),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f498])).
% 1.05/0.44 thf(f509,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f330,f308])).
% 1.05/0.44 thf(f510,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_23 | ~spl15_26 | ~spl15_28)),
% 1.05/0.44 inference(forward_demodulation,[],[f493,f415])).
% 1.05/0.44 thf(f511,plain,(
% 1.05/0.44 $false | (~spl15_23 | ~spl15_26 | ~spl15_28)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f510])).
% 1.05/0.44 thf(f512,plain,(
% 1.05/0.44 ~spl15_23 | ~spl15_26 | ~spl15_28),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f511])).
% 1.05/0.44 thf(f513,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_30 | ~spl15_32)),
% 1.05/0.44 inference(forward_demodulation,[],[f212,f203])).
% 1.05/0.44 thf(f514,plain,(
% 1.05/0.44 $false | (~spl15_30 | ~spl15_32)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f513])).
% 1.05/0.44 thf(f515,plain,(
% 1.05/0.44 ~spl15_30 | ~spl15_32),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f514])).
% 1.05/0.44 thf(f516,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_19 | ~spl15_22 | ~spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f509,f405])).
% 1.05/0.44 thf(f517,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_22 | ~spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f516])).
% 1.05/0.44 thf(f518,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_22 | ~spl15_53 | ~spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f517])).
% 1.05/0.44 thf(f521,plain,(
% 1.05/0.44 ($false != ((f0 @ $false))) | (~spl15_27 | spl15_30)),
% 1.05/0.44 inference(forward_demodulation,[],[f202,f190])).
% 1.05/0.44 thf(f522,plain,(
% 1.05/0.44 ($true = ((f0 @ $false))) | (~spl15_27 | ~spl15_32)),
% 1.05/0.44 inference(forward_demodulation,[],[f212,f190])).
% 1.05/0.44 thf(f530,plain,(
% 1.05/0.44 $false | (~spl15_23 | ~spl15_26 | ~spl15_27 | spl15_30)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f521,f415])).
% 1.05/0.44 thf(f531,plain,(
% 1.05/0.44 ~spl15_23 | ~spl15_26 | ~spl15_27 | spl15_30),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f530])).
% 1.05/0.44 thf(f532,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_23 | ~spl15_26 | ~spl15_27 | ~spl15_32)),
% 1.05/0.44 inference(forward_demodulation,[],[f522,f415])).
% 1.05/0.44 thf(f533,plain,(
% 1.05/0.44 $false | (~spl15_23 | ~spl15_26 | ~spl15_27 | ~spl15_32)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f532])).
% 1.05/0.44 thf(f534,plain,(
% 1.05/0.44 ~spl15_23 | ~spl15_26 | ~spl15_27 | ~spl15_32),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f533])).
% 1.05/0.44 thf(f538,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f312,f290])).
% 1.05/0.44 thf(f539,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_56 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f330,f321])).
% 1.05/0.44 thf(f540,plain,(
% 1.05/0.44 $false | (~spl15_56 | ~spl15_58)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f539])).
% 1.05/0.44 thf(f541,plain,(
% 1.05/0.44 ~spl15_56 | ~spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f540])).
% 1.05/0.44 thf(f542,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_18 | ~spl15_20)),
% 1.05/0.44 inference(forward_demodulation,[],[f158,f149])).
% 1.05/0.44 thf(f543,plain,(
% 1.05/0.44 $false | (~spl15_18 | ~spl15_20)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f542])).
% 1.05/0.44 thf(f544,plain,(
% 1.05/0.44 ~spl15_18 | ~spl15_20),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f543])).
% 1.05/0.44 thf(f546,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_45 | ~spl15_48 | ~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f538,f466])).
% 1.05/0.44 thf(f547,plain,(
% 1.05/0.44 $false | (~spl15_45 | ~spl15_48 | ~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f546])).
% 1.05/0.44 thf(f548,plain,(
% 1.05/0.44 ~spl15_45 | ~spl15_48 | ~spl15_49 | ~spl15_54),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f547])).
% 1.05/0.44 thf(f549,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_45 | ~spl15_50)),
% 1.05/0.44 inference(forward_demodulation,[],[f294,f272])).
% 1.05/0.44 thf(f550,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_52 | ~spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f312,f303])).
% 1.05/0.44 thf(f551,plain,(
% 1.05/0.44 $false | (~spl15_52 | ~spl15_54)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f550])).
% 1.05/0.44 thf(f552,plain,(
% 1.05/0.44 ~spl15_52 | ~spl15_54),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f551])).
% 1.05/0.44 thf(f556,plain,(
% 1.05/0.44 ($true = ((f2 @ $false))) | (~spl15_41 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f276,f254])).
% 1.05/0.44 thf(f557,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_48 | ~spl15_50)),
% 1.05/0.44 inference(forward_demodulation,[],[f294,f285])).
% 1.05/0.44 thf(f558,plain,(
% 1.05/0.44 $false | (~spl15_48 | ~spl15_50)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f557])).
% 1.05/0.44 thf(f559,plain,(
% 1.05/0.44 ~spl15_48 | ~spl15_50),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f558])).
% 1.05/0.44 thf(f560,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_41 | ~spl15_44 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f556,f456])).
% 1.05/0.44 thf(f561,plain,(
% 1.05/0.44 $false | (~spl15_41 | ~spl15_44 | ~spl15_46)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f560])).
% 1.05/0.44 thf(f562,plain,(
% 1.05/0.44 ~spl15_41 | ~spl15_44 | ~spl15_46),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f561])).
% 1.05/0.44 thf(f563,plain,(
% 1.05/0.44 ($false != ((f2 @ $false))) | (~spl15_41 | spl15_44)),
% 1.05/0.44 inference(forward_demodulation,[],[f266,f254])).
% 1.05/0.44 thf(f564,plain,(
% 1.05/0.44 ($false != ((f1 @ $true))) | (~spl15_43 | spl15_48)),
% 1.05/0.44 inference(forward_demodulation,[],[f284,f263])).
% 1.05/0.44 thf(f567,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF2) | spl15_13),
% 1.05/0.44 inference(constrained_superposition,[],[f126,f6])).
% 1.05/0.44 thf(f568,plain,(
% 1.05/0.44 ($false = sF2) | spl15_13),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f567])).
% 1.05/0.44 thf(f581,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF6) | spl15_29),
% 1.05/0.44 inference(constrained_superposition,[],[f198,f6])).
% 1.05/0.44 thf(f582,plain,(
% 1.05/0.44 ($false = sF6) | spl15_29),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f581])).
% 1.05/0.44 thf(f594,plain,(
% 1.05/0.44 ($true = ((f3 @ $true))) | (x = $false) | ~spl15_8),
% 1.05/0.44 inference(constrained_superposition,[],[f104,f6])).
% 1.05/0.44 thf(f595,plain,(
% 1.05/0.44 ($true = $false) | (x = $false) | (~spl15_5 | ~spl15_8 | ~spl15_36)),
% 1.05/0.44 inference(forward_demodulation,[],[f594,f436])).
% 1.05/0.44 thf(f596,plain,(
% 1.05/0.44 (x = $false) | (~spl15_5 | ~spl15_8 | ~spl15_36)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f595])).
% 1.05/0.44 thf(f602,plain,(
% 1.05/0.44 ($true = ((f3 @ $false))) | (~spl15_5 | ~spl15_8 | ~spl15_36)),
% 1.05/0.44 inference(constrained_superposition,[],[f104,f596])).
% 1.05/0.44 thf(f604,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_5 | ~spl15_8 | ~spl15_36 | ~spl15_37 | ~spl15_40)),
% 1.05/0.44 inference(forward_demodulation,[],[f602,f446])).
% 1.05/0.44 thf(f605,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_8 | ~spl15_36 | ~spl15_37 | ~spl15_40)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f604])).
% 1.05/0.44 thf(f606,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_8 | ~spl15_36 | ~spl15_37 | ~spl15_40),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f605])).
% 1.05/0.44 thf(f611,definition,(
% 1.05/0.44 spl15_61 <=> (x = $false)),
% 1.05/0.44 introduced(definition,[new_symbols(definition,[spl15_61])],[avatar_definition])).
% 1.05/0.44 thf(f612,plain,(
% 1.05/0.44 (x != $false) | spl15_61),
% 1.05/0.44 inference(avatar_component_clause,[],[f611])).
% 1.05/0.44 thf(f613,plain,(
% 1.05/0.44 (x = $false) | ~spl15_61),
% 1.05/0.44 inference(avatar_component_clause,[],[f611])).
% 1.05/0.44 thf(f621,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF0) | spl15_5),
% 1.05/0.44 inference(constrained_superposition,[],[f90,f6])).
% 1.05/0.44 thf(f622,plain,(
% 1.05/0.44 ($false = sF0) | spl15_5),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f621])).
% 1.05/0.44 thf(f639,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_5 | ~spl15_9 | ~spl15_12 | ~spl15_14)),
% 1.05/0.44 inference(forward_demodulation,[],[f375,f385])).
% 1.05/0.44 thf(f640,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_9 | ~spl15_12 | ~spl15_14)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f639])).
% 1.05/0.44 thf(f641,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_9 | ~spl15_12 | ~spl15_14),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f640])).
% 1.05/0.44 thf(f647,plain,(
% 1.05/0.44 ($true = ((f2 @ $true))) | (~spl15_39 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f276,f245])).
% 1.05/0.44 thf(f648,plain,(
% 1.05/0.44 ($false != ((f2 @ $true))) | (~spl15_39 | spl15_44)),
% 1.05/0.44 inference(forward_demodulation,[],[f266,f245])).
% 1.05/0.44 thf(f651,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_9 | ~spl15_14 | ~spl15_39 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f647,f385])).
% 1.05/0.44 thf(f652,plain,(
% 1.05/0.44 $false | (~spl15_9 | ~spl15_14 | ~spl15_39 | ~spl15_46)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f651])).
% 1.05/0.44 thf(f653,plain,(
% 1.05/0.44 ~spl15_9 | ~spl15_14 | ~spl15_39 | ~spl15_46),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f652])).
% 1.05/0.44 thf(f654,plain,(
% 1.05/0.44 $false | (~spl15_9 | ~spl15_14 | ~spl15_39 | spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f648,f385])).
% 1.05/0.44 thf(f655,plain,(
% 1.05/0.44 ~spl15_9 | ~spl15_14 | ~spl15_39 | spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f654])).
% 1.05/0.44 thf(f656,plain,(
% 1.05/0.44 ($false = ((f2 @ $true))) | (~spl15_5 | ~spl15_10)),
% 1.05/0.44 inference(forward_demodulation,[],[f113,f91])).
% 1.05/0.44 thf(f659,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF1) | spl15_9),
% 1.05/0.44 inference(constrained_superposition,[],[f108,f6])).
% 1.05/0.44 thf(f660,plain,(
% 1.05/0.44 ($false = sF1) | spl15_9),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f659])).
% 1.05/0.44 thf(f672,plain,(
% 1.05/0.44 ($false = ((f2 @ $false))) | (~spl15_11 | ~spl15_14)),
% 1.05/0.44 inference(constrained_superposition,[],[f131,f118])).
% 1.05/0.44 thf(f679,plain,(
% 1.05/0.44 ($false = ((f1 @ $true))) | (~spl15_17 | ~spl15_22)),
% 1.05/0.44 inference(constrained_superposition,[],[f167,f145])).
% 1.05/0.44 thf(f682,plain,(
% 1.05/0.44 $false | (~spl15_17 | ~spl15_22 | ~spl15_43 | spl15_48)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f679,f564])).
% 1.05/0.44 thf(f683,plain,(
% 1.05/0.44 ~spl15_17 | ~spl15_22 | ~spl15_43 | spl15_48),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f682])).
% 1.05/0.44 thf(f687,plain,(
% 1.05/0.44 ($false = ((f2 @ $true))) | (~spl15_39 | ~spl15_44)),
% 1.05/0.44 inference(forward_demodulation,[],[f267,f245])).
% 1.05/0.44 thf(f695,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF3) | spl15_17),
% 1.05/0.44 inference(constrained_superposition,[],[f144,f6])).
% 1.05/0.44 thf(f696,plain,(
% 1.05/0.44 ($false = sF3) | spl15_17),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f695])).
% 1.05/0.44 thf(f717,plain,(
% 1.05/0.44 ($false != ((f1 @ $true))) | (~spl15_47 | spl15_52)),
% 1.05/0.44 inference(constrained_superposition,[],[f302,f281])).
% 1.05/0.44 thf(f720,plain,(
% 1.05/0.44 ($true = ((f1 @ $true))) | (~spl15_47 | ~spl15_54)),
% 1.05/0.44 inference(constrained_superposition,[],[f312,f281])).
% 1.05/0.44 thf(f725,plain,(
% 1.05/0.44 ($true = ((f1 @ $true))) | ($false = sF12) | ~spl15_58),
% 1.05/0.44 inference(constrained_superposition,[],[f330,f6])).
% 1.05/0.44 thf(f726,plain,(
% 1.05/0.44 ($true = ((f1 @ $true))) | (~spl15_51 | ~spl15_58)),
% 1.05/0.44 inference(constrained_superposition,[],[f330,f299])).
% 1.05/0.44 thf(f754,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_5 | ~spl15_10 | ~spl15_12)),
% 1.05/0.44 inference(constrained_superposition,[],[f656,f375])).
% 1.05/0.44 thf(f758,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_10 | ~spl15_12)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f754])).
% 1.05/0.44 thf(f759,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_10 | ~spl15_12),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f758])).
% 1.05/0.44 thf(f762,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_5 | ~spl15_10 | ~spl15_39 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f647,f656])).
% 1.05/0.44 thf(f763,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_10 | ~spl15_39 | ~spl15_46)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f762])).
% 1.05/0.44 thf(f764,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_10 | ~spl15_39 | ~spl15_46),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f763])).
% 1.05/0.44 thf(f766,plain,(
% 1.05/0.44 spl15_7 | spl15_5),
% 1.05/0.44 inference(avatar_split_clause,[],[f622,f89,f98])).
% 1.05/0.44 thf(f767,plain,(
% 1.05/0.44 ($false = ((f3 @ $false))) | (~spl15_6 | ~spl15_61)),
% 1.05/0.44 inference(forward_demodulation,[],[f95,f613])).
% 1.05/0.44 thf(f773,plain,(
% 1.05/0.44 ($false = ((f2 @ $false))) | (~spl15_7 | ~spl15_10)),
% 1.05/0.44 inference(forward_demodulation,[],[f113,f100])).
% 1.05/0.44 thf(f779,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_11 | ~spl15_14 | ~spl15_41 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f556,f672])).
% 1.05/0.44 thf(f780,plain,(
% 1.05/0.44 $false | (~spl15_11 | ~spl15_14 | ~spl15_41 | ~spl15_46)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f779])).
% 1.05/0.44 thf(f781,plain,(
% 1.05/0.44 ~spl15_11 | ~spl15_14 | ~spl15_41 | ~spl15_46),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f780])).
% 1.05/0.44 thf(f785,plain,(
% 1.05/0.44 ($false != ((f2 @ $false))) | (~spl15_11 | spl15_14)),
% 1.05/0.44 inference(forward_demodulation,[],[f130,f118])).
% 1.05/0.44 thf(f787,plain,(
% 1.05/0.44 ($true = ((f2 @ $false))) | (~spl15_11 | ~spl15_16)),
% 1.05/0.44 inference(forward_demodulation,[],[f140,f118])).
% 1.05/0.44 thf(f788,plain,(
% 1.05/0.44 ($false = ((f2 @ $true))) | (~spl15_13 | ~spl15_18)),
% 1.05/0.44 inference(forward_demodulation,[],[f149,f127])).
% 1.05/0.44 thf(f789,plain,(
% 1.05/0.44 ($true != ((f2 @ $true))) | (~spl15_13 | spl15_20)),
% 1.05/0.44 inference(forward_demodulation,[],[f157,f127])).
% 1.05/0.44 thf(f791,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_10 | ~spl15_41 | spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f563,f773])).
% 1.05/0.44 thf(f792,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_10 | ~spl15_41 | spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f791])).
% 1.05/0.44 thf(f793,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_7 | ~spl15_10 | ~spl15_41 | ~spl15_46)),
% 1.05/0.44 inference(forward_demodulation,[],[f556,f773])).
% 1.05/0.44 thf(f794,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_10 | ~spl15_41 | ~spl15_46)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f793])).
% 1.05/0.44 thf(f795,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_10 | ~spl15_41 | ~spl15_46),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f794])).
% 1.05/0.44 thf(f796,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_10 | ~spl15_11 | spl15_14)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f785,f773])).
% 1.05/0.44 thf(f797,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_10 | ~spl15_11 | spl15_14),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f796])).
% 1.05/0.44 thf(f798,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_7 | ~spl15_10 | ~spl15_11 | ~spl15_16)),
% 1.05/0.44 inference(forward_demodulation,[],[f787,f773])).
% 1.05/0.44 thf(f799,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_10 | ~spl15_11 | ~spl15_16)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f798])).
% 1.05/0.44 thf(f800,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_10 | ~spl15_11 | ~spl15_16),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f799])).
% 1.05/0.44 thf(f802,plain,(
% 1.05/0.44 spl15_15 | spl15_13),
% 1.05/0.44 inference(avatar_split_clause,[],[f568,f125,f134])).
% 1.05/0.44 thf(f806,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_36 | ~spl15_38)),
% 1.05/0.44 inference(forward_demodulation,[],[f240,f231])).
% 1.05/0.44 thf(f807,plain,(
% 1.05/0.44 $false | (~spl15_36 | ~spl15_38)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f806])).
% 1.05/0.44 thf(f808,plain,(
% 1.05/0.44 ~spl15_36 | ~spl15_38),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f807])).
% 1.05/0.44 thf(f810,plain,(
% 1.05/0.44 ($false = ((f2 @ $false))) | (~spl15_15 | ~spl15_18)),
% 1.05/0.44 inference(forward_demodulation,[],[f149,f136])).
% 1.05/0.44 thf(f815,plain,(
% 1.05/0.44 ($false != ((f2 @ $false))) | (~spl15_7 | spl15_10)),
% 1.05/0.44 inference(forward_demodulation,[],[f112,f100])).
% 1.05/0.44 thf(f817,plain,(
% 1.05/0.44 ($true = ((f2 @ $false))) | (~spl15_7 | ~spl15_12)),
% 1.05/0.44 inference(forward_demodulation,[],[f122,f100])).
% 1.05/0.44 thf(f829,plain,(
% 1.05/0.44 $false | (~spl15_15 | ~spl15_18 | ~spl15_41 | spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f810,f563])).
% 1.05/0.44 thf(f830,plain,(
% 1.05/0.44 ~spl15_15 | ~spl15_18 | ~spl15_41 | spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f829])).
% 1.05/0.44 thf(f834,plain,(
% 1.05/0.44 ($false != ((f2 @ $true))) | (~spl15_9 | spl15_14)),
% 1.05/0.44 inference(forward_demodulation,[],[f130,f109])).
% 1.05/0.44 thf(f836,plain,(
% 1.05/0.44 ($true = ((f2 @ $true))) | (~spl15_9 | ~spl15_16)),
% 1.05/0.44 inference(forward_demodulation,[],[f140,f109])).
% 1.05/0.44 thf(f841,plain,(
% 1.05/0.44 $false | (~spl15_9 | ~spl15_13 | spl15_14 | ~spl15_18)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f834,f788])).
% 1.05/0.44 thf(f842,plain,(
% 1.05/0.44 ~spl15_9 | ~spl15_13 | spl15_14 | ~spl15_18),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f841])).
% 1.05/0.44 thf(f843,plain,(
% 1.05/0.44 $false | (~spl15_9 | ~spl15_13 | ~spl15_16 | spl15_20)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f836,f789])).
% 1.05/0.44 thf(f844,plain,(
% 1.05/0.44 ~spl15_9 | ~spl15_13 | ~spl15_16 | spl15_20),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f843])).
% 1.05/0.44 thf(f848,plain,(
% 1.05/0.44 ($false != ((f1 @ $true))) | (~spl15_17 | spl15_22)),
% 1.05/0.44 inference(forward_demodulation,[],[f166,f145])).
% 1.05/0.44 thf(f850,plain,(
% 1.05/0.44 ($true = ((f1 @ $true))) | (~spl15_17 | ~spl15_24)),
% 1.05/0.44 inference(forward_demodulation,[],[f176,f145])).
% 1.05/0.44 thf(f851,plain,(
% 1.05/0.44 ($false = ((f0 @ $true))) | (~spl15_21 | ~spl15_26)),
% 1.05/0.44 inference(forward_demodulation,[],[f185,f163])).
% 1.05/0.44 thf(f858,plain,(
% 1.05/0.44 ($true = ((f0 @ $true))) | (~spl15_21 | ~spl15_28)),
% 1.05/0.44 inference(forward_demodulation,[],[f194,f163])).
% 1.05/0.44 thf(f863,plain,(
% 1.05/0.44 ($false = ((f3 @ $false))) | (~spl15_7 | ~spl15_36)),
% 1.05/0.44 inference(constrained_superposition,[],[f231,f100])).
% 1.05/0.44 thf(f865,plain,(
% 1.05/0.44 ($true != $true) | ($false = sF8) | spl15_35),
% 1.05/0.44 inference(constrained_superposition,[],[f226,f6])).
% 1.05/0.44 thf(f866,plain,(
% 1.05/0.44 ($false = sF8) | spl15_35),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f865])).
% 1.05/0.44 thf(f875,plain,(
% 1.05/0.44 ($false = ((f3 @ $true))) | ($false = sF8) | ~spl15_40),
% 1.05/0.44 inference(constrained_superposition,[],[f249,f6])).
% 1.05/0.44 thf(f893,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_21 | ~spl15_26 | ~spl15_55 | ~spl15_60)),
% 1.05/0.44 inference(constrained_superposition,[],[f851,f345])).
% 1.05/0.44 thf(f897,plain,(
% 1.05/0.44 $false | (~spl15_21 | ~spl15_26 | ~spl15_55 | ~spl15_60)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f893])).
% 1.05/0.44 thf(f898,plain,(
% 1.05/0.44 ~spl15_21 | ~spl15_26 | ~spl15_55 | ~spl15_60),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f897])).
% 1.05/0.44 thf(f901,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_21 | ~spl15_26 | ~spl15_28)),
% 1.05/0.44 inference(forward_demodulation,[],[f858,f851])).
% 1.05/0.44 thf(f902,plain,(
% 1.05/0.44 $false | (~spl15_21 | ~spl15_26 | ~spl15_28)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f901])).
% 1.05/0.44 thf(f903,plain,(
% 1.05/0.44 ~spl15_21 | ~spl15_26 | ~spl15_28),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f902])).
% 1.05/0.44 thf(f909,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_1 | ~spl15_3)),
% 1.05/0.44 inference(constrained_superposition,[],[f73,f82])).
% 1.05/0.44 thf(f913,plain,(
% 1.05/0.44 $false | (~spl15_1 | ~spl15_3)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f909])).
% 1.05/0.44 thf(f914,plain,(
% 1.05/0.44 ~spl15_1 | ~spl15_3),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f913])).
% 1.05/0.44 thf(f920,plain,(
% 1.05/0.44 ($false = ((f0 @ $true))) | (~spl15_55 | ~spl15_59)),
% 1.05/0.44 inference(forward_demodulation,[],[f335,f317])).
% 1.05/0.44 thf(f922,plain,(
% 1.05/0.44 ($false != ((f0 @ $true))) | (~spl15_21 | spl15_26)),
% 1.05/0.44 inference(forward_demodulation,[],[f184,f163])).
% 1.05/0.44 thf(f935,plain,(
% 1.05/0.44 $false | (~spl15_21 | ~spl15_25 | spl15_26 | ~spl15_30)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f922,f494])).
% 1.05/0.44 thf(f936,plain,(
% 1.05/0.44 ~spl15_21 | ~spl15_25 | spl15_26 | ~spl15_30),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f935])).
% 1.05/0.44 thf(f952,plain,(
% 1.05/0.44 ($true = ((f0 @ $false))) | (~spl15_31 | ~spl15_34)),
% 1.05/0.44 inference(forward_demodulation,[],[f222,f208])).
% 1.05/0.44 thf(f960,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_27 | ~spl15_30 | ~spl15_31 | ~spl15_34)),
% 1.05/0.44 inference(forward_demodulation,[],[f952,f425])).
% 1.05/0.44 thf(f961,plain,(
% 1.05/0.44 $false | (~spl15_27 | ~spl15_30 | ~spl15_31 | ~spl15_34)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f960])).
% 1.05/0.44 thf(f962,plain,(
% 1.05/0.44 ~spl15_27 | ~spl15_30 | ~spl15_31 | ~spl15_34),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f961])).
% 1.05/0.44 thf(f972,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_17 | ~spl15_22 | ~spl15_51 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f726,f679])).
% 1.05/0.44 thf(f973,plain,(
% 1.05/0.44 $false | (~spl15_17 | ~spl15_22 | ~spl15_51 | ~spl15_58)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f972])).
% 1.05/0.44 thf(f974,plain,(
% 1.05/0.44 ~spl15_17 | ~spl15_22 | ~spl15_51 | ~spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f973])).
% 1.05/0.44 thf(f975,plain,(
% 1.05/0.44 ($true = ((f1 @ $true))) | (spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f725,f307])).
% 1.05/0.44 thf(f976,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_17 | ~spl15_22 | ~spl15_24)),
% 1.05/0.44 inference(forward_demodulation,[],[f850,f679])).
% 1.05/0.44 thf(f977,plain,(
% 1.05/0.44 $false | (~spl15_17 | ~spl15_22 | ~spl15_24)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f976])).
% 1.05/0.44 thf(f978,plain,(
% 1.05/0.44 ~spl15_17 | ~spl15_22 | ~spl15_24),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f977])).
% 1.05/0.44 thf(f985,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_17 | ~spl15_22 | spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f975,f679])).
% 1.05/0.44 thf(f986,plain,(
% 1.05/0.44 $false | (~spl15_17 | ~spl15_22 | spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f985])).
% 1.05/0.44 thf(f987,plain,(
% 1.05/0.44 ~spl15_17 | ~spl15_22 | spl15_53 | ~spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f986])).
% 1.05/0.44 thf(f993,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_49 | ~spl15_52 | ~spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f509,f476])).
% 1.05/0.44 thf(f994,plain,(
% 1.05/0.44 $false | (~spl15_49 | ~spl15_52 | ~spl15_53 | ~spl15_58)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f993])).
% 1.05/0.44 thf(f995,plain,(
% 1.05/0.44 ~spl15_49 | ~spl15_52 | ~spl15_53 | ~spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f994])).
% 1.05/0.44 thf(f1007,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_7 | ~spl15_12 | ~spl15_41 | ~spl15_44)),
% 1.05/0.44 inference(forward_demodulation,[],[f817,f456])).
% 1.05/0.44 thf(f1008,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_12 | ~spl15_41 | ~spl15_44)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1007])).
% 1.05/0.44 thf(f1009,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_12 | ~spl15_41 | ~spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1008])).
% 1.05/0.44 thf(f1010,plain,(
% 1.05/0.44 $false | (~spl15_7 | spl15_10 | ~spl15_41 | ~spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f815,f456])).
% 1.05/0.44 thf(f1011,plain,(
% 1.05/0.44 ~spl15_7 | spl15_10 | ~spl15_41 | ~spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1010])).
% 1.05/0.44 thf(f1018,plain,(
% 1.05/0.44 ($false != ((f3 @ $true))) | (~spl15_5 | spl15_36)),
% 1.05/0.44 inference(forward_demodulation,[],[f230,f91])).
% 1.05/0.44 thf(f1021,plain,(
% 1.05/0.44 ($true = $false) | ($false = ((f3 @ $true))) | (~spl15_35 | ~spl15_40)),
% 1.05/0.44 inference(forward_demodulation,[],[f875,f227])).
% 1.05/0.44 thf(f1022,plain,(
% 1.05/0.44 ($false = ((f3 @ $true))) | (~spl15_35 | ~spl15_40)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1021])).
% 1.05/0.44 thf(f1027,plain,(
% 1.05/0.44 $false | (~spl15_5 | ~spl15_35 | spl15_36 | ~spl15_40)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1022,f1018])).
% 1.05/0.44 thf(f1028,plain,(
% 1.05/0.44 ~spl15_5 | ~spl15_35 | spl15_36 | ~spl15_40),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1027])).
% 1.05/0.44 thf(f1034,plain,(
% 1.05/0.44 spl15_11 | spl15_9),
% 1.05/0.44 inference(avatar_split_clause,[],[f660,f107,f116])).
% 1.05/0.44 thf(f1048,plain,(
% 1.05/0.44 ($true = ((f3 @ $false))) | (~spl15_7 | ~spl15_38)),
% 1.05/0.44 inference(forward_demodulation,[],[f240,f100])).
% 1.05/0.44 thf(f1059,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_6 | ~spl15_7 | ~spl15_38 | ~spl15_61)),
% 1.05/0.44 inference(forward_demodulation,[],[f1048,f767])).
% 1.05/0.44 thf(f1060,plain,(
% 1.05/0.44 $false | (~spl15_6 | ~spl15_7 | ~spl15_38 | ~spl15_61)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1059])).
% 1.05/0.44 thf(f1061,plain,(
% 1.05/0.44 ~spl15_6 | ~spl15_7 | ~spl15_38 | ~spl15_61),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1060])).
% 1.05/0.44 thf(f1063,plain,(
% 1.05/0.44 spl15_19 | spl15_17),
% 1.05/0.44 inference(avatar_split_clause,[],[f696,f143,f152])).
% 1.05/0.44 thf(f1071,plain,(
% 1.05/0.44 ($false != ((f1 @ $false))) | (~spl15_19 | spl15_22)),
% 1.05/0.44 inference(forward_demodulation,[],[f166,f154])).
% 1.05/0.44 thf(f1073,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_19 | ~spl15_24)),
% 1.05/0.44 inference(forward_demodulation,[],[f176,f154])).
% 1.05/0.44 thf(f1078,plain,(
% 1.05/0.44 ($true = ((f0 @ $true))) | (~spl15_29 | ~spl15_34)),
% 1.05/0.44 inference(forward_demodulation,[],[f222,f199])).
% 1.05/0.44 thf(f1088,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_29 | ~spl15_34 | ~spl15_55 | ~spl15_59)),
% 1.05/0.44 inference(forward_demodulation,[],[f1078,f920])).
% 1.05/0.44 thf(f1089,plain,(
% 1.05/0.44 $false | (~spl15_29 | ~spl15_34 | ~spl15_55 | ~spl15_59)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1088])).
% 1.05/0.44 thf(f1090,plain,(
% 1.05/0.44 ~spl15_29 | ~spl15_34 | ~spl15_55 | ~spl15_59),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1089])).
% 1.05/0.44 thf(f1093,plain,(
% 1.05/0.44 ($true != ((f1 @ $false))) | (~spl15_53 | spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f329,f308])).
% 1.05/0.44 thf(f1101,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_21 | ~spl15_26 | ~spl15_29 | ~spl15_34)),
% 1.05/0.44 inference(forward_demodulation,[],[f1078,f851])).
% 1.05/0.44 thf(f1102,plain,(
% 1.05/0.44 $false | (~spl15_21 | ~spl15_26 | ~spl15_29 | ~spl15_34)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1101])).
% 1.05/0.44 thf(f1103,plain,(
% 1.05/0.44 ~spl15_21 | ~spl15_26 | ~spl15_29 | ~spl15_34),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1102])).
% 1.05/0.44 thf(f1104,plain,(
% 1.05/0.44 $false | (~spl15_45 | ~spl15_50 | ~spl15_53 | spl15_58)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1093,f549])).
% 1.05/0.44 thf(f1105,plain,(
% 1.05/0.44 ~spl15_45 | ~spl15_50 | ~spl15_53 | spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1104])).
% 1.05/0.44 thf(f1118,plain,(
% 1.05/0.44 ($false = ((f1 @ $true))) | (~spl15_51 | ~spl15_56)),
% 1.05/0.44 inference(forward_demodulation,[],[f321,f299])).
% 1.05/0.44 thf(f1119,plain,(
% 1.05/0.44 ($true != ((f1 @ $true))) | (~spl15_51 | spl15_58)),
% 1.05/0.44 inference(forward_demodulation,[],[f329,f299])).
% 1.05/0.44 thf(f1121,plain,(
% 1.05/0.44 $false | (~spl15_47 | ~spl15_51 | spl15_52 | ~spl15_56)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1118,f717])).
% 1.05/0.44 thf(f1122,plain,(
% 1.05/0.44 ~spl15_47 | ~spl15_51 | spl15_52 | ~spl15_56),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1121])).
% 1.05/0.44 thf(f1123,plain,(
% 1.05/0.44 $false | (~spl15_47 | ~spl15_51 | ~spl15_54 | spl15_58)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1119,f720])).
% 1.05/0.44 thf(f1124,plain,(
% 1.05/0.44 ~spl15_47 | ~spl15_51 | ~spl15_54 | spl15_58),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1123])).
% 1.05/0.44 thf(f1133,plain,(
% 1.05/0.44 $false | (~spl15_19 | spl15_22 | ~spl15_45 | ~spl15_48)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1071,f466])).
% 1.05/0.44 thf(f1134,plain,(
% 1.05/0.44 ~spl15_19 | spl15_22 | ~spl15_45 | ~spl15_48),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1133])).
% 1.05/0.44 thf(f1135,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_19 | ~spl15_24 | ~spl15_45 | ~spl15_48)),
% 1.05/0.44 inference(forward_demodulation,[],[f1073,f466])).
% 1.05/0.44 thf(f1136,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_24 | ~spl15_45 | ~spl15_48)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1135])).
% 1.05/0.44 thf(f1137,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_24 | ~spl15_45 | ~spl15_48),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1136])).
% 1.05/0.44 thf(f1159,plain,(
% 1.05/0.44 ($false = ((f1 @ $true))) | (~spl15_43 | ~spl15_48)),
% 1.05/0.44 inference(forward_demodulation,[],[f285,f263])).
% 1.05/0.44 thf(f1169,plain,(
% 1.05/0.44 $false | (~spl15_17 | spl15_22 | ~spl15_43 | ~spl15_48)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1159,f848])).
% 1.05/0.44 thf(f1170,plain,(
% 1.05/0.44 ~spl15_17 | spl15_22 | ~spl15_43 | ~spl15_48),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1169])).
% 1.05/0.44 thf(f1181,plain,(
% 1.05/0.44 spl15_31 | spl15_29),
% 1.05/0.44 inference(avatar_split_clause,[],[f582,f197,f206])).
% 1.05/0.44 thf(f1186,plain,(
% 1.05/0.44 ($false = ((f0 @ $false))) | (~spl15_57 | ~spl15_59)),
% 1.05/0.44 inference(forward_demodulation,[],[f335,f326])).
% 1.05/0.44 thf(f1193,plain,(
% 1.05/0.44 $false | (~spl15_23 | spl15_26 | ~spl15_57 | ~spl15_59)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1186,f491])).
% 1.05/0.44 thf(f1194,plain,(
% 1.05/0.44 ~spl15_23 | spl15_26 | ~spl15_57 | ~spl15_59),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1193])).
% 1.05/0.44 thf(f1217,plain,(
% 1.05/0.44 ($false != ((f1 @ $false))) | (~spl15_45 | spl15_48)),
% 1.05/0.44 inference(forward_demodulation,[],[f284,f272])).
% 1.05/0.44 thf(f1219,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_45 | ~spl15_50)),
% 1.05/0.44 inference(forward_demodulation,[],[f294,f272])).
% 1.05/0.44 thf(f1238,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_22 | ~spl15_45 | spl15_48)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1217,f405])).
% 1.05/0.44 thf(f1239,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_22 | ~spl15_45 | spl15_48),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1238])).
% 1.05/0.44 thf(f1240,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_19 | ~spl15_22 | ~spl15_45 | ~spl15_50)),
% 1.05/0.44 inference(forward_demodulation,[],[f1219,f405])).
% 1.05/0.44 thf(f1241,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_22 | ~spl15_45 | ~spl15_50)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1240])).
% 1.05/0.44 thf(f1242,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_22 | ~spl15_45 | ~spl15_50),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1241])).
% 1.05/0.44 thf(f1254,plain,(
% 1.05/0.44 ($false != ((f0 @ $true))) | (~spl15_25 | spl15_30)),
% 1.05/0.44 inference(forward_demodulation,[],[f202,f181])).
% 1.05/0.44 thf(f1260,plain,(
% 1.05/0.44 ($false != ((f0 @ $true))) | (~spl15_21 | spl15_26)),
% 1.05/0.44 inference(forward_demodulation,[],[f184,f163])).
% 1.05/0.44 thf(f1262,plain,(
% 1.05/0.44 $false | (~spl15_25 | ~spl15_29 | spl15_30 | ~spl15_33)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1254,f347])).
% 1.05/0.44 thf(f1263,plain,(
% 1.05/0.44 ~spl15_25 | ~spl15_29 | spl15_30 | ~spl15_33),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1262])).
% 1.05/0.44 thf(f1266,plain,(
% 1.05/0.44 $false | (~spl15_21 | spl15_26 | ~spl15_29 | ~spl15_33)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1260,f347])).
% 1.05/0.44 thf(f1267,plain,(
% 1.05/0.44 ~spl15_21 | spl15_26 | ~spl15_29 | ~spl15_33),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1266])).
% 1.05/0.44 thf(f1283,plain,(
% 1.05/0.44 ($false = ((f1 @ $true))) | (~spl15_47 | ~spl15_52)),
% 1.05/0.44 inference(forward_demodulation,[],[f303,f281])).
% 1.05/0.44 thf(f1288,plain,(
% 1.05/0.44 ($true != ((f1 @ $true))) | (~spl15_47 | spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f311,f281])).
% 1.05/0.44 thf(f1304,plain,(
% 1.05/0.44 $false | (~spl15_17 | spl15_22 | ~spl15_47 | ~spl15_52)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1283,f848])).
% 1.05/0.44 thf(f1305,plain,(
% 1.05/0.44 ~spl15_17 | spl15_22 | ~spl15_47 | ~spl15_52),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1304])).
% 1.05/0.44 thf(f1306,plain,(
% 1.05/0.44 $false | (~spl15_17 | ~spl15_24 | ~spl15_47 | spl15_54)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1288,f850])).
% 1.05/0.44 thf(f1307,plain,(
% 1.05/0.44 ~spl15_17 | ~spl15_24 | ~spl15_47 | spl15_54),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1306])).
% 1.05/0.44 thf(f1338,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_40 | ~spl15_42)),
% 1.05/0.44 inference(forward_demodulation,[],[f258,f249])).
% 1.05/0.44 thf(f1339,plain,(
% 1.05/0.44 $false | (~spl15_40 | ~spl15_42)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1338])).
% 1.05/0.44 thf(f1340,plain,(
% 1.05/0.44 ~spl15_40 | ~spl15_42),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1339])).
% 1.05/0.44 thf(f1364,plain,(
% 1.05/0.44 ($false != ((f3 @ $true))) | (~spl15_35 | spl15_40)),
% 1.05/0.44 inference(forward_demodulation,[],[f248,f227])).
% 1.05/0.44 thf(f1378,plain,(
% 1.05/0.44 ($false != ((f1 @ $false))) | (~spl15_49 | spl15_52)),
% 1.05/0.44 inference(forward_demodulation,[],[f302,f290])).
% 1.05/0.44 thf(f1379,plain,(
% 1.05/0.44 ($true = ((f1 @ $false))) | (~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f312,f290])).
% 1.05/0.44 thf(f1393,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_22 | ~spl15_49 | spl15_52)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1378,f405])).
% 1.05/0.44 thf(f1394,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_22 | ~spl15_49 | spl15_52),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1393])).
% 1.05/0.44 thf(f1395,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_19 | ~spl15_22 | ~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(forward_demodulation,[],[f1379,f405])).
% 1.05/0.44 thf(f1396,plain,(
% 1.05/0.44 $false | (~spl15_19 | ~spl15_22 | ~spl15_49 | ~spl15_54)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1395])).
% 1.05/0.44 thf(f1397,plain,(
% 1.05/0.44 ~spl15_19 | ~spl15_22 | ~spl15_49 | ~spl15_54),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1396])).
% 1.05/0.44 thf(f1446,plain,(
% 1.05/0.44 ($false = ((f3 @ $true))) | (x = $false) | ~spl15_6),
% 1.05/0.44 inference(constrained_superposition,[],[f95,f6])).
% 1.05/0.44 thf(f1449,plain,(
% 1.05/0.44 (x = $false) | (~spl15_6 | ~spl15_35 | spl15_40)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1446,f1364])).
% 1.05/0.44 thf(f1450,plain,(
% 1.05/0.44 $false | (~spl15_6 | ~spl15_35 | spl15_40 | spl15_61)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1449,f612])).
% 1.05/0.44 thf(f1451,plain,(
% 1.05/0.44 ~spl15_6 | ~spl15_35 | spl15_40 | spl15_61),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1450])).
% 1.05/0.44 thf(f1452,plain,(
% 1.05/0.44 spl15_37 | spl15_35),
% 1.05/0.44 inference(avatar_split_clause,[],[f866,f225,f234])).
% 1.05/0.44 thf(f1461,plain,(
% 1.05/0.44 ($true = ((f3 @ $false))) | (~spl15_37 | ~spl15_42)),
% 1.05/0.44 inference(forward_demodulation,[],[f258,f236])).
% 1.05/0.44 thf(f1466,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_7 | ~spl15_36 | ~spl15_37 | ~spl15_42)),
% 1.05/0.44 inference(forward_demodulation,[],[f1461,f863])).
% 1.05/0.44 thf(f1467,plain,(
% 1.05/0.44 $false | (~spl15_7 | ~spl15_36 | ~spl15_37 | ~spl15_42)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1466])).
% 1.05/0.44 thf(f1468,plain,(
% 1.05/0.44 ~spl15_7 | ~spl15_36 | ~spl15_37 | ~spl15_42),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1467])).
% 1.05/0.44 thf(f1474,plain,(
% 1.05/0.44 ($false != ((f2 @ $true))) | (~spl15_5 | spl15_10)),
% 1.05/0.44 inference(forward_demodulation,[],[f112,f91])).
% 1.05/0.44 thf(f1485,plain,(
% 1.05/0.44 ($false != ((f2 @ $true))) | (~spl15_13 | spl15_18)),
% 1.05/0.44 inference(forward_demodulation,[],[f148,f127])).
% 1.05/0.44 thf(f1507,plain,(
% 1.05/0.44 $false | (~spl15_5 | spl15_10 | ~spl15_39 | ~spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1474,f687])).
% 1.05/0.44 thf(f1508,plain,(
% 1.05/0.44 ~spl15_5 | spl15_10 | ~spl15_39 | ~spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1507])).
% 1.05/0.44 thf(f1511,plain,(
% 1.05/0.44 $false | (~spl15_13 | spl15_18 | ~spl15_39 | ~spl15_44)),
% 1.05/0.44 inference(forward_subsumption_resolution,[],[f1485,f687])).
% 1.05/0.44 thf(f1512,plain,(
% 1.05/0.44 ~spl15_13 | spl15_18 | ~spl15_39 | ~spl15_44),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1511])).
% 1.05/0.44 thf(f1543,plain,(
% 1.05/0.44 ($true = ((f2 @ $false))) | (~spl15_15 | ~spl15_20)),
% 1.05/0.44 inference(forward_demodulation,[],[f158,f136])).
% 1.05/0.44 thf(f1549,plain,(
% 1.05/0.44 ($true = $false) | (~spl15_11 | ~spl15_14 | ~spl15_15 | ~spl15_20)),
% 1.05/0.44 inference(forward_demodulation,[],[f1543,f672])).
% 1.05/0.44 thf(f1550,plain,(
% 1.05/0.44 $false | (~spl15_11 | ~spl15_14 | ~spl15_15 | ~spl15_20)),
% 1.05/0.44 inference(trivial_inequality_removal,[],[f1549])).
% 1.05/0.44 thf(f1551,plain,(
% 1.05/0.44 ~spl15_11 | ~spl15_14 | ~spl15_15 | ~spl15_20),
% 1.05/0.44 inference(avatar_contradiction_clause,[],[f1550])).
% 1.05/0.44 cnf(s1, plain, spl15_1 | spl15_2, inference(sat_conversion,[],[f78])).
% 1.05/0.44 cnf(s2, plain, spl15_3 | spl15_4, inference(sat_conversion,[],[f87])).
% 1.05/0.44 cnf(s3, plain, spl15_5 | spl15_6, inference(sat_conversion,[],[f96])).
% 1.05/0.44 cnf(s4, plain, spl15_7 | spl15_8, inference(sat_conversion,[],[f105])).
% 1.05/0.44 cnf(s5, plain, spl15_9 | spl15_10, inference(sat_conversion,[],[f114])).
% 1.05/0.44 cnf(s6, plain, spl15_11 | spl15_12, inference(sat_conversion,[],[f123])).
% 1.05/0.44 cnf(s7, plain, spl15_13 | spl15_14, inference(sat_conversion,[],[f132])).
% 1.05/0.44 cnf(s8, plain, spl15_15 | spl15_16, inference(sat_conversion,[],[f141])).
% 1.05/0.44 cnf(s9, plain, spl15_17 | spl15_18, inference(sat_conversion,[],[f150])).
% 1.05/0.44 cnf(s10, plain, spl15_19 | spl15_20, inference(sat_conversion,[],[f159])).
% 1.05/0.44 cnf(s11, plain, spl15_21 | spl15_22, inference(sat_conversion,[],[f168])).
% 1.05/0.44 cnf(s12, plain, spl15_23 | spl15_24, inference(sat_conversion,[],[f177])).
% 1.05/0.44 cnf(s13, plain, spl15_25 | spl15_26, inference(sat_conversion,[],[f186])).
% 1.05/0.44 cnf(s14, plain, spl15_27 | spl15_28, inference(sat_conversion,[],[f195])).
% 1.05/0.44 cnf(s15, plain, spl15_29 | spl15_30, inference(sat_conversion,[],[f204])).
% 1.05/0.44 cnf(s16, plain, spl15_31 | spl15_32, inference(sat_conversion,[],[f213])).
% 1.05/0.44 cnf(s17, plain, spl15_4 | spl15_33, inference(sat_conversion,[],[f218])).
% 1.05/0.44 cnf(s18, plain, spl15_2 | spl15_34, inference(sat_conversion,[],[f223])).
% 1.05/0.44 cnf(s19, plain, spl15_35 | spl15_36, inference(sat_conversion,[],[f232])).
% 1.05/0.44 cnf(s20, plain, spl15_37 | spl15_38, inference(sat_conversion,[],[f241])).
% 1.05/0.44 cnf(s21, plain, spl15_39 | spl15_40, inference(sat_conversion,[],[f250])).
% 1.05/0.44 cnf(s22, plain, spl15_41 | spl15_42, inference(sat_conversion,[],[f259])).
% 1.05/0.44 cnf(s23, plain, spl15_43 | spl15_44, inference(sat_conversion,[],[f268])).
% 1.05/0.44 cnf(s24, plain, spl15_45 | spl15_46, inference(sat_conversion,[],[f277])).
% 1.05/0.44 cnf(s25, plain, spl15_47 | spl15_48, inference(sat_conversion,[],[f286])).
% 1.05/0.44 cnf(s26, plain, spl15_49 | spl15_50, inference(sat_conversion,[],[f295])).
% 1.05/0.44 cnf(s27, plain, spl15_51 | spl15_52, inference(sat_conversion,[],[f304])).
% 1.05/0.44 cnf(s28, plain, spl15_53 | spl15_54, inference(sat_conversion,[],[f313])).
% 1.05/0.44 cnf(s29, plain, spl15_55 | spl15_56, inference(sat_conversion,[],[f322])).
% 1.05/0.44 cnf(s30, plain, spl15_57 | spl15_58, inference(sat_conversion,[],[f331])).
% 1.05/0.44 cnf(s31, plain, spl15_3 | spl15_59, inference(sat_conversion,[],[f336])).
% 1.05/0.44 cnf(s32, plain, spl15_1 | spl15_60, inference(sat_conversion,[],[f341])).
% 1.05/0.44 cnf(s33, plain, ~spl15_2 | ~spl15_4, inference(sat_conversion,[],[f344])).
% 1.05/0.44 cnf(s35, plain, ~spl15_5 | ~spl15_7, inference(sat_conversion,[],[f363])).
% 1.05/0.44 cnf(s37, plain, ~spl15_9 | ~spl15_11, inference(sat_conversion,[],[f372])).
% 1.05/0.44 cnf(s43, plain, ~spl15_21 | ~spl15_23, inference(sat_conversion,[],[f402])).
% 1.05/0.44 cnf(s49, plain, ~spl15_35 | ~spl15_37, inference(sat_conversion,[],[f433])).
% 1.05/0.44 cnf(s53, plain, ~spl15_43 | ~spl15_45, inference(sat_conversion,[],[f453])).
% 1.05/0.44 cnf(s55, plain, ~spl15_47 | ~spl15_49, inference(sat_conversion,[],[f463])).
% 1.05/0.44 cnf(s60, plain, ~spl15_23 | ~spl15_26 | ~spl15_57 | ~spl15_60, inference(sat_conversion,[],[f490])).
% 1.05/0.44 cnf(s61, plain, ~spl15_31 | ~spl15_33 | ~spl15_57 | ~spl15_60, inference(sat_conversion,[],[f497])).
% 1.05/0.44 cnf(s62, plain, ~spl15_23 | spl15_26 | ~spl15_31 | ~spl15_33, inference(sat_conversion,[],[f499])).
% 1.05/0.44 cnf(s65, plain, ~spl15_23 | ~spl15_26 | ~spl15_28, inference(sat_conversion,[],[f512])).
% 1.05/0.44 cnf(s66, plain, ~spl15_30 | ~spl15_32, inference(sat_conversion,[],[f515])).
% 1.05/0.44 cnf(s67, plain, ~spl15_19 | ~spl15_22 | ~spl15_53 | ~spl15_58, inference(sat_conversion,[],[f518])).
% 1.05/0.44 cnf(s70, plain, ~spl15_23 | ~spl15_26 | ~spl15_27 | spl15_30, inference(sat_conversion,[],[f531])).
% 1.05/0.44 cnf(s71, plain, ~spl15_23 | ~spl15_26 | ~spl15_27 | ~spl15_32, inference(sat_conversion,[],[f534])).
% 1.05/0.44 cnf(s72, plain, ~spl15_56 | ~spl15_58, inference(sat_conversion,[],[f541])).
% 1.05/0.44 cnf(s73, plain, ~spl15_18 | ~spl15_20, inference(sat_conversion,[],[f544])).
% 1.05/0.44 cnf(s74, plain, ~spl15_45 | ~spl15_48 | ~spl15_49 | ~spl15_54, inference(sat_conversion,[],[f548])).
% 1.05/0.44 cnf(s75, plain, ~spl15_52 | ~spl15_54, inference(sat_conversion,[],[f552])).
% 1.05/0.44 cnf(s77, plain, ~spl15_48 | ~spl15_50, inference(sat_conversion,[],[f559])).
% 1.05/0.44 cnf(s78, plain, ~spl15_41 | ~spl15_44 | ~spl15_46, inference(sat_conversion,[],[f562])).
% 1.05/0.44 cnf(s80, plain, ~spl15_5 | ~spl15_8 | ~spl15_36 | ~spl15_37 | ~spl15_40, inference(sat_conversion,[],[f606])).
% 1.05/0.44 cnf(s86, plain, ~spl15_5 | ~spl15_9 | ~spl15_12 | ~spl15_14, inference(sat_conversion,[],[f641])).
% 1.05/0.44 cnf(s87, plain, ~spl15_9 | ~spl15_14 | ~spl15_39 | ~spl15_46, inference(sat_conversion,[],[f653])).
% 1.05/0.44 cnf(s88, plain, ~spl15_9 | ~spl15_14 | ~spl15_39 | spl15_44, inference(sat_conversion,[],[f655])).
% 1.05/0.44 cnf(s90, plain, ~spl15_17 | ~spl15_22 | ~spl15_43 | spl15_48, inference(sat_conversion,[],[f683])).
% 1.05/0.44 cnf(s94, plain, ~spl15_5 | ~spl15_10 | ~spl15_12, inference(sat_conversion,[],[f759])).
% 1.05/0.44 cnf(s95, plain, ~spl15_5 | ~spl15_10 | ~spl15_39 | ~spl15_46, inference(sat_conversion,[],[f764])).
% 1.05/0.44 cnf(s96, plain, spl15_5 | spl15_7, inference(sat_conversion,[],[f766])).
% 1.05/0.44 cnf(s99, plain, ~spl15_11 | ~spl15_14 | ~spl15_41 | ~spl15_46, inference(sat_conversion,[],[f781])).
% 1.05/0.44 cnf(s100, plain, ~spl15_7 | ~spl15_10 | ~spl15_41 | spl15_44, inference(sat_conversion,[],[f792])).
% 1.05/0.44 cnf(s101, plain, ~spl15_7 | ~spl15_10 | ~spl15_41 | ~spl15_46, inference(sat_conversion,[],[f795])).
% 1.05/0.44 cnf(s102, plain, ~spl15_7 | ~spl15_10 | ~spl15_11 | spl15_14, inference(sat_conversion,[],[f797])).
% 1.05/0.44 cnf(s103, plain, ~spl15_7 | ~spl15_10 | ~spl15_11 | ~spl15_16, inference(sat_conversion,[],[f800])).
% 1.05/0.44 cnf(s104, plain, spl15_13 | spl15_15, inference(sat_conversion,[],[f802])).
% 1.05/0.44 cnf(s105, plain, ~spl15_36 | ~spl15_38, inference(sat_conversion,[],[f808])).
% 1.05/0.44 cnf(s109, plain, ~spl15_15 | ~spl15_18 | ~spl15_41 | spl15_44, inference(sat_conversion,[],[f830])).
% 1.05/0.44 cnf(s112, plain, ~spl15_9 | ~spl15_13 | spl15_14 | ~spl15_18, inference(sat_conversion,[],[f842])).
% 1.05/0.44 cnf(s113, plain, ~spl15_9 | ~spl15_13 | ~spl15_16 | spl15_20, inference(sat_conversion,[],[f844])).
% 1.05/0.44 cnf(s116, plain, ~spl15_21 | ~spl15_26 | ~spl15_55 | ~spl15_60, inference(sat_conversion,[],[f898])).
% 1.05/0.44 cnf(s117, plain, ~spl15_21 | ~spl15_26 | ~spl15_28, inference(sat_conversion,[],[f903])).
% 1.05/0.44 cnf(s119, plain, ~spl15_1 | ~spl15_3, inference(sat_conversion,[],[f914])).
% 1.05/0.44 cnf(s123, plain, ~spl15_21 | ~spl15_25 | spl15_26 | ~spl15_30, inference(sat_conversion,[],[f936])).
% 1.05/0.44 cnf(s128, plain, ~spl15_27 | ~spl15_30 | ~spl15_31 | ~spl15_34, inference(sat_conversion,[],[f962])).
% 1.05/0.44 cnf(s129, plain, ~spl15_17 | ~spl15_22 | ~spl15_51 | ~spl15_58, inference(sat_conversion,[],[f974])).
% 1.05/0.44 cnf(s130, plain, ~spl15_17 | ~spl15_22 | ~spl15_24, inference(sat_conversion,[],[f978])).
% 1.05/0.44 cnf(s132, plain, ~spl15_17 | ~spl15_22 | spl15_53 | ~spl15_58, inference(sat_conversion,[],[f987])).
% 1.05/0.44 cnf(s134, plain, ~spl15_49 | ~spl15_52 | ~spl15_53 | ~spl15_58, inference(sat_conversion,[],[f995])).
% 1.05/0.44 cnf(s136, plain, ~spl15_7 | ~spl15_12 | ~spl15_41 | ~spl15_44, inference(sat_conversion,[],[f1009])).
% 1.05/0.44 cnf(s137, plain, ~spl15_7 | spl15_10 | ~spl15_41 | ~spl15_44, inference(sat_conversion,[],[f1011])).
% 1.05/0.44 cnf(s139, plain, ~spl15_5 | ~spl15_35 | spl15_36 | ~spl15_40, inference(sat_conversion,[],[f1028])).
% 1.05/0.44 cnf(s142, plain, spl15_9 | spl15_11, inference(sat_conversion,[],[f1034])).
% 1.05/0.44 cnf(s149, plain, ~spl15_6 | ~spl15_7 | ~spl15_38 | ~spl15_61, inference(sat_conversion,[],[f1061])).
% 1.05/0.44 cnf(s150, plain, spl15_17 | spl15_19, inference(sat_conversion,[],[f1063])).
% 1.05/0.44 cnf(s152, plain, ~spl15_29 | ~spl15_34 | ~spl15_55 | ~spl15_59, inference(sat_conversion,[],[f1090])).
% 1.05/0.44 cnf(s154, plain, ~spl15_21 | ~spl15_26 | ~spl15_29 | ~spl15_34, inference(sat_conversion,[],[f1103])).
% 1.05/0.44 cnf(s155, plain, ~spl15_45 | ~spl15_50 | ~spl15_53 | spl15_58, inference(sat_conversion,[],[f1105])).
% 1.05/0.44 cnf(s158, plain, ~spl15_47 | ~spl15_51 | spl15_52 | ~spl15_56, inference(sat_conversion,[],[f1122])).
% 1.05/0.44 cnf(s159, plain, ~spl15_47 | ~spl15_51 | ~spl15_54 | spl15_58, inference(sat_conversion,[],[f1124])).
% 1.05/0.44 cnf(s160, plain, ~spl15_19 | spl15_22 | ~spl15_45 | ~spl15_48, inference(sat_conversion,[],[f1134])).
% 1.05/0.44 cnf(s161, plain, ~spl15_19 | ~spl15_24 | ~spl15_45 | ~spl15_48, inference(sat_conversion,[],[f1137])).
% 1.05/0.44 cnf(s164, plain, ~spl15_17 | spl15_22 | ~spl15_43 | ~spl15_48, inference(sat_conversion,[],[f1170])).
% 1.05/0.44 cnf(s166, plain, spl15_29 | spl15_31, inference(sat_conversion,[],[f1181])).
% 1.05/0.44 cnf(s168, plain, ~spl15_23 | spl15_26 | ~spl15_57 | ~spl15_59, inference(sat_conversion,[],[f1194])).
% 1.05/0.44 cnf(s175, plain, ~spl15_19 | ~spl15_22 | ~spl15_45 | spl15_48, inference(sat_conversion,[],[f1239])).
% 1.05/0.44 cnf(s176, plain, ~spl15_19 | ~spl15_22 | ~spl15_45 | ~spl15_50, inference(sat_conversion,[],[f1242])).
% 1.05/0.44 cnf(s178, plain, ~spl15_25 | ~spl15_29 | spl15_30 | ~spl15_33, inference(sat_conversion,[],[f1263])).
% 1.05/0.44 cnf(s180, plain, ~spl15_21 | spl15_26 | ~spl15_29 | ~spl15_33, inference(sat_conversion,[],[f1267])).
% 1.05/0.44 cnf(s183, plain, ~spl15_17 | spl15_22 | ~spl15_47 | ~spl15_52, inference(sat_conversion,[],[f1305])).
% 1.05/0.44 cnf(s184, plain, ~spl15_17 | ~spl15_24 | ~spl15_47 | spl15_54, inference(sat_conversion,[],[f1307])).
% 1.05/0.44 cnf(s197, plain, ~spl15_40 | ~spl15_42, inference(sat_conversion,[],[f1340])).
% 1.05/0.44 cnf(s209, plain, ~spl15_19 | ~spl15_22 | ~spl15_49 | spl15_52, inference(sat_conversion,[],[f1394])).
% 1.05/0.44 cnf(s210, plain, ~spl15_19 | ~spl15_22 | ~spl15_49 | ~spl15_54, inference(sat_conversion,[],[f1397])).
% 1.05/0.44 cnf(s212, plain, ~spl15_6 | ~spl15_35 | spl15_40 | spl15_61, inference(sat_conversion,[],[f1451])).
% 1.05/0.44 cnf(s213, plain, spl15_35 | spl15_37, inference(sat_conversion,[],[f1452])).
% 1.05/0.44 cnf(s217, plain, ~spl15_7 | ~spl15_36 | ~spl15_37 | ~spl15_42, inference(sat_conversion,[],[f1468])).
% 1.05/0.44 cnf(s220, plain, ~spl15_5 | spl15_10 | ~spl15_39 | ~spl15_44, inference(sat_conversion,[],[f1508])).
% 1.05/0.44 cnf(s222, plain, ~spl15_13 | spl15_18 | ~spl15_39 | ~spl15_44, inference(sat_conversion,[],[f1512])).
% 1.05/0.44 cnf(s235, plain, ~spl15_11 | ~spl15_14 | ~spl15_15 | ~spl15_20, inference(sat_conversion,[],[f1551])).
% 1.05/0.44 cnf(s237, plain, spl15_35 | ~spl15_42 | ~spl15_7, inference(rat,[],[s217,s19,s213])).
% 1.05/0.44 cnf(s238, plain, ~spl15_42 | spl15_5, inference(rat,[],[s20,s149,s49,s212,s237,s197,s96,s3])).
% 1.05/0.44 cnf(s239, plain, ~spl15_22 | ~spl15_45 | ~spl15_19 | spl15_1, inference(rat,[],[s66,s178,s13,s16,s166,s60,s61,s30,s134,s12,s28,s209,s161,s74,s26,s175,s176,s32,s17,s33,s1])).
% 1.05/0.44 cnf(s240, plain, spl15_58 | ~spl15_47 | ~spl15_45, inference(rat,[],[s27,s159,s75,s28,s155,s26,s55])).
% 1.05/0.44 cnf(s241, plain, spl15_26 | ~spl15_21 | ~spl15_33, inference(rat,[],[s15,s123,s13,s180])).
% 1.05/0.44 cnf(s242, plain, spl15_9 | spl15_5 | spl15_1, inference(rat,[],[s241,s116,s29,s72,s240,s25,s160,s11,s239,s24,s99,s10,s235,s8,s103,s102,s5,s142,s32,s17,s33,s1,s96,s22,s238])).
% 1.05/0.44 cnf(s243, plain, ~spl15_17 | ~spl15_26 | ~spl15_22 | ~spl15_43 | ~spl15_60, inference(rat,[],[s134,s27,s132,s129,s30,s60,s26,s12,s77,s130,s90])).
% 1.05/0.44 cnf(s244, plain, ~spl15_18 | spl15_44 | ~spl15_9 | ~spl15_41, inference(rat,[],[s113,s8,s104,s109,s73])).
% 1.05/0.44 cnf(s245, plain, spl15_26 | ~spl15_23 | ~spl15_33, inference(rat,[],[s66,s178,s16,s166,s13,s62])).
% 1.05/0.44 cnf(s246, plain, ~spl15_22 | spl15_5 | spl15_1, inference(rat,[],[s245,s12,s243,s130,s32,s17,s33,s1,s23,s9,s244,s136,s6,s37,s96,s242,s22,s238])).
% 1.05/0.44 cnf(s247, plain, spl15_5 | spl15_1, inference(rat,[],[s158,s27,s29,s183,s116,s25,s241,s164,s11,s246,s9,s244,s23,s136,s6,s37,s242,s22,s238,s96,s32,s17,s33,s1])).
% 1.05/0.44 cnf(s248, plain, ~spl15_11 | ~spl15_22 | ~spl15_39 | spl15_1, inference(rat,[],[s235,s7,s104,s222,s73,s10,s23,s239,s53,s24,s95,s5,s37,s247])).
% 1.05/0.44 cnf(s249, plain, ~spl15_22 | ~spl15_39 | ~spl15_26 | spl15_1, inference(rat,[],[s9,s243,s112,s23,s7,s220,s86,s94,s6,s142,s248,s32,s247])).
% 1.05/0.44 cnf(s250, plain, ~spl15_11 | spl15_58 | ~spl15_24 | ~spl15_39 | ~spl15_5, inference(rat,[],[s235,s7,s104,s222,s73,s10,s161,s25,s23,s240,s53,s24,s95,s5,s37])).
% 1.05/0.44 cnf(s251, plain, ~spl15_39 | ~spl15_26 | spl15_1, inference(rat,[],[s27,s159,s183,s184,s25,s164,s9,s112,s23,s7,s220,s86,s94,s6,s142,s250,s72,s29,s12,s116,s43,s11,s249,s32,s247])).
% 1.05/0.44 cnf(s252, plain, spl15_35 | ~spl15_40 | ~spl15_5, inference(rat,[],[s80,s19,s213,s4,s35])).
% 1.05/0.44 cnf(s253, plain, ~spl15_40 | ~spl15_5, inference(rat,[],[s105,s20,s139,s49,s252])).
% 1.05/0.44 cnf(s254, plain, ~spl15_18 | spl15_14 | ~spl15_9, inference(rat,[],[s7,s112])).
% 1.05/0.44 cnf(s255, plain, spl15_1, inference(rat,[],[s254,s86,s9,s6,s142,s130,s248,s12,s11,s245,s241,s251,s21,s253,s247,s17,s33,s1])).
% 1.05/0.44 cnf(s256, plain, ~spl15_3, inference(rat,[],[s119,s255])).
% 1.05/0.44 cnf(s257, plain, spl15_59, inference(rat,[],[s31,s256])).
% 1.05/0.44 cnf(s258, plain, spl15_4, inference(rat,[],[s2,s256])).
% 1.05/0.44 cnf(s259, plain, ~spl15_2, inference(rat,[],[s33,s258])).
% 1.05/0.44 cnf(s260, plain, spl15_34, inference(rat,[],[s18,s259])).
% 1.05/0.44 cnf(s262, plain, ~spl15_27 | ~spl15_23 | ~spl15_26, inference(rat,[],[s128,s16,s70,s71,s260])).
% 1.05/0.44 cnf(s263, plain, ~spl15_23 | ~spl15_26, inference(rat,[],[s262,s14,s65])).
% 1.05/0.44 cnf(s264, plain, ~spl15_45 | ~spl15_22 | ~spl15_24, inference(rat,[],[s161,s175,s150,s130])).
% 1.05/0.44 cnf(s265, plain, ~spl15_22 | ~spl15_24 | spl15_5, inference(rat,[],[s244,s5,s78,s101,s24,s264,s9,s130,s96,s22,s238])).
% 1.05/0.44 cnf(s266, plain, ~spl15_21 | ~spl15_26, inference(rat,[],[s128,s15,s166,s14,s154,s117,s260])).
% 1.05/0.44 cnf(s267, plain, ~spl15_26 | spl15_5, inference(rat,[],[s266,s11,s265,s12,s263])).
% 1.05/0.44 cnf(s268, plain, ~spl15_10 | ~spl15_22 | spl15_5, inference(rat,[],[s210,s26,s28,s176,s67,s10,s235,s8,s103,s102,s6,s24,s136,s101,s100,s96,s22,s238,s30,s168,s12,s265,s267,s257])).
% 1.05/0.44 cnf(s269, plain, ~spl15_22 | spl15_5, inference(rat,[],[s134,s26,s27,s77,s132,s129,s90,s9,s244,s23,s5,s137,s268,s30,s168,s12,s265,s96,s22,s238,s267,s257])).
% 1.05/0.44 cnf(s270, plain, ~spl15_10 | spl15_5, inference(rat,[],[s10,s235,s161,s8,s25,s103,s102,s240,s6,s24,s136,s101,s100,s96,s22,s238,s12,s43,s72,s29,s152,s15,s123,s11,s269,s13,s267,s257,s260])).
% 1.05/0.44 cnf(s271, plain, spl15_5, inference(rat,[],[s27,s159,s183,s184,s25,s164,s9,s244,s23,s5,s137,s270,s72,s29,s152,s15,s12,s123,s43,s11,s269,s13,s267,s22,s238,s96,s260,s257])).
% 1.05/0.44 cnf(s273, plain, ~spl15_40, inference(rat,[],[s253,s271])).
% 1.05/0.44 cnf(s275, plain, spl15_39, inference(rat,[],[s21,s273])).
% 1.05/0.44 cnf(s279, plain, ~spl15_24 | ~spl15_22, inference(rat,[],[s87,s254,s5,s95,s24,s9,s264,s130,s271,s275])).
% 1.05/0.44 cnf(s280, plain, ~spl15_26, inference(rat,[],[s279,s11,s12,s266,s263])).
% 1.05/0.44 cnf(s281, plain, spl15_25, inference(rat,[],[s13,s280])).
% 1.05/0.44 cnf(s284, plain, ~spl15_19 | ~spl15_45 | ~spl15_22, inference(rat,[],[s210,s28,s26,s67,s176,s30,s168,s12,s279,s257,s280])).
% 1.05/0.44 cnf(s285, plain, ~spl15_10 | ~spl15_22, inference(rat,[],[s235,s7,s104,s222,s73,s10,s284,s23,s53,s6,s24,s94,s95,s275,s271])).
% 1.05/0.44 cnf(s286, plain, ~spl15_22, inference(rat,[],[s134,s26,s27,s77,s132,s129,s90,s9,s254,s88,s23,s220,s5,s285,s30,s168,s12,s279,s275,s271,s280,s257])).
% 1.05/0.44 cnf(s287, plain, spl15_21, inference(rat,[],[s11,s286])).
% 1.05/0.44 cnf(s288, plain, ~spl15_23, inference(rat,[],[s43,s287])).
% 1.05/0.44 cnf(s289, plain, ~spl15_30, inference(rat,[],[s123,s281,s280,s287])).
% 1.05/0.44 cnf(s290, plain, spl15_24, inference(rat,[],[s12,s288])).
% 1.05/0.44 cnf(s291, plain, spl15_29, inference(rat,[],[s15,s289])).
% 1.05/0.44 cnf(s292, plain, ~spl15_55, inference(rat,[],[s152,s257,s260,s291])).
% 1.05/0.44 cnf(s294, plain, spl15_56, inference(rat,[],[s29,s292])).
% 1.05/0.44 cnf(s296, plain, ~spl15_58, inference(rat,[],[s72,s294])).
% 1.05/0.44 cnf(s298, plain, ~spl15_11, inference(rat,[],[s250,s271,s275,s290,s296])).
% 1.05/0.44 cnf(s299, plain, spl15_9, inference(rat,[],[s142,s298])).
% 1.05/0.44 cnf(s300, plain, spl15_12, inference(rat,[],[s6,s298])).
% 1.05/0.44 cnf(s301, plain, ~spl15_10, inference(rat,[],[s94,s271,s300])).
% 1.05/0.44 cnf(s302, plain, ~spl15_14, inference(rat,[],[s86,s299,s271,s300])).
% 1.05/0.44 cnf(s303, plain, ~spl15_44, inference(rat,[],[s220,s275,s271,s301])).
% 1.05/0.44 cnf(s305, plain, ~spl15_18, inference(rat,[],[s254,s299,s302])).
% 1.05/0.44 cnf(s306, plain, spl15_43, inference(rat,[],[s23,s303])).
% 1.05/0.44 cnf(s308, plain, spl15_17, inference(rat,[],[s9,s305])).
% 1.05/0.44 cnf(s312, plain, ~spl15_48, inference(rat,[],[s164,s286,s306,s308])).
% 1.05/0.44 cnf(s316, plain, spl15_47, inference(rat,[],[s25,s312])).
% 1.05/0.44 cnf(s318, plain, spl15_54, inference(rat,[],[s184,s290,s308,s316])).
% 1.05/0.44 cnf(s319, plain, ~spl15_52, inference(rat,[],[s183,s286,s308,s316])).
% 1.05/0.44 cnf(s320, plain, ~spl15_51, inference(rat,[],[s159,s316,s296,s318])).
% 1.05/0.44 cnf(s321, plain, $false, inference(rat,[],[s27,s319,s320])).
% 1.05/0.45 thf(f1555,plain,(
% 1.05/0.45 $false),
% 1.05/0.45 inference(avatar_sat_refutation,[],[s321])).
% 1.05/0.45 % SZS output end Proof for theBenchmark
% 1.05/0.45 % (3447956)------------------------------
% 1.05/0.45 % (3447956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.05/0.45 % (3447956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.05/0.45 % (3447956)CaDiCaL version: 2.1.3
% 1.05/0.45 % (3447956)Termination reason: Refutation
% 1.05/0.45 % (3447956)Time elapsed: 0.044 s
% 1.05/0.45 % (3447956)Peak memory usage: 13 MB
% 1.05/0.45 % (3447956)Instructions burned: 60 (million)
% 1.05/0.45 % (3447925)Success in time 0.205 s
% 1.05/0.45 % Vampire exiting
%------------------------------------------------------------------------------