%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO444^1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:49:59 AM UTC 2026
% Result : Theorem 8.92s 2.40s
% Output : Refutation 8.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO444^1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n017.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Sep 29 16:47:22 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 Running first-order model finding
% 0.07/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.47/0.85 % (595427)Will run a generic schedule for satisfiability detection.
% 3.47/0.85 % (595434)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1484012113:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.47/0.85 % (595433)% WARNING: option uhcvi not known.
% 3.47/0.85 % (595433)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2058252056:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.47/0.85 % (595435)dis+10_1_sil=32000:sp=arity:random_seed=1471668805:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.47/0.85 % (595436)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1018892142:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.47/0.85 % (595438)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2403826765:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.47/0.85 % (595437)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3048807266:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.47/0.85 % (595433)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.47/0.85 % (595436)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.47/0.85 % (595433)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.47/0.85 % (595432)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3772214582_2999 on theBenchmark for (2999ds/0Mi)
% 3.47/0.85 % Exception at run slice level
% 3.47/0.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.47/0.85 % (595435)Instruction limit reached!
% 3.47/0.85 % (595435)------------------------------
% 3.47/0.85 % (595435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.85 % (595435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.85 % (595435)CaDiCaL version: 2.1.3
% 3.47/0.85 % (595435)Termination reason: Instruction limit
% 3.47/0.85 % (595435)Termination phase: Saturation
% 3.47/0.85 % (595435)Time elapsed: 0.048 s
% 3.47/0.85 % (595435)Peak memory usage: 12 MB
% 3.47/0.85 % (595435)Instructions burned: 103 (million)
% 3.47/0.85 % (595446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1534755106:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.47/0.85 % Exception at run slice level
% 3.47/0.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.47/0.85 % (595436)Instruction limit reached!
% 3.47/0.85 % (595436)------------------------------
% 3.47/0.85 % (595436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.85 % (595436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.85 % (595436)CaDiCaL version: 2.1.3
% 3.47/0.85 % (595436)Termination reason: Instruction limit
% 3.47/0.85 % (595436)Termination phase: Saturation
% 3.47/0.85 % (595436)Time elapsed: 0.053 s
% 3.47/0.85 % (595436)Peak memory usage: 12 MB
% 3.47/0.85 % (595436)Instructions burned: 116 (million)
% 3.47/0.85 % (595437)Instruction limit reached!
% 3.47/0.85 % (595437)------------------------------
% 3.47/0.85 % (595437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.85 % (595437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.85 % (595437)CaDiCaL version: 2.1.3
% 3.47/0.85 % (595437)Termination reason: Instruction limit
% 3.47/0.85 % (595437)Termination phase: Saturation
% 3.47/0.85 % (595437)Time elapsed: 0.061 s
% 3.47/0.85 % (595437)Peak memory usage: 12 MB
% 3.47/0.85 % (595437)Instructions burned: 133 (million)
% 3.47/0.85 % (595449)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=1828875284:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.47/0.85 % (595449)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.47/0.85 % (595449)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.47/0.85 % (595447)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1061710676:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.47/0.85 % (595450)ott-21_1_sil=16000:fs=off:random_seed=2047394522:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.47/0.85 % (595451)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4220360070:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 8.92/2.40 % (595438)Instruction limit reached!
% 8.92/2.40 % (595438)------------------------------
% 8.92/2.40 % (595438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595438)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595438)Termination reason: Instruction limit
% 8.92/2.40 % (595438)Termination phase: Saturation
% 8.92/2.40 % (595438)Time elapsed: 0.085 s
% 8.92/2.40 % (595438)Peak memory usage: 12 MB
% 8.92/2.40 % (595438)Instructions burned: 159 (million)
% 8.92/2.40 % (595456)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1229504599:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595458)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=605978677:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 8.92/2.40 % (595447)Instruction limit reached!
% 8.92/2.40 % (595447)------------------------------
% 8.92/2.40 % (595447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595447)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595447)Termination reason: Instruction limit
% 8.92/2.40 % (595447)Termination phase: Saturation
% 8.92/2.40 % (595447)Time elapsed: 0.061 s
% 8.92/2.40 % (595447)Peak memory usage: 12 MB
% 8.92/2.40 % (595447)Instructions burned: 132 (million)
% 8.92/2.40 % (595450)Instruction limit reached!
% 8.92/2.40 % (595450)------------------------------
% 8.92/2.40 % (595450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595450)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595450)Termination reason: Instruction limit
% 8.92/2.40 % (595450)Termination phase: Saturation
% 8.92/2.40 % (595450)Time elapsed: 0.080 s
% 8.92/2.40 % (595450)Peak memory usage: 12 MB
% 8.92/2.40 % (595450)Instructions burned: 181 (million)
% 8.92/2.40 % (595460)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=337514002:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595461)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=644707708: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)
% 8.92/2.40 % (595461)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.92/2.40 % (595463)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1645971373:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 8.92/2.40 % (595463)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.92/2.40 % (595449)Instruction limit reached!
% 8.92/2.40 % (595449)------------------------------
% 8.92/2.40 % (595449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595449)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595449)Termination reason: Instruction limit
% 8.92/2.40 % (595449)Termination phase: Saturation
% 8.92/2.40 % (595449)Time elapsed: 0.218 s
% 8.92/2.40 % (595449)Peak memory usage: 14 MB
% 8.92/2.40 % (595449)Instructions burned: 684 (million)
% 8.92/2.40 % (595451)Instruction limit reached!
% 8.92/2.40 % (595451)------------------------------
% 8.92/2.40 % (595451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595451)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595451)Termination reason: Instruction limit
% 8.92/2.40 % (595451)Termination phase: Saturation
% 8.92/2.40 % (595451)Time elapsed: 0.215 s
% 8.92/2.40 % (595451)Peak memory usage: 13 MB
% 8.92/2.40 % (595451)Instructions burned: 479 (million)
% 8.92/2.40 % (595504)fmb+10_1_sil=64000:random_seed=1222559412:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 8.92/2.40 % (595504)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595513)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2462947873:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595518)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4274057168:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595531)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1651445002:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 8.92/2.40 % (595531)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.92/2.40 % (595533)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2120439288:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 8.92/2.40 % (595533)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 8.92/2.40 % (595533)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 8.92/2.40 % (595458)Instruction limit reached!
% 8.92/2.40 % (595458)------------------------------
% 8.92/2.40 % (595458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595458)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595458)Termination reason: Instruction limit
% 8.92/2.40 % (595458)Termination phase: Saturation
% 8.92/2.40 % (595458)Time elapsed: 0.272 s
% 8.92/2.40 % (595458)Peak memory usage: 12 MB
% 8.92/2.40 % (595458)Instructions burned: 1181 (million)
% 8.92/2.40 % (595559)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1577089298:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595568)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1125294570:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595583)ott-2_1_sil=16000:newcnf=on:random_seed=2639905593:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 8.92/2.40 % (595583)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.92/2.40 % (595461)Instruction limit reached!
% 8.92/2.40 % (595461)------------------------------
% 8.92/2.40 % (595461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595461)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595461)Termination reason: Instruction limit
% 8.92/2.40 % (595461)Termination phase: Saturation
% 8.92/2.40 % (595461)Time elapsed: 0.302 s
% 8.92/2.40 % (595461)Peak memory usage: 15 MB
% 8.92/2.40 % (595461)Instructions burned: 692 (million)
% 8.92/2.40 % (595587)ott+10_1_sil=32000:tgt=ground:random_seed=4008918857:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 8.92/2.40 % (595463)Instruction limit reached!
% 8.92/2.40 % (595463)------------------------------
% 8.92/2.40 % (595463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595463)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595463)Termination reason: Instruction limit
% 8.92/2.40 % (595463)Termination phase: Saturation
% 8.92/2.40 % (595463)Time elapsed: 0.379 s
% 8.92/2.40 % (595463)Peak memory usage: 13 MB
% 8.92/2.40 % (595463)Instructions burned: 880 (million)
% 8.92/2.40 % (595607)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1764210560:i=54282_2994 on theBenchmark for (2994ds/54282Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595613)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4151238857:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 8.92/2.40 % (595613)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 8.92/2.40 % (595583)Instruction limit reached!
% 8.92/2.40 % (595583)------------------------------
% 8.92/2.40 % (595583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595583)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595583)Termination reason: Instruction limit
% 8.92/2.40 % (595583)Termination phase: Saturation
% 8.92/2.40 % (595583)Time elapsed: 0.263 s
% 8.92/2.40 % (595583)Peak memory usage: 14 MB
% 8.92/2.40 % (595583)Instructions burned: 871 (million)
% 8.92/2.40 % (595652)dis+21_1_sil=32000:sas=cadical:random_seed=2949092050:i=3773:amm=off_2992 on theBenchmark for (2992ds/3773Mi)
% 8.92/2.40 % (595533)Instruction limit reached!
% 8.92/2.40 % (595533)------------------------------
% 8.92/2.40 % (595533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595533)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595533)Termination reason: Instruction limit
% 8.92/2.40 % (595533)Termination phase: Saturation
% 8.92/2.40 % (595533)Time elapsed: 0.807 s
% 8.92/2.40 % (595533)Peak memory usage: 19 MB
% 8.92/2.40 % (595533)Instructions burned: 1474 (million)
% 8.92/2.40 % (595763)ott+11_1_sil=16000:gs=on:random_seed=2608807286:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 8.92/2.40 % (595763)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 8.92/2.40 % (595652)Instruction limit reached!
% 8.92/2.40 % (595652)------------------------------
% 8.92/2.40 % (595652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595652)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595652)Termination reason: Instruction limit
% 8.92/2.40 % (595652)Termination phase: Saturation
% 8.92/2.40 % (595652)Time elapsed: 0.790 s
% 8.92/2.40 % (595652)Peak memory usage: 17 MB
% 8.92/2.40 % (595652)Instructions burned: 3779 (million)
% 8.92/2.40 % (595812)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1426503059:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 8.92/2.40 % Exception at run slice level
% 8.92/2.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.92/2.40 % (595814)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2722976116:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi)
% 8.92/2.40 % (595763)Instruction limit reached!
% 8.92/2.40 % (595763)------------------------------
% 8.92/2.40 % (595763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595763)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595763)Termination reason: Instruction limit
% 8.92/2.40 % (595763)Termination phase: Saturation
% 8.92/2.40 % (595763)Time elapsed: 0.843 s
% 8.92/2.40 % (595763)Peak memory usage: 13 MB
% 8.92/2.40 % (595763)Instructions burned: 2253 (million)
% 8.92/2.40 % (595816)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3902706448:i=29340_2979 on theBenchmark for (2979ds/29340Mi)
% 8.92/2.40 % (595613)Instruction limit reached!
% 8.92/2.40 % (595613)------------------------------
% 8.92/2.40 % (595613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.40 % (595613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.40 % (595613)CaDiCaL version: 2.1.3
% 8.92/2.40 % (595613)Termination reason: Instruction limit
% 8.92/2.40 % (595613)Termination phase: Saturation
% 8.92/2.40 % (595613)Time elapsed: 1.439 s
% 8.92/2.40 % (595613)Peak memory usage: 16 MB
% 8.92/2.40 % (595613)Instructions burned: 3513 (million)
% 8.92/2.40 % (595818)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3776909804:i=5211_2979 on theBenchmark for (2979ds/5211Mi)
% 8.92/2.40 % (595814) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-595427-595814"...
% 8.92/2.40 % (595814)...printing done.
% 8.92/2.40 % (595814)Refutation found. Thanks to Tanya!
% 8.92/2.40 % SZS status Theorem for theBenchmark
% 8.92/2.40 % SZS output start Proof for theBenchmark
% 8.92/2.40 thf(type_def_5, type, mu: $tType).
% 8.92/2.40 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 8.92/2.40 thf(func_def_0, type, meq_ind: (mu > mu > $i > $o)).
% 8.92/2.40 thf(func_def_1, type, meq_prop: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_3, type, mnot: (($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_4, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_5, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_6, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_7, type, mimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_8, type, mequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_9, type, mxor: (($i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_10, type, mforall_ind: ((mu > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_11, type, mforall_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_12, type, mexists_ind: ((mu > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_13, type, mexists_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_14, type, mtrue: ($i > $o)).
% 8.92/2.40 thf(func_def_15, type, mfalse: ($i > $o)).
% 8.92/2.40 thf(func_def_16, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_17, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_18, type, mreflexive: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_19, type, msymmetric: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_20, type, mserial: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_21, type, mtransitive: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_22, type, meuclidean: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_23, type, mpartially_functional: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_24, type, mfunctional: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_25, type, mweakly_dense: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_26, type, mweakly_connected: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_27, type, mweakly_directed: (($i > $i > $o) > $o)).
% 8.92/2.40 thf(func_def_28, type, mvalid: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_29, type, minvalid: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_30, type, msatisfiable: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_31, type, mcountersatisfiable: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_32, type, rel_s5: ($i > $i > $o)).
% 8.92/2.40 thf(func_def_33, type, mbox_s5: (($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_34, type, mdia_s5: (($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_35, type, p: ($i > $o)).
% 8.92/2.40 thf(func_def_36, type, q: ($i > $o)).
% 8.92/2.40 thf(func_def_37, type, db2: !>[X0: $tType]:(X0)).
% 8.92/2.40 thf(func_def_38, type, db1: !>[X0: $tType]:(X0)).
% 8.92/2.40 thf(func_def_39, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 8.92/2.40 thf(func_def_40, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 8.92/2.40 thf(func_def_41, type, db0: !>[X0: $tType]:(X0)).
% 8.92/2.40 thf(func_def_42, type, vNOT: ($o > $o)).
% 8.92/2.40 thf(func_def_43, type, vOR: ($o > $o > $o)).
% 8.92/2.40 thf(func_def_44, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.92/2.40 thf(func_def_47, type, db3: !>[X0: $tType]:(X0)).
% 8.92/2.40 thf(func_def_48, type, vIMP: ($o > $o > $o)).
% 8.92/2.40 thf(func_def_49, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.92/2.40 thf(func_def_50, type, vAND: ($o > $o > $o)).
% 8.92/2.40 thf(func_def_51, type, db4: !>[X0: $tType]:(X0)).
% 8.92/2.40 thf(func_def_52, type, sP0: ($o > $o)).
% 8.92/2.40 thf(func_def_53, type, sF1: $o).
% 8.92/2.40 thf(func_def_54, type, sF2: $o).
% 8.92/2.40 thf(func_def_55, type, sF3: $o).
% 8.92/2.40 thf(func_def_58, type, sK6: ($i > $i)).
% 8.92/2.40 thf(func_def_59, type, sK7: ($i > $i)).
% 8.92/2.40 thf(func_def_62, type, sK10: ($i > $i)).
% 8.92/2.40 thf(func_def_63, type, sK11: ($i > $i)).
% 8.92/2.40 thf(func_def_64, type, sK12: ($i > $i)).
% 8.92/2.40 thf(func_def_66, type, sK14: ($i > $i)).
% 8.92/2.40 thf(func_def_67, type, sK15: ($i > $i)).
% 8.92/2.40 thf(func_def_68, type, sK16: ($i > $i)).
% 8.92/2.40 thf(func_def_69, type, sK17: ($i > $i)).
% 8.92/2.40 thf(func_def_70, type, sK18: ($i > $i)).
% 8.92/2.40 thf(func_def_71, type, sF19: ($i > $i > $o)).
% 8.92/2.40 thf(func_def_73, type, sF21: ($o > $o)).
% 8.92/2.40 thf(func_def_74, type, sF22: (($o > $o) > $o > $o)).
% 8.92/2.40 thf(func_def_75, type, sF23: ($i > ($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_76, type, sF24: !>[X0: $tType]:((X0 > (X0 > $i > $o) > $i > $o))).
% 8.92/2.40 thf(func_def_77, type, sF25: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_78, type, sF26: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_79, type, sF27: (($i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_80, type, sF28: !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 8.92/2.40 thf(func_def_81, type, sF29: ($o > $o)).
% 8.92/2.40 thf(func_def_82, type, sF30: ($i > $o)).
% 8.92/2.40 thf(func_def_83, type, sF31: ($i > $o)).
% 8.92/2.40 thf(func_def_84, type, sF32: ($i > $i > $o)).
% 8.92/2.40 thf(func_def_85, type, sF33: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_86, type, sF34: !>[X0: $tType]:(($i > ($i > X0) > X0))).
% 8.92/2.40 thf(func_def_87, type, sF35: ($i > $o)).
% 8.92/2.40 thf(func_def_88, type, sF36: ($i > $o)).
% 8.92/2.40 thf(func_def_89, type, sF37: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_90, type, sF38: (($o > $o) > $o)).
% 8.92/2.40 thf(func_def_91, type, sF39: !>[X0: $tType, X1: $tType]:((X0 > $i > ($i > X0 > X1) > X1))).
% 8.92/2.40 thf(func_def_92, type, sF40: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_93, type, sF41: !>[X0: $tType]:((($i > X0) > X0))).
% 8.92/2.40 thf(func_def_94, type, sF42: ($i > $o)).
% 8.92/2.40 thf(func_def_95, type, sF43: ($i > $o)).
% 8.92/2.40 thf(func_def_96, type, sF44: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_97, type, sF45: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > X0 > X1 > X2))).
% 8.92/2.40 thf(func_def_98, type, sF46: ($i > $o)).
% 8.92/2.40 thf(func_def_99, type, sF47: ($i > $o)).
% 8.92/2.40 thf(func_def_100, type, sF48: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_101, type, sF49: ($i > $o)).
% 8.92/2.40 thf(func_def_102, type, sF50: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_103, type, sF51: ($i > $o)).
% 8.92/2.40 thf(func_def_104, type, sF52: ($i > $o)).
% 8.92/2.40 thf(func_def_105, type, sF53: ($i > $o)).
% 8.92/2.40 thf(func_def_106, type, sF54: ($i > $o)).
% 8.92/2.40 thf(func_def_107, type, sF55: (($i > $i) > $i > $i)).
% 8.92/2.40 thf(func_def_108, type, sF56: ($i > $o)).
% 8.92/2.40 thf(func_def_109, type, sF57: ($i > $o)).
% 8.92/2.40 thf(func_def_110, type, sF58: !>[X0: $tType]:((($i > X0) > X0))).
% 8.92/2.40 thf(func_def_111, type, sF59: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_112, type, sF60: (($i > $o) > $o)).
% 8.92/2.40 thf(func_def_113, type, sF61: !>[X0: $tType]:((($i > X0) > (($i > X0) > X0) > X0))).
% 8.92/2.40 thf(func_def_114, type, sF62: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X1) > (X0 > X1) > X1))).
% 8.92/2.40 thf(func_def_115, type, sF63: ($i > $o)).
% 8.92/2.40 thf(func_def_116, type, sF64: (($i > $i > $o) > $i > $o)).
% 8.92/2.40 thf(func_def_117, type, sF65: ($i > $o)).
% 8.92/2.40 thf(func_def_118, type, sF66: ($i > $o)).
% 8.92/2.40 thf(func_def_119, type, sF67: ($i > $o)).
% 8.92/2.40 thf(func_def_120, type, sF68: ($i > $o)).
% 8.92/2.40 thf(func_def_121, type, sF69: !>[X0: $tType]:((($i > X0) > X0))).
% 8.92/2.40 thf(func_def_122, type, sF70: ($i > $o)).
% 8.92/2.40 thf(func_def_123, type, sF71: ($i > $o)).
% 8.92/2.40 thf(func_def_124, type, sF72: ($i > $o)).
% 8.92/2.40 thf(func_def_125, type, sF73: !>[X0: $tType]:((($i > X0) > X0))).
% 8.92/2.40 thf(f3,axiom,(
% 8.92/2.40 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mnot)).
% 8.92/2.40 thf(f4,axiom,(
% 8.92/2.40 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mor)).
% 8.92/2.40 thf(f5,axiom,(
% 8.92/2.40 (mand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mnot @ (mor @ (mnot @ X0) @ (mnot @ X1))))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mand)).
% 8.92/2.40 thf(f6,axiom,(
% 8.92/2.40 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mimplies)).
% 8.92/2.40 thf(f8,axiom,(
% 8.92/2.40 (mequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ (mimplies @ X0 @ X1) @ (mimplies @ X1 @ X0)))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mequiv)).
% 8.92/2.40 thf(f18,axiom,(
% 8.92/2.40 (mreflexive = (^[X0 : ($i > $i > $o)] : (! [X1 : $i] : (X0 @ X1 @ X1))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mreflexive)).
% 8.92/2.40 thf(f19,axiom,(
% 8.92/2.40 (msymmetric = (^[X0 : ($i > $i > $o)] : (! [X1 : $i,X2 : $i] : ((X0 @ X1 @ X2) => (X0 @ X2 @ X1)))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',msymmetric)).
% 8.92/2.40 thf(f21,axiom,(
% 8.92/2.40 (mtransitive = (^[X0 : ($i > $i > $o)] : (! [X1 : $i,X2 : $i,X3 : $i] : (((X0 @ X2 @ X3) & (X0 @ X1 @ X2)) => (X0 @ X1 @ X3)))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mtransitive)).
% 8.92/2.40 thf(f28,axiom,(
% 8.92/2.40 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mvalid)).
% 8.92/2.40 thf(f32,axiom,(
% 8.92/2.40 (mbox_s5 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((X0 @ X2) | ~(rel_s5 @ X1 @ X2)))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^6.ax',mbox_s5)).
% 8.92/2.40 thf(f33,axiom,(
% 8.92/2.40 (mdia_s5 = (^[X0 : ($i > $o)] : ((mnot @ (mbox_s5 @ (mnot @ X0))))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^6.ax',mdia_s5)).
% 8.92/2.40 thf(f34,axiom,(
% 8.92/2.40 (mreflexive @ rel_s5)),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^6.ax',a1)).
% 8.92/2.40 thf(f35,axiom,(
% 8.92/2.40 (mtransitive @ rel_s5)),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^6.ax',a2)).
% 8.92/2.40 thf(f36,axiom,(
% 8.92/2.40 (msymmetric @ rel_s5)),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/Axioms/LCL013^6.ax',a3)).
% 8.92/2.40 thf(f37,conjecture,(
% 8.92/2.40 (mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))),
% 8.92/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove)).
% 8.92/2.40 thf(f38,negated_conjecture,(
% 8.92/2.40 ~(mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))),
% 8.92/2.40 inference(negated_conjecture,[status(cth)],[f37])).
% 8.92/2.40 thf(f41,plain,(
% 8.92/2.40 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 8.92/2.40 inference(rectify,[],[f3])).
% 8.92/2.40 thf(f42,plain,(
% 8.92/2.40 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 8.92/2.40 inference(fool_elimination,[],[f41])).
% 8.92/2.40 thf(f43,plain,(
% 8.92/2.40 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 8.92/2.40 inference(rectify,[],[f4])).
% 8.92/2.40 thf(f44,plain,(
% 8.92/2.40 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 8.92/2.40 inference(fool_elimination,[],[f43])).
% 8.92/2.40 thf(f45,plain,(
% 8.92/2.40 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mnot @ (mor @ (mnot @ Y0) @ (mnot @ Y1)))))))),
% 8.92/2.40 inference(fool_elimination,[],[f5])).
% 8.92/2.40 thf(f46,plain,(
% 8.92/2.40 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 8.92/2.40 inference(fool_elimination,[],[f6])).
% 8.92/2.40 thf(f48,plain,(
% 8.92/2.40 (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 8.92/2.40 inference(fool_elimination,[],[f8])).
% 8.92/2.40 thf(f62,plain,(
% 8.92/2.40 (mreflexive = (^[X0 : ($i > $i > $o)] : (! [X1 : $i] : (X0 @ X1 @ X1))))),
% 8.92/2.40 inference(rectify,[],[f18])).
% 8.92/2.40 thf(f63,plain,(
% 8.92/2.40 (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1)))))),
% 8.92/2.40 inference(fool_elimination,[],[f62])).
% 8.92/2.40 thf(f64,plain,(
% 8.92/2.40 (msymmetric = (^[X0 : ($i > $i > $o)] : (! [X1 : $i,X2 : $i] : ((X0 @ X1 @ X2) => (X0 @ X2 @ X1)))))),
% 8.92/2.40 inference(rectify,[],[f19])).
% 8.92/2.40 thf(f65,plain,(
% 8.92/2.40 (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2))))))))),
% 8.92/2.40 inference(fool_elimination,[],[f64])).
% 8.92/2.40 thf(f68,plain,(
% 8.92/2.40 (mtransitive = (^[X0 : ($i > $i > $o)] : (! [X1 : $i,X2 : $i,X3 : $i] : (((X0 @ X2 @ X3) & (X0 @ X1 @ X2)) => (X0 @ X1 @ X3)))))),
% 8.92/2.40 inference(rectify,[],[f21])).
% 8.92/2.40 thf(f69,plain,(
% 8.92/2.40 (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) & (Y0 @ Y2 @ Y1)) => (Y0 @ Y3 @ Y1))))))))))),
% 8.92/2.40 inference(fool_elimination,[],[f68])).
% 8.92/2.40 thf(f82,plain,(
% 8.92/2.40 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 8.92/2.40 inference(rectify,[],[f28])).
% 8.92/2.40 thf(f83,plain,(
% 8.92/2.40 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 8.92/2.40 inference(fool_elimination,[],[f82])).
% 8.92/2.40 thf(f90,plain,(
% 8.92/2.40 (mbox_s5 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((X0 @ X2) | ~(rel_s5 @ X1 @ X2)))))),
% 8.92/2.40 inference(rectify,[],[f32])).
% 8.92/2.40 thf(f91,plain,(
% 8.92/2.40 (mbox_s5 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))))),
% 8.92/2.40 inference(fool_elimination,[],[f90])).
% 8.92/2.40 thf(f92,plain,(
% 8.92/2.40 (mdia_s5 = (^[Y0 : $i > $o]: (mnot @ (mbox_s5 @ (mnot @ Y0)))))),
% 8.92/2.40 inference(fool_elimination,[],[f33])).
% 8.92/2.40 thf(f93,plain,(
% 8.92/2.40 (mreflexive @ rel_s5)),
% 8.92/2.40 inference(rectify,[],[f34])).
% 8.92/2.40 thf(f94,plain,(
% 8.92/2.40 (((mreflexive @ rel_s5)) = $true)),
% 8.92/2.40 inference(fool_elimination,[],[f93])).
% 8.92/2.40 thf(f95,plain,(
% 8.92/2.40 (mtransitive @ rel_s5)),
% 8.92/2.40 inference(rectify,[],[f35])).
% 8.92/2.40 thf(f96,plain,(
% 8.92/2.40 (((mtransitive @ rel_s5)) = $true)),
% 8.92/2.40 inference(fool_elimination,[],[f95])).
% 8.92/2.40 thf(f97,plain,(
% 8.92/2.40 (msymmetric @ rel_s5)),
% 8.92/2.40 inference(rectify,[],[f36])).
% 8.92/2.40 thf(f98,plain,(
% 8.92/2.40 (((msymmetric @ rel_s5)) = $true)),
% 8.92/2.40 inference(fool_elimination,[],[f97])).
% 8.92/2.40 thf(f99,plain,(
% 8.92/2.40 ~(mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))),
% 8.92/2.40 inference(rectify,[],[f38])).
% 8.92/2.40 thf(f100,plain,(
% 8.92/2.40 ~ (((mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))) = $true)),
% 8.92/2.40 inference(fool_elimination,[],[f99])).
% 8.92/2.40 thf(f101,plain,(
% 8.92/2.40 (((mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))) != $true)),
% 8.92/2.40 inference(flattening,[],[f100])).
% 8.92/2.40 thf(f104,plain,(
% 8.92/2.40 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f42])).
% 8.92/2.40 thf(f105,plain,(
% 8.92/2.40 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f44])).
% 8.92/2.40 thf(f106,plain,(
% 8.92/2.40 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mnot @ (mor @ (mnot @ Y0) @ (mnot @ Y1)))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f45])).
% 8.92/2.40 thf(f107,plain,(
% 8.92/2.40 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 8.92/2.40 inference(cnf_transformation,[],[f46])).
% 8.92/2.40 thf(f109,plain,(
% 8.92/2.40 (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ (mimplies @ Y0 @ Y1) @ (mimplies @ Y1 @ Y0))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f48])).
% 8.92/2.40 thf(f119,plain,(
% 8.92/2.40 (mreflexive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1)))))),
% 8.92/2.40 inference(cnf_transformation,[],[f63])).
% 8.92/2.40 thf(f120,plain,(
% 8.92/2.40 (msymmetric = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2))))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f65])).
% 8.92/2.40 thf(f122,plain,(
% 8.92/2.40 (mtransitive = (^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) & (Y0 @ Y2 @ Y1)) => (Y0 @ Y3 @ Y1))))))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f69])).
% 8.92/2.40 thf(f129,plain,(
% 8.92/2.40 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 8.92/2.40 inference(cnf_transformation,[],[f83])).
% 8.92/2.40 thf(f133,plain,(
% 8.92/2.40 (mbox_s5 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))))),
% 8.92/2.40 inference(cnf_transformation,[],[f91])).
% 8.92/2.40 thf(f134,plain,(
% 8.92/2.40 (mdia_s5 = (^[Y0 : $i > $o]: (mnot @ (mbox_s5 @ (mnot @ Y0)))))),
% 8.92/2.40 inference(cnf_transformation,[],[f92])).
% 8.92/2.40 thf(f135,plain,(
% 8.92/2.40 (((mreflexive @ rel_s5)) = $true)),
% 8.92/2.40 inference(cnf_transformation,[],[f94])).
% 8.92/2.40 thf(f136,plain,(
% 8.92/2.40 (((mtransitive @ rel_s5)) = $true)),
% 8.92/2.40 inference(cnf_transformation,[],[f96])).
% 8.92/2.40 thf(f137,plain,(
% 8.92/2.40 (((msymmetric @ rel_s5)) = $true)),
% 8.92/2.40 inference(cnf_transformation,[],[f98])).
% 8.92/2.40 thf(f138,plain,(
% 8.92/2.40 (((mvalid @ (mequiv @ (mbox_s5 @ (mor @ (mnot @ p) @ (mdia_s5 @ q))) @ (mor @ (mnot @ (mdia_s5 @ p)) @ (mdia_s5 @ q))))) != $true)),
% 8.92/2.40 inference(cnf_transformation,[],[f101])).
% 8.92/2.40 thf(f140,definition,(
% 8.92/2.40 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 8.92/2.40 introduced(theory,[fool_exhaustiveness_axiom])).
% 8.92/2.40 thf(f141,plain,(
% 8.92/2.40 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y1)))))))),
% 8.92/2.40 inference(definition_unfolding,[],[f106,f104,f105,f104,f104])).
% 8.92/2.40 thf(f142,plain,(
% 8.92/2.40 (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)))))),
% 8.92/2.40 inference(definition_unfolding,[],[f107,f105,f104])).
% 8.92/2.40 thf(f144,plain,(
% 8.92/2.40 (mequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))))),
% 8.92/2.40 inference(definition_unfolding,[],[f109,f141,f142,f142])).
% 8.92/2.40 thf(f150,plain,(
% 8.92/2.40 (mdia_s5 = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))))),
% 8.92/2.40 inference(definition_unfolding,[],[f134,f104,f133,f104])).
% 8.92/2.40 thf(f151,plain,(
% 8.92/2.40 ($true = (((^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1 @ Y1)))) @ rel_s5)))),
% 8.92/2.40 inference(definition_unfolding,[],[f135,f119])).
% 8.92/2.40 thf(f152,plain,(
% 8.92/2.40 ($true = (((^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (((Y0 @ Y3 @ Y2) & (Y0 @ Y2 @ Y1)) => (Y0 @ Y3 @ Y1))))))))) @ rel_s5)))),
% 8.92/2.40 inference(definition_unfolding,[],[f136,f122])).
% 8.92/2.40 thf(f153,plain,(
% 8.92/2.40 ($true = (((^[Y0 : $i > $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2))))))) @ rel_s5)))),
% 8.92/2.40 inference(definition_unfolding,[],[f137,f120])).
% 8.92/2.40 thf(f154,plain,(
% 8.92/2.40 ($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]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ p) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ p)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))))))),
% 8.92/2.40 inference(definition_unfolding,[],[f138,f129,f144,f133,f105,f104,f150,f105,f104,f150,f150])).
% 8.92/2.40 thf(f155,definition,(
% 8.92/2.40 ($false = ((sP0 @ ((^[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]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ p) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ p)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q)))))))),
% 8.92/2.40 introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction])).
% 8.92/2.40 thf(f156,plain,(
% 8.92/2.40 ($true = ((sP0 @ $true)))),
% 8.92/2.40 inference(inequality_splitting,[],[f154,f155])).
% 8.92/2.40 thf(f157,definition,(
% 8.92/2.40 (sF1 = (((^[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]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ p) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ p)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))))))),
% 8.92/2.40 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 8.92/2.40 thf(f158,plain,(
% 8.92/2.40 ((((^[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]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ p) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ p)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))))) = sF1)),
% 8.92/2.40 inference(reorient_equations,[],[f157])).
% 8.92/2.40 thf(f159,definition,(
% 8.92/2.40 (sF2 = ((sP0 @ sF1)))),
% 8.92/2.40 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 8.92/2.40 thf(f160,plain,(
% 8.92/2.40 (((sP0 @ sF1)) = sF2)),
% 8.92/2.40 inference(reorient_equations,[],[f159])).
% 8.92/2.40 thf(f161,plain,(
% 8.92/2.40 ($false = sF2)),
% 8.92/2.40 inference(definition_folding,[],[f155,f160,f158])).
% 8.92/2.40 thf(f162,definition,(
% 8.92/2.40 (sF3 = ((sP0 @ $true)))),
% 8.92/2.40 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 8.92/2.40 thf(f163,plain,(
% 8.92/2.40 (((sP0 @ $true)) = sF3)),
% 8.92/2.40 inference(reorient_equations,[],[f162])).
% 8.92/2.40 thf(f164,plain,(
% 8.92/2.40 ($true = sF3)),
% 8.92/2.40 inference(definition_folding,[],[f156,f163])).
% 8.92/2.40 thf(f165,plain,(
% 8.92/2.40 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel_s5 @ Y1 @ Y0) => (rel_s5 @ Y0 @ Y1))))))))),
% 8.92/2.40 inference(beta-eta_normalization,[],[f153])).
% 8.92/2.40 thf(f166,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel_s5 @ Y1 @ Y0) => (rel_s5 @ Y0 @ Y1))))) @ X1)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f165])).
% 8.92/2.40 thf(f167,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((rel_s5 @ Y0 @ X1) => (rel_s5 @ X1 @ Y0))))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f166])).
% 8.92/2.40 thf(f168,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((rel_s5 @ Y0 @ X1) => (rel_s5 @ X1 @ Y0))) @ X2)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f167])).
% 8.92/2.40 thf(f169,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = (((rel_s5 @ X2 @ X1) => (rel_s5 @ X1 @ X2))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f168])).
% 8.92/2.40 thf(f170,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($false = ((rel_s5 @ X2 @ X1))) | (((rel_s5 @ X1 @ X2)) = $true)) )),
% 8.92/2.40 inference(imp_proxy_clausification,[],[f169])).
% 8.92/2.40 thf(f171,plain,(
% 8.92/2.40 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((rel_s5 @ Y2 @ Y1) & (rel_s5 @ Y1 @ Y0)) => (rel_s5 @ Y2 @ Y0))))))))))),
% 8.92/2.40 inference(beta-eta_normalization,[],[f152])).
% 8.92/2.40 thf(f172,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((rel_s5 @ Y2 @ Y1) & (rel_s5 @ Y1 @ Y0)) => (rel_s5 @ Y2 @ Y0))))))) @ X1)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f171])).
% 8.92/2.40 thf(f173,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((rel_s5 @ Y1 @ Y0) & (rel_s5 @ Y0 @ X1)) => (rel_s5 @ Y1 @ X1))))))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f172])).
% 8.92/2.40 thf(f174,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((rel_s5 @ Y1 @ Y0) & (rel_s5 @ Y0 @ X1)) => (rel_s5 @ Y1 @ X1))))) @ X2)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f173])).
% 8.92/2.40 thf(f175,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (((rel_s5 @ Y0 @ X2) & (rel_s5 @ X2 @ X1)) => (rel_s5 @ Y0 @ X1))))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f174])).
% 8.92/2.40 thf(f176,plain,(
% 8.92/2.40 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (((rel_s5 @ Y0 @ X2) & (rel_s5 @ X2 @ X1)) => (rel_s5 @ Y0 @ X1))) @ X3)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f175])).
% 8.92/2.40 thf(f177,plain,(
% 8.92/2.40 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((((rel_s5 @ X3 @ X2) & (rel_s5 @ X2 @ X1)) => (rel_s5 @ X3 @ X1))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f176])).
% 8.92/2.40 thf(f178,plain,(
% 8.92/2.40 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = (((rel_s5 @ X3 @ X2) & (rel_s5 @ X2 @ X1)))) | ($true = ((rel_s5 @ X3 @ X1)))) )),
% 8.92/2.40 inference(imp_proxy_clausification,[],[f177])).
% 8.92/2.40 thf(f179,plain,(
% 8.92/2.40 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((rel_s5 @ X2 @ X1))) | ($true = ((rel_s5 @ X3 @ X1))) | ($false = ((rel_s5 @ X3 @ X2)))) )),
% 8.92/2.40 inference(and_proxy_clausification,[],[f178])).
% 8.92/2.40 thf(f180,plain,(
% 8.92/2.40 ($true = ((!! @ $i @ (^[Y0 : $i]: (rel_s5 @ Y0 @ Y0)))))),
% 8.92/2.40 inference(beta-eta_normalization,[],[f151])).
% 8.92/2.40 thf(f181,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (rel_s5 @ Y0 @ Y0)) @ X1)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f180])).
% 8.92/2.40 thf(f182,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ X1)))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f181])).
% 8.92/2.40 thf(f184,plain,(
% 8.92/2.40 ($false = (((^[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]: (~ (Y4 @ Y5))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y3)))))) @ ((^[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)))) @ Y0 @ Y1) @ ((^[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)))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (Y0 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ p) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ p)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((~ (rel_s5 @ Y2 @ Y3)) | (Y1 @ Y3))))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ Y0)))) @ q)))))) | ($true = sF1)),
% 8.92/2.40 inference(iff_proxy_clausification,[],[f158])).
% 8.92/2.40 thf(f185,plain,(
% 8.92/2.40 ($false = ((!! @ $i @ (^[Y0 : $i]: (~ ((~ ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | ((~ (p @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (~ (q @ Y2))))))))))) | ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (p @ Y1))))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) | (~ ((~ ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (p @ Y1))))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | ((~ (p @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (~ (q @ Y2)))))))))))))))))) | ($true = sF1)),
% 8.92/2.40 inference(beta-eta_normalization,[],[f184])).
% 8.92/2.40 thf(f186,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: (~ ((~ ((~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | ((~ (p @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (~ (q @ Y2))))))))))) | ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (p @ Y1))))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) | (~ ((~ ((~ (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (p @ Y1))))))) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))) | (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | ((~ (p @ Y1)) | (~ (!! @ $i @ (^[Y2 : $i]: ((~ (rel_s5 @ Y1 @ Y2)) | (~ (q @ Y2))))))))))))))) @ sK4))) | ($true = sF1)),
% 8.92/2.40 inference(sigma_proxy_clausification,[],[f185])).
% 8.92/2.40 thf(f187,plain,(
% 8.92/2.40 ($false = ((~ ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))) | (~ ((~ ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))))))))))) | ($true = sF1)),
% 8.92/2.40 inference(beta-eta_normalization,[],[f186])).
% 8.92/2.40 thf(f188,plain,(
% 8.92/2.40 ($true = (((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))) | (~ ((~ ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))))))) | ($true = sF1)),
% 8.92/2.40 inference(not_proxy_clausification,[],[f187])).
% 8.92/2.40 thf(f189,plain,(
% 8.92/2.40 ($true = ((~ ((~ ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f188])).
% 8.92/2.40 thf(f190,plain,(
% 8.92/2.40 ($false = (((~ ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))) | (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.40 inference(not_proxy_clausification,[],[f189])).
% 8.92/2.40 thf(f191,plain,(
% 8.92/2.40 ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f190])).
% 8.92/2.40 thf(f192,plain,(
% 8.92/2.40 ($false = ((~ ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f190])).
% 8.92/2.40 thf(f193,plain,(
% 8.92/2.40 ($true = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.40 inference(not_proxy_clausification,[],[f192])).
% 8.92/2.40 thf(f194,plain,(
% 8.92/2.40 ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f193])).
% 8.92/2.40 thf(f195,plain,(
% 8.92/2.40 ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(not_proxy_clausification,[],[f194])).
% 8.92/2.40 thf(f196,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(sigma_proxy_clausification,[],[f195])).
% 8.92/2.40 thf(f197,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(not_proxy_clausification,[],[f196])).
% 8.92/2.40 thf(f198,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f197])).
% 8.92/2.40 thf(f199,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f197])).
% 8.92/2.40 thf(f200,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(not_proxy_clausification,[],[f199])).
% 8.92/2.40 thf(f201,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ X1))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f200])).
% 8.92/2.40 thf(f202,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f201])).
% 8.92/2.40 thf(f203,plain,(
% 8.92/2.40 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f202])).
% 8.92/2.40 thf(f204,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ X1))) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ X2)))) )),
% 8.92/2.40 inference(pi_proxy_clausification,[],[f203])).
% 8.92/2.40 thf(f205,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($false = (((~ (rel_s5 @ sK4 @ sK5)) | (~ (q @ sK5))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2)))))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f204])).
% 8.92/2.40 thf(f206,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($false = ((~ (q @ sK5)))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2)))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f205])).
% 8.92/2.40 thf(f207,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($false = ((~ (rel_s5 @ sK4 @ sK5)))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2)))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f205])).
% 8.92/2.40 thf(f208,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2)))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f207])).
% 8.92/2.40 thf(f209,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = (((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f208])).
% 8.92/2.40 thf(f210,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f209])).
% 8.92/2.40 thf(f211,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f210])).
% 8.92/2.40 thf(f212,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(sigma_proxy_clausification,[],[f211])).
% 8.92/2.40 thf(f213,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($true = ((~ (p @ X2)))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f212])).
% 8.92/2.40 thf(f214,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f213])).
% 8.92/2.40 thf(f215,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f214])).
% 8.92/2.40 thf(f216,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f215])).
% 8.92/2.40 thf(f217,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f216])).
% 8.92/2.40 thf(f218,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((~ (rel_s5 @ X1 @ (sK6 @ X1))) | (~ (q @ (sK6 @ X1)))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f217])).
% 8.92/2.40 thf(f219,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = ((~ (q @ (sK6 @ X1))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f218])).
% 8.92/2.40 thf(f220,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = ((~ (rel_s5 @ X1 @ (sK6 @ X1))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f218])).
% 8.92/2.40 thf(f221,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ X1 @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f220])).
% 8.92/2.40 thf(f222,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((q @ (sK6 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f219])).
% 8.92/2.40 thf(f223,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2)))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f206])).
% 8.92/2.40 thf(f224,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = (((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f223])).
% 8.92/2.40 thf(f225,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f224])).
% 8.92/2.40 thf(f226,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f225])).
% 8.92/2.40 thf(f227,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($true = (((~ (rel_s5 @ sK4 @ X2)) | (~ (p @ X2))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.40 inference(sigma_proxy_clausification,[],[f226])).
% 8.92/2.40 thf(f228,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($true = ((~ (p @ X2)))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f227])).
% 8.92/2.40 thf(f229,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f228])).
% 8.92/2.40 thf(f230,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f229])).
% 8.92/2.40 thf(f231,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X2))))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f230])).
% 8.92/2.40 thf(f232,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f231])).
% 8.92/2.40 thf(f233,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((~ (rel_s5 @ X1 @ (sK7 @ X1))) | (~ (q @ (sK7 @ X1)))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(beta-eta_normalization,[],[f232])).
% 8.92/2.40 thf(f234,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = ((~ (q @ (sK7 @ X1))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f233])).
% 8.92/2.40 thf(f235,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = ((~ (rel_s5 @ X1 @ (sK7 @ X1))))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(or_proxy_clausification,[],[f233])).
% 8.92/2.40 thf(f236,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ X1 @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f235])).
% 8.92/2.40 thf(f237,plain,(
% 8.92/2.40 ( ! [X2 : $i,X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((q @ (sK7 @ X1)))) | ($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X2)))) )),
% 8.92/2.40 inference(not_proxy_clausification,[],[f234])).
% 8.92/2.40 thf(f239,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.40 inference(or_proxy_clausification,[],[f198])).
% 8.92/2.40 thf(f240,plain,(
% 8.92/2.40 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f239])).
% 8.92/2.41 thf(f241,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f240])).
% 8.92/2.41 thf(f242,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ sK8))) | ($true = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.41 inference(sigma_proxy_clausification,[],[f241])).
% 8.92/2.41 thf(f243,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ sK8))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f242])).
% 8.92/2.41 thf(f244,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ sK8))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f243])).
% 8.92/2.41 thf(f245,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ sK5))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ sK8))) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ X1)))) )),
% 8.92/2.41 inference(pi_proxy_clausification,[],[f244])).
% 8.92/2.41 thf(f246,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((~ (rel_s5 @ sK4 @ sK5)) | (~ (q @ sK5))))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK8)) | (~ (p @ sK8))))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f245])).
% 8.92/2.41 thf(f247,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((~ (q @ sK5)))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK8)) | (~ (p @ sK8))))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f246])).
% 8.92/2.41 thf(f248,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((~ (rel_s5 @ sK4 @ sK5)))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK8)) | (~ (p @ sK8))))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f246])).
% 8.92/2.41 thf(f249,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK8)) | (~ (p @ sK8))))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f248])).
% 8.92/2.41 thf(f250,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = ((~ (p @ sK8)))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f249])).
% 8.92/2.41 thf(f251,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($false = ((~ (rel_s5 @ sK4 @ sK8)))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f249])).
% 8.92/2.41 thf(f252,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f251])).
% 8.92/2.41 thf(f253,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f252])).
% 8.92/2.41 thf(f254,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f253])).
% 8.92/2.41 thf(f255,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f254])).
% 8.92/2.41 thf(f256,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f250])).
% 8.92/2.41 thf(f257,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f256])).
% 8.92/2.41 thf(f258,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f257])).
% 8.92/2.41 thf(f259,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f258])).
% 8.92/2.41 thf(f260,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK8)) | (~ (p @ sK8))))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f247])).
% 8.92/2.41 thf(f261,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = ((~ (p @ sK8)))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f260])).
% 8.92/2.41 thf(f262,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($false = ((~ (rel_s5 @ sK4 @ sK8)))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f260])).
% 8.92/2.41 thf(f263,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f262])).
% 8.92/2.41 thf(f264,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f263])).
% 8.92/2.41 thf(f265,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f264])).
% 8.92/2.41 thf(f266,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK8))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f265])).
% 8.92/2.41 thf(f267,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (p @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f261])).
% 8.92/2.41 thf(f268,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($true = ((~ (p @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f267])).
% 8.92/2.41 thf(f269,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($false = ((p @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f268])).
% 8.92/2.41 thf(f270,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((q @ sK5))) | ($true = sF1) | ($true = ((p @ sK8))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f269])).
% 8.92/2.41 thf(f293,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = ((~ ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))))),
% 8.92/2.41 inference(sigma_proxy_clausification,[],[f191])).
% 8.92/2.41 thf(f294,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))) | ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f293])).
% 8.92/2.41 thf(f295,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = (((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f294])).
% 8.92/2.41 thf(f296,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1)))))))))))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f294])).
% 8.92/2.41 thf(f297,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f296])).
% 8.92/2.41 thf(f298,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ X1)))) )),
% 8.92/2.41 inference(pi_proxy_clausification,[],[f297])).
% 8.92/2.41 thf(f299,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((~ (rel_s5 @ sK4 @ sK9)) | ((~ (p @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f298])).
% 8.92/2.41 thf(f301,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((~ (rel_s5 @ sK4 @ sK9)))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f299])).
% 8.92/2.41 thf(f302,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | ((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f301])).
% 8.92/2.41 thf(f303,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = (((~ (p @ X1)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f302])).
% 8.92/2.41 thf(f304,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f303])).
% 8.92/2.41 thf(f305,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0))))))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f304])).
% 8.92/2.41 thf(f306,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK10 @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1)))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.41 inference(sigma_proxy_clausification,[],[f305])).
% 8.92/2.41 thf(f307,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK10 @ X1)))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($true = ((~ (p @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f306])).
% 8.92/2.41 thf(f308,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ X1 @ Y0)) | (~ (q @ Y0)))) @ (sK10 @ X1)))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f307])).
% 8.92/2.41 thf(f309,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = (((~ (rel_s5 @ X1 @ (sK10 @ X1))) | (~ (q @ (sK10 @ X1)))))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f308])).
% 8.92/2.41 thf(f310,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((~ (q @ (sK10 @ X1))))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f309])).
% 8.92/2.41 thf(f311,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((~ (rel_s5 @ X1 @ (sK10 @ X1))))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f309])).
% 8.92/2.41 thf(f312,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((rel_s5 @ X1 @ (sK10 @ X1)))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f311])).
% 8.92/2.41 thf(f313,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((q @ (sK10 @ X1)))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f310])).
% 8.92/2.41 thf(f345,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0))))))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f295])).
% 8.92/2.41 thf(f346,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = ((~ (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f295])).
% 8.92/2.41 thf(f347,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0))))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f346])).
% 8.92/2.41 thf(f348,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f347])).
% 8.92/2.41 thf(f349,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (p @ Y0)))) @ sK13)))),
% 8.92/2.41 inference(sigma_proxy_clausification,[],[f348])).
% 8.92/2.41 thf(f350,plain,(
% 8.92/2.41 ($false = (((~ (rel_s5 @ sK4 @ sK9)) | ((~ (p @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(beta-eta_normalization,[],[f349])).
% 8.92/2.41 thf(f351,plain,(
% 8.92/2.41 ($false = (((~ (p @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0))))))))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f350])).
% 8.92/2.41 thf(f352,plain,(
% 8.92/2.41 ($false = ((~ (rel_s5 @ sK4 @ sK9)))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f350])).
% 8.92/2.41 thf(f353,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f352])).
% 8.92/2.41 thf(f354,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((~ (p @ sK13))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f353])).
% 8.92/2.41 thf(f355,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((~ (rel_s5 @ sK4 @ sK13))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f353])).
% 8.92/2.41 thf(f356,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13)))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f355])).
% 8.92/2.41 thf(f357,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((p @ sK13)))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f354])).
% 8.92/2.41 thf(f358,plain,(
% 8.92/2.41 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))))))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f351])).
% 8.92/2.41 thf(f359,plain,(
% 8.92/2.41 ($false = ((~ (p @ sK9)))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f351])).
% 8.92/2.41 thf(f360,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f359])).
% 8.92/2.41 thf(f361,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ($true = sF1) | ($false = ((~ (p @ sK13))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f360])).
% 8.92/2.41 thf(f362,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ($true = sF1) | ($false = ((~ (rel_s5 @ sK4 @ sK13))))),
% 8.92/2.41 inference(or_proxy_clausification,[],[f360])).
% 8.92/2.41 thf(f363,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13)))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f362])).
% 8.92/2.41 thf(f364,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ($true = sF1) | ($true = ((p @ sK13)))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f361])).
% 8.92/2.41 thf(f365,plain,(
% 8.92/2.41 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0))))))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f358])).
% 8.92/2.41 thf(f366,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X1))) | ($true = sF1) | ($false = (((~ (rel_s5 @ sK4 @ sK13)) | (~ (p @ sK13)))))) )),
% 8.92/2.41 inference(pi_proxy_clausification,[],[f365])).
% 8.92/2.41 thf(f368,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X1))) | ($true = sF1) | ($false = ((~ (rel_s5 @ sK4 @ sK13))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f366])).
% 8.92/2.41 thf(f369,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X1))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f368])).
% 8.92/2.41 thf(f370,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = (((~ (rel_s5 @ sK9 @ X1)) | (~ (q @ X1))))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13)))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f369])).
% 8.92/2.41 thf(f371,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((~ (q @ X1)))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13))) | ($true = ((~ (rel_s5 @ sK9 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f370])).
% 8.92/2.41 thf(f372,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((q @ X1))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13))) | ($true = ((~ (rel_s5 @ sK9 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f371])).
% 8.92/2.41 thf(f373,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((q @ X1))) | ($true = sF1) | ($true = ((rel_s5 @ sK4 @ sK13))) | ($false = ((rel_s5 @ sK9 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f372])).
% 8.92/2.41 thf(f379,plain,(
% 8.92/2.41 ($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))))))),
% 8.92/2.41 inference(not_proxy_clausification,[],[f345])).
% 8.92/2.41 thf(f380,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | ((~ (p @ Y0)) | (~ (!! @ $i @ (^[Y1 : $i]: ((~ (rel_s5 @ Y0 @ Y1)) | (~ (q @ Y1))))))))) @ sK9))) | ($true = sF1) | ($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK4 @ Y0)) | (~ (q @ Y0)))) @ X1)))) )),
% 8.92/2.41 inference(pi_proxy_clausification,[],[f379])).
% 8.92/2.41 thf(f381,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((~ (rel_s5 @ sK4 @ sK9)) | ((~ (p @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))))))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f380])).
% 8.92/2.41 thf(f382,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = (((~ (p @ sK9)) | (~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0))))))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f381])).
% 8.92/2.41 thf(f383,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((~ (rel_s5 @ sK4 @ sK9)))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f381])).
% 8.92/2.41 thf(f384,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f383])).
% 8.92/2.41 thf(f385,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($true = ((~ (q @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f384])).
% 8.92/2.41 thf(f386,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((q @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f385])).
% 8.92/2.41 thf(f387,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ sK4 @ sK9))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f386])).
% 8.92/2.41 thf(f388,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f382])).
% 8.92/2.41 thf(f394,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0))))))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f388])).
% 8.92/2.41 thf(f395,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X2))) | ($true = sF1) | ($true = (((~ (rel_s5 @ sK4 @ X1)) | (~ (q @ X1)))))) )),
% 8.92/2.41 inference(pi_proxy_clausification,[],[f394])).
% 8.92/2.41 thf(f396,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X2))) | ($true = sF1) | ($true = ((~ (q @ X1)))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f395])).
% 8.92/2.41 thf(f397,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X2))) | ($true = sF1) | ($false = ((q @ X1))) | ($true = ((~ (rel_s5 @ sK4 @ X1))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f396])).
% 8.92/2.41 thf(f398,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (rel_s5 @ sK9 @ Y0)) | (~ (q @ Y0)))) @ X2))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f397])).
% 8.92/2.41 thf(f399,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = (((~ (rel_s5 @ sK9 @ X2)) | (~ (q @ X2))))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) )),
% 8.92/2.41 inference(beta-eta_normalization,[],[f398])).
% 8.92/2.41 thf(f400,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($true = ((~ (q @ X2)))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($true = ((~ (rel_s5 @ sK9 @ X2))))) )),
% 8.92/2.41 inference(or_proxy_clausification,[],[f399])).
% 8.92/2.41 thf(f401,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($false = ((q @ X2))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($true = ((~ (rel_s5 @ sK9 @ X2))))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f400])).
% 8.92/2.41 thf(f402,plain,(
% 8.92/2.41 ( ! [X2 : $i,X1 : $i] : (($false = ((q @ X2))) | ($true = sF1) | ($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((rel_s5 @ sK9 @ X2)))) )),
% 8.92/2.41 inference(not_proxy_clausification,[],[f401])).
% 8.92/2.41 thf(f516,plain,(
% 8.92/2.41 ($false = ((sP0 @ sF1))) | ($true = sF2)),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f160])).
% 8.92/2.41 thf(f517,plain,(
% 8.92/2.41 ($true = ((sP0 @ $true))) | ($false = sF3)),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f163])).
% 8.92/2.41 thf(f519,definition,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : ((((sF19 @ X0 @ X1)) = ((rel_s5 @ X0 @ X1)))) )),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 8.92/2.41 thf(f520,plain,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : ((((rel_s5 @ X0 @ X1)) = ((sF19 @ X0 @ X1)))) )),
% 8.92/2.41 inference(reorient_equations,[],[f519])).
% 8.92/2.41 thf(f522,definition,(
% 8.92/2.41 spl20_1 <=> ! [X2 : $i] : (($false = ((p @ X2))) | ($false = ((rel_s5 @ sK4 @ X2))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition])).
% 8.92/2.41 thf(f523,plain,(
% 8.92/2.41 ( ! [X2 : $i] : (($false = ((rel_s5 @ sK4 @ X2))) | ($false = ((p @ X2)))) ) | ~spl20_1),
% 8.92/2.41 inference(avatar_component_clause,[],[f522])).
% 8.92/2.41 thf(f525,definition,(
% 8.92/2.41 spl20_2 <=> ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK6 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition])).
% 8.92/2.41 thf(f526,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK6 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) ) | ~spl20_2),
% 8.92/2.41 inference(avatar_component_clause,[],[f525])).
% 8.92/2.41 thf(f528,definition,(
% 8.92/2.41 spl20_3 <=> ($true = sF1)),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition])).
% 8.92/2.41 thf(f530,plain,(
% 8.92/2.41 ($true = sF1) | ~spl20_3),
% 8.92/2.41 inference(avatar_component_clause,[],[f528])).
% 8.92/2.41 thf(f532,definition,(
% 8.92/2.41 spl20_4 <=> ($true = ((rel_s5 @ sK4 @ sK5)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition])).
% 8.92/2.41 thf(f534,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK5))) | ~spl20_4),
% 8.92/2.41 inference(avatar_component_clause,[],[f532])).
% 8.92/2.41 thf(f535,plain,(
% 8.92/2.41 spl20_1 | spl20_2 | spl20_3 | spl20_4),
% 8.92/2.41 inference(avatar_split_clause,[],[f221,f532,f528,f525,f522])).
% 8.92/2.41 thf(f537,definition,(
% 8.92/2.41 spl20_5 <=> ! [X1 : $i] : (($true = ((q @ (sK6 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition])).
% 8.92/2.41 thf(f538,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($true = ((q @ (sK6 @ X1))))) ) | ~spl20_5),
% 8.92/2.41 inference(avatar_component_clause,[],[f537])).
% 8.92/2.41 thf(f539,plain,(
% 8.92/2.41 spl20_1 | spl20_5 | spl20_3 | spl20_4),
% 8.92/2.41 inference(avatar_split_clause,[],[f222,f532,f528,f537,f522])).
% 8.92/2.41 thf(f541,definition,(
% 8.92/2.41 spl20_6 <=> ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK7 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition])).
% 8.92/2.41 thf(f542,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK7 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) ) | ~spl20_6),
% 8.92/2.41 inference(avatar_component_clause,[],[f541])).
% 8.92/2.41 thf(f544,definition,(
% 8.92/2.41 spl20_7 <=> ($true = ((q @ sK5)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition])).
% 8.92/2.41 thf(f546,plain,(
% 8.92/2.41 ($true = ((q @ sK5))) | ~spl20_7),
% 8.92/2.41 inference(avatar_component_clause,[],[f544])).
% 8.92/2.41 thf(f547,plain,(
% 8.92/2.41 spl20_1 | spl20_6 | spl20_3 | spl20_7),
% 8.92/2.41 inference(avatar_split_clause,[],[f236,f544,f528,f541,f522])).
% 8.92/2.41 thf(f549,definition,(
% 8.92/2.41 spl20_8 <=> ! [X1 : $i] : (($true = ((q @ (sK7 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition])).
% 8.92/2.41 thf(f550,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($true = ((q @ (sK7 @ X1))))) ) | ~spl20_8),
% 8.92/2.41 inference(avatar_component_clause,[],[f549])).
% 8.92/2.41 thf(f551,plain,(
% 8.92/2.41 spl20_1 | spl20_8 | spl20_3 | spl20_7),
% 8.92/2.41 inference(avatar_split_clause,[],[f237,f544,f528,f549,f522])).
% 8.92/2.41 thf(f553,definition,(
% 8.92/2.41 spl20_9 <=> ($true = ((rel_s5 @ sK4 @ sK8)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition])).
% 8.92/2.41 thf(f555,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK8))) | ~spl20_9),
% 8.92/2.41 inference(avatar_component_clause,[],[f553])).
% 8.92/2.41 thf(f556,plain,(
% 8.92/2.41 spl20_1 | spl20_9 | spl20_3 | spl20_4),
% 8.92/2.41 inference(avatar_split_clause,[],[f255,f532,f528,f553,f522])).
% 8.92/2.41 thf(f558,definition,(
% 8.92/2.41 spl20_10 <=> ($true = ((p @ sK8)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition])).
% 8.92/2.41 thf(f560,plain,(
% 8.92/2.41 ($true = ((p @ sK8))) | ~spl20_10),
% 8.92/2.41 inference(avatar_component_clause,[],[f558])).
% 8.92/2.41 thf(f561,plain,(
% 8.92/2.41 spl20_1 | spl20_10 | spl20_3 | spl20_4),
% 8.92/2.41 inference(avatar_split_clause,[],[f259,f532,f528,f558,f522])).
% 8.92/2.41 thf(f562,plain,(
% 8.92/2.41 spl20_1 | spl20_9 | spl20_3 | spl20_7),
% 8.92/2.41 inference(avatar_split_clause,[],[f266,f544,f528,f553,f522])).
% 8.92/2.41 thf(f563,plain,(
% 8.92/2.41 spl20_1 | spl20_10 | spl20_3 | spl20_7),
% 8.92/2.41 inference(avatar_split_clause,[],[f270,f544,f528,f558,f522])).
% 8.92/2.41 thf(f565,definition,(
% 8.92/2.41 spl20_11 <=> ! [X1 : $i] : (($false = ((q @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition])).
% 8.92/2.41 thf(f566,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((q @ X1)))) ) | ~spl20_11),
% 8.92/2.41 inference(avatar_component_clause,[],[f565])).
% 8.92/2.41 thf(f570,definition,(
% 8.92/2.41 spl20_12 <=> ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK10 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition])).
% 8.92/2.41 thf(f571,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($true = ((rel_s5 @ X1 @ (sK10 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1)))) ) | ~spl20_12),
% 8.92/2.41 inference(avatar_component_clause,[],[f570])).
% 8.92/2.41 thf(f573,definition,(
% 8.92/2.41 spl20_13 <=> ($true = ((rel_s5 @ sK4 @ sK9)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition])).
% 8.92/2.41 thf(f575,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK9))) | ~spl20_13),
% 8.92/2.41 inference(avatar_component_clause,[],[f573])).
% 8.92/2.41 thf(f576,plain,(
% 8.92/2.41 spl20_12 | spl20_3 | spl20_13),
% 8.92/2.41 inference(avatar_split_clause,[],[f312,f573,f528,f570])).
% 8.92/2.41 thf(f578,definition,(
% 8.92/2.41 spl20_14 <=> ! [X1 : $i] : (($true = ((q @ (sK10 @ X1)))) | ($false = ((p @ X1))) | ($false = ((rel_s5 @ sK4 @ X1))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition])).
% 8.92/2.41 thf(f579,plain,(
% 8.92/2.41 ( ! [X1 : $i] : (($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((p @ X1))) | ($true = ((q @ (sK10 @ X1))))) ) | ~spl20_14),
% 8.92/2.41 inference(avatar_component_clause,[],[f578])).
% 8.92/2.41 thf(f580,plain,(
% 8.92/2.41 spl20_14 | spl20_3 | spl20_13),
% 8.92/2.41 inference(avatar_split_clause,[],[f313,f573,f528,f578])).
% 8.92/2.41 thf(f585,definition,(
% 8.92/2.41 spl20_16 <=> ($true = ((p @ sK9)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition])).
% 8.92/2.41 thf(f587,plain,(
% 8.92/2.41 ($true = ((p @ sK9))) | ~spl20_16),
% 8.92/2.41 inference(avatar_component_clause,[],[f585])).
% 8.92/2.41 thf(f597,definition,(
% 8.92/2.41 spl20_19 <=> ! [X2 : $i] : (($false = ((q @ X2))) | ($false = ((rel_s5 @ sK9 @ X2))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition])).
% 8.92/2.41 thf(f598,plain,(
% 8.92/2.41 ( ! [X2 : $i] : (($false = ((rel_s5 @ sK9 @ X2))) | ($false = ((q @ X2)))) ) | ~spl20_19),
% 8.92/2.41 inference(avatar_component_clause,[],[f597])).
% 8.92/2.41 thf(f605,definition,(
% 8.92/2.41 spl20_21 <=> ($true = ((rel_s5 @ sK4 @ sK13)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition])).
% 8.92/2.41 thf(f607,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK4 @ sK13))) | ~spl20_21),
% 8.92/2.41 inference(avatar_component_clause,[],[f605])).
% 8.92/2.41 thf(f608,plain,(
% 8.92/2.41 spl20_21 | spl20_3 | spl20_13),
% 8.92/2.41 inference(avatar_split_clause,[],[f356,f573,f528,f605])).
% 8.92/2.41 thf(f610,definition,(
% 8.92/2.41 spl20_22 <=> ($true = ((p @ sK13)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_22])],[avatar_definition])).
% 8.92/2.41 thf(f612,plain,(
% 8.92/2.41 ($true = ((p @ sK13))) | ~spl20_22),
% 8.92/2.41 inference(avatar_component_clause,[],[f610])).
% 8.92/2.41 thf(f613,plain,(
% 8.92/2.41 spl20_22 | spl20_3 | spl20_13),
% 8.92/2.41 inference(avatar_split_clause,[],[f357,f573,f528,f610])).
% 8.92/2.41 thf(f614,plain,(
% 8.92/2.41 spl20_21 | spl20_3 | spl20_16),
% 8.92/2.41 inference(avatar_split_clause,[],[f363,f585,f528,f605])).
% 8.92/2.41 thf(f615,plain,(
% 8.92/2.41 spl20_22 | spl20_3 | spl20_16),
% 8.92/2.41 inference(avatar_split_clause,[],[f364,f585,f528,f610])).
% 8.92/2.41 thf(f616,plain,(
% 8.92/2.41 spl20_21 | spl20_3 | spl20_19),
% 8.92/2.41 inference(avatar_split_clause,[],[f373,f597,f528,f605])).
% 8.92/2.41 thf(f618,plain,(
% 8.92/2.41 spl20_11 | spl20_3 | spl20_13),
% 8.92/2.41 inference(avatar_split_clause,[],[f387,f573,f528,f565])).
% 8.92/2.41 thf(f620,plain,(
% 8.92/2.41 spl20_11 | spl20_3 | spl20_19),
% 8.92/2.41 inference(avatar_split_clause,[],[f402,f597,f528,f565])).
% 8.92/2.41 thf(f622,definition,(
% 8.92/2.41 spl20_23 <=> ($false = sF1)),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition])).
% 8.92/2.41 thf(f624,plain,(
% 8.92/2.41 ($false = sF1) | ~spl20_23),
% 8.92/2.41 inference(avatar_component_clause,[],[f622])).
% 8.92/2.41 thf(f673,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((sP0 @ sF1)))),
% 8.92/2.41 inference(forward_demodulation,[],[f516,f161])).
% 8.92/2.41 thf(f674,plain,(
% 8.92/2.41 ($false = ((sP0 @ sF1)))),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f673])).
% 8.92/2.41 thf(f675,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((sP0 @ $true)))),
% 8.92/2.41 inference(forward_demodulation,[],[f517,f164])).
% 8.92/2.41 thf(f676,plain,(
% 8.92/2.41 ($true = ((sP0 @ $true)))),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f675])).
% 8.92/2.41 thf(f681,plain,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : (($true = ((rel_s5 @ X0 @ X1))) | ($false = ((sF19 @ X0 @ X1)))) )),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f520])).
% 8.92/2.41 thf(f682,plain,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : (($false = ((rel_s5 @ X0 @ X1))) | ($true = ((sF19 @ X0 @ X1)))) )),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f520])).
% 8.92/2.41 thf(f693,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_3 | ~spl20_23)),
% 8.92/2.41 inference(constrained_superposition,[],[f530,f624])).
% 8.92/2.41 thf(f699,plain,(
% 8.92/2.41 $false | (~spl20_3 | ~spl20_23)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f693])).
% 8.92/2.41 thf(f700,plain,(
% 8.92/2.41 ~spl20_3 | ~spl20_23),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f699])).
% 8.92/2.41 thf(f721,plain,(
% 8.92/2.41 ( ! [X0 : $o] : ((((sP0 @ X0)) = X0) | ($false = X0)) )),
% 8.92/2.41 inference(constrained_superposition,[],[f676,f140])).
% 8.92/2.41 thf(f734,plain,(
% 8.92/2.41 ( ! [X0 : $o] : (($true = ((sP0 @ X0))) | ($false = X0) | ($false = X0)) )),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f721])).
% 8.92/2.41 thf(f736,plain,(
% 8.92/2.41 ( ! [X0 : $o] : (($true = ((sP0 @ X0))) | ($false = X0)) )),
% 8.92/2.41 inference(duplicate_literal_removal,[],[f734])).
% 8.92/2.41 thf(f742,plain,(
% 8.92/2.41 ($true = $false) | ($false = sF1)),
% 8.92/2.41 inference(constrained_superposition,[],[f674,f736])).
% 8.92/2.41 thf(f743,plain,(
% 8.92/2.41 ($false = sF1)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f742])).
% 8.92/2.41 thf(f865,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ X0 @ sK9)))) ) | ~spl20_19),
% 8.92/2.41 inference(constrained_superposition,[],[f598,f170])).
% 8.92/2.41 thf(f867,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ X0 @ sK9))) | ($false = ((q @ X0)))) ) | ~spl20_19),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f865])).
% 8.92/2.41 thf(f888,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((sF19 @ sK9 @ X0))) | ($false = ((q @ X0)))) ) | ~spl20_19),
% 8.92/2.41 inference(constrained_superposition,[],[f681,f598])).
% 8.92/2.41 thf(f900,definition,(
% 8.92/2.41 ( ! [X0 : $i] : ((((sF30 @ X0)) = ((q @ X0)))) )),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[sF30])],[function_definition])).
% 8.92/2.41 thf(f901,plain,(
% 8.92/2.41 ( ! [X0 : $i] : ((((q @ X0)) = ((sF30 @ X0)))) )),
% 8.92/2.41 inference(reorient_equations,[],[f900])).
% 8.92/2.41 thf(f903,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((q @ X0))) | ($false = ((sF30 @ X0)))) )),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f901])).
% 8.92/2.41 thf(f904,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((q @ X0))) | ($true = ((sF30 @ X0)))) )),
% 8.92/2.41 inference(iff_proxy_clausification,[],[f901])).
% 8.92/2.41 thf(f1003,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK9))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_13),
% 8.92/2.41 inference(constrained_superposition,[],[f575,f179])).
% 8.92/2.41 thf(f1026,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK9))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_13),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1003])).
% 8.92/2.41 thf(f1053,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_13),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f1026])).
% 8.92/2.41 thf(f1057,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | (~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(constrained_superposition,[],[f867,f1026])).
% 8.92/2.41 thf(f1058,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ X0 @ sK4))) | ($false = ((q @ X0)))) ) | (~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1057])).
% 8.92/2.41 thf(f1062,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_13),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1053])).
% 8.92/2.41 thf(f1076,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK4 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f1058])).
% 8.92/2.41 thf(f1081,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK4 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1076])).
% 8.92/2.41 thf(f1090,plain,(
% 8.92/2.41 spl20_11 | ~spl20_13 | ~spl20_19),
% 8.92/2.41 inference(avatar_split_clause,[],[f1081,f597,f573,f565])).
% 8.92/2.41 thf(f1096,plain,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ X1 @ X0))) | ($false = ((rel_s5 @ sK4 @ X1)))) ) | ~spl20_11),
% 8.92/2.41 inference(constrained_superposition,[],[f566,f179])).
% 8.92/2.41 thf(f1099,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((q @ sK5))) | (~spl20_4 | ~spl20_11)),
% 8.92/2.41 inference(constrained_superposition,[],[f534,f566])).
% 8.92/2.41 thf(f1114,plain,(
% 8.92/2.41 ($false = ((q @ sK5))) | (~spl20_4 | ~spl20_11)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1099])).
% 8.92/2.41 thf(f1125,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_4 | ~spl20_7 | ~spl20_11)),
% 8.92/2.41 inference(constrained_superposition,[],[f1114,f546])).
% 8.92/2.41 thf(f1131,plain,(
% 8.92/2.41 $false | (~spl20_4 | ~spl20_7 | ~spl20_11)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1125])).
% 8.92/2.41 thf(f1132,plain,(
% 8.92/2.41 ~spl20_4 | ~spl20_7 | ~spl20_11),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f1131])).
% 8.92/2.41 thf(f1142,plain,(
% 8.92/2.41 spl20_23),
% 8.92/2.41 inference(avatar_split_clause,[],[f743,f622])).
% 8.92/2.41 thf(f1150,plain,(
% 8.92/2.41 ( ! [X0 : $i,X1 : $i] : (($false = ((rel_s5 @ X1 @ X0))) | ($false = ((rel_s5 @ sK4 @ X1))) | ($false = ((q @ X0)))) ) | ~spl20_11),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1096])).
% 8.92/2.41 thf(f1259,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK8))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_9),
% 8.92/2.41 inference(constrained_superposition,[],[f179,f555])).
% 8.92/2.41 thf(f1262,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK8))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_9),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1259])).
% 8.92/2.41 thf(f1267,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_21),
% 8.92/2.41 inference(constrained_superposition,[],[f179,f607])).
% 8.92/2.41 thf(f1270,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_21),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1267])).
% 8.92/2.41 thf(f1522,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK8 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_9),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f1262])).
% 8.92/2.41 thf(f1529,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK8 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_9),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1522])).
% 8.92/2.41 thf(f1542,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_21),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f1270])).
% 8.92/2.41 thf(f1549,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK4)))) ) | ~spl20_21),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f1542])).
% 8.92/2.41 thf(f2090,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK4))) | ($true = ((rel_s5 @ sK8 @ sK9))) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f1062,f1529])).
% 8.92/2.41 thf(f2091,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK4))) | ($true = ((rel_s5 @ sK8 @ sK9))) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2090])).
% 8.92/2.41 thf(f2124,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((rel_s5 @ sK8 @ sK9))) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(forward_demodulation,[],[f2091,f182])).
% 8.92/2.41 thf(f2125,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK8 @ sK9))) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2124])).
% 8.92/2.41 thf(f2148,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK9))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f179,f2125])).
% 8.92/2.41 thf(f2153,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK9))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2148])).
% 8.92/2.41 thf(f2250,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((rel_s5 @ sK9 @ sK13))) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f1062,f1549])).
% 8.92/2.41 thf(f2256,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((rel_s5 @ sK8 @ sK13))) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f1529,f1549])).
% 8.92/2.41 thf(f2265,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK8 @ sK13))) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2256])).
% 8.92/2.41 thf(f2271,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK9 @ sK13))) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2250])).
% 8.92/2.41 thf(f2294,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((rel_s5 @ sK8 @ sK13))) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f2265,f182])).
% 8.92/2.41 thf(f2295,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK8 @ sK13))) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2294])).
% 8.92/2.41 thf(f2302,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((rel_s5 @ sK9 @ sK13))) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f2271,f182])).
% 8.92/2.41 thf(f2303,plain,(
% 8.92/2.41 ($true = ((rel_s5 @ sK9 @ sK13))) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2302])).
% 8.92/2.41 thf(f2318,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f179,f2295])).
% 8.92/2.41 thf(f2323,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2318])).
% 8.92/2.41 thf(f2336,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK9)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f179,f2303])).
% 8.92/2.41 thf(f2339,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ X0 @ sK13))) | ($false = ((rel_s5 @ X0 @ sK9)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f2336])).
% 8.92/2.41 thf(f3537,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f2153])).
% 8.92/2.41 thf(f3558,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f3537])).
% 8.92/2.41 thf(f3625,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f2323])).
% 8.92/2.41 thf(f3646,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK8)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f3625])).
% 8.92/2.41 thf(f3713,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK9)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f2339])).
% 8.92/2.41 thf(f3734,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ X0 @ sK9)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f3713])).
% 8.92/2.41 thf(f5101,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK8 @ X0))) | ($true = ((rel_s5 @ sK9 @ X0)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f3558])).
% 8.92/2.41 thf(f5120,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f5101])).
% 8.92/2.41 thf(f5548,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK8 @ X0))) | ($true = ((rel_s5 @ sK13 @ X0)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f3646])).
% 8.92/2.41 thf(f5561,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f5548])).
% 8.92/2.41 thf(f6014,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK9 @ X0))) | ($true = ((rel_s5 @ sK13 @ X0)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f170,f3734])).
% 8.92/2.41 thf(f6031,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = ((rel_s5 @ sK13 @ X0))) | ($false = ((rel_s5 @ sK9 @ X0)))) ) | (~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f6014])).
% 8.92/2.41 thf(f7132,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK8))) | ($true = ((q @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9)),
% 8.92/2.41 inference(constrained_superposition,[],[f555,f550])).
% 8.92/2.41 thf(f7137,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ($true = ((q @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f7132])).
% 8.92/2.41 thf(f7200,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((q @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9 | ~spl20_10)),
% 8.92/2.41 inference(forward_demodulation,[],[f7137,f560])).
% 8.92/2.41 thf(f7201,plain,(
% 8.92/2.41 ($true = ((q @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9 | ~spl20_10)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f7200])).
% 8.92/2.41 thf(f7332,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((sF30 @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9 | ~spl20_10)),
% 8.92/2.41 inference(constrained_superposition,[],[f7201,f904])).
% 8.92/2.41 thf(f8690,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($true = ((sF19 @ sK9 @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f682,f5120])).
% 8.92/2.41 thf(f8729,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK8 @ X0))) | ($true = ((sF19 @ sK9 @ X0)))) ) | (~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f8690])).
% 8.92/2.41 thf(f12658,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f542,f8729])).
% 8.92/2.41 thf(f12737,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f12658])).
% 8.92/2.41 thf(f12787,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK8))) | ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13)),
% 8.92/2.41 inference(forward_demodulation,[],[f12737,f560])).
% 8.92/2.41 thf(f12788,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK8))) | ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f12787])).
% 8.92/2.41 thf(f12791,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13)),
% 8.92/2.41 inference(forward_demodulation,[],[f12788,f555])).
% 8.92/2.41 thf(f20703,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK4 @ sK9))) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f1150,f5120])).
% 8.92/2.41 thf(f20825,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK8 @ X0))) | ($false = ((rel_s5 @ sK4 @ sK13))) | ($false = ((q @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f5561,f1150])).
% 8.92/2.41 thf(f20830,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ sK4 @ sK13))) | ($false = ((q @ X0)))) ) | (~spl20_11 | ~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f6031,f1150])).
% 8.92/2.41 thf(f20853,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK9 @ X0))) | ($false = ((rel_s5 @ sK4 @ sK13))) | ($false = ((q @ X0)))) ) | (~spl20_11 | ~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f20830])).
% 8.92/2.41 thf(f20858,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK8 @ X0))) | ($false = ((rel_s5 @ sK4 @ sK13))) | ($false = ((q @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f20825])).
% 8.92/2.41 thf(f20985,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK4 @ sK9))) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f20703])).
% 8.92/2.41 thf(f21082,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK9 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_11 | ~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f20853,f607])).
% 8.92/2.41 thf(f21083,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK9 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_11 | ~spl20_13 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f21082])).
% 8.92/2.41 thf(f21090,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((rel_s5 @ sK8 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f20858,f607])).
% 8.92/2.41 thf(f21091,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK8 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f21090])).
% 8.92/2.41 thf(f21152,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($true = $false) | ($false = ((q @ X0))) | ($false = ((rel_s5 @ sK8 @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(forward_demodulation,[],[f20985,f575])).
% 8.92/2.41 thf(f21172,plain,(
% 8.92/2.41 spl20_19 | ~spl20_11 | ~spl20_13 | ~spl20_21),
% 8.92/2.41 inference(avatar_split_clause,[],[f21083,f605,f573,f565,f597])).
% 8.92/2.41 thf(f22362,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK8))) | ($true = ((q @ (sK10 @ sK8)))) | (~spl20_9 | ~spl20_14)),
% 8.92/2.41 inference(constrained_superposition,[],[f555,f579])).
% 8.92/2.41 thf(f22366,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ($true = ((q @ (sK10 @ sK8)))) | (~spl20_9 | ~spl20_14)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f22362])).
% 8.92/2.41 thf(f22434,plain,(
% 8.92/2.41 ($true = $false) | ($true = ((q @ (sK10 @ sK8)))) | (~spl20_9 | ~spl20_10 | ~spl20_14)),
% 8.92/2.41 inference(forward_demodulation,[],[f22366,f560])).
% 8.92/2.41 thf(f22435,plain,(
% 8.92/2.41 ($true = ((q @ (sK10 @ sK8)))) | (~spl20_9 | ~spl20_10 | ~spl20_14)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f22434])).
% 8.92/2.41 thf(f23593,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((q @ (sK10 @ sK8)))) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_11 | ~spl20_12 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f21091,f571])).
% 8.92/2.41 thf(f23594,plain,(
% 8.92/2.41 ($false = ((q @ (sK10 @ sK8)))) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_11 | ~spl20_12 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f23593])).
% 8.92/2.41 thf(f23642,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f23594,f22435])).
% 8.92/2.41 thf(f23643,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f23642])).
% 8.92/2.41 thf(f23652,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f23643,f560])).
% 8.92/2.41 thf(f23653,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f23652])).
% 8.92/2.41 thf(f23665,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f23653,f1262])).
% 8.92/2.41 thf(f23710,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f23665])).
% 8.92/2.41 thf(f23739,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(forward_demodulation,[],[f23710,f182])).
% 8.92/2.41 thf(f23740,plain,(
% 8.92/2.41 $false | (~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f23739])).
% 8.92/2.41 thf(f23741,plain,(
% 8.92/2.41 ~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f23740])).
% 8.92/2.41 thf(f23747,definition,(
% 8.92/2.41 spl20_209 <=> ($false = ((p @ sK8)))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_209])],[avatar_definition])).
% 8.92/2.41 thf(f23748,plain,(
% 8.92/2.41 ($false != ((p @ sK8))) | spl20_209),
% 8.92/2.41 inference(avatar_component_clause,[],[f23747])).
% 8.92/2.41 thf(f23749,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ~spl20_209),
% 8.92/2.41 inference(avatar_component_clause,[],[f23747])).
% 8.92/2.41 thf(f23882,definition,(
% 8.92/2.41 spl20_212 <=> ($true = ((sF30 @ (sK7 @ sK8))))),
% 8.92/2.41 introduced(definition,[new_symbols(definition,[spl20_212])],[avatar_definition])).
% 8.92/2.41 thf(f23884,plain,(
% 8.92/2.41 ($true = ((sF30 @ (sK7 @ sK8)))) | ~spl20_212),
% 8.92/2.41 inference(avatar_component_clause,[],[f23882])).
% 8.92/2.41 thf(f24373,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK13))) | (~spl20_1 | ~spl20_21)),
% 8.92/2.41 inference(constrained_superposition,[],[f607,f523])).
% 8.92/2.41 thf(f24374,plain,(
% 8.92/2.41 ($false = ((p @ sK13))) | (~spl20_1 | ~spl20_21)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f24373])).
% 8.92/2.41 thf(f24448,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_1 | ~spl20_21 | ~spl20_22)),
% 8.92/2.41 inference(constrained_superposition,[],[f24374,f612])).
% 8.92/2.41 thf(f24454,plain,(
% 8.92/2.41 $false | (~spl20_1 | ~spl20_21 | ~spl20_22)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f24448])).
% 8.92/2.41 thf(f24455,plain,(
% 8.92/2.41 ~spl20_1 | ~spl20_21 | ~spl20_22),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f24454])).
% 8.92/2.41 thf(f26730,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((rel_s5 @ sK8 @ X0))) | ($false = ((q @ X0)))) ) | (~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f21152])).
% 8.92/2.41 thf(f28806,plain,(
% 8.92/2.41 ( ! [X0 : $i] : (($false = ((sF19 @ sK9 @ X0))) | ($false = ((q @ X0)))) ) | ~spl20_19),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f888])).
% 8.92/2.41 thf(f31343,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK9))) | (~spl20_1 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f523,f575])).
% 8.92/2.41 thf(f31366,plain,(
% 8.92/2.41 ($false = ((p @ sK9))) | (~spl20_1 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f31343])).
% 8.92/2.41 thf(f31389,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_1 | ~spl20_13 | ~spl20_16)),
% 8.92/2.41 inference(constrained_superposition,[],[f31366,f587])).
% 8.92/2.41 thf(f31395,plain,(
% 8.92/2.41 $false | (~spl20_1 | ~spl20_13 | ~spl20_16)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f31389])).
% 8.92/2.41 thf(f31396,plain,(
% 8.92/2.41 ~spl20_1 | ~spl20_13 | ~spl20_16),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f31395])).
% 8.92/2.41 thf(f31408,plain,(
% 8.92/2.41 ($true = ((sF30 @ (sK7 @ sK8)))) | (~spl20_8 | ~spl20_9 | ~spl20_10)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f7332])).
% 8.92/2.41 thf(f31423,plain,(
% 8.92/2.41 ($true = ((sF19 @ sK9 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f12791])).
% 8.92/2.41 thf(f31463,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_10 | ~spl20_209)),
% 8.92/2.41 inference(forward_demodulation,[],[f560,f23749])).
% 8.92/2.41 thf(f31464,plain,(
% 8.92/2.41 $false | (~spl20_10 | ~spl20_209)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f31463])).
% 8.92/2.41 thf(f31465,plain,(
% 8.92/2.41 ~spl20_10 | ~spl20_209),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f31464])).
% 8.92/2.41 thf(f31477,plain,(
% 8.92/2.41 spl20_212 | ~spl20_8 | ~spl20_9 | ~spl20_10),
% 8.92/2.41 inference(avatar_split_clause,[],[f31408,f558,f553,f549,f23882])).
% 8.92/2.41 thf(f32201,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((q @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(constrained_superposition,[],[f31423,f28806])).
% 8.92/2.41 thf(f32230,plain,(
% 8.92/2.41 ($false = ((q @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f32201])).
% 8.92/2.41 thf(f32263,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((sF30 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(constrained_superposition,[],[f903,f32230])).
% 8.92/2.41 thf(f32273,plain,(
% 8.92/2.41 ($false = ((sF30 @ (sK7 @ sK8)))) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f32263])).
% 8.92/2.41 thf(f32428,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19 | ~spl20_212)),
% 8.92/2.41 inference(constrained_superposition,[],[f32273,f23884])).
% 8.92/2.41 thf(f32432,plain,(
% 8.92/2.41 $false | (~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19 | ~spl20_212)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f32428])).
% 8.92/2.41 thf(f32433,plain,(
% 8.92/2.41 ~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19 | ~spl20_212),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f32432])).
% 8.92/2.41 thf(f33168,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((p @ sK8))) | ($true = ((q @ (sK6 @ sK8)))) | (~spl20_5 | ~spl20_9)),
% 8.92/2.41 inference(constrained_superposition,[],[f555,f538])).
% 8.92/2.41 thf(f33172,plain,(
% 8.92/2.41 ($false = ((p @ sK8))) | ($true = ((q @ (sK6 @ sK8)))) | (~spl20_5 | ~spl20_9)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f33168])).
% 8.92/2.41 thf(f33204,plain,(
% 8.92/2.41 ($true = ((q @ (sK6 @ sK8)))) | (~spl20_5 | ~spl20_9 | spl20_209)),
% 8.92/2.41 inference(forward_subsumption_resolution,[],[f33172,f23748])).
% 8.92/2.41 thf(f33686,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((q @ (sK6 @ sK8)))) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_2 | ~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(constrained_superposition,[],[f26730,f526])).
% 8.92/2.41 thf(f33689,plain,(
% 8.92/2.41 ($false = ((q @ (sK6 @ sK8)))) | ($false = ((p @ sK8))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_2 | ~spl20_9 | ~spl20_11 | ~spl20_13)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f33686])).
% 8.92/2.41 thf(f33718,plain,(
% 8.92/2.41 ($false = ((q @ (sK6 @ sK8)))) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_2 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(forward_subsumption_resolution,[],[f33689,f23748])).
% 8.92/2.41 thf(f33721,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(forward_demodulation,[],[f33718,f33204])).
% 8.92/2.41 thf(f33722,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK8))) | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f33721])).
% 8.92/2.41 thf(f37216,plain,(
% 8.92/2.41 ($true = $false) | ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(constrained_superposition,[],[f33722,f1262])).
% 8.92/2.41 thf(f37249,plain,(
% 8.92/2.41 ($false = ((rel_s5 @ sK4 @ sK4))) | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f37216])).
% 8.92/2.41 thf(f37274,plain,(
% 8.92/2.41 ($true = $false) | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(forward_demodulation,[],[f37249,f182])).
% 8.92/2.41 thf(f37275,plain,(
% 8.92/2.41 $false | (~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209)),
% 8.92/2.41 inference(trivial_inequality_removal,[],[f37274])).
% 8.92/2.41 thf(f37276,plain,(
% 8.92/2.41 ~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209),
% 8.92/2.41 inference(avatar_contradiction_clause,[],[f37275])).
% 8.92/2.41 cnf(s1, plain, spl20_1 | spl20_2 | spl20_3 | spl20_4, inference(sat_conversion,[],[f535])).
% 8.92/2.41 cnf(s2, plain, spl20_1 | spl20_3 | spl20_4 | spl20_5, inference(sat_conversion,[],[f539])).
% 8.92/2.41 cnf(s3, plain, spl20_1 | spl20_3 | spl20_6 | spl20_7, inference(sat_conversion,[],[f547])).
% 8.92/2.41 cnf(s4, plain, spl20_1 | spl20_3 | spl20_7 | spl20_8, inference(sat_conversion,[],[f551])).
% 8.92/2.41 cnf(s5, plain, spl20_1 | spl20_3 | spl20_4 | spl20_9, inference(sat_conversion,[],[f556])).
% 8.92/2.41 cnf(s6, plain, spl20_1 | spl20_3 | spl20_4 | spl20_10, inference(sat_conversion,[],[f561])).
% 8.92/2.41 cnf(s7, plain, spl20_1 | spl20_3 | spl20_7 | spl20_9, inference(sat_conversion,[],[f562])).
% 8.92/2.41 cnf(s8, plain, spl20_1 | spl20_3 | spl20_7 | spl20_10, inference(sat_conversion,[],[f563])).
% 8.92/2.41 cnf(s11, plain, spl20_3 | spl20_12 | spl20_13, inference(sat_conversion,[],[f576])).
% 8.92/2.41 cnf(s12, plain, spl20_3 | spl20_13 | spl20_14, inference(sat_conversion,[],[f580])).
% 8.92/2.41 cnf(s17, plain, spl20_3 | spl20_13 | spl20_21, inference(sat_conversion,[],[f608])).
% 8.92/2.41 cnf(s18, plain, spl20_3 | spl20_13 | spl20_22, inference(sat_conversion,[],[f613])).
% 8.92/2.41 cnf(s19, plain, spl20_3 | spl20_16 | spl20_21, inference(sat_conversion,[],[f614])).
% 8.92/2.41 cnf(s20, plain, spl20_3 | spl20_16 | spl20_22, inference(sat_conversion,[],[f615])).
% 8.92/2.41 cnf(s21, plain, spl20_3 | spl20_19 | spl20_21, inference(sat_conversion,[],[f616])).
% 8.92/2.41 cnf(s23, plain, spl20_3 | spl20_11 | spl20_13, inference(sat_conversion,[],[f618])).
% 8.92/2.41 cnf(s25, plain, spl20_3 | spl20_11 | spl20_19, inference(sat_conversion,[],[f620])).
% 8.92/2.41 cnf(s39, plain, ~spl20_3 | ~spl20_23, inference(sat_conversion,[],[f700])).
% 8.92/2.41 cnf(s40, plain, spl20_11 | ~spl20_13 | ~spl20_19, inference(sat_conversion,[],[f1090])).
% 8.92/2.41 cnf(s43, plain, ~spl20_4 | ~spl20_7 | ~spl20_11, inference(sat_conversion,[],[f1132])).
% 8.92/2.41 cnf(s44, plain, spl20_23, inference(sat_conversion,[],[f1142])).
% 8.92/2.41 cnf(s673, plain, ~spl20_11 | ~spl20_13 | spl20_19 | ~spl20_21, inference(sat_conversion,[],[f21172])).
% 8.92/2.41 cnf(s704, plain, ~spl20_9 | ~spl20_10 | ~spl20_11 | ~spl20_12 | ~spl20_14 | ~spl20_21, inference(sat_conversion,[],[f23741])).
% 8.92/2.41 cnf(s906, plain, ~spl20_1 | ~spl20_21 | ~spl20_22, inference(sat_conversion,[],[f24455])).
% 8.92/2.41 cnf(s1812, plain, ~spl20_1 | ~spl20_13 | ~spl20_16, inference(sat_conversion,[],[f31396])).
% 8.92/2.41 cnf(s1813, plain, ~spl20_10 | ~spl20_209, inference(sat_conversion,[],[f31465])).
% 8.92/2.41 cnf(s1817, plain, ~spl20_8 | ~spl20_9 | ~spl20_10 | spl20_212, inference(sat_conversion,[],[f31477])).
% 8.92/2.41 cnf(s1937, plain, ~spl20_6 | ~spl20_9 | ~spl20_10 | ~spl20_13 | ~spl20_19 | ~spl20_212, inference(sat_conversion,[],[f32433])).
% 8.92/2.41 cnf(s2254, plain, ~spl20_2 | ~spl20_5 | ~spl20_9 | ~spl20_11 | ~spl20_13 | spl20_209, inference(sat_conversion,[],[f37276])).
% 8.92/2.41 cnf(s2255, plain, ~spl20_3, inference(rat,[],[s39,s44])).
% 8.92/2.41 cnf(s2256, plain, spl20_11 | spl20_19, inference(rat,[],[s25,s2255])).
% 8.92/2.41 cnf(s2258, plain, spl20_11 | spl20_13, inference(rat,[],[s23,s2255])).
% 8.92/2.41 cnf(s2260, plain, spl20_19 | spl20_21, inference(rat,[],[s21,s2255])).
% 8.92/2.41 cnf(s2261, plain, spl20_16 | spl20_22, inference(rat,[],[s20,s2255])).
% 8.92/2.41 cnf(s2262, plain, spl20_16 | spl20_21, inference(rat,[],[s19,s2255])).
% 8.92/2.41 cnf(s2263, plain, spl20_13 | spl20_22, inference(rat,[],[s18,s2255])).
% 8.92/2.41 cnf(s2264, plain, spl20_13 | spl20_21, inference(rat,[],[s17,s2255])).
% 8.92/2.41 cnf(s2269, plain, spl20_13 | spl20_14, inference(rat,[],[s12,s2255])).
% 8.92/2.41 cnf(s2270, plain, spl20_12 | spl20_13, inference(rat,[],[s11,s2255])).
% 8.92/2.41 cnf(s2273, plain, spl20_1 | spl20_7 | spl20_10, inference(rat,[],[s8,s2255])).
% 8.92/2.41 cnf(s2274, plain, spl20_1 | spl20_7 | spl20_9, inference(rat,[],[s7,s2255])).
% 8.92/2.41 cnf(s2275, plain, spl20_1 | spl20_4 | spl20_10, inference(rat,[],[s6,s2255])).
% 8.92/2.41 cnf(s2276, plain, spl20_1 | spl20_4 | spl20_9, inference(rat,[],[s5,s2255])).
% 8.92/2.41 cnf(s2277, plain, spl20_1 | spl20_7 | spl20_8, inference(rat,[],[s4,s2255])).
% 8.92/2.41 cnf(s2278, plain, spl20_1 | spl20_6 | spl20_7, inference(rat,[],[s3,s2255])).
% 8.92/2.41 cnf(s2279, plain, spl20_1 | spl20_4 | spl20_5, inference(rat,[],[s2,s2255])).
% 8.92/2.41 cnf(s2280, plain, spl20_1 | spl20_2 | spl20_4, inference(rat,[],[s1,s2255])).
% 8.92/2.41 cnf(s2281, plain, spl20_11, inference(rat,[],[s40,s2258,s2256])).
% 8.92/2.41 cnf(s2284, plain, ~spl20_13 | ~spl20_212 | ~spl20_6 | ~spl20_10 | ~spl20_9, inference(rat,[],[s673,s2260,s1937,s2281])).
% 8.92/2.41 cnf(s2285, plain, ~spl20_212 | ~spl20_9 | ~spl20_6 | ~spl20_10, inference(rat,[],[s704,s2270,s2269,s2264,s2284,s2281])).
% 8.92/2.41 cnf(s2286, plain, spl20_7 | spl20_1, inference(rat,[],[s2285,s1817,s2278,s2277,s2274,s2273])).
% 8.92/2.41 cnf(s2287, plain, spl20_4 | spl20_1, inference(rat,[],[s704,s2270,s2269,s2264,s2254,s1813,s2280,s2279,s2276,s2275,s2281])).
% 8.92/2.41 cnf(s2288, plain, spl20_1, inference(rat,[],[s2287,s43,s2286,s2281])).
% 8.92/2.41 cnf(s2293, plain, spl20_16, inference(rat,[],[s906,s2262,s2261,s2288])).
% 8.92/2.41 cnf(s2295, plain, ~spl20_13, inference(rat,[],[s1812,s2288,s2293])).
% 8.92/2.41 cnf(s2296, plain, spl20_22, inference(rat,[],[s2263,s2295])).
% 8.92/2.41 cnf(s2297, plain, spl20_21, inference(rat,[],[s2264,s2295])).
% 8.92/2.41 cnf(s2300, plain, $false, inference(rat,[],[s906,s2288,s2296,s2297])).
% 8.92/2.41 thf(f37277,plain,(
% 8.92/2.41 $false),
% 8.92/2.41 inference(avatar_sat_refutation,[],[s2300])).
% 8.92/2.41 % SZS output end Proof for theBenchmark
% 8.92/2.41 % (595814)------------------------------
% 8.92/2.41 % (595814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/2.41 % (595814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.41 % (595814)CaDiCaL version: 2.1.3
% 8.92/2.41 % (595814)Termination reason: Refutation
% 8.92/2.41 % (595814)Time elapsed: 0.578 s
% 8.92/2.41 % (595814)Peak memory usage: 20 MB
% 8.92/2.41 % (595814)Instructions burned: 2320 (million)
% 8.92/2.41 % (595427)Success in time 2.194 s
% 8.92/2.41 % Vampire exiting
%------------------------------------------------------------------------------