%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n005.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:48:08 AM UTC 2026
% Result : Theorem 0.21s 0.37s
% Output : Refutation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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 THM
% 0.08/0.19 % Computer : n005.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:10:46 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.37 % (1947174)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.37 % (1947180)lrs+10_16_si=on:nwc=1.5:random_seed=877653303:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.37 % (1947180)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947180)------------------------------
% 0.21/0.37 % (1947180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947180)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947180)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947180)Time elapsed: 0.001 s
% 0.21/0.37 % (1947180)Peak memory usage: 12 MB
% 0.21/0.37 % (1947180)Instructions burned: 1 (million)
% 0.21/0.37 % (1947180)------------------------------
% 0.21/0.37 % (1947180)------------------------------
% 0.21/0.37 % (1947179)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3962544820:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.37 % (1947181)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4038765044:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.37 % (1947181)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947181)------------------------------
% 0.21/0.37 % (1947181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947181)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947181)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947181)Time elapsed: 0.001 s
% 0.21/0.37 % (1947179)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947179)------------------------------
% 0.21/0.37 % (1947179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947181)Peak memory usage: 12 MB
% 0.21/0.37 % (1947179)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947179)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947179)Time elapsed: 0.001 s
% 0.21/0.37 % (1947179)Peak memory usage: 12 MB
% 0.21/0.37 % (1947179)Instructions burned: 1 (million)
% 0.21/0.37 % (1947181)------------------------------
% 0.21/0.37 % (1947181)------------------------------
% 0.21/0.37 % (1947179)------------------------------
% 0.21/0.37 % (1947179)------------------------------
% 0.21/0.37 % (1947187)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1405588905:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.37 % (1947187)Instruction limit reached!
% 0.21/0.37 % (1947187)------------------------------
% 0.21/0.37 % (1947187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947187)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947187)Termination reason: Instruction limit
% 0.21/0.37 % (1947187)Termination phase: Saturation
% 0.21/0.37 % (1947187)Time elapsed: 0.001 s
% 0.21/0.37 % (1947187)Peak memory usage: 12 MB
% 0.21/0.37 % (1947187)Instructions burned: 2 (million)
% 0.21/0.37 % (1947182)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2550482300:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.37 % (1947193)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1481068942:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.21/0.37 % (1947191)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.37 % (1947191)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2943373332:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.37 % (1947193)Instruction limit reached!
% 0.21/0.37 % (1947193)------------------------------
% 0.21/0.37 % (1947193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947193)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947193)Termination reason: Instruction limit
% 0.21/0.37 % (1947193)Termination phase: Saturation
% 0.21/0.37 % (1947193)Time elapsed: 0.004 s
% 0.21/0.37 % (1947193)Peak memory usage: 12 MB
% 0.21/0.37 % (1947193)Instructions burned: 12 (million)
% 0.21/0.37 % (1947190)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1698473979:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.37 % (1947191)Instruction limit reached!
% 0.21/0.37 % (1947191)------------------------------
% 0.21/0.37 % (1947191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947191)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947191)Termination reason: Instruction limit
% 0.21/0.37 % (1947191)Termination phase: Saturation
% 0.21/0.37 % (1947191)Time elapsed: 0.005 s
% 0.21/0.37 % (1947191)Peak memory usage: 12 MB
% 0.21/0.37 % (1947191)Instructions burned: 9 (million)
% 0.21/0.37 % (1947190)Instruction limit reached!
% 0.21/0.37 % (1947190)------------------------------
% 0.21/0.37 % (1947190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947190)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947190)Termination reason: Instruction limit
% 0.21/0.37 % (1947190)Termination phase: Saturation
% 0.21/0.37 % (1947190)Time elapsed: 0.005 s
% 0.21/0.37 % (1947190)Peak memory usage: 11 MB
% 0.21/0.37 % (1947190)Instructions burned: 7 (million)
% 0.21/0.37 % (1947198)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.37 % (1947198)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.37 % (1947185)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.37 % (1947185)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.37 % (1947198)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3396808829:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.21/0.37 % (1947185)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2893795889:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.37 % (1947183)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1699005939:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.37 % (1947184)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3923584411:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.37 % (1947183)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947183)------------------------------
% 0.21/0.37 % (1947183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947183)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947183)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947183)Time elapsed: 0.003 s
% 0.21/0.37 % (1947183)Peak memory usage: 11 MB
% 0.21/0.37 % (1947183)Instructions burned: 2 (million)
% 0.21/0.37 % (1947198)Instruction limit reached!
% 0.21/0.37 % (1947198)------------------------------
% 0.21/0.37 % (1947198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947198)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947198)Termination reason: Instruction limit
% 0.21/0.37 % (1947198)Termination phase: Saturation
% 0.21/0.37 % (1947198)Time elapsed: 0.008 s
% 0.21/0.37 % (1947198)Peak memory usage: 12 MB
% 0.21/0.37 % (1947198)Instructions burned: 31 (million)
% 0.21/0.37 % (1947183)------------------------------
% 0.21/0.37 % (1947183)------------------------------
% 0.21/0.37 % (1947199)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3644653142:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.21/0.37 % (1947200)lrs+10_1_si=on:cs=on:random_seed=1936293395:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.21/0.37 % (1947206)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=252141451:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.21/0.37 % (1947206)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947206)------------------------------
% 0.21/0.37 % (1947206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947206)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947206)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947206)Time elapsed: 0.0000 s
% 0.21/0.37 % (1947206)Peak memory usage: 12 MB
% 0.21/0.37 % (1947206)Instructions burned: 1 (million)
% 0.21/0.37 % (1947206)------------------------------
% 0.21/0.37 % (1947206)------------------------------
% 0.21/0.37 % (1947199)Refutation not found, incomplete strategy
% 0.21/0.37 % (1947199)------------------------------
% 0.21/0.37 % (1947199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947199)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947199)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (1947199)Time elapsed: 0.006 s
% 0.21/0.37 % (1947199)Peak memory usage: 12 MB
% 0.21/0.37 % (1947199)Instructions burned: 3 (million)
% 0.21/0.37 % (1947199)------------------------------
% 0.21/0.37 % (1947199)------------------------------
% 0.21/0.37 % (1947200)Instruction limit reached!
% 0.21/0.37 % (1947200)------------------------------
% 0.21/0.37 % (1947200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (1947200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (1947200)CaDiCaL version: 2.1.3
% 0.21/0.37 % (1947200)Termination reason: Instruction limit
% 0.21/0.37 % (1947200)Termination phase: Saturation
% 0.21/0.37 % (1947200)Time elapsed: 0.008 s
% 0.21/0.37 % (1947200)Peak memory usage: 11 MB
% 0.21/0.37 % (1947200)Instructions burned: 11 (million)
% 0.21/0.37 % (1947210)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2582038507:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.21/0.37 % (1947205)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.21/0.37 % (1947185) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1947174-1947185"...
% 0.21/0.37 % (1947205)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1103461285:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.37 % (1947185)...printing done.
% 0.21/0.37 % (1947185)Refutation found. Thanks to Tanya!
% 0.21/0.37 % SZS status Theorem for theBenchmark
% 0.21/0.37 % SZS output start Proof for theBenchmark
% 0.21/0.37 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.37 thf(func_def_0, type, x: $o).
% 0.21/0.37 thf(func_def_1, type, f0: ($o > $o)).
% 0.21/0.37 thf(func_def_2, type, f1: ($o > $o)).
% 0.21/0.37 thf(func_def_3, type, f2: ($o > $o)).
% 0.21/0.37 thf(func_def_4, type, f3: ($o > $o)).
% 0.21/0.37 thf(func_def_8, type, sF0: $o).
% 0.21/0.37 thf(func_def_9, type, sF1: $o).
% 0.21/0.37 thf(func_def_10, type, sF2: $o).
% 0.21/0.37 thf(func_def_11, type, sF3: $o).
% 0.21/0.37 thf(func_def_12, type, sF4: $o).
% 0.21/0.37 thf(func_def_13, type, sF5: $o).
% 0.21/0.37 thf(func_def_14, type, sF6: $o).
% 0.21/0.37 thf(func_def_15, type, sF7: $o).
% 0.21/0.37 thf(func_def_16, type, sF8: $o).
% 0.21/0.37 thf(func_def_17, type, sF9: $o).
% 0.21/0.37 thf(func_def_18, type, sF10: $o).
% 0.21/0.37 thf(func_def_19, type, sF11: $o).
% 0.21/0.37 thf(func_def_20, type, sF12: $o).
% 0.21/0.37 thf(func_def_21, type, sF13: $o).
% 0.21/0.37 thf(func_def_22, type, sF14: $o).
% 0.21/0.37 thf(f1,conjecture,(
% 0.21/0.37 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 0.21/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski4)).
% 0.21/0.37 thf(f2,negated_conjecture,(
% 0.21/0.37 ~ (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 0.21/0.37 inference(negated_conjecture,[status(cth)],[f1])).
% 0.21/0.37 thf(f3,plain,(
% 0.21/0.37 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 0.21/0.37 inference(flattening,[],[f2])).
% 0.21/0.37 thf(f4,plain,(
% 0.21/0.37 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ x))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ x))))))))))),
% 0.21/0.37 inference(cnf_transformation,[],[f3])).
% 0.21/0.37 thf(f6,definition,(
% 0.21/0.37 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.21/0.37 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.21/0.37 thf(f7,definition,(
% 0.21/0.37 (sF0 = ((f3 @ x)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.21/0.37 thf(f8,plain,(
% 0.21/0.37 (((f3 @ x)) = sF0)),
% 0.21/0.37 inference(reorient_equations,[],[f7])).
% 0.21/0.37 thf(f9,definition,(
% 0.21/0.37 (sF1 = ((f2 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.21/0.37 thf(f10,definition,(
% 0.21/0.37 (sF2 = ((f2 @ sF1)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.21/0.37 thf(f11,plain,(
% 0.21/0.37 (((f2 @ sF1)) = sF2)),
% 0.21/0.37 inference(reorient_equations,[],[f10])).
% 0.21/0.37 thf(f12,definition,(
% 0.21/0.37 (sF3 = ((f2 @ sF2)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.21/0.37 thf(f13,definition,(
% 0.21/0.37 (sF4 = ((f1 @ sF3)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.21/0.37 thf(f14,plain,(
% 0.21/0.37 (((f1 @ sF3)) = sF4)),
% 0.21/0.37 inference(reorient_equations,[],[f13])).
% 0.21/0.37 thf(f15,definition,(
% 0.21/0.37 (sF5 = ((f0 @ sF4)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 0.21/0.37 thf(f16,definition,(
% 0.21/0.37 (sF6 = ((f0 @ sF5)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.21/0.37 thf(f17,plain,(
% 0.21/0.37 (((f0 @ sF5)) = sF6)),
% 0.21/0.37 inference(reorient_equations,[],[f16])).
% 0.21/0.37 thf(f18,definition,(
% 0.21/0.37 (sF7 = ((f0 @ sF6)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 0.21/0.37 thf(f19,definition,(
% 0.21/0.37 (sF8 = ((f3 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 0.21/0.37 thf(f20,definition,(
% 0.21/0.37 (sF9 = ((f3 @ sF8)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.21/0.37 thf(f21,plain,(
% 0.21/0.37 (((f3 @ sF8)) = sF9)),
% 0.21/0.37 inference(reorient_equations,[],[f20])).
% 0.21/0.37 thf(f22,definition,(
% 0.21/0.37 (sF10 = ((f2 @ sF9)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.21/0.37 thf(f23,plain,(
% 0.21/0.37 (((f2 @ sF9)) = sF10)),
% 0.21/0.37 inference(reorient_equations,[],[f22])).
% 0.21/0.37 thf(f24,definition,(
% 0.21/0.37 (sF11 = ((f1 @ sF10)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 0.21/0.37 thf(f25,definition,(
% 0.21/0.37 (sF12 = ((f1 @ sF11)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.21/0.37 thf(f26,plain,(
% 0.21/0.37 (((f1 @ sF11)) = sF12)),
% 0.21/0.37 inference(reorient_equations,[],[f25])).
% 0.21/0.37 thf(f27,definition,(
% 0.21/0.37 (sF13 = ((f1 @ sF12)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.21/0.37 thf(f28,plain,(
% 0.21/0.37 (((f1 @ sF12)) = sF13)),
% 0.21/0.37 inference(reorient_equations,[],[f27])).
% 0.21/0.37 thf(f29,definition,(
% 0.21/0.37 (sF14 = ((f0 @ sF13)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.21/0.37 thf(f30,plain,(
% 0.21/0.37 (((f0 @ sF13)) = sF14)),
% 0.21/0.37 inference(reorient_equations,[],[f29])).
% 0.21/0.37 thf(f31,plain,(
% 0.21/0.37 (sF7 != sF14)),
% 0.21/0.37 inference(definition_folding,[],[f4,f30,f28,f26,f24,f23,f21,f19,f8,f18,f17,f15,f14,f12,f11,f9,f8])).
% 0.21/0.37 thf(f32,plain,(
% 0.21/0.37 ($false = ((f0 @ sF6))) | (sF7 = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f18])).
% 0.21/0.37 thf(f33,plain,(
% 0.21/0.37 (((f0 @ sF6)) = $true) | (sF7 = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f18])).
% 0.21/0.37 thf(f34,plain,(
% 0.21/0.37 (((f1 @ sF3)) = $true) | ($false = sF4)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f14])).
% 0.21/0.37 thf(f35,plain,(
% 0.21/0.37 (sF4 = $true) | ($false = ((f1 @ sF3)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f14])).
% 0.21/0.37 thf(f36,plain,(
% 0.21/0.37 (((f3 @ sF8)) = $true) | ($false = sF9)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f21])).
% 0.21/0.37 thf(f37,plain,(
% 0.21/0.37 (((f3 @ sF8)) = $false) | (sF9 = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f21])).
% 0.21/0.37 thf(f38,plain,(
% 0.21/0.37 ($true = sF14) | (sF7 = $true)),
% 0.21/0.37 inference(xor_proxy_clausification,[],[f31])).
% 0.21/0.37 thf(f39,plain,(
% 0.21/0.37 ($false = sF14) | (sF7 = $false)),
% 0.21/0.37 inference(xor_proxy_clausification,[],[f31])).
% 0.21/0.37 thf(f40,plain,(
% 0.21/0.37 ($true = ((f2 @ sF1))) | ($false = sF2)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f11])).
% 0.21/0.37 thf(f41,plain,(
% 0.21/0.37 ($false = ((f2 @ sF1))) | ($true = sF2)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f11])).
% 0.21/0.37 thf(f42,plain,(
% 0.21/0.37 (((f0 @ sF5)) = $true) | (sF6 = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f17])).
% 0.21/0.37 thf(f43,plain,(
% 0.21/0.37 (sF6 = $true) | (((f0 @ sF5)) = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f17])).
% 0.21/0.37 thf(f44,plain,(
% 0.21/0.37 (sF5 = $true) | ($false = ((f0 @ sF4)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f15])).
% 0.21/0.37 thf(f45,plain,(
% 0.21/0.37 (((f0 @ sF4)) = $true) | ($false = sF5)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f15])).
% 0.21/0.37 thf(f46,plain,(
% 0.21/0.37 (sF0 = $false) | (((f3 @ x)) = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f8])).
% 0.21/0.37 thf(f47,plain,(
% 0.21/0.37 (((f3 @ x)) = $false) | (sF0 = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f8])).
% 0.21/0.37 thf(f48,plain,(
% 0.21/0.37 ($false = sF10) | (((f2 @ sF9)) = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f23])).
% 0.21/0.37 thf(f49,plain,(
% 0.21/0.37 ($false = ((f2 @ sF9))) | ($true = sF10)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f23])).
% 0.21/0.37 thf(f50,plain,(
% 0.21/0.37 (sF1 = $true) | ($false = ((f2 @ sF0)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f9])).
% 0.21/0.37 thf(f51,plain,(
% 0.21/0.37 ($true = ((f2 @ sF0))) | (sF1 = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f9])).
% 0.21/0.37 thf(f52,plain,(
% 0.21/0.37 ($false = ((f3 @ sF0))) | (sF8 = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f19])).
% 0.21/0.37 thf(f53,plain,(
% 0.21/0.37 ($true = ((f3 @ sF0))) | ($false = sF8)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f19])).
% 0.21/0.37 thf(f54,plain,(
% 0.21/0.37 (sF11 = $true) | ($false = ((f1 @ sF10)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f24])).
% 0.21/0.37 thf(f55,plain,(
% 0.21/0.37 ($true = ((f1 @ sF10))) | (sF11 = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f24])).
% 0.21/0.37 thf(f56,plain,(
% 0.21/0.37 (sF3 = $true) | ($false = ((f2 @ sF2)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f12])).
% 0.21/0.37 thf(f57,plain,(
% 0.21/0.37 (sF3 = $false) | (((f2 @ sF2)) = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f12])).
% 0.21/0.37 thf(f58,plain,(
% 0.21/0.37 ($true = ((f0 @ sF13))) | ($false = sF14)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f30])).
% 0.21/0.37 thf(f59,plain,(
% 0.21/0.37 ($true = sF14) | ($false = ((f0 @ sF13)))),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f30])).
% 0.21/0.37 thf(f60,plain,(
% 0.21/0.37 (((f1 @ sF12)) = $true) | (sF13 = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f28])).
% 0.21/0.37 thf(f61,plain,(
% 0.21/0.37 (sF13 = $true) | (((f1 @ sF12)) = $false)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f28])).
% 0.21/0.37 thf(f62,plain,(
% 0.21/0.37 ($false = sF12) | (((f1 @ sF11)) = $true)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f26])).
% 0.21/0.37 thf(f63,plain,(
% 0.21/0.37 (((f1 @ sF11)) = $false) | ($true = sF12)),
% 0.21/0.37 inference(iff_proxy_clausification,[],[f26])).
% 0.21/0.37 thf(f65,definition,(
% 0.21/0.37 spl15_1 <=> (((f0 @ sF6)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition])).
% 0.21/0.37 thf(f66,plain,(
% 0.21/0.37 (((f0 @ sF6)) != $true) | spl15_1),
% 0.21/0.37 inference(avatar_component_clause,[],[f65])).
% 0.21/0.37 thf(f67,plain,(
% 0.21/0.37 (((f0 @ sF6)) = $true) | ~spl15_1),
% 0.21/0.37 inference(avatar_component_clause,[],[f65])).
% 0.21/0.37 thf(f69,definition,(
% 0.21/0.37 spl15_2 <=> (sF7 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition])).
% 0.21/0.37 thf(f71,plain,(
% 0.21/0.37 (sF7 = $false) | ~spl15_2),
% 0.21/0.37 inference(avatar_component_clause,[],[f69])).
% 0.21/0.37 thf(f72,plain,(
% 0.21/0.37 spl15_1 | spl15_2),
% 0.21/0.37 inference(avatar_split_clause,[],[f33,f69,f65])).
% 0.21/0.37 thf(f74,definition,(
% 0.21/0.37 spl15_3 <=> ($false = ((f0 @ sF6)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition])).
% 0.21/0.37 thf(f76,plain,(
% 0.21/0.37 ($false = ((f0 @ sF6))) | ~spl15_3),
% 0.21/0.37 inference(avatar_component_clause,[],[f74])).
% 0.21/0.37 thf(f78,definition,(
% 0.21/0.37 spl15_4 <=> (sF7 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition])).
% 0.21/0.37 thf(f80,plain,(
% 0.21/0.37 (sF7 = $true) | ~spl15_4),
% 0.21/0.37 inference(avatar_component_clause,[],[f78])).
% 0.21/0.37 thf(f81,plain,(
% 0.21/0.37 spl15_3 | spl15_4),
% 0.21/0.37 inference(avatar_split_clause,[],[f32,f78,f74])).
% 0.21/0.37 thf(f83,definition,(
% 0.21/0.37 spl15_5 <=> (sF4 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition])).
% 0.21/0.37 thf(f84,plain,(
% 0.21/0.37 (sF4 != $true) | spl15_5),
% 0.21/0.37 inference(avatar_component_clause,[],[f83])).
% 0.21/0.37 thf(f85,plain,(
% 0.21/0.37 (sF4 = $true) | ~spl15_5),
% 0.21/0.37 inference(avatar_component_clause,[],[f83])).
% 0.21/0.37 thf(f87,definition,(
% 0.21/0.37 spl15_6 <=> ($false = ((f1 @ sF3)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition])).
% 0.21/0.37 thf(f88,plain,(
% 0.21/0.37 ($false != ((f1 @ sF3))) | spl15_6),
% 0.21/0.37 inference(avatar_component_clause,[],[f87])).
% 0.21/0.37 thf(f89,plain,(
% 0.21/0.37 ($false = ((f1 @ sF3))) | ~spl15_6),
% 0.21/0.37 inference(avatar_component_clause,[],[f87])).
% 0.21/0.37 thf(f90,plain,(
% 0.21/0.37 spl15_5 | spl15_6),
% 0.21/0.37 inference(avatar_split_clause,[],[f35,f87,f83])).
% 0.21/0.37 thf(f92,definition,(
% 0.21/0.37 spl15_7 <=> ($false = sF4)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition])).
% 0.21/0.37 thf(f94,plain,(
% 0.21/0.37 ($false = sF4) | ~spl15_7),
% 0.21/0.37 inference(avatar_component_clause,[],[f92])).
% 0.21/0.37 thf(f96,definition,(
% 0.21/0.37 spl15_8 <=> (((f1 @ sF3)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition])).
% 0.21/0.37 thf(f97,plain,(
% 0.21/0.37 (((f1 @ sF3)) != $true) | spl15_8),
% 0.21/0.37 inference(avatar_component_clause,[],[f96])).
% 0.21/0.37 thf(f98,plain,(
% 0.21/0.37 (((f1 @ sF3)) = $true) | ~spl15_8),
% 0.21/0.37 inference(avatar_component_clause,[],[f96])).
% 0.21/0.37 thf(f99,plain,(
% 0.21/0.37 spl15_7 | spl15_8),
% 0.21/0.37 inference(avatar_split_clause,[],[f34,f96,f92])).
% 0.21/0.37 thf(f101,definition,(
% 0.21/0.37 spl15_9 <=> (((f3 @ sF8)) = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition])).
% 0.21/0.37 thf(f102,plain,(
% 0.21/0.37 (((f3 @ sF8)) != $false) | spl15_9),
% 0.21/0.37 inference(avatar_component_clause,[],[f101])).
% 0.21/0.37 thf(f103,plain,(
% 0.21/0.37 (((f3 @ sF8)) = $false) | ~spl15_9),
% 0.21/0.37 inference(avatar_component_clause,[],[f101])).
% 0.21/0.37 thf(f105,definition,(
% 0.21/0.37 spl15_10 <=> (sF9 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition])).
% 0.21/0.37 thf(f106,plain,(
% 0.21/0.37 (sF9 != $true) | spl15_10),
% 0.21/0.37 inference(avatar_component_clause,[],[f105])).
% 0.21/0.37 thf(f107,plain,(
% 0.21/0.37 (sF9 = $true) | ~spl15_10),
% 0.21/0.37 inference(avatar_component_clause,[],[f105])).
% 0.21/0.37 thf(f108,plain,(
% 0.21/0.37 spl15_9 | spl15_10),
% 0.21/0.37 inference(avatar_split_clause,[],[f37,f105,f101])).
% 0.21/0.37 thf(f110,definition,(
% 0.21/0.37 spl15_11 <=> (((f3 @ sF8)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition])).
% 0.21/0.37 thf(f112,plain,(
% 0.21/0.37 (((f3 @ sF8)) = $true) | ~spl15_11),
% 0.21/0.37 inference(avatar_component_clause,[],[f110])).
% 0.21/0.37 thf(f114,definition,(
% 0.21/0.37 spl15_12 <=> ($false = sF9)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition])).
% 0.21/0.37 thf(f116,plain,(
% 0.21/0.37 ($false = sF9) | ~spl15_12),
% 0.21/0.37 inference(avatar_component_clause,[],[f114])).
% 0.21/0.37 thf(f117,plain,(
% 0.21/0.37 spl15_11 | spl15_12),
% 0.21/0.37 inference(avatar_split_clause,[],[f36,f114,f110])).
% 0.21/0.37 thf(f119,definition,(
% 0.21/0.37 spl15_13 <=> ($false = sF14)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition])).
% 0.21/0.37 thf(f121,plain,(
% 0.21/0.37 ($false = sF14) | ~spl15_13),
% 0.21/0.37 inference(avatar_component_clause,[],[f119])).
% 0.21/0.37 thf(f122,plain,(
% 0.21/0.37 spl15_13 | spl15_2),
% 0.21/0.37 inference(avatar_split_clause,[],[f39,f69,f119])).
% 0.21/0.37 thf(f124,definition,(
% 0.21/0.37 spl15_14 <=> ($true = sF14)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition])).
% 0.21/0.37 thf(f126,plain,(
% 0.21/0.37 ($true = sF14) | ~spl15_14),
% 0.21/0.37 inference(avatar_component_clause,[],[f124])).
% 0.21/0.37 thf(f127,plain,(
% 0.21/0.37 spl15_14 | spl15_4),
% 0.21/0.37 inference(avatar_split_clause,[],[f38,f78,f124])).
% 0.21/0.37 thf(f129,definition,(
% 0.21/0.37 spl15_15 <=> ($false = ((f2 @ sF1)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition])).
% 0.21/0.37 thf(f130,plain,(
% 0.21/0.37 ($false != ((f2 @ sF1))) | spl15_15),
% 0.21/0.37 inference(avatar_component_clause,[],[f129])).
% 0.21/0.37 thf(f131,plain,(
% 0.21/0.37 ($false = ((f2 @ sF1))) | ~spl15_15),
% 0.21/0.37 inference(avatar_component_clause,[],[f129])).
% 0.21/0.37 thf(f133,definition,(
% 0.21/0.37 spl15_16 <=> ($true = sF2)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition])).
% 0.21/0.37 thf(f134,plain,(
% 0.21/0.37 ($true != sF2) | spl15_16),
% 0.21/0.37 inference(avatar_component_clause,[],[f133])).
% 0.21/0.37 thf(f135,plain,(
% 0.21/0.37 ($true = sF2) | ~spl15_16),
% 0.21/0.37 inference(avatar_component_clause,[],[f133])).
% 0.21/0.37 thf(f136,plain,(
% 0.21/0.37 spl15_15 | spl15_16),
% 0.21/0.37 inference(avatar_split_clause,[],[f41,f133,f129])).
% 0.21/0.37 thf(f138,definition,(
% 0.21/0.37 spl15_17 <=> ($false = sF2)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition])).
% 0.21/0.37 thf(f140,plain,(
% 0.21/0.37 ($false = sF2) | ~spl15_17),
% 0.21/0.37 inference(avatar_component_clause,[],[f138])).
% 0.21/0.37 thf(f142,definition,(
% 0.21/0.37 spl15_18 <=> ($true = ((f2 @ sF1)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition])).
% 0.21/0.37 thf(f143,plain,(
% 0.21/0.37 ($true != ((f2 @ sF1))) | spl15_18),
% 0.21/0.37 inference(avatar_component_clause,[],[f142])).
% 0.21/0.37 thf(f144,plain,(
% 0.21/0.37 ($true = ((f2 @ sF1))) | ~spl15_18),
% 0.21/0.37 inference(avatar_component_clause,[],[f142])).
% 0.21/0.37 thf(f145,plain,(
% 0.21/0.37 spl15_17 | spl15_18),
% 0.21/0.37 inference(avatar_split_clause,[],[f40,f142,f138])).
% 0.21/0.37 thf(f147,definition,(
% 0.21/0.37 spl15_19 <=> (((f0 @ sF5)) = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition])).
% 0.21/0.37 thf(f149,plain,(
% 0.21/0.37 (((f0 @ sF5)) = $false) | ~spl15_19),
% 0.21/0.37 inference(avatar_component_clause,[],[f147])).
% 0.21/0.37 thf(f151,definition,(
% 0.21/0.37 spl15_20 <=> (sF6 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition])).
% 0.21/0.37 thf(f152,plain,(
% 0.21/0.37 (sF6 != $true) | spl15_20),
% 0.21/0.37 inference(avatar_component_clause,[],[f151])).
% 0.21/0.37 thf(f153,plain,(
% 0.21/0.37 (sF6 = $true) | ~spl15_20),
% 0.21/0.37 inference(avatar_component_clause,[],[f151])).
% 0.21/0.37 thf(f154,plain,(
% 0.21/0.37 spl15_19 | spl15_20),
% 0.21/0.37 inference(avatar_split_clause,[],[f43,f151,f147])).
% 0.21/0.37 thf(f156,definition,(
% 0.21/0.37 spl15_21 <=> (((f0 @ sF5)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition])).
% 0.21/0.37 thf(f158,plain,(
% 0.21/0.37 (((f0 @ sF5)) = $true) | ~spl15_21),
% 0.21/0.37 inference(avatar_component_clause,[],[f156])).
% 0.21/0.37 thf(f160,definition,(
% 0.21/0.37 spl15_22 <=> (sF6 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition])).
% 0.21/0.37 thf(f162,plain,(
% 0.21/0.37 (sF6 = $false) | ~spl15_22),
% 0.21/0.37 inference(avatar_component_clause,[],[f160])).
% 0.21/0.37 thf(f163,plain,(
% 0.21/0.37 spl15_21 | spl15_22),
% 0.21/0.37 inference(avatar_split_clause,[],[f42,f160,f156])).
% 0.21/0.37 thf(f165,definition,(
% 0.21/0.37 spl15_23 <=> (((f0 @ sF4)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_23])],[avatar_definition])).
% 0.21/0.37 thf(f166,plain,(
% 0.21/0.37 (((f0 @ sF4)) != $true) | spl15_23),
% 0.21/0.37 inference(avatar_component_clause,[],[f165])).
% 0.21/0.37 thf(f167,plain,(
% 0.21/0.37 (((f0 @ sF4)) = $true) | ~spl15_23),
% 0.21/0.37 inference(avatar_component_clause,[],[f165])).
% 0.21/0.37 thf(f169,definition,(
% 0.21/0.37 spl15_24 <=> ($false = sF5)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_24])],[avatar_definition])).
% 0.21/0.37 thf(f171,plain,(
% 0.21/0.37 ($false = sF5) | ~spl15_24),
% 0.21/0.37 inference(avatar_component_clause,[],[f169])).
% 0.21/0.37 thf(f172,plain,(
% 0.21/0.37 spl15_23 | spl15_24),
% 0.21/0.37 inference(avatar_split_clause,[],[f45,f169,f165])).
% 0.21/0.37 thf(f174,definition,(
% 0.21/0.37 spl15_25 <=> (sF5 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition])).
% 0.21/0.37 thf(f175,plain,(
% 0.21/0.37 (sF5 != $true) | spl15_25),
% 0.21/0.37 inference(avatar_component_clause,[],[f174])).
% 0.21/0.37 thf(f176,plain,(
% 0.21/0.37 (sF5 = $true) | ~spl15_25),
% 0.21/0.37 inference(avatar_component_clause,[],[f174])).
% 0.21/0.37 thf(f178,definition,(
% 0.21/0.37 spl15_26 <=> ($false = ((f0 @ sF4)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition])).
% 0.21/0.37 thf(f180,plain,(
% 0.21/0.37 ($false = ((f0 @ sF4))) | ~spl15_26),
% 0.21/0.37 inference(avatar_component_clause,[],[f178])).
% 0.21/0.37 thf(f181,plain,(
% 0.21/0.37 spl15_25 | spl15_26),
% 0.21/0.37 inference(avatar_split_clause,[],[f44,f178,f174])).
% 0.21/0.37 thf(f183,definition,(
% 0.21/0.37 spl15_27 <=> (((f3 @ x)) = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_27])],[avatar_definition])).
% 0.21/0.37 thf(f184,plain,(
% 0.21/0.37 (((f3 @ x)) != $false) | spl15_27),
% 0.21/0.37 inference(avatar_component_clause,[],[f183])).
% 0.21/0.37 thf(f185,plain,(
% 0.21/0.37 (((f3 @ x)) = $false) | ~spl15_27),
% 0.21/0.37 inference(avatar_component_clause,[],[f183])).
% 0.21/0.37 thf(f187,definition,(
% 0.21/0.37 spl15_28 <=> (sF0 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition])).
% 0.21/0.37 thf(f188,plain,(
% 0.21/0.37 (sF0 != $true) | spl15_28),
% 0.21/0.37 inference(avatar_component_clause,[],[f187])).
% 0.21/0.37 thf(f189,plain,(
% 0.21/0.37 (sF0 = $true) | ~spl15_28),
% 0.21/0.37 inference(avatar_component_clause,[],[f187])).
% 0.21/0.37 thf(f190,plain,(
% 0.21/0.37 spl15_27 | spl15_28),
% 0.21/0.37 inference(avatar_split_clause,[],[f47,f187,f183])).
% 0.21/0.37 thf(f192,definition,(
% 0.21/0.37 spl15_29 <=> (((f3 @ x)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_29])],[avatar_definition])).
% 0.21/0.37 thf(f194,plain,(
% 0.21/0.37 (((f3 @ x)) = $true) | ~spl15_29),
% 0.21/0.37 inference(avatar_component_clause,[],[f192])).
% 0.21/0.37 thf(f196,definition,(
% 0.21/0.37 spl15_30 <=> (sF0 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_30])],[avatar_definition])).
% 0.21/0.37 thf(f198,plain,(
% 0.21/0.37 (sF0 = $false) | ~spl15_30),
% 0.21/0.37 inference(avatar_component_clause,[],[f196])).
% 0.21/0.37 thf(f199,plain,(
% 0.21/0.37 spl15_29 | spl15_30),
% 0.21/0.37 inference(avatar_split_clause,[],[f46,f196,f192])).
% 0.21/0.37 thf(f201,definition,(
% 0.21/0.37 spl15_31 <=> ($false = ((f2 @ sF9)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition])).
% 0.21/0.37 thf(f202,plain,(
% 0.21/0.37 ($false != ((f2 @ sF9))) | spl15_31),
% 0.21/0.37 inference(avatar_component_clause,[],[f201])).
% 0.21/0.37 thf(f203,plain,(
% 0.21/0.37 ($false = ((f2 @ sF9))) | ~spl15_31),
% 0.21/0.37 inference(avatar_component_clause,[],[f201])).
% 0.21/0.37 thf(f205,definition,(
% 0.21/0.37 spl15_32 <=> ($true = sF10)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_32])],[avatar_definition])).
% 0.21/0.37 thf(f206,plain,(
% 0.21/0.37 ($true != sF10) | spl15_32),
% 0.21/0.37 inference(avatar_component_clause,[],[f205])).
% 0.21/0.37 thf(f207,plain,(
% 0.21/0.37 ($true = sF10) | ~spl15_32),
% 0.21/0.37 inference(avatar_component_clause,[],[f205])).
% 0.21/0.37 thf(f208,plain,(
% 0.21/0.37 spl15_31 | spl15_32),
% 0.21/0.37 inference(avatar_split_clause,[],[f49,f205,f201])).
% 0.21/0.37 thf(f210,definition,(
% 0.21/0.37 spl15_33 <=> ($false = sF10)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_33])],[avatar_definition])).
% 0.21/0.37 thf(f212,plain,(
% 0.21/0.37 ($false = sF10) | ~spl15_33),
% 0.21/0.37 inference(avatar_component_clause,[],[f210])).
% 0.21/0.37 thf(f214,definition,(
% 0.21/0.37 spl15_34 <=> (((f2 @ sF9)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition])).
% 0.21/0.37 thf(f216,plain,(
% 0.21/0.37 (((f2 @ sF9)) = $true) | ~spl15_34),
% 0.21/0.37 inference(avatar_component_clause,[],[f214])).
% 0.21/0.37 thf(f217,plain,(
% 0.21/0.37 spl15_33 | spl15_34),
% 0.21/0.37 inference(avatar_split_clause,[],[f48,f214,f210])).
% 0.21/0.37 thf(f219,definition,(
% 0.21/0.37 spl15_35 <=> ($true = ((f2 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition])).
% 0.21/0.37 thf(f221,plain,(
% 0.21/0.37 ($true = ((f2 @ sF0))) | ~spl15_35),
% 0.21/0.37 inference(avatar_component_clause,[],[f219])).
% 0.21/0.37 thf(f223,definition,(
% 0.21/0.37 spl15_36 <=> (sF1 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_36])],[avatar_definition])).
% 0.21/0.37 thf(f224,plain,(
% 0.21/0.37 (sF1 != $false) | spl15_36),
% 0.21/0.37 inference(avatar_component_clause,[],[f223])).
% 0.21/0.37 thf(f225,plain,(
% 0.21/0.37 (sF1 = $false) | ~spl15_36),
% 0.21/0.37 inference(avatar_component_clause,[],[f223])).
% 0.21/0.37 thf(f226,plain,(
% 0.21/0.37 spl15_35 | spl15_36),
% 0.21/0.37 inference(avatar_split_clause,[],[f51,f223,f219])).
% 0.21/0.37 thf(f228,definition,(
% 0.21/0.37 spl15_37 <=> (sF1 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_37])],[avatar_definition])).
% 0.21/0.37 thf(f229,plain,(
% 0.21/0.37 (sF1 != $true) | spl15_37),
% 0.21/0.37 inference(avatar_component_clause,[],[f228])).
% 0.21/0.37 thf(f230,plain,(
% 0.21/0.37 (sF1 = $true) | ~spl15_37),
% 0.21/0.37 inference(avatar_component_clause,[],[f228])).
% 0.21/0.37 thf(f232,definition,(
% 0.21/0.37 spl15_38 <=> ($false = ((f2 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_38])],[avatar_definition])).
% 0.21/0.37 thf(f234,plain,(
% 0.21/0.37 ($false = ((f2 @ sF0))) | ~spl15_38),
% 0.21/0.37 inference(avatar_component_clause,[],[f232])).
% 0.21/0.37 thf(f235,plain,(
% 0.21/0.37 spl15_37 | spl15_38),
% 0.21/0.37 inference(avatar_split_clause,[],[f50,f232,f228])).
% 0.21/0.37 thf(f237,definition,(
% 0.21/0.37 spl15_39 <=> ($false = sF8)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_39])],[avatar_definition])).
% 0.21/0.37 thf(f239,plain,(
% 0.21/0.37 ($false = sF8) | ~spl15_39),
% 0.21/0.37 inference(avatar_component_clause,[],[f237])).
% 0.21/0.37 thf(f241,definition,(
% 0.21/0.37 spl15_40 <=> ($true = ((f3 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_40])],[avatar_definition])).
% 0.21/0.37 thf(f243,plain,(
% 0.21/0.37 ($true = ((f3 @ sF0))) | ~spl15_40),
% 0.21/0.37 inference(avatar_component_clause,[],[f241])).
% 0.21/0.37 thf(f244,plain,(
% 0.21/0.37 spl15_39 | spl15_40),
% 0.21/0.37 inference(avatar_split_clause,[],[f53,f241,f237])).
% 0.21/0.37 thf(f246,definition,(
% 0.21/0.37 spl15_41 <=> ($false = ((f3 @ sF0)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_41])],[avatar_definition])).
% 0.21/0.37 thf(f248,plain,(
% 0.21/0.37 ($false = ((f3 @ sF0))) | ~spl15_41),
% 0.21/0.37 inference(avatar_component_clause,[],[f246])).
% 0.21/0.37 thf(f250,definition,(
% 0.21/0.37 spl15_42 <=> (sF8 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_42])],[avatar_definition])).
% 0.21/0.37 thf(f252,plain,(
% 0.21/0.37 (sF8 = $true) | ~spl15_42),
% 0.21/0.37 inference(avatar_component_clause,[],[f250])).
% 0.21/0.37 thf(f253,plain,(
% 0.21/0.37 spl15_41 | spl15_42),
% 0.21/0.37 inference(avatar_split_clause,[],[f52,f250,f246])).
% 0.21/0.37 thf(f255,definition,(
% 0.21/0.37 spl15_43 <=> ($true = ((f1 @ sF10)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_43])],[avatar_definition])).
% 0.21/0.37 thf(f257,plain,(
% 0.21/0.37 ($true = ((f1 @ sF10))) | ~spl15_43),
% 0.21/0.37 inference(avatar_component_clause,[],[f255])).
% 0.21/0.37 thf(f259,definition,(
% 0.21/0.37 spl15_44 <=> (sF11 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_44])],[avatar_definition])).
% 0.21/0.37 thf(f261,plain,(
% 0.21/0.37 (sF11 = $false) | ~spl15_44),
% 0.21/0.37 inference(avatar_component_clause,[],[f259])).
% 0.21/0.37 thf(f262,plain,(
% 0.21/0.37 spl15_43 | spl15_44),
% 0.21/0.37 inference(avatar_split_clause,[],[f55,f259,f255])).
% 0.21/0.37 thf(f264,definition,(
% 0.21/0.37 spl15_45 <=> ($false = ((f1 @ sF10)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_45])],[avatar_definition])).
% 0.21/0.37 thf(f266,plain,(
% 0.21/0.37 ($false = ((f1 @ sF10))) | ~spl15_45),
% 0.21/0.37 inference(avatar_component_clause,[],[f264])).
% 0.21/0.37 thf(f268,definition,(
% 0.21/0.37 spl15_46 <=> (sF11 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_46])],[avatar_definition])).
% 0.21/0.37 thf(f270,plain,(
% 0.21/0.37 (sF11 = $true) | ~spl15_46),
% 0.21/0.37 inference(avatar_component_clause,[],[f268])).
% 0.21/0.37 thf(f271,plain,(
% 0.21/0.37 spl15_45 | spl15_46),
% 0.21/0.37 inference(avatar_split_clause,[],[f54,f268,f264])).
% 0.21/0.37 thf(f273,definition,(
% 0.21/0.37 spl15_47 <=> (sF3 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_47])],[avatar_definition])).
% 0.21/0.37 thf(f275,plain,(
% 0.21/0.37 (sF3 = $false) | ~spl15_47),
% 0.21/0.37 inference(avatar_component_clause,[],[f273])).
% 0.21/0.37 thf(f277,definition,(
% 0.21/0.37 spl15_48 <=> (((f2 @ sF2)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_48])],[avatar_definition])).
% 0.21/0.37 thf(f279,plain,(
% 0.21/0.37 (((f2 @ sF2)) = $true) | ~spl15_48),
% 0.21/0.37 inference(avatar_component_clause,[],[f277])).
% 0.21/0.37 thf(f280,plain,(
% 0.21/0.37 spl15_47 | spl15_48),
% 0.21/0.37 inference(avatar_split_clause,[],[f57,f277,f273])).
% 0.21/0.37 thf(f282,definition,(
% 0.21/0.37 spl15_49 <=> ($false = ((f2 @ sF2)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_49])],[avatar_definition])).
% 0.21/0.37 thf(f284,plain,(
% 0.21/0.37 ($false = ((f2 @ sF2))) | ~spl15_49),
% 0.21/0.37 inference(avatar_component_clause,[],[f282])).
% 0.21/0.37 thf(f286,definition,(
% 0.21/0.37 spl15_50 <=> (sF3 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_50])],[avatar_definition])).
% 0.21/0.37 thf(f287,plain,(
% 0.21/0.37 (sF3 != $true) | spl15_50),
% 0.21/0.37 inference(avatar_component_clause,[],[f286])).
% 0.21/0.37 thf(f288,plain,(
% 0.21/0.37 (sF3 = $true) | ~spl15_50),
% 0.21/0.37 inference(avatar_component_clause,[],[f286])).
% 0.21/0.37 thf(f289,plain,(
% 0.21/0.37 spl15_49 | spl15_50),
% 0.21/0.37 inference(avatar_split_clause,[],[f56,f286,f282])).
% 0.21/0.37 thf(f291,definition,(
% 0.21/0.37 spl15_51 <=> ($false = ((f0 @ sF13)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_51])],[avatar_definition])).
% 0.21/0.37 thf(f292,plain,(
% 0.21/0.37 ($false != ((f0 @ sF13))) | spl15_51),
% 0.21/0.37 inference(avatar_component_clause,[],[f291])).
% 0.21/0.37 thf(f293,plain,(
% 0.21/0.37 ($false = ((f0 @ sF13))) | ~spl15_51),
% 0.21/0.37 inference(avatar_component_clause,[],[f291])).
% 0.21/0.37 thf(f294,plain,(
% 0.21/0.37 spl15_14 | spl15_51),
% 0.21/0.37 inference(avatar_split_clause,[],[f59,f291,f124])).
% 0.21/0.37 thf(f296,definition,(
% 0.21/0.37 spl15_52 <=> ($true = ((f0 @ sF13)))),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_52])],[avatar_definition])).
% 0.21/0.37 thf(f297,plain,(
% 0.21/0.37 ($true != ((f0 @ sF13))) | spl15_52),
% 0.21/0.37 inference(avatar_component_clause,[],[f296])).
% 0.21/0.37 thf(f298,plain,(
% 0.21/0.37 ($true = ((f0 @ sF13))) | ~spl15_52),
% 0.21/0.37 inference(avatar_component_clause,[],[f296])).
% 0.21/0.37 thf(f299,plain,(
% 0.21/0.37 spl15_52 | spl15_13),
% 0.21/0.37 inference(avatar_split_clause,[],[f58,f119,f296])).
% 0.21/0.37 thf(f301,definition,(
% 0.21/0.37 spl15_53 <=> (((f1 @ sF12)) = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition])).
% 0.21/0.37 thf(f303,plain,(
% 0.21/0.37 (((f1 @ sF12)) = $false) | ~spl15_53),
% 0.21/0.37 inference(avatar_component_clause,[],[f301])).
% 0.21/0.37 thf(f305,definition,(
% 0.21/0.37 spl15_54 <=> (sF13 = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_54])],[avatar_definition])).
% 0.21/0.37 thf(f307,plain,(
% 0.21/0.37 (sF13 = $true) | ~spl15_54),
% 0.21/0.37 inference(avatar_component_clause,[],[f305])).
% 0.21/0.37 thf(f308,plain,(
% 0.21/0.37 spl15_53 | spl15_54),
% 0.21/0.37 inference(avatar_split_clause,[],[f61,f305,f301])).
% 0.21/0.37 thf(f310,definition,(
% 0.21/0.37 spl15_55 <=> (sF13 = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_55])],[avatar_definition])).
% 0.21/0.37 thf(f311,plain,(
% 0.21/0.37 (sF13 != $false) | spl15_55),
% 0.21/0.37 inference(avatar_component_clause,[],[f310])).
% 0.21/0.37 thf(f312,plain,(
% 0.21/0.37 (sF13 = $false) | ~spl15_55),
% 0.21/0.37 inference(avatar_component_clause,[],[f310])).
% 0.21/0.37 thf(f314,definition,(
% 0.21/0.37 spl15_56 <=> (((f1 @ sF12)) = $true)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_56])],[avatar_definition])).
% 0.21/0.37 thf(f316,plain,(
% 0.21/0.37 (((f1 @ sF12)) = $true) | ~spl15_56),
% 0.21/0.37 inference(avatar_component_clause,[],[f314])).
% 0.21/0.37 thf(f317,plain,(
% 0.21/0.37 spl15_55 | spl15_56),
% 0.21/0.37 inference(avatar_split_clause,[],[f60,f314,f310])).
% 0.21/0.37 thf(f319,definition,(
% 0.21/0.37 spl15_57 <=> (((f1 @ sF11)) = $false)),
% 0.21/0.37 introduced(definition,[new_symbols(definition,[spl15_57])],[avatar_definition])).
% 0.21/0.37 thf(f321,plain,(
% 0.21/0.37 (((f1 @ sF11)) = $false) | ~spl15_57),
% 0.77/0.37 inference(avatar_component_clause,[],[f319])).
% 0.77/0.37 thf(f323,definition,(
% 0.77/0.37 spl15_58 <=> ($true = sF12)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition])).
% 0.77/0.37 thf(f324,plain,(
% 0.77/0.37 ($true != sF12) | spl15_58),
% 0.77/0.37 inference(avatar_component_clause,[],[f323])).
% 0.77/0.37 thf(f325,plain,(
% 0.77/0.37 ($true = sF12) | ~spl15_58),
% 0.77/0.37 inference(avatar_component_clause,[],[f323])).
% 0.77/0.37 thf(f326,plain,(
% 0.77/0.37 spl15_57 | spl15_58),
% 0.77/0.37 inference(avatar_split_clause,[],[f63,f323,f319])).
% 0.77/0.37 thf(f328,definition,(
% 0.77/0.37 spl15_59 <=> ($false = sF12)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_59])],[avatar_definition])).
% 0.77/0.37 thf(f330,plain,(
% 0.77/0.37 ($false = sF12) | ~spl15_59),
% 0.77/0.37 inference(avatar_component_clause,[],[f328])).
% 0.77/0.37 thf(f332,definition,(
% 0.77/0.37 spl15_60 <=> (((f1 @ sF11)) = $true)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition])).
% 0.77/0.37 thf(f334,plain,(
% 0.77/0.37 (((f1 @ sF11)) = $true) | ~spl15_60),
% 0.77/0.37 inference(avatar_component_clause,[],[f332])).
% 0.77/0.37 thf(f335,plain,(
% 0.77/0.37 spl15_59 | spl15_60),
% 0.77/0.37 inference(avatar_split_clause,[],[f62,f332,f328])).
% 0.77/0.37 thf(f336,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_13 | ~spl15_14)),
% 0.77/0.37 inference(forward_demodulation,[],[f126,f121])).
% 0.77/0.37 thf(f337,plain,(
% 0.77/0.37 $false | (~spl15_13 | ~spl15_14)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f336])).
% 0.77/0.37 thf(f338,plain,(
% 0.77/0.37 ~spl15_13 | ~spl15_14),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f337])).
% 0.77/0.37 thf(f340,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_2 | ~spl15_4)),
% 0.77/0.37 inference(forward_demodulation,[],[f80,f71])).
% 0.77/0.37 thf(f341,plain,(
% 0.77/0.37 $false | (~spl15_2 | ~spl15_4)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f340])).
% 0.77/0.37 thf(f342,plain,(
% 0.77/0.37 ~spl15_2 | ~spl15_4),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f341])).
% 0.77/0.37 thf(f345,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_5 | ~spl15_7)),
% 0.77/0.37 inference(forward_demodulation,[],[f94,f85])).
% 0.77/0.37 thf(f346,plain,(
% 0.77/0.37 $false | (~spl15_5 | ~spl15_7)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f345])).
% 0.77/0.37 thf(f347,plain,(
% 0.77/0.37 ~spl15_5 | ~spl15_7),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f346])).
% 0.77/0.37 thf(f371,plain,(
% 0.77/0.37 (sF6 = $false) | (((f0 @ $true)) = $false) | ~spl15_3),
% 0.77/0.37 inference(constrained_superposition,[],[f76,f6])).
% 0.77/0.37 thf(f375,definition,(
% 0.77/0.37 spl15_61 <=> (((f0 @ $true)) = $false)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_61])],[avatar_definition])).
% 0.77/0.37 thf(f377,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | ~spl15_61),
% 0.77/0.37 inference(avatar_component_clause,[],[f375])).
% 0.77/0.37 thf(f378,plain,(
% 0.77/0.37 spl15_61 | spl15_22 | ~spl15_3),
% 0.77/0.37 inference(avatar_split_clause,[],[f371,f74,f160,f375])).
% 0.77/0.37 thf(f385,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | (~spl15_15 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f131,f230])).
% 0.77/0.37 thf(f386,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | (~spl15_19 | ~spl15_25)),
% 0.77/0.37 inference(forward_demodulation,[],[f149,f176])).
% 0.77/0.37 thf(f387,plain,(
% 0.77/0.37 spl15_61 | ~spl15_19 | ~spl15_25),
% 0.77/0.37 inference(avatar_split_clause,[],[f386,f174,f147,f375])).
% 0.77/0.37 thf(f389,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_20 | ~spl15_22)),
% 0.77/0.37 inference(forward_demodulation,[],[f153,f162])).
% 0.77/0.37 thf(f390,plain,(
% 0.77/0.37 $false | (~spl15_20 | ~spl15_22)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f389])).
% 0.77/0.37 thf(f391,plain,(
% 0.77/0.37 ~spl15_20 | ~spl15_22),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f390])).
% 0.77/0.37 thf(f393,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | (~spl15_5 | ~spl15_26)),
% 0.77/0.37 inference(forward_demodulation,[],[f180,f85])).
% 0.77/0.37 thf(f395,plain,(
% 0.77/0.37 spl15_61 | ~spl15_5 | ~spl15_26),
% 0.77/0.37 inference(avatar_split_clause,[],[f393,f178,f83,f375])).
% 0.77/0.37 thf(f414,definition,(
% 0.77/0.37 spl15_62 <=> (((f3 @ $true)) = $false)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_62])],[avatar_definition])).
% 0.77/0.37 thf(f416,plain,(
% 0.77/0.37 (((f3 @ $true)) = $false) | ~spl15_62),
% 0.77/0.37 inference(avatar_component_clause,[],[f414])).
% 0.77/0.37 thf(f418,definition,(
% 0.77/0.37 spl15_63 <=> (x = $false)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_63])],[avatar_definition])).
% 0.77/0.37 thf(f419,plain,(
% 0.77/0.37 (x != $false) | spl15_63),
% 0.77/0.37 inference(avatar_component_clause,[],[f418])).
% 0.77/0.37 thf(f420,plain,(
% 0.77/0.37 (x = $false) | ~spl15_63),
% 0.77/0.37 inference(avatar_component_clause,[],[f418])).
% 0.77/0.37 thf(f428,definition,(
% 0.77/0.37 spl15_64 <=> (((f3 @ $true)) = $true)),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_64])],[avatar_definition])).
% 0.77/0.37 thf(f430,plain,(
% 0.77/0.37 (((f3 @ $true)) = $true) | ~spl15_64),
% 0.77/0.37 inference(avatar_component_clause,[],[f428])).
% 0.77/0.37 thf(f435,plain,(
% 0.77/0.37 (sF0 = $false) | ($true != $true) | spl15_28),
% 0.77/0.37 inference(constrained_superposition,[],[f188,f6])).
% 0.77/0.37 thf(f436,plain,(
% 0.77/0.37 (sF0 = $false) | spl15_28),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f435])).
% 0.77/0.37 thf(f437,plain,(
% 0.77/0.37 spl15_30 | spl15_28),
% 0.77/0.37 inference(avatar_split_clause,[],[f436,f187,f196])).
% 0.77/0.37 thf(f450,definition,(
% 0.77/0.37 spl15_65 <=> ($false = ((f2 @ $true)))),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_65])],[avatar_definition])).
% 0.77/0.37 thf(f452,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | ~spl15_65),
% 0.77/0.37 inference(avatar_component_clause,[],[f450])).
% 0.77/0.37 thf(f458,plain,(
% 0.77/0.37 (((f3 @ $false)) = $false) | (~spl15_30 | ~spl15_41)),
% 0.77/0.37 inference(forward_demodulation,[],[f248,f198])).
% 0.77/0.37 thf(f462,plain,(
% 0.77/0.37 ($false = ((f0 @ $false))) | (~spl15_51 | ~spl15_55)),
% 0.77/0.37 inference(forward_demodulation,[],[f293,f312])).
% 0.77/0.37 thf(f469,definition,(
% 0.77/0.37 spl15_66 <=> ($false = ((f1 @ $true)))),
% 0.77/0.37 introduced(definition,[new_symbols(definition,[spl15_66])],[avatar_definition])).
% 0.77/0.37 thf(f471,plain,(
% 0.77/0.37 ($false = ((f1 @ $true))) | ~spl15_66),
% 0.77/0.37 inference(avatar_component_clause,[],[f469])).
% 0.77/0.37 thf(f481,plain,(
% 0.77/0.37 (((f3 @ $false)) = $true) | (~spl15_30 | ~spl15_40)),
% 0.77/0.37 inference(forward_demodulation,[],[f243,f198])).
% 0.77/0.37 thf(f488,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_9 | ~spl15_11)),
% 0.77/0.37 inference(forward_demodulation,[],[f112,f103])).
% 0.77/0.37 thf(f489,plain,(
% 0.77/0.37 $false | (~spl15_9 | ~spl15_11)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f488])).
% 0.77/0.37 thf(f490,plain,(
% 0.77/0.37 ~spl15_9 | ~spl15_11),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f489])).
% 0.77/0.37 thf(f495,plain,(
% 0.77/0.37 ($false = sF8) | (((f3 @ $true)) = $false) | ~spl15_9),
% 0.77/0.37 inference(constrained_superposition,[],[f103,f6])).
% 0.77/0.37 thf(f500,plain,(
% 0.77/0.37 spl15_65 | ~spl15_15 | ~spl15_37),
% 0.77/0.37 inference(avatar_split_clause,[],[f385,f228,f129,f450])).
% 0.77/0.37 thf(f501,plain,(
% 0.77/0.37 ($false != ((f2 @ $true))) | (spl15_15 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f130,f230])).
% 0.77/0.37 thf(f505,plain,(
% 0.77/0.37 ~spl15_65 | spl15_15 | ~spl15_37),
% 0.77/0.37 inference(avatar_split_clause,[],[f501,f228,f129,f450])).
% 0.77/0.37 thf(f506,plain,(
% 0.77/0.37 (((f2 @ $true)) = $true) | (~spl15_18 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f144,f230])).
% 0.77/0.37 thf(f508,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | (~spl15_16 | ~spl15_49)),
% 0.77/0.37 inference(forward_demodulation,[],[f284,f135])).
% 0.77/0.37 thf(f509,plain,(
% 0.77/0.37 spl15_65 | ~spl15_16 | ~spl15_49),
% 0.77/0.37 inference(avatar_split_clause,[],[f508,f282,f133,f450])).
% 0.77/0.37 thf(f518,plain,(
% 0.77/0.37 (((f1 @ $true)) = $true) | (~spl15_8 | ~spl15_50)),
% 0.77/0.37 inference(forward_demodulation,[],[f98,f288])).
% 0.77/0.37 thf(f528,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_31 | ~spl15_34)),
% 0.77/0.37 inference(forward_demodulation,[],[f216,f203])).
% 0.77/0.37 thf(f529,plain,(
% 0.77/0.37 $false | (~spl15_31 | ~spl15_34)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f528])).
% 0.77/0.37 thf(f530,plain,(
% 0.77/0.37 ~spl15_31 | ~spl15_34),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f529])).
% 0.77/0.37 thf(f531,plain,(
% 0.77/0.37 (((f2 @ $false)) = $true) | (~spl15_12 | ~spl15_34)),
% 0.77/0.37 inference(forward_demodulation,[],[f216,f116])).
% 0.77/0.37 thf(f535,plain,(
% 0.77/0.37 (((f1 @ $true)) = $true) | (~spl15_32 | ~spl15_43)),
% 0.77/0.37 inference(forward_demodulation,[],[f257,f207])).
% 0.77/0.37 thf(f536,plain,(
% 0.77/0.37 ($false = ((f1 @ $true))) | (~spl15_32 | ~spl15_45)),
% 0.77/0.37 inference(forward_demodulation,[],[f266,f207])).
% 0.77/0.37 thf(f537,plain,(
% 0.77/0.37 spl15_66 | ~spl15_32 | ~spl15_45),
% 0.77/0.37 inference(avatar_split_clause,[],[f536,f264,f205,f469])).
% 0.77/0.37 thf(f547,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_30 | ~spl15_40 | ~spl15_41)),
% 0.77/0.37 inference(forward_demodulation,[],[f481,f458])).
% 0.77/0.37 thf(f548,plain,(
% 0.77/0.37 $false | (~spl15_30 | ~spl15_40 | ~spl15_41)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f547])).
% 0.77/0.37 thf(f549,plain,(
% 0.77/0.37 ~spl15_30 | ~spl15_40 | ~spl15_41),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f548])).
% 0.77/0.37 thf(f551,plain,(
% 0.77/0.37 spl15_39 | spl15_62 | ~spl15_9),
% 0.77/0.37 inference(avatar_split_clause,[],[f495,f101,f414,f237])).
% 0.77/0.37 thf(f569,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_8 | ~spl15_50 | ~spl15_66)),
% 0.77/0.37 inference(forward_demodulation,[],[f471,f518])).
% 0.77/0.37 thf(f570,plain,(
% 0.77/0.37 $false | (~spl15_8 | ~spl15_50 | ~spl15_66)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f569])).
% 0.77/0.37 thf(f571,plain,(
% 0.77/0.37 ~spl15_8 | ~spl15_50 | ~spl15_66),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f570])).
% 0.77/0.37 thf(f572,plain,(
% 0.77/0.37 ($false = ((f1 @ $true))) | (~spl15_6 | ~spl15_50)),
% 0.77/0.37 inference(forward_demodulation,[],[f89,f288])).
% 0.77/0.37 thf(f573,plain,(
% 0.77/0.37 (((f1 @ $true)) != $true) | (spl15_8 | ~spl15_50)),
% 0.77/0.37 inference(forward_demodulation,[],[f97,f288])).
% 0.77/0.37 thf(f574,plain,(
% 0.77/0.37 spl15_66 | ~spl15_6 | ~spl15_50),
% 0.77/0.37 inference(avatar_split_clause,[],[f572,f286,f87,f469])).
% 0.77/0.37 thf(f575,plain,(
% 0.77/0.37 ($false = sF4) | ($true != $true) | spl15_5),
% 0.77/0.37 inference(constrained_superposition,[],[f84,f6])).
% 0.77/0.37 thf(f576,plain,(
% 0.77/0.37 ($false = sF4) | spl15_5),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f575])).
% 0.77/0.37 thf(f577,plain,(
% 0.77/0.37 spl15_7 | spl15_5),
% 0.77/0.37 inference(avatar_split_clause,[],[f576,f83,f92])).
% 0.77/0.37 thf(f581,plain,(
% 0.77/0.37 ($true = ((f0 @ $false))) | (~spl15_7 | ~spl15_23)),
% 0.77/0.37 inference(forward_demodulation,[],[f167,f94])).
% 0.77/0.37 thf(f582,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_7 | ~spl15_23 | ~spl15_51 | ~spl15_55)),
% 0.77/0.37 inference(forward_demodulation,[],[f581,f462])).
% 0.77/0.37 thf(f583,plain,(
% 0.77/0.37 $false | (~spl15_7 | ~spl15_23 | ~spl15_51 | ~spl15_55)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f582])).
% 0.77/0.37 thf(f584,plain,(
% 0.77/0.37 ~spl15_7 | ~spl15_23 | ~spl15_51 | ~spl15_55),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f583])).
% 0.77/0.37 thf(f585,plain,(
% 0.77/0.37 ($true = ((f0 @ $false))) | (~spl15_52 | ~spl15_55)),
% 0.77/0.37 inference(forward_demodulation,[],[f298,f312])).
% 0.77/0.37 thf(f587,plain,(
% 0.77/0.37 ($false = ((f0 @ $false))) | (~spl15_7 | ~spl15_26)),
% 0.77/0.37 inference(forward_demodulation,[],[f180,f94])).
% 0.77/0.37 thf(f593,plain,(
% 0.77/0.37 (sF6 = $false) | ($true != $true) | spl15_20),
% 0.77/0.37 inference(constrained_superposition,[],[f152,f6])).
% 0.77/0.37 thf(f594,plain,(
% 0.77/0.37 (sF6 = $false) | spl15_20),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f593])).
% 0.77/0.37 thf(f595,plain,(
% 0.77/0.37 spl15_22 | spl15_20),
% 0.77/0.37 inference(avatar_split_clause,[],[f594,f151,f160])).
% 0.77/0.37 thf(f599,plain,(
% 0.77/0.37 ($false = sF5) | ($true != $true) | spl15_25),
% 0.77/0.37 inference(constrained_superposition,[],[f175,f6])).
% 0.77/0.37 thf(f600,plain,(
% 0.77/0.37 ($false = sF5) | spl15_25),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f599])).
% 0.77/0.37 thf(f601,plain,(
% 0.77/0.37 spl15_24 | spl15_25),
% 0.77/0.37 inference(avatar_split_clause,[],[f600,f174,f169])).
% 0.77/0.37 thf(f607,plain,(
% 0.77/0.37 (((f0 @ $true)) = $true) | (~spl15_21 | ~spl15_25)),
% 0.77/0.37 inference(forward_demodulation,[],[f158,f176])).
% 0.77/0.37 thf(f612,plain,(
% 0.77/0.37 $false | (spl15_8 | ~spl15_32 | ~spl15_43 | ~spl15_50)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f573,f535])).
% 0.77/0.37 thf(f613,plain,(
% 0.77/0.37 spl15_8 | ~spl15_32 | ~spl15_43 | ~spl15_50),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f612])).
% 0.77/0.37 thf(f614,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_18 | ~spl15_37 | ~spl15_65)),
% 0.77/0.37 inference(forward_demodulation,[],[f452,f506])).
% 0.77/0.37 thf(f615,plain,(
% 0.77/0.37 $false | (~spl15_18 | ~spl15_37 | ~spl15_65)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f614])).
% 0.77/0.37 thf(f616,plain,(
% 0.77/0.37 ~spl15_18 | ~spl15_37 | ~spl15_65),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f615])).
% 0.77/0.37 thf(f617,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | (~spl15_15 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f131,f230])).
% 0.77/0.37 thf(f618,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_15 | ~spl15_18 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f617,f506])).
% 0.77/0.37 thf(f619,plain,(
% 0.77/0.37 $false | (~spl15_15 | ~spl15_18 | ~spl15_37)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f618])).
% 0.77/0.37 thf(f620,plain,(
% 0.77/0.37 ~spl15_15 | ~spl15_18 | ~spl15_37),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f619])).
% 0.77/0.37 thf(f621,plain,(
% 0.77/0.37 (((f2 @ $true)) != $true) | (spl15_18 | ~spl15_37)),
% 0.77/0.37 inference(forward_demodulation,[],[f143,f230])).
% 0.77/0.37 thf(f622,plain,(
% 0.77/0.37 ($true != $true) | ($false = sF2) | spl15_16),
% 0.77/0.37 inference(constrained_superposition,[],[f134,f6])).
% 0.77/0.37 thf(f623,plain,(
% 0.77/0.37 ($false = sF2) | spl15_16),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f622])).
% 0.77/0.37 thf(f624,plain,(
% 0.77/0.37 spl15_17 | spl15_16),
% 0.77/0.37 inference(avatar_split_clause,[],[f623,f133,f138])).
% 0.77/0.37 thf(f628,plain,(
% 0.77/0.37 (sF3 = $false) | ($true != $true) | spl15_50),
% 0.77/0.37 inference(constrained_superposition,[],[f287,f6])).
% 0.77/0.37 thf(f629,plain,(
% 0.77/0.37 (sF3 = $false) | spl15_50),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f628])).
% 0.77/0.37 thf(f632,plain,(
% 0.77/0.37 spl15_47 | spl15_50),
% 0.77/0.37 inference(avatar_split_clause,[],[f629,f286,f273])).
% 0.77/0.37 thf(f636,plain,(
% 0.77/0.37 (((f1 @ $false)) = $false) | (~spl15_6 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f89,f275])).
% 0.77/0.37 thf(f640,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_17 | ~spl15_49)),
% 0.77/0.37 inference(forward_demodulation,[],[f284,f140])).
% 0.77/0.37 thf(f648,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_27 | ~spl15_29)),
% 0.77/0.37 inference(forward_demodulation,[],[f194,f185])).
% 0.77/0.37 thf(f649,plain,(
% 0.77/0.37 $false | (~spl15_27 | ~spl15_29)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f648])).
% 0.77/0.37 thf(f650,plain,(
% 0.77/0.37 ~spl15_27 | ~spl15_29),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f649])).
% 0.77/0.37 thf(f651,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_62 | ~spl15_64)),
% 0.77/0.37 inference(forward_demodulation,[],[f430,f416])).
% 0.77/0.37 thf(f652,plain,(
% 0.77/0.37 $false | (~spl15_62 | ~spl15_64)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f651])).
% 0.77/0.37 thf(f653,plain,(
% 0.77/0.37 ~spl15_62 | ~spl15_64),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f652])).
% 0.77/0.37 thf(f662,plain,(
% 0.77/0.37 (((f2 @ $true)) = $true) | (~spl15_28 | ~spl15_35)),
% 0.77/0.37 inference(forward_demodulation,[],[f221,f189])).
% 0.77/0.37 thf(f669,plain,(
% 0.77/0.37 (((f3 @ $true)) = $false) | (~spl15_28 | ~spl15_41)),
% 0.77/0.37 inference(forward_demodulation,[],[f248,f189])).
% 0.77/0.37 thf(f670,plain,(
% 0.77/0.37 spl15_62 | ~spl15_28 | ~spl15_41),
% 0.77/0.37 inference(avatar_split_clause,[],[f669,f246,f187,f414])).
% 0.77/0.37 thf(f673,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_7 | ~spl15_23 | ~spl15_26)),
% 0.77/0.37 inference(forward_demodulation,[],[f587,f581])).
% 0.77/0.37 thf(f674,plain,(
% 0.77/0.37 $false | (~spl15_7 | ~spl15_23 | ~spl15_26)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f673])).
% 0.77/0.37 thf(f675,plain,(
% 0.77/0.37 ~spl15_7 | ~spl15_23 | ~spl15_26),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f674])).
% 0.77/0.37 thf(f695,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_12 | ~spl15_17 | ~spl15_34 | ~spl15_49)),
% 0.77/0.37 inference(forward_demodulation,[],[f640,f531])).
% 0.77/0.37 thf(f696,plain,(
% 0.77/0.37 $false | (~spl15_12 | ~spl15_17 | ~spl15_34 | ~spl15_49)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f695])).
% 0.77/0.37 thf(f697,plain,(
% 0.77/0.37 ~spl15_12 | ~spl15_17 | ~spl15_34 | ~spl15_49),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f696])).
% 0.77/0.37 thf(f698,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_44 | ~spl15_46)),
% 0.77/0.37 inference(forward_demodulation,[],[f270,f261])).
% 0.77/0.37 thf(f699,plain,(
% 0.77/0.37 $false | (~spl15_44 | ~spl15_46)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f698])).
% 0.77/0.37 thf(f700,plain,(
% 0.77/0.37 ~spl15_44 | ~spl15_46),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f699])).
% 0.77/0.37 thf(f703,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_32 | ~spl15_33)),
% 0.77/0.37 inference(forward_demodulation,[],[f212,f207])).
% 0.77/0.37 thf(f704,plain,(
% 0.77/0.37 $false | (~spl15_32 | ~spl15_33)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f703])).
% 0.77/0.37 thf(f705,plain,(
% 0.77/0.37 ~spl15_32 | ~spl15_33),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f704])).
% 0.77/0.37 thf(f721,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_58 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f325,f330])).
% 0.77/0.37 thf(f722,plain,(
% 0.77/0.37 $false | (~spl15_58 | ~spl15_59)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f721])).
% 0.77/0.37 thf(f723,plain,(
% 0.77/0.37 ~spl15_58 | ~spl15_59),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f722])).
% 0.77/0.37 thf(f728,plain,(
% 0.77/0.37 ($false != ((f2 @ $true))) | (~spl15_10 | spl15_31)),
% 0.77/0.37 inference(forward_demodulation,[],[f202,f107])).
% 0.77/0.37 thf(f729,plain,(
% 0.77/0.37 ~spl15_65 | ~spl15_10 | spl15_31),
% 0.77/0.37 inference(avatar_split_clause,[],[f728,f201,f105,f450])).
% 0.77/0.37 thf(f732,plain,(
% 0.77/0.37 ($false = sF9) | ($true != $true) | spl15_10),
% 0.77/0.37 inference(constrained_superposition,[],[f106,f6])).
% 0.77/0.37 thf(f733,plain,(
% 0.77/0.37 ($false = sF9) | spl15_10),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f732])).
% 0.77/0.37 thf(f734,plain,(
% 0.77/0.37 spl15_12 | spl15_10),
% 0.77/0.37 inference(avatar_split_clause,[],[f733,f105,f114])).
% 0.77/0.37 thf(f738,plain,(
% 0.77/0.37 ($false = sF10) | ($true != $true) | spl15_32),
% 0.77/0.37 inference(constrained_superposition,[],[f206,f6])).
% 0.77/0.37 thf(f739,plain,(
% 0.77/0.37 ($false = sF10) | spl15_32),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f738])).
% 0.77/0.37 thf(f740,plain,(
% 0.77/0.37 spl15_33 | spl15_32),
% 0.77/0.37 inference(avatar_split_clause,[],[f739,f205,f210])).
% 0.77/0.37 thf(f746,plain,(
% 0.77/0.37 (((f1 @ $false)) = $true) | (~spl15_33 | ~spl15_43)),
% 0.77/0.37 inference(forward_demodulation,[],[f257,f212])).
% 0.77/0.37 thf(f748,plain,(
% 0.77/0.37 ($false = ((f1 @ $true))) | (~spl15_53 | ~spl15_58)),
% 0.77/0.37 inference(forward_demodulation,[],[f303,f325])).
% 0.77/0.37 thf(f749,plain,(
% 0.77/0.37 spl15_66 | ~spl15_53 | ~spl15_58),
% 0.77/0.37 inference(avatar_split_clause,[],[f748,f323,f301,f469])).
% 0.77/0.37 thf(f752,plain,(
% 0.77/0.37 ($false = ((f1 @ $true))) | (~spl15_46 | ~spl15_57)),
% 0.77/0.37 inference(forward_demodulation,[],[f321,f270])).
% 0.77/0.37 thf(f753,plain,(
% 0.77/0.37 spl15_66 | ~spl15_46 | ~spl15_57),
% 0.77/0.37 inference(avatar_split_clause,[],[f752,f319,f268,f469])).
% 0.77/0.37 thf(f764,plain,(
% 0.77/0.37 $false | (spl15_18 | ~spl15_28 | ~spl15_35 | ~spl15_37)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f662,f621])).
% 0.77/0.37 thf(f765,plain,(
% 0.77/0.37 spl15_18 | ~spl15_28 | ~spl15_35 | ~spl15_37),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f764])).
% 0.77/0.37 thf(f776,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_15 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f131,f225])).
% 0.77/0.37 thf(f781,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_30 | ~spl15_38)),
% 0.77/0.37 inference(forward_demodulation,[],[f234,f198])).
% 0.77/0.37 thf(f789,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_6 | ~spl15_33 | ~spl15_43 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f746,f636])).
% 0.77/0.37 thf(f790,plain,(
% 0.77/0.37 $false | (~spl15_6 | ~spl15_33 | ~spl15_43 | ~spl15_47)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f789])).
% 0.77/0.37 thf(f791,plain,(
% 0.77/0.37 ~spl15_6 | ~spl15_33 | ~spl15_43 | ~spl15_47),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f790])).
% 0.77/0.37 thf(f793,plain,(
% 0.77/0.37 (((f1 @ $false)) = $true) | (~spl15_8 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f98,f275])).
% 0.77/0.37 thf(f795,plain,(
% 0.77/0.37 (((f0 @ $true)) = $true) | (~spl15_5 | ~spl15_23)),
% 0.77/0.37 inference(forward_demodulation,[],[f167,f85])).
% 0.77/0.37 thf(f800,plain,(
% 0.77/0.37 (((f0 @ $true)) != $true) | (spl15_1 | ~spl15_20)),
% 0.77/0.37 inference(forward_demodulation,[],[f66,f153])).
% 0.77/0.37 thf(f814,plain,(
% 0.77/0.37 $false | (spl15_1 | ~spl15_20 | ~spl15_21 | ~spl15_25)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f800,f607])).
% 0.77/0.37 thf(f815,plain,(
% 0.77/0.37 spl15_1 | ~spl15_20 | ~spl15_21 | ~spl15_25),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f814])).
% 0.77/0.37 thf(f821,plain,(
% 0.77/0.37 ($true != ((f0 @ $false))) | (spl15_1 | ~spl15_22)),
% 0.77/0.37 inference(forward_demodulation,[],[f66,f162])).
% 0.77/0.37 thf(f822,plain,(
% 0.77/0.37 $false | (spl15_1 | ~spl15_22 | ~spl15_52 | ~spl15_55)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f821,f585])).
% 0.77/0.37 thf(f823,plain,(
% 0.77/0.37 spl15_1 | ~spl15_22 | ~spl15_52 | ~spl15_55),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f822])).
% 0.77/0.37 thf(f826,plain,(
% 0.77/0.37 ($false = ((f0 @ $false))) | (~spl15_3 | ~spl15_22)),
% 0.77/0.37 inference(forward_demodulation,[],[f76,f162])).
% 0.77/0.37 thf(f836,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_51 | ~spl15_52)),
% 0.77/0.37 inference(forward_demodulation,[],[f298,f293])).
% 0.77/0.37 thf(f837,plain,(
% 0.77/0.37 $false | (~spl15_51 | ~spl15_52)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f836])).
% 0.77/0.37 thf(f838,plain,(
% 0.77/0.37 ~spl15_51 | ~spl15_52),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f837])).
% 0.77/0.37 thf(f839,plain,(
% 0.77/0.37 ($true = ((f0 @ $false))) | (~spl15_1 | ~spl15_22)),
% 0.77/0.37 inference(forward_demodulation,[],[f67,f162])).
% 0.77/0.37 thf(f850,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_1 | ~spl15_3 | ~spl15_22)),
% 0.77/0.37 inference(forward_demodulation,[],[f839,f826])).
% 0.77/0.37 thf(f851,plain,(
% 0.77/0.37 $false | (~spl15_1 | ~spl15_3 | ~spl15_22)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f850])).
% 0.77/0.37 thf(f852,plain,(
% 0.77/0.37 ~spl15_1 | ~spl15_3 | ~spl15_22),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f851])).
% 0.77/0.37 thf(f854,plain,(
% 0.77/0.37 ($true != ((f0 @ $false))) | (spl15_52 | ~spl15_55)),
% 0.77/0.37 inference(forward_demodulation,[],[f297,f312])).
% 0.77/0.37 thf(f862,plain,(
% 0.77/0.37 $false | (~spl15_1 | ~spl15_22 | spl15_52 | ~spl15_55)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f854,f839])).
% 0.77/0.37 thf(f863,plain,(
% 0.77/0.37 ~spl15_1 | ~spl15_22 | spl15_52 | ~spl15_55),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f862])).
% 0.77/0.37 thf(f865,plain,(
% 0.77/0.37 (sF13 = $false) | (((f0 @ $true)) = $false) | ~spl15_51),
% 0.77/0.37 inference(constrained_superposition,[],[f293,f6])).
% 0.77/0.37 thf(f868,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | (~spl15_51 | spl15_55)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f865,f311])).
% 0.77/0.37 thf(f869,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_5 | ~spl15_23 | ~spl15_51 | spl15_55)),
% 0.77/0.37 inference(forward_demodulation,[],[f868,f795])).
% 0.77/0.37 thf(f870,plain,(
% 0.77/0.37 $false | (~spl15_5 | ~spl15_23 | ~spl15_51 | spl15_55)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f869])).
% 0.77/0.37 thf(f871,plain,(
% 0.77/0.37 ~spl15_5 | ~spl15_23 | ~spl15_51 | spl15_55),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f870])).
% 0.77/0.37 thf(f872,plain,(
% 0.77/0.37 (((f1 @ $false)) = $false) | (~spl15_33 | ~spl15_45)),
% 0.77/0.37 inference(forward_demodulation,[],[f266,f212])).
% 0.77/0.37 thf(f873,plain,(
% 0.77/0.37 (((f1 @ $false)) = $false) | (~spl15_6 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f89,f275])).
% 0.77/0.37 thf(f887,plain,(
% 0.77/0.37 (((f1 @ $false)) = $false) | (~spl15_44 | ~spl15_57)),
% 0.77/0.37 inference(forward_demodulation,[],[f321,f261])).
% 0.77/0.37 thf(f893,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_8 | ~spl15_33 | ~spl15_45 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f872,f793])).
% 0.77/0.37 thf(f894,plain,(
% 0.77/0.37 $false | (~spl15_8 | ~spl15_33 | ~spl15_45 | ~spl15_47)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f893])).
% 0.77/0.37 thf(f895,plain,(
% 0.77/0.37 ~spl15_8 | ~spl15_33 | ~spl15_45 | ~spl15_47),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f894])).
% 0.77/0.37 thf(f905,plain,(
% 0.77/0.37 ($false = sF12) | ($true != $true) | spl15_58),
% 0.77/0.37 inference(constrained_superposition,[],[f324,f6])).
% 0.77/0.37 thf(f906,plain,(
% 0.77/0.37 ($false = sF12) | spl15_58),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f905])).
% 0.77/0.37 thf(f907,plain,(
% 0.77/0.37 spl15_59 | spl15_58),
% 0.77/0.37 inference(avatar_split_clause,[],[f906,f323,f328])).
% 0.77/0.37 thf(f912,plain,(
% 0.77/0.37 (((f1 @ $false)) = $true) | (~spl15_56 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f316,f330])).
% 0.77/0.37 thf(f933,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_6 | ~spl15_47 | ~spl15_56 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f912,f873])).
% 0.77/0.37 thf(f934,plain,(
% 0.77/0.37 $false | (~spl15_6 | ~spl15_47 | ~spl15_56 | ~spl15_59)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f933])).
% 0.77/0.37 thf(f935,plain,(
% 0.77/0.37 ~spl15_6 | ~spl15_47 | ~spl15_56 | ~spl15_59),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f934])).
% 0.77/0.37 thf(f936,plain,(
% 0.77/0.37 (((f1 @ $false)) = $true) | (~spl15_44 | ~spl15_60)),
% 0.77/0.37 inference(forward_demodulation,[],[f334,f261])).
% 0.77/0.37 thf(f937,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_6 | ~spl15_44 | ~spl15_47 | ~spl15_60)),
% 0.77/0.37 inference(forward_demodulation,[],[f936,f873])).
% 0.77/0.37 thf(f938,plain,(
% 0.77/0.37 $false | (~spl15_6 | ~spl15_44 | ~spl15_47 | ~spl15_60)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f937])).
% 0.77/0.37 thf(f939,plain,(
% 0.77/0.37 ~spl15_6 | ~spl15_44 | ~spl15_47 | ~spl15_60),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f938])).
% 0.77/0.37 thf(f951,plain,(
% 0.77/0.37 ($false = ((f0 @ $false))) | (~spl15_19 | ~spl15_24)),
% 0.77/0.37 inference(forward_demodulation,[],[f149,f171])).
% 0.77/0.37 thf(f952,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_1 | ~spl15_19 | ~spl15_22 | ~spl15_24)),
% 0.77/0.37 inference(forward_demodulation,[],[f951,f839])).
% 0.77/0.37 thf(f953,plain,(
% 0.77/0.37 $false | (~spl15_1 | ~spl15_19 | ~spl15_22 | ~spl15_24)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f952])).
% 0.77/0.37 thf(f954,plain,(
% 0.77/0.37 ~spl15_1 | ~spl15_19 | ~spl15_22 | ~spl15_24),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f953])).
% 0.77/0.37 thf(f958,plain,(
% 0.77/0.37 (((f3 @ $false)) = $false) | (~spl15_9 | ~spl15_39)),
% 0.77/0.37 inference(forward_demodulation,[],[f103,f239])).
% 0.77/0.37 thf(f959,plain,(
% 0.77/0.37 (((f2 @ $false)) = $true) | (~spl15_18 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f144,f225])).
% 0.77/0.37 thf(f979,plain,(
% 0.77/0.37 (((f1 @ $true)) != $true) | (spl15_8 | ~spl15_50)),
% 0.77/0.37 inference(forward_demodulation,[],[f97,f288])).
% 0.77/0.37 thf(f982,plain,(
% 0.77/0.37 (((f2 @ $false)) != $false) | (~spl15_12 | spl15_31)),
% 0.77/0.37 inference(forward_demodulation,[],[f202,f116])).
% 0.77/0.37 thf(f984,plain,(
% 0.77/0.37 (((f2 @ $true)) = $true) | (~spl15_16 | ~spl15_48)),
% 0.77/0.37 inference(forward_demodulation,[],[f279,f135])).
% 0.77/0.37 thf(f993,plain,(
% 0.77/0.37 (((f1 @ $false)) = $true) | (~spl15_56 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f316,f330])).
% 0.77/0.37 thf(f1009,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_15 | ~spl15_18 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f959,f776])).
% 0.77/0.37 thf(f1010,plain,(
% 0.77/0.37 $false | (~spl15_15 | ~spl15_18 | ~spl15_36)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1009])).
% 0.77/0.37 thf(f1011,plain,(
% 0.77/0.37 ~spl15_15 | ~spl15_18 | ~spl15_36),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1010])).
% 0.77/0.37 thf(f1014,plain,(
% 0.77/0.37 ($true != $true) | (sF1 = $false) | spl15_37),
% 0.77/0.37 inference(constrained_superposition,[],[f229,f6])).
% 0.77/0.37 thf(f1015,plain,(
% 0.77/0.37 (sF1 = $false) | spl15_37),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1014])).
% 0.77/0.37 thf(f1016,plain,(
% 0.77/0.37 $false | (spl15_36 | spl15_37)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1015,f224])).
% 0.77/0.37 thf(f1017,plain,(
% 0.77/0.37 spl15_36 | spl15_37),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1016])).
% 0.77/0.37 thf(f1018,plain,(
% 0.77/0.37 spl15_36 | spl15_37),
% 0.77/0.37 inference(avatar_split_clause,[],[f1015,f228,f223])).
% 0.77/0.37 thf(f1027,plain,(
% 0.77/0.37 $false | (~spl15_12 | ~spl15_30 | spl15_31 | ~spl15_38)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f982,f781])).
% 0.77/0.37 thf(f1028,plain,(
% 0.77/0.37 ~spl15_12 | ~spl15_30 | spl15_31 | ~spl15_38),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1027])).
% 0.77/0.37 thf(f1029,plain,(
% 0.77/0.37 (((f3 @ $false)) != $false) | (spl15_27 | ~spl15_63)),
% 0.77/0.37 inference(forward_demodulation,[],[f184,f420])).
% 0.77/0.37 thf(f1033,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | (~spl15_28 | ~spl15_38)),
% 0.77/0.37 inference(forward_demodulation,[],[f234,f189])).
% 0.77/0.37 thf(f1034,plain,(
% 0.77/0.37 spl15_65 | ~spl15_28 | ~spl15_38),
% 0.77/0.37 inference(avatar_split_clause,[],[f1033,f232,f187,f450])).
% 0.77/0.37 thf(f1048,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_44 | ~spl15_56 | ~spl15_57 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f993,f887])).
% 0.77/0.37 thf(f1049,plain,(
% 0.77/0.37 $false | (~spl15_44 | ~spl15_56 | ~spl15_57 | ~spl15_59)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1048])).
% 0.77/0.37 thf(f1050,plain,(
% 0.77/0.37 ~spl15_44 | ~spl15_56 | ~spl15_57 | ~spl15_59),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1049])).
% 0.77/0.37 thf(f1077,plain,(
% 0.77/0.37 (((f0 @ $true)) != $false) | (spl15_51 | ~spl15_54)),
% 0.77/0.37 inference(constrained_superposition,[],[f292,f307])).
% 0.77/0.37 thf(f1079,plain,(
% 0.77/0.37 ~spl15_61 | spl15_51 | ~spl15_54),
% 0.77/0.37 inference(avatar_split_clause,[],[f1077,f305,f291,f375])).
% 0.77/0.37 thf(f1082,plain,(
% 0.77/0.37 $false | (~spl15_9 | spl15_27 | ~spl15_39 | ~spl15_63)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1029,f958])).
% 0.77/0.37 thf(f1083,plain,(
% 0.77/0.37 ~spl15_9 | spl15_27 | ~spl15_39 | ~spl15_63),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1082])).
% 0.77/0.37 thf(f1084,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_39 | ~spl15_42)),
% 0.77/0.37 inference(forward_demodulation,[],[f252,f239])).
% 0.77/0.37 thf(f1085,plain,(
% 0.77/0.37 $false | (~spl15_39 | ~spl15_42)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1084])).
% 0.77/0.37 thf(f1086,plain,(
% 0.77/0.37 ~spl15_39 | ~spl15_42),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1085])).
% 0.77/0.37 thf(f1088,plain,(
% 0.77/0.37 (((f3 @ $true)) = $true) | (~spl15_28 | ~spl15_40)),
% 0.77/0.37 inference(forward_demodulation,[],[f243,f189])).
% 0.77/0.37 thf(f1090,plain,(
% 0.77/0.37 spl15_64 | ~spl15_28 | ~spl15_40),
% 0.77/0.37 inference(avatar_split_clause,[],[f1088,f241,f187,f428])).
% 0.77/0.37 thf(f1094,plain,(
% 0.77/0.37 (((f3 @ $true)) != $false) | (spl15_9 | ~spl15_42)),
% 0.77/0.37 inference(forward_demodulation,[],[f102,f252])).
% 0.77/0.37 thf(f1095,plain,(
% 0.77/0.37 ~spl15_62 | spl15_9 | ~spl15_42),
% 0.77/0.37 inference(avatar_split_clause,[],[f1094,f250,f101,f414])).
% 0.77/0.37 thf(f1098,plain,(
% 0.77/0.37 (((f3 @ $true)) != $false) | (x = $false) | spl15_27),
% 0.77/0.37 inference(constrained_superposition,[],[f184,f6])).
% 0.77/0.37 thf(f1100,plain,(
% 0.77/0.37 ~spl15_62 | spl15_63 | spl15_27),
% 0.77/0.37 inference(avatar_split_clause,[],[f1098,f183,f418,f414])).
% 0.77/0.37 thf(f1104,plain,(
% 0.77/0.37 ($false = ((f2 @ $true))) | (~spl15_10 | ~spl15_31)),
% 0.77/0.37 inference(forward_demodulation,[],[f203,f107])).
% 0.77/0.37 thf(f1105,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_10 | ~spl15_16 | ~spl15_31 | ~spl15_48)),
% 0.77/0.37 inference(forward_demodulation,[],[f1104,f984])).
% 0.77/0.37 thf(f1106,plain,(
% 0.77/0.37 $false | (~spl15_10 | ~spl15_16 | ~spl15_31 | ~spl15_48)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1105])).
% 0.77/0.37 thf(f1107,plain,(
% 0.77/0.37 ~spl15_10 | ~spl15_16 | ~spl15_31 | ~spl15_48),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1106])).
% 0.77/0.37 thf(f1131,plain,(
% 0.77/0.37 (((f1 @ $true)) = $true) | (~spl15_56 | ~spl15_58)),
% 0.77/0.37 inference(forward_demodulation,[],[f316,f325])).
% 0.77/0.37 thf(f1132,plain,(
% 0.77/0.37 $false | (spl15_8 | ~spl15_50 | ~spl15_56 | ~spl15_58)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1131,f979])).
% 0.77/0.37 thf(f1133,plain,(
% 0.77/0.37 spl15_8 | ~spl15_50 | ~spl15_56 | ~spl15_58),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1132])).
% 0.77/0.37 thf(f1136,plain,(
% 0.77/0.37 (((f0 @ $true)) != $true) | (spl15_52 | ~spl15_54)),
% 0.77/0.37 inference(forward_demodulation,[],[f297,f307])).
% 0.77/0.37 thf(f1172,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_15 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f131,f225])).
% 0.77/0.37 thf(f1177,plain,(
% 0.77/0.37 (((f2 @ $false)) = $true) | (~spl15_17 | ~spl15_48)),
% 0.77/0.37 inference(forward_demodulation,[],[f279,f140])).
% 0.77/0.37 thf(f1188,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | ($true != $true) | (spl15_52 | ~spl15_54)),
% 0.77/0.37 inference(constrained_superposition,[],[f1136,f6])).
% 0.77/0.37 thf(f1189,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | (spl15_52 | ~spl15_54)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1188])).
% 0.77/0.37 thf(f1193,plain,(
% 0.77/0.37 spl15_61 | spl15_52 | ~spl15_54),
% 0.77/0.37 inference(avatar_split_clause,[],[f1189,f305,f296,f375])).
% 0.77/0.37 thf(f1206,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_15 | ~spl15_17 | ~spl15_36 | ~spl15_48)),
% 0.77/0.37 inference(forward_demodulation,[],[f1177,f1172])).
% 0.77/0.37 thf(f1207,plain,(
% 0.77/0.37 $false | (~spl15_15 | ~spl15_17 | ~spl15_36 | ~spl15_48)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1206])).
% 0.77/0.37 thf(f1208,plain,(
% 0.77/0.37 ~spl15_15 | ~spl15_17 | ~spl15_36 | ~spl15_48),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1207])).
% 0.77/0.37 thf(f1209,plain,(
% 0.77/0.37 (((f2 @ $false)) != $false) | (spl15_15 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f130,f225])).
% 0.77/0.37 thf(f1229,plain,(
% 0.77/0.37 (((f3 @ $false)) = $false) | (~spl15_27 | ~spl15_63)),
% 0.77/0.37 inference(forward_demodulation,[],[f185,f420])).
% 0.77/0.37 thf(f1231,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_12 | ~spl15_31)),
% 0.77/0.37 inference(forward_demodulation,[],[f203,f116])).
% 0.77/0.37 thf(f1233,plain,(
% 0.77/0.37 (((f2 @ $false)) = $false) | (~spl15_30 | ~spl15_38)),
% 0.77/0.37 inference(forward_demodulation,[],[f234,f198])).
% 0.77/0.37 thf(f1245,plain,(
% 0.77/0.37 $false | (~spl15_12 | spl15_15 | ~spl15_31 | ~spl15_36)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1231,f1209])).
% 0.77/0.37 thf(f1246,plain,(
% 0.77/0.37 ~spl15_12 | spl15_15 | ~spl15_31 | ~spl15_36),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1245])).
% 0.77/0.37 thf(f1247,plain,(
% 0.77/0.37 (((f2 @ $false)) = $true) | (~spl15_30 | ~spl15_35)),
% 0.77/0.37 inference(forward_demodulation,[],[f221,f198])).
% 0.77/0.37 thf(f1260,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_12 | ~spl15_30 | ~spl15_31 | ~spl15_35)),
% 0.77/0.37 inference(forward_demodulation,[],[f1247,f1231])).
% 0.77/0.37 thf(f1261,plain,(
% 0.77/0.37 $false | (~spl15_12 | ~spl15_30 | ~spl15_31 | ~spl15_35)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1260])).
% 0.77/0.37 thf(f1262,plain,(
% 0.77/0.37 ~spl15_12 | ~spl15_30 | ~spl15_31 | ~spl15_35),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1261])).
% 0.77/0.37 thf(f1264,plain,(
% 0.77/0.37 ($true != ((f0 @ $false))) | (~spl15_7 | spl15_23)),
% 0.77/0.37 inference(forward_demodulation,[],[f166,f94])).
% 0.77/0.37 thf(f1292,plain,(
% 0.77/0.37 (((f2 @ $false)) != $false) | (spl15_15 | ~spl15_36)),
% 0.77/0.37 inference(forward_demodulation,[],[f130,f225])).
% 0.77/0.37 thf(f1294,plain,(
% 0.77/0.37 ($true = ((f0 @ $false))) | (~spl15_21 | ~spl15_24)),
% 0.77/0.37 inference(forward_demodulation,[],[f158,f171])).
% 0.77/0.37 thf(f1313,plain,(
% 0.77/0.37 (((f3 @ $false)) = $true) | (~spl15_30 | ~spl15_40)),
% 0.77/0.37 inference(forward_demodulation,[],[f243,f198])).
% 0.77/0.37 thf(f1315,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_27 | ~spl15_30 | ~spl15_40 | ~spl15_63)),
% 0.77/0.37 inference(forward_demodulation,[],[f1313,f1229])).
% 0.77/0.37 thf(f1316,plain,(
% 0.77/0.37 $false | (~spl15_27 | ~spl15_30 | ~spl15_40 | ~spl15_63)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1315])).
% 0.77/0.37 thf(f1317,plain,(
% 0.77/0.37 ~spl15_27 | ~spl15_30 | ~spl15_40 | ~spl15_63),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1316])).
% 0.77/0.37 thf(f1320,plain,(
% 0.77/0.37 (((f3 @ $false)) = $false) | (~spl15_30 | ~spl15_41)),
% 0.77/0.37 inference(forward_demodulation,[],[f248,f198])).
% 0.77/0.37 thf(f1326,plain,(
% 0.77/0.37 (((f3 @ $false)) != $false) | (spl15_9 | ~spl15_39)),
% 0.77/0.37 inference(forward_demodulation,[],[f102,f239])).
% 0.77/0.37 thf(f1328,plain,(
% 0.77/0.37 (((f3 @ $true)) = $false) | (x = $false) | ~spl15_27),
% 0.77/0.37 inference(constrained_superposition,[],[f185,f6])).
% 0.77/0.37 thf(f1331,plain,(
% 0.77/0.37 (((f3 @ $true)) = $false) | (~spl15_27 | spl15_63)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1328,f419])).
% 0.77/0.37 thf(f1332,plain,(
% 0.77/0.37 spl15_62 | ~spl15_27 | spl15_63),
% 0.77/0.37 inference(avatar_split_clause,[],[f1331,f418,f183,f414])).
% 0.77/0.37 thf(f1339,plain,(
% 0.77/0.37 $false | (spl15_15 | ~spl15_30 | ~spl15_36 | ~spl15_38)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1292,f1233])).
% 0.77/0.37 thf(f1340,plain,(
% 0.77/0.37 spl15_15 | ~spl15_30 | ~spl15_36 | ~spl15_38),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1339])).
% 0.77/0.37 thf(f1347,plain,(
% 0.77/0.37 $false | (~spl15_7 | ~spl15_21 | spl15_23 | ~spl15_24)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1294,f1264])).
% 0.77/0.37 thf(f1348,plain,(
% 0.77/0.37 ~spl15_7 | ~spl15_21 | spl15_23 | ~spl15_24),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1347])).
% 0.77/0.37 thf(f1351,plain,(
% 0.77/0.37 (((f0 @ $true)) = $true) | (~spl15_1 | ~spl15_20)),
% 0.77/0.37 inference(forward_demodulation,[],[f67,f153])).
% 0.77/0.37 thf(f1361,plain,(
% 0.77/0.37 $false | (spl15_9 | ~spl15_30 | ~spl15_39 | ~spl15_41)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1326,f1320])).
% 0.77/0.37 thf(f1362,plain,(
% 0.77/0.37 spl15_9 | ~spl15_30 | ~spl15_39 | ~spl15_41),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1361])).
% 0.77/0.37 thf(f1380,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_1 | ~spl15_20 | ~spl15_61)),
% 0.77/0.37 inference(forward_demodulation,[],[f377,f1351])).
% 0.77/0.37 thf(f1381,plain,(
% 0.77/0.37 $false | (~spl15_1 | ~spl15_20 | ~spl15_61)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1380])).
% 0.77/0.37 thf(f1382,plain,(
% 0.77/0.37 ~spl15_1 | ~spl15_20 | ~spl15_61),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1381])).
% 0.77/0.37 thf(f1387,plain,(
% 0.77/0.37 (((f0 @ $true)) != $true) | (spl15_1 | ~spl15_20)),
% 0.77/0.37 inference(forward_demodulation,[],[f66,f153])).
% 0.77/0.37 thf(f1415,plain,(
% 0.77/0.37 (((f1 @ $false)) != $false) | (spl15_6 | ~spl15_47)),
% 0.77/0.37 inference(forward_demodulation,[],[f88,f275])).
% 0.77/0.37 thf(f1426,plain,(
% 0.77/0.37 (((f1 @ $false)) = $false) | (~spl15_53 | ~spl15_59)),
% 0.77/0.37 inference(forward_demodulation,[],[f303,f330])).
% 0.77/0.37 thf(f1435,plain,(
% 0.77/0.37 ($true != $true) | (((f0 @ $true)) = $false) | (spl15_1 | ~spl15_20)),
% 0.77/0.37 inference(constrained_superposition,[],[f1387,f6])).
% 0.77/0.37 thf(f1439,plain,(
% 0.77/0.37 (((f0 @ $true)) = $false) | (spl15_1 | ~spl15_20)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1435])).
% 0.77/0.37 thf(f1440,plain,(
% 0.77/0.37 spl15_61 | spl15_1 | ~spl15_20),
% 0.77/0.37 inference(avatar_split_clause,[],[f1439,f151,f65,f375])).
% 0.77/0.37 thf(f1446,plain,(
% 0.77/0.37 $false | (spl15_6 | ~spl15_47 | ~spl15_53 | ~spl15_59)),
% 0.77/0.37 inference(forward_subsumption_resolution,[],[f1426,f1415])).
% 0.77/0.37 thf(f1447,plain,(
% 0.77/0.37 spl15_6 | ~spl15_47 | ~spl15_53 | ~spl15_59),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1446])).
% 0.77/0.37 thf(f1448,plain,(
% 0.77/0.37 (((f1 @ $true)) = $true) | (~spl15_46 | ~spl15_60)),
% 0.77/0.37 inference(forward_demodulation,[],[f334,f270])).
% 0.77/0.37 thf(f1467,plain,(
% 0.77/0.37 ($false = $true) | (~spl15_46 | ~spl15_60 | ~spl15_66)),
% 0.77/0.37 inference(forward_demodulation,[],[f471,f1448])).
% 0.77/0.37 thf(f1468,plain,(
% 0.77/0.37 $false | (~spl15_46 | ~spl15_60 | ~spl15_66)),
% 0.77/0.37 inference(trivial_inequality_removal,[],[f1467])).
% 0.77/0.37 thf(f1469,plain,(
% 0.77/0.37 ~spl15_46 | ~spl15_60 | ~spl15_66),
% 0.77/0.37 inference(avatar_contradiction_clause,[],[f1468])).
% 0.77/0.37 cnf(s1, plain, spl15_1 | spl15_2, inference(sat_conversion,[],[f72])).
% 0.77/0.37 cnf(s2, plain, spl15_3 | spl15_4, inference(sat_conversion,[],[f81])).
% 0.77/0.37 cnf(s3, plain, spl15_5 | spl15_6, inference(sat_conversion,[],[f90])).
% 0.77/0.37 cnf(s4, plain, spl15_7 | spl15_8, inference(sat_conversion,[],[f99])).
% 0.77/0.37 cnf(s5, plain, spl15_9 | spl15_10, inference(sat_conversion,[],[f108])).
% 0.77/0.37 cnf(s6, plain, spl15_11 | spl15_12, inference(sat_conversion,[],[f117])).
% 0.77/0.37 cnf(s7, plain, spl15_2 | spl15_13, inference(sat_conversion,[],[f122])).
% 0.77/0.37 cnf(s8, plain, spl15_4 | spl15_14, inference(sat_conversion,[],[f127])).
% 0.77/0.37 cnf(s9, plain, spl15_15 | spl15_16, inference(sat_conversion,[],[f136])).
% 0.77/0.37 cnf(s10, plain, spl15_17 | spl15_18, inference(sat_conversion,[],[f145])).
% 0.77/0.37 cnf(s11, plain, spl15_19 | spl15_20, inference(sat_conversion,[],[f154])).
% 0.77/0.37 cnf(s12, plain, spl15_21 | spl15_22, inference(sat_conversion,[],[f163])).
% 0.77/0.37 cnf(s13, plain, spl15_23 | spl15_24, inference(sat_conversion,[],[f172])).
% 0.77/0.37 cnf(s14, plain, spl15_25 | spl15_26, inference(sat_conversion,[],[f181])).
% 0.77/0.37 cnf(s15, plain, spl15_27 | spl15_28, inference(sat_conversion,[],[f190])).
% 0.77/0.37 cnf(s16, plain, spl15_29 | spl15_30, inference(sat_conversion,[],[f199])).
% 0.77/0.37 cnf(s17, plain, spl15_31 | spl15_32, inference(sat_conversion,[],[f208])).
% 0.77/0.37 cnf(s18, plain, spl15_33 | spl15_34, inference(sat_conversion,[],[f217])).
% 0.77/0.37 cnf(s19, plain, spl15_35 | spl15_36, inference(sat_conversion,[],[f226])).
% 0.77/0.37 cnf(s20, plain, spl15_37 | spl15_38, inference(sat_conversion,[],[f235])).
% 0.77/0.37 cnf(s21, plain, spl15_39 | spl15_40, inference(sat_conversion,[],[f244])).
% 0.77/0.37 cnf(s22, plain, spl15_41 | spl15_42, inference(sat_conversion,[],[f253])).
% 0.77/0.37 cnf(s23, plain, spl15_43 | spl15_44, inference(sat_conversion,[],[f262])).
% 0.77/0.37 cnf(s24, plain, spl15_45 | spl15_46, inference(sat_conversion,[],[f271])).
% 0.77/0.37 cnf(s25, plain, spl15_47 | spl15_48, inference(sat_conversion,[],[f280])).
% 0.77/0.37 cnf(s26, plain, spl15_49 | spl15_50, inference(sat_conversion,[],[f289])).
% 0.77/0.37 cnf(s27, plain, spl15_14 | spl15_51, inference(sat_conversion,[],[f294])).
% 0.77/0.37 cnf(s28, plain, spl15_13 | spl15_52, inference(sat_conversion,[],[f299])).
% 0.77/0.37 cnf(s29, plain, spl15_53 | spl15_54, inference(sat_conversion,[],[f308])).
% 0.77/0.37 cnf(s30, plain, spl15_55 | spl15_56, inference(sat_conversion,[],[f317])).
% 0.77/0.37 cnf(s31, plain, spl15_57 | spl15_58, inference(sat_conversion,[],[f326])).
% 0.77/0.37 cnf(s32, plain, spl15_59 | spl15_60, inference(sat_conversion,[],[f335])).
% 0.77/0.37 cnf(s33, plain, ~spl15_13 | ~spl15_14, inference(sat_conversion,[],[f338])).
% 0.77/0.37 cnf(s34, plain, ~spl15_2 | ~spl15_4, inference(sat_conversion,[],[f342])).
% 0.77/0.37 cnf(s35, plain, ~spl15_5 | ~spl15_7, inference(sat_conversion,[],[f347])).
% 0.77/0.37 cnf(s36, plain, ~spl15_3 | spl15_22 | spl15_61, inference(sat_conversion,[],[f378])).
% 0.77/0.37 cnf(s37, plain, ~spl15_19 | ~spl15_25 | spl15_61, inference(sat_conversion,[],[f387])).
% 0.77/0.37 cnf(s38, plain, ~spl15_20 | ~spl15_22, inference(sat_conversion,[],[f391])).
% 0.77/0.37 cnf(s40, plain, ~spl15_5 | ~spl15_26 | spl15_61, inference(sat_conversion,[],[f395])).
% 0.77/0.37 cnf(s48, plain, spl15_28 | spl15_30, inference(sat_conversion,[],[f437])).
% 0.77/0.37 cnf(s54, plain, ~spl15_9 | ~spl15_11, inference(sat_conversion,[],[f490])).
% 0.77/0.37 cnf(s57, plain, ~spl15_15 | ~spl15_37 | spl15_65, inference(sat_conversion,[],[f500])).
% 0.77/0.37 cnf(s59, plain, spl15_15 | ~spl15_37 | ~spl15_65, inference(sat_conversion,[],[f505])).
% 0.77/0.37 cnf(s60, plain, ~spl15_16 | ~spl15_49 | spl15_65, inference(sat_conversion,[],[f509])).
% 0.77/0.37 cnf(s64, plain, ~spl15_31 | ~spl15_34, inference(sat_conversion,[],[f530])).
% 0.77/0.37 cnf(s65, plain, ~spl15_32 | ~spl15_45 | spl15_66, inference(sat_conversion,[],[f537])).
% 0.77/0.37 cnf(s67, plain, ~spl15_30 | ~spl15_40 | ~spl15_41, inference(sat_conversion,[],[f549])).
% 0.77/0.37 cnf(s68, plain, ~spl15_9 | spl15_39 | spl15_62, inference(sat_conversion,[],[f551])).
% 0.77/0.37 cnf(s69, plain, ~spl15_8 | ~spl15_50 | ~spl15_66, inference(sat_conversion,[],[f571])).
% 0.77/0.37 cnf(s70, plain, ~spl15_6 | ~spl15_50 | spl15_66, inference(sat_conversion,[],[f574])).
% 0.77/0.37 cnf(s71, plain, spl15_5 | spl15_7, inference(sat_conversion,[],[f577])).
% 0.77/0.37 cnf(s72, plain, ~spl15_7 | ~spl15_23 | ~spl15_51 | ~spl15_55, inference(sat_conversion,[],[f584])).
% 0.77/0.37 cnf(s73, plain, spl15_20 | spl15_22, inference(sat_conversion,[],[f595])).
% 0.77/0.37 cnf(s74, plain, spl15_24 | spl15_25, inference(sat_conversion,[],[f601])).
% 0.77/0.37 cnf(s77, plain, spl15_8 | ~spl15_32 | ~spl15_43 | ~spl15_50, inference(sat_conversion,[],[f613])).
% 0.77/0.37 cnf(s78, plain, ~spl15_18 | ~spl15_37 | ~spl15_65, inference(sat_conversion,[],[f616])).
% 0.77/0.37 cnf(s79, plain, ~spl15_15 | ~spl15_18 | ~spl15_37, inference(sat_conversion,[],[f620])).
% 0.77/0.37 cnf(s81, plain, spl15_16 | spl15_17, inference(sat_conversion,[],[f624])).
% 0.77/0.37 cnf(s83, plain, spl15_47 | spl15_50, inference(sat_conversion,[],[f632])).
% 0.77/0.37 cnf(s86, plain, ~spl15_27 | ~spl15_29, inference(sat_conversion,[],[f650])).
% 0.77/0.37 cnf(s87, plain, ~spl15_62 | ~spl15_64, inference(sat_conversion,[],[f653])).
% 0.77/0.37 cnf(s91, plain, ~spl15_28 | ~spl15_41 | spl15_62, inference(sat_conversion,[],[f670])).
% 0.77/0.37 cnf(s92, plain, ~spl15_7 | ~spl15_23 | ~spl15_26, inference(sat_conversion,[],[f675])).
% 0.77/0.37 cnf(s95, plain, ~spl15_12 | ~spl15_17 | ~spl15_34 | ~spl15_49, inference(sat_conversion,[],[f697])).
% 0.77/0.37 cnf(s96, plain, ~spl15_44 | ~spl15_46, inference(sat_conversion,[],[f700])).
% 0.77/0.37 cnf(s97, plain, ~spl15_32 | ~spl15_33, inference(sat_conversion,[],[f705])).
% 0.77/0.37 cnf(s100, plain, ~spl15_58 | ~spl15_59, inference(sat_conversion,[],[f723])).
% 0.77/0.37 cnf(s101, plain, ~spl15_10 | spl15_31 | ~spl15_65, inference(sat_conversion,[],[f729])).
% 0.77/0.37 cnf(s102, plain, spl15_10 | spl15_12, inference(sat_conversion,[],[f734])).
% 0.77/0.37 cnf(s103, plain, spl15_32 | spl15_33, inference(sat_conversion,[],[f740])).
% 0.77/0.37 cnf(s104, plain, ~spl15_53 | ~spl15_58 | spl15_66, inference(sat_conversion,[],[f749])).
% 0.77/0.37 cnf(s106, plain, ~spl15_46 | ~spl15_57 | spl15_66, inference(sat_conversion,[],[f753])).
% 0.77/0.37 cnf(s108, plain, spl15_18 | ~spl15_28 | ~spl15_35 | ~spl15_37, inference(sat_conversion,[],[f765])).
% 0.77/0.37 cnf(s110, plain, ~spl15_6 | ~spl15_33 | ~spl15_43 | ~spl15_47, inference(sat_conversion,[],[f791])).
% 0.77/0.37 cnf(s113, plain, spl15_1 | ~spl15_20 | ~spl15_21 | ~spl15_25, inference(sat_conversion,[],[f815])).
% 0.77/0.37 cnf(s115, plain, spl15_1 | ~spl15_22 | ~spl15_52 | ~spl15_55, inference(sat_conversion,[],[f823])).
% 0.77/0.37 cnf(s118, plain, ~spl15_51 | ~spl15_52, inference(sat_conversion,[],[f838])).
% 0.77/0.37 cnf(s119, plain, ~spl15_1 | ~spl15_3 | ~spl15_22, inference(sat_conversion,[],[f852])).
% 0.77/0.37 cnf(s120, plain, ~spl15_1 | ~spl15_22 | spl15_52 | ~spl15_55, inference(sat_conversion,[],[f863])).
% 0.77/0.37 cnf(s121, plain, ~spl15_5 | ~spl15_23 | ~spl15_51 | spl15_55, inference(sat_conversion,[],[f871])).
% 0.77/0.37 cnf(s124, plain, ~spl15_8 | ~spl15_33 | ~spl15_45 | ~spl15_47, inference(sat_conversion,[],[f895])).
% 0.77/0.37 cnf(s126, plain, spl15_58 | spl15_59, inference(sat_conversion,[],[f907])).
% 0.77/0.37 cnf(s130, plain, ~spl15_6 | ~spl15_47 | ~spl15_56 | ~spl15_59, inference(sat_conversion,[],[f935])).
% 0.77/0.37 cnf(s131, plain, ~spl15_6 | ~spl15_44 | ~spl15_47 | ~spl15_60, inference(sat_conversion,[],[f939])).
% 0.77/0.37 cnf(s133, plain, ~spl15_1 | ~spl15_19 | ~spl15_22 | ~spl15_24, inference(sat_conversion,[],[f954])).
% 0.77/0.37 cnf(s140, plain, ~spl15_15 | ~spl15_18 | ~spl15_36, inference(sat_conversion,[],[f1011])).
% 0.77/0.37 cnf(s141, plain, spl15_36 | spl15_37, inference(sat_conversion,[],[f1017])).
% 0.77/0.37 cnf(s142, plain, spl15_36 | spl15_37, inference(sat_conversion,[],[f1018])).
% 0.77/0.37 cnf(s143, plain, ~spl15_12 | ~spl15_30 | spl15_31 | ~spl15_38, inference(sat_conversion,[],[f1028])).
% 0.77/0.37 cnf(s144, plain, ~spl15_28 | ~spl15_38 | spl15_65, inference(sat_conversion,[],[f1034])).
% 0.77/0.37 cnf(s147, plain, ~spl15_44 | ~spl15_56 | ~spl15_57 | ~spl15_59, inference(sat_conversion,[],[f1050])).
% 0.77/0.37 cnf(s152, plain, spl15_51 | ~spl15_54 | ~spl15_61, inference(sat_conversion,[],[f1079])).
% 0.77/0.37 cnf(s153, plain, ~spl15_9 | spl15_27 | ~spl15_39 | ~spl15_63, inference(sat_conversion,[],[f1083])).
% 0.77/0.37 cnf(s154, plain, ~spl15_39 | ~spl15_42, inference(sat_conversion,[],[f1086])).
% 0.77/0.37 cnf(s156, plain, ~spl15_28 | ~spl15_40 | spl15_64, inference(sat_conversion,[],[f1090])).
% 0.77/0.37 cnf(s157, plain, spl15_9 | ~spl15_42 | ~spl15_62, inference(sat_conversion,[],[f1095])).
% 0.77/0.37 cnf(s159, plain, spl15_27 | ~spl15_62 | spl15_63, inference(sat_conversion,[],[f1100])).
% 0.77/0.37 cnf(s161, plain, ~spl15_10 | ~spl15_16 | ~spl15_31 | ~spl15_48, inference(sat_conversion,[],[f1107])).
% 0.77/0.37 cnf(s165, plain, spl15_8 | ~spl15_50 | ~spl15_56 | ~spl15_58, inference(sat_conversion,[],[f1133])).
% 0.77/0.37 cnf(s175, plain, spl15_52 | ~spl15_54 | spl15_61, inference(sat_conversion,[],[f1193])).
% 0.77/0.37 cnf(s177, plain, ~spl15_15 | ~spl15_17 | ~spl15_36 | ~spl15_48, inference(sat_conversion,[],[f1208])).
% 0.77/0.37 cnf(s181, plain, ~spl15_12 | spl15_15 | ~spl15_31 | ~spl15_36, inference(sat_conversion,[],[f1246])).
% 0.77/0.37 cnf(s183, plain, ~spl15_12 | ~spl15_30 | ~spl15_31 | ~spl15_35, inference(sat_conversion,[],[f1262])).
% 0.77/0.37 cnf(s189, plain, ~spl15_27 | ~spl15_30 | ~spl15_40 | ~spl15_63, inference(sat_conversion,[],[f1317])).
% 0.77/0.37 cnf(s191, plain, ~spl15_27 | spl15_62 | spl15_63, inference(sat_conversion,[],[f1332])).
% 0.77/0.37 cnf(s192, plain, spl15_15 | ~spl15_30 | ~spl15_36 | ~spl15_38, inference(sat_conversion,[],[f1340])).
% 0.77/0.37 cnf(s193, plain, ~spl15_7 | ~spl15_21 | spl15_23 | ~spl15_24, inference(sat_conversion,[],[f1348])).
% 0.77/0.37 cnf(s195, plain, spl15_9 | ~spl15_30 | ~spl15_39 | ~spl15_41, inference(sat_conversion,[],[f1362])).
% 0.77/0.37 cnf(s197, plain, ~spl15_1 | ~spl15_20 | ~spl15_61, inference(sat_conversion,[],[f1382])).
% 0.77/0.37 cnf(s203, plain, spl15_1 | ~spl15_20 | spl15_61, inference(sat_conversion,[],[f1440])).
% 0.77/0.37 cnf(s205, plain, spl15_6 | ~spl15_47 | ~spl15_53 | ~spl15_59, inference(sat_conversion,[],[f1447])).
% 0.77/0.37 cnf(s208, plain, ~spl15_46 | ~spl15_60 | ~spl15_66, inference(sat_conversion,[],[f1469])).
% 0.77/0.37 cnf(s210, plain, ~spl15_20 | ~spl15_7 | spl15_1, inference(rat,[],[s92,s193,s14,s74,s113,s12,s38])).
% 0.77/0.37 cnf(s211, plain, spl15_31 | ~spl15_16 | ~spl15_10 | spl15_8 | ~spl15_56, inference(rat,[],[s147,s23,s31,s126,s77,s165,s26,s60,s17,s101])).
% 0.77/0.37 cnf(s212, plain, ~spl15_16 | ~spl15_10 | spl15_8 | ~spl15_56 | ~spl15_6, inference(rat,[],[s131,s32,s23,s130,s110,s25,s18,s161,s64,s211])).
% 0.77/0.37 cnf(s213, plain, ~spl15_40 | spl15_28 | spl15_9, inference(rat,[],[s157,s191,s22,s189,s67,s48,s15])).
% 0.77/0.37 cnf(s214, plain, spl15_28 | spl15_9, inference(rat,[],[s22,s195,s154,s21,s213,s48])).
% 0.77/0.37 cnf(s215, plain, spl15_65 | ~spl15_28 | ~spl15_15, inference(rat,[],[s20,s144,s57])).
% 0.77/0.37 cnf(s216, plain, ~spl15_47 | ~spl15_33 | ~spl15_56 | ~spl15_6, inference(rat,[],[s131,s23,s32,s110,s130])).
% 0.77/0.37 cnf(s217, plain, spl15_9 | spl15_8 | ~spl15_56 | ~spl15_6, inference(rat,[],[s108,s78,s19,s142,s177,s25,s216,s18,s64,s101,s215,s214,s9,s81,s212,s5])).
% 0.77/0.37 cnf(s219, plain, ~spl15_50 | ~spl15_32 | spl15_8 | ~spl15_56, inference(rat,[],[s147,s23,s31,s126,s77,s165])).
% 0.77/0.37 cnf(s220, plain, ~spl15_18 | ~spl15_15, inference(rat,[],[s141,s79,s140])).
% 0.77/0.37 cnf(s221, plain, spl15_39 | ~spl15_28 | ~spl15_9, inference(rat,[],[s87,s156,s68,s21])).
% 0.77/0.37 cnf(s222, plain, spl15_30 | ~spl15_9, inference(rat,[],[s91,s159,s22,s153,s154,s221,s86,s16,s48])).
% 0.77/0.37 cnf(s223, plain, ~spl15_32 | ~spl15_17 | ~spl15_12 | spl15_8 | ~spl15_56, inference(rat,[],[s95,s26,s18,s219,s97])).
% 0.77/0.37 cnf(s224, plain, ~spl15_15 | spl15_8 | ~spl15_56 | ~spl15_6, inference(rat,[],[s177,s19,s25,s183,s216,s17,s103,s223,s10,s220,s6,s54,s222,s217])).
% 0.77/0.37 cnf(s225, plain, spl15_31 | spl15_15 | ~spl15_30 | ~spl15_12 | spl15_8 | ~spl15_56, inference(rat,[],[s60,s59,s26,s20,s219,s143,s17,s9])).
% 0.77/0.37 cnf(s226, plain, spl15_15 | ~spl15_30 | ~spl15_56 | ~spl15_12 | spl15_8, inference(rat,[],[s19,s181,s183,s225])).
% 0.77/0.37 cnf(s227, plain, spl15_8 | ~spl15_6 | ~spl15_56, inference(rat,[],[s226,s224,s222,s6,s54,s217])).
% 0.77/0.37 cnf(s228, plain, spl15_9 | spl15_31 | ~spl15_15, inference(rat,[],[s215,s101,s214,s5])).
% 0.77/0.37 cnf(s229, plain, ~spl15_50 | ~spl15_8 | ~spl15_6, inference(rat,[],[s69,s70])).
% 0.77/0.37 cnf(s230, plain, ~spl15_15 | ~spl15_34 | ~spl15_49, inference(rat,[],[s54,s6,s228,s95,s10,s220,s64])).
% 0.77/0.37 cnf(s231, plain, ~spl15_6 | ~spl15_56, inference(rat,[],[s222,s192,s5,s20,s142,s101,s59,s60,s9,s230,s64,s18,s216,s26,s83,s229,s227])).
% 0.77/0.37 cnf(s232, plain, spl15_5 | spl15_1, inference(rat,[],[s231,s30,s115,s73,s210,s3,s71,s28,s33,s8,s34,s1])).
% 0.77/0.37 cnf(s233, plain, spl15_61 | spl15_1, inference(rat,[],[s37,s14,s11,s40,s203,s232])).
% 0.77/0.37 cnf(s234, plain, spl15_59 | spl15_1, inference(rat,[],[s222,s192,s5,s20,s142,s101,s59,s60,s9,s230,s64,s18,s124,s26,s83,s24,s69,s208,s104,s32,s126,s4,s35,s232,s29,s152,s233,s118,s28,s33,s8,s34,s1])).
% 0.77/0.37 cnf(s235, plain, ~spl15_32 | ~spl15_15 | spl15_1, inference(rat,[],[s24,s106,s65,s69,s26,s230,s18,s97,s4,s35,s232,s31,s100,s234])).
% 0.77/0.37 cnf(s236, plain, ~spl15_6 | ~spl15_33 | ~spl15_8, inference(rat,[],[s96,s23,s24,s110,s124,s83,s229])).
% 0.77/0.37 cnf(s237, plain, ~spl15_15 | spl15_1, inference(rat,[],[s6,s54,s183,s214,s48,s108,s19,s142,s177,s25,s205,s236,s17,s103,s235,s10,s220,s4,s35,s232,s29,s152,s233,s118,s28,s33,s8,s34,s1,s234])).
% 0.77/0.37 cnf(s238, plain, ~spl15_65 | spl15_31 | spl15_15, inference(rat,[],[s222,s192,s5,s20,s142,s101,s59])).
% 0.77/0.37 cnf(s239, plain, spl15_31 | spl15_1, inference(rat,[],[s24,s106,s65,s69,s26,s60,s238,s17,s4,s35,s232,s31,s100,s234,s9,s237])).
% 0.77/0.37 cnf(s240, plain, spl15_1, inference(rat,[],[s183,s19,s222,s181,s5,s102,s161,s25,s205,s236,s18,s64,s239,s9,s237,s234,s29,s152,s233,s4,s35,s232,s118,s28,s33,s8,s34,s1])).
% 0.77/0.37 cnf(s241, plain, ~spl15_3, inference(rat,[],[s197,s36,s73,s119,s240])).
% 0.77/0.37 cnf(s242, plain, spl15_4, inference(rat,[],[s2,s241])).
% 0.77/0.37 cnf(s243, plain, ~spl15_2, inference(rat,[],[s34,s242])).
% 0.77/0.37 cnf(s244, plain, spl15_13, inference(rat,[],[s7,s243])).
% 0.77/0.37 cnf(s245, plain, ~spl15_14, inference(rat,[],[s33,s244])).
% 0.77/0.37 cnf(s246, plain, spl15_51, inference(rat,[],[s27,s245])).
% 0.77/0.37 cnf(s247, plain, ~spl15_52, inference(rat,[],[s118,s246])).
% 0.77/0.37 cnf(s248, plain, ~spl15_7, inference(rat,[],[s193,s13,s12,s72,s120,s30,s231,s3,s35,s246,s240,s247])).
% 0.77/0.37 cnf(s249, plain, spl15_5, inference(rat,[],[s71,s248])).
% 0.77/0.37 cnf(s250, plain, spl15_8, inference(rat,[],[s4,s248])).
% 0.77/0.37 cnf(s251, plain, spl15_20, inference(rat,[],[s13,s121,s133,s120,s11,s73,s246,s249,s240,s247])).
% 0.77/0.37 cnf(s252, plain, ~spl15_61, inference(rat,[],[s197,s240,s251])).
% 0.77/0.37 cnf(s255, plain, ~spl15_54, inference(rat,[],[s175,s247,s252])).
% 0.77/0.37 cnf(s259, plain, spl15_53, inference(rat,[],[s29,s255])).
% 0.77/0.37 cnf(s263, plain, spl15_66 | ~spl15_32, inference(rat,[],[s106,s31,s24,s104,s65,s259])).
% 0.77/0.37 cnf(s264, plain, ~spl15_32 | ~spl15_15, inference(rat,[],[s263,s69,s26,s230,s18,s97,s250])).
% 0.77/0.37 cnf(s265, plain, ~spl15_47 | ~spl15_33, inference(rat,[],[s208,s104,s24,s32,s126,s124,s205,s236,s259,s250])).
% 0.77/0.37 cnf(s266, plain, ~spl15_15, inference(rat,[],[s6,s54,s183,s214,s48,s108,s19,s142,s177,s25,s265,s17,s103,s264,s10,s220])).
% 0.77/0.37 cnf(s267, plain, spl15_16, inference(rat,[],[s9,s266])).
% 0.77/0.37 cnf(s270, plain, spl15_31, inference(rat,[],[s26,s69,s60,s263,s238,s17,s250,s267,s266])).
% 0.77/0.37 cnf(s271, plain, ~spl15_34, inference(rat,[],[s64,s270])).
% 0.77/0.37 cnf(s272, plain, spl15_33, inference(rat,[],[s18,s271])).
% 0.77/0.37 cnf(s275, plain, ~spl15_47, inference(rat,[],[s265,s272])).
% 0.77/0.37 cnf(s277, plain, spl15_48, inference(rat,[],[s25,s275])).
% 0.77/0.37 cnf(s279, plain, ~spl15_10, inference(rat,[],[s161,s267,s270,s277])).
% 0.77/0.37 cnf(s281, plain, spl15_12, inference(rat,[],[s102,s279])).
% 0.77/0.37 cnf(s282, plain, spl15_9, inference(rat,[],[s5,s279])).
% 0.77/0.37 cnf(s285, plain, ~spl15_36, inference(rat,[],[s181,s270,s266,s281])).
% 0.77/0.37 cnf(s287, plain, spl15_30, inference(rat,[],[s222,s282])).
% 0.77/0.37 cnf(s292, plain, spl15_35, inference(rat,[],[s19,s285])).
% 0.77/0.37 cnf(s294, plain, $false, inference(rat,[],[s183,s270,s281,s292,s287])).
% 0.77/0.37 thf(f1470,plain,(
% 0.77/0.37 $false),
% 0.77/0.37 inference(avatar_sat_refutation,[],[s294])).
% 0.77/0.37 % SZS output end Proof for theBenchmark
% 0.77/0.37 % (1947185)------------------------------
% 0.77/0.37 % (1947185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (1947185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (1947185)CaDiCaL version: 2.1.3
% 0.77/0.37 % (1947185)Termination reason: Refutation
% 0.77/0.37 % (1947185)Time elapsed: 0.040 s
% 0.77/0.37 % (1947185)Peak memory usage: 13 MB
% 0.77/0.37 % (1947185)Instructions burned: 67 (million)
% 0.77/0.37 % (1947174)Success in time 0.12 s
% 0.77/0.37 % Vampire exiting
%------------------------------------------------------------------------------