% 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(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, d_jon: human). tff(func_def_6, type, d_garfield: cat). tff(func_def_7, type, d_arlene: cat). tff(func_def_8, type, d_nermal: cat). tff(func_def_9, type, sK0: cat). tff(func_def_10, type, sK1: cat). tff(func_def_11, type, sK2: human). tff(pred_def_1, type, owns: (human * cat) > \$o). tff(f122,plain,( \$false), inference(avatar_sat_refutation,[],[f56,f66,f76,f86,f89,f92,f97,f121])). tff(f121,plain,( ~spl3_3), inference(avatar_contradiction_clause,[],[f120])). tff(f120,plain,( \$false | ~spl3_3), inference(subsumption_resolution,[],[f119,f36])). tff(f36,plain,( arlene != nermal), inference(definition_unfolding,[],[f19,f22,f23])). tff(f23,plain,( d_nermal = nermal), inference(cnf_transformation,[],[f5])). tff(f5,plain,( ~owns(d_jon,d_nermal) & ~owns(d_jon,d_arlene) & owns(d_jon,d_garfield) & d_garfield = loves(d_nermal) & d_garfield = loves(d_arlene) & d_garfield = loves(d_garfield) & d_nermal = nermal & d_arlene = arlene & d_garfield = garfield & d_jon = jon & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X0 : cat] : (d_nermal = X0 | d_arlene = X0 | d_garfield = X0) & ! [X1 : human] : d_jon = X1), inference(rectify,[],[f1])). tff(f1,axiom,( ~owns(d_jon,d_nermal) & ~owns(d_jon,d_arlene) & owns(d_jon,d_garfield) & d_garfield = loves(d_nermal) & d_garfield = loves(d_arlene) & d_garfield = loves(d_garfield) & d_nermal = nermal & d_arlene = arlene & d_garfield = garfield & d_jon = jon & d_arlene != d_nermal & d_garfield != d_nermal & d_garfield != d_arlene & ! [X1 : cat] : (d_nermal = X1 | d_arlene = X1 | d_garfield = X1) & ! [X0 : human] : d_jon = X0), file('TFF_Finite.s.p',unknown)). tff(f22,plain,( d_arlene = arlene), inference(cnf_transformation,[],[f5])). tff(f19,plain,( d_arlene != d_nermal), inference(cnf_transformation,[],[f5])). tff(f119,plain,( arlene = nermal | ~spl3_3), inference(subsumption_resolution,[],[f111,f30])). tff(f30,plain,( ~owns(jon,nermal)), inference(definition_unfolding,[],[f29,f20,f23])). tff(f20,plain,( d_jon = jon), inference(cnf_transformation,[],[f5])). tff(f29,plain,( ~owns(d_jon,d_nermal)), inference(cnf_transformation,[],[f5])). tff(f111,plain,( owns(jon,nermal) | arlene = nermal | ~spl3_3), inference(trivial_inequality_removal,[],[f107])). tff(f107,plain,( garfield != garfield | owns(jon,nermal) | arlene = nermal | ~spl3_3), inference(superposition,[],[f55,f33])). tff(f33,plain,( garfield = loves(nermal)), inference(definition_unfolding,[],[f26,f21,f23])). tff(f21,plain,( d_garfield = garfield), inference(cnf_transformation,[],[f5])). tff(f26,plain,( d_garfield = loves(d_nermal)), inference(cnf_transformation,[],[f5])). tff(f55,plain,( ( ! [X0 : cat] : (garfield != loves(X0) | owns(jon,X0) | arlene = X0) ) | ~spl3_3), inference(avatar_component_clause,[],[f54])). tff(f54,plain,( spl3_3 <=> ! [X0 : cat] : (owns(jon,X0) | garfield != loves(X0) | arlene = X0)), introduced(avatar_definition,[new_symbols(naming,[spl3_3])])). tff(f97,plain,( spl3_1 | spl3_4 | spl3_5), inference(avatar_contradiction_clause,[],[f96])). tff(f96,plain,( \$false | (spl3_1 | spl3_4 | spl3_5)), inference(subsumption_resolution,[],[f95,f75])). tff(f75,plain,( garfield != sK1 | spl3_5), inference(avatar_component_clause,[],[f74])). tff(f74,plain,( spl3_5 <=> garfield = sK1), introduced(avatar_definition,[new_symbols(naming,[spl3_5])])). tff(f95,plain,( garfield = sK1 | (spl3_1 | spl3_4)), inference(subsumption_resolution,[],[f94,f65])). tff(f65,plain,( arlene != sK1 | spl3_4), inference(avatar_component_clause,[],[f64])). tff(f64,plain,( spl3_4 <=> arlene = sK1), introduced(avatar_definition,[new_symbols(naming,[spl3_4])])). tff(f94,plain,( arlene = sK1 | garfield = sK1 | spl3_1), inference(trivial_inequality_removal,[],[f93])). tff(f93,plain,( nermal != nermal | arlene = sK1 | garfield = sK1 | spl3_1), inference(superposition,[],[f49,f39])). tff(f39,plain,( ( ! [X0 : cat] : (nermal = X0 | arlene = X0 | garfield = X0) )), inference(definition_unfolding,[],[f16,f23,f22,f21])). tff(f16,plain,( ( ! [X0 : cat] : (d_nermal = X0 | d_arlene = X0 | d_garfield = X0) )), inference(cnf_transformation,[],[f5])). tff(f49,plain,( nermal != sK1 | spl3_1), inference(avatar_component_clause,[],[f48])). tff(f48,plain,( spl3_1 <=> nermal = sK1), introduced(avatar_definition,[new_symbols(naming,[spl3_1])])). tff(f92,plain,( spl3_2 | ~spl3_7), inference(avatar_contradiction_clause,[],[f91])). tff(f91,plain,( \$false | (spl3_2 | ~spl3_7)), inference(subsumption_resolution,[],[f90,f34])). tff(f34,plain,( garfield = loves(arlene)), inference(definition_unfolding,[],[f25,f21,f22])). tff(f25,plain,( d_garfield = loves(d_arlene)), inference(cnf_transformation,[],[f5])). tff(f90,plain,( garfield != loves(arlene) | (spl3_2 | ~spl3_7)), inference(backward_demodulation,[],[f52,f85])). tff(f85,plain,( arlene = sK0 | ~spl3_7), inference(avatar_component_clause,[],[f84])). tff(f84,plain,( spl3_7 <=> arlene = sK0), introduced(avatar_definition,[new_symbols(naming,[spl3_7])])). tff(f52,plain,( garfield != loves(sK0) | spl3_2), inference(avatar_component_clause,[],[f51])). tff(f51,plain,( spl3_2 <=> garfield = loves(sK0)), introduced(avatar_definition,[new_symbols(naming,[spl3_2])])). tff(f89,plain,( spl3_2 | ~spl3_6), inference(avatar_contradiction_clause,[],[f88])). tff(f88,plain,( \$false | (spl3_2 | ~spl3_6)), inference(subsumption_resolution,[],[f87,f35])). tff(f35,plain,( garfield = loves(garfield)), inference(definition_unfolding,[],[f24,f21,f21])). tff(f24,plain,( d_garfield = loves(d_garfield)), inference(cnf_transformation,[],[f5])). tff(f87,plain,( garfield != loves(garfield) | (spl3_2 | ~spl3_6)), inference(backward_demodulation,[],[f52,f82])). tff(f82,plain,( garfield = sK0 | ~spl3_6), inference(avatar_component_clause,[],[f81])). tff(f81,plain,( spl3_6 <=> garfield = sK0), introduced(avatar_definition,[new_symbols(naming,[spl3_6])])). tff(f86,plain,( spl3_6 | spl3_7 | spl3_2), inference(avatar_split_clause,[],[f79,f51,f84,f81])). tff(f79,plain,( arlene = sK0 | garfield = sK0 | spl3_2), inference(subsumption_resolution,[],[f77,f33])). tff(f77,plain,( garfield != loves(nermal) | arlene = sK0 | garfield = sK0 | spl3_2), inference(superposition,[],[f52,f39])). tff(f76,plain,( ~spl3_5 | ~spl3_2 | spl3_3), inference(avatar_split_clause,[],[f72,f54,f51,f74])). tff(f72,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield != sK1) )), inference(subsumption_resolution,[],[f71,f40])). tff(f40,plain,( ( ! [X1 : human] : (jon = X1) )), inference(definition_unfolding,[],[f15,f20])). tff(f15,plain,( ( ! [X1 : human] : (d_jon = X1) )), inference(cnf_transformation,[],[f5])). tff(f71,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f70,f38])). tff(f38,plain,( garfield != arlene), inference(definition_unfolding,[],[f17,f21,f22])). tff(f17,plain,( d_garfield != d_arlene), inference(cnf_transformation,[],[f5])). tff(f70,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = arlene | garfield != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f69,f37])). tff(f37,plain,( garfield != nermal), inference(definition_unfolding,[],[f18,f21,f23])). tff(f18,plain,( d_garfield != d_nermal), inference(cnf_transformation,[],[f5])). tff(f69,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = nermal | garfield = arlene | garfield != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f68,f36])). tff(f68,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | arlene = nermal | garfield = nermal | garfield = arlene | garfield != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f67,f32])). tff(f32,plain,( owns(jon,garfield)), inference(definition_unfolding,[],[f27,f20,f21])). tff(f27,plain,( owns(d_jon,d_garfield)), inference(cnf_transformation,[],[f5])). tff(f67,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene | garfield != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f12,f31])). tff(f31,plain,( ~owns(jon,arlene)), inference(definition_unfolding,[],[f28,f20,f22])). tff(f28,plain,( ~owns(d_jon,d_arlene)), inference(cnf_transformation,[],[f5])). tff(f12,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 | garfield != sK1 | jon != sK2) )), inference(cnf_transformation,[],[f11])). tff(f11,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 | (nermal != sK1 & arlene != sK1 & garfield != sK1) | jon != sK2), inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f7,f10,f9,f8])). tff(f8,plain,( ? [X1 : cat] : garfield != loves(X1) => garfield != loves(sK0)), introduced(choice_axiom,[])). tff(f9,plain,( ? [X2 : cat] : (nermal != X2 & arlene != X2 & garfield != X2) => (nermal != sK1 & arlene != sK1 & garfield != sK1)), introduced(choice_axiom,[])). tff(f10,plain,( ? [X3 : human] : jon != X3 => jon != sK2), 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 | ? [X2 : cat] : (nermal != X2 & arlene != X2 & garfield != X2) | ? [X3 : human] : jon != X3), 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 | ? [X2 : cat] : (nermal != X2 & arlene != X2 & garfield != X2) | ? [X3 : human] : jon != X3), 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 & ! [X2 : cat] : (nermal = X2 | arlene = X2 | garfield = X2) & ! [X3 : human] : jon = X3)), inference(rectify,[],[f3])). tff(f3,negated_conjecture,( ~(~! [X3 : cat] : ((arlene != X3 & garfield = loves(X3)) => owns(jon,X3)) & ! [X3 : cat] : garfield = loves(X3) & ~owns(jon,arlene) & owns(jon,garfield) & arlene != nermal & garfield != nermal & garfield != arlene & ! [X3 : cat] : (nermal = X3 | arlene = X3 | garfield = X3) & ! [X2 : human] : jon = X2)), inference(negated_conjecture,[],[f2])). tff(f2,conjecture,( ~! [X3 : cat] : ((arlene != X3 & garfield = loves(X3)) => owns(jon,X3)) & ! [X3 : cat] : garfield = loves(X3) & ~owns(jon,arlene) & owns(jon,garfield) & arlene != nermal & garfield != nermal & garfield != arlene & ! [X3 : cat] : (nermal = X3 | arlene = X3 | garfield = X3) & ! [X2 : human] : jon = X2), file('TFF_Finite.s.p',unknown)). tff(f66,plain,( ~spl3_4 | ~spl3_2 | spl3_3), inference(avatar_split_clause,[],[f62,f54,f51,f64])). tff(f62,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | arlene != sK1) )), inference(subsumption_resolution,[],[f61,f40])). tff(f61,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | arlene != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f60,f38])). tff(f60,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = arlene | arlene != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f59,f37])). tff(f59,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = nermal | garfield = arlene | arlene != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f58,f36])). tff(f58,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | arlene = nermal | garfield = nermal | garfield = arlene | arlene != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f57,f32])). tff(f57,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene | arlene != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f13,f31])). tff(f13,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 | arlene != sK1 | jon != sK2) )), inference(cnf_transformation,[],[f11])). tff(f56,plain,( ~spl3_1 | ~spl3_2 | spl3_3), inference(avatar_split_clause,[],[f46,f54,f51,f48])). tff(f46,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | nermal != sK1) )), inference(subsumption_resolution,[],[f45,f40])). tff(f45,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | nermal != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f44,f38])). tff(f44,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = arlene | nermal != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f43,f37])). tff(f43,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | garfield = nermal | garfield = arlene | nermal != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f42,f36])). tff(f42,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | arlene = nermal | garfield = nermal | garfield = arlene | nermal != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f41,f32])). tff(f41,plain,( ( ! [X0 : cat] : (owns(jon,X0) | arlene = X0 | garfield != loves(X0) | garfield != loves(sK0) | ~owns(jon,garfield) | arlene = nermal | garfield = nermal | garfield = arlene | nermal != sK1 | jon != sK2) )), inference(subsumption_resolution,[],[f14,f31])). 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 | nermal != sK1 | jon != sK2) )), inference(cnf_transformation,[],[f11])). % SZS output end Proof for TFF_Finite.s