% 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:32_anc=all:to=lpo:sil=256000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:plsql=on:sac=on:newcnf=on:i=222662:add=off:fsr=off:rawr=on_0 on reducedaxiom2 for (599ds)
% Refutation not found, incomplete strategy% ------------------------------
% Version: Vampire 4.9 (commit )
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 988
% Time elapsed: 0.002 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_4:1_sil=256000:rp=on:newcnf=on:i=257909:aac=none:gsp=on_0 on reducedaxiom2 for (599ds)
% Solution written to "/var/folders/jc/2nvlxl_15xg4t3zqqv9mpn7c0000gn/T/vampire-proof-37394"
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for reducedaxiom2
% SZS output start Proof for reducedaxiom2
fof(f84,plain,(
  $false),
  inference(resolution,[],[f76,f23])).
fof(f23,plain,(
  ( ! [X0,X1] : (~good(X0,sK0(X0,X1),X1)) )),
  inference(consistent_polarity_flipping,[],[f12])).
fof(f12,plain,(
  ( ! [X0,X1] : (good(X0,sK0(X0,X1),X1)) )),
  inference(cnf_transformation,[],[f1])).
fof(f1,axiom,(
  ! [X0,X1] : ? [X2] : good(X0,X2,X1)),
  file('reducedaxiom2.p',unknown)).
fof(f76,plain,(
  ( ! [X0,X1] : (good(2,X0,X1)) )),
  inference(resolution,[],[f72,f22])).
fof(f22,plain,(
  ~good(0,1,2)),
  inference(consistent_polarity_flipping,[],[f11])).
fof(f11,plain,(
  good(0,1,2)),
  inference(cnf_transformation,[],[f3])).
fof(f3,axiom,(
  good(0,1,2)),
  file('reducedaxiom2.p',unknown)).
fof(f72,plain,(
  ( ! [X2,X3,X0,X1] : (good(0,X0,X1) | good(X1,X2,X3)) )),
  inference(resolution,[],[f53,f23])).
fof(f53,plain,(
  ( ! [X2,X3,X0,X1,X4] : (good(X0,X1,0) | good(0,X2,X3) | good(X3,X0,X4)) )),
  inference(resolution,[],[f50,f23])).
fof(f50,plain,(
  ( ! [X2,X3,X0,X1,X4,X5] : (good(2,X0,X1) | good(X2,X1,0) | good(0,X3,X4) | good(X4,X2,X5)) )),
  inference(resolution,[],[f27,f25])).
fof(f25,plain,(
  ( ! [X2,X3,X0,X1,X4,X5] : (~good(X1,X2,X3) | good(X0,X1,X2) | good(X2,X3,X4) | good(X4,X0,X5)) )),
  inference(resolution,[],[f24,f20])).
fof(f20,plain,(
  ( ! [X0,X1,X5] : (sP1(X0,X1) | good(X0,X1,X5)) )),
  inference(consistent_polarity_flipping,[],[f14])).
fof(f14,plain,(
  ( ! [X0,X1,X5] : (~good(X0,X1,X5) | sP1(X0,X1)) )),
  inference(cnf_transformation,[],[f14_D])).
fof(f14_D,plain,(
  ( ! [X1,X0] : (( ! [X5] : ~good(X0,X1,X5) ) <=> ~sP1(X0,X1)) )),
  introduced(general_splitting_component_introduction,[new_symbols(naming,[sP1])])).
fof(f24,plain,(
  ( ! [X2,X3,X0,X1,X4] : (~sP1(X4,X3) | good(X3,X0,X1) | ~good(X0,X1,X2) | good(X1,X2,X4)) )),
  inference(resolution,[],[f19,f18])).
fof(f18,plain,(
  ( ! [X3,X0,X1,X4] : (~sP2(X4,X3,X1) | ~sP1(X0,X1) | good(X3,X4,X0)) )),
  inference(consistent_polarity_flipping,[],[f17])).
fof(f17,plain,(
  ( ! [X3,X0,X1,X4] : (~good(X3,X4,X0) | ~sP1(X0,X1) | ~sP2(X4,X3,X1)) )),
  inference(general_splitting,[],[f15,f16_D])).
fof(f16,plain,(
  ( ! [X2,X3,X1,X4] : (~good(X1,X2,X3) | good(X2,X3,X4) | sP2(X4,X3,X1)) )),
  inference(cnf_transformation,[],[f16_D])).
fof(f16_D,plain,(
  ( ! [X1,X3,X4] : (( ! [X2] : (~good(X1,X2,X3) | good(X2,X3,X4)) ) <=> ~sP2(X4,X3,X1)) )),
  introduced(general_splitting_component_introduction,[new_symbols(naming,[sP2])])).
fof(f15,plain,(
  ( ! [X2,X3,X0,X1,X4] : (~good(X1,X2,X3) | ~good(X3,X4,X0) | good(X2,X3,X4) | ~sP1(X0,X1)) )),
  inference(general_splitting,[],[f13,f14_D])).
fof(f13,plain,(
  ( ! [X2,X3,X0,X1,X4,X5] : (~good(X0,X1,X5) | ~good(X1,X2,X3) | ~good(X3,X4,X0) | good(X2,X3,X4)) )),
  inference(cnf_transformation,[],[f9])).
fof(f9,plain,(
  ! [X0,X1,X2,X3,X4,X5] : (good(X2,X3,X4) | ~good(X3,X4,X0) | ~good(X1,X2,X3) | ~good(X0,X1,X5))),
  inference(flattening,[],[f8])).
fof(f8,plain,(
  ! [X0,X1,X2,X3,X4,X5] : (good(X2,X3,X4) | (~good(X3,X4,X0) | ~good(X1,X2,X3) | ~good(X0,X1,X5)))),
  inference(ennf_transformation,[],[f2])).
fof(f2,axiom,(
  ! [X0,X1,X2,X3,X4,X5] : ((good(X3,X4,X0) & good(X1,X2,X3) & good(X0,X1,X5)) => good(X2,X3,X4))),
  file('reducedaxiom2.p',unknown)).
fof(f19,plain,(
  ( ! [X2,X3,X1,X4] : (sP2(X4,X3,X1) | ~good(X2,X3,X4) | good(X1,X2,X3)) )),
  inference(consistent_polarity_flipping,[],[f16])).
fof(f27,plain,(
  ( ! [X2,X0,X1] : (good(X1,0,X2) | good(2,X0,X1)) )),
  inference(resolution,[],[f26,f22])).
fof(f26,plain,(
  ( ! [X2,X3,X0,X1] : (good(X0,1,2) | good(2,X1,X2) | good(X2,X0,X3)) )),
  inference(resolution,[],[f25,f21])).
fof(f21,plain,(
  ( ! [X0] : (good(1,2,X0)) )),
  inference(consistent_polarity_flipping,[],[f10])).
fof(f10,plain,(
  ( ! [X0] : (~good(1,2,X0)) )),
  inference(cnf_transformation,[],[f7])).
fof(f7,plain,(
  ! [X0] : ~good(1,2,X0)),
  inference(ennf_transformation,[],[f6])).
fof(f6,plain,(
  ~? [X0] : good(1,2,X0)),
  inference(rectify,[],[f5])).
fof(f5,negated_conjecture,(
  ~? [X2] : good(1,2,X2)),
  inference(negated_conjecture,[],[f4])).
fof(f4,conjecture,(
  ? [X2] : good(1,2,X2)),
  file('reducedaxiom2.p',unknown)).
% SZS output end Proof for reducedaxiom2
% ------------------------------
% Version: Vampire 4.9 (commit )
% Termination reason: Refutation

% Memory used [KB]: 1027
% Time elapsed: 0.003 s
% ------------------------------
% ------------------------------
% Success in time 0.011 s