%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO063^4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:51 AM UTC 2026
% Result : Theorem 138.11s 19.77s
% Output : Refutation 138.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO063^4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n011.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 16:26:31 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 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
% 4.21/0.94 % (297157)Will run a generic schedule for satisfiability detection.
% 4.21/0.94 % (297167)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3054463033:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.21/0.94 % (297163)% WARNING: option uhcvi not known.
% 4.21/0.94 % (297164)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1053468867:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.21/0.94 % (297162)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1939432050_2999 on theBenchmark for (2999ds/0Mi)
% 4.21/0.94 % (297163)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2698583830:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.21/0.94 % (297165)dis+10_1_sil=32000:sp=arity:random_seed=1815336228:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.21/0.94 % (297166)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3228568510:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.21/0.94 % (297168)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=929746585:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.21/0.94 % (297163)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.94 % (297166)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.94 % Exception at run slice level
% 4.21/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.21/0.94 % (297163)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.21/0.94 % (297176)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2223543863:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.21/0.94 % Exception at run slice level
% 4.21/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.21/0.94 % (297167)Instruction limit reached!
% 4.21/0.94 % (297167)------------------------------
% 4.21/0.94 % (297167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.94 % (297167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.94 % (297167)CaDiCaL version: 2.1.3
% 4.21/0.94 % (297167)Termination reason: Instruction limit
% 4.21/0.94 % (297167)Termination phase: Saturation
% 4.21/0.94 % (297167)Time elapsed: 0.035 s
% 4.21/0.94 % (297167)Peak memory usage: 12 MB
% 4.21/0.94 % (297167)Instructions burned: 133 (million)
% 4.21/0.94 % (297179)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=1218349333:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.21/0.94 % (297179)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.94 % (297179)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.21/0.94 % (297178)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3652553789:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.21/0.94 % (297165)Instruction limit reached!
% 4.21/0.94 % (297165)------------------------------
% 4.21/0.94 % (297165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.94 % (297165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.94 % (297165)CaDiCaL version: 2.1.3
% 4.21/0.94 % (297165)Termination reason: Instruction limit
% 4.21/0.94 % (297165)Termination phase: Saturation
% 4.21/0.94 % (297165)Time elapsed: 0.051 s
% 4.21/0.94 % (297165)Peak memory usage: 12 MB
% 4.21/0.94 % (297165)Instructions burned: 105 (million)
% 4.21/0.94 % (297166)Instruction limit reached!
% 4.21/0.94 % (297166)------------------------------
% 4.21/0.94 % (297166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.94 % (297166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.94 % (297166)CaDiCaL version: 2.1.3
% 4.21/0.94 % (297166)Termination reason: Instruction limit
% 4.21/0.94 % (297166)Termination phase: Saturation
% 4.21/0.94 % (297166)Time elapsed: 0.056 s
% 4.21/0.94 % (297166)Peak memory usage: 12 MB
% 4.21/0.94 % (297166)Instructions burned: 119 (million)
% 4.21/0.94 % (297182)ott-21_1_sil=16000:fs=off:random_seed=1239175054:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.21/0.94 % (297183)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1671795125:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 16.75/2.72 % (297168)Instruction limit reached!
% 16.75/2.72 % (297168)------------------------------
% 16.75/2.72 % (297168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/2.72 % (297168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/2.72 % (297168)CaDiCaL version: 2.1.3
% 16.75/2.72 % (297168)Termination reason: Instruction limit
% 16.75/2.72 % (297168)Termination phase: Saturation
% 16.75/2.72 % (297168)Time elapsed: 0.075 s
% 16.75/2.72 % (297168)Peak memory usage: 12 MB
% 16.75/2.72 % (297168)Instructions burned: 159 (million)
% 16.75/2.72 % (297186)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3234104703:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 16.75/2.72 % Exception at run slice level
% 16.75/2.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.75/2.72 % (297178)Instruction limit reached!
% 16.75/2.72 % (297178)------------------------------
% 16.75/2.72 % (297178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/2.72 % (297178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/2.72 % (297178)CaDiCaL version: 2.1.3
% 16.75/2.72 % (297178)Termination reason: Instruction limit
% 16.75/2.72 % (297178)Termination phase: Saturation
% 16.75/2.72 % (297178)Time elapsed: 0.062 s
% 16.75/2.72 % (297178)Peak memory usage: 12 MB
% 16.75/2.72 % (297178)Instructions burned: 132 (million)
% 16.75/2.72 % (297188)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2488548603:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 16.75/2.72 % (297189)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3030368809:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 16.75/2.72 % Exception at run slice level
% 16.75/2.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.75/2.72 % (297192)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=3621223078: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)
% 16.75/2.72 % (297192)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.75/2.72 % (297182)Instruction limit reached!
% 16.75/2.72 % (297182)------------------------------
% 16.75/2.72 % (297182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/2.72 % (297182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/2.72 % (297182)CaDiCaL version: 2.1.3
% 16.75/2.72 % (297182)Termination reason: Instruction limit
% 16.75/2.72 % (297182)Termination phase: Saturation
% 16.75/2.72 % (297182)Time elapsed: 0.083 s
% 16.75/2.72 % (297182)Peak memory usage: 12 MB
% 16.75/2.72 % (297182)Instructions burned: 181 (million)
% 16.75/2.72 % (297194)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3876098579:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 16.75/2.72 % (297194)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.75/2.72 % (297179)Instruction limit reached!
% 16.75/2.72 % (297179)------------------------------
% 16.75/2.72 % (297179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/2.72 % (297179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/2.72 % (297179)CaDiCaL version: 2.1.3
% 16.75/2.72 % (297179)Termination reason: Instruction limit
% 16.75/2.72 % (297179)Termination phase: Saturation
% 16.75/2.72 % (297179)Time elapsed: 0.167 s
% 16.75/2.72 % (297179)Peak memory usage: 16 MB
% 16.75/2.72 % (297179)Instructions burned: 686 (million)
% 16.75/2.72 % (297196)fmb+10_1_sil=64000:random_seed=732943115:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 16.75/2.72 % (297196)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.75/2.72 % Exception at run slice level
% 16.75/2.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.75/2.72 % (297198)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=876697298:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 16.75/2.72 % Exception at run slice level
% 16.75/2.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.75/2.72 % (297200)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=340389288:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 43.01/6.34 % Exception at run slice level
% 43.01/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.01/6.34 % (297202)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=116022598:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 43.01/6.34 % (297202)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 43.01/6.34 % (297183)Instruction limit reached!
% 43.01/6.34 % (297183)------------------------------
% 43.01/6.34 % (297183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.01/6.34 % (297183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.01/6.34 % (297183)CaDiCaL version: 2.1.3
% 43.01/6.34 % (297183)Termination reason: Instruction limit
% 43.01/6.34 % (297183)Termination phase: Saturation
% 43.01/6.34 % (297183)Time elapsed: 0.237 s
% 43.01/6.34 % (297183)Peak memory usage: 14 MB
% 43.01/6.34 % (297183)Instructions burned: 477 (million)
% 43.01/6.34 % (297204)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2096711345:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 43.01/6.34 % (297204)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 43.01/6.34 % (297204)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 43.01/6.34 % (297192)Instruction limit reached!
% 43.01/6.34 % (297192)------------------------------
% 43.01/6.34 % (297192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.01/6.34 % (297192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.01/6.34 % (297192)CaDiCaL version: 2.1.3
% 43.01/6.34 % (297192)Termination reason: Instruction limit
% 43.01/6.34 % (297192)Termination phase: Saturation
% 43.01/6.34 % (297192)Time elapsed: 0.291 s
% 43.01/6.34 % (297192)Peak memory usage: 14 MB
% 43.01/6.34 % (297192)Instructions burned: 692 (million)
% 43.01/6.34 % (297206)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4084269007:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 43.01/6.34 % Exception at run slice level
% 43.01/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.01/6.34 % (297208)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3950205094:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 43.01/6.34 % Exception at run slice level
% 43.01/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.01/6.34 % (297210)ott-2_1_sil=16000:newcnf=on:random_seed=1367454367:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 43.01/6.34 % (297210)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 43.01/6.34 % (297194)Instruction limit reached!
% 43.01/6.34 % (297194)------------------------------
% 43.01/6.34 % (297194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.01/6.34 % (297194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.01/6.34 % (297194)CaDiCaL version: 2.1.3
% 43.01/6.34 % (297194)Termination reason: Instruction limit
% 43.01/6.34 % (297194)Termination phase: Saturation
% 43.01/6.34 % (297194)Time elapsed: 0.400 s
% 43.01/6.34 % (297194)Peak memory usage: 15 MB
% 43.01/6.34 % (297194)Instructions burned: 879 (million)
% 43.01/6.34 % (297212)ott+10_1_sil=32000:tgt=ground:random_seed=43345141:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 43.01/6.34 % (297188)Instruction limit reached!
% 43.01/6.34 % (297188)------------------------------
% 43.01/6.34 % (297188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.01/6.34 % (297188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.01/6.34 % (297188)CaDiCaL version: 2.1.3
% 43.01/6.34 % (297188)Termination reason: Instruction limit
% 43.01/6.34 % (297188)Termination phase: Saturation
% 43.01/6.34 % (297188)Time elapsed: 0.507 s
% 43.01/6.34 % (297188)Peak memory usage: 13 MB
% 43.01/6.34 % (297188)Instructions burned: 1180 (million)
% 43.01/6.34 % (297214)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2528155148:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 43.01/6.34 % Exception at run slice level
% 43.01/6.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.01/6.34 % (297216)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1936235536:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 90.78/13.07 % (297216)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 90.78/13.07 % (297210)Instruction limit reached!
% 90.78/13.07 % (297210)------------------------------
% 90.78/13.07 % (297210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.78/13.07 % (297210)CaDiCaL version: 2.1.3
% 90.78/13.07 % (297210)Termination reason: Instruction limit
% 90.78/13.07 % (297210)Termination phase: Saturation
% 90.78/13.07 % (297210)Time elapsed: 0.398 s
% 90.78/13.07 % (297210)Peak memory usage: 15 MB
% 90.78/13.07 % (297210)Instructions burned: 871 (million)
% 90.78/13.07 % (297218)dis+21_1_sil=32000:sas=cadical:random_seed=3068581485:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 90.78/13.07 % (297204)Instruction limit reached!
% 90.78/13.07 % (297204)------------------------------
% 90.78/13.07 % (297204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.78/13.07 % (297204)CaDiCaL version: 2.1.3
% 90.78/13.07 % (297204)Termination reason: Instruction limit
% 90.78/13.07 % (297204)Termination phase: Saturation
% 90.78/13.07 % (297204)Time elapsed: 0.724 s
% 90.78/13.07 % (297204)Peak memory usage: 18 MB
% 90.78/13.07 % (297204)Instructions burned: 1472 (million)
% 90.78/13.07 % (297220)ott+11_1_sil=16000:gs=on:random_seed=3134175019:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 90.78/13.07 % (297220)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 90.78/13.07 % (297202)Instruction limit reached!
% 90.78/13.07 % (297202)------------------------------
% 90.78/13.07 % (297202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.78/13.07 % (297202)CaDiCaL version: 2.1.3
% 90.78/13.07 % (297202)Termination reason: Instruction limit
% 90.78/13.07 % (297202)Termination phase: Saturation
% 90.78/13.07 % (297202)Time elapsed: 1.134 s
% 90.78/13.07 % (297202)Peak memory usage: 18 MB
% 90.78/13.07 % (297202)Instructions burned: 5135 (million)
% 90.78/13.07 % (297222)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4168841645:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi)
% 90.78/13.07 % Exception at run slice level
% 90.78/13.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 90.78/13.07 % (297224)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=35474020:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi)
% 90.78/13.07 % (297220)Instruction limit reached!
% 90.78/13.07 % (297220)------------------------------
% 90.78/13.07 % (297220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.78/13.07 % (297220)CaDiCaL version: 2.1.3
% 90.78/13.07 % (297220)Termination reason: Instruction limit
% 90.78/13.07 % (297220)Termination phase: Saturation
% 90.78/13.07 % (297220)Time elapsed: 0.906 s
% 90.78/13.07 % (297220)Peak memory usage: 15 MB
% 90.78/13.07 % (297220)Instructions burned: 2251 (million)
% 90.78/13.07 % (297226)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3362242860:i=29340_2979 on theBenchmark for (2979ds/29340Mi)
% 90.78/13.07 % (297216)Instruction limit reached!
% 90.78/13.07 % (297216)------------------------------
% 90.78/13.07 % (297216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.78/13.07 % (297216)CaDiCaL version: 2.1.3
% 90.78/13.07 % (297216)Termination reason: Instruction limit
% 90.78/13.07 % (297216)Termination phase: Saturation
% 90.78/13.07 % (297216)Time elapsed: 1.478 s
% 90.78/13.07 % (297216)Peak memory usage: 17 MB
% 90.78/13.07 % (297216)Instructions burned: 3513 (million)
% 90.78/13.07 % (297228)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1381832450:i=5211_2978 on theBenchmark for (2978ds/5211Mi)
% 90.78/13.07 % (297224)Instruction limit reached!
% 90.78/13.07 % (297224)------------------------------
% 90.78/13.07 % (297224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.78/13.07 % (297224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.76 % (297224)CaDiCaL version: 2.1.3
% 138.11/19.76 % (297224)Termination reason: Instruction limit
% 138.11/19.76 % (297224)Termination phase: Saturation
% 138.11/19.76 % (297224)Time elapsed: 1.037 s
% 138.11/19.76 % (297224)Peak memory usage: 20 MB
% 138.11/19.76 % (297224)Instructions burned: 4594 (million)
% 138.11/19.76 % (297230)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2656646275:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi)
% 138.11/19.76 % Exception at run slice level
% 138.11/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.76 % (297232)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2654434818:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi)
% 138.11/19.76 % Exception at run slice level
% 138.11/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.76 % (297234)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2696760106:i=14071_2974 on theBenchmark for (2974ds/14071Mi)
% 138.11/19.76 % Exception at run slice level
% 138.11/19.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.76 % (297218)Instruction limit reached!
% 138.11/19.76 % (297218)------------------------------
% 138.11/19.76 % (297218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.76 % (297218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.76 % (297218)CaDiCaL version: 2.1.3
% 138.11/19.76 % (297218)Termination reason: Instruction limit
% 138.11/19.76 % (297218)Termination phase: Saturation
% 138.11/19.76 % (297218)Time elapsed: 1.567 s
% 138.11/19.76 % (297218)Peak memory usage: 16 MB
% 138.11/19.76 % (297218)Instructions burned: 3774 (million)
% 138.11/19.76 % (297236)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4206211055:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi)
% 138.11/19.76 % (297237)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2005540496:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi)
% 138.11/19.76 % (297212)Instruction limit reached!
% 138.11/19.76 % (297212)------------------------------
% 138.11/19.77 % (297212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297212)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297212)Termination reason: Instruction limit
% 138.11/19.77 % (297212)Termination phase: Saturation
% 138.11/19.77 % (297212)Time elapsed: 2.182 s
% 138.11/19.77 % (297212)Peak memory usage: 17 MB
% 138.11/19.77 % (297212)Instructions burned: 5114 (million)
% 138.11/19.77 % (297240)dis+10_16:1_sil=16000:random_seed=4112779200:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi)
% 138.11/19.77 % (297228)Instruction limit reached!
% 138.11/19.77 % (297228)------------------------------
% 138.11/19.77 % (297228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297228)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297228)Termination reason: Instruction limit
% 138.11/19.77 % (297228)Termination phase: Saturation
% 138.11/19.77 % (297228)Time elapsed: 2.308 s
% 138.11/19.77 % (297228)Peak memory usage: 33 MB
% 138.11/19.77 % (297228)Instructions burned: 5213 (million)
% 138.11/19.77 % (297242)ott-3_8_sil=64000:random_seed=3963612982:i=20139:bs=on_2954 on theBenchmark for (2954ds/20139Mi)
% 138.11/19.77 % (297237)Instruction limit reached!
% 138.11/19.77 % (297237)------------------------------
% 138.11/19.77 % (297237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297237)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297237)Termination reason: Instruction limit
% 138.11/19.77 % (297237)Termination phase: Saturation
% 138.11/19.77 % (297237)Time elapsed: 3.519 s
% 138.11/19.77 % (297237)Peak memory usage: 21 MB
% 138.11/19.77 % (297237)Instructions burned: 8174 (million)
% 138.11/19.77 % (297244)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3996877905:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297246)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=369704045:i=11404_2939 on theBenchmark for (2939ds/11404Mi)
% 138.11/19.77 % (297240)Instruction limit reached!
% 138.11/19.77 % (297240)------------------------------
% 138.11/19.77 % (297240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297240)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297240)Termination reason: Instruction limit
% 138.11/19.77 % (297240)Termination phase: Saturation
% 138.11/19.77 % (297240)Time elapsed: 3.865 s
% 138.11/19.77 % (297240)Peak memory usage: 25 MB
% 138.11/19.77 % (297240)Instructions burned: 9157 (million)
% 138.11/19.77 % (297248)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2023287409:i=14134_2932 on theBenchmark for (2932ds/14134Mi)
% 138.11/19.77 % (297248)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 138.11/19.77 % (297236)Instruction limit reached!
% 138.11/19.77 % (297236)------------------------------
% 138.11/19.77 % (297236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297236)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297236)Termination reason: Instruction limit
% 138.11/19.77 % (297236)Termination phase: Saturation
% 138.11/19.77 % (297236)Time elapsed: 5.100 s
% 138.11/19.77 % (297236)Peak memory usage: 57 MB
% 138.11/19.77 % (297236)Instructions burned: 22569 (million)
% 138.11/19.77 % (297250)dis+33_16_sil=32000:sac=on:random_seed=2875793546:i=15851:nm=0_2923 on theBenchmark for (2923ds/15851Mi)
% 138.11/19.77 % (297246)Instruction limit reached!
% 138.11/19.77 % (297246)------------------------------
% 138.11/19.77 % (297246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297246)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297246)Termination reason: Instruction limit
% 138.11/19.77 % (297246)Termination phase: Saturation
% 138.11/19.77 % (297246)Time elapsed: 5.015 s
% 138.11/19.77 % (297246)Peak memory usage: 24 MB
% 138.11/19.77 % (297246)Instructions burned: 11404 (million)
% 138.11/19.77 % (297252)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2849783209:avsq=on:i=17627:add=on:amm=off_2888 on theBenchmark for (2888ds/17627Mi)
% 138.11/19.77 % (297250)Instruction limit reached!
% 138.11/19.77 % (297250)------------------------------
% 138.11/19.77 % (297250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297250)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297250)Termination reason: Instruction limit
% 138.11/19.77 % (297250)Termination phase: Saturation
% 138.11/19.77 % (297250)Time elapsed: 3.574 s
% 138.11/19.77 % (297250)Peak memory usage: 34 MB
% 138.11/19.77 % (297250)Instructions burned: 15852 (million)
% 138.11/19.77 % (297254)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1850994072:s2a=on:i=53295_2887 on theBenchmark for (2887ds/53295Mi)
% 138.11/19.77 % (297242)Instruction limit reached!
% 138.11/19.77 % (297242)------------------------------
% 138.11/19.77 % (297242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297242)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297242)Termination reason: Instruction limit
% 138.11/19.77 % (297242)Termination phase: Saturation
% 138.11/19.77 % (297242)Time elapsed: 7.935 s
% 138.11/19.77 % (297242)Peak memory usage: 26 MB
% 138.11/19.77 % (297242)Instructions burned: 20139 (million)
% 138.11/19.77 % (297256)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1224376960:i=26857:ins=20_2875 on theBenchmark for (2875ds/26857Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297258)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1809518431:i=28120:bs=on:fsr=off_2875 on theBenchmark for (2875ds/28120Mi)
% 138.11/19.77 % (297248)Instruction limit reached!
% 138.11/19.77 % (297248)------------------------------
% 138.11/19.77 % (297248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297248)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297248)Termination reason: Instruction limit
% 138.11/19.77 % (297248)Termination phase: Saturation
% 138.11/19.77 % (297248)Time elapsed: 6.113 s
% 138.11/19.77 % (297248)Peak memory usage: 29 MB
% 138.11/19.77 % (297248)Instructions burned: 14135 (million)
% 138.11/19.77 % (297260)fmb+10_1_sil=256000:fmbss=7:random_seed=1884930281:fmbsr=1.6:i=182295_2871 on theBenchmark for (2871ds/182295Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297262)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=331923464:i=44625:gsp=on_2871 on theBenchmark for (2871ds/44625Mi)
% 138.11/19.77 % (297262)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 138.11/19.77 % (297262)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297264)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2118662687:i=160505_2871 on theBenchmark for (2871ds/160505Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297266)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3631817292:fmbsr=1.3:i=225729_2870 on theBenchmark for (2870ds/225729Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297268)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4155233831:fmbsr=2:i=185024:ins=7_2870 on theBenchmark for (2870ds/185024Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297270)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1963281017:rtra=on_2870 on theBenchmark for (2870ds/0Mi)
% 138.11/19.77 % Exception at run slice level
% 138.11/19.77 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.11/19.77 % (297272)% WARNING: option uhcvi not known.
% 138.11/19.77 % (297272)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=354715897:i=271062:add=off:rtra=on:rawr=on_2870 on theBenchmark for (2870ds/271062Mi)
% 138.11/19.77 % (297272)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 138.11/19.77 % (297272)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 138.11/19.77 % (297226)Instruction limit reached!
% 138.11/19.77 % (297226)------------------------------
% 138.11/19.77 % (297226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297226)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297226)Termination reason: Instruction limit
% 138.11/19.77 % (297226)Termination phase: Saturation
% 138.11/19.77 % (297226)Time elapsed: 12.522 s
% 138.11/19.77 % (297226)Peak memory usage: 45 MB
% 138.11/19.77 % (297226)Instructions burned: 29342 (million)
% 138.11/19.77 % (297274)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2170189166:i=176048:add=on:rtra=on:rawr=on_2854 on theBenchmark for (2854ds/176048Mi)
% 138.11/19.77 % (297254) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-297157-297254"...
% 138.11/19.77 % (297252)Instruction limit reached!
% 138.11/19.77 % (297252)------------------------------
% 138.11/19.77 % (297252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297252)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297252)Termination reason: Instruction limit
% 138.11/19.77 % (297252)Termination phase: Saturation
% 138.11/19.77 % (297252)Time elapsed: 8.349 s
% 138.11/19.77 % (297252)Peak memory usage: 63 MB
% 138.11/19.77 % (297252)Instructions burned: 17628 (million)
% 138.11/19.77 % (297254)...printing done.
% 138.11/19.77 % (297254)Refutation found. Thanks to Tanya!
% 138.11/19.77 % SZS status Theorem for theBenchmark
% 138.11/19.77 % SZS output start Proof for theBenchmark
% 138.11/19.77 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 138.11/19.77 thf(func_def_0, type, irel: ($i > $i > $o)).
% 138.11/19.77 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_9, type, itrue: ($i > $o)).
% 138.11/19.77 thf(func_def_10, type, ifalse: ($i > $o)).
% 138.11/19.77 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 138.11/19.77 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 138.11/19.77 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 138.11/19.77 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 138.11/19.77 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 138.11/19.77 thf(func_def_21, type, p: ($i > $o)).
% 138.11/19.77 thf(func_def_22, type, q: ($i > $o)).
% 138.11/19.77 thf(func_def_23, type, r: ($i > $o)).
% 138.11/19.77 thf(func_def_24, type, s: ($i > $o)).
% 138.11/19.77 thf(func_def_25, type, t: ($i > $o)).
% 138.11/19.77 thf(func_def_28, type, vNOT: ($o > $o)).
% 138.11/19.77 thf(func_def_29, type, db1: !>[X0: $tType]:(X0)).
% 138.11/19.77 thf(func_def_30, type, db0: !>[X0: $tType]:(X0)).
% 138.11/19.77 thf(func_def_31, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 138.11/19.77 thf(func_def_32, type, vOR: ($o > $o > $o)).
% 138.11/19.77 thf(func_def_33, type, db2: !>[X0: $tType]:(X0)).
% 138.11/19.77 thf(func_def_34, type, vAND: ($o > $o > $o)).
% 138.11/19.77 thf(func_def_35, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 138.11/19.77 thf(func_def_36, type, vIMP: ($o > $o > $o)).
% 138.11/19.77 thf(func_def_37, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 138.11/19.77 thf(func_def_39, type, sK1: ($i > $i)).
% 138.11/19.77 thf(func_def_40, type, sK2: ($i > $i)).
% 138.11/19.77 thf(func_def_41, type, sK3: ($i > $i)).
% 138.11/19.77 thf(func_def_42, type, sK4: ($i > $i)).
% 138.11/19.77 thf(func_def_44, type, sK6: ($i > $i)).
% 138.11/19.77 thf(func_def_45, type, sK7: ($i > $i)).
% 138.11/19.77 thf(func_def_46, type, sK8: ($i > $i)).
% 138.11/19.77 thf(f1,axiom,(
% 138.11/19.77 ! [X0 : $i] : (irel @ X0 @ X0)),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 138.11/19.77 thf(f2,axiom,(
% 138.11/19.77 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 138.11/19.77 thf(f3,axiom,(
% 138.11/19.77 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mnot)).
% 138.11/19.77 thf(f4,axiom,(
% 138.11/19.77 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mor)).
% 138.11/19.77 thf(f5,axiom,(
% 138.11/19.77 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mand)).
% 138.11/19.77 thf(f6,axiom,(
% 138.11/19.77 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mimplies)).
% 138.11/19.77 thf(f7,axiom,(
% 138.11/19.77 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 138.11/19.77 thf(f8,axiom,(
% 138.11/19.77 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iatom)).
% 138.11/19.77 thf(f9,axiom,(
% 138.11/19.77 (inot = (^[X0 : ($i > $o)] : ((mnot @ (mbox_s4 @ X0)))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',inot)).
% 138.11/19.77 thf(f12,axiom,(
% 138.11/19.77 (iand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ X0 @ X1))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iand)).
% 138.11/19.77 thf(f14,axiom,(
% 138.11/19.77 (iimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iimplies)).
% 138.11/19.77 thf(f18,axiom,(
% 138.11/19.77 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 138.11/19.77 thf(f22,axiom,(
% 138.11/19.77 (ivalid @ (iatom @ s))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom1)).
% 138.11/19.77 thf(f23,axiom,(
% 138.11/19.77 (ivalid @ (iimplies @ (inot @ (iimplies @ (iatom @ t) @ (iatom @ r))) @ (iatom @ p)))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom2)).
% 138.11/19.77 thf(f24,conjecture,(
% 138.11/19.77 (ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))),
% 138.11/19.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 138.11/19.77 thf(f25,negated_conjecture,(
% 138.11/19.77 ~(ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))),
% 138.11/19.77 inference(negated_conjecture,[status(cth)],[f24])).
% 138.11/19.77 thf(f26,plain,(
% 138.11/19.77 ! [X0 : $i] : (irel @ X0 @ X0)),
% 138.11/19.77 inference(rectify,[],[f1])).
% 138.11/19.77 thf(f27,plain,(
% 138.11/19.77 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 138.11/19.77 inference(fool_elimination,[],[f26])).
% 138.11/19.77 thf(f28,plain,(
% 138.11/19.77 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 138.11/19.77 inference(rectify,[],[f2])).
% 138.11/19.77 thf(f29,plain,(
% 138.11/19.77 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 138.11/19.77 inference(fool_elimination,[],[f28])).
% 138.11/19.77 thf(f30,plain,(
% 138.11/19.77 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 138.11/19.77 inference(rectify,[],[f3])).
% 138.11/19.77 thf(f31,plain,(
% 138.11/19.77 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 138.11/19.77 inference(fool_elimination,[],[f30])).
% 138.11/19.77 thf(f32,plain,(
% 138.11/19.77 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 138.11/19.77 inference(rectify,[],[f4])).
% 138.11/19.77 thf(f33,plain,(
% 138.11/19.77 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 138.11/19.77 inference(fool_elimination,[],[f32])).
% 138.11/19.77 thf(f34,plain,(
% 138.11/19.77 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 138.11/19.77 inference(rectify,[],[f5])).
% 138.11/19.77 thf(f35,plain,(
% 138.11/19.77 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 138.11/19.77 inference(fool_elimination,[],[f34])).
% 138.11/19.77 thf(f36,plain,(
% 138.11/19.77 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 138.11/19.77 inference(fool_elimination,[],[f6])).
% 138.11/19.77 thf(f37,plain,(
% 138.11/19.77 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 138.11/19.77 inference(rectify,[],[f7])).
% 138.11/19.77 thf(f38,plain,(
% 138.11/19.77 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 138.11/19.77 inference(fool_elimination,[],[f37])).
% 138.11/19.77 thf(f39,plain,(
% 138.11/19.77 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 138.11/19.77 inference(fool_elimination,[],[f8])).
% 138.11/19.77 thf(f40,plain,(
% 138.11/19.77 (inot = (^[Y0 : $i > $o]: (mnot @ (mbox_s4 @ Y0))))),
% 138.11/19.77 inference(fool_elimination,[],[f9])).
% 138.11/19.77 thf(f42,plain,(
% 138.11/19.77 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 138.11/19.77 inference(fool_elimination,[],[f12])).
% 138.11/19.77 thf(f44,plain,(
% 138.11/19.77 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 138.11/19.77 inference(fool_elimination,[],[f14])).
% 138.11/19.77 thf(f48,plain,(
% 138.11/19.77 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 138.11/19.77 inference(rectify,[],[f18])).
% 138.11/19.77 thf(f49,plain,(
% 138.11/19.77 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 138.11/19.77 inference(fool_elimination,[],[f48])).
% 138.11/19.77 thf(f56,plain,(
% 138.11/19.77 (ivalid @ (iatom @ s))),
% 138.11/19.77 inference(rectify,[],[f22])).
% 138.11/19.77 thf(f57,plain,(
% 138.11/19.77 (((ivalid @ (iatom @ s))) = $true)),
% 138.11/19.77 inference(fool_elimination,[],[f56])).
% 138.11/19.77 thf(f58,plain,(
% 138.11/19.77 (ivalid @ (iimplies @ (inot @ (iimplies @ (iatom @ t) @ (iatom @ r))) @ (iatom @ p)))),
% 138.11/19.77 inference(rectify,[],[f23])).
% 138.11/19.77 thf(f59,plain,(
% 138.11/19.77 (((ivalid @ (iimplies @ (inot @ (iimplies @ (iatom @ t) @ (iatom @ r))) @ (iatom @ p)))) = $true)),
% 138.11/19.77 inference(fool_elimination,[],[f58])).
% 138.11/19.77 thf(f60,plain,(
% 138.11/19.77 ~(ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))),
% 138.11/19.77 inference(rectify,[],[f25])).
% 138.11/19.77 thf(f61,plain,(
% 138.11/19.77 ~ (((ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))) = $true)),
% 138.11/19.77 inference(fool_elimination,[],[f60])).
% 138.11/19.77 thf(f62,plain,(
% 138.11/19.77 (((ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))) != $true)),
% 138.11/19.77 inference(flattening,[],[f61])).
% 138.11/19.77 thf(f63,plain,(
% 138.11/19.77 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 138.11/19.77 inference(ennf_transformation,[],[f29])).
% 138.11/19.77 thf(f64,plain,(
% 138.11/19.77 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 138.11/19.77 inference(flattening,[],[f63])).
% 138.11/19.77 thf(f65,plain,(
% 138.11/19.77 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 138.11/19.77 inference(cnf_transformation,[],[f27])).
% 138.11/19.77 thf(f66,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)) )),
% 138.11/19.77 inference(cnf_transformation,[],[f64])).
% 138.11/19.77 thf(f67,plain,(
% 138.11/19.77 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 138.11/19.77 inference(cnf_transformation,[],[f31])).
% 138.11/19.77 thf(f68,plain,(
% 138.11/19.77 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 138.11/19.77 inference(cnf_transformation,[],[f33])).
% 138.11/19.77 thf(f69,plain,(
% 138.11/19.77 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 138.11/19.77 inference(cnf_transformation,[],[f35])).
% 138.11/19.77 thf(f70,plain,(
% 138.11/19.77 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 138.11/19.77 inference(cnf_transformation,[],[f36])).
% 138.11/19.77 thf(f71,plain,(
% 138.11/19.77 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 138.11/19.77 inference(cnf_transformation,[],[f38])).
% 138.11/19.77 thf(f72,plain,(
% 138.11/19.77 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 138.11/19.77 inference(cnf_transformation,[],[f39])).
% 138.11/19.77 thf(f73,plain,(
% 138.11/19.77 (inot = (^[Y0 : $i > $o]: (mnot @ (mbox_s4 @ Y0))))),
% 138.11/19.77 inference(cnf_transformation,[],[f40])).
% 138.11/19.77 thf(f76,plain,(
% 138.11/19.77 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 138.11/19.77 inference(cnf_transformation,[],[f42])).
% 138.11/19.77 thf(f78,plain,(
% 138.11/19.77 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 138.11/19.77 inference(cnf_transformation,[],[f44])).
% 138.11/19.77 thf(f82,plain,(
% 138.11/19.77 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 138.11/19.77 inference(cnf_transformation,[],[f49])).
% 138.11/19.77 thf(f86,plain,(
% 138.11/19.77 (((ivalid @ (iatom @ s))) = $true)),
% 138.11/19.77 inference(cnf_transformation,[],[f57])).
% 138.11/19.77 thf(f87,plain,(
% 138.11/19.77 (((ivalid @ (iimplies @ (inot @ (iimplies @ (iatom @ t) @ (iatom @ r))) @ (iatom @ p)))) = $true)),
% 138.11/19.77 inference(cnf_transformation,[],[f59])).
% 138.11/19.77 thf(f88,plain,(
% 138.11/19.77 (((ivalid @ (iimplies @ (inot @ (iand @ (iimplies @ (iatom @ p) @ (iatom @ q)) @ (iimplies @ (iatom @ t) @ (iatom @ r)))) @ (iand @ (inot @ (inot @ (iatom @ p))) @ (iand @ (iatom @ s) @ (iatom @ s)))))) != $true)),
% 138.11/19.77 inference(cnf_transformation,[],[f62])).
% 138.11/19.77 thf(f90,definition,(
% 138.11/19.77 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 138.11/19.77 introduced(theory,[fool_exhaustiveness_axiom])).
% 138.11/19.77 thf(f91,plain,(
% 138.11/19.77 (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)))))),
% 138.11/19.77 inference(definition_unfolding,[],[f70,f68,f67])).
% 138.11/19.77 thf(f92,plain,(
% 138.11/19.77 (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))))),
% 138.11/19.77 inference(definition_unfolding,[],[f73,f67,f71])).
% 138.11/19.77 thf(f94,plain,(
% 138.11/19.77 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))))),
% 138.11/19.77 inference(definition_unfolding,[],[f76,f69])).
% 138.11/19.77 thf(f96,plain,(
% 138.11/19.77 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 138.11/19.77 inference(definition_unfolding,[],[f78,f91,f71,f71])).
% 138.11/19.77 thf(f100,plain,(
% 138.11/19.77 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ s))))),
% 138.11/19.77 inference(definition_unfolding,[],[f86,f82,f72])).
% 138.11/19.77 thf(f101,plain,(
% 138.11/19.77 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ t) @ ((^[Y0 : $i > $o]: (Y0)) @ r))) @ ((^[Y0 : $i > $o]: (Y0)) @ p)))))),
% 138.11/19.77 inference(definition_unfolding,[],[f87,f82,f96,f92,f96,f72,f72,f72])).
% 138.11/19.77 thf(f102,plain,(
% 138.11/19.77 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ p) @ ((^[Y0 : $i > $o]: (Y0)) @ q)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ t) @ ((^[Y0 : $i > $o]: (Y0)) @ r)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: (Y0)) @ p))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ s) @ ((^[Y0 : $i > $o]: (Y0)) @ s)))))))),
% 138.11/19.77 inference(definition_unfolding,[],[f88,f82,f96,f92,f94,f96,f72,f72,f96,f72,f72,f94,f92,f92,f72,f94,f72,f72])).
% 138.11/19.77 thf(f103,plain,(
% 138.11/19.77 ($true != ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (q @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (t @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (r @ Y3)))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p @ Y3))))))))) & ((s @ Y1) & (s @ Y1)))))))))))),
% 138.11/19.77 inference(beta-eta_normalization,[],[f102])).
% 138.11/19.77 thf(f104,plain,(
% 138.11/19.77 ($false = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (q @ Y3))))) & ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (t @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (r @ Y3)))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p @ Y3))))))))) & ((s @ Y1) & (s @ Y1)))))))) @ sK0)))),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f103])).
% 138.11/19.77 thf(f105,plain,(
% 138.11/19.77 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))))))) & ((s @ Y0) & (s @ Y0)))))))))),
% 138.11/19.77 inference(beta-eta_normalization,[],[f104])).
% 138.11/19.77 thf(f106,plain,(
% 138.11/19.77 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))))))) & ((s @ Y0) & (s @ Y0))))))))),
% 138.11/19.77 inference(or_proxy_clausification,[],[f105])).
% 138.11/19.77 thf(f107,plain,(
% 138.11/19.77 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2))))))))))))))))),
% 138.11/19.77 inference(or_proxy_clausification,[],[f105])).
% 138.11/19.77 thf(f108,plain,(
% 138.11/19.77 ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))))))),
% 138.11/19.77 inference(not_proxy_clausification,[],[f107])).
% 138.11/19.77 thf(f109,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2))))) & ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))) @ X1)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f108])).
% 138.11/19.77 thf(f110,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = (((irel @ sK0 @ X1) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f109])).
% 138.11/19.77 thf(f111,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))))))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f110])).
% 138.11/19.77 thf(f112,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f111])).
% 138.11/19.77 thf(f113,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))) @ (sK1 @ X1))))) )),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f112])).
% 138.11/19.77 thf(f114,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((irel @ X1 @ (sK1 @ X1)) => (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0)))))))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f113])).
% 138.11/19.77 thf(f115,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))))))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f114])).
% 138.11/19.77 thf(f116,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ X1 @ (sK1 @ X1))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f114])).
% 138.11/19.77 thf(f117,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(and_proxy_clausification,[],[f115])).
% 138.11/19.77 thf(f118,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f117])).
% 138.11/19.77 thf(f119,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f117])).
% 138.11/19.77 thf(f120,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f119])).
% 138.11/19.77 thf(f121,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))) @ X2))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f120])).
% 138.11/19.77 thf(f123,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))) @ X2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0)))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f121])).
% 138.11/19.77 thf(f124,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f123])).
% 138.11/19.77 thf(f125,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (t @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))) @ X3)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f124])).
% 138.11/19.77 thf(f126,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((irel @ (sK1 @ X1) @ X2) => (t @ X2)))) | ($true = (((irel @ (sK1 @ X1) @ X3) => (p @ X3))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f125])).
% 138.11/19.77 thf(f127,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($true = (((irel @ (sK1 @ X1) @ X3) => (p @ X3)))) | ($true = ((t @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f126])).
% 138.11/19.77 thf(f128,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($false = ((irel @ (sK1 @ X1) @ X3))) | ($true = ((t @ X2))) | ($true = ((p @ X3)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f127])).
% 138.11/19.77 thf(f134,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))) @ (sK3 @ X1)))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (q @ Y0)))))))) )),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f118])).
% 138.11/19.77 thf(f136,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))) @ (sK3 @ X1)))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0)))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f134])).
% 138.11/19.77 thf(f137,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))) @ (sK3 @ X1)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f136])).
% 138.11/19.77 thf(f138,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (r @ Y0))) @ (sK3 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p @ Y0))) @ X2)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f137])).
% 138.11/19.77 thf(f139,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((irel @ (sK1 @ X1) @ (sK3 @ X1)) => (r @ (sK3 @ X1))))) | ($true = (((irel @ (sK1 @ X1) @ X2) => (p @ X2))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f138])).
% 138.11/19.77 thf(f140,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((r @ (sK3 @ X1)))) | ($true = (((irel @ (sK1 @ X1) @ X2) => (p @ X2))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f139])).
% 138.11/19.77 thf(f141,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ (sK1 @ X1) @ (sK3 @ X1)))) | ($true = (((irel @ (sK1 @ X1) @ X2) => (p @ X2))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f139])).
% 138.11/19.77 thf(f142,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ (sK1 @ X1) @ (sK3 @ X1)))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f141])).
% 138.11/19.77 thf(f143,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((r @ (sK3 @ X1)))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f140])).
% 138.11/19.77 thf(f152,plain,(
% 138.11/19.77 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p @ Y2))))))))) & ((s @ Y0) & (s @ Y0))))) @ sK5)))),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f106])).
% 138.11/19.77 thf(f153,plain,(
% 138.11/19.77 ($false = (((irel @ sK0 @ sK5) => ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))))) & ((s @ sK5) & (s @ sK5))))))),
% 138.11/19.77 inference(beta-eta_normalization,[],[f152])).
% 138.11/19.77 thf(f154,plain,(
% 138.11/19.77 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))))) & ((s @ sK5) & (s @ sK5)))))),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f153])).
% 138.11/19.77 thf(f155,plain,(
% 138.11/19.77 ($true = ((irel @ sK0 @ sK5)))),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f153])).
% 138.11/19.77 thf(f156,plain,(
% 138.11/19.77 ($false = (((s @ sK5) & (s @ sK5)))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1)))))))))))),
% 138.11/19.77 inference(and_proxy_clausification,[],[f154])).
% 138.11/19.77 thf(f157,plain,(
% 138.11/19.77 ($false = ((s @ sK5))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))))))) | ($false = ((s @ sK5)))),
% 138.11/19.77 inference(and_proxy_clausification,[],[f156])).
% 138.11/19.77 thf(f158,plain,(
% 138.11/19.77 ($false = ((s @ sK5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1)))))))))) | ($false = ((s @ sK5)))),
% 138.11/19.77 inference(not_proxy_clausification,[],[f157])).
% 138.11/19.77 thf(f159,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($true = (((^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))) @ X1))) | ($false = ((s @ sK5)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f158])).
% 138.11/19.77 thf(f160,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($true = (((^[Y0 : $i]: ((irel @ sK5 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))) @ X1)))) )),
% 138.11/19.77 inference(duplicate_literal_removal,[],[f159])).
% 138.11/19.77 thf(f161,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($true = (((irel @ sK5 @ X1) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))))))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f160])).
% 138.11/19.77 thf(f162,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0)))))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f161])).
% 138.11/19.77 thf(f163,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f162])).
% 138.11/19.77 thf(f164,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))) @ (sK6 @ X1))))) )),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f163])).
% 138.11/19.77 thf(f165,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($false = (((irel @ X1 @ (sK6 @ X1)) => (p @ (sK6 @ X1)))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f164])).
% 138.11/19.77 thf(f166,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($false = ((p @ (sK6 @ X1))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f165])).
% 138.11/19.77 thf(f167,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((s @ sK5))) | ($false = ((irel @ sK5 @ X1))) | ($true = ((irel @ X1 @ (sK6 @ X1))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f165])).
% 138.11/19.77 thf(f168,plain,(
% 138.11/19.77 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (t @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (r @ Y3))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1)))))))))),
% 138.11/19.77 inference(beta-eta_normalization,[],[f101])).
% 138.11/19.77 thf(f169,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (t @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (r @ Y3))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1)))))) @ X1)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f168])).
% 138.11/19.77 thf(f170,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2))))))))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0)))))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f169])).
% 138.11/19.77 thf(f171,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0)))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f170])).
% 138.11/19.77 thf(f172,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))))))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f171])).
% 138.11/19.77 thf(f173,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2))))))))))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f172])).
% 138.11/19.77 thf(f174,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (t @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2))))))))))) @ (sK7 @ X1))))) )),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f173])).
% 138.11/19.77 thf(f175,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (p @ X2)))) | ($false = (((irel @ X1 @ (sK7 @ X1)) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK7 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))))))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f174])).
% 138.11/19.77 thf(f176,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK7 @ X1)) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK7 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f175])).
% 138.11/19.77 thf(f177,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK7 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))))))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f176])).
% 138.11/19.77 thf(f178,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK7 @ X1)))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f176])).
% 138.11/19.77 thf(f179,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK7 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f177])).
% 138.11/19.77 thf(f180,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((^[Y0 : $i]: ((irel @ (sK7 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (t @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))) @ X3))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f179])).
% 138.11/19.77 thf(f181,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ (sK7 @ X1) @ X3) => ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0)))))))) | ($true = ((p @ X2)))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f180])).
% 138.11/19.77 thf(f182,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0)))))))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f181])).
% 138.11/19.77 thf(f183,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0)))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0)))))))) )),
% 138.11/19.77 inference(or_proxy_clausification,[],[f182])).
% 138.11/19.77 thf(f184,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0))) @ X4))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0)))))))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f183])).
% 138.11/19.77 thf(f185,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0))) @ X4))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0))))))) )),
% 138.11/19.77 inference(not_proxy_clausification,[],[f184])).
% 138.11/19.77 thf(f186,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (r @ Y0))) @ X4))) | ($false = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (t @ Y0))) @ (sK8 @ X3))))) )),
% 138.11/19.77 inference(sigma_proxy_clausification,[],[f185])).
% 138.11/19.77 thf(f187,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($true = (((irel @ X3 @ X4) => (r @ X4)))) | ($false = (((irel @ X3 @ (sK8 @ X3)) => (t @ (sK8 @ X3)))))) )),
% 138.11/19.77 inference(beta-eta_normalization,[],[f186])).
% 138.11/19.77 thf(f188,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($false = ((irel @ X3 @ X4))) | ($false = (((irel @ X3 @ (sK8 @ X3)) => (t @ (sK8 @ X3))))) | ($true = ((r @ X4)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f187])).
% 138.11/19.77 thf(f189,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($false = ((irel @ X3 @ X4))) | ($false = ((t @ (sK8 @ X3)))) | ($true = ((r @ X4)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f188])).
% 138.11/19.77 thf(f190,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($false = ((irel @ X3 @ X4))) | ($true = ((irel @ X3 @ (sK8 @ X3)))) | ($true = ((r @ X4)))) )),
% 138.11/19.77 inference(imp_proxy_clausification,[],[f188])).
% 138.11/19.77 thf(f191,plain,(
% 138.11/19.77 ($true = ((!! @ $i @ s)))),
% 138.11/19.77 inference(beta-eta_normalization,[],[f100])).
% 138.11/19.77 thf(f192,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = ((s @ X1)))) )),
% 138.11/19.77 inference(pi_proxy_clausification,[],[f191])).
% 138.11/19.77 thf(f200,definition,(
% 138.11/19.77 spl9_3 <=> ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ X1 @ (sK1 @ X1)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition])).
% 138.11/19.77 thf(f201,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = ((irel @ X1 @ (sK1 @ X1)))) | ($false = ((irel @ sK0 @ X1)))) ) | ~spl9_3),
% 138.11/19.77 inference(avatar_component_clause,[],[f200])).
% 138.11/19.77 thf(f202,plain,(
% 138.11/19.77 spl9_3),
% 138.11/19.77 inference(avatar_split_clause,[],[f116,f200])).
% 138.11/19.77 thf(f213,definition,(
% 138.11/19.77 spl9_7 <=> ! [X2 : $i,X1 : $i,X3 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($false = ((irel @ (sK1 @ X1) @ X3))) | ($true = ((t @ X2))) | ($true = ((p @ X3))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition])).
% 138.11/19.77 thf(f214,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ X1) @ X3))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((t @ X2))) | ($true = ((p @ X3)))) ) | ~spl9_7),
% 138.11/19.77 inference(avatar_component_clause,[],[f213])).
% 138.11/19.77 thf(f215,plain,(
% 138.11/19.77 spl9_7),
% 138.11/19.77 inference(avatar_split_clause,[],[f128,f213])).
% 138.11/19.77 thf(f234,definition,(
% 138.11/19.77 spl9_13 <=> ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ (sK1 @ X1) @ (sK3 @ X1)))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($true = ((p @ X2))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_13])],[avatar_definition])).
% 138.11/19.77 thf(f235,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ (sK1 @ X1) @ (sK3 @ X1)))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p @ X2)))) ) | ~spl9_13),
% 138.11/19.77 inference(avatar_component_clause,[],[f234])).
% 138.11/19.77 thf(f236,plain,(
% 138.11/19.77 spl9_13),
% 138.11/19.77 inference(avatar_split_clause,[],[f142,f234])).
% 138.11/19.77 thf(f241,definition,(
% 138.11/19.77 spl9_15 <=> ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((r @ (sK3 @ X1)))) | ($false = ((irel @ (sK1 @ X1) @ X2))) | ($true = ((p @ X2))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_15])],[avatar_definition])).
% 138.11/19.77 thf(f242,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ X1) @ X2))) | ($false = ((r @ (sK3 @ X1)))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p @ X2)))) ) | ~spl9_15),
% 138.11/19.77 inference(avatar_component_clause,[],[f241])).
% 138.11/19.77 thf(f243,plain,(
% 138.11/19.77 spl9_15),
% 138.11/19.77 inference(avatar_split_clause,[],[f143,f241])).
% 138.11/19.77 thf(f267,definition,(
% 138.11/19.77 spl9_22 <=> ($true = ((irel @ sK0 @ sK5)))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_22])],[avatar_definition])).
% 138.11/19.77 thf(f269,plain,(
% 138.11/19.77 ($true = ((irel @ sK0 @ sK5))) | ~spl9_22),
% 138.11/19.77 inference(avatar_component_clause,[],[f267])).
% 138.11/19.77 thf(f270,plain,(
% 138.11/19.77 spl9_22),
% 138.11/19.77 inference(avatar_split_clause,[],[f155,f267])).
% 138.11/19.77 thf(f278,definition,(
% 138.11/19.77 spl9_25 <=> ! [X1 : $i] : (($false = ((irel @ sK5 @ X1))) | ($true = ((irel @ X1 @ (sK6 @ X1)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_25])],[avatar_definition])).
% 138.11/19.77 thf(f279,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = ((irel @ X1 @ (sK6 @ X1)))) | ($false = ((irel @ sK5 @ X1)))) ) | ~spl9_25),
% 138.11/19.77 inference(avatar_component_clause,[],[f278])).
% 138.11/19.77 thf(f281,definition,(
% 138.11/19.77 spl9_26 <=> ($false = ((s @ sK5)))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_26])],[avatar_definition])).
% 138.11/19.77 thf(f283,plain,(
% 138.11/19.77 ($false = ((s @ sK5))) | ~spl9_26),
% 138.11/19.77 inference(avatar_component_clause,[],[f281])).
% 138.11/19.77 thf(f284,plain,(
% 138.11/19.77 spl9_25 | spl9_26),
% 138.11/19.77 inference(avatar_split_clause,[],[f167,f281,f278])).
% 138.11/19.77 thf(f289,definition,(
% 138.11/19.77 spl9_28 <=> ! [X1 : $i] : (($false = ((irel @ sK5 @ X1))) | ($false = ((p @ (sK6 @ X1)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_28])],[avatar_definition])).
% 138.11/19.77 thf(f290,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ sK5 @ X1))) | ($false = ((p @ (sK6 @ X1))))) ) | ~spl9_28),
% 138.11/19.77 inference(avatar_component_clause,[],[f289])).
% 138.11/19.77 thf(f291,plain,(
% 138.11/19.77 spl9_28 | spl9_26),
% 138.11/19.77 inference(avatar_split_clause,[],[f166,f281,f289])).
% 138.11/19.77 thf(f299,definition,(
% 138.11/19.77 spl9_31 <=> ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK7 @ X1)))) | ($true = ((p @ X2))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_31])],[avatar_definition])).
% 138.11/19.77 thf(f300,plain,(
% 138.11/19.77 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK7 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p @ X2)))) ) | ~spl9_31),
% 138.11/19.77 inference(avatar_component_clause,[],[f299])).
% 138.11/19.77 thf(f301,plain,(
% 138.11/19.77 spl9_31),
% 138.11/19.77 inference(avatar_split_clause,[],[f178,f299])).
% 138.11/19.77 thf(f312,definition,(
% 138.11/19.77 spl9_35 <=> ! [X4 : $i,X3 : $i,X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($false = ((irel @ X3 @ X4))) | ($true = ((irel @ X3 @ (sK8 @ X3)))) | ($true = ((r @ X4))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_35])],[avatar_definition])).
% 138.11/19.77 thf(f313,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((irel @ X3 @ (sK8 @ X3)))) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($false = ((irel @ X3 @ X4))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p @ X2))) | ($true = ((r @ X4)))) ) | ~spl9_35),
% 138.11/19.77 inference(avatar_component_clause,[],[f312])).
% 138.11/19.77 thf(f314,plain,(
% 138.11/19.77 spl9_35),
% 138.11/19.77 inference(avatar_split_clause,[],[f190,f312])).
% 138.11/19.77 thf(f319,definition,(
% 138.11/19.77 spl9_37 <=> ! [X4 : $i,X3 : $i,X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((irel @ (sK7 @ X1) @ X3))) | ($true = ((p @ X2))) | ($false = ((irel @ X3 @ X4))) | ($false = ((t @ (sK8 @ X3)))) | ($true = ((r @ X4))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_37])],[avatar_definition])).
% 138.11/19.77 thf(f320,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (sK7 @ X1) @ X3))) | ($false = ((irel @ X3 @ X4))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p @ X2))) | ($false = ((t @ (sK8 @ X3)))) | ($true = ((r @ X4)))) ) | ~spl9_37),
% 138.11/19.77 inference(avatar_component_clause,[],[f319])).
% 138.11/19.77 thf(f321,plain,(
% 138.11/19.77 spl9_37),
% 138.11/19.77 inference(avatar_split_clause,[],[f189,f319])).
% 138.11/19.77 thf(f323,definition,(
% 138.11/19.77 spl9_38 <=> ! [X1 : $i] : ($true = ((s @ X1)))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_38])],[avatar_definition])).
% 138.11/19.77 thf(f324,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($true = ((s @ X1)))) ) | ~spl9_38),
% 138.11/19.77 inference(avatar_component_clause,[],[f323])).
% 138.11/19.77 thf(f325,plain,(
% 138.11/19.77 spl9_38),
% 138.11/19.77 inference(avatar_split_clause,[],[f192,f323])).
% 138.11/19.77 thf(f333,definition,(
% 138.11/19.77 spl9_41 <=> ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_41])],[avatar_definition])).
% 138.11/19.77 thf(f334,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) ) | ~spl9_41),
% 138.11/19.77 inference(avatar_component_clause,[],[f333])).
% 138.11/19.77 thf(f335,plain,(
% 138.11/19.77 spl9_41),
% 138.11/19.77 inference(avatar_split_clause,[],[f66,f333])).
% 138.11/19.77 thf(f337,definition,(
% 138.11/19.77 spl9_42 <=> ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_42])],[avatar_definition])).
% 138.11/19.77 thf(f338,plain,(
% 138.11/19.77 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) ) | ~spl9_42),
% 138.11/19.77 inference(avatar_component_clause,[],[f337])).
% 138.11/19.77 thf(f339,plain,(
% 138.11/19.77 spl9_42),
% 138.11/19.77 inference(avatar_split_clause,[],[f65,f337])).
% 138.11/19.77 thf(f352,definition,(
% 138.11/19.77 spl9_46 <=> ! [X0 : $o] : (($true = X0) | ($false = X0))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_46])],[avatar_definition])).
% 138.11/19.77 thf(f353,plain,(
% 138.11/19.77 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) ) | ~spl9_46),
% 138.11/19.77 inference(avatar_component_clause,[],[f352])).
% 138.11/19.77 thf(f354,plain,(
% 138.11/19.77 spl9_46),
% 138.11/19.77 inference(avatar_split_clause,[],[f90,f352])).
% 138.11/19.77 thf(f421,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_26 | ~spl9_38)),
% 138.11/19.77 inference(constrained_superposition,[],[f283,f324])).
% 138.11/19.77 thf(f427,plain,(
% 138.11/19.77 $false | (~spl9_26 | ~spl9_38)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f421])).
% 138.11/19.77 thf(f428,plain,(
% 138.11/19.77 ~spl9_26 | ~spl9_38),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f427])).
% 138.11/19.77 thf(f514,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((p @ (sK6 @ sK5)))) | (~spl9_28 | ~spl9_42)),
% 138.11/19.77 inference(constrained_superposition,[],[f338,f290])).
% 138.11/19.77 thf(f523,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ sK5)))) | (~spl9_28 | ~spl9_42)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f514])).
% 138.11/19.77 thf(f536,definition,(
% 138.11/19.77 spl9_51 <=> ($false = ((p @ (sK6 @ (sK7 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_51])],[avatar_definition])).
% 138.11/19.77 thf(f538,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK7 @ sK5))))) | ~spl9_51),
% 138.11/19.77 inference(avatar_component_clause,[],[f536])).
% 138.11/19.77 thf(f541,definition,(
% 138.11/19.77 spl9_52 <=> ($false = ((p @ (sK6 @ (sK6 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_52])],[avatar_definition])).
% 138.11/19.77 thf(f543,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK6 @ sK5))))) | ~spl9_52),
% 138.11/19.77 inference(avatar_component_clause,[],[f541])).
% 138.11/19.77 thf(f551,definition,(
% 138.11/19.77 spl9_54 <=> ($false = ((p @ (sK6 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_54])],[avatar_definition])).
% 138.11/19.77 thf(f553,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ sK5)))) | ~spl9_54),
% 138.11/19.77 inference(avatar_component_clause,[],[f551])).
% 138.11/19.77 thf(f554,plain,(
% 138.11/19.77 spl9_54 | ~spl9_28 | ~spl9_42),
% 138.11/19.77 inference(avatar_split_clause,[],[f523,f337,f289,f551])).
% 138.11/19.77 thf(f569,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((p @ (sK6 @ (sK6 @ sK5))))) | ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | ~spl9_28)),
% 138.11/19.77 inference(constrained_superposition,[],[f290,f279])).
% 138.11/19.77 thf(f570,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK6 @ sK5))))) | ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | ~spl9_28)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f569])).
% 138.11/19.77 thf(f572,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((p @ (sK6 @ (sK6 @ sK5))))) | (~spl9_25 | ~spl9_28 | ~spl9_42)),
% 138.11/19.77 inference(forward_demodulation,[],[f570,f338])).
% 138.11/19.77 thf(f573,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK6 @ sK5))))) | (~spl9_25 | ~spl9_28 | ~spl9_42)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f572])).
% 138.11/19.77 thf(f576,plain,(
% 138.11/19.77 spl9_52 | ~spl9_25 | ~spl9_28 | ~spl9_42),
% 138.11/19.77 inference(avatar_split_clause,[],[f573,f337,f289,f278,f541])).
% 138.11/19.77 thf(f579,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0))) | ($false = ((p @ (sK6 @ (sK7 @ sK5)))))) ) | (~spl9_28 | ~spl9_31)),
% 138.11/19.77 inference(constrained_superposition,[],[f300,f290])).
% 138.11/19.77 thf(f585,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0))) | ($false = ((p @ (sK6 @ (sK7 @ sK5)))))) ) | (~spl9_28 | ~spl9_31)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f579])).
% 138.11/19.77 thf(f587,definition,(
% 138.11/19.77 spl9_55 <=> ! [X0 : $i] : (($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_55])],[avatar_definition])).
% 138.11/19.77 thf(f588,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0)))) ) | ~spl9_55),
% 138.11/19.77 inference(avatar_component_clause,[],[f587])).
% 138.11/19.77 thf(f590,plain,(
% 138.11/19.77 spl9_51 | spl9_55 | ~spl9_28 | ~spl9_31),
% 138.11/19.77 inference(avatar_split_clause,[],[f585,f299,f289,f587,f536])).
% 138.11/19.77 thf(f1762,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p @ X2))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((r @ X1)))) ) | (~spl9_3 | ~spl9_37)),
% 138.11/19.77 inference(constrained_superposition,[],[f201,f320])).
% 138.11/19.77 thf(f1815,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p @ X2))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((r @ X1)))) ) | (~spl9_3 | ~spl9_37)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f1762])).
% 138.11/19.77 thf(f1867,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) ) | (~spl9_41 | ~spl9_46)),
% 138.11/19.77 inference(constrained_superposition,[],[f334,f353])).
% 138.11/19.77 thf(f1868,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) ) | (~spl9_41 | ~spl9_46)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f1867])).
% 138.11/19.77 thf(f1879,definition,(
% 138.11/19.77 spl9_115 <=> ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_115])],[avatar_definition])).
% 138.11/19.77 thf(f1880,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X2 @ X0))) | ($true = ((irel @ X2 @ X1))) | (((irel @ X0 @ X1)) = $false)) ) | ~spl9_115),
% 138.11/19.77 inference(avatar_component_clause,[],[f1879])).
% 138.11/19.77 thf(f1881,plain,(
% 138.11/19.77 spl9_115 | ~spl9_41 | ~spl9_46),
% 138.11/19.77 inference(avatar_split_clause,[],[f1868,f352,f333,f1879])).
% 138.11/19.77 thf(f9648,definition,(
% 138.11/19.77 spl9_486 <=> ($false = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5))))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_486])],[avatar_definition])).
% 138.11/19.77 thf(f9650,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | ~spl9_486),
% 138.11/19.77 inference(avatar_component_clause,[],[f9648])).
% 138.11/19.77 thf(f28666,definition,(
% 138.11/19.77 spl9_943 <=> ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p @ X2))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((r @ X1))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_943])],[avatar_definition])).
% 138.11/19.77 thf(f28667,plain,(
% 138.11/19.77 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($true = ((p @ X2))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((r @ X1)))) ) | ~spl9_943),
% 138.11/19.77 inference(avatar_component_clause,[],[f28666])).
% 138.11/19.77 thf(f28668,plain,(
% 138.11/19.77 spl9_943 | ~spl9_3 | ~spl9_37),
% 138.11/19.77 inference(avatar_split_clause,[],[f1815,f319,f200,f28666])).
% 138.11/19.77 thf(f29186,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK5 @ sK5))) | ($true = ((p @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_55)),
% 138.11/19.77 inference(constrained_superposition,[],[f279,f588])).
% 138.11/19.77 thf(f29196,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((r @ (sK3 @ X0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ (sK6 @ (sK1 @ X0))))) | ($false = ((irel @ sK5 @ (sK1 @ X0))))) ) | (~spl9_15 | ~spl9_25)),
% 138.11/19.77 inference(constrained_superposition,[],[f242,f279])).
% 138.11/19.77 thf(f29199,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((r @ (sK3 @ X0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ (sK6 @ (sK1 @ X0))))) | ($false = ((irel @ sK5 @ (sK1 @ X0))))) ) | (~spl9_15 | ~spl9_25)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29196])).
% 138.11/19.77 thf(f29209,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ sK5))) | ($true = ((p @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_55)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29186])).
% 138.11/19.77 thf(f29224,definition,(
% 138.11/19.77 spl9_976 <=> ! [X0 : $i] : (($false = ((r @ (sK3 @ X0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ (sK6 @ (sK1 @ X0))))) | ($false = ((irel @ sK5 @ (sK1 @ X0)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_976])],[avatar_definition])).
% 138.11/19.77 thf(f29225,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ sK5 @ (sK1 @ X0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ (sK6 @ (sK1 @ X0))))) | ($false = ((r @ (sK3 @ X0))))) ) | ~spl9_976),
% 138.11/19.77 inference(avatar_component_clause,[],[f29224])).
% 138.11/19.77 thf(f29226,plain,(
% 138.11/19.77 spl9_976 | ~spl9_15 | ~spl9_25),
% 138.11/19.77 inference(avatar_split_clause,[],[f29199,f278,f241,f29224])).
% 138.11/19.77 thf(f29233,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((p @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_42 | ~spl9_55)),
% 138.11/19.77 inference(forward_demodulation,[],[f29209,f338])).
% 138.11/19.77 thf(f29234,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_42 | ~spl9_55)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29233])).
% 138.11/19.77 thf(f29238,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_25 | ~spl9_42 | ~spl9_54 | ~spl9_55)),
% 138.11/19.77 inference(forward_demodulation,[],[f29234,f553])).
% 138.11/19.77 thf(f29239,plain,(
% 138.11/19.77 $false | (~spl9_25 | ~spl9_42 | ~spl9_54 | ~spl9_55)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29238])).
% 138.11/19.77 thf(f29240,plain,(
% 138.11/19.77 ~spl9_25 | ~spl9_42 | ~spl9_54 | ~spl9_55),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f29239])).
% 138.11/19.77 thf(f29466,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK5 @ X0)))) ) | (~spl9_22 | ~spl9_115)),
% 138.11/19.77 inference(constrained_superposition,[],[f1880,f269])).
% 138.11/19.77 thf(f29471,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK5 @ X0)))) ) | (~spl9_22 | ~spl9_115)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29466])).
% 138.11/19.77 thf(f29488,definition,(
% 138.11/19.77 spl9_992 <=> ! [X0 : $i] : (($true = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK5 @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_992])],[avatar_definition])).
% 138.11/19.77 thf(f29489,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ sK5 @ X0))) | ($true = ((irel @ sK0 @ X0)))) ) | ~spl9_992),
% 138.11/19.77 inference(avatar_component_clause,[],[f29488])).
% 138.11/19.77 thf(f29490,plain,(
% 138.11/19.77 spl9_992 | ~spl9_22 | ~spl9_115),
% 138.11/19.77 inference(avatar_split_clause,[],[f29471,f1879,f267,f29488])).
% 138.11/19.77 thf(f29557,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ sK0 @ (sK7 @ sK5)))) | ($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_992)),
% 138.11/19.77 inference(constrained_superposition,[],[f29489,f300])).
% 138.11/19.77 thf(f29575,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK0 @ (sK7 @ sK5)))) | ($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_992)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f29557])).
% 138.11/19.77 thf(f29580,definition,(
% 138.11/19.77 spl9_997 <=> ($true = ((irel @ sK0 @ (sK7 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_997])],[avatar_definition])).
% 138.11/19.77 thf(f29582,plain,(
% 138.11/19.77 ($true = ((irel @ sK0 @ (sK7 @ sK5)))) | ~spl9_997),
% 138.11/19.77 inference(avatar_component_clause,[],[f29580])).
% 138.11/19.77 thf(f29588,plain,(
% 138.11/19.77 spl9_55 | spl9_997 | ~spl9_31 | ~spl9_992),
% 138.11/19.77 inference(avatar_split_clause,[],[f29575,f29488,f299,f29580,f587])).
% 138.11/19.77 thf(f29997,definition,(
% 138.11/19.77 spl9_1023 <=> ($false = ((irel @ sK5 @ (sK6 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1023])],[avatar_definition])).
% 138.11/19.77 thf(f29998,plain,(
% 138.11/19.77 ($false != ((irel @ sK5 @ (sK6 @ sK5)))) | spl9_1023),
% 138.11/19.77 inference(avatar_component_clause,[],[f29997])).
% 138.11/19.77 thf(f29999,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ (sK6 @ sK5)))) | ~spl9_1023),
% 138.11/19.77 inference(avatar_component_clause,[],[f29997])).
% 138.11/19.77 thf(f30013,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | ~spl9_1023)),
% 138.11/19.77 inference(constrained_superposition,[],[f29999,f279])).
% 138.11/19.77 thf(f30024,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | ~spl9_1023)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f30013])).
% 138.11/19.77 thf(f30029,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_25 | ~spl9_42 | ~spl9_1023)),
% 138.11/19.77 inference(forward_demodulation,[],[f30024,f338])).
% 138.11/19.77 thf(f30030,plain,(
% 138.11/19.77 $false | (~spl9_25 | ~spl9_42 | ~spl9_1023)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f30029])).
% 138.11/19.77 thf(f30031,plain,(
% 138.11/19.77 ~spl9_25 | ~spl9_42 | ~spl9_1023),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f30030])).
% 138.11/19.77 thf(f30980,definition,(
% 138.11/19.77 spl9_1070 <=> ! [X0 : $i] : (($false = ((irel @ (sK7 @ sK5) @ X0))) | ($true = ((p @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1070])],[avatar_definition])).
% 138.11/19.77 thf(f30981,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK7 @ sK5) @ X0))) | ($true = ((p @ X0)))) ) | ~spl9_1070),
% 138.11/19.77 inference(avatar_component_clause,[],[f30980])).
% 138.11/19.77 thf(f30988,definition,(
% 138.11/19.77 spl9_1072 <=> ($false = ((irel @ sK5 @ (sK7 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1072])],[avatar_definition])).
% 138.11/19.77 thf(f30989,plain,(
% 138.11/19.77 ($false != ((irel @ sK5 @ (sK7 @ sK5)))) | spl9_1072),
% 138.11/19.77 inference(avatar_component_clause,[],[f30988])).
% 138.11/19.77 thf(f30990,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ (sK7 @ sK5)))) | ~spl9_1072),
% 138.11/19.77 inference(avatar_component_clause,[],[f30988])).
% 138.11/19.77 thf(f31008,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_1072)),
% 138.11/19.77 inference(constrained_superposition,[],[f300,f30990])).
% 138.11/19.77 thf(f31009,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ sK5 @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_1072)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f31008])).
% 138.11/19.77 thf(f31012,plain,(
% 138.11/19.77 spl9_55 | ~spl9_31 | ~spl9_1072),
% 138.11/19.77 inference(avatar_split_clause,[],[f31009,f30988,f299,f587])).
% 138.11/19.77 thf(f31364,definition,(
% 138.11/19.77 spl9_1087 <=> ! [X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X1))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1087])],[avatar_definition])).
% 138.11/19.77 thf(f31365,plain,(
% 138.11/19.77 ( ! [X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X1)))) ) | ~spl9_1087),
% 138.11/19.77 inference(avatar_component_clause,[],[f31364])).
% 138.11/19.77 thf(f31379,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((p @ (sK6 @ (sK7 @ sK5))))) | ($false = ((irel @ sK5 @ (sK7 @ sK5)))) | (~spl9_25 | ~spl9_1070)),
% 138.11/19.77 inference(constrained_superposition,[],[f30981,f279])).
% 138.11/19.77 thf(f31413,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ (sK7 @ sK5))))) | ($false = ((irel @ sK5 @ (sK7 @ sK5)))) | (~spl9_25 | ~spl9_1070)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f31379])).
% 138.11/19.77 thf(f31417,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ (sK7 @ sK5))))) | (~spl9_25 | ~spl9_1070 | spl9_1072)),
% 138.11/19.77 inference(forward_subsumption_resolution,[],[f31413,f30989])).
% 138.11/19.77 thf(f31421,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_25 | ~spl9_51 | ~spl9_1070 | spl9_1072)),
% 138.11/19.77 inference(forward_demodulation,[],[f31417,f538])).
% 138.11/19.77 thf(f31422,plain,(
% 138.11/19.77 $false | (~spl9_25 | ~spl9_51 | ~spl9_1070 | spl9_1072)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f31421])).
% 138.11/19.77 thf(f31423,plain,(
% 138.11/19.77 ~spl9_25 | ~spl9_51 | ~spl9_1070 | spl9_1072),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f31422])).
% 138.11/19.77 thf(f31584,definition,(
% 138.11/19.77 spl9_1097 <=> ($false = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5))))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1097])],[avatar_definition])).
% 138.11/19.77 thf(f31586,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ~spl9_1097),
% 138.11/19.77 inference(avatar_component_clause,[],[f31584])).
% 138.11/19.77 thf(f34820,definition,(
% 138.11/19.77 spl9_1227 <=> ($true = ((irel @ sK5 @ (sK7 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1227])],[avatar_definition])).
% 138.11/19.77 thf(f34821,plain,(
% 138.11/19.77 ($true != ((irel @ sK5 @ (sK7 @ sK5)))) | spl9_1227),
% 138.11/19.77 inference(avatar_component_clause,[],[f34820])).
% 138.11/19.77 thf(f34822,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK7 @ sK5)))) | ~spl9_1227),
% 138.11/19.77 inference(avatar_component_clause,[],[f34820])).
% 138.11/19.77 thf(f34829,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ sK5) @ X0)))) ) | (~spl9_115 | ~spl9_1227)),
% 138.11/19.77 inference(constrained_superposition,[],[f1880,f34822])).
% 138.11/19.77 thf(f34831,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ sK5) @ X0)))) ) | (~spl9_115 | ~spl9_1227)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f34829])).
% 138.11/19.77 thf(f34841,definition,(
% 138.11/19.77 spl9_1229 <=> ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ sK5) @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1229])],[avatar_definition])).
% 138.11/19.77 thf(f34842,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK7 @ sK5) @ X0))) | ($true = ((irel @ sK5 @ X0)))) ) | ~spl9_1229),
% 138.11/19.77 inference(avatar_component_clause,[],[f34841])).
% 138.11/19.77 thf(f34843,plain,(
% 138.11/19.77 spl9_1229 | ~spl9_115 | ~spl9_1227),
% 138.11/19.77 inference(avatar_split_clause,[],[f34831,f34820,f1879,f34841])).
% 138.11/19.77 thf(f35297,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5))))) | ($false = ((irel @ (sK7 @ sK5) @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_1229)),
% 138.11/19.77 inference(constrained_superposition,[],[f34842,f300])).
% 138.11/19.77 thf(f35309,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | (~spl9_3 | ~spl9_1229)),
% 138.11/19.77 inference(constrained_superposition,[],[f201,f34842])).
% 138.11/19.77 thf(f35341,plain,(
% 138.11/19.77 ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | (~spl9_3 | ~spl9_1229)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35309])).
% 138.11/19.77 thf(f35351,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5))))) | ($false = ((irel @ (sK7 @ sK5) @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_31 | ~spl9_1229)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35297])).
% 138.11/19.77 thf(f35357,definition,(
% 138.11/19.77 spl9_1243 <=> ($true = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1243])],[avatar_definition])).
% 138.11/19.77 thf(f35359,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5))))) | ~spl9_1243),
% 138.11/19.77 inference(avatar_component_clause,[],[f35357])).
% 138.11/19.77 thf(f35362,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | (~spl9_3 | ~spl9_997 | ~spl9_1229)),
% 138.11/19.77 inference(forward_demodulation,[],[f35341,f29582])).
% 138.11/19.77 thf(f35363,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | (~spl9_3 | ~spl9_997 | ~spl9_1229)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35362])).
% 138.11/19.77 thf(f35364,plain,(
% 138.11/19.77 spl9_1070 | spl9_1243 | ~spl9_31 | ~spl9_1229),
% 138.11/19.77 inference(avatar_split_clause,[],[f35351,f34841,f299,f35357,f30980])).
% 138.11/19.77 thf(f35374,definition,(
% 138.11/19.77 spl9_1245 <=> ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1245])],[avatar_definition])).
% 138.11/19.77 thf(f35376,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | ~spl9_1245),
% 138.11/19.77 inference(avatar_component_clause,[],[f35374])).
% 138.11/19.77 thf(f35377,plain,(
% 138.11/19.77 spl9_1245 | ~spl9_3 | ~spl9_997 | ~spl9_1229),
% 138.11/19.77 inference(avatar_split_clause,[],[f35363,f34841,f29580,f200,f35374])).
% 138.11/19.77 thf(f35387,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_28 | ~spl9_1243)),
% 138.11/19.77 inference(constrained_superposition,[],[f290,f35359])).
% 138.11/19.77 thf(f35394,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ (sK7 @ sK5)) @ X0)))) ) | (~spl9_115 | ~spl9_1243)),
% 138.11/19.77 inference(constrained_superposition,[],[f1880,f35359])).
% 138.11/19.77 thf(f35397,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ (sK7 @ sK5)) @ X0)))) ) | (~spl9_115 | ~spl9_1243)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35394])).
% 138.11/19.77 thf(f35404,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_28 | ~spl9_1243)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35387])).
% 138.11/19.77 thf(f35415,definition,(
% 138.11/19.77 spl9_1246 <=> ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK7 @ (sK7 @ sK5)) @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1246])],[avatar_definition])).
% 138.11/19.77 thf(f35416,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK7 @ (sK7 @ sK5)) @ X0))) | ($true = ((irel @ sK5 @ X0)))) ) | ~spl9_1246),
% 138.11/19.77 inference(avatar_component_clause,[],[f35415])).
% 138.11/19.77 thf(f35417,plain,(
% 138.11/19.77 spl9_1246 | ~spl9_115 | ~spl9_1243),
% 138.11/19.77 inference(avatar_split_clause,[],[f35397,f35357,f1879,f35415])).
% 138.11/19.77 thf(f35422,plain,(
% 138.11/19.77 spl9_1097 | ~spl9_28 | ~spl9_1243),
% 138.11/19.77 inference(avatar_split_clause,[],[f35404,f35357,f289,f31584])).
% 138.11/19.77 thf(f35481,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_28 | ~spl9_1245)),
% 138.11/19.77 inference(constrained_superposition,[],[f290,f35376])).
% 138.11/19.77 thf(f35498,plain,(
% 138.11/19.77 ($false = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_28 | ~spl9_1245)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35481])).
% 138.11/19.77 thf(f35516,plain,(
% 138.11/19.77 spl9_486 | ~spl9_28 | ~spl9_1245),
% 138.11/19.77 inference(avatar_split_clause,[],[f35498,f35374,f289,f9648])).
% 138.11/19.77 thf(f35615,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = $false) | ($false = ((irel @ (sK7 @ X1) @ (sK1 @ X0)))) | ($false = ((irel @ (sK1 @ X0) @ X2))) | ($false = ((irel @ X1 @ X3))) | ($true = ((p @ X3))) | ($true = ((r @ X2))) | ($false = ((irel @ (sK1 @ X0) @ X4))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ X0))))) | ($true = ((p @ X4)))) ) | (~spl9_7 | ~spl9_35)),
% 138.11/19.77 inference(constrained_superposition,[],[f313,f214])).
% 138.11/19.77 thf(f35644,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (sK7 @ X1) @ (sK1 @ X0)))) | ($false = ((irel @ (sK1 @ X0) @ X2))) | ($false = ((irel @ X1 @ X3))) | ($true = ((p @ X3))) | ($true = ((r @ X2))) | ($false = ((irel @ (sK1 @ X0) @ X4))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ X0))))) | ($true = ((p @ X4)))) ) | (~spl9_7 | ~spl9_35)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f35615])).
% 138.11/19.77 thf(f35696,definition,(
% 138.11/19.77 spl9_1256 <=> ! [X4 : $i,X0 : $i,X3 : $i,X2 : $i,X1 : $i] : (($false = ((irel @ (sK7 @ X1) @ (sK1 @ X0)))) | ($false = ((irel @ (sK1 @ X0) @ X2))) | ($false = ((irel @ X1 @ X3))) | ($true = ((p @ X3))) | ($true = ((r @ X2))) | ($false = ((irel @ (sK1 @ X0) @ X4))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ X0))))) | ($true = ((p @ X4))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1256])],[avatar_definition])).
% 138.11/19.77 thf(f35697,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ (sK7 @ X1) @ (sK1 @ X0)))) | ($false = ((irel @ (sK1 @ X0) @ X4))) | ($false = ((irel @ (sK1 @ X0) @ X2))) | ($false = ((irel @ X1 @ X3))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ X0))))) | ($true = ((p @ X4)))) ) | ~spl9_1256),
% 138.11/19.77 inference(avatar_component_clause,[],[f35696])).
% 138.11/19.77 thf(f35698,plain,(
% 138.11/19.77 spl9_1256 | ~spl9_7 | ~spl9_35),
% 138.11/19.77 inference(avatar_split_clause,[],[f35644,f312,f213,f35696])).
% 138.11/19.77 thf(f38542,definition,(
% 138.11/19.77 spl9_1344 <=> ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1344])],[avatar_definition])).
% 138.11/19.77 thf(f38543,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0)))) ) | ~spl9_1344),
% 138.11/19.77 inference(avatar_component_clause,[],[f38542])).
% 138.11/19.77 thf(f39200,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1344)),
% 138.11/19.77 inference(constrained_superposition,[],[f279,f38543])).
% 138.11/19.77 thf(f39240,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ (sK1 @ (sK7 @ sK5))))) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1344)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f39200])).
% 138.11/19.77 thf(f39260,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1245 | ~spl9_1344)),
% 138.11/19.77 inference(forward_demodulation,[],[f39240,f35376])).
% 138.11/19.77 thf(f39261,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1245 | ~spl9_1344)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f39260])).
% 138.11/19.77 thf(f39264,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_25 | ~spl9_486 | ~spl9_1245 | ~spl9_1344)),
% 138.11/19.77 inference(forward_demodulation,[],[f39261,f9650])).
% 138.11/19.77 thf(f39265,plain,(
% 138.11/19.77 $false | (~spl9_25 | ~spl9_486 | ~spl9_1245 | ~spl9_1344)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f39264])).
% 138.11/19.77 thf(f39266,plain,(
% 138.11/19.77 ~spl9_25 | ~spl9_486 | ~spl9_1245 | ~spl9_1344),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f39265])).
% 138.11/19.77 thf(f48068,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5))))) | ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1246)),
% 138.11/19.77 inference(constrained_superposition,[],[f279,f35416])).
% 138.11/19.77 thf(f48129,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ (sK7 @ (sK7 @ sK5))))) | ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1246)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f48068])).
% 138.11/19.77 thf(f48162,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1243 | ~spl9_1246)),
% 138.11/19.77 inference(forward_demodulation,[],[f48129,f35359])).
% 138.11/19.77 thf(f48163,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | (~spl9_25 | ~spl9_1243 | ~spl9_1246)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f48162])).
% 138.11/19.77 thf(f48172,definition,(
% 138.11/19.77 spl9_1593 <=> ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5))))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1593])],[avatar_definition])).
% 138.11/19.77 thf(f48174,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ~spl9_1593),
% 138.11/19.77 inference(avatar_component_clause,[],[f48172])).
% 138.11/19.77 thf(f48175,plain,(
% 138.11/19.77 spl9_1593 | ~spl9_25 | ~spl9_1243 | ~spl9_1246),
% 138.11/19.77 inference(avatar_split_clause,[],[f48163,f35415,f35357,f278,f48172])).
% 138.11/19.77 thf(f48513,definition,(
% 138.11/19.77 spl9_1603 <=> ($true = ((irel @ sK5 @ (sK6 @ sK5))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1603])],[avatar_definition])).
% 138.11/19.77 thf(f48514,plain,(
% 138.11/19.77 ($true != ((irel @ sK5 @ (sK6 @ sK5)))) | spl9_1603),
% 138.11/19.77 inference(avatar_component_clause,[],[f48513])).
% 138.11/19.77 thf(f48515,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK6 @ sK5)))) | ~spl9_1603),
% 138.11/19.77 inference(avatar_component_clause,[],[f48513])).
% 138.11/19.77 thf(f48563,definition,(
% 138.11/19.77 spl9_1613 <=> ($true = ((irel @ sK5 @ (sK6 @ (sK6 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1613])],[avatar_definition])).
% 138.11/19.77 thf(f48564,plain,(
% 138.11/19.77 ($true != ((irel @ sK5 @ (sK6 @ (sK6 @ sK5))))) | spl9_1613),
% 138.11/19.77 inference(avatar_component_clause,[],[f48563])).
% 138.11/19.77 thf(f48565,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK6 @ (sK6 @ sK5))))) | ~spl9_1613),
% 138.11/19.77 inference(avatar_component_clause,[],[f48563])).
% 138.11/19.77 thf(f48631,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK6 @ sK5) @ X0)))) ) | (~spl9_115 | ~spl9_1603)),
% 138.11/19.77 inference(constrained_superposition,[],[f1880,f48515])).
% 138.11/19.77 thf(f48633,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK6 @ sK5) @ X0)))) ) | (~spl9_115 | ~spl9_1603)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f48631])).
% 138.11/19.77 thf(f48640,definition,(
% 138.11/19.77 spl9_1619 <=> ! [X0 : $i] : (($true = ((irel @ sK5 @ X0))) | ($false = ((irel @ (sK6 @ sK5) @ X0))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1619])],[avatar_definition])).
% 138.11/19.77 thf(f48641,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK6 @ sK5) @ X0))) | ($true = ((irel @ sK5 @ X0)))) ) | ~spl9_1619),
% 138.11/19.77 inference(avatar_component_clause,[],[f48640])).
% 138.11/19.77 thf(f48642,plain,(
% 138.11/19.77 spl9_1619 | ~spl9_115 | ~spl9_1603),
% 138.11/19.77 inference(avatar_split_clause,[],[f48633,f48513,f1879,f48640])).
% 138.11/19.77 thf(f53720,plain,(
% 138.11/19.77 ($true != $true) | ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | spl9_1603)),
% 138.11/19.77 inference(constrained_superposition,[],[f48514,f279])).
% 138.11/19.77 thf(f53725,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ sK5))) | (~spl9_25 | spl9_1603)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f53720])).
% 138.11/19.77 thf(f53729,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_25 | ~spl9_42 | spl9_1603)),
% 138.11/19.77 inference(forward_demodulation,[],[f53725,f338])).
% 138.11/19.77 thf(f53730,plain,(
% 138.11/19.77 $false | (~spl9_25 | ~spl9_42 | spl9_1603)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f53729])).
% 138.11/19.77 thf(f53731,plain,(
% 138.11/19.77 ~spl9_25 | ~spl9_42 | spl9_1603),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f53730])).
% 138.11/19.77 thf(f54768,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_1593)),
% 138.11/19.77 inference(constrained_superposition,[],[f28667,f48174])).
% 138.11/19.77 thf(f54986,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_1593)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f54768])).
% 138.11/19.77 thf(f55104,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_997 | ~spl9_1593)),
% 138.11/19.77 inference(forward_demodulation,[],[f54986,f29582])).
% 138.11/19.77 thf(f55105,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_997 | ~spl9_1593)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f55104])).
% 138.11/19.77 thf(f55168,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_997 | ~spl9_1097 | ~spl9_1593)),
% 138.11/19.77 inference(forward_demodulation,[],[f55105,f31586])).
% 138.11/19.77 thf(f55169,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((r @ X0)))) ) | (~spl9_943 | ~spl9_997 | ~spl9_1097 | ~spl9_1593)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f55168])).
% 138.11/19.77 thf(f55195,definition,(
% 138.11/19.77 spl9_1738 <=> ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5))))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_1738])],[avatar_definition])).
% 138.11/19.77 thf(f55197,plain,(
% 138.11/19.77 ($false = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ~spl9_1738),
% 138.11/19.77 inference(avatar_component_clause,[],[f55195])).
% 138.11/19.77 thf(f55221,plain,(
% 138.11/19.77 spl9_1738 | spl9_1087 | ~spl9_943 | ~spl9_997 | ~spl9_1097 | ~spl9_1593),
% 138.11/19.77 inference(avatar_split_clause,[],[f55169,f48172,f31584,f29580,f28666,f31364,f55195])).
% 138.11/19.77 thf(f55892,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((irel @ sK5 @ (sK6 @ (sK6 @ sK5))))) | ($false = ((irel @ sK5 @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_1619)),
% 138.11/19.77 inference(constrained_superposition,[],[f48641,f279])).
% 138.11/19.77 thf(f56029,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK6 @ (sK6 @ sK5))))) | ($false = ((irel @ sK5 @ (sK6 @ sK5)))) | (~spl9_25 | ~spl9_1619)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f55892])).
% 138.11/19.77 thf(f57931,plain,(
% 138.11/19.77 ($false = ((irel @ sK5 @ (sK6 @ sK5)))) | (~spl9_25 | spl9_1613 | ~spl9_1619)),
% 138.11/19.77 inference(forward_subsumption_resolution,[],[f56029,f48564])).
% 138.11/19.77 thf(f57965,plain,(
% 138.11/19.77 $false | (~spl9_25 | spl9_1023 | spl9_1613 | ~spl9_1619)),
% 138.11/19.77 inference(forward_subsumption_resolution,[],[f57931,f29998])).
% 138.11/19.77 thf(f57966,plain,(
% 138.11/19.77 ~spl9_25 | spl9_1023 | spl9_1613 | ~spl9_1619),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f57965])).
% 138.11/19.77 thf(f58391,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((irel @ sK5 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK6 @ sK5))))) | (~spl9_31 | ~spl9_1613)),
% 138.11/19.77 inference(constrained_superposition,[],[f48565,f300])).
% 138.11/19.77 thf(f58435,plain,(
% 138.11/19.77 ($true = ((irel @ sK5 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK6 @ sK5))))) | (~spl9_31 | ~spl9_1613)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f58391])).
% 138.11/19.77 thf(f111297,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X2))) | ($false = ((irel @ X0 @ X3))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((p @ X1)))) ) | (~spl9_3 | ~spl9_1256)),
% 138.11/19.77 inference(constrained_superposition,[],[f201,f35697])).
% 138.11/19.77 thf(f111772,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X2))) | ($false = ((irel @ X0 @ X3))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((p @ X1)))) ) | (~spl9_3 | ~spl9_1256)),
% 138.11/19.77 inference(duplicate_literal_removal,[],[f111297])).
% 138.11/19.77 thf(f111773,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X2))) | ($false = ((irel @ X0 @ X3))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((p @ X1)))) ) | (~spl9_3 | ~spl9_1256)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f111772])).
% 138.11/19.77 thf(f112108,definition,(
% 138.11/19.77 spl9_2678 <=> ! [X0 : $i,X3 : $i,X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X2))) | ($false = ((irel @ X0 @ X3))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((p @ X1))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_2678])],[avatar_definition])).
% 138.11/19.77 thf(f112109,plain,(
% 138.11/19.77 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X2))) | ($false = ((irel @ (sK1 @ (sK7 @ X0)) @ X1))) | ($false = ((irel @ X0 @ X3))) | ($false = ((irel @ sK0 @ (sK7 @ X0)))) | ($true = ((r @ X2))) | ($true = ((p @ X3))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ X0)))))) | ($true = ((p @ X1)))) ) | ~spl9_2678),
% 138.11/19.77 inference(avatar_component_clause,[],[f112108])).
% 138.11/19.77 thf(f112110,plain,(
% 138.11/19.77 spl9_2678 | ~spl9_3 | ~spl9_1256),
% 138.11/19.77 inference(avatar_split_clause,[],[f111773,f35696,f200,f112108])).
% 138.11/19.77 thf(f139783,definition,(
% 138.11/19.77 spl9_3053 <=> ($false = ((r @ (sK3 @ (sK7 @ sK5)))))),
% 138.11/19.77 introduced(definition,[new_symbols(definition,[spl9_3053])],[avatar_definition])).
% 138.11/19.77 thf(f139785,plain,(
% 138.11/19.77 ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | ~spl9_3053),
% 138.11/19.77 inference(avatar_component_clause,[],[f139783])).
% 138.11/19.77 thf(f165792,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_976 | ~spl9_1245)),
% 138.11/19.77 inference(constrained_superposition,[],[f35376,f29225])).
% 138.11/19.77 thf(f165829,plain,(
% 138.11/19.77 ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_976 | ~spl9_1245)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f165792])).
% 138.11/19.77 thf(f232928,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((r @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(constrained_superposition,[],[f112109,f48174])).
% 138.11/19.77 thf(f233824,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((r @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f232928])).
% 138.11/19.77 thf(f234319,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(forward_demodulation,[],[f233824,f29582])).
% 138.11/19.77 thf(f234320,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((p @ (sK6 @ (sK7 @ (sK7 @ sK5)))))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f234319])).
% 138.11/19.77 thf(f234559,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1097 | ~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(forward_demodulation,[],[f234320,f31586])).
% 138.11/19.77 thf(f234560,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((t @ (sK8 @ (sK1 @ (sK7 @ sK5)))))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1097 | ~spl9_1593 | ~spl9_2678)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f234559])).
% 138.11/19.77 thf(f234799,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1097 | ~spl9_1593 | ~spl9_1738 | ~spl9_2678)),
% 138.11/19.77 inference(forward_demodulation,[],[f234560,f55197])).
% 138.11/19.77 thf(f234800,plain,(
% 138.11/19.77 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X1))) | ($true = ((r @ X0))) | ($true = ((p @ X1)))) ) | (~spl9_997 | ~spl9_1097 | ~spl9_1593 | ~spl9_1738 | ~spl9_2678)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f234799])).
% 138.11/19.77 thf(f234978,plain,(
% 138.11/19.77 spl9_1344 | spl9_1087 | ~spl9_997 | ~spl9_1097 | ~spl9_1593 | ~spl9_1738 | ~spl9_2678),
% 138.11/19.77 inference(avatar_split_clause,[],[f234800,f112108,f55195,f48172,f31584,f29580,f31364,f38542])).
% 138.11/19.77 thf(f248513,plain,(
% 138.11/19.77 ($true = $false) | ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_976 | ~spl9_997 | ~spl9_1245)),
% 138.11/19.77 inference(forward_demodulation,[],[f165829,f29582])).
% 138.11/19.77 thf(f248514,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ (sK1 @ (sK7 @ sK5)))))) | ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_976 | ~spl9_997 | ~spl9_1245)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f248513])).
% 138.11/19.77 thf(f248796,plain,(
% 138.11/19.77 ($true = $false) | ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_486 | ~spl9_976 | ~spl9_997 | ~spl9_1245)),
% 138.11/19.77 inference(forward_demodulation,[],[f248514,f9650])).
% 138.11/19.77 thf(f258392,plain,(
% 138.11/19.77 ($false = ((r @ (sK3 @ (sK7 @ sK5))))) | (~spl9_486 | ~spl9_976 | ~spl9_997 | ~spl9_1245)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f248796])).
% 138.11/19.77 thf(f262206,plain,(
% 138.11/19.77 spl9_3053 | ~spl9_486 | ~spl9_976 | ~spl9_997 | ~spl9_1245),
% 138.11/19.77 inference(avatar_split_clause,[],[f258392,f35374,f29580,f29224,f9648,f139783])).
% 138.11/19.77 thf(f266595,plain,(
% 138.11/19.77 ($true = ((p @ (sK6 @ (sK6 @ sK5))))) | (~spl9_31 | spl9_1227 | ~spl9_1613)),
% 138.11/19.77 inference(forward_subsumption_resolution,[],[f58435,f34821])).
% 138.11/19.77 thf(f266799,plain,(
% 138.11/19.77 ($true = $false) | (~spl9_31 | ~spl9_52 | spl9_1227 | ~spl9_1613)),
% 138.11/19.77 inference(forward_demodulation,[],[f266595,f543])).
% 138.11/19.77 thf(f266800,plain,(
% 138.11/19.77 $false | (~spl9_31 | ~spl9_52 | spl9_1227 | ~spl9_1613)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f266799])).
% 138.11/19.77 thf(f266801,plain,(
% 138.11/19.77 ~spl9_31 | ~spl9_52 | spl9_1227 | ~spl9_1613),
% 138.11/19.77 inference(avatar_contradiction_clause,[],[f266800])).
% 138.11/19.77 thf(f429553,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ X0))) | ($true = ((r @ (sK3 @ (sK7 @ sK5)))))) ) | (~spl9_13 | ~spl9_1087)),
% 138.11/19.77 inference(constrained_superposition,[],[f235,f31365])).
% 138.11/19.77 thf(f429735,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($false = ((irel @ sK0 @ (sK7 @ sK5)))) | ($true = ((p @ X0))) | ($true = ((r @ (sK3 @ (sK7 @ sK5)))))) ) | (~spl9_13 | ~spl9_1087)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f429553])).
% 138.11/19.77 thf(f433987,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0))) | ($true = ((r @ (sK3 @ (sK7 @ sK5)))))) ) | (~spl9_13 | ~spl9_997 | ~spl9_1087)),
% 138.11/19.77 inference(forward_demodulation,[],[f429735,f29582])).
% 138.11/19.77 thf(f433988,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0))) | ($true = ((r @ (sK3 @ (sK7 @ sK5)))))) ) | (~spl9_13 | ~spl9_997 | ~spl9_1087)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f433987])).
% 138.11/19.77 thf(f434395,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_13 | ~spl9_997 | ~spl9_1087 | ~spl9_3053)),
% 138.11/19.77 inference(forward_demodulation,[],[f433988,f139785])).
% 138.11/19.77 thf(f434396,plain,(
% 138.11/19.77 ( ! [X0 : $i] : (($false = ((irel @ (sK1 @ (sK7 @ sK5)) @ X0))) | ($true = ((p @ X0)))) ) | (~spl9_13 | ~spl9_997 | ~spl9_1087 | ~spl9_3053)),
% 138.11/19.77 inference(trivial_inequality_removal,[],[f434395])).
% 138.11/19.77 thf(f434741,plain,(
% 138.11/19.77 spl9_1344 | ~spl9_13 | ~spl9_997 | ~spl9_1087 | ~spl9_3053),
% 138.11/19.77 inference(avatar_split_clause,[],[f434396,f139783,f31364,f29580,f234,f38542])).
% 138.11/19.77 cnf(s1, plain, spl9_3, inference(sat_conversion,[],[f202])).
% 138.11/19.77 cnf(s2, plain, spl9_7, inference(sat_conversion,[],[f215])).
% 138.11/19.77 cnf(s5, plain, spl9_13, inference(sat_conversion,[],[f236])).
% 138.11/19.77 cnf(s6, plain, spl9_15, inference(sat_conversion,[],[f243])).
% 138.11/19.77 cnf(s11, plain, spl9_22, inference(sat_conversion,[],[f270])).
% 138.11/19.77 cnf(s12, plain, spl9_25 | spl9_26, inference(sat_conversion,[],[f284])).
% 138.11/19.77 cnf(s13, plain, spl9_26 | spl9_28, inference(sat_conversion,[],[f291])).
% 138.11/19.77 cnf(s14, plain, spl9_31, inference(sat_conversion,[],[f301])).
% 138.11/19.77 cnf(s15, plain, spl9_35, inference(sat_conversion,[],[f314])).
% 138.11/19.77 cnf(s16, plain, spl9_37, inference(sat_conversion,[],[f321])).
% 138.11/19.77 cnf(s17, plain, spl9_38, inference(sat_conversion,[],[f325])).
% 138.11/19.77 cnf(s18, plain, spl9_41, inference(sat_conversion,[],[f335])).
% 138.11/19.77 cnf(s19, plain, spl9_42, inference(sat_conversion,[],[f339])).
% 138.11/19.77 cnf(s21, plain, spl9_46, inference(sat_conversion,[],[f354])).
% 138.11/19.77 cnf(s42, plain, ~spl9_26 | ~spl9_38, inference(sat_conversion,[],[f428])).
% 138.11/19.77 cnf(s66, plain, ~spl9_28 | ~spl9_42 | spl9_54, inference(sat_conversion,[],[f554])).
% 138.11/19.77 cnf(s74, plain, ~spl9_25 | ~spl9_28 | ~spl9_42 | spl9_52, inference(sat_conversion,[],[f576])).
% 138.11/19.77 cnf(s77, plain, ~spl9_28 | ~spl9_31 | spl9_51 | spl9_55, inference(sat_conversion,[],[f590])).
% 138.11/19.77 cnf(s328, plain, ~spl9_41 | ~spl9_46 | spl9_115, inference(sat_conversion,[],[f1881])).
% 138.11/19.77 cnf(s5658, plain, ~spl9_3 | ~spl9_37 | spl9_943, inference(sat_conversion,[],[f28668])).
% 138.11/19.77 cnf(s5740, plain, ~spl9_15 | ~spl9_25 | spl9_976, inference(sat_conversion,[],[f29226])).
% 138.11/19.77 cnf(s5746, plain, ~spl9_25 | ~spl9_42 | ~spl9_54 | ~spl9_55, inference(sat_conversion,[],[f29240])).
% 138.11/19.77 cnf(s5779, plain, ~spl9_22 | ~spl9_115 | spl9_992, inference(sat_conversion,[],[f29490])).
% 138.11/19.77 cnf(s5800, plain, ~spl9_31 | spl9_55 | ~spl9_992 | spl9_997, inference(sat_conversion,[],[f29588])).
% 138.11/19.77 cnf(s5853, plain, ~spl9_25 | ~spl9_42 | ~spl9_1023, inference(sat_conversion,[],[f30031])).
% 138.11/19.77 cnf(s5953, plain, ~spl9_31 | spl9_55 | ~spl9_1072, inference(sat_conversion,[],[f31012])).
% 138.11/19.77 cnf(s5992, plain, ~spl9_25 | ~spl9_51 | ~spl9_1070 | spl9_1072, inference(sat_conversion,[],[f31423])).
% 138.11/19.77 cnf(s6221, plain, ~spl9_115 | ~spl9_1227 | spl9_1229, inference(sat_conversion,[],[f34843])).
% 138.11/19.77 cnf(s6256, plain, ~spl9_31 | spl9_1070 | ~spl9_1229 | spl9_1243, inference(sat_conversion,[],[f35364])).
% 138.11/19.77 cnf(s6258, plain, ~spl9_3 | ~spl9_997 | ~spl9_1229 | spl9_1245, inference(sat_conversion,[],[f35377])).
% 138.11/19.77 cnf(s6261, plain, ~spl9_115 | ~spl9_1243 | spl9_1246, inference(sat_conversion,[],[f35417])).
% 138.11/19.77 cnf(s6263, plain, ~spl9_28 | spl9_1097 | ~spl9_1243, inference(sat_conversion,[],[f35422])).
% 138.11/19.77 cnf(s6271, plain, ~spl9_28 | spl9_486 | ~spl9_1245, inference(sat_conversion,[],[f35516])).
% 138.11/19.77 cnf(s6276, plain, ~spl9_7 | ~spl9_35 | spl9_1256, inference(sat_conversion,[],[f35698])).
% 138.11/19.77 cnf(s6533, plain, ~spl9_25 | ~spl9_486 | ~spl9_1245 | ~spl9_1344, inference(sat_conversion,[],[f39266])).
% 138.11/19.77 cnf(s7003, plain, ~spl9_25 | ~spl9_1243 | ~spl9_1246 | spl9_1593, inference(sat_conversion,[],[f48175])).
% 138.11/19.77 cnf(s7054, plain, ~spl9_115 | ~spl9_1603 | spl9_1619, inference(sat_conversion,[],[f48642])).
% 138.11/19.77 cnf(s7256, plain, ~spl9_25 | ~spl9_42 | spl9_1603, inference(sat_conversion,[],[f53731])).
% 138.11/19.77 cnf(s7385, plain, ~spl9_943 | ~spl9_997 | spl9_1087 | ~spl9_1097 | ~spl9_1593 | spl9_1738, inference(sat_conversion,[],[f55221])).
% 138.11/19.77 cnf(s7420, plain, ~spl9_25 | spl9_1023 | spl9_1613 | ~spl9_1619, inference(sat_conversion,[],[f57966])).
% 138.11/19.77 cnf(s9624, plain, ~spl9_3 | ~spl9_1256 | spl9_2678, inference(sat_conversion,[],[f112110])).
% 138.11/19.77 cnf(s14335, plain, ~spl9_997 | spl9_1087 | ~spl9_1097 | spl9_1344 | ~spl9_1593 | ~spl9_1738 | ~spl9_2678, inference(sat_conversion,[],[f234978])).
% 138.11/19.77 cnf(s17166, plain, ~spl9_486 | ~spl9_976 | ~spl9_997 | ~spl9_1245 | spl9_3053, inference(sat_conversion,[],[f262206])).
% 138.11/19.77 cnf(s18017, plain, ~spl9_31 | ~spl9_52 | spl9_1227 | ~spl9_1613, inference(sat_conversion,[],[f266801])).
% 138.11/19.77 cnf(s25867, plain, ~spl9_13 | ~spl9_997 | ~spl9_1087 | spl9_1344 | ~spl9_3053, inference(sat_conversion,[],[f434741])).
% 138.11/19.77 cnf(s26345, plain, spl9_115, inference(rat,[],[s328,s21,s18])).
% 138.11/19.77 cnf(s26347, plain, ~spl9_26, inference(rat,[],[s42,s17])).
% 138.11/19.77 cnf(s26360, plain, spl9_28, inference(rat,[],[s13,s26347])).
% 138.11/19.77 cnf(s26361, plain, spl9_54, inference(rat,[],[s66,s19,s26360])).
% 138.11/19.77 cnf(s26366, plain, spl9_25, inference(rat,[],[s12,s26347])).
% 138.11/19.77 cnf(s26367, plain, spl9_1603, inference(rat,[],[s7256,s19,s26366])).
% 138.11/19.77 cnf(s26368, plain, ~spl9_1023, inference(rat,[],[s5853,s19,s26366])).
% 138.11/19.77 cnf(s26372, plain, ~spl9_55, inference(rat,[],[s5746,s26361,s19,s26366])).
% 138.11/19.77 cnf(s26375, plain, spl9_52, inference(rat,[],[s74,s26360,s19,s26366])).
% 138.11/19.77 cnf(s26377, plain, spl9_1619, inference(rat,[],[s7054,s26345,s26367])).
% 138.11/19.77 cnf(s26378, plain, spl9_1613, inference(rat,[],[s7420,s26377,s26366,s26368])).
% 138.11/19.77 cnf(s26381, plain, ~spl9_1072, inference(rat,[],[s5953,s14,s26372])).
% 138.11/19.77 cnf(s26383, plain, spl9_51, inference(rat,[],[s77,s26360,s14,s26372])).
% 138.11/19.77 cnf(s26385, plain, spl9_1227, inference(rat,[],[s18017,s26378,s14,s26375])).
% 138.11/19.77 cnf(s26394, plain, ~spl9_1070, inference(rat,[],[s5992,s26381,s26366,s26383])).
% 138.11/19.77 cnf(s26397, plain, spl9_1229, inference(rat,[],[s6221,s26345,s26385])).
% 138.11/19.77 cnf(s26406, plain, spl9_1243, inference(rat,[],[s6256,s26394,s14,s26397])).
% 138.11/19.77 cnf(s26418, plain, spl9_1246, inference(rat,[],[s6261,s26345,s26406])).
% 138.11/19.77 cnf(s26419, plain, spl9_1097, inference(rat,[],[s6263,s26360,s26406])).
% 138.11/19.77 cnf(s26430, plain, spl9_1593, inference(rat,[],[s7003,s26406,s26366,s26418])).
% 138.11/19.77 cnf(s26461, plain, spl9_992, inference(rat,[],[s5779,s26345,s11])).
% 138.11/19.77 cnf(s26465, plain, spl9_997, inference(rat,[],[s5800,s26372,s14,s26461])).
% 138.11/19.77 cnf(s26551, plain, spl9_976, inference(rat,[],[s5740,s26366,s6])).
% 138.11/19.77 cnf(s26578, plain, spl9_1256, inference(rat,[],[s6276,s15,s2])).
% 138.11/19.77 cnf(s26603, plain, spl9_2678, inference(rat,[],[s9624,s26578,s1])).
% 138.11/19.77 cnf(s26616, plain, spl9_1245, inference(rat,[],[s6258,s26465,s26397,s1])).
% 138.11/19.77 cnf(s26626, plain, spl9_943, inference(rat,[],[s5658,s16,s1])).
% 138.11/19.77 cnf(s26665, plain, spl9_486, inference(rat,[],[s6271,s26360,s26616])).
% 138.11/19.77 cnf(s26700, plain, spl9_3053, inference(rat,[],[s17166,s26616,s26551,s26465,s26665])).
% 138.11/19.77 cnf(s26704, plain, ~spl9_1344, inference(rat,[],[s6533,s26616,s26366,s26665])).
% 138.11/19.77 cnf(s26750, plain, ~spl9_1087, inference(rat,[],[s25867,s26700,s5,s26465,s26704])).
% 138.11/19.77 cnf(s26813, plain, ~spl9_1738, inference(rat,[],[s14335,s26603,s26704,s26430,s26465,s26419,s26750])).
% 138.11/19.77 cnf(s26814, plain, $false, inference(rat,[],[s7385,s26626,s26430,s26419,s26465,s26813,s26750])).
% 138.11/19.77 thf(f435013,plain,(
% 138.11/19.77 $false),
% 138.11/19.77 inference(avatar_sat_refutation,[],[s26814])).
% 138.11/19.77 % SZS output end Proof for theBenchmark
% 138.11/19.77 % (297254)------------------------------
% 138.11/19.77 % (297254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.11/19.77 % (297254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.11/19.77 % (297254)CaDiCaL version: 2.1.3
% 138.11/19.77 % (297254)Termination reason: Refutation
% 138.11/19.77 % (297254)Time elapsed: 8.257 s
% 138.11/19.77 % (297254)Peak memory usage: 113 MB
% 138.11/19.77 % (297254)Instructions burned: 35360 (million)
% 138.11/19.77 % (297157)Success in time 19.533 s
% 138.11/19.77 % Vampire exiting
%------------------------------------------------------------------------------