%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO500^1.005 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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.29s 0.38s
% Output : Refutation 1.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.005 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.19 % Computer : n015.cluster.edu
% 0.13/0.19 % Model : x86_64 x86_64
% 0.13/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.19 % Memory : 8046.5625MB
% 0.13/0.19 % OS : Linux 6.8.0-71-generic
% 0.13/0.19 % CPULimit : 300
% 0.13/0.19 % WCLimit : 300
% 0.13/0.19 % DateTime : Tue Sep 29 17:14:19 UTC 2026
% 0.13/0.19 % CPUTime :
% 0.13/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.22 Running higher-order theorem proving
% 0.13/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.34 % (3825607)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.29/0.34 % (3825617)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3966880005:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.29/0.34 % (3825613)lrs+10_16_si=on:nwc=1.5:random_seed=854308489:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.29/0.34 % (3825612)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3246159918:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.29/0.34 % (3825614)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=114236234:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.29/0.34 % (3825616)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1960864887:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.29/0.34 % (3825615)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=1511732516: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.29/0.34 % (3825614)Refutation not found, incomplete strategy
% 0.29/0.34 % (3825614)------------------------------
% 0.29/0.34 % (3825614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.34 % (3825614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.34 % (3825614)CaDiCaL version: 2.1.3
% 0.29/0.34 % (3825614)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.34 % (3825614)Time elapsed: 0.001 s
% 0.29/0.34 % (3825614)Peak memory usage: 12 MB
% 0.29/0.34 % (3825613)Refutation not found, incomplete strategy
% 0.29/0.34 % (3825613)------------------------------
% 0.29/0.34 % (3825613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.34 % (3825612)Refutation not found, incomplete strategy
% 0.29/0.34 % (3825612)------------------------------
% 0.29/0.34 % (3825612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.34 % (3825612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.34 % (3825612)CaDiCaL version: 2.1.3
% 0.29/0.34 % (3825613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.34 % (3825613)CaDiCaL version: 2.1.3
% 0.29/0.34 % (3825612)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.34 % (3825612)Time elapsed: 0.001 s
% 0.29/0.34 % (3825612)Peak memory usage: 12 MB
% 0.29/0.34 % (3825612)Instructions burned: 1 (million)
% 0.29/0.34 % (3825613)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.34 % (3825613)Time elapsed: 0.002 s
% 0.29/0.34 % (3825613)Peak memory usage: 12 MB
% 0.29/0.34 % (3825613)Instructions burned: 2 (million)
% 0.29/0.34 % (3825614)------------------------------
% 0.29/0.34 % (3825614)------------------------------
% 0.29/0.34 % (3825616)Refutation not found, incomplete strategy
% 0.29/0.34 % (3825616)------------------------------
% 0.29/0.34 % (3825616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.34 % (3825612)------------------------------
% 0.29/0.34 % (3825612)------------------------------
% 0.29/0.34 % (3825616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.34 % (3825616)CaDiCaL version: 2.1.3
% 0.29/0.34 % (3825613)------------------------------
% 0.29/0.34 % (3825613)------------------------------
% 0.29/0.34 % (3825616)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.34 % (3825616)Time elapsed: 0.002 s
% 0.29/0.34 % (3825616)Peak memory usage: 12 MB
% 0.29/0.34 % (3825616)Instructions burned: 3 (million)
% 0.29/0.34 % (3825616)------------------------------
% 0.29/0.34 % (3825616)------------------------------
% 0.29/0.34 % (3825618)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.29/0.34 % (3825618)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.29/0.34 % (3825618)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=1419376431:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.29/0.34 % (3825617)Instruction limit reached!
% 0.29/0.37 % (3825617)------------------------------
% 0.29/0.37 % (3825617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.37 % (3825617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.37 % (3825617)CaDiCaL version: 2.1.3
% 0.29/0.37 % (3825617)Termination reason: Instruction limit
% 0.29/0.37 % (3825617)Termination phase: Saturation
% 0.29/0.37 % (3825617)Time elapsed: 0.022 s
% 0.29/0.37 % (3825617)Peak memory usage: 12 MB
% 0.29/0.37 % (3825617)Instructions burned: 78 (million)
% 0.29/0.37 % (3825627)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.29/0.37 % (3825625)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2145197225:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.29/0.37 % (3825628)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2432494031:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.29/0.37 % (3825626)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=256843557:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.29/0.37 % (3825627)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1017580857:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.29/0.37 % (3825625)Instruction limit reached!
% 0.29/0.37 % (3825625)------------------------------
% 0.29/0.37 % (3825625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.37 % (3825625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.37 % (3825625)CaDiCaL version: 2.1.3
% 0.29/0.37 % (3825625)Termination reason: Instruction limit
% 0.29/0.37 % (3825625)Termination phase: Saturation
% 0.29/0.37 % (3825625)Time elapsed: 0.002 s
% 0.29/0.37 % (3825625)Peak memory usage: 12 MB
% 0.29/0.37 % (3825625)Instructions burned: 2 (million)
% 0.29/0.37 % (3825626)Instruction limit reached!
% 0.29/0.37 % (3825626)------------------------------
% 0.29/0.37 % (3825626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.37 % (3825626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.37 % (3825626)CaDiCaL version: 2.1.3
% 0.29/0.37 % (3825626)Termination reason: Instruction limit
% 0.29/0.37 % (3825626)Termination phase: Saturation
% 0.29/0.37 % (3825626)Time elapsed: 0.004 s
% 0.29/0.37 % (3825626)Peak memory usage: 11 MB
% 0.29/0.37 % (3825626)Instructions burned: 6 (million)
% 0.29/0.37 % (3825627)Instruction limit reached!
% 0.29/0.37 % (3825627)------------------------------
% 0.29/0.37 % (3825627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.37 % (3825627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.37 % (3825627)CaDiCaL version: 2.1.3
% 0.29/0.37 % (3825627)Termination reason: Instruction limit
% 0.29/0.37 % (3825627)Termination phase: Saturation
% 0.29/0.37 % (3825627)Time elapsed: 0.004 s
% 0.29/0.37 % (3825627)Peak memory usage: 12 MB
% 0.29/0.37 % (3825627)Instructions burned: 7 (million)
% 0.29/0.37 % (3825630)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.29/0.37 % (3825630)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.29/0.37 % (3825628)Instruction limit reached!
% 0.29/0.37 % (3825628)------------------------------
% 0.29/0.37 % (3825628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.37 % (3825628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.37 % (3825628)CaDiCaL version: 2.1.3
% 0.29/0.37 % (3825628)Termination reason: Instruction limit
% 0.29/0.37 % (3825628)Termination phase: Saturation
% 0.29/0.37 % (3825628)Time elapsed: 0.007 s
% 0.29/0.37 % (3825628)Peak memory usage: 12 MB
% 0.29/0.37 % (3825628)Instructions burned: 13 (million)
% 0.29/0.37 % (3825630)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1702063312: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.29/0.37 % (3825637)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.29/0.38 % (3825635)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=1862373675:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.29/0.38 % (3825636)lrs+10_1_si=on:cs=on:random_seed=3276877922:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.29/0.38 % (3825637)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=1089697762:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.29/0.38 % (3825635)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825635)------------------------------
% 0.29/0.38 % (3825635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825635)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825635)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825635)Time elapsed: 0.003 s
% 0.29/0.38 % (3825635)Peak memory usage: 12 MB
% 0.29/0.38 % (3825635)Instructions burned: 5 (million)
% 0.29/0.38 % (3825630)Instruction limit reached!
% 0.29/0.38 % (3825630)------------------------------
% 0.29/0.38 % (3825630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825630)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825630)Termination reason: Instruction limit
% 0.29/0.38 % (3825630)Termination phase: Saturation
% 0.29/0.38 % (3825630)Time elapsed: 0.015 s
% 0.29/0.38 % (3825630)Peak memory usage: 12 MB
% 0.29/0.38 % (3825630)Instructions burned: 30 (million)
% 0.29/0.38 % (3825637)Instruction limit reached!
% 0.29/0.38 % (3825637)------------------------------
% 0.29/0.38 % (3825637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825637)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825637)Termination reason: Instruction limit
% 0.29/0.38 % (3825637)Termination phase: Saturation
% 0.29/0.38 % (3825637)Time elapsed: 0.002 s
% 0.29/0.38 % (3825637)Peak memory usage: 12 MB
% 0.29/0.38 % (3825637)Instructions burned: 3 (million)
% 0.29/0.38 % (3825635)------------------------------
% 0.29/0.38 % (3825635)------------------------------
% 0.29/0.38 % (3825638)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2054917468:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.29/0.38 % (3825636)Instruction limit reached!
% 0.29/0.38 % (3825636)------------------------------
% 0.29/0.38 % (3825636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825636)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825636)Termination reason: Instruction limit
% 0.29/0.38 % (3825636)Termination phase: Saturation
% 0.29/0.38 % (3825636)Time elapsed: 0.004 s
% 0.29/0.38 % (3825636)Peak memory usage: 11 MB
% 0.29/0.38 % (3825636)Instructions burned: 10 (million)
% 0.29/0.38 % (3825638)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825638)------------------------------
% 0.29/0.38 % (3825638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825638)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825638)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825638)Time elapsed: 0.002 s
% 0.29/0.38 % (3825638)Peak memory usage: 12 MB
% 0.29/0.38 % (3825638)Instructions burned: 2 (million)
% 0.29/0.38 % (3825638)------------------------------
% 0.29/0.38 % (3825638)------------------------------
% 0.29/0.38 % (3825645)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3444892060:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.29/0.38 % (3825646)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1967873852:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.29/0.38 % (3825647)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1836461043:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.29/0.38 % (3825645)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825645)------------------------------
% 0.29/0.38 % (3825645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825645)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825645)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825645)Time elapsed: 0.002 s
% 0.29/0.38 % (3825645)Peak memory usage: 12 MB
% 0.29/0.38 % (3825645)Instructions burned: 2 (million)
% 0.29/0.38 % (3825646)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825646)------------------------------
% 0.29/0.38 % (3825646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825646)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825646)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825646)Time elapsed: 0.001 s
% 0.29/0.38 % (3825646)Peak memory usage: 12 MB
% 0.29/0.38 % (3825646)Instructions burned: 1 (million)
% 0.29/0.38 % (3825645)------------------------------
% 0.29/0.38 % (3825645)------------------------------
% 0.29/0.38 % (3825648)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1744490933:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.29/0.38 % (3825646)------------------------------
% 0.29/0.38 % (3825646)------------------------------
% 0.29/0.38 % (3825644)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=270953002:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.29/0.38 % (3825648)Instruction limit reached!
% 0.29/0.38 % (3825648)------------------------------
% 0.29/0.38 % (3825648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825648)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825648)Termination reason: Instruction limit
% 0.29/0.38 % (3825648)Termination phase: Saturation
% 0.29/0.38 % (3825648)Time elapsed: 0.008 s
% 0.29/0.38 % (3825648)Peak memory usage: 12 MB
% 0.29/0.38 % (3825648)Instructions burned: 15 (million)
% 0.29/0.38 % (3825653)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=593082477: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.29/0.38 % (3825654)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2189170585:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.29/0.38 % (3825653)Instruction limit reached!
% 0.29/0.38 % (3825653)------------------------------
% 0.29/0.38 % (3825653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825653)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825653)Termination reason: Instruction limit
% 0.29/0.38 % (3825653)Termination phase: Saturation
% 0.29/0.38 % (3825653)Time elapsed: 0.002 s
% 0.29/0.38 % (3825653)Peak memory usage: 11 MB
% 0.29/0.38 % (3825653)Instructions burned: 3 (million)
% 0.29/0.38 % (3825654)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825654)------------------------------
% 0.29/0.38 % (3825654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825654)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825654)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825654)Time elapsed: 0.001 s
% 0.29/0.38 % (3825654)Peak memory usage: 12 MB
% 0.29/0.38 % (3825654)Instructions burned: 2 (million)
% 0.29/0.38 % (3825618) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3825607-3825618"...
% 0.29/0.38 % (3825654)------------------------------
% 0.29/0.38 % (3825654)------------------------------
% 0.29/0.38 % (3825656)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=756954371:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.29/0.38 % (3825656)Refutation not found, incomplete strategy
% 0.29/0.38 % (3825656)------------------------------
% 0.29/0.38 % (3825656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.38 % (3825656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.38 % (3825656)CaDiCaL version: 2.1.3
% 0.29/0.38 % (3825656)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.38 % (3825656)Time elapsed: 0.001 s
% 0.29/0.38 % (3825656)Peak memory usage: 11 MB
% 0.29/0.38 % (3825656)Instructions burned: 1 (million)
% 0.29/0.38 % (3825656)------------------------------
% 0.29/0.38 % (3825656)------------------------------
% 0.29/0.38 % (3825618)...printing done.
% 0.29/0.38 % (3825618)Refutation found. Thanks to Tanya!
% 0.29/0.38 % SZS status Theorem for theBenchmark
% 0.29/0.38 % SZS output start Proof for theBenchmark
% 0.29/0.38 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.29/0.38 thf(func_def_0, type, x: $o).
% 0.29/0.38 thf(func_def_1, type, f0: ($o > $o)).
% 0.29/0.38 thf(func_def_2, type, f1: ($o > $o)).
% 0.29/0.38 thf(func_def_3, type, f2: ($o > $o)).
% 0.29/0.38 thf(func_def_4, type, f3: ($o > $o)).
% 0.29/0.38 thf(func_def_5, type, f4: ($o > $o)).
% 0.29/0.38 thf(func_def_9, type, sF0: $o).
% 0.29/0.38 thf(func_def_10, type, sF1: $o).
% 0.29/0.38 thf(func_def_11, type, sF2: $o).
% 0.29/0.38 thf(func_def_12, type, sF3: $o).
% 0.29/0.38 thf(func_def_13, type, sF4: $o).
% 0.29/0.38 thf(func_def_14, type, sF5: $o).
% 0.29/0.38 thf(func_def_15, type, sF6: $o).
% 0.29/0.38 thf(func_def_16, type, sF7: $o).
% 0.29/0.38 thf(func_def_17, type, sF8: $o).
% 0.29/0.38 thf(func_def_18, type, sF9: $o).
% 0.29/0.38 thf(func_def_19, type, sF10: $o).
% 0.29/0.38 thf(func_def_20, type, sF11: $o).
% 0.29/0.38 thf(func_def_21, type, sF12: $o).
% 0.29/0.38 thf(func_def_22, type, sF13: $o).
% 0.29/0.38 thf(func_def_23, type, sF14: $o).
% 0.29/0.38 thf(func_def_24, type, sF15: $o).
% 0.29/0.38 thf(func_def_25, type, sF16: $o).
% 0.29/0.38 thf(func_def_26, type, sF17: $o).
% 0.29/0.38 thf(func_def_27, type, sF18: $o).
% 0.29/0.38 thf(f1,conjecture,(
% 0.29/0.38 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.29/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kaminski5)).
% 0.29/0.38 thf(f2,negated_conjecture,(
% 0.29/0.38 ~ (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) = ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.29/0.38 inference(negated_conjecture,[status(cth)],[f1])).
% 0.29/0.38 thf(f3,plain,(
% 0.29/0.38 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.29/0.38 inference(flattening,[],[f2])).
% 0.29/0.38 thf(f4,plain,(
% 0.29/0.38 (((f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ x)))))))))) != ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ x)))))))))))))),
% 0.29/0.38 inference(cnf_transformation,[],[f3])).
% 0.29/0.38 thf(f6,definition,(
% 0.29/0.38 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.29/0.38 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.29/0.38 thf(f7,definition,(
% 0.29/0.38 (sF0 = ((f4 @ x)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.29/0.38 thf(f8,plain,(
% 0.29/0.38 (((f4 @ x)) = sF0)),
% 0.29/0.38 inference(reorient_equations,[],[f7])).
% 0.29/0.38 thf(f9,definition,(
% 0.29/0.38 (sF1 = ((f3 @ sF0)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.29/0.38 thf(f10,plain,(
% 0.29/0.38 (((f3 @ sF0)) = sF1)),
% 0.29/0.38 inference(reorient_equations,[],[f9])).
% 0.29/0.38 thf(f11,definition,(
% 0.29/0.38 (sF2 = ((f3 @ sF1)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.29/0.38 thf(f12,plain,(
% 0.29/0.38 (((f3 @ sF1)) = sF2)),
% 0.29/0.38 inference(reorient_equations,[],[f11])).
% 0.29/0.38 thf(f13,definition,(
% 0.29/0.38 (sF3 = ((f3 @ sF2)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.29/0.38 thf(f14,plain,(
% 0.29/0.38 (((f3 @ sF2)) = sF3)),
% 0.29/0.38 inference(reorient_equations,[],[f13])).
% 0.29/0.38 thf(f15,definition,(
% 0.29/0.38 (sF4 = ((f2 @ sF3)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.29/0.38 thf(f16,plain,(
% 0.29/0.38 (((f2 @ sF3)) = sF4)),
% 0.29/0.38 inference(reorient_equations,[],[f15])).
% 0.29/0.38 thf(f17,definition,(
% 0.29/0.38 (sF5 = ((f1 @ sF4)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 0.29/0.38 thf(f18,plain,(
% 0.29/0.38 (((f1 @ sF4)) = sF5)),
% 0.29/0.38 inference(reorient_equations,[],[f17])).
% 0.29/0.38 thf(f19,definition,(
% 0.29/0.38 (sF6 = ((f1 @ sF5)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 0.29/0.38 thf(f20,definition,(
% 0.29/0.38 (sF7 = ((f1 @ sF6)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 0.29/0.38 thf(f21,definition,(
% 0.29/0.38 (sF8 = ((f0 @ sF7)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 0.29/0.38 thf(f22,plain,(
% 0.29/0.38 (((f0 @ sF7)) = sF8)),
% 0.29/0.38 inference(reorient_equations,[],[f21])).
% 0.29/0.38 thf(f23,definition,(
% 0.29/0.38 (sF9 = ((f4 @ sF0)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.29/0.38 thf(f24,definition,(
% 0.29/0.38 (sF10 = ((f4 @ sF9)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 0.29/0.38 thf(f25,definition,(
% 0.29/0.38 (sF11 = ((f3 @ sF10)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 0.29/0.38 thf(f26,definition,(
% 0.29/0.38 (sF12 = ((f2 @ sF11)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.29/0.38 thf(f27,definition,(
% 0.29/0.38 (sF13 = ((f2 @ sF12)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.29/0.38 thf(f28,plain,(
% 0.29/0.38 (((f2 @ sF12)) = sF13)),
% 0.29/0.38 inference(reorient_equations,[],[f27])).
% 0.29/0.38 thf(f29,definition,(
% 0.29/0.38 (sF14 = ((f2 @ sF13)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.29/0.38 thf(f30,plain,(
% 0.29/0.38 (((f2 @ sF13)) = sF14)),
% 0.29/0.38 inference(reorient_equations,[],[f29])).
% 0.29/0.38 thf(f31,definition,(
% 0.29/0.38 (sF15 = ((f1 @ sF14)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 0.29/0.38 thf(f32,definition,(
% 0.29/0.38 (sF16 = ((f0 @ sF15)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 0.29/0.38 thf(f33,plain,(
% 0.29/0.38 (((f0 @ sF15)) = sF16)),
% 0.29/0.38 inference(reorient_equations,[],[f32])).
% 0.29/0.38 thf(f34,definition,(
% 0.29/0.38 (sF17 = ((f0 @ sF16)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 0.29/0.38 thf(f35,plain,(
% 0.29/0.38 (((f0 @ sF16)) = sF17)),
% 0.29/0.38 inference(reorient_equations,[],[f34])).
% 0.29/0.38 thf(f36,definition,(
% 0.29/0.38 (sF18 = ((f0 @ sF17)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 0.29/0.38 thf(f37,plain,(
% 0.29/0.38 (sF18 != sF8)),
% 0.29/0.38 inference(definition_folding,[],[f4,f36,f35,f33,f31,f30,f28,f26,f25,f24,f23,f8,f22,f20,f19,f18,f16,f14,f12,f10,f8])).
% 0.29/0.38 thf(f38,plain,(
% 0.29/0.38 ($false = sF3) | ($true = ((f3 @ sF2)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f14])).
% 0.29/0.38 thf(f39,plain,(
% 0.29/0.38 ($false = ((f3 @ sF2))) | ($true = sF3)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f14])).
% 0.29/0.38 thf(f40,plain,(
% 0.29/0.38 ($false = ((f1 @ sF5))) | ($true = sF6)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f19])).
% 0.29/0.38 thf(f41,plain,(
% 0.29/0.38 ($false = sF6) | ($true = ((f1 @ sF5)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f19])).
% 0.29/0.38 thf(f42,plain,(
% 0.29/0.38 (sF10 = $true) | ($false = ((f4 @ sF9)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f24])).
% 0.29/0.38 thf(f43,plain,(
% 0.29/0.38 ($false = sF10) | ($true = ((f4 @ sF9)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f24])).
% 0.29/0.38 thf(f44,plain,(
% 0.29/0.38 ($false = sF4) | ($true = ((f2 @ sF3)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f16])).
% 0.29/0.38 thf(f45,plain,(
% 0.29/0.38 ($false = ((f2 @ sF3))) | ($true = sF4)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f16])).
% 0.29/0.38 thf(f46,plain,(
% 0.29/0.38 ($false = ((f1 @ sF14))) | ($true = sF15)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f31])).
% 0.29/0.38 thf(f47,plain,(
% 0.29/0.38 ($true = ((f1 @ sF14))) | ($false = sF15)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f31])).
% 0.29/0.38 thf(f48,plain,(
% 0.29/0.38 ($true = ((f3 @ sF1))) | ($false = sF2)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f12])).
% 0.29/0.38 thf(f49,plain,(
% 0.29/0.38 ($true = sF2) | ($false = ((f3 @ sF1)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f12])).
% 0.29/0.38 thf(f50,plain,(
% 0.29/0.38 ($false = sF1) | ($true = ((f3 @ sF0)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f10])).
% 0.29/0.38 thf(f51,plain,(
% 0.29/0.38 ($true = sF1) | ($false = ((f3 @ sF0)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f10])).
% 0.29/0.38 thf(f52,plain,(
% 0.29/0.38 ($true = ((f0 @ sF7))) | ($false = sF8)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f22])).
% 0.29/0.38 thf(f53,plain,(
% 0.29/0.38 ($false = ((f0 @ sF7))) | ($true = sF8)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f22])).
% 0.29/0.38 thf(f54,plain,(
% 0.29/0.38 ($true = ((f0 @ sF15))) | ($false = sF16)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f33])).
% 0.29/0.38 thf(f55,plain,(
% 0.29/0.38 ($true = sF16) | ($false = ((f0 @ sF15)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f33])).
% 0.29/0.38 thf(f56,plain,(
% 0.29/0.38 ($false = sF5) | (((f1 @ sF4)) = $true)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f18])).
% 0.29/0.38 thf(f57,plain,(
% 0.29/0.38 ($true = sF5) | ($false = ((f1 @ sF4)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f18])).
% 0.29/0.38 thf(f58,plain,(
% 0.29/0.38 ($false = sF13) | ($true = ((f2 @ sF12)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f28])).
% 0.29/0.38 thf(f59,plain,(
% 0.29/0.38 ($false = ((f2 @ sF12))) | ($true = sF13)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f28])).
% 0.29/0.38 thf(f60,plain,(
% 0.29/0.38 ($false = ((f1 @ sF6))) | ($true = sF7)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f20])).
% 0.29/0.38 thf(f61,plain,(
% 0.29/0.38 ($true = ((f1 @ sF6))) | ($false = sF7)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f20])).
% 0.29/0.38 thf(f62,plain,(
% 0.29/0.38 ($true = sF18) | ($false = ((f0 @ sF17)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f36])).
% 0.29/0.38 thf(f63,plain,(
% 0.29/0.38 ($true = ((f0 @ sF17))) | ($false = sF18)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f36])).
% 0.29/0.38 thf(f64,plain,(
% 0.29/0.38 ($true = ((f2 @ sF13))) | ($false = sF14)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f30])).
% 0.29/0.38 thf(f65,plain,(
% 0.29/0.38 ($true = sF14) | ($false = ((f2 @ sF13)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f30])).
% 0.29/0.38 thf(f66,plain,(
% 0.29/0.38 (((f4 @ x)) = $true) | ($false = sF0)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f8])).
% 0.29/0.38 thf(f67,plain,(
% 0.29/0.38 (((f4 @ x)) = $false) | ($true = sF0)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f8])).
% 0.29/0.38 thf(f68,plain,(
% 0.29/0.38 ($false = ((f4 @ sF0))) | (sF9 = $true)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f23])).
% 0.29/0.38 thf(f69,plain,(
% 0.29/0.38 ($false = sF9) | ($true = ((f4 @ sF0)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f23])).
% 0.29/0.38 thf(f70,plain,(
% 0.29/0.38 ($true = sF8) | ($true = sF18)),
% 0.29/0.38 inference(xor_proxy_clausification,[],[f37])).
% 0.29/0.38 thf(f71,plain,(
% 0.29/0.38 ($false = sF8) | ($false = sF18)),
% 0.29/0.38 inference(xor_proxy_clausification,[],[f37])).
% 0.29/0.38 thf(f72,plain,(
% 0.29/0.38 (sF11 = $true) | ($false = ((f3 @ sF10)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f25])).
% 0.29/0.38 thf(f73,plain,(
% 0.29/0.38 ($false = sF11) | ($true = ((f3 @ sF10)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f25])).
% 0.29/0.38 thf(f74,plain,(
% 0.29/0.38 (((f0 @ sF16)) = $true) | ($false = sF17)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f35])).
% 0.29/0.38 thf(f75,plain,(
% 0.29/0.38 ($false = ((f0 @ sF16))) | ($true = sF17)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f35])).
% 0.29/0.38 thf(f76,plain,(
% 0.29/0.38 ($false = ((f2 @ sF11))) | ($true = sF12)),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f26])).
% 0.29/0.38 thf(f77,plain,(
% 0.29/0.38 ($false = sF12) | ($true = ((f2 @ sF11)))),
% 0.29/0.38 inference(iff_proxy_clausification,[],[f26])).
% 0.29/0.38 thf(f79,definition,(
% 0.29/0.38 spl19_1 <=> ($false = ((f3 @ sF2)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition])).
% 0.29/0.38 thf(f80,plain,(
% 0.29/0.38 ($false != ((f3 @ sF2))) | spl19_1),
% 0.29/0.38 inference(avatar_component_clause,[],[f79])).
% 0.29/0.38 thf(f81,plain,(
% 0.29/0.38 ($false = ((f3 @ sF2))) | ~spl19_1),
% 0.29/0.38 inference(avatar_component_clause,[],[f79])).
% 0.29/0.38 thf(f83,definition,(
% 0.29/0.38 spl19_2 <=> ($true = sF3)),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition])).
% 0.29/0.38 thf(f85,plain,(
% 0.29/0.38 ($true = sF3) | ~spl19_2),
% 0.29/0.38 inference(avatar_component_clause,[],[f83])).
% 0.29/0.38 thf(f86,plain,(
% 0.29/0.38 spl19_1 | spl19_2),
% 0.29/0.38 inference(avatar_split_clause,[],[f39,f83,f79])).
% 0.29/0.38 thf(f88,definition,(
% 0.29/0.38 spl19_3 <=> ($false = sF3)),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition])).
% 0.29/0.38 thf(f90,plain,(
% 0.29/0.38 ($false = sF3) | ~spl19_3),
% 0.29/0.38 inference(avatar_component_clause,[],[f88])).
% 0.29/0.38 thf(f92,definition,(
% 0.29/0.38 spl19_4 <=> ($true = ((f3 @ sF2)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition])).
% 0.29/0.38 thf(f94,plain,(
% 0.29/0.38 ($true = ((f3 @ sF2))) | ~spl19_4),
% 0.29/0.38 inference(avatar_component_clause,[],[f92])).
% 0.29/0.38 thf(f95,plain,(
% 0.29/0.38 spl19_3 | spl19_4),
% 0.29/0.38 inference(avatar_split_clause,[],[f38,f92,f88])).
% 0.29/0.38 thf(f97,definition,(
% 0.29/0.38 spl19_5 <=> ($true = ((f1 @ sF5)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition])).
% 0.29/0.38 thf(f98,plain,(
% 0.29/0.38 ($true != ((f1 @ sF5))) | spl19_5),
% 0.29/0.38 inference(avatar_component_clause,[],[f97])).
% 0.29/0.38 thf(f99,plain,(
% 0.29/0.38 ($true = ((f1 @ sF5))) | ~spl19_5),
% 0.29/0.38 inference(avatar_component_clause,[],[f97])).
% 0.29/0.38 thf(f101,definition,(
% 0.29/0.38 spl19_6 <=> ($false = sF6)),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition])).
% 0.29/0.38 thf(f103,plain,(
% 0.29/0.38 ($false = sF6) | ~spl19_6),
% 0.29/0.38 inference(avatar_component_clause,[],[f101])).
% 0.29/0.38 thf(f104,plain,(
% 0.29/0.38 spl19_5 | spl19_6),
% 0.29/0.38 inference(avatar_split_clause,[],[f41,f101,f97])).
% 0.29/0.38 thf(f106,definition,(
% 0.29/0.38 spl19_7 <=> ($false = ((f1 @ sF5)))),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition])).
% 0.29/0.38 thf(f107,plain,(
% 0.29/0.38 ($false != ((f1 @ sF5))) | spl19_7),
% 0.29/0.38 inference(avatar_component_clause,[],[f106])).
% 0.29/0.38 thf(f108,plain,(
% 0.29/0.38 ($false = ((f1 @ sF5))) | ~spl19_7),
% 0.29/0.38 inference(avatar_component_clause,[],[f106])).
% 0.29/0.38 thf(f110,definition,(
% 0.29/0.38 spl19_8 <=> ($true = sF6)),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition])).
% 0.29/0.38 thf(f112,plain,(
% 0.29/0.38 ($true = sF6) | ~spl19_8),
% 0.29/0.38 inference(avatar_component_clause,[],[f110])).
% 0.29/0.38 thf(f113,plain,(
% 0.29/0.38 spl19_7 | spl19_8),
% 0.29/0.38 inference(avatar_split_clause,[],[f40,f110,f106])).
% 0.29/0.38 thf(f115,definition,(
% 0.29/0.38 spl19_9 <=> ($false = sF10)),
% 0.29/0.38 introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition])).
% 0.29/0.38 thf(f116,plain,(
% 0.29/0.38 ($false != sF10) | spl19_9),
% 0.29/0.38 inference(avatar_component_clause,[],[f115])).
% 0.29/0.38 thf(f117,plain,(
% 0.29/0.38 ($false = sF10) | ~spl19_9),
% 0.29/0.38 inference(avatar_component_clause,[],[f115])).
% 0.29/0.38 thf(f119,definition,(
% 0.29/0.38 spl19_10 <=> ($true = ((f4 @ sF9)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition])).
% 0.29/0.39 thf(f120,plain,(
% 0.29/0.39 ($true != ((f4 @ sF9))) | spl19_10),
% 0.29/0.39 inference(avatar_component_clause,[],[f119])).
% 0.29/0.39 thf(f121,plain,(
% 0.29/0.39 ($true = ((f4 @ sF9))) | ~spl19_10),
% 0.29/0.39 inference(avatar_component_clause,[],[f119])).
% 0.29/0.39 thf(f122,plain,(
% 0.29/0.39 spl19_9 | spl19_10),
% 0.29/0.39 inference(avatar_split_clause,[],[f43,f119,f115])).
% 0.29/0.39 thf(f124,definition,(
% 0.29/0.39 spl19_11 <=> (sF10 = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition])).
% 0.29/0.39 thf(f125,plain,(
% 0.29/0.39 (sF10 != $true) | spl19_11),
% 0.29/0.39 inference(avatar_component_clause,[],[f124])).
% 0.29/0.39 thf(f126,plain,(
% 0.29/0.39 (sF10 = $true) | ~spl19_11),
% 0.29/0.39 inference(avatar_component_clause,[],[f124])).
% 0.29/0.39 thf(f128,definition,(
% 0.29/0.39 spl19_12 <=> ($false = ((f4 @ sF9)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition])).
% 0.29/0.39 thf(f129,plain,(
% 0.29/0.39 ($false != ((f4 @ sF9))) | spl19_12),
% 0.29/0.39 inference(avatar_component_clause,[],[f128])).
% 0.29/0.39 thf(f130,plain,(
% 0.29/0.39 ($false = ((f4 @ sF9))) | ~spl19_12),
% 0.29/0.39 inference(avatar_component_clause,[],[f128])).
% 0.29/0.39 thf(f131,plain,(
% 0.29/0.39 spl19_11 | spl19_12),
% 0.29/0.39 inference(avatar_split_clause,[],[f42,f128,f124])).
% 0.29/0.39 thf(f133,definition,(
% 0.29/0.39 spl19_13 <=> ($false = ((f2 @ sF3)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition])).
% 0.29/0.39 thf(f134,plain,(
% 0.29/0.39 ($false != ((f2 @ sF3))) | spl19_13),
% 0.29/0.39 inference(avatar_component_clause,[],[f133])).
% 0.29/0.39 thf(f135,plain,(
% 0.29/0.39 ($false = ((f2 @ sF3))) | ~spl19_13),
% 0.29/0.39 inference(avatar_component_clause,[],[f133])).
% 0.29/0.39 thf(f137,definition,(
% 0.29/0.39 spl19_14 <=> ($true = sF4)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition])).
% 0.29/0.39 thf(f139,plain,(
% 0.29/0.39 ($true = sF4) | ~spl19_14),
% 0.29/0.39 inference(avatar_component_clause,[],[f137])).
% 0.29/0.39 thf(f140,plain,(
% 0.29/0.39 spl19_13 | spl19_14),
% 0.29/0.39 inference(avatar_split_clause,[],[f45,f137,f133])).
% 0.29/0.39 thf(f142,definition,(
% 0.29/0.39 spl19_15 <=> ($false = sF4)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition])).
% 0.29/0.39 thf(f144,plain,(
% 0.29/0.39 ($false = sF4) | ~spl19_15),
% 0.29/0.39 inference(avatar_component_clause,[],[f142])).
% 0.29/0.39 thf(f146,definition,(
% 0.29/0.39 spl19_16 <=> ($true = ((f2 @ sF3)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition])).
% 0.29/0.39 thf(f147,plain,(
% 0.29/0.39 ($true != ((f2 @ sF3))) | spl19_16),
% 0.29/0.39 inference(avatar_component_clause,[],[f146])).
% 0.29/0.39 thf(f148,plain,(
% 0.29/0.39 ($true = ((f2 @ sF3))) | ~spl19_16),
% 0.29/0.39 inference(avatar_component_clause,[],[f146])).
% 0.29/0.39 thf(f149,plain,(
% 0.29/0.39 spl19_15 | spl19_16),
% 0.29/0.39 inference(avatar_split_clause,[],[f44,f146,f142])).
% 0.29/0.39 thf(f151,definition,(
% 0.29/0.39 spl19_17 <=> ($false = sF15)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition])).
% 0.29/0.39 thf(f153,plain,(
% 0.29/0.39 ($false = sF15) | ~spl19_17),
% 0.29/0.39 inference(avatar_component_clause,[],[f151])).
% 0.29/0.39 thf(f155,definition,(
% 0.29/0.39 spl19_18 <=> ($true = ((f1 @ sF14)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition])).
% 0.29/0.39 thf(f156,plain,(
% 0.29/0.39 ($true != ((f1 @ sF14))) | spl19_18),
% 0.29/0.39 inference(avatar_component_clause,[],[f155])).
% 0.29/0.39 thf(f157,plain,(
% 0.29/0.39 ($true = ((f1 @ sF14))) | ~spl19_18),
% 0.29/0.39 inference(avatar_component_clause,[],[f155])).
% 0.29/0.39 thf(f158,plain,(
% 0.29/0.39 spl19_17 | spl19_18),
% 0.29/0.39 inference(avatar_split_clause,[],[f47,f155,f151])).
% 0.29/0.39 thf(f160,definition,(
% 0.29/0.39 spl19_19 <=> ($false = ((f1 @ sF14)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition])).
% 0.29/0.39 thf(f162,plain,(
% 0.29/0.39 ($false = ((f1 @ sF14))) | ~spl19_19),
% 0.29/0.39 inference(avatar_component_clause,[],[f160])).
% 0.29/0.39 thf(f164,definition,(
% 0.29/0.39 spl19_20 <=> ($true = sF15)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition])).
% 0.29/0.39 thf(f166,plain,(
% 0.29/0.39 ($true = sF15) | ~spl19_20),
% 0.29/0.39 inference(avatar_component_clause,[],[f164])).
% 0.29/0.39 thf(f167,plain,(
% 0.29/0.39 spl19_19 | spl19_20),
% 0.29/0.39 inference(avatar_split_clause,[],[f46,f164,f160])).
% 0.29/0.39 thf(f169,definition,(
% 0.29/0.39 spl19_21 <=> ($false = ((f3 @ sF1)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition])).
% 0.29/0.39 thf(f170,plain,(
% 0.29/0.39 ($false != ((f3 @ sF1))) | spl19_21),
% 0.29/0.39 inference(avatar_component_clause,[],[f169])).
% 0.29/0.39 thf(f171,plain,(
% 0.29/0.39 ($false = ((f3 @ sF1))) | ~spl19_21),
% 0.29/0.39 inference(avatar_component_clause,[],[f169])).
% 0.29/0.39 thf(f173,definition,(
% 0.29/0.39 spl19_22 <=> ($true = sF2)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition])).
% 0.29/0.39 thf(f174,plain,(
% 0.29/0.39 ($true != sF2) | spl19_22),
% 0.29/0.39 inference(avatar_component_clause,[],[f173])).
% 0.29/0.39 thf(f175,plain,(
% 0.29/0.39 ($true = sF2) | ~spl19_22),
% 0.29/0.39 inference(avatar_component_clause,[],[f173])).
% 0.29/0.39 thf(f176,plain,(
% 0.29/0.39 spl19_21 | spl19_22),
% 0.29/0.39 inference(avatar_split_clause,[],[f49,f173,f169])).
% 0.29/0.39 thf(f178,definition,(
% 0.29/0.39 spl19_23 <=> ($false = sF2)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition])).
% 0.29/0.39 thf(f180,plain,(
% 0.29/0.39 ($false = sF2) | ~spl19_23),
% 0.29/0.39 inference(avatar_component_clause,[],[f178])).
% 0.29/0.39 thf(f182,definition,(
% 0.29/0.39 spl19_24 <=> ($true = ((f3 @ sF1)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition])).
% 0.29/0.39 thf(f183,plain,(
% 0.29/0.39 ($true != ((f3 @ sF1))) | spl19_24),
% 0.29/0.39 inference(avatar_component_clause,[],[f182])).
% 0.29/0.39 thf(f184,plain,(
% 0.29/0.39 ($true = ((f3 @ sF1))) | ~spl19_24),
% 0.29/0.39 inference(avatar_component_clause,[],[f182])).
% 0.29/0.39 thf(f185,plain,(
% 0.29/0.39 spl19_23 | spl19_24),
% 0.29/0.39 inference(avatar_split_clause,[],[f48,f182,f178])).
% 0.29/0.39 thf(f187,definition,(
% 0.29/0.39 spl19_25 <=> ($true = sF1)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition])).
% 0.29/0.39 thf(f188,plain,(
% 0.29/0.39 ($true != sF1) | spl19_25),
% 0.29/0.39 inference(avatar_component_clause,[],[f187])).
% 0.29/0.39 thf(f189,plain,(
% 0.29/0.39 ($true = sF1) | ~spl19_25),
% 0.29/0.39 inference(avatar_component_clause,[],[f187])).
% 0.29/0.39 thf(f191,definition,(
% 0.29/0.39 spl19_26 <=> ($false = ((f3 @ sF0)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition])).
% 0.29/0.39 thf(f193,plain,(
% 0.29/0.39 ($false = ((f3 @ sF0))) | ~spl19_26),
% 0.29/0.39 inference(avatar_component_clause,[],[f191])).
% 0.29/0.39 thf(f194,plain,(
% 0.29/0.39 spl19_25 | spl19_26),
% 0.29/0.39 inference(avatar_split_clause,[],[f51,f191,f187])).
% 0.29/0.39 thf(f196,definition,(
% 0.29/0.39 spl19_27 <=> ($false = sF1)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition])).
% 0.29/0.39 thf(f198,plain,(
% 0.29/0.39 ($false = sF1) | ~spl19_27),
% 0.29/0.39 inference(avatar_component_clause,[],[f196])).
% 0.29/0.39 thf(f200,definition,(
% 0.29/0.39 spl19_28 <=> ($true = ((f3 @ sF0)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition])).
% 0.29/0.39 thf(f202,plain,(
% 0.29/0.39 ($true = ((f3 @ sF0))) | ~spl19_28),
% 0.29/0.39 inference(avatar_component_clause,[],[f200])).
% 0.29/0.39 thf(f203,plain,(
% 0.29/0.39 spl19_27 | spl19_28),
% 0.29/0.39 inference(avatar_split_clause,[],[f50,f200,f196])).
% 0.29/0.39 thf(f205,definition,(
% 0.29/0.39 spl19_29 <=> ($false = ((f0 @ sF7)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition])).
% 0.29/0.39 thf(f206,plain,(
% 0.29/0.39 ($false != ((f0 @ sF7))) | spl19_29),
% 0.29/0.39 inference(avatar_component_clause,[],[f205])).
% 0.29/0.39 thf(f207,plain,(
% 0.29/0.39 ($false = ((f0 @ sF7))) | ~spl19_29),
% 0.29/0.39 inference(avatar_component_clause,[],[f205])).
% 0.29/0.39 thf(f209,definition,(
% 0.29/0.39 spl19_30 <=> ($true = sF8)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_30])],[avatar_definition])).
% 0.29/0.39 thf(f211,plain,(
% 0.29/0.39 ($true = sF8) | ~spl19_30),
% 0.29/0.39 inference(avatar_component_clause,[],[f209])).
% 0.29/0.39 thf(f212,plain,(
% 0.29/0.39 spl19_29 | spl19_30),
% 0.29/0.39 inference(avatar_split_clause,[],[f53,f209,f205])).
% 0.29/0.39 thf(f214,definition,(
% 0.29/0.39 spl19_31 <=> ($false = sF8)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_31])],[avatar_definition])).
% 0.29/0.39 thf(f216,plain,(
% 0.29/0.39 ($false = sF8) | ~spl19_31),
% 0.29/0.39 inference(avatar_component_clause,[],[f214])).
% 0.29/0.39 thf(f218,definition,(
% 0.29/0.39 spl19_32 <=> ($true = ((f0 @ sF7)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_32])],[avatar_definition])).
% 0.29/0.39 thf(f219,plain,(
% 0.29/0.39 ($true != ((f0 @ sF7))) | spl19_32),
% 0.29/0.39 inference(avatar_component_clause,[],[f218])).
% 0.29/0.39 thf(f220,plain,(
% 0.29/0.39 ($true = ((f0 @ sF7))) | ~spl19_32),
% 0.29/0.39 inference(avatar_component_clause,[],[f218])).
% 0.29/0.39 thf(f221,plain,(
% 0.29/0.39 spl19_31 | spl19_32),
% 0.29/0.39 inference(avatar_split_clause,[],[f52,f218,f214])).
% 0.29/0.39 thf(f223,definition,(
% 0.29/0.39 spl19_33 <=> ($true = sF16)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition])).
% 0.29/0.39 thf(f224,plain,(
% 0.29/0.39 ($true != sF16) | spl19_33),
% 0.29/0.39 inference(avatar_component_clause,[],[f223])).
% 0.29/0.39 thf(f225,plain,(
% 0.29/0.39 ($true = sF16) | ~spl19_33),
% 0.29/0.39 inference(avatar_component_clause,[],[f223])).
% 0.29/0.39 thf(f227,definition,(
% 0.29/0.39 spl19_34 <=> ($false = ((f0 @ sF15)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_34])],[avatar_definition])).
% 0.29/0.39 thf(f229,plain,(
% 0.29/0.39 ($false = ((f0 @ sF15))) | ~spl19_34),
% 0.29/0.39 inference(avatar_component_clause,[],[f227])).
% 0.29/0.39 thf(f230,plain,(
% 0.29/0.39 spl19_33 | spl19_34),
% 0.29/0.39 inference(avatar_split_clause,[],[f55,f227,f223])).
% 0.29/0.39 thf(f232,definition,(
% 0.29/0.39 spl19_35 <=> ($false = sF16)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_35])],[avatar_definition])).
% 0.29/0.39 thf(f234,plain,(
% 0.29/0.39 ($false = sF16) | ~spl19_35),
% 0.29/0.39 inference(avatar_component_clause,[],[f232])).
% 0.29/0.39 thf(f236,definition,(
% 0.29/0.39 spl19_36 <=> ($true = ((f0 @ sF15)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_36])],[avatar_definition])).
% 0.29/0.39 thf(f238,plain,(
% 0.29/0.39 ($true = ((f0 @ sF15))) | ~spl19_36),
% 0.29/0.39 inference(avatar_component_clause,[],[f236])).
% 0.29/0.39 thf(f239,plain,(
% 0.29/0.39 spl19_35 | spl19_36),
% 0.29/0.39 inference(avatar_split_clause,[],[f54,f236,f232])).
% 0.29/0.39 thf(f241,definition,(
% 0.29/0.39 spl19_37 <=> ($false = ((f1 @ sF4)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_37])],[avatar_definition])).
% 0.29/0.39 thf(f243,plain,(
% 0.29/0.39 ($false = ((f1 @ sF4))) | ~spl19_37),
% 0.29/0.39 inference(avatar_component_clause,[],[f241])).
% 0.29/0.39 thf(f245,definition,(
% 0.29/0.39 spl19_38 <=> ($true = sF5)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_38])],[avatar_definition])).
% 0.29/0.39 thf(f247,plain,(
% 0.29/0.39 ($true = sF5) | ~spl19_38),
% 0.29/0.39 inference(avatar_component_clause,[],[f245])).
% 0.29/0.39 thf(f248,plain,(
% 0.29/0.39 spl19_37 | spl19_38),
% 0.29/0.39 inference(avatar_split_clause,[],[f57,f245,f241])).
% 0.29/0.39 thf(f250,definition,(
% 0.29/0.39 spl19_39 <=> (((f1 @ sF4)) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_39])],[avatar_definition])).
% 0.29/0.39 thf(f252,plain,(
% 0.29/0.39 (((f1 @ sF4)) = $true) | ~spl19_39),
% 0.29/0.39 inference(avatar_component_clause,[],[f250])).
% 0.29/0.39 thf(f254,definition,(
% 0.29/0.39 spl19_40 <=> ($false = sF5)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_40])],[avatar_definition])).
% 0.29/0.39 thf(f256,plain,(
% 0.29/0.39 ($false = sF5) | ~spl19_40),
% 0.29/0.39 inference(avatar_component_clause,[],[f254])).
% 0.29/0.39 thf(f257,plain,(
% 0.29/0.39 spl19_39 | spl19_40),
% 0.29/0.39 inference(avatar_split_clause,[],[f56,f254,f250])).
% 0.29/0.39 thf(f259,definition,(
% 0.29/0.39 spl19_41 <=> ($false = ((f2 @ sF12)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_41])],[avatar_definition])).
% 0.29/0.39 thf(f260,plain,(
% 0.29/0.39 ($false != ((f2 @ sF12))) | spl19_41),
% 0.29/0.39 inference(avatar_component_clause,[],[f259])).
% 0.29/0.39 thf(f261,plain,(
% 0.29/0.39 ($false = ((f2 @ sF12))) | ~spl19_41),
% 0.29/0.39 inference(avatar_component_clause,[],[f259])).
% 0.29/0.39 thf(f263,definition,(
% 0.29/0.39 spl19_42 <=> ($true = sF13)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_42])],[avatar_definition])).
% 0.29/0.39 thf(f264,plain,(
% 0.29/0.39 ($true != sF13) | spl19_42),
% 0.29/0.39 inference(avatar_component_clause,[],[f263])).
% 0.29/0.39 thf(f265,plain,(
% 0.29/0.39 ($true = sF13) | ~spl19_42),
% 0.29/0.39 inference(avatar_component_clause,[],[f263])).
% 0.29/0.39 thf(f266,plain,(
% 0.29/0.39 spl19_41 | spl19_42),
% 0.29/0.39 inference(avatar_split_clause,[],[f59,f263,f259])).
% 0.29/0.39 thf(f268,definition,(
% 0.29/0.39 spl19_43 <=> ($true = ((f2 @ sF12)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_43])],[avatar_definition])).
% 0.29/0.39 thf(f270,plain,(
% 0.29/0.39 ($true = ((f2 @ sF12))) | ~spl19_43),
% 0.29/0.39 inference(avatar_component_clause,[],[f268])).
% 0.29/0.39 thf(f272,definition,(
% 0.29/0.39 spl19_44 <=> ($false = sF13)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_44])],[avatar_definition])).
% 0.29/0.39 thf(f274,plain,(
% 0.29/0.39 ($false = sF13) | ~spl19_44),
% 0.29/0.39 inference(avatar_component_clause,[],[f272])).
% 0.29/0.39 thf(f275,plain,(
% 0.29/0.39 spl19_43 | spl19_44),
% 0.29/0.39 inference(avatar_split_clause,[],[f58,f272,f268])).
% 0.29/0.39 thf(f277,definition,(
% 0.29/0.39 spl19_45 <=> ($true = ((f1 @ sF6)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_45])],[avatar_definition])).
% 0.29/0.39 thf(f279,plain,(
% 0.29/0.39 ($true = ((f1 @ sF6))) | ~spl19_45),
% 0.29/0.39 inference(avatar_component_clause,[],[f277])).
% 0.29/0.39 thf(f281,definition,(
% 0.29/0.39 spl19_46 <=> ($false = sF7)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_46])],[avatar_definition])).
% 0.29/0.39 thf(f283,plain,(
% 0.29/0.39 ($false = sF7) | ~spl19_46),
% 0.29/0.39 inference(avatar_component_clause,[],[f281])).
% 0.29/0.39 thf(f284,plain,(
% 0.29/0.39 spl19_45 | spl19_46),
% 0.29/0.39 inference(avatar_split_clause,[],[f61,f281,f277])).
% 0.29/0.39 thf(f286,definition,(
% 0.29/0.39 spl19_47 <=> ($false = ((f1 @ sF6)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_47])],[avatar_definition])).
% 0.29/0.39 thf(f288,plain,(
% 0.29/0.39 ($false = ((f1 @ sF6))) | ~spl19_47),
% 0.29/0.39 inference(avatar_component_clause,[],[f286])).
% 0.29/0.39 thf(f290,definition,(
% 0.29/0.39 spl19_48 <=> ($true = sF7)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_48])],[avatar_definition])).
% 0.29/0.39 thf(f292,plain,(
% 0.29/0.39 ($true = sF7) | ~spl19_48),
% 0.29/0.39 inference(avatar_component_clause,[],[f290])).
% 0.29/0.39 thf(f293,plain,(
% 0.29/0.39 spl19_47 | spl19_48),
% 0.29/0.39 inference(avatar_split_clause,[],[f60,f290,f286])).
% 0.29/0.39 thf(f295,definition,(
% 0.29/0.39 spl19_49 <=> ($false = sF18)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_49])],[avatar_definition])).
% 0.29/0.39 thf(f297,plain,(
% 0.29/0.39 ($false = sF18) | ~spl19_49),
% 0.29/0.39 inference(avatar_component_clause,[],[f295])).
% 0.29/0.39 thf(f299,definition,(
% 0.29/0.39 spl19_50 <=> ($true = ((f0 @ sF17)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_50])],[avatar_definition])).
% 0.29/0.39 thf(f300,plain,(
% 0.29/0.39 ($true != ((f0 @ sF17))) | spl19_50),
% 0.29/0.39 inference(avatar_component_clause,[],[f299])).
% 0.29/0.39 thf(f301,plain,(
% 0.29/0.39 ($true = ((f0 @ sF17))) | ~spl19_50),
% 0.29/0.39 inference(avatar_component_clause,[],[f299])).
% 0.29/0.39 thf(f302,plain,(
% 0.29/0.39 spl19_49 | spl19_50),
% 0.29/0.39 inference(avatar_split_clause,[],[f63,f299,f295])).
% 0.29/0.39 thf(f304,definition,(
% 0.29/0.39 spl19_51 <=> ($true = sF18)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_51])],[avatar_definition])).
% 0.29/0.39 thf(f306,plain,(
% 0.29/0.39 ($true = sF18) | ~spl19_51),
% 0.29/0.39 inference(avatar_component_clause,[],[f304])).
% 0.29/0.39 thf(f308,definition,(
% 0.29/0.39 spl19_52 <=> ($false = ((f0 @ sF17)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_52])],[avatar_definition])).
% 0.29/0.39 thf(f310,plain,(
% 0.29/0.39 ($false = ((f0 @ sF17))) | ~spl19_52),
% 0.29/0.39 inference(avatar_component_clause,[],[f308])).
% 0.29/0.39 thf(f311,plain,(
% 0.29/0.39 spl19_51 | spl19_52),
% 0.29/0.39 inference(avatar_split_clause,[],[f62,f308,f304])).
% 0.29/0.39 thf(f313,definition,(
% 0.29/0.39 spl19_53 <=> ($false = ((f2 @ sF13)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_53])],[avatar_definition])).
% 0.29/0.39 thf(f314,plain,(
% 0.29/0.39 ($false != ((f2 @ sF13))) | spl19_53),
% 0.29/0.39 inference(avatar_component_clause,[],[f313])).
% 0.29/0.39 thf(f315,plain,(
% 0.29/0.39 ($false = ((f2 @ sF13))) | ~spl19_53),
% 0.29/0.39 inference(avatar_component_clause,[],[f313])).
% 0.29/0.39 thf(f317,definition,(
% 0.29/0.39 spl19_54 <=> ($true = sF14)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_54])],[avatar_definition])).
% 0.29/0.39 thf(f318,plain,(
% 0.29/0.39 ($true != sF14) | spl19_54),
% 0.29/0.39 inference(avatar_component_clause,[],[f317])).
% 0.29/0.39 thf(f319,plain,(
% 0.29/0.39 ($true = sF14) | ~spl19_54),
% 0.29/0.39 inference(avatar_component_clause,[],[f317])).
% 0.29/0.39 thf(f320,plain,(
% 0.29/0.39 spl19_53 | spl19_54),
% 0.29/0.39 inference(avatar_split_clause,[],[f65,f317,f313])).
% 0.29/0.39 thf(f322,definition,(
% 0.29/0.39 spl19_55 <=> ($true = ((f2 @ sF13)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_55])],[avatar_definition])).
% 0.29/0.39 thf(f323,plain,(
% 0.29/0.39 ($true != ((f2 @ sF13))) | spl19_55),
% 0.29/0.39 inference(avatar_component_clause,[],[f322])).
% 0.29/0.39 thf(f324,plain,(
% 0.29/0.39 ($true = ((f2 @ sF13))) | ~spl19_55),
% 0.29/0.39 inference(avatar_component_clause,[],[f322])).
% 0.29/0.39 thf(f326,definition,(
% 0.29/0.39 spl19_56 <=> ($false = sF14)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_56])],[avatar_definition])).
% 0.29/0.39 thf(f328,plain,(
% 0.29/0.39 ($false = sF14) | ~spl19_56),
% 0.29/0.39 inference(avatar_component_clause,[],[f326])).
% 0.29/0.39 thf(f329,plain,(
% 0.29/0.39 spl19_55 | spl19_56),
% 0.29/0.39 inference(avatar_split_clause,[],[f64,f326,f322])).
% 0.29/0.39 thf(f331,definition,(
% 0.29/0.39 spl19_57 <=> (((f4 @ x)) = $false)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_57])],[avatar_definition])).
% 0.29/0.39 thf(f332,plain,(
% 0.29/0.39 (((f4 @ x)) != $false) | spl19_57),
% 0.29/0.39 inference(avatar_component_clause,[],[f331])).
% 0.29/0.39 thf(f333,plain,(
% 0.29/0.39 (((f4 @ x)) = $false) | ~spl19_57),
% 0.29/0.39 inference(avatar_component_clause,[],[f331])).
% 0.29/0.39 thf(f335,definition,(
% 0.29/0.39 spl19_58 <=> ($true = sF0)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_58])],[avatar_definition])).
% 0.29/0.39 thf(f336,plain,(
% 0.29/0.39 ($true != sF0) | spl19_58),
% 0.29/0.39 inference(avatar_component_clause,[],[f335])).
% 0.29/0.39 thf(f337,plain,(
% 0.29/0.39 ($true = sF0) | ~spl19_58),
% 0.29/0.39 inference(avatar_component_clause,[],[f335])).
% 0.29/0.39 thf(f338,plain,(
% 0.29/0.39 spl19_57 | spl19_58),
% 0.29/0.39 inference(avatar_split_clause,[],[f67,f335,f331])).
% 0.29/0.39 thf(f340,definition,(
% 0.29/0.39 spl19_59 <=> ($false = sF0)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_59])],[avatar_definition])).
% 0.29/0.39 thf(f342,plain,(
% 0.29/0.39 ($false = sF0) | ~spl19_59),
% 0.29/0.39 inference(avatar_component_clause,[],[f340])).
% 0.29/0.39 thf(f344,definition,(
% 0.29/0.39 spl19_60 <=> (((f4 @ x)) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_60])],[avatar_definition])).
% 0.29/0.39 thf(f346,plain,(
% 0.29/0.39 (((f4 @ x)) = $true) | ~spl19_60),
% 0.29/0.39 inference(avatar_component_clause,[],[f344])).
% 0.29/0.39 thf(f347,plain,(
% 0.29/0.39 spl19_59 | spl19_60),
% 0.29/0.39 inference(avatar_split_clause,[],[f66,f344,f340])).
% 0.29/0.39 thf(f349,definition,(
% 0.29/0.39 spl19_61 <=> ($false = sF9)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_61])],[avatar_definition])).
% 0.29/0.39 thf(f350,plain,(
% 0.29/0.39 ($false != sF9) | spl19_61),
% 0.29/0.39 inference(avatar_component_clause,[],[f349])).
% 0.29/0.39 thf(f351,plain,(
% 0.29/0.39 ($false = sF9) | ~spl19_61),
% 0.29/0.39 inference(avatar_component_clause,[],[f349])).
% 0.29/0.39 thf(f353,definition,(
% 0.29/0.39 spl19_62 <=> ($true = ((f4 @ sF0)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_62])],[avatar_definition])).
% 0.29/0.39 thf(f355,plain,(
% 0.29/0.39 ($true = ((f4 @ sF0))) | ~spl19_62),
% 0.29/0.39 inference(avatar_component_clause,[],[f353])).
% 0.29/0.39 thf(f356,plain,(
% 0.29/0.39 spl19_61 | spl19_62),
% 0.29/0.39 inference(avatar_split_clause,[],[f69,f353,f349])).
% 0.29/0.39 thf(f358,definition,(
% 0.29/0.39 spl19_63 <=> (sF9 = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_63])],[avatar_definition])).
% 0.29/0.39 thf(f359,plain,(
% 0.29/0.39 (sF9 != $true) | spl19_63),
% 0.29/0.39 inference(avatar_component_clause,[],[f358])).
% 0.29/0.39 thf(f360,plain,(
% 0.29/0.39 (sF9 = $true) | ~spl19_63),
% 0.29/0.39 inference(avatar_component_clause,[],[f358])).
% 0.29/0.39 thf(f362,definition,(
% 0.29/0.39 spl19_64 <=> ($false = ((f4 @ sF0)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_64])],[avatar_definition])).
% 0.29/0.39 thf(f364,plain,(
% 0.29/0.39 ($false = ((f4 @ sF0))) | ~spl19_64),
% 0.29/0.39 inference(avatar_component_clause,[],[f362])).
% 0.29/0.39 thf(f365,plain,(
% 0.29/0.39 spl19_63 | spl19_64),
% 0.29/0.39 inference(avatar_split_clause,[],[f68,f362,f358])).
% 0.29/0.39 thf(f366,plain,(
% 0.29/0.39 spl19_49 | spl19_31),
% 0.29/0.39 inference(avatar_split_clause,[],[f71,f214,f295])).
% 0.29/0.39 thf(f367,plain,(
% 0.29/0.39 spl19_51 | spl19_30),
% 0.29/0.39 inference(avatar_split_clause,[],[f70,f209,f304])).
% 0.29/0.39 thf(f369,definition,(
% 0.29/0.39 spl19_65 <=> ($true = ((f3 @ sF10)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_65])],[avatar_definition])).
% 0.29/0.39 thf(f371,plain,(
% 0.29/0.39 ($true = ((f3 @ sF10))) | ~spl19_65),
% 0.29/0.39 inference(avatar_component_clause,[],[f369])).
% 0.29/0.39 thf(f373,definition,(
% 0.29/0.39 spl19_66 <=> ($false = sF11)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_66])],[avatar_definition])).
% 0.29/0.39 thf(f375,plain,(
% 0.29/0.39 ($false = sF11) | ~spl19_66),
% 0.29/0.39 inference(avatar_component_clause,[],[f373])).
% 0.29/0.39 thf(f376,plain,(
% 0.29/0.39 spl19_65 | spl19_66),
% 0.29/0.39 inference(avatar_split_clause,[],[f73,f373,f369])).
% 0.29/0.39 thf(f378,definition,(
% 0.29/0.39 spl19_67 <=> (sF11 = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_67])],[avatar_definition])).
% 0.29/0.39 thf(f380,plain,(
% 0.29/0.39 (sF11 = $true) | ~spl19_67),
% 0.29/0.39 inference(avatar_component_clause,[],[f378])).
% 0.29/0.39 thf(f382,definition,(
% 0.29/0.39 spl19_68 <=> ($false = ((f3 @ sF10)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_68])],[avatar_definition])).
% 0.29/0.39 thf(f383,plain,(
% 0.29/0.39 ($false != ((f3 @ sF10))) | spl19_68),
% 0.29/0.39 inference(avatar_component_clause,[],[f382])).
% 0.29/0.39 thf(f384,plain,(
% 0.29/0.39 ($false = ((f3 @ sF10))) | ~spl19_68),
% 0.29/0.39 inference(avatar_component_clause,[],[f382])).
% 0.29/0.39 thf(f385,plain,(
% 0.29/0.39 spl19_67 | spl19_68),
% 0.29/0.39 inference(avatar_split_clause,[],[f72,f382,f378])).
% 0.29/0.39 thf(f387,definition,(
% 0.29/0.39 spl19_69 <=> ($true = sF17)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_69])],[avatar_definition])).
% 0.29/0.39 thf(f388,plain,(
% 0.29/0.39 ($true != sF17) | spl19_69),
% 0.29/0.39 inference(avatar_component_clause,[],[f387])).
% 0.29/0.39 thf(f389,plain,(
% 0.29/0.39 ($true = sF17) | ~spl19_69),
% 0.29/0.39 inference(avatar_component_clause,[],[f387])).
% 0.29/0.39 thf(f391,definition,(
% 0.29/0.39 spl19_70 <=> ($false = ((f0 @ sF16)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_70])],[avatar_definition])).
% 0.29/0.39 thf(f393,plain,(
% 0.29/0.39 ($false = ((f0 @ sF16))) | ~spl19_70),
% 0.29/0.39 inference(avatar_component_clause,[],[f391])).
% 0.29/0.39 thf(f394,plain,(
% 0.29/0.39 spl19_69 | spl19_70),
% 0.29/0.39 inference(avatar_split_clause,[],[f75,f391,f387])).
% 0.29/0.39 thf(f396,definition,(
% 0.29/0.39 spl19_71 <=> (((f0 @ sF16)) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_71])],[avatar_definition])).
% 0.29/0.39 thf(f398,plain,(
% 0.29/0.39 (((f0 @ sF16)) = $true) | ~spl19_71),
% 0.29/0.39 inference(avatar_component_clause,[],[f396])).
% 0.29/0.39 thf(f400,definition,(
% 0.29/0.39 spl19_72 <=> ($false = sF17)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_72])],[avatar_definition])).
% 0.29/0.39 thf(f402,plain,(
% 0.29/0.39 ($false = sF17) | ~spl19_72),
% 0.29/0.39 inference(avatar_component_clause,[],[f400])).
% 0.29/0.39 thf(f403,plain,(
% 0.29/0.39 spl19_71 | spl19_72),
% 0.29/0.39 inference(avatar_split_clause,[],[f74,f400,f396])).
% 0.29/0.39 thf(f405,definition,(
% 0.29/0.39 spl19_73 <=> ($false = sF12)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_73])],[avatar_definition])).
% 0.29/0.39 thf(f406,plain,(
% 0.29/0.39 ($false != sF12) | spl19_73),
% 0.29/0.39 inference(avatar_component_clause,[],[f405])).
% 0.29/0.39 thf(f407,plain,(
% 0.29/0.39 ($false = sF12) | ~spl19_73),
% 0.29/0.39 inference(avatar_component_clause,[],[f405])).
% 0.29/0.39 thf(f409,definition,(
% 0.29/0.39 spl19_74 <=> ($true = ((f2 @ sF11)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_74])],[avatar_definition])).
% 0.29/0.39 thf(f411,plain,(
% 0.29/0.39 ($true = ((f2 @ sF11))) | ~spl19_74),
% 0.29/0.39 inference(avatar_component_clause,[],[f409])).
% 0.29/0.39 thf(f412,plain,(
% 0.29/0.39 spl19_73 | spl19_74),
% 0.29/0.39 inference(avatar_split_clause,[],[f77,f409,f405])).
% 0.29/0.39 thf(f414,definition,(
% 0.29/0.39 spl19_75 <=> ($false = ((f2 @ sF11)))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_75])],[avatar_definition])).
% 0.29/0.39 thf(f415,plain,(
% 0.29/0.39 ($false != ((f2 @ sF11))) | spl19_75),
% 0.29/0.39 inference(avatar_component_clause,[],[f414])).
% 0.29/0.39 thf(f416,plain,(
% 0.29/0.39 ($false = ((f2 @ sF11))) | ~spl19_75),
% 0.29/0.39 inference(avatar_component_clause,[],[f414])).
% 0.29/0.39 thf(f418,definition,(
% 0.29/0.39 spl19_76 <=> ($true = sF12)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl19_76])],[avatar_definition])).
% 0.29/0.39 thf(f419,plain,(
% 0.29/0.39 ($true != sF12) | spl19_76),
% 0.29/0.39 inference(avatar_component_clause,[],[f418])).
% 0.29/0.39 thf(f420,plain,(
% 0.29/0.39 ($true = sF12) | ~spl19_76),
% 0.29/0.39 inference(avatar_component_clause,[],[f418])).
% 0.29/0.39 thf(f421,plain,(
% 0.29/0.39 spl19_75 | spl19_76),
% 0.29/0.39 inference(avatar_split_clause,[],[f76,f418,f414])).
% 1.10/0.39 thf(f429,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_2 | ~spl19_3)),
% 1.10/0.39 inference(forward_demodulation,[],[f90,f85])).
% 1.10/0.39 thf(f430,plain,(
% 1.10/0.39 $false | (~spl19_2 | ~spl19_3)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f429])).
% 1.10/0.39 thf(f431,plain,(
% 1.10/0.39 ~spl19_2 | ~spl19_3),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f430])).
% 1.10/0.39 thf(f440,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_9 | ~spl19_11)),
% 1.10/0.39 inference(forward_demodulation,[],[f126,f117])).
% 1.10/0.39 thf(f441,plain,(
% 1.10/0.39 $false | (~spl19_9 | ~spl19_11)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f440])).
% 1.10/0.39 thf(f442,plain,(
% 1.10/0.39 ~spl19_9 | ~spl19_11),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f441])).
% 1.10/0.39 thf(f451,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_25 | ~spl19_27)),
% 1.10/0.39 inference(forward_demodulation,[],[f198,f189])).
% 1.10/0.39 thf(f452,plain,(
% 1.10/0.39 $false | (~spl19_25 | ~spl19_27)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f451])).
% 1.10/0.39 thf(f453,plain,(
% 1.10/0.39 ~spl19_25 | ~spl19_27),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f452])).
% 1.10/0.39 thf(f454,plain,(
% 1.10/0.39 ($false = sF1) | ($true != $true) | spl19_25),
% 1.10/0.39 inference(constrained_superposition,[],[f188,f6])).
% 1.10/0.39 thf(f455,plain,(
% 1.10/0.39 ($false = sF1) | spl19_25),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f454])).
% 1.10/0.39 thf(f456,plain,(
% 1.10/0.39 spl19_27 | spl19_25),
% 1.10/0.39 inference(avatar_split_clause,[],[f455,f187,f196])).
% 1.10/0.39 thf(f462,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_33 | ~spl19_35)),
% 1.10/0.39 inference(forward_demodulation,[],[f234,f225])).
% 1.10/0.39 thf(f463,plain,(
% 1.10/0.39 $false | (~spl19_33 | ~spl19_35)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f462])).
% 1.10/0.39 thf(f464,plain,(
% 1.10/0.39 ~spl19_33 | ~spl19_35),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f463])).
% 1.10/0.39 thf(f466,plain,(
% 1.10/0.39 ($false = sF16) | ($true != $true) | spl19_33),
% 1.10/0.39 inference(constrained_superposition,[],[f224,f6])).
% 1.10/0.39 thf(f467,plain,(
% 1.10/0.39 ($false = sF16) | spl19_33),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f466])).
% 1.10/0.39 thf(f468,plain,(
% 1.10/0.39 spl19_35 | spl19_33),
% 1.10/0.39 inference(avatar_split_clause,[],[f467,f223,f232])).
% 1.10/0.39 thf(f474,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_49 | ~spl19_51)),
% 1.10/0.39 inference(forward_demodulation,[],[f306,f297])).
% 1.10/0.39 thf(f475,plain,(
% 1.10/0.39 $false | (~spl19_49 | ~spl19_51)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f474])).
% 1.10/0.39 thf(f476,plain,(
% 1.10/0.39 ~spl19_49 | ~spl19_51),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f475])).
% 1.10/0.39 thf(f483,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_61 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f360,f351])).
% 1.10/0.39 thf(f484,plain,(
% 1.10/0.39 $false | (~spl19_61 | ~spl19_63)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f483])).
% 1.10/0.39 thf(f485,plain,(
% 1.10/0.39 ~spl19_61 | ~spl19_63),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f484])).
% 1.10/0.39 thf(f494,definition,(
% 1.10/0.39 spl19_77 <=> ($true = ((f1 @ $true)))),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_77])],[avatar_definition])).
% 1.10/0.39 thf(f496,plain,(
% 1.10/0.39 ($true = ((f1 @ $true))) | ~spl19_77),
% 1.10/0.39 inference(avatar_component_clause,[],[f494])).
% 1.10/0.39 thf(f501,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_5 | ~spl19_7)),
% 1.10/0.39 inference(forward_demodulation,[],[f108,f99])).
% 1.10/0.39 thf(f502,plain,(
% 1.10/0.39 $false | (~spl19_5 | ~spl19_7)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f501])).
% 1.10/0.39 thf(f503,plain,(
% 1.10/0.39 ~spl19_5 | ~spl19_7),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f502])).
% 1.10/0.39 thf(f508,plain,(
% 1.10/0.39 ($true = ((f4 @ $true))) | (~spl19_10 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f121,f360])).
% 1.10/0.39 thf(f509,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_3 | ~spl19_13)),
% 1.10/0.39 inference(forward_demodulation,[],[f135,f90])).
% 1.10/0.39 thf(f514,definition,(
% 1.10/0.39 spl19_78 <=> ($false = ((f1 @ $true)))),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_78])],[avatar_definition])).
% 1.10/0.39 thf(f516,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | ~spl19_78),
% 1.10/0.39 inference(avatar_component_clause,[],[f514])).
% 1.10/0.39 thf(f518,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_17 | ~spl19_20)),
% 1.10/0.39 inference(forward_demodulation,[],[f166,f153])).
% 1.10/0.39 thf(f519,plain,(
% 1.10/0.39 $false | (~spl19_17 | ~spl19_20)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f518])).
% 1.10/0.39 thf(f520,plain,(
% 1.10/0.39 ~spl19_17 | ~spl19_20),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f519])).
% 1.10/0.39 thf(f523,plain,(
% 1.10/0.39 ($true = ((f1 @ $true))) | ($false = sF14) | ~spl19_18),
% 1.10/0.39 inference(constrained_superposition,[],[f157,f6])).
% 1.10/0.39 thf(f524,plain,(
% 1.10/0.39 spl19_77 | spl19_56 | ~spl19_18),
% 1.10/0.39 inference(avatar_split_clause,[],[f523,f155,f326,f494])).
% 1.10/0.39 thf(f530,plain,(
% 1.10/0.39 ($false = ((f1 @ $false))) | (~spl19_19 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f162,f328])).
% 1.10/0.39 thf(f531,plain,(
% 1.10/0.39 ($false = ((f3 @ $false))) | (~spl19_21 | ~spl19_27)),
% 1.10/0.39 inference(forward_demodulation,[],[f171,f198])).
% 1.10/0.39 thf(f537,definition,(
% 1.10/0.39 spl19_79 <=> ($false = ((f0 @ $true)))),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_79])],[avatar_definition])).
% 1.10/0.39 thf(f539,plain,(
% 1.10/0.39 ($false = ((f0 @ $true))) | ~spl19_79),
% 1.10/0.39 inference(avatar_component_clause,[],[f537])).
% 1.10/0.39 thf(f542,plain,(
% 1.10/0.39 ($false = ((f0 @ $false))) | (~spl19_29 | ~spl19_46)),
% 1.10/0.39 inference(constrained_superposition,[],[f207,f283])).
% 1.10/0.39 thf(f544,plain,(
% 1.10/0.39 ($false = ((f0 @ $false))) | (~spl19_17 | ~spl19_34)),
% 1.10/0.39 inference(forward_demodulation,[],[f229,f153])).
% 1.10/0.39 thf(f547,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_41 | ~spl19_73)),
% 1.10/0.39 inference(forward_demodulation,[],[f261,f407])).
% 1.10/0.39 thf(f548,plain,(
% 1.10/0.39 ($true = ((f2 @ $false))) | (~spl19_43 | ~spl19_73)),
% 1.10/0.39 inference(forward_demodulation,[],[f270,f407])).
% 1.10/0.39 thf(f549,plain,(
% 1.10/0.39 ($true = ((f1 @ $false))) | (~spl19_6 | ~spl19_45)),
% 1.10/0.39 inference(forward_demodulation,[],[f279,f103])).
% 1.10/0.39 thf(f551,plain,(
% 1.10/0.39 ($true = ((f0 @ $true))) | (~spl19_50 | ~spl19_69)),
% 1.10/0.39 inference(forward_demodulation,[],[f301,f389])).
% 1.10/0.39 thf(f556,definition,(
% 1.10/0.39 spl19_80 <=> ($false = ((f2 @ $true)))),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_80])],[avatar_definition])).
% 1.10/0.39 thf(f563,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_53 | ~spl19_55)),
% 1.10/0.39 inference(forward_demodulation,[],[f324,f315])).
% 1.10/0.39 thf(f564,plain,(
% 1.10/0.39 $false | (~spl19_53 | ~spl19_55)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f563])).
% 1.10/0.39 thf(f565,plain,(
% 1.10/0.39 ~spl19_53 | ~spl19_55),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f564])).
% 1.10/0.39 thf(f571,definition,(
% 1.10/0.39 spl19_81 <=> ($false = ((f4 @ $true)))),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_81])],[avatar_definition])).
% 1.10/0.39 thf(f575,definition,(
% 1.10/0.39 spl19_82 <=> (x = $false)),
% 1.10/0.39 introduced(definition,[new_symbols(definition,[spl19_82])],[avatar_definition])).
% 1.10/0.39 thf(f576,plain,(
% 1.10/0.39 (x != $false) | spl19_82),
% 1.10/0.39 inference(avatar_component_clause,[],[f575])).
% 1.10/0.39 thf(f577,plain,(
% 1.10/0.39 (x = $false) | ~spl19_82),
% 1.10/0.39 inference(avatar_component_clause,[],[f575])).
% 1.10/0.39 thf(f579,plain,(
% 1.10/0.39 ($true = ((f3 @ $true))) | (~spl19_11 | ~spl19_65)),
% 1.10/0.39 inference(forward_demodulation,[],[f371,f126])).
% 1.10/0.39 thf(f580,plain,(
% 1.10/0.39 (((f0 @ $false)) = $true) | (~spl19_35 | ~spl19_71)),
% 1.10/0.39 inference(forward_demodulation,[],[f398,f234])).
% 1.10/0.39 thf(f599,plain,(
% 1.10/0.39 ($true = ((f2 @ $false))) | (~spl19_3 | ~spl19_16)),
% 1.10/0.39 inference(forward_demodulation,[],[f148,f90])).
% 1.10/0.39 thf(f600,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_3 | ~spl19_13 | ~spl19_16)),
% 1.10/0.39 inference(forward_demodulation,[],[f599,f509])).
% 1.10/0.39 thf(f601,plain,(
% 1.10/0.39 $false | (~spl19_3 | ~spl19_13 | ~spl19_16)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f600])).
% 1.10/0.39 thf(f602,plain,(
% 1.10/0.39 ~spl19_3 | ~spl19_13 | ~spl19_16),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f601])).
% 1.10/0.39 thf(f605,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | (~spl19_14 | ~spl19_37)),
% 1.10/0.39 inference(forward_demodulation,[],[f243,f139])).
% 1.10/0.39 thf(f606,plain,(
% 1.10/0.39 spl19_78 | ~spl19_14 | ~spl19_37),
% 1.10/0.39 inference(avatar_split_clause,[],[f605,f241,f137,f514])).
% 1.10/0.39 thf(f607,plain,(
% 1.10/0.39 ($true = ((f3 @ $false))) | (~spl19_4 | ~spl19_23)),
% 1.10/0.39 inference(forward_demodulation,[],[f94,f180])).
% 1.10/0.39 thf(f621,plain,(
% 1.10/0.39 ($true != $true) | ($false = ((f1 @ sF5))) | spl19_5),
% 1.10/0.39 inference(constrained_superposition,[],[f98,f6])).
% 1.10/0.39 thf(f622,plain,(
% 1.10/0.39 ($false = ((f1 @ sF5))) | spl19_5),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f621])).
% 1.10/0.39 thf(f623,plain,(
% 1.10/0.39 spl19_7 | spl19_5),
% 1.10/0.39 inference(avatar_split_clause,[],[f622,f97,f106])).
% 1.10/0.39 thf(f635,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | (~spl19_7 | ~spl19_38)),
% 1.10/0.39 inference(constrained_superposition,[],[f108,f247])).
% 1.10/0.39 thf(f638,plain,(
% 1.10/0.39 spl19_78 | ~spl19_7 | ~spl19_38),
% 1.10/0.39 inference(avatar_split_clause,[],[f635,f245,f106,f514])).
% 1.10/0.39 thf(f652,plain,(
% 1.10/0.39 ($false = ((f2 @ $true))) | (~spl19_2 | ~spl19_13)),
% 1.10/0.39 inference(forward_demodulation,[],[f135,f85])).
% 1.10/0.39 thf(f653,plain,(
% 1.10/0.39 spl19_80 | ~spl19_2 | ~spl19_13),
% 1.10/0.39 inference(avatar_split_clause,[],[f652,f133,f83,f556])).
% 1.10/0.39 thf(f654,plain,(
% 1.10/0.39 (((f2 @ $true)) = $true) | (~spl19_2 | ~spl19_16)),
% 1.10/0.39 inference(forward_demodulation,[],[f148,f85])).
% 1.10/0.39 thf(f663,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_41 | ~spl19_43 | ~spl19_73)),
% 1.10/0.39 inference(forward_demodulation,[],[f548,f547])).
% 1.10/0.39 thf(f664,plain,(
% 1.10/0.39 $false | (~spl19_41 | ~spl19_43 | ~spl19_73)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f663])).
% 1.10/0.39 thf(f665,plain,(
% 1.10/0.39 ~spl19_41 | ~spl19_43 | ~spl19_73),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f664])).
% 1.10/0.39 thf(f668,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_6 | ~spl19_19 | ~spl19_45 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f549,f530])).
% 1.10/0.39 thf(f669,plain,(
% 1.10/0.39 $false | (~spl19_6 | ~spl19_19 | ~spl19_45 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f668])).
% 1.10/0.39 thf(f670,plain,(
% 1.10/0.39 ~spl19_6 | ~spl19_19 | ~spl19_45 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f669])).
% 1.10/0.39 thf(f681,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_17 | ~spl19_34 | ~spl19_35 | ~spl19_71)),
% 1.10/0.39 inference(forward_demodulation,[],[f580,f544])).
% 1.10/0.39 thf(f682,plain,(
% 1.10/0.39 $false | (~spl19_17 | ~spl19_34 | ~spl19_35 | ~spl19_71)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f681])).
% 1.10/0.39 thf(f683,plain,(
% 1.10/0.39 ~spl19_17 | ~spl19_34 | ~spl19_35 | ~spl19_71),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f682])).
% 1.10/0.39 thf(f684,plain,(
% 1.10/0.39 (((f0 @ $false)) = $true) | (~spl19_17 | ~spl19_36)),
% 1.10/0.39 inference(forward_demodulation,[],[f238,f153])).
% 1.10/0.39 thf(f686,plain,(
% 1.10/0.39 ($true = ((f0 @ $true))) | (~spl19_33 | ~spl19_71)),
% 1.10/0.39 inference(forward_demodulation,[],[f398,f225])).
% 1.10/0.39 thf(f687,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_4 | ~spl19_21 | ~spl19_23 | ~spl19_27)),
% 1.10/0.39 inference(forward_demodulation,[],[f607,f531])).
% 1.10/0.39 thf(f688,plain,(
% 1.10/0.39 $false | (~spl19_4 | ~spl19_21 | ~spl19_23 | ~spl19_27)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f687])).
% 1.10/0.39 thf(f689,plain,(
% 1.10/0.39 ~spl19_4 | ~spl19_21 | ~spl19_23 | ~spl19_27),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f688])).
% 1.10/0.39 thf(f690,plain,(
% 1.10/0.39 ($true = ((f3 @ $false))) | (~spl19_28 | ~spl19_59)),
% 1.10/0.39 inference(forward_demodulation,[],[f202,f342])).
% 1.10/0.39 thf(f692,plain,(
% 1.10/0.39 ($false = ((f3 @ $true))) | (~spl19_21 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f171,f189])).
% 1.10/0.39 thf(f693,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_11 | ~spl19_21 | ~spl19_25 | ~spl19_65)),
% 1.10/0.39 inference(forward_demodulation,[],[f692,f579])).
% 1.10/0.39 thf(f694,plain,(
% 1.10/0.39 $false | (~spl19_11 | ~spl19_21 | ~spl19_25 | ~spl19_65)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f693])).
% 1.10/0.39 thf(f695,plain,(
% 1.10/0.39 ~spl19_11 | ~spl19_21 | ~spl19_25 | ~spl19_65),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f694])).
% 1.10/0.39 thf(f696,plain,(
% 1.10/0.39 ($false = ((f4 @ $true))) | (~spl19_12 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f130,f360])).
% 1.10/0.39 thf(f697,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_10 | ~spl19_12 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f696,f508])).
% 1.10/0.39 thf(f698,plain,(
% 1.10/0.39 $false | (~spl19_10 | ~spl19_12 | ~spl19_63)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f697])).
% 1.10/0.39 thf(f699,plain,(
% 1.10/0.39 ~spl19_10 | ~spl19_12 | ~spl19_63),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f698])).
% 1.10/0.39 thf(f733,plain,(
% 1.10/0.39 ($false = ((f3 @ $true))) | (~spl19_11 | ~spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f384,f126])).
% 1.10/0.39 thf(f739,plain,(
% 1.10/0.39 ($true = ((f3 @ $true))) | (~spl19_24 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f184,f189])).
% 1.10/0.39 thf(f754,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_11 | ~spl19_24 | ~spl19_25 | ~spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f739,f733])).
% 1.10/0.39 thf(f755,plain,(
% 1.10/0.39 $false | (~spl19_11 | ~spl19_24 | ~spl19_25 | ~spl19_68)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f754])).
% 1.10/0.39 thf(f756,plain,(
% 1.10/0.39 ~spl19_11 | ~spl19_24 | ~spl19_25 | ~spl19_68),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f755])).
% 1.10/0.39 thf(f757,plain,(
% 1.10/0.39 ($true = ((f3 @ $true))) | (~spl19_11 | ~spl19_65)),
% 1.10/0.39 inference(forward_demodulation,[],[f371,f126])).
% 1.10/0.39 thf(f758,plain,(
% 1.10/0.39 ($false != ((f3 @ $true))) | (spl19_21 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f170,f189])).
% 1.10/0.39 thf(f759,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_11 | ~spl19_65 | ~spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f757,f733])).
% 1.10/0.39 thf(f760,plain,(
% 1.10/0.39 $false | (~spl19_11 | ~spl19_65 | ~spl19_68)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f759])).
% 1.10/0.39 thf(f761,plain,(
% 1.10/0.39 ~spl19_11 | ~spl19_65 | ~spl19_68),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f760])).
% 1.10/0.39 thf(f762,plain,(
% 1.10/0.39 $false | (~spl19_11 | spl19_21 | ~spl19_25 | ~spl19_68)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f758,f733])).
% 1.10/0.39 thf(f763,plain,(
% 1.10/0.39 ~spl19_11 | spl19_21 | ~spl19_25 | ~spl19_68),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f762])).
% 1.10/0.39 thf(f770,plain,(
% 1.10/0.39 ($false = ((f2 @ $true))) | (~spl19_67 | ~spl19_75)),
% 1.10/0.39 inference(forward_demodulation,[],[f416,f380])).
% 1.10/0.39 thf(f771,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_2 | ~spl19_16 | ~spl19_67 | ~spl19_75)),
% 1.10/0.39 inference(forward_demodulation,[],[f770,f654])).
% 1.10/0.39 thf(f772,plain,(
% 1.10/0.39 $false | (~spl19_2 | ~spl19_16 | ~spl19_67 | ~spl19_75)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f771])).
% 1.10/0.39 thf(f773,plain,(
% 1.10/0.39 ~spl19_2 | ~spl19_16 | ~spl19_67 | ~spl19_75),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f772])).
% 1.10/0.39 thf(f799,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_17 | ~spl19_29 | ~spl19_36 | ~spl19_46)),
% 1.10/0.39 inference(forward_demodulation,[],[f542,f684])).
% 1.10/0.39 thf(f800,plain,(
% 1.10/0.39 $false | (~spl19_17 | ~spl19_29 | ~spl19_36 | ~spl19_46)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f799])).
% 1.10/0.39 thf(f801,plain,(
% 1.10/0.39 ~spl19_17 | ~spl19_29 | ~spl19_36 | ~spl19_46),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f800])).
% 1.10/0.39 thf(f803,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_50 | ~spl19_69 | ~spl19_79)),
% 1.10/0.39 inference(forward_demodulation,[],[f539,f551])).
% 1.10/0.39 thf(f804,plain,(
% 1.10/0.39 $false | (~spl19_50 | ~spl19_69 | ~spl19_79)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f803])).
% 1.10/0.39 thf(f805,plain,(
% 1.10/0.39 ~spl19_50 | ~spl19_69 | ~spl19_79),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f804])).
% 1.10/0.39 thf(f806,plain,(
% 1.10/0.39 ($true = ((f1 @ $false))) | (~spl19_5 | ~spl19_40)),
% 1.10/0.39 inference(forward_demodulation,[],[f99,f256])).
% 1.10/0.39 thf(f809,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_5 | ~spl19_19 | ~spl19_40 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f806,f530])).
% 1.10/0.39 thf(f810,plain,(
% 1.10/0.39 $false | (~spl19_5 | ~spl19_19 | ~spl19_40 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f809])).
% 1.10/0.39 thf(f811,plain,(
% 1.10/0.39 ~spl19_5 | ~spl19_19 | ~spl19_40 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f810])).
% 1.10/0.39 thf(f813,plain,(
% 1.10/0.39 ($false = ((f0 @ $true))) | (~spl19_33 | ~spl19_70)),
% 1.10/0.39 inference(forward_demodulation,[],[f393,f225])).
% 1.10/0.39 thf(f814,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_30 | ~spl19_31)),
% 1.10/0.39 inference(forward_demodulation,[],[f211,f216])).
% 1.10/0.39 thf(f815,plain,(
% 1.10/0.39 $false | (~spl19_30 | ~spl19_31)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f814])).
% 1.10/0.39 thf(f816,plain,(
% 1.10/0.39 ~spl19_30 | ~spl19_31),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f815])).
% 1.10/0.39 thf(f818,plain,(
% 1.10/0.39 spl19_79 | ~spl19_33 | ~spl19_70),
% 1.10/0.39 inference(avatar_split_clause,[],[f813,f391,f223,f537])).
% 1.10/0.39 thf(f832,plain,(
% 1.10/0.39 ($false = sF17) | ($true != $true) | spl19_69),
% 1.10/0.39 inference(constrained_superposition,[],[f388,f6])).
% 1.10/0.39 thf(f833,plain,(
% 1.10/0.39 ($false = sF17) | spl19_69),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f832])).
% 1.10/0.39 thf(f834,plain,(
% 1.10/0.39 spl19_72 | spl19_69),
% 1.10/0.39 inference(avatar_split_clause,[],[f833,f387,f400])).
% 1.10/0.39 thf(f841,plain,(
% 1.10/0.39 ($true != ((f0 @ $true))) | (spl19_50 | ~spl19_69)),
% 1.10/0.39 inference(forward_demodulation,[],[f300,f389])).
% 1.10/0.39 thf(f842,plain,(
% 1.10/0.39 ($false = ((f0 @ $true))) | (~spl19_52 | ~spl19_69)),
% 1.10/0.39 inference(forward_demodulation,[],[f310,f389])).
% 1.10/0.39 thf(f843,plain,(
% 1.10/0.39 spl19_79 | ~spl19_52 | ~spl19_69),
% 1.10/0.39 inference(avatar_split_clause,[],[f842,f387,f308,f537])).
% 1.10/0.39 thf(f848,plain,(
% 1.10/0.39 $false | (~spl19_33 | spl19_50 | ~spl19_69 | ~spl19_71)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f841,f686])).
% 1.10/0.39 thf(f849,plain,(
% 1.10/0.39 ~spl19_33 | spl19_50 | ~spl19_69 | ~spl19_71),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f848])).
% 1.10/0.39 thf(f855,plain,(
% 1.10/0.39 ($false = ((f0 @ $false))) | (~spl19_52 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f310,f402])).
% 1.10/0.39 thf(f856,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_17 | ~spl19_36 | ~spl19_52 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f855,f684])).
% 1.10/0.39 thf(f857,plain,(
% 1.10/0.39 $false | (~spl19_17 | ~spl19_36 | ~spl19_52 | ~spl19_72)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f856])).
% 1.10/0.39 thf(f858,plain,(
% 1.10/0.39 ~spl19_17 | ~spl19_36 | ~spl19_52 | ~spl19_72),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f857])).
% 1.10/0.39 thf(f861,plain,(
% 1.10/0.39 ($true = ((f1 @ $false))) | (~spl19_15 | ~spl19_39)),
% 1.10/0.39 inference(forward_demodulation,[],[f252,f144])).
% 1.10/0.39 thf(f863,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_15 | ~spl19_19 | ~spl19_39 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f861,f530])).
% 1.10/0.39 thf(f864,plain,(
% 1.10/0.39 $false | (~spl19_15 | ~spl19_19 | ~spl19_39 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f863])).
% 1.10/0.39 thf(f865,plain,(
% 1.10/0.39 ~spl19_15 | ~spl19_19 | ~spl19_39 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f864])).
% 1.10/0.39 thf(f866,plain,(
% 1.10/0.39 ($false != ((f2 @ $true))) | (~spl19_67 | spl19_75)),
% 1.10/0.39 inference(forward_demodulation,[],[f415,f380])).
% 1.10/0.39 thf(f871,plain,(
% 1.10/0.39 ~spl19_80 | ~spl19_67 | spl19_75),
% 1.10/0.39 inference(avatar_split_clause,[],[f866,f414,f378,f556])).
% 1.10/0.39 thf(f873,plain,(
% 1.10/0.39 ($true != ((f4 @ $true))) | (spl19_10 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f120,f360])).
% 1.10/0.39 thf(f911,plain,(
% 1.10/0.39 ($true = ((f1 @ $false))) | (~spl19_18 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f157,f328])).
% 1.10/0.39 thf(f913,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_18 | ~spl19_19 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f911,f530])).
% 1.10/0.39 thf(f914,plain,(
% 1.10/0.39 $false | (~spl19_18 | ~spl19_19 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f913])).
% 1.10/0.39 thf(f915,plain,(
% 1.10/0.39 ~spl19_18 | ~spl19_19 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f914])).
% 1.10/0.39 thf(f932,plain,(
% 1.10/0.39 ($false = ((f2 @ $true))) | (~spl19_41 | ~spl19_76)),
% 1.10/0.39 inference(forward_demodulation,[],[f261,f420])).
% 1.10/0.39 thf(f933,plain,(
% 1.10/0.39 spl19_80 | ~spl19_41 | ~spl19_76),
% 1.10/0.39 inference(avatar_split_clause,[],[f932,f418,f259,f556])).
% 1.10/0.39 thf(f936,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | (~spl19_8 | ~spl19_47)),
% 1.10/0.39 inference(forward_demodulation,[],[f288,f112])).
% 1.10/0.39 thf(f937,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_8 | ~spl19_47 | ~spl19_77)),
% 1.10/0.39 inference(forward_demodulation,[],[f936,f496])).
% 1.10/0.39 thf(f938,plain,(
% 1.10/0.39 $false | (~spl19_8 | ~spl19_47 | ~spl19_77)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f937])).
% 1.10/0.39 thf(f939,plain,(
% 1.10/0.39 ~spl19_8 | ~spl19_47 | ~spl19_77),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f938])).
% 1.10/0.39 thf(f946,plain,(
% 1.10/0.39 ($false = ((f3 @ $false))) | (~spl19_9 | ~spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f384,f117])).
% 1.10/0.39 thf(f947,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_9 | ~spl19_28 | ~spl19_59 | ~spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f946,f690])).
% 1.10/0.39 thf(f948,plain,(
% 1.10/0.39 $false | (~spl19_9 | ~spl19_28 | ~spl19_59 | ~spl19_68)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f947])).
% 1.10/0.39 thf(f949,plain,(
% 1.10/0.39 ~spl19_9 | ~spl19_28 | ~spl19_59 | ~spl19_68),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f948])).
% 1.10/0.39 thf(f950,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_57 | ~spl19_60)),
% 1.10/0.39 inference(forward_demodulation,[],[f346,f333])).
% 1.10/0.39 thf(f951,plain,(
% 1.10/0.39 $false | (~spl19_57 | ~spl19_60)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f950])).
% 1.10/0.39 thf(f952,plain,(
% 1.10/0.39 ~spl19_57 | ~spl19_60),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f951])).
% 1.10/0.39 thf(f963,plain,(
% 1.10/0.39 ($true = ((f4 @ $false))) | (~spl19_60 | ~spl19_82)),
% 1.10/0.39 inference(forward_demodulation,[],[f346,f577])).
% 1.10/0.39 thf(f964,plain,(
% 1.10/0.39 ($true = ((f4 @ $true))) | (~spl19_58 | ~spl19_62)),
% 1.10/0.39 inference(forward_demodulation,[],[f355,f337])).
% 1.10/0.39 thf(f993,plain,(
% 1.10/0.39 $false | (spl19_10 | ~spl19_58 | ~spl19_62 | ~spl19_63)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f964,f873])).
% 1.10/0.39 thf(f994,plain,(
% 1.10/0.39 spl19_10 | ~spl19_58 | ~spl19_62 | ~spl19_63),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f993])).
% 1.10/0.39 thf(f995,plain,(
% 1.10/0.39 ($false = ((f4 @ $true))) | (~spl19_58 | ~spl19_64)),
% 1.10/0.39 inference(forward_demodulation,[],[f364,f337])).
% 1.10/0.39 thf(f996,plain,(
% 1.10/0.39 spl19_81 | ~spl19_58 | ~spl19_64),
% 1.10/0.39 inference(avatar_split_clause,[],[f995,f362,f335,f571])).
% 1.10/0.39 thf(f997,plain,(
% 1.10/0.39 ($false = sF9) | ($true != $true) | spl19_63),
% 1.10/0.39 inference(constrained_superposition,[],[f359,f6])).
% 1.10/0.39 thf(f998,plain,(
% 1.10/0.39 ($false = sF9) | spl19_63),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f997])).
% 1.10/0.39 thf(f999,plain,(
% 1.10/0.39 $false | (spl19_61 | spl19_63)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f998,f350])).
% 1.10/0.39 thf(f1000,plain,(
% 1.10/0.39 spl19_61 | spl19_63),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f999])).
% 1.10/0.39 thf(f1001,plain,(
% 1.10/0.39 spl19_61 | spl19_63),
% 1.10/0.39 inference(avatar_split_clause,[],[f998,f358,f349])).
% 1.10/0.39 thf(f1005,plain,(
% 1.10/0.39 ($false = ((f4 @ $false))) | (~spl19_12 | ~spl19_61)),
% 1.10/0.39 inference(forward_demodulation,[],[f130,f351])).
% 1.10/0.39 thf(f1006,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_12 | ~spl19_60 | ~spl19_61 | ~spl19_82)),
% 1.10/0.39 inference(forward_demodulation,[],[f1005,f963])).
% 1.10/0.39 thf(f1007,plain,(
% 1.10/0.39 $false | (~spl19_12 | ~spl19_60 | ~spl19_61 | ~spl19_82)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1006])).
% 1.10/0.39 thf(f1008,plain,(
% 1.10/0.39 ~spl19_12 | ~spl19_60 | ~spl19_61 | ~spl19_82),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1007])).
% 1.10/0.39 thf(f1009,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_58 | ~spl19_59)),
% 1.10/0.39 inference(forward_demodulation,[],[f342,f337])).
% 1.10/0.39 thf(f1010,plain,(
% 1.10/0.39 $false | (~spl19_58 | ~spl19_59)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1009])).
% 1.10/0.39 thf(f1011,plain,(
% 1.10/0.39 ~spl19_58 | ~spl19_59),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1010])).
% 1.10/0.39 thf(f1012,plain,(
% 1.10/0.39 ($true = ((f4 @ $false))) | (~spl19_10 | ~spl19_61)),
% 1.10/0.39 inference(forward_demodulation,[],[f121,f351])).
% 1.10/0.39 thf(f1015,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF10) | spl19_11),
% 1.10/0.39 inference(constrained_superposition,[],[f125,f6])).
% 1.10/0.39 thf(f1016,plain,(
% 1.10/0.39 ($false = sF10) | spl19_11),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1015])).
% 1.10/0.39 thf(f1017,plain,(
% 1.10/0.39 $false | (spl19_9 | spl19_11)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1016,f116])).
% 1.10/0.39 thf(f1018,plain,(
% 1.10/0.39 spl19_9 | spl19_11),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1017])).
% 1.10/0.39 thf(f1025,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF0) | spl19_58),
% 1.10/0.39 inference(constrained_superposition,[],[f336,f6])).
% 1.10/0.39 thf(f1026,plain,(
% 1.10/0.39 ($false = sF0) | spl19_58),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1025])).
% 1.10/0.39 thf(f1027,plain,(
% 1.10/0.39 spl19_59 | spl19_58),
% 1.10/0.39 inference(avatar_split_clause,[],[f1026,f335,f340])).
% 1.10/0.39 thf(f1031,plain,(
% 1.10/0.39 ($false != ((f3 @ $false))) | (spl19_21 | ~spl19_27)),
% 1.10/0.39 inference(forward_demodulation,[],[f170,f198])).
% 1.10/0.39 thf(f1032,plain,(
% 1.10/0.39 ($true = ((f3 @ $false))) | (~spl19_24 | ~spl19_27)),
% 1.10/0.39 inference(forward_demodulation,[],[f184,f198])).
% 1.10/0.39 thf(f1033,plain,(
% 1.10/0.39 ($false = ((f3 @ $false))) | (~spl19_26 | ~spl19_59)),
% 1.10/0.39 inference(forward_demodulation,[],[f193,f342])).
% 1.10/0.39 thf(f1047,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_10 | ~spl19_12 | ~spl19_61)),
% 1.10/0.39 inference(forward_demodulation,[],[f1012,f1005])).
% 1.10/0.39 thf(f1048,plain,(
% 1.10/0.39 $false | (~spl19_10 | ~spl19_12 | ~spl19_61)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1047])).
% 1.10/0.39 thf(f1049,plain,(
% 1.10/0.39 ~spl19_10 | ~spl19_12 | ~spl19_61),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1048])).
% 1.10/0.39 thf(f1059,plain,(
% 1.10/0.39 $false | (spl19_21 | ~spl19_26 | ~spl19_27 | ~spl19_59)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1033,f1031])).
% 1.10/0.39 thf(f1060,plain,(
% 1.10/0.39 spl19_21 | ~spl19_26 | ~spl19_27 | ~spl19_59),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1059])).
% 1.10/0.39 thf(f1061,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_24 | ~spl19_26 | ~spl19_27 | ~spl19_59)),
% 1.10/0.39 inference(forward_demodulation,[],[f1033,f1032])).
% 1.10/0.39 thf(f1062,plain,(
% 1.10/0.39 $false | (~spl19_24 | ~spl19_26 | ~spl19_27 | ~spl19_59)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1061])).
% 1.10/0.39 thf(f1063,plain,(
% 1.10/0.39 ~spl19_24 | ~spl19_26 | ~spl19_27 | ~spl19_59),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1062])).
% 1.10/0.39 thf(f1068,plain,(
% 1.10/0.39 ($true = ((f3 @ $false))) | (~spl19_9 | ~spl19_65)),
% 1.10/0.39 inference(forward_demodulation,[],[f371,f117])).
% 1.10/0.39 thf(f1069,plain,(
% 1.10/0.39 (((f2 @ $true)) != $true) | (~spl19_2 | spl19_16)),
% 1.10/0.39 inference(forward_demodulation,[],[f147,f85])).
% 1.10/0.39 thf(f1085,plain,(
% 1.10/0.39 ($true = ((f3 @ $true))) | (~spl19_24 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f184,f189])).
% 1.10/0.39 thf(f1089,plain,(
% 1.10/0.39 (((f2 @ $true)) = $true) | (~spl19_67 | ~spl19_74)),
% 1.10/0.39 inference(forward_demodulation,[],[f411,f380])).
% 1.10/0.39 thf(f1122,plain,(
% 1.10/0.39 $false | (~spl19_2 | spl19_16 | ~spl19_67 | ~spl19_74)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1089,f1069])).
% 1.10/0.39 thf(f1123,plain,(
% 1.10/0.39 ~spl19_2 | spl19_16 | ~spl19_67 | ~spl19_74),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1122])).
% 1.10/0.39 thf(f1137,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_69 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f389,f402])).
% 1.10/0.39 thf(f1138,plain,(
% 1.10/0.39 $false | (~spl19_69 | ~spl19_72)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1137])).
% 1.10/0.39 thf(f1139,plain,(
% 1.10/0.39 ~spl19_69 | ~spl19_72),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1138])).
% 1.10/0.39 thf(f1140,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_29 | ~spl19_32)),
% 1.10/0.39 inference(forward_demodulation,[],[f207,f220])).
% 1.10/0.39 thf(f1141,plain,(
% 1.10/0.39 $false | (~spl19_29 | ~spl19_32)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1140])).
% 1.10/0.39 thf(f1142,plain,(
% 1.10/0.39 ~spl19_29 | ~spl19_32),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1141])).
% 1.10/0.39 thf(f1145,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_46 | ~spl19_48)),
% 1.10/0.39 inference(forward_demodulation,[],[f283,f292])).
% 1.10/0.39 thf(f1146,plain,(
% 1.10/0.39 $false | (~spl19_46 | ~spl19_48)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1145])).
% 1.10/0.39 thf(f1147,plain,(
% 1.10/0.39 ~spl19_46 | ~spl19_48),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1146])).
% 1.10/0.39 thf(f1152,plain,(
% 1.10/0.39 ($false = ((f1 @ $false))) | (~spl19_15 | ~spl19_37)),
% 1.10/0.39 inference(forward_demodulation,[],[f243,f144])).
% 1.10/0.39 thf(f1155,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_15 | ~spl19_18 | ~spl19_37 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f1152,f911])).
% 1.10/0.39 thf(f1156,plain,(
% 1.10/0.39 $false | (~spl19_15 | ~spl19_18 | ~spl19_37 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1155])).
% 1.10/0.39 thf(f1157,plain,(
% 1.10/0.39 ~spl19_15 | ~spl19_18 | ~spl19_37 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1156])).
% 1.10/0.39 thf(f1164,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_77 | ~spl19_78)),
% 1.10/0.39 inference(forward_demodulation,[],[f516,f496])).
% 1.10/0.39 thf(f1165,plain,(
% 1.10/0.39 $false | (~spl19_77 | ~spl19_78)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1164])).
% 1.10/0.39 thf(f1166,plain,(
% 1.10/0.39 ~spl19_77 | ~spl19_78),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1165])).
% 1.10/0.39 thf(f1169,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_54 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f319,f328])).
% 1.10/0.39 thf(f1170,plain,(
% 1.10/0.39 $false | (~spl19_54 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1169])).
% 1.10/0.39 thf(f1171,plain,(
% 1.10/0.39 ~spl19_54 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1170])).
% 1.10/0.39 thf(f1172,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_1 | ~spl19_4)),
% 1.10/0.39 inference(forward_demodulation,[],[f81,f94])).
% 1.10/0.39 thf(f1173,plain,(
% 1.10/0.39 $false | (~spl19_1 | ~spl19_4)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1172])).
% 1.10/0.39 thf(f1174,plain,(
% 1.10/0.39 ~spl19_1 | ~spl19_4),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1173])).
% 1.10/0.39 thf(f1178,plain,(
% 1.10/0.39 ($false = ((f3 @ $true))) | (~spl19_1 | ~spl19_22)),
% 1.10/0.39 inference(forward_demodulation,[],[f81,f175])).
% 1.10/0.39 thf(f1181,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_1 | ~spl19_22 | ~spl19_24 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f1178,f1085])).
% 1.10/0.39 thf(f1182,plain,(
% 1.10/0.39 $false | (~spl19_1 | ~spl19_22 | ~spl19_24 | ~spl19_25)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1181])).
% 1.10/0.39 thf(f1183,plain,(
% 1.10/0.39 ~spl19_1 | ~spl19_22 | ~spl19_24 | ~spl19_25),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1182])).
% 1.10/0.39 thf(f1184,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_22 | ~spl19_23)),
% 1.10/0.39 inference(forward_demodulation,[],[f180,f175])).
% 1.10/0.39 thf(f1185,plain,(
% 1.10/0.39 $false | (~spl19_22 | ~spl19_23)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1184])).
% 1.10/0.39 thf(f1186,plain,(
% 1.10/0.39 ~spl19_22 | ~spl19_23),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1185])).
% 1.10/0.39 thf(f1187,plain,(
% 1.10/0.39 ($true != ((f3 @ $true))) | (spl19_24 | ~spl19_25)),
% 1.10/0.39 inference(forward_demodulation,[],[f183,f189])).
% 1.10/0.39 thf(f1202,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF2) | spl19_22),
% 1.10/0.39 inference(constrained_superposition,[],[f174,f6])).
% 1.10/0.39 thf(f1203,plain,(
% 1.10/0.39 ($false = sF2) | spl19_22),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1202])).
% 1.10/0.39 thf(f1204,plain,(
% 1.10/0.39 spl19_23 | spl19_22),
% 1.10/0.39 inference(avatar_split_clause,[],[f1203,f173,f178])).
% 1.10/0.39 thf(f1214,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF13) | spl19_42),
% 1.10/0.39 inference(constrained_superposition,[],[f264,f6])).
% 1.10/0.39 thf(f1215,plain,(
% 1.10/0.39 ($false = sF13) | spl19_42),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1214])).
% 1.10/0.39 thf(f1216,plain,(
% 1.10/0.39 spl19_44 | spl19_42),
% 1.10/0.39 inference(avatar_split_clause,[],[f1215,f263,f272])).
% 1.10/0.39 thf(f1228,plain,(
% 1.10/0.39 ($false = ((f3 @ $false))) | (~spl19_1 | ~spl19_23)),
% 1.10/0.39 inference(forward_demodulation,[],[f81,f180])).
% 1.10/0.39 thf(f1229,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_1 | ~spl19_9 | ~spl19_23 | ~spl19_65)),
% 1.10/0.39 inference(forward_demodulation,[],[f1228,f1068])).
% 1.10/0.39 thf(f1230,plain,(
% 1.10/0.39 $false | (~spl19_1 | ~spl19_9 | ~spl19_23 | ~spl19_65)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1229])).
% 1.10/0.39 thf(f1231,plain,(
% 1.10/0.39 ~spl19_1 | ~spl19_9 | ~spl19_23 | ~spl19_65),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1230])).
% 1.10/0.39 thf(f1249,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_41 | ~spl19_73)),
% 1.10/0.39 inference(forward_demodulation,[],[f261,f407])).
% 1.10/0.39 thf(f1252,plain,(
% 1.10/0.39 ($false = ((f1 @ $false))) | (~spl19_6 | ~spl19_47)),
% 1.10/0.39 inference(forward_demodulation,[],[f288,f103])).
% 1.10/0.39 thf(f1253,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_6 | ~spl19_18 | ~spl19_47 | ~spl19_56)),
% 1.10/0.39 inference(forward_demodulation,[],[f1252,f911])).
% 1.10/0.39 thf(f1254,plain,(
% 1.10/0.39 $false | (~spl19_6 | ~spl19_18 | ~spl19_47 | ~spl19_56)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1253])).
% 1.10/0.39 thf(f1255,plain,(
% 1.10/0.39 ~spl19_6 | ~spl19_18 | ~spl19_47 | ~spl19_56),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1254])).
% 1.10/0.39 thf(f1259,plain,(
% 1.10/0.39 ($false != ((f1 @ $true))) | (spl19_7 | ~spl19_38)),
% 1.10/0.39 inference(forward_demodulation,[],[f107,f247])).
% 1.10/0.39 thf(f1261,plain,(
% 1.10/0.39 ~spl19_78 | spl19_7 | ~spl19_38),
% 1.10/0.39 inference(avatar_split_clause,[],[f1259,f245,f106,f514])).
% 1.10/0.39 thf(f1263,plain,(
% 1.10/0.39 ($false != ((f2 @ $false))) | (~spl19_44 | spl19_53)),
% 1.10/0.39 inference(forward_demodulation,[],[f314,f274])).
% 1.10/0.39 thf(f1278,plain,(
% 1.10/0.39 ($true = ((f1 @ $true))) | (~spl19_18 | ~spl19_54)),
% 1.10/0.39 inference(forward_demodulation,[],[f157,f319])).
% 1.10/0.39 thf(f1279,plain,(
% 1.10/0.39 spl19_77 | ~spl19_18 | ~spl19_54),
% 1.10/0.39 inference(avatar_split_clause,[],[f1278,f317,f155,f494])).
% 1.10/0.39 thf(f1310,plain,(
% 1.10/0.39 $false | (~spl19_41 | ~spl19_44 | spl19_53 | ~spl19_73)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1263,f1249])).
% 1.10/0.39 thf(f1311,plain,(
% 1.10/0.39 ~spl19_41 | ~spl19_44 | spl19_53 | ~spl19_73),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1310])).
% 1.10/0.39 thf(f1315,plain,(
% 1.10/0.39 ($false != ((f2 @ $true))) | (~spl19_42 | spl19_53)),
% 1.10/0.39 inference(forward_demodulation,[],[f314,f265])).
% 1.10/0.39 thf(f1316,plain,(
% 1.10/0.39 ~spl19_80 | ~spl19_42 | spl19_53),
% 1.10/0.39 inference(avatar_split_clause,[],[f1315,f313,f263,f556])).
% 1.10/0.39 thf(f1317,plain,(
% 1.10/0.39 (((f2 @ $true)) != $true) | (~spl19_42 | spl19_55)),
% 1.10/0.39 inference(forward_demodulation,[],[f323,f265])).
% 1.10/0.39 thf(f1318,plain,(
% 1.10/0.39 ($false = ((f0 @ $true))) | (~spl19_20 | ~spl19_34)),
% 1.10/0.39 inference(forward_demodulation,[],[f229,f166])).
% 1.10/0.39 thf(f1324,plain,(
% 1.10/0.39 spl19_79 | ~spl19_20 | ~spl19_34),
% 1.10/0.39 inference(avatar_split_clause,[],[f1318,f227,f164,f537])).
% 1.10/0.39 thf(f1340,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF14) | spl19_54),
% 1.10/0.39 inference(constrained_superposition,[],[f318,f6])).
% 1.10/0.39 thf(f1341,plain,(
% 1.10/0.39 ($false = sF14) | spl19_54),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1340])).
% 1.10/0.39 thf(f1342,plain,(
% 1.10/0.39 spl19_56 | spl19_54),
% 1.10/0.39 inference(avatar_split_clause,[],[f1341,f317,f326])).
% 1.10/0.39 thf(f1350,plain,(
% 1.10/0.39 ($false != ((f0 @ $true))) | (spl19_29 | ~spl19_48)),
% 1.10/0.39 inference(forward_demodulation,[],[f206,f292])).
% 1.10/0.39 thf(f1351,plain,(
% 1.10/0.39 ~spl19_79 | spl19_29 | ~spl19_48),
% 1.10/0.39 inference(avatar_split_clause,[],[f1350,f290,f205,f537])).
% 1.10/0.39 thf(f1355,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | (~spl19_8 | ~spl19_47)),
% 1.10/0.39 inference(forward_demodulation,[],[f288,f112])).
% 1.10/0.39 thf(f1356,plain,(
% 1.10/0.39 spl19_78 | ~spl19_8 | ~spl19_47),
% 1.10/0.39 inference(avatar_split_clause,[],[f1355,f286,f110,f514])).
% 1.10/0.39 thf(f1386,plain,(
% 1.10/0.39 ($false != ((f4 @ $true))) | (spl19_12 | ~spl19_63)),
% 1.10/0.39 inference(forward_demodulation,[],[f129,f360])).
% 1.10/0.39 thf(f1387,plain,(
% 1.10/0.39 ~spl19_81 | spl19_12 | ~spl19_63),
% 1.10/0.39 inference(avatar_split_clause,[],[f1386,f358,f128,f571])).
% 1.10/0.39 thf(f1396,plain,(
% 1.10/0.39 ($true = ((f1 @ $true))) | (~spl19_14 | ~spl19_39)),
% 1.10/0.39 inference(forward_demodulation,[],[f252,f139])).
% 1.10/0.39 thf(f1397,plain,(
% 1.10/0.39 spl19_77 | ~spl19_14 | ~spl19_39),
% 1.10/0.39 inference(avatar_split_clause,[],[f1396,f250,f137,f494])).
% 1.10/0.39 thf(f1400,plain,(
% 1.10/0.39 ($true = ((f1 @ $true))) | (~spl19_8 | ~spl19_45)),
% 1.10/0.39 inference(forward_demodulation,[],[f279,f112])).
% 1.10/0.39 thf(f1401,plain,(
% 1.10/0.39 spl19_77 | ~spl19_8 | ~spl19_45),
% 1.10/0.39 inference(avatar_split_clause,[],[f1400,f277,f110,f494])).
% 1.10/0.39 thf(f1446,plain,(
% 1.10/0.39 ($true = ((f3 @ $true))) | (~spl19_28 | ~spl19_58)),
% 1.10/0.39 inference(forward_demodulation,[],[f202,f337])).
% 1.10/0.39 thf(f1447,plain,(
% 1.10/0.39 $false | (spl19_24 | ~spl19_25 | ~spl19_28 | ~spl19_58)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1446,f1187])).
% 1.10/0.39 thf(f1448,plain,(
% 1.10/0.39 spl19_24 | ~spl19_25 | ~spl19_28 | ~spl19_58),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1447])).
% 1.10/0.39 thf(f1449,plain,(
% 1.10/0.39 ($false = ((f4 @ $false))) | (~spl19_57 | ~spl19_82)),
% 1.10/0.39 inference(forward_demodulation,[],[f333,f577])).
% 1.10/0.39 thf(f1460,plain,(
% 1.10/0.39 (((f2 @ $true)) = $true) | (~spl19_2 | ~spl19_16)),
% 1.10/0.39 inference(forward_demodulation,[],[f148,f85])).
% 1.10/0.39 thf(f1461,plain,(
% 1.10/0.39 $false | (~spl19_2 | ~spl19_16 | ~spl19_42 | spl19_55)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1460,f1317])).
% 1.10/0.39 thf(f1462,plain,(
% 1.10/0.39 ~spl19_2 | ~spl19_16 | ~spl19_42 | spl19_55),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1461])).
% 1.10/0.39 thf(f1474,plain,(
% 1.10/0.39 ($true = ((f4 @ $false))) | (~spl19_59 | ~spl19_62)),
% 1.10/0.39 inference(forward_demodulation,[],[f355,f342])).
% 1.10/0.39 thf(f1497,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_57 | ~spl19_59 | ~spl19_62 | ~spl19_82)),
% 1.10/0.39 inference(forward_demodulation,[],[f1474,f1449])).
% 1.10/0.39 thf(f1498,plain,(
% 1.10/0.39 $false | (~spl19_57 | ~spl19_59 | ~spl19_62 | ~spl19_82)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1497])).
% 1.10/0.39 thf(f1499,plain,(
% 1.10/0.39 ~spl19_57 | ~spl19_59 | ~spl19_62 | ~spl19_82),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1498])).
% 1.10/0.39 thf(f1500,plain,(
% 1.10/0.39 ($false = ((f4 @ $false))) | (~spl19_59 | ~spl19_64)),
% 1.10/0.39 inference(forward_demodulation,[],[f364,f342])).
% 1.10/0.39 thf(f1506,plain,(
% 1.10/0.39 ($true = ((f4 @ $false))) | (~spl19_10 | ~spl19_61)),
% 1.10/0.39 inference(forward_demodulation,[],[f121,f351])).
% 1.10/0.39 thf(f1512,plain,(
% 1.10/0.39 ($false = ((f4 @ $true))) | (x = $false) | ~spl19_57),
% 1.10/0.39 inference(constrained_superposition,[],[f333,f6])).
% 1.10/0.39 thf(f1515,plain,(
% 1.10/0.39 ($false = ((f4 @ $true))) | (~spl19_57 | spl19_82)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1512,f576])).
% 1.10/0.39 thf(f1516,plain,(
% 1.10/0.39 spl19_81 | ~spl19_57 | spl19_82),
% 1.10/0.39 inference(avatar_split_clause,[],[f1515,f575,f331,f571])).
% 1.10/0.39 thf(f1521,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_10 | ~spl19_59 | ~spl19_61 | ~spl19_64)),
% 1.10/0.39 inference(forward_demodulation,[],[f1506,f1500])).
% 1.10/0.39 thf(f1522,plain,(
% 1.10/0.39 $false | (~spl19_10 | ~spl19_59 | ~spl19_61 | ~spl19_64)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1521])).
% 1.10/0.39 thf(f1523,plain,(
% 1.10/0.39 ~spl19_10 | ~spl19_59 | ~spl19_61 | ~spl19_64),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1522])).
% 1.10/0.39 thf(f1525,plain,(
% 1.10/0.39 ($false = ((f0 @ $false))) | (~spl19_35 | ~spl19_70)),
% 1.10/0.39 inference(forward_demodulation,[],[f393,f234])).
% 1.10/0.39 thf(f1559,plain,(
% 1.10/0.39 ($false = ((f0 @ $true))) | (~spl19_29 | ~spl19_48)),
% 1.10/0.39 inference(forward_demodulation,[],[f207,f292])).
% 1.10/0.39 thf(f1560,plain,(
% 1.10/0.39 spl19_79 | ~spl19_29 | ~spl19_48),
% 1.10/0.39 inference(avatar_split_clause,[],[f1559,f290,f205,f537])).
% 1.10/0.39 thf(f1568,plain,(
% 1.10/0.39 (((f0 @ $false)) = $true) | (~spl19_50 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f301,f402])).
% 1.10/0.39 thf(f1598,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_35 | ~spl19_50 | ~spl19_70 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f1568,f1525])).
% 1.10/0.39 thf(f1599,plain,(
% 1.10/0.39 $false | (~spl19_35 | ~spl19_50 | ~spl19_70 | ~spl19_72)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1598])).
% 1.10/0.39 thf(f1600,plain,(
% 1.10/0.39 ~spl19_35 | ~spl19_50 | ~spl19_70 | ~spl19_72),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1599])).
% 1.10/0.39 thf(f1627,plain,(
% 1.10/0.39 ($false != ((f0 @ $false))) | (spl19_29 | ~spl19_46)),
% 1.10/0.39 inference(forward_demodulation,[],[f206,f283])).
% 1.10/0.39 thf(f1628,plain,(
% 1.10/0.39 $false | (spl19_29 | ~spl19_35 | ~spl19_46 | ~spl19_70)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1627,f1525])).
% 1.10/0.39 thf(f1629,plain,(
% 1.10/0.39 spl19_29 | ~spl19_35 | ~spl19_46 | ~spl19_70),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1628])).
% 1.10/0.39 thf(f1637,plain,(
% 1.10/0.39 ($true = ((f2 @ $false))) | (~spl19_44 | ~spl19_55)),
% 1.10/0.39 inference(forward_demodulation,[],[f324,f274])).
% 1.10/0.39 thf(f1658,plain,(
% 1.10/0.39 ($true != $true) | ($false = sF12) | spl19_76),
% 1.10/0.39 inference(constrained_superposition,[],[f419,f6])).
% 1.10/0.39 thf(f1659,plain,(
% 1.10/0.39 ($false = sF12) | spl19_76),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1658])).
% 1.10/0.39 thf(f1660,plain,(
% 1.10/0.39 $false | (spl19_73 | spl19_76)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1659,f406])).
% 1.10/0.39 thf(f1661,plain,(
% 1.10/0.39 spl19_73 | spl19_76),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1660])).
% 1.10/0.39 thf(f1663,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_3 | ~spl19_13)),
% 1.10/0.39 inference(forward_demodulation,[],[f135,f90])).
% 1.10/0.39 thf(f1676,plain,(
% 1.10/0.39 ($true = ((f2 @ $false))) | (~spl19_66 | ~spl19_74)),
% 1.10/0.39 inference(forward_demodulation,[],[f411,f375])).
% 1.10/0.39 thf(f1677,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_66 | ~spl19_75)),
% 1.10/0.39 inference(forward_demodulation,[],[f416,f375])).
% 1.10/0.39 thf(f1691,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_3 | ~spl19_13 | ~spl19_44 | ~spl19_55)),
% 1.10/0.39 inference(forward_demodulation,[],[f1663,f1637])).
% 1.10/0.39 thf(f1692,plain,(
% 1.10/0.39 $false | (~spl19_3 | ~spl19_13 | ~spl19_44 | ~spl19_55)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1691])).
% 1.10/0.39 thf(f1693,plain,(
% 1.10/0.39 ~spl19_3 | ~spl19_13 | ~spl19_44 | ~spl19_55),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1692])).
% 1.10/0.39 thf(f1710,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_3 | ~spl19_13 | ~spl19_66 | ~spl19_74)),
% 1.10/0.39 inference(forward_demodulation,[],[f1676,f1663])).
% 1.10/0.39 thf(f1711,plain,(
% 1.10/0.39 $false | (~spl19_3 | ~spl19_13 | ~spl19_66 | ~spl19_74)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1710])).
% 1.10/0.39 thf(f1712,plain,(
% 1.10/0.39 ~spl19_3 | ~spl19_13 | ~spl19_66 | ~spl19_74),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1711])).
% 1.10/0.39 thf(f1718,plain,(
% 1.10/0.39 ($false != ((f2 @ $false))) | (spl19_41 | ~spl19_73)),
% 1.10/0.39 inference(forward_demodulation,[],[f260,f407])).
% 1.10/0.39 thf(f1719,plain,(
% 1.10/0.39 $false | (~spl19_3 | ~spl19_13 | spl19_41 | ~spl19_73)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1718,f1663])).
% 1.10/0.39 thf(f1720,plain,(
% 1.10/0.39 ~spl19_3 | ~spl19_13 | spl19_41 | ~spl19_73),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1719])).
% 1.10/0.39 thf(f1722,plain,(
% 1.10/0.39 ($true = ((f0 @ $true))) | (~spl19_20 | ~spl19_36)),
% 1.10/0.39 inference(forward_demodulation,[],[f238,f166])).
% 1.10/0.39 thf(f1746,plain,(
% 1.10/0.39 ($true != ((f0 @ $true))) | (spl19_32 | ~spl19_48)),
% 1.10/0.39 inference(forward_demodulation,[],[f219,f292])).
% 1.10/0.39 thf(f1754,plain,(
% 1.10/0.39 (((f0 @ $false)) = $true) | (~spl19_50 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f301,f402])).
% 1.10/0.39 thf(f1765,plain,(
% 1.10/0.39 $false | (spl19_41 | ~spl19_66 | ~spl19_73 | ~spl19_75)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1718,f1677])).
% 1.10/0.39 thf(f1766,plain,(
% 1.10/0.39 spl19_41 | ~spl19_66 | ~spl19_73 | ~spl19_75),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1765])).
% 1.10/0.39 thf(f1778,plain,(
% 1.10/0.39 $false | (~spl19_20 | spl19_32 | ~spl19_36 | ~spl19_48)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1746,f1722])).
% 1.10/0.39 thf(f1779,plain,(
% 1.10/0.39 ~spl19_20 | spl19_32 | ~spl19_36 | ~spl19_48),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1778])).
% 1.10/0.39 thf(f1781,plain,(
% 1.10/0.39 ($true != ((f1 @ $true))) | (spl19_18 | ~spl19_54)),
% 1.10/0.39 inference(forward_demodulation,[],[f156,f319])).
% 1.10/0.39 thf(f1782,plain,(
% 1.10/0.39 ($false = ((f1 @ $true))) | (~spl19_19 | ~spl19_54)),
% 1.10/0.39 inference(forward_demodulation,[],[f162,f319])).
% 1.10/0.39 thf(f1784,plain,(
% 1.10/0.39 ~spl19_77 | spl19_18 | ~spl19_54),
% 1.10/0.39 inference(avatar_split_clause,[],[f1781,f317,f155,f494])).
% 1.10/0.39 thf(f1785,plain,(
% 1.10/0.39 spl19_78 | ~spl19_19 | ~spl19_54),
% 1.10/0.39 inference(avatar_split_clause,[],[f1782,f317,f160,f514])).
% 1.10/0.39 thf(f1797,plain,(
% 1.10/0.39 ($true != ((f1 @ $false))) | (spl19_5 | ~spl19_40)),
% 1.10/0.39 inference(forward_demodulation,[],[f98,f256])).
% 1.10/0.39 thf(f1799,plain,(
% 1.10/0.39 ($false = ((f0 @ $false))) | (~spl19_17 | ~spl19_34)),
% 1.10/0.39 inference(forward_demodulation,[],[f229,f153])).
% 1.10/0.39 thf(f1801,plain,(
% 1.10/0.39 ($true = ((f1 @ $false))) | (~spl19_6 | ~spl19_45)),
% 1.10/0.39 inference(forward_demodulation,[],[f279,f103])).
% 1.10/0.39 thf(f1816,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_17 | ~spl19_34 | ~spl19_50 | ~spl19_72)),
% 1.10/0.39 inference(forward_demodulation,[],[f1799,f1754])).
% 1.10/0.39 thf(f1817,plain,(
% 1.10/0.39 $false | (~spl19_17 | ~spl19_34 | ~spl19_50 | ~spl19_72)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f1816])).
% 1.10/0.39 thf(f1818,plain,(
% 1.10/0.39 ~spl19_17 | ~spl19_34 | ~spl19_50 | ~spl19_72),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1817])).
% 1.10/0.39 thf(f1821,plain,(
% 1.10/0.39 $false | (spl19_5 | ~spl19_6 | ~spl19_40 | ~spl19_45)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1801,f1797])).
% 1.10/0.39 thf(f1822,plain,(
% 1.10/0.39 spl19_5 | ~spl19_6 | ~spl19_40 | ~spl19_45),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1821])).
% 1.10/0.39 thf(f1845,plain,(
% 1.10/0.39 ($false != ((f3 @ $true))) | (spl19_1 | ~spl19_22)),
% 1.10/0.39 inference(forward_demodulation,[],[f80,f175])).
% 1.10/0.39 thf(f1853,plain,(
% 1.10/0.39 ($false = ((f3 @ $true))) | (~spl19_26 | ~spl19_58)),
% 1.10/0.39 inference(forward_demodulation,[],[f193,f337])).
% 1.10/0.39 thf(f1858,plain,(
% 1.10/0.39 ($false != ((f4 @ $true))) | (x = $false) | spl19_57),
% 1.10/0.39 inference(constrained_superposition,[],[f332,f6])).
% 1.10/0.39 thf(f1860,plain,(
% 1.10/0.39 ($false != ((f4 @ $true))) | (spl19_57 | spl19_82)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1858,f576])).
% 1.10/0.39 thf(f1861,plain,(
% 1.10/0.39 ~spl19_81 | spl19_57 | spl19_82),
% 1.10/0.39 inference(avatar_split_clause,[],[f1860,f575,f331,f571])).
% 1.10/0.39 thf(f1889,plain,(
% 1.10/0.39 $false | (spl19_1 | ~spl19_22 | ~spl19_26 | ~spl19_58)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1853,f1845])).
% 1.10/0.39 thf(f1890,plain,(
% 1.10/0.39 spl19_1 | ~spl19_22 | ~spl19_26 | ~spl19_58),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1889])).
% 1.10/0.39 thf(f1897,plain,(
% 1.10/0.39 ($false != ((f3 @ $true))) | (~spl19_11 | spl19_68)),
% 1.10/0.39 inference(forward_demodulation,[],[f383,f126])).
% 1.10/0.39 thf(f1899,plain,(
% 1.10/0.39 (((f2 @ $true)) = $true) | (~spl19_43 | ~spl19_76)),
% 1.10/0.39 inference(forward_demodulation,[],[f270,f420])).
% 1.10/0.39 thf(f1958,plain,(
% 1.10/0.39 $false | (~spl19_11 | ~spl19_26 | ~spl19_58 | spl19_68)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1897,f1853])).
% 1.10/0.39 thf(f1959,plain,(
% 1.10/0.39 ~spl19_11 | ~spl19_26 | ~spl19_58 | spl19_68),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f1958])).
% 1.10/0.39 thf(f1962,plain,(
% 1.10/0.39 ($false != ((f2 @ $false))) | (~spl19_3 | spl19_13)),
% 1.10/0.39 inference(forward_demodulation,[],[f134,f90])).
% 1.10/0.39 thf(f1990,plain,(
% 1.10/0.39 ($false = ((f2 @ $false))) | (~spl19_44 | ~spl19_53)),
% 1.10/0.39 inference(forward_demodulation,[],[f315,f274])).
% 1.10/0.39 thf(f2009,plain,(
% 1.10/0.39 $false | (~spl19_3 | spl19_13 | ~spl19_44 | ~spl19_53)),
% 1.10/0.39 inference(forward_subsumption_resolution,[],[f1990,f1962])).
% 1.10/0.39 thf(f2010,plain,(
% 1.10/0.39 ~spl19_3 | spl19_13 | ~spl19_44 | ~spl19_53),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f2009])).
% 1.10/0.39 thf(f2012,plain,(
% 1.10/0.39 ($false = ((f2 @ $true))) | (~spl19_42 | ~spl19_53)),
% 1.10/0.39 inference(forward_demodulation,[],[f315,f265])).
% 1.10/0.39 thf(f2013,plain,(
% 1.10/0.39 ($false = $true) | (~spl19_42 | ~spl19_43 | ~spl19_53 | ~spl19_76)),
% 1.10/0.39 inference(forward_demodulation,[],[f2012,f1899])).
% 1.10/0.39 thf(f2014,plain,(
% 1.10/0.39 $false | (~spl19_42 | ~spl19_43 | ~spl19_53 | ~spl19_76)),
% 1.10/0.39 inference(trivial_inequality_removal,[],[f2013])).
% 1.10/0.39 thf(f2015,plain,(
% 1.10/0.39 ~spl19_42 | ~spl19_43 | ~spl19_53 | ~spl19_76),
% 1.10/0.39 inference(avatar_contradiction_clause,[],[f2014])).
% 1.10/0.39 cnf(s1, plain, spl19_1 | spl19_2, inference(sat_conversion,[],[f86])).
% 1.10/0.39 cnf(s2, plain, spl19_3 | spl19_4, inference(sat_conversion,[],[f95])).
% 1.10/0.39 cnf(s3, plain, spl19_5 | spl19_6, inference(sat_conversion,[],[f104])).
% 1.10/0.39 cnf(s4, plain, spl19_7 | spl19_8, inference(sat_conversion,[],[f113])).
% 1.10/0.39 cnf(s5, plain, spl19_9 | spl19_10, inference(sat_conversion,[],[f122])).
% 1.10/0.39 cnf(s6, plain, spl19_11 | spl19_12, inference(sat_conversion,[],[f131])).
% 1.10/0.39 cnf(s7, plain, spl19_13 | spl19_14, inference(sat_conversion,[],[f140])).
% 1.10/0.39 cnf(s8, plain, spl19_15 | spl19_16, inference(sat_conversion,[],[f149])).
% 1.10/0.39 cnf(s9, plain, spl19_17 | spl19_18, inference(sat_conversion,[],[f158])).
% 1.10/0.39 cnf(s10, plain, spl19_19 | spl19_20, inference(sat_conversion,[],[f167])).
% 1.10/0.39 cnf(s11, plain, spl19_21 | spl19_22, inference(sat_conversion,[],[f176])).
% 1.10/0.39 cnf(s12, plain, spl19_23 | spl19_24, inference(sat_conversion,[],[f185])).
% 1.10/0.39 cnf(s13, plain, spl19_25 | spl19_26, inference(sat_conversion,[],[f194])).
% 1.10/0.39 cnf(s14, plain, spl19_27 | spl19_28, inference(sat_conversion,[],[f203])).
% 1.10/0.39 cnf(s15, plain, spl19_29 | spl19_30, inference(sat_conversion,[],[f212])).
% 1.10/0.39 cnf(s16, plain, spl19_31 | spl19_32, inference(sat_conversion,[],[f221])).
% 1.10/0.39 cnf(s17, plain, spl19_33 | spl19_34, inference(sat_conversion,[],[f230])).
% 1.10/0.39 cnf(s18, plain, spl19_35 | spl19_36, inference(sat_conversion,[],[f239])).
% 1.10/0.39 cnf(s19, plain, spl19_37 | spl19_38, inference(sat_conversion,[],[f248])).
% 1.10/0.39 cnf(s20, plain, spl19_39 | spl19_40, inference(sat_conversion,[],[f257])).
% 1.10/0.39 cnf(s21, plain, spl19_41 | spl19_42, inference(sat_conversion,[],[f266])).
% 1.10/0.39 cnf(s22, plain, spl19_43 | spl19_44, inference(sat_conversion,[],[f275])).
% 1.10/0.39 cnf(s23, plain, spl19_45 | spl19_46, inference(sat_conversion,[],[f284])).
% 1.10/0.39 cnf(s24, plain, spl19_47 | spl19_48, inference(sat_conversion,[],[f293])).
% 1.10/0.39 cnf(s25, plain, spl19_49 | spl19_50, inference(sat_conversion,[],[f302])).
% 1.10/0.39 cnf(s26, plain, spl19_51 | spl19_52, inference(sat_conversion,[],[f311])).
% 1.10/0.39 cnf(s27, plain, spl19_53 | spl19_54, inference(sat_conversion,[],[f320])).
% 1.10/0.39 cnf(s28, plain, spl19_55 | spl19_56, inference(sat_conversion,[],[f329])).
% 1.10/0.39 cnf(s29, plain, spl19_57 | spl19_58, inference(sat_conversion,[],[f338])).
% 1.10/0.39 cnf(s30, plain, spl19_59 | spl19_60, inference(sat_conversion,[],[f347])).
% 1.10/0.39 cnf(s31, plain, spl19_61 | spl19_62, inference(sat_conversion,[],[f356])).
% 1.10/0.39 cnf(s32, plain, spl19_63 | spl19_64, inference(sat_conversion,[],[f365])).
% 1.10/0.39 cnf(s33, plain, spl19_31 | spl19_49, inference(sat_conversion,[],[f366])).
% 1.10/0.39 cnf(s34, plain, spl19_30 | spl19_51, inference(sat_conversion,[],[f367])).
% 1.10/0.39 cnf(s35, plain, spl19_65 | spl19_66, inference(sat_conversion,[],[f376])).
% 1.10/0.39 cnf(s36, plain, spl19_67 | spl19_68, inference(sat_conversion,[],[f385])).
% 1.10/0.39 cnf(s37, plain, spl19_69 | spl19_70, inference(sat_conversion,[],[f394])).
% 1.10/0.39 cnf(s38, plain, spl19_71 | spl19_72, inference(sat_conversion,[],[f403])).
% 1.10/0.39 cnf(s39, plain, spl19_73 | spl19_74, inference(sat_conversion,[],[f412])).
% 1.10/0.39 cnf(s40, plain, spl19_75 | spl19_76, inference(sat_conversion,[],[f421])).
% 1.10/0.39 cnf(s41, plain, ~spl19_2 | ~spl19_3, inference(sat_conversion,[],[f431])).
% 1.10/0.39 cnf(s43, plain, ~spl19_9 | ~spl19_11, inference(sat_conversion,[],[f442])).
% 1.10/0.39 cnf(s44, plain, ~spl19_25 | ~spl19_27, inference(sat_conversion,[],[f453])).
% 1.10/0.39 cnf(s45, plain, spl19_25 | spl19_27, inference(sat_conversion,[],[f456])).
% 1.10/0.39 cnf(s46, plain, ~spl19_33 | ~spl19_35, inference(sat_conversion,[],[f464])).
% 1.10/0.39 cnf(s47, plain, spl19_33 | spl19_35, inference(sat_conversion,[],[f468])).
% 1.10/0.39 cnf(s48, plain, ~spl19_49 | ~spl19_51, inference(sat_conversion,[],[f476])).
% 1.10/0.39 cnf(s49, plain, ~spl19_61 | ~spl19_63, inference(sat_conversion,[],[f485])).
% 1.10/0.39 cnf(s51, plain, ~spl19_5 | ~spl19_7, inference(sat_conversion,[],[f503])).
% 1.10/0.39 cnf(s53, plain, ~spl19_17 | ~spl19_20, inference(sat_conversion,[],[f520])).
% 1.10/0.39 cnf(s54, plain, ~spl19_18 | spl19_56 | spl19_77, inference(sat_conversion,[],[f524])).
% 1.10/0.39 cnf(s57, plain, ~spl19_53 | ~spl19_55, inference(sat_conversion,[],[f565])).
% 1.10/0.39 cnf(s61, plain, ~spl19_3 | ~spl19_13 | ~spl19_16, inference(sat_conversion,[],[f602])).
% 1.10/0.39 cnf(s62, plain, ~spl19_14 | ~spl19_37 | spl19_78, inference(sat_conversion,[],[f606])).
% 1.10/0.39 cnf(s65, plain, spl19_5 | spl19_7, inference(sat_conversion,[],[f623])).
% 1.10/0.39 cnf(s71, plain, ~spl19_7 | ~spl19_38 | spl19_78, inference(sat_conversion,[],[f638])).
% 1.10/0.39 cnf(s74, plain, ~spl19_2 | ~spl19_13 | spl19_80, inference(sat_conversion,[],[f653])).
% 1.10/0.39 cnf(s75, plain, ~spl19_41 | ~spl19_43 | ~spl19_73, inference(sat_conversion,[],[f665])).
% 1.10/0.39 cnf(s76, plain, ~spl19_6 | ~spl19_19 | ~spl19_45 | ~spl19_56, inference(sat_conversion,[],[f670])).
% 1.10/0.39 cnf(s77, plain, ~spl19_17 | ~spl19_34 | ~spl19_35 | ~spl19_71, inference(sat_conversion,[],[f683])).
% 1.10/0.39 cnf(s78, plain, ~spl19_4 | ~spl19_21 | ~spl19_23 | ~spl19_27, inference(sat_conversion,[],[f689])).
% 1.10/0.39 cnf(s79, plain, ~spl19_11 | ~spl19_21 | ~spl19_25 | ~spl19_65, inference(sat_conversion,[],[f695])).
% 1.10/0.39 cnf(s80, plain, ~spl19_10 | ~spl19_12 | ~spl19_63, inference(sat_conversion,[],[f699])).
% 1.10/0.39 cnf(s85, plain, ~spl19_11 | ~spl19_24 | ~spl19_25 | ~spl19_68, inference(sat_conversion,[],[f756])).
% 1.10/0.39 cnf(s86, plain, ~spl19_11 | ~spl19_65 | ~spl19_68, inference(sat_conversion,[],[f761])).
% 1.10/0.39 cnf(s87, plain, ~spl19_11 | spl19_21 | ~spl19_25 | ~spl19_68, inference(sat_conversion,[],[f763])).
% 1.10/0.39 cnf(s88, plain, ~spl19_2 | ~spl19_16 | ~spl19_67 | ~spl19_75, inference(sat_conversion,[],[f773])).
% 1.10/0.39 cnf(s92, plain, ~spl19_17 | ~spl19_29 | ~spl19_36 | ~spl19_46, inference(sat_conversion,[],[f801])).
% 1.10/0.39 cnf(s93, plain, ~spl19_50 | ~spl19_69 | ~spl19_79, inference(sat_conversion,[],[f805])).
% 1.10/0.39 cnf(s95, plain, ~spl19_5 | ~spl19_19 | ~spl19_40 | ~spl19_56, inference(sat_conversion,[],[f811])).
% 1.10/0.39 cnf(s96, plain, ~spl19_30 | ~spl19_31, inference(sat_conversion,[],[f816])).
% 1.10/0.39 cnf(s97, plain, ~spl19_33 | ~spl19_70 | spl19_79, inference(sat_conversion,[],[f818])).
% 1.10/0.39 cnf(s99, plain, spl19_69 | spl19_72, inference(sat_conversion,[],[f834])).
% 1.10/0.39 cnf(s100, plain, ~spl19_52 | ~spl19_69 | spl19_79, inference(sat_conversion,[],[f843])).
% 1.10/0.39 cnf(s101, plain, ~spl19_33 | spl19_50 | ~spl19_69 | ~spl19_71, inference(sat_conversion,[],[f849])).
% 1.10/0.39 cnf(s103, plain, ~spl19_17 | ~spl19_36 | ~spl19_52 | ~spl19_72, inference(sat_conversion,[],[f858])).
% 1.10/0.39 cnf(s104, plain, ~spl19_15 | ~spl19_19 | ~spl19_39 | ~spl19_56, inference(sat_conversion,[],[f865])).
% 1.10/0.39 cnf(s106, plain, ~spl19_67 | spl19_75 | ~spl19_80, inference(sat_conversion,[],[f871])).
% 1.10/0.39 cnf(s112, plain, ~spl19_18 | ~spl19_19 | ~spl19_56, inference(sat_conversion,[],[f915])).
% 1.10/0.39 cnf(s113, plain, ~spl19_41 | ~spl19_76 | spl19_80, inference(sat_conversion,[],[f933])).
% 1.10/0.39 cnf(s114, plain, ~spl19_8 | ~spl19_47 | ~spl19_77, inference(sat_conversion,[],[f939])).
% 1.10/0.39 cnf(s115, plain, ~spl19_9 | ~spl19_28 | ~spl19_59 | ~spl19_68, inference(sat_conversion,[],[f949])).
% 1.10/0.39 cnf(s116, plain, ~spl19_57 | ~spl19_60, inference(sat_conversion,[],[f952])).
% 1.10/0.39 cnf(s122, plain, spl19_10 | ~spl19_58 | ~spl19_62 | ~spl19_63, inference(sat_conversion,[],[f994])).
% 1.10/0.39 cnf(s123, plain, ~spl19_58 | ~spl19_64 | spl19_81, inference(sat_conversion,[],[f996])).
% 1.10/0.39 cnf(s124, plain, spl19_61 | spl19_63, inference(sat_conversion,[],[f1000])).
% 1.10/0.39 cnf(s125, plain, spl19_61 | spl19_63, inference(sat_conversion,[],[f1001])).
% 1.10/0.39 cnf(s126, plain, ~spl19_12 | ~spl19_60 | ~spl19_61 | ~spl19_82, inference(sat_conversion,[],[f1008])).
% 1.10/0.39 cnf(s127, plain, ~spl19_58 | ~spl19_59, inference(sat_conversion,[],[f1011])).
% 1.10/0.39 cnf(s128, plain, spl19_9 | spl19_11, inference(sat_conversion,[],[f1018])).
% 1.10/0.39 cnf(s130, plain, spl19_58 | spl19_59, inference(sat_conversion,[],[f1027])).
% 1.10/0.39 cnf(s132, plain, ~spl19_10 | ~spl19_12 | ~spl19_61, inference(sat_conversion,[],[f1049])).
% 1.10/0.39 cnf(s133, plain, spl19_21 | ~spl19_26 | ~spl19_27 | ~spl19_59, inference(sat_conversion,[],[f1060])).
% 1.10/0.39 cnf(s134, plain, ~spl19_24 | ~spl19_26 | ~spl19_27 | ~spl19_59, inference(sat_conversion,[],[f1063])).
% 1.10/0.39 cnf(s143, plain, ~spl19_2 | spl19_16 | ~spl19_67 | ~spl19_74, inference(sat_conversion,[],[f1123])).
% 1.10/0.39 cnf(s145, plain, ~spl19_69 | ~spl19_72, inference(sat_conversion,[],[f1139])).
% 1.10/0.39 cnf(s146, plain, ~spl19_29 | ~spl19_32, inference(sat_conversion,[],[f1142])).
% 1.10/0.39 cnf(s147, plain, ~spl19_46 | ~spl19_48, inference(sat_conversion,[],[f1147])).
% 1.10/0.39 cnf(s149, plain, ~spl19_15 | ~spl19_18 | ~spl19_37 | ~spl19_56, inference(sat_conversion,[],[f1157])).
% 1.10/0.39 cnf(s151, plain, ~spl19_77 | ~spl19_78, inference(sat_conversion,[],[f1166])).
% 1.10/0.39 cnf(s154, plain, ~spl19_54 | ~spl19_56, inference(sat_conversion,[],[f1171])).
% 1.10/0.39 cnf(s155, plain, ~spl19_1 | ~spl19_4, inference(sat_conversion,[],[f1174])).
% 1.10/0.39 cnf(s158, plain, ~spl19_1 | ~spl19_22 | ~spl19_24 | ~spl19_25, inference(sat_conversion,[],[f1183])).
% 1.10/0.39 cnf(s159, plain, ~spl19_22 | ~spl19_23, inference(sat_conversion,[],[f1186])).
% 1.10/0.39 cnf(s162, plain, spl19_22 | spl19_23, inference(sat_conversion,[],[f1204])).
% 1.10/0.39 cnf(s164, plain, spl19_42 | spl19_44, inference(sat_conversion,[],[f1216])).
% 1.10/0.39 cnf(s165, plain, ~spl19_1 | ~spl19_9 | ~spl19_23 | ~spl19_65, inference(sat_conversion,[],[f1231])).
% 1.10/0.39 cnf(s169, plain, ~spl19_6 | ~spl19_18 | ~spl19_47 | ~spl19_56, inference(sat_conversion,[],[f1255])).
% 1.10/0.39 cnf(s171, plain, spl19_7 | ~spl19_38 | ~spl19_78, inference(sat_conversion,[],[f1261])).
% 1.10/0.39 cnf(s174, plain, ~spl19_18 | ~spl19_54 | spl19_77, inference(sat_conversion,[],[f1279])).
% 1.10/0.39 cnf(s177, plain, ~spl19_41 | ~spl19_44 | spl19_53 | ~spl19_73, inference(sat_conversion,[],[f1311])).
% 1.10/0.39 cnf(s178, plain, ~spl19_42 | spl19_53 | ~spl19_80, inference(sat_conversion,[],[f1316])).
% 1.10/0.39 cnf(s179, plain, ~spl19_20 | ~spl19_34 | spl19_79, inference(sat_conversion,[],[f1324])).
% 1.10/0.39 cnf(s183, plain, spl19_54 | spl19_56, inference(sat_conversion,[],[f1342])).
% 1.10/0.39 cnf(s186, plain, spl19_29 | ~spl19_48 | ~spl19_79, inference(sat_conversion,[],[f1351])).
% 1.10/0.39 cnf(s187, plain, ~spl19_8 | ~spl19_47 | spl19_78, inference(sat_conversion,[],[f1356])).
% 1.10/0.39 cnf(s192, plain, spl19_12 | ~spl19_63 | ~spl19_81, inference(sat_conversion,[],[f1387])).
% 1.10/0.39 cnf(s194, plain, ~spl19_14 | ~spl19_39 | spl19_77, inference(sat_conversion,[],[f1397])).
% 1.10/0.39 cnf(s196, plain, ~spl19_8 | ~spl19_45 | spl19_77, inference(sat_conversion,[],[f1401])).
% 1.10/0.39 cnf(s203, plain, spl19_24 | ~spl19_25 | ~spl19_28 | ~spl19_58, inference(sat_conversion,[],[f1448])).
% 1.10/0.39 cnf(s206, plain, ~spl19_2 | ~spl19_16 | ~spl19_42 | spl19_55, inference(sat_conversion,[],[f1462])).
% 1.10/0.39 cnf(s208, plain, ~spl19_57 | ~spl19_59 | ~spl19_62 | ~spl19_82, inference(sat_conversion,[],[f1499])).
% 1.10/0.39 cnf(s210, plain, ~spl19_57 | spl19_81 | spl19_82, inference(sat_conversion,[],[f1516])).
% 1.10/0.39 cnf(s211, plain, ~spl19_10 | ~spl19_59 | ~spl19_61 | ~spl19_64, inference(sat_conversion,[],[f1523])).
% 1.10/0.39 cnf(s217, plain, ~spl19_29 | ~spl19_48 | spl19_79, inference(sat_conversion,[],[f1560])).
% 1.10/0.39 cnf(s222, plain, ~spl19_35 | ~spl19_50 | ~spl19_70 | ~spl19_72, inference(sat_conversion,[],[f1600])).
% 1.10/0.39 cnf(s224, plain, spl19_29 | ~spl19_35 | ~spl19_46 | ~spl19_70, inference(sat_conversion,[],[f1629])).
% 1.10/0.39 cnf(s227, plain, spl19_73 | spl19_76, inference(sat_conversion,[],[f1661])).
% 1.10/0.39 cnf(s233, plain, ~spl19_3 | ~spl19_13 | ~spl19_44 | ~spl19_55, inference(sat_conversion,[],[f1693])).
% 1.10/0.39 cnf(s237, plain, ~spl19_3 | ~spl19_13 | ~spl19_66 | ~spl19_74, inference(sat_conversion,[],[f1712])).
% 1.10/0.39 cnf(s238, plain, ~spl19_3 | ~spl19_13 | spl19_41 | ~spl19_73, inference(sat_conversion,[],[f1720])).
% 1.10/0.39 cnf(s249, plain, spl19_41 | ~spl19_66 | ~spl19_73 | ~spl19_75, inference(sat_conversion,[],[f1766])).
% 1.10/0.39 cnf(s250, plain, ~spl19_20 | spl19_32 | ~spl19_36 | ~spl19_48, inference(sat_conversion,[],[f1779])).
% 1.10/0.39 cnf(s252, plain, spl19_18 | ~spl19_54 | ~spl19_77, inference(sat_conversion,[],[f1784])).
% 1.10/0.39 cnf(s253, plain, ~spl19_19 | ~spl19_54 | spl19_78, inference(sat_conversion,[],[f1785])).
% 1.10/0.39 cnf(s257, plain, ~spl19_17 | ~spl19_34 | ~spl19_50 | ~spl19_72, inference(sat_conversion,[],[f1818])).
% 1.10/0.39 cnf(s258, plain, spl19_5 | ~spl19_6 | ~spl19_40 | ~spl19_45, inference(sat_conversion,[],[f1822])).
% 1.10/0.39 cnf(s266, plain, spl19_57 | ~spl19_81 | spl19_82, inference(sat_conversion,[],[f1861])).
% 1.10/0.39 cnf(s269, plain, spl19_1 | ~spl19_22 | ~spl19_26 | ~spl19_58, inference(sat_conversion,[],[f1890])).
% 1.10/0.39 cnf(s281, plain, ~spl19_11 | ~spl19_26 | ~spl19_58 | spl19_68, inference(sat_conversion,[],[f1959])).
% 1.10/0.39 cnf(s289, plain, ~spl19_3 | spl19_13 | ~spl19_44 | ~spl19_53, inference(sat_conversion,[],[f2010])).
% 1.10/0.39 cnf(s290, plain, ~spl19_42 | ~spl19_43 | ~spl19_53 | ~spl19_76, inference(sat_conversion,[],[f2015])).
% 1.10/0.39 cnf(s291, plain, spl19_25 | ~spl19_22 | spl19_1, inference(rat,[],[s130,s269,s134,s13,s45,s12,s159])).
% 1.10/0.39 cnf(s292, plain, spl19_78 | ~spl19_14 | ~spl19_7, inference(rat,[],[s19,s62,s71])).
% 1.10/0.39 cnf(s294, plain, spl19_21 | ~spl19_68 | ~spl19_11 | spl19_1, inference(rat,[],[s291,s87,s11])).
% 1.10/0.39 cnf(s295, plain, ~spl19_22 | ~spl19_68 | ~spl19_11 | spl19_1, inference(rat,[],[s85,s12,s291,s159])).
% 1.10/0.39 cnf(s296, plain, spl19_33 | spl19_29 | ~spl19_17 | ~spl19_46, inference(rat,[],[s145,s38,s37,s77,s224,s17,s47])).
% 1.10/0.39 cnf(s297, plain, spl19_29 | ~spl19_17 | ~spl19_46, inference(rat,[],[s101,s93,s100,s38,s99,s103,s18,s46,s296,s26,s48,s33,s96,s15])).
% 1.10/0.39 cnf(s298, plain, ~spl19_17 | ~spl19_46, inference(rat,[],[s257,s38,s25,s77,s48,s17,s34,s46,s96,s18,s16,s92,s146,s297])).
% 1.10/0.39 cnf(s299, plain, ~spl19_14 | spl19_5, inference(rat,[],[s169,s54,s9,s298,s24,s147,s23,s258,s20,s194,s151,s292,s65,s3])).
% 1.10/0.39 cnf(s300, plain, spl19_61 | spl19_58 | spl19_12, inference(rat,[],[s210,s208,s192,s31,s125,s130,s29])).
% 1.10/0.39 cnf(s301, plain, spl19_58 | spl19_12 | ~spl19_10, inference(rat,[],[s32,s211,s49,s300,s130])).
% 1.10/0.39 cnf(s302, plain, ~spl19_67 | ~spl19_74 | ~spl19_80 | ~spl19_2, inference(rat,[],[s88,s143,s106])).
% 1.10/0.39 cnf(s303, plain, ~spl19_68 | ~spl19_58 | ~spl19_11 | spl19_1, inference(rat,[],[s203,s85,s14,s45,s78,s162,s295,s294,s2,s41,s1])).
% 1.10/0.39 cnf(s304, plain, spl19_53 | ~spl19_73 | ~spl19_80, inference(rat,[],[s177,s21,s164,s178])).
% 1.10/0.39 cnf(s305, plain, ~spl19_17 | ~spl19_56 | ~spl19_6, inference(rat,[],[s76,s23,s10,s298,s53])).
% 1.10/0.39 cnf(s306, plain, spl19_29 | ~spl19_20 | ~spl19_48, inference(rat,[],[s100,s37,s26,s97,s48,s17,s33,s179,s96,s186,s15])).
% 1.10/0.39 cnf(s307, plain, ~spl19_20 | ~spl19_48, inference(rat,[],[s222,s37,s99,s93,s25,s48,s34,s18,s96,s250,s16,s146,s217,s306])).
% 1.10/0.39 cnf(s308, plain, ~spl19_18 | ~spl19_56 | ~spl19_6, inference(rat,[],[s307,s10,s24,s112,s169])).
% 1.10/0.39 cnf(s309, plain, ~spl19_56 | ~spl19_6, inference(rat,[],[s308,s9,s305])).
% 1.10/0.39 cnf(s310, plain, ~spl19_12 | ~spl19_10, inference(rat,[],[s124,s80,s132])).
% 1.10/0.39 cnf(s311, plain, spl19_58 | ~spl19_10, inference(rat,[],[s310,s301])).
% 1.10/0.39 cnf(s312, plain, spl19_9 | ~spl19_68 | spl19_1, inference(rat,[],[s311,s303,s5,s128])).
% 1.10/0.39 cnf(s313, plain, ~spl19_59 | ~spl19_68 | spl19_1, inference(rat,[],[s78,s162,s133,s291,s13,s44,s14,s115,s2,s41,s1,s312])).
% 1.10/0.39 cnf(s314, plain, spl19_61 | ~spl19_58 | spl19_10, inference(rat,[],[s122,s31,s125])).
% 1.10/0.39 cnf(s315, plain, ~spl19_68 | spl19_1, inference(rat,[],[s123,s266,s32,s126,s49,s314,s116,s30,s130,s313,s310,s6,s43,s312])).
% 1.10/0.39 cnf(s316, plain, ~spl19_80 | spl19_53 | spl19_1, inference(rat,[],[s39,s304,s302,s1,s36,s315])).
% 1.10/0.39 cnf(s317, plain, spl19_18 | ~spl19_8 | ~spl19_54, inference(rat,[],[s23,s298,s196,s9,s252])).
% 1.10/0.39 cnf(s318, plain, ~spl19_8 | ~spl19_54, inference(rat,[],[s307,s10,s24,s253,s114,s151,s174,s317])).
% 1.10/0.39 cnf(s319, plain, spl19_56 | spl19_1, inference(rat,[],[s318,s4,s51,s299,s7,s74,s316,s57,s28,s183,s1])).
% 1.10/0.39 cnf(s320, plain, ~spl19_19 | ~spl19_15 | ~spl19_56, inference(rat,[],[s20,s95,s104,s3,s309])).
% 1.10/0.39 cnf(s321, plain, ~spl19_15 | ~spl19_56, inference(rat,[],[s171,s19,s187,s149,s24,s9,s307,s53,s10,s320,s4,s51,s3,s309])).
% 1.10/0.39 cnf(s322, plain, spl19_1, inference(rat,[],[s113,s21,s40,s106,s206,s88,s8,s321,s57,s27,s154,s319,s36,s315,s1])).
% 1.10/0.39 cnf(s323, plain, ~spl19_4, inference(rat,[],[s155,s322])).
% 1.10/0.39 cnf(s324, plain, spl19_3, inference(rat,[],[s2,s323])).
% 1.10/0.39 cnf(s326, plain, ~spl19_73 | spl19_56, inference(rat,[],[s75,s238,s22,s233,s7,s299,s51,s4,s318,s183,s28,s324])).
% 1.10/0.39 cnf(s327, plain, spl19_58 | ~spl19_65, inference(rat,[],[s134,s13,s45,s158,s12,s162,s165,s5,s311,s130,s322])).
% 1.10/0.39 cnf(s328, plain, ~spl19_11 | ~spl19_65, inference(rat,[],[s158,s203,s11,s14,s79,s44,s13,s281,s86,s327,s322])).
% 1.10/0.39 cnf(s329, plain, ~spl19_65, inference(rat,[],[s123,s266,s32,s126,s49,s314,s310,s6,s328,s116,s30,s127,s327])).
% 1.10/0.39 cnf(s330, plain, spl19_66, inference(rat,[],[s35,s329])).
% 1.10/0.39 cnf(s333, plain, spl19_56, inference(rat,[],[s299,s7,s51,s237,s4,s39,s318,s326,s183,s330,s324])).
% 1.10/0.39 cnf(s334, plain, ~spl19_54, inference(rat,[],[s154,s333])).
% 1.10/0.39 cnf(s336, plain, ~spl19_15, inference(rat,[],[s321,s333])).
% 1.10/0.39 cnf(s337, plain, spl19_53, inference(rat,[],[s27,s334])).
% 1.10/0.39 cnf(s340, plain, spl19_16, inference(rat,[],[s8,s336])).
% 1.10/0.39 cnf(s343, plain, ~spl19_13, inference(rat,[],[s61,s324,s340])).
% 1.10/0.39 cnf(s345, plain, ~spl19_44, inference(rat,[],[s289,s337,s324,s343])).
% 1.10/0.39 cnf(s346, plain, spl19_42, inference(rat,[],[s164,s345])).
% 1.10/0.39 cnf(s348, plain, spl19_43, inference(rat,[],[s22,s345])).
% 1.10/0.39 cnf(s349, plain, ~spl19_76, inference(rat,[],[s290,s346,s337,s348])).
% 1.10/0.39 cnf(s350, plain, spl19_73, inference(rat,[],[s227,s349])).
% 1.10/0.39 cnf(s351, plain, spl19_75, inference(rat,[],[s40,s349])).
% 1.10/0.39 cnf(s352, plain, ~spl19_41, inference(rat,[],[s75,s348,s350])).
% 1.10/0.39 cnf(s353, plain, $false, inference(rat,[],[s249,s351,s330,s350,s352])).
% 1.10/0.39 thf(f2016,plain,(
% 1.10/0.39 $false),
% 1.10/0.39 inference(avatar_sat_refutation,[],[s353])).
% 1.10/0.39 % SZS output end Proof for theBenchmark
% 1.10/0.39 % (3825618)------------------------------
% 1.10/0.39 % (3825618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.39 % (3825618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.39 % (3825618)CaDiCaL version: 2.1.3
% 1.10/0.39 % (3825618)Termination reason: Refutation
% 1.10/0.39 % (3825618)Time elapsed: 0.092 s
% 1.10/0.39 % (3825618)Peak memory usage: 13 MB
% 1.10/0.39 % (3825618)Instructions burned: 92 (million)
% 1.10/0.39 % (3825607)Success in time 0.142 s
% 1.10/0.39 % Vampire exiting
%------------------------------------------------------------------------------