% SZS status Theorem for NTF_Infinite-Finite.s % SZS output start Proof for NTF_Infinite-Finite.s tff(type_def_5, type, '\$ki_world': \$tType). tff(type_def_6, type, person: \$tType). tff(func_def_0, type, '\$local_ki_world': '\$ki_world'). tff(func_def_1, type, geoff: person). tff(func_def_2, type, id_of: (person) > \$int). tff(func_def_3, type, int2ki_world: (\$int) > '\$ki_world'). tff(func_def_4, type, int2person: (\$int) > person). tff(func_def_11, type, bG0: (person) > \$o). tff(func_def_12, type, sK1: person). tff(func_def_13, type, sK2: \$int). tff(func_def_14, type, sK3: person). tff(func_def_15, type, sK4: person). tff(func_def_16, type, sK5: \$int). tff(func_def_17, type, sK6: (person) > person). tff(func_def_18, type, sK7: (person) > \$int). tff(func_def_19, type, sK8: (person) > \$int). tff(func_def_20, type, sK9: ('\$ki_world') > \$int). tff(func_def_21, type, sK10: (\$int) > '\$ki_world'). tff(func_def_22, type, sK11: ('\$ki_world' * \$o) > '\$ki_world'). tff(func_def_23, type, sK12: ('\$ki_world' * \$o) > '\$ki_world'). tff(pred_def_1, type, '\$accessible_ki_world': ('\$ki_world' * '\$ki_world') > \$o). tff(pred_def_2, type, '\$in_ki_world': ('\$ki_world') > \$o). tff(pred_def_3, type, '\$necessary': (\$o) > \$o). tff(pred_def_4, type, '\$possible': (\$o) > \$o). tff(pred_def_5, type, like: (person) > \$o). tff(f4159,plain,( \$false), inference(avatar_smt_refutation,[],[f111,f116,f124,f133,f135,f141,f154,f159,f165,f171,f173,f185,f194,f199,f206,f207,f233,f244,f274,f275,f276,f283,f335,f351,f383,f388,f393,f403,f415,f444,f461,f487,f488,f517,f524,f537,f552,f560,f575,f576,f603,f654,f783,f893,f894,f927,f967,f1111,f1116,f1333,f1334,f1380,f1422,f1501,f1502,f1662,f1668,f1924,f1927,f1967,f1968,f1988,f1992,f1999,f2007,f2051,f2068,f2186,f2322,f2620,f2672,f2677,f3008,f3025,f3084,f3230,f3278,f3427,f3438,f3450,f3457,f3473,f3482,f3499,f3510,f3515,f3528,f3547,f3559,f3577,f3614,f3619,f3620,f3635,f3670,f3672,f3692,f3700,f3714,f3723,f3754,f3782,f3783,f3814,f3833,f3862,f3863,f3864,f3880,f3893,f3898,f3927,f3930,f3969,f3978,f3988,f3992,f3993,f3994,f4010,f4014,f4031,f4033,f4053,f4054,f4073,f4117,f4121,f4126,f4158])). tff(f4158,plain,( spl13_15 | spl13_74 | ~spl13_16 | ~spl13_70 | ~spl13_83), inference(avatar_split_clause,[],[f4155,f3697,f3479,f203,f3522,f197])). tff(f197,plain,( spl13_15 <=> ! [X6 : person] : (sK6(X6) != X6 | ~like(X6))), introduced(avatar_definition,[new_symbols(naming,[spl13_15])])). tff(f3522,plain,( spl13_74 <=> ! [X4 : person] : id_of(X4) != sK2), introduced(avatar_definition,[new_symbols(naming,[spl13_74])])). tff(f203,plain,( spl13_16 <=> like(geoff)), introduced(avatar_definition,[new_symbols(naming,[spl13_16])])). tff(f3479,plain,( spl13_70 <=> '\$possible'(bG0(sK1))), introduced(avatar_definition,[new_symbols(naming,[spl13_70])])). tff(f3697,plain,( spl13_83 <=> sK3 = sK4), introduced(avatar_definition,[new_symbols(naming,[spl13_83])])). tff(f4155,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(X4) != sK2 | sK6(X6) != X6 | ~like(X6)) ) | ~spl13_83), inference(trivial_inequality_removal,[],[f4154])). tff(f4154,plain,( ( ! [X6 : person,X4 : person] : (sK3 != sK3 | ~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(X4) != sK2 | sK6(X6) != X6 | ~like(X6)) ) | ~spl13_83), inference(forward_demodulation,[],[f77,f3699])). tff(f3699,plain,( sK3 = sK4 | ~spl13_83), inference(avatar_component_clause,[],[f3697])). tff(f77,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | sK3 != sK4 | id_of(X4) != sK2 | sK6(X6) != X6 | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f45,plain,( ((~'\$possible'(bG0(sK1)) | ~like(geoff) | (((sK3 != sK4 & id_of(sK3) = id_of(sK4)) | ! [X4 : person] : id_of(X4) != sK2) & ~\$less(sK2,0))) & '\$in_ki_world'('\$local_ki_world')) | (! [X6 : person] : ((sK6(X6) != X6 & like(sK6(X6))) | ~like(X6)) & '\$in_ki_world'(int2ki_world(sK5)) & ~\$less(sK5,0))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6])],[f33,f44,f43,f42,f41,f40])). tff(f40,plain,( ? [X0 : person] : ~'\$possible'(bG0(X0)) => ~'\$possible'(bG0(sK1))), introduced(choice_axiom,[])). tff(f41,plain,( ? [X1 : \$int] : ((? [X2 : person,X3 : person] : (X2 != X3 & id_of(X2) = id_of(X3)) | ! [X4 : person] : id_of(X4) != X1) & ~\$less(X1,0)) => ((? [X2 : person,X3 : person] : (X2 != X3 & id_of(X2) = id_of(X3)) | ! [X4 : person] : id_of(X4) != sK2) & ~\$less(sK2,0))), introduced(choice_axiom,[])). tff(f42,plain,( ? [X2 : person,X3 : person] : (X2 != X3 & id_of(X2) = id_of(X3)) => (sK3 != sK4 & id_of(sK3) = id_of(sK4))), introduced(choice_axiom,[])). tff(f43,plain,( ? [X5 : \$int] : (! [X6 : person] : (? [X7 : person] : (X6 != X7 & like(X7)) | ~like(X6)) & '\$in_ki_world'(int2ki_world(X5)) & ~\$less(X5,0)) => (! [X6 : person] : (? [X7 : person] : (X6 != X7 & like(X7)) | ~like(X6)) & '\$in_ki_world'(int2ki_world(sK5)) & ~\$less(sK5,0))), introduced(choice_axiom,[])). tff(f44,plain,( ! [X6 : person] : (? [X7 : person] : (X6 != X7 & like(X7)) => (sK6(X6) != X6 & like(sK6(X6))))), introduced(choice_axiom,[])). tff(f33,plain,( ((? [X0 : person] : ~'\$possible'(bG0(X0)) | ~like(geoff) | ? [X1 : \$int] : ((? [X2 : person,X3 : person] : (X2 != X3 & id_of(X2) = id_of(X3)) | ! [X4 : person] : id_of(X4) != X1) & ~\$less(X1,0))) & '\$in_ki_world'('\$local_ki_world')) | ? [X5 : \$int] : (! [X6 : person] : (? [X7 : person] : (X6 != X7 & like(X7)) | ~like(X6)) & '\$in_ki_world'(int2ki_world(X5)) & ~\$less(X5,0))), inference(flattening,[],[f32])). tff(f32,plain,( ((? [X0 : person] : ~'\$possible'(bG0(X0)) | ~like(geoff) | ? [X1 : \$int] : ((? [X2 : person,X3 : person] : (X2 != X3 & id_of(X2) = id_of(X3)) | ! [X4 : person] : id_of(X4) != X1) & ~\$less(X1,0))) & '\$in_ki_world'('\$local_ki_world')) | ? [X5 : \$int] : (! [X6 : person] : (? [X7 : person] : (X6 != X7 & like(X7)) | ~like(X6)) & ('\$in_ki_world'(int2ki_world(X5)) & ~\$less(X5,0)))), inference(ennf_transformation,[],[f26])). tff(f26,plain,( ~(('\$in_ki_world'('\$local_ki_world') => (! [X0 : person] : '\$possible'(bG0(X0)) & like(geoff) & ! [X1 : \$int] : (~\$less(X1,0) => (! [X2 : person,X3 : person] : (id_of(X2) = id_of(X3) => X2 = X3) & ? [X4 : person] : id_of(X4) = X1)))) & ! [X5 : \$int] : (('\$in_ki_world'(int2ki_world(X5)) & ~\$less(X5,0)) => ? [X6 : person] : (! [X7 : person] : (like(X7) => X6 = X7) & like(X6))))), inference(fool_elimination,[],[f24])). tff(f24,plain,( ~(('\$in_ki_world'('\$local_ki_world') => (! [X0 : person] : '\$possible'(like(X0)) & like(geoff) & ! [X1 : \$int] : (~\$less(X1,0) => (! [X2 : person,X3 : person] : (id_of(X2) = id_of(X3) => X2 = X3) & ? [X4 : person] : id_of(X4) = X1)))) & ! [X5 : \$int] : (('\$in_ki_world'(int2ki_world(X5)) & ~\$less(X5,0)) => ? [X6 : person] : (! [X7 : person] : (like(X7) => X6 = X7) & like(X6))))), inference(rectify,[],[f6])). tff(f6,plain,( ~(('\$in_ki_world'('\$local_ki_world') => (! [X14 : person] : '\$possible'(like(X14)) & like(geoff) & ! [X3 : \$int] : (~\$less(X3,0) => (! [X12 : person,X13 : person] : (id_of(X12) = id_of(X13) => X12 = X13) & ? [X10 : person] : id_of(X10) = X3)))) & ! [X9 : \$int] : (('\$in_ki_world'(int2ki_world(X9)) & ~\$less(X9,0)) => ? [X10 : person] : (! [X11 : person] : (like(X11) => X10 = X11) & like(X10))))), inference(theory_normalization,[],[f5])). tff(f5,negated_conjecture,( ~(('\$in_ki_world'('\$local_ki_world') => (! [X14 : person] : '\$possible'(like(X14)) & like(geoff) & ! [X3 : \$int] : (\$greatereq(X3,0) => (! [X12 : person,X13 : person] : (id_of(X12) = id_of(X13) => X12 = X13) & ? [X10 : person] : id_of(X10) = X3)))) & ! [X9 : \$int] : (('\$in_ki_world'(int2ki_world(X9)) & \$greatereq(X9,0)) => ? [X10 : person] : (! [X11 : person] : (like(X11) => X10 = X11) & like(X10))))), inference(negated_conjecture,[],[f4])). tff(f4,conjecture,( ('\$in_ki_world'('\$local_ki_world') => (! [X14 : person] : '\$possible'(like(X14)) & like(geoff) & ! [X3 : \$int] : (\$greatereq(X3,0) => (! [X12 : person,X13 : person] : (id_of(X12) = id_of(X13) => X12 = X13) & ? [X10 : person] : id_of(X10) = X3)))) & ! [X9 : \$int] : (('\$in_ki_world'(int2ki_world(X9)) & \$greatereq(X9,0)) => ? [X10 : person] : (! [X11 : person] : (like(X11) => X10 = X11) & like(X10)))), file('NTF_Infinite-Finite.s.p',prove_formulae)). tff(f4126,plain,( spl13_11 | spl13_74 | ~spl13_16 | ~spl13_70 | ~spl13_83), inference(avatar_split_clause,[],[f4125,f3697,f3479,f203,f3522,f169])). tff(f169,plain,( spl13_11 <=> ! [X6 : person] : (like(sK6(X6)) | ~like(X6))), introduced(avatar_definition,[new_symbols(naming,[spl13_11])])). tff(f4125,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(X4) != sK2 | like(sK6(X6)) | ~like(X6)) ) | ~spl13_83), inference(trivial_inequality_removal,[],[f4124])). tff(f4124,plain,( ( ! [X6 : person,X4 : person] : (sK3 != sK3 | ~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(X4) != sK2 | like(sK6(X6)) | ~like(X6)) ) | ~spl13_83), inference(forward_demodulation,[],[f76,f3699])). tff(f76,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | sK3 != sK4 | id_of(X4) != sK2 | like(sK6(X6)) | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f4121,plain,( spl13_83 | ~spl13_26 | ~spl13_67 | ~spl13_75), inference(avatar_split_clause,[],[f3695,f3525,f3455,f381,f3697])). tff(f381,plain,( spl13_26 <=> ! [X4 : person] : int2person(sK7(X4)) = X4), introduced(avatar_definition,[new_symbols(naming,[spl13_26])])). tff(f3455,plain,( spl13_67 <=> ! [X6 : \$int] : id_of(int2person(X6)) = X6), introduced(avatar_definition,[new_symbols(naming,[spl13_67])])). tff(f3525,plain,( spl13_75 <=> id_of(sK3) = id_of(sK4)), introduced(avatar_definition,[new_symbols(naming,[spl13_75])])). tff(f3695,plain,( sK3 = sK4 | (~spl13_26 | ~spl13_67 | ~spl13_75)), inference(forward_demodulation,[],[f3694,f3561])). tff(f3561,plain,( ( ! [X4 : person] : (int2person(id_of(X4)) = X4) ) | (~spl13_26 | ~spl13_67)), inference(backward_demodulation,[],[f382,f3459])). tff(f3459,plain,( ( ! [X0 : person] : (id_of(X0) = sK7(X0)) ) | (~spl13_26 | ~spl13_67)), inference(superposition,[],[f3456,f382])). tff(f3456,plain,( ( ! [X6 : \$int] : (id_of(int2person(X6)) = X6) ) | ~spl13_67), inference(avatar_component_clause,[],[f3455])). tff(f382,plain,( ( ! [X4 : person] : (int2person(sK7(X4)) = X4) ) | ~spl13_26), inference(avatar_component_clause,[],[f381])). tff(f3694,plain,( sK4 = int2person(id_of(sK3)) | (~spl13_26 | ~spl13_67 | ~spl13_75)), inference(superposition,[],[f3561,f3527])). tff(f3527,plain,( id_of(sK3) = id_of(sK4) | ~spl13_75), inference(avatar_component_clause,[],[f3525])). tff(f4117,plain,( spl13_15 | spl13_74 | spl13_75 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f73,f3479,f203,f3525,f3522,f197])). tff(f73,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(sK3) = id_of(sK4) | id_of(X4) != sK2 | sK6(X6) != X6 | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f4073,plain,( spl13_11 | spl13_74 | spl13_75 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f72,f3479,f203,f3525,f3522,f169])). tff(f72,plain,( ( ! [X6 : person,X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(sK3) = id_of(sK4) | id_of(X4) != sK2 | like(sK6(X6)) | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f4054,plain,( ~spl13_5 | spl13_74 | spl13_75 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f70,f3479,f203,f3525,f3522,f126])). tff(f126,plain,( spl13_5 <=> \$less(sK5,0)), introduced(avatar_definition,[new_symbols(naming,[spl13_5])])). tff(f70,plain,( ( ! [X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(sK3) = id_of(sK4) | id_of(X4) != sK2 | ~\$less(sK5,0)) )), inference(cnf_transformation,[],[f45])). tff(f4053,plain,( ~spl13_5 | spl13_74 | spl13_75 | ~spl13_16 | ~spl13_73 | ~spl13_72), inference(avatar_split_clause,[],[f4036,f3507,f3512,f203,f3525,f3522,f126])). tff(f3512,plain,( spl13_73 <=> '\$possible'(\$false)), introduced(avatar_definition,[new_symbols(naming,[spl13_73])])). tff(f3507,plain,( spl13_72 <=> (\$false = bG0(sK1))), introduced(avatar_definition,[new_symbols(naming,[spl13_72])])). tff(f4036,plain,( ( ! [X4 : person] : (~'\$possible'(\$false) | ~like(geoff) | id_of(sK3) = id_of(sK4) | id_of(X4) != sK2 | ~\$less(sK5,0)) ) | ~spl13_72), inference(forward_demodulation,[],[f70,f3509])). tff(f3509,plain,( (\$false = bG0(sK1)) | ~spl13_72), inference(avatar_component_clause,[],[f3507])). tff(f4033,plain,( ~spl13_8 | ~spl13_84), inference(avatar_contradiction_clause,[],[f4032])). tff(f4032,plain,( \$false | (~spl13_8 | ~spl13_84)), inference(evaluation,[],[f4025])). tff(f4025,plain,( 0 = 1 | \$less(1,0) | (~spl13_8 | ~spl13_84)), inference(resolution,[],[f3440,f3861])). tff(f3861,plain,( '\$in_ki_world'(int2ki_world(1)) | ~spl13_84), inference(avatar_component_clause,[],[f3859])). tff(f3859,plain,( spl13_84 <=> '\$in_ki_world'(int2ki_world(1))), introduced(avatar_definition,[new_symbols(naming,[spl13_84])])). tff(f3440,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | 0 = X0 | \$less(X0,0)) ) | ~spl13_8), inference(resolution,[],[f153,f94])). tff(f94,plain,( ( ! [X0 : \$int,X1 : \$int] : (~like(int2person(X1)) | X0 = X1 | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f51,plain,( ! [X0 : \$int] : ((! [X1 : \$int] : ((like(int2person(X1)) | X0 != X1) & (X0 = X1 | ~like(int2person(X1)))) & like(int2person(X0)) & id_of(int2person(X0)) = X0 & geoff = int2person(X0) & ! [X2 : \$int,X3 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2)) & ! [X4 : person] : int2person(sK7(X4)) = X4) | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) & ((like(int2person(0)) & ! [X6 : \$int] : id_of(int2person(X6)) = X6 & geoff = int2person(0) & ! [X7 : \$int,X8 : \$int] : (X7 = X8 | int2person(X8) != int2person(X7)) & ! [X9 : person] : int2person(sK8(X9)) = X9) | ~'\$in_ki_world'(int2ki_world(0))) & ! [X11 : \$int] : ('\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11)) | ~\$less(0,X11)) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X12 : '\$ki_world'] : int2ki_world(sK9(X12)) = X12 & ! [X14 : \$int,X15 : \$int] : (X14 = X15 | int2ki_world(X14) != int2ki_world(X15)) & '\$local_ki_world' = int2ki_world(0) & ! [X16 : \$int] : (int2ki_world(X16) = sK10(X16) | \$less(X16,0))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10])],[f46,f50,f49,f48,f47])). tff(f47,plain,( ! [X4 : person] : (? [X5 : \$int] : int2person(X5) = X4 => int2person(sK7(X4)) = X4)), introduced(choice_axiom,[])). tff(f48,plain,( ! [X9 : person] : (? [X10 : \$int] : int2person(X10) = X9 => int2person(sK8(X9)) = X9)), introduced(choice_axiom,[])). tff(f49,plain,( ! [X12 : '\$ki_world'] : (? [X13 : \$int] : int2ki_world(X13) = X12 => int2ki_world(sK9(X12)) = X12)), introduced(choice_axiom,[])). tff(f50,plain,( ! [X16 : \$int] : (? [X17 : '\$ki_world'] : int2ki_world(X16) = X17 => int2ki_world(X16) = sK10(X16))), introduced(choice_axiom,[])). tff(f46,plain,( ! [X0 : \$int] : ((! [X1 : \$int] : ((like(int2person(X1)) | X0 != X1) & (X0 = X1 | ~like(int2person(X1)))) & like(int2person(X0)) & id_of(int2person(X0)) = X0 & geoff = int2person(X0) & ! [X2 : \$int,X3 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2)) & ! [X4 : person] : ? [X5 : \$int] : int2person(X5) = X4) | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) & ((like(int2person(0)) & ! [X6 : \$int] : id_of(int2person(X6)) = X6 & geoff = int2person(0) & ! [X7 : \$int,X8 : \$int] : (X7 = X8 | int2person(X8) != int2person(X7)) & ! [X9 : person] : ? [X10 : \$int] : int2person(X10) = X9) | ~'\$in_ki_world'(int2ki_world(0))) & ! [X11 : \$int] : ('\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11)) | ~\$less(0,X11)) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X12 : '\$ki_world'] : ? [X13 : \$int] : int2ki_world(X13) = X12 & ! [X14 : \$int,X15 : \$int] : (X14 = X15 | int2ki_world(X14) != int2ki_world(X15)) & '\$local_ki_world' = int2ki_world(0) & ! [X16 : \$int] : (? [X17 : '\$ki_world'] : int2ki_world(X16) = X17 | \$less(X16,0))), inference(nnf_transformation,[],[f35])). tff(f35,plain,( ! [X0 : \$int] : ((! [X1 : \$int] : (like(int2person(X1)) <=> X0 = X1) & like(int2person(X0)) & id_of(int2person(X0)) = X0 & geoff = int2person(X0) & ! [X2 : \$int,X3 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2)) & ! [X4 : person] : ? [X5 : \$int] : int2person(X5) = X4) | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) & ((like(int2person(0)) & ! [X6 : \$int] : id_of(int2person(X6)) = X6 & geoff = int2person(0) & ! [X7 : \$int,X8 : \$int] : (X7 = X8 | int2person(X8) != int2person(X7)) & ! [X9 : person] : ? [X10 : \$int] : int2person(X10) = X9) | ~'\$in_ki_world'(int2ki_world(0))) & ! [X11 : \$int] : ('\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11)) | ~\$less(0,X11)) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X12 : '\$ki_world'] : ? [X13 : \$int] : int2ki_world(X13) = X12 & ! [X14 : \$int,X15 : \$int] : (X14 = X15 | int2ki_world(X14) != int2ki_world(X15)) & '\$local_ki_world' = int2ki_world(0) & ! [X16 : \$int] : (? [X17 : '\$ki_world'] : int2ki_world(X16) = X17 | \$less(X16,0))), inference(flattening,[],[f34])). tff(f34,plain,( ! [X0 : \$int] : ((! [X1 : \$int] : (like(int2person(X1)) <=> X0 = X1) & like(int2person(X0)) & id_of(int2person(X0)) = X0 & geoff = int2person(X0) & ! [X2 : \$int,X3 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2)) & ! [X4 : person] : ? [X5 : \$int] : int2person(X5) = X4) | (~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0))) & ((like(int2person(0)) & ! [X6 : \$int] : id_of(int2person(X6)) = X6 & geoff = int2person(0) & ! [X7 : \$int,X8 : \$int] : (X7 = X8 | int2person(X8) != int2person(X7)) & ! [X9 : person] : ? [X10 : \$int] : int2person(X10) = X9) | ~'\$in_ki_world'(int2ki_world(0))) & ! [X11 : \$int] : ('\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11)) | ~\$less(0,X11)) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X12 : '\$ki_world'] : ? [X13 : \$int] : int2ki_world(X13) = X12 & ! [X14 : \$int,X15 : \$int] : (X14 = X15 | int2ki_world(X14) != int2ki_world(X15)) & '\$local_ki_world' = int2ki_world(0) & ! [X16 : \$int] : (? [X17 : '\$ki_world'] : int2ki_world(X16) = X17 | \$less(X16,0))), inference(ennf_transformation,[],[f31])). tff(f31,plain,( ! [X0 : \$int] : (('\$in_ki_world'(int2ki_world(X0)) & ~\$less(X0,0)) => (! [X1 : \$int] : (like(int2person(X1)) <=> X0 = X1) & like(int2person(X0)) & id_of(int2person(X0)) = X0 & geoff = int2person(X0) & ! [X2 : \$int,X3 : \$int] : (int2person(X3) = int2person(X2) => X2 = X3) & ! [X4 : person] : ? [X5 : \$int] : int2person(X5) = X4)) & ('\$in_ki_world'(int2ki_world(0)) => (like(int2person(0)) & ! [X6 : \$int] : id_of(int2person(X6)) = X6 & geoff = int2person(0) & ! [X7 : \$int,X8 : \$int] : (int2person(X8) = int2person(X7) => X7 = X8) & ! [X9 : person] : ? [X10 : \$int] : int2person(X10) = X9)) & ! [X11 : \$int] : (\$less(0,X11) => '\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11))) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X12 : '\$ki_world'] : ? [X13 : \$int] : int2ki_world(X13) = X12 & ! [X14 : \$int,X15 : \$int] : (int2ki_world(X14) = int2ki_world(X15) => X14 = X15) & '\$local_ki_world' = int2ki_world(0) & ! [X16 : \$int] : (~\$less(X16,0) => ? [X17 : '\$ki_world'] : int2ki_world(X16) = X17)), inference(rectify,[],[f7])). tff(f7,plain,( ! [X9 : \$int] : (('\$in_ki_world'(int2ki_world(X9)) & ~\$less(X9,0)) => (! [X8 : \$int] : (like(int2person(X8)) <=> X8 = X9) & like(int2person(X9)) & id_of(int2person(X9)) = X9 & geoff = int2person(X9) & ! [X5 : \$int,X6 : \$int] : (int2person(X5) = int2person(X6) => X5 = X6) & ! [X10 : person] : ? [X8 : \$int] : int2person(X8) = X10)) & ('\$in_ki_world'(int2ki_world(0)) => (like(int2person(0)) & ! [X3 : \$int] : id_of(int2person(X3)) = X3 & geoff = int2person(0) & ! [X5 : \$int,X6 : \$int] : (int2person(X5) = int2person(X6) => X5 = X6) & ! [X7 : person] : ? [X8 : \$int] : int2person(X8) = X7)) & ! [X3 : \$int] : (\$less(0,X3) => '\$accessible_ki_world'(int2ki_world(0),int2ki_world(X3))) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X4 : '\$ki_world'] : ? [X3 : \$int] : int2ki_world(X3) = X4 & ! [X5 : \$int,X6 : \$int] : (int2ki_world(X5) = int2ki_world(X6) => X5 = X6) & '\$local_ki_world' = int2ki_world(0) & ! [X3 : \$int] : (~\$less(X3,0) => ? [X4 : '\$ki_world'] : int2ki_world(X3) = X4)), inference(theory_normalization,[],[f3])). tff(f3,axiom,( ! [X9 : \$int] : (('\$in_ki_world'(int2ki_world(X9)) & \$greatereq(X9,0)) => (! [X8 : \$int] : (like(int2person(X8)) <=> X8 = X9) & like(int2person(X9)) & id_of(int2person(X9)) = X9 & geoff = int2person(X9) & ! [X5 : \$int,X6 : \$int] : (int2person(X5) = int2person(X6) => X5 = X6) & ! [X10 : person] : ? [X8 : \$int] : int2person(X8) = X10)) & ('\$in_ki_world'(int2ki_world(0)) => (like(int2person(0)) & ! [X3 : \$int] : id_of(int2person(X3)) = X3 & geoff = int2person(0) & ! [X5 : \$int,X6 : \$int] : (int2person(X5) = int2person(X6) => X5 = X6) & ! [X7 : person] : ? [X8 : \$int] : int2person(X8) = X7)) & ! [X3 : \$int] : (\$greater(X3,0) => '\$accessible_ki_world'(int2ki_world(0),int2ki_world(X3))) & '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0)) & ! [X4 : '\$ki_world'] : ? [X3 : \$int] : int2ki_world(X3) = X4 & ! [X5 : \$int,X6 : \$int] : (int2ki_world(X5) = int2ki_world(X6) => X5 = X6) & '\$local_ki_world' = int2ki_world(0) & ! [X3 : \$int] : (\$greatereq(X3,0) => ? [X4 : '\$ki_world'] : int2ki_world(X3) = X4)), file('NTF_Infinite-Finite.s.p',like_geoff)). tff(f153,plain,( like(int2person(0)) | ~spl13_8), inference(avatar_component_clause,[],[f151])). tff(f151,plain,( spl13_8 <=> like(int2person(0))), introduced(avatar_definition,[new_symbols(naming,[spl13_8])])). tff(f4031,plain,( ~spl13_8 | ~spl13_87), inference(avatar_contradiction_clause,[],[f4030])). tff(f4030,plain,( \$false | (~spl13_8 | ~spl13_87)), inference(evaluation,[],[f4027])). tff(f4027,plain,( 0 = 2 | \$less(2,0) | (~spl13_8 | ~spl13_87)), inference(resolution,[],[f3440,f3987])). tff(f3987,plain,( '\$in_ki_world'(int2ki_world(2)) | ~spl13_87), inference(avatar_component_clause,[],[f3985])). tff(f3985,plain,( spl13_87 <=> '\$in_ki_world'(int2ki_world(2))), introduced(avatar_definition,[new_symbols(naming,[spl13_87])])). tff(f4014,plain,( spl13_72 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3487,f3479,f191,f3507])). tff(f191,plain,( spl13_14 <=> '\$possible'(\$true)), introduced(avatar_definition,[new_symbols(naming,[spl13_14])])). tff(f3487,plain,( (\$false = bG0(sK1)) | (~spl13_14 | spl13_70)), inference(resolution,[],[f3481,f195])). tff(f195,plain,( ( ! [X0 : \$o] : ('\$possible'(X0) | (\$false = X0)) ) | ~spl13_14), inference(superposition,[],[f193,f23])). tff(f23,plain,( ( ! [X0 : \$o] : ((\$true = X0) | (\$false = X0)) )), introduced(fool_axiom,[])). tff(f193,plain,( '\$possible'(\$true) | ~spl13_14), inference(avatar_component_clause,[],[f191])). tff(f3481,plain,( ~'\$possible'(bG0(sK1)) | spl13_70), inference(avatar_component_clause,[],[f3479])). tff(f4010,plain,( spl13_88 | ~spl13_87), inference(avatar_split_clause,[],[f4001,f3985,f4007])). tff(f4007,plain,( spl13_88 <=> like(int2person(2))), introduced(avatar_definition,[new_symbols(naming,[spl13_88])])). tff(f4001,plain,( like(int2person(2)) | ~spl13_87), inference(evaluation,[],[f3999])). tff(f3999,plain,( like(int2person(2)) | \$less(2,0) | ~spl13_87), inference(resolution,[],[f3987,f93])). tff(f93,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | like(int2person(X0)) | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f3994,plain,( spl13_87 | ~spl13_82), inference(avatar_split_clause,[],[f3959,f3633,f3985])). tff(f3633,plain,( spl13_82 <=> ! [X0 : \$int] : ('\$in_ki_world'(int2ki_world(X0)) | ~\$less(0,X0))), introduced(avatar_definition,[new_symbols(naming,[spl13_82])])). tff(f3959,plain,( '\$in_ki_world'(int2ki_world(2)) | ~spl13_82), inference(evaluation,[],[f3949])). tff(f3949,plain,( '\$in_ki_world'(int2ki_world(\$sum(2,0))) | ~spl13_82), inference(resolution,[],[f3634,f2139])). tff(f2139,plain,( ( ! [X9 : \$int] : (\$less(X9,\$sum(2,X9))) )), inference(evaluation,[],[f2128])). tff(f2128,plain,( ( ! [X9 : \$int] : (\$less(X9,\$sum(\$sum(X9,1),1))) )), inference(resolution,[],[f2072,f19])). tff(f19,plain,( ( ! [X0 : \$int,X1 : \$int] : (\$less(X1,\$sum(X0,1)) | \$less(X0,X1)) )), introduced(theory_axiom_151,[])). tff(f2072,plain,( ( ! [X6 : \$int] : (~\$less(\$sum(X6,1),X6)) )), inference(resolution,[],[f261,f15])). tff(f15,plain,( ( ! [X0 : \$int] : (~\$less(X0,X0)) )), introduced(theory_axiom_146,[])). tff(f261,plain,( ( ! [X2 : \$int,X1 : \$int] : (\$less(X1,\$sum(X2,1)) | ~\$less(X1,X2)) )), inference(resolution,[],[f212,f16])). tff(f16,plain,( ( ! [X2 : \$int,X0 : \$int,X1 : \$int] : (~\$less(X1,X2) | ~\$less(X0,X1) | \$less(X0,X2)) )), introduced(theory_axiom_147,[])). tff(f212,plain,( ( ! [X0 : \$int] : (\$less(X0,\$sum(X0,1))) )), inference(resolution,[],[f19,f15])). tff(f3634,plain,( ( ! [X0 : \$int] : (~\$less(0,X0) | '\$in_ki_world'(int2ki_world(X0))) ) | ~spl13_82), inference(avatar_component_clause,[],[f3633])). tff(f3993,plain,( spl13_87 | ~spl13_82), inference(avatar_split_clause,[],[f3829,f3633,f3985])). tff(f3829,plain,( '\$in_ki_world'(int2ki_world(2)) | ~spl13_82), inference(evaluation,[],[f3651])). tff(f3651,plain,( '\$in_ki_world'(int2ki_world(\$sum(2,0))) | ~spl13_82), inference(resolution,[],[f3634,f2139])). tff(f3992,plain,( spl13_87 | ~spl13_82), inference(avatar_split_clause,[],[f3729,f3633,f3985])). tff(f3729,plain,( '\$in_ki_world'(int2ki_world(2)) | ~spl13_82), inference(evaluation,[],[f3651])). tff(f3988,plain,( spl13_87 | ~spl13_82), inference(avatar_split_clause,[],[f3664,f3633,f3985])). tff(f3664,plain,( '\$in_ki_world'(int2ki_world(2)) | ~spl13_82), inference(evaluation,[],[f3651])). tff(f3978,plain,( ~spl13_58 | ~spl13_57), inference(avatar_split_clause,[],[f2277,f2183,f2319])). tff(f2319,plain,( spl13_58 <=> \$less(sK5,-1)), introduced(avatar_definition,[new_symbols(naming,[spl13_58])])). tff(f2183,plain,( spl13_57 <=> \$less(-1,\$sum(1,sK5))), introduced(avatar_definition,[new_symbols(naming,[spl13_57])])). tff(f2277,plain,( ~\$less(sK5,-1) | ~spl13_57), inference(resolution,[],[f2185,f216])). tff(f216,plain,( ( ! [X0 : \$int,X1 : \$int] : (~\$less(X1,\$sum(1,X0)) | ~\$less(X0,X1)) )), inference(superposition,[],[f21,f10])). tff(f10,plain,( ( ! [X0 : \$int,X1 : \$int] : (\$sum(X0,X1) = \$sum(X1,X0)) )), introduced(theory_axiom_139,[])). tff(f21,plain,( ( ! [X0 : \$int,X1 : \$int] : (~\$less(X1,\$sum(X0,1)) | ~\$less(X0,X1)) )), introduced(theory_axiom_165,[])). tff(f2185,plain,( \$less(-1,\$sum(1,sK5)) | ~spl13_57), inference(avatar_component_clause,[],[f2183])). tff(f3969,plain,( spl13_86 | ~spl13_79 | ~spl13_82), inference(avatar_split_clause,[],[f3941,f3633,f3574,f3966])). tff(f3966,plain,( spl13_86 <=> '\$in_ki_world'(int2ki_world(sK2))), introduced(avatar_definition,[new_symbols(naming,[spl13_86])])). tff(f3574,plain,( spl13_79 <=> \$less(0,sK2)), introduced(avatar_definition,[new_symbols(naming,[spl13_79])])). tff(f3941,plain,( '\$in_ki_world'(int2ki_world(sK2)) | (~spl13_79 | ~spl13_82)), inference(resolution,[],[f3634,f3576])). tff(f3576,plain,( \$less(0,sK2) | ~spl13_79), inference(avatar_component_clause,[],[f3574])). tff(f3930,plain,( spl13_72 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3842,f3479,f191,f3507])). tff(f3842,plain,( ~'\$possible'(\$true) | (\$false = bG0(sK1)) | spl13_70), inference(superposition,[],[f3481,f23])). tff(f3927,plain,( spl13_72 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3741,f3479,f191,f3507])). tff(f3741,plain,( ~'\$possible'(\$true) | (\$false = bG0(sK1)) | spl13_70), inference(superposition,[],[f3481,f23])). tff(f3898,plain,( spl13_85 | ~spl13_84), inference(avatar_split_clause,[],[f3868,f3859,f3895])). tff(f3895,plain,( spl13_85 <=> like(int2person(1))), introduced(avatar_definition,[new_symbols(naming,[spl13_85])])). tff(f3868,plain,( like(int2person(1)) | ~spl13_84), inference(evaluation,[],[f3866])). tff(f3866,plain,( like(int2person(1)) | \$less(1,0) | ~spl13_84), inference(resolution,[],[f3861,f93])). tff(f3893,plain,( spl13_72 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3488,f3479,f191,f3507])). tff(f3488,plain,( ~'\$possible'(\$true) | (\$false = bG0(sK1)) | spl13_70), inference(superposition,[],[f3481,f23])). tff(f3880,plain,( spl13_71 | spl13_69), inference(avatar_split_clause,[],[f3483,f3475,f3496])). tff(f3496,plain,( spl13_71 <=> \$less(-1,sK2)), introduced(avatar_definition,[new_symbols(naming,[spl13_71])])). tff(f3475,plain,( spl13_69 <=> \$less(sK2,0)), introduced(avatar_definition,[new_symbols(naming,[spl13_69])])). tff(f3483,plain,( \$less(-1,sK2) | spl13_69), inference(resolution,[],[f3477,f433])). tff(f433,plain,( ( ! [X10 : \$int] : (\$less(X10,0) | \$less(-1,X10)) )), inference(evaluation,[],[f432])). tff(f432,plain,( ( ! [X10 : \$int] : (\$less(X10,0) | \$less(\$uminus(1),X10)) )), inference(superposition,[],[f19,f142])). tff(f142,plain,( ( ! [X0 : \$int] : (0 = \$sum(\$uminus(X0),X0)) )), inference(superposition,[],[f14,f20])). tff(f20,plain,( ( ! [X0 : \$int] : (\$uminus(\$uminus(X0)) = X0) )), introduced(theory_axiom_152,[])). tff(f14,plain,( ( ! [X0 : \$int] : (0 = \$sum(X0,\$uminus(X0))) )), introduced(theory_axiom_144,[])). tff(f3477,plain,( ~\$less(sK2,0) | spl13_69), inference(avatar_component_clause,[],[f3475])). tff(f3864,plain,( spl13_84 | ~spl13_82), inference(avatar_split_clause,[],[f3830,f3633,f3859])). tff(f3830,plain,( '\$in_ki_world'(int2ki_world(1)) | ~spl13_82), inference(evaluation,[],[f3656])). tff(f3656,plain,( '\$in_ki_world'(int2ki_world(\$sum(0,1))) | ~spl13_82), inference(resolution,[],[f3634,f212])). tff(f3863,plain,( spl13_84 | ~spl13_82), inference(avatar_split_clause,[],[f3730,f3633,f3859])). tff(f3730,plain,( '\$in_ki_world'(int2ki_world(1)) | ~spl13_82), inference(evaluation,[],[f3656])). tff(f3862,plain,( spl13_84 | ~spl13_82), inference(avatar_split_clause,[],[f3663,f3633,f3859])). tff(f3663,plain,( '\$in_ki_world'(int2ki_world(1)) | ~spl13_82), inference(evaluation,[],[f3656])). tff(f3833,plain,( ~spl13_73 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3505,f3479,f191,f3512])). tff(f3505,plain,( ~'\$possible'(\$false) | (~spl13_14 | spl13_70)), inference(backward_demodulation,[],[f3481,f3487])). tff(f3814,plain,( spl13_9 | spl13_74 | ~spl13_83 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f75,f3479,f203,f3697,f3522,f156])). tff(f156,plain,( spl13_9 <=> '\$in_ki_world'(int2ki_world(sK5))), introduced(avatar_definition,[new_symbols(naming,[spl13_9])])). tff(f75,plain,( ( ! [X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | sK3 != sK4 | id_of(X4) != sK2 | '\$in_ki_world'(int2ki_world(sK5))) )), inference(cnf_transformation,[],[f45])). tff(f3783,plain,( ~spl13_5 | spl13_74 | ~spl13_83 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f74,f3479,f203,f3697,f3522,f126])). tff(f74,plain,( ( ! [X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | sK3 != sK4 | id_of(X4) != sK2 | ~\$less(sK5,0)) )), inference(cnf_transformation,[],[f45])). tff(f3782,plain,( spl13_83 | ~spl13_26 | ~spl13_67 | ~spl13_75), inference(avatar_split_clause,[],[f3695,f3525,f3455,f381,f3697])). tff(f3754,plain,( ~spl13_6 | ~spl13_7 | ~spl13_13), inference(avatar_split_clause,[],[f3748,f188,f138,f130])). tff(f130,plain,( spl13_6 <=> '\$in_ki_world'('\$local_ki_world')), introduced(avatar_definition,[new_symbols(naming,[spl13_6])])). tff(f138,plain,( spl13_7 <=> '\$accessible_ki_world'('\$local_ki_world','\$local_ki_world')), introduced(avatar_definition,[new_symbols(naming,[spl13_7])])). tff(f188,plain,( spl13_13 <=> ! [X2 : '\$ki_world',X0 : '\$ki_world'] : (~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0))), introduced(avatar_definition,[new_symbols(naming,[spl13_13])])). tff(f3748,plain,( ~'\$in_ki_world'('\$local_ki_world') | (~spl13_7 | ~spl13_13)), inference(resolution,[],[f189,f140])). tff(f140,plain,( '\$accessible_ki_world'('\$local_ki_world','\$local_ki_world') | ~spl13_7), inference(avatar_component_clause,[],[f138])). tff(f189,plain,( ( ! [X2 : '\$ki_world',X0 : '\$ki_world'] : (~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0)) ) | ~spl13_13), inference(avatar_component_clause,[],[f188])). tff(f3723,plain,( spl13_14 | ~spl13_21), inference(avatar_contradiction_clause,[],[f3715])). tff(f3715,plain,( \$false | (spl13_14 | ~spl13_21)), inference(resolution,[],[f192,f282])). tff(f282,plain,( ( ! [X1 : \$o] : ('\$possible'(X1)) ) | ~spl13_21), inference(avatar_component_clause,[],[f281])). tff(f281,plain,( spl13_21 <=> ! [X1 : \$o] : '\$possible'(X1)), introduced(avatar_definition,[new_symbols(naming,[spl13_21])])). tff(f192,plain,( ~'\$possible'(\$true) | spl13_14), inference(avatar_component_clause,[],[f191])). tff(f3714,plain,( ~spl13_67 | ~spl13_74), inference(avatar_contradiction_clause,[],[f3713])). tff(f3713,plain,( \$false | (~spl13_67 | ~spl13_74)), inference(equality_resolution,[],[f3680])). tff(f3680,plain,( ( ! [X0 : \$int] : (sK2 != X0) ) | (~spl13_67 | ~spl13_74)), inference(superposition,[],[f3523,f3456])). tff(f3523,plain,( ( ! [X4 : person] : (id_of(X4) != sK2) ) | ~spl13_74), inference(avatar_component_clause,[],[f3522])). tff(f3700,plain,( spl13_83 | ~spl13_26 | ~spl13_67 | ~spl13_75), inference(avatar_split_clause,[],[f3695,f3525,f3455,f381,f3697])). tff(f3692,plain,( ~spl13_68 | ~spl13_74 | ~spl13_78), inference(avatar_contradiction_clause,[],[f3691])). tff(f3691,plain,( \$false | (~spl13_68 | ~spl13_74 | ~spl13_78)), inference(trivial_inequality_removal,[],[f3690])). tff(f3690,plain,( 0 != 0 | (~spl13_68 | ~spl13_74 | ~spl13_78)), inference(superposition,[],[f3683,f3472])). tff(f3472,plain,( 0 = id_of(geoff) | ~spl13_68), inference(avatar_component_clause,[],[f3470])). tff(f3470,plain,( spl13_68 <=> 0 = id_of(geoff)), introduced(avatar_definition,[new_symbols(naming,[spl13_68])])). tff(f3683,plain,( ( ! [X4 : person] : (0 != id_of(X4)) ) | (~spl13_74 | ~spl13_78)), inference(backward_demodulation,[],[f3523,f3572])). tff(f3572,plain,( 0 = sK2 | ~spl13_78), inference(avatar_component_clause,[],[f3570])). tff(f3570,plain,( spl13_78 <=> 0 = sK2), introduced(avatar_definition,[new_symbols(naming,[spl13_78])])). tff(f3672,plain,( ~spl13_21 | spl13_73), inference(avatar_contradiction_clause,[],[f3671])). tff(f3671,plain,( \$false | (~spl13_21 | spl13_73)), inference(resolution,[],[f282,f3514])). tff(f3514,plain,( ~'\$possible'(\$false) | spl13_73), inference(avatar_component_clause,[],[f3512])). tff(f3670,plain,( spl13_9 | ~spl13_24 | ~spl13_82), inference(avatar_split_clause,[],[f3643,f3633,f348,f156])). tff(f348,plain,( spl13_24 <=> \$less(0,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_24])])). tff(f3643,plain,( '\$in_ki_world'(int2ki_world(sK5)) | (~spl13_24 | ~spl13_82)), inference(resolution,[],[f3634,f350])). tff(f350,plain,( \$less(0,sK5) | ~spl13_24), inference(avatar_component_clause,[],[f348])). tff(f3635,plain,( spl13_82 | ~spl13_6 | ~spl13_2 | ~spl13_20), inference(avatar_split_clause,[],[f288,f278,f113,f130,f3633])). tff(f113,plain,( spl13_2 <=> '\$local_ki_world' = int2ki_world(0)), introduced(avatar_definition,[new_symbols(naming,[spl13_2])])). tff(f278,plain,( spl13_20 <=> ! [X2 : '\$ki_world',X0 : '\$ki_world'] : ('\$in_ki_world'(X2) | ~'\$in_ki_world'(X0) | ~'\$accessible_ki_world'(X0,X2))), introduced(avatar_definition,[new_symbols(naming,[spl13_20])])). tff(f288,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'('\$local_ki_world') | '\$in_ki_world'(int2ki_world(X0)) | ~\$less(0,X0)) ) | (~spl13_2 | ~spl13_20)), inference(resolution,[],[f279,f239])). tff(f239,plain,( ( ! [X11 : \$int] : ('\$accessible_ki_world'('\$local_ki_world',int2ki_world(X11)) | ~\$less(0,X11)) ) | ~spl13_2), inference(forward_demodulation,[],[f83,f115])). tff(f115,plain,( '\$local_ki_world' = int2ki_world(0) | ~spl13_2), inference(avatar_component_clause,[],[f113])). tff(f83,plain,( ( ! [X11 : \$int] : ('\$accessible_ki_world'(int2ki_world(0),int2ki_world(X11)) | ~\$less(0,X11)) )), inference(cnf_transformation,[],[f51])). tff(f279,plain,( ( ! [X2 : '\$ki_world',X0 : '\$ki_world'] : (~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0) | '\$in_ki_world'(X2)) ) | ~spl13_20), inference(avatar_component_clause,[],[f278])). tff(f3620,plain,( spl13_81 | ~spl13_69), inference(avatar_split_clause,[],[f3606,f3475,f3616])). tff(f3616,plain,( spl13_81 <=> \$less(sK2,1)), introduced(avatar_definition,[new_symbols(naming,[spl13_81])])). tff(f3606,plain,( \$less(sK2,1) | ~spl13_69), inference(evaluation,[],[f3594])). tff(f3594,plain,( \$less(0,0) | \$less(sK2,1) | ~spl13_69), inference(resolution,[],[f3582,f224])). tff(f224,plain,( ( ! [X3 : \$int] : (\$less(X3,1) | \$less(0,X3)) )), inference(superposition,[],[f19,f174])). tff(f174,plain,( ( ! [X0 : \$int] : (\$sum(0,X0) = X0) )), inference(superposition,[],[f10,f12])). tff(f12,plain,( ( ! [X0 : \$int] : (\$sum(X0,0) = X0) )), introduced(theory_axiom_141,[])). tff(f3582,plain,( ( ! [X2 : \$int] : (~\$less(X2,sK2) | \$less(X2,0)) ) | ~spl13_69), inference(resolution,[],[f3476,f16])). tff(f3476,plain,( \$less(sK2,0) | ~spl13_69), inference(avatar_component_clause,[],[f3475])). tff(f3619,plain,( spl13_81 | spl13_79), inference(avatar_split_clause,[],[f3584,f3574,f3616])). tff(f3584,plain,( \$less(sK2,1) | spl13_79), inference(resolution,[],[f3575,f224])). tff(f3575,plain,( ~\$less(0,sK2) | spl13_79), inference(avatar_component_clause,[],[f3574])). tff(f3614,plain,( spl13_80 | ~spl13_24 | ~spl13_69), inference(avatar_split_clause,[],[f3578,f3475,f348,f3611])). tff(f3611,plain,( spl13_80 <=> \$less(sK2,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_80])])). tff(f3578,plain,( \$less(sK2,sK5) | (~spl13_24 | ~spl13_69)), inference(resolution,[],[f3476,f375])). tff(f375,plain,( ( ! [X0 : \$int] : (~\$less(X0,0) | \$less(X0,sK5)) ) | ~spl13_24), inference(resolution,[],[f350,f16])). tff(f3577,plain,( spl13_78 | spl13_79 | spl13_69), inference(avatar_split_clause,[],[f3485,f3475,f3574,f3570])). tff(f3485,plain,( \$less(0,sK2) | 0 = sK2 | spl13_69), inference(resolution,[],[f3477,f17])). tff(f17,plain,( ( ! [X0 : \$int,X1 : \$int] : (\$less(X1,X0) | \$less(X0,X1) | X0 = X1) )), introduced(theory_axiom_148,[])). tff(f3559,plain,( spl13_77 | spl13_69), inference(avatar_split_clause,[],[f3484,f3475,f3556])). tff(f3556,plain,( spl13_77 <=> int2ki_world(sK2) = sK10(sK2)), introduced(avatar_definition,[new_symbols(naming,[spl13_77])])). tff(f3484,plain,( int2ki_world(sK2) = sK10(sK2) | spl13_69), inference(resolution,[],[f3477,f78])). tff(f78,plain,( ( ! [X16 : \$int] : (\$less(X16,0) | int2ki_world(X16) = sK10(X16)) )), inference(cnf_transformation,[],[f51])). tff(f3547,plain,( ~spl13_76 | spl13_60), inference(avatar_split_clause,[],[f3178,f2669,f3544])). tff(f3544,plain,( spl13_76 <=> \$less(1,\$uminus(sK5))), introduced(avatar_definition,[new_symbols(naming,[spl13_76])])). tff(f2669,plain,( spl13_60 <=> \$less(\$sum(1,sK5),0)), introduced(avatar_definition,[new_symbols(naming,[spl13_60])])). tff(f3178,plain,( ~\$less(1,\$uminus(sK5)) | spl13_60), inference(resolution,[],[f425,f2671])). tff(f2671,plain,( ~\$less(\$sum(1,sK5),0) | spl13_60), inference(avatar_component_clause,[],[f2669])). tff(f425,plain,( ( ! [X3 : \$int,X4 : \$int] : (\$less(\$sum(X4,X3),0) | ~\$less(X4,\$uminus(X3))) )), inference(superposition,[],[f18,f142])). tff(f18,plain,( ( ! [X2 : \$int,X0 : \$int,X1 : \$int] : (\$less(\$sum(X0,X2),\$sum(X1,X2)) | ~\$less(X0,X1)) )), introduced(theory_axiom_149,[])). tff(f3528,plain,( spl13_9 | spl13_74 | spl13_75 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f71,f3479,f203,f3525,f3522,f156])). tff(f71,plain,( ( ! [X4 : person] : (~'\$possible'(bG0(sK1)) | ~like(geoff) | id_of(sK3) = id_of(sK4) | id_of(X4) != sK2 | '\$in_ki_world'(int2ki_world(sK5))) )), inference(cnf_transformation,[],[f45])). tff(f3515,plain,( ~spl13_73 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3505,f3479,f191,f3512])). tff(f3510,plain,( spl13_72 | ~spl13_14 | spl13_70), inference(avatar_split_clause,[],[f3487,f3479,f191,f3507])). tff(f3499,plain,( spl13_71 | spl13_69), inference(avatar_split_clause,[],[f3483,f3475,f3496])). tff(f3482,plain,( spl13_9 | ~spl13_69 | ~spl13_16 | ~spl13_70), inference(avatar_split_clause,[],[f67,f3479,f203,f3475,f156])). tff(f67,plain,( ~'\$possible'(bG0(sK1)) | ~like(geoff) | ~\$less(sK2,0) | '\$in_ki_world'(int2ki_world(sK5))), inference(cnf_transformation,[],[f45])). tff(f3473,plain,( spl13_68 | ~spl13_12 | ~spl13_67), inference(avatar_split_clause,[],[f3458,f3455,f182,f3470])). tff(f182,plain,( spl13_12 <=> geoff = int2person(0)), introduced(avatar_definition,[new_symbols(naming,[spl13_12])])). tff(f3458,plain,( 0 = id_of(geoff) | (~spl13_12 | ~spl13_67)), inference(superposition,[],[f3456,f184])). tff(f184,plain,( geoff = int2person(0) | ~spl13_12), inference(avatar_component_clause,[],[f182])). tff(f3457,plain,( spl13_67 | ~spl13_6 | ~spl13_2), inference(avatar_split_clause,[],[f248,f113,f130,f3455])). tff(f248,plain,( ( ! [X6 : \$int] : (~'\$in_ki_world'('\$local_ki_world') | id_of(int2person(X6)) = X6) ) | ~spl13_2), inference(forward_demodulation,[],[f87,f115])). tff(f87,plain,( ( ! [X6 : \$int] : (id_of(int2person(X6)) = X6 | ~'\$in_ki_world'(int2ki_world(0))) )), inference(cnf_transformation,[],[f51])). tff(f3450,plain,( spl13_66 | ~spl13_6 | ~spl13_2), inference(avatar_split_clause,[],[f247,f113,f130,f3448])). tff(f3448,plain,( spl13_66 <=> ! [X9 : person] : int2person(sK8(X9)) = X9), introduced(avatar_definition,[new_symbols(naming,[spl13_66])])). tff(f247,plain,( ( ! [X9 : person] : (~'\$in_ki_world'('\$local_ki_world') | int2person(sK8(X9)) = X9) ) | ~spl13_2), inference(forward_demodulation,[],[f84,f115])). tff(f84,plain,( ( ! [X9 : person] : (int2person(sK8(X9)) = X9 | ~'\$in_ki_world'(int2ki_world(0))) )), inference(cnf_transformation,[],[f51])). tff(f3438,plain,( ~spl13_6 | ~spl13_2 | ~spl13_25), inference(avatar_split_clause,[],[f387,f378,f113,f130])). tff(f378,plain,( spl13_25 <=> ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0))), introduced(avatar_definition,[new_symbols(naming,[spl13_25])])). tff(f387,plain,( ~'\$in_ki_world'('\$local_ki_world') | (~spl13_2 | ~spl13_25)), inference(evaluation,[],[f385])). tff(f385,plain,( ~'\$in_ki_world'('\$local_ki_world') | \$less(0,0) | (~spl13_2 | ~spl13_25)), inference(superposition,[],[f379,f115])). tff(f379,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) ) | ~spl13_25), inference(avatar_component_clause,[],[f378])). tff(f3427,plain,( ~spl13_16 | ~spl13_15 | ~spl13_65), inference(avatar_split_clause,[],[f3391,f3227,f197,f203])). tff(f3227,plain,( spl13_65 <=> geoff = sK6(geoff)), introduced(avatar_definition,[new_symbols(naming,[spl13_65])])). tff(f3391,plain,( ~like(geoff) | (~spl13_15 | ~spl13_65)), inference(trivial_inequality_removal,[],[f3389])). tff(f3389,plain,( geoff != geoff | ~like(geoff) | (~spl13_15 | ~spl13_65)), inference(superposition,[],[f198,f3229])). tff(f3229,plain,( geoff = sK6(geoff) | ~spl13_65), inference(avatar_component_clause,[],[f3227])). tff(f198,plain,( ( ! [X6 : person] : (sK6(X6) != X6 | ~like(X6)) ) | ~spl13_15), inference(avatar_component_clause,[],[f197])). tff(f3278,plain,( spl13_37 | ~spl13_26 | ~spl13_35 | ~spl13_46 | ~spl13_64), inference(avatar_split_clause,[],[f3222,f3081,f964,f521,f381,f549])). tff(f549,plain,( spl13_37 <=> like(sK6(geoff))), introduced(avatar_definition,[new_symbols(naming,[spl13_37])])). tff(f521,plain,( spl13_35 <=> geoff = int2person(sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_35])])). tff(f964,plain,( spl13_46 <=> like(sK6(sK6(geoff)))), introduced(avatar_definition,[new_symbols(naming,[spl13_46])])). tff(f3081,plain,( spl13_64 <=> sK5 = sK7(sK6(geoff))), introduced(avatar_definition,[new_symbols(naming,[spl13_64])])). tff(f3222,plain,( like(sK6(geoff)) | (~spl13_26 | ~spl13_35 | ~spl13_46 | ~spl13_64)), inference(backward_demodulation,[],[f966,f3177])). tff(f3177,plain,( geoff = sK6(geoff) | (~spl13_26 | ~spl13_35 | ~spl13_64)), inference(forward_demodulation,[],[f3176,f523])). tff(f523,plain,( geoff = int2person(sK5) | ~spl13_35), inference(avatar_component_clause,[],[f521])). tff(f3176,plain,( sK6(geoff) = int2person(sK5) | (~spl13_26 | ~spl13_64)), inference(superposition,[],[f382,f3083])). tff(f3083,plain,( sK5 = sK7(sK6(geoff)) | ~spl13_64), inference(avatar_component_clause,[],[f3081])). tff(f966,plain,( like(sK6(sK6(geoff))) | ~spl13_46), inference(avatar_component_clause,[],[f964])). tff(f3230,plain,( spl13_65 | ~spl13_26 | ~spl13_35 | ~spl13_64), inference(avatar_split_clause,[],[f3177,f3081,f521,f381,f3227])). tff(f3084,plain,( spl13_64 | ~spl13_37 | ~spl13_63), inference(avatar_split_clause,[],[f3077,f3023,f549,f3081])). tff(f3023,plain,( spl13_63 <=> ! [X0 : person] : (sK5 = sK7(X0) | ~like(X0))), introduced(avatar_definition,[new_symbols(naming,[spl13_63])])). tff(f3077,plain,( sK5 = sK7(sK6(geoff)) | (~spl13_37 | ~spl13_63)), inference(resolution,[],[f3024,f551])). tff(f551,plain,( like(sK6(geoff)) | ~spl13_37), inference(avatar_component_clause,[],[f549])). tff(f3024,plain,( ( ! [X0 : person] : (~like(X0) | sK5 = sK7(X0)) ) | ~spl13_63), inference(avatar_component_clause,[],[f3023])). tff(f3025,plain,( spl13_5 | spl13_63 | ~spl13_9 | ~spl13_26), inference(avatar_split_clause,[],[f1461,f381,f156,f3023,f126])). tff(f1461,plain,( ( ! [X0 : person] : (sK5 = sK7(X0) | ~like(X0) | \$less(sK5,0)) ) | (~spl13_9 | ~spl13_26)), inference(resolution,[],[f406,f158])). tff(f158,plain,( '\$in_ki_world'(int2ki_world(sK5)) | ~spl13_9), inference(avatar_component_clause,[],[f156])). tff(f406,plain,( ( ! [X0 : person,X1 : \$int] : (~'\$in_ki_world'(int2ki_world(X1)) | sK7(X0) = X1 | ~like(X0) | \$less(X1,0)) ) | ~spl13_26), inference(superposition,[],[f94,f382])). tff(f3008,plain,( spl13_62 | ~spl13_55), inference(avatar_split_clause,[],[f2984,f1996,f3005])). tff(f3005,plain,( spl13_62 <=> \$less(-12,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_62])])). tff(f1996,plain,( spl13_55 <=> \$less(-10,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_55])])). tff(f2984,plain,( \$less(-12,sK5) | ~spl13_55), inference(evaluation,[],[f2977])). tff(f2977,plain,( \$less(\$sum(-10,-2),sK5) | ~spl13_55), inference(resolution,[],[f2491,f2020])). tff(f2020,plain,( ( ! [X2 : \$int] : (~\$less(X2,-10) | \$less(X2,sK5)) ) | ~spl13_55), inference(resolution,[],[f1998,f16])). tff(f1998,plain,( \$less(-10,sK5) | ~spl13_55), inference(avatar_component_clause,[],[f1996])). tff(f2491,plain,( ( ! [X4 : \$int] : (\$less(\$sum(X4,-2),X4)) )), inference(evaluation,[],[f2487])). tff(f2487,plain,( ( ! [X4 : \$int] : (\$less(\$sum(X4,\$uminus(2)),X4)) )), inference(superposition,[],[f2139,f611])). tff(f611,plain,( ( ! [X3 : \$int,X4 : \$int] : (\$sum(X3,\$sum(X4,\$uminus(X3))) = X4) )), inference(superposition,[],[f372,f10])). tff(f372,plain,( ( ! [X2 : \$int,X3 : \$int] : (\$sum(X2,\$sum(\$uminus(X2),X3)) = X3) )), inference(forward_demodulation,[],[f353,f174])). tff(f353,plain,( ( ! [X2 : \$int,X3 : \$int] : (\$sum(X2,\$sum(\$uminus(X2),X3)) = \$sum(0,X3)) )), inference(superposition,[],[f11,f14])). tff(f11,plain,( ( ! [X2 : \$int,X0 : \$int,X1 : \$int] : (\$sum(X0,\$sum(X1,X2)) = \$sum(\$sum(X0,X1),X2)) )), introduced(theory_axiom_140,[])). tff(f2677,plain,( spl13_61 | ~spl13_24), inference(avatar_split_clause,[],[f2551,f348,f2674])). tff(f2674,plain,( spl13_61 <=> \$less(-1,\$sum(2,sK5))), introduced(avatar_definition,[new_symbols(naming,[spl13_61])])). tff(f2551,plain,( \$less(-1,\$sum(2,sK5)) | ~spl13_24), inference(resolution,[],[f2140,f473])). tff(f473,plain,( ( ! [X0 : \$int] : (\$less(-1,X0) | \$less(X0,sK5)) ) | ~spl13_24), inference(resolution,[],[f433,f375])). tff(f2140,plain,( ( ! [X8 : \$int] : (~\$less(\$sum(2,X8),X8)) )), inference(evaluation,[],[f2127])). tff(f2127,plain,( ( ! [X8 : \$int] : (~\$less(\$sum(\$sum(X8,1),1),X8)) )), inference(resolution,[],[f2072,f261])). tff(f2672,plain,( ~spl13_60 | ~spl13_57), inference(avatar_split_clause,[],[f2276,f2183,f2669])). tff(f2276,plain,( ~\$less(\$sum(1,sK5),0) | ~spl13_57), inference(resolution,[],[f2185,f434])). tff(f434,plain,( ( ! [X9 : \$int] : (~\$less(-1,X9) | ~\$less(X9,0)) )), inference(evaluation,[],[f431])). tff(f431,plain,( ( ! [X9 : \$int] : (~\$less(X9,0) | ~\$less(\$uminus(1),X9)) )), inference(superposition,[],[f21,f142])). tff(f2620,plain,( spl13_59), inference(avatar_split_clause,[],[f2142,f2617])). tff(f2617,plain,( spl13_59 <=> int2ki_world(1) = sK10(1)), introduced(avatar_definition,[new_symbols(naming,[spl13_59])])). tff(f2142,plain,( int2ki_world(1) = sK10(1)), inference(evaluation,[],[f2124])). tff(f2124,plain,( int2ki_world(\$sum(0,1)) = sK10(\$sum(0,1))), inference(resolution,[],[f2072,f78])). tff(f2322,plain,( ~spl13_58 | ~spl13_57), inference(avatar_split_clause,[],[f2277,f2183,f2319])). tff(f2186,plain,( spl13_57 | ~spl13_24), inference(avatar_split_clause,[],[f2144,f348,f2183])). tff(f2144,plain,( \$less(-1,\$sum(1,sK5)) | ~spl13_24), inference(forward_demodulation,[],[f2131,f10])). tff(f2131,plain,( \$less(-1,\$sum(sK5,1)) | ~spl13_24), inference(resolution,[],[f2072,f473])). tff(f2068,plain,( spl13_56 | ~spl13_55), inference(avatar_split_clause,[],[f2040,f1996,f2048])). tff(f2048,plain,( spl13_56 <=> \$less(-11,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_56])])). tff(f2040,plain,( \$less(-11,sK5) | ~spl13_55), inference(evaluation,[],[f2034])). tff(f2034,plain,( \$less(\$sum(-1,-10),sK5) | ~spl13_55), inference(resolution,[],[f2020,f626])). tff(f626,plain,( ( ! [X18 : \$int] : (\$less(\$sum(-1,X18),X18)) )), inference(evaluation,[],[f624])). tff(f624,plain,( ( ! [X18 : \$int] : (\$less(\$sum(\$uminus(1),X18),X18)) )), inference(superposition,[],[f262,f372])). tff(f262,plain,( ( ! [X0 : \$int] : (\$less(X0,\$sum(1,X0))) )), inference(superposition,[],[f212,f10])). tff(f2051,plain,( spl13_56 | ~spl13_55), inference(avatar_split_clause,[],[f2039,f1996,f2048])). tff(f2039,plain,( \$less(-11,sK5) | ~spl13_55), inference(evaluation,[],[f2035])). tff(f2035,plain,( \$less(\$sum(-10,-1),sK5) | ~spl13_55), inference(resolution,[],[f2020,f637])). tff(f637,plain,( ( ! [X0 : \$int] : (\$less(\$sum(X0,-1),X0)) )), inference(superposition,[],[f626,f10])). tff(f2007,plain,( spl13_55 | ~spl13_53), inference(avatar_split_clause,[],[f1984,f1964,f1996])). tff(f1964,plain,( spl13_53 <=> \$less(-9,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_53])])). tff(f1984,plain,( \$less(-10,sK5) | ~spl13_53), inference(evaluation,[],[f1978])). tff(f1978,plain,( \$less(\$sum(-1,-9),sK5) | ~spl13_53), inference(resolution,[],[f1973,f626])). tff(f1973,plain,( ( ! [X2 : \$int] : (~\$less(X2,-9) | \$less(X2,sK5)) ) | ~spl13_53), inference(resolution,[],[f1966,f16])). tff(f1966,plain,( \$less(-9,sK5) | ~spl13_53), inference(avatar_component_clause,[],[f1964])). tff(f1999,plain,( spl13_55 | ~spl13_53), inference(avatar_split_clause,[],[f1983,f1964,f1996])). tff(f1983,plain,( \$less(-10,sK5) | ~spl13_53), inference(evaluation,[],[f1979])). tff(f1979,plain,( \$less(\$sum(-9,-1),sK5) | ~spl13_53), inference(resolution,[],[f1973,f637])). tff(f1992,plain,( ~spl13_3 | ~spl13_9), inference(avatar_contradiction_clause,[],[f1989])). tff(f1989,plain,( \$false | (~spl13_3 | ~spl13_9)), inference(resolution,[],[f119,f158])). tff(f119,plain,( ( ! [X0 : '\$ki_world'] : (~'\$in_ki_world'(X0)) ) | ~spl13_3), inference(avatar_component_clause,[],[f118])). tff(f118,plain,( spl13_3 <=> ! [X0 : '\$ki_world'] : ~'\$in_ki_world'(X0)), introduced(avatar_definition,[new_symbols(naming,[spl13_3])])). tff(f1988,plain,( spl13_54 | spl13_3 | ~spl13_20), inference(avatar_split_clause,[],[f605,f278,f118,f1986])). tff(f1986,plain,( spl13_54 <=> ! [X1 : \$o] : (~'\$possible'(X1) | (\$true = X1))), introduced(avatar_definition,[new_symbols(naming,[spl13_54])])). tff(f605,plain,( ( ! [X0 : '\$ki_world',X1 : \$o] : (~'\$in_ki_world'(X0) | ~'\$possible'(X1) | (\$true = X1)) ) | ~spl13_20), inference(duplicate_literal_removal,[],[f604])). tff(f604,plain,( ( ! [X0 : '\$ki_world',X1 : \$o] : (~'\$in_ki_world'(X0) | ~'\$possible'(X1) | (\$true = X1) | ~'\$possible'(X1) | ~'\$in_ki_world'(X0)) ) | ~spl13_20), inference(resolution,[],[f291,f101])). tff(f101,plain,( ( ! [X0 : '\$ki_world',X1 : \$o] : (~'\$in_ki_world'(sK12(X0,X1)) | (\$true = X1) | ~'\$possible'(X1) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f59])). tff(f59,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$possible'(X1) | ! [X2 : '\$ki_world'] : (((\$true != X1) & '\$in_ki_world'(X2)) | ~'\$accessible_ki_world'(X0,X2))) & ((((\$true = X1) | ~'\$in_ki_world'(sK12(X0,X1))) & '\$accessible_ki_world'(X0,sK12(X0,X1))) | ~'\$possible'(X1))) | ~'\$in_ki_world'(X0))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK12])],[f57,f58])). tff(f58,plain,( ! [X0 : '\$ki_world',X1 : \$o] : (? [X3 : '\$ki_world'] : (((\$true = X1) | ~'\$in_ki_world'(X3)) & '\$accessible_ki_world'(X0,X3)) => (((\$true = X1) | ~'\$in_ki_world'(sK12(X0,X1))) & '\$accessible_ki_world'(X0,sK12(X0,X1))))), introduced(choice_axiom,[])). tff(f57,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$possible'(X1) | ! [X2 : '\$ki_world'] : (((\$true != X1) & '\$in_ki_world'(X2)) | ~'\$accessible_ki_world'(X0,X2))) & (? [X3 : '\$ki_world'] : (((\$true = X1) | ~'\$in_ki_world'(X3)) & '\$accessible_ki_world'(X0,X3)) | ~'\$possible'(X1))) | ~'\$in_ki_world'(X0))), inference(rectify,[],[f56])). tff(f56,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$possible'(X1) | ! [X2 : '\$ki_world'] : (((\$true != X1) & '\$in_ki_world'(X2)) | ~'\$accessible_ki_world'(X0,X2))) & (? [X2 : '\$ki_world'] : (((\$true = X1) | ~'\$in_ki_world'(X2)) & '\$accessible_ki_world'(X0,X2)) | ~'\$possible'(X1))) | ~'\$in_ki_world'(X0))), inference(nnf_transformation,[],[f38])). tff(f38,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : ('\$possible'(X1) <=> ? [X2 : '\$ki_world'] : (((\$true = X1) | ~'\$in_ki_world'(X2)) & '\$accessible_ki_world'(X0,X2))) | ~'\$in_ki_world'(X0))), inference(ennf_transformation,[],[f30])). tff(f30,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$possible'(X1) <=> ? [X2 : '\$ki_world'] : (('\$in_ki_world'(X2) => (\$true = X1)) & '\$accessible_ki_world'(X0,X2))))), inference(fool_elimination,[],[f29])). tff(f29,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$possible'(X1) <=> ? [X2 : '\$ki_world'] : (('\$in_ki_world'(X2) => X1) & '\$accessible_ki_world'(X0,X2))))), inference(rectify,[],[f9])). tff(f9,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$possible'(X1) <=> ? [X2 : '\$ki_world'] : (('\$in_ki_world'(X2) => X1) & '\$accessible_ki_world'(X0,X2))))), inference(theory_normalization,[],[f2])). tff(f2,axiom,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$possible'(X1) <=> ? [X2 : '\$ki_world'] : (('\$in_ki_world'(X2) => X1) & '\$accessible_ki_world'(X0,X2))))), file('NTF_Infinite-Finite.s.p',possible_defn)). tff(f291,plain,( ( ! [X3 : '\$ki_world',X4 : \$o] : ('\$in_ki_world'(sK12(X3,X4)) | ~'\$in_ki_world'(X3) | ~'\$possible'(X4)) ) | ~spl13_20), inference(duplicate_literal_removal,[],[f290])). tff(f290,plain,( ( ! [X3 : '\$ki_world',X4 : \$o] : (~'\$in_ki_world'(X3) | '\$in_ki_world'(sK12(X3,X4)) | ~'\$possible'(X4) | ~'\$in_ki_world'(X3)) ) | ~spl13_20), inference(resolution,[],[f279,f100])). tff(f100,plain,( ( ! [X0 : '\$ki_world',X1 : \$o] : ('\$accessible_ki_world'(X0,sK12(X0,X1)) | ~'\$possible'(X1) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f59])). tff(f1968,plain,( spl13_53 | ~spl13_52), inference(avatar_split_clause,[],[f1943,f1921,f1964])). tff(f1921,plain,( spl13_52 <=> \$less(-8,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_52])])). tff(f1943,plain,( \$less(-9,sK5) | ~spl13_52), inference(evaluation,[],[f1937])). tff(f1937,plain,( \$less(\$sum(-1,-8),sK5) | ~spl13_52), inference(resolution,[],[f1931,f626])). tff(f1931,plain,( ( ! [X2 : \$int] : (~\$less(X2,-8) | \$less(X2,sK5)) ) | ~spl13_52), inference(resolution,[],[f1923,f16])). tff(f1923,plain,( \$less(-8,sK5) | ~spl13_52), inference(avatar_component_clause,[],[f1921])). tff(f1967,plain,( spl13_53 | ~spl13_52), inference(avatar_split_clause,[],[f1942,f1921,f1964])). tff(f1942,plain,( \$less(-9,sK5) | ~spl13_52), inference(evaluation,[],[f1938])). tff(f1938,plain,( \$less(\$sum(-8,-1),sK5) | ~spl13_52), inference(resolution,[],[f1931,f637])). tff(f1927,plain,( spl13_52 | ~spl13_51), inference(avatar_split_clause,[],[f1856,f1659,f1921])). tff(f1659,plain,( spl13_51 <=> \$less(-7,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_51])])). tff(f1856,plain,( \$less(-8,sK5) | ~spl13_51), inference(evaluation,[],[f1850])). tff(f1850,plain,( \$less(\$sum(-1,-7),sK5) | ~spl13_51), inference(resolution,[],[f1783,f626])). tff(f1783,plain,( ( ! [X2 : \$int] : (~\$less(X2,-7) | \$less(X2,sK5)) ) | ~spl13_51), inference(resolution,[],[f1661,f16])). tff(f1661,plain,( \$less(-7,sK5) | ~spl13_51), inference(avatar_component_clause,[],[f1659])). tff(f1924,plain,( spl13_52 | ~spl13_51), inference(avatar_split_clause,[],[f1855,f1659,f1921])). tff(f1855,plain,( \$less(-8,sK5) | ~spl13_51), inference(evaluation,[],[f1851])). tff(f1851,plain,( \$less(\$sum(-7,-1),sK5) | ~spl13_51), inference(resolution,[],[f1783,f637])). tff(f1668,plain,( spl13_51 | ~spl13_50), inference(avatar_split_clause,[],[f1605,f1498,f1659])). tff(f1498,plain,( spl13_50 <=> \$less(-6,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_50])])). tff(f1605,plain,( \$less(-7,sK5) | ~spl13_50), inference(evaluation,[],[f1599])). tff(f1599,plain,( \$less(\$sum(-1,-6),sK5) | ~spl13_50), inference(resolution,[],[f1540,f626])). tff(f1540,plain,( ( ! [X2 : \$int] : (~\$less(X2,-6) | \$less(X2,sK5)) ) | ~spl13_50), inference(resolution,[],[f1500,f16])). tff(f1500,plain,( \$less(-6,sK5) | ~spl13_50), inference(avatar_component_clause,[],[f1498])). tff(f1662,plain,( spl13_51 | ~spl13_50), inference(avatar_split_clause,[],[f1604,f1498,f1659])). tff(f1604,plain,( \$less(-7,sK5) | ~spl13_50), inference(evaluation,[],[f1600])). tff(f1600,plain,( \$less(\$sum(-6,-1),sK5) | ~spl13_50), inference(resolution,[],[f1540,f637])). tff(f1502,plain,( spl13_50 | ~spl13_49), inference(avatar_split_clause,[],[f1474,f1377,f1498])). tff(f1377,plain,( spl13_49 <=> \$less(-5,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_49])])). tff(f1474,plain,( \$less(-6,sK5) | ~spl13_49), inference(evaluation,[],[f1469])). tff(f1469,plain,( \$less(\$sum(-1,-5),sK5) | ~spl13_49), inference(resolution,[],[f1460,f626])). tff(f1460,plain,( ( ! [X2 : \$int] : (~\$less(X2,-5) | \$less(X2,sK5)) ) | ~spl13_49), inference(resolution,[],[f1379,f16])). tff(f1379,plain,( \$less(-5,sK5) | ~spl13_49), inference(avatar_component_clause,[],[f1377])). tff(f1501,plain,( spl13_50 | ~spl13_49), inference(avatar_split_clause,[],[f1473,f1377,f1498])). tff(f1473,plain,( \$less(-6,sK5) | ~spl13_49), inference(evaluation,[],[f1470])). tff(f1470,plain,( \$less(\$sum(-5,-1),sK5) | ~spl13_49), inference(resolution,[],[f1460,f637])). tff(f1422,plain,( spl13_49 | ~spl13_48), inference(avatar_split_clause,[],[f1375,f1330,f1377])). tff(f1330,plain,( spl13_48 <=> \$less(-4,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_48])])). tff(f1375,plain,( \$less(-5,sK5) | ~spl13_48), inference(evaluation,[],[f1370])). tff(f1370,plain,( \$less(\$sum(-1,-4),sK5) | ~spl13_48), inference(resolution,[],[f1337,f626])). tff(f1337,plain,( ( ! [X1 : \$int] : (~\$less(X1,-4) | \$less(X1,sK5)) ) | ~spl13_48), inference(resolution,[],[f1332,f16])). tff(f1332,plain,( \$less(-4,sK5) | ~spl13_48), inference(avatar_component_clause,[],[f1330])). tff(f1380,plain,( spl13_49 | ~spl13_48), inference(avatar_split_clause,[],[f1374,f1330,f1377])). tff(f1374,plain,( \$less(-5,sK5) | ~spl13_48), inference(evaluation,[],[f1371])). tff(f1371,plain,( \$less(\$sum(-4,-1),sK5) | ~spl13_48), inference(resolution,[],[f1337,f637])). tff(f1334,plain,( spl13_48 | ~spl13_47), inference(avatar_split_clause,[],[f1328,f1108,f1330])). tff(f1108,plain,( spl13_47 <=> \$less(-3,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_47])])). tff(f1328,plain,( \$less(-4,sK5) | ~spl13_47), inference(evaluation,[],[f1323])). tff(f1323,plain,( \$less(\$sum(-1,-3),sK5) | ~spl13_47), inference(resolution,[],[f1172,f626])). tff(f1172,plain,( ( ! [X1 : \$int] : (~\$less(X1,-3) | \$less(X1,sK5)) ) | ~spl13_47), inference(resolution,[],[f1110,f16])). tff(f1110,plain,( \$less(-3,sK5) | ~spl13_47), inference(avatar_component_clause,[],[f1108])). tff(f1333,plain,( spl13_48 | ~spl13_47), inference(avatar_split_clause,[],[f1327,f1108,f1330])). tff(f1327,plain,( \$less(-4,sK5) | ~spl13_47), inference(evaluation,[],[f1324])). tff(f1324,plain,( \$less(\$sum(-3,-1),sK5) | ~spl13_47), inference(resolution,[],[f1172,f637])). tff(f1116,plain,( spl13_47 | ~spl13_44), inference(avatar_split_clause,[],[f1078,f890,f1108])). tff(f890,plain,( spl13_44 <=> \$less(-2,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_44])])). tff(f1078,plain,( \$less(-3,sK5) | ~spl13_44), inference(evaluation,[],[f1073])). tff(f1073,plain,( \$less(\$sum(-1,-2),sK5) | ~spl13_44), inference(resolution,[],[f922,f626])). tff(f922,plain,( ( ! [X0 : \$int] : (~\$less(X0,-2) | \$less(X0,sK5)) ) | ~spl13_44), inference(resolution,[],[f892,f16])). tff(f892,plain,( \$less(-2,sK5) | ~spl13_44), inference(avatar_component_clause,[],[f890])). tff(f1111,plain,( spl13_47 | ~spl13_44), inference(avatar_split_clause,[],[f1077,f890,f1108])). tff(f1077,plain,( \$less(-3,sK5) | ~spl13_44), inference(evaluation,[],[f1074])). tff(f1074,plain,( \$less(\$sum(-2,-1),sK5) | ~spl13_44), inference(resolution,[],[f922,f637])). tff(f967,plain,( spl13_46 | ~spl13_45), inference(avatar_split_clause,[],[f960,f924,f964])). tff(f924,plain,( spl13_45 <=> (\$true = bG0(sK6(sK6(geoff))))), introduced(avatar_definition,[new_symbols(naming,[spl13_45])])). tff(f960,plain,( like(sK6(sK6(geoff))) | ~spl13_45), inference(trivial_inequality_removal,[],[f959])). tff(f959,plain,( (\$true != \$true) | like(sK6(sK6(geoff))) | ~spl13_45), inference(superposition,[],[f61,f926])). tff(f926,plain,( (\$true = bG0(sK6(sK6(geoff)))) | ~spl13_45), inference(avatar_component_clause,[],[f924])). tff(f61,plain,( ( ! [X0 : person] : ((\$true != bG0(X0)) | like(X0)) )), inference(cnf_transformation,[],[f39])). tff(f39,plain,( ! [X0 : person] : ((like(X0) | (\$true != bG0(X0))) & ((\$true = bG0(X0)) | ~like(X0)))), inference(nnf_transformation,[],[f25])). tff(f25,plain,( ! [X0 : person] : (like(X0) <=> (\$true = bG0(X0)))), inference(fool_elimination,[],[f24])). tff(f927,plain,( spl13_45 | ~spl13_11 | ~spl13_37), inference(avatar_split_clause,[],[f554,f549,f169,f924])). tff(f554,plain,( (\$true = bG0(sK6(sK6(geoff)))) | (~spl13_11 | ~spl13_37)), inference(resolution,[],[f551,f186])). tff(f186,plain,( ( ! [X0 : person] : (~like(X0) | (\$true = bG0(sK6(X0)))) ) | ~spl13_11), inference(resolution,[],[f170,f60])). tff(f60,plain,( ( ! [X0 : person] : (~like(X0) | (\$true = bG0(X0))) )), inference(cnf_transformation,[],[f39])). tff(f170,plain,( ( ! [X6 : person] : (like(sK6(X6)) | ~like(X6)) ) | ~spl13_11), inference(avatar_component_clause,[],[f169])). tff(f894,plain,( spl13_44 | ~spl13_33), inference(avatar_split_clause,[],[f888,f484,f890])). tff(f484,plain,( spl13_33 <=> \$less(-1,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_33])])). tff(f888,plain,( \$less(-2,sK5) | ~spl13_33), inference(evaluation,[],[f882])). tff(f882,plain,( \$less(\$sum(-1,-1),sK5) | ~spl13_33), inference(resolution,[],[f489,f626])). tff(f489,plain,( ( ! [X0 : \$int] : (~\$less(X0,-1) | \$less(X0,sK5)) ) | ~spl13_33), inference(resolution,[],[f486,f16])). tff(f486,plain,( \$less(-1,sK5) | ~spl13_33), inference(avatar_component_clause,[],[f484])). tff(f893,plain,( spl13_44 | ~spl13_33), inference(avatar_split_clause,[],[f887,f484,f890])). tff(f887,plain,( \$less(-2,sK5) | ~spl13_33), inference(evaluation,[],[f883])). tff(f883,plain,( \$less(\$sum(-1,-1),sK5) | ~spl13_33), inference(resolution,[],[f489,f637])). tff(f783,plain,( spl13_42 | spl13_43 | spl13_32), inference(avatar_split_clause,[],[f462,f458,f780,f776])). tff(f776,plain,( spl13_42 <=> 1 = sK5), introduced(avatar_definition,[new_symbols(naming,[spl13_42])])). tff(f780,plain,( spl13_43 <=> \$less(1,sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_43])])). tff(f458,plain,( spl13_32 <=> \$less(sK5,1)), introduced(avatar_definition,[new_symbols(naming,[spl13_32])])). tff(f462,plain,( \$less(1,sK5) | 1 = sK5 | spl13_32), inference(resolution,[],[f460,f17])). tff(f460,plain,( ~\$less(sK5,1) | spl13_32), inference(avatar_component_clause,[],[f458])). tff(f654,plain,( spl13_41 | ~spl13_26 | ~spl13_31 | ~spl13_35), inference(avatar_split_clause,[],[f649,f521,f442,f381,f651])). tff(f651,plain,( spl13_41 <=> sK5 = sK7(geoff)), introduced(avatar_definition,[new_symbols(naming,[spl13_41])])). tff(f442,plain,( spl13_31 <=> ! [X2 : \$int,X3 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2))), introduced(avatar_definition,[new_symbols(naming,[spl13_31])])). tff(f649,plain,( sK5 = sK7(geoff) | (~spl13_26 | ~spl13_31 | ~spl13_35)), inference(superposition,[],[f648,f523])). tff(f648,plain,( ( ! [X0 : \$int] : (sK7(int2person(X0)) = X0) ) | (~spl13_26 | ~spl13_31)), inference(equality_resolution,[],[f454])). tff(f454,plain,( ( ! [X0 : person,X1 : \$int] : (int2person(X1) != X0 | sK7(X0) = X1) ) | (~spl13_26 | ~spl13_31)), inference(superposition,[],[f443,f382])). tff(f443,plain,( ( ! [X2 : \$int,X3 : \$int] : (int2person(X3) != int2person(X2) | X2 = X3) ) | ~spl13_31), inference(avatar_component_clause,[],[f442])). tff(f603,plain,( spl13_40 | ~spl13_2), inference(avatar_split_clause,[],[f597,f113,f600])). tff(f600,plain,( spl13_40 <=> 0 = sK9('\$local_ki_world')), introduced(avatar_definition,[new_symbols(naming,[spl13_40])])). tff(f597,plain,( 0 = sK9('\$local_ki_world') | ~spl13_2), inference(superposition,[],[f596,f115])). tff(f596,plain,( ( ! [X0 : \$int] : (sK9(int2ki_world(X0)) = X0) )), inference(equality_resolution,[],[f235])). tff(f235,plain,( ( ! [X2 : \$int,X1 : '\$ki_world'] : (int2ki_world(X2) != X1 | sK9(X1) = X2) )), inference(superposition,[],[f80,f81])). tff(f81,plain,( ( ! [X12 : '\$ki_world'] : (int2ki_world(sK9(X12)) = X12) )), inference(cnf_transformation,[],[f51])). tff(f80,plain,( ( ! [X14 : \$int,X15 : \$int] : (int2ki_world(X14) != int2ki_world(X15) | X14 = X15) )), inference(cnf_transformation,[],[f51])). tff(f576,plain,( spl13_39 | ~spl13_34 | ~spl13_35), inference(avatar_split_clause,[],[f527,f521,f514,f572])). tff(f572,plain,( spl13_39 <=> (\$true = bG0(sK6(geoff)))), introduced(avatar_definition,[new_symbols(naming,[spl13_39])])). tff(f514,plain,( spl13_34 <=> (\$true = bG0(sK6(int2person(sK5))))), introduced(avatar_definition,[new_symbols(naming,[spl13_34])])). tff(f527,plain,( (\$true = bG0(sK6(geoff))) | (~spl13_34 | ~spl13_35)), inference(backward_demodulation,[],[f516,f523])). tff(f516,plain,( (\$true = bG0(sK6(int2person(sK5)))) | ~spl13_34), inference(avatar_component_clause,[],[f514])). tff(f575,plain,( spl13_39 | ~spl13_11 | ~spl13_16), inference(avatar_split_clause,[],[f525,f203,f169,f572])). tff(f525,plain,( (\$true = bG0(sK6(geoff))) | (~spl13_11 | ~spl13_16)), inference(resolution,[],[f205,f186])). tff(f205,plain,( like(geoff) | ~spl13_16), inference(avatar_component_clause,[],[f203])). tff(f560,plain,( spl13_5 | spl13_38 | ~spl13_9 | ~spl13_35), inference(avatar_split_clause,[],[f553,f521,f156,f557,f126])). tff(f557,plain,( spl13_38 <=> sK5 = id_of(geoff)), introduced(avatar_definition,[new_symbols(naming,[spl13_38])])). tff(f553,plain,( sK5 = id_of(geoff) | \$less(sK5,0) | (~spl13_9 | ~spl13_35)), inference(forward_demodulation,[],[f394,f523])). tff(f394,plain,( sK5 = id_of(int2person(sK5)) | \$less(sK5,0) | ~spl13_9), inference(resolution,[],[f92,f158])). tff(f92,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | id_of(int2person(X0)) = X0 | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f552,plain,( spl13_37 | ~spl13_34 | ~spl13_35), inference(avatar_split_clause,[],[f544,f521,f514,f549])). tff(f544,plain,( like(sK6(geoff)) | (~spl13_34 | ~spl13_35)), inference(forward_demodulation,[],[f519,f523])). tff(f519,plain,( like(sK6(int2person(sK5))) | ~spl13_34), inference(trivial_inequality_removal,[],[f518])). tff(f518,plain,( (\$true != \$true) | like(sK6(int2person(sK5))) | ~spl13_34), inference(superposition,[],[f61,f516])). tff(f537,plain,( spl13_36 | ~spl13_16), inference(avatar_split_clause,[],[f526,f203,f534])). tff(f534,plain,( spl13_36 <=> (\$true = bG0(geoff))), introduced(avatar_definition,[new_symbols(naming,[spl13_36])])). tff(f526,plain,( (\$true = bG0(geoff)) | ~spl13_16), inference(resolution,[],[f205,f60])). tff(f524,plain,( spl13_5 | spl13_35 | ~spl13_9), inference(avatar_split_clause,[],[f336,f156,f521,f126])). tff(f336,plain,( geoff = int2person(sK5) | \$less(sK5,0) | ~spl13_9), inference(resolution,[],[f91,f158])). tff(f91,plain,( ( ! [X0 : \$int] : (~'\$in_ki_world'(int2ki_world(X0)) | geoff = int2person(X0) | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f517,plain,( spl13_34 | ~spl13_11 | ~spl13_27), inference(avatar_split_clause,[],[f512,f390,f169,f514])). tff(f390,plain,( spl13_27 <=> like(int2person(sK5))), introduced(avatar_definition,[new_symbols(naming,[spl13_27])])). tff(f512,plain,( (\$true = bG0(sK6(int2person(sK5)))) | (~spl13_11 | ~spl13_27)), inference(resolution,[],[f186,f392])). tff(f392,plain,( like(int2person(sK5)) | ~spl13_27), inference(avatar_component_clause,[],[f390])). tff(f488,plain,( spl13_33 | ~spl13_24), inference(avatar_split_clause,[],[f482,f348,f484])). tff(f482,plain,( \$less(-1,sK5) | ~spl13_24), inference(evaluation,[],[f480])). tff(f480,plain,( \$less(0,0) | \$less(-1,sK5) | ~spl13_24), inference(resolution,[],[f433,f375])). tff(f487,plain,( spl13_33 | spl13_5), inference(avatar_split_clause,[],[f476,f126,f484])). tff(f476,plain,( \$less(-1,sK5) | spl13_5), inference(resolution,[],[f433,f128])). tff(f128,plain,( ~\$less(sK5,0) | spl13_5), inference(avatar_component_clause,[],[f126])). tff(f461,plain,( ~spl13_32 | ~spl13_24), inference(avatar_split_clause,[],[f445,f348,f458])). tff(f445,plain,( ~\$less(sK5,1) | ~spl13_24), inference(resolution,[],[f223,f350])). tff(f223,plain,( ( ! [X2 : \$int] : (~\$less(0,X2) | ~\$less(X2,1)) )), inference(superposition,[],[f21,f174])). tff(f444,plain,( spl13_25 | spl13_31), inference(avatar_split_clause,[],[f90,f442,f378])). tff(f90,plain,( ( ! [X2 : \$int,X3 : \$int,X0 : \$int] : (X2 = X3 | int2person(X3) != int2person(X2) | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f415,plain,( spl13_29 | spl13_30), inference(avatar_split_clause,[],[f96,f413,f410])). tff(f410,plain,( spl13_29 <=> ! [X0 : '\$ki_world',X3 : '\$ki_world'] : (~'\$in_ki_world'(X3) | ~'\$in_ki_world'(X0) | ~'\$accessible_ki_world'(X0,X3))), introduced(avatar_definition,[new_symbols(naming,[spl13_29])])). tff(f413,plain,( spl13_30 <=> ! [X1 : \$o] : ((\$true = X1) | ~'\$necessary'(X1))), introduced(avatar_definition,[new_symbols(naming,[spl13_30])])). tff(f96,plain,( ( ! [X3 : '\$ki_world',X0 : '\$ki_world',X1 : \$o] : ((\$true = X1) | ~'\$in_ki_world'(X3) | ~'\$accessible_ki_world'(X0,X3) | ~'\$necessary'(X1) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f55])). tff(f55,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$necessary'(X1) | ((\$true != X1) & '\$in_ki_world'(sK11(X0,X1)) & '\$accessible_ki_world'(X0,sK11(X0,X1)))) & (! [X3 : '\$ki_world'] : ((\$true = X1) | ~'\$in_ki_world'(X3) | ~'\$accessible_ki_world'(X0,X3)) | ~'\$necessary'(X1))) | ~'\$in_ki_world'(X0))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK11])],[f53,f54])). tff(f54,plain,( ! [X0 : '\$ki_world',X1 : \$o] : (? [X2 : '\$ki_world'] : ((\$true != X1) & '\$in_ki_world'(X2) & '\$accessible_ki_world'(X0,X2)) => ((\$true != X1) & '\$in_ki_world'(sK11(X0,X1)) & '\$accessible_ki_world'(X0,sK11(X0,X1))))), introduced(choice_axiom,[])). tff(f53,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$necessary'(X1) | ? [X2 : '\$ki_world'] : ((\$true != X1) & '\$in_ki_world'(X2) & '\$accessible_ki_world'(X0,X2))) & (! [X3 : '\$ki_world'] : ((\$true = X1) | ~'\$in_ki_world'(X3) | ~'\$accessible_ki_world'(X0,X3)) | ~'\$necessary'(X1))) | ~'\$in_ki_world'(X0))), inference(rectify,[],[f52])). tff(f52,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : (('\$necessary'(X1) | ? [X2 : '\$ki_world'] : ((\$true != X1) & '\$in_ki_world'(X2) & '\$accessible_ki_world'(X0,X2))) & (! [X2 : '\$ki_world'] : ((\$true = X1) | ~'\$in_ki_world'(X2) | ~'\$accessible_ki_world'(X0,X2)) | ~'\$necessary'(X1))) | ~'\$in_ki_world'(X0))), inference(nnf_transformation,[],[f37])). tff(f37,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : ((\$true = X1) | ~'\$in_ki_world'(X2) | ~'\$accessible_ki_world'(X0,X2))) | ~'\$in_ki_world'(X0))), inference(flattening,[],[f36])). tff(f36,plain,( ! [X0 : '\$ki_world'] : (! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : (((\$true = X1) | ~'\$in_ki_world'(X2)) | ~'\$accessible_ki_world'(X0,X2))) | ~'\$in_ki_world'(X0))), inference(ennf_transformation,[],[f28])). tff(f28,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : ('\$accessible_ki_world'(X0,X2) => ('\$in_ki_world'(X2) => (\$true = X1)))))), inference(fool_elimination,[],[f27])). tff(f27,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : ('\$accessible_ki_world'(X0,X2) => ('\$in_ki_world'(X2) => X1))))), inference(rectify,[],[f8])). tff(f8,plain,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : ('\$accessible_ki_world'(X0,X2) => ('\$in_ki_world'(X2) => X1))))), inference(theory_normalization,[],[f1])). tff(f1,axiom,( ! [X0 : '\$ki_world'] : ('\$in_ki_world'(X0) => ! [X1 : \$o] : ('\$necessary'(X1) <=> ! [X2 : '\$ki_world'] : ('\$accessible_ki_world'(X0,X2) => ('\$in_ki_world'(X2) => X1))))), file('NTF_Infinite-Finite.s.p',necessary_defn)). tff(f403,plain,( spl13_28 | ~spl13_27), inference(avatar_split_clause,[],[f398,f390,f400])). tff(f400,plain,( spl13_28 <=> (\$true = bG0(int2person(sK5)))), introduced(avatar_definition,[new_symbols(naming,[spl13_28])])). tff(f398,plain,( (\$true = bG0(int2person(sK5))) | ~spl13_27), inference(resolution,[],[f392,f60])). tff(f393,plain,( spl13_5 | spl13_27 | ~spl13_9), inference(avatar_split_clause,[],[f265,f156,f390,f126])). tff(f265,plain,( like(int2person(sK5)) | \$less(sK5,0) | ~spl13_9), inference(resolution,[],[f93,f158])). tff(f388,plain,( spl13_5 | ~spl13_9 | ~spl13_25), inference(avatar_split_clause,[],[f384,f378,f156,f126])). tff(f384,plain,( \$less(sK5,0) | (~spl13_9 | ~spl13_25)), inference(resolution,[],[f379,f158])). tff(f383,plain,( spl13_25 | spl13_26), inference(avatar_split_clause,[],[f89,f381,f378])). tff(f89,plain,( ( ! [X0 : \$int,X4 : person] : (int2person(sK7(X4)) = X4 | ~'\$in_ki_world'(int2ki_world(X0)) | \$less(X0,0)) )), inference(cnf_transformation,[],[f51])). tff(f351,plain,( spl13_23 | spl13_24 | spl13_5), inference(avatar_split_clause,[],[f254,f126,f348,f344])). tff(f344,plain,( spl13_23 <=> 0 = sK5), introduced(avatar_definition,[new_symbols(naming,[spl13_23])])). tff(f254,plain,( \$less(0,sK5) | 0 = sK5 | spl13_5), inference(resolution,[],[f17,f128])). tff(f335,plain,( spl13_22 | spl13_16), inference(avatar_split_clause,[],[f312,f203,f332])). tff(f332,plain,( spl13_22 <=> (\$false = bG0(geoff))), introduced(avatar_definition,[new_symbols(naming,[spl13_22])])). tff(f312,plain,( (\$false = bG0(geoff)) | spl13_16), inference(resolution,[],[f148,f204])). tff(f204,plain,( ~like(geoff) | spl13_16), inference(avatar_component_clause,[],[f203])). tff(f148,plain,( ( ! [X0 : person] : (like(X0) | (\$false = bG0(X0))) )), inference(trivial_inequality_removal,[],[f146])). tff(f146,plain,( ( ! [X0 : person] : ((\$true != \$true) | like(X0) | (\$false = bG0(X0))) )), inference(superposition,[],[f61,f23])). tff(f283,plain,( spl13_20 | spl13_21), inference(avatar_split_clause,[],[f102,f281,f278])). tff(f102,plain,( ( ! [X2 : '\$ki_world',X0 : '\$ki_world',X1 : \$o] : ('\$possible'(X1) | '\$in_ki_world'(X2) | ~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f59])). tff(f276,plain,( spl13_19 | spl13_10), inference(avatar_split_clause,[],[f211,f162,f271])). tff(f271,plain,( spl13_19 <=> (\$false = bG0(int2person(0)))), introduced(avatar_definition,[new_symbols(naming,[spl13_19])])). tff(f162,plain,( spl13_10 <=> (\$true = bG0(int2person(0)))), introduced(avatar_definition,[new_symbols(naming,[spl13_10])])). tff(f211,plain,( (\$false = bG0(int2person(0))) | spl13_10), inference(trivial_inequality_removal,[],[f210])). tff(f210,plain,( (\$true != \$true) | (\$false = bG0(int2person(0))) | spl13_10), inference(superposition,[],[f163,f23])). tff(f163,plain,( (\$true != bG0(int2person(0))) | spl13_10), inference(avatar_component_clause,[],[f162])). tff(f275,plain,( spl13_19 | spl13_10), inference(avatar_split_clause,[],[f208,f162,f271])). tff(f208,plain,( (\$false = bG0(int2person(0))) | spl13_10), inference(trivial_inequality_removal,[],[f166])). tff(f166,plain,( (\$true != \$true) | (\$false = bG0(int2person(0))) | spl13_10), inference(superposition,[],[f163,f23])). tff(f274,plain,( spl13_19 | spl13_10), inference(avatar_split_clause,[],[f167,f162,f271])). tff(f167,plain,( (\$false = bG0(int2person(0))) | spl13_10), inference(trivial_inequality_removal,[],[f166])). tff(f244,plain,( spl13_18 | spl13_5), inference(avatar_split_clause,[],[f227,f126,f241])). tff(f241,plain,( spl13_18 <=> int2ki_world(sK5) = sK10(sK5)), introduced(avatar_definition,[new_symbols(naming,[spl13_18])])). tff(f227,plain,( int2ki_world(sK5) = sK10(sK5) | spl13_5), inference(resolution,[],[f78,f128])). tff(f233,plain,( spl13_17 | ~spl13_2), inference(avatar_split_clause,[],[f228,f113,f230])). tff(f230,plain,( spl13_17 <=> '\$local_ki_world' = sK10(0)), introduced(avatar_definition,[new_symbols(naming,[spl13_17])])). tff(f228,plain,( '\$local_ki_world' = sK10(0) | ~spl13_2), inference(forward_demodulation,[],[f226,f115])). tff(f226,plain,( int2ki_world(0) = sK10(0)), inference(resolution,[],[f78,f15])). tff(f207,plain,( spl13_8 | ~spl13_10), inference(avatar_split_clause,[],[f179,f162,f151])). tff(f179,plain,( like(int2person(0)) | ~spl13_10), inference(trivial_inequality_removal,[],[f178])). tff(f178,plain,( (\$true != \$true) | like(int2person(0)) | ~spl13_10), inference(superposition,[],[f61,f164])). tff(f164,plain,( (\$true = bG0(int2person(0))) | ~spl13_10), inference(avatar_component_clause,[],[f162])). tff(f206,plain,( spl13_16 | ~spl13_8 | ~spl13_12), inference(avatar_split_clause,[],[f201,f182,f151,f203])). tff(f201,plain,( like(geoff) | (~spl13_8 | ~spl13_12)), inference(backward_demodulation,[],[f153,f184])). tff(f199,plain,( spl13_15 | spl13_6), inference(avatar_split_clause,[],[f65,f130,f197])). tff(f65,plain,( ( ! [X6 : person] : ('\$in_ki_world'('\$local_ki_world') | sK6(X6) != X6 | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f194,plain,( spl13_13 | spl13_14), inference(avatar_split_clause,[],[f106,f191,f188])). tff(f106,plain,( ( ! [X2 : '\$ki_world',X0 : '\$ki_world'] : ('\$possible'(\$true) | ~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0)) )), inference(equality_resolution,[],[f103])). tff(f103,plain,( ( ! [X2 : '\$ki_world',X0 : '\$ki_world',X1 : \$o] : ('\$possible'(X1) | (\$true != X1) | ~'\$accessible_ki_world'(X0,X2) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f59])). tff(f185,plain,( spl13_12 | ~spl13_6 | ~spl13_2), inference(avatar_split_clause,[],[f180,f113,f130,f182])). tff(f180,plain,( ~'\$in_ki_world'('\$local_ki_world') | geoff = int2person(0) | ~spl13_2), inference(forward_demodulation,[],[f86,f115])). tff(f86,plain,( geoff = int2person(0) | ~'\$in_ki_world'(int2ki_world(0))), inference(cnf_transformation,[],[f51])). tff(f173,plain,( spl13_10 | ~spl13_8), inference(avatar_split_clause,[],[f160,f151,f162])). tff(f160,plain,( (\$true = bG0(int2person(0))) | ~spl13_8), inference(resolution,[],[f153,f60])). tff(f171,plain,( spl13_11 | spl13_6), inference(avatar_split_clause,[],[f64,f130,f169])). tff(f64,plain,( ( ! [X6 : person] : ('\$in_ki_world'('\$local_ki_world') | like(sK6(X6)) | ~like(X6)) )), inference(cnf_transformation,[],[f45])). tff(f165,plain,( spl13_10 | ~spl13_8), inference(avatar_split_clause,[],[f160,f151,f162])). tff(f159,plain,( spl13_9 | spl13_6), inference(avatar_split_clause,[],[f63,f130,f156])). tff(f63,plain,( '\$in_ki_world'('\$local_ki_world') | '\$in_ki_world'(int2ki_world(sK5))), inference(cnf_transformation,[],[f45])). tff(f154,plain,( spl13_8 | ~spl13_6 | ~spl13_2), inference(avatar_split_clause,[],[f149,f113,f130,f151])). tff(f149,plain,( ~'\$in_ki_world'('\$local_ki_world') | like(int2person(0)) | ~spl13_2), inference(forward_demodulation,[],[f88,f115])). tff(f88,plain,( like(int2person(0)) | ~'\$in_ki_world'(int2ki_world(0))), inference(cnf_transformation,[],[f51])). tff(f141,plain,( spl13_7 | ~spl13_2), inference(avatar_split_clause,[],[f136,f113,f138])). tff(f136,plain,( '\$accessible_ki_world'('\$local_ki_world','\$local_ki_world') | ~spl13_2), inference(forward_demodulation,[],[f82,f115])). tff(f82,plain,( '\$accessible_ki_world'(int2ki_world(0),int2ki_world(0))), inference(cnf_transformation,[],[f51])). tff(f135,plain,( ~spl13_3 | ~spl13_6), inference(avatar_contradiction_clause,[],[f134])). tff(f134,plain,( \$false | (~spl13_3 | ~spl13_6)), inference(resolution,[],[f132,f119])). tff(f132,plain,( '\$in_ki_world'('\$local_ki_world') | ~spl13_6), inference(avatar_component_clause,[],[f130])). tff(f133,plain,( ~spl13_5 | spl13_6), inference(avatar_split_clause,[],[f62,f130,f126])). tff(f62,plain,( '\$in_ki_world'('\$local_ki_world') | ~\$less(sK5,0)), inference(cnf_transformation,[],[f45])). tff(f124,plain,( spl13_3 | spl13_4), inference(avatar_split_clause,[],[f105,f121,f118])). tff(f121,plain,( spl13_4 <=> '\$necessary'(\$true)), introduced(avatar_definition,[new_symbols(naming,[spl13_4])])). tff(f105,plain,( ( ! [X0 : '\$ki_world'] : ('\$necessary'(\$true) | ~'\$in_ki_world'(X0)) )), inference(equality_resolution,[],[f99])). tff(f99,plain,( ( ! [X0 : '\$ki_world',X1 : \$o] : ('\$necessary'(X1) | (\$true != X1) | ~'\$in_ki_world'(X0)) )), inference(cnf_transformation,[],[f55])). tff(f116,plain,( spl13_2), inference(avatar_split_clause,[],[f79,f113])). tff(f79,plain,( '\$local_ki_world' = int2ki_world(0)), inference(cnf_transformation,[],[f51])). tff(f111,plain,( ~spl13_1), inference(avatar_split_clause,[],[f22,f108])). tff(f108,plain,( spl13_1 <=> (\$true = \$false)), introduced(avatar_definition,[new_symbols(naming,[spl13_1])])). tff(f22,plain,( (\$true != \$false)), introduced(fool_axiom,[])). % SZS output end Proof for NTF_Infinite-Finite.s