%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL942_2 : 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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:01:12 PM UTC 2026
% Result : Theorem 5.05s 1.15s
% Output : Refutation 5.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 31
% Syntax : Number of formulae : 455 ( 13 unt; 0 typ; 29 def)
% Number of atoms : 4132 ( 0 equ)
% Maximal formula atoms : 66 ( 9 avg)
% Number of connectives : 3096 (1159 ~;1561 |; 256 &)
% ( 18 <=>; 102 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 1740 (1740 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 38 ( 37 usr; 23 prp; 0-3 aty)
% Number of functors : 101 ( 101 usr; 2 con; 0-3 aty)
% Number of variables : 453 ( 0 sgn 369 !; 84 ?; 453 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_8,type,
sK11: '$ki_world' > $i ).
tff(func_def_9,type,
sK12: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_10,type,
sK13: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_11,type,
sK14: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_12,type,
sK15: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_13,type,
sK16: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_14,type,
sK17: ( $i * $i * '$ki_world' ) > '$ki_world' ).
tff(func_def_15,type,
sK18: '$ki_world' > '$ki_world' ).
tff(func_def_16,type,
sK19: '$ki_world' > '$ki_world' ).
tff(func_def_17,type,
sK20: '$ki_world' > '$ki_world' ).
tff(func_def_18,type,
sK21: '$ki_world' > '$ki_world' ).
tff(func_def_19,type,
sK22: '$ki_world' > '$ki_world' ).
tff(func_def_20,type,
sK23: '$ki_world' > '$ki_world' ).
tff(func_def_21,type,
sK24: '$ki_world' > '$ki_world' ).
tff(func_def_22,type,
sK25: '$ki_world' > '$ki_world' ).
tff(func_def_23,type,
sK26: '$ki_world' > '$ki_world' ).
tff(func_def_24,type,
sK27: '$ki_world' > '$ki_world' ).
tff(func_def_25,type,
sK28: '$ki_world' > '$ki_world' ).
tff(func_def_26,type,
sK29: '$ki_world' > '$ki_world' ).
tff(func_def_27,type,
sK30: '$ki_world' > '$ki_world' ).
tff(func_def_28,type,
sK31: '$ki_world' > '$ki_world' ).
tff(func_def_29,type,
sK32: '$ki_world' > '$ki_world' ).
tff(func_def_30,type,
sK33: '$ki_world' > '$ki_world' ).
tff(func_def_31,type,
sK34: '$ki_world' > '$ki_world' ).
tff(func_def_32,type,
sK35: '$ki_world' > '$ki_world' ).
tff(func_def_33,type,
sK36: '$ki_world' > '$ki_world' ).
tff(func_def_34,type,
sK37: '$ki_world' > '$ki_world' ).
tff(func_def_35,type,
sK38: '$ki_world' > '$ki_world' ).
tff(func_def_36,type,
sK39: '$ki_world' > '$ki_world' ).
tff(func_def_37,type,
sK40: '$ki_world' > '$ki_world' ).
tff(func_def_38,type,
sK41: '$ki_world' > '$ki_world' ).
tff(func_def_39,type,
sK42: '$ki_world' > '$ki_world' ).
tff(func_def_40,type,
sK43: '$ki_world' > '$ki_world' ).
tff(func_def_41,type,
sK44: '$ki_world' > '$ki_world' ).
tff(func_def_42,type,
sK45: '$ki_world' > '$ki_world' ).
tff(func_def_43,type,
sK46: '$ki_world' > '$ki_world' ).
tff(func_def_44,type,
sK47: '$ki_world' > '$ki_world' ).
tff(func_def_45,type,
sK48: '$ki_world' > '$ki_world' ).
tff(func_def_46,type,
sK49: '$ki_world' > '$ki_world' ).
tff(func_def_47,type,
sK50: '$ki_world' > '$ki_world' ).
tff(func_def_48,type,
sK51: '$ki_world' > '$ki_world' ).
tff(func_def_49,type,
sK52: '$ki_world' > '$ki_world' ).
tff(func_def_50,type,
sK53: '$ki_world' > '$ki_world' ).
tff(func_def_51,type,
sK54: '$ki_world' > '$ki_world' ).
tff(func_def_52,type,
sK55: '$ki_world' > '$ki_world' ).
tff(func_def_53,type,
sK56: '$ki_world' > '$ki_world' ).
tff(func_def_54,type,
sK57: '$ki_world' > '$ki_world' ).
tff(func_def_55,type,
sK58: '$ki_world' > '$ki_world' ).
tff(func_def_56,type,
sK59: '$ki_world' > '$ki_world' ).
tff(func_def_57,type,
sK60: '$ki_world' > '$ki_world' ).
tff(func_def_58,type,
sK61: '$ki_world' > '$ki_world' ).
tff(func_def_59,type,
sK62: '$ki_world' > '$ki_world' ).
tff(func_def_60,type,
sK63: '$ki_world' > '$ki_world' ).
tff(func_def_61,type,
sK64: '$ki_world' > '$ki_world' ).
tff(func_def_62,type,
sK65: '$ki_world' > '$ki_world' ).
tff(func_def_63,type,
sK66: '$ki_world' > '$ki_world' ).
tff(func_def_64,type,
sK67: '$ki_world' > '$ki_world' ).
tff(func_def_65,type,
sK68: '$ki_world' > '$ki_world' ).
tff(func_def_66,type,
sK69: '$ki_world' > '$ki_world' ).
tff(func_def_67,type,
sK70: '$ki_world' > '$ki_world' ).
tff(func_def_68,type,
sK71: '$ki_world' > '$ki_world' ).
tff(func_def_69,type,
sK72: '$ki_world' > '$ki_world' ).
tff(func_def_70,type,
sK73: '$ki_world' > '$ki_world' ).
tff(func_def_71,type,
sK74: '$ki_world' > '$ki_world' ).
tff(func_def_72,type,
sK75: '$ki_world' > '$ki_world' ).
tff(func_def_73,type,
sK76: '$ki_world' > '$ki_world' ).
tff(func_def_74,type,
sK77: '$ki_world' > '$ki_world' ).
tff(func_def_75,type,
sK78: '$ki_world' > '$ki_world' ).
tff(func_def_76,type,
sK79: '$ki_world' > '$ki_world' ).
tff(func_def_77,type,
sK80: '$ki_world' > '$ki_world' ).
tff(func_def_78,type,
sK81: '$ki_world' > '$ki_world' ).
tff(func_def_79,type,
sK82: '$ki_world' > '$ki_world' ).
tff(func_def_80,type,
sK83: '$ki_world' > '$ki_world' ).
tff(func_def_81,type,
sK84: '$ki_world' > '$ki_world' ).
tff(func_def_82,type,
sK85: '$ki_world' > '$ki_world' ).
tff(func_def_83,type,
sK86: '$ki_world' > '$ki_world' ).
tff(func_def_84,type,
sK87: '$ki_world' > '$ki_world' ).
tff(func_def_85,type,
sK88: '$ki_world' > '$ki_world' ).
tff(func_def_86,type,
sK89: '$ki_world' > '$ki_world' ).
tff(func_def_87,type,
sK90: '$ki_world' > '$ki_world' ).
tff(func_def_88,type,
sK91: '$ki_world' > '$ki_world' ).
tff(func_def_89,type,
sK92: '$ki_world' > '$ki_world' ).
tff(func_def_90,type,
sK93: '$ki_world' > '$ki_world' ).
tff(func_def_91,type,
sK94: '$ki_world' > '$ki_world' ).
tff(func_def_92,type,
sK95: '$ki_world' > '$ki_world' ).
tff(func_def_93,type,
sK96: '$ki_world' > '$ki_world' ).
tff(func_def_94,type,
sK97: '$ki_world' > '$ki_world' ).
tff(func_def_95,type,
sK98: '$ki_world' > '$ki_world' ).
tff(func_def_96,type,
sK99: '$ki_world' > '$ki_world' ).
tff(func_def_97,type,
sK100: '$ki_world' > '$ki_world' ).
tff(func_def_98,type,
sK101: '$ki_world' > '$ki_world' ).
tff(func_def_99,type,
sK102: '$ki_world' > '$ki_world' ).
tff(func_def_100,type,
sK103: '$ki_world' > '$ki_world' ).
tff(func_def_101,type,
sK104: '$ki_world' > '$ki_world' ).
tff(func_def_102,type,
sK105: '$ki_world' > '$ki_world' ).
tff(func_def_103,type,
sK106: '$ki_world' > '$ki_world' ).
tff(func_def_104,type,
sK107: '$ki_world' > '$ki_world' ).
tff(func_def_105,type,
sK108: '$ki_world' > '$ki_world' ).
tff(func_def_106,type,
sK109: '$ki_world' > '$ki_world' ).
tff(func_def_107,type,
sK110: '$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(pred_def_7,type,
sP3: '$ki_world' > $o ).
tff(pred_def_8,type,
sP4: '$ki_world' > $o ).
tff(pred_def_9,type,
sP5: '$ki_world' > $o ).
tff(pred_def_10,type,
sP6: '$ki_world' > $o ).
tff(pred_def_11,type,
sP7: '$ki_world' > $o ).
tff(pred_def_12,type,
sP8: '$ki_world' > $o ).
tff(pred_def_13,type,
sP9: '$ki_world' > $o ).
tff(pred_def_14,type,
sP10: '$ki_world' > $o ).
tff(f1,axiom,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_reflexive) ).
tff(f21,conjecture,
! [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) ) ) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ~ ( ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e0) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e1) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e2) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,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)
=> ~ ( ( ( ! [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) ) ) )
& ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> ~ ( ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e0) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e1) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e1) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e2) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e2) ) )
| ( ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e0,e0),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e1,e1),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e2,e2),e3) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X1,X2)
=> qmltpeq(X2,op(e3,e3),e3) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f21]) ).
tff(f38,plain,
~ ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ~ ( ( ( ! [X1: '$ki_world'] :
( '$ki_accessible'(X0,X1)
=> qmltpeq(X1,op(e0,e0),e0) )
& ! [X2: '$ki_world'] :
( '$ki_accessible'(X0,X2)
=> qmltpeq(X2,op(e1,e1),e0) )
& ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> qmltpeq(X3,op(e2,e2),e0) )
& ! [X4: '$ki_world'] :
( '$ki_accessible'(X0,X4)
=> qmltpeq(X4,op(e3,e3),e0) ) )
| ( ! [X5: '$ki_world'] :
( '$ki_accessible'(X0,X5)
=> qmltpeq(X5,op(e0,e0),e1) )
& ! [X6: '$ki_world'] :
( '$ki_accessible'(X0,X6)
=> qmltpeq(X6,op(e1,e1),e1) )
& ! [X7: '$ki_world'] :
( '$ki_accessible'(X0,X7)
=> qmltpeq(X7,op(e2,e2),e1) )
& ! [X8: '$ki_world'] :
( '$ki_accessible'(X0,X8)
=> qmltpeq(X8,op(e3,e3),e1) ) )
| ( ! [X9: '$ki_world'] :
( '$ki_accessible'(X0,X9)
=> qmltpeq(X9,op(e0,e0),e2) )
& ! [X10: '$ki_world'] :
( '$ki_accessible'(X0,X10)
=> qmltpeq(X10,op(e1,e1),e2) )
& ! [X11: '$ki_world'] :
( '$ki_accessible'(X0,X11)
=> qmltpeq(X11,op(e2,e2),e2) )
& ! [X12: '$ki_world'] :
( '$ki_accessible'(X0,X12)
=> qmltpeq(X12,op(e3,e3),e2) ) )
| ( ! [X13: '$ki_world'] :
( '$ki_accessible'(X0,X13)
=> qmltpeq(X13,op(e0,e0),e3) )
& ! [X14: '$ki_world'] :
( '$ki_accessible'(X0,X14)
=> qmltpeq(X14,op(e1,e1),e3) )
& ! [X15: '$ki_world'] :
( '$ki_accessible'(X0,X15)
=> qmltpeq(X15,op(e2,e2),e3) )
& ! [X16: '$ki_world'] :
( '$ki_accessible'(X0,X16)
=> qmltpeq(X16,op(e3,e3),e3) ) ) )
& ! [X17: '$ki_world'] :
( '$ki_accessible'(X0,X17)
=> ~ ( ( ! [X18: '$ki_world'] :
( '$ki_accessible'(X17,X18)
=> qmltpeq(X18,op(e0,e0),e0) )
& ! [X19: '$ki_world'] :
( '$ki_accessible'(X17,X19)
=> qmltpeq(X19,op(e1,e1),e0) )
& ! [X20: '$ki_world'] :
( '$ki_accessible'(X17,X20)
=> qmltpeq(X20,op(e2,e2),e0) )
& ! [X21: '$ki_world'] :
( '$ki_accessible'(X17,X21)
=> qmltpeq(X21,op(e3,e3),e0) ) )
| ( ! [X22: '$ki_world'] :
( '$ki_accessible'(X17,X22)
=> qmltpeq(X22,op(e0,e0),e1) )
& ! [X23: '$ki_world'] :
( '$ki_accessible'(X17,X23)
=> qmltpeq(X23,op(e1,e1),e1) )
& ! [X24: '$ki_world'] :
( '$ki_accessible'(X17,X24)
=> qmltpeq(X24,op(e2,e2),e1) )
& ! [X25: '$ki_world'] :
( '$ki_accessible'(X17,X25)
=> qmltpeq(X25,op(e3,e3),e1) ) )
| ( ! [X26: '$ki_world'] :
( '$ki_accessible'(X17,X26)
=> qmltpeq(X26,op(e0,e0),e2) )
& ! [X27: '$ki_world'] :
( '$ki_accessible'(X17,X27)
=> qmltpeq(X27,op(e1,e1),e2) )
& ! [X28: '$ki_world'] :
( '$ki_accessible'(X17,X28)
=> qmltpeq(X28,op(e2,e2),e2) )
& ! [X29: '$ki_world'] :
( '$ki_accessible'(X17,X29)
=> qmltpeq(X29,op(e3,e3),e2) ) )
| ( ! [X30: '$ki_world'] :
( '$ki_accessible'(X17,X30)
=> qmltpeq(X30,op(e0,e0),e3) )
& ! [X31: '$ki_world'] :
( '$ki_accessible'(X17,X31)
=> qmltpeq(X31,op(e1,e1),e3) )
& ! [X32: '$ki_world'] :
( '$ki_accessible'(X17,X32)
=> qmltpeq(X32,op(e2,e2),e3) )
& ! [X33: '$ki_world'] :
( '$ki_accessible'(X17,X33)
=> qmltpeq(X33,op(e3,e3),e3) ) ) ) ) ) ),
inference(rectify,[],[f22]) ).
tff(f62,plain,
? [X0: '$ki_world'] :
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(X0,X4) ) )
| ( ! [X5: '$ki_world'] :
( qmltpeq(X5,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X5) )
& ! [X6: '$ki_world'] :
( qmltpeq(X6,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X6) )
& ! [X7: '$ki_world'] :
( qmltpeq(X7,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X7) )
& ! [X8: '$ki_world'] :
( qmltpeq(X8,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X8) ) )
| ( ! [X9: '$ki_world'] :
( qmltpeq(X9,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X9) )
& ! [X10: '$ki_world'] :
( qmltpeq(X10,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X10) )
& ! [X11: '$ki_world'] :
( qmltpeq(X11,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X11) )
& ! [X12: '$ki_world'] :
( qmltpeq(X12,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X12) ) )
| ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X16) ) ) )
& ! [X17: '$ki_world'] :
( ( ( ? [X18: '$ki_world'] :
( ~ qmltpeq(X18,op(e0,e0),e0)
& '$ki_accessible'(X17,X18) )
| ? [X19: '$ki_world'] :
( ~ qmltpeq(X19,op(e1,e1),e0)
& '$ki_accessible'(X17,X19) )
| ? [X20: '$ki_world'] :
( ~ qmltpeq(X20,op(e2,e2),e0)
& '$ki_accessible'(X17,X20) )
| ? [X21: '$ki_world'] :
( ~ qmltpeq(X21,op(e3,e3),e0)
& '$ki_accessible'(X17,X21) ) )
& ( ? [X22: '$ki_world'] :
( ~ qmltpeq(X22,op(e0,e0),e1)
& '$ki_accessible'(X17,X22) )
| ? [X23: '$ki_world'] :
( ~ qmltpeq(X23,op(e1,e1),e1)
& '$ki_accessible'(X17,X23) )
| ? [X24: '$ki_world'] :
( ~ qmltpeq(X24,op(e2,e2),e1)
& '$ki_accessible'(X17,X24) )
| ? [X25: '$ki_world'] :
( ~ qmltpeq(X25,op(e3,e3),e1)
& '$ki_accessible'(X17,X25) ) )
& ( ? [X26: '$ki_world'] :
( ~ qmltpeq(X26,op(e0,e0),e2)
& '$ki_accessible'(X17,X26) )
| ? [X27: '$ki_world'] :
( ~ qmltpeq(X27,op(e1,e1),e2)
& '$ki_accessible'(X17,X27) )
| ? [X28: '$ki_world'] :
( ~ qmltpeq(X28,op(e2,e2),e2)
& '$ki_accessible'(X17,X28) )
| ? [X29: '$ki_world'] :
( ~ qmltpeq(X29,op(e3,e3),e2)
& '$ki_accessible'(X17,X29) ) )
& ( ? [X30: '$ki_world'] :
( ~ qmltpeq(X30,op(e0,e0),e3)
& '$ki_accessible'(X17,X30) )
| ? [X31: '$ki_world'] :
( ~ qmltpeq(X31,op(e1,e1),e3)
& '$ki_accessible'(X17,X31) )
| ? [X32: '$ki_world'] :
( ~ qmltpeq(X32,op(e2,e2),e3)
& '$ki_accessible'(X17,X32) )
| ? [X33: '$ki_world'] :
( ~ qmltpeq(X33,op(e3,e3),e3)
& '$ki_accessible'(X17,X33) ) ) )
| ~ '$ki_accessible'(X0,X17) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f38]) ).
tff(f63,plain,
? [X0: '$ki_world'] :
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(X0,X4) ) )
| ( ! [X5: '$ki_world'] :
( qmltpeq(X5,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X5) )
& ! [X6: '$ki_world'] :
( qmltpeq(X6,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X6) )
& ! [X7: '$ki_world'] :
( qmltpeq(X7,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X7) )
& ! [X8: '$ki_world'] :
( qmltpeq(X8,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X8) ) )
| ( ! [X9: '$ki_world'] :
( qmltpeq(X9,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X9) )
& ! [X10: '$ki_world'] :
( qmltpeq(X10,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X10) )
& ! [X11: '$ki_world'] :
( qmltpeq(X11,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X11) )
& ! [X12: '$ki_world'] :
( qmltpeq(X12,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X12) ) )
| ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X16) ) ) )
& ! [X17: '$ki_world'] :
( ( ( ? [X18: '$ki_world'] :
( ~ qmltpeq(X18,op(e0,e0),e0)
& '$ki_accessible'(X17,X18) )
| ? [X19: '$ki_world'] :
( ~ qmltpeq(X19,op(e1,e1),e0)
& '$ki_accessible'(X17,X19) )
| ? [X20: '$ki_world'] :
( ~ qmltpeq(X20,op(e2,e2),e0)
& '$ki_accessible'(X17,X20) )
| ? [X21: '$ki_world'] :
( ~ qmltpeq(X21,op(e3,e3),e0)
& '$ki_accessible'(X17,X21) ) )
& ( ? [X22: '$ki_world'] :
( ~ qmltpeq(X22,op(e0,e0),e1)
& '$ki_accessible'(X17,X22) )
| ? [X23: '$ki_world'] :
( ~ qmltpeq(X23,op(e1,e1),e1)
& '$ki_accessible'(X17,X23) )
| ? [X24: '$ki_world'] :
( ~ qmltpeq(X24,op(e2,e2),e1)
& '$ki_accessible'(X17,X24) )
| ? [X25: '$ki_world'] :
( ~ qmltpeq(X25,op(e3,e3),e1)
& '$ki_accessible'(X17,X25) ) )
& ( ? [X26: '$ki_world'] :
( ~ qmltpeq(X26,op(e0,e0),e2)
& '$ki_accessible'(X17,X26) )
| ? [X27: '$ki_world'] :
( ~ qmltpeq(X27,op(e1,e1),e2)
& '$ki_accessible'(X17,X27) )
| ? [X28: '$ki_world'] :
( ~ qmltpeq(X28,op(e2,e2),e2)
& '$ki_accessible'(X17,X28) )
| ? [X29: '$ki_world'] :
( ~ qmltpeq(X29,op(e3,e3),e2)
& '$ki_accessible'(X17,X29) ) )
& ( ? [X30: '$ki_world'] :
( ~ qmltpeq(X30,op(e0,e0),e3)
& '$ki_accessible'(X17,X30) )
| ? [X31: '$ki_world'] :
( ~ qmltpeq(X31,op(e1,e1),e3)
& '$ki_accessible'(X17,X31) )
| ? [X32: '$ki_world'] :
( ~ qmltpeq(X32,op(e2,e2),e3)
& '$ki_accessible'(X17,X32) )
| ? [X33: '$ki_world'] :
( ~ qmltpeq(X33,op(e3,e3),e3)
& '$ki_accessible'(X17,X33) ) ) )
| ~ '$ki_accessible'(X0,X17) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(flattening,[],[f62]) ).
tff(f64,definition,
! [X17: '$ki_world'] :
( ? [X33: '$ki_world'] :
( ~ qmltpeq(X33,op(e3,e3),e3)
& '$ki_accessible'(X17,X33) )
| ~ sP0(X17) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f65,definition,
! [X17: '$ki_world'] :
( ? [X29: '$ki_world'] :
( ~ qmltpeq(X29,op(e3,e3),e2)
& '$ki_accessible'(X17,X29) )
| ~ sP1(X17) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f66,definition,
! [X17: '$ki_world'] :
( ? [X25: '$ki_world'] :
( ~ qmltpeq(X25,op(e3,e3),e1)
& '$ki_accessible'(X17,X25) )
| ~ sP2(X17) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f67,definition,
! [X17: '$ki_world'] :
( ? [X21: '$ki_world'] :
( ~ qmltpeq(X21,op(e3,e3),e0)
& '$ki_accessible'(X17,X21) )
| ~ sP3(X17) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f68,definition,
! [X17: '$ki_world'] :
( ? [X30: '$ki_world'] :
( ~ qmltpeq(X30,op(e0,e0),e3)
& '$ki_accessible'(X17,X30) )
| ? [X31: '$ki_world'] :
( ~ qmltpeq(X31,op(e1,e1),e3)
& '$ki_accessible'(X17,X31) )
| ? [X32: '$ki_world'] :
( ~ qmltpeq(X32,op(e2,e2),e3)
& '$ki_accessible'(X17,X32) )
| sP0(X17)
| ~ sP4(X17) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
tff(f69,definition,
! [X17: '$ki_world'] :
( ? [X26: '$ki_world'] :
( ~ qmltpeq(X26,op(e0,e0),e2)
& '$ki_accessible'(X17,X26) )
| ? [X27: '$ki_world'] :
( ~ qmltpeq(X27,op(e1,e1),e2)
& '$ki_accessible'(X17,X27) )
| ? [X28: '$ki_world'] :
( ~ qmltpeq(X28,op(e2,e2),e2)
& '$ki_accessible'(X17,X28) )
| sP1(X17)
| ~ sP5(X17) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
tff(f70,definition,
! [X17: '$ki_world'] :
( ? [X22: '$ki_world'] :
( ~ qmltpeq(X22,op(e0,e0),e1)
& '$ki_accessible'(X17,X22) )
| ? [X23: '$ki_world'] :
( ~ qmltpeq(X23,op(e1,e1),e1)
& '$ki_accessible'(X17,X23) )
| ? [X24: '$ki_world'] :
( ~ qmltpeq(X24,op(e2,e2),e1)
& '$ki_accessible'(X17,X24) )
| sP2(X17)
| ~ sP6(X17) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
tff(f71,definition,
! [X17: '$ki_world'] :
( ? [X18: '$ki_world'] :
( ~ qmltpeq(X18,op(e0,e0),e0)
& '$ki_accessible'(X17,X18) )
| ? [X19: '$ki_world'] :
( ~ qmltpeq(X19,op(e1,e1),e0)
& '$ki_accessible'(X17,X19) )
| ? [X20: '$ki_world'] :
( ~ qmltpeq(X20,op(e2,e2),e0)
& '$ki_accessible'(X17,X20) )
| sP3(X17)
| ~ sP7(X17) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
tff(f72,definition,
! [X0: '$ki_world'] :
( ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X16) ) )
| ~ sP8(X0) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
tff(f73,definition,
! [X0: '$ki_world'] :
( ( ! [X9: '$ki_world'] :
( qmltpeq(X9,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X9) )
& ! [X10: '$ki_world'] :
( qmltpeq(X10,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X10) )
& ! [X11: '$ki_world'] :
( qmltpeq(X11,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X11) )
& ! [X12: '$ki_world'] :
( qmltpeq(X12,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X12) ) )
| ~ sP9(X0) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
tff(f74,definition,
! [X0: '$ki_world'] :
( ( ! [X5: '$ki_world'] :
( qmltpeq(X5,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X5) )
& ! [X6: '$ki_world'] :
( qmltpeq(X6,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X6) )
& ! [X7: '$ki_world'] :
( qmltpeq(X7,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X7) )
& ! [X8: '$ki_world'] :
( qmltpeq(X8,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X8) ) )
| ~ sP10(X0) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
tff(f75,plain,
? [X0: '$ki_world'] :
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(X0,X4) ) )
| sP10(X0)
| sP9(X0)
| sP8(X0) )
& ! [X17: '$ki_world'] :
( ( sP7(X17)
& sP6(X17)
& sP5(X17)
& sP4(X17) )
| ~ '$ki_accessible'(X0,X17) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(definition_folding,[],[f63,f74,f73,f72,f71,f70,f69,f68,f67,f66,f65,f64]) ).
tff(f92,plain,
! [X0: '$ki_world'] :
( ( ! [X5: '$ki_world'] :
( qmltpeq(X5,op(e0,e0),e1)
| ~ '$ki_accessible'(X0,X5) )
& ! [X6: '$ki_world'] :
( qmltpeq(X6,op(e1,e1),e1)
| ~ '$ki_accessible'(X0,X6) )
& ! [X7: '$ki_world'] :
( qmltpeq(X7,op(e2,e2),e1)
| ~ '$ki_accessible'(X0,X7) )
& ! [X8: '$ki_world'] :
( qmltpeq(X8,op(e3,e3),e1)
| ~ '$ki_accessible'(X0,X8) ) )
| ~ sP10(X0) ),
inference(nnf_transformation,[],[f74]) ).
tff(f93,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) ) )
| ~ sP10(X0) ),
inference(rectify,[],[f92]) ).
tff(f94,plain,
! [X0: '$ki_world'] :
( ( ! [X9: '$ki_world'] :
( qmltpeq(X9,op(e0,e0),e2)
| ~ '$ki_accessible'(X0,X9) )
& ! [X10: '$ki_world'] :
( qmltpeq(X10,op(e1,e1),e2)
| ~ '$ki_accessible'(X0,X10) )
& ! [X11: '$ki_world'] :
( qmltpeq(X11,op(e2,e2),e2)
| ~ '$ki_accessible'(X0,X11) )
& ! [X12: '$ki_world'] :
( qmltpeq(X12,op(e3,e3),e2)
| ~ '$ki_accessible'(X0,X12) ) )
| ~ sP9(X0) ),
inference(nnf_transformation,[],[f73]) ).
tff(f95,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) ) )
| ~ sP9(X0) ),
inference(rectify,[],[f94]) ).
tff(f96,plain,
! [X0: '$ki_world'] :
( ( ! [X13: '$ki_world'] :
( qmltpeq(X13,op(e0,e0),e3)
| ~ '$ki_accessible'(X0,X13) )
& ! [X14: '$ki_world'] :
( qmltpeq(X14,op(e1,e1),e3)
| ~ '$ki_accessible'(X0,X14) )
& ! [X15: '$ki_world'] :
( qmltpeq(X15,op(e2,e2),e3)
| ~ '$ki_accessible'(X0,X15) )
& ! [X16: '$ki_world'] :
( qmltpeq(X16,op(e3,e3),e3)
| ~ '$ki_accessible'(X0,X16) ) )
| ~ sP8(X0) ),
inference(nnf_transformation,[],[f72]) ).
tff(f97,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) ) )
| ~ sP8(X0) ),
inference(rectify,[],[f96]) ).
tff(f98,plain,
! [X17: '$ki_world'] :
( ? [X18: '$ki_world'] :
( ~ qmltpeq(X18,op(e0,e0),e0)
& '$ki_accessible'(X17,X18) )
| ? [X19: '$ki_world'] :
( ~ qmltpeq(X19,op(e1,e1),e0)
& '$ki_accessible'(X17,X19) )
| ? [X20: '$ki_world'] :
( ~ qmltpeq(X20,op(e2,e2),e0)
& '$ki_accessible'(X17,X20) )
| sP3(X17)
| ~ sP7(X17) ),
inference(nnf_transformation,[],[f71]) ).
tff(f99,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e0,e0),e0)
& '$ki_accessible'(X0,X1) )
| ? [X2: '$ki_world'] :
( ~ qmltpeq(X2,op(e1,e1),e0)
& '$ki_accessible'(X0,X2) )
| ? [X3: '$ki_world'] :
( ~ qmltpeq(X3,op(e2,e2),e0)
& '$ki_accessible'(X0,X3) )
| sP3(X0)
| ~ sP7(X0) ),
inference(rectify,[],[f98]) ).
tff(f100,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK94(X0),op(e0,e0),e0)
& '$ki_accessible'(X0,sK94(X0)) )
| ( ~ qmltpeq(sK95(X0),op(e1,e1),e0)
& '$ki_accessible'(X0,sK95(X0)) )
| ( ~ qmltpeq(sK96(X0),op(e2,e2),e0)
& '$ki_accessible'(X0,sK96(X0)) )
| sP3(X0)
| ~ sP7(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94,sK95,sK96]),skolemize(X1,sK94(X0)),skolemize(X2,sK95(X0)),skolemize(X3,sK96(X0))],[f99]) ).
tff(f101,plain,
! [X17: '$ki_world'] :
( ? [X22: '$ki_world'] :
( ~ qmltpeq(X22,op(e0,e0),e1)
& '$ki_accessible'(X17,X22) )
| ? [X23: '$ki_world'] :
( ~ qmltpeq(X23,op(e1,e1),e1)
& '$ki_accessible'(X17,X23) )
| ? [X24: '$ki_world'] :
( ~ qmltpeq(X24,op(e2,e2),e1)
& '$ki_accessible'(X17,X24) )
| sP2(X17)
| ~ sP6(X17) ),
inference(nnf_transformation,[],[f70]) ).
tff(f102,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) )
| sP2(X0)
| ~ sP6(X0) ),
inference(rectify,[],[f101]) ).
tff(f103,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK97(X0),op(e0,e0),e1)
& '$ki_accessible'(X0,sK97(X0)) )
| ( ~ qmltpeq(sK98(X0),op(e1,e1),e1)
& '$ki_accessible'(X0,sK98(X0)) )
| ( ~ qmltpeq(sK99(X0),op(e2,e2),e1)
& '$ki_accessible'(X0,sK99(X0)) )
| sP2(X0)
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK97,sK98,sK99]),skolemize(X1,sK97(X0)),skolemize(X2,sK98(X0)),skolemize(X3,sK99(X0))],[f102]) ).
tff(f104,plain,
! [X17: '$ki_world'] :
( ? [X26: '$ki_world'] :
( ~ qmltpeq(X26,op(e0,e0),e2)
& '$ki_accessible'(X17,X26) )
| ? [X27: '$ki_world'] :
( ~ qmltpeq(X27,op(e1,e1),e2)
& '$ki_accessible'(X17,X27) )
| ? [X28: '$ki_world'] :
( ~ qmltpeq(X28,op(e2,e2),e2)
& '$ki_accessible'(X17,X28) )
| sP1(X17)
| ~ sP5(X17) ),
inference(nnf_transformation,[],[f69]) ).
tff(f105,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) )
| sP1(X0)
| ~ sP5(X0) ),
inference(rectify,[],[f104]) ).
tff(f106,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK100(X0),op(e0,e0),e2)
& '$ki_accessible'(X0,sK100(X0)) )
| ( ~ qmltpeq(sK101(X0),op(e1,e1),e2)
& '$ki_accessible'(X0,sK101(X0)) )
| ( ~ qmltpeq(sK102(X0),op(e2,e2),e2)
& '$ki_accessible'(X0,sK102(X0)) )
| sP1(X0)
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100,sK101,sK102]),skolemize(X1,sK100(X0)),skolemize(X2,sK101(X0)),skolemize(X3,sK102(X0))],[f105]) ).
tff(f107,plain,
! [X17: '$ki_world'] :
( ? [X30: '$ki_world'] :
( ~ qmltpeq(X30,op(e0,e0),e3)
& '$ki_accessible'(X17,X30) )
| ? [X31: '$ki_world'] :
( ~ qmltpeq(X31,op(e1,e1),e3)
& '$ki_accessible'(X17,X31) )
| ? [X32: '$ki_world'] :
( ~ qmltpeq(X32,op(e2,e2),e3)
& '$ki_accessible'(X17,X32) )
| sP0(X17)
| ~ sP4(X17) ),
inference(nnf_transformation,[],[f68]) ).
tff(f108,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) )
| sP0(X0)
| ~ sP4(X0) ),
inference(rectify,[],[f107]) ).
tff(f109,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK103(X0),op(e0,e0),e3)
& '$ki_accessible'(X0,sK103(X0)) )
| ( ~ qmltpeq(sK104(X0),op(e1,e1),e3)
& '$ki_accessible'(X0,sK104(X0)) )
| ( ~ qmltpeq(sK105(X0),op(e2,e2),e3)
& '$ki_accessible'(X0,sK105(X0)) )
| sP0(X0)
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103,sK104,sK105]),skolemize(X1,sK103(X0)),skolemize(X2,sK104(X0)),skolemize(X3,sK105(X0))],[f108]) ).
tff(f110,plain,
! [X17: '$ki_world'] :
( ? [X21: '$ki_world'] :
( ~ qmltpeq(X21,op(e3,e3),e0)
& '$ki_accessible'(X17,X21) )
| ~ sP3(X17) ),
inference(nnf_transformation,[],[f67]) ).
tff(f111,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e0)
& '$ki_accessible'(X0,X1) )
| ~ sP3(X0) ),
inference(rectify,[],[f110]) ).
tff(f112,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK106(X0),op(e3,e3),e0)
& '$ki_accessible'(X0,sK106(X0)) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK106]),skolemize(X1,sK106(X0))],[f111]) ).
tff(f113,plain,
! [X17: '$ki_world'] :
( ? [X25: '$ki_world'] :
( ~ qmltpeq(X25,op(e3,e3),e1)
& '$ki_accessible'(X17,X25) )
| ~ sP2(X17) ),
inference(nnf_transformation,[],[f66]) ).
tff(f114,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e1)
& '$ki_accessible'(X0,X1) )
| ~ sP2(X0) ),
inference(rectify,[],[f113]) ).
tff(f115,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK107(X0),op(e3,e3),e1)
& '$ki_accessible'(X0,sK107(X0)) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107]),skolemize(X1,sK107(X0))],[f114]) ).
tff(f116,plain,
! [X17: '$ki_world'] :
( ? [X29: '$ki_world'] :
( ~ qmltpeq(X29,op(e3,e3),e2)
& '$ki_accessible'(X17,X29) )
| ~ sP1(X17) ),
inference(nnf_transformation,[],[f65]) ).
tff(f117,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e2)
& '$ki_accessible'(X0,X1) )
| ~ sP1(X0) ),
inference(rectify,[],[f116]) ).
tff(f118,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK108(X0),op(e3,e3),e2)
& '$ki_accessible'(X0,sK108(X0)) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK108]),skolemize(X1,sK108(X0))],[f117]) ).
tff(f119,plain,
! [X17: '$ki_world'] :
( ? [X33: '$ki_world'] :
( ~ qmltpeq(X33,op(e3,e3),e3)
& '$ki_accessible'(X17,X33) )
| ~ sP0(X17) ),
inference(nnf_transformation,[],[f64]) ).
tff(f120,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e3)
& '$ki_accessible'(X0,X1) )
| ~ sP0(X0) ),
inference(rectify,[],[f119]) ).
tff(f121,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK109(X0),op(e3,e3),e3)
& '$ki_accessible'(X0,sK109(X0)) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109]),skolemize(X1,sK109(X0))],[f120]) ).
tff(f122,plain,
? [X0: '$ki_world'] :
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(X0,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(X0,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(X0,X4) ) )
| sP10(X0)
| sP9(X0)
| sP8(X0) )
& ! [X5: '$ki_world'] :
( ( sP7(X5)
& sP6(X5)
& sP5(X5)
& sP4(X5) )
| ~ '$ki_accessible'(X0,X5) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(rectify,[],[f75]) ).
tff(f123,plain,
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK110,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK110,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK110,X4) ) )
| sP10(sK110)
| sP9(sK110)
| sP8(sK110) )
& ! [X5: '$ki_world'] :
( ( sP7(X5)
& sP6(X5)
& sP5(X5)
& sP4(X5) )
| ~ '$ki_accessible'(sK110,X5) )
& '$ki_accessible'('$ki_local_world',sK110) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110]),skolemize(X0,sK110)],[f122]) ).
tff(f124,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f400,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f93]) ).
tff(f401,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f93]) ).
tff(f402,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f93]) ).
tff(f403,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f93]) ).
tff(f404,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f405,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f406,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f407,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f408,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f97]) ).
tff(f409,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f97]) ).
tff(f410,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f97]) ).
tff(f411,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f97]) ).
tff(f412,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK96(X0))
| '$ki_accessible'(X0,sK95(X0))
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f413,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK96(X0),op(e2,e2),e0)
| '$ki_accessible'(X0,sK95(X0))
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f414,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| '$ki_accessible'(X0,sK94(X0))
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f415,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK96(X0),op(e2,e2),e0)
| ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f416,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK95(X0))
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f417,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK96(X0),op(e2,e2),e0)
| '$ki_accessible'(X0,sK95(X0))
| ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f418,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f419,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK96(X0),op(e2,e2),e0)
| ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f420,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK99(X0))
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f421,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK99(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f422,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK97(X0))
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f423,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK99(X0),op(e2,e2),e1)
| ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f424,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK97(X0),op(e0,e0),e1)
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f425,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK99(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK98(X0))
| ~ qmltpeq(sK97(X0),op(e0,e0),e1)
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f426,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| ~ qmltpeq(sK97(X0),op(e0,e0),e1)
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f427,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK99(X0),op(e2,e2),e1)
| ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| ~ qmltpeq(sK97(X0),op(e0,e0),e1)
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f428,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK102(X0))
| '$ki_accessible'(X0,sK101(X0))
| '$ki_accessible'(X0,sK100(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f429,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK102(X0),op(e2,e2),e2)
| '$ki_accessible'(X0,sK101(X0))
| '$ki_accessible'(X0,sK100(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f430,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK101(X0),op(e1,e1),e2)
| '$ki_accessible'(X0,sK100(X0))
| '$ki_accessible'(X0,sK102(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f431,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK102(X0),op(e2,e2),e2)
| ~ qmltpeq(sK101(X0),op(e1,e1),e2)
| '$ki_accessible'(X0,sK100(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f432,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK100(X0),op(e0,e0),e2)
| '$ki_accessible'(X0,sK101(X0))
| '$ki_accessible'(X0,sK102(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f433,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK102(X0),op(e2,e2),e2)
| '$ki_accessible'(X0,sK101(X0))
| ~ qmltpeq(sK100(X0),op(e0,e0),e2)
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f434,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK101(X0),op(e1,e1),e2)
| ~ qmltpeq(sK100(X0),op(e0,e0),e2)
| '$ki_accessible'(X0,sK102(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f435,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK102(X0),op(e2,e2),e2)
| ~ qmltpeq(sK101(X0),op(e1,e1),e2)
| ~ qmltpeq(sK100(X0),op(e0,e0),e2)
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f106]) ).
tff(f436,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK105(X0))
| '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f437,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK105(X0),op(e2,e2),e3)
| '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f438,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK103(X0))
| '$ki_accessible'(X0,sK105(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f439,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK105(X0),op(e2,e2),e3)
| ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f440,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK103(X0),op(e0,e0),e3)
| '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK105(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f441,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK105(X0),op(e2,e2),e3)
| '$ki_accessible'(X0,sK104(X0))
| ~ qmltpeq(sK103(X0),op(e0,e0),e3)
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f442,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| ~ qmltpeq(sK103(X0),op(e0,e0),e3)
| '$ki_accessible'(X0,sK105(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f443,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK105(X0),op(e2,e2),e3)
| ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| ~ qmltpeq(sK103(X0),op(e0,e0),e3)
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f109]) ).
tff(f444,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK106(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f112]) ).
tff(f445,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK106(X0),op(e3,e3),e0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f112]) ).
tff(f446,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK107(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f115]) ).
tff(f447,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK107(X0),op(e3,e3),e1)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f115]) ).
tff(f448,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK108(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f118]) ).
tff(f449,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK108(X0),op(e3,e3),e2)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f118]) ).
tff(f450,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK109(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f121]) ).
tff(f451,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK109(X0),op(e3,e3),e3)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f121]) ).
tff(f453,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK110,X5)
| sP4(X5) ),
inference(cnf_transformation,[],[f123]) ).
tff(f454,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK110,X5)
| sP5(X5) ),
inference(cnf_transformation,[],[f123]) ).
tff(f455,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK110,X5)
| sP6(X5) ),
inference(cnf_transformation,[],[f123]) ).
tff(f456,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK110,X5)
| sP7(X5) ),
inference(cnf_transformation,[],[f123]) ).
tff(f457,plain,
! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK110,X4)
| sP10(sK110)
| sP9(sK110)
| sP8(sK110) ),
inference(cnf_transformation,[],[f123]) ).
tff(f458,plain,
! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3)
| sP10(sK110)
| sP9(sK110)
| sP8(sK110) ),
inference(cnf_transformation,[],[f123]) ).
tff(f459,plain,
! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK110,X2)
| sP10(sK110)
| sP9(sK110)
| sP8(sK110) ),
inference(cnf_transformation,[],[f123]) ).
tff(f460,plain,
! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK110,X1)
| sP10(sK110)
| sP9(sK110)
| sP8(sK110) ),
inference(cnf_transformation,[],[f123]) ).
tff(f677,plain,
sP4(sK110),
inference(resolution,[],[f124,f453]) ).
tff(f682,plain,
sP5(sK110),
inference(resolution,[],[f454,f124]) ).
tff(f686,plain,
sP6(sK110),
inference(resolution,[],[f455,f124]) ).
tff(f690,plain,
sP7(sK110),
inference(resolution,[],[f456,f124]) ).
tff(f692,definition,
( spl111_75
<=> sP8(sK110) ),
introduced(definition,[new_symbols(definition,[spl111_75])],[avatar_definition]) ).
tff(f693,plain,
( ~ sP8(sK110)
| spl111_75 ),
inference(avatar_component_clause,[],[f692]) ).
tff(f694,plain,
( sP8(sK110)
| ~ spl111_75 ),
inference(avatar_component_clause,[],[f692]) ).
tff(f696,definition,
( spl111_76
<=> sP9(sK110) ),
introduced(definition,[new_symbols(definition,[spl111_76])],[avatar_definition]) ).
tff(f697,plain,
( ~ sP9(sK110)
| spl111_76 ),
inference(avatar_component_clause,[],[f696]) ).
tff(f698,plain,
( sP9(sK110)
| ~ spl111_76 ),
inference(avatar_component_clause,[],[f696]) ).
tff(f700,definition,
( spl111_77
<=> sP10(sK110) ),
introduced(definition,[new_symbols(definition,[spl111_77])],[avatar_definition]) ).
tff(f701,plain,
( ~ sP10(sK110)
| spl111_77 ),
inference(avatar_component_clause,[],[f700]) ).
tff(f702,plain,
( sP10(sK110)
| ~ spl111_77 ),
inference(avatar_component_clause,[],[f700]) ).
tff(f707,definition,
( spl111_79
<=> ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK110,X4) ) ),
introduced(definition,[new_symbols(definition,[spl111_79])],[avatar_definition]) ).
tff(f708,plain,
( ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK110,X4) )
| ~ spl111_79 ),
inference(avatar_component_clause,[],[f707]) ).
tff(f709,plain,
( spl111_75
| spl111_76
| spl111_77
| spl111_79 ),
inference(avatar_split_clause,[],[f457,f707,f700,f696,f692]) ).
tff(f6496,definition,
( spl111_314
<=> ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3) ) ),
introduced(definition,[new_symbols(definition,[spl111_314])],[avatar_definition]) ).
tff(f6497,plain,
( ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3) )
| ~ spl111_314 ),
inference(avatar_component_clause,[],[f6496]) ).
tff(f9981,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK106(X0))
| ~ sP3(X0) )
| ~ spl111_79 ),
inference(resolution,[],[f708,f445]) ).
tff(f10000,plain,
( ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3)
| sP10(sK110)
| sP8(sK110) )
| spl111_76 ),
inference(forward_subsumption_resolution,[],[f458,f697]) ).
tff(f10001,plain,
( ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3)
| sP10(sK110) )
| spl111_75
| spl111_76 ),
inference(forward_subsumption_resolution,[],[f10000,f693]) ).
tff(f10033,plain,
( ~ sP3(sK110)
| ~ sP3(sK110)
| ~ spl111_79 ),
inference(resolution,[],[f444,f9981]) ).
tff(f10067,plain,
( ~ sP3(sK110)
| ~ spl111_79 ),
inference(duplicate_literal_removal,[],[f10033]) ).
tff(f10242,plain,
! [X0: '$ki_world'] :
( ~ sP2(X0)
| qmltpeq(sK107(X0),op(e3,e3),e1)
| ~ sP10(X0) ),
inference(resolution,[],[f446,f400]) ).
tff(f10271,plain,
! [X0: '$ki_world'] :
( ~ sP10(X0)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f10242,f447]) ).
tff(f10815,definition,
( spl111_666
<=> '$ki_accessible'(sK110,sK98(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_666])],[avatar_definition]) ).
tff(f10816,plain,
( ~ '$ki_accessible'(sK110,sK98(sK110))
| spl111_666 ),
inference(avatar_component_clause,[],[f10815]) ).
tff(f10817,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| ~ spl111_666 ),
inference(avatar_component_clause,[],[f10815]) ).
tff(f10870,plain,
( ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK110,X3) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(forward_subsumption_resolution,[],[f10001,f701]) ).
tff(f10871,plain,
( spl111_314
| spl111_75
| spl111_76
| spl111_77 ),
inference(avatar_split_clause,[],[f10870,f700,f696,f692,f6496]) ).
tff(f11786,plain,
( ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK110,X2)
| sP10(sK110)
| sP8(sK110) )
| spl111_76 ),
inference(forward_subsumption_resolution,[],[f459,f697]) ).
tff(f11787,plain,
( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK110,X1)
| sP10(sK110)
| sP8(sK110) )
| spl111_76 ),
inference(forward_subsumption_resolution,[],[f460,f697]) ).
tff(f11916,plain,
( ~ sP2(sK110)
| ~ spl111_77 ),
inference(resolution,[],[f10271,f702]) ).
tff(f13408,plain,
( qmltpeq(sK98(sK110),op(e1,e1),e1)
| ~ sP10(sK110)
| ~ spl111_666 ),
inference(resolution,[],[f10817,f402]) ).
tff(f13418,plain,
( qmltpeq(sK98(sK110),op(e1,e1),e1)
| ~ spl111_77
| ~ spl111_666 ),
inference(forward_subsumption_resolution,[],[f13408,f702]) ).
tff(f14156,definition,
( spl111_967
<=> '$ki_accessible'(sK110,sK97(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_967])],[avatar_definition]) ).
tff(f14157,plain,
( ~ '$ki_accessible'(sK110,sK97(sK110))
| spl111_967 ),
inference(avatar_component_clause,[],[f14156]) ).
tff(f14158,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| ~ spl111_967 ),
inference(avatar_component_clause,[],[f14156]) ).
tff(f14297,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| '$ki_accessible'(sK110,sK99(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666 ),
inference(resolution,[],[f422,f13418]) ).
tff(f14299,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| '$ki_accessible'(sK110,sK99(sK110))
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666 ),
inference(forward_subsumption_resolution,[],[f14297,f11916]) ).
tff(f14301,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| '$ki_accessible'(sK110,sK99(sK110))
| ~ spl111_77
| ~ spl111_666 ),
inference(forward_subsumption_resolution,[],[f14299,f686]) ).
tff(f14303,definition,
( spl111_968
<=> '$ki_accessible'(sK110,sK99(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_968])],[avatar_definition]) ).
tff(f14304,plain,
( ~ '$ki_accessible'(sK110,sK99(sK110))
| spl111_968 ),
inference(avatar_component_clause,[],[f14303]) ).
tff(f14305,plain,
( '$ki_accessible'(sK110,sK99(sK110))
| ~ spl111_968 ),
inference(avatar_component_clause,[],[f14303]) ).
tff(f14306,plain,
( spl111_968
| spl111_967
| ~ spl111_77
| ~ spl111_666 ),
inference(avatar_split_clause,[],[f14301,f10815,f700,f14156,f14303]) ).
tff(f14516,plain,
( qmltpeq(sK97(sK110),op(e0,e0),e1)
| ~ sP10(sK110)
| ~ spl111_967 ),
inference(resolution,[],[f14158,f403]) ).
tff(f14528,plain,
( qmltpeq(sK97(sK110),op(e0,e0),e1)
| ~ spl111_77
| ~ spl111_967 ),
inference(forward_subsumption_resolution,[],[f14516,f702]) ).
tff(f14560,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0)
| qmltpeq(sK99(X0),op(e2,e2),e1)
| ~ sP10(X0) ),
inference(resolution,[],[f420,f401]) ).
tff(f14588,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK99(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK98(X0))
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0) ),
inference(forward_subsumption_resolution,[],[f14560,f10271]) ).
tff(f14957,plain,
( ~ qmltpeq(sK97(sK110),op(e0,e0),e1)
| '$ki_accessible'(sK110,sK99(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666 ),
inference(resolution,[],[f426,f13418]) ).
tff(f14959,plain,
( '$ki_accessible'(sK110,sK99(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967 ),
inference(forward_subsumption_resolution,[],[f14957,f14528]) ).
tff(f14961,plain,
( sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f14959,f14304]) ).
tff(f14963,plain,
( ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f14961,f11916]) ).
tff(f14964,plain,
( $false
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f14963,f686]) ).
tff(f14965,plain,
( ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| spl111_968 ),
inference(avatar_contradiction_clause,[],[f14964]) ).
tff(f14973,plain,
( qmltpeq(sK99(sK110),op(e2,e2),e1)
| ~ sP10(sK110)
| ~ spl111_968 ),
inference(resolution,[],[f14305,f401]) ).
tff(f14987,plain,
( qmltpeq(sK99(sK110),op(e2,e2),e1)
| ~ spl111_77
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14973,f702]) ).
tff(f14988,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| '$ki_accessible'(sK110,sK97(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_968 ),
inference(resolution,[],[f14987,f421]) ).
tff(f14989,plain,
( ~ qmltpeq(sK98(sK110),op(e1,e1),e1)
| '$ki_accessible'(sK110,sK97(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_968 ),
inference(resolution,[],[f14987,f423]) ).
tff(f14990,plain,
( ~ qmltpeq(sK98(sK110),op(e1,e1),e1)
| ~ qmltpeq(sK97(sK110),op(e0,e0),e1)
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_968 ),
inference(resolution,[],[f14987,f427]) ).
tff(f14991,plain,
( ~ qmltpeq(sK97(sK110),op(e0,e0),e1)
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14990,f13418]) ).
tff(f14992,plain,
( sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14991,f14528]) ).
tff(f14993,plain,
( ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14992,f11916]) ).
tff(f14994,plain,
( $false
| ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14993,f686]) ).
tff(f14995,plain,
( ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| ~ spl111_968 ),
inference(avatar_contradiction_clause,[],[f14994]) ).
tff(f15001,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14989,f13418]) ).
tff(f15002,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_666
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15001,f11916]) ).
tff(f15003,plain,
( '$ki_accessible'(sK110,sK97(sK110))
| ~ spl111_77
| ~ spl111_666
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15002,f686]) ).
tff(f15005,plain,
( $false
| ~ spl111_77
| ~ spl111_666
| spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15003,f14157]) ).
tff(f15006,plain,
( ~ spl111_77
| ~ spl111_666
| spl111_967
| ~ spl111_968 ),
inference(avatar_contradiction_clause,[],[f15005]) ).
tff(f15009,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f14988,f14157]) ).
tff(f15012,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| ~ sP6(sK110)
| ~ spl111_77
| spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15009,f11916]) ).
tff(f15014,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| ~ spl111_77
| spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15012,f686]) ).
tff(f15016,plain,
( $false
| ~ spl111_77
| spl111_666
| spl111_967
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15014,f10816]) ).
tff(f15017,plain,
( ~ spl111_77
| spl111_666
| spl111_967
| ~ spl111_968 ),
inference(avatar_contradiction_clause,[],[f15016]) ).
tff(f15024,definition,
( spl111_969
<=> qmltpeq(sK97(sK110),op(e0,e0),e1) ),
introduced(definition,[new_symbols(definition,[spl111_969])],[avatar_definition]) ).
tff(f15025,plain,
( qmltpeq(sK97(sK110),op(e0,e0),e1)
| ~ spl111_969 ),
inference(avatar_component_clause,[],[f15024]) ).
tff(f15040,plain,
( qmltpeq(sK97(sK110),op(e0,e0),e1)
| ~ sP10(sK110)
| ~ spl111_967 ),
inference(resolution,[],[f14158,f403]) ).
tff(f15052,plain,
( qmltpeq(sK97(sK110),op(e0,e0),e1)
| ~ spl111_77
| ~ spl111_967 ),
inference(forward_subsumption_resolution,[],[f15040,f702]) ).
tff(f15055,plain,
( spl111_969
| ~ spl111_77
| ~ spl111_967 ),
inference(avatar_split_clause,[],[f15052,f14156,f700,f15024]) ).
tff(f15058,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK98(X0))
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(resolution,[],[f14588,f421]) ).
tff(f15079,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK98(X0))
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| sP2(X0) ),
inference(duplicate_literal_removal,[],[f15058]) ).
tff(f15082,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK98(X0))
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0) ),
inference(forward_subsumption_resolution,[],[f15079,f10271]) ).
tff(f15090,plain,
! [X0: '$ki_world'] :
( ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| qmltpeq(sK98(X0),op(e1,e1),e1)
| ~ sP10(X0) ),
inference(resolution,[],[f15082,f402]) ).
tff(f15118,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK98(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| ~ sP6(X0) ),
inference(duplicate_literal_removal,[],[f15090]) ).
tff(f15122,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(resolution,[],[f15118,f422]) ).
tff(f15140,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0) ),
inference(duplicate_literal_removal,[],[f15122]) ).
tff(f15142,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK99(X0))
| ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0)) ),
inference(forward_subsumption_resolution,[],[f15140,f10271]) ).
tff(f15150,plain,
! [X0: '$ki_world'] :
( ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK97(X0))
| qmltpeq(sK99(X0),op(e2,e2),e1)
| ~ sP10(X0) ),
inference(resolution,[],[f15142,f401]) ).
tff(f15180,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK99(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK97(X0))
| ~ sP6(X0)
| ~ sP10(X0) ),
inference(duplicate_literal_removal,[],[f15150]) ).
tff(f15183,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP6(X0)
| ~ sP10(X0)
| ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK97(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(resolution,[],[f15180,f423]) ).
tff(f15202,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP6(X0)
| ~ sP10(X0)
| ~ qmltpeq(sK98(X0),op(e1,e1),e1)
| sP2(X0) ),
inference(duplicate_literal_removal,[],[f15183]) ).
tff(f15205,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP6(X0)
| ~ sP10(X0)
| sP2(X0) ),
inference(forward_subsumption_resolution,[],[f15202,f15118]) ).
tff(f15207,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK97(X0))
| ~ sP6(X0)
| ~ sP10(X0) ),
inference(forward_subsumption_resolution,[],[f15205,f10271]) ).
tff(f15215,plain,
! [X0: '$ki_world'] :
( ~ sP6(X0)
| ~ sP10(X0)
| qmltpeq(sK97(X0),op(e0,e0),e1)
| ~ sP10(X0) ),
inference(resolution,[],[f15207,f403]) ).
tff(f15241,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK97(X0),op(e0,e0),e1)
| ~ sP10(X0)
| ~ sP6(X0) ),
inference(duplicate_literal_removal,[],[f15215]) ).
tff(f15245,plain,
! [X0: '$ki_world'] :
( ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(resolution,[],[f15241,f424]) ).
tff(f15246,plain,
! [X0: '$ki_world'] :
( ~ sP10(X0)
| ~ sP6(X0)
| '$ki_accessible'(X0,sK98(X0))
| '$ki_accessible'(X0,sK99(X0))
| sP2(X0) ),
inference(duplicate_literal_removal,[],[f15245]) ).
tff(f15247,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK99(X0))
| ~ sP6(X0)
| '$ki_accessible'(X0,sK98(X0))
| ~ sP10(X0) ),
inference(forward_subsumption_resolution,[],[f15246,f10271]) ).
tff(f15326,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| ~ qmltpeq(sK97(sK110),op(e0,e0),e1)
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| ~ spl111_968 ),
inference(resolution,[],[f425,f14987]) ).
tff(f15332,plain,
( ~ qmltpeq(sK97(sK110),op(e0,e0),e1)
| sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| spl111_666
| ~ spl111_968 ),
inference(forward_subsumption_resolution,[],[f15326,f10816]) ).
tff(f15335,plain,
( sP2(sK110)
| ~ sP6(sK110)
| ~ spl111_77
| spl111_666
| ~ spl111_968
| ~ spl111_969 ),
inference(forward_subsumption_resolution,[],[f15332,f15025]) ).
tff(f15338,plain,
( ~ sP6(sK110)
| ~ spl111_77
| spl111_666
| ~ spl111_968
| ~ spl111_969 ),
inference(forward_subsumption_resolution,[],[f15335,f11916]) ).
tff(f15340,plain,
( $false
| ~ spl111_77
| spl111_666
| ~ spl111_968
| ~ spl111_969 ),
inference(forward_subsumption_resolution,[],[f15338,f686]) ).
tff(f15341,plain,
( ~ spl111_77
| spl111_666
| ~ spl111_968
| ~ spl111_969 ),
inference(avatar_contradiction_clause,[],[f15340]) ).
tff(f15345,plain,
( ~ sP6(sK110)
| '$ki_accessible'(sK110,sK98(sK110))
| ~ sP10(sK110)
| spl111_968 ),
inference(resolution,[],[f14304,f15247]) ).
tff(f15348,plain,
( '$ki_accessible'(sK110,sK98(sK110))
| ~ sP10(sK110)
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f15345,f686]) ).
tff(f15349,plain,
( ~ sP10(sK110)
| spl111_666
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f15348,f10816]) ).
tff(f15350,plain,
( $false
| ~ spl111_77
| spl111_666
| spl111_968 ),
inference(forward_subsumption_resolution,[],[f15349,f702]) ).
tff(f15351,plain,
( ~ spl111_77
| spl111_666
| spl111_968 ),
inference(avatar_contradiction_clause,[],[f15350]) ).
tff(f15589,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK96(X0))
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0)
| '$ki_accessible'(X0,sK95(X0)) )
| ~ spl111_314 ),
inference(resolution,[],[f413,f6497]) ).
tff(f15591,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| '$ki_accessible'(sK110,sK95(sK110))
| '$ki_accessible'(sK110,sK95(sK110))
| '$ki_accessible'(sK110,sK94(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| ~ spl111_314 ),
inference(resolution,[],[f15589,f412]) ).
tff(f15592,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| '$ki_accessible'(sK110,sK95(sK110))
| ~ spl111_314 ),
inference(duplicate_literal_removal,[],[f15591]) ).
tff(f15606,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| ~ sP7(sK110)
| '$ki_accessible'(sK110,sK95(sK110))
| ~ spl111_79
| ~ spl111_314 ),
inference(forward_subsumption_resolution,[],[f15592,f10067]) ).
tff(f15610,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| '$ki_accessible'(sK110,sK95(sK110))
| ~ spl111_79
| ~ spl111_314 ),
inference(forward_subsumption_resolution,[],[f15606,f690]) ).
tff(f15737,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK96(X0)) )
| ~ spl111_314 ),
inference(resolution,[],[f415,f6497]) ).
tff(f15787,plain,
! [X0: '$ki_world'] :
( ~ sP0(X0)
| qmltpeq(sK109(X0),op(e3,e3),e3)
| ~ sP8(X0) ),
inference(resolution,[],[f450,f408]) ).
tff(f15808,plain,
! [X0: '$ki_world'] :
( ~ sP8(X0)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f15787,f451]) ).
tff(f15812,plain,
( ~ sP0(sK110)
| ~ spl111_75 ),
inference(resolution,[],[f15808,f694]) ).
tff(f16809,definition,
( spl111_1145
<=> '$ki_accessible'(sK110,sK103(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1145])],[avatar_definition]) ).
tff(f16810,plain,
( ~ '$ki_accessible'(sK110,sK103(sK110))
| spl111_1145 ),
inference(avatar_component_clause,[],[f16809]) ).
tff(f16811,plain,
( '$ki_accessible'(sK110,sK103(sK110))
| ~ spl111_1145 ),
inference(avatar_component_clause,[],[f16809]) ).
tff(f17918,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0)
| qmltpeq(sK105(X0),op(e2,e2),e3)
| ~ sP8(X0) ),
inference(resolution,[],[f436,f409]) ).
tff(f17938,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0)
| ~ sP8(X0) ),
inference(forward_subsumption_resolution,[],[f17918,f437]) ).
tff(f17940,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK104(X0))
| '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0) ),
inference(forward_subsumption_resolution,[],[f17938,f15808]) ).
tff(f17948,definition,
( spl111_1228
<=> '$ki_accessible'(sK110,sK104(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1228])],[avatar_definition]) ).
tff(f17949,plain,
( ~ '$ki_accessible'(sK110,sK104(sK110))
| spl111_1228 ),
inference(avatar_component_clause,[],[f17948]) ).
tff(f17950,plain,
( '$ki_accessible'(sK110,sK104(sK110))
| ~ spl111_1228 ),
inference(avatar_component_clause,[],[f17948]) ).
tff(f18396,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0)
| qmltpeq(sK104(X0),op(e1,e1),e3)
| ~ sP8(X0) ),
inference(resolution,[],[f17940,f410]) ).
tff(f18416,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK104(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK103(X0))
| ~ sP8(X0)
| ~ sP4(X0) ),
inference(duplicate_literal_removal,[],[f18396]) ).
tff(f18477,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP8(X0)
| ~ sP4(X0)
| '$ki_accessible'(X0,sK103(X0))
| '$ki_accessible'(X0,sK105(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(resolution,[],[f18416,f438]) ).
tff(f18494,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP8(X0)
| ~ sP4(X0)
| '$ki_accessible'(X0,sK105(X0))
| sP0(X0) ),
inference(duplicate_literal_removal,[],[f18477]) ).
tff(f18496,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK105(X0))
| ~ sP8(X0)
| ~ sP4(X0)
| '$ki_accessible'(X0,sK103(X0)) ),
inference(forward_subsumption_resolution,[],[f18494,f15808]) ).
tff(f18513,plain,
! [X0: '$ki_world'] :
( ~ sP8(X0)
| ~ sP4(X0)
| '$ki_accessible'(X0,sK103(X0))
| qmltpeq(sK105(X0),op(e2,e2),e3)
| ~ sP8(X0) ),
inference(resolution,[],[f18496,f409]) ).
tff(f18535,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK105(X0),op(e2,e2),e3)
| '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0) ),
inference(duplicate_literal_removal,[],[f18513]) ).
tff(f18538,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0)
| ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK103(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(resolution,[],[f18535,f439]) ).
tff(f18557,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0)
| ~ qmltpeq(sK104(X0),op(e1,e1),e3)
| sP0(X0) ),
inference(duplicate_literal_removal,[],[f18538]) ).
tff(f18561,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0)
| sP0(X0) ),
inference(forward_subsumption_resolution,[],[f18557,f18416]) ).
tff(f18563,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK103(X0))
| ~ sP4(X0)
| ~ sP8(X0) ),
inference(forward_subsumption_resolution,[],[f18561,f15808]) ).
tff(f18564,plain,
( ~ sP4(sK110)
| ~ sP8(sK110)
| spl111_1145 ),
inference(resolution,[],[f18563,f16810]) ).
tff(f18606,plain,
( ~ sP8(sK110)
| spl111_1145 ),
inference(forward_subsumption_resolution,[],[f18564,f677]) ).
tff(f18610,plain,
( $false
| ~ spl111_75
| spl111_1145 ),
inference(forward_subsumption_resolution,[],[f18606,f694]) ).
tff(f18611,plain,
( ~ spl111_75
| spl111_1145 ),
inference(avatar_contradiction_clause,[],[f18610]) ).
tff(f19192,plain,
( qmltpeq(sK103(sK110),op(e0,e0),e3)
| ~ sP8(sK110)
| ~ spl111_1145 ),
inference(resolution,[],[f16811,f411]) ).
tff(f19193,plain,
( qmltpeq(sK103(sK110),op(e0,e0),e3)
| ~ spl111_75
| ~ spl111_1145 ),
inference(forward_subsumption_resolution,[],[f19192,f694]) ).
tff(f19198,plain,
( '$ki_accessible'(sK110,sK104(sK110))
| '$ki_accessible'(sK110,sK105(sK110))
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145 ),
inference(resolution,[],[f19193,f440]) ).
tff(f19251,plain,
( qmltpeq(sK104(sK110),op(e1,e1),e3)
| ~ sP8(sK110)
| ~ spl111_1228 ),
inference(resolution,[],[f17950,f410]) ).
tff(f19253,plain,
( qmltpeq(sK104(sK110),op(e1,e1),e3)
| ~ spl111_75
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19251,f694]) ).
tff(f19254,plain,
( ~ qmltpeq(sK103(sK110),op(e0,e0),e3)
| '$ki_accessible'(sK110,sK105(sK110))
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1228 ),
inference(resolution,[],[f19253,f442]) ).
tff(f19288,plain,
( '$ki_accessible'(sK110,sK105(sK110))
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19254,f19193]) ).
tff(f19289,plain,
( '$ki_accessible'(sK110,sK105(sK110))
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19288,f15812]) ).
tff(f19290,plain,
( '$ki_accessible'(sK110,sK105(sK110))
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19289,f677]) ).
tff(f19304,plain,
( qmltpeq(sK105(sK110),op(e2,e2),e3)
| ~ sP8(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(resolution,[],[f19290,f409]) ).
tff(f19307,plain,
( qmltpeq(sK105(sK110),op(e2,e2),e3)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19304,f694]) ).
tff(f19311,plain,
( ~ qmltpeq(sK104(sK110),op(e1,e1),e3)
| ~ qmltpeq(sK103(sK110),op(e0,e0),e3)
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(resolution,[],[f19307,f443]) ).
tff(f19312,plain,
( ~ qmltpeq(sK103(sK110),op(e0,e0),e3)
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19311,f19253]) ).
tff(f19313,plain,
( sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19312,f19193]) ).
tff(f19314,plain,
( ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19313,f15812]) ).
tff(f19315,plain,
( $false
| ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19314,f677]) ).
tff(f19316,plain,
( ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(avatar_contradiction_clause,[],[f19315]) ).
tff(f19317,plain,
( '$ki_accessible'(sK110,sK104(sK110))
| '$ki_accessible'(sK110,sK105(sK110))
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145 ),
inference(forward_subsumption_resolution,[],[f19198,f15812]) ).
tff(f19318,plain,
( '$ki_accessible'(sK110,sK104(sK110))
| '$ki_accessible'(sK110,sK105(sK110))
| ~ spl111_75
| ~ spl111_1145 ),
inference(forward_subsumption_resolution,[],[f19317,f677]) ).
tff(f19320,plain,
( '$ki_accessible'(sK110,sK105(sK110))
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19318,f17949]) ).
tff(f19334,plain,
( qmltpeq(sK105(sK110),op(e2,e2),e3)
| ~ sP8(sK110)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(resolution,[],[f19320,f409]) ).
tff(f19337,plain,
( qmltpeq(sK105(sK110),op(e2,e2),e3)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19334,f694]) ).
tff(f19338,plain,
( '$ki_accessible'(sK110,sK104(sK110))
| ~ qmltpeq(sK103(sK110),op(e0,e0),e3)
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(resolution,[],[f19337,f441]) ).
tff(f19343,plain,
( ~ qmltpeq(sK103(sK110),op(e0,e0),e3)
| sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19338,f17949]) ).
tff(f19345,plain,
( sP0(sK110)
| ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19343,f19193]) ).
tff(f19347,plain,
( ~ sP4(sK110)
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19345,f15812]) ).
tff(f19348,plain,
( $false
| ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(forward_subsumption_resolution,[],[f19347,f677]) ).
tff(f19349,plain,
( ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(avatar_contradiction_clause,[],[f19348]) ).
tff(f19546,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK95(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK96(X0)) )
| ~ spl111_314 ),
inference(resolution,[],[f417,f6497]) ).
tff(f19651,plain,
( ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK110,X2)
| sP8(sK110) )
| spl111_76
| spl111_77 ),
inference(forward_subsumption_resolution,[],[f11786,f701]) ).
tff(f19652,plain,
( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK110,X1)
| sP8(sK110) )
| spl111_76
| spl111_77 ),
inference(forward_subsumption_resolution,[],[f11787,f701]) ).
tff(f19889,plain,
( ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK110,X2) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(forward_subsumption_resolution,[],[f19651,f693]) ).
tff(f19890,plain,
( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK110,X1) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(forward_subsumption_resolution,[],[f19652,f693]) ).
tff(f19892,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK96(X0))
| '$ki_accessible'(X0,sK94(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK95(X0)) )
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(resolution,[],[f19889,f15737]) ).
tff(f19893,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK95(X0))
| '$ki_accessible'(X0,sK94(X0))
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(resolution,[],[f19889,f414]) ).
tff(f19894,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK96(X0))
| '$ki_accessible'(X0,sK95(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK94(X0)) )
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(resolution,[],[f19890,f19546]) ).
tff(f19895,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK94(X0))
| '$ki_accessible'(X0,sK95(X0))
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(resolution,[],[f19890,f416]) ).
tff(f20248,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK95(X0),op(e1,e1),e0)
| ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK96(X0)) )
| ~ spl111_314 ),
inference(resolution,[],[f419,f6497]) ).
tff(f20249,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK96(X0))
| ~ '$ki_accessible'(sK110,sK95(X0)) )
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(resolution,[],[f20248,f19889]) ).
tff(f20250,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK96(X0))
| ~ sP7(X0)
| sP3(X0)
| ~ '$ki_accessible'(sK110,sK95(X0))
| ~ '$ki_accessible'(sK110,sK94(X0)) )
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(resolution,[],[f20249,f19890]) ).
tff(f20352,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK94(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK96(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK110,sK95(X0)) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(resolution,[],[f418,f19889]) ).
tff(f20353,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK110,sK95(X0))
| sP3(X0)
| ~ sP7(X0)
| '$ki_accessible'(X0,sK96(X0))
| ~ '$ki_accessible'(sK110,sK94(X0)) )
| spl111_75
| spl111_76
| spl111_77 ),
inference(resolution,[],[f20352,f19890]) ).
tff(f20361,definition,
( spl111_1230
<=> '$ki_accessible'(sK110,sK95(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1230])],[avatar_definition]) ).
tff(f20362,plain,
( ~ '$ki_accessible'(sK110,sK95(sK110))
| spl111_1230 ),
inference(avatar_component_clause,[],[f20361]) ).
tff(f20363,plain,
( '$ki_accessible'(sK110,sK95(sK110))
| ~ spl111_1230 ),
inference(avatar_component_clause,[],[f20361]) ).
tff(f20365,definition,
( spl111_1231
<=> '$ki_accessible'(sK110,sK94(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1231])],[avatar_definition]) ).
tff(f20366,plain,
( ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_1231 ),
inference(avatar_component_clause,[],[f20365]) ).
tff(f20367,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| ~ spl111_1231 ),
inference(avatar_component_clause,[],[f20365]) ).
tff(f20368,plain,
( spl111_1230
| spl111_1231
| ~ spl111_79
| ~ spl111_314 ),
inference(avatar_split_clause,[],[f15610,f6496,f707,f20365,f20361]) ).
tff(f20369,plain,
( sP3(sK110)
| ~ sP7(sK110)
| '$ki_accessible'(sK110,sK96(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_1230 ),
inference(resolution,[],[f20363,f20353]) ).
tff(f20386,plain,
( ~ sP7(sK110)
| '$ki_accessible'(sK110,sK96(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20369,f10067]) ).
tff(f20387,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20386,f690]) ).
tff(f20391,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_1230 ),
inference(resolution,[],[f19893,f20363]) ).
tff(f20392,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20391,f20366]) ).
tff(f20397,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20392,f10067]) ).
tff(f20398,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20397,f690]) ).
tff(f20399,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK95(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(resolution,[],[f20398,f19892]) ).
tff(f20419,plain,
( sP3(sK110)
| ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK95(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20399,f20366]) ).
tff(f20420,plain,
( ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK95(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20419,f10067]) ).
tff(f20421,plain,
( ~ '$ki_accessible'(sK110,sK95(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20420,f690]) ).
tff(f20422,plain,
( $false
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20421,f20363]) ).
tff(f20423,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(avatar_contradiction_clause,[],[f20422]) ).
tff(f20424,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20391,f10067]) ).
tff(f20425,plain,
( '$ki_accessible'(sK110,sK94(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20424,f690]) ).
tff(f20426,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1230 ),
inference(global_subsumption,[],[f20425,f20387]) ).
tff(f20427,plain,
( '$ki_accessible'(sK110,sK95(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_1231 ),
inference(resolution,[],[f20367,f19895]) ).
tff(f20446,plain,
( ~ sP7(sK110)
| sP3(sK110)
| ~ '$ki_accessible'(sK110,sK95(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230 ),
inference(resolution,[],[f20426,f20250]) ).
tff(f20465,plain,
( sP3(sK110)
| ~ '$ki_accessible'(sK110,sK95(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20446,f690]) ).
tff(f20466,plain,
( ~ '$ki_accessible'(sK110,sK95(sK110))
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20465,f10067]) ).
tff(f20467,plain,
( ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230 ),
inference(forward_subsumption_resolution,[],[f20466,f20363]) ).
tff(f20468,plain,
( $false
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20467,f20367]) ).
tff(f20469,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| ~ spl111_1231 ),
inference(avatar_contradiction_clause,[],[f20468]) ).
tff(f20470,plain,
( '$ki_accessible'(sK110,sK95(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| ~ sP7(sK110)
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20427,f10067]) ).
tff(f20471,plain,
( '$ki_accessible'(sK110,sK95(sK110))
| '$ki_accessible'(sK110,sK96(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20470,f690]) ).
tff(f20472,plain,
( '$ki_accessible'(sK110,sK96(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20471,f20362]) ).
tff(f20475,plain,
( '$ki_accessible'(sK110,sK95(sK110))
| sP3(sK110)
| ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(resolution,[],[f20472,f19894]) ).
tff(f20493,plain,
( sP3(sK110)
| ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20475,f20362]) ).
tff(f20494,plain,
( ~ sP7(sK110)
| ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20493,f10067]) ).
tff(f20495,plain,
( ~ '$ki_accessible'(sK110,sK94(sK110))
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20494,f690]) ).
tff(f20496,plain,
( $false
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(forward_subsumption_resolution,[],[f20495,f20367]) ).
tff(f20497,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(avatar_contradiction_clause,[],[f20496]) ).
tff(f20567,plain,
! [X0: '$ki_world'] :
( ~ sP1(X0)
| qmltpeq(sK108(X0),op(e3,e3),e2)
| ~ sP9(X0) ),
inference(resolution,[],[f448,f404]) ).
tff(f20661,plain,
! [X0: '$ki_world'] :
( ~ sP9(X0)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f20567,f449]) ).
tff(f20915,plain,
( ~ sP1(sK110)
| ~ spl111_76 ),
inference(resolution,[],[f20661,f698]) ).
tff(f22073,definition,
( spl111_1395
<=> '$ki_accessible'(sK110,sK100(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1395])],[avatar_definition]) ).
tff(f22074,plain,
( ~ '$ki_accessible'(sK110,sK100(sK110))
| spl111_1395 ),
inference(avatar_component_clause,[],[f22073]) ).
tff(f22075,plain,
( '$ki_accessible'(sK110,sK100(sK110))
| ~ spl111_1395 ),
inference(avatar_component_clause,[],[f22073]) ).
tff(f22996,plain,
( qmltpeq(sK100(sK110),op(e0,e0),e2)
| ~ sP9(sK110)
| ~ spl111_1395 ),
inference(resolution,[],[f22075,f407]) ).
tff(f23063,plain,
( qmltpeq(sK100(sK110),op(e0,e0),e2)
| ~ spl111_76
| ~ spl111_1395 ),
inference(forward_subsumption_resolution,[],[f22996,f698]) ).
tff(f23324,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| '$ki_accessible'(sK110,sK102(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395 ),
inference(resolution,[],[f432,f23063]) ).
tff(f23327,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| '$ki_accessible'(sK110,sK102(sK110))
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395 ),
inference(forward_subsumption_resolution,[],[f23324,f20915]) ).
tff(f23329,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| '$ki_accessible'(sK110,sK102(sK110))
| ~ spl111_76
| ~ spl111_1395 ),
inference(forward_subsumption_resolution,[],[f23327,f682]) ).
tff(f23332,definition,
( spl111_1478
<=> '$ki_accessible'(sK110,sK102(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1478])],[avatar_definition]) ).
tff(f23333,plain,
( ~ '$ki_accessible'(sK110,sK102(sK110))
| spl111_1478 ),
inference(avatar_component_clause,[],[f23332]) ).
tff(f23334,plain,
( '$ki_accessible'(sK110,sK102(sK110))
| ~ spl111_1478 ),
inference(avatar_component_clause,[],[f23332]) ).
tff(f23336,definition,
( spl111_1479
<=> '$ki_accessible'(sK110,sK101(sK110)) ),
introduced(definition,[new_symbols(definition,[spl111_1479])],[avatar_definition]) ).
tff(f23337,plain,
( ~ '$ki_accessible'(sK110,sK101(sK110))
| spl111_1479 ),
inference(avatar_component_clause,[],[f23336]) ).
tff(f23338,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| ~ spl111_1479 ),
inference(avatar_component_clause,[],[f23336]) ).
tff(f23339,plain,
( spl111_1478
| spl111_1479
| ~ spl111_76
| ~ spl111_1395 ),
inference(avatar_split_clause,[],[f23329,f22073,f696,f23336,f23332]) ).
tff(f23524,plain,
( qmltpeq(sK102(sK110),op(e2,e2),e2)
| ~ sP9(sK110)
| ~ spl111_1478 ),
inference(resolution,[],[f23334,f405]) ).
tff(f23534,plain,
( qmltpeq(sK102(sK110),op(e2,e2),e2)
| ~ spl111_76
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23524,f698]) ).
tff(f23536,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478 ),
inference(resolution,[],[f23534,f435]) ).
tff(f23537,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| '$ki_accessible'(sK110,sK100(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478 ),
inference(resolution,[],[f23534,f431]) ).
tff(f23710,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478 ),
inference(resolution,[],[f433,f23534]) ).
tff(f23714,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23710,f23337]) ).
tff(f23718,plain,
( sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23714,f23063]) ).
tff(f23722,plain,
( ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23718,f20915]) ).
tff(f23723,plain,
( $false
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23722,f682]) ).
tff(f23724,plain,
( ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(avatar_contradiction_clause,[],[f23723]) ).
tff(f23726,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23536,f23063]) ).
tff(f23728,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23726,f20915]) ).
tff(f23730,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23728,f682]) ).
tff(f23743,plain,
( qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ sP9(sK110)
| ~ spl111_1479 ),
inference(resolution,[],[f23338,f406]) ).
tff(f23749,plain,
( ~ sP9(sK110)
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| ~ spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23743,f23730]) ).
tff(f23750,plain,
( $false
| ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| ~ spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23749,f698]) ).
tff(f23751,plain,
( ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| ~ spl111_1479 ),
inference(avatar_contradiction_clause,[],[f23750]) ).
tff(f23755,plain,
( qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ spl111_76
| ~ spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23743,f698]) ).
tff(f23759,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| '$ki_accessible'(sK110,sK100(sK110))
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23537,f20915]) ).
tff(f23760,plain,
( ~ qmltpeq(sK101(sK110),op(e1,e1),e2)
| '$ki_accessible'(sK110,sK100(sK110))
| ~ spl111_76
| ~ spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23759,f682]) ).
tff(f23762,definition,
( spl111_1481
<=> qmltpeq(sK100(sK110),op(e0,e0),e2) ),
introduced(definition,[new_symbols(definition,[spl111_1481])],[avatar_definition]) ).
tff(f23764,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| spl111_1481 ),
inference(avatar_component_clause,[],[f23762]) ).
tff(f23766,definition,
( spl111_1482
<=> qmltpeq(sK101(sK110),op(e1,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl111_1482])],[avatar_definition]) ).
tff(f23767,plain,
( qmltpeq(sK101(sK110),op(e1,e1),e2)
| ~ spl111_1482 ),
inference(avatar_component_clause,[],[f23766]) ).
tff(f23776,plain,
( spl111_1482
| ~ spl111_76
| ~ spl111_1479 ),
inference(avatar_split_clause,[],[f23755,f23336,f696,f23766]) ).
tff(f23781,plain,
( '$ki_accessible'(sK110,sK100(sK110))
| ~ spl111_76
| ~ spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23760,f23767]) ).
tff(f23782,plain,
( $false
| ~ spl111_76
| spl111_1395
| ~ spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23781,f22074]) ).
tff(f23783,plain,
( ~ spl111_76
| spl111_1395
| ~ spl111_1478
| ~ spl111_1482 ),
inference(avatar_contradiction_clause,[],[f23782]) ).
tff(f23843,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| '$ki_accessible'(sK110,sK100(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478 ),
inference(resolution,[],[f429,f23534]) ).
tff(f23845,plain,
( '$ki_accessible'(sK110,sK100(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23843,f23337]) ).
tff(f23847,plain,
( sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_76
| spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23845,f22074]) ).
tff(f23848,plain,
( ~ sP5(sK110)
| ~ spl111_76
| spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23847,f20915]) ).
tff(f23849,plain,
( $false
| ~ spl111_76
| spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(forward_subsumption_resolution,[],[f23848,f682]) ).
tff(f23850,plain,
( ~ spl111_76
| spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(avatar_contradiction_clause,[],[f23849]) ).
tff(f23863,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| '$ki_accessible'(sK110,sK100(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| spl111_1478 ),
inference(resolution,[],[f23333,f428]) ).
tff(f23864,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| spl111_1395
| spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23863,f22074]) ).
tff(f23865,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| ~ sP5(sK110)
| ~ spl111_76
| spl111_1395
| spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23864,f20915]) ).
tff(f23866,plain,
( '$ki_accessible'(sK110,sK101(sK110))
| ~ spl111_76
| spl111_1395
| spl111_1478 ),
inference(forward_subsumption_resolution,[],[f23865,f682]) ).
tff(f23867,plain,
( spl111_1479
| ~ spl111_76
| spl111_1395
| spl111_1478 ),
inference(avatar_split_clause,[],[f23866,f23332,f22073,f696,f23336]) ).
tff(f23886,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| '$ki_accessible'(sK110,sK102(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_1482 ),
inference(resolution,[],[f23767,f434]) ).
tff(f23887,plain,
( '$ki_accessible'(sK110,sK100(sK110))
| '$ki_accessible'(sK110,sK102(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| ~ spl111_1482 ),
inference(resolution,[],[f23767,f430]) ).
tff(f23888,plain,
( '$ki_accessible'(sK110,sK102(sK110))
| sP1(sK110)
| ~ sP5(sK110)
| spl111_1395
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23887,f22074]) ).
tff(f23889,plain,
( sP1(sK110)
| ~ sP5(sK110)
| spl111_1395
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23888,f23333]) ).
tff(f23890,plain,
( ~ sP5(sK110)
| ~ spl111_76
| spl111_1395
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23889,f20915]) ).
tff(f23891,plain,
( $false
| ~ spl111_76
| spl111_1395
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23890,f682]) ).
tff(f23892,plain,
( ~ spl111_76
| spl111_1395
| spl111_1478
| ~ spl111_1482 ),
inference(avatar_contradiction_clause,[],[f23891]) ).
tff(f23907,plain,
( qmltpeq(sK100(sK110),op(e0,e0),e2)
| ~ sP9(sK110)
| ~ spl111_1395 ),
inference(resolution,[],[f22075,f407]) ).
tff(f23912,plain,
( ~ sP9(sK110)
| ~ spl111_1395
| spl111_1481 ),
inference(forward_subsumption_resolution,[],[f23907,f23764]) ).
tff(f23913,plain,
( $false
| ~ spl111_76
| ~ spl111_1395
| spl111_1481 ),
inference(forward_subsumption_resolution,[],[f23912,f698]) ).
tff(f23914,plain,
( ~ spl111_76
| ~ spl111_1395
| spl111_1481 ),
inference(avatar_contradiction_clause,[],[f23913]) ).
tff(f23915,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| sP1(sK110)
| ~ sP5(sK110)
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23886,f23333]) ).
tff(f23917,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| ~ sP5(sK110)
| ~ spl111_76
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23915,f20915]) ).
tff(f23918,plain,
( ~ qmltpeq(sK100(sK110),op(e0,e0),e2)
| ~ spl111_76
| spl111_1478
| ~ spl111_1482 ),
inference(forward_subsumption_resolution,[],[f23917,f682]) ).
tff(f23919,plain,
( ~ spl111_1481
| ~ spl111_76
| spl111_1478
| ~ spl111_1482 ),
inference(avatar_split_clause,[],[f23918,f23766,f23332,f696,f23762]) ).
cnf(s586,plain,
( spl111_75
| spl111_76
| spl111_77
| spl111_79 ),
inference(sat_conversion,[],[f709]) ).
cnf(s9305,plain,
( spl111_75
| spl111_76
| spl111_77
| spl111_314 ),
inference(sat_conversion,[],[f10871]) ).
cnf(s12128,plain,
( ~ spl111_77
| ~ spl111_666
| spl111_967
| spl111_968 ),
inference(sat_conversion,[],[f14306]) ).
cnf(s12267,plain,
( ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| spl111_968 ),
inference(sat_conversion,[],[f14965]) ).
cnf(s12274,plain,
( ~ spl111_77
| ~ spl111_666
| ~ spl111_967
| ~ spl111_968 ),
inference(sat_conversion,[],[f14995]) ).
cnf(s12286,plain,
( ~ spl111_77
| ~ spl111_666
| spl111_967
| ~ spl111_968 ),
inference(sat_conversion,[],[f15006]) ).
cnf(s12296,plain,
( ~ spl111_77
| spl111_666
| spl111_967
| ~ spl111_968 ),
inference(sat_conversion,[],[f15017]) ).
cnf(s12318,plain,
( ~ spl111_77
| ~ spl111_967
| spl111_969 ),
inference(sat_conversion,[],[f15055]) ).
cnf(s12352,plain,
( ~ spl111_77
| spl111_666
| ~ spl111_968
| ~ spl111_969 ),
inference(sat_conversion,[],[f15341]) ).
cnf(s12361,plain,
( ~ spl111_77
| spl111_666
| spl111_968 ),
inference(sat_conversion,[],[f15351]) ).
cnf(s14419,plain,
( ~ spl111_75
| spl111_1145 ),
inference(sat_conversion,[],[f18611]) ).
cnf(s14588,plain,
( ~ spl111_75
| ~ spl111_1145
| ~ spl111_1228 ),
inference(sat_conversion,[],[f19316]) ).
cnf(s14597,plain,
( ~ spl111_75
| ~ spl111_1145
| spl111_1228 ),
inference(sat_conversion,[],[f19349]) ).
cnf(s15117,plain,
( ~ spl111_79
| ~ spl111_314
| spl111_1230
| spl111_1231 ),
inference(sat_conversion,[],[f20368]) ).
cnf(s15140,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| spl111_1231 ),
inference(sat_conversion,[],[f20423]) ).
cnf(s15158,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| ~ spl111_1230
| ~ spl111_1231 ),
inference(sat_conversion,[],[f20469]) ).
cnf(s15167,plain,
( spl111_75
| spl111_76
| spl111_77
| ~ spl111_79
| ~ spl111_314
| spl111_1230
| ~ spl111_1231 ),
inference(sat_conversion,[],[f20497]) ).
cnf(s17422,plain,
( ~ spl111_76
| ~ spl111_1395
| spl111_1478
| spl111_1479 ),
inference(sat_conversion,[],[f23339]) ).
cnf(s17507,plain,
( ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(sat_conversion,[],[f23724]) ).
cnf(s17522,plain,
( ~ spl111_76
| ~ spl111_1395
| ~ spl111_1478
| ~ spl111_1479 ),
inference(sat_conversion,[],[f23751]) ).
cnf(s17554,plain,
( ~ spl111_76
| ~ spl111_1479
| spl111_1482 ),
inference(sat_conversion,[],[f23776]) ).
cnf(s17559,plain,
( ~ spl111_76
| spl111_1395
| ~ spl111_1478
| ~ spl111_1482 ),
inference(sat_conversion,[],[f23783]) ).
cnf(s17581,plain,
( ~ spl111_76
| spl111_1395
| ~ spl111_1478
| spl111_1479 ),
inference(sat_conversion,[],[f23850]) ).
cnf(s17594,plain,
( ~ spl111_76
| spl111_1395
| spl111_1478
| spl111_1479 ),
inference(sat_conversion,[],[f23867]) ).
cnf(s17611,plain,
( ~ spl111_76
| spl111_1395
| spl111_1478
| ~ spl111_1482 ),
inference(sat_conversion,[],[f23892]) ).
cnf(s17620,plain,
( ~ spl111_76
| ~ spl111_1395
| spl111_1481 ),
inference(sat_conversion,[],[f23914]) ).
cnf(s17625,plain,
( ~ spl111_76
| spl111_1478
| ~ spl111_1481
| ~ spl111_1482 ),
inference(sat_conversion,[],[f23919]) ).
cnf(s17626,plain,
( spl111_1230
| ~ spl111_79
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(rat,[],[s15117,s15167]) ).
cnf(s17627,plain,
( ~ spl111_1230
| ~ spl111_79
| spl111_75
| spl111_76
| spl111_77
| ~ spl111_314 ),
inference(rat,[],[s15158,s15140]) ).
cnf(s17628,plain,
( ~ spl111_79
| ~ spl111_314
| spl111_75
| spl111_76
| spl111_77 ),
inference(rat,[],[s17627,s17626]) ).
cnf(s17629,plain,
( spl111_77
| spl111_76
| spl111_75 ),
inference(rat,[],[s17628,s586,s9305]) ).
cnf(s17630,plain,
( spl111_666
| ~ spl111_968
| ~ spl111_77 ),
inference(rat,[],[s12318,s12352,s12296]) ).
cnf(s17631,plain,
( spl111_666
| ~ spl111_77 ),
inference(rat,[],[s17630,s12361]) ).
cnf(s17632,plain,
( spl111_968
| ~ spl111_666
| ~ spl111_77 ),
inference(rat,[],[s12128,s12267]) ).
cnf(s17633,plain,
( ~ spl111_968
| ~ spl111_666
| ~ spl111_77 ),
inference(rat,[],[s12274,s12286]) ).
cnf(s17634,plain,
( ~ spl111_666
| ~ spl111_77 ),
inference(rat,[],[s17633,s17632]) ).
cnf(s17635,plain,
~ spl111_77,
inference(rat,[],[s17634,s17631]) ).
cnf(s17636,plain,
( spl111_1478
| spl111_1395
| ~ spl111_76 ),
inference(rat,[],[s17554,s17611,s17594]) ).
cnf(s17637,plain,
( ~ spl111_1478
| spl111_1395
| ~ spl111_76 ),
inference(rat,[],[s17554,s17559,s17581]) ).
cnf(s17638,plain,
( spl111_1395
| ~ spl111_76 ),
inference(rat,[],[s17637,s17636]) ).
cnf(s17639,plain,
( spl111_1478
| ~ spl111_76 ),
inference(rat,[],[s17554,s17625,s17422,s17620,s17638]) ).
cnf(s17640,plain,
( ~ spl111_1478
| ~ spl111_76
| ~ spl111_1395 ),
inference(rat,[],[s17507,s17522]) ).
cnf(s17641,plain,
~ spl111_76,
inference(rat,[],[s17640,s17639,s17638]) ).
cnf(s17642,plain,
spl111_75,
inference(rat,[],[s17629,s17635,s17641]) ).
cnf(s17644,plain,
spl111_1145,
inference(rat,[],[s14419,s17642]) ).
cnf(s17647,plain,
spl111_1228,
inference(rat,[],[s14597,s17642,s17644]) ).
cnf(s17648,plain,
$false,
inference(rat,[],[s14588,s17642,s17647,s17644]) ).
tff(f23920,plain,
$false,
inference(avatar_sat_refutation,[],[s17648]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL942_2 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 17:10:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 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
% 5.05/1.15 % (3749331)Will run a generic schedule for satisfiability detection.
% 5.05/1.15 % (3749336)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1276542866_2999 on theBenchmark for (2999ds/0Mi)
% 5.05/1.15 % (3749337)% WARNING: option uhcvi not known.
% 5.05/1.15 % (3749338)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=712043043:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.05/1.15 % (3749339)dis+10_1_sil=32000:sp=arity:random_seed=329291089:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.05/1.15 % (3749340)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2386557653:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.05/1.15 % (3749341)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4172760624:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.05/1.15 % (3749342)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2073267597:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.05/1.15 % (3749337)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=285618489:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.05/1.15 % TRYING [1]
% 5.05/1.15 % TRYING [2]
% 5.05/1.15 % TRYING [3]
% 5.05/1.15 % TRYING [4]
% 5.05/1.15 % (3749339)Instruction limit reached!
% 5.05/1.15 % (3749339)------------------------------
% 5.05/1.15 % (3749339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749339)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749339)Termination reason: Instruction limit
% 5.05/1.15 % (3749339)Termination phase: Saturation
% 5.05/1.15 % (3749339)Time elapsed: 0.055 s
% 5.05/1.15 % (3749339)Peak memory usage: 15 MB
% 5.05/1.15 % (3749339)Instructions burned: 103 (million)
% 5.05/1.15 % (3749340)Instruction limit reached!
% 5.05/1.15 % (3749340)------------------------------
% 5.05/1.15 % (3749340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749340)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749340)Termination reason: Instruction limit
% 5.05/1.15 % (3749340)Termination phase: Saturation
% 5.05/1.15 % (3749340)Time elapsed: 0.060 s
% 5.05/1.15 % (3749340)Peak memory usage: 13 MB
% 5.05/1.15 % (3749340)Instructions burned: 118 (million)
% 5.05/1.15 % (3749341)Instruction limit reached!
% 5.05/1.15 % (3749341)------------------------------
% 5.05/1.15 % (3749341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749341)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749341)Termination reason: Instruction limit
% 5.05/1.15 % (3749341)Termination phase: Saturation
% 5.05/1.15 % (3749341)Time elapsed: 0.066 s
% 5.05/1.15 % (3749341)Peak memory usage: 17 MB
% 5.05/1.15 % (3749341)Instructions burned: 131 (million)
% 5.05/1.15 % (3749350)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1187501339:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.05/1.15 % (3749342)Instruction limit reached!
% 5.05/1.15 % (3749342)------------------------------
% 5.05/1.15 % (3749342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749351)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=954384789:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.05/1.15 % (3749342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749342)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749342)Termination reason: Instruction limit
% 5.05/1.15 % (3749342)Termination phase: Saturation
% 5.05/1.15 % (3749342)Time elapsed: 0.079 s
% 5.05/1.15 % (3749342)Peak memory usage: 16 MB
% 5.05/1.15 % (3749342)Instructions burned: 160 (million)
% 5.05/1.15 % (3749352)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1996025833:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.05/1.15 % (3749360)ott-21_1_sil=16000:fs=off:random_seed=893023954:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.05/1.15 % TRYING [1]
% 5.05/1.15 % TRYING [2]
% 5.05/1.15 % TRYING [3]
% 5.05/1.15 % (3749351)Instruction limit reached!
% 5.05/1.15 % (3749351)------------------------------
% 5.05/1.15 % (3749351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749351)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749351)Termination reason: Instruction limit
% 5.05/1.15 % (3749351)Termination phase: Saturation
% 5.05/1.15 % (3749351)Time elapsed: 0.067 s
% 5.05/1.15 % (3749351)Peak memory usage: 16 MB
% 5.05/1.15 % (3749351)Instructions burned: 132 (million)
% 5.05/1.15 % TRYING [4]
% 5.05/1.15 % (3749392)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2815897555:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.05/1.15 % (3749360)Instruction limit reached!
% 5.05/1.15 % (3749360)------------------------------
% 5.05/1.15 % (3749360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749360)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749360)Termination reason: Instruction limit
% 5.05/1.15 % (3749360)Termination phase: Saturation
% 5.05/1.15 % (3749360)Time elapsed: 0.087 s
% 5.05/1.15 % (3749360)Peak memory usage: 13 MB
% 5.05/1.15 % (3749360)Instructions burned: 180 (million)
% 5.05/1.15 % (3749407)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2619428610:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.05/1.15 % TRYING [5]
% 5.05/1.15 % TRYING [1]
% 5.05/1.15 % TRYING [2]
% 5.05/1.15 % TRYING [5]
% 5.05/1.15 % TRYING [3]
% 5.05/1.15 % (3749350)Instruction limit reached!
% 5.05/1.15 % (3749350)------------------------------
% 5.05/1.15 % (3749350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749350)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749350)Termination reason: Instruction limit
% 5.05/1.15 % (3749350)Termination phase: Finite model building constraint generation
% 5.05/1.15 % (3749350)Time elapsed: 0.293 s
% 5.05/1.15 % (3749350)Peak memory usage: 29 MB
% 5.05/1.15 % (3749350)Instructions burned: 716 (million)
% 5.05/1.15 % (3749409)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1757153369:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 5.05/1.15 % (3749352)Instruction limit reached!
% 5.05/1.15 % (3749352)------------------------------
% 5.05/1.15 % (3749352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749352)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749352)Termination reason: Instruction limit
% 5.05/1.15 % (3749352)Termination phase: Saturation
% 5.05/1.15 % (3749352)Time elapsed: 0.318 s
% 5.05/1.15 % (3749352)Peak memory usage: 26 MB
% 5.05/1.15 % (3749352)Instructions burned: 685 (million)
% 5.05/1.15 % (3749392)Instruction limit reached!
% 5.05/1.15 % (3749392)------------------------------
% 5.05/1.15 % (3749392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749392)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749392)Termination reason: Instruction limit
% 5.05/1.15 % (3749392)Termination phase: Saturation
% 5.05/1.15 % (3749392)Time elapsed: 0.247 s
% 5.05/1.15 % (3749392)Peak memory usage: 18 MB
% 5.05/1.15 % (3749392)Instructions burned: 478 (million)
% 5.05/1.15 % (3749411)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=186992468:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.05/1.15 % TRYING [4]
% 5.05/1.15 % (3749412)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4222848623:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 5.05/1.15 % (3749407)Instruction limit reached!
% 5.05/1.15 % (3749407)------------------------------
% 5.05/1.15 % (3749407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.15 % (3749407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.15 % (3749407)CaDiCaL version: 2.1.3
% 5.05/1.15 % (3749407)Termination reason: Instruction limit
% 5.05/1.15 % (3749407)Termination phase: Finite model building SAT solving
% 5.05/1.15 % (3749407)Time elapsed: 0.354 s
% 5.05/1.15 % (3749407)Peak memory usage: 25 MB
% 5.05/1.15 % (3749407)Instructions burned: 867 (million)
% 5.05/1.15 % (3749415)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2472345685:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.05/1.15 % (3749338) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3749331-3749338"...
% 5.05/1.15 % (3749338)...printing done.
% 5.05/1.15 % (3749338)Refutation found. Thanks to Tanya!
% 5.05/1.15 % SZS status Theorem for theBenchmark
% 5.05/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 5.05/1.16 % (3749338)------------------------------
% 5.05/1.16 % (3749338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.05/1.16 % (3749338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.05/1.16 % (3749338)CaDiCaL version: 2.1.3
% 5.05/1.16 % (3749338)Termination reason: Refutation
% 5.05/1.16 % (3749338)Time elapsed: 0.701 s
% 5.05/1.16 % (3749338)Peak memory usage: 26 MB
% 5.05/1.16 % (3749338)Instructions burned: 1543 (million)
% 5.05/1.16 % (3749331)Success in time 0.742 s
% 5.05/1.16 % Vampire exiting
%------------------------------------------------------------------------------