%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL941_5 : 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 : 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 11:57:14 AM UTC 2026
% Result : Theorem 3.94s 1.54s
% Output : Refutation 4.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 36
% Syntax : Number of formulae : 219 ( 12 unt; 0 typ; 34 def)
% Number of atoms : 2236 ( 0 equ)
% Maximal formula atoms : 65 ( 10 avg)
% Number of connectives : 1156 ( 387 ~; 435 |; 208 &)
% ( 27 <=>; 99 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 1248 (1248 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 43 ( 42 usr; 36 prp; 0-3 aty)
% Number of functors : 101 ( 101 usr; 18 con; 0-3 aty)
% Number of variables : 279 ( 0 sgn 224 !; 55 ?; 279 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_8,type,
sK7: '$ki_world' > $i ).
tff(func_def_9,type,
sK8: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_10,type,
sK9: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_11,type,
sK10: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_12,type,
sK11: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_13,type,
sK12: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_14,type,
sK13: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_15,type,
sK14: '$ki_world' > '$ki_world' ).
tff(func_def_16,type,
sK15: '$ki_world' > '$ki_world' ).
tff(func_def_17,type,
sK16: '$ki_world' > '$ki_world' ).
tff(func_def_18,type,
sK17: '$ki_world' > '$ki_world' ).
tff(func_def_19,type,
sK18: '$ki_world' > '$ki_world' ).
tff(func_def_20,type,
sK19: '$ki_world' > '$ki_world' ).
tff(func_def_21,type,
sK20: '$ki_world' > '$ki_world' ).
tff(func_def_22,type,
sK21: '$ki_world' > '$ki_world' ).
tff(func_def_23,type,
sK22: '$ki_world' > '$ki_world' ).
tff(func_def_24,type,
sK23: '$ki_world' > '$ki_world' ).
tff(func_def_25,type,
sK24: '$ki_world' > '$ki_world' ).
tff(func_def_26,type,
sK25: '$ki_world' > '$ki_world' ).
tff(func_def_27,type,
sK26: '$ki_world' > '$ki_world' ).
tff(func_def_28,type,
sK27: '$ki_world' > '$ki_world' ).
tff(func_def_29,type,
sK28: '$ki_world' > '$ki_world' ).
tff(func_def_30,type,
sK29: '$ki_world' > '$ki_world' ).
tff(func_def_31,type,
sK30: '$ki_world' > '$ki_world' ).
tff(func_def_32,type,
sK31: '$ki_world' > '$ki_world' ).
tff(func_def_33,type,
sK32: '$ki_world' > '$ki_world' ).
tff(func_def_34,type,
sK33: '$ki_world' > '$ki_world' ).
tff(func_def_35,type,
sK34: '$ki_world' > '$ki_world' ).
tff(func_def_36,type,
sK35: '$ki_world' > '$ki_world' ).
tff(func_def_37,type,
sK36: '$ki_world' > '$ki_world' ).
tff(func_def_38,type,
sK37: '$ki_world' > '$ki_world' ).
tff(func_def_39,type,
sK38: '$ki_world' > '$ki_world' ).
tff(func_def_40,type,
sK39: '$ki_world' > '$ki_world' ).
tff(func_def_41,type,
sK40: '$ki_world' > '$ki_world' ).
tff(func_def_42,type,
sK41: '$ki_world' > '$ki_world' ).
tff(func_def_43,type,
sK42: '$ki_world' > '$ki_world' ).
tff(func_def_44,type,
sK43: '$ki_world' > '$ki_world' ).
tff(func_def_45,type,
sK44: '$ki_world' > '$ki_world' ).
tff(func_def_46,type,
sK45: '$ki_world' > '$ki_world' ).
tff(func_def_47,type,
sK46: '$ki_world' > '$ki_world' ).
tff(func_def_48,type,
sK47: '$ki_world' > '$ki_world' ).
tff(func_def_49,type,
sK48: '$ki_world' > '$ki_world' ).
tff(func_def_50,type,
sK49: '$ki_world' > '$ki_world' ).
tff(func_def_51,type,
sK50: '$ki_world' > '$ki_world' ).
tff(func_def_52,type,
sK51: '$ki_world' > '$ki_world' ).
tff(func_def_53,type,
sK52: '$ki_world' > '$ki_world' ).
tff(func_def_54,type,
sK53: '$ki_world' > '$ki_world' ).
tff(func_def_55,type,
sK54: '$ki_world' > '$ki_world' ).
tff(func_def_56,type,
sK55: '$ki_world' > '$ki_world' ).
tff(func_def_57,type,
sK56: '$ki_world' > '$ki_world' ).
tff(func_def_58,type,
sK57: '$ki_world' > '$ki_world' ).
tff(func_def_59,type,
sK58: '$ki_world' > '$ki_world' ).
tff(func_def_60,type,
sK59: '$ki_world' > '$ki_world' ).
tff(func_def_61,type,
sK60: '$ki_world' > '$ki_world' ).
tff(func_def_62,type,
sK61: '$ki_world' > '$ki_world' ).
tff(func_def_63,type,
sK62: '$ki_world' > '$ki_world' ).
tff(func_def_64,type,
sK63: '$ki_world' > '$ki_world' ).
tff(func_def_65,type,
sK64: '$ki_world' > '$ki_world' ).
tff(func_def_66,type,
sK65: '$ki_world' > '$ki_world' ).
tff(func_def_67,type,
sK66: '$ki_world' > '$ki_world' ).
tff(func_def_68,type,
sK67: '$ki_world' > '$ki_world' ).
tff(func_def_69,type,
sK68: '$ki_world' > '$ki_world' ).
tff(func_def_70,type,
sK69: '$ki_world' > '$ki_world' ).
tff(func_def_71,type,
sK70: '$ki_world' > '$ki_world' ).
tff(func_def_72,type,
sK71: '$ki_world' > '$ki_world' ).
tff(func_def_73,type,
sK72: '$ki_world' > '$ki_world' ).
tff(func_def_74,type,
sK73: '$ki_world' > '$ki_world' ).
tff(func_def_75,type,
sK74: '$ki_world' > '$ki_world' ).
tff(func_def_76,type,
sK75: '$ki_world' > '$ki_world' ).
tff(func_def_77,type,
sK76: '$ki_world' > '$ki_world' ).
tff(func_def_78,type,
sK77: '$ki_world' > '$ki_world' ).
tff(func_def_79,type,
sK78: '$ki_world' > '$ki_world' ).
tff(func_def_80,type,
sK79: '$ki_world' > '$ki_world' ).
tff(func_def_81,type,
sK80: '$ki_world' > '$ki_world' ).
tff(func_def_82,type,
sK81: '$ki_world' > '$ki_world' ).
tff(func_def_83,type,
sK82: '$ki_world' > '$ki_world' ).
tff(func_def_84,type,
sK83: '$ki_world' > '$ki_world' ).
tff(func_def_85,type,
sK84: '$ki_world' > '$ki_world' ).
tff(func_def_86,type,
sK85: '$ki_world' > '$ki_world' ).
tff(func_def_87,type,
sK86: '$ki_world' > '$ki_world' ).
tff(func_def_88,type,
sK87: '$ki_world' > '$ki_world' ).
tff(func_def_89,type,
sK88: '$ki_world' > '$ki_world' ).
tff(func_def_90,type,
sK89: '$ki_world' > '$ki_world' ).
tff(func_def_91,type,
sK90: '$ki_world' ).
tff(func_def_92,type,
sK91: '$ki_world' ).
tff(func_def_93,type,
sK92: '$ki_world' ).
tff(func_def_94,type,
sK93: '$ki_world' ).
tff(func_def_95,type,
sK94: '$ki_world' ).
tff(func_def_96,type,
sK95: '$ki_world' ).
tff(func_def_97,type,
sK96: '$ki_world' ).
tff(func_def_98,type,
sK97: '$ki_world' ).
tff(func_def_99,type,
sK98: '$ki_world' ).
tff(func_def_100,type,
sK99: '$ki_world' ).
tff(func_def_101,type,
sK100: '$ki_world' ).
tff(func_def_102,type,
sK101: '$ki_world' ).
tff(func_def_103,type,
sK102: '$ki_world' ).
tff(func_def_104,type,
sK103: '$ki_world' ).
tff(func_def_105,type,
sK104: '$ki_world' ).
tff(func_def_106,type,
sK105: '$ki_world' ).
tff(func_def_107,type,
sK106: '$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,
'$ki_exists_in_world_$i': ( '$ki_world' * $i ) > $o ).
tff(pred_def_4,type,
sP0: '$ki_world' > $o ).
tff(pred_def_5,type,
sP1: '$ki_world' > $o ).
tff(pred_def_6,type,
sP2: '$ki_world' > $o ).
tff(f1,axiom,
! [X0: '$ki_world',X1: '$ki_world'] : '$ki_accessible'(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_universal) ).
tff(f21,conjecture,
( ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e0) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e1) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e2) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e3) ) )
| ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ~ ( ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e0) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e1) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e2) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',verify) ).
tff(f22,negated_conjecture,
~ ( ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e0) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e0) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e1) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e1) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e2) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e2) ) )
| ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e1,e1),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e2,e2),e3) )
& ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e3,e3),e3) ) )
| ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ~ ( ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e0) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e1) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e1) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e2) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e2) ) )
| ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e1,e1),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e2,e2),e3) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e3,e3),e3) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f21]) ).
tff(f37,plain,
~ ( ( ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> qmltpeq(X0,op(e0,e0),e0) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X1)
=> qmltpeq(X1,op(e1,e1),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X2)
=> qmltpeq(X2,op(e2,e2),e0) )
& ! [X3: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X3)
=> qmltpeq(X3,op(e3,e3),e0) ) )
| ( ! [X4: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X4)
=> qmltpeq(X4,op(e0,e0),e1) )
& ! [X5: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X5)
=> qmltpeq(X5,op(e1,e1),e1) )
& ! [X6: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X6)
=> qmltpeq(X6,op(e2,e2),e1) )
& ! [X7: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X7)
=> qmltpeq(X7,op(e3,e3),e1) ) )
| ( ! [X8: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X8)
=> qmltpeq(X8,op(e0,e0),e2) )
& ! [X9: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X9)
=> qmltpeq(X9,op(e1,e1),e2) )
& ! [X10: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X10)
=> qmltpeq(X10,op(e2,e2),e2) )
& ! [X11: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X11)
=> qmltpeq(X11,op(e3,e3),e2) ) )
| ( ! [X12: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X12)
=> qmltpeq(X12,op(e0,e0),e3) )
& ! [X13: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X13)
=> qmltpeq(X13,op(e1,e1),e3) )
& ! [X14: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X14)
=> qmltpeq(X14,op(e2,e2),e3) )
& ! [X15: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X15)
=> qmltpeq(X15,op(e3,e3),e3) ) )
| ! [X16: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X16)
=> ~ ( ( ! [X17: '$ki_world'] :
( '$ki_accessible'(X16,X17)
=> qmltpeq(X17,op(e0,e0),e0) )
& ! [X18: '$ki_world'] :
( '$ki_accessible'(X16,X18)
=> qmltpeq(X18,op(e1,e1),e0) )
& ! [X19: '$ki_world'] :
( '$ki_accessible'(X16,X19)
=> qmltpeq(X19,op(e2,e2),e0) )
& ! [X20: '$ki_world'] :
( '$ki_accessible'(X16,X20)
=> qmltpeq(X20,op(e3,e3),e0) ) )
| ( ! [X21: '$ki_world'] :
( '$ki_accessible'(X16,X21)
=> qmltpeq(X21,op(e0,e0),e1) )
& ! [X22: '$ki_world'] :
( '$ki_accessible'(X16,X22)
=> qmltpeq(X22,op(e1,e1),e1) )
& ! [X23: '$ki_world'] :
( '$ki_accessible'(X16,X23)
=> qmltpeq(X23,op(e2,e2),e1) )
& ! [X24: '$ki_world'] :
( '$ki_accessible'(X16,X24)
=> qmltpeq(X24,op(e3,e3),e1) ) )
| ( ! [X25: '$ki_world'] :
( '$ki_accessible'(X16,X25)
=> qmltpeq(X25,op(e0,e0),e2) )
& ! [X26: '$ki_world'] :
( '$ki_accessible'(X16,X26)
=> qmltpeq(X26,op(e1,e1),e2) )
& ! [X27: '$ki_world'] :
( '$ki_accessible'(X16,X27)
=> qmltpeq(X27,op(e2,e2),e2) )
& ! [X28: '$ki_world'] :
( '$ki_accessible'(X16,X28)
=> qmltpeq(X28,op(e3,e3),e2) ) )
| ( ! [X29: '$ki_world'] :
( '$ki_accessible'(X16,X29)
=> qmltpeq(X29,op(e0,e0),e3) )
& ! [X30: '$ki_world'] :
( '$ki_accessible'(X16,X30)
=> qmltpeq(X30,op(e1,e1),e3) )
& ! [X31: '$ki_world'] :
( '$ki_accessible'(X16,X31)
=> qmltpeq(X31,op(e2,e2),e3) )
& ! [X32: '$ki_world'] :
( '$ki_accessible'(X16,X32)
=> qmltpeq(X32,op(e3,e3),e3) ) ) ) ) ),
inference(rectify,[],[f22]) ).
tff(f61,plain,
( ( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e0,e0),e0)
& '$ki_accessible'('$ki_local_world',X0) )
| ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e1,e1),e0)
& '$ki_accessible'('$ki_local_world',X1) )
| ? [X2: '$ki_world'] :
( ~ qmltpeq(X2,op(e2,e2),e0)
& '$ki_accessible'('$ki_local_world',X2) )
| ? [X3: '$ki_world'] :
( ~ qmltpeq(X3,op(e3,e3),e0)
& '$ki_accessible'('$ki_local_world',X3) ) )
& ( ? [X4: '$ki_world'] :
( ~ qmltpeq(X4,op(e0,e0),e1)
& '$ki_accessible'('$ki_local_world',X4) )
| ? [X5: '$ki_world'] :
( ~ qmltpeq(X5,op(e1,e1),e1)
& '$ki_accessible'('$ki_local_world',X5) )
| ? [X6: '$ki_world'] :
( ~ qmltpeq(X6,op(e2,e2),e1)
& '$ki_accessible'('$ki_local_world',X6) )
| ? [X7: '$ki_world'] :
( ~ qmltpeq(X7,op(e3,e3),e1)
& '$ki_accessible'('$ki_local_world',X7) ) )
& ( ? [X8: '$ki_world'] :
( ~ qmltpeq(X8,op(e0,e0),e2)
& '$ki_accessible'('$ki_local_world',X8) )
| ? [X9: '$ki_world'] :
( ~ qmltpeq(X9,op(e1,e1),e2)
& '$ki_accessible'('$ki_local_world',X9) )
| ? [X10: '$ki_world'] :
( ~ qmltpeq(X10,op(e2,e2),e2)
& '$ki_accessible'('$ki_local_world',X10) )
| ? [X11: '$ki_world'] :
( ~ qmltpeq(X11,op(e3,e3),e2)
& '$ki_accessible'('$ki_local_world',X11) ) )
& ( ? [X12: '$ki_world'] :
( ~ qmltpeq(X12,op(e0,e0),e3)
& '$ki_accessible'('$ki_local_world',X12) )
| ? [X13: '$ki_world'] :
( ~ qmltpeq(X13,op(e1,e1),e3)
& '$ki_accessible'('$ki_local_world',X13) )
| ? [X14: '$ki_world'] :
( ~ qmltpeq(X14,op(e2,e2),e3)
& '$ki_accessible'('$ki_local_world',X14) )
| ? [X15: '$ki_world'] :
( ~ qmltpeq(X15,op(e3,e3),e3)
& '$ki_accessible'('$ki_local_world',X15) ) )
& ? [X16: '$ki_world'] :
( ( ( ! [X17: '$ki_world'] :
( qmltpeq(X17,op(e0,e0),e0)
| ~ '$ki_accessible'(X16,X17) )
& ! [X18: '$ki_world'] :
( qmltpeq(X18,op(e1,e1),e0)
| ~ '$ki_accessible'(X16,X18) )
& ! [X19: '$ki_world'] :
( qmltpeq(X19,op(e2,e2),e0)
| ~ '$ki_accessible'(X16,X19) )
& ! [X20: '$ki_world'] :
( qmltpeq(X20,op(e3,e3),e0)
| ~ '$ki_accessible'(X16,X20) ) )
| ( ! [X21: '$ki_world'] :
( qmltpeq(X21,op(e0,e0),e1)
| ~ '$ki_accessible'(X16,X21) )
& ! [X22: '$ki_world'] :
( qmltpeq(X22,op(e1,e1),e1)
| ~ '$ki_accessible'(X16,X22) )
& ! [X23: '$ki_world'] :
( qmltpeq(X23,op(e2,e2),e1)
| ~ '$ki_accessible'(X16,X23) )
& ! [X24: '$ki_world'] :
( qmltpeq(X24,op(e3,e3),e1)
| ~ '$ki_accessible'(X16,X24) ) )
| ( ! [X25: '$ki_world'] :
( qmltpeq(X25,op(e0,e0),e2)
| ~ '$ki_accessible'(X16,X25) )
& ! [X26: '$ki_world'] :
( qmltpeq(X26,op(e1,e1),e2)
| ~ '$ki_accessible'(X16,X26) )
& ! [X27: '$ki_world'] :
( qmltpeq(X27,op(e2,e2),e2)
| ~ '$ki_accessible'(X16,X27) )
& ! [X28: '$ki_world'] :
( qmltpeq(X28,op(e3,e3),e2)
| ~ '$ki_accessible'(X16,X28) ) )
| ( ! [X29: '$ki_world'] :
( qmltpeq(X29,op(e0,e0),e3)
| ~ '$ki_accessible'(X16,X29) )
& ! [X30: '$ki_world'] :
( qmltpeq(X30,op(e1,e1),e3)
| ~ '$ki_accessible'(X16,X30) )
& ! [X31: '$ki_world'] :
( qmltpeq(X31,op(e2,e2),e3)
| ~ '$ki_accessible'(X16,X31) )
& ! [X32: '$ki_world'] :
( qmltpeq(X32,op(e3,e3),e3)
| ~ '$ki_accessible'(X16,X32) ) ) )
& '$ki_accessible'('$ki_local_world',X16) ) ),
inference(ennf_transformation,[],[f37]) ).
tff(f62,definition,
! [X16: '$ki_world'] :
( ( ! [X29: '$ki_world'] :
( qmltpeq(X29,op(e0,e0),e3)
| ~ '$ki_accessible'(X16,X29) )
& ! [X30: '$ki_world'] :
( qmltpeq(X30,op(e1,e1),e3)
| ~ '$ki_accessible'(X16,X30) )
& ! [X31: '$ki_world'] :
( qmltpeq(X31,op(e2,e2),e3)
| ~ '$ki_accessible'(X16,X31) )
& ! [X32: '$ki_world'] :
( qmltpeq(X32,op(e3,e3),e3)
| ~ '$ki_accessible'(X16,X32) ) )
| ~ sP0(X16) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f63,definition,
! [X16: '$ki_world'] :
( ( ! [X25: '$ki_world'] :
( qmltpeq(X25,op(e0,e0),e2)
| ~ '$ki_accessible'(X16,X25) )
& ! [X26: '$ki_world'] :
( qmltpeq(X26,op(e1,e1),e2)
| ~ '$ki_accessible'(X16,X26) )
& ! [X27: '$ki_world'] :
( qmltpeq(X27,op(e2,e2),e2)
| ~ '$ki_accessible'(X16,X27) )
& ! [X28: '$ki_world'] :
( qmltpeq(X28,op(e3,e3),e2)
| ~ '$ki_accessible'(X16,X28) ) )
| ~ sP1(X16) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f64,definition,
! [X16: '$ki_world'] :
( ( ! [X21: '$ki_world'] :
( qmltpeq(X21,op(e0,e0),e1)
| ~ '$ki_accessible'(X16,X21) )
& ! [X22: '$ki_world'] :
( qmltpeq(X22,op(e1,e1),e1)
| ~ '$ki_accessible'(X16,X22) )
& ! [X23: '$ki_world'] :
( qmltpeq(X23,op(e2,e2),e1)
| ~ '$ki_accessible'(X16,X23) )
& ! [X24: '$ki_world'] :
( qmltpeq(X24,op(e3,e3),e1)
| ~ '$ki_accessible'(X16,X24) ) )
| ~ sP2(X16) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f65,definition,
( ? [X15: '$ki_world'] :
( ~ qmltpeq(X15,op(e3,e3),e3)
& '$ki_accessible'('$ki_local_world',X15) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f66,definition,
( ? [X11: '$ki_world'] :
( ~ qmltpeq(X11,op(e3,e3),e2)
& '$ki_accessible'('$ki_local_world',X11) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
tff(f67,definition,
( ? [X7: '$ki_world'] :
( ~ qmltpeq(X7,op(e3,e3),e1)
& '$ki_accessible'('$ki_local_world',X7) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
tff(f68,definition,
( ? [X3: '$ki_world'] :
( ~ qmltpeq(X3,op(e3,e3),e0)
& '$ki_accessible'('$ki_local_world',X3) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
tff(f69,plain,
( ( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e0,e0),e0)
& '$ki_accessible'('$ki_local_world',X0) )
| ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e1,e1),e0)
& '$ki_accessible'('$ki_local_world',X1) )
| ? [X2: '$ki_world'] :
( ~ qmltpeq(X2,op(e2,e2),e0)
& '$ki_accessible'('$ki_local_world',X2) )
| sP6 )
& ( ? [X4: '$ki_world'] :
( ~ qmltpeq(X4,op(e0,e0),e1)
& '$ki_accessible'('$ki_local_world',X4) )
| ? [X5: '$ki_world'] :
( ~ qmltpeq(X5,op(e1,e1),e1)
& '$ki_accessible'('$ki_local_world',X5) )
| ? [X6: '$ki_world'] :
( ~ qmltpeq(X6,op(e2,e2),e1)
& '$ki_accessible'('$ki_local_world',X6) )
| sP5 )
& ( ? [X8: '$ki_world'] :
( ~ qmltpeq(X8,op(e0,e0),e2)
& '$ki_accessible'('$ki_local_world',X8) )
| ? [X9: '$ki_world'] :
( ~ qmltpeq(X9,op(e1,e1),e2)
& '$ki_accessible'('$ki_local_world',X9) )
| ? [X10: '$ki_world'] :
( ~ qmltpeq(X10,op(e2,e2),e2)
& '$ki_accessible'('$ki_local_world',X10) )
| sP4 )
& ( ? [X12: '$ki_world'] :
( ~ qmltpeq(X12,op(e0,e0),e3)
& '$ki_accessible'('$ki_local_world',X12) )
| ? [X13: '$ki_world'] :
( ~ qmltpeq(X13,op(e1,e1),e3)
& '$ki_accessible'('$ki_local_world',X13) )
| ? [X14: '$ki_world'] :
( ~ qmltpeq(X14,op(e2,e2),e3)
& '$ki_accessible'('$ki_local_world',X14) )
| sP3 )
& ? [X16: '$ki_world'] :
( ( ( ! [X17: '$ki_world'] :
( qmltpeq(X17,op(e0,e0),e0)
| ~ '$ki_accessible'(X16,X17) )
& ! [X18: '$ki_world'] :
( qmltpeq(X18,op(e1,e1),e0)
| ~ '$ki_accessible'(X16,X18) )
& ! [X19: '$ki_world'] :
( qmltpeq(X19,op(e2,e2),e0)
| ~ '$ki_accessible'(X16,X19) )
& ! [X20: '$ki_world'] :
( qmltpeq(X20,op(e3,e3),e0)
| ~ '$ki_accessible'(X16,X20) ) )
| sP2(X16)
| sP1(X16)
| sP0(X16) )
& '$ki_accessible'('$ki_local_world',X16) ) ),
inference(definition_folding,[],[f61,f68,f67,f66,f65,f64,f63,f62]) ).
tff(f86,plain,
( ? [X3: '$ki_world'] :
( ~ qmltpeq(X3,op(e3,e3),e0)
& '$ki_accessible'('$ki_local_world',X3) )
| ~ sP6 ),
inference(nnf_transformation,[],[f68]) ).
tff(f87,plain,
( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e3,e3),e0)
& '$ki_accessible'('$ki_local_world',X0) )
| ~ sP6 ),
inference(rectify,[],[f86]) ).
tff(f88,plain,
( ( ~ qmltpeq(sK90,op(e3,e3),e0)
& '$ki_accessible'('$ki_local_world',sK90) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK90]),skolemize(X0,sK90)],[f87]) ).
tff(f89,plain,
( ? [X7: '$ki_world'] :
( ~ qmltpeq(X7,op(e3,e3),e1)
& '$ki_accessible'('$ki_local_world',X7) )
| ~ sP5 ),
inference(nnf_transformation,[],[f67]) ).
tff(f90,plain,
( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e3,e3),e1)
& '$ki_accessible'('$ki_local_world',X0) )
| ~ sP5 ),
inference(rectify,[],[f89]) ).
tff(f91,plain,
( ( ~ qmltpeq(sK91,op(e3,e3),e1)
& '$ki_accessible'('$ki_local_world',sK91) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91]),skolemize(X0,sK91)],[f90]) ).
tff(f92,plain,
( ? [X11: '$ki_world'] :
( ~ qmltpeq(X11,op(e3,e3),e2)
& '$ki_accessible'('$ki_local_world',X11) )
| ~ sP4 ),
inference(nnf_transformation,[],[f66]) ).
tff(f93,plain,
( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e3,e3),e2)
& '$ki_accessible'('$ki_local_world',X0) )
| ~ sP4 ),
inference(rectify,[],[f92]) ).
tff(f94,plain,
( ( ~ qmltpeq(sK92,op(e3,e3),e2)
& '$ki_accessible'('$ki_local_world',sK92) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92]),skolemize(X0,sK92)],[f93]) ).
tff(f95,plain,
( ? [X15: '$ki_world'] :
( ~ qmltpeq(X15,op(e3,e3),e3)
& '$ki_accessible'('$ki_local_world',X15) )
| ~ sP3 ),
inference(nnf_transformation,[],[f65]) ).
tff(f96,plain,
( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e3,e3),e3)
& '$ki_accessible'('$ki_local_world',X0) )
| ~ sP3 ),
inference(rectify,[],[f95]) ).
tff(f97,plain,
( ( ~ qmltpeq(sK93,op(e3,e3),e3)
& '$ki_accessible'('$ki_local_world',sK93) )
| ~ sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93]),skolemize(X0,sK93)],[f96]) ).
tff(f98,plain,
! [X16: '$ki_world'] :
( ( ! [X21: '$ki_world'] :
( qmltpeq(X21,op(e0,e0),e1)
| ~ '$ki_accessible'(X16,X21) )
& ! [X22: '$ki_world'] :
( qmltpeq(X22,op(e1,e1),e1)
| ~ '$ki_accessible'(X16,X22) )
& ! [X23: '$ki_world'] :
( qmltpeq(X23,op(e2,e2),e1)
| ~ '$ki_accessible'(X16,X23) )
& ! [X24: '$ki_world'] :
( qmltpeq(X24,op(e3,e3),e1)
| ~ '$ki_accessible'(X16,X24) ) )
| ~ sP2(X16) ),
inference(nnf_transformation,[],[f64]) ).
tff(f99,plain,
! [X0: '$ki_world'] :
( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X4) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f98]) ).
tff(f100,plain,
! [X16: '$ki_world'] :
( ( ! [X25: '$ki_world'] :
( qmltpeq(X25,op(e0,e0),e2)
| ~ '$ki_accessible'(X16,X25) )
& ! [X26: '$ki_world'] :
( qmltpeq(X26,op(e1,e1),e2)
| ~ '$ki_accessible'(X16,X26) )
& ! [X27: '$ki_world'] :
( qmltpeq(X27,op(e2,e2),e2)
| ~ '$ki_accessible'(X16,X27) )
& ! [X28: '$ki_world'] :
( qmltpeq(X28,op(e3,e3),e2)
| ~ '$ki_accessible'(X16,X28) ) )
| ~ sP1(X16) ),
inference(nnf_transformation,[],[f63]) ).
tff(f101,plain,
! [X0: '$ki_world'] :
( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X4) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f100]) ).
tff(f102,plain,
! [X16: '$ki_world'] :
( ( ! [X29: '$ki_world'] :
( qmltpeq(X29,op(e0,e0),e3)
| ~ '$ki_accessible'(X16,X29) )
& ! [X30: '$ki_world'] :
( qmltpeq(X30,op(e1,e1),e3)
| ~ '$ki_accessible'(X16,X30) )
& ! [X31: '$ki_world'] :
( qmltpeq(X31,op(e2,e2),e3)
| ~ '$ki_accessible'(X16,X31) )
& ! [X32: '$ki_world'] :
( qmltpeq(X32,op(e3,e3),e3)
| ~ '$ki_accessible'(X16,X32) ) )
| ~ sP0(X16) ),
inference(nnf_transformation,[],[f62]) ).
tff(f103,plain,
! [X0: '$ki_world'] :
( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X4) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f102]) ).
tff(f104,plain,
( ( ? [X0: '$ki_world'] :
( ~ qmltpeq(X0,op(e0,e0),e0)
& '$ki_accessible'('$ki_local_world',X0) )
| ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e1,e1),e0)
& '$ki_accessible'('$ki_local_world',X1) )
| ? [X2: '$ki_world'] :
( ~ qmltpeq(X2,op(e2,e2),e0)
& '$ki_accessible'('$ki_local_world',X2) )
| sP6 )
& ( ? [X3: '$ki_world'] :
( ~ qmltpeq(X3,op(e0,e0),e1)
& '$ki_accessible'('$ki_local_world',X3) )
| ? [X4: '$ki_world'] :
( ~ qmltpeq(X4,op(e1,e1),e1)
& '$ki_accessible'('$ki_local_world',X4) )
| ? [X5: '$ki_world'] :
( ~ qmltpeq(X5,op(e2,e2),e1)
& '$ki_accessible'('$ki_local_world',X5) )
| sP5 )
& ( ? [X6: '$ki_world'] :
( ~ qmltpeq(X6,op(e0,e0),e2)
& '$ki_accessible'('$ki_local_world',X6) )
| ? [X7: '$ki_world'] :
( ~ qmltpeq(X7,op(e1,e1),e2)
& '$ki_accessible'('$ki_local_world',X7) )
| ? [X8: '$ki_world'] :
( ~ qmltpeq(X8,op(e2,e2),e2)
& '$ki_accessible'('$ki_local_world',X8) )
| sP4 )
& ( ? [X9: '$ki_world'] :
( ~ qmltpeq(X9,op(e0,e0),e3)
& '$ki_accessible'('$ki_local_world',X9) )
| ? [X10: '$ki_world'] :
( ~ qmltpeq(X10,op(e1,e1),e3)
& '$ki_accessible'('$ki_local_world',X10) )
| ? [X11: '$ki_world'] :
( ~ qmltpeq(X11,op(e2,e2),e3)
& '$ki_accessible'('$ki_local_world',X11) )
| sP3 )
& ? [X12: '$ki_world'] :
( ( ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(X12,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(X12,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(X12,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(X12,X16) ) )
| sP2(X12)
| sP1(X12)
| sP0(X12) )
& '$ki_accessible'('$ki_local_world',X12) ) ),
inference(rectify,[],[f69]) ).
tff(f105,plain,
( ( ( ~ qmltpeq(sK94,op(e0,e0),e0)
& '$ki_accessible'('$ki_local_world',sK94) )
| ( ~ qmltpeq(sK95,op(e1,e1),e0)
& '$ki_accessible'('$ki_local_world',sK95) )
| ( ~ qmltpeq(sK96,op(e2,e2),e0)
& '$ki_accessible'('$ki_local_world',sK96) )
| sP6 )
& ( ( ~ qmltpeq(sK97,op(e0,e0),e1)
& '$ki_accessible'('$ki_local_world',sK97) )
| ( ~ qmltpeq(sK98,op(e1,e1),e1)
& '$ki_accessible'('$ki_local_world',sK98) )
| ( ~ qmltpeq(sK99,op(e2,e2),e1)
& '$ki_accessible'('$ki_local_world',sK99) )
| sP5 )
& ( ( ~ qmltpeq(sK100,op(e0,e0),e2)
& '$ki_accessible'('$ki_local_world',sK100) )
| ( ~ qmltpeq(sK101,op(e1,e1),e2)
& '$ki_accessible'('$ki_local_world',sK101) )
| ( ~ qmltpeq(sK102,op(e2,e2),e2)
& '$ki_accessible'('$ki_local_world',sK102) )
| sP4 )
& ( ( ~ qmltpeq(sK103,op(e0,e0),e3)
& '$ki_accessible'('$ki_local_world',sK103) )
| ( ~ qmltpeq(sK104,op(e1,e1),e3)
& '$ki_accessible'('$ki_local_world',sK104) )
| ( ~ qmltpeq(sK105,op(e2,e2),e3)
& '$ki_accessible'('$ki_local_world',sK105) )
| sP3 )
& ( ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16) ) )
| sP2(sK106)
| sP1(sK106)
| sP0(sK106) )
& '$ki_accessible'('$ki_local_world',sK106) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94,sK95,sK96,sK97,sK98,sK99,sK100,sK101,sK102,sK103,sK104,sK105,sK106]),skolemize(X0,sK94),skolemize(X1,sK95),skolemize(X2,sK96),skolemize(X3,sK97),skolemize(X4,sK98),skolemize(X5,sK99),skolemize(X6,sK100),skolemize(X7,sK101),skolemize(X8,sK102),skolemize(X9,sK103),skolemize(X10,sK104),skolemize(X11,sK105),skolemize(X12,sK106)],[f104]) ).
tff(f106,plain,
! [X0: '$ki_world',X1: '$ki_world'] : '$ki_accessible'(X0,X1),
inference(cnf_transformation,[],[f1]) ).
tff(f382,plain,
( ~ qmltpeq(sK90,op(e3,e3),e0)
| ~ sP6 ),
inference(cnf_transformation,[],[f88]) ).
tff(f384,plain,
( ~ qmltpeq(sK91,op(e3,e3),e1)
| ~ sP5 ),
inference(cnf_transformation,[],[f91]) ).
tff(f386,plain,
( ~ qmltpeq(sK92,op(e3,e3),e2)
| ~ sP4 ),
inference(cnf_transformation,[],[f94]) ).
tff(f388,plain,
( ~ qmltpeq(sK93,op(e3,e3),e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f97]) ).
tff(f389,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ sP2(X0)
| ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f390,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ sP2(X0)
| ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f391,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ sP2(X0)
| ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f392,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ sP2(X0)
| ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f393,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ sP1(X0)
| ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e2) ),
inference(cnf_transformation,[],[f101]) ).
tff(f394,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ sP1(X0)
| ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e2) ),
inference(cnf_transformation,[],[f101]) ).
tff(f395,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ sP1(X0)
| ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e2) ),
inference(cnf_transformation,[],[f101]) ).
tff(f396,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ sP1(X0)
| ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e2) ),
inference(cnf_transformation,[],[f101]) ).
tff(f397,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ sP0(X0)
| ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e3) ),
inference(cnf_transformation,[],[f103]) ).
tff(f398,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ sP0(X0)
| ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e3) ),
inference(cnf_transformation,[],[f103]) ).
tff(f399,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ sP0(X0)
| ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e3) ),
inference(cnf_transformation,[],[f103]) ).
tff(f400,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ sP0(X0)
| ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e3) ),
inference(cnf_transformation,[],[f103]) ).
tff(f402,plain,
! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16)
| sP2(sK106)
| sP1(sK106)
| sP0(sK106) ),
inference(cnf_transformation,[],[f105]) ).
tff(f403,plain,
! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15)
| sP2(sK106)
| sP1(sK106)
| sP0(sK106) ),
inference(cnf_transformation,[],[f105]) ).
tff(f404,plain,
! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14)
| sP2(sK106)
| sP1(sK106)
| sP0(sK106) ),
inference(cnf_transformation,[],[f105]) ).
tff(f405,plain,
! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13)
| sP2(sK106)
| sP1(sK106)
| sP0(sK106) ),
inference(cnf_transformation,[],[f105]) ).
tff(f413,plain,
( ~ qmltpeq(sK103,op(e0,e0),e3)
| ~ qmltpeq(sK104,op(e1,e1),e3)
| ~ qmltpeq(sK105,op(e2,e2),e3)
| sP3 ),
inference(cnf_transformation,[],[f105]) ).
tff(f421,plain,
( ~ qmltpeq(sK100,op(e0,e0),e2)
| ~ qmltpeq(sK101,op(e1,e1),e2)
| ~ qmltpeq(sK102,op(e2,e2),e2)
| sP4 ),
inference(cnf_transformation,[],[f105]) ).
tff(f429,plain,
( ~ qmltpeq(sK97,op(e0,e0),e1)
| ~ qmltpeq(sK98,op(e1,e1),e1)
| ~ qmltpeq(sK99,op(e2,e2),e1)
| sP5 ),
inference(cnf_transformation,[],[f105]) ).
tff(f437,plain,
( ~ qmltpeq(sK94,op(e0,e0),e0)
| ~ qmltpeq(sK95,op(e1,e1),e0)
| ~ qmltpeq(sK96,op(e2,e2),e0)
| sP6 ),
inference(cnf_transformation,[],[f105]) ).
tff(f439,definition,
( spl107_1
<=> sP0(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_1])],[avatar_definition]) ).
tff(f440,plain,
( sP0(sK106)
| ~ spl107_1 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,definition,
( spl107_2
<=> sP1(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_2])],[avatar_definition]) ).
tff(f443,plain,
( sP1(sK106)
| ~ spl107_2 ),
inference(avatar_component_clause,[],[f442]) ).
tff(f445,definition,
( spl107_3
<=> sP2(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_3])],[avatar_definition]) ).
tff(f446,plain,
( sP2(sK106)
| ~ spl107_3 ),
inference(avatar_component_clause,[],[f445]) ).
tff(f448,definition,
( spl107_4
<=> ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16) ) ),
introduced(definition,[new_symbols(definition,[spl107_4])],[avatar_definition]) ).
tff(f449,plain,
( ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16) )
| ~ spl107_4 ),
inference(avatar_component_clause,[],[f448]) ).
tff(f450,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_4 ),
inference(avatar_split_clause,[],[f402,f448,f445,f442,f439]) ).
tff(f452,definition,
( spl107_5
<=> ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15) ) ),
introduced(definition,[new_symbols(definition,[spl107_5])],[avatar_definition]) ).
tff(f453,plain,
( ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15) )
| ~ spl107_5 ),
inference(avatar_component_clause,[],[f452]) ).
tff(f454,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_5 ),
inference(avatar_split_clause,[],[f403,f452,f445,f442,f439]) ).
tff(f456,definition,
( spl107_6
<=> ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14) ) ),
introduced(definition,[new_symbols(definition,[spl107_6])],[avatar_definition]) ).
tff(f457,plain,
( ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14) )
| ~ spl107_6 ),
inference(avatar_component_clause,[],[f456]) ).
tff(f458,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_6 ),
inference(avatar_split_clause,[],[f404,f456,f445,f442,f439]) ).
tff(f460,definition,
( spl107_7
<=> ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13) ) ),
introduced(definition,[new_symbols(definition,[spl107_7])],[avatar_definition]) ).
tff(f461,plain,
( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13) )
| ~ spl107_7 ),
inference(avatar_component_clause,[],[f460]) ).
tff(f462,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_7 ),
inference(avatar_split_clause,[],[f405,f460,f445,f442,f439]) ).
tff(f464,definition,
( spl107_8
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl107_8])],[avatar_definition]) ).
tff(f477,definition,
( spl107_12
<=> qmltpeq(sK105,op(e2,e2),e3) ),
introduced(definition,[new_symbols(definition,[spl107_12])],[avatar_definition]) ).
tff(f478,plain,
( ~ qmltpeq(sK105,op(e2,e2),e3)
| spl107_12 ),
inference(avatar_component_clause,[],[f477]) ).
tff(f481,definition,
( spl107_13
<=> qmltpeq(sK104,op(e1,e1),e3) ),
introduced(definition,[new_symbols(definition,[spl107_13])],[avatar_definition]) ).
tff(f482,plain,
( ~ qmltpeq(sK104,op(e1,e1),e3)
| spl107_13 ),
inference(avatar_component_clause,[],[f481]) ).
tff(f486,definition,
( spl107_14
<=> qmltpeq(sK103,op(e0,e0),e3) ),
introduced(definition,[new_symbols(definition,[spl107_14])],[avatar_definition]) ).
tff(f487,plain,
( ~ qmltpeq(sK103,op(e0,e0),e3)
| spl107_14 ),
inference(avatar_component_clause,[],[f486]) ).
tff(f491,plain,
( spl107_8
| ~ spl107_12
| ~ spl107_13
| ~ spl107_14 ),
inference(avatar_split_clause,[],[f413,f486,f481,f477,f464]) ).
tff(f493,definition,
( spl107_15
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl107_15])],[avatar_definition]) ).
tff(f506,definition,
( spl107_19
<=> qmltpeq(sK102,op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl107_19])],[avatar_definition]) ).
tff(f507,plain,
( ~ qmltpeq(sK102,op(e2,e2),e2)
| spl107_19 ),
inference(avatar_component_clause,[],[f506]) ).
tff(f510,definition,
( spl107_20
<=> qmltpeq(sK101,op(e1,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl107_20])],[avatar_definition]) ).
tff(f511,plain,
( ~ qmltpeq(sK101,op(e1,e1),e2)
| spl107_20 ),
inference(avatar_component_clause,[],[f510]) ).
tff(f515,definition,
( spl107_21
<=> qmltpeq(sK100,op(e0,e0),e2) ),
introduced(definition,[new_symbols(definition,[spl107_21])],[avatar_definition]) ).
tff(f516,plain,
( ~ qmltpeq(sK100,op(e0,e0),e2)
| spl107_21 ),
inference(avatar_component_clause,[],[f515]) ).
tff(f520,plain,
( spl107_15
| ~ spl107_19
| ~ spl107_20
| ~ spl107_21 ),
inference(avatar_split_clause,[],[f421,f515,f510,f506,f493]) ).
tff(f522,definition,
( spl107_22
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl107_22])],[avatar_definition]) ).
tff(f535,definition,
( spl107_26
<=> qmltpeq(sK99,op(e2,e2),e1) ),
introduced(definition,[new_symbols(definition,[spl107_26])],[avatar_definition]) ).
tff(f536,plain,
( ~ qmltpeq(sK99,op(e2,e2),e1)
| spl107_26 ),
inference(avatar_component_clause,[],[f535]) ).
tff(f539,definition,
( spl107_27
<=> qmltpeq(sK98,op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl107_27])],[avatar_definition]) ).
tff(f540,plain,
( ~ qmltpeq(sK98,op(e1,e1),e1)
| spl107_27 ),
inference(avatar_component_clause,[],[f539]) ).
tff(f544,definition,
( spl107_28
<=> qmltpeq(sK97,op(e0,e0),e1) ),
introduced(definition,[new_symbols(definition,[spl107_28])],[avatar_definition]) ).
tff(f545,plain,
( ~ qmltpeq(sK97,op(e0,e0),e1)
| spl107_28 ),
inference(avatar_component_clause,[],[f544]) ).
tff(f549,plain,
( spl107_22
| ~ spl107_26
| ~ spl107_27
| ~ spl107_28 ),
inference(avatar_split_clause,[],[f429,f544,f539,f535,f522]) ).
tff(f551,definition,
( spl107_29
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl107_29])],[avatar_definition]) ).
tff(f564,definition,
( spl107_33
<=> qmltpeq(sK96,op(e2,e2),e0) ),
introduced(definition,[new_symbols(definition,[spl107_33])],[avatar_definition]) ).
tff(f565,plain,
( ~ qmltpeq(sK96,op(e2,e2),e0)
| spl107_33 ),
inference(avatar_component_clause,[],[f564]) ).
tff(f568,definition,
( spl107_34
<=> qmltpeq(sK95,op(e1,e1),e0) ),
introduced(definition,[new_symbols(definition,[spl107_34])],[avatar_definition]) ).
tff(f569,plain,
( ~ qmltpeq(sK95,op(e1,e1),e0)
| spl107_34 ),
inference(avatar_component_clause,[],[f568]) ).
tff(f573,definition,
( spl107_35
<=> qmltpeq(sK94,op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl107_35])],[avatar_definition]) ).
tff(f574,plain,
( ~ qmltpeq(sK94,op(e0,e0),e0)
| spl107_35 ),
inference(avatar_component_clause,[],[f573]) ).
tff(f578,plain,
( spl107_29
| ~ spl107_33
| ~ spl107_34
| ~ spl107_35 ),
inference(avatar_split_clause,[],[f437,f573,f568,f564,f551]) ).
tff(f585,definition,
( spl107_37
<=> qmltpeq(sK93,op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl107_37])],[avatar_definition]) ).
tff(f586,plain,
( ~ qmltpeq(sK93,op(e3,e3),e3)
| spl107_37 ),
inference(avatar_component_clause,[],[f585]) ).
tff(f587,plain,
( ~ spl107_8
| ~ spl107_37 ),
inference(avatar_split_clause,[],[f388,f585,f464]) ).
tff(f594,definition,
( spl107_39
<=> qmltpeq(sK92,op(e3,e3),e2) ),
introduced(definition,[new_symbols(definition,[spl107_39])],[avatar_definition]) ).
tff(f595,plain,
( ~ qmltpeq(sK92,op(e3,e3),e2)
| spl107_39 ),
inference(avatar_component_clause,[],[f594]) ).
tff(f596,plain,
( ~ spl107_15
| ~ spl107_39 ),
inference(avatar_split_clause,[],[f386,f594,f493]) ).
tff(f603,definition,
( spl107_41
<=> qmltpeq(sK91,op(e3,e3),e1) ),
introduced(definition,[new_symbols(definition,[spl107_41])],[avatar_definition]) ).
tff(f604,plain,
( ~ qmltpeq(sK91,op(e3,e3),e1)
| spl107_41 ),
inference(avatar_component_clause,[],[f603]) ).
tff(f605,plain,
( ~ spl107_22
| ~ spl107_41 ),
inference(avatar_split_clause,[],[f384,f603,f522]) ).
tff(f612,definition,
( spl107_43
<=> qmltpeq(sK90,op(e3,e3),e0) ),
introduced(definition,[new_symbols(definition,[spl107_43])],[avatar_definition]) ).
tff(f613,plain,
( ~ qmltpeq(sK90,op(e3,e3),e0)
| spl107_43 ),
inference(avatar_component_clause,[],[f612]) ).
tff(f614,plain,
( ~ spl107_29
| ~ spl107_43 ),
inference(avatar_split_clause,[],[f382,f612,f551]) ).
tff(f903,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e3,e3),e2)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_2 ),
inference(resolution,[],[f393,f443]) ).
tff(f904,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e2,e2),e2)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_2 ),
inference(resolution,[],[f394,f443]) ).
tff(f905,plain,
( ~ '$ki_accessible'(sK106,sK102)
| ~ spl107_2
| spl107_19 ),
inference(resolution,[],[f904,f507]) ).
tff(f906,plain,
( $false
| ~ spl107_2
| spl107_19 ),
inference(resolution,[],[f905,f106]) ).
tff(f907,plain,
( ~ spl107_2
| spl107_19 ),
inference(avatar_contradiction_clause,[],[f906]) ).
tff(f908,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e1,e1),e2)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_2 ),
inference(resolution,[],[f395,f443]) ).
tff(f909,plain,
( ~ '$ki_accessible'(sK106,sK101)
| ~ spl107_2
| spl107_20 ),
inference(resolution,[],[f908,f511]) ).
tff(f910,plain,
( $false
| ~ spl107_2
| spl107_20 ),
inference(resolution,[],[f909,f106]) ).
tff(f911,plain,
( ~ spl107_2
| spl107_20 ),
inference(avatar_contradiction_clause,[],[f910]) ).
tff(f912,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e0,e0),e2)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_2 ),
inference(resolution,[],[f396,f443]) ).
tff(f913,plain,
( ~ '$ki_accessible'(sK106,sK100)
| ~ spl107_2
| spl107_21 ),
inference(resolution,[],[f912,f516]) ).
tff(f914,plain,
( $false
| ~ spl107_2
| spl107_21 ),
inference(resolution,[],[f913,f106]) ).
tff(f915,plain,
( ~ spl107_2
| spl107_21 ),
inference(avatar_contradiction_clause,[],[f914]) ).
tff(f916,plain,
( ~ '$ki_accessible'(sK106,sK92)
| ~ spl107_2
| spl107_39 ),
inference(resolution,[],[f595,f903]) ).
tff(f918,plain,
( $false
| ~ spl107_2
| spl107_39 ),
inference(resolution,[],[f916,f106]) ).
tff(f919,plain,
( ~ spl107_2
| spl107_39 ),
inference(avatar_contradiction_clause,[],[f918]) ).
tff(f920,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e3,e3),e3)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_1 ),
inference(resolution,[],[f397,f440]) ).
tff(f921,plain,
( ~ '$ki_accessible'(sK106,sK93)
| ~ spl107_1
| spl107_37 ),
inference(resolution,[],[f920,f586]) ).
tff(f922,plain,
( $false
| ~ spl107_1
| spl107_37 ),
inference(resolution,[],[f921,f106]) ).
tff(f923,plain,
( ~ spl107_1
| spl107_37 ),
inference(avatar_contradiction_clause,[],[f922]) ).
tff(f924,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e0,e0),e1)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_3 ),
inference(resolution,[],[f446,f392]) ).
tff(f925,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e1,e1),e1)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_3 ),
inference(resolution,[],[f446,f391]) ).
tff(f926,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e2,e2),e1)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_3 ),
inference(resolution,[],[f446,f390]) ).
tff(f927,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e3,e3),e1)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_3 ),
inference(resolution,[],[f446,f389]) ).
tff(f928,plain,
( ~ '$ki_accessible'(sK106,sK97)
| ~ spl107_3
| spl107_28 ),
inference(resolution,[],[f924,f545]) ).
tff(f929,plain,
( $false
| ~ spl107_3
| spl107_28 ),
inference(resolution,[],[f928,f106]) ).
tff(f930,plain,
( ~ spl107_3
| spl107_28 ),
inference(avatar_contradiction_clause,[],[f929]) ).
tff(f931,plain,
( ~ '$ki_accessible'(sK106,sK99)
| ~ spl107_3
| spl107_26 ),
inference(resolution,[],[f926,f536]) ).
tff(f932,plain,
( $false
| ~ spl107_3
| spl107_26 ),
inference(resolution,[],[f931,f106]) ).
tff(f933,plain,
( ~ spl107_3
| spl107_26 ),
inference(avatar_contradiction_clause,[],[f932]) ).
tff(f934,plain,
( ~ '$ki_accessible'(sK106,sK98)
| ~ spl107_3
| spl107_27 ),
inference(resolution,[],[f540,f925]) ).
tff(f935,plain,
( $false
| ~ spl107_3
| spl107_27 ),
inference(resolution,[],[f934,f106]) ).
tff(f936,plain,
( ~ spl107_3
| spl107_27 ),
inference(avatar_contradiction_clause,[],[f935]) ).
tff(f937,plain,
( ~ '$ki_accessible'(sK106,sK91)
| ~ spl107_3
| spl107_41 ),
inference(resolution,[],[f604,f927]) ).
tff(f938,plain,
( $false
| ~ spl107_3
| spl107_41 ),
inference(resolution,[],[f937,f106]) ).
tff(f939,plain,
( ~ spl107_3
| spl107_41 ),
inference(avatar_contradiction_clause,[],[f938]) ).
tff(f946,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e0,e0),e3)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_1 ),
inference(resolution,[],[f400,f440]) ).
tff(f947,plain,
( ~ '$ki_accessible'(sK106,sK103)
| ~ spl107_1
| spl107_14 ),
inference(resolution,[],[f946,f487]) ).
tff(f948,plain,
( $false
| ~ spl107_1
| spl107_14 ),
inference(resolution,[],[f947,f106]) ).
tff(f949,plain,
( ~ spl107_1
| spl107_14 ),
inference(avatar_contradiction_clause,[],[f948]) ).
tff(f950,plain,
( ~ '$ki_accessible'(sK106,sK96)
| ~ spl107_5
| spl107_33 ),
inference(resolution,[],[f453,f565]) ).
tff(f951,plain,
( $false
| ~ spl107_5
| spl107_33 ),
inference(resolution,[],[f950,f106]) ).
tff(f952,plain,
( ~ spl107_5
| spl107_33 ),
inference(avatar_contradiction_clause,[],[f951]) ).
tff(f956,plain,
( ~ '$ki_accessible'(sK106,sK94)
| ~ spl107_7
| spl107_35 ),
inference(resolution,[],[f461,f574]) ).
tff(f957,plain,
( $false
| ~ spl107_7
| spl107_35 ),
inference(resolution,[],[f956,f106]) ).
tff(f958,plain,
( ~ spl107_7
| spl107_35 ),
inference(avatar_contradiction_clause,[],[f957]) ).
tff(f959,plain,
( ~ '$ki_accessible'(sK106,sK95)
| ~ spl107_6
| spl107_34 ),
inference(resolution,[],[f569,f457]) ).
tff(f960,plain,
( $false
| ~ spl107_6
| spl107_34 ),
inference(resolution,[],[f959,f106]) ).
tff(f961,plain,
( ~ spl107_6
| spl107_34 ),
inference(avatar_contradiction_clause,[],[f960]) ).
tff(f962,plain,
( ~ '$ki_accessible'(sK106,sK90)
| ~ spl107_4
| spl107_43 ),
inference(resolution,[],[f613,f449]) ).
tff(f964,plain,
( $false
| ~ spl107_4
| spl107_43 ),
inference(resolution,[],[f962,f106]) ).
tff(f965,plain,
( ~ spl107_4
| spl107_43 ),
inference(avatar_contradiction_clause,[],[f964]) ).
tff(f967,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e1,e1),e3)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_1 ),
inference(resolution,[],[f440,f399]) ).
tff(f968,plain,
( ! [X0: '$ki_world'] :
( qmltpeq(X0,op(e2,e2),e3)
| ~ '$ki_accessible'(sK106,X0) )
| ~ spl107_1 ),
inference(resolution,[],[f440,f398]) ).
tff(f972,plain,
( ~ '$ki_accessible'(sK106,sK105)
| ~ spl107_1
| spl107_12 ),
inference(resolution,[],[f968,f478]) ).
tff(f973,plain,
( $false
| ~ spl107_1
| spl107_12 ),
inference(resolution,[],[f972,f106]) ).
tff(f974,plain,
( ~ spl107_1
| spl107_12 ),
inference(avatar_contradiction_clause,[],[f973]) ).
tff(f975,plain,
( ~ '$ki_accessible'(sK106,sK104)
| ~ spl107_1
| spl107_13 ),
inference(resolution,[],[f482,f967]) ).
tff(f976,plain,
( $false
| ~ spl107_1
| spl107_13 ),
inference(resolution,[],[f975,f106]) ).
tff(f977,plain,
( ~ spl107_1
| spl107_13 ),
inference(avatar_contradiction_clause,[],[f976]) ).
cnf(s1,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_4 ),
inference(sat_conversion,[],[f450]) ).
cnf(s2,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_5 ),
inference(sat_conversion,[],[f454]) ).
cnf(s3,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_6 ),
inference(sat_conversion,[],[f458]) ).
cnf(s4,plain,
( spl107_1
| spl107_2
| spl107_3
| spl107_7 ),
inference(sat_conversion,[],[f462]) ).
cnf(s12,plain,
( spl107_8
| ~ spl107_12
| ~ spl107_13
| ~ spl107_14 ),
inference(sat_conversion,[],[f491]) ).
cnf(s20,plain,
( spl107_15
| ~ spl107_19
| ~ spl107_20
| ~ spl107_21 ),
inference(sat_conversion,[],[f520]) ).
cnf(s28,plain,
( spl107_22
| ~ spl107_26
| ~ spl107_27
| ~ spl107_28 ),
inference(sat_conversion,[],[f549]) ).
cnf(s36,plain,
( spl107_29
| ~ spl107_33
| ~ spl107_34
| ~ spl107_35 ),
inference(sat_conversion,[],[f578]) ).
cnf(s38,plain,
( ~ spl107_8
| ~ spl107_37 ),
inference(sat_conversion,[],[f587]) ).
cnf(s40,plain,
( ~ spl107_15
| ~ spl107_39 ),
inference(sat_conversion,[],[f596]) ).
cnf(s42,plain,
( ~ spl107_22
| ~ spl107_41 ),
inference(sat_conversion,[],[f605]) ).
cnf(s44,plain,
( ~ spl107_29
| ~ spl107_43 ),
inference(sat_conversion,[],[f614]) ).
cnf(s72,plain,
( ~ spl107_2
| spl107_19 ),
inference(sat_conversion,[],[f907]) ).
cnf(s73,plain,
( ~ spl107_2
| spl107_20 ),
inference(sat_conversion,[],[f911]) ).
cnf(s74,plain,
( ~ spl107_2
| spl107_21 ),
inference(sat_conversion,[],[f915]) ).
cnf(s75,plain,
( ~ spl107_2
| spl107_39 ),
inference(sat_conversion,[],[f919]) ).
cnf(s76,plain,
( ~ spl107_1
| spl107_37 ),
inference(sat_conversion,[],[f923]) ).
cnf(s77,plain,
( ~ spl107_3
| spl107_28 ),
inference(sat_conversion,[],[f930]) ).
cnf(s78,plain,
( ~ spl107_3
| spl107_26 ),
inference(sat_conversion,[],[f933]) ).
cnf(s79,plain,
( ~ spl107_3
| spl107_27 ),
inference(sat_conversion,[],[f936]) ).
cnf(s80,plain,
( ~ spl107_3
| spl107_41 ),
inference(sat_conversion,[],[f939]) ).
cnf(s82,plain,
( ~ spl107_1
| spl107_14 ),
inference(sat_conversion,[],[f949]) ).
cnf(s83,plain,
( ~ spl107_5
| spl107_33 ),
inference(sat_conversion,[],[f952]) ).
cnf(s85,plain,
( ~ spl107_7
| spl107_35 ),
inference(sat_conversion,[],[f958]) ).
cnf(s86,plain,
( ~ spl107_6
| spl107_34 ),
inference(sat_conversion,[],[f961]) ).
cnf(s87,plain,
( ~ spl107_4
| spl107_43 ),
inference(sat_conversion,[],[f965]) ).
cnf(s89,plain,
( ~ spl107_1
| spl107_12 ),
inference(sat_conversion,[],[f974]) ).
cnf(s90,plain,
( ~ spl107_1
| spl107_13 ),
inference(sat_conversion,[],[f977]) ).
cnf(s91,plain,
( spl107_3
| spl107_2
| spl107_1 ),
inference(rat,[],[s36,s44,s85,s86,s87,s83,s4,s3,s1,s2]) ).
cnf(s92,plain,
~ spl107_3,
inference(rat,[],[s28,s42,s77,s78,s79,s80]) ).
cnf(s93,plain,
~ spl107_2,
inference(rat,[],[s20,s40,s72,s73,s74,s75]) ).
cnf(s94,plain,
spl107_1,
inference(rat,[],[s91,s92,s93]) ).
cnf(s95,plain,
spl107_13,
inference(rat,[],[s90,s94]) ).
cnf(s96,plain,
spl107_12,
inference(rat,[],[s89,s94]) ).
cnf(s97,plain,
spl107_14,
inference(rat,[],[s82,s94]) ).
cnf(s98,plain,
spl107_37,
inference(rat,[],[s76,s94]) ).
cnf(s99,plain,
spl107_8,
inference(rat,[],[s12,s97,s95,s96]) ).
cnf(s100,plain,
$false,
inference(rat,[],[s38,s98,s99]) ).
tff(f978,plain,
$false,
inference(avatar_sat_refutation,[],[s100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n002.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 17:10:07 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 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
% 3.94/1.54 % (3748286)Detected formulas, will run a generic FOF schedule.
% 3.94/1.54 % (3748344)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=1667607410:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.94/1.54 % (3748343)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=2451861058:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.94/1.54 % (3748349)dis-21_1_sil=8000:lcm=predicate:random_seed=430397167: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)
% 3.94/1.54 % (3748349)First to succeed.
% 3.94/1.54 % (3748349)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3748286"
% 3.94/1.54 % (3748345)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4084375791:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.94/1.54 % (3748342)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=525504560:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.94/1.54 % (3748346)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2381436027:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.94/1.54 % (3748346)Also succeeded, but the first one will report.
% 3.94/1.54 % (3748345)Refutation not found, incomplete strategy
% 3.94/1.54 % (3748345)------------------------------
% 3.94/1.54 % (3748345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.54 % (3748345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.54 % (3748345)CaDiCaL version: 2.1.3
% 3.94/1.54 % (3748345)Termination reason: Refutation not found, incomplete strategy
% 3.94/1.54 % (3748345)Time elapsed: 0.032 s
% 3.94/1.54 % (3748345)Peak memory usage: 89 MB
% 3.94/1.54 % (3748345)Instructions burned: 39 (million)
% 3.94/1.54 % (3748348)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2810078547:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.94/1.54 % (3748348)Also succeeded, but the first one will report.
% 3.94/1.54 % (3748349)Refutation found. Thanks to Tanya!
% 3.94/1.54 % SZS status Theorem for theBenchmark
% 3.94/1.54 % SZS output start Proof for theBenchmark
% See solution above
% 4.86/1.80 % (3748349)------------------------------
% 4.86/1.80 % (3748349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.86/1.80 % (3748349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.86/1.80 % (3748349)CaDiCaL version: 2.1.3
% 4.86/1.80 % (3748349)Termination reason: Refutation
% 4.86/1.80 % (3748349)Time elapsed: 0.019 s
% 4.86/1.80 % (3748349)Peak memory usage: 90 MB
% 4.86/1.80 % (3748349)Instructions burned: 28 (million)
% 4.86/1.80 % (3748349)------------------------------
% 4.86/1.80 % (3748349)------------------------------
% 4.86/1.80 % (3748286)Success in time 0.605 s
% 4.86/1.80 % Vampire exiting
%------------------------------------------------------------------------------