%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT053_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 09:48:02 AM UTC 2026
% Result : Theorem 6.80s 1.25s
% Output : Refutation 6.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT053_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n009.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 : Tue Sep 29 00:07:15 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.67/0.88 % (3620116)Will run a generic schedule for satisfiability detection.
% 3.67/0.88 % (3620129)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3248249902:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.67/0.88 % (3620126)% WARNING: option uhcvi not known.
% 3.67/0.88 % (3620125)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4145584131_2999 on theBenchmark for (2999ds/0Mi)
% 3.67/0.88 % (3620127)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=599762992:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.67/0.88 % (3620126)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2243676795:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.67/0.88 % (3620128)dis+10_1_sil=32000:sp=arity:random_seed=1027817800:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.67/0.88 % (3620131)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3369524870:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.67/0.88 % (3620130)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2929194463:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.67/0.88 % (3620125)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.67/0.88 % (3620125)Terminated due to inappropriate strategy.
% 3.67/0.88 % (3620125)------------------------------
% 3.67/0.88 % (3620125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.88 % (3620125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.88 % (3620125)CaDiCaL version: 2.1.3
% 3.67/0.88 % (3620125)Termination reason: Inappropriate
% 3.67/0.88 % (3620125)Time elapsed: 0.001 s
% 3.67/0.88 % (3620125)Peak memory usage: 10 MB
% 3.67/0.88 % (3620125)Instructions burned: 1 (million)
% 3.67/0.88 % (3620125)------------------------------
% 3.67/0.88 % (3620125)------------------------------
% 3.67/0.88 % (3620146)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=686674318:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.67/0.88 % (3620146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.67/0.88 % (3620146)Terminated due to inappropriate strategy.
% 3.67/0.88 % (3620146)------------------------------
% 3.67/0.88 % (3620146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.88 % (3620146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.88 % (3620146)CaDiCaL version: 2.1.3
% 3.67/0.88 % (3620146)Termination reason: Inappropriate
% 3.67/0.88 % (3620146)Time elapsed: 0.001 s
% 3.67/0.88 % (3620146)Peak memory usage: 10 MB
% 3.67/0.88 % (3620146)Instructions burned: 1 (million)
% 3.67/0.88 % (3620146)------------------------------
% 3.67/0.88 % (3620146)------------------------------
% 3.67/0.88 % (3620129)Instruction limit reached!
% 3.67/0.88 % (3620129)------------------------------
% 3.67/0.88 % (3620129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.88 % (3620129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.88 % (3620129)CaDiCaL version: 2.1.3
% 3.67/0.88 % (3620129)Termination reason: Instruction limit
% 3.67/0.88 % (3620129)Termination phase: Saturation
% 3.67/0.88 % (3620129)Time elapsed: 0.039 s
% 3.67/0.88 % (3620129)Peak memory usage: 13 MB
% 3.67/0.88 % (3620129)Instructions burned: 116 (million)
% 3.67/0.88 % (3620156)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=241626415:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.67/0.88 % (3620157)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=1085625777:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.67/0.88 % (3620128)Instruction limit reached!
% 3.67/0.88 % (3620128)------------------------------
% 3.67/0.88 % (3620128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.88 % (3620128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.88 % (3620128)CaDiCaL version: 2.1.3
% 3.67/0.88 % (3620128)Termination reason: Instruction limit
% 3.67/0.88 % (3620128)Termination phase: Saturation
% 3.67/0.88 % (3620128)Time elapsed: 0.065 s
% 3.67/0.88 % (3620128)Peak memory usage: 13 MB
% 3.67/0.88 % (3620128)Instructions burned: 104 (million)
% 3.67/0.88 % (3620130)Instruction limit reached!
% 3.67/0.88 % (3620130)------------------------------
% 3.67/0.88 % (3620130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620130)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620130)Termination reason: Instruction limit
% 6.37/1.17 % (3620130)Termination phase: Saturation
% 6.37/1.17 % (3620130)Time elapsed: 0.083 s
% 6.37/1.17 % (3620130)Peak memory usage: 13 MB
% 6.37/1.17 % (3620130)Instructions burned: 131 (million)
% 6.37/1.17 % (3620168)ott-21_1_sil=16000:fs=off:random_seed=330024536:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.37/1.17 % (3620177)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2034803660:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.37/1.17 % (3620131)Instruction limit reached!
% 6.37/1.17 % (3620131)------------------------------
% 6.37/1.17 % (3620131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620131)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620131)Termination reason: Instruction limit
% 6.37/1.17 % (3620131)Termination phase: Saturation
% 6.37/1.17 % (3620131)Time elapsed: 0.113 s
% 6.37/1.17 % (3620131)Peak memory usage: 14 MB
% 6.37/1.17 % (3620131)Instructions burned: 160 (million)
% 6.37/1.17 % (3620156)Instruction limit reached!
% 6.37/1.17 % (3620156)------------------------------
% 6.37/1.17 % (3620156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620156)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620156)Termination reason: Instruction limit
% 6.37/1.17 % (3620156)Termination phase: Saturation
% 6.37/1.17 % (3620156)Time elapsed: 0.088 s
% 6.37/1.17 % (3620156)Peak memory usage: 13 MB
% 6.37/1.17 % (3620156)Instructions burned: 131 (million)
% 6.37/1.17 % (3620186)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3997120423:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.37/1.17 % (3620186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.37/1.17 % (3620186)Terminated due to inappropriate strategy.
% 6.37/1.17 % (3620186)------------------------------
% 6.37/1.17 % (3620186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620186)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620186)Termination reason: Inappropriate
% 6.37/1.17 % (3620186)Time elapsed: 0.001 s
% 6.37/1.17 % (3620186)Peak memory usage: 10 MB
% 6.37/1.17 % (3620186)Instructions burned: 1 (million)
% 6.37/1.17 % (3620186)------------------------------
% 6.37/1.17 % (3620186)------------------------------
% 6.37/1.17 % (3620195)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3162568079:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.37/1.17 % (3620200)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1116783845:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.37/1.17 % (3620200)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.37/1.17 % (3620200)Terminated due to inappropriate strategy.
% 6.37/1.17 % (3620200)------------------------------
% 6.37/1.17 % (3620200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620200)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620200)Termination reason: Inappropriate
% 6.37/1.17 % (3620200)Time elapsed: 0.001 s
% 6.37/1.17 % (3620200)Peak memory usage: 10 MB
% 6.37/1.17 % (3620200)Instructions burned: 1 (million)
% 6.37/1.17 % (3620200)------------------------------
% 6.37/1.17 % (3620200)------------------------------
% 6.37/1.17 % (3620168)Instruction limit reached!
% 6.37/1.17 % (3620168)------------------------------
% 6.37/1.17 % (3620168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.17 % (3620168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.17 % (3620168)CaDiCaL version: 2.1.3
% 6.37/1.17 % (3620168)Termination reason: Instruction limit
% 6.37/1.17 % (3620168)Termination phase: Saturation
% 6.37/1.17 % (3620168)Time elapsed: 0.084 s
% 6.37/1.17 % (3620168)Peak memory usage: 12 MB
% 6.37/1.17 % (3620168)Instructions burned: 184 (million)
% 6.37/1.17 % (3620216)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=1759371899: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)
% 6.80/1.25 % (3620226)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2588606013:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 6.80/1.25 % (3620157)Instruction limit reached!
% 6.80/1.25 % (3620157)------------------------------
% 6.80/1.25 % (3620157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620157)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620157)Termination reason: Instruction limit
% 6.80/1.25 % (3620157)Termination phase: Saturation
% 6.80/1.25 % (3620157)Time elapsed: 0.218 s
% 6.80/1.25 % (3620157)Peak memory usage: 16 MB
% 6.80/1.25 % (3620157)Instructions burned: 685 (million)
% 6.80/1.25 % (3620235)fmb+10_1_sil=64000:random_seed=2170217961:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 6.80/1.25 % (3620235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620235)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620235)------------------------------
% 6.80/1.25 % (3620235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620235)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620235)Termination reason: Inappropriate
% 6.80/1.25 % (3620235)Time elapsed: 0.0000 s
% 6.80/1.25 % (3620235)Peak memory usage: 10 MB
% 6.80/1.25 % (3620235)Instructions burned: 1 (million)
% 6.80/1.25 % (3620235)------------------------------
% 6.80/1.25 % (3620235)------------------------------
% 6.80/1.25 % (3620237)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2975021750:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 6.80/1.25 % (3620237)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620237)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620237)------------------------------
% 6.80/1.25 % (3620237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620237)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620237)Termination reason: Inappropriate
% 6.80/1.25 % (3620237)Time elapsed: 0.0000 s
% 6.80/1.25 % (3620237)Peak memory usage: 10 MB
% 6.80/1.25 % (3620237)Instructions burned: 1 (million)
% 6.80/1.25 % (3620237)------------------------------
% 6.80/1.25 % (3620237)------------------------------
% 6.80/1.25 % (3620239)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3455052988:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 6.80/1.25 % (3620239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620239)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620239)------------------------------
% 6.80/1.25 % (3620239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620239)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620239)Termination reason: Inappropriate
% 6.80/1.25 % (3620239)Time elapsed: 0.0000 s
% 6.80/1.25 % (3620239)Peak memory usage: 10 MB
% 6.80/1.25 % (3620239)Instructions burned: 1 (million)
% 6.80/1.25 % (3620239)------------------------------
% 6.80/1.25 % (3620239)------------------------------
% 6.80/1.25 % (3620241)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1543567931:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 6.80/1.25 % (3620177)Instruction limit reached!
% 6.80/1.25 % (3620177)------------------------------
% 6.80/1.25 % (3620177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620177)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620177)Termination reason: Instruction limit
% 6.80/1.25 % (3620177)Termination phase: Saturation
% 6.80/1.25 % (3620177)Time elapsed: 0.317 s
% 6.80/1.25 % (3620177)Peak memory usage: 14 MB
% 6.80/1.25 % (3620177)Instructions burned: 477 (million)
% 6.80/1.25 % (3620243)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2331380091:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 6.80/1.25 % (3620216)Instruction limit reached!
% 6.80/1.25 % (3620216)------------------------------
% 6.80/1.25 % (3620216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620216)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620216)Termination reason: Instruction limit
% 6.80/1.25 % (3620216)Termination phase: Saturation
% 6.80/1.25 % (3620216)Time elapsed: 0.436 s
% 6.80/1.25 % (3620216)Peak memory usage: 18 MB
% 6.80/1.25 % (3620216)Instructions burned: 693 (million)
% 6.80/1.25 % (3620245)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1600739435:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 6.80/1.25 % (3620245)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620245)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620245)------------------------------
% 6.80/1.25 % (3620245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620245)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620245)Termination reason: Inappropriate
% 6.80/1.25 % (3620245)Time elapsed: 0.001 s
% 6.80/1.25 % (3620245)Peak memory usage: 10 MB
% 6.80/1.25 % (3620245)Instructions burned: 1 (million)
% 6.80/1.25 % (3620245)------------------------------
% 6.80/1.25 % (3620245)------------------------------
% 6.80/1.25 % (3620247)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2198434121:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 6.80/1.25 % (3620247)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620247)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620247)------------------------------
% 6.80/1.25 % (3620247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620247)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620247)Termination reason: Inappropriate
% 6.80/1.25 % (3620247)Time elapsed: 0.001 s
% 6.80/1.25 % (3620247)Peak memory usage: 10 MB
% 6.80/1.25 % (3620247)Instructions burned: 1 (million)
% 6.80/1.25 % (3620247)------------------------------
% 6.80/1.25 % (3620247)------------------------------
% 6.80/1.25 % (3620249)ott-2_1_sil=16000:newcnf=on:random_seed=4116974229:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 6.80/1.25 % (3620226)Instruction limit reached!
% 6.80/1.25 % (3620226)------------------------------
% 6.80/1.25 % (3620226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620226)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620226)Termination reason: Instruction limit
% 6.80/1.25 % (3620226)Termination phase: Saturation
% 6.80/1.25 % (3620226)Time elapsed: 0.503 s
% 6.80/1.25 % (3620226)Peak memory usage: 22 MB
% 6.80/1.25 % (3620226)Instructions burned: 880 (million)
% 6.80/1.25 % (3620251)ott+10_1_sil=32000:tgt=ground:random_seed=1480012624:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 6.80/1.25 % (3620195)Instruction limit reached!
% 6.80/1.25 % (3620195)------------------------------
% 6.80/1.25 % (3620195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620195)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620195)Termination reason: Instruction limit
% 6.80/1.25 % (3620195)Termination phase: Saturation
% 6.80/1.25 % (3620195)Time elapsed: 0.725 s
% 6.80/1.25 % (3620195)Peak memory usage: 19 MB
% 6.80/1.25 % (3620195)Instructions burned: 1179 (million)
% 6.80/1.25 % (3620253)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=854672111:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 6.80/1.25 % (3620253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.80/1.25 % (3620253)Terminated due to inappropriate strategy.
% 6.80/1.25 % (3620253)------------------------------
% 6.80/1.25 % (3620253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620253)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620253)Termination reason: Inappropriate
% 6.80/1.25 % (3620253)Time elapsed: 0.001 s
% 6.80/1.25 % (3620253)Peak memory usage: 10 MB
% 6.80/1.25 % (3620253)Instructions burned: 1 (million)
% 6.80/1.25 % (3620253)------------------------------
% 6.80/1.25 % (3620253)------------------------------
% 6.80/1.25 % (3620255)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=998490760:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 6.80/1.25 % (3620251) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3620116-3620251"...
% 6.80/1.25 % (3620251)...printing done.
% 6.80/1.25 % (3620251)Refutation found. Thanks to Tanya!
% 6.80/1.25 % SZS status Theorem for theBenchmark
% 6.80/1.25 % SZS output start Proof for theBenchmark
% 6.80/1.25 tff(type_def_5, type, record: $tType).
% 6.80/1.25 tff(func_def_0, type, length: record > $int).
% 6.80/1.25 tff(func_def_1, type, next: record > record).
% 6.80/1.25 tff(func_def_2, type, data: record > $int).
% 6.80/1.25 tff(func_def_3, type, split1: record > record).
% 6.80/1.25 tff(func_def_4, type, split2: record > record).
% 6.80/1.25 tff(func_def_8, type, a: record).
% 6.80/1.25 tff(func_def_9, type, b: record).
% 6.80/1.25 tff(func_def_13, type, sF0: record).
% 6.80/1.25 tff(func_def_14, type, sF1: $int).
% 6.80/1.25 tff(func_def_15, type, sF2: $int).
% 6.80/1.25 tff(func_def_16, type, sF3: $int).
% 6.80/1.25 tff(func_def_17, type, sF4: $int).
% 6.80/1.25 tff(func_def_18, type, sF5: record).
% 6.80/1.25 tff(func_def_19, type, sF6: record).
% 6.80/1.25 tff(func_def_20, type, sF7: record).
% 6.80/1.25 tff(func_def_21, type, sF8: $int).
% 6.80/1.25 tff(func_def_22, type, sF9: $int).
% 6.80/1.25 tff(func_def_23, type, sF10: $int).
% 6.80/1.25 tff(func_def_24, type, sF11: $int).
% 6.80/1.25 tff(pred_def_1, type, isrecord: record > $o).
% 6.80/1.25 tff(f3,axiom,(
% 6.80/1.25 ! [X0 : record] : (isrecord(X0) => length(X0) = $sum(length(next(X0)),1))),
% 6.80/1.25 file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax3)).
% 6.80/1.25 tff(f5,axiom,(
% 6.80/1.25 ! [X0 : record] : (isrecord(X0) => isrecord(split1(X0)))),
% 6.80/1.25 file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax5)).
% 6.80/1.25 tff(f8,axiom,(
% 6.80/1.25 ! [X0 : record] : ((isrecord(X0) & isrecord(next(X0))) => next(split1(X0)) = split1(next(next(X0))))),
% 6.80/1.25 file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax8)).
% 6.80/1.25 tff(f14,conjecture,(
% 6.80/1.25 (isrecord(b) & isrecord(next(b)) & next(next(b)) = a & ($product(2,length(split1(a))) = $sum(length(a),1) | $product(2,length(split1(a))) = length(a))) => ($product(2,length(split1(b))) = $sum(length(b),1) | $product(2,length(split1(b))) = length(b))),
% 6.80/1.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1)).
% 6.80/1.25 tff(f15,negated_conjecture,(
% 6.80/1.25 ~((isrecord(b) & isrecord(next(b)) & next(next(b)) = a & ($product(2,length(split1(a))) = $sum(length(a),1) | $product(2,length(split1(a))) = length(a))) => ($product(2,length(split1(b))) = $sum(length(b),1) | $product(2,length(split1(b))) = length(b)))),
% 6.80/1.25 inference(negated_conjecture,[status(cth)],[f14])).
% 6.80/1.25 tff(f17,definition,(
% 6.80/1.25 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 6.80/1.25 introduced(theory,[tha_commutativity])).
% 6.80/1.25 tff(f18,definition,(
% 6.80/1.25 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 6.80/1.25 introduced(theory,[tha_associativity])).
% 6.80/1.25 tff(f21,definition,(
% 6.80/1.25 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 6.80/1.25 introduced(theory,[tha_inverse_op_unit])).
% 6.80/1.25 tff(f32,definition,(
% 6.80/1.25 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 6.80/1.25 introduced(theory,[tha_distributivity])).
% 6.80/1.25 tff(f37,plain,(
% 6.80/1.25 ! [X0 : record] : (length(X0) = $sum(length(next(X0)),1) | ~isrecord(X0))),
% 6.80/1.25 inference(ennf_transformation,[],[f3])).
% 6.80/1.25 tff(f39,plain,(
% 6.80/1.25 ! [X0 : record] : (isrecord(split1(X0)) | ~isrecord(X0))),
% 6.80/1.25 inference(ennf_transformation,[],[f5])).
% 6.80/1.25 tff(f43,plain,(
% 6.80/1.25 ! [X0 : record] : (next(split1(X0)) = split1(next(next(X0))) | (~isrecord(X0) | ~isrecord(next(X0))))),
% 6.80/1.25 inference(ennf_transformation,[],[f8])).
% 6.80/1.25 tff(f44,plain,(
% 6.80/1.25 ! [X0 : record] : (next(split1(X0)) = split1(next(next(X0))) | ~isrecord(X0) | ~isrecord(next(X0)))),
% 6.80/1.25 inference(flattening,[],[f43])).
% 6.80/1.25 tff(f53,plain,(
% 6.80/1.25 ($product(2,length(split1(b))) != $sum(length(b),1) & $product(2,length(split1(b))) != length(b)) & (isrecord(b) & isrecord(next(b)) & next(next(b)) = a & ($product(2,length(split1(a))) = $sum(length(a),1) | $product(2,length(split1(a))) = length(a)))),
% 6.80/1.25 inference(ennf_transformation,[],[f15])).
% 6.80/1.25 tff(f54,plain,(
% 6.80/1.25 $product(2,length(split1(b))) != $sum(length(b),1) & $product(2,length(split1(b))) != length(b) & isrecord(b) & isrecord(next(b)) & next(next(b)) = a & ($product(2,length(split1(a))) = $sum(length(a),1) | $product(2,length(split1(a))) = length(a))),
% 6.80/1.25 inference(flattening,[],[f53])).
% 6.80/1.25 tff(f57,plain,(
% 6.80/1.25 ( ! [X0 : record] : (~isrecord(X0) | length(X0) = $sum(length(next(X0)),1)) )),
% 6.80/1.25 inference(cnf_transformation,[],[f37])).
% 6.80/1.25 tff(f59,plain,(
% 6.80/1.25 ( ! [X0 : record] : (isrecord(split1(X0)) | ~isrecord(X0)) )),
% 6.80/1.25 inference(cnf_transformation,[],[f39])).
% 6.80/1.25 tff(f62,plain,(
% 6.80/1.25 ( ! [X0 : record] : (~isrecord(next(X0)) | ~isrecord(X0) | next(split1(X0)) = split1(next(next(X0)))) )),
% 6.80/1.25 inference(cnf_transformation,[],[f44])).
% 6.80/1.25 tff(f68,plain,(
% 6.80/1.25 $product(2,length(split1(a))) = $sum(length(a),1) | $product(2,length(split1(a))) = length(a)),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f69,plain,(
% 6.80/1.25 next(next(b)) = a),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f70,plain,(
% 6.80/1.25 isrecord(next(b))),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f71,plain,(
% 6.80/1.25 isrecord(b)),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f72,plain,(
% 6.80/1.25 $product(2,length(split1(b))) != length(b)),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f73,plain,(
% 6.80/1.25 $product(2,length(split1(b))) != $sum(length(b),1)),
% 6.80/1.25 inference(cnf_transformation,[],[f54])).
% 6.80/1.25 tff(f75,definition,(
% 6.80/1.25 sF0 = split1(b)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 6.80/1.25 tff(f76,plain,(
% 6.80/1.25 split1(b) = sF0),
% 6.80/1.25 inference(reorient_equations,[],[f75])).
% 6.80/1.25 tff(f77,definition,(
% 6.80/1.25 sF1 = length(sF0)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 6.80/1.25 tff(f78,plain,(
% 6.80/1.25 length(sF0) = sF1),
% 6.80/1.25 inference(reorient_equations,[],[f77])).
% 6.80/1.25 tff(f79,definition,(
% 6.80/1.25 sF2 = $product(2,sF1)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 6.80/1.25 tff(f80,plain,(
% 6.80/1.25 $product(2,sF1) = sF2),
% 6.80/1.25 inference(reorient_equations,[],[f79])).
% 6.80/1.25 tff(f81,definition,(
% 6.80/1.25 sF3 = length(b)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 6.80/1.25 tff(f82,plain,(
% 6.80/1.25 length(b) = sF3),
% 6.80/1.25 inference(reorient_equations,[],[f81])).
% 6.80/1.25 tff(f83,definition,(
% 6.80/1.25 sF4 = $sum(sF3,1)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 6.80/1.25 tff(f84,plain,(
% 6.80/1.25 $sum(sF3,1) = sF4),
% 6.80/1.25 inference(reorient_equations,[],[f83])).
% 6.80/1.25 tff(f85,plain,(
% 6.80/1.25 sF2 != sF4),
% 6.80/1.25 inference(definition_folding,[],[f73,f84,f82,f80,f78,f76])).
% 6.80/1.25 tff(f86,plain,(
% 6.80/1.25 sF2 != sF3),
% 6.80/1.25 inference(definition_folding,[],[f72,f82,f80,f78,f76])).
% 6.80/1.25 tff(f87,definition,(
% 6.80/1.25 sF5 = next(b)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 6.80/1.25 tff(f88,plain,(
% 6.80/1.25 next(b) = sF5),
% 6.80/1.25 inference(reorient_equations,[],[f87])).
% 6.80/1.25 tff(f89,plain,(
% 6.80/1.25 isrecord(sF5)),
% 6.80/1.25 inference(definition_folding,[],[f70,f88])).
% 6.80/1.25 tff(f90,definition,(
% 6.80/1.25 sF6 = next(sF5)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 6.80/1.25 tff(f91,plain,(
% 6.80/1.25 next(sF5) = sF6),
% 6.80/1.25 inference(reorient_equations,[],[f90])).
% 6.80/1.25 tff(f92,plain,(
% 6.80/1.25 a = sF6),
% 6.80/1.25 inference(definition_folding,[],[f69,f91,f88])).
% 6.80/1.25 tff(f93,definition,(
% 6.80/1.25 sF7 = split1(a)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 6.80/1.25 tff(f94,plain,(
% 6.80/1.25 split1(a) = sF7),
% 6.80/1.25 inference(reorient_equations,[],[f93])).
% 6.80/1.25 tff(f95,definition,(
% 6.80/1.25 sF8 = length(sF7)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 6.80/1.25 tff(f96,plain,(
% 6.80/1.25 length(sF7) = sF8),
% 6.80/1.25 inference(reorient_equations,[],[f95])).
% 6.80/1.25 tff(f97,definition,(
% 6.80/1.25 sF9 = $product(2,sF8)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 6.80/1.25 tff(f98,plain,(
% 6.80/1.25 $product(2,sF8) = sF9),
% 6.80/1.25 inference(reorient_equations,[],[f97])).
% 6.80/1.25 tff(f99,definition,(
% 6.80/1.25 sF10 = length(a)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 6.80/1.25 tff(f100,plain,(
% 6.80/1.25 length(a) = sF10),
% 6.80/1.25 inference(reorient_equations,[],[f99])).
% 6.80/1.25 tff(f101,definition,(
% 6.80/1.25 sF11 = $sum(sF10,1)),
% 6.80/1.25 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 6.80/1.25 tff(f102,plain,(
% 6.80/1.25 $sum(sF10,1) = sF11),
% 6.80/1.25 inference(reorient_equations,[],[f101])).
% 6.80/1.25 tff(f103,plain,(
% 6.80/1.25 sF9 = sF11 | sF9 = sF10),
% 6.80/1.25 inference(definition_folding,[],[f68,f100,f98,f96,f94,f102,f100,f98,f96,f94])).
% 6.80/1.25 tff(f104,plain,(
% 6.80/1.25 sF4 = $sum(1,sF3)),
% 6.80/1.25 inference(forward_demodulation,[],[f84,f17])).
% 6.80/1.25 tff(f105,plain,(
% 6.80/1.25 a = next(sF5)),
% 6.80/1.25 inference(forward_demodulation,[],[f91,f92])).
% 6.80/1.25 tff(f106,plain,(
% 6.80/1.25 sF11 = $sum(1,sF10)),
% 6.80/1.25 inference(forward_demodulation,[],[f102,f17])).
% 6.80/1.25 tff(f110,plain,(
% 6.80/1.25 isrecord(sF0) | ~isrecord(b)),
% 6.80/1.25 inference(superposition,[],[f59,f76])).
% 6.80/1.25 tff(f112,plain,(
% 6.80/1.25 isrecord(sF0)),
% 6.80/1.25 inference(forward_subsumption_resolution,[],[f110,f71])).
% 6.80/1.25 tff(f232,plain,(
% 6.80/1.25 length(b) = $sum(length(next(b)),1)),
% 6.80/1.25 inference(resolution,[],[f57,f71])).
% 6.80/1.25 tff(f233,plain,(
% 6.80/1.25 length(sF0) = $sum(length(next(sF0)),1)),
% 6.80/1.25 inference(resolution,[],[f57,f112])).
% 6.80/1.25 tff(f234,plain,(
% 6.80/1.25 length(sF5) = $sum(length(next(sF5)),1)),
% 6.80/1.25 inference(resolution,[],[f57,f89])).
% 6.80/1.25 tff(f235,plain,(
% 6.80/1.25 length(sF5) = $sum(1,length(next(sF5)))),
% 6.80/1.25 inference(forward_demodulation,[],[f234,f17])).
% 6.80/1.25 tff(f236,plain,(
% 6.80/1.25 length(sF0) = $sum(1,length(next(sF0)))),
% 6.80/1.25 inference(forward_demodulation,[],[f233,f17])).
% 6.80/1.25 tff(f237,plain,(
% 6.80/1.25 length(b) = $sum(1,length(next(b)))),
% 6.80/1.25 inference(forward_demodulation,[],[f232,f17])).
% 6.80/1.25 tff(f243,plain,(
% 6.80/1.25 length(sF5) = $sum(1,length(a))),
% 6.80/1.25 inference(forward_demodulation,[],[f235,f105])).
% 6.80/1.25 tff(f244,plain,(
% 6.80/1.25 sF1 = $sum(1,length(next(sF0)))),
% 6.80/1.25 inference(forward_demodulation,[],[f236,f78])).
% 6.80/1.25 tff(f245,plain,(
% 6.80/1.25 length(b) = $sum(1,length(sF5))),
% 6.80/1.25 inference(forward_demodulation,[],[f237,f88])).
% 6.80/1.25 tff(f247,plain,(
% 6.80/1.25 $sum(1,sF10) = length(sF5)),
% 6.80/1.25 inference(forward_demodulation,[],[f243,f100])).
% 6.80/1.25 tff(f248,plain,(
% 6.80/1.25 sF3 = $sum(1,length(sF5))),
% 6.80/1.25 inference(forward_demodulation,[],[f245,f82])).
% 6.80/1.25 tff(f249,plain,(
% 6.80/1.25 sF11 = length(sF5)),
% 6.80/1.25 inference(forward_demodulation,[],[f247,f106])).
% 6.80/1.25 tff(f253,plain,(
% 6.80/1.25 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 6.80/1.25 inference(superposition,[],[f18,f21])).
% 6.80/1.25 tff(f256,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($sum(1,$sum(sF3,X0)) = $sum(sF4,X0)) )),
% 6.80/1.25 inference(superposition,[],[f18,f104])).
% 6.80/1.25 tff(f257,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($sum(1,$sum(sF10,X0)) = $sum(sF11,X0)) )),
% 6.80/1.25 inference(superposition,[],[f18,f106])).
% 6.80/1.25 tff(f273,plain,(
% 6.80/1.25 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 6.80/1.25 inference(evaluation,[],[f253])).
% 6.80/1.25 tff(f297,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($sum(sF3,X0) = $sum(1,$sum(length(sF5),X0))) )),
% 6.80/1.25 inference(superposition,[],[f18,f248])).
% 6.80/1.25 tff(f302,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($sum(sF3,X0) = $sum(1,$sum(sF11,X0))) )),
% 6.80/1.25 inference(forward_demodulation,[],[f297,f249])).
% 6.80/1.25 tff(f325,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($product(2,$sum(X0,sF8)) = $sum($product(2,X0),sF9)) )),
% 6.80/1.25 inference(superposition,[],[f32,f98])).
% 6.80/1.25 tff(f335,plain,(
% 6.80/1.25 ( ! [X0 : $int] : ($sum(sF9,$product(2,X0)) = $product(2,$sum(X0,sF8))) )),
% 6.80/1.25 inference(forward_demodulation,[],[f325,f17])).
% 6.80/1.25 tff(f345,plain,(
% 6.80/1.25 ~isrecord(sF5) | ~isrecord(b) | next(split1(b)) = split1(next(sF5))),
% 6.80/1.25 inference(superposition,[],[f62,f88])).
% 6.80/1.25 tff(f346,plain,(
% 6.80/1.25 ~isrecord(b) | next(split1(b)) = split1(next(sF5))),
% 6.80/1.25 inference(forward_subsumption_resolution,[],[f345,f89])).
% 6.80/1.25 tff(f348,plain,(
% 6.80/1.25 next(split1(b)) = split1(next(sF5))),
% 6.80/1.25 inference(forward_subsumption_resolution,[],[f346,f71])).
% 6.80/1.25 tff(f349,plain,(
% 6.80/1.25 split1(a) = next(split1(b))),
% 6.80/1.25 inference(forward_demodulation,[],[f348,f105])).
% 6.80/1.25 tff(f350,plain,(
% 6.80/1.25 split1(a) = next(sF0)),
% 6.80/1.25 inference(forward_demodulation,[],[f349,f76])).
% 6.80/1.25 tff(f351,plain,(
% 6.80/1.25 sF7 = next(sF0)),
% 6.80/1.25 inference(forward_demodulation,[],[f350,f94])).
% 6.80/1.25 tff(f415,plain,(
% 6.80/1.25 sF1 = $sum(1,length(sF7))),
% 6.80/1.25 inference(superposition,[],[f244,f351])).
% 6.80/1.25 tff(f422,plain,(
% 6.80/1.25 sF1 = $sum(1,sF8)),
% 6.80/1.25 inference(forward_demodulation,[],[f415,f96])).
% 6.80/1.25 tff(f595,plain,(
% 6.80/1.25 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 6.80/1.25 inference(superposition,[],[f273,f17])).
% 6.80/1.25 tff(f683,plain,(
% 6.80/1.25 $sum(1,0) = $sum(sF11,$uminus(sF10))),
% 6.80/1.25 inference(superposition,[],[f257,f21])).
% 6.80/1.25 tff(f689,plain,(
% 6.80/1.25 1 = $sum(sF11,$uminus(sF10))),
% 6.80/1.25 inference(evaluation,[],[f683])).
% 6.80/1.25 tff(f1861,plain,(
% 6.80/1.25 $product(2,sF1) = $sum(sF9,$product(2,1))),
% 6.80/1.25 inference(superposition,[],[f335,f422])).
% 6.80/1.25 tff(f1882,plain,(
% 6.80/1.25 $product(2,sF1) = $sum(sF9,2)),
% 6.80/1.25 inference(evaluation,[],[f1861])).
% 6.80/1.25 tff(f1891,plain,(
% 6.80/1.25 $product(2,sF1) = $sum(2,sF9)),
% 6.80/1.25 inference(forward_demodulation,[],[f1882,f17])).
% 6.80/1.25 tff(f1898,plain,(
% 6.80/1.25 sF2 = $sum(2,sF9)),
% 6.80/1.25 inference(forward_demodulation,[],[f1891,f80])).
% 6.80/1.25 tff(f3949,plain,(
% 6.80/1.25 $sum(1,0) = $sum(sF3,$uminus(sF11))),
% 6.80/1.25 inference(superposition,[],[f302,f21])).
% 6.80/1.25 tff(f3986,plain,(
% 6.80/1.25 1 = $sum(sF3,$uminus(sF11))),
% 6.80/1.25 inference(evaluation,[],[f3949])).
% 6.80/1.25 tff(f4016,plain,(
% 6.80/1.25 $sum(1,1) = $sum(sF4,$uminus(sF11))),
% 6.80/1.25 inference(superposition,[],[f256,f3986])).
% 6.80/1.25 tff(f4049,plain,(
% 6.80/1.25 2 = $sum(sF4,$uminus(sF11))),
% 6.80/1.25 inference(evaluation,[],[f4016])).
% 6.80/1.25 tff(f5064,plain,(
% 6.80/1.25 $sum(1,1) = $sum(sF3,$uminus(sF10))),
% 6.80/1.25 inference(superposition,[],[f302,f689])).
% 6.80/1.25 tff(f5099,plain,(
% 6.80/1.25 2 = $sum(sF3,$uminus(sF10))),
% 6.80/1.25 inference(evaluation,[],[f5064])).
% 6.80/1.25 tff(f5954,plain,(
% 6.80/1.25 sF3 = $sum(sF10,2)),
% 6.80/1.25 inference(superposition,[],[f595,f5099])).
% 6.80/1.25 tff(f5955,plain,(
% 6.80/1.25 sF4 = $sum(sF11,2)),
% 6.80/1.25 inference(superposition,[],[f595,f4049])).
% 6.80/1.25 tff(f6075,plain,(
% 6.80/1.25 sF4 = $sum(2,sF11)),
% 6.80/1.25 inference(forward_demodulation,[],[f5955,f17])).
% 6.80/1.25 tff(f6076,plain,(
% 6.80/1.25 sF3 = $sum(2,sF10)),
% 6.80/1.25 inference(forward_demodulation,[],[f5954,f17])).
% 6.80/1.25 tff(f8986,plain,(
% 6.80/1.25 sF4 = $sum(2,sF9) | sF9 = sF10),
% 6.80/1.25 inference(superposition,[],[f6075,f103])).
% 6.80/1.25 tff(f9031,plain,(
% 6.80/1.25 sF2 = sF4 | sF9 = sF10),
% 6.80/1.25 inference(forward_demodulation,[],[f8986,f1898])).
% 6.80/1.25 tff(f9033,plain,(
% 6.80/1.25 sF9 = sF10),
% 6.80/1.25 inference(forward_subsumption_resolution,[],[f9031,f85])).
% 6.80/1.25 tff(f9221,plain,(
% 6.80/1.25 sF3 = $sum(2,sF9)),
% 6.80/1.25 inference(superposition,[],[f6076,f9033])).
% 6.80/1.25 tff(f9231,plain,(
% 6.80/1.25 sF2 = sF3),
% 6.80/1.25 inference(forward_demodulation,[],[f9221,f1898])).
% 6.80/1.25 tff(f9232,plain,(
% 6.80/1.25 $false),
% 6.80/1.25 inference(forward_subsumption_resolution,[],[f9231,f86])).
% 6.80/1.25 % SZS output end Proof for theBenchmark
% 6.80/1.25 % (3620251)------------------------------
% 6.80/1.25 % (3620251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.80/1.25 % (3620251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.25 % (3620251)CaDiCaL version: 2.1.3
% 6.80/1.25 % (3620251)Termination reason: Refutation
% 6.80/1.25 % (3620251)Time elapsed: 0.257 s
% 6.80/1.25 % (3620251)Peak memory usage: 16 MB
% 6.80/1.25 % (3620251)Instructions burned: 419 (million)
% 6.80/1.25 % (3620116)Success in time 1.012 s
% 6.80/1.25 % Vampire exiting
%------------------------------------------------------------------------------