%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP134^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:10:50 AM UTC 2026
% Result : Theorem 128.05s 33.96s
% Output : Refutation 128.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP134^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 % Computer : n015.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Tue Sep 29 20:02:04 UTC 2026
% 0.25/0.27 % CPUTime :
% 0.25/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.32 Running first-order model finding
% 0.25/0.32 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
% 7.19/1.55 % (4041028)Will run a generic schedule for satisfiability detection.
% 7.19/1.55 % (4041033)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3988203495_2999 on theBenchmark for (2999ds/0Mi)
% 7.19/1.55 % (4041034)% WARNING: option uhcvi not known.
% 7.19/1.55 % (4041034)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2778325403:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.19/1.55 % (4041035)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2420245728:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.19/1.55 % (4041037)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3583147918:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.19/1.55 % (4041036)dis+10_1_sil=32000:sp=arity:random_seed=3071286312:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.19/1.55 % (4041038)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4235133248:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.19/1.55 % (4041039)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=260949608:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.19/1.55 % Exception at run slice level
% 7.19/1.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.19/1.55 % (4041037)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.19/1.55 % (4041034)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.19/1.55 % (4041047)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3140650506:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.19/1.55 % (4041034)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.19/1.55 % Exception at run slice level
% 7.19/1.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.19/1.55 % (4041036)Instruction limit reached!
% 7.19/1.55 % (4041036)------------------------------
% 7.19/1.55 % (4041036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.55 % (4041036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.55 % (4041036)CaDiCaL version: 2.1.3
% 7.19/1.55 % (4041036)Termination reason: Instruction limit
% 7.19/1.55 % (4041036)Termination phase: Saturation
% 7.19/1.55 % (4041036)Time elapsed: 0.088 s
% 7.19/1.55 % (4041036)Peak memory usage: 13 MB
% 7.19/1.55 % (4041036)Instructions burned: 103 (million)
% 7.19/1.55 % (4041049)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1013211497:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.19/1.55 % (4041037)Instruction limit reached!
% 7.19/1.55 % (4041037)------------------------------
% 7.19/1.55 % (4041037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.55 % (4041037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.55 % (4041037)CaDiCaL version: 2.1.3
% 7.19/1.55 % (4041037)Termination reason: Instruction limit
% 7.19/1.55 % (4041037)Termination phase: Saturation
% 7.19/1.55 % (4041037)Time elapsed: 0.096 s
% 7.19/1.55 % (4041037)Peak memory usage: 13 MB
% 7.19/1.55 % (4041037)Instructions burned: 116 (million)
% 7.19/1.55 % (4041038)Instruction limit reached!
% 7.19/1.55 % (4041038)------------------------------
% 7.19/1.55 % (4041038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.55 % (4041038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.55 % (4041038)CaDiCaL version: 2.1.3
% 7.19/1.55 % (4041038)Termination reason: Instruction limit
% 7.19/1.55 % (4041038)Termination phase: Saturation
% 7.19/1.55 % (4041038)Time elapsed: 0.110 s
% 7.19/1.55 % (4041038)Peak memory usage: 13 MB
% 7.19/1.55 % (4041038)Instructions burned: 131 (million)
% 7.19/1.55 % (4041050)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=2280549180:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.19/1.55 % (4041052)ott-21_1_sil=16000:fs=off:random_seed=759363570:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.19/1.55 % (4041039)Instruction limit reached!
% 7.19/1.55 % (4041039)------------------------------
% 7.19/1.55 % (4041039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.55 % (4041039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/4.56 % (4041039)CaDiCaL version: 2.1.3
% 29.50/4.56 % (4041039)Termination reason: Instruction limit
% 29.50/4.56 % (4041039)Termination phase: Saturation
% 29.50/4.56 % (4041039)Time elapsed: 0.137 s
% 29.50/4.56 % (4041039)Peak memory usage: 14 MB
% 29.50/4.56 % (4041039)Instructions burned: 159 (million)
% 29.50/4.56 % (4041053)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2258018761:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 29.50/4.56 % (4041050)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 29.50/4.56 % (4041049)Instruction limit reached!
% 29.50/4.56 % (4041049)------------------------------
% 29.50/4.56 % (4041049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.50/4.56 % (4041049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/4.56 % (4041049)CaDiCaL version: 2.1.3
% 29.50/4.56 % (4041049)Termination reason: Instruction limit
% 29.50/4.56 % (4041049)Termination phase: Saturation
% 29.50/4.56 % (4041049)Time elapsed: 0.062 s
% 29.50/4.56 % (4041049)Peak memory usage: 13 MB
% 29.50/4.56 % (4041049)Instructions burned: 131 (million)
% 29.50/4.56 % (4041058)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2431152477:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 29.50/4.56 % (4041056)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2522313186:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 29.50/4.56 % (4041050)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 29.50/4.56 % Exception at run slice level
% 29.50/4.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 29.50/4.56 % (4041061)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2308670763:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 29.50/4.56 % (4041052)Instruction limit reached!
% 29.50/4.56 % (4041052)------------------------------
% 29.50/4.56 % (4041052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.50/4.56 % (4041052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/4.56 % (4041052)CaDiCaL version: 2.1.3
% 29.50/4.56 % (4041052)Termination reason: Instruction limit
% 29.50/4.56 % (4041052)Termination phase: Saturation
% 29.50/4.56 % (4041052)Time elapsed: 0.132 s
% 29.50/4.56 % (4041052)Peak memory usage: 13 MB
% 29.50/4.56 % (4041052)Instructions burned: 181 (million)
% 29.50/4.56 % (4041063)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=1240866101:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 29.50/4.56 % Exception at run slice level
% 29.50/4.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 29.50/4.56 % (4041063)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 29.50/4.56 % (4041066)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1751705769:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 29.50/4.56 % (4041066)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 29.50/4.56 % (4041053)Instruction limit reached!
% 29.50/4.56 % (4041053)------------------------------
% 29.50/4.56 % (4041053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.50/4.56 % (4041053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/4.56 % (4041053)CaDiCaL version: 2.1.3
% 29.50/4.56 % (4041053)Termination reason: Instruction limit
% 29.50/4.56 % (4041053)Termination phase: Saturation
% 29.50/4.56 % (4041053)Time elapsed: 0.439 s
% 29.50/4.56 % (4041053)Peak memory usage: 15 MB
% 29.50/4.56 % (4041053)Instructions burned: 477 (million)
% 29.50/4.56 % (4041069)fmb+10_1_sil=64000:random_seed=1254016073:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 29.50/4.56 % (4041069)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 29.50/4.56 % Exception at run slice level
% 29.50/4.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 29.50/4.56 % (4041058)Instruction limit reached!
% 29.50/4.56 % (4041058)------------------------------
% 29.50/4.56 % (4041058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.50/4.56 % (4041058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.67 % (4041058)CaDiCaL version: 2.1.3
% 87.16/12.67 % (4041058)Termination reason: Instruction limit
% 87.16/12.67 % (4041058)Termination phase: Saturation
% 87.16/12.67 % (4041058)Time elapsed: 0.531 s
% 87.16/12.67 % (4041058)Peak memory usage: 18 MB
% 87.16/12.67 % (4041058)Instructions burned: 1180 (million)
% 87.16/12.67 % (4041071)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3999286750:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 87.16/12.67 % (4041050)Instruction limit reached!
% 87.16/12.67 % (4041050)------------------------------
% 87.16/12.67 % (4041050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.67 % (4041050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.67 % (4041050)CaDiCaL version: 2.1.3
% 87.16/12.67 % (4041050)Termination reason: Instruction limit
% 87.16/12.67 % (4041050)Termination phase: Saturation
% 87.16/12.67 % (4041050)Time elapsed: 0.601 s
% 87.16/12.67 % (4041050)Peak memory usage: 16 MB
% 87.16/12.67 % (4041050)Instructions burned: 685 (million)
% 87.16/12.67 % (4041072)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4119244560:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 87.16/12.67 % (4041075)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2544632380:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 87.16/12.67 % (4041075)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 87.16/12.67 % Exception at run slice level
% 87.16/12.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 87.16/12.67 % Exception at run slice level
% 87.16/12.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 87.16/12.67 % (4041078)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3816876560:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 87.16/12.67 % (4041077)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=388808068:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 87.16/12.67 % Exception at run slice level
% 87.16/12.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 87.16/12.67 % (4041077)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 87.16/12.67 % (4041077)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 87.16/12.67 % (4041081)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1090610209:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 87.16/12.67 % Exception at run slice level
% 87.16/12.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 87.16/12.67 % (4041063)Instruction limit reached!
% 87.16/12.67 % (4041063)------------------------------
% 87.16/12.67 % (4041063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.67 % (4041063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.67 % (4041063)CaDiCaL version: 2.1.3
% 87.16/12.67 % (4041063)Termination reason: Instruction limit
% 87.16/12.67 % (4041063)Termination phase: Saturation
% 87.16/12.67 % (4041063)Time elapsed: 0.619 s
% 87.16/12.67 % (4041063)Peak memory usage: 19 MB
% 87.16/12.67 % (4041063)Instructions burned: 692 (million)
% 87.16/12.67 % (4041083)ott-2_1_sil=16000:newcnf=on:random_seed=170003760:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 87.16/12.67 % (4041084)ott+10_1_sil=32000:tgt=ground:random_seed=2735132137:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi)
% 87.16/12.67 % (4041083)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 87.16/12.67 % (4041066)Instruction limit reached!
% 87.16/12.67 % (4041066)------------------------------
% 87.16/12.67 % (4041066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.67 % (4041066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.67 % (4041066)CaDiCaL version: 2.1.3
% 87.16/12.67 % (4041066)Termination reason: Instruction limit
% 87.16/12.67 % (4041066)Termination phase: Saturation
% 87.16/12.67 % (4041066)Time elapsed: 0.768 s
% 87.16/12.67 % (4041066)Peak memory usage: 19 MB
% 87.16/12.67 % (4041066)Instructions burned: 879 (million)
% 87.16/12.67 % (4041087)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4107178190:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 87.16/12.67 % Exception at run slice level
% 138.25/19.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.25/19.87 % (4041089)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=575171584:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 138.25/19.87 % (4041089)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 138.25/19.87 % (4041083)Instruction limit reached!
% 138.25/19.87 % (4041083)------------------------------
% 138.25/19.87 % (4041083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.25/19.87 % (4041083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.25/19.87 % (4041083)CaDiCaL version: 2.1.3
% 138.25/19.87 % (4041083)Termination reason: Instruction limit
% 138.25/19.87 % (4041083)Termination phase: Saturation
% 138.25/19.87 % (4041083)Time elapsed: 0.743 s
% 138.25/19.87 % (4041083)Peak memory usage: 17 MB
% 138.25/19.87 % (4041083)Instructions burned: 869 (million)
% 138.25/19.87 % (4041091)dis+21_1_sil=32000:sas=cadical:random_seed=810604967:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi)
% 138.25/19.87 % (4041077)Instruction limit reached!
% 138.25/19.87 % (4041077)------------------------------
% 138.25/19.87 % (4041077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.25/19.87 % (4041077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.25/19.87 % (4041077)CaDiCaL version: 2.1.3
% 138.25/19.87 % (4041077)Termination reason: Instruction limit
% 138.25/19.87 % (4041077)Termination phase: Saturation
% 138.25/19.87 % (4041077)Time elapsed: 1.318 s
% 138.25/19.87 % (4041077)Peak memory usage: 16 MB
% 138.25/19.87 % (4041077)Instructions burned: 1472 (million)
% 138.25/19.87 % (4041093)ott+11_1_sil=16000:gs=on:random_seed=1418616200:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi)
% 138.25/19.87 % (4041093)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 138.25/19.87 % (4041075)Instruction limit reached!
% 138.25/19.87 % (4041075)------------------------------
% 138.25/19.87 % (4041075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.25/19.87 % (4041075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.25/19.87 % (4041075)CaDiCaL version: 2.1.3
% 138.25/19.87 % (4041075)Termination reason: Instruction limit
% 138.25/19.87 % (4041075)Termination phase: Saturation
% 138.25/19.87 % (4041075)Time elapsed: 2.268 s
% 138.25/19.87 % (4041075)Peak memory usage: 30 MB
% 138.25/19.87 % (4041075)Instructions burned: 5133 (million)
% 138.25/19.87 % (4041095)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2644464866:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi)
% 138.25/19.87 % Exception at run slice level
% 138.25/19.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 138.25/19.87 % (4041097)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=267079613:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi)
% 138.25/19.87 % (4041089)Instruction limit reached!
% 138.25/19.87 % (4041089)------------------------------
% 138.25/19.87 % (4041089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.25/19.87 % (4041089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.25/19.87 % (4041089)CaDiCaL version: 2.1.3
% 138.25/19.87 % (4041089)Termination reason: Instruction limit
% 138.25/19.87 % (4041089)Termination phase: Saturation
% 138.25/19.87 % (4041089)Time elapsed: 2.863 s
% 138.25/19.87 % (4041089)Peak memory usage: 29 MB
% 138.25/19.87 % (4041089)Instructions burned: 3512 (million)
% 138.25/19.87 % (4041099)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3722951143:i=29340_2958 on theBenchmark for (2958ds/29340Mi)
% 138.25/19.87 % (4041093)Instruction limit reached!
% 138.25/19.87 % (4041093)------------------------------
% 138.25/19.87 % (4041093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.25/19.87 % (4041093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.25/19.87 % (4041093)CaDiCaL version: 2.1.3
% 138.25/19.87 % (4041093)Termination reason: Instruction limit
% 138.25/19.87 % (4041093)Termination phase: Saturation
% 138.25/19.87 % (4041093)Time elapsed: 2.006 s
% 138.25/19.87 % (4041093)Peak memory usage: 24 MB
% 138.25/19.87 % (4041093)Instructions burned: 2251 (million)
% 138.25/19.87 % (4041101)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2699589796:i=5211_2958 on theBenchmark for (2958ds/5211Mi)
% 150.06/21.57 % (4041091)Instruction limit reached!
% 150.06/21.57 % (4041091)------------------------------
% 150.06/21.57 % (4041091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.06/21.57 % (4041091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.06/21.57 % (4041091)CaDiCaL version: 2.1.3
% 150.06/21.57 % (4041091)Termination reason: Instruction limit
% 150.06/21.57 % (4041091)Termination phase: Saturation
% 150.06/21.57 % (4041091)Time elapsed: 3.109 s
% 150.06/21.57 % (4041091)Peak memory usage: 27 MB
% 150.06/21.57 % (4041091)Instructions burned: 3773 (million)
% 150.06/21.57 % (4041105)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1934895190:i=5497:nm=2_2951 on theBenchmark for (2951ds/5497Mi)
% 150.06/21.57 % Exception at run slice level
% 150.06/21.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.06/21.57 % (4041107)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3802107198:fmbsr=2:i=46332_2950 on theBenchmark for (2950ds/46332Mi)
% 150.06/21.57 % Exception at run slice level
% 150.06/21.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.06/21.57 % (4041109)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=21213789:i=14071_2949 on theBenchmark for (2949ds/14071Mi)
% 150.06/21.57 % Exception at run slice level
% 150.06/21.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.06/21.57 % (4041111)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2376904092:i=22565:add=on:rawr=on_2949 on theBenchmark for (2949ds/22565Mi)
% 150.06/21.57 % (4041097)Instruction limit reached!
% 150.06/21.57 % (4041097)------------------------------
% 150.06/21.57 % (4041097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.06/21.57 % (4041097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.06/21.57 % (4041097)CaDiCaL version: 2.1.3
% 150.06/21.57 % (4041097)Termination reason: Instruction limit
% 150.06/21.57 % (4041097)Termination phase: Saturation
% 150.06/21.57 % (4041097)Time elapsed: 1.959 s
% 150.06/21.57 % (4041097)Peak memory usage: 23 MB
% 150.06/21.57 % (4041097)Instructions burned: 4591 (million)
% 150.06/21.57 % (4041113)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3980917933:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi)
% 150.06/21.57 % (4041084)Instruction limit reached!
% 150.06/21.57 % (4041084)------------------------------
% 150.06/21.57 % (4041084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.06/21.57 % (4041084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.06/21.57 % (4041084)CaDiCaL version: 2.1.3
% 150.06/21.57 % (4041084)Termination reason: Instruction limit
% 150.06/21.57 % (4041084)Termination phase: Saturation
% 150.06/21.57 % (4041084)Time elapsed: 4.263 s
% 150.06/21.57 % (4041084)Peak memory usage: 31 MB
% 150.06/21.57 % (4041084)Instructions burned: 5115 (million)
% 150.06/21.57 % (4041115)dis+10_16:1_sil=16000:random_seed=611029021:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi)
% 150.06/21.57 % (4041101)Instruction limit reached!
% 150.06/21.57 % (4041101)------------------------------
% 150.06/21.57 % (4041101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.06/21.57 % (4041101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.06/21.57 % (4041101)CaDiCaL version: 2.1.3
% 150.06/21.57 % (4041101)Termination reason: Instruction limit
% 150.06/21.57 % (4041101)Termination phase: Saturation
% 150.06/21.57 % (4041101)Time elapsed: 4.563 s
% 150.06/21.57 % (4041101)Peak memory usage: 50 MB
% 150.06/21.57 % (4041101)Instructions burned: 5211 (million)
% 150.06/21.57 % (4041123)ott-3_8_sil=64000:random_seed=2529708785:i=20139:bs=on_2911 on theBenchmark for (2911ds/20139Mi)
% 150.06/21.57 % (4041113)Instruction limit reached!
% 150.06/21.57 % (4041113)------------------------------
% 150.06/21.57 % (4041113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.06/21.57 % (4041113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.06/21.57 % (4041113)CaDiCaL version: 2.1.3
% 150.06/21.57 % (4041113)Termination reason: Instruction limit
% 150.06/21.57 % (4041113)Termination phase: Saturation
% 150.06/21.57 % (4041113)Time elapsed: 7.161 s
% 150.06/21.57 % (4041113)Peak memory usage: 46 MB
% 150.06/21.57 % (4041113)Instructions burned: 8174 (million)
% 150.06/21.57 % (4041130)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=286565535:fmbsr=2:i=32576_2876 on theBenchmark for (2876ds/32576Mi)
% 156.04/22.33 % Exception at run slice level
% 156.04/22.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 156.04/22.33 % (4041136)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1631856347:i=11404_2876 on theBenchmark for (2876ds/11404Mi)
% 156.04/22.33 % (4041115)Instruction limit reached!
% 156.04/22.33 % (4041115)------------------------------
% 156.04/22.33 % (4041115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.04/22.33 % (4041115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.04/22.33 % (4041115)CaDiCaL version: 2.1.3
% 156.04/22.33 % (4041115)Termination reason: Instruction limit
% 156.04/22.33 % (4041115)Termination phase: Saturation
% 156.04/22.33 % (4041115)Time elapsed: 7.308 s
% 156.04/22.33 % (4041115)Peak memory usage: 47 MB
% 156.04/22.33 % (4041115)Instructions burned: 9157 (million)
% 156.04/22.33 % (4041185)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2342340797:i=14134_2874 on theBenchmark for (2874ds/14134Mi)
% 156.04/22.33 % (4041185)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 156.04/22.33 % (4041111)Instruction limit reached!
% 156.04/22.33 % (4041111)------------------------------
% 156.04/22.33 % (4041111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.04/22.33 % (4041111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.04/22.33 % (4041111)CaDiCaL version: 2.1.3
% 156.04/22.33 % (4041111)Termination reason: Instruction limit
% 156.04/22.33 % (4041111)Termination phase: Saturation
% 156.04/22.33 % (4041111)Time elapsed: 8.377 s
% 156.04/22.33 % (4041111)Peak memory usage: 67 MB
% 156.04/22.33 % (4041111)Instructions burned: 22566 (million)
% 156.04/22.33 % (4041289)dis+33_16_sil=32000:sac=on:random_seed=2780163604:i=15851:nm=0_2865 on theBenchmark for (2865ds/15851Mi)
% 156.04/22.33 % (4041289)Instruction limit reached!
% 156.04/22.33 % (4041289)------------------------------
% 156.04/22.33 % (4041289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.04/22.33 % (4041289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.04/22.33 % (4041289)CaDiCaL version: 2.1.3
% 156.04/22.33 % (4041289)Termination reason: Instruction limit
% 156.04/22.33 % (4041289)Termination phase: Saturation
% 156.04/22.33 % (4041289)Time elapsed: 3.955 s
% 156.04/22.33 % (4041289)Peak memory usage: 29 MB
% 156.04/22.33 % (4041289)Instructions burned: 15854 (million)
% 156.04/22.33 % (4041291)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=472080977:avsq=on:i=17627:add=on:amm=off_2825 on theBenchmark for (2825ds/17627Mi)
% 156.04/22.33 % (4041123)Instruction limit reached!
% 156.04/22.33 % (4041123)------------------------------
% 156.04/22.33 % (4041123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.04/22.33 % (4041123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.04/22.33 % (4041123)CaDiCaL version: 2.1.3
% 156.04/22.33 % (4041123)Termination reason: Instruction limit
% 156.04/22.33 % (4041123)Termination phase: Saturation
% 156.04/22.33 % (4041123)Time elapsed: 9.263 s
% 156.04/22.33 % (4041123)Peak memory usage: 31 MB
% 156.04/22.33 % (4041123)Instructions burned: 20139 (million)
% 156.04/22.33 % (4041293)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3669509132:s2a=on:i=53295_2819 on theBenchmark for (2819ds/53295Mi)
% 156.04/22.33 % (4041136)Instruction limit reached!
% 156.04/22.33 % (4041136)------------------------------
% 156.04/22.33 % (4041136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.04/22.33 % (4041136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.04/22.33 % (4041136)CaDiCaL version: 2.1.3
% 156.04/22.33 % (4041136)Termination reason: Instruction limit
% 156.04/22.33 % (4041136)Termination phase: Saturation
% 156.04/22.33 % (4041136)Time elapsed: 5.790 s
% 156.04/22.33 % (4041136)Peak memory usage: 62 MB
% 156.04/22.33 % (4041136)Instructions burned: 11405 (million)
% 156.04/22.33 % (4041295)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3961637787:i=26857:ins=20_2818 on theBenchmark for (2818ds/26857Mi)
% 156.04/22.33 % Exception at run slice level
% 156.04/22.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 156.04/22.33 % (4041297)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1616877960:i=28120:bs=on:fsr=off_2817 on theBenchmark for (2817ds/28120Mi)
% 156.04/22.33 % (4041185)Instruction limit reached!
% 156.04/22.33 % (4041185)------------------------------
% 156.04/22.33 % (4041185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.31/23.89 % (4041185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.31/23.89 % (4041185)CaDiCaL version: 2.1.3
% 166.31/23.89 % (4041185)Termination reason: Instruction limit
% 166.31/23.89 % (4041185)Termination phase: Saturation
% 166.31/23.89 % (4041185)Time elapsed: 6.927 s
% 166.31/23.89 % (4041185)Peak memory usage: 73 MB
% 166.31/23.89 % (4041185)Instructions burned: 14135 (million)
% 166.31/23.89 % (4041299)fmb+10_1_sil=256000:fmbss=7:random_seed=483385447:fmbsr=1.6:i=182295_2804 on theBenchmark for (2804ds/182295Mi)
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041301)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1282739699:i=44625:gsp=on_2803 on theBenchmark for (2803ds/44625Mi)
% 166.31/23.89 % (4041301)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 166.31/23.89 % (4041301)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041303)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1028970836:i=160505_2803 on theBenchmark for (2803ds/160505Mi)
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041305)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3196994367:fmbsr=1.3:i=225729_2802 on theBenchmark for (2802ds/225729Mi)
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041307)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1375755860:fmbsr=2:i=185024:ins=7_2802 on theBenchmark for (2802ds/185024Mi)
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041309)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3946730400:rtra=on_2801 on theBenchmark for (2801ds/0Mi)
% 166.31/23.89 % Exception at run slice level
% 166.31/23.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.31/23.89 % (4041311)% WARNING: option uhcvi not known.
% 166.31/23.89 % (4041311)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=555023252:i=271062:add=off:rtra=on:rawr=on_2801 on theBenchmark for (2801ds/271062Mi)
% 166.31/23.89 % (4041311)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 166.31/23.89 % (4041311)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 166.31/23.89 % (4041099)Instruction limit reached!
% 166.31/23.89 % (4041099)------------------------------
% 166.31/23.89 % (4041099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.31/23.89 % (4041099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.31/23.89 % (4041099)CaDiCaL version: 2.1.3
% 166.31/23.89 % (4041099)Termination reason: Instruction limit
% 166.31/23.89 % (4041099)Termination phase: Saturation
% 166.31/23.89 % (4041099)Time elapsed: 16.693 s
% 166.31/23.89 % (4041099)Peak memory usage: 363 MB
% 166.31/23.89 % (4041099)Instructions burned: 29340 (million)
% 166.31/23.89 % (4041313)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3281755344:i=176048:add=on:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/176048Mi)
% 166.31/23.89 % (4041291)Instruction limit reached!
% 166.31/23.89 % (4041291)------------------------------
% 166.31/23.89 % (4041291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.31/23.89 % (4041291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.31/23.89 % (4041291)CaDiCaL version: 2.1.3
% 166.31/23.89 % (4041291)Termination reason: Instruction limit
% 166.31/23.89 % (4041291)Termination phase: Saturation
% 166.31/23.89 % (4041291)Time elapsed: 3.682 s
% 166.31/23.89 % (4041291)Peak memory usage: 80 MB
% 166.31/23.89 % (4041291)Instructions burned: 17632 (million)
% 166.31/23.89 % (4041315)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3620101877:i=206:fgj=on:rtra=on_2788 on theBenchmark for (2788ds/206Mi)
% 166.31/23.89 % (4041315)Instruction limit reached!
% 166.31/23.89 % (4041315)------------------------------
% 200.30/28.62 % (4041315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.30/28.62 % (4041315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.30/28.62 % (4041315)CaDiCaL version: 2.1.3
% 200.30/28.62 % (4041315)Termination reason: Instruction limit
% 200.30/28.62 % (4041315)Termination phase: Saturation
% 200.30/28.62 % (4041315)Time elapsed: 0.058 s
% 200.30/28.62 % (4041315)Peak memory usage: 14 MB
% 200.30/28.62 % (4041315)Instructions burned: 206 (million)
% 200.30/28.62 % (4041317)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=184576965:i=232:rtra=on_2787 on theBenchmark for (2787ds/232Mi)
% 200.30/28.62 % (4041317)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 200.30/28.62 % (4041317)Instruction limit reached!
% 200.30/28.62 % (4041317)------------------------------
% 200.30/28.62 % (4041317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.30/28.62 % (4041317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.30/28.62 % (4041317)CaDiCaL version: 2.1.3
% 200.30/28.62 % (4041317)Termination reason: Instruction limit
% 200.30/28.62 % (4041317)Termination phase: Saturation
% 200.30/28.62 % (4041317)Time elapsed: 0.063 s
% 200.30/28.62 % (4041317)Peak memory usage: 14 MB
% 200.30/28.62 % (4041317)Instructions burned: 234 (million)
% 200.30/28.62 % (4041319)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1355399019:i=262:rtra=on_2786 on theBenchmark for (2786ds/262Mi)
% 200.30/28.62 % (4041319)Instruction limit reached!
% 200.30/28.62 % (4041319)------------------------------
% 200.30/28.62 % (4041319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.30/28.62 % (4041319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.30/28.62 % (4041319)CaDiCaL version: 2.1.3
% 200.30/28.62 % (4041319)Termination reason: Instruction limit
% 200.30/28.62 % (4041319)Termination phase: Saturation
% 200.30/28.62 % (4041319)Time elapsed: 0.075 s
% 200.30/28.62 % (4041319)Peak memory usage: 15 MB
% 200.30/28.62 % (4041319)Instructions burned: 265 (million)
% 200.30/28.62 % (4041321)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2730435462:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2785 on theBenchmark for (2785ds/318Mi)
% 200.30/28.62 % (4041321)Instruction limit reached!
% 200.30/28.62 % (4041321)------------------------------
% 200.30/28.62 % (4041321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.30/28.62 % (4041321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.30/28.62 % (4041321)CaDiCaL version: 2.1.3
% 200.30/28.62 % (4041321)Termination reason: Instruction limit
% 200.30/28.62 % (4041321)Termination phase: Saturation
% 200.30/28.62 % (4041321)Time elapsed: 0.095 s
% 200.30/28.62 % (4041321)Peak memory usage: 15 MB
% 200.30/28.62 % (4041321)Instructions burned: 320 (million)
% 200.30/28.62 % (4041323)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=636226694:i=1428:nm=2:rtra=on_2784 on theBenchmark for (2784ds/1428Mi)
% 200.30/28.62 % Exception at run slice level
% 200.30/28.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 200.30/28.62 % (4041325)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3243263877:i=262:bd=preordered:rtra=on:fsd=on_2784 on theBenchmark for (2784ds/262Mi)
% 200.30/28.62 % (4041325)Instruction limit reached!
% 200.30/28.62 % (4041325)------------------------------
% 200.30/28.62 % (4041325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.30/28.62 % (4041325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.30/28.62 % (4041325)CaDiCaL version: 2.1.3
% 200.30/28.62 % (4041325)Termination reason: Instruction limit
% 200.30/28.62 % (4041325)Termination phase: Saturation
% 200.30/28.62 % (4041325)Time elapsed: 0.075 s
% 200.30/28.62 % (4041325)Peak memory usage: 14 MB
% 200.30/28.62 % (4041325)Instructions burned: 264 (million)
% 200.30/28.62 % (4041327)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=2600795536:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/1368Mi)
% 200.30/28.62 % (4041327)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 200.30/28.62 % (4041327)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 200.30/28.62 % (4041327)Instruction limit reached!
% 200.30/28.62 % (4041327)------------------------------
% 200.30/28.62 % (4041327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.26/33.57 % (4041327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.26/33.57 % (4041327)CaDiCaL version: 2.1.3
% 235.26/33.57 % (4041327)Termination reason: Instruction limit
% 235.26/33.57 % (4041327)Termination phase: Saturation
% 235.26/33.57 % (4041327)Time elapsed: 0.365 s
% 235.26/33.57 % (4041327)Peak memory usage: 17 MB
% 235.26/33.57 % (4041327)Instructions burned: 1370 (million)
% 235.26/33.57 % (4041329)ott-21_1_sil=16000:si=on:fs=off:random_seed=3672569958:i=360:av=off:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/360Mi)
% 235.26/33.57 % (4041329)Instruction limit reached!
% 235.26/33.57 % (4041329)------------------------------
% 235.26/33.57 % (4041329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.26/33.57 % (4041329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.26/33.57 % (4041329)CaDiCaL version: 2.1.3
% 235.26/33.57 % (4041329)Termination reason: Instruction limit
% 235.26/33.57 % (4041329)Termination phase: Saturation
% 235.26/33.57 % (4041329)Time elapsed: 0.095 s
% 235.26/33.57 % (4041329)Peak memory usage: 14 MB
% 235.26/33.57 % (4041329)Instructions burned: 361 (million)
% 235.26/33.57 % (4041331)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3481054625:i=954:bd=all:rtra=on_2778 on theBenchmark for (2778ds/954Mi)
% 235.26/33.57 % (4041331)Instruction limit reached!
% 235.26/33.57 % (4041331)------------------------------
% 235.26/33.57 % (4041331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.26/33.57 % (4041331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.26/33.57 % (4041331)CaDiCaL version: 2.1.3
% 235.26/33.57 % (4041331)Termination reason: Instruction limit
% 235.26/33.57 % (4041331)Termination phase: Saturation
% 235.26/33.57 % (4041331)Time elapsed: 0.279 s
% 235.26/33.57 % (4041331)Peak memory usage: 17 MB
% 235.26/33.57 % (4041331)Instructions burned: 955 (million)
% 235.26/33.57 % (4041333)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3028169517:fmbsr=1.3:i=1730:ins=25:rtra=on_2775 on theBenchmark for (2775ds/1730Mi)
% 235.26/33.57 % Exception at run slice level
% 235.26/33.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 235.26/33.57 % (4041335)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2837168079:i=2358:rtra=on_2775 on theBenchmark for (2775ds/2358Mi)
% 235.26/33.57 % (4041335)Instruction limit reached!
% 235.26/33.57 % (4041335)------------------------------
% 235.26/33.57 % (4041335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.26/33.57 % (4041335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.26/33.57 % (4041335)CaDiCaL version: 2.1.3
% 235.26/33.57 % (4041335)Termination reason: Instruction limit
% 235.26/33.57 % (4041335)Termination phase: Saturation
% 235.26/33.57 % (4041335)Time elapsed: 0.648 s
% 235.26/33.57 % (4041335)Peak memory usage: 28 MB
% 235.26/33.57 % (4041335)Instructions burned: 2361 (million)
% 235.26/33.57 % (4041337)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2388741176:i=1778:ins=1:rtra=on_2769 on theBenchmark for (2769ds/1778Mi)
% 235.26/33.57 % Exception at run slice level
% 235.26/33.57 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 235.26/33.57 % (4041339)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=1919778077:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2768 on theBenchmark for (2768ds/1384Mi)
% 235.26/33.57 % (4041339)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 235.26/33.57 % (4041339)Instruction limit reached!
% 235.26/33.57 % (4041339)------------------------------
% 235.26/33.57 % (4041339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.26/33.57 % (4041339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.26/33.57 % (4041339)CaDiCaL version: 2.1.3
% 235.26/33.57 % (4041339)Termination reason: Instruction limit
% 235.26/33.57 % (4041339)Termination phase: Saturation
% 235.26/33.57 % (4041339)Time elapsed: 0.407 s
% 235.26/33.57 % (4041339)Peak memory usage: 23 MB
% 235.26/33.57 % (4041339)Instructions burned: 1385 (million)
% 235.26/33.57 % (4041341)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1378499321:i=1758:kws=inv_precedence:fsr=off:rtra=on_2764 on theBenchmark for (2764ds/1758Mi)
% 235.26/33.57 % (4041341)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 128.05/33.94 % (4041341)Instruction limit reached!
% 128.05/33.94 % (4041341)------------------------------
% 128.05/33.94 % (4041341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.94 % (4041341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.94 % (4041341)CaDiCaL version: 2.1.3
% 128.05/33.94 % (4041341)Termination reason: Instruction limit
% 128.05/33.94 % (4041341)Termination phase: Saturation
% 128.05/33.94 % (4041341)Time elapsed: 0.486 s
% 128.05/33.94 % (4041341)Peak memory usage: 25 MB
% 128.05/33.94 % (4041341)Instructions burned: 1758 (million)
% 128.05/33.94 % (4041343)fmb+10_1_sil=64000:si=on:random_seed=3621077694:i=44122:nm=2:rtra=on:gsp=on_2759 on theBenchmark for (2759ds/44122Mi)
% 128.05/33.94 % (4041343)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 128.05/33.94 % Exception at run slice level
% 128.05/33.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.94 % (4041345)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=731238922:i=19030:nm=5:rtra=on_2759 on theBenchmark for (2759ds/19030Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041347)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1262589635:fmbsr=1.7:i=1840:rtra=on_2758 on theBenchmark for (2758ds/1840Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041349)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1262939926:i=10262:rtra=on_2758 on theBenchmark for (2758ds/10262Mi)
% 128.05/33.96 % (4041349)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 128.05/33.96 % (4041349)Instruction limit reached!
% 128.05/33.96 % (4041349)------------------------------
% 128.05/33.96 % (4041349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041349)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041349)Termination reason: Instruction limit
% 128.05/33.96 % (4041349)Termination phase: Saturation
% 128.05/33.96 % (4041349)Time elapsed: 2.782 s
% 128.05/33.96 % (4041349)Peak memory usage: 42 MB
% 128.05/33.96 % (4041349)Instructions burned: 10262 (million)
% 128.05/33.96 % (4041351)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3700960110:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2730 on theBenchmark for (2730ds/2944Mi)
% 128.05/33.96 % (4041351)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 128.05/33.96 % (4041351)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 128.05/33.96 % (4041351)Instruction limit reached!
% 128.05/33.96 % (4041351)------------------------------
% 128.05/33.96 % (4041351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041351)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041351)Termination reason: Instruction limit
% 128.05/33.96 % (4041351)Termination phase: Saturation
% 128.05/33.96 % (4041351)Time elapsed: 0.794 s
% 128.05/33.96 % (4041351)Peak memory usage: 19 MB
% 128.05/33.96 % (4041351)Instructions burned: 2946 (million)
% 128.05/33.96 % (4041353)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3179992416:i=12648:rtra=on_2722 on theBenchmark for (2722ds/12648Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041355)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3434757908:fmbsr=2.30978:i=4348:rtra=on_2722 on theBenchmark for (2722ds/4348Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041357)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3811196777:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2721 on theBenchmark for (2721ds/1738Mi)
% 128.05/33.96 % (4041357)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 128.05/33.96 % (4041357)Instruction limit reached!
% 128.05/33.96 % (4041357)------------------------------
% 128.05/33.96 % (4041357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041357)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041357)Termination reason: Instruction limit
% 128.05/33.96 % (4041357)Termination phase: Saturation
% 128.05/33.96 % (4041357)Time elapsed: 0.463 s
% 128.05/33.96 % (4041357)Peak memory usage: 17 MB
% 128.05/33.96 % (4041357)Instructions burned: 1738 (million)
% 128.05/33.96 % (4041407)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4210599850:i=10228:av=off:rtra=on_2717 on theBenchmark for (2717ds/10228Mi)
% 128.05/33.96 % (4041297)Instruction limit reached!
% 128.05/33.96 % (4041297)------------------------------
% 128.05/33.96 % (4041297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041297)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041297)Termination reason: Instruction limit
% 128.05/33.96 % (4041297)Termination phase: Saturation
% 128.05/33.96 % (4041297)Time elapsed: 10.999 s
% 128.05/33.96 % (4041297)Peak memory usage: 64 MB
% 128.05/33.96 % (4041297)Instructions burned: 28122 (million)
% 128.05/33.96 % (4041477)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3684667628:i=108564:rtra=on_2707 on theBenchmark for (2707ds/108564Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041479)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1253204655:i=7024:aac=none:rtra=on_2706 on theBenchmark for (2706ds/7024Mi)
% 128.05/33.96 % (4041479)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 128.05/33.96 % (4041407)Instruction limit reached!
% 128.05/33.96 % (4041407)------------------------------
% 128.05/33.96 % (4041407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041407)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041407)Termination reason: Instruction limit
% 128.05/33.96 % (4041407)Termination phase: Saturation
% 128.05/33.96 % (4041407)Time elapsed: 2.903 s
% 128.05/33.96 % (4041407)Peak memory usage: 45 MB
% 128.05/33.96 % (4041407)Instructions burned: 10232 (million)
% 128.05/33.96 % (4041777)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2519897802:i=7546:rtra=on:amm=off_2687 on theBenchmark for (2687ds/7546Mi)
% 128.05/33.96 % (4041479)Instruction limit reached!
% 128.05/33.96 % (4041479)------------------------------
% 128.05/33.96 % (4041479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041479)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041479)Termination reason: Instruction limit
% 128.05/33.96 % (4041479)Termination phase: Saturation
% 128.05/33.96 % (4041479)Time elapsed: 3.544 s
% 128.05/33.96 % (4041479)Peak memory usage: 44 MB
% 128.05/33.96 % (4041479)Instructions burned: 7024 (million)
% 128.05/33.96 % (4041826)ott+11_1_sil=16000:si=on:gs=on:random_seed=2774841823:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2671 on theBenchmark for (2671ds/4502Mi)
% 128.05/33.96 % (4041826)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 128.05/33.96 % (4041777)Instruction limit reached!
% 128.05/33.96 % (4041777)------------------------------
% 128.05/33.96 % (4041777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041777)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041777)Termination reason: Instruction limit
% 128.05/33.96 % (4041777)Termination phase: Saturation
% 128.05/33.96 % (4041777)Time elapsed: 1.981 s
% 128.05/33.96 % (4041777)Peak memory usage: 38 MB
% 128.05/33.96 % (4041777)Instructions burned: 7547 (million)
% 128.05/33.96 % (4041828)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3172150012:fmbsr=1.6:i=135068:rtra=on_2667 on theBenchmark for (2667ds/135068Mi)
% 128.05/33.96 % Exception at run slice level
% 128.05/33.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.05/33.96 % (4041830)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1699399371:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2667 on theBenchmark for (2667ds/9182Mi)
% 128.05/33.96 % (4041826) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4041028-4041826"...
% 128.05/33.96 % (4041826)...printing done.
% 128.05/33.96 % (4041826)Refutation found. Thanks to Tanya!
% 128.05/33.96 % SZS status Theorem for theBenchmark
% 128.05/33.96 % SZS output start Proof for theBenchmark
% 128.05/33.96 thf(type_def_5, type, set: $tType > $tType).
% 128.05/33.96 thf(type_def_6, type, nat: $tType).
% 128.05/33.96 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 128.05/33.96 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_1, type, one: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_2, type, zero: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_3, type, ord: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_4, type, neg_numeral: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_5, type, order: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_6, type, group_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_7, type, finite_finite: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_8, type, monoid_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_9, type, linorder: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_10, type, preorder: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_11, type, zero_neq_one: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_12, type, wellorder: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_13, type, semigroup_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_14, type, linordered_idom: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_15, type, comm_monoid_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_16, type, ab_semigroup_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_17, type, dense_linorder: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_18, type, cancel_semigroup_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_19, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_20, type, linord219039673up_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_21, type, ordere216010020id_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_22, type, ordere779506340up_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_23, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_24, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_25, type, strict797366125id_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_26, type, ordere236663937imp_le: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_27, type, ordere223160158up_add: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_28, type, ordere516151231imp_le: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_29, type, semiri456707255roduct: !>[X0: $tType]:($o)).
% 128.05/33.96 thf(func_def_30, type, finite_Fpow: !>[X0: $tType]:((set @ X0 > set @ set @ X0))).
% 128.05/33.96 thf(func_def_31, type, finite_finite2: !>[X0: $tType]:((set @ X0 > $o))).
% 128.05/33.96 thf(func_def_32, type, one_one: !>[X0: $tType]:(X0)).
% 128.05/33.96 thf(func_def_33, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_34, type, zero_zero: !>[X0: $tType]:(X0)).
% 128.05/33.96 thf(func_def_35, type, neg_numeral_dbl_inc: !>[X0: $tType]:((X0 > X0))).
% 128.05/33.96 thf(func_def_36, type, number2016821345itions: ((nat > nat) > nat > $o)).
% 128.05/33.96 thf(func_def_37, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_38, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_39, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 128.05/33.96 thf(func_def_40, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 128.05/33.96 thf(func_def_41, type, n: nat).
% 128.05/33.96 thf(func_def_45, type, vNOT: ($o > $o)).
% 128.05/33.96 thf(func_def_46, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_47, type, vAND: ($o > $o > $o)).
% 128.05/33.96 thf(func_def_48, type, db0: !>[X0: $tType]:(X0)).
% 128.05/33.96 thf(func_def_49, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 128.05/33.96 thf(func_def_50, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 128.05/33.96 thf(func_def_51, type, db1: !>[X0: $tType]:(X0)).
% 128.05/33.96 thf(func_def_52, type, vIMP: ($o > $o > $o)).
% 128.05/33.96 thf(func_def_53, type, db2: !>[X0: $tType]:(X0)).
% 128.05/33.96 thf(func_def_54, type, vOR: ($o > $o > $o)).
% 128.05/33.96 thf(func_def_55, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 128.05/33.96 thf(func_def_56, type, sP0: !>[X0: $tType]:((set @ X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_57, type, sP1: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > set @ X0 > $o))).
% 128.05/33.96 thf(func_def_58, type, sP2: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_59, type, sP3: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_60, type, sP4: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_61, type, sP5: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_62, type, sP6: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_63, type, sP7: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_64, type, sP8: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_65, type, sP9: !>[X0: $tType]:(((X0 > X0 > $o) > $o))).
% 128.05/33.96 thf(func_def_66, type, sP10: (nat > (nat > $o) > $o)).
% 128.05/33.96 thf(func_def_67, type, sP11: !>[X0: $tType]:((set @ X0 > X0 > $o))).
% 128.05/33.96 thf(func_def_68, type, sP12: !>[X0: $tType, X1: $tType]:((set @ X1 > (X0 > X1 > $o) > set @ X0 > $o))).
% 128.05/33.96 thf(func_def_69, type, sP13: ((nat > $o) > nat > $o)).
% 128.05/33.96 thf(func_def_70, type, sK14: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_71, type, sK15: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_72, type, sK16: !>[X0: $tType]:((set @ X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_73, type, sK17: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_74, type, sK18: ((nat > nat) > nat)).
% 128.05/33.96 thf(func_def_75, type, sK19: ((nat > nat) > nat)).
% 128.05/33.96 thf(func_def_76, type, sK20: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > set @ X0 > X0))).
% 128.05/33.96 thf(func_def_77, type, sK21: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_78, type, sK22: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_79, type, sK23: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_80, type, sK24: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_81, type, sK25: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_82, type, sK26: !>[X0: $tType]:((X0 > X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_83, type, sK27: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_84, type, sK28: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_85, type, sK29: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 128.05/33.96 thf(func_def_86, type, sK30: !>[X0: $tType]:((X0 > X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_87, type, sK31: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_88, type, sK32: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_89, type, sK33: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_90, type, sK34: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_91, type, sK35: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_92, type, sK36: !>[X0: $tType]:((X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_93, type, sK37: ((nat > nat > $o) > nat)).
% 128.05/33.96 thf(func_def_94, type, sK38: ((nat > nat > $o) > nat)).
% 128.05/33.96 thf(func_def_95, type, sK39: ((nat > nat > $o) > nat)).
% 128.05/33.96 thf(func_def_96, type, sK40: ((nat > nat > $o) > nat)).
% 128.05/33.96 thf(func_def_97, type, sK41: ((nat > nat > $o) > nat)).
% 128.05/33.96 thf(func_def_98, type, sK42: !>[X0: $tType]:((X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_99, type, sK43: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_100, type, sK44: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_101, type, sK45: (nat > (nat > $o) > nat)).
% 128.05/33.96 thf(func_def_102, type, sK46: ((nat > $o) > nat)).
% 128.05/33.96 thf(func_def_103, type, sK47: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_104, type, sK48: !>[X0: $tType]:((set @ X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_105, type, sK49: !>[X0: $tType, X1: $tType]:((set @ X1 > (X0 > X1 > $o) > set @ X0 > X1))).
% 128.05/33.96 thf(func_def_106, type, sK50: !>[X0: $tType, X1: $tType]:((set @ X0 > set @ X1 > (X0 > X1 > $o) > X0))).
% 128.05/33.96 thf(func_def_107, type, sK51: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_108, type, sK52: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_109, type, sK53: (nat > set @ nat > nat)).
% 128.05/33.96 thf(func_def_110, type, sK54: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 128.05/33.96 thf(func_def_111, type, sK55: (nat > nat > nat)).
% 128.05/33.96 thf(func_def_112, type, sK56: ((nat > $o) > nat > nat)).
% 128.05/33.96 thf(func_def_113, type, sK57: ((nat > $o) > nat)).
% 128.05/33.96 thf(func_def_114, type, sK58: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_115, type, sK59: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_116, type, sK60: !>[X0: $tType]:((X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_117, type, sK61: ((nat > nat) > nat)).
% 128.05/33.96 thf(func_def_118, type, sK62: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_119, type, sK63: !>[X0: $tType]:((X0 > X0 > X0))).
% 128.05/33.96 thf(func_def_120, type, sK64: !>[X0: $tType, X1: $tType]:((set @ X0 > (X0 > X1 > $o) > X0))).
% 128.05/33.96 thf(func_def_121, type, sK65: !>[X0: $tType, X1: $tType]:((set @ X0 > (X0 > X1 > $o) > X0 > X1))).
% 128.05/33.96 thf(func_def_122, type, sK66: !>[X0: $tType]:(((X0 > $o) > X0))).
% 128.05/33.96 thf(func_def_123, type, sK67: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_124, type, sK68: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 128.05/33.96 thf(func_def_125, type, sK69: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 128.05/33.96 thf(func_def_126, type, sK70: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 128.05/33.96 thf(f1,axiom,(
% 128.05/33.96 (finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[X1 : (nat > nat)] : (! [X2 : nat] : (ord_less_eq @ nat @ (X1 @ X2) @ n) & ! [X2 : nat] : ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ X2) => (((X1 @ X2)) = zero_zero @ nat))))))),
% 128.05/33.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062finite_A_123f_O_A_I_092_060forall_062i_O_Af_Ai_A_092_060le_062_An_J_A_092_060and_062_A_I_092_060forall_062i_092_060ge_062n_A_L_A1_O_Af_Ai_A_061_A0_J_125_092_060close_062)).
% 128.05/33.96 thf(f2,axiom,(
% 128.05/33.96 (ord_less_eq @ set @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : ((number2016821345itions @ X0 @ n)))) @ (collect @ (nat > nat) @ (^[X1 : (nat > nat)] : (! [X2 : nat] : (ord_less_eq @ nat @ (X1 @ X2) @ n) & ! [X2 : nat] : ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ X2) => (((X1 @ X2)) = zero_zero @ nat))))))),
% 128.05/33.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062_123p_O_Ap_Apartitions_An_125_A_092_060subseteq_062_A_123f_O_A_I_092_060forall_062i_O_Af_Ai_A_092_060le_062_An_J_A_092_060and_062_A_I_092_060forall_062i_092_060ge_062n_A_L_A1_O_Af_Ai_A_061_A0_J_125_092_060close_062)).
% 128.05/33.96 thf(f19,axiom,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : ((ord_less_eq @ set @ X0 @ X1 @ X2) => (~(finite_finite2 @ X0 @ X1) => ~(finite_finite2 @ X0 @ X2)))),
% 128.05/33.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_infinite__super)).
% 128.05/33.96 thf(f290,conjecture,(
% 128.05/33.96 (finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : ((number2016821345itions @ X0 @ n)))))),
% 128.05/33.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 128.05/33.96 thf(f291,negated_conjecture,(
% 128.05/33.96 ~(finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : ((number2016821345itions @ X0 @ n)))))),
% 128.05/33.96 inference(negated_conjecture,[status(cth)],[f290])).
% 128.05/33.96 thf(f424,plain,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : ((ord_less_eq @ set @ X0 @ X1 @ X2) => (~(finite_finite2 @ X0 @ X1) => ~(finite_finite2 @ X0 @ X2)))),
% 128.05/33.96 inference(rectify,[],[f19])).
% 128.05/33.96 thf(f425,plain,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : ((((ord_less_eq @ set @ X0 @ X1 @ X2)) = $true) => (~ (((finite_finite2 @ X0 @ X1)) = $true) => ~ (((finite_finite2 @ X0 @ X2)) = $true)))),
% 128.05/33.96 inference(fool_elimination,[],[f424])).
% 128.05/33.96 thf(f530,plain,(
% 128.05/33.96 (finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : (! [X1 : nat] : (ord_less_eq @ nat @ (X0 @ X1) @ n) & ! [X2 : nat] : ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ X2) => (zero_zero @ nat = ((X0 @ X2))))))))),
% 128.05/33.96 inference(rectify,[],[f1])).
% 128.05/33.96 thf(f531,plain,(
% 128.05/33.96 (((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) = $true)),
% 128.05/33.96 inference(fool_elimination,[],[f530])).
% 128.05/33.96 thf(f534,plain,(
% 128.05/33.96 ~(finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : ((number2016821345itions @ X0 @ n)))))),
% 128.05/33.96 inference(rectify,[],[f291])).
% 128.05/33.96 thf(f535,plain,(
% 128.05/33.96 ~ ($true = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(fool_elimination,[],[f534])).
% 128.05/33.96 thf(f556,plain,(
% 128.05/33.96 (ord_less_eq @ set @ (nat > nat) @ (collect @ (nat > nat) @ (^[X0 : (nat > nat)] : ((number2016821345itions @ X0 @ n)))) @ (collect @ (nat > nat) @ (^[X1 : (nat > nat)] : (! [X2 : nat] : (ord_less_eq @ nat @ (X1 @ X2) @ n) & ! [X3 : nat] : ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ X3) => (zero_zero @ nat = ((X1 @ X3))))))))),
% 128.05/33.96 inference(rectify,[],[f2])).
% 128.05/33.96 thf(f557,plain,(
% 128.05/33.96 (((ord_less_eq @ set @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) = $true)),
% 128.05/33.96 inference(fool_elimination,[],[f556])).
% 128.05/33.96 thf(f858,plain,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : ((((ord_less_eq @ set @ X0 @ X1 @ X2)) = $true) => ((((finite_finite2 @ X0 @ X1)) != $true) => (((finite_finite2 @ X0 @ X2)) != $true)))),
% 128.05/33.96 inference(flattening,[],[f425])).
% 128.05/33.96 thf(f862,plain,(
% 128.05/33.96 ($true != ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(flattening,[],[f535])).
% 128.05/33.96 thf(f1149,plain,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : (((((finite_finite2 @ X0 @ X2)) != $true) | (((finite_finite2 @ X0 @ X1)) = $true)) | (((ord_less_eq @ set @ X0 @ X1 @ X2)) != $true))),
% 128.05/33.96 inference(ennf_transformation,[],[f858])).
% 128.05/33.96 thf(f1150,plain,(
% 128.05/33.96 ! [X0 : $tType,X2 : set @ X0,X1 : set @ X0] : ((((finite_finite2 @ X0 @ X2)) != $true) | (((finite_finite2 @ X0 @ X1)) = $true) | (((ord_less_eq @ set @ X0 @ X1 @ X2)) != $true))),
% 128.05/33.96 inference(flattening,[],[f1149])).
% 128.05/33.96 thf(f1342,plain,(
% 128.05/33.96 ! [X0 : $tType,X1 : set @ X0,X2 : set @ X0] : ((((finite_finite2 @ X0 @ X1)) != $true) | (((finite_finite2 @ X0 @ X2)) = $true) | (((ord_less_eq @ set @ X0 @ X2 @ X1)) != $true))),
% 128.05/33.96 inference(rectify,[],[f1150])).
% 128.05/33.96 thf(f1459,plain,(
% 128.05/33.96 (((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) = $true)),
% 128.05/33.96 inference(cnf_transformation,[],[f531])).
% 128.05/33.96 thf(f1533,plain,(
% 128.05/33.96 ($true != ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(cnf_transformation,[],[f862])).
% 128.05/33.96 thf(f1648,plain,(
% 128.05/33.96 (((ord_less_eq @ set @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) = $true)),
% 128.05/33.96 inference(cnf_transformation,[],[f557])).
% 128.05/33.96 thf(f1661,plain,(
% 128.05/33.96 ( ! [X0 : $tType,X2 : set @ X0,X1 : set @ X0] : ((((ord_less_eq @ set @ X0 @ X2 @ X1)) != $true) | (((finite_finite2 @ X0 @ X2)) = $true) | (((finite_finite2 @ X0 @ X1)) != $true)) )),
% 128.05/33.96 inference(cnf_transformation,[],[f1342])).
% 128.05/33.96 thf(f1732,definition,(
% 128.05/33.96 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 128.05/33.96 introduced(theory,[fool_exhaustiveness_axiom])).
% 128.05/33.96 thf(f2627,plain,(
% 128.05/33.96 ($false = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n)))))) | ($true != $true)),
% 128.05/33.96 inference(constrained_superposition,[],[f1533,f1732])).
% 128.05/33.96 thf(f2655,plain,(
% 128.05/33.96 ($false = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(trivial_inequality_removal,[],[f2627])).
% 128.05/33.96 thf(f6198,plain,(
% 128.05/33.96 ($true = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n)))))) | (((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) != $true) | ($true != $true)),
% 128.05/33.96 inference(constrained_superposition,[],[f1661,f1648])).
% 128.05/33.96 thf(f6216,plain,(
% 128.05/33.96 (((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: ((!! @ nat @ (^[Y1 : nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ n @ one_one @ nat) @ Y1) => (zero_zero @ nat = (Y0 @ Y1))))) & (!! @ nat @ (^[Y1 : nat]: (ord_less_eq @ nat @ (Y0 @ Y1) @ n)))))))) != $true) | ($true = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(trivial_inequality_removal,[],[f6198])).
% 128.05/33.96 thf(f6235,plain,(
% 128.05/33.96 ($true = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n)))))) | ($true != $true)),
% 128.05/33.96 inference(forward_demodulation,[],[f6216,f1459])).
% 128.05/33.96 thf(f6236,plain,(
% 128.05/33.96 ($true = ((finite_finite2 @ (nat > nat) @ (collect @ (nat > nat) @ (^[Y0 : nat > nat]: (number2016821345itions @ Y0 @ n))))))),
% 128.05/33.96 inference(trivial_inequality_removal,[],[f6235])).
% 128.05/33.96 thf(f6237,plain,(
% 128.05/33.96 ($false = $true)),
% 128.05/33.96 inference(forward_demodulation,[],[f6236,f2655])).
% 128.05/33.96 thf(f6238,plain,(
% 128.05/33.96 $false),
% 128.05/33.96 inference(trivial_inequality_removal,[],[f6237])).
% 128.05/33.96 % SZS output end Proof for theBenchmark
% 128.05/33.96 % (4041826)------------------------------
% 128.05/33.96 % (4041826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.05/33.96 % (4041826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.05/33.96 % (4041826)CaDiCaL version: 2.1.3
% 128.05/33.96 % (4041826)Termination reason: Refutation
% 128.05/33.96 % (4041826)Time elapsed: 0.655 s
% 128.05/33.96 % (4041826)Peak memory usage: 20 MB
% 128.05/33.96 % (4041826)Instructions burned: 1229 (million)
% 128.05/33.96 % (4041028)Success in time 33.633 s
% 128.05/33.96 % Vampire exiting
%------------------------------------------------------------------------------