%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 12:01:13 PM UTC 2026
% Result : Theorem 0.17s 0.52s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 63 ( 9 unt; 0 typ; 1 def)
% Number of atoms : 424 ( 0 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 550 ( 231 ~; 218 |; 33 &)
% ( 1 <=>; 67 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 42 ( 42 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 39 ( 38 usr; 2 prp; 0-3 aty)
% Number of functors : 189 ( 189 usr; 2 con; 0-3 aty)
% Number of variables : 202 ( 0 sgn 177 !; 25 ?; 202 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_6,type,
sK0: '$ki_world' > $i ).
tff(func_def_7,type,
sK1: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_8,type,
sK2: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_9,type,
sK3: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_10,type,
sK4: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_11,type,
sK5: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_12,type,
sK6: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_13,type,
sK7: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_14,type,
sK8: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_15,type,
sK9: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_16,type,
sK10: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_17,type,
sK11: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_18,type,
sK12: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_19,type,
sK13: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_20,type,
sK14: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_21,type,
sK15: '$ki_world' > '$ki_world' ).
tff(func_def_22,type,
sK16: '$ki_world' > '$ki_world' ).
tff(func_def_23,type,
sK17: '$ki_world' > $i ).
tff(func_def_24,type,
sK18: '$ki_world' > '$ki_world' ).
tff(func_def_25,type,
sK19: '$ki_world' > $i ).
tff(func_def_26,type,
sK20: '$ki_world' > '$ki_world' ).
tff(func_def_27,type,
sK21: '$ki_world' > '$ki_world' ).
tff(func_def_28,type,
sK22: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_29,type,
sK23: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_30,type,
sK24: '$ki_world' > '$ki_world' ).
tff(func_def_31,type,
sK25: '$ki_world' > '$ki_world' ).
tff(func_def_32,type,
sK26: '$ki_world' > $i ).
tff(func_def_33,type,
sK27: '$ki_world' > '$ki_world' ).
tff(func_def_34,type,
sK28: '$ki_world' > $i ).
tff(func_def_35,type,
sK29: '$ki_world' > '$ki_world' ).
tff(func_def_36,type,
sK30: '$ki_world' > '$ki_world' ).
tff(func_def_37,type,
sK31: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_38,type,
sK32: '$ki_world' > '$ki_world' ).
tff(func_def_39,type,
sK33: '$ki_world' > '$ki_world' ).
tff(func_def_40,type,
sK34: '$ki_world' > $i ).
tff(func_def_41,type,
sK35: '$ki_world' > '$ki_world' ).
tff(func_def_42,type,
sK36: '$ki_world' > $i ).
tff(func_def_43,type,
sK37: '$ki_world' > '$ki_world' ).
tff(func_def_44,type,
sK38: '$ki_world' > '$ki_world' ).
tff(func_def_45,type,
sK39: '$ki_world' > '$ki_world' ).
tff(func_def_46,type,
sK40: '$ki_world' > $i ).
tff(func_def_47,type,
sK41: '$ki_world' > '$ki_world' ).
tff(func_def_48,type,
sK42: '$ki_world' > $i ).
tff(func_def_49,type,
sK43: '$ki_world' > '$ki_world' ).
tff(func_def_50,type,
sK44: '$ki_world' > '$ki_world' ).
tff(func_def_51,type,
sK45: '$ki_world' > '$ki_world' ).
tff(func_def_52,type,
sK46: '$ki_world' > $i ).
tff(func_def_53,type,
sK47: '$ki_world' > '$ki_world' ).
tff(func_def_54,type,
sK48: '$ki_world' > $i ).
tff(func_def_55,type,
sK49: '$ki_world' > '$ki_world' ).
tff(func_def_56,type,
sK50: '$ki_world' > '$ki_world' ).
tff(func_def_57,type,
sK51: '$ki_world' > '$ki_world' ).
tff(func_def_58,type,
sK52: '$ki_world' > $i ).
tff(func_def_59,type,
sK53: '$ki_world' > '$ki_world' ).
tff(func_def_60,type,
sK54: '$ki_world' > $i ).
tff(func_def_61,type,
sK55: '$ki_world' > '$ki_world' ).
tff(func_def_62,type,
sK56: '$ki_world' > $i ).
tff(func_def_63,type,
sK57: '$ki_world' > '$ki_world' ).
tff(func_def_64,type,
sK58: '$ki_world' > '$ki_world' ).
tff(func_def_65,type,
sK59: '$ki_world' > '$ki_world' ).
tff(func_def_66,type,
sK60: '$ki_world' > $i ).
tff(func_def_67,type,
sK61: '$ki_world' > '$ki_world' ).
tff(func_def_68,type,
sK62: '$ki_world' > $i ).
tff(func_def_69,type,
sK63: '$ki_world' > '$ki_world' ).
tff(func_def_70,type,
sK64: '$ki_world' > '$ki_world' ).
tff(func_def_71,type,
sK65: '$ki_world' > '$ki_world' ).
tff(func_def_72,type,
sK66: '$ki_world' > $i ).
tff(func_def_73,type,
sK67: '$ki_world' > '$ki_world' ).
tff(func_def_74,type,
sK68: '$ki_world' > $i ).
tff(func_def_75,type,
sK69: '$ki_world' > '$ki_world' ).
tff(func_def_76,type,
sK70: '$ki_world' > '$ki_world' ).
tff(func_def_77,type,
sK71: '$ki_world' > '$ki_world' ).
tff(func_def_78,type,
sK72: '$ki_world' > $i ).
tff(func_def_79,type,
sK73: '$ki_world' > '$ki_world' ).
tff(func_def_80,type,
sK74: '$ki_world' > $i ).
tff(func_def_81,type,
sK75: '$ki_world' > '$ki_world' ).
tff(func_def_82,type,
sK76: '$ki_world' > '$ki_world' ).
tff(func_def_83,type,
sK77: '$ki_world' > '$ki_world' ).
tff(func_def_84,type,
sK78: '$ki_world' > $i ).
tff(func_def_85,type,
sK79: '$ki_world' > '$ki_world' ).
tff(func_def_86,type,
sK80: '$ki_world' > $i ).
tff(func_def_87,type,
sK81: '$ki_world' > '$ki_world' ).
tff(func_def_88,type,
sK82: '$ki_world' > '$ki_world' ).
tff(func_def_89,type,
sK83: '$ki_world' > '$ki_world' ).
tff(func_def_90,type,
sK84: '$ki_world' > $i ).
tff(func_def_91,type,
sK85: '$ki_world' > '$ki_world' ).
tff(func_def_92,type,
sK86: '$ki_world' > $i ).
tff(func_def_93,type,
sK87: '$ki_world' > '$ki_world' ).
tff(func_def_94,type,
sK88: '$ki_world' > '$ki_world' ).
tff(func_def_95,type,
sK89: '$ki_world' > '$ki_world' ).
tff(func_def_96,type,
sK90: '$ki_world' > $i ).
tff(func_def_97,type,
sK91: '$ki_world' > '$ki_world' ).
tff(func_def_98,type,
sK92: '$ki_world' > $i ).
tff(func_def_99,type,
sK93: '$ki_world' > '$ki_world' ).
tff(func_def_100,type,
sK94: '$ki_world' > $i ).
tff(func_def_101,type,
sK95: '$ki_world' > '$ki_world' ).
tff(func_def_102,type,
sK96: '$ki_world' > '$ki_world' ).
tff(func_def_103,type,
sK97: '$ki_world' > '$ki_world' ).
tff(func_def_104,type,
sK98: '$ki_world' > $i ).
tff(func_def_105,type,
sK99: '$ki_world' > '$ki_world' ).
tff(func_def_106,type,
sK100: '$ki_world' > $i ).
tff(func_def_107,type,
sK101: '$ki_world' > '$ki_world' ).
tff(func_def_108,type,
sK102: '$ki_world' > '$ki_world' ).
tff(func_def_109,type,
sK103: '$ki_world' > '$ki_world' ).
tff(func_def_110,type,
sK104: '$ki_world' > $i ).
tff(func_def_111,type,
sK105: '$ki_world' > '$ki_world' ).
tff(func_def_112,type,
sK106: '$ki_world' > $i ).
tff(func_def_113,type,
sK107: '$ki_world' > '$ki_world' ).
tff(func_def_114,type,
sK108: '$ki_world' > '$ki_world' ).
tff(func_def_115,type,
sK109: '$ki_world' > '$ki_world' ).
tff(func_def_116,type,
sK110: '$ki_world' > $i ).
tff(func_def_117,type,
sK111: '$ki_world' > '$ki_world' ).
tff(func_def_118,type,
sK112: '$ki_world' > $i ).
tff(func_def_119,type,
sK113: '$ki_world' > '$ki_world' ).
tff(func_def_120,type,
sK114: '$ki_world' > '$ki_world' ).
tff(func_def_121,type,
sK115: '$ki_world' > '$ki_world' ).
tff(func_def_122,type,
sK116: '$ki_world' > $i ).
tff(func_def_123,type,
sK117: '$ki_world' > '$ki_world' ).
tff(func_def_124,type,
sK118: '$ki_world' > '$ki_world' ).
tff(func_def_125,type,
sK119: '$ki_world' > '$ki_world' ).
tff(func_def_126,type,
sK120: '$ki_world' > $i ).
tff(func_def_127,type,
sK121: '$ki_world' > '$ki_world' ).
tff(func_def_128,type,
sK122: '$ki_world' > $i ).
tff(func_def_129,type,
sK123: '$ki_world' > '$ki_world' ).
tff(func_def_130,type,
sK124: '$ki_world' > '$ki_world' ).
tff(func_def_131,type,
sK125: '$ki_world' > '$ki_world' ).
tff(func_def_132,type,
sK126: '$ki_world' > $i ).
tff(func_def_133,type,
sK127: '$ki_world' > '$ki_world' ).
tff(func_def_134,type,
sK128: '$ki_world' > $i ).
tff(func_def_135,type,
sK129: '$ki_world' > '$ki_world' ).
tff(func_def_136,type,
sK130: '$ki_world' > $i ).
tff(func_def_137,type,
sK131: '$ki_world' > '$ki_world' ).
tff(func_def_138,type,
sK132: '$ki_world' > '$ki_world' ).
tff(func_def_139,type,
sK133: '$ki_world' > '$ki_world' ).
tff(func_def_140,type,
sK134: '$ki_world' > $i ).
tff(func_def_141,type,
sK135: '$ki_world' > '$ki_world' ).
tff(func_def_142,type,
sK136: '$ki_world' > $i ).
tff(func_def_143,type,
sK137: '$ki_world' > '$ki_world' ).
tff(func_def_144,type,
sK138: '$ki_world' > $i ).
tff(func_def_145,type,
sK139: '$ki_world' > '$ki_world' ).
tff(func_def_146,type,
sK140: '$ki_world' > '$ki_world' ).
tff(func_def_147,type,
sK141: '$ki_world' > '$ki_world' ).
tff(func_def_148,type,
sK142: '$ki_world' > $i ).
tff(func_def_149,type,
sK143: '$ki_world' > '$ki_world' ).
tff(func_def_150,type,
sK144: '$ki_world' > $i ).
tff(func_def_151,type,
sK145: '$ki_world' > '$ki_world' ).
tff(func_def_152,type,
sK146: '$ki_world' > '$ki_world' ).
tff(func_def_153,type,
sK147: '$ki_world' > '$ki_world' ).
tff(func_def_154,type,
sK148: '$ki_world' > $i ).
tff(func_def_155,type,
sK149: '$ki_world' > '$ki_world' ).
tff(func_def_156,type,
sK150: '$ki_world' > '$ki_world' ).
tff(func_def_157,type,
sK151: '$ki_world' > '$ki_world' ).
tff(func_def_158,type,
sK152: '$ki_world' > $i ).
tff(func_def_159,type,
sK153: '$ki_world' > '$ki_world' ).
tff(func_def_160,type,
sK154: '$ki_world' > '$ki_world' ).
tff(func_def_161,type,
sK155: '$ki_world' > '$ki_world' ).
tff(func_def_162,type,
sK156: '$ki_world' > $i ).
tff(func_def_163,type,
sK157: '$ki_world' > '$ki_world' ).
tff(func_def_164,type,
sK158: '$ki_world' > $i ).
tff(func_def_165,type,
sK159: '$ki_world' > '$ki_world' ).
tff(func_def_166,type,
sK160: '$ki_world' > '$ki_world' ).
tff(func_def_167,type,
sK161: '$ki_world' > '$ki_world' ).
tff(func_def_168,type,
sK162: '$ki_world' > $i ).
tff(func_def_169,type,
sK163: '$ki_world' > '$ki_world' ).
tff(func_def_170,type,
sK164: '$ki_world' > $i ).
tff(func_def_171,type,
sK165: '$ki_world' > '$ki_world' ).
tff(func_def_172,type,
sK166: '$ki_world' > '$ki_world' ).
tff(func_def_173,type,
sK167: '$ki_world' > '$ki_world' ).
tff(func_def_174,type,
sK168: '$ki_world' > $i ).
tff(func_def_175,type,
sK169: '$ki_world' > '$ki_world' ).
tff(func_def_176,type,
sK170: '$ki_world' > $i ).
tff(func_def_177,type,
sK171: '$ki_world' > '$ki_world' ).
tff(func_def_178,type,
sK172: '$ki_world' > $i ).
tff(func_def_179,type,
sK173: '$ki_world' > '$ki_world' ).
tff(func_def_180,type,
sK174: '$ki_world' > '$ki_world' ).
tff(func_def_181,type,
sK175: '$ki_world' > '$ki_world' ).
tff(func_def_182,type,
sK176: '$ki_world' > $i ).
tff(func_def_183,type,
sK177: '$ki_world' > '$ki_world' ).
tff(func_def_184,type,
sK178: '$ki_world' > $i ).
tff(func_def_185,type,
sK179: '$ki_world' > '$ki_world' ).
tff(func_def_186,type,
sK180: '$ki_world' > $i ).
tff(func_def_187,type,
sK181: '$ki_world' > '$ki_world' ).
tff(func_def_188,type,
sK182: '$ki_world' > '$ki_world' ).
tff(func_def_189,type,
sK183: '$ki_world' > '$ki_world' ).
tff(func_def_190,type,
sK184: '$ki_world' > '$ki_world' ).
tff(func_def_191,type,
sK185: '$ki_world' > '$ki_world' ).
tff(func_def_192,type,
sK186: '$ki_world' > '$ki_world' ).
tff(func_def_193,type,
sK187: '$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(f1,axiom,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',r2_0) ).
tff(f59,axiom,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> or_2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_2) ).
tff(f68,conjecture,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> r2(X0) ),
file('/export/starexec/sandbox/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(f222,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f348,plain,
! [X2: '$ki_world',X3: $i,X0: '$ki_world',X6: '$ki_world',X4: '$ki_world',X5: $i] :
( ~ or_2(sK83(X0))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,X2)
| ~ '$ki_exists_in_world_$i'(X2,X3)
| ~ '$ki_accessible'(X2,X4)
| ~ '$ki_exists_in_world_$i'(X4,X5)
| ~ '$ki_accessible'(X4,X6)
| is_a_theorem(X6,implies(X5,or(X3,X5))) ),
inference(cnf_transformation,[],[f159]) ).
tff(f349,plain,
! [X2: '$ki_world',X3: $i,X0: '$ki_world',X6: '$ki_world',X4: '$ki_world',X5: $i] :
( is_a_theorem(X6,implies(X5,or(X3,X5)))
| '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'(X0,X2)
| ~ '$ki_exists_in_world_$i'(X2,X3)
| ~ '$ki_accessible'(X2,X4)
| ~ '$ki_exists_in_world_$i'(X4,X5)
| ~ '$ki_accessible'(X4,X6)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f159]) ).
tff(f446,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| '$ki_accessible'(sK157(X7),sK159(X7))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f447,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| ~ is_a_theorem(sK159(X7),implies(sK158(X7),or(sK156(X7),sK158(X7))))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f448,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| '$ki_exists_in_world_$i'(sK157(X7),sK158(X7))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f449,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| '$ki_accessible'(sK154(X7),sK157(X7))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f450,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| '$ki_exists_in_world_$i'(sK154(X7),sK156(X7))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f451,plain,
! [X7: '$ki_world',X13: '$ki_world'] :
( r2(X13)
| '$ki_accessible'(X7,sK154(X7))
| ~ '$ki_accessible'(X7,X13)
| ~ '$ki_accessible'('$ki_local_world',X7) ),
inference(cnf_transformation,[],[f183]) ).
tff(f502,plain,
! [X0: '$ki_world'] :
( or_2(X0)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f212]) ).
tff(f511,plain,
'$ki_accessible'('$ki_local_world',sK187),
inference(cnf_transformation,[],[f221]) ).
tff(f512,plain,
~ r2(sK187),
inference(cnf_transformation,[],[f221]) ).
tff(f513,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK154(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f451,f512]) ).
tff(f514,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(sK157(X0),sK159(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f446,f512]) ).
tff(f515,plain,
! [X0: '$ki_world'] :
( '$ki_exists_in_world_$i'(sK157(X0),sK158(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f448,f512]) ).
tff(f516,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(sK154(X0),sK157(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f449,f512]) ).
tff(f517,plain,
! [X0: '$ki_world'] :
( '$ki_exists_in_world_$i'(sK154(X0),sK156(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f450,f512]) ).
tff(f518,plain,
! [X0: '$ki_world'] :
( ~ is_a_theorem(sK159(X0),implies(sK158(X0),or(sK156(X0),sK158(X0))))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f447,f512]) ).
tff(f565,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'(X0,X1)
| ~ '$ki_exists_in_world_$i'(X1,X2)
| ~ '$ki_accessible'(X1,X3)
| ~ '$ki_exists_in_world_$i'(X3,X4)
| ~ '$ki_accessible'(X3,X5)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'('$ki_local_world',sK83(X0)) ),
inference(resolution,[],[f348,f502]) ).
tff(f582,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X2))
| ~ '$ki_exists_in_world_$i'(X3,sK158(X2))
| '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'(X1,X3)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X3,sK159(X2))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X2,sK187)
| ~ '$ki_accessible'('$ki_local_world',X2) ),
inference(resolution,[],[f349,f518]) ).
tff(f584,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| '$ki_accessible'(X2,sK83(X2))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'(sK157(X0),sK159(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f582,f515]) ).
tff(f585,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| '$ki_accessible'(X2,sK83(X2))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'(sK157(X0),sK159(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f584]) ).
tff(f587,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| '$ki_accessible'(X2,sK83(X2))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(forward_subsumption_resolution,[],[f585,f514]) ).
tff(f588,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'(sK154(X1),sK157(X1))
| ~ '$ki_accessible'(X0,sK154(X1))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(resolution,[],[f587,f517]) ).
tff(f589,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'(sK154(X1),sK157(X1))
| ~ '$ki_accessible'(X0,sK154(X1))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(duplicate_literal_removal,[],[f588]) ).
tff(f590,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( '$ki_accessible'(X0,sK83(X0))
| ~ '$ki_accessible'(X0,sK154(X1))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(forward_subsumption_resolution,[],[f589,f516]) ).
tff(f646,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X2))
| ~ '$ki_exists_in_world_$i'(X3,sK158(X2))
| ~ '$ki_accessible'(X1,X3)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X3,sK159(X2))
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'('$ki_local_world',sK83(X0))
| ~ '$ki_accessible'(X2,sK187)
| ~ '$ki_accessible'('$ki_local_world',X2) ),
inference(resolution,[],[f565,f518]) ).
tff(f648,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'(sK157(X0),sK159(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'('$ki_local_world',sK83(X2))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f646,f515]) ).
tff(f649,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'(sK157(X0),sK159(X0))
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'('$ki_local_world',sK83(X2))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f648]) ).
tff(f651,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(X1,sK156(X0))
| ~ '$ki_accessible'(X1,sK157(X0))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'('$ki_local_world',sK83(X2))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(forward_subsumption_resolution,[],[f649,f514]) ).
tff(f652,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK154(X0),sK157(X0))
| ~ '$ki_accessible'(X1,sK154(X0))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f651,f517]) ).
tff(f653,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK154(X0),sK157(X0))
| ~ '$ki_accessible'(X1,sK154(X0))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(duplicate_literal_removal,[],[f652]) ).
tff(f654,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK154(X0))
| ~ '$ki_accessible'('$ki_local_world',sK83(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(forward_subsumption_resolution,[],[f653,f516]) ).
tff(f657,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK154(X0))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'('$ki_local_world',sK154(X1))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(resolution,[],[f654,f590]) ).
tff(f658,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK154(X0))
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'('$ki_local_world',sK154(X1))
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(duplicate_literal_removal,[],[f657]) ).
tff(f660,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK154(X0))
| ~ '$ki_accessible'(X0,sK187)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'('$ki_local_world',sK154(X1))
| ~ '$ki_accessible'(X1,sK187)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(forward_subsumption_resolution,[],[f658,f222]) ).
tff(f662,definition,
( spl188_1
<=> ! [X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK154(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X1,sK187) ) ),
introduced(definition,[new_symbols(definition,[spl188_1])],[avatar_definition]) ).
tff(f663,plain,
( ! [X1: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',sK154(X1))
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X1,sK187) )
| ~ spl188_1 ),
inference(avatar_component_clause,[],[f662]) ).
tff(f664,plain,
( spl188_1
| spl188_1 ),
inference(avatar_split_clause,[],[f660,f662,f662]) ).
tff(f667,plain,
( ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'('$ki_local_world',sK187)
| ~ '$ki_accessible'('$ki_local_world',sK187)
| ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ spl188_1 ),
inference(resolution,[],[f663,f513]) ).
tff(f668,plain,
( ~ '$ki_accessible'('$ki_local_world','$ki_local_world')
| ~ '$ki_accessible'('$ki_local_world',sK187)
| ~ spl188_1 ),
inference(duplicate_literal_removal,[],[f667]) ).
tff(f669,plain,
( ~ '$ki_accessible'('$ki_local_world',sK187)
| ~ spl188_1 ),
inference(forward_subsumption_resolution,[],[f668,f222]) ).
tff(f670,plain,
( $false
| ~ spl188_1 ),
inference(forward_subsumption_resolution,[],[f669,f511]) ).
tff(f671,plain,
~ spl188_1,
inference(avatar_contradiction_clause,[],[f670]) ).
cnf(s1,plain,
( spl188_1
| spl188_1 ),
inference(sat_conversion,[],[f664]) ).
cnf(s2,plain,
spl188_1,
inference(rat,[],[s1]) ).
cnf(s3,plain,
~ spl188_1,
inference(sat_conversion,[],[f671]) ).
cnf(s4,plain,
$false,
inference(rat,[],[s2,s3]) ).
tff(f672,plain,
$false,
inference(avatar_sat_refutation,[],[s4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n002.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 17:10:21 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.52 % (3749121)Will run a generic schedule for satisfiability detection.
% 0.17/0.52 % (3749142)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1873356077:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.52 % (3749138)% WARNING: option uhcvi not known.
% 0.17/0.52 % (3749137)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2584264129_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.52 % (3749138)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4150059884:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.52 % (3749140)dis+10_1_sil=32000:sp=arity:random_seed=958242110:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.52 % (3749139)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1808175642:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.52 % (3749141)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4222317244:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.52 % (3749143)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2693227937:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.52 % (3749142)Instruction limit reached!
% 0.17/0.52 % (3749142)------------------------------
% 0.17/0.52 % (3749142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.52 % (3749142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.52 % (3749142)CaDiCaL version: 2.1.3
% 0.17/0.52 % (3749142)Termination reason: Instruction limit
% 0.17/0.52 % (3749142)Termination phase: Saturation
% 0.17/0.52 % (3749142)Time elapsed: 0.036 s
% 0.17/0.52 % (3749142)Peak memory usage: 14 MB
% 0.17/0.52 % (3749142)Instructions burned: 131 (million)
% 0.17/0.52 % (3749173)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2900493817:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.17/0.52 % (3749141) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3749121-3749141"...
% 0.17/0.52 % (3749141)...printing done.
% 0.17/0.52 % (3749141)Refutation found. Thanks to Tanya!
% 0.17/0.52 % SZS status Theorem for theBenchmark
% 0.17/0.52 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.53 % (3749141)------------------------------
% 0.17/0.53 % (3749141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.53 % (3749141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.53 % (3749141)CaDiCaL version: 2.1.3
% 0.17/0.53 % (3749141)Termination reason: Refutation
% 0.17/0.53 % (3749141)Time elapsed: 0.044 s
% 0.17/0.53 % (3749141)Peak memory usage: 14 MB
% 0.17/0.53 % (3749141)Instructions burned: 86 (million)
% 0.17/0.53 % (3749121)Success in time 0.093 s
% 0.17/0.53 % Vampire exiting
%------------------------------------------------------------------------------