%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n014.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:02 PM UTC 2026
% Result : Theorem 0.22s 0.52s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 43
% Syntax : Number of formulae : 252 ( 14 unt; 0 typ; 41 def)
% Number of atoms : 2434 ( 0 equ)
% Maximal formula atoms : 65 ( 9 avg)
% Number of connectives : 1222 ( 420 ~; 461 |; 208 &)
% ( 34 <=>; 99 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 1380 (1380 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 50 ( 49 usr; 43 prp; 0-3 aty)
% Number of functors : 101 ( 101 usr; 18 con; 0-3 aty)
% Number of variables : 330 ( 0 sgn 275 !; 55 ?; 330 :)
% 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'] :
( qmltpeq(X4,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f99]) ).
tff(f390,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X3)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f99]) ).
tff(f391,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X2)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f99]) ).
tff(f392,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X1)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f99]) ).
tff(f393,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X4)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f101]) ).
tff(f394,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X3)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f101]) ).
tff(f395,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X2)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f101]) ).
tff(f396,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X1)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f101]) ).
tff(f397,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X4)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f398,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X3)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f399,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X2)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f400,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X1)
| ~ sP0(X0) ),
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(f440,definition,
( spl107_1
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl107_1])],[avatar_definition]) ).
tff(f444,definition,
( spl107_2
<=> qmltpeq(sK90,op(e3,e3),e0) ),
introduced(definition,[new_symbols(definition,[spl107_2])],[avatar_definition]) ).
tff(f446,plain,
( ~ qmltpeq(sK90,op(e3,e3),e0)
| spl107_2 ),
inference(avatar_component_clause,[],[f444]) ).
tff(f447,plain,
( ~ spl107_1
| ~ spl107_2 ),
inference(avatar_split_clause,[],[f382,f444,f440]) ).
tff(f449,definition,
( spl107_3
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl107_3])],[avatar_definition]) ).
tff(f453,definition,
( spl107_4
<=> qmltpeq(sK91,op(e3,e3),e1) ),
introduced(definition,[new_symbols(definition,[spl107_4])],[avatar_definition]) ).
tff(f455,plain,
( ~ qmltpeq(sK91,op(e3,e3),e1)
| spl107_4 ),
inference(avatar_component_clause,[],[f453]) ).
tff(f456,plain,
( ~ spl107_3
| ~ spl107_4 ),
inference(avatar_split_clause,[],[f384,f453,f449]) ).
tff(f458,definition,
( spl107_5
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl107_5])],[avatar_definition]) ).
tff(f460,plain,
( ~ sP4
| spl107_5 ),
inference(avatar_component_clause,[],[f458]) ).
tff(f462,definition,
( spl107_6
<=> qmltpeq(sK92,op(e3,e3),e2) ),
introduced(definition,[new_symbols(definition,[spl107_6])],[avatar_definition]) ).
tff(f464,plain,
( ~ qmltpeq(sK92,op(e3,e3),e2)
| spl107_6 ),
inference(avatar_component_clause,[],[f462]) ).
tff(f465,plain,
( ~ spl107_5
| ~ spl107_6 ),
inference(avatar_split_clause,[],[f386,f462,f458]) ).
tff(f467,definition,
( spl107_7
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl107_7])],[avatar_definition]) ).
tff(f469,plain,
( ~ sP3
| spl107_7 ),
inference(avatar_component_clause,[],[f467]) ).
tff(f471,definition,
( spl107_8
<=> qmltpeq(sK93,op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl107_8])],[avatar_definition]) ).
tff(f473,plain,
( ~ qmltpeq(sK93,op(e3,e3),e3)
| spl107_8 ),
inference(avatar_component_clause,[],[f471]) ).
tff(f474,plain,
( ~ spl107_7
| ~ spl107_8 ),
inference(avatar_split_clause,[],[f388,f471,f467]) ).
tff(f718,definition,
( spl107_82
<=> qmltpeq(sK105,op(e2,e2),e3) ),
introduced(definition,[new_symbols(definition,[spl107_82])],[avatar_definition]) ).
tff(f720,plain,
( ~ qmltpeq(sK105,op(e2,e2),e3)
| spl107_82 ),
inference(avatar_component_clause,[],[f718]) ).
tff(f724,definition,
( spl107_83
<=> qmltpeq(sK102,op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl107_83])],[avatar_definition]) ).
tff(f726,plain,
( ~ qmltpeq(sK102,op(e2,e2),e2)
| spl107_83 ),
inference(avatar_component_clause,[],[f724]) ).
tff(f741,definition,
( spl107_86
<=> sP0(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_86])],[avatar_definition]) ).
tff(f743,plain,
( sP0(sK106)
| ~ spl107_86 ),
inference(avatar_component_clause,[],[f741]) ).
tff(f745,definition,
( spl107_87
<=> sP1(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_87])],[avatar_definition]) ).
tff(f747,plain,
( sP1(sK106)
| ~ spl107_87 ),
inference(avatar_component_clause,[],[f745]) ).
tff(f749,definition,
( spl107_88
<=> sP2(sK106) ),
introduced(definition,[new_symbols(definition,[spl107_88])],[avatar_definition]) ).
tff(f751,plain,
( sP2(sK106)
| ~ spl107_88 ),
inference(avatar_component_clause,[],[f749]) ).
tff(f756,definition,
( spl107_90
<=> ! [X16: '$ki_world'] : qmltpeq(X16,op(e3,e3),e0) ),
introduced(definition,[new_symbols(definition,[spl107_90])],[avatar_definition]) ).
tff(f757,plain,
( ! [X16: '$ki_world'] : qmltpeq(X16,op(e3,e3),e0)
| ~ spl107_90 ),
inference(avatar_component_clause,[],[f756]) ).
tff(f759,definition,
( spl107_91
<=> ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16) ) ),
introduced(definition,[new_symbols(definition,[spl107_91])],[avatar_definition]) ).
tff(f760,plain,
( ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e0)
| ~ '$ki_accessible'(sK106,X16) )
| ~ spl107_91 ),
inference(avatar_component_clause,[],[f759]) ).
tff(f761,plain,
( spl107_86
| spl107_87
| spl107_88
| spl107_91 ),
inference(avatar_split_clause,[],[f402,f759,f749,f745,f741]) ).
tff(f764,definition,
( spl107_92
<=> qmltpeq(sK104,op(e1,e1),e3) ),
introduced(definition,[new_symbols(definition,[spl107_92])],[avatar_definition]) ).
tff(f766,plain,
( ~ qmltpeq(sK104,op(e1,e1),e3)
| spl107_92 ),
inference(avatar_component_clause,[],[f764]) ).
tff(f770,definition,
( spl107_93
<=> qmltpeq(sK101,op(e1,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl107_93])],[avatar_definition]) ).
tff(f772,plain,
( ~ qmltpeq(sK101,op(e1,e1),e2)
| spl107_93 ),
inference(avatar_component_clause,[],[f770]) ).
tff(f786,plain,
( ~ qmltpeq(sK103,op(e0,e0),e3)
| ~ qmltpeq(sK104,op(e1,e1),e3)
| ~ qmltpeq(sK105,op(e2,e2),e3)
| spl107_7 ),
inference(forward_subsumption_resolution,[],[f413,f469]) ).
tff(f787,plain,
( ~ qmltpeq(sK100,op(e0,e0),e2)
| ~ qmltpeq(sK101,op(e1,e1),e2)
| ~ qmltpeq(sK102,op(e2,e2),e2)
| spl107_5 ),
inference(forward_subsumption_resolution,[],[f421,f460]) ).
tff(f789,definition,
( spl107_96
<=> qmltpeq(sK103,op(e0,e0),e3) ),
introduced(definition,[new_symbols(definition,[spl107_96])],[avatar_definition]) ).
tff(f791,plain,
( ~ qmltpeq(sK103,op(e0,e0),e3)
| spl107_96 ),
inference(avatar_component_clause,[],[f789]) ).
tff(f792,plain,
( ~ spl107_82
| ~ spl107_92
| ~ spl107_96
| spl107_7 ),
inference(avatar_split_clause,[],[f786,f467,f789,f764,f718]) ).
tff(f794,definition,
( spl107_97
<=> qmltpeq(sK100,op(e0,e0),e2) ),
introduced(definition,[new_symbols(definition,[spl107_97])],[avatar_definition]) ).
tff(f796,plain,
( ~ qmltpeq(sK100,op(e0,e0),e2)
| spl107_97 ),
inference(avatar_component_clause,[],[f794]) ).
tff(f797,plain,
( ~ spl107_83
| ~ spl107_93
| ~ spl107_97
| spl107_5 ),
inference(avatar_split_clause,[],[f787,f458,f794,f770,f724]) ).
tff(f834,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f389,f106]) ).
tff(f836,definition,
( spl107_100
<=> ! [X0: '$ki_world'] : ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[spl107_100])],[avatar_definition]) ).
tff(f837,plain,
( ! [X0: '$ki_world'] : ~ sP2(X0)
| ~ spl107_100 ),
inference(avatar_component_clause,[],[f836]) ).
tff(f839,definition,
( spl107_101
<=> ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e1) ),
introduced(definition,[new_symbols(definition,[spl107_101])],[avatar_definition]) ).
tff(f840,plain,
( ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e1)
| ~ spl107_101 ),
inference(avatar_component_clause,[],[f839]) ).
tff(f841,plain,
( spl107_100
| spl107_101 ),
inference(avatar_split_clause,[],[f834,f839,f836]) ).
tff(f842,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e2)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f393,f106]) ).
tff(f844,definition,
( spl107_102
<=> ! [X0: '$ki_world'] : ~ sP1(X0) ),
introduced(definition,[new_symbols(definition,[spl107_102])],[avatar_definition]) ).
tff(f845,plain,
( ! [X0: '$ki_world'] : ~ sP1(X0)
| ~ spl107_102 ),
inference(avatar_component_clause,[],[f844]) ).
tff(f847,definition,
( spl107_103
<=> ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e2) ),
introduced(definition,[new_symbols(definition,[spl107_103])],[avatar_definition]) ).
tff(f848,plain,
( ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e2)
| ~ spl107_103 ),
inference(avatar_component_clause,[],[f847]) ).
tff(f849,plain,
( spl107_102
| spl107_103 ),
inference(avatar_split_clause,[],[f842,f847,f844]) ).
tff(f850,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e3)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f397,f106]) ).
tff(f852,definition,
( spl107_104
<=> ! [X0: '$ki_world'] : ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[spl107_104])],[avatar_definition]) ).
tff(f853,plain,
( ! [X0: '$ki_world'] : ~ sP0(X0)
| ~ spl107_104 ),
inference(avatar_component_clause,[],[f852]) ).
tff(f855,definition,
( spl107_105
<=> ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl107_105])],[avatar_definition]) ).
tff(f856,plain,
( ! [X4: '$ki_world'] : qmltpeq(X4,op(e3,e3),e3)
| ~ spl107_105 ),
inference(avatar_component_clause,[],[f855]) ).
tff(f857,plain,
( spl107_104
| spl107_105 ),
inference(avatar_split_clause,[],[f850,f855,f852]) ).
tff(f858,plain,
( $false
| ~ spl107_86
| ~ spl107_104 ),
inference(resolution,[],[f853,f743]) ).
tff(f859,plain,
( ~ spl107_86
| ~ spl107_104 ),
inference(avatar_contradiction_clause,[],[f858]) ).
tff(f860,plain,
( ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15)
| sP1(sK106)
| sP0(sK106) )
| ~ spl107_100 ),
inference(forward_subsumption_resolution,[],[f403,f837]) ).
tff(f861,plain,
( ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14)
| sP1(sK106)
| sP0(sK106) )
| ~ spl107_100 ),
inference(forward_subsumption_resolution,[],[f404,f837]) ).
tff(f862,plain,
( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13)
| sP1(sK106)
| sP0(sK106) )
| ~ spl107_100 ),
inference(forward_subsumption_resolution,[],[f405,f837]) ).
tff(f863,plain,
( ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15)
| sP0(sK106) )
| ~ spl107_100
| ~ spl107_102 ),
inference(forward_subsumption_resolution,[],[f860,f845]) ).
tff(f864,plain,
( ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14)
| sP0(sK106) )
| ~ spl107_100
| ~ spl107_102 ),
inference(forward_subsumption_resolution,[],[f861,f845]) ).
tff(f865,plain,
( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13)
| sP0(sK106) )
| ~ spl107_100
| ~ spl107_102 ),
inference(forward_subsumption_resolution,[],[f862,f845]) ).
tff(f866,plain,
( ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e0)
| ~ '$ki_accessible'(sK106,X15) )
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f863,f853]) ).
tff(f867,plain,
( ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e0)
| ~ '$ki_accessible'(sK106,X14) )
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f864,f853]) ).
tff(f868,plain,
( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e0)
| ~ '$ki_accessible'(sK106,X13) )
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f865,f853]) ).
tff(f869,plain,
( ! [X15: '$ki_world'] : qmltpeq(X15,op(e2,e2),e0)
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f866,f106]) ).
tff(f870,plain,
( ! [X14: '$ki_world'] : qmltpeq(X14,op(e1,e1),e0)
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f867,f106]) ).
tff(f871,plain,
( ! [X13: '$ki_world'] : qmltpeq(X13,op(e0,e0),e0)
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f868,f106]) ).
tff(f878,plain,
( $false
| spl107_2
| ~ spl107_90 ),
inference(forward_subsumption_resolution,[],[f446,f757]) ).
tff(f879,plain,
( spl107_2
| ~ spl107_90 ),
inference(avatar_contradiction_clause,[],[f878]) ).
tff(f880,plain,
( ~ qmltpeq(sK95,op(e1,e1),e0)
| ~ qmltpeq(sK96,op(e2,e2),e0)
| sP6
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f437,f871]) ).
tff(f881,plain,
( ~ qmltpeq(sK96,op(e2,e2),e0)
| sP6
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f880,f870]) ).
tff(f882,plain,
( sP6
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(forward_subsumption_resolution,[],[f881,f869]) ).
tff(f883,plain,
( ! [X16: '$ki_world'] : qmltpeq(X16,op(e3,e3),e0)
| ~ spl107_91 ),
inference(forward_subsumption_resolution,[],[f760,f106]) ).
tff(f884,plain,
( spl107_1
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(avatar_split_clause,[],[f882,f852,f844,f836,f440]) ).
tff(f885,plain,
( spl107_90
| ~ spl107_91 ),
inference(avatar_split_clause,[],[f883,f759,f756]) ).
tff(f886,plain,
( $false
| ~ spl107_87
| ~ spl107_102 ),
inference(forward_subsumption_resolution,[],[f747,f845]) ).
tff(f887,plain,
( ~ spl107_87
| ~ spl107_102 ),
inference(avatar_contradiction_clause,[],[f886]) ).
tff(f888,plain,
( $false
| ~ spl107_88
| ~ spl107_100 ),
inference(forward_subsumption_resolution,[],[f751,f837]) ).
tff(f889,plain,
( ~ spl107_88
| ~ spl107_100 ),
inference(avatar_contradiction_clause,[],[f888]) ).
tff(f890,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f390,f106]) ).
tff(f891,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f391,f106]) ).
tff(f892,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f392,f106]) ).
tff(f907,definition,
( spl107_106
<=> ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e1) ),
introduced(definition,[new_symbols(definition,[spl107_106])],[avatar_definition]) ).
tff(f908,plain,
( ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e1)
| ~ spl107_106 ),
inference(avatar_component_clause,[],[f907]) ).
tff(f909,plain,
( spl107_100
| spl107_106 ),
inference(avatar_split_clause,[],[f890,f907,f836]) ).
tff(f913,definition,
( spl107_107
<=> ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl107_107])],[avatar_definition]) ).
tff(f914,plain,
( ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e1)
| ~ spl107_107 ),
inference(avatar_component_clause,[],[f913]) ).
tff(f915,plain,
( spl107_100
| spl107_107 ),
inference(avatar_split_clause,[],[f891,f913,f836]) ).
tff(f917,definition,
( spl107_108
<=> ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e1) ),
introduced(definition,[new_symbols(definition,[spl107_108])],[avatar_definition]) ).
tff(f918,plain,
( ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e1)
| ~ spl107_108 ),
inference(avatar_component_clause,[],[f917]) ).
tff(f919,plain,
( spl107_100
| spl107_108 ),
inference(avatar_split_clause,[],[f892,f917,f836]) ).
tff(f924,plain,
( $false
| spl107_4
| ~ spl107_101 ),
inference(forward_subsumption_resolution,[],[f455,f840]) ).
tff(f925,plain,
( spl107_4
| ~ spl107_101 ),
inference(avatar_contradiction_clause,[],[f924]) ).
tff(f926,plain,
( ~ qmltpeq(sK98,op(e1,e1),e1)
| ~ qmltpeq(sK99,op(e2,e2),e1)
| sP5
| ~ spl107_108 ),
inference(forward_subsumption_resolution,[],[f429,f918]) ).
tff(f927,plain,
( ~ qmltpeq(sK99,op(e2,e2),e1)
| sP5
| ~ spl107_107
| ~ spl107_108 ),
inference(forward_subsumption_resolution,[],[f926,f914]) ).
tff(f928,plain,
( sP5
| ~ spl107_106
| ~ spl107_107
| ~ spl107_108 ),
inference(forward_subsumption_resolution,[],[f927,f908]) ).
tff(f930,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e2)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f394,f106]) ).
tff(f931,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e2)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f395,f106]) ).
tff(f932,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e2)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f396,f106]) ).
tff(f940,plain,
( spl107_3
| ~ spl107_106
| ~ spl107_107
| ~ spl107_108 ),
inference(avatar_split_clause,[],[f928,f917,f913,f907,f449]) ).
tff(f960,definition,
( spl107_109
<=> ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl107_109])],[avatar_definition]) ).
tff(f961,plain,
( ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e2)
| ~ spl107_109 ),
inference(avatar_component_clause,[],[f960]) ).
tff(f962,plain,
( spl107_102
| spl107_109 ),
inference(avatar_split_clause,[],[f930,f960,f844]) ).
tff(f963,plain,
( $false
| spl107_83
| ~ spl107_109 ),
inference(resolution,[],[f961,f726]) ).
tff(f964,plain,
( spl107_83
| ~ spl107_109 ),
inference(avatar_contradiction_clause,[],[f963]) ).
tff(f966,definition,
( spl107_110
<=> ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl107_110])],[avatar_definition]) ).
tff(f967,plain,
( ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e2)
| ~ spl107_110 ),
inference(avatar_component_clause,[],[f966]) ).
tff(f968,plain,
( spl107_102
| spl107_110 ),
inference(avatar_split_clause,[],[f931,f966,f844]) ).
tff(f970,definition,
( spl107_111
<=> ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e2) ),
introduced(definition,[new_symbols(definition,[spl107_111])],[avatar_definition]) ).
tff(f971,plain,
( ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e2)
| ~ spl107_111 ),
inference(avatar_component_clause,[],[f970]) ).
tff(f972,plain,
( spl107_102
| spl107_111 ),
inference(avatar_split_clause,[],[f932,f970,f844]) ).
tff(f973,plain,
( $false
| spl107_97
| ~ spl107_111 ),
inference(resolution,[],[f971,f796]) ).
tff(f974,plain,
( spl107_97
| ~ spl107_111 ),
inference(avatar_contradiction_clause,[],[f973]) ).
tff(f975,plain,
( $false
| spl107_93
| ~ spl107_110 ),
inference(forward_subsumption_resolution,[],[f772,f967]) ).
tff(f976,plain,
( spl107_93
| ~ spl107_110 ),
inference(avatar_contradiction_clause,[],[f975]) ).
tff(f977,plain,
( $false
| spl107_6
| ~ spl107_103 ),
inference(forward_subsumption_resolution,[],[f464,f848]) ).
tff(f978,plain,
( spl107_6
| ~ spl107_103 ),
inference(avatar_contradiction_clause,[],[f977]) ).
tff(f1010,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e3)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f398,f106]) ).
tff(f1012,definition,
( spl107_112
<=> ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e3) ),
introduced(definition,[new_symbols(definition,[spl107_112])],[avatar_definition]) ).
tff(f1013,plain,
( ! [X3: '$ki_world'] : qmltpeq(X3,op(e2,e2),e3)
| ~ spl107_112 ),
inference(avatar_component_clause,[],[f1012]) ).
tff(f1014,plain,
( spl107_104
| spl107_112 ),
inference(avatar_split_clause,[],[f1010,f1012,f852]) ).
tff(f1015,plain,
( $false
| spl107_82
| ~ spl107_112 ),
inference(resolution,[],[f1013,f720]) ).
tff(f1016,plain,
( spl107_82
| ~ spl107_112 ),
inference(avatar_contradiction_clause,[],[f1015]) ).
tff(f1017,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e3)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f399,f106]) ).
tff(f1019,definition,
( spl107_113
<=> ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e3) ),
introduced(definition,[new_symbols(definition,[spl107_113])],[avatar_definition]) ).
tff(f1020,plain,
( ! [X2: '$ki_world'] : qmltpeq(X2,op(e1,e1),e3)
| ~ spl107_113 ),
inference(avatar_component_clause,[],[f1019]) ).
tff(f1021,plain,
( spl107_104
| spl107_113 ),
inference(avatar_split_clause,[],[f1017,f1019,f852]) ).
tff(f1022,plain,
( $false
| spl107_92
| ~ spl107_113 ),
inference(resolution,[],[f1020,f766]) ).
tff(f1023,plain,
( spl107_92
| ~ spl107_113 ),
inference(avatar_contradiction_clause,[],[f1022]) ).
tff(f1024,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e3)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f400,f106]) ).
tff(f1026,definition,
( spl107_114
<=> ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e3) ),
introduced(definition,[new_symbols(definition,[spl107_114])],[avatar_definition]) ).
tff(f1027,plain,
( ! [X1: '$ki_world'] : qmltpeq(X1,op(e0,e0),e3)
| ~ spl107_114 ),
inference(avatar_component_clause,[],[f1026]) ).
tff(f1028,plain,
( spl107_104
| spl107_114 ),
inference(avatar_split_clause,[],[f1024,f1026,f852]) ).
tff(f1029,plain,
( $false
| spl107_96
| ~ spl107_114 ),
inference(resolution,[],[f1027,f791]) ).
tff(f1030,plain,
( spl107_96
| ~ spl107_114 ),
inference(avatar_contradiction_clause,[],[f1029]) ).
tff(f1031,plain,
( $false
| spl107_8
| ~ spl107_105 ),
inference(forward_subsumption_resolution,[],[f473,f856]) ).
tff(f1032,plain,
( spl107_8
| ~ spl107_105 ),
inference(avatar_contradiction_clause,[],[f1031]) ).
cnf(s335,plain,
( ~ spl107_1
| ~ spl107_2 ),
inference(sat_conversion,[],[f447]) ).
cnf(s339,plain,
( ~ spl107_3
| ~ spl107_4 ),
inference(sat_conversion,[],[f456]) ).
cnf(s343,plain,
( ~ spl107_5
| ~ spl107_6 ),
inference(sat_conversion,[],[f465]) ).
cnf(s347,plain,
( ~ spl107_7
| ~ spl107_8 ),
inference(sat_conversion,[],[f474]) ).
cnf(s635,plain,
( spl107_86
| spl107_87
| spl107_88
| spl107_91 ),
inference(sat_conversion,[],[f761]) ).
cnf(s665,plain,
( spl107_7
| ~ spl107_82
| ~ spl107_92
| ~ spl107_96 ),
inference(sat_conversion,[],[f792]) ).
cnf(s669,plain,
( spl107_5
| ~ spl107_83
| ~ spl107_93
| ~ spl107_97 ),
inference(sat_conversion,[],[f797]) ).
cnf(s731,plain,
( spl107_100
| spl107_101 ),
inference(sat_conversion,[],[f841]) ).
cnf(s736,plain,
( spl107_102
| spl107_103 ),
inference(sat_conversion,[],[f849]) ).
cnf(s741,plain,
( spl107_104
| spl107_105 ),
inference(sat_conversion,[],[f857]) ).
cnf(s744,plain,
( ~ spl107_86
| ~ spl107_104 ),
inference(sat_conversion,[],[f859]) ).
cnf(s757,plain,
( spl107_2
| ~ spl107_90 ),
inference(sat_conversion,[],[f879]) ).
cnf(s763,plain,
( spl107_1
| ~ spl107_100
| ~ spl107_102
| ~ spl107_104 ),
inference(sat_conversion,[],[f884]) ).
cnf(s765,plain,
( spl107_90
| ~ spl107_91 ),
inference(sat_conversion,[],[f885]) ).
cnf(s766,plain,
( ~ spl107_87
| ~ spl107_102 ),
inference(sat_conversion,[],[f887]) ).
cnf(s767,plain,
( ~ spl107_88
| ~ spl107_100 ),
inference(sat_conversion,[],[f889]) ).
cnf(s790,plain,
( spl107_100
| spl107_106 ),
inference(sat_conversion,[],[f909]) ).
cnf(s797,plain,
( spl107_100
| spl107_107 ),
inference(sat_conversion,[],[f915]) ).
cnf(s801,plain,
( spl107_100
| spl107_108 ),
inference(sat_conversion,[],[f919]) ).
cnf(s807,plain,
( spl107_4
| ~ spl107_101 ),
inference(sat_conversion,[],[f925]) ).
cnf(s833,plain,
( spl107_3
| ~ spl107_106
| ~ spl107_107
| ~ spl107_108 ),
inference(sat_conversion,[],[f940]) ).
cnf(s863,plain,
( spl107_102
| spl107_109 ),
inference(sat_conversion,[],[f962]) ).
cnf(s866,plain,
( spl107_83
| ~ spl107_109 ),
inference(sat_conversion,[],[f964]) ).
cnf(s870,plain,
( spl107_102
| spl107_110 ),
inference(sat_conversion,[],[f968]) ).
cnf(s874,plain,
( spl107_102
| spl107_111 ),
inference(sat_conversion,[],[f972]) ).
cnf(s877,plain,
( spl107_97
| ~ spl107_111 ),
inference(sat_conversion,[],[f974]) ).
cnf(s878,plain,
( spl107_93
| ~ spl107_110 ),
inference(sat_conversion,[],[f976]) ).
cnf(s880,plain,
( spl107_6
| ~ spl107_103 ),
inference(sat_conversion,[],[f978]) ).
cnf(s932,plain,
( spl107_104
| spl107_112 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s935,plain,
( spl107_82
| ~ spl107_112 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s940,plain,
( spl107_104
| spl107_113 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s943,plain,
( spl107_92
| ~ spl107_113 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s948,plain,
( spl107_104
| spl107_114 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s951,plain,
( spl107_96
| ~ spl107_114 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s953,plain,
( spl107_8
| ~ spl107_105 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s955,plain,
spl107_104,
inference(rat,[],[s347,s665,s953,s935,s943,s951,s741,s932,s940,s948]) ).
cnf(s956,plain,
~ spl107_86,
inference(rat,[],[s744,s955]) ).
cnf(s957,plain,
spl107_102,
inference(rat,[],[s343,s669,s880,s866,s878,s877,s736,s863,s870,s874]) ).
cnf(s958,plain,
~ spl107_87,
inference(rat,[],[s766,s957]) ).
cnf(s959,plain,
spl107_100,
inference(rat,[],[s339,s807,s833,s731,s790,s797,s801]) ).
cnf(s963,plain,
~ spl107_88,
inference(rat,[],[s767,s959]) ).
cnf(s964,plain,
spl107_1,
inference(rat,[],[s763,s955,s957,s959]) ).
cnf(s965,plain,
spl107_91,
inference(rat,[],[s635,s958,s956,s963]) ).
cnf(s966,plain,
~ spl107_2,
inference(rat,[],[s335,s964]) ).
cnf(s967,plain,
spl107_90,
inference(rat,[],[s765,s965]) ).
cnf(s968,plain,
$false,
inference(rat,[],[s757,s967,s966]) ).
tff(f1036,plain,
$false,
inference(avatar_sat_refutation,[],[s968]) ).
%------------------------------------------------------------------------------
%----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 SAT
% 0.14/0.40 % Computer : n014.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 17:07:31 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.46 Running first-order model finding
% 0.14/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.52 % (1021415)Will run a generic schedule for satisfiability detection.
% 0.22/0.52 % (1021422)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2752281782:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.22/0.52 % (1021420)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3168082668_2999 on theBenchmark for (2999ds/0Mi)
% 0.22/0.52 % (1021421)% WARNING: option uhcvi not known.
% 0.22/0.52 % (1021423)dis+10_1_sil=32000:sp=arity:random_seed=1801872197:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.22/0.52 % (1021424)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3724917190:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.22/0.52 % (1021421)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3603592846:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.22/0.52 % (1021425)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3291110401:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.52 % (1021426)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3397327089:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.22/0.52 % (1021422) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1021415-1021422"...
% 0.22/0.52 % (1021422)...printing done.
% 0.22/0.52 % (1021422)Refutation found. Thanks to Tanya!
% 0.22/0.52 % SZS status Theorem for theBenchmark
% 0.22/0.52 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/0.52 % (1021422)------------------------------
% 0.22/0.52 % (1021422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.52 % (1021422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.52 % (1021422)CaDiCaL version: 2.1.3
% 0.22/0.52 % (1021422)Termination reason: Refutation
% 0.22/0.52 % (1021422)Time elapsed: 0.023 s
% 0.22/0.52 % (1021422)Peak memory usage: 14 MB
% 0.22/0.52 % (1021422)Instructions burned: 49 (million)
% 0.22/0.52 % (1021415)Success in time 0.053 s
% 0.22/0.52 % Vampire exiting
%------------------------------------------------------------------------------