% SZS status Theorem for TFF_Finite.s
% SZS output start Proof for TFF_Finite.s
tff(type_def_5, type, man: $tType).
tff(type_def_6, type, grade: $tType).
tff(type_def_7, type, d_man: $tType).
tff(type_def_8, type, d_grade: $tType).
tff(func_def_0, type, john: man).
tff(func_def_1, type, a: grade).
tff(func_def_2, type, f: grade).
tff(func_def_3, type, grade_of: (man) > grade).
tff(func_def_4, type, d2man: (d_man) > man).
tff(func_def_5, type, d2grade: (d_grade) > grade).
tff(func_def_6, type, d_john: d_man).
tff(func_def_7, type, d_gotA: d_man).
tff(func_def_8, type, d_a: d_grade).
tff(func_def_9, type, d_f: d_grade).
tff(func_def_10, type, sK0: man).
tff(func_def_11, type, sK1: man).
tff(func_def_12, type, sK2: (grade) > d_grade).
tff(func_def_13, type, sK3: (man) > d_man).
tff(pred_def_1, type, created_equal: (man * man) > $o).
tff(f452,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f56,f130,f139,f166,f202,f262,f297,f346,f371,f451])).
tff(f451,plain,(
  ~spl4_6),
  inference(avatar_contradiction_clause,[],[f450])).
tff(f450,plain,(
  $false | ~spl4_6),
  inference(subsumption_resolution,[],[f447,f18])).
tff(f18,plain,(
  d_john != d_gotA),
  inference(cnf_transformation,[],[f13])).
tff(f13,plain,(
  created_equal(d2man(d_gotA),d2man(d_gotA)) & created_equal(d2man(d_gotA),d2man(d_john)) & created_equal(d2man(d_john),d2man(d_gotA)) & created_equal(d2man(d_john),d2man(d_john)) & d2grade(d_a) = grade_of(d2man(d_gotA)) & d2grade(d_f) = grade_of(d2man(d_john)) & john = d2man(d_john) & f = d2grade(d_f) & a = d2grade(d_a) & ! [X0 : d_grade,X1 : d_grade] : (X0 = X1 | d2grade(X0) != d2grade(X1)) & d_a != d_f & ! [X2 : d_grade] : (d_f = X2 | d_a = X2) & ! [X3 : grade] : d2grade(sK2(X3)) = X3 & ! [X5 : d_man,X6 : d_man] : (X5 = X6 | d2man(X5) != d2man(X6)) & d_john != d_gotA & ! [X7 : d_man] : (d_gotA = X7 | d_john = X7) & ! [X8 : man] : d2man(sK3(X8)) = X8),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK2,sK3])],[f7,f12,f11])).
tff(f11,plain,(
  ! [X3 : grade] : (? [X4 : d_grade] : d2grade(X4) = X3 => d2grade(sK2(X3)) = X3)),
  introduced(choice_axiom,[])).
tff(f12,plain,(
  ! [X8 : man] : (? [X9 : d_man] : d2man(X9) = X8 => d2man(sK3(X8)) = X8)),
  introduced(choice_axiom,[])).
tff(f7,plain,(
  created_equal(d2man(d_gotA),d2man(d_gotA)) & created_equal(d2man(d_gotA),d2man(d_john)) & created_equal(d2man(d_john),d2man(d_gotA)) & created_equal(d2man(d_john),d2man(d_john)) & d2grade(d_a) = grade_of(d2man(d_gotA)) & d2grade(d_f) = grade_of(d2man(d_john)) & john = d2man(d_john) & f = d2grade(d_f) & a = d2grade(d_a) & ! [X0 : d_grade,X1 : d_grade] : (X0 = X1 | d2grade(X0) != d2grade(X1)) & d_a != d_f & ! [X2 : d_grade] : (d_f = X2 | d_a = X2) & ! [X3 : grade] : ? [X4 : d_grade] : d2grade(X4) = X3 & ! [X5 : d_man,X6 : d_man] : (X5 = X6 | d2man(X5) != d2man(X6)) & d_john != d_gotA & ! [X7 : d_man] : (d_gotA = X7 | d_john = X7) & ! [X8 : man] : ? [X9 : d_man] : d2man(X9) = X8),
  inference(ennf_transformation,[],[f5])).
tff(f5,plain,(
  created_equal(d2man(d_gotA),d2man(d_gotA)) & created_equal(d2man(d_gotA),d2man(d_john)) & created_equal(d2man(d_john),d2man(d_gotA)) & created_equal(d2man(d_john),d2man(d_john)) & d2grade(d_a) = grade_of(d2man(d_gotA)) & d2grade(d_f) = grade_of(d2man(d_john)) & john = d2man(d_john) & f = d2grade(d_f) & a = d2grade(d_a) & ! [X0 : d_grade,X1 : d_grade] : (d2grade(X0) = d2grade(X1) => X0 = X1) & d_a != d_f & ! [X2 : d_grade] : (d_f = X2 | d_a = X2) & ! [X3 : grade] : ? [X4 : d_grade] : d2grade(X4) = X3 & ! [X5 : d_man,X6 : d_man] : (d2man(X5) = d2man(X6) => X5 = X6) & d_john != d_gotA & ! [X7 : d_man] : (d_gotA = X7 | d_john = X7) & ! [X8 : man] : ? [X9 : d_man] : d2man(X9) = X8),
  inference(rectify,[],[f1])).
tff(f1,axiom,(
  created_equal(d2man(d_gotA),d2man(d_gotA)) & created_equal(d2man(d_gotA),d2man(d_john)) & created_equal(d2man(d_john),d2man(d_gotA)) & created_equal(d2man(d_john),d2man(d_john)) & d2grade(d_a) = grade_of(d2man(d_gotA)) & d2grade(d_f) = grade_of(d2man(d_john)) & john = d2man(d_john) & f = d2grade(d_f) & a = d2grade(d_a) & ! [X6 : d_grade,X7 : d_grade] : (d2grade(X6) = d2grade(X7) => X6 = X7) & d_a != d_f & ! [X5 : d_grade] : (d_f = X5 | d_a = X5) & ! [X4 : grade] : ? [X5 : d_grade] : d2grade(X5) = X4 & ! [X2 : d_man,X3 : d_man] : (d2man(X2) = d2man(X3) => X2 = X3) & d_john != d_gotA & ! [X1 : d_man] : (d_gotA = X1 | d_john = X1) & ! [X0 : man] : ? [X1 : d_man] : d2man(X1) = X0),
  file('TFF_Finite.s.p',equality_lost)).
tff(f447,plain,(
  d_john = d_gotA | ~spl4_6),
  inference(trivial_inequality_removal,[],[f446])).
tff(f446,plain,(
  john != john | d_john = d_gotA | ~spl4_6),
  inference(superposition,[],[f94,f434])).
tff(f434,plain,(
  john = d2man(d_gotA) | ~spl4_6),
  inference(resolution,[],[f58,f55])).
tff(f55,plain,(
  ( ! [X0 : man,X1 : man] : (~created_equal(X0,X1) | X0 = X1) ) | ~spl4_6),
  inference(avatar_component_clause,[],[f54])).
tff(f54,plain,(
  spl4_6 <=> ! [X0 : man,X1 : man] : (X0 = X1 | ~created_equal(X0,X1))),
  introduced(avatar_definition,[new_symbols(naming,[spl4_6])])).
tff(f58,plain,(
  created_equal(john,d2man(d_gotA))),
  inference(forward_demodulation,[],[f30,f26])).
tff(f26,plain,(
  john = d2man(d_john)),
  inference(cnf_transformation,[],[f13])).
tff(f30,plain,(
  created_equal(d2man(d_john),d2man(d_gotA))),
  inference(cnf_transformation,[],[f13])).
tff(f94,plain,(
  ( ! [X0 : d_man] : (john != d2man(X0) | d_john = X0) )),
  inference(superposition,[],[f19,f26])).
tff(f19,plain,(
  ( ! [X6 : d_man,X5 : d_man] : (d2man(X5) != d2man(X6) | X5 = X6) )),
  inference(cnf_transformation,[],[f13])).
tff(f371,plain,(
  ~spl4_7 | spl4_10),
  inference(avatar_contradiction_clause,[],[f370])).
tff(f370,plain,(
  $false | (~spl4_7 | spl4_10)),
  inference(subsumption_resolution,[],[f138,f351])).
tff(f351,plain,(
  created_equal(sK0,john) | ~spl4_7),
  inference(forward_demodulation,[],[f59,f125])).
tff(f125,plain,(
  d2man(d_gotA) = sK0 | ~spl4_7),
  inference(avatar_component_clause,[],[f123])).
tff(f123,plain,(
  spl4_7 <=> d2man(d_gotA) = sK0),
  introduced(avatar_definition,[new_symbols(naming,[spl4_7])])).
tff(f59,plain,(
  created_equal(d2man(d_gotA),john)),
  inference(forward_demodulation,[],[f31,f26])).
tff(f31,plain,(
  created_equal(d2man(d_gotA),d2man(d_john))),
  inference(cnf_transformation,[],[f13])).
tff(f138,plain,(
  ~created_equal(sK0,john) | spl4_10),
  inference(avatar_component_clause,[],[f136])).
tff(f136,plain,(
  spl4_10 <=> created_equal(sK0,john)),
  introduced(avatar_definition,[new_symbols(naming,[spl4_10])])).
tff(f346,plain,(
  spl4_1 | ~spl4_7 | ~spl4_9),
  inference(avatar_contradiction_clause,[],[f345])).
tff(f345,plain,(
  $false | (spl4_1 | ~spl4_7 | ~spl4_9)),
  inference(subsumption_resolution,[],[f323,f331])).
tff(f331,plain,(
  created_equal(sK0,sK0) | (~spl4_7 | ~spl4_9)),
  inference(backward_demodulation,[],[f259,f313])).
tff(f313,plain,(
  sK0 = sK1 | (~spl4_7 | ~spl4_9)),
  inference(backward_demodulation,[],[f134,f125])).
tff(f134,plain,(
  d2man(d_gotA) = sK1 | ~spl4_9),
  inference(avatar_component_clause,[],[f132])).
tff(f132,plain,(
  spl4_9 <=> d2man(d_gotA) = sK1),
  introduced(avatar_definition,[new_symbols(naming,[spl4_9])])).
tff(f259,plain,(
  created_equal(sK1,sK1) | ~spl4_9),
  inference(forward_demodulation,[],[f32,f134])).
tff(f32,plain,(
  created_equal(d2man(d_gotA),d2man(d_gotA))),
  inference(cnf_transformation,[],[f13])).
tff(f323,plain,(
  ~created_equal(sK0,sK0) | (spl4_1 | ~spl4_7 | ~spl4_9)),
  inference(backward_demodulation,[],[f37,f313])).
tff(f37,plain,(
  ~created_equal(sK0,sK1) | spl4_1),
  inference(avatar_component_clause,[],[f35])).
tff(f35,plain,(
  spl4_1 <=> created_equal(sK0,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl4_1])])).
tff(f297,plain,(
  ~spl4_4),
  inference(avatar_contradiction_clause,[],[f296])).
tff(f296,plain,(
  $false | ~spl4_4),
  inference(subsumption_resolution,[],[f293,f285])).
tff(f285,plain,(
  ( ! [X0 : d_grade,X1 : d_grade] : (X0 = X1) ) | ~spl4_4),
  inference(superposition,[],[f282,f282])).
tff(f282,plain,(
  ( ! [X3 : d_grade] : (d_f = X3) ) | ~spl4_4),
  inference(subsumption_resolution,[],[f275,f70])).
tff(f70,plain,(
  ( ! [X0 : d_grade] : (a = d2grade(X0) | d_f = X0) )),
  inference(superposition,[],[f24,f21])).
tff(f21,plain,(
  ( ! [X2 : d_grade] : (d_a = X2 | d_f = X2) )),
  inference(cnf_transformation,[],[f13])).
tff(f24,plain,(
  a = d2grade(d_a)),
  inference(cnf_transformation,[],[f13])).
tff(f275,plain,(
  ( ! [X3 : d_grade] : (a != d2grade(X3) | d_f = X3) ) | ~spl4_4),
  inference(superposition,[],[f23,f265])).
tff(f265,plain,(
  a = d2grade(d_f) | ~spl4_4),
  inference(backward_demodulation,[],[f25,f48])).
tff(f48,plain,(
  a = f | ~spl4_4),
  inference(avatar_component_clause,[],[f46])).
tff(f46,plain,(
  spl4_4 <=> a = f),
  introduced(avatar_definition,[new_symbols(naming,[spl4_4])])).
tff(f25,plain,(
  f = d2grade(d_f)),
  inference(cnf_transformation,[],[f13])).
tff(f23,plain,(
  ( ! [X0 : d_grade,X1 : d_grade] : (d2grade(X0) != d2grade(X1) | X0 = X1) )),
  inference(cnf_transformation,[],[f13])).
tff(f293,plain,(
  ( ! [X0 : d_grade] : (d_a != X0) ) | ~spl4_4),
  inference(superposition,[],[f22,f285])).
tff(f22,plain,(
  d_a != d_f),
  inference(cnf_transformation,[],[f13])).
tff(f262,plain,(
  ~spl4_3),
  inference(avatar_contradiction_clause,[],[f261])).
tff(f261,plain,(
  $false | ~spl4_3),
  inference(subsumption_resolution,[],[f78,f44])).
tff(f44,plain,(
  ( ! [X2 : man] : (a != grade_of(X2)) ) | ~spl4_3),
  inference(avatar_component_clause,[],[f43])).
tff(f43,plain,(
  spl4_3 <=> ! [X2 : man] : a != grade_of(X2)),
  introduced(avatar_definition,[new_symbols(naming,[spl4_3])])).
tff(f78,plain,(
  a = grade_of(d2man(d_gotA))),
  inference(forward_demodulation,[],[f28,f24])).
tff(f28,plain,(
  d2grade(d_a) = grade_of(d2man(d_gotA))),
  inference(cnf_transformation,[],[f13])).
tff(f202,plain,(
  spl4_2),
  inference(avatar_contradiction_clause,[],[f201])).
tff(f201,plain,(
  $false | spl4_2),
  inference(subsumption_resolution,[],[f41,f77])).
tff(f77,plain,(
  f = grade_of(john)),
  inference(forward_demodulation,[],[f76,f25])).
tff(f76,plain,(
  d2grade(d_f) = grade_of(john)),
  inference(forward_demodulation,[],[f27,f26])).
tff(f27,plain,(
  d2grade(d_f) = grade_of(d2man(d_john))),
  inference(cnf_transformation,[],[f13])).
tff(f41,plain,(
  f != grade_of(john) | spl4_2),
  inference(avatar_component_clause,[],[f39])).
tff(f39,plain,(
  spl4_2 <=> f = grade_of(john)),
  introduced(avatar_definition,[new_symbols(naming,[spl4_2])])).
tff(f166,plain,(
  spl4_8),
  inference(avatar_contradiction_clause,[],[f165])).
tff(f165,plain,(
  $false | spl4_8),
  inference(subsumption_resolution,[],[f157,f129])).
tff(f129,plain,(
  ~created_equal(john,sK1) | spl4_8),
  inference(avatar_component_clause,[],[f127])).
tff(f127,plain,(
  spl4_8 <=> created_equal(john,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl4_8])])).
tff(f157,plain,(
  created_equal(john,sK1) | spl4_8),
  inference(backward_demodulation,[],[f58,f150])).
tff(f150,plain,(
  d2man(d_gotA) = sK1 | spl4_8),
  inference(subsumption_resolution,[],[f149,f57])).
tff(f57,plain,(
  created_equal(john,john)),
  inference(forward_demodulation,[],[f29,f26])).
tff(f29,plain,(
  created_equal(d2man(d_john),d2man(d_john))),
  inference(cnf_transformation,[],[f13])).
tff(f149,plain,(
  ~created_equal(john,john) | d2man(d_gotA) = sK1 | spl4_8),
  inference(superposition,[],[f129,f87])).
tff(f87,plain,(
  ( ! [X0 : man] : (john = X0 | d2man(d_gotA) = X0) )),
  inference(superposition,[],[f16,f68])).
tff(f68,plain,(
  ( ! [X0 : man] : (d_gotA = sK3(X0) | john = X0) )),
  inference(forward_demodulation,[],[f66,f26])).
tff(f66,plain,(
  ( ! [X0 : man] : (d2man(d_john) = X0 | d_gotA = sK3(X0)) )),
  inference(superposition,[],[f16,f17])).
tff(f17,plain,(
  ( ! [X7 : d_man] : (d_john = X7 | d_gotA = X7) )),
  inference(cnf_transformation,[],[f13])).
tff(f16,plain,(
  ( ! [X8 : man] : (d2man(sK3(X8)) = X8) )),
  inference(cnf_transformation,[],[f13])).
tff(f139,plain,(
  spl4_9 | ~spl4_10 | spl4_1),
  inference(avatar_split_clause,[],[f119,f35,f136,f132])).
tff(f119,plain,(
  ~created_equal(sK0,john) | d2man(d_gotA) = sK1 | spl4_1),
  inference(superposition,[],[f37,f87])).
tff(f130,plain,(
  spl4_7 | ~spl4_8 | spl4_1),
  inference(avatar_split_clause,[],[f118,f35,f127,f123])).
tff(f118,plain,(
  ~created_equal(john,sK1) | d2man(d_gotA) = sK0 | spl4_1),
  inference(superposition,[],[f37,f87])).
tff(f56,plain,(
  ~spl4_1 | ~spl4_2 | spl4_3 | spl4_4 | spl4_6),
  inference(avatar_split_clause,[],[f14,f54,f46,f43,f39,f35])).
tff(f14,plain,(
  ( ! [X2 : man,X0 : man,X1 : man] : (X0 = X1 | ~created_equal(X0,X1) | a = f | a != grade_of(X2) | f != grade_of(john) | ~created_equal(sK0,sK1)) )),
  inference(cnf_transformation,[],[f10])).
tff(f10,plain,(
  ! [X0 : man,X1 : man] : ((created_equal(X0,X1) | X0 != X1) & (X0 = X1 | ~created_equal(X0,X1))) | a = f | ! [X2 : man] : a != grade_of(X2) | f != grade_of(john) | ~created_equal(sK0,sK1)),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f8,f9])).
tff(f9,plain,(
  ? [X3 : man,X4 : man] : ~created_equal(X3,X4) => ~created_equal(sK0,sK1)),
  introduced(choice_axiom,[])).
tff(f8,plain,(
  ! [X0 : man,X1 : man] : ((created_equal(X0,X1) | X0 != X1) & (X0 = X1 | ~created_equal(X0,X1))) | a = f | ! [X2 : man] : a != grade_of(X2) | f != grade_of(john) | ? [X3 : man,X4 : man] : ~created_equal(X3,X4)),
  inference(nnf_transformation,[],[f6])).
tff(f6,plain,(
  ! [X0 : man,X1 : man] : (created_equal(X0,X1) <=> X0 = X1) | a = f | ! [X2 : man] : a != grade_of(X2) | f != grade_of(john) | ? [X3 : man,X4 : man] : ~created_equal(X3,X4)),
  inference(ennf_transformation,[],[f4])).
tff(f4,plain,(
  ~(~! [X0 : man,X1 : man] : (created_equal(X0,X1) <=> X0 = X1) & a != f & ? [X2 : man] : a = grade_of(X2) & f = grade_of(john) & ! [X3 : man,X4 : man] : created_equal(X3,X4))),
  inference(rectify,[],[f3])).
tff(f3,negated_conjecture,(
  ~(~! [X8 : man,X9 : man] : (created_equal(X8,X9) <=> X8 = X9) & a != f & ? [X10 : man] : a = grade_of(X10) & f = grade_of(john) & ! [X8 : man,X9 : man] : created_equal(X8,X9))),
  inference(negated_conjecture,[],[f2])).
tff(f2,conjecture,(
  ~! [X8 : man,X9 : man] : (created_equal(X8,X9) <=> X8 = X9) & a != f & ? [X10 : man] : a = grade_of(X10) & f = grade_of(john) & ! [X8 : man,X9 : man] : created_equal(X8,X9)),
  file('TFF_Finite.s.p',prove_formulae)).
% SZS output end Proof for TFF_Finite.s