%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL949_4 : 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 : 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 12:01:14 PM UTC 2026
% Result : Theorem 0.08s 0.38s
% Output : Refutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 7
% Syntax : Number of formulae : 64 ( 15 unt; 0 typ; 3 def)
% Number of atoms : 437 ( 0 equ)
% Maximal formula atoms : 24 ( 6 avg)
% Number of connectives : 554 ( 233 ~; 216 |; 53 &)
% ( 2 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 52 ( 52 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 18 usr; 4 prp; 0-4 aty)
% Number of functors : 129 ( 129 usr; 3 con; 0-5 aty)
% Number of variables : 263 ( 0 sgn 232 !; 31 ?; 263 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_27,type,
sK7: '$ki_world' > $i ).
tff(func_def_28,type,
sK8: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_29,type,
sK9: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_30,type,
sK10: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_31,type,
sK11: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_32,type,
sK12: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_33,type,
sK13: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_34,type,
sK14: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_35,type,
sK15: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_36,type,
sK16: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_37,type,
sK17: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_38,type,
sK18: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_39,type,
sK19: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_40,type,
sK20: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_41,type,
sK21: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_42,type,
sK22: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_43,type,
sK23: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_44,type,
sK24: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_45,type,
sK25: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_46,type,
sK26: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_47,type,
sK27: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_48,type,
sK28: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_49,type,
sK29: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_50,type,
sK30: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_51,type,
sK31: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_52,type,
sK32: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_53,type,
sK33: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_54,type,
sK34: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_55,type,
sK35: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_56,type,
sK36: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_57,type,
sK37: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_58,type,
sK38: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_59,type,
sK39: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_60,type,
sK40: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_61,type,
sK41: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_62,type,
sK42: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_63,type,
sK43: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_64,type,
sK44: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_65,type,
sK45: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_66,type,
sK46: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_67,type,
sK47: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_68,type,
sK48: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_69,type,
sK49: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_70,type,
sK50: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_71,type,
sK51: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_72,type,
sK52: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_73,type,
sK53: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_74,type,
sK54: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_75,type,
sK55: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_76,type,
sK56: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_77,type,
sK57: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_78,type,
sK58: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_79,type,
sK59: ( $i * $i * '$ki_world' ) > $i ).
tff(func_def_80,type,
sK60: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_81,type,
sK61: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_82,type,
sK62: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_83,type,
sK63: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_84,type,
sK64: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_85,type,
sK65: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_86,type,
sK66: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_87,type,
sK67: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_88,type,
sK68: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_89,type,
sK69: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_90,type,
sK70: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_91,type,
sK71: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_92,type,
sK72: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_93,type,
sK73: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_94,type,
sK74: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_95,type,
sK75: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_96,type,
sK76: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_97,type,
sK77: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_98,type,
sK78: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_99,type,
sK79: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_100,type,
sK80: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_101,type,
sK81: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_102,type,
sK82: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_103,type,
sK83: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_104,type,
sK84: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_105,type,
sK85: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_106,type,
sK86: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_107,type,
sK87: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_108,type,
sK88: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_109,type,
sK89: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_110,type,
sK90: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_111,type,
sK91: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_112,type,
sK92: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_113,type,
sK93: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_114,type,
sK94: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_115,type,
sK95: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_116,type,
sK96: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_117,type,
sK97: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_118,type,
sK98: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_119,type,
sK99: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_120,type,
sK100: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_121,type,
sK101: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_122,type,
sK102: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_123,type,
sK103: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_124,type,
sK104: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_125,type,
sK105: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_127,type,
sK107: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_128,type,
sK108: ( $i * $i * '$ki_world' ) > $i ).
tff(func_def_129,type,
sK109: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_130,type,
sK110: ( $i * '$ki_world' * $i ) > '$ki_world' ).
tff(func_def_131,type,
sK111: ( $i * '$ki_world' * $i ) > '$ki_world' ).
tff(func_def_132,type,
sK112: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_133,type,
sK113: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_134,type,
sK114: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_135,type,
sK115: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_136,type,
sK116: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_137,type,
sK117: ( $i * $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_138,type,
sK118: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_139,type,
sK119: ( $i * $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_140,type,
sK120: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_141,type,
sK121: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_142,type,
sK122: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_143,type,
sK123: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_144,type,
sK124: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_145,type,
sK125: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_146,type,
sK126: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_147,type,
sK127: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_148,type,
sK128: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_149,type,
sK129: ( $i * $i * '$ki_world' ) > $i ).
tff(func_def_150,type,
sK130: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_151,type,
sK131: ( $i * '$ki_world' ) > $i ).
tff(func_def_152,type,
sK132: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_154,type,
sK134: ( $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_155,type,
sK135: '$ki_world' ).
tff(func_def_157,type,
sK137: '$ki_world' ).
tff(pred_def_1,type,
'$ki_accessible': ( '$ki_world' * '$ki_world' ) > $o ).
tff(pred_def_2,type,
qmltpeq: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_3,type,
inductive: ( '$ki_world' * $i ) > $o ).
tff(pred_def_4,type,
disjoint: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_5,type,
function: ( '$ki_world' * $i ) > $o ).
tff(pred_def_6,type,
member: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_7,type,
subclass: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_8,type,
'$ki_exists_in_world_$i': ( '$ki_world' * $i ) > $o ).
tff(pred_def_9,type,
sP0: ( $i * $i * '$ki_world' ) > $o ).
tff(pred_def_10,type,
sP1: ( $i * $i * $i * '$ki_world' ) > $o ).
tff(pred_def_11,type,
sP2: ( $i * $i * '$ki_world' ) > $o ).
tff(pred_def_12,type,
sP3: ( $i * $i * '$ki_world' ) > $o ).
tff(pred_def_13,type,
sP4: ( $i * $i * '$ki_world' ) > $o ).
tff(pred_def_14,type,
sP5: ( $i * $i * '$ki_world' ) > $o ).
tff(pred_def_15,type,
sP6: ( $i * $i * '$ki_world' ) > $o ).
tff(f1,axiom,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_reflexive) ).
tff(f3,axiom,
! [X0: '$ki_world',X1: $i] : '$ki_exists_in_world_$i'(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$ki_exists_in_world_$i_const') ).
tff(f47,axiom,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,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: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> subclass(X5,X1,X3) )
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> ! [X6: $i] :
( '$ki_exists_in_world_$i'(X5,X6)
=> ! [X7: '$ki_world'] :
( '$ki_accessible'(X5,X7)
=> ( ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> member(X8,X6,X1) )
=> ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> member(X8,X6,X3) ) ) ) ) ) ) )
& ! [X4: '$ki_world'] :
( '$ki_accessible'(X2,X4)
=> ( ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> ! [X6: $i] :
( '$ki_exists_in_world_$i'(X5,X6)
=> ! [X7: '$ki_world'] :
( '$ki_accessible'(X5,X7)
=> ( ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> member(X8,X6,X1) )
=> ! [X8: '$ki_world'] :
( '$ki_accessible'(X7,X8)
=> member(X8,X6,X3) ) ) ) ) )
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> subclass(X5,X1,X3) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_defn) ).
tff(f88,conjecture,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
=> ! [X2: '$ki_world'] :
( '$ki_accessible'(X0,X2)
=> subclass(X2,X1,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',verify) ).
tff(f89,negated_conjecture,
~ ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
=> ! [X2: '$ki_world'] :
( '$ki_accessible'(X0,X2)
=> subclass(X2,X1,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
tff(f131,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,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: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> subclass(X5,X1,X3) )
=> ! [X6: '$ki_world'] :
( '$ki_accessible'(X4,X6)
=> ! [X7: $i] :
( '$ki_exists_in_world_$i'(X6,X7)
=> ! [X8: '$ki_world'] :
( '$ki_accessible'(X6,X8)
=> ( ! [X9: '$ki_world'] :
( '$ki_accessible'(X8,X9)
=> member(X9,X7,X1) )
=> ! [X10: '$ki_world'] :
( '$ki_accessible'(X8,X10)
=> member(X10,X7,X3) ) ) ) ) ) ) )
& ! [X11: '$ki_world'] :
( '$ki_accessible'(X2,X11)
=> ( ! [X12: '$ki_world'] :
( '$ki_accessible'(X11,X12)
=> ! [X13: $i] :
( '$ki_exists_in_world_$i'(X12,X13)
=> ! [X14: '$ki_world'] :
( '$ki_accessible'(X12,X14)
=> ( ! [X15: '$ki_world'] :
( '$ki_accessible'(X14,X15)
=> member(X15,X13,X1) )
=> ! [X16: '$ki_world'] :
( '$ki_accessible'(X14,X16)
=> member(X16,X13,X3) ) ) ) ) )
=> ! [X17: '$ki_world'] :
( '$ki_accessible'(X11,X17)
=> subclass(X17,X1,X3) ) ) ) ) ) ) ) ),
inference(rectify,[],[f47]) ).
tff(f241,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ( ! [X4: '$ki_world'] :
( ! [X6: '$ki_world'] :
( ! [X7: $i] :
( ! [X8: '$ki_world'] :
( ! [X10: '$ki_world'] :
( member(X10,X7,X3)
| ~ '$ki_accessible'(X8,X10) )
| ? [X9: '$ki_world'] :
( ~ member(X9,X7,X1)
& '$ki_accessible'(X8,X9) )
| ~ '$ki_accessible'(X6,X8) )
| ~ '$ki_exists_in_world_$i'(X6,X7) )
| ~ '$ki_accessible'(X4,X6) )
| ? [X5: '$ki_world'] :
( ~ subclass(X5,X1,X3)
& '$ki_accessible'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
& ! [X11: '$ki_world'] :
( ! [X17: '$ki_world'] :
( subclass(X17,X1,X3)
| ~ '$ki_accessible'(X11,X17) )
| ? [X12: '$ki_world'] :
( ? [X13: $i] :
( ? [X14: '$ki_world'] :
( ? [X16: '$ki_world'] :
( ~ member(X16,X13,X3)
& '$ki_accessible'(X14,X16) )
& ! [X15: '$ki_world'] :
( member(X15,X13,X1)
| ~ '$ki_accessible'(X14,X15) )
& '$ki_accessible'(X12,X14) )
& '$ki_exists_in_world_$i'(X12,X13) )
& '$ki_accessible'(X11,X12) )
| ~ '$ki_accessible'(X2,X11) ) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f131]) ).
tff(f242,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ( ! [X4: '$ki_world'] :
( ! [X6: '$ki_world'] :
( ! [X7: $i] :
( ! [X8: '$ki_world'] :
( ! [X10: '$ki_world'] :
( member(X10,X7,X3)
| ~ '$ki_accessible'(X8,X10) )
| ? [X9: '$ki_world'] :
( ~ member(X9,X7,X1)
& '$ki_accessible'(X8,X9) )
| ~ '$ki_accessible'(X6,X8) )
| ~ '$ki_exists_in_world_$i'(X6,X7) )
| ~ '$ki_accessible'(X4,X6) )
| ? [X5: '$ki_world'] :
( ~ subclass(X5,X1,X3)
& '$ki_accessible'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
& ! [X11: '$ki_world'] :
( ! [X17: '$ki_world'] :
( subclass(X17,X1,X3)
| ~ '$ki_accessible'(X11,X17) )
| ? [X12: '$ki_world'] :
( ? [X13: $i] :
( ? [X14: '$ki_world'] :
( ? [X16: '$ki_world'] :
( ~ member(X16,X13,X3)
& '$ki_accessible'(X14,X16) )
& ! [X15: '$ki_world'] :
( member(X15,X13,X1)
| ~ '$ki_accessible'(X14,X15) )
& '$ki_accessible'(X12,X14) )
& '$ki_exists_in_world_$i'(X12,X13) )
& '$ki_accessible'(X11,X12) )
| ~ '$ki_accessible'(X2,X11) ) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(flattening,[],[f241]) ).
tff(f307,plain,
? [X0: '$ki_world'] :
( ? [X1: $i] :
( ? [X2: '$ki_world'] :
( ~ subclass(X2,X1,X1)
& '$ki_accessible'(X0,X2) )
& '$ki_exists_in_world_$i'(X0,X1) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f89]) ).
tff(f308,definition,
! [X3: $i,X1: $i,X2: '$ki_world'] :
( ! [X11: '$ki_world'] :
( ! [X17: '$ki_world'] :
( subclass(X17,X1,X3)
| ~ '$ki_accessible'(X11,X17) )
| ? [X12: '$ki_world'] :
( ? [X13: $i] :
( ? [X14: '$ki_world'] :
( ? [X16: '$ki_world'] :
( ~ member(X16,X13,X3)
& '$ki_accessible'(X14,X16) )
& ! [X15: '$ki_world'] :
( member(X15,X13,X1)
| ~ '$ki_accessible'(X14,X15) )
& '$ki_accessible'(X12,X14) )
& '$ki_exists_in_world_$i'(X12,X13) )
& '$ki_accessible'(X11,X12) )
| ~ '$ki_accessible'(X2,X11) )
| ~ sP0(X3,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f309,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ( ! [X4: '$ki_world'] :
( ! [X6: '$ki_world'] :
( ! [X7: $i] :
( ! [X8: '$ki_world'] :
( ! [X10: '$ki_world'] :
( member(X10,X7,X3)
| ~ '$ki_accessible'(X8,X10) )
| ? [X9: '$ki_world'] :
( ~ member(X9,X7,X1)
& '$ki_accessible'(X8,X9) )
| ~ '$ki_accessible'(X6,X8) )
| ~ '$ki_exists_in_world_$i'(X6,X7) )
| ~ '$ki_accessible'(X4,X6) )
| ? [X5: '$ki_world'] :
( ~ subclass(X5,X1,X3)
& '$ki_accessible'(X4,X5) )
| ~ '$ki_accessible'(X2,X4) )
& sP0(X3,X1,X2) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(definition_folding,[],[f242,f308]) ).
tff(f405,plain,
! [X3: $i,X1: $i,X2: '$ki_world'] :
( ! [X11: '$ki_world'] :
( ! [X17: '$ki_world'] :
( subclass(X17,X1,X3)
| ~ '$ki_accessible'(X11,X17) )
| ? [X12: '$ki_world'] :
( ? [X13: $i] :
( ? [X14: '$ki_world'] :
( ? [X16: '$ki_world'] :
( ~ member(X16,X13,X3)
& '$ki_accessible'(X14,X16) )
& ! [X15: '$ki_world'] :
( member(X15,X13,X1)
| ~ '$ki_accessible'(X14,X15) )
& '$ki_accessible'(X12,X14) )
& '$ki_exists_in_world_$i'(X12,X13) )
& '$ki_accessible'(X11,X12) )
| ~ '$ki_accessible'(X2,X11) )
| ~ sP0(X3,X1,X2) ),
inference(nnf_transformation,[],[f308]) ).
tff(f406,plain,
! [X0: $i,X1: $i,X2: '$ki_world'] :
( ! [X3: '$ki_world'] :
( ! [X4: '$ki_world'] :
( subclass(X4,X1,X0)
| ~ '$ki_accessible'(X3,X4) )
| ? [X5: '$ki_world'] :
( ? [X6: $i] :
( ? [X7: '$ki_world'] :
( ? [X8: '$ki_world'] :
( ~ member(X8,X6,X0)
& '$ki_accessible'(X7,X8) )
& ! [X9: '$ki_world'] :
( member(X9,X6,X1)
| ~ '$ki_accessible'(X7,X9) )
& '$ki_accessible'(X5,X7) )
& '$ki_exists_in_world_$i'(X5,X6) )
& '$ki_accessible'(X3,X5) )
| ~ '$ki_accessible'(X2,X3) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f405]) ).
tff(f407,plain,
! [X0: $i,X1: $i,X2: '$ki_world'] :
( ! [X3: '$ki_world'] :
( ! [X4: '$ki_world'] :
( subclass(X4,X1,X0)
| ~ '$ki_accessible'(X3,X4) )
| ( ~ member(sK61(X0,X1,X3),sK59(X0,X1,X3),X0)
& '$ki_accessible'(sK60(X0,X1,X3),sK61(X0,X1,X3))
& ! [X9: '$ki_world'] :
( member(X9,sK59(X0,X1,X3),X1)
| ~ '$ki_accessible'(sK60(X0,X1,X3),X9) )
& '$ki_accessible'(sK58(X0,X1,X3),sK60(X0,X1,X3))
& '$ki_exists_in_world_$i'(sK58(X0,X1,X3),sK59(X0,X1,X3))
& '$ki_accessible'(X3,sK58(X0,X1,X3)) )
| ~ '$ki_accessible'(X2,X3) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58,sK59,sK60,sK61]),skolemize(X5,sK58(X0,X1,X3)),skolemize(X6,sK59(X0,X1,X3)),skolemize(X7,sK60(X0,X1,X3)),skolemize(X8,sK61(X0,X1,X3))],[f406]) ).
tff(f408,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ( ! [X4: '$ki_world'] :
( ! [X5: '$ki_world'] :
( ! [X6: $i] :
( ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( member(X8,X6,X3)
| ~ '$ki_accessible'(X7,X8) )
| ? [X9: '$ki_world'] :
( ~ member(X9,X6,X1)
& '$ki_accessible'(X7,X9) )
| ~ '$ki_accessible'(X5,X7) )
| ~ '$ki_exists_in_world_$i'(X5,X6) )
| ~ '$ki_accessible'(X4,X5) )
| ? [X10: '$ki_world'] :
( ~ subclass(X10,X1,X3)
& '$ki_accessible'(X4,X10) )
| ~ '$ki_accessible'(X2,X4) )
& sP0(X3,X1,X2) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(rectify,[],[f309]) ).
tff(f409,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: '$ki_world'] :
( ! [X3: $i] :
( ( ! [X4: '$ki_world'] :
( ! [X5: '$ki_world'] :
( ! [X6: $i] :
( ! [X7: '$ki_world'] :
( ! [X8: '$ki_world'] :
( member(X8,X6,X3)
| ~ '$ki_accessible'(X7,X8) )
| ( ~ member(sK62(X1,X6,X7),X6,X1)
& '$ki_accessible'(X7,sK62(X1,X6,X7)) )
| ~ '$ki_accessible'(X5,X7) )
| ~ '$ki_exists_in_world_$i'(X5,X6) )
| ~ '$ki_accessible'(X4,X5) )
| ( ~ subclass(sK63(X1,X3,X4),X1,X3)
& '$ki_accessible'(X4,sK63(X1,X3,X4)) )
| ~ '$ki_accessible'(X2,X4) )
& sP0(X3,X1,X2) )
| ~ '$ki_exists_in_world_$i'(X2,X3) )
| ~ '$ki_accessible'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62,sK63]),skolemize(X9,sK62(X1,X6,X7)),skolemize(X10,sK63(X1,X3,X4))],[f408]) ).
tff(f477,plain,
( ~ subclass(sK137,sK136,sK136)
& '$ki_accessible'(sK135,sK137)
& '$ki_exists_in_world_$i'(sK135,sK136)
& '$ki_accessible'('$ki_local_world',sK135) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK135,sK136,sK137]),skolemize(X0,sK135),skolemize(X1,sK136),skolemize(X2,sK137)],[f307]) ).
tff(f478,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f480,plain,
! [X0: '$ki_world',X1: $i] : '$ki_exists_in_world_$i'(X0,X1),
inference(cnf_transformation,[],[f3]) ).
tff(f586,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X9: '$ki_world',X4: '$ki_world'] :
( subclass(X4,X1,X0)
| ~ '$ki_accessible'(X3,X4)
| member(X9,sK59(X0,X1,X3),X1)
| ~ '$ki_accessible'(sK60(X0,X1,X3),X9)
| ~ '$ki_accessible'(X2,X3)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f407]) ).
tff(f587,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X4: '$ki_world'] :
( subclass(X4,X1,X0)
| ~ '$ki_accessible'(X3,X4)
| '$ki_accessible'(sK60(X0,X1,X3),sK61(X0,X1,X3))
| ~ '$ki_accessible'(X2,X3)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f407]) ).
tff(f588,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X4: '$ki_world'] :
( subclass(X4,X1,X0)
| ~ '$ki_accessible'(X3,X4)
| ~ member(sK61(X0,X1,X3),sK59(X0,X1,X3),X0)
| ~ '$ki_accessible'(X2,X3)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f407]) ).
tff(f589,plain,
! [X2: '$ki_world',X3: $i,X0: '$ki_world',X1: $i] :
( sP0(X3,X1,X2)
| ~ '$ki_exists_in_world_$i'(X2,X3)
| ~ '$ki_accessible'(X0,X2)
| ~ '$ki_exists_in_world_$i'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f409]) ).
tff(f799,plain,
'$ki_accessible'('$ki_local_world',sK135),
inference(cnf_transformation,[],[f477]) ).
tff(f801,plain,
'$ki_accessible'(sK135,sK137),
inference(cnf_transformation,[],[f477]) ).
tff(f802,plain,
~ subclass(sK137,sK136,sK136),
inference(cnf_transformation,[],[f477]) ).
tff(f803,plain,
! [X0: '$ki_world',X1: $i] : ~ '$ki_exists_in_world_$i'(X0,X1),
inference(consistent_polarity_flipping,[],[f480]) ).
tff(f906,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X4: '$ki_world'] :
( ~ sP0(X0,X1,X2)
| ~ '$ki_accessible'(X3,X4)
| ~ member(sK61(X0,X1,X3),sK59(X0,X1,X3),X0)
| ~ '$ki_accessible'(X2,X3)
| ~ subclass(X4,X1,X0) ),
inference(consistent_polarity_flipping,[],[f588]) ).
tff(f907,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X4: '$ki_world'] :
( '$ki_accessible'(sK60(X0,X1,X3),sK61(X0,X1,X3))
| ~ '$ki_accessible'(X3,X4)
| ~ subclass(X4,X1,X0)
| ~ '$ki_accessible'(X2,X3)
| ~ sP0(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f587]) ).
tff(f908,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i,X9: '$ki_world',X4: '$ki_world'] :
( member(X9,sK59(X0,X1,X3),X1)
| ~ '$ki_accessible'(X3,X4)
| ~ subclass(X4,X1,X0)
| ~ '$ki_accessible'(sK60(X0,X1,X3),X9)
| ~ '$ki_accessible'(X2,X3)
| ~ sP0(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f586]) ).
tff(f916,plain,
! [X2: '$ki_world',X3: $i,X0: '$ki_world',X1: $i] :
( '$ki_exists_in_world_$i'(X2,X3)
| sP0(X3,X1,X2)
| ~ '$ki_accessible'(X0,X2)
| '$ki_exists_in_world_$i'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(consistent_polarity_flipping,[],[f589]) ).
tff(f1105,plain,
subclass(sK137,sK136,sK136),
inference(consistent_polarity_flipping,[],[f802]) ).
tff(f1109,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: $i,X1: $i] :
( '$ki_exists_in_world_$i'(X3,X1)
| ~ '$ki_accessible'(X3,X2)
| sP0(X0,X1,X2)
| ~ '$ki_accessible'('$ki_local_world',X3) ),
inference(resolution,[],[f916,f803]) ).
tff(f1110,plain,
! [X2: $i,X3: $i,X0: '$ki_world',X1: '$ki_world'] :
( sP0(X2,X3,X1)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(resolution,[],[f1109,f803]) ).
tff(f1129,plain,
! [X2: $i,X3: $i,X0: '$ki_world',X1: '$ki_world',X4: '$ki_world',X5: '$ki_world'] :
( ~ subclass(X1,X3,X2)
| ~ member(sK61(X2,X3,X0),sK59(X2,X3,X0),X2)
| ~ '$ki_accessible'(X4,X0)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X5,X4)
| ~ '$ki_accessible'('$ki_local_world',X5) ),
inference(resolution,[],[f906,f1110]) ).
tff(f1137,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ member(sK61(sK136,sK136,X0),sK59(sK136,sK136,X0),sK136)
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'('$ki_local_world',X2) ),
inference(resolution,[],[f1129,f1105]) ).
tff(f1139,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: '$ki_world'] :
( ~ sP0(sK136,sK136,X2)
| ~ subclass(X1,sK136,sK136)
| ~ '$ki_accessible'(sK60(sK136,sK136,X0),sK61(sK136,sK136,X0))
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X3,X0)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X4,X3)
| ~ '$ki_accessible'('$ki_local_world',X4) ),
inference(resolution,[],[f908,f1137]) ).
tff(f1140,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: '$ki_world',X5: '$ki_world'] :
( ~ subclass(X0,sK136,sK136)
| ~ '$ki_accessible'(sK60(sK136,sK136,X1),sK61(sK136,sK136,X1))
| ~ '$ki_accessible'(X2,X1)
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'(X3,X1)
| ~ '$ki_accessible'(X1,sK137)
| ~ '$ki_accessible'(X4,X3)
| ~ '$ki_accessible'('$ki_local_world',X4)
| ~ '$ki_accessible'(X5,X2)
| ~ '$ki_accessible'('$ki_local_world',X5) ),
inference(resolution,[],[f1139,f1110]) ).
tff(f1141,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(sK60(sK136,sK136,X0),sK61(sK136,sK136,X0))
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'(X4,X1)
| ~ '$ki_accessible'('$ki_local_world',X4) ),
inference(resolution,[],[f1140,f1105]) ).
tff(f1142,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(sK60(sK136,sK136,X0),sK61(sK136,sK136,X0))
| ~ '$ki_accessible'(X4,X1)
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'('$ki_local_world',X3)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'('$ki_local_world',X4) ),
inference(duplicate_literal_removal,[],[f1141]) ).
tff(f1151,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK60(sK136,sK136,X2),sK61(sK136,sK136,X2))
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X1,X2)
| ~ '$ki_accessible'(X1,X2)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X2,sK137)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(factoring,[],[f1142]) ).
tff(f1155,plain,
! [X2: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK60(sK136,sK136,X2),sK61(sK136,sK136,X2))
| ~ '$ki_accessible'(X1,X2)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X2,sK137) ),
inference(duplicate_literal_removal,[],[f1151]) ).
tff(f1159,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK60(sK136,sK136,X1),sK61(sK136,sK136,X1))
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X1,sK137) ),
inference(resolution,[],[f1155,f478]) ).
tff(f1161,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ sP0(sK136,sK136,X3)
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X0,X2)
| ~ subclass(X2,sK136,sK136)
| ~ '$ki_accessible'(X3,X0)
| ~ '$ki_accessible'(X1,X0) ),
inference(resolution,[],[f1159,f907]) ).
tff(f1171,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world',X4: '$ki_world'] :
( ~ subclass(X2,sK136,sK136)
| ~ '$ki_accessible'(X1,sK137)
| ~ '$ki_accessible'(X1,X2)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X3,X1)
| ~ '$ki_accessible'(X0,X1)
| ~ '$ki_accessible'(X4,X3)
| ~ '$ki_accessible'('$ki_local_world',X4) ),
inference(resolution,[],[f1161,f1110]) ).
tff(f1237,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'('$ki_local_world',X3) ),
inference(resolution,[],[f1171,f1105]) ).
tff(f1238,plain,
! [X2: '$ki_world',X3: '$ki_world',X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'('$ki_local_world',X1)
| ~ '$ki_accessible'(X2,X0)
| ~ '$ki_accessible'(X1,X0)
| ~ '$ki_accessible'(X3,X2)
| ~ '$ki_accessible'('$ki_local_world',X3) ),
inference(duplicate_literal_removal,[],[f1237]) ).
tff(f1252,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(sK137,sK137)
| ~ '$ki_accessible'('$ki_local_world',X0)
| ~ '$ki_accessible'(X0,sK137)
| ~ '$ki_accessible'(X1,sK137)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(factoring,[],[f1238]) ).
tff(f1294,definition,
( spl138_8
<=> '$ki_accessible'(sK137,sK137) ),
introduced(definition,[new_symbols(definition,[spl138_8])],[avatar_definition]) ).
tff(f1296,plain,
( ~ '$ki_accessible'(sK137,sK137)
| spl138_8 ),
inference(avatar_component_clause,[],[f1294]) ).
tff(f1299,definition,
( spl138_9
<=> ! [X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK137)
| ~ '$ki_accessible'('$ki_local_world',X1) ) ),
introduced(definition,[new_symbols(definition,[spl138_9])],[avatar_definition]) ).
tff(f1300,plain,
( ! [X1: '$ki_world'] :
( ~ '$ki_accessible'(X1,sK137)
| ~ '$ki_accessible'('$ki_local_world',X1) )
| ~ spl138_9 ),
inference(avatar_component_clause,[],[f1299]) ).
tff(f1301,plain,
( spl138_9
| spl138_9
| ~ spl138_8 ),
inference(avatar_split_clause,[],[f1252,f1294,f1299,f1299]) ).
tff(f1316,plain,
( $false
| spl138_8 ),
inference(resolution,[],[f1296,f478]) ).
tff(f1318,plain,
spl138_8,
inference(avatar_contradiction_clause,[],[f1316]) ).
tff(f1330,plain,
( ~ '$ki_accessible'('$ki_local_world',sK135)
| ~ spl138_9 ),
inference(resolution,[],[f1300,f801]) ).
tff(f1332,plain,
( $false
| ~ spl138_9 ),
inference(resolution,[],[f1330,f799]) ).
tff(f1334,plain,
~ spl138_9,
inference(avatar_contradiction_clause,[],[f1332]) ).
cnf(s6,plain,
( spl138_9
| ~ spl138_8
| spl138_9 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s7,plain,
( ~ spl138_8
| spl138_9 ),
inference(rat,[],[s6]) ).
cnf(s12,plain,
spl138_8,
inference(sat_conversion,[],[f1318]) ).
cnf(s15,plain,
~ spl138_9,
inference(sat_conversion,[],[f1334]) ).
cnf(s21,plain,
$false,
inference(rat,[],[s7,s15,s12]) ).
tff(f1336,plain,
$false,
inference(avatar_sat_refutation,[],[s21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL949_4 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 17:07:49 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.32 Running first-order model finding
% 0.08/0.32 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.08/0.38 % (2599096)Will run a generic schedule for satisfiability detection.
% 0.08/0.38 % (2599102)% WARNING: option uhcvi not known.
% 0.08/0.38 % (2599105)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=177278859:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.38 % (2599103)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1372494729:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.38 % (2599104)dis+10_1_sil=32000:sp=arity:random_seed=2412159047:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.38 % (2599102)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=463540451:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.38 % (2599101)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3850339377_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.38 % (2599106)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2568382654:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.38 % (2599107)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=852269032:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.38 % (2599107) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2599096-2599107"...
% 0.08/0.38 % (2599107)...printing done.
% 0.08/0.38 % (2599107)Refutation found. Thanks to Tanya!
% 0.08/0.38 % SZS status Theorem for theBenchmark
% 0.08/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/0.38 % (2599107)------------------------------
% 0.08/0.38 % (2599107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.38 % (2599107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.38 % (2599107)CaDiCaL version: 2.1.3
% 0.08/0.38 % (2599107)Termination reason: Refutation
% 0.08/0.38 % (2599107)Time elapsed: 0.023 s
% 0.08/0.38 % (2599107)Peak memory usage: 14 MB
% 0.08/0.38 % (2599107)Instructions burned: 79 (million)
% 0.08/0.38 % (2599096)Success in time 0.053 s
% 0.08/0.38 % Vampire exiting
%------------------------------------------------------------------------------