%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP095^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:40 AM UTC 2026
% Result : Theorem 49.30s 7.26s
% Output : Refutation 49.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP095^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n013.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 19:52:21 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.10/1.03 % (2577541)Will run a generic schedule for satisfiability detection.
% 4.10/1.03 % (2577552)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3803413341:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.10/1.03 % (2577547)% WARNING: option uhcvi not known.
% 4.10/1.03 % (2577546)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=757826348_2999 on theBenchmark for (2999ds/0Mi)
% 4.10/1.03 % (2577549)dis+10_1_sil=32000:sp=arity:random_seed=3341398160:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.10/1.03 % (2577548)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1311090350:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.10/1.03 % (2577547)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3787892803:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.10/1.03 % (2577550)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2842739918:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.10/1.03 % (2577551)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3321836771:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.10/1.03 % (2577547)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.10/1.03 % (2577550)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.10/1.03 % Exception at run slice level
% 4.10/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.10/1.03 % (2577547)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.10/1.03 % (2577552)Instruction limit reached!
% 4.10/1.03 % (2577552)------------------------------
% 4.10/1.03 % (2577552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.03 % (2577552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.03 % (2577552)CaDiCaL version: 2.1.3
% 4.10/1.03 % (2577552)Termination reason: Instruction limit
% 4.10/1.03 % (2577552)Termination phase: Saturation
% 4.10/1.03 % (2577552)Time elapsed: 0.040 s
% 4.10/1.03 % (2577552)Peak memory usage: 14 MB
% 4.10/1.03 % (2577552)Instructions burned: 162 (million)
% 4.10/1.03 % (2577561)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2470681523:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.10/1.03 % (2577549)Instruction limit reached!
% 4.10/1.03 % (2577549)------------------------------
% 4.10/1.03 % (2577549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.03 % (2577549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.03 % (2577549)CaDiCaL version: 2.1.3
% 4.10/1.03 % (2577549)Termination reason: Instruction limit
% 4.10/1.03 % (2577549)Termination phase: Saturation
% 4.10/1.03 % (2577549)Time elapsed: 0.047 s
% 4.10/1.03 % (2577549)Peak memory usage: 12 MB
% 4.10/1.03 % (2577549)Instructions burned: 104 (million)
% 4.10/1.03 % (2577560)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2236424123:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.10/1.03 % (2577550)Instruction limit reached!
% 4.10/1.03 % (2577550)------------------------------
% 4.10/1.03 % (2577550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.03 % (2577550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.03 % (2577550)CaDiCaL version: 2.1.3
% 4.10/1.03 % (2577550)Termination reason: Instruction limit
% 4.10/1.03 % (2577550)Termination phase: Saturation
% 4.10/1.03 % (2577550)Time elapsed: 0.060 s
% 4.10/1.03 % (2577550)Peak memory usage: 12 MB
% 4.10/1.03 % (2577550)Instructions burned: 116 (million)
% 4.10/1.03 % (2577551)Instruction limit reached!
% 4.10/1.03 % (2577551)------------------------------
% 4.10/1.03 % (2577551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/1.03 % (2577551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.03 % (2577551)CaDiCaL version: 2.1.3
% 4.10/1.03 % (2577551)Termination reason: Instruction limit
% 4.10/1.03 % (2577551)Termination phase: Saturation
% 4.10/1.03 % (2577551)Time elapsed: 0.061 s
% 4.10/1.03 % (2577551)Peak memory usage: 13 MB
% 4.10/1.03 % (2577551)Instructions burned: 132 (million)
% 4.10/1.03 % (2577563)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=566833743:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 25.48/3.99 % (2577561)Instruction limit reached!
% 25.48/3.99 % (2577561)------------------------------
% 25.48/3.99 % (2577561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.48/3.99 % (2577561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.48/3.99 % (2577561)CaDiCaL version: 2.1.3
% 25.48/3.99 % (2577561)Termination reason: Instruction limit
% 25.48/3.99 % (2577561)Termination phase: Saturation
% 25.48/3.99 % (2577561)Time elapsed: 0.033 s
% 25.48/3.99 % (2577561)Peak memory usage: 13 MB
% 25.48/3.99 % (2577561)Instructions burned: 134 (million)
% 25.48/3.99 % Exception at run slice level
% 25.48/3.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.48/3.99 % (2577563)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 25.48/3.99 % (2577565)ott-21_1_sil=16000:fs=off:random_seed=1895540852:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 25.48/3.99 % (2577569)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3161227139:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 25.48/3.99 % (2577566)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1744005660:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 25.48/3.99 % (2577563)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 25.48/3.99 % (2577568)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4254129474:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 25.48/3.99 % Exception at run slice level
% 25.48/3.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.48/3.99 % (2577574)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4193989919:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 25.48/3.99 % Exception at run slice level
% 25.48/3.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.48/3.99 % (2577576)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=763102219:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 25.48/3.99 % (2577565)Instruction limit reached!
% 25.48/3.99 % (2577565)------------------------------
% 25.48/3.99 % (2577565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.48/3.99 % (2577565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.48/3.99 % (2577565)CaDiCaL version: 2.1.3
% 25.48/3.99 % (2577565)Termination reason: Instruction limit
% 25.48/3.99 % (2577565)Termination phase: Saturation
% 25.48/3.99 % (2577565)Time elapsed: 0.096 s
% 25.48/3.99 % (2577565)Peak memory usage: 13 MB
% 25.48/3.99 % (2577565)Instructions burned: 180 (million)
% 25.48/3.99 % (2577576)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 25.48/3.99 % (2577578)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3836860878:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 25.48/3.99 % (2577578)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 25.48/3.99 % (2577576)Instruction limit reached!
% 25.48/3.99 % (2577576)------------------------------
% 25.48/3.99 % (2577576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.48/3.99 % (2577576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.48/3.99 % (2577576)CaDiCaL version: 2.1.3
% 25.48/3.99 % (2577576)Termination reason: Instruction limit
% 25.48/3.99 % (2577576)Termination phase: Saturation
% 25.48/3.99 % (2577576)Time elapsed: 0.175 s
% 25.48/3.99 % (2577576)Peak memory usage: 16 MB
% 25.48/3.99 % (2577576)Instructions burned: 697 (million)
% 25.48/3.99 % (2577616)fmb+10_1_sil=64000:random_seed=442330707:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 25.48/3.99 % (2577563)Instruction limit reached!
% 25.48/3.99 % (2577563)------------------------------
% 25.48/3.99 % (2577563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.48/3.99 % (2577563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.48/3.99 % (2577563)CaDiCaL version: 2.1.3
% 25.48/3.99 % (2577563)Termination reason: Instruction limit
% 25.48/3.99 % (2577563)Termination phase: Saturation
% 25.48/3.99 % (2577563)Time elapsed: 0.327 s
% 25.48/3.99 % (2577563)Peak memory usage: 15 MB
% 25.48/3.99 % (2577563)Instructions burned: 684 (million)
% 46.27/6.85 % (2577616)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.27/6.85 % Exception at run slice level
% 46.27/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.27/6.85 % (2577566)Instruction limit reached!
% 46.27/6.85 % (2577566)------------------------------
% 46.27/6.85 % (2577566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.27/6.85 % (2577566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.27/6.85 % (2577566)CaDiCaL version: 2.1.3
% 46.27/6.85 % (2577566)Termination reason: Instruction limit
% 46.27/6.85 % (2577566)Termination phase: Saturation
% 46.27/6.85 % (2577566)Time elapsed: 0.313 s
% 46.27/6.85 % (2577566)Peak memory usage: 13 MB
% 46.27/6.85 % (2577566)Instructions burned: 478 (million)
% 46.27/6.85 % (2577641)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1529309543:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 46.27/6.85 % (2577643)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=752915116:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 46.27/6.85 % (2577648)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3135312478:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 46.27/6.85 % Exception at run slice level
% 46.27/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.27/6.85 % Exception at run slice level
% 46.27/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.27/6.85 % (2577654)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4186443827:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 46.27/6.85 % (2577648)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.27/6.85 % (2577654)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.27/6.85 % (2577655)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1335527786:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 46.27/6.85 % (2577654)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 46.27/6.85 % Exception at run slice level
% 46.27/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.27/6.85 % (2577672)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1915363242:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 46.27/6.85 % Exception at run slice level
% 46.27/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.27/6.85 % (2577677)ott-2_1_sil=16000:newcnf=on:random_seed=3095373448:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 46.27/6.85 % (2577677)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.27/6.85 % (2577569)Instruction limit reached!
% 46.27/6.85 % (2577569)------------------------------
% 46.27/6.85 % (2577569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.27/6.85 % (2577569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.27/6.85 % (2577569)CaDiCaL version: 2.1.3
% 46.27/6.85 % (2577569)Termination reason: Instruction limit
% 46.27/6.85 % (2577569)Termination phase: Saturation
% 46.27/6.85 % (2577569)Time elapsed: 0.584 s
% 46.27/6.85 % (2577569)Peak memory usage: 18 MB
% 46.27/6.85 % (2577569)Instructions burned: 1179 (million)
% 46.27/6.85 % (2577578)Instruction limit reached!
% 46.27/6.85 % (2577578)------------------------------
% 46.27/6.85 % (2577578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.27/6.85 % (2577578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.27/6.85 % (2577578)CaDiCaL version: 2.1.3
% 46.27/6.85 % (2577578)Termination reason: Instruction limit
% 46.27/6.85 % (2577578)Termination phase: Saturation
% 46.27/6.85 % (2577578)Time elapsed: 0.484 s
% 46.27/6.85 % (2577578)Peak memory usage: 15 MB
% 46.27/6.85 % (2577578)Instructions burned: 879 (million)
% 46.27/6.85 % (2577717)ott+10_1_sil=32000:tgt=ground:random_seed=1011126000:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 46.27/6.85 % (2577718)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=351260176:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 46.27/6.85 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577730)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2857733662:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 49.30/7.26 % (2577730)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 49.30/7.26 % (2577654)Instruction limit reached!
% 49.30/7.26 % (2577654)------------------------------
% 49.30/7.26 % (2577654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577654)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577654)Termination reason: Instruction limit
% 49.30/7.26 % (2577654)Termination phase: Saturation
% 49.30/7.26 % (2577654)Time elapsed: 0.400 s
% 49.30/7.26 % (2577654)Peak memory usage: 16 MB
% 49.30/7.26 % (2577654)Instructions burned: 1476 (million)
% 49.30/7.26 % (2577748)dis+21_1_sil=32000:sas=cadical:random_seed=3718774706:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 49.30/7.26 % (2577677)Instruction limit reached!
% 49.30/7.26 % (2577677)------------------------------
% 49.30/7.26 % (2577677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577677)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577677)Termination reason: Instruction limit
% 49.30/7.26 % (2577677)Termination phase: Saturation
% 49.30/7.26 % (2577677)Time elapsed: 0.608 s
% 49.30/7.26 % (2577677)Peak memory usage: 15 MB
% 49.30/7.26 % (2577677)Instructions burned: 869 (million)
% 49.30/7.26 % (2577768)ott+11_1_sil=16000:gs=on:random_seed=913108147:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 49.30/7.26 % (2577768)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 49.30/7.26 % (2577748)Instruction limit reached!
% 49.30/7.26 % (2577748)------------------------------
% 49.30/7.26 % (2577748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577748)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577748)Termination reason: Instruction limit
% 49.30/7.26 % (2577748)Termination phase: Saturation
% 49.30/7.26 % (2577748)Time elapsed: 1.748 s
% 49.30/7.26 % (2577748)Peak memory usage: 25 MB
% 49.30/7.26 % (2577748)Instructions burned: 3775 (million)
% 49.30/7.26 % (2577796)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3673927046:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi)
% 49.30/7.26 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577798)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2568458924:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi)
% 49.30/7.26 % (2577768)Instruction limit reached!
% 49.30/7.26 % (2577768)------------------------------
% 49.30/7.26 % (2577768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577768)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577768)Termination reason: Instruction limit
% 49.30/7.26 % (2577768)Termination phase: Saturation
% 49.30/7.26 % (2577768)Time elapsed: 2.023 s
% 49.30/7.26 % (2577768)Peak memory usage: 24 MB
% 49.30/7.26 % (2577768)Instructions burned: 2251 (million)
% 49.30/7.26 % (2577800)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=495424869:i=29340_2967 on theBenchmark for (2967ds/29340Mi)
% 49.30/7.26 % (2577730)Instruction limit reached!
% 49.30/7.26 % (2577730)------------------------------
% 49.30/7.26 % (2577730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577730)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577730)Termination reason: Instruction limit
% 49.30/7.26 % (2577730)Termination phase: Saturation
% 49.30/7.26 % (2577730)Time elapsed: 2.918 s
% 49.30/7.26 % (2577730)Peak memory usage: 23 MB
% 49.30/7.26 % (2577730)Instructions burned: 3513 (million)
% 49.30/7.26 % (2577803)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=76213802:i=5211_2962 on theBenchmark for (2962ds/5211Mi)
% 49.30/7.26 % (2577717)Instruction limit reached!
% 49.30/7.26 % (2577717)------------------------------
% 49.30/7.26 % (2577717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577717)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577717)Termination reason: Instruction limit
% 49.30/7.26 % (2577717)Termination phase: Saturation
% 49.30/7.26 % (2577717)Time elapsed: 3.262 s
% 49.30/7.26 % (2577717)Peak memory usage: 24 MB
% 49.30/7.26 % (2577717)Instructions burned: 5116 (million)
% 49.30/7.26 % (2577907)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1690089926:i=5497:nm=2_2959 on theBenchmark for (2959ds/5497Mi)
% 49.30/7.26 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577912)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4002844486:fmbsr=2:i=46332_2959 on theBenchmark for (2959ds/46332Mi)
% 49.30/7.26 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577648)Instruction limit reached!
% 49.30/7.26 % (2577648)------------------------------
% 49.30/7.26 % (2577648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577648)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577648)Termination reason: Instruction limit
% 49.30/7.26 % (2577648)Termination phase: Saturation
% 49.30/7.26 % (2577648)Time elapsed: 3.644 s
% 49.30/7.26 % (2577648)Peak memory usage: 26 MB
% 49.30/7.26 % (2577648)Instructions burned: 5131 (million)
% 49.30/7.26 % (2577914)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1104953458:i=14071_2958 on theBenchmark for (2958ds/14071Mi)
% 49.30/7.26 % (2577915)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=122940300:i=22565:add=on:rawr=on_2958 on theBenchmark for (2958ds/22565Mi)
% 49.30/7.26 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577923)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1764535838:i=8173:av=off_2958 on theBenchmark for (2958ds/8173Mi)
% 49.30/7.26 % (2577798)Instruction limit reached!
% 49.30/7.26 % (2577798)------------------------------
% 49.30/7.26 % (2577798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577798)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577798)Termination reason: Instruction limit
% 49.30/7.26 % (2577798)Termination phase: Saturation
% 49.30/7.26 % (2577798)Time elapsed: 1.547 s
% 49.30/7.26 % (2577798)Peak memory usage: 26 MB
% 49.30/7.26 % (2577798)Instructions burned: 4592 (million)
% 49.30/7.26 % (2577967)dis+10_16:1_sil=16000:random_seed=1852685859:i=9155:fsr=off_2957 on theBenchmark for (2957ds/9155Mi)
% 49.30/7.26 % (2577803)Instruction limit reached!
% 49.30/7.26 % (2577803)------------------------------
% 49.30/7.26 % (2577803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577803)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577803)Termination reason: Instruction limit
% 49.30/7.26 % (2577803)Termination phase: Saturation
% 49.30/7.26 % (2577803)Time elapsed: 2.575 s
% 49.30/7.26 % (2577803)Peak memory usage: 32 MB
% 49.30/7.26 % (2577803)Instructions burned: 5213 (million)
% 49.30/7.26 % (2577969)ott-3_8_sil=64000:random_seed=1819008980:i=20139:bs=on_2936 on theBenchmark for (2936ds/20139Mi)
% 49.30/7.26 % (2577967)Instruction limit reached!
% 49.30/7.26 % (2577967)------------------------------
% 49.30/7.26 % (2577967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577967)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577967)Termination reason: Instruction limit
% 49.30/7.26 % (2577967)Termination phase: Saturation
% 49.30/7.26 % (2577967)Time elapsed: 2.306 s
% 49.30/7.26 % (2577967)Peak memory usage: 44 MB
% 49.30/7.26 % (2577967)Instructions burned: 9156 (million)
% 49.30/7.26 % (2577971)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1893959188:fmbsr=2:i=32576_2934 on theBenchmark for (2934ds/32576Mi)
% 49.30/7.26 % Exception at run slice level
% 49.30/7.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.30/7.26 % (2577973)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1644387399:i=11404_2933 on theBenchmark for (2933ds/11404Mi)
% 49.30/7.26 % (2577923) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2577541-2577923"...
% 49.30/7.26 % (2577923)...printing done.
% 49.30/7.26 % (2577923)Refutation found. Thanks to Tanya!
% 49.30/7.26 % SZS status Theorem for theBenchmark
% 49.30/7.26 % SZS output start Proof for theBenchmark
% 49.30/7.26 thf(type_def_5, type, poly_poly_real: $tType).
% 49.30/7.26 thf(type_def_6, type, set_poly_real: $tType).
% 49.30/7.26 thf(type_def_7, type, poly_real: $tType).
% 49.30/7.26 thf(type_def_8, type, poly_nat: $tType).
% 49.30/7.26 thf(type_def_9, type, poly_int: $tType).
% 49.30/7.26 thf(type_def_10, type, set_real: $tType).
% 49.30/7.26 thf(type_def_11, type, set_int: $tType).
% 49.30/7.26 thf(type_def_12, type, real: $tType).
% 49.30/7.26 thf(type_def_13, type, nat: $tType).
% 49.30/7.26 thf(type_def_14, type, int: $tType).
% 49.30/7.26 thf(type_def_15, type, sTfun: ($tType * $tType) > $tType).
% 49.30/7.26 thf(func_def_0, type, abs_abs_int: (int > int)).
% 49.30/7.26 thf(func_def_1, type, abs_abs_poly_real: (poly_real > poly_real)).
% 49.30/7.26 thf(func_def_2, type, abs_abs_real: (real > real)).
% 49.30/7.26 thf(func_def_3, type, minus_minus_real: (real > real > real)).
% 49.30/7.26 thf(func_def_4, type, one_one_int: int).
% 49.30/7.26 thf(func_def_5, type, one_one_nat: nat).
% 49.30/7.26 thf(func_def_6, type, one_one_poly_int: poly_int).
% 49.30/7.26 thf(func_def_7, type, one_one_poly_nat: poly_nat).
% 49.30/7.26 thf(func_def_8, type, one_one_poly_real: poly_real).
% 49.30/7.26 thf(func_def_9, type, one_one_real: real).
% 49.30/7.26 thf(func_def_10, type, zero_zero_int: int).
% 49.30/7.26 thf(func_def_11, type, zero_zero_nat: nat).
% 49.30/7.26 thf(func_def_12, type, zero_zero_poly_int: poly_int).
% 49.30/7.26 thf(func_def_13, type, zero_zero_poly_nat: poly_nat).
% 49.30/7.26 thf(func_def_14, type, zero_z1423781445y_real: poly_poly_real).
% 49.30/7.26 thf(func_def_15, type, zero_zero_poly_real: poly_real).
% 49.30/7.26 thf(func_def_16, type, zero_zero_real: real).
% 49.30/7.26 thf(func_def_17, type, ring_1_Ints_int: set_int).
% 49.30/7.26 thf(func_def_18, type, ring_1690226883y_real: set_poly_real).
% 49.30/7.26 thf(func_def_19, type, ring_1_Ints_real: set_real).
% 49.30/7.26 thf(func_def_20, type, ring_1_of_int_int: (int > int)).
% 49.30/7.26 thf(func_def_21, type, ring_12102921859ly_int: (int > poly_int)).
% 49.30/7.26 thf(func_def_22, type, ring_11511526659y_real: (int > poly_real)).
% 49.30/7.26 thf(func_def_23, type, ring_1_of_int_real: (int > real)).
% 49.30/7.26 thf(func_def_24, type, ord_less_int: (int > int > $o)).
% 49.30/7.26 thf(func_def_25, type, ord_less_nat: (nat > nat > $o)).
% 49.30/7.26 thf(func_def_26, type, ord_less_poly_real: (poly_real > poly_real > $o)).
% 49.30/7.26 thf(func_def_27, type, ord_less_real: (real > real > $o)).
% 49.30/7.26 thf(func_def_28, type, ord_less_eq_int: (int > int > $o)).
% 49.30/7.26 thf(func_def_29, type, ord_less_eq_nat: (nat > nat > $o)).
% 49.30/7.26 thf(func_def_30, type, ord_le1180086932y_real: (poly_real > poly_real > $o)).
% 49.30/7.26 thf(func_def_31, type, ord_less_eq_real: (real > real > $o)).
% 49.30/7.26 thf(func_def_32, type, algebraic_real: (real > $o)).
% 49.30/7.26 thf(func_def_33, type, degree_int: (poly_int > nat)).
% 49.30/7.26 thf(func_def_34, type, degree_nat: (poly_nat > nat)).
% 49.30/7.26 thf(func_def_35, type, degree_poly_real: (poly_poly_real > nat)).
% 49.30/7.26 thf(func_def_36, type, degree_real: (poly_real > nat)).
% 49.30/7.26 thf(func_def_37, type, poly_int2: (poly_int > int > int)).
% 49.30/7.26 thf(func_def_38, type, poly_nat2: (poly_nat > nat > nat)).
% 49.30/7.26 thf(func_def_39, type, poly_poly_real2: (poly_poly_real > poly_real > poly_real)).
% 49.30/7.26 thf(func_def_40, type, poly_real2: (poly_real > real > real)).
% 49.30/7.26 thf(func_def_41, type, coeff_int: (poly_int > nat > int)).
% 49.30/7.26 thf(func_def_42, type, coeff_nat: (poly_nat > nat > nat)).
% 49.30/7.26 thf(func_def_43, type, coeff_poly_real: (poly_poly_real > nat > poly_real)).
% 49.30/7.26 thf(func_def_44, type, coeff_real: (poly_real > nat > real)).
% 49.30/7.26 thf(func_def_45, type, power_power_int: (int > nat > int)).
% 49.30/7.26 thf(func_def_46, type, power_power_nat: (nat > nat > nat)).
% 49.30/7.26 thf(func_def_47, type, power_power_poly_int: (poly_int > nat > poly_int)).
% 49.30/7.26 thf(func_def_48, type, power_power_poly_nat: (poly_nat > nat > poly_nat)).
% 49.30/7.26 thf(func_def_49, type, power_2108872382y_real: (poly_real > nat > poly_real)).
% 49.30/7.26 thf(func_def_50, type, power_power_real: (real > nat > real)).
% 49.30/7.26 thf(func_def_51, type, field_1537545994s_real: set_real).
% 49.30/7.26 thf(func_def_52, type, divide_divide_int: (int > int > int)).
% 49.30/7.26 thf(func_def_53, type, divide_divide_nat: (nat > nat > nat)).
% 49.30/7.26 thf(func_def_54, type, divide1727078534y_real: (poly_real > poly_real > poly_real)).
% 49.30/7.26 thf(func_def_55, type, divide_divide_real: (real > real > real)).
% 49.30/7.26 thf(func_def_56, type, collect_real: ((real > $o) > set_real)).
% 49.30/7.26 thf(func_def_57, type, member_int: (int > set_int > $o)).
% 49.30/7.26 thf(func_def_58, type, member_poly_real: (poly_real > set_poly_real > $o)).
% 49.30/7.26 thf(func_def_59, type, member_real: (real > set_real > $o)).
% 49.30/7.26 thf(func_def_60, type, a: real).
% 49.30/7.26 thf(func_def_61, type, m: real).
% 49.30/7.26 thf(func_def_62, type, a2: int).
% 49.30/7.26 thf(func_def_63, type, b: int).
% 49.30/7.26 thf(func_def_64, type, n: nat).
% 49.30/7.26 thf(func_def_65, type, p: poly_real).
% 49.30/7.26 thf(func_def_66, type, roots: set_real).
% 49.30/7.26 thf(func_def_67, type, thesis: $o).
% 49.30/7.26 thf(func_def_68, type, x: real).
% 49.30/7.26 thf(func_def_72, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 49.30/7.26 thf(func_def_73, type, db0: !>[X0: $tType]:(X0)).
% 49.30/7.26 thf(func_def_74, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 49.30/7.26 thf(func_def_75, type, db1: !>[X0: $tType]:(X0)).
% 49.30/7.26 thf(func_def_76, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 49.30/7.26 thf(func_def_77, type, db2: !>[X0: $tType]:(X0)).
% 49.30/7.26 thf(func_def_78, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 49.30/7.26 thf(func_def_79, type, vAND: ($o > $o > $o)).
% 49.30/7.26 thf(func_def_80, type, vNOT: ($o > $o)).
% 49.30/7.26 thf(func_def_81, type, vOR: ($o > $o > $o)).
% 49.30/7.26 thf(func_def_82, type, vIMP: ($o > $o > $o)).
% 49.30/7.26 thf(func_def_83, type, sK0: poly_real).
% 49.30/7.26 thf(func_def_84, type, sK1: (poly_real > poly_real > nat)).
% 49.30/7.26 thf(func_def_85, type, sK2: (poly_real > nat)).
% 49.30/7.26 thf(func_def_86, type, sK3: (real > poly_real)).
% 49.30/7.26 thf(func_def_87, type, sK4: ((real > $o) > int)).
% 49.30/7.26 thf(func_def_88, type, sK5: ((int > $o) > int)).
% 49.30/7.26 thf(func_def_89, type, sK6: (real > int)).
% 49.30/7.26 thf(func_def_90, type, sK7: (int > int)).
% 49.30/7.26 thf(func_def_91, type, sK8: (poly_real > nat)).
% 49.30/7.26 thf(func_def_92, type, sK9: (poly_real > real > real > real)).
% 49.30/7.26 thf(func_def_93, type, sK10: (poly_real > real > real > real)).
% 49.30/7.26 thf(func_def_94, type, sK11: (real > real)).
% 49.30/7.26 thf(func_def_95, type, sK12: (real > real)).
% 49.30/7.26 thf(func_def_96, type, sK13: (poly_poly_real > nat > nat)).
% 49.30/7.26 thf(func_def_97, type, sK14: (poly_int > nat > nat)).
% 49.30/7.26 thf(func_def_98, type, sK15: (poly_real > nat > nat)).
% 49.30/7.26 thf(func_def_99, type, sK16: (poly_nat > nat > nat)).
% 49.30/7.26 thf(func_def_100, type, sK17: (poly_poly_real > nat > nat)).
% 49.30/7.26 thf(func_def_101, type, sK18: (poly_int > nat > nat)).
% 49.30/7.26 thf(func_def_102, type, sK19: (poly_real > nat > nat)).
% 49.30/7.26 thf(func_def_103, type, sK20: (poly_nat > nat > nat)).
% 49.30/7.26 thf(func_def_104, type, sK21: (real > int)).
% 49.30/7.26 thf(func_def_105, type, sK22: (real > int)).
% 49.30/7.26 thf(func_def_106, type, sK23: (poly_real > real)).
% 49.30/7.26 thf(func_def_107, type, sK24: (nat > real > int)).
% 49.30/7.26 thf(func_def_108, type, sK25: (nat > real > int)).
% 49.30/7.26 thf(func_def_109, type, sK26: (poly_real > real)).
% 49.30/7.26 thf(func_def_110, type, sK27: (poly_int > int)).
% 49.30/7.26 thf(func_def_111, type, sK28: (poly_poly_real > poly_real)).
% 49.30/7.26 thf(func_def_112, type, sK29: (poly_real > nat)).
% 49.30/7.26 thf(func_def_113, type, sK30: (poly_real > nat)).
% 49.30/7.26 thf(func_def_114, type, sK31: (poly_real > nat)).
% 49.30/7.26 thf(func_def_115, type, sK32: (real > poly_real)).
% 49.30/7.26 thf(func_def_116, type, sK33: poly_real).
% 49.30/7.26 thf(func_def_117, type, sK34: (real > poly_real)).
% 49.30/7.26 thf(func_def_118, type, sK35: (poly_real > nat)).
% 49.30/7.26 thf(func_def_119, type, sK36: (poly_real > nat)).
% 49.30/7.26 thf(func_def_120, type, sK37: (poly_real > nat)).
% 49.30/7.26 thf(func_def_121, type, sK38: (real > poly_real)).
% 49.30/7.26 thf(func_def_122, type, sK39: (poly_real > nat)).
% 49.30/7.26 thf(func_def_123, type, sK40: (poly_real > nat)).
% 49.30/7.26 thf(func_def_124, type, sK41: (poly_real > nat)).
% 49.30/7.26 thf(func_def_125, type, sK42: (poly_real > poly_real > real)).
% 49.30/7.26 thf(func_def_126, type, sK43: (poly_real > poly_real > nat)).
% 49.30/7.26 thf(func_def_127, type, sK44: (poly_real > poly_real > nat)).
% 49.30/7.26 thf(f3,axiom,(
% 49.30/7.26 ! [X0 : nat] : (member_real @ (coeff_real @ p @ X0) @ ring_1_Ints_real)),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_p_I1_J)).
% 49.30/7.26 thf(f4,axiom,(
% 49.30/7.26 (ord_less_int @ zero_zero_int @ b)),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_b)).
% 49.30/7.26 thf(f6,axiom,(
% 49.30/7.26 (((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))) != zero_zero_real)),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_no__root)).
% 49.30/7.26 thf(f7,axiom,(
% 49.30/7.26 (n = ((degree_real @ p)))),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_n__def)).
% 49.30/7.26 thf(f35,axiom,(
% 49.30/7.26 ! [X0 : int,X1 : int] : ((((ring_1_of_int_real @ X0)) = ((ring_1_of_int_real @ X1))) = (X0 = X1))),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_of__int__eq__iff)).
% 49.30/7.26 thf(f155,axiom,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : (! [X3 : nat] : (member_real @ (coeff_real @ X0 @ X3) @ ring_1_Ints_real) => ((ord_less_int @ zero_zero_int @ X1) => ((((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))) != zero_zero_real) => (ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))))))),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_int__poly__rat__no__root__ge)).
% 49.30/7.26 thf(f354,conjecture,(
% 49.30/7.26 (ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))),
% 49.30/7.26 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 49.30/7.26 thf(f355,negated_conjecture,(
% 49.30/7.26 ~(ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))),
% 49.30/7.26 inference(negated_conjecture,[status(cth)],[f354])).
% 49.30/7.26 thf(f358,plain,(
% 49.30/7.26 ! [X0 : nat] : (member_real @ (coeff_real @ p @ X0) @ ring_1_Ints_real)),
% 49.30/7.26 inference(rectify,[],[f3])).
% 49.30/7.26 thf(f359,plain,(
% 49.30/7.26 ! [X0 : nat] : (((member_real @ (coeff_real @ p @ X0) @ ring_1_Ints_real)) = $true)),
% 49.30/7.26 inference(fool_elimination,[],[f358])).
% 49.30/7.26 thf(f360,plain,(
% 49.30/7.26 (ord_less_int @ zero_zero_int @ b)),
% 49.30/7.26 inference(rectify,[],[f4])).
% 49.30/7.26 thf(f361,plain,(
% 49.30/7.26 (((ord_less_int @ zero_zero_int @ b)) = $true)),
% 49.30/7.26 inference(fool_elimination,[],[f360])).
% 49.30/7.26 thf(f370,plain,(
% 49.30/7.26 ! [X0 : int,X1 : int] : ((((ring_1_of_int_real @ X0) = (ring_1_of_int_real @ X1))) = ((X0 = X1)))),
% 49.30/7.26 inference(fool_elimination,[],[f35])).
% 49.30/7.26 thf(f479,plain,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : (! [X3 : nat] : (member_real @ (coeff_real @ X0 @ X3) @ ring_1_Ints_real) => ((ord_less_int @ zero_zero_int @ X1) => ((((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))) != zero_zero_real) => (ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))))))),
% 49.30/7.26 inference(rectify,[],[f155])).
% 49.30/7.26 thf(f480,plain,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : (! [X3 : nat] : (((member_real @ (coeff_real @ X0 @ X3) @ ring_1_Ints_real)) = $true) => ((((ord_less_int @ zero_zero_int @ X1)) = $true) => ((zero_zero_real != ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))) => (((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) = $true))))),
% 49.30/7.26 inference(fool_elimination,[],[f479])).
% 49.30/7.26 thf(f790,plain,(
% 49.30/7.26 ~(ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))),
% 49.30/7.26 inference(rectify,[],[f355])).
% 49.30/7.26 thf(f791,plain,(
% 49.30/7.26 ~ (((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))) = $true)),
% 49.30/7.26 inference(fool_elimination,[],[f790])).
% 49.30/7.26 thf(f796,plain,(
% 49.30/7.26 (((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))) != $true)),
% 49.30/7.26 inference(flattening,[],[f791])).
% 49.30/7.26 thf(f848,plain,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : ((((((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) = $true) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) | (((ord_less_int @ zero_zero_int @ X1)) != $true)) | ? [X3 : nat] : (((member_real @ (coeff_real @ X0 @ X3) @ ring_1_Ints_real)) != $true))),
% 49.30/7.26 inference(ennf_transformation,[],[f480])).
% 49.30/7.26 thf(f849,plain,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : ((((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) = $true) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))) | (((ord_less_int @ zero_zero_int @ X1)) != $true) | ? [X3 : nat] : (((member_real @ (coeff_real @ X0 @ X3) @ ring_1_Ints_real)) != $true))),
% 49.30/7.26 inference(flattening,[],[f848])).
% 49.30/7.26 thf(f1062,plain,(
% 49.30/7.26 ! [X0 : poly_real,X1 : int,X2 : int] : ((((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) = $true) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))) | (((ord_less_int @ zero_zero_int @ X1)) != $true) | ($true != ((member_real @ (coeff_real @ X0 @ (sK8 @ X0)) @ ring_1_Ints_real))))),
% 49.30/7.26 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK1 @ X1 @ X0)],[f849])).
% 49.30/7.26 thf(f1080,plain,(
% 49.30/7.26 ( ! [X0 : nat] : ((((member_real @ (coeff_real @ p @ X0) @ ring_1_Ints_real)) = $true)) )),
% 49.30/7.26 inference(cnf_transformation,[],[f359])).
% 49.30/7.26 thf(f1081,plain,(
% 49.30/7.26 (((ord_less_int @ zero_zero_int @ b)) = $true)),
% 49.30/7.26 inference(cnf_transformation,[],[f361])).
% 49.30/7.26 thf(f1083,plain,(
% 49.30/7.26 (zero_zero_real != ((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))),
% 49.30/7.26 inference(cnf_transformation,[],[f6])).
% 49.30/7.26 thf(f1084,plain,(
% 49.30/7.26 (n = ((degree_real @ p)))),
% 49.30/7.26 inference(cnf_transformation,[],[f7])).
% 49.30/7.26 thf(f1112,plain,(
% 49.30/7.26 ( ! [X0 : int,X1 : int] : (((((ring_1_of_int_real @ X0) = (ring_1_of_int_real @ X1))) = ((X0 = X1)))) )),
% 49.30/7.26 inference(cnf_transformation,[],[f370])).
% 49.30/7.26 thf(f1236,plain,(
% 49.30/7.26 ( ! [X2 : int,X0 : poly_real,X1 : int] : ((((ord_less_int @ zero_zero_int @ X1)) != $true) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1))))) | (((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ X1) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X2) @ (ring_1_of_int_real @ X1)))))) = $true) | ($true != ((member_real @ (coeff_real @ X0 @ (sK8 @ X0)) @ ring_1_Ints_real)))) )),
% 49.30/7.26 inference(cnf_transformation,[],[f1062])).
% 49.30/7.26 thf(f1454,plain,(
% 49.30/7.26 (((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))) != $true)),
% 49.30/7.26 inference(cnf_transformation,[],[f796])).
% 49.30/7.26 thf(f2070,plain,(
% 49.30/7.26 ( ! [X0 : int,X1 : int] : (($true = (((ring_1_of_int_real @ X0) = (ring_1_of_int_real @ X1)))) | (((X0 = X1)) = $false)) )),
% 49.30/7.26 inference(iff_proxy_clausification,[],[f1112])).
% 49.30/7.26 thf(f2074,plain,(
% 49.30/7.26 ( ! [X0 : int,X1 : int] : ((((ring_1_of_int_real @ X0)) = ((ring_1_of_int_real @ X1))) | (((X0 = X1)) = $false)) )),
% 49.30/7.26 inference(equality_proxy_clausification,[],[f2070])).
% 49.30/7.26 thf(f2075,plain,(
% 49.30/7.26 ( ! [X0 : int,X1 : int] : ((((ring_1_of_int_real @ X0)) = ((ring_1_of_int_real @ X1))) | (X0 != X1)) )),
% 49.30/7.26 inference(equality_proxy_clausification,[],[f2074])).
% 49.30/7.26 thf(f2154,plain,(
% 49.30/7.26 ($true != ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ n)) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ a2) @ (ring_1_of_int_real @ b)))))))),
% 49.30/7.26 inference(constrained_superposition,[],[f1454,f1084])).
% 49.30/7.26 thf(f2270,plain,(
% 49.30/7.26 ( ! [X0 : int] : (($true != ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ n)) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b))))))) | (a2 != X0)) )),
% 49.30/7.26 inference(constrained_superposition,[],[f2154,f2075])).
% 49.30/7.26 thf(f2548,plain,(
% 49.30/7.26 ( ! [X0 : int] : ((zero_zero_real != ((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b))))) | (a2 != X0)) )),
% 49.30/7.26 inference(constrained_superposition,[],[f1083,f2075])).
% 49.30/7.26 thf(f3924,plain,(
% 49.30/7.26 ( ! [X0 : poly_real,X1 : int] : (($true != $true) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X1) @ (ring_1_of_int_real @ b))))) | ($true = ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X1) @ (ring_1_of_int_real @ b))))))) | ($true != ((member_real @ (coeff_real @ X0 @ (sK8 @ X0)) @ ring_1_Ints_real)))) )),
% 49.30/7.26 inference(constrained_superposition,[],[f1236,f1081])).
% 49.30/7.26 thf(f3926,plain,(
% 49.30/7.26 ( ! [X0 : poly_real,X1 : int] : (($true != ((member_real @ (coeff_real @ X0 @ (sK8 @ X0)) @ ring_1_Ints_real))) | ($true = ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ X0))) @ (abs_abs_real @ (poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X1) @ (ring_1_of_int_real @ b))))))) | (zero_zero_real = ((poly_real2 @ X0 @ (divide_divide_real @ (ring_1_of_int_real @ X1) @ (ring_1_of_int_real @ b)))))) )),
% 49.30/7.26 inference(trivial_inequality_removal,[],[f3924])).
% 49.30/7.26 thf(f25963,plain,(
% 49.30/7.26 ( ! [X0 : int] : (($true != $true) | ($true = ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b))))))) | (zero_zero_real = ((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b)))))) )),
% 49.30/7.26 inference(constrained_superposition,[],[f3926,f1080])).
% 49.30/7.26 thf(f25966,plain,(
% 49.30/7.26 ( ! [X0 : int] : (($true = ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ (degree_real @ p))) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b))))))) | (zero_zero_real = ((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b)))))) )),
% 49.30/7.26 inference(trivial_inequality_removal,[],[f25963])).
% 49.30/7.26 thf(f25968,plain,(
% 49.30/7.26 ( ! [X0 : int] : (($true = ((ord_less_eq_real @ (divide_divide_real @ one_one_real @ (power_power_real @ (ring_1_of_int_real @ b) @ n)) @ (abs_abs_real @ (poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b))))))) | (zero_zero_real = ((poly_real2 @ p @ (divide_divide_real @ (ring_1_of_int_real @ X0) @ (ring_1_of_int_real @ b)))))) )),
% 49.30/7.26 inference(forward_demodulation,[],[f25966,f1084])).
% 49.30/7.26 thf(f28473,plain,(
% 49.30/7.26 ( ! [X2 : int] : ((a2 != X2)) )),
% 49.30/7.26 inference(global_subsumption,[],[f25968,f2548,f2270])).
% 49.30/7.26 thf(f28628,plain,(
% 49.30/7.26 $false),
% 49.30/7.26 inference(equality_resolution,[],[f28473])).
% 49.30/7.26 % SZS output end Proof for theBenchmark
% 49.30/7.26 % (2577923)------------------------------
% 49.30/7.26 % (2577923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.30/7.26 % (2577923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.30/7.26 % (2577923)CaDiCaL version: 2.1.3
% 49.30/7.26 % (2577923)Termination reason: Refutation
% 49.30/7.26 % (2577923)Time elapsed: 2.826 s
% 49.30/7.26 % (2577923)Peak memory usage: 43 MB
% 49.30/7.26 % (2577923)Instructions burned: 5659 (million)
% 49.30/7.26 % (2577541)Success in time 7.022 s
% 49.30/7.26 % Vampire exiting
%------------------------------------------------------------------------------