%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO064^4.002 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:51 AM UTC 2026
% Result : Theorem 3.74s 1.03s
% Output : Refutation 3.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO064^4.002 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n004.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 16:26:22 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.74/1.01 % (1511647)Will run a generic schedule for satisfiability detection.
% 3.74/1.01 % (1511652)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=682739647_2999 on theBenchmark for (2999ds/0Mi)
% 3.74/1.01 % Exception at run slice level
% 3.74/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.01 % (1511653)% WARNING: option uhcvi not known.
% 3.74/1.01 % (1511653)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1221373908:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.74/1.01 % (1511653)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.01 % (1511653)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.74/1.01 % (1511660)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1215565499:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.74/1.01 % Exception at run slice level
% 3.74/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.01 % (1511656)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1101361586:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.74/1.01 % (1511656)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.01 % (1511654)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1702054939:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.74/1.01 % (1511663)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=540675677:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.74/1.01 % (1511657)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1497532585:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.74/1.01 % (1511655)dis+10_1_sil=32000:sp=arity:random_seed=4001601567:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.74/1.01 % (1511658)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4095264168:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.74/1.01 % (1511663)Instruction limit reached!
% 3.74/1.01 % (1511663)------------------------------
% 3.74/1.01 % (1511663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (1511663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (1511663)CaDiCaL version: 2.1.3
% 3.74/1.01 % (1511663)Termination reason: Instruction limit
% 3.74/1.01 % (1511663)Termination phase: Saturation
% 3.74/1.01 % (1511663)Time elapsed: 0.032 s
% 3.74/1.01 % (1511663)Peak memory usage: 12 MB
% 3.74/1.01 % (1511663)Instructions burned: 132 (million)
% 3.74/1.01 % (1511670)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2828441680:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.74/1.01 % (1511670)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.01 % (1511670)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.74/1.01 % (1511656)Instruction limit reached!
% 3.74/1.01 % (1511656)------------------------------
% 3.74/1.01 % (1511656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (1511656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (1511656)CaDiCaL version: 2.1.3
% 3.74/1.01 % (1511656)Termination reason: Instruction limit
% 3.74/1.01 % (1511656)Termination phase: Saturation
% 3.74/1.01 % (1511656)Time elapsed: 0.096 s
% 3.74/1.01 % (1511656)Peak memory usage: 12 MB
% 3.74/1.01 % (1511656)Instructions burned: 116 (million)
% 3.74/1.01 % (1511655)Instruction limit reached!
% 3.74/1.01 % (1511655)------------------------------
% 3.74/1.01 % (1511655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (1511655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (1511655)CaDiCaL version: 2.1.3
% 3.74/1.01 % (1511655)Termination reason: Instruction limit
% 3.74/1.01 % (1511655)Termination phase: Saturation
% 3.74/1.01 % (1511655)Time elapsed: 0.089 s
% 3.74/1.01 % (1511655)Peak memory usage: 12 MB
% 3.74/1.01 % (1511655)Instructions burned: 104 (million)
% 3.74/1.01 % (1511657)Instruction limit reached!
% 3.74/1.01 % (1511657)------------------------------
% 3.74/1.01 % (1511657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511657)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511657)Termination reason: Instruction limit
% 3.74/1.03 % (1511657)Termination phase: Saturation
% 3.74/1.03 % (1511657)Time elapsed: 0.101 s
% 3.74/1.03 % (1511657)Peak memory usage: 12 MB
% 3.74/1.03 % (1511657)Instructions burned: 132 (million)
% 3.74/1.03 % (1511672)ott-21_1_sil=16000:fs=off:random_seed=478916452:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.74/1.03 % (1511673)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2586665508:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.74/1.03 % (1511674)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2794347481:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511658)Instruction limit reached!
% 3.74/1.03 % (1511658)------------------------------
% 3.74/1.03 % (1511658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511658)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511658)Termination reason: Instruction limit
% 3.74/1.03 % (1511658)Termination phase: Saturation
% 3.74/1.03 % (1511658)Time elapsed: 0.134 s
% 3.74/1.03 % (1511658)Peak memory usage: 12 MB
% 3.74/1.03 % (1511658)Instructions burned: 159 (million)
% 3.74/1.03 % (1511678)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2871516235:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.74/1.03 % (1511679)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3159577341:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511670)Instruction limit reached!
% 3.74/1.03 % (1511670)------------------------------
% 3.74/1.03 % (1511670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511670)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511670)Termination reason: Instruction limit
% 3.74/1.03 % (1511670)Termination phase: Saturation
% 3.74/1.03 % (1511670)Time elapsed: 0.156 s
% 3.74/1.03 % (1511670)Peak memory usage: 14 MB
% 3.74/1.03 % (1511670)Instructions burned: 688 (million)
% 3.74/1.03 % (1511683)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=106884524:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 3.74/1.03 % (1511683)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.03 % (1511682)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3475035050:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 3.74/1.03 % (1511682)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.03 % (1511672)Instruction limit reached!
% 3.74/1.03 % (1511672)------------------------------
% 3.74/1.03 % (1511672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511672)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511672)Termination reason: Instruction limit
% 3.74/1.03 % (1511672)Termination phase: Saturation
% 3.74/1.03 % (1511672)Time elapsed: 0.112 s
% 3.74/1.03 % (1511672)Peak memory usage: 12 MB
% 3.74/1.03 % (1511672)Instructions burned: 180 (million)
% 3.74/1.03 % (1511686)fmb+10_1_sil=64000:random_seed=1684495227:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 3.74/1.03 % (1511686)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511688)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=358974775:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511690)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2842325147:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511692)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2745277504:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 3.74/1.03 % (1511692)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.03 % (1511683)Instruction limit reached!
% 3.74/1.03 % (1511683)------------------------------
% 3.74/1.03 % (1511683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511683)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511683)Termination reason: Instruction limit
% 3.74/1.03 % (1511683)Termination phase: Saturation
% 3.74/1.03 % (1511683)Time elapsed: 0.212 s
% 3.74/1.03 % (1511683)Peak memory usage: 14 MB
% 3.74/1.03 % (1511683)Instructions burned: 881 (million)
% 3.74/1.03 % (1511694)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=922718965:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 3.74/1.03 % (1511694)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.74/1.03 % (1511694)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.74/1.03 % (1511673)Instruction limit reached!
% 3.74/1.03 % (1511673)------------------------------
% 3.74/1.03 % (1511673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511673)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511673)Termination reason: Instruction limit
% 3.74/1.03 % (1511673)Termination phase: Saturation
% 3.74/1.03 % (1511673)Time elapsed: 0.358 s
% 3.74/1.03 % (1511673)Peak memory usage: 13 MB
% 3.74/1.03 % (1511673)Instructions burned: 477 (million)
% 3.74/1.03 % (1511696)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2680449209:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511698)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1732464063:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511700)ott-2_1_sil=16000:newcnf=on:random_seed=4281450834:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 3.74/1.03 % (1511700)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.74/1.03 % (1511678)Instruction limit reached!
% 3.74/1.03 % (1511678)------------------------------
% 3.74/1.03 % (1511678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511678)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511678)Termination reason: Instruction limit
% 3.74/1.03 % (1511678)Termination phase: Saturation
% 3.74/1.03 % (1511678)Time elapsed: 0.501 s
% 3.74/1.03 % (1511678)Peak memory usage: 13 MB
% 3.74/1.03 % (1511678)Instructions burned: 1179 (million)
% 3.74/1.03 % (1511702)ott+10_1_sil=32000:tgt=ground:random_seed=254013687:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 3.74/1.03 % (1511682)Instruction limit reached!
% 3.74/1.03 % (1511682)------------------------------
% 3.74/1.03 % (1511682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511682)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511682)Termination reason: Instruction limit
% 3.74/1.03 % (1511682)Termination phase: Saturation
% 3.74/1.03 % (1511682)Time elapsed: 0.461 s
% 3.74/1.03 % (1511682)Peak memory usage: 14 MB
% 3.74/1.03 % (1511682)Instructions burned: 692 (million)
% 3.74/1.03 % (1511704)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2556309311:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 3.74/1.03 % Exception at run slice level
% 3.74/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.74/1.03 % (1511700) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1511647-1511700"...
% 3.74/1.03 % (1511700)...printing done.
% 3.74/1.03 % (1511700)Refutation found. Thanks to Tanya!
% 3.74/1.03 % SZS status Theorem for theBenchmark
% 3.74/1.03 % SZS output start Proof for theBenchmark
% 3.74/1.03 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 3.74/1.03 thf(func_def_0, type, irel: ($i > $i > $o)).
% 3.74/1.03 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_9, type, itrue: ($i > $o)).
% 3.74/1.03 thf(func_def_10, type, ifalse: ($i > $o)).
% 3.74/1.03 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.74/1.03 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 3.74/1.03 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 3.74/1.03 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 3.74/1.03 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 3.74/1.03 thf(func_def_21, type, a: ($i > $o)).
% 3.74/1.03 thf(func_def_22, type, a1: ($i > $o)).
% 3.74/1.03 thf(func_def_23, type, a2: ($i > $o)).
% 3.74/1.03 thf(func_def_24, type, b: ($i > $o)).
% 3.74/1.03 thf(func_def_25, type, b1: ($i > $o)).
% 3.74/1.03 thf(func_def_28, type, vNOT: ($o > $o)).
% 3.74/1.03 thf(func_def_29, type, db1: !>[X0: $tType]:(X0)).
% 3.74/1.03 thf(func_def_30, type, db0: !>[X0: $tType]:(X0)).
% 3.74/1.03 thf(func_def_31, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.74/1.03 thf(func_def_32, type, vOR: ($o > $o > $o)).
% 3.74/1.03 thf(func_def_33, type, db2: !>[X0: $tType]:(X0)).
% 3.74/1.03 thf(func_def_34, type, vAND: ($o > $o > $o)).
% 3.74/1.03 thf(func_def_35, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.74/1.03 thf(func_def_36, type, vIMP: ($o > $o > $o)).
% 3.74/1.03 thf(func_def_37, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.74/1.03 thf(func_def_43, type, sK5: ($i > $i)).
% 3.74/1.03 thf(f1,axiom,(
% 3.74/1.03 ! [X0 : $i] : (irel @ X0 @ X0)),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 3.74/1.03 thf(f2,axiom,(
% 3.74/1.03 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 3.74/1.03 thf(f3,axiom,(
% 3.74/1.03 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mnot)).
% 3.74/1.03 thf(f4,axiom,(
% 3.74/1.03 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mor)).
% 3.74/1.03 thf(f5,axiom,(
% 3.74/1.03 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mand)).
% 3.74/1.03 thf(f6,axiom,(
% 3.74/1.03 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mimplies)).
% 3.74/1.03 thf(f7,axiom,(
% 3.74/1.03 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 3.74/1.03 thf(f8,axiom,(
% 3.74/1.03 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iatom)).
% 3.74/1.03 thf(f12,axiom,(
% 3.74/1.03 (iand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ X0 @ X1))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iand)).
% 3.74/1.03 thf(f13,axiom,(
% 3.74/1.03 (ior = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ior)).
% 3.74/1.03 thf(f14,axiom,(
% 3.74/1.03 (iimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iimplies)).
% 3.74/1.03 thf(f18,axiom,(
% 3.74/1.03 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 3.74/1.03 thf(f22,axiom,(
% 3.74/1.03 (ivalid @ (iatom @ a2))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom1)).
% 3.74/1.03 thf(f23,axiom,(
% 3.74/1.03 (ivalid @ (iimplies @ (iatom @ b) @ (ior @ (ior @ (iatom @ b1) @ (iatom @ a1)) @ (iatom @ b1))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom2)).
% 3.74/1.03 thf(f24,axiom,(
% 3.74/1.03 (ivalid @ (ior @ (ior @ (iatom @ b) @ (iatom @ a)) @ (iatom @ b)))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom3)).
% 3.74/1.03 thf(f25,conjecture,(
% 3.74/1.03 (ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))),
% 3.74/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 3.74/1.03 thf(f26,negated_conjecture,(
% 3.74/1.03 ~(ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))),
% 3.74/1.03 inference(negated_conjecture,[status(cth)],[f25])).
% 3.74/1.03 thf(f27,plain,(
% 3.74/1.03 ! [X0 : $i] : (irel @ X0 @ X0)),
% 3.74/1.03 inference(rectify,[],[f1])).
% 3.74/1.03 thf(f28,plain,(
% 3.74/1.03 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 3.74/1.03 inference(fool_elimination,[],[f27])).
% 3.74/1.03 thf(f29,plain,(
% 3.74/1.03 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 3.74/1.03 inference(rectify,[],[f2])).
% 3.74/1.03 thf(f30,plain,(
% 3.74/1.03 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 3.74/1.03 inference(fool_elimination,[],[f29])).
% 3.74/1.03 thf(f31,plain,(
% 3.74/1.03 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.74/1.03 inference(rectify,[],[f3])).
% 3.74/1.03 thf(f32,plain,(
% 3.74/1.03 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.74/1.03 inference(fool_elimination,[],[f31])).
% 3.74/1.03 thf(f33,plain,(
% 3.74/1.03 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 3.74/1.03 inference(rectify,[],[f4])).
% 3.74/1.03 thf(f34,plain,(
% 3.74/1.03 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 3.74/1.03 inference(fool_elimination,[],[f33])).
% 3.74/1.03 thf(f35,plain,(
% 3.74/1.03 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 3.74/1.03 inference(rectify,[],[f5])).
% 3.74/1.03 thf(f36,plain,(
% 3.74/1.03 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 3.74/1.03 inference(fool_elimination,[],[f35])).
% 3.74/1.03 thf(f37,plain,(
% 3.74/1.03 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.74/1.03 inference(fool_elimination,[],[f6])).
% 3.74/1.03 thf(f38,plain,(
% 3.74/1.03 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 3.74/1.03 inference(rectify,[],[f7])).
% 3.74/1.03 thf(f39,plain,(
% 3.74/1.03 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 3.74/1.03 inference(fool_elimination,[],[f38])).
% 3.74/1.03 thf(f40,plain,(
% 3.74/1.03 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 3.74/1.03 inference(fool_elimination,[],[f8])).
% 3.74/1.03 thf(f43,plain,(
% 3.74/1.03 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 3.74/1.03 inference(fool_elimination,[],[f12])).
% 3.74/1.03 thf(f44,plain,(
% 3.74/1.03 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.74/1.03 inference(fool_elimination,[],[f13])).
% 3.74/1.03 thf(f45,plain,(
% 3.74/1.03 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.74/1.03 inference(fool_elimination,[],[f14])).
% 3.74/1.03 thf(f49,plain,(
% 3.74/1.03 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 3.74/1.03 inference(rectify,[],[f18])).
% 3.74/1.03 thf(f50,plain,(
% 3.74/1.03 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.74/1.03 inference(fool_elimination,[],[f49])).
% 3.74/1.03 thf(f57,plain,(
% 3.74/1.03 (ivalid @ (iatom @ a2))),
% 3.74/1.03 inference(rectify,[],[f22])).
% 3.74/1.03 thf(f58,plain,(
% 3.74/1.03 (((ivalid @ (iatom @ a2))) = $true)),
% 3.74/1.03 inference(fool_elimination,[],[f57])).
% 3.74/1.03 thf(f59,plain,(
% 3.74/1.03 (ivalid @ (iimplies @ (iatom @ b) @ (ior @ (ior @ (iatom @ b1) @ (iatom @ a1)) @ (iatom @ b1))))),
% 3.74/1.03 inference(rectify,[],[f23])).
% 3.74/1.03 thf(f60,plain,(
% 3.74/1.03 (((ivalid @ (iimplies @ (iatom @ b) @ (ior @ (ior @ (iatom @ b1) @ (iatom @ a1)) @ (iatom @ b1))))) = $true)),
% 3.74/1.03 inference(fool_elimination,[],[f59])).
% 3.74/1.03 thf(f61,plain,(
% 3.74/1.03 (ivalid @ (ior @ (ior @ (iatom @ b) @ (iatom @ a)) @ (iatom @ b)))),
% 3.74/1.03 inference(rectify,[],[f24])).
% 3.74/1.03 thf(f62,plain,(
% 3.74/1.03 (((ivalid @ (ior @ (ior @ (iatom @ b) @ (iatom @ a)) @ (iatom @ b)))) = $true)),
% 3.74/1.03 inference(fool_elimination,[],[f61])).
% 3.74/1.03 thf(f63,plain,(
% 3.74/1.03 ~(ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))),
% 3.74/1.03 inference(rectify,[],[f26])).
% 3.74/1.03 thf(f64,plain,(
% 3.74/1.03 ~ (((ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))) = $true)),
% 3.74/1.03 inference(fool_elimination,[],[f63])).
% 3.74/1.03 thf(f65,plain,(
% 3.74/1.03 (((ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))) != $true)),
% 3.74/1.03 inference(flattening,[],[f64])).
% 3.74/1.03 thf(f66,plain,(
% 3.74/1.03 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 3.74/1.03 inference(ennf_transformation,[],[f30])).
% 3.74/1.03 thf(f67,plain,(
% 3.74/1.03 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 3.74/1.03 inference(flattening,[],[f66])).
% 3.74/1.03 thf(f68,plain,(
% 3.74/1.03 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 3.74/1.03 inference(cnf_transformation,[],[f28])).
% 3.74/1.03 thf(f69,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) )),
% 3.74/1.03 inference(cnf_transformation,[],[f67])).
% 3.74/1.03 thf(f70,plain,(
% 3.74/1.03 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f32])).
% 3.74/1.03 thf(f71,plain,(
% 3.74/1.03 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f34])).
% 3.74/1.03 thf(f72,plain,(
% 3.74/1.03 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f36])).
% 3.74/1.03 thf(f73,plain,(
% 3.74/1.03 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.74/1.03 inference(cnf_transformation,[],[f37])).
% 3.74/1.03 thf(f74,plain,(
% 3.74/1.03 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f39])).
% 3.74/1.03 thf(f75,plain,(
% 3.74/1.03 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 3.74/1.03 inference(cnf_transformation,[],[f40])).
% 3.74/1.03 thf(f79,plain,(
% 3.74/1.03 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 3.74/1.03 inference(cnf_transformation,[],[f43])).
% 3.74/1.03 thf(f80,plain,(
% 3.74/1.03 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f44])).
% 3.74/1.03 thf(f81,plain,(
% 3.74/1.03 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.74/1.03 inference(cnf_transformation,[],[f45])).
% 3.74/1.03 thf(f85,plain,(
% 3.74/1.03 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.74/1.03 inference(cnf_transformation,[],[f50])).
% 3.74/1.03 thf(f89,plain,(
% 3.74/1.03 (((ivalid @ (iatom @ a2))) = $true)),
% 3.74/1.03 inference(cnf_transformation,[],[f58])).
% 3.74/1.03 thf(f90,plain,(
% 3.74/1.03 (((ivalid @ (iimplies @ (iatom @ b) @ (ior @ (ior @ (iatom @ b1) @ (iatom @ a1)) @ (iatom @ b1))))) = $true)),
% 3.74/1.03 inference(cnf_transformation,[],[f60])).
% 3.74/1.03 thf(f91,plain,(
% 3.74/1.03 (((ivalid @ (ior @ (ior @ (iatom @ b) @ (iatom @ a)) @ (iatom @ b)))) = $true)),
% 3.74/1.03 inference(cnf_transformation,[],[f62])).
% 3.74/1.03 thf(f92,plain,(
% 3.74/1.03 (((ivalid @ (ior @ (iatom @ a) @ (ior @ (iand @ (iatom @ b) @ (iatom @ a1)) @ (iand @ (iatom @ b1) @ (iatom @ a2)))))) != $true)),
% 3.74/1.03 inference(cnf_transformation,[],[f65])).
% 3.74/1.03 thf(f94,definition,(
% 3.74/1.03 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.74/1.03 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.74/1.03 thf(f95,plain,(
% 3.74/1.03 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))))),
% 3.74/1.03 inference(definition_unfolding,[],[f73,f71,f70])).
% 3.74/1.03 thf(f98,plain,(
% 3.74/1.03 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))))),
% 3.74/1.03 inference(definition_unfolding,[],[f79,f72])).
% 3.74/1.03 thf(f99,plain,(
% 3.74/1.03 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 3.74/1.03 inference(definition_unfolding,[],[f80,f71,f74,f74])).
% 3.74/1.03 thf(f100,plain,(
% 3.74/1.03 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 3.74/1.03 inference(definition_unfolding,[],[f81,f95,f74,f74])).
% 3.74/1.03 thf(f104,plain,(
% 3.74/1.03 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ a2))))),
% 3.74/1.03 inference(definition_unfolding,[],[f89,f85,f75])).
% 3.74/1.03 thf(f105,plain,(
% 3.74/1.03 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ b) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ b1) @ ((^[Y0 : $i > $o]: (Y0)) @ a1)) @ ((^[Y0 : $i > $o]: (Y0)) @ b1))))))),
% 3.74/1.03 inference(definition_unfolding,[],[f90,f85,f100,f75,f99,f99,f75,f75,f75])).
% 3.74/1.03 thf(f106,plain,(
% 3.74/1.03 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ b) @ ((^[Y0 : $i > $o]: (Y0)) @ a)) @ ((^[Y0 : $i > $o]: (Y0)) @ b)))))),
% 3.74/1.03 inference(definition_unfolding,[],[f91,f85,f99,f99,f75,f75,f75])).
% 3.74/1.03 thf(f107,plain,(
% 3.74/1.03 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ a) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ b) @ ((^[Y0 : $i > $o]: (Y0)) @ a1)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ b1) @ ((^[Y0 : $i > $o]: (Y0)) @ a2)))))))),
% 3.74/1.03 inference(definition_unfolding,[],[f92,f85,f99,f75,f99,f98,f75,f75,f98,f75,f75])).
% 3.74/1.03 thf(f108,plain,(
% 3.74/1.03 ($true != ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((b @ Y2) & (a1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((b1 @ Y2) & (a2 @ Y2))))))))))))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f107])).
% 3.74/1.03 thf(f109,plain,(
% 3.74/1.03 ($false = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((b @ Y2) & (a1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((b1 @ Y2) & (a2 @ Y2))))))))))) @ sK0)))),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f108])).
% 3.74/1.03 thf(f110,plain,(
% 3.74/1.03 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (a @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b @ Y1) & (a1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b1 @ Y1) & (a2 @ Y1))))))))))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f109])).
% 3.74/1.03 thf(f111,plain,(
% 3.74/1.03 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b @ Y1) & (a1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b1 @ Y1) & (a2 @ Y1)))))))))))),
% 3.74/1.03 inference(or_proxy_clausification,[],[f110])).
% 3.74/1.03 thf(f112,plain,(
% 3.74/1.03 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (a @ Y0))))))),
% 3.74/1.03 inference(or_proxy_clausification,[],[f110])).
% 3.74/1.03 thf(f113,plain,(
% 3.74/1.03 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (a @ Y0))) @ sK1)))),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f112])).
% 3.74/1.03 thf(f114,plain,(
% 3.74/1.03 ($false = (((irel @ sK0 @ sK1) => (a @ sK1))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f113])).
% 3.74/1.03 thf(f115,plain,(
% 3.74/1.03 ($false = ((a @ sK1)))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f114])).
% 3.74/1.03 thf(f116,plain,(
% 3.74/1.03 ($true = ((irel @ sK0 @ sK1)))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f114])).
% 3.74/1.03 thf(f117,plain,(
% 3.74/1.03 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b @ Y1) & (a1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((b1 @ Y1) & (a2 @ Y1)))))))) @ sK2)))),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f111])).
% 3.74/1.03 thf(f118,plain,(
% 3.74/1.03 ($false = (((irel @ sK0 @ sK2) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b @ Y0) & (a1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b1 @ Y0) & (a2 @ Y0)))))))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f117])).
% 3.74/1.03 thf(f119,plain,(
% 3.74/1.03 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b @ Y0) & (a1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b1 @ Y0) & (a2 @ Y0))))))))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f118])).
% 3.74/1.03 thf(f120,plain,(
% 3.74/1.03 ($true = ((irel @ sK0 @ sK2)))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f118])).
% 3.74/1.03 thf(f121,plain,(
% 3.74/1.03 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b1 @ Y0) & (a2 @ Y0)))))))),
% 3.74/1.03 inference(or_proxy_clausification,[],[f119])).
% 3.74/1.03 thf(f122,plain,(
% 3.74/1.03 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b @ Y0) & (a1 @ Y0)))))))),
% 3.74/1.03 inference(or_proxy_clausification,[],[f119])).
% 3.74/1.03 thf(f123,plain,(
% 3.74/1.03 ($false = (((^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b @ Y0) & (a1 @ Y0)))) @ sK3)))),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f122])).
% 3.74/1.03 thf(f124,plain,(
% 3.74/1.03 ($false = (((irel @ sK2 @ sK3) => ((b @ sK3) & (a1 @ sK3)))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f123])).
% 3.74/1.03 thf(f125,plain,(
% 3.74/1.03 ($false = (((b @ sK3) & (a1 @ sK3))))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f124])).
% 3.74/1.03 thf(f126,plain,(
% 3.74/1.03 ($true = ((irel @ sK2 @ sK3)))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f124])).
% 3.74/1.03 thf(f127,plain,(
% 3.74/1.03 ($false = ((a1 @ sK3))) | ($false = ((b @ sK3)))),
% 3.74/1.03 inference(and_proxy_clausification,[],[f125])).
% 3.74/1.03 thf(f128,plain,(
% 3.74/1.03 ($false = (((^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((b1 @ Y0) & (a2 @ Y0)))) @ sK4)))),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f121])).
% 3.74/1.03 thf(f129,plain,(
% 3.74/1.03 ($false = (((irel @ sK2 @ sK4) => ((b1 @ sK4) & (a2 @ sK4)))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f128])).
% 3.74/1.03 thf(f130,plain,(
% 3.74/1.03 ($false = (((b1 @ sK4) & (a2 @ sK4))))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f129])).
% 3.74/1.03 thf(f131,plain,(
% 3.74/1.03 ($true = ((irel @ sK2 @ sK4)))),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f129])).
% 3.74/1.03 thf(f132,plain,(
% 3.74/1.03 ($false = ((a2 @ sK4))) | ($false = ((b1 @ sK4)))),
% 3.74/1.03 inference(and_proxy_clausification,[],[f130])).
% 3.74/1.03 thf(f133,plain,(
% 3.74/1.03 ($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))))))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f106])).
% 3.74/1.03 thf(f134,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))))) @ X1)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f133])).
% 3.74/1.03 thf(f135,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0)))))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f134])).
% 3.74/1.03 thf(f136,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1))))))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f135])).
% 3.74/1.03 thf(f137,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1))))))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f136])).
% 3.74/1.03 thf(f138,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a @ Y1))))))) @ X3)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f137])).
% 3.74/1.03 thf(f139,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (b @ X2)))) | ($true = (((irel @ X1 @ X3) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0))))))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f138])).
% 3.74/1.03 thf(f140,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0)))))))) | ($true = ((b @ X2)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f139])).
% 3.74/1.03 thf(f141,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f140])).
% 3.74/1.03 thf(f142,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f141])).
% 3.74/1.03 thf(f143,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0))) @ X4))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f142])).
% 3.74/1.03 thf(f144,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (a @ Y0))) @ X4))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (b @ Y0))) @ X5)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f143])).
% 3.74/1.03 thf(f145,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($true = (((irel @ X3 @ X4) => (a @ X4)))) | ($true = (((irel @ X3 @ X5) => (b @ X5))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f144])).
% 3.74/1.03 thf(f146,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((b @ X2))) | ($false = ((irel @ X3 @ X4))) | ($true = (((irel @ X3 @ X5) => (b @ X5)))) | ($true = ((a @ X4)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f145])).
% 3.74/1.03 thf(f147,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ X3 @ X5))) | ($false = ((irel @ X3 @ X4))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((b @ X2))) | ($true = ((a @ X4))) | ($true = ((b @ X5)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f146])).
% 3.74/1.03 thf(f148,plain,(
% 3.74/1.03 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (b1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (a1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))))))))))))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f105])).
% 3.74/1.03 thf(f149,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (b1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (a1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))))))))) @ X1)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f148])).
% 3.74/1.03 thf(f150,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))))))))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f149])).
% 3.74/1.03 thf(f151,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0)))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f150])).
% 3.74/1.03 thf(f152,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1))))))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0)))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f151])).
% 3.74/1.03 thf(f153,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1))))))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0))))))) )),
% 3.74/1.03 inference(not_proxy_clausification,[],[f152])).
% 3.74/1.03 thf(f154,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (b1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (a1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1))))))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (b @ Y0))) @ (sK5 @ X1))))) )),
% 3.74/1.03 inference(sigma_proxy_clausification,[],[f153])).
% 3.74/1.03 thf(f155,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))))) | ($false = (((irel @ X1 @ (sK5 @ X1)) => (b @ (sK5 @ X1)))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f154])).
% 3.74/1.03 thf(f156,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK5 @ X1)) => (b @ (sK5 @ X1))))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f155])).
% 3.74/1.03 thf(f157,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f156])).
% 3.74/1.03 thf(f158,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f156])).
% 3.74/1.03 thf(f159,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f158])).
% 3.74/1.03 thf(f160,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f159])).
% 3.74/1.03 thf(f161,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0))) @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))) @ X4)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f160])).
% 3.74/1.03 thf(f162,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = (((irel @ X2 @ X3) => (b1 @ X3)))) | ($true = (((irel @ X2 @ X4) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))))))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f161])).
% 3.74/1.03 thf(f163,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($true = (((irel @ X2 @ X4) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))))) | ($true = ((b1 @ X3)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f162])).
% 3.74/1.03 thf(f164,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f163])).
% 3.74/1.03 thf(f165,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f164])).
% 3.74/1.03 thf(f166,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f165])).
% 3.74/1.03 thf(f167,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))) @ X5))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))) @ X6)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f166])).
% 3.74/1.03 thf(f168,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((irel @ X4 @ X5) => (a1 @ X5)))) | ($true = (((irel @ X4 @ X6) => (b1 @ X6))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f167])).
% 3.74/1.03 thf(f169,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($false = ((irel @ X4 @ X5))) | ($true = (((irel @ X4 @ X6) => (b1 @ X6)))) | ($true = ((a1 @ X5)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f168])).
% 3.74/1.03 thf(f170,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ X4 @ X6))) | ($false = ((irel @ X4 @ X5))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X2 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((b1 @ X3))) | ($true = ((a1 @ X5))) | ($true = ((b1 @ X6)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f169])).
% 3.74/1.03 thf(f171,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f157])).
% 3.74/1.03 thf(f172,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f171])).
% 3.74/1.03 thf(f173,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (b1 @ Y0))) @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (b1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (a1 @ Y1))))))) @ X4)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f172])).
% 3.74/1.03 thf(f174,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($true = (((irel @ X2 @ X3) => (b1 @ X3)))) | ($true = (((irel @ X2 @ X4) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))))))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f173])).
% 3.74/1.03 thf(f175,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($true = (((irel @ X2 @ X4) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))))) | ($true = ((b1 @ X3)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f174])).
% 3.74/1.03 thf(f176,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f175])).
% 3.74/1.03 thf(f177,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))))))) )),
% 3.74/1.03 inference(or_proxy_clausification,[],[f176])).
% 3.74/1.03 thf(f178,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))))))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f177])).
% 3.74/1.03 thf(f179,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (a1 @ Y0))) @ X5))) | ($true = (((^[Y0 : $i]: ((irel @ X4 @ Y0) => (b1 @ Y0))) @ X6)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f178])).
% 3.74/1.03 thf(f180,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($true = (((irel @ X4 @ X5) => (a1 @ X5)))) | ($true = (((irel @ X4 @ X6) => (b1 @ X6))))) )),
% 3.74/1.03 inference(beta-eta_normalization,[],[f179])).
% 3.74/1.03 thf(f181,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((b @ (sK5 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X4))) | ($true = ((b1 @ X3))) | ($false = ((irel @ X4 @ X5))) | ($true = (((irel @ X4 @ X6) => (b1 @ X6)))) | ($true = ((a1 @ X5)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f180])).
% 3.74/1.03 thf(f182,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($false = ((irel @ X4 @ X6))) | ($false = ((irel @ X4 @ X5))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X2 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((b1 @ X3))) | ($false = ((b @ (sK5 @ X1)))) | ($true = ((a1 @ X5))) | ($true = ((b1 @ X6)))) )),
% 3.74/1.03 inference(imp_proxy_clausification,[],[f181])).
% 3.74/1.03 thf(f183,plain,(
% 3.74/1.03 ($true = ((!! @ $i @ a2)))),
% 3.74/1.03 inference(beta-eta_normalization,[],[f104])).
% 3.74/1.03 thf(f184,plain,(
% 3.74/1.03 ( ! [X1 : $i] : (($true = ((a2 @ X1)))) )),
% 3.74/1.03 inference(pi_proxy_clausification,[],[f183])).
% 3.74/1.03 thf(f186,definition,(
% 3.74/1.03 spl6_1 <=> ($false = ((b @ sK3)))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 3.74/1.03 thf(f188,plain,(
% 3.74/1.03 ($false = ((b @ sK3))) | ~spl6_1),
% 3.74/1.03 inference(avatar_component_clause,[],[f186])).
% 3.74/1.03 thf(f190,definition,(
% 3.74/1.03 spl6_2 <=> ($false = ((a1 @ sK3)))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 3.74/1.03 thf(f192,plain,(
% 3.74/1.03 ($false = ((a1 @ sK3))) | ~spl6_2),
% 3.74/1.03 inference(avatar_component_clause,[],[f190])).
% 3.74/1.03 thf(f193,plain,(
% 3.74/1.03 spl6_1 | spl6_2),
% 3.74/1.03 inference(avatar_split_clause,[],[f127,f190,f186])).
% 3.74/1.03 thf(f195,definition,(
% 3.74/1.03 spl6_3 <=> ($false = ((b1 @ sK4)))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 3.74/1.03 thf(f197,plain,(
% 3.74/1.03 ($false = ((b1 @ sK4))) | ~spl6_3),
% 3.74/1.03 inference(avatar_component_clause,[],[f195])).
% 3.74/1.03 thf(f199,definition,(
% 3.74/1.03 spl6_4 <=> ($false = ((a2 @ sK4)))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition])).
% 3.74/1.03 thf(f201,plain,(
% 3.74/1.03 ($false = ((a2 @ sK4))) | ~spl6_4),
% 3.74/1.03 inference(avatar_component_clause,[],[f199])).
% 3.74/1.03 thf(f202,plain,(
% 3.74/1.03 spl6_3 | spl6_4),
% 3.74/1.03 inference(avatar_split_clause,[],[f132,f199,f195])).
% 3.74/1.03 thf(f216,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f69,f116])).
% 3.74/1.03 thf(f219,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK4))) | ($true != ((irel @ X0 @ sK2)))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f69,f131])).
% 3.74/1.03 thf(f221,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) )),
% 3.74/1.03 inference(constrained_superposition,[],[f69,f94])).
% 3.74/1.03 thf(f222,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X2 @ X0))) | ($true = ((irel @ X2 @ X1))) | (((irel @ X0 @ X1)) = $false)) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f221])).
% 3.74/1.03 thf(f223,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK4))) | ($true != ((irel @ X0 @ sK2)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f219])).
% 3.74/1.03 thf(f226,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f216])).
% 3.74/1.03 thf(f404,definition,(
% 3.74/1.03 spl6_16 <=> ! [X0 : $i,X3 : $i,X2 : $i,X1 : $i] : (($true != ((irel @ X0 @ sK0))) | ($true = ((b @ X1))) | ($true = ((b @ X3))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition])).
% 3.74/1.03 thf(f405,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X0 @ sK0))) | ($true = ((b @ X1))) | ($true = ((b @ X3))) | ($false = ((irel @ X2 @ X3))) | ($false = ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) ) | ~spl6_16),
% 3.74/1.03 inference(avatar_component_clause,[],[f404])).
% 3.74/1.03 thf(f421,definition,(
% 3.74/1.03 spl6_20 <=> ! [X2 : $i,X1 : $i] : (($false = ((irel @ X1 @ sK0))) | ($true = ((b @ X2))) | (((irel @ X1 @ X2)) = $false))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_20])],[avatar_definition])).
% 3.74/1.03 thf(f422,plain,(
% 3.74/1.03 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ X1 @ sK0))) | (((irel @ X1 @ X2)) = $false) | ($true = ((b @ X2)))) ) | ~spl6_20),
% 3.74/1.03 inference(avatar_component_clause,[],[f421])).
% 3.74/1.03 thf(f518,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X2 @ X0))) | ($false = ((irel @ X2 @ X3))) | ($true = ((b @ X3))) | ($true = ((a @ sK1))) | ($true = ((b @ X1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f147,f226])).
% 3.74/1.03 thf(f523,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X2 @ X0))) | ($false = ((irel @ X2 @ X3))) | ($true = ((b @ X3))) | ($true = ((a @ sK1))) | ($true = ((b @ X1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f518])).
% 3.74/1.03 thf(f530,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X2 @ X0))) | ($false = ((irel @ X2 @ X3))) | ($true = ((b @ X3))) | ($true = ((b @ X1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(forward_demodulation,[],[f523,f115])).
% 3.74/1.03 thf(f531,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X2 @ X0))) | ($false = ((irel @ X2 @ X3))) | ($true = ((b @ X3))) | ($true = ((b @ X1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f530])).
% 3.74/1.03 thf(f534,plain,(
% 3.74/1.03 spl6_16),
% 3.74/1.03 inference(avatar_split_clause,[],[f531,f404])).
% 3.74/1.03 thf(f589,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((b @ X1))) | ($true = ((b @ X2))) | ($false = ((irel @ X3 @ X2))) | ($false = ((irel @ X3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0)))) ) | ~spl6_16),
% 3.74/1.03 inference(constrained_superposition,[],[f405,f94])).
% 3.74/1.03 thf(f590,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ X3 @ X2))) | ($false = ((irel @ X3 @ X0))) | ($false = ((irel @ X0 @ sK0))) | (((irel @ X0 @ X1)) = $false) | ($true = ((b @ X2))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f589])).
% 3.74/1.03 thf(f648,plain,(
% 3.74/1.03 ( ! [X0 : $i,X1 : $i] : (($false != $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X0)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((b @ X1))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(equality_factoring,[],[f590])).
% 3.74/1.03 thf(f653,plain,(
% 3.74/1.03 ( ! [X0 : $i,X1 : $i] : (($false != $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X0)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(duplicate_literal_removal,[],[f648])).
% 3.74/1.03 thf(f654,plain,(
% 3.74/1.03 ( ! [X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X0)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f653])).
% 3.74/1.03 thf(f707,plain,(
% 3.74/1.03 ( ! [X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(forward_demodulation,[],[f654,f68])).
% 3.74/1.03 thf(f708,plain,(
% 3.74/1.03 ( ! [X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((b @ X1)))) ) | ~spl6_16),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f707])).
% 3.74/1.03 thf(f722,plain,(
% 3.74/1.03 spl6_20 | ~spl6_16),
% 3.74/1.03 inference(avatar_split_clause,[],[f708,f404,f421])).
% 3.74/1.03 thf(f1162,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK2 @ X0)))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f222,f120])).
% 3.74/1.03 thf(f1172,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((irel @ sK0 @ X0)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f1162])).
% 3.74/1.03 thf(f1189,plain,(
% 3.74/1.03 ($true = $false) | ($true = ((irel @ sK0 @ sK3)))),
% 3.74/1.03 inference(constrained_superposition,[],[f126,f1172])).
% 3.74/1.03 thf(f1192,plain,(
% 3.74/1.03 ($true = ((irel @ sK0 @ sK3)))),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f1189])).
% 3.74/1.03 thf(f1458,plain,(
% 3.74/1.03 ($true = $false) | ($false = ((irel @ sK0 @ sK0))) | ($true = ((b @ sK3))) | ~spl6_20),
% 3.74/1.03 inference(constrained_superposition,[],[f1192,f422])).
% 3.74/1.03 thf(f1515,plain,(
% 3.74/1.03 ($false = ((irel @ sK0 @ sK0))) | ($true = ((b @ sK3))) | ~spl6_20),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f1458])).
% 3.74/1.03 thf(f3185,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK2 @ X0))) | ($false = ((irel @ X3 @ sK2))) | ($true = ((b1 @ sK4))) | ($false = ((b @ (sK5 @ X3)))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1)))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f182,f131])).
% 3.74/1.03 thf(f3370,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK2 @ X0))) | ($false = ((irel @ X3 @ sK2))) | ($true = ((b1 @ sK4))) | ($false = ((b @ (sK5 @ X3)))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1)))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3185])).
% 3.74/1.03 thf(f3457,definition,(
% 3.74/1.03 spl6_40 <=> ! [X4 : $i] : (($false = ((irel @ sK2 @ X4))) | ($true = ((b1 @ X4))))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_40])],[avatar_definition])).
% 3.74/1.03 thf(f3458,plain,(
% 3.74/1.03 ( ! [X4 : $i] : (($false = ((irel @ sK2 @ X4))) | ($true = ((b1 @ X4)))) ) | ~spl6_40),
% 3.74/1.03 inference(avatar_component_clause,[],[f3457])).
% 3.74/1.03 thf(f3460,definition,(
% 3.74/1.03 spl6_41 <=> ! [X2 : $i,X1 : $i,X3 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((b1 @ X2))) | ($true = ((a1 @ X3))) | ($false = ((irel @ sK2 @ X1))) | ($false = ((irel @ X1 @ X3))))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_41])],[avatar_definition])).
% 3.74/1.03 thf(f3461,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK2 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((a1 @ X3))) | ($true = ((b1 @ X2)))) ) | ~spl6_41),
% 3.74/1.03 inference(avatar_component_clause,[],[f3460])).
% 3.74/1.03 thf(f3477,definition,(
% 3.74/1.03 spl6_45 <=> ! [X3 : $i] : (($false = ((irel @ X3 @ sK2))) | ($false = ((b @ (sK5 @ X3)))))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_45])],[avatar_definition])).
% 3.74/1.03 thf(f3478,plain,(
% 3.74/1.03 ( ! [X3 : $i] : (($false = ((irel @ X3 @ sK2))) | ($false = ((b @ (sK5 @ X3))))) ) | ~spl6_45),
% 3.74/1.03 inference(avatar_component_clause,[],[f3477])).
% 3.74/1.03 thf(f3605,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK2 @ X0))) | ($false = ((irel @ X3 @ sK2))) | ($false = ((b @ (sK5 @ X3)))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1)))) ) | ~spl6_3),
% 3.74/1.03 inference(forward_demodulation,[],[f3370,f197])).
% 3.74/1.03 thf(f3606,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK2 @ X0))) | ($false = ((irel @ X3 @ sK2))) | ($false = ((b @ (sK5 @ X3)))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1)))) ) | ~spl6_3),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3605])).
% 3.74/1.03 thf(f3665,plain,(
% 3.74/1.03 spl6_45 | spl6_41 | ~spl6_3),
% 3.74/1.03 inference(avatar_split_clause,[],[f3606,f195,f3460,f3477])).
% 3.74/1.03 thf(f3671,plain,(
% 3.74/1.03 ($true = $false) | ~spl6_4),
% 3.74/1.03 inference(forward_demodulation,[],[f201,f184])).
% 3.74/1.03 thf(f3672,plain,(
% 3.74/1.03 $false | ~spl6_4),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3671])).
% 3.74/1.03 thf(f3673,plain,(
% 3.74/1.03 ~spl6_4),
% 3.74/1.03 inference(avatar_contradiction_clause,[],[f3672])).
% 3.74/1.03 thf(f3752,plain,(
% 3.74/1.03 ($true = $false) | ($true = ((b1 @ sK4))) | ($true != ((irel @ sK2 @ sK2))) | ~spl6_40),
% 3.74/1.03 inference(constrained_superposition,[],[f3458,f223])).
% 3.74/1.03 thf(f3779,plain,(
% 3.74/1.03 ($true = ((b1 @ sK4))) | ($true != ((irel @ sK2 @ sK2))) | ~spl6_40),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3752])).
% 3.74/1.03 thf(f3794,plain,(
% 3.74/1.03 ($true = ((b1 @ sK4))) | ~spl6_40),
% 3.74/1.03 inference(forward_subsumption_resolution,[],[f3779,f68])).
% 3.74/1.03 thf(f3800,plain,(
% 3.74/1.03 ($true = $false) | (~spl6_3 | ~spl6_40)),
% 3.74/1.03 inference(forward_demodulation,[],[f3794,f197])).
% 3.74/1.03 thf(f3801,plain,(
% 3.74/1.03 $false | (~spl6_3 | ~spl6_40)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3800])).
% 3.74/1.03 thf(f3802,plain,(
% 3.74/1.03 ~spl6_3 | ~spl6_40),
% 3.74/1.03 inference(avatar_contradiction_clause,[],[f3801])).
% 3.74/1.03 thf(f3842,plain,(
% 3.74/1.03 ($true = $false) | ($true = ((b @ sK3))) | ~spl6_20),
% 3.74/1.03 inference(forward_demodulation,[],[f1515,f68])).
% 3.74/1.03 thf(f3843,plain,(
% 3.74/1.03 ($true = ((b @ sK3))) | ~spl6_20),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3842])).
% 3.74/1.03 thf(f3883,plain,(
% 3.74/1.03 ($true = $false) | (~spl6_1 | ~spl6_20)),
% 3.74/1.03 inference(forward_demodulation,[],[f3843,f188])).
% 3.74/1.03 thf(f3884,plain,(
% 3.74/1.03 $false | (~spl6_1 | ~spl6_20)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f3883])).
% 3.74/1.03 thf(f3885,plain,(
% 3.74/1.03 ~spl6_1 | ~spl6_20),
% 3.74/1.03 inference(avatar_contradiction_clause,[],[f3884])).
% 3.74/1.03 thf(f4086,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ sK2))) | ($false = ((irel @ sK2 @ X0))) | ($true = ((a1 @ sK3))) | ($true = ((b1 @ X0)))) ) | ~spl6_41),
% 3.74/1.03 inference(constrained_superposition,[],[f126,f3461])).
% 3.74/1.03 thf(f4125,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ sK2))) | ($false = ((irel @ sK2 @ X0))) | ($true = ((a1 @ sK3))) | ($true = ((b1 @ X0)))) ) | ~spl6_41),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f4086])).
% 3.74/1.03 thf(f4163,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ X0))) | ($true = ((a1 @ sK3))) | ($true = ((b1 @ X0)))) ) | ~spl6_41),
% 3.74/1.03 inference(forward_demodulation,[],[f4125,f68])).
% 3.74/1.03 thf(f4164,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((a1 @ sK3))) | ($true = ((b1 @ X0)))) ) | ~spl6_41),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f4163])).
% 3.74/1.03 thf(f4187,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ X0))) | ($true = ((b1 @ X0)))) ) | (~spl6_2 | ~spl6_41)),
% 3.74/1.03 inference(forward_demodulation,[],[f4164,f192])).
% 3.74/1.03 thf(f4188,plain,(
% 3.74/1.03 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((b1 @ X0)))) ) | (~spl6_2 | ~spl6_41)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f4187])).
% 3.74/1.03 thf(f4194,plain,(
% 3.74/1.03 spl6_40 | ~spl6_2 | ~spl6_41),
% 3.74/1.03 inference(avatar_split_clause,[],[f4188,f3460,f190,f3457])).
% 3.74/1.03 thf(f4420,plain,(
% 3.74/1.03 ($true = $false) | ($false = ((b @ (sK5 @ sK2)))) | ~spl6_45),
% 3.74/1.03 inference(constrained_superposition,[],[f68,f3478])).
% 3.74/1.03 thf(f4428,plain,(
% 3.74/1.03 ($false = ((b @ (sK5 @ sK2)))) | ~spl6_45),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f4420])).
% 3.74/1.03 thf(f4486,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ X3 @ X0))) | ($false = ((irel @ X3 @ X4))) | ($false = ((irel @ sK2 @ X3))) | ($true = ((b1 @ X4))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1))) | ($true = ((irel @ sK0 @ (sK5 @ sK2))))) )),
% 3.74/1.03 inference(constrained_superposition,[],[f170,f1172])).
% 3.74/1.03 thf(f4790,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ X3 @ X0))) | ($false = ((irel @ X3 @ X4))) | ($false = ((irel @ sK2 @ X3))) | ($true = ((b1 @ X4))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1))) | ($true = ((irel @ sK0 @ (sK5 @ sK2))))) )),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f4486])).
% 3.74/1.03 thf(f4899,definition,(
% 3.74/1.03 spl6_80 <=> ! [X4 : $i,X0 : $i,X3 : $i,X2 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | ($true = ((b1 @ X1))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X4))) | ($false = ((irel @ sK2 @ X3))) | ($false = ((irel @ X3 @ X4))) | ($false = ((irel @ X3 @ X0))) | (((irel @ X0 @ X2)) = $false))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_80])],[avatar_definition])).
% 3.74/1.03 thf(f4900,plain,(
% 3.74/1.03 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ sK2 @ X3))) | ($false = ((irel @ X3 @ X4))) | ($false = ((irel @ X3 @ X0))) | (((irel @ X0 @ X2)) = $false) | (((irel @ X0 @ X1)) = $false) | ($true = ((b1 @ X4))) | ($true = ((a1 @ X2))) | ($true = ((b1 @ X1)))) ) | ~spl6_80),
% 3.74/1.03 inference(avatar_component_clause,[],[f4899])).
% 3.74/1.03 thf(f4902,definition,(
% 3.74/1.03 spl6_81 <=> ($true = ((irel @ sK0 @ (sK5 @ sK2))))),
% 3.74/1.03 introduced(definition,[new_symbols(definition,[spl6_81])],[avatar_definition])).
% 3.74/1.03 thf(f4904,plain,(
% 3.74/1.03 ($true = ((irel @ sK0 @ (sK5 @ sK2)))) | ~spl6_81),
% 3.74/1.03 inference(avatar_component_clause,[],[f4902])).
% 3.74/1.03 thf(f4938,plain,(
% 3.74/1.03 spl6_81 | spl6_80),
% 3.74/1.03 inference(avatar_split_clause,[],[f4790,f4899,f4902])).
% 3.74/1.03 thf(f5086,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ sK2))) | ($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((b1 @ sK4))) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | ~spl6_80),
% 3.74/1.03 inference(constrained_superposition,[],[f131,f4900])).
% 3.74/1.03 thf(f5208,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK2 @ sK2))) | ($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((b1 @ sK4))) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | ~spl6_80),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5086])).
% 3.74/1.03 thf(f5302,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((b1 @ sK4))) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | ~spl6_80),
% 3.74/1.03 inference(forward_demodulation,[],[f5208,f68])).
% 3.74/1.03 thf(f5303,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((b1 @ sK4))) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | ~spl6_80),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5302])).
% 3.74/1.03 thf(f5337,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | (~spl6_3 | ~spl6_80)),
% 3.74/1.03 inference(forward_demodulation,[],[f5303,f197])).
% 3.74/1.03 thf(f5338,plain,(
% 3.74/1.03 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK2 @ X0))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($true = ((a1 @ X1))) | ($true = ((b1 @ X2)))) ) | (~spl6_3 | ~spl6_80)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5337])).
% 3.74/1.03 thf(f5343,plain,(
% 3.74/1.03 spl6_41 | ~spl6_3 | ~spl6_80),
% 3.74/1.03 inference(avatar_split_clause,[],[f5338,f4899,f195,f3460])).
% 3.74/1.03 thf(f5372,plain,(
% 3.74/1.03 ($true = $false) | ($false = ((irel @ sK0 @ sK0))) | ($true = ((b @ (sK5 @ sK2)))) | (~spl6_20 | ~spl6_81)),
% 3.74/1.03 inference(constrained_superposition,[],[f4904,f422])).
% 3.74/1.03 thf(f5471,plain,(
% 3.74/1.03 ($false = ((irel @ sK0 @ sK0))) | ($true = ((b @ (sK5 @ sK2)))) | (~spl6_20 | ~spl6_81)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5372])).
% 3.74/1.03 thf(f5515,plain,(
% 3.74/1.03 ($true = $false) | ($true = ((b @ (sK5 @ sK2)))) | (~spl6_20 | ~spl6_81)),
% 3.74/1.03 inference(forward_demodulation,[],[f5471,f68])).
% 3.74/1.03 thf(f5516,plain,(
% 3.74/1.03 ($true = ((b @ (sK5 @ sK2)))) | (~spl6_20 | ~spl6_81)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5515])).
% 3.74/1.03 thf(f5524,plain,(
% 3.74/1.03 ($true = $false) | (~spl6_20 | ~spl6_45 | ~spl6_81)),
% 3.74/1.03 inference(forward_demodulation,[],[f5516,f4428])).
% 3.74/1.03 thf(f5525,plain,(
% 3.74/1.03 $false | (~spl6_20 | ~spl6_45 | ~spl6_81)),
% 3.74/1.03 inference(trivial_inequality_removal,[],[f5524])).
% 3.74/1.03 thf(f5526,plain,(
% 3.74/1.03 ~spl6_20 | ~spl6_45 | ~spl6_81),
% 3.74/1.03 inference(avatar_contradiction_clause,[],[f5525])).
% 3.74/1.03 cnf(s1, plain, spl6_1 | spl6_2, inference(sat_conversion,[],[f193])).
% 3.74/1.03 cnf(s2, plain, spl6_3 | spl6_4, inference(sat_conversion,[],[f202])).
% 3.74/1.03 cnf(s41, plain, spl6_16, inference(sat_conversion,[],[f534])).
% 3.74/1.03 cnf(s47, plain, ~spl6_16 | spl6_20, inference(sat_conversion,[],[f722])).
% 3.74/1.03 cnf(s142, plain, ~spl6_3 | spl6_41 | spl6_45, inference(sat_conversion,[],[f3665])).
% 3.74/1.03 cnf(s153, plain, ~spl6_4, inference(sat_conversion,[],[f3673])).
% 3.74/1.03 cnf(s179, plain, ~spl6_3 | ~spl6_40, inference(sat_conversion,[],[f3802])).
% 3.74/1.03 cnf(s190, plain, ~spl6_1 | ~spl6_20, inference(sat_conversion,[],[f3885])).
% 3.74/1.03 cnf(s223, plain, ~spl6_2 | spl6_40 | ~spl6_41, inference(sat_conversion,[],[f4194])).
% 3.74/1.03 cnf(s241, plain, spl6_80 | spl6_81, inference(sat_conversion,[],[f4938])).
% 3.74/1.03 cnf(s267, plain, ~spl6_3 | spl6_41 | ~spl6_80, inference(sat_conversion,[],[f5343])).
% 3.74/1.03 cnf(s275, plain, ~spl6_20 | ~spl6_45 | ~spl6_81, inference(sat_conversion,[],[f5526])).
% 3.74/1.03 cnf(s277, plain, spl6_20, inference(rat,[],[s47,s41])).
% 3.74/1.03 cnf(s279, plain, ~spl6_1, inference(rat,[],[s190,s277])).
% 3.74/1.03 cnf(s283, plain, spl6_3, inference(rat,[],[s2,s153])).
% 3.74/1.03 cnf(s285, plain, ~spl6_40, inference(rat,[],[s179,s283])).
% 3.74/1.03 cnf(s290, plain, spl6_2, inference(rat,[],[s1,s279])).
% 3.74/1.03 cnf(s291, plain, ~spl6_41, inference(rat,[],[s223,s285,s290])).
% 3.74/1.03 cnf(s295, plain, ~spl6_80, inference(rat,[],[s267,s283,s291])).
% 3.74/1.03 cnf(s296, plain, spl6_45, inference(rat,[],[s142,s283,s291])).
% 3.74/1.03 cnf(s300, plain, spl6_81, inference(rat,[],[s241,s295])).
% 3.74/1.03 cnf(s301, plain, $false, inference(rat,[],[s275,s277,s300,s296])).
% 3.74/1.03 thf(f5527,plain,(
% 3.74/1.03 $false),
% 3.74/1.03 inference(avatar_sat_refutation,[],[s301])).
% 3.74/1.03 % SZS output end Proof for theBenchmark
% 3.74/1.03 % (1511700)------------------------------
% 3.74/1.03 % (1511700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.03 % (1511700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.03 % (1511700)CaDiCaL version: 2.1.3
% 3.74/1.03 % (1511700)Termination reason: Refutation
% 3.74/1.03 % (1511700)Time elapsed: 0.185 s
% 3.74/1.03 % (1511700)Peak memory usage: 14 MB
% 3.74/1.03 % (1511700)Instructions burned: 691 (million)
% 3.74/1.03 % (1511647)Success in time 0.796 s
% 3.74/1.03 % Vampire exiting
%------------------------------------------------------------------------------