%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:57:15 AM UTC 2026
% Result : Theorem 2.59s 1.09s
% Output : Refutation 3.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 9
% Syntax : Number of formulae : 85 ( 12 unt; 0 typ; 4 def)
% Number of atoms : 581 ( 0 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 768 ( 330 ~; 305 |; 62 &)
% ( 4 <=>; 67 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 58 ( 58 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 43 ( 42 usr; 5 prp; 0-3 aty)
% Number of functors : 189 ( 189 usr; 2 con; 0-3 aty)
% Number of variables : 252 ( 0 sgn 215 !; 37 ?; 252 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_6,type,
sK1: '$ki_world' > $i ).
tff(func_def_7,type,
sK2: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_8,type,
sK3: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_9,type,
sK4: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_10,type,
sK5: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_11,type,
sK6: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_12,type,
sK7: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_13,type,
sK8: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_14,type,
sK9: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_15,type,
sK10: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_16,type,
sK11: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_17,type,
sK12: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_18,type,
sK13: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_19,type,
sK14: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_20,type,
sK15: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_21,type,
sK16: '$ki_world' > $i ).
tff(func_def_22,type,
sK17: '$ki_world' > '$ki_world' ).
tff(func_def_23,type,
sK18: '$ki_world' > $i ).
tff(func_def_24,type,
sK19: '$ki_world' > '$ki_world' ).
tff(func_def_25,type,
sK20: '$ki_world' > '$ki_world' ).
tff(func_def_26,type,
sK21: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_27,type,
sK22: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_28,type,
sK23: '$ki_world' > '$ki_world' ).
tff(func_def_29,type,
sK24: '$ki_world' > '$ki_world' ).
tff(func_def_30,type,
sK25: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_31,type,
sK26: '$ki_world' > '$ki_world' ).
tff(func_def_32,type,
sK27: '$ki_world' > '$ki_world' ).
tff(func_def_33,type,
sK28: '$ki_world' > $i ).
tff(func_def_34,type,
sK29: '$ki_world' > '$ki_world' ).
tff(func_def_35,type,
sK30: '$ki_world' > $i ).
tff(func_def_36,type,
sK31: '$ki_world' > '$ki_world' ).
tff(func_def_37,type,
sK32: '$ki_world' > '$ki_world' ).
tff(func_def_38,type,
sK33: '$ki_world' > '$ki_world' ).
tff(func_def_39,type,
sK34: '$ki_world' > '$ki_world' ).
tff(func_def_40,type,
sK35: '$ki_world' > $i ).
tff(func_def_41,type,
sK36: '$ki_world' > '$ki_world' ).
tff(func_def_42,type,
sK37: '$ki_world' > $i ).
tff(func_def_43,type,
sK38: '$ki_world' > '$ki_world' ).
tff(func_def_44,type,
sK39: '$ki_world' > '$ki_world' ).
tff(func_def_45,type,
sK40: '$ki_world' > '$ki_world' ).
tff(func_def_46,type,
sK41: '$ki_world' > $i ).
tff(func_def_47,type,
sK42: '$ki_world' > '$ki_world' ).
tff(func_def_48,type,
sK43: '$ki_world' > $i ).
tff(func_def_49,type,
sK44: '$ki_world' > '$ki_world' ).
tff(func_def_50,type,
sK45: '$ki_world' > '$ki_world' ).
tff(func_def_51,type,
sK46: '$ki_world' > '$ki_world' ).
tff(func_def_52,type,
sK47: '$ki_world' > $i ).
tff(func_def_53,type,
sK48: '$ki_world' > '$ki_world' ).
tff(func_def_54,type,
sK49: '$ki_world' > $i ).
tff(func_def_55,type,
sK50: '$ki_world' > '$ki_world' ).
tff(func_def_56,type,
sK51: '$ki_world' > '$ki_world' ).
tff(func_def_57,type,
sK52: '$ki_world' > '$ki_world' ).
tff(func_def_58,type,
sK53: '$ki_world' > $i ).
tff(func_def_59,type,
sK54: '$ki_world' > '$ki_world' ).
tff(func_def_60,type,
sK55: '$ki_world' > $i ).
tff(func_def_61,type,
sK56: '$ki_world' > '$ki_world' ).
tff(func_def_62,type,
sK57: '$ki_world' > $i ).
tff(func_def_63,type,
sK58: '$ki_world' > '$ki_world' ).
tff(func_def_64,type,
sK59: '$ki_world' > '$ki_world' ).
tff(func_def_65,type,
sK60: '$ki_world' > '$ki_world' ).
tff(func_def_66,type,
sK61: '$ki_world' > $i ).
tff(func_def_67,type,
sK62: '$ki_world' > '$ki_world' ).
tff(func_def_68,type,
sK63: '$ki_world' > $i ).
tff(func_def_69,type,
sK64: '$ki_world' > '$ki_world' ).
tff(func_def_70,type,
sK65: '$ki_world' > '$ki_world' ).
tff(func_def_71,type,
sK66: '$ki_world' > '$ki_world' ).
tff(func_def_72,type,
sK67: '$ki_world' > $i ).
tff(func_def_73,type,
sK68: '$ki_world' > '$ki_world' ).
tff(func_def_74,type,
sK69: '$ki_world' > $i ).
tff(func_def_75,type,
sK70: '$ki_world' > '$ki_world' ).
tff(func_def_76,type,
sK71: '$ki_world' > '$ki_world' ).
tff(func_def_77,type,
sK72: '$ki_world' > '$ki_world' ).
tff(func_def_78,type,
sK73: '$ki_world' > $i ).
tff(func_def_79,type,
sK74: '$ki_world' > '$ki_world' ).
tff(func_def_80,type,
sK75: '$ki_world' > $i ).
tff(func_def_81,type,
sK76: '$ki_world' > '$ki_world' ).
tff(func_def_82,type,
sK77: '$ki_world' > '$ki_world' ).
tff(func_def_83,type,
sK78: '$ki_world' > '$ki_world' ).
tff(func_def_84,type,
sK79: '$ki_world' > $i ).
tff(func_def_85,type,
sK80: '$ki_world' > '$ki_world' ).
tff(func_def_86,type,
sK81: '$ki_world' > $i ).
tff(func_def_87,type,
sK82: '$ki_world' > '$ki_world' ).
tff(func_def_88,type,
sK83: '$ki_world' > '$ki_world' ).
tff(func_def_89,type,
sK84: '$ki_world' > '$ki_world' ).
tff(func_def_90,type,
sK85: '$ki_world' > $i ).
tff(func_def_91,type,
sK86: '$ki_world' > '$ki_world' ).
tff(func_def_92,type,
sK87: '$ki_world' > $i ).
tff(func_def_93,type,
sK88: '$ki_world' > '$ki_world' ).
tff(func_def_94,type,
sK89: '$ki_world' > '$ki_world' ).
tff(func_def_95,type,
sK90: '$ki_world' > '$ki_world' ).
tff(func_def_96,type,
sK91: '$ki_world' > $i ).
tff(func_def_97,type,
sK92: '$ki_world' > '$ki_world' ).
tff(func_def_98,type,
sK93: '$ki_world' > $i ).
tff(func_def_99,type,
sK94: '$ki_world' > '$ki_world' ).
tff(func_def_100,type,
sK95: '$ki_world' > $i ).
tff(func_def_101,type,
sK96: '$ki_world' > '$ki_world' ).
tff(func_def_102,type,
sK97: '$ki_world' > '$ki_world' ).
tff(func_def_103,type,
sK98: '$ki_world' > '$ki_world' ).
tff(func_def_104,type,
sK99: '$ki_world' > $i ).
tff(func_def_105,type,
sK100: '$ki_world' > '$ki_world' ).
tff(func_def_106,type,
sK101: '$ki_world' > $i ).
tff(func_def_107,type,
sK102: '$ki_world' > '$ki_world' ).
tff(func_def_108,type,
sK103: '$ki_world' > '$ki_world' ).
tff(func_def_109,type,
sK104: '$ki_world' > '$ki_world' ).
tff(func_def_110,type,
sK105: '$ki_world' > $i ).
tff(func_def_111,type,
sK106: '$ki_world' > '$ki_world' ).
tff(func_def_112,type,
sK107: '$ki_world' > $i ).
tff(func_def_113,type,
sK108: '$ki_world' > '$ki_world' ).
tff(func_def_114,type,
sK109: '$ki_world' > '$ki_world' ).
tff(func_def_115,type,
sK110: '$ki_world' > '$ki_world' ).
tff(func_def_116,type,
sK111: '$ki_world' > $i ).
tff(func_def_117,type,
sK112: '$ki_world' > '$ki_world' ).
tff(func_def_118,type,
sK113: '$ki_world' > $i ).
tff(func_def_119,type,
sK114: '$ki_world' > '$ki_world' ).
tff(func_def_120,type,
sK115: '$ki_world' > '$ki_world' ).
tff(func_def_121,type,
sK116: '$ki_world' > '$ki_world' ).
tff(func_def_122,type,
sK117: '$ki_world' > $i ).
tff(func_def_123,type,
sK118: '$ki_world' > '$ki_world' ).
tff(func_def_124,type,
sK119: '$ki_world' > '$ki_world' ).
tff(func_def_125,type,
sK120: '$ki_world' > '$ki_world' ).
tff(func_def_126,type,
sK121: '$ki_world' > $i ).
tff(func_def_127,type,
sK122: '$ki_world' > '$ki_world' ).
tff(func_def_128,type,
sK123: '$ki_world' > $i ).
tff(func_def_129,type,
sK124: '$ki_world' > '$ki_world' ).
tff(func_def_130,type,
sK125: '$ki_world' > '$ki_world' ).
tff(func_def_131,type,
sK126: '$ki_world' > '$ki_world' ).
tff(func_def_132,type,
sK127: '$ki_world' > $i ).
tff(func_def_133,type,
sK128: '$ki_world' > '$ki_world' ).
tff(func_def_134,type,
sK129: '$ki_world' > $i ).
tff(func_def_135,type,
sK130: '$ki_world' > '$ki_world' ).
tff(func_def_136,type,
sK131: '$ki_world' > $i ).
tff(func_def_137,type,
sK132: '$ki_world' > '$ki_world' ).
tff(func_def_138,type,
sK133: '$ki_world' > '$ki_world' ).
tff(func_def_139,type,
sK134: '$ki_world' > '$ki_world' ).
tff(func_def_140,type,
sK135: '$ki_world' > $i ).
tff(func_def_141,type,
sK136: '$ki_world' > '$ki_world' ).
tff(func_def_142,type,
sK137: '$ki_world' > $i ).
tff(func_def_143,type,
sK138: '$ki_world' > '$ki_world' ).
tff(func_def_144,type,
sK139: '$ki_world' > $i ).
tff(func_def_145,type,
sK140: '$ki_world' > '$ki_world' ).
tff(func_def_146,type,
sK141: '$ki_world' > '$ki_world' ).
tff(func_def_147,type,
sK142: '$ki_world' > '$ki_world' ).
tff(func_def_148,type,
sK143: '$ki_world' > $i ).
tff(func_def_149,type,
sK144: '$ki_world' > '$ki_world' ).
tff(func_def_150,type,
sK145: '$ki_world' > $i ).
tff(func_def_151,type,
sK146: '$ki_world' > '$ki_world' ).
tff(func_def_152,type,
sK147: '$ki_world' > '$ki_world' ).
tff(func_def_153,type,
sK148: '$ki_world' > '$ki_world' ).
tff(func_def_154,type,
sK149: '$ki_world' > $i ).
tff(func_def_155,type,
sK150: '$ki_world' > '$ki_world' ).
tff(func_def_156,type,
sK151: '$ki_world' > '$ki_world' ).
tff(func_def_157,type,
sK152: '$ki_world' > '$ki_world' ).
tff(func_def_158,type,
sK153: '$ki_world' > $i ).
tff(func_def_159,type,
sK154: '$ki_world' > '$ki_world' ).
tff(func_def_160,type,
sK155: '$ki_world' > '$ki_world' ).
tff(func_def_161,type,
sK156: '$ki_world' > '$ki_world' ).
tff(func_def_162,type,
sK157: '$ki_world' > $i ).
tff(func_def_163,type,
sK158: '$ki_world' > '$ki_world' ).
tff(func_def_164,type,
sK159: '$ki_world' > $i ).
tff(func_def_165,type,
sK160: '$ki_world' > '$ki_world' ).
tff(func_def_166,type,
sK161: '$ki_world' > '$ki_world' ).
tff(func_def_167,type,
sK162: '$ki_world' > '$ki_world' ).
tff(func_def_168,type,
sK163: '$ki_world' > $i ).
tff(func_def_169,type,
sK164: '$ki_world' > '$ki_world' ).
tff(func_def_170,type,
sK165: '$ki_world' > $i ).
tff(func_def_171,type,
sK166: '$ki_world' > '$ki_world' ).
tff(func_def_172,type,
sK167: '$ki_world' > '$ki_world' ).
tff(func_def_173,type,
sK168: '$ki_world' > '$ki_world' ).
tff(func_def_174,type,
sK169: '$ki_world' > $i ).
tff(func_def_175,type,
sK170: '$ki_world' > '$ki_world' ).
tff(func_def_176,type,
sK171: '$ki_world' > $i ).
tff(func_def_177,type,
sK172: '$ki_world' > '$ki_world' ).
tff(func_def_178,type,
sK173: '$ki_world' > $i ).
tff(func_def_179,type,
sK174: '$ki_world' > '$ki_world' ).
tff(func_def_180,type,
sK175: '$ki_world' > '$ki_world' ).
tff(func_def_181,type,
sK176: '$ki_world' > '$ki_world' ).
tff(func_def_182,type,
sK177: '$ki_world' > $i ).
tff(func_def_183,type,
sK178: '$ki_world' > '$ki_world' ).
tff(func_def_184,type,
sK179: '$ki_world' > $i ).
tff(func_def_185,type,
sK180: '$ki_world' > '$ki_world' ).
tff(func_def_186,type,
sK181: '$ki_world' > $i ).
tff(func_def_187,type,
sK182: '$ki_world' > '$ki_world' ).
tff(func_def_188,type,
sK183: '$ki_world' > '$ki_world' ).
tff(func_def_189,type,
sK184: '$ki_world' > '$ki_world' ).
tff(func_def_190,type,
sK185: '$ki_world' > '$ki_world' ).
tff(func_def_191,type,
sK186: '$ki_world' > '$ki_world' ).
tff(func_def_192,type,
sK187: '$ki_world' > '$ki_world' ).
tff(func_def_193,type,
sK188: '$ki_world' ).
tff(pred_def_1,type,
'$ki_accessible': ( '$ki_world' * '$ki_world' ) > $o ).
tff(pred_def_2,type,
r2: '$ki_world' > $o ).
tff(pred_def_3,type,
r3: '$ki_world' > $o ).
tff(pred_def_4,type,
r4: '$ki_world' > $o ).
tff(pred_def_5,type,
r5: '$ki_world' > $o ).
tff(pred_def_6,type,
equivalence_1: '$ki_world' > $o ).
tff(pred_def_7,type,
equivalence_2: '$ki_world' > $o ).
tff(pred_def_8,type,
cn2: '$ki_world' > $o ).
tff(pred_def_9,type,
cn1: '$ki_world' > $o ).
tff(pred_def_10,type,
cn3: '$ki_world' > $o ).
tff(pred_def_11,type,
kn2: '$ki_world' > $o ).
tff(pred_def_12,type,
kn1: '$ki_world' > $o ).
tff(pred_def_13,type,
kn3: '$ki_world' > $o ).
tff(pred_def_14,type,
equivalence_3: '$ki_world' > $o ).
tff(pred_def_15,type,
op_implies_or: '$ki_world' > $o ).
tff(pred_def_16,type,
op_and: '$ki_world' > $o ).
tff(pred_def_17,type,
and_2: '$ki_world' > $o ).
tff(pred_def_18,type,
and_3: '$ki_world' > $o ).
tff(pred_def_19,type,
and_1: '$ki_world' > $o ).
tff(pred_def_20,type,
implies_2: '$ki_world' > $o ).
tff(pred_def_21,type,
implies_3: '$ki_world' > $o ).
tff(pred_def_22,type,
op_implies_and: '$ki_world' > $o ).
tff(pred_def_23,type,
implies_1: '$ki_world' > $o ).
tff(pred_def_24,type,
substitution_of_equivalents: '$ki_world' > $o ).
tff(pred_def_25,type,
op_or: '$ki_world' > $o ).
tff(pred_def_26,type,
modus_tollens: '$ki_world' > $o ).
tff(pred_def_27,type,
or_1: '$ki_world' > $o ).
tff(pred_def_28,type,
or_2: '$ki_world' > $o ).
tff(pred_def_29,type,
or_3: '$ki_world' > $o ).
tff(pred_def_30,type,
op_equiv: '$ki_world' > $o ).
tff(pred_def_31,type,
modus_ponens: '$ki_world' > $o ).
tff(pred_def_32,type,
r1: '$ki_world' > $o ).
tff(pred_def_33,type,
qmltpeq: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_34,type,
is_a_theorem: ( '$ki_world' * $i ) > $o ).
tff(pred_def_35,type,
'$ki_exists_in_world_$i': ( '$ki_world' * $i ) > $o ).
tff(pred_def_36,type,
sP0: '$ki_world' > $o ).
tff(f1,axiom,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_reflexive) ).
tff(f26,axiom,
( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> or_2(X1) )
=> ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X1,X2)
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X1,X3)
=> ! [X4: $i] :
( '$ki_exists_in_world_$i'(X3,X4)
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X3,X5)
=> is_a_theorem(X5,implies(X4,or(X2,X4))) ) ) ) ) ) ) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X1,X2)
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X1,X3)
=> ! [X4: $i] :
( '$ki_exists_in_world_$i'(X3,X4)
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X3,X5)
=> is_a_theorem(X5,implies(X4,or(X2,X4))) ) ) ) ) )
=> ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> or_2(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_2_0) ).
tff(f38,axiom,
( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> r2(X1) )
=> ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X1,X2)
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X1,X3)
=> ! [X4: $i] :
( '$ki_exists_in_world_$i'(X3,X4)
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X3,X5)
=> is_a_theorem(X5,implies(X4,or(X2,X4))) ) ) ) ) ) ) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X1,X2)
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X1,X3)
=> ! [X4: $i] :
( '$ki_exists_in_world_$i'(X3,X4)
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X3,X5)
=> is_a_theorem(X5,implies(X4,or(X2,X4))) ) ) ) ) )
=> ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> r2(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',r2_0) ).
tff(f59,axiom,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> or_2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hilbert_or_2) ).
tff(f68,conjecture,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> r2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',verify) ).
tff(f69,negated_conjecture,
~ ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> r2(X0) ),
inference(negated_conjecture,[status(cth)],[f68]) ).
tff(f92,plain,
( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> or_2(X1) )
=> ! [X2: '$ki_world'] :
( '$ki_accessible'(X0,X2)
=> ! [X3: $i] :
( '$ki_exists_in_world_$i'(X2,X3)
=> ! [X4: '$ki_world'] :
( '$ki_accessible'(X2,X4)
=> ! [X5: $i] :
( '$ki_exists_in_world_$i'(X4,X5)
=> ! [X6: '$ki_world'] :
( '$ki_accessible'(X4,X6)
=> is_a_theorem(X6,implies(X5,or(X3,X5))) ) ) ) ) ) ) )
& ! [X7: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X7)
=> ( ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> ! [X9: $i] :
( '$ki_exists_in_world_$i'(X8,X9)
=> ! [X10: '$ki_world'] :
( '$ki_accessible'(X8,X10)
=> ! [X11: $i] :
( '$ki_exists_in_world_$i'(X10,X11)
=> ! [X12: '$ki_world'] :
( '$ki_accessible'(X10,X12)
=> is_a_theorem(X12,implies(X11,or(X9,X11))) ) ) ) ) )
=> ! [X13: '$ki_world'] :
( '$ki_accessible'(X7,X13)
=> or_2(X13) ) ) ) ),
inference(rectify,[],[f26]) ).
tff(f104,plain,
( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> r2(X1) )
=> ! [X2: '$ki_world'] :
( '$ki_accessible'(X0,X2)
=> ! [X3: $i] :
( '$ki_exists_in_world_$i'(X2,X3)
=> ! [X4: '$ki_world'] :
( '$ki_accessible'(X2,X4)
=> ! [X5: $i] :
( '$ki_exists_in_world_$i'(X4,X5)
=> ! [X6: '$ki_world'] :
( '$ki_accessible'(X4,X6)
=> is_a_theorem(X6,implies(X5,or(X3,X5))) ) ) ) ) ) ) )
& ! [X7: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X7)
=> ( ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> ! [X9: $i] :
( '$ki_exists_in_world_$i'(X8,X9)
=> ! [X10: '$ki_world'] :
( '$ki_accessible'(X8,X10)
=> ! [X11: $i] :
( '$ki_exists_in_world_$i'(X10,X11)
=> ! [X12: '$ki_world'] :
( '$ki_accessible'(X10,X12)
=> is_a_theorem(X12,implies(X11,or(X9,X11))) ) ) ) ) )
=> ! [X13: '$ki_world'] :
( '$ki_accessible'(X7,X13)
=> r2(X13) ) ) ) ),
inference(rectify,[],[f38]) ).
tff(f158,plain,
( ! [X0: '$ki_world'] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ! [X4: '$ki_world'] :
( ! [X5: $i] :
( ! [X6: '$ki_world'] :
( is_a_theorem(X6,implies(X5,or(X3,X5)))
| ~ '$ki_accessible'(X4,X6) )
| ~ '$ki_exists_in_world_$i'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ? [X1: '$ki_world'] :
( ~ or_2(X1)
& '$ki_accessible'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X13: '$ki_world'] :
( or_2(X13)
| ~ '$ki_accessible'(X7,X13) )
| ? [X8: '$ki_world'] :
( ? [X9: $i] :
( ? [X10: '$ki_world'] :
( ? [X11: $i] :
( ? [X12: '$ki_world'] :
( ~ is_a_theorem(X12,implies(X11,or(X9,X11)))
& '$ki_accessible'(X10,X12) )
& '$ki_exists_in_world_$i'(X10,X11) )
& '$ki_accessible'(X8,X10) )
& '$ki_exists_in_world_$i'(X8,X9) )
& '$ki_accessible'(X7,X8) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(ennf_transformation,[],[f92]) ).
tff(f159,plain,
( ! [X0: '$ki_world'] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ! [X4: '$ki_world'] :
( ! [X5: $i] :
( ! [X6: '$ki_world'] :
( is_a_theorem(X6,implies(X5,or(X3,X5)))
| ~ '$ki_accessible'(X4,X6) )
| ~ '$ki_exists_in_world_$i'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ? [X1: '$ki_world'] :
( ~ or_2(X1)
& '$ki_accessible'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X13: '$ki_world'] :
( or_2(X13)
| ~ '$ki_accessible'(X7,X13) )
| ? [X8: '$ki_world'] :
( ? [X9: $i] :
( ? [X10: '$ki_world'] :
( ? [X11: $i] :
( ? [X12: '$ki_world'] :
( ~ is_a_theorem(X12,implies(X11,or(X9,X11)))
& '$ki_accessible'(X10,X12) )
& '$ki_exists_in_world_$i'(X10,X11) )
& '$ki_accessible'(X8,X10) )
& '$ki_exists_in_world_$i'(X8,X9) )
& '$ki_accessible'(X7,X8) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(flattening,[],[f158]) ).
tff(f182,plain,
( ! [X0: '$ki_world'] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ! [X4: '$ki_world'] :
( ! [X5: $i] :
( ! [X6: '$ki_world'] :
( is_a_theorem(X6,implies(X5,or(X3,X5)))
| ~ '$ki_accessible'(X4,X6) )
| ~ '$ki_exists_in_world_$i'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ? [X1: '$ki_world'] :
( ~ r2(X1)
& '$ki_accessible'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X13: '$ki_world'] :
( r2(X13)
| ~ '$ki_accessible'(X7,X13) )
| ? [X8: '$ki_world'] :
( ? [X9: $i] :
( ? [X10: '$ki_world'] :
( ? [X11: $i] :
( ? [X12: '$ki_world'] :
( ~ is_a_theorem(X12,implies(X11,or(X9,X11)))
& '$ki_accessible'(X10,X12) )
& '$ki_exists_in_world_$i'(X10,X11) )
& '$ki_accessible'(X8,X10) )
& '$ki_exists_in_world_$i'(X8,X9) )
& '$ki_accessible'(X7,X8) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(ennf_transformation,[],[f104]) ).
tff(f183,plain,
( ! [X0: '$ki_world'] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ! [X4: '$ki_world'] :
( ! [X5: $i] :
( ! [X6: '$ki_world'] :
( is_a_theorem(X6,implies(X5,or(X3,X5)))
| ~ '$ki_accessible'(X4,X6) )
| ~ '$ki_exists_in_world_$i'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ? [X1: '$ki_world'] :
( ~ r2(X1)
& '$ki_accessible'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X13: '$ki_world'] :
( r2(X13)
| ~ '$ki_accessible'(X7,X13) )
| ? [X8: '$ki_world'] :
( ? [X9: $i] :
( ? [X10: '$ki_world'] :
( ? [X11: $i] :
( ? [X12: '$ki_world'] :
( ~ is_a_theorem(X12,implies(X11,or(X9,X11)))
& '$ki_accessible'(X10,X12) )
& '$ki_exists_in_world_$i'(X10,X11) )
& '$ki_accessible'(X8,X10) )
& '$ki_exists_in_world_$i'(X8,X9) )
& '$ki_accessible'(X7,X8) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(flattening,[],[f182]) ).
tff(f212,plain,
! [X0: '$ki_world'] :
( or_2(X0)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f59]) ).
tff(f221,plain,
? [X0: '$ki_world'] :
( ~ r2(X0)
& '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f69]) ).
tff(f272,plain,
( ! [X0: '$ki_world'] :
( ! [X1: '$ki_world'] :
( ! [X2: $i] :
( ! [X3: '$ki_world'] :
( ! [X4: $i] :
( ! [X5: '$ki_world'] :
( is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'(X3,X5) )
| ~ '$ki_exists_in_world_$i'(X3,X4) )
| ~ '$ki_accessible'(X1,X3) )
| ~ '$ki_exists_in_world_$i'(X1,X2) )
| ~ '$ki_accessible'(X0,X1) )
| ? [X6: '$ki_world'] :
( ~ or_2(X6)
& '$ki_accessible'(X0,X6) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( or_2(X8)
| ~ '$ki_accessible'(X7,X8) )
| ? [X9: '$ki_world'] :
( ? [X10: $i] :
( ? [X11: '$ki_world'] :
( ? [X12: $i] :
( ? [X13: '$ki_world'] :
( ~ is_a_theorem(X13,implies(X12,or(X10,X12)))
& '$ki_accessible'(X11,X13) )
& '$ki_exists_in_world_$i'(X11,X12) )
& '$ki_accessible'(X9,X11) )
& '$ki_exists_in_world_$i'(X9,X10) )
& '$ki_accessible'(X7,X9) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(rectify,[],[f159]) ).
tff(f273,plain,
( ! [X0: '$ki_world'] :
( ! [X1: '$ki_world'] :
( ! [X2: $i] :
( ! [X3: '$ki_world'] :
( ! [X4: $i] :
( ! [X5: '$ki_world'] :
( is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'(X3,X5) )
| ~ '$ki_exists_in_world_$i'(X3,X4) )
| ~ '$ki_accessible'(X1,X3) )
| ~ '$ki_exists_in_world_$i'(X1,X2) )
| ~ '$ki_accessible'(X0,X1) )
| ( ~ or_2(sK83(X0))
& '$ki_accessible'(X0,sK83(X0)) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( or_2(X8)
| ~ '$ki_accessible'(X7,X8) )
| ( ~ is_a_theorem(sK88(X7),implies(sK87(X7),or(sK85(X7),sK87(X7))))
& '$ki_accessible'(sK86(X7),sK88(X7))
& '$ki_exists_in_world_$i'(sK86(X7),sK87(X7))
& '$ki_accessible'(sK84(X7),sK86(X7))
& '$ki_exists_in_world_$i'(sK84(X7),sK85(X7))
& '$ki_accessible'(X7,sK84(X7)) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83,sK84,sK85,sK86,sK87,sK88]),skolemize(X6,sK83(X0)),skolemize(X9,sK84(X7)),skolemize(X10,sK85(X7)),skolemize(X11,sK86(X7)),skolemize(X12,sK87(X7)),skolemize(X13,sK88(X7))],[f272]) ).
tff(f296,plain,
( ! [X0: '$ki_world'] :
( ! [X1: '$ki_world'] :
( ! [X2: $i] :
( ! [X3: '$ki_world'] :
( ! [X4: $i] :
( ! [X5: '$ki_world'] :
( is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'(X3,X5) )
| ~ '$ki_exists_in_world_$i'(X3,X4) )
| ~ '$ki_accessible'(X1,X3) )
| ~ '$ki_exists_in_world_$i'(X1,X2) )
| ~ '$ki_accessible'(X0,X1) )
| ? [X6: '$ki_world'] :
( ~ r2(X6)
& '$ki_accessible'(X0,X6) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8) )
| ? [X9: '$ki_world'] :
( ? [X10: $i] :
( ? [X11: '$ki_world'] :
( ? [X12: $i] :
( ? [X13: '$ki_world'] :
( ~ is_a_theorem(X13,implies(X12,or(X10,X12)))
& '$ki_accessible'(X11,X13) )
& '$ki_exists_in_world_$i'(X11,X12) )
& '$ki_accessible'(X9,X11) )
& '$ki_exists_in_world_$i'(X9,X10) )
& '$ki_accessible'(X7,X9) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(rectify,[],[f183]) ).
tff(f297,plain,
( ! [X0: '$ki_world'] :
( ! [X1: '$ki_world'] :
( ! [X2: $i] :
( ! [X3: '$ki_world'] :
( ! [X4: $i] :
( ! [X5: '$ki_world'] :
( is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'(X3,X5) )
| ~ '$ki_exists_in_world_$i'(X3,X4) )
| ~ '$ki_accessible'(X1,X3) )
| ~ '$ki_exists_in_world_$i'(X1,X2) )
| ~ '$ki_accessible'(X0,X1) )
| ( ~ r2(sK155(X0))
& '$ki_accessible'(X0,sK155(X0)) )
| ~ '$ki_accessible'('$ki_local_world',X0) )
& ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8) )
| ( ~ is_a_theorem(sK160(X7),implies(sK159(X7),or(sK157(X7),sK159(X7))))
& '$ki_accessible'(sK158(X7),sK160(X7))
& '$ki_exists_in_world_$i'(sK158(X7),sK159(X7))
& '$ki_accessible'(sK156(X7),sK158(X7))
& '$ki_exists_in_world_$i'(sK156(X7),sK157(X7))
& '$ki_accessible'(X7,sK156(X7)) )
| ~ '$ki_accessible'('$ki_local_world',X7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK155,sK156,sK157,sK158,sK159,sK160]),skolemize(X6,sK155(X0)),skolemize(X9,sK156(X7)),skolemize(X10,sK157(X7)),skolemize(X11,sK158(X7)),skolemize(X12,sK159(X7)),skolemize(X13,sK160(X7))],[f296]) ).
tff(f314,plain,
( ~ r2(sK188)
& '$ki_accessible'('$ki_local_world',sK188) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK188]),skolemize(X0,sK188)],[f221]) ).
tff(f315,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f448,plain,
! [X2: $i,X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: $i,X5: '$ki_world'] :
( is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'(X3,X5)
| ~ '$ki_exists_in_world_$i'(X3,X4)
| ~ '$ki_accessible'(X1,X3)
| ~ '$ki_exists_in_world_$i'(X1,X2)
| ~ '$ki_accessible'(X0,X1)
| '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f273]) ).
tff(f449,plain,
! [X2: $i,X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: $i,X5: '$ki_world'] :
( ~ or_2(sK83(X0))
| ~ '$ki_accessible'(X3,X5)
| ~ '$ki_exists_in_world_$i'(X3,X4)
| ~ '$ki_accessible'(X1,X3)
| ~ '$ki_exists_in_world_$i'(X1,X2)
| ~ '$ki_accessible'(X0,X1)
| is_a_theorem(X5,implies(X4,or(X2,X4)))
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f273]) ).
tff(f538,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| '$ki_accessible'(X7,sK156(X7))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f539,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| '$ki_exists_in_world_$i'(sK156(X7),sK157(X7))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f540,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| '$ki_accessible'(sK156(X7),sK158(X7))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f541,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| '$ki_exists_in_world_$i'(sK158(X7),sK159(X7))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f542,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| '$ki_accessible'(sK158(X7),sK160(X7))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f543,plain,
! [X8: '$ki_world',X7: '$ki_world'] :
( r2(X8)
| ~ '$ki_accessible'(X7,X8)
| ~ is_a_theorem(sK160(X7),implies(sK159(X7),or(sK157(X7),sK159(X7))))
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f297]) ).
tff(f596,plain,
! [X0: '$ki_world'] :
( or_2(X0)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f212]) ).
tff(f605,plain,
'$ki_accessible'('$ki_local_world',sK188),
inference(cnf_transformation,[],[f314]) ).
tff(f606,plain,
~ r2(sK188),
inference(cnf_transformation,[],[f314]) ).
tff(f607,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK156(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f538,f606]) ).
tff(f608,plain,
! [X0: '$ki_world'] :
( '$ki_exists_in_world_$i'(sK156(X0),sK157(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f539,f606]) ).
tff(f609,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f540,f606]) ).
tff(f610,plain,
! [X0: '$ki_world'] :
( '$ki_exists_in_world_$i'(sK158(X0),sK159(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f541,f606]) ).
tff(f611,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(sK158(X0),sK160(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f542,f606]) ).
tff(f612,plain,
! [X0: '$ki_world'] :
( ~ is_a_theorem(sK160(X0),implies(sK159(X0),or(sK157(X0),sK159(X0))))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f543,f606]) ).
tff(f659,plain,
! [X2: $i,X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: $i,X5: '$ki_world'] :
( is_a_theorem(X1,implies(X2,or(X4,X2)))
| ~ '$ki_exists_in_world_$i'(X0,X2)
| ~ '$ki_accessible'(X3,X0)
| ~ '$ki_exists_in_world_$i'(X3,X4)
| ~ '$ki_accessible'(X5,X3)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X5)
| ~ '$ki_accessible'('$ki_local_world',sK83(X5)) ),
inference(resolution,[],[f449,f596]) ).
tff(f672,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( '$ki_accessible'(X3,sK83(X3))
| ~ '$ki_exists_in_world_$i'(X0,sK159(X1))
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_exists_in_world_$i'(X2,sK157(X1))
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'(X0,sK160(X1))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'(X1,sK188)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(resolution,[],[f448,f612]) ).
tff(f701,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X0,sK159(X1))
| ~ '$ki_exists_in_world_$i'(X2,sK157(X1))
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'(X0,sK160(X1))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'('$ki_local_world',sK83(X3))
| ~ '$ki_accessible'(X1,sK188)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(resolution,[],[f659,f612]) ).
tff(f703,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X0))
| ~ '$ki_accessible'(sK156(X0),X1)
| ~ '$ki_accessible'(X2,sK156(X0))
| ~ '$ki_accessible'(X1,sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'('$ki_local_world',sK83(X2))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f701,f608]) ).
tff(f704,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X0))
| ~ '$ki_accessible'(sK156(X0),X1)
| ~ '$ki_accessible'(X2,sK156(X0))
| ~ '$ki_accessible'(X1,sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'('$ki_local_world',sK83(X2))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f703]) ).
tff(f712,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'(sK158(X0),sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f704,f610]) ).
tff(f713,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'(sK158(X0),sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f712]) ).
tff(f715,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f713,f611]) ).
tff(f716,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f715]) ).
tff(f717,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f716,f609]) ).
tff(f718,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f717]) ).
tff(f721,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_exists_in_world_$i'(X1,sK159(X2))
| ~ '$ki_accessible'(X3,X1)
| ~ '$ki_exists_in_world_$i'(X3,sK157(X2))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'(X1,sK160(X2))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X2,sK188)
| ~ '$ki_accessible'('$ki_local_world',X2) ),
inference(resolution,[],[f718,f672]) ).
tff(f722,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_exists_in_world_$i'(X1,sK159(X2))
| ~ '$ki_accessible'(X3,X1)
| ~ '$ki_exists_in_world_$i'(X3,sK157(X2))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'(X1,sK160(X2))
| ~ '$ki_accessible'(X2,sK188)
| ~ '$ki_accessible'('$ki_local_world',X2) ),
inference(duplicate_literal_removal,[],[f721]) ).
tff(f725,definition,
( spl189_1
<=> ! [X2: '$ki_world',X1: '$ki_world',X3: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X2))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X2,sK188)
| ~ '$ki_accessible'(X1,sK160(X2))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_exists_in_world_$i'(X3,sK157(X2))
| ~ '$ki_accessible'(X3,X1) ) ),
introduced(definition,[new_symbols(definition,[spl189_1])],[avatar_definition]) ).
tff(f726,plain,
( ! [X2: '$ki_world',X3: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X2))
| ~ '$ki_exists_in_world_$i'(X3,sK157(X2))
| ~ '$ki_accessible'(X2,sK188)
| ~ '$ki_accessible'(X1,sK160(X2))
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X3,X1) )
| ~ spl189_1 ),
inference(avatar_component_clause,[],[f725]) ).
tff(f728,definition,
( spl189_2
<=> '$ki_accessible'('$ki_local_world','$ki_local_world') ),
introduced(definition,[new_symbols(definition,[spl189_2])],[avatar_definition]) ).
tff(f729,plain,
( ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| spl189_2 ),
inference(avatar_component_clause,[],[f728]) ).
tff(f731,definition,
( spl189_3
<=> ! [X0: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188) ) ),
introduced(definition,[new_symbols(definition,[spl189_3])],[avatar_definition]) ).
tff(f732,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188) )
| ~ spl189_3 ),
inference(avatar_component_clause,[],[f731]) ).
tff(f733,plain,
( spl189_1
| ~ spl189_2
| spl189_3 ),
inference(avatar_split_clause,[],[f722,f731,f728,f725]) ).
tff(f734,plain,
( $false
| spl189_2 ),
inference(resolution,[],[f729,f315]) ).
tff(f735,plain,
spl189_2,
inference(avatar_contradiction_clause,[],[f734]) ).
tff(f736,plain,
( ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'('$ki_local_world',sK188)
| ~ '$ki_accessible'('$ki_local_world',sK188)
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ spl189_3 ),
inference(resolution,[],[f732,f607]) ).
tff(f737,plain,
( ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'('$ki_local_world',sK188)
| ~ spl189_3 ),
inference(duplicate_literal_removal,[],[f736]) ).
tff(f739,definition,
( spl189_4
<=> '$ki_accessible'('$ki_local_world',sK188) ),
introduced(definition,[new_symbols(definition,[spl189_4])],[avatar_definition]) ).
tff(f740,plain,
( ~ '$ki_accessible'('$ki_local_world',sK188)
| spl189_4 ),
inference(avatar_component_clause,[],[f739]) ).
tff(f741,plain,
( ~ spl189_4
| ~ spl189_2
| ~ spl189_3 ),
inference(avatar_split_clause,[],[f737,f731,f728,f739]) ).
tff(f742,plain,
( $false
| spl189_4 ),
inference(resolution,[],[f740,f605]) ).
tff(f743,plain,
spl189_4,
inference(avatar_contradiction_clause,[],[f742]) ).
tff(f745,plain,
( ! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'(X1,sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(sK156(X0),X1)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) )
| ~ spl189_1 ),
inference(resolution,[],[f726,f608]) ).
tff(f746,plain,
( ! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK159(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'(X1,sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(sK156(X0),X1) )
| ~ spl189_1 ),
inference(duplicate_literal_removal,[],[f745]) ).
tff(f748,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'(sK158(X0),sK160(X0))
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) )
| ~ spl189_1 ),
inference(resolution,[],[f746,f610]) ).
tff(f749,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK158(X0),sK160(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(sK156(X0),sK158(X0)) )
| ~ spl189_1 ),
inference(duplicate_literal_removal,[],[f748]) ).
tff(f752,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) )
| ~ spl189_1 ),
inference(resolution,[],[f749,f611]) ).
tff(f753,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK156(X0),sK158(X0))
| ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188) )
| ~ spl189_1 ),
inference(duplicate_literal_removal,[],[f752]) ).
tff(f754,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'(X0,sK188)
| ~ '$ki_accessible'('$ki_local_world',X0) )
| ~ spl189_1 ),
inference(resolution,[],[f753,f609]) ).
tff(f755,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK156(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK188) )
| ~ spl189_1 ),
inference(duplicate_literal_removal,[],[f754]) ).
tff(f756,plain,
( spl189_3
| ~ spl189_1 ),
inference(avatar_split_clause,[],[f755,f725,f731]) ).
cnf(s1,plain,
( spl189_1
| ~ spl189_2
| spl189_3 ),
inference(sat_conversion,[],[f733]) ).
cnf(s2,plain,
spl189_2,
inference(sat_conversion,[],[f735]) ).
cnf(s3,plain,
( ~ spl189_2
| ~ spl189_3
| ~ spl189_4 ),
inference(sat_conversion,[],[f741]) ).
cnf(s4,plain,
spl189_4,
inference(sat_conversion,[],[f743]) ).
cnf(s5,plain,
( ~ spl189_1
| spl189_3 ),
inference(sat_conversion,[],[f756]) ).
cnf(s6,plain,
( ~ spl189_2
| ~ spl189_3 ),
inference(rat,[],[s3,s4]) ).
cnf(s7,plain,
~ spl189_3,
inference(rat,[],[s6,s2]) ).
cnf(s8,plain,
~ spl189_1,
inference(rat,[],[s5,s7]) ).
cnf(s9,plain,
$false,
inference(rat,[],[s1,s7,s2,s8]) ).
tff(f757,plain,
$false,
inference(avatar_sat_refutation,[],[s9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.33 % Computer : n012.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Sun Sep 27 17:07:19 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.06/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 Running first-order theorem proving
% 0.11/0.36 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.59/1.09 % (2597832)Detected formulas, will run a generic FOF schedule.
% 2.59/1.09 % (2597847)dis-21_1_sil=8000:lcm=predicate:random_seed=2935257506:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.59/1.09 % (2597847)First to succeed.
% 2.59/1.09 % (2597847)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2597832"
% 2.59/1.09 % (2597842)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2273741703:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.59/1.09 % (2597844)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=715842384:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.59/1.09 % (2597843)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1122968375:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.59/1.09 % (2597845)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2762699777:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.59/1.09 % (2597846)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3071517364:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.59/1.09 % (2597841)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2996505632:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.59/1.09 % (2597844)Refutation not found, incomplete strategy
% 2.59/1.09 % (2597844)------------------------------
% 2.59/1.09 % (2597844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.09 % (2597844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.09 % (2597844)CaDiCaL version: 2.1.3
% 2.59/1.09 % (2597844)Termination reason: Refutation not found, incomplete strategy
% 2.59/1.09 % (2597844)Time elapsed: 0.002 s
% 2.59/1.09 % (2597844)Peak memory usage: 87 MB
% 2.59/1.09 % (2597844)Instructions burned: 2 (million)
% 2.59/1.09 % (2597846)Also succeeded, but the first one will report.
% 2.59/1.09 % (2597845)Instruction limit reached!
% 2.59/1.09 % (2597845)------------------------------
% 2.59/1.09 % (2597845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.09 % (2597845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.09 % (2597845)CaDiCaL version: 2.1.3
% 2.59/1.09 % (2597845)Termination reason: Instruction limit
% 2.59/1.09 % (2597845)Termination phase: Saturation
% 2.59/1.09 % (2597845)Time elapsed: 0.054 s
% 2.59/1.09 % (2597845)Peak memory usage: 89 MB
% 2.59/1.09 % (2597845)Instructions burned: 121 (million)
% 2.59/1.09 % (2597847)Refutation found. Thanks to Tanya!
% 2.59/1.09 % SZS status Theorem for theBenchmark
% 2.59/1.09 % SZS output start Proof for theBenchmark
% See solution above
% 3.09/1.25 % (2597847)------------------------------
% 3.09/1.25 % (2597847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.25 % (2597847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.25 % (2597847)CaDiCaL version: 2.1.3
% 3.09/1.25 % (2597847)Termination reason: Refutation
% 3.09/1.25 % (2597847)Time elapsed: 0.012 s
% 3.09/1.25 % (2597847)Peak memory usage: 90 MB
% 3.09/1.25 % (2597847)Instructions burned: 36 (million)
% 3.09/1.25 % (2597847)------------------------------
% 3.09/1.25 % (2597847)------------------------------
% 3.09/1.25 % (2597832)Success in time 0.378 s
% 3.09/1.25 % Vampire exiting
%------------------------------------------------------------------------------