%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:57:14 AM UTC 2026
% Result : Theorem 2.29s 1.51s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 39
% Syntax : Number of formulae : 497 ( 16 unt; 0 typ; 37 def)
% Number of atoms : 4249 ( 0 equ)
% Maximal formula atoms : 66 ( 8 avg)
% Number of connectives : 3306 (1258 ~;1664 |; 256 &)
% ( 26 <=>; 102 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 1704 (1704 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 46 ( 45 usr; 31 prp; 0-3 aty)
% Number of functors : 72 ( 72 usr; 2 con; 0-1 aty)
% Number of variables : 413 ( 0 sgn 329 !; 84 ?; 413 :)
% 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' > '$ki_world' ).
tff(func_def_9,type,
sK12: '$ki_world' > '$ki_world' ).
tff(func_def_10,type,
sK13: '$ki_world' > '$ki_world' ).
tff(func_def_11,type,
sK14: '$ki_world' > '$ki_world' ).
tff(func_def_12,type,
sK15: '$ki_world' > '$ki_world' ).
tff(func_def_13,type,
sK16: '$ki_world' > '$ki_world' ).
tff(func_def_14,type,
sK17: '$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' ).
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(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(f23,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(f29,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,[],[f23]) ).
tff(f30,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,[],[f29]) ).
tff(f36,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(f37,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(f38,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(f39,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(f40,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(f41,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(f42,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(f43,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(f44,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(f45,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(f46,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(f47,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,[],[f30,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36]) ).
tff(f48,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,[],[f46]) ).
tff(f49,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,[],[f48]) ).
tff(f50,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,[],[f45]) ).
tff(f51,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,[],[f50]) ).
tff(f52,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,[],[f44]) ).
tff(f53,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,[],[f52]) ).
tff(f54,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,[],[f43]) ).
tff(f55,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,[],[f54]) ).
tff(f56,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK11(X0),op(e0,e0),e0)
& '$ki_accessible'(X0,sK11(X0)) )
| ( ~ qmltpeq(sK12(X0),op(e1,e1),e0)
& '$ki_accessible'(X0,sK12(X0)) )
| ( ~ qmltpeq(sK13(X0),op(e2,e2),e0)
& '$ki_accessible'(X0,sK13(X0)) )
| sP3(X0)
| ~ sP7(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X1,sK11(X0)),skolemize(X2,sK12(X0)),skolemize(X3,sK13(X0))],[f55]) ).
tff(f57,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,[],[f42]) ).
tff(f58,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,[],[f57]) ).
tff(f59,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK14(X0),op(e0,e0),e1)
& '$ki_accessible'(X0,sK14(X0)) )
| ( ~ qmltpeq(sK15(X0),op(e1,e1),e1)
& '$ki_accessible'(X0,sK15(X0)) )
| ( ~ qmltpeq(sK16(X0),op(e2,e2),e1)
& '$ki_accessible'(X0,sK16(X0)) )
| sP2(X0)
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X1,sK14(X0)),skolemize(X2,sK15(X0)),skolemize(X3,sK16(X0))],[f58]) ).
tff(f60,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,[],[f41]) ).
tff(f61,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,[],[f60]) ).
tff(f62,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK17(X0),op(e0,e0),e2)
& '$ki_accessible'(X0,sK17(X0)) )
| ( ~ qmltpeq(sK18(X0),op(e1,e1),e2)
& '$ki_accessible'(X0,sK18(X0)) )
| ( ~ qmltpeq(sK19(X0),op(e2,e2),e2)
& '$ki_accessible'(X0,sK19(X0)) )
| sP1(X0)
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X1,sK17(X0)),skolemize(X2,sK18(X0)),skolemize(X3,sK19(X0))],[f61]) ).
tff(f63,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,[],[f40]) ).
tff(f64,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,[],[f63]) ).
tff(f65,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK20(X0),op(e0,e0),e3)
& '$ki_accessible'(X0,sK20(X0)) )
| ( ~ qmltpeq(sK21(X0),op(e1,e1),e3)
& '$ki_accessible'(X0,sK21(X0)) )
| ( ~ qmltpeq(sK22(X0),op(e2,e2),e3)
& '$ki_accessible'(X0,sK22(X0)) )
| sP0(X0)
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X1,sK20(X0)),skolemize(X2,sK21(X0)),skolemize(X3,sK22(X0))],[f64]) ).
tff(f66,plain,
! [X17: '$ki_world'] :
( ? [X21: '$ki_world'] :
( ~ qmltpeq(X21,op(e3,e3),e0)
& '$ki_accessible'(X17,X21) )
| ~ sP3(X17) ),
inference(nnf_transformation,[],[f39]) ).
tff(f67,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e0)
& '$ki_accessible'(X0,X1) )
| ~ sP3(X0) ),
inference(rectify,[],[f66]) ).
tff(f68,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK23(X0),op(e3,e3),e0)
& '$ki_accessible'(X0,sK23(X0)) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(X1,sK23(X0))],[f67]) ).
tff(f69,plain,
! [X17: '$ki_world'] :
( ? [X25: '$ki_world'] :
( ~ qmltpeq(X25,op(e3,e3),e1)
& '$ki_accessible'(X17,X25) )
| ~ sP2(X17) ),
inference(nnf_transformation,[],[f38]) ).
tff(f70,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e1)
& '$ki_accessible'(X0,X1) )
| ~ sP2(X0) ),
inference(rectify,[],[f69]) ).
tff(f71,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK24(X0),op(e3,e3),e1)
& '$ki_accessible'(X0,sK24(X0)) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X1,sK24(X0))],[f70]) ).
tff(f72,plain,
! [X17: '$ki_world'] :
( ? [X29: '$ki_world'] :
( ~ qmltpeq(X29,op(e3,e3),e2)
& '$ki_accessible'(X17,X29) )
| ~ sP1(X17) ),
inference(nnf_transformation,[],[f37]) ).
tff(f73,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e2)
& '$ki_accessible'(X0,X1) )
| ~ sP1(X0) ),
inference(rectify,[],[f72]) ).
tff(f74,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK25(X0),op(e3,e3),e2)
& '$ki_accessible'(X0,sK25(X0)) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X1,sK25(X0))],[f73]) ).
tff(f75,plain,
! [X17: '$ki_world'] :
( ? [X33: '$ki_world'] :
( ~ qmltpeq(X33,op(e3,e3),e3)
& '$ki_accessible'(X17,X33) )
| ~ sP0(X17) ),
inference(nnf_transformation,[],[f36]) ).
tff(f76,plain,
! [X0: '$ki_world'] :
( ? [X1: '$ki_world'] :
( ~ qmltpeq(X1,op(e3,e3),e3)
& '$ki_accessible'(X0,X1) )
| ~ sP0(X0) ),
inference(rectify,[],[f75]) ).
tff(f77,plain,
! [X0: '$ki_world'] :
( ( ~ qmltpeq(sK26(X0),op(e3,e3),e3)
& '$ki_accessible'(X0,sK26(X0)) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X1,sK26(X0))],[f76]) ).
tff(f78,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,[],[f47]) ).
tff(f79,plain,
( ( ( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,X1) )
& ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,X2) )
& ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK27,X3) )
& ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK27,X4) ) )
| sP10(sK27)
| sP9(sK27)
| sP8(sK27) )
& ! [X5: '$ki_world'] :
( ( sP7(X5)
& sP6(X5)
& sP5(X5)
& sP4(X5) )
| ~ '$ki_accessible'(sK27,X5) )
& '$ki_accessible'('$ki_local_world',sK27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X0,sK27)],[f78]) ).
tff(f82,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f83,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f84,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f85,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f86,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f87,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f88,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f89,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e2)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f90,plain,
! [X0: '$ki_world',X4: '$ki_world'] :
( ~ '$ki_accessible'(X0,X4)
| qmltpeq(X4,op(e3,e3),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f91,plain,
! [X3: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X3)
| qmltpeq(X3,op(e2,e2),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f92,plain,
! [X2: '$ki_world',X0: '$ki_world'] :
( ~ '$ki_accessible'(X0,X2)
| qmltpeq(X2,op(e1,e1),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f93,plain,
! [X0: '$ki_world',X1: '$ki_world'] :
( ~ '$ki_accessible'(X0,X1)
| qmltpeq(X1,op(e0,e0),e3)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f94,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK13(X0))
| '$ki_accessible'(X0,sK12(X0))
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f95,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK13(X0),op(e2,e2),e0)
| '$ki_accessible'(X0,sK12(X0))
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f96,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| '$ki_accessible'(X0,sK11(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f97,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK13(X0),op(e2,e2),e0)
| ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f98,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK12(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f99,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK13(X0),op(e2,e2),e0)
| '$ki_accessible'(X0,sK12(X0))
| ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f100,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f101,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK13(X0),op(e2,e2),e0)
| ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f56]) ).
tff(f102,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK16(X0))
| '$ki_accessible'(X0,sK15(X0))
| '$ki_accessible'(X0,sK14(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f103,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK16(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK15(X0))
| '$ki_accessible'(X0,sK14(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f104,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK15(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK14(X0))
| '$ki_accessible'(X0,sK16(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f105,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK16(X0),op(e2,e2),e1)
| ~ qmltpeq(sK15(X0),op(e1,e1),e1)
| '$ki_accessible'(X0,sK14(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f106,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK14(X0),op(e0,e0),e1)
| '$ki_accessible'(X0,sK15(X0))
| '$ki_accessible'(X0,sK16(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f107,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK16(X0),op(e2,e2),e1)
| '$ki_accessible'(X0,sK15(X0))
| ~ qmltpeq(sK14(X0),op(e0,e0),e1)
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f108,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK15(X0),op(e1,e1),e1)
| ~ qmltpeq(sK14(X0),op(e0,e0),e1)
| '$ki_accessible'(X0,sK16(X0))
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f109,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK16(X0),op(e2,e2),e1)
| ~ qmltpeq(sK15(X0),op(e1,e1),e1)
| ~ qmltpeq(sK14(X0),op(e0,e0),e1)
| sP2(X0)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tff(f110,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK19(X0))
| '$ki_accessible'(X0,sK18(X0))
| '$ki_accessible'(X0,sK17(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f111,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK19(X0),op(e2,e2),e2)
| '$ki_accessible'(X0,sK18(X0))
| '$ki_accessible'(X0,sK17(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f112,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK18(X0),op(e1,e1),e2)
| '$ki_accessible'(X0,sK17(X0))
| '$ki_accessible'(X0,sK19(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f113,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK19(X0),op(e2,e2),e2)
| ~ qmltpeq(sK18(X0),op(e1,e1),e2)
| '$ki_accessible'(X0,sK17(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f114,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK17(X0),op(e0,e0),e2)
| '$ki_accessible'(X0,sK18(X0))
| '$ki_accessible'(X0,sK19(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f115,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK19(X0),op(e2,e2),e2)
| '$ki_accessible'(X0,sK18(X0))
| ~ qmltpeq(sK17(X0),op(e0,e0),e2)
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f116,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK18(X0),op(e1,e1),e2)
| ~ qmltpeq(sK17(X0),op(e0,e0),e2)
| '$ki_accessible'(X0,sK19(X0))
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f117,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK19(X0),op(e2,e2),e2)
| ~ qmltpeq(sK18(X0),op(e1,e1),e2)
| ~ qmltpeq(sK17(X0),op(e0,e0),e2)
| sP1(X0)
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f62]) ).
tff(f118,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK22(X0))
| '$ki_accessible'(X0,sK21(X0))
| '$ki_accessible'(X0,sK20(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f119,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK22(X0),op(e2,e2),e3)
| '$ki_accessible'(X0,sK21(X0))
| '$ki_accessible'(X0,sK20(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f120,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK21(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK20(X0))
| '$ki_accessible'(X0,sK22(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f121,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK22(X0),op(e2,e2),e3)
| ~ qmltpeq(sK21(X0),op(e1,e1),e3)
| '$ki_accessible'(X0,sK20(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f122,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK20(X0),op(e0,e0),e3)
| '$ki_accessible'(X0,sK21(X0))
| '$ki_accessible'(X0,sK22(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f123,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK22(X0),op(e2,e2),e3)
| '$ki_accessible'(X0,sK21(X0))
| ~ qmltpeq(sK20(X0),op(e0,e0),e3)
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f124,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK21(X0),op(e1,e1),e3)
| ~ qmltpeq(sK20(X0),op(e0,e0),e3)
| '$ki_accessible'(X0,sK22(X0))
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f125,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK22(X0),op(e2,e2),e3)
| ~ qmltpeq(sK21(X0),op(e1,e1),e3)
| ~ qmltpeq(sK20(X0),op(e0,e0),e3)
| sP0(X0)
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f65]) ).
tff(f126,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK23(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f68]) ).
tff(f127,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK23(X0),op(e3,e3),e0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f68]) ).
tff(f128,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK24(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f71]) ).
tff(f129,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK24(X0),op(e3,e3),e1)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f71]) ).
tff(f130,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK25(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f131,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK25(X0),op(e3,e3),e2)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f132,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'(X0,sK26(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f77]) ).
tff(f133,plain,
! [X0: '$ki_world'] :
( ~ qmltpeq(sK26(X0),op(e3,e3),e3)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f77]) ).
tff(f135,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK27,X5)
| sP4(X5) ),
inference(cnf_transformation,[],[f79]) ).
tff(f136,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK27,X5)
| sP5(X5) ),
inference(cnf_transformation,[],[f79]) ).
tff(f137,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK27,X5)
| sP6(X5) ),
inference(cnf_transformation,[],[f79]) ).
tff(f138,plain,
! [X5: '$ki_world'] :
( ~ '$ki_accessible'(sK27,X5)
| sP7(X5) ),
inference(cnf_transformation,[],[f79]) ).
tff(f139,plain,
! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK27,X4)
| sP10(sK27)
| sP9(sK27)
| sP8(sK27) ),
inference(cnf_transformation,[],[f79]) ).
tff(f140,plain,
! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK27,X3)
| sP10(sK27)
| sP9(sK27)
| sP8(sK27) ),
inference(cnf_transformation,[],[f79]) ).
tff(f141,plain,
! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,X2)
| sP10(sK27)
| sP9(sK27)
| sP8(sK27) ),
inference(cnf_transformation,[],[f79]) ).
tff(f142,plain,
! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,X1)
| sP10(sK27)
| sP9(sK27)
| sP8(sK27) ),
inference(cnf_transformation,[],[f79]) ).
tff(f143,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f543,definition,
( spl82_65
<=> sP8(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_65])],[avatar_definition]) ).
tff(f545,plain,
( sP8(sK27)
| ~ spl82_65 ),
inference(avatar_component_clause,[],[f543]) ).
tff(f547,definition,
( spl82_66
<=> sP9(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_66])],[avatar_definition]) ).
tff(f549,plain,
( sP9(sK27)
| ~ spl82_66 ),
inference(avatar_component_clause,[],[f547]) ).
tff(f551,definition,
( spl82_67
<=> sP10(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_67])],[avatar_definition]) ).
tff(f553,plain,
( sP10(sK27)
| ~ spl82_67 ),
inference(avatar_component_clause,[],[f551]) ).
tff(f555,definition,
( spl82_68
<=> ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK27,X4) ) ),
introduced(definition,[new_symbols(definition,[spl82_68])],[avatar_definition]) ).
tff(f556,plain,
( ! [X4: '$ki_world'] :
( qmltpeq(X4,op(e3,e3),e0)
| ~ '$ki_accessible'(sK27,X4) )
| ~ spl82_68 ),
inference(avatar_component_clause,[],[f555]) ).
tff(f557,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_68 ),
inference(avatar_split_clause,[],[f139,f555,f551,f547,f543]) ).
tff(f559,definition,
( spl82_69
<=> ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK27,X3) ) ),
introduced(definition,[new_symbols(definition,[spl82_69])],[avatar_definition]) ).
tff(f560,plain,
( ! [X3: '$ki_world'] :
( qmltpeq(X3,op(e2,e2),e0)
| ~ '$ki_accessible'(sK27,X3) )
| ~ spl82_69 ),
inference(avatar_component_clause,[],[f559]) ).
tff(f561,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_69 ),
inference(avatar_split_clause,[],[f140,f559,f551,f547,f543]) ).
tff(f563,definition,
( spl82_70
<=> ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,X2) ) ),
introduced(definition,[new_symbols(definition,[spl82_70])],[avatar_definition]) ).
tff(f564,plain,
( ! [X2: '$ki_world'] :
( qmltpeq(X2,op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,X2) )
| ~ spl82_70 ),
inference(avatar_component_clause,[],[f563]) ).
tff(f565,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_70 ),
inference(avatar_split_clause,[],[f141,f563,f551,f547,f543]) ).
tff(f567,definition,
( spl82_71
<=> ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,X1) ) ),
introduced(definition,[new_symbols(definition,[spl82_71])],[avatar_definition]) ).
tff(f568,plain,
( ! [X1: '$ki_world'] :
( qmltpeq(X1,op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,X1) )
| ~ spl82_71 ),
inference(avatar_component_clause,[],[f567]) ).
tff(f569,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_71 ),
inference(avatar_split_clause,[],[f142,f567,f551,f547,f543]) ).
tff(f570,plain,
sP7(sK27),
inference(resolution,[],[f143,f138]) ).
tff(f571,plain,
sP6(sK27),
inference(resolution,[],[f143,f137]) ).
tff(f572,plain,
sP5(sK27),
inference(resolution,[],[f143,f136]) ).
tff(f573,plain,
sP4(sK27),
inference(resolution,[],[f143,f135]) ).
tff(f583,definition,
( spl82_73
<=> sP3(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_73])],[avatar_definition]) ).
tff(f584,plain,
( sP3(sK27)
| ~ spl82_73 ),
inference(avatar_component_clause,[],[f583]) ).
tff(f585,plain,
( ~ sP3(sK27)
| spl82_73 ),
inference(avatar_component_clause,[],[f583]) ).
tff(f611,definition,
( spl82_78
<=> sP2(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_78])],[avatar_definition]) ).
tff(f613,plain,
( ~ sP2(sK27)
| spl82_78 ),
inference(avatar_component_clause,[],[f611]) ).
tff(f639,definition,
( spl82_83
<=> sP1(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_83])],[avatar_definition]) ).
tff(f641,plain,
( ~ sP1(sK27)
| spl82_83 ),
inference(avatar_component_clause,[],[f639]) ).
tff(f667,definition,
( spl82_88
<=> sP0(sK27) ),
introduced(definition,[new_symbols(definition,[spl82_88])],[avatar_definition]) ).
tff(f669,plain,
( ~ sP0(sK27)
| spl82_88 ),
inference(avatar_component_clause,[],[f667]) ).
tff(f1122,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK24(X0),op(e3,e3),e1)
| ~ sP10(X0)
| ~ sP2(X0) ),
inference(resolution,[],[f82,f128]) ).
tff(f1179,plain,
! [X0: '$ki_world'] :
( ~ sP10(X0)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f1122,f129]) ).
tff(f1373,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK25(X0),op(e3,e3),e2)
| ~ sP9(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f86,f130]) ).
tff(f1429,plain,
! [X0: '$ki_world'] :
( ~ sP9(X0)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f1373,f131]) ).
tff(f1624,plain,
! [X0: '$ki_world'] :
( qmltpeq(sK26(X0),op(e3,e3),e3)
| ~ sP8(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f90,f132]) ).
tff(f1679,plain,
! [X0: '$ki_world'] :
( ~ sP8(X0)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f1624,f133]) ).
tff(f1898,definition,
( spl82_99
<=> '$ki_accessible'(sK27,sK11(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_99])],[avatar_definition]) ).
tff(f1899,plain,
( ~ '$ki_accessible'(sK27,sK11(sK27))
| spl82_99 ),
inference(avatar_component_clause,[],[f1898]) ).
tff(f1900,plain,
( '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_99 ),
inference(avatar_component_clause,[],[f1898]) ).
tff(f1902,definition,
( spl82_100
<=> '$ki_accessible'(sK27,sK12(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_100])],[avatar_definition]) ).
tff(f1904,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_100 ),
inference(avatar_component_clause,[],[f1902]) ).
tff(f1955,definition,
( spl82_105
<=> '$ki_accessible'(sK27,sK14(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_105])],[avatar_definition]) ).
tff(f1956,plain,
( ~ '$ki_accessible'(sK27,sK14(sK27))
| spl82_105 ),
inference(avatar_component_clause,[],[f1955]) ).
tff(f1957,plain,
( '$ki_accessible'(sK27,sK14(sK27))
| ~ spl82_105 ),
inference(avatar_component_clause,[],[f1955]) ).
tff(f1959,definition,
( spl82_106
<=> '$ki_accessible'(sK27,sK15(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_106])],[avatar_definition]) ).
tff(f1960,plain,
( ~ '$ki_accessible'(sK27,sK15(sK27))
| spl82_106 ),
inference(avatar_component_clause,[],[f1959]) ).
tff(f1961,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| ~ spl82_106 ),
inference(avatar_component_clause,[],[f1959]) ).
tff(f2012,definition,
( spl82_111
<=> '$ki_accessible'(sK27,sK17(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_111])],[avatar_definition]) ).
tff(f2013,plain,
( ~ '$ki_accessible'(sK27,sK17(sK27))
| spl82_111 ),
inference(avatar_component_clause,[],[f2012]) ).
tff(f2014,plain,
( '$ki_accessible'(sK27,sK17(sK27))
| ~ spl82_111 ),
inference(avatar_component_clause,[],[f2012]) ).
tff(f2016,definition,
( spl82_112
<=> '$ki_accessible'(sK27,sK18(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_112])],[avatar_definition]) ).
tff(f2017,plain,
( ~ '$ki_accessible'(sK27,sK18(sK27))
| spl82_112 ),
inference(avatar_component_clause,[],[f2016]) ).
tff(f2018,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| ~ spl82_112 ),
inference(avatar_component_clause,[],[f2016]) ).
tff(f2069,definition,
( spl82_117
<=> '$ki_accessible'(sK27,sK20(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_117])],[avatar_definition]) ).
tff(f2070,plain,
( ~ '$ki_accessible'(sK27,sK20(sK27))
| spl82_117 ),
inference(avatar_component_clause,[],[f2069]) ).
tff(f2071,plain,
( '$ki_accessible'(sK27,sK20(sK27))
| ~ spl82_117 ),
inference(avatar_component_clause,[],[f2069]) ).
tff(f2073,definition,
( spl82_118
<=> '$ki_accessible'(sK27,sK21(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_118])],[avatar_definition]) ).
tff(f2074,plain,
( ~ '$ki_accessible'(sK27,sK21(sK27))
| spl82_118 ),
inference(avatar_component_clause,[],[f2073]) ).
tff(f2075,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| ~ spl82_118 ),
inference(avatar_component_clause,[],[f2073]) ).
tff(f2099,plain,
( ~ sP0(sK27)
| ~ spl82_65 ),
inference(resolution,[],[f1679,f545]) ).
tff(f2102,plain,
( ~ sP1(sK27)
| ~ spl82_66 ),
inference(resolution,[],[f549,f1429]) ).
tff(f2105,plain,
( ~ sP2(sK27)
| ~ spl82_67 ),
inference(resolution,[],[f553,f1179]) ).
tff(f2108,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK23(X0))
| ~ sP3(X0) )
| ~ spl82_68 ),
inference(resolution,[],[f556,f127]) ).
tff(f2110,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| '$ki_accessible'(X0,sK12(X0))
| ~ '$ki_accessible'(sK27,sK13(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_69 ),
inference(resolution,[],[f560,f99]) ).
tff(f2113,plain,
( ~ sP3(sK27)
| ~ sP3(sK27)
| ~ spl82_68 ),
inference(resolution,[],[f2108,f126]) ).
tff(f2114,plain,
( ~ sP3(sK27)
| ~ spl82_68 ),
inference(duplicate_literal_removal,[],[f2113]) ).
tff(f2115,plain,
( $false
| ~ spl82_68
| ~ spl82_73 ),
inference(forward_subsumption_resolution,[],[f2114,f584]) ).
tff(f2116,plain,
( ~ spl82_68
| ~ spl82_73 ),
inference(avatar_contradiction_clause,[],[f2115]) ).
tff(f2117,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,sK12(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_70 ),
inference(resolution,[],[f564,f100]) ).
tff(f2119,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK11(X0))
| '$ki_accessible'(X0,sK12(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_71 ),
inference(resolution,[],[f568,f98]) ).
tff(f2138,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK13(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_71
| ~ spl82_99 ),
inference(resolution,[],[f2119,f1900]) ).
tff(f2139,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK13(sK27))
| ~ sP7(sK27)
| ~ spl82_71
| spl82_73
| ~ spl82_99 ),
inference(forward_subsumption_resolution,[],[f2138,f585]) ).
tff(f2140,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK13(sK27))
| ~ spl82_71
| spl82_73
| ~ spl82_99 ),
inference(forward_subsumption_resolution,[],[f2139,f570]) ).
tff(f2142,definition,
( spl82_122
<=> '$ki_accessible'(sK27,sK13(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_122])],[avatar_definition]) ).
tff(f2144,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ spl82_122 ),
inference(avatar_component_clause,[],[f2142]) ).
tff(f2145,plain,
( spl82_122
| spl82_100
| ~ spl82_71
| spl82_73
| ~ spl82_99 ),
inference(avatar_split_clause,[],[f2140,f1898,f583,f567,f1902,f2142]) ).
tff(f2163,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK13(X0))
| '$ki_accessible'(X0,sK12(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK27,sK11(X0)) )
| ~ spl82_69
| ~ spl82_71 ),
inference(resolution,[],[f2110,f568]) ).
tff(f2165,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK12(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK27,sK11(X0)) )
| ~ spl82_70
| ~ spl82_71 ),
inference(resolution,[],[f2117,f568]) ).
tff(f2178,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_70
| ~ spl82_71
| ~ spl82_100 ),
inference(resolution,[],[f2165,f1904]) ).
tff(f2179,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2178,f585]) ).
tff(f2180,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2179,f570]) ).
tff(f2181,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2180,f1900]) ).
tff(f2182,plain,
( spl82_122
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100 ),
inference(avatar_split_clause,[],[f2181,f1902,f1898,f583,f567,f563,f2142]) ).
tff(f2183,plain,
( ~ spl82_78
| ~ spl82_67 ),
inference(avatar_split_clause,[],[f2105,f551,f611]) ).
tff(f2200,plain,
( qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ sP10(sK27)
| ~ spl82_105 ),
inference(resolution,[],[f1957,f85]) ).
tff(f2209,plain,
( qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ spl82_67
| ~ spl82_105 ),
inference(forward_subsumption_resolution,[],[f2200,f553]) ).
tff(f2232,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| '$ki_accessible'(sK27,sK16(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_105 ),
inference(resolution,[],[f2209,f106]) ).
tff(f2233,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| '$ki_accessible'(sK27,sK16(sK27))
| ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| ~ spl82_105 ),
inference(forward_subsumption_resolution,[],[f2232,f613]) ).
tff(f2234,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| '$ki_accessible'(sK27,sK16(sK27))
| ~ spl82_67
| spl82_78
| ~ spl82_105 ),
inference(forward_subsumption_resolution,[],[f2233,f571]) ).
tff(f2236,definition,
( spl82_123
<=> '$ki_accessible'(sK27,sK16(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_123])],[avatar_definition]) ).
tff(f2237,plain,
( ~ '$ki_accessible'(sK27,sK16(sK27))
| spl82_123 ),
inference(avatar_component_clause,[],[f2236]) ).
tff(f2238,plain,
( '$ki_accessible'(sK27,sK16(sK27))
| ~ spl82_123 ),
inference(avatar_component_clause,[],[f2236]) ).
tff(f2239,plain,
( spl82_123
| spl82_106
| ~ spl82_67
| spl82_78
| ~ spl82_105 ),
inference(avatar_split_clause,[],[f2234,f1955,f611,f551,f1959,f2236]) ).
tff(f2270,plain,
( qmltpeq(sK15(sK27),op(e1,e1),e1)
| ~ sP10(sK27)
| ~ spl82_106 ),
inference(resolution,[],[f1961,f84]) ).
tff(f2281,plain,
( qmltpeq(sK15(sK27),op(e1,e1),e1)
| ~ spl82_67
| ~ spl82_106 ),
inference(forward_subsumption_resolution,[],[f2270,f553]) ).
tff(f2285,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| '$ki_accessible'(sK27,sK16(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_106 ),
inference(resolution,[],[f2281,f108]) ).
tff(f2287,plain,
( '$ki_accessible'(sK27,sK16(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_105
| ~ spl82_106 ),
inference(forward_subsumption_resolution,[],[f2285,f2209]) ).
tff(f2288,plain,
( sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2287,f2237]) ).
tff(f2289,plain,
( ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2288,f613]) ).
tff(f2290,plain,
( $false
| ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2289,f571]) ).
tff(f2291,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| spl82_123 ),
inference(avatar_contradiction_clause,[],[f2290]) ).
tff(f2292,plain,
( ~ spl82_83
| ~ spl82_66 ),
inference(avatar_split_clause,[],[f2102,f547,f639]) ).
tff(f2321,plain,
( qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ sP9(sK27)
| ~ spl82_111 ),
inference(resolution,[],[f2014,f89]) ).
tff(f2326,plain,
( qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ spl82_66
| ~ spl82_111 ),
inference(forward_subsumption_resolution,[],[f2321,f549]) ).
tff(f2330,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| '$ki_accessible'(sK27,sK19(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_111 ),
inference(resolution,[],[f2326,f114]) ).
tff(f2331,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| '$ki_accessible'(sK27,sK19(sK27))
| ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| ~ spl82_111 ),
inference(forward_subsumption_resolution,[],[f2330,f641]) ).
tff(f2332,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| '$ki_accessible'(sK27,sK19(sK27))
| ~ spl82_66
| spl82_83
| ~ spl82_111 ),
inference(forward_subsumption_resolution,[],[f2331,f572]) ).
tff(f2334,definition,
( spl82_124
<=> '$ki_accessible'(sK27,sK19(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_124])],[avatar_definition]) ).
tff(f2335,plain,
( ~ '$ki_accessible'(sK27,sK19(sK27))
| spl82_124 ),
inference(avatar_component_clause,[],[f2334]) ).
tff(f2336,plain,
( '$ki_accessible'(sK27,sK19(sK27))
| ~ spl82_124 ),
inference(avatar_component_clause,[],[f2334]) ).
tff(f2337,plain,
( spl82_124
| spl82_112
| ~ spl82_66
| spl82_83
| ~ spl82_111 ),
inference(avatar_split_clause,[],[f2332,f2012,f639,f547,f2016,f2334]) ).
tff(f2372,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ sP9(sK27)
| ~ spl82_112 ),
inference(resolution,[],[f2018,f88]) ).
tff(f2379,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ spl82_66
| ~ spl82_112 ),
inference(forward_subsumption_resolution,[],[f2372,f549]) ).
tff(f2382,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| spl82_124 ),
inference(resolution,[],[f2335,f110]) ).
tff(f2383,plain,
( ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| '$ki_accessible'(sK27,sK19(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_112 ),
inference(resolution,[],[f2379,f116]) ).
tff(f2385,plain,
( '$ki_accessible'(sK27,sK19(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_111
| ~ spl82_112 ),
inference(forward_subsumption_resolution,[],[f2383,f2326]) ).
tff(f2386,plain,
( sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2385,f2335]) ).
tff(f2387,plain,
( ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| ~ spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2386,f641]) ).
tff(f2388,plain,
( $false
| ~ spl82_66
| spl82_83
| ~ spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2387,f572]) ).
tff(f2389,plain,
( ~ spl82_66
| spl82_83
| ~ spl82_111
| ~ spl82_112
| spl82_124 ),
inference(avatar_contradiction_clause,[],[f2388]) ).
tff(f2390,plain,
( ~ spl82_88
| ~ spl82_65 ),
inference(avatar_split_clause,[],[f2099,f543,f667]) ).
tff(f2431,plain,
( qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ sP8(sK27)
| ~ spl82_117 ),
inference(resolution,[],[f2071,f93]) ).
tff(f2432,plain,
( qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ spl82_65
| ~ spl82_117 ),
inference(forward_subsumption_resolution,[],[f2431,f545]) ).
tff(f2436,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| '$ki_accessible'(sK27,sK22(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_117 ),
inference(resolution,[],[f2432,f122]) ).
tff(f2437,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| '$ki_accessible'(sK27,sK22(sK27))
| ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| ~ spl82_117 ),
inference(forward_subsumption_resolution,[],[f2436,f669]) ).
tff(f2438,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| '$ki_accessible'(sK27,sK22(sK27))
| ~ spl82_65
| spl82_88
| ~ spl82_117 ),
inference(forward_subsumption_resolution,[],[f2437,f573]) ).
tff(f2440,definition,
( spl82_125
<=> '$ki_accessible'(sK27,sK22(sK27)) ),
introduced(definition,[new_symbols(definition,[spl82_125])],[avatar_definition]) ).
tff(f2441,plain,
( ~ '$ki_accessible'(sK27,sK22(sK27))
| spl82_125 ),
inference(avatar_component_clause,[],[f2440]) ).
tff(f2442,plain,
( '$ki_accessible'(sK27,sK22(sK27))
| ~ spl82_125 ),
inference(avatar_component_clause,[],[f2440]) ).
tff(f2443,plain,
( spl82_125
| spl82_118
| ~ spl82_65
| spl82_88
| ~ spl82_117 ),
inference(avatar_split_clause,[],[f2438,f2069,f667,f543,f2073,f2440]) ).
tff(f2482,plain,
( qmltpeq(sK21(sK27),op(e1,e1),e3)
| ~ sP8(sK27)
| ~ spl82_118 ),
inference(resolution,[],[f2075,f92]) ).
tff(f2485,plain,
( qmltpeq(sK21(sK27),op(e1,e1),e3)
| ~ spl82_65
| ~ spl82_118 ),
inference(forward_subsumption_resolution,[],[f2482,f545]) ).
tff(f2489,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| '$ki_accessible'(sK27,sK22(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_118 ),
inference(resolution,[],[f2485,f124]) ).
tff(f2491,plain,
( '$ki_accessible'(sK27,sK22(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_117
| ~ spl82_118 ),
inference(forward_subsumption_resolution,[],[f2489,f2432]) ).
tff(f2492,plain,
( sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2491,f2441]) ).
tff(f2493,plain,
( ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2492,f669]) ).
tff(f2494,plain,
( $false
| ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2493,f573]) ).
tff(f2495,plain,
( ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| spl82_125 ),
inference(avatar_contradiction_clause,[],[f2494]) ).
tff(f2496,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_71
| ~ spl82_122 ),
inference(resolution,[],[f2144,f2163]) ).
tff(f2518,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_71
| spl82_73
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2496,f585]) ).
tff(f2519,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_71
| spl82_73
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2518,f570]) ).
tff(f2520,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2519,f1900]) ).
tff(f2521,plain,
( spl82_100
| ~ spl82_69
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_122 ),
inference(avatar_split_clause,[],[f2520,f2142,f1898,f583,f567,f559,f1902]) ).
tff(f2527,plain,
( qmltpeq(sK15(sK27),op(e1,e1),e1)
| ~ spl82_67
| ~ spl82_106 ),
inference(forward_subsumption_resolution,[],[f2270,f553]) ).
tff(f2552,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK12(X0))
| '$ki_accessible'(X0,sK11(X0))
| '$ki_accessible'(X0,sK13(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_70 ),
inference(resolution,[],[f564,f96]) ).
tff(f2555,plain,
( '$ki_accessible'(sK27,sK14(sK27))
| '$ki_accessible'(sK27,sK16(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_106 ),
inference(resolution,[],[f2527,f104]) ).
tff(f2556,plain,
( '$ki_accessible'(sK27,sK16(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_105
| ~ spl82_106 ),
inference(forward_subsumption_resolution,[],[f2555,f1956]) ).
tff(f2558,plain,
( sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2556,f2237]) ).
tff(f2560,plain,
( ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2558,f613]) ).
tff(f2562,plain,
( $false
| ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2560,f571]) ).
tff(f2563,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| spl82_123 ),
inference(avatar_contradiction_clause,[],[f2562]) ).
tff(f2569,plain,
( qmltpeq(sK16(sK27),op(e2,e2),e1)
| ~ sP10(sK27)
| ~ spl82_123 ),
inference(resolution,[],[f2238,f83]) ).
tff(f2582,plain,
( qmltpeq(sK16(sK27),op(e2,e2),e1)
| ~ spl82_67
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2569,f553]) ).
tff(f2584,plain,
( ~ qmltpeq(sK15(sK27),op(e1,e1),e1)
| ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_123 ),
inference(resolution,[],[f2582,f109]) ).
tff(f2585,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_123 ),
inference(resolution,[],[f2582,f107]) ).
tff(f2586,plain,
( ~ qmltpeq(sK15(sK27),op(e1,e1),e1)
| '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_123 ),
inference(resolution,[],[f2582,f105]) ).
tff(f2588,plain,
( '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2586,f2527]) ).
tff(f2589,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2584,f2527]) ).
tff(f2590,plain,
( sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2588,f1956]) ).
tff(f2591,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2589,f613]) ).
tff(f2592,plain,
( ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2590,f613]) ).
tff(f2593,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ spl82_67
| spl82_78
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2591,f571]) ).
tff(f2594,plain,
( $false
| ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2592,f571]) ).
tff(f2595,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(avatar_contradiction_clause,[],[f2594]) ).
tff(f2603,plain,
( qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ sP10(sK27)
| ~ spl82_105 ),
inference(resolution,[],[f1957,f85]) ).
tff(f2612,plain,
( ~ sP10(sK27)
| ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2603,f2593]) ).
tff(f2616,plain,
( $false
| ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2612,f553]) ).
tff(f2617,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(avatar_contradiction_clause,[],[f2616]) ).
tff(f2618,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2585,f1960]) ).
tff(f2620,plain,
( qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ spl82_67
| ~ spl82_105 ),
inference(forward_subsumption_resolution,[],[f2603,f553]) ).
tff(f2621,plain,
( ~ qmltpeq(sK14(sK27),op(e0,e0),e1)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2618,f613]) ).
tff(f2623,plain,
( ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| ~ spl82_105
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2621,f2620]) ).
tff(f2625,plain,
( $false
| ~ spl82_67
| spl82_78
| ~ spl82_105
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2623,f571]) ).
tff(f2626,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| spl82_106
| ~ spl82_123 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
tff(f2632,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ spl82_66
| ~ spl82_112 ),
inference(forward_subsumption_resolution,[],[f2372,f549]) ).
tff(f2657,plain,
( '$ki_accessible'(sK27,sK17(sK27))
| '$ki_accessible'(sK27,sK19(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_112 ),
inference(resolution,[],[f2632,f112]) ).
tff(f2658,plain,
( '$ki_accessible'(sK27,sK19(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_111
| ~ spl82_112 ),
inference(forward_subsumption_resolution,[],[f2657,f2013]) ).
tff(f2660,plain,
( sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2658,f2335]) ).
tff(f2662,plain,
( ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2660,f641]) ).
tff(f2664,plain,
( $false
| ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2662,f572]) ).
tff(f2665,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| spl82_124 ),
inference(avatar_contradiction_clause,[],[f2664]) ).
tff(f2666,plain,
( '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2382,f2017]) ).
tff(f2667,plain,
( sP1(sK27)
| ~ sP5(sK27)
| spl82_111
| spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2666,f2013]) ).
tff(f2668,plain,
( ~ sP5(sK27)
| spl82_83
| spl82_111
| spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2667,f641]) ).
tff(f2669,plain,
( $false
| spl82_83
| spl82_111
| spl82_112
| spl82_124 ),
inference(forward_subsumption_resolution,[],[f2668,f572]) ).
tff(f2670,plain,
( spl82_83
| spl82_111
| spl82_112
| spl82_124 ),
inference(avatar_contradiction_clause,[],[f2669]) ).
tff(f2675,plain,
( qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ spl82_65
| ~ spl82_117 ),
inference(forward_subsumption_resolution,[],[f2431,f545]) ).
tff(f2680,plain,
( qmltpeq(sK21(sK27),op(e1,e1),e3)
| ~ spl82_65
| ~ spl82_118 ),
inference(forward_subsumption_resolution,[],[f2482,f545]) ).
tff(f2706,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ sP9(sK27)
| ~ spl82_112 ),
inference(resolution,[],[f2018,f88]) ).
tff(f2729,plain,
( qmltpeq(sK22(sK27),op(e2,e2),e3)
| ~ sP8(sK27)
| ~ spl82_125 ),
inference(resolution,[],[f2442,f91]) ).
tff(f2734,plain,
( qmltpeq(sK22(sK27),op(e2,e2),e3)
| ~ spl82_65
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2729,f545]) ).
tff(f2738,plain,
( '$ki_accessible'(sK27,sK20(sK27))
| '$ki_accessible'(sK27,sK22(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_118 ),
inference(resolution,[],[f2680,f120]) ).
tff(f2739,plain,
( ~ qmltpeq(sK21(sK27),op(e1,e1),e3)
| ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_125 ),
inference(resolution,[],[f2734,f125]) ).
tff(f2741,plain,
( ~ qmltpeq(sK21(sK27),op(e1,e1),e3)
| '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_125 ),
inference(resolution,[],[f2734,f121]) ).
tff(f2743,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2739,f2680]) ).
tff(f2744,plain,
( sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2743,f2675]) ).
tff(f2745,plain,
( ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2744,f669]) ).
tff(f2746,plain,
( $false
| ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2745,f573]) ).
tff(f2747,plain,
( ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(avatar_contradiction_clause,[],[f2746]) ).
tff(f2748,plain,
( '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2741,f2680]) ).
tff(f2750,plain,
( sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2748,f2070]) ).
tff(f2752,plain,
( ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2750,f669]) ).
tff(f2753,plain,
( $false
| ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f2752,f573]) ).
tff(f2754,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(avatar_contradiction_clause,[],[f2753]) ).
tff(f2756,plain,
( '$ki_accessible'(sK27,sK22(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_117
| ~ spl82_118 ),
inference(forward_subsumption_resolution,[],[f2738,f2070]) ).
tff(f2758,plain,
( sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2756,f2441]) ).
tff(f2760,plain,
( ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2758,f669]) ).
tff(f2761,plain,
( $false
| ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2760,f573]) ).
tff(f2762,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| spl82_125 ),
inference(avatar_contradiction_clause,[],[f2761]) ).
tff(f2766,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK13(X0))
| '$ki_accessible'(X0,sK12(X0))
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_69 ),
inference(resolution,[],[f560,f95]) ).
tff(f2767,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK11(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK11(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_69 ),
inference(resolution,[],[f2766,f94]) ).
tff(f2768,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| '$ki_accessible'(sK27,sK11(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_69 ),
inference(duplicate_literal_removal,[],[f2767]) ).
tff(f2769,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_69
| spl82_99 ),
inference(forward_subsumption_resolution,[],[f2768,f1899]) ).
tff(f2770,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ sP7(sK27)
| ~ spl82_69
| spl82_73
| spl82_99 ),
inference(forward_subsumption_resolution,[],[f2769,f585]) ).
tff(f2771,plain,
( '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| spl82_73
| spl82_99 ),
inference(forward_subsumption_resolution,[],[f2770,f570]) ).
tff(f2772,plain,
( spl82_100
| ~ spl82_69
| spl82_73
| spl82_99 ),
inference(avatar_split_clause,[],[f2771,f1898,f583,f559,f1902]) ).
tff(f2786,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ spl82_66
| ~ spl82_112 ),
inference(forward_subsumption_resolution,[],[f2706,f549]) ).
tff(f2799,plain,
( qmltpeq(sK19(sK27),op(e2,e2),e2)
| ~ sP9(sK27)
| ~ spl82_124 ),
inference(resolution,[],[f2336,f87]) ).
tff(f2808,plain,
( qmltpeq(sK19(sK27),op(e2,e2),e2)
| ~ spl82_66
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2799,f549]) ).
tff(f2810,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| spl82_125 ),
inference(resolution,[],[f2441,f118]) ).
tff(f2813,plain,
( ~ qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_124 ),
inference(resolution,[],[f2808,f117]) ).
tff(f2814,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_124 ),
inference(resolution,[],[f2808,f115]) ).
tff(f2815,plain,
( ~ qmltpeq(sK18(sK27),op(e1,e1),e2)
| '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_124 ),
inference(resolution,[],[f2808,f113]) ).
tff(f2816,plain,
( '$ki_accessible'(sK27,sK18(sK27))
| '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_124 ),
inference(resolution,[],[f2808,f111]) ).
tff(f2817,plain,
( '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| ~ spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2815,f2786]) ).
tff(f2819,plain,
( sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_111
| ~ spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2817,f2013]) ).
tff(f2821,plain,
( ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2819,f641]) ).
tff(f2823,plain,
( $false
| ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2821,f572]) ).
tff(f2824,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| ~ spl82_124 ),
inference(avatar_contradiction_clause,[],[f2823]) ).
tff(f2825,plain,
( '$ki_accessible'(sK27,sK17(sK27))
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2816,f2017]) ).
tff(f2827,plain,
( ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2814,f2017]) ).
tff(f2828,plain,
( ~ qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2813,f641]) ).
tff(f2829,plain,
( sP1(sK27)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_111
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2825,f2013]) ).
tff(f2831,plain,
( ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2827,f641]) ).
tff(f2832,plain,
( ~ qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ spl82_66
| spl82_83
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2828,f572]) ).
tff(f2833,plain,
( ~ sP5(sK27)
| ~ spl82_66
| spl82_83
| spl82_111
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2829,f641]) ).
tff(f2835,plain,
( ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ spl82_66
| spl82_83
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2831,f572]) ).
tff(f2837,definition,
( spl82_126
<=> qmltpeq(sK17(sK27),op(e0,e0),e2) ),
introduced(definition,[new_symbols(definition,[spl82_126])],[avatar_definition]) ).
tff(f2839,plain,
( ~ qmltpeq(sK17(sK27),op(e0,e0),e2)
| spl82_126 ),
inference(avatar_component_clause,[],[f2837]) ).
tff(f2841,definition,
( spl82_127
<=> qmltpeq(sK18(sK27),op(e1,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl82_127])],[avatar_definition]) ).
tff(f2843,plain,
( ~ qmltpeq(sK18(sK27),op(e1,e1),e2)
| spl82_127 ),
inference(avatar_component_clause,[],[f2841]) ).
tff(f2844,plain,
( ~ spl82_126
| ~ spl82_127
| ~ spl82_66
| spl82_83
| ~ spl82_124 ),
inference(avatar_split_clause,[],[f2832,f2334,f639,f547,f2841,f2837]) ).
tff(f2845,plain,
( $false
| ~ spl82_66
| spl82_83
| spl82_111
| spl82_112
| ~ spl82_124 ),
inference(forward_subsumption_resolution,[],[f2833,f572]) ).
tff(f2846,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| spl82_112
| ~ spl82_124 ),
inference(avatar_contradiction_clause,[],[f2845]) ).
tff(f2848,plain,
( ~ spl82_126
| ~ spl82_66
| spl82_83
| spl82_112
| ~ spl82_124 ),
inference(avatar_split_clause,[],[f2835,f2334,f2016,f639,f547,f2837]) ).
tff(f2855,plain,
( qmltpeq(sK16(sK27),op(e2,e2),e1)
| ~ spl82_67
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2569,f553]) ).
tff(f2865,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| ~ spl82_123 ),
inference(resolution,[],[f2855,f103]) ).
tff(f2866,plain,
( '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2865,f1960]) ).
tff(f2870,plain,
( sP2(sK27)
| ~ sP6(sK27)
| ~ spl82_67
| spl82_105
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2866,f1956]) ).
tff(f2874,plain,
( ~ sP6(sK27)
| ~ spl82_67
| spl82_78
| spl82_105
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2870,f613]) ).
tff(f2886,plain,
( $false
| ~ spl82_67
| spl82_78
| spl82_105
| spl82_106
| ~ spl82_123 ),
inference(forward_subsumption_resolution,[],[f2874,f571]) ).
tff(f2887,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| spl82_106
| ~ spl82_123 ),
inference(avatar_contradiction_clause,[],[f2886]) ).
tff(f2890,plain,
( '$ki_accessible'(sK27,sK15(sK27))
| '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| spl82_123 ),
inference(resolution,[],[f2237,f102]) ).
tff(f2891,plain,
( '$ki_accessible'(sK27,sK14(sK27))
| sP2(sK27)
| ~ sP6(sK27)
| spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2890,f1960]) ).
tff(f2892,plain,
( sP2(sK27)
| ~ sP6(sK27)
| spl82_105
| spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2891,f1956]) ).
tff(f2893,plain,
( ~ sP6(sK27)
| spl82_78
| spl82_105
| spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2892,f613]) ).
tff(f2894,plain,
( $false
| spl82_78
| spl82_105
| spl82_106
| spl82_123 ),
inference(forward_subsumption_resolution,[],[f2893,f571]) ).
tff(f2895,plain,
( spl82_78
| spl82_105
| spl82_106
| spl82_123 ),
inference(avatar_contradiction_clause,[],[f2894]) ).
tff(f2897,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,sK13(X0))
| ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_69 ),
inference(resolution,[],[f560,f101]) ).
tff(f2899,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK12(X0),op(e1,e1),e0)
| ~ '$ki_accessible'(sK27,sK13(X0))
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0) )
| ~ spl82_69 ),
inference(resolution,[],[f560,f97]) ).
tff(f2901,plain,
( '$ki_accessible'(sK27,sK11(sK27))
| '$ki_accessible'(sK27,sK13(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_70
| ~ spl82_100 ),
inference(resolution,[],[f1904,f2552]) ).
tff(f2918,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ spl82_70
| spl82_99
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2901,f1899]) ).
tff(f2919,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ sP7(sK27)
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2918,f585]) ).
tff(f2920,plain,
( '$ki_accessible'(sK27,sK13(sK27))
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100 ),
inference(forward_subsumption_resolution,[],[f2919,f570]) ).
tff(f2921,plain,
( spl82_122
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100 ),
inference(avatar_split_clause,[],[f2920,f1902,f1898,f583,f563,f2142]) ).
tff(f2941,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK13(X0))
| '$ki_accessible'(X0,sK11(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK27,sK12(X0)) )
| ~ spl82_69
| ~ spl82_70 ),
inference(resolution,[],[f2899,f564]) ).
tff(f2942,plain,
( ! [X0: '$ki_world'] :
( ~ qmltpeq(sK11(X0),op(e0,e0),e0)
| ~ '$ki_accessible'(sK27,sK13(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK27,sK12(X0)) )
| ~ spl82_69
| ~ spl82_70 ),
inference(resolution,[],[f2897,f564]) ).
tff(f2964,plain,
( '$ki_accessible'(sK27,sK11(sK27))
| sP3(sK27)
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| ~ spl82_70
| ~ spl82_122 ),
inference(resolution,[],[f2941,f2144]) ).
tff(f2967,plain,
( sP3(sK27)
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| ~ spl82_70
| spl82_99
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2964,f1899]) ).
tff(f2968,plain,
( ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2967,f585]) ).
tff(f2969,plain,
( ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ spl82_69
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2968,f570]) ).
tff(f2970,plain,
( $false
| ~ spl82_69
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2969,f1904]) ).
tff(f2971,plain,
( ~ spl82_69
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(avatar_contradiction_clause,[],[f2970]) ).
tff(f2989,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK27,sK13(X0))
| sP3(X0)
| ~ sP7(X0)
| ~ '$ki_accessible'(sK27,sK12(X0))
| ~ '$ki_accessible'(sK27,sK11(X0)) )
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71 ),
inference(resolution,[],[f2942,f568]) ).
tff(f2990,plain,
( sP3(sK27)
| ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| ~ spl82_122 ),
inference(resolution,[],[f2989,f2144]) ).
tff(f2993,plain,
( ~ sP7(sK27)
| ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2990,f585]) ).
tff(f2994,plain,
( ~ '$ki_accessible'(sK27,sK12(sK27))
| ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2993,f570]) ).
tff(f2995,plain,
( ~ '$ki_accessible'(sK27,sK11(sK27))
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_100
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2994,f1904]) ).
tff(f2996,plain,
( $false
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(forward_subsumption_resolution,[],[f2995,f1900]) ).
tff(f2997,plain,
( ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(avatar_contradiction_clause,[],[f2996]) ).
tff(f2998,plain,
( '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2810,f2074]) ).
tff(f3015,plain,
( sP0(sK27)
| ~ sP4(sK27)
| spl82_117
| spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f2998,f2070]) ).
tff(f3016,plain,
( ~ sP4(sK27)
| spl82_88
| spl82_117
| spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f3015,f669]) ).
tff(f3017,plain,
( $false
| spl82_88
| spl82_117
| spl82_118
| spl82_125 ),
inference(forward_subsumption_resolution,[],[f3016,f573]) ).
tff(f3018,plain,
( spl82_88
| spl82_117
| spl82_118
| spl82_125 ),
inference(avatar_contradiction_clause,[],[f3017]) ).
tff(f3033,plain,
( qmltpeq(sK22(sK27),op(e2,e2),e3)
| ~ sP8(sK27)
| ~ spl82_125 ),
inference(resolution,[],[f2442,f91]) ).
tff(f3038,plain,
( qmltpeq(sK22(sK27),op(e2,e2),e3)
| ~ spl82_65
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3033,f545]) ).
tff(f3041,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_125 ),
inference(resolution,[],[f3038,f123]) ).
tff(f3043,plain,
( '$ki_accessible'(sK27,sK21(sK27))
| '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| ~ spl82_125 ),
inference(resolution,[],[f3038,f119]) ).
tff(f3044,plain,
( '$ki_accessible'(sK27,sK20(sK27))
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3043,f2074]) ).
tff(f3046,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3041,f2074]) ).
tff(f3048,plain,
( sP0(sK27)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_117
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3044,f2070]) ).
tff(f3050,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3046,f669]) ).
tff(f3052,plain,
( ~ sP4(sK27)
| ~ spl82_65
| spl82_88
| spl82_117
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3048,f669]) ).
tff(f3054,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ spl82_65
| spl82_88
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3050,f573]) ).
tff(f3056,definition,
( spl82_130
<=> qmltpeq(sK20(sK27),op(e0,e0),e3) ),
introduced(definition,[new_symbols(definition,[spl82_130])],[avatar_definition]) ).
tff(f3058,plain,
( ~ qmltpeq(sK20(sK27),op(e0,e0),e3)
| spl82_130 ),
inference(avatar_component_clause,[],[f3056]) ).
tff(f3064,plain,
( $false
| ~ spl82_65
| spl82_88
| spl82_117
| spl82_118
| ~ spl82_125 ),
inference(forward_subsumption_resolution,[],[f3052,f573]) ).
tff(f3065,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| spl82_118
| ~ spl82_125 ),
inference(avatar_contradiction_clause,[],[f3064]) ).
tff(f3067,plain,
( ~ spl82_130
| ~ spl82_65
| spl82_88
| spl82_118
| ~ spl82_125 ),
inference(avatar_split_clause,[],[f3054,f2440,f2073,f667,f543,f3056]) ).
tff(f3083,plain,
( qmltpeq(sK20(sK27),op(e0,e0),e3)
| ~ sP8(sK27)
| ~ spl82_117 ),
inference(resolution,[],[f2071,f93]) ).
tff(f3084,plain,
( ~ sP8(sK27)
| ~ spl82_117
| spl82_130 ),
inference(forward_subsumption_resolution,[],[f3083,f3058]) ).
tff(f3088,plain,
( $false
| ~ spl82_65
| ~ spl82_117
| spl82_130 ),
inference(forward_subsumption_resolution,[],[f3084,f545]) ).
tff(f3089,plain,
( ~ spl82_65
| ~ spl82_117
| spl82_130 ),
inference(avatar_contradiction_clause,[],[f3088]) ).
tff(f3126,plain,
( qmltpeq(sK17(sK27),op(e0,e0),e2)
| ~ sP9(sK27)
| ~ spl82_111 ),
inference(resolution,[],[f2014,f89]) ).
tff(f3131,plain,
( ~ sP9(sK27)
| ~ spl82_111
| spl82_126 ),
inference(forward_subsumption_resolution,[],[f3126,f2839]) ).
tff(f3135,plain,
( $false
| ~ spl82_66
| ~ spl82_111
| spl82_126 ),
inference(forward_subsumption_resolution,[],[f3131,f549]) ).
tff(f3136,plain,
( ~ spl82_66
| ~ spl82_111
| spl82_126 ),
inference(avatar_contradiction_clause,[],[f3135]) ).
tff(f3147,plain,
( qmltpeq(sK18(sK27),op(e1,e1),e2)
| ~ sP9(sK27)
| ~ spl82_112 ),
inference(resolution,[],[f2018,f88]) ).
tff(f3154,plain,
( ~ sP9(sK27)
| ~ spl82_112
| spl82_127 ),
inference(forward_subsumption_resolution,[],[f3147,f2843]) ).
tff(f3157,plain,
( $false
| ~ spl82_66
| ~ spl82_112
| spl82_127 ),
inference(forward_subsumption_resolution,[],[f3154,f549]) ).
tff(f3158,plain,
( ~ spl82_66
| ~ spl82_112
| spl82_127 ),
inference(avatar_contradiction_clause,[],[f3157]) ).
cnf(s17,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_68 ),
inference(sat_conversion,[],[f557]) ).
cnf(s18,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_69 ),
inference(sat_conversion,[],[f561]) ).
cnf(s19,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_70 ),
inference(sat_conversion,[],[f565]) ).
cnf(s20,plain,
( spl82_65
| spl82_66
| spl82_67
| spl82_71 ),
inference(sat_conversion,[],[f569]) ).
cnf(s59,plain,
( ~ spl82_68
| ~ spl82_73 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s60,plain,
( ~ spl82_71
| spl82_73
| ~ spl82_99
| spl82_100
| spl82_122 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s61,plain,
( ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100
| spl82_122 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s62,plain,
( ~ spl82_67
| ~ spl82_78 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s63,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| spl82_106
| spl82_123 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s68,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| spl82_123 ),
inference(sat_conversion,[],[f2291]) ).
cnf(s69,plain,
( ~ spl82_66
| ~ spl82_83 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s70,plain,
( ~ spl82_66
| spl82_83
| ~ spl82_111
| spl82_112
| spl82_124 ),
inference(sat_conversion,[],[f2337]) ).
cnf(s75,plain,
( ~ spl82_66
| spl82_83
| ~ spl82_111
| ~ spl82_112
| spl82_124 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s76,plain,
( ~ spl82_65
| ~ spl82_88 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s77,plain,
( ~ spl82_65
| spl82_88
| ~ spl82_117
| spl82_118
| spl82_125 ),
inference(sat_conversion,[],[f2443]) ).
cnf(s82,plain,
( ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| spl82_125 ),
inference(sat_conversion,[],[f2495]) ).
cnf(s87,plain,
( ~ spl82_69
| ~ spl82_71
| spl82_73
| ~ spl82_99
| spl82_100
| ~ spl82_122 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s88,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| spl82_123 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s89,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(sat_conversion,[],[f2595]) ).
cnf(s90,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| ~ spl82_106
| ~ spl82_123 ),
inference(sat_conversion,[],[f2617]) ).
cnf(s91,plain,
( ~ spl82_67
| spl82_78
| ~ spl82_105
| spl82_106
| ~ spl82_123 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s92,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| spl82_124 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s93,plain,
( spl82_83
| spl82_111
| spl82_112
| spl82_124 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s94,plain,
( ~ spl82_65
| spl82_88
| ~ spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(sat_conversion,[],[f2747]) ).
cnf(s95,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| ~ spl82_125 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s96,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| ~ spl82_118
| spl82_125 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s97,plain,
( ~ spl82_69
| spl82_73
| spl82_99
| spl82_100 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s98,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| ~ spl82_112
| ~ spl82_124 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s99,plain,
( ~ spl82_66
| spl82_83
| ~ spl82_124
| ~ spl82_126
| ~ spl82_127 ),
inference(sat_conversion,[],[f2844]) ).
cnf(s100,plain,
( ~ spl82_66
| spl82_83
| spl82_111
| spl82_112
| ~ spl82_124 ),
inference(sat_conversion,[],[f2846]) ).
cnf(s102,plain,
( ~ spl82_66
| spl82_83
| spl82_112
| ~ spl82_124
| ~ spl82_126 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s104,plain,
( ~ spl82_67
| spl82_78
| spl82_105
| spl82_106
| ~ spl82_123 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s107,plain,
( spl82_78
| spl82_105
| spl82_106
| spl82_123 ),
inference(sat_conversion,[],[f2895]) ).
cnf(s109,plain,
( ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100
| spl82_122 ),
inference(sat_conversion,[],[f2921]) ).
cnf(s110,plain,
( ~ spl82_69
| ~ spl82_70
| spl82_73
| spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s111,plain,
( ~ spl82_69
| ~ spl82_70
| ~ spl82_71
| spl82_73
| ~ spl82_99
| ~ spl82_100
| ~ spl82_122 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s112,plain,
( spl82_88
| spl82_117
| spl82_118
| spl82_125 ),
inference(sat_conversion,[],[f3018]) ).
cnf(s114,plain,
( ~ spl82_65
| spl82_88
| spl82_117
| spl82_118
| ~ spl82_125 ),
inference(sat_conversion,[],[f3065]) ).
cnf(s116,plain,
( ~ spl82_65
| spl82_88
| spl82_118
| ~ spl82_125
| ~ spl82_130 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s117,plain,
( ~ spl82_65
| ~ spl82_117
| spl82_130 ),
inference(sat_conversion,[],[f3089]) ).
cnf(s118,plain,
( ~ spl82_66
| ~ spl82_111
| spl82_126 ),
inference(sat_conversion,[],[f3136]) ).
cnf(s119,plain,
( ~ spl82_66
| ~ spl82_112
| spl82_127 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s120,plain,
( spl82_99
| spl82_122
| spl82_73
| ~ spl82_69
| ~ spl82_70 ),
inference(rat,[],[s97,s109]) ).
cnf(s121,plain,
( spl82_122
| spl82_73
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71 ),
inference(rat,[],[s61,s60,s120]) ).
cnf(s122,plain,
( spl82_99
| ~ spl82_122
| spl82_73
| ~ spl82_69
| ~ spl82_70 ),
inference(rat,[],[s110,s97]) ).
cnf(s123,plain,
( ~ spl82_99
| spl82_73
| ~ spl82_122
| ~ spl82_69
| ~ spl82_70
| ~ spl82_71 ),
inference(rat,[],[s87,s111]) ).
cnf(s124,plain,
( spl82_73
| ~ spl82_71
| ~ spl82_69
| ~ spl82_70 ),
inference(rat,[],[s123,s122,s121]) ).
cnf(s125,plain,
( spl82_67
| spl82_66
| spl82_65 ),
inference(rat,[],[s124,s59,s18,s19,s20,s17]) ).
cnf(s127,plain,
( spl82_105
| spl82_123
| ~ spl82_67 ),
inference(rat,[],[s88,s107,s62]) ).
cnf(s128,plain,
( ~ spl82_105
| spl82_123
| ~ spl82_67
| spl82_78 ),
inference(rat,[],[s68,s63]) ).
cnf(s129,plain,
( spl82_123
| ~ spl82_67 ),
inference(rat,[],[s128,s127,s62]) ).
cnf(s130,plain,
( spl82_105
| ~ spl82_123
| ~ spl82_67
| spl82_78 ),
inference(rat,[],[s89,s104]) ).
cnf(s131,plain,
( ~ spl82_105
| ~ spl82_123
| ~ spl82_67
| spl82_78 ),
inference(rat,[],[s90,s91]) ).
cnf(s132,plain,
( ~ spl82_123
| spl82_78
| ~ spl82_67 ),
inference(rat,[],[s131,s130]) ).
cnf(s133,plain,
~ spl82_67,
inference(rat,[],[s132,s129,s62]) ).
cnf(s134,plain,
( spl82_111
| spl82_124
| ~ spl82_66
| spl82_83 ),
inference(rat,[],[s93,s92]) ).
cnf(s135,plain,
( ~ spl82_111
| spl82_124
| ~ spl82_66
| spl82_83 ),
inference(rat,[],[s70,s75]) ).
cnf(s136,plain,
( spl82_124
| spl82_83
| ~ spl82_66 ),
inference(rat,[],[s135,s134]) ).
cnf(s137,plain,
( spl82_111
| ~ spl82_124
| ~ spl82_66
| spl82_83 ),
inference(rat,[],[s100,s98]) ).
cnf(s138,plain,
( ~ spl82_126
| ~ spl82_124
| ~ spl82_66
| spl82_83 ),
inference(rat,[],[s119,s102,s99]) ).
cnf(s139,plain,
( ~ spl82_124
| spl82_83
| ~ spl82_66 ),
inference(rat,[],[s138,s118,s137]) ).
cnf(s140,plain,
( spl82_83
| ~ spl82_66 ),
inference(rat,[],[s139,s136]) ).
cnf(s141,plain,
~ spl82_66,
inference(rat,[],[s140,s69]) ).
cnf(s142,plain,
spl82_65,
inference(rat,[],[s125,s133,s141]) ).
cnf(s143,plain,
~ spl82_88,
inference(rat,[],[s76,s142]) ).
cnf(s144,plain,
( spl82_117
| spl82_125 ),
inference(rat,[],[s96,s112,s143,s142]) ).
cnf(s145,plain,
( ~ spl82_117
| spl82_125 ),
inference(rat,[],[s82,s77,s143,s142]) ).
cnf(s146,plain,
spl82_125,
inference(rat,[],[s145,s144]) ).
cnf(s151,plain,
spl82_117,
inference(rat,[],[s95,s114,s142,s143,s146]) ).
cnf(s152,plain,
spl82_130,
inference(rat,[],[s117,s142,s151]) ).
cnf(s153,plain,
~ spl82_118,
inference(rat,[],[s94,s146,s143,s142,s151]) ).
cnf(s155,plain,
$false,
inference(rat,[],[s116,s146,s143,s142,s152,s153]) ).
tff(f3159,plain,
$false,
inference(avatar_sat_refutation,[],[s155]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % 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 THM
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 17:07:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.29/1.51 % (2256708)Detected formulas, will run a generic FOF schedule.
% 2.29/1.51 % (2256713)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=775911101:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.29/1.51 % (2256719)dis-21_1_sil=8000:lcm=predicate:random_seed=3733737030:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.29/1.51 % (2256717)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3177114790:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.29/1.51 % (2256714)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3225461730:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.29/1.51 % (2256715)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3782352386:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.29/1.51 % (2256716)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2033328131:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.29/1.51 % (2256718)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4153837279:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.29/1.51 % (2256716)Refutation not found, incomplete strategy
% 2.29/1.51 % (2256716)------------------------------
% 2.29/1.51 % (2256716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256716)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256716)Termination reason: Refutation not found, incomplete strategy
% 2.29/1.51 % (2256716)Time elapsed: 0.023 s
% 2.29/1.51 % (2256716)Peak memory usage: 89 MB
% 2.29/1.51 % (2256716)Instructions burned: 49 (million)
% 2.29/1.51 % (2256717)Instruction limit reached!
% 2.29/1.51 % (2256717)------------------------------
% 2.29/1.51 % (2256717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256717)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256717)Termination reason: Instruction limit
% 2.29/1.51 % (2256717)Termination phase: Saturation
% 2.29/1.51 % (2256717)Time elapsed: 0.057 s
% 2.29/1.51 % (2256717)Peak memory usage: 89 MB
% 2.29/1.51 % (2256717)Instructions burned: 120 (million)
% 2.29/1.51 % (2256719)Instruction limit reached!
% 2.29/1.51 % (2256719)------------------------------
% 2.29/1.51 % (2256719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256719)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256719)Termination reason: Instruction limit
% 2.29/1.51 % (2256719)Termination phase: Saturation
% 2.29/1.51 % (2256719)Time elapsed: 0.070 s
% 2.29/1.51 % (2256719)Peak memory usage: 90 MB
% 2.29/1.51 % (2256719)Instructions burned: 131 (million)
% 2.29/1.51 % (2256718)Instruction limit reached!
% 2.29/1.51 % (2256718)------------------------------
% 2.29/1.51 % (2256718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256718)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256718)Termination reason: Instruction limit
% 2.29/1.51 % (2256718)Termination phase: Saturation
% 2.29/1.51 % (2256718)Time elapsed: 0.084 s
% 2.29/1.51 % (2256718)Peak memory usage: 90 MB
% 2.29/1.51 % (2256718)Instructions burned: 139 (million)
% 2.29/1.51 % (2256727)lrs+10_1_sil=8000:sp=occurrence:random_seed=1082165143:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.29/1.51 % (2256728)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3949290168:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.29/1.51 % (2256729)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3582783008:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.29/1.51 % (2256727)First to succeed.
% 2.29/1.51 % (2256727)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2256708"
% 2.29/1.51 % (2256729)Also succeeded, but the first one will report.
% 2.29/1.51 % (2256716)------------------------------
% 2.29/1.51 % (2256716)------------------------------
% 2.29/1.51 % (2256728)Instruction limit reached!
% 2.29/1.51 % (2256728)------------------------------
% 2.29/1.51 % (2256728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256728)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256728)Termination reason: Instruction limit
% 2.29/1.51 % (2256728)Termination phase: Saturation
% 2.29/1.51 % (2256728)Time elapsed: 0.079 s
% 2.29/1.51 % (2256728)Peak memory usage: 93 MB
% 2.29/1.51 % (2256728)Instructions burned: 158 (million)
% 2.29/1.51 % (2256734)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=484629971:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 2.29/1.51 % (2256733)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=628564580:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 2.29/1.51 % (2256734)Refutation not found, incomplete strategy
% 2.29/1.51 % (2256734)------------------------------
% 2.29/1.51 % (2256734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.51 % (2256734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.51 % (2256734)CaDiCaL version: 2.1.3
% 2.29/1.51 % (2256734)Termination reason: Refutation not found, incomplete strategy
% 2.29/1.51 % (2256734)Time elapsed: 0.027 s
% 2.29/1.51 % (2256734)Peak memory usage: 89 MB
% 2.29/1.51 % (2256734)Instructions burned: 58 (million)
% 2.29/1.51 % (2256713)Also succeeded, but the first one will report.
% 2.29/1.51 % (2256727)Refutation found. Thanks to Tanya!
% 2.29/1.51 % SZS status Theorem for theBenchmark
% 2.29/1.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/1.70 % (2256727)------------------------------
% 0.15/1.70 % (2256727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/1.70 % (2256727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/1.70 % (2256727)CaDiCaL version: 2.1.3
% 0.15/1.70 % (2256727)Termination reason: Refutation
% 0.15/1.70 % (2256727)Time elapsed: 0.052 s
% 0.15/1.70 % (2256727)Peak memory usage: 91 MB
% 0.15/1.70 % (2256727)Instructions burned: 97 (million)
% 0.15/1.70 % (2256727)------------------------------
% 0.15/1.70 % (2256727)------------------------------
% 0.15/1.70 % (2256708)Success in time 0.665 s
% 0.15/1.70 % Vampire exiting
%------------------------------------------------------------------------------