%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV149^5 : 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 : n010.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:39:03 AM UTC 2026
% Result : Theorem 22.50s 3.42s
% Output : Refutation 22.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV149^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n010.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 15:17:18 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/0.91 % (2981979)Will run a generic schedule for satisfiability detection.
% 3.86/0.91 % (2981992)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3050885088:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.86/0.91 % (2981988)% WARNING: option uhcvi not known.
% 3.86/0.91 % (2981987)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1148974472_2999 on theBenchmark for (2999ds/0Mi)
% 3.86/0.91 % (2981988)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3864731548:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.86/0.91 % (2981991)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2191116132:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.86/0.91 % (2981989)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=358701950:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.86/0.91 % (2981990)dis+10_1_sil=32000:sp=arity:random_seed=2393533900:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.86/0.91 % (2981993)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3854054430:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.86/0.91 % (2981988)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.91 % (2981991)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.91 % Exception at run slice level
% 3.86/0.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.91 % (2981988)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.86/0.91 % (2981992)Instruction limit reached!
% 3.86/0.91 % (2981992)------------------------------
% 3.86/0.91 % (2981992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.91 % (2981992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.91 % (2981992)CaDiCaL version: 2.1.3
% 3.86/0.91 % (2981992)Termination reason: Instruction limit
% 3.86/0.91 % (2981992)Termination phase: Saturation
% 3.86/0.91 % (2981992)Time elapsed: 0.034 s
% 3.86/0.91 % (2981992)Peak memory usage: 12 MB
% 3.86/0.91 % (2981992)Instructions burned: 131 (million)
% 3.86/0.91 % (2982002)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2599198031:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.86/0.91 % (2982001)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4112403423:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.86/0.91 % Exception at run slice level
% 3.86/0.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.91 % (2981990)Instruction limit reached!
% 3.86/0.91 % (2981990)------------------------------
% 3.86/0.91 % (2981990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.91 % (2981990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.91 % (2981990)CaDiCaL version: 2.1.3
% 3.86/0.91 % (2981990)Termination reason: Instruction limit
% 3.86/0.91 % (2981990)Termination phase: Saturation
% 3.86/0.91 % (2981990)Time elapsed: 0.052 s
% 3.86/0.91 % (2981990)Peak memory usage: 12 MB
% 3.86/0.91 % (2981990)Instructions burned: 103 (million)
% 3.86/0.91 % (2981991)Instruction limit reached!
% 3.86/0.91 % (2981991)------------------------------
% 3.86/0.91 % (2981991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.91 % (2981991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.91 % (2981991)CaDiCaL version: 2.1.3
% 3.86/0.91 % (2981991)Termination reason: Instruction limit
% 3.86/0.91 % (2981991)Termination phase: Saturation
% 3.86/0.91 % (2981991)Time elapsed: 0.058 s
% 3.86/0.91 % (2981991)Peak memory usage: 12 MB
% 3.86/0.91 % (2981991)Instructions burned: 116 (million)
% 3.86/0.91 % (2982005)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=1598106662:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.86/0.91 % (2982005)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.91 % (2982005)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.86/0.91 % (2982009)ott-21_1_sil=16000:fs=off:random_seed=1573736314:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.86/0.91 % (2982002)Instruction limit reached!
% 15.35/2.50 % (2982002)------------------------------
% 15.35/2.50 % (2982002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.35/2.50 % (2982002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/2.50 % (2982002)CaDiCaL version: 2.1.3
% 15.35/2.50 % (2982002)Termination reason: Instruction limit
% 15.35/2.50 % (2982002)Termination phase: Saturation
% 15.35/2.50 % (2982002)Time elapsed: 0.036 s
% 15.35/2.50 % (2982002)Peak memory usage: 12 MB
% 15.35/2.50 % (2982002)Instructions burned: 131 (million)
% 15.35/2.50 % (2982012)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2574568926:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 15.35/2.50 % (2982022)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4159262471:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 15.35/2.50 % Exception at run slice level
% 15.35/2.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.35/2.50 % (2982030)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2650442439:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 15.35/2.50 % (2981993)Instruction limit reached!
% 15.35/2.50 % (2981993)------------------------------
% 15.35/2.50 % (2981993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.35/2.50 % (2981993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/2.50 % (2981993)CaDiCaL version: 2.1.3
% 15.35/2.50 % (2981993)Termination reason: Instruction limit
% 15.35/2.50 % (2981993)Termination phase: Saturation
% 15.35/2.50 % (2981993)Time elapsed: 0.099 s
% 15.35/2.50 % (2981993)Peak memory usage: 13 MB
% 15.35/2.50 % (2981993)Instructions burned: 159 (million)
% 15.35/2.50 % (2982038)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1301281962:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 15.35/2.50 % Exception at run slice level
% 15.35/2.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.35/2.50 % (2982050)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=2352388734: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)
% 15.35/2.50 % (2982050)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.35/2.50 % (2982009)Instruction limit reached!
% 15.35/2.50 % (2982009)------------------------------
% 15.35/2.50 % (2982009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.35/2.50 % (2982009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/2.50 % (2982009)CaDiCaL version: 2.1.3
% 15.35/2.50 % (2982009)Termination reason: Instruction limit
% 15.35/2.50 % (2982009)Termination phase: Saturation
% 15.35/2.50 % (2982009)Time elapsed: 0.096 s
% 15.35/2.50 % (2982009)Peak memory usage: 12 MB
% 15.35/2.50 % (2982009)Instructions burned: 182 (million)
% 15.35/2.50 % (2982071)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=861836668:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 15.35/2.50 % (2982071)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.35/2.50 % (2982012)Instruction limit reached!
% 15.35/2.50 % (2982012)------------------------------
% 15.35/2.50 % (2982012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.35/2.50 % (2982012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/2.50 % (2982012)CaDiCaL version: 2.1.3
% 15.35/2.50 % (2982012)Termination reason: Instruction limit
% 15.35/2.50 % (2982012)Termination phase: Saturation
% 15.35/2.50 % (2982012)Time elapsed: 0.241 s
% 15.35/2.50 % (2982012)Peak memory usage: 14 MB
% 15.35/2.50 % (2982012)Instructions burned: 477 (million)
% 15.35/2.50 % (2982126)fmb+10_1_sil=64000:random_seed=1426196395:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 15.35/2.50 % (2982126)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.35/2.50 % Exception at run slice level
% 15.35/2.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.35/2.50 % (2982134)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2313246672:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 15.35/2.50 % Exception at run slice level
% 15.35/2.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982005)Instruction limit reached!
% 22.50/3.42 % (2982005)------------------------------
% 22.50/3.42 % (2982005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982005)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982005)Termination reason: Instruction limit
% 22.50/3.42 % (2982005)Termination phase: Saturation
% 22.50/3.42 % (2982005)Time elapsed: 0.313 s
% 22.50/3.42 % (2982005)Peak memory usage: 15 MB
% 22.50/3.42 % (2982005)Instructions burned: 684 (million)
% 22.50/3.42 % (2982145)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2652299907:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982030)Instruction limit reached!
% 22.50/3.42 % (2982030)------------------------------
% 22.50/3.42 % (2982030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982030)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982030)Termination reason: Instruction limit
% 22.50/3.42 % (2982030)Termination phase: Saturation
% 22.50/3.42 % (2982030)Time elapsed: 0.296 s
% 22.50/3.42 % (2982030)Peak memory usage: 16 MB
% 22.50/3.42 % (2982030)Instructions burned: 1185 (million)
% 22.50/3.42 % (2982157)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3783553952:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 22.50/3.42 % (2982157)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.50/3.42 % (2982161)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=915465568:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 22.50/3.42 % (2982161)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 22.50/3.42 % (2982161)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.50/3.42 % (2982170)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3370076963:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982181)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=948116063:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982187)ott-2_1_sil=16000:newcnf=on:random_seed=2655856489:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 22.50/3.42 % (2982187)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.50/3.42 % (2982050)Instruction limit reached!
% 22.50/3.42 % (2982050)------------------------------
% 22.50/3.42 % (2982050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982050)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982050)Termination reason: Instruction limit
% 22.50/3.42 % (2982050)Termination phase: Saturation
% 22.50/3.42 % (2982050)Time elapsed: 0.335 s
% 22.50/3.42 % (2982050)Peak memory usage: 20 MB
% 22.50/3.42 % (2982050)Instructions burned: 692 (million)
% 22.50/3.42 % (2982189)ott+10_1_sil=32000:tgt=ground:random_seed=2892196284:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 22.50/3.42 % (2982071)Instruction limit reached!
% 22.50/3.42 % (2982071)------------------------------
% 22.50/3.42 % (2982071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982071)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982071)Termination reason: Instruction limit
% 22.50/3.42 % (2982071)Termination phase: Saturation
% 22.50/3.42 % (2982071)Time elapsed: 0.444 s
% 22.50/3.42 % (2982071)Peak memory usage: 16 MB
% 22.50/3.42 % (2982071)Instructions burned: 880 (million)
% 22.50/3.42 % (2982191)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2670808906:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982187)Instruction limit reached!
% 22.50/3.42 % (2982187)------------------------------
% 22.50/3.42 % (2982187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982187)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982187)Termination reason: Instruction limit
% 22.50/3.42 % (2982187)Termination phase: Saturation
% 22.50/3.42 % (2982187)Time elapsed: 0.215 s
% 22.50/3.42 % (2982187)Peak memory usage: 15 MB
% 22.50/3.42 % (2982187)Instructions burned: 872 (million)
% 22.50/3.42 % (2982193)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1202509324:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 22.50/3.42 % (2982193)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.50/3.42 % (2982194)dis+21_1_sil=32000:sas=cadical:random_seed=389804261:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi)
% 22.50/3.42 % (2982161)Instruction limit reached!
% 22.50/3.42 % (2982161)------------------------------
% 22.50/3.42 % (2982161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982161)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982161)Termination reason: Instruction limit
% 22.50/3.42 % (2982161)Termination phase: Saturation
% 22.50/3.42 % (2982161)Time elapsed: 0.664 s
% 22.50/3.42 % (2982161)Peak memory usage: 17 MB
% 22.50/3.42 % (2982161)Instructions burned: 1472 (million)
% 22.50/3.42 % (2982197)ott+11_1_sil=16000:gs=on:random_seed=3415466191:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 22.50/3.42 % (2982197)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.50/3.42 % (2982194)Instruction limit reached!
% 22.50/3.42 % (2982194)------------------------------
% 22.50/3.42 % (2982194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982194)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982194)Termination reason: Instruction limit
% 22.50/3.42 % (2982194)Termination phase: Saturation
% 22.50/3.42 % (2982194)Time elapsed: 0.888 s
% 22.50/3.42 % (2982194)Peak memory usage: 21 MB
% 22.50/3.42 % (2982194)Instructions burned: 3776 (million)
% 22.50/3.42 % (2982199)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3290725610:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982201)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4054547593:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi)
% 22.50/3.42 % (2982197)Instruction limit reached!
% 22.50/3.42 % (2982197)------------------------------
% 22.50/3.42 % (2982197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982197)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982197)Termination reason: Instruction limit
% 22.50/3.42 % (2982197)Termination phase: Saturation
% 22.50/3.42 % (2982197)Time elapsed: 0.993 s
% 22.50/3.42 % (2982197)Peak memory usage: 27 MB
% 22.50/3.42 % (2982197)Instructions burned: 2253 (million)
% 22.50/3.42 % (2982203)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4098421456:i=29340_2978 on theBenchmark for (2978ds/29340Mi)
% 22.50/3.42 % (2982193)Instruction limit reached!
% 22.50/3.42 % (2982193)------------------------------
% 22.50/3.42 % (2982193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982193)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982193)Termination reason: Instruction limit
% 22.50/3.42 % (2982193)Termination phase: Saturation
% 22.50/3.42 % (2982193)Time elapsed: 1.550 s
% 22.50/3.42 % (2982193)Peak memory usage: 19 MB
% 22.50/3.42 % (2982193)Instructions burned: 3513 (million)
% 22.50/3.42 % (2982205)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2665659686:i=5211_2977 on theBenchmark for (2977ds/5211Mi)
% 22.50/3.42 % (2982201)Instruction limit reached!
% 22.50/3.42 % (2982201)------------------------------
% 22.50/3.42 % (2982201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982201)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982201)Termination reason: Instruction limit
% 22.50/3.42 % (2982201)Termination phase: Saturation
% 22.50/3.42 % (2982201)Time elapsed: 0.932 s
% 22.50/3.42 % (2982201)Peak memory usage: 13 MB
% 22.50/3.42 % (2982201)Instructions burned: 4592 (million)
% 22.50/3.42 % (2982207)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3362134476:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982209)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=761616218:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982211)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=53818856:i=14071_2974 on theBenchmark for (2974ds/14071Mi)
% 22.50/3.42 % Exception at run slice level
% 22.50/3.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.50/3.42 % (2982213)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4259580352:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi)
% 22.50/3.42 % (2982157)Instruction limit reached!
% 22.50/3.42 % (2982157)------------------------------
% 22.50/3.42 % (2982157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982157)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982157)Termination reason: Instruction limit
% 22.50/3.42 % (2982157)Termination phase: Saturation
% 22.50/3.42 % (2982157)Time elapsed: 2.243 s
% 22.50/3.42 % (2982157)Peak memory usage: 21 MB
% 22.50/3.42 % (2982157)Instructions burned: 5131 (million)
% 22.50/3.42 % (2982215)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2952165050:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi)
% 22.50/3.42 % (2982189)Instruction limit reached!
% 22.50/3.42 % (2982189)------------------------------
% 22.50/3.42 % (2982189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2982189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2982189)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2982189)Termination reason: Instruction limit
% 22.50/3.42 % (2982189)Termination phase: Saturation
% 22.50/3.42 % (2982189)Time elapsed: 2.222 s
% 22.50/3.42 % (2982189)Peak memory usage: 24 MB
% 22.50/3.42 % (2982189)Instructions burned: 5115 (million)
% 22.50/3.42 % (2982217)dis+10_16:1_sil=16000:random_seed=3366236009:i=9155:fsr=off_2972 on theBenchmark for (2972ds/9155Mi)
% 22.50/3.42 % (2981988) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2981979-2981988"...
% 22.50/3.42 % (2981988)...printing done.
% 22.50/3.42 % (2981988)Refutation found. Thanks to Tanya!
% 22.50/3.42 % SZS status Theorem for theBenchmark
% 22.50/3.42 % SZS output start Proof for theBenchmark
% 22.50/3.42 thf(type_def_5, type, a: $tType).
% 22.50/3.42 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 22.50/3.42 thf(func_def_3, type, sK0: (a > a > $o)).
% 22.50/3.42 thf(func_def_4, type, sK1: (a > a > $o)).
% 22.50/3.42 thf(func_def_5, type, sK2: a).
% 22.50/3.42 thf(func_def_6, type, sK3: a).
% 22.50/3.42 thf(func_def_7, type, sK4: (a > $o)).
% 22.50/3.42 thf(func_def_8, type, sK5: (a > a > a > $o)).
% 22.50/3.42 thf(func_def_9, type, sK6: (a > a > a > $o)).
% 22.50/3.42 thf(func_def_10, type, sK7: (a > a > $o)).
% 22.50/3.42 thf(func_def_11, type, sK8: (a > a > $o)).
% 22.50/3.42 thf(func_def_12, type, sK9: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_13, type, sK10: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_14, type, sK11: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_15, type, vNOT: ($o > $o)).
% 22.50/3.42 thf(func_def_16, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 22.50/3.42 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 22.50/3.42 thf(func_def_18, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 22.50/3.42 thf(func_def_20, type, db1: !>[X0: $tType]:(X0)).
% 22.50/3.42 thf(func_def_21, type, db2: !>[X0: $tType]:(X0)).
% 22.50/3.42 thf(func_def_22, type, sK13: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_23, type, sK14: ((a > a) > a)).
% 22.50/3.42 thf(func_def_24, type, sK15: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_25, type, sK16: ((a > $o) > a)).
% 22.50/3.42 thf(func_def_26, type, sK17: ((a > a) > a)).
% 22.50/3.42 thf(func_def_27, type, sK18: ((a > a) > (a > $o) > a)).
% 22.50/3.42 thf(f1,conjecture,(
% 22.50/3.42 ! [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (! [X4 : (a > $o)] : ((! [X6 : a,X7 : a] : ((((X1 @ X6 @ X7) | (X0 @ X6 @ X7)) & (X4 @ X6)) => (X4 @ X7)) & ! [X5 : a] : (((X1 @ X2 @ X5) | (X0 @ X2 @ X5)) => (X4 @ X5))) => (X4 @ X3)) => ! [X4 : (a > $o)] : ((! [X6 : a,X7 : a] : (((! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X1 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11)) & ! [X5 : a] : ((X1 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7)) | ! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X0 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11)) & ! [X5 : a] : ((X0 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7))) & (X4 @ X6)) => (X4 @ X7)) & ! [X5 : a] : ((! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X1 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X1 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5)) | ! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X0 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X0 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5))) => (X4 @ X5))) => (X4 @ X3)))),
% 22.50/3.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM251B_pme)).
% 22.50/3.42 thf(f2,negated_conjecture,(
% 22.50/3.42 ~ ! [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (! [X4 : (a > $o)] : ((! [X6 : a,X7 : a] : ((((X1 @ X6 @ X7) | (X0 @ X6 @ X7)) & (X4 @ X6)) => (X4 @ X7)) & ! [X5 : a] : (((X1 @ X2 @ X5) | (X0 @ X2 @ X5)) => (X4 @ X5))) => (X4 @ X3)) => ! [X4 : (a > $o)] : ((! [X6 : a,X7 : a] : (((! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X1 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11)) & ! [X5 : a] : ((X1 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7)) | ! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X0 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11)) & ! [X5 : a] : ((X0 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7))) & (X4 @ X6)) => (X4 @ X7)) & ! [X5 : a] : ((! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X1 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X1 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5)) | ! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X0 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X0 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5))) => (X4 @ X5))) => (X4 @ X3)))),
% 22.50/3.42 inference(negated_conjecture,[status(cth)],[f1])).
% 22.50/3.42 thf(f3,plain,(
% 22.50/3.42 ~ ! [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (! [X4 : (a > $o)] : ((! [X5 : a,X6 : a] : ((((X1 @ X5 @ X6) | (X0 @ X5 @ X6)) & (X4 @ X5)) => (X4 @ X6)) & ! [X7 : a] : (((X1 @ X2 @ X7) | (X0 @ X2 @ X7)) => (X4 @ X7))) => (X4 @ X3)) => ! [X8 : (a > $o)] : ((! [X9 : a,X10 : a] : (((! [X11 : (a > $o)] : ((! [X12 : a,X13 : a] : (((X1 @ X12 @ X13) & (X11 @ X12)) => (X11 @ X13)) & ! [X14 : a] : ((X1 @ X9 @ X14) => (X11 @ X14))) => (X11 @ X10)) | ! [X15 : (a > $o)] : ((! [X16 : a,X17 : a] : (((X0 @ X16 @ X17) & (X15 @ X16)) => (X15 @ X17)) & ! [X18 : a] : ((X0 @ X9 @ X18) => (X15 @ X18))) => (X15 @ X10))) & (X8 @ X9)) => (X8 @ X10)) & ! [X19 : a] : ((! [X20 : (a > $o)] : ((! [X21 : a,X22 : a] : (((X1 @ X21 @ X22) & (X20 @ X21)) => (X20 @ X22)) & ! [X23 : a] : ((X1 @ X2 @ X23) => (X20 @ X23))) => (X20 @ X19)) | ! [X24 : (a > $o)] : ((! [X25 : a,X26 : a] : (((X0 @ X25 @ X26) & (X24 @ X25)) => (X24 @ X26)) & ! [X27 : a] : ((X0 @ X2 @ X27) => (X24 @ X27))) => (X24 @ X19))) => (X8 @ X19))) => (X8 @ X3)))),
% 22.50/3.42 inference(rectify,[],[f2])).
% 22.50/3.42 thf(f4,plain,(
% 22.50/3.42 ~ ! [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (! [X4 : (a > $o)] : ((! [X5 : a,X6 : a] : ((((((X1 @ X5 @ X6)) = $true) | (((X0 @ X5 @ X6)) = $true)) & (((X4 @ X5)) = $true)) => (((X4 @ X6)) = $true)) & ! [X7 : a] : (((((X1 @ X2 @ X7)) = $true) | (((X0 @ X2 @ X7)) = $true)) => (((X4 @ X7)) = $true))) => (((X4 @ X3)) = $true)) => ! [X8 : (a > $o)] : ((! [X9 : a,X10 : a] : (((! [X11 : (a > $o)] : ((! [X12 : a,X13 : a] : (((((X1 @ X12 @ X13)) = $true) & (((X11 @ X12)) = $true)) => (((X11 @ X13)) = $true)) & ! [X14 : a] : ((((X1 @ X9 @ X14)) = $true) => (((X11 @ X14)) = $true))) => (((X11 @ X10)) = $true)) | ! [X15 : (a > $o)] : ((! [X16 : a,X17 : a] : (((((X0 @ X16 @ X17)) = $true) & (((X15 @ X16)) = $true)) => (((X15 @ X17)) = $true)) & ! [X18 : a] : ((((X0 @ X9 @ X18)) = $true) => (((X15 @ X18)) = $true))) => (((X15 @ X10)) = $true))) & (((X8 @ X9)) = $true)) => (((X8 @ X10)) = $true)) & ! [X19 : a] : ((! [X20 : (a > $o)] : ((! [X21 : a,X22 : a] : (((((X1 @ X21 @ X22)) = $true) & (((X20 @ X21)) = $true)) => (((X20 @ X22)) = $true)) & ! [X23 : a] : ((((X1 @ X2 @ X23)) = $true) => (((X20 @ X23)) = $true))) => (((X20 @ X19)) = $true)) | ! [X24 : (a > $o)] : ((! [X25 : a,X26 : a] : (((((X0 @ X25 @ X26)) = $true) & (((X24 @ X25)) = $true)) => (((X24 @ X26)) = $true)) & ! [X27 : a] : ((((X0 @ X2 @ X27)) = $true) => (((X24 @ X27)) = $true))) => (((X24 @ X19)) = $true))) => (((X8 @ X19)) = $true))) => (((X8 @ X3)) = $true)))),
% 22.50/3.42 inference(fool_elimination,[],[f3])).
% 22.50/3.42 thf(f5,plain,(
% 22.50/3.42 ? [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (? [X8 : (a > $o)] : ((((X8 @ X3)) != $true) & (! [X9 : a,X10 : a] : ((((X8 @ X10)) = $true) | ((? [X11 : (a > $o)] : ((((X11 @ X10)) != $true) & (! [X12 : a,X13 : a] : ((((X11 @ X13)) = $true) | ((((X1 @ X12 @ X13)) != $true) | (((X11 @ X12)) != $true))) & ! [X14 : a] : ((((X11 @ X14)) = $true) | (((X1 @ X9 @ X14)) != $true)))) & ? [X15 : (a > $o)] : ((((X15 @ X10)) != $true) & (! [X16 : a,X17 : a] : ((((X15 @ X17)) = $true) | ((((X0 @ X16 @ X17)) != $true) | (((X15 @ X16)) != $true))) & ! [X18 : a] : ((((X15 @ X18)) = $true) | (((X0 @ X9 @ X18)) != $true))))) | (((X8 @ X9)) != $true))) & ! [X19 : a] : ((((X8 @ X19)) = $true) | (? [X20 : (a > $o)] : ((((X20 @ X19)) != $true) & (! [X21 : a,X22 : a] : ((((X20 @ X22)) = $true) | ((((X1 @ X21 @ X22)) != $true) | (((X20 @ X21)) != $true))) & ! [X23 : a] : ((((X20 @ X23)) = $true) | (((X1 @ X2 @ X23)) != $true)))) & ? [X24 : (a > $o)] : ((((X24 @ X19)) != $true) & (! [X25 : a,X26 : a] : ((((X24 @ X26)) = $true) | ((((X0 @ X25 @ X26)) != $true) | (((X24 @ X25)) != $true))) & ! [X27 : a] : ((((X24 @ X27)) = $true) | (((X0 @ X2 @ X27)) != $true)))))))) & ! [X4 : (a > $o)] : ((((X4 @ X3)) = $true) | (? [X5 : a,X6 : a] : ((((X4 @ X6)) != $true) & (((((X1 @ X5 @ X6)) = $true) | (((X0 @ X5 @ X6)) = $true)) & (((X4 @ X5)) = $true))) | ? [X7 : a] : ((((X4 @ X7)) != $true) & ((((X1 @ X2 @ X7)) = $true) | (((X0 @ X2 @ X7)) = $true))))))),
% 22.50/3.42 inference(ennf_transformation,[],[f4])).
% 22.50/3.42 thf(f6,plain,(
% 22.50/3.42 ? [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (? [X8 : (a > $o)] : ((((X8 @ X3)) != $true) & ! [X9 : a,X10 : a] : ((((X8 @ X10)) = $true) | (? [X11 : (a > $o)] : ((((X11 @ X10)) != $true) & ! [X12 : a,X13 : a] : ((((X11 @ X13)) = $true) | (((X1 @ X12 @ X13)) != $true) | (((X11 @ X12)) != $true)) & ! [X14 : a] : ((((X11 @ X14)) = $true) | (((X1 @ X9 @ X14)) != $true))) & ? [X15 : (a > $o)] : ((((X15 @ X10)) != $true) & ! [X16 : a,X17 : a] : ((((X15 @ X17)) = $true) | (((X0 @ X16 @ X17)) != $true) | (((X15 @ X16)) != $true)) & ! [X18 : a] : ((((X15 @ X18)) = $true) | (((X0 @ X9 @ X18)) != $true)))) | (((X8 @ X9)) != $true)) & ! [X19 : a] : ((((X8 @ X19)) = $true) | (? [X20 : (a > $o)] : ((((X20 @ X19)) != $true) & ! [X21 : a,X22 : a] : ((((X20 @ X22)) = $true) | (((X1 @ X21 @ X22)) != $true) | (((X20 @ X21)) != $true)) & ! [X23 : a] : ((((X20 @ X23)) = $true) | (((X1 @ X2 @ X23)) != $true))) & ? [X24 : (a > $o)] : ((((X24 @ X19)) != $true) & ! [X25 : a,X26 : a] : ((((X24 @ X26)) = $true) | (((X0 @ X25 @ X26)) != $true) | (((X24 @ X25)) != $true)) & ! [X27 : a] : ((((X24 @ X27)) = $true) | (((X0 @ X2 @ X27)) != $true)))))) & ! [X4 : (a > $o)] : ((((X4 @ X3)) = $true) | ? [X5 : a,X6 : a] : ((((X4 @ X6)) != $true) & ((((X1 @ X5 @ X6)) = $true) | (((X0 @ X5 @ X6)) = $true)) & (((X4 @ X5)) = $true)) | ? [X7 : a] : ((((X4 @ X7)) != $true) & ((((X1 @ X2 @ X7)) = $true) | (((X0 @ X2 @ X7)) = $true)))))),
% 22.50/3.42 inference(flattening,[],[f5])).
% 22.50/3.42 thf(f7,plain,(
% 22.50/3.42 ? [X0 : (a > a > $o),X1 : (a > a > $o),X2 : a,X3 : a] : (? [X4 : (a > $o)] : ((((X4 @ X3)) != $true) & ! [X5 : a,X6 : a] : ((((X4 @ X6)) = $true) | (? [X7 : (a > $o)] : (($true != ((X7 @ X6))) & ! [X8 : a,X9 : a] : (($true = ((X7 @ X9))) | ($true != ((X1 @ X8 @ X9))) | ($true != ((X7 @ X8)))) & ! [X10 : a] : (($true = ((X7 @ X10))) | ($true != ((X1 @ X5 @ X10))))) & ? [X11 : (a > $o)] : (($true != ((X11 @ X6))) & ! [X12 : a,X13 : a] : ((((X11 @ X13)) = $true) | ($true != ((X0 @ X12 @ X13))) | (((X11 @ X12)) != $true)) & ! [X14 : a] : ((((X11 @ X14)) = $true) | ($true != ((X0 @ X5 @ X14)))))) | (((X4 @ X5)) != $true)) & ! [X15 : a] : (($true = ((X4 @ X15))) | (? [X16 : (a > $o)] : (($true != ((X16 @ X15))) & ! [X17 : a,X18 : a] : (($true = ((X16 @ X18))) | ($true != ((X1 @ X17 @ X18))) | ($true != ((X16 @ X17)))) & ! [X19 : a] : (($true = ((X16 @ X19))) | ($true != ((X1 @ X2 @ X19))))) & ? [X20 : (a > $o)] : (($true != ((X20 @ X15))) & ! [X21 : a,X22 : a] : ((((X20 @ X22)) = $true) | ($true != ((X0 @ X21 @ X22))) | (((X20 @ X21)) != $true)) & ! [X23 : a] : ((((X20 @ X23)) = $true) | ($true != ((X0 @ X2 @ X23)))))))) & ! [X24 : (a > $o)] : (($true = ((X24 @ X3))) | ? [X25 : a,X26 : a] : ((((X24 @ X26)) != $true) & (($true = ((X1 @ X25 @ X26))) | (((X0 @ X25 @ X26)) = $true)) & (((X24 @ X25)) = $true)) | ? [X27 : a] : ((((X24 @ X27)) != $true) & (($true = ((X1 @ X2 @ X27))) | (((X0 @ X2 @ X27)) = $true)))))),
% 22.50/3.42 inference(rectify,[],[f6])).
% 22.50/3.42 thf(f8,plain,(
% 22.50/3.42 (($true != ((sK4 @ sK3))) & ! [X5 : a,X6 : a] : (($true = ((sK4 @ X6))) | ((($true != ((sK5 @ X6 @ X5 @ X6))) & ! [X8 : a,X9 : a] : (($true = ((sK5 @ X6 @ X5 @ X9))) | ($true != ((sK1 @ X8 @ X9))) | ($true != ((sK5 @ X6 @ X5 @ X8)))) & ! [X10 : a] : (($true = ((sK5 @ X6 @ X5 @ X10))) | ($true != ((sK1 @ X5 @ X10))))) & (($true != ((sK6 @ X6 @ X5 @ X6))) & ! [X12 : a,X13 : a] : (($true = ((sK6 @ X6 @ X5 @ X13))) | ($true != ((sK0 @ X12 @ X13))) | ($true != ((sK6 @ X6 @ X5 @ X12)))) & ! [X14 : a] : (($true = ((sK6 @ X6 @ X5 @ X14))) | ($true != ((sK0 @ X5 @ X14)))))) | ($true != ((sK4 @ X5)))) & ! [X15 : a] : (($true = ((sK4 @ X15))) | ((($true != ((sK7 @ X15 @ X15))) & ! [X17 : a,X18 : a] : (($true = ((sK7 @ X15 @ X18))) | ($true != ((sK1 @ X17 @ X18))) | ($true != ((sK7 @ X15 @ X17)))) & ! [X19 : a] : (($true = ((sK7 @ X15 @ X19))) | ($true != ((sK1 @ sK2 @ X19))))) & (($true != ((sK8 @ X15 @ X15))) & ! [X21 : a,X22 : a] : (($true = ((sK8 @ X15 @ X22))) | ($true != ((sK0 @ X21 @ X22))) | ($true != ((sK8 @ X15 @ X21)))) & ! [X23 : a] : (($true = ((sK8 @ X15 @ X23))) | ($true != ((sK0 @ sK2 @ X23)))))))) & ! [X24 : (a > $o)] : (($true = ((X24 @ sK3))) | (($true != ((X24 @ (sK10 @ X24)))) & (($true = ((sK1 @ (sK9 @ X24) @ (sK10 @ X24)))) | ($true = ((sK0 @ (sK9 @ X24) @ (sK10 @ X24))))) & ($true = ((X24 @ (sK9 @ X24))))) | (($true != ((X24 @ (sK11 @ X24)))) & (($true = ((sK1 @ sK2 @ (sK11 @ X24)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X24)))))))),
% 22.50/3.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24),skolemize(X27,sK11 @ X24)],[f7])).
% 22.50/3.42 thf(f9,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true = ((sK1 @ sK2 @ (sK11 @ X24)))) | ($true = ((X24 @ (sK9 @ X24)))) | ($true = ((X24 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK11 @ X24))))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f10,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true != ((X24 @ (sK11 @ X24)))) | ($true = ((X24 @ (sK9 @ X24)))) | ($true = ((X24 @ sK3)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f11,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true = ((sK1 @ (sK9 @ X24) @ (sK10 @ X24)))) | ($true = ((X24 @ sK3))) | ($true = ((sK0 @ (sK9 @ X24) @ (sK10 @ X24)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X24)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X24))))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f12,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true != ((X24 @ (sK11 @ X24)))) | ($true = ((sK1 @ (sK9 @ X24) @ (sK10 @ X24)))) | ($true = ((sK0 @ (sK9 @ X24) @ (sK10 @ X24)))) | ($true = ((X24 @ sK3)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f13,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true != ((X24 @ (sK10 @ X24)))) | ($true = ((X24 @ sK3))) | ($true = ((sK1 @ sK2 @ (sK11 @ X24)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X24))))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f14,plain,(
% 22.50/3.42 ( ! [X24 : (a > $o)] : (($true != ((X24 @ (sK11 @ X24)))) | ($true != ((X24 @ (sK10 @ X24)))) | ($true = ((X24 @ sK3)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f15,plain,(
% 22.50/3.42 ( ! [X15 : a,X23 : a] : (($true != ((sK0 @ sK2 @ X23))) | ($true = ((sK8 @ X15 @ X23))) | ($true = ((sK4 @ X15)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f17,plain,(
% 22.50/3.42 ( ! [X15 : a] : (($true != ((sK8 @ X15 @ X15))) | ($true = ((sK4 @ X15)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f18,plain,(
% 22.50/3.42 ( ! [X19 : a,X15 : a] : (($true != ((sK1 @ sK2 @ X19))) | ($true = ((sK7 @ X15 @ X19))) | ($true = ((sK4 @ X15)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f20,plain,(
% 22.50/3.42 ( ! [X15 : a] : (($true != ((sK7 @ X15 @ X15))) | ($true = ((sK4 @ X15)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f21,plain,(
% 22.50/3.42 ( ! [X6 : a,X14 : a,X5 : a] : (($true != ((sK0 @ X5 @ X14))) | ($true = ((sK6 @ X6 @ X5 @ X14))) | ($true = ((sK4 @ X6))) | ($true != ((sK4 @ X5)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f23,plain,(
% 22.50/3.42 ( ! [X6 : a,X5 : a] : (($true != ((sK6 @ X6 @ X5 @ X6))) | ($true = ((sK4 @ X6))) | ($true != ((sK4 @ X5)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f24,plain,(
% 22.50/3.42 ( ! [X10 : a,X6 : a,X5 : a] : (($true != ((sK1 @ X5 @ X10))) | ($true = ((sK5 @ X6 @ X5 @ X10))) | ($true = ((sK4 @ X6))) | ($true != ((sK4 @ X5)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f26,plain,(
% 22.50/3.42 ( ! [X6 : a,X5 : a] : (($true != ((sK5 @ X6 @ X5 @ X6))) | ($true = ((sK4 @ X6))) | ($true != ((sK4 @ X5)))) )),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f27,plain,(
% 22.50/3.42 ($true != ((sK4 @ sK3)))),
% 22.50/3.42 inference(cnf_transformation,[],[f8])).
% 22.50/3.42 thf(f29,definition,(
% 22.50/3.42 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 22.50/3.42 introduced(theory,[fool_exhaustiveness_axiom])).
% 22.50/3.42 thf(f179,definition,(
% 22.50/3.42 spl12_4 <=> ! [X0 : (a > $o)] : (($true = ((X0 @ (sK9 @ X0)))) | ($false = ((X0 @ (sK11 @ X0)))) | ($true = ((X0 @ sK3))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition])).
% 22.50/3.42 thf(f180,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true = ((X0 @ (sK9 @ X0)))) | ($false = ((X0 @ (sK11 @ X0)))) | ($true = ((X0 @ sK3)))) ) | ~spl12_4),
% 22.50/3.42 inference(avatar_component_clause,[],[f179])).
% 22.50/3.42 thf(f233,definition,(
% 22.50/3.42 spl12_12 <=> ! [X0 : (a > $o)] : (($true = ((X0 @ sK3))) | ($false = ((X0 @ (sK10 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition])).
% 22.50/3.42 thf(f234,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($false = ((X0 @ (sK10 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($true = ((X0 @ sK3)))) ) | ~spl12_12),
% 22.50/3.42 inference(avatar_component_clause,[],[f233])).
% 22.50/3.42 thf(f269,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK8 @ X1 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK0 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f15,f29])).
% 22.50/3.42 thf(f270,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK7 @ X1 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK1 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f18,f29])).
% 22.50/3.42 thf(f271,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($true != ((sK4 @ X1))) | ($false = ((sK6 @ X0 @ X1 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f23,f29])).
% 22.50/3.42 thf(f272,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($true != ((sK4 @ X1))) | ($false = ((sK5 @ X0 @ X1 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f26,f29])).
% 22.50/3.42 thf(f273,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | ($true = ((sK6 @ X2 @ X0 @ X1))) | ($true = ((sK4 @ X2))) | ($true != ((sK4 @ X0))) | ($false = ((sK0 @ X0 @ X1)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f21,f29])).
% 22.50/3.42 thf(f274,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | ($true = ((sK5 @ X2 @ X0 @ X1))) | ($true = ((sK4 @ X2))) | ($true != ((sK4 @ X0))) | ($false = ((sK1 @ X0 @ X1)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f24,f29])).
% 22.50/3.42 thf(f278,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((X0 @ (sK9 @ X0)))) | ($true = ((X0 @ sK3))) | ($false = ((X0 @ (sK11 @ X0))))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f10,f29])).
% 22.50/3.42 thf(f279,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((X0 @ sK3))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($false = ((X0 @ (sK10 @ X0))))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f13,f29])).
% 22.50/3.42 thf(f281,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true = ((X0 @ sK3))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($false = ((X0 @ (sK10 @ X0))))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f279])).
% 22.50/3.42 thf(f282,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o)] : (($true = ((X0 @ (sK9 @ X0)))) | ($true = ((X0 @ sK3))) | ($false = ((X0 @ (sK11 @ X0))))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f278])).
% 22.50/3.42 thf(f286,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sK4 @ X0))) | ($true = ((sK4 @ X2))) | ($true = ((sK5 @ X2 @ X0 @ X1))) | ($false = ((sK1 @ X0 @ X1)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f274])).
% 22.50/3.42 thf(f287,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sK4 @ X0))) | ($true = ((sK4 @ X2))) | ($true = ((sK6 @ X2 @ X0 @ X1))) | ($false = ((sK0 @ X0 @ X1)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f273])).
% 22.50/3.42 thf(f288,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != ((sK4 @ X1))) | ($true = ((sK4 @ X0))) | ($false = ((sK5 @ X0 @ X1 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f272])).
% 22.50/3.42 thf(f289,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != ((sK4 @ X1))) | ($true = ((sK4 @ X0))) | ($false = ((sK6 @ X0 @ X1 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f271])).
% 22.50/3.42 thf(f290,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = ((sK7 @ X1 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK1 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f270])).
% 22.50/3.42 thf(f291,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = ((sK8 @ X1 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK0 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f269])).
% 22.50/3.42 thf(f303,plain,(
% 22.50/3.42 spl12_12),
% 22.50/3.42 inference(avatar_split_clause,[],[f281,f233])).
% 22.50/3.42 thf(f304,plain,(
% 22.50/3.42 spl12_4),
% 22.50/3.42 inference(avatar_split_clause,[],[f282,f179])).
% 22.50/3.42 thf(f360,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o),X1 : a] : (($true != $true) | ($true = ((sK5 @ X1 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK4 @ X1))) | ($true != ((sK4 @ (sK9 @ X0)))) | ($true = ((X0 @ sK3))) | ($true = ((sK0 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0))))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f24,f11])).
% 22.50/3.42 thf(f382,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o),X1 : a] : (($true != ((sK4 @ (sK9 @ X0)))) | ($true = ((sK4 @ X1))) | ($true = ((sK5 @ X1 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((X0 @ sK3))) | ($true = ((sK0 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0))))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f360])).
% 22.50/3.42 thf(f569,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($true = ((sK4 @ X0))) | ($false = ((sK1 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f20,f290])).
% 22.50/3.42 thf(f585,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK1 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(duplicate_literal_removal,[],[f569])).
% 22.50/3.42 thf(f586,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($false = ((sK1 @ sK2 @ X0))) | ($true = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f585])).
% 22.50/3.42 thf(f593,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f17,f291])).
% 22.50/3.42 thf(f609,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ sK2 @ X0)))) )),
% 22.50/3.42 inference(duplicate_literal_removal,[],[f593])).
% 22.50/3.42 thf(f610,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($false = ((sK0 @ sK2 @ X0))) | ($true = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f609])).
% 22.50/3.42 thf(f618,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X1))) | ($false = ((sK5 @ X1 @ X0 @ X1))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f288,f29])).
% 22.50/3.42 thf(f619,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($false = ((sK5 @ X1 @ X0 @ X1))) | ($true = ((sK4 @ X1))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f618])).
% 22.50/3.42 thf(f699,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X1))) | ($false = ((sK6 @ X1 @ X0 @ X1))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f289,f29])).
% 22.50/3.42 thf(f700,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($false = ((sK6 @ X1 @ X0 @ X1))) | ($true = ((sK4 @ X1))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f699])).
% 22.50/3.42 thf(f751,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X1))) | ($true = ((sK5 @ X1 @ X0 @ X2))) | ($false = ((sK1 @ X0 @ X2))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f286,f29])).
% 22.50/3.42 thf(f752,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true = ((sK5 @ X1 @ X0 @ X2))) | ($true = ((sK4 @ X1))) | ($false = ((sK1 @ X0 @ X2))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f751])).
% 22.50/3.42 thf(f759,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | ($true = ((sK4 @ X1))) | ($true = ((sK6 @ X1 @ X0 @ X2))) | ($false = ((sK0 @ X0 @ X2))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f287,f29])).
% 22.50/3.42 thf(f760,plain,(
% 22.50/3.42 ( ! [X2 : a,X0 : a,X1 : a] : (($true = ((sK6 @ X1 @ X0 @ X2))) | ($true = ((sK4 @ X1))) | ($false = ((sK0 @ X0 @ X2))) | ($false = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f759])).
% 22.50/3.42 thf(f2461,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o),X1 : a] : (($true != $true) | ($true = ((sK4 @ X1))) | ($true = ((sK5 @ X1 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((X0 @ sK3))) | ($true = ((sK0 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($false = ((sK4 @ (sK9 @ X0))))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f382,f29])).
% 22.50/3.42 thf(f2462,plain,(
% 22.50/3.42 ( ! [X0 : (a > $o),X1 : a] : (($true = ((sK5 @ X1 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK4 @ X1))) | ($true = ((X0 @ sK3))) | ($true = ((sK0 @ (sK9 @ X0) @ (sK10 @ X0)))) | ($true = ((sK1 @ sK2 @ (sK11 @ X0)))) | ($true = ((sK0 @ sK2 @ (sK11 @ X0)))) | ($false = ((sK4 @ (sK9 @ X0))))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f2461])).
% 22.50/3.42 thf(f2487,definition,(
% 22.50/3.42 spl12_39 <=> ($true = ((sK0 @ sK2 @ (sK11 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition])).
% 22.50/3.42 thf(f2488,plain,(
% 22.50/3.42 ($true != ((sK0 @ sK2 @ (sK11 @ sK4)))) | spl12_39),
% 22.50/3.42 inference(avatar_component_clause,[],[f2487])).
% 22.50/3.42 thf(f2489,plain,(
% 22.50/3.42 ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ~spl12_39),
% 22.50/3.42 inference(avatar_component_clause,[],[f2487])).
% 22.50/3.42 thf(f2491,definition,(
% 22.50/3.42 spl12_40 <=> ($true = ((sK1 @ sK2 @ (sK11 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition])).
% 22.50/3.42 thf(f2492,plain,(
% 22.50/3.42 ($true != ((sK1 @ sK2 @ (sK11 @ sK4)))) | spl12_40),
% 22.50/3.42 inference(avatar_component_clause,[],[f2491])).
% 22.50/3.42 thf(f2493,plain,(
% 22.50/3.42 ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ~spl12_40),
% 22.50/3.42 inference(avatar_component_clause,[],[f2491])).
% 22.50/3.42 thf(f2649,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK11 @ sK4)))) | ~spl12_39),
% 22.50/3.42 inference(constrained_superposition,[],[f2489,f610])).
% 22.50/3.42 thf(f2802,definition,(
% 22.50/3.42 spl12_48 <=> ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_48])],[avatar_definition])).
% 22.50/3.42 thf(f2804,plain,(
% 22.50/3.42 ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ~spl12_48),
% 22.50/3.42 inference(avatar_component_clause,[],[f2802])).
% 22.50/3.42 thf(f2806,definition,(
% 22.50/3.42 spl12_49 <=> ($true = ((sK1 @ (sK9 @ sK4) @ (sK10 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition])).
% 22.50/3.42 thf(f2808,plain,(
% 22.50/3.42 ($true = ((sK1 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ~spl12_49),
% 22.50/3.42 inference(avatar_component_clause,[],[f2806])).
% 22.50/3.42 thf(f4137,definition,(
% 22.50/3.42 spl12_66 <=> ($false = ((sK4 @ (sK11 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_66])],[avatar_definition])).
% 22.50/3.42 thf(f4138,plain,(
% 22.50/3.42 ($false != ((sK4 @ (sK11 @ sK4)))) | spl12_66),
% 22.50/3.42 inference(avatar_component_clause,[],[f4137])).
% 22.50/3.42 thf(f4139,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK11 @ sK4)))) | ~spl12_66),
% 22.50/3.42 inference(avatar_component_clause,[],[f4137])).
% 22.50/3.42 thf(f5320,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = $false) | ($true = ((sK4 @ X0))) | ($false = ((sK4 @ X1))) | ($true = ((sK4 @ X0))) | ($false = ((sK1 @ X1 @ X0))) | ($false = ((sK4 @ X1)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f619,f752])).
% 22.50/3.42 thf(f5350,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = $false) | ($true = ((sK4 @ X0))) | ($false = ((sK4 @ X1))) | ($false = ((sK1 @ X1 @ X0)))) )),
% 22.50/3.42 inference(duplicate_literal_removal,[],[f5320])).
% 22.50/3.42 thf(f5351,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($false = ((sK1 @ X1 @ X0))) | ($false = ((sK4 @ X1))) | ($true = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f5350])).
% 22.50/3.42 thf(f5363,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = $false) | ($true = ((sK4 @ X0))) | ($false = ((sK4 @ X1))) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ X1 @ X0))) | ($false = ((sK4 @ X1)))) )),
% 22.50/3.42 inference(constrained_superposition,[],[f700,f760])).
% 22.50/3.42 thf(f5393,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($true = $false) | ($true = ((sK4 @ X0))) | ($false = ((sK4 @ X1))) | ($false = ((sK0 @ X1 @ X0)))) )),
% 22.50/3.42 inference(duplicate_literal_removal,[],[f5363])).
% 22.50/3.42 thf(f5394,plain,(
% 22.50/3.42 ( ! [X0 : a,X1 : a] : (($false = ((sK0 @ X1 @ X0))) | ($false = ((sK4 @ X1))) | ($true = ((sK4 @ X0)))) )),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f5393])).
% 22.50/3.42 thf(f5884,definition,(
% 22.50/3.42 spl12_83 <=> ($true = ((sK4 @ (sK11 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_83])],[avatar_definition])).
% 22.50/3.42 thf(f5886,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK11 @ sK4)))) | ~spl12_83),
% 22.50/3.42 inference(avatar_component_clause,[],[f5884])).
% 22.50/3.42 thf(f5888,definition,(
% 22.50/3.42 spl12_84 <=> ($true = ((sK4 @ (sK9 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition])).
% 22.50/3.42 thf(f5890,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(avatar_component_clause,[],[f5888])).
% 22.50/3.42 thf(f6282,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK5 @ X0 @ (sK9 @ sK4) @ X0)))) ) | ~spl12_84),
% 22.50/3.42 inference(constrained_superposition,[],[f288,f5890])).
% 22.50/3.42 thf(f6317,plain,(
% 22.50/3.42 ( ! [X0 : a] : (($false = ((sK5 @ X0 @ (sK9 @ sK4) @ X0))) | ($true = ((sK4 @ X0)))) ) | ~spl12_84),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f6282])).
% 22.50/3.42 thf(f13673,definition,(
% 22.50/3.42 spl12_104 <=> ($true = ((sK4 @ (sK10 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_104])],[avatar_definition])).
% 22.50/3.42 thf(f13675,plain,(
% 22.50/3.42 ($true != ((sK4 @ (sK10 @ sK4)))) | spl12_104),
% 22.50/3.42 inference(avatar_component_clause,[],[f13673])).
% 22.50/3.42 thf(f25071,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(constrained_superposition,[],[f2462,f6317])).
% 22.50/3.42 thf(f25122,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(duplicate_literal_removal,[],[f25071])).
% 22.50/3.42 thf(f25123,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25122])).
% 22.50/3.42 thf(f25167,plain,(
% 22.50/3.42 ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25123,f13])).
% 22.50/3.42 thf(f25180,plain,(
% 22.50/3.42 ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | ~spl12_84),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25167,f27])).
% 22.50/3.42 thf(f25182,plain,(
% 22.50/3.42 ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | ($false = ((sK4 @ (sK9 @ sK4)))) | (spl12_39 | ~spl12_84)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25180,f2488])).
% 22.50/3.42 thf(f25184,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | (spl12_39 | ~spl12_84)),
% 22.50/3.42 inference(forward_demodulation,[],[f25182,f5890])).
% 22.50/3.42 thf(f25185,plain,(
% 22.50/3.42 ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK1 @ sK2 @ (sK11 @ sK4)))) | (spl12_39 | ~spl12_84)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25184])).
% 22.50/3.42 thf(f25507,plain,(
% 22.50/3.42 spl12_40 | spl12_48 | spl12_39 | ~spl12_84),
% 22.50/3.42 inference(avatar_split_clause,[],[f25185,f5888,f2487,f2802,f2491])).
% 22.50/3.42 thf(f25525,definition,(
% 22.50/3.42 spl12_151 <=> ($false = ((sK4 @ (sK9 @ sK4))))),
% 22.50/3.42 introduced(definition,[new_symbols(definition,[spl12_151])],[avatar_definition])).
% 22.50/3.42 thf(f25527,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK9 @ sK4)))) | ~spl12_151),
% 22.50/3.42 inference(avatar_component_clause,[],[f25525])).
% 22.50/3.42 thf(f25565,plain,(
% 22.50/3.42 ($true != $true) | ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(constrained_superposition,[],[f14,f5886])).
% 22.50/3.42 thf(f25567,plain,(
% 22.50/3.42 ($true != $true) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(constrained_superposition,[],[f10,f5886])).
% 22.50/3.42 thf(f25604,plain,(
% 22.50/3.42 ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25567])).
% 22.50/3.42 thf(f25605,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(beta-eta_normalization,[],[f25604])).
% 22.50/3.42 thf(f25608,plain,(
% 22.50/3.42 ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25565])).
% 22.50/3.42 thf(f25609,plain,(
% 22.50/3.42 ($true != ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(beta-eta_normalization,[],[f25608])).
% 22.50/3.42 thf(f25643,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | ~spl12_83),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25605,f27])).
% 22.50/3.42 thf(f25644,plain,(
% 22.50/3.42 ($true != ((sK4 @ (sK10 @ sK4)))) | ~spl12_83),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25609,f27])).
% 22.50/3.42 thf(f25646,plain,(
% 22.50/3.42 spl12_84 | ~spl12_83),
% 22.50/3.42 inference(avatar_split_clause,[],[f25643,f5884,f5888])).
% 22.50/3.42 thf(f25647,plain,(
% 22.50/3.42 ~spl12_104 | ~spl12_83),
% 22.50/3.42 inference(avatar_split_clause,[],[f25644,f5884,f13673])).
% 22.50/3.42 thf(f25657,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK11 @ sK4)))) | ~spl12_40),
% 22.50/3.42 inference(constrained_superposition,[],[f586,f2493])).
% 22.50/3.42 thf(f25724,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK11 @ sK4)))) | ~spl12_40),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25657])).
% 22.50/3.42 thf(f25740,plain,(
% 22.50/3.42 spl12_83 | ~spl12_40),
% 22.50/3.42 inference(avatar_split_clause,[],[f25724,f2491,f5884])).
% 22.50/3.42 thf(f25796,plain,(
% 22.50/3.42 ($true != $true) | ($false = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl12_12 | spl12_40)),
% 22.50/3.42 inference(constrained_superposition,[],[f2492,f234])).
% 22.50/3.42 thf(f25797,plain,(
% 22.50/3.42 ($true != $true) | ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | spl12_40),
% 22.50/3.42 inference(constrained_superposition,[],[f2492,f9])).
% 22.50/3.42 thf(f25855,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | spl12_40),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25797])).
% 22.50/3.42 thf(f25856,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl12_12 | spl12_40)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f25796])).
% 22.50/3.42 thf(f25861,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK11 @ sK4)))) | spl12_40),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25855,f27])).
% 22.50/3.42 thf(f25862,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl12_12 | spl12_39 | spl12_40)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25856,f2488])).
% 22.50/3.42 thf(f25867,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK9 @ sK4)))) | (spl12_39 | spl12_40)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25861,f2488])).
% 22.50/3.42 thf(f25868,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl12_12 | spl12_39 | spl12_40)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f25862,f27])).
% 22.50/3.42 thf(f25869,plain,(
% 22.50/3.42 spl12_84 | spl12_39 | spl12_40),
% 22.50/3.42 inference(avatar_split_clause,[],[f25867,f2491,f2487,f5888])).
% 22.50/3.42 thf(f28366,plain,(
% 22.50/3.42 ($true = $false) | ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_48),
% 22.50/3.42 inference(constrained_superposition,[],[f2804,f5394])).
% 22.50/3.42 thf(f28382,plain,(
% 22.50/3.42 ($true = $false) | ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_48),
% 22.50/3.42 inference(constrained_superposition,[],[f5394,f2804])).
% 22.50/3.42 thf(f28427,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_48),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28382])).
% 22.50/3.42 thf(f28448,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_48),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28366])).
% 22.50/3.42 thf(f28453,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(forward_demodulation,[],[f28427,f5890])).
% 22.50/3.42 thf(f28454,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28453])).
% 22.50/3.42 thf(f28471,plain,(
% 22.50/3.42 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(forward_demodulation,[],[f28448,f5890])).
% 22.50/3.42 thf(f28472,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28471])).
% 22.50/3.42 thf(f28482,plain,(
% 22.50/3.42 ($true = $false) | (~spl12_12 | spl12_39 | spl12_40 | ~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(forward_demodulation,[],[f28472,f25868])).
% 22.50/3.42 thf(f28483,plain,(
% 22.50/3.42 $false | (~spl12_12 | spl12_39 | spl12_40 | ~spl12_48 | ~spl12_84)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28482])).
% 22.50/3.42 thf(f28484,plain,(
% 22.50/3.42 ~spl12_12 | spl12_39 | spl12_40 | ~spl12_48 | ~spl12_84),
% 22.50/3.42 inference(avatar_contradiction_clause,[],[f28483])).
% 22.50/3.42 thf(f28485,plain,(
% 22.50/3.42 ($true = ((sK4 @ (sK11 @ sK4)))) | ~spl12_39),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f2649])).
% 22.50/3.42 thf(f28595,plain,(
% 22.50/3.42 spl12_104 | ~spl12_48 | ~spl12_84),
% 22.50/3.42 inference(avatar_split_clause,[],[f28454,f5888,f2802,f13673])).
% 22.50/3.42 thf(f28687,plain,(
% 22.50/3.42 ($true = $false) | (~spl12_66 | ~spl12_83)),
% 22.50/3.42 inference(forward_demodulation,[],[f5886,f4139])).
% 22.50/3.42 thf(f28688,plain,(
% 22.50/3.42 $false | (~spl12_66 | ~spl12_83)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f28687])).
% 22.50/3.42 thf(f28689,plain,(
% 22.50/3.42 ~spl12_66 | ~spl12_83),
% 22.50/3.42 inference(avatar_contradiction_clause,[],[f28688])).
% 22.50/3.42 thf(f28770,plain,(
% 22.50/3.42 spl12_83 | ~spl12_39),
% 22.50/3.42 inference(avatar_split_clause,[],[f28485,f2487,f5884])).
% 22.50/3.42 thf(f29381,plain,(
% 22.50/3.42 ($true != $true) | ($true = ((sK1 @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = ((sK0 @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(constrained_superposition,[],[f12,f5886])).
% 22.50/3.42 thf(f29430,plain,(
% 22.50/3.42 ($true = ((sK1 @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = ((sK0 @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f29381])).
% 22.50/3.42 thf(f29431,plain,(
% 22.50/3.42 ($true = ((sK1 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK3))) | ~spl12_83),
% 22.50/3.42 inference(beta-eta_normalization,[],[f29430])).
% 22.50/3.42 thf(f29462,plain,(
% 22.50/3.42 ($true = ((sK1 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ($true = ((sK0 @ (sK9 @ sK4) @ (sK10 @ sK4)))) | ~spl12_83),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f29431,f27])).
% 22.50/3.42 thf(f29463,plain,(
% 22.50/3.42 spl12_48 | spl12_49 | ~spl12_83),
% 22.50/3.42 inference(avatar_split_clause,[],[f29462,f5884,f2806,f2802])).
% 22.50/3.42 thf(f31984,plain,(
% 22.50/3.42 ($true = $false) | ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_49),
% 22.50/3.42 inference(constrained_superposition,[],[f5351,f2808])).
% 22.50/3.42 thf(f32032,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl12_49),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f31984])).
% 22.50/3.42 thf(f32055,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK9 @ sK4)))) | (~spl12_49 | spl12_104)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f32032,f13675])).
% 22.50/3.42 thf(f32073,plain,(
% 22.50/3.42 spl12_151 | ~spl12_49 | spl12_104),
% 22.50/3.42 inference(avatar_split_clause,[],[f32055,f13673,f2806,f25525])).
% 22.50/3.42 thf(f33607,plain,(
% 22.50/3.42 ($true = $false) | ($false = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (~spl12_4 | ~spl12_151)),
% 22.50/3.42 inference(constrained_superposition,[],[f25527,f180])).
% 22.50/3.42 thf(f33767,plain,(
% 22.50/3.42 ($false = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (~spl12_4 | ~spl12_151)),
% 22.50/3.42 inference(trivial_inequality_removal,[],[f33607])).
% 22.50/3.42 thf(f33768,plain,(
% 22.50/3.42 ($false = ((sK4 @ (sK11 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl12_4 | ~spl12_151)),
% 22.50/3.42 inference(beta-eta_normalization,[],[f33767])).
% 22.50/3.42 thf(f33779,plain,(
% 22.50/3.42 ($true = ((sK4 @ sK3))) | (~spl12_4 | spl12_66 | ~spl12_151)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f33768,f4138])).
% 22.50/3.42 thf(f33784,plain,(
% 22.50/3.42 $false | (~spl12_4 | spl12_66 | ~spl12_151)),
% 22.50/3.42 inference(forward_subsumption_resolution,[],[f33779,f27])).
% 22.50/3.42 thf(f33785,plain,(
% 22.50/3.42 ~spl12_4 | spl12_66 | ~spl12_151),
% 22.50/3.42 inference(avatar_contradiction_clause,[],[f33784])).
% 22.50/3.42 cnf(s10, plain, spl12_12, inference(sat_conversion,[],[f303])).
% 22.50/3.42 cnf(s11, plain, spl12_4, inference(sat_conversion,[],[f304])).
% 22.50/3.42 cnf(s337, plain, spl12_39 | spl12_40 | spl12_48 | ~spl12_84, inference(sat_conversion,[],[f25507])).
% 22.50/3.42 cnf(s354, plain, ~spl12_83 | spl12_84, inference(sat_conversion,[],[f25646])).
% 22.50/3.42 cnf(s355, plain, ~spl12_83 | ~spl12_104, inference(sat_conversion,[],[f25647])).
% 22.50/3.42 cnf(s359, plain, ~spl12_40 | spl12_83, inference(sat_conversion,[],[f25740])).
% 22.50/3.42 cnf(s362, plain, spl12_39 | spl12_40 | spl12_84, inference(sat_conversion,[],[f25869])).
% 22.50/3.42 cnf(s381, plain, ~spl12_12 | spl12_39 | spl12_40 | ~spl12_48 | ~spl12_84, inference(sat_conversion,[],[f28484])).
% 22.50/3.42 cnf(s404, plain, ~spl12_48 | ~spl12_84 | spl12_104, inference(sat_conversion,[],[f28595])).
% 22.50/3.42 cnf(s413, plain, ~spl12_66 | ~spl12_83, inference(sat_conversion,[],[f28689])).
% 22.50/3.42 cnf(s461, plain, ~spl12_39 | spl12_83, inference(sat_conversion,[],[f28770])).
% 22.50/3.42 cnf(s477, plain, spl12_48 | spl12_49 | ~spl12_83, inference(sat_conversion,[],[f29463])).
% 22.50/3.42 cnf(s495, plain, ~spl12_49 | spl12_104 | spl12_151, inference(sat_conversion,[],[f32073])).
% 22.50/3.42 cnf(s513, plain, ~spl12_4 | spl12_66 | ~spl12_151, inference(sat_conversion,[],[f33785])).
% 22.50/3.42 cnf(s520, plain, spl12_40 | ~spl12_84 | spl12_39, inference(rat,[],[s381,s337,s10])).
% 22.50/3.42 cnf(s521, plain, spl12_40 | spl12_39, inference(rat,[],[s520,s362])).
% 22.50/3.42 cnf(s522, plain, ~spl12_83, inference(rat,[],[s477,s404,s495,s513,s354,s355,s413,s11])).
% 22.50/3.42 cnf(s523, plain, ~spl12_39, inference(rat,[],[s461,s522])).
% 22.50/3.42 cnf(s525, plain, ~spl12_40, inference(rat,[],[s359,s522])).
% 22.50/3.42 cnf(s528, plain, $false, inference(rat,[],[s521,s523,s525])).
% 22.50/3.42 thf(f33786,plain,(
% 22.50/3.42 $false),
% 22.50/3.42 inference(avatar_sat_refutation,[],[s528])).
% 22.50/3.42 % SZS output end Proof for theBenchmark
% 22.50/3.42 % (2981988)------------------------------
% 22.50/3.42 % (2981988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.50/3.42 % (2981988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.50/3.42 % (2981988)CaDiCaL version: 2.1.3
% 22.50/3.42 % (2981988)Termination reason: Refutation
% 22.50/3.42 % (2981988)Time elapsed: 3.159 s
% 22.50/3.42 % (2981988)Peak memory usage: 25 MB
% 22.50/3.42 % (2981988)Instructions burned: 7193 (million)
% 22.50/3.42 % (2981979)Success in time 3.2 s
% 22.50/3.42 % Vampire exiting
%------------------------------------------------------------------------------