%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU691^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:30:48 AM UTC 2026
% Result : Theorem 0.89s 0.46s
% Output : Refutation 1.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU691^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n003.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 14:12:31 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.35 % (2564161)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.19/0.35 % (2564171)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4111675509:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.19/0.35 % (2564172)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.19/0.35 % (2564172)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.19/0.35 % (2564167)lrs+10_16_si=on:nwc=1.5:random_seed=1219636461:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.19/0.35 % (2564166)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3380096453:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.19/0.35 % (2564168)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2526676839:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.19/0.35 % (2564170)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1670959502:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.19/0.35 % (2564169)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=266916475: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.19/0.35 % (2564172)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=839689442:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.19/0.35 % (2564168)Instruction limit reached!
% 0.19/0.35 % (2564168)------------------------------
% 0.19/0.35 % (2564168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (2564168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (2564168)CaDiCaL version: 2.1.3
% 0.19/0.35 % (2564168)Termination reason: Instruction limit
% 0.19/0.35 % (2564168)Termination phase: Property scanning
% 0.19/0.35 % (2564168)Time elapsed: 0.002 s
% 0.19/0.35 % (2564168)Peak memory usage: 10 MB
% 0.19/0.35 % (2564168)Instructions burned: 4 (million)
% 0.19/0.35 % (2564167)Instruction limit reached!
% 0.19/0.35 % (2564167)------------------------------
% 0.19/0.35 % (2564167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (2564167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (2564167)CaDiCaL version: 2.1.3
% 0.19/0.35 % (2564167)Termination reason: Instruction limit
% 0.19/0.35 % (2564167)Termination phase: Saturation
% 0.19/0.35 % (2564167)Time elapsed: 0.009 s
% 0.19/0.35 % (2564167)Peak memory usage: 12 MB
% 0.19/0.35 % (2564167)Instructions burned: 19 (million)
% 0.19/0.35 % (2564170)Instruction limit reached!
% 0.19/0.35 % (2564170)------------------------------
% 0.19/0.35 % (2564170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (2564170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (2564170)CaDiCaL version: 2.1.3
% 0.19/0.35 % (2564170)Termination reason: Instruction limit
% 0.19/0.35 % (2564170)Termination phase: Saturation
% 0.19/0.35 % (2564170)Time elapsed: 0.014 s
% 0.19/0.35 % (2564170)Peak memory usage: 12 MB
% 0.19/0.35 % (2564170)Instructions burned: 24 (million)
% 0.19/0.35 % (2564171)Instruction limit reached!
% 0.19/0.35 % (2564171)------------------------------
% 0.19/0.35 % (2564171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (2564171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (2564171)CaDiCaL version: 2.1.3
% 0.19/0.35 % (2564171)Termination reason: Instruction limit
% 0.19/0.35 % (2564171)Termination phase: Saturation
% 0.19/0.35 % (2564171)Time elapsed: 0.023 s
% 0.19/0.35 % (2564171)Peak memory usage: 13 MB
% 0.19/0.35 % (2564171)Instructions burned: 78 (million)
% 0.19/0.35 % (2564180)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2386687485:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.19/0.35 % (2564180)Instruction limit reached!
% 0.19/0.35 % (2564180)------------------------------
% 0.19/0.35 % (2564180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.37 % (2564180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.37 % (2564180)CaDiCaL version: 2.1.3
% 0.89/0.37 % (2564180)Termination reason: Instruction limit
% 0.89/0.37 % (2564180)Termination phase: Function definition elimination
% 0.89/0.37 % (2564180)Time elapsed: 0.002 s
% 0.89/0.37 % (2564180)Peak memory usage: 10 MB
% 0.89/0.37 % (2564180)Instructions burned: 4 (million)
% 0.89/0.37 % (2564183)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1697578190:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.89/0.37 % (2564181)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2345235482:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.89/0.37 % (2564182)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.37 % (2564183)Instruction limit reached!
% 0.89/0.37 % (2564183)------------------------------
% 0.89/0.37 % (2564183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.37 % (2564183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.37 % (2564183)CaDiCaL version: 2.1.3
% 0.89/0.37 % (2564183)Termination reason: Instruction limit
% 0.89/0.37 % (2564183)Termination phase: Saturation
% 0.89/0.37 % (2564183)Time elapsed: 0.003 s
% 0.89/0.37 % (2564183)Peak memory usage: 11 MB
% 0.89/0.37 % (2564183)Instructions burned: 12 (million)
% 0.89/0.37 % (2564181)Instruction limit reached!
% 0.89/0.37 % (2564181)------------------------------
% 0.89/0.37 % (2564181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.37 % (2564181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.37 % (2564181)CaDiCaL version: 2.1.3
% 0.89/0.37 % (2564181)Termination reason: Instruction limit
% 0.89/0.37 % (2564181)Termination phase: Saturation
% 0.89/0.37 % (2564181)Time elapsed: 0.003 s
% 0.89/0.37 % (2564181)Peak memory usage: 11 MB
% 0.89/0.37 % (2564181)Instructions burned: 6 (million)
% 0.89/0.37 % (2564182)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3003309755:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.89/0.37 % (2564182)Instruction limit reached!
% 0.89/0.37 % (2564182)------------------------------
% 0.89/0.37 % (2564182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.37 % (2564182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.37 % (2564182)CaDiCaL version: 2.1.3
% 0.89/0.37 % (2564182)Termination reason: Instruction limit
% 0.89/0.37 % (2564182)Termination phase: Saturation
% 0.89/0.37 % (2564182)Time elapsed: 0.004 s
% 0.89/0.37 % (2564182)Peak memory usage: 11 MB
% 0.89/0.37 % (2564182)Instructions burned: 9 (million)
% 0.89/0.37 % (2564185)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.89/0.37 % (2564185)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.37 % (2564188)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=970103844:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.89/0.37 % (2564166)Instruction limit reached!
% 0.89/0.37 % (2564166)------------------------------
% 0.89/0.37 % (2564166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.37 % (2564166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.37 % (2564166)CaDiCaL version: 2.1.3
% 0.89/0.37 % (2564166)Termination reason: Instruction limit
% 0.89/0.37 % (2564166)Termination phase: Saturation
% 0.89/0.37 % (2564166)Time elapsed: 0.043 s
% 0.89/0.37 % (2564166)Peak memory usage: 13 MB
% 0.89/0.37 % (2564166)Instructions burned: 88 (million)
% 0.89/0.37 % (2564185)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1530316172: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.89/0.37 % (2564189)lrs+10_1_si=on:cs=on:random_seed=156349363:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.89/0.37 % (2564191)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.89/0.39 % (2564189)Instruction limit reached!
% 0.89/0.39 % (2564189)------------------------------
% 0.89/0.39 % (2564189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.39 % (2564189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.39 % (2564189)CaDiCaL version: 2.1.3
% 0.89/0.39 % (2564189)Termination reason: Instruction limit
% 0.89/0.39 % (2564189)Termination phase: Saturation
% 0.89/0.39 % (2564189)Time elapsed: 0.004 s
% 0.89/0.39 % (2564189)Peak memory usage: 11 MB
% 0.89/0.39 % (2564189)Instructions burned: 8 (million)
% 0.89/0.39 % (2564185)Instruction limit reached!
% 0.89/0.39 % (2564185)------------------------------
% 0.89/0.39 % (2564185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.39 % (2564185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.39 % (2564185)CaDiCaL version: 2.1.3
% 0.89/0.39 % (2564185)Termination reason: Instruction limit
% 0.89/0.39 % (2564185)Termination phase: Saturation
% 0.89/0.39 % (2564185)Time elapsed: 0.013 s
% 0.89/0.39 % (2564185)Peak memory usage: 11 MB
% 0.89/0.39 % (2564185)Instructions burned: 28 (million)
% 0.89/0.39 % (2564191)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=3950139689:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.89/0.39 % (2564191)Instruction limit reached!
% 0.89/0.39 % (2564191)------------------------------
% 0.89/0.39 % (2564191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.39 % (2564191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.39 % (2564191)CaDiCaL version: 2.1.3
% 0.89/0.39 % (2564191)Termination reason: Instruction limit
% 0.89/0.39 % (2564191)Termination phase: Property scanning
% 0.89/0.39 % (2564191)Time elapsed: 0.001 s
% 0.89/0.39 % (2564191)Peak memory usage: 9 MB
% 0.89/0.39 % (2564191)Instructions burned: 2 (million)
% 0.89/0.39 % (2564193)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1711178394:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.89/0.39 % (2564188)Instruction limit reached!
% 0.89/0.39 % (2564188)------------------------------
% 0.89/0.39 % (2564188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.39 % (2564188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.39 % (2564188)CaDiCaL version: 2.1.3
% 0.89/0.39 % (2564188)Termination reason: Instruction limit
% 0.89/0.39 % (2564188)Termination phase: Saturation
% 0.89/0.39 % (2564188)Time elapsed: 0.023 s
% 0.89/0.39 % (2564188)Peak memory usage: 12 MB
% 0.89/0.39 % (2564188)Instructions burned: 88 (million)
% 0.89/0.39 % (2564193)Refutation not found, incomplete strategy
% 0.89/0.39 % (2564193)------------------------------
% 0.89/0.39 % (2564193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.39 % (2564193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.39 % (2564193)CaDiCaL version: 2.1.3
% 0.89/0.39 % (2564193)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.39 % (2564193)Time elapsed: 0.008 s
% 0.89/0.39 % (2564193)Peak memory usage: 12 MB
% 0.89/0.39 % (2564193)Instructions burned: 15 (million)
% 0.89/0.39 % (2564193)------------------------------
% 0.89/0.39 % (2564193)------------------------------
% 0.89/0.39 % (2564198)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=365486060:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.89/0.39 % (2564196)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3625573234:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.89/0.39 % (2564199)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2752197988:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.89/0.39 % (2564201)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3969274704:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.89/0.39 % (2564172)Instruction limit reached!
% 0.89/0.39 % (2564172)------------------------------
% 0.89/0.39 % (2564172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564172)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564172)Termination reason: Instruction limit
% 0.89/0.44 % (2564172)Termination phase: Saturation
% 0.89/0.44 % (2564172)Time elapsed: 0.081 s
% 0.89/0.44 % (2564172)Peak memory usage: 13 MB
% 0.89/0.44 % (2564172)Instructions burned: 157 (million)
% 0.89/0.44 % (2564199)Instruction limit reached!
% 0.89/0.44 % (2564199)------------------------------
% 0.89/0.44 % (2564199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564199)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564199)Termination reason: Instruction limit
% 0.89/0.44 % (2564199)Termination phase: Saturation
% 0.89/0.44 % (2564199)Time elapsed: 0.007 s
% 0.89/0.44 % (2564199)Peak memory usage: 11 MB
% 0.89/0.44 % (2564199)Instructions burned: 15 (million)
% 0.89/0.44 % (2564202)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2403243642:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.89/0.44 % (2564198)Instruction limit reached!
% 0.89/0.44 % (2564198)------------------------------
% 0.89/0.44 % (2564198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564198)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564198)Termination reason: Instruction limit
% 0.89/0.44 % (2564198)Termination phase: Saturation
% 0.89/0.44 % (2564198)Time elapsed: 0.014 s
% 0.89/0.44 % (2564198)Peak memory usage: 12 MB
% 0.89/0.44 % (2564198)Instructions burned: 26 (million)
% 0.89/0.44 % (2564196)Refutation not found, incomplete strategy
% 0.89/0.44 % (2564196)------------------------------
% 0.89/0.44 % (2564196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564196)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564196)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.44 % (2564196)Time elapsed: 0.019 s
% 0.89/0.44 % (2564196)Peak memory usage: 12 MB
% 0.89/0.44 % (2564196)Instructions burned: 28 (million)
% 0.89/0.44 % (2564196)------------------------------
% 0.89/0.44 % (2564196)------------------------------
% 0.89/0.44 % (2564202)Instruction limit reached!
% 0.89/0.44 % (2564202)------------------------------
% 0.89/0.44 % (2564202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564202)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564202)Termination reason: Instruction limit
% 0.89/0.44 % (2564202)Termination phase: Saturation
% 0.89/0.44 % (2564202)Time elapsed: 0.007 s
% 0.89/0.44 % (2564202)Peak memory usage: 12 MB
% 0.89/0.44 % (2564202)Instructions burned: 14 (million)
% 0.89/0.44 % (2564201)Refutation not found, incomplete strategy
% 0.89/0.44 % (2564201)------------------------------
% 0.89/0.44 % (2564201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564201)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564201)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.44 % (2564201)Time elapsed: 0.022 s
% 0.89/0.44 % (2564201)Peak memory usage: 12 MB
% 0.89/0.44 % (2564201)Instructions burned: 74 (million)
% 0.89/0.44 % (2564201)------------------------------
% 0.89/0.44 % (2564201)------------------------------
% 0.89/0.44 % (2564207)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=642648077: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.89/0.44 % (2564208)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3312193561:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.89/0.44 % (2564207)Instruction limit reached!
% 0.89/0.44 % (2564207)------------------------------
% 0.89/0.44 % (2564207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (2564207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (2564207)CaDiCaL version: 2.1.3
% 0.89/0.44 % (2564207)Termination reason: Instruction limit
% 0.89/0.44 % (2564207)Termination phase: Property scanning
% 0.89/0.46 % (2564207)Time elapsed: 0.002 s
% 0.89/0.46 % (2564207)Peak memory usage: 10 MB
% 0.89/0.46 % (2564207)Instructions burned: 3 (million)
% 0.89/0.46 % (2564210)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1375837743:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.89/0.46 % (2564213)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.89/0.46 % (2564213)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=973892653:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.89/0.46 % (2564212)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) 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.89/0.46 % (2564212)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.89/0.46 % (2564213)Instruction limit reached!
% 0.89/0.46 % (2564213)------------------------------
% 0.89/0.46 % (2564213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564213)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564213)Termination reason: Instruction limit
% 0.89/0.46 % (2564213)Termination phase: Saturation
% 0.89/0.46 % (2564213)Time elapsed: 0.003 s
% 0.89/0.46 % (2564213)Peak memory usage: 11 MB
% 0.89/0.46 % (2564213)Instructions burned: 12 (million)
% 0.89/0.46 % (2564211)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1356788156:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.89/0.46 % (2564212)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=1505451163:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.89/0.46 % (2564208)Instruction limit reached!
% 0.89/0.46 % (2564208)------------------------------
% 0.89/0.46 % (2564208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564208)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564208)Termination reason: Instruction limit
% 0.89/0.46 % (2564208)Termination phase: Saturation
% 0.89/0.46 % (2564208)Time elapsed: 0.013 s
% 0.89/0.46 % (2564208)Peak memory usage: 12 MB
% 0.89/0.46 % (2564208)Instructions burned: 26 (million)
% 0.89/0.46 % (2564210)Instruction limit reached!
% 0.89/0.46 % (2564210)------------------------------
% 0.89/0.46 % (2564210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564210)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564210)Termination reason: Instruction limit
% 0.89/0.46 % (2564210)Termination phase: Saturation
% 0.89/0.46 % (2564210)Time elapsed: 0.012 s
% 0.89/0.46 % (2564210)Peak memory usage: 12 MB
% 0.89/0.46 % (2564210)Instructions burned: 24 (million)
% 0.89/0.46 % (2564216)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2651861841:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.89/0.46 % (2564212)Instruction limit reached!
% 0.89/0.46 % (2564212)------------------------------
% 0.89/0.46 % (2564212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564212)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564212)Termination reason: Instruction limit
% 0.89/0.46 % (2564212)Termination phase: Saturation
% 0.89/0.46 % (2564212)Time elapsed: 0.007 s
% 0.89/0.46 % (2564212)Peak memory usage: 12 MB
% 0.89/0.46 % (2564212)Instructions burned: 15 (million)
% 0.89/0.46 % (2564219)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=561013850:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.89/0.46 % (2564219)Instruction limit reached!
% 0.89/0.46 % (2564219)------------------------------
% 0.89/0.46 % (2564219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564219)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564219)Termination reason: Instruction limit
% 0.89/0.46 % (2564219)Termination phase: Saturation
% 0.89/0.46 % (2564219)Time elapsed: 0.002 s
% 0.89/0.46 % (2564219)Peak memory usage: 11 MB
% 0.89/0.46 % (2564219)Instructions burned: 8 (million)
% 0.89/0.46 % (2564222)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=15782281:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.89/0.46 % (2564227)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2714012475:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 0.89/0.46 % (2564216)Instruction limit reached!
% 0.89/0.46 % (2564216)------------------------------
% 0.89/0.46 % (2564216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564216)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564216)Termination reason: Instruction limit
% 0.89/0.46 % (2564216)Termination phase: Saturation
% 0.89/0.46 % (2564216)Time elapsed: 0.016 s
% 0.89/0.46 % (2564216)Peak memory usage: 12 MB
% 0.89/0.46 % (2564216)Instructions burned: 31 (million)
% 0.89/0.46 % (2564223)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=602490749:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 0.89/0.46 % (2564225)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3828476989:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 0.89/0.46 % (2564222)Instruction limit reached!
% 0.89/0.46 % (2564222)------------------------------
% 0.89/0.46 % (2564222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564222)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564222)Termination reason: Instruction limit
% 0.89/0.46 % (2564222)Termination phase: Saturation
% 0.89/0.46 % (2564222)Time elapsed: 0.010 s
% 0.89/0.46 % (2564222)Peak memory usage: 11 MB
% 0.89/0.46 % (2564222)Instructions burned: 24 (million)
% 0.89/0.46 % (2564211)Instruction limit reached!
% 0.89/0.46 % (2564211)------------------------------
% 0.89/0.46 % (2564211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564211)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564211)Termination reason: Instruction limit
% 0.89/0.46 % (2564211)Termination phase: Saturation
% 0.89/0.46 % (2564211)Time elapsed: 0.032 s
% 0.89/0.46 % (2564211)Peak memory usage: 12 MB
% 0.89/0.46 % (2564211)Instructions burned: 60 (million)
% 0.89/0.46 % (2564223)Instruction limit reached!
% 0.89/0.46 % (2564223)------------------------------
% 0.89/0.46 % (2564223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564223)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564223)Termination reason: Instruction limit
% 0.89/0.46 % (2564223)Termination phase: Saturation
% 0.89/0.46 % (2564223)Time elapsed: 0.010 s
% 0.89/0.46 % (2564223)Peak memory usage: 12 MB
% 0.89/0.46 % (2564223)Instructions burned: 21 (million)
% 0.89/0.46 % (2564230)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3909662256:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 0.89/0.46 % (2564234)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.46 % (2564233)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1125443286:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 0.89/0.46 % (2564234)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3383487158:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 0.89/0.46 % (2564235)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3192515035:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 0.89/0.46 % (2564234)Instruction limit reached!
% 0.89/0.46 % (2564234)------------------------------
% 0.89/0.46 % (2564234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564234)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564234)Termination reason: Instruction limit
% 0.89/0.46 % (2564234)Termination phase: Saturation
% 0.89/0.46 % (2564234)Time elapsed: 0.004 s
% 0.89/0.46 % (2564234)Peak memory usage: 11 MB
% 0.89/0.46 % (2564234)Instructions burned: 7 (million)
% 0.89/0.46 % (2564230)Refutation not found, incomplete strategy
% 0.89/0.46 % (2564230)------------------------------
% 0.89/0.46 % (2564230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564230)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564230)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.46 % (2564230)Time elapsed: 0.016 s
% 0.89/0.46 % (2564230)Peak memory usage: 12 MB
% 0.89/0.46 % (2564230)Instructions burned: 30 (million)
% 0.89/0.46 % (2564230)------------------------------
% 0.89/0.46 % (2564230)------------------------------
% 0.89/0.46 % (2564169) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2564161-2564169"...
% 0.89/0.46 % (2564227)Instruction limit reached!
% 0.89/0.46 % (2564227)------------------------------
% 0.89/0.46 % (2564227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564227)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564227)Termination reason: Instruction limit
% 0.89/0.46 % (2564227)Termination phase: Saturation
% 0.89/0.46 % (2564227)Time elapsed: 0.037 s
% 0.89/0.46 % (2564227)Peak memory usage: 13 MB
% 0.89/0.46 % (2564227)Instructions burned: 146 (million)
% 0.89/0.46 % (2564242)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2500646637:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 0.89/0.46 % (2564233)Instruction limit reached!
% 0.89/0.46 % (2564233)------------------------------
% 0.89/0.46 % (2564233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.46 % (2564233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.46 % (2564233)CaDiCaL version: 2.1.3
% 0.89/0.46 % (2564233)Termination reason: Instruction limit
% 0.89/0.46 % (2564233)Termination phase: Saturation
% 0.89/0.46 % (2564233)Time elapsed: 0.021 s
% 0.89/0.46 % (2564233)Peak memory usage: 12 MB
% 0.89/0.46 % (2564233)Instructions burned: 42 (million)
% 0.89/0.46 % (2564169)...printing done.
% 0.89/0.46 % (2564240)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=3255920201:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 0.89/0.46 % (2564241)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 0.89/0.46 % (2564169)Refutation found. Thanks to Tanya!
% 0.89/0.46 % SZS status Theorem for theBenchmark
% 0.89/0.46 % SZS output start Proof for theBenchmark
% 0.89/0.46 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.89/0.46 thf(func_def_0, type, in: ($i > $i > $o)).
% 0.89/0.46 thf(func_def_2, type, setadjoin: ($i > $i > $i)).
% 0.89/0.46 thf(func_def_3, type, dsetconstr: ($i > ($i > $o) > $i)).
% 0.89/0.46 thf(func_def_4, type, subset: ($i > $i > $o)).
% 0.89/0.46 thf(func_def_5, type, kpair: ($i > $i > $i)).
% 0.89/0.46 thf(func_def_6, type, cartprod: ($i > $i > $i)).
% 0.89/0.46 thf(func_def_7, type, singleton: ($i > $o)).
% 0.89/0.46 thf(func_def_9, type, ex1: ($i > ($i > $o) > $o)).
% 0.89/0.46 thf(func_def_10, type, breln: ($i > $i > $i > $o)).
% 0.89/0.46 thf(func_def_11, type, func: ($i > $i > $i > $o)).
% 0.89/0.46 thf(func_def_12, type, ap: ($i > $i > $i > $i > $i)).
% 0.89/0.46 thf(func_def_13, type, funcGraphProp1: $o).
% 0.89/0.46 thf(func_def_14, type, funcGraphProp2: $o).
% 0.89/0.46 thf(func_def_15, type, eqbreln: $o).
% 0.89/0.46 thf(func_def_18, type, db0: !>[X0: $tType]:(X0)).
% 0.89/0.46 thf(func_def_19, type, db2: !>[X0: $tType]:(X0)).
% 0.89/0.46 thf(func_def_20, type, db1: !>[X0: $tType]:(X0)).
% 0.89/0.46 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.89/0.46 thf(func_def_22, type, vAND: ($o > $o > $o)).
% 0.89/0.46 thf(func_def_23, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.89/0.46 thf(func_def_24, type, vIMP: ($o > $o > $o)).
% 0.89/0.46 thf(func_def_25, type, db3: !>[X0: $tType]:(X0)).
% 0.89/0.46 thf(func_def_26, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.89/0.46 thf(func_def_27, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.89/0.46 thf(func_def_28, type, sP0: $o).
% 0.89/0.46 thf(func_def_33, type, sK5: ($i > $i > $i > $i > $i)).
% 0.89/0.46 thf(func_def_34, type, sK6: ($i > $i > $i > $i > $i)).
% 0.89/0.46 thf(func_def_35, type, sK7: ($i > $i > $i > $i > $i)).
% 0.89/0.46 thf(func_def_36, type, sK8: ($i > $i > $i > $i > $i)).
% 0.89/0.46 thf(func_def_51, type, sK23: ($i > $i)).
% 0.89/0.46 thf(func_def_52, type, sK24: ($i > $i > $i > $i)).
% 0.89/0.46 thf(f4,axiom,(
% 0.89/0.46 ((^[X0 : $i, X1 : $i, X2 : $i] : ((breln @ X0 @ X1 @ X2) & ! [X3 : $i] : ((in @ X3 @ X0) => (ex1 @ X1 @ (^[X4 : $i] : ((in @ (kpair @ X3 @ X4) @ X2))))))) = func)),
% 0.89/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',func)).
% 0.89/0.46 thf(f5,axiom,(
% 0.89/0.46 (funcGraphProp1 = ! [X1 : $i,X0 : $i,X2 : $i] : ((func @ X0 @ X1 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => (in @ (kpair @ X3 @ (ap @ X0 @ X1 @ X2 @ X3)) @ X2))))),
% 0.89/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',funcGraphProp1)).
% 0.89/0.46 thf(f6,axiom,(
% 0.89/0.46 (! [X0 : $i,X2 : $i,X1 : $i] : ((func @ X0 @ X1 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X1) => ((in @ (kpair @ X3 @ X4) @ X2) => (((ap @ X0 @ X1 @ X2 @ X3)) = X4))))) = funcGraphProp2)),
% 0.89/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',funcGraphProp2)).
% 0.89/0.46 thf(f7,axiom,(
% 0.89/0.46 (eqbreln = ! [X1 : $i,X0 : $i,X2 : $i] : ((breln @ X0 @ X1 @ X2) => ! [X3 : $i] : ((breln @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((in @ (kpair @ X4 @ X5) @ X2) => (in @ (kpair @ X4 @ X5) @ X3)))) => (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((in @ (kpair @ X4 @ X5) @ X3) => (in @ (kpair @ X4 @ X5) @ X2)))) => (X2 = X3))))))),
% 0.89/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',eqbreln)).
% 0.89/0.46 thf(f8,conjecture,(
% 0.89/0.46 funcGraphProp1 => (funcGraphProp2 => (eqbreln => ! [X0 : $i,X1 : $i,X2 : $i] : ((func @ X0 @ X1 @ X2) => ! [X3 : $i] : ((func @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4)))) => (X2 = X3))))))),
% 0.89/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',funcext)).
% 0.89/0.46 thf(f9,negated_conjecture,(
% 0.89/0.46 ~(funcGraphProp1 => (funcGraphProp2 => (eqbreln => ! [X0 : $i,X1 : $i,X2 : $i] : ((func @ X0 @ X1 @ X2) => ! [X3 : $i] : ((func @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4)))) => (X2 = X3)))))))),
% 0.89/0.46 inference(negated_conjecture,[status(cth)],[f8])).
% 0.89/0.46 thf(f10,plain,(
% 0.89/0.46 (! [X0 : $i,X1 : $i,X2 : $i] : ((func @ X0 @ X2 @ X1) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X2) => ((in @ (kpair @ X3 @ X4) @ X1) => (((ap @ X0 @ X2 @ X1 @ X3)) = X4))))) = funcGraphProp2)),
% 0.89/0.46 inference(rectify,[],[f6])).
% 0.89/0.46 thf(f11,plain,(
% 0.89/0.46 (funcGraphProp2 = $true) <=> ! [X0 : $i,X1 : $i,X2 : $i] : ((((func @ X0 @ X2 @ X1)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ! [X4 : $i] : (($true = ((in @ X4 @ X2))) => (($true = ((in @ (kpair @ X3 @ X4) @ X1))) => (((ap @ X0 @ X2 @ X1 @ X3)) = X4)))))),
% 0.89/0.46 inference(fool_elimination,[],[f10])).
% 0.89/0.46 thf(f13,plain,(
% 0.89/0.46 ((^[X0 : $i, X1 : $i, X2 : $i] : ((breln @ X0 @ X1 @ X2) & ! [X3 : $i] : ((in @ X3 @ X0) => (ex1 @ X1 @ (^[X4 : $i] : ((in @ (kpair @ X3 @ X4) @ X2))))))) = func)),
% 0.89/0.46 inference(rectify,[],[f4])).
% 0.89/0.46 thf(f14,plain,(
% 0.89/0.46 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))) & (breln @ Y0 @ Y1 @ Y2))))))))),
% 0.89/0.46 inference(fool_elimination,[],[f13])).
% 0.89/0.46 thf(f17,plain,(
% 0.89/0.46 (eqbreln = ! [X0 : $i,X1 : $i,X2 : $i] : ((breln @ X1 @ X0 @ X2) => ! [X3 : $i] : ((breln @ X1 @ X0 @ X3) => (! [X4 : $i] : ((in @ X4 @ X1) => ! [X5 : $i] : ((in @ X5 @ X0) => ((in @ (kpair @ X4 @ X5) @ X2) => (in @ (kpair @ X4 @ X5) @ X3)))) => (! [X6 : $i] : ((in @ X6 @ X1) => ! [X7 : $i] : ((in @ X7 @ X0) => ((in @ (kpair @ X6 @ X7) @ X3) => (in @ (kpair @ X6 @ X7) @ X2)))) => (X2 = X3))))))),
% 0.89/0.46 inference(rectify,[],[f7])).
% 0.89/0.46 thf(f18,plain,(
% 0.89/0.46 ! [X2 : $i,X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ X2)) = $true) => ! [X3 : $i] : ((((breln @ X1 @ X0 @ X3)) = $true) => (! [X4 : $i] : ((((in @ X4 @ X1)) = $true) => ! [X5 : $i] : ((((in @ X5 @ X0)) = $true) => ((((in @ (kpair @ X4 @ X5) @ X2)) = $true) => (((in @ (kpair @ X4 @ X5) @ X3)) = $true)))) => (! [X6 : $i] : ((((in @ X6 @ X1)) = $true) => ! [X7 : $i] : ((((in @ X7 @ X0)) = $true) => ((((in @ (kpair @ X6 @ X7) @ X3)) = $true) => (((in @ (kpair @ X6 @ X7) @ X2)) = $true)))) => (X2 = X3))))) <=> (eqbreln = $true)),
% 0.89/0.46 inference(fool_elimination,[],[f17])).
% 0.89/0.46 thf(f21,plain,(
% 0.89/0.46 ~(funcGraphProp1 => (funcGraphProp2 => (eqbreln => ! [X0 : $i,X1 : $i,X2 : $i] : ((func @ X0 @ X1 @ X2) => ! [X3 : $i] : ((func @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4)))) => (X2 = X3)))))))),
% 0.89/0.46 inference(rectify,[],[f9])).
% 0.89/0.46 thf(f22,plain,(
% 0.89/0.46 ~((funcGraphProp1 = $true) => ((funcGraphProp2 = $true) => ((eqbreln = $true) => ! [X1 : $i,X0 : $i,X2 : $i] : ((((func @ X0 @ X1 @ X2)) = $true) => ! [X3 : $i] : ((((func @ X0 @ X1 @ X3)) = $true) => (! [X4 : $i] : ((((in @ X4 @ X0)) = $true) => (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4)))) => (X2 = X3)))))))),
% 0.89/0.46 inference(fool_elimination,[],[f21])).
% 0.89/0.46 thf(f23,plain,(
% 0.89/0.46 (funcGraphProp1 = ! [X0 : $i,X1 : $i,X2 : $i] : ((func @ X1 @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X1) => (in @ (kpair @ X3 @ (ap @ X1 @ X0 @ X2 @ X3)) @ X2))))),
% 0.89/0.46 inference(rectify,[],[f5])).
% 0.89/0.46 thf(f24,plain,(
% 0.89/0.46 (funcGraphProp1 = $true) <=> ! [X1 : $i,X2 : $i,X0 : $i] : ((((func @ X1 @ X0 @ X2)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X1)) = $true) => (((in @ (kpair @ X3 @ (ap @ X1 @ X0 @ X2 @ X3)) @ X2)) = $true)))),
% 0.89/0.46 inference(fool_elimination,[],[f23])).
% 0.89/0.46 thf(f25,plain,(
% 0.89/0.46 ((? [X1 : $i,X0 : $i,X2 : $i] : (? [X3 : $i] : (((X2 != X3) & ! [X4 : $i] : ((((in @ X4 @ X0)) != $true) | (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4))))) & (((func @ X0 @ X1 @ X3)) = $true)) & (((func @ X0 @ X1 @ X2)) = $true)) & (eqbreln = $true)) & (funcGraphProp2 = $true)) & (funcGraphProp1 = $true)),
% 0.89/0.46 inference(ennf_transformation,[],[f22])).
% 0.89/0.46 thf(f26,plain,(
% 0.89/0.46 ? [X0 : $i,X1 : $i,X2 : $i] : (? [X3 : $i] : ((((func @ X0 @ X1 @ X3)) = $true) & (X2 != X3) & ! [X4 : $i] : ((((in @ X4 @ X0)) != $true) | (((ap @ X0 @ X1 @ X2 @ X4)) = ((ap @ X0 @ X1 @ X3 @ X4))))) & (((func @ X0 @ X1 @ X2)) = $true)) & (funcGraphProp2 = $true) & (eqbreln = $true) & (funcGraphProp1 = $true)),
% 0.89/0.46 inference(flattening,[],[f25])).
% 0.89/0.46 thf(f27,plain,(
% 0.89/0.46 ! [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X1 @ X0 @ X2)) != $true) | ! [X3 : $i] : ((((in @ (kpair @ X3 @ (ap @ X1 @ X0 @ X2 @ X3)) @ X2)) = $true) | (((in @ X3 @ X1)) != $true))) <=> (funcGraphProp1 = $true)),
% 0.89/0.46 inference(ennf_transformation,[],[f24])).
% 0.89/0.46 thf(f28,plain,(
% 0.89/0.46 (funcGraphProp2 = $true) <=> ! [X0 : $i,X1 : $i,X2 : $i] : (! [X3 : $i] : (! [X4 : $i] : (((((ap @ X0 @ X2 @ X1 @ X3)) = X4) | ($true != ((in @ (kpair @ X3 @ X4) @ X1)))) | ($true != ((in @ X4 @ X2)))) | (((in @ X3 @ X0)) != $true)) | (((func @ X0 @ X2 @ X1)) != $true))),
% 0.89/0.46 inference(ennf_transformation,[],[f11])).
% 0.89/0.46 thf(f29,plain,(
% 0.89/0.46 (funcGraphProp2 = $true) <=> ! [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X0 @ X2 @ X1)) != $true) | ! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | ! [X4 : $i] : (($true != ((in @ (kpair @ X3 @ X4) @ X1))) | (((ap @ X0 @ X2 @ X1 @ X3)) = X4) | ($true != ((in @ X4 @ X2))))))),
% 0.89/0.46 inference(flattening,[],[f28])).
% 0.89/0.46 thf(f30,plain,(
% 0.89/0.46 ! [X2 : $i,X0 : $i,X1 : $i] : (! [X3 : $i] : ((((X2 = X3) | ? [X6 : $i] : (? [X7 : $i] : (((((in @ (kpair @ X6 @ X7) @ X2)) != $true) & (((in @ (kpair @ X6 @ X7) @ X3)) = $true)) & (((in @ X7 @ X0)) = $true)) & (((in @ X6 @ X1)) = $true))) | ? [X4 : $i] : (? [X5 : $i] : (((((in @ (kpair @ X4 @ X5) @ X3)) != $true) & (((in @ (kpair @ X4 @ X5) @ X2)) = $true)) & (((in @ X5 @ X0)) = $true)) & (((in @ X4 @ X1)) = $true))) | (((breln @ X1 @ X0 @ X3)) != $true)) | (((breln @ X1 @ X0 @ X2)) != $true)) <=> (eqbreln = $true)),
% 0.89/0.46 inference(ennf_transformation,[],[f18])).
% 0.89/0.46 thf(f31,plain,(
% 0.89/0.46 ! [X1 : $i,X0 : $i,X2 : $i] : (! [X3 : $i] : ((X2 = X3) | (((breln @ X1 @ X0 @ X3)) != $true) | ? [X6 : $i] : (? [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ X3)) = $true) & (((in @ (kpair @ X6 @ X7) @ X2)) != $true) & (((in @ X7 @ X0)) = $true)) & (((in @ X6 @ X1)) = $true)) | ? [X4 : $i] : ((((in @ X4 @ X1)) = $true) & ? [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ X3)) != $true) & (((in @ X5 @ X0)) = $true) & (((in @ (kpair @ X4 @ X5) @ X2)) = $true)))) | (((breln @ X1 @ X0 @ X2)) != $true)) <=> (eqbreln = $true)),
% 0.89/0.46 inference(flattening,[],[f30])).
% 0.89/0.46 thf(f32,definition,(
% 0.89/0.46 (sP0 = $true) <=> ! [X1 : $i,X0 : $i,X2 : $i] : (! [X3 : $i] : ((X2 = X3) | (((breln @ X1 @ X0 @ X3)) != $true) | ? [X6 : $i] : (? [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ X3)) = $true) & (((in @ (kpair @ X6 @ X7) @ X2)) != $true) & (((in @ X7 @ X0)) = $true)) & (((in @ X6 @ X1)) = $true)) | ? [X4 : $i] : ((((in @ X4 @ X1)) = $true) & ? [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ X3)) != $true) & (((in @ X5 @ X0)) = $true) & (((in @ (kpair @ X4 @ X5) @ X2)) = $true)))) | (((breln @ X1 @ X0 @ X2)) != $true))),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.89/0.46 thf(f33,plain,(
% 0.89/0.46 (sP0 = $true) <=> (eqbreln = $true)),
% 0.89/0.46 inference(definition_folding,[],[f31,f32])).
% 0.89/0.46 thf(f34,plain,(
% 0.89/0.46 ((sP0 = $true) | ? [X1 : $i,X0 : $i,X2 : $i] : (? [X3 : $i] : ((X2 != X3) & (((breln @ X1 @ X0 @ X3)) = $true) & ! [X6 : $i] : (! [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ X3)) != $true) | (((in @ (kpair @ X6 @ X7) @ X2)) = $true) | (((in @ X7 @ X0)) != $true)) | (((in @ X6 @ X1)) != $true)) & ! [X4 : $i] : ((((in @ X4 @ X1)) != $true) | ! [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ X3)) = $true) | (((in @ X5 @ X0)) != $true) | (((in @ (kpair @ X4 @ X5) @ X2)) != $true)))) & (((breln @ X1 @ X0 @ X2)) = $true))) & (! [X1 : $i,X0 : $i,X2 : $i] : (! [X3 : $i] : ((X2 = X3) | (((breln @ X1 @ X0 @ X3)) != $true) | ? [X6 : $i] : (? [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ X3)) = $true) & (((in @ (kpair @ X6 @ X7) @ X2)) != $true) & (((in @ X7 @ X0)) = $true)) & (((in @ X6 @ X1)) = $true)) | ? [X4 : $i] : ((((in @ X4 @ X1)) = $true) & ? [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ X3)) != $true) & (((in @ X5 @ X0)) = $true) & (((in @ (kpair @ X4 @ X5) @ X2)) = $true)))) | (((breln @ X1 @ X0 @ X2)) != $true)) | (sP0 != $true))),
% 0.89/0.46 inference(nnf_transformation,[],[f32])).
% 0.89/0.46 thf(f35,plain,(
% 0.89/0.46 ((sP0 = $true) | ? [X0 : $i,X1 : $i,X2 : $i] : (? [X3 : $i] : ((X2 != X3) & (((breln @ X0 @ X1 @ X3)) = $true) & ! [X4 : $i] : (! [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ X3)) != $true) | (((in @ (kpair @ X4 @ X5) @ X2)) = $true) | (((in @ X5 @ X1)) != $true)) | (((in @ X4 @ X0)) != $true)) & ! [X6 : $i] : ((((in @ X6 @ X0)) != $true) | ! [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ X3)) = $true) | ($true != ((in @ X7 @ X1))) | (((in @ (kpair @ X6 @ X7) @ X2)) != $true)))) & (((breln @ X0 @ X1 @ X2)) = $true))) & (! [X8 : $i,X9 : $i,X10 : $i] : (! [X11 : $i] : ((X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | ? [X12 : $i] : (? [X13 : $i] : ((((in @ (kpair @ X12 @ X13) @ X11)) = $true) & (((in @ (kpair @ X12 @ X13) @ X10)) != $true) & (((in @ X13 @ X9)) = $true)) & (((in @ X12 @ X8)) = $true)) | ? [X14 : $i] : ((((in @ X14 @ X8)) = $true) & ? [X15 : $i] : ((((in @ (kpair @ X14 @ X15) @ X11)) != $true) & (((in @ X15 @ X9)) = $true) & (((in @ (kpair @ X14 @ X15) @ X10)) = $true)))) | (((breln @ X8 @ X9 @ X10)) != $true)) | (sP0 != $true))),
% 0.89/0.46 inference(rectify,[],[f34])).
% 0.89/0.46 thf(f36,plain,(
% 0.89/0.46 ((sP0 = $true) | (((sK4 != sK3) & (((breln @ sK1 @ sK2 @ sK4)) = $true) & ! [X4 : $i] : (! [X5 : $i] : ((((in @ (kpair @ X4 @ X5) @ sK4)) != $true) | (((in @ (kpair @ X4 @ X5) @ sK3)) = $true) | (((in @ X5 @ sK2)) != $true)) | (((in @ X4 @ sK1)) != $true)) & ! [X6 : $i] : ((((in @ X6 @ sK1)) != $true) | ! [X7 : $i] : ((((in @ (kpair @ X6 @ X7) @ sK4)) = $true) | (((in @ X7 @ sK2)) != $true) | (((in @ (kpair @ X6 @ X7) @ sK3)) != $true)))) & (((breln @ sK1 @ sK2 @ sK3)) = $true))) & (! [X8 : $i,X9 : $i,X10 : $i] : (! [X11 : $i] : ((X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | ((($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) & (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) & (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true)) & ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8)))) | (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) & ((((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) & ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) & ($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10)))))) | (((breln @ X8 @ X9 @ X10)) != $true)) | (sP0 != $true))),
% 0.89/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,vAPP,vAPP,vAPP,vAPP]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X15,sK8 @ X11 @ X10 @ X9 @ X8),skolemize(X15,sK8 @ X11 @ X10 @ X9 @ X8),skolemize(X15,sK8 @ X11 @ X10 @ X9 @ X8),skolemize(X15,sK8 @ X11 @ X10 @ X9 @ X8)],[f35])).
% 0.89/0.46 thf(f37,plain,(
% 0.89/0.46 ((sP0 = $true) | (eqbreln != $true)) & ((eqbreln = $true) | (sP0 != $true))),
% 0.89/0.46 inference(nnf_transformation,[],[f33])).
% 0.89/0.46 thf(f38,plain,(
% 0.89/0.46 (((((func @ sK9 @ sK10 @ sK12)) = $true) & (sK11 != sK12) & ! [X4 : $i] : ((((in @ X4 @ sK9)) != $true) | (((ap @ sK9 @ sK10 @ sK11 @ X4)) = ((ap @ sK9 @ sK10 @ sK12 @ X4))))) & (((func @ sK9 @ sK10 @ sK11)) = $true)) & (funcGraphProp2 = $true) & (eqbreln = $true) & (funcGraphProp1 = $true)),
% 0.89/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK12]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11),skolemize(X3,sK12)],[f26])).
% 0.89/0.46 thf(f39,plain,(
% 0.89/0.46 (! [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X1 @ X0 @ X2)) != $true) | ! [X3 : $i] : ((((in @ (kpair @ X3 @ (ap @ X1 @ X0 @ X2 @ X3)) @ X2)) = $true) | (((in @ X3 @ X1)) != $true))) | (funcGraphProp1 != $true)) & ((funcGraphProp1 = $true) | ? [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X1 @ X0 @ X2)) = $true) & ? [X3 : $i] : ((((in @ (kpair @ X3 @ (ap @ X1 @ X0 @ X2 @ X3)) @ X2)) != $true) & (((in @ X3 @ X1)) = $true))))),
% 0.89/0.46 inference(nnf_transformation,[],[f27])).
% 0.89/0.46 thf(f40,plain,(
% 0.89/0.46 (! [X0 : $i,X1 : $i,X2 : $i] : ((((func @ X1 @ X2 @ X0)) != $true) | ! [X3 : $i] : (($true = ((in @ (kpair @ X3 @ (ap @ X1 @ X2 @ X0 @ X3)) @ X0))) | (((in @ X3 @ X1)) != $true))) | (funcGraphProp1 != $true)) & ((funcGraphProp1 = $true) | ? [X4 : $i,X5 : $i,X6 : $i] : (($true = ((func @ X5 @ X6 @ X4))) & ? [X7 : $i] : ((((in @ (kpair @ X7 @ (ap @ X5 @ X6 @ X4 @ X7)) @ X4)) != $true) & (((in @ X7 @ X5)) = $true))))),
% 0.89/0.46 inference(rectify,[],[f39])).
% 0.89/0.46 thf(f41,plain,(
% 0.89/0.46 (! [X0 : $i,X1 : $i,X2 : $i] : ((((func @ X1 @ X2 @ X0)) != $true) | ! [X3 : $i] : (($true = ((in @ (kpair @ X3 @ (ap @ X1 @ X2 @ X0 @ X3)) @ X0))) | (((in @ X3 @ X1)) != $true))) | (funcGraphProp1 != $true)) & ((funcGraphProp1 = $true) | ((((func @ sK14 @ sK15 @ sK13)) = $true) & ((((in @ (kpair @ sK16 @ (ap @ sK14 @ sK15 @ sK13 @ sK16)) @ sK13)) != $true) & (((in @ sK16 @ sK14)) = $true))))),
% 0.89/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16]),skolemize(X4,sK13),skolemize(X5,sK14),skolemize(X6,sK15),skolemize(X7,sK16)],[f40])).
% 0.89/0.46 thf(f42,plain,(
% 0.89/0.46 ((funcGraphProp2 = $true) | ? [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X0 @ X2 @ X1)) = $true) & ? [X3 : $i] : ((((in @ X3 @ X0)) = $true) & ? [X4 : $i] : (($true = ((in @ (kpair @ X3 @ X4) @ X1))) & (((ap @ X0 @ X2 @ X1 @ X3)) != X4) & ($true = ((in @ X4 @ X2))))))) & (! [X2 : $i,X1 : $i,X0 : $i] : ((((func @ X0 @ X2 @ X1)) != $true) | ! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | ! [X4 : $i] : (($true != ((in @ (kpair @ X3 @ X4) @ X1))) | (((ap @ X0 @ X2 @ X1 @ X3)) = X4) | ($true != ((in @ X4 @ X2)))))) | (funcGraphProp2 != $true))),
% 0.89/0.46 inference(nnf_transformation,[],[f29])).
% 0.89/0.46 thf(f43,plain,(
% 0.89/0.46 ((funcGraphProp2 = $true) | ? [X0 : $i,X1 : $i,X2 : $i] : (($true = ((func @ X2 @ X0 @ X1))) & ? [X3 : $i] : (($true = ((in @ X3 @ X2))) & ? [X4 : $i] : (($true = ((in @ (kpair @ X3 @ X4) @ X1))) & (((ap @ X2 @ X0 @ X1 @ X3)) != X4) & (((in @ X4 @ X0)) = $true))))) & (! [X5 : $i,X6 : $i,X7 : $i] : (($true != ((func @ X7 @ X5 @ X6))) | ! [X8 : $i] : ((((in @ X8 @ X7)) != $true) | ! [X9 : $i] : ((((in @ (kpair @ X8 @ X9) @ X6)) != $true) | (((ap @ X7 @ X5 @ X6 @ X8)) = X9) | ($true != ((in @ X9 @ X5)))))) | (funcGraphProp2 != $true))),
% 0.89/0.46 inference(rectify,[],[f42])).
% 0.89/0.46 thf(f44,plain,(
% 0.89/0.46 ((funcGraphProp2 = $true) | ((((func @ sK19 @ sK17 @ sK18)) = $true) & ((((in @ sK20 @ sK19)) = $true) & ((((in @ (kpair @ sK20 @ sK21) @ sK18)) = $true) & (((ap @ sK19 @ sK17 @ sK18 @ sK20)) != sK21) & (((in @ sK21 @ sK17)) = $true))))) & (! [X5 : $i,X6 : $i,X7 : $i] : (($true != ((func @ X7 @ X5 @ X6))) | ! [X8 : $i] : ((((in @ X8 @ X7)) != $true) | ! [X9 : $i] : ((((in @ (kpair @ X8 @ X9) @ X6)) != $true) | (((ap @ X7 @ X5 @ X6 @ X8)) = X9) | ($true != ((in @ X9 @ X5)))))) | (funcGraphProp2 != $true))),
% 0.89/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20,sK21]),skolemize(X0,sK17),skolemize(X1,sK18),skolemize(X2,sK19),skolemize(X3,sK20),skolemize(X4,sK21)],[f43])).
% 0.89/0.46 thf(f46,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | ($true != ((breln @ X8 @ X9 @ X11))) | (sP0 != $true) | (X10 = X11)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f47,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((X10 = X11) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (sP0 != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f48,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((sP0 != $true) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f49,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (sP0 != $true) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f50,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | (sP0 != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f51,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (sP0 != $true) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f52,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (sP0 != $true) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f53,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | (sP0 != $true) | ($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f54,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((X10 = X11) | (sP0 != $true) | ($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f55,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (sP0 != $true) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f56,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((sP0 != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f57,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11))) | (sP0 != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f58,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | ($true != ((breln @ X8 @ X9 @ X11))) | (sP0 != $true) | (X10 = X11) | ($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f59,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (sP0 != $true) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (((breln @ X8 @ X9 @ X10)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f60,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (sP0 != $true) | ($true != ((breln @ X8 @ X9 @ X11)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f61,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((sP0 != $true) | ($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | ($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | ($true != ((breln @ X8 @ X9 @ X11)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f36])).
% 0.89/0.46 thf(f68,plain,(
% 0.89/0.46 (eqbreln != $true) | (sP0 = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f37])).
% 0.89/0.46 thf(f69,plain,(
% 0.89/0.46 (funcGraphProp1 = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f70,plain,(
% 0.89/0.46 (eqbreln = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f71,plain,(
% 0.89/0.46 (funcGraphProp2 = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f72,plain,(
% 0.89/0.46 (((func @ sK9 @ sK10 @ sK11)) = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f73,plain,(
% 0.89/0.46 ( ! [X4 : $i] : ((((ap @ sK9 @ sK10 @ sK11 @ X4)) = ((ap @ sK9 @ sK10 @ sK12 @ X4))) | (((in @ X4 @ sK9)) != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f74,plain,(
% 0.89/0.46 (sK11 != sK12)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f75,plain,(
% 0.89/0.46 (((func @ sK9 @ sK10 @ sK12)) = $true)),
% 0.89/0.46 inference(cnf_transformation,[],[f38])).
% 0.89/0.46 thf(f78,plain,(
% 0.89/0.46 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))) & (breln @ Y0 @ Y1 @ Y2))))))))),
% 0.89/0.46 inference(cnf_transformation,[],[f14])).
% 0.89/0.46 thf(f82,plain,(
% 0.89/0.46 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X3 @ (ap @ X1 @ X2 @ X0 @ X3)) @ X0))) | (((in @ X3 @ X1)) != $true) | (((func @ X1 @ X2 @ X0)) != $true) | (funcGraphProp1 != $true)) )),
% 0.89/0.46 inference(cnf_transformation,[],[f41])).
% 0.89/0.46 thf(f83,plain,(
% 0.89/0.46 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : ((((in @ (kpair @ X8 @ X9) @ X6)) != $true) | ($true != ((func @ X7 @ X5 @ X6))) | (((in @ X8 @ X7)) != $true) | (((ap @ X7 @ X5 @ X6 @ X8)) = X9) | (funcGraphProp2 != $true) | ($true != ((in @ X9 @ X5)))) )),
% 0.89/0.46 inference(cnf_transformation,[],[f44])).
% 0.89/0.46 thf(f92,definition,(
% 0.89/0.46 spl22_1 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (X10 = X11))),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition])).
% 0.89/0.46 thf(f93,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true)) ) | ~spl22_1),
% 0.89/0.46 inference(avatar_component_clause,[],[f92])).
% 0.89/0.46 thf(f95,definition,(
% 0.89/0.46 spl22_2 <=> (sP0 = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition])).
% 0.89/0.46 thf(f98,plain,(
% 0.89/0.46 spl22_1 | ~spl22_2),
% 0.89/0.46 inference(avatar_split_clause,[],[f56,f95,f92])).
% 0.89/0.46 thf(f104,definition,(
% 0.89/0.46 spl22_4 <=> (funcGraphProp1 = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition])).
% 0.89/0.46 thf(f118,definition,(
% 0.89/0.46 spl22_7 <=> (eqbreln = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition])).
% 0.89/0.46 thf(f121,plain,(
% 0.89/0.46 spl22_7),
% 0.89/0.46 inference(avatar_split_clause,[],[f70,f118])).
% 0.89/0.46 thf(f123,definition,(
% 0.89/0.46 spl22_8 <=> (((func @ sK9 @ sK10 @ sK12)) = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition])).
% 0.89/0.46 thf(f125,plain,(
% 0.89/0.46 (((func @ sK9 @ sK10 @ sK12)) = $true) | ~spl22_8),
% 0.89/0.46 inference(avatar_component_clause,[],[f123])).
% 0.89/0.46 thf(f126,plain,(
% 0.89/0.46 spl22_8),
% 0.89/0.46 inference(avatar_split_clause,[],[f75,f123])).
% 0.89/0.46 thf(f128,definition,(
% 0.89/0.46 spl22_9 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true))),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition])).
% 0.89/0.46 thf(f129,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (X10 = X11)) ) | ~spl22_9),
% 0.89/0.46 inference(avatar_component_clause,[],[f128])).
% 0.89/0.46 thf(f130,plain,(
% 0.89/0.46 spl22_9 | ~spl22_2),
% 0.89/0.46 inference(avatar_split_clause,[],[f61,f95,f128])).
% 0.89/0.46 thf(f132,definition,(
% 0.89/0.46 spl22_10 <=> (((func @ sK9 @ sK10 @ sK11)) = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition])).
% 0.89/0.46 thf(f134,plain,(
% 0.89/0.46 (((func @ sK9 @ sK10 @ sK11)) = $true) | ~spl22_10),
% 0.89/0.46 inference(avatar_component_clause,[],[f132])).
% 0.89/0.46 thf(f135,plain,(
% 0.89/0.46 spl22_10),
% 0.89/0.46 inference(avatar_split_clause,[],[f72,f132])).
% 0.89/0.46 thf(f137,definition,(
% 0.89/0.46 spl22_11 <=> ! [X5 : $i,X9 : $i,X7 : $i,X6 : $i,X8 : $i] : ((((in @ (kpair @ X8 @ X9) @ X6)) != $true) | ($true != ((in @ X9 @ X5))) | (((ap @ X7 @ X5 @ X6 @ X8)) = X9) | (((in @ X8 @ X7)) != $true) | ($true != ((func @ X7 @ X5 @ X6))))),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition])).
% 0.89/0.46 thf(f138,plain,(
% 0.89/0.46 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : ((((ap @ X7 @ X5 @ X6 @ X8)) = X9) | (((in @ (kpair @ X8 @ X9) @ X6)) != $true) | ($true != ((in @ X9 @ X5))) | (((in @ X8 @ X7)) != $true) | ($true != ((func @ X7 @ X5 @ X6)))) ) | ~spl22_11),
% 0.89/0.46 inference(avatar_component_clause,[],[f137])).
% 0.89/0.46 thf(f140,definition,(
% 0.89/0.46 spl22_12 <=> (funcGraphProp2 = $true)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition])).
% 0.89/0.46 thf(f143,plain,(
% 0.89/0.46 spl22_11 | ~spl22_12),
% 0.89/0.46 inference(avatar_split_clause,[],[f83,f140,f137])).
% 0.89/0.46 thf(f145,definition,(
% 0.89/0.46 spl22_13 <=> (sK11 = sK12)),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition])).
% 0.89/0.46 thf(f147,plain,(
% 0.89/0.46 (sK11 != sK12) | spl22_13),
% 0.89/0.46 inference(avatar_component_clause,[],[f145])).
% 0.89/0.46 thf(f148,plain,(
% 0.89/0.46 ~spl22_13),
% 0.89/0.46 inference(avatar_split_clause,[],[f74,f145])).
% 0.89/0.46 thf(f165,definition,(
% 0.89/0.46 spl22_17 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11))),
% 0.89/0.46 introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition])).
% 0.89/0.46 thf(f166,plain,(
% 0.89/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11)) ) | ~spl22_17),
% 0.89/0.46 inference(avatar_component_clause,[],[f165])).
% 0.89/0.46 thf(f167,plain,(
% 0.89/0.46 spl22_17 | ~spl22_2),
% 0.89/0.46 inference(avatar_split_clause,[],[f59,f95,f165])).
% 0.89/0.46 thf(f169,definition,(
% 0.89/0.46 spl22_18 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((breln @ X8 @ X9 @ X10)) != $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition])).
% 1.65/0.46 thf(f170,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (X10 = X11)) ) | ~spl22_18),
% 1.65/0.46 inference(avatar_component_clause,[],[f169])).
% 1.65/0.46 thf(f171,plain,(
% 1.65/0.46 ~spl22_2 | spl22_18),
% 1.65/0.46 inference(avatar_split_clause,[],[f46,f169,f95])).
% 1.65/0.46 thf(f173,definition,(
% 1.65/0.46 spl22_19 <=> ! [X0 : $i,X3 : $i,X2 : $i,X1 : $i] : (($true = ((in @ (kpair @ X3 @ (ap @ X1 @ X2 @ X0 @ X3)) @ X0))) | (((func @ X1 @ X2 @ X0)) != $true) | (((in @ X3 @ X1)) != $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition])).
% 1.65/0.46 thf(f174,plain,(
% 1.65/0.46 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X3 @ (ap @ X1 @ X2 @ X0 @ X3)) @ X0))) | (((func @ X1 @ X2 @ X0)) != $true) | (((in @ X3 @ X1)) != $true)) ) | ~spl22_19),
% 1.65/0.46 inference(avatar_component_clause,[],[f173])).
% 1.65/0.46 thf(f175,plain,(
% 1.65/0.46 ~spl22_4 | spl22_19),
% 1.65/0.46 inference(avatar_split_clause,[],[f82,f173,f104])).
% 1.65/0.46 thf(f176,plain,(
% 1.65/0.46 spl22_12),
% 1.65/0.46 inference(avatar_split_clause,[],[f71,f140])).
% 1.65/0.46 thf(f178,definition,(
% 1.65/0.46 spl22_20 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : ((X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | ($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition])).
% 1.65/0.46 thf(f179,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11)))) ) | ~spl22_20),
% 1.65/0.46 inference(avatar_component_clause,[],[f178])).
% 1.65/0.46 thf(f180,plain,(
% 1.65/0.46 spl22_20 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f54,f95,f178])).
% 1.65/0.46 thf(f181,plain,(
% 1.65/0.46 spl22_2 | ~spl22_7),
% 1.65/0.46 inference(avatar_split_clause,[],[f68,f118,f95])).
% 1.65/0.46 thf(f193,definition,(
% 1.65/0.46 spl22_23 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition])).
% 1.65/0.46 thf(f194,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11)))) ) | ~spl22_23),
% 1.65/0.46 inference(avatar_component_clause,[],[f193])).
% 1.65/0.46 thf(f195,plain,(
% 1.65/0.46 spl22_23 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f49,f95,f193])).
% 1.65/0.46 thf(f197,definition,(
% 1.65/0.46 spl22_24 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition])).
% 1.65/0.46 thf(f198,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | ($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true)) ) | ~spl22_24),
% 1.65/0.46 inference(avatar_component_clause,[],[f197])).
% 1.65/0.46 thf(f199,plain,(
% 1.65/0.46 ~spl22_2 | spl22_24),
% 1.65/0.46 inference(avatar_split_clause,[],[f57,f197,f95])).
% 1.65/0.46 thf(f211,definition,(
% 1.65/0.46 spl22_27 <=> (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))) & (breln @ Y0 @ Y1 @ Y2))))))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition])).
% 1.65/0.46 thf(f213,plain,(
% 1.65/0.46 (func = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))) & (breln @ Y0 @ Y1 @ Y2)))))))) | ~spl22_27),
% 1.65/0.46 inference(avatar_component_clause,[],[f211])).
% 1.65/0.46 thf(f214,plain,(
% 1.65/0.46 spl22_27),
% 1.65/0.46 inference(avatar_split_clause,[],[f78,f211])).
% 1.65/0.46 thf(f216,definition,(
% 1.65/0.46 spl22_28 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : ((X10 = X11) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition])).
% 1.65/0.46 thf(f217,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true)) ) | ~spl22_28),
% 1.65/0.46 inference(avatar_component_clause,[],[f216])).
% 1.65/0.46 thf(f218,plain,(
% 1.65/0.46 spl22_28 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f47,f95,f216])).
% 1.65/0.46 thf(f225,definition,(
% 1.65/0.46 spl22_30 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | ($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition])).
% 1.65/0.46 thf(f226,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (X10 = X11)) ) | ~spl22_30),
% 1.65/0.46 inference(avatar_component_clause,[],[f225])).
% 1.65/0.46 thf(f227,plain,(
% 1.65/0.46 spl22_30 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f60,f95,f225])).
% 1.65/0.46 thf(f233,plain,(
% 1.65/0.46 spl22_4),
% 1.65/0.46 inference(avatar_split_clause,[],[f69,f104])).
% 1.65/0.46 thf(f240,definition,(
% 1.65/0.46 spl22_33 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : ((((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8))) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition])).
% 1.65/0.46 thf(f241,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK5 @ X11 @ X10 @ X9 @ X8) @ X8)))) ) | ~spl22_33),
% 1.65/0.46 inference(avatar_component_clause,[],[f240])).
% 1.65/0.46 thf(f242,plain,(
% 1.65/0.46 ~spl22_2 | spl22_33),
% 1.65/0.46 inference(avatar_split_clause,[],[f48,f240,f95])).
% 1.65/0.46 thf(f254,definition,(
% 1.65/0.46 spl22_36 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : ((X10 = X11) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition])).
% 1.65/0.46 thf(f255,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X10)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11)))) ) | ~spl22_36),
% 1.65/0.46 inference(avatar_component_clause,[],[f254])).
% 1.65/0.46 thf(f256,plain,(
% 1.65/0.46 ~spl22_2 | spl22_36),
% 1.65/0.46 inference(avatar_split_clause,[],[f55,f254,f95])).
% 1.65/0.46 thf(f258,definition,(
% 1.65/0.46 spl22_37 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : ((X10 = X11) | ($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition])).
% 1.65/0.46 thf(f259,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK8 @ X11 @ X10 @ X9 @ X8) @ X9))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11)) ) | ~spl22_37),
% 1.65/0.46 inference(avatar_component_clause,[],[f258])).
% 1.65/0.46 thf(f260,plain,(
% 1.65/0.46 spl22_37 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f51,f95,f258])).
% 1.65/0.46 thf(f262,definition,(
% 1.65/0.46 spl22_38 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition])).
% 1.65/0.46 thf(f263,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11)) ) | ~spl22_38),
% 1.65/0.46 inference(avatar_component_clause,[],[f262])).
% 1.65/0.46 thf(f264,plain,(
% 1.65/0.46 ~spl22_2 | spl22_38),
% 1.65/0.46 inference(avatar_split_clause,[],[f50,f262,f95])).
% 1.65/0.46 thf(f266,definition,(
% 1.65/0.46 spl22_39 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition])).
% 1.65/0.46 thf(f267,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (sK7 @ X11 @ X10 @ X9 @ X8) @ X8))) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (((breln @ X8 @ X9 @ X10)) != $true) | (X10 = X11)) ) | ~spl22_39),
% 1.65/0.46 inference(avatar_component_clause,[],[f266])).
% 1.65/0.46 thf(f268,plain,(
% 1.65/0.46 ~spl22_2 | spl22_39),
% 1.65/0.46 inference(avatar_split_clause,[],[f53,f266,f95])).
% 1.65/0.46 thf(f275,definition,(
% 1.65/0.46 spl22_41 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true != ((breln @ X8 @ X9 @ X11))) | (((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | (X10 = X11))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_41])],[avatar_definition])).
% 1.65/0.46 thf(f276,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : ((((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X11)) != $true) | (((breln @ X8 @ X9 @ X10)) != $true) | (((in @ (sK6 @ X11 @ X10 @ X9 @ X8) @ X9)) = $true) | ($true != ((breln @ X8 @ X9 @ X11))) | (X10 = X11)) ) | ~spl22_41),
% 1.65/0.46 inference(avatar_component_clause,[],[f275])).
% 1.65/0.46 thf(f277,plain,(
% 1.65/0.46 spl22_41 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f52,f95,f275])).
% 1.65/0.46 thf(f279,definition,(
% 1.65/0.46 spl22_42 <=> ! [X10 : $i,X11 : $i,X9 : $i,X8 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (X10 = X11) | ($true != ((breln @ X8 @ X9 @ X11))))),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_42])],[avatar_definition])).
% 1.65/0.46 thf(f280,plain,(
% 1.65/0.46 ( ! [X10 : $i,X11 : $i,X8 : $i,X9 : $i] : (($true = ((in @ (kpair @ (sK7 @ X11 @ X10 @ X9 @ X8) @ (sK8 @ X11 @ X10 @ X9 @ X8)) @ X10))) | (((breln @ X8 @ X9 @ X10)) != $true) | ($true != ((breln @ X8 @ X9 @ X11))) | ($true = ((in @ (kpair @ (sK5 @ X11 @ X10 @ X9 @ X8) @ (sK6 @ X11 @ X10 @ X9 @ X8)) @ X11))) | (X10 = X11)) ) | ~spl22_42),
% 1.65/0.46 inference(avatar_component_clause,[],[f279])).
% 1.65/0.46 thf(f281,plain,(
% 1.65/0.46 spl22_42 | ~spl22_2),
% 1.65/0.46 inference(avatar_split_clause,[],[f58,f95,f279])).
% 1.65/0.46 thf(f285,plain,(
% 1.65/0.46 ( ! [X0 : $i] : ((((in @ (kpair @ X0 @ (ap @ sK9 @ sK10 @ sK11 @ X0)) @ sK12)) = $true) | (((in @ X0 @ sK9)) != $true) | (((in @ X0 @ sK9)) != $true) | (((func @ sK9 @ sK10 @ sK12)) != $true)) ) | ~spl22_19),
% 1.65/0.46 inference(superposition,[],[f174,f73])).
% 1.65/0.46 thf(f286,plain,(
% 1.65/0.46 ( ! [X0 : $i] : ((((in @ (kpair @ X0 @ (ap @ sK9 @ sK10 @ sK11 @ X0)) @ sK12)) = $true) | (((in @ X0 @ sK9)) != $true) | (((func @ sK9 @ sK10 @ sK12)) != $true)) ) | ~spl22_19),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f285])).
% 1.65/0.46 thf(f287,plain,(
% 1.65/0.46 ( ! [X0 : $i] : ((((in @ (kpair @ X0 @ (ap @ sK9 @ sK10 @ sK11 @ X0)) @ sK12)) = $true) | (((in @ X0 @ sK9)) != $true)) ) | (~spl22_8 | ~spl22_19)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f286,f125])).
% 1.65/0.46 thf(f288,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((func @ sK9 @ sK10 @ sK12)) != $true) | (((ap @ sK9 @ sK10 @ sK11 @ X0)) = X1) | (((in @ X0 @ sK9)) != $true) | (((in @ X0 @ sK9)) != $true) | (((in @ X1 @ sK10)) != $true) | (((in @ (kpair @ X0 @ X1) @ sK12)) != $true)) ) | ~spl22_11),
% 1.65/0.46 inference(superposition,[],[f138,f73])).
% 1.65/0.46 thf(f293,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ X0 @ sK9)) != $true) | (((ap @ sK9 @ sK10 @ sK11 @ X0)) = X1) | (((in @ (kpair @ X0 @ X1) @ sK12)) != $true) | (((func @ sK9 @ sK10 @ sK12)) != $true) | (((in @ X1 @ sK10)) != $true)) ) | ~spl22_11),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f288])).
% 1.65/0.46 thf(f296,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((ap @ sK9 @ sK10 @ sK11 @ X0)) = X1) | (((in @ X1 @ sK10)) != $true) | (((in @ X0 @ sK9)) != $true) | (((in @ (kpair @ X0 @ X1) @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_11)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f293,f125])).
% 1.65/0.46 thf(f298,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ X1 @ sK9)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK12)) = $true) | (((in @ (kpair @ X1 @ X0) @ sK11)) != $true) | (((func @ sK9 @ sK10 @ sK11)) != $true) | (((in @ X0 @ sK10)) != $true) | (((in @ X1 @ sK9)) != $true)) ) | (~spl22_8 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(superposition,[],[f287,f138])).
% 1.65/0.46 thf(f299,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ X1 @ sK9)) != $true) | (((func @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK11)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK12)) = $true) | (((in @ X0 @ sK10)) != $true)) ) | (~spl22_8 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f298])).
% 1.65/0.46 thf(f300,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ X1 @ X0) @ sK12)) = $true) | (((in @ X1 @ sK9)) != $true) | (((in @ X0 @ sK10)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f299,f134])).
% 1.65/0.46 thf(f305,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ X1 @ sK9)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK11)) = $true) | (((func @ sK9 @ sK10 @ sK11)) != $true) | (((in @ X1 @ sK9)) != $true) | (((in @ X0 @ sK10)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(superposition,[],[f174,f296])).
% 1.65/0.46 thf(f306,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ X0 @ sK10)) != $true) | (((in @ X1 @ sK9)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK11)) = $true) | (((func @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (kpair @ X1 @ X0) @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f305])).
% 1.65/0.46 thf(f311,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ X1 @ X0) @ sK11)) = $true) | (((in @ (kpair @ X1 @ X0) @ sK12)) != $true) | (((in @ X1 @ sK9)) != $true) | (((in @ X0 @ sK10)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f306,f134])).
% 1.65/0.46 thf(f477,plain,(
% 1.65/0.46 ( ! [X1 : $i] : ((((func @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (ex1 @ Y1 @ (^[Y4 : $i]: (in @ (kpair @ Y3 @ Y4) @ Y2)))))) & (breln @ Y0 @ Y1 @ Y2))))))) @ X1)))) ) | ~spl22_27),
% 1.65/0.46 inference(argument_congruence,[],[f213])).
% 1.65/0.46 thf(f478,plain,(
% 1.65/0.46 ( ! [X1 : $i] : ((((func @ X1)) = (^[Y0 : $i]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X1) => (ex1 @ Y0 @ (^[Y3 : $i]: (in @ (kpair @ Y2 @ Y3) @ Y1)))))) & (breln @ X1 @ Y0 @ Y1))))))) ) | ~spl22_27),
% 1.65/0.46 inference(beta-eta_normalization,[],[f477])).
% 1.65/0.46 thf(f567,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((in @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ sK9)) != $true) | (((in @ (kpair @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ (sK6 @ X0 @ sK12 @ X1 @ X2)) @ sK11)) != $true) | (((breln @ X2 @ X1 @ X0)) != $true) | (((breln @ X2 @ X1 @ sK12)) != $true) | (sK12 = X0) | ($true != ((in @ (sK6 @ X0 @ sK12 @ X1 @ X2) @ sK10))) | (((in @ (sK7 @ X0 @ sK12 @ X1 @ X2) @ X2)) = $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(superposition,[],[f198,f300])).
% 1.65/0.46 thf(f570,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ (sK6 @ X0 @ sK12 @ X1 @ X2)) @ sK11)) != $true) | (((breln @ X2 @ X1 @ sK12)) != $true) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ sK9)) != $true) | ($true != ((in @ (sK6 @ X0 @ sK12 @ X1 @ X2) @ sK10))) | (((in @ (sK7 @ X0 @ sK12 @ X1 @ X2) @ X2)) = $true) | (sK12 = X0)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f567])).
% 1.65/0.46 thf(f573,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | ($true != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12)) ) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(superposition,[],[f570,f129])).
% 1.65/0.46 thf(f576,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK12)) != $true) | ($true != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true)) ) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f573])).
% 1.65/0.46 thf(f577,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (sK11 = sK12) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f576])).
% 1.65/0.46 thf(f582,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f577,f147])).
% 1.65/0.46 thf(f585,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (sK11 = X0) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9))) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true) | ($true = ((in @ (sK5 @ sK11 @ X0 @ X1 @ X2) @ X2))) | (((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | (((breln @ X2 @ X1 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(superposition,[],[f241,f311])).
% 1.65/0.46 thf(f588,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | ($true = ((in @ (sK5 @ sK11 @ X0 @ X1 @ X2) @ X2))) | (((breln @ X2 @ X1 @ X0)) != $true) | (sK11 = X0) | (((breln @ X2 @ X1 @ sK11)) != $true) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9))) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f585])).
% 1.65/0.46 thf(f589,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK8 @ X0 @ sK12 @ X1 @ X2) @ X1)) = $true) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ sK9)) != $true) | (sK12 = X0) | (((breln @ X2 @ X1 @ sK12)) != $true) | ($true != ((in @ (sK6 @ X0 @ sK12 @ X1 @ X2) @ sK10))) | ($true != $true) | (((in @ (kpair @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ (sK6 @ X0 @ sK12 @ X1 @ X2)) @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(superposition,[],[f255,f300])).
% 1.65/0.46 thf(f593,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ (sK6 @ X0 @ sK12 @ X1 @ X2)) @ sK11)) != $true) | (((in @ (sK8 @ X0 @ sK12 @ X1 @ X2) @ X1)) = $true) | (((breln @ X2 @ X1 @ sK12)) != $true) | ($true != ((in @ (sK6 @ X0 @ sK12 @ X1 @ X2) @ sK10))) | (sK12 = X0) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (sK5 @ X0 @ sK12 @ X1 @ X2) @ sK9)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f589])).
% 1.65/0.46 thf(f637,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_18 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(superposition,[],[f588,f170])).
% 1.65/0.46 thf(f642,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (sK11 = sK12) | ($true != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_18 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f637])).
% 1.65/0.46 thf(f643,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_18 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f642])).
% 1.65/0.46 thf(f647,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ X1)) = $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_18 | ~spl22_19 | ~spl22_33)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f643,f147])).
% 1.65/0.46 thf(f661,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true) | (((breln @ X2 @ X1 @ X0)) != $true) | (sK11 = X0) | (((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | (((breln @ X2 @ X1 @ sK11)) != $true) | ($true = ((in @ (sK6 @ sK11 @ X0 @ X1 @ X2) @ X1))) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9)))) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_41)),
% 1.65/0.46 inference(superposition,[],[f276,f311])).
% 1.65/0.46 thf(f663,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | (((breln @ X2 @ X1 @ sK11)) != $true) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9))) | (sK11 = X0) | ($true = ((in @ (sK6 @ sK11 @ X0 @ X1 @ X2) @ X1))) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true) | (((breln @ X2 @ X1 @ X0)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_41)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f661])).
% 1.65/0.46 thf(f666,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK5 @ sK11 @ X0 @ X1 @ X2) @ (sK6 @ sK11 @ X0 @ X1 @ X2)) @ X0)) != $true) | (((breln @ X2 @ X1 @ sK11)) != $true) | (sK11 = X0) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true) | (((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9))) | ($true != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(superposition,[],[f93,f311])).
% 1.65/0.46 thf(f669,plain,(
% 1.65/0.46 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ (sK8 @ sK11 @ X0 @ X1 @ X2)) @ sK12)) != $true) | (sK11 = X0) | (((breln @ X2 @ X1 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ X0 @ X1 @ X2) @ sK10)) != $true) | (((breln @ X2 @ X1 @ X0)) != $true) | (((in @ (kpair @ (sK5 @ sK11 @ X0 @ X1 @ X2) @ (sK6 @ sK11 @ X0 @ X1 @ X2)) @ X0)) != $true) | ($true != ((in @ (sK7 @ sK11 @ X0 @ X1 @ X2) @ sK9)))) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f666])).
% 1.65/0.46 thf(f696,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((sK11 = sK12) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_17 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(superposition,[],[f593,f166])).
% 1.65/0.46 thf(f700,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_17 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f696])).
% 1.65/0.46 thf(f701,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (sK11 = sK12) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_17 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f700])).
% 1.65/0.46 thf(f706,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f701,f147])).
% 1.65/0.46 thf(f773,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (sK11 = sK12)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_38 | ~spl22_41)),
% 1.65/0.46 inference(superposition,[],[f663,f263])).
% 1.65/0.46 thf(f783,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (sK11 = sK12) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_38 | ~spl22_41)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f773])).
% 1.65/0.46 thf(f784,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (sK11 = sK12) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_38 | ~spl22_41)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f783])).
% 1.65/0.46 thf(f789,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ X0)) = $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_38 | ~spl22_41)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f784,f147])).
% 1.65/0.46 thf(f911,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK12)) != $true) | ($true != ((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK12))) | ($true != ((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK12))) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (sK11 = sK12) | ($true != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(superposition,[],[f669,f179])).
% 1.65/0.46 thf(f918,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | ($true != ((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK12))) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (sK11 = sK12)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f911])).
% 1.65/0.46 thf(f919,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | ($true != ((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK12))) | (sK11 = sK12) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f918])).
% 1.65/0.46 thf(f926,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK12))) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f919,f147])).
% 1.65/0.46 thf(f970,plain,(
% 1.65/0.46 ( ! [X2 : $i,X1 : $i] : ((((func @ X1 @ X2)) = (((^[Y0 : $i]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X1) => (ex1 @ Y0 @ (^[Y3 : $i]: (in @ (kpair @ Y2 @ Y3) @ Y1)))))) & (breln @ X1 @ Y0 @ Y1))))) @ X2)))) ) | ~spl22_27),
% 1.65/0.46 inference(argument_congruence,[],[f478])).
% 1.65/0.46 thf(f971,plain,(
% 1.65/0.46 ( ! [X2 : $i,X1 : $i] : (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (ex1 @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y1 @ Y2) @ Y0)))))) & (breln @ X1 @ X2 @ Y0))) = ((func @ X1 @ X2)))) ) | ~spl22_27),
% 1.65/0.46 inference(beta-eta_normalization,[],[f970])).
% 1.65/0.46 thf(f999,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | ($true != $true) | (((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(superposition,[],[f926,f300])).
% 1.65/0.46 thf(f1001,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f999])).
% 1.65/0.46 thf(f1053,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | ($true != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(superposition,[],[f1001,f226])).
% 1.65/0.46 thf(f1060,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | ($true != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f1053])).
% 1.65/0.46 thf(f1061,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1060])).
% 1.65/0.46 thf(f1068,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1061,f147])).
% 1.65/0.46 thf(f1088,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(superposition,[],[f1068,f311])).
% 1.65/0.46 thf(f1090,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | ($true != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f1088])).
% 1.65/0.46 thf(f1091,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ (sK8 @ sK11 @ sK12 @ X0 @ X1)) @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1090])).
% 1.65/0.46 thf(f1144,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | ($true != $true) | (((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) = $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (sK11 = sK12) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_42)),
% 1.65/0.46 inference(superposition,[],[f1091,f280])).
% 1.65/0.46 thf(f1150,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((sK11 = sK12) | ($true != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) = $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_42)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f1144])).
% 1.65/0.46 thf(f1151,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (kpair @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ (sK6 @ sK11 @ sK12 @ X0 @ X1)) @ sK11)) = $true) | (sK11 = sK12) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_42)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1150])).
% 1.65/0.46 thf(f1160,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (sK11 = sK12) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_42)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1151,f1001])).
% 1.65/0.46 thf(f1161,plain,(
% 1.65/0.46 ( ! [X0 : $i,X1 : $i] : ((((in @ (sK8 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true) | (((breln @ X1 @ X0 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((breln @ X1 @ X0 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ X0 @ X1) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ X0 @ X1) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_42)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1160,f147])).
% 1.65/0.46 thf(f1164,plain,(
% 1.65/0.46 ( ! [X0 : $i] : ((((in @ (sK7 @ sK11 @ sK12 @ sK10 @ X0) @ sK9)) != $true) | (((breln @ X0 @ sK10 @ sK12)) != $true) | ($true != ((in @ (sK5 @ sK11 @ sK12 @ sK10 @ X0) @ sK9))) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ X0) @ sK10)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ X0) @ sK10)) != $true) | (((breln @ X0 @ sK10 @ sK11)) != $true) | ($true != ((in @ (sK5 @ sK11 @ sK12 @ sK10 @ X0) @ sK9))) | ($true != $true) | (((breln @ X0 @ sK10 @ sK12)) != $true) | (((breln @ X0 @ sK10 @ sK11)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(superposition,[],[f1161,f706])).
% 1.65/0.46 thf(f1166,plain,(
% 1.65/0.46 ( ! [X0 : $i] : ((((breln @ X0 @ sK10 @ sK12)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ X0) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ X0) @ sK10)) != $true) | (((breln @ X0 @ sK10 @ sK11)) != $true) | ($true != $true) | ($true != ((in @ (sK5 @ sK11 @ sK12 @ sK10 @ X0) @ sK9)))) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f1164])).
% 1.65/0.46 thf(f1167,plain,(
% 1.65/0.46 ( ! [X0 : $i] : (($true != ((in @ (sK5 @ sK11 @ sK12 @ sK10 @ X0) @ sK9))) | (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ X0) @ sK9)) != $true) | (((breln @ X0 @ sK10 @ sK11)) != $true) | (((breln @ X0 @ sK10 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ X0) @ sK10)) != $true)) ) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1166])).
% 1.65/0.46 thf(f1181,definition,(
% 1.65/0.46 spl22_48 <=> (((breln @ sK9 @ sK10 @ sK11)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_48])],[avatar_definition])).
% 1.65/0.46 thf(f1182,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) = $true) | ~spl22_48),
% 1.65/0.46 inference(avatar_component_clause,[],[f1181])).
% 1.65/0.46 thf(f1183,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | spl22_48),
% 1.65/0.46 inference(avatar_component_clause,[],[f1181])).
% 1.65/0.46 thf(f1189,definition,(
% 1.65/0.46 spl22_50 <=> (((breln @ sK9 @ sK10 @ sK12)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition])).
% 1.65/0.46 thf(f1190,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) = $true) | ~spl22_50),
% 1.65/0.46 inference(avatar_component_clause,[],[f1189])).
% 1.65/0.46 thf(f1191,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | spl22_50),
% 1.65/0.46 inference(avatar_component_clause,[],[f1189])).
% 1.65/0.46 thf(f1214,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | ($true != $true) | (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(superposition,[],[f1167,f647])).
% 1.65/0.46 thf(f1218,plain,(
% 1.65/0.46 (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | ($true != $true) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(duplicate_literal_removal,[],[f1214])).
% 1.65/0.46 thf(f1219,plain,(
% 1.65/0.46 (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_42)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1218])).
% 1.65/0.46 thf(f1221,plain,(
% 1.65/0.46 (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_38 | ~spl22_41 | ~spl22_42)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1219,f789])).
% 1.65/0.46 thf(f1231,definition,(
% 1.65/0.46 spl22_54 <=> (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_54])],[avatar_definition])).
% 1.65/0.46 thf(f1233,plain,(
% 1.65/0.46 (((in @ (sK7 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | spl22_54),
% 1.65/0.46 inference(avatar_component_clause,[],[f1231])).
% 1.65/0.46 thf(f1235,definition,(
% 1.65/0.46 spl22_55 <=> (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_55])],[avatar_definition])).
% 1.65/0.46 thf(f1240,definition,(
% 1.65/0.46 spl22_56 <=> (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition])).
% 1.65/0.46 thf(f1242,plain,(
% 1.65/0.46 (((in @ (sK8 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | spl22_56),
% 1.65/0.46 inference(avatar_component_clause,[],[f1240])).
% 1.65/0.46 thf(f1243,plain,(
% 1.65/0.46 ~spl22_56 | ~spl22_50 | ~spl22_48 | ~spl22_54 | ~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_38 | ~spl22_41 | ~spl22_42),
% 1.65/0.46 inference(avatar_split_clause,[],[f1221,f279,f275,f262,f254,f240,f225,f178,f173,f169,f165,f145,f137,f132,f123,f92,f1231,f1181,f1189,f1240])).
% 1.65/0.46 thf(f1244,plain,(
% 1.65/0.46 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((func @ X1 @ X2 @ X3)) = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (ex1 @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y1 @ Y2) @ Y0)))))) & (breln @ X1 @ X2 @ Y0))) @ X3)))) ) | ~spl22_27),
% 1.65/0.46 inference(argument_congruence,[],[f971])).
% 1.65/0.46 thf(f1246,plain,(
% 1.65/0.46 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((func @ X1 @ X2 @ X3))) | ($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (ex1 @ X2 @ (^[Y2 : $i]: (in @ (kpair @ Y1 @ Y2) @ Y0)))))) & (breln @ X1 @ X2 @ Y0))) @ X3)))) ) | ~spl22_27),
% 1.65/0.46 inference(iff_proxy_clausification,[],[f1244])).
% 1.65/0.46 thf(f1247,plain,(
% 1.65/0.46 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (ex1 @ X2 @ (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ X3)))))) & (breln @ X1 @ X2 @ X3)))) | ($false = ((func @ X1 @ X2 @ X3)))) ) | ~spl22_27),
% 1.65/0.46 inference(beta-eta_normalization,[],[f1246])).
% 1.65/0.46 thf(f1248,plain,(
% 1.65/0.46 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((breln @ X1 @ X2 @ X3))) | ($false = ((func @ X1 @ X2 @ X3)))) ) | ~spl22_27),
% 1.65/0.46 inference(and_proxy_clausification,[],[f1247])).
% 1.65/0.46 thf(f1273,plain,(
% 1.65/0.46 (((func @ sK9 @ sK10 @ sK11)) = $false) | ($true != $true) | (~spl22_27 | spl22_48)),
% 1.65/0.46 inference(superposition,[],[f1183,f1248])).
% 1.65/0.46 thf(f1274,plain,(
% 1.65/0.46 (((func @ sK9 @ sK10 @ sK11)) = $false) | (~spl22_27 | spl22_48)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1273])).
% 1.65/0.46 thf(f1276,definition,(
% 1.65/0.46 spl22_57 <=> (((func @ sK9 @ sK10 @ sK11)) = $false)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition])).
% 1.65/0.46 thf(f1278,plain,(
% 1.65/0.46 (((func @ sK9 @ sK10 @ sK11)) = $false) | ~spl22_57),
% 1.65/0.46 inference(avatar_component_clause,[],[f1276])).
% 1.65/0.46 thf(f1279,plain,(
% 1.65/0.46 spl22_57 | ~spl22_27 | spl22_48),
% 1.65/0.46 inference(avatar_split_clause,[],[f1274,f1181,f211,f1276])).
% 1.65/0.46 thf(f1329,plain,(
% 1.65/0.46 ($true != $true) | (((func @ sK9 @ sK10 @ sK12)) = $false) | (~spl22_27 | spl22_50)),
% 1.65/0.46 inference(superposition,[],[f1191,f1248])).
% 1.65/0.46 thf(f1330,plain,(
% 1.65/0.46 (((func @ sK9 @ sK10 @ sK12)) = $false) | (~spl22_27 | spl22_50)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1329])).
% 1.65/0.46 thf(f1332,definition,(
% 1.65/0.46 spl22_58 <=> (((func @ sK9 @ sK10 @ sK12)) = $false)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition])).
% 1.65/0.46 thf(f1335,plain,(
% 1.65/0.46 spl22_58 | ~spl22_27 | spl22_50),
% 1.65/0.46 inference(avatar_split_clause,[],[f1330,f1189,f211,f1332])).
% 1.65/0.46 thf(f1378,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (sK11 = sK12) | ($true != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (~spl22_39 | spl22_54)),
% 1.65/0.46 inference(superposition,[],[f1233,f267])).
% 1.65/0.46 thf(f1379,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (sK11 = sK12) | ($true != $true) | (~spl22_23 | spl22_54)),
% 1.65/0.46 inference(superposition,[],[f1233,f194])).
% 1.65/0.46 thf(f1380,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | ($true != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | spl22_54)),
% 1.65/0.46 inference(superposition,[],[f1233,f582])).
% 1.65/0.46 thf(f1382,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | spl22_54)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1380])).
% 1.65/0.46 thf(f1383,plain,(
% 1.65/0.46 (sK11 = sK12) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_23 | spl22_54)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1379])).
% 1.65/0.46 thf(f1384,plain,(
% 1.65/0.46 (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (sK11 = sK12) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_39 | spl22_54)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1378])).
% 1.65/0.46 thf(f1385,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | ~spl22_50 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1382,f1190])).
% 1.65/0.46 thf(f1386,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (spl22_13 | ~spl22_23 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1383,f147])).
% 1.65/0.46 thf(f1387,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (spl22_13 | ~spl22_39 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1384,f147])).
% 1.65/0.46 thf(f1388,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | ~spl22_48 | ~spl22_50 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1385,f1182])).
% 1.65/0.46 thf(f1389,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (spl22_13 | ~spl22_23 | ~spl22_48 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1386,f1182])).
% 1.65/0.46 thf(f1390,plain,(
% 1.65/0.46 (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (spl22_13 | ~spl22_39 | ~spl22_50 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1387,f1190])).
% 1.65/0.46 thf(f1392,definition,(
% 1.65/0.46 spl22_61 <=> (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true)),
% 1.65/0.46 introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition])).
% 1.65/0.46 thf(f1395,plain,(
% 1.65/0.46 ~spl22_55 | ~spl22_61 | ~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | ~spl22_48 | ~spl22_50 | spl22_54),
% 1.65/0.46 inference(avatar_split_clause,[],[f1388,f1231,f1189,f1181,f197,f173,f145,f137,f132,f128,f123,f1392,f1235])).
% 1.65/0.46 thf(f1396,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (spl22_13 | ~spl22_23 | ~spl22_48 | ~spl22_50 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1389,f1190])).
% 1.65/0.46 thf(f1397,plain,(
% 1.65/0.46 (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (spl22_13 | ~spl22_39 | ~spl22_48 | ~spl22_50 | spl22_54)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1390,f1182])).
% 1.65/0.46 thf(f1398,plain,(
% 1.65/0.46 spl22_61 | spl22_13 | ~spl22_23 | ~spl22_48 | ~spl22_50 | spl22_54),
% 1.65/0.46 inference(avatar_split_clause,[],[f1396,f1231,f1189,f1181,f193,f145,f1392])).
% 1.65/0.46 thf(f1399,plain,(
% 1.65/0.46 spl22_55 | spl22_13 | ~spl22_39 | ~spl22_48 | ~spl22_50 | spl22_54),
% 1.65/0.46 inference(avatar_split_clause,[],[f1397,f1231,f1189,f1181,f266,f145,f1235])).
% 1.65/0.46 thf(f1586,plain,(
% 1.65/0.46 ($false = $true) | (~spl22_10 | ~spl22_57)),
% 1.65/0.46 inference(superposition,[],[f1278,f134])).
% 1.65/0.46 thf(f1590,plain,(
% 1.65/0.46 $false | (~spl22_10 | ~spl22_57)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1586])).
% 1.65/0.46 thf(f1591,plain,(
% 1.65/0.46 ~spl22_10 | ~spl22_57),
% 1.65/0.46 inference(avatar_contradiction_clause,[],[f1590])).
% 1.65/0.46 thf(f1629,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK12)) != $true) | (sK11 = sK12) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | ($true != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_37 | spl22_56)),
% 1.65/0.46 inference(superposition,[],[f1242,f259])).
% 1.65/0.46 thf(f1630,plain,(
% 1.65/0.46 (sK11 = sK12) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | ($true != $true) | (~spl22_28 | spl22_56)),
% 1.65/0.46 inference(superposition,[],[f1242,f217])).
% 1.65/0.46 thf(f1631,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | ($true != $true) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36 | spl22_56)),
% 1.65/0.46 inference(superposition,[],[f1242,f706])).
% 1.65/0.46 thf(f1633,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (sK11 = sK12) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (~spl22_28 | spl22_56)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1630])).
% 1.65/0.46 thf(f1634,plain,(
% 1.65/0.46 (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36 | spl22_56)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1631])).
% 1.65/0.46 thf(f1635,plain,(
% 1.65/0.46 (sK11 = sK12) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (~spl22_37 | spl22_56)),
% 1.65/0.46 inference(trivial_inequality_removal,[],[f1629])).
% 1.65/0.46 thf(f1636,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (spl22_13 | ~spl22_28 | spl22_56)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1633,f147])).
% 1.65/0.46 thf(f1637,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) != $true) | (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) != $true) | (~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36 | ~spl22_50 | spl22_56)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1634,f1190])).
% 1.65/0.46 thf(f1638,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((breln @ sK9 @ sK10 @ sK12)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (spl22_13 | ~spl22_37 | spl22_56)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1635,f147])).
% 1.65/0.46 thf(f1639,plain,(
% 1.65/0.46 (((in @ (sK5 @ sK11 @ sK12 @ sK10 @ sK9) @ sK9)) = $true) | (((breln @ sK9 @ sK10 @ sK11)) != $true) | (spl22_13 | ~spl22_28 | ~spl22_50 | spl22_56)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1636,f1190])).
% 1.65/0.46 thf(f1640,plain,(
% 1.65/0.46 ~spl22_48 | ~spl22_61 | ~spl22_55 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36 | ~spl22_50 | spl22_56),
% 1.65/0.46 inference(avatar_split_clause,[],[f1637,f1240,f1189,f254,f173,f165,f145,f137,f132,f123,f1235,f1392,f1181])).
% 1.65/0.46 thf(f1641,plain,(
% 1.65/0.46 (((breln @ sK9 @ sK10 @ sK11)) != $true) | (((in @ (sK6 @ sK11 @ sK12 @ sK10 @ sK9) @ sK10)) = $true) | (spl22_13 | ~spl22_37 | ~spl22_50 | spl22_56)),
% 1.65/0.46 inference(forward_subsumption_resolution,[],[f1638,f1190])).
% 1.65/0.46 thf(f1642,plain,(
% 1.65/0.46 ~spl22_48 | spl22_61 | spl22_13 | ~spl22_28 | ~spl22_50 | spl22_56),
% 1.65/0.46 inference(avatar_split_clause,[],[f1639,f1240,f1189,f216,f145,f1392,f1181])).
% 1.65/0.46 thf(f1643,plain,(
% 1.65/0.46 ~spl22_48 | spl22_55 | spl22_13 | ~spl22_37 | ~spl22_50 | spl22_56),
% 1.65/0.46 inference(avatar_split_clause,[],[f1641,f1240,f1189,f258,f145,f1235,f1181])).
% 1.65/0.46 thf(f1644,definition,(
% 1.65/0.46 (((func @ sK9 @ sK10 @ sK12)) != $false) | (((func @ sK9 @ sK10 @ sK12)) != $true) | (((func @ sK9 @ sK10 @ sK11)) != $true) | (((func @ sK9 @ sK10 @ sK11)) = $false)),
% 1.65/0.46 introduced(theory,[theory_tautology_sat_conflict])).
% 1.65/0.46 cnf(s1, plain, spl22_1 | ~spl22_2, inference(sat_conversion,[],[f98])).
% 1.65/0.46 cnf(s5, plain, spl22_7, inference(sat_conversion,[],[f121])).
% 1.65/0.46 cnf(s6, plain, spl22_8, inference(sat_conversion,[],[f126])).
% 1.65/0.46 cnf(s7, plain, ~spl22_2 | spl22_9, inference(sat_conversion,[],[f130])).
% 1.65/0.46 cnf(s8, plain, spl22_10, inference(sat_conversion,[],[f135])).
% 1.65/0.46 cnf(s9, plain, spl22_11 | ~spl22_12, inference(sat_conversion,[],[f143])).
% 1.65/0.46 cnf(s10, plain, ~spl22_13, inference(sat_conversion,[],[f148])).
% 1.65/0.46 cnf(s15, plain, ~spl22_2 | spl22_17, inference(sat_conversion,[],[f167])).
% 1.65/0.46 cnf(s16, plain, ~spl22_2 | spl22_18, inference(sat_conversion,[],[f171])).
% 1.65/0.46 cnf(s17, plain, ~spl22_4 | spl22_19, inference(sat_conversion,[],[f175])).
% 1.65/0.46 cnf(s18, plain, spl22_12, inference(sat_conversion,[],[f176])).
% 1.65/0.46 cnf(s19, plain, ~spl22_2 | spl22_20, inference(sat_conversion,[],[f180])).
% 1.65/0.46 cnf(s20, plain, spl22_2 | ~spl22_7, inference(sat_conversion,[],[f181])).
% 1.65/0.46 cnf(s23, plain, ~spl22_2 | spl22_23, inference(sat_conversion,[],[f195])).
% 1.65/0.46 cnf(s24, plain, ~spl22_2 | spl22_24, inference(sat_conversion,[],[f199])).
% 1.65/0.46 cnf(s27, plain, spl22_27, inference(sat_conversion,[],[f214])).
% 1.65/0.46 cnf(s28, plain, ~spl22_2 | spl22_28, inference(sat_conversion,[],[f218])).
% 1.65/0.46 cnf(s30, plain, ~spl22_2 | spl22_30, inference(sat_conversion,[],[f227])).
% 1.65/0.46 cnf(s32, plain, spl22_4, inference(sat_conversion,[],[f233])).
% 1.65/0.46 cnf(s34, plain, ~spl22_2 | spl22_33, inference(sat_conversion,[],[f242])).
% 1.65/0.46 cnf(s37, plain, ~spl22_2 | spl22_36, inference(sat_conversion,[],[f256])).
% 1.65/0.46 cnf(s38, plain, ~spl22_2 | spl22_37, inference(sat_conversion,[],[f260])).
% 1.65/0.46 cnf(s39, plain, ~spl22_2 | spl22_38, inference(sat_conversion,[],[f264])).
% 1.65/0.46 cnf(s40, plain, ~spl22_2 | spl22_39, inference(sat_conversion,[],[f268])).
% 1.65/0.46 cnf(s42, plain, ~spl22_2 | spl22_41, inference(sat_conversion,[],[f277])).
% 1.65/0.46 cnf(s43, plain, ~spl22_2 | spl22_42, inference(sat_conversion,[],[f281])).
% 1.65/0.46 cnf(s52, plain, ~spl22_1 | ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_18 | ~spl22_19 | ~spl22_20 | ~spl22_30 | ~spl22_33 | ~spl22_36 | ~spl22_38 | ~spl22_41 | ~spl22_42 | ~spl22_48 | ~spl22_50 | ~spl22_54 | ~spl22_56, inference(sat_conversion,[],[f1243])).
% 1.65/0.46 cnf(s53, plain, ~spl22_27 | spl22_48 | spl22_57, inference(sat_conversion,[],[f1279])).
% 1.65/0.46 cnf(s54, plain, ~spl22_27 | spl22_50 | spl22_58, inference(sat_conversion,[],[f1335])).
% 1.65/0.46 cnf(s56, plain, ~spl22_8 | ~spl22_9 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_19 | ~spl22_24 | ~spl22_48 | ~spl22_50 | spl22_54 | ~spl22_55 | ~spl22_61, inference(sat_conversion,[],[f1395])).
% 1.65/0.46 cnf(s57, plain, spl22_13 | ~spl22_23 | ~spl22_48 | ~spl22_50 | spl22_54 | spl22_61, inference(sat_conversion,[],[f1398])).
% 1.65/0.46 cnf(s58, plain, spl22_13 | ~spl22_39 | ~spl22_48 | ~spl22_50 | spl22_54 | spl22_55, inference(sat_conversion,[],[f1399])).
% 1.65/0.46 cnf(s77, plain, ~spl22_10 | ~spl22_57, inference(sat_conversion,[],[f1591])).
% 1.65/0.46 cnf(s78, plain, ~spl22_8 | ~spl22_10 | ~spl22_11 | spl22_13 | ~spl22_17 | ~spl22_19 | ~spl22_36 | ~spl22_48 | ~spl22_50 | ~spl22_55 | spl22_56 | ~spl22_61, inference(sat_conversion,[],[f1640])).
% 1.65/0.46 cnf(s79, plain, spl22_13 | ~spl22_28 | ~spl22_48 | ~spl22_50 | spl22_56 | spl22_61, inference(sat_conversion,[],[f1642])).
% 1.65/0.46 cnf(s80, plain, spl22_13 | ~spl22_37 | ~spl22_48 | ~spl22_50 | spl22_55 | spl22_56, inference(sat_conversion,[],[f1643])).
% 1.65/0.46 cnf(s81, plain, ~spl22_8 | ~spl22_10 | spl22_57 | ~spl22_58, inference(sat_conversion,[],[f1644])).
% 1.65/0.46 cnf(s82, plain, spl22_19, inference(rat,[],[s17,s32])).
% 1.65/0.46 cnf(s83, plain, spl22_11, inference(rat,[],[s9,s18])).
% 1.65/0.46 cnf(s84, plain, ~spl22_57, inference(rat,[],[s77,s8])).
% 1.65/0.46 cnf(s85, plain, spl22_48, inference(rat,[],[s53,s27,s84])).
% 1.65/0.46 cnf(s86, plain, ~spl22_58, inference(rat,[],[s81,s84,s8,s6])).
% 1.65/0.46 cnf(s87, plain, spl22_50, inference(rat,[],[s54,s27,s86])).
% 1.65/0.46 cnf(s88, plain, spl22_2, inference(rat,[],[s20,s5])).
% 1.65/0.46 cnf(s89, plain, spl22_42, inference(rat,[],[s43,s88])).
% 1.65/0.46 cnf(s90, plain, spl22_41, inference(rat,[],[s42,s88])).
% 1.65/0.46 cnf(s91, plain, spl22_39, inference(rat,[],[s40,s88])).
% 1.65/0.46 cnf(s92, plain, spl22_38, inference(rat,[],[s39,s88])).
% 1.65/0.46 cnf(s93, plain, spl22_37, inference(rat,[],[s38,s88])).
% 1.65/0.46 cnf(s94, plain, spl22_36, inference(rat,[],[s37,s88])).
% 1.65/0.46 cnf(s95, plain, spl22_33, inference(rat,[],[s34,s88])).
% 1.65/0.46 cnf(s96, plain, spl22_30, inference(rat,[],[s30,s88])).
% 1.65/0.46 cnf(s97, plain, spl22_28, inference(rat,[],[s28,s88])).
% 1.65/0.46 cnf(s98, plain, spl22_24, inference(rat,[],[s24,s88])).
% 1.65/0.46 cnf(s99, plain, spl22_23, inference(rat,[],[s23,s88])).
% 1.65/0.46 cnf(s100, plain, spl22_20, inference(rat,[],[s19,s88])).
% 1.65/0.46 cnf(s101, plain, spl22_18, inference(rat,[],[s16,s88])).
% 1.65/0.46 cnf(s102, plain, spl22_17, inference(rat,[],[s15,s88])).
% 1.65/0.46 cnf(s103, plain, spl22_9, inference(rat,[],[s7,s88])).
% 1.65/0.46 cnf(s104, plain, spl22_1, inference(rat,[],[s1,s88])).
% 1.65/0.46 cnf(s105, plain, spl22_54, inference(rat,[],[s56,s57,s58,s8,s83,s10,s82,s6,s85,s87,s98,s103,s99,s91])).
% 1.65/0.46 cnf(s106, plain, ~spl22_56, inference(rat,[],[s52,s104,s102,s87,s85,s89,s90,s92,s94,s95,s96,s100,s82,s101,s6,s10,s83,s8,s105])).
% 1.65/0.46 cnf(s107, plain, spl22_61, inference(rat,[],[s79,s97,s87,s85,s10,s106])).
% 1.65/0.46 cnf(s108, plain, spl22_55, inference(rat,[],[s80,s93,s87,s85,s10,s106])).
% 1.65/0.46 cnf(s109, plain, $false, inference(rat,[],[s78,s108,s102,s94,s87,s85,s6,s82,s8,s10,s83,s107,s106])).
% 1.65/0.46 thf(f1645,plain,(
% 1.65/0.46 $false),
% 1.65/0.46 inference(avatar_sat_refutation,[],[s109])).
% 1.65/0.46 % SZS output end Proof for theBenchmark
% 1.65/0.46 % (2564169)------------------------------
% 1.65/0.46 % (2564169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.46 % (2564169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.46 % (2564169)CaDiCaL version: 2.1.3
% 1.65/0.46 % (2564169)Termination reason: Refutation
% 1.65/0.46 % (2564169)Time elapsed: 0.188 s
% 1.65/0.46 % (2564169)Peak memory usage: 14 MB
% 1.65/0.46 % (2564169)Instructions burned: 373 (million)
% 1.65/0.46 % (2564161)Success in time 0.228 s
% 1.65/0.46 % Vampire exiting
%------------------------------------------------------------------------------