%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500^1.006 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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.69s 0.36s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO500^1.006 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n003.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 17:12:44 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.35 % (2784547)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (2784556)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1669595305:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (2784556)Refutation not found, incomplete strategy
% 0.21/0.35 % (2784556)------------------------------
% 0.21/0.35 % (2784556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2784556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2784556)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2784556)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (2784556)Time elapsed: 0.001 s
% 0.21/0.35 % (2784556)Peak memory usage: 12 MB
% 0.21/0.35 % (2784556)Instructions burned: 3 (million)
% 0.21/0.35 % (2784556)------------------------------
% 0.21/0.35 % (2784556)------------------------------
% 0.21/0.35 % (2784558)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.35 % (2784558)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.35 % (2784553)lrs+10_16_si=on:nwc=1.5:random_seed=273441559:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (2784552)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1948571532:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (2784554)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1922738409:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (2784555)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=1145193046: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.35 % (2784557)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=375301580:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (2784558)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=2510035778:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (2784554)Refutation not found, incomplete strategy
% 0.21/0.35 % (2784554)------------------------------
% 0.21/0.35 % (2784554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2784554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2784554)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2784554)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (2784554)Time elapsed: 0.001 s
% 0.21/0.35 % (2784554)Peak memory usage: 12 MB
% 0.21/0.35 % (2784552)Refutation not found, incomplete strategy
% 0.21/0.35 % (2784552)------------------------------
% 0.21/0.35 % (2784552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2784552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2784552)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2784552)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (2784552)Time elapsed: 0.001 s
% 0.21/0.35 % (2784552)Peak memory usage: 12 MB
% 0.21/0.35 % (2784552)Instructions burned: 1 (million)
% 0.21/0.35 % (2784553)Refutation not found, incomplete strategy
% 0.21/0.35 % (2784553)------------------------------
% 0.21/0.35 % (2784553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2784553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2784553)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2784553)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (2784553)Time elapsed: 0.002 s
% 0.21/0.35 % (2784553)Peak memory usage: 12 MB
% 0.21/0.35 % (2784553)Instructions burned: 2 (million)
% 0.21/0.35 % (2784554)------------------------------
% 0.21/0.35 % (2784554)------------------------------
% 0.21/0.35 % (2784552)------------------------------
% 0.21/0.35 % (2784552)------------------------------
% 0.21/0.35 % (2784553)------------------------------
% 0.21/0.35 % (2784553)------------------------------
% 0.21/0.35 % (2784560)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1971782911:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.69/0.36 % (2784560)Instruction limit reached!
% 0.69/0.36 % (2784560)------------------------------
% 0.69/0.36 % (2784560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784560)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784560)Termination reason: Instruction limit
% 0.69/0.36 % (2784560)Termination phase: Saturation
% 0.69/0.36 % (2784560)Time elapsed: 0.001 s
% 0.69/0.36 % (2784560)Peak memory usage: 12 MB
% 0.69/0.36 % (2784560)Instructions burned: 2 (million)
% 0.69/0.36 % (2784571)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.69/0.36 % (2784571)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.69/0.36 % (2784568)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.69/0.36 % (2784571)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2129504932: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.69/0.36 % (2784568)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2951733922:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.69/0.36 % (2784567)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1118696996:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.69/0.36 % (2784569)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2632878546:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.69/0.36 % (2784567)Instruction limit reached!
% 0.69/0.36 % (2784567)------------------------------
% 0.69/0.36 % (2784567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784567)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784567)Termination reason: Instruction limit
% 0.69/0.36 % (2784567)Termination phase: Saturation
% 0.69/0.36 % (2784567)Time elapsed: 0.004 s
% 0.69/0.36 % (2784567)Peak memory usage: 11 MB
% 0.69/0.36 % (2784567)Instructions burned: 6 (million)
% 0.69/0.36 % (2784571)Instruction limit reached!
% 0.69/0.36 % (2784571)------------------------------
% 0.69/0.36 % (2784571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784571)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784571)Termination reason: Instruction limit
% 0.69/0.36 % (2784571)Termination phase: Saturation
% 0.69/0.36 % (2784571)Time elapsed: 0.008 s
% 0.69/0.36 % (2784571)Peak memory usage: 12 MB
% 0.69/0.36 % (2784571)Instructions burned: 29 (million)
% 0.69/0.36 % (2784568)Instruction limit reached!
% 0.69/0.36 % (2784568)------------------------------
% 0.69/0.36 % (2784568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784568)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784568)Termination reason: Instruction limit
% 0.69/0.36 % (2784568)Termination phase: Saturation
% 0.69/0.36 % (2784568)Time elapsed: 0.004 s
% 0.69/0.36 % (2784568)Peak memory usage: 12 MB
% 0.69/0.36 % (2784568)Instructions burned: 8 (million)
% 0.69/0.36 % (2784569)Instruction limit reached!
% 0.69/0.36 % (2784569)------------------------------
% 0.69/0.36 % (2784569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784569)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784569)Termination reason: Instruction limit
% 0.69/0.36 % (2784569)Termination phase: Saturation
% 0.69/0.36 % (2784569)Time elapsed: 0.006 s
% 0.69/0.36 % (2784569)Peak memory usage: 12 MB
% 0.69/0.36 % (2784569)Instructions burned: 12 (million)
% 0.69/0.36 % (2784577)lrs+10_1_si=on:cs=on:random_seed=1736633482:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.69/0.36 % (2784557)Instruction limit reached!
% 0.69/0.36 % (2784557)------------------------------
% 0.69/0.36 % (2784557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784557)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784557)Termination reason: Instruction limit
% 0.69/0.36 % (2784557)Termination phase: Saturation
% 0.69/0.36 % (2784557)Time elapsed: 0.038 s
% 0.69/0.36 % (2784557)Peak memory usage: 12 MB
% 0.69/0.36 % (2784557)Instructions burned: 76 (million)
% 0.69/0.36 % (2784577)Instruction limit reached!
% 0.69/0.36 % (2784577)------------------------------
% 0.69/0.36 % (2784577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784577)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784577)Termination reason: Instruction limit
% 0.69/0.36 % (2784577)Termination phase: Saturation
% 0.69/0.36 % (2784577)Time elapsed: 0.004 s
% 0.69/0.36 % (2784577)Peak memory usage: 11 MB
% 0.69/0.36 % (2784577)Instructions burned: 17 (million)
% 0.69/0.36 % (2784578)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.69/0.36 % (2784576)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=3951048345:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.69/0.36 % (2784578)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=200318973:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.69/0.36 % (2784579)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1964311325:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.69/0.36 % (2784576)Refutation not found, incomplete strategy
% 0.69/0.36 % (2784576)------------------------------
% 0.69/0.36 % (2784576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784576)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784576)Termination reason: Refutation not found, incomplete strategy
% 0.69/0.36 % (2784576)Time elapsed: 0.003 s
% 0.69/0.36 % (2784576)Peak memory usage: 12 MB
% 0.69/0.36 % (2784576)Instructions burned: 5 (million)
% 0.69/0.36 % (2784576)------------------------------
% 0.69/0.36 % (2784576)------------------------------
% 0.69/0.36 % (2784579)Refutation not found, incomplete strategy
% 0.69/0.36 % (2784579)------------------------------
% 0.69/0.36 % (2784579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784579)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784579)Termination reason: Refutation not found, incomplete strategy
% 0.69/0.36 % (2784579)Time elapsed: 0.002 s
% 0.69/0.36 % (2784579)Peak memory usage: 12 MB
% 0.69/0.36 % (2784579)Instructions burned: 2 (million)
% 0.69/0.36 % (2784578)Instruction limit reached!
% 0.69/0.36 % (2784578)------------------------------
% 0.69/0.36 % (2784578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784578)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784578)Termination reason: Instruction limit
% 0.69/0.36 % (2784578)Termination phase: Saturation
% 0.69/0.36 % (2784578)Time elapsed: 0.002 s
% 0.69/0.36 % (2784578)Peak memory usage: 12 MB
% 0.69/0.36 % (2784578)Instructions burned: 2 (million)
% 0.69/0.36 % (2784579)------------------------------
% 0.69/0.36 % (2784579)------------------------------
% 0.69/0.36 % (2784582)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2064202584:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.69/0.36 % (2784582)Refutation not found, incomplete strategy
% 0.69/0.36 % (2784582)------------------------------
% 0.69/0.36 % (2784582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784582)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784582)Termination reason: Refutation not found, incomplete strategy
% 0.69/0.36 % (2784582)Time elapsed: 0.0000 s
% 0.69/0.36 % (2784582)Peak memory usage: 12 MB
% 0.69/0.36 % (2784582)Instructions burned: 1 (million)
% 0.69/0.36 % (2784582)------------------------------
% 0.69/0.36 % (2784582)------------------------------
% 0.69/0.36 % (2784558) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2784547-2784558"...
% 0.69/0.36 % (2784581)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3311171414:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.69/0.36 % (2784590)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3341088668:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.69/0.36 % (2784558)...printing done.
% 0.69/0.36 % (2784590)Instruction limit reached!
% 0.69/0.36 % (2784590)------------------------------
% 0.69/0.36 % (2784590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.36 % (2784590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.36 % (2784590)CaDiCaL version: 2.1.3
% 0.69/0.36 % (2784590)Termination reason: Instruction limit
% 0.69/0.36 % (2784590)Termination phase: Saturation
% 0.69/0.36 % (2784590)Time elapsed: 0.001 s
% 0.69/0.36 % (2784590)Peak memory usage: 12 MB
% 0.69/0.36 % (2784590)Instructions burned: 3 (million)
% 0.69/0.36 % (2784558)Refutation found. Thanks to Tanya!
% 0.69/0.36 % SZS status Theorem for theBenchmark
% 0.69/0.36 % SZS output start Proof for theBenchmark
% 0.69/0.36 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.69/0.36 thf(func_def_0, type, x: $o).
% 0.69/0.36 thf(func_def_1, type, f0: ($o > $o)).
% 0.69/0.36 thf(func_def_2, type, f1: ($o > $o)).
% 0.69/0.36 thf(func_def_3, type, f2: ($o > $o)).
% 0.69/0.36 thf(func_def_4, type, f3: ($o > $o)).
% 0.69/0.36 thf(func_def_5, type, f4: ($o > $o)).
% 0.69/0.36 thf(func_def_6, type, f5: ($o > $o)).
% 0.69/0.36 thf(func_def_10, type, sF0: $o).
% 0.69/0.36 thf(func_def_11, type, sF1: $o).
% 0.69/0.36 thf(func_def_12, type, sF2: $o).
% 0.69/0.36 thf(func_def_13, type, sF3: $o).
% 0.69/0.36 thf(func_def_14, type, sF4: $o).
% 0.69/0.36 thf(func_def_15, type, sF5: $o).
% 0.69/0.36 thf(func_def_16, type, sF6: $o).
% 0.69/0.36 thf(func_def_17, type, sF7: $o).
% 0.69/0.36 thf(func_def_18, type, sF8: $o).
% 0.69/0.36 thf(func_def_19, type, sF9: $o).
% 0.69/0.36 thf(func_def_20, type, sF10: $o).
% 0.69/0.36 thf(func_def_21, type, sF11: $o).
% 0.69/0.36 thf(func_def_22, type, sF12: $o).
% 0.69/0.36 thf(func_def_23, type, sF13: $o).
% 0.69/0.36 thf(func_def_24, type, sF14: $o).
% 0.69/0.36 thf(func_def_25, type, sF15: $o).
% 0.69/0.36 thf(func_def_26, type, sF16: $o).
% 0.69/0.36 thf(func_def_27, type, sF17: $o).
% 0.69/0.36 thf(func_def_28, type, sF18: $o).
% 0.69/0.36 thf(func_def_29, type, sF19: $o).
% 0.69/0.36 thf(func_def_30, type, sF20: $o).
% 0.69/0.36 thf(func_def_31, type, sF21: $o).
% 0.69/0.36 thf(func_def_32, type, sF22: $o).
% 0.69/0.36 thf(f1,conjecture,(
% 0.69/0.36 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 0.69/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski6)).
% 0.69/0.36 thf(f2,negated_conjecture,(
% 0.69/0.36 ~ (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) = ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 0.69/0.36 inference(negated_conjecture,[status(cth)],[f1])).
% 0.69/0.36 thf(f3,plain,(
% 0.69/0.36 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 0.69/0.36 inference(flattening,[],[f2])).
% 0.69/0.36 thf(f4,plain,(
% 0.69/0.36 (((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ x))))))))))))) != ((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ x))))))))))))))),
% 0.69/0.36 inference(cnf_transformation,[],[f3])).
% 0.69/0.36 thf(f6,definition,(
% 0.69/0.36 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.69/0.36 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.69/0.36 thf(f7,definition,(
% 0.69/0.36 (sF0 = ((f5 @ x)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.69/0.36 thf(f8,plain,(
% 0.69/0.36 (((f5 @ x)) = sF0)),
% 0.69/0.36 inference(reorient_equations,[],[f7])).
% 0.69/0.36 thf(f9,definition,(
% 0.69/0.36 (sF1 = ((f4 @ sF0)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.69/0.36 thf(f10,definition,(
% 0.69/0.36 (sF2 = ((f4 @ sF1)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.69/0.36 thf(f11,definition,(
% 0.69/0.36 (sF3 = ((f4 @ sF2)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.69/0.36 thf(f12,definition,(
% 0.69/0.36 (sF4 = ((f3 @ sF3)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.69/0.36 thf(f13,plain,(
% 0.69/0.36 (((f3 @ sF3)) = sF4)),
% 0.69/0.36 inference(reorient_equations,[],[f12])).
% 0.69/0.36 thf(f14,definition,(
% 0.69/0.36 (sF5 = ((f2 @ sF4)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 0.69/0.36 thf(f15,plain,(
% 0.69/0.36 (((f2 @ sF4)) = sF5)),
% 0.69/0.36 inference(reorient_equations,[],[f14])).
% 0.69/0.36 thf(f16,definition,(
% 0.69/0.36 (sF6 = ((f2 @ sF5)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.69/0.36 thf(f17,definition,(
% 0.69/0.36 (sF7 = ((f2 @ sF6)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 0.69/0.36 thf(f18,definition,(
% 0.69/0.36 (sF8 = ((f1 @ sF7)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 0.69/0.36 thf(f19,plain,(
% 0.69/0.36 (((f1 @ sF7)) = sF8)),
% 0.69/0.36 inference(reorient_equations,[],[f18])).
% 0.69/0.36 thf(f20,definition,(
% 0.69/0.36 (sF9 = ((f0 @ sF8)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.69/0.36 thf(f21,definition,(
% 0.69/0.36 (sF10 = ((f0 @ sF9)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.69/0.36 thf(f22,plain,(
% 0.69/0.36 (((f0 @ sF9)) = sF10)),
% 0.69/0.36 inference(reorient_equations,[],[f21])).
% 0.69/0.36 thf(f23,definition,(
% 0.69/0.36 (sF11 = ((f0 @ sF10)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 0.69/0.36 thf(f24,plain,(
% 0.69/0.36 (((f0 @ sF10)) = sF11)),
% 0.69/0.36 inference(reorient_equations,[],[f23])).
% 0.69/0.36 thf(f25,definition,(
% 0.69/0.36 (sF12 = ((f5 @ sF0)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.69/0.36 thf(f26,plain,(
% 0.69/0.36 (((f5 @ sF0)) = sF12)),
% 0.69/0.36 inference(reorient_equations,[],[f25])).
% 0.69/0.36 thf(f27,definition,(
% 0.69/0.36 (sF13 = ((f5 @ sF12)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.69/0.36 thf(f28,plain,(
% 0.69/0.36 (((f5 @ sF12)) = sF13)),
% 0.69/0.36 inference(reorient_equations,[],[f27])).
% 0.69/0.36 thf(f29,definition,(
% 0.69/0.36 (sF14 = ((f4 @ sF13)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.69/0.36 thf(f30,definition,(
% 0.69/0.36 (sF15 = ((f3 @ sF14)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 0.69/0.36 thf(f31,plain,(
% 0.69/0.36 (((f3 @ sF14)) = sF15)),
% 0.69/0.36 inference(reorient_equations,[],[f30])).
% 0.69/0.36 thf(f32,definition,(
% 0.69/0.36 (sF16 = ((f3 @ sF15)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 0.69/0.36 thf(f33,definition,(
% 0.69/0.36 (sF17 = ((f3 @ sF16)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 0.69/0.36 thf(f34,definition,(
% 0.69/0.36 (sF18 = ((f2 @ sF17)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 0.69/0.36 thf(f35,plain,(
% 0.69/0.36 (((f2 @ sF17)) = sF18)),
% 0.69/0.36 inference(reorient_equations,[],[f34])).
% 0.69/0.36 thf(f36,definition,(
% 0.69/0.36 (sF19 = ((f1 @ sF18)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 0.69/0.36 thf(f37,definition,(
% 0.69/0.36 (sF20 = ((f1 @ sF19)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 0.69/0.36 thf(f38,plain,(
% 0.69/0.36 (((f1 @ sF19)) = sF20)),
% 0.69/0.36 inference(reorient_equations,[],[f37])).
% 0.69/0.36 thf(f39,definition,(
% 0.69/0.36 (sF21 = ((f1 @ sF20)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 0.69/0.36 thf(f40,definition,(
% 0.69/0.36 (sF22 = ((f0 @ sF21)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 0.69/0.36 thf(f41,plain,(
% 0.69/0.36 (((f0 @ sF21)) = sF22)),
% 0.69/0.36 inference(reorient_equations,[],[f40])).
% 0.69/0.36 thf(f42,plain,(
% 0.69/0.36 (sF22 != sF11)),
% 0.69/0.36 inference(definition_folding,[],[f4,f41,f39,f38,f36,f35,f33,f32,f31,f29,f28,f26,f8,f24,f22,f20,f19,f17,f16,f15,f13,f11,f10,f9,f8])).
% 0.69/0.36 thf(f43,plain,(
% 0.69/0.36 ($false = ((f3 @ sF15))) | (sF16 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f32])).
% 0.69/0.36 thf(f44,plain,(
% 0.69/0.36 (((f3 @ sF15)) = $true) | ($false = sF16)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f32])).
% 0.69/0.36 thf(f45,plain,(
% 0.69/0.36 ($false = sF11) | (((f0 @ sF10)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f24])).
% 0.69/0.36 thf(f46,plain,(
% 0.69/0.36 ($true = sF11) | ($false = ((f0 @ sF10)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f24])).
% 0.69/0.36 thf(f47,plain,(
% 0.69/0.36 (((f1 @ sF7)) = $true) | ($false = sF8)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f19])).
% 0.69/0.36 thf(f48,plain,(
% 0.69/0.36 (((f1 @ sF7)) = $false) | ($true = sF8)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f19])).
% 0.69/0.36 thf(f49,plain,(
% 0.69/0.36 ($true = sF11) | (sF22 = $true)),
% 0.69/0.36 inference(xor_proxy_clausification,[],[f42])).
% 0.69/0.36 thf(f50,plain,(
% 0.69/0.36 ($false = sF11) | ($false = sF22)),
% 0.69/0.36 inference(xor_proxy_clausification,[],[f42])).
% 0.69/0.36 thf(f51,plain,(
% 0.69/0.36 ($false = sF4) | (((f3 @ sF3)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f13])).
% 0.69/0.36 thf(f52,plain,(
% 0.69/0.36 ($false = ((f3 @ sF3))) | ($true = sF4)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f13])).
% 0.69/0.36 thf(f53,plain,(
% 0.69/0.36 ($false = sF20) | (((f1 @ sF19)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f38])).
% 0.69/0.36 thf(f54,plain,(
% 0.69/0.36 ($false = ((f1 @ sF19))) | (sF20 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f38])).
% 0.69/0.36 thf(f55,plain,(
% 0.69/0.36 ($false = sF22) | (((f0 @ sF21)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f41])).
% 0.69/0.36 thf(f56,plain,(
% 0.69/0.36 (sF22 = $true) | (((f0 @ sF21)) = $false)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f41])).
% 0.69/0.36 thf(f57,plain,(
% 0.69/0.36 (sF9 = $true) | ($false = ((f0 @ sF8)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f20])).
% 0.69/0.36 thf(f58,plain,(
% 0.69/0.36 (((f0 @ sF8)) = $true) | ($false = sF9)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f20])).
% 0.69/0.36 thf(f59,plain,(
% 0.69/0.36 ($false = sF10) | (((f0 @ sF9)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f22])).
% 0.69/0.36 thf(f60,plain,(
% 0.69/0.36 (((f0 @ sF9)) = $false) | ($true = sF10)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f22])).
% 0.69/0.36 thf(f61,plain,(
% 0.69/0.36 ($false = sF13) | (((f5 @ sF12)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f28])).
% 0.69/0.36 thf(f62,plain,(
% 0.69/0.36 (((f5 @ sF12)) = $false) | (sF13 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f28])).
% 0.69/0.36 thf(f63,plain,(
% 0.69/0.36 ($false = ((f2 @ sF5))) | (sF6 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f16])).
% 0.69/0.36 thf(f64,plain,(
% 0.69/0.36 ($false = sF6) | (((f2 @ sF5)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f16])).
% 0.69/0.36 thf(f65,plain,(
% 0.69/0.36 ($false = ((f2 @ sF6))) | (sF7 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f17])).
% 0.69/0.36 thf(f66,plain,(
% 0.69/0.36 ($true = ((f2 @ sF6))) | ($false = sF7)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f17])).
% 0.69/0.36 thf(f67,plain,(
% 0.69/0.36 ($false = ((f3 @ sF16))) | ($true = sF17)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f33])).
% 0.69/0.36 thf(f68,plain,(
% 0.69/0.36 ($false = sF17) | ($true = ((f3 @ sF16)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f33])).
% 0.69/0.36 thf(f69,plain,(
% 0.69/0.36 (sF1 = $true) | ($false = ((f4 @ sF0)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f9])).
% 0.69/0.36 thf(f70,plain,(
% 0.69/0.36 ($false = sF1) | ($true = ((f4 @ sF0)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f9])).
% 0.69/0.36 thf(f71,plain,(
% 0.69/0.36 (((f2 @ sF4)) = $true) | ($false = sF5)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f15])).
% 0.69/0.36 thf(f72,plain,(
% 0.69/0.36 (((f2 @ sF4)) = $false) | (sF5 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f15])).
% 0.69/0.36 thf(f73,plain,(
% 0.69/0.36 (sF14 = $true) | ($false = ((f4 @ sF13)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f29])).
% 0.69/0.36 thf(f74,plain,(
% 0.69/0.36 ($true = ((f4 @ sF13))) | ($false = sF14)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f29])).
% 0.69/0.36 thf(f75,plain,(
% 0.69/0.36 ($false = sF18) | (((f2 @ sF17)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f35])).
% 0.69/0.36 thf(f76,plain,(
% 0.69/0.36 (sF18 = $true) | ($false = ((f2 @ sF17)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f35])).
% 0.69/0.36 thf(f77,plain,(
% 0.69/0.36 (sF19 = $true) | ($false = ((f1 @ sF18)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f36])).
% 0.69/0.36 thf(f78,plain,(
% 0.69/0.36 (sF19 = $false) | (((f1 @ sF18)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f36])).
% 0.69/0.36 thf(f79,plain,(
% 0.69/0.36 (((f3 @ sF14)) = $true) | ($false = sF15)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f31])).
% 0.69/0.36 thf(f80,plain,(
% 0.69/0.36 ($true = sF15) | (((f3 @ sF14)) = $false)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f31])).
% 0.69/0.36 thf(f81,plain,(
% 0.69/0.36 (((f5 @ sF0)) = $true) | ($false = sF12)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f26])).
% 0.69/0.36 thf(f82,plain,(
% 0.69/0.36 (sF12 = $true) | (((f5 @ sF0)) = $false)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f26])).
% 0.69/0.36 thf(f83,plain,(
% 0.69/0.36 (((f5 @ x)) = $true) | ($false = sF0)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f8])).
% 0.69/0.36 thf(f84,plain,(
% 0.69/0.36 (((f5 @ x)) = $false) | (sF0 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f8])).
% 0.69/0.36 thf(f85,plain,(
% 0.69/0.36 (sF2 = $true) | (((f4 @ sF1)) = $false)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f10])).
% 0.69/0.36 thf(f86,plain,(
% 0.69/0.36 (sF2 = $false) | (((f4 @ sF1)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f10])).
% 0.69/0.36 thf(f87,plain,(
% 0.69/0.36 (((f4 @ sF2)) = $false) | (sF3 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f11])).
% 0.69/0.36 thf(f88,plain,(
% 0.69/0.36 (sF3 = $false) | (((f4 @ sF2)) = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f11])).
% 0.69/0.36 thf(f89,plain,(
% 0.69/0.36 ($false = ((f1 @ sF20))) | (sF21 = $true)),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f39])).
% 0.69/0.36 thf(f90,plain,(
% 0.69/0.36 ($false = sF21) | ($true = ((f1 @ sF20)))),
% 0.69/0.36 inference(iff_proxy_clausification,[],[f39])).
% 0.69/0.36 thf(f92,definition,(
% 0.69/0.36 spl23_1 <=> ($false = sF16)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition])).
% 0.69/0.36 thf(f93,plain,(
% 0.69/0.36 ($false != sF16) | spl23_1),
% 0.69/0.36 inference(avatar_component_clause,[],[f92])).
% 0.69/0.36 thf(f94,plain,(
% 0.69/0.36 ($false = sF16) | ~spl23_1),
% 0.69/0.36 inference(avatar_component_clause,[],[f92])).
% 0.69/0.36 thf(f96,definition,(
% 0.69/0.36 spl23_2 <=> (((f3 @ sF15)) = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition])).
% 0.69/0.36 thf(f97,plain,(
% 0.69/0.36 (((f3 @ sF15)) != $true) | spl23_2),
% 0.69/0.36 inference(avatar_component_clause,[],[f96])).
% 0.69/0.36 thf(f98,plain,(
% 0.69/0.36 (((f3 @ sF15)) = $true) | ~spl23_2),
% 0.69/0.36 inference(avatar_component_clause,[],[f96])).
% 0.69/0.36 thf(f99,plain,(
% 0.69/0.36 spl23_1 | spl23_2),
% 0.69/0.36 inference(avatar_split_clause,[],[f44,f96,f92])).
% 0.69/0.36 thf(f101,definition,(
% 0.69/0.36 spl23_3 <=> ($false = ((f3 @ sF15)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition])).
% 0.69/0.36 thf(f102,plain,(
% 0.69/0.36 ($false != ((f3 @ sF15))) | spl23_3),
% 0.69/0.36 inference(avatar_component_clause,[],[f101])).
% 0.69/0.36 thf(f103,plain,(
% 0.69/0.36 ($false = ((f3 @ sF15))) | ~spl23_3),
% 0.69/0.36 inference(avatar_component_clause,[],[f101])).
% 0.69/0.36 thf(f105,definition,(
% 0.69/0.36 spl23_4 <=> (sF16 = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_4])],[avatar_definition])).
% 0.69/0.36 thf(f106,plain,(
% 0.69/0.36 (sF16 != $true) | spl23_4),
% 0.69/0.36 inference(avatar_component_clause,[],[f105])).
% 0.69/0.36 thf(f107,plain,(
% 0.69/0.36 (sF16 = $true) | ~spl23_4),
% 0.69/0.36 inference(avatar_component_clause,[],[f105])).
% 0.69/0.36 thf(f108,plain,(
% 0.69/0.36 spl23_3 | spl23_4),
% 0.69/0.36 inference(avatar_split_clause,[],[f43,f105,f101])).
% 0.69/0.36 thf(f110,definition,(
% 0.69/0.36 spl23_5 <=> ($false = ((f0 @ sF10)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition])).
% 0.69/0.36 thf(f111,plain,(
% 0.69/0.36 ($false != ((f0 @ sF10))) | spl23_5),
% 0.69/0.36 inference(avatar_component_clause,[],[f110])).
% 0.69/0.36 thf(f112,plain,(
% 0.69/0.36 ($false = ((f0 @ sF10))) | ~spl23_5),
% 0.69/0.36 inference(avatar_component_clause,[],[f110])).
% 0.69/0.36 thf(f114,definition,(
% 0.69/0.36 spl23_6 <=> ($true = sF11)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition])).
% 0.69/0.36 thf(f116,plain,(
% 0.69/0.36 ($true = sF11) | ~spl23_6),
% 0.69/0.36 inference(avatar_component_clause,[],[f114])).
% 0.69/0.36 thf(f117,plain,(
% 0.69/0.36 spl23_5 | spl23_6),
% 0.69/0.36 inference(avatar_split_clause,[],[f46,f114,f110])).
% 0.69/0.36 thf(f119,definition,(
% 0.69/0.36 spl23_7 <=> (((f0 @ sF10)) = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition])).
% 0.69/0.36 thf(f121,plain,(
% 0.69/0.36 (((f0 @ sF10)) = $true) | ~spl23_7),
% 0.69/0.36 inference(avatar_component_clause,[],[f119])).
% 0.69/0.36 thf(f123,definition,(
% 0.69/0.36 spl23_8 <=> ($false = sF11)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition])).
% 0.69/0.36 thf(f125,plain,(
% 0.69/0.36 ($false = sF11) | ~spl23_8),
% 0.69/0.36 inference(avatar_component_clause,[],[f123])).
% 0.69/0.36 thf(f126,plain,(
% 0.69/0.36 spl23_7 | spl23_8),
% 0.69/0.36 inference(avatar_split_clause,[],[f45,f123,f119])).
% 0.69/0.36 thf(f128,definition,(
% 0.69/0.36 spl23_9 <=> (((f1 @ sF7)) = $false)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition])).
% 0.69/0.36 thf(f129,plain,(
% 0.69/0.36 (((f1 @ sF7)) != $false) | spl23_9),
% 0.69/0.36 inference(avatar_component_clause,[],[f128])).
% 0.69/0.36 thf(f130,plain,(
% 0.69/0.36 (((f1 @ sF7)) = $false) | ~spl23_9),
% 0.69/0.36 inference(avatar_component_clause,[],[f128])).
% 0.69/0.36 thf(f132,definition,(
% 0.69/0.36 spl23_10 <=> ($true = sF8)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition])).
% 0.69/0.36 thf(f134,plain,(
% 0.69/0.36 ($true = sF8) | ~spl23_10),
% 0.69/0.36 inference(avatar_component_clause,[],[f132])).
% 0.69/0.36 thf(f135,plain,(
% 0.69/0.36 spl23_9 | spl23_10),
% 0.69/0.36 inference(avatar_split_clause,[],[f48,f132,f128])).
% 0.69/0.36 thf(f137,definition,(
% 0.69/0.36 spl23_11 <=> ($false = sF8)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition])).
% 0.69/0.36 thf(f139,plain,(
% 0.69/0.36 ($false = sF8) | ~spl23_11),
% 0.69/0.36 inference(avatar_component_clause,[],[f137])).
% 0.69/0.36 thf(f141,definition,(
% 0.69/0.36 spl23_12 <=> (((f1 @ sF7)) = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition])).
% 0.69/0.36 thf(f142,plain,(
% 0.69/0.36 (((f1 @ sF7)) != $true) | spl23_12),
% 0.69/0.36 inference(avatar_component_clause,[],[f141])).
% 0.69/0.36 thf(f143,plain,(
% 0.69/0.36 (((f1 @ sF7)) = $true) | ~spl23_12),
% 0.69/0.36 inference(avatar_component_clause,[],[f141])).
% 0.69/0.36 thf(f144,plain,(
% 0.69/0.36 spl23_11 | spl23_12),
% 0.69/0.36 inference(avatar_split_clause,[],[f47,f141,f137])).
% 0.69/0.36 thf(f146,definition,(
% 0.69/0.36 spl23_13 <=> ($false = sF22)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition])).
% 0.69/0.36 thf(f148,plain,(
% 0.69/0.36 ($false = sF22) | ~spl23_13),
% 0.69/0.36 inference(avatar_component_clause,[],[f146])).
% 0.69/0.36 thf(f149,plain,(
% 0.69/0.36 spl23_13 | spl23_8),
% 0.69/0.36 inference(avatar_split_clause,[],[f50,f123,f146])).
% 0.69/0.36 thf(f151,definition,(
% 0.69/0.36 spl23_14 <=> (sF22 = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition])).
% 0.69/0.36 thf(f153,plain,(
% 0.69/0.36 (sF22 = $true) | ~spl23_14),
% 0.69/0.36 inference(avatar_component_clause,[],[f151])).
% 0.69/0.36 thf(f154,plain,(
% 0.69/0.36 spl23_6 | spl23_14),
% 0.69/0.36 inference(avatar_split_clause,[],[f49,f151,f114])).
% 0.69/0.36 thf(f156,definition,(
% 0.69/0.36 spl23_15 <=> ($false = ((f3 @ sF3)))),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition])).
% 0.69/0.36 thf(f157,plain,(
% 0.69/0.36 ($false != ((f3 @ sF3))) | spl23_15),
% 0.69/0.36 inference(avatar_component_clause,[],[f156])).
% 0.69/0.36 thf(f158,plain,(
% 0.69/0.36 ($false = ((f3 @ sF3))) | ~spl23_15),
% 0.69/0.36 inference(avatar_component_clause,[],[f156])).
% 0.69/0.36 thf(f160,definition,(
% 0.69/0.36 spl23_16 <=> ($true = sF4)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition])).
% 0.69/0.36 thf(f162,plain,(
% 0.69/0.36 ($true = sF4) | ~spl23_16),
% 0.69/0.36 inference(avatar_component_clause,[],[f160])).
% 0.69/0.36 thf(f163,plain,(
% 0.69/0.36 spl23_15 | spl23_16),
% 0.69/0.36 inference(avatar_split_clause,[],[f52,f160,f156])).
% 0.69/0.36 thf(f165,definition,(
% 0.69/0.36 spl23_17 <=> ($false = sF4)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition])).
% 0.69/0.36 thf(f167,plain,(
% 0.69/0.36 ($false = sF4) | ~spl23_17),
% 0.69/0.36 inference(avatar_component_clause,[],[f165])).
% 0.69/0.36 thf(f169,definition,(
% 0.69/0.36 spl23_18 <=> (((f3 @ sF3)) = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition])).
% 0.69/0.36 thf(f170,plain,(
% 0.69/0.36 (((f3 @ sF3)) != $true) | spl23_18),
% 0.69/0.36 inference(avatar_component_clause,[],[f169])).
% 0.69/0.36 thf(f171,plain,(
% 0.69/0.36 (((f3 @ sF3)) = $true) | ~spl23_18),
% 0.69/0.36 inference(avatar_component_clause,[],[f169])).
% 0.69/0.36 thf(f172,plain,(
% 0.69/0.36 spl23_17 | spl23_18),
% 0.69/0.36 inference(avatar_split_clause,[],[f51,f169,f165])).
% 0.69/0.36 thf(f174,definition,(
% 0.69/0.36 spl23_19 <=> (sF20 = $true)),
% 0.69/0.36 introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition])).
% 0.69/0.36 thf(f175,plain,(
% 0.69/0.36 (sF20 != $true) | spl23_19),
% 0.69/0.36 inference(avatar_component_clause,[],[f174])).
% 0.69/0.37 thf(f176,plain,(
% 0.69/0.37 (sF20 = $true) | ~spl23_19),
% 0.69/0.37 inference(avatar_component_clause,[],[f174])).
% 0.69/0.37 thf(f178,definition,(
% 0.69/0.37 spl23_20 <=> ($false = ((f1 @ sF19)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition])).
% 0.69/0.37 thf(f180,plain,(
% 0.69/0.37 ($false = ((f1 @ sF19))) | ~spl23_20),
% 0.69/0.37 inference(avatar_component_clause,[],[f178])).
% 0.69/0.37 thf(f181,plain,(
% 0.69/0.37 spl23_19 | spl23_20),
% 0.69/0.37 inference(avatar_split_clause,[],[f54,f178,f174])).
% 0.69/0.37 thf(f183,definition,(
% 0.69/0.37 spl23_21 <=> (((f1 @ sF19)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition])).
% 0.69/0.37 thf(f184,plain,(
% 0.69/0.37 (((f1 @ sF19)) != $true) | spl23_21),
% 0.69/0.37 inference(avatar_component_clause,[],[f183])).
% 0.69/0.37 thf(f185,plain,(
% 0.69/0.37 (((f1 @ sF19)) = $true) | ~spl23_21),
% 0.69/0.37 inference(avatar_component_clause,[],[f183])).
% 0.69/0.37 thf(f187,definition,(
% 0.69/0.37 spl23_22 <=> ($false = sF20)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition])).
% 0.69/0.37 thf(f189,plain,(
% 0.69/0.37 ($false = sF20) | ~spl23_22),
% 0.69/0.37 inference(avatar_component_clause,[],[f187])).
% 0.69/0.37 thf(f190,plain,(
% 0.69/0.37 spl23_21 | spl23_22),
% 0.69/0.37 inference(avatar_split_clause,[],[f53,f187,f183])).
% 0.69/0.37 thf(f192,definition,(
% 0.69/0.37 spl23_23 <=> (((f0 @ sF21)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_23])],[avatar_definition])).
% 0.69/0.37 thf(f194,plain,(
% 0.69/0.37 (((f0 @ sF21)) = $false) | ~spl23_23),
% 0.69/0.37 inference(avatar_component_clause,[],[f192])).
% 0.69/0.37 thf(f195,plain,(
% 0.69/0.37 spl23_14 | spl23_23),
% 0.69/0.37 inference(avatar_split_clause,[],[f56,f192,f151])).
% 0.69/0.37 thf(f197,definition,(
% 0.69/0.37 spl23_24 <=> (((f0 @ sF21)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_24])],[avatar_definition])).
% 0.69/0.37 thf(f199,plain,(
% 0.69/0.37 (((f0 @ sF21)) = $true) | ~spl23_24),
% 0.69/0.37 inference(avatar_component_clause,[],[f197])).
% 0.69/0.37 thf(f200,plain,(
% 0.69/0.37 spl23_24 | spl23_13),
% 0.69/0.37 inference(avatar_split_clause,[],[f55,f146,f197])).
% 0.69/0.37 thf(f202,definition,(
% 0.69/0.37 spl23_25 <=> (((f0 @ sF8)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition])).
% 0.69/0.37 thf(f203,plain,(
% 0.69/0.37 (((f0 @ sF8)) != $true) | spl23_25),
% 0.69/0.37 inference(avatar_component_clause,[],[f202])).
% 0.69/0.37 thf(f204,plain,(
% 0.69/0.37 (((f0 @ sF8)) = $true) | ~spl23_25),
% 0.69/0.37 inference(avatar_component_clause,[],[f202])).
% 0.69/0.37 thf(f206,definition,(
% 0.69/0.37 spl23_26 <=> ($false = sF9)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition])).
% 0.69/0.37 thf(f208,plain,(
% 0.69/0.37 ($false = sF9) | ~spl23_26),
% 0.69/0.37 inference(avatar_component_clause,[],[f206])).
% 0.69/0.37 thf(f209,plain,(
% 0.69/0.37 spl23_25 | spl23_26),
% 0.69/0.37 inference(avatar_split_clause,[],[f58,f206,f202])).
% 0.69/0.37 thf(f211,definition,(
% 0.69/0.37 spl23_27 <=> (sF9 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_27])],[avatar_definition])).
% 0.69/0.37 thf(f213,plain,(
% 0.69/0.37 (sF9 = $true) | ~spl23_27),
% 0.69/0.37 inference(avatar_component_clause,[],[f211])).
% 0.69/0.37 thf(f215,definition,(
% 0.69/0.37 spl23_28 <=> ($false = ((f0 @ sF8)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition])).
% 0.69/0.37 thf(f217,plain,(
% 0.69/0.37 ($false = ((f0 @ sF8))) | ~spl23_28),
% 0.69/0.37 inference(avatar_component_clause,[],[f215])).
% 0.69/0.37 thf(f218,plain,(
% 0.69/0.37 spl23_27 | spl23_28),
% 0.69/0.37 inference(avatar_split_clause,[],[f57,f215,f211])).
% 0.69/0.37 thf(f220,definition,(
% 0.69/0.37 spl23_29 <=> (((f0 @ sF9)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_29])],[avatar_definition])).
% 0.69/0.37 thf(f221,plain,(
% 0.69/0.37 (((f0 @ sF9)) != $false) | spl23_29),
% 0.69/0.37 inference(avatar_component_clause,[],[f220])).
% 0.69/0.37 thf(f222,plain,(
% 0.69/0.37 (((f0 @ sF9)) = $false) | ~spl23_29),
% 0.69/0.37 inference(avatar_component_clause,[],[f220])).
% 0.69/0.37 thf(f224,definition,(
% 0.69/0.37 spl23_30 <=> ($true = sF10)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_30])],[avatar_definition])).
% 0.69/0.37 thf(f226,plain,(
% 0.69/0.37 ($true = sF10) | ~spl23_30),
% 0.69/0.37 inference(avatar_component_clause,[],[f224])).
% 0.69/0.37 thf(f227,plain,(
% 0.69/0.37 spl23_29 | spl23_30),
% 0.69/0.37 inference(avatar_split_clause,[],[f60,f224,f220])).
% 0.69/0.37 thf(f229,definition,(
% 0.69/0.37 spl23_31 <=> ($false = sF10)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_31])],[avatar_definition])).
% 0.69/0.37 thf(f231,plain,(
% 0.69/0.37 ($false = sF10) | ~spl23_31),
% 0.69/0.37 inference(avatar_component_clause,[],[f229])).
% 0.69/0.37 thf(f233,definition,(
% 0.69/0.37 spl23_32 <=> (((f0 @ sF9)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition])).
% 0.69/0.37 thf(f235,plain,(
% 0.69/0.37 (((f0 @ sF9)) = $true) | ~spl23_32),
% 0.69/0.37 inference(avatar_component_clause,[],[f233])).
% 0.69/0.37 thf(f236,plain,(
% 0.69/0.37 spl23_31 | spl23_32),
% 0.69/0.37 inference(avatar_split_clause,[],[f59,f233,f229])).
% 0.69/0.37 thf(f238,definition,(
% 0.69/0.37 spl23_33 <=> (sF13 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition])).
% 0.69/0.37 thf(f239,plain,(
% 0.69/0.37 (sF13 != $true) | spl23_33),
% 0.69/0.37 inference(avatar_component_clause,[],[f238])).
% 0.69/0.37 thf(f240,plain,(
% 0.69/0.37 (sF13 = $true) | ~spl23_33),
% 0.69/0.37 inference(avatar_component_clause,[],[f238])).
% 0.69/0.37 thf(f242,definition,(
% 0.69/0.37 spl23_34 <=> (((f5 @ sF12)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_34])],[avatar_definition])).
% 0.69/0.37 thf(f243,plain,(
% 0.69/0.37 (((f5 @ sF12)) != $false) | spl23_34),
% 0.69/0.37 inference(avatar_component_clause,[],[f242])).
% 0.69/0.37 thf(f244,plain,(
% 0.69/0.37 (((f5 @ sF12)) = $false) | ~spl23_34),
% 0.69/0.37 inference(avatar_component_clause,[],[f242])).
% 0.69/0.37 thf(f245,plain,(
% 0.69/0.37 spl23_33 | spl23_34),
% 0.69/0.37 inference(avatar_split_clause,[],[f62,f242,f238])).
% 0.69/0.37 thf(f247,definition,(
% 0.69/0.37 spl23_35 <=> ($false = sF13)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_35])],[avatar_definition])).
% 0.69/0.37 thf(f249,plain,(
% 0.69/0.37 ($false = sF13) | ~spl23_35),
% 0.69/0.37 inference(avatar_component_clause,[],[f247])).
% 0.69/0.37 thf(f251,definition,(
% 0.69/0.37 spl23_36 <=> (((f5 @ sF12)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition])).
% 0.69/0.37 thf(f252,plain,(
% 0.69/0.37 (((f5 @ sF12)) != $true) | spl23_36),
% 0.69/0.37 inference(avatar_component_clause,[],[f251])).
% 0.69/0.37 thf(f253,plain,(
% 0.69/0.37 (((f5 @ sF12)) = $true) | ~spl23_36),
% 0.69/0.37 inference(avatar_component_clause,[],[f251])).
% 0.69/0.37 thf(f254,plain,(
% 0.69/0.37 spl23_35 | spl23_36),
% 0.69/0.37 inference(avatar_split_clause,[],[f61,f251,f247])).
% 0.69/0.37 thf(f256,definition,(
% 0.69/0.37 spl23_37 <=> (((f2 @ sF5)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_37])],[avatar_definition])).
% 0.69/0.37 thf(f257,plain,(
% 0.69/0.37 (((f2 @ sF5)) != $true) | spl23_37),
% 0.69/0.37 inference(avatar_component_clause,[],[f256])).
% 0.69/0.37 thf(f258,plain,(
% 0.69/0.37 (((f2 @ sF5)) = $true) | ~spl23_37),
% 0.69/0.37 inference(avatar_component_clause,[],[f256])).
% 0.69/0.37 thf(f260,definition,(
% 0.69/0.37 spl23_38 <=> ($false = sF6)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_38])],[avatar_definition])).
% 0.69/0.37 thf(f261,plain,(
% 0.69/0.37 ($false != sF6) | spl23_38),
% 0.69/0.37 inference(avatar_component_clause,[],[f260])).
% 0.69/0.37 thf(f262,plain,(
% 0.69/0.37 ($false = sF6) | ~spl23_38),
% 0.69/0.37 inference(avatar_component_clause,[],[f260])).
% 0.69/0.37 thf(f263,plain,(
% 0.69/0.37 spl23_37 | spl23_38),
% 0.69/0.37 inference(avatar_split_clause,[],[f64,f260,f256])).
% 0.69/0.37 thf(f265,definition,(
% 0.69/0.37 spl23_39 <=> (sF6 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition])).
% 0.69/0.37 thf(f266,plain,(
% 0.69/0.37 (sF6 != $true) | spl23_39),
% 0.69/0.37 inference(avatar_component_clause,[],[f265])).
% 0.69/0.37 thf(f267,plain,(
% 0.69/0.37 (sF6 = $true) | ~spl23_39),
% 0.69/0.37 inference(avatar_component_clause,[],[f265])).
% 0.69/0.37 thf(f269,definition,(
% 0.69/0.37 spl23_40 <=> ($false = ((f2 @ sF5)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition])).
% 0.69/0.37 thf(f271,plain,(
% 0.69/0.37 ($false = ((f2 @ sF5))) | ~spl23_40),
% 0.69/0.37 inference(avatar_component_clause,[],[f269])).
% 0.69/0.37 thf(f272,plain,(
% 0.69/0.37 spl23_39 | spl23_40),
% 0.69/0.37 inference(avatar_split_clause,[],[f63,f269,f265])).
% 0.69/0.37 thf(f274,definition,(
% 0.69/0.37 spl23_41 <=> ($true = ((f2 @ sF6)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_41])],[avatar_definition])).
% 0.69/0.37 thf(f275,plain,(
% 0.69/0.37 ($true != ((f2 @ sF6))) | spl23_41),
% 0.69/0.37 inference(avatar_component_clause,[],[f274])).
% 0.69/0.37 thf(f276,plain,(
% 0.69/0.37 ($true = ((f2 @ sF6))) | ~spl23_41),
% 0.69/0.37 inference(avatar_component_clause,[],[f274])).
% 0.69/0.37 thf(f278,definition,(
% 0.69/0.37 spl23_42 <=> ($false = sF7)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_42])],[avatar_definition])).
% 0.69/0.37 thf(f279,plain,(
% 0.69/0.37 ($false != sF7) | spl23_42),
% 0.69/0.37 inference(avatar_component_clause,[],[f278])).
% 0.69/0.37 thf(f280,plain,(
% 0.69/0.37 ($false = sF7) | ~spl23_42),
% 0.69/0.37 inference(avatar_component_clause,[],[f278])).
% 0.69/0.37 thf(f281,plain,(
% 0.69/0.37 spl23_41 | spl23_42),
% 0.69/0.37 inference(avatar_split_clause,[],[f66,f278,f274])).
% 0.69/0.37 thf(f283,definition,(
% 0.69/0.37 spl23_43 <=> ($false = ((f2 @ sF6)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_43])],[avatar_definition])).
% 0.69/0.37 thf(f285,plain,(
% 0.69/0.37 ($false = ((f2 @ sF6))) | ~spl23_43),
% 0.69/0.37 inference(avatar_component_clause,[],[f283])).
% 0.69/0.37 thf(f287,definition,(
% 0.69/0.37 spl23_44 <=> (sF7 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_44])],[avatar_definition])).
% 0.69/0.37 thf(f288,plain,(
% 0.69/0.37 (sF7 != $true) | spl23_44),
% 0.69/0.37 inference(avatar_component_clause,[],[f287])).
% 0.69/0.37 thf(f289,plain,(
% 0.69/0.37 (sF7 = $true) | ~spl23_44),
% 0.69/0.37 inference(avatar_component_clause,[],[f287])).
% 0.69/0.37 thf(f290,plain,(
% 0.69/0.37 spl23_43 | spl23_44),
% 0.69/0.37 inference(avatar_split_clause,[],[f65,f287,f283])).
% 0.69/0.37 thf(f292,definition,(
% 0.69/0.37 spl23_45 <=> ($false = sF17)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_45])],[avatar_definition])).
% 0.69/0.37 thf(f294,plain,(
% 0.69/0.37 ($false = sF17) | ~spl23_45),
% 0.69/0.37 inference(avatar_component_clause,[],[f292])).
% 0.69/0.37 thf(f296,definition,(
% 0.69/0.37 spl23_46 <=> ($true = ((f3 @ sF16)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition])).
% 0.69/0.37 thf(f298,plain,(
% 0.69/0.37 ($true = ((f3 @ sF16))) | ~spl23_46),
% 0.69/0.37 inference(avatar_component_clause,[],[f296])).
% 0.69/0.37 thf(f299,plain,(
% 0.69/0.37 spl23_45 | spl23_46),
% 0.69/0.37 inference(avatar_split_clause,[],[f68,f296,f292])).
% 0.69/0.37 thf(f301,definition,(
% 0.69/0.37 spl23_47 <=> ($true = sF17)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_47])],[avatar_definition])).
% 0.69/0.37 thf(f303,plain,(
% 0.69/0.37 ($true = sF17) | ~spl23_47),
% 0.69/0.37 inference(avatar_component_clause,[],[f301])).
% 0.69/0.37 thf(f305,definition,(
% 0.69/0.37 spl23_48 <=> ($false = ((f3 @ sF16)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_48])],[avatar_definition])).
% 0.69/0.37 thf(f306,plain,(
% 0.69/0.37 ($false != ((f3 @ sF16))) | spl23_48),
% 0.69/0.37 inference(avatar_component_clause,[],[f305])).
% 0.69/0.37 thf(f307,plain,(
% 0.69/0.37 ($false = ((f3 @ sF16))) | ~spl23_48),
% 0.69/0.37 inference(avatar_component_clause,[],[f305])).
% 0.69/0.37 thf(f308,plain,(
% 0.69/0.37 spl23_47 | spl23_48),
% 0.69/0.37 inference(avatar_split_clause,[],[f67,f305,f301])).
% 0.69/0.37 thf(f310,definition,(
% 0.69/0.37 spl23_49 <=> ($false = sF1)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_49])],[avatar_definition])).
% 0.69/0.37 thf(f312,plain,(
% 0.69/0.37 ($false = sF1) | ~spl23_49),
% 0.69/0.37 inference(avatar_component_clause,[],[f310])).
% 0.69/0.37 thf(f314,definition,(
% 0.69/0.37 spl23_50 <=> ($true = ((f4 @ sF0)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition])).
% 0.69/0.37 thf(f316,plain,(
% 0.69/0.37 ($true = ((f4 @ sF0))) | ~spl23_50),
% 0.69/0.37 inference(avatar_component_clause,[],[f314])).
% 0.69/0.37 thf(f317,plain,(
% 0.69/0.37 spl23_49 | spl23_50),
% 0.69/0.37 inference(avatar_split_clause,[],[f70,f314,f310])).
% 0.69/0.37 thf(f319,definition,(
% 0.69/0.37 spl23_51 <=> ($false = ((f4 @ sF0)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_51])],[avatar_definition])).
% 0.69/0.37 thf(f321,plain,(
% 0.69/0.37 ($false = ((f4 @ sF0))) | ~spl23_51),
% 0.69/0.37 inference(avatar_component_clause,[],[f319])).
% 0.69/0.37 thf(f323,definition,(
% 0.69/0.37 spl23_52 <=> (sF1 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_52])],[avatar_definition])).
% 0.69/0.37 thf(f325,plain,(
% 0.69/0.37 (sF1 = $true) | ~spl23_52),
% 0.69/0.37 inference(avatar_component_clause,[],[f323])).
% 0.69/0.37 thf(f326,plain,(
% 0.69/0.37 spl23_51 | spl23_52),
% 0.69/0.37 inference(avatar_split_clause,[],[f69,f323,f319])).
% 0.69/0.37 thf(f328,definition,(
% 0.69/0.37 spl23_53 <=> (sF5 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_53])],[avatar_definition])).
% 0.69/0.37 thf(f329,plain,(
% 0.69/0.37 (sF5 != $true) | spl23_53),
% 0.69/0.37 inference(avatar_component_clause,[],[f328])).
% 0.69/0.37 thf(f330,plain,(
% 0.69/0.37 (sF5 = $true) | ~spl23_53),
% 0.69/0.37 inference(avatar_component_clause,[],[f328])).
% 0.69/0.37 thf(f332,definition,(
% 0.69/0.37 spl23_54 <=> (((f2 @ sF4)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition])).
% 0.69/0.37 thf(f333,plain,(
% 0.69/0.37 (((f2 @ sF4)) != $false) | spl23_54),
% 0.69/0.37 inference(avatar_component_clause,[],[f332])).
% 0.69/0.37 thf(f334,plain,(
% 0.69/0.37 (((f2 @ sF4)) = $false) | ~spl23_54),
% 0.69/0.37 inference(avatar_component_clause,[],[f332])).
% 0.69/0.37 thf(f335,plain,(
% 0.69/0.37 spl23_53 | spl23_54),
% 0.69/0.37 inference(avatar_split_clause,[],[f72,f332,f328])).
% 0.69/0.37 thf(f337,definition,(
% 0.69/0.37 spl23_55 <=> ($false = sF5)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition])).
% 0.69/0.37 thf(f339,plain,(
% 0.69/0.37 ($false = sF5) | ~spl23_55),
% 0.69/0.37 inference(avatar_component_clause,[],[f337])).
% 0.69/0.37 thf(f341,definition,(
% 0.69/0.37 spl23_56 <=> (((f2 @ sF4)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_56])],[avatar_definition])).
% 0.69/0.37 thf(f343,plain,(
% 0.69/0.37 (((f2 @ sF4)) = $true) | ~spl23_56),
% 0.69/0.37 inference(avatar_component_clause,[],[f341])).
% 0.69/0.37 thf(f344,plain,(
% 0.69/0.37 spl23_55 | spl23_56),
% 0.69/0.37 inference(avatar_split_clause,[],[f71,f341,f337])).
% 0.69/0.37 thf(f346,definition,(
% 0.69/0.37 spl23_57 <=> ($false = sF14)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_57])],[avatar_definition])).
% 0.69/0.37 thf(f348,plain,(
% 0.69/0.37 ($false = sF14) | ~spl23_57),
% 0.69/0.37 inference(avatar_component_clause,[],[f346])).
% 0.69/0.37 thf(f350,definition,(
% 0.69/0.37 spl23_58 <=> ($true = ((f4 @ sF13)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_58])],[avatar_definition])).
% 0.69/0.37 thf(f352,plain,(
% 0.69/0.37 ($true = ((f4 @ sF13))) | ~spl23_58),
% 0.69/0.37 inference(avatar_component_clause,[],[f350])).
% 0.69/0.37 thf(f353,plain,(
% 0.69/0.37 spl23_57 | spl23_58),
% 0.69/0.37 inference(avatar_split_clause,[],[f74,f350,f346])).
% 0.69/0.37 thf(f355,definition,(
% 0.69/0.37 spl23_59 <=> ($false = ((f4 @ sF13)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition])).
% 0.69/0.37 thf(f357,plain,(
% 0.69/0.37 ($false = ((f4 @ sF13))) | ~spl23_59),
% 0.69/0.37 inference(avatar_component_clause,[],[f355])).
% 0.69/0.37 thf(f359,definition,(
% 0.69/0.37 spl23_60 <=> (sF14 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_60])],[avatar_definition])).
% 0.69/0.37 thf(f361,plain,(
% 0.69/0.37 (sF14 = $true) | ~spl23_60),
% 0.69/0.37 inference(avatar_component_clause,[],[f359])).
% 0.69/0.37 thf(f362,plain,(
% 0.69/0.37 spl23_59 | spl23_60),
% 0.69/0.37 inference(avatar_split_clause,[],[f73,f359,f355])).
% 0.69/0.37 thf(f364,definition,(
% 0.69/0.37 spl23_61 <=> (sF18 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_61])],[avatar_definition])).
% 0.69/0.37 thf(f365,plain,(
% 0.69/0.37 (sF18 != $true) | spl23_61),
% 0.69/0.37 inference(avatar_component_clause,[],[f364])).
% 0.69/0.37 thf(f366,plain,(
% 0.69/0.37 (sF18 = $true) | ~spl23_61),
% 0.69/0.37 inference(avatar_component_clause,[],[f364])).
% 0.69/0.37 thf(f368,definition,(
% 0.69/0.37 spl23_62 <=> ($false = ((f2 @ sF17)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_62])],[avatar_definition])).
% 0.69/0.37 thf(f370,plain,(
% 0.69/0.37 ($false = ((f2 @ sF17))) | ~spl23_62),
% 0.69/0.37 inference(avatar_component_clause,[],[f368])).
% 0.69/0.37 thf(f371,plain,(
% 0.69/0.37 spl23_61 | spl23_62),
% 0.69/0.37 inference(avatar_split_clause,[],[f76,f368,f364])).
% 0.69/0.37 thf(f373,definition,(
% 0.69/0.37 spl23_63 <=> ($false = sF18)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_63])],[avatar_definition])).
% 0.69/0.37 thf(f375,plain,(
% 0.69/0.37 ($false = sF18) | ~spl23_63),
% 0.69/0.37 inference(avatar_component_clause,[],[f373])).
% 0.69/0.37 thf(f377,definition,(
% 0.69/0.37 spl23_64 <=> (((f2 @ sF17)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_64])],[avatar_definition])).
% 0.69/0.37 thf(f379,plain,(
% 0.69/0.37 (((f2 @ sF17)) = $true) | ~spl23_64),
% 0.69/0.37 inference(avatar_component_clause,[],[f377])).
% 0.69/0.37 thf(f380,plain,(
% 0.69/0.37 spl23_63 | spl23_64),
% 0.69/0.37 inference(avatar_split_clause,[],[f75,f377,f373])).
% 0.69/0.37 thf(f382,definition,(
% 0.69/0.37 spl23_65 <=> (((f1 @ sF18)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition])).
% 0.69/0.37 thf(f384,plain,(
% 0.69/0.37 (((f1 @ sF18)) = $true) | ~spl23_65),
% 0.69/0.37 inference(avatar_component_clause,[],[f382])).
% 0.69/0.37 thf(f386,definition,(
% 0.69/0.37 spl23_66 <=> (sF19 = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_66])],[avatar_definition])).
% 0.69/0.37 thf(f387,plain,(
% 0.69/0.37 (sF19 != $false) | spl23_66),
% 0.69/0.37 inference(avatar_component_clause,[],[f386])).
% 0.69/0.37 thf(f388,plain,(
% 0.69/0.37 (sF19 = $false) | ~spl23_66),
% 0.69/0.37 inference(avatar_component_clause,[],[f386])).
% 0.69/0.37 thf(f389,plain,(
% 0.69/0.37 spl23_65 | spl23_66),
% 0.69/0.37 inference(avatar_split_clause,[],[f78,f386,f382])).
% 0.69/0.37 thf(f391,definition,(
% 0.69/0.37 spl23_67 <=> ($false = ((f1 @ sF18)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_67])],[avatar_definition])).
% 0.69/0.37 thf(f393,plain,(
% 0.69/0.37 ($false = ((f1 @ sF18))) | ~spl23_67),
% 0.69/0.37 inference(avatar_component_clause,[],[f391])).
% 0.69/0.37 thf(f395,definition,(
% 0.69/0.37 spl23_68 <=> (sF19 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_68])],[avatar_definition])).
% 0.69/0.37 thf(f396,plain,(
% 0.69/0.37 (sF19 != $true) | spl23_68),
% 0.69/0.37 inference(avatar_component_clause,[],[f395])).
% 0.69/0.37 thf(f397,plain,(
% 0.69/0.37 (sF19 = $true) | ~spl23_68),
% 0.69/0.37 inference(avatar_component_clause,[],[f395])).
% 0.69/0.37 thf(f398,plain,(
% 0.69/0.37 spl23_67 | spl23_68),
% 0.69/0.37 inference(avatar_split_clause,[],[f77,f395,f391])).
% 0.69/0.37 thf(f400,definition,(
% 0.69/0.37 spl23_69 <=> ($true = sF15)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_69])],[avatar_definition])).
% 0.69/0.37 thf(f401,plain,(
% 0.69/0.37 ($true != sF15) | spl23_69),
% 0.69/0.37 inference(avatar_component_clause,[],[f400])).
% 0.69/0.37 thf(f402,plain,(
% 0.69/0.37 ($true = sF15) | ~spl23_69),
% 0.69/0.37 inference(avatar_component_clause,[],[f400])).
% 0.69/0.37 thf(f404,definition,(
% 0.69/0.37 spl23_70 <=> (((f3 @ sF14)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_70])],[avatar_definition])).
% 0.69/0.37 thf(f406,plain,(
% 0.69/0.37 (((f3 @ sF14)) = $false) | ~spl23_70),
% 0.69/0.37 inference(avatar_component_clause,[],[f404])).
% 0.69/0.37 thf(f407,plain,(
% 0.69/0.37 spl23_69 | spl23_70),
% 0.69/0.37 inference(avatar_split_clause,[],[f80,f404,f400])).
% 0.69/0.37 thf(f409,definition,(
% 0.69/0.37 spl23_71 <=> ($false = sF15)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_71])],[avatar_definition])).
% 0.69/0.37 thf(f411,plain,(
% 0.69/0.37 ($false = sF15) | ~spl23_71),
% 0.69/0.37 inference(avatar_component_clause,[],[f409])).
% 0.69/0.37 thf(f413,definition,(
% 0.69/0.37 spl23_72 <=> (((f3 @ sF14)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_72])],[avatar_definition])).
% 0.69/0.37 thf(f415,plain,(
% 0.69/0.37 (((f3 @ sF14)) = $true) | ~spl23_72),
% 0.69/0.37 inference(avatar_component_clause,[],[f413])).
% 0.69/0.37 thf(f416,plain,(
% 0.69/0.37 spl23_71 | spl23_72),
% 0.69/0.37 inference(avatar_split_clause,[],[f79,f413,f409])).
% 0.69/0.37 thf(f418,definition,(
% 0.69/0.37 spl23_73 <=> (((f5 @ sF0)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_73])],[avatar_definition])).
% 0.69/0.37 thf(f420,plain,(
% 0.69/0.37 (((f5 @ sF0)) = $false) | ~spl23_73),
% 0.69/0.37 inference(avatar_component_clause,[],[f418])).
% 0.69/0.37 thf(f422,definition,(
% 0.69/0.37 spl23_74 <=> (sF12 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_74])],[avatar_definition])).
% 0.69/0.37 thf(f424,plain,(
% 0.69/0.37 (sF12 = $true) | ~spl23_74),
% 0.69/0.37 inference(avatar_component_clause,[],[f422])).
% 0.69/0.37 thf(f425,plain,(
% 0.69/0.37 spl23_73 | spl23_74),
% 0.69/0.37 inference(avatar_split_clause,[],[f82,f422,f418])).
% 0.69/0.37 thf(f427,definition,(
% 0.69/0.37 spl23_75 <=> ($false = sF12)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_75])],[avatar_definition])).
% 0.69/0.37 thf(f429,plain,(
% 0.69/0.37 ($false = sF12) | ~spl23_75),
% 0.69/0.37 inference(avatar_component_clause,[],[f427])).
% 0.69/0.37 thf(f431,definition,(
% 0.69/0.37 spl23_76 <=> (((f5 @ sF0)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_76])],[avatar_definition])).
% 0.69/0.37 thf(f432,plain,(
% 0.69/0.37 (((f5 @ sF0)) != $true) | spl23_76),
% 0.69/0.37 inference(avatar_component_clause,[],[f431])).
% 0.69/0.37 thf(f433,plain,(
% 0.69/0.37 (((f5 @ sF0)) = $true) | ~spl23_76),
% 0.69/0.37 inference(avatar_component_clause,[],[f431])).
% 0.69/0.37 thf(f434,plain,(
% 0.69/0.37 spl23_75 | spl23_76),
% 0.69/0.37 inference(avatar_split_clause,[],[f81,f431,f427])).
% 0.69/0.37 thf(f436,definition,(
% 0.69/0.37 spl23_77 <=> (sF0 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_77])],[avatar_definition])).
% 0.69/0.37 thf(f437,plain,(
% 0.69/0.37 (sF0 != $true) | spl23_77),
% 0.69/0.37 inference(avatar_component_clause,[],[f436])).
% 0.69/0.37 thf(f438,plain,(
% 0.69/0.37 (sF0 = $true) | ~spl23_77),
% 0.69/0.37 inference(avatar_component_clause,[],[f436])).
% 0.69/0.37 thf(f440,definition,(
% 0.69/0.37 spl23_78 <=> (((f5 @ x)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_78])],[avatar_definition])).
% 0.69/0.37 thf(f441,plain,(
% 0.69/0.37 (((f5 @ x)) != $false) | spl23_78),
% 0.69/0.37 inference(avatar_component_clause,[],[f440])).
% 0.69/0.37 thf(f442,plain,(
% 0.69/0.37 (((f5 @ x)) = $false) | ~spl23_78),
% 0.69/0.37 inference(avatar_component_clause,[],[f440])).
% 0.69/0.37 thf(f443,plain,(
% 0.69/0.37 spl23_77 | spl23_78),
% 0.69/0.37 inference(avatar_split_clause,[],[f84,f440,f436])).
% 0.69/0.37 thf(f445,definition,(
% 0.69/0.37 spl23_79 <=> (((f5 @ x)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_79])],[avatar_definition])).
% 0.69/0.37 thf(f447,plain,(
% 0.69/0.37 (((f5 @ x)) = $true) | ~spl23_79),
% 0.69/0.37 inference(avatar_component_clause,[],[f445])).
% 0.69/0.37 thf(f449,definition,(
% 0.69/0.37 spl23_80 <=> ($false = sF0)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_80])],[avatar_definition])).
% 0.69/0.37 thf(f451,plain,(
% 0.69/0.37 ($false = sF0) | ~spl23_80),
% 0.69/0.37 inference(avatar_component_clause,[],[f449])).
% 0.69/0.37 thf(f452,plain,(
% 0.69/0.37 spl23_79 | spl23_80),
% 0.69/0.37 inference(avatar_split_clause,[],[f83,f449,f445])).
% 0.69/0.37 thf(f454,definition,(
% 0.69/0.37 spl23_81 <=> (((f4 @ sF1)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_81])],[avatar_definition])).
% 0.69/0.37 thf(f455,plain,(
% 0.69/0.37 (((f4 @ sF1)) != $true) | spl23_81),
% 0.69/0.37 inference(avatar_component_clause,[],[f454])).
% 0.69/0.37 thf(f456,plain,(
% 0.69/0.37 (((f4 @ sF1)) = $true) | ~spl23_81),
% 0.69/0.37 inference(avatar_component_clause,[],[f454])).
% 0.69/0.37 thf(f458,definition,(
% 0.69/0.37 spl23_82 <=> (sF2 = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_82])],[avatar_definition])).
% 0.69/0.37 thf(f460,plain,(
% 0.69/0.37 (sF2 = $false) | ~spl23_82),
% 0.69/0.37 inference(avatar_component_clause,[],[f458])).
% 0.69/0.37 thf(f461,plain,(
% 0.69/0.37 spl23_81 | spl23_82),
% 0.69/0.37 inference(avatar_split_clause,[],[f86,f458,f454])).
% 0.69/0.37 thf(f463,definition,(
% 0.69/0.37 spl23_83 <=> (sF2 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_83])],[avatar_definition])).
% 0.69/0.37 thf(f464,plain,(
% 0.69/0.37 (sF2 != $true) | spl23_83),
% 0.69/0.37 inference(avatar_component_clause,[],[f463])).
% 0.69/0.37 thf(f465,plain,(
% 0.69/0.37 (sF2 = $true) | ~spl23_83),
% 0.69/0.37 inference(avatar_component_clause,[],[f463])).
% 0.69/0.37 thf(f467,definition,(
% 0.69/0.37 spl23_84 <=> (((f4 @ sF1)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_84])],[avatar_definition])).
% 0.69/0.37 thf(f468,plain,(
% 0.69/0.37 (((f4 @ sF1)) != $false) | spl23_84),
% 0.69/0.37 inference(avatar_component_clause,[],[f467])).
% 0.69/0.37 thf(f469,plain,(
% 0.69/0.37 (((f4 @ sF1)) = $false) | ~spl23_84),
% 0.69/0.37 inference(avatar_component_clause,[],[f467])).
% 0.69/0.37 thf(f470,plain,(
% 0.69/0.37 spl23_83 | spl23_84),
% 0.69/0.37 inference(avatar_split_clause,[],[f85,f467,f463])).
% 0.69/0.37 thf(f472,definition,(
% 0.69/0.37 spl23_85 <=> (sF3 = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_85])],[avatar_definition])).
% 0.69/0.37 thf(f474,plain,(
% 0.69/0.37 (sF3 = $false) | ~spl23_85),
% 0.69/0.37 inference(avatar_component_clause,[],[f472])).
% 0.69/0.37 thf(f476,definition,(
% 0.69/0.37 spl23_86 <=> (((f4 @ sF2)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_86])],[avatar_definition])).
% 0.69/0.37 thf(f477,plain,(
% 0.69/0.37 (((f4 @ sF2)) != $true) | spl23_86),
% 0.69/0.37 inference(avatar_component_clause,[],[f476])).
% 0.69/0.37 thf(f478,plain,(
% 0.69/0.37 (((f4 @ sF2)) = $true) | ~spl23_86),
% 0.69/0.37 inference(avatar_component_clause,[],[f476])).
% 0.69/0.37 thf(f479,plain,(
% 0.69/0.37 spl23_85 | spl23_86),
% 0.69/0.37 inference(avatar_split_clause,[],[f88,f476,f472])).
% 0.69/0.37 thf(f481,definition,(
% 0.69/0.37 spl23_87 <=> (((f4 @ sF2)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_87])],[avatar_definition])).
% 0.69/0.37 thf(f483,plain,(
% 0.69/0.37 (((f4 @ sF2)) = $false) | ~spl23_87),
% 0.69/0.37 inference(avatar_component_clause,[],[f481])).
% 0.69/0.37 thf(f485,definition,(
% 0.69/0.37 spl23_88 <=> (sF3 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_88])],[avatar_definition])).
% 0.69/0.37 thf(f487,plain,(
% 0.69/0.37 (sF3 = $true) | ~spl23_88),
% 0.69/0.37 inference(avatar_component_clause,[],[f485])).
% 0.69/0.37 thf(f488,plain,(
% 0.69/0.37 spl23_87 | spl23_88),
% 0.69/0.37 inference(avatar_split_clause,[],[f87,f485,f481])).
% 0.69/0.37 thf(f490,definition,(
% 0.69/0.37 spl23_89 <=> ($false = sF21)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_89])],[avatar_definition])).
% 0.69/0.37 thf(f492,plain,(
% 0.69/0.37 ($false = sF21) | ~spl23_89),
% 0.69/0.37 inference(avatar_component_clause,[],[f490])).
% 0.69/0.37 thf(f494,definition,(
% 0.69/0.37 spl23_90 <=> ($true = ((f1 @ sF20)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_90])],[avatar_definition])).
% 0.69/0.37 thf(f496,plain,(
% 0.69/0.37 ($true = ((f1 @ sF20))) | ~spl23_90),
% 0.69/0.37 inference(avatar_component_clause,[],[f494])).
% 0.69/0.37 thf(f497,plain,(
% 0.69/0.37 spl23_89 | spl23_90),
% 0.69/0.37 inference(avatar_split_clause,[],[f90,f494,f490])).
% 0.69/0.37 thf(f499,definition,(
% 0.69/0.37 spl23_91 <=> ($false = ((f1 @ sF20)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_91])],[avatar_definition])).
% 0.69/0.37 thf(f501,plain,(
% 0.69/0.37 ($false = ((f1 @ sF20))) | ~spl23_91),
% 0.69/0.37 inference(avatar_component_clause,[],[f499])).
% 0.69/0.37 thf(f503,definition,(
% 0.69/0.37 spl23_92 <=> (sF21 = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_92])],[avatar_definition])).
% 0.69/0.37 thf(f505,plain,(
% 0.69/0.37 (sF21 = $true) | ~spl23_92),
% 0.69/0.37 inference(avatar_component_clause,[],[f503])).
% 0.69/0.37 thf(f506,plain,(
% 0.69/0.37 spl23_91 | spl23_92),
% 0.69/0.37 inference(avatar_split_clause,[],[f89,f503,f499])).
% 0.69/0.37 thf(f507,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_13 | ~spl23_14)),
% 0.69/0.37 inference(forward_demodulation,[],[f153,f148])).
% 0.69/0.37 thf(f508,plain,(
% 0.69/0.37 $false | (~spl23_13 | ~spl23_14)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f507])).
% 0.69/0.37 thf(f509,plain,(
% 0.69/0.37 ~spl23_13 | ~spl23_14),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f508])).
% 0.69/0.37 thf(f526,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_33 | ~spl23_35)),
% 0.69/0.37 inference(forward_demodulation,[],[f249,f240])).
% 0.69/0.37 thf(f527,plain,(
% 0.69/0.37 $false | (~spl23_33 | ~spl23_35)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f526])).
% 0.69/0.37 thf(f528,plain,(
% 0.69/0.37 ~spl23_33 | ~spl23_35),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f527])).
% 0.69/0.37 thf(f529,plain,(
% 0.69/0.37 ($false = sF13) | ($true != $true) | spl23_33),
% 0.69/0.37 inference(constrained_superposition,[],[f239,f6])).
% 0.69/0.37 thf(f530,plain,(
% 0.69/0.37 ($false = sF13) | spl23_33),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f529])).
% 0.69/0.37 thf(f531,plain,(
% 0.69/0.37 spl23_35 | spl23_33),
% 0.69/0.37 inference(avatar_split_clause,[],[f530,f238,f247])).
% 0.69/0.37 thf(f544,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_53 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f339,f330])).
% 0.69/0.37 thf(f545,plain,(
% 0.69/0.37 $false | (~spl23_53 | ~spl23_55)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f544])).
% 0.69/0.37 thf(f546,plain,(
% 0.69/0.37 ~spl23_53 | ~spl23_55),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f545])).
% 0.69/0.37 thf(f547,plain,(
% 0.69/0.37 ($false = ((f2 @ $false))) | (~spl23_17 | ~spl23_54)),
% 0.69/0.37 inference(forward_demodulation,[],[f334,f167])).
% 0.69/0.37 thf(f548,plain,(
% 0.69/0.37 ($false = sF5) | ($true != $true) | spl23_53),
% 0.69/0.37 inference(constrained_superposition,[],[f329,f6])).
% 0.69/0.37 thf(f549,plain,(
% 0.69/0.37 ($false = sF5) | spl23_53),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f548])).
% 0.69/0.37 thf(f550,plain,(
% 0.69/0.37 spl23_55 | spl23_53),
% 0.69/0.37 inference(avatar_split_clause,[],[f549,f328,f337])).
% 0.69/0.37 thf(f559,plain,(
% 0.69/0.37 ($false = ((f2 @ $true))) | (~spl23_47 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f370,f303])).
% 0.69/0.37 thf(f560,plain,(
% 0.69/0.37 ($true != $true) | ($false = sF18) | spl23_61),
% 0.69/0.37 inference(constrained_superposition,[],[f365,f6])).
% 0.69/0.37 thf(f561,plain,(
% 0.69/0.37 ($false = sF18) | spl23_61),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f560])).
% 0.69/0.37 thf(f562,plain,(
% 0.69/0.37 spl23_63 | spl23_61),
% 0.69/0.37 inference(avatar_split_clause,[],[f561,f364,f373])).
% 0.69/0.37 thf(f566,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_69 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f411,f402])).
% 0.69/0.37 thf(f567,plain,(
% 0.69/0.37 $false | (~spl23_69 | ~spl23_71)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f566])).
% 0.69/0.37 thf(f568,plain,(
% 0.69/0.37 ~spl23_69 | ~spl23_71),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f567])).
% 0.69/0.37 thf(f569,plain,(
% 0.69/0.37 ($false = ((f3 @ $false))) | (~spl23_57 | ~spl23_70)),
% 0.69/0.37 inference(forward_demodulation,[],[f406,f348])).
% 0.69/0.37 thf(f570,plain,(
% 0.69/0.37 ($true != $true) | ($false = sF15) | spl23_69),
% 0.69/0.37 inference(constrained_superposition,[],[f401,f6])).
% 0.69/0.37 thf(f571,plain,(
% 0.69/0.37 ($false = sF15) | spl23_69),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f570])).
% 0.69/0.37 thf(f572,plain,(
% 0.69/0.37 spl23_71 | spl23_69),
% 0.69/0.37 inference(avatar_split_clause,[],[f571,f400,f409])).
% 0.69/0.37 thf(f582,plain,(
% 0.69/0.37 ($true = ((f3 @ $false))) | (~spl23_2 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f98,f411])).
% 0.69/0.37 thf(f590,definition,(
% 0.69/0.37 spl23_93 <=> (((f1 @ $true)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_93])],[avatar_definition])).
% 0.69/0.37 thf(f592,plain,(
% 0.69/0.37 (((f1 @ $true)) = $false) | ~spl23_93),
% 0.69/0.37 inference(avatar_component_clause,[],[f590])).
% 0.69/0.37 thf(f597,plain,(
% 0.69/0.37 ($false = ((f3 @ $false))) | (~spl23_15 | ~spl23_85)),
% 0.69/0.37 inference(forward_demodulation,[],[f158,f474])).
% 0.69/0.37 thf(f598,plain,(
% 0.69/0.37 (sF19 = $false) | (((f1 @ $true)) = $true) | ~spl23_21),
% 0.69/0.37 inference(constrained_superposition,[],[f185,f6])).
% 0.69/0.37 thf(f600,definition,(
% 0.69/0.37 spl23_94 <=> (((f1 @ $true)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_94])],[avatar_definition])).
% 0.69/0.37 thf(f602,plain,(
% 0.69/0.37 (((f1 @ $true)) = $true) | ~spl23_94),
% 0.69/0.37 inference(avatar_component_clause,[],[f600])).
% 0.69/0.37 thf(f603,plain,(
% 0.69/0.37 spl23_66 | spl23_94 | ~spl23_21),
% 0.69/0.37 inference(avatar_split_clause,[],[f598,f183,f600,f386])).
% 0.69/0.37 thf(f604,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_19 | ~spl23_22)),
% 0.69/0.37 inference(forward_demodulation,[],[f189,f176])).
% 0.69/0.37 thf(f605,plain,(
% 0.69/0.37 $false | (~spl23_19 | ~spl23_22)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f604])).
% 0.69/0.37 thf(f606,plain,(
% 0.69/0.37 ~spl23_19 | ~spl23_22),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f605])).
% 0.69/0.37 thf(f607,plain,(
% 0.69/0.37 ($true != $true) | ($false = sF20) | spl23_19),
% 0.69/0.37 inference(constrained_superposition,[],[f175,f6])).
% 0.69/0.37 thf(f608,plain,(
% 0.69/0.37 ($false = sF20) | spl23_19),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f607])).
% 0.69/0.37 thf(f609,plain,(
% 0.69/0.37 spl23_22 | spl23_19),
% 0.69/0.37 inference(avatar_split_clause,[],[f608,f174,f187])).
% 0.69/0.37 thf(f613,plain,(
% 0.69/0.37 (((f1 @ $true)) = $false) | (sF19 = $false) | ~spl23_20),
% 0.69/0.37 inference(constrained_superposition,[],[f180,f6])).
% 0.69/0.37 thf(f616,plain,(
% 0.69/0.37 spl23_93 | spl23_66 | ~spl23_20),
% 0.69/0.37 inference(avatar_split_clause,[],[f613,f178,f386,f590])).
% 0.69/0.37 thf(f620,plain,(
% 0.69/0.37 (((f1 @ $false)) = $true) | (~spl23_21 | ~spl23_66)),
% 0.69/0.37 inference(forward_demodulation,[],[f185,f388])).
% 0.69/0.37 thf(f622,plain,(
% 0.69/0.37 (((f0 @ $false)) = $true) | (~spl23_11 | ~spl23_25)),
% 0.69/0.37 inference(forward_demodulation,[],[f204,f139])).
% 0.69/0.37 thf(f623,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | (~spl23_27 | ~spl23_29)),
% 0.69/0.37 inference(forward_demodulation,[],[f222,f213])).
% 0.69/0.37 thf(f625,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_37 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f258,f339])).
% 0.69/0.37 thf(f626,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_39 | ~spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f276,f267])).
% 0.69/0.37 thf(f627,plain,(
% 0.69/0.37 ($false = ((f2 @ $true))) | (~spl23_39 | ~spl23_43)),
% 0.69/0.37 inference(forward_demodulation,[],[f285,f267])).
% 0.69/0.37 thf(f628,plain,(
% 0.69/0.37 ($true = ((f3 @ $true))) | ($false = sF16) | ~spl23_46),
% 0.69/0.37 inference(constrained_superposition,[],[f298,f6])).
% 0.69/0.37 thf(f630,definition,(
% 0.69/0.37 spl23_95 <=> ($true = ((f3 @ $true)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_95])],[avatar_definition])).
% 0.69/0.37 thf(f632,plain,(
% 0.69/0.37 ($true = ((f3 @ $true))) | ~spl23_95),
% 0.69/0.37 inference(avatar_component_clause,[],[f630])).
% 0.69/0.37 thf(f633,plain,(
% 0.69/0.37 spl23_95 | spl23_1 | ~spl23_46),
% 0.69/0.37 inference(avatar_split_clause,[],[f628,f296,f92,f630])).
% 0.69/0.37 thf(f634,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_51 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f321,f438])).
% 0.69/0.37 thf(f635,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_35 | ~spl23_59)),
% 0.69/0.37 inference(forward_demodulation,[],[f357,f249])).
% 0.69/0.37 thf(f637,plain,(
% 0.69/0.37 (((f1 @ $false)) = $false) | (~spl23_63 | ~spl23_67)),
% 0.69/0.37 inference(forward_demodulation,[],[f393,f375])).
% 0.69/0.37 thf(f639,plain,(
% 0.69/0.37 (x = $false) | (((f5 @ $true)) = $true) | ~spl23_79),
% 0.69/0.37 inference(constrained_superposition,[],[f447,f6])).
% 0.69/0.37 thf(f641,definition,(
% 0.69/0.37 spl23_96 <=> (((f5 @ $true)) = $true)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_96])],[avatar_definition])).
% 0.69/0.37 thf(f645,definition,(
% 0.69/0.37 spl23_97 <=> (x = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_97])],[avatar_definition])).
% 0.69/0.37 thf(f646,plain,(
% 0.69/0.37 (x != $false) | spl23_97),
% 0.69/0.37 inference(avatar_component_clause,[],[f645])).
% 0.69/0.37 thf(f647,plain,(
% 0.69/0.37 (x = $false) | ~spl23_97),
% 0.69/0.37 inference(avatar_component_clause,[],[f645])).
% 0.69/0.37 thf(f648,plain,(
% 0.69/0.37 spl23_96 | spl23_97 | ~spl23_79),
% 0.69/0.37 inference(avatar_split_clause,[],[f639,f445,f645,f641])).
% 0.69/0.37 thf(f652,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_49 | ~spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f456,f312])).
% 0.69/0.37 thf(f654,plain,(
% 0.69/0.37 (((f1 @ $true)) = $false) | (~spl23_19 | ~spl23_91)),
% 0.69/0.37 inference(forward_demodulation,[],[f501,f176])).
% 0.69/0.37 thf(f655,plain,(
% 0.69/0.37 spl23_93 | ~spl23_19 | ~spl23_91),
% 0.69/0.37 inference(avatar_split_clause,[],[f654,f499,f174,f590])).
% 0.69/0.37 thf(f661,plain,(
% 0.69/0.37 (((f1 @ $true)) = $true) | (~spl23_19 | ~spl23_90)),
% 0.69/0.37 inference(forward_demodulation,[],[f496,f176])).
% 0.69/0.37 thf(f662,plain,(
% 0.69/0.37 spl23_94 | ~spl23_19 | ~spl23_90),
% 0.69/0.37 inference(avatar_split_clause,[],[f661,f494,f174,f600])).
% 0.69/0.37 thf(f673,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_2 | ~spl23_57 | ~spl23_70 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f582,f569])).
% 0.69/0.37 thf(f674,plain,(
% 0.69/0.37 $false | (~spl23_2 | ~spl23_57 | ~spl23_70 | ~spl23_71)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f673])).
% 0.69/0.37 thf(f675,plain,(
% 0.69/0.37 ~spl23_2 | ~spl23_57 | ~spl23_70 | ~spl23_71),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f674])).
% 0.69/0.37 thf(f676,plain,(
% 0.69/0.37 ($true = ((f3 @ $false))) | (~spl23_57 | ~spl23_72)),
% 0.69/0.37 inference(forward_demodulation,[],[f415,f348])).
% 0.69/0.37 thf(f678,plain,(
% 0.69/0.37 ($true = ((f3 @ $true))) | (~spl23_2 | ~spl23_69)),
% 0.69/0.37 inference(forward_demodulation,[],[f98,f402])).
% 0.69/0.37 thf(f679,plain,(
% 0.69/0.37 spl23_95 | ~spl23_2 | ~spl23_69),
% 0.69/0.37 inference(avatar_split_clause,[],[f678,f400,f96,f630])).
% 0.69/0.37 thf(f686,plain,(
% 0.69/0.37 (((f0 @ $true)) = $true) | (~spl23_27 | ~spl23_32)),
% 0.69/0.37 inference(forward_demodulation,[],[f235,f213])).
% 0.69/0.37 thf(f692,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_5 | ~spl23_7)),
% 0.69/0.37 inference(forward_demodulation,[],[f121,f112])).
% 0.69/0.37 thf(f693,plain,(
% 0.69/0.37 $false | (~spl23_5 | ~spl23_7)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f692])).
% 0.69/0.37 thf(f694,plain,(
% 0.69/0.37 ~spl23_5 | ~spl23_7),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f693])).
% 0.69/0.37 thf(f695,plain,(
% 0.69/0.37 ($false = sF10) | (((f0 @ $true)) != $false) | spl23_5),
% 0.69/0.37 inference(constrained_superposition,[],[f111,f6])).
% 0.69/0.37 thf(f708,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_17 | ~spl23_37 | ~spl23_54 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f625,f547])).
% 0.69/0.37 thf(f709,plain,(
% 0.69/0.37 $false | (~spl23_17 | ~spl23_37 | ~spl23_54 | ~spl23_55)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f708])).
% 0.69/0.37 thf(f710,plain,(
% 0.69/0.37 ~spl23_17 | ~spl23_37 | ~spl23_54 | ~spl23_55),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f709])).
% 0.69/0.37 thf(f711,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_17 | ~spl23_56)),
% 0.69/0.37 inference(forward_demodulation,[],[f343,f167])).
% 0.69/0.37 thf(f717,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_37 | ~spl23_53)),
% 0.69/0.37 inference(forward_demodulation,[],[f258,f330])).
% 0.69/0.37 thf(f718,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_37 | ~spl23_47 | ~spl23_53 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f717,f559])).
% 0.69/0.37 thf(f719,plain,(
% 0.69/0.37 $false | (~spl23_37 | ~spl23_47 | ~spl23_53 | ~spl23_62)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f718])).
% 0.69/0.37 thf(f720,plain,(
% 0.69/0.37 ~spl23_37 | ~spl23_47 | ~spl23_53 | ~spl23_62),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f719])).
% 0.69/0.37 thf(f721,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_46 | ~spl23_48)),
% 0.69/0.37 inference(forward_demodulation,[],[f307,f298])).
% 0.69/0.37 thf(f722,plain,(
% 0.69/0.37 $false | (~spl23_46 | ~spl23_48)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f721])).
% 0.69/0.37 thf(f723,plain,(
% 0.69/0.37 ~spl23_46 | ~spl23_48),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f722])).
% 0.69/0.37 thf(f736,plain,(
% 0.69/0.37 ($false = ((f3 @ $false))) | (~spl23_1 | ~spl23_48)),
% 0.69/0.37 inference(forward_demodulation,[],[f307,f94])).
% 0.69/0.37 thf(f737,plain,(
% 0.69/0.37 ($false = ((f2 @ $false))) | (~spl23_45 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f370,f294])).
% 0.69/0.37 thf(f742,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_39 | ~spl23_41 | ~spl23_43)),
% 0.69/0.37 inference(forward_demodulation,[],[f627,f626])).
% 0.69/0.37 thf(f743,plain,(
% 0.69/0.37 $false | (~spl23_39 | ~spl23_41 | ~spl23_43)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f742])).
% 0.69/0.37 thf(f744,plain,(
% 0.69/0.37 ~spl23_39 | ~spl23_41 | ~spl23_43),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f743])).
% 0.69/0.37 thf(f758,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_21 | ~spl23_63 | ~spl23_66 | ~spl23_67)),
% 0.69/0.37 inference(forward_demodulation,[],[f637,f620])).
% 0.69/0.37 thf(f759,plain,(
% 0.69/0.37 $false | (~spl23_21 | ~spl23_63 | ~spl23_66 | ~spl23_67)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f758])).
% 0.69/0.37 thf(f760,plain,(
% 0.69/0.37 ~spl23_21 | ~spl23_63 | ~spl23_66 | ~spl23_67),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f759])).
% 0.69/0.37 thf(f763,plain,(
% 0.69/0.37 (((f1 @ $true)) = $true) | (~spl23_61 | ~spl23_65)),
% 0.69/0.37 inference(forward_demodulation,[],[f384,f366])).
% 0.69/0.37 thf(f764,plain,(
% 0.69/0.37 spl23_94 | ~spl23_61 | ~spl23_65),
% 0.69/0.37 inference(avatar_split_clause,[],[f763,f382,f364,f600])).
% 0.69/0.37 thf(f765,plain,(
% 0.69/0.37 (((f1 @ $true)) = $false) | (~spl23_61 | ~spl23_67)),
% 0.69/0.37 inference(forward_demodulation,[],[f393,f366])).
% 0.69/0.37 thf(f766,plain,(
% 0.69/0.37 spl23_93 | ~spl23_61 | ~spl23_67),
% 0.69/0.37 inference(avatar_split_clause,[],[f765,f391,f364,f590])).
% 0.69/0.37 thf(f767,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_66 | ~spl23_68)),
% 0.69/0.37 inference(forward_demodulation,[],[f397,f388])).
% 0.69/0.37 thf(f768,plain,(
% 0.69/0.37 $false | (~spl23_66 | ~spl23_68)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f767])).
% 0.69/0.37 thf(f769,plain,(
% 0.69/0.37 ~spl23_66 | ~spl23_68),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f768])).
% 0.69/0.37 thf(f770,plain,(
% 0.69/0.37 (((f1 @ $false)) = $false) | (~spl23_20 | ~spl23_66)),
% 0.69/0.37 inference(forward_demodulation,[],[f180,f388])).
% 0.69/0.37 thf(f785,plain,(
% 0.69/0.37 (((f1 @ $false)) = $true) | (~spl23_22 | ~spl23_90)),
% 0.69/0.37 inference(forward_demodulation,[],[f496,f189])).
% 0.69/0.37 thf(f790,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_35 | ~spl23_49 | ~spl23_59 | ~spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f652,f635])).
% 0.69/0.37 thf(f791,plain,(
% 0.69/0.37 $false | (~spl23_35 | ~spl23_49 | ~spl23_59 | ~spl23_81)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f790])).
% 0.69/0.37 thf(f792,plain,(
% 0.69/0.37 ~spl23_35 | ~spl23_49 | ~spl23_59 | ~spl23_81),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f791])).
% 0.69/0.37 thf(f799,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_33 | ~spl23_59)),
% 0.69/0.37 inference(forward_demodulation,[],[f357,f240])).
% 0.69/0.37 thf(f800,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_15 | ~spl23_57 | ~spl23_72 | ~spl23_85)),
% 0.69/0.37 inference(forward_demodulation,[],[f676,f597])).
% 0.69/0.37 thf(f801,plain,(
% 0.69/0.37 $false | (~spl23_15 | ~spl23_57 | ~spl23_72 | ~spl23_85)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f800])).
% 0.69/0.37 thf(f802,plain,(
% 0.69/0.37 ~spl23_15 | ~spl23_57 | ~spl23_72 | ~spl23_85),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f801])).
% 0.69/0.37 thf(f804,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_16 | ~spl23_17)),
% 0.69/0.37 inference(forward_demodulation,[],[f162,f167])).
% 0.69/0.37 thf(f805,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_17)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f804])).
% 0.69/0.37 thf(f806,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_17),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f805])).
% 0.69/0.37 thf(f808,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f478,f465])).
% 0.69/0.37 thf(f809,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_51 | ~spl23_77 | ~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f808,f634])).
% 0.69/0.37 thf(f810,plain,(
% 0.69/0.37 $false | (~spl23_51 | ~spl23_77 | ~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f809])).
% 0.69/0.37 thf(f811,plain,(
% 0.69/0.37 ~spl23_51 | ~spl23_77 | ~spl23_83 | ~spl23_86),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f810])).
% 0.69/0.37 thf(f812,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_49 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f469,f312])).
% 0.69/0.37 thf(f813,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_49 | ~spl23_81 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f812,f652])).
% 0.69/0.37 thf(f814,plain,(
% 0.69/0.37 $false | (~spl23_49 | ~spl23_81 | ~spl23_84)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f813])).
% 0.69/0.37 thf(f815,plain,(
% 0.69/0.37 ~spl23_49 | ~spl23_81 | ~spl23_84),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f814])).
% 0.69/0.37 thf(f816,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_50 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f316,f438])).
% 0.69/0.37 thf(f817,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_50 | ~spl23_51 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f816,f634])).
% 0.69/0.37 thf(f818,plain,(
% 0.69/0.37 $false | (~spl23_50 | ~spl23_51 | ~spl23_77)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f817])).
% 0.69/0.37 thf(f819,plain,(
% 0.69/0.37 ~spl23_50 | ~spl23_51 | ~spl23_77),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f818])).
% 0.69/0.37 thf(f823,plain,(
% 0.69/0.37 ($true != $true) | (sF2 = $false) | spl23_83),
% 0.69/0.37 inference(constrained_superposition,[],[f464,f6])).
% 0.69/0.37 thf(f824,plain,(
% 0.69/0.37 (sF2 = $false) | spl23_83),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f823])).
% 0.69/0.37 thf(f825,plain,(
% 0.69/0.37 spl23_82 | spl23_83),
% 0.69/0.37 inference(avatar_split_clause,[],[f824,f463,f458])).
% 0.69/0.37 thf(f830,plain,(
% 0.69/0.37 ($false = ((f3 @ $true))) | (sF3 = $false) | ~spl23_15),
% 0.69/0.37 inference(constrained_superposition,[],[f158,f6])).
% 0.69/0.37 thf(f834,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_52 | ~spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f456,f325])).
% 0.69/0.37 thf(f835,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_52 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f469,f325])).
% 0.69/0.37 thf(f836,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_82 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f478,f460])).
% 0.69/0.37 thf(f837,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_82 | ~spl23_87)),
% 0.69/0.37 inference(forward_demodulation,[],[f483,f460])).
% 0.69/0.37 thf(f841,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_27 | ~spl23_29 | ~spl23_32)),
% 0.69/0.37 inference(forward_demodulation,[],[f686,f623])).
% 0.69/0.37 thf(f842,plain,(
% 0.69/0.37 $false | (~spl23_27 | ~spl23_29 | ~spl23_32)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f841])).
% 0.69/0.37 thf(f843,plain,(
% 0.69/0.37 ~spl23_27 | ~spl23_29 | ~spl23_32),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f842])).
% 0.69/0.37 thf(f852,plain,(
% 0.69/0.37 (((f0 @ $false)) = $true) | (~spl23_7 | ~spl23_31)),
% 0.69/0.37 inference(constrained_superposition,[],[f121,f231])).
% 0.69/0.37 thf(f875,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_17 | ~spl23_45 | ~spl23_56 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f737,f711])).
% 0.69/0.37 thf(f876,plain,(
% 0.69/0.37 $false | (~spl23_17 | ~spl23_45 | ~spl23_56 | ~spl23_62)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f875])).
% 0.69/0.37 thf(f877,plain,(
% 0.69/0.37 ~spl23_17 | ~spl23_45 | ~spl23_56 | ~spl23_62),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f876])).
% 0.69/0.37 thf(f878,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_38 | ~spl23_39)),
% 0.69/0.37 inference(forward_demodulation,[],[f262,f267])).
% 0.69/0.37 thf(f879,plain,(
% 0.69/0.37 $false | (~spl23_38 | ~spl23_39)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f878])).
% 0.69/0.37 thf(f880,plain,(
% 0.69/0.37 ~spl23_38 | ~spl23_39),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f879])).
% 0.69/0.37 thf(f910,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_20 | ~spl23_22 | ~spl23_66 | ~spl23_90)),
% 0.69/0.37 inference(forward_demodulation,[],[f785,f770])).
% 0.69/0.37 thf(f911,plain,(
% 0.69/0.37 $false | (~spl23_20 | ~spl23_22 | ~spl23_66 | ~spl23_90)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f910])).
% 0.69/0.37 thf(f912,plain,(
% 0.69/0.37 ~spl23_20 | ~spl23_22 | ~spl23_66 | ~spl23_90),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f911])).
% 0.69/0.37 thf(f919,plain,(
% 0.69/0.37 ($false = ((f0 @ $false))) | (~spl23_23 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f194,f492])).
% 0.69/0.37 thf(f920,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_11 | ~spl23_23 | ~spl23_25 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f919,f622])).
% 0.69/0.37 thf(f921,plain,(
% 0.69/0.37 $false | (~spl23_11 | ~spl23_23 | ~spl23_25 | ~spl23_89)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f920])).
% 0.69/0.37 thf(f922,plain,(
% 0.69/0.37 ~spl23_11 | ~spl23_23 | ~spl23_25 | ~spl23_89),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f921])).
% 0.69/0.37 thf(f923,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_9 | ~spl23_12)),
% 0.69/0.37 inference(forward_demodulation,[],[f143,f130])).
% 0.69/0.37 thf(f924,plain,(
% 0.69/0.37 $false | (~spl23_9 | ~spl23_12)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f923])).
% 0.69/0.37 thf(f925,plain,(
% 0.69/0.37 ~spl23_9 | ~spl23_12),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f924])).
% 0.69/0.37 thf(f927,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_26 | ~spl23_27)),
% 0.69/0.37 inference(forward_demodulation,[],[f208,f213])).
% 0.69/0.37 thf(f928,plain,(
% 0.69/0.37 $false | (~spl23_26 | ~spl23_27)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f927])).
% 0.69/0.37 thf(f929,plain,(
% 0.69/0.37 ~spl23_26 | ~spl23_27),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f928])).
% 0.69/0.37 thf(f935,plain,(
% 0.69/0.37 (((f0 @ $false)) != $true) | (~spl23_11 | spl23_25)),
% 0.69/0.37 inference(forward_demodulation,[],[f203,f139])).
% 0.69/0.37 thf(f936,plain,(
% 0.69/0.37 ($false = ((f0 @ $false))) | (~spl23_11 | ~spl23_28)),
% 0.69/0.37 inference(forward_demodulation,[],[f217,f139])).
% 0.69/0.37 thf(f943,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_33 | ~spl23_50 | ~spl23_59 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f816,f799])).
% 0.69/0.37 thf(f944,plain,(
% 0.69/0.37 $false | (~spl23_33 | ~spl23_50 | ~spl23_59 | ~spl23_77)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f943])).
% 0.69/0.37 thf(f945,plain,(
% 0.69/0.37 ~spl23_33 | ~spl23_50 | ~spl23_59 | ~spl23_77),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f944])).
% 0.69/0.37 thf(f946,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_78 | ~spl23_79)),
% 0.69/0.37 inference(forward_demodulation,[],[f442,f447])).
% 0.69/0.37 thf(f947,plain,(
% 0.69/0.37 $false | (~spl23_78 | ~spl23_79)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f946])).
% 0.69/0.37 thf(f948,plain,(
% 0.69/0.37 ~spl23_78 | ~spl23_79),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f947])).
% 0.69/0.37 thf(f949,plain,(
% 0.69/0.37 ($false = ((f5 @ $false))) | (~spl23_78 | ~spl23_97)),
% 0.69/0.37 inference(forward_demodulation,[],[f442,f647])).
% 0.69/0.37 thf(f963,plain,(
% 0.69/0.37 ($false = sF0) | ($true != $true) | spl23_77),
% 0.69/0.37 inference(constrained_superposition,[],[f437,f6])).
% 0.69/0.37 thf(f964,plain,(
% 0.69/0.37 ($false = sF0) | spl23_77),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f963])).
% 0.69/0.37 thf(f965,plain,(
% 0.69/0.37 spl23_80 | spl23_77),
% 0.69/0.37 inference(avatar_split_clause,[],[f964,f436,f449])).
% 0.69/0.37 thf(f969,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_50 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f316,f451])).
% 0.69/0.37 thf(f972,plain,(
% 0.69/0.37 ($false = ((f5 @ $false))) | (~spl23_73 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f420,f451])).
% 0.69/0.37 thf(f977,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_52 | ~spl23_81 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f835,f834])).
% 0.69/0.37 thf(f978,plain,(
% 0.69/0.37 $false | (~spl23_52 | ~spl23_81 | ~spl23_84)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f977])).
% 0.69/0.37 thf(f979,plain,(
% 0.69/0.37 ~spl23_52 | ~spl23_81 | ~spl23_84),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f978])).
% 0.69/0.37 thf(f984,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_82 | ~spl23_86 | ~spl23_87)),
% 0.69/0.37 inference(forward_demodulation,[],[f837,f836])).
% 0.69/0.37 thf(f985,plain,(
% 0.69/0.37 $false | (~spl23_82 | ~spl23_86 | ~spl23_87)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f984])).
% 0.69/0.37 thf(f986,plain,(
% 0.69/0.37 ~spl23_82 | ~spl23_86 | ~spl23_87),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f985])).
% 0.69/0.37 thf(f1021,plain,(
% 0.69/0.37 (((f5 @ $false)) = $true) | (~spl23_76 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f433,f451])).
% 0.69/0.37 thf(f1024,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_76 | ~spl23_78 | ~spl23_80 | ~spl23_97)),
% 0.69/0.37 inference(forward_demodulation,[],[f1021,f949])).
% 0.69/0.37 thf(f1025,plain,(
% 0.69/0.37 $false | (~spl23_76 | ~spl23_78 | ~spl23_80 | ~spl23_97)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1024])).
% 0.69/0.37 thf(f1026,plain,(
% 0.69/0.37 ~spl23_76 | ~spl23_78 | ~spl23_80 | ~spl23_97),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1025])).
% 0.69/0.37 thf(f1034,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_34 | ~spl23_36)),
% 0.69/0.37 inference(forward_demodulation,[],[f253,f244])).
% 0.69/0.37 thf(f1035,plain,(
% 0.69/0.37 $false | (~spl23_34 | ~spl23_36)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1034])).
% 0.69/0.37 thf(f1036,plain,(
% 0.69/0.37 ~spl23_34 | ~spl23_36),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1035])).
% 0.69/0.37 thf(f1038,plain,(
% 0.69/0.37 (((f4 @ $false)) != $true) | (~spl23_82 | spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f477,f460])).
% 0.69/0.37 thf(f1040,definition,(
% 0.69/0.37 spl23_98 <=> ($false = ((f3 @ $true)))),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_98])],[avatar_definition])).
% 0.69/0.37 thf(f1042,plain,(
% 0.69/0.37 ($false = ((f3 @ $true))) | ~spl23_98),
% 0.69/0.37 inference(avatar_component_clause,[],[f1040])).
% 0.69/0.37 thf(f1043,plain,(
% 0.69/0.37 spl23_85 | spl23_98 | ~spl23_15),
% 0.69/0.37 inference(avatar_split_clause,[],[f830,f156,f1040,f472])).
% 0.69/0.37 thf(f1054,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_35 | ~spl23_59)),
% 0.69/0.37 inference(forward_demodulation,[],[f357,f249])).
% 0.69/0.37 thf(f1055,plain,(
% 0.69/0.37 (((f5 @ $true)) = $false) | (x = $false) | ~spl23_78),
% 0.69/0.37 inference(constrained_superposition,[],[f442,f6])).
% 0.69/0.37 thf(f1058,plain,(
% 0.69/0.37 (((f5 @ $true)) = $false) | (~spl23_78 | spl23_97)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1055,f646])).
% 0.69/0.37 thf(f1064,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_73 | ~spl23_76 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f1021,f972])).
% 0.69/0.37 thf(f1065,plain,(
% 0.69/0.37 $false | (~spl23_73 | ~spl23_76 | ~spl23_80)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1064])).
% 0.69/0.37 thf(f1066,plain,(
% 0.69/0.37 ~spl23_73 | ~spl23_76 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1065])).
% 0.69/0.37 thf(f1070,plain,(
% 0.69/0.37 $false | (~spl23_50 | ~spl23_80 | ~spl23_82 | spl23_86)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1038,f969])).
% 0.69/0.37 thf(f1071,plain,(
% 0.69/0.37 ~spl23_50 | ~spl23_80 | ~spl23_82 | spl23_86),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1070])).
% 0.69/0.37 thf(f1072,plain,(
% 0.69/0.37 (((f4 @ $true)) != $false) | (~spl23_52 | spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f468,f325])).
% 0.69/0.37 thf(f1076,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_83 | ~spl23_87)),
% 0.69/0.37 inference(forward_demodulation,[],[f483,f465])).
% 0.69/0.37 thf(f1077,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_35 | ~spl23_50 | ~spl23_59 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f1054,f969])).
% 0.69/0.37 thf(f1078,plain,(
% 0.69/0.37 $false | (~spl23_35 | ~spl23_50 | ~spl23_59 | ~spl23_80)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1077])).
% 0.69/0.37 thf(f1079,plain,(
% 0.69/0.37 ~spl23_35 | ~spl23_50 | ~spl23_59 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1078])).
% 0.69/0.37 thf(f1080,plain,(
% 0.69/0.37 (((f5 @ $true)) != $false) | (spl23_34 | ~spl23_74)),
% 0.69/0.37 inference(forward_demodulation,[],[f243,f424])).
% 0.69/0.37 thf(f1084,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_33 | ~spl23_59)),
% 0.69/0.37 inference(forward_demodulation,[],[f357,f240])).
% 0.69/0.37 thf(f1093,plain,(
% 0.69/0.37 $false | (~spl23_52 | ~spl23_83 | spl23_84 | ~spl23_87)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1076,f1072])).
% 0.69/0.37 thf(f1094,plain,(
% 0.69/0.37 ~spl23_52 | ~spl23_83 | spl23_84 | ~spl23_87),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1093])).
% 0.69/0.37 thf(f1095,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_51 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f321,f451])).
% 0.69/0.37 thf(f1096,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_50 | ~spl23_51 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f1095,f969])).
% 0.69/0.37 thf(f1097,plain,(
% 0.69/0.37 $false | (~spl23_50 | ~spl23_51 | ~spl23_80)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1096])).
% 0.69/0.37 thf(f1098,plain,(
% 0.69/0.37 ~spl23_50 | ~spl23_51 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1097])).
% 0.69/0.37 thf(f1101,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f478,f465])).
% 0.69/0.37 thf(f1117,plain,(
% 0.69/0.37 ($false = ((f4 @ $false))) | (~spl23_51 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f321,f451])).
% 0.69/0.37 thf(f1123,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_49 | ~spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f456,f312])).
% 0.69/0.37 thf(f1125,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_33 | ~spl23_59 | ~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f1101,f1084])).
% 0.69/0.37 thf(f1126,plain,(
% 0.69/0.37 $false | (~spl23_33 | ~spl23_59 | ~spl23_83 | ~spl23_86)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1125])).
% 0.69/0.37 thf(f1127,plain,(
% 0.69/0.37 ~spl23_33 | ~spl23_59 | ~spl23_83 | ~spl23_86),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1126])).
% 0.69/0.37 thf(f1137,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_49 | ~spl23_51 | ~spl23_80 | ~spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f1123,f1117])).
% 0.69/0.37 thf(f1138,plain,(
% 0.69/0.37 $false | (~spl23_49 | ~spl23_51 | ~spl23_80 | ~spl23_81)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1137])).
% 0.69/0.37 thf(f1139,plain,(
% 0.69/0.37 ~spl23_49 | ~spl23_51 | ~spl23_80 | ~spl23_81),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1138])).
% 0.69/0.37 thf(f1140,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_82 | ~spl23_83)),
% 0.69/0.37 inference(forward_demodulation,[],[f460,f465])).
% 0.69/0.37 thf(f1141,plain,(
% 0.69/0.37 $false | (~spl23_82 | ~spl23_83)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1140])).
% 0.69/0.37 thf(f1142,plain,(
% 0.69/0.37 ~spl23_82 | ~spl23_83),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1141])).
% 0.69/0.37 thf(f1169,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_7 | ~spl23_23 | ~spl23_31 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f852,f919])).
% 0.69/0.37 thf(f1170,plain,(
% 0.69/0.37 $false | (~spl23_7 | ~spl23_23 | ~spl23_31 | ~spl23_89)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1169])).
% 0.69/0.37 thf(f1171,plain,(
% 0.69/0.37 ~spl23_7 | ~spl23_23 | ~spl23_31 | ~spl23_89),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1170])).
% 0.69/0.37 thf(f1173,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_6 | ~spl23_8)),
% 0.69/0.37 inference(forward_demodulation,[],[f125,f116])).
% 0.69/0.37 thf(f1174,plain,(
% 0.69/0.37 $false | (~spl23_6 | ~spl23_8)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1173])).
% 0.69/0.37 thf(f1175,plain,(
% 0.69/0.37 ~spl23_6 | ~spl23_8),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1174])).
% 0.69/0.37 thf(f1179,definition,(
% 0.69/0.37 spl23_99 <=> (((f0 @ $true)) = $false)),
% 0.69/0.37 introduced(definition,[new_symbols(definition,[spl23_99])],[avatar_definition])).
% 0.69/0.37 thf(f1180,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | ~spl23_99),
% 0.69/0.37 inference(avatar_component_clause,[],[f1179])).
% 0.69/0.37 thf(f1182,plain,(
% 0.69/0.37 ~spl23_99 | spl23_31 | spl23_5),
% 0.69/0.37 inference(avatar_split_clause,[],[f695,f110,f229,f1179])).
% 0.69/0.37 thf(f1183,plain,(
% 0.69/0.37 (((f0 @ $false)) = $true) | (~spl23_26 | ~spl23_32)),
% 0.69/0.37 inference(forward_demodulation,[],[f235,f208])).
% 0.69/0.37 thf(f1187,plain,(
% 0.69/0.37 (((f0 @ $false)) = $true) | (~spl23_24 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f199,f492])).
% 0.69/0.37 thf(f1198,plain,(
% 0.69/0.37 ($false = sF10) | (((f0 @ $true)) = $false) | ~spl23_5),
% 0.69/0.37 inference(constrained_superposition,[],[f112,f6])).
% 0.69/0.37 thf(f1203,plain,(
% 0.69/0.37 spl23_31 | spl23_99 | ~spl23_5),
% 0.69/0.37 inference(avatar_split_clause,[],[f1198,f110,f1179,f229])).
% 0.69/0.37 thf(f1205,plain,(
% 0.69/0.37 ($false = ((f0 @ $false))) | (~spl23_5 | ~spl23_31)),
% 0.69/0.37 inference(constrained_superposition,[],[f112,f231])).
% 0.69/0.37 thf(f1213,plain,(
% 0.69/0.37 $false | (~spl23_11 | spl23_25 | ~spl23_26 | ~spl23_32)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1183,f935])).
% 0.69/0.37 thf(f1214,plain,(
% 0.69/0.37 ~spl23_11 | spl23_25 | ~spl23_26 | ~spl23_32),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1213])).
% 0.69/0.37 thf(f1226,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_11 | ~spl23_24 | ~spl23_28 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f1187,f936])).
% 0.69/0.37 thf(f1227,plain,(
% 0.69/0.37 $false | (~spl23_11 | ~spl23_24 | ~spl23_28 | ~spl23_89)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1226])).
% 0.69/0.37 thf(f1228,plain,(
% 0.69/0.37 ~spl23_11 | ~spl23_24 | ~spl23_28 | ~spl23_89),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1227])).
% 0.69/0.37 thf(f1233,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | (~spl23_27 | ~spl23_29)),
% 0.69/0.37 inference(forward_demodulation,[],[f222,f213])).
% 0.69/0.37 thf(f1234,plain,(
% 0.69/0.37 spl23_99 | ~spl23_27 | ~spl23_29),
% 0.69/0.37 inference(avatar_split_clause,[],[f1233,f220,f211,f1179])).
% 0.69/0.37 thf(f1245,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_95 | ~spl23_98)),
% 0.69/0.37 inference(forward_demodulation,[],[f1042,f632])).
% 0.69/0.37 thf(f1246,plain,(
% 0.69/0.37 $false | (~spl23_95 | ~spl23_98)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1245])).
% 0.69/0.37 thf(f1247,plain,(
% 0.69/0.37 ~spl23_95 | ~spl23_98),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1246])).
% 0.69/0.37 thf(f1249,plain,(
% 0.69/0.37 $false | (spl23_34 | ~spl23_74 | ~spl23_78 | spl23_97)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1058,f1080])).
% 0.69/0.37 thf(f1250,plain,(
% 0.69/0.37 spl23_34 | ~spl23_74 | ~spl23_78 | spl23_97),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1249])).
% 0.69/0.37 thf(f1251,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_77 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f438,f451])).
% 0.69/0.37 thf(f1252,plain,(
% 0.69/0.37 $false | (~spl23_77 | ~spl23_80)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1251])).
% 0.69/0.37 thf(f1253,plain,(
% 0.69/0.37 ~spl23_77 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1252])).
% 0.69/0.37 thf(f1254,plain,(
% 0.69/0.37 ($false = ((f5 @ $false))) | (~spl23_73 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f420,f451])).
% 0.69/0.37 thf(f1263,plain,(
% 0.69/0.37 ($false != ((f5 @ $false))) | (spl23_34 | ~spl23_75)),
% 0.69/0.37 inference(forward_demodulation,[],[f243,f429])).
% 0.69/0.37 thf(f1276,plain,(
% 0.69/0.37 $false | (spl23_34 | ~spl23_73 | ~spl23_75 | ~spl23_80)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1263,f1254])).
% 0.69/0.37 thf(f1277,plain,(
% 0.69/0.37 spl23_34 | ~spl23_73 | ~spl23_75 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1276])).
% 0.69/0.37 thf(f1297,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_5 | ~spl23_24 | ~spl23_31 | ~spl23_89)),
% 0.69/0.37 inference(forward_demodulation,[],[f1205,f1187])).
% 0.69/0.37 thf(f1298,plain,(
% 0.69/0.37 $false | (~spl23_5 | ~spl23_24 | ~spl23_31 | ~spl23_89)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1297])).
% 0.69/0.37 thf(f1299,plain,(
% 0.69/0.37 ~spl23_5 | ~spl23_24 | ~spl23_31 | ~spl23_89),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1298])).
% 0.69/0.37 thf(f1300,plain,(
% 0.69/0.37 (((f1 @ $false)) != $false) | (spl23_9 | ~spl23_42)),
% 0.69/0.37 inference(forward_demodulation,[],[f129,f280])).
% 0.69/0.37 thf(f1302,plain,(
% 0.69/0.37 $false | (spl23_9 | ~spl23_20 | ~spl23_42 | ~spl23_66)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1300,f770])).
% 0.69/0.37 thf(f1303,plain,(
% 0.69/0.37 spl23_9 | ~spl23_20 | ~spl23_42 | ~spl23_66),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1302])).
% 0.69/0.37 thf(f1307,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_38 | ~spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f276,f262])).
% 0.69/0.37 thf(f1308,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_38 | ~spl23_41 | ~spl23_45 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f1307,f737])).
% 0.69/0.37 thf(f1309,plain,(
% 0.69/0.37 $false | (~spl23_38 | ~spl23_41 | ~spl23_45 | ~spl23_62)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1308])).
% 0.69/0.37 thf(f1310,plain,(
% 0.69/0.37 ~spl23_38 | ~spl23_41 | ~spl23_45 | ~spl23_62),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1309])).
% 0.69/0.37 thf(f1337,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_15 | ~spl23_18)),
% 0.69/0.37 inference(forward_demodulation,[],[f171,f158])).
% 0.69/0.37 thf(f1338,plain,(
% 0.69/0.37 $false | (~spl23_15 | ~spl23_18)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1337])).
% 0.69/0.37 thf(f1339,plain,(
% 0.69/0.37 ~spl23_15 | ~spl23_18),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1338])).
% 0.69/0.37 thf(f1340,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_37 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f258,f339])).
% 0.69/0.37 thf(f1341,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_37 | ~spl23_45 | ~spl23_55 | ~spl23_62)),
% 0.69/0.37 inference(forward_demodulation,[],[f1340,f737])).
% 0.69/0.37 thf(f1342,plain,(
% 0.69/0.37 $false | (~spl23_37 | ~spl23_45 | ~spl23_55 | ~spl23_62)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1341])).
% 0.69/0.37 thf(f1343,plain,(
% 0.69/0.37 ~spl23_37 | ~spl23_45 | ~spl23_55 | ~spl23_62),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1342])).
% 0.69/0.37 thf(f1344,plain,(
% 0.69/0.37 ($false != ((f3 @ $false))) | (spl23_15 | ~spl23_85)),
% 0.69/0.37 inference(forward_demodulation,[],[f157,f474])).
% 0.69/0.37 thf(f1346,plain,(
% 0.69/0.37 $false | (~spl23_1 | spl23_15 | ~spl23_48 | ~spl23_85)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1344,f736])).
% 0.69/0.37 thf(f1347,plain,(
% 0.69/0.37 ~spl23_1 | spl23_15 | ~spl23_48 | ~spl23_85),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1346])).
% 0.69/0.37 thf(f1364,plain,(
% 0.69/0.37 ($false = sF6) | ($true != $true) | spl23_39),
% 0.69/0.37 inference(constrained_superposition,[],[f266,f6])).
% 0.69/0.37 thf(f1365,plain,(
% 0.69/0.37 ($false = sF6) | spl23_39),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1364])).
% 0.69/0.37 thf(f1366,plain,(
% 0.69/0.37 $false | (spl23_38 | spl23_39)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1365,f261])).
% 0.69/0.37 thf(f1367,plain,(
% 0.69/0.37 spl23_38 | spl23_39),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1366])).
% 0.69/0.37 thf(f1380,plain,(
% 0.69/0.37 (((f0 @ $true)) = $true) | (~spl23_10 | ~spl23_25)),
% 0.69/0.37 inference(forward_demodulation,[],[f204,f134])).
% 0.69/0.37 thf(f1381,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_10 | ~spl23_25 | ~spl23_99)),
% 0.69/0.37 inference(forward_demodulation,[],[f1380,f1180])).
% 0.69/0.37 thf(f1382,plain,(
% 0.69/0.37 $false | (~spl23_10 | ~spl23_25 | ~spl23_99)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1381])).
% 0.69/0.37 thf(f1383,plain,(
% 0.69/0.37 ~spl23_10 | ~spl23_25 | ~spl23_99),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1382])).
% 0.69/0.37 thf(f1390,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_37 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f258,f339])).
% 0.69/0.37 thf(f1391,plain,(
% 0.69/0.37 ($false = ((f2 @ $false))) | (~spl23_40 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f271,f339])).
% 0.69/0.37 thf(f1392,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_39 | ~spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f276,f267])).
% 0.69/0.37 thf(f1394,plain,(
% 0.69/0.37 ($false = ((f2 @ $true))) | (~spl23_16 | ~spl23_54)),
% 0.69/0.37 inference(forward_demodulation,[],[f334,f162])).
% 0.69/0.37 thf(f1403,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_35 | ~spl23_58)),
% 0.69/0.37 inference(forward_demodulation,[],[f352,f249])).
% 0.69/0.37 thf(f1404,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_35 | ~spl23_51 | ~spl23_58 | ~spl23_80)),
% 0.69/0.37 inference(forward_demodulation,[],[f1403,f1117])).
% 0.69/0.37 thf(f1405,plain,(
% 0.69/0.37 $false | (~spl23_35 | ~spl23_51 | ~spl23_58 | ~spl23_80)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1404])).
% 0.69/0.37 thf(f1406,plain,(
% 0.69/0.37 ~spl23_35 | ~spl23_51 | ~spl23_58 | ~spl23_80),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1405])).
% 0.69/0.37 thf(f1408,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_74 | ~spl23_75)),
% 0.69/0.37 inference(forward_demodulation,[],[f424,f429])).
% 0.69/0.37 thf(f1409,plain,(
% 0.69/0.37 $false | (~spl23_74 | ~spl23_75)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1408])).
% 0.69/0.37 thf(f1410,plain,(
% 0.69/0.37 ~spl23_74 | ~spl23_75),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1409])).
% 0.69/0.37 thf(f1418,plain,(
% 0.69/0.37 ($true != ((f3 @ $true))) | (spl23_2 | ~spl23_69)),
% 0.69/0.37 inference(forward_demodulation,[],[f97,f402])).
% 0.69/0.37 thf(f1421,plain,(
% 0.69/0.37 ~spl23_95 | spl23_2 | ~spl23_69),
% 0.69/0.37 inference(avatar_split_clause,[],[f1418,f400,f96,f630])).
% 0.69/0.37 thf(f1422,plain,(
% 0.69/0.37 ($false = ((f3 @ $true))) | (~spl23_3 | ~spl23_69)),
% 0.69/0.37 inference(forward_demodulation,[],[f103,f402])).
% 0.69/0.37 thf(f1423,plain,(
% 0.69/0.37 spl23_98 | ~spl23_3 | ~spl23_69),
% 0.69/0.37 inference(avatar_split_clause,[],[f1422,f400,f101,f1040])).
% 0.69/0.37 thf(f1424,plain,(
% 0.69/0.37 ($false != ((f3 @ $true))) | (spl23_3 | ~spl23_69)),
% 0.69/0.37 inference(forward_demodulation,[],[f102,f402])).
% 0.69/0.37 thf(f1425,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_1 | ~spl23_4)),
% 0.69/0.37 inference(forward_demodulation,[],[f107,f94])).
% 0.69/0.37 thf(f1426,plain,(
% 0.69/0.37 $false | (~spl23_1 | ~spl23_4)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1425])).
% 0.69/0.37 thf(f1427,plain,(
% 0.69/0.37 ~spl23_1 | ~spl23_4),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1426])).
% 0.69/0.37 thf(f1428,plain,(
% 0.69/0.37 ~spl23_98 | spl23_3 | ~spl23_69),
% 0.69/0.37 inference(avatar_split_clause,[],[f1424,f400,f101,f1040])).
% 0.69/0.37 thf(f1440,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_37 | ~spl23_40 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f1391,f1390])).
% 0.69/0.37 thf(f1441,plain,(
% 0.69/0.37 $false | (~spl23_37 | ~spl23_40 | ~spl23_55)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1440])).
% 0.69/0.37 thf(f1442,plain,(
% 0.69/0.37 ~spl23_37 | ~spl23_40 | ~spl23_55),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1441])).
% 0.69/0.37 thf(f1450,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_16 | ~spl23_39 | ~spl23_41 | ~spl23_54)),
% 0.69/0.37 inference(forward_demodulation,[],[f1394,f1392])).
% 0.69/0.37 thf(f1451,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_39 | ~spl23_41 | ~spl23_54)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1450])).
% 0.69/0.37 thf(f1452,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_39 | ~spl23_41 | ~spl23_54),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1451])).
% 0.69/0.37 thf(f1454,plain,(
% 0.69/0.37 (((f0 @ $true)) != $false) | (spl23_5 | ~spl23_30)),
% 0.69/0.37 inference(forward_demodulation,[],[f111,f226])).
% 0.69/0.37 thf(f1460,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_47 | ~spl23_64)),
% 0.69/0.37 inference(forward_demodulation,[],[f379,f303])).
% 0.69/0.37 thf(f1462,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_93 | ~spl23_94)),
% 0.69/0.37 inference(forward_demodulation,[],[f592,f602])).
% 0.69/0.37 thf(f1463,plain,(
% 0.69/0.37 $false | (~spl23_93 | ~spl23_94)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1462])).
% 0.69/0.37 thf(f1464,plain,(
% 0.69/0.37 ~spl23_93 | ~spl23_94),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1463])).
% 0.69/0.37 thf(f1465,plain,(
% 0.69/0.37 ~spl23_99 | spl23_5 | ~spl23_30),
% 0.69/0.37 inference(avatar_split_clause,[],[f1454,f224,f110,f1179])).
% 0.69/0.37 thf(f1489,plain,(
% 0.69/0.37 ($true != $true) | (sF19 = $false) | spl23_68),
% 0.69/0.37 inference(constrained_superposition,[],[f396,f6])).
% 0.69/0.37 thf(f1490,plain,(
% 0.69/0.37 (sF19 = $false) | spl23_68),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1489])).
% 0.69/0.37 thf(f1491,plain,(
% 0.69/0.37 $false | (spl23_66 | spl23_68)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1490,f387])).
% 0.69/0.37 thf(f1492,plain,(
% 0.69/0.37 spl23_66 | spl23_68),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1491])).
% 0.69/0.37 thf(f1502,plain,(
% 0.69/0.37 (((f1 @ $true)) = $false) | (~spl23_20 | ~spl23_68)),
% 0.69/0.37 inference(forward_demodulation,[],[f180,f397])).
% 0.69/0.37 thf(f1503,plain,(
% 0.69/0.37 spl23_93 | ~spl23_20 | ~spl23_68),
% 0.69/0.37 inference(avatar_split_clause,[],[f1502,f395,f178,f590])).
% 0.69/0.37 thf(f1504,plain,(
% 0.69/0.37 (((f1 @ $true)) != $true) | (spl23_21 | ~spl23_68)),
% 0.69/0.37 inference(forward_demodulation,[],[f184,f397])).
% 0.69/0.37 thf(f1505,plain,(
% 0.69/0.37 ~spl23_94 | spl23_21 | ~spl23_68),
% 0.69/0.37 inference(avatar_split_clause,[],[f1504,f395,f183,f600])).
% 0.69/0.37 thf(f1506,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | (~spl23_23 | ~spl23_92)),
% 0.69/0.37 inference(forward_demodulation,[],[f194,f505])).
% 0.69/0.37 thf(f1507,plain,(
% 0.69/0.37 spl23_99 | ~spl23_23 | ~spl23_92),
% 0.69/0.37 inference(avatar_split_clause,[],[f1506,f503,f192,f1179])).
% 0.69/0.37 thf(f1508,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | (~spl23_5 | ~spl23_30)),
% 0.69/0.37 inference(forward_demodulation,[],[f112,f226])).
% 0.69/0.37 thf(f1514,plain,(
% 0.69/0.37 spl23_99 | ~spl23_5 | ~spl23_30),
% 0.69/0.37 inference(avatar_split_clause,[],[f1508,f224,f110,f1179])).
% 0.69/0.37 thf(f1516,plain,(
% 0.69/0.37 (((f0 @ $true)) = $false) | (~spl23_10 | ~spl23_28)),
% 0.69/0.37 inference(forward_demodulation,[],[f217,f134])).
% 0.69/0.37 thf(f1517,plain,(
% 0.69/0.37 spl23_99 | ~spl23_10 | ~spl23_28),
% 0.69/0.37 inference(avatar_split_clause,[],[f1516,f215,f132,f1179])).
% 0.69/0.37 thf(f1518,plain,(
% 0.69/0.37 (((f1 @ $false)) != $true) | (spl23_12 | ~spl23_42)),
% 0.69/0.37 inference(forward_demodulation,[],[f142,f280])).
% 0.69/0.37 thf(f1543,plain,(
% 0.69/0.37 (((f0 @ $true)) = $true) | (~spl23_24 | ~spl23_92)),
% 0.69/0.37 inference(forward_demodulation,[],[f199,f505])).
% 0.69/0.37 thf(f1546,plain,(
% 0.69/0.37 ($false = ((f0 @ $false))) | (~spl23_26 | ~spl23_29)),
% 0.69/0.37 inference(forward_demodulation,[],[f222,f208])).
% 0.69/0.37 thf(f1548,plain,(
% 0.69/0.37 (((f1 @ $false)) = $true) | (~spl23_63 | ~spl23_65)),
% 0.69/0.37 inference(forward_demodulation,[],[f384,f375])).
% 0.69/0.37 thf(f1551,plain,(
% 0.69/0.37 (((f1 @ $false)) = $false) | (~spl23_22 | ~spl23_91)),
% 0.69/0.37 inference(forward_demodulation,[],[f501,f189])).
% 0.69/0.37 thf(f1556,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_16 | ~spl23_47 | ~spl23_54 | ~spl23_64)),
% 0.69/0.37 inference(forward_demodulation,[],[f1460,f1394])).
% 0.69/0.37 thf(f1557,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_47 | ~spl23_54 | ~spl23_64)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1556])).
% 0.69/0.37 thf(f1558,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_47 | ~spl23_54 | ~spl23_64),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1557])).
% 0.69/0.37 thf(f1575,plain,(
% 0.69/0.37 $false | (spl23_12 | ~spl23_42 | ~spl23_63 | ~spl23_65)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1548,f1518])).
% 0.69/0.37 thf(f1576,plain,(
% 0.69/0.37 spl23_12 | ~spl23_42 | ~spl23_63 | ~spl23_65),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1575])).
% 0.69/0.37 thf(f1577,plain,(
% 0.69/0.37 (((f2 @ $false)) != $true) | (spl23_37 | ~spl23_55)),
% 0.69/0.37 inference(forward_demodulation,[],[f257,f339])).
% 0.69/0.37 thf(f1583,plain,(
% 0.69/0.37 ($false = sF7) | ($true != $true) | spl23_44),
% 0.69/0.37 inference(constrained_superposition,[],[f288,f6])).
% 0.69/0.37 thf(f1584,plain,(
% 0.69/0.37 ($false = sF7) | spl23_44),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1583])).
% 0.69/0.37 thf(f1585,plain,(
% 0.69/0.37 $false | (spl23_42 | spl23_44)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1584,f279])).
% 0.69/0.37 thf(f1586,plain,(
% 0.69/0.37 spl23_42 | spl23_44),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1585])).
% 0.69/0.37 thf(f1590,plain,(
% 0.69/0.37 (((f1 @ $true)) != $true) | (spl23_12 | ~spl23_44)),
% 0.69/0.37 inference(forward_demodulation,[],[f142,f289])).
% 0.69/0.37 thf(f1591,plain,(
% 0.69/0.37 ~spl23_94 | spl23_12 | ~spl23_44),
% 0.69/0.37 inference(avatar_split_clause,[],[f1590,f287,f141,f600])).
% 0.69/0.37 thf(f1592,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_38 | ~spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f276,f262])).
% 0.69/0.37 thf(f1593,plain,(
% 0.69/0.37 ($false = ((f2 @ $false))) | (~spl23_38 | ~spl23_43)),
% 0.69/0.37 inference(forward_demodulation,[],[f285,f262])).
% 0.69/0.37 thf(f1599,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_22 | ~spl23_63 | ~spl23_65 | ~spl23_91)),
% 0.69/0.37 inference(forward_demodulation,[],[f1551,f1548])).
% 0.69/0.37 thf(f1600,plain,(
% 0.69/0.37 $false | (~spl23_22 | ~spl23_63 | ~spl23_65 | ~spl23_91)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1599])).
% 0.69/0.37 thf(f1601,plain,(
% 0.69/0.37 ~spl23_22 | ~spl23_63 | ~spl23_65 | ~spl23_91),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1600])).
% 0.69/0.37 thf(f1609,plain,(
% 0.69/0.37 $false | (spl23_37 | ~spl23_38 | ~spl23_41 | ~spl23_55)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1592,f1577])).
% 0.69/0.37 thf(f1610,plain,(
% 0.69/0.37 spl23_37 | ~spl23_38 | ~spl23_41 | ~spl23_55),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1609])).
% 0.69/0.37 thf(f1611,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_16 | ~spl23_56)),
% 0.69/0.37 inference(forward_demodulation,[],[f343,f162])).
% 0.69/0.37 thf(f1612,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_16 | ~spl23_54 | ~spl23_56)),
% 0.69/0.37 inference(forward_demodulation,[],[f1611,f1394])).
% 0.69/0.37 thf(f1613,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_54 | ~spl23_56)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1612])).
% 0.69/0.37 thf(f1614,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_54 | ~spl23_56),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1613])).
% 0.69/0.37 thf(f1623,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_38 | ~spl23_41 | ~spl23_43)),
% 0.69/0.37 inference(forward_demodulation,[],[f1593,f1592])).
% 0.69/0.37 thf(f1624,plain,(
% 0.69/0.37 $false | (~spl23_38 | ~spl23_41 | ~spl23_43)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1623])).
% 0.69/0.37 thf(f1625,plain,(
% 0.69/0.37 ~spl23_38 | ~spl23_41 | ~spl23_43),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1624])).
% 0.69/0.37 thf(f1647,plain,(
% 0.69/0.37 ($false = ((f3 @ $false))) | (~spl23_3 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f103,f411])).
% 0.69/0.37 thf(f1658,plain,(
% 0.69/0.37 ($true = ((f3 @ $false))) | (~spl23_2 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f98,f411])).
% 0.69/0.37 thf(f1659,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_49 | ~spl23_52)),
% 0.69/0.37 inference(forward_demodulation,[],[f325,f312])).
% 0.69/0.37 thf(f1660,plain,(
% 0.69/0.37 $false | (~spl23_49 | ~spl23_52)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1659])).
% 0.69/0.37 thf(f1661,plain,(
% 0.69/0.37 ~spl23_49 | ~spl23_52),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1660])).
% 0.69/0.37 thf(f1667,plain,(
% 0.69/0.37 ($true != $true) | ($false = sF16) | spl23_4),
% 0.69/0.37 inference(constrained_superposition,[],[f106,f6])).
% 0.69/0.37 thf(f1668,plain,(
% 0.69/0.37 ($false = sF16) | spl23_4),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1667])).
% 0.69/0.37 thf(f1669,plain,(
% 0.69/0.37 $false | (spl23_1 | spl23_4)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1668,f93])).
% 0.69/0.37 thf(f1670,plain,(
% 0.69/0.37 spl23_1 | spl23_4),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1669])).
% 0.69/0.37 thf(f1686,plain,(
% 0.69/0.37 ($false != ((f3 @ $true))) | (spl23_15 | ~spl23_88)),
% 0.69/0.37 inference(forward_demodulation,[],[f157,f487])).
% 0.69/0.37 thf(f1687,plain,(
% 0.69/0.37 ~spl23_98 | spl23_15 | ~spl23_88),
% 0.69/0.37 inference(avatar_split_clause,[],[f1686,f485,f156,f1040])).
% 0.69/0.37 thf(f1688,plain,(
% 0.69/0.37 ($true = ((f3 @ $true))) | (~spl23_18 | ~spl23_88)),
% 0.69/0.37 inference(forward_demodulation,[],[f171,f487])).
% 0.69/0.37 thf(f1689,plain,(
% 0.69/0.37 spl23_95 | ~spl23_18 | ~spl23_88),
% 0.69/0.37 inference(avatar_split_clause,[],[f1688,f485,f169,f630])).
% 0.69/0.37 thf(f1691,plain,(
% 0.69/0.37 ($true != ((f3 @ $true))) | (spl23_18 | ~spl23_88)),
% 0.69/0.37 inference(forward_demodulation,[],[f170,f487])).
% 0.69/0.37 thf(f1693,plain,(
% 0.69/0.37 ~spl23_95 | spl23_18 | ~spl23_88),
% 0.69/0.37 inference(avatar_split_clause,[],[f1691,f485,f169,f630])).
% 0.69/0.37 thf(f1709,plain,(
% 0.69/0.37 ($true = ((f3 @ $false))) | (~spl23_1 | ~spl23_46)),
% 0.69/0.37 inference(forward_demodulation,[],[f298,f94])).
% 0.69/0.37 thf(f1715,plain,(
% 0.69/0.37 ($false = ((f3 @ $true))) | (~spl23_60 | ~spl23_70)),
% 0.69/0.37 inference(forward_demodulation,[],[f406,f361])).
% 0.69/0.37 thf(f1716,plain,(
% 0.69/0.37 spl23_98 | ~spl23_60 | ~spl23_70),
% 0.69/0.37 inference(avatar_split_clause,[],[f1715,f404,f359,f1040])).
% 0.69/0.37 thf(f1728,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_2 | ~spl23_3 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f1658,f1647])).
% 0.69/0.37 thf(f1729,plain,(
% 0.69/0.37 $false | (~spl23_2 | ~spl23_3 | ~spl23_71)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1728])).
% 0.69/0.37 thf(f1730,plain,(
% 0.69/0.37 ~spl23_2 | ~spl23_3 | ~spl23_71),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1729])).
% 0.69/0.37 thf(f1731,plain,(
% 0.69/0.37 ($true = ((f3 @ $true))) | (~spl23_60 | ~spl23_72)),
% 0.69/0.37 inference(forward_demodulation,[],[f415,f361])).
% 0.69/0.37 thf(f1732,plain,(
% 0.69/0.37 spl23_95 | ~spl23_60 | ~spl23_72),
% 0.69/0.37 inference(avatar_split_clause,[],[f1731,f413,f359,f630])).
% 0.69/0.37 thf(f1739,plain,(
% 0.69/0.37 ($true != ((f3 @ $false))) | (spl23_2 | ~spl23_71)),
% 0.69/0.37 inference(forward_demodulation,[],[f97,f411])).
% 0.69/0.37 thf(f1754,plain,(
% 0.69/0.37 $false | (~spl23_1 | spl23_2 | ~spl23_46 | ~spl23_71)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1739,f1709])).
% 0.69/0.37 thf(f1755,plain,(
% 0.69/0.37 ~spl23_1 | spl23_2 | ~spl23_46 | ~spl23_71),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1754])).
% 0.69/0.37 thf(f1759,plain,(
% 0.69/0.37 (((f1 @ $true)) = $true) | (~spl23_21 | ~spl23_68)),
% 0.69/0.37 inference(forward_demodulation,[],[f185,f397])).
% 0.69/0.37 thf(f1762,plain,(
% 0.69/0.37 (((f0 @ $false)) = $true) | (~spl23_7 | ~spl23_31)),
% 0.69/0.37 inference(forward_demodulation,[],[f121,f231])).
% 0.69/0.37 thf(f1765,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_24 | ~spl23_92 | ~spl23_99)),
% 0.69/0.37 inference(forward_demodulation,[],[f1180,f1543])).
% 0.69/0.37 thf(f1766,plain,(
% 0.69/0.37 $false | (~spl23_24 | ~spl23_92 | ~spl23_99)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1765])).
% 0.69/0.37 thf(f1767,plain,(
% 0.69/0.37 ~spl23_24 | ~spl23_92 | ~spl23_99),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1766])).
% 0.69/0.37 thf(f1774,plain,(
% 0.69/0.37 spl23_94 | ~spl23_21 | ~spl23_68),
% 0.69/0.37 inference(avatar_split_clause,[],[f1759,f395,f183,f600])).
% 0.69/0.37 thf(f1840,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_7 | ~spl23_26 | ~spl23_29 | ~spl23_31)),
% 0.69/0.37 inference(forward_demodulation,[],[f1762,f1546])).
% 0.69/0.37 thf(f1841,plain,(
% 0.69/0.37 $false | (~spl23_7 | ~spl23_26 | ~spl23_29 | ~spl23_31)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1840])).
% 0.69/0.37 thf(f1842,plain,(
% 0.69/0.37 ~spl23_7 | ~spl23_26 | ~spl23_29 | ~spl23_31),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1841])).
% 0.69/0.37 thf(f1878,plain,(
% 0.69/0.37 (((f0 @ $true)) != $false) | (~spl23_27 | spl23_29)),
% 0.69/0.37 inference(forward_demodulation,[],[f221,f213])).
% 0.69/0.37 thf(f1879,plain,(
% 0.69/0.37 ~spl23_99 | ~spl23_27 | spl23_29),
% 0.69/0.37 inference(avatar_split_clause,[],[f1878,f220,f211,f1179])).
% 0.69/0.37 thf(f1882,plain,(
% 0.69/0.37 ($false = ((f2 @ $true))) | (~spl23_40 | ~spl23_53)),
% 0.69/0.37 inference(forward_demodulation,[],[f271,f330])).
% 0.69/0.37 thf(f1885,plain,(
% 0.69/0.37 ($false != ((f3 @ $true))) | (~spl23_4 | spl23_48)),
% 0.69/0.37 inference(forward_demodulation,[],[f306,f107])).
% 0.69/0.37 thf(f1886,plain,(
% 0.69/0.37 ~spl23_98 | ~spl23_4 | spl23_48),
% 0.69/0.37 inference(avatar_split_clause,[],[f1885,f305,f105,f1040])).
% 0.69/0.37 thf(f1887,plain,(
% 0.69/0.37 ($false != ((f2 @ $true))) | (~spl23_16 | spl23_54)),
% 0.69/0.37 inference(forward_demodulation,[],[f333,f162])).
% 0.69/0.37 thf(f1888,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_16 | ~spl23_56)),
% 0.69/0.37 inference(forward_demodulation,[],[f343,f162])).
% 0.69/0.37 thf(f1920,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_40 | ~spl23_53 | spl23_54)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1887,f1882])).
% 0.69/0.37 thf(f1921,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_40 | ~spl23_53 | spl23_54),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1920])).
% 0.69/0.37 thf(f1922,plain,(
% 0.69/0.37 (((f2 @ $true)) = $true) | (~spl23_37 | ~spl23_53)),
% 0.69/0.37 inference(forward_demodulation,[],[f258,f330])).
% 0.69/0.37 thf(f1926,plain,(
% 0.69/0.37 (((f2 @ $true)) != $true) | (~spl23_39 | spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f275,f267])).
% 0.69/0.37 thf(f1935,plain,(
% 0.69/0.37 $false | (~spl23_16 | ~spl23_39 | spl23_41 | ~spl23_56)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1926,f1888])).
% 0.69/0.37 thf(f1936,plain,(
% 0.69/0.37 ~spl23_16 | ~spl23_39 | spl23_41 | ~spl23_56),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1935])).
% 0.69/0.37 thf(f1937,plain,(
% 0.69/0.37 (((f4 @ $false)) = $true) | (~spl23_82 | ~spl23_86)),
% 0.69/0.37 inference(forward_demodulation,[],[f478,f460])).
% 0.69/0.37 thf(f1974,plain,(
% 0.69/0.37 (((f2 @ $false)) = $true) | (~spl23_45 | ~spl23_64)),
% 0.69/0.37 inference(forward_demodulation,[],[f379,f294])).
% 0.69/0.37 thf(f1984,plain,(
% 0.69/0.37 $false | (~spl23_37 | ~spl23_39 | spl23_41 | ~spl23_53)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1926,f1922])).
% 0.69/0.37 thf(f1985,plain,(
% 0.69/0.37 ~spl23_37 | ~spl23_39 | spl23_41 | ~spl23_53),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1984])).
% 0.69/0.37 thf(f1986,plain,(
% 0.69/0.37 ($false = ((f2 @ $true))) | (~spl23_40 | ~spl23_53)),
% 0.69/0.37 inference(forward_demodulation,[],[f271,f330])).
% 0.69/0.37 thf(f1987,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_37 | ~spl23_40 | ~spl23_53)),
% 0.69/0.37 inference(forward_demodulation,[],[f1986,f1922])).
% 0.69/0.37 thf(f1988,plain,(
% 0.69/0.37 $false | (~spl23_37 | ~spl23_40 | ~spl23_53)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f1987])).
% 0.69/0.37 thf(f1989,plain,(
% 0.69/0.37 ~spl23_37 | ~spl23_40 | ~spl23_53),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f1988])).
% 0.69/0.37 thf(f1994,plain,(
% 0.69/0.37 (((f2 @ $false)) != $true) | (~spl23_38 | spl23_41)),
% 0.69/0.37 inference(forward_demodulation,[],[f275,f262])).
% 0.69/0.37 thf(f2033,plain,(
% 0.69/0.37 $false | (~spl23_38 | spl23_41 | ~spl23_45 | ~spl23_64)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f1994,f1974])).
% 0.69/0.37 thf(f2034,plain,(
% 0.69/0.37 ~spl23_38 | spl23_41 | ~spl23_45 | ~spl23_64),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f2033])).
% 0.69/0.37 thf(f2061,plain,(
% 0.69/0.37 (((f5 @ $true)) = $false) | (~spl23_73 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f420,f438])).
% 0.69/0.37 thf(f2062,plain,(
% 0.69/0.37 (((f5 @ $true)) != $true) | (spl23_76 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f432,f438])).
% 0.69/0.37 thf(f2063,plain,(
% 0.69/0.37 ~spl23_96 | spl23_76 | ~spl23_77),
% 0.69/0.37 inference(avatar_split_clause,[],[f2062,f436,f431,f641])).
% 0.69/0.37 thf(f2066,plain,(
% 0.69/0.37 ($false != ((f5 @ $false))) | (spl23_78 | ~spl23_97)),
% 0.69/0.37 inference(forward_demodulation,[],[f441,f647])).
% 0.69/0.37 thf(f2068,plain,(
% 0.69/0.37 (((f4 @ $false)) != $true) | (~spl23_49 | spl23_81)),
% 0.69/0.37 inference(forward_demodulation,[],[f455,f312])).
% 0.69/0.37 thf(f2069,plain,(
% 0.69/0.37 $false | (~spl23_49 | spl23_81 | ~spl23_82 | ~spl23_86)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f2068,f1937])).
% 0.69/0.37 thf(f2070,plain,(
% 0.69/0.37 ~spl23_49 | spl23_81 | ~spl23_82 | ~spl23_86),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f2069])).
% 0.69/0.37 thf(f2071,plain,(
% 0.69/0.37 ($false = ((f5 @ $false))) | (~spl23_34 | ~spl23_75)),
% 0.69/0.37 inference(forward_demodulation,[],[f244,f429])).
% 0.69/0.37 thf(f2072,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_50 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f316,f438])).
% 0.69/0.37 thf(f2104,plain,(
% 0.69/0.37 $false | (~spl23_34 | ~spl23_75 | spl23_78 | ~spl23_97)),
% 0.69/0.37 inference(forward_subsumption_resolution,[],[f2071,f2066])).
% 0.69/0.37 thf(f2105,plain,(
% 0.69/0.37 ~spl23_34 | ~spl23_75 | spl23_78 | ~spl23_97),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f2104])).
% 0.69/0.37 thf(f2106,plain,(
% 0.69/0.37 (((f5 @ $true)) = $true) | (~spl23_76 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f433,f438])).
% 0.69/0.37 thf(f2107,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_73 | ~spl23_76 | ~spl23_77)),
% 0.69/0.37 inference(forward_demodulation,[],[f2106,f2061])).
% 0.69/0.37 thf(f2108,plain,(
% 0.69/0.37 $false | (~spl23_73 | ~spl23_76 | ~spl23_77)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f2107])).
% 0.69/0.37 thf(f2109,plain,(
% 0.69/0.37 ~spl23_73 | ~spl23_76 | ~spl23_77),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f2108])).
% 0.69/0.37 thf(f2110,plain,(
% 0.69/0.37 spl23_96 | ~spl23_76 | ~spl23_77),
% 0.69/0.37 inference(avatar_split_clause,[],[f2106,f436,f431,f641])).
% 0.69/0.37 thf(f2114,plain,(
% 0.69/0.37 (((f5 @ $true)) != $true) | (spl23_36 | ~spl23_74)),
% 0.69/0.37 inference(forward_demodulation,[],[f252,f424])).
% 0.69/0.37 thf(f2115,plain,(
% 0.69/0.37 ~spl23_96 | spl23_36 | ~spl23_74),
% 0.69/0.37 inference(avatar_split_clause,[],[f2114,f422,f251,f641])).
% 0.69/0.37 thf(f2118,plain,(
% 0.69/0.37 (((f4 @ $true)) = $false) | (~spl23_52 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f469,f325])).
% 0.69/0.37 thf(f2137,plain,(
% 0.69/0.37 ($false = ((f3 @ $true))) | (~spl23_4 | ~spl23_48)),
% 0.69/0.37 inference(forward_demodulation,[],[f307,f107])).
% 0.69/0.37 thf(f2138,plain,(
% 0.69/0.37 spl23_98 | ~spl23_4 | ~spl23_48),
% 0.69/0.37 inference(avatar_split_clause,[],[f2137,f305,f105,f1040])).
% 0.69/0.37 thf(f2139,plain,(
% 0.69/0.37 (((f4 @ $true)) = $true) | (~spl23_33 | ~spl23_58)),
% 0.69/0.37 inference(forward_demodulation,[],[f352,f240])).
% 0.69/0.37 thf(f2153,plain,(
% 0.69/0.37 ($false = $true) | (~spl23_50 | ~spl23_52 | ~spl23_77 | ~spl23_84)),
% 0.69/0.37 inference(forward_demodulation,[],[f2118,f2072])).
% 0.69/0.37 thf(f2154,plain,(
% 0.69/0.37 $false | (~spl23_50 | ~spl23_52 | ~spl23_77 | ~spl23_84)),
% 0.69/0.37 inference(trivial_inequality_removal,[],[f2153])).
% 0.69/0.37 thf(f2155,plain,(
% 0.69/0.37 ~spl23_50 | ~spl23_52 | ~spl23_77 | ~spl23_84),
% 0.69/0.37 inference(avatar_contradiction_clause,[],[f2154])).
% 0.69/0.38 thf(f2180,plain,(
% 0.69/0.38 (((f1 @ $true)) != $false) | (spl23_9 | ~spl23_44)),
% 0.69/0.38 inference(forward_demodulation,[],[f129,f289])).
% 0.69/0.38 thf(f2181,plain,(
% 0.69/0.38 ~spl23_93 | spl23_9 | ~spl23_44),
% 0.69/0.38 inference(avatar_split_clause,[],[f2180,f287,f128,f590])).
% 0.69/0.38 thf(f2184,plain,(
% 0.69/0.38 (((f4 @ $true)) = $false) | (~spl23_51 | ~spl23_77)),
% 0.69/0.38 inference(forward_demodulation,[],[f321,f438])).
% 0.69/0.38 thf(f2265,plain,(
% 0.69/0.38 ($false = $true) | (~spl23_33 | ~spl23_51 | ~spl23_58 | ~spl23_77)),
% 0.69/0.38 inference(forward_demodulation,[],[f2184,f2139])).
% 0.69/0.38 thf(f2266,plain,(
% 0.69/0.38 $false | (~spl23_33 | ~spl23_51 | ~spl23_58 | ~spl23_77)),
% 0.69/0.38 inference(trivial_inequality_removal,[],[f2265])).
% 0.69/0.38 thf(f2267,plain,(
% 0.69/0.38 ~spl23_33 | ~spl23_51 | ~spl23_58 | ~spl23_77),
% 0.69/0.38 inference(avatar_contradiction_clause,[],[f2266])).
% 0.69/0.38 cnf(s1, plain, spl23_1 | spl23_2, inference(sat_conversion,[],[f99])).
% 0.69/0.38 cnf(s2, plain, spl23_3 | spl23_4, inference(sat_conversion,[],[f108])).
% 0.69/0.38 cnf(s3, plain, spl23_5 | spl23_6, inference(sat_conversion,[],[f117])).
% 0.69/0.38 cnf(s4, plain, spl23_7 | spl23_8, inference(sat_conversion,[],[f126])).
% 0.69/0.38 cnf(s5, plain, spl23_9 | spl23_10, inference(sat_conversion,[],[f135])).
% 0.69/0.38 cnf(s6, plain, spl23_11 | spl23_12, inference(sat_conversion,[],[f144])).
% 0.69/0.38 cnf(s7, plain, spl23_8 | spl23_13, inference(sat_conversion,[],[f149])).
% 0.69/0.38 cnf(s8, plain, spl23_6 | spl23_14, inference(sat_conversion,[],[f154])).
% 0.69/0.38 cnf(s9, plain, spl23_15 | spl23_16, inference(sat_conversion,[],[f163])).
% 0.69/0.38 cnf(s10, plain, spl23_17 | spl23_18, inference(sat_conversion,[],[f172])).
% 0.69/0.38 cnf(s11, plain, spl23_19 | spl23_20, inference(sat_conversion,[],[f181])).
% 0.69/0.38 cnf(s12, plain, spl23_21 | spl23_22, inference(sat_conversion,[],[f190])).
% 0.69/0.38 cnf(s13, plain, spl23_14 | spl23_23, inference(sat_conversion,[],[f195])).
% 0.69/0.38 cnf(s14, plain, spl23_13 | spl23_24, inference(sat_conversion,[],[f200])).
% 0.69/0.38 cnf(s15, plain, spl23_25 | spl23_26, inference(sat_conversion,[],[f209])).
% 0.69/0.38 cnf(s16, plain, spl23_27 | spl23_28, inference(sat_conversion,[],[f218])).
% 0.69/0.38 cnf(s17, plain, spl23_29 | spl23_30, inference(sat_conversion,[],[f227])).
% 0.69/0.38 cnf(s18, plain, spl23_31 | spl23_32, inference(sat_conversion,[],[f236])).
% 0.69/0.38 cnf(s19, plain, spl23_33 | spl23_34, inference(sat_conversion,[],[f245])).
% 0.69/0.38 cnf(s20, plain, spl23_35 | spl23_36, inference(sat_conversion,[],[f254])).
% 0.69/0.38 cnf(s21, plain, spl23_37 | spl23_38, inference(sat_conversion,[],[f263])).
% 0.69/0.38 cnf(s22, plain, spl23_39 | spl23_40, inference(sat_conversion,[],[f272])).
% 0.69/0.38 cnf(s23, plain, spl23_41 | spl23_42, inference(sat_conversion,[],[f281])).
% 0.69/0.38 cnf(s24, plain, spl23_43 | spl23_44, inference(sat_conversion,[],[f290])).
% 0.69/0.38 cnf(s25, plain, spl23_45 | spl23_46, inference(sat_conversion,[],[f299])).
% 0.69/0.38 cnf(s26, plain, spl23_47 | spl23_48, inference(sat_conversion,[],[f308])).
% 0.69/0.38 cnf(s27, plain, spl23_49 | spl23_50, inference(sat_conversion,[],[f317])).
% 0.69/0.38 cnf(s28, plain, spl23_51 | spl23_52, inference(sat_conversion,[],[f326])).
% 0.69/0.38 cnf(s29, plain, spl23_53 | spl23_54, inference(sat_conversion,[],[f335])).
% 0.69/0.38 cnf(s30, plain, spl23_55 | spl23_56, inference(sat_conversion,[],[f344])).
% 0.69/0.38 cnf(s31, plain, spl23_57 | spl23_58, inference(sat_conversion,[],[f353])).
% 0.69/0.38 cnf(s32, plain, spl23_59 | spl23_60, inference(sat_conversion,[],[f362])).
% 0.69/0.38 cnf(s33, plain, spl23_61 | spl23_62, inference(sat_conversion,[],[f371])).
% 0.69/0.38 cnf(s34, plain, spl23_63 | spl23_64, inference(sat_conversion,[],[f380])).
% 0.69/0.38 cnf(s35, plain, spl23_65 | spl23_66, inference(sat_conversion,[],[f389])).
% 0.69/0.38 cnf(s36, plain, spl23_67 | spl23_68, inference(sat_conversion,[],[f398])).
% 0.69/0.38 cnf(s37, plain, spl23_69 | spl23_70, inference(sat_conversion,[],[f407])).
% 0.69/0.38 cnf(s38, plain, spl23_71 | spl23_72, inference(sat_conversion,[],[f416])).
% 0.69/0.38 cnf(s39, plain, spl23_73 | spl23_74, inference(sat_conversion,[],[f425])).
% 0.69/0.38 cnf(s40, plain, spl23_75 | spl23_76, inference(sat_conversion,[],[f434])).
% 0.69/0.38 cnf(s41, plain, spl23_77 | spl23_78, inference(sat_conversion,[],[f443])).
% 0.69/0.38 cnf(s42, plain, spl23_79 | spl23_80, inference(sat_conversion,[],[f452])).
% 0.69/0.38 cnf(s43, plain, spl23_81 | spl23_82, inference(sat_conversion,[],[f461])).
% 0.69/0.38 cnf(s44, plain, spl23_83 | spl23_84, inference(sat_conversion,[],[f470])).
% 0.69/0.38 cnf(s45, plain, spl23_85 | spl23_86, inference(sat_conversion,[],[f479])).
% 0.69/0.38 cnf(s46, plain, spl23_87 | spl23_88, inference(sat_conversion,[],[f488])).
% 0.69/0.38 cnf(s47, plain, spl23_89 | spl23_90, inference(sat_conversion,[],[f497])).
% 0.69/0.38 cnf(s48, plain, spl23_91 | spl23_92, inference(sat_conversion,[],[f506])).
% 0.69/0.38 cnf(s49, plain, ~spl23_13 | ~spl23_14, inference(sat_conversion,[],[f509])).
% 0.69/0.38 cnf(s50, plain, ~spl23_33 | ~spl23_35, inference(sat_conversion,[],[f528])).
% 0.69/0.38 cnf(s51, plain, spl23_33 | spl23_35, inference(sat_conversion,[],[f531])).
% 0.69/0.38 cnf(s53, plain, ~spl23_53 | ~spl23_55, inference(sat_conversion,[],[f546])).
% 0.69/0.38 cnf(s54, plain, spl23_53 | spl23_55, inference(sat_conversion,[],[f550])).
% 0.69/0.38 cnf(s56, plain, spl23_61 | spl23_63, inference(sat_conversion,[],[f562])).
% 0.69/0.38 cnf(s57, plain, ~spl23_69 | ~spl23_71, inference(sat_conversion,[],[f568])).
% 0.69/0.38 cnf(s58, plain, spl23_69 | spl23_71, inference(sat_conversion,[],[f572])).
% 0.69/0.38 cnf(s60, plain, ~spl23_21 | spl23_66 | spl23_94, inference(sat_conversion,[],[f603])).
% 0.69/0.38 cnf(s61, plain, ~spl23_19 | ~spl23_22, inference(sat_conversion,[],[f606])).
% 0.69/0.38 cnf(s62, plain, spl23_19 | spl23_22, inference(sat_conversion,[],[f609])).
% 0.69/0.38 cnf(s63, plain, ~spl23_20 | spl23_66 | spl23_93, inference(sat_conversion,[],[f616])).
% 0.69/0.38 cnf(s64, plain, spl23_1 | ~spl23_46 | spl23_95, inference(sat_conversion,[],[f633])).
% 0.69/0.38 cnf(s65, plain, ~spl23_79 | spl23_96 | spl23_97, inference(sat_conversion,[],[f648])).
% 0.69/0.38 cnf(s66, plain, ~spl23_19 | ~spl23_91 | spl23_93, inference(sat_conversion,[],[f655])).
% 0.69/0.38 cnf(s69, plain, ~spl23_19 | ~spl23_90 | spl23_94, inference(sat_conversion,[],[f662])).
% 0.69/0.38 cnf(s70, plain, ~spl23_2 | ~spl23_57 | ~spl23_70 | ~spl23_71, inference(sat_conversion,[],[f675])).
% 0.69/0.38 cnf(s71, plain, ~spl23_2 | ~spl23_69 | spl23_95, inference(sat_conversion,[],[f679])).
% 0.69/0.38 cnf(s73, plain, ~spl23_5 | ~spl23_7, inference(sat_conversion,[],[f694])).
% 0.69/0.38 cnf(s74, plain, ~spl23_17 | ~spl23_37 | ~spl23_54 | ~spl23_55, inference(sat_conversion,[],[f710])).
% 0.69/0.38 cnf(s76, plain, ~spl23_37 | ~spl23_47 | ~spl23_53 | ~spl23_62, inference(sat_conversion,[],[f720])).
% 0.69/0.38 cnf(s77, plain, ~spl23_46 | ~spl23_48, inference(sat_conversion,[],[f723])).
% 0.69/0.38 cnf(s80, plain, ~spl23_39 | ~spl23_41 | ~spl23_43, inference(sat_conversion,[],[f744])).
% 0.69/0.38 cnf(s82, plain, ~spl23_21 | ~spl23_63 | ~spl23_66 | ~spl23_67, inference(sat_conversion,[],[f760])).
% 0.69/0.38 cnf(s83, plain, ~spl23_61 | ~spl23_65 | spl23_94, inference(sat_conversion,[],[f764])).
% 0.69/0.38 cnf(s84, plain, ~spl23_61 | ~spl23_67 | spl23_93, inference(sat_conversion,[],[f766])).
% 0.69/0.38 cnf(s85, plain, ~spl23_66 | ~spl23_68, inference(sat_conversion,[],[f769])).
% 0.69/0.38 cnf(s88, plain, ~spl23_35 | ~spl23_49 | ~spl23_59 | ~spl23_81, inference(sat_conversion,[],[f792])).
% 0.69/0.38 cnf(s90, plain, ~spl23_15 | ~spl23_57 | ~spl23_72 | ~spl23_85, inference(sat_conversion,[],[f802])).
% 0.69/0.38 cnf(s91, plain, ~spl23_16 | ~spl23_17, inference(sat_conversion,[],[f806])).
% 0.69/0.38 cnf(s92, plain, ~spl23_51 | ~spl23_77 | ~spl23_83 | ~spl23_86, inference(sat_conversion,[],[f811])).
% 0.69/0.38 cnf(s93, plain, ~spl23_49 | ~spl23_81 | ~spl23_84, inference(sat_conversion,[],[f815])).
% 0.69/0.38 cnf(s94, plain, ~spl23_50 | ~spl23_51 | ~spl23_77, inference(sat_conversion,[],[f819])).
% 0.69/0.38 cnf(s95, plain, spl23_82 | spl23_83, inference(sat_conversion,[],[f825])).
% 0.69/0.38 cnf(s96, plain, ~spl23_27 | ~spl23_29 | ~spl23_32, inference(sat_conversion,[],[f843])).
% 0.69/0.38 cnf(s101, plain, ~spl23_17 | ~spl23_45 | ~spl23_56 | ~spl23_62, inference(sat_conversion,[],[f877])).
% 0.69/0.38 cnf(s102, plain, ~spl23_38 | ~spl23_39, inference(sat_conversion,[],[f880])).
% 0.69/0.38 cnf(s106, plain, ~spl23_20 | ~spl23_22 | ~spl23_66 | ~spl23_90, inference(sat_conversion,[],[f912])).
% 0.69/0.38 cnf(s107, plain, ~spl23_11 | ~spl23_23 | ~spl23_25 | ~spl23_89, inference(sat_conversion,[],[f922])).
% 0.69/0.38 cnf(s108, plain, ~spl23_9 | ~spl23_12, inference(sat_conversion,[],[f925])).
% 0.69/0.38 cnf(s109, plain, ~spl23_26 | ~spl23_27, inference(sat_conversion,[],[f929])).
% 0.69/0.38 cnf(s110, plain, ~spl23_33 | ~spl23_50 | ~spl23_59 | ~spl23_77, inference(sat_conversion,[],[f945])).
% 0.69/0.38 cnf(s111, plain, ~spl23_78 | ~spl23_79, inference(sat_conversion,[],[f948])).
% 0.69/0.38 cnf(s115, plain, spl23_77 | spl23_80, inference(sat_conversion,[],[f965])).
% 0.69/0.38 cnf(s116, plain, ~spl23_52 | ~spl23_81 | ~spl23_84, inference(sat_conversion,[],[f979])).
% 0.69/0.38 cnf(s117, plain, ~spl23_82 | ~spl23_86 | ~spl23_87, inference(sat_conversion,[],[f986])).
% 0.69/0.38 cnf(s121, plain, ~spl23_76 | ~spl23_78 | ~spl23_80 | ~spl23_97, inference(sat_conversion,[],[f1026])).
% 0.69/0.38 cnf(s122, plain, ~spl23_34 | ~spl23_36, inference(sat_conversion,[],[f1036])).
% 0.69/0.38 cnf(s123, plain, ~spl23_15 | spl23_85 | spl23_98, inference(sat_conversion,[],[f1043])).
% 0.69/0.38 cnf(s125, plain, ~spl23_73 | ~spl23_76 | ~spl23_80, inference(sat_conversion,[],[f1066])).
% 0.69/0.38 cnf(s126, plain, ~spl23_50 | ~spl23_80 | ~spl23_82 | spl23_86, inference(sat_conversion,[],[f1071])).
% 0.69/0.38 cnf(s127, plain, ~spl23_35 | ~spl23_50 | ~spl23_59 | ~spl23_80, inference(sat_conversion,[],[f1079])).
% 0.69/0.38 cnf(s129, plain, ~spl23_52 | ~spl23_83 | spl23_84 | ~spl23_87, inference(sat_conversion,[],[f1094])).
% 0.69/0.38 cnf(s130, plain, ~spl23_50 | ~spl23_51 | ~spl23_80, inference(sat_conversion,[],[f1098])).
% 0.69/0.38 cnf(s133, plain, ~spl23_33 | ~spl23_59 | ~spl23_83 | ~spl23_86, inference(sat_conversion,[],[f1127])).
% 0.69/0.38 cnf(s134, plain, ~spl23_49 | ~spl23_51 | ~spl23_80 | ~spl23_81, inference(sat_conversion,[],[f1139])).
% 0.69/0.38 cnf(s135, plain, ~spl23_82 | ~spl23_83, inference(sat_conversion,[],[f1142])).
% 0.69/0.38 cnf(s136, plain, ~spl23_7 | ~spl23_23 | ~spl23_31 | ~spl23_89, inference(sat_conversion,[],[f1171])).
% 0.69/0.38 cnf(s137, plain, ~spl23_6 | ~spl23_8, inference(sat_conversion,[],[f1175])).
% 0.69/0.38 cnf(s138, plain, spl23_5 | spl23_31 | ~spl23_99, inference(sat_conversion,[],[f1182])).
% 0.69/0.38 cnf(s142, plain, ~spl23_5 | spl23_31 | spl23_99, inference(sat_conversion,[],[f1203])).
% 0.69/0.38 cnf(s143, plain, ~spl23_11 | spl23_25 | ~spl23_26 | ~spl23_32, inference(sat_conversion,[],[f1214])).
% 0.69/0.38 cnf(s146, plain, ~spl23_11 | ~spl23_24 | ~spl23_28 | ~spl23_89, inference(sat_conversion,[],[f1228])).
% 0.69/0.38 cnf(s147, plain, ~spl23_27 | ~spl23_29 | spl23_99, inference(sat_conversion,[],[f1234])).
% 0.69/0.38 cnf(s149, plain, ~spl23_95 | ~spl23_98, inference(sat_conversion,[],[f1247])).
% 0.69/0.38 cnf(s150, plain, spl23_34 | ~spl23_74 | ~spl23_78 | spl23_97, inference(sat_conversion,[],[f1250])).
% 0.69/0.38 cnf(s151, plain, ~spl23_77 | ~spl23_80, inference(sat_conversion,[],[f1253])).
% 0.69/0.38 cnf(s154, plain, spl23_34 | ~spl23_73 | ~spl23_75 | ~spl23_80, inference(sat_conversion,[],[f1277])).
% 0.69/0.38 cnf(s156, plain, ~spl23_5 | ~spl23_24 | ~spl23_31 | ~spl23_89, inference(sat_conversion,[],[f1299])).
% 0.69/0.38 cnf(s157, plain, spl23_9 | ~spl23_20 | ~spl23_42 | ~spl23_66, inference(sat_conversion,[],[f1303])).
% 0.69/0.38 cnf(s159, plain, ~spl23_38 | ~spl23_41 | ~spl23_45 | ~spl23_62, inference(sat_conversion,[],[f1310])).
% 0.69/0.38 cnf(s163, plain, ~spl23_15 | ~spl23_18, inference(sat_conversion,[],[f1339])).
% 0.69/0.38 cnf(s164, plain, ~spl23_37 | ~spl23_45 | ~spl23_55 | ~spl23_62, inference(sat_conversion,[],[f1343])).
% 0.69/0.38 cnf(s165, plain, ~spl23_1 | spl23_15 | ~spl23_48 | ~spl23_85, inference(sat_conversion,[],[f1347])).
% 0.69/0.38 cnf(s169, plain, spl23_38 | spl23_39, inference(sat_conversion,[],[f1367])).
% 0.69/0.38 cnf(s171, plain, ~spl23_10 | ~spl23_25 | ~spl23_99, inference(sat_conversion,[],[f1383])).
% 0.69/0.38 cnf(s173, plain, ~spl23_35 | ~spl23_51 | ~spl23_58 | ~spl23_80, inference(sat_conversion,[],[f1406])).
% 0.69/0.38 cnf(s174, plain, ~spl23_74 | ~spl23_75, inference(sat_conversion,[],[f1410])).
% 0.69/0.38 cnf(s176, plain, spl23_2 | ~spl23_69 | ~spl23_95, inference(sat_conversion,[],[f1421])).
% 0.69/0.38 cnf(s177, plain, ~spl23_3 | ~spl23_69 | spl23_98, inference(sat_conversion,[],[f1423])).
% 0.69/0.38 cnf(s178, plain, ~spl23_1 | ~spl23_4, inference(sat_conversion,[],[f1427])).
% 0.69/0.38 cnf(s179, plain, spl23_3 | ~spl23_69 | ~spl23_98, inference(sat_conversion,[],[f1428])).
% 0.69/0.38 cnf(s181, plain, ~spl23_37 | ~spl23_40 | ~spl23_55, inference(sat_conversion,[],[f1442])).
% 0.69/0.38 cnf(s182, plain, ~spl23_16 | ~spl23_39 | ~spl23_41 | ~spl23_54, inference(sat_conversion,[],[f1452])).
% 0.69/0.38 cnf(s183, plain, ~spl23_93 | ~spl23_94, inference(sat_conversion,[],[f1464])).
% 0.69/0.38 cnf(s184, plain, spl23_5 | ~spl23_30 | ~spl23_99, inference(sat_conversion,[],[f1465])).
% 0.69/0.38 cnf(s188, plain, spl23_66 | spl23_68, inference(sat_conversion,[],[f1492])).
% 0.69/0.38 cnf(s190, plain, ~spl23_20 | ~spl23_68 | spl23_93, inference(sat_conversion,[],[f1503])).
% 0.69/0.38 cnf(s191, plain, spl23_21 | ~spl23_68 | ~spl23_94, inference(sat_conversion,[],[f1505])).
% 0.69/0.38 cnf(s192, plain, ~spl23_23 | ~spl23_92 | spl23_99, inference(sat_conversion,[],[f1507])).
% 0.69/0.38 cnf(s194, plain, ~spl23_5 | ~spl23_30 | spl23_99, inference(sat_conversion,[],[f1514])).
% 0.69/0.38 cnf(s196, plain, ~spl23_10 | ~spl23_28 | spl23_99, inference(sat_conversion,[],[f1517])).
% 0.69/0.38 cnf(s200, plain, ~spl23_16 | ~spl23_47 | ~spl23_54 | ~spl23_64, inference(sat_conversion,[],[f1558])).
% 0.69/0.38 cnf(s201, plain, spl23_12 | ~spl23_42 | ~spl23_63 | ~spl23_65, inference(sat_conversion,[],[f1576])).
% 0.69/0.38 cnf(s202, plain, spl23_42 | spl23_44, inference(sat_conversion,[],[f1586])).
% 0.69/0.38 cnf(s204, plain, spl23_12 | ~spl23_44 | ~spl23_94, inference(sat_conversion,[],[f1591])).
% 0.69/0.38 cnf(s206, plain, ~spl23_22 | ~spl23_63 | ~spl23_65 | ~spl23_91, inference(sat_conversion,[],[f1601])).
% 0.69/0.38 cnf(s207, plain, spl23_37 | ~spl23_38 | ~spl23_41 | ~spl23_55, inference(sat_conversion,[],[f1610])).
% 0.69/0.38 cnf(s208, plain, ~spl23_16 | ~spl23_54 | ~spl23_56, inference(sat_conversion,[],[f1614])).
% 0.69/0.38 cnf(s209, plain, ~spl23_38 | ~spl23_41 | ~spl23_43, inference(sat_conversion,[],[f1625])).
% 0.69/0.38 cnf(s214, plain, ~spl23_49 | ~spl23_52, inference(sat_conversion,[],[f1661])).
% 0.69/0.38 cnf(s215, plain, spl23_1 | spl23_4, inference(sat_conversion,[],[f1670])).
% 0.69/0.38 cnf(s216, plain, spl23_15 | ~spl23_88 | ~spl23_98, inference(sat_conversion,[],[f1687])).
% 0.69/0.38 cnf(s217, plain, ~spl23_18 | ~spl23_88 | spl23_95, inference(sat_conversion,[],[f1689])).
% 0.69/0.38 cnf(s219, plain, spl23_18 | ~spl23_88 | ~spl23_95, inference(sat_conversion,[],[f1693])).
% 0.69/0.38 cnf(s221, plain, ~spl23_60 | ~spl23_70 | spl23_98, inference(sat_conversion,[],[f1716])).
% 0.69/0.38 cnf(s223, plain, ~spl23_2 | ~spl23_3 | ~spl23_71, inference(sat_conversion,[],[f1730])).
% 0.69/0.38 cnf(s224, plain, ~spl23_60 | ~spl23_72 | spl23_95, inference(sat_conversion,[],[f1732])).
% 0.69/0.38 cnf(s227, plain, ~spl23_1 | spl23_2 | ~spl23_46 | ~spl23_71, inference(sat_conversion,[],[f1755])).
% 0.69/0.38 cnf(s228, plain, ~spl23_24 | ~spl23_92 | ~spl23_99, inference(sat_conversion,[],[f1767])).
% 0.69/0.38 cnf(s229, plain, ~spl23_21 | ~spl23_68 | spl23_94, inference(sat_conversion,[],[f1774])).
% 0.69/0.38 cnf(s237, plain, ~spl23_7 | ~spl23_26 | ~spl23_29 | ~spl23_31, inference(sat_conversion,[],[f1842])).
% 0.69/0.38 cnf(s244, plain, ~spl23_27 | spl23_29 | ~spl23_99, inference(sat_conversion,[],[f1879])).
% 0.69/0.38 cnf(s246, plain, ~spl23_4 | spl23_48 | ~spl23_98, inference(sat_conversion,[],[f1886])).
% 0.69/0.38 cnf(s249, plain, ~spl23_16 | ~spl23_40 | ~spl23_53 | spl23_54, inference(sat_conversion,[],[f1921])).
% 0.69/0.38 cnf(s250, plain, ~spl23_16 | ~spl23_39 | spl23_41 | ~spl23_56, inference(sat_conversion,[],[f1936])).
% 0.69/0.38 cnf(s257, plain, ~spl23_37 | ~spl23_39 | spl23_41 | ~spl23_53, inference(sat_conversion,[],[f1985])).
% 0.69/0.38 cnf(s258, plain, ~spl23_37 | ~spl23_40 | ~spl23_53, inference(sat_conversion,[],[f1989])).
% 0.69/0.38 cnf(s261, plain, ~spl23_38 | spl23_41 | ~spl23_45 | ~spl23_64, inference(sat_conversion,[],[f2034])).
% 0.69/0.38 cnf(s264, plain, spl23_76 | ~spl23_77 | ~spl23_96, inference(sat_conversion,[],[f2063])).
% 0.69/0.38 cnf(s265, plain, ~spl23_49 | spl23_81 | ~spl23_82 | ~spl23_86, inference(sat_conversion,[],[f2070])).
% 0.69/0.38 cnf(s267, plain, ~spl23_34 | ~spl23_75 | spl23_78 | ~spl23_97, inference(sat_conversion,[],[f2105])).
% 0.69/0.38 cnf(s268, plain, ~spl23_73 | ~spl23_76 | ~spl23_77, inference(sat_conversion,[],[f2109])).
% 0.69/0.38 cnf(s269, plain, ~spl23_76 | ~spl23_77 | spl23_96, inference(sat_conversion,[],[f2110])).
% 0.69/0.38 cnf(s270, plain, spl23_36 | ~spl23_74 | ~spl23_96, inference(sat_conversion,[],[f2115])).
% 0.69/0.38 cnf(s273, plain, ~spl23_4 | ~spl23_48 | spl23_98, inference(sat_conversion,[],[f2138])).
% 0.69/0.38 cnf(s276, plain, ~spl23_50 | ~spl23_52 | ~spl23_77 | ~spl23_84, inference(sat_conversion,[],[f2155])).
% 0.69/0.38 cnf(s283, plain, spl23_9 | ~spl23_44 | ~spl23_93, inference(sat_conversion,[],[f2181])).
% 0.69/0.38 cnf(s297, plain, ~spl23_33 | ~spl23_51 | ~spl23_58 | ~spl23_77, inference(sat_conversion,[],[f2267])).
% 0.69/0.38 cnf(s298, plain, ~spl23_26 | ~spl23_10 | spl23_5, inference(rat,[],[s237,s17,s138,s184,s196,s16,s109,s4,s137,s3])).
% 0.69/0.38 cnf(s299, plain, spl23_66 | spl23_21 | ~spl23_22 | ~spl23_91, inference(rat,[],[s56,s206,s83,s191,s35,s188])).
% 0.69/0.38 cnf(s300, plain, spl23_37 | ~spl23_41 | ~spl23_16, inference(rat,[],[s208,s249,s30,s54,s22,s207,s102,s21])).
% 0.69/0.38 cnf(s301, plain, ~spl23_40 | ~spl23_37, inference(rat,[],[s54,s181,s258])).
% 0.69/0.38 cnf(s302, plain, ~spl23_82 | ~spl23_80 | ~spl23_50 | ~spl23_87, inference(rat,[],[s117,s126])).
% 0.69/0.38 cnf(s303, plain, spl23_82 | ~spl23_52 | ~spl23_87, inference(rat,[],[s116,s129,s43,s95])).
% 0.69/0.38 cnf(s304, plain, ~spl23_52 | ~spl23_50 | ~spl23_87, inference(rat,[],[s276,s115,s44,s302,s135,s303])).
% 0.69/0.38 cnf(s305, plain, ~spl23_51 | ~spl23_50, inference(rat,[],[s115,s94,s130])).
% 0.69/0.38 cnf(s306, plain, ~spl23_50 | ~spl23_87, inference(rat,[],[s305,s28,s304])).
% 0.69/0.38 cnf(s307, plain, ~spl23_76 | ~spl23_77 | spl23_36, inference(rat,[],[s39,s270,s268,s269])).
% 0.69/0.38 cnf(s308, plain, spl23_33 | ~spl23_51 | ~spl23_58, inference(rat,[],[s65,s267,s264,s40,s307,s111,s42,s115,s173,s122,s19,s51])).
% 0.69/0.38 cnf(s309, plain, ~spl23_76 | spl23_34 | ~spl23_78 | ~spl23_80, inference(rat,[],[s150,s39,s121,s125])).
% 0.69/0.38 cnf(s310, plain, spl23_34 | ~spl23_80 | ~spl23_78, inference(rat,[],[s39,s154,s174,s40,s309])).
% 0.69/0.38 cnf(s311, plain, ~spl23_33 | ~spl23_51 | ~spl23_58, inference(rat,[],[s310,s122,s20,s41,s115,s50,s297])).
% 0.69/0.38 cnf(s312, plain, ~spl23_51 | ~spl23_58, inference(rat,[],[s311,s308])).
% 0.69/0.38 cnf(s313, plain, ~spl23_98 | spl23_15 | spl23_3 | ~spl23_2, inference(rat,[],[s312,s28,s214,s27,s306,s31,s70,s46,s37,s58,s216,s179])).
% 0.69/0.38 cnf(s314, plain, ~spl23_41 | ~spl23_20 | ~spl23_47 | ~spl23_16 | spl23_9, inference(rat,[],[s84,s36,s33,s190,s76,s283,s29,s24,s182,s80,s22,s301,s300])).
% 0.69/0.38 cnf(s315, plain, spl23_19 | ~spl23_47 | ~spl23_16 | ~spl23_91 | spl23_9, inference(rat,[],[s229,s183,s299,s63,s188,s157,s23,s314,s11,s62])).
% 0.69/0.38 cnf(s316, plain, ~spl23_47 | ~spl23_16 | spl23_9 | ~spl23_91, inference(rat,[],[s250,s80,s22,s30,s249,s53,s29,s200,s34,s82,s36,s60,s229,s24,s12,s283,s183,s61,s66,s315])).
% 0.69/0.38 cnf(s317, plain, spl23_15 | ~spl23_91 | spl23_9 | spl23_3 | spl23_1, inference(rat,[],[s316,s26,s273,s313,s9,s215,s1])).
% 0.69/0.38 cnf(s318, plain, ~spl23_62 | ~spl23_41 | ~spl23_45 | ~spl23_17, inference(rat,[],[s164,s21,s30,s159,s101])).
% 0.69/0.38 cnf(s319, plain, spl23_93 | ~spl23_20 | ~spl23_61, inference(rat,[],[s36,s84,s190])).
% 0.69/0.38 cnf(s320, plain, ~spl23_20 | ~spl23_61 | spl23_9, inference(rat,[],[s157,s35,s202,s83,s283,s183,s319])).
% 0.69/0.38 cnf(s321, plain, ~spl23_43 | ~spl23_41, inference(rat,[],[s169,s80,s209])).
% 0.69/0.38 cnf(s322, plain, ~spl23_41 | ~spl23_45 | ~spl23_17 | ~spl23_91 | spl23_9, inference(rat,[],[s321,s24,s283,s66,s11,s320,s33,s318])).
% 0.69/0.38 cnf(s323, plain, spl23_93 | ~spl23_42 | ~spl23_91 | spl23_9, inference(rat,[],[s63,s157,s11,s66])).
% 0.69/0.38 cnf(s324, plain, spl23_19 | ~spl23_42 | ~spl23_91 | spl23_9, inference(rat,[],[s60,s299,s157,s11,s62,s183,s323])).
% 0.69/0.38 cnf(s325, plain, ~spl23_45 | spl23_9 | ~spl23_17 | ~spl23_91, inference(rat,[],[s74,s29,s54,s257,s21,s169,s261,s34,s82,s36,s60,s229,s12,s61,s324,s183,s323,s23,s322])).
% 0.69/0.38 cnf(s326, plain, spl23_9 | spl23_5 | spl23_3 | spl23_1, inference(rat,[],[s37,s70,s57,s38,s90,s31,s312,s28,s214,s27,s306,s46,s123,s219,s246,s64,s77,s25,s325,s10,s163,s317,s48,s192,s171,s15,s298,s5,s215,s1,s13,s49,s7,s137,s3])).
% 0.69/0.38 cnf(s327, plain, spl23_25 | ~spl23_32 | ~spl23_11, inference(rat,[],[s15,s143])).
% 0.69/0.38 cnf(s328, plain, ~spl23_89 | ~spl23_11 | ~spl23_23 | ~spl23_7, inference(rat,[],[s327,s18,s107,s136])).
% 0.69/0.38 cnf(s329, plain, spl23_15 | ~spl23_62 | ~spl23_41 | spl23_3 | spl23_1, inference(rat,[],[s29,s182,s76,s22,s26,s301,s273,s300,s313,s9,s215,s1])).
% 0.69/0.38 cnf(s330, plain, ~spl23_41 | spl23_5 | spl23_3 | spl23_1, inference(rat,[],[s37,s70,s57,s38,s90,s31,s312,s28,s214,s27,s306,s46,s123,s219,s246,s64,s77,s25,s318,s10,s163,s329,s33,s83,s35,s106,s11,s62,s69,s204,s24,s321,s215,s1,s47,s328,s6,s108,s326,s13,s49,s7,s4,s137,s3])).
% 0.69/0.38 cnf(s331, plain, spl23_19 | ~spl23_42 | ~spl23_90 | spl23_12, inference(rat,[],[s56,s201,s83,s183,s35,s63,s106,s11,s62])).
% 0.69/0.38 cnf(s333, plain, ~spl23_66 | spl23_93 | ~spl23_21, inference(rat,[],[s56,s82,s84,s36,s85])).
% 0.69/0.38 cnf(s334, plain, spl23_15 | spl23_5 | spl23_3 | spl23_1, inference(rat,[],[s250,s22,s30,s249,s53,s29,s200,s26,s273,s313,s9,s215,s1,s34,s201,s35,s333,s183,s69,s12,s61,s331,s47,s328,s6,s13,s49,s7,s4,s137,s3,s108,s326,s23,s330])).
% 0.69/0.38 cnf(s335, plain, spl23_38 | ~spl23_17 | spl23_41, inference(rat,[],[s74,s29,s54,s257,s21,s169])).
% 0.69/0.38 cnf(s336, plain, spl23_5 | spl23_3 | spl23_1, inference(rat,[],[s37,s70,s57,s38,s90,s31,s312,s28,s214,s27,s306,s46,s123,s219,s246,s64,s77,s25,s261,s335,s10,s163,s334,s34,s201,s35,s333,s183,s12,s69,s61,s331,s23,s330,s47,s328,s6,s108,s326,s13,s49,s4,s7,s137,s3,s215,s1])).
% 0.69/0.38 cnf(s337, plain, spl23_19 | ~spl23_47 | ~spl23_61 | ~spl23_16 | ~spl23_41 | ~spl23_5, inference(rat,[],[s96,s244,s16,s142,s18,s146,s156,s47,s106,s35,s83,s6,s183,s108,s319,s314,s11,s62,s14,s49,s8,s137,s4,s73])).
% 0.69/0.38 cnf(s338, plain, spl23_9 | spl23_15 | spl23_3 | spl23_1, inference(rat,[],[s147,s17,s16,s194,s196,s228,s48,s317,s5,s14,s49,s8,s137,s4,s73,s336])).
% 0.69/0.38 cnf(s339, plain, spl23_15 | ~spl23_41 | spl23_3 | spl23_1, inference(rat,[],[s244,s96,s16,s142,s18,s146,s156,s47,s69,s204,s6,s108,s338,s337,s26,s33,s273,s329,s313,s9,s215,s1,s14,s49,s8,s137,s4,s73,s336,s24,s321])).
% 0.69/0.38 cnf(s340, plain, ~spl23_46 | ~spl23_15 | spl23_1, inference(rat,[],[s37,s70,s57,s38,s90,s31,s312,s28,s214,s27,s306,s46,s123,s219,s246,s64,s77,s215,s1,s163])).
% 0.69/0.38 cnf(s341, plain, spl23_9 | ~spl23_45 | ~spl23_17 | ~spl23_5, inference(rat,[],[s147,s17,s16,s194,s196,s228,s48,s325,s5,s14,s49,s8,s137,s4,s73])).
% 0.69/0.38 cnf(s342, plain, ~spl23_89 | ~spl23_11 | ~spl23_5, inference(rat,[],[s96,s244,s16,s142,s18,s146,s156,s14,s49,s8,s137,s4,s73])).
% 0.69/0.38 cnf(s343, plain, ~spl23_41 | spl23_3 | spl23_1, inference(rat,[],[s106,s11,s62,s69,s47,s342,s35,s83,s204,s6,s108,s341,s33,s318,s25,s340,s10,s163,s339,s24,s321,s336])).
% 0.69/0.38 cnf(s344, plain, spl23_15 | spl23_3 | spl23_1, inference(rat,[],[s250,s22,s30,s249,s53,s29,s200,s34,s201,s35,s333,s183,s12,s69,s61,s331,s47,s342,s6,s26,s108,s273,s338,s313,s9,s215,s1,s336,s23,s343])).
% 0.69/0.38 cnf(s345, plain, spl23_3 | spl23_1, inference(rat,[],[s12,s82,s61,s36,s331,s85,s47,s35,s342,s201,s6,s34,s108,s261,s341,s335,s25,s10,s340,s163,s344,s23,s343,s336])).
% 0.69/0.38 cnf(s346, plain, ~spl23_3 | ~spl23_2, inference(rat,[],[s149,s177,s71,s58,s223])).
% 0.69/0.38 cnf(s347, plain, spl23_1, inference(rat,[],[s346,s345,s1])).
% 0.69/0.38 cnf(s348, plain, ~spl23_4, inference(rat,[],[s178,s347])).
% 0.69/0.38 cnf(s349, plain, spl23_3, inference(rat,[],[s2,s348])).
% 0.69/0.38 cnf(s350, plain, ~spl23_2, inference(rat,[],[s346,s349])).
% 0.69/0.38 cnf(s351, plain, ~spl23_87 | ~spl23_86, inference(rat,[],[s115,s134,s92,s28,s303,s43,s95,s27,s117,s306])).
% 0.69/0.38 cnf(s352, plain, ~spl23_80 | ~spl23_50 | ~spl23_59, inference(rat,[],[s122,s310,s20,s41,s127,s151])).
% 0.69/0.38 cnf(s353, plain, ~spl23_50 | ~spl23_59, inference(rat,[],[s65,s267,s264,s40,s307,s122,s19,s111,s110,s42,s115,s352])).
% 0.69/0.38 cnf(s354, plain, spl23_81 | ~spl23_49 | ~spl23_86, inference(rat,[],[s265,s43])).
% 0.69/0.38 cnf(s355, plain, ~spl23_86 | spl23_15, inference(rat,[],[s133,s51,s44,s88,s93,s354,s27,s353,s32,s221,s37,s176,s216,s217,s46,s351,s10,s91,s9,s350])).
% 0.69/0.38 cnf(s356, plain, spl23_5 | ~spl23_92 | ~spl23_10, inference(rat,[],[s13,s192,s49,s171,s7,s15,s137,s298,s3])).
% 0.69/0.38 cnf(s357, plain, ~spl23_92 | ~spl23_10, inference(rat,[],[s147,s17,s16,s194,s196,s228,s14,s49,s8,s137,s4,s73,s356])).
% 0.69/0.38 cnf(s358, plain, spl23_9 | spl23_15, inference(rat,[],[s357,s48,s316,s5,s9,s26,s165,s45,s355,s347])).
% 0.69/0.38 cnf(s359, plain, ~spl23_41 | ~spl23_90 | spl23_15, inference(rat,[],[s83,s33,s35,s76,s106,s29,s11,s62,s182,s69,s22,s204,s301,s24,s300,s321,s9,s26,s165,s45,s355,s108,s358,s347])).
% 0.69/0.38 cnf(s360, plain, ~spl23_90 | spl23_15, inference(rat,[],[s250,s22,s30,s249,s53,s29,s200,s34,s201,s35,s333,s183,s12,s69,s61,s331,s23,s359,s9,s26,s165,s45,s355,s108,s358,s347])).
% 0.69/0.38 cnf(s361, plain, ~spl23_89 | ~spl23_11, inference(rat,[],[s13,s328,s49,s4,s7,s137,s3,s342])).
% 0.69/0.38 cnf(s362, plain, spl23_15, inference(rat,[],[s361,s47,s360,s6,s108,s358])).
% 0.69/0.38 cnf(s363, plain, ~spl23_18, inference(rat,[],[s163,s362])).
% 0.69/0.38 cnf(s364, plain, spl23_17, inference(rat,[],[s10,s363])).
% 0.69/0.38 cnf(s366, plain, ~spl23_72 | spl23_95, inference(rat,[],[s133,s51,s44,s88,s93,s354,s45,s90,s31,s312,s28,s214,s27,s353,s32,s224,s362])).
% 0.69/0.38 cnf(s367, plain, spl23_71, inference(rat,[],[s366,s176,s38,s58,s350])).
% 0.69/0.38 cnf(s369, plain, ~spl23_46, inference(rat,[],[s227,s347,s350,s367])).
% 0.69/0.38 cnf(s372, plain, spl23_45, inference(rat,[],[s25,s369])).
% 0.69/0.38 cnf(s374, plain, spl23_9, inference(rat,[],[s48,s357,s325,s5,s364,s372])).
% 0.69/0.38 cnf(s375, plain, ~spl23_12, inference(rat,[],[s108,s374])).
% 0.69/0.38 cnf(s376, plain, spl23_11, inference(rat,[],[s6,s375])).
% 0.69/0.38 cnf(s378, plain, ~spl23_89, inference(rat,[],[s361,s376])).
% 0.69/0.38 cnf(s380, plain, spl23_90, inference(rat,[],[s47,s378])).
% 0.69/0.38 cnf(s381, plain, spl23_94 | ~spl23_61, inference(rat,[],[s106,s11,s62,s69,s35,s83,s380])).
% 0.69/0.38 cnf(s382, plain, ~spl23_41, inference(rat,[],[s381,s204,s33,s318,s24,s321,s375,s372,s364])).
% 0.69/0.38 cnf(s383, plain, spl23_42, inference(rat,[],[s23,s382])).
% 0.69/0.38 cnf(s384, plain, spl23_38, inference(rat,[],[s335,s364,s382])).
% 0.69/0.38 cnf(s386, plain, spl23_19, inference(rat,[],[s331,s375,s380,s383])).
% 0.69/0.38 cnf(s389, plain, ~spl23_64, inference(rat,[],[s261,s372,s382,s384])).
% 0.69/0.38 cnf(s391, plain, ~spl23_22, inference(rat,[],[s61,s386])).
% 0.69/0.38 cnf(s392, plain, spl23_94, inference(rat,[],[s69,s380,s386])).
% 0.69/0.38 cnf(s395, plain, spl23_63, inference(rat,[],[s34,s389])).
% 0.69/0.38 cnf(s396, plain, spl23_21, inference(rat,[],[s12,s391])).
% 0.69/0.38 cnf(s397, plain, ~spl23_93, inference(rat,[],[s183,s392])).
% 0.69/0.38 cnf(s401, plain, ~spl23_65, inference(rat,[],[s201,s383,s375,s395])).
% 0.69/0.38 cnf(s403, plain, ~spl23_66, inference(rat,[],[s333,s397,s396])).
% 0.69/0.38 cnf(s407, plain, $false, inference(rat,[],[s35,s403,s401])).
% 0.69/0.38 thf(f2268,plain,(
% 0.69/0.38 $false),
% 0.69/0.38 inference(avatar_sat_refutation,[],[s407])).
% 0.69/0.38 % SZS output end Proof for theBenchmark
% 0.69/0.38 % (2784558)------------------------------
% 0.69/0.38 % (2784558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.69/0.38 % (2784558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.69/0.38 % (2784558)CaDiCaL version: 2.1.3
% 0.69/0.38 % (2784558)Termination reason: Refutation
% 0.69/0.38 % (2784558)Time elapsed: 0.064 s
% 0.69/0.38 % (2784558)Peak memory usage: 13 MB
% 0.69/0.38 % (2784558)Instructions burned: 108 (million)
% 0.69/0.38 % (2784547)Success in time 0.109 s
% 0.69/0.38 % Vampire exiting
%------------------------------------------------------------------------------