%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL872^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:15:12 AM UTC 2026
% Result : Theorem 68.26s 10.00s
% Output : Refutation 68.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL872^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n026.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 10:21:12 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.42/1.19 % (403264)Will run a generic schedule for satisfiability detection.
% 6.42/1.19 % (403270)% WARNING: option uhcvi not known.
% 6.42/1.19 % (403272)dis+10_1_sil=32000:sp=arity:random_seed=915388042:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.42/1.19 % (403275)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1069847999:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.42/1.19 % (403270)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=874525370:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.42/1.19 % (403270)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.42/1.19 % (403270)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.42/1.19 % (403273)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1817985636:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.42/1.19 % (403273)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.42/1.19 % (403271)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2098157055:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.42/1.19 % (403269)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1998998840_2999 on theBenchmark for (2999ds/0Mi)
% 6.42/1.19 % (403274)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1865600117:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.42/1.19 % Exception at run slice level
% 6.42/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.42/1.19 % (403283)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=401929044:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.42/1.19 % Exception at run slice level
% 6.42/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.42/1.19 % (403275)Instruction limit reached!
% 6.42/1.19 % (403275)------------------------------
% 6.42/1.19 % (403275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.42/1.19 % (403275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.19 % (403275)CaDiCaL version: 2.1.3
% 6.42/1.19 % (403275)Termination reason: Instruction limit
% 6.42/1.19 % (403275)Termination phase: Saturation
% 6.42/1.19 % (403275)Time elapsed: 0.049 s
% 6.42/1.19 % (403275)Peak memory usage: 13 MB
% 6.42/1.19 % (403275)Instructions burned: 160 (million)
% 6.42/1.19 % (403272)Instruction limit reached!
% 6.42/1.19 % (403272)------------------------------
% 6.42/1.19 % (403272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.42/1.19 % (403272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.19 % (403272)CaDiCaL version: 2.1.3
% 6.42/1.19 % (403272)Termination reason: Instruction limit
% 6.42/1.19 % (403272)Termination phase: Saturation
% 6.42/1.19 % (403272)Time elapsed: 0.068 s
% 6.42/1.19 % (403272)Peak memory usage: 12 MB
% 6.42/1.19 % (403272)Instructions burned: 104 (million)
% 6.42/1.19 % (403286)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=148735059:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.42/1.19 % (403285)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3119412835:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.42/1.19 % (403286)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.42/1.19 % (403286)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.42/1.19 % (403287)ott-21_1_sil=16000:fs=off:random_seed=1759845120:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.42/1.19 % (403274)Instruction limit reached!
% 6.42/1.19 % (403274)------------------------------
% 6.42/1.19 % (403274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.42/1.19 % (403274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.19 % (403274)CaDiCaL version: 2.1.3
% 6.42/1.19 % (403274)Termination reason: Instruction limit
% 6.42/1.19 % (403274)Termination phase: Saturation
% 6.42/1.19 % (403274)Time elapsed: 0.087 s
% 6.42/1.19 % (403274)Peak memory usage: 13 MB
% 6.42/1.19 % (403274)Instructions burned: 132 (million)
% 6.42/1.19 % (403273)Instruction limit reached!
% 6.42/1.19 % (403273)------------------------------
% 17.98/2.96 % (403273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/2.96 % (403273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/2.96 % (403273)CaDiCaL version: 2.1.3
% 17.98/2.96 % (403273)Termination reason: Instruction limit
% 17.98/2.96 % (403273)Termination phase: Saturation
% 17.98/2.96 % (403273)Time elapsed: 0.099 s
% 17.98/2.96 % (403273)Peak memory usage: 13 MB
% 17.98/2.96 % (403273)Instructions burned: 116 (million)
% 17.98/2.96 % (403287)Instruction limit reached!
% 17.98/2.96 % (403287)------------------------------
% 17.98/2.96 % (403287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/2.96 % (403287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/2.96 % (403287)CaDiCaL version: 2.1.3
% 17.98/2.96 % (403287)Termination reason: Instruction limit
% 17.98/2.96 % (403287)Termination phase: Saturation
% 17.98/2.96 % (403287)Time elapsed: 0.042 s
% 17.98/2.96 % (403287)Peak memory usage: 14 MB
% 17.98/2.96 % (403287)Instructions burned: 184 (million)
% 17.98/2.96 % (403293)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=157588154:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 17.98/2.96 % (403285)Instruction limit reached!
% 17.98/2.96 % (403285)------------------------------
% 17.98/2.96 % (403285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/2.96 % (403285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/2.96 % (403285)CaDiCaL version: 2.1.3
% 17.98/2.96 % (403285)Termination reason: Instruction limit
% 17.98/2.96 % (403285)Termination phase: Saturation
% 17.98/2.96 % (403285)Time elapsed: 0.067 s
% 17.98/2.96 % (403285)Peak memory usage: 13 MB
% 17.98/2.96 % (403285)Instructions burned: 136 (million)
% 17.98/2.96 % (403292)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=587746130:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.98/2.96 % Exception at run slice level
% 17.98/2.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.98/2.96 % (403291)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4077380318:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 17.98/2.96 % (403295)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3989898167:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 17.98/2.96 % Exception at run slice level
% 17.98/2.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.98/2.96 % (403297)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=3252553886:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 17.98/2.96 % (403297)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.98/2.96 % (403301)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2481388335:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 17.98/2.96 % (403301)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.98/2.96 % (403291)Instruction limit reached!
% 17.98/2.96 % (403291)------------------------------
% 17.98/2.96 % (403291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/2.96 % (403291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/2.96 % (403291)CaDiCaL version: 2.1.3
% 17.98/2.96 % (403291)Termination reason: Instruction limit
% 17.98/2.96 % (403291)Termination phase: Saturation
% 17.98/2.96 % (403291)Time elapsed: 0.235 s
% 17.98/2.96 % (403291)Peak memory usage: 14 MB
% 17.98/2.96 % (403291)Instructions burned: 478 (million)
% 17.98/2.96 % (403304)fmb+10_1_sil=64000:random_seed=613347479:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 17.98/2.96 % (403304)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.98/2.96 % Exception at run slice level
% 17.98/2.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.98/2.96 % (403306)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1114591140:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 17.98/2.96 % Exception at run slice level
% 17.98/2.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.98/2.96 % (403308)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=21035957:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 42.96/6.34 % Exception at run slice level
% 42.96/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 42.96/6.34 % (403293)Instruction limit reached!
% 42.96/6.34 % (403293)------------------------------
% 42.96/6.34 % (403293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.96/6.34 % (403293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.96/6.34 % (403293)CaDiCaL version: 2.1.3
% 42.96/6.34 % (403293)Termination reason: Instruction limit
% 42.96/6.34 % (403293)Termination phase: Saturation
% 42.96/6.34 % (403293)Time elapsed: 0.339 s
% 42.96/6.34 % (403293)Peak memory usage: 16 MB
% 42.96/6.34 % (403293)Instructions burned: 1179 (million)
% 42.96/6.34 % (403310)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2784429102:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 42.96/6.34 % (403310)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 42.96/6.34 % (403297)Instruction limit reached!
% 42.96/6.34 % (403297)------------------------------
% 42.96/6.34 % (403297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.96/6.34 % (403297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.96/6.34 % (403297)CaDiCaL version: 2.1.3
% 42.96/6.34 % (403297)Termination reason: Instruction limit
% 42.96/6.34 % (403297)Termination phase: Saturation
% 42.96/6.34 % (403297)Time elapsed: 0.319 s
% 42.96/6.34 % (403297)Peak memory usage: 15 MB
% 42.96/6.34 % (403297)Instructions burned: 694 (million)
% 42.96/6.34 % (403311)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2804783082:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 42.96/6.34 % (403311)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 42.96/6.34 % (403311)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 42.96/6.34 % (403313)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=309705781:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 42.96/6.34 % Exception at run slice level
% 42.96/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 42.96/6.35 % (403316)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1452479548:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 42.96/6.35 % Exception at run slice level
% 42.96/6.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 42.96/6.35 % (403318)ott-2_1_sil=16000:newcnf=on:random_seed=2122003410:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 42.96/6.35 % (403318)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 42.96/6.35 % (403286)Instruction limit reached!
% 42.96/6.35 % (403286)------------------------------
% 42.96/6.35 % (403286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.96/6.35 % (403286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.96/6.35 % (403286)CaDiCaL version: 2.1.3
% 42.96/6.35 % (403286)Termination reason: Instruction limit
% 42.96/6.35 % (403286)Termination phase: Saturation
% 42.96/6.35 % (403286)Time elapsed: 0.539 s
% 42.96/6.35 % (403286)Peak memory usage: 14 MB
% 42.96/6.35 % (403286)Instructions burned: 685 (million)
% 42.96/6.35 % (403320)ott+10_1_sil=32000:tgt=ground:random_seed=3303428469:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 42.96/6.35 % (403318)Instruction limit reached!
% 42.96/6.35 % (403318)------------------------------
% 42.96/6.35 % (403318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.96/6.35 % (403318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.96/6.35 % (403318)CaDiCaL version: 2.1.3
% 42.96/6.35 % (403318)Termination reason: Instruction limit
% 42.96/6.35 % (403318)Termination phase: Saturation
% 42.96/6.35 % (403318)Time elapsed: 0.393 s
% 42.96/6.35 % (403318)Peak memory usage: 16 MB
% 42.96/6.35 % (403318)Instructions burned: 871 (million)
% 42.96/6.35 % (403301)Instruction limit reached!
% 42.96/6.35 % (403301)------------------------------
% 42.96/6.35 % (403301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.96/6.35 % (403301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.96/6.35 % (403301)CaDiCaL version: 2.1.3
% 42.96/6.35 % (403301)Termination reason: Instruction limit
% 68.26/10.00 % (403301)Termination phase: Saturation
% 68.26/10.00 % (403301)Time elapsed: 0.752 s
% 68.26/10.00 % (403301)Peak memory usage: 15 MB
% 68.26/10.00 % (403301)Instructions burned: 879 (million)
% 68.26/10.00 % (403322)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1079481022:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403323)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3634768265:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 68.26/10.00 % (403323)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.26/10.00 % (403325)dis+21_1_sil=32000:sas=cadical:random_seed=2319788303:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 68.26/10.00 % (403311)Instruction limit reached!
% 68.26/10.00 % (403311)------------------------------
% 68.26/10.00 % (403311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403311)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403311)Termination reason: Instruction limit
% 68.26/10.00 % (403311)Termination phase: Saturation
% 68.26/10.00 % (403311)Time elapsed: 1.094 s
% 68.26/10.00 % (403311)Peak memory usage: 17 MB
% 68.26/10.00 % (403311)Instructions burned: 1472 (million)
% 68.26/10.00 % (403328)ott+11_1_sil=16000:gs=on:random_seed=3648693345:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 68.26/10.00 % (403328)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.26/10.00 % (403320)Instruction limit reached!
% 68.26/10.00 % (403320)------------------------------
% 68.26/10.00 % (403320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403320)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403320)Termination reason: Instruction limit
% 68.26/10.00 % (403320)Termination phase: Saturation
% 68.26/10.00 % (403320)Time elapsed: 1.228 s
% 68.26/10.00 % (403320)Peak memory usage: 23 MB
% 68.26/10.00 % (403320)Instructions burned: 5114 (million)
% 68.26/10.00 % (403331)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3624822268:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403333)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3904923518:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 68.26/10.00 % (403323)Instruction limit reached!
% 68.26/10.00 % (403323)------------------------------
% 68.26/10.00 % (403323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403323)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403323)Termination reason: Instruction limit
% 68.26/10.00 % (403323)Termination phase: Saturation
% 68.26/10.00 % (403323)Time elapsed: 1.616 s
% 68.26/10.00 % (403323)Peak memory usage: 18 MB
% 68.26/10.00 % (403323)Instructions burned: 3514 (million)
% 68.26/10.00 % (403336)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2124435733:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 68.26/10.00 % (403325)Instruction limit reached!
% 68.26/10.00 % (403325)------------------------------
% 68.26/10.00 % (403325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403325)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403325)Termination reason: Instruction limit
% 68.26/10.00 % (403325)Termination phase: Saturation
% 68.26/10.00 % (403325)Time elapsed: 1.691 s
% 68.26/10.00 % (403325)Peak memory usage: 19 MB
% 68.26/10.00 % (403325)Instructions burned: 3775 (million)
% 68.26/10.00 % (403338)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1230381028:i=5211_2972 on theBenchmark for (2972ds/5211Mi)
% 68.26/10.00 % (403310)Instruction limit reached!
% 68.26/10.00 % (403310)------------------------------
% 68.26/10.00 % (403310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403310)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403310)Termination reason: Instruction limit
% 68.26/10.00 % (403310)Termination phase: Saturation
% 68.26/10.00 % (403310)Time elapsed: 2.241 s
% 68.26/10.00 % (403310)Peak memory usage: 20 MB
% 68.26/10.00 % (403310)Instructions burned: 5133 (million)
% 68.26/10.00 % (403340)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2840195703:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403342)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1852250785:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403344)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2715470220:i=14071_2971 on theBenchmark for (2971ds/14071Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403346)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=594650533:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi)
% 68.26/10.00 % (403328)Instruction limit reached!
% 68.26/10.00 % (403328)------------------------------
% 68.26/10.00 % (403328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403328)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403328)Termination reason: Instruction limit
% 68.26/10.00 % (403328)Termination phase: Saturation
% 68.26/10.00 % (403328)Time elapsed: 1.231 s
% 68.26/10.00 % (403328)Peak memory usage: 19 MB
% 68.26/10.00 % (403328)Instructions burned: 2251 (million)
% 68.26/10.00 % (403348)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1909355390:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi)
% 68.26/10.00 % (403333)Instruction limit reached!
% 68.26/10.00 % (403333)------------------------------
% 68.26/10.00 % (403333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403333)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403333)Termination reason: Instruction limit
% 68.26/10.00 % (403333)Termination phase: Saturation
% 68.26/10.00 % (403333)Time elapsed: 1.422 s
% 68.26/10.00 % (403333)Peak memory usage: 20 MB
% 68.26/10.00 % (403333)Instructions burned: 4596 (million)
% 68.26/10.00 % (403350)dis+10_16:1_sil=16000:random_seed=2819764159:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi)
% 68.26/10.00 % (403338)Instruction limit reached!
% 68.26/10.00 % (403338)------------------------------
% 68.26/10.00 % (403338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403338)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403338)Termination reason: Instruction limit
% 68.26/10.00 % (403338)Termination phase: Saturation
% 68.26/10.00 % (403338)Time elapsed: 3.005 s
% 68.26/10.00 % (403338)Peak memory usage: 22 MB
% 68.26/10.00 % (403338)Instructions burned: 5211 (million)
% 68.26/10.00 % (403354)ott-3_8_sil=64000:random_seed=2902021945:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi)
% 68.26/10.00 % (403350)Instruction limit reached!
% 68.26/10.00 % (403350)------------------------------
% 68.26/10.00 % (403350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403350)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403350)Termination reason: Instruction limit
% 68.26/10.00 % (403350)Termination phase: Saturation
% 68.26/10.00 % (403350)Time elapsed: 2.699 s
% 68.26/10.00 % (403350)Peak memory usage: 23 MB
% 68.26/10.00 % (403350)Instructions burned: 9156 (million)
% 68.26/10.00 % (403357)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1609289390:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi)
% 68.26/10.00 % Exception at run slice level
% 68.26/10.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.26/10.00 % (403359)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1966790251:i=11404_2938 on theBenchmark for (2938ds/11404Mi)
% 68.26/10.00 % (403348)Instruction limit reached!
% 68.26/10.00 % (403348)------------------------------
% 68.26/10.00 % (403348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.00 % (403348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.00 % (403348)CaDiCaL version: 2.1.3
% 68.26/10.00 % (403348)Termination reason: Instruction limit
% 68.26/10.00 % (403348)Termination phase: Saturation
% 68.26/10.00 % (403348)Time elapsed: 4.287 s
% 68.26/10.00 % (403348)Peak memory usage: 25 MB
% 68.26/10.00 % (403348)Instructions burned: 8174 (million)
% 68.26/10.00 % (403363)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=176597715:i=14134_2928 on theBenchmark for (2928ds/14134Mi)
% 68.26/10.00 % (403363)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.26/10.00 % (403336) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-403264-403336"...
% 68.26/10.00 % (403336)...printing done.
% 68.26/10.00 % (403336)Refutation found. Thanks to Tanya!
% 68.26/10.00 % SZS status Theorem for theBenchmark
% 68.26/10.00 % SZS output start Proof for theBenchmark
% 68.26/10.00 thf(type_def_5, type, mu: $tType).
% 68.26/10.00 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 68.26/10.00 thf(func_def_0, type, meq_ind: (mu > mu > $i > $o)).
% 68.26/10.00 thf(func_def_1, type, meq_prop: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_3, type, mnot: (($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_4, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_5, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_6, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_7, type, mimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_8, type, mequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_9, type, mxor: (($i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_10, type, mforall_ind: ((mu > $i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_11, type, mforall_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_12, type, mexists_ind: ((mu > $i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_13, type, mexists_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_14, type, mtrue: ($i > $o)).
% 68.26/10.00 thf(func_def_15, type, mfalse: ($i > $o)).
% 68.26/10.00 thf(func_def_16, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_17, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 68.26/10.00 thf(func_def_18, type, mreflexive: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_19, type, msymmetric: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_20, type, mserial: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_21, type, mtransitive: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_22, type, meuclidean: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_23, type, mpartially_functional: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_24, type, mfunctional: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_25, type, mweakly_dense: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_26, type, mweakly_connected: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_27, type, mweakly_directed: (($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_28, type, mvalid: (($i > $o) > $o)).
% 68.26/10.00 thf(func_def_29, type, minvalid: (($i > $o) > $o)).
% 68.26/10.00 thf(func_def_30, type, msatisfiable: (($i > $o) > $o)).
% 68.26/10.00 thf(func_def_31, type, mcountersatisfiable: (($i > $o) > $o)).
% 68.26/10.00 thf(func_def_32, type, i: ($i > $i > $o)).
% 68.26/10.00 thf(func_def_33, type, j: ($i > $i > $o)).
% 68.26/10.00 thf(func_def_34, type, k: ($i > $i > $o)).
% 68.26/10.00 thf(func_def_35, type, l: ($i > $i > $o)).
% 68.26/10.00 thf(func_def_36, type, confluence: (($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $o)).
% 68.26/10.00 thf(func_def_37, type, db2: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_38, type, db1: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_39, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 68.26/10.00 thf(func_def_40, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 68.26/10.00 thf(func_def_41, type, db0: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_42, type, vNOT: ($o > $o)).
% 68.26/10.00 thf(func_def_43, type, vOR: ($o > $o > $o)).
% 68.26/10.00 thf(func_def_44, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 68.26/10.00 thf(func_def_47, type, db3: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_48, type, vIMP: ($o > $o > $o)).
% 68.26/10.00 thf(func_def_49, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 68.26/10.00 thf(func_def_50, type, vAND: ($o > $o > $o)).
% 68.26/10.00 thf(func_def_51, type, db4: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_52, type, db6: !>[X0: $tType]:(X0)).
% 68.26/10.00 thf(func_def_56, type, sK3: ($i > $o)).
% 68.26/10.00 thf(func_def_60, type, sK7: (($i > $o) > $i > $i)).
% 68.26/10.00 thf(func_def_61, type, sK8: ($i > ($i > $o) > $i)).
% 68.26/10.00 thf(func_def_62, type, sK9: ($i > $i > $i)).
% 68.26/10.00 thf(func_def_64, type, sK11: (($i > $o) > ($i > $i) > $i)).
% 68.26/10.00 thf(func_def_65, type, sK12: (($i > $o) > $i)).
% 68.26/10.00 thf(func_def_66, type, sK13: (($i > $i) > $i)).
% 68.26/10.00 thf(func_def_67, type, sK14: (($i > $o) > $i)).
% 68.26/10.00 thf(func_def_68, type, sK15: (($i > $o) > ($i > $i) > $i)).
% 68.26/10.00 thf(func_def_69, type, sK16: (($i > $i) > $i)).
% 68.26/10.00 thf(func_def_70, type, sK17: (($i > $o) > $i)).
% 68.26/10.00 thf(f3,axiom,(
% 68.26/10.00 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mnot)).
% 68.26/10.00 thf(f4,axiom,(
% 68.26/10.00 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mor)).
% 68.26/10.00 thf(f6,axiom,(
% 68.26/10.00 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mimplies)).
% 68.26/10.00 thf(f11,axiom,(
% 68.26/10.00 (mforall_prop = (^[X0 : (($i > $o) > $i > $o), X1 : $i] : (! [X2 : ($i > $o)] : (X0 @ X2 @ X1))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mforall_prop)).
% 68.26/10.00 thf(f16,axiom,(
% 68.26/10.00 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : ((X1 @ X3) | ~(X0 @ X2 @ X3)))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mbox)).
% 68.26/10.00 thf(f17,axiom,(
% 68.26/10.00 (mdia = (^[X0 : ($i > $i > $o), X1 : ($i > $o)] : ((mnot @ (mbox @ X0 @ (mnot @ X1))))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mdia)).
% 68.26/10.00 thf(f28,axiom,(
% 68.26/10.00 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mvalid)).
% 68.26/10.00 thf(f32,axiom,(
% 68.26/10.00 (confluence = (^[X0 : ($i > $i > $o), X1 : ($i > $i > $o), X2 : ($i > $i > $o), X3 : ($i > $i > $o)] : (! [X4 : $i,X5 : $i,X6 : $i] : (((X2 @ X4 @ X6) & (X0 @ X4 @ X5)) => ? [X7 : $i] : ((X3 @ X6 @ X7) & (X1 @ X5 @ X7))))))),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',confluence)).
% 68.26/10.00 thf(f33,conjecture,(
% 68.26/10.00 (mvalid @ (mforall_prop @ (^[X0 : ($i > $o)] : ((mimplies @ (mdia @ i @ (mbox @ j @ X0)) @ (mbox @ k @ (mdia @ l @ X0))))))) <=> (confluence @ i @ j @ k @ l)),
% 68.26/10.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 68.26/10.00 thf(f34,negated_conjecture,(
% 68.26/10.00 ~((mvalid @ (mforall_prop @ (^[X0 : ($i > $o)] : ((mimplies @ (mdia @ i @ (mbox @ j @ X0)) @ (mbox @ k @ (mdia @ l @ X0))))))) <=> (confluence @ i @ j @ k @ l))),
% 68.26/10.00 inference(negated_conjecture,[status(cth)],[f33])).
% 68.26/10.00 thf(f37,plain,(
% 68.26/10.00 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 68.26/10.00 inference(rectify,[],[f3])).
% 68.26/10.00 thf(f38,plain,(
% 68.26/10.00 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 68.26/10.00 inference(fool_elimination,[],[f37])).
% 68.26/10.00 thf(f39,plain,(
% 68.26/10.00 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 68.26/10.00 inference(rectify,[],[f4])).
% 68.26/10.00 thf(f40,plain,(
% 68.26/10.00 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 68.26/10.00 inference(fool_elimination,[],[f39])).
% 68.26/10.00 thf(f42,plain,(
% 68.26/10.00 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 68.26/10.00 inference(fool_elimination,[],[f6])).
% 68.26/10.00 thf(f48,plain,(
% 68.26/10.00 (mforall_prop = (^[X0 : (($i > $o) > $i > $o), X1 : $i] : (! [X2 : ($i > $o)] : (X0 @ X2 @ X1))))),
% 68.26/10.00 inference(rectify,[],[f11])).
% 68.26/10.00 thf(f49,plain,(
% 68.26/10.00 (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))))),
% 68.26/10.00 inference(fool_elimination,[],[f48])).
% 68.26/10.00 thf(f55,plain,(
% 68.26/10.00 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : ((X1 @ X3) | ~(X0 @ X2 @ X3)))))),
% 68.26/10.00 inference(rectify,[],[f16])).
% 68.26/10.00 thf(f56,plain,(
% 68.26/10.00 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3))))))))))),
% 68.26/10.00 inference(fool_elimination,[],[f55])).
% 68.26/10.00 thf(f57,plain,(
% 68.26/10.00 (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: (mnot @ (mbox @ Y0 @ (mnot @ Y1)))))))),
% 68.26/10.00 inference(fool_elimination,[],[f17])).
% 68.26/10.00 thf(f78,plain,(
% 68.26/10.00 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 68.26/10.00 inference(rectify,[],[f28])).
% 68.26/10.00 thf(f79,plain,(
% 68.26/10.00 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 68.26/10.00 inference(fool_elimination,[],[f78])).
% 68.26/10.00 thf(f86,plain,(
% 68.26/10.00 (confluence = (^[X0 : ($i > $i > $o), X1 : ($i > $i > $o), X2 : ($i > $i > $o), X3 : ($i > $i > $o)] : (! [X4 : $i,X5 : $i,X6 : $i] : (((X2 @ X4 @ X6) & (X0 @ X4 @ X5)) => ? [X7 : $i] : ((X3 @ X6 @ X7) & (X1 @ X5 @ X7))))))),
% 68.26/10.00 inference(rectify,[],[f32])).
% 68.26/10.00 thf(f87,plain,(
% 68.26/10.00 (confluence = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $i > $o]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((Y0 @ Y6 @ Y5) & (Y2 @ Y6 @ Y4)) => (?? @ $i @ (^[Y7 : $i]: ((Y1 @ Y5 @ Y7) & (Y3 @ Y4 @ Y7)))))))))))))))))))),
% 68.26/10.00 inference(fool_elimination,[],[f86])).
% 68.26/10.00 thf(f88,plain,(
% 68.26/10.00 ~((mvalid @ (mforall_prop @ (^[X0 : ($i > $o)] : ((mimplies @ (mdia @ i @ (mbox @ j @ X0)) @ (mbox @ k @ (mdia @ l @ X0))))))) <=> (confluence @ i @ j @ k @ l))),
% 68.26/10.00 inference(rectify,[],[f34])).
% 68.26/10.00 thf(f89,plain,(
% 68.26/10.00 ~ (((confluence @ i @ j @ k @ l)) = ((mvalid @ (mforall_prop @ (^[Y0 : $i > $o]: (mimplies @ (mdia @ i @ (mbox @ j @ Y0)) @ (mbox @ k @ (mdia @ l @ Y0))))))))),
% 68.26/10.00 inference(fool_elimination,[],[f88])).
% 68.26/10.00 thf(f90,plain,(
% 68.26/10.00 (((confluence @ i @ j @ k @ l)) != ((mvalid @ (mforall_prop @ (^[Y0 : $i > $o]: (mimplies @ (mdia @ i @ (mbox @ j @ Y0)) @ (mbox @ k @ (mdia @ l @ Y0))))))))),
% 68.26/10.00 inference(flattening,[],[f89])).
% 68.26/10.00 thf(f93,plain,(
% 68.26/10.00 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f38])).
% 68.26/10.00 thf(f94,plain,(
% 68.26/10.00 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f40])).
% 68.26/10.00 thf(f96,plain,(
% 68.26/10.00 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 68.26/10.00 inference(cnf_transformation,[],[f42])).
% 68.26/10.00 thf(f101,plain,(
% 68.26/10.00 (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f49])).
% 68.26/10.00 thf(f106,plain,(
% 68.26/10.00 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (Y0 @ Y2 @ Y3)) | (Y1 @ Y3))))))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f56])).
% 68.26/10.00 thf(f107,plain,(
% 68.26/10.00 (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: (mnot @ (mbox @ Y0 @ (mnot @ Y1)))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f57])).
% 68.26/10.00 thf(f118,plain,(
% 68.26/10.00 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 68.26/10.00 inference(cnf_transformation,[],[f79])).
% 68.26/10.00 thf(f122,plain,(
% 68.26/10.00 (confluence = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $i > $o]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((Y0 @ Y6 @ Y5) & (Y2 @ Y6 @ Y4)) => (?? @ $i @ (^[Y7 : $i]: ((Y1 @ Y5 @ Y7) & (Y3 @ Y4 @ Y7)))))))))))))))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f87])).
% 68.26/10.00 thf(f123,plain,(
% 68.26/10.00 (((confluence @ i @ j @ k @ l)) != ((mvalid @ (mforall_prop @ (^[Y0 : $i > $o]: (mimplies @ (mdia @ i @ (mbox @ j @ Y0)) @ (mbox @ k @ (mdia @ l @ Y0))))))))),
% 68.26/10.00 inference(cnf_transformation,[],[f90])).
% 68.26/10.00 thf(f125,definition,(
% 68.26/10.00 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 68.26/10.00 introduced(theory,[fool_exhaustiveness_axiom])).
% 68.26/10.00 thf(f127,plain,(
% 68.26/10.00 (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)))))),
% 68.26/10.00 inference(definition_unfolding,[],[f96,f94,f93])).
% 68.26/10.00 thf(f134,plain,(
% 68.26/10.00 (mdia = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((~ (Y2 @ Y4 @ Y5)) | (Y3 @ Y5))))))))) @ Y0 @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y1)))))))),
% 68.26/10.00 inference(definition_unfolding,[],[f107,f93,f106,f93])).
% 68.26/10.00 thf(f135,plain,(
% 68.26/10.00 ((((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $i > $o]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((Y0 @ Y6 @ Y5) & (Y2 @ Y6 @ Y4)) => (?? @ $i @ (^[Y7 : $i]: ((Y1 @ Y5 @ Y7) & (Y3 @ Y4 @ Y7)))))))))))))))))) @ i @ j @ k @ l)) != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: ((Y3 @ Y5) | (Y4 @ Y5))))))) @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y1) @ Y2)))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ i @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ j @ Y0)) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ k @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ l @ Y0))))))))),
% 68.26/10.00 inference(definition_unfolding,[],[f123,f122,f118,f101,f127,f134,f106,f106,f134])).
% 68.26/10.00 thf(f136,plain,(
% 68.26/10.00 ($true = (((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $i > $o]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((Y0 @ Y6 @ Y5) & (Y2 @ Y6 @ Y4)) => (?? @ $i @ (^[Y7 : $i]: ((Y1 @ Y5 @ Y7) & (Y3 @ Y4 @ Y7)))))))))))))))))) @ i @ j @ k @ l))) | ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: ((Y3 @ Y5) | (Y4 @ Y5))))))) @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y1) @ Y2)))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ i @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ j @ Y0)) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ k @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ l @ Y0))))))))),
% 68.26/10.00 inference(xor_proxy_clausification,[],[f135])).
% 68.26/10.00 thf(f137,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $i > $o]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (((Y0 @ Y6 @ Y5) & (Y2 @ Y6 @ Y4)) => (?? @ $i @ (^[Y7 : $i]: ((Y1 @ Y5 @ Y7) & (Y3 @ Y4 @ Y7)))))))))))))))))) @ i @ j @ k @ l))) | ($false = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: ((Y3 @ Y5) | (Y4 @ Y5))))))) @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y1) @ Y2)))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ i @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ j @ Y0)) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (Y1 @ Y3 @ Y4)) | (Y2 @ Y4))))))))) @ k @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ ((^[Y3 : $i > $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((~ (Y3 @ Y5 @ Y6)) | (Y4 @ Y6))))))))) @ Y1 @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y2)))))) @ l @ Y0))))))))),
% 68.26/10.00 inference(xor_proxy_clausification,[],[f135])).
% 68.26/10.00 thf(f138,plain,(
% 68.26/10.00 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3))))))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f137])).
% 68.26/10.00 thf(f139,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3)))))))))) @ sK0))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))))))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f138])).
% 68.26/10.00 thf(f140,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3)))))))))) @ sK0))) | ($false = (((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))) @ sK1)))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f139])).
% 68.26/10.00 thf(f141,plain,(
% 68.26/10.00 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ sK0)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ sK0 @ Y2))))))))))) | ($false = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f140])).
% 68.26/10.00 thf(f142,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ sK0)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ sK0 @ Y2)))))))) @ sK2))) | ($false = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))))))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f141])).
% 68.26/10.00 thf(f143,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ sK0)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ sK0 @ Y2)))))))) @ sK2))) | ($false = (((^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ sK1 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))) @ sK3)))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f142])).
% 68.26/10.00 thf(f144,plain,(
% 68.26/10.00 ($false = ((!! @ $i @ (^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1))))))))) | ($false = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1)))))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (k @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (sK3 @ Y1))))))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f143])).
% 68.26/10.00 thf(f145,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1)))))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (k @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (sK3 @ Y1))))))))))))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f144])).
% 68.26/10.00 thf(f146,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (k @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (sK3 @ Y1)))))))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f145])).
% 68.26/10.00 thf(f147,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1))))))))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f145])).
% 68.26/10.00 thf(f148,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1)))))))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f147])).
% 68.26/10.00 thf(f149,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1))))))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f148])).
% 68.26/10.00 thf(f150,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = (((^[Y0 : $i]: ((~ (i @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (sK3 @ Y1))))))) @ sK5)))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f149])).
% 68.26/10.00 thf(f151,plain,(
% 68.26/10.00 ($false = ((((i @ sK4 @ sK2) & (k @ sK4 @ sK0)) => (?? @ $i @ (^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))))))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f150])).
% 68.26/10.00 thf(f152,plain,(
% 68.26/10.00 ($false = ((?? @ $i @ (^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0)))))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))),
% 68.26/10.00 inference(imp_proxy_clausification,[],[f151])).
% 68.26/10.00 thf(f153,plain,(
% 68.26/10.00 ($true = (((i @ sK4 @ sK2) & (k @ sK4 @ sK0)))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))),
% 68.26/10.00 inference(imp_proxy_clausification,[],[f151])).
% 68.26/10.00 thf(f154,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))),
% 68.26/10.00 inference(and_proxy_clausification,[],[f153])).
% 68.26/10.00 thf(f155,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))),
% 68.26/10.00 inference(and_proxy_clausification,[],[f153])).
% 68.26/10.00 thf(f156,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0)))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f155])).
% 68.26/10.00 thf(f157,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = ((~ (i @ sK1 @ sK5))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f155])).
% 68.26/10.00 thf(f158,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($true = ((i @ sK1 @ sK5)))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f157])).
% 68.26/10.00 thf(f159,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f156])).
% 68.26/10.00 thf(f160,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = (((^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))) @ X1)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f159])).
% 68.26/10.00 thf(f161,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = (((~ (j @ sK5 @ X1)) | (sK3 @ X1))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f160])).
% 68.26/10.00 thf(f162,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = ((sK3 @ X1))) | ($true = ((~ (j @ sK5 @ X1))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f161])).
% 68.26/10.00 thf(f163,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = ((sK3 @ X1))) | ($false = ((j @ sK5 @ X1)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f162])).
% 68.26/10.00 thf(f164,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0)))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f154])).
% 68.26/10.00 thf(f165,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = ((~ (i @ sK1 @ sK5))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f154])).
% 68.26/10.00 thf(f166,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($true = ((i @ sK1 @ sK5)))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f165])).
% 68.26/10.00 thf(f167,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f164])).
% 68.26/10.00 thf(f168,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = (((^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))) @ X1)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f167])).
% 68.26/10.00 thf(f169,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = (((~ (j @ sK5 @ X1)) | (sK3 @ X1))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f168])).
% 68.26/10.00 thf(f170,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = ((sK3 @ X1))) | ($true = ((~ (j @ sK5 @ X1))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f169])).
% 68.26/10.00 thf(f171,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = ((sK3 @ X1))) | ($false = ((j @ sK5 @ X1)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f170])).
% 68.26/10.00 thf(f172,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = (((~ (i @ sK1 @ sK5)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f152])).
% 68.26/10.00 thf(f173,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0)))))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f172])).
% 68.26/10.00 thf(f174,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = ((~ (i @ sK1 @ sK5))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f172])).
% 68.26/10.00 thf(f175,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = ((i @ sK1 @ sK5)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f174])).
% 68.26/10.00 thf(f176,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((j @ sK2 @ X1) & (l @ sK0 @ X1)))) | ($true = ((i @ sK1 @ sK5)))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f175])).
% 68.26/10.00 thf(f177,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = ((i @ sK1 @ sK5))) | ($false = ((j @ sK2 @ X1)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f176])).
% 68.26/10.00 thf(f178,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f173])).
% 68.26/10.00 thf(f179,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (j @ sK5 @ Y0)) | (sK3 @ Y0))) @ X2)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f178])).
% 68.26/10.00 thf(f180,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = (((j @ sK2 @ X1) & (l @ sK0 @ X1)))) | ($true = (((~ (j @ sK5 @ X2)) | (sK3 @ X2))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f179])).
% 68.26/10.00 thf(f181,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = (((~ (j @ sK5 @ X2)) | (sK3 @ X2)))) | ($false = ((j @ sK2 @ X1)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f180])).
% 68.26/10.00 thf(f182,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = ((sK3 @ X2))) | ($false = ((j @ sK2 @ X1))) | ($true = ((~ (j @ sK5 @ X2))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f181])).
% 68.26/10.00 thf(f183,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = ((sK3 @ X2))) | ($false = ((j @ sK2 @ X1))) | ($false = ((j @ sK5 @ X2)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f182])).
% 68.26/10.00 thf(f184,plain,(
% 68.26/10.00 ($false = (((^[Y0 : $i]: (((i @ Y0 @ sK2) & (k @ Y0 @ sK0)) => (?? @ $i @ (^[Y1 : $i]: ((j @ sK2 @ Y1) & (l @ sK0 @ Y1)))))) @ sK4))) | ($false = (((^[Y0 : $i]: ((~ (k @ sK1 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (sK3 @ Y1)))))))) @ sK6)))),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f146])).
% 68.26/10.00 thf(f185,plain,(
% 68.26/10.00 ($false = ((((i @ sK4 @ sK2) & (k @ sK4 @ sK0)) => (?? @ $i @ (^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))))))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f184])).
% 68.26/10.00 thf(f186,plain,(
% 68.26/10.00 ($false = ((?? @ $i @ (^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0)))))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))),
% 68.26/10.00 inference(imp_proxy_clausification,[],[f185])).
% 68.26/10.00 thf(f187,plain,(
% 68.26/10.00 ($true = (((i @ sK4 @ sK2) & (k @ sK4 @ sK0)))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))),
% 68.26/10.00 inference(imp_proxy_clausification,[],[f185])).
% 68.26/10.00 thf(f188,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))),
% 68.26/10.00 inference(and_proxy_clausification,[],[f187])).
% 68.26/10.00 thf(f189,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))),
% 68.26/10.00 inference(and_proxy_clausification,[],[f187])).
% 68.26/10.00 thf(f190,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0))))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f189])).
% 68.26/10.00 thf(f191,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($false = ((~ (k @ sK1 @ sK6))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f189])).
% 68.26/10.00 thf(f192,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($true = ((k @ sK1 @ sK6)))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f191])).
% 68.26/10.00 thf(f193,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f190])).
% 68.26/10.00 thf(f194,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = (((^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))) @ X1)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f193])).
% 68.26/10.00 thf(f195,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = (((~ (l @ sK6 @ X1)) | (~ (sK3 @ X1)))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f194])).
% 68.26/10.00 thf(f196,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($true = ((~ (sK3 @ X1)))) | ($true = ((~ (l @ sK6 @ X1))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f195])).
% 68.26/10.00 thf(f197,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($false = ((sK3 @ X1))) | ($true = ((~ (l @ sK6 @ X1))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f196])).
% 68.26/10.00 thf(f198,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((i @ sK4 @ sK2))) | ($false = ((sK3 @ X1))) | ($false = ((l @ sK6 @ X1)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f197])).
% 68.26/10.00 thf(f199,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0))))))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f188])).
% 68.26/10.00 thf(f200,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($false = ((~ (k @ sK1 @ sK6))))),
% 68.26/10.00 inference(or_proxy_clausification,[],[f188])).
% 68.26/10.00 thf(f201,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($true = ((k @ sK1 @ sK6)))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f200])).
% 68.26/10.00 thf(f202,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))),
% 68.26/10.00 inference(not_proxy_clausification,[],[f199])).
% 68.26/10.00 thf(f203,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = (((^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))) @ X1)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f202])).
% 68.26/10.00 thf(f204,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = (((~ (l @ sK6 @ X1)) | (~ (sK3 @ X1)))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f203])).
% 68.26/10.00 thf(f205,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($true = ((~ (sK3 @ X1)))) | ($true = ((~ (l @ sK6 @ X1))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f204])).
% 68.26/10.00 thf(f206,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($false = ((sK3 @ X1))) | ($true = ((~ (l @ sK6 @ X1))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f205])).
% 68.26/10.00 thf(f207,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((k @ sK4 @ sK0))) | ($false = ((sK3 @ X1))) | ($false = ((l @ sK6 @ X1)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f206])).
% 68.26/10.00 thf(f208,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = (((~ (k @ sK1 @ sK6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f186])).
% 68.26/10.00 thf(f209,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0))))))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f208])).
% 68.26/10.00 thf(f210,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($false = ((~ (k @ sK1 @ sK6))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f208])).
% 68.26/10.00 thf(f211,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = ((k @ sK1 @ sK6)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f210])).
% 68.26/10.00 thf(f212,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((j @ sK2 @ X1) & (l @ sK0 @ X1)))) | ($true = ((k @ sK1 @ sK6)))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f211])).
% 68.26/10.00 thf(f213,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = ((k @ sK1 @ sK6))) | ($false = ((j @ sK2 @ X1)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f212])).
% 68.26/10.00 thf(f214,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f209])).
% 68.26/10.00 thf(f215,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((j @ sK2 @ Y0) & (l @ sK0 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (l @ sK6 @ Y0)) | (~ (sK3 @ Y0)))) @ X2)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f214])).
% 68.26/10.00 thf(f216,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = (((j @ sK2 @ X1) & (l @ sK0 @ X1)))) | ($true = (((~ (l @ sK6 @ X2)) | (~ (sK3 @ X2)))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f215])).
% 68.26/10.00 thf(f217,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = (((~ (l @ sK6 @ X2)) | (~ (sK3 @ X2))))) | ($false = ((j @ sK2 @ X1)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f216])).
% 68.26/10.00 thf(f218,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($true = ((~ (sK3 @ X2)))) | ($false = ((j @ sK2 @ X1))) | ($true = ((~ (l @ sK6 @ X2))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f217])).
% 68.26/10.00 thf(f219,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($false = ((sK3 @ X2))) | ($false = ((j @ sK2 @ X1))) | ($true = ((~ (l @ sK6 @ X2))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f218])).
% 68.26/10.00 thf(f220,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($false = ((sK3 @ X2))) | ($false = ((j @ sK2 @ X1))) | ($false = ((l @ sK6 @ X2)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f219])).
% 68.26/10.00 thf(f221,plain,(
% 68.26/10.00 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3))))))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))))))),
% 68.26/10.00 inference(beta-eta_normalization,[],[f136])).
% 68.26/10.00 thf(f222,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3)))))))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f221])).
% 68.26/10.00 thf(f223,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((i @ Y2 @ Y1) & (k @ Y2 @ Y0)) => (?? @ $i @ (^[Y3 : $i]: ((j @ Y1 @ Y3) & (l @ Y0 @ Y3)))))))))) @ X1))) | ($true = (((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y2 : $i]: ((~ (i @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (j @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) | (!! @ $i @ (^[Y2 : $i]: ((~ (k @ Y0 @ Y2)) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (l @ Y2 @ Y3)) | (~ (Y1 @ Y3))))))))))))) @ X2)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f222])).
% 68.26/10.00 thf(f224,plain,(
% 68.26/10.00 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ X1)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ X1 @ Y2))))))))))) | ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f223])).
% 68.26/10.00 thf(f225,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ X1)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ X1 @ Y2)))))))) @ X3))) | ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f224])).
% 68.26/10.00 thf(f226,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : ($i > $o)] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((i @ Y1 @ Y0) & (k @ Y1 @ X1)) => (?? @ $i @ (^[Y2 : $i]: ((j @ Y0 @ Y2) & (l @ X1 @ Y2)))))))) @ X3))) | ($true = (((^[Y0 : $i > $o]: ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (i @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (j @ Y1 @ Y2)) | (Y0 @ Y2)))))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (k @ X2 @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (l @ Y1 @ Y2)) | (~ (Y0 @ Y2))))))))))) @ X4)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f225])).
% 68.26/10.00 thf(f227,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : ($i > $o)] : (($true = ((!! @ $i @ (^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1))))))))) | ($true = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1)))))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1))))))))))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f226])).
% 68.26/10.00 thf(f228,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1)))))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1))))))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f227])).
% 68.26/10.00 thf(f229,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1))))))))))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f228])).
% 68.26/10.00 thf(f230,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = (((^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1)))))))) @ X6))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1))))))))))))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f229])).
% 68.26/10.00 thf(f231,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = (((^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1)))))))) @ X6))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1)))))))))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f230])).
% 68.26/10.00 thf(f232,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = (((^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1)))))))) @ X6))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1))))))))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f231])).
% 68.26/10.00 thf(f233,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($true = (((^[Y0 : $i]: (((i @ Y0 @ X3) & (k @ Y0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: ((j @ X3 @ Y1) & (l @ X1 @ Y1)))))) @ X5))) | ($true = (((^[Y0 : $i]: ((~ (k @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (l @ Y0 @ Y1)) | (~ (X4 @ Y1)))))))) @ X6))) | ($true = (((^[Y0 : $i]: ((~ (i @ X2 @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (j @ Y0 @ Y1)) | (X4 @ Y1))))))) @ X7)))) )),
% 68.26/10.00 inference(pi_proxy_clausification,[],[f232])).
% 68.26/10.00 thf(f234,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($true = ((((i @ X5 @ X3) & (k @ X5 @ X1)) => (?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0))))))) | ($true = (((~ (k @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0))))))))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))))))))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f233])).
% 68.26/10.00 thf(f235,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = (((i @ X5 @ X3) & (k @ X5 @ X1)))) | ($true = (((~ (k @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0))))))))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0))))))) )),
% 68.26/10.00 inference(imp_proxy_clausification,[],[f234])).
% 68.26/10.00 thf(f236,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = (((~ (k @ X2 @ X6)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0))))))))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f235])).
% 68.26/10.00 thf(f237,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))))))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f236])).
% 68.26/10.00 thf(f238,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0))))))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f237])).
% 68.26/10.00 thf(f239,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($true = (((~ (i @ X2 @ X7)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6))))) )),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f238])).
% 68.26/10.00 thf(f240,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6)))) | ($true = ((~ (i @ X2 @ X7))))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f239])).
% 68.26/10.00 thf(f241,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0)))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6)))) | ($true = ((~ (i @ X2 @ X7))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f240])).
% 68.26/10.00 thf(f242,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($false = (((^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))) @ (sK8 @ X7 @ X4)))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0)))))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6)))) | ($true = ((~ (i @ X2 @ X7))))) )),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f241])).
% 68.26/10.00 thf(f243,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($false = (((^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))) @ (sK8 @ X7 @ X4)))) | ($true = (((^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0))) @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($true = ((~ (k @ X2 @ X6)))) | ($true = ((~ (i @ X2 @ X7))))) )),
% 68.26/10.00 inference(sigma_proxy_clausification,[],[f242])).
% 68.26/10.00 thf(f244,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($false = (((^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))) @ (sK8 @ X7 @ X4)))) | ($true = (((^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0))) @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($true = ((~ (i @ X2 @ X7))))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f243])).
% 68.26/10.00 thf(f245,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((^[Y0 : $i]: ((~ (l @ X6 @ Y0)) | (~ (X4 @ Y0)))) @ (sK7 @ X4 @ X6)))) | ($false = (((^[Y0 : $i]: ((~ (j @ X7 @ Y0)) | (X4 @ Y0))) @ (sK8 @ X7 @ X4)))) | ($true = (((^[Y0 : $i]: ((j @ X3 @ Y0) & (l @ X1 @ Y0))) @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f244])).
% 68.26/10.00 thf(f246,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = (((~ (l @ X6 @ (sK7 @ X4 @ X6))) | (~ (X4 @ (sK7 @ X4 @ X6)))))) | ($false = (((~ (j @ X7 @ (sK8 @ X7 @ X4))) | (X4 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(beta-eta_normalization,[],[f245])).
% 68.26/10.00 thf(f247,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((~ (X4 @ (sK7 @ X4 @ X6))))) | ($false = (((~ (j @ X7 @ (sK8 @ X7 @ X4))) | (X4 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f246])).
% 68.26/10.00 thf(f248,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((~ (l @ X6 @ (sK7 @ X4 @ X6))))) | ($false = (((~ (j @ X7 @ (sK8 @ X7 @ X4))) | (X4 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f246])).
% 68.26/10.00 thf(f249,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = (((~ (j @ X7 @ (sK8 @ X7 @ X4))) | (X4 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f248])).
% 68.26/10.00 thf(f250,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f249])).
% 68.26/10.00 thf(f251,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((~ (j @ X7 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f249])).
% 68.26/10.00 thf(f252,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f251])).
% 68.26/10.00 thf(f253,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f252])).
% 68.26/10.00 thf(f254,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f252])).
% 68.26/10.00 thf(f255,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f250])).
% 68.26/10.00 thf(f256,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f250])).
% 68.26/10.00 thf(f257,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = (((~ (j @ X7 @ (sK8 @ X7 @ X4))) | (X4 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f247])).
% 68.26/10.00 thf(f258,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f257])).
% 68.26/10.00 thf(f259,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((~ (j @ X7 @ (sK8 @ X7 @ X4))))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(or_proxy_clausification,[],[f257])).
% 68.26/10.00 thf(f260,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = (((j @ X3 @ (sK9 @ X3 @ X1)) & (l @ X1 @ (sK9 @ X3 @ X1))))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(not_proxy_clausification,[],[f259])).
% 68.26/10.00 thf(f261,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f260])).
% 68.26/10.00 thf(f262,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f260])).
% 68.26/10.00 thf(f263,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f258])).
% 68.26/10.00 thf(f264,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : $i,X7 : $i,X4 : ($i > $o),X5 : $i] : (($false = ((k @ X5 @ X1))) | ($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1)))) | ($false = ((i @ X5 @ X3))) | ($false = ((k @ X2 @ X6))) | ($false = ((i @ X2 @ X7)))) )),
% 68.26/10.00 inference(and_proxy_clausification,[],[f258])).
% 68.26/10.00 thf(f266,definition,(
% 68.26/10.00 spl10_1 <=> ($true = ((i @ sK1 @ sK5)))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition])).
% 68.26/10.00 thf(f268,plain,(
% 68.26/10.00 ($true = ((i @ sK1 @ sK5))) | ~spl10_1),
% 68.26/10.00 inference(avatar_component_clause,[],[f266])).
% 68.26/10.00 thf(f270,definition,(
% 68.26/10.00 spl10_2 <=> ($true = ((i @ sK4 @ sK2)))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition])).
% 68.26/10.00 thf(f271,plain,(
% 68.26/10.00 ($true != ((i @ sK4 @ sK2))) | spl10_2),
% 68.26/10.00 inference(avatar_component_clause,[],[f270])).
% 68.26/10.00 thf(f272,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | ~spl10_2),
% 68.26/10.00 inference(avatar_component_clause,[],[f270])).
% 68.26/10.00 thf(f273,plain,(
% 68.26/10.00 spl10_1 | spl10_2),
% 68.26/10.00 inference(avatar_split_clause,[],[f158,f270,f266])).
% 68.26/10.00 thf(f275,definition,(
% 68.26/10.00 spl10_3 <=> ($true = ((k @ sK4 @ sK0)))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition])).
% 68.26/10.00 thf(f276,plain,(
% 68.26/10.00 ($true != ((k @ sK4 @ sK0))) | spl10_3),
% 68.26/10.00 inference(avatar_component_clause,[],[f275])).
% 68.26/10.00 thf(f277,plain,(
% 68.26/10.00 ($true = ((k @ sK4 @ sK0))) | ~spl10_3),
% 68.26/10.00 inference(avatar_component_clause,[],[f275])).
% 68.26/10.00 thf(f278,plain,(
% 68.26/10.00 spl10_1 | spl10_3),
% 68.26/10.00 inference(avatar_split_clause,[],[f166,f275,f266])).
% 68.26/10.00 thf(f280,definition,(
% 68.26/10.00 spl10_4 <=> ($true = ((k @ sK1 @ sK6)))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition])).
% 68.26/10.00 thf(f281,plain,(
% 68.26/10.00 ($true != ((k @ sK1 @ sK6))) | spl10_4),
% 68.26/10.00 inference(avatar_component_clause,[],[f280])).
% 68.26/10.00 thf(f282,plain,(
% 68.26/10.00 ($true = ((k @ sK1 @ sK6))) | ~spl10_4),
% 68.26/10.00 inference(avatar_component_clause,[],[f280])).
% 68.26/10.00 thf(f283,plain,(
% 68.26/10.00 spl10_4 | spl10_3),
% 68.26/10.00 inference(avatar_split_clause,[],[f201,f275,f280])).
% 68.26/10.00 thf(f285,definition,(
% 68.26/10.00 spl10_5 <=> ! [X1 : $i] : (($false = ((l @ sK0 @ X1))) | ($false = ((j @ sK2 @ X1))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition])).
% 68.26/10.00 thf(f286,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((j @ sK2 @ X1))) | ($false = ((l @ sK0 @ X1)))) ) | ~spl10_5),
% 68.26/10.00 inference(avatar_component_clause,[],[f285])).
% 68.26/10.00 thf(f287,plain,(
% 68.26/10.00 spl10_4 | spl10_5),
% 68.26/10.00 inference(avatar_split_clause,[],[f213,f285,f280])).
% 68.26/10.00 thf(f289,definition,(
% 68.26/10.00 spl10_6 <=> ! [X2 : $i] : (($true = ((sK3 @ X2))) | ($false = ((j @ sK5 @ X2))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition])).
% 68.26/10.00 thf(f290,plain,(
% 68.26/10.00 ( ! [X2 : $i] : (($false = ((j @ sK5 @ X2))) | ($true = ((sK3 @ X2)))) ) | ~spl10_6),
% 68.26/10.00 inference(avatar_component_clause,[],[f289])).
% 68.26/10.00 thf(f291,plain,(
% 68.26/10.00 spl10_6 | spl10_5),
% 68.26/10.00 inference(avatar_split_clause,[],[f183,f285,f289])).
% 68.26/10.00 thf(f304,definition,(
% 68.26/10.00 spl10_7 <=> ! [X4 : ($i > $o),X7 : $i,X6 : $i,X2 : $i] : (($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_7])],[avatar_definition])).
% 68.26/10.00 thf(f305,plain,(
% 68.26/10.00 ( ! [X2 : $i,X6 : $i,X7 : $i,X4 : ($i > $o)] : (($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($false = ((X4 @ (sK8 @ X7 @ X4))))) ) | ~spl10_7),
% 68.26/10.00 inference(avatar_component_clause,[],[f304])).
% 68.26/10.00 thf(f307,definition,(
% 68.26/10.00 spl10_8 <=> ! [X5 : $i,X1 : $i,X3 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((i @ X5 @ X3))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition])).
% 68.26/10.00 thf(f308,plain,(
% 68.26/10.00 ( ! [X3 : $i,X1 : $i,X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((i @ X5 @ X3))) | ($true = ((l @ X1 @ (sK9 @ X3 @ X1))))) ) | ~spl10_8),
% 68.26/10.00 inference(avatar_component_clause,[],[f307])).
% 68.26/10.00 thf(f309,plain,(
% 68.26/10.00 spl10_7 | spl10_8),
% 68.26/10.00 inference(avatar_split_clause,[],[f263,f307,f304])).
% 68.26/10.00 thf(f332,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($true = $false) | ($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($false = (((^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))) @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_7)),
% 68.26/10.00 inference(constrained_superposition,[],[f286,f305])).
% 68.26/10.00 thf(f349,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i] : (($false != ((X0 @ (sK7 @ X0 @ X2)))) | ($true = ((X0 @ (sK7 @ X0 @ X2)))) | ($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X2))) | ($true != ((X0 @ (sK8 @ X1 @ X0))))) ) | ~spl10_7),
% 68.26/10.00 inference(equality_factoring,[],[f305])).
% 68.26/10.00 thf(f405,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($false = (((^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))) @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_7)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f332])).
% 68.26/10.00 thf(f406,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($false = ((j @ sK2 @ (X1 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0)))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_7)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f405])).
% 68.26/10.00 thf(f450,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ (sK8 @ X1 @ X0)))) | ($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X2))) | ($true = ((X0 @ (sK7 @ X0 @ X2))))) ) | ~spl10_7),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f349,f125])).
% 68.26/10.00 thf(f893,definition,(
% 68.26/10.00 spl10_9 <=> ! [X4 : ($i > $o),X7 : $i,X6 : $i,X2 : $i] : (($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($false = ((X4 @ (sK8 @ X7 @ X4)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_9])],[avatar_definition])).
% 68.26/10.00 thf(f894,plain,(
% 68.26/10.00 ( ! [X2 : $i,X6 : $i,X7 : $i,X4 : ($i > $o)] : (($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($false = ((X4 @ (sK8 @ X7 @ X4))))) ) | ~spl10_9),
% 68.26/10.00 inference(avatar_component_clause,[],[f893])).
% 68.26/10.00 thf(f895,plain,(
% 68.26/10.00 spl10_9 | spl10_8),
% 68.26/10.00 inference(avatar_split_clause,[],[f255,f307,f893])).
% 68.26/10.00 thf(f967,definition,(
% 68.26/10.00 spl10_10 <=> ! [X5 : $i,X1 : $i,X3 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((i @ X5 @ X3))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_10])],[avatar_definition])).
% 68.26/10.00 thf(f968,plain,(
% 68.26/10.00 ( ! [X3 : $i,X1 : $i,X5 : $i] : (($false = ((k @ X5 @ X1))) | ($false = ((i @ X5 @ X3))) | ($true = ((j @ X3 @ (sK9 @ X3 @ X1))))) ) | ~spl10_10),
% 68.26/10.00 inference(avatar_component_clause,[],[f967])).
% 68.26/10.00 thf(f969,plain,(
% 68.26/10.00 spl10_9 | spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f256,f967,f893])).
% 68.26/10.00 thf(f1030,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i] : (($false != ((l @ X2 @ (sK7 @ X0 @ X2)))) | ($true = ((l @ X2 @ (sK7 @ X0 @ X2)))) | ($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X2))) | ($true != ((X0 @ (sK8 @ X1 @ X0))))) ) | ~spl10_9),
% 68.26/10.00 inference(equality_factoring,[],[f894])).
% 68.26/10.00 thf(f1174,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ (sK8 @ X1 @ X0)))) | ($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X2))) | ($true = ((l @ X2 @ (sK7 @ X0 @ X2))))) ) | ~spl10_9),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f1030,f125])).
% 68.26/10.00 thf(f2111,definition,(
% 68.26/10.00 spl10_11 <=> ! [X4 : ($i > $o),X7 : $i,X6 : $i,X2 : $i] : (($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_11])],[avatar_definition])).
% 68.26/10.00 thf(f2112,plain,(
% 68.26/10.00 ( ! [X2 : $i,X6 : $i,X7 : $i,X4 : ($i > $o)] : (($true = ((X4 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4))))) ) | ~spl10_11),
% 68.26/10.00 inference(avatar_component_clause,[],[f2111])).
% 68.26/10.00 thf(f2113,plain,(
% 68.26/10.00 spl10_11 | spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f262,f967,f2111])).
% 68.26/10.00 thf(f2144,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((l @ sK0 @ (sK9 @ sK2 @ X0)))) | ($false = ((k @ X1 @ X0))) | ($false = ((i @ X1 @ sK2)))) ) | (~spl10_5 | ~spl10_10)),
% 68.26/10.00 inference(constrained_superposition,[],[f286,f968])).
% 68.26/10.00 thf(f2169,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((l @ sK0 @ (sK9 @ sK2 @ X0)))) | ($false = ((k @ X1 @ X0))) | ($false = ((i @ X1 @ sK2)))) ) | (~spl10_5 | ~spl10_10)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f2144])).
% 68.26/10.00 thf(f2232,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X0 @ sK0))) | ($false = ((i @ X0 @ sK2))) | ($false = ((k @ X1 @ sK0))) | ($false = ((i @ X1 @ sK2)))) ) | (~spl10_5 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(constrained_superposition,[],[f308,f2169])).
% 68.26/10.00 thf(f2304,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ sK0))) | ($false = ((i @ X0 @ sK2))) | ($false = ((k @ X1 @ sK0))) | ($false = ((i @ X1 @ sK2)))) ) | (~spl10_5 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f2232])).
% 68.26/10.00 thf(f2328,definition,(
% 68.26/10.00 spl10_12 <=> ! [X1 : $i] : (($false = ((k @ X1 @ sK0))) | ($false = ((i @ X1 @ sK2))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_12])],[avatar_definition])).
% 68.26/10.00 thf(f2329,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((k @ X1 @ sK0))) | ($false = ((i @ X1 @ sK2)))) ) | ~spl10_12),
% 68.26/10.00 inference(avatar_component_clause,[],[f2328])).
% 68.26/10.00 thf(f2330,plain,(
% 68.26/10.00 spl10_12 | spl10_12 | ~spl10_5 | ~spl10_8 | ~spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f2304,f967,f307,f285,f2328,f2328])).
% 68.26/10.00 thf(f2331,plain,(
% 68.26/10.00 spl10_11 | spl10_8),
% 68.26/10.00 inference(avatar_split_clause,[],[f261,f307,f2111])).
% 68.26/10.00 thf(f2385,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($true = $false) | ($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_11)),
% 68.26/10.00 inference(constrained_superposition,[],[f286,f2112])).
% 68.26/10.00 thf(f2562,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ (X1 @ Y0))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_11)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f2385])).
% 68.26/10.00 thf(f2563,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $i),X4 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X2))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))))))) | (((X1 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X1 @ Y0))) @ X2))) != X0)) ) | (~spl10_5 | ~spl10_11)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f2562])).
% 68.26/10.00 thf(f5245,definition,(
% 68.26/10.00 spl10_19 <=> ! [X4 : ($i > $o),X7 : $i,X6 : $i,X2 : $i] : (($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_19])],[avatar_definition])).
% 68.26/10.00 thf(f5246,plain,(
% 68.26/10.00 ( ! [X2 : $i,X6 : $i,X7 : $i,X4 : ($i > $o)] : (($true = ((l @ X6 @ (sK7 @ X4 @ X6)))) | ($false = ((i @ X2 @ X7))) | ($false = ((k @ X2 @ X6))) | ($true = ((j @ X7 @ (sK8 @ X7 @ X4))))) ) | ~spl10_19),
% 68.26/10.00 inference(avatar_component_clause,[],[f5245])).
% 68.26/10.00 thf(f5247,plain,(
% 68.26/10.00 spl10_19 | spl10_8),
% 68.26/10.00 inference(avatar_split_clause,[],[f253,f307,f5245])).
% 68.26/10.00 thf(f5488,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i,X6 : ($i > $i),X4 : $i,X5 : $i] : (($true = $false) | ($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK0))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X5))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ sK2 @ (X6 @ Y0))))))) | (((sK7 @ X0 @ sK0)) != ((X6 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X6 @ Y0))) @ X5))))) ) | (~spl10_5 | ~spl10_9 | ~spl10_11)),
% 68.26/10.00 inference(constrained_superposition,[],[f894,f2563])).
% 68.26/10.00 thf(f5648,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $o),X1 : $i,X6 : ($i > $i),X4 : $i,X5 : $i] : ((((sK7 @ X0 @ sK0)) != ((X6 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X6 @ Y0))) @ X5)))) | ($false = ((k @ X1 @ sK0))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ X5))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ sK2 @ (X6 @ Y0))))))) | ($false = ((i @ X1 @ X2)))) ) | (~spl10_5 | ~spl10_9 | ~spl10_11)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f5488])).
% 68.26/10.00 thf(f6015,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($true = $false) | ($false = ((l @ sK0 @ X1))) | ($false = ((i @ X2 @ sK2))) | ($false = ((k @ X2 @ X3))) | (((X0 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X0 @ Y0))) @ X3))) != X1) | ($false = ((l @ sK0 @ X4))) | ($false = ((i @ X5 @ sK2))) | ($false = ((k @ X5 @ X6))) | ((((^[Y0 : $i]: (Y0)) @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X6))) != X4) | ((^[Y0 : $i]: (Y0)) != X0)) ) | (~spl10_5 | ~spl10_7 | ~spl10_11)),
% 68.26/10.00 inference(constrained_superposition,[],[f2563,f406])).
% 68.26/10.00 thf(f6057,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($false = ((l @ sK0 @ X1))) | ($false = ((i @ X2 @ sK2))) | ($false = ((k @ X2 @ X3))) | (((X0 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X0 @ Y0))) @ X3))) != X1) | ($false = ((l @ sK0 @ X4))) | ($false = ((i @ X5 @ sK2))) | ($false = ((k @ X5 @ X6))) | ((((^[Y0 : $i]: (Y0)) @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X6))) != X4) | ((^[Y0 : $i]: (Y0)) != X0)) ) | (~spl10_5 | ~spl10_7 | ~spl10_11)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f6015])).
% 68.26/10.00 thf(f6058,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X6 : $i,X4 : $i,X5 : $i] : (($false = ((l @ sK0 @ X1))) | ($false = ((i @ X2 @ sK2))) | ($false = ((k @ X2 @ X3))) | (((X0 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X0 @ Y0))) @ X3))) != X1) | ($false = ((l @ sK0 @ X4))) | ($false = ((i @ X5 @ sK2))) | ($false = ((k @ X5 @ X6))) | (((sK7 @ (j @ sK2) @ X6)) != X4) | ((^[Y0 : $i]: (Y0)) != X0)) ) | (~spl10_5 | ~spl10_7 | ~spl10_11)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f6057])).
% 68.26/10.00 thf(f6203,plain,(
% 68.26/10.00 spl10_19 | spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f254,f967,f5245])).
% 68.26/10.00 thf(f7321,definition,(
% 68.26/10.00 spl10_20 <=> ! [X6 : $i,X4 : $i,X5 : $i] : (($false = ((l @ sK0 @ X4))) | ($false = ((i @ X5 @ sK2))) | (((sK7 @ (j @ sK2) @ X6)) != X4) | ($false = ((k @ X5 @ X6))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_20])],[avatar_definition])).
% 68.26/10.00 thf(f7322,plain,(
% 68.26/10.00 ( ! [X6 : $i,X4 : $i,X5 : $i] : ((((sK7 @ (j @ sK2) @ X6)) != X4) | ($false = ((i @ X5 @ sK2))) | ($false = ((l @ sK0 @ X4))) | ($false = ((k @ X5 @ X6)))) ) | ~spl10_20),
% 68.26/10.00 inference(avatar_component_clause,[],[f7321])).
% 68.26/10.00 thf(f7324,definition,(
% 68.26/10.00 spl10_21 <=> ! [X0 : ($i > $i),X3 : $i,X2 : $i,X1 : $i] : (($false = ((l @ sK0 @ X1))) | ((^[Y0 : $i]: (Y0)) != X0) | (((X0 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X0 @ Y0))) @ X3))) != X1) | ($false = ((i @ X2 @ sK2))) | ($false = ((k @ X2 @ X3))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_21])],[avatar_definition])).
% 68.26/10.00 thf(f7325,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i] : (((^[Y0 : $i]: (Y0)) != X0) | ($false = ((l @ sK0 @ X1))) | ($false = ((i @ X2 @ sK2))) | ($false = ((k @ X2 @ X3))) | (((X0 @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ (X0 @ Y0))) @ X3))) != X1)) ) | ~spl10_21),
% 68.26/10.00 inference(avatar_component_clause,[],[f7324])).
% 68.26/10.00 thf(f7326,plain,(
% 68.26/10.00 spl10_20 | spl10_21 | ~spl10_5 | ~spl10_7 | ~spl10_11),
% 68.26/10.00 inference(avatar_split_clause,[],[f6058,f2111,f304,f285,f7324,f7321])).
% 68.26/10.00 thf(f7327,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X0 @ sK2))) | ($false = ((l @ sK0 @ (sK7 @ (j @ sK2) @ X1)))) | ($false = ((k @ X0 @ X1)))) ) | ~spl10_20),
% 68.26/10.00 inference(equality_resolution,[],[f7322])).
% 68.26/10.00 thf(f9975,plain,(
% 68.26/10.00 spl10_7 | spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f264,f967,f304])).
% 68.26/10.00 thf(f10047,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((sK3 @ X1))) | ($false = ((j @ sK5 @ X1)))) ) | spl10_2),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f163,f271])).
% 68.26/10.00 thf(f10048,plain,(
% 68.26/10.00 spl10_6 | spl10_2),
% 68.26/10.00 inference(avatar_split_clause,[],[f10047,f270,f289])).
% 68.26/10.00 thf(f22782,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $o),X4 : $i] : (($false = ((k @ X0 @ sK0))) | ($false = ((X1 @ (sK8 @ X2 @ X1)))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ sK0))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($false = ((i @ X0 @ X2))) | (((j @ sK2)) != X1)) ) | (~spl10_5 | ~spl10_9 | ~spl10_11)),
% 68.26/10.00 inference(equality_resolution,[],[f5648])).
% 68.26/10.00 thf(f22785,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $o),X4 : $i] : (($false = ((k @ X0 @ sK0))) | ($false = ((X1 @ (sK8 @ X2 @ X1)))) | ($false = ((i @ X3 @ X4))) | ($false = ((k @ X3 @ sK0))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (j @ sK2))))) | ($false = ((i @ X0 @ X2))) | (((j @ sK2)) != X1)) ) | (~spl10_5 | ~spl10_9 | ~spl10_11)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f22782])).
% 68.26/10.00 thf(f22787,definition,(
% 68.26/10.00 spl10_28 <=> ! [X4 : $i,X3 : $i] : (($false = ((i @ X3 @ X4))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (j @ sK2))))) | ($false = ((k @ X3 @ sK0))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_28])],[avatar_definition])).
% 68.26/10.00 thf(f22788,plain,(
% 68.26/10.00 ( ! [X3 : $i,X4 : $i] : (($false = ((i @ X3 @ X4))) | ($true = ((j @ X4 @ (sK8 @ X4 @ (j @ sK2))))) | ($false = ((k @ X3 @ sK0)))) ) | ~spl10_28),
% 68.26/10.00 inference(avatar_component_clause,[],[f22787])).
% 68.26/10.00 thf(f22790,definition,(
% 68.26/10.00 spl10_29 <=> ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((k @ X0 @ sK0))) | (((j @ sK2)) != X1) | ($false = ((i @ X0 @ X2))) | ($false = ((X1 @ (sK8 @ X2 @ X1)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_29])],[avatar_definition])).
% 68.26/10.00 thf(f22791,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((j @ sK2)) != X1) | ($false = ((k @ X0 @ sK0))) | ($false = ((i @ X0 @ X2))) | ($false = ((X1 @ (sK8 @ X2 @ X1))))) ) | ~spl10_29),
% 68.26/10.00 inference(avatar_component_clause,[],[f22790])).
% 68.26/10.00 thf(f22792,plain,(
% 68.26/10.00 spl10_28 | spl10_29 | ~spl10_5 | ~spl10_9 | ~spl10_11),
% 68.26/10.00 inference(avatar_split_clause,[],[f22785,f2111,f893,f285,f22790,f22787])).
% 68.26/10.00 thf(f31095,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X4))) | ($true = ((l @ X4 @ (sK7 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X4)))) | ($false = ((i @ X5 @ X2))) | ($false = ((k @ X5 @ sK0))) | ((^[Y0 : $i]: (sK2)) != X0) | (X1 != X2) | (((X0 @ (sK8 @ X1 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ Y0))))) != X2)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(constrained_superposition,[],[f1174,f22788])).
% 68.26/10.00 thf(f31153,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X4 : $i,X5 : $i] : (($false = ((i @ X3 @ X1))) | ($false = ((k @ X3 @ X4))) | ($true = ((l @ X4 @ (sK7 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X4)))) | ($false = ((i @ X5 @ X2))) | ($false = ((k @ X5 @ sK0))) | ((^[Y0 : $i]: (sK2)) != X0) | (X1 != X2) | (((X0 @ (sK8 @ X1 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ Y0))))) != X2)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f31095])).
% 68.26/10.00 thf(f31154,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i),X1 : $i,X4 : $i,X5 : $i] : (((^[Y0 : $i]: (sK2)) != X0) | ($false = ((k @ X3 @ X4))) | ($true = ((l @ X4 @ (sK7 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ Y0)) @ X4)))) | ($false = ((i @ X5 @ X2))) | ($false = ((k @ X5 @ sK0))) | ($false = ((i @ X3 @ X1))) | (X1 != X2) | (((X0 @ (sK8 @ X1 @ (^[Y0 : $i]: (j @ (X0 @ Y0) @ Y0))))) != X2)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f31153])).
% 68.26/10.00 thf(f31343,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($false = ((k @ X0 @ X1))) | ($true = ((l @ X1 @ (sK7 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ Y0)) @ X1)))) | ($false = ((i @ X2 @ X3))) | ($false = ((k @ X2 @ sK0))) | ($false = ((i @ X0 @ X4))) | (X3 != X4) | ((((^[Y0 : $i]: (sK2)) @ (sK8 @ X4 @ (^[Y0 : $i]: (j @ ((^[Y1 : $i]: (sK2)) @ Y0) @ Y0))))) != X3)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(equality_resolution,[],[f31154])).
% 68.26/10.00 thf(f31344,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((sK2 != X3) | ($true = ((l @ X1 @ (sK7 @ (j @ sK2) @ X1)))) | ($false = ((i @ X2 @ X3))) | ($false = ((k @ X2 @ sK0))) | ($false = ((i @ X0 @ X4))) | ($false = ((k @ X0 @ X1))) | (X3 != X4)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f31343])).
% 68.26/10.00 thf(f31346,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ sK0))) | ($false = ((i @ X2 @ X3))) | ($false = ((k @ X2 @ X0))) | (sK2 != X3)) ) | (~spl10_9 | ~spl10_28)),
% 68.26/10.00 inference(equality_resolution,[],[f31344])).
% 68.26/10.00 thf(f31348,definition,(
% 68.26/10.00 spl10_34 <=> ! [X2 : $i,X0 : $i,X3 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | (sK2 != X3) | ($false = ((i @ X2 @ X3))) | ($false = ((k @ X2 @ X0))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_34])],[avatar_definition])).
% 68.26/10.00 thf(f31349,plain,(
% 68.26/10.00 ( ! [X2 : $i,X3 : $i,X0 : $i] : ((sK2 != X3) | ($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X2 @ X3))) | ($false = ((k @ X2 @ X0)))) ) | ~spl10_34),
% 68.26/10.00 inference(avatar_component_clause,[],[f31348])).
% 68.26/10.00 thf(f31350,plain,(
% 68.26/10.00 spl10_12 | spl10_34 | ~spl10_9 | ~spl10_28),
% 68.26/10.00 inference(avatar_split_clause,[],[f31346,f22787,f893,f31348,f2328])).
% 68.26/10.00 thf(f31351,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X0)))) ) | ~spl10_34),
% 68.26/10.00 inference(equality_resolution,[],[f31349])).
% 68.26/10.00 thf(f31789,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ sK0))) | ($false = ((i @ X0 @ X1))) | ($false = ((j @ sK2 @ (sK8 @ X1 @ (j @ sK2)))))) ) | ~spl10_29),
% 68.26/10.00 inference(equality_resolution,[],[f22791])).
% 68.26/10.00 thf(f31858,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X0))) | ($false = ((k @ X2 @ sK0))) | ($false = ((i @ X2 @ sK2)))) ) | (~spl10_19 | ~spl10_29)),
% 68.26/10.00 inference(constrained_superposition,[],[f5246,f31789])).
% 68.26/10.00 thf(f31918,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X0))) | ($false = ((k @ X2 @ sK0))) | ($false = ((i @ X2 @ sK2)))) ) | (~spl10_19 | ~spl10_29)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f31858])).
% 68.26/10.00 thf(f40146,definition,(
% 68.26/10.00 spl10_36 <=> ! [X0 : $i,X1 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X0))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_36])],[avatar_definition])).
% 68.26/10.00 thf(f40147,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = ((l @ X0 @ (sK7 @ (j @ sK2) @ X0)))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X0)))) ) | ~spl10_36),
% 68.26/10.00 inference(avatar_component_clause,[],[f40146])).
% 68.26/10.00 thf(f40148,plain,(
% 68.26/10.00 spl10_12 | spl10_36 | ~spl10_19 | ~spl10_29),
% 68.26/10.00 inference(avatar_split_clause,[],[f31918,f22790,f5245,f40146,f2328])).
% 68.26/10.00 thf(f40183,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((i @ X0 @ sK2))) | ($false = ((k @ X0 @ sK0))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ sK0)))) ) | (~spl10_20 | ~spl10_36)),
% 68.26/10.00 inference(constrained_superposition,[],[f7327,f40147])).
% 68.26/10.00 thf(f40372,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X0 @ sK2))) | ($false = ((k @ X0 @ sK0))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ sK0)))) ) | (~spl10_20 | ~spl10_36)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f40183])).
% 68.26/10.00 thf(f40980,plain,(
% 68.26/10.00 ($true = ((i @ sK4 @ sK2))) | spl10_4),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f192,f281])).
% 68.26/10.00 thf(f41079,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = $false) | ($true = ((l @ X1 @ (sK7 @ X0 @ X1)))) | ($false = ((i @ X2 @ sK5))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(constrained_superposition,[],[f5246,f290])).
% 68.26/10.00 thf(f41080,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = $false) | ($true = ((X0 @ (sK7 @ X0 @ X1)))) | ($false = ((i @ X2 @ sK5))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_11)),
% 68.26/10.00 inference(constrained_superposition,[],[f2112,f290])).
% 68.26/10.00 thf(f41155,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = ((X0 @ (sK7 @ X0 @ X1)))) | ($false = ((i @ X2 @ sK5))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_11)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f41080])).
% 68.26/10.00 thf(f41156,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = ((l @ X1 @ (sK7 @ X0 @ X1)))) | ($false = ((i @ X2 @ sK5))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f41079])).
% 68.26/10.00 thf(f41207,plain,(
% 68.26/10.00 ($true = $false) | ($false = ((i @ sK4 @ sK2))) | (~spl10_3 | ~spl10_12)),
% 68.26/10.00 inference(constrained_superposition,[],[f277,f2329])).
% 68.26/10.00 thf(f41308,plain,(
% 68.26/10.00 ($false = ((i @ sK4 @ sK2))) | (~spl10_3 | ~spl10_12)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f41207])).
% 68.26/10.00 thf(f41344,plain,(
% 68.26/10.00 ($true = $false) | (~spl10_2 | ~spl10_3 | ~spl10_12)),
% 68.26/10.00 inference(constrained_superposition,[],[f41308,f272])).
% 68.26/10.00 thf(f41424,plain,(
% 68.26/10.00 $false | (~spl10_2 | ~spl10_3 | ~spl10_12)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f41344])).
% 68.26/10.00 thf(f41425,plain,(
% 68.26/10.00 ~spl10_2 | ~spl10_3 | ~spl10_12),
% 68.26/10.00 inference(avatar_contradiction_clause,[],[f41424])).
% 68.26/10.00 thf(f41475,plain,(
% 68.26/10.00 spl10_1 | spl10_5),
% 68.26/10.00 inference(avatar_split_clause,[],[f177,f285,f266])).
% 68.26/10.00 thf(f41634,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($true = ((sK3 @ (sK9 @ sK5 @ X0)))) | ($false = ((k @ X1 @ X0))) | ($false = ((i @ X1 @ sK5)))) ) | (~spl10_6 | ~spl10_10)),
% 68.26/10.00 inference(constrained_superposition,[],[f290,f968])).
% 68.26/10.00 thf(f41665,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = ((sK3 @ (sK9 @ sK5 @ X0)))) | ($false = ((k @ X1 @ X0))) | ($false = ((i @ X1 @ sK5)))) ) | (~spl10_6 | ~spl10_10)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f41634])).
% 68.26/10.00 thf(f42254,plain,(
% 68.26/10.00 spl10_36 | ~spl10_34),
% 68.26/10.00 inference(avatar_split_clause,[],[f31351,f31348,f40146])).
% 68.26/10.00 thf(f44705,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X2))) | ((((^[Y0 : $i]: (Y0)) @ (sK7 @ (^[Y0 : $i]: (j @ sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) != X0)) ) | ~spl10_21),
% 68.26/10.00 inference(equality_resolution,[],[f7325])).
% 68.26/10.00 thf(f44706,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((l @ sK0 @ X0))) | ($false = ((i @ X1 @ sK2))) | ($false = ((k @ X1 @ X2))) | (((sK7 @ (j @ sK2) @ X2)) != X0)) ) | ~spl10_21),
% 68.26/10.00 inference(beta-eta_normalization,[],[f44705])).
% 68.26/10.00 thf(f44708,plain,(
% 68.26/10.00 spl10_20 | ~spl10_21),
% 68.26/10.00 inference(avatar_split_clause,[],[f44706,f7324,f7321])).
% 68.26/10.00 thf(f44858,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((l @ sK6 @ X1))) | ($false = ((sK3 @ X1)))) ) | spl10_2),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f198,f271])).
% 68.26/10.00 thf(f44885,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_2 | ~spl10_9)),
% 68.26/10.00 inference(constrained_superposition,[],[f894,f44858])).
% 68.26/10.00 thf(f44896,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_2 | ~spl10_9)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f44885])).
% 68.26/10.00 thf(f45087,plain,(
% 68.26/10.00 spl10_12 | spl10_12 | ~spl10_20 | ~spl10_36),
% 68.26/10.00 inference(avatar_split_clause,[],[f40372,f40146,f7321,f2328,f2328])).
% 68.26/10.00 thf(f45640,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((k @ X2 @ X1))) | ($false = ((i @ X2 @ sK5))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0)))) | ($false != ((X0 @ (sK7 @ X0 @ X1))))) ) | (~spl10_6 | ~spl10_11)),
% 68.26/10.00 inference(equality_factoring,[],[f41155])).
% 68.26/10.00 thf(f45978,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($false != ((X0 @ (sK7 @ X0 @ X1)))) | ($false = ((k @ X2 @ X1))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0)))) | ($false = ((i @ X2 @ sK5)))) ) | (~spl10_6 | ~spl10_11)),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f45640,f125])).
% 68.26/10.00 thf(f47486,plain,(
% 68.26/10.00 ( ! [X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (spl10_2 | ~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(constrained_superposition,[],[f44858,f41156])).
% 68.26/10.00 thf(f47600,plain,(
% 68.26/10.00 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (spl10_2 | ~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f47486])).
% 68.26/10.00 thf(f47673,definition,(
% 68.26/10.00 spl10_51 <=> ! [X1 : $i] : (($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_51])],[avatar_definition])).
% 68.26/10.00 thf(f47674,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | ~spl10_51),
% 68.26/10.00 inference(avatar_component_clause,[],[f47673])).
% 68.26/10.00 thf(f47676,definition,(
% 68.26/10.00 spl10_52 <=> ! [X0 : ($i > $o)] : (($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0)))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_52])],[avatar_definition])).
% 68.26/10.00 thf(f47677,plain,(
% 68.26/10.00 ( ! [X0 : ($i > $o)] : (($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | ~spl10_52),
% 68.26/10.00 inference(avatar_component_clause,[],[f47676])).
% 68.26/10.00 thf(f47678,plain,(
% 68.26/10.00 spl10_51 | spl10_52 | spl10_2 | ~spl10_6 | ~spl10_19),
% 68.26/10.00 inference(avatar_split_clause,[],[f47600,f5245,f289,f270,f47676,f47673])).
% 68.26/10.00 thf(f47699,plain,(
% 68.26/10.00 ($true = $false) | ($false = ((i @ sK1 @ sK5))) | (~spl10_4 | ~spl10_51)),
% 68.26/10.00 inference(constrained_superposition,[],[f282,f47674])).
% 68.26/10.00 thf(f47700,plain,(
% 68.26/10.00 ($false = ((i @ sK1 @ sK5))) | (~spl10_4 | ~spl10_51)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f47699])).
% 68.26/10.00 thf(f47736,plain,(
% 68.26/10.00 ($true = $false) | (~spl10_1 | ~spl10_4 | ~spl10_51)),
% 68.26/10.00 inference(constrained_superposition,[],[f47700,f268])).
% 68.26/10.00 thf(f47793,plain,(
% 68.26/10.00 $false | (~spl10_1 | ~spl10_4 | ~spl10_51)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f47736])).
% 68.26/10.00 thf(f47794,plain,(
% 68.26/10.00 ~spl10_1 | ~spl10_4 | ~spl10_51),
% 68.26/10.00 inference(avatar_contradiction_clause,[],[f47793])).
% 68.26/10.00 thf(f47848,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($true = $false) | ($false = ((i @ X2 @ X0))) | ($false = ((k @ X2 @ sK6))) | ($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | ($false = ((sK3 @ (sK7 @ X1 @ sK6)))) | (sK5 != X0) | (sK3 != X1)) ) | (spl10_2 | ~spl10_9 | ~spl10_52)),
% 68.26/10.00 inference(constrained_superposition,[],[f44896,f47677])).
% 68.26/10.00 thf(f47856,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((i @ X2 @ X0))) | ($false = ((k @ X2 @ sK6))) | ($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | ($false = ((sK3 @ (sK7 @ X1 @ sK6)))) | (sK5 != X0) | (sK3 != X1)) ) | (spl10_2 | ~spl10_9 | ~spl10_52)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f47848])).
% 68.26/10.00 thf(f47857,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((i @ X2 @ X0))) | ($false = ((k @ X2 @ sK6))) | ($false = ((sK3 @ (sK7 @ sK3 @ sK6)))) | ($false = ((sK3 @ (sK7 @ X1 @ sK6)))) | (sK5 != X0) | (sK3 != X1)) ) | (spl10_2 | ~spl10_9 | ~spl10_52)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f47856])).
% 68.26/10.00 thf(f48220,definition,(
% 68.26/10.00 spl10_53 <=> ! [X1 : ($i > $o)] : (($false = ((sK3 @ (sK7 @ X1 @ sK6)))) | (sK3 != X1))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_53])],[avatar_definition])).
% 68.26/10.00 thf(f48221,plain,(
% 68.26/10.00 ( ! [X1 : ($i > $o)] : ((sK3 != X1) | ($false = ((sK3 @ (sK7 @ X1 @ sK6))))) ) | ~spl10_53),
% 68.26/10.00 inference(avatar_component_clause,[],[f48220])).
% 68.26/10.00 thf(f48223,definition,(
% 68.26/10.00 spl10_54 <=> ($false = ((sK3 @ (sK7 @ sK3 @ sK6))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_54])],[avatar_definition])).
% 68.26/10.00 thf(f48224,plain,(
% 68.26/10.00 ($false != ((sK3 @ (sK7 @ sK3 @ sK6)))) | spl10_54),
% 68.26/10.00 inference(avatar_component_clause,[],[f48223])).
% 68.26/10.00 thf(f48225,plain,(
% 68.26/10.00 ($false = ((sK3 @ (sK7 @ sK3 @ sK6)))) | ~spl10_54),
% 68.26/10.00 inference(avatar_component_clause,[],[f48223])).
% 68.26/10.00 thf(f48227,definition,(
% 68.26/10.00 spl10_55 <=> ! [X2 : $i,X0 : $i] : (($false = ((i @ X2 @ X0))) | (sK5 != X0) | ($false = ((k @ X2 @ sK6))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_55])],[avatar_definition])).
% 68.26/10.00 thf(f48228,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i] : ((sK5 != X0) | ($false = ((i @ X2 @ X0))) | ($false = ((k @ X2 @ sK6)))) ) | ~spl10_55),
% 68.26/10.00 inference(avatar_component_clause,[],[f48227])).
% 68.26/10.00 thf(f48229,plain,(
% 68.26/10.00 spl10_53 | spl10_54 | spl10_55 | spl10_2 | ~spl10_9 | ~spl10_52),
% 68.26/10.00 inference(avatar_split_clause,[],[f47857,f47676,f893,f270,f48227,f48223,f48220])).
% 68.26/10.00 thf(f48231,plain,(
% 68.26/10.00 ($false = ((sK3 @ (sK7 @ sK3 @ sK6)))) | ~spl10_53),
% 68.26/10.00 inference(equality_resolution,[],[f48221])).
% 68.26/10.00 thf(f48234,plain,(
% 68.26/10.00 spl10_54 | ~spl10_53),
% 68.26/10.00 inference(avatar_split_clause,[],[f48231,f48220,f48223])).
% 68.26/10.00 thf(f48235,plain,(
% 68.26/10.00 ( ! [X0 : $i] : (($false = ((i @ X0 @ sK5))) | ($false = ((k @ X0 @ sK6)))) ) | ~spl10_55),
% 68.26/10.00 inference(equality_resolution,[],[f48228])).
% 68.26/10.00 thf(f48236,plain,(
% 68.26/10.00 spl10_51 | ~spl10_55),
% 68.26/10.00 inference(avatar_split_clause,[],[f48235,f48227,f47673])).
% 68.26/10.00 thf(f48261,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false != $false) | ($false = ((k @ X1 @ X0))) | ($true = ((sK3 @ (sK8 @ sK5 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($false = ((i @ X1 @ sK5))) | (sK6 != X0)) ) | (~spl10_6 | ~spl10_11 | ~spl10_54)),
% 68.26/10.00 inference(constrained_superposition,[],[f45978,f48225])).
% 68.26/10.00 thf(f48277,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X1 @ X0))) | ($true = ((sK3 @ (sK8 @ sK5 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($false = ((i @ X1 @ sK5))) | (sK6 != X0)) ) | (~spl10_6 | ~spl10_11 | ~spl10_54)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f48261])).
% 68.26/10.00 thf(f48278,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X1 @ X0))) | ($true = ((sK3 @ (sK8 @ sK5 @ sK3)))) | ($false = ((i @ X1 @ sK5))) | (sK6 != X0)) ) | (~spl10_6 | ~spl10_11 | ~spl10_54)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f48277])).
% 68.26/10.00 thf(f48327,definition,(
% 68.26/10.00 spl10_56 <=> ($true = ((sK3 @ (sK8 @ sK5 @ sK3))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_56])],[avatar_definition])).
% 68.26/10.00 thf(f48329,plain,(
% 68.26/10.00 ($true = ((sK3 @ (sK8 @ sK5 @ sK3)))) | ~spl10_56),
% 68.26/10.00 inference(avatar_component_clause,[],[f48327])).
% 68.26/10.00 thf(f48331,definition,(
% 68.26/10.00 spl10_57 <=> ! [X0 : $i,X1 : $i] : (($false = ((k @ X1 @ X0))) | (sK6 != X0) | ($false = ((i @ X1 @ sK5))))),
% 68.26/10.00 introduced(definition,[new_symbols(definition,[spl10_57])],[avatar_definition])).
% 68.26/10.00 thf(f48332,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : ((sK6 != X0) | ($false = ((k @ X1 @ X0))) | ($false = ((i @ X1 @ sK5)))) ) | ~spl10_57),
% 68.26/10.00 inference(avatar_component_clause,[],[f48331])).
% 68.26/10.00 thf(f48333,plain,(
% 68.26/10.00 spl10_56 | spl10_57 | ~spl10_6 | ~spl10_11 | ~spl10_54),
% 68.26/10.00 inference(avatar_split_clause,[],[f48278,f48223,f2111,f289,f48331,f48327])).
% 68.26/10.00 thf(f48334,plain,(
% 68.26/10.00 ( ! [X0 : $i] : (($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5)))) ) | ~spl10_57),
% 68.26/10.00 inference(equality_resolution,[],[f48332])).
% 68.26/10.00 thf(f48335,plain,(
% 68.26/10.00 spl10_51 | ~spl10_57),
% 68.26/10.00 inference(avatar_split_clause,[],[f48334,f48331,f47673])).
% 68.26/10.00 thf(f48351,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ X2))) | ($true = (((^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2)))) | (sK5 != X0)) ) | (~spl10_7 | ~spl10_56)),
% 68.26/10.00 inference(constrained_superposition,[],[f450,f48329])).
% 68.26/10.00 thf(f48375,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ X2))) | ($true = (((^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2)))) | (sK5 != X0)) ) | (~spl10_7 | ~spl10_56)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f48351])).
% 68.26/10.00 thf(f48376,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((sK5 != X0) | ($false = ((k @ X1 @ X2))) | ($true = ((sK3 @ (sK7 @ sK3 @ X2)))) | ($false = ((i @ X1 @ X0)))) ) | (~spl10_7 | ~spl10_56)),
% 68.26/10.00 inference(beta-eta_normalization,[],[f48375])).
% 68.26/10.00 thf(f48403,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ X1))) | ($true = ((sK3 @ (sK7 @ sK3 @ X1)))) | ($false = ((i @ X0 @ sK5)))) ) | (~spl10_7 | ~spl10_56)),
% 68.26/10.00 inference(equality_resolution,[],[f48376])).
% 68.26/10.00 thf(f48450,plain,(
% 68.26/10.00 ( ! [X0 : $i] : (($true = $false) | ($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5)))) ) | (~spl10_7 | ~spl10_54 | ~spl10_56)),
% 68.26/10.00 inference(constrained_superposition,[],[f48225,f48403])).
% 68.26/10.00 thf(f48487,plain,(
% 68.26/10.00 ( ! [X0 : $i] : (($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5)))) ) | (~spl10_7 | ~spl10_54 | ~spl10_56)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f48450])).
% 68.26/10.00 thf(f48555,plain,(
% 68.26/10.00 spl10_51 | ~spl10_7 | ~spl10_54 | ~spl10_56),
% 68.26/10.00 inference(avatar_split_clause,[],[f48487,f48327,f48223,f304,f47673])).
% 68.26/10.00 thf(f48556,plain,(
% 68.26/10.00 $false | (spl10_2 | spl10_4)),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f40980,f271])).
% 68.26/10.00 thf(f48557,plain,(
% 68.26/10.00 spl10_2 | spl10_4),
% 68.26/10.00 inference(avatar_contradiction_clause,[],[f48556])).
% 68.26/10.00 thf(f48696,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK3 @ (sK9 @ X0 @ sK6)))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0)))) ) | (spl10_2 | ~spl10_8)),
% 68.26/10.00 inference(constrained_superposition,[],[f44858,f308])).
% 68.26/10.00 thf(f48697,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((sK3 @ (sK9 @ X0 @ sK6)))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0)))) ) | (spl10_2 | ~spl10_8)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f48696])).
% 68.26/10.00 thf(f48885,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (spl10_2 | ~spl10_6 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(constrained_superposition,[],[f41665,f48697])).
% 68.26/10.00 thf(f48935,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (spl10_2 | ~spl10_6 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f48885])).
% 68.26/10.00 thf(f49203,plain,(
% 68.26/10.00 spl10_51 | spl10_51 | spl10_2 | ~spl10_6 | ~spl10_8 | ~spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f48935,f967,f307,f289,f270,f47673,f47673])).
% 68.26/10.00 thf(f49303,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($false = ((l @ sK6 @ X1))) | ($false = ((sK3 @ X1)))) ) | spl10_3),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f207,f276])).
% 68.26/10.00 thf(f49327,plain,(
% 68.26/10.00 ( ! [X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(constrained_superposition,[],[f41156,f49303])).
% 68.26/10.00 thf(f49330,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_9)),
% 68.26/10.00 inference(constrained_superposition,[],[f894,f49303])).
% 68.26/10.00 thf(f49331,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0))) | ($false = ((sK3 @ (sK9 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_8)),
% 68.26/10.00 inference(constrained_superposition,[],[f308,f49303])).
% 68.26/10.00 thf(f49338,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0))) | ($false = ((sK3 @ (sK9 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_8)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f49331])).
% 68.26/10.00 thf(f49339,plain,(
% 68.26/10.00 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_9)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f49330])).
% 68.26/10.00 thf(f49342,plain,(
% 68.26/10.00 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0)))) | ($false = ((sK3 @ (sK7 @ X0 @ sK6))))) ) | (spl10_3 | ~spl10_6 | ~spl10_19)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f49327])).
% 68.26/10.00 thf(f49424,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (spl10_3 | ~spl10_6 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(constrained_superposition,[],[f41665,f49338])).
% 68.26/10.00 thf(f49425,plain,(
% 68.26/10.00 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (spl10_3 | ~spl10_6 | ~spl10_8 | ~spl10_10)),
% 68.26/10.00 inference(trivial_inequality_removal,[],[f49424])).
% 68.26/10.00 thf(f49498,plain,(
% 68.26/10.00 spl10_51 | spl10_51 | spl10_3 | ~spl10_6 | ~spl10_8 | ~spl10_10),
% 68.26/10.00 inference(avatar_split_clause,[],[f49425,f967,f307,f289,f275,f47673,f47673])).
% 68.26/10.00 thf(f49499,plain,(
% 68.26/10.00 ( ! [X1 : $i] : (($true = ((sK3 @ X1))) | ($false = ((j @ sK5 @ X1)))) ) | spl10_3),
% 68.26/10.00 inference(forward_subsumption_resolution,[],[f171,f276])).
% 68.26/10.00 thf(f49500,plain,(
% 68.26/10.00 spl10_6 | spl10_3),
% 68.26/10.01 inference(avatar_split_clause,[],[f49499,f275,f289])).
% 68.26/10.01 thf(f49592,plain,(
% 68.26/10.01 ($true = ((sK3 @ (sK8 @ sK5 @ sK3)))) | (~spl10_52 | spl10_54)),
% 68.26/10.01 inference(unit_resulting_resolution,[],[f47677,f48224])).
% 68.26/10.01 thf(f49698,plain,(
% 68.26/10.01 spl10_56 | ~spl10_52 | spl10_54),
% 68.26/10.01 inference(avatar_split_clause,[],[f49592,f48223,f47676,f48327])).
% 68.26/10.01 thf(f52845,plain,(
% 68.26/10.01 spl10_52 | spl10_51 | spl10_3 | ~spl10_6 | ~spl10_19),
% 68.26/10.01 inference(avatar_split_clause,[],[f49342,f5245,f289,f275,f47673,f47676])).
% 68.26/10.01 thf(f52872,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | ($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | (sK5 != X0)) ) | (spl10_3 | ~spl10_9 | ~spl10_56)),
% 68.26/10.01 inference(constrained_superposition,[],[f49339,f48329])).
% 68.26/10.01 thf(f52878,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | ($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | (sK5 != X0)) ) | (spl10_3 | ~spl10_9 | ~spl10_56)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f52872])).
% 68.26/10.01 thf(f52879,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | ($false = ((sK3 @ (sK7 @ sK3 @ sK6)))) | (sK5 != X0)) ) | (spl10_3 | ~spl10_9 | ~spl10_56)),
% 68.26/10.01 inference(beta-eta_normalization,[],[f52878])).
% 68.26/10.01 thf(f52918,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | (sK5 != X0)) ) | (spl10_3 | ~spl10_9 | spl10_54 | ~spl10_56)),
% 68.26/10.01 inference(forward_subsumption_resolution,[],[f52879,f48224])).
% 68.26/10.01 thf(f52920,plain,(
% 68.26/10.01 spl10_55 | spl10_3 | ~spl10_9 | spl10_54 | ~spl10_56),
% 68.26/10.01 inference(avatar_split_clause,[],[f52918,f48327,f48223,f893,f275,f48227])).
% 68.26/10.01 thf(f53075,definition,(
% 68.26/10.01 spl10_60 <=> ! [X2 : $i] : (($false = ((sK3 @ X2))) | ($false = ((l @ sK6 @ X2))))),
% 68.26/10.01 introduced(definition,[new_symbols(definition,[spl10_60])],[avatar_definition])).
% 68.26/10.01 thf(f53076,plain,(
% 68.26/10.01 ( ! [X2 : $i] : (($false = ((l @ sK6 @ X2))) | ($false = ((sK3 @ X2)))) ) | ~spl10_60),
% 68.26/10.01 inference(avatar_component_clause,[],[f53075])).
% 68.26/10.01 thf(f53077,plain,(
% 68.26/10.01 spl10_60 | spl10_5),
% 68.26/10.01 inference(avatar_split_clause,[],[f220,f285,f53075])).
% 68.26/10.01 thf(f53092,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0))) | ($false = ((sK3 @ (sK9 @ X0 @ sK6))))) ) | (~spl10_8 | ~spl10_60)),
% 68.26/10.01 inference(constrained_superposition,[],[f308,f53076])).
% 68.26/10.01 thf(f53093,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ X0))) | ($false = ((sK3 @ (sK9 @ X0 @ sK6))))) ) | (~spl10_8 | ~spl10_60)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f53092])).
% 68.26/10.01 thf(f53186,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (~spl10_6 | ~spl10_8 | ~spl10_10 | ~spl10_60)),
% 68.26/10.01 inference(constrained_superposition,[],[f41665,f53093])).
% 68.26/10.01 thf(f53187,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((k @ X0 @ sK6))) | ($false = ((i @ X0 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($false = ((i @ X1 @ sK5)))) ) | (~spl10_6 | ~spl10_8 | ~spl10_10 | ~spl10_60)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f53186])).
% 68.26/10.01 thf(f53328,plain,(
% 68.26/10.01 spl10_51 | spl10_51 | ~spl10_6 | ~spl10_8 | ~spl10_10 | ~spl10_60),
% 68.26/10.01 inference(avatar_split_clause,[],[f53187,f53075,f967,f307,f289,f47673,f47673])).
% 68.26/10.01 thf(f53847,plain,(
% 68.26/10.01 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0))))) ) | (~spl10_9 | ~spl10_60)),
% 68.26/10.01 inference(constrained_superposition,[],[f53076,f894])).
% 68.26/10.01 thf(f54031,plain,(
% 68.26/10.01 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ X2))) | ($false = ((k @ X1 @ sK6))) | ($false = ((X0 @ (sK8 @ X2 @ X0))))) ) | (~spl10_9 | ~spl10_60)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f53847])).
% 68.26/10.01 thf(f55070,plain,(
% 68.26/10.01 ( ! [X0 : ($i > $o),X1 : $i] : (($true = $false) | ($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_19 | ~spl10_60)),
% 68.26/10.01 inference(constrained_superposition,[],[f53076,f41156])).
% 68.26/10.01 thf(f55156,plain,(
% 68.26/10.01 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((sK3 @ (sK7 @ X0 @ sK6)))) | ($false = ((i @ X1 @ sK5))) | ($false = ((k @ X1 @ sK6))) | ($true = ((sK3 @ (sK8 @ sK5 @ X0))))) ) | (~spl10_6 | ~spl10_19 | ~spl10_60)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f55070])).
% 68.26/10.01 thf(f55220,plain,(
% 68.26/10.01 spl10_51 | spl10_52 | ~spl10_6 | ~spl10_19 | ~spl10_60),
% 68.26/10.01 inference(avatar_split_clause,[],[f55156,f53075,f5245,f289,f47676,f47673])).
% 68.26/10.01 thf(f55249,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | ($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | (sK5 != X0)) ) | (~spl10_9 | ~spl10_56 | ~spl10_60)),
% 68.26/10.01 inference(constrained_superposition,[],[f54031,f48329])).
% 68.26/10.01 thf(f55253,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((sK3 @ (sK7 @ (^[Y0 : $i]: (sK3 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ sK6)))) | ($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | (sK5 != X0)) ) | (~spl10_9 | ~spl10_56 | ~spl10_60)),
% 68.26/10.01 inference(trivial_inequality_removal,[],[f55249])).
% 68.26/10.01 thf(f55254,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((sK3 @ (sK7 @ sK3 @ sK6)))) | ($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | (sK5 != X0)) ) | (~spl10_9 | ~spl10_56 | ~spl10_60)),
% 68.26/10.01 inference(beta-eta_normalization,[],[f55253])).
% 68.26/10.01 thf(f55292,plain,(
% 68.26/10.01 ( ! [X0 : $i,X1 : $i] : (($false = ((i @ X1 @ X0))) | ($false = ((k @ X1 @ sK6))) | (sK5 != X0)) ) | (~spl10_9 | spl10_54 | ~spl10_56 | ~spl10_60)),
% 68.26/10.01 inference(forward_subsumption_resolution,[],[f55254,f48224])).
% 68.26/10.01 thf(f55294,plain,(
% 68.26/10.01 spl10_55 | ~spl10_9 | spl10_54 | ~spl10_56 | ~spl10_60),
% 68.26/10.01 inference(avatar_split_clause,[],[f55292,f53075,f48327,f48223,f893,f48227])).
% 68.26/10.01 cnf(s1, plain, spl10_1 | spl10_2, inference(sat_conversion,[],[f273])).
% 68.26/10.01 cnf(s2, plain, spl10_1 | spl10_3, inference(sat_conversion,[],[f278])).
% 68.26/10.01 cnf(s3, plain, spl10_3 | spl10_4, inference(sat_conversion,[],[f283])).
% 68.26/10.01 cnf(s4, plain, spl10_4 | spl10_5, inference(sat_conversion,[],[f287])).
% 68.26/10.01 cnf(s5, plain, spl10_5 | spl10_6, inference(sat_conversion,[],[f291])).
% 68.26/10.01 cnf(s6, plain, spl10_7 | spl10_8, inference(sat_conversion,[],[f309])).
% 68.26/10.01 cnf(s7, plain, spl10_8 | spl10_9, inference(sat_conversion,[],[f895])).
% 68.26/10.01 cnf(s8, plain, spl10_9 | spl10_10, inference(sat_conversion,[],[f969])).
% 68.26/10.01 cnf(s9, plain, spl10_10 | spl10_11, inference(sat_conversion,[],[f2113])).
% 68.26/10.01 cnf(s10, plain, spl10_12 | ~spl10_8 | ~spl10_10 | ~spl10_5 | spl10_12, inference(sat_conversion,[],[f2330])).
% 68.26/10.01 cnf(s11, plain, ~spl10_5 | ~spl10_8 | ~spl10_10 | spl10_12, inference(rat,[],[s10])).
% 68.26/10.01 cnf(s12, plain, spl10_8 | spl10_11, inference(sat_conversion,[],[f2331])).
% 68.26/10.01 cnf(s18, plain, spl10_8 | spl10_19, inference(sat_conversion,[],[f5247])).
% 68.26/10.01 cnf(s19, plain, spl10_10 | spl10_19, inference(sat_conversion,[],[f6203])).
% 68.26/10.01 cnf(s20, plain, ~spl10_5 | ~spl10_7 | ~spl10_11 | spl10_20 | spl10_21, inference(sat_conversion,[],[f7326])).
% 68.26/10.01 cnf(s24, plain, spl10_7 | spl10_10, inference(sat_conversion,[],[f9975])).
% 68.26/10.01 cnf(s25, plain, spl10_2 | spl10_6, inference(sat_conversion,[],[f10048])).
% 68.26/10.01 cnf(s27, plain, ~spl10_5 | ~spl10_9 | ~spl10_11 | spl10_28 | spl10_29, inference(sat_conversion,[],[f22792])).
% 68.26/10.01 cnf(s31, plain, ~spl10_9 | spl10_12 | ~spl10_28 | spl10_34, inference(sat_conversion,[],[f31350])).
% 68.26/10.01 cnf(s34, plain, spl10_12 | ~spl10_19 | ~spl10_29 | spl10_36, inference(sat_conversion,[],[f40148])).
% 68.26/10.01 cnf(s42, plain, ~spl10_2 | ~spl10_3 | ~spl10_12, inference(sat_conversion,[],[f41425])).
% 68.26/10.01 cnf(s44, plain, spl10_1 | spl10_5, inference(sat_conversion,[],[f41475])).
% 68.26/10.01 cnf(s50, plain, ~spl10_34 | spl10_36, inference(sat_conversion,[],[f42254])).
% 68.26/10.01 cnf(s51, plain, spl10_20 | ~spl10_21, inference(sat_conversion,[],[f44708])).
% 68.26/10.01 cnf(s55, plain, spl10_12 | spl10_12 | ~spl10_20 | ~spl10_36, inference(sat_conversion,[],[f45087])).
% 68.26/10.01 cnf(s56, plain, spl10_12 | ~spl10_20 | ~spl10_36, inference(rat,[],[s55])).
% 68.26/10.01 cnf(s66, plain, spl10_2 | ~spl10_6 | ~spl10_19 | spl10_51 | spl10_52, inference(sat_conversion,[],[f47678])).
% 68.26/10.01 cnf(s68, plain, ~spl10_1 | ~spl10_4 | ~spl10_51, inference(sat_conversion,[],[f47794])).
% 68.26/10.01 cnf(s69, plain, spl10_2 | ~spl10_9 | ~spl10_52 | spl10_53 | spl10_54 | spl10_55, inference(sat_conversion,[],[f48229])).
% 68.26/10.01 cnf(s70, plain, ~spl10_53 | spl10_54, inference(sat_conversion,[],[f48234])).
% 68.26/10.01 cnf(s71, plain, spl10_51 | ~spl10_55, inference(sat_conversion,[],[f48236])).
% 68.26/10.01 cnf(s72, plain, ~spl10_6 | ~spl10_11 | ~spl10_54 | spl10_56 | spl10_57, inference(sat_conversion,[],[f48333])).
% 68.26/10.01 cnf(s73, plain, spl10_51 | ~spl10_57, inference(sat_conversion,[],[f48335])).
% 68.26/10.01 cnf(s74, plain, ~spl10_7 | spl10_51 | ~spl10_54 | ~spl10_56, inference(sat_conversion,[],[f48555])).
% 68.26/10.01 cnf(s75, plain, spl10_2 | spl10_4, inference(sat_conversion,[],[f48557])).
% 68.26/10.01 cnf(s76, plain, spl10_51 | ~spl10_6 | ~spl10_8 | ~spl10_10 | spl10_2 | spl10_51, inference(sat_conversion,[],[f49203])).
% 68.26/10.01 cnf(s77, plain, spl10_2 | ~spl10_6 | ~spl10_8 | ~spl10_10 | spl10_51, inference(rat,[],[s76])).
% 68.26/10.01 cnf(s78, plain, spl10_51 | ~spl10_6 | ~spl10_8 | ~spl10_10 | spl10_3 | spl10_51, inference(sat_conversion,[],[f49498])).
% 68.26/10.01 cnf(s79, plain, spl10_3 | ~spl10_6 | ~spl10_8 | ~spl10_10 | spl10_51, inference(rat,[],[s78])).
% 68.26/10.01 cnf(s80, plain, spl10_3 | spl10_6, inference(sat_conversion,[],[f49500])).
% 68.26/10.01 cnf(s81, plain, ~spl10_52 | spl10_54 | spl10_56, inference(sat_conversion,[],[f49698])).
% 68.26/10.01 cnf(s84, plain, spl10_3 | ~spl10_6 | ~spl10_19 | spl10_51 | spl10_52, inference(sat_conversion,[],[f52845])).
% 68.26/10.01 cnf(s85, plain, spl10_3 | ~spl10_9 | spl10_54 | spl10_55 | ~spl10_56, inference(sat_conversion,[],[f52920])).
% 68.26/10.01 cnf(s86, plain, spl10_5 | spl10_60, inference(sat_conversion,[],[f53077])).
% 68.26/10.01 cnf(s87, plain, spl10_51 | ~spl10_8 | ~spl10_10 | ~spl10_6 | spl10_51 | ~spl10_60, inference(sat_conversion,[],[f53328])).
% 68.26/10.01 cnf(s88, plain, ~spl10_6 | ~spl10_8 | ~spl10_10 | spl10_51 | ~spl10_60, inference(rat,[],[s87])).
% 68.26/10.01 cnf(s89, plain, ~spl10_6 | ~spl10_19 | spl10_51 | spl10_52 | ~spl10_60, inference(sat_conversion,[],[f55220])).
% 68.26/10.01 cnf(s90, plain, ~spl10_9 | spl10_54 | spl10_55 | ~spl10_56 | ~spl10_60, inference(sat_conversion,[],[f55294])).
% 68.26/10.01 cnf(s91, plain, spl10_7 | spl10_1, inference(rat,[],[s11,s6,s24,s44,s42,s1,s2])).
% 68.26/10.01 cnf(s92, plain, spl10_20 | ~spl10_11 | spl10_1, inference(rat,[],[s20,s51,s44,s91])).
% 68.26/10.01 cnf(s93, plain, spl10_10 | spl10_1, inference(rat,[],[s27,s31,s34,s50,s56,s92,s8,s9,s19,s44,s42,s1,s2])).
% 68.26/10.01 cnf(s94, plain, spl10_1, inference(rat,[],[s27,s31,s34,s50,s56,s92,s7,s12,s18,s11,s93,s42,s1,s2,s44])).
% 68.26/10.01 cnf(s95, plain, spl10_20 | spl10_10 | ~spl10_5, inference(rat,[],[s20,s51,s24,s9])).
% 68.26/10.01 cnf(s96, plain, spl10_12 | spl10_10 | ~spl10_5, inference(rat,[],[s27,s31,s34,s50,s56,s19,s9,s8,s95])).
% 68.26/10.01 cnf(s97, plain, spl10_54 | ~spl10_52 | spl10_3 | ~spl10_9, inference(rat,[],[s85,s81,s71,s68,s3,s94])).
% 68.26/10.01 cnf(s98, plain, spl10_3 | spl10_10, inference(rat,[],[s72,s74,s97,s84,s73,s68,s3,s80,s24,s19,s9,s8,s94])).
% 68.26/10.01 cnf(s99, plain, spl10_54 | ~spl10_52 | spl10_2 | ~spl10_9, inference(rat,[],[s69,s70,s71,s68,s75,s94])).
% 68.26/10.01 cnf(s100, plain, spl10_10 | ~spl10_5, inference(rat,[],[s72,s74,s99,s66,s73,s68,s25,s75,s42,s98,s96,s8,s9,s19,s24,s94])).
% 68.26/10.01 cnf(s101, plain, spl10_3 | ~spl10_8 | ~spl10_10, inference(rat,[],[s68,s79,s3,s80,s94])).
% 68.26/10.01 cnf(s102, plain, ~spl10_10 | ~spl10_8 | ~spl10_5, inference(rat,[],[s77,s68,s25,s75,s42,s101,s11,s94])).
% 68.26/10.01 cnf(s103, plain, spl10_3 | spl10_8, inference(rat,[],[s72,s74,s97,s84,s73,s68,s3,s80,s18,s12,s7,s6,s94])).
% 68.26/10.01 cnf(s104, plain, spl10_2 | spl10_8, inference(rat,[],[s72,s74,s99,s66,s73,s68,s25,s75,s18,s12,s7,s6,s94])).
% 68.26/10.01 cnf(s105, plain, spl10_36 | ~spl10_5, inference(rat,[],[s27,s31,s34,s50,s18,s12,s7,s42,s104,s103,s102,s100])).
% 68.26/10.01 cnf(s106, plain, ~spl10_10 | ~spl10_5, inference(rat,[],[s20,s51,s56,s105,s42,s104,s103,s6,s12,s102])).
% 68.26/10.01 cnf(s107, plain, ~spl10_5, inference(rat,[],[s106,s100])).
% 68.26/10.01 cnf(s108, plain, spl10_60, inference(rat,[],[s86,s107])).
% 68.26/10.01 cnf(s109, plain, spl10_6, inference(rat,[],[s5,s107])).
% 68.26/10.01 cnf(s110, plain, spl10_4, inference(rat,[],[s4,s107])).
% 68.26/10.01 cnf(s111, plain, ~spl10_51, inference(rat,[],[s68,s94,s110])).
% 68.26/10.01 cnf(s115, plain, ~spl10_57, inference(rat,[],[s73,s111])).
% 68.26/10.01 cnf(s116, plain, ~spl10_55, inference(rat,[],[s71,s111])).
% 68.26/10.01 cnf(s119, plain, spl10_54 | spl10_10, inference(rat,[],[s90,s81,s8,s89,s19,s116,s108,s109,s111])).
% 68.26/10.01 cnf(s120, plain, spl10_10, inference(rat,[],[s72,s74,s119,s9,s24,s109,s115,s111])).
% 68.26/10.01 cnf(s121, plain, ~spl10_8, inference(rat,[],[s88,s109,s108,s111,s120])).
% 68.26/10.01 cnf(s122, plain, spl10_19, inference(rat,[],[s18,s121])).
% 68.26/10.01 cnf(s123, plain, spl10_11, inference(rat,[],[s12,s121])).
% 68.26/10.01 cnf(s124, plain, spl10_9, inference(rat,[],[s7,s121])).
% 68.26/10.01 cnf(s125, plain, spl10_7, inference(rat,[],[s6,s121])).
% 68.26/10.01 cnf(s128, plain, spl10_52, inference(rat,[],[s89,s108,s109,s111,s122])).
% 68.26/10.01 cnf(s134, plain, spl10_54, inference(rat,[],[s90,s81,s116,s124,s108,s128])).
% 68.26/10.01 cnf(s135, plain, ~spl10_56, inference(rat,[],[s74,s111,s125,s134])).
% 68.26/10.01 cnf(s136, plain, $false, inference(rat,[],[s72,s115,s123,s109,s134,s135])).
% 68.26/10.01 thf(f55295,plain,(
% 68.26/10.01 $false),
% 68.26/10.01 inference(avatar_sat_refutation,[],[s136])).
% 68.26/10.01 % SZS output end Proof for theBenchmark
% 68.26/10.01 % (403336)------------------------------
% 68.26/10.01 % (403336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.26/10.01 % (403336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/10.01 % (403336)CaDiCaL version: 2.1.3
% 68.26/10.01 % (403336)Termination reason: Refutation
% 68.26/10.01 % (403336)Time elapsed: 7.124 s
% 68.26/10.01 % (403336)Peak memory usage: 30 MB
% 68.26/10.01 % (403336)Instructions burned: 12497 (million)
% 68.26/10.01 % (403264)Success in time 9.787 s
% 68.26/10.01 % Vampire exiting
%------------------------------------------------------------------------------