%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN391^4 : 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 : n006.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:41:53 AM UTC 2026
% Result : Theorem 22.37s 3.41s
% Output : Refutation 22.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN391^4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.18 % Computer : n006.cluster.edu
% 0.12/0.18 % Model : x86_64 x86_64
% 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.18 % Memory : 8046.5625MB
% 0.12/0.18 % OS : Linux 6.8.0-71-generic
% 0.12/0.18 % CPULimit : 300
% 0.12/0.18 % WCLimit : 300
% 0.12/0.18 % DateTime : Tue Sep 29 16:15:39 UTC 2026
% 0.12/0.18 % CPUTime :
% 0.12/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.22 Running first-order model finding
% 0.12/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.21/0.91 % (927024)Will run a generic schedule for satisfiability detection.
% 4.21/0.91 % (927042)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3335753399_2999 on theBenchmark for (2999ds/0Mi)
% 4.21/0.91 % Exception at run slice level
% 4.21/0.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.21/0.91 % (927047)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2276651452:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.21/0.91 % (927043)% WARNING: option uhcvi not known.
% 4.21/0.91 % (927044)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1604104223:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.21/0.91 % (927043)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=489966939:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.21/0.91 % (927045)dis+10_1_sil=32000:sp=arity:random_seed=1291979669:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.21/0.91 % (927043)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.91 % (927048)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3801096428:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.21/0.91 % (927046)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1273113524:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.21/0.91 % (927043)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.21/0.91 % (927046)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.91 % (927051)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=968458691:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.21/0.91 % Exception at run slice level
% 4.21/0.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.21/0.91 % (927047)Instruction limit reached!
% 4.21/0.91 % (927047)------------------------------
% 4.21/0.91 % (927047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.91 % (927047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.91 % (927047)CaDiCaL version: 2.1.3
% 4.21/0.91 % (927047)Termination reason: Instruction limit
% 4.21/0.91 % (927047)Termination phase: Saturation
% 4.21/0.91 % (927047)Time elapsed: 0.032 s
% 4.21/0.91 % (927047)Peak memory usage: 12 MB
% 4.21/0.91 % (927047)Instructions burned: 131 (million)
% 4.21/0.91 % (927061)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=728536268:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.21/0.91 % (927062)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=3587232005:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.21/0.91 % (927062)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.21/0.91 % (927062)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.21/0.91 % (927045)Instruction limit reached!
% 4.21/0.91 % (927045)------------------------------
% 4.21/0.91 % (927045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.91 % (927045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.91 % (927045)CaDiCaL version: 2.1.3
% 4.21/0.91 % (927045)Termination reason: Instruction limit
% 4.21/0.91 % (927045)Termination phase: Saturation
% 4.21/0.91 % (927045)Time elapsed: 0.049 s
% 4.21/0.91 % (927045)Peak memory usage: 12 MB
% 4.21/0.91 % (927045)Instructions burned: 104 (million)
% 4.21/0.91 % (927046)Instruction limit reached!
% 4.21/0.91 % (927046)------------------------------
% 4.21/0.91 % (927046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/0.91 % (927046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/0.91 % (927046)CaDiCaL version: 2.1.3
% 4.21/0.91 % (927046)Termination reason: Instruction limit
% 4.21/0.91 % (927046)Termination phase: Saturation
% 4.21/0.91 % (927046)Time elapsed: 0.054 s
% 4.21/0.91 % (927046)Peak memory usage: 12 MB
% 4.21/0.91 % (927046)Instructions burned: 117 (million)
% 4.21/0.91 % (927065)ott-21_1_sil=16000:fs=off:random_seed=2054583518:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.21/0.91 % (927048)Instruction limit reached!
% 4.21/0.91 % (927048)------------------------------
% 16.15/2.65 % (927048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.65 % (927048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.65 % (927048)CaDiCaL version: 2.1.3
% 16.15/2.65 % (927048)Termination reason: Instruction limit
% 16.15/2.65 % (927048)Termination phase: Saturation
% 16.15/2.65 % (927048)Time elapsed: 0.074 s
% 16.15/2.65 % (927048)Peak memory usage: 12 MB
% 16.15/2.65 % (927048)Instructions burned: 159 (million)
% 16.15/2.65 % (927066)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=309538319:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 16.15/2.65 % (927061)Instruction limit reached!
% 16.15/2.65 % (927061)------------------------------
% 16.15/2.65 % (927061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.65 % (927061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.65 % (927061)CaDiCaL version: 2.1.3
% 16.15/2.65 % (927061)Termination reason: Instruction limit
% 16.15/2.65 % (927061)Termination phase: Saturation
% 16.15/2.65 % (927061)Time elapsed: 0.060 s
% 16.15/2.65 % (927061)Peak memory usage: 12 MB
% 16.15/2.65 % (927061)Instructions burned: 131 (million)
% 16.15/2.65 % (927069)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2050761680:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 16.15/2.65 % Exception at run slice level
% 16.15/2.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.15/2.65 % (927076)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1706783789:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 16.15/2.65 % (927080)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=125265556:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 16.15/2.65 % Exception at run slice level
% 16.15/2.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.15/2.65 % (927093)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=3785475726:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 16.15/2.65 % (927093)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.15/2.65 % (927065)Instruction limit reached!
% 16.15/2.65 % (927065)------------------------------
% 16.15/2.65 % (927065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.65 % (927065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.65 % (927065)CaDiCaL version: 2.1.3
% 16.15/2.65 % (927065)Termination reason: Instruction limit
% 16.15/2.65 % (927065)Termination phase: Saturation
% 16.15/2.65 % (927065)Time elapsed: 0.085 s
% 16.15/2.65 % (927065)Peak memory usage: 12 MB
% 16.15/2.65 % (927065)Instructions burned: 189 (million)
% 16.15/2.65 % (927112)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3679218064:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 16.15/2.65 % (927112)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.15/2.65 % (927062)Instruction limit reached!
% 16.15/2.65 % (927062)------------------------------
% 16.15/2.65 % (927062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.15/2.65 % (927062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/2.65 % (927062)CaDiCaL version: 2.1.3
% 16.15/2.65 % (927062)Termination reason: Instruction limit
% 16.15/2.65 % (927062)Termination phase: Saturation
% 16.15/2.65 % (927062)Time elapsed: 0.156 s
% 16.15/2.65 % (927062)Peak memory usage: 14 MB
% 16.15/2.65 % (927062)Instructions burned: 687 (million)
% 16.15/2.65 % (927129)fmb+10_1_sil=64000:random_seed=1389929750:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 16.15/2.65 % (927129)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.15/2.65 % Exception at run slice level
% 16.15/2.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.15/2.65 % (927136)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3503320628:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 16.15/2.65 % Exception at run slice level
% 16.15/2.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.15/2.65 % (927145)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3014367764:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927155)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=933366478:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 22.37/3.41 % (927155)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.37/3.41 % (927066)Instruction limit reached!
% 22.37/3.41 % (927066)------------------------------
% 22.37/3.41 % (927066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927066)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927066)Termination reason: Instruction limit
% 22.37/3.41 % (927066)Termination phase: Saturation
% 22.37/3.41 % (927066)Time elapsed: 0.217 s
% 22.37/3.41 % (927066)Peak memory usage: 13 MB
% 22.37/3.41 % (927066)Instructions burned: 477 (million)
% 22.37/3.41 % (927177)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2476784716:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 22.37/3.41 % (927177)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 22.37/3.41 % (927177)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.37/3.41 % (927093)Instruction limit reached!
% 22.37/3.41 % (927093)------------------------------
% 22.37/3.41 % (927093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927093)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927093)Termination reason: Instruction limit
% 22.37/3.41 % (927093)Termination phase: Saturation
% 22.37/3.41 % (927093)Time elapsed: 0.303 s
% 22.37/3.41 % (927093)Peak memory usage: 14 MB
% 22.37/3.41 % (927093)Instructions burned: 693 (million)
% 22.37/3.41 % (927237)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2320751470:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927243)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3868049165:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927245)ott-2_1_sil=16000:newcnf=on:random_seed=3112935383:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 22.37/3.41 % (927245)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.37/3.41 % (927112)Instruction limit reached!
% 22.37/3.41 % (927112)------------------------------
% 22.37/3.41 % (927112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927112)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927112)Termination reason: Instruction limit
% 22.37/3.41 % (927112)Termination phase: Saturation
% 22.37/3.41 % (927112)Time elapsed: 0.407 s
% 22.37/3.41 % (927112)Peak memory usage: 14 MB
% 22.37/3.41 % (927112)Instructions burned: 879 (million)
% 22.37/3.41 % (927076)Instruction limit reached!
% 22.37/3.41 % (927076)------------------------------
% 22.37/3.41 % (927076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927076)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927076)Termination reason: Instruction limit
% 22.37/3.41 % (927076)Termination phase: Saturation
% 22.37/3.41 % (927076)Time elapsed: 0.482 s
% 22.37/3.41 % (927076)Peak memory usage: 14 MB
% 22.37/3.41 % (927076)Instructions burned: 1179 (million)
% 22.37/3.41 % (927247)ott+10_1_sil=32000:tgt=ground:random_seed=508366805:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 22.37/3.41 % (927248)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2680958670:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927251)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2792192065:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 22.37/3.41 % (927251)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.37/3.41 % (927245)Instruction limit reached!
% 22.37/3.41 % (927245)------------------------------
% 22.37/3.41 % (927245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927245)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927245)Termination reason: Instruction limit
% 22.37/3.41 % (927245)Termination phase: Saturation
% 22.37/3.41 % (927245)Time elapsed: 0.344 s
% 22.37/3.41 % (927245)Peak memory usage: 13 MB
% 22.37/3.41 % (927245)Instructions burned: 870 (million)
% 22.37/3.41 % (927253)dis+21_1_sil=32000:sas=cadical:random_seed=1098374879:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 22.37/3.41 % (927177)Instruction limit reached!
% 22.37/3.41 % (927177)------------------------------
% 22.37/3.41 % (927177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927177)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927177)Termination reason: Instruction limit
% 22.37/3.41 % (927177)Termination phase: Saturation
% 22.37/3.41 % (927177)Time elapsed: 0.731 s
% 22.37/3.41 % (927177)Peak memory usage: 21 MB
% 22.37/3.41 % (927177)Instructions burned: 1473 (million)
% 22.37/3.41 % (927255)ott+11_1_sil=16000:gs=on:random_seed=3233215540:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 22.37/3.41 % (927255)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.37/3.41 % (927155)Instruction limit reached!
% 22.37/3.41 % (927155)------------------------------
% 22.37/3.41 % (927155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927155)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927155)Termination reason: Instruction limit
% 22.37/3.41 % (927155)Termination phase: Saturation
% 22.37/3.41 % (927155)Time elapsed: 1.086 s
% 22.37/3.41 % (927155)Peak memory usage: 16 MB
% 22.37/3.41 % (927155)Instructions burned: 5131 (million)
% 22.37/3.41 % (927257)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3962220353:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927259)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3194385814:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi)
% 22.37/3.41 % (927255)Instruction limit reached!
% 22.37/3.41 % (927255)------------------------------
% 22.37/3.41 % (927255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927255)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927255)Termination reason: Instruction limit
% 22.37/3.41 % (927255)Termination phase: Saturation
% 22.37/3.41 % (927255)Time elapsed: 0.871 s
% 22.37/3.41 % (927255)Peak memory usage: 14 MB
% 22.37/3.41 % (927255)Instructions burned: 2253 (million)
% 22.37/3.41 % (927261)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2897504716:i=29340_2980 on theBenchmark for (2980ds/29340Mi)
% 22.37/3.41 % (927251)Instruction limit reached!
% 22.37/3.41 % (927251)------------------------------
% 22.37/3.41 % (927251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927251)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927251)Termination reason: Instruction limit
% 22.37/3.41 % (927251)Termination phase: Saturation
% 22.37/3.41 % (927251)Time elapsed: 1.465 s
% 22.37/3.41 % (927251)Peak memory usage: 17 MB
% 22.37/3.41 % (927251)Instructions burned: 3514 (million)
% 22.37/3.41 % (927263)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=326682877:i=5211_2978 on theBenchmark for (2978ds/5211Mi)
% 22.37/3.41 % (927259)Instruction limit reached!
% 22.37/3.41 % (927259)------------------------------
% 22.37/3.41 % (927259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927259)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927259)Termination reason: Instruction limit
% 22.37/3.41 % (927259)Termination phase: Saturation
% 22.37/3.41 % (927259)Time elapsed: 1.011 s
% 22.37/3.41 % (927259)Peak memory usage: 19 MB
% 22.37/3.41 % (927259)Instructions burned: 4595 (million)
% 22.37/3.41 % (927265)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=855501957:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927267)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4049532367:fmbsr=2:i=46332_2975 on theBenchmark for (2975ds/46332Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927269)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1174236818:i=14071_2975 on theBenchmark for (2975ds/14071Mi)
% 22.37/3.41 % Exception at run slice level
% 22.37/3.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.37/3.41 % (927271)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=811202193:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi)
% 22.37/3.41 % (927253)Instruction limit reached!
% 22.37/3.41 % (927253)------------------------------
% 22.37/3.41 % (927253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927253)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927253)Termination reason: Instruction limit
% 22.37/3.41 % (927253)Termination phase: Saturation
% 22.37/3.41 % (927253)Time elapsed: 1.593 s
% 22.37/3.41 % (927253)Peak memory usage: 17 MB
% 22.37/3.41 % (927253)Instructions burned: 3775 (million)
% 22.37/3.41 % (927273)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3960627169:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi)
% 22.37/3.41 % (927247)Instruction limit reached!
% 22.37/3.41 % (927247)------------------------------
% 22.37/3.41 % (927247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.41 % (927247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.41 % (927247)CaDiCaL version: 2.1.3
% 22.37/3.41 % (927247)Termination reason: Instruction limit
% 22.37/3.41 % (927247)Termination phase: Saturation
% 22.37/3.41 % (927247)Time elapsed: 2.037 s
% 22.37/3.41 % (927247)Peak memory usage: 15 MB
% 22.37/3.41 % (927247)Instructions burned: 5115 (million)
% 22.37/3.41 % (927275)dis+10_16:1_sil=16000:random_seed=3398746992:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi)
% 22.37/3.41 % (927043) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-927024-927043"...
% 22.37/3.41 % (927043)...printing done.
% 22.37/3.41 % (927043)Refutation found. Thanks to Tanya!
% 22.37/3.41 % SZS status Theorem for theBenchmark
% 22.37/3.41 % SZS output start Proof for theBenchmark
% 22.37/3.41 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 22.37/3.41 thf(func_def_0, type, irel: ($i > $i > $o)).
% 22.37/3.41 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_9, type, itrue: ($i > $o)).
% 22.37/3.41 thf(func_def_10, type, ifalse: ($i > $o)).
% 22.37/3.41 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 22.37/3.41 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 22.37/3.41 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 22.37/3.41 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 22.37/3.41 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 22.37/3.41 thf(func_def_21, type, p1: ($i > $o)).
% 22.37/3.41 thf(func_def_22, type, p2: ($i > $o)).
% 22.37/3.41 thf(func_def_25, type, vNOT: ($o > $o)).
% 22.37/3.41 thf(func_def_26, type, db1: !>[X0: $tType]:(X0)).
% 22.37/3.41 thf(func_def_27, type, db0: !>[X0: $tType]:(X0)).
% 22.37/3.41 thf(func_def_28, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 22.37/3.41 thf(func_def_29, type, vOR: ($o > $o > $o)).
% 22.37/3.41 thf(func_def_30, type, db2: !>[X0: $tType]:(X0)).
% 22.37/3.41 thf(func_def_31, type, vAND: ($o > $o > $o)).
% 22.37/3.41 thf(func_def_32, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 22.37/3.41 thf(func_def_33, type, vIMP: ($o > $o > $o)).
% 22.37/3.41 thf(func_def_34, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 22.37/3.41 thf(func_def_36, type, sK1: ($i > $i)).
% 22.37/3.41 thf(func_def_37, type, sK2: ($i > $i)).
% 22.37/3.41 thf(func_def_39, type, sK4: ($i > $i)).
% 22.37/3.41 thf(func_def_40, type, sK5: ($i > $i)).
% 22.37/3.41 thf(f1,axiom,(
% 22.37/3.41 ! [X0 : $i] : (irel @ X0 @ X0)),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 22.37/3.41 thf(f2,axiom,(
% 22.37/3.41 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 22.37/3.41 thf(f3,axiom,(
% 22.37/3.41 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mnot)).
% 22.37/3.41 thf(f4,axiom,(
% 22.37/3.41 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mor)).
% 22.37/3.41 thf(f5,axiom,(
% 22.37/3.41 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mand)).
% 22.37/3.41 thf(f6,axiom,(
% 22.37/3.41 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mimplies)).
% 22.37/3.41 thf(f7,axiom,(
% 22.37/3.41 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 22.37/3.41 thf(f8,axiom,(
% 22.37/3.41 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iatom)).
% 22.37/3.41 thf(f9,axiom,(
% 22.37/3.41 (inot = (^[X0 : ($i > $o)] : ((mnot @ (mbox_s4 @ X0)))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',inot)).
% 22.37/3.41 thf(f12,axiom,(
% 22.37/3.41 (iand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ X0 @ X1))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iand)).
% 22.37/3.41 thf(f13,axiom,(
% 22.37/3.41 (ior = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ior)).
% 22.37/3.41 thf(f14,axiom,(
% 22.37/3.41 (iimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iimplies)).
% 22.37/3.41 thf(f18,axiom,(
% 22.37/3.41 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 22.37/3.41 thf(f22,conjecture,(
% 22.37/3.41 (ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))),
% 22.37/3.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel9)).
% 22.37/3.41 thf(f23,negated_conjecture,(
% 22.37/3.41 ~(ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))),
% 22.37/3.41 inference(negated_conjecture,[status(cth)],[f22])).
% 22.37/3.41 thf(f24,plain,(
% 22.37/3.41 ! [X0 : $i] : (irel @ X0 @ X0)),
% 22.37/3.41 inference(rectify,[],[f1])).
% 22.37/3.41 thf(f25,plain,(
% 22.37/3.41 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 22.37/3.41 inference(fool_elimination,[],[f24])).
% 22.37/3.41 thf(f26,plain,(
% 22.37/3.41 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 22.37/3.41 inference(rectify,[],[f2])).
% 22.37/3.41 thf(f27,plain,(
% 22.37/3.41 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 22.37/3.41 inference(fool_elimination,[],[f26])).
% 22.37/3.41 thf(f28,plain,(
% 22.37/3.41 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 22.37/3.41 inference(rectify,[],[f3])).
% 22.37/3.42 thf(f29,plain,(
% 22.37/3.42 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 22.37/3.42 inference(fool_elimination,[],[f28])).
% 22.37/3.42 thf(f30,plain,(
% 22.37/3.42 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 22.37/3.42 inference(rectify,[],[f4])).
% 22.37/3.42 thf(f31,plain,(
% 22.37/3.42 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 22.37/3.42 inference(fool_elimination,[],[f30])).
% 22.37/3.42 thf(f32,plain,(
% 22.37/3.42 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 22.37/3.42 inference(rectify,[],[f5])).
% 22.37/3.42 thf(f33,plain,(
% 22.37/3.42 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 22.37/3.42 inference(fool_elimination,[],[f32])).
% 22.37/3.42 thf(f34,plain,(
% 22.37/3.42 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 22.37/3.42 inference(fool_elimination,[],[f6])).
% 22.37/3.42 thf(f35,plain,(
% 22.37/3.42 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 22.37/3.42 inference(rectify,[],[f7])).
% 22.37/3.42 thf(f36,plain,(
% 22.37/3.42 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 22.37/3.42 inference(fool_elimination,[],[f35])).
% 22.37/3.42 thf(f37,plain,(
% 22.37/3.42 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 22.37/3.42 inference(fool_elimination,[],[f8])).
% 22.37/3.42 thf(f38,plain,(
% 22.37/3.42 (inot = (^[Y0 : $i > $o]: (mnot @ (mbox_s4 @ Y0))))),
% 22.37/3.42 inference(fool_elimination,[],[f9])).
% 22.37/3.42 thf(f40,plain,(
% 22.37/3.42 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 22.37/3.42 inference(fool_elimination,[],[f12])).
% 22.37/3.42 thf(f41,plain,(
% 22.37/3.42 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 22.37/3.42 inference(fool_elimination,[],[f13])).
% 22.37/3.42 thf(f42,plain,(
% 22.37/3.42 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 22.37/3.42 inference(fool_elimination,[],[f14])).
% 22.37/3.42 thf(f46,plain,(
% 22.37/3.42 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 22.37/3.42 inference(rectify,[],[f18])).
% 22.37/3.42 thf(f47,plain,(
% 22.37/3.42 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 22.37/3.42 inference(fool_elimination,[],[f46])).
% 22.37/3.42 thf(f54,plain,(
% 22.37/3.42 ~(ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))),
% 22.37/3.42 inference(rectify,[],[f23])).
% 22.37/3.42 thf(f55,plain,(
% 22.37/3.42 ~ (((ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))) = $true)),
% 22.37/3.42 inference(fool_elimination,[],[f54])).
% 22.37/3.42 thf(f56,plain,(
% 22.37/3.42 (((ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))) != $true)),
% 22.37/3.42 inference(flattening,[],[f55])).
% 22.37/3.42 thf(f57,plain,(
% 22.37/3.42 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 22.37/3.42 inference(ennf_transformation,[],[f27])).
% 22.37/3.42 thf(f58,plain,(
% 22.37/3.42 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 22.37/3.42 inference(flattening,[],[f57])).
% 22.37/3.42 thf(f59,plain,(
% 22.37/3.42 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 22.37/3.42 inference(cnf_transformation,[],[f25])).
% 22.37/3.42 thf(f60,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) )),
% 22.37/3.42 inference(cnf_transformation,[],[f58])).
% 22.37/3.42 thf(f61,plain,(
% 22.37/3.42 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f29])).
% 22.37/3.42 thf(f62,plain,(
% 22.37/3.42 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f31])).
% 22.37/3.42 thf(f63,plain,(
% 22.37/3.42 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f33])).
% 22.37/3.42 thf(f64,plain,(
% 22.37/3.42 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 22.37/3.42 inference(cnf_transformation,[],[f34])).
% 22.37/3.42 thf(f65,plain,(
% 22.37/3.42 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f36])).
% 22.37/3.42 thf(f66,plain,(
% 22.37/3.42 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 22.37/3.42 inference(cnf_transformation,[],[f37])).
% 22.37/3.42 thf(f67,plain,(
% 22.37/3.42 (inot = (^[Y0 : $i > $o]: (mnot @ (mbox_s4 @ Y0))))),
% 22.37/3.42 inference(cnf_transformation,[],[f38])).
% 22.37/3.42 thf(f70,plain,(
% 22.37/3.42 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 22.37/3.42 inference(cnf_transformation,[],[f40])).
% 22.37/3.42 thf(f71,plain,(
% 22.37/3.42 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f41])).
% 22.37/3.42 thf(f72,plain,(
% 22.37/3.42 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 22.37/3.42 inference(cnf_transformation,[],[f42])).
% 22.37/3.42 thf(f76,plain,(
% 22.37/3.42 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 22.37/3.42 inference(cnf_transformation,[],[f47])).
% 22.37/3.42 thf(f80,plain,(
% 22.37/3.42 (((ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))) != $true)),
% 22.37/3.42 inference(cnf_transformation,[],[f56])).
% 22.37/3.42 thf(f82,definition,(
% 22.37/3.42 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 22.37/3.42 introduced(theory,[fool_exhaustiveness_axiom])).
% 22.37/3.42 thf(f83,plain,(
% 22.37/3.42 (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)))))),
% 22.37/3.42 inference(definition_unfolding,[],[f64,f62,f61])).
% 22.37/3.42 thf(f84,plain,(
% 22.37/3.42 (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))))),
% 22.37/3.42 inference(definition_unfolding,[],[f67,f61,f65])).
% 22.37/3.42 thf(f86,plain,(
% 22.37/3.42 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))))),
% 22.37/3.42 inference(definition_unfolding,[],[f70,f63])).
% 22.37/3.42 thf(f87,plain,(
% 22.37/3.42 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 22.37/3.42 inference(definition_unfolding,[],[f71,f62,f65,f65])).
% 22.37/3.42 thf(f88,plain,(
% 22.37/3.42 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 22.37/3.42 inference(definition_unfolding,[],[f72,f83,f65,f65])).
% 22.37/3.42 thf(f92,plain,(
% 22.37/3.42 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ p1) @ ((^[Y0 : $i > $o]: (Y0)) @ p2)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: (Y0)) @ p1)) @ ((^[Y0 : $i > $o]: (Y0)) @ p2)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ p1) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: (Y0)) @ p2))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: (Y0)) @ p1)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (Y1 @ Y2))))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (Y1 @ Y3))))))) @ Y0))) @ ((^[Y0 : $i > $o]: (Y0)) @ p2))))))))),
% 22.37/3.42 inference(definition_unfolding,[],[f80,f76,f88,f86,f87,f66,f66,f86,f87,f84,f66,f66,f87,f66,f84,f66,f84,f87,f84,f66,f84,f66])).
% 22.37/3.42 thf(f93,plain,(
% 22.37/3.42 ($true != ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))) & (((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))) & ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p2 @ Y3))))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (~ (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (p1 @ Y4)))))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (~ (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (p2 @ Y4)))))))))))))))))))))),
% 22.37/3.42 inference(beta-eta_normalization,[],[f92])).
% 22.37/3.42 thf(f94,plain,(
% 22.37/3.42 ($false = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))) & (((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))) & ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p2 @ Y3))))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (~ (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (p1 @ Y4)))))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (~ (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (p2 @ Y4)))))))))))))))))) @ sK0)))),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f93])).
% 22.37/3.42 thf(f95,plain,(
% 22.37/3.42 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p2 @ Y3)))))))))))))))))))),
% 22.37/3.42 inference(beta-eta_normalization,[],[f94])).
% 22.37/3.42 thf(f96,plain,(
% 22.37/3.42 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p2 @ Y3))))))))))))))))))),
% 22.37/3.42 inference(or_proxy_clausification,[],[f95])).
% 22.37/3.42 thf(f97,plain,(
% 22.37/3.42 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2)))))))))))))))))),
% 22.37/3.42 inference(or_proxy_clausification,[],[f95])).
% 22.37/3.42 thf(f98,plain,(
% 22.37/3.42 ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))))))))),
% 22.37/3.42 inference(not_proxy_clausification,[],[f97])).
% 22.37/3.42 thf(f99,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & (((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))) & ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))))) @ X1)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f98])).
% 22.37/3.42 thf(f100,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($true = (((irel @ sK0 @ X1) => (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))))) & (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))))) & ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))))))))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f99])).
% 22.37/3.42 thf(f101,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))))) & (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))))) & ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1)))))))))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f100])).
% 22.37/3.42 thf(f102,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))))) & ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))))))))) )),
% 22.37/3.42 inference(and_proxy_clausification,[],[f101])).
% 22.37/3.42 thf(f103,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0)))))))) )),
% 22.37/3.42 inference(and_proxy_clausification,[],[f101])).
% 22.37/3.42 thf(f104,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(or_proxy_clausification,[],[f103])).
% 22.37/3.42 thf(f105,plain,(
% 22.37/3.42 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f104])).
% 22.37/3.42 thf(f106,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))) @ X3)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f105])).
% 22.37/3.42 thf(f107,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((irel @ X1 @ X2) => (p2 @ X2)))) | ($true = (((irel @ X1 @ X3) => (p1 @ X3))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f106])).
% 22.37/3.42 thf(f108,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (p1 @ X3)))) | ($true = ((p2 @ X2)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f107])).
% 22.37/3.42 thf(f109,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p2 @ X2))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f108])).
% 22.37/3.42 thf(f110,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1)))))))))))) )),
% 22.37/3.42 inference(and_proxy_clausification,[],[f102])).
% 22.37/3.42 thf(f111,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0)))))))) )),
% 22.37/3.42 inference(and_proxy_clausification,[],[f102])).
% 22.37/3.42 thf(f112,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))))))) )),
% 22.37/3.42 inference(or_proxy_clausification,[],[f111])).
% 22.37/3.42 thf(f113,plain,(
% 22.37/3.42 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))))))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f112])).
% 22.37/3.42 thf(f114,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p2 @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))) @ X3)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f113])).
% 22.37/3.42 thf(f115,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((irel @ X1 @ X2) => (p2 @ X2)))) | ($true = (((irel @ X1 @ X3) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))))))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f114])).
% 22.37/3.42 thf(f116,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) | ($true = ((p2 @ X2)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f115])).
% 22.37/3.42 thf(f117,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((p2 @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f116])).
% 22.37/3.42 thf(f118,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((p2 @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(not_proxy_clausification,[],[f117])).
% 22.37/3.42 thf(f119,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((p2 @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))) @ (sK1 @ X3))))) )),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f118])).
% 22.37/3.42 thf(f120,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((p2 @ X2))) | ($false = (((irel @ X3 @ (sK1 @ X3)) => (p1 @ (sK1 @ X3)))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f119])).
% 22.37/3.42 thf(f121,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p2 @ X2))) | ($false = ((p1 @ (sK1 @ X3))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f120])).
% 22.37/3.42 thf(f122,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ X3 @ (sK1 @ X3)))) | ($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p2 @ X2)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f120])).
% 22.37/3.42 thf(f123,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1)))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(or_proxy_clausification,[],[f110])).
% 22.37/3.42 thf(f124,plain,(
% 22.37/3.42 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f123])).
% 22.37/3.42 thf(f125,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p1 @ Y0))) @ X3)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f124])).
% 22.37/3.42 thf(f126,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((irel @ X1 @ X2) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))))) | ($true = (((irel @ X1 @ X3) => (p1 @ X3))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f125])).
% 22.37/3.42 thf(f127,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (p1 @ X3)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f126])).
% 22.37/3.42 thf(f128,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))))))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f127])).
% 22.37/3.42 thf(f129,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(not_proxy_clausification,[],[f128])).
% 22.37/3.42 thf(f130,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))) @ (sK2 @ X2)))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f129])).
% 22.37/3.42 thf(f131,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((irel @ X2 @ (sK2 @ X2)) => (p2 @ (sK2 @ X2))))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f130])).
% 22.37/3.42 thf(f132,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($false = ((p2 @ (sK2 @ X2)))) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f131])).
% 22.37/3.42 thf(f133,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ X2 @ (sK2 @ X2)))) | ($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p1 @ X3)))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f131])).
% 22.37/3.42 thf(f134,plain,(
% 22.37/3.42 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3)))))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p2 @ Y3))))))))))))))) @ sK3)))),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f96])).
% 22.37/3.42 thf(f135,plain,(
% 22.37/3.42 ($false = (((irel @ sK0 @ sK3) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK3 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))))))))),
% 22.37/3.42 inference(beta-eta_normalization,[],[f134])).
% 22.37/3.42 thf(f136,plain,(
% 22.37/3.42 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK3 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2)))))))))))))))),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f135])).
% 22.37/3.42 thf(f137,plain,(
% 22.37/3.42 ($true = ((irel @ sK0 @ sK3)))),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f135])).
% 22.37/3.42 thf(f138,plain,(
% 22.37/3.42 ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK3 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))))))),
% 22.37/3.42 inference(not_proxy_clausification,[],[f136])).
% 22.37/3.42 thf(f139,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK3 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p2 @ Y2))))))))))) @ X1)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f138])).
% 22.37/3.42 thf(f140,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($true = (((irel @ sK3 @ X1) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))))))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f139])).
% 22.37/3.42 thf(f141,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1)))))))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f140])).
% 22.37/3.42 thf(f142,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1)))))))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))))))) )),
% 22.37/3.42 inference(or_proxy_clausification,[],[f141])).
% 22.37/3.42 thf(f143,plain,(
% 22.37/3.42 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))))))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f142])).
% 22.37/3.42 thf(f144,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p2 @ Y1))))))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))))) @ X3)))) )),
% 22.37/3.42 inference(pi_proxy_clausification,[],[f143])).
% 22.37/3.42 thf(f145,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = (((irel @ X1 @ X2) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))))) | ($true = (((irel @ X1 @ X3) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))))))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f144])).
% 22.37/3.42 thf(f146,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f145])).
% 22.37/3.42 thf(f147,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f146])).
% 22.37/3.42 thf(f148,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0)))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) )),
% 22.37/3.42 inference(not_proxy_clausification,[],[f147])).
% 22.37/3.42 thf(f149,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))) @ (sK4 @ X2)))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0)))))))) )),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f148])).
% 22.37/3.42 thf(f150,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))) @ (sK4 @ X2)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))))))) )),
% 22.37/3.42 inference(not_proxy_clausification,[],[f149])).
% 22.37/3.42 thf(f151,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (p2 @ Y0))) @ (sK4 @ X2)))) | ($false = (((^[Y0 : $i]: ((irel @ X3 @ Y0) => (p1 @ Y0))) @ (sK5 @ X3))))) )),
% 22.37/3.42 inference(sigma_proxy_clausification,[],[f150])).
% 22.37/3.42 thf(f152,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = (((irel @ X2 @ (sK4 @ X2)) => (p2 @ (sK4 @ X2))))) | ($false = (((irel @ X3 @ (sK5 @ X3)) => (p1 @ (sK5 @ X3)))))) )),
% 22.37/3.42 inference(beta-eta_normalization,[],[f151])).
% 22.37/3.42 thf(f153,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($false = ((p2 @ (sK4 @ X2)))) | ($false = (((irel @ X3 @ (sK5 @ X3)) => (p1 @ (sK5 @ X3)))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f152])).
% 22.37/3.42 thf(f154,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((irel @ X2 @ (sK4 @ X2)))) | ($false = (((irel @ X3 @ (sK5 @ X3)) => (p1 @ (sK5 @ X3)))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f152])).
% 22.37/3.42 thf(f155,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ X2 @ (sK4 @ X2)))) | ($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($false = ((p1 @ (sK5 @ X3))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f154])).
% 22.37/3.42 thf(f156,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X1 @ X3))) | ($true = ((irel @ X2 @ (sK4 @ X2)))) | ($true = ((irel @ X3 @ (sK5 @ X3))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f154])).
% 22.37/3.42 thf(f157,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($false = ((p2 @ (sK4 @ X2)))) | ($false = ((p1 @ (sK5 @ X3))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f153])).
% 22.37/3.42 thf(f158,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((irel @ X3 @ (sK5 @ X3)))) | ($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($false = ((p2 @ (sK4 @ X2))))) )),
% 22.37/3.42 inference(imp_proxy_clausification,[],[f153])).
% 22.37/3.42 thf(f166,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(constrained_superposition,[],[f60,f82])).
% 22.37/3.42 thf(f167,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK3))) | ($true != ((irel @ X0 @ sK0)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f60,f137])).
% 22.37/3.42 thf(f169,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK0))) | ($true = ((irel @ X0 @ sK3)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f167])).
% 22.37/3.42 thf(f170,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X2 @ X0))) | ($true = ((irel @ X2 @ X1))) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f166])).
% 22.37/3.42 thf(f175,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) = $false) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(constrained_superposition,[],[f170,f82])).
% 22.37/3.42 thf(f180,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) = $false) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f175])).
% 22.37/3.42 thf(f233,definition,(
% 22.37/3.42 spl6_2 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p1 @ X0))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 22.37/3.42 thf(f234,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p1 @ X0)))) ) | ~spl6_2),
% 22.37/3.42 inference(avatar_component_clause,[],[f233])).
% 22.37/3.42 thf(f236,definition,(
% 22.37/3.42 spl6_3 <=> ($false = ((irel @ sK0 @ sK0)))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 22.37/3.42 thf(f237,plain,(
% 22.37/3.42 ($false != ((irel @ sK0 @ sK0))) | spl6_3),
% 22.37/3.42 inference(avatar_component_clause,[],[f236])).
% 22.37/3.42 thf(f238,plain,(
% 22.37/3.42 ($false = ((irel @ sK0 @ sK0))) | ~spl6_3),
% 22.37/3.42 inference(avatar_component_clause,[],[f236])).
% 22.37/3.42 thf(f245,definition,(
% 22.37/3.42 spl6_5 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition])).
% 22.37/3.42 thf(f246,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0)))) ) | ~spl6_5),
% 22.37/3.42 inference(avatar_component_clause,[],[f245])).
% 22.37/3.42 thf(f265,plain,(
% 22.37/3.42 ($true = $false) | ~spl6_3),
% 22.37/3.42 inference(constrained_superposition,[],[f238,f59])).
% 22.37/3.42 thf(f272,plain,(
% 22.37/3.42 $false | ~spl6_3),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f265])).
% 22.37/3.42 thf(f273,plain,(
% 22.37/3.42 ~spl6_3),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f272])).
% 22.37/3.42 thf(f276,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false != $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p2 @ X1))) | ($true = ((p1 @ X0)))) ) | spl6_3),
% 22.37/3.42 inference(constrained_superposition,[],[f237,f109])).
% 22.37/3.42 thf(f278,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p2 @ X1))) | ($true = ((p1 @ X0)))) ) | spl6_3),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f276])).
% 22.37/3.42 thf(f279,plain,(
% 22.37/3.42 spl6_5 | spl6_2 | spl6_3),
% 22.37/3.42 inference(avatar_split_clause,[],[f278,f236,f233,f245])).
% 22.37/3.42 thf(f297,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X0 @ X3)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f170,f180])).
% 22.37/3.42 thf(f298,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X1 @ sK0))) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(constrained_superposition,[],[f169,f180])).
% 22.37/3.42 thf(f299,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X0 @ sK0)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f137,f180])).
% 22.37/3.42 thf(f316,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X0 @ sK0)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f299])).
% 22.37/3.42 thf(f317,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X1 @ sK0))) | (((irel @ X0 @ X1)) = $false)) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f298])).
% 22.37/3.42 thf(f318,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) = $false) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ X0 @ X3)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f297])).
% 22.37/3.42 thf(f366,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ X1 @ X0))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p2 @ X0)))) ) | ~spl6_5),
% 22.37/3.42 inference(constrained_superposition,[],[f180,f246])).
% 22.37/3.42 thf(f368,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ X1 @ X0))) | ($true = ((p2 @ X0)))) ) | ~spl6_5),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f366])).
% 22.37/3.42 thf(f401,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $true) | ($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X0 @ sK0)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f180,f316])).
% 22.37/3.42 thf(f404,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $true) | ($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X0 @ sK0)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f401])).
% 22.37/3.42 thf(f418,definition,(
% 22.37/3.42 spl6_8 <=> ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p2 @ X1))) | (((irel @ X0 @ X1)) = $false))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition])).
% 22.37/3.42 thf(f419,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | (((irel @ X0 @ X1)) = $false) | ($true = ((p2 @ X1)))) ) | ~spl6_8),
% 22.37/3.42 inference(avatar_component_clause,[],[f418])).
% 22.37/3.42 thf(f679,definition,(
% 22.37/3.42 spl6_9 <=> ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = ((p2 @ X1))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition])).
% 22.37/3.42 thf(f680,plain,(
% 22.37/3.42 ( ! [X1 : $i] : (($false = ((irel @ sK3 @ X1))) | ($true = ((p2 @ X1)))) ) | ~spl6_9),
% 22.37/3.42 inference(avatar_component_clause,[],[f679])).
% 22.37/3.42 thf(f682,definition,(
% 22.37/3.42 spl6_10 <=> ! [X2 : $i,X0 : $i] : (($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X2))) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK0 @ X0))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition])).
% 22.37/3.42 thf(f683,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p1 @ X2)))) ) | ~spl6_10),
% 22.37/3.42 inference(avatar_component_clause,[],[f682])).
% 22.37/3.42 thf(f806,definition,(
% 22.37/3.42 spl6_12 <=> ! [X2 : $i] : (($false = ((irel @ sK3 @ X2))) | ($true = ((p1 @ X2))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_12])],[avatar_definition])).
% 22.37/3.42 thf(f807,plain,(
% 22.37/3.42 ( ! [X2 : $i] : (($false = ((irel @ sK3 @ X2))) | ($true = ((p1 @ X2)))) ) | ~spl6_12),
% 22.37/3.42 inference(avatar_component_clause,[],[f806])).
% 22.37/3.42 thf(f809,definition,(
% 22.37/3.42 spl6_13 <=> ! [X0 : $i] : (($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ sK0 @ X0))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition])).
% 22.37/3.42 thf(f810,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ sK0 @ X0)))) ) | ~spl6_13),
% 22.37/3.42 inference(avatar_component_clause,[],[f809])).
% 22.37/3.42 thf(f813,definition,(
% 22.37/3.42 spl6_14 <=> ! [X0 : $i,X1 : $i] : (($false = ((irel @ X1 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition])).
% 22.37/3.42 thf(f814,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ X1 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false)) ) | ~spl6_14),
% 22.37/3.42 inference(avatar_component_clause,[],[f813])).
% 22.37/3.42 thf(f935,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($true = ((p2 @ X0))) | ($false = ((irel @ X1 @ X0))) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ sK0 @ X2)))) ) | ~spl6_5),
% 22.37/3.42 inference(constrained_superposition,[],[f246,f318])).
% 22.37/3.42 thf(f983,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ X0 @ sK0))) | (((irel @ X0 @ X1)) = $true) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ sK3 @ X2)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f316,f318])).
% 22.37/3.42 thf(f995,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ X0 @ sK0))) | (((irel @ X0 @ X1)) = $true) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ sK3 @ X2)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f983])).
% 22.37/3.42 thf(f1033,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X2))) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ X1 @ X0))) | ($true = ((p2 @ X0)))) ) | ~spl6_5),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f935])).
% 22.37/3.42 thf(f2511,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false != $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ sK0))) | ($false = ((p2 @ (sK2 @ sK0)))) | ($true = ((p1 @ X0)))) )),
% 22.37/3.42 inference(equality_factoring,[],[f132])).
% 22.37/3.42 thf(f2520,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ sK0))) | ($false = ((p2 @ (sK2 @ sK0)))) | ($true = ((p1 @ X0)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f2511])).
% 22.37/3.42 thf(f2578,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((p2 @ (sK2 @ sK0)))) | ($true = ((p1 @ X0)))) ) | spl6_3),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f2520,f237])).
% 22.37/3.42 thf(f2613,definition,(
% 22.37/3.42 spl6_30 <=> ($false = ((p2 @ (sK2 @ sK0))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_30])],[avatar_definition])).
% 22.37/3.42 thf(f2615,plain,(
% 22.37/3.42 ($false = ((p2 @ (sK2 @ sK0)))) | ~spl6_30),
% 22.37/3.42 inference(avatar_component_clause,[],[f2613])).
% 22.37/3.42 thf(f2618,plain,(
% 22.37/3.42 spl6_30 | spl6_2 | spl6_3),
% 22.37/3.42 inference(avatar_split_clause,[],[f2578,f236,f233,f2613])).
% 22.37/3.42 thf(f2648,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ X1 @ X0))) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ sK0 @ X2))) | ($true = ((p1 @ X0)))) ) | ~spl6_2),
% 22.37/3.42 inference(constrained_superposition,[],[f318,f234])).
% 22.37/3.42 thf(f2658,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X2))) | ($false = ((irel @ X2 @ X1))) | ($false = ((irel @ X1 @ X0))) | ($true = ((p1 @ X0)))) ) | ~spl6_2),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f2648])).
% 22.37/3.42 thf(f2965,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false != $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ sK3 @ sK3))) | ($false = ((p2 @ (sK4 @ sK3)))) | ($false = ((p1 @ (sK5 @ X0))))) )),
% 22.37/3.42 inference(equality_factoring,[],[f157])).
% 22.37/3.42 thf(f2974,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ sK3 @ sK3))) | ($false = ((p2 @ (sK4 @ sK3)))) | ($false = ((p1 @ (sK5 @ X0))))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f2965])).
% 22.37/3.42 thf(f3030,definition,(
% 22.37/3.42 spl6_31 <=> ($false = ((p2 @ (sK4 @ sK3))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_31])],[avatar_definition])).
% 22.37/3.42 thf(f3031,plain,(
% 22.37/3.42 ($false != ((p2 @ (sK4 @ sK3)))) | spl6_31),
% 22.37/3.42 inference(avatar_component_clause,[],[f3030])).
% 22.37/3.42 thf(f3032,plain,(
% 22.37/3.42 ($false = ((p2 @ (sK4 @ sK3)))) | ~spl6_31),
% 22.37/3.42 inference(avatar_component_clause,[],[f3030])).
% 22.37/3.42 thf(f3034,definition,(
% 22.37/3.42 spl6_32 <=> ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((p1 @ (sK5 @ X0)))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_32])],[avatar_definition])).
% 22.37/3.42 thf(f3035,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((p1 @ (sK5 @ X0))))) ) | ~spl6_32),
% 22.37/3.42 inference(avatar_component_clause,[],[f3034])).
% 22.37/3.42 thf(f3037,definition,(
% 22.37/3.42 spl6_33 <=> ($false = ((irel @ sK3 @ sK3)))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_33])],[avatar_definition])).
% 22.37/3.42 thf(f3038,plain,(
% 22.37/3.42 ($false != ((irel @ sK3 @ sK3))) | spl6_33),
% 22.37/3.42 inference(avatar_component_clause,[],[f3037])).
% 22.37/3.42 thf(f3039,plain,(
% 22.37/3.42 ($false = ((irel @ sK3 @ sK3))) | ~spl6_33),
% 22.37/3.42 inference(avatar_component_clause,[],[f3037])).
% 22.37/3.42 thf(f3042,definition,(
% 22.37/3.42 spl6_34 <=> ($false = ((p1 @ (sK5 @ sK3))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_34])],[avatar_definition])).
% 22.37/3.42 thf(f3043,plain,(
% 22.37/3.42 ($false != ((p1 @ (sK5 @ sK3)))) | spl6_34),
% 22.37/3.42 inference(avatar_component_clause,[],[f3042])).
% 22.37/3.42 thf(f3044,plain,(
% 22.37/3.42 ($false = ((p1 @ (sK5 @ sK3)))) | ~spl6_34),
% 22.37/3.42 inference(avatar_component_clause,[],[f3042])).
% 22.37/3.42 thf(f3049,plain,(
% 22.37/3.42 spl6_31 | spl6_33 | spl6_32),
% 22.37/3.42 inference(avatar_split_clause,[],[f2974,f3034,f3037,f3030])).
% 22.37/3.42 thf(f3054,plain,(
% 22.37/3.42 ($true = $false) | ~spl6_33),
% 22.37/3.42 inference(constrained_superposition,[],[f3039,f59])).
% 22.37/3.42 thf(f3086,plain,(
% 22.37/3.42 $false | ~spl6_33),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3054])).
% 22.37/3.42 thf(f3087,plain,(
% 22.37/3.42 ~spl6_33),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f3086])).
% 22.37/3.42 thf(f3332,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false != $false) | ($false = ((irel @ sK0 @ sK3))) | ($false = ((irel @ sK3 @ X0))) | ($true = ((p2 @ X0)))) ) | (~spl6_5 | spl6_33)),
% 22.37/3.42 inference(constrained_superposition,[],[f3038,f1033])).
% 22.37/3.42 thf(f3389,plain,(
% 22.37/3.42 ($true = $false) | ($false = ((p1 @ (sK5 @ sK3)))) | ~spl6_32),
% 22.37/3.42 inference(constrained_superposition,[],[f3035,f59])).
% 22.37/3.42 thf(f3426,plain,(
% 22.37/3.42 ($true = $false) | ($true = $false) | ~spl6_13),
% 22.37/3.42 inference(constrained_superposition,[],[f810,f59])).
% 22.37/3.42 thf(f3479,plain,(
% 22.37/3.42 ($true = $false) | ~spl6_13),
% 22.37/3.42 inference(duplicate_literal_removal,[],[f3426])).
% 22.37/3.42 thf(f3480,plain,(
% 22.37/3.42 $false | ~spl6_13),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3479])).
% 22.37/3.42 thf(f3481,plain,(
% 22.37/3.42 ~spl6_13),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f3480])).
% 22.37/3.42 thf(f3723,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false != $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((p2 @ (sK4 @ X1))))) )),
% 22.37/3.42 inference(equality_factoring,[],[f158])).
% 22.37/3.42 thf(f3724,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((p2 @ (sK4 @ X1))))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3723])).
% 22.37/3.42 thf(f3943,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ sK0 @ X0)))) ) | ~spl6_14),
% 22.37/3.42 inference(constrained_superposition,[],[f59,f814])).
% 22.37/3.42 thf(f3986,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ sK0 @ X0)))) ) | ~spl6_14),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3943])).
% 22.37/3.42 thf(f4035,plain,(
% 22.37/3.42 spl6_13 | ~spl6_14),
% 22.37/3.42 inference(avatar_split_clause,[],[f3986,f813,f809])).
% 22.37/3.42 thf(f4277,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false != $false) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = ((irel @ X1 @ (sK5 @ X1))))) )),
% 22.37/3.42 inference(equality_factoring,[],[f156])).
% 22.37/3.42 thf(f4278,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK5 @ X1)))) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1))))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f4277])).
% 22.37/3.42 thf(f4777,definition,(
% 22.37/3.42 spl6_57 <=> ($false = ((p1 @ (sK1 @ sK3))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_57])],[avatar_definition])).
% 22.37/3.42 thf(f4779,plain,(
% 22.37/3.42 ($false = ((p1 @ (sK1 @ sK3)))) | ~spl6_57),
% 22.37/3.42 inference(avatar_component_clause,[],[f4777])).
% 22.37/3.42 thf(f5522,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1))) | ($false = ((irel @ sK3 @ X1))) | ($false = ((irel @ X0 @ sK0)))) ) | ~spl6_10),
% 22.37/3.42 inference(constrained_superposition,[],[f683,f404])).
% 22.37/3.42 thf(f5614,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1))) | ($false = ((irel @ sK3 @ X1)))) ) | ~spl6_10),
% 22.37/3.42 inference(duplicate_literal_removal,[],[f5522])).
% 22.37/3.42 thf(f5615,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1))) | ($false = ((irel @ sK3 @ X1)))) ) | ~spl6_10),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f5614])).
% 22.37/3.42 thf(f6067,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($true = ((p2 @ (sK2 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1)))) ) | ~spl6_5),
% 22.37/3.42 inference(constrained_superposition,[],[f246,f133])).
% 22.37/3.42 thf(f6222,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = ((p2 @ (sK2 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1)))) ) | ~spl6_5),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f6067])).
% 22.37/3.42 thf(f6341,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1)))) ) | (~spl6_5 | ~spl6_30)),
% 22.37/3.42 inference(forward_demodulation,[],[f6222,f2615])).
% 22.37/3.42 thf(f6342,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((irel @ X0 @ sK0))) | ($true = ((p1 @ X1)))) ) | (~spl6_5 | ~spl6_30)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f6341])).
% 22.37/3.42 thf(f6360,plain,(
% 22.37/3.42 spl6_10 | ~spl6_5 | ~spl6_30),
% 22.37/3.42 inference(avatar_split_clause,[],[f6342,f2613,f245,f682])).
% 22.37/3.42 thf(f6987,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK3 @ X1))) | ($true = ((p1 @ X1))) | ($false = ((irel @ X2 @ sK0))) | (((irel @ X0 @ X2)) = $false)) ) | ~spl6_2),
% 22.37/3.42 inference(constrained_superposition,[],[f2658,f317])).
% 22.37/3.42 thf(f7124,plain,(
% 22.37/3.42 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK3 @ X1))) | ($true = ((p1 @ X1))) | ($false = ((irel @ X2 @ sK0))) | (((irel @ X0 @ X2)) = $false)) ) | ~spl6_2),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f6987])).
% 22.37/3.42 thf(f7571,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($false != $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((p1 @ (sK5 @ X1))))) )),
% 22.37/3.42 inference(equality_factoring,[],[f155])).
% 22.37/3.42 thf(f7572,plain,(
% 22.37/3.42 ( ! [X0 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK4 @ X1)))) | ($false = ((irel @ sK3 @ X0))) | (((irel @ X0 @ X1)) = $false) | ($false = ((p1 @ (sK5 @ X1))))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f7571])).
% 22.37/3.42 thf(f15335,definition,(
% 22.37/3.42 spl6_139 <=> ! [X2 : $i] : (($false = ((irel @ X2 @ sK3))) | ($false = ((irel @ sK3 @ X2))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_139])],[avatar_definition])).
% 22.37/3.42 thf(f15336,plain,(
% 22.37/3.42 ( ! [X2 : $i] : (($false = ((irel @ X2 @ sK3))) | ($false = ((irel @ sK3 @ X2)))) ) | ~spl6_139),
% 22.37/3.42 inference(avatar_component_clause,[],[f15335])).
% 22.37/3.42 thf(f18052,definition,(
% 22.37/3.42 spl6_147 <=> ($true = ((irel @ sK3 @ (sK4 @ sK3))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_147])],[avatar_definition])).
% 22.37/3.42 thf(f18054,plain,(
% 22.37/3.42 ($true = ((irel @ sK3 @ (sK4 @ sK3)))) | ~spl6_147),
% 22.37/3.42 inference(avatar_component_clause,[],[f18052])).
% 22.37/3.42 thf(f18136,plain,(
% 22.37/3.42 ($true = $false) | ($false = ((irel @ sK0 @ sK3))) | ($true = ((p2 @ (sK4 @ sK3)))) | (~spl6_5 | ~spl6_147)),
% 22.37/3.42 inference(constrained_superposition,[],[f368,f18054])).
% 22.37/3.42 thf(f18197,plain,(
% 22.37/3.42 ($false = ((irel @ sK0 @ sK3))) | ($true = ((p2 @ (sK4 @ sK3)))) | (~spl6_5 | ~spl6_147)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f18136])).
% 22.37/3.42 thf(f18294,plain,(
% 22.37/3.42 ($true = $false) | ($false = ((irel @ sK0 @ sK3))) | (~spl6_5 | ~spl6_31 | ~spl6_147)),
% 22.37/3.42 inference(forward_demodulation,[],[f18197,f3032])).
% 22.37/3.42 thf(f18295,plain,(
% 22.37/3.42 ($false = ((irel @ sK0 @ sK3))) | (~spl6_5 | ~spl6_31 | ~spl6_147)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f18294])).
% 22.37/3.42 thf(f18297,definition,(
% 22.37/3.42 spl6_151 <=> ($false = ((irel @ sK0 @ sK3)))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_151])],[avatar_definition])).
% 22.37/3.42 thf(f18298,plain,(
% 22.37/3.42 ($false != ((irel @ sK0 @ sK3))) | spl6_151),
% 22.37/3.42 inference(avatar_component_clause,[],[f18297])).
% 22.37/3.42 thf(f18299,plain,(
% 22.37/3.42 ($false = ((irel @ sK0 @ sK3))) | ~spl6_151),
% 22.37/3.42 inference(avatar_component_clause,[],[f18297])).
% 22.37/3.42 thf(f18358,plain,(
% 22.37/3.42 spl6_151 | ~spl6_5 | ~spl6_31 | ~spl6_147),
% 22.37/3.42 inference(avatar_split_clause,[],[f18295,f18052,f3030,f245,f18297])).
% 22.37/3.42 thf(f18473,plain,(
% 22.37/3.42 ($false = ((p1 @ (sK5 @ sK3)))) | ~spl6_32),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3389])).
% 22.37/3.42 thf(f18552,plain,(
% 22.37/3.42 $false | (~spl6_32 | spl6_34)),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f18473,f3043])).
% 22.37/3.42 thf(f18553,plain,(
% 22.37/3.42 ~spl6_32 | spl6_34),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f18552])).
% 22.37/3.42 thf(f18700,plain,(
% 22.37/3.42 spl6_12 | spl6_13 | ~spl6_10),
% 22.37/3.42 inference(avatar_split_clause,[],[f5615,f682,f809,f806])).
% 22.37/3.42 thf(f18726,plain,(
% 22.37/3.42 spl6_12 | spl6_14 | ~spl6_2),
% 22.37/3.42 inference(avatar_split_clause,[],[f7124,f233,f813,f806])).
% 22.37/3.42 thf(f19247,plain,(
% 22.37/3.42 ($true = $false) | ~spl6_151),
% 22.37/3.42 inference(constrained_superposition,[],[f18299,f137])).
% 22.37/3.42 thf(f19273,plain,(
% 22.37/3.42 $false | ~spl6_151),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f19247])).
% 22.37/3.42 thf(f19274,plain,(
% 22.37/3.42 ~spl6_151),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f19273])).
% 22.37/3.42 thf(f19296,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false != $false) | ($false = ((irel @ sK0 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0))) | ($false = ((p1 @ (sK1 @ sK3))))) ) | spl6_151),
% 22.37/3.42 inference(constrained_superposition,[],[f18298,f121])).
% 22.37/3.42 thf(f19353,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0))) | ($false = ((p1 @ (sK1 @ sK3))))) ) | spl6_151),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f19296])).
% 22.37/3.42 thf(f21606,plain,(
% 22.37/3.42 ($true = $false) | ($true = $false) | ~spl6_139),
% 22.37/3.42 inference(constrained_superposition,[],[f15336,f59])).
% 22.37/3.42 thf(f21713,plain,(
% 22.37/3.42 ($true = $false) | ~spl6_139),
% 22.37/3.42 inference(duplicate_literal_removal,[],[f21606])).
% 22.37/3.42 thf(f21714,plain,(
% 22.37/3.42 $false | ~spl6_139),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f21713])).
% 22.37/3.42 thf(f21715,plain,(
% 22.37/3.42 ~spl6_139),
% 22.37/3.42 inference(avatar_contradiction_clause,[],[f21714])).
% 22.37/3.42 thf(f21886,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p1 @ (sK5 @ sK3)))) | ($true = ((p2 @ (sK4 @ sK3))))) ) | ~spl6_9),
% 22.37/3.42 inference(constrained_superposition,[],[f7572,f680])).
% 22.37/3.42 thf(f22210,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p1 @ (sK5 @ sK3)))) | ($true = ((p2 @ (sK4 @ sK3))))) ) | ~spl6_9),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f21886])).
% 22.37/3.42 thf(f22450,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p1 @ (sK5 @ sK3))))) ) | (~spl6_9 | ~spl6_31)),
% 22.37/3.42 inference(forward_demodulation,[],[f22210,f3032])).
% 22.37/3.42 thf(f22451,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p1 @ (sK5 @ sK3))))) ) | (~spl6_9 | ~spl6_31)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f22450])).
% 22.37/3.42 thf(f22460,plain,(
% 22.37/3.42 spl6_34 | spl6_139 | ~spl6_9 | ~spl6_31),
% 22.37/3.42 inference(avatar_split_clause,[],[f22451,f3030,f679,f15335,f3042])).
% 22.37/3.42 thf(f26872,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($true = ((irel @ sK3 @ (sK4 @ sK3)))) | ($true = ((p1 @ (sK5 @ sK3))))) ) | ~spl6_12),
% 22.37/3.42 inference(constrained_superposition,[],[f4278,f807])).
% 22.37/3.42 thf(f27236,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($true = ((irel @ sK3 @ (sK4 @ sK3)))) | ($true = ((p1 @ (sK5 @ sK3))))) ) | ~spl6_12),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f26872])).
% 22.37/3.42 thf(f28592,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($true = ((irel @ sK3 @ (sK4 @ sK3))))) ) | (~spl6_12 | ~spl6_34)),
% 22.37/3.42 inference(forward_demodulation,[],[f27236,f3044])).
% 22.37/3.42 thf(f28593,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($true = ((irel @ sK3 @ (sK4 @ sK3))))) ) | (~spl6_12 | ~spl6_34)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f28592])).
% 22.37/3.42 thf(f28675,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0))) | ($false = ((p1 @ (sK1 @ sK3))))) ) | (spl6_3 | spl6_151)),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f19353,f237])).
% 22.37/3.42 thf(f28774,plain,(
% 22.37/3.42 spl6_147 | spl6_139 | ~spl6_12 | ~spl6_34),
% 22.37/3.42 inference(avatar_split_clause,[],[f28593,f3042,f806,f15335,f18052])).
% 22.37/3.42 thf(f28792,plain,(
% 22.37/3.42 spl6_57 | spl6_5 | spl6_3 | spl6_151),
% 22.37/3.42 inference(avatar_split_clause,[],[f28675,f18297,f236,f245,f4777])).
% 22.37/3.42 thf(f28912,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false != $false) | ($false = ((irel @ sK0 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0)))) ) | ~spl6_8),
% 22.37/3.42 inference(equality_factoring,[],[f419])).
% 22.37/3.42 thf(f28920,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ sK0))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0)))) ) | ~spl6_8),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f28912])).
% 22.37/3.42 thf(f29019,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p2 @ X0)))) ) | (spl6_3 | ~spl6_8)),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f28920,f237])).
% 22.37/3.42 thf(f29038,plain,(
% 22.37/3.42 spl6_5 | spl6_3 | ~spl6_8),
% 22.37/3.42 inference(avatar_split_clause,[],[f29019,f418,f236,f245])).
% 22.37/3.42 thf(f29146,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($true = ((irel @ X1 @ (sK1 @ X1)))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p2 @ X2))) | ($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ sK3 @ X3)))) )),
% 22.37/3.42 inference(constrained_superposition,[],[f122,f995])).
% 22.37/3.42 thf(f29510,plain,(
% 22.37/3.42 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK1 @ X1)))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X2)) = $false) | ($true = ((p2 @ X2))) | ($false = ((irel @ X0 @ sK0))) | ($false = ((irel @ X3 @ X1))) | ($false = ((irel @ sK3 @ X3)))) )),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f29146])).
% 22.37/3.42 thf(f29639,definition,(
% 22.37/3.42 spl6_223 <=> ! [X2 : $i,X1 : $i] : (($false = ((irel @ X2 @ X1))) | ($true = ((irel @ X1 @ (sK1 @ X1)))) | ($false = ((irel @ sK3 @ X2))))),
% 22.37/3.42 introduced(definition,[new_symbols(definition,[spl6_223])],[avatar_definition])).
% 22.37/3.42 thf(f29640,plain,(
% 22.37/3.42 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ X2 @ X1))) | ($true = ((irel @ X1 @ (sK1 @ X1)))) | ($false = ((irel @ sK3 @ X2)))) ) | ~spl6_223),
% 22.37/3.42 inference(avatar_component_clause,[],[f29639])).
% 22.37/3.42 thf(f29723,plain,(
% 22.37/3.42 spl6_8 | spl6_223),
% 22.37/3.42 inference(avatar_split_clause,[],[f29510,f29639,f418])).
% 22.37/3.42 thf(f30436,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ sK3))) | ($false = ((irel @ sK3 @ X0))) | ($true = ((p2 @ X0)))) ) | (~spl6_5 | spl6_33)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f3332])).
% 22.37/3.42 thf(f31301,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($true = ((p2 @ X0)))) ) | (~spl6_5 | spl6_33 | spl6_151)),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f30436,f18298])).
% 22.37/3.42 thf(f31754,plain,(
% 22.37/3.42 spl6_9 | ~spl6_5 | spl6_33 | spl6_151),
% 22.37/3.42 inference(avatar_split_clause,[],[f31301,f18297,f3037,f245,f679])).
% 22.37/3.42 thf(f41853,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($true = ((p1 @ (sK1 @ sK3)))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((irel @ sK3 @ X0)))) ) | (~spl6_12 | ~spl6_223)),
% 22.37/3.42 inference(constrained_superposition,[],[f807,f29640])).
% 22.37/3.42 thf(f41881,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = ((p1 @ (sK1 @ sK3)))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((irel @ sK3 @ X0)))) ) | (~spl6_12 | ~spl6_223)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f41853])).
% 22.37/3.42 thf(f42131,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ X0 @ sK3))) | ($false = ((irel @ sK3 @ X0)))) ) | (~spl6_12 | ~spl6_57 | ~spl6_223)),
% 22.37/3.42 inference(forward_demodulation,[],[f41881,f4779])).
% 22.37/3.42 thf(f42132,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ X0 @ sK3))) | ($false = ((irel @ sK3 @ X0)))) ) | (~spl6_12 | ~spl6_57 | ~spl6_223)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f42131])).
% 22.37/3.42 thf(f42174,plain,(
% 22.37/3.42 spl6_139 | ~spl6_12 | ~spl6_57 | ~spl6_223),
% 22.37/3.42 inference(avatar_split_clause,[],[f42132,f29639,f4777,f806,f15335])).
% 22.37/3.42 thf(f48201,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($true = ((p1 @ (sK5 @ sK3)))) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p2 @ (sK4 @ sK3))))) ) | ~spl6_12),
% 22.37/3.42 inference(constrained_superposition,[],[f807,f3724])).
% 22.37/3.42 thf(f48265,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = ((p1 @ (sK5 @ sK3)))) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3))) | ($false = ((p2 @ (sK4 @ sK3))))) ) | ~spl6_12),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f48201])).
% 22.37/3.42 thf(f48531,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = ((p1 @ (sK5 @ sK3)))) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3)))) ) | (~spl6_12 | spl6_31)),
% 22.37/3.42 inference(forward_subsumption_resolution,[],[f48265,f3031])).
% 22.37/3.42 thf(f48560,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3)))) ) | (~spl6_12 | spl6_31 | ~spl6_34)),
% 22.37/3.42 inference(forward_demodulation,[],[f48531,f3044])).
% 22.37/3.42 thf(f48561,plain,(
% 22.37/3.42 ( ! [X0 : $i] : (($false = ((irel @ sK3 @ X0))) | ($false = ((irel @ X0 @ sK3)))) ) | (~spl6_12 | spl6_31 | ~spl6_34)),
% 22.37/3.42 inference(trivial_inequality_removal,[],[f48560])).
% 22.37/3.42 thf(f48585,plain,(
% 22.37/3.42 spl6_139 | ~spl6_12 | spl6_31 | ~spl6_34),
% 22.37/3.42 inference(avatar_split_clause,[],[f48561,f3042,f3030,f806,f15335])).
% 22.37/3.42 cnf(s12, plain, ~spl6_3, inference(sat_conversion,[],[f273])).
% 22.37/3.42 cnf(s13, plain, spl6_2 | spl6_3 | spl6_5, inference(sat_conversion,[],[f279])).
% 22.37/3.42 cnf(s93, plain, spl6_2 | spl6_3 | spl6_30, inference(sat_conversion,[],[f2618])).
% 22.37/3.42 cnf(s115, plain, spl6_31 | spl6_32 | spl6_33, inference(sat_conversion,[],[f3049])).
% 22.37/3.42 cnf(s120, plain, ~spl6_33, inference(sat_conversion,[],[f3087])).
% 22.37/3.42 cnf(s135, plain, ~spl6_13, inference(sat_conversion,[],[f3481])).
% 22.37/3.42 cnf(s160, plain, spl6_13 | ~spl6_14, inference(sat_conversion,[],[f4035])).
% 22.37/3.42 cnf(s483, plain, ~spl6_5 | spl6_10 | ~spl6_30, inference(sat_conversion,[],[f6360])).
% 22.37/3.42 cnf(s988, plain, ~spl6_5 | ~spl6_31 | ~spl6_147 | spl6_151, inference(sat_conversion,[],[f18358])).
% 22.37/3.42 cnf(s1042, plain, ~spl6_32 | spl6_34, inference(sat_conversion,[],[f18553])).
% 22.37/3.42 cnf(s1160, plain, ~spl6_10 | spl6_12 | spl6_13, inference(sat_conversion,[],[f18700])).
% 22.37/3.42 cnf(s1182, plain, ~spl6_2 | spl6_12 | spl6_14, inference(sat_conversion,[],[f18726])).
% 22.37/3.42 cnf(s1310, plain, ~spl6_151, inference(sat_conversion,[],[f19274])).
% 22.37/3.42 cnf(s1514, plain, ~spl6_139, inference(sat_conversion,[],[f21715])).
% 22.37/3.42 cnf(s1600, plain, ~spl6_9 | ~spl6_31 | spl6_34 | spl6_139, inference(sat_conversion,[],[f22460])).
% 22.37/3.42 cnf(s2345, plain, ~spl6_12 | ~spl6_34 | spl6_139 | spl6_147, inference(sat_conversion,[],[f28774])).
% 22.37/3.42 cnf(s2357, plain, spl6_3 | spl6_5 | spl6_57 | spl6_151, inference(sat_conversion,[],[f28792])).
% 22.37/3.42 cnf(s2407, plain, spl6_3 | spl6_5 | ~spl6_8, inference(sat_conversion,[],[f29038])).
% 22.37/3.42 cnf(s2443, plain, spl6_8 | spl6_223, inference(sat_conversion,[],[f29723])).
% 22.37/3.42 cnf(s3034, plain, ~spl6_5 | spl6_9 | spl6_33 | spl6_151, inference(sat_conversion,[],[f31754])).
% 22.37/3.42 cnf(s4747, plain, ~spl6_12 | ~spl6_57 | spl6_139 | ~spl6_223, inference(sat_conversion,[],[f42174])).
% 22.37/3.42 cnf(s5488, plain, ~spl6_12 | spl6_31 | ~spl6_34 | spl6_139, inference(sat_conversion,[],[f48585])).
% 22.37/3.42 cnf(s5511, plain, ~spl6_5 | ~spl6_31 | ~spl6_147, inference(rat,[],[s988,s1310])).
% 22.37/3.42 cnf(s5533, plain, ~spl6_14, inference(rat,[],[s160,s135])).
% 22.37/3.42 cnf(s5537, plain, spl6_31 | spl6_32, inference(rat,[],[s115,s120])).
% 22.37/3.42 cnf(s5558, plain, spl6_5 | ~spl6_12, inference(rat,[],[s4747,s2443,s2357,s2407,s1514,s12,s1310])).
% 22.37/3.42 cnf(s5559, plain, spl6_31 | ~spl6_12, inference(rat,[],[s1042,s5537,s5488,s1514])).
% 22.37/3.42 cnf(s5560, plain, ~spl6_12, inference(rat,[],[s2345,s5511,s1600,s5559,s3034,s5558,s1514,s120,s1310])).
% 22.37/3.42 cnf(s5568, plain, ~spl6_2, inference(rat,[],[s1182,s5533,s5560])).
% 22.37/3.42 cnf(s5569, plain, ~spl6_10, inference(rat,[],[s1160,s135,s5560])).
% 22.37/3.42 cnf(s5580, plain, spl6_30, inference(rat,[],[s93,s12,s5568])).
% 22.37/3.42 cnf(s5583, plain, spl6_5, inference(rat,[],[s13,s12,s5568])).
% 22.37/3.42 cnf(s5586, plain, $false, inference(rat,[],[s483,s5583,s5580,s5569])).
% 22.37/3.42 thf(f48589,plain,(
% 22.37/3.42 $false),
% 22.37/3.42 inference(avatar_sat_refutation,[],[s5586])).
% 22.37/3.42 % SZS output end Proof for theBenchmark
% 22.37/3.42 % (927043)------------------------------
% 22.37/3.42 % (927043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.37/3.42 % (927043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.37/3.42 % (927043)CaDiCaL version: 2.1.3
% 22.37/3.42 % (927043)Termination reason: Refutation
% 22.37/3.42 % (927043)Time elapsed: 3.126 s
% 22.37/3.42 % (927043)Peak memory usage: 24 MB
% 22.37/3.42 % (927043)Instructions burned: 7458 (million)
% 22.37/3.42 % (927024)Success in time 3.189 s
% 22.37/3.42 % Vampire exiting
%------------------------------------------------------------------------------