% SZS status Theorem for TFF_Peano.s % SZS output start Proof for TFF_Peano.s tff(type_def_5, type, person: \$tType). tff(type_def_6, type, peano: \$tType). tff(func_def_0, type, bob: person). tff(func_def_1, type, child_of: person > person). tff(func_def_2, type, zero: peano). tff(func_def_3, type, s: peano > peano). tff(func_def_4, type, peano2person: peano > person). tff(func_def_5, type, sK0: person). tff(func_def_6, type, sK1: person). tff(func_def_7, type, sK2: person). tff(func_def_8, type, sK3: person). tff(func_def_9, type, sK4: person). tff(func_def_10, type, sK5: person). tff(func_def_11, type, sK6: person). tff(func_def_12, type, sK7: peano > peano). tff(func_def_13, type, sK8: person > peano). tff(func_def_14, type, sF9: person). tff(pred_def_1, type, is_descendant: (person * person) > \$o). tff(pred_def_2, type, peano_less: (peano * peano) > \$o). tff(f3793,plain,( \$false), inference(subsumption_resolution,[],[f3792,f3724])). tff(f3724,plain,( ~is_descendant(sK2,sK4)), inference(subsumption_resolution,[],[f3723,f90])). tff(f90,plain,( is_descendant(sK1,sF9)), inference(superposition,[],[f81,f42])). tff(f42,plain,( child_of(sK1) = sF9), introduced(function_definition,[new_symbols(definition,[sF9])])). tff(f81,plain,( ( ! [X0 : person] : (is_descendant(X0,child_of(X0))) )), inference(forward_demodulation,[],[f74,f50])). tff(f50,plain,( ( ! [X0 : person] : (child_of(X0) = peano2person(s(sK8(X0)))) )), inference(superposition,[],[f32,f25])). tff(f25,plain,( ( ! [X10 : person] : (peano2person(sK8(X10)) = X10) )), inference(cnf_transformation,[],[f18])). tff(f18,plain,( ! [X0 : peano,X1 : peano] : ((is_descendant(peano2person(X0),peano2person(X1)) | ~peano_less(X0,X1)) & (peano_less(X0,X1) | ~is_descendant(peano2person(X0),peano2person(X1)))) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | ~peano_less(X4,X5) | ~peano_less(X3,X4)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (s(sK7(X8)) = X8 | zero = X8) & ! [X10 : person] : peano2person(sK8(X10)) = X10), inference(skolemisation,[status(esa),new_symbols(skolem,[sK7,sK8])],[f15,f17,f16])). tff(f16,plain,( ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 => s(sK7(X8)) = X8)), introduced(choice_axiom,[])). tff(f17,plain,( ! [X10 : person] : (? [X11 : peano] : peano2person(X11) = X10 => peano2person(sK8(X10)) = X10)), introduced(choice_axiom,[])). tff(f15,plain,( ! [X0 : peano,X1 : peano] : ((is_descendant(peano2person(X0),peano2person(X1)) | ~peano_less(X0,X1)) & (peano_less(X0,X1) | ~is_descendant(peano2person(X0),peano2person(X1)))) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | ~peano_less(X4,X5) | ~peano_less(X3,X4)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10), inference(nnf_transformation,[],[f9])). tff(f9,plain,( ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | ~peano_less(X4,X5) | ~peano_less(X3,X4)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10), inference(flattening,[],[f8])). tff(f8,plain,( ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((X3 != X4 | ~peano_less(X3,X4)) & (peano_less(X3,X5) | (~peano_less(X4,X5) | ~peano_less(X3,X4))) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (X6 = X7 | peano2person(X6) != peano2person(X7)) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10), inference(ennf_transformation,[],[f5])). tff(f5,plain,( ! [X0 : peano,X1 : peano] : (is_descendant(peano2person(X0),peano2person(X1)) <=> peano_less(X0,X1)) & ! [X2 : peano] : child_of(peano2person(X2)) = peano2person(s(X2)) & bob = peano2person(zero) & ! [X3 : peano,X4 : peano,X5 : peano] : ((peano_less(X3,X4) => X3 != X4) & ((peano_less(X4,X5) & peano_less(X3,X4)) => peano_less(X3,X5)) & peano_less(X3,s(X3))) & ! [X6 : peano,X7 : peano] : (peano2person(X6) = peano2person(X7) => X6 = X7) & ! [X8 : peano] : (? [X9 : peano] : s(X9) = X8 | zero = X8) & ! [X10 : person] : ? [X11 : peano] : peano2person(X11) = X10), inference(rectify,[],[f1])). tff(f1,axiom,( ! [X5 : peano,X6 : peano] : (is_descendant(peano2person(X5),peano2person(X6)) <=> peano_less(X5,X6)) & ! [X1 : peano] : child_of(peano2person(X1)) = peano2person(s(X1)) & bob = peano2person(zero) & ! [X2 : peano,X3 : peano,X4 : peano] : ((peano_less(X2,X3) => X2 != X3) & ((peano_less(X3,X4) & peano_less(X2,X3)) => peano_less(X2,X4)) & peano_less(X2,s(X2))) & ! [X2 : peano,X3 : peano] : (peano2person(X2) = peano2person(X3) => X2 = X3) & ! [X1 : peano] : (? [X0 : peano] : s(X0) = X1 | zero = X1) & ! [X0 : person] : ? [X1 : peano] : peano2person(X1) = X0), file('TFF_Peano.s.p',unknown)). tff(f32,plain,( ( ! [X2 : peano] : (child_of(peano2person(X2)) = peano2person(s(X2))) )), inference(cnf_transformation,[],[f18])). tff(f74,plain,( ( ! [X0 : person] : (is_descendant(X0,peano2person(s(sK8(X0))))) )), inference(superposition,[],[f68,f25])). tff(f68,plain,( ( ! [X0 : peano] : (is_descendant(peano2person(X0),peano2person(s(X0)))) )), inference(resolution,[],[f34,f28])). tff(f28,plain,( ( ! [X3 : peano] : (peano_less(X3,s(X3))) )), inference(cnf_transformation,[],[f18])). tff(f34,plain,( ( ! [X0 : peano,X1 : peano] : (~peano_less(X0,X1) | is_descendant(peano2person(X0),peano2person(X1))) )), inference(cnf_transformation,[],[f18])). tff(f3723,plain,( ~is_descendant(sK2,sK4) | ~is_descendant(sK1,sF9)), inference(subsumption_resolution,[],[f3714,f65])). tff(f65,plain,( ( ! [X0 : person] : (~is_descendant(X0,X0)) )), inference(superposition,[],[f63,f25])). tff(f63,plain,( ( ! [X0 : peano] : (~is_descendant(peano2person(X0),peano2person(X0))) )), inference(resolution,[],[f33,f41])). tff(f41,plain,( ( ! [X4 : peano] : (~peano_less(X4,X4)) )), inference(equality_resolution,[],[f30])). tff(f30,plain,( ( ! [X3 : peano,X4 : peano] : (X3 != X4 | ~peano_less(X3,X4)) )), inference(cnf_transformation,[],[f18])). tff(f33,plain,( ( ! [X0 : peano,X1 : peano] : (peano_less(X0,X1) | ~is_descendant(peano2person(X0),peano2person(X1))) )), inference(cnf_transformation,[],[f18])). tff(f3714,plain,( is_descendant(sK5,sK5) | ~is_descendant(sK2,sK4) | ~is_descendant(sK1,sF9)), inference(backward_demodulation,[],[f44,f3713])). tff(f3713,plain,( sK5 = sK6), inference(subsumption_resolution,[],[f3712,f90])). tff(f3712,plain,( sK5 = sK6 | ~is_descendant(sK1,sF9)), inference(duplicate_literal_removal,[],[f3709])). tff(f3709,plain,( sK5 = sK6 | ~is_descendant(sK1,sF9) | sK5 = sK6), inference(resolution,[],[f3688,f43])). tff(f43,plain,( ~is_descendant(sK2,sK4) | ~is_descendant(sK1,sF9) | sK5 = sK6), inference(definition_folding,[],[f35,f42])). tff(f35,plain,( ~is_descendant(sK1,child_of(sK1)) | ~is_descendant(sK2,sK4) | sK5 = sK6), inference(equality_resolution,[],[f24])). tff(f24,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | ~is_descendant(sK2,sK4) | sK5 = sK6) )), inference(cnf_transformation,[],[f14])). tff(f14,plain,( ! [X1 : person] : child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | (~is_descendant(sK2,sK4) & is_descendant(sK3,sK4) & is_descendant(sK2,sK3)) | (sK5 = sK6 & is_descendant(sK5,sK6))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6])],[f7,f13,f12,f11,f10])). tff(f10,plain,( ? [X0 : person] : ! [X1 : person] : child_of(X0) != X1 => ! [X1 : person] : child_of(sK0) != X1), introduced(choice_axiom,[])). tff(f11,plain,( ? [X2 : person] : ~is_descendant(X2,child_of(X2)) => ~is_descendant(sK1,child_of(sK1))), introduced(choice_axiom,[])). tff(f12,plain,( ? [X3 : person,X4 : person,X5 : person] : (~is_descendant(X3,X5) & is_descendant(X4,X5) & is_descendant(X3,X4)) => (~is_descendant(sK2,sK4) & is_descendant(sK3,sK4) & is_descendant(sK2,sK3))), introduced(choice_axiom,[])). tff(f13,plain,( ? [X6 : person,X7 : person] : (X6 = X7 & is_descendant(X6,X7)) => (sK5 = sK6 & is_descendant(sK5,sK6))), introduced(choice_axiom,[])). tff(f7,plain,( ? [X0 : person] : ! [X1 : person] : child_of(X0) != X1 | ? [X2 : person] : ~is_descendant(X2,child_of(X2)) | ? [X3 : person,X4 : person,X5 : person] : (~is_descendant(X3,X5) & is_descendant(X4,X5) & is_descendant(X3,X4)) | ? [X6 : person,X7 : person] : (X6 = X7 & is_descendant(X6,X7))), inference(flattening,[],[f6])). tff(f6,plain,( ? [X0 : person] : ! [X1 : person] : child_of(X0) != X1 | ? [X2 : person] : ~is_descendant(X2,child_of(X2)) | ? [X3 : person,X4 : person,X5 : person] : (~is_descendant(X3,X5) & (is_descendant(X4,X5) & is_descendant(X3,X4))) | ? [X6 : person,X7 : person] : (X6 = X7 & is_descendant(X6,X7))), inference(ennf_transformation,[],[f4])). tff(f4,plain,( ~(! [X0 : person] : ? [X1 : person] : child_of(X0) = X1 & ! [X2 : person] : is_descendant(X2,child_of(X2)) & ! [X3 : person,X4 : person,X5 : person] : ((is_descendant(X4,X5) & is_descendant(X3,X4)) => is_descendant(X3,X5)) & ! [X6 : person,X7 : person] : (is_descendant(X6,X7) => X6 != X7))), inference(rectify,[],[f3])). tff(f3,negated_conjecture,( ~(! [X0 : person] : ? [X7 : person] : child_of(X0) = X7 & ! [X0 : person] : is_descendant(X0,child_of(X0)) & ! [X5 : person,X7 : person,X8 : person] : ((is_descendant(X7,X8) & is_descendant(X5,X7)) => is_descendant(X5,X8)) & ! [X5 : person,X6 : person] : (is_descendant(X5,X6) => X5 != X6))), inference(negated_conjecture,[],[f2])). tff(f2,conjecture,( ! [X0 : person] : ? [X7 : person] : child_of(X0) = X7 & ! [X0 : person] : is_descendant(X0,child_of(X0)) & ! [X5 : person,X7 : person,X8 : person] : ((is_descendant(X7,X8) & is_descendant(X5,X7)) => is_descendant(X5,X8)) & ! [X5 : person,X6 : person] : (is_descendant(X5,X6) => X5 != X6)), file('TFF_Peano.s.p',unknown)). tff(f3688,plain,( is_descendant(sK2,sK4) | sK5 = sK6), inference(subsumption_resolution,[],[f3687,f90])). tff(f3687,plain,( is_descendant(sK2,sK4) | sK5 = sK6 | ~is_descendant(sK1,sF9)), inference(duplicate_literal_removal,[],[f3686])). tff(f3686,plain,( is_descendant(sK2,sK4) | sK5 = sK6 | ~is_descendant(sK1,sF9) | sK5 = sK6), inference(resolution,[],[f3633,f47])). tff(f47,plain,( is_descendant(sK2,sK3) | ~is_descendant(sK1,sF9) | sK5 = sK6), inference(definition_folding,[],[f39,f42])). tff(f39,plain,( ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK2,sK3) | sK5 = sK6), inference(equality_resolution,[],[f20])). tff(f20,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK2,sK3) | sK5 = sK6) )), inference(cnf_transformation,[],[f14])). tff(f3633,plain,( ( ! [X0 : person] : (~is_descendant(X0,sK3) | is_descendant(X0,sK4) | sK5 = sK6) )), inference(subsumption_resolution,[],[f3628,f90])). tff(f3628,plain,( ( ! [X0 : person] : (is_descendant(X0,sK4) | ~is_descendant(X0,sK3) | ~is_descendant(sK1,sF9) | sK5 = sK6) )), inference(resolution,[],[f3428,f45])). tff(f45,plain,( is_descendant(sK3,sK4) | ~is_descendant(sK1,sF9) | sK5 = sK6), inference(definition_folding,[],[f37,f42])). tff(f37,plain,( ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK3,sK4) | sK5 = sK6), inference(equality_resolution,[],[f22])). tff(f22,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK3,sK4) | sK5 = sK6) )), inference(cnf_transformation,[],[f14])). tff(f3428,plain,( ( ! [X2 : person,X0 : person,X1 : person] : (~is_descendant(X2,X1) | is_descendant(X0,X1) | ~is_descendant(X0,X2)) )), inference(superposition,[],[f1662,f25])). tff(f1662,plain,( ( ! [X2 : peano,X0 : person,X1 : person] : (is_descendant(peano2person(X2),X0) | ~is_descendant(X1,X0) | ~is_descendant(peano2person(X2),X1)) )), inference(superposition,[],[f822,f25])). tff(f822,plain,( ( ! [X2 : peano,X0 : person,X1 : peano] : (~is_descendant(X0,peano2person(X1)) | is_descendant(peano2person(X2),peano2person(X1)) | ~is_descendant(peano2person(X2),X0)) )), inference(superposition,[],[f278,f25])). tff(f278,plain,( ( ! [X2 : peano,X0 : peano,X1 : peano] : (~is_descendant(peano2person(X2),peano2person(X1)) | is_descendant(peano2person(X0),peano2person(X1)) | ~is_descendant(peano2person(X0),peano2person(X2))) )), inference(resolution,[],[f105,f33])). tff(f105,plain,( ( ! [X2 : peano,X0 : peano,X1 : peano] : (~peano_less(X0,X1) | is_descendant(peano2person(X0),peano2person(X2)) | ~is_descendant(peano2person(X1),peano2person(X2))) )), inference(resolution,[],[f72,f33])). tff(f72,plain,( ( ! [X2 : peano,X0 : peano,X1 : peano] : (~peano_less(X0,X1) | ~peano_less(X2,X0) | is_descendant(peano2person(X2),peano2person(X1))) )), inference(resolution,[],[f29,f34])). tff(f29,plain,( ( ! [X3 : peano,X4 : peano,X5 : peano] : (peano_less(X3,X5) | ~peano_less(X4,X5) | ~peano_less(X3,X4)) )), inference(cnf_transformation,[],[f18])). tff(f44,plain,( is_descendant(sK5,sK6) | ~is_descendant(sK2,sK4) | ~is_descendant(sK1,sF9)), inference(definition_folding,[],[f36,f42])). tff(f36,plain,( ~is_descendant(sK1,child_of(sK1)) | ~is_descendant(sK2,sK4) | is_descendant(sK5,sK6)), inference(equality_resolution,[],[f23])). tff(f23,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | ~is_descendant(sK2,sK4) | is_descendant(sK5,sK6)) )), inference(cnf_transformation,[],[f14])). tff(f3792,plain,( is_descendant(sK2,sK4)), inference(resolution,[],[f3729,f3728])). tff(f3728,plain,( is_descendant(sK2,sK3)), inference(subsumption_resolution,[],[f3727,f90])). tff(f3727,plain,( is_descendant(sK2,sK3) | ~is_descendant(sK1,sF9)), inference(subsumption_resolution,[],[f3716,f65])). tff(f3716,plain,( is_descendant(sK5,sK5) | is_descendant(sK2,sK3) | ~is_descendant(sK1,sF9)), inference(backward_demodulation,[],[f48,f3713])). tff(f48,plain,( is_descendant(sK5,sK6) | is_descendant(sK2,sK3) | ~is_descendant(sK1,sF9)), inference(definition_folding,[],[f40,f42])). tff(f40,plain,( ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK2,sK3) | is_descendant(sK5,sK6)), inference(equality_resolution,[],[f19])). tff(f19,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK2,sK3) | is_descendant(sK5,sK6)) )), inference(cnf_transformation,[],[f14])). tff(f3729,plain,( ( ! [X0 : person] : (~is_descendant(X0,sK3) | is_descendant(X0,sK4)) )), inference(resolution,[],[f3726,f3428])). tff(f3726,plain,( is_descendant(sK3,sK4)), inference(subsumption_resolution,[],[f3725,f90])). tff(f3725,plain,( is_descendant(sK3,sK4) | ~is_descendant(sK1,sF9)), inference(subsumption_resolution,[],[f3715,f65])). tff(f3715,plain,( is_descendant(sK5,sK5) | is_descendant(sK3,sK4) | ~is_descendant(sK1,sF9)), inference(backward_demodulation,[],[f46,f3713])). tff(f46,plain,( is_descendant(sK5,sK6) | is_descendant(sK3,sK4) | ~is_descendant(sK1,sF9)), inference(definition_folding,[],[f38,f42])). tff(f38,plain,( ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK3,sK4) | is_descendant(sK5,sK6)), inference(equality_resolution,[],[f21])). tff(f21,plain,( ( ! [X1 : person] : (child_of(sK0) != X1 | ~is_descendant(sK1,child_of(sK1)) | is_descendant(sK3,sK4) | is_descendant(sK5,sK6)) )), inference(cnf_transformation,[],[f14])). % SZS output end Proof for TFF_Peano.s