% SZS status Theorem for TFF_Peano.s
% SZS output start Proof for TFF_Peano.s
tff(type_def_5, type, person: $tType).
tff(type_def_6, type, peano: $tType).
tff(func_def_0, type, bob: person).
tff(func_def_1, type, child_of: (person) > person).
tff(func_def_2, type, zero: peano).
tff(func_def_3, type, s: (peano) > peano).
tff(func_def_4, type, peano2person: (peano) > person).
tff(func_def_5, type, sK0: person).
tff(func_def_6, type, sK1: person).
tff(func_def_7, type, sK2: person).
tff(func_def_8, type, sK3: person).
tff(func_def_9, type, sK4: person).
tff(func_def_10, type, sK5: person).
tff(func_def_11, type, sK6: person).
tff(func_def_12, type, sK7: (person) > peano).
tff(func_def_13, type, sK8: (peano) > peano).
tff(pred_def_1, type, is_descendant: (person * person) > $o).
tff(pred_def_2, type, peano_less: (peano * peano) > $o).
tff(f857,plain,(
  $false),
  inference(subsumption_resolution,[],[f739,f119])).
tff(f119,plain,(
  ( ! [X0 : person] : (~is_descendant(X0,X0)) )),
  inference(forward_demodulation,[],[f114,f23])).
tff(f23,plain,(
  ( ! [X10 : person] : (peano2person(sK7(X10)) = X10) )),
  inference(cnf_transformation,[],[f9])).
tff(f9,plain,(
  ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | ~peano_less(X4,X5) | ~peano_less(X3,X4)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10),
  inference(flattening,[],[f8])).
tff(f8,plain,(
  ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | (~peano_less(X4,X5) | ~peano_less(X3,X4))) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10),
  inference(ennf_transformation,[],[f5])).
tff(f5,plain,(
  ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((peano_less(X3,X4) => X3 != X4) & ((peano_less(X4,X5) & peano_less(X3,X4)) => peano_less(X3,X5)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (peano2person(X6) = peano2person(X7) => X6 = X7) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10),
  inference(rectify,[],[f1])).
tff(f1,axiom,(
  ! [X5 : peano,X6 : peano] : (is_descendant(peano2person(X5),peano2person(X6)) <=> peano_less(X5,X6)) & ! [X1 : peano] : child_of(peano2person(X1)) = peano2person(s(X1)) & bob = peano2person(zero) & ! [X2 : peano,X3 : peano,X4 : peano] : ((peano_less(X2,X3) => X2 != X3) & ((peano_less(X3,X4) & peano_less(X2,X3)) => peano_less(X2,X4)) & peano_less(X2,s(X2))) & ! [X2 : peano,X3 : peano] : (peano2person(X2) = peano2person(X3) => X2 = X3) & ! [X1 : peano] : (? [X0 : peano] : s(X0) = X1 | zero = X1) & ! [X0 : person] : ? [X1 : peano] : peano2person(X1) = X0),
  file('TFF_Peano.s.p',people)).
tff(f114,plain,(
  ( ! [X0 : person] : (~is_descendant(peano2person(sK7(X0)),X0)) )),
  inference(resolution,[],[f48,f32])).
tff(f32,plain,(
  ( ! [X4 : peano] : (~peano_less(X4,X4)) )),
  inference(equality_resolution,[],[f16])).
tff(f16,plain,(
  ( ! [X3 : peano,X4 : peano] : (~peano_less(X3,X4) | X3 != X4) )),
  inference(cnf_transformation,[],[f9])).
tff(f48,plain,(
  ( ! [X2 : peano,X1 : person] : (peano_less(X2,sK7(X1)) | ~is_descendant(peano2person(X2),X1)) )),
  inference(superposition,[],[f19,f23])).
tff(f19,plain,(
  ( ! [X0 : peano,X1 : peano] : (~is_descendant(peano2person(X0),peano2person(X1)) | peano_less(X0,X1)) )),
  inference(cnf_transformation,[],[f9])).
tff(f739,plain,(
  is_descendant(sK0,sK0)),
  inference(backward_demodulation,[],[f508,f691])).
tff(f691,plain,(
  sK0 = sK1),
  inference(subsumption_resolution,[],[f690,f40])).
tff(f40,plain,(
  ~is_descendant(sK2,sK4) | sK0 = sK1),
  inference(resolution,[],[f36,f29])).
tff(f29,plain,(
  ~is_descendant(sK5,child_of(sK5)) | ~is_descendant(sK2,sK4) | sK0 = sK1),
  inference(equality_resolution,[],[f12])).
tff(f12,plain,(
  ( ! [X1 : person] : (sK0 = sK1 | ~is_descendant(sK2,sK4) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
tff(f7,plain,(
  ? [X0 : person] : ! [X1 : person] : child_of(X0) != X1 | ? [X2 : person] : ~is_descendant(X2,child_of(X2)) | ? [X3 : person,X4 : person,X5 : person] : (~is_descendant(X3,X5) & is_descendant(X4,X5) & is_descendant(X3,X4)) | ? [X6 : person,X7 : person] : (X6 = X7 & is_descendant(X6,X7))),
  inference(flattening,[],[f6])).
tff(f6,plain,(
  ? [X0 : person] : ! [X1 : person] : child_of(X0) != X1 | ? [X2 : person] : ~is_descendant(X2,child_of(X2)) | ? [X3 : person,X4 : person,X5 : person] : (~is_descendant(X3,X5) & (is_descendant(X4,X5) & is_descendant(X3,X4))) | ? [X6 : person,X7 : person] : (X6 = X7 & is_descendant(X6,X7))),
  inference(ennf_transformation,[],[f4])).
tff(f4,plain,(
  ~(! [X0 : person] : ? [X1 : person] : child_of(X0) = X1 & ! [X2 : person] : is_descendant(X2,child_of(X2)) & ! [X3 : person,X4 : person,X5 : person] : ((is_descendant(X4,X5) & is_descendant(X3,X4)) => is_descendant(X3,X5)) & ! [X6 : person,X7 : person] : (is_descendant(X6,X7) => X6 != X7))),
  inference(rectify,[],[f3])).
tff(f3,negated_conjecture,(
  ~(! [X0 : person] : ? [X7 : person] : child_of(X0) = X7 & ! [X0 : person] : is_descendant(X0,child_of(X0)) & ! [X5 : person,X7 : person,X8 : person] : ((is_descendant(X7,X8) & is_descendant(X5,X7)) => is_descendant(X5,X8)) & ! [X5 : person,X6 : person] : (is_descendant(X5,X6) => X5 != X6))),
  inference(negated_conjecture,[],[f2])).
tff(f2,conjecture,(
  ! [X0 : person] : ? [X7 : person] : child_of(X0) = X7 & ! [X0 : person] : is_descendant(X0,child_of(X0)) & ! [X5 : person,X7 : person,X8 : person] : ((is_descendant(X7,X8) & is_descendant(X5,X7)) => is_descendant(X5,X8)) & ! [X5 : person,X6 : person] : (is_descendant(X5,X6) => X5 != X6)),
  file('TFF_Peano.s.p',prove_formulae)).
tff(f36,plain,(
  ( ! [X0 : person] : (is_descendant(X0,child_of(X0))) )),
  inference(superposition,[],[f34,f23])).
tff(f34,plain,(
  ( ! [X0 : peano] : (is_descendant(peano2person(X0),child_of(peano2person(X0)))) )),
  inference(forward_demodulation,[],[f33,f25])).
tff(f25,plain,(
  ( ! [X2 : peano] : (child_of(peano2person(X2)) = peano2person(s(X2))) )),
  inference(cnf_transformation,[],[f9])).
tff(f33,plain,(
  ( ! [X0 : peano] : (is_descendant(peano2person(X0),peano2person(s(X0)))) )),
  inference(resolution,[],[f18,f20])).
tff(f20,plain,(
  ( ! [X3 : peano] : (peano_less(X3,s(X3))) )),
  inference(cnf_transformation,[],[f9])).
tff(f18,plain,(
  ( ! [X0 : peano,X1 : peano] : (~peano_less(X0,X1) | is_descendant(peano2person(X0),peano2person(X1))) )),
  inference(cnf_transformation,[],[f9])).
tff(f690,plain,(
  is_descendant(sK2,sK4) | sK0 = sK1),
  inference(forward_demodulation,[],[f689,f23])).
tff(f689,plain,(
  is_descendant(peano2person(sK7(sK2)),sK4) | sK0 = sK1),
  inference(forward_demodulation,[],[f686,f23])).
tff(f686,plain,(
  sK0 = sK1 | is_descendant(peano2person(sK7(sK2)),peano2person(sK7(sK4)))),
  inference(resolution,[],[f683,f18])).
tff(f683,plain,(
  peano_less(sK7(sK2),sK7(sK4)) | sK0 = sK1),
  inference(duplicate_literal_removal,[],[f679])).
tff(f679,plain,(
  sK0 = sK1 | peano_less(sK7(sK2),sK7(sK4)) | sK0 = sK1),
  inference(resolution,[],[f252,f214])).
tff(f214,plain,(
  peano_less(sK7(sK2),sK7(sK3)) | sK0 = sK1),
  inference(resolution,[],[f112,f38])).
tff(f38,plain,(
  is_descendant(sK2,sK3) | sK0 = sK1),
  inference(resolution,[],[f36,f31])).
tff(f31,plain,(
  ~is_descendant(sK5,child_of(sK5)) | is_descendant(sK2,sK3) | sK0 = sK1),
  inference(equality_resolution,[],[f10])).
tff(f10,plain,(
  ( ! [X1 : person] : (sK0 = sK1 | is_descendant(sK2,sK3) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
tff(f112,plain,(
  ( ! [X2 : person,X1 : person] : (~is_descendant(X2,X1) | peano_less(sK7(X2),sK7(X1))) )),
  inference(superposition,[],[f45,f23])).
tff(f45,plain,(
  ( ! [X2 : peano,X1 : person] : (~is_descendant(X1,peano2person(X2)) | peano_less(sK7(X1),X2)) )),
  inference(superposition,[],[f19,f23])).
tff(f252,plain,(
  ( ! [X0 : peano] : (~peano_less(X0,sK7(sK3)) | sK0 = sK1 | peano_less(X0,sK7(sK4))) )),
  inference(resolution,[],[f216,f17])).
tff(f17,plain,(
  ( ! [X3 : peano,X4 : peano,X5 : peano] : (~peano_less(X4,X5) | ~peano_less(X3,X4) | peano_less(X3,X5)) )),
  inference(cnf_transformation,[],[f9])).
tff(f216,plain,(
  peano_less(sK7(sK3),sK7(sK4)) | sK0 = sK1),
  inference(resolution,[],[f112,f39])).
tff(f39,plain,(
  is_descendant(sK3,sK4) | sK0 = sK1),
  inference(resolution,[],[f36,f30])).
tff(f30,plain,(
  ~is_descendant(sK5,child_of(sK5)) | is_descendant(sK3,sK4) | sK0 = sK1),
  inference(equality_resolution,[],[f11])).
tff(f11,plain,(
  ( ! [X1 : person] : (sK0 = sK1 | is_descendant(sK3,sK4) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
tff(f508,plain,(
  is_descendant(sK0,sK1)),
  inference(subsumption_resolution,[],[f507,f43])).
tff(f43,plain,(
  ~is_descendant(sK2,sK4) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f36,f26])).
tff(f26,plain,(
  ~is_descendant(sK5,child_of(sK5)) | ~is_descendant(sK2,sK4) | is_descendant(sK0,sK1)),
  inference(equality_resolution,[],[f15])).
tff(f15,plain,(
  ( ! [X1 : person] : (is_descendant(sK0,sK1) | ~is_descendant(sK2,sK4) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
tff(f507,plain,(
  is_descendant(sK2,sK4) | is_descendant(sK0,sK1)),
  inference(forward_demodulation,[],[f506,f23])).
tff(f506,plain,(
  is_descendant(peano2person(sK7(sK2)),sK4) | is_descendant(sK0,sK1)),
  inference(forward_demodulation,[],[f503,f23])).
tff(f503,plain,(
  is_descendant(sK0,sK1) | is_descendant(peano2person(sK7(sK2)),peano2person(sK7(sK4)))),
  inference(resolution,[],[f500,f18])).
tff(f500,plain,(
  peano_less(sK7(sK2),sK7(sK4)) | is_descendant(sK0,sK1)),
  inference(duplicate_literal_removal,[],[f497])).
tff(f497,plain,(
  is_descendant(sK0,sK1) | peano_less(sK7(sK2),sK7(sK4)) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f245,f213])).
tff(f213,plain,(
  peano_less(sK7(sK2),sK7(sK3)) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f112,f41])).
tff(f41,plain,(
  is_descendant(sK2,sK3) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f36,f28])).
tff(f28,plain,(
  ~is_descendant(sK5,child_of(sK5)) | is_descendant(sK2,sK3) | is_descendant(sK0,sK1)),
  inference(equality_resolution,[],[f13])).
tff(f13,plain,(
  ( ! [X1 : person] : (is_descendant(sK0,sK1) | is_descendant(sK2,sK3) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
tff(f245,plain,(
  ( ! [X0 : peano] : (~peano_less(X0,sK7(sK3)) | is_descendant(sK0,sK1) | peano_less(X0,sK7(sK4))) )),
  inference(resolution,[],[f215,f17])).
tff(f215,plain,(
  peano_less(sK7(sK3),sK7(sK4)) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f112,f42])).
tff(f42,plain,(
  is_descendant(sK3,sK4) | is_descendant(sK0,sK1)),
  inference(resolution,[],[f36,f27])).
tff(f27,plain,(
  ~is_descendant(sK5,child_of(sK5)) | is_descendant(sK3,sK4) | is_descendant(sK0,sK1)),
  inference(equality_resolution,[],[f14])).
tff(f14,plain,(
  ( ! [X1 : person] : (is_descendant(sK0,sK1) | is_descendant(sK3,sK4) | ~is_descendant(sK5,child_of(sK5)) | child_of(sK6) != X1) )),
  inference(cnf_transformation,[],[f7])).
% SZS output end Proof for TFF_Peano.s