% SZS status Theorem for NTF_Finite-Infinite.s
% SZS output start Proof for NTF_Finite-Infinite.s
tff(type_def_5, type, '$world': $tType).
tff(type_def_6, type, sequence: $tType).
tff(func_def_0, type, '$local_world': '$world').
tff(func_def_1, type, null: sequence).
tff(func_def_2, type, toss: (sequence) > sequence).
tff(func_def_3, type, w1: '$world').
tff(func_def_4, type, w2: '$world').
tff(func_def_5, type, int2sequence: ($int) > sequence).
tff(func_def_16, type, sK0: '$world').
tff(func_def_19, type, sK1: sequence).
tff(func_def_20, type, sK2: sequence).
tff(func_def_21, type, sK3: sequence).
tff(func_def_22, type, sK4: sequence).
tff(func_def_23, type, sK5: sequence).
tff(func_def_24, type, sK6: sequence).
tff(func_def_25, type, sK7: $int).
tff(func_def_26, type, sK8: $int).
tff(func_def_27, type, sK9: $int).
tff(func_def_28, type, sK10: $int).
tff(func_def_29, type, sK11: sequence).
tff(func_def_30, type, sK12: $int).
tff(func_def_31, type, sK13: $int).
tff(func_def_32, type, sK14: $int).
tff(func_def_33, type, sK15: $int).
tff(func_def_34, type, sK16: (sequence) > $int).
tff(func_def_35, type, sK17: (sequence) > $int).
tff(func_def_36, type, sK18: ('$world' * $o) > '$world').
tff(func_def_37, type, sK20: ('$world' * $o) > '$world').
tff(pred_def_1, type, '$accessible_world': ('$world' * '$world') > $o).
tff(pred_def_2, type, '$in_world': ('$world' * $o) > $o).
tff(pred_def_3, type, '$necessary': ('$world' * $o) > $o).
tff(pred_def_4, type, '$possible': ('$world' * $o) > $o).
tff(pred_def_5, type, all_heads: (sequence) > $o).
tff(pred_def_8, type, sK19: ('$world') > $o).
tff(pred_def_9, type, sK21: ('$world') > $o).
tff(f1521,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f224,f441,f446,f460,f464,f469,f474,f478,f483,f488,f489,f493,f497,f498,f502,f506,f510,f514,f518,f547,f553,f559,f561,f567,f569,f571,f573,f574,f575,f576,f577,f606,f612,f618,f620,f626,f628,f630,f632,f638,f640,f642,f644,f646,f648,f650,f652,f655,f658,f670,f769,f880,f882,f883,f884,f909,f912,f913,f914,f922,f936,f1184,f1204,f1207,f1298,f1304,f1322,f1327,f1329,f1360,f1361,f1363,f1373,f1429,f1441,f1451,f1491,f1520])).
tff(f1520,plain,(
  ~spl22_32 | ~spl22_55),
  inference(avatar_contradiction_clause,[],[f1519])).
tff(f1519,plain,(
  $false | (~spl22_32 | ~spl22_55)),
  inference(equality_resolution,[],[f1466])).
tff(f1466,plain,(
  ( ! [X2 : sequence] : (sK11 != X2) ) | (~spl22_32 | ~spl22_55)),
  inference(superposition,[],[f605,f492])).
tff(f492,plain,(
  ( ! [X4 : sequence] : (int2sequence(sK17(X4)) = X4) ) | ~spl22_32),
  inference(avatar_component_clause,[],[f491])).
tff(f491,plain,(
  spl22_32 <=> ! [X4 : sequence] : int2sequence(sK17(X4)) = X4),
  introduced(avatar_definition,[new_symbols(naming,[spl22_32])])).
tff(f605,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11) ) | ~spl22_55),
  inference(avatar_component_clause,[],[f604])).
tff(f604,plain,(
  spl22_55 <=> ! [X5 : $int] : int2sequence(X5) != sK11),
  introduced(avatar_definition,[new_symbols(naming,[spl22_55])])).
tff(f1491,plain,(
  spl22_57 | ~spl22_51 | spl22_50 | ~spl22_35 | ~spl22_56),
  inference(avatar_split_clause,[],[f1490,f609,f504,f584,f588,f615])).
tff(f615,plain,(
  spl22_57 <=> $less(sK15,2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_57])])).
tff(f588,plain,(
  spl22_51 <=> all_heads(int2sequence($quotient_e(sK15,2)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_51])])).
tff(f584,plain,(
  spl22_50 <=> all_heads(int2sequence(sK15))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_50])])).
tff(f504,plain,(
  spl22_35 <=> ! [X6 : $int] : ($less(X6,2) | all_heads(int2sequence(X6)) | ~all_heads(int2sequence($quotient_e(X6,2))) | $remainder_e(X6,2) != 0)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_35])])).
tff(f609,plain,(
  spl22_56 <=> 0 = $remainder_e(sK15,2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_56])])).
tff(f1490,plain,(
  all_heads(int2sequence(sK15)) | ~all_heads(int2sequence($quotient_e(sK15,2))) | $less(sK15,2) | (~spl22_35 | ~spl22_56)),
  inference(trivial_inequality_removal,[],[f1489])).
tff(f1489,plain,(
  0 != 0 | all_heads(int2sequence(sK15)) | ~all_heads(int2sequence($quotient_e(sK15,2))) | $less(sK15,2) | (~spl22_35 | ~spl22_56)),
  inference(superposition,[],[f505,f611])).
tff(f611,plain,(
  0 = $remainder_e(sK15,2) | ~spl22_56),
  inference(avatar_component_clause,[],[f609])).
tff(f505,plain,(
  ( ! [X6 : $int] : ($remainder_e(X6,2) != 0 | all_heads(int2sequence(X6)) | ~all_heads(int2sequence($quotient_e(X6,2))) | $less(X6,2)) ) | ~spl22_35),
  inference(avatar_component_clause,[],[f504])).
tff(f1451,plain,(
  ~spl22_4 | ~spl22_85),
  inference(avatar_split_clause,[],[f1014,f957,f241])).
tff(f241,plain,(
  spl22_4 <=> '$necessary'('$local_world',$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_4])])).
tff(f957,plain,(
  spl22_85 <=> '$possible'('$local_world',$false)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_85])])).
tff(f1014,plain,(
  ~'$necessary'('$local_world',$true) | ~spl22_85),
  inference(resolution,[],[f959,f195])).
tff(f195,plain,(
  ( ! [X0 : '$world'] : (~'$possible'(X0,$false) | ~'$necessary'(X0,$true)) )),
  inference(cnf_transformation,[],[f46])).
tff(f46,plain,(
  ! [X0 : '$world',X1 : $o] : ((~'$possible'(X0,X1) <=> '$necessary'(X0,~X1)) & (~'$necessary'(X0,X1) <=> '$possible'(X0,~X1)))),
  inference(ennf_transformation,[],[f41])).
tff(f41,plain,(
  ! [X0 : '$world',X1 : $o] : ((~'$possible'(X0,X1) <=> '$necessary'(X0,~X1)) & (~'$necessary'(X0,X1) <=> '$possible'(X0,~X1)))),
  inference(rectify,[],[f36])).
tff(f36,plain,(
  ! [X4 : '$world',X1 : $o] : ((~'$possible'(X4,X1) <=> '$necessary'(X4,~X1)) & (~'$necessary'(X4,X1) <=> '$possible'(X4,~X1)))),
  inference(theory_normalization,[],[f9])).
tff(f9,plain,(
  ! [X4 : '$world',X1 : $o] : ((~'$possible'(X4,X1) <=> '$necessary'(X4,~X1)) & (~'$necessary'(X4,X1) <=> '$possible'(X4,~X1)))),
  inference(theory_normalization,[],[f3])).
tff(f3,axiom,(
  ! [X4 : '$world',X1 : $o] : ((~'$possible'(X4,X1) <=> '$necessary'(X4,~X1)) & (~'$necessary'(X4,X1) <=> '$possible'(X4,~X1)))),
  file('NTF_Finite-Infinite.s.p',duality)).
tff(f959,plain,(
  '$possible'('$local_world',$false) | ~spl22_85),
  inference(avatar_component_clause,[],[f957])).
tff(f1441,plain,(
  spl22_85 | ~spl22_2 | ~spl22_61),
  inference(avatar_split_clause,[],[f1438,f667,f226,f957])).
tff(f226,plain,(
  spl22_2 <=> '$in_world'('$local_world',$false)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_2])])).
tff(f667,plain,(
  spl22_61 <=> '$accessible_world'('$local_world','$local_world')),
  introduced(avatar_definition,[new_symbols(naming,[spl22_61])])).
tff(f1438,plain,(
  '$possible'('$local_world',$false) | (~spl22_2 | ~spl22_61)),
  inference(resolution,[],[f1378,f669])).
tff(f669,plain,(
  '$accessible_world'('$local_world','$local_world') | ~spl22_61),
  inference(avatar_component_clause,[],[f667])).
tff(f1378,plain,(
  ( ! [X1 : '$world'] : (~'$accessible_world'(X1,'$local_world') | '$possible'(X1,$false)) ) | ~spl22_2),
  inference(resolution,[],[f227,f212])).
tff(f212,plain,(
  ( ! [X3 : '$world',X0 : '$world'] : (~'$in_world'(X3,$false) | ~'$accessible_world'(X0,X3) | '$possible'(X0,$false)) )),
  inference(cnf_transformation,[],[f48])).
tff(f48,plain,(
  ! [X0 : '$world',X2 : $o] : ('$possible'(X0,X2) <=> ? [X3 : '$world'] : (? [X4 : $o] : ((X2 | ~X4) & '$in_world'(X3,X4)) & '$accessible_world'(X0,X3)))),
  inference(ennf_transformation,[],[f43])).
tff(f43,plain,(
  ! [X0 : '$world',X2 : $o] : ('$possible'(X0,X2) <=> ? [X3 : '$world'] : (? [X4 : $o] : ((X4 => X2) & '$in_world'(X3,X4)) & '$accessible_world'(X0,X3)))),
  inference(rectify,[],[f38])).
tff(f38,plain,(
  ! [X0 : '$world',X1 : $o,X1 : $o] : ('$possible'(X0,X1) <=> ? [X2 : '$world'] : (? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3)) & '$accessible_world'(X0,X2)))),
  inference(theory_normalization,[],[f11])).
tff(f11,plain,(
  ! [X0 : '$world',X1 : $o,X1 : $o] : ('$possible'(X0,X1) <=> ? [X2 : '$world'] : (? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3)) & '$accessible_world'(X0,X2)))),
  inference(theory_normalization,[],[f2])).
tff(f2,axiom,(
  ! [X0 : '$world',X1 : $o,X1 : $o] : ('$possible'(X0,X1) <=> ? [X2 : '$world'] : (? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3)) & '$accessible_world'(X0,X2)))),
  file('NTF_Finite-Infinite.s.p',possible_defn)).
tff(f227,plain,(
  '$in_world'('$local_world',$false) | ~spl22_2),
  inference(avatar_component_clause,[],[f226])).
tff(f1429,plain,(
  spl22_58 | ~spl22_34 | spl22_52),
  inference(avatar_split_clause,[],[f1428,f592,f500,f623])).
tff(f623,plain,(
  spl22_58 <=> 1 = sK14),
  introduced(avatar_definition,[new_symbols(naming,[spl22_58])])).
tff(f500,plain,(
  spl22_34 <=> ! [X1 : $int] : (1 = X1 | toss(int2sequence(X1)) = int2sequence($product(X1,2)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_34])])).
tff(f592,plain,(
  spl22_52 <=> toss(int2sequence(sK14)) = int2sequence($product(sK14,2))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_52])])).
tff(f1428,plain,(
  1 = sK14 | (~spl22_34 | spl22_52)),
  inference(trivial_inequality_removal,[],[f1422])).
tff(f1422,plain,(
  toss(int2sequence(sK14)) != toss(int2sequence(sK14)) | 1 = sK14 | (~spl22_34 | spl22_52)),
  inference(superposition,[],[f594,f501])).
tff(f501,plain,(
  ( ! [X1 : $int] : (toss(int2sequence(X1)) = int2sequence($product(X1,2)) | 1 = X1) ) | ~spl22_34),
  inference(avatar_component_clause,[],[f500])).
tff(f594,plain,(
  toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | spl22_52),
  inference(avatar_component_clause,[],[f592])).
tff(f1373,plain,(
  spl22_2 | ~spl22_1 | ~spl22_24),
  inference(avatar_split_clause,[],[f1372,f453,f221,f226])).
tff(f221,plain,(
  spl22_1 <=> w1 = '$local_world'),
  introduced(avatar_definition,[new_symbols(naming,[spl22_1])])).
tff(f453,plain,(
  spl22_24 <=> '$in_world'(w1,$false)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_24])])).
tff(f1372,plain,(
  '$in_world'('$local_world',$false) | (~spl22_1 | ~spl22_24)),
  inference(forward_demodulation,[],[f455,f223])).
tff(f223,plain,(
  w1 = '$local_world' | ~spl22_1),
  inference(avatar_component_clause,[],[f221])).
tff(f455,plain,(
  '$in_world'(w1,$false) | ~spl22_24),
  inference(avatar_component_clause,[],[f453])).
tff(f1363,plain,(
  spl22_107 | ~spl22_2 | ~spl22_82),
  inference(avatar_split_clause,[],[f1290,f907,f226,f1325])).
tff(f1325,plain,(
  spl22_107 <=> ! [X2 : '$world'] : '$necessary'(X2,$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_107])])).
tff(f907,plain,(
  spl22_82 <=> ! [X0 : '$world'] : ('$local_world' = sK18(X0,$true) | '$necessary'(X0,$true))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_82])])).
tff(f1290,plain,(
  ( ! [X1 : '$world'] : (~'$in_world'('$local_world',$false) | '$necessary'(X1,$true)) ) | ~spl22_82),
  inference(duplicate_literal_removal,[],[f1286])).
tff(f1286,plain,(
  ( ! [X1 : '$world'] : (~'$in_world'('$local_world',$false) | '$necessary'(X1,$true) | '$necessary'(X1,$true)) ) | ~spl22_82),
  inference(superposition,[],[f202,f908])).
tff(f908,plain,(
  ( ! [X0 : '$world'] : ('$local_world' = sK18(X0,$true) | '$necessary'(X0,$true)) ) | ~spl22_82),
  inference(avatar_component_clause,[],[f907])).
tff(f202,plain,(
  ( ! [X0 : '$world'] : (~'$in_world'(sK18(X0,$true),$false) | '$necessary'(X0,$true)) )),
  inference(cnf_transformation,[],[f47])).
tff(f47,plain,(
  ! [X0 : '$world',X1 : $o] : ('$necessary'(X0,X1) <=> ! [X2 : '$world'] : (? [X3 : $o] : ((X1 | ~X3) & '$in_world'(X2,X3)) | ~'$accessible_world'(X0,X2)))),
  inference(ennf_transformation,[],[f42])).
tff(f42,plain,(
  ! [X0 : '$world',X1 : $o] : ('$necessary'(X0,X1) <=> ! [X2 : '$world'] : ('$accessible_world'(X0,X2) => ? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3))))),
  inference(rectify,[],[f37])).
tff(f37,plain,(
  ! [X0 : '$world',X1 : $o] : ('$necessary'(X0,X1) <=> ! [X2 : '$world'] : ('$accessible_world'(X0,X2) => ? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3))))),
  inference(theory_normalization,[],[f10])).
tff(f10,plain,(
  ! [X0 : '$world',X1 : $o] : ('$necessary'(X0,X1) <=> ! [X2 : '$world'] : ('$accessible_world'(X0,X2) => ? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3))))),
  inference(theory_normalization,[],[f1])).
tff(f1,axiom,(
  ! [X0 : '$world',X1 : $o] : ('$necessary'(X0,X1) <=> ! [X2 : '$world'] : ('$accessible_world'(X0,X2) => ? [X3 : $o] : ((X3 => X1) & '$in_world'(X2,X3))))),
  file('NTF_Finite-Infinite.s.p',necessary_defn)).
tff(f1361,plain,(
  spl22_4 | ~spl22_107),
  inference(avatar_contradiction_clause,[],[f1356])).
tff(f1356,plain,(
  $false | (spl22_4 | ~spl22_107)),
  inference(resolution,[],[f1326,f242])).
tff(f242,plain,(
  ~'$necessary'('$local_world',$true) | spl22_4),
  inference(avatar_component_clause,[],[f241])).
tff(f1326,plain,(
  ( ! [X2 : '$world'] : ('$necessary'(X2,$true)) ) | ~spl22_107),
  inference(avatar_component_clause,[],[f1325])).
tff(f1360,plain,(
  spl22_77 | ~spl22_107),
  inference(avatar_contradiction_clause,[],[f1357])).
tff(f1357,plain,(
  $false | (spl22_77 | ~spl22_107)),
  inference(resolution,[],[f1326,f814])).
tff(f814,plain,(
  ~'$necessary'(w2,$true) | spl22_77),
  inference(avatar_component_clause,[],[f813])).
tff(f813,plain,(
  spl22_77 <=> '$necessary'(w2,$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_77])])).
tff(f1329,plain,(
  spl22_6 | ~spl22_1 | ~spl22_39),
  inference(avatar_split_clause,[],[f1328,f521,f221,f248])).
tff(f248,plain,(
  spl22_6 <=> '$in_world'('$local_world',$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_6])])).
tff(f521,plain,(
  spl22_39 <=> '$in_world'(w1,$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_39])])).
tff(f1328,plain,(
  '$in_world'('$local_world',$true) | (~spl22_1 | ~spl22_39)),
  inference(forward_demodulation,[],[f523,f223])).
tff(f523,plain,(
  '$in_world'(w1,$true) | ~spl22_39),
  inference(avatar_component_clause,[],[f521])).
tff(f1327,plain,(
  spl22_107 | ~spl22_6 | ~spl22_82),
  inference(avatar_split_clause,[],[f1289,f907,f248,f1325])).
tff(f1289,plain,(
  ( ! [X2 : '$world'] : (~'$in_world'('$local_world',$true) | '$necessary'(X2,$true)) ) | ~spl22_82),
  inference(duplicate_literal_removal,[],[f1287])).
tff(f1287,plain,(
  ( ! [X2 : '$world'] : (~'$in_world'('$local_world',$true) | '$necessary'(X2,$true) | '$necessary'(X2,$true)) ) | ~spl22_82),
  inference(superposition,[],[f199,f908])).
tff(f199,plain,(
  ( ! [X0 : '$world'] : (~'$in_world'(sK18(X0,$true),$true) | '$necessary'(X0,$true)) )),
  inference(cnf_transformation,[],[f47])).
tff(f1322,plain,(
  spl22_47 | ~spl22_41 | spl22_40 | ~spl22_35 | ~spl22_46),
  inference(avatar_split_clause,[],[f1321,f550,f504,f525,f529,f556])).
tff(f556,plain,(
  spl22_47 <=> $less(sK10,2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_47])])).
tff(f529,plain,(
  spl22_41 <=> all_heads(int2sequence($quotient_e(sK10,2)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_41])])).
tff(f525,plain,(
  spl22_40 <=> all_heads(int2sequence(sK10))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_40])])).
tff(f550,plain,(
  spl22_46 <=> 0 = $remainder_e(sK10,2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_46])])).
tff(f1321,plain,(
  all_heads(int2sequence(sK10)) | ~all_heads(int2sequence($quotient_e(sK10,2))) | $less(sK10,2) | (~spl22_35 | ~spl22_46)),
  inference(trivial_inequality_removal,[],[f1320])).
tff(f1320,plain,(
  0 != 0 | all_heads(int2sequence(sK10)) | ~all_heads(int2sequence($quotient_e(sK10,2))) | $less(sK10,2) | (~spl22_35 | ~spl22_46)),
  inference(superposition,[],[f505,f552])).
tff(f552,plain,(
  0 = $remainder_e(sK10,2) | ~spl22_46),
  inference(avatar_component_clause,[],[f550])).
tff(f1304,plain,(
  spl22_44 | ~spl22_33 | ~spl22_48),
  inference(avatar_split_clause,[],[f1303,f564,f495,f541])).
tff(f541,plain,(
  spl22_44 <=> sK7 = sK8),
  introduced(avatar_definition,[new_symbols(naming,[spl22_44])])).
tff(f495,plain,(
  spl22_33 <=> ! [X9 : $int,X8 : $int] : (int2sequence(X8) != int2sequence(X9) | X8 = X9)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_33])])).
tff(f564,plain,(
  spl22_48 <=> int2sequence(sK7) = int2sequence(sK8)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_48])])).
tff(f1303,plain,(
  sK7 = sK8 | (~spl22_33 | ~spl22_48)),
  inference(equality_resolution,[],[f923])).
tff(f923,plain,(
  ( ! [X0 : $int] : (int2sequence(X0) != int2sequence(sK7) | sK8 = X0) ) | (~spl22_33 | ~spl22_48)),
  inference(superposition,[],[f496,f566])).
tff(f566,plain,(
  int2sequence(sK7) = int2sequence(sK8) | ~spl22_48),
  inference(avatar_component_clause,[],[f564])).
tff(f496,plain,(
  ( ! [X8 : $int,X9 : $int] : (int2sequence(X8) != int2sequence(X9) | X8 = X9) ) | ~spl22_33),
  inference(avatar_component_clause,[],[f495])).
tff(f1298,plain,(
  spl22_59 | ~spl22_33 | ~spl22_54),
  inference(avatar_split_clause,[],[f1297,f600,f495,f635])).
tff(f635,plain,(
  spl22_59 <=> sK12 = sK13),
  introduced(avatar_definition,[new_symbols(naming,[spl22_59])])).
tff(f600,plain,(
  spl22_54 <=> int2sequence(sK12) = int2sequence(sK13)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_54])])).
tff(f1297,plain,(
  sK12 = sK13 | (~spl22_33 | ~spl22_54)),
  inference(equality_resolution,[],[f919])).
tff(f919,plain,(
  ( ! [X0 : $int] : (int2sequence(X0) != int2sequence(sK12) | sK13 = X0) ) | (~spl22_33 | ~spl22_54)),
  inference(superposition,[],[f496,f602])).
tff(f602,plain,(
  int2sequence(sK12) = int2sequence(sK13) | ~spl22_54),
  inference(avatar_component_clause,[],[f600])).
tff(f1207,plain,(
  ~spl22_77 | ~spl22_72),
  inference(avatar_split_clause,[],[f841,f763,f813])).
tff(f763,plain,(
  spl22_72 <=> '$possible'(w2,$false)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_72])])).
tff(f841,plain,(
  ~'$necessary'(w2,$true) | ~spl22_72),
  inference(resolution,[],[f764,f195])).
tff(f764,plain,(
  '$possible'(w2,$false) | ~spl22_72),
  inference(avatar_component_clause,[],[f763])).
tff(f1204,plain,(
  ~spl22_33 | ~spl22_43 | ~spl22_53),
  inference(avatar_contradiction_clause,[],[f1203])).
tff(f1203,plain,(
  $false | (~spl22_33 | ~spl22_43 | ~spl22_53)),
  inference(evaluation,[],[f1202])).
tff(f1202,plain,(
  2 = 3 | (~spl22_33 | ~spl22_43 | ~spl22_53)),
  inference(trivial_inequality_removal,[],[f1197])).
tff(f1197,plain,(
  toss(null) != toss(null) | 2 = 3 | (~spl22_33 | ~spl22_43 | ~spl22_53)),
  inference(superposition,[],[f858,f597])).
tff(f597,plain,(
  int2sequence(3) = toss(null) | ~spl22_53),
  inference(avatar_component_clause,[],[f596])).
tff(f596,plain,(
  spl22_53 <=> int2sequence(3) = toss(null)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_53])])).
tff(f858,plain,(
  ( ! [X1 : $int] : (int2sequence(X1) != toss(null) | 2 = X1) ) | (~spl22_33 | ~spl22_43)),
  inference(superposition,[],[f496,f538])).
tff(f538,plain,(
  int2sequence(2) = toss(null) | ~spl22_43),
  inference(avatar_component_clause,[],[f537])).
tff(f537,plain,(
  spl22_43 <=> int2sequence(2) = toss(null)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_43])])).
tff(f1184,plain,(
  spl22_72 | ~spl22_21 | ~spl22_30),
  inference(avatar_split_clause,[],[f1178,f480,f438,f763])).
tff(f438,plain,(
  spl22_21 <=> '$accessible_world'(w2,w2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_21])])).
tff(f480,plain,(
  spl22_30 <=> '$in_world'(w2,$false)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_30])])).
tff(f1178,plain,(
  '$possible'(w2,$false) | (~spl22_21 | ~spl22_30)),
  inference(resolution,[],[f1147,f440])).
tff(f440,plain,(
  '$accessible_world'(w2,w2) | ~spl22_21),
  inference(avatar_component_clause,[],[f438])).
tff(f1147,plain,(
  ( ! [X1 : '$world'] : (~'$accessible_world'(X1,w2) | '$possible'(X1,$false)) ) | ~spl22_30),
  inference(resolution,[],[f482,f212])).
tff(f482,plain,(
  '$in_world'(w2,$false) | ~spl22_30),
  inference(avatar_component_clause,[],[f480])).
tff(f936,plain,(
  ~spl22_30 | spl22_82 | ~spl22_1),
  inference(avatar_split_clause,[],[f935,f221,f907,f480])).
tff(f935,plain,(
  ( ! [X0 : '$world'] : ('$local_world' = sK18(X0,$true) | ~'$in_world'(w2,$false) | '$necessary'(X0,$true)) ) | ~spl22_1),
  inference(forward_demodulation,[],[f845,f223])).
tff(f845,plain,(
  ( ! [X0 : '$world'] : (~'$in_world'(w2,$false) | '$necessary'(X0,$true) | w1 = sK18(X0,$true)) )),
  inference(superposition,[],[f202,f184])).
tff(f184,plain,(
  ( ! [X12 : '$world'] : (w2 = X12 | w1 = X12) )),
  inference(cnf_transformation,[],[f45])).
tff(f45,plain,(
  '$in_world'(w2,! [X0 : $int] : (all_heads(int2sequence(X0)) <=> (all_heads(int2sequence($quotient_e(X0,2))) & 0 = $remainder_e(X0,2) & ~$less(X0,2))) & all_heads(int2sequence(1)) & ! [X1 : $int] : (toss(int2sequence(X1)) = int2sequence($product(X1,2)) | 1 = X1) & toss(int2sequence(1)) = int2sequence(3) & null = int2sequence(1) & ! [X2 : $int,X3 : $int] : (X2 = X3 | int2sequence(X2) != int2sequence(X3)) & ! [X4 : sequence] : ? [X5 : $int] : int2sequence(X5) = X4) & '$in_world'(w1,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & ~$less(X6,2))) & all_heads(int2sequence(1)) & ! [X7 : $int] : toss(int2sequence(X7)) = int2sequence($product(X7,2)) & toss(int2sequence(1)) = int2sequence(2) & null = int2sequence(1) & ! [X8 : $int,X9 : $int] : (X8 = X9 | int2sequence(X8) != int2sequence(X9)) & ! [X10 : sequence] : ? [X11 : $int] : int2sequence(X11) = X10) & '$accessible_world'(w1,w2) & '$accessible_world'(w2,w2) & '$accessible_world'(w1,w1) & w1 = '$local_world' & w1 != w2 & ! [X12 : '$world'] : (w2 = X12 | w1 = X12)),
  inference(ennf_transformation,[],[f40])).
tff(f40,plain,(
  '$in_world'(w2,! [X0 : $int] : (all_heads(int2sequence(X0)) <=> (all_heads(int2sequence($quotient_e(X0,2))) & 0 = $remainder_e(X0,2) & ~$less(X0,2))) & all_heads(int2sequence(1)) & ! [X1 : $int] : (1 != X1 => toss(int2sequence(X1)) = int2sequence($product(X1,2))) & toss(int2sequence(1)) = int2sequence(3) & null = int2sequence(1) & ! [X2 : $int,X3 : $int] : (int2sequence(X2) = int2sequence(X3) => X2 = X3) & ! [X4 : sequence] : ? [X5 : $int] : int2sequence(X5) = X4) & '$in_world'(w1,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & ~$less(X6,2))) & all_heads(int2sequence(1)) & ! [X7 : $int] : toss(int2sequence(X7)) = int2sequence($product(X7,2)) & toss(int2sequence(1)) = int2sequence(2) & null = int2sequence(1) & ! [X8 : $int,X9 : $int] : (int2sequence(X8) = int2sequence(X9) => X8 = X9) & ! [X10 : sequence] : ? [X11 : $int] : int2sequence(X11) = X10) & '$accessible_world'(w1,w2) & '$accessible_world'(w2,w2) & '$accessible_world'(w1,w1) & w1 = '$local_world' & w1 != w2 & ! [X12 : '$world'] : (w2 = X12 | w1 = X12)),
  inference(rectify,[],[f8])).
tff(f8,plain,(
  '$in_world'(w2,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & ~$less(X6,2))) & all_heads(int2sequence(1)) & ! [X6 : $int] : (1 != X6 => toss(int2sequence(X6)) = int2sequence($product(X6,2))) & toss(int2sequence(1)) = int2sequence(3) & null = int2sequence(1) & ! [X7 : $int,X8 : $int] : (int2sequence(X7) = int2sequence(X8) => X7 = X8) & ! [X5 : sequence] : ? [X6 : $int] : int2sequence(X6) = X5) & '$in_world'(w1,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & ~$less(X6,2))) & all_heads(int2sequence(1)) & ! [X6 : $int] : toss(int2sequence(X6)) = int2sequence($product(X6,2)) & toss(int2sequence(1)) = int2sequence(2) & null = int2sequence(1) & ! [X7 : $int,X8 : $int] : (int2sequence(X7) = int2sequence(X8) => X7 = X8) & ! [X5 : sequence] : ? [X6 : $int] : int2sequence(X6) = X5) & '$accessible_world'(w1,w2) & '$accessible_world'(w2,w2) & '$accessible_world'(w1,w1) & w1 = '$local_world' & w1 != w2 & ! [X4 : '$world'] : (w2 = X4 | w1 = X4)),
  inference(theory_normalization,[],[f4])).
tff(f4,axiom,(
  '$in_world'(w2,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & $greatereq(X6,2))) & all_heads(int2sequence(1)) & ! [X6 : $int] : (1 != X6 => toss(int2sequence(X6)) = int2sequence($product(X6,2))) & toss(int2sequence(1)) = int2sequence(3) & null = int2sequence(1) & ! [X7 : $int,X8 : $int] : (int2sequence(X7) = int2sequence(X8) => X7 = X8) & ! [X5 : sequence] : ? [X6 : $int] : int2sequence(X6) = X5) & '$in_world'(w1,! [X6 : $int] : (all_heads(int2sequence(X6)) <=> (all_heads(int2sequence($quotient_e(X6,2))) & $remainder_e(X6,2) = 0 & $greatereq(X6,2))) & all_heads(int2sequence(1)) & ! [X6 : $int] : toss(int2sequence(X6)) = int2sequence($product(X6,2)) & toss(int2sequence(1)) = int2sequence(2) & null = int2sequence(1) & ! [X7 : $int,X8 : $int] : (int2sequence(X7) = int2sequence(X8) => X7 = X8) & ! [X5 : sequence] : ? [X6 : $int] : int2sequence(X6) = X5) & '$accessible_world'(w1,w2) & '$accessible_world'(w2,w2) & '$accessible_world'(w1,w1) & w1 = '$local_world' & w1 != w2 & ! [X4 : '$world'] : (w2 = X4 | w1 = X4)),
  file('NTF_Finite-Infinite.s.p',tossed_worlds)).
tff(f922,plain,(
  ~spl22_29 | ~spl22_45),
  inference(avatar_contradiction_clause,[],[f921])).
tff(f921,plain,(
  $false | (~spl22_29 | ~spl22_45)),
  inference(equality_resolution,[],[f889])).
tff(f889,plain,(
  ( ! [X1 : sequence] : (sK6 != X1) ) | (~spl22_29 | ~spl22_45)),
  inference(superposition,[],[f546,f477])).
tff(f477,plain,(
  ( ! [X10 : sequence] : (int2sequence(sK16(X10)) = X10) ) | ~spl22_29),
  inference(avatar_component_clause,[],[f476])).
tff(f476,plain,(
  spl22_29 <=> ! [X10 : sequence] : int2sequence(sK16(X10)) = X10),
  introduced(avatar_definition,[new_symbols(naming,[spl22_29])])).
tff(f546,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6) ) | ~spl22_45),
  inference(avatar_component_clause,[],[f545])).
tff(f545,plain,(
  spl22_45 <=> ! [X11 : $int] : int2sequence(X11) != sK6),
  introduced(avatar_definition,[new_symbols(naming,[spl22_45])])).
tff(f914,plain,(
  ~spl22_50 | ~spl22_38 | ~spl22_57),
  inference(avatar_split_clause,[],[f836,f615,f516,f584])).
tff(f516,plain,(
  spl22_38 <=> ! [X6 : $int] : (~$less(X6,2) | ~all_heads(int2sequence(X6)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_38])])).
tff(f836,plain,(
  ~all_heads(int2sequence(sK15)) | (~spl22_38 | ~spl22_57)),
  inference(resolution,[],[f517,f616])).
tff(f616,plain,(
  $less(sK15,2) | ~spl22_57),
  inference(avatar_component_clause,[],[f615])).
tff(f517,plain,(
  ( ! [X6 : $int] : (~$less(X6,2) | ~all_heads(int2sequence(X6))) ) | ~spl22_38),
  inference(avatar_component_clause,[],[f516])).
tff(f913,plain,(
  ~spl22_50 | ~spl22_36 | spl22_51),
  inference(avatar_split_clause,[],[f871,f588,f508,f584])).
tff(f508,plain,(
  spl22_36 <=> ! [X6 : $int] : (all_heads(int2sequence($quotient_e(X6,2))) | ~all_heads(int2sequence(X6)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_36])])).
tff(f871,plain,(
  ~all_heads(int2sequence(sK15)) | (~spl22_36 | spl22_51)),
  inference(resolution,[],[f509,f589])).
tff(f589,plain,(
  ~all_heads(int2sequence($quotient_e(sK15,2))) | spl22_51),
  inference(avatar_component_clause,[],[f588])).
tff(f509,plain,(
  ( ! [X6 : $int] : (all_heads(int2sequence($quotient_e(X6,2))) | ~all_heads(int2sequence(X6))) ) | ~spl22_36),
  inference(avatar_component_clause,[],[f508])).
tff(f912,plain,(
  ~spl22_50 | ~spl22_37 | spl22_56),
  inference(avatar_split_clause,[],[f876,f609,f512,f584])).
tff(f512,plain,(
  spl22_37 <=> ! [X6 : $int] : ($remainder_e(X6,2) = 0 | ~all_heads(int2sequence(X6)))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_37])])).
tff(f876,plain,(
  ~all_heads(int2sequence(sK15)) | (~spl22_37 | spl22_56)),
  inference(trivial_inequality_removal,[],[f875])).
tff(f875,plain,(
  0 != 0 | ~all_heads(int2sequence(sK15)) | (~spl22_37 | spl22_56)),
  inference(superposition,[],[f610,f513])).
tff(f513,plain,(
  ( ! [X6 : $int] : ($remainder_e(X6,2) = 0 | ~all_heads(int2sequence(X6))) ) | ~spl22_37),
  inference(avatar_component_clause,[],[f512])).
tff(f610,plain,(
  0 != $remainder_e(sK15,2) | spl22_56),
  inference(avatar_component_clause,[],[f609])).
tff(f909,plain,(
  ~spl22_49 | spl22_82 | ~spl22_1),
  inference(avatar_split_clause,[],[f905,f221,f907,f580])).
tff(f580,plain,(
  spl22_49 <=> '$in_world'(w2,$true)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_49])])).
tff(f905,plain,(
  ( ! [X0 : '$world'] : ('$local_world' = sK18(X0,$true) | ~'$in_world'(w2,$true) | '$necessary'(X0,$true)) ) | ~spl22_1),
  inference(forward_demodulation,[],[f837,f223])).
tff(f837,plain,(
  ( ! [X0 : '$world'] : (~'$in_world'(w2,$true) | '$necessary'(X0,$true) | w1 = sK18(X0,$true)) )),
  inference(superposition,[],[f199,f184])).
tff(f884,plain,(
  ~spl22_40 | ~spl22_38 | ~spl22_47),
  inference(avatar_split_clause,[],[f835,f556,f516,f525])).
tff(f835,plain,(
  ~all_heads(int2sequence(sK10)) | (~spl22_38 | ~spl22_47)),
  inference(resolution,[],[f517,f557])).
tff(f557,plain,(
  $less(sK10,2) | ~spl22_47),
  inference(avatar_component_clause,[],[f556])).
tff(f883,plain,(
  ~spl22_40 | ~spl22_36 | spl22_41),
  inference(avatar_split_clause,[],[f870,f529,f508,f525])).
tff(f870,plain,(
  ~all_heads(int2sequence(sK10)) | (~spl22_36 | spl22_41)),
  inference(resolution,[],[f509,f530])).
tff(f530,plain,(
  ~all_heads(int2sequence($quotient_e(sK10,2))) | spl22_41),
  inference(avatar_component_clause,[],[f529])).
tff(f882,plain,(
  ~spl22_40 | ~spl22_37 | spl22_46),
  inference(avatar_split_clause,[],[f877,f550,f512,f525])).
tff(f877,plain,(
  ~all_heads(int2sequence(sK10)) | (~spl22_37 | spl22_46)),
  inference(trivial_inequality_removal,[],[f874])).
tff(f874,plain,(
  0 != 0 | ~all_heads(int2sequence(sK10)) | (~spl22_37 | spl22_46)),
  inference(superposition,[],[f551,f513])).
tff(f551,plain,(
  0 != $remainder_e(sK10,2) | spl22_46),
  inference(avatar_component_clause,[],[f550])).
tff(f880,plain,(
  ~spl22_26 | spl22_42),
  inference(avatar_contradiction_clause,[],[f879])).
tff(f879,plain,(
  $false | (~spl22_26 | spl22_42)),
  inference(trivial_inequality_removal,[],[f878])).
tff(f878,plain,(
  toss(int2sequence(sK9)) != toss(int2sequence(sK9)) | (~spl22_26 | spl22_42)),
  inference(superposition,[],[f535,f463])).
tff(f463,plain,(
  ( ! [X7 : $int] : (toss(int2sequence(X7)) = int2sequence($product(X7,2))) ) | ~spl22_26),
  inference(avatar_component_clause,[],[f462])).
tff(f462,plain,(
  spl22_26 <=> ! [X7 : $int] : toss(int2sequence(X7)) = int2sequence($product(X7,2))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_26])])).
tff(f535,plain,(
  toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | spl22_42),
  inference(avatar_component_clause,[],[f533])).
tff(f533,plain,(
  spl22_42 <=> toss(int2sequence(sK9)) = int2sequence($product(sK9,2))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_42])])).
tff(f769,plain,(
  null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | int2sequence(3) = toss(null)),
  introduced(theory_tautology_sat_conflict,[])).
tff(f670,plain,(
  spl22_61 | ~spl22_1 | ~spl22_22),
  inference(avatar_split_clause,[],[f665,f443,f221,f667])).
tff(f443,plain,(
  spl22_22 <=> '$accessible_world'(w1,w1)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_22])])).
tff(f665,plain,(
  '$accessible_world'('$local_world','$local_world') | (~spl22_1 | ~spl22_22)),
  inference(superposition,[],[f445,f223])).
tff(f445,plain,(
  '$accessible_world'(w1,w1) | ~spl22_22),
  inference(avatar_component_clause,[],[f443])).
tff(f658,plain,(
  spl22_10 | ~spl22_25 | ~spl22_28),
  inference(avatar_split_clause,[],[f657,f471,f457,f267])).
tff(f267,plain,(
  spl22_10 <=> all_heads(null)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_10])])).
tff(f457,plain,(
  spl22_25 <=> all_heads(int2sequence(1))),
  introduced(avatar_definition,[new_symbols(naming,[spl22_25])])).
tff(f471,plain,(
  spl22_28 <=> null = int2sequence(1)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_28])])).
tff(f657,plain,(
  all_heads(null) | (~spl22_25 | ~spl22_28)),
  inference(forward_demodulation,[],[f459,f473])).
tff(f473,plain,(
  null = int2sequence(1) | ~spl22_28),
  inference(avatar_component_clause,[],[f471])).
tff(f459,plain,(
  all_heads(int2sequence(1)) | ~spl22_25),
  inference(avatar_component_clause,[],[f457])).
tff(f655,plain,(
  null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | int2sequence(2) = toss(null)),
  introduced(theory_tautology_sat_conflict,[])).
tff(f652,plain,(
  spl22_49 | ~spl22_50 | ~spl22_51 | ~spl22_56 | spl22_57 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f651,f604,f635,f471,f596,f623,f267,f615,f609,f588,f584,f580])).
tff(f651,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f140])).
tff(f140,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f650,plain,(
  spl22_49 | spl22_50 | ~spl22_57 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f649,f604,f635,f471,f596,f623,f267,f615,f584,f580])).
tff(f649,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f141])).
tff(f141,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f648,plain,(
  spl22_49 | spl22_50 | spl22_56 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f647,f604,f635,f471,f596,f623,f267,f609,f584,f580])).
tff(f647,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f142])).
tff(f142,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f646,plain,(
  spl22_49 | spl22_50 | spl22_51 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f645,f604,f635,f471,f596,f623,f267,f588,f584,f580])).
tff(f645,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f143])).
tff(f143,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f644,plain,(
  spl22_49 | ~spl22_50 | ~spl22_51 | ~spl22_56 | spl22_57 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f643,f604,f635,f471,f596,f592,f267,f615,f609,f588,f584,f580])).
tff(f643,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f144])).
tff(f144,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f642,plain,(
  spl22_49 | spl22_50 | ~spl22_57 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f641,f604,f635,f471,f596,f592,f267,f615,f584,f580])).
tff(f641,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f145])).
tff(f145,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f640,plain,(
  spl22_49 | spl22_50 | spl22_56 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f639,f604,f635,f471,f596,f592,f267,f609,f584,f580])).
tff(f639,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f146])).
tff(f146,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f638,plain,(
  spl22_49 | spl22_50 | spl22_51 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | ~spl22_59 | spl22_55),
  inference(avatar_split_clause,[],[f633,f604,f635,f471,f596,f592,f267,f588,f584,f580])).
tff(f633,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f147])).
tff(f147,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | sK12 != sK13 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f632,plain,(
  spl22_49 | ~spl22_50 | ~spl22_51 | ~spl22_56 | spl22_57 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f631,f604,f600,f471,f596,f623,f267,f615,f609,f588,f584,f580])).
tff(f631,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f148])).
tff(f148,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f630,plain,(
  spl22_49 | spl22_50 | ~spl22_57 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f629,f604,f600,f471,f596,f623,f267,f615,f584,f580])).
tff(f629,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f149])).
tff(f149,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f628,plain,(
  spl22_49 | spl22_50 | spl22_56 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f627,f604,f600,f471,f596,f623,f267,f609,f584,f580])).
tff(f627,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f150])).
tff(f150,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f626,plain,(
  spl22_49 | spl22_50 | spl22_51 | ~spl22_10 | ~spl22_58 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f621,f604,f600,f471,f596,f623,f267,f588,f584,f580])).
tff(f621,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | 1 != sK14 | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f151])).
tff(f151,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | 1 != sK14 | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f620,plain,(
  spl22_49 | ~spl22_50 | ~spl22_51 | ~spl22_56 | spl22_57 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f619,f604,f600,f471,f596,f592,f267,f615,f609,f588,f584,f580])).
tff(f619,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f152])).
tff(f152,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | $less(sK15,2) | 0 != $remainder_e(sK15,2) | ~all_heads(int2sequence($quotient_e(sK15,2))) | ~all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f618,plain,(
  spl22_49 | spl22_50 | ~spl22_57 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f613,f604,f600,f471,f596,f592,f267,f615,f584,f580])).
tff(f613,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f153])).
tff(f153,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | ~$less(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f612,plain,(
  spl22_49 | spl22_50 | spl22_56 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f607,f604,f600,f471,f596,f592,f267,f609,f584,f580])).
tff(f607,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f154])).
tff(f154,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK15,2) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f606,plain,(
  spl22_49 | spl22_50 | spl22_51 | ~spl22_10 | ~spl22_52 | ~spl22_53 | ~spl22_28 | spl22_54 | spl22_55),
  inference(avatar_split_clause,[],[f578,f604,f600,f471,f596,f592,f267,f588,f584,f580])).
tff(f578,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | int2sequence(3) != toss(null) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(inner_rewriting,[],[f155])).
tff(f155,plain,(
  ( ! [X5 : $int] : (int2sequence(X5) != sK11 | int2sequence(sK12) = int2sequence(sK13) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(3) | toss(int2sequence(sK14)) != int2sequence($product(sK14,2)) | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK15,2))) | all_heads(int2sequence(sK15)) | '$in_world'(w2,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f577,plain,(
  spl22_30 | spl22_38),
  inference(avatar_split_clause,[],[f156,f516,f480])).
tff(f156,plain,(
  ( ! [X0 : $int] : (~$less(X0,2) | ~all_heads(int2sequence(X0)) | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f576,plain,(
  spl22_30 | spl22_37),
  inference(avatar_split_clause,[],[f157,f512,f480])).
tff(f157,plain,(
  ( ! [X0 : $int] : (0 = $remainder_e(X0,2) | ~all_heads(int2sequence(X0)) | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f575,plain,(
  spl22_30 | spl22_36),
  inference(avatar_split_clause,[],[f158,f508,f480])).
tff(f158,plain,(
  ( ! [X0 : $int] : (all_heads(int2sequence($quotient_e(X0,2))) | ~all_heads(int2sequence(X0)) | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f574,plain,(
  spl22_30 | spl22_35),
  inference(avatar_split_clause,[],[f159,f504,f480])).
tff(f159,plain,(
  ( ! [X0 : $int] : ($less(X0,2) | 0 != $remainder_e(X0,2) | ~all_heads(int2sequence($quotient_e(X0,2))) | all_heads(int2sequence(X0)) | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f573,plain,(
  spl22_39 | ~spl22_40 | ~spl22_41 | ~spl22_46 | spl22_47 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | spl22_48 | spl22_45),
  inference(avatar_split_clause,[],[f572,f545,f564,f471,f537,f533,f267,f556,f550,f529,f525,f521])).
tff(f572,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | $less(sK10,2) | 0 != $remainder_e(sK10,2) | ~all_heads(int2sequence($quotient_e(sK10,2))) | ~all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f160])).
tff(f160,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | $less(sK10,2) | 0 != $remainder_e(sK10,2) | ~all_heads(int2sequence($quotient_e(sK10,2))) | ~all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f571,plain,(
  spl22_39 | spl22_40 | ~spl22_47 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | spl22_48 | spl22_45),
  inference(avatar_split_clause,[],[f570,f545,f564,f471,f537,f533,f267,f556,f525,f521])).
tff(f570,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | ~$less(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f161])).
tff(f161,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | ~$less(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f569,plain,(
  spl22_39 | spl22_40 | spl22_46 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | spl22_48 | spl22_45),
  inference(avatar_split_clause,[],[f568,f545,f564,f471,f537,f533,f267,f550,f525,f521])).
tff(f568,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | 0 = $remainder_e(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f162])).
tff(f162,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f567,plain,(
  spl22_39 | spl22_40 | spl22_41 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | spl22_48 | spl22_45),
  inference(avatar_split_clause,[],[f562,f545,f564,f471,f537,f533,f267,f529,f525,f521])).
tff(f562,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK10,2))) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f163])).
tff(f163,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | int2sequence(sK7) = int2sequence(sK8) | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK10,2))) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f561,plain,(
  spl22_39 | ~spl22_40 | ~spl22_41 | ~spl22_46 | spl22_47 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | ~spl22_44 | spl22_45),
  inference(avatar_split_clause,[],[f560,f545,f541,f471,f537,f533,f267,f556,f550,f529,f525,f521])).
tff(f560,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | $less(sK10,2) | 0 != $remainder_e(sK10,2) | ~all_heads(int2sequence($quotient_e(sK10,2))) | ~all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f164])).
tff(f164,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | $less(sK10,2) | 0 != $remainder_e(sK10,2) | ~all_heads(int2sequence($quotient_e(sK10,2))) | ~all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f559,plain,(
  spl22_39 | spl22_40 | ~spl22_47 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | ~spl22_44 | spl22_45),
  inference(avatar_split_clause,[],[f554,f545,f541,f471,f537,f533,f267,f556,f525,f521])).
tff(f554,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | ~$less(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f165])).
tff(f165,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | ~$less(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f553,plain,(
  spl22_39 | spl22_40 | spl22_46 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | ~spl22_44 | spl22_45),
  inference(avatar_split_clause,[],[f548,f545,f541,f471,f537,f533,f267,f550,f525,f521])).
tff(f548,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | 0 = $remainder_e(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f166])).
tff(f166,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | 0 = $remainder_e(sK10,2) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f547,plain,(
  spl22_39 | spl22_40 | spl22_41 | ~spl22_10 | ~spl22_42 | ~spl22_43 | ~spl22_28 | ~spl22_44 | spl22_45),
  inference(avatar_split_clause,[],[f519,f545,f541,f471,f537,f533,f267,f529,f525,f521])).
tff(f519,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | int2sequence(2) != toss(null) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(null) | all_heads(int2sequence($quotient_e(sK10,2))) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(inner_rewriting,[],[f167])).
tff(f167,plain,(
  ( ! [X11 : $int] : (int2sequence(X11) != sK6 | sK7 != sK8 | null != int2sequence(1) | toss(int2sequence(1)) != int2sequence(2) | toss(int2sequence(sK9)) != int2sequence($product(sK9,2)) | ~all_heads(int2sequence(1)) | all_heads(int2sequence($quotient_e(sK10,2))) | all_heads(int2sequence(sK10)) | '$in_world'(w1,$true)) )),
  inference(cnf_transformation,[],[f45])).
tff(f518,plain,(
  spl22_24 | spl22_38),
  inference(avatar_split_clause,[],[f168,f516,f453])).
tff(f168,plain,(
  ( ! [X6 : $int] : (~$less(X6,2) | ~all_heads(int2sequence(X6)) | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f514,plain,(
  spl22_24 | spl22_37),
  inference(avatar_split_clause,[],[f169,f512,f453])).
tff(f169,plain,(
  ( ! [X6 : $int] : ($remainder_e(X6,2) = 0 | ~all_heads(int2sequence(X6)) | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f510,plain,(
  spl22_24 | spl22_36),
  inference(avatar_split_clause,[],[f170,f508,f453])).
tff(f170,plain,(
  ( ! [X6 : $int] : (all_heads(int2sequence($quotient_e(X6,2))) | ~all_heads(int2sequence(X6)) | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f506,plain,(
  spl22_24 | spl22_35),
  inference(avatar_split_clause,[],[f171,f504,f453])).
tff(f171,plain,(
  ( ! [X6 : $int] : ($less(X6,2) | $remainder_e(X6,2) != 0 | ~all_heads(int2sequence($quotient_e(X6,2))) | all_heads(int2sequence(X6)) | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f502,plain,(
  spl22_30 | spl22_34),
  inference(avatar_split_clause,[],[f172,f500,f480])).
tff(f172,plain,(
  ( ! [X1 : $int] : (1 = X1 | toss(int2sequence(X1)) = int2sequence($product(X1,2)) | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f498,plain,(
  spl22_30 | spl22_33),
  inference(avatar_split_clause,[],[f173,f495,f480])).
tff(f173,plain,(
  ( ! [X2 : $int,X3 : $int] : (int2sequence(X2) != int2sequence(X3) | X2 = X3 | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f497,plain,(
  spl22_24 | spl22_33),
  inference(avatar_split_clause,[],[f174,f495,f453])).
tff(f174,plain,(
  ( ! [X8 : $int,X9 : $int] : (int2sequence(X8) != int2sequence(X9) | X8 = X9 | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f493,plain,(
  spl22_30 | spl22_32),
  inference(avatar_split_clause,[],[f175,f491,f480])).
tff(f175,plain,(
  ( ! [X4 : sequence] : (int2sequence(sK17(X4)) = X4 | '$in_world'(w2,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f489,plain,(
  spl22_30 | spl22_28),
  inference(avatar_split_clause,[],[f176,f471,f480])).
tff(f176,plain,(
  null = int2sequence(1) | '$in_world'(w2,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f488,plain,(
  spl22_30 | spl22_31),
  inference(avatar_split_clause,[],[f177,f485,f480])).
tff(f485,plain,(
  spl22_31 <=> toss(int2sequence(1)) = int2sequence(3)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_31])])).
tff(f177,plain,(
  toss(int2sequence(1)) = int2sequence(3) | '$in_world'(w2,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f483,plain,(
  spl22_30 | spl22_25),
  inference(avatar_split_clause,[],[f178,f457,f480])).
tff(f178,plain,(
  all_heads(int2sequence(1)) | '$in_world'(w2,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f478,plain,(
  spl22_24 | spl22_29),
  inference(avatar_split_clause,[],[f179,f476,f453])).
tff(f179,plain,(
  ( ! [X10 : sequence] : (int2sequence(sK16(X10)) = X10 | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f474,plain,(
  spl22_24 | spl22_28),
  inference(avatar_split_clause,[],[f180,f471,f453])).
tff(f180,plain,(
  null = int2sequence(1) | '$in_world'(w1,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f469,plain,(
  spl22_24 | spl22_27),
  inference(avatar_split_clause,[],[f181,f466,f453])).
tff(f466,plain,(
  spl22_27 <=> toss(int2sequence(1)) = int2sequence(2)),
  introduced(avatar_definition,[new_symbols(naming,[spl22_27])])).
tff(f181,plain,(
  toss(int2sequence(1)) = int2sequence(2) | '$in_world'(w1,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f464,plain,(
  spl22_24 | spl22_26),
  inference(avatar_split_clause,[],[f182,f462,f453])).
tff(f182,plain,(
  ( ! [X7 : $int] : (toss(int2sequence(X7)) = int2sequence($product(X7,2)) | '$in_world'(w1,$false)) )),
  inference(cnf_transformation,[],[f45])).
tff(f460,plain,(
  spl22_24 | spl22_25),
  inference(avatar_split_clause,[],[f183,f457,f453])).
tff(f183,plain,(
  all_heads(int2sequence(1)) | '$in_world'(w1,$false)),
  inference(cnf_transformation,[],[f45])).
tff(f446,plain,(
  spl22_22),
  inference(avatar_split_clause,[],[f187,f443])).
tff(f187,plain,(
  '$accessible_world'(w1,w1)),
  inference(cnf_transformation,[],[f45])).
tff(f441,plain,(
  spl22_21),
  inference(avatar_split_clause,[],[f188,f438])).
tff(f188,plain,(
  '$accessible_world'(w2,w2)),
  inference(cnf_transformation,[],[f45])).
tff(f224,plain,(
  spl22_1),
  inference(avatar_split_clause,[],[f186,f221])).
tff(f186,plain,(
  w1 = '$local_world'),
  inference(cnf_transformation,[],[f45])).
% SZS output end Proof for NTF_Finite-Infinite.s