%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM858_1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 : Tue Sep 29 12:25:57 PM UTC 2026
% Result : Theorem 112.94s 17.05s
% Output : Refutation 112.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM858_1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 21:37:42 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.17/1.07 % (3224693)Will run a generic schedule for satisfiability detection.
% 4.17/1.07 % (3224701)dis+10_1_sil=32000:sp=arity:random_seed=1539283470:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.17/1.07 % (3224699)% WARNING: option uhcvi not known.
% 4.17/1.07 % (3224698)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=558335669_2999 on theBenchmark for (2999ds/0Mi)
% 4.17/1.07 % (3224699)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3247108982:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.17/1.07 % (3224700)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2566873005:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.17/1.07 % (3224702)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2227772185:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.17/1.07 % (3224703)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3205105032:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.17/1.07 % (3224698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.17/1.07 % (3224698)Terminated due to inappropriate strategy.
% 4.17/1.07 % (3224698)------------------------------
% 4.17/1.07 % (3224698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.17/1.07 % (3224698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.17/1.07 % (3224698)CaDiCaL version: 2.1.3
% 4.17/1.07 % (3224698)Termination reason: Inappropriate
% 4.17/1.07 % (3224698)Time elapsed: 0.001 s
% 4.17/1.07 % (3224698)Peak memory usage: 10 MB
% 4.17/1.07 % (3224698)Instructions burned: 1 (million)
% 4.17/1.07 % (3224704)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=965129104:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.17/1.07 % (3224698)------------------------------
% 4.17/1.07 % (3224698)------------------------------
% 4.17/1.07 % (3224712)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1408981969:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.17/1.07 % (3224712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.17/1.07 % (3224712)Terminated due to inappropriate strategy.
% 4.17/1.07 % (3224712)------------------------------
% 4.17/1.07 % (3224712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.17/1.07 % (3224712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.17/1.07 % (3224712)CaDiCaL version: 2.1.3
% 4.17/1.07 % (3224712)Termination reason: Inappropriate
% 4.17/1.07 % (3224712)Time elapsed: 0.001 s
% 4.17/1.07 % (3224712)Peak memory usage: 10 MB
% 4.17/1.07 % (3224712)Instructions burned: 1 (million)
% 4.17/1.07 % (3224712)------------------------------
% 4.17/1.07 % (3224712)------------------------------
% 4.17/1.07 % (3224701)Instruction limit reached!
% 4.17/1.07 % (3224701)------------------------------
% 4.17/1.07 % (3224701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.17/1.07 % (3224701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.17/1.07 % (3224701)CaDiCaL version: 2.1.3
% 4.17/1.07 % (3224701)Termination reason: Instruction limit
% 4.17/1.07 % (3224701)Termination phase: Saturation
% 4.17/1.07 % (3224701)Time elapsed: 0.035 s
% 4.17/1.07 % (3224701)Peak memory usage: 12 MB
% 4.17/1.07 % (3224701)Instructions burned: 103 (million)
% 4.17/1.07 % (3224715)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=6651712:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.17/1.07 % (3224714)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=273440471:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.17/1.07 % (3224702)Instruction limit reached!
% 4.17/1.07 % (3224702)------------------------------
% 4.17/1.07 % (3224702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.17/1.07 % (3224702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.17/1.07 % (3224702)CaDiCaL version: 2.1.3
% 4.17/1.07 % (3224702)Termination reason: Instruction limit
% 4.17/1.07 % (3224702)Termination phase: Saturation
% 4.17/1.07 % (3224702)Time elapsed: 0.072 s
% 4.17/1.07 % (3224702)Peak memory usage: 12 MB
% 4.17/1.07 % (3224702)Instructions burned: 116 (million)
% 4.17/1.07 % (3224703)Instruction limit reached!
% 4.17/1.07 % (3224703)------------------------------
% 4.17/1.07 % (3224703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224703)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224703)Termination reason: Instruction limit
% 5.81/1.38 % (3224703)Termination phase: Saturation
% 5.81/1.38 % (3224703)Time elapsed: 0.084 s
% 5.81/1.38 % (3224703)Peak memory usage: 12 MB
% 5.81/1.38 % (3224703)Instructions burned: 132 (million)
% 5.81/1.38 % (3224718)ott-21_1_sil=16000:fs=off:random_seed=4215387786:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.81/1.38 % (3224719)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4078107561:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.81/1.38 % (3224704)Instruction limit reached!
% 5.81/1.38 % (3224704)------------------------------
% 5.81/1.38 % (3224704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224704)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224704)Termination reason: Instruction limit
% 5.81/1.38 % (3224704)Termination phase: Saturation
% 5.81/1.38 % (3224704)Time elapsed: 0.110 s
% 5.81/1.38 % (3224704)Peak memory usage: 13 MB
% 5.81/1.38 % (3224704)Instructions burned: 159 (million)
% 5.81/1.38 % (3224714)Instruction limit reached!
% 5.81/1.38 % (3224714)------------------------------
% 5.81/1.38 % (3224714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224714)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224714)Termination reason: Instruction limit
% 5.81/1.38 % (3224714)Termination phase: Saturation
% 5.81/1.38 % (3224714)Time elapsed: 0.076 s
% 5.81/1.38 % (3224714)Peak memory usage: 12 MB
% 5.81/1.38 % (3224714)Instructions burned: 132 (million)
% 5.81/1.38 % (3224722)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3948991048:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.81/1.38 % (3224722)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.81/1.38 % (3224722)Terminated due to inappropriate strategy.
% 5.81/1.38 % (3224722)------------------------------
% 5.81/1.38 % (3224722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224722)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224722)Termination reason: Inappropriate
% 5.81/1.38 % (3224722)Time elapsed: 0.001 s
% 5.81/1.38 % (3224722)Peak memory usage: 10 MB
% 5.81/1.38 % (3224722)------------------------------
% 5.81/1.38 % (3224722)------------------------------
% 5.81/1.38 % (3224723)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=598719009:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.81/1.38 % (3224725)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2670355686:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.81/1.38 % (3224725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.81/1.38 % (3224725)Terminated due to inappropriate strategy.
% 5.81/1.38 % (3224725)------------------------------
% 5.81/1.38 % (3224725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224725)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224725)Termination reason: Inappropriate
% 5.81/1.38 % (3224725)Time elapsed: 0.001 s
% 5.81/1.38 % (3224725)Peak memory usage: 10 MB
% 5.81/1.38 % (3224725)------------------------------
% 5.81/1.38 % (3224725)------------------------------
% 5.81/1.38 % (3224728)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=1622149929:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 5.81/1.38 % (3224718)Instruction limit reached!
% 5.81/1.38 % (3224718)------------------------------
% 5.81/1.38 % (3224718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.38 % (3224718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.38 % (3224718)CaDiCaL version: 2.1.3
% 5.81/1.38 % (3224718)Termination reason: Instruction limit
% 5.81/1.38 % (3224718)Termination phase: Saturation
% 5.81/1.38 % (3224718)Time elapsed: 0.081 s
% 5.81/1.38 % (3224718)Peak memory usage: 12 MB
% 19.58/3.22 % (3224718)Instructions burned: 181 (million)
% 19.58/3.22 % (3224730)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=518078970:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 19.58/3.22 % (3224715)Instruction limit reached!
% 19.58/3.22 % (3224715)------------------------------
% 19.58/3.22 % (3224715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.58/3.22 % (3224715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.22 % (3224715)CaDiCaL version: 2.1.3
% 19.58/3.22 % (3224715)Termination reason: Instruction limit
% 19.58/3.22 % (3224715)Termination phase: Saturation
% 19.58/3.22 % (3224715)Time elapsed: 0.223 s
% 19.58/3.22 % (3224715)Peak memory usage: 18 MB
% 19.58/3.22 % (3224715)Instructions burned: 687 (million)
% 19.58/3.22 % (3224732)fmb+10_1_sil=64000:random_seed=2694245316:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 19.58/3.22 % (3224732)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 19.58/3.22 % (3224732)Terminated due to inappropriate strategy.
% 19.58/3.22 % (3224732)------------------------------
% 19.58/3.22 % (3224732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.58/3.22 % (3224732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.22 % (3224732)CaDiCaL version: 2.1.3
% 19.58/3.22 % (3224732)Termination reason: Inappropriate
% 19.58/3.22 % (3224732)Time elapsed: 0.0000 s
% 19.58/3.22 % (3224732)Peak memory usage: 10 MB
% 19.58/3.22 % (3224732)Instructions burned: 1 (million)
% 19.58/3.22 % (3224732)------------------------------
% 19.58/3.22 % (3224732)------------------------------
% 19.58/3.22 % (3224734)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3231121800:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 19.58/3.22 % (3224734)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 19.58/3.22 % (3224734)Terminated due to inappropriate strategy.
% 19.58/3.22 % (3224734)------------------------------
% 19.58/3.22 % (3224734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.58/3.22 % (3224734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.22 % (3224734)CaDiCaL version: 2.1.3
% 19.58/3.22 % (3224734)Termination reason: Inappropriate
% 19.58/3.22 % (3224734)Time elapsed: 0.0000 s
% 19.58/3.22 % (3224734)Peak memory usage: 10 MB
% 19.58/3.22 % (3224734)Instructions burned: 1 (million)
% 19.58/3.22 % (3224734)------------------------------
% 19.58/3.22 % (3224734)------------------------------
% 19.58/3.22 % (3224736)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=606748695:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 19.58/3.22 % (3224736)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 19.58/3.22 % (3224736)Terminated due to inappropriate strategy.
% 19.58/3.22 % (3224736)------------------------------
% 19.58/3.22 % (3224736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.58/3.22 % (3224736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.22 % (3224736)CaDiCaL version: 2.1.3
% 19.58/3.22 % (3224736)Termination reason: Inappropriate
% 19.58/3.22 % (3224736)Time elapsed: 0.0000 s
% 19.58/3.22 % (3224736)Peak memory usage: 10 MB
% 19.58/3.22 % (3224736)Instructions burned: 1 (million)
% 19.58/3.22 % (3224736)------------------------------
% 19.58/3.22 % (3224736)------------------------------
% 19.58/3.22 % (3224738)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4238535454:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 19.58/3.22 % (3224719)Instruction limit reached!
% 19.58/3.22 % (3224719)------------------------------
% 19.58/3.22 % (3224719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.58/3.22 % (3224719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.22 % (3224719)CaDiCaL version: 2.1.3
% 19.58/3.22 % (3224719)Termination reason: Instruction limit
% 19.58/3.22 % (3224719)Termination phase: Saturation
% 19.58/3.22 % (3224719)Time elapsed: 0.327 s
% 19.58/3.22 % (3224719)Peak memory usage: 14 MB
% 19.58/3.22 % (3224719)Instructions burned: 477 (million)
% 19.58/3.22 % (3224740)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=681909258:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 19.58/3.22 % (3224728)Instruction limit reached!
% 19.58/3.22 % (3224728)------------------------------
% 19.58/3.22 % (3224728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224728)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224728)Termination reason: Instruction limit
% 27.38/4.31 % (3224728)Termination phase: Saturation
% 27.38/4.31 % (3224728)Time elapsed: 0.427 s
% 27.38/4.31 % (3224728)Peak memory usage: 19 MB
% 27.38/4.31 % (3224728)Instructions burned: 693 (million)
% 27.38/4.31 % (3224742)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3399981225:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 27.38/4.31 % (3224742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 27.38/4.31 % (3224742)Terminated due to inappropriate strategy.
% 27.38/4.31 % (3224742)------------------------------
% 27.38/4.31 % (3224742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224742)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224742)Termination reason: Inappropriate
% 27.38/4.31 % (3224742)Time elapsed: 0.001 s
% 27.38/4.31 % (3224742)Peak memory usage: 10 MB
% 27.38/4.31 % (3224742)Instructions burned: 1 (million)
% 27.38/4.31 % (3224742)------------------------------
% 27.38/4.31 % (3224742)------------------------------
% 27.38/4.31 % (3224744)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3605965445:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 27.38/4.31 % (3224744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 27.38/4.31 % (3224744)Terminated due to inappropriate strategy.
% 27.38/4.31 % (3224744)------------------------------
% 27.38/4.31 % (3224744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224744)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224744)Termination reason: Inappropriate
% 27.38/4.31 % (3224744)Time elapsed: 0.001 s
% 27.38/4.31 % (3224744)Peak memory usage: 10 MB
% 27.38/4.31 % (3224744)Instructions burned: 1 (million)
% 27.38/4.31 % (3224744)------------------------------
% 27.38/4.31 % (3224744)------------------------------
% 27.38/4.31 % (3224746)ott-2_1_sil=16000:newcnf=on:random_seed=3767078571:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 27.38/4.31 % (3224730)Instruction limit reached!
% 27.38/4.31 % (3224730)------------------------------
% 27.38/4.31 % (3224730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224730)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224730)Termination reason: Instruction limit
% 27.38/4.31 % (3224730)Termination phase: Saturation
% 27.38/4.31 % (3224730)Time elapsed: 0.516 s
% 27.38/4.31 % (3224730)Peak memory usage: 18 MB
% 27.38/4.31 % (3224730)Instructions burned: 879 (million)
% 27.38/4.31 % (3224748)ott+10_1_sil=32000:tgt=ground:random_seed=430231691:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 27.38/4.31 % (3224723)Instruction limit reached!
% 27.38/4.31 % (3224723)------------------------------
% 27.38/4.31 % (3224723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224723)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224723)Termination reason: Instruction limit
% 27.38/4.31 % (3224723)Termination phase: Saturation
% 27.38/4.31 % (3224723)Time elapsed: 0.727 s
% 27.38/4.31 % (3224723)Peak memory usage: 17 MB
% 27.38/4.31 % (3224723)Instructions burned: 1179 (million)
% 27.38/4.31 % (3224750)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=570062682:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 27.38/4.31 % (3224750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 27.38/4.31 % (3224750)Terminated due to inappropriate strategy.
% 27.38/4.31 % (3224750)------------------------------
% 27.38/4.31 % (3224750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.38/4.31 % (3224750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.38/4.31 % (3224750)CaDiCaL version: 2.1.3
% 27.38/4.31 % (3224750)Termination reason: Inappropriate
% 27.38/4.31 % (3224750)Time elapsed: 0.001 s
% 27.38/4.31 % (3224750)Peak memory usage: 10 MB
% 27.38/4.31 % (3224750)Instructions burned: 1 (million)
% 27.38/4.31 % (3224750)------------------------------
% 27.38/4.31 % (3224750)------------------------------
% 27.38/4.31 % (3224752)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1775874465:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 84.17/12.30 % (3224746)Instruction limit reached!
% 84.17/12.30 % (3224746)------------------------------
% 84.17/12.30 % (3224746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224746)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224746)Termination reason: Instruction limit
% 84.17/12.30 % (3224746)Termination phase: Saturation
% 84.17/12.30 % (3224746)Time elapsed: 0.451 s
% 84.17/12.30 % (3224746)Peak memory usage: 13 MB
% 84.17/12.30 % (3224746)Instructions burned: 870 (million)
% 84.17/12.30 % (3224754)dis+21_1_sil=32000:sas=cadical:random_seed=3405766338:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 84.17/12.30 % (3224740)Instruction limit reached!
% 84.17/12.30 % (3224740)------------------------------
% 84.17/12.30 % (3224740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224740)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224740)Termination reason: Instruction limit
% 84.17/12.30 % (3224740)Termination phase: Saturation
% 84.17/12.30 % (3224740)Time elapsed: 0.848 s
% 84.17/12.30 % (3224740)Peak memory usage: 29 MB
% 84.17/12.30 % (3224740)Instructions burned: 1473 (million)
% 84.17/12.30 % (3224756)ott+11_1_sil=16000:gs=on:random_seed=2844577290:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 84.17/12.30 % (3224738)Instruction limit reached!
% 84.17/12.30 % (3224738)------------------------------
% 84.17/12.30 % (3224738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224738)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224738)Termination reason: Instruction limit
% 84.17/12.30 % (3224738)Termination phase: Saturation
% 84.17/12.30 % (3224738)Time elapsed: 1.439 s
% 84.17/12.30 % (3224738)Peak memory usage: 39 MB
% 84.17/12.30 % (3224738)Instructions burned: 5131 (million)
% 84.17/12.30 % (3224758)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4109769501:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 84.17/12.30 % (3224758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 84.17/12.30 % (3224758)Terminated due to inappropriate strategy.
% 84.17/12.30 % (3224758)------------------------------
% 84.17/12.30 % (3224758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224758)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224758)Termination reason: Inappropriate
% 84.17/12.30 % (3224758)Time elapsed: 0.0000 s
% 84.17/12.30 % (3224758)Peak memory usage: 10 MB
% 84.17/12.30 % (3224758)Instructions burned: 1 (million)
% 84.17/12.30 % (3224758)------------------------------
% 84.17/12.30 % (3224758)------------------------------
% 84.17/12.30 % (3224760)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=160354377:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 84.17/12.30 % (3224756)Instruction limit reached!
% 84.17/12.30 % (3224756)------------------------------
% 84.17/12.30 % (3224756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224756)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224756)Termination reason: Instruction limit
% 84.17/12.30 % (3224756)Termination phase: Saturation
% 84.17/12.30 % (3224756)Time elapsed: 1.123 s
% 84.17/12.30 % (3224756)Peak memory usage: 17 MB
% 84.17/12.30 % (3224756)Instructions burned: 2251 (million)
% 84.17/12.30 % (3224762)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=970018720:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 84.17/12.30 % (3224752)Instruction limit reached!
% 84.17/12.30 % (3224752)------------------------------
% 84.17/12.30 % (3224752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.17/12.30 % (3224752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.17/12.30 % (3224752)CaDiCaL version: 2.1.3
% 84.17/12.30 % (3224752)Termination reason: Instruction limit
% 84.17/12.30 % (3224752)Termination phase: Saturation
% 84.17/12.30 % (3224752)Time elapsed: 1.845 s
% 112.94/17.04 % (3224752)Peak memory usage: 29 MB
% 112.94/17.04 % (3224752)Instructions burned: 3514 (million)
% 112.94/17.04 % (3224764)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2372140275:i=5211_2972 on theBenchmark for (2972ds/5211Mi)
% 112.94/17.04 % (3224760)Instruction limit reached!
% 112.94/17.04 % (3224760)------------------------------
% 112.94/17.04 % (3224760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224760)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224760)Termination reason: Instruction limit
% 112.94/17.04 % (3224760)Termination phase: Saturation
% 112.94/17.04 % (3224760)Time elapsed: 1.258 s
% 112.94/17.04 % (3224760)Peak memory usage: 43 MB
% 112.94/17.04 % (3224760)Instructions burned: 4595 (million)
% 112.94/17.04 % (3224766)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3827842631:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 112.94/17.04 % (3224766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.94/17.04 % (3224766)Terminated due to inappropriate strategy.
% 112.94/17.04 % (3224766)------------------------------
% 112.94/17.04 % (3224766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224766)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224766)Termination reason: Inappropriate
% 112.94/17.04 % (3224766)Time elapsed: 0.0000 s
% 112.94/17.04 % (3224766)Peak memory usage: 10 MB
% 112.94/17.04 % (3224766)Instructions burned: 1 (million)
% 112.94/17.04 % (3224766)------------------------------
% 112.94/17.04 % (3224766)------------------------------
% 112.94/17.04 % (3224768)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2002832815:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 112.94/17.04 % (3224768)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.94/17.04 % (3224768)Terminated due to inappropriate strategy.
% 112.94/17.04 % (3224768)------------------------------
% 112.94/17.04 % (3224768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224768)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224768)Termination reason: Inappropriate
% 112.94/17.04 % (3224768)Time elapsed: 0.0000 s
% 112.94/17.04 % (3224768)Peak memory usage: 10 MB
% 112.94/17.04 % (3224768)Instructions burned: 1 (million)
% 112.94/17.04 % (3224768)------------------------------
% 112.94/17.04 % (3224768)------------------------------
% 112.94/17.04 % (3224770)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=962431047:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 112.94/17.04 % (3224770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.94/17.04 % (3224770)Terminated due to inappropriate strategy.
% 112.94/17.04 % (3224770)------------------------------
% 112.94/17.04 % (3224770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224770)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224770)Termination reason: Inappropriate
% 112.94/17.04 % (3224770)Time elapsed: 0.0000 s
% 112.94/17.04 % (3224770)Peak memory usage: 10 MB
% 112.94/17.04 % (3224770)Instructions burned: 1 (million)
% 112.94/17.04 % (3224770)------------------------------
% 112.94/17.04 % (3224770)------------------------------
% 112.94/17.04 % (3224772)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=417526084:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi)
% 112.94/17.04 % (3224754)Instruction limit reached!
% 112.94/17.04 % (3224754)------------------------------
% 112.94/17.04 % (3224754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224754)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224754)Termination reason: Instruction limit
% 112.94/17.04 % (3224754)Termination phase: Saturation
% 112.94/17.04 % (3224754)Time elapsed: 1.980 s
% 112.94/17.04 % (3224754)Peak memory usage: 31 MB
% 112.94/17.04 % (3224754)Instructions burned: 3774 (million)
% 112.94/17.04 % (3224774)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=114807343:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi)
% 112.94/17.04 % (3224748)Instruction limit reached!
% 112.94/17.04 % (3224748)------------------------------
% 112.94/17.04 % (3224748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224748)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224748)Termination reason: Instruction limit
% 112.94/17.04 % (3224748)Termination phase: Saturation
% 112.94/17.04 % (3224748)Time elapsed: 3.113 s
% 112.94/17.04 % (3224748)Peak memory usage: 31 MB
% 112.94/17.04 % (3224748)Instructions burned: 5116 (million)
% 112.94/17.04 % (3224776)dis+10_16:1_sil=16000:random_seed=403674617:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi)
% 112.94/17.04 % (3224764)Instruction limit reached!
% 112.94/17.04 % (3224764)------------------------------
% 112.94/17.04 % (3224764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.04 % (3224764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.04 % (3224764)CaDiCaL version: 2.1.3
% 112.94/17.04 % (3224764)Termination reason: Instruction limit
% 112.94/17.04 % (3224764)Termination phase: Saturation
% 112.94/17.04 % (3224764)Time elapsed: 2.794 s
% 112.94/17.04 % (3224764)Peak memory usage: 50 MB
% 112.94/17.04 % (3224764)Instructions burned: 5212 (million)
% 112.94/17.05 % (3224778)ott-3_8_sil=64000:random_seed=2646638885:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi)
% 112.94/17.05 % (3224772)Instruction limit reached!
% 112.94/17.05 % (3224772)------------------------------
% 112.94/17.05 % (3224772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224772)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224772)Termination reason: Instruction limit
% 112.94/17.05 % (3224772)Termination phase: Saturation
% 112.94/17.05 % (3224772)Time elapsed: 4.772 s
% 112.94/17.05 % (3224772)Peak memory usage: 59 MB
% 112.94/17.05 % (3224772)Instructions burned: 22571 (million)
% 112.94/17.05 % (3224780)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3726235050:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi)
% 112.94/17.05 % (3224780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.94/17.05 % (3224780)Terminated due to inappropriate strategy.
% 112.94/17.05 % (3224780)------------------------------
% 112.94/17.05 % (3224780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224780)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224780)Termination reason: Inappropriate
% 112.94/17.05 % (3224780)Time elapsed: 0.0000 s
% 112.94/17.05 % (3224780)Peak memory usage: 10 MB
% 112.94/17.05 % (3224780)Instructions burned: 1 (million)
% 112.94/17.05 % (3224780)------------------------------
% 112.94/17.05 % (3224780)------------------------------
% 112.94/17.05 % (3224782)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=788705062:i=11404_2920 on theBenchmark for (2920ds/11404Mi)
% 112.94/17.05 % (3224774)Instruction limit reached!
% 112.94/17.05 % (3224774)------------------------------
% 112.94/17.05 % (3224774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224774)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224774)Termination reason: Instruction limit
% 112.94/17.05 % (3224774)Termination phase: Saturation
% 112.94/17.05 % (3224774)Time elapsed: 4.884 s
% 112.94/17.05 % (3224774)Peak memory usage: 48 MB
% 112.94/17.05 % (3224774)Instructions burned: 8174 (million)
% 112.94/17.05 % (3224784)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2145282955:i=14134_2919 on theBenchmark for (2919ds/14134Mi)
% 112.94/17.05 % (3224776)Instruction limit reached!
% 112.94/17.05 % (3224776)------------------------------
% 112.94/17.05 % (3224776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224776)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224776)Termination reason: Instruction limit
% 112.94/17.05 % (3224776)Termination phase: Saturation
% 112.94/17.05 % (3224776)Time elapsed: 4.616 s
% 112.94/17.05 % (3224776)Peak memory usage: 50 MB
% 112.94/17.05 % (3224776)Instructions burned: 9156 (million)
% 112.94/17.05 % (3224786)dis+33_16_sil=32000:sac=on:random_seed=16855726:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi)
% 112.94/17.05 % (3224782)Instruction limit reached!
% 112.94/17.05 % (3224782)------------------------------
% 112.94/17.05 % (3224782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224782)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224782)Termination reason: Instruction limit
% 112.94/17.05 % (3224782)Termination phase: Saturation
% 112.94/17.05 % (3224782)Time elapsed: 3.955 s
% 112.94/17.05 % (3224782)Peak memory usage: 50 MB
% 112.94/17.05 % (3224782)Instructions burned: 11405 (million)
% 112.94/17.05 % (3224788)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2260395281:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi)
% 112.94/17.05 % (3224786)Instruction limit reached!
% 112.94/17.05 % (3224786)------------------------------
% 112.94/17.05 % (3224786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224786)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224786)Termination reason: Instruction limit
% 112.94/17.05 % (3224786)Termination phase: Saturation
% 112.94/17.05 % (3224786)Time elapsed: 6.976 s
% 112.94/17.05 % (3224786)Peak memory usage: 29 MB
% 112.94/17.05 % (3224786)Instructions burned: 15853 (million)
% 112.94/17.05 % (3224836)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1588558915:s2a=on:i=53295_2844 on theBenchmark for (2844ds/53295Mi)
% 112.94/17.05 % (3224762)Instruction limit reached!
% 112.94/17.05 % (3224762)------------------------------
% 112.94/17.05 % (3224762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224762)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224762)Termination reason: Instruction limit
% 112.94/17.05 % (3224762)Termination phase: Saturation
% 112.94/17.05 % (3224762)Time elapsed: 13.750 s
% 112.94/17.05 % (3224762)Peak memory usage: 272 MB
% 112.94/17.05 % (3224762)Instructions burned: 29340 (million)
% 112.94/17.05 % (3224838)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=248015883:i=26857:ins=20_2837 on theBenchmark for (2837ds/26857Mi)
% 112.94/17.05 % (3224838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.94/17.05 % (3224838)Terminated due to inappropriate strategy.
% 112.94/17.05 % (3224838)------------------------------
% 112.94/17.05 % (3224838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224838)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224838)Termination reason: Inappropriate
% 112.94/17.05 % (3224838)Time elapsed: 0.001 s
% 112.94/17.05 % (3224838)Peak memory usage: 10 MB
% 112.94/17.05 % (3224838)Instructions burned: 1 (million)
% 112.94/17.05 % (3224838)------------------------------
% 112.94/17.05 % (3224838)------------------------------
% 112.94/17.05 % (3224840)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3184741085:i=28120:bs=on:fsr=off_2836 on theBenchmark for (2836ds/28120Mi)
% 112.94/17.05 % (3224784) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3224693-3224784"...
% 112.94/17.05 % (3224784)...printing done.
% 112.94/17.05 % (3224784)Refutation found. Thanks to Tanya!
% 112.94/17.05 % SZS status Theorem for theBenchmark
% 112.94/17.05 % SZS output start Proof for theBenchmark
% 112.94/17.05 tff(func_def_0, type, summation: $int > $int).
% 112.94/17.05 tff(func_def_1, type, max: ($int * $int) > $int).
% 112.94/17.05 tff(func_def_6, type, sK0: ($int * $int * $int) > $int).
% 112.94/17.05 tff(func_def_7, type, sK1: ($int * $int * $int) > $int).
% 112.94/17.05 tff(func_def_8, type, sK2: $int).
% 112.94/17.05 tff(func_def_9, type, sK3: $int).
% 112.94/17.05 tff(func_def_10, type, sK4: $int).
% 112.94/17.05 tff(pred_def_1, type, ub: ($int * $int * $int) > $o).
% 112.94/17.05 tff(pred_def_2, type, model_max: ($int * $int * $int) > $o).
% 112.94/17.05 tff(pred_def_3, type, model_ub: ($int * $int * $int) > $o).
% 112.94/17.05 tff(pred_def_4, type, minsol_model_max: ($int * $int * $int) > $o).
% 112.94/17.05 tff(pred_def_5, type, minsol_model_ub: ($int * $int * $int) > $o).
% 112.94/17.05 tff(f2,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int] : (max(X0,X1) = X0 | ~$lesseq(X1,X0))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_1)).
% 112.94/17.05 tff(f3,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int] : (max(X0,X1) = X1 | ~$lesseq(X0,X1))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_2)).
% 112.94/17.05 tff(f4,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (ub(X0,X1,X2) <=> ($lesseq(X0,X2) & $lesseq(X1,X2)))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ub)).
% 112.94/17.05 tff(f5,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (model_max(X0,X1,X2) <=> X2 = max(X0,X1))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_max_1)).
% 112.94/17.05 tff(f6,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (model_ub(X0,X1,X2) <=> ub(X0,X1,X2))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_ub_1)).
% 112.94/17.05 tff(f7,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_max(X0,X1,X2) <=> (model_max(X0,X1,X2) & ! [X3 : $int] : (model_max(X0,X1,X3) => $lesseq(X2,X3))))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_max)).
% 112.94/17.05 tff(f8,axiom,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <=> (model_ub(X0,X1,X2) & ! [X3 : $int] : (model_ub(X0,X1,X3) => $lesseq(X2,X3))))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_ub)).
% 112.94/17.05 tff(f9,conjecture,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <=> minsol_model_max(X0,X1,X2))),
% 112.94/17.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_is_ub_1)).
% 112.94/17.05 tff(f10,negated_conjecture,(
% 112.94/17.05 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <=> minsol_model_max(X0,X1,X2))),
% 112.94/17.05 inference(negated_conjecture,[status(cth)],[f9])).
% 112.94/17.05 tff(f12,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int] : (max(X0,X1) = X0 | $less(X0,X1))),
% 112.94/17.05 inference(theory_normalization,[],[f2])).
% 112.94/17.05 tff(f13,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int] : (max(X0,X1) = X1 | $less(X1,X0))),
% 112.94/17.05 inference(theory_normalization,[],[f3])).
% 112.94/17.05 tff(f14,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (ub(X0,X1,X2) <=> (~$less(X2,X0) & ~$less(X2,X1)))),
% 112.94/17.05 inference(theory_normalization,[],[f4])).
% 112.94/17.05 tff(f15,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_max(X0,X1,X2) <=> (model_max(X0,X1,X2) & ! [X3 : $int] : (model_max(X0,X1,X3) => ~$less(X3,X2))))),
% 112.94/17.05 inference(theory_normalization,[],[f7])).
% 112.94/17.05 tff(f16,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <=> (model_ub(X0,X1,X2) & ! [X3 : $int] : (model_ub(X0,X1,X3) => ~$less(X3,X2))))),
% 112.94/17.05 inference(theory_normalization,[],[f8])).
% 112.94/17.05 tff(f22,definition,(
% 112.94/17.05 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 112.94/17.05 introduced(theory,[tha_non-reflexivity])).
% 112.94/17.05 tff(f23,definition,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X0,X2) | ~$less(X1,X2) | ~$less(X0,X1)) )),
% 112.94/17.05 introduced(theory,[tha_transitivity])).
% 112.94/17.05 tff(f24,definition,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 112.94/17.05 introduced(theory,[tha_order_totality])).
% 112.94/17.05 tff(f29,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_max(X0,X1,X2) <=> (model_max(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_max(X0,X1,X3))))),
% 112.94/17.05 inference(ennf_transformation,[],[f15])).
% 112.94/17.05 tff(f30,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <=> (model_ub(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_ub(X0,X1,X3))))),
% 112.94/17.05 inference(ennf_transformation,[],[f16])).
% 112.94/17.05 tff(f31,plain,(
% 112.94/17.05 ? [X0 : $int,X1 : $int,X2 : $int] : (minsol_model_ub(X0,X1,X2) <~> minsol_model_max(X0,X1,X2))),
% 112.94/17.05 inference(ennf_transformation,[],[f10])).
% 112.94/17.05 tff(f33,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((ub(X0,X1,X2) | ($less(X2,X0) | $less(X2,X1))) & ((~$less(X2,X0) & ~$less(X2,X1)) | ~ub(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f14])).
% 112.94/17.05 tff(f34,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((ub(X0,X1,X2) | $less(X2,X0) | $less(X2,X1)) & ((~$less(X2,X0) & ~$less(X2,X1)) | ~ub(X0,X1,X2)))),
% 112.94/17.05 inference(flattening,[],[f33])).
% 112.94/17.05 tff(f35,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((model_max(X0,X1,X2) | max(X0,X1) != X2) & (X2 = max(X0,X1) | ~model_max(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f5])).
% 112.94/17.05 tff(f36,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((model_ub(X0,X1,X2) | ~ub(X0,X1,X2)) & (ub(X0,X1,X2) | ~model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f6])).
% 112.94/17.05 tff(f37,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_max(X0,X1,X2) | (~model_max(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_max(X0,X1,X3)))) & ((model_max(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_max(X0,X1,X3))) | ~minsol_model_max(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f29])).
% 112.94/17.05 tff(f38,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_max(X0,X1,X2) | ~model_max(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_max(X0,X1,X3))) & ((model_max(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_max(X0,X1,X3))) | ~minsol_model_max(X0,X1,X2)))),
% 112.94/17.05 inference(flattening,[],[f37])).
% 112.94/17.05 tff(f39,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_max(X0,X1,X2) | ~model_max(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_max(X0,X1,X3))) & ((model_max(X0,X1,X2) & ! [X4 : $int] : (~$less(X4,X2) | ~model_max(X0,X1,X4))) | ~minsol_model_max(X0,X1,X2)))),
% 112.94/17.05 inference(rectify,[],[f38])).
% 112.94/17.05 tff(f40,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_max(X0,X1,X2) | ~model_max(X0,X1,X2) | ($less(sK0(X0,X1,X2),X2) & model_max(X0,X1,sK0(X0,X1,X2)))) & ((model_max(X0,X1,X2) & ! [X4 : $int] : (~$less(X4,X2) | ~model_max(X0,X1,X4))) | ~minsol_model_max(X0,X1,X2)))),
% 112.94/17.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f39])).
% 112.94/17.05 tff(f41,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_ub(X0,X1,X2) | (~model_ub(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_ub(X0,X1,X3)))) & ((model_ub(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_ub(X0,X1,X3))) | ~minsol_model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f30])).
% 112.94/17.05 tff(f42,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_ub(X0,X1,X3))) & ((model_ub(X0,X1,X2) & ! [X3 : $int] : (~$less(X3,X2) | ~model_ub(X0,X1,X3))) | ~minsol_model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(flattening,[],[f41])).
% 112.94/17.05 tff(f43,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | ? [X3 : $int] : ($less(X3,X2) & model_ub(X0,X1,X3))) & ((model_ub(X0,X1,X2) & ! [X4 : $int] : (~$less(X4,X2) | ~model_ub(X0,X1,X4))) | ~minsol_model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(rectify,[],[f42])).
% 112.94/17.05 tff(f44,plain,(
% 112.94/17.05 ! [X0 : $int,X1 : $int,X2 : $int] : ((minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | ($less(sK1(X0,X1,X2),X2) & model_ub(X0,X1,sK1(X0,X1,X2)))) & ((model_ub(X0,X1,X2) & ! [X4 : $int] : (~$less(X4,X2) | ~model_ub(X0,X1,X4))) | ~minsol_model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f43])).
% 112.94/17.05 tff(f45,plain,(
% 112.94/17.05 ? [X0 : $int,X1 : $int,X2 : $int] : ((~minsol_model_max(X0,X1,X2) | ~minsol_model_ub(X0,X1,X2)) & (minsol_model_max(X0,X1,X2) | minsol_model_ub(X0,X1,X2)))),
% 112.94/17.05 inference(nnf_transformation,[],[f31])).
% 112.94/17.05 tff(f46,plain,(
% 112.94/17.05 (~minsol_model_max(sK2,sK3,sK4) | ~minsol_model_ub(sK2,sK3,sK4)) & (minsol_model_max(sK2,sK3,sK4) | minsol_model_ub(sK2,sK3,sK4))),
% 112.94/17.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f45])).
% 112.94/17.05 tff(f49,plain,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | max(X0,X1) = X0) )),
% 112.94/17.05 inference(cnf_transformation,[],[f12])).
% 112.94/17.05 tff(f50,plain,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | max(X0,X1) = X1) )),
% 112.94/17.05 inference(cnf_transformation,[],[f13])).
% 112.94/17.05 tff(f51,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~ub(X0,X1,X2) | ~$less(X2,X1)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f34])).
% 112.94/17.05 tff(f52,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~ub(X0,X1,X2) | ~$less(X2,X0)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f34])).
% 112.94/17.05 tff(f53,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (ub(X0,X1,X2) | $less(X2,X0) | $less(X2,X1)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f34])).
% 112.94/17.05 tff(f54,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~model_max(X0,X1,X2) | max(X0,X1) = X2) )),
% 112.94/17.05 inference(cnf_transformation,[],[f35])).
% 112.94/17.05 tff(f55,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (model_max(X0,X1,X2) | max(X0,X1) != X2) )),
% 112.94/17.05 inference(cnf_transformation,[],[f35])).
% 112.94/17.05 tff(f56,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (ub(X0,X1,X2) | ~model_ub(X0,X1,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f36])).
% 112.94/17.05 tff(f57,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (model_ub(X0,X1,X2) | ~ub(X0,X1,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f36])).
% 112.94/17.05 tff(f58,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int,X4 : $int] : (~model_max(X0,X1,X4) | ~minsol_model_max(X0,X1,X2) | ~$less(X4,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f40])).
% 112.94/17.05 tff(f59,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (model_max(X0,X1,X2) | ~minsol_model_max(X0,X1,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f40])).
% 112.94/17.05 tff(f60,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (minsol_model_max(X0,X1,X2) | ~model_max(X0,X1,X2) | model_max(X0,X1,sK0(X0,X1,X2))) )),
% 112.94/17.05 inference(cnf_transformation,[],[f40])).
% 112.94/17.05 tff(f61,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (minsol_model_max(X0,X1,X2) | ~model_max(X0,X1,X2) | $less(sK0(X0,X1,X2),X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f40])).
% 112.94/17.05 tff(f62,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int,X4 : $int] : (~model_ub(X0,X1,X4) | ~minsol_model_ub(X0,X1,X2) | ~$less(X4,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f44])).
% 112.94/17.05 tff(f63,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~minsol_model_ub(X0,X1,X2) | model_ub(X0,X1,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f44])).
% 112.94/17.05 tff(f64,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (model_ub(X0,X1,sK1(X0,X1,X2)) | ~model_ub(X0,X1,X2) | minsol_model_ub(X0,X1,X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f44])).
% 112.94/17.05 tff(f65,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | $less(sK1(X0,X1,X2),X2)) )),
% 112.94/17.05 inference(cnf_transformation,[],[f44])).
% 112.94/17.05 tff(f66,plain,(
% 112.94/17.05 minsol_model_max(sK2,sK3,sK4) | minsol_model_ub(sK2,sK3,sK4)),
% 112.94/17.05 inference(cnf_transformation,[],[f46])).
% 112.94/17.05 tff(f67,plain,(
% 112.94/17.05 ~minsol_model_max(sK2,sK3,sK4) | ~minsol_model_ub(sK2,sK3,sK4)),
% 112.94/17.05 inference(cnf_transformation,[],[f46])).
% 112.94/17.05 tff(f68,plain,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : (model_max(X0,X1,max(X0,X1))) )),
% 112.94/17.05 inference(equality_resolution,[],[f55])).
% 112.94/17.05 tff(f70,definition,(
% 112.94/17.05 spl5_1 <=> minsol_model_ub(sK2,sK3,sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 112.94/17.05 tff(f71,plain,(
% 112.94/17.05 ~minsol_model_ub(sK2,sK3,sK4) | spl5_1),
% 112.94/17.05 inference(avatar_component_clause,[],[f70])).
% 112.94/17.05 tff(f72,plain,(
% 112.94/17.05 minsol_model_ub(sK2,sK3,sK4) | ~spl5_1),
% 112.94/17.05 inference(avatar_component_clause,[],[f70])).
% 112.94/17.05 tff(f74,definition,(
% 112.94/17.05 spl5_2 <=> minsol_model_max(sK2,sK3,sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 112.94/17.05 tff(f75,plain,(
% 112.94/17.05 ~minsol_model_max(sK2,sK3,sK4) | spl5_2),
% 112.94/17.05 inference(avatar_component_clause,[],[f74])).
% 112.94/17.05 tff(f76,plain,(
% 112.94/17.05 minsol_model_max(sK2,sK3,sK4) | ~spl5_2),
% 112.94/17.05 inference(avatar_component_clause,[],[f74])).
% 112.94/17.05 tff(f77,plain,(
% 112.94/17.05 spl5_1 | spl5_2),
% 112.94/17.05 inference(avatar_split_clause,[],[f66,f74,f70])).
% 112.94/17.05 tff(f78,plain,(
% 112.94/17.05 ~spl5_1 | ~spl5_2),
% 112.94/17.05 inference(avatar_split_clause,[],[f67,f74,f70])).
% 112.94/17.05 tff(f108,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~model_ub(X0,X1,X2) | ~$less(X2,X0)) )),
% 112.94/17.05 inference(resolution,[],[f56,f52])).
% 112.94/17.05 tff(f109,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~model_ub(X0,X1,X2) | ~$less(X2,X1)) )),
% 112.94/17.05 inference(resolution,[],[f56,f51])).
% 112.94/17.05 tff(f122,plain,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0)) )),
% 112.94/17.05 inference(resolution,[],[f23,f22])).
% 112.94/17.05 tff(f132,plain,(
% 112.94/17.05 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | max(X1,X0) = X0) )),
% 112.94/17.05 inference(resolution,[],[f122,f50])).
% 112.94/17.05 tff(f155,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~minsol_model_max(X0,X1,X2) | max(X0,X1) = X2) )),
% 112.94/17.05 inference(resolution,[],[f54,f59])).
% 112.94/17.05 tff(f266,plain,(
% 112.94/17.05 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~minsol_model_ub(X0,X1,X3) | ~ub(X0,X1,X2) | ~$less(X2,X3)) )),
% 112.94/17.05 inference(resolution,[],[f62,f57])).
% 112.94/17.05 tff(f273,plain,(
% 112.94/17.05 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($less(sK0(X0,X1,X2),X2) | ~model_max(X0,X1,X2) | ~model_max(X0,X1,X3) | ~$less(X3,X2)) )),
% 112.94/17.05 inference(resolution,[],[f61,f58])).
% 112.94/17.05 tff(f276,plain,(
% 112.94/17.05 ~model_ub(sK2,sK3,sK4) | $less(sK1(sK2,sK3,sK4),sK4) | spl5_1),
% 112.94/17.05 inference(resolution,[],[f65,f71])).
% 112.94/17.05 tff(f295,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | ~$less(sK1(X0,X1,X2),X1)) )),
% 112.94/17.05 inference(resolution,[],[f64,f109])).
% 112.94/17.05 tff(f296,plain,(
% 112.94/17.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (minsol_model_ub(X0,X1,X2) | ~model_ub(X0,X1,X2) | ~$less(sK1(X0,X1,X2),X0)) )),
% 112.94/17.05 inference(resolution,[],[f64,f108])).
% 112.94/17.05 tff(f304,definition,(
% 112.94/17.05 spl5_3 <=> $less(sK1(sK2,sK3,sK4),sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 112.94/17.05 tff(f306,plain,(
% 112.94/17.05 $less(sK1(sK2,sK3,sK4),sK4) | ~spl5_3),
% 112.94/17.05 inference(avatar_component_clause,[],[f304])).
% 112.94/17.05 tff(f308,definition,(
% 112.94/17.05 spl5_4 <=> model_ub(sK2,sK3,sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 112.94/17.05 tff(f309,plain,(
% 112.94/17.05 model_ub(sK2,sK3,sK4) | ~spl5_4),
% 112.94/17.05 inference(avatar_component_clause,[],[f308])).
% 112.94/17.05 tff(f310,plain,(
% 112.94/17.05 ~model_ub(sK2,sK3,sK4) | spl5_4),
% 112.94/17.05 inference(avatar_component_clause,[],[f308])).
% 112.94/17.05 tff(f311,plain,(
% 112.94/17.05 spl5_3 | ~spl5_4 | spl5_1),
% 112.94/17.05 inference(avatar_split_clause,[],[f276,f70,f308,f304])).
% 112.94/17.05 tff(f912,definition,(
% 112.94/17.05 spl5_5 <=> sK4 = max(sK2,sK3)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 112.94/17.05 tff(f913,plain,(
% 112.94/17.05 sK4 != max(sK2,sK3) | spl5_5),
% 112.94/17.05 inference(avatar_component_clause,[],[f912])).
% 112.94/17.05 tff(f914,plain,(
% 112.94/17.05 sK4 = max(sK2,sK3) | ~spl5_5),
% 112.94/17.05 inference(avatar_component_clause,[],[f912])).
% 112.94/17.05 tff(f921,plain,(
% 112.94/17.05 model_ub(sK2,sK3,sK4) | ~spl5_1),
% 112.94/17.05 inference(resolution,[],[f72,f63])).
% 112.94/17.05 tff(f922,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK4) | model_max(sK2,sK3,sK0(sK2,sK3,sK4)) | spl5_2),
% 112.94/17.05 inference(resolution,[],[f75,f60])).
% 112.94/17.05 tff(f923,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK4) | $less(sK0(sK2,sK3,sK4),sK4) | spl5_2),
% 112.94/17.05 inference(resolution,[],[f75,f61])).
% 112.94/17.05 tff(f924,plain,(
% 112.94/17.05 spl5_4 | ~spl5_1),
% 112.94/17.05 inference(avatar_split_clause,[],[f921,f70,f308])).
% 112.94/17.05 tff(f925,plain,(
% 112.94/17.05 ~$less(sK4,sK3) | ~spl5_4),
% 112.94/17.05 inference(resolution,[],[f309,f109])).
% 112.94/17.05 tff(f926,plain,(
% 112.94/17.05 ~$less(sK4,sK2) | ~spl5_4),
% 112.94/17.05 inference(resolution,[],[f309,f108])).
% 112.94/17.05 tff(f940,definition,(
% 112.94/17.05 spl5_7 <=> $less(sK0(sK2,sK3,sK4),sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 112.94/17.05 tff(f942,plain,(
% 112.94/17.05 $less(sK0(sK2,sK3,sK4),sK4) | ~spl5_7),
% 112.94/17.05 inference(avatar_component_clause,[],[f940])).
% 112.94/17.05 tff(f944,definition,(
% 112.94/17.05 spl5_8 <=> model_max(sK2,sK3,sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 112.94/17.05 tff(f946,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK4) | spl5_8),
% 112.94/17.05 inference(avatar_component_clause,[],[f944])).
% 112.94/17.05 tff(f947,plain,(
% 112.94/17.05 spl5_7 | ~spl5_8 | spl5_2),
% 112.94/17.05 inference(avatar_split_clause,[],[f923,f74,f944,f940])).
% 112.94/17.05 tff(f952,plain,(
% 112.94/17.05 sK4 = max(sK2,sK4) | ~spl5_4),
% 112.94/17.05 inference(resolution,[],[f926,f50])).
% 112.94/17.05 tff(f968,definition,(
% 112.94/17.05 spl5_9 <=> model_max(sK2,sK3,sK0(sK2,sK3,sK4))),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 112.94/17.05 tff(f970,plain,(
% 112.94/17.05 model_max(sK2,sK3,sK0(sK2,sK3,sK4)) | ~spl5_9),
% 112.94/17.05 inference(avatar_component_clause,[],[f968])).
% 112.94/17.05 tff(f971,plain,(
% 112.94/17.05 spl5_9 | ~spl5_8 | spl5_2),
% 112.94/17.05 inference(avatar_split_clause,[],[f922,f74,f944,f968])).
% 112.94/17.05 tff(f1101,plain,(
% 112.94/17.05 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~minsol_model_ub(X0,X1,X3) | ~$less(X2,X3) | $less(X2,X0) | $less(X2,X1)) )),
% 112.94/17.05 inference(resolution,[],[f266,f53])).
% 112.94/17.05 tff(f1232,plain,(
% 112.94/17.05 model_max(sK2,sK4,sK4) | ~spl5_4),
% 112.94/17.05 inference(superposition,[],[f68,f952])).
% 112.94/17.05 tff(f1588,definition,(
% 112.94/17.05 spl5_10 <=> sK3 = sK4),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 112.94/17.05 tff(f1589,plain,(
% 112.94/17.05 sK3 != sK4 | spl5_10),
% 112.94/17.05 inference(avatar_component_clause,[],[f1588])).
% 112.94/17.05 tff(f1590,plain,(
% 112.94/17.05 sK3 = sK4 | ~spl5_10),
% 112.94/17.05 inference(avatar_component_clause,[],[f1588])).
% 112.94/17.05 tff(f1592,definition,(
% 112.94/17.05 spl5_11 <=> $less(sK3,sK4)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 112.94/17.05 tff(f1594,plain,(
% 112.94/17.05 $less(sK3,sK4) | ~spl5_11),
% 112.94/17.05 inference(avatar_component_clause,[],[f1592])).
% 112.94/17.05 tff(f1607,plain,(
% 112.94/17.05 ~ub(sK2,sK3,sK4) | spl5_4),
% 112.94/17.05 inference(resolution,[],[f310,f57])).
% 112.94/17.05 tff(f1613,plain,(
% 112.94/17.05 $less(sK4,sK2) | $less(sK4,sK3) | spl5_4),
% 112.94/17.05 inference(resolution,[],[f1607,f53])).
% 112.94/17.05 tff(f1638,definition,(
% 112.94/17.05 spl5_12 <=> $less(sK4,sK3)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 112.94/17.05 tff(f1639,plain,(
% 112.94/17.05 ~$less(sK4,sK3) | spl5_12),
% 112.94/17.05 inference(avatar_component_clause,[],[f1638])).
% 112.94/17.05 tff(f1640,plain,(
% 112.94/17.05 $less(sK4,sK3) | ~spl5_12),
% 112.94/17.05 inference(avatar_component_clause,[],[f1638])).
% 112.94/17.05 tff(f1642,definition,(
% 112.94/17.05 spl5_13 <=> $less(sK4,sK2)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition])).
% 112.94/17.05 tff(f1643,plain,(
% 112.94/17.05 ~$less(sK4,sK2) | spl5_13),
% 112.94/17.05 inference(avatar_component_clause,[],[f1642])).
% 112.94/17.05 tff(f1644,plain,(
% 112.94/17.05 $less(sK4,sK2) | ~spl5_13),
% 112.94/17.05 inference(avatar_component_clause,[],[f1642])).
% 112.94/17.05 tff(f1645,plain,(
% 112.94/17.05 spl5_12 | spl5_13 | spl5_4),
% 112.94/17.05 inference(avatar_split_clause,[],[f1613,f308,f1642,f1638])).
% 112.94/17.05 tff(f1648,plain,(
% 112.94/17.05 ~spl5_12 | ~spl5_4),
% 112.94/17.05 inference(avatar_split_clause,[],[f925,f308,f1638])).
% 112.94/17.05 tff(f1656,plain,(
% 112.94/17.05 ~spl5_13 | ~spl5_4),
% 112.94/17.05 inference(avatar_split_clause,[],[f926,f308,f1642])).
% 112.94/17.05 tff(f1663,plain,(
% 112.94/17.05 ~minsol_model_ub(sK2,sK3,sK3) | (spl5_1 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f71,f1590])).
% 112.94/17.05 tff(f1665,plain,(
% 112.94/17.05 $less(sK1(sK2,sK3,sK3),sK3) | (~spl5_3 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f306,f1590])).
% 112.94/17.05 tff(f1666,plain,(
% 112.94/17.05 model_ub(sK2,sK3,sK3) | (~spl5_4 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f309,f1590])).
% 112.94/17.05 tff(f1679,plain,(
% 112.94/17.05 $less(sK0(sK2,sK3,sK3),sK3) | (~spl5_7 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f942,f1590])).
% 112.94/17.05 tff(f1753,plain,(
% 112.94/17.05 model_max(sK2,sK3,sK3) | (~spl5_4 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f1232,f1590])).
% 112.94/17.05 tff(f2519,definition,(
% 112.94/17.05 spl5_15 <=> $less(sK2,sK3)),
% 112.94/17.05 introduced(definition,[new_symbols(definition,[spl5_15])],[avatar_definition])).
% 112.94/17.05 tff(f2520,plain,(
% 112.94/17.05 ~$less(sK2,sK3) | spl5_15),
% 112.94/17.05 inference(avatar_component_clause,[],[f2519])).
% 112.94/17.05 tff(f2521,plain,(
% 112.94/17.05 $less(sK2,sK3) | ~spl5_15),
% 112.94/17.05 inference(avatar_component_clause,[],[f2519])).
% 112.94/17.05 tff(f2525,plain,(
% 112.94/17.05 $less(sK3,sK2) | (~spl5_10 | ~spl5_13)),
% 112.94/17.05 inference(forward_demodulation,[],[f1644,f1590])).
% 112.94/17.05 tff(f2531,plain,(
% 112.94/17.05 ~$less(sK2,sK3) | (~spl5_10 | ~spl5_13)),
% 112.94/17.05 inference(resolution,[],[f2525,f122])).
% 112.94/17.05 tff(f2541,plain,(
% 112.94/17.05 ~spl5_15 | ~spl5_10 | ~spl5_13),
% 112.94/17.05 inference(avatar_split_clause,[],[f2531,f1642,f1588,f2519])).
% 112.94/17.05 tff(f2580,plain,(
% 112.94/17.05 sK2 = max(sK2,sK3) | spl5_15),
% 112.94/17.05 inference(resolution,[],[f2520,f49])).
% 112.94/17.05 tff(f3363,plain,(
% 112.94/17.05 $less(sK4,sK2) | $less(sK4,sK3) | spl5_4),
% 112.94/17.05 inference(resolution,[],[f1607,f53])).
% 112.94/17.05 tff(f3366,plain,(
% 112.94/17.05 $less(sK3,sK4) | sK3 = sK4 | spl5_12),
% 112.94/17.05 inference(resolution,[],[f1639,f24])).
% 112.94/17.05 tff(f3374,plain,(
% 112.94/17.05 $less(sK3,sK4) | (spl5_10 | spl5_12)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f3366,f1589])).
% 112.94/17.05 tff(f3509,plain,(
% 112.94/17.05 spl5_11 | spl5_10 | spl5_12),
% 112.94/17.05 inference(avatar_split_clause,[],[f3374,f1638,f1588,f1592])).
% 112.94/17.05 tff(f4457,plain,(
% 112.94/17.05 sK2 = sK4 | (~spl5_5 | spl5_15)),
% 112.94/17.05 inference(superposition,[],[f914,f2580])).
% 112.94/17.05 tff(f4458,plain,(
% 112.94/17.05 model_max(sK2,sK3,sK2) | spl5_15),
% 112.94/17.05 inference(superposition,[],[f68,f2580])).
% 112.94/17.05 tff(f4527,plain,(
% 112.94/17.05 $less(sK1(sK2,sK3,sK2),sK2) | (~spl5_3 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(superposition,[],[f306,f4457])).
% 112.94/17.05 tff(f4567,plain,(
% 112.94/17.05 $less(sK2,sK2) | $less(sK4,sK3) | (spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f3363,f4457])).
% 112.94/17.05 tff(f4572,plain,(
% 112.94/17.05 $less(sK4,sK3) | (spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f4567,f22])).
% 112.94/17.05 tff(f4573,plain,(
% 112.94/17.05 $less(sK2,sK3) | (spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f4572,f4457])).
% 112.94/17.05 tff(f4574,plain,(
% 112.94/17.05 $false | (spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f4573,f2520])).
% 112.94/17.05 tff(f4575,plain,(
% 112.94/17.05 spl5_4 | ~spl5_5 | spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f4574])).
% 112.94/17.05 tff(f4576,plain,(
% 112.94/17.05 model_ub(sK2,sK3,sK2) | (~spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f309,f4457])).
% 112.94/17.05 tff(f16351,plain,(
% 112.94/17.05 ~model_ub(sK2,sK3,sK4) | ~$less(sK1(sK2,sK3,sK4),sK2) | spl5_1),
% 112.94/17.05 inference(resolution,[],[f296,f71])).
% 112.94/17.05 tff(f16355,plain,(
% 112.94/17.05 ~model_ub(sK2,sK3,sK2) | ~$less(sK1(sK2,sK3,sK4),sK2) | (spl5_1 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f16351,f4457])).
% 112.94/17.05 tff(f16358,plain,(
% 112.94/17.05 ~$less(sK1(sK2,sK3,sK4),sK2) | (spl5_1 | ~spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16355,f4576])).
% 112.94/17.05 tff(f16359,plain,(
% 112.94/17.05 ~$less(sK1(sK2,sK3,sK2),sK2) | (spl5_1 | ~spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f16358,f4457])).
% 112.94/17.05 tff(f16360,plain,(
% 112.94/17.05 $false | (spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16359,f4527])).
% 112.94/17.05 tff(f16361,plain,(
% 112.94/17.05 spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_5 | spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f16360])).
% 112.94/17.05 tff(f16364,plain,(
% 112.94/17.05 ~minsol_model_max(sK2,sK3,sK2) | (spl5_2 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f75,f4457])).
% 112.94/17.05 tff(f16365,plain,(
% 112.94/17.05 model_max(sK2,sK3,sK0(sK2,sK3,sK2)) | (~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f970,f4457])).
% 112.94/17.05 tff(f16370,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK2) | $less(sK0(sK2,sK3,sK2),sK2) | (spl5_2 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(resolution,[],[f16364,f61])).
% 112.94/17.05 tff(f16409,plain,(
% 112.94/17.05 max(sK2,sK3) = sK0(sK2,sK3,sK2) | (~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(resolution,[],[f16365,f54])).
% 112.94/17.05 tff(f16410,plain,(
% 112.94/17.05 sK4 = sK0(sK2,sK3,sK2) | (~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f16409,f914])).
% 112.94/17.05 tff(f16411,plain,(
% 112.94/17.05 sK2 = sK0(sK2,sK3,sK2) | (~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f16410,f4457])).
% 112.94/17.05 tff(f16425,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK2) | (~spl5_5 | spl5_8 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f946,f4457])).
% 112.94/17.05 tff(f16428,plain,(
% 112.94/17.05 $less(sK0(sK2,sK3,sK2),sK2) | (spl5_2 | ~spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16370,f4458])).
% 112.94/17.05 tff(f16430,plain,(
% 112.94/17.05 $false | (~spl5_5 | spl5_8 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16425,f4458])).
% 112.94/17.05 tff(f16431,plain,(
% 112.94/17.05 ~spl5_5 | spl5_8 | spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f16430])).
% 112.94/17.05 tff(f16432,plain,(
% 112.94/17.05 $less(sK2,sK2) | (spl5_2 | ~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f16428,f16411])).
% 112.94/17.05 tff(f16433,plain,(
% 112.94/17.05 $false | (spl5_2 | ~spl5_5 | ~spl5_9 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16432,f22])).
% 112.94/17.05 tff(f16434,plain,(
% 112.94/17.05 spl5_2 | ~spl5_5 | ~spl5_9 | spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f16433])).
% 112.94/17.05 tff(f16435,plain,(
% 112.94/17.05 sK2 != sK4 | (spl5_5 | spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f913,f2580])).
% 112.94/17.05 tff(f16448,plain,(
% 112.94/17.05 ( ! [X0 : $int] : (~$less(X0,sK4) | $less(X0,sK2) | $less(X0,sK3)) ) | ~spl5_1),
% 112.94/17.05 inference(resolution,[],[f72,f1101])).
% 112.94/17.05 tff(f16473,plain,(
% 112.94/17.05 $less(sK2,sK4) | sK2 = sK4 | spl5_13),
% 112.94/17.05 inference(resolution,[],[f1643,f24])).
% 112.94/17.05 tff(f16487,plain,(
% 112.94/17.05 $less(sK2,sK4) | (spl5_5 | spl5_13 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f16473,f16435])).
% 112.94/17.05 tff(f131083,plain,(
% 112.94/17.05 $less(sK2,sK2) | $less(sK2,sK3) | (~spl5_1 | spl5_5 | spl5_13 | spl5_15)),
% 112.94/17.05 inference(resolution,[],[f16448,f16487])).
% 112.94/17.05 tff(f131085,plain,(
% 112.94/17.05 $less(sK2,sK3) | (~spl5_1 | spl5_5 | spl5_13 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131083,f22])).
% 112.94/17.05 tff(f131093,plain,(
% 112.94/17.05 $false | (~spl5_1 | spl5_5 | spl5_13 | spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131085,f2520])).
% 112.94/17.05 tff(f131094,plain,(
% 112.94/17.05 ~spl5_1 | spl5_5 | spl5_13 | spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131093])).
% 112.94/17.05 tff(f131195,plain,(
% 112.94/17.05 sK4 = max(sK2,sK3) | ~spl5_2),
% 112.94/17.05 inference(resolution,[],[f76,f155])).
% 112.94/17.05 tff(f131206,plain,(
% 112.94/17.05 $false | (~spl5_2 | spl5_5)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131195,f913])).
% 112.94/17.05 tff(f131207,plain,(
% 112.94/17.05 ~spl5_2 | spl5_5),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131206])).
% 112.94/17.05 tff(f131209,plain,(
% 112.94/17.05 ( ! [X0 : $int] : (~$less(X0,sK4) | $less(X0,sK2) | $less(X0,sK3)) ) | ~spl5_1),
% 112.94/17.05 inference(resolution,[],[f72,f1101])).
% 112.94/17.05 tff(f131246,plain,(
% 112.94/17.05 sK3 = max(sK2,sK3) | ~spl5_15),
% 112.94/17.05 inference(resolution,[],[f2521,f132])).
% 112.94/17.05 tff(f131492,plain,(
% 112.94/17.05 $less(sK3,sK2) | $less(sK3,sK3) | (~spl5_1 | ~spl5_11)),
% 112.94/17.05 inference(resolution,[],[f131209,f1594])).
% 112.94/17.05 tff(f131493,plain,(
% 112.94/17.05 $less(sK3,sK2) | (~spl5_1 | ~spl5_11)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131492,f22])).
% 112.94/17.05 tff(f131508,plain,(
% 112.94/17.05 ~$less(sK2,sK3) | (~spl5_1 | ~spl5_11)),
% 112.94/17.05 inference(resolution,[],[f131493,f122])).
% 112.94/17.05 tff(f131551,plain,(
% 112.94/17.05 $false | (~spl5_1 | ~spl5_11 | ~spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131508,f2521])).
% 112.94/17.05 tff(f131552,plain,(
% 112.94/17.05 ~spl5_1 | ~spl5_11 | ~spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131551])).
% 112.94/17.05 tff(f131587,plain,(
% 112.94/17.05 ~model_max(sK2,sK3,sK3) | (spl5_8 | ~spl5_10)),
% 112.94/17.05 inference(superposition,[],[f946,f1590])).
% 112.94/17.05 tff(f131604,plain,(
% 112.94/17.05 $false | (~spl5_4 | spl5_8 | ~spl5_10)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131587,f1753])).
% 112.94/17.05 tff(f131605,plain,(
% 112.94/17.05 ~spl5_4 | spl5_8 | ~spl5_10),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131604])).
% 112.94/17.05 tff(f131616,plain,(
% 112.94/17.05 model_max(sK2,sK3,sK0(sK2,sK3,sK3)) | (~spl5_9 | ~spl5_10)),
% 112.94/17.05 inference(forward_demodulation,[],[f970,f1590])).
% 112.94/17.05 tff(f131661,plain,(
% 112.94/17.05 max(sK2,sK3) = sK0(sK2,sK3,sK3) | (~spl5_9 | ~spl5_10)),
% 112.94/17.05 inference(resolution,[],[f131616,f54])).
% 112.94/17.05 tff(f131684,plain,(
% 112.94/17.05 sK3 = sK0(sK2,sK3,sK3) | (~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f131661,f131246])).
% 112.94/17.05 tff(f131704,plain,(
% 112.94/17.05 ( ! [X0 : $int] : ($less(sK3,sK3) | ~model_max(sK2,sK3,sK3) | ~model_max(sK2,sK3,X0) | ~$less(X0,sK3)) ) | (~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(superposition,[],[f273,f131684])).
% 112.94/17.05 tff(f131705,plain,(
% 112.94/17.05 ( ! [X0 : $int] : (~model_max(sK2,sK3,sK3) | ~model_max(sK2,sK3,X0) | ~$less(X0,sK3)) ) | (~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131704,f22])).
% 112.94/17.05 tff(f131707,plain,(
% 112.94/17.05 ( ! [X0 : $int] : (~model_max(sK2,sK3,X0) | ~$less(X0,sK3)) ) | (~spl5_4 | ~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131705,f1753])).
% 112.94/17.05 tff(f131719,plain,(
% 112.94/17.05 ~$less(sK0(sK2,sK3,sK3),sK3) | (~spl5_4 | ~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(resolution,[],[f131707,f131616])).
% 112.94/17.05 tff(f131727,plain,(
% 112.94/17.05 $false | (~spl5_4 | ~spl5_7 | ~spl5_9 | ~spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131719,f1679])).
% 112.94/17.05 tff(f131728,plain,(
% 112.94/17.05 ~spl5_4 | ~spl5_7 | ~spl5_9 | ~spl5_10 | ~spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131727])).
% 112.94/17.05 tff(f131732,plain,(
% 112.94/17.05 sK3 = sK4 | (~spl5_5 | ~spl5_15)),
% 112.94/17.05 inference(forward_demodulation,[],[f914,f131246])).
% 112.94/17.05 tff(f131744,plain,(
% 112.94/17.05 ~model_ub(sK2,sK3,sK3) | ~$less(sK1(sK2,sK3,sK3),sK3) | (spl5_1 | ~spl5_10)),
% 112.94/17.05 inference(resolution,[],[f1663,f295])).
% 112.94/17.05 tff(f131748,plain,(
% 112.94/17.05 ~$less(sK1(sK2,sK3,sK3),sK3) | (spl5_1 | ~spl5_4 | ~spl5_10)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131744,f1666])).
% 112.94/17.05 tff(f131750,plain,(
% 112.94/17.05 $false | (spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_10)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131748,f1665])).
% 112.94/17.05 tff(f131751,plain,(
% 112.94/17.05 spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_10),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131750])).
% 112.94/17.05 tff(f131758,plain,(
% 112.94/17.05 $false | (~spl5_5 | spl5_10 | ~spl5_15)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131732,f1589])).
% 112.94/17.05 tff(f131759,plain,(
% 112.94/17.05 ~spl5_5 | spl5_10 | ~spl5_15),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131758])).
% 112.94/17.05 tff(f131764,plain,(
% 112.94/17.05 $less(sK3,sK3) | (~spl5_10 | ~spl5_12)),
% 112.94/17.05 inference(forward_demodulation,[],[f1640,f1590])).
% 112.94/17.05 tff(f131767,plain,(
% 112.94/17.05 $false | (~spl5_10 | ~spl5_12)),
% 112.94/17.05 inference(forward_subsumption_resolution,[],[f131764,f22])).
% 112.94/17.05 tff(f131768,plain,(
% 112.94/17.05 ~spl5_10 | ~spl5_12),
% 112.94/17.05 inference(avatar_contradiction_clause,[],[f131767])).
% 112.94/17.05 cnf(s1, plain, spl5_1 | spl5_2, inference(sat_conversion,[],[f77])).
% 112.94/17.05 cnf(s2, plain, ~spl5_1 | ~spl5_2, inference(sat_conversion,[],[f78])).
% 112.94/17.05 cnf(s3, plain, spl5_1 | spl5_3 | ~spl5_4, inference(sat_conversion,[],[f311])).
% 112.94/17.05 cnf(s5, plain, ~spl5_1 | spl5_4, inference(sat_conversion,[],[f924])).
% 112.94/17.05 cnf(s6, plain, spl5_2 | spl5_7 | ~spl5_8, inference(sat_conversion,[],[f947])).
% 112.94/17.05 cnf(s7, plain, spl5_2 | ~spl5_8 | spl5_9, inference(sat_conversion,[],[f971])).
% 112.94/17.05 cnf(s11, plain, spl5_4 | spl5_12 | spl5_13, inference(sat_conversion,[],[f1645])).
% 112.94/17.05 cnf(s12, plain, ~spl5_4 | ~spl5_12, inference(sat_conversion,[],[f1648])).
% 112.94/17.05 cnf(s13, plain, ~spl5_4 | ~spl5_13, inference(sat_conversion,[],[f1656])).
% 112.94/17.05 cnf(s15, plain, ~spl5_10 | ~spl5_13 | ~spl5_15, inference(sat_conversion,[],[f2541])).
% 112.94/17.05 cnf(s20, plain, spl5_10 | spl5_11 | spl5_12, inference(sat_conversion,[],[f3509])).
% 112.94/17.05 cnf(s23, plain, spl5_4 | ~spl5_5 | spl5_15, inference(sat_conversion,[],[f4575])).
% 112.94/17.05 cnf(s25, plain, spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_5 | spl5_15, inference(sat_conversion,[],[f16361])).
% 112.94/17.05 cnf(s27, plain, ~spl5_5 | spl5_8 | spl5_15, inference(sat_conversion,[],[f16431])).
% 112.94/17.05 cnf(s28, plain, spl5_2 | ~spl5_5 | ~spl5_9 | spl5_15, inference(sat_conversion,[],[f16434])).
% 112.94/17.05 cnf(s31, plain, ~spl5_1 | spl5_5 | spl5_13 | spl5_15, inference(sat_conversion,[],[f131094])).
% 112.94/17.05 cnf(s36, plain, ~spl5_2 | spl5_5, inference(sat_conversion,[],[f131207])).
% 112.94/17.05 cnf(s40, plain, ~spl5_1 | ~spl5_11 | ~spl5_15, inference(sat_conversion,[],[f131552])).
% 112.94/17.05 cnf(s41, plain, ~spl5_4 | spl5_8 | ~spl5_10, inference(sat_conversion,[],[f131605])).
% 112.94/17.05 cnf(s45, plain, ~spl5_4 | ~spl5_7 | ~spl5_9 | ~spl5_10 | ~spl5_15, inference(sat_conversion,[],[f131728])).
% 112.94/17.05 cnf(s46, plain, spl5_1 | ~spl5_3 | ~spl5_4 | ~spl5_10, inference(sat_conversion,[],[f131751])).
% 112.94/17.05 cnf(s47, plain, ~spl5_5 | spl5_10 | ~spl5_15, inference(sat_conversion,[],[f131759])).
% 112.94/17.05 cnf(s48, plain, ~spl5_10 | ~spl5_12, inference(sat_conversion,[],[f131768])).
% 112.94/17.05 cnf(s50, plain, spl5_4 | ~spl5_5, inference(rat,[],[s11,s15,s48,s47,s23])).
% 112.94/17.05 cnf(s51, plain, spl5_1, inference(rat,[],[s47,s25,s46,s3,s50,s36,s1])).
% 112.94/17.05 cnf(s52, plain, spl5_4, inference(rat,[],[s5,s51])).
% 112.94/17.05 cnf(s53, plain, ~spl5_2, inference(rat,[],[s2,s51])).
% 112.94/17.05 cnf(s54, plain, ~spl5_13, inference(rat,[],[s13,s52])).
% 112.94/17.05 cnf(s55, plain, ~spl5_12, inference(rat,[],[s12,s52])).
% 112.94/17.05 cnf(s56, plain, ~spl5_10 | ~spl5_5, inference(rat,[],[s28,s45,s6,s7,s41,s53,s52])).
% 112.94/17.05 cnf(s57, plain, spl5_15 | ~spl5_5, inference(rat,[],[s7,s27,s28,s53])).
% 112.94/17.05 cnf(s58, plain, spl5_10 | ~spl5_5, inference(rat,[],[s57,s47])).
% 112.94/17.05 cnf(s59, plain, ~spl5_5, inference(rat,[],[s58,s56])).
% 112.94/17.05 cnf(s60, plain, spl5_15, inference(rat,[],[s31,s51,s54,s59])).
% 112.94/17.05 cnf(s61, plain, ~spl5_11, inference(rat,[],[s40,s51,s60])).
% 112.94/17.05 cnf(s62, plain, spl5_10, inference(rat,[],[s20,s55,s61])).
% 112.94/17.05 cnf(s63, plain, spl5_8, inference(rat,[],[s41,s52,s62])).
% 112.94/17.05 cnf(s65, plain, spl5_9, inference(rat,[],[s7,s53,s63])).
% 112.94/17.05 cnf(s66, plain, spl5_7, inference(rat,[],[s6,s53,s63])).
% 112.94/17.05 cnf(s67, plain, $false, inference(rat,[],[s45,s60,s52,s62,s66,s65])).
% 112.94/17.05 tff(f131771,plain,(
% 112.94/17.05 $false),
% 112.94/17.05 inference(avatar_sat_refutation,[],[s67])).
% 112.94/17.05 % SZS output end Proof for theBenchmark
% 112.94/17.05 % (3224784)------------------------------
% 112.94/17.05 % (3224784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.94/17.05 % (3224784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.94/17.05 % (3224784)CaDiCaL version: 2.1.3
% 112.94/17.05 % (3224784)Termination reason: Refutation
% 112.94/17.05 % (3224784)Time elapsed: 8.484 s
% 112.94/17.05 % (3224784)Peak memory usage: 58 MB
% 112.94/17.05 % (3224784)Instructions burned: 13175 (million)
% 112.94/17.05 % (3224693)Success in time 16.609 s
% 112.94/17.05 % Vampire exiting
%------------------------------------------------------------------------------