%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX105_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 01:46:29 PM UTC 2026
% Result : Theorem 21.82s 3.38s
% Output : Refutation 21.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX105_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n020.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 15:02:34 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.94/0.87 % (226273)Will run a generic schedule for satisfiability detection.
% 3.94/0.87 % (226279)% WARNING: option uhcvi not known.
% 3.94/0.87 % (226279)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3322491068:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.94/0.87 % (226278)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3598331323_2999 on theBenchmark for (2999ds/0Mi)
% 3.94/0.87 % (226280)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=141953307:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.94/0.87 % (226281)dis+10_1_sil=32000:sp=arity:random_seed=3279184671:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.94/0.87 % (226283)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3636665531:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.94/0.87 % (226282)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1263887424:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.94/0.87 % (226284)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1230827467:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.94/0.87 % (226278)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.94/0.87 % (226278)Terminated due to inappropriate strategy.
% 3.94/0.87 % (226278)------------------------------
% 3.94/0.87 % (226278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.87 % (226278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.87 % (226278)CaDiCaL version: 2.1.3
% 3.94/0.87 % (226278)Termination reason: Inappropriate
% 3.94/0.87 % (226278)Time elapsed: 0.001 s
% 3.94/0.87 % (226278)Peak memory usage: 10 MB
% 3.94/0.87 % (226278)Instructions burned: 1 (million)
% 3.94/0.87 % (226278)------------------------------
% 3.94/0.87 % (226278)------------------------------
% 3.94/0.87 % (226292)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2268911222:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.94/0.87 % (226292)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.94/0.87 % (226292)Terminated due to inappropriate strategy.
% 3.94/0.87 % (226292)------------------------------
% 3.94/0.87 % (226292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.87 % (226292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.87 % (226292)CaDiCaL version: 2.1.3
% 3.94/0.87 % (226292)Termination reason: Inappropriate
% 3.94/0.87 % (226292)Time elapsed: 0.001 s
% 3.94/0.87 % (226292)Peak memory usage: 10 MB
% 3.94/0.87 % (226292)Instructions burned: 1 (million)
% 3.94/0.87 % (226292)------------------------------
% 3.94/0.87 % (226292)------------------------------
% 3.94/0.87 % (226294)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3997448436:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.94/0.87 % (226281)Instruction limit reached!
% 3.94/0.87 % (226281)------------------------------
% 3.94/0.87 % (226281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.87 % (226281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.87 % (226281)CaDiCaL version: 2.1.3
% 3.94/0.87 % (226281)Termination reason: Instruction limit
% 3.94/0.87 % (226281)Termination phase: Saturation
% 3.94/0.87 % (226281)Time elapsed: 0.063 s
% 3.94/0.87 % (226281)Peak memory usage: 12 MB
% 3.94/0.87 % (226281)Instructions burned: 104 (million)
% 3.94/0.87 % (226282)Instruction limit reached!
% 3.94/0.87 % (226282)------------------------------
% 3.94/0.87 % (226282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.87 % (226282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.87 % (226282)CaDiCaL version: 2.1.3
% 3.94/0.87 % (226282)Termination reason: Instruction limit
% 3.94/0.87 % (226282)Termination phase: Saturation
% 3.94/0.87 % (226282)Time elapsed: 0.071 s
% 3.94/0.87 % (226282)Peak memory usage: 12 MB
% 3.94/0.87 % (226282)Instructions burned: 119 (million)
% 3.94/0.87 % (226296)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=2294951053:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.94/0.87 % (226283)Instruction limit reached!
% 3.94/0.87 % (226283)------------------------------
% 3.94/0.87 % (226283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226283)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226283)Termination reason: Instruction limit
% 7.92/1.42 % (226283)Termination phase: Saturation
% 7.92/1.42 % (226283)Time elapsed: 0.083 s
% 7.92/1.42 % (226283)Peak memory usage: 13 MB
% 7.92/1.42 % (226283)Instructions burned: 132 (million)
% 7.92/1.42 % (226297)ott-21_1_sil=16000:fs=off:random_seed=4028959705:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.92/1.42 % (226284)Instruction limit reached!
% 7.92/1.42 % (226284)------------------------------
% 7.92/1.42 % (226284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226284)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226284)Termination reason: Instruction limit
% 7.92/1.42 % (226284)Termination phase: Saturation
% 7.92/1.42 % (226284)Time elapsed: 0.094 s
% 7.92/1.42 % (226284)Peak memory usage: 13 MB
% 7.92/1.42 % (226284)Instructions burned: 161 (million)
% 7.92/1.42 % (226299)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1172273383:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.92/1.42 % (226301)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=467086600:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.92/1.42 % (226301)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.92/1.42 % (226301)Terminated due to inappropriate strategy.
% 7.92/1.42 % (226301)------------------------------
% 7.92/1.42 % (226301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226301)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226301)Termination reason: Inappropriate
% 7.92/1.42 % (226301)Time elapsed: 0.001 s
% 7.92/1.42 % (226301)Peak memory usage: 10 MB
% 7.92/1.42 % (226301)Instructions burned: 1 (million)
% 7.92/1.42 % (226301)------------------------------
% 7.92/1.42 % (226301)------------------------------
% 7.92/1.42 % (226294)Instruction limit reached!
% 7.92/1.42 % (226294)------------------------------
% 7.92/1.42 % (226294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226294)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226294)Termination reason: Instruction limit
% 7.92/1.42 % (226294)Termination phase: Saturation
% 7.92/1.42 % (226294)Time elapsed: 0.089 s
% 7.92/1.42 % (226294)Peak memory usage: 13 MB
% 7.92/1.42 % (226294)Instructions burned: 132 (million)
% 7.92/1.42 % (226304)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3062805307:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.92/1.42 % (226305)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2596943981:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.92/1.42 % (226305)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.92/1.42 % (226305)Terminated due to inappropriate strategy.
% 7.92/1.42 % (226305)------------------------------
% 7.92/1.42 % (226305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226305)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226305)Termination reason: Inappropriate
% 7.92/1.42 % (226305)Time elapsed: 0.001 s
% 7.92/1.42 % (226305)Peak memory usage: 10 MB
% 7.92/1.42 % (226305)Instructions burned: 1 (million)
% 7.92/1.42 % (226305)------------------------------
% 7.92/1.42 % (226305)------------------------------
% 7.92/1.42 % (226308)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=835854775: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)
% 7.92/1.42 % (226297)Instruction limit reached!
% 7.92/1.42 % (226297)------------------------------
% 7.92/1.42 % (226297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.92/1.42 % (226297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.92/1.42 % (226297)CaDiCaL version: 2.1.3
% 7.92/1.42 % (226297)Termination reason: Instruction limit
% 7.92/1.42 % (226297)Termination phase: Saturation
% 7.92/1.42 % (226297)Time elapsed: 0.081 s
% 7.92/1.42 % (226297)Peak memory usage: 12 MB
% 7.92/1.42 % (226297)Instructions burned: 180 (million)
% 21.82/3.38 % (226310)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1808640232:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 21.82/3.38 % (226299)Instruction limit reached!
% 21.82/3.38 % (226299)------------------------------
% 21.82/3.38 % (226299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226299)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226299)Termination reason: Instruction limit
% 21.82/3.38 % (226299)Termination phase: Saturation
% 21.82/3.38 % (226299)Time elapsed: 0.295 s
% 21.82/3.38 % (226299)Peak memory usage: 14 MB
% 21.82/3.38 % (226299)Instructions burned: 479 (million)
% 21.82/3.38 % (226312)fmb+10_1_sil=64000:random_seed=959657405:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 21.82/3.38 % (226312)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226312)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226312)------------------------------
% 21.82/3.38 % (226312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226312)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226312)Termination reason: Inappropriate
% 21.82/3.38 % (226312)Time elapsed: 0.001 s
% 21.82/3.38 % (226312)Peak memory usage: 10 MB
% 21.82/3.38 % (226312)Instructions burned: 1 (million)
% 21.82/3.38 % (226312)------------------------------
% 21.82/3.38 % (226312)------------------------------
% 21.82/3.38 % (226314)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1732032453:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 21.82/3.38 % (226314)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226314)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226314)------------------------------
% 21.82/3.38 % (226314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226314)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226314)Termination reason: Inappropriate
% 21.82/3.38 % (226314)Time elapsed: 0.001 s
% 21.82/3.38 % (226314)Peak memory usage: 10 MB
% 21.82/3.38 % (226314)Instructions burned: 1 (million)
% 21.82/3.38 % (226314)------------------------------
% 21.82/3.38 % (226314)------------------------------
% 21.82/3.38 % (226296)Instruction limit reached!
% 21.82/3.38 % (226296)------------------------------
% 21.82/3.38 % (226296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226296)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226296)Termination reason: Instruction limit
% 21.82/3.38 % (226296)Termination phase: Saturation
% 21.82/3.38 % (226296)Time elapsed: 0.376 s
% 21.82/3.38 % (226296)Peak memory usage: 16 MB
% 21.82/3.38 % (226296)Instructions burned: 685 (million)
% 21.82/3.38 % (226316)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1136892225:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 21.82/3.38 % (226316)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226316)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226316)------------------------------
% 21.82/3.38 % (226316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226316)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226316)Termination reason: Inappropriate
% 21.82/3.38 % (226316)Time elapsed: 0.001 s
% 21.82/3.38 % (226316)Peak memory usage: 10 MB
% 21.82/3.38 % (226316)Instructions burned: 1 (million)
% 21.82/3.38 % (226316)------------------------------
% 21.82/3.38 % (226316)------------------------------
% 21.82/3.38 % (226317)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2046906096:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 21.82/3.38 % (226319)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1467617410:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 21.82/3.38 % (226308)Instruction limit reached!
% 21.82/3.38 % (226308)------------------------------
% 21.82/3.38 % (226308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226308)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226308)Termination reason: Instruction limit
% 21.82/3.38 % (226308)Termination phase: Saturation
% 21.82/3.38 % (226308)Time elapsed: 0.434 s
% 21.82/3.38 % (226308)Peak memory usage: 18 MB
% 21.82/3.38 % (226308)Instructions burned: 693 (million)
% 21.82/3.38 % (226322)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=210610502:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 21.82/3.38 % (226322)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226322)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226322)------------------------------
% 21.82/3.38 % (226322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226322)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226322)Termination reason: Inappropriate
% 21.82/3.38 % (226322)Time elapsed: 0.001 s
% 21.82/3.38 % (226322)Peak memory usage: 10 MB
% 21.82/3.38 % (226322)Instructions burned: 1 (million)
% 21.82/3.38 % (226322)------------------------------
% 21.82/3.38 % (226322)------------------------------
% 21.82/3.38 % (226324)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3274766909:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 21.82/3.38 % (226324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226324)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226324)------------------------------
% 21.82/3.38 % (226324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226324)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226324)Termination reason: Inappropriate
% 21.82/3.38 % (226324)Time elapsed: 0.001 s
% 21.82/3.38 % (226324)Peak memory usage: 10 MB
% 21.82/3.38 % (226324)Instructions burned: 1 (million)
% 21.82/3.38 % (226324)------------------------------
% 21.82/3.38 % (226324)------------------------------
% 21.82/3.38 % (226326)ott-2_1_sil=16000:newcnf=on:random_seed=590730114:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 21.82/3.38 % (226310)Instruction limit reached!
% 21.82/3.38 % (226310)------------------------------
% 21.82/3.38 % (226310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226310)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226310)Termination reason: Instruction limit
% 21.82/3.38 % (226310)Termination phase: Saturation
% 21.82/3.38 % (226310)Time elapsed: 0.506 s
% 21.82/3.38 % (226310)Peak memory usage: 19 MB
% 21.82/3.38 % (226310)Instructions burned: 881 (million)
% 21.82/3.38 % (226304)Instruction limit reached!
% 21.82/3.38 % (226304)------------------------------
% 21.82/3.38 % (226304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226304)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226304)Termination reason: Instruction limit
% 21.82/3.38 % (226304)Termination phase: Saturation
% 21.82/3.38 % (226304)Time elapsed: 0.580 s
% 21.82/3.38 % (226304)Peak memory usage: 17 MB
% 21.82/3.38 % (226304)Instructions burned: 1181 (million)
% 21.82/3.38 % (226328)ott+10_1_sil=32000:tgt=ground:random_seed=1616501878:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 21.82/3.38 % (226329)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=495698296:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 21.82/3.38 % (226329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226329)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226329)------------------------------
% 21.82/3.38 % (226329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226329)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226329)Termination reason: Inappropriate
% 21.82/3.38 % (226329)Time elapsed: 0.001 s
% 21.82/3.38 % (226329)Peak memory usage: 10 MB
% 21.82/3.38 % (226329)Instructions burned: 1 (million)
% 21.82/3.38 % (226329)------------------------------
% 21.82/3.38 % (226329)------------------------------
% 21.82/3.38 % (226332)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1380697767:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 21.82/3.38 % (226326)Instruction limit reached!
% 21.82/3.38 % (226326)------------------------------
% 21.82/3.38 % (226326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226326)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226326)Termination reason: Instruction limit
% 21.82/3.38 % (226326)Termination phase: Saturation
% 21.82/3.38 % (226326)Time elapsed: 0.487 s
% 21.82/3.38 % (226326)Peak memory usage: 17 MB
% 21.82/3.38 % (226326)Instructions burned: 871 (million)
% 21.82/3.38 % (226319)Instruction limit reached!
% 21.82/3.38 % (226319)------------------------------
% 21.82/3.38 % (226319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226319)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226319)Termination reason: Instruction limit
% 21.82/3.38 % (226319)Termination phase: Saturation
% 21.82/3.38 % (226319)Time elapsed: 0.685 s
% 21.82/3.38 % (226319)Peak memory usage: 25 MB
% 21.82/3.38 % (226319)Instructions burned: 1473 (million)
% 21.82/3.38 % (226334)dis+21_1_sil=32000:sas=cadical:random_seed=300103201:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 21.82/3.38 % (226335)ott+11_1_sil=16000:gs=on:random_seed=564401514:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 21.82/3.38 % (226335)Instruction limit reached!
% 21.82/3.38 % (226335)------------------------------
% 21.82/3.38 % (226335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226335)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226335)Termination reason: Instruction limit
% 21.82/3.38 % (226335)Termination phase: Saturation
% 21.82/3.38 % (226335)Time elapsed: 1.240 s
% 21.82/3.38 % (226335)Peak memory usage: 24 MB
% 21.82/3.38 % (226335)Instructions burned: 2252 (million)
% 21.82/3.38 % (226338)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2280036698:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi)
% 21.82/3.38 % (226338)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.82/3.38 % (226338)Terminated due to inappropriate strategy.
% 21.82/3.38 % (226338)------------------------------
% 21.82/3.38 % (226338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226338)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226338)Termination reason: Inappropriate
% 21.82/3.38 % (226338)Time elapsed: 0.001 s
% 21.82/3.38 % (226338)Peak memory usage: 10 MB
% 21.82/3.38 % (226338)Instructions burned: 1 (million)
% 21.82/3.38 % (226338)------------------------------
% 21.82/3.38 % (226338)------------------------------
% 21.82/3.38 % (226340)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=939917856:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi)
% 21.82/3.38 % (226332)Instruction limit reached!
% 21.82/3.38 % (226332)------------------------------
% 21.82/3.38 % (226332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226332)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226332)Termination reason: Instruction limit
% 21.82/3.38 % (226332)Termination phase: Saturation
% 21.82/3.38 % (226332)Time elapsed: 1.834 s
% 21.82/3.38 % (226332)Peak memory usage: 29 MB
% 21.82/3.38 % (226332)Instructions burned: 3513 (million)
% 21.82/3.38 % (226342)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1905734590:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 21.82/3.38 % (226328) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-226273-226328"...
% 21.82/3.38 % (226328)...printing done.
% 21.82/3.38 % (226328)Refutation found. Thanks to Tanya!
% 21.82/3.38 % SZS status Theorem for theBenchmark
% 21.82/3.38 % SZS output start Proof for theBenchmark
% 21.82/3.38 tff(type_def_5, type, general: $tType).
% 21.82/3.38 tff(type_def_6, type, symbol: $tType).
% 21.82/3.38 tff(func_def_0, type, f__integer__: $int > general).
% 21.82/3.38 tff(func_def_1, type, f__symbolic__: symbol > general).
% 21.82/3.38 tff(func_def_2, type, c__infimum__: general).
% 21.82/3.38 tff(func_def_3, type, c__supremum__: general).
% 21.82/3.38 tff(func_def_4, type, n_i: $int).
% 21.82/3.38 tff(func_def_11, type, sK0: general > $int).
% 21.82/3.38 tff(func_def_12, type, sK1: general > symbol).
% 21.82/3.38 tff(func_def_13, type, sK2: $int).
% 21.82/3.38 tff(func_def_14, type, sF3: $int).
% 21.82/3.38 tff(func_def_15, type, sF4: $int).
% 21.82/3.38 tff(func_def_16, type, sF5: $int).
% 21.82/3.38 tff(pred_def_1, type, p__is_integer__: general > $o).
% 21.82/3.38 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 21.82/3.38 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 21.82/3.38 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 21.82/3.38 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 21.82/3.38 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 21.82/3.38 tff(pred_def_8, type, p: general > $o).
% 21.82/3.38 tff(f17,conjecture,(
% 21.82/3.38 ! [X0 : $int] : $product(X0,X0) = $product($uminus(X0),$uminus(X0))),
% 21.82/3.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_unnamed_formula)).
% 21.82/3.38 tff(f18,negated_conjecture,(
% 21.82/3.38 ~ ! [X0 : $int] : $product(X0,X0) = $product($uminus(X0),$uminus(X0))),
% 21.82/3.38 inference(negated_conjecture,[status(cth)],[f17])).
% 21.82/3.38 tff(f21,definition,(
% 21.82/3.38 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 21.82/3.38 introduced(theory,[tha_commutativity])).
% 21.82/3.38 tff(f25,definition,(
% 21.82/3.38 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 21.82/3.38 introduced(theory,[tha_inverse_op_unit])).
% 21.82/3.38 tff(f28,definition,(
% 21.82/3.38 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 21.82/3.38 introduced(theory,[tha_order_totality])).
% 21.82/3.38 tff(f29,definition,(
% 21.82/3.38 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 21.82/3.38 introduced(theory,[tha_order_monotonicity])).
% 21.82/3.38 tff(f32,definition,(
% 21.82/3.38 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 21.82/3.38 introduced(theory,[tha_commutativity])).
% 21.82/3.38 tff(f36,definition,(
% 21.82/3.38 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 21.82/3.38 introduced(theory,[tha_distributivity])).
% 21.82/3.38 tff(f50,plain,(
% 21.82/3.38 ? [X0 : $int] : $product(X0,X0) != $product($uminus(X0),$uminus(X0))),
% 21.82/3.38 inference(ennf_transformation,[],[f18])).
% 21.82/3.38 tff(f56,plain,(
% 21.82/3.38 $product(sK2,sK2) != $product($uminus(sK2),$uminus(sK2))),
% 21.82/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f50])).
% 21.82/3.38 tff(f74,plain,(
% 21.82/3.38 $product(sK2,sK2) != $product($uminus(sK2),$uminus(sK2))),
% 21.82/3.38 inference(cnf_transformation,[],[f56])).
% 21.82/3.38 tff(f79,definition,(
% 21.82/3.38 sF3 = $product(sK2,sK2)),
% 21.82/3.38 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 21.82/3.38 tff(f80,plain,(
% 21.82/3.38 $product(sK2,sK2) = sF3),
% 21.82/3.38 inference(reorient_equations,[],[f79])).
% 21.82/3.38 tff(f81,definition,(
% 21.82/3.38 sF4 = $uminus(sK2)),
% 21.82/3.38 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 21.82/3.38 tff(f82,plain,(
% 21.82/3.38 $uminus(sK2) = sF4),
% 21.82/3.38 inference(reorient_equations,[],[f81])).
% 21.82/3.38 tff(f83,definition,(
% 21.82/3.38 sF5 = $product(sF4,sF4)),
% 21.82/3.38 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 21.82/3.38 tff(f84,plain,(
% 21.82/3.38 $product(sF4,sF4) = sF5),
% 21.82/3.38 inference(reorient_equations,[],[f83])).
% 21.82/3.38 tff(f85,plain,(
% 21.82/3.38 sF3 != sF5),
% 21.82/3.38 inference(definition_folding,[],[f74,f84,f82,f82,f80])).
% 21.82/3.38 tff(f88,plain,(
% 21.82/3.38 0 = $sum(sK2,sF4)),
% 21.82/3.38 inference(superposition,[],[f25,f82])).
% 21.82/3.38 tff(f293,plain,(
% 21.82/3.38 ( ! [X0 : $int] : ($product(sK2,$sum(sK2,X0)) = $sum(sF3,$product(sK2,X0))) )),
% 21.82/3.38 inference(superposition,[],[f36,f80])).
% 21.82/3.38 tff(f301,plain,(
% 21.82/3.38 ( ! [X0 : $int] : ($product(sF4,$sum(X0,sF4)) = $sum($product(sF4,X0),sF5)) )),
% 21.82/3.38 inference(superposition,[],[f36,f84])).
% 21.82/3.38 tff(f309,plain,(
% 21.82/3.38 ( ! [X0 : $int] : ($sum(sF5,$product(sF4,X0)) = $product(sF4,$sum(X0,sF4))) )),
% 21.82/3.38 inference(forward_demodulation,[],[f301,f21])).
% 21.82/3.38 tff(f1442,plain,(
% 21.82/3.38 ( ! [X0 : $int,X1 : $int] : ($less($sum(X1,$product(sK2,X0)),$product(sK2,$sum(sK2,X0))) | ~$less(X1,sF3)) )),
% 21.82/3.38 inference(superposition,[],[f29,f293])).
% 21.82/3.38 tff(f1443,plain,(
% 21.82/3.38 ( ! [X0 : $int,X1 : $int] : ($less($product(sK2,$sum(sK2,X0)),$sum(X1,$product(sK2,X0))) | ~$less(sF3,X1)) )),
% 21.82/3.38 inference(superposition,[],[f29,f293])).
% 21.82/3.38 tff(f1502,plain,(
% 21.82/3.38 ( ! [X0 : $int] : ($product(sF4,$sum(X0,sF4)) = $sum(sF5,$product(X0,sF4))) )),
% 21.82/3.38 inference(superposition,[],[f309,f32])).
% 21.82/3.38 tff(f67572,plain,(
% 21.82/3.38 $less($product(sF4,$sum(sK2,sF4)),$product(sK2,$sum(sK2,sF4))) | ~$less(sF5,sF3)),
% 21.82/3.38 inference(superposition,[],[f1442,f1502])).
% 21.82/3.38 tff(f67664,plain,(
% 21.82/3.38 $less($product(sF4,0),$product(sK2,0)) | ~$less(sF5,sF3)),
% 21.82/3.38 inference(forward_demodulation,[],[f67572,f88])).
% 21.82/3.38 tff(f67665,plain,(
% 21.82/3.38 ~$less(sF5,sF3)),
% 21.82/3.38 inference(evaluation,[],[f67664])).
% 21.82/3.38 tff(f67718,plain,(
% 21.82/3.38 $less(sF3,sF5) | sF3 = sF5),
% 21.82/3.38 inference(resolution,[],[f67665,f28])).
% 21.82/3.38 tff(f67721,plain,(
% 21.82/3.38 $less(sF3,sF5)),
% 21.82/3.38 inference(forward_subsumption_resolution,[],[f67718,f85])).
% 21.82/3.38 tff(f67836,plain,(
% 21.82/3.38 $less($product(sK2,$sum(sK2,sF4)),$product(sF4,$sum(sK2,sF4))) | ~$less(sF3,sF5)),
% 21.82/3.38 inference(superposition,[],[f1443,f1502])).
% 21.82/3.38 tff(f67850,plain,(
% 21.82/3.38 $less($product(sK2,$sum(sK2,sF4)),$product(sF4,$sum(sK2,sF4)))),
% 21.82/3.38 inference(forward_subsumption_resolution,[],[f67836,f67721])).
% 21.82/3.38 tff(f67898,plain,(
% 21.82/3.38 $less($product(sK2,0),$product(sF4,0))),
% 21.82/3.38 inference(forward_demodulation,[],[f67850,f88])).
% 21.82/3.38 tff(f67899,plain,(
% 21.82/3.38 $false),
% 21.82/3.38 inference(evaluation,[],[f67898])).
% 21.82/3.38 % SZS output end Proof for theBenchmark
% 21.82/3.38 % (226328)------------------------------
% 21.82/3.38 % (226328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.82/3.38 % (226328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.82/3.38 % (226328)CaDiCaL version: 2.1.3
% 21.82/3.38 % (226328)Termination reason: Refutation
% 21.82/3.38 % (226328)Time elapsed: 2.369 s
% 21.82/3.38 % (226328)Peak memory usage: 30 MB
% 21.82/3.38 % (226328)Instructions burned: 3751 (million)
% 21.82/3.38 % (226273)Success in time 3.148 s
% 21.82/3.38 % Vampire exiting
%------------------------------------------------------------------------------