%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX175^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:40:39 AM UTC 2026
% Result : Theorem 0.21s 0.33s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX175^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 16:10:03 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.33 % (3056310)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.33 % (3056319)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2934911382:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.33 % (3056321)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.33 % (3056321)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.33 % (3056316)lrs+10_16_si=on:nwc=1.5:random_seed=88037139:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.33 % (3056315)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=133008346:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.33 % (3056317)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=173988064:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.33 % (3056319)Instruction limit reached!
% 0.21/0.33 % (3056319)------------------------------
% 0.21/0.33 % (3056319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056319)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056319)Termination reason: Instruction limit
% 0.21/0.33 % (3056319)Termination phase: Saturation
% 0.21/0.33 % (3056319)Time elapsed: 0.007 s
% 0.21/0.33 % (3056319)Peak memory usage: 12 MB
% 0.21/0.33 % (3056319)Instructions burned: 24 (million)
% 0.21/0.33 % (3056318)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=2914194757:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.33 % (3056320)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=389364736:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.33 % (3056321)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=2582207150:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.33 % (3056317)Instruction limit reached!
% 0.21/0.33 % (3056317)------------------------------
% 0.21/0.33 % (3056317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056317)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056317)Termination reason: Instruction limit
% 0.21/0.33 % (3056317)Termination phase: Saturation
% 0.21/0.33 % (3056317)Time elapsed: 0.003 s
% 0.21/0.33 % (3056317)Peak memory usage: 11 MB
% 0.21/0.33 % (3056317)Instructions burned: 6 (million)
% 0.21/0.33 % (3056316)Instruction limit reached!
% 0.21/0.33 % (3056316)------------------------------
% 0.21/0.33 % (3056316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056316)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056316)Termination reason: Instruction limit
% 0.21/0.33 % (3056316)Termination phase: Saturation
% 0.21/0.33 % (3056316)Time elapsed: 0.010 s
% 0.21/0.33 % (3056316)Peak memory usage: 12 MB
% 0.21/0.33 % (3056316)Instructions burned: 20 (million)
% 0.21/0.33 % (3056329)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2090339685:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.33 % (3056329)Instruction limit reached!
% 0.21/0.33 % (3056329)------------------------------
% 0.21/0.33 % (3056329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056329)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056329)Termination reason: Instruction limit
% 0.21/0.33 % (3056329)Termination phase: Property scanning
% 0.21/0.33 % (3056329)Time elapsed: 0.001 s
% 0.21/0.33 % (3056329)Peak memory usage: 10 MB
% 0.21/0.33 % (3056329)Instructions burned: 4 (million)
% 0.21/0.33 % (3056333)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1529407693:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.21/0.33 % (3056330)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3161970158:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.33 % (3056332)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.33 % (3056330)Instruction limit reached!
% 0.21/0.33 % (3056330)------------------------------
% 0.21/0.33 % (3056330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056330)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056330)Termination reason: Instruction limit
% 0.21/0.33 % (3056330)Termination phase: Saturation
% 0.21/0.33 % (3056330)Time elapsed: 0.003 s
% 0.21/0.33 % (3056330)Peak memory usage: 11 MB
% 0.21/0.33 % (3056330)Instructions burned: 7 (million)
% 0.21/0.33 % (3056333)Instruction limit reached!
% 0.21/0.33 % (3056333)------------------------------
% 0.21/0.33 % (3056333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056321) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3056310-3056321"...
% 0.21/0.33 % (3056333)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056333)Termination reason: Instruction limit
% 0.21/0.33 % (3056333)Termination phase: Saturation
% 0.21/0.33 % (3056333)Time elapsed: 0.004 s
% 0.21/0.33 % (3056333)Peak memory usage: 12 MB
% 0.21/0.33 % (3056333)Instructions burned: 14 (million)
% 0.21/0.33 % (3056315) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3056310-3056315"...
% 0.21/0.33 % (3056332)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=734049040:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.33 % (3056332)Instruction limit reached!
% 0.21/0.33 % (3056332)------------------------------
% 0.21/0.33 % (3056332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056332)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056332)Termination reason: Instruction limit
% 0.21/0.33 % (3056332)Termination phase: Saturation
% 0.21/0.33 % (3056320)Instruction limit reached!
% 0.21/0.33 % (3056320)------------------------------
% 0.21/0.33 % (3056320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056332)Time elapsed: 0.004 s
% 0.21/0.33 % (3056320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056332)Peak memory usage: 12 MB
% 0.21/0.33 % (3056332)Instructions burned: 9 (million)
% 0.21/0.33 % (3056320)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056320)Termination reason: Instruction limit
% 0.21/0.33 % (3056320)Termination phase: Saturation
% 0.21/0.33 % (3056320)Time elapsed: 0.033 s
% 0.21/0.33 % (3056320)Peak memory usage: 12 MB
% 0.21/0.33 % (3056320)Instructions burned: 76 (million)
% 0.21/0.33 % (3056336)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.33 % (3056336)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.33 % (3056336)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=53164179:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.21/0.33 % (3056336)Instruction limit reached!
% 0.21/0.33 % (3056336)------------------------------
% 0.21/0.33 % (3056336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3056336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3056336)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3056336)Termination reason: Instruction limit
% 0.21/0.33 % (3056336)Termination phase: Saturation
% 0.21/0.33 % (3056336)Time elapsed: 0.007 s
% 0.21/0.33 % (3056336)Peak memory usage: 12 MB
% 0.21/0.33 % (3056336)Instructions burned: 30 (million)
% 0.21/0.33 % (3056337)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=3248770155:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.21/0.33 % (3056321)...printing done.
% 0.21/0.33 % (3056315)...printing done.
% 0.21/0.33 % (3056321)Refutation found. Thanks to Tanya!
% 0.21/0.33 % SZS status Theorem for theBenchmark
% 0.21/0.33 % SZS output start Proof for theBenchmark
% 0.21/0.33 thf(type_def_5, type, unsorted: $tType).
% 0.21/0.33 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.33 thf(type_def_7, type, d_unsorted: $tType).
% 0.21/0.33 thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.21/0.33 thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_8, type, itrue: ($i > $o)).
% 0.21/0.33 thf(func_def_9, type, ifalse: ($i > $o)).
% 0.21/0.33 thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.21/0.33 thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.21/0.33 thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.21/0.33 thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.21/0.33 thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.21/0.33 thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.21/0.33 thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.21/0.33 thf(func_def_23, type, vOR: ($o > $o > $o)).
% 0.21/0.33 thf(func_def_24, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.21/0.33 thf(func_def_25, type, db3: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_26, type, db0: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_27, type, vNOT: ($o > $o)).
% 0.21/0.33 thf(func_def_28, type, db1: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_29, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.21/0.33 thf(func_def_30, type, db2: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_31, type, vAND: ($o > $o > $o)).
% 0.21/0.33 thf(func_def_32, type, db5: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_33, type, db6: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_34, type, db4: !>[X0: $tType]:(X0)).
% 0.21/0.33 thf(func_def_37, type, sK0: ($i > d_unsorted)).
% 0.21/0.33 thf(func_def_38, type, sK1: ($i > $o)).
% 0.21/0.33 thf(func_def_39, type, sK2: ($i > $o)).
% 0.21/0.33 thf(func_def_41, type, sK4: ($i > $i)).
% 0.21/0.33 thf(func_def_42, type, sK5: ($i > $i)).
% 0.21/0.33 thf(func_def_43, type, sK6: ($i > $i)).
% 0.21/0.33 thf(func_def_44, type, sK7: ($i > $i)).
% 0.21/0.33 thf(func_def_45, type, sK8: ($i > $i)).
% 0.21/0.33 thf(func_def_46, type, sK9: ($i > $i)).
% 0.21/0.33 thf(func_def_47, type, sK10: ($i > $i)).
% 0.21/0.33 thf(func_def_48, type, sK11: ($i > $i)).
% 0.21/0.33 thf(func_def_49, type, sK12: ($i > $i)).
% 0.21/0.33 thf(func_def_50, type, sK13: ($i > $i)).
% 0.21/0.33 thf(f1,axiom,(
% 0.21/0.33 (mor = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X4 @ X0) | (X5 @ X0)))) & ((^[X4 : ($i > $o), X0 : $i] : (~(X4 @ X0))) = mnot) & ((^[X8 : ($i > $o), X4 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X4 @ X5)))) = mbox_s4) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1))) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))) & (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5))))) = iequiv) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)))) = iimplies) & (itrue @ (d2unsorted @ d_unsorted_0)) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (mimplies = (^[X0 : ($i > $o), X6 : ($i > $o), X7 : $i] : (~(X0 @ X7) | (X6 @ X7)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X10 : $i,X11 : $i,X5 : $i] : (~(irel @ X7 @ X5) | (((X9 @ X10) | ~(irel @ X5 @ X10) | ~ ! [X12 : $i] : (~(irel @ X5 @ X12) | (X8 @ X12))) & (~(irel @ X5 @ X11) | ~ ! [X13 : $i] : (~(irel @ X5 @ X13) | (X9 @ X13)) | (X8 @ X11)))))) = ixor) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & (ivalid = (^[X14 : ($i > $o)] : (! [X15 : $i] : (X14 @ X15)))) & ((^[X8 : ($i > $o), X7 : $i] : ((X8 @ X7))) = iatom) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : ((X9 @ X7) & (X8 @ X7))) = iand) & ((^[X14 : ($i > $o)] : (~ ! [X15 : $i] : ~(X14 @ X15))) = isatisfiable) & (inot = (^[X8 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))))) & ((^[X14 : ($i > $o)] : (! [X15 : $i] : ~(X14 @ X15))) = iinvalid) & (icountersatisfiable = (^[X14 : ($i > $o)] : (~ ! [X15 : $i] : (X14 @ X15)))) & (mand = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X4 @ X0) & (X5 @ X0)))) & (ior = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & (iimplied = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)) | ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)))))),
% 0.21/0.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcl695_1)).
% 0.21/0.33 thf(f2,conjecture,(
% 0.21/0.33 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))) = ixor)),
% 0.21/0.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ixor)).
% 0.21/0.33 thf(f3,negated_conjecture,(
% 0.21/0.33 ~ ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((inot @ (iequiv @ X0 @ X1)))) = ixor)),
% 0.21/0.33 inference(negated_conjecture,[status(cth)],[f2])).
% 0.21/0.33 thf(f4,plain,(
% 0.21/0.33 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X0 @ X2) | (X1 @ X2)))) & ((^[X3 : ($i > $o), X4 : $i] : (~(X3 @ X4))) = mnot) & ((^[X5 : ($i > $o), X6 : $i] : (! [X7 : $i] : ((X5 @ X7) | ~(irel @ X6 @ X7)))) = mbox_s4) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8) & ((^[X10 : ($i > $o), X11 : ($i > $o), X12 : $i] : ((! [X13 : $i] : ((X11 @ X13) | ~(irel @ X12 @ X13)) | ~ ! [X14 : $i] : (~(irel @ X12 @ X14) | (X10 @ X14))) & (! [X15 : $i] : ((X10 @ X15) | ~(irel @ X12 @ X15)) | ~ ! [X16 : $i] : (~(irel @ X12 @ X16) | (X11 @ X16))))) = iequiv) & ((^[X17 : ($i > $o), X18 : ($i > $o), X19 : $i] : (! [X20 : $i] : ((X18 @ X20) | ~(irel @ X19 @ X20)) | ~ ! [X21 : $i] : (~(irel @ X19 @ X21) | (X17 @ X21)))) = iimplies) & (itrue @ (d2unsorted @ d_unsorted_0)) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X22 : d_unsorted,X23 : d_unsorted] : ((((d2unsorted @ X23)) = ((d2unsorted @ X22))) => (X22 = X23)) & (mimplies = (^[X24 : ($i > $o), X25 : ($i > $o), X26 : $i] : (~(X24 @ X26) | (X25 @ X26)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & ((^[X27 : ($i > $o), X28 : ($i > $o), X29 : $i] : (~ ! [X30 : $i,X31 : $i,X32 : $i] : (~(irel @ X29 @ X32) | (((X28 @ X30) | ~(irel @ X32 @ X30) | ~ ! [X33 : $i] : (~(irel @ X32 @ X33) | (X27 @ X33))) & (~(irel @ X32 @ X31) | ~ ! [X34 : $i] : (~(irel @ X32 @ X34) | (X28 @ X34)) | (X27 @ X31)))))) = ixor) & ! [X35 : d_unsorted] : (d_unsorted_0 = X35) & (ivalid = (^[X36 : ($i > $o)] : (! [X37 : $i] : (X36 @ X37)))) & ((^[X38 : ($i > $o), X39 : $i] : ((X38 @ X39))) = iatom) & ((^[X40 : ($i > $o), X41 : ($i > $o), X42 : $i] : ((X41 @ X42) & (X40 @ X42))) = iand) & ((^[X43 : ($i > $o)] : (~ ! [X44 : $i] : ~(X43 @ X44))) = isatisfiable) & (inot = (^[X45 : ($i > $o), X46 : $i] : (~ ! [X47 : $i] : (~(irel @ X46 @ X47) | (X45 @ X47))))) & ((^[X48 : ($i > $o)] : (! [X49 : $i] : ~(X48 @ X49))) = iinvalid) & (icountersatisfiable = (^[X50 : ($i > $o)] : (~ ! [X51 : $i] : (X50 @ X51)))) & (mand = (^[X52 : ($i > $o), X53 : ($i > $o), X54 : $i] : ((X52 @ X54) & (X53 @ X54)))) & (ior = (^[X55 : ($i > $o), X56 : ($i > $o), X57 : $i] : (! [X58 : $i] : ((X56 @ X58) | ~(irel @ X57 @ X58)) | ! [X59 : $i] : ((X55 @ X59) | ~(irel @ X57 @ X59))))) & (iimplied = (^[X60 : ($i > $o), X61 : ($i > $o), X62 : $i] : (~ ! [X63 : $i] : (~(irel @ X62 @ X63) | (X61 @ X63)) | ! [X64 : $i] : (~(irel @ X62 @ X64) | (X60 @ X64)))))),
% 0.21/0.33 inference(rectify,[],[f1])).
% 0.21/0.33 thf(f5,plain,(
% 0.21/0.33 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X22 : d_unsorted,X23 : d_unsorted] : ((((d2unsorted @ X23)) = ((d2unsorted @ X22))) => (X22 = X23)) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & ! [X35 : d_unsorted] : (d_unsorted_0 = X35) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))))),
% 0.21/0.33 inference(fool_elimination,[],[f4])).
% 0.21/0.33 thf(f6,plain,(
% 0.21/0.33 ~ (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.21/0.33 inference(fool_elimination,[],[f3])).
% 0.21/0.33 thf(f7,plain,(
% 0.21/0.33 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))))),
% 0.21/0.33 inference(rectify,[],[f5])).
% 0.21/0.33 thf(f8,plain,(
% 0.21/0.33 ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3)))))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.21/0.33 inference(flattening,[],[f7])).
% 0.21/0.33 thf(f9,plain,(
% 0.21/0.33 (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.21/0.33 inference(flattening,[],[f6])).
% 0.21/0.33 thf(f10,plain,(
% 0.21/0.33 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((((d2unsorted @ X2)) != ((d2unsorted @ X3))) | (X2 = X3)) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(ennf_transformation,[],[f8])).
% 0.21/0.33 thf(f11,plain,(
% 0.21/0.33 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) != ((d2unsorted @ X3))) | (X2 = X3)) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(rectify,[],[f10])).
% 0.21/0.33 thf(f12,plain,(
% 0.21/0.33 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X0 : $i] : (((d2unsorted @ (sK0 @ X0))) = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) != ((d2unsorted @ X3))) | (X2 = X3)) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK0 @ X0)],[f11])).
% 0.21/0.33 thf(f13,plain,(
% 0.21/0.33 (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f18,plain,(
% 0.21/0.33 (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2))))))))))),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f22,plain,(
% 0.21/0.33 (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f23,plain,(
% 0.21/0.33 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))))),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f24,plain,(
% 0.21/0.33 ( ! [X4 : d_unsorted] : ((d_unsorted_0 = X4)) )),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f33,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((d2unsorted @ (sK0 @ X0))) = X0)) )),
% 0.21/0.33 inference(cnf_transformation,[],[f12])).
% 0.21/0.33 thf(f36,plain,(
% 0.21/0.33 (ixor != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (inot @ (iequiv @ Y0 @ Y1))))))),
% 0.21/0.33 inference(cnf_transformation,[],[f9])).
% 0.21/0.33 thf(f39,plain,(
% 0.21/0.33 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (!! @ $i @ (^[Y4 : $i]: ((Y2 @ Y4) | (~ (irel @ Y3 @ Y4))))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (((~ (!! @ $i @ (^[Y5 : $i]: ((Y3 @ Y5) | (~ (irel @ Y4 @ Y5)))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) & ((~ (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y5) | (~ (irel @ Y4 @ Y5)))))) | (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5))))))))))) @ Y0 @ Y1))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(definition_unfolding,[],[f36,f13,f18,f23])).
% 0.21/0.33 thf(f40,plain,(
% 0.21/0.33 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((((~ (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) & ((~ (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4)))))) | (~ (irel @ Y2 @ Y3))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))))),
% 0.21/0.33 inference(beta-eta_normalization,[],[f39])).
% 0.21/0.33 thf(f59,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((d2unsorted @ d_unsorted_0)) = X0)) )),
% 0.21/0.33 inference(forward_demodulation,[],[f33,f24])).
% 0.21/0.33 thf(f63,plain,(
% 0.21/0.33 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.21/0.33 inference(constrained_superposition,[],[f59,f59])).
% 0.21/0.33 thf(f77,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 0.21/0.33 inference(constrained_superposition,[],[f22,f59])).
% 0.21/0.33 thf(f84,plain,(
% 0.21/0.33 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (((((Y0 @ Y4) | (~ (!! @ $i @ (^[Y6 : $i]: ((Y1 @ Y6) | (~ (irel @ Y3 @ Y6))))))) | (~ (irel @ Y3 @ Y4))) & (((~ (!! @ $i @ (^[Y6 : $i]: ((Y0 @ Y6) | (~ (irel @ Y3 @ Y6)))))) | (~ (irel @ Y3 @ Y5))) | (Y1 @ Y5))) | (~ (irel @ Y2 @ Y3))))))))))))))) @ sK1)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: ((((~ (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) & ((~ (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4)))))) | (~ (irel @ Y2 @ Y3))))))))))) @ sK1)))),
% 0.21/0.33 inference(negative_extensionality,[],[f40])).
% 0.21/0.33 thf(f85,plain,(
% 0.21/0.33 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))) | (~ (irel @ Y1 @ Y2))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((sK1 @ Y3) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y2 @ Y5))))))) | (~ (irel @ Y2 @ Y3))) & (((~ (!! @ $i @ (^[Y5 : $i]: ((sK1 @ Y5) | (~ (irel @ Y2 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y0 @ Y4))) | (~ (irel @ Y1 @ Y2))))))))))))))),
% 0.21/0.33 inference(beta-eta_normalization,[],[f84])).
% 0.21/0.33 thf(f86,plain,(
% 0.21/0.33 ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (((((sK1 @ Y3) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y0 @ Y5) | (~ (irel @ Y2 @ Y5))))))) | (~ (irel @ Y2 @ Y3))) & (((~ (!! @ $i @ (^[Y5 : $i]: ((sK1 @ Y5) | (~ (irel @ Y2 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y0 @ Y4))) | (~ (irel @ Y1 @ Y2))))))))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((((~ (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))) | (~ (irel @ Y1 @ Y2))))))))) @ sK2)))),
% 0.21/0.33 inference(negative_extensionality,[],[f85])).
% 0.21/0.33 thf(f87,plain,(
% 0.21/0.33 ((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((((~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))))) != (^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((sK1 @ Y2) | (~ (!! @ $i @ (^[Y4 : $i]: ((sK2 @ Y4) | (~ (irel @ Y1 @ Y4))))))) | (~ (irel @ Y1 @ Y2))) & (((~ (!! @ $i @ (^[Y4 : $i]: ((sK1 @ Y4) | (~ (irel @ Y1 @ Y4)))))) | (~ (irel @ Y1 @ Y3))) | (sK2 @ Y3))) | (~ (irel @ Y0 @ Y1))))))))))))),
% 0.21/0.33 inference(beta-eta_normalization,[],[f86])).
% 0.21/0.33 thf(f88,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((sK1 @ Y2) | (~ (!! @ $i @ (^[Y4 : $i]: ((sK2 @ Y4) | (~ (irel @ Y1 @ Y4))))))) | (~ (irel @ Y1 @ Y2))) & (((~ (!! @ $i @ (^[Y4 : $i]: ((sK1 @ Y4) | (~ (irel @ Y1 @ Y4)))))) | (~ (irel @ Y1 @ Y3))) | (sK2 @ Y3))) | (~ (irel @ Y0 @ Y1))))))))))) @ sK3)) != (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((((~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))))) @ sK3)))),
% 0.21/0.33 inference(negative_extensionality,[],[f87])).
% 0.21/0.33 thf(f89,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((sK1 @ Y2) | (~ (!! @ $i @ (^[Y4 : $i]: ((sK2 @ Y4) | (~ (irel @ Y1 @ Y4))))))) | (~ (irel @ Y1 @ Y2))) & (((~ (!! @ $i @ (^[Y4 : $i]: ((sK1 @ Y4) | (~ (irel @ Y1 @ Y4)))))) | (~ (irel @ Y1 @ Y3))) | (sK2 @ Y3))) | (~ (irel @ Y0 @ Y1))))))))))) @ sK3)) = $true) | ($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((((~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))))) @ sK3)))),
% 0.21/0.33 inference(xor_proxy_clausification,[],[f88])).
% 0.21/0.33 thf(f90,plain,(
% 0.21/0.33 ($false = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((((~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))))) @ sK3))) | ((((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((((sK1 @ Y2) | (~ (!! @ $i @ (^[Y4 : $i]: ((sK2 @ Y4) | (~ (irel @ Y1 @ Y4))))))) | (~ (irel @ Y1 @ Y2))) & (((~ (!! @ $i @ (^[Y4 : $i]: ((sK1 @ Y4) | (~ (irel @ Y1 @ Y4)))))) | (~ (irel @ Y1 @ Y3))) | (sK2 @ Y3))) | (~ (irel @ Y0 @ Y1))))))))))) @ sK3)) = $false)),
% 0.21/0.33 inference(xor_proxy_clausification,[],[f88])).
% 0.21/0.33 thf(f91,plain,(
% 0.21/0.33 (((~ (!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))))) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0))))))))))))),
% 0.21/0.33 inference(beta-eta_normalization,[],[f90])).
% 0.21/0.33 thf(f92,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))))) = $true) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0))))))))))))),
% 0.21/0.33 inference(not_proxy_clausification,[],[f91])).
% 0.21/0.33 thf(f93,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0))))))))))))) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f92])).
% 0.21/0.33 thf(f94,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))))) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f93])).
% 0.21/0.33 thf(f95,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))) @ X2)) = $true) | ((((^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ X1)) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f94])).
% 0.21/0.33 thf(f96,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2))))))))) | ((((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK3 @ X1)))) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f95])).
% 0.21/0.33 thf(f97,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | ((((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK3 @ X1)))) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f96])).
% 0.21/0.33 thf(f98,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0))))))) = $true) | (((~ (irel @ sK3 @ X1))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f97])).
% 0.21/0.33 thf(f99,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((~ (irel @ sK3 @ X1))) = $true) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0)))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f98])).
% 0.21/0.33 thf(f100,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) | (((~ (irel @ sK3 @ X1))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f98])).
% 0.21/0.33 thf(f101,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))) = $true) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0))))))) = $true) | (((~ (irel @ sK3 @ X1))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f100])).
% 0.21/0.33 thf(f102,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))) @ X4)) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0))))))) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f101])).
% 0.21/0.33 thf(f103,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0))))))) = $true) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))) @ X4)) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f102])).
% 0.21/0.33 thf(f104,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))) = $false) | (((irel @ sK3 @ X1)) = $false) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))) @ X4)) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f103])).
% 0.21/0.33 thf(f105,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))) @ X4)) = $true) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK4 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f104])).
% 0.21/0.33 thf(f106,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))))) = $true) | ($false = (((sK2 @ (sK4 @ X1)) | (~ (irel @ X1 @ (sK4 @ X1)))))) | ((((~ (irel @ X1 @ X4)) | (sK1 @ X4))) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f105])).
% 0.21/0.33 thf(f107,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (((((~ (irel @ X1 @ X4)) | (sK1 @ X4))) = $true) | (((irel @ sK3 @ X1)) = $false) | ($false = (((sK2 @ (sK4 @ X1)) | (~ (irel @ X1 @ (sK4 @ X1)))))) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f106])).
% 0.21/0.33 thf(f108,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((~ (irel @ X1 @ X4))) = $true) | (((irel @ sK3 @ X1)) = $false) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true) | ($false = (((sK2 @ (sK4 @ X1)) | (~ (irel @ X1 @ (sK4 @ X1)))))) | (((sK1 @ X4)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f107])).
% 0.21/0.33 thf(f109,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ X4)) = $true) | ($false = (((sK2 @ (sK4 @ X1)) | (~ (irel @ X1 @ (sK4 @ X1)))))) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f108])).
% 0.21/0.33 thf(f111,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true) | (((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ X4)) = $true) | (((sK2 @ (sK4 @ X1))) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f109])).
% 0.21/0.33 thf(f112,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK1 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false) | ($true = ((((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))) | (~ (irel @ sK3 @ X2))))) | (((sK2 @ (sK4 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f111])).
% 0.21/0.33 thf(f113,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X1)) = $false) | (((~ (irel @ sK3 @ X2))) = $true) | (((sK1 @ X4)) = $true) | ($true = (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))))) | (((sK2 @ (sK4 @ X1))) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f112])).
% 0.21/0.33 thf(f114,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X4)) = $false) | (((sK2 @ (sK4 @ X1))) = $false) | ($true = (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))))) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f113])).
% 0.21/0.33 thf(f116,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ X4)) = $true) | (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3)))) = $true) | (((irel @ X1 @ X4)) = $false) | (((sK2 @ (sK4 @ X1))) = $false)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f114])).
% 0.21/0.33 thf(f117,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((~ (irel @ X2 @ X3))) = $true) | (((irel @ X1 @ X4)) = $false) | ((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))))) = $true) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ (sK4 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ X4)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f116])).
% 0.21/0.33 thf(f118,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X3))) | (((sK1 @ X4)) = $true) | ((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))))) = $true) | (((irel @ sK3 @ X1)) = $false) | (((sK2 @ (sK4 @ X1))) = $false) | (((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f117])).
% 0.21/0.33 thf(f119,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) = $true) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X4)) = $true) | (((sK2 @ (sK4 @ X1))) = $false) | (((sK1 @ X3)) = $true) | (((irel @ X1 @ X4)) = $false) | ($false = ((irel @ X2 @ X3)))) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f118])).
% 0.21/0.33 thf(f120,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ X4)) = $true) | (((sK1 @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ (sK4 @ X1))) = $false) | ($false = ((irel @ X2 @ X3)))) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f119])).
% 0.21/0.33 thf(f121,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK2 @ (sK4 @ X1))) = $false) | (((sK1 @ X3)) = $true) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))) @ (sK5 @ X2)))) | (((irel @ sK3 @ X1)) = $false) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X4)) = $true) | ($false = ((irel @ X2 @ X3))) | (((irel @ X1 @ X4)) = $false)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f120])).
% 0.21/0.33 thf(f122,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((sK2 @ (sK5 @ X2)) | (~ (irel @ X2 @ (sK5 @ X2))))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X3)) = $true) | (((sK1 @ X4)) = $true) | (((sK2 @ (sK4 @ X1))) = $false) | ($false = ((irel @ X2 @ X3)))) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f121])).
% 0.21/0.33 thf(f124,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK1 @ X4)) = $true) | (((irel @ sK3 @ X1)) = $false) | ($false = ((irel @ X2 @ X3))) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ (sK4 @ X1))) = $false) | ($false = ((sK2 @ (sK5 @ X2)))) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ X3)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f122])).
% 0.21/0.33 thf(f159,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0)))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f99])).
% 0.21/0.33 thf(f160,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0))))) = $true) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0))))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f159])).
% 0.21/0.33 thf(f161,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0))))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | (((irel @ sK3 @ X1)) = $false) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0))) @ X4)) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f160])).
% 0.21/0.33 thf(f162,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0))) @ X4)) = $true) | (((irel @ sK3 @ X1)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f161])).
% 0.21/0.33 thf(f163,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ X2 @ Y2))))))) | (~ (irel @ X2 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ X2 @ Y2)))))) | (~ (irel @ X2 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ X2)))))) @ X3)) = $true) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK2 @ Y0))) @ X4)) = $true) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK9 @ X1))) = $false)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f162])).
% 0.21/0.33 thf(f164,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((sK1 @ (sK9 @ X1)) | (~ (irel @ X1 @ (sK9 @ X1))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))))) = $true) | ((((~ (irel @ X1 @ X4)) | (sK2 @ X4))) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f163])).
% 0.21/0.33 thf(f166,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((sK1 @ (sK9 @ X1))) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))))) = $true) | ((((~ (irel @ X1 @ X4)) | (sK2 @ X4))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f164])).
% 0.21/0.33 thf(f167,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK1 @ (sK9 @ X1))) = $false) | ((((~ (irel @ X1 @ X4)) | (sK2 @ X4))) = $true) | (((irel @ sK3 @ X1)) = $false) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f166])).
% 0.21/0.33 thf(f168,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK2 @ X4)) = $true) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true) | (((~ (irel @ X1 @ X4))) = $true) | (((sK1 @ (sK9 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f167])).
% 0.21/0.33 thf(f169,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X4)) = $false) | (((sK1 @ (sK9 @ X1))) = $false) | (((sK2 @ X4)) = $true) | ((((^[Y0 : $i]: (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X2 @ Y1))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ X2 @ Y1)))))) | (~ (irel @ X2 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ X2)))) @ X5)) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f168])).
% 0.21/0.33 thf(f170,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | ($true = ((((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))) | (~ (irel @ sK3 @ X2))))) | (((sK1 @ (sK9 @ X1))) = $false) | (((sK2 @ X4)) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f169])).
% 0.21/0.33 thf(f171,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK2 @ X4)) = $true) | ($true = (((((sK1 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) | (~ (irel @ X2 @ X3))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))))) | (((~ (irel @ sK3 @ X2))) = $true) | (((sK1 @ (sK9 @ X1))) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f170])).
% 0.21/0.33 thf(f172,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK2 @ X4)) = $true) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5))) | (sK2 @ X5))) = $true) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ (sK9 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((~ (irel @ sK3 @ X2))) = $true)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f171])).
% 0.21/0.33 thf(f184,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK2 @ X5)) = $true) | (((sK2 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ (sK9 @ X1))) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ X2 @ X5)))) = $true) | (((~ (irel @ sK3 @ X2))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f172])).
% 0.21/0.33 thf(f185,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK1 @ (sK9 @ X1))) = $false) | (((~ (irel @ X2 @ X5))) = $true) | (((sK2 @ X5)) = $true) | (((irel @ X1 @ X4)) = $false) | (((sK2 @ X4)) = $true) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))))) | (((~ (irel @ sK3 @ X2))) = $true) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f184])).
% 0.21/0.33 thf(f186,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))))) | (((sK2 @ X5)) = $true) | (((sK2 @ X4)) = $true) | (((sK1 @ (sK9 @ X1))) = $false) | (((~ (irel @ sK3 @ X2))) = $true) | ($false = ((irel @ X2 @ X5))) | (((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f185])).
% 0.21/0.33 thf(f187,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ X2 @ X5))) | (((sK2 @ X4)) = $true) | (((irel @ sK3 @ X1)) = $false) | (((sK2 @ X5)) = $true) | (((irel @ X1 @ X4)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $false) | (((~ (irel @ sK3 @ X2))) = $true) | (((sK1 @ (sK9 @ X1))) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f186])).
% 0.21/0.33 thf(f188,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK1 @ (sK9 @ X1))) = $false) | (((~ (irel @ sK3 @ X2))) = $true) | (((sK2 @ X5)) = $true) | (((irel @ sK3 @ X1)) = $false) | ($false = ((irel @ X2 @ X5))) | (((irel @ X1 @ X4)) = $false) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))) @ (sK11 @ X2))) = $false) | (((sK2 @ X4)) = $true)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f187])).
% 0.21/0.33 thf(f189,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK2 @ X4)) = $true) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))) @ (sK11 @ X2))) = $false) | (((sK2 @ X5)) = $true) | (((sK1 @ (sK9 @ X1))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | ($false = ((irel @ X2 @ X5))) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f188])).
% 0.21/0.33 thf(f190,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X4)) = $false) | ((((sK1 @ (sK11 @ X2)) | (~ (irel @ X2 @ (sK11 @ X2))))) = $false) | (((irel @ sK3 @ X1)) = $false) | ($false = ((irel @ X2 @ X5))) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ X4)) = $true) | (((sK1 @ (sK9 @ X1))) = $false) | (((sK2 @ X5)) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f189])).
% 0.21/0.33 thf(f192,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK2 @ X5)) = $true) | ($false = ((irel @ X2 @ X5))) | (((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ (sK9 @ X1))) = $false) | (((sK1 @ (sK11 @ X2))) = $false) | (((sK2 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f190])).
% 0.21/0.33 thf(f222,plain,(
% 0.21/0.33 ($true = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))))))) | (((~ (!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))))) = $true)),
% 0.21/0.33 inference(beta-eta_normalization,[],[f89])).
% 0.21/0.33 thf(f223,plain,(
% 0.21/0.33 (((~ (!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))))) = $false)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f222])).
% 0.21/0.33 thf(f224,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))))) = $false)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f223])).
% 0.21/0.33 thf(f225,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))) @ sK14)) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f224])).
% 0.21/0.33 thf(f226,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((((sK1 @ Y1) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y0 @ Y3))))))) | (~ (irel @ Y0 @ Y1))) & (((~ (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y0 @ Y3)))))) | (~ (irel @ Y0 @ Y2))) | (sK2 @ Y2))) | (~ (irel @ sK3 @ Y0)))))))) @ sK14)) = $false) | ((((^[Y0 : $i]: ((((~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ sK15)) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f225])).
% 0.21/0.33 thf(f227,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))))) = $false) | ((((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK3 @ sK15)))) = $false)),
% 0.21/0.33 inference(beta-eta_normalization,[],[f226])).
% 0.21/0.33 thf(f228,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | ((((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) | (~ (irel @ sK3 @ sK15)))) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f227])).
% 0.21/0.33 thf(f230,plain,(
% 0.21/0.33 ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f228])).
% 0.21/0.33 thf(f231,plain,(
% 0.21/0.33 ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0)))))) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)),
% 0.21/0.33 inference(and_proxy_clausification,[],[f230])).
% 0.21/0.33 thf(f232,plain,(
% 0.21/0.33 ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f231])).
% 0.21/0.33 thf(f233,plain,(
% 0.21/0.33 ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0)))))) = $false) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0))))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f231])).
% 0.21/0.33 thf(f234,plain,(
% 0.21/0.33 (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0))))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f233])).
% 0.21/0.33 thf(f235,plain,(
% 0.21/0.33 (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0))))))) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f233])).
% 0.21/0.33 thf(f236,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) = $true)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f235])).
% 0.21/0.33 thf(f237,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) = $true)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f236])).
% 0.21/0.33 thf(f238,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))) @ X1)) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f237])).
% 0.21/0.33 thf(f239,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))) @ X2)) = $true) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK15 @ Y0)))) @ X1)) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f238])).
% 0.21/0.33 thf(f240,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (((((sK1 @ X1) | (~ (irel @ sK15 @ X1)))) = $true) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false) | ((((sK2 @ X2) | (~ (irel @ sK15 @ X2)))) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f239])).
% 0.21/0.33 thf(f241,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false) | ((((sK2 @ X2) | (~ (irel @ sK15 @ X2)))) = $true) | (((~ (irel @ sK15 @ X1))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f240])).
% 0.21/0.33 thf(f242,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK15 @ X1))) = $true) | (((sK1 @ X1)) = $true) | ((((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK17)) = $false) | ((((sK2 @ X2) | (~ (irel @ sK15 @ X2)))) = $true)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f241])).
% 0.21/0.33 thf(f243,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true) | ((((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK17)) = $false) | ((((sK2 @ X2) | (~ (irel @ sK15 @ X2)))) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f242])).
% 0.21/0.33 thf(f244,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | ((((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK17)) = $false) | (((sK2 @ X2)) = $true) | (((~ (irel @ sK15 @ X2))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f243])).
% 0.21/0.33 thf(f245,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK17)) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f244])).
% 0.21/0.33 thf(f246,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (($false = ((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) | (~ (irel @ sK3 @ sK14))))) | (((sK1 @ X1)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f245])).
% 0.21/0.33 thf(f248,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X2)) = $false) | (((sK1 @ X1)) = $true) | ((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17)))) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f246])).
% 0.21/0.33 thf(f249,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((sK2 @ X2)) = $true) | (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16)))) = $false) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) = $false)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f248])).
% 0.21/0.33 thf(f251,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) = $false) | (((sK1 @ X1)) = $true) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f249])).
% 0.21/0.33 thf(f252,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) = $false) | (((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f251])).
% 0.21/0.33 thf(f253,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X2)) = $false) | (((sK1 @ X1)) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) = $false) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f251])).
% 0.21/0.33 thf(f255,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X2)) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17)))) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f253])).
% 0.21/0.33 thf(f257,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f255])).
% 0.21/0.33 thf(f258,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((sK1 @ sK16)) = $false) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f257])).
% 0.21/0.33 thf(f259,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((sK1 @ sK16)) = $false) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X3)) = $true) | (((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f258])).
% 0.21/0.33 thf(f260,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true) | (((sK1 @ sK16)) = $false) | ((((sK1 @ X3) | (~ (irel @ sK14 @ X3)))) = $true)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f259])).
% 0.21/0.33 thf(f261,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((~ (irel @ sK14 @ X3))) = $true) | (((sK2 @ X2)) = $true) | (((sK1 @ sK16)) = $false) | (((sK1 @ X3)) = $true) | (((irel @ sK15 @ X2)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f260])).
% 0.21/0.33 thf(f262,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((sK1 @ sK16)) = $false) | (((sK1 @ X3)) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK14 @ X3)) = $false) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f261])).
% 0.21/0.33 thf(f264,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17))) | (sK2 @ sK17))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f252])).
% 0.21/0.33 thf(f266,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK17)))) = $false) | (((sK1 @ X1)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((sK2 @ X2)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f264])).
% 0.21/0.33 thf(f268,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((irel @ sK15 @ X2)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((sK2 @ X2)) = $true) | (((sK1 @ X1)) = $true) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0))))))))) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f266])).
% 0.21/0.33 thf(f269,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) | (((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X3)) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f268])).
% 0.21/0.33 thf(f270,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((irel @ sK15 @ X1)) = $false) | (((irel @ sK15 @ X2)) = $false) | (((sK2 @ X2)) = $true) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X3)) = $true) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f269])).
% 0.21/0.33 thf(f271,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X4)) = $true) | (((irel @ sK15 @ X2)) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X3)) = $true) | (((sK2 @ X2)) = $true)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f270])).
% 0.21/0.33 thf(f272,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((sK1 @ X4) | (~ (irel @ sK14 @ X4)))) = $true) | (((sK1 @ X1)) = $true) | ((((sK2 @ X3) | (~ (irel @ sK14 @ X3)))) = $true) | (((irel @ sK15 @ X2)) = $false) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f271])).
% 0.21/0.33 thf(f273,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | ((((sK2 @ X3) | (~ (irel @ sK14 @ X3)))) = $true) | (((~ (irel @ sK14 @ X4))) = $true) | (((sK1 @ X4)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f272])).
% 0.21/0.33 thf(f274,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK2 @ X3)) = $true) | (((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((~ (irel @ sK14 @ X3))) = $true) | (((~ (irel @ sK14 @ X4))) = $true) | (((sK1 @ X4)) = $true) | (((sK1 @ X1)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f273])).
% 0.21/0.33 thf(f275,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK15 @ X2)) = $false) | (((sK1 @ X1)) = $true) | (((~ (irel @ sK14 @ X4))) = $true) | (((sK2 @ X2)) = $true) | (((sK2 @ X3)) = $true) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X4)) = $true) | (((irel @ sK14 @ X3)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f274])).
% 0.21/0.33 thf(f276,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK2 @ X3)) = $true) | (((sK1 @ X1)) = $true) | (((irel @ sK14 @ X3)) = $false) | (((irel @ sK15 @ X2)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X2)) = $true) | (((sK1 @ X4)) = $true) | ($false = ((irel @ sK14 @ X4)))) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f275])).
% 0.21/0.33 thf(f299,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) = $false)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f234])).
% 0.21/0.33 thf(f300,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))) @ X1))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f299])).
% 0.21/0.33 thf(f301,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ sK18)) = $false) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK15 @ Y0)))) @ X1))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false)) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f300])).
% 0.21/0.33 thf(f302,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false) | ($false = (((~ (irel @ sK15 @ sK18)) | (sK2 @ sK18)))) | ($true = (((sK2 @ X1) | (~ (irel @ sK15 @ X1)))))) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f301])).
% 0.21/0.33 thf(f303,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (($true = (((sK2 @ X1) | (~ (irel @ sK15 @ X1))))) | ($false = (((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK19))) | ($false = (((~ (irel @ sK15 @ sK18)) | (sK2 @ sK18))))) )),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f302])).
% 0.21/0.33 thf(f304,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true) | (((~ (irel @ sK15 @ X1))) = $true) | ($false = (((~ (irel @ sK15 @ sK18)) | (sK2 @ sK18)))) | ($false = (((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK19)))) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f303])).
% 0.21/0.33 thf(f305,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true) | ($false = (((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK19))) | ($false = (((~ (irel @ sK15 @ sK18)) | (sK2 @ sK18)))) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f304])).
% 0.21/0.33 thf(f306,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ sK18)) = $false) | ($false = (((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK19))) | (((sK2 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f305])).
% 0.21/0.33 thf(f365,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19))) | (sK2 @ sK19))) | (~ (irel @ sK3 @ sK14)))) = $false) | (((sK2 @ X1)) = $true) | (((sK2 @ sK18)) = $false) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f306])).
% 0.21/0.33 thf(f367,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ sK18)) = $false) | (((irel @ sK15 @ X1)) = $false) | ((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19))) | (sK2 @ sK19)))) = $false) | (((sK2 @ X1)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f365])).
% 0.21/0.33 thf(f368,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19))) | (sK2 @ sK19)))) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ X1)) = $true) | (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16)))) = $false) | (((sK2 @ sK18)) = $false)) )),
% 0.21/0.33 inference(and_proxy_clausification,[],[f367])).
% 0.21/0.33 thf(f370,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true) | (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16)))) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19)))) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK2 @ sK18)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f368])).
% 0.21/0.33 thf(f372,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) = $false) | (((sK2 @ sK18)) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19)))) = $false) | (((sK2 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f370])).
% 0.21/0.33 thf(f374,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ X1)) = $true) | (((sK2 @ sK18)) = $false) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK19)))) = $false) | (((sK1 @ sK16)) = $false) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f372])).
% 0.21/0.33 thf(f376,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((sK1 @ sK16)) = $false) | (((sK2 @ sK18)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) | (((sK2 @ X1)) = $true)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f374])).
% 0.21/0.33 thf(f377,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((sK2 @ sK18)) = $false) | (((sK2 @ X1)) = $true) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f376])).
% 0.21/0.33 thf(f378,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK2 @ sK18)) = $false) | (((sK2 @ X1)) = $true) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X2)) = $true) | (((sK1 @ sK16)) = $false) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f377])).
% 0.21/0.33 thf(f379,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((sK2 @ sK18)) = $false) | (((sK2 @ X1)) = $true) | ((((sK1 @ X2) | (~ (irel @ sK14 @ X2)))) = $true) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f378])).
% 0.21/0.33 thf(f380,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK14 @ X2))) = $true) | (((sK2 @ X1)) = $true) | (((sK1 @ sK16)) = $false) | (((sK2 @ sK18)) = $false) | (((sK1 @ X2)) = $true) | (((irel @ sK15 @ X1)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f379])).
% 0.21/0.33 thf(f381,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i] : ((((irel @ sK14 @ X2)) = $false) | (((sK2 @ sK18)) = $false) | (((irel @ sK15 @ X1)) = $false) | (((sK1 @ X2)) = $true) | (((sK2 @ X1)) = $true) | (((sK1 @ sK16)) = $false)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f380])).
% 0.21/0.33 thf(f421,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))))) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f232])).
% 0.21/0.33 thf(f538,plain,(
% 0.21/0.33 ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ sK23))) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))))) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f421])).
% 0.21/0.33 thf(f539,plain,(
% 0.21/0.33 ($false = (((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK1 @ Y0))) @ sK23))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((((sK1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ sK14 @ Y2))))))) | (~ (irel @ sK14 @ Y0))) & (((~ (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ sK14 @ Y2)))))) | (~ (irel @ sK14 @ Y1))) | (sK2 @ Y1))) | (~ (irel @ sK3 @ sK14)))))) @ sK16)) = $false) | ((((^[Y0 : $i]: ((~ (irel @ sK15 @ Y0)) | (sK2 @ Y0))) @ sK24)) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f538])).
% 0.21/0.33 thf(f540,plain,(
% 0.21/0.33 ((((~ (irel @ sK15 @ sK23)) | (sK1 @ sK23))) = $false) | ((((~ (irel @ sK15 @ sK24)) | (sK2 @ sK24))) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false)),
% 0.21/0.33 inference(beta-eta_normalization,[],[f539])).
% 0.21/0.33 thf(f541,plain,(
% 0.21/0.33 ((((~ (irel @ sK15 @ sK24)) | (sK2 @ sK24))) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false) | (((sK1 @ sK23)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f540])).
% 0.21/0.33 thf(f657,plain,(
% 0.21/0.33 (((sK2 @ sK24)) = $false) | (((!! @ $i @ (^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))))) = $false) | (((sK1 @ sK23)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f541])).
% 0.21/0.33 thf(f717,plain,(
% 0.21/0.33 (((sK1 @ sK23)) = $false) | (((sK2 @ sK24)) = $false) | ((((^[Y0 : $i]: (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK14 @ Y1))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ sK14 @ Y1)))))) | (~ (irel @ sK14 @ Y0))) | (sK2 @ Y0))) | (~ (irel @ sK3 @ sK14)))) @ sK28)) = $false)),
% 0.21/0.33 inference(sigma_proxy_clausification,[],[f657])).
% 0.21/0.33 thf(f718,plain,(
% 0.21/0.33 (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false) | ($false = ((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK28))) | (sK2 @ sK28))) | (~ (irel @ sK3 @ sK14)))))),
% 0.21/0.33 inference(beta-eta_normalization,[],[f717])).
% 0.21/0.33 thf(f720,plain,(
% 0.21/0.33 ((((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16))) & (((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK28))) | (sK2 @ sK28)))) = $false) | (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f718])).
% 0.21/0.33 thf(f721,plain,(
% 0.21/0.33 (((((~ (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK14 @ Y0)))))) | (~ (irel @ sK14 @ sK28))) | (sK2 @ sK28))) = $false) | (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false) | (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16)))) = $false)),
% 0.21/0.33 inference(and_proxy_clausification,[],[f720])).
% 0.21/0.33 thf(f722,plain,(
% 0.21/0.33 (((sK2 @ sK24)) = $false) | (((sK2 @ sK28)) = $false) | (((sK1 @ sK23)) = $false) | (((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) | (~ (irel @ sK14 @ sK16)))) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f721])).
% 0.21/0.33 thf(f763,plain,(
% 0.21/0.33 (((sK2 @ sK24)) = $false) | ((((sK1 @ sK16) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))))) = $false) | (((sK2 @ sK28)) = $false) | (((sK1 @ sK23)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f722])).
% 0.21/0.33 thf(f764,plain,(
% 0.21/0.33 (((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0))))))) = $false) | (((sK2 @ sK28)) = $false) | (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f763])).
% 0.21/0.33 thf(f765,plain,(
% 0.21/0.33 (((sK2 @ sK28)) = $false) | (((sK1 @ sK16)) = $false) | (((sK1 @ sK23)) = $false) | (((sK2 @ sK24)) = $false)),
% 0.21/0.33 inference(or_proxy_clausification,[],[f763])).
% 0.21/0.33 thf(f766,plain,(
% 0.21/0.33 (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))))) = $true) | (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false) | (((sK2 @ sK28)) = $false)),
% 0.21/0.33 inference(not_proxy_clausification,[],[f764])).
% 0.21/0.33 thf(f767,plain,(
% 0.21/0.33 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK14 @ Y0)))) @ X1)) = $true) | (((sK1 @ sK23)) = $false) | (((sK2 @ sK28)) = $false) | (((sK2 @ sK24)) = $false)) )),
% 0.21/0.33 inference(pi_proxy_clausification,[],[f766])).
% 0.21/0.33 thf(f768,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK1 @ sK23)) = $false) | (((sK2 @ sK28)) = $false) | (((sK2 @ sK24)) = $false) | ($true = (((sK2 @ X1) | (~ (irel @ sK14 @ X1)))))) )),
% 0.21/0.33 inference(beta-eta_normalization,[],[f767])).
% 0.21/0.33 thf(f769,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((~ (irel @ sK14 @ X1))) = $true) | (((sK2 @ sK24)) = $false) | (((sK2 @ X1)) = $true) | (((sK2 @ sK28)) = $false) | (((sK1 @ sK23)) = $false)) )),
% 0.21/0.33 inference(or_proxy_clausification,[],[f768])).
% 0.21/0.33 thf(f770,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK2 @ sK28)) = $false) | (((irel @ sK14 @ X1)) = $false) | (((sK2 @ sK24)) = $false) | (((sK1 @ sK23)) = $false) | (((sK2 @ X1)) = $true)) )),
% 0.21/0.33 inference(not_proxy_clausification,[],[f769])).
% 0.21/0.33 thf(f830,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK1 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false) | ($false = ((irel @ X2 @ X3))) | (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (sK5 @ X2)))) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.21/0.33 inference(forward_demodulation,[],[f124,f59])).
% 0.21/0.33 thf(f840,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X5))) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | (((irel @ sK3 @ X1)) = $false) | (((sK1 @ (sK11 @ X2))) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK2 @ X4)) = $true) | (((sK2 @ X5)) = $true)) )),
% 0.21/0.33 inference(forward_demodulation,[],[f192,f59])).
% 0.21/0.33 thf(f847,definition,(
% 0.21/0.33 spl30_1 <=> ! [X2 : $i] : ((((sK2 @ X2)) = $true) | (((irel @ sK15 @ X2)) = $false))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition])).
% 0.21/0.33 thf(f848,plain,(
% 0.21/0.33 ( ! [X2 : $i] : ((((irel @ sK15 @ X2)) = $false) | (((sK2 @ X2)) = $true)) ) | ~spl30_1),
% 0.21/0.33 inference(avatar_component_clause,[],[f847])).
% 0.21/0.33 thf(f850,definition,(
% 0.21/0.33 spl30_2 <=> ! [X3 : $i] : ((((sK1 @ X3)) = $true) | (((irel @ sK14 @ X3)) = $false))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition])).
% 0.21/0.33 thf(f851,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((irel @ sK14 @ X3)) = $false) | (((sK1 @ X3)) = $true)) ) | ~spl30_2),
% 0.21/0.33 inference(avatar_component_clause,[],[f850])).
% 0.21/0.33 thf(f853,definition,(
% 0.21/0.33 spl30_3 <=> (((sK1 @ sK16)) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition])).
% 0.21/0.33 thf(f855,plain,(
% 0.21/0.33 (((sK1 @ sK16)) = $false) | ~spl30_3),
% 0.21/0.33 inference(avatar_component_clause,[],[f853])).
% 0.21/0.33 thf(f857,definition,(
% 0.21/0.33 spl30_4 <=> ! [X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | (((sK1 @ X1)) = $true))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition])).
% 0.21/0.33 thf(f858,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK15 @ X1)) = $false)) ) | ~spl30_4),
% 0.21/0.33 inference(avatar_component_clause,[],[f857])).
% 0.21/0.33 thf(f859,plain,(
% 0.21/0.33 spl30_1 | spl30_2 | spl30_3 | spl30_4),
% 0.21/0.33 inference(avatar_split_clause,[],[f262,f857,f853,f850,f847])).
% 0.21/0.33 thf(f871,definition,(
% 0.21/0.33 spl30_7 <=> ! [X3 : $i] : ((((sK2 @ X3)) = $true) | (((irel @ sK14 @ X3)) = $false))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition])).
% 0.21/0.33 thf(f872,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((sK2 @ X3)) = $true) | (((irel @ sK14 @ X3)) = $false)) ) | ~spl30_7),
% 0.21/0.33 inference(avatar_component_clause,[],[f871])).
% 0.21/0.33 thf(f873,plain,(
% 0.21/0.33 spl30_2 | spl30_7 | spl30_4 | spl30_1),
% 0.21/0.33 inference(avatar_split_clause,[],[f276,f847,f857,f871,f850])).
% 0.21/0.33 thf(f884,definition,(
% 0.21/0.33 spl30_9 <=> (((irel @ sK3 @ sK14)) = $true)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition])).
% 0.21/0.33 thf(f885,plain,(
% 0.21/0.33 (((irel @ sK3 @ sK14)) != $true) | spl30_9),
% 0.21/0.33 inference(avatar_component_clause,[],[f884])).
% 0.21/0.33 thf(f886,plain,(
% 0.21/0.33 (((irel @ sK3 @ sK14)) = $true) | ~spl30_9),
% 0.21/0.33 inference(avatar_component_clause,[],[f884])).
% 0.21/0.33 thf(f911,definition,(
% 0.21/0.33 spl30_13 <=> (((sK2 @ sK18)) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition])).
% 0.21/0.33 thf(f913,plain,(
% 0.21/0.33 (((sK2 @ sK18)) = $false) | ~spl30_13),
% 0.21/0.33 inference(avatar_component_clause,[],[f911])).
% 0.21/0.33 thf(f914,plain,(
% 0.21/0.33 spl30_3 | spl30_1 | spl30_2 | spl30_13),
% 0.21/0.33 inference(avatar_split_clause,[],[f381,f911,f850,f847,f853])).
% 0.21/0.33 thf(f995,definition,(
% 0.21/0.33 spl30_24 <=> (((sK2 @ sK24)) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition])).
% 0.21/0.33 thf(f997,plain,(
% 0.21/0.33 (((sK2 @ sK24)) = $false) | ~spl30_24),
% 0.21/0.33 inference(avatar_component_clause,[],[f995])).
% 0.21/0.33 thf(f1017,definition,(
% 0.21/0.33 spl30_27 <=> (((sK1 @ sK23)) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_27])],[avatar_definition])).
% 0.21/0.33 thf(f1019,plain,(
% 0.21/0.33 (((sK1 @ sK23)) = $false) | ~spl30_27),
% 0.21/0.33 inference(avatar_component_clause,[],[f1017])).
% 0.21/0.33 thf(f1049,definition,(
% 0.21/0.33 spl30_31 <=> (((sK2 @ sK28)) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_31])],[avatar_definition])).
% 0.21/0.33 thf(f1051,plain,(
% 0.21/0.33 (((sK2 @ sK28)) = $false) | ~spl30_31),
% 0.21/0.33 inference(avatar_component_clause,[],[f1049])).
% 0.21/0.33 thf(f1052,plain,(
% 0.21/0.33 spl30_24 | spl30_3 | spl30_27 | spl30_31),
% 0.21/0.33 inference(avatar_split_clause,[],[f765,f1049,f1017,f853,f995])).
% 0.21/0.33 thf(f1053,plain,(
% 0.21/0.33 spl30_31 | spl30_27 | spl30_24 | spl30_7),
% 0.21/0.33 inference(avatar_split_clause,[],[f770,f871,f995,f1017,f1049])).
% 0.21/0.33 thf(f1078,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X3)) = $true) | (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false) | (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false) | (((sK1 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false) | ($false = ((irel @ X2 @ X3)))) )),
% 0.21/0.33 inference(forward_demodulation,[],[f830,f59])).
% 0.21/0.33 thf(f1079,plain,(
% 0.21/0.33 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X3)) = $true) | (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false) | ($false = ((irel @ X2 @ X3)))) )),
% 0.21/0.33 inference(duplicate_literal_removal,[],[f1078])).
% 0.21/0.33 thf(f1089,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | (((irel @ sK3 @ X1)) = $false) | ($false = ((irel @ X2 @ X5))) | (((sK2 @ X5)) = $true) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ X4)) = $true)) )),
% 0.21/0.33 inference(forward_demodulation,[],[f840,f59])).
% 0.21/0.33 thf(f1090,plain,(
% 0.21/0.33 ( ! [X2 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK2 @ X4)) = $true) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | (((sK2 @ X5)) = $true) | ($false = ((irel @ X2 @ X5))) | (((irel @ sK3 @ X1)) = $false)) )),
% 0.21/0.33 inference(duplicate_literal_removal,[],[f1089])).
% 0.21/0.33 thf(f1097,definition,(
% 0.21/0.33 spl30_35 <=> ! [X4 : $i,X1 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((sK1 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_35])],[avatar_definition])).
% 0.21/0.33 thf(f1098,plain,(
% 0.21/0.33 ( ! [X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | (((sK1 @ X4)) = $true)) ) | ~spl30_35),
% 0.21/0.33 inference(avatar_component_clause,[],[f1097])).
% 0.21/0.33 thf(f1100,definition,(
% 0.21/0.33 spl30_36 <=> (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_36])],[avatar_definition])).
% 0.21/0.33 thf(f1102,plain,(
% 0.21/0.33 (((sK2 @ (d2unsorted @ d_unsorted_0))) = $false) | ~spl30_36),
% 0.21/0.33 inference(avatar_component_clause,[],[f1100])).
% 0.21/0.33 thf(f1103,plain,(
% 0.21/0.33 spl30_35 | spl30_36 | spl30_35),
% 0.21/0.33 inference(avatar_split_clause,[],[f1079,f1097,f1100,f1097])).
% 0.21/0.33 thf(f1109,definition,(
% 0.21/0.33 spl30_38 <=> (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false)),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_38])],[avatar_definition])).
% 0.21/0.33 thf(f1111,plain,(
% 0.21/0.33 (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | ~spl30_38),
% 0.21/0.33 inference(avatar_component_clause,[],[f1109])).
% 0.21/0.33 thf(f1113,definition,(
% 0.21/0.33 spl30_39 <=> ! [X2 : $i,X5 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((sK2 @ X5)) = $true) | ($false = ((irel @ X2 @ X5))))),
% 0.21/0.33 introduced(definition,[new_symbols(definition,[spl30_39])],[avatar_definition])).
% 0.21/0.33 thf(f1114,plain,(
% 0.21/0.33 ( ! [X2 : $i,X5 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((sK2 @ X5)) = $true) | ($false = ((irel @ X2 @ X5)))) ) | ~spl30_39),
% 0.21/0.33 inference(avatar_component_clause,[],[f1113])).
% 0.21/0.33 thf(f1126,plain,(
% 0.21/0.33 spl30_39 | spl30_39 | spl30_38),
% 0.21/0.33 inference(avatar_split_clause,[],[f1090,f1109,f1113,f1113])).
% 0.21/0.33 thf(f1135,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((sK1 @ X0)) = $false)) ) | ~spl30_38),
% 0.21/0.33 inference(constrained_superposition,[],[f1111,f59])).
% 0.21/0.33 thf(f1142,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((irel @ sK3 @ X0)) = $true)) ) | ~spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f886,f63])).
% 0.21/0.33 thf(f1146,plain,(
% 0.21/0.33 ( ! [X1 : $i,X4 : $i] : ((((irel @ sK3 @ X1)) = $false) | (((irel @ X1 @ X4)) = $false) | ($true = $false)) ) | (~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f1098,f1135])).
% 0.21/0.33 thf(f1147,plain,(
% 0.21/0.33 ( ! [X1 : $i,X4 : $i] : ((((irel @ X1 @ X4)) = $false) | (((irel @ sK3 @ X1)) = $false)) ) | (~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1146])).
% 0.21/0.33 thf(f1148,plain,(
% 0.21/0.33 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f1142,f63])).
% 0.21/0.33 thf(f1152,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK3 @ X1)) = $false) | ($true = $false)) ) | (~spl30_9 | ~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f1147,f1148])).
% 0.21/0.33 thf(f1153,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK3 @ X1)) = $false)) ) | (~spl30_9 | ~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1152])).
% 0.21/0.33 thf(f1154,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_9 | ~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f1153,f1148])).
% 0.21/0.33 thf(f1155,plain,(
% 0.21/0.33 $false | (~spl30_9 | ~spl30_35 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1154])).
% 0.21/0.33 thf(f1156,plain,(
% 0.21/0.33 ~spl30_9 | ~spl30_35 | ~spl30_38),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1155])).
% 0.21/0.33 thf(f1157,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK15 @ X1)) = $false) | ($true = $false)) ) | (~spl30_4 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f858,f1135])).
% 0.21/0.33 thf(f1158,plain,(
% 0.21/0.33 ( ! [X1 : $i] : ((((irel @ sK15 @ X1)) = $false)) ) | (~spl30_4 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1157])).
% 0.21/0.33 thf(f1159,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((sK2 @ X0)) = $false)) ) | ~spl30_13),
% 0.21/0.33 inference(constrained_superposition,[],[f913,f63])).
% 0.21/0.33 thf(f1169,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((irel @ sK3 @ X0)) != $true)) ) | spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f885,f63])).
% 0.21/0.33 thf(f1177,plain,(
% 0.21/0.33 ($true != $true) | spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f1169,f77])).
% 0.21/0.33 thf(f1180,plain,(
% 0.21/0.33 $false | spl30_9),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1177])).
% 0.21/0.33 thf(f1181,plain,(
% 0.21/0.33 spl30_9),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1180])).
% 0.21/0.33 thf(f1182,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((irel @ sK3 @ X0)) = $true)) ) | ~spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f886,f63])).
% 0.21/0.33 thf(f1186,plain,(
% 0.21/0.33 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl30_9),
% 0.21/0.33 inference(constrained_superposition,[],[f1182,f63])).
% 0.21/0.33 thf(f1190,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_4 | ~spl30_9 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f1158,f1186])).
% 0.21/0.33 thf(f1191,plain,(
% 0.21/0.33 $false | (~spl30_4 | ~spl30_9 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1190])).
% 0.21/0.33 thf(f1192,plain,(
% 0.21/0.33 ~spl30_4 | ~spl30_9 | ~spl30_38),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1191])).
% 0.21/0.33 thf(f1193,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((irel @ sK14 @ X3)) = $false) | ($true = $false)) ) | (~spl30_7 | ~spl30_13)),
% 0.21/0.33 inference(forward_demodulation,[],[f872,f1159])).
% 0.21/0.33 thf(f1194,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((irel @ sK14 @ X3)) = $false)) ) | (~spl30_7 | ~spl30_13)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1193])).
% 0.21/0.33 thf(f1195,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_7 | ~spl30_9 | ~spl30_13)),
% 0.21/0.33 inference(forward_demodulation,[],[f1194,f1186])).
% 0.21/0.33 thf(f1196,plain,(
% 0.21/0.33 $false | (~spl30_7 | ~spl30_9 | ~spl30_13)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1195])).
% 0.21/0.33 thf(f1197,plain,(
% 0.21/0.33 ~spl30_7 | ~spl30_9 | ~spl30_13),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1196])).
% 0.21/0.33 thf(f1198,plain,(
% 0.21/0.33 ( ! [X3 : $i] : (($true = $false) | (((sK2 @ X3)) = $true)) ) | (~spl30_7 | ~spl30_9)),
% 0.21/0.33 inference(forward_demodulation,[],[f872,f1186])).
% 0.21/0.33 thf(f1199,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((sK2 @ X3)) = $true)) ) | (~spl30_7 | ~spl30_9)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1198])).
% 0.21/0.33 thf(f1208,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_7 | ~spl30_9 | ~spl30_36)),
% 0.21/0.33 inference(forward_demodulation,[],[f1102,f1199])).
% 0.21/0.33 thf(f1209,plain,(
% 0.21/0.33 $false | (~spl30_7 | ~spl30_9 | ~spl30_36)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1208])).
% 0.21/0.33 thf(f1210,plain,(
% 0.21/0.33 ~spl30_7 | ~spl30_9 | ~spl30_36),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1209])).
% 0.21/0.33 thf(f1211,plain,(
% 0.21/0.33 ( ! [X1 : $i,X4 : $i] : ((((sK1 @ X4)) = $true) | (((irel @ X1 @ X4)) = $false) | ($true = $false)) ) | (~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(forward_demodulation,[],[f1098,f1186])).
% 0.21/0.33 thf(f1212,plain,(
% 0.21/0.33 ( ! [X1 : $i,X4 : $i] : ((((irel @ X1 @ X4)) = $false) | (((sK1 @ X4)) = $true)) ) | (~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1211])).
% 0.21/0.33 thf(f1214,plain,(
% 0.21/0.33 ( ! [X4 : $i] : (($true = $false) | (((sK1 @ X4)) = $true)) ) | (~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(forward_demodulation,[],[f1212,f1186])).
% 0.21/0.33 thf(f1215,plain,(
% 0.21/0.33 ( ! [X4 : $i] : ((((sK1 @ X4)) = $true)) ) | (~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1214])).
% 0.21/0.33 thf(f1216,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_3 | ~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(forward_demodulation,[],[f855,f1215])).
% 0.21/0.33 thf(f1217,plain,(
% 0.21/0.33 $false | (~spl30_3 | ~spl30_9 | ~spl30_35)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1216])).
% 0.21/0.33 thf(f1218,plain,(
% 0.21/0.33 ~spl30_3 | ~spl30_9 | ~spl30_35),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1217])).
% 0.21/0.33 thf(f1220,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_9 | ~spl30_27 | ~spl30_35)),
% 0.21/0.33 inference(forward_demodulation,[],[f1019,f1215])).
% 0.21/0.33 thf(f1221,plain,(
% 0.21/0.33 $false | (~spl30_9 | ~spl30_27 | ~spl30_35)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1220])).
% 0.21/0.33 thf(f1222,plain,(
% 0.21/0.33 ~spl30_9 | ~spl30_27 | ~spl30_35),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1221])).
% 0.21/0.33 thf(f1234,plain,(
% 0.21/0.33 ( ! [X2 : $i] : ((((sK2 @ X2)) = $true) | ($true = $false)) ) | (~spl30_1 | ~spl30_9)),
% 0.21/0.33 inference(forward_demodulation,[],[f848,f1186])).
% 0.21/0.33 thf(f1235,plain,(
% 0.21/0.33 ( ! [X2 : $i] : ((((sK2 @ X2)) = $true)) ) | (~spl30_1 | ~spl30_9)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1234])).
% 0.21/0.33 thf(f1237,plain,(
% 0.21/0.33 ( ! [X2 : $i,X5 : $i] : (($false = ((irel @ X2 @ X5))) | ($true = $false) | (((sK2 @ X5)) = $true)) ) | (~spl30_9 | ~spl30_39)),
% 0.21/0.33 inference(forward_demodulation,[],[f1114,f1186])).
% 0.21/0.33 thf(f1238,plain,(
% 0.21/0.33 ( ! [X2 : $i,X5 : $i] : (($false = ((irel @ X2 @ X5))) | (((sK2 @ X5)) = $true)) ) | (~spl30_9 | ~spl30_39)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1237])).
% 0.21/0.33 thf(f1239,plain,(
% 0.21/0.33 ( ! [X5 : $i] : ((((sK2 @ X5)) = $true) | ($true = $false)) ) | (~spl30_9 | ~spl30_39)),
% 0.21/0.33 inference(forward_demodulation,[],[f1238,f1186])).
% 0.21/0.33 thf(f1240,plain,(
% 0.21/0.33 ( ! [X5 : $i] : ((((sK2 @ X5)) = $true)) ) | (~spl30_9 | ~spl30_39)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1239])).
% 0.21/0.33 thf(f1246,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_9 | ~spl30_31 | ~spl30_39)),
% 0.21/0.33 inference(forward_demodulation,[],[f1051,f1240])).
% 0.21/0.33 thf(f1247,plain,(
% 0.21/0.33 $false | (~spl30_9 | ~spl30_31 | ~spl30_39)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1246])).
% 0.21/0.33 thf(f1248,plain,(
% 0.21/0.33 ~spl30_9 | ~spl30_31 | ~spl30_39),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1247])).
% 0.21/0.33 thf(f1249,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_9 | ~spl30_24 | ~spl30_39)),
% 0.21/0.33 inference(forward_demodulation,[],[f997,f1240])).
% 0.21/0.33 thf(f1250,plain,(
% 0.21/0.33 $false | (~spl30_9 | ~spl30_24 | ~spl30_39)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1249])).
% 0.21/0.33 thf(f1251,plain,(
% 0.21/0.33 ~spl30_9 | ~spl30_24 | ~spl30_39),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1250])).
% 0.21/0.33 thf(f1254,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((sK1 @ X3)) = $true) | ($true = $false)) ) | (~spl30_2 | ~spl30_9)),
% 0.21/0.33 inference(forward_demodulation,[],[f851,f1186])).
% 0.21/0.33 thf(f1255,plain,(
% 0.21/0.33 ( ! [X3 : $i] : ((((sK1 @ X3)) = $true)) ) | (~spl30_2 | ~spl30_9)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1254])).
% 0.21/0.33 thf(f1256,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_9 | ~spl30_36 | ~spl30_39)),
% 0.21/0.33 inference(forward_demodulation,[],[f1102,f1240])).
% 0.21/0.33 thf(f1257,plain,(
% 0.21/0.33 $false | (~spl30_9 | ~spl30_36 | ~spl30_39)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1256])).
% 0.21/0.33 thf(f1258,plain,(
% 0.21/0.33 ~spl30_9 | ~spl30_36 | ~spl30_39),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1257])).
% 0.21/0.33 thf(f1267,plain,(
% 0.21/0.33 ( ! [X0 : $i] : ((((sK2 @ X0)) = $false)) ) | ~spl30_36),
% 0.21/0.33 inference(constrained_superposition,[],[f1102,f59])).
% 0.21/0.33 thf(f1274,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_1 | ~spl30_9 | ~spl30_36)),
% 0.21/0.33 inference(forward_demodulation,[],[f1235,f1267])).
% 0.21/0.33 thf(f1275,plain,(
% 0.21/0.33 $false | (~spl30_1 | ~spl30_9 | ~spl30_36)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1274])).
% 0.21/0.33 thf(f1276,plain,(
% 0.21/0.33 ~spl30_1 | ~spl30_9 | ~spl30_36),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1275])).
% 0.21/0.33 thf(f1281,plain,(
% 0.21/0.33 ($true = $false) | (~spl30_2 | ~spl30_9 | ~spl30_38)),
% 0.21/0.33 inference(forward_demodulation,[],[f1111,f1255])).
% 0.21/0.33 thf(f1282,plain,(
% 0.21/0.33 $false | (~spl30_2 | ~spl30_9 | ~spl30_38)),
% 0.21/0.33 inference(trivial_inequality_removal,[],[f1281])).
% 0.21/0.33 thf(f1283,plain,(
% 0.21/0.33 ~spl30_2 | ~spl30_9 | ~spl30_38),
% 0.21/0.33 inference(avatar_contradiction_clause,[],[f1282])).
% 0.21/0.33 cnf(s1, plain, spl30_1 | spl30_2 | spl30_3 | spl30_4, inference(sat_conversion,[],[f859])).
% 0.21/0.33 cnf(s4, plain, spl30_1 | spl30_2 | spl30_4 | spl30_7, inference(sat_conversion,[],[f873])).
% 0.21/0.33 cnf(s21, plain, spl30_1 | spl30_2 | spl30_3 | spl30_13, inference(sat_conversion,[],[f914])).
% 0.21/0.33 cnf(s87, plain, spl30_3 | spl30_24 | spl30_27 | spl30_31, inference(sat_conversion,[],[f1052])).
% 0.21/0.33 cnf(s88, plain, spl30_7 | spl30_24 | spl30_27 | spl30_31, inference(sat_conversion,[],[f1053])).
% 0.21/0.33 cnf(s101, plain, spl30_35 | spl30_35 | spl30_36, inference(sat_conversion,[],[f1103])).
% 0.21/0.33 cnf(s102, plain, spl30_35 | spl30_36, inference(rat,[],[s101])).
% 0.21/0.33 cnf(s113, plain, spl30_39 | spl30_38 | spl30_39, inference(sat_conversion,[],[f1126])).
% 0.21/0.33 cnf(s114, plain, spl30_38 | spl30_39, inference(rat,[],[s113])).
% 0.21/0.33 cnf(s121, plain, ~spl30_9 | ~spl30_35 | ~spl30_38, inference(sat_conversion,[],[f1156])).
% 0.21/0.33 cnf(s122, plain, spl30_9, inference(sat_conversion,[],[f1181])).
% 0.21/0.33 cnf(s123, plain, ~spl30_4 | ~spl30_9 | ~spl30_38, inference(sat_conversion,[],[f1192])).
% 0.21/0.33 cnf(s124, plain, ~spl30_7 | ~spl30_9 | ~spl30_13, inference(sat_conversion,[],[f1197])).
% 0.21/0.33 cnf(s127, plain, ~spl30_7 | ~spl30_9 | ~spl30_36, inference(sat_conversion,[],[f1210])).
% 0.21/0.33 cnf(s128, plain, ~spl30_3 | ~spl30_9 | ~spl30_35, inference(sat_conversion,[],[f1218])).
% 0.21/0.33 cnf(s129, plain, ~spl30_9 | ~spl30_27 | ~spl30_35, inference(sat_conversion,[],[f1222])).
% 0.21/0.33 cnf(s134, plain, ~spl30_9 | ~spl30_31 | ~spl30_39, inference(sat_conversion,[],[f1248])).
% 0.21/0.34 cnf(s135, plain, ~spl30_9 | ~spl30_24 | ~spl30_39, inference(sat_conversion,[],[f1251])).
% 0.21/0.34 cnf(s136, plain, ~spl30_9 | ~spl30_36 | ~spl30_39, inference(sat_conversion,[],[f1258])).
% 0.21/0.34 cnf(s137, plain, ~spl30_1 | ~spl30_9 | ~spl30_36, inference(sat_conversion,[],[f1276])).
% 0.21/0.34 cnf(s139, plain, ~spl30_2 | ~spl30_9 | ~spl30_38, inference(sat_conversion,[],[f1283])).
% 0.21/0.34 cnf(s140, plain, ~spl30_35 | ~spl30_38, inference(rat,[],[s121,s122])).
% 0.21/0.34 cnf(s141, plain, spl30_3 | spl30_2 | spl30_1, inference(rat,[],[s129,s88,s102,s134,s135,s136,s114,s124,s123,s21,s1,s122])).
% 0.21/0.34 cnf(s142, plain, spl30_2 | spl30_1, inference(rat,[],[s123,s4,s114,s127,s136,s102,s128,s141,s122])).
% 0.21/0.34 cnf(s143, plain, ~spl30_39, inference(rat,[],[s87,s128,s129,s102,s134,s135,s136,s122])).
% 0.21/0.34 cnf(s144, plain, spl30_38, inference(rat,[],[s114,s143])).
% 0.21/0.34 cnf(s145, plain, ~spl30_2, inference(rat,[],[s139,s122,s144])).
% 0.21/0.34 cnf(s147, plain, ~spl30_35, inference(rat,[],[s140,s144])).
% 0.21/0.34 cnf(s148, plain, spl30_1, inference(rat,[],[s142,s145])).
% 0.21/0.34 cnf(s149, plain, spl30_36, inference(rat,[],[s102,s147])).
% 0.21/0.34 cnf(s150, plain, $false, inference(rat,[],[s137,s122,s149,s148])).
% 0.21/0.34 thf(f1284,plain,(
% 0.21/0.34 $false),
% 0.21/0.34 inference(avatar_sat_refutation,[],[s150])).
% 0.21/0.34 % SZS output end Proof for theBenchmark
% 0.21/0.34 % (3056321)------------------------------
% 0.21/0.34 % (3056321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.34 % (3056321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.34 % (3056321)CaDiCaL version: 2.1.3
% 0.21/0.34 % (3056321)Termination reason: Refutation
% 0.21/0.34 % (3056321)Time elapsed: 0.045 s
% 0.21/0.34 % (3056321)Peak memory usage: 14 MB
% 0.21/0.34 % (3056321)Instructions burned: 99 (million)
% 0.21/0.34 % (3056310)Success in time 0.079 s
% 0.21/0.34 % Vampire exiting
%------------------------------------------------------------------------------