% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option i not known.
% ott+4_40_av=off:bce=on:fsd=off:fde=unused:nm=4:nwc=1.1:sos=all:sp=frequency:i=69040_0 on 1 for (346ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 989
% Time elapsed: 0.005 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+1011_8:1_sil=128000:tgt=ground:fde=unused:sp=frequency:nwc=5.0:lwlo=on:i=105338:awrs=converge:awrsf=1385:av=off_0 on 1 for (527ds)
% Refutation not found, non-redundant clauses discarded% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, non-redundant clauses discarded

% Memory used [KB]: 30916
% Time elapsed: 52.690 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option i not known.
% WARNING: option sil not known.
% dis+1011_1:99_anc=none:fde=unused:plsqc=2:bsd=on:plsq=on:plsqr=109,504:sp=reverse_frequency:spb=intro:rp=on:alpa=random:s2a=on:i=257151:s2at=-1.0:aac=none:nm=16:rawr=on:sil=256000:acc=model_0 on 1 for (72ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 3569
% Time elapsed: 0.151 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+21_2461:262144_anc=none:drc=off:sil=2000:sp=occurrence:nwc=6.0:updr=off:st=3.0:i=109:sd=2:afp=4000:erml=3:nm=14:afq=2.0:uhcvi=on:ss=included:er=filter:abs=on:nicw=on:ile=on:sims=off:s2a=on:s2agt=50:s2at=-1.0:plsq=on:plsql=on:plsqc=2:plsqr=1,32:newcnf=on:bd=off:to=lpo_0 on 1 for (1ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit

% Memory used [KB]: 1622
% Time elapsed: 0.205 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs-1011_37821:262144_bsr=unit_only:sil=2000:fde=none:plsq=on:plsqr=43543,131072:bce=on:rnwc=on:plsql=on:rp=on:nwc=10.0:newcnf=on:i=109:awrs=decay:awrsf=10:ep=R:mep=off:amm=sco_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 992
% Time elapsed: 0.003 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% ott-1011_16:1_sil=2000:sp=const_max:urr=on:lsd=20:st=3.0:i=117:ss=axioms:gsp=on:rp=on:sos=on:fd=off:aac=none_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 1052
% Time elapsed: 0.003 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+1010_1:1_to=lpo:sil=2000:sos=on:fd=off:i=117:bd=off_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 986
% Time elapsed: 0.004 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+21_1:64_drc=encompass:sil=32000:bsd=on:lma=on:spb=goal:nwc=10.0:i=123:add=large:ss=axioms:sgt=16:irw=on_0 on 1 for (1ds)
% Refutation not found, non-redundant clauses discarded% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, non-redundant clauses discarded

% Memory used [KB]: 1264
% Time elapsed: 0.064 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+2_1:1_sil=16000:fde=none:sos=all:nwc=5.0:i=117:ep=RS:s2pl=on:lma=on:afp=100000_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 989
% Time elapsed: 0.011 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+1011_1:12_anc=none:drc=off:sil=64000:sims=off:sp=unary_first:spb=goal_then_units:lsd=20:rnwc=on:nwc=2.0:i=138:add=off:awrs=converge:bd=off:uhcvi=on:tgt=ground:afp=300:afq=1.63_0 on 1 for (1ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 3501
% Time elapsed: 0.200 s
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% dis+2_1:28_anc=none:sil=2000:plsqc=1:plsq=on:plsqr=87,4:sp=unary_first:spb=intro:plsql=on:st=2.0:i=117:afp=10:bd=off:nm=16:afr=on:ss=axioms:to=lpo:cond=fast:fsr=off:nwc=7.0_0 on 1 for (1ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 3392
% Time elapsed: 0.200 s
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+1011_1:4_to=lpo:sil=4000:plsq=on:plsqr=32,1:sp=reverse_frequency:fs=off:spb=goal:plsql=on:rp=on:i=108:nm=16:fsr=off:amm=off:rawr=on:drc=off:avsq=on:avsql=on:avsqr=31485,524288:plsqc=2:nwc=5.0_0 on 1 for (1ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 1916
% Time elapsed: 0.200 s
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs-1002_1:1024_anc=none:slsqr=6559637,262144:sil=256000:tgt=ground:fde=unused:bsd=on:sp=const_min:sos=on:bce=on:rp=on:slsqc=3:slsq=on:cond=on:s2a=on:i=109:s2at=3.5:sd=3:kws=inv_arity:afp=300:slsql=off:bsdmm=3:afq=3.34235:uhcvi=on:ss=axioms:rawr=on:add=large:acc=model_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 987
% Time elapsed: 0.005 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option i not known.
% WARNING: option sil not known.
% lrs+11_1:1_sos=on:urr=on:s2a=on:i=124:sd=1:aac=none:ss=axioms:gsp=on:sil=128000:nm=3:bce=on:fd=preordered:alpa=true:etr=on:bd=off:lcm=predicate_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 986
% Time elapsed: 0.003 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs-1_1:1_drc=off:sil=4000:tgt=full:sp=occurrence:sos=on:urr=on:rp=on:i=247:bs=on:ins=1:av=off:rawr=on:to=lpo:br=off_0 on 1 for (2ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit

% Memory used [KB]: 3416
% Time elapsed: 0.305 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+21_1:6_to=lpo:drc=off:sil=64000:tgt=ground:fd=preordered:i=151_0 on 1 for (1ds)
% Refutation not found, non-redundant clauses discarded% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, non-redundant clauses discarded

% Memory used [KB]: 1559
% Time elapsed: 0.095 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% lrs+1011_1:32_sil=2000:tgt=ground:acc=model:lsd=10:nwc=1.1:flr=on:s2pl=no:i=113:bd=off:gsp=on:rawr=on_0 on 1 for (1ds)
% Refutation not found, non-redundant clauses discarded% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, non-redundant clauses discarded

% Memory used [KB]: 2600
% Time elapsed: 0.099 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% dis+1010_5:1_sil=64000:sp=const_min:sos=on:acc=model:i=120:kws=precedence:bd=off:nm=20:alpa=random:ss=axioms_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 985
% Time elapsed: 0.004 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% dis+1002_1:128_sil=2000:fde=none:i=145:plsq=on:plsqc=1:plsqr=6,1:bd=off:tgt=ground:sac=on:sfv=off:s2a=on:s2at=5.0_0 on 1 for (1ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 1246
% Time elapsed: 0.034 s
% ------------------------------
% ------------------------------
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option i not known.
% WARNING: option sil not known.
% lrs+1010_974213:1048576_nwc=9.0:s2a=on:i=123:bd=off:lwlo=on:fd=off:sil=256000:s2agt=10:sims=off:nm=9:sp=const_min:rp=on:er=known:cond=fast:bce=on:abs=on:irw=on:amm=sco:afp=2000:updr=off:add=off:to=lpo:awrs=decay:awrsf=260:rawr=on:afq=2.0:uhcvi=on_0 on 1 for (1ds)
% Time limit reached!
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 3774
% Time elapsed: 0.200 s
% Running in auto input_syntax mode. Trying TPTP
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% WARNING: option sil not known.
% WARNING: option i not known.
% dis+11_1:7_sil=2000:tgt=ground:sp=reverse_arity:i=851:fd=preordered:fsr=off:drc=encompass_0 on 1 for (5ds)
% Solution written to "/var/folders/7m/5r450rvs0fbdh3n_8_kb8td80000gn/T/vampire-proof-52994"
% Running in auto input_syntax mode. Trying TPTP
% SZS status CounterSatisfiable for 1
% # SZS output start Saturation.
cnf(u646,axiom,
    1 = 2).

cnf(u961,axiom,
    f(mul(1,X1),1) = X0).

cnf(u968,axiom,
    X1 = X2).

cnf(u944,axiom,
    1 = X0).

% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)
% Termination reason: Satisfiable

% Memory used [KB]: 1248
% Time elapsed: 0.014 s
% ------------------------------
% ------------------------------
% Success in time 54.617 s