%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL950_17 : TPTP v9.3.1. Released v8.2.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n011.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 : Mon Sep 7 03:01:13 PM UTC 2026
% Result : Theorem 2.67s 2.91s
% Output : Proof 2.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL950_17 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 17:17:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 2.67/2.91 % SZS status Theorem
% 2.67/2.91 % SZS output start Proof
% 2.67/2.91 tff(intersect_type, type, (
% 2.67/2.91 intersect: ( |'$ki_world'| * $i * $i ) > $o)).
% 2.67/2.91 tff(tptp_fun_D_10_type, type, (
% 2.67/2.91 tptp_fun_D_10: $i)).
% 2.67/2.91 tff(tptp_fun_C_8_type, type, (
% 2.67/2.91 tptp_fun_C_8: $i)).
% 2.67/2.91 tff(tptp_fun___ki_accessible__type, type, (
% 2.67/2.91 tptp_fun___ki_accessible_: ( |'$ki_world'| * |'$ki_world'| ) > $o)).
% 2.67/2.91 tff(tptp_fun_W2_11_type, type, (
% 2.67/2.91 tptp_fun_W2_11: |'$ki_world'|)).
% 2.67/2.91 tff(member_type, type, (
% 2.67/2.91 member: ( |'$ki_world'| * $i * $i ) > $o)).
% 2.67/2.91 tff(tptp_fun_W2_4_type, type, (
% 2.67/2.91 tptp_fun_W2_4: ( $i * |'$ki_world'| * $i ) > |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun_W2_3_type, type, (
% 2.67/2.91 tptp_fun_W2_3: ( $i * |'$ki_world'| * $i ) > |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun___ki_exists_in_world__i__type, type, (
% 2.67/2.91 tptp_fun___ki_exists_in_world__i_: ( |'$ki_world'| * $i ) > $o)).
% 2.67/2.91 tff(tptp_fun_B_6_type, type, (
% 2.67/2.91 tptp_fun_B_6: $i)).
% 2.67/2.91 tff(tptp_fun_W3_12_type, type, (
% 2.67/2.91 tptp_fun_W3_12: |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun_W1_9_type, type, (
% 2.67/2.91 tptp_fun_W1_9: |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun_W0_7_type, type, (
% 2.67/2.91 tptp_fun_W0_7: |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun_W_5_type, type, (
% 2.67/2.91 tptp_fun_W_5: |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun___ki_local_world__type, type, (
% 2.67/2.91 tptp_fun___ki_local_world_: |'$ki_world'|)).
% 2.67/2.91 tff(tptp_fun_D_1_type, type, (
% 2.67/2.91 tptp_fun_D_1: ( |'$ki_world'| * $i * $i ) > $i)).
% 2.67/2.91 tff(tptp_fun_W2_2_type, type, (
% 2.67/2.91 tptp_fun_W2_2: ( |'$ki_world'| * $i * $i ) > |'$ki_world'|)).
% 2.67/2.91 tff(1,assumption,(~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)), introduced(assumption)).
% 2.67/2.91 tff(2,plain,
% 2.67/2.91 (^[W: |'$ki_world'|, X: $i] : refl(tptp_fun___ki_exists_in_world__i_(W, X) <=> tptp_fun___ki_exists_in_world__i_(W, X))),
% 2.67/2.91 inference(bind,[status(th)],[])).
% 2.67/2.91 tff(3,plain,
% 2.67/2.91 (![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X) <=> ![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)),
% 2.67/2.91 inference(quant_intro,[status(thm)],[2])).
% 2.67/2.91 tff(4,plain,
% 2.67/2.91 (![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X) <=> ![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)),
% 2.67/2.91 inference(rewrite,[status(thm)],[])).
% 2.67/2.91 tff(5,axiom,(![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''$ki_exists_in_world_$i_const'')).
% 2.67/2.91 tff(6,plain,
% 2.67/2.91 (![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)),
% 2.67/2.91 inference(modus_ponens,[status(thm)],[5, 4])).
% 2.67/2.91 tff(7,plain,(
% 2.67/2.91 ![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)),
% 2.67/2.91 inference(skolemize,[status(sab)],[6])).
% 2.67/2.91 tff(8,plain,
% 2.67/2.91 (![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)),
% 2.67/2.91 inference(modus_ponens,[status(thm)],[7, 3])).
% 2.67/2.91 tff(9,plain,
% 2.67/2.91 ((~![W: |'$ki_world'|, X: $i] : tptp_fun___ki_exists_in_world__i_(W, X)) | tptp_fun___ki_exists_in_world__i_(W2!11, B!6)),
% 2.67/2.91 inference(quant_inst,[status(thm)],[])).
% 2.67/2.91 tff(10,plain,
% 2.67/2.91 ($false),
% 2.67/2.91 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 2.67/2.91 tff(11,plain,(tptp_fun___ki_exists_in_world__i_(W2!11, B!6)), inference(lemma,lemma(discharge,[]))).
% 2.67/2.91 tff(12,assumption,(~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))), introduced(assumption)).
% 2.67/2.91 tff(13,plain,
% 2.67/2.91 (((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)) | (~member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))),
% 2.67/2.91 inference(tautology,[status(thm)],[])).
% 2.67/2.91 tff(14,plain,
% 2.67/2.91 (~member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)),
% 2.67/2.91 inference(unit_resolution,[status(thm)],[13, 12])).
% 2.67/2.91 tff(15,plain,
% 2.67/2.91 (((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)) | tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))),
% 2.67/2.91 inference(tautology,[status(thm)],[])).
% 2.67/2.91 tff(16,plain,
% 2.67/2.91 (tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))),
% 2.67/2.91 inference(unit_resolution,[status(thm)],[15, 12])).
% 2.67/2.91 tff(17,plain,
% 2.67/2.91 (^[W3: |'$ki_world'|] : refl(((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) <=> ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)))),
% 2.67/2.91 inference(bind,[status(th)],[])).
% 2.67/2.91 tff(18,plain,
% 2.67/2.91 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) <=> ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))),
% 2.67/2.91 inference(quant_intro,[status(thm)],[17])).
% 2.67/2.91 tff(19,plain,
% 2.67/2.91 ((tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.91 inference(rewrite,[status(thm)],[])).
% 2.67/2.91 tff(20,plain,
% 2.67/2.91 ((tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.91 inference(rewrite,[status(thm)],[])).
% 2.67/2.91 tff(21,plain,
% 2.67/2.91 ((tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.91 inference(rewrite,[status(thm)],[])).
% 2.67/2.91 tff(22,plain,
% 2.67/2.91 ((tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(rewrite,[status(thm)],[])).
% 2.67/2.92 tff(23,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(rewrite,[status(thm)],[])).
% 2.67/2.92 tff(24,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(rewrite,[status(thm)],[])).
% 2.67/2.92 tff(25,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))) <=> (tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(rewrite,[status(thm)],[])).
% 2.67/2.92 tff(26,plain,
% 2.67/2.92 ((![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) <=> (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)))),
% 2.67/2.92 inference(rewrite,[status(thm)],[])).
% 2.67/2.92 tff(27,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))) <=> (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[26])).
% 2.67/2.92 tff(28,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))) <=> (tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[27, 25])).
% 2.67/2.92 tff(29,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[28])).
% 2.67/2.92 tff(30,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))) <=> (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[29, 24])).
% 2.67/2.92 tff(31,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))) <=> (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[30])).
% 2.67/2.92 tff(32,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))) <=> (tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[31, 23])).
% 2.67/2.92 tff(33,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))))) <=> (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[32])).
% 2.67/2.92 tff(34,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))))) <=> (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[33, 22])).
% 2.67/2.92 tff(35,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))))) <=> (tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[34])).
% 2.67/2.92 tff(36,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))))) <=> (tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[35, 21])).
% 2.67/2.92 tff(37,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))))))) <=> (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[36])).
% 2.67/2.92 tff(38,plain,
% 2.67/2.92 ((tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))))))) <=> (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.92 inference(transitivity,[status(thm)],[37, 20])).
% 2.67/2.92 tff(39,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))))))) <=> (tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))),
% 2.67/2.92 inference(monotonicity,[status(thm)],[38])).
% 2.67/2.92 tff(40,plain,
% 2.67/2.92 ((tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & (tptp_fun___ki_exists_in_world__i_(W!5, B!6) & (tptp_fun___ki_accessible_(W!5, W0!7) & (tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & (tptp_fun___ki_accessible_(W0!7, W1!9) & (tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & (tptp_fun___ki_accessible_(W1!9, W2!11) & (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))))))))) <=> (tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))))),
% 2.67/2.93 inference(transitivity,[status(thm)],[39, 19])).
% 2.67/2.93 tff(41,plain,
% 2.67/2.93 ((~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D)))))))))) <=> (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D))))))))))),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(42,plain,
% 2.67/2.93 ((~![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => ![D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => ((![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => member(W3, B, C)) & ![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => member(W3, B, D))) => ![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => intersect(W3, C, D))))))))))) <=> (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D))))))))))),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(43,axiom,(~![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => ![D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => ((![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => member(W3, B, C)) & ![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => member(W3, B, D))) => ![W3: |'$ki_world'|] : (tptp_fun___ki_accessible_(W2, W3) => intersect(W3, C, D))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','verify')).
% 2.67/2.93 tff(44,plain,
% 2.67/2.93 (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D)))))))))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[43, 42])).
% 2.67/2.93 tff(45,plain,
% 2.67/2.93 (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D)))))))))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[44, 41])).
% 2.67/2.93 tff(46,plain,
% 2.67/2.93 (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D)))))))))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[45, 41])).
% 2.67/2.93 tff(47,plain,
% 2.67/2.93 (~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | (~(![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, C)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | member(W3, B, D)))) | ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2, W3)) | intersect(W3, C, D)))))))))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[46, 41])).
% 2.67/2.93 tff(48,plain,
% 2.67/2.93 (tptp_fun___ki_accessible_(|'$ki_local_world'|, W!5) & tptp_fun___ki_exists_in_world__i_(W!5, B!6) & tptp_fun___ki_accessible_(W!5, W0!7) & tptp_fun___ki_exists_in_world__i_(W0!7, C!8) & tptp_fun___ki_accessible_(W0!7, W1!9) & tptp_fun___ki_exists_in_world__i_(W1!9, D!10) & tptp_fun___ki_accessible_(W1!9, W2!11) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) & ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10)) & (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[47, 40])).
% 2.67/2.93 tff(49,plain,
% 2.67/2.93 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))),
% 2.67/2.93 inference(and_elim,[status(thm)],[48])).
% 2.67/2.93 tff(50,plain,
% 2.67/2.93 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[49, 18])).
% 2.67/2.93 tff(51,plain,
% 2.67/2.93 (((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) | ((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))) <=> ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) | (~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(52,plain,
% 2.67/2.93 ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) | ((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))),
% 2.67/2.93 inference(quant_inst,[status(thm)],[])).
% 2.67/2.93 tff(53,plain,
% 2.67/2.93 ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, D!10))) | (~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[52, 51])).
% 2.67/2.93 tff(54,plain,
% 2.67/2.93 ($false),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[53, 50, 16, 14])).
% 2.67/2.93 tff(55,plain,((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)), inference(lemma,lemma(discharge,[]))).
% 2.67/2.93 tff(56,assumption,(~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))), introduced(assumption)).
% 2.67/2.93 tff(57,plain,
% 2.67/2.93 (^[W: |'$ki_world'|, V: |'$ki_world'|] : refl(tptp_fun___ki_accessible_(W, V) <=> tptp_fun___ki_accessible_(W, V))),
% 2.67/2.93 inference(bind,[status(th)],[])).
% 2.67/2.93 tff(58,plain,
% 2.67/2.93 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V) <=> ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 2.67/2.93 inference(quant_intro,[status(thm)],[57])).
% 2.67/2.93 tff(59,plain,
% 2.67/2.93 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V) <=> ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(60,axiom,(![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mrel_universal')).
% 2.67/2.93 tff(61,plain,
% 2.67/2.93 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[60, 59])).
% 2.67/2.93 tff(62,plain,(
% 2.67/2.93 ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 2.67/2.93 inference(skolemize,[status(sab)],[61])).
% 2.67/2.93 tff(63,plain,
% 2.67/2.93 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[62, 58])).
% 2.67/2.93 tff(64,plain,
% 2.67/2.93 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))),
% 2.67/2.93 inference(quant_inst,[status(thm)],[])).
% 2.67/2.93 tff(65,plain,
% 2.67/2.93 ($false),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[64, 63, 56])).
% 2.67/2.93 tff(66,plain,(tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))), inference(lemma,lemma(discharge,[]))).
% 2.67/2.93 tff(67,assumption,(~member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)), introduced(assumption)).
% 2.67/2.93 tff(68,assumption,(tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))), introduced(assumption)).
% 2.67/2.93 tff(69,plain,
% 2.67/2.93 (^[W3: |'$ki_world'|] : refl(((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) <=> ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)))),
% 2.67/2.93 inference(bind,[status(th)],[])).
% 2.67/2.93 tff(70,plain,
% 2.67/2.93 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8)) <=> ![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))),
% 2.67/2.93 inference(quant_intro,[status(thm)],[69])).
% 2.67/2.93 tff(71,plain,
% 2.67/2.93 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))),
% 2.67/2.93 inference(and_elim,[status(thm)],[48])).
% 2.67/2.93 tff(72,plain,
% 2.67/2.93 (![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[71, 70])).
% 2.67/2.93 tff(73,plain,
% 2.67/2.93 (((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))) | ((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))) <=> ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))) | (~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(74,plain,
% 2.67/2.93 ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))) | ((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))),
% 2.67/2.93 inference(quant_inst,[status(thm)],[])).
% 2.67/2.93 tff(75,plain,
% 2.67/2.93 ((~![W3: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W3)) | member(W3, B!6, C!8))) | (~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[74, 73])).
% 2.67/2.93 tff(76,plain,
% 2.67/2.93 ($false),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[75, 72, 68, 67])).
% 2.67/2.93 tff(77,plain,((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)), inference(lemma,lemma(discharge,[]))).
% 2.67/2.93 tff(78,plain,
% 2.67/2.93 (member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[77, 66])).
% 2.67/2.93 tff(79,plain,
% 2.67/2.93 (((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)) | (~member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))),
% 2.67/2.93 inference(tautology,[status(thm)],[])).
% 2.67/2.93 tff(80,plain,
% 2.67/2.93 ((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8)),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[79, 78])).
% 2.67/2.93 tff(81,plain,
% 2.67/2.93 (((~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))) | ((~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))))) <=> ((~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))) | (~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))))),
% 2.67/2.93 inference(rewrite,[status(thm)],[])).
% 2.67/2.93 tff(82,plain,
% 2.67/2.93 ((~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))) | ((~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10))))),
% 2.67/2.93 inference(quant_inst,[status(thm)],[])).
% 2.67/2.93 tff(83,plain,
% 2.67/2.93 ((~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))) | (~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(B!6, W2!11, C!8))) | member(tptp_fun_W2_3(B!6, W2!11, C!8), B!6, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)))),
% 2.67/2.93 inference(modus_ponens,[status(thm)],[82, 81])).
% 2.67/2.93 tff(84,plain,
% 2.67/2.93 ((~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))) | (~tptp_fun___ki_exists_in_world__i_(W2!11, B!6)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(B!6, W2!11, D!10))) | member(tptp_fun_W2_4(B!6, W2!11, D!10), B!6, D!10)))),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[83, 80])).
% 2.67/2.93 tff(85,plain,
% 2.67/2.93 (~![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10))))),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[84, 55, 11])).
% 2.67/2.93 tff(86,assumption,(~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)), introduced(assumption)).
% 2.67/2.93 tff(87,plain,
% 2.67/2.93 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)),
% 2.67/2.93 inference(quant_inst,[status(thm)],[])).
% 2.67/2.93 tff(88,plain,
% 2.67/2.93 ($false),
% 2.67/2.93 inference(unit_resolution,[status(thm)],[87, 63, 86])).
% 2.67/2.93 tff(89,plain,(tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)), inference(lemma,lemma(discharge,[]))).
% 2.67/2.93 tff(90,plain,
% 2.67/2.93 (^[W: |'$ki_world'|] : rewrite(((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))))),
% 2.67/2.93 inference(bind,[status(th)],[])).
% 2.67/2.94 tff(91,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.94 inference(quant_intro,[status(thm)],[90])).
% 2.67/2.94 tff(92,plain,
% 2.67/2.94 (^[W: |'$ki_world'|] : refl(((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))))),
% 2.67/2.94 inference(bind,[status(th)],[])).
% 2.67/2.94 tff(93,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.94 inference(quant_intro,[status(thm)],[92])).
% 2.67/2.94 tff(94,plain,
% 2.67/2.94 (^[W: |'$ki_world'|] : rewrite(((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))))),
% 2.67/2.94 inference(bind,[status(th)],[])).
% 2.67/2.94 tff(95,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.94 inference(quant_intro,[status(thm)],[94])).
% 2.67/2.94 tff(96,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.94 inference(transitivity,[status(thm)],[95, 93])).
% 2.67/2.94 tff(97,plain,
% 2.67/2.94 (^[W: |'$ki_world'|] : rewrite(((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))))),
% 2.67/2.94 inference(bind,[status(th)],[])).
% 2.67/2.94 tff(98,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.94 inference(quant_intro,[status(thm)],[97])).
% 2.67/2.94 tff(99,plain,
% 2.67/2.94 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))),
% 2.67/2.94 inference(rewrite,[status(thm)],[])).
% 2.67/2.94 tff(100,plain,
% 2.67/2.94 (^[W: |'$ki_world'|] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[W0: |'$ki_world'|] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite((![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))) <=> (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))), ((tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))) <=> (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))), rewrite((tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))) <=> ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))), ((tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))) <=> ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))), (![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))) <=> ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))), ((tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))) <=> (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))), rewrite((tptp_fun___ki_accessible_(W, W0) => ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))) <=> ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))), ((tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))) <=> ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))), (![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))) <=> ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))), ((tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))))) <=> (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))), rewrite((tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))) <=> ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))), ((tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))))) <=> ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))))), (![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))))) <=> ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))), ((tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))))) <=> (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))))), rewrite((tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C)))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))), ((tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))))) <=> ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))))),
% 2.67/2.95 inference(bind,[status(th)],[])).
% 2.67/2.95 tff(101,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C))))))))) <=> ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))),
% 2.67/2.95 inference(quant_intro,[status(thm)],[100])).
% 2.67/2.95 tff(102,axiom,(![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => ![B: $i] : (tptp_fun___ki_exists_in_world__i_(W, B) => ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => ![C: $i] : (tptp_fun___ki_exists_in_world__i_(W0, C) => (![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)) => ?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))))) & ![W1: |'$ki_world'|] : (tptp_fun___ki_accessible_(W0, W1) => (?[D: $i] : ((tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, B))) & ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => member(W2, D, C))) => ![W2: |'$ki_world'|] : (tptp_fun___ki_accessible_(W1, W2) => intersect(W2, B, C)))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersect_defn')).
% 2.67/2.95 tff(103,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))),
% 2.67/2.95 inference(modus_ponens,[status(thm)],[102, 101])).
% 2.67/2.95 tff(104,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | (~?[D: $i] : (tptp_fun___ki_exists_in_world__i_(W1, D) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, D, C))))))))))),
% 2.67/2.95 inference(modus_ponens,[status(thm)],[103, 99])).
% 2.67/2.95 tff(105,plain,(
% 2.67/2.95 ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B)) & ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C)))) & ![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))),
% 2.67/2.95 inference(skolemize,[status(sab)],[104])).
% 2.67/2.95 tff(106,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.95 inference(modus_ponens,[status(thm)],[105, 98])).
% 2.67/2.95 tff(107,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | (~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.95 inference(modus_ponens,[status(thm)],[106, 96])).
% 2.67/2.95 tff(108,plain,
% 2.67/2.95 (![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.95 inference(modus_ponens,[status(thm)],[107, 91])).
% 2.67/2.95 tff(109,plain,
% 2.67/2.95 (((~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))) | ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))) <=> ((~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))) | (~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.95 inference(rewrite,[status(thm)],[])).
% 2.67/2.95 tff(110,plain,
% 2.67/2.95 ((~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))) | ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))),
% 2.67/2.96 inference(quant_inst,[status(thm)],[])).
% 2.67/2.96 tff(111,plain,
% 2.67/2.96 ((~![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))))) | (~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))),
% 2.67/2.96 inference(modus_ponens,[status(thm)],[110, 109])).
% 2.67/2.96 tff(112,plain,
% 2.67/2.96 ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W0!7)) | ![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))),
% 2.67/2.96 inference(unit_resolution,[status(thm)],[111, 108])).
% 2.67/2.96 tff(113,plain,
% 2.67/2.96 (![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))),
% 2.67/2.96 inference(unit_resolution,[status(thm)],[112, 89])).
% 2.67/2.96 tff(114,plain,
% 2.67/2.96 (tptp_fun___ki_exists_in_world__i_(W0!7, C!8)),
% 2.67/2.96 inference(and_elim,[status(thm)],[48])).
% 2.67/2.96 tff(115,plain,
% 2.67/2.96 (((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))))) <=> ((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | (~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))))),
% 2.67/2.96 inference(rewrite,[status(thm)],[])).
% 2.67/2.96 tff(116,plain,
% 2.67/2.96 (((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C))))))))))) <=> ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))))),
% 2.67/2.96 inference(rewrite,[status(thm)],[])).
% 2.67/2.96 tff(117,plain,
% 2.67/2.96 (((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))))),
% 2.67/2.96 inference(monotonicity,[status(thm)],[116])).
% 2.67/2.96 tff(118,plain,
% 2.67/2.96 (((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) <=> ((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | (~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))))),
% 2.67/2.96 inference(transitivity,[status(thm)],[117, 115])).
% 2.67/2.96 tff(119,plain,
% 2.67/2.96 ((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | ((~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))),
% 2.67/2.96 inference(quant_inst,[status(thm)],[])).
% 2.67/2.96 tff(120,plain,
% 2.67/2.96 ((~![B: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0!7, B)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, B))) | intersect(tptp_fun_W2_2(W1, C, B), B, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), B))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, B), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, B, C)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, B))) | member(tptp_fun_W2_3(D, W1, B), D, B))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))))))))))) | (~tptp_fun___ki_exists_in_world__i_(W0!7, C!8)) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))),
% 2.67/2.97 inference(modus_ponens,[status(thm)],[119, 118])).
% 2.67/2.97 tff(121,plain,
% 2.67/2.97 (![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))),
% 2.67/2.97 inference(unit_resolution,[status(thm)],[120, 114, 113])).
% 2.67/2.97 tff(122,plain,
% 2.67/2.97 (tptp_fun___ki_accessible_(W0!7, W1!9)),
% 2.67/2.97 inference(and_elim,[status(thm)],[48])).
% 2.67/2.97 tff(123,plain,
% 2.67/2.97 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))) | ((~tptp_fun___ki_accessible_(W0!7, W1!9)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))) <=> ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))) | (~tptp_fun___ki_accessible_(W0!7, W1!9)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))),
% 2.67/2.97 inference(rewrite,[status(thm)],[])).
% 2.67/2.97 tff(124,plain,
% 2.67/2.97 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))) | ((~tptp_fun___ki_accessible_(W0!7, W1!9)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))),
% 2.67/2.97 inference(quant_inst,[status(thm)],[])).
% 2.67/2.97 tff(125,plain,
% 2.67/2.97 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0!7, W0)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W0, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W0, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C))))))))) | (~tptp_fun___ki_accessible_(W0!7, W1!9)) | ![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))),
% 2.67/2.97 inference(modus_ponens,[status(thm)],[124, 123])).
% 2.67/2.97 tff(126,plain,
% 2.67/2.97 (![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))),
% 2.67/2.97 inference(unit_resolution,[status(thm)],[125, 122, 121])).
% 2.67/2.97 tff(127,plain,
% 2.67/2.97 (tptp_fun___ki_exists_in_world__i_(W1!9, D!10)),
% 2.67/2.97 inference(and_elim,[status(thm)],[48])).
% 2.67/2.97 tff(128,plain,
% 2.67/2.97 (((~![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))) | ((~tptp_fun___ki_exists_in_world__i_(W1!9, D!10)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))))))) <=> ((~![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))) | (~tptp_fun___ki_exists_in_world__i_(W1!9, D!10)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))))))),
% 2.67/2.97 inference(rewrite,[status(thm)],[])).
% 2.67/2.97 tff(129,plain,
% 2.67/2.97 ((~![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))) | ((~tptp_fun___ki_exists_in_world__i_(W1!9, D!10)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))))))),
% 2.67/2.97 inference(quant_inst,[status(thm)],[])).
% 2.67/2.97 tff(130,plain,
% 2.67/2.97 ((~![C: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1!9, C)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, C, C!8))) | intersect(tptp_fun_W2_2(W1, C, C!8), C!8, C))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, C, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, C, C!8), C))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, C))) | member(tptp_fun_W2_4(D, W1, C), D, C)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, C)))))))) | (~tptp_fun___ki_exists_in_world__i_(W1!9, D!10)) | (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10))))))),
% 2.67/2.97 inference(modus_ponens,[status(thm)],[129, 128])).
% 2.67/2.97 tff(131,plain,
% 2.67/2.97 (~((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))))),
% 2.67/2.98 inference(unit_resolution,[status(thm)],[130, 127, 126])).
% 2.67/2.98 tff(132,plain,
% 2.67/2.98 (((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_2(W1, D!10, C!8))) | intersect(tptp_fun_W2_2(W1, D!10, C!8), C!8, D!10))) | (~((~tptp_fun___ki_exists_in_world__i_(W1, tptp_fun_D_1(W1, D!10, C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), C!8))) | (~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | member(W2, tptp_fun_D_1(W1, D!10, C!8), D!10))))))) | (~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10))))) | ![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))),
% 2.67/2.98 inference(tautology,[status(thm)],[])).
% 2.67/2.98 tff(133,plain,
% 2.67/2.98 (![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))),
% 2.67/2.98 inference(unit_resolution,[status(thm)],[132, 131])).
% 2.67/2.98 tff(134,plain,
% 2.67/2.98 (tptp_fun___ki_accessible_(W1!9, W2!11)),
% 2.67/2.98 inference(and_elim,[status(thm)],[48])).
% 2.67/2.98 tff(135,plain,
% 2.67/2.98 (((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))) | ((~tptp_fun___ki_accessible_(W1!9, W2!11)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10)))) <=> ((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))) | (~tptp_fun___ki_accessible_(W1!9, W2!11)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10)))),
% 2.67/2.98 inference(rewrite,[status(thm)],[])).
% 2.67/2.98 tff(136,plain,
% 2.67/2.98 ((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))) | ((~tptp_fun___ki_accessible_(W1!9, W2!11)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10)))),
% 2.67/2.98 inference(quant_inst,[status(thm)],[])).
% 2.67/2.98 tff(137,plain,
% 2.67/2.98 ((~![W1: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1!9, W1)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W1, D)) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_3(D, W1, C!8))) | member(tptp_fun_W2_3(D, W1, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W1, tptp_fun_W2_4(D, W1, D!10))) | member(tptp_fun_W2_4(D, W1, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W1, W2)) | intersect(W2, C!8, D!10)))) | (~tptp_fun___ki_accessible_(W1!9, W2!11)) | ![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))),
% 2.67/2.98 inference(modus_ponens,[status(thm)],[136, 135])).
% 2.67/2.98 tff(138,plain,
% 2.67/2.98 (![D: $i] : ((~tptp_fun___ki_exists_in_world__i_(W2!11, D)) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_3(D, W2!11, C!8))) | member(tptp_fun_W2_3(D, W2!11, C!8), D, C!8))) | (~((~tptp_fun___ki_accessible_(W2!11, tptp_fun_W2_4(D, W2!11, D!10))) | member(tptp_fun_W2_4(D, W2!11, D!10), D, D!10)))) | ![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))),
% 2.67/2.98 inference(unit_resolution,[status(thm)],[137, 134, 133])).
% 2.67/2.98 tff(139,plain,
% 2.67/2.98 (![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))),
% 2.67/2.98 inference(unit_resolution,[status(thm)],[138, 85])).
% 2.67/2.98 tff(140,plain,
% 2.67/2.98 (~((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))),
% 2.67/2.98 inference(and_elim,[status(thm)],[48])).
% 2.67/2.98 tff(141,plain,
% 2.67/2.98 (~intersect(W3!12, C!8, D!10)),
% 2.67/2.98 inference(or_elim,[status(thm)],[140])).
% 2.67/2.98 tff(142,plain,
% 2.67/2.98 (tptp_fun___ki_accessible_(W2!11, W3!12)),
% 2.67/2.98 inference(or_elim,[status(thm)],[140])).
% 2.67/2.98 tff(143,plain,
% 2.67/2.98 (((~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))) | ((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))) <=> ((~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))) | (~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))),
% 2.67/2.98 inference(rewrite,[status(thm)],[])).
% 2.67/2.98 tff(144,plain,
% 2.67/2.98 ((~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))) | ((~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10))),
% 2.67/2.98 inference(quant_inst,[status(thm)],[])).
% 2.67/2.98 tff(145,plain,
% 2.67/2.98 ((~![W2: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W2!11, W2)) | intersect(W2, C!8, D!10))) | (~tptp_fun___ki_accessible_(W2!11, W3!12)) | intersect(W3!12, C!8, D!10)),
% 2.67/2.98 inference(modus_ponens,[status(thm)],[144, 143])).
% 2.67/2.98 tff(146,plain,
% 2.67/2.98 ($false),
% 2.67/2.98 inference(unit_resolution,[status(thm)],[145, 142, 141, 139])).
% 2.67/2.98 % SZS output end Proof
% 2.67/2.99 % E exiting
%------------------------------------------------------------------------------