%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX178^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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.20s 0.34s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX178^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n002.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 16:12:52 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running higher-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.34 % (1479219)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.20/0.34 % (1479225)lrs+10_16_si=on:nwc=1.5:random_seed=316575646:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.20/0.34 % (1479225)Instruction limit reached!
% 0.20/0.34 % (1479225)------------------------------
% 0.20/0.34 % (1479225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479225)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479225)Termination reason: Instruction limit
% 0.20/0.34 % (1479225)Termination phase: Saturation
% 0.20/0.34 % (1479225)Time elapsed: 0.005 s
% 0.20/0.34 % (1479225)Peak memory usage: 12 MB
% 0.20/0.34 % (1479225)Instructions burned: 20 (million)
% 0.20/0.34 % (1479224)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1654568863:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.20/0.34 % (1479226)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3108425197:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.20/0.34 % (1479228)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=835222424:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.20/0.34 % (1479227)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=777747620: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.20/0.34 % (1479226)Instruction limit reached!
% 0.20/0.34 % (1479226)------------------------------
% 0.20/0.34 % (1479226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479226)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479226)Termination reason: Instruction limit
% 0.20/0.34 % (1479226)Termination phase: Property scanning
% 0.20/0.34 % (1479226)Time elapsed: 0.001 s
% 0.20/0.34 % (1479226)Peak memory usage: 10 MB
% 0.20/0.34 % (1479226)Instructions burned: 3 (million)
% 0.20/0.34 % (1479229)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2643680780:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.20/0.34 % (1479230)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.20/0.34 % (1479230)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.20/0.34 % (1479230)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=3076773231:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.20/0.34 % (1479228)Instruction limit reached!
% 0.20/0.34 % (1479228)------------------------------
% 0.20/0.34 % (1479228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479228)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479228)Termination reason: Instruction limit
% 0.20/0.34 % (1479228)Termination phase: Saturation
% 0.20/0.34 % (1479228)Time elapsed: 0.013 s
% 0.20/0.34 % (1479228)Peak memory usage: 12 MB
% 0.20/0.34 % (1479228)Instructions burned: 24 (million)
% 0.20/0.34 % (1479232)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=160326524:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.34 % (1479237)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3147728187:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.20/0.34 % (1479229)Instruction limit reached!
% 0.20/0.34 % (1479229)------------------------------
% 0.20/0.34 % (1479229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479232)Instruction limit reached!
% 0.20/0.34 % (1479232)------------------------------
% 0.20/0.34 % (1479232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479229)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479232)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479229)Termination reason: Instruction limit
% 0.20/0.34 % (1479229)Termination phase: Saturation
% 0.20/0.34 % (1479232)Termination reason: Instruction limit
% 0.20/0.34 % (1479232)Termination phase: Saturation
% 0.20/0.34 % (1479229)Time elapsed: 0.017 s
% 0.20/0.34 % (1479232)Time elapsed: 0.003 s
% 0.20/0.34 % (1479229)Peak memory usage: 12 MB
% 0.20/0.34 % (1479232)Peak memory usage: 10 MB
% 0.20/0.34 % (1479232)Instructions burned: 7 (million)
% 0.20/0.34 % (1479229)Instructions burned: 77 (million)
% 0.20/0.34 % (1479237)Instruction limit reached!
% 0.20/0.34 % (1479237)------------------------------
% 0.20/0.34 % (1479237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479237)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479237)Termination reason: Instruction limit
% 0.20/0.34 % (1479237)Termination phase: Saturation
% 0.20/0.34 % (1479237)Time elapsed: 0.004 s
% 0.20/0.34 % (1479237)Peak memory usage: 11 MB
% 0.20/0.34 % (1479237)Instructions burned: 7 (million)
% 0.20/0.34 % (1479240)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.20/0.34 % (1479240)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3933143759:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.20/0.34 % (1479243)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3709392994:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.20/0.34 % (1479240)Instruction limit reached!
% 0.20/0.34 % (1479240)------------------------------
% 0.20/0.34 % (1479240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479240)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479240)Termination reason: Instruction limit
% 0.20/0.34 % (1479240)Termination phase: Saturation
% 0.20/0.34 % (1479240)Time elapsed: 0.003 s
% 0.20/0.34 % (1479240)Peak memory usage: 11 MB
% 0.20/0.34 % (1479240)Instructions burned: 7 (million)
% 0.20/0.34 % (1479243)Instruction limit reached!
% 0.20/0.34 % (1479243)------------------------------
% 0.20/0.34 % (1479243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479243)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479243)Termination reason: Instruction limit
% 0.20/0.34 % (1479243)Termination phase: Saturation
% 0.20/0.34 % (1479243)Time elapsed: 0.004 s
% 0.20/0.34 % (1479243)Peak memory usage: 12 MB
% 0.20/0.34 % (1479243)Instructions burned: 15 (million)
% 0.20/0.34 % (1479244)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.20/0.34 % (1479244)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.20/0.34 % (1479224)Instruction limit reached!
% 0.20/0.34 % (1479224)------------------------------
% 0.20/0.34 % (1479224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479224)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479224)Termination reason: Instruction limit
% 0.20/0.34 % (1479224)Termination phase: Saturation
% 0.20/0.34 % (1479224)Time elapsed: 0.040 s
% 0.20/0.34 % (1479224)Peak memory usage: 13 MB
% 0.20/0.34 % (1479224)Instructions burned: 89 (million)
% 0.20/0.34 % (1479244)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2240232782: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.20/0.34 % (1479245)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=2131607074:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.20/0.34 % (1479249)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.20/0.34 % (1479249)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=311929360:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.34 % (1479249)Instruction limit reached!
% 0.20/0.34 % (1479249)------------------------------
% 0.20/0.34 % (1479249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479249)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479249)Termination reason: Instruction limit
% 0.20/0.34 % (1479249)Termination phase: Saturation
% 0.20/0.34 % (1479249)Time elapsed: 0.002 s
% 0.20/0.34 % (1479249)Peak memory usage: 11 MB
% 0.20/0.34 % (1479249)Instructions burned: 9 (million)
% 0.20/0.34 % (1479230) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1479219-1479230"...
% 0.20/0.34 % (1479248)lrs+10_1_si=on:cs=on:random_seed=4292886604:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.20/0.34 % (1479244)Instruction limit reached!
% 0.20/0.34 % (1479244)------------------------------
% 0.20/0.34 % (1479244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479244)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479244)Termination reason: Instruction limit
% 0.20/0.34 % (1479244)Termination phase: Saturation
% 0.20/0.34 % (1479244)Time elapsed: 0.013 s
% 0.20/0.34 % (1479244)Peak memory usage: 12 MB
% 0.20/0.34 % (1479244)Instructions burned: 28 (million)
% 0.20/0.34 % (1479250)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1032001893:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.20/0.34 % (1479248)Instruction limit reached!
% 0.20/0.34 % (1479248)------------------------------
% 0.20/0.34 % (1479248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479248)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479248)Termination reason: Instruction limit
% 0.20/0.34 % (1479248)Termination phase: Saturation
% 0.20/0.34 % (1479248)Time elapsed: 0.005 s
% 0.20/0.34 % (1479248)Peak memory usage: 12 MB
% 0.20/0.34 % (1479248)Instructions burned: 8 (million)
% 0.20/0.34 % (1479254)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=375666485:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.20/0.34 % (1479250)Refutation not found, incomplete strategy
% 0.20/0.34 % (1479250)------------------------------
% 0.20/0.34 % (1479250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479250)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479250)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.34 % (1479250)Time elapsed: 0.003 s
% 0.20/0.34 % (1479250)Peak memory usage: 12 MB
% 0.20/0.34 % (1479250)Instructions burned: 5 (million)
% 0.20/0.34 % (1479250)------------------------------
% 0.20/0.34 % (1479250)------------------------------
% 0.20/0.34 % (1479256)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3581950409:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.20/0.34 % (1479230)...printing done.
% 0.20/0.34 % (1479230)Refutation found. Thanks to Tanya!
% 0.20/0.34 % SZS status Theorem for theBenchmark
% 0.20/0.34 % SZS output start Proof for theBenchmark
% 0.20/0.34 thf(type_def_5, type, unsorted: $tType).
% 0.20/0.34 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.34 thf(type_def_7, type, d_unsorted: $tType).
% 0.20/0.34 thf(func_def_0, type, irel: ($i > $i > $o)).
% 0.20/0.34 thf(func_def_1, type, mnot: (($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_2, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_3, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_4, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_5, type, mbox_s4: (($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_6, type, iatom: (($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_7, type, inot: (($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_8, type, itrue: ($i > $o)).
% 0.20/0.34 thf(func_def_9, type, ifalse: ($i > $o)).
% 0.20/0.34 thf(func_def_10, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_11, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_12, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_13, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_14, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_15, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 0.20/0.34 thf(func_def_16, type, ivalid: (($i > $o) > $o)).
% 0.20/0.34 thf(func_def_17, type, isatisfiable: (($i > $o) > $o)).
% 0.20/0.34 thf(func_def_18, type, icountersatisfiable: (($i > $o) > $o)).
% 0.20/0.34 thf(func_def_19, type, iinvalid: (($i > $o) > $o)).
% 0.20/0.34 thf(func_def_20, type, d2unsorted: (d_unsorted > $i)).
% 0.20/0.34 thf(func_def_21, type, d_unsorted_0: d_unsorted).
% 0.20/0.34 thf(func_def_23, type, vAND: ($o > $o > $o)).
% 0.20/0.34 thf(func_def_24, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.20/0.34 thf(func_def_25, type, vOR: ($o > $o > $o)).
% 0.20/0.34 thf(func_def_26, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_27, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_28, type, vNOT: ($o > $o)).
% 0.20/0.34 thf(func_def_29, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_30, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_31, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.34 thf(func_def_32, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_33, type, db5: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_36, type, db8: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_37, type, db6: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_38, type, db7: !>[X0: $tType]:(X0)).
% 0.20/0.34 thf(func_def_39, type, sK0: ($i > d_unsorted)).
% 0.20/0.34 thf(func_def_40, type, sK1: ($i > $o)).
% 0.20/0.34 thf(func_def_41, type, sK2: ($i > $o)).
% 0.20/0.34 thf(func_def_58, type, sK19: ($i > $i)).
% 0.20/0.34 thf(func_def_59, type, sK20: ($i > $i)).
% 0.20/0.34 thf(func_def_60, type, sK21: ($i > $i)).
% 0.20/0.34 thf(func_def_61, type, sK22: ($i > $i)).
% 0.20/0.34 thf(func_def_62, type, sK23: ($i > $i)).
% 0.20/0.34 thf(func_def_63, type, sK24: ($i > $i)).
% 0.20/0.34 thf(func_def_64, type, sK25: ($i > $i)).
% 0.20/0.34 thf(func_def_65, type, sK26: ($i > $i)).
% 0.20/0.34 thf(func_def_66, type, sK27: ($i > $i)).
% 0.20/0.34 thf(func_def_67, type, sK28: ($i > $i)).
% 0.20/0.34 thf(func_def_68, type, sK29: ($i > $i)).
% 0.20/0.34 thf(func_def_69, type, sK30: ($i > $i)).
% 0.20/0.34 thf(f1,axiom,(
% 0.20/0.34 ((^[X18 : ($i > $o)] : (! [X19 : $i] : ~(X18 @ X19))) = iinvalid) & ((^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X4 @ X0) & (X5 @ X0))) = mand) & (mor = (^[X4 : ($i > $o), X5 : ($i > $o), X0 : $i] : ((X5 @ X0) | (X4 @ X0)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & ! [X0 : $i] : ? [X1 : d_unsorted] : (X0 = ((d2unsorted @ X1))) & (ior = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))))) & ((^[X8 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)))) = inot) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & ((^[X18 : ($i > $o)] : (! [X19 : $i] : (X18 @ X19))) = ivalid) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) & ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)))) = iand) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)) | ~ ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)))) = iimplies) & ((^[X18 : ($i > $o)] : (~ ! [X19 : $i] : ~(X18 @ X19))) = isatisfiable) & ((^[X8 : ($i > $o), X7 : $i] : ((X8 @ X7))) = iatom) & ! [X1 : d_unsorted] : (X1 = d_unsorted_0) & ((^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i,X14 : $i,X17 : $i,X16 : $i,X15 : $i] : (((~(irel @ X16 @ X17) | (X8 @ X17) | ~(irel @ X5 @ X16) | ~ ! [X13 : $i] : ((X9 @ X13) | ~(irel @ X16 @ X13))) & (~(irel @ X5 @ X14) | ~(irel @ X14 @ X15) | (X9 @ X15) | ~ ! [X11 : $i] : ((X8 @ X11) | ~(irel @ X14 @ X11)))) | ~(irel @ X7 @ X5)))) = ixor) & (mbox_s4 = (^[X8 : ($i > $o), X4 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X4 @ X5))))) & (itrue @ (d2unsorted @ d_unsorted_0)) & (iimplied = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (~ ! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & ((^[X18 : ($i > $o)] : (~ ! [X19 : $i] : (X18 @ X19))) = icountersatisfiable) & ((^[X4 : ($i > $o), X0 : $i] : (~(X4 @ X0))) = mnot) & (mimplies = (^[X0 : ($i > $o), X6 : ($i > $o), X7 : $i] : ((X6 @ X7) | ~(X0 @ X7)))) & (iequiv = (^[X8 : ($i > $o), X9 : ($i > $o), X7 : $i] : (! [X10 : $i,X5 : $i] : (~(irel @ X7 @ X5) | ~(irel @ X5 @ X10) | ~ ! [X11 : $i] : ((X8 @ X11) | ~(irel @ X5 @ X11)) | (X9 @ X10)) & ! [X12 : $i,X5 : $i] : (~ ! [X13 : $i] : (~(irel @ X5 @ X13) | (X9 @ X13)) | ~(irel @ X7 @ X5) | ~(irel @ X5 @ X12) | (X8 @ X12)))))),
% 0.20/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p',lcl696_1)).
% 0.20/0.34 thf(f2,conjecture,(
% 0.20/0.34 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((iand @ (iimplies @ X0 @ X1) @ (iimplies @ X1 @ X0)))) = iequiv)),
% 0.20/0.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p',iequiv)).
% 0.20/0.34 thf(f3,negated_conjecture,(
% 0.20/0.34 ~ ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((iand @ (iimplies @ X0 @ X1) @ (iimplies @ X1 @ X0)))) = iequiv)),
% 0.20/0.34 inference(negated_conjecture,[status(cth)],[f2])).
% 0.20/0.34 thf(f4,plain,(
% 0.20/0.34 ((^[X0 : ($i > $o)] : (! [X1 : $i] : ~(X0 @ X1))) = iinvalid) & ((^[X2 : ($i > $o), X3 : ($i > $o), X4 : $i] : ((X2 @ X4) & (X3 @ X4))) = mand) & (mor = (^[X5 : ($i > $o), X6 : ($i > $o), X7 : $i] : ((X6 @ X7) | (X5 @ X7)))) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8) & (ior = (^[X10 : ($i > $o), X11 : ($i > $o), X12 : $i] : (! [X13 : $i] : ((X11 @ X13) | ~(irel @ X12 @ X13)) | ! [X14 : $i] : (~(irel @ X12 @ X14) | (X10 @ X14))))) & ((^[X15 : ($i > $o), X16 : $i] : (~ ! [X17 : $i] : (~(irel @ X16 @ X17) | (X15 @ X17)))) = inot) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & ! [X18 : d_unsorted,X19 : d_unsorted] : ((((d2unsorted @ X19)) = ((d2unsorted @ X18))) => (X18 = X19)) & ((^[X20 : ($i > $o)] : (! [X21 : $i] : (X20 @ X21))) = ivalid) & ((^[X22 : ($i > $o), X23 : ($i > $o), X24 : $i] : (! [X25 : $i] : ((X23 @ X25) | ~(irel @ X24 @ X25)) & ! [X26 : $i] : (~(irel @ X24 @ X26) | (X22 @ X26)))) = iand) & ((^[X27 : ($i > $o), X28 : ($i > $o), X29 : $i] : (! [X30 : $i] : (~(irel @ X29 @ X30) | (X28 @ X30)) | ~ ! [X31 : $i] : ((X27 @ X31) | ~(irel @ X29 @ X31)))) = iimplies) & ((^[X32 : ($i > $o)] : (~ ! [X33 : $i] : ~(X32 @ X33))) = isatisfiable) & ((^[X34 : ($i > $o), X35 : $i] : ((X34 @ X35))) = iatom) & ! [X36 : d_unsorted] : (d_unsorted_0 = X36) & ((^[X37 : ($i > $o), X38 : ($i > $o), X39 : $i] : (~ ! [X40 : $i,X41 : $i,X42 : $i,X43 : $i,X44 : $i] : (((~(irel @ X43 @ X42) | (X37 @ X42) | ~(irel @ X40 @ X43) | ~ ! [X45 : $i] : ((X38 @ X45) | ~(irel @ X43 @ X45))) & (~(irel @ X40 @ X41) | ~(irel @ X41 @ X44) | (X38 @ X44) | ~ ! [X46 : $i] : ((X37 @ X46) | ~(irel @ X41 @ X46)))) | ~(irel @ X39 @ X40)))) = ixor) & (mbox_s4 = (^[X47 : ($i > $o), X48 : $i] : (! [X49 : $i] : ((X47 @ X49) | ~(irel @ X48 @ X49))))) & (itrue @ (d2unsorted @ d_unsorted_0)) & (iimplied = (^[X50 : ($i > $o), X51 : ($i > $o), X52 : $i] : (~ ! [X53 : $i] : ((X51 @ X53) | ~(irel @ X52 @ X53)) | ! [X54 : $i] : ((X50 @ X54) | ~(irel @ X52 @ X54))))) & ((^[X55 : ($i > $o)] : (~ ! [X56 : $i] : (X55 @ X56))) = icountersatisfiable) & ((^[X57 : ($i > $o), X58 : $i] : (~(X57 @ X58))) = mnot) & (mimplies = (^[X59 : ($i > $o), X60 : ($i > $o), X61 : $i] : ((X60 @ X61) | ~(X59 @ X61)))) & (iequiv = (^[X62 : ($i > $o), X63 : ($i > $o), X64 : $i] : (! [X65 : $i,X66 : $i] : (~(irel @ X64 @ X66) | ~(irel @ X66 @ X65) | ~ ! [X67 : $i] : ((X62 @ X67) | ~(irel @ X66 @ X67)) | (X63 @ X65)) & ! [X68 : $i,X69 : $i] : (~ ! [X70 : $i] : (~(irel @ X69 @ X70) | (X63 @ X70)) | ~(irel @ X64 @ X69) | ~(irel @ X69 @ X68) | (X62 @ X68)))))),
% 0.20/0.34 inference(rectify,[],[f1])).
% 0.20/0.34 thf(f5,plain,(
% 0.20/0.34 (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X8 : $i] : ? [X9 : d_unsorted] : (((d2unsorted @ X9)) = X8) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X18 : d_unsorted,X19 : d_unsorted] : ((((d2unsorted @ X19)) = ((d2unsorted @ X18))) => (X18 = X19)) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $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]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & ! [X36 : d_unsorted] : (d_unsorted_0 = X36) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))))),
% 0.20/0.34 inference(fool_elimination,[],[f4])).
% 0.20/0.34 thf(f6,plain,(
% 0.20/0.34 ~ (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.20/0.34 inference(fool_elimination,[],[f3])).
% 0.20/0.34 thf(f7,plain,(
% 0.20/0.34 (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ~ (((ifalse @ (d2unsorted @ d_unsorted_0))) = $true) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $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]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))))),
% 0.20/0.34 inference(rectify,[],[f5])).
% 0.20/0.34 thf(f8,plain,(
% 0.20/0.34 (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (isatisfiable = (^[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)))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((((d2unsorted @ X2)) = ((d2unsorted @ X3))) => (X2 = X3)) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : (((d2unsorted @ X1)) = X0) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3)))))))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2))))))))),
% 0.20/0.34 inference(flattening,[],[f7])).
% 0.20/0.34 thf(f9,plain,(
% 0.20/0.34 (iequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.20/0.34 inference(flattening,[],[f6])).
% 0.20/0.34 thf(f10,plain,(
% 0.20/0.34 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3)))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[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) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X3 : d_unsorted,X2 : d_unsorted] : ((X2 = X3) | (((d2unsorted @ X2)) != ((d2unsorted @ X3)))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 0.20/0.34 inference(ennf_transformation,[],[f8])).
% 0.20/0.34 thf(f11,plain,(
% 0.20/0.34 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3)))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & ! [X1 : $i] : ? [X2 : d_unsorted] : (((d2unsorted @ X2)) = X1) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((X3 = X4) | (((d2unsorted @ X3)) != ((d2unsorted @ X4)))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 0.20/0.34 inference(rectify,[],[f10])).
% 0.20/0.34 thf(f12,plain,(
% 0.20/0.34 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3)))))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ! [X0 : d_unsorted] : (d_unsorted_0 = X0) & (((ifalse @ (d2unsorted @ d_unsorted_0))) != $true) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (((itrue @ (d2unsorted @ d_unsorted_0))) = $true) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & ! [X1 : $i] : (((d2unsorted @ (sK0 @ X1))) = X1) & (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X3 : d_unsorted,X4 : d_unsorted] : ((X3 = X4) | (((d2unsorted @ X3)) != ((d2unsorted @ X4)))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((~ (irel @ Y2 @ Y7)) | (((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y6 @ Y8)) | (Y0 @ Y8))))) | (Y1 @ Y3)) | (~ (irel @ Y6 @ Y3))) | (~ (irel @ Y7 @ Y6))) & ((((~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y1 @ Y8))))) | (~ (irel @ Y7 @ Y4))) | (Y0 @ Y5)) | (~ (irel @ Y4 @ Y5)))))))))))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (Y0 @ Y2)) | (Y1 @ Y2)))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2)))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 0.20/0.34 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X1)],[f11])).
% 0.20/0.34 thf(f13,plain,(
% 0.20/0.34 (iequiv != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 0.20/0.34 inference(cnf_transformation,[],[f9])).
% 0.20/0.34 thf(f22,plain,(
% 0.20/0.34 (((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))) = $true)),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f23,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((d2unsorted @ (sK0 @ X1))) = X1)) )),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f25,plain,(
% 0.20/0.34 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f29,plain,(
% 0.20/0.34 ( ! [X0 : d_unsorted] : ((d_unsorted_0 = X0)) )),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f30,plain,(
% 0.20/0.34 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f34,plain,(
% 0.20/0.34 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))))),
% 0.20/0.34 inference(cnf_transformation,[],[f12])).
% 0.20/0.34 thf(f39,plain,(
% 0.20/0.34 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y5) | (~ (irel @ Y4 @ Y5))))) & (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y3 @ Y5)))))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((Y3 @ Y5) | (~ (irel @ Y4 @ Y5))))))))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y2 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((Y3 @ Y5) | (~ (irel @ Y4 @ Y5))))))))))) @ Y1 @ Y0))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))))),
% 0.20/0.34 inference(definition_unfolding,[],[f13,f34,f25,f30,f30])).
% 0.20/0.34 thf(f40,plain,(
% 0.20/0.34 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))))))))))))))))),
% 0.20/0.34 inference(beta-eta_normalization,[],[f39])).
% 0.20/0.34 thf(f51,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((d2unsorted @ d_unsorted_0)) = X1)) )),
% 0.20/0.34 inference(forward_demodulation,[],[f23,f29])).
% 0.20/0.34 thf(f55,plain,(
% 0.20/0.34 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 0.20/0.34 inference(constrained_superposition,[],[f51,f51])).
% 0.20/0.34 thf(f81,plain,(
% 0.20/0.34 ( ! [X0 : $i] : (($true = ((irel @ X0 @ X0)))) )),
% 0.20/0.34 inference(constrained_superposition,[],[f22,f51])).
% 0.20/0.34 thf(f84,plain,(
% 0.20/0.34 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))) | (~ (!! @ $i @ (^[Y5 : $i]: ((Y1 @ Y5) | (~ (irel @ Y3 @ Y5))))))))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((Y1 @ Y4) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y3 @ Y4))) | (~ (irel @ Y2 @ Y3))))))))))))) @ sK1)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y0 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y4) | (~ (irel @ Y3 @ Y4)))))) | (~ (irel @ Y2 @ Y3))))) & (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | ((~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y1 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y3 @ Y4))))))))))))))) @ sK1)))),
% 0.20/0.34 inference(negative_extensionality,[],[f40])).
% 0.20/0.34 thf(f85,plain,(
% 0.20/0.34 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (~ (irel @ Y1 @ Y2))))) & (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((sK1 @ Y3) | (~ (irel @ Y2 @ Y3))) | (~ (irel @ Y1 @ Y2))) | (~ (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y2 @ Y4))))))))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((Y0 @ Y3) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK1 @ Y4)))))) | (~ (irel @ Y2 @ Y3))) | (~ (irel @ Y1 @ Y2))))))))))))),
% 0.20/0.34 inference(beta-eta_normalization,[],[f84])).
% 0.20/0.34 thf(f86,plain,(
% 0.20/0.34 ((((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (sK1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3)))))) | (~ (irel @ Y1 @ Y2))))) & (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((sK1 @ Y3) | (~ (irel @ Y2 @ Y3))))))))))))) @ sK2)) != (((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((sK1 @ Y3) | (~ (irel @ Y2 @ Y3))) | (~ (irel @ Y1 @ Y2))) | (~ (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y4) | (~ (irel @ Y2 @ Y4))))))))))) & (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((((Y0 @ Y3) | (~ (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y2 @ Y4)) | (sK1 @ Y4)))))) | (~ (irel @ Y2 @ Y3))) | (~ (irel @ Y1 @ Y2))))))))))) @ sK2)))),
% 0.20/0.34 inference(negative_extensionality,[],[f85])).
% 0.20/0.34 thf(f87,plain,(
% 0.20/0.34 ((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y1 @ Y3))))))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK2 @ Y2) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))))))))) != (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))) & (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))))))))))))),
% 0.20/0.34 inference(beta-eta_normalization,[],[f86])).
% 0.20/0.34 thf(f88,plain,(
% 0.20/0.34 ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))) & (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))))))))))) @ sK3)) != (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y1 @ Y3))))))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK2 @ Y2) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))))))))) @ sK3)))),
% 0.20/0.34 inference(negative_extensionality,[],[f87])).
% 0.20/0.34 thf(f89,plain,(
% 0.20/0.34 ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y1 @ Y3))))))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK2 @ Y2) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))))))))) @ sK3)) = $true) | ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))) & (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))))))))))) @ sK3)) = $true)),
% 0.20/0.34 inference(xor_proxy_clausification,[],[f88])).
% 0.20/0.34 thf(f90,plain,(
% 0.20/0.34 ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))) | (~ (!! @ $i @ (^[Y3 : $i]: ((sK2 @ Y3) | (~ (irel @ Y1 @ Y3))))))))))) & (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((((sK2 @ Y2) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y1 @ Y3)) | (sK1 @ Y3)))))) | (~ (irel @ Y1 @ Y2))) | (~ (irel @ Y0 @ Y1))))))))) @ sK3)) = $false) | ((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))))) & (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | ((~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK2 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((sK1 @ Y2) | (~ (irel @ Y1 @ Y2))))))))))) @ sK3)) = $false)),
% 0.20/0.34 inference(xor_proxy_clausification,[],[f88])).
% 0.20/0.34 thf(f91,plain,(
% 0.20/0.34 ($false = (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))))) | ($false = (((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))))),
% 0.20/0.34 inference(beta-eta_normalization,[],[f90])).
% 0.20/0.34 thf(f92,plain,(
% 0.20/0.34 ($false = (((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))) = $false)),
% 0.20/0.34 inference(and_proxy_clausification,[],[f91])).
% 0.20/0.34 thf(f93,plain,(
% 0.20/0.34 ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))) = $false)),
% 0.20/0.34 inference(and_proxy_clausification,[],[f92])).
% 0.20/0.34 thf(f94,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))) @ sK4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))) = $false)),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f93])).
% 0.20/0.34 thf(f95,plain,(
% 0.20/0.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))) @ sK4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | ((((^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ sK5)) = $false)),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f94])).
% 0.20/0.34 thf(f96,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))) @ sK4))) | ((((^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ sK5)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))) @ sK6)))),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f95])).
% 0.20/0.34 thf(f97,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))) @ sK4))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2)))))))))) @ sK7)) = $false) | ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))) @ sK6))) | ((((^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ sK5)) = $false)),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f96])).
% 0.20/0.34 thf(f98,plain,(
% 0.20/0.34 (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))))) | (~ (irel @ sK3 @ sK5)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1))))))))))) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0)))))))))),
% 0.20/0.34 inference(beta-eta_normalization,[],[f97])).
% 0.20/0.34 thf(f100,plain,(
% 0.20/0.34 ($false = ((!! @ $i @ (^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1))))))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))))))) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f98])).
% 0.20/0.34 thf(f101,plain,(
% 0.20/0.34 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))))))) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false)),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f100])).
% 0.20/0.34 thf(f102,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))))))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f101])).
% 0.20/0.34 thf(f103,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))))) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f101])).
% 0.20/0.34 thf(f104,plain,(
% 0.20/0.34 (((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))))) = $false) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))))))),
% 0.20/0.34 inference(not_proxy_clausification,[],[f103])).
% 0.20/0.34 thf(f105,plain,(
% 0.20/0.34 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0)))))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8)))),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f104])).
% 0.20/0.34 thf(f106,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ X1))) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8)))) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f105])).
% 0.20/0.34 thf(f107,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0)))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ X1)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f106])).
% 0.20/0.34 thf(f197,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ X1)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f107])).
% 0.20/0.34 thf(f198,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ X1))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) = $true) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8)))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f197])).
% 0.20/0.34 thf(f199,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK9)) = $false) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK1 @ Y0))) @ X1))) | ((((^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))) @ X2)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f198])).
% 0.20/0.34 thf(f200,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = (((~ (irel @ sK5 @ X1)) | (sK1 @ X1)))) | ($true = (((~ (irel @ sK4 @ X2)) | (sK2 @ X2)))) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | ($false = (((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))) | (~ (irel @ sK3 @ sK6)))))) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f199])).
% 0.20/0.34 thf(f201,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = (((~ (irel @ sK4 @ X2)) | (sK2 @ X2)))) | (((sK1 @ X1)) = $true) | ($false = (((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))) | (~ (irel @ sK3 @ sK6))))) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | (((~ (irel @ sK5 @ X1))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f200])).
% 0.20/0.34 thf(f202,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = (((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))) | (~ (irel @ sK3 @ sK6))))) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | ($true = ((sK2 @ X2))) | (((sK1 @ X1)) = $true) | (((~ (irel @ sK5 @ X1))) = $true) | (((~ (irel @ sK4 @ X2))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f201])).
% 0.20/0.34 thf(f204,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK5 @ X1))) = $true) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | (((~ (irel @ sK4 @ X2))) = $true) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))))) | ($true = ((sK2 @ X2))) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f202])).
% 0.20/0.34 thf(f205,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | (((irel @ sK5 @ X1)) = $false) | ($true = ((sK2 @ X2))) | (((~ (irel @ sK4 @ X2))) = $true) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9)))))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f204])).
% 0.20/0.34 thf(f206,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))))))) | ($true = ((sK2 @ X2))) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))))) | (((irel @ sK5 @ X1)) = $false) | (((~ (irel @ sK4 @ X2))) = $true) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f205])).
% 0.20/0.34 thf(f207,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))))) | (((~ (irel @ sK4 @ X2))) = $true) | (((sK1 @ X1)) = $true) | (((irel @ sK5 @ X1)) = $false) | ($true = ((sK2 @ X2))) | ($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7)))))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f205])).
% 0.20/0.34 thf(f209,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ X1)) = $true) | (((~ (irel @ sK4 @ X2))) = $true) | ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | ($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))))) | ($true = ((sK2 @ X2))) | (((irel @ sK5 @ X1)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f207])).
% 0.20/0.34 thf(f210,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))))) | (((sK1 @ X1)) = $true) | (((irel @ sK5 @ X1)) = $false) | ($false = ((irel @ sK4 @ X2))) | ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | ($true = ((sK2 @ X2)))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f209])).
% 0.20/0.34 thf(f212,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK4 @ X2))) | ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8)))) = $false) | (((sK1 @ X1)) = $true) | ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | (((irel @ sK5 @ X1)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f210])).
% 0.20/0.34 thf(f214,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ sK8)) = $false) | (((sK1 @ X1)) = $true) | ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | ($false = ((irel @ sK4 @ X2))) | (((irel @ sK5 @ X1)) = $false) | ($true = ((sK2 @ X2)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f212])).
% 0.20/0.34 thf(f215,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((sK1 @ sK8)) = $false) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true) | ($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f214])).
% 0.20/0.34 thf(f217,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = ((sK2 @ X2))) | (((sK1 @ sK8)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (((irel @ sK5 @ X1)) = $false) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f215])).
% 0.20/0.34 thf(f218,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2))) | (((sK1 @ sK8)) = $false) | (((irel @ sK5 @ X1)) = $false) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))) @ X3))) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f217])).
% 0.20/0.34 thf(f219,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((~ (irel @ sK6 @ X3)) | (sK1 @ X3))) = $true) | (((sK1 @ X1)) = $true) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK4 @ X2))) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ sK8)) = $false)) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f218])).
% 0.20/0.34 thf(f220,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | (((sK1 @ sK8)) = $false) | (((sK1 @ X1)) = $true) | (((sK1 @ X3)) = $true) | (((~ (irel @ sK6 @ X3))) = $true) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK4 @ X2)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f219])).
% 0.20/0.34 thf(f221,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X1)) = $true) | (((sK1 @ X3)) = $true) | (((irel @ sK6 @ X3)) = $false) | ($true = ((sK2 @ X2))) | (((sK1 @ sK8)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f220])).
% 0.20/0.34 thf(f248,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK4 @ X2))) = $true) | (((sK1 @ X1)) = $true) | (((irel @ sK5 @ X1)) = $false) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))))) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))))) = $true) | ($true = ((sK2 @ X2)))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f206])).
% 0.20/0.34 thf(f249,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2))) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))))) = $true) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9)))))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f248])).
% 0.20/0.34 thf(f250,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | ($false = ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK9))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))) @ X3))) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f249])).
% 0.20/0.34 thf(f252,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))) @ X3))) | ($false = ((irel @ sK4 @ X2))) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true) | ($true = ((sK2 @ X2))) | ((((sK2 @ sK9) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f250])).
% 0.20/0.34 thf(f253,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))) @ X3))) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X1)) = $true) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) | ($true = ((sK2 @ X2)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f252])).
% 0.20/0.34 thf(f258,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))) @ X3))) | ($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2))) | (((sK1 @ X1)) = $true) | (((irel @ sK5 @ X1)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f253])).
% 0.20/0.34 thf(f259,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))) @ X3))) | ($false = ((irel @ sK4 @ X2))) | (((irel @ sK5 @ X1)) = $false) | ($true = ((sK2 @ X2))) | (((sK1 @ X1)) = $true) | ($true = (((^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))) @ X4)))) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f258])).
% 0.20/0.34 thf(f260,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK5 @ X1)) = $false) | ($false = ((irel @ sK4 @ X2))) | ($true = (((~ (irel @ sK6 @ X4)) | (sK1 @ X4)))) | ($true = ((sK2 @ X2))) | (((sK1 @ X1)) = $true) | ($true = (((sK2 @ X3) | (~ (irel @ sK7 @ X3)))))) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f259])).
% 0.20/0.34 thf(f261,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($true = (((sK2 @ X3) | (~ (irel @ sK7 @ X3))))) | ($false = ((irel @ sK4 @ X2))) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X4)) = $true) | ($true = ((~ (irel @ sK6 @ X4)))) | (((sK1 @ X1)) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f260])).
% 0.20/0.34 thf(f262,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X3))) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true) | ($true = ((~ (irel @ sK6 @ X4)))) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X4)) = $true) | (((~ (irel @ sK7 @ X3))) = $true) | ($true = ((sK2 @ X2)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f261])).
% 0.20/0.34 thf(f263,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X4)) = $true) | (((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true) | ($true = ((sK2 @ X3))) | ($false = ((irel @ sK6 @ X4))) | (((~ (irel @ sK7 @ X3))) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f262])).
% 0.20/0.34 thf(f264,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK7 @ X3))) | (((irel @ sK5 @ X1)) = $false) | ($true = ((sK2 @ X3))) | ($false = ((irel @ sK4 @ X2))) | (((sK1 @ X1)) = $true) | ($true = ((sK2 @ X2))) | ($false = ((irel @ sK6 @ X4))) | (((sK1 @ X4)) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f263])).
% 0.20/0.34 thf(f452,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0))))))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK11)) = $false) | ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0)))))))))),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f102])).
% 0.20/0.34 thf(f453,plain,(
% 0.20/0.34 ($false = (((~ (irel @ sK3 @ sK4)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))))) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))) @ sK12)) = $false) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK11)) = $false)),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f452])).
% 0.20/0.34 thf(f454,plain,(
% 0.20/0.34 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK4 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0)))))))) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))) @ sK12)) = $false) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK11)) = $false) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8)))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f453])).
% 0.20/0.34 thf(f620,plain,(
% 0.20/0.34 ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0))))))) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK11)) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))) @ sK12)) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f454])).
% 0.20/0.34 thf(f798,plain,(
% 0.20/0.34 ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ sK6 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ sK6 @ Y0))) | (~ (irel @ sK3 @ sK6)))) @ sK11)) = $false) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ sK4 @ Y0)))) @ sK13)) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK5 @ Y0)))) @ sK12)) = $false) | ($false = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ sK7 @ Y0))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ sK7 @ Y1)))))))) @ sK8)))),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f620])).
% 0.20/0.34 thf(f799,plain,(
% 0.20/0.34 ((((sK2 @ sK12) | (~ (irel @ sK5 @ sK12)))) = $false) | ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | ((((((sK2 @ sK11) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK11))) | (~ (irel @ sK3 @ sK6)))) = $false)),
% 0.20/0.34 inference(beta-eta_normalization,[],[f798])).
% 0.20/0.34 thf(f801,plain,(
% 0.20/0.34 ((((((sK2 @ sK11) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK11))) | (~ (irel @ sK3 @ sK6)))) = $false) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | ($false = ((sK2 @ sK12))) | ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f799])).
% 0.20/0.34 thf(f803,plain,(
% 0.20/0.34 ($false = ((((sK2 @ sK11) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ sK6 @ sK11))))) | ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false) | ($false = ((sK2 @ sK12))) | ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0)))))))))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f801])).
% 0.20/0.34 thf(f805,plain,(
% 0.20/0.34 ($false = (((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ sK7 @ Y0))))))))) | ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false) | ((((sK2 @ sK11) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | ($false = ((sK2 @ sK12)))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f803])).
% 0.20/0.34 thf(f807,plain,(
% 0.20/0.34 ((((sK2 @ sK11) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK6 @ Y0)) | (sK1 @ Y0))))))) = $false) | ($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))))) | ($false = ((sK2 @ sK12))) | ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f805])).
% 0.20/0.34 thf(f809,plain,(
% 0.20/0.34 ((((sK1 @ sK13) | (~ (irel @ sK4 @ sK13)))) = $false) | ($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))))) | ($false = ((sK2 @ sK12))) | ($false = ((sK2 @ sK11)))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f807])).
% 0.20/0.34 thf(f811,plain,(
% 0.20/0.34 ($false = ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8))) | (~ (irel @ sK3 @ sK7))))) | ($false = ((sK2 @ sK12))) | (((sK1 @ sK13)) = $false) | ($false = ((sK2 @ sK11)))),
% 0.20/0.34 inference(or_proxy_clausification,[],[f809])).
% 0.20/0.34 thf(f813,plain,(
% 0.20/0.34 ($false = ((sK2 @ sK12))) | ((((sK1 @ sK8) | (~ (irel @ sK7 @ sK8)))) = $false) | ($false = ((sK2 @ sK11))) | (((sK1 @ sK13)) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f811])).
% 0.20/0.34 thf(f815,plain,(
% 0.20/0.34 ($false = ((sK2 @ sK12))) | ($false = ((sK2 @ sK11))) | (((sK1 @ sK13)) = $false) | (((sK1 @ sK8)) = $false)),
% 0.20/0.34 inference(or_proxy_clausification,[],[f813])).
% 0.20/0.34 thf(f1482,plain,(
% 0.20/0.34 ((((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))) & (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))))))))) = $true) | ((((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) = $true)),
% 0.20/0.34 inference(beta-eta_normalization,[],[f89])).
% 0.20/0.34 thf(f1483,plain,(
% 0.20/0.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))))) = $true) | ((((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) = $true)),
% 0.20/0.34 inference(and_proxy_clausification,[],[f1482])).
% 0.20/0.34 thf(f1484,plain,(
% 0.20/0.34 ((((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) = $true) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2)))))))))))))),
% 0.20/0.34 inference(and_proxy_clausification,[],[f1482])).
% 0.20/0.34 thf(f1485,plain,(
% 0.20/0.34 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2))))))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))))))),
% 0.20/0.34 inference(and_proxy_clausification,[],[f1484])).
% 0.20/0.34 thf(f1526,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2)))))))))) @ X1)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1485])).
% 0.20/0.34 thf(f1527,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1)))))))) @ X2))) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0))) | (~ (!! @ $i @ (^[Y2 : $i]: ((sK2 @ Y2) | (~ (irel @ Y0 @ Y2)))))))))) @ X1)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1526])).
% 0.20/0.34 thf(f1528,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))))) = $true) | ($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))))))) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1527])).
% 0.20/0.34 thf(f1529,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((~ (irel @ sK3 @ X2)) | ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0))))))))) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3)))) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1528])).
% 0.20/0.34 thf(f1530,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))))) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3))) | (((~ (irel @ sK3 @ X2))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1529])).
% 0.20/0.34 thf(f1531,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0)))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $true) | (((~ (irel @ sK3 @ X2))) = $true) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1530])).
% 0.20/0.34 thf(f1532,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))))) = $false) | (((~ (irel @ sK3 @ X2))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $true) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3)))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1531])).
% 0.20/0.34 thf(f1533,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $true) | (((~ (irel @ sK3 @ X2))) = $true) | ($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ (sK22 @ X2)))) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3)))) )),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f1532])).
% 0.20/0.34 thf(f1534,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ (sK22 @ X2)))) | (((~ (irel @ sK3 @ X2))) = $true) | ($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3))) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))) @ X4)) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1533])).
% 0.20/0.34 thf(f1535,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: ((((sK1 @ Y0) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ X1 @ Y1)))))))) @ X3))) | (((irel @ sK3 @ X2)) = $false) | ($false = (((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK2 @ Y0))) @ (sK22 @ X2)))) | ((((^[Y0 : $i]: ((sK1 @ Y0) | (~ (irel @ X2 @ Y0)))) @ X4)) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1534])).
% 0.20/0.34 thf(f1536,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((sK1 @ X4) | (~ (irel @ X2 @ X4)))) = $true) | ((((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))))) = $true) | ($false = (((~ (irel @ X2 @ (sK22 @ X2))) | (sK2 @ (sK22 @ X2))))) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1535])).
% 0.20/0.34 thf(f1537,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = (((~ (irel @ X2 @ (sK22 @ X2))) | (sK2 @ (sK22 @ X2))))) | (((~ (irel @ X2 @ X4))) = $true) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | ((((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1536])).
% 0.20/0.34 thf(f1538,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK2 @ (sK22 @ X2)))) | (((sK1 @ X4)) = $true) | (((~ (irel @ X2 @ X4))) = $true) | ((((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))))) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1537])).
% 0.20/0.34 thf(f1553,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | ((((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1))) | (~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))))) = $true) | ($false = ((irel @ X2 @ X4))) | (((sK1 @ X4)) = $true) | ($false = ((sK2 @ (sK22 @ X2))))) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1538])).
% 0.20/0.34 thf(f1554,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | ($false = ((sK2 @ (sK22 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))))))) | (((sK1 @ X4)) = $true) | (((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1)))) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1553])).
% 0.20/0.34 thf(f1555,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK2 @ (sK22 @ X2)))) | (((sK1 @ X4)) = $true) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0))))))) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X4))) | (((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1)))) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1554])).
% 0.20/0.34 thf(f1556,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((((sK1 @ X3) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1)))) = $true) | ($false = ((sK2 @ (sK22 @ X2)))) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X4))) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK24 @ X1))))) )),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f1555])).
% 0.20/0.34 thf(f1557,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK2 @ (sK22 @ X2)))) | (((~ (irel @ sK3 @ X1))) = $true) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK24 @ X1)))) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | ((((sK1 @ X3) | (~ (irel @ X1 @ X3)))) = $true) | ($false = ((irel @ X2 @ X4)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1556])).
% 0.20/0.34 thf(f1558,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | ((((sK1 @ X3) | (~ (irel @ X1 @ X3)))) = $true) | ($false = ((irel @ sK3 @ X1))) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK24 @ X1)))) | ($false = ((sK2 @ (sK22 @ X2)))) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X4)) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1557])).
% 0.20/0.34 thf(f1559,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK24 @ X1)))) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X4))) | (((sK1 @ X4)) = $true) | (((~ (irel @ X1 @ X3))) = $true) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (sK22 @ X2))))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1558])).
% 0.20/0.34 thf(f1560,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (sK22 @ X2)))) | ($false = (((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X1 @ Y0)))) @ (sK24 @ X1)))) | (((sK1 @ X4)) = $true) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ X2 @ X4))) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1559])).
% 0.20/0.34 thf(f1561,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK2 @ (sK22 @ X2)))) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ X2 @ X4))) | (((sK1 @ X3)) = $true) | ($false = (((sK2 @ (sK24 @ X1)) | (~ (irel @ X1 @ (sK24 @ X1)))))) | ($false = ((irel @ sK3 @ X1))) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1560])).
% 0.20/0.34 thf(f1563,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK1 @ X4)) = $true) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (sK24 @ X1)))) | ($false = ((sK2 @ (sK22 @ X2)))) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1561])).
% 0.20/0.34 thf(f1565,plain,(
% 0.20/0.34 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))) @ X1)) = $true) | ((((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0))))) & (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK3 @ Y0)) | ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK2 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) | (~ (irel @ Y0 @ Y1))))))))))) = $true)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1483])).
% 0.20/0.34 thf(f1567,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))))) = $true) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))) @ X1)) = $true)) )),
% 0.20/0.34 inference(and_proxy_clausification,[],[f1565])).
% 0.20/0.34 thf(f1568,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((sK2 @ Y1) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y0 @ Y2)) | (sK1 @ Y2)))))) | (~ (irel @ Y0 @ Y1))) | (~ (irel @ sK3 @ Y0)))))) @ X1)) = $true) | ($true = (((^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) | (~ (irel @ Y0 @ Y1)))))) | (~ (irel @ sK3 @ Y0)))) @ X2)))) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1567])).
% 0.20/0.34 thf(f1569,plain,(
% 0.20/0.34 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1))))))) | ($true = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ sK3 @ X2)))))) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1568])).
% 0.20/0.34 thf(f1570,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | ($true = ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))) | (~ (irel @ sK3 @ X2)))))) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1569])).
% 0.20/0.34 thf(f1571,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | (((~ (irel @ sK3 @ X2))) = $true) | ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1570])).
% 0.20/0.34 thf(f1572,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0))))))) = $true) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1571])).
% 0.20/0.34 thf(f1573,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0)))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1572])).
% 0.20/0.34 thf(f1574,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))))) = $true) | (((irel @ sK3 @ X2)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) = $false) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1573])).
% 0.20/0.34 thf(f1575,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))))) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))) @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(pi_proxy_clausification,[],[f1574])).
% 0.20/0.34 thf(f1576,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((^[Y0 : $i]: ((~ (irel @ X2 @ Y0)) | (sK1 @ Y0))) @ (sK25 @ X2))) = $false) | ((((^[Y0 : $i]: ((sK2 @ Y0) | (~ (irel @ X2 @ Y0)))) @ X4)) = $true) | ((((^[Y0 : $i]: ((((sK2 @ Y0) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ X1 @ Y1)) | (sK1 @ Y1)))))) | (~ (irel @ X1 @ Y0))) | (~ (irel @ sK3 @ X1)))) @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f1575])).
% 0.20/0.34 thf(f1577,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((sK2 @ X4) | (~ (irel @ X2 @ X4))))) | ((((((sK2 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1)))) = $true) | (((irel @ sK3 @ X2)) = $false) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false)) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1576])).
% 0.20/0.34 thf(f1578,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (((((((sK2 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X1 @ X3))) | (~ (irel @ sK3 @ X1)))) = $true) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | (((irel @ sK3 @ X2)) = $false) | (((~ (irel @ X2 @ X4))) = $true) | (((sK2 @ X4)) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1577])).
% 0.20/0.34 thf(f1579,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((((sK2 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0)))))) | (~ (irel @ X1 @ X3)))) = $true) | (((irel @ sK3 @ X2)) = $false) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | (((sK2 @ X4)) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | (((~ (irel @ X2 @ X4))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1578])).
% 0.20/0.34 thf(f1580,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((~ (irel @ X1 @ X3))) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | ((((sK2 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) = $true) | (((sK2 @ X4)) = $true) | (((~ (irel @ X2 @ X4))) = $true)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1579])).
% 0.20/0.34 thf(f1581,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X3)) = $false) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ X4)) = $true) | ((((sK2 @ X3) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) = $true) | (((~ (irel @ X2 @ X4))) = $true) | (((~ (irel @ sK3 @ X1))) = $true) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1580])).
% 0.20/0.34 thf(f1582,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((~ (irel @ X2 @ X4))) = $true) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) | (((irel @ X1 @ X3)) = $false) | ($true = ((sK2 @ X3))) | (((sK2 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | (((~ (irel @ sK3 @ X1))) = $true) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false)) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1581])).
% 0.20/0.34 thf(f1583,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((~ (irel @ sK3 @ X1))) = $true) | (((irel @ X1 @ X3)) = $false) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | (((sK2 @ X4)) = $true) | ($false = ((irel @ X2 @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) | ($true = ((sK2 @ X3))) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1582])).
% 0.20/0.34 thf(f1584,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK2 @ X3))) | (((sK2 @ X4)) = $true) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))))))) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | (((irel @ sK3 @ X2)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1583])).
% 0.20/0.34 thf(f1585,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((sK2 @ X4)) = $true) | ((((~ (irel @ X2 @ (sK25 @ X2))) | (sK1 @ (sK25 @ X2)))) = $false) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK2 @ X3))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0)))))) | ($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false)) )),
% 0.20/0.34 inference(not_proxy_clausification,[],[f1584])).
% 0.20/0.34 thf(f1586,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK1 @ (sK25 @ X2)))) | ($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false) | (((sK2 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0)))))) | ($true = ((sK2 @ X3)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1585])).
% 0.20/0.34 thf(f1594,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((irel @ X1 @ X3)) = $false) | (((sK2 @ X4)) = $true) | ($true = ((sK2 @ X3))) | ((((^[Y0 : $i]: ((~ (irel @ X1 @ Y0)) | (sK1 @ Y0))) @ (sK27 @ X1))) = $false) | ($false = ((irel @ X2 @ X4))) | ($false = ((sK1 @ (sK25 @ X2)))) | ($false = ((irel @ sK3 @ X1)))) )),
% 0.20/0.34 inference(sigma_proxy_clausification,[],[f1586])).
% 0.20/0.34 thf(f1595,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | ($false = (((~ (irel @ X1 @ (sK27 @ X1))) | (sK1 @ (sK27 @ X1))))) | ($false = ((sK1 @ (sK25 @ X2)))) | (((irel @ sK3 @ X2)) = $false) | (((sK2 @ X4)) = $true) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ X2 @ X4))) | ($true = ((sK2 @ X3)))) )),
% 0.20/0.34 inference(beta-eta_normalization,[],[f1594])).
% 0.20/0.34 thf(f1596,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | ($false = ((sK1 @ (sK25 @ X2)))) | (((irel @ X1 @ X3)) = $false) | (((sK2 @ X4)) = $true) | ($true = ((sK2 @ X3))) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ (sK27 @ X1))) = $false) | ($false = ((irel @ sK3 @ X1)))) )),
% 0.20/0.34 inference(or_proxy_clausification,[],[f1595])).
% 0.20/0.34 thf(f1638,definition,(
% 0.20/0.34 spl31_2 <=> (((sK1 @ sK8)) = $false)),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_2])],[avatar_definition])).
% 0.20/0.34 thf(f1640,plain,(
% 0.20/0.34 (((sK1 @ sK8)) = $false) | ~spl31_2),
% 0.20/0.34 inference(avatar_component_clause,[],[f1638])).
% 0.20/0.34 thf(f1646,definition,(
% 0.20/0.34 spl31_4 <=> ! [X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | (((sK1 @ X1)) = $true))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_4])],[avatar_definition])).
% 0.20/0.34 thf(f1647,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((sK1 @ X1)) = $true) | (((irel @ sK5 @ X1)) = $false)) ) | ~spl31_4),
% 0.20/0.34 inference(avatar_component_clause,[],[f1646])).
% 0.20/0.34 thf(f1650,definition,(
% 0.20/0.34 spl31_5 <=> ! [X2 : $i] : (($true = ((sK1 @ X2))) | ($false = ((irel @ sK6 @ X2))))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_5])],[avatar_definition])).
% 0.20/0.34 thf(f1651,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($true = ((sK1 @ X2))) | ($false = ((irel @ sK6 @ X2)))) ) | ~spl31_5),
% 0.20/0.34 inference(avatar_component_clause,[],[f1650])).
% 0.20/0.34 thf(f1666,definition,(
% 0.20/0.34 spl31_8 <=> ($true = ((irel @ sK3 @ sK6)))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition])).
% 0.20/0.34 thf(f1667,plain,(
% 0.20/0.34 ($true != ((irel @ sK3 @ sK6))) | spl31_8),
% 0.20/0.34 inference(avatar_component_clause,[],[f1666])).
% 0.20/0.34 thf(f1668,plain,(
% 0.20/0.34 ($true = ((irel @ sK3 @ sK6))) | ~spl31_8),
% 0.20/0.34 inference(avatar_component_clause,[],[f1666])).
% 0.20/0.34 thf(f1680,definition,(
% 0.20/0.34 spl31_10 <=> ! [X2 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK7 @ X2))))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_10])],[avatar_definition])).
% 0.20/0.34 thf(f1681,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($true = ((sK2 @ X2))) | ($false = ((irel @ sK7 @ X2)))) ) | ~spl31_10),
% 0.20/0.34 inference(avatar_component_clause,[],[f1680])).
% 0.20/0.34 thf(f1687,definition,(
% 0.20/0.34 spl31_11 <=> ! [X2 : $i] : (($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2))))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_11])],[avatar_definition])).
% 0.20/0.34 thf(f1688,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($false = ((irel @ sK4 @ X2))) | ($true = ((sK2 @ X2)))) ) | ~spl31_11),
% 0.20/0.34 inference(avatar_component_clause,[],[f1687])).
% 0.20/0.34 thf(f1690,plain,(
% 0.20/0.34 spl31_5 | spl31_4 | spl31_2 | spl31_11),
% 0.20/0.34 inference(avatar_split_clause,[],[f221,f1687,f1638,f1646,f1650])).
% 0.20/0.34 thf(f1699,plain,(
% 0.20/0.34 spl31_10 | spl31_5 | spl31_4 | spl31_11),
% 0.20/0.34 inference(avatar_split_clause,[],[f264,f1687,f1646,f1650,f1680])).
% 0.20/0.34 thf(f1746,definition,(
% 0.20/0.34 spl31_14 <=> ($false = ((sK2 @ sK12)))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_14])],[avatar_definition])).
% 0.20/0.34 thf(f1748,plain,(
% 0.20/0.34 ($false = ((sK2 @ sK12))) | ~spl31_14),
% 0.20/0.34 inference(avatar_component_clause,[],[f1746])).
% 0.20/0.34 thf(f1750,definition,(
% 0.20/0.34 spl31_15 <=> ($false = ((sK2 @ sK11)))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition])).
% 0.20/0.34 thf(f1752,plain,(
% 0.20/0.34 ($false = ((sK2 @ sK11))) | ~spl31_15),
% 0.20/0.34 inference(avatar_component_clause,[],[f1750])).
% 0.20/0.34 thf(f1826,definition,(
% 0.20/0.34 spl31_18 <=> (((sK1 @ sK13)) = $false)),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_18])],[avatar_definition])).
% 0.20/0.34 thf(f1828,plain,(
% 0.20/0.34 (((sK1 @ sK13)) = $false) | ~spl31_18),
% 0.20/0.34 inference(avatar_component_clause,[],[f1826])).
% 0.20/0.34 thf(f1829,plain,(
% 0.20/0.34 spl31_15 | spl31_18 | spl31_2 | spl31_14),
% 0.20/0.34 inference(avatar_split_clause,[],[f815,f1746,f1638,f1826,f1750])).
% 0.20/0.34 thf(f2011,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (sK22 @ X2)))) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ X4)) = $true) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ X2 @ X4)))) )),
% 0.20/0.34 inference(forward_demodulation,[],[f1563,f51])).
% 0.20/0.34 thf(f2016,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ sK3 @ X2)) = $false) | (((sK1 @ (sK27 @ X1))) = $false) | (((sK2 @ X4)) = $true) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | ($false = ((irel @ X2 @ X4))) | ($true = ((sK2 @ X3))) | (((irel @ X1 @ X3)) = $false)) )),
% 0.20/0.34 inference(forward_demodulation,[],[f1596,f51])).
% 0.20/0.34 thf(f2027,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | (((sK1 @ X3)) = $true) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | (((irel @ X1 @ X3)) = $false) | ($false = ((irel @ X2 @ X4))) | (((sK1 @ X4)) = $true) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ sK3 @ X1)))) )),
% 0.20/0.34 inference(forward_demodulation,[],[f2011,f51])).
% 0.20/0.34 thf(f2028,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((sK1 @ X3)) = $true) | (((sK1 @ X4)) = $true) | ($false = ((irel @ sK3 @ X1))) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false) | ($false = ((sK2 @ (d2unsorted @ d_unsorted_0))))) )),
% 0.20/0.34 inference(duplicate_literal_removal,[],[f2027])).
% 0.20/0.34 thf(f2033,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | (((sK2 @ X4)) = $true) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | (((irel @ sK3 @ X2)) = $false) | ($true = ((sK2 @ X3))) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | ($false = ((irel @ X2 @ X4))) | (((irel @ X1 @ X3)) = $false)) )),
% 0.20/0.34 inference(forward_demodulation,[],[f2016,f51])).
% 0.20/0.34 thf(f2034,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ sK3 @ X2)) = $false) | (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ sK3 @ X1))) | ($true = ((sK2 @ X3))) | (((irel @ X1 @ X3)) = $false) | (((sK2 @ X4)) = $true)) )),
% 0.20/0.34 inference(duplicate_literal_removal,[],[f2033])).
% 0.20/0.34 thf(f2040,definition,(
% 0.20/0.34 spl31_31 <=> ! [X2 : $i,X3 : $i] : (($false = ((irel @ X2 @ X3))) | (((sK1 @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_31])],[avatar_definition])).
% 0.20/0.34 thf(f2041,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i] : ((((sK1 @ X3)) = $true) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X3)))) ) | ~spl31_31),
% 0.20/0.34 inference(avatar_component_clause,[],[f2040])).
% 0.20/0.34 thf(f2046,definition,(
% 0.20/0.34 spl31_33 <=> ($false = ((sK2 @ (d2unsorted @ d_unsorted_0))))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_33])],[avatar_definition])).
% 0.20/0.34 thf(f2048,plain,(
% 0.20/0.34 ($false = ((sK2 @ (d2unsorted @ d_unsorted_0)))) | ~spl31_33),
% 0.20/0.34 inference(avatar_component_clause,[],[f2046])).
% 0.20/0.34 thf(f2055,definition,(
% 0.20/0.34 spl31_35 <=> (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false)),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_35])],[avatar_definition])).
% 0.20/0.34 thf(f2057,plain,(
% 0.20/0.34 (((sK1 @ (d2unsorted @ d_unsorted_0))) = $false) | ~spl31_35),
% 0.20/0.34 inference(avatar_component_clause,[],[f2055])).
% 0.20/0.34 thf(f2059,definition,(
% 0.20/0.34 spl31_36 <=> ! [X4 : $i,X1 : $i] : (($false = ((irel @ X1 @ X4))) | (((sK2 @ X4)) = $true) | ($false = ((irel @ sK3 @ X1))))),
% 0.20/0.34 introduced(definition,[new_symbols(definition,[spl31_36])],[avatar_definition])).
% 0.20/0.34 thf(f2060,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : (($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X1 @ X4))) | (((sK2 @ X4)) = $true)) ) | ~spl31_36),
% 0.20/0.34 inference(avatar_component_clause,[],[f2059])).
% 0.20/0.34 thf(f2065,plain,(
% 0.20/0.34 spl31_31 | spl31_33 | spl31_31),
% 0.20/0.34 inference(avatar_split_clause,[],[f2028,f2040,f2046,f2040])).
% 0.20/0.34 thf(f2070,plain,(
% 0.20/0.34 spl31_36 | spl31_36 | spl31_35),
% 0.20/0.34 inference(avatar_split_clause,[],[f2034,f2055,f2059,f2059])).
% 0.20/0.34 thf(f2078,plain,(
% 0.20/0.34 ( ! [X0 : $i] : (($false = ((sK1 @ X0)))) ) | ~spl31_35),
% 0.20/0.34 inference(constrained_superposition,[],[f2057,f51])).
% 0.20/0.34 thf(f2089,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i] : (($false = $true) | (((irel @ sK3 @ X2)) = $false) | ($false = ((irel @ X2 @ X3)))) ) | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(forward_demodulation,[],[f2041,f2078])).
% 0.20/0.34 thf(f2090,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i] : (($false = ((irel @ X2 @ X3))) | (((irel @ sK3 @ X2)) = $false)) ) | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2089])).
% 0.20/0.34 thf(f2149,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((irel @ sK5 @ X1)) = $false) | ($false = $true)) ) | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(forward_demodulation,[],[f1647,f2078])).
% 0.20/0.34 thf(f2150,plain,(
% 0.20/0.34 ( ! [X1 : $i] : ((((irel @ sK5 @ X1)) = $false)) ) | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2149])).
% 0.20/0.34 thf(f2151,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($false = $true) | ($false = ((irel @ sK6 @ X2)))) ) | (~spl31_5 | ~spl31_35)),
% 0.20/0.34 inference(forward_demodulation,[],[f1651,f2078])).
% 0.20/0.34 thf(f2152,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($false = ((irel @ sK6 @ X2)))) ) | (~spl31_5 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2151])).
% 0.20/0.34 thf(f2153,plain,(
% 0.20/0.34 ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | ~spl31_15),
% 0.20/0.34 inference(constrained_superposition,[],[f1752,f55])).
% 0.20/0.34 thf(f2174,plain,(
% 0.20/0.34 ( ! [X0 : $i] : ((((irel @ sK3 @ X0)) != $true)) ) | spl31_8),
% 0.20/0.34 inference(constrained_superposition,[],[f1667,f55])).
% 0.20/0.34 thf(f2191,plain,(
% 0.20/0.34 ($false = ((irel @ sK3 @ sK3))) | ($false != $false) | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(equality_factoring,[],[f2090])).
% 0.20/0.34 thf(f2197,plain,(
% 0.20/0.34 ($false = ((irel @ sK3 @ sK3))) | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2191])).
% 0.20/0.34 thf(f2202,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(forward_demodulation,[],[f2197,f81])).
% 0.20/0.34 thf(f2203,plain,(
% 0.20/0.34 $false | (~spl31_31 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2202])).
% 0.20/0.34 thf(f2204,plain,(
% 0.20/0.34 ~spl31_31 | ~spl31_35),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2203])).
% 0.20/0.34 thf(f2213,plain,(
% 0.20/0.34 ($true != $true) | spl31_8),
% 0.20/0.34 inference(constrained_superposition,[],[f2174,f81])).
% 0.20/0.34 thf(f2216,plain,(
% 0.20/0.34 $false | spl31_8),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2213])).
% 0.20/0.34 thf(f2217,plain,(
% 0.20/0.34 spl31_8),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2216])).
% 0.20/0.34 thf(f2221,plain,(
% 0.20/0.34 ( ! [X0 : $i] : ((((irel @ sK3 @ X0)) = $true)) ) | ~spl31_8),
% 0.20/0.34 inference(constrained_superposition,[],[f1668,f55])).
% 0.20/0.34 thf(f2229,plain,(
% 0.20/0.34 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ X1)))) ) | ~spl31_8),
% 0.20/0.34 inference(constrained_superposition,[],[f2221,f55])).
% 0.20/0.34 thf(f2245,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(constrained_superposition,[],[f2150,f81])).
% 0.20/0.34 thf(f2249,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(constrained_superposition,[],[f81,f2150])).
% 0.20/0.34 thf(f2258,plain,(
% 0.20/0.34 $false | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2245])).
% 0.20/0.34 thf(f2259,plain,(
% 0.20/0.34 ~spl31_4 | ~spl31_35),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2258])).
% 0.20/0.34 thf(f2262,plain,(
% 0.20/0.34 $false | (~spl31_4 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2249])).
% 0.20/0.34 thf(f2263,plain,(
% 0.20/0.34 ~spl31_4 | ~spl31_35),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2262])).
% 0.20/0.34 thf(f2267,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_5 | ~spl31_35)),
% 0.20/0.34 inference(constrained_superposition,[],[f2152,f81])).
% 0.20/0.34 thf(f2281,plain,(
% 0.20/0.34 $false | (~spl31_5 | ~spl31_35)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2267])).
% 0.20/0.34 thf(f2282,plain,(
% 0.20/0.34 ~spl31_5 | ~spl31_35),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2281])).
% 0.20/0.34 thf(f2309,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : ((((sK2 @ X4)) = $true) | ($false = $true) | ($false = ((irel @ X1 @ X4)))) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2060,f2229])).
% 0.20/0.34 thf(f2310,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : ((((sK2 @ X4)) = $true) | ($false = ((irel @ X1 @ X4)))) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2309])).
% 0.20/0.34 thf(f2311,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : (($false = $true) | ($false = ((irel @ X1 @ X4)))) ) | (~spl31_8 | ~spl31_15 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2310,f2153])).
% 0.20/0.34 thf(f2312,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : (($false = ((irel @ X1 @ X4)))) ) | (~spl31_8 | ~spl31_15 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2311])).
% 0.20/0.34 thf(f2313,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_15 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2312,f2229])).
% 0.20/0.34 thf(f2314,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_15 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2313])).
% 0.20/0.34 thf(f2315,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_15 | ~spl31_36),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2314])).
% 0.20/0.34 thf(f2321,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($true = ((sK2 @ X2))) | ($false = $true)) ) | (~spl31_8 | ~spl31_10)),
% 0.20/0.34 inference(forward_demodulation,[],[f1681,f2229])).
% 0.20/0.34 thf(f2322,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($true = ((sK2 @ X2)))) ) | (~spl31_8 | ~spl31_10)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2321])).
% 0.20/0.34 thf(f2332,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_10 | ~spl31_33)),
% 0.20/0.34 inference(forward_demodulation,[],[f2048,f2322])).
% 0.20/0.34 thf(f2333,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_10 | ~spl31_33)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2332])).
% 0.20/0.34 thf(f2334,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_10 | ~spl31_33),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2333])).
% 0.20/0.34 thf(f2335,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i] : (($false = $true) | ($false = ((irel @ X2 @ X3))) | (((sK1 @ X3)) = $true)) ) | (~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(forward_demodulation,[],[f2041,f2229])).
% 0.20/0.34 thf(f2336,plain,(
% 0.20/0.34 ( ! [X2 : $i,X3 : $i] : ((((sK1 @ X3)) = $true) | ($false = ((irel @ X2 @ X3)))) ) | (~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2335])).
% 0.20/0.34 thf(f2338,plain,(
% 0.20/0.34 ( ! [X3 : $i] : ((((sK1 @ X3)) = $true) | ($false = $true)) ) | (~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(forward_demodulation,[],[f2336,f2229])).
% 0.20/0.34 thf(f2339,plain,(
% 0.20/0.34 ( ! [X3 : $i] : ((((sK1 @ X3)) = $true)) ) | (~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2338])).
% 0.20/0.34 thf(f2340,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_2 | ~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(constrained_superposition,[],[f2339,f1640])).
% 0.20/0.34 thf(f2344,plain,(
% 0.20/0.34 $false | (~spl31_2 | ~spl31_8 | ~spl31_31)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2340])).
% 0.20/0.34 thf(f2345,plain,(
% 0.20/0.34 ~spl31_2 | ~spl31_8 | ~spl31_31),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2344])).
% 0.20/0.34 thf(f2346,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_18 | ~spl31_31)),
% 0.20/0.34 inference(forward_demodulation,[],[f1828,f2339])).
% 0.20/0.34 thf(f2347,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_18 | ~spl31_31)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2346])).
% 0.20/0.34 thf(f2348,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_18 | ~spl31_31),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2347])).
% 0.20/0.34 thf(f2350,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : (($false = ((irel @ X1 @ X4))) | (((sK2 @ X4)) = $true) | ($false = $true)) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2060,f2229])).
% 0.20/0.34 thf(f2351,plain,(
% 0.20/0.34 ( ! [X1 : $i,X4 : $i] : ((((sK2 @ X4)) = $true) | ($false = ((irel @ X1 @ X4)))) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2350])).
% 0.20/0.34 thf(f2353,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($false = $true) | ($true = ((sK2 @ X2)))) ) | (~spl31_8 | ~spl31_11)),
% 0.20/0.34 inference(forward_demodulation,[],[f1688,f2229])).
% 0.20/0.34 thf(f2354,plain,(
% 0.20/0.34 ( ! [X2 : $i] : (($true = ((sK2 @ X2)))) ) | (~spl31_8 | ~spl31_11)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2353])).
% 0.20/0.34 thf(f2355,plain,(
% 0.20/0.34 ( ! [X4 : $i] : ((((sK2 @ X4)) = $true) | ($false = $true)) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2351,f2229])).
% 0.20/0.34 thf(f2356,plain,(
% 0.20/0.34 ( ! [X4 : $i] : ((((sK2 @ X4)) = $true)) ) | (~spl31_8 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2355])).
% 0.20/0.34 thf(f2357,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_14 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f1748,f2356])).
% 0.20/0.34 thf(f2358,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_14 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2357])).
% 0.20/0.34 thf(f2359,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_14 | ~spl31_36),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2358])).
% 0.20/0.34 thf(f2361,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_33 | ~spl31_36)),
% 0.20/0.34 inference(forward_demodulation,[],[f2048,f2356])).
% 0.20/0.34 thf(f2362,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_33 | ~spl31_36)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2361])).
% 0.20/0.34 thf(f2363,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_33 | ~spl31_36),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2362])).
% 0.20/0.34 thf(f2376,plain,(
% 0.20/0.34 ($false = $true) | (~spl31_8 | ~spl31_11 | ~spl31_33)),
% 0.20/0.34 inference(forward_demodulation,[],[f2048,f2354])).
% 0.20/0.34 thf(f2377,plain,(
% 0.20/0.34 $false | (~spl31_8 | ~spl31_11 | ~spl31_33)),
% 0.20/0.34 inference(trivial_inequality_removal,[],[f2376])).
% 0.20/0.34 thf(f2378,plain,(
% 0.20/0.34 ~spl31_8 | ~spl31_11 | ~spl31_33),
% 0.20/0.34 inference(avatar_contradiction_clause,[],[f2377])).
% 0.20/0.34 cnf(s18, plain, spl31_2 | spl31_4 | spl31_5 | spl31_11, inference(sat_conversion,[],[f1690])).
% 0.20/0.34 cnf(s27, plain, spl31_4 | spl31_5 | spl31_10 | spl31_11, inference(sat_conversion,[],[f1699])).
% 0.20/0.34 cnf(s129, plain, spl31_2 | spl31_14 | spl31_15 | spl31_18, inference(sat_conversion,[],[f1829])).
% 0.20/0.34 cnf(s264, plain, spl31_31 | spl31_31 | spl31_33, inference(sat_conversion,[],[f2065])).
% 0.20/0.34 cnf(s265, plain, spl31_31 | spl31_33, inference(rat,[],[s264])).
% 0.20/0.34 cnf(s271, plain, spl31_36 | spl31_35 | spl31_36, inference(sat_conversion,[],[f2070])).
% 0.20/0.34 cnf(s272, plain, spl31_35 | spl31_36, inference(rat,[],[s271])).
% 0.20/0.34 cnf(s292, plain, ~spl31_31 | ~spl31_35, inference(sat_conversion,[],[f2204])).
% 0.20/0.34 cnf(s295, plain, spl31_8, inference(sat_conversion,[],[f2217])).
% 0.20/0.34 cnf(s300, plain, ~spl31_4 | ~spl31_35, inference(sat_conversion,[],[f2259])).
% 0.20/0.34 cnf(s302, plain, ~spl31_4 | ~spl31_35, inference(sat_conversion,[],[f2263])).
% 0.20/0.34 cnf(s305, plain, ~spl31_5 | ~spl31_35, inference(sat_conversion,[],[f2282])).
% 0.20/0.34 cnf(s312, plain, ~spl31_8 | ~spl31_15 | ~spl31_36, inference(sat_conversion,[],[f2315])).
% 0.20/0.34 cnf(s315, plain, ~spl31_8 | ~spl31_10 | ~spl31_33, inference(sat_conversion,[],[f2334])).
% 0.20/0.34 cnf(s317, plain, ~spl31_2 | ~spl31_8 | ~spl31_31, inference(sat_conversion,[],[f2345])).
% 0.20/0.34 cnf(s318, plain, ~spl31_8 | ~spl31_18 | ~spl31_31, inference(sat_conversion,[],[f2348])).
% 0.20/0.34 cnf(s319, plain, ~spl31_8 | ~spl31_14 | ~spl31_36, inference(sat_conversion,[],[f2359])).
% 0.20/0.34 cnf(s320, plain, ~spl31_8 | ~spl31_33 | ~spl31_36, inference(sat_conversion,[],[f2363])).
% 0.20/0.34 cnf(s321, plain, ~spl31_8 | ~spl31_11 | ~spl31_33, inference(sat_conversion,[],[f2378])).
% 0.20/0.34 cnf(s338, plain, ~spl31_36 | spl31_2, inference(rat,[],[s318,s129,s265,s312,s319,s320,s295])).
% 0.20/0.34 cnf(s339, plain, spl31_2, inference(rat,[],[s321,s265,s18,s292,s302,s305,s272,s338,s295])).
% 0.20/0.34 cnf(s340, plain, ~spl31_31, inference(rat,[],[s317,s295,s339])).
% 0.20/0.34 cnf(s341, plain, spl31_33, inference(rat,[],[s265,s340])).
% 0.20/0.34 cnf(s342, plain, ~spl31_36, inference(rat,[],[s320,s295,s341])).
% 0.20/0.34 cnf(s343, plain, ~spl31_11, inference(rat,[],[s321,s295,s341])).
% 0.20/0.34 cnf(s344, plain, ~spl31_10, inference(rat,[],[s315,s295,s341])).
% 0.20/0.34 cnf(s345, plain, spl31_35, inference(rat,[],[s272,s342])).
% 0.20/0.34 cnf(s346, plain, ~spl31_5, inference(rat,[],[s305,s345])).
% 0.20/0.34 cnf(s347, plain, ~spl31_4, inference(rat,[],[s300,s345])).
% 0.20/0.34 cnf(s348, plain, $false, inference(rat,[],[s27,s343,s346,s347,s344])).
% 0.20/0.34 thf(f2379,plain,(
% 0.20/0.34 $false),
% 0.20/0.34 inference(avatar_sat_refutation,[],[s348])).
% 0.20/0.34 % SZS output end Proof for theBenchmark
% 0.20/0.34 % (1479230)------------------------------
% 0.20/0.34 % (1479230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (1479230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (1479230)CaDiCaL version: 2.1.3
% 0.20/0.34 % (1479230)Termination reason: Refutation
% 0.20/0.34 % (1479230)Time elapsed: 0.060 s
% 0.20/0.34 % (1479230)Peak memory usage: 14 MB
% 0.20/0.34 % (1479230)Instructions burned: 130 (million)
% 0.20/0.34 % (1479219)Success in time 0.118 s
% 0.20/0.34 % Vampire exiting
%------------------------------------------------------------------------------