% 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