% 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