%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500^1.007 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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.72s 0.44s
% Output : Refutation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.007 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n026.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 17:13:57 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.27 Running higher-order theorem proving
% 0.23/0.29 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.40 % (886984)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.23/0.40 % (886990)lrs+10_16_si=on:nwc=1.5:random_seed=3300225211:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.23/0.40 % (886990)Refutation not found, incomplete strategy
% 0.23/0.40 % (886990)------------------------------
% 0.23/0.40 % (886990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.40 % (886990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.40 % (886990)CaDiCaL version: 2.1.3
% 0.23/0.40 % (886990)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.40 % (886990)Time elapsed: 0.001 s
% 0.23/0.40 % (886990)Peak memory usage: 12 MB
% 0.23/0.40 % (886990)Instructions burned: 2 (million)
% 0.23/0.40 % (886990)------------------------------
% 0.23/0.40 % (886990)------------------------------
% 0.23/0.40 % (886995)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.23/0.40 % (886995)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.23/0.40 % (886989)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3901062554:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.23/0.40 % (886993)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3628626562:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.23/0.40 % (886992)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=296142612: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.23/0.40 % (886991)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1982852711:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.23/0.40 % (886995)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=682028997:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.23/0.40 % (886994)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2781353513:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.23/0.40 % (886989)Refutation not found, incomplete strategy
% 0.23/0.40 % (886989)------------------------------
% 0.23/0.40 % (886989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.40 % (886989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.40 % (886989)CaDiCaL version: 2.1.3
% 0.23/0.40 % (886989)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.40 % (886989)Time elapsed: 0.002 s
% 0.23/0.40 % (886989)Peak memory usage: 12 MB
% 0.23/0.40 % (886989)Instructions burned: 2 (million)
% 0.23/0.40 % (886991)Refutation not found, incomplete strategy
% 0.23/0.40 % (886991)------------------------------
% 0.23/0.40 % (886991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.40 % (886991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.40 % (886991)CaDiCaL version: 2.1.3
% 0.23/0.40 % (886991)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.40 % (886991)Time elapsed: 0.001 s
% 0.23/0.40 % (886991)Peak memory usage: 12 MB
% 0.23/0.40 % (886991)Instructions burned: 1 (million)
% 0.23/0.40 % (886993)Refutation not found, incomplete strategy
% 0.23/0.40 % (886993)------------------------------
% 0.23/0.40 % (886993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.40 % (886993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.40 % (886993)CaDiCaL version: 2.1.3
% 0.23/0.40 % (886993)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.40 % (886993)Time elapsed: 0.002 s
% 0.23/0.40 % (886993)Peak memory usage: 12 MB
% 0.23/0.40 % (886993)Instructions burned: 4 (million)
% 0.23/0.40 % (886989)------------------------------
% 0.23/0.40 % (886989)------------------------------
% 0.23/0.40 % (886991)------------------------------
% 0.23/0.40 % (886991)------------------------------
% 0.23/0.40 % (886993)------------------------------
% 0.23/0.40 % (886993)------------------------------
% 0.23/0.40 % (886999)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2809952965:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.43 % (886999)Instruction limit reached!
% 0.72/0.43 % (886999)------------------------------
% 0.72/0.43 % (886999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.43 % (886999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.43 % (886999)CaDiCaL version: 2.1.3
% 0.72/0.43 % (886999)Termination reason: Instruction limit
% 0.72/0.43 % (886999)Termination phase: Saturation
% 0.72/0.43 % (886999)Time elapsed: 0.001 s
% 0.72/0.43 % (886999)Peak memory usage: 12 MB
% 0.72/0.43 % (886999)Instructions burned: 3 (million)
% 0.72/0.43 % (887011)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.72/0.43 % (887011)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.43 % (887008)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.43 % (887011)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2084313729: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.72/0.43 % (887008)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2702686868:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.72/0.43 % (887009)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2544387769:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.72/0.43 % (887007)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2587187110:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.72/0.43 % (887008)Instruction limit reached!
% 0.72/0.43 % (887008)------------------------------
% 0.72/0.43 % (887008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887008)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887008)Termination reason: Instruction limit
% 0.72/0.44 % (887008)Termination phase: Saturation
% 0.72/0.44 % (887008)Time elapsed: 0.004 s
% 0.72/0.44 % (887008)Peak memory usage: 12 MB
% 0.72/0.44 % (887008)Instructions burned: 9 (million)
% 0.72/0.44 % (887011)Instruction limit reached!
% 0.72/0.44 % (887011)------------------------------
% 0.72/0.44 % (887011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887011)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887011)Termination reason: Instruction limit
% 0.72/0.44 % (887011)Termination phase: Saturation
% 0.72/0.44 % (887011)Time elapsed: 0.008 s
% 0.72/0.44 % (887011)Peak memory usage: 12 MB
% 0.72/0.44 % (887011)Instructions burned: 31 (million)
% 0.72/0.44 % (887007)Instruction limit reached!
% 0.72/0.44 % (887007)------------------------------
% 0.72/0.44 % (887007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887007)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887007)Termination reason: Instruction limit
% 0.72/0.44 % (887007)Termination phase: Saturation
% 0.72/0.44 % (887007)Time elapsed: 0.005 s
% 0.72/0.44 % (887007)Peak memory usage: 12 MB
% 0.72/0.44 % (887007)Instructions burned: 6 (million)
% 0.72/0.44 % (887009)Instruction limit reached!
% 0.72/0.44 % (887009)------------------------------
% 0.72/0.44 % (887009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887009)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887009)Termination reason: Instruction limit
% 0.72/0.44 % (887009)Termination phase: Saturation
% 0.72/0.44 % (887009)Time elapsed: 0.009 s
% 0.72/0.44 % (887009)Peak memory usage: 12 MB
% 0.72/0.44 % (887009)Instructions burned: 19 (million)
% 0.72/0.44 % (886994)Instruction limit reached!
% 0.72/0.44 % (886994)------------------------------
% 0.72/0.44 % (886994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (886994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (886994)CaDiCaL version: 2.1.3
% 0.72/0.44 % (886994)Termination reason: Instruction limit
% 0.72/0.44 % (886994)Termination phase: Saturation
% 0.72/0.44 % (886994)Time elapsed: 0.035 s
% 0.72/0.44 % (886994)Peak memory usage: 12 MB
% 0.72/0.44 % (886994)Instructions burned: 77 (million)
% 0.72/0.44 % (887016)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=2614620975:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.72/0.44 % (887016)Refutation not found, incomplete strategy
% 0.72/0.44 % (887016)------------------------------
% 0.72/0.44 % (887016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887016)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887016)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887016)Time elapsed: 0.001 s
% 0.72/0.44 % (887016)Peak memory usage: 12 MB
% 0.72/0.44 % (887016)Instructions burned: 6 (million)
% 0.72/0.44 % (887016)------------------------------
% 0.72/0.44 % (887016)------------------------------
% 0.72/0.44 % (887018)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.72/0.44 % (887017)lrs+10_1_si=on:cs=on:random_seed=1179482411:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.72/0.44 % (887018)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=468488194:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.44 % (887022)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1207810680:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.72/0.44 % (887017)Instruction limit reached!
% 0.72/0.44 % (887017)------------------------------
% 0.72/0.44 % (887017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887017)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887017)Termination reason: Instruction limit
% 0.72/0.44 % (887017)Termination phase: Saturation
% 0.72/0.44 % (887017)Time elapsed: 0.004 s
% 0.72/0.44 % (887017)Peak memory usage: 11 MB
% 0.72/0.44 % (887017)Instructions burned: 9 (million)
% 0.72/0.44 % (887019)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1078067093:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.72/0.44 % (887022)Refutation not found, incomplete strategy
% 0.72/0.44 % (887022)------------------------------
% 0.72/0.44 % (887022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887022)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887022)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887022)Time elapsed: 0.001 s
% 0.72/0.44 % (887022)Peak memory usage: 12 MB
% 0.72/0.44 % (887022)Instructions burned: 3 (million)
% 0.72/0.44 % (887022)------------------------------
% 0.72/0.44 % (887022)------------------------------
% 0.72/0.44 % (887018)Refutation not found, incomplete strategy
% 0.72/0.44 % (887018)------------------------------
% 0.72/0.44 % (887018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887018)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887018)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887018)Time elapsed: 0.003 s
% 0.72/0.44 % (887018)Peak memory usage: 12 MB
% 0.72/0.44 % (887018)Instructions burned: 5 (million)
% 0.72/0.44 % (887018)------------------------------
% 0.72/0.44 % (887018)------------------------------
% 0.72/0.44 % (887019)Refutation not found, incomplete strategy
% 0.72/0.44 % (887019)------------------------------
% 0.72/0.44 % (887019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887019)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887019)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887019)Time elapsed: 0.003 s
% 0.72/0.44 % (887019)Peak memory usage: 12 MB
% 0.72/0.44 % (887019)Instructions burned: 3 (million)
% 0.72/0.44 % (887019)------------------------------
% 0.72/0.44 % (887019)------------------------------
% 0.72/0.44 % (887021)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1481660564:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.72/0.44 % (887027)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=86375230:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.72/0.44 % (887027)Refutation not found, incomplete strategy
% 0.72/0.44 % (887027)------------------------------
% 0.72/0.44 % (887027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887027)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887027)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887027)Time elapsed: 0.001 s
% 0.72/0.44 % (887027)Peak memory usage: 12 MB
% 0.72/0.44 % (887027)Instructions burned: 2 (million)
% 0.72/0.44 % (887027)------------------------------
% 0.72/0.44 % (887027)------------------------------
% 0.72/0.44 % (887028)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1712177677:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.72/0.44 % (887029)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2638722104:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.72/0.44 % (887030)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3863904000:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.72/0.44 % (887033)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3665833220:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.72/0.44 % (887033)Refutation not found, incomplete strategy
% 0.72/0.44 % (887033)------------------------------
% 0.72/0.44 % (887033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887033)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887033)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887033)Time elapsed: 0.001 s
% 0.72/0.44 % (887033)Peak memory usage: 12 MB
% 0.72/0.44 % (887033)Instructions burned: 2 (million)
% 0.72/0.44 % (887033)------------------------------
% 0.72/0.44 % (887033)------------------------------
% 0.72/0.44 % (887030)Instruction limit reached!
% 0.72/0.44 % (887030)------------------------------
% 0.72/0.44 % (887030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887030)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887030)Termination reason: Instruction limit
% 0.72/0.44 % (887030)Termination phase: Saturation
% 0.72/0.44 % (887030)Time elapsed: 0.001 s
% 0.72/0.44 % (887030)Peak memory usage: 11 MB
% 0.72/0.44 % (887030)Instructions burned: 2 (million)
% 0.72/0.44 % (886995) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-886984-886995"...
% 0.72/0.44 % (887029)Instruction limit reached!
% 0.72/0.44 % (887029)------------------------------
% 0.72/0.44 % (887029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887029)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887029)Termination reason: Instruction limit
% 0.72/0.44 % (887029)Termination phase: Saturation
% 0.72/0.44 % (887029)Time elapsed: 0.007 s
% 0.72/0.44 % (887029)Peak memory usage: 12 MB
% 0.72/0.44 % (887029)Instructions burned: 14 (million)
% 0.72/0.44 % (887038)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=4006540463:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.72/0.44 % (887038)Refutation not found, incomplete strategy
% 0.72/0.44 % (887038)------------------------------
% 0.72/0.44 % (887038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (887038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (887038)CaDiCaL version: 2.1.3
% 0.72/0.44 % (887038)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.44 % (887038)Time elapsed: 0.0000 s
% 0.72/0.44 % (887038)Peak memory usage: 11 MB
% 0.72/0.44 % (887038)Instructions burned: 1 (million)
% 0.72/0.44 % (887038)------------------------------
% 0.72/0.44 % (887038)------------------------------
% 0.72/0.44 % (886995)...printing done.
% 0.72/0.44 % (886995)Refutation found. Thanks to Tanya!
% 0.72/0.44 % SZS status Theorem for theBenchmark
% 0.72/0.44 % SZS output start Proof for theBenchmark
% 0.72/0.44 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.72/0.44 thf(func_def_0, type, x: $o).
% 0.72/0.44 thf(func_def_1, type, f0: ($o > $o)).
% 0.72/0.44 thf(func_def_2, type, f1: ($o > $o)).
% 0.72/0.44 thf(func_def_3, type, f2: ($o > $o)).
% 0.72/0.44 thf(func_def_4, type, f3: ($o > $o)).
% 0.72/0.44 thf(func_def_5, type, f4: ($o > $o)).
% 0.72/0.44 thf(func_def_6, type, f5: ($o > $o)).
% 0.72/0.44 thf(func_def_7, type, f6: ($o > $o)).
% 0.72/0.44 thf(func_def_11, type, sF0: $o).
% 0.72/0.44 thf(func_def_12, type, sF1: $o).
% 0.72/0.44 thf(func_def_13, type, sF2: $o).
% 0.72/0.44 thf(func_def_14, type, sF3: $o).
% 0.72/0.44 thf(func_def_15, type, sF4: $o).
% 0.72/0.44 thf(func_def_16, type, sF5: $o).
% 0.72/0.44 thf(func_def_17, type, sF6: $o).
% 0.72/0.44 thf(func_def_18, type, sF7: $o).
% 0.72/0.44 thf(func_def_19, type, sF8: $o).
% 0.72/0.44 thf(func_def_20, type, sF9: $o).
% 0.72/0.44 thf(func_def_21, type, sF10: $o).
% 0.72/0.44 thf(func_def_22, type, sF11: $o).
% 0.72/0.44 thf(func_def_23, type, sF12: $o).
% 0.72/0.44 thf(func_def_24, type, sF13: $o).
% 0.72/0.44 thf(func_def_25, type, sF14: $o).
% 0.72/0.44 thf(func_def_26, type, sF15: $o).
% 0.72/0.44 thf(func_def_27, type, sF16: $o).
% 0.72/0.44 thf(func_def_28, type, sF17: $o).
% 0.72/0.44 thf(func_def_29, type, sF18: $o).
% 0.72/0.44 thf(func_def_30, type, sF19: $o).
% 0.72/0.44 thf(func_def_31, type, sF20: $o).
% 0.72/0.44 thf(func_def_32, type, sF21: $o).
% 0.72/0.44 thf(func_def_33, type, sF22: $o).
% 0.72/0.44 thf(func_def_34, type, sF23: $o).
% 0.72/0.44 thf(func_def_35, type, sF24: $o).
% 0.72/0.44 thf(func_def_36, type, sF25: $o).
% 0.72/0.44 thf(func_def_37, type, sF26: $o).
% 0.72/0.44 thf(f1,conjecture,(
% 0.72/0.44 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 0.72/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski7)).
% 0.72/0.44 thf(f2,negated_conjecture,(
% 0.72/0.44 ~ (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 0.72/0.44 inference(negated_conjecture,[status(cth)],[f1])).
% 0.72/0.44 thf(f3,plain,(
% 0.72/0.44 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 0.72/0.44 inference(flattening,[],[f2])).
% 0.72/0.44 thf(f4,plain,(
% 0.72/0.44 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ x)))))))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ x)))))))))))))))))),
% 0.72/0.44 inference(cnf_transformation,[],[f3])).
% 0.72/0.44 thf(f6,definition,(
% 0.72/0.44 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.72/0.44 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.72/0.44 thf(f7,definition,(
% 0.72/0.44 (sF0 = ((f6 @ x)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.72/0.44 thf(f8,plain,(
% 0.72/0.44 (((f6 @ x)) = sF0)),
% 0.72/0.44 inference(reorient_equations,[],[f7])).
% 0.72/0.44 thf(f9,definition,(
% 0.72/0.44 (sF1 = ((f5 @ sF0)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.72/0.44 thf(f10,plain,(
% 0.72/0.44 (((f5 @ sF0)) = sF1)),
% 0.72/0.44 inference(reorient_equations,[],[f9])).
% 0.72/0.44 thf(f11,definition,(
% 0.72/0.44 (sF2 = ((f5 @ sF1)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.72/0.44 thf(f12,plain,(
% 0.72/0.44 (((f5 @ sF1)) = sF2)),
% 0.72/0.44 inference(reorient_equations,[],[f11])).
% 0.72/0.44 thf(f13,definition,(
% 0.72/0.44 (sF3 = ((f5 @ sF2)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.72/0.44 thf(f14,plain,(
% 0.72/0.44 (((f5 @ sF2)) = sF3)),
% 0.72/0.44 inference(reorient_equations,[],[f13])).
% 0.72/0.44 thf(f15,definition,(
% 0.72/0.44 (sF4 = ((f4 @ sF3)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.72/0.44 thf(f16,definition,(
% 0.72/0.44 (sF5 = ((f3 @ sF4)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 0.72/0.44 thf(f17,definition,(
% 0.72/0.44 (sF6 = ((f3 @ sF5)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.72/0.44 thf(f18,definition,(
% 0.72/0.44 (sF7 = ((f3 @ sF6)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 0.72/0.44 thf(f19,definition,(
% 0.72/0.44 (sF8 = ((f2 @ sF7)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 0.72/0.44 thf(f20,plain,(
% 0.72/0.44 (((f2 @ sF7)) = sF8)),
% 0.72/0.44 inference(reorient_equations,[],[f19])).
% 0.72/0.44 thf(f21,definition,(
% 0.72/0.44 (sF9 = ((f1 @ sF8)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.72/0.44 thf(f22,definition,(
% 0.72/0.44 (sF10 = ((f1 @ sF9)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.72/0.44 thf(f23,definition,(
% 0.72/0.44 (sF11 = ((f1 @ sF10)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 0.72/0.44 thf(f24,definition,(
% 0.72/0.44 (sF12 = ((f0 @ sF11)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.72/0.44 thf(f25,definition,(
% 0.72/0.44 (sF13 = ((f6 @ sF0)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.72/0.44 thf(f26,definition,(
% 0.72/0.44 (sF14 = ((f6 @ sF13)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.72/0.44 thf(f27,definition,(
% 0.72/0.44 (sF15 = ((f5 @ sF14)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 0.72/0.44 thf(f28,plain,(
% 0.72/0.44 (((f5 @ sF14)) = sF15)),
% 0.72/0.44 inference(reorient_equations,[],[f27])).
% 0.72/0.44 thf(f29,definition,(
% 0.72/0.44 (sF16 = ((f4 @ sF15)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 0.72/0.44 thf(f30,definition,(
% 0.72/0.44 (sF17 = ((f4 @ sF16)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 0.72/0.44 thf(f31,definition,(
% 0.72/0.44 (sF18 = ((f4 @ sF17)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 0.72/0.44 thf(f32,definition,(
% 0.72/0.44 (sF19 = ((f3 @ sF18)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 0.72/0.44 thf(f33,plain,(
% 0.72/0.44 (((f3 @ sF18)) = sF19)),
% 0.72/0.44 inference(reorient_equations,[],[f32])).
% 0.72/0.44 thf(f34,definition,(
% 0.72/0.44 (sF20 = ((f2 @ sF19)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 0.72/0.44 thf(f35,plain,(
% 0.72/0.44 (((f2 @ sF19)) = sF20)),
% 0.72/0.44 inference(reorient_equations,[],[f34])).
% 0.72/0.44 thf(f36,definition,(
% 0.72/0.44 (sF21 = ((f2 @ sF20)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 0.72/0.44 thf(f37,plain,(
% 0.72/0.44 (((f2 @ sF20)) = sF21)),
% 0.72/0.44 inference(reorient_equations,[],[f36])).
% 0.72/0.44 thf(f38,definition,(
% 0.72/0.44 (sF22 = ((f2 @ sF21)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 0.72/0.44 thf(f39,definition,(
% 0.72/0.44 (sF23 = ((f1 @ sF22)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 0.72/0.44 thf(f40,definition,(
% 0.72/0.44 (sF24 = ((f0 @ sF23)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 0.72/0.44 thf(f41,definition,(
% 0.72/0.44 (sF25 = ((f0 @ sF24)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 0.72/0.44 thf(f42,definition,(
% 0.72/0.44 (sF26 = ((f0 @ sF25)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 0.72/0.44 thf(f43,plain,(
% 0.72/0.44 (sF26 != sF12)),
% 0.72/0.44 inference(definition_folding,[],[f4,f42,f41,f40,f39,f38,f37,f35,f33,f31,f30,f29,f28,f26,f25,f8,f24,f23,f22,f21,f20,f18,f17,f16,f15,f14,f12,f10,f8])).
% 0.72/0.44 thf(f44,plain,(
% 0.72/0.44 ($true = sF12) | (sF26 = $true)),
% 0.72/0.44 inference(xor_proxy_clausification,[],[f43])).
% 0.72/0.44 thf(f45,plain,(
% 0.72/0.44 (sF26 = $false) | ($false = sF12)),
% 0.72/0.44 inference(xor_proxy_clausification,[],[f43])).
% 0.72/0.44 thf(f46,plain,(
% 0.72/0.44 ($false = sF20) | ($true = ((f2 @ sF19)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f35])).
% 0.72/0.44 thf(f47,plain,(
% 0.72/0.44 ($true = sF20) | ($false = ((f2 @ sF19)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f35])).
% 0.72/0.44 thf(f48,plain,(
% 0.72/0.44 ($true = sF16) | (((f4 @ sF15)) = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f29])).
% 0.72/0.44 thf(f49,plain,(
% 0.72/0.44 (sF16 = $false) | ($true = ((f4 @ sF15)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f29])).
% 0.72/0.44 thf(f50,plain,(
% 0.72/0.44 ($true = sF7) | ($false = ((f3 @ sF6)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f18])).
% 0.72/0.44 thf(f51,plain,(
% 0.72/0.44 ($false = sF7) | ($true = ((f3 @ sF6)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f18])).
% 0.72/0.44 thf(f52,plain,(
% 0.72/0.44 ($false = ((f6 @ sF0))) | (sF13 = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f25])).
% 0.72/0.44 thf(f53,plain,(
% 0.72/0.44 (sF13 = $false) | ($true = ((f6 @ sF0)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f25])).
% 0.72/0.44 thf(f54,plain,(
% 0.72/0.44 (sF10 = $true) | (((f1 @ sF9)) = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f22])).
% 0.72/0.44 thf(f55,plain,(
% 0.72/0.44 ($true = ((f1 @ sF9))) | (sF10 = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f22])).
% 0.72/0.44 thf(f56,plain,(
% 0.72/0.44 ($false = ((f2 @ sF21))) | ($true = sF22)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f38])).
% 0.72/0.44 thf(f57,plain,(
% 0.72/0.44 ($false = sF22) | ($true = ((f2 @ sF21)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f38])).
% 0.72/0.44 thf(f58,plain,(
% 0.72/0.44 ($false = ((f0 @ sF24))) | ($true = sF25)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f41])).
% 0.72/0.44 thf(f59,plain,(
% 0.72/0.44 ($true = ((f0 @ sF24))) | ($false = sF25)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f41])).
% 0.72/0.44 thf(f60,plain,(
% 0.72/0.44 ($false = ((f4 @ sF16))) | ($true = sF17)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f30])).
% 0.72/0.44 thf(f61,plain,(
% 0.72/0.44 (sF17 = $false) | ($true = ((f4 @ sF16)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f30])).
% 0.72/0.44 thf(f62,plain,(
% 0.72/0.44 (((f5 @ sF2)) = $true) | (sF3 = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f14])).
% 0.72/0.44 thf(f63,plain,(
% 0.72/0.44 (((f5 @ sF2)) = $false) | (sF3 = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f14])).
% 0.72/0.44 thf(f64,plain,(
% 0.72/0.44 (sF14 = $true) | ($false = ((f6 @ sF13)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f26])).
% 0.72/0.44 thf(f65,plain,(
% 0.72/0.44 (sF14 = $false) | ($true = ((f6 @ sF13)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f26])).
% 0.72/0.44 thf(f66,plain,(
% 0.72/0.44 (sF4 = $true) | ($false = ((f4 @ sF3)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f15])).
% 0.72/0.44 thf(f67,plain,(
% 0.72/0.44 (sF4 = $false) | ($true = ((f4 @ sF3)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f15])).
% 0.72/0.44 thf(f68,plain,(
% 0.72/0.44 (((f3 @ sF5)) = $false) | ($true = sF6)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f17])).
% 0.72/0.44 thf(f69,plain,(
% 0.72/0.44 ($true = ((f3 @ sF5))) | (sF6 = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f17])).
% 0.72/0.44 thf(f70,plain,(
% 0.72/0.44 ($false = ((f1 @ sF10))) | (sF11 = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f23])).
% 0.72/0.44 thf(f71,plain,(
% 0.72/0.44 (sF11 = $false) | ($true = ((f1 @ sF10)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f23])).
% 0.72/0.44 thf(f72,plain,(
% 0.72/0.44 ($false = ((f0 @ sF23))) | ($true = sF24)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f40])).
% 0.72/0.44 thf(f73,plain,(
% 0.72/0.44 ($true = ((f0 @ sF23))) | ($false = sF24)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f40])).
% 0.72/0.44 thf(f74,plain,(
% 0.72/0.44 ($true = ((f2 @ sF20))) | ($false = sF21)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f37])).
% 0.72/0.44 thf(f75,plain,(
% 0.72/0.44 ($true = sF21) | ($false = ((f2 @ sF20)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f37])).
% 0.72/0.44 thf(f76,plain,(
% 0.72/0.44 (sF9 = $true) | ($false = ((f1 @ sF8)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f21])).
% 0.72/0.44 thf(f77,plain,(
% 0.72/0.44 (sF9 = $false) | ($true = ((f1 @ sF8)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f21])).
% 0.72/0.44 thf(f78,plain,(
% 0.72/0.44 (sF15 = $false) | (((f5 @ sF14)) = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f28])).
% 0.72/0.44 thf(f79,plain,(
% 0.72/0.44 (sF15 = $true) | (((f5 @ sF14)) = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f28])).
% 0.72/0.44 thf(f80,plain,(
% 0.72/0.44 ($false = ((f1 @ sF22))) | (sF23 = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f39])).
% 0.72/0.44 thf(f81,plain,(
% 0.72/0.44 (sF23 = $false) | ($true = ((f1 @ sF22)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f39])).
% 0.72/0.44 thf(f82,plain,(
% 0.72/0.44 ($true = sF18) | ($false = ((f4 @ sF17)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f31])).
% 0.72/0.44 thf(f83,plain,(
% 0.72/0.44 ($true = ((f4 @ sF17))) | (sF18 = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f31])).
% 0.72/0.44 thf(f84,plain,(
% 0.72/0.44 ($false = sF0) | (((f6 @ x)) = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f8])).
% 0.72/0.44 thf(f85,plain,(
% 0.72/0.44 (((f6 @ x)) = $false) | ($true = sF0)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f8])).
% 0.72/0.44 thf(f86,plain,(
% 0.72/0.44 ($false = sF19) | (((f3 @ sF18)) = $true)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f33])).
% 0.72/0.44 thf(f87,plain,(
% 0.72/0.44 ($true = sF19) | (((f3 @ sF18)) = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f33])).
% 0.72/0.44 thf(f88,plain,(
% 0.72/0.44 (sF26 = $true) | ($false = ((f0 @ sF25)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f42])).
% 0.72/0.44 thf(f89,plain,(
% 0.72/0.44 (sF26 = $false) | ($true = ((f0 @ sF25)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f42])).
% 0.72/0.44 thf(f90,plain,(
% 0.72/0.44 ($false = ((f3 @ sF4))) | ($true = sF5)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f16])).
% 0.72/0.44 thf(f91,plain,(
% 0.72/0.44 ($true = ((f3 @ sF4))) | ($false = sF5)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f16])).
% 0.72/0.44 thf(f92,plain,(
% 0.72/0.44 ($true = ((f5 @ sF0))) | ($false = sF1)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f10])).
% 0.72/0.44 thf(f93,plain,(
% 0.72/0.44 ($true = sF1) | (((f5 @ sF0)) = $false)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f10])).
% 0.72/0.44 thf(f94,plain,(
% 0.72/0.44 ($false = ((f0 @ sF11))) | ($true = sF12)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f24])).
% 0.72/0.44 thf(f95,plain,(
% 0.72/0.44 ($false = sF12) | ($true = ((f0 @ sF11)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f24])).
% 0.72/0.44 thf(f96,plain,(
% 0.72/0.44 ($false = sF8) | ($true = ((f2 @ sF7)))),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f20])).
% 0.72/0.44 thf(f97,plain,(
% 0.72/0.44 ($false = ((f2 @ sF7))) | ($true = sF8)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f20])).
% 0.72/0.44 thf(f98,plain,(
% 0.72/0.44 ($true = ((f5 @ sF1))) | ($false = sF2)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f12])).
% 0.72/0.44 thf(f99,plain,(
% 0.72/0.44 ($false = ((f5 @ sF1))) | ($true = sF2)),
% 0.72/0.44 inference(iff_proxy_clausification,[],[f12])).
% 0.72/0.44 thf(f101,definition,(
% 0.72/0.44 spl27_1 <=> (sF26 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition])).
% 0.72/0.44 thf(f103,plain,(
% 0.72/0.44 (sF26 = $false) | ~spl27_1),
% 0.72/0.44 inference(avatar_component_clause,[],[f101])).
% 0.72/0.44 thf(f105,definition,(
% 0.72/0.44 spl27_2 <=> ($false = sF12)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition])).
% 0.72/0.44 thf(f107,plain,(
% 0.72/0.44 ($false = sF12) | ~spl27_2),
% 0.72/0.44 inference(avatar_component_clause,[],[f105])).
% 0.72/0.44 thf(f108,plain,(
% 0.72/0.44 spl27_1 | spl27_2),
% 0.72/0.44 inference(avatar_split_clause,[],[f45,f105,f101])).
% 0.72/0.44 thf(f110,definition,(
% 0.72/0.44 spl27_3 <=> (sF26 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition])).
% 0.72/0.44 thf(f112,plain,(
% 0.72/0.44 (sF26 = $true) | ~spl27_3),
% 0.72/0.44 inference(avatar_component_clause,[],[f110])).
% 0.72/0.44 thf(f114,definition,(
% 0.72/0.44 spl27_4 <=> ($true = sF12)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition])).
% 0.72/0.44 thf(f116,plain,(
% 0.72/0.44 ($true = sF12) | ~spl27_4),
% 0.72/0.44 inference(avatar_component_clause,[],[f114])).
% 0.72/0.44 thf(f117,plain,(
% 0.72/0.44 spl27_3 | spl27_4),
% 0.72/0.44 inference(avatar_split_clause,[],[f44,f114,f110])).
% 0.72/0.44 thf(f119,definition,(
% 0.72/0.44 spl27_5 <=> ($false = ((f2 @ sF19)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition])).
% 0.72/0.44 thf(f120,plain,(
% 0.72/0.44 ($false != ((f2 @ sF19))) | spl27_5),
% 0.72/0.44 inference(avatar_component_clause,[],[f119])).
% 0.72/0.44 thf(f121,plain,(
% 0.72/0.44 ($false = ((f2 @ sF19))) | ~spl27_5),
% 0.72/0.44 inference(avatar_component_clause,[],[f119])).
% 0.72/0.44 thf(f123,definition,(
% 0.72/0.44 spl27_6 <=> ($true = sF20)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition])).
% 0.72/0.44 thf(f125,plain,(
% 0.72/0.44 ($true = sF20) | ~spl27_6),
% 0.72/0.44 inference(avatar_component_clause,[],[f123])).
% 0.72/0.44 thf(f126,plain,(
% 0.72/0.44 spl27_5 | spl27_6),
% 0.72/0.44 inference(avatar_split_clause,[],[f47,f123,f119])).
% 0.72/0.44 thf(f128,definition,(
% 0.72/0.44 spl27_7 <=> ($true = ((f2 @ sF19)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition])).
% 0.72/0.44 thf(f130,plain,(
% 0.72/0.44 ($true = ((f2 @ sF19))) | ~spl27_7),
% 0.72/0.44 inference(avatar_component_clause,[],[f128])).
% 0.72/0.44 thf(f132,definition,(
% 0.72/0.44 spl27_8 <=> ($false = sF20)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition])).
% 0.72/0.44 thf(f134,plain,(
% 0.72/0.44 ($false = sF20) | ~spl27_8),
% 0.72/0.44 inference(avatar_component_clause,[],[f132])).
% 0.72/0.44 thf(f135,plain,(
% 0.72/0.44 spl27_7 | spl27_8),
% 0.72/0.44 inference(avatar_split_clause,[],[f46,f132,f128])).
% 0.72/0.44 thf(f137,definition,(
% 0.72/0.44 spl27_9 <=> ($true = ((f4 @ sF15)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition])).
% 0.72/0.44 thf(f138,plain,(
% 0.72/0.44 ($true != ((f4 @ sF15))) | spl27_9),
% 0.72/0.44 inference(avatar_component_clause,[],[f137])).
% 0.72/0.44 thf(f139,plain,(
% 0.72/0.44 ($true = ((f4 @ sF15))) | ~spl27_9),
% 0.72/0.44 inference(avatar_component_clause,[],[f137])).
% 0.72/0.44 thf(f141,definition,(
% 0.72/0.44 spl27_10 <=> (sF16 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition])).
% 0.72/0.44 thf(f143,plain,(
% 0.72/0.44 (sF16 = $false) | ~spl27_10),
% 0.72/0.44 inference(avatar_component_clause,[],[f141])).
% 0.72/0.44 thf(f144,plain,(
% 0.72/0.44 spl27_9 | spl27_10),
% 0.72/0.44 inference(avatar_split_clause,[],[f49,f141,f137])).
% 0.72/0.44 thf(f146,definition,(
% 0.72/0.44 spl27_11 <=> (((f4 @ sF15)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition])).
% 0.72/0.44 thf(f148,plain,(
% 0.72/0.44 (((f4 @ sF15)) = $false) | ~spl27_11),
% 0.72/0.44 inference(avatar_component_clause,[],[f146])).
% 0.72/0.44 thf(f150,definition,(
% 0.72/0.44 spl27_12 <=> ($true = sF16)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition])).
% 0.72/0.44 thf(f152,plain,(
% 0.72/0.44 ($true = sF16) | ~spl27_12),
% 0.72/0.44 inference(avatar_component_clause,[],[f150])).
% 0.72/0.44 thf(f153,plain,(
% 0.72/0.44 spl27_11 | spl27_12),
% 0.72/0.44 inference(avatar_split_clause,[],[f48,f150,f146])).
% 0.72/0.44 thf(f155,definition,(
% 0.72/0.44 spl27_13 <=> ($true = ((f3 @ sF6)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition])).
% 0.72/0.44 thf(f156,plain,(
% 0.72/0.44 ($true != ((f3 @ sF6))) | spl27_13),
% 0.72/0.44 inference(avatar_component_clause,[],[f155])).
% 0.72/0.44 thf(f157,plain,(
% 0.72/0.44 ($true = ((f3 @ sF6))) | ~spl27_13),
% 0.72/0.44 inference(avatar_component_clause,[],[f155])).
% 0.72/0.44 thf(f159,definition,(
% 0.72/0.44 spl27_14 <=> ($false = sF7)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition])).
% 0.72/0.44 thf(f161,plain,(
% 0.72/0.44 ($false = sF7) | ~spl27_14),
% 0.72/0.44 inference(avatar_component_clause,[],[f159])).
% 0.72/0.44 thf(f162,plain,(
% 0.72/0.44 spl27_13 | spl27_14),
% 0.72/0.44 inference(avatar_split_clause,[],[f51,f159,f155])).
% 0.72/0.44 thf(f164,definition,(
% 0.72/0.44 spl27_15 <=> ($false = ((f3 @ sF6)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_15])],[avatar_definition])).
% 0.72/0.44 thf(f165,plain,(
% 0.72/0.44 ($false != ((f3 @ sF6))) | spl27_15),
% 0.72/0.44 inference(avatar_component_clause,[],[f164])).
% 0.72/0.44 thf(f166,plain,(
% 0.72/0.44 ($false = ((f3 @ sF6))) | ~spl27_15),
% 0.72/0.44 inference(avatar_component_clause,[],[f164])).
% 0.72/0.44 thf(f168,definition,(
% 0.72/0.44 spl27_16 <=> ($true = sF7)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_16])],[avatar_definition])).
% 0.72/0.44 thf(f170,plain,(
% 0.72/0.44 ($true = sF7) | ~spl27_16),
% 0.72/0.44 inference(avatar_component_clause,[],[f168])).
% 0.72/0.44 thf(f171,plain,(
% 0.72/0.44 spl27_15 | spl27_16),
% 0.72/0.44 inference(avatar_split_clause,[],[f50,f168,f164])).
% 0.72/0.44 thf(f173,definition,(
% 0.72/0.44 spl27_17 <=> ($true = ((f6 @ sF0)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_17])],[avatar_definition])).
% 0.72/0.44 thf(f175,plain,(
% 0.72/0.44 ($true = ((f6 @ sF0))) | ~spl27_17),
% 0.72/0.44 inference(avatar_component_clause,[],[f173])).
% 0.72/0.44 thf(f177,definition,(
% 0.72/0.44 spl27_18 <=> (sF13 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition])).
% 0.72/0.44 thf(f178,plain,(
% 0.72/0.44 (sF13 != $false) | spl27_18),
% 0.72/0.44 inference(avatar_component_clause,[],[f177])).
% 0.72/0.44 thf(f179,plain,(
% 0.72/0.44 (sF13 = $false) | ~spl27_18),
% 0.72/0.44 inference(avatar_component_clause,[],[f177])).
% 0.72/0.44 thf(f180,plain,(
% 0.72/0.44 spl27_17 | spl27_18),
% 0.72/0.44 inference(avatar_split_clause,[],[f53,f177,f173])).
% 0.72/0.44 thf(f182,definition,(
% 0.72/0.44 spl27_19 <=> ($false = ((f6 @ sF0)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_19])],[avatar_definition])).
% 0.72/0.44 thf(f184,plain,(
% 0.72/0.44 ($false = ((f6 @ sF0))) | ~spl27_19),
% 0.72/0.44 inference(avatar_component_clause,[],[f182])).
% 0.72/0.44 thf(f186,definition,(
% 0.72/0.44 spl27_20 <=> (sF13 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition])).
% 0.72/0.44 thf(f187,plain,(
% 0.72/0.44 (sF13 != $true) | spl27_20),
% 0.72/0.44 inference(avatar_component_clause,[],[f186])).
% 0.72/0.44 thf(f188,plain,(
% 0.72/0.44 (sF13 = $true) | ~spl27_20),
% 0.72/0.44 inference(avatar_component_clause,[],[f186])).
% 0.72/0.44 thf(f189,plain,(
% 0.72/0.44 spl27_19 | spl27_20),
% 0.72/0.44 inference(avatar_split_clause,[],[f52,f186,f182])).
% 0.72/0.44 thf(f191,definition,(
% 0.72/0.44 spl27_21 <=> ($true = ((f1 @ sF9)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition])).
% 0.72/0.44 thf(f193,plain,(
% 0.72/0.44 ($true = ((f1 @ sF9))) | ~spl27_21),
% 0.72/0.44 inference(avatar_component_clause,[],[f191])).
% 0.72/0.44 thf(f195,definition,(
% 0.72/0.44 spl27_22 <=> (sF10 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_22])],[avatar_definition])).
% 0.72/0.44 thf(f197,plain,(
% 0.72/0.44 (sF10 = $false) | ~spl27_22),
% 0.72/0.44 inference(avatar_component_clause,[],[f195])).
% 0.72/0.44 thf(f198,plain,(
% 0.72/0.44 spl27_21 | spl27_22),
% 0.72/0.44 inference(avatar_split_clause,[],[f55,f195,f191])).
% 0.72/0.44 thf(f200,definition,(
% 0.72/0.44 spl27_23 <=> (((f1 @ sF9)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_23])],[avatar_definition])).
% 0.72/0.44 thf(f202,plain,(
% 0.72/0.44 (((f1 @ sF9)) = $false) | ~spl27_23),
% 0.72/0.44 inference(avatar_component_clause,[],[f200])).
% 0.72/0.44 thf(f204,definition,(
% 0.72/0.44 spl27_24 <=> (sF10 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_24])],[avatar_definition])).
% 0.72/0.44 thf(f205,plain,(
% 0.72/0.44 (sF10 != $true) | spl27_24),
% 0.72/0.44 inference(avatar_component_clause,[],[f204])).
% 0.72/0.44 thf(f206,plain,(
% 0.72/0.44 (sF10 = $true) | ~spl27_24),
% 0.72/0.44 inference(avatar_component_clause,[],[f204])).
% 0.72/0.44 thf(f207,plain,(
% 0.72/0.44 spl27_23 | spl27_24),
% 0.72/0.44 inference(avatar_split_clause,[],[f54,f204,f200])).
% 0.72/0.44 thf(f209,definition,(
% 0.72/0.44 spl27_25 <=> ($false = sF22)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_25])],[avatar_definition])).
% 0.72/0.44 thf(f211,plain,(
% 0.72/0.44 ($false = sF22) | ~spl27_25),
% 0.72/0.44 inference(avatar_component_clause,[],[f209])).
% 0.72/0.44 thf(f213,definition,(
% 0.72/0.44 spl27_26 <=> ($true = ((f2 @ sF21)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_26])],[avatar_definition])).
% 0.72/0.44 thf(f215,plain,(
% 0.72/0.44 ($true = ((f2 @ sF21))) | ~spl27_26),
% 0.72/0.44 inference(avatar_component_clause,[],[f213])).
% 0.72/0.44 thf(f216,plain,(
% 0.72/0.44 spl27_25 | spl27_26),
% 0.72/0.44 inference(avatar_split_clause,[],[f57,f213,f209])).
% 0.72/0.44 thf(f218,definition,(
% 0.72/0.44 spl27_27 <=> ($false = ((f2 @ sF21)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_27])],[avatar_definition])).
% 0.72/0.44 thf(f219,plain,(
% 0.72/0.44 ($false != ((f2 @ sF21))) | spl27_27),
% 0.72/0.44 inference(avatar_component_clause,[],[f218])).
% 0.72/0.44 thf(f220,plain,(
% 0.72/0.44 ($false = ((f2 @ sF21))) | ~spl27_27),
% 0.72/0.44 inference(avatar_component_clause,[],[f218])).
% 0.72/0.44 thf(f222,definition,(
% 0.72/0.44 spl27_28 <=> ($true = sF22)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_28])],[avatar_definition])).
% 0.72/0.44 thf(f224,plain,(
% 0.72/0.44 ($true = sF22) | ~spl27_28),
% 0.72/0.44 inference(avatar_component_clause,[],[f222])).
% 0.72/0.44 thf(f225,plain,(
% 0.72/0.44 spl27_27 | spl27_28),
% 0.72/0.44 inference(avatar_split_clause,[],[f56,f222,f218])).
% 0.72/0.44 thf(f227,definition,(
% 0.72/0.44 spl27_29 <=> ($false = sF25)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition])).
% 0.72/0.44 thf(f229,plain,(
% 0.72/0.44 ($false = sF25) | ~spl27_29),
% 0.72/0.44 inference(avatar_component_clause,[],[f227])).
% 0.72/0.44 thf(f231,definition,(
% 0.72/0.44 spl27_30 <=> ($true = ((f0 @ sF24)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition])).
% 0.72/0.44 thf(f232,plain,(
% 0.72/0.44 ($true != ((f0 @ sF24))) | spl27_30),
% 0.72/0.44 inference(avatar_component_clause,[],[f231])).
% 0.72/0.44 thf(f233,plain,(
% 0.72/0.44 ($true = ((f0 @ sF24))) | ~spl27_30),
% 0.72/0.44 inference(avatar_component_clause,[],[f231])).
% 0.72/0.44 thf(f234,plain,(
% 0.72/0.44 spl27_29 | spl27_30),
% 0.72/0.44 inference(avatar_split_clause,[],[f59,f231,f227])).
% 0.72/0.44 thf(f236,definition,(
% 0.72/0.44 spl27_31 <=> ($true = sF25)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_31])],[avatar_definition])).
% 0.72/0.44 thf(f237,plain,(
% 0.72/0.44 ($true != sF25) | spl27_31),
% 0.72/0.44 inference(avatar_component_clause,[],[f236])).
% 0.72/0.44 thf(f238,plain,(
% 0.72/0.44 ($true = sF25) | ~spl27_31),
% 0.72/0.44 inference(avatar_component_clause,[],[f236])).
% 0.72/0.44 thf(f240,definition,(
% 0.72/0.44 spl27_32 <=> ($false = ((f0 @ sF24)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_32])],[avatar_definition])).
% 0.72/0.44 thf(f242,plain,(
% 0.72/0.44 ($false = ((f0 @ sF24))) | ~spl27_32),
% 0.72/0.44 inference(avatar_component_clause,[],[f240])).
% 0.72/0.44 thf(f243,plain,(
% 0.72/0.44 spl27_31 | spl27_32),
% 0.72/0.44 inference(avatar_split_clause,[],[f58,f240,f236])).
% 0.72/0.44 thf(f245,definition,(
% 0.72/0.44 spl27_33 <=> (sF17 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_33])],[avatar_definition])).
% 0.72/0.44 thf(f247,plain,(
% 0.72/0.44 (sF17 = $false) | ~spl27_33),
% 0.72/0.44 inference(avatar_component_clause,[],[f245])).
% 0.72/0.44 thf(f249,definition,(
% 0.72/0.44 spl27_34 <=> ($true = ((f4 @ sF16)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition])).
% 0.72/0.44 thf(f250,plain,(
% 0.72/0.44 ($true != ((f4 @ sF16))) | spl27_34),
% 0.72/0.44 inference(avatar_component_clause,[],[f249])).
% 0.72/0.44 thf(f251,plain,(
% 0.72/0.44 ($true = ((f4 @ sF16))) | ~spl27_34),
% 0.72/0.44 inference(avatar_component_clause,[],[f249])).
% 0.72/0.44 thf(f252,plain,(
% 0.72/0.44 spl27_33 | spl27_34),
% 0.72/0.44 inference(avatar_split_clause,[],[f61,f249,f245])).
% 0.72/0.44 thf(f254,definition,(
% 0.72/0.44 spl27_35 <=> ($true = sF17)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition])).
% 0.72/0.44 thf(f256,plain,(
% 0.72/0.44 ($true = sF17) | ~spl27_35),
% 0.72/0.44 inference(avatar_component_clause,[],[f254])).
% 0.72/0.44 thf(f258,definition,(
% 0.72/0.44 spl27_36 <=> ($false = ((f4 @ sF16)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_36])],[avatar_definition])).
% 0.72/0.44 thf(f260,plain,(
% 0.72/0.44 ($false = ((f4 @ sF16))) | ~spl27_36),
% 0.72/0.44 inference(avatar_component_clause,[],[f258])).
% 0.72/0.44 thf(f261,plain,(
% 0.72/0.44 spl27_35 | spl27_36),
% 0.72/0.44 inference(avatar_split_clause,[],[f60,f258,f254])).
% 0.72/0.44 thf(f263,definition,(
% 0.72/0.44 spl27_37 <=> (sF3 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_37])],[avatar_definition])).
% 0.72/0.44 thf(f264,plain,(
% 0.72/0.44 (sF3 != $true) | spl27_37),
% 0.72/0.44 inference(avatar_component_clause,[],[f263])).
% 0.72/0.44 thf(f265,plain,(
% 0.72/0.44 (sF3 = $true) | ~spl27_37),
% 0.72/0.44 inference(avatar_component_clause,[],[f263])).
% 0.72/0.44 thf(f267,definition,(
% 0.72/0.44 spl27_38 <=> (((f5 @ sF2)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_38])],[avatar_definition])).
% 0.72/0.44 thf(f268,plain,(
% 0.72/0.44 (((f5 @ sF2)) != $false) | spl27_38),
% 0.72/0.44 inference(avatar_component_clause,[],[f267])).
% 0.72/0.44 thf(f269,plain,(
% 0.72/0.44 (((f5 @ sF2)) = $false) | ~spl27_38),
% 0.72/0.44 inference(avatar_component_clause,[],[f267])).
% 0.72/0.44 thf(f270,plain,(
% 0.72/0.44 spl27_37 | spl27_38),
% 0.72/0.44 inference(avatar_split_clause,[],[f63,f267,f263])).
% 0.72/0.44 thf(f272,definition,(
% 0.72/0.44 spl27_39 <=> (sF3 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_39])],[avatar_definition])).
% 0.72/0.44 thf(f274,plain,(
% 0.72/0.44 (sF3 = $false) | ~spl27_39),
% 0.72/0.44 inference(avatar_component_clause,[],[f272])).
% 0.72/0.44 thf(f276,definition,(
% 0.72/0.44 spl27_40 <=> (((f5 @ sF2)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_40])],[avatar_definition])).
% 0.72/0.44 thf(f278,plain,(
% 0.72/0.44 (((f5 @ sF2)) = $true) | ~spl27_40),
% 0.72/0.44 inference(avatar_component_clause,[],[f276])).
% 0.72/0.44 thf(f279,plain,(
% 0.72/0.44 spl27_39 | spl27_40),
% 0.72/0.44 inference(avatar_split_clause,[],[f62,f276,f272])).
% 0.72/0.44 thf(f281,definition,(
% 0.72/0.44 spl27_41 <=> ($true = ((f6 @ sF13)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_41])],[avatar_definition])).
% 0.72/0.44 thf(f282,plain,(
% 0.72/0.44 ($true != ((f6 @ sF13))) | spl27_41),
% 0.72/0.44 inference(avatar_component_clause,[],[f281])).
% 0.72/0.44 thf(f283,plain,(
% 0.72/0.44 ($true = ((f6 @ sF13))) | ~spl27_41),
% 0.72/0.44 inference(avatar_component_clause,[],[f281])).
% 0.72/0.44 thf(f285,definition,(
% 0.72/0.44 spl27_42 <=> (sF14 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_42])],[avatar_definition])).
% 0.72/0.44 thf(f287,plain,(
% 0.72/0.44 (sF14 = $false) | ~spl27_42),
% 0.72/0.44 inference(avatar_component_clause,[],[f285])).
% 0.72/0.44 thf(f288,plain,(
% 0.72/0.44 spl27_41 | spl27_42),
% 0.72/0.44 inference(avatar_split_clause,[],[f65,f285,f281])).
% 0.72/0.44 thf(f290,definition,(
% 0.72/0.44 spl27_43 <=> (sF14 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_43])],[avatar_definition])).
% 0.72/0.44 thf(f292,plain,(
% 0.72/0.44 (sF14 = $true) | ~spl27_43),
% 0.72/0.44 inference(avatar_component_clause,[],[f290])).
% 0.72/0.44 thf(f294,definition,(
% 0.72/0.44 spl27_44 <=> ($false = ((f6 @ sF13)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_44])],[avatar_definition])).
% 0.72/0.44 thf(f296,plain,(
% 0.72/0.44 ($false = ((f6 @ sF13))) | ~spl27_44),
% 0.72/0.44 inference(avatar_component_clause,[],[f294])).
% 0.72/0.44 thf(f297,plain,(
% 0.72/0.44 spl27_43 | spl27_44),
% 0.72/0.44 inference(avatar_split_clause,[],[f64,f294,f290])).
% 0.72/0.44 thf(f299,definition,(
% 0.72/0.44 spl27_45 <=> ($true = ((f4 @ sF3)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition])).
% 0.72/0.44 thf(f300,plain,(
% 0.72/0.44 ($true != ((f4 @ sF3))) | spl27_45),
% 0.72/0.44 inference(avatar_component_clause,[],[f299])).
% 0.72/0.44 thf(f301,plain,(
% 0.72/0.44 ($true = ((f4 @ sF3))) | ~spl27_45),
% 0.72/0.44 inference(avatar_component_clause,[],[f299])).
% 0.72/0.44 thf(f303,definition,(
% 0.72/0.44 spl27_46 <=> (sF4 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition])).
% 0.72/0.44 thf(f305,plain,(
% 0.72/0.44 (sF4 = $false) | ~spl27_46),
% 0.72/0.44 inference(avatar_component_clause,[],[f303])).
% 0.72/0.44 thf(f306,plain,(
% 0.72/0.44 spl27_45 | spl27_46),
% 0.72/0.44 inference(avatar_split_clause,[],[f67,f303,f299])).
% 0.72/0.44 thf(f308,definition,(
% 0.72/0.44 spl27_47 <=> ($false = ((f4 @ sF3)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_47])],[avatar_definition])).
% 0.72/0.44 thf(f310,plain,(
% 0.72/0.44 ($false = ((f4 @ sF3))) | ~spl27_47),
% 0.72/0.44 inference(avatar_component_clause,[],[f308])).
% 0.72/0.44 thf(f312,definition,(
% 0.72/0.44 spl27_48 <=> (sF4 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition])).
% 0.72/0.44 thf(f314,plain,(
% 0.72/0.44 (sF4 = $true) | ~spl27_48),
% 0.72/0.44 inference(avatar_component_clause,[],[f312])).
% 0.72/0.44 thf(f315,plain,(
% 0.72/0.44 spl27_47 | spl27_48),
% 0.72/0.44 inference(avatar_split_clause,[],[f66,f312,f308])).
% 0.72/0.44 thf(f317,definition,(
% 0.72/0.44 spl27_49 <=> ($true = ((f3 @ sF5)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_49])],[avatar_definition])).
% 0.72/0.44 thf(f319,plain,(
% 0.72/0.44 ($true = ((f3 @ sF5))) | ~spl27_49),
% 0.72/0.44 inference(avatar_component_clause,[],[f317])).
% 0.72/0.44 thf(f321,definition,(
% 0.72/0.44 spl27_50 <=> (sF6 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_50])],[avatar_definition])).
% 0.72/0.44 thf(f323,plain,(
% 0.72/0.44 (sF6 = $false) | ~spl27_50),
% 0.72/0.44 inference(avatar_component_clause,[],[f321])).
% 0.72/0.44 thf(f324,plain,(
% 0.72/0.44 spl27_49 | spl27_50),
% 0.72/0.44 inference(avatar_split_clause,[],[f69,f321,f317])).
% 0.72/0.44 thf(f326,definition,(
% 0.72/0.44 spl27_51 <=> ($true = sF6)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_51])],[avatar_definition])).
% 0.72/0.44 thf(f327,plain,(
% 0.72/0.44 ($true != sF6) | spl27_51),
% 0.72/0.44 inference(avatar_component_clause,[],[f326])).
% 0.72/0.44 thf(f328,plain,(
% 0.72/0.44 ($true = sF6) | ~spl27_51),
% 0.72/0.44 inference(avatar_component_clause,[],[f326])).
% 0.72/0.44 thf(f330,definition,(
% 0.72/0.44 spl27_52 <=> (((f3 @ sF5)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_52])],[avatar_definition])).
% 0.72/0.44 thf(f332,plain,(
% 0.72/0.44 (((f3 @ sF5)) = $false) | ~spl27_52),
% 0.72/0.44 inference(avatar_component_clause,[],[f330])).
% 0.72/0.44 thf(f333,plain,(
% 0.72/0.44 spl27_51 | spl27_52),
% 0.72/0.44 inference(avatar_split_clause,[],[f68,f330,f326])).
% 0.72/0.44 thf(f335,definition,(
% 0.72/0.44 spl27_53 <=> (sF11 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_53])],[avatar_definition])).
% 0.72/0.44 thf(f337,plain,(
% 0.72/0.44 (sF11 = $false) | ~spl27_53),
% 0.72/0.44 inference(avatar_component_clause,[],[f335])).
% 0.72/0.44 thf(f339,definition,(
% 0.72/0.44 spl27_54 <=> ($true = ((f1 @ sF10)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_54])],[avatar_definition])).
% 0.72/0.44 thf(f340,plain,(
% 0.72/0.44 ($true != ((f1 @ sF10))) | spl27_54),
% 0.72/0.44 inference(avatar_component_clause,[],[f339])).
% 0.72/0.44 thf(f341,plain,(
% 0.72/0.44 ($true = ((f1 @ sF10))) | ~spl27_54),
% 0.72/0.44 inference(avatar_component_clause,[],[f339])).
% 0.72/0.44 thf(f342,plain,(
% 0.72/0.44 spl27_53 | spl27_54),
% 0.72/0.44 inference(avatar_split_clause,[],[f71,f339,f335])).
% 0.72/0.44 thf(f344,definition,(
% 0.72/0.44 spl27_55 <=> (sF11 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_55])],[avatar_definition])).
% 0.72/0.44 thf(f346,plain,(
% 0.72/0.44 (sF11 = $true) | ~spl27_55),
% 0.72/0.44 inference(avatar_component_clause,[],[f344])).
% 0.72/0.44 thf(f348,definition,(
% 0.72/0.44 spl27_56 <=> ($false = ((f1 @ sF10)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_56])],[avatar_definition])).
% 0.72/0.44 thf(f350,plain,(
% 0.72/0.44 ($false = ((f1 @ sF10))) | ~spl27_56),
% 0.72/0.44 inference(avatar_component_clause,[],[f348])).
% 0.72/0.44 thf(f351,plain,(
% 0.72/0.44 spl27_55 | spl27_56),
% 0.72/0.44 inference(avatar_split_clause,[],[f70,f348,f344])).
% 0.72/0.44 thf(f353,definition,(
% 0.72/0.44 spl27_57 <=> ($true = ((f0 @ sF23)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_57])],[avatar_definition])).
% 0.72/0.44 thf(f354,plain,(
% 0.72/0.44 ($true != ((f0 @ sF23))) | spl27_57),
% 0.72/0.44 inference(avatar_component_clause,[],[f353])).
% 0.72/0.44 thf(f355,plain,(
% 0.72/0.44 ($true = ((f0 @ sF23))) | ~spl27_57),
% 0.72/0.44 inference(avatar_component_clause,[],[f353])).
% 0.72/0.44 thf(f357,definition,(
% 0.72/0.44 spl27_58 <=> ($false = sF24)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_58])],[avatar_definition])).
% 0.72/0.44 thf(f358,plain,(
% 0.72/0.44 ($false != sF24) | spl27_58),
% 0.72/0.44 inference(avatar_component_clause,[],[f357])).
% 0.72/0.44 thf(f359,plain,(
% 0.72/0.44 ($false = sF24) | ~spl27_58),
% 0.72/0.44 inference(avatar_component_clause,[],[f357])).
% 0.72/0.44 thf(f360,plain,(
% 0.72/0.44 spl27_57 | spl27_58),
% 0.72/0.44 inference(avatar_split_clause,[],[f73,f357,f353])).
% 0.72/0.44 thf(f362,definition,(
% 0.72/0.44 spl27_59 <=> ($true = sF24)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_59])],[avatar_definition])).
% 0.72/0.44 thf(f363,plain,(
% 0.72/0.44 ($true != sF24) | spl27_59),
% 0.72/0.44 inference(avatar_component_clause,[],[f362])).
% 0.72/0.44 thf(f364,plain,(
% 0.72/0.44 ($true = sF24) | ~spl27_59),
% 0.72/0.44 inference(avatar_component_clause,[],[f362])).
% 0.72/0.44 thf(f366,definition,(
% 0.72/0.44 spl27_60 <=> ($false = ((f0 @ sF23)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_60])],[avatar_definition])).
% 0.72/0.44 thf(f368,plain,(
% 0.72/0.44 ($false = ((f0 @ sF23))) | ~spl27_60),
% 0.72/0.44 inference(avatar_component_clause,[],[f366])).
% 0.72/0.44 thf(f369,plain,(
% 0.72/0.44 spl27_59 | spl27_60),
% 0.72/0.44 inference(avatar_split_clause,[],[f72,f366,f362])).
% 0.72/0.44 thf(f371,definition,(
% 0.72/0.44 spl27_61 <=> ($true = sF21)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_61])],[avatar_definition])).
% 0.72/0.44 thf(f372,plain,(
% 0.72/0.44 ($true != sF21) | spl27_61),
% 0.72/0.44 inference(avatar_component_clause,[],[f371])).
% 0.72/0.44 thf(f373,plain,(
% 0.72/0.44 ($true = sF21) | ~spl27_61),
% 0.72/0.44 inference(avatar_component_clause,[],[f371])).
% 0.72/0.44 thf(f375,definition,(
% 0.72/0.44 spl27_62 <=> ($false = ((f2 @ sF20)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_62])],[avatar_definition])).
% 0.72/0.44 thf(f376,plain,(
% 0.72/0.44 ($false != ((f2 @ sF20))) | spl27_62),
% 0.72/0.44 inference(avatar_component_clause,[],[f375])).
% 0.72/0.44 thf(f377,plain,(
% 0.72/0.44 ($false = ((f2 @ sF20))) | ~spl27_62),
% 0.72/0.44 inference(avatar_component_clause,[],[f375])).
% 0.72/0.44 thf(f378,plain,(
% 0.72/0.44 spl27_61 | spl27_62),
% 0.72/0.44 inference(avatar_split_clause,[],[f75,f375,f371])).
% 0.72/0.44 thf(f380,definition,(
% 0.72/0.44 spl27_63 <=> ($false = sF21)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_63])],[avatar_definition])).
% 0.72/0.44 thf(f382,plain,(
% 0.72/0.44 ($false = sF21) | ~spl27_63),
% 0.72/0.44 inference(avatar_component_clause,[],[f380])).
% 0.72/0.44 thf(f384,definition,(
% 0.72/0.44 spl27_64 <=> ($true = ((f2 @ sF20)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_64])],[avatar_definition])).
% 0.72/0.44 thf(f385,plain,(
% 0.72/0.44 ($true != ((f2 @ sF20))) | spl27_64),
% 0.72/0.44 inference(avatar_component_clause,[],[f384])).
% 0.72/0.44 thf(f386,plain,(
% 0.72/0.44 ($true = ((f2 @ sF20))) | ~spl27_64),
% 0.72/0.44 inference(avatar_component_clause,[],[f384])).
% 0.72/0.44 thf(f387,plain,(
% 0.72/0.44 spl27_63 | spl27_64),
% 0.72/0.44 inference(avatar_split_clause,[],[f74,f384,f380])).
% 0.72/0.44 thf(f389,definition,(
% 0.72/0.44 spl27_65 <=> ($true = ((f1 @ sF8)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_65])],[avatar_definition])).
% 0.72/0.44 thf(f391,plain,(
% 0.72/0.44 ($true = ((f1 @ sF8))) | ~spl27_65),
% 0.72/0.44 inference(avatar_component_clause,[],[f389])).
% 0.72/0.44 thf(f393,definition,(
% 0.72/0.44 spl27_66 <=> (sF9 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_66])],[avatar_definition])).
% 0.72/0.44 thf(f395,plain,(
% 0.72/0.44 (sF9 = $false) | ~spl27_66),
% 0.72/0.44 inference(avatar_component_clause,[],[f393])).
% 0.72/0.44 thf(f396,plain,(
% 0.72/0.44 spl27_65 | spl27_66),
% 0.72/0.44 inference(avatar_split_clause,[],[f77,f393,f389])).
% 0.72/0.44 thf(f398,definition,(
% 0.72/0.44 spl27_67 <=> (sF9 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_67])],[avatar_definition])).
% 0.72/0.44 thf(f400,plain,(
% 0.72/0.44 (sF9 = $true) | ~spl27_67),
% 0.72/0.44 inference(avatar_component_clause,[],[f398])).
% 0.72/0.44 thf(f402,definition,(
% 0.72/0.44 spl27_68 <=> ($false = ((f1 @ sF8)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_68])],[avatar_definition])).
% 0.72/0.44 thf(f404,plain,(
% 0.72/0.44 ($false = ((f1 @ sF8))) | ~spl27_68),
% 0.72/0.44 inference(avatar_component_clause,[],[f402])).
% 0.72/0.44 thf(f405,plain,(
% 0.72/0.44 spl27_67 | spl27_68),
% 0.72/0.44 inference(avatar_split_clause,[],[f76,f402,f398])).
% 0.72/0.44 thf(f407,definition,(
% 0.72/0.44 spl27_69 <=> (sF15 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_69])],[avatar_definition])).
% 0.72/0.44 thf(f408,plain,(
% 0.72/0.44 (sF15 != $true) | spl27_69),
% 0.72/0.44 inference(avatar_component_clause,[],[f407])).
% 0.72/0.44 thf(f409,plain,(
% 0.72/0.44 (sF15 = $true) | ~spl27_69),
% 0.72/0.44 inference(avatar_component_clause,[],[f407])).
% 0.72/0.44 thf(f411,definition,(
% 0.72/0.44 spl27_70 <=> (((f5 @ sF14)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_70])],[avatar_definition])).
% 0.72/0.44 thf(f412,plain,(
% 0.72/0.44 (((f5 @ sF14)) != $false) | spl27_70),
% 0.72/0.44 inference(avatar_component_clause,[],[f411])).
% 0.72/0.44 thf(f413,plain,(
% 0.72/0.44 (((f5 @ sF14)) = $false) | ~spl27_70),
% 0.72/0.44 inference(avatar_component_clause,[],[f411])).
% 0.72/0.44 thf(f414,plain,(
% 0.72/0.44 spl27_69 | spl27_70),
% 0.72/0.44 inference(avatar_split_clause,[],[f79,f411,f407])).
% 0.72/0.44 thf(f416,definition,(
% 0.72/0.44 spl27_71 <=> (((f5 @ sF14)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_71])],[avatar_definition])).
% 0.72/0.44 thf(f417,plain,(
% 0.72/0.44 (((f5 @ sF14)) != $true) | spl27_71),
% 0.72/0.44 inference(avatar_component_clause,[],[f416])).
% 0.72/0.44 thf(f418,plain,(
% 0.72/0.44 (((f5 @ sF14)) = $true) | ~spl27_71),
% 0.72/0.44 inference(avatar_component_clause,[],[f416])).
% 0.72/0.44 thf(f420,definition,(
% 0.72/0.44 spl27_72 <=> (sF15 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_72])],[avatar_definition])).
% 0.72/0.44 thf(f422,plain,(
% 0.72/0.44 (sF15 = $false) | ~spl27_72),
% 0.72/0.44 inference(avatar_component_clause,[],[f420])).
% 0.72/0.44 thf(f423,plain,(
% 0.72/0.44 spl27_71 | spl27_72),
% 0.72/0.44 inference(avatar_split_clause,[],[f78,f420,f416])).
% 0.72/0.44 thf(f425,definition,(
% 0.72/0.44 spl27_73 <=> (sF23 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_73])],[avatar_definition])).
% 0.72/0.44 thf(f426,plain,(
% 0.72/0.44 (sF23 != $false) | spl27_73),
% 0.72/0.44 inference(avatar_component_clause,[],[f425])).
% 0.72/0.44 thf(f427,plain,(
% 0.72/0.44 (sF23 = $false) | ~spl27_73),
% 0.72/0.44 inference(avatar_component_clause,[],[f425])).
% 0.72/0.44 thf(f429,definition,(
% 0.72/0.44 spl27_74 <=> ($true = ((f1 @ sF22)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_74])],[avatar_definition])).
% 0.72/0.44 thf(f430,plain,(
% 0.72/0.44 ($true != ((f1 @ sF22))) | spl27_74),
% 0.72/0.44 inference(avatar_component_clause,[],[f429])).
% 0.72/0.44 thf(f431,plain,(
% 0.72/0.44 ($true = ((f1 @ sF22))) | ~spl27_74),
% 0.72/0.44 inference(avatar_component_clause,[],[f429])).
% 0.72/0.44 thf(f432,plain,(
% 0.72/0.44 spl27_73 | spl27_74),
% 0.72/0.44 inference(avatar_split_clause,[],[f81,f429,f425])).
% 0.72/0.44 thf(f434,definition,(
% 0.72/0.44 spl27_75 <=> ($false = ((f1 @ sF22)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_75])],[avatar_definition])).
% 0.72/0.44 thf(f435,plain,(
% 0.72/0.44 ($false != ((f1 @ sF22))) | spl27_75),
% 0.72/0.44 inference(avatar_component_clause,[],[f434])).
% 0.72/0.44 thf(f436,plain,(
% 0.72/0.44 ($false = ((f1 @ sF22))) | ~spl27_75),
% 0.72/0.44 inference(avatar_component_clause,[],[f434])).
% 0.72/0.44 thf(f438,definition,(
% 0.72/0.44 spl27_76 <=> (sF23 = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_76])],[avatar_definition])).
% 0.72/0.44 thf(f439,plain,(
% 0.72/0.44 (sF23 != $true) | spl27_76),
% 0.72/0.44 inference(avatar_component_clause,[],[f438])).
% 0.72/0.44 thf(f440,plain,(
% 0.72/0.44 (sF23 = $true) | ~spl27_76),
% 0.72/0.44 inference(avatar_component_clause,[],[f438])).
% 0.72/0.44 thf(f441,plain,(
% 0.72/0.44 spl27_75 | spl27_76),
% 0.72/0.44 inference(avatar_split_clause,[],[f80,f438,f434])).
% 0.72/0.44 thf(f443,definition,(
% 0.72/0.44 spl27_77 <=> (sF18 = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_77])],[avatar_definition])).
% 0.72/0.44 thf(f444,plain,(
% 0.72/0.44 (sF18 != $false) | spl27_77),
% 0.72/0.44 inference(avatar_component_clause,[],[f443])).
% 0.72/0.44 thf(f445,plain,(
% 0.72/0.44 (sF18 = $false) | ~spl27_77),
% 0.72/0.44 inference(avatar_component_clause,[],[f443])).
% 0.72/0.44 thf(f447,definition,(
% 0.72/0.44 spl27_78 <=> ($true = ((f4 @ sF17)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_78])],[avatar_definition])).
% 0.72/0.44 thf(f449,plain,(
% 0.72/0.44 ($true = ((f4 @ sF17))) | ~spl27_78),
% 0.72/0.44 inference(avatar_component_clause,[],[f447])).
% 0.72/0.44 thf(f450,plain,(
% 0.72/0.44 spl27_77 | spl27_78),
% 0.72/0.44 inference(avatar_split_clause,[],[f83,f447,f443])).
% 0.72/0.44 thf(f452,definition,(
% 0.72/0.44 spl27_79 <=> ($false = ((f4 @ sF17)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_79])],[avatar_definition])).
% 0.72/0.44 thf(f454,plain,(
% 0.72/0.44 ($false = ((f4 @ sF17))) | ~spl27_79),
% 0.72/0.44 inference(avatar_component_clause,[],[f452])).
% 0.72/0.44 thf(f456,definition,(
% 0.72/0.44 spl27_80 <=> ($true = sF18)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_80])],[avatar_definition])).
% 0.72/0.44 thf(f457,plain,(
% 0.72/0.44 ($true != sF18) | spl27_80),
% 0.72/0.44 inference(avatar_component_clause,[],[f456])).
% 0.72/0.44 thf(f458,plain,(
% 0.72/0.44 ($true = sF18) | ~spl27_80),
% 0.72/0.44 inference(avatar_component_clause,[],[f456])).
% 0.72/0.44 thf(f459,plain,(
% 0.72/0.44 spl27_79 | spl27_80),
% 0.72/0.44 inference(avatar_split_clause,[],[f82,f456,f452])).
% 0.72/0.44 thf(f461,definition,(
% 0.72/0.44 spl27_81 <=> ($true = sF0)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_81])],[avatar_definition])).
% 0.72/0.44 thf(f462,plain,(
% 0.72/0.44 ($true != sF0) | spl27_81),
% 0.72/0.44 inference(avatar_component_clause,[],[f461])).
% 0.72/0.44 thf(f463,plain,(
% 0.72/0.44 ($true = sF0) | ~spl27_81),
% 0.72/0.44 inference(avatar_component_clause,[],[f461])).
% 0.72/0.44 thf(f465,definition,(
% 0.72/0.44 spl27_82 <=> (((f6 @ x)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_82])],[avatar_definition])).
% 0.72/0.44 thf(f467,plain,(
% 0.72/0.44 (((f6 @ x)) = $false) | ~spl27_82),
% 0.72/0.44 inference(avatar_component_clause,[],[f465])).
% 0.72/0.44 thf(f468,plain,(
% 0.72/0.44 spl27_81 | spl27_82),
% 0.72/0.44 inference(avatar_split_clause,[],[f85,f465,f461])).
% 0.72/0.44 thf(f470,definition,(
% 0.72/0.44 spl27_83 <=> (((f6 @ x)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_83])],[avatar_definition])).
% 0.72/0.44 thf(f472,plain,(
% 0.72/0.44 (((f6 @ x)) = $true) | ~spl27_83),
% 0.72/0.44 inference(avatar_component_clause,[],[f470])).
% 0.72/0.44 thf(f474,definition,(
% 0.72/0.44 spl27_84 <=> ($false = sF0)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_84])],[avatar_definition])).
% 0.72/0.44 thf(f476,plain,(
% 0.72/0.44 ($false = sF0) | ~spl27_84),
% 0.72/0.44 inference(avatar_component_clause,[],[f474])).
% 0.72/0.44 thf(f477,plain,(
% 0.72/0.44 spl27_83 | spl27_84),
% 0.72/0.44 inference(avatar_split_clause,[],[f84,f474,f470])).
% 0.72/0.44 thf(f479,definition,(
% 0.72/0.44 spl27_85 <=> ($true = sF19)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_85])],[avatar_definition])).
% 0.72/0.44 thf(f481,plain,(
% 0.72/0.44 ($true = sF19) | ~spl27_85),
% 0.72/0.44 inference(avatar_component_clause,[],[f479])).
% 0.72/0.44 thf(f483,definition,(
% 0.72/0.44 spl27_86 <=> (((f3 @ sF18)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_86])],[avatar_definition])).
% 0.72/0.44 thf(f484,plain,(
% 0.72/0.44 (((f3 @ sF18)) != $false) | spl27_86),
% 0.72/0.44 inference(avatar_component_clause,[],[f483])).
% 0.72/0.44 thf(f485,plain,(
% 0.72/0.44 (((f3 @ sF18)) = $false) | ~spl27_86),
% 0.72/0.44 inference(avatar_component_clause,[],[f483])).
% 0.72/0.44 thf(f486,plain,(
% 0.72/0.44 spl27_85 | spl27_86),
% 0.72/0.44 inference(avatar_split_clause,[],[f87,f483,f479])).
% 0.72/0.44 thf(f488,definition,(
% 0.72/0.44 spl27_87 <=> ($false = sF19)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_87])],[avatar_definition])).
% 0.72/0.44 thf(f490,plain,(
% 0.72/0.44 ($false = sF19) | ~spl27_87),
% 0.72/0.44 inference(avatar_component_clause,[],[f488])).
% 0.72/0.44 thf(f492,definition,(
% 0.72/0.44 spl27_88 <=> (((f3 @ sF18)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_88])],[avatar_definition])).
% 0.72/0.44 thf(f494,plain,(
% 0.72/0.44 (((f3 @ sF18)) = $true) | ~spl27_88),
% 0.72/0.44 inference(avatar_component_clause,[],[f492])).
% 0.72/0.44 thf(f495,plain,(
% 0.72/0.44 spl27_87 | spl27_88),
% 0.72/0.44 inference(avatar_split_clause,[],[f86,f492,f488])).
% 0.72/0.44 thf(f497,definition,(
% 0.72/0.44 spl27_89 <=> ($true = ((f0 @ sF25)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_89])],[avatar_definition])).
% 0.72/0.44 thf(f499,plain,(
% 0.72/0.44 ($true = ((f0 @ sF25))) | ~spl27_89),
% 0.72/0.44 inference(avatar_component_clause,[],[f497])).
% 0.72/0.44 thf(f500,plain,(
% 0.72/0.44 spl27_89 | spl27_1),
% 0.72/0.44 inference(avatar_split_clause,[],[f89,f101,f497])).
% 0.72/0.44 thf(f502,definition,(
% 0.72/0.44 spl27_90 <=> ($false = ((f0 @ sF25)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_90])],[avatar_definition])).
% 0.72/0.44 thf(f504,plain,(
% 0.72/0.44 ($false = ((f0 @ sF25))) | ~spl27_90),
% 0.72/0.44 inference(avatar_component_clause,[],[f502])).
% 0.72/0.44 thf(f505,plain,(
% 0.72/0.44 spl27_3 | spl27_90),
% 0.72/0.44 inference(avatar_split_clause,[],[f88,f502,f110])).
% 0.72/0.44 thf(f507,definition,(
% 0.72/0.44 spl27_91 <=> ($false = sF5)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_91])],[avatar_definition])).
% 0.72/0.44 thf(f509,plain,(
% 0.72/0.44 ($false = sF5) | ~spl27_91),
% 0.72/0.44 inference(avatar_component_clause,[],[f507])).
% 0.72/0.44 thf(f511,definition,(
% 0.72/0.44 spl27_92 <=> ($true = ((f3 @ sF4)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_92])],[avatar_definition])).
% 0.72/0.44 thf(f512,plain,(
% 0.72/0.44 ($true != ((f3 @ sF4))) | spl27_92),
% 0.72/0.44 inference(avatar_component_clause,[],[f511])).
% 0.72/0.44 thf(f513,plain,(
% 0.72/0.44 ($true = ((f3 @ sF4))) | ~spl27_92),
% 0.72/0.44 inference(avatar_component_clause,[],[f511])).
% 0.72/0.44 thf(f514,plain,(
% 0.72/0.44 spl27_91 | spl27_92),
% 0.72/0.44 inference(avatar_split_clause,[],[f91,f511,f507])).
% 0.72/0.44 thf(f516,definition,(
% 0.72/0.44 spl27_93 <=> ($true = sF5)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_93])],[avatar_definition])).
% 0.72/0.44 thf(f518,plain,(
% 0.72/0.44 ($true = sF5) | ~spl27_93),
% 0.72/0.44 inference(avatar_component_clause,[],[f516])).
% 0.72/0.44 thf(f520,definition,(
% 0.72/0.44 spl27_94 <=> ($false = ((f3 @ sF4)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_94])],[avatar_definition])).
% 0.72/0.44 thf(f522,plain,(
% 0.72/0.44 ($false = ((f3 @ sF4))) | ~spl27_94),
% 0.72/0.44 inference(avatar_component_clause,[],[f520])).
% 0.72/0.44 thf(f523,plain,(
% 0.72/0.44 spl27_93 | spl27_94),
% 0.72/0.44 inference(avatar_split_clause,[],[f90,f520,f516])).
% 0.72/0.44 thf(f525,definition,(
% 0.72/0.44 spl27_95 <=> ($true = sF1)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_95])],[avatar_definition])).
% 0.72/0.44 thf(f526,plain,(
% 0.72/0.44 ($true != sF1) | spl27_95),
% 0.72/0.44 inference(avatar_component_clause,[],[f525])).
% 0.72/0.44 thf(f527,plain,(
% 0.72/0.44 ($true = sF1) | ~spl27_95),
% 0.72/0.44 inference(avatar_component_clause,[],[f525])).
% 0.72/0.44 thf(f529,definition,(
% 0.72/0.44 spl27_96 <=> (((f5 @ sF0)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_96])],[avatar_definition])).
% 0.72/0.44 thf(f530,plain,(
% 0.72/0.44 (((f5 @ sF0)) != $false) | spl27_96),
% 0.72/0.44 inference(avatar_component_clause,[],[f529])).
% 0.72/0.44 thf(f531,plain,(
% 0.72/0.44 (((f5 @ sF0)) = $false) | ~spl27_96),
% 0.72/0.44 inference(avatar_component_clause,[],[f529])).
% 0.72/0.44 thf(f532,plain,(
% 0.72/0.44 spl27_95 | spl27_96),
% 0.72/0.44 inference(avatar_split_clause,[],[f93,f529,f525])).
% 0.72/0.44 thf(f534,definition,(
% 0.72/0.44 spl27_97 <=> ($false = sF1)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_97])],[avatar_definition])).
% 0.72/0.44 thf(f536,plain,(
% 0.72/0.44 ($false = sF1) | ~spl27_97),
% 0.72/0.44 inference(avatar_component_clause,[],[f534])).
% 0.72/0.44 thf(f538,definition,(
% 0.72/0.44 spl27_98 <=> ($true = ((f5 @ sF0)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_98])],[avatar_definition])).
% 0.72/0.44 thf(f540,plain,(
% 0.72/0.44 ($true = ((f5 @ sF0))) | ~spl27_98),
% 0.72/0.44 inference(avatar_component_clause,[],[f538])).
% 0.72/0.44 thf(f541,plain,(
% 0.72/0.44 spl27_97 | spl27_98),
% 0.72/0.44 inference(avatar_split_clause,[],[f92,f538,f534])).
% 0.72/0.44 thf(f543,definition,(
% 0.72/0.44 spl27_99 <=> ($true = ((f0 @ sF11)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_99])],[avatar_definition])).
% 0.72/0.44 thf(f545,plain,(
% 0.72/0.44 ($true = ((f0 @ sF11))) | ~spl27_99),
% 0.72/0.44 inference(avatar_component_clause,[],[f543])).
% 0.72/0.44 thf(f546,plain,(
% 0.72/0.44 spl27_99 | spl27_2),
% 0.72/0.44 inference(avatar_split_clause,[],[f95,f105,f543])).
% 0.72/0.44 thf(f548,definition,(
% 0.72/0.44 spl27_100 <=> ($false = ((f0 @ sF11)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_100])],[avatar_definition])).
% 0.72/0.44 thf(f550,plain,(
% 0.72/0.44 ($false = ((f0 @ sF11))) | ~spl27_100),
% 0.72/0.44 inference(avatar_component_clause,[],[f548])).
% 0.72/0.44 thf(f551,plain,(
% 0.72/0.44 spl27_100 | spl27_4),
% 0.72/0.44 inference(avatar_split_clause,[],[f94,f114,f548])).
% 0.72/0.44 thf(f553,definition,(
% 0.72/0.44 spl27_101 <=> ($true = sF8)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_101])],[avatar_definition])).
% 0.72/0.44 thf(f555,plain,(
% 0.72/0.44 ($true = sF8) | ~spl27_101),
% 0.72/0.44 inference(avatar_component_clause,[],[f553])).
% 0.72/0.44 thf(f557,definition,(
% 0.72/0.44 spl27_102 <=> ($false = ((f2 @ sF7)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_102])],[avatar_definition])).
% 0.72/0.44 thf(f558,plain,(
% 0.72/0.44 ($false != ((f2 @ sF7))) | spl27_102),
% 0.72/0.44 inference(avatar_component_clause,[],[f557])).
% 0.72/0.44 thf(f559,plain,(
% 0.72/0.44 ($false = ((f2 @ sF7))) | ~spl27_102),
% 0.72/0.44 inference(avatar_component_clause,[],[f557])).
% 0.72/0.44 thf(f560,plain,(
% 0.72/0.44 spl27_101 | spl27_102),
% 0.72/0.44 inference(avatar_split_clause,[],[f97,f557,f553])).
% 0.72/0.44 thf(f562,definition,(
% 0.72/0.44 spl27_103 <=> ($true = ((f2 @ sF7)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_103])],[avatar_definition])).
% 0.72/0.44 thf(f563,plain,(
% 0.72/0.44 ($true != ((f2 @ sF7))) | spl27_103),
% 0.72/0.44 inference(avatar_component_clause,[],[f562])).
% 0.72/0.44 thf(f564,plain,(
% 0.72/0.44 ($true = ((f2 @ sF7))) | ~spl27_103),
% 0.72/0.44 inference(avatar_component_clause,[],[f562])).
% 0.72/0.44 thf(f566,definition,(
% 0.72/0.44 spl27_104 <=> ($false = sF8)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_104])],[avatar_definition])).
% 0.72/0.44 thf(f568,plain,(
% 0.72/0.44 ($false = sF8) | ~spl27_104),
% 0.72/0.44 inference(avatar_component_clause,[],[f566])).
% 0.72/0.44 thf(f569,plain,(
% 0.72/0.44 spl27_103 | spl27_104),
% 0.72/0.44 inference(avatar_split_clause,[],[f96,f566,f562])).
% 0.72/0.44 thf(f571,definition,(
% 0.72/0.44 spl27_105 <=> ($true = sF2)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_105])],[avatar_definition])).
% 0.72/0.44 thf(f572,plain,(
% 0.72/0.44 ($true != sF2) | spl27_105),
% 0.72/0.44 inference(avatar_component_clause,[],[f571])).
% 0.72/0.44 thf(f573,plain,(
% 0.72/0.44 ($true = sF2) | ~spl27_105),
% 0.72/0.44 inference(avatar_component_clause,[],[f571])).
% 0.72/0.44 thf(f575,definition,(
% 0.72/0.44 spl27_106 <=> ($false = ((f5 @ sF1)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_106])],[avatar_definition])).
% 0.72/0.44 thf(f577,plain,(
% 0.72/0.44 ($false = ((f5 @ sF1))) | ~spl27_106),
% 0.72/0.44 inference(avatar_component_clause,[],[f575])).
% 0.72/0.44 thf(f578,plain,(
% 0.72/0.44 spl27_105 | spl27_106),
% 0.72/0.44 inference(avatar_split_clause,[],[f99,f575,f571])).
% 0.72/0.44 thf(f580,definition,(
% 0.72/0.44 spl27_107 <=> ($false = sF2)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_107])],[avatar_definition])).
% 0.72/0.44 thf(f582,plain,(
% 0.72/0.44 ($false = sF2) | ~spl27_107),
% 0.72/0.44 inference(avatar_component_clause,[],[f580])).
% 0.72/0.44 thf(f584,definition,(
% 0.72/0.44 spl27_108 <=> ($true = ((f5 @ sF1)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_108])],[avatar_definition])).
% 0.72/0.44 thf(f586,plain,(
% 0.72/0.44 ($true = ((f5 @ sF1))) | ~spl27_108),
% 0.72/0.44 inference(avatar_component_clause,[],[f584])).
% 0.72/0.44 thf(f587,plain,(
% 0.72/0.44 spl27_107 | spl27_108),
% 0.72/0.44 inference(avatar_split_clause,[],[f98,f584,f580])).
% 0.72/0.44 thf(f588,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_2 | ~spl27_4)),
% 0.72/0.44 inference(forward_demodulation,[],[f116,f107])).
% 0.72/0.44 thf(f589,plain,(
% 0.72/0.44 $false | (~spl27_2 | ~spl27_4)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f588])).
% 0.72/0.44 thf(f590,plain,(
% 0.72/0.44 ~spl27_2 | ~spl27_4),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f589])).
% 0.72/0.44 thf(f615,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_37 | ~spl27_39)),
% 0.72/0.44 inference(forward_demodulation,[],[f274,f265])).
% 0.72/0.44 thf(f616,plain,(
% 0.72/0.44 $false | (~spl27_37 | ~spl27_39)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f615])).
% 0.72/0.44 thf(f617,plain,(
% 0.72/0.44 ~spl27_37 | ~spl27_39),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f616])).
% 0.72/0.44 thf(f618,plain,(
% 0.72/0.44 ($true != $true) | (sF3 = $false) | spl27_37),
% 0.72/0.44 inference(constrained_superposition,[],[f264,f6])).
% 0.72/0.44 thf(f619,plain,(
% 0.72/0.44 (sF3 = $false) | spl27_37),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f618])).
% 0.72/0.44 thf(f620,plain,(
% 0.72/0.44 spl27_39 | spl27_37),
% 0.72/0.44 inference(avatar_split_clause,[],[f619,f263,f272])).
% 0.72/0.44 thf(f631,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_61 | ~spl27_63)),
% 0.72/0.44 inference(forward_demodulation,[],[f382,f373])).
% 0.72/0.44 thf(f632,plain,(
% 0.72/0.44 $false | (~spl27_61 | ~spl27_63)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f631])).
% 0.72/0.44 thf(f633,plain,(
% 0.72/0.44 ~spl27_61 | ~spl27_63),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f632])).
% 0.72/0.44 thf(f634,plain,(
% 0.72/0.44 ($false = sF21) | ($true != $true) | spl27_61),
% 0.72/0.44 inference(constrained_superposition,[],[f372,f6])).
% 0.72/0.44 thf(f635,plain,(
% 0.72/0.44 ($false = sF21) | spl27_61),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f634])).
% 0.72/0.44 thf(f636,plain,(
% 0.72/0.44 spl27_63 | spl27_61),
% 0.72/0.44 inference(avatar_split_clause,[],[f635,f371,f380])).
% 0.72/0.44 thf(f647,plain,(
% 0.72/0.44 (((f3 @ $false)) = $false) | (~spl27_77 | ~spl27_86)),
% 0.72/0.44 inference(forward_demodulation,[],[f485,f445])).
% 0.72/0.44 thf(f665,plain,(
% 0.72/0.44 ($true != $true) | ($false = sF1) | spl27_95),
% 0.72/0.44 inference(constrained_superposition,[],[f526,f6])).
% 0.72/0.44 thf(f666,plain,(
% 0.72/0.44 ($false = sF1) | spl27_95),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f665])).
% 0.72/0.44 thf(f667,plain,(
% 0.72/0.44 spl27_97 | spl27_95),
% 0.72/0.44 inference(avatar_split_clause,[],[f666,f525,f534])).
% 0.72/0.44 thf(f674,plain,(
% 0.72/0.44 ($false = ((f5 @ $false))) | (~spl27_97 | ~spl27_106)),
% 0.72/0.44 inference(forward_demodulation,[],[f577,f536])).
% 0.72/0.44 thf(f675,plain,(
% 0.72/0.44 ($true != $true) | ($false = sF2) | spl27_105),
% 0.72/0.44 inference(constrained_superposition,[],[f572,f6])).
% 0.72/0.44 thf(f676,plain,(
% 0.72/0.44 ($false = sF2) | spl27_105),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f675])).
% 0.72/0.44 thf(f677,plain,(
% 0.72/0.44 spl27_107 | spl27_105),
% 0.72/0.44 inference(avatar_split_clause,[],[f676,f571,f580])).
% 0.72/0.44 thf(f681,plain,(
% 0.72/0.44 ($false = ((f2 @ $false))) | (~spl27_5 | ~spl27_87)),
% 0.72/0.44 inference(forward_demodulation,[],[f121,f490])).
% 0.72/0.44 thf(f682,plain,(
% 0.72/0.44 ($true = ((f2 @ $false))) | (~spl27_7 | ~spl27_87)),
% 0.72/0.44 inference(forward_demodulation,[],[f130,f490])).
% 0.72/0.44 thf(f683,plain,(
% 0.72/0.44 ($true = ((f4 @ $true))) | (~spl27_9 | ~spl27_69)),
% 0.72/0.44 inference(forward_demodulation,[],[f139,f409])).
% 0.72/0.44 thf(f684,plain,(
% 0.72/0.44 ($false = ((f4 @ $true))) | (~spl27_11 | ~spl27_69)),
% 0.72/0.44 inference(forward_demodulation,[],[f148,f409])).
% 0.72/0.44 thf(f685,plain,(
% 0.72/0.44 (((f3 @ $true)) = $true) | (~spl27_13 | ~spl27_51)),
% 0.72/0.44 inference(forward_demodulation,[],[f157,f328])).
% 0.72/0.44 thf(f687,plain,(
% 0.72/0.44 (((f6 @ $true)) = $true) | (~spl27_17 | ~spl27_81)),
% 0.72/0.44 inference(forward_demodulation,[],[f175,f463])).
% 0.72/0.44 thf(f689,plain,(
% 0.72/0.44 ($true = ((f1 @ $true))) | (~spl27_21 | ~spl27_67)),
% 0.72/0.44 inference(forward_demodulation,[],[f193,f400])).
% 0.72/0.44 thf(f690,plain,(
% 0.72/0.44 ($false = ((f1 @ $true))) | (~spl27_23 | ~spl27_67)),
% 0.72/0.44 inference(forward_demodulation,[],[f202,f400])).
% 0.72/0.44 thf(f695,definition,(
% 0.72/0.44 spl27_109 <=> ($true = ((f4 @ $true)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_109])],[avatar_definition])).
% 0.72/0.44 thf(f697,plain,(
% 0.72/0.44 ($true = ((f4 @ $true))) | ~spl27_109),
% 0.72/0.44 inference(avatar_component_clause,[],[f695])).
% 0.72/0.44 thf(f712,definition,(
% 0.72/0.44 spl27_110 <=> ($false = ((f4 @ $true)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_110])],[avatar_definition])).
% 0.72/0.44 thf(f714,plain,(
% 0.72/0.44 ($false = ((f4 @ $true))) | ~spl27_110),
% 0.72/0.44 inference(avatar_component_clause,[],[f712])).
% 0.72/0.44 thf(f720,plain,(
% 0.72/0.44 ($false = ((f5 @ $false))) | (~spl27_38 | ~spl27_107)),
% 0.72/0.44 inference(forward_demodulation,[],[f269,f582])).
% 0.72/0.44 thf(f723,definition,(
% 0.72/0.44 spl27_111 <=> (((f6 @ $true)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_111])],[avatar_definition])).
% 0.72/0.44 thf(f725,plain,(
% 0.72/0.44 (((f6 @ $true)) = $true) | ~spl27_111),
% 0.72/0.44 inference(avatar_component_clause,[],[f723])).
% 0.72/0.44 thf(f730,plain,(
% 0.72/0.44 ($true = ((f4 @ $false))) | (~spl27_39 | ~spl27_45)),
% 0.72/0.44 inference(forward_demodulation,[],[f301,f274])).
% 0.72/0.44 thf(f731,plain,(
% 0.72/0.44 ($false = ((f4 @ $false))) | (~spl27_39 | ~spl27_47)),
% 0.72/0.44 inference(forward_demodulation,[],[f310,f274])).
% 0.72/0.44 thf(f732,plain,(
% 0.72/0.44 (((f3 @ $true)) = $true) | (~spl27_49 | ~spl27_93)),
% 0.72/0.44 inference(forward_demodulation,[],[f319,f518])).
% 0.72/0.44 thf(f733,plain,(
% 0.72/0.44 (sF10 = $false) | ($true = ((f1 @ $true))) | ~spl27_54),
% 0.72/0.44 inference(constrained_superposition,[],[f341,f6])).
% 0.72/0.44 thf(f735,definition,(
% 0.72/0.44 spl27_112 <=> ($true = ((f1 @ $true)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_112])],[avatar_definition])).
% 0.72/0.44 thf(f737,plain,(
% 0.72/0.44 ($true = ((f1 @ $true))) | ~spl27_112),
% 0.72/0.44 inference(avatar_component_clause,[],[f735])).
% 0.72/0.44 thf(f738,plain,(
% 0.72/0.44 spl27_22 | spl27_112 | ~spl27_54),
% 0.72/0.44 inference(avatar_split_clause,[],[f733,f339,f735,f195])).
% 0.72/0.44 thf(f747,definition,(
% 0.72/0.44 spl27_113 <=> (((f2 @ $true)) = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_113])],[avatar_definition])).
% 0.72/0.44 thf(f749,plain,(
% 0.72/0.44 (((f2 @ $true)) = $false) | ~spl27_113),
% 0.72/0.44 inference(avatar_component_clause,[],[f747])).
% 0.72/0.44 thf(f751,plain,(
% 0.72/0.44 ($true = ((f1 @ $true))) | (~spl27_65 | ~spl27_101)),
% 0.72/0.44 inference(forward_demodulation,[],[f391,f555])).
% 0.72/0.44 thf(f752,plain,(
% 0.72/0.44 spl27_112 | ~spl27_65 | ~spl27_101),
% 0.72/0.44 inference(avatar_split_clause,[],[f751,f553,f389,f735])).
% 0.72/0.44 thf(f753,plain,(
% 0.72/0.44 (((f5 @ $true)) = $true) | (~spl27_43 | ~spl27_71)),
% 0.72/0.44 inference(forward_demodulation,[],[f418,f292])).
% 0.72/0.44 thf(f755,plain,(
% 0.72/0.44 ($false = ((f4 @ $false))) | (~spl27_33 | ~spl27_79)),
% 0.72/0.44 inference(forward_demodulation,[],[f454,f247])).
% 0.72/0.44 thf(f756,plain,(
% 0.72/0.44 (((f6 @ $true)) = $true) | (x = $false) | ~spl27_83),
% 0.72/0.44 inference(constrained_superposition,[],[f472,f6])).
% 0.72/0.44 thf(f758,definition,(
% 0.72/0.44 spl27_114 <=> (x = $false)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_114])],[avatar_definition])).
% 0.72/0.44 thf(f760,plain,(
% 0.72/0.44 (x = $false) | ~spl27_114),
% 0.72/0.44 inference(avatar_component_clause,[],[f758])).
% 0.72/0.44 thf(f761,plain,(
% 0.72/0.44 spl27_114 | spl27_111 | ~spl27_83),
% 0.72/0.44 inference(avatar_split_clause,[],[f756,f470,f723,f758])).
% 0.72/0.44 thf(f768,definition,(
% 0.72/0.44 spl27_115 <=> (((f3 @ $true)) = $true)),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_115])],[avatar_definition])).
% 0.72/0.44 thf(f770,plain,(
% 0.72/0.44 (((f3 @ $true)) = $true) | ~spl27_115),
% 0.72/0.44 inference(avatar_component_clause,[],[f768])).
% 0.72/0.44 thf(f772,plain,(
% 0.72/0.44 ($false = ((f0 @ $true))) | (~spl27_55 | ~spl27_100)),
% 0.72/0.44 inference(forward_demodulation,[],[f550,f346])).
% 0.72/0.44 thf(f775,definition,(
% 0.72/0.44 spl27_116 <=> ($true = ((f2 @ $true)))),
% 0.72/0.44 introduced(definition,[new_symbols(definition,[spl27_116])],[avatar_definition])).
% 0.72/0.44 thf(f788,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_5 | ~spl27_7 | ~spl27_87)),
% 0.72/0.44 inference(forward_demodulation,[],[f682,f681])).
% 0.72/0.44 thf(f789,plain,(
% 0.72/0.44 $false | (~spl27_5 | ~spl27_7 | ~spl27_87)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f788])).
% 0.72/0.44 thf(f790,plain,(
% 0.72/0.44 ~spl27_5 | ~spl27_7 | ~spl27_87),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f789])).
% 0.72/0.44 thf(f792,plain,(
% 0.72/0.44 (((f2 @ $true)) = $false) | (~spl27_6 | ~spl27_62)),
% 0.72/0.44 inference(constrained_superposition,[],[f377,f125])).
% 0.72/0.44 thf(f793,plain,(
% 0.72/0.44 spl27_113 | ~spl27_6 | ~spl27_62),
% 0.72/0.44 inference(avatar_split_clause,[],[f792,f375,f123,f747])).
% 0.72/0.44 thf(f794,plain,(
% 0.72/0.44 spl27_109 | ~spl27_9 | ~spl27_69),
% 0.72/0.44 inference(avatar_split_clause,[],[f683,f407,f137,f695])).
% 0.72/0.44 thf(f795,plain,(
% 0.72/0.44 ($true != ((f4 @ $true))) | (spl27_9 | ~spl27_69)),
% 0.72/0.44 inference(forward_demodulation,[],[f138,f409])).
% 0.72/0.44 thf(f796,plain,(
% 0.72/0.44 ~spl27_109 | spl27_9 | ~spl27_69),
% 0.72/0.44 inference(avatar_split_clause,[],[f795,f407,f137,f695])).
% 0.72/0.44 thf(f797,plain,(
% 0.72/0.44 spl27_110 | ~spl27_11 | ~spl27_69),
% 0.72/0.44 inference(avatar_split_clause,[],[f684,f407,f146,f712])).
% 0.72/0.44 thf(f803,plain,(
% 0.72/0.44 (((f5 @ $true)) = $false) | (~spl27_43 | ~spl27_70)),
% 0.72/0.44 inference(forward_demodulation,[],[f413,f292])).
% 0.72/0.44 thf(f805,plain,(
% 0.72/0.44 (sF15 = $false) | ($true != $true) | spl27_69),
% 0.72/0.44 inference(constrained_superposition,[],[f408,f6])).
% 0.72/0.44 thf(f806,plain,(
% 0.72/0.44 (sF15 = $false) | spl27_69),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f805])).
% 0.72/0.44 thf(f807,plain,(
% 0.72/0.44 spl27_72 | spl27_69),
% 0.72/0.44 inference(avatar_split_clause,[],[f806,f407,f420])).
% 0.72/0.44 thf(f812,plain,(
% 0.72/0.44 ($false = ((f4 @ $false))) | (~spl27_11 | ~spl27_72)),
% 0.72/0.44 inference(forward_demodulation,[],[f148,f422])).
% 0.72/0.44 thf(f813,plain,(
% 0.72/0.44 spl27_115 | ~spl27_13 | ~spl27_51),
% 0.72/0.44 inference(avatar_split_clause,[],[f685,f326,f155,f768])).
% 0.72/0.44 thf(f817,plain,(
% 0.72/0.44 spl27_111 | ~spl27_17 | ~spl27_81),
% 0.72/0.44 inference(avatar_split_clause,[],[f687,f461,f173,f723])).
% 0.72/0.44 thf(f821,plain,(
% 0.72/0.44 spl27_112 | ~spl27_21 | ~spl27_67),
% 0.72/0.44 inference(avatar_split_clause,[],[f689,f398,f191,f735])).
% 0.72/0.44 thf(f841,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_39 | ~spl27_45 | ~spl27_47)),
% 0.72/0.44 inference(forward_demodulation,[],[f731,f730])).
% 0.72/0.44 thf(f842,plain,(
% 0.72/0.44 $false | (~spl27_39 | ~spl27_45 | ~spl27_47)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f841])).
% 0.72/0.44 thf(f843,plain,(
% 0.72/0.44 ~spl27_39 | ~spl27_45 | ~spl27_47),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f842])).
% 0.72/0.44 thf(f852,plain,(
% 0.72/0.44 (sF6 = $false) | ($true != $true) | spl27_51),
% 0.72/0.44 inference(constrained_superposition,[],[f327,f6])).
% 0.72/0.44 thf(f853,plain,(
% 0.72/0.44 (sF6 = $false) | spl27_51),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f852])).
% 0.72/0.44 thf(f854,plain,(
% 0.72/0.44 spl27_50 | spl27_51),
% 0.72/0.44 inference(avatar_split_clause,[],[f853,f326,f321])).
% 0.72/0.44 thf(f858,plain,(
% 0.72/0.44 (((f3 @ $false)) = $true) | (~spl27_13 | ~spl27_50)),
% 0.72/0.44 inference(forward_demodulation,[],[f157,f323])).
% 0.72/0.44 thf(f859,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_13 | ~spl27_50 | ~spl27_77 | ~spl27_86)),
% 0.72/0.44 inference(forward_demodulation,[],[f858,f647])).
% 0.72/0.44 thf(f860,plain,(
% 0.72/0.44 $false | (~spl27_13 | ~spl27_50 | ~spl27_77 | ~spl27_86)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f859])).
% 0.72/0.44 thf(f861,plain,(
% 0.72/0.44 ~spl27_13 | ~spl27_50 | ~spl27_77 | ~spl27_86),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f860])).
% 0.72/0.44 thf(f862,plain,(
% 0.72/0.44 ($true = ((f5 @ $false))) | (~spl27_40 | ~spl27_107)),
% 0.72/0.44 inference(forward_demodulation,[],[f278,f582])).
% 0.72/0.44 thf(f863,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_40 | ~spl27_97 | ~spl27_106 | ~spl27_107)),
% 0.72/0.44 inference(forward_demodulation,[],[f862,f674])).
% 0.72/0.44 thf(f864,plain,(
% 0.72/0.44 $false | (~spl27_40 | ~spl27_97 | ~spl27_106 | ~spl27_107)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f863])).
% 0.72/0.44 thf(f865,plain,(
% 0.72/0.44 ~spl27_40 | ~spl27_97 | ~spl27_106 | ~spl27_107),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f864])).
% 0.72/0.44 thf(f891,plain,(
% 0.72/0.44 (((f3 @ $true)) != $false) | (spl27_15 | ~spl27_51)),
% 0.72/0.44 inference(forward_demodulation,[],[f165,f328])).
% 0.72/0.44 thf(f894,plain,(
% 0.72/0.44 ($true = ((f4 @ $false))) | (~spl27_39 | ~spl27_45)),
% 0.72/0.44 inference(forward_demodulation,[],[f301,f274])).
% 0.72/0.44 thf(f896,plain,(
% 0.72/0.44 (((f5 @ $true)) = $false) | (~spl27_81 | ~spl27_96)),
% 0.72/0.44 inference(forward_demodulation,[],[f531,f463])).
% 0.72/0.44 thf(f901,plain,(
% 0.72/0.44 spl27_115 | ~spl27_49 | ~spl27_93),
% 0.72/0.44 inference(avatar_split_clause,[],[f732,f516,f317,f768])).
% 0.72/0.44 thf(f916,plain,(
% 0.72/0.44 ($true = ((f0 @ $false))) | (~spl27_29 | ~spl27_89)),
% 0.72/0.44 inference(forward_demodulation,[],[f499,f229])).
% 0.72/0.44 thf(f921,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_43 | ~spl27_70 | ~spl27_71)),
% 0.72/0.44 inference(forward_demodulation,[],[f803,f753])).
% 0.72/0.44 thf(f922,plain,(
% 0.72/0.44 $false | (~spl27_43 | ~spl27_70 | ~spl27_71)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f921])).
% 0.72/0.44 thf(f923,plain,(
% 0.72/0.44 ~spl27_43 | ~spl27_70 | ~spl27_71),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f922])).
% 0.72/0.44 thf(f941,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_33 | ~spl27_39 | ~spl27_45 | ~spl27_79)),
% 0.72/0.44 inference(forward_demodulation,[],[f894,f755])).
% 0.72/0.44 thf(f942,plain,(
% 0.72/0.44 $false | (~spl27_33 | ~spl27_39 | ~spl27_45 | ~spl27_79)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f941])).
% 0.72/0.44 thf(f943,plain,(
% 0.72/0.44 ~spl27_33 | ~spl27_39 | ~spl27_45 | ~spl27_79),
% 0.72/0.44 inference(avatar_contradiction_clause,[],[f942])).
% 0.72/0.44 thf(f944,plain,(
% 0.72/0.44 ($true = $false) | (~spl27_77 | ~spl27_80)),
% 0.72/0.44 inference(forward_demodulation,[],[f458,f445])).
% 0.72/0.44 thf(f945,plain,(
% 0.72/0.44 $false | (~spl27_77 | ~spl27_80)),
% 0.72/0.44 inference(trivial_inequality_removal,[],[f944])).
% 0.72/0.45 thf(f946,plain,(
% 0.72/0.45 ~spl27_77 | ~spl27_80),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f945])).
% 0.72/0.45 thf(f960,plain,(
% 0.72/0.45 (((f3 @ $true)) = $false) | (~spl27_80 | ~spl27_86)),
% 0.72/0.45 inference(forward_demodulation,[],[f485,f458])).
% 0.72/0.45 thf(f961,plain,(
% 0.72/0.45 $false | (spl27_15 | ~spl27_51 | ~spl27_80 | ~spl27_86)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f960,f891])).
% 0.72/0.45 thf(f962,plain,(
% 0.72/0.45 spl27_15 | ~spl27_51 | ~spl27_80 | ~spl27_86),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f961])).
% 0.72/0.45 thf(f985,plain,(
% 0.72/0.45 ($true = ((f4 @ $false))) | (~spl27_9 | ~spl27_72)),
% 0.72/0.45 inference(forward_demodulation,[],[f139,f422])).
% 0.72/0.45 thf(f986,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_9 | ~spl27_11 | ~spl27_72)),
% 0.72/0.45 inference(forward_demodulation,[],[f985,f812])).
% 0.72/0.45 thf(f987,plain,(
% 0.72/0.45 $false | (~spl27_9 | ~spl27_11 | ~spl27_72)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f986])).
% 0.72/0.45 thf(f988,plain,(
% 0.72/0.45 ~spl27_9 | ~spl27_11 | ~spl27_72),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f987])).
% 0.72/0.45 thf(f989,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_41 | ~spl27_44)),
% 0.72/0.45 inference(forward_demodulation,[],[f296,f283])).
% 0.72/0.45 thf(f990,plain,(
% 0.72/0.45 $false | (~spl27_41 | ~spl27_44)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f989])).
% 0.72/0.45 thf(f991,plain,(
% 0.72/0.45 ~spl27_41 | ~spl27_44),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f990])).
% 0.72/0.45 thf(f1000,plain,(
% 0.72/0.45 ($false = ((f5 @ $false))) | (~spl27_42 | ~spl27_70)),
% 0.72/0.45 inference(forward_demodulation,[],[f413,f287])).
% 0.72/0.45 thf(f1001,plain,(
% 0.72/0.45 ($true = ((f5 @ $false))) | (~spl27_42 | ~spl27_71)),
% 0.72/0.45 inference(forward_demodulation,[],[f418,f287])).
% 0.72/0.45 thf(f1002,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_38 | ~spl27_42 | ~spl27_71 | ~spl27_107)),
% 0.72/0.45 inference(forward_demodulation,[],[f1001,f720])).
% 0.72/0.45 thf(f1003,plain,(
% 0.72/0.45 $false | (~spl27_38 | ~spl27_42 | ~spl27_71 | ~spl27_107)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1002])).
% 0.72/0.45 thf(f1004,plain,(
% 0.72/0.45 ~spl27_38 | ~spl27_42 | ~spl27_71 | ~spl27_107),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1003])).
% 0.72/0.45 thf(f1007,plain,(
% 0.72/0.45 (((f5 @ $true)) = $false) | (~spl27_38 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f269,f573])).
% 0.72/0.45 thf(f1018,plain,(
% 0.72/0.45 (((f3 @ $true)) = $false) | (~spl27_52 | ~spl27_93)),
% 0.72/0.45 inference(forward_demodulation,[],[f332,f518])).
% 0.72/0.45 thf(f1030,plain,(
% 0.72/0.45 (((f3 @ $true)) = $true) | (~spl27_48 | ~spl27_92)),
% 0.72/0.45 inference(constrained_superposition,[],[f513,f314])).
% 0.72/0.45 thf(f1031,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_48 | ~spl27_80 | ~spl27_86 | ~spl27_92)),
% 0.72/0.45 inference(forward_demodulation,[],[f1030,f960])).
% 0.72/0.45 thf(f1032,plain,(
% 0.72/0.45 $false | (~spl27_48 | ~spl27_80 | ~spl27_86 | ~spl27_92)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1031])).
% 0.72/0.45 thf(f1033,plain,(
% 0.72/0.45 ~spl27_48 | ~spl27_80 | ~spl27_86 | ~spl27_92),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1032])).
% 0.72/0.45 thf(f1034,plain,(
% 0.72/0.45 (((f3 @ $true)) != $false) | (~spl27_80 | spl27_86)),
% 0.72/0.45 inference(forward_demodulation,[],[f484,f458])).
% 0.72/0.45 thf(f1035,plain,(
% 0.72/0.45 (((f3 @ $true)) = $true) | (~spl27_80 | ~spl27_88)),
% 0.72/0.45 inference(forward_demodulation,[],[f494,f458])).
% 0.72/0.45 thf(f1036,plain,(
% 0.72/0.45 spl27_115 | ~spl27_80 | ~spl27_88),
% 0.72/0.45 inference(avatar_split_clause,[],[f1035,f492,f456,f768])).
% 0.72/0.45 thf(f1041,plain,(
% 0.72/0.45 (((f2 @ $true)) != $false) | (spl27_5 | ~spl27_85)),
% 0.72/0.45 inference(forward_demodulation,[],[f120,f481])).
% 0.72/0.45 thf(f1042,plain,(
% 0.72/0.45 ~spl27_113 | spl27_5 | ~spl27_85),
% 0.72/0.45 inference(avatar_split_clause,[],[f1041,f479,f119,f747])).
% 0.72/0.45 thf(f1043,plain,(
% 0.72/0.45 (((f2 @ $true)) = $false) | (~spl27_5 | ~spl27_85)),
% 0.72/0.45 inference(forward_demodulation,[],[f121,f481])).
% 0.72/0.45 thf(f1044,plain,(
% 0.72/0.45 spl27_113 | ~spl27_5 | ~spl27_85),
% 0.72/0.45 inference(avatar_split_clause,[],[f1043,f479,f119,f747])).
% 0.72/0.45 thf(f1045,plain,(
% 0.72/0.45 ($true = ((f2 @ $true))) | (~spl27_7 | ~spl27_85)),
% 0.72/0.45 inference(forward_demodulation,[],[f130,f481])).
% 0.72/0.45 thf(f1046,plain,(
% 0.72/0.45 spl27_116 | ~spl27_7 | ~spl27_85),
% 0.72/0.45 inference(avatar_split_clause,[],[f1045,f479,f128,f775])).
% 0.72/0.45 thf(f1047,plain,(
% 0.72/0.45 (((f3 @ $false)) = $true) | (~spl27_13 | ~spl27_50)),
% 0.72/0.45 inference(forward_demodulation,[],[f157,f323])).
% 0.72/0.45 thf(f1048,plain,(
% 0.72/0.45 (((f3 @ $false)) = $false) | (~spl27_15 | ~spl27_50)),
% 0.72/0.45 inference(forward_demodulation,[],[f166,f323])).
% 0.72/0.45 thf(f1062,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_42 | ~spl27_70 | ~spl27_71)),
% 0.72/0.45 inference(forward_demodulation,[],[f1001,f1000])).
% 0.72/0.45 thf(f1063,plain,(
% 0.72/0.45 $false | (~spl27_42 | ~spl27_70 | ~spl27_71)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1062])).
% 0.72/0.45 thf(f1064,plain,(
% 0.72/0.45 ~spl27_42 | ~spl27_70 | ~spl27_71),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1063])).
% 0.72/0.45 thf(f1065,plain,(
% 0.72/0.45 (((f6 @ $false)) = $true) | (~spl27_18 | ~spl27_41)),
% 0.72/0.45 inference(forward_demodulation,[],[f283,f179])).
% 0.72/0.45 thf(f1067,plain,(
% 0.72/0.45 (((f5 @ $true)) != $false) | (~spl27_43 | spl27_70)),
% 0.72/0.45 inference(forward_demodulation,[],[f412,f292])).
% 0.72/0.45 thf(f1068,plain,(
% 0.72/0.45 $false | (~spl27_43 | spl27_70 | ~spl27_81 | ~spl27_96)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1067,f896])).
% 0.72/0.45 thf(f1069,plain,(
% 0.72/0.45 ~spl27_43 | spl27_70 | ~spl27_81 | ~spl27_96),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1068])).
% 0.72/0.45 thf(f1070,plain,(
% 0.72/0.45 (((f5 @ $true)) = $true) | (~spl27_81 | ~spl27_98)),
% 0.72/0.45 inference(forward_demodulation,[],[f540,f463])).
% 0.72/0.45 thf(f1083,plain,(
% 0.72/0.45 $false | (~spl27_52 | ~spl27_80 | spl27_86 | ~spl27_93)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1034,f1018])).
% 0.72/0.45 thf(f1084,plain,(
% 0.72/0.45 ~spl27_52 | ~spl27_80 | spl27_86 | ~spl27_93),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1083])).
% 0.72/0.45 thf(f1085,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_92 | ~spl27_94)),
% 0.72/0.45 inference(forward_demodulation,[],[f522,f513])).
% 0.72/0.45 thf(f1086,plain,(
% 0.72/0.45 $false | (~spl27_92 | ~spl27_94)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1085])).
% 0.72/0.45 thf(f1087,plain,(
% 0.72/0.45 ~spl27_92 | ~spl27_94),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1086])).
% 0.72/0.45 thf(f1089,plain,(
% 0.72/0.45 (((f3 @ $true)) != $true) | (~spl27_48 | spl27_92)),
% 0.72/0.45 inference(forward_demodulation,[],[f512,f314])).
% 0.72/0.45 thf(f1090,plain,(
% 0.72/0.45 ~spl27_115 | ~spl27_48 | spl27_92),
% 0.72/0.45 inference(avatar_split_clause,[],[f1089,f511,f312,f768])).
% 0.72/0.45 thf(f1092,plain,(
% 0.72/0.45 (((f5 @ $true)) = $true) | (~spl27_40 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f278,f573])).
% 0.72/0.45 thf(f1096,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_38 | ~spl27_40 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f1092,f1007])).
% 0.72/0.45 thf(f1097,plain,(
% 0.72/0.45 $false | (~spl27_38 | ~spl27_40 | ~spl27_105)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1096])).
% 0.72/0.45 thf(f1098,plain,(
% 0.72/0.45 ~spl27_38 | ~spl27_40 | ~spl27_105),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1097])).
% 0.72/0.45 thf(f1108,plain,(
% 0.72/0.45 ($true = ((f4 @ $true))) | (~spl27_37 | ~spl27_45)),
% 0.72/0.45 inference(forward_demodulation,[],[f301,f265])).
% 0.72/0.45 thf(f1109,plain,(
% 0.72/0.45 spl27_109 | ~spl27_37 | ~spl27_45),
% 0.72/0.45 inference(avatar_split_clause,[],[f1108,f299,f263,f695])).
% 0.72/0.45 thf(f1113,plain,(
% 0.72/0.45 ($false = ((f4 @ $true))) | (~spl27_37 | ~spl27_47)),
% 0.72/0.45 inference(forward_demodulation,[],[f310,f265])).
% 0.72/0.45 thf(f1114,plain,(
% 0.72/0.45 spl27_110 | ~spl27_37 | ~spl27_47),
% 0.72/0.45 inference(avatar_split_clause,[],[f1113,f308,f263,f712])).
% 0.72/0.45 thf(f1119,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_13 | ~spl27_15 | ~spl27_50)),
% 0.72/0.45 inference(forward_demodulation,[],[f1048,f1047])).
% 0.72/0.45 thf(f1120,plain,(
% 0.72/0.45 $false | (~spl27_13 | ~spl27_15 | ~spl27_50)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1119])).
% 0.72/0.45 thf(f1121,plain,(
% 0.72/0.45 ~spl27_13 | ~spl27_15 | ~spl27_50),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1120])).
% 0.72/0.45 thf(f1122,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_14 | ~spl27_16)),
% 0.72/0.45 inference(forward_demodulation,[],[f161,f170])).
% 0.72/0.45 thf(f1123,plain,(
% 0.72/0.45 $false | (~spl27_14 | ~spl27_16)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1122])).
% 0.72/0.45 thf(f1124,plain,(
% 0.72/0.45 ~spl27_14 | ~spl27_16),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1123])).
% 0.72/0.45 thf(f1170,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_109 | ~spl27_110)),
% 0.72/0.45 inference(forward_demodulation,[],[f714,f697])).
% 0.72/0.45 thf(f1171,plain,(
% 0.72/0.45 $false | (~spl27_109 | ~spl27_110)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1170])).
% 0.72/0.45 thf(f1172,plain,(
% 0.72/0.45 ~spl27_109 | ~spl27_110),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1171])).
% 0.72/0.45 thf(f1174,plain,(
% 0.72/0.45 (((f5 @ $true)) != $true) | (~spl27_43 | spl27_71)),
% 0.72/0.45 inference(forward_demodulation,[],[f417,f292])).
% 0.72/0.45 thf(f1178,plain,(
% 0.72/0.45 (((f5 @ $true)) = $false) | (~spl27_43 | ~spl27_70)),
% 0.72/0.45 inference(forward_demodulation,[],[f413,f292])).
% 0.72/0.45 thf(f1183,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_43 | ~spl27_70 | ~spl27_81 | ~spl27_98)),
% 0.72/0.45 inference(forward_demodulation,[],[f1178,f1070])).
% 0.72/0.45 thf(f1184,plain,(
% 0.72/0.45 $false | (~spl27_43 | ~spl27_70 | ~spl27_81 | ~spl27_98)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1183])).
% 0.72/0.45 thf(f1185,plain,(
% 0.72/0.45 ~spl27_43 | ~spl27_70 | ~spl27_81 | ~spl27_98),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1184])).
% 0.72/0.45 thf(f1198,plain,(
% 0.72/0.45 ($true != ((f4 @ $false))) | (spl27_9 | ~spl27_72)),
% 0.72/0.45 inference(forward_demodulation,[],[f138,f422])).
% 0.72/0.45 thf(f1208,plain,(
% 0.72/0.45 $false | (~spl27_40 | ~spl27_43 | spl27_71 | ~spl27_105)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1174,f1092])).
% 0.72/0.45 thf(f1209,plain,(
% 0.72/0.45 ~spl27_40 | ~spl27_43 | spl27_71 | ~spl27_105),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1208])).
% 0.72/0.45 thf(f1217,plain,(
% 0.72/0.45 ($true != $true) | ($false = sF0) | spl27_81),
% 0.72/0.45 inference(constrained_superposition,[],[f462,f6])).
% 0.72/0.45 thf(f1218,plain,(
% 0.72/0.45 ($false = sF0) | spl27_81),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1217])).
% 0.72/0.45 thf(f1219,plain,(
% 0.72/0.45 spl27_84 | spl27_81),
% 0.72/0.45 inference(avatar_split_clause,[],[f1218,f461,f474])).
% 0.72/0.45 thf(f1231,plain,(
% 0.72/0.45 (((f6 @ $false)) = $false) | (~spl27_19 | ~spl27_84)),
% 0.72/0.45 inference(forward_demodulation,[],[f184,f476])).
% 0.72/0.45 thf(f1232,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_18 | ~spl27_19 | ~spl27_41 | ~spl27_84)),
% 0.72/0.45 inference(forward_demodulation,[],[f1231,f1065])).
% 0.72/0.45 thf(f1233,plain,(
% 0.72/0.45 $false | (~spl27_18 | ~spl27_19 | ~spl27_41 | ~spl27_84)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1232])).
% 0.72/0.45 thf(f1234,plain,(
% 0.72/0.45 ~spl27_18 | ~spl27_19 | ~spl27_41 | ~spl27_84),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1233])).
% 0.72/0.45 thf(f1236,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_18 | ~spl27_20)),
% 0.72/0.45 inference(forward_demodulation,[],[f188,f179])).
% 0.72/0.45 thf(f1237,plain,(
% 0.72/0.45 $false | (~spl27_18 | ~spl27_20)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1236])).
% 0.72/0.45 thf(f1238,plain,(
% 0.72/0.45 ~spl27_18 | ~spl27_20),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1237])).
% 0.72/0.45 thf(f1242,plain,(
% 0.72/0.45 ($false != ((f5 @ $false))) | (spl27_38 | ~spl27_107)),
% 0.72/0.45 inference(forward_demodulation,[],[f268,f582])).
% 0.72/0.45 thf(f1243,plain,(
% 0.72/0.45 ($true = ((f5 @ $false))) | (~spl27_40 | ~spl27_107)),
% 0.72/0.45 inference(forward_demodulation,[],[f278,f582])).
% 0.72/0.45 thf(f1244,plain,(
% 0.72/0.45 (sF13 = $false) | (((f6 @ $true)) = $true) | ~spl27_41),
% 0.72/0.45 inference(constrained_superposition,[],[f283,f6])).
% 0.72/0.45 thf(f1245,plain,(
% 0.72/0.45 (((f6 @ $true)) = $true) | (spl27_18 | ~spl27_41)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1244,f178])).
% 0.72/0.45 thf(f1246,plain,(
% 0.72/0.45 spl27_111 | spl27_18 | ~spl27_41),
% 0.72/0.45 inference(avatar_split_clause,[],[f1245,f281,f177,f723])).
% 0.72/0.45 thf(f1253,plain,(
% 0.72/0.45 ($false = ((f5 @ $false))) | (~spl27_84 | ~spl27_96)),
% 0.72/0.45 inference(forward_demodulation,[],[f531,f476])).
% 0.72/0.45 thf(f1254,plain,(
% 0.72/0.45 ($true = ((f5 @ $false))) | (~spl27_84 | ~spl27_98)),
% 0.72/0.45 inference(forward_demodulation,[],[f540,f476])).
% 0.72/0.45 thf(f1277,plain,(
% 0.72/0.45 $false | (spl27_38 | ~spl27_84 | ~spl27_96 | ~spl27_107)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1253,f1242])).
% 0.72/0.45 thf(f1278,plain,(
% 0.72/0.45 spl27_38 | ~spl27_84 | ~spl27_96 | ~spl27_107),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1277])).
% 0.72/0.45 thf(f1282,plain,(
% 0.72/0.45 ($false = ((f5 @ $false))) | (~spl27_38 | ~spl27_107)),
% 0.72/0.45 inference(forward_demodulation,[],[f269,f582])).
% 0.72/0.45 thf(f1283,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_38 | ~spl27_40 | ~spl27_107)),
% 0.72/0.45 inference(forward_demodulation,[],[f1282,f1243])).
% 0.72/0.45 thf(f1284,plain,(
% 0.72/0.45 $false | (~spl27_38 | ~spl27_40 | ~spl27_107)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1283])).
% 0.72/0.45 thf(f1285,plain,(
% 0.72/0.45 ~spl27_38 | ~spl27_40 | ~spl27_107),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1284])).
% 0.72/0.45 thf(f1298,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_23 | ~spl27_67 | ~spl27_112)),
% 0.72/0.45 inference(forward_demodulation,[],[f737,f690])).
% 0.72/0.45 thf(f1299,plain,(
% 0.72/0.45 $false | (~spl27_23 | ~spl27_67 | ~spl27_112)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1298])).
% 0.72/0.45 thf(f1300,plain,(
% 0.72/0.45 ~spl27_23 | ~spl27_67 | ~spl27_112),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1299])).
% 0.72/0.45 thf(f1307,plain,(
% 0.72/0.45 ($true = ((f1 @ $true))) | (~spl27_24 | ~spl27_54)),
% 0.72/0.45 inference(constrained_superposition,[],[f341,f206])).
% 0.72/0.45 thf(f1308,plain,(
% 0.72/0.45 spl27_112 | ~spl27_24 | ~spl27_54),
% 0.72/0.45 inference(avatar_split_clause,[],[f1307,f339,f204,f735])).
% 0.72/0.45 thf(f1318,plain,(
% 0.72/0.45 ($true = ((f1 @ $true))) | (~spl27_28 | ~spl27_74)),
% 0.72/0.45 inference(forward_demodulation,[],[f431,f224])).
% 0.72/0.45 thf(f1319,plain,(
% 0.72/0.45 spl27_112 | ~spl27_28 | ~spl27_74),
% 0.72/0.45 inference(avatar_split_clause,[],[f1318,f429,f222,f735])).
% 0.72/0.45 thf(f1322,plain,(
% 0.72/0.45 ($true = ((f0 @ $true))) | (~spl27_57 | ~spl27_76)),
% 0.72/0.45 inference(forward_demodulation,[],[f355,f440])).
% 0.72/0.45 thf(f1323,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_55 | ~spl27_57 | ~spl27_76 | ~spl27_100)),
% 0.72/0.45 inference(forward_demodulation,[],[f1322,f772])).
% 0.72/0.45 thf(f1324,plain,(
% 0.72/0.45 $false | (~spl27_55 | ~spl27_57 | ~spl27_76 | ~spl27_100)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1323])).
% 0.72/0.45 thf(f1325,plain,(
% 0.72/0.45 ~spl27_55 | ~spl27_57 | ~spl27_76 | ~spl27_100),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1324])).
% 0.72/0.45 thf(f1326,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_54 | ~spl27_56)),
% 0.72/0.45 inference(forward_demodulation,[],[f350,f341])).
% 0.72/0.45 thf(f1327,plain,(
% 0.72/0.45 $false | (~spl27_54 | ~spl27_56)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1326])).
% 0.72/0.45 thf(f1328,plain,(
% 0.72/0.45 ~spl27_54 | ~spl27_56),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1327])).
% 0.72/0.45 thf(f1329,plain,(
% 0.72/0.45 ($false = ((f1 @ $true))) | (~spl27_28 | ~spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f436,f224])).
% 0.72/0.45 thf(f1339,plain,(
% 0.72/0.45 (sF23 = $false) | ($true != $true) | spl27_76),
% 0.72/0.45 inference(constrained_superposition,[],[f439,f6])).
% 0.72/0.45 thf(f1340,plain,(
% 0.72/0.45 (sF23 = $false) | spl27_76),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1339])).
% 0.72/0.45 thf(f1341,plain,(
% 0.72/0.45 $false | (spl27_73 | spl27_76)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1340,f426])).
% 0.72/0.45 thf(f1342,plain,(
% 0.72/0.45 spl27_73 | spl27_76),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1341])).
% 0.72/0.45 thf(f1350,plain,(
% 0.72/0.45 ($true = ((f1 @ $false))) | (~spl27_21 | ~spl27_66)),
% 0.72/0.45 inference(forward_demodulation,[],[f193,f395])).
% 0.72/0.45 thf(f1352,plain,(
% 0.72/0.45 ($true != ((f0 @ $false))) | (spl27_30 | ~spl27_58)),
% 0.72/0.45 inference(forward_demodulation,[],[f232,f359])).
% 0.72/0.45 thf(f1353,plain,(
% 0.72/0.45 ($false = ((f0 @ $false))) | (~spl27_32 | ~spl27_58)),
% 0.72/0.45 inference(forward_demodulation,[],[f242,f359])).
% 0.72/0.45 thf(f1354,plain,(
% 0.72/0.45 ($true != ((f0 @ $true))) | (spl27_57 | ~spl27_76)),
% 0.72/0.45 inference(forward_demodulation,[],[f354,f440])).
% 0.72/0.45 thf(f1361,plain,(
% 0.72/0.45 $false | (~spl27_29 | spl27_30 | ~spl27_58 | ~spl27_89)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1352,f916])).
% 0.72/0.45 thf(f1362,plain,(
% 0.72/0.45 ~spl27_29 | spl27_30 | ~spl27_58 | ~spl27_89),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1361])).
% 0.72/0.45 thf(f1363,plain,(
% 0.72/0.45 ($true = ((f0 @ $false))) | (~spl27_30 | ~spl27_58)),
% 0.72/0.45 inference(forward_demodulation,[],[f233,f359])).
% 0.72/0.45 thf(f1364,plain,(
% 0.72/0.45 ($true != $true) | ($false = sF25) | spl27_31),
% 0.72/0.45 inference(constrained_superposition,[],[f237,f6])).
% 0.72/0.45 thf(f1365,plain,(
% 0.72/0.45 ($false = sF25) | spl27_31),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1364])).
% 0.72/0.45 thf(f1366,plain,(
% 0.72/0.45 spl27_29 | spl27_31),
% 0.72/0.45 inference(avatar_split_clause,[],[f1365,f236,f227])).
% 0.72/0.45 thf(f1369,plain,(
% 0.72/0.45 ($true = ((f0 @ $true))) | (~spl27_31 | ~spl27_89)),
% 0.72/0.45 inference(forward_demodulation,[],[f499,f238])).
% 0.72/0.45 thf(f1382,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_30 | ~spl27_32 | ~spl27_58)),
% 0.72/0.45 inference(forward_demodulation,[],[f1363,f1353])).
% 0.72/0.45 thf(f1383,plain,(
% 0.72/0.45 $false | (~spl27_30 | ~spl27_32 | ~spl27_58)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1382])).
% 0.72/0.45 thf(f1384,plain,(
% 0.72/0.45 ~spl27_30 | ~spl27_32 | ~spl27_58),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1383])).
% 0.72/0.45 thf(f1386,plain,(
% 0.72/0.45 $false | (~spl27_31 | spl27_57 | ~spl27_76 | ~spl27_89)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1369,f1354])).
% 0.72/0.45 thf(f1387,plain,(
% 0.72/0.45 ~spl27_31 | spl27_57 | ~spl27_76 | ~spl27_89),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1386])).
% 0.72/0.45 thf(f1391,plain,(
% 0.72/0.45 ($true != ((f0 @ $false))) | (spl27_57 | ~spl27_73)),
% 0.72/0.45 inference(forward_demodulation,[],[f354,f427])).
% 0.72/0.45 thf(f1392,plain,(
% 0.72/0.45 $false | (~spl27_30 | spl27_57 | ~spl27_58 | ~spl27_73)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1391,f1363])).
% 0.72/0.45 thf(f1393,plain,(
% 0.72/0.45 ~spl27_30 | spl27_57 | ~spl27_58 | ~spl27_73),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1392])).
% 0.72/0.45 thf(f1394,plain,(
% 0.72/0.45 ($true != ((f1 @ $true))) | (~spl27_24 | spl27_54)),
% 0.72/0.45 inference(forward_demodulation,[],[f340,f206])).
% 0.72/0.45 thf(f1404,plain,(
% 0.72/0.45 ($false = ((f0 @ $false))) | (~spl27_53 | ~spl27_100)),
% 0.72/0.45 inference(forward_demodulation,[],[f550,f337])).
% 0.72/0.45 thf(f1405,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_30 | ~spl27_53 | ~spl27_58 | ~spl27_100)),
% 0.72/0.45 inference(forward_demodulation,[],[f1404,f1363])).
% 0.72/0.45 thf(f1406,plain,(
% 0.72/0.45 $false | (~spl27_30 | ~spl27_53 | ~spl27_58 | ~spl27_100)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1405])).
% 0.72/0.45 thf(f1407,plain,(
% 0.72/0.45 ~spl27_30 | ~spl27_53 | ~spl27_58 | ~spl27_100),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1406])).
% 0.72/0.45 thf(f1410,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_1 | ~spl27_3)),
% 0.72/0.45 inference(forward_demodulation,[],[f103,f112])).
% 0.72/0.45 thf(f1411,plain,(
% 0.72/0.45 $false | (~spl27_1 | ~spl27_3)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1410])).
% 0.72/0.45 thf(f1412,plain,(
% 0.72/0.45 ~spl27_1 | ~spl27_3),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1411])).
% 0.72/0.45 thf(f1414,plain,(
% 0.72/0.45 ($false = ((f0 @ $true))) | (~spl27_31 | ~spl27_90)),
% 0.72/0.45 inference(forward_demodulation,[],[f504,f238])).
% 0.72/0.45 thf(f1432,plain,(
% 0.72/0.45 ($false = ((f0 @ $false))) | (~spl27_60 | ~spl27_73)),
% 0.72/0.45 inference(forward_demodulation,[],[f368,f427])).
% 0.72/0.45 thf(f1433,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_30 | ~spl27_58 | ~spl27_60 | ~spl27_73)),
% 0.72/0.45 inference(forward_demodulation,[],[f1432,f1363])).
% 0.72/0.45 thf(f1434,plain,(
% 0.72/0.45 $false | (~spl27_30 | ~spl27_58 | ~spl27_60 | ~spl27_73)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1433])).
% 0.72/0.45 thf(f1435,plain,(
% 0.72/0.45 ~spl27_30 | ~spl27_58 | ~spl27_60 | ~spl27_73),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1434])).
% 0.72/0.45 thf(f1440,plain,(
% 0.72/0.45 ($false = ((f0 @ $true))) | (~spl27_60 | ~spl27_76)),
% 0.72/0.45 inference(forward_demodulation,[],[f368,f440])).
% 0.72/0.45 thf(f1450,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_28 | ~spl27_75 | ~spl27_112)),
% 0.72/0.45 inference(forward_demodulation,[],[f737,f1329])).
% 0.72/0.45 thf(f1451,plain,(
% 0.72/0.45 $false | (~spl27_28 | ~spl27_75 | ~spl27_112)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1450])).
% 0.72/0.45 thf(f1452,plain,(
% 0.72/0.45 ~spl27_28 | ~spl27_75 | ~spl27_112),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1451])).
% 0.72/0.45 thf(f1453,plain,(
% 0.72/0.45 ~spl27_112 | ~spl27_24 | spl27_54),
% 0.72/0.45 inference(avatar_split_clause,[],[f1394,f339,f204,f735])).
% 0.72/0.45 thf(f1467,plain,(
% 0.72/0.45 ($false = ((f1 @ $false))) | (~spl27_25 | ~spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f436,f211])).
% 0.72/0.45 thf(f1468,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_21 | ~spl27_25 | ~spl27_66 | ~spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f1467,f1350])).
% 0.72/0.45 thf(f1469,plain,(
% 0.72/0.45 $false | (~spl27_21 | ~spl27_25 | ~spl27_66 | ~spl27_75)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1468])).
% 0.72/0.45 thf(f1470,plain,(
% 0.72/0.45 ~spl27_21 | ~spl27_25 | ~spl27_66 | ~spl27_75),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1469])).
% 0.72/0.45 thf(f1471,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_62 | ~spl27_64)),
% 0.72/0.45 inference(forward_demodulation,[],[f386,f377])).
% 0.72/0.45 thf(f1472,plain,(
% 0.72/0.45 $false | (~spl27_62 | ~spl27_64)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1471])).
% 0.72/0.45 thf(f1473,plain,(
% 0.72/0.45 ~spl27_62 | ~spl27_64),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1472])).
% 0.72/0.45 thf(f1474,plain,(
% 0.72/0.45 (((f2 @ $true)) != $false) | (~spl27_6 | spl27_62)),
% 0.72/0.45 inference(forward_demodulation,[],[f376,f125])).
% 0.72/0.45 thf(f1476,plain,(
% 0.72/0.45 ~spl27_113 | ~spl27_6 | spl27_62),
% 0.72/0.45 inference(avatar_split_clause,[],[f1474,f375,f123,f747])).
% 0.72/0.45 thf(f1500,plain,(
% 0.72/0.45 (((f2 @ $true)) = $false) | (~spl27_27 | ~spl27_61)),
% 0.72/0.45 inference(forward_demodulation,[],[f220,f373])).
% 0.72/0.45 thf(f1501,plain,(
% 0.72/0.45 spl27_113 | ~spl27_27 | ~spl27_61),
% 0.72/0.45 inference(avatar_split_clause,[],[f1500,f371,f218,f747])).
% 0.72/0.45 thf(f1504,plain,(
% 0.72/0.45 ($true = ((f1 @ $false))) | (~spl27_25 | ~spl27_74)),
% 0.72/0.45 inference(forward_demodulation,[],[f431,f211])).
% 0.72/0.45 thf(f1505,plain,(
% 0.72/0.45 ($false = ((f1 @ $false))) | (~spl27_25 | ~spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f436,f211])).
% 0.72/0.45 thf(f1506,plain,(
% 0.72/0.45 ($true = ((f0 @ $true))) | (~spl27_55 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f545,f346])).
% 0.72/0.45 thf(f1507,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_31 | ~spl27_55 | ~spl27_90 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f1506,f1414])).
% 0.72/0.45 thf(f1508,plain,(
% 0.72/0.45 $false | (~spl27_31 | ~spl27_55 | ~spl27_90 | ~spl27_99)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1507])).
% 0.72/0.45 thf(f1509,plain,(
% 0.72/0.45 ~spl27_31 | ~spl27_55 | ~spl27_90 | ~spl27_99),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1508])).
% 0.72/0.45 thf(f1521,plain,(
% 0.72/0.45 ($true != ((f1 @ $false))) | (~spl27_22 | spl27_54)),
% 0.72/0.45 inference(forward_demodulation,[],[f340,f197])).
% 0.72/0.45 thf(f1531,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_25 | ~spl27_74 | ~spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f1505,f1504])).
% 0.72/0.45 thf(f1532,plain,(
% 0.72/0.45 $false | (~spl27_25 | ~spl27_74 | ~spl27_75)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1531])).
% 0.72/0.45 thf(f1533,plain,(
% 0.72/0.45 ~spl27_25 | ~spl27_74 | ~spl27_75),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1532])).
% 0.72/0.45 thf(f1542,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_102 | ~spl27_103)),
% 0.72/0.45 inference(forward_demodulation,[],[f559,f564])).
% 0.72/0.45 thf(f1543,plain,(
% 0.72/0.45 $false | (~spl27_102 | ~spl27_103)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1542])).
% 0.72/0.45 thf(f1544,plain,(
% 0.72/0.45 ~spl27_102 | ~spl27_103),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1543])).
% 0.72/0.45 thf(f1568,plain,(
% 0.72/0.45 ($false = ((f2 @ $false))) | (~spl27_27 | ~spl27_63)),
% 0.72/0.45 inference(forward_demodulation,[],[f220,f382])).
% 0.72/0.45 thf(f1585,plain,(
% 0.72/0.45 ($false = ((f1 @ $false))) | (~spl27_68 | ~spl27_104)),
% 0.72/0.45 inference(forward_demodulation,[],[f404,f568])).
% 0.72/0.45 thf(f1586,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_25 | ~spl27_68 | ~spl27_74 | ~spl27_104)),
% 0.72/0.45 inference(forward_demodulation,[],[f1585,f1504])).
% 0.72/0.45 thf(f1587,plain,(
% 0.72/0.45 $false | (~spl27_25 | ~spl27_68 | ~spl27_74 | ~spl27_104)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1586])).
% 0.72/0.45 thf(f1588,plain,(
% 0.72/0.45 ~spl27_25 | ~spl27_68 | ~spl27_74 | ~spl27_104),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1587])).
% 0.72/0.45 thf(f1591,plain,(
% 0.72/0.45 $false | (~spl27_22 | ~spl27_25 | spl27_54 | ~spl27_74)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1521,f1504])).
% 0.72/0.45 thf(f1592,plain,(
% 0.72/0.45 ~spl27_22 | ~spl27_25 | spl27_54 | ~spl27_74),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1591])).
% 0.72/0.45 thf(f1593,plain,(
% 0.72/0.45 ($false != ((f2 @ $false))) | (~spl27_14 | spl27_102)),
% 0.72/0.45 inference(forward_demodulation,[],[f558,f161])).
% 0.72/0.45 thf(f1614,plain,(
% 0.72/0.45 $false | (~spl27_14 | ~spl27_27 | ~spl27_63 | spl27_102)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1593,f1568])).
% 0.72/0.45 thf(f1615,plain,(
% 0.72/0.45 ~spl27_14 | ~spl27_27 | ~spl27_63 | spl27_102),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1614])).
% 0.72/0.45 thf(f1616,plain,(
% 0.72/0.45 (((f3 @ $false)) = $false) | (~spl27_52 | ~spl27_91)),
% 0.72/0.45 inference(forward_demodulation,[],[f332,f509])).
% 0.72/0.45 thf(f1618,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_34 | ~spl27_36)),
% 0.72/0.45 inference(forward_demodulation,[],[f251,f260])).
% 0.72/0.45 thf(f1619,plain,(
% 0.72/0.45 $false | (~spl27_34 | ~spl27_36)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1618])).
% 0.72/0.45 thf(f1620,plain,(
% 0.72/0.45 ~spl27_34 | ~spl27_36),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1619])).
% 0.72/0.45 thf(f1621,plain,(
% 0.72/0.45 ($true = ((f4 @ $false))) | (~spl27_10 | ~spl27_34)),
% 0.72/0.45 inference(forward_demodulation,[],[f251,f143])).
% 0.72/0.45 thf(f1631,plain,(
% 0.72/0.45 (sF18 = $false) | ($true != $true) | spl27_80),
% 0.72/0.45 inference(constrained_superposition,[],[f457,f6])).
% 0.72/0.45 thf(f1632,plain,(
% 0.72/0.45 (sF18 = $false) | spl27_80),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1631])).
% 0.72/0.45 thf(f1633,plain,(
% 0.72/0.45 $false | (spl27_77 | spl27_80)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1632,f444])).
% 0.72/0.45 thf(f1634,plain,(
% 0.72/0.45 spl27_77 | spl27_80),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1633])).
% 0.72/0.45 thf(f1643,plain,(
% 0.72/0.45 (((f3 @ $false)) = $true) | (~spl27_13 | ~spl27_50)),
% 0.72/0.45 inference(forward_demodulation,[],[f157,f323])).
% 0.72/0.45 thf(f1646,plain,(
% 0.72/0.45 ($false = ((f4 @ $true))) | (~spl27_35 | ~spl27_79)),
% 0.72/0.45 inference(forward_demodulation,[],[f454,f256])).
% 0.72/0.45 thf(f1647,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_35 | ~spl27_79 | ~spl27_109)),
% 0.72/0.45 inference(forward_demodulation,[],[f1646,f697])).
% 0.72/0.45 thf(f1648,plain,(
% 0.72/0.45 $false | (~spl27_35 | ~spl27_79 | ~spl27_109)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1647])).
% 0.72/0.45 thf(f1649,plain,(
% 0.72/0.45 ~spl27_35 | ~spl27_79 | ~spl27_109),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1648])).
% 0.72/0.45 thf(f1655,plain,(
% 0.72/0.45 (((f2 @ $true)) != $false) | (~spl27_16 | spl27_102)),
% 0.72/0.45 inference(forward_demodulation,[],[f558,f170])).
% 0.72/0.45 thf(f1656,plain,(
% 0.72/0.45 ~spl27_113 | ~spl27_16 | spl27_102),
% 0.72/0.45 inference(avatar_split_clause,[],[f1655,f557,f168,f747])).
% 0.72/0.45 thf(f1672,plain,(
% 0.72/0.45 $false | (spl27_9 | ~spl27_10 | ~spl27_34 | ~spl27_72)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1621,f1198])).
% 0.72/0.45 thf(f1673,plain,(
% 0.72/0.45 spl27_9 | ~spl27_10 | ~spl27_34 | ~spl27_72),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1672])).
% 0.72/0.45 thf(f1674,plain,(
% 0.72/0.45 ($true = ((f4 @ $false))) | (~spl27_9 | ~spl27_72)),
% 0.72/0.45 inference(forward_demodulation,[],[f139,f422])).
% 0.72/0.45 thf(f1681,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_13 | ~spl27_50 | ~spl27_52 | ~spl27_91)),
% 0.72/0.45 inference(forward_demodulation,[],[f1643,f1616])).
% 0.72/0.45 thf(f1682,plain,(
% 0.72/0.45 $false | (~spl27_13 | ~spl27_50 | ~spl27_52 | ~spl27_91)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1681])).
% 0.72/0.45 thf(f1683,plain,(
% 0.72/0.45 ~spl27_13 | ~spl27_50 | ~spl27_52 | ~spl27_91),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1682])).
% 0.72/0.45 thf(f1701,plain,(
% 0.72/0.45 (((f3 @ $true)) = $false) | (~spl27_15 | ~spl27_51)),
% 0.72/0.45 inference(forward_demodulation,[],[f166,f328])).
% 0.72/0.45 thf(f1702,plain,(
% 0.72/0.45 ($true != ((f4 @ $false))) | (~spl27_39 | spl27_45)),
% 0.72/0.45 inference(forward_demodulation,[],[f300,f274])).
% 0.72/0.45 thf(f1706,plain,(
% 0.72/0.45 (((f3 @ $false)) = $true) | (~spl27_46 | ~spl27_92)),
% 0.72/0.45 inference(forward_demodulation,[],[f513,f305])).
% 0.72/0.45 thf(f1715,plain,(
% 0.72/0.45 ($false = ((f5 @ $false))) | (~spl27_84 | ~spl27_96)),
% 0.72/0.45 inference(forward_demodulation,[],[f531,f476])).
% 0.72/0.45 thf(f1716,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_84 | ~spl27_96 | ~spl27_98)),
% 0.72/0.45 inference(forward_demodulation,[],[f1715,f1254])).
% 0.72/0.45 thf(f1717,plain,(
% 0.72/0.45 $false | (~spl27_84 | ~spl27_96 | ~spl27_98)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1716])).
% 0.72/0.45 thf(f1718,plain,(
% 0.72/0.45 ~spl27_84 | ~spl27_96 | ~spl27_98),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1717])).
% 0.72/0.45 thf(f1729,plain,(
% 0.72/0.45 ($true = ((f5 @ $false))) | (~spl27_97 | ~spl27_108)),
% 0.72/0.45 inference(forward_demodulation,[],[f586,f536])).
% 0.72/0.45 thf(f1730,plain,(
% 0.72/0.45 $false | (~spl27_9 | ~spl27_39 | spl27_45 | ~spl27_72)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1702,f1674])).
% 0.72/0.45 thf(f1731,plain,(
% 0.72/0.45 ~spl27_9 | ~spl27_39 | spl27_45 | ~spl27_72),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1730])).
% 0.72/0.45 thf(f1747,plain,(
% 0.72/0.45 (((f3 @ $false)) = $false) | (~spl27_77 | ~spl27_86)),
% 0.72/0.45 inference(forward_demodulation,[],[f485,f445])).
% 0.72/0.45 thf(f1761,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_84 | ~spl27_96 | ~spl27_97 | ~spl27_108)),
% 0.72/0.45 inference(forward_demodulation,[],[f1729,f1715])).
% 0.72/0.45 thf(f1762,plain,(
% 0.72/0.45 $false | (~spl27_84 | ~spl27_96 | ~spl27_97 | ~spl27_108)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1761])).
% 0.72/0.45 thf(f1763,plain,(
% 0.72/0.45 ~spl27_84 | ~spl27_96 | ~spl27_97 | ~spl27_108),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1762])).
% 0.72/0.45 thf(f1782,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_46 | ~spl27_77 | ~spl27_86 | ~spl27_92)),
% 0.72/0.45 inference(forward_demodulation,[],[f1747,f1706])).
% 0.72/0.45 thf(f1783,plain,(
% 0.72/0.45 $false | (~spl27_46 | ~spl27_77 | ~spl27_86 | ~spl27_92)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1782])).
% 0.72/0.45 thf(f1784,plain,(
% 0.72/0.45 ~spl27_46 | ~spl27_77 | ~spl27_86 | ~spl27_92),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1783])).
% 0.72/0.45 thf(f1814,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_15 | ~spl27_51 | ~spl27_115)),
% 0.72/0.45 inference(forward_demodulation,[],[f770,f1701])).
% 0.72/0.45 thf(f1815,plain,(
% 0.72/0.45 $false | (~spl27_15 | ~spl27_51 | ~spl27_115)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1814])).
% 0.72/0.45 thf(f1816,plain,(
% 0.72/0.45 ~spl27_15 | ~spl27_51 | ~spl27_115),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1815])).
% 0.72/0.45 thf(f1818,plain,(
% 0.72/0.45 ($true != ((f2 @ $false))) | (~spl27_8 | spl27_64)),
% 0.72/0.45 inference(forward_demodulation,[],[f385,f134])).
% 0.72/0.45 thf(f1819,plain,(
% 0.72/0.45 ($false = ((f2 @ $false))) | (~spl27_8 | ~spl27_62)),
% 0.72/0.45 inference(forward_demodulation,[],[f377,f134])).
% 0.72/0.45 thf(f1861,plain,(
% 0.72/0.45 ($true = ((f0 @ $true))) | (~spl27_55 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f545,f346])).
% 0.72/0.45 thf(f1886,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_55 | ~spl27_60 | ~spl27_76 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f1861,f1440])).
% 0.72/0.45 thf(f1887,plain,(
% 0.72/0.45 $false | (~spl27_55 | ~spl27_60 | ~spl27_76 | ~spl27_99)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1886])).
% 0.72/0.45 thf(f1888,plain,(
% 0.72/0.45 ~spl27_55 | ~spl27_60 | ~spl27_76 | ~spl27_99),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1887])).
% 0.72/0.45 thf(f1894,plain,(
% 0.72/0.45 ($false = ((f0 @ $true))) | (~spl27_32 | ~spl27_59)),
% 0.72/0.45 inference(forward_demodulation,[],[f242,f364])).
% 0.72/0.45 thf(f1909,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_32 | ~spl27_55 | ~spl27_59 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f1894,f1861])).
% 0.72/0.45 thf(f1910,plain,(
% 0.72/0.45 $false | (~spl27_32 | ~spl27_55 | ~spl27_59 | ~spl27_99)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1909])).
% 0.72/0.45 thf(f1911,plain,(
% 0.72/0.45 ~spl27_32 | ~spl27_55 | ~spl27_59 | ~spl27_99),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1910])).
% 0.72/0.45 thf(f1913,plain,(
% 0.72/0.45 ($true = ((f2 @ $false))) | (~spl27_26 | ~spl27_63)),
% 0.72/0.45 inference(forward_demodulation,[],[f215,f382])).
% 0.72/0.45 thf(f1914,plain,(
% 0.72/0.45 ($false != ((f2 @ $false))) | (spl27_27 | ~spl27_63)),
% 0.72/0.45 inference(forward_demodulation,[],[f219,f382])).
% 0.72/0.45 thf(f1919,plain,(
% 0.72/0.45 $false | (~spl27_8 | ~spl27_26 | ~spl27_63 | spl27_64)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1913,f1818])).
% 0.72/0.45 thf(f1920,plain,(
% 0.72/0.45 ~spl27_8 | ~spl27_26 | ~spl27_63 | spl27_64),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1919])).
% 0.72/0.45 thf(f1921,plain,(
% 0.72/0.45 $false | (~spl27_8 | spl27_27 | ~spl27_62 | ~spl27_63)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f1914,f1819])).
% 0.72/0.45 thf(f1922,plain,(
% 0.72/0.45 ~spl27_8 | spl27_27 | ~spl27_62 | ~spl27_63),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1921])).
% 0.72/0.45 thf(f1923,plain,(
% 0.72/0.45 ($true = ((f2 @ $false))) | (~spl27_8 | ~spl27_64)),
% 0.72/0.45 inference(forward_demodulation,[],[f386,f134])).
% 0.72/0.45 thf(f1931,plain,(
% 0.72/0.45 (sF10 = $false) | ($true != $true) | spl27_24),
% 0.72/0.45 inference(constrained_superposition,[],[f205,f6])).
% 0.72/0.45 thf(f1932,plain,(
% 0.72/0.45 (sF10 = $false) | spl27_24),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1931])).
% 0.72/0.45 thf(f1933,plain,(
% 0.72/0.45 spl27_22 | spl27_24),
% 0.72/0.45 inference(avatar_split_clause,[],[f1932,f204,f195])).
% 0.72/0.45 thf(f1948,plain,(
% 0.72/0.45 ($true = ((f2 @ $true))) | (~spl27_26 | ~spl27_61)),
% 0.72/0.45 inference(forward_demodulation,[],[f215,f373])).
% 0.72/0.45 thf(f1949,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_26 | ~spl27_61 | ~spl27_113)),
% 0.72/0.45 inference(forward_demodulation,[],[f1948,f749])).
% 0.72/0.45 thf(f1950,plain,(
% 0.72/0.45 $false | (~spl27_26 | ~spl27_61 | ~spl27_113)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f1949])).
% 0.72/0.45 thf(f1951,plain,(
% 0.72/0.45 ~spl27_26 | ~spl27_61 | ~spl27_113),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f1950])).
% 0.72/0.45 thf(f1955,plain,(
% 0.72/0.45 (((f3 @ $false)) = $false) | (~spl27_15 | ~spl27_50)),
% 0.72/0.45 inference(forward_demodulation,[],[f166,f323])).
% 0.72/0.45 thf(f1981,plain,(
% 0.72/0.45 ($false = ((f2 @ $false))) | (~spl27_5 | ~spl27_87)),
% 0.72/0.45 inference(forward_demodulation,[],[f121,f490])).
% 0.72/0.45 thf(f1998,plain,(
% 0.72/0.45 (((f6 @ $true)) = $false) | (x = $false) | ~spl27_82),
% 0.72/0.45 inference(constrained_superposition,[],[f467,f6])).
% 0.72/0.45 thf(f2005,plain,(
% 0.72/0.45 ($true = $false) | (x = $false) | (~spl27_82 | ~spl27_111)),
% 0.72/0.45 inference(forward_demodulation,[],[f1998,f725])).
% 0.72/0.45 thf(f2006,plain,(
% 0.72/0.45 (x = $false) | (~spl27_82 | ~spl27_111)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2005])).
% 0.72/0.45 thf(f2007,plain,(
% 0.72/0.45 spl27_114 | ~spl27_82 | ~spl27_111),
% 0.72/0.45 inference(avatar_split_clause,[],[f2006,f723,f465,f758])).
% 0.72/0.45 thf(f2019,plain,(
% 0.72/0.45 (((f5 @ $true)) = $true) | (~spl27_43 | ~spl27_71)),
% 0.72/0.45 inference(forward_demodulation,[],[f418,f292])).
% 0.72/0.45 thf(f2033,plain,(
% 0.72/0.45 ($true = ((f4 @ $true))) | (~spl27_35 | ~spl27_78)),
% 0.72/0.45 inference(forward_demodulation,[],[f449,f256])).
% 0.72/0.45 thf(f2034,plain,(
% 0.72/0.45 spl27_109 | ~spl27_35 | ~spl27_78),
% 0.72/0.45 inference(avatar_split_clause,[],[f2033,f447,f254,f695])).
% 0.72/0.45 thf(f2050,plain,(
% 0.72/0.45 (((f3 @ $false)) = $true) | (~spl27_77 | ~spl27_88)),
% 0.72/0.45 inference(forward_demodulation,[],[f494,f445])).
% 0.72/0.45 thf(f2054,plain,(
% 0.72/0.45 ($false = ((f0 @ $false))) | (~spl27_53 | ~spl27_100)),
% 0.72/0.45 inference(forward_demodulation,[],[f550,f337])).
% 0.72/0.45 thf(f2057,plain,(
% 0.72/0.45 (((f5 @ $true)) = $false) | (~spl27_95 | ~spl27_106)),
% 0.72/0.45 inference(forward_demodulation,[],[f577,f527])).
% 0.72/0.45 thf(f2076,plain,(
% 0.72/0.45 ($true = ((f0 @ $true))) | (~spl27_30 | ~spl27_59)),
% 0.72/0.45 inference(forward_demodulation,[],[f233,f364])).
% 0.72/0.45 thf(f2092,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_5 | ~spl27_8 | ~spl27_64 | ~spl27_87)),
% 0.72/0.45 inference(forward_demodulation,[],[f1981,f1923])).
% 0.72/0.45 thf(f2093,plain,(
% 0.72/0.45 $false | (~spl27_5 | ~spl27_8 | ~spl27_64 | ~spl27_87)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2092])).
% 0.72/0.45 thf(f2094,plain,(
% 0.72/0.45 ~spl27_5 | ~spl27_8 | ~spl27_64 | ~spl27_87),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2093])).
% 0.72/0.45 thf(f2127,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_15 | ~spl27_50 | ~spl27_77 | ~spl27_88)),
% 0.72/0.45 inference(forward_demodulation,[],[f2050,f1955])).
% 0.72/0.45 thf(f2128,plain,(
% 0.72/0.45 $false | (~spl27_15 | ~spl27_50 | ~spl27_77 | ~spl27_88)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2127])).
% 0.72/0.45 thf(f2129,plain,(
% 0.72/0.45 ~spl27_15 | ~spl27_50 | ~spl27_77 | ~spl27_88),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2128])).
% 0.72/0.45 thf(f2131,plain,(
% 0.72/0.45 ($false = ((f1 @ $false))) | (~spl27_23 | ~spl27_66)),
% 0.72/0.45 inference(forward_demodulation,[],[f202,f395])).
% 0.72/0.45 thf(f2132,plain,(
% 0.72/0.45 ($true != ((f1 @ $false))) | (~spl27_25 | spl27_74)),
% 0.72/0.45 inference(forward_demodulation,[],[f430,f211])).
% 0.72/0.45 thf(f2159,plain,(
% 0.72/0.45 ($true = ((f0 @ $false))) | (~spl27_57 | ~spl27_73)),
% 0.72/0.45 inference(forward_demodulation,[],[f355,f427])).
% 0.72/0.45 thf(f2163,plain,(
% 0.72/0.45 (((f2 @ $true)) = $false) | (~spl27_16 | ~spl27_102)),
% 0.72/0.45 inference(forward_demodulation,[],[f559,f170])).
% 0.72/0.45 thf(f2164,plain,(
% 0.72/0.45 spl27_113 | ~spl27_16 | ~spl27_102),
% 0.72/0.45 inference(avatar_split_clause,[],[f2163,f557,f168,f747])).
% 0.72/0.45 thf(f2165,plain,(
% 0.72/0.45 ($true != ((f2 @ $true))) | (~spl27_16 | spl27_103)),
% 0.72/0.45 inference(forward_demodulation,[],[f563,f170])).
% 0.72/0.45 thf(f2166,plain,(
% 0.72/0.45 ~spl27_116 | ~spl27_16 | spl27_103),
% 0.72/0.45 inference(avatar_split_clause,[],[f2165,f562,f168,f775])).
% 0.72/0.45 thf(f2173,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_43 | ~spl27_71 | ~spl27_95 | ~spl27_106)),
% 0.72/0.45 inference(forward_demodulation,[],[f2057,f2019])).
% 0.72/0.45 thf(f2174,plain,(
% 0.72/0.45 $false | (~spl27_43 | ~spl27_71 | ~spl27_95 | ~spl27_106)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2173])).
% 0.72/0.45 thf(f2175,plain,(
% 0.72/0.45 ~spl27_43 | ~spl27_71 | ~spl27_95 | ~spl27_106),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2174])).
% 0.72/0.45 thf(f2208,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_53 | ~spl27_57 | ~spl27_73 | ~spl27_100)),
% 0.72/0.45 inference(forward_demodulation,[],[f2159,f2054])).
% 0.72/0.45 thf(f2209,plain,(
% 0.72/0.45 $false | (~spl27_53 | ~spl27_57 | ~spl27_73 | ~spl27_100)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2208])).
% 0.72/0.45 thf(f2210,plain,(
% 0.72/0.45 ~spl27_53 | ~spl27_57 | ~spl27_73 | ~spl27_100),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2209])).
% 0.72/0.45 thf(f2213,plain,(
% 0.72/0.45 ($false = ((f0 @ $true))) | (~spl27_31 | ~spl27_90)),
% 0.72/0.45 inference(forward_demodulation,[],[f504,f238])).
% 0.72/0.45 thf(f2214,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_30 | ~spl27_31 | ~spl27_59 | ~spl27_90)),
% 0.72/0.45 inference(forward_demodulation,[],[f2213,f2076])).
% 0.72/0.45 thf(f2215,plain,(
% 0.72/0.45 $false | (~spl27_30 | ~spl27_31 | ~spl27_59 | ~spl27_90)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2214])).
% 0.72/0.45 thf(f2216,plain,(
% 0.72/0.45 ~spl27_30 | ~spl27_31 | ~spl27_59 | ~spl27_90),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2215])).
% 0.72/0.45 thf(f2223,plain,(
% 0.72/0.45 ($false = sF24) | ($true != $true) | spl27_59),
% 0.72/0.45 inference(constrained_superposition,[],[f363,f6])).
% 0.72/0.45 thf(f2224,plain,(
% 0.72/0.45 ($false = sF24) | spl27_59),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2223])).
% 0.72/0.45 thf(f2225,plain,(
% 0.72/0.45 $false | (spl27_58 | spl27_59)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2224,f358])).
% 0.72/0.45 thf(f2226,plain,(
% 0.72/0.45 spl27_58 | spl27_59),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2225])).
% 0.72/0.45 thf(f2227,plain,(
% 0.72/0.45 ($true = ((f1 @ $false))) | (~spl27_22 | ~spl27_54)),
% 0.72/0.45 inference(forward_demodulation,[],[f341,f197])).
% 0.72/0.45 thf(f2229,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_22 | ~spl27_23 | ~spl27_54 | ~spl27_66)),
% 0.72/0.45 inference(forward_demodulation,[],[f2227,f2131])).
% 0.72/0.45 thf(f2230,plain,(
% 0.72/0.45 $false | (~spl27_22 | ~spl27_23 | ~spl27_54 | ~spl27_66)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2229])).
% 0.72/0.45 thf(f2231,plain,(
% 0.72/0.45 ~spl27_22 | ~spl27_23 | ~spl27_54 | ~spl27_66),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2230])).
% 0.72/0.45 thf(f2234,plain,(
% 0.72/0.45 ($true = ((f1 @ $false))) | (~spl27_65 | ~spl27_104)),
% 0.72/0.45 inference(forward_demodulation,[],[f391,f568])).
% 0.72/0.45 thf(f2268,plain,(
% 0.72/0.45 $false | (~spl27_22 | ~spl27_25 | ~spl27_54 | spl27_74)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2227,f2132])).
% 0.72/0.45 thf(f2269,plain,(
% 0.72/0.45 ~spl27_22 | ~spl27_25 | ~spl27_54 | spl27_74),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2268])).
% 0.72/0.45 thf(f2276,plain,(
% 0.72/0.45 $false | (~spl27_25 | ~spl27_65 | spl27_74 | ~spl27_104)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2234,f2132])).
% 0.72/0.45 thf(f2277,plain,(
% 0.72/0.45 ~spl27_25 | ~spl27_65 | spl27_74 | ~spl27_104),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2276])).
% 0.72/0.45 thf(f2279,plain,(
% 0.72/0.45 ($true != ((f4 @ $false))) | (~spl27_10 | spl27_34)),
% 0.72/0.45 inference(forward_demodulation,[],[f250,f143])).
% 0.72/0.45 thf(f2307,plain,(
% 0.72/0.45 ($true = ((f4 @ $false))) | (~spl27_33 | ~spl27_78)),
% 0.72/0.45 inference(forward_demodulation,[],[f449,f247])).
% 0.72/0.45 thf(f2340,plain,(
% 0.72/0.45 $false | (~spl27_10 | ~spl27_33 | spl27_34 | ~spl27_78)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2307,f2279])).
% 0.72/0.45 thf(f2341,plain,(
% 0.72/0.45 ~spl27_10 | ~spl27_33 | spl27_34 | ~spl27_78),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2340])).
% 0.72/0.45 thf(f2343,plain,(
% 0.72/0.45 ($false = ((f2 @ $false))) | (~spl27_14 | ~spl27_102)),
% 0.72/0.45 inference(forward_demodulation,[],[f559,f161])).
% 0.72/0.45 thf(f2372,plain,(
% 0.72/0.45 ($false != ((f2 @ $false))) | (spl27_5 | ~spl27_87)),
% 0.72/0.45 inference(forward_demodulation,[],[f120,f490])).
% 0.72/0.45 thf(f2393,plain,(
% 0.72/0.45 $false | (spl27_5 | ~spl27_14 | ~spl27_87 | ~spl27_102)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2372,f2343])).
% 0.72/0.45 thf(f2394,plain,(
% 0.72/0.45 spl27_5 | ~spl27_14 | ~spl27_87 | ~spl27_102),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2393])).
% 0.72/0.45 thf(f2398,plain,(
% 0.72/0.45 (((f5 @ $true)) = $false) | (~spl27_38 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f269,f573])).
% 0.72/0.45 thf(f2405,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_38 | ~spl27_43 | ~spl27_71 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f2398,f2019])).
% 0.72/0.45 thf(f2406,plain,(
% 0.72/0.45 $false | (~spl27_38 | ~spl27_43 | ~spl27_71 | ~spl27_105)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2405])).
% 0.72/0.45 thf(f2407,plain,(
% 0.72/0.45 ~spl27_38 | ~spl27_43 | ~spl27_71 | ~spl27_105),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2406])).
% 0.72/0.45 thf(f2409,plain,(
% 0.72/0.45 (((f6 @ $false)) = $false) | (~spl27_82 | ~spl27_114)),
% 0.72/0.45 inference(forward_demodulation,[],[f467,f760])).
% 0.72/0.45 thf(f2441,plain,(
% 0.72/0.45 (((f6 @ $false)) = $true) | (~spl27_17 | ~spl27_84)),
% 0.72/0.45 inference(forward_demodulation,[],[f175,f476])).
% 0.72/0.45 thf(f2443,plain,(
% 0.72/0.45 ($true = ((f4 @ $true))) | (~spl27_12 | ~spl27_34)),
% 0.72/0.45 inference(forward_demodulation,[],[f251,f152])).
% 0.72/0.45 thf(f2444,plain,(
% 0.72/0.45 spl27_109 | ~spl27_12 | ~spl27_34),
% 0.72/0.45 inference(avatar_split_clause,[],[f2443,f249,f150,f695])).
% 0.72/0.45 thf(f2473,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_17 | ~spl27_82 | ~spl27_84 | ~spl27_114)),
% 0.72/0.45 inference(forward_demodulation,[],[f2441,f2409])).
% 0.72/0.45 thf(f2474,plain,(
% 0.72/0.45 $false | (~spl27_17 | ~spl27_82 | ~spl27_84 | ~spl27_114)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2473])).
% 0.72/0.45 thf(f2475,plain,(
% 0.72/0.45 ~spl27_17 | ~spl27_82 | ~spl27_84 | ~spl27_114),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2474])).
% 0.72/0.45 thf(f2480,plain,(
% 0.72/0.45 (((f6 @ $false)) = $true) | (~spl27_83 | ~spl27_114)),
% 0.72/0.45 inference(forward_demodulation,[],[f472,f760])).
% 0.72/0.45 thf(f2487,plain,(
% 0.72/0.45 ($true != $true) | (sF13 = $false) | spl27_20),
% 0.72/0.45 inference(constrained_superposition,[],[f187,f6])).
% 0.72/0.45 thf(f2488,plain,(
% 0.72/0.45 (sF13 = $false) | spl27_20),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2487])).
% 0.72/0.45 thf(f2491,plain,(
% 0.72/0.45 spl27_18 | spl27_20),
% 0.72/0.45 inference(avatar_split_clause,[],[f2488,f186,f177])).
% 0.72/0.45 thf(f2501,plain,(
% 0.72/0.45 (((f6 @ $true)) = $false) | (~spl27_19 | ~spl27_81)),
% 0.72/0.45 inference(forward_demodulation,[],[f184,f463])).
% 0.72/0.45 thf(f2502,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_19 | ~spl27_81 | ~spl27_111)),
% 0.72/0.45 inference(forward_demodulation,[],[f2501,f725])).
% 0.72/0.45 thf(f2503,plain,(
% 0.72/0.45 $false | (~spl27_19 | ~spl27_81 | ~spl27_111)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2502])).
% 0.72/0.45 thf(f2504,plain,(
% 0.72/0.45 ~spl27_19 | ~spl27_81 | ~spl27_111),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2503])).
% 0.72/0.45 thf(f2509,plain,(
% 0.72/0.45 (((f6 @ $false)) != $true) | (~spl27_18 | spl27_41)),
% 0.72/0.45 inference(forward_demodulation,[],[f282,f179])).
% 0.72/0.45 thf(f2532,plain,(
% 0.72/0.45 $false | (~spl27_18 | spl27_41 | ~spl27_83 | ~spl27_114)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2509,f2480])).
% 0.72/0.45 thf(f2533,plain,(
% 0.72/0.45 ~spl27_18 | spl27_41 | ~spl27_83 | ~spl27_114),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2532])).
% 0.72/0.45 thf(f2539,plain,(
% 0.72/0.45 ($false = ((f0 @ $false))) | (~spl27_29 | ~spl27_90)),
% 0.72/0.45 inference(forward_demodulation,[],[f504,f229])).
% 0.72/0.45 thf(f2541,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_69 | ~spl27_72)),
% 0.72/0.45 inference(forward_demodulation,[],[f422,f409])).
% 0.72/0.45 thf(f2542,plain,(
% 0.72/0.45 $false | (~spl27_69 | ~spl27_72)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2541])).
% 0.72/0.45 thf(f2543,plain,(
% 0.72/0.45 ~spl27_69 | ~spl27_72),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2542])).
% 0.72/0.45 thf(f2545,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_81 | ~spl27_84)),
% 0.72/0.45 inference(forward_demodulation,[],[f476,f463])).
% 0.72/0.45 thf(f2546,plain,(
% 0.72/0.45 $false | (~spl27_81 | ~spl27_84)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2545])).
% 0.72/0.45 thf(f2547,plain,(
% 0.72/0.45 ~spl27_81 | ~spl27_84),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2546])).
% 0.72/0.45 thf(f2561,plain,(
% 0.72/0.45 ($false = ((f5 @ $false))) | (~spl27_42 | ~spl27_70)),
% 0.72/0.45 inference(forward_demodulation,[],[f413,f287])).
% 0.72/0.45 thf(f2613,plain,(
% 0.72/0.45 ($false = ((f1 @ $true))) | (~spl27_68 | ~spl27_101)),
% 0.72/0.45 inference(forward_demodulation,[],[f404,f555])).
% 0.72/0.45 thf(f2627,plain,(
% 0.72/0.45 ($true = ((f0 @ $false))) | (~spl27_53 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f545,f337])).
% 0.72/0.45 thf(f2663,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_29 | ~spl27_53 | ~spl27_90 | ~spl27_99)),
% 0.72/0.45 inference(forward_demodulation,[],[f2627,f2539])).
% 0.72/0.45 thf(f2664,plain,(
% 0.72/0.45 $false | (~spl27_29 | ~spl27_53 | ~spl27_90 | ~spl27_99)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2663])).
% 0.72/0.45 thf(f2665,plain,(
% 0.72/0.45 ~spl27_29 | ~spl27_53 | ~spl27_90 | ~spl27_99),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2664])).
% 0.72/0.45 thf(f2666,plain,(
% 0.72/0.45 ($false != ((f1 @ $true))) | (~spl27_28 | spl27_75)),
% 0.72/0.45 inference(forward_demodulation,[],[f435,f224])).
% 0.72/0.45 thf(f2683,plain,(
% 0.72/0.45 $false | (~spl27_28 | ~spl27_68 | spl27_75 | ~spl27_101)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2666,f2613])).
% 0.72/0.45 thf(f2684,plain,(
% 0.72/0.45 ~spl27_28 | ~spl27_68 | spl27_75 | ~spl27_101),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2683])).
% 0.72/0.45 thf(f2685,plain,(
% 0.72/0.45 ($false = ((f4 @ $true))) | (~spl27_12 | ~spl27_36)),
% 0.72/0.45 inference(forward_demodulation,[],[f260,f152])).
% 0.72/0.45 thf(f2687,plain,(
% 0.72/0.45 ($false != ((f5 @ $false))) | (~spl27_84 | spl27_96)),
% 0.72/0.45 inference(forward_demodulation,[],[f530,f476])).
% 0.72/0.45 thf(f2691,plain,(
% 0.72/0.45 spl27_110 | ~spl27_12 | ~spl27_36),
% 0.72/0.45 inference(avatar_split_clause,[],[f2685,f258,f150,f712])).
% 0.72/0.45 thf(f2732,plain,(
% 0.72/0.45 (((f5 @ $true)) = $true) | (~spl27_95 | ~spl27_108)),
% 0.72/0.45 inference(forward_demodulation,[],[f586,f527])).
% 0.72/0.45 thf(f2752,plain,(
% 0.72/0.45 $false | (~spl27_42 | ~spl27_70 | ~spl27_84 | spl27_96)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2687,f2561])).
% 0.72/0.45 thf(f2753,plain,(
% 0.72/0.45 ~spl27_42 | ~spl27_70 | ~spl27_84 | spl27_96),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2752])).
% 0.72/0.45 thf(f2757,plain,(
% 0.72/0.45 (((f5 @ $true)) = $false) | (~spl27_38 | ~spl27_105)),
% 0.72/0.45 inference(forward_demodulation,[],[f269,f573])).
% 0.72/0.45 thf(f2794,plain,(
% 0.72/0.45 (((f6 @ $true)) != $true) | (~spl27_20 | spl27_41)),
% 0.72/0.45 inference(forward_demodulation,[],[f282,f188])).
% 0.72/0.45 thf(f2795,plain,(
% 0.72/0.45 ~spl27_111 | ~spl27_20 | spl27_41),
% 0.72/0.45 inference(avatar_split_clause,[],[f2794,f281,f186,f723])).
% 0.72/0.45 thf(f2821,plain,(
% 0.72/0.45 ($true = $false) | (~spl27_38 | ~spl27_95 | ~spl27_105 | ~spl27_108)),
% 0.72/0.45 inference(forward_demodulation,[],[f2757,f2732])).
% 0.72/0.45 thf(f2822,plain,(
% 0.72/0.45 $false | (~spl27_38 | ~spl27_95 | ~spl27_105 | ~spl27_108)),
% 0.72/0.45 inference(trivial_inequality_removal,[],[f2821])).
% 0.72/0.45 thf(f2823,plain,(
% 0.72/0.45 ~spl27_38 | ~spl27_95 | ~spl27_105 | ~spl27_108),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2822])).
% 0.72/0.45 thf(f2824,plain,(
% 0.72/0.45 (((f3 @ $false)) != $true) | (~spl27_46 | spl27_92)),
% 0.72/0.45 inference(forward_demodulation,[],[f512,f305])).
% 0.72/0.45 thf(f2879,plain,(
% 0.72/0.45 (((f3 @ $true)) != $true) | (spl27_13 | ~spl27_51)),
% 0.72/0.45 inference(forward_demodulation,[],[f156,f328])).
% 0.72/0.45 thf(f2880,plain,(
% 0.72/0.45 ~spl27_115 | spl27_13 | ~spl27_51),
% 0.72/0.45 inference(avatar_split_clause,[],[f2879,f326,f155,f768])).
% 0.72/0.45 thf(f2893,plain,(
% 0.72/0.45 (((f3 @ $false)) = $true) | (~spl27_49 | ~spl27_91)),
% 0.72/0.45 inference(forward_demodulation,[],[f319,f509])).
% 0.72/0.45 thf(f2932,plain,(
% 0.72/0.45 $false | (~spl27_46 | ~spl27_49 | ~spl27_91 | spl27_92)),
% 0.72/0.45 inference(forward_subsumption_resolution,[],[f2893,f2824])).
% 0.72/0.45 thf(f2933,plain,(
% 0.72/0.45 ~spl27_46 | ~spl27_49 | ~spl27_91 | spl27_92),
% 0.72/0.45 inference(avatar_contradiction_clause,[],[f2932])).
% 0.72/0.45 cnf(s1, plain, spl27_1 | spl27_2, inference(sat_conversion,[],[f108])).
% 0.72/0.45 cnf(s2, plain, spl27_3 | spl27_4, inference(sat_conversion,[],[f117])).
% 0.72/0.45 cnf(s3, plain, spl27_5 | spl27_6, inference(sat_conversion,[],[f126])).
% 0.72/0.45 cnf(s4, plain, spl27_7 | spl27_8, inference(sat_conversion,[],[f135])).
% 0.72/0.45 cnf(s5, plain, spl27_9 | spl27_10, inference(sat_conversion,[],[f144])).
% 0.72/0.45 cnf(s6, plain, spl27_11 | spl27_12, inference(sat_conversion,[],[f153])).
% 0.72/0.45 cnf(s7, plain, spl27_13 | spl27_14, inference(sat_conversion,[],[f162])).
% 0.72/0.45 cnf(s8, plain, spl27_15 | spl27_16, inference(sat_conversion,[],[f171])).
% 0.72/0.45 cnf(s9, plain, spl27_17 | spl27_18, inference(sat_conversion,[],[f180])).
% 0.72/0.45 cnf(s10, plain, spl27_19 | spl27_20, inference(sat_conversion,[],[f189])).
% 0.72/0.45 cnf(s11, plain, spl27_21 | spl27_22, inference(sat_conversion,[],[f198])).
% 0.72/0.45 cnf(s12, plain, spl27_23 | spl27_24, inference(sat_conversion,[],[f207])).
% 0.72/0.45 cnf(s13, plain, spl27_25 | spl27_26, inference(sat_conversion,[],[f216])).
% 0.72/0.45 cnf(s14, plain, spl27_27 | spl27_28, inference(sat_conversion,[],[f225])).
% 0.72/0.45 cnf(s15, plain, spl27_29 | spl27_30, inference(sat_conversion,[],[f234])).
% 0.72/0.45 cnf(s16, plain, spl27_31 | spl27_32, inference(sat_conversion,[],[f243])).
% 0.72/0.45 cnf(s17, plain, spl27_33 | spl27_34, inference(sat_conversion,[],[f252])).
% 0.72/0.45 cnf(s18, plain, spl27_35 | spl27_36, inference(sat_conversion,[],[f261])).
% 0.72/0.45 cnf(s19, plain, spl27_37 | spl27_38, inference(sat_conversion,[],[f270])).
% 0.72/0.45 cnf(s20, plain, spl27_39 | spl27_40, inference(sat_conversion,[],[f279])).
% 0.72/0.45 cnf(s21, plain, spl27_41 | spl27_42, inference(sat_conversion,[],[f288])).
% 0.72/0.45 cnf(s22, plain, spl27_43 | spl27_44, inference(sat_conversion,[],[f297])).
% 0.72/0.45 cnf(s23, plain, spl27_45 | spl27_46, inference(sat_conversion,[],[f306])).
% 0.72/0.45 cnf(s24, plain, spl27_47 | spl27_48, inference(sat_conversion,[],[f315])).
% 0.72/0.45 cnf(s25, plain, spl27_49 | spl27_50, inference(sat_conversion,[],[f324])).
% 0.72/0.45 cnf(s26, plain, spl27_51 | spl27_52, inference(sat_conversion,[],[f333])).
% 0.72/0.45 cnf(s27, plain, spl27_53 | spl27_54, inference(sat_conversion,[],[f342])).
% 0.72/0.45 cnf(s28, plain, spl27_55 | spl27_56, inference(sat_conversion,[],[f351])).
% 0.72/0.45 cnf(s29, plain, spl27_57 | spl27_58, inference(sat_conversion,[],[f360])).
% 0.72/0.45 cnf(s30, plain, spl27_59 | spl27_60, inference(sat_conversion,[],[f369])).
% 0.72/0.45 cnf(s31, plain, spl27_61 | spl27_62, inference(sat_conversion,[],[f378])).
% 0.72/0.45 cnf(s32, plain, spl27_63 | spl27_64, inference(sat_conversion,[],[f387])).
% 0.72/0.45 cnf(s33, plain, spl27_65 | spl27_66, inference(sat_conversion,[],[f396])).
% 0.72/0.45 cnf(s34, plain, spl27_67 | spl27_68, inference(sat_conversion,[],[f405])).
% 0.72/0.45 cnf(s35, plain, spl27_69 | spl27_70, inference(sat_conversion,[],[f414])).
% 0.72/0.45 cnf(s36, plain, spl27_71 | spl27_72, inference(sat_conversion,[],[f423])).
% 0.72/0.45 cnf(s37, plain, spl27_73 | spl27_74, inference(sat_conversion,[],[f432])).
% 0.72/0.45 cnf(s38, plain, spl27_75 | spl27_76, inference(sat_conversion,[],[f441])).
% 0.72/0.45 cnf(s39, plain, spl27_77 | spl27_78, inference(sat_conversion,[],[f450])).
% 0.72/0.45 cnf(s40, plain, spl27_79 | spl27_80, inference(sat_conversion,[],[f459])).
% 0.72/0.45 cnf(s41, plain, spl27_81 | spl27_82, inference(sat_conversion,[],[f468])).
% 0.72/0.45 cnf(s42, plain, spl27_83 | spl27_84, inference(sat_conversion,[],[f477])).
% 0.72/0.45 cnf(s43, plain, spl27_85 | spl27_86, inference(sat_conversion,[],[f486])).
% 0.72/0.45 cnf(s44, plain, spl27_87 | spl27_88, inference(sat_conversion,[],[f495])).
% 0.72/0.45 cnf(s45, plain, spl27_1 | spl27_89, inference(sat_conversion,[],[f500])).
% 0.72/0.45 cnf(s46, plain, spl27_3 | spl27_90, inference(sat_conversion,[],[f505])).
% 0.72/0.45 cnf(s47, plain, spl27_91 | spl27_92, inference(sat_conversion,[],[f514])).
% 0.72/0.45 cnf(s48, plain, spl27_93 | spl27_94, inference(sat_conversion,[],[f523])).
% 0.72/0.45 cnf(s49, plain, spl27_95 | spl27_96, inference(sat_conversion,[],[f532])).
% 0.72/0.45 cnf(s50, plain, spl27_97 | spl27_98, inference(sat_conversion,[],[f541])).
% 0.72/0.45 cnf(s51, plain, spl27_2 | spl27_99, inference(sat_conversion,[],[f546])).
% 0.72/0.45 cnf(s52, plain, spl27_4 | spl27_100, inference(sat_conversion,[],[f551])).
% 0.72/0.45 cnf(s53, plain, spl27_101 | spl27_102, inference(sat_conversion,[],[f560])).
% 0.72/0.45 cnf(s54, plain, spl27_103 | spl27_104, inference(sat_conversion,[],[f569])).
% 0.72/0.45 cnf(s55, plain, spl27_105 | spl27_106, inference(sat_conversion,[],[f578])).
% 0.72/0.45 cnf(s56, plain, spl27_107 | spl27_108, inference(sat_conversion,[],[f587])).
% 0.72/0.45 cnf(s57, plain, ~spl27_2 | ~spl27_4, inference(sat_conversion,[],[f590])).
% 0.72/0.45 cnf(s60, plain, ~spl27_37 | ~spl27_39, inference(sat_conversion,[],[f617])).
% 0.72/0.45 cnf(s61, plain, spl27_37 | spl27_39, inference(sat_conversion,[],[f620])).
% 0.72/0.45 cnf(s63, plain, ~spl27_61 | ~spl27_63, inference(sat_conversion,[],[f633])).
% 0.72/0.45 cnf(s64, plain, spl27_61 | spl27_63, inference(sat_conversion,[],[f636])).
% 0.72/0.45 cnf(s69, plain, spl27_95 | spl27_97, inference(sat_conversion,[],[f667])).
% 0.72/0.45 cnf(s71, plain, spl27_105 | spl27_107, inference(sat_conversion,[],[f677])).
% 0.72/0.45 cnf(s77, plain, spl27_22 | ~spl27_54 | spl27_112, inference(sat_conversion,[],[f738])).
% 0.72/0.45 cnf(s79, plain, ~spl27_65 | ~spl27_101 | spl27_112, inference(sat_conversion,[],[f752])).
% 0.72/0.45 cnf(s80, plain, ~spl27_83 | spl27_111 | spl27_114, inference(sat_conversion,[],[f761])).
% 0.72/0.45 cnf(s83, plain, ~spl27_5 | ~spl27_7 | ~spl27_87, inference(sat_conversion,[],[f790])).
% 0.72/0.45 cnf(s84, plain, ~spl27_6 | ~spl27_62 | spl27_113, inference(sat_conversion,[],[f793])).
% 0.72/0.45 cnf(s85, plain, ~spl27_9 | ~spl27_69 | spl27_109, inference(sat_conversion,[],[f794])).
% 0.72/0.45 cnf(s86, plain, spl27_9 | ~spl27_69 | ~spl27_109, inference(sat_conversion,[],[f796])).
% 0.72/0.45 cnf(s87, plain, ~spl27_11 | ~spl27_69 | spl27_110, inference(sat_conversion,[],[f797])).
% 0.72/0.45 cnf(s90, plain, spl27_69 | spl27_72, inference(sat_conversion,[],[f807])).
% 0.72/0.45 cnf(s91, plain, ~spl27_13 | ~spl27_51 | spl27_115, inference(sat_conversion,[],[f813])).
% 0.72/0.45 cnf(s92, plain, ~spl27_17 | ~spl27_81 | spl27_111, inference(sat_conversion,[],[f817])).
% 0.72/0.45 cnf(s93, plain, ~spl27_21 | ~spl27_67 | spl27_112, inference(sat_conversion,[],[f821])).
% 0.72/0.45 cnf(s96, plain, ~spl27_39 | ~spl27_45 | ~spl27_47, inference(sat_conversion,[],[f843])).
% 0.72/0.45 cnf(s99, plain, spl27_50 | spl27_51, inference(sat_conversion,[],[f854])).
% 0.72/0.45 cnf(s100, plain, ~spl27_13 | ~spl27_50 | ~spl27_77 | ~spl27_86, inference(sat_conversion,[],[f861])).
% 0.72/0.45 cnf(s101, plain, ~spl27_40 | ~spl27_97 | ~spl27_106 | ~spl27_107, inference(sat_conversion,[],[f865])).
% 0.72/0.45 cnf(s110, plain, ~spl27_49 | ~spl27_93 | spl27_115, inference(sat_conversion,[],[f901])).
% 0.72/0.45 cnf(s112, plain, ~spl27_43 | ~spl27_70 | ~spl27_71, inference(sat_conversion,[],[f923])).
% 0.72/0.45 cnf(s114, plain, ~spl27_33 | ~spl27_39 | ~spl27_45 | ~spl27_79, inference(sat_conversion,[],[f943])).
% 0.72/0.45 cnf(s115, plain, ~spl27_77 | ~spl27_80, inference(sat_conversion,[],[f946])).
% 0.72/0.45 cnf(s117, plain, spl27_15 | ~spl27_51 | ~spl27_80 | ~spl27_86, inference(sat_conversion,[],[f962])).
% 0.72/0.45 cnf(s120, plain, ~spl27_9 | ~spl27_11 | ~spl27_72, inference(sat_conversion,[],[f988])).
% 0.72/0.45 cnf(s121, plain, ~spl27_41 | ~spl27_44, inference(sat_conversion,[],[f991])).
% 0.72/0.45 cnf(s124, plain, ~spl27_38 | ~spl27_42 | ~spl27_71 | ~spl27_107, inference(sat_conversion,[],[f1004])).
% 0.72/0.45 cnf(s127, plain, ~spl27_48 | ~spl27_80 | ~spl27_86 | ~spl27_92, inference(sat_conversion,[],[f1033])).
% 0.72/0.45 cnf(s129, plain, ~spl27_80 | ~spl27_88 | spl27_115, inference(sat_conversion,[],[f1036])).
% 0.72/0.45 cnf(s130, plain, spl27_5 | ~spl27_85 | ~spl27_113, inference(sat_conversion,[],[f1042])).
% 0.72/0.45 cnf(s131, plain, ~spl27_5 | ~spl27_85 | spl27_113, inference(sat_conversion,[],[f1044])).
% 0.72/0.45 cnf(s132, plain, ~spl27_7 | ~spl27_85 | spl27_116, inference(sat_conversion,[],[f1046])).
% 0.72/0.45 cnf(s134, plain, ~spl27_42 | ~spl27_70 | ~spl27_71, inference(sat_conversion,[],[f1064])).
% 0.72/0.45 cnf(s135, plain, ~spl27_43 | spl27_70 | ~spl27_81 | ~spl27_96, inference(sat_conversion,[],[f1069])).
% 0.72/0.45 cnf(s136, plain, ~spl27_52 | ~spl27_80 | spl27_86 | ~spl27_93, inference(sat_conversion,[],[f1084])).
% 0.72/0.45 cnf(s137, plain, ~spl27_92 | ~spl27_94, inference(sat_conversion,[],[f1087])).
% 0.72/0.45 cnf(s138, plain, ~spl27_48 | spl27_92 | ~spl27_115, inference(sat_conversion,[],[f1090])).
% 0.72/0.45 cnf(s140, plain, ~spl27_38 | ~spl27_40 | ~spl27_105, inference(sat_conversion,[],[f1098])).
% 0.72/0.45 cnf(s141, plain, ~spl27_37 | ~spl27_45 | spl27_109, inference(sat_conversion,[],[f1109])).
% 0.72/0.45 cnf(s144, plain, ~spl27_37 | ~spl27_47 | spl27_110, inference(sat_conversion,[],[f1114])).
% 0.72/0.45 cnf(s145, plain, ~spl27_13 | ~spl27_15 | ~spl27_50, inference(sat_conversion,[],[f1121])).
% 0.72/0.45 cnf(s146, plain, ~spl27_14 | ~spl27_16, inference(sat_conversion,[],[f1124])).
% 0.72/0.45 cnf(s150, plain, ~spl27_109 | ~spl27_110, inference(sat_conversion,[],[f1172])).
% 0.72/0.45 cnf(s152, plain, ~spl27_43 | ~spl27_70 | ~spl27_81 | ~spl27_98, inference(sat_conversion,[],[f1185])).
% 0.72/0.45 cnf(s155, plain, ~spl27_40 | ~spl27_43 | spl27_71 | ~spl27_105, inference(sat_conversion,[],[f1209])).
% 0.72/0.45 cnf(s158, plain, spl27_81 | spl27_84, inference(sat_conversion,[],[f1219])).
% 0.72/0.45 cnf(s160, plain, ~spl27_18 | ~spl27_19 | ~spl27_41 | ~spl27_84, inference(sat_conversion,[],[f1234])).
% 0.72/0.45 cnf(s161, plain, ~spl27_18 | ~spl27_20, inference(sat_conversion,[],[f1238])).
% 0.72/0.45 cnf(s162, plain, spl27_18 | ~spl27_41 | spl27_111, inference(sat_conversion,[],[f1246])).
% 0.72/0.45 cnf(s165, plain, spl27_38 | ~spl27_84 | ~spl27_96 | ~spl27_107, inference(sat_conversion,[],[f1278])).
% 0.72/0.45 cnf(s167, plain, ~spl27_38 | ~spl27_40 | ~spl27_107, inference(sat_conversion,[],[f1285])).
% 0.72/0.45 cnf(s169, plain, ~spl27_23 | ~spl27_67 | ~spl27_112, inference(sat_conversion,[],[f1300])).
% 0.72/0.45 cnf(s171, plain, ~spl27_24 | ~spl27_54 | spl27_112, inference(sat_conversion,[],[f1308])).
% 0.72/0.45 cnf(s174, plain, ~spl27_28 | ~spl27_74 | spl27_112, inference(sat_conversion,[],[f1319])).
% 0.72/0.45 cnf(s175, plain, ~spl27_55 | ~spl27_57 | ~spl27_76 | ~spl27_100, inference(sat_conversion,[],[f1325])).
% 0.72/0.45 cnf(s176, plain, ~spl27_54 | ~spl27_56, inference(sat_conversion,[],[f1328])).
% 0.72/0.45 cnf(s178, plain, spl27_73 | spl27_76, inference(sat_conversion,[],[f1342])).
% 0.72/0.45 cnf(s180, plain, ~spl27_29 | spl27_30 | ~spl27_58 | ~spl27_89, inference(sat_conversion,[],[f1362])).
% 0.72/0.45 cnf(s181, plain, spl27_29 | spl27_31, inference(sat_conversion,[],[f1366])).
% 0.72/0.45 cnf(s182, plain, ~spl27_30 | ~spl27_32 | ~spl27_58, inference(sat_conversion,[],[f1384])).
% 0.72/0.45 cnf(s183, plain, ~spl27_31 | spl27_57 | ~spl27_76 | ~spl27_89, inference(sat_conversion,[],[f1387])).
% 0.72/0.45 cnf(s184, plain, ~spl27_30 | spl27_57 | ~spl27_58 | ~spl27_73, inference(sat_conversion,[],[f1393])).
% 0.72/0.45 cnf(s185, plain, ~spl27_30 | ~spl27_53 | ~spl27_58 | ~spl27_100, inference(sat_conversion,[],[f1407])).
% 0.72/0.45 cnf(s186, plain, ~spl27_1 | ~spl27_3, inference(sat_conversion,[],[f1412])).
% 0.72/0.45 cnf(s188, plain, ~spl27_30 | ~spl27_58 | ~spl27_60 | ~spl27_73, inference(sat_conversion,[],[f1435])).
% 0.72/0.45 cnf(s190, plain, ~spl27_28 | ~spl27_75 | ~spl27_112, inference(sat_conversion,[],[f1452])).
% 0.72/0.45 cnf(s191, plain, ~spl27_24 | spl27_54 | ~spl27_112, inference(sat_conversion,[],[f1453])).
% 0.72/0.45 cnf(s194, plain, ~spl27_21 | ~spl27_25 | ~spl27_66 | ~spl27_75, inference(sat_conversion,[],[f1470])).
% 0.72/0.45 cnf(s195, plain, ~spl27_62 | ~spl27_64, inference(sat_conversion,[],[f1473])).
% 0.72/0.45 cnf(s196, plain, ~spl27_6 | spl27_62 | ~spl27_113, inference(sat_conversion,[],[f1476])).
% 0.72/0.45 cnf(s203, plain, ~spl27_27 | ~spl27_61 | spl27_113, inference(sat_conversion,[],[f1501])).
% 0.72/0.45 cnf(s204, plain, ~spl27_31 | ~spl27_55 | ~spl27_90 | ~spl27_99, inference(sat_conversion,[],[f1509])).
% 0.72/0.45 cnf(s205, plain, ~spl27_25 | ~spl27_74 | ~spl27_75, inference(sat_conversion,[],[f1533])).
% 0.72/0.45 cnf(s208, plain, ~spl27_102 | ~spl27_103, inference(sat_conversion,[],[f1544])).
% 0.72/0.45 cnf(s219, plain, ~spl27_25 | ~spl27_68 | ~spl27_74 | ~spl27_104, inference(sat_conversion,[],[f1588])).
% 0.72/0.45 cnf(s220, plain, ~spl27_22 | ~spl27_25 | spl27_54 | ~spl27_74, inference(sat_conversion,[],[f1592])).
% 0.72/0.45 cnf(s223, plain, ~spl27_14 | ~spl27_27 | ~spl27_63 | spl27_102, inference(sat_conversion,[],[f1615])).
% 0.72/0.45 cnf(s224, plain, ~spl27_34 | ~spl27_36, inference(sat_conversion,[],[f1620])).
% 0.72/0.45 cnf(s226, plain, spl27_77 | spl27_80, inference(sat_conversion,[],[f1634])).
% 0.72/0.45 cnf(s228, plain, ~spl27_35 | ~spl27_79 | ~spl27_109, inference(sat_conversion,[],[f1649])).
% 0.72/0.45 cnf(s229, plain, ~spl27_16 | spl27_102 | ~spl27_113, inference(sat_conversion,[],[f1656])).
% 0.72/0.45 cnf(s232, plain, spl27_9 | ~spl27_10 | ~spl27_34 | ~spl27_72, inference(sat_conversion,[],[f1673])).
% 0.72/0.45 cnf(s233, plain, ~spl27_13 | ~spl27_50 | ~spl27_52 | ~spl27_91, inference(sat_conversion,[],[f1683])).
% 0.72/0.45 cnf(s240, plain, ~spl27_84 | ~spl27_96 | ~spl27_98, inference(sat_conversion,[],[f1718])).
% 0.72/0.45 cnf(s242, plain, ~spl27_9 | ~spl27_39 | spl27_45 | ~spl27_72, inference(sat_conversion,[],[f1731])).
% 0.72/0.45 cnf(s243, plain, ~spl27_84 | ~spl27_96 | ~spl27_97 | ~spl27_108, inference(sat_conversion,[],[f1763])).
% 0.72/0.45 cnf(s245, plain, ~spl27_46 | ~spl27_77 | ~spl27_86 | ~spl27_92, inference(sat_conversion,[],[f1784])).
% 0.72/0.45 cnf(s253, plain, ~spl27_15 | ~spl27_51 | ~spl27_115, inference(sat_conversion,[],[f1816])).
% 0.72/0.45 cnf(s257, plain, ~spl27_55 | ~spl27_60 | ~spl27_76 | ~spl27_99, inference(sat_conversion,[],[f1888])).
% 0.72/0.45 cnf(s259, plain, ~spl27_32 | ~spl27_55 | ~spl27_59 | ~spl27_99, inference(sat_conversion,[],[f1911])).
% 0.72/0.45 cnf(s261, plain, ~spl27_8 | ~spl27_26 | ~spl27_63 | spl27_64, inference(sat_conversion,[],[f1920])).
% 0.72/0.45 cnf(s262, plain, ~spl27_8 | spl27_27 | ~spl27_62 | ~spl27_63, inference(sat_conversion,[],[f1922])).
% 0.72/0.45 cnf(s263, plain, spl27_22 | spl27_24, inference(sat_conversion,[],[f1933])).
% 0.72/0.45 cnf(s264, plain, ~spl27_26 | ~spl27_61 | ~spl27_113, inference(sat_conversion,[],[f1951])).
% 0.72/0.45 cnf(s274, plain, ~spl27_82 | ~spl27_111 | spl27_114, inference(sat_conversion,[],[f2007])).
% 0.72/0.45 cnf(s280, plain, ~spl27_35 | ~spl27_78 | spl27_109, inference(sat_conversion,[],[f2034])).
% 0.72/0.45 cnf(s286, plain, ~spl27_5 | ~spl27_8 | ~spl27_64 | ~spl27_87, inference(sat_conversion,[],[f2094])).
% 0.72/0.45 cnf(s293, plain, ~spl27_15 | ~spl27_50 | ~spl27_77 | ~spl27_88, inference(sat_conversion,[],[f2129])).
% 0.72/0.45 cnf(s296, plain, ~spl27_16 | ~spl27_102 | spl27_113, inference(sat_conversion,[],[f2164])).
% 0.72/0.45 cnf(s297, plain, ~spl27_16 | spl27_103 | ~spl27_116, inference(sat_conversion,[],[f2166])).
% 0.72/0.45 cnf(s299, plain, ~spl27_43 | ~spl27_71 | ~spl27_95 | ~spl27_106, inference(sat_conversion,[],[f2175])).
% 0.72/0.45 cnf(s300, plain, ~spl27_53 | ~spl27_57 | ~spl27_73 | ~spl27_100, inference(sat_conversion,[],[f2210])).
% 0.72/0.45 cnf(s301, plain, ~spl27_30 | ~spl27_31 | ~spl27_59 | ~spl27_90, inference(sat_conversion,[],[f2216])).
% 0.72/0.45 cnf(s302, plain, spl27_58 | spl27_59, inference(sat_conversion,[],[f2226])).
% 0.72/0.45 cnf(s303, plain, ~spl27_22 | ~spl27_23 | ~spl27_54 | ~spl27_66, inference(sat_conversion,[],[f2231])).
% 0.72/0.45 cnf(s307, plain, ~spl27_22 | ~spl27_25 | ~spl27_54 | spl27_74, inference(sat_conversion,[],[f2269])).
% 0.72/0.45 cnf(s310, plain, ~spl27_25 | ~spl27_65 | spl27_74 | ~spl27_104, inference(sat_conversion,[],[f2277])).
% 0.72/0.45 cnf(s316, plain, ~spl27_10 | ~spl27_33 | spl27_34 | ~spl27_78, inference(sat_conversion,[],[f2341])).
% 0.72/0.45 cnf(s324, plain, spl27_5 | ~spl27_14 | ~spl27_87 | ~spl27_102, inference(sat_conversion,[],[f2394])).
% 0.72/0.45 cnf(s326, plain, ~spl27_38 | ~spl27_43 | ~spl27_71 | ~spl27_105, inference(sat_conversion,[],[f2407])).
% 0.72/0.45 cnf(s333, plain, ~spl27_12 | ~spl27_34 | spl27_109, inference(sat_conversion,[],[f2444])).
% 0.72/0.45 cnf(s341, plain, ~spl27_17 | ~spl27_82 | ~spl27_84 | ~spl27_114, inference(sat_conversion,[],[f2475])).
% 0.72/0.45 cnf(s345, plain, spl27_18 | spl27_20, inference(sat_conversion,[],[f2491])).
% 0.72/0.45 cnf(s346, plain, ~spl27_19 | ~spl27_81 | ~spl27_111, inference(sat_conversion,[],[f2504])).
% 0.72/0.45 cnf(s348, plain, ~spl27_18 | spl27_41 | ~spl27_83 | ~spl27_114, inference(sat_conversion,[],[f2533])).
% 0.72/0.45 cnf(s349, plain, ~spl27_69 | ~spl27_72, inference(sat_conversion,[],[f2543])).
% 0.72/0.45 cnf(s350, plain, ~spl27_81 | ~spl27_84, inference(sat_conversion,[],[f2547])).
% 0.72/0.45 cnf(s360, plain, ~spl27_29 | ~spl27_53 | ~spl27_90 | ~spl27_99, inference(sat_conversion,[],[f2665])).
% 0.72/0.45 cnf(s363, plain, ~spl27_28 | ~spl27_68 | spl27_75 | ~spl27_101, inference(sat_conversion,[],[f2684])).
% 0.72/0.45 cnf(s364, plain, ~spl27_12 | ~spl27_36 | spl27_110, inference(sat_conversion,[],[f2691])).
% 0.72/0.45 cnf(s372, plain, ~spl27_42 | ~spl27_70 | ~spl27_84 | spl27_96, inference(sat_conversion,[],[f2753])).
% 0.72/0.45 cnf(s381, plain, ~spl27_20 | spl27_41 | ~spl27_111, inference(sat_conversion,[],[f2795])).
% 0.72/0.45 cnf(s387, plain, ~spl27_38 | ~spl27_95 | ~spl27_105 | ~spl27_108, inference(sat_conversion,[],[f2823])).
% 0.72/0.45 cnf(s394, plain, spl27_13 | ~spl27_51 | ~spl27_115, inference(sat_conversion,[],[f2880])).
% 0.72/0.45 cnf(s399, plain, ~spl27_46 | ~spl27_49 | ~spl27_91 | spl27_92, inference(sat_conversion,[],[f2933])).
% 0.72/0.45 cnf(s400, plain, spl27_41 | ~spl27_38 | ~spl27_71 | ~spl27_18, inference(rat,[],[s80,s348,s346,s42,s158,s243,s49,s69,s387,s56,s71,s124,s21,s10,s161])).
% 0.72/0.45 cnf(s401, plain, ~spl27_38 | ~spl27_71 | ~spl27_18, inference(rat,[],[s299,s49,s55,s135,s326,s112,s158,s22,s160,s121,s400,s10,s161])).
% 0.72/0.45 cnf(s402, plain, ~spl27_81 | spl27_41 | ~spl27_18, inference(rat,[],[s348,s80,s42,s346,s350,s10,s161])).
% 0.72/0.45 cnf(s405, plain, ~spl27_34 | ~spl27_88 | ~spl27_18 | spl27_13 | spl27_9, inference(rat,[],[s399,s47,s137,s48,s110,s394,s25,s99,s293,s23,s141,s19,s401,s39,s280,s86,s36,s90,s18,s232,s224,s5,s8,s146,s7])).
% 0.72/0.45 cnf(s406, plain, ~spl27_71 | ~spl27_70, inference(rat,[],[s121,s22,s21,s112,s134])).
% 0.72/0.45 cnf(s407, plain, spl27_41 | spl27_38 | ~spl27_70 | ~spl27_18, inference(rat,[],[s243,s56,s50,s165,s240,s372,s158,s402,s21])).
% 0.72/0.45 cnf(s408, plain, ~spl27_41 | ~spl27_70 | ~spl27_40 | ~spl27_18, inference(rat,[],[s101,s50,s55,s71,s152,s155,s158,s22,s160,s121,s10,s161,s406])).
% 0.72/0.45 cnf(s409, plain, ~spl27_38 | ~spl27_40, inference(rat,[],[s71,s140,s167])).
% 0.72/0.45 cnf(s410, plain, ~spl27_70 | ~spl27_40 | ~spl27_18, inference(rat,[],[s409,s407,s408])).
% 0.72/0.45 cnf(s411, plain, ~spl27_88 | ~spl27_18 | spl27_13 | spl27_9, inference(rat,[],[s410,s35,s86,s141,s20,s61,s114,s23,s399,s47,s137,s48,s110,s394,s25,s99,s40,s293,s115,s39,s316,s17,s405,s5,s8,s146,s7])).
% 0.72/0.45 cnf(s413, plain, ~spl27_27 | spl27_102 | ~spl27_14 | ~spl27_6, inference(rat,[],[s196,s195,s203,s32,s64,s223])).
% 0.72/0.45 cnf(s414, plain, spl27_112 | ~spl27_54 | ~spl27_101, inference(rat,[],[s303,s12,s33,s77,s171,s79])).
% 0.72/0.45 cnf(s415, plain, spl27_57 | ~spl27_76 | ~spl27_89, inference(rat,[],[s182,s180,s16,s181,s29,s183])).
% 0.72/0.45 cnf(s416, plain, ~spl27_54 | ~spl27_28 | ~spl27_101 | spl27_1, inference(rat,[],[s415,s175,s38,s190,s414,s28,s176,s45,s52,s57,s1])).
% 0.72/0.45 cnf(s417, plain, ~spl27_58 | ~spl27_53 | spl27_1, inference(rat,[],[s180,s15,s185,s45,s52,s57,s1])).
% 0.72/0.45 cnf(s418, plain, spl27_102 | ~spl27_14 | ~spl27_6 | spl27_1, inference(rat,[],[s169,s34,s12,s363,s191,s190,s174,s37,s300,s29,s417,s27,s416,s14,s413,s53,s52,s57,s1])).
% 0.72/0.45 cnf(s419, plain, spl27_57 | ~spl27_89, inference(rat,[],[s180,s15,s184,s178,s29,s415])).
% 0.72/0.45 cnf(s420, plain, spl27_50 | ~spl27_46 | spl27_13, inference(rat,[],[s399,s47,s137,s48,s110,s394,s25,s99])).
% 0.72/0.45 cnf(s421, plain, spl27_109 | ~spl27_37 | ~spl27_88 | spl27_13 | ~spl27_10, inference(rat,[],[s316,s17,s224,s18,s280,s39,s293,s420,s23,s141,s8,s146,s7])).
% 0.72/0.45 cnf(s422, plain, spl27_41 | ~spl27_70 | spl27_38 | spl27_18, inference(rat,[],[s243,s56,s50,s165,s240,s372,s158,s92,s21,s381,s345,s9])).
% 0.72/0.45 cnf(s423, plain, spl27_38 | ~spl27_88 | spl27_13 | spl27_9, inference(rat,[],[s274,s341,s41,s158,s152,s50,s101,s55,s71,s155,s22,s162,s121,s422,s406,s35,s86,s421,s20,s60,s19,s5,s9,s411])).
% 0.72/0.45 cnf(s424, plain, spl27_41 | ~spl27_71 | ~spl27_38 | ~spl27_17 | ~spl27_20, inference(rat,[],[s243,s49,s69,s387,s56,s71,s158,s124,s92,s21,s381])).
% 0.72/0.45 cnf(s425, plain, spl27_70 | ~spl27_38 | spl27_18, inference(rat,[],[s274,s341,s41,s158,s135,s49,s299,s55,s326,s22,s162,s121,s424,s36,s349,s35,s345,s9])).
% 0.72/0.45 cnf(s426, plain, spl27_13 | spl27_9 | spl27_5 | spl27_1, inference(rat,[],[s23,s114,s420,s40,s293,s115,s39,s316,s17,s232,s36,s406,s425,s20,s409,s423,s411,s44,s324,s418,s8,s146,s7,s3,s5])).
% 0.72/0.45 cnf(s427, plain, ~spl27_15 | ~spl27_13, inference(rat,[],[s91,s253,s99,s145])).
% 0.72/0.45 cnf(s428, plain, spl27_113 | ~spl27_16 | ~spl27_6 | spl27_1, inference(rat,[],[s169,s34,s12,s363,s191,s190,s174,s37,s300,s27,s416,s53,s296,s14,s203,s31,s84,s52,s57,s1,s419,s45])).
% 0.72/0.45 cnf(s429, plain, spl27_50 | ~spl27_46 | ~spl27_86 | spl27_15, inference(rat,[],[s399,s47,s245,s226,s117,s25,s99])).
% 0.72/0.45 cnf(s430, plain, spl27_109 | ~spl27_37 | ~spl27_86 | ~spl27_13 | ~spl27_10, inference(rat,[],[s316,s17,s224,s18,s280,s39,s100,s429,s23,s141,s427])).
% 0.72/0.45 cnf(s431, plain, spl27_18 | ~spl27_70 | spl27_38, inference(rat,[],[s274,s341,s41,s158,s152,s50,s101,s55,s71,s155,s22,s162,s121,s422,s9,s20,s60,s19,s406])).
% 0.72/0.45 cnf(s432, plain, spl27_38 | ~spl27_86 | ~spl27_13 | spl27_9, inference(rat,[],[s410,s431,s35,s86,s430,s20,s60,s19,s5])).
% 0.72/0.45 cnf(s433, plain, spl27_70 | ~spl27_38, inference(rat,[],[s36,s401,s349,s425,s35])).
% 0.72/0.45 cnf(s434, plain, spl27_9 | spl27_5 | spl27_1, inference(rat,[],[s23,s114,s429,s40,s100,s115,s39,s316,s17,s232,s36,s406,s433,s20,s409,s432,s43,s130,s428,s8,s427,s426,s5,s3])).
% 0.72/0.45 cnf(s435, plain, ~spl27_69 | ~spl27_37 | ~spl27_88 | spl27_13 | ~spl27_9, inference(rat,[],[s136,s48,s26,s127,s137,s394,s138,s129,s40,s228,s18,s364,s24,s6,s144,s87,s150,s85])).
% 0.72/0.45 cnf(s436, plain, spl27_38 | ~spl27_88 | spl27_13 | ~spl27_9, inference(rat,[],[s431,s410,s35,s435,s20,s60,s19])).
% 0.72/0.45 cnf(s437, plain, ~spl27_80 | ~spl27_48 | ~spl27_88 | spl27_13, inference(rat,[],[s136,s48,s26,s127,s137,s394,s138,s129])).
% 0.72/0.45 cnf(s438, plain, ~spl27_88 | spl27_13 | ~spl27_9, inference(rat,[],[s18,s228,s224,s333,s17,s114,s40,s437,s24,s96,s6,s242,s120,s36,s406,s20,s433,s409,s436])).
% 0.72/0.45 cnf(s439, plain, spl27_13 | spl27_5 | spl27_1, inference(rat,[],[s438,s44,s324,s418,s7,s3,s434])).
% 0.72/0.45 cnf(s440, plain, ~spl27_69 | ~spl27_37 | ~spl27_86 | ~spl27_13 | ~spl27_9, inference(rat,[],[s233,s47,s26,s99,s127,s117,s40,s228,s18,s364,s24,s6,s144,s87,s150,s85,s427])).
% 0.72/0.45 cnf(s441, plain, spl27_38 | ~spl27_86 | ~spl27_13 | ~spl27_9, inference(rat,[],[s431,s410,s35,s440,s20,s60,s19])).
% 0.72/0.45 cnf(s443, plain, ~spl27_79 | ~spl27_12 | ~spl27_45 | ~spl27_39, inference(rat,[],[s18,s228,s224,s333,s17,s114])).
% 0.72/0.45 cnf(s444, plain, spl27_5 | spl27_1, inference(rat,[],[s233,s47,s26,s99,s127,s117,s40,s443,s24,s96,s6,s242,s120,s36,s406,s20,s433,s409,s441,s43,s130,s428,s8,s427,s439,s434,s3])).
% 0.72/0.45 cnf(s445, plain, ~spl27_54 | ~spl27_104 | ~spl27_25 | spl27_1, inference(rat,[],[s194,s11,s33,s307,s310,s205,s38,s175,s28,s176,s52,s57,s1,s419,s45])).
% 0.72/0.45 cnf(s446, plain, ~spl27_87 | ~spl27_14 | spl27_1, inference(rat,[],[s93,s191,s11,s263,s34,s220,s219,s37,s300,s27,s445,s54,s208,s223,s262,s13,s31,s261,s63,s32,s286,s4,s83,s52,s57,s1,s419,s45,s444])).
% 0.72/0.45 cnf(s447, plain, spl27_13 | spl27_9 | spl27_1, inference(rat,[],[s23,s114,s420,s40,s293,s115,s39,s316,s17,s232,s36,s406,s20,s433,s409,s423,s44,s446,s8,s146,s7,s5])).
% 0.72/0.45 cnf(s449, plain, ~spl27_26 | ~spl27_8 | ~spl27_113, inference(rat,[],[s195,s261,s31,s64,s264])).
% 0.72/0.45 cnf(s450, plain, ~spl27_85 | ~spl27_16 | spl27_1, inference(rat,[],[s93,s191,s11,s263,s34,s220,s219,s37,s300,s27,s445,s13,s449,s4,s132,s54,s297,s208,s229,s131,s52,s57,s1,s419,s45,s444])).
% 0.72/0.45 cnf(s451, plain, spl27_9 | spl27_1, inference(rat,[],[s23,s114,s429,s40,s100,s115,s39,s316,s17,s232,s36,s406,s20,s433,s409,s432,s43,s450,s8,s427,s447,s5])).
% 0.72/0.45 cnf(s452, plain, spl27_13 | spl27_1, inference(rat,[],[s44,s446,s438,s7,s451])).
% 0.72/0.45 cnf(s453, plain, spl27_1, inference(rat,[],[s233,s47,s26,s99,s127,s117,s40,s24,s443,s96,s6,s242,s120,s36,s406,s20,s433,s409,s441,s43,s450,s8,s427,s452,s451])).
% 0.72/0.45 cnf(s454, plain, ~spl27_3, inference(rat,[],[s186,s453])).
% 0.72/0.45 cnf(s455, plain, spl27_90, inference(rat,[],[s46,s454])).
% 0.72/0.45 cnf(s456, plain, spl27_4, inference(rat,[],[s2,s454])).
% 0.72/0.45 cnf(s457, plain, ~spl27_2, inference(rat,[],[s57,s456])).
% 0.72/0.45 cnf(s458, plain, spl27_99, inference(rat,[],[s51,s457])).
% 0.72/0.45 cnf(s459, plain, ~spl27_54 | ~spl27_28 | ~spl27_101, inference(rat,[],[s30,s259,s257,s16,s38,s204,s190,s28,s414,s176,s458,s455])).
% 0.72/0.45 cnf(s460, plain, ~spl27_28 | ~spl27_101, inference(rat,[],[s169,s34,s12,s363,s191,s190,s174,s37,s188,s30,s302,s301,s15,s181,s360,s27,s459,s458,s455])).
% 0.72/0.45 cnf(s461, plain, spl27_102 | ~spl27_6 | ~spl27_14, inference(rat,[],[s460,s14,s413,s53])).
% 0.72/0.45 cnf(s462, plain, ~spl27_88 | spl27_13 | spl27_9, inference(rat,[],[s23,s114,s420,s40,s293,s115,s39,s316,s17,s232,s36,s406,s20,s433,s409,s423,s5,s8,s146,s7])).
% 0.72/0.45 cnf(s463, plain, spl27_5 | ~spl27_87 | ~spl27_14, inference(rat,[],[s461,s324,s3])).
% 0.72/0.45 cnf(s464, plain, ~spl27_54 | ~spl27_104 | ~spl27_25, inference(rat,[],[s194,s11,s33,s307,s310,s205,s38,s257,s30,s259,s16,s204,s28,s176,s458,s455])).
% 0.72/0.45 cnf(s465, plain, ~spl27_104 | ~spl27_25, inference(rat,[],[s93,s191,s11,s263,s34,s220,s219,s37,s188,s30,s302,s301,s15,s181,s360,s27,s464,s458,s455])).
% 0.72/0.45 cnf(s466, plain, ~spl27_87 | ~spl27_14, inference(rat,[],[s465,s54,s208,s223,s262,s13,s31,s261,s63,s32,s286,s4,s83,s463])).
% 0.72/0.45 cnf(s467, plain, spl27_13 | spl27_9, inference(rat,[],[s466,s44,s462,s7])).
% 0.72/0.45 cnf(s468, plain, spl27_113 | ~spl27_6 | ~spl27_16, inference(rat,[],[s14,s460,s203,s53,s31,s296,s84])).
% 0.72/0.45 cnf(s469, plain, ~spl27_86 | spl27_9, inference(rat,[],[s23,s114,s429,s40,s100,s115,s39,s316,s17,s232,s36,s406,s20,s433,s409,s432,s5,s427,s467])).
% 0.72/0.45 cnf(s470, plain, spl27_5 | spl27_9, inference(rat,[],[s468,s130,s3,s8,s427,s467,s43,s469])).
% 0.72/0.45 cnf(s471, plain, spl27_9, inference(rat,[],[s449,s13,s4,s465,s132,s54,s297,s208,s229,s131,s470,s43,s469,s8,s427,s467])).
% 0.72/0.45 cnf(s472, plain, spl27_13, inference(rat,[],[s44,s466,s438,s7,s471])).
% 0.72/0.45 cnf(s473, plain, ~spl27_15, inference(rat,[],[s427,s472])).
% 0.72/0.45 cnf(s474, plain, spl27_16, inference(rat,[],[s8,s473])).
% 0.72/0.45 cnf(s476, plain, ~spl27_86, inference(rat,[],[s233,s47,s26,s99,s127,s117,s40,s24,s443,s96,s6,s242,s120,s36,s406,s20,s433,s409,s441,s472,s473,s471])).
% 0.72/0.45 cnf(s477, plain, spl27_85, inference(rat,[],[s43,s476])).
% 0.72/0.45 cnf(s480, plain, spl27_5, inference(rat,[],[s468,s130,s3,s474,s477])).
% 0.72/0.45 cnf(s481, plain, spl27_113, inference(rat,[],[s131,s477,s480])).
% 0.72/0.45 cnf(s482, plain, spl27_102, inference(rat,[],[s229,s474,s481])).
% 0.72/0.45 cnf(s483, plain, ~spl27_103, inference(rat,[],[s208,s482])).
% 0.72/0.45 cnf(s484, plain, ~spl27_116, inference(rat,[],[s297,s474,s483])).
% 0.72/0.45 cnf(s485, plain, spl27_104, inference(rat,[],[s54,s483])).
% 0.72/0.45 cnf(s486, plain, ~spl27_7, inference(rat,[],[s132,s477,s484])).
% 0.72/0.45 cnf(s488, plain, ~spl27_25, inference(rat,[],[s465,s485])).
% 0.72/0.45 cnf(s489, plain, spl27_8, inference(rat,[],[s4,s486])).
% 0.72/0.45 cnf(s491, plain, spl27_26, inference(rat,[],[s13,s488])).
% 0.72/0.45 cnf(s493, plain, $false, inference(rat,[],[s449,s481,s489,s491])).
% 0.72/0.45 thf(f2934,plain,(
% 0.72/0.45 $false),
% 0.72/0.45 inference(avatar_sat_refutation,[],[s493])).
% 0.72/0.45 % SZS output end Proof for theBenchmark
% 0.72/0.45 % (886995)------------------------------
% 0.72/0.45 % (886995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (886995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (886995)CaDiCaL version: 2.1.3
% 0.72/0.45 % (886995)Termination reason: Refutation
% 0.72/0.45 % (886995)Time elapsed: 0.085 s
% 0.72/0.45 % (886995)Peak memory usage: 14 MB
% 0.72/0.45 % (886995)Instructions burned: 145 (million)
% 0.72/0.45 % (886984)Success in time 0.14 s
% 0.72/0.45 % Vampire exiting
%------------------------------------------------------------------------------