% SZS status Theorem for TFF_Finite.s
% SZS output start Proof for TFF_Finite.s
tff(type_def_5, type, human: $tType).
tff(type_def_6, type, cat: $tType).
tff(type_def_7, type, d_human: $tType).
tff(type_def_8, type, d_cat: $tType).
tff(func_def_0, type, jon: human).
tff(func_def_1, type, garfield: cat).
tff(func_def_2, type, arlene: cat).
tff(func_def_3, type, nermal: cat).
tff(func_def_4, type, loves: (cat) > cat).
tff(func_def_5, type, d2human: (d_human) > human).
tff(func_def_6, type, d2cat: (d_cat) > cat).
tff(func_def_7, type, d_jon: d_human).
tff(func_def_8, type, d_garfield: d_cat).
tff(func_def_9, type, d_arlene: d_cat).
tff(func_def_10, type, d_nermal: d_cat).
tff(func_def_11, type, sK0: cat).
tff(func_def_12, type, sK1: (cat) > d_cat).
tff(func_def_13, type, sK2: (human) > d_human).
tff(pred_def_1, type, owns: (human * cat) > $o).
tff(f325,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f61,f74,f286,f288,f290,f300,f306,f312,f322,f324])).
tff(f324,plain,(
  ~spl3_1),
  inference(avatar_contradiction_clause,[],[f323])).
tff(f323,plain,(
  $false | ~spl3_1),
  inference(subsumption_resolution,[],[f37,f105])).
tff(f105,plain,(
  garfield != arlene),
  inference(subsumption_resolution,[],[f102,f20])).
tff(f20,plain,(
  d_garfield != d_arlene),
  inference(cnf_transformation,[],[f13])).
tff(f13,plain,(
  ~owns(d2human(d_jon),d2cat(d_nermal)) & ~owns(d2human(d_jon),d2cat(d_arlene)) & owns(d2human(d_jon),d2cat(d_garfield)) & d2cat(d_garfield) = loves(d2cat(d_nermal)) & d2cat(d_garfield) = loves(d2cat(d_arlene)) & d2cat(d_garfield) = loves(d2cat(d_garfield)) & nermal = d2cat(d_nermal) & arlene = d2cat(d_arlene) & garfield = d2cat(d_garfield) & jon = d2human(d_jon) & ! [X0 : d_cat,X1 : d_cat] : (X0 = X1 | d2cat(X0) != d2cat(X1)) & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X2 : d_cat] : (d_nermal = X2 | d_arlene = X2 | d_garfield = X2) & ! [X3 : cat] : d2cat(sK1(X3)) = X3 & ! [X5 : d_human,X6 : d_human] : (X5 = X6 | d2human(X5) != d2human(X6)) & ! [X7 : d_human] : d_jon = X7 & ! [X8 : human] : d2human(sK2(X8)) = X8),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK1,sK2])],[f8,f12,f11])).
tff(f11,plain,(
  ! [X3 : cat] : (? [X4 : d_cat] : d2cat(X4) = X3 => d2cat(sK1(X3)) = X3)),
  introduced(choice_axiom,[])).
tff(f12,plain,(
  ! [X8 : human] : (? [X9 : d_human] : d2human(X9) = X8 => d2human(sK2(X8)) = X8)),
  introduced(choice_axiom,[])).
tff(f8,plain,(
  ~owns(d2human(d_jon),d2cat(d_nermal)) & ~owns(d2human(d_jon),d2cat(d_arlene)) & owns(d2human(d_jon),d2cat(d_garfield)) & d2cat(d_garfield) = loves(d2cat(d_nermal)) & d2cat(d_garfield) = loves(d2cat(d_arlene)) & d2cat(d_garfield) = loves(d2cat(d_garfield)) & nermal = d2cat(d_nermal) & arlene = d2cat(d_arlene) & garfield = d2cat(d_garfield) & jon = d2human(d_jon) & ! [X0 : d_cat,X1 : d_cat] : (X0 = X1 | d2cat(X0) != d2cat(X1)) & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X2 : d_cat] : (d_nermal = X2 | d_arlene = X2 | d_garfield = X2) & ! [X3 : cat] : ? [X4 : d_cat] : d2cat(X4) = X3 & ! [X5 : d_human,X6 : d_human] : (X5 = X6 | d2human(X5) != d2human(X6)) & ! [X7 : d_human] : d_jon = X7 & ! [X8 : human] : ? [X9 : d_human] : d2human(X9) = X8),
  inference(ennf_transformation,[],[f5])).
tff(f5,plain,(
  ~owns(d2human(d_jon),d2cat(d_nermal)) & ~owns(d2human(d_jon),d2cat(d_arlene)) & owns(d2human(d_jon),d2cat(d_garfield)) & d2cat(d_garfield) = loves(d2cat(d_nermal)) & d2cat(d_garfield) = loves(d2cat(d_arlene)) & d2cat(d_garfield) = loves(d2cat(d_garfield)) & nermal = d2cat(d_nermal) & arlene = d2cat(d_arlene) & garfield = d2cat(d_garfield) & jon = d2human(d_jon) & ! [X0 : d_cat,X1 : d_cat] : (d2cat(X0) = d2cat(X1) => X0 = X1) & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X2 : d_cat] : (d_nermal = X2 | d_arlene = X2 | d_garfield = X2) & ! [X3 : cat] : ? [X4 : d_cat] : d2cat(X4) = X3 & ! [X5 : d_human,X6 : d_human] : (d2human(X5) = d2human(X6) => X5 = X6) & ! [X7 : d_human] : d_jon = X7 & ! [X8 : human] : ? [X9 : d_human] : d2human(X9) = X8),
  inference(rectify,[],[f1])).
tff(f1,axiom,(
  ~owns(d2human(d_jon),d2cat(d_nermal)) & ~owns(d2human(d_jon),d2cat(d_arlene)) & owns(d2human(d_jon),d2cat(d_garfield)) & d2cat(d_garfield) = loves(d2cat(d_nermal)) & d2cat(d_garfield) = loves(d2cat(d_arlene)) & d2cat(d_garfield) = loves(d2cat(d_garfield)) & nermal = d2cat(d_nermal) & arlene = d2cat(d_arlene) & garfield = d2cat(d_garfield) & jon = d2human(d_jon) & ! [X6 : d_cat,X7 : d_cat] : (d2cat(X6) = d2cat(X7) => X6 = X7) & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X5 : d_cat] : (d_nermal = X5 | d_arlene = X5 | d_garfield = X5) & ! [X4 : cat] : ? [X5 : d_cat] : d2cat(X5) = X4 & ! [X2 : d_human,X3 : d_human] : (d2human(X2) = d2human(X3) => X2 = X3) & ! [X1 : d_human] : d_jon = X1 & ! [X0 : human] : ? [X1 : d_human] : d2human(X1) = X0),
  file('TFF_Finite.s.p',garfield)).
tff(f102,plain,(
  garfield != arlene | d_garfield = d_arlene),
  inference(superposition,[],[f92,f26])).
tff(f26,plain,(
  arlene = d2cat(d_arlene)),
  inference(cnf_transformation,[],[f13])).
tff(f92,plain,(
  ( ! [X0 : d_cat] : (garfield != d2cat(X0) | d_garfield = X0) )),
  inference(superposition,[],[f23,f25])).
tff(f25,plain,(
  garfield = d2cat(d_garfield)),
  inference(cnf_transformation,[],[f13])).
tff(f23,plain,(
  ( ! [X0 : d_cat,X1 : d_cat] : (d2cat(X0) != d2cat(X1) | X0 = X1) )),
  inference(cnf_transformation,[],[f13])).
tff(f37,plain,(
  garfield = arlene | ~spl3_1),
  inference(avatar_component_clause,[],[f35])).
tff(f35,plain,(
  spl3_1 <=> garfield = arlene),
  introduced(avatar_definition,[new_symbols(naming,[spl3_1])])).
tff(f322,plain,(
  spl3_6 | ~spl3_11),
  inference(avatar_contradiction_clause,[],[f321])).
tff(f321,plain,(
  $false | (spl3_6 | ~spl3_11)),
  inference(subsumption_resolution,[],[f320,f89])).
tff(f89,plain,(
  garfield = loves(arlene)),
  inference(forward_demodulation,[],[f88,f25])).
tff(f88,plain,(
  d2cat(d_garfield) = loves(arlene)),
  inference(forward_demodulation,[],[f29,f26])).
tff(f29,plain,(
  d2cat(d_garfield) = loves(d2cat(d_arlene))),
  inference(cnf_transformation,[],[f13])).
tff(f320,plain,(
  garfield != loves(arlene) | (spl3_6 | ~spl3_11)),
  inference(forward_demodulation,[],[f57,f275])).
tff(f275,plain,(
  arlene = sK0 | ~spl3_11),
  inference(avatar_component_clause,[],[f273])).
tff(f273,plain,(
  spl3_11 <=> arlene = sK0),
  introduced(avatar_definition,[new_symbols(naming,[spl3_11])])).
tff(f57,plain,(
  garfield != loves(sK0) | spl3_6),
  inference(avatar_component_clause,[],[f55])).
tff(f55,plain,(
  spl3_6 <=> garfield = loves(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl3_6])])).
tff(f312,plain,(
  spl3_6 | ~spl3_10),
  inference(avatar_contradiction_clause,[],[f311])).
tff(f311,plain,(
  $false | (spl3_6 | ~spl3_10)),
  inference(subsumption_resolution,[],[f309,f91])).
tff(f91,plain,(
  garfield = loves(nermal)),
  inference(forward_demodulation,[],[f90,f25])).
tff(f90,plain,(
  d2cat(d_garfield) = loves(nermal)),
  inference(forward_demodulation,[],[f30,f27])).
tff(f27,plain,(
  nermal = d2cat(d_nermal)),
  inference(cnf_transformation,[],[f13])).
tff(f30,plain,(
  d2cat(d_garfield) = loves(d2cat(d_nermal))),
  inference(cnf_transformation,[],[f13])).
tff(f309,plain,(
  garfield != loves(nermal) | (spl3_6 | ~spl3_10)),
  inference(backward_demodulation,[],[f57,f271])).
tff(f271,plain,(
  nermal = sK0 | ~spl3_10),
  inference(avatar_component_clause,[],[f269])).
tff(f269,plain,(
  spl3_10 <=> nermal = sK0),
  introduced(avatar_definition,[new_symbols(naming,[spl3_10])])).
tff(f306,plain,(
  spl3_10 | spl3_11 | spl3_6),
  inference(avatar_split_clause,[],[f305,f55,f273,f269])).
tff(f305,plain,(
  arlene = sK0 | nermal = sK0 | spl3_6),
  inference(forward_demodulation,[],[f304,f26])).
tff(f304,plain,(
  nermal = sK0 | d2cat(d_arlene) = sK0 | spl3_6),
  inference(subsumption_resolution,[],[f301,f87])).
tff(f87,plain,(
  garfield = loves(garfield)),
  inference(forward_demodulation,[],[f28,f25])).
tff(f28,plain,(
  d2cat(d_garfield) = loves(d2cat(d_garfield))),
  inference(cnf_transformation,[],[f13])).
tff(f301,plain,(
  garfield != loves(garfield) | nermal = sK0 | d2cat(d_arlene) = sK0 | spl3_6),
  inference(superposition,[],[f57,f209])).
tff(f209,plain,(
  ( ! [X2 : cat] : (garfield = X2 | nermal = X2 | d2cat(d_arlene) = X2) )),
  inference(superposition,[],[f18,f200])).
tff(f200,plain,(
  ( ! [X1 : cat] : (d_arlene = sK1(X1) | nermal = X1 | garfield = X1) )),
  inference(forward_demodulation,[],[f195,f27])).
tff(f195,plain,(
  ( ! [X1 : cat] : (d2cat(d_nermal) = X1 | d_arlene = sK1(X1) | garfield = X1) )),
  inference(superposition,[],[f18,f122])).
tff(f122,plain,(
  ( ! [X0 : cat] : (d_nermal = sK1(X0) | d_arlene = sK1(X0) | garfield = X0) )),
  inference(forward_demodulation,[],[f119,f25])).
tff(f119,plain,(
  ( ! [X0 : cat] : (d2cat(d_garfield) = X0 | d_arlene = sK1(X0) | d_nermal = sK1(X0)) )),
  inference(superposition,[],[f18,f19])).
tff(f19,plain,(
  ( ! [X2 : d_cat] : (d_garfield = X2 | d_arlene = X2 | d_nermal = X2) )),
  inference(cnf_transformation,[],[f13])).
tff(f18,plain,(
  ( ! [X3 : cat] : (d2cat(sK1(X3)) = X3) )),
  inference(cnf_transformation,[],[f13])).
tff(f300,plain,(
  ~spl3_7),
  inference(avatar_contradiction_clause,[],[f299])).
tff(f299,plain,(
  $false | ~spl3_7),
  inference(subsumption_resolution,[],[f298,f111])).
tff(f111,plain,(
  arlene != nermal),
  inference(subsumption_resolution,[],[f109,f22])).
tff(f22,plain,(
  d_arlene != d_nermal),
  inference(cnf_transformation,[],[f13])).
tff(f109,plain,(
  arlene != nermal | d_arlene = d_nermal),
  inference(superposition,[],[f93,f27])).
tff(f93,plain,(
  ( ! [X1 : d_cat] : (arlene != d2cat(X1) | d_arlene = X1) )),
  inference(superposition,[],[f23,f26])).
tff(f298,plain,(
  arlene = nermal | ~spl3_7),
  inference(subsumption_resolution,[],[f295,f91])).
tff(f295,plain,(
  garfield != loves(nermal) | arlene = nermal | ~spl3_7),
  inference(resolution,[],[f60,f85])).
tff(f85,plain,(
  ( ! [X0 : human] : (~owns(X0,nermal)) )),
  inference(superposition,[],[f82,f69])).
tff(f69,plain,(
  ( ! [X0 : human,X1 : human] : (X0 = X1) )),
  inference(superposition,[],[f67,f67])).
tff(f67,plain,(
  ( ! [X1 : human] : (jon = X1) )),
  inference(superposition,[],[f15,f63])).
tff(f63,plain,(
  ( ! [X0 : d_human] : (jon = d2human(X0)) )),
  inference(superposition,[],[f24,f62])).
tff(f62,plain,(
  ( ! [X0 : d_human,X1 : d_human] : (X0 = X1) )),
  inference(superposition,[],[f16,f16])).
tff(f16,plain,(
  ( ! [X7 : d_human] : (d_jon = X7) )),
  inference(cnf_transformation,[],[f13])).
tff(f24,plain,(
  jon = d2human(d_jon)),
  inference(cnf_transformation,[],[f13])).
tff(f15,plain,(
  ( ! [X8 : human] : (d2human(sK2(X8)) = X8) )),
  inference(cnf_transformation,[],[f13])).
tff(f82,plain,(
  ~owns(d2human(d_jon),nermal)),
  inference(forward_demodulation,[],[f33,f27])).
tff(f33,plain,(
  ~owns(d2human(d_jon),d2cat(d_nermal))),
  inference(cnf_transformation,[],[f13])).
tff(f60,plain,(
  ( ! [X0 : cat] : (owns(jon,X0) | garfield != loves(X0) | arlene = X0) ) | ~spl3_7),
  inference(avatar_component_clause,[],[f59])).
tff(f59,plain,(
  spl3_7 <=> ! [X0 : cat] : (owns(jon,X0) | garfield != loves(X0) | arlene = X0)),
  introduced(avatar_definition,[new_symbols(naming,[spl3_7])])).
tff(f290,plain,(
  ~spl3_5),
  inference(avatar_contradiction_clause,[],[f289])).
tff(f289,plain,(
  $false | ~spl3_5),
  inference(subsumption_resolution,[],[f53,f80])).
tff(f80,plain,(
  ( ! [X0 : human] : (~owns(X0,arlene)) )),
  inference(superposition,[],[f77,f69])).
tff(f77,plain,(
  ~owns(d2human(d_jon),arlene)),
  inference(forward_demodulation,[],[f32,f26])).
tff(f32,plain,(
  ~owns(d2human(d_jon),d2cat(d_arlene))),
  inference(cnf_transformation,[],[f13])).
tff(f53,plain,(
  owns(jon,arlene) | ~spl3_5),
  inference(avatar_component_clause,[],[f51])).
tff(f51,plain,(
  spl3_5 <=> owns(jon,arlene)),
  introduced(avatar_definition,[new_symbols(naming,[spl3_5])])).
tff(f288,plain,(
  ~spl3_2),
  inference(avatar_contradiction_clause,[],[f287])).
tff(f287,plain,(
  $false | ~spl3_2),
  inference(subsumption_resolution,[],[f41,f106])).
tff(f106,plain,(
  garfield != nermal),
  inference(subsumption_resolution,[],[f103,f21])).
tff(f21,plain,(
  d_garfield != d_nermal),
  inference(cnf_transformation,[],[f13])).
tff(f103,plain,(
  garfield != nermal | d_garfield = d_nermal),
  inference(superposition,[],[f92,f27])).
tff(f41,plain,(
  garfield = nermal | ~spl3_2),
  inference(avatar_component_clause,[],[f39])).
tff(f39,plain,(
  spl3_2 <=> garfield = nermal),
  introduced(avatar_definition,[new_symbols(naming,[spl3_2])])).
tff(f286,plain,(
  ~spl3_3),
  inference(avatar_contradiction_clause,[],[f285])).
tff(f285,plain,(
  $false | ~spl3_3),
  inference(subsumption_resolution,[],[f45,f111])).
tff(f45,plain,(
  arlene = nermal | ~spl3_3),
  inference(avatar_component_clause,[],[f43])).
tff(f43,plain,(
  spl3_3 <=> arlene = nermal),
  introduced(avatar_definition,[new_symbols(naming,[spl3_3])])).
tff(f74,plain,(
  spl3_4),
  inference(avatar_contradiction_clause,[],[f73])).
tff(f73,plain,(
  $false | spl3_4),
  inference(subsumption_resolution,[],[f72,f70])).
tff(f70,plain,(
  ( ! [X0 : human] : (~owns(X0,garfield)) ) | spl3_4),
  inference(superposition,[],[f49,f67])).
tff(f49,plain,(
  ~owns(jon,garfield) | spl3_4),
  inference(avatar_component_clause,[],[f47])).
tff(f47,plain,(
  spl3_4 <=> owns(jon,garfield)),
  introduced(avatar_definition,[new_symbols(naming,[spl3_4])])).
tff(f72,plain,(
  owns(d2human(d_jon),garfield)),
  inference(forward_demodulation,[],[f31,f25])).
tff(f31,plain,(
  owns(d2human(d_jon),d2cat(d_garfield))),
  inference(cnf_transformation,[],[f13])).
tff(f61,plain,(
  spl3_1 | spl3_2 | spl3_3 | ~spl3_4 | spl3_5 | ~spl3_6 | spl3_7),
  inference(avatar_split_clause,[],[f14,f59,f55,f51,f47,f43,f39,f35])).
tff(f14,plain,(
  ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | owns(jon,arlene) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene) )),
  inference(cnf_transformation,[],[f10])).
tff(f10,plain,(
  ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0)) | garfield != loves(sK0) | owns(jon,arlene) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f7,f9])).
tff(f9,plain,(
  ? [X1 : cat] : garfield != loves(X1) => garfield != loves(sK0)),
  introduced(choice_axiom,[])).
tff(f7,plain,(
  ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0)) | ? [X1 : cat] : garfield != loves(X1) | owns(jon,arlene) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene),
  inference(flattening,[],[f6])).
tff(f6,plain,(
  ! [X0 : cat] : (owns(jon,X0) | (arlene = X0 | garfield != loves(X0))) | ? [X1 : cat] : garfield != loves(X1) | owns(jon,arlene) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene),
  inference(ennf_transformation,[],[f4])).
tff(f4,plain,(
  ~(~! [X0 : cat] : ((arlene != X0 & garfield = loves(X0)) => owns(jon,X0)) & ! [X1 : cat] : garfield = loves(X1) & ~owns(jon,arlene) & owns(jon,garfield) & arlene != nermal & garfield != nermal & garfield != arlene)),
  inference(rectify,[],[f3])).
tff(f3,negated_conjecture,(
  ~(~! [X4 : cat] : ((arlene != X4 & garfield = loves(X4)) => owns(jon,X4)) & ! [X4 : cat] : garfield = loves(X4) & ~owns(jon,arlene) & owns(jon,garfield) & arlene != nermal & garfield != nermal & garfield != arlene)),
  inference(negated_conjecture,[],[f2])).
tff(f2,conjecture,(
  ~! [X4 : cat] : ((arlene != X4 & garfield = loves(X4)) => owns(jon,X4)) & ! [X4 : cat] : garfield = loves(X4) & ~owns(jon,arlene) & owns(jon,garfield) & arlene != nermal & garfield != nermal & garfield != arlene),
  file('TFF_Finite.s.p',verify)).
% SZS output end Proof for TFF_Finite.s