%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU968^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:34:29 AM UTC 2026
% Result : Theorem 116.53s 30.82s
% Output : Refutation 116.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU968^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n005.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 14:53:16 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.25 Running first-order model finding
% 0.09/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.11/1.03 % (1767766)Will run a generic schedule for satisfiability detection.
% 4.11/1.03 % (1767775)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1839483434:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.11/1.03 % (1767775)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.11/1.03 % (1767772)% WARNING: option uhcvi not known.
% 4.11/1.03 % (1767772)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2438578646:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.11/1.03 % (1767771)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=499510456_2999 on theBenchmark for (2999ds/0Mi)
% 4.11/1.03 % (1767773)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3842122024:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.11/1.03 % (1767774)dis+10_1_sil=32000:sp=arity:random_seed=67954749:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.11/1.03 % (1767772)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.11/1.03 % (1767776)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1801457498:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.11/1.03 % (1767772)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.11/1.03 % (1767777)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=797031557:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.11/1.03 % Exception at run slice level
% 4.11/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.11/1.03 % (1767785)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=693823146:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.11/1.03 % Exception at run slice level
% 4.11/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.11/1.03 % (1767775)Instruction limit reached!
% 4.11/1.03 % (1767775)------------------------------
% 4.11/1.03 % (1767775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/1.03 % (1767775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/1.03 % (1767775)CaDiCaL version: 2.1.3
% 4.11/1.03 % (1767775)Termination reason: Instruction limit
% 4.11/1.03 % (1767775)Termination phase: Saturation
% 4.11/1.03 % (1767775)Time elapsed: 0.033 s
% 4.11/1.03 % (1767775)Peak memory usage: 12 MB
% 4.11/1.03 % (1767775)Instructions burned: 118 (million)
% 4.11/1.03 % (1767788)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=3748452493:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.11/1.03 % (1767788)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.11/1.03 % (1767788)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.11/1.03 % (1767787)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3779440325:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.11/1.03 % (1767774)Instruction limit reached!
% 4.11/1.03 % (1767774)------------------------------
% 4.11/1.03 % (1767774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/1.03 % (1767774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/1.03 % (1767774)CaDiCaL version: 2.1.3
% 4.11/1.03 % (1767774)Termination reason: Instruction limit
% 4.11/1.03 % (1767774)Termination phase: Saturation
% 4.11/1.03 % (1767774)Time elapsed: 0.052 s
% 4.11/1.03 % (1767774)Peak memory usage: 12 MB
% 4.11/1.03 % (1767774)Instructions burned: 104 (million)
% 4.11/1.03 % (1767776)Instruction limit reached!
% 4.11/1.03 % (1767776)------------------------------
% 4.11/1.03 % (1767776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/1.03 % (1767776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/1.03 % (1767776)CaDiCaL version: 2.1.3
% 4.11/1.03 % (1767776)Termination reason: Instruction limit
% 4.11/1.03 % (1767776)Termination phase: Saturation
% 4.11/1.03 % (1767776)Time elapsed: 0.064 s
% 4.11/1.03 % (1767776)Peak memory usage: 12 MB
% 4.11/1.03 % (1767776)Instructions burned: 132 (million)
% 4.11/1.03 % (1767791)ott-21_1_sil=16000:fs=off:random_seed=1150698250:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.11/1.03 % (1767777)Instruction limit reached!
% 16.30/2.66 % (1767777)------------------------------
% 16.30/2.66 % (1767777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.30/2.66 % (1767777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.30/2.66 % (1767777)CaDiCaL version: 2.1.3
% 16.30/2.66 % (1767777)Termination reason: Instruction limit
% 16.30/2.66 % (1767777)Termination phase: Saturation
% 16.30/2.66 % (1767777)Time elapsed: 0.075 s
% 16.30/2.66 % (1767777)Peak memory usage: 12 MB
% 16.30/2.66 % (1767777)Instructions burned: 159 (million)
% 16.30/2.66 % (1767792)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3095624807:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 16.30/2.66 % (1767794)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2919360368:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 16.30/2.66 % Exception at run slice level
% 16.30/2.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.30/2.66 % (1767797)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3596016692:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 16.30/2.66 % (1767787)Instruction limit reached!
% 16.30/2.66 % (1767787)------------------------------
% 16.30/2.66 % (1767787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.30/2.66 % (1767787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.30/2.66 % (1767787)CaDiCaL version: 2.1.3
% 16.30/2.66 % (1767787)Termination reason: Instruction limit
% 16.30/2.66 % (1767787)Termination phase: Saturation
% 16.30/2.66 % (1767787)Time elapsed: 0.102 s
% 16.30/2.66 % (1767787)Peak memory usage: 12 MB
% 16.30/2.66 % (1767787)Instructions burned: 131 (million)
% 16.30/2.66 % (1767791)Instruction limit reached!
% 16.30/2.66 % (1767791)------------------------------
% 16.30/2.66 % (1767791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.30/2.66 % (1767791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.30/2.66 % (1767791)CaDiCaL version: 2.1.3
% 16.30/2.66 % (1767791)Termination reason: Instruction limit
% 16.30/2.66 % (1767791)Termination phase: Saturation
% 16.30/2.66 % (1767791)Time elapsed: 0.085 s
% 16.30/2.66 % (1767791)Peak memory usage: 12 MB
% 16.30/2.66 % (1767791)Instructions burned: 182 (million)
% 16.30/2.66 % (1767799)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2274583880:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 16.30/2.66 % Exception at run slice level
% 16.30/2.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.30/2.66 % (1767800)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=171106688: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.30/2.66 % (1767800)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.30/2.66 % (1767802)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3458997943:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 16.30/2.66 % (1767788)Instruction limit reached!
% 16.30/2.66 % (1767788)------------------------------
% 16.30/2.66 % (1767788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.30/2.66 % (1767788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.30/2.66 % (1767788)CaDiCaL version: 2.1.3
% 16.30/2.66 % (1767788)Termination reason: Instruction limit
% 16.30/2.66 % (1767788)Termination phase: Saturation
% 16.30/2.66 % (1767788)Time elapsed: 0.158 s
% 16.30/2.66 % (1767788)Peak memory usage: 13 MB
% 16.30/2.66 % (1767788)Instructions burned: 684 (million)
% 16.30/2.66 % (1767802)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.30/2.66 % (1767805)fmb+10_1_sil=64000:random_seed=3828403317:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 16.30/2.66 % (1767805)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.30/2.66 % Exception at run slice level
% 16.30/2.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.30/2.66 % (1767807)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2917163882:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 16.30/2.66 % Exception at run slice level
% 16.30/2.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 33.87/5.05 % (1767809)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2742920733:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 33.87/5.05 % Exception at run slice level
% 33.87/5.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 33.87/5.05 % (1767811)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1025943650:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 33.87/5.05 % (1767811)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 33.87/5.05 % (1767792)Instruction limit reached!
% 33.87/5.05 % (1767792)------------------------------
% 33.87/5.05 % (1767792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.87/5.05 % (1767792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.05 % (1767792)CaDiCaL version: 2.1.3
% 33.87/5.05 % (1767792)Termination reason: Instruction limit
% 33.87/5.05 % (1767792)Termination phase: Saturation
% 33.87/5.05 % (1767792)Time elapsed: 0.233 s
% 33.87/5.05 % (1767792)Peak memory usage: 13 MB
% 33.87/5.05 % (1767792)Instructions burned: 477 (million)
% 33.87/5.05 % (1767813)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=740755775:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 33.87/5.05 % (1767813)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 33.87/5.05 % (1767813)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 33.87/5.05 % (1767800)Instruction limit reached!
% 33.87/5.05 % (1767800)------------------------------
% 33.87/5.05 % (1767800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.87/5.05 % (1767800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.05 % (1767800)CaDiCaL version: 2.1.3
% 33.87/5.05 % (1767800)Termination reason: Instruction limit
% 33.87/5.05 % (1767800)Termination phase: Saturation
% 33.87/5.05 % (1767800)Time elapsed: 0.301 s
% 33.87/5.05 % (1767800)Peak memory usage: 14 MB
% 33.87/5.05 % (1767800)Instructions burned: 692 (million)
% 33.87/5.05 % (1767815)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1455783034:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 33.87/5.05 % Exception at run slice level
% 33.87/5.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 33.87/5.05 % (1767817)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=492003191:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 33.87/5.05 % Exception at run slice level
% 33.87/5.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 33.87/5.05 % (1767819)ott-2_1_sil=16000:newcnf=on:random_seed=2798072092:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 33.87/5.05 % (1767819)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 33.87/5.05 % (1767797)Instruction limit reached!
% 33.87/5.05 % (1767797)------------------------------
% 33.87/5.05 % (1767797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.87/5.05 % (1767797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.05 % (1767797)CaDiCaL version: 2.1.3
% 33.87/5.05 % (1767797)Termination reason: Instruction limit
% 33.87/5.05 % (1767797)Termination phase: Saturation
% 33.87/5.05 % (1767797)Time elapsed: 0.543 s
% 33.87/5.05 % (1767797)Peak memory usage: 16 MB
% 33.87/5.05 % (1767797)Instructions burned: 1181 (million)
% 33.87/5.05 % (1767821)ott+10_1_sil=32000:tgt=ground:random_seed=143936136:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 33.87/5.05 % (1767802)Instruction limit reached!
% 33.87/5.05 % (1767802)------------------------------
% 33.87/5.05 % (1767802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.87/5.05 % (1767802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.05 % (1767802)CaDiCaL version: 2.1.3
% 33.87/5.05 % (1767802)Termination reason: Instruction limit
% 33.87/5.05 % (1767802)Termination phase: Saturation
% 33.87/5.05 % (1767802)Time elapsed: 0.509 s
% 33.87/5.05 % (1767802)Peak memory usage: 15 MB
% 33.87/5.05 % (1767802)Instructions burned: 881 (million)
% 33.87/5.05 % (1767823)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2484930283:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 33.87/5.05 % Exception at run slice level
% 33.87/5.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 91.74/13.22 % (1767825)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3963804030:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 91.74/13.22 % (1767825)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 91.74/13.22 % (1767819)Instruction limit reached!
% 91.74/13.22 % (1767819)------------------------------
% 91.74/13.22 % (1767819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.74/13.22 % (1767819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.74/13.22 % (1767819)CaDiCaL version: 2.1.3
% 91.74/13.22 % (1767819)Termination reason: Instruction limit
% 91.74/13.22 % (1767819)Termination phase: Saturation
% 91.74/13.22 % (1767819)Time elapsed: 0.404 s
% 91.74/13.22 % (1767819)Peak memory usage: 16 MB
% 91.74/13.22 % (1767819)Instructions burned: 870 (million)
% 91.74/13.22 % (1767827)dis+21_1_sil=32000:sas=cadical:random_seed=2322319855:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 91.74/13.22 % (1767813)Instruction limit reached!
% 91.74/13.22 % (1767813)------------------------------
% 91.74/13.22 % (1767813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.74/13.22 % (1767813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.74/13.22 % (1767813)CaDiCaL version: 2.1.3
% 91.74/13.22 % (1767813)Termination reason: Instruction limit
% 91.74/13.22 % (1767813)Termination phase: Saturation
% 91.74/13.22 % (1767813)Time elapsed: 0.692 s
% 91.74/13.22 % (1767813)Peak memory usage: 15 MB
% 91.74/13.22 % (1767813)Instructions burned: 1472 (million)
% 91.74/13.22 % (1767829)ott+11_1_sil=16000:gs=on:random_seed=1263031224:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 91.74/13.22 % (1767829)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 91.74/13.22 % (1767811)Instruction limit reached!
% 91.74/13.22 % (1767811)------------------------------
% 91.74/13.22 % (1767811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.74/13.22 % (1767811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.74/13.22 % (1767811)CaDiCaL version: 2.1.3
% 91.74/13.22 % (1767811)Termination reason: Instruction limit
% 91.74/13.22 % (1767811)Termination phase: Saturation
% 91.74/13.22 % (1767811)Time elapsed: 1.143 s
% 91.74/13.22 % (1767811)Peak memory usage: 19 MB
% 91.74/13.22 % (1767811)Instructions burned: 5132 (million)
% 91.74/13.22 % (1767831)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4155242299:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi)
% 91.74/13.22 % Exception at run slice level
% 91.74/13.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 91.74/13.22 % (1767833)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2540432792:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi)
% 91.74/13.22 % (1767829)Instruction limit reached!
% 91.74/13.22 % (1767829)------------------------------
% 91.74/13.22 % (1767829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.74/13.22 % (1767829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.74/13.22 % (1767829)CaDiCaL version: 2.1.3
% 91.74/13.22 % (1767829)Termination reason: Instruction limit
% 91.74/13.22 % (1767829)Termination phase: Saturation
% 91.74/13.22 % (1767829)Time elapsed: 1.004 s
% 91.74/13.22 % (1767829)Peak memory usage: 19 MB
% 91.74/13.22 % (1767829)Instructions burned: 2253 (million)
% 91.74/13.22 % (1767836)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1517192201:i=29340_2979 on theBenchmark for (2979ds/29340Mi)
% 91.74/13.22 % (1767825)Instruction limit reached!
% 91.74/13.22 % (1767825)------------------------------
% 91.74/13.22 % (1767825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.74/13.22 % (1767825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.74/13.22 % (1767825)CaDiCaL version: 2.1.3
% 91.74/13.22 % (1767825)Termination reason: Instruction limit
% 91.74/13.22 % (1767825)Termination phase: Saturation
% 91.74/13.22 % (1767825)Time elapsed: 1.576 s
% 91.74/13.22 % (1767825)Peak memory usage: 18 MB
% 91.74/13.22 % (1767825)Instructions burned: 3513 (million)
% 91.74/13.22 % (1767838)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1166688867:i=5211_2976 on theBenchmark for (2976ds/5211Mi)
% 123.79/17.75 % (1767833)Instruction limit reached!
% 123.79/17.75 % (1767833)------------------------------
% 123.79/17.75 % (1767833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 123.79/17.75 % (1767833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.79/17.75 % (1767833)CaDiCaL version: 2.1.3
% 123.79/17.75 % (1767833)Termination reason: Instruction limit
% 123.79/17.75 % (1767833)Termination phase: Saturation
% 123.79/17.75 % (1767833)Time elapsed: 1.198 s
% 123.79/17.75 % (1767833)Peak memory usage: 22 MB
% 123.79/17.75 % (1767833)Instructions burned: 4593 (million)
% 123.79/17.75 % (1767840)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=40483966:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi)
% 123.79/17.75 % Exception at run slice level
% 123.79/17.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 123.79/17.75 % (1767842)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3968670446:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 123.79/17.75 % Exception at run slice level
% 123.79/17.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 123.79/17.75 % (1767844)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1080867110:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 123.79/17.75 % Exception at run slice level
% 123.79/17.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 123.79/17.75 % (1767827)Instruction limit reached!
% 123.79/17.75 % (1767827)------------------------------
% 123.79/17.75 % (1767827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 123.79/17.75 % (1767827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.79/17.75 % (1767827)CaDiCaL version: 2.1.3
% 123.79/17.75 % (1767827)Termination reason: Instruction limit
% 123.79/17.75 % (1767827)Termination phase: Saturation
% 123.79/17.75 % (1767827)Time elapsed: 1.692 s
% 123.79/17.75 % (1767827)Peak memory usage: 21 MB
% 123.79/17.75 % (1767827)Instructions burned: 3775 (million)
% 123.79/17.75 % (1767846)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1253843357:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 123.79/17.75 % (1767848)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2447577926:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi)
% 123.79/17.75 % (1767821)Instruction limit reached!
% 123.79/17.75 % (1767821)------------------------------
% 123.79/17.75 % (1767821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 123.79/17.75 % (1767821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.79/17.75 % (1767821)CaDiCaL version: 2.1.3
% 123.79/17.75 % (1767821)Termination reason: Instruction limit
% 123.79/17.75 % (1767821)Termination phase: Saturation
% 123.79/17.75 % (1767821)Time elapsed: 2.196 s
% 123.79/17.75 % (1767821)Peak memory usage: 25 MB
% 123.79/17.75 % (1767821)Instructions burned: 5116 (million)
% 123.79/17.75 % (1767850)dis+10_16:1_sil=16000:random_seed=4054376412:i=9155:fsr=off_2970 on theBenchmark for (2970ds/9155Mi)
% 123.79/17.75 % (1767848)Instruction limit reached!
% 123.79/17.75 % (1767848)------------------------------
% 123.79/17.75 % (1767848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 123.79/17.75 % (1767848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.79/17.75 % (1767848)CaDiCaL version: 2.1.3
% 123.79/17.75 % (1767848)Termination reason: Instruction limit
% 123.79/17.75 % (1767848)Termination phase: Saturation
% 123.79/17.75 % (1767848)Time elapsed: 1.917 s
% 123.79/17.75 % (1767848)Peak memory usage: 33 MB
% 123.79/17.75 % (1767848)Instructions burned: 8175 (million)
% 123.79/17.75 % (1767852)ott-3_8_sil=64000:random_seed=972326961:i=20139:bs=on_2953 on theBenchmark for (2953ds/20139Mi)
% 123.79/17.75 % (1767838)Instruction limit reached!
% 123.79/17.75 % (1767838)------------------------------
% 123.79/17.75 % (1767838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 123.79/17.75 % (1767838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.79/17.75 % (1767838)CaDiCaL version: 2.1.3
% 123.79/17.75 % (1767838)Termination reason: Instruction limit
% 123.79/17.75 % (1767838)Termination phase: Saturation
% 123.79/17.75 % (1767838)Time elapsed: 2.366 s
% 123.79/17.75 % (1767838)Peak memory usage: 24 MB
% 123.79/17.75 % (1767838)Instructions burned: 5211 (million)
% 123.79/17.75 % (1767854)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2829509930:fmbsr=2:i=32576_2952 on theBenchmark for (2952ds/32576Mi)
% 131.87/18.98 % Exception at run slice level
% 131.87/18.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.87/18.98 % (1767856)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1438366584:i=11404_2952 on theBenchmark for (2952ds/11404Mi)
% 131.87/18.98 % (1767850)Instruction limit reached!
% 131.87/18.98 % (1767850)------------------------------
% 131.87/18.98 % (1767850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.87/18.98 % (1767850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/18.98 % (1767850)CaDiCaL version: 2.1.3
% 131.87/18.98 % (1767850)Termination reason: Instruction limit
% 131.87/18.98 % (1767850)Termination phase: Saturation
% 131.87/18.98 % (1767850)Time elapsed: 3.952 s
% 131.87/18.98 % (1767850)Peak memory usage: 26 MB
% 131.87/18.98 % (1767850)Instructions burned: 9156 (million)
% 131.87/18.98 % (1767858)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1228184468:i=14134_2931 on theBenchmark for (2931ds/14134Mi)
% 131.87/18.98 % (1767858)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 131.87/18.98 % (1767852)Instruction limit reached!
% 131.87/18.98 % (1767852)------------------------------
% 131.87/18.98 % (1767852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.87/18.98 % (1767852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/18.98 % (1767852)CaDiCaL version: 2.1.3
% 131.87/18.98 % (1767852)Termination reason: Instruction limit
% 131.87/18.98 % (1767852)Termination phase: Saturation
% 131.87/18.98 % (1767852)Time elapsed: 4.455 s
% 131.87/18.98 % (1767852)Peak memory usage: 32 MB
% 131.87/18.98 % (1767852)Instructions burned: 20142 (million)
% 131.87/18.98 % (1767860)dis+33_16_sil=32000:sac=on:random_seed=125691028:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi)
% 131.87/18.98 % (1767856)Instruction limit reached!
% 131.87/18.98 % (1767856)------------------------------
% 131.87/18.98 % (1767856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.87/18.98 % (1767856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/18.98 % (1767856)CaDiCaL version: 2.1.3
% 131.87/18.98 % (1767856)Termination reason: Instruction limit
% 131.87/18.98 % (1767856)Termination phase: Saturation
% 131.87/18.98 % (1767856)Time elapsed: 5.003 s
% 131.87/18.98 % (1767856)Peak memory usage: 37 MB
% 131.87/18.98 % (1767856)Instructions burned: 11405 (million)
% 131.87/18.98 % (1767862)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=640411209:avsq=on:i=17627:add=on:amm=off_2901 on theBenchmark for (2901ds/17627Mi)
% 131.87/18.98 % (1767846)Instruction limit reached!
% 131.87/18.98 % (1767846)------------------------------
% 131.87/18.98 % (1767846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.87/18.98 % (1767846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/18.98 % (1767846)CaDiCaL version: 2.1.3
% 131.87/18.98 % (1767846)Termination reason: Instruction limit
% 131.87/18.98 % (1767846)Termination phase: Saturation
% 131.87/18.98 % (1767846)Time elapsed: 9.529 s
% 131.87/18.98 % (1767846)Peak memory usage: 29 MB
% 131.87/18.98 % (1767846)Instructions burned: 22566 (million)
% 131.87/18.98 % (1767864)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2935816909:s2a=on:i=53295_2877 on theBenchmark for (2877ds/53295Mi)
% 131.87/18.98 % (1767860)Instruction limit reached!
% 131.87/18.98 % (1767860)------------------------------
% 131.87/18.98 % (1767860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.87/18.98 % (1767860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/18.98 % (1767860)CaDiCaL version: 2.1.3
% 131.87/18.98 % (1767860)Termination reason: Instruction limit
% 131.87/18.98 % (1767860)Termination phase: Saturation
% 131.87/18.98 % (1767860)Time elapsed: 3.698 s
% 131.87/18.98 % (1767860)Peak memory usage: 25 MB
% 131.87/18.98 % (1767860)Instructions burned: 15856 (million)
% 131.87/18.98 % (1767866)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3624468371:i=26857:ins=20_2871 on theBenchmark for (2871ds/26857Mi)
% 131.87/18.98 % Exception at run slice level
% 131.87/18.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.87/18.98 % (1767868)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2242779759:i=28120:bs=on:fsr=off_2871 on theBenchmark for (2871ds/28120Mi)
% 131.87/18.98 % (1767858)Instruction limit reached!
% 131.87/18.98 % (1767858)------------------------------
% 131.87/18.98 % (1767858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.64/20.15 % (1767858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.64/20.15 % (1767858)CaDiCaL version: 2.1.3
% 140.64/20.15 % (1767858)Termination reason: Instruction limit
% 140.64/20.15 % (1767858)Termination phase: Saturation
% 140.64/20.15 % (1767858)Time elapsed: 6.059 s
% 140.64/20.15 % (1767858)Peak memory usage: 38 MB
% 140.64/20.15 % (1767858)Instructions burned: 14135 (million)
% 140.64/20.15 % (1767870)fmb+10_1_sil=256000:fmbss=7:random_seed=1969709198:fmbsr=1.6:i=182295_2870 on theBenchmark for (2870ds/182295Mi)
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767872)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4071216126:i=44625:gsp=on_2870 on theBenchmark for (2870ds/44625Mi)
% 140.64/20.15 % (1767872)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 140.64/20.15 % (1767872)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767874)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=492510025:i=160505_2869 on theBenchmark for (2869ds/160505Mi)
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767876)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2577416144:fmbsr=1.3:i=225729_2869 on theBenchmark for (2869ds/225729Mi)
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767878)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=760827706:fmbsr=2:i=185024:ins=7_2869 on theBenchmark for (2869ds/185024Mi)
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767880)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=460335109:rtra=on_2869 on theBenchmark for (2869ds/0Mi)
% 140.64/20.15 % Exception at run slice level
% 140.64/20.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.64/20.15 % (1767882)% WARNING: option uhcvi not known.
% 140.64/20.15 % (1767882)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3346469409:i=271062:add=off:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/271062Mi)
% 140.64/20.15 % (1767882)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 140.64/20.15 % (1767882)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 140.64/20.15 % (1767836)Instruction limit reached!
% 140.64/20.15 % (1767836)------------------------------
% 140.64/20.15 % (1767836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.64/20.15 % (1767836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.64/20.15 % (1767836)CaDiCaL version: 2.1.3
% 140.64/20.15 % (1767836)Termination reason: Instruction limit
% 140.64/20.15 % (1767836)Termination phase: Saturation
% 140.64/20.15 % (1767836)Time elapsed: 12.290 s
% 140.64/20.15 % (1767836)Peak memory usage: 35 MB
% 140.64/20.15 % (1767836)Instructions burned: 29341 (million)
% 140.64/20.15 % (1767884)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4184580966:i=176048:add=on:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/176048Mi)
% 140.64/20.15 % (1767862)Instruction limit reached!
% 140.64/20.15 % (1767862)------------------------------
% 140.64/20.15 % (1767862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.64/20.15 % (1767862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.64/20.15 % (1767862)CaDiCaL version: 2.1.3
% 140.64/20.15 % (1767862)Termination reason: Instruction limit
% 140.64/20.15 % (1767862)Termination phase: Saturation
% 140.64/20.15 % (1767862)Time elapsed: 7.530 s
% 140.64/20.15 % (1767862)Peak memory usage: 36 MB
% 140.64/20.15 % (1767862)Instructions burned: 17628 (million)
% 140.64/20.15 % (1767886)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2915201666:i=206:fgj=on:rtra=on_2826 on theBenchmark for (2826ds/206Mi)
% 140.64/20.15 % (1767886)Instruction limit reached!
% 140.64/20.15 % (1767886)------------------------------
% 152.66/21.86 % (1767886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.66/21.86 % (1767886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.66/21.86 % (1767886)CaDiCaL version: 2.1.3
% 152.66/21.86 % (1767886)Termination reason: Instruction limit
% 152.66/21.86 % (1767886)Termination phase: Saturation
% 152.66/21.86 % (1767886)Time elapsed: 0.101 s
% 152.66/21.86 % (1767886)Peak memory usage: 12 MB
% 152.66/21.86 % (1767886)Instructions burned: 208 (million)
% 152.66/21.86 % (1767888)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3911376703:i=232:rtra=on_2825 on theBenchmark for (2825ds/232Mi)
% 152.66/21.86 % (1767888)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 152.66/21.86 % (1767888)Instruction limit reached!
% 152.66/21.86 % (1767888)------------------------------
% 152.66/21.86 % (1767888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.66/21.86 % (1767888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.66/21.86 % (1767888)CaDiCaL version: 2.1.3
% 152.66/21.86 % (1767888)Termination reason: Instruction limit
% 152.66/21.86 % (1767888)Termination phase: Saturation
% 152.66/21.86 % (1767888)Time elapsed: 0.111 s
% 152.66/21.86 % (1767888)Peak memory usage: 13 MB
% 152.66/21.86 % (1767888)Instructions burned: 233 (million)
% 152.66/21.86 % (1767890)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3310520359:i=262:rtra=on_2823 on theBenchmark for (2823ds/262Mi)
% 152.66/21.86 % (1767890)Instruction limit reached!
% 152.66/21.86 % (1767890)------------------------------
% 152.66/21.86 % (1767890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.66/21.86 % (1767890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.66/21.86 % (1767890)CaDiCaL version: 2.1.3
% 152.66/21.86 % (1767890)Termination reason: Instruction limit
% 152.66/21.86 % (1767890)Termination phase: Saturation
% 152.66/21.86 % (1767890)Time elapsed: 0.123 s
% 152.66/21.86 % (1767890)Peak memory usage: 13 MB
% 152.66/21.86 % (1767890)Instructions burned: 262 (million)
% 152.66/21.86 % (1767892)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2526451126:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2822 on theBenchmark for (2822ds/318Mi)
% 152.66/21.86 % (1767892)Instruction limit reached!
% 152.66/21.86 % (1767892)------------------------------
% 152.66/21.86 % (1767892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.66/21.86 % (1767892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.66/21.86 % (1767892)CaDiCaL version: 2.1.3
% 152.66/21.86 % (1767892)Termination reason: Instruction limit
% 152.66/21.86 % (1767892)Termination phase: Saturation
% 152.66/21.86 % (1767892)Time elapsed: 0.145 s
% 152.66/21.86 % (1767892)Peak memory usage: 13 MB
% 152.66/21.86 % (1767892)Instructions burned: 319 (million)
% 152.66/21.86 % (1767894)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3729904222:i=1428:nm=2:rtra=on_2820 on theBenchmark for (2820ds/1428Mi)
% 152.66/21.86 % Exception at run slice level
% 152.66/21.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.66/21.86 % (1767896)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3492475783:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi)
% 152.66/21.86 % (1767896)Instruction limit reached!
% 152.66/21.86 % (1767896)------------------------------
% 152.66/21.86 % (1767896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.66/21.86 % (1767896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.66/21.86 % (1767896)CaDiCaL version: 2.1.3
% 152.66/21.86 % (1767896)Termination reason: Instruction limit
% 152.66/21.86 % (1767896)Termination phase: Saturation
% 152.66/21.86 % (1767896)Time elapsed: 0.137 s
% 152.66/21.86 % (1767896)Peak memory usage: 13 MB
% 152.66/21.86 % (1767896)Instructions burned: 263 (million)
% 152.66/21.86 % (1767898)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2511412281:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/1368Mi)
% 152.66/21.86 % (1767898)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 152.66/21.86 % (1767898)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 152.66/21.86 % (1767898)Instruction limit reached!
% 152.66/21.86 % (1767898)------------------------------
% 152.66/21.86 % (1767898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.11/27.33 % (1767898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.11/27.33 % (1767898)CaDiCaL version: 2.1.3
% 192.11/27.33 % (1767898)Termination reason: Instruction limit
% 192.11/27.33 % (1767898)Termination phase: Saturation
% 192.11/27.33 % (1767898)Time elapsed: 0.591 s
% 192.11/27.33 % (1767898)Peak memory usage: 13 MB
% 192.11/27.33 % (1767898)Instructions burned: 1368 (million)
% 192.11/27.33 % (1767900)ott-21_1_sil=16000:si=on:fs=off:random_seed=3526136957:i=360:av=off:fsr=off:rtra=on_2812 on theBenchmark for (2812ds/360Mi)
% 192.11/27.33 % (1767900)Instruction limit reached!
% 192.11/27.33 % (1767900)------------------------------
% 192.11/27.33 % (1767900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.11/27.33 % (1767900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.11/27.33 % (1767900)CaDiCaL version: 2.1.3
% 192.11/27.33 % (1767900)Termination reason: Instruction limit
% 192.11/27.33 % (1767900)Termination phase: Saturation
% 192.11/27.33 % (1767900)Time elapsed: 0.165 s
% 192.11/27.33 % (1767900)Peak memory usage: 12 MB
% 192.11/27.33 % (1767900)Instructions burned: 361 (million)
% 192.11/27.33 % (1767902)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3004856184:i=954:bd=all:rtra=on_2810 on theBenchmark for (2810ds/954Mi)
% 192.11/27.33 % (1767868)Instruction limit reached!
% 192.11/27.33 % (1767868)------------------------------
% 192.11/27.33 % (1767868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.11/27.33 % (1767868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.11/27.33 % (1767868)CaDiCaL version: 2.1.3
% 192.11/27.33 % (1767868)Termination reason: Instruction limit
% 192.11/27.33 % (1767868)Termination phase: Saturation
% 192.11/27.33 % (1767868)Time elapsed: 6.355 s
% 192.11/27.33 % (1767868)Peak memory usage: 54 MB
% 192.11/27.33 % (1767868)Instructions burned: 28125 (million)
% 192.11/27.33 % (1767904)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1289343654:fmbsr=1.3:i=1730:ins=25:rtra=on_2808 on theBenchmark for (2808ds/1730Mi)
% 192.11/27.33 % Exception at run slice level
% 192.11/27.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 192.11/27.33 % (1767906)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3217163256:i=2358:rtra=on_2807 on theBenchmark for (2807ds/2358Mi)
% 192.11/27.33 % (1767902)Instruction limit reached!
% 192.11/27.33 % (1767902)------------------------------
% 192.11/27.33 % (1767902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.11/27.33 % (1767902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.11/27.33 % (1767902)CaDiCaL version: 2.1.3
% 192.11/27.33 % (1767902)Termination reason: Instruction limit
% 192.11/27.33 % (1767902)Termination phase: Saturation
% 192.11/27.33 % (1767902)Time elapsed: 0.456 s
% 192.11/27.33 % (1767902)Peak memory usage: 14 MB
% 192.11/27.33 % (1767902)Instructions burned: 955 (million)
% 192.11/27.33 % (1767908)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1258010772:i=1778:ins=1:rtra=on_2806 on theBenchmark for (2806ds/1778Mi)
% 192.11/27.33 % Exception at run slice level
% 192.11/27.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 192.11/27.33 % (1767910)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3708009904:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/1384Mi)
% 192.11/27.33 % (1767910)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 192.11/27.33 % (1767906)Instruction limit reached!
% 192.11/27.33 % (1767906)------------------------------
% 192.11/27.33 % (1767906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.11/27.33 % (1767906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.11/27.33 % (1767906)CaDiCaL version: 2.1.3
% 192.11/27.33 % (1767906)Termination reason: Instruction limit
% 192.11/27.33 % (1767906)Termination phase: Saturation
% 192.11/27.33 % (1767906)Time elapsed: 0.667 s
% 192.11/27.33 % (1767906)Peak memory usage: 20 MB
% 192.11/27.33 % (1767906)Instructions burned: 2362 (million)
% 192.11/27.33 % (1767912)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1056742395:i=1758:kws=inv_precedence:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/1758Mi)
% 192.11/27.33 % (1767912)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 116.53/30.82 % (1767910)Instruction limit reached!
% 116.53/30.82 % (1767910)------------------------------
% 116.53/30.82 % (1767910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767910)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767910)Termination reason: Instruction limit
% 116.53/30.82 % (1767910)Termination phase: Saturation
% 116.53/30.82 % (1767910)Time elapsed: 0.595 s
% 116.53/30.82 % (1767910)Peak memory usage: 15 MB
% 116.53/30.82 % (1767910)Instructions burned: 1384 (million)
% 116.53/30.82 % (1767914)fmb+10_1_sil=64000:si=on:random_seed=2445997022:i=44122:nm=2:rtra=on:gsp=on_2799 on theBenchmark for (2799ds/44122Mi)
% 116.53/30.82 % (1767914)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767916)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=685256391:i=19030:nm=5:rtra=on_2799 on theBenchmark for (2799ds/19030Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767918)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3087152245:fmbsr=1.7:i=1840:rtra=on_2799 on theBenchmark for (2799ds/1840Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767920)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2317784090:i=10262:rtra=on_2799 on theBenchmark for (2799ds/10262Mi)
% 116.53/30.82 % (1767920)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 116.53/30.82 % (1767912)Instruction limit reached!
% 116.53/30.82 % (1767912)------------------------------
% 116.53/30.82 % (1767912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767912)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767912)Termination reason: Instruction limit
% 116.53/30.82 % (1767912)Termination phase: Saturation
% 116.53/30.82 % (1767912)Time elapsed: 0.441 s
% 116.53/30.82 % (1767912)Peak memory usage: 17 MB
% 116.53/30.82 % (1767912)Instructions burned: 1760 (million)
% 116.53/30.82 % (1767922)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2099345458:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2796 on theBenchmark for (2796ds/2944Mi)
% 116.53/30.82 % (1767922)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 116.53/30.82 % (1767922)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 116.53/30.82 % (1767922)Instruction limit reached!
% 116.53/30.82 % (1767922)------------------------------
% 116.53/30.82 % (1767922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767922)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767922)Termination reason: Instruction limit
% 116.53/30.82 % (1767922)Termination phase: Saturation
% 116.53/30.82 % (1767922)Time elapsed: 0.801 s
% 116.53/30.82 % (1767922)Peak memory usage: 20 MB
% 116.53/30.82 % (1767922)Instructions burned: 2946 (million)
% 116.53/30.82 % (1767924)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1290628009:i=12648:rtra=on_2788 on theBenchmark for (2788ds/12648Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767926)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=344206735:fmbsr=2.30978:i=4348:rtra=on_2788 on theBenchmark for (2788ds/4348Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767928)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2176542355:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2788 on theBenchmark for (2788ds/1738Mi)
% 116.53/30.82 % (1767928)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 116.53/30.82 % (1767928)Instruction limit reached!
% 116.53/30.82 % (1767928)------------------------------
% 116.53/30.82 % (1767928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767928)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767928)Termination reason: Instruction limit
% 116.53/30.82 % (1767928)Termination phase: Saturation
% 116.53/30.82 % (1767928)Time elapsed: 0.420 s
% 116.53/30.82 % (1767928)Peak memory usage: 20 MB
% 116.53/30.82 % (1767928)Instructions burned: 1742 (million)
% 116.53/30.82 % (1767930)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1373821126:i=10228:av=off:rtra=on_2783 on theBenchmark for (2783ds/10228Mi)
% 116.53/30.82 % (1767930)Instruction limit reached!
% 116.53/30.82 % (1767930)------------------------------
% 116.53/30.82 % (1767930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767930)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767930)Termination reason: Instruction limit
% 116.53/30.82 % (1767930)Termination phase: Saturation
% 116.53/30.82 % (1767930)Time elapsed: 2.623 s
% 116.53/30.82 % (1767930)Peak memory usage: 33 MB
% 116.53/30.82 % (1767930)Instructions burned: 10232 (million)
% 116.53/30.82 % (1767932)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3419330415:i=108564:rtra=on_2757 on theBenchmark for (2757ds/108564Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767934)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3800679004:i=7024:aac=none:rtra=on_2757 on theBenchmark for (2757ds/7024Mi)
% 116.53/30.82 % (1767934)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 116.53/30.82 % (1767920)Instruction limit reached!
% 116.53/30.82 % (1767920)------------------------------
% 116.53/30.82 % (1767920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767920)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767920)Termination reason: Instruction limit
% 116.53/30.82 % (1767920)Termination phase: Saturation
% 116.53/30.82 % (1767920)Time elapsed: 4.412 s
% 116.53/30.82 % (1767920)Peak memory usage: 25 MB
% 116.53/30.82 % (1767920)Instructions burned: 10263 (million)
% 116.53/30.82 % (1767936)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3490963372:i=7546:rtra=on:amm=off_2754 on theBenchmark for (2754ds/7546Mi)
% 116.53/30.82 % (1767934)Instruction limit reached!
% 116.53/30.82 % (1767934)------------------------------
% 116.53/30.82 % (1767934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767934)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767934)Termination reason: Instruction limit
% 116.53/30.82 % (1767934)Termination phase: Saturation
% 116.53/30.82 % (1767934)Time elapsed: 1.642 s
% 116.53/30.82 % (1767934)Peak memory usage: 22 MB
% 116.53/30.82 % (1767934)Instructions burned: 7027 (million)
% 116.53/30.82 % (1767938)ott+11_1_sil=16000:si=on:gs=on:random_seed=1211845336:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2740 on theBenchmark for (2740ds/4502Mi)
% 116.53/30.82 % (1767938)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 116.53/30.82 % (1767938)Instruction limit reached!
% 116.53/30.82 % (1767938)------------------------------
% 116.53/30.82 % (1767938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767938)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767938)Termination reason: Instruction limit
% 116.53/30.82 % (1767938)Termination phase: Saturation
% 116.53/30.82 % (1767938)Time elapsed: 1.131 s
% 116.53/30.82 % (1767938)Peak memory usage: 24 MB
% 116.53/30.82 % (1767938)Instructions burned: 4504 (million)
% 116.53/30.82 % (1767940)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=564528141:fmbsr=1.6:i=135068:rtra=on_2729 on theBenchmark for (2729ds/135068Mi)
% 116.53/30.82 % Exception at run slice level
% 116.53/30.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.53/30.82 % (1767942)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2477434106:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2729 on theBenchmark for (2729ds/9182Mi)
% 116.53/30.82 % (1767936)Instruction limit reached!
% 116.53/30.82 % (1767936)------------------------------
% 116.53/30.82 % (1767936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767936)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767936)Termination reason: Instruction limit
% 116.53/30.82 % (1767936)Termination phase: Saturation
% 116.53/30.82 % (1767936)Time elapsed: 3.417 s
% 116.53/30.82 % (1767936)Peak memory usage: 29 MB
% 116.53/30.82 % (1767936)Instructions burned: 7547 (million)
% 116.53/30.82 % (1767944)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=3013310052:i=58680:rtra=on_2720 on theBenchmark for (2720ds/58680Mi)
% 116.53/30.82 % (1767942)Instruction limit reached!
% 116.53/30.82 % (1767942)------------------------------
% 116.53/30.82 % (1767942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767942)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767942)Termination reason: Instruction limit
% 116.53/30.82 % (1767942)Termination phase: Saturation
% 116.53/30.82 % (1767942)Time elapsed: 2.441 s
% 116.53/30.82 % (1767942)Peak memory usage: 21 MB
% 116.53/30.82 % (1767942)Instructions burned: 9183 (million)
% 116.53/30.82 % (1767946)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=1544100839:i=10422:rtra=on_2704 on theBenchmark for (2704ds/10422Mi)
% 116.53/30.82 % (1767882) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1767766-1767882"...
% 116.53/30.82 % (1767882)...printing done.
% 116.53/30.82 % (1767882)Refutation found. Thanks to Tanya!
% 116.53/30.82 % SZS status Theorem for theBenchmark
% 116.53/30.82 % SZS output start Proof for theBenchmark
% 116.53/30.82 thf(type_def_5, type, a: $tType).
% 116.53/30.82 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 116.53/30.82 thf(func_def_1, type, db0: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_2, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 116.53/30.82 thf(func_def_5, type, sK0: (a > a)).
% 116.53/30.82 thf(func_def_6, type, sK1: (a > a)).
% 116.53/30.82 thf(func_def_7, type, sK2: (a > a)).
% 116.53/30.82 thf(func_def_8, type, sK3: (((a > a) > $o) > a > a)).
% 116.53/30.82 thf(func_def_9, type, sK4: (((a > a) > $o) > a > a)).
% 116.53/30.82 thf(func_def_10, type, sK5: ((a > a) > $o)).
% 116.53/30.82 thf(func_def_11, type, vNOT: ($o > $o)).
% 116.53/30.82 thf(func_def_12, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 116.53/30.82 thf(func_def_13, type, db1: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_15, type, sK7: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_16, type, db2: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_17, type, sK8: a).
% 116.53/30.82 thf(func_def_18, type, sK9: a).
% 116.53/30.82 thf(func_def_19, type, sK10: a).
% 116.53/30.82 thf(func_def_20, type, sK11: a).
% 116.53/30.82 thf(func_def_21, type, sK12: a).
% 116.53/30.82 thf(func_def_22, type, sK13: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_23, type, sK14: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_24, type, sK15: a).
% 116.53/30.82 thf(func_def_25, type, sK16: a).
% 116.53/30.82 thf(func_def_26, type, sK17: a).
% 116.53/30.82 thf(func_def_27, type, sK18: ((a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_28, type, sK19: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_29, type, sK20: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_30, type, sK21: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_31, type, sK22: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_32, type, sK23: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_33, type, sK24: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_34, type, sK25: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_35, type, sK26: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_36, type, sK27: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_37, type, sK28: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_38, type, sK29: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_39, type, sK30: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_40, type, sK31: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_41, type, sK32: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_42, type, sK33: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_43, type, db3: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_44, type, db4: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_45, type, sK34: ((a > (a > a) > $o) > a > a)).
% 116.53/30.82 thf(func_def_46, type, sK35: (a > a)).
% 116.53/30.82 thf(func_def_47, type, sK36: (a > a)).
% 116.53/30.82 thf(func_def_48, type, sK37: (a > a)).
% 116.53/30.82 thf(func_def_49, type, sK38: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_50, type, sK39: a).
% 116.53/30.82 thf(func_def_51, type, sK40: a).
% 116.53/30.82 thf(func_def_52, type, sK41: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_53, type, sK42: a).
% 116.53/30.82 thf(func_def_54, type, sK43: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_55, type, sK44: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_56, type, sK45: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_57, type, sK46: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_58, type, sK47: ((a > a) > a)).
% 116.53/30.82 thf(func_def_59, type, sK48: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_60, type, sK49: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_61, type, db5: !>[X0: $tType]:(X0)).
% 116.53/30.82 thf(func_def_62, type, sK50: ((a > a) > a)).
% 116.53/30.82 thf(func_def_63, type, sK51: ((a > a) > a)).
% 116.53/30.82 thf(func_def_64, type, sK52: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_65, type, sK53: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_66, type, sK54: ((a > a) > a)).
% 116.53/30.82 thf(func_def_67, type, sK55: a).
% 116.53/30.82 thf(func_def_68, type, sK56: a).
% 116.53/30.82 thf(func_def_69, type, sK57: ((a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_70, type, sK58: ((a > a) > a)).
% 116.53/30.82 thf(func_def_71, type, sK59: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_72, type, sK60: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_73, type, sK61: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_74, type, sK62: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_75, type, sK63: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_76, type, sK64: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_77, type, sK65: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_78, type, sK66: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_79, type, sK67: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_80, type, sK68: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_81, type, sK69: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_82, type, sK70: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_83, type, sK71: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_84, type, sK72: ((a > a) > a)).
% 116.53/30.82 thf(func_def_85, type, sK73: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_86, type, sK74: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_87, type, sK75: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_88, type, sK76: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_89, type, sK77: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_90, type, sK78: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_91, type, sK79: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_92, type, sK80: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_93, type, sK81: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_94, type, sK82: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_95, type, sK83: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_96, type, sK84: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_97, type, sK85: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_98, type, sK86: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_99, type, sK87: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_100, type, sK88: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_101, type, sK89: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_102, type, sK90: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_103, type, sK91: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_104, type, sK92: ((a > a) > a)).
% 116.53/30.82 thf(func_def_105, type, sK93: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_106, type, sK94: ((a > a) > a)).
% 116.53/30.82 thf(func_def_107, type, sK95: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_108, type, sK96: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_109, type, sK97: ((a > a) > a)).
% 116.53/30.82 thf(func_def_110, type, sK98: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_111, type, sK99: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_112, type, sK100: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_113, type, sK101: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_114, type, sK102: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_115, type, sK103: (((a > a) > a > a) > (a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_116, type, sK104: a).
% 116.53/30.82 thf(func_def_117, type, sK105: ((a > a) > a)).
% 116.53/30.82 thf(func_def_118, type, sK106: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_119, type, sK107: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_120, type, sK108: (((a > a) > a > a) > (a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_121, type, sK109: (((a > a) > a > a) > (a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_122, type, sK110: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_123, type, sK111: ((a > a) > a)).
% 116.53/30.82 thf(func_def_124, type, sK112: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_125, type, sK113: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_126, type, sK114: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_127, type, sK115: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_128, type, sK116: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_129, type, sK117: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_130, type, sK118: ((a > a) > a)).
% 116.53/30.82 thf(func_def_131, type, sK119: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_132, type, sK120: (((a > a) > a > a) > (a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_133, type, sK121: (((a > a) > a > a) > (a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_134, type, sK122: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_135, type, sK123: ((a > a) > a)).
% 116.53/30.82 thf(func_def_136, type, sK124: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_137, type, sK125: a).
% 116.53/30.82 thf(func_def_138, type, sK126: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_139, type, sK127: a).
% 116.53/30.82 thf(func_def_140, type, sK128: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_141, type, sK129: a).
% 116.53/30.82 thf(func_def_142, type, sK130: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_143, type, sK131: a).
% 116.53/30.82 thf(func_def_144, type, sK132: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_145, type, sK133: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_146, type, sK134: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_147, type, sK135: a).
% 116.53/30.82 thf(func_def_148, type, sK136: a).
% 116.53/30.82 thf(func_def_149, type, sK137: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_150, type, sK138: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_151, type, sK139: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_152, type, sK140: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_153, type, sK141: ((a > a) > a)).
% 116.53/30.82 thf(func_def_154, type, sK142: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_155, type, sK143: a).
% 116.53/30.82 thf(func_def_156, type, sK144: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_157, type, sK145: a).
% 116.53/30.82 thf(func_def_158, type, sK146: a).
% 116.53/30.82 thf(func_def_159, type, sK147: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_160, type, sK148: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_161, type, sK149: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_162, type, sK150: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_163, type, sK151: ((a > a) > a)).
% 116.53/30.82 thf(func_def_164, type, sK152: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_165, type, sK153: ((a > a) > a)).
% 116.53/30.82 thf(func_def_166, type, sK154: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_167, type, sK155: a).
% 116.53/30.82 thf(func_def_168, type, sK156: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_169, type, sK157: a).
% 116.53/30.82 thf(func_def_170, type, sK158: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_171, type, sK159: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_172, type, sK160: a).
% 116.53/30.82 thf(func_def_173, type, sK161: a).
% 116.53/30.82 thf(func_def_174, type, sK162: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_175, type, sK163: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_176, type, sK164: a).
% 116.53/30.82 thf(func_def_177, type, sK165: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_178, type, sK166: a).
% 116.53/30.82 thf(func_def_179, type, sK167: a).
% 116.53/30.82 thf(func_def_180, type, sK168: a).
% 116.53/30.82 thf(func_def_181, type, sK169: a).
% 116.53/30.82 thf(func_def_182, type, sK170: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_183, type, sK171: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_184, type, sK172: a).
% 116.53/30.82 thf(func_def_185, type, sK173: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_186, type, sK174: ((a > a) > a)).
% 116.53/30.82 thf(func_def_187, type, sK175: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_188, type, sK176: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_189, type, sK177: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_190, type, sK178: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_191, type, sK179: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_192, type, sK180: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_193, type, sK181: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_194, type, sK182: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_195, type, sK183: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_196, type, sK184: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_197, type, sK185: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_198, type, sK186: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_199, type, sK187: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_200, type, sK188: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_201, type, sK189: a).
% 116.53/30.82 thf(func_def_202, type, sK190: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_203, type, sK191: a).
% 116.53/30.82 thf(func_def_204, type, sK192: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_205, type, sK193: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_206, type, sK194: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_207, type, sK195: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_208, type, sK196: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_209, type, sK197: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_210, type, sK198: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_211, type, sK199: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_212, type, sK200: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_213, type, sK201: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_214, type, sK202: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_215, type, sK203: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_216, type, sK204: (((a > a) > a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_217, type, sK205: (a > a)).
% 116.53/30.82 thf(func_def_218, type, sK206: (a > a)).
% 116.53/30.82 thf(func_def_219, type, sK207: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_220, type, sK208: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_221, type, sK209: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_222, type, sK210: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_223, type, sK211: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_224, type, sK212: a).
% 116.53/30.82 thf(func_def_225, type, sK213: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_226, type, sK214: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_227, type, sK215: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_228, type, sK216: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_229, type, sK217: a).
% 116.53/30.82 thf(func_def_230, type, sK218: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_231, type, sK219: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_232, type, sK220: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_233, type, sK221: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_234, type, sK222: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_235, type, sK223: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_236, type, sK224: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_237, type, sK225: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_238, type, sK226: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_239, type, sK227: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_240, type, sK228: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_241, type, sK229: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_242, type, sK230: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_243, type, sK231: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_244, type, sK232: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_245, type, sK233: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_246, type, sK234: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_247, type, sK235: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_248, type, sK236: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_249, type, sK237: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_250, type, sK238: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_251, type, sK239: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_252, type, sK240: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_253, type, sK241: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_254, type, sK242: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_255, type, sK243: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_256, type, sK244: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_257, type, sK245: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_258, type, sK246: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_259, type, sK247: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_260, type, sK248: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_261, type, sK249: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_262, type, sK250: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_263, type, sK251: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_264, type, sK252: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_265, type, sK253: ((a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_266, type, sK254: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_267, type, sK255: a).
% 116.53/30.82 thf(func_def_268, type, sK256: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_269, type, sK257: (a > a)).
% 116.53/30.82 thf(func_def_270, type, sK258: a).
% 116.53/30.82 thf(func_def_271, type, sK259: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_272, type, sK260: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_273, type, sK261: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_274, type, sK262: ((a > (a > a) > $o) > a)).
% 116.53/30.82 thf(func_def_275, type, sK263: a).
% 116.53/30.82 thf(func_def_276, type, sK264: (a > a)).
% 116.53/30.82 thf(func_def_277, type, sK265: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_278, type, sK266: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_279, type, sK267: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_280, type, sK268: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_281, type, sK269: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_282, type, sK270: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_283, type, sK271: ((a > a) > a)).
% 116.53/30.82 thf(func_def_284, type, sK272: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_285, type, sK273: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_286, type, sK274: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_287, type, sK275: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_288, type, sK276: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_289, type, sK277: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_290, type, sK278: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_291, type, sK279: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_292, type, sK280: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_293, type, sK281: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_294, type, sK282: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_295, type, sK283: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_296, type, sK284: ((a > a) > a)).
% 116.53/30.82 thf(func_def_297, type, sK285: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_298, type, sK286: (((a > a) > a > a) > (a > a) > a)).
% 116.53/30.82 thf(func_def_299, type, sK287: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_300, type, sK288: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_301, type, sK289: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_302, type, sK290: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_303, type, sK291: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_304, type, sK292: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_305, type, sK293: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_306, type, sK294: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_307, type, sK295: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_308, type, sK296: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_309, type, sK297: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_310, type, sK298: a).
% 116.53/30.82 thf(func_def_311, type, sK299: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_312, type, sK300: a).
% 116.53/30.82 thf(func_def_313, type, sK301: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_314, type, sK302: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_315, type, sK303: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_316, type, sK304: a).
% 116.53/30.82 thf(func_def_317, type, sK305: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_318, type, sK306: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_319, type, sK307: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_320, type, sK308: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_321, type, sK309: a).
% 116.53/30.82 thf(func_def_322, type, sK310: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_323, type, sK311: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_324, type, sK312: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_325, type, sK313: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_326, type, sK314: a).
% 116.53/30.82 thf(func_def_327, type, sK315: (((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_328, type, sK316: a).
% 116.53/30.82 thf(func_def_329, type, sK317: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_330, type, sK318: ((a > a) > a)).
% 116.53/30.82 thf(func_def_331, type, sK319: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_332, type, sK320: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_333, type, sK321: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_334, type, sK322: ((a > a) > a)).
% 116.53/30.82 thf(func_def_335, type, sK323: a).
% 116.53/30.82 thf(func_def_336, type, sK324: a).
% 116.53/30.82 thf(func_def_337, type, sK325: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_338, type, sK326: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_339, type, sK327: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_340, type, sK328: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_341, type, sK329: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_342, type, sK330: ((a > a) > ((a > a) > a > a) > a)).
% 116.53/30.82 thf(func_def_343, type, sK331: a).
% 116.53/30.82 thf(f1,conjecture,(
% 116.53/30.82 ! [X0 : (a > a)] : (X0 = (^[X1 : a] : ((X0 @ X1)))) => ! [X2 : (a > a),X4 : (a > a),X3 : (a > a)] : ((! [X5 : ((a > a) > $o)] : ((! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1)))))) & (X5 @ (^[X6 : a] : (X6)))) => (X5 @ X3)) & ! [X5 : ((a > a) > $o)] : (((X5 @ (^[X6 : a] : (X6))) & ! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1))))))) => (X5 @ X4))) => ! [X5 : ((a > a) > $o)] : (((X5 @ (^[X6 : a] : (X6))) & ! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1))))))) => (X5 @ (^[X1 : a] : ((X3 @ (X4 @ X1)))))))),
% 116.53/30.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM135C_pme)).
% 116.53/30.82 thf(f2,negated_conjecture,(
% 116.53/30.82 ~(! [X0 : (a > a)] : (X0 = (^[X1 : a] : ((X0 @ X1)))) => ! [X2 : (a > a),X4 : (a > a),X3 : (a > a)] : ((! [X5 : ((a > a) > $o)] : ((! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1)))))) & (X5 @ (^[X6 : a] : (X6)))) => (X5 @ X3)) & ! [X5 : ((a > a) > $o)] : (((X5 @ (^[X6 : a] : (X6))) & ! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1))))))) => (X5 @ X4))) => ! [X5 : ((a > a) > $o)] : (((X5 @ (^[X6 : a] : (X6))) & ! [X7 : (a > a)] : ((X5 @ X7) => (X5 @ (^[X1 : a] : ((X2 @ (X7 @ X1))))))) => (X5 @ (^[X1 : a] : ((X3 @ (X4 @ X1))))))))),
% 116.53/30.82 inference(negated_conjecture,[status(cth)],[f1])).
% 116.53/30.82 thf(f3,plain,(
% 116.53/30.82 ~(! [X0 : (a > a)] : (X0 = (^[X1 : a] : ((X0 @ X1)))) => ! [X2 : (a > a),X3 : (a > a),X4 : (a > a)] : ((! [X5 : ((a > a) > $o)] : ((! [X6 : (a > a)] : ((X5 @ X6) => (X5 @ (^[X7 : a] : ((X2 @ (X6 @ X7)))))) & (X5 @ (^[X8 : a] : (X8)))) => (X5 @ X4)) & ! [X9 : ((a > a) > $o)] : (((X9 @ (^[X10 : a] : (X10))) & ! [X11 : (a > a)] : ((X9 @ X11) => (X9 @ (^[X12 : a] : ((X2 @ (X11 @ X12))))))) => (X9 @ X3))) => ! [X13 : ((a > a) > $o)] : (((X13 @ (^[X14 : a] : (X14))) & ! [X15 : (a > a)] : ((X13 @ X15) => (X13 @ (^[X16 : a] : ((X2 @ (X15 @ X16))))))) => (X13 @ (^[X17 : a] : ((X4 @ (X3 @ X17))))))))),
% 116.53/30.82 inference(rectify,[],[f2])).
% 116.53/30.82 thf(f4,plain,(
% 116.53/30.82 ~(! [X0 : (a > a)] : ((^[Y0 : a]: (X0 @ Y0)) = X0) => ! [X2 : (a > a),X3 : (a > a),X4 : (a > a)] : ((! [X5 : ((a > a) > $o)] : ((! [X6 : (a > a)] : (($true = ((X5 @ X6))) => ($true = ((X5 @ (^[Y0 : a]: (X2 @ (X6 @ Y0))))))) & (((X5 @ (^[Y0 : a]: (Y0)))) = $true)) => (((X5 @ X4)) = $true)) & ! [X9 : ((a > a) > $o)] : ((($true = ((X9 @ (^[Y0 : a]: (Y0))))) & ! [X11 : (a > a)] : (($true = ((X9 @ X11))) => ($true = ((X9 @ (^[Y0 : a]: (X2 @ (X11 @ Y0)))))))) => (((X9 @ X3)) = $true))) => ! [X13 : ((a > a) > $o)] : ((($true = ((X13 @ (^[Y0 : a]: (Y0))))) & ! [X15 : (a > a)] : (($true = ((X13 @ X15))) => ($true = ((X13 @ (^[Y0 : a]: (X2 @ (X15 @ Y0)))))))) => ($true = ((X13 @ (^[Y0 : a]: (X4 @ (X3 @ Y0)))))))))),
% 116.53/30.82 inference(fool_elimination,[],[f3])).
% 116.53/30.82 thf(f5,plain,(
% 116.53/30.82 ~(! [X0 : (a > a)] : ((^[Y0 : a]: (X0 @ Y0)) = X0) => ! [X3 : (a > a),X1 : (a > a),X2 : (a > a)] : ((! [X6 : ((a > a) > $o)] : ((! [X7 : (a > a)] : (($true = ((X6 @ X7))) => (((X6 @ (^[Y0 : a]: (X1 @ (X7 @ Y0))))) = $true)) & (((X6 @ (^[Y0 : a]: (Y0)))) = $true)) => (((X6 @ X2)) = $true)) & ! [X4 : ((a > a) > $o)] : ((! [X5 : (a > a)] : (($true = ((X4 @ X5))) => ($true = ((X4 @ (^[Y0 : a]: (X1 @ (X5 @ Y0))))))) & ($true = ((X4 @ (^[Y0 : a]: (Y0)))))) => ($true = ((X4 @ X3))))) => ! [X8 : ((a > a) > $o)] : ((! [X9 : (a > a)] : ((((X8 @ X9)) = $true) => (((X8 @ (^[Y0 : a]: (X1 @ (X9 @ Y0))))) = $true)) & ($true = ((X8 @ (^[Y0 : a]: (Y0)))))) => ($true = ((X8 @ (^[Y0 : a]: (X3 @ (X2 @ Y0)))))))))),
% 116.53/30.82 inference(rectify,[],[f4])).
% 116.53/30.82 thf(f6,plain,(
% 116.53/30.82 ? [X3 : (a > a),X1 : (a > a),X2 : (a > a)] : (? [X8 : ((a > a) > $o)] : (($true != ((X8 @ (^[Y0 : a]: (X3 @ (X2 @ Y0)))))) & (! [X9 : (a > a)] : ((((X8 @ (^[Y0 : a]: (X1 @ (X9 @ Y0))))) = $true) | (((X8 @ X9)) != $true)) & ($true = ((X8 @ (^[Y0 : a]: (Y0))))))) & (! [X6 : ((a > a) > $o)] : ((((X6 @ X2)) = $true) | (? [X7 : (a > a)] : (($true = ((X6 @ X7))) & (((X6 @ (^[Y0 : a]: (X1 @ (X7 @ Y0))))) != $true)) | (((X6 @ (^[Y0 : a]: (Y0)))) != $true))) & ! [X4 : ((a > a) > $o)] : (($true = ((X4 @ X3))) | (? [X5 : (a > a)] : (($true != ((X4 @ (^[Y0 : a]: (X1 @ (X5 @ Y0)))))) & ($true = ((X4 @ X5)))) | ($true != ((X4 @ (^[Y0 : a]: (Y0))))))))) & ! [X0 : (a > a)] : ((^[Y0 : a]: (X0 @ Y0)) = X0)),
% 116.53/30.82 inference(ennf_transformation,[],[f5])).
% 116.53/30.82 thf(f7,plain,(
% 116.53/30.82 ? [X1 : (a > a),X2 : (a > a),X3 : (a > a)] : (! [X4 : ((a > a) > $o)] : (? [X5 : (a > a)] : (($true != ((X4 @ (^[Y0 : a]: (X1 @ (X5 @ Y0)))))) & ($true = ((X4 @ X5)))) | ($true != ((X4 @ (^[Y0 : a]: (Y0))))) | ($true = ((X4 @ X3)))) & ! [X6 : ((a > a) > $o)] : ((((X6 @ (^[Y0 : a]: (Y0)))) != $true) | ? [X7 : (a > a)] : (($true = ((X6 @ X7))) & (((X6 @ (^[Y0 : a]: (X1 @ (X7 @ Y0))))) != $true)) | (((X6 @ X2)) = $true)) & ? [X8 : ((a > a) > $o)] : (($true = ((X8 @ (^[Y0 : a]: (Y0))))) & ($true != ((X8 @ (^[Y0 : a]: (X3 @ (X2 @ Y0)))))) & ! [X9 : (a > a)] : ((((X8 @ (^[Y0 : a]: (X1 @ (X9 @ Y0))))) = $true) | (((X8 @ X9)) != $true)))) & ! [X0 : (a > a)] : ((^[Y0 : a]: (X0 @ Y0)) = X0)),
% 116.53/30.82 inference(flattening,[],[f6])).
% 116.53/30.82 thf(f8,plain,(
% 116.53/30.82 ? [X0 : (a > a),X1 : (a > a),X2 : (a > a)] : (! [X3 : ((a > a) > $o)] : (? [X4 : (a > a)] : (($true != ((X3 @ (^[Y0 : a]: (X0 @ (X4 @ Y0)))))) & (((X3 @ X4)) = $true)) | ($true != ((X3 @ (^[Y0 : a]: (Y0))))) | ($true = ((X3 @ X2)))) & ! [X5 : ((a > a) > $o)] : ((((X5 @ (^[Y0 : a]: (Y0)))) != $true) | ? [X6 : (a > a)] : (($true = ((X5 @ X6))) & (((X5 @ (^[Y0 : a]: (X0 @ (X6 @ Y0))))) != $true)) | ($true = ((X5 @ X1)))) & ? [X7 : ((a > a) > $o)] : ((((X7 @ (^[Y0 : a]: (Y0)))) = $true) & ($true != ((X7 @ (^[Y0 : a]: (X2 @ (X1 @ Y0)))))) & ! [X8 : (a > a)] : ((((X7 @ (^[Y0 : a]: (X0 @ (X8 @ Y0))))) = $true) | (((X7 @ X8)) != $true)))) & ! [X9 : (a > a)] : ((^[Y0 : a]: (X9 @ Y0)) = X9)),
% 116.53/30.82 inference(rectify,[],[f7])).
% 116.53/30.82 thf(f9,plain,(
% 116.53/30.82 (! [X3 : ((a > a) > $o)] : ((($true != ((X3 @ (^[Y0 : a]: (sK0 @ (sK3 @ X3 @ Y0)))))) & ($true = ((X3 @ (sK3 @ X3))))) | ($true != ((X3 @ (^[Y0 : a]: (Y0))))) | ($true = ((X3 @ sK2)))) & ! [X5 : ((a > a) > $o)] : ((((X5 @ (^[Y0 : a]: (Y0)))) != $true) | (($true = ((X5 @ (sK4 @ X5)))) & (((X5 @ (^[Y0 : a]: (sK0 @ (sK4 @ X5 @ Y0))))) != $true)) | (((X5 @ sK1)) = $true)) & (($true = ((sK5 @ (^[Y0 : a]: (Y0))))) & (((sK5 @ (^[Y0 : a]: (sK2 @ (sK1 @ Y0))))) != $true) & ! [X8 : (a > a)] : (($true = ((sK5 @ (^[Y0 : a]: (sK0 @ (X8 @ Y0)))))) | ($true != ((sK5 @ X8)))))) & ! [X9 : (a > a)] : ((^[Y0 : a]: (X9 @ Y0)) = X9)),
% 116.53/30.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,vAPP,vAPP,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X6,sK4 @ X5),skolemize(X6,sK4 @ X5),skolemize(X7,sK5)],[f8])).
% 116.53/30.82 thf(f11,plain,(
% 116.53/30.82 ( ! [X8 : (a > a)] : (($true != ((sK5 @ X8))) | ($true = ((sK5 @ (^[Y0 : a]: (sK0 @ (X8 @ Y0))))))) )),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f12,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK2 @ (sK1 @ Y0))))) != $true)),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f13,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (Y0)))))),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f14,plain,(
% 116.53/30.82 ( ! [X5 : ((a > a) > $o)] : ((((X5 @ (^[Y0 : a]: (sK0 @ (sK4 @ X5 @ Y0))))) != $true) | (((X5 @ (^[Y0 : a]: (Y0)))) != $true) | (((X5 @ sK1)) = $true)) )),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f15,plain,(
% 116.53/30.82 ( ! [X5 : ((a > a) > $o)] : ((((X5 @ (^[Y0 : a]: (Y0)))) != $true) | ($true = ((X5 @ (sK4 @ X5)))) | (((X5 @ sK1)) = $true)) )),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f16,plain,(
% 116.53/30.82 ( ! [X3 : ((a > a) > $o)] : (($true != ((X3 @ (^[Y0 : a]: (Y0))))) | ($true = ((X3 @ (sK3 @ X3)))) | ($true = ((X3 @ sK2)))) )),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f17,plain,(
% 116.53/30.82 ( ! [X3 : ((a > a) > $o)] : (($true != ((X3 @ (^[Y0 : a]: (sK0 @ (sK3 @ X3 @ Y0)))))) | ($true = ((X3 @ sK2))) | ($true != ((X3 @ (^[Y0 : a]: (Y0)))))) )),
% 116.53/30.82 inference(cnf_transformation,[],[f9])).
% 116.53/30.82 thf(f19,definition,(
% 116.53/30.82 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 116.53/30.82 introduced(theory,[fool_exhaustiveness_axiom])).
% 116.53/30.82 thf(f36,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : ((((X0 @ (^[Y0 : a]: (Y0)))) != (^[Y0 : a]: (Y0))) | ((((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK1)) = $true) | ($true != $true) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK4 @ (^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0)))))))) )),
% 116.53/30.82 inference(constrained_superposition,[],[f15,f13])).
% 116.53/30.82 thf(f67,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (((((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK1)) = $true) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK4 @ (^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))))))) | (((X0 @ (^[Y0 : a]: (Y0)))) != (^[Y0 : a]: (Y0)))) )),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f36])).
% 116.53/30.82 thf(f68,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : ((((X0 @ (^[Y0 : a]: (Y0)))) != (^[Y0 : a]: (Y0))) | ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ (X0 @ sK1 @ Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0))))))) )),
% 116.53/30.82 inference(beta-eta_normalization,[],[f67])).
% 116.53/30.82 thf(f207,plain,(
% 116.53/30.82 ( ! [X0 : (a > a)] : (($true != $true) | (((sK5 @ X0)) = $false) | ($true = ((sK5 @ (^[Y0 : a]: (sK0 @ (X0 @ Y0))))))) )),
% 116.53/30.82 inference(constrained_superposition,[],[f11,f19])).
% 116.53/30.82 thf(f223,plain,(
% 116.53/30.82 ( ! [X0 : (a > a)] : (($true = ((sK5 @ (^[Y0 : a]: (sK0 @ (X0 @ Y0)))))) | (((sK5 @ X0)) = $false)) )),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f207])).
% 116.53/30.82 thf(f263,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : ((((sK5 @ X1)) = $false) | ((^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1) | ((((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK1)) = $true) | ($true != (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: (Y0))))) | ($true != $true)) )),
% 116.53/30.82 inference(constrained_superposition,[],[f14,f223])).
% 116.53/30.82 thf(f265,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : ((((sK5 @ X1)) = $false) | ($true != (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: (Y0))))) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK2))) | ($true != $true) | ((^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1)) )),
% 116.53/30.82 inference(constrained_superposition,[],[f17,f223])).
% 116.53/30.82 thf(f269,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : ((((sK5 @ X1)) = $false) | ((((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK1)) = $true) | ($true != (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: (Y0))))) | ((^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1)) )),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f263])).
% 116.53/30.82 thf(f270,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : (((^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1) | ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ (X0 @ sK1 @ Y0)))))) | (((sK5 @ X1)) = $false) | ($true != ((sK5 @ (X0 @ (^[Y0 : a]: (Y0))))))) )),
% 116.53/30.82 inference(beta-eta_normalization,[],[f269])).
% 116.53/30.82 thf(f277,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : (($true != (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: (Y0))))) | ((^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK2))) | (((sK5 @ X1)) = $false)) )),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f265])).
% 116.53/30.82 thf(f278,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a),X1 : (a > a)] : (((^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))) != X1) | (((sK5 @ X1)) = $false) | ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ (X0 @ sK2 @ Y0)))))) | ($true != ((sK5 @ (X0 @ (^[Y0 : a]: (Y0))))))) )),
% 116.53/30.82 inference(beta-eta_normalization,[],[f277])).
% 116.53/30.82 thf(f902,definition,(
% 116.53/30.82 spl6_19 <=> (((sK5 @ sK1)) = $true)),
% 116.53/30.82 introduced(definition,[new_symbols(definition,[spl6_19])],[avatar_definition])).
% 116.53/30.82 thf(f904,plain,(
% 116.53/30.82 (((sK5 @ sK1)) = $true) | ~spl6_19),
% 116.53/30.82 inference(avatar_component_clause,[],[f902])).
% 116.53/30.82 thf(f1167,definition,(
% 116.53/30.82 spl6_21 <=> ($true = ((sK5 @ (sK4 @ sK5))))),
% 116.53/30.82 introduced(definition,[new_symbols(definition,[spl6_21])],[avatar_definition])).
% 116.53/30.82 thf(f1169,plain,(
% 116.53/30.82 ($true = ((sK5 @ (sK4 @ sK5)))) | ~spl6_21),
% 116.53/30.82 inference(avatar_component_clause,[],[f1167])).
% 116.53/30.82 thf(f1610,definition,(
% 116.53/30.82 spl6_42 <=> (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $true)),
% 116.53/30.82 introduced(definition,[new_symbols(definition,[spl6_42])],[avatar_definition])).
% 116.53/30.82 thf(f1611,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) != $true) | spl6_42),
% 116.53/30.82 inference(avatar_component_clause,[],[f1610])).
% 116.53/30.82 thf(f1612,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $true) | ~spl6_42),
% 116.53/30.82 inference(avatar_component_clause,[],[f1610])).
% 116.53/30.82 thf(f36329,definition,(
% 116.53/30.82 spl6_210 <=> ($false = ((sK5 @ (sK4 @ sK5))))),
% 116.53/30.82 introduced(definition,[new_symbols(definition,[spl6_210])],[avatar_definition])).
% 116.53/30.82 thf(f36331,plain,(
% 116.53/30.82 ($false = ((sK5 @ (sK4 @ sK5)))) | ~spl6_210),
% 116.53/30.82 inference(avatar_component_clause,[],[f36329])).
% 116.53/30.82 thf(f41087,plain,(
% 116.53/30.82 ($true = $false) | (~spl6_21 | ~spl6_210)),
% 116.53/30.82 inference(constrained_superposition,[],[f36331,f1169])).
% 116.53/30.82 thf(f41160,plain,(
% 116.53/30.82 $false | (~spl6_21 | ~spl6_210)),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f41087])).
% 116.53/30.82 thf(f41161,plain,(
% 116.53/30.82 ~spl6_21 | ~spl6_210),
% 116.53/30.82 inference(avatar_contradiction_clause,[],[f41160])).
% 116.53/30.82 thf(f41319,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK3 @ (^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))))))) | (sK1 != ((X0 @ (^[Y0 : a]: (Y0))))) | ($true != $true) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK2)))) ) | ~spl6_19),
% 116.53/30.82 inference(constrained_superposition,[],[f16,f904])).
% 116.53/30.82 thf(f41346,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK3 @ (^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))))))) | ($true = (((^[Y0 : a > a]: (sK5 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK2))) | (sK1 != ((X0 @ (^[Y0 : a]: (Y0)))))) ) | ~spl6_19),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f41319])).
% 116.53/30.82 thf(f41347,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : ((sK1 != ((X0 @ (^[Y0 : a]: (Y0))))) | (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0))))) = $true) | ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ (X0 @ sK2 @ Y0))))))) ) | ~spl6_19),
% 116.53/30.82 inference(beta-eta_normalization,[],[f41346])).
% 116.53/30.82 thf(f47079,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (($true = ((sK5 @ (^[Y0 : a]: (sK1 @ (X0 @ sK1 @ Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0)))))) | (((X0 @ (^[Y0 : a]: (Y0)) @ (sK170 @ X0))) != (((^[Y0 : a]: (Y0)) @ (sK170 @ X0))))) )),
% 116.53/30.82 inference(negative_extensionality,[],[f68])).
% 116.53/30.82 thf(f47131,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : ((((X0 @ (^[Y0 : a]: (Y0)) @ (sK170 @ X0))) != ((sK170 @ X0))) | ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ (X0 @ sK1 @ Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0))))))) )),
% 116.53/30.82 inference(beta-eta_normalization,[],[f47079])).
% 116.53/30.82 thf(f59028,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (($true != ((sK5 @ (X0 @ (^[Y0 : a]: (Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ (X0 @ sK1 @ Y0)))))) | (((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))))) = $false)) )),
% 116.53/30.82 inference(equality_resolution,[],[f270])).
% 116.53/30.82 thf(f59191,plain,(
% 116.53/30.82 ( ! [X0 : ((a > a) > a > a)] : (($true != ((sK5 @ (X0 @ (^[Y0 : a]: (Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ (X0 @ sK2 @ Y0)))))) | ($false = ((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0))))))) )),
% 116.53/30.82 inference(equality_resolution,[],[f278])).
% 116.53/30.82 thf(f59375,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2)))))) @ Y0))))) = $true) | ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ sK1 @ Y0))))))),
% 116.53/30.82 inference(equality_resolution,[],[f47131])).
% 116.53/30.82 thf(f59388,plain,(
% 116.53/30.82 ($true = ((sK5 @ (sK4 @ sK5)))) | (((sK5 @ sK1)) = $true)),
% 116.53/30.82 inference(beta-eta_normalization,[],[f59375])).
% 116.53/30.82 thf(f94347,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (sK1 @ ((^[Y5 : a > a]: ((^[Y6 : a]: (Y6)))) @ Y3 @ Y4))))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (sK1 @ ((^[Y5 : a > a]: ((^[Y6 : a]: (Y6)))) @ Y3 @ Y4))))) @ Y1 @ Y2)))))) @ Y0)))))) | ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ sK2 @ Y0)))))) | ~spl6_19),
% 116.53/30.82 inference(equality_resolution,[],[f41347])).
% 116.53/30.82 thf(f94376,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK2 @ (sK1 @ Y0))))) = $true) | (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $true) | ~spl6_19),
% 116.53/30.82 inference(beta-eta_normalization,[],[f94347])).
% 116.53/30.82 thf(f94397,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $true) | ~spl6_19),
% 116.53/30.82 inference(forward_subsumption_resolution,[],[f94376,f12])).
% 116.53/30.82 thf(f94399,plain,(
% 116.53/30.82 $false | (~spl6_19 | spl6_42)),
% 116.53/30.82 inference(forward_subsumption_resolution,[],[f94397,f1611])).
% 116.53/30.82 thf(f94400,plain,(
% 116.53/30.82 ~spl6_19 | spl6_42),
% 116.53/30.82 inference(avatar_contradiction_clause,[],[f94399])).
% 116.53/30.82 thf(f101990,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ sK1 @ Y0)))))) | ($true != $true) | (((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (Y5)))) @ Y2 @ Y3))))) @ Y1))) @ Y0))))) = $false)),
% 116.53/30.82 inference(constrained_superposition,[],[f59028,f13])).
% 116.53/30.82 thf(f102901,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ sK1 @ Y0)))))) | (((sK5 @ (^[Y0 : a]: (sK4 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (Y2)))) @ (^[Y1 : a]: (sK0 @ (sK4 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (Y5)))) @ Y2 @ Y3))))) @ Y1))) @ Y0))))) = $false)),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f101990])).
% 116.53/30.82 thf(f102902,plain,(
% 116.53/30.82 (((sK5 @ sK1)) = $true) | ($false = ((sK5 @ (sK4 @ sK5))))),
% 116.53/30.82 inference(beta-eta_normalization,[],[f102901])).
% 116.53/30.82 thf(f104944,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ sK2 @ Y0)))))) | ($true != $true) | (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (sK1 @ ((^[Y5 : a > a]: ((^[Y6 : a]: (Y6)))) @ Y3 @ Y4))))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (sK1 @ ((^[Y6 : a > a]: ((^[Y7 : a]: (Y7)))) @ Y4 @ Y5))))) @ Y2 @ Y3))))) @ Y1))) @ Y0))))) = $false) | ~spl6_19),
% 116.53/30.82 inference(constrained_superposition,[],[f59191,f904])).
% 116.53/30.82 thf(f105003,plain,(
% 116.53/30.82 ($true = ((sK5 @ (^[Y0 : a]: (sK2 @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ sK2 @ Y0)))))) | (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (sK1 @ ((^[Y5 : a > a]: ((^[Y6 : a]: (Y6)))) @ Y3 @ Y4))))) @ Y1 @ Y2))))) @ ((^[Y1 : a > a]: ((^[Y2 : a]: (sK1 @ ((^[Y3 : a > a]: ((^[Y4 : a]: (Y4)))) @ Y1 @ Y2))))) @ (^[Y1 : a]: (sK0 @ (sK3 @ (^[Y2 : a > a]: (sK5 @ (^[Y3 : a]: (Y2 @ ((^[Y4 : a > a]: ((^[Y5 : a]: (sK1 @ ((^[Y6 : a > a]: ((^[Y7 : a]: (Y7)))) @ Y4 @ Y5))))) @ Y2 @ Y3))))) @ Y1))) @ Y0))))) = $false) | ~spl6_19),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f104944])).
% 116.53/30.82 thf(f105004,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK2 @ (sK1 @ Y0))))) = $true) | (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $false) | ~spl6_19),
% 116.53/30.82 inference(beta-eta_normalization,[],[f105003])).
% 116.53/30.82 thf(f106411,plain,(
% 116.53/30.82 (((sK5 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > a]: (sK5 @ (^[Y2 : a]: (Y1 @ (sK1 @ Y2))))) @ (sK1 @ Y0))))) = $false) | ~spl6_19),
% 116.53/30.82 inference(forward_subsumption_resolution,[],[f105004,f12])).
% 116.53/30.82 thf(f140077,plain,(
% 116.53/30.82 ($true = $false) | (~spl6_19 | ~spl6_42)),
% 116.53/30.82 inference(constrained_superposition,[],[f106411,f1612])).
% 116.53/30.82 thf(f140423,plain,(
% 116.53/30.82 $false | (~spl6_19 | ~spl6_42)),
% 116.53/30.82 inference(trivial_inequality_removal,[],[f140077])).
% 116.53/30.82 thf(f140424,plain,(
% 116.53/30.82 ~spl6_19 | ~spl6_42),
% 116.53/30.82 inference(avatar_contradiction_clause,[],[f140423])).
% 116.53/30.82 thf(f141784,plain,(
% 116.53/30.82 spl6_19 | spl6_210),
% 116.53/30.82 inference(avatar_split_clause,[],[f102902,f36329,f902])).
% 116.53/30.82 thf(f141785,plain,(
% 116.53/30.82 spl6_19 | spl6_21),
% 116.53/30.82 inference(avatar_split_clause,[],[f59388,f1167,f902])).
% 116.53/30.82 cnf(s799, plain, ~spl6_21 | ~spl6_210, inference(sat_conversion,[],[f41161])).
% 116.53/30.82 cnf(s1099, plain, ~spl6_19 | spl6_42, inference(sat_conversion,[],[f94400])).
% 116.53/30.82 cnf(s1265, plain, ~spl6_19 | ~spl6_42, inference(sat_conversion,[],[f140424])).
% 116.53/30.82 cnf(s1729, plain, spl6_19 | spl6_210, inference(sat_conversion,[],[f141784])).
% 116.53/30.82 cnf(s1730, plain, spl6_19 | spl6_21, inference(sat_conversion,[],[f141785])).
% 116.53/30.82 cnf(s1731, plain, ~spl6_19, inference(rat,[],[s1099,s1265])).
% 116.53/30.82 cnf(s1732, plain, spl6_21, inference(rat,[],[s1730,s1731])).
% 116.53/30.82 cnf(s1733, plain, spl6_210, inference(rat,[],[s1729,s1731])).
% 116.53/30.82 cnf(s1738, plain, $false, inference(rat,[],[s799,s1733,s1732])).
% 116.53/30.82 thf(f141786,plain,(
% 116.53/30.82 $false),
% 116.53/30.82 inference(avatar_sat_refutation,[],[s1738])).
% 116.53/30.82 % SZS output end Proof for theBenchmark
% 116.53/30.82 % (1767882)------------------------------
% 116.53/30.82 % (1767882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.53/30.82 % (1767882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.53/30.82 % (1767882)CaDiCaL version: 2.1.3
% 116.53/30.82 % (1767882)Termination reason: Refutation
% 116.53/30.82 % (1767882)Time elapsed: 17.425 s
% 116.53/30.82 % (1767882)Peak memory usage: 55 MB
% 116.53/30.82 % (1767882)Instructions burned: 39866 (million)
% 116.53/30.82 % (1767766)Success in time 30.565 s
% 116.53/30.82 % Vampire exiting
%------------------------------------------------------------------------------