%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYP033_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n015.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 : Sun Sep 27 09:51:45 AM UTC 2026
% Result : Theorem 102.67s 24.11s
% Output : Refutation 100.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 70
% Syntax : Number of formulae : 243 ( 77 unt; 0 typ; 68 def)
% Number of atoms : 5058 ( 243 equ; 0 cnn)
% Maximal formula atoms : 2078 ( 20 avg)
% Number of connectives : 12303 (1327 ~;3350 |; 253 &;6385 @)
% ( 0 <=>; 988 =>; 0 <=; 0 <~>)
% Maximal formula depth : 271 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 83 ( 80 usr; 39 con; 0-4 aty)
% Number of variables : 986 ( 48 ^; 795 !; 75 ?; 986 :)
% ( 0 !>; 0 ?*; 0 @-; 68 @+)
% Comments :
%------------------------------------------------------------------------------
thf('$world_type',type,
'$world': $tType ).
thf('$local_world_decl',type,
'$local_world': '$world' ).
thf('$accessible_world_decl',type,
'$accessible_world': '$world' > '$world' > $o ).
thf(p1_decl,type,
p1: '$world' > $o ).
thf(p2_decl,type,
p2: '$world' > $o ).
thf(p3_decl,type,
p3: '$world' > $o ).
thf(p4_decl,type,
p4: '$world' > $o ).
thf(sk1_decl,type,
sk1: '$world' > '$world' ).
thf(sk2_decl,type,
sk2: '$world' ).
thf(sk3_decl,type,
sk3: '$world' > '$world' ).
thf(sk4_decl,type,
sk4: '$world' ).
thf(sk5_decl,type,
sk5: '$world' ).
thf(sk6_decl,type,
sk6: '$world' > '$world' ).
thf(sk7_decl,type,
sk7: '$world' ).
thf(sk8_decl,type,
sk8: '$world' ).
thf(sk9_decl,type,
sk9: '$world' > '$world' ).
thf(sk10_decl,type,
sk10: '$world' ).
thf(sk11_decl,type,
sk11: '$world' ).
thf(sk12_decl,type,
sk12: '$world' > '$world' ).
thf(sk13_decl,type,
sk13: '$world' ).
thf(sk14_decl,type,
sk14: '$world' ).
thf(sk15_decl,type,
sk15: '$world' > '$world' ).
thf(sk16_decl,type,
sk16: '$world' > '$world' ).
thf(sk17_decl,type,
sk17: '$world' ).
thf(sk18_decl,type,
sk18: '$world' ).
thf(sk19_decl,type,
sk19: '$world' ).
thf(sk20_decl,type,
sk20: '$world' > '$world' ).
thf(sk21_decl,type,
sk21: '$world' > '$world' ).
thf(sk22_decl,type,
sk22: '$world' ).
thf(sk23_decl,type,
sk23: '$world' ).
thf(sk24_decl,type,
sk24: '$world' ).
thf(sk25_decl,type,
sk25: '$world' > '$world' ).
thf(sk26_decl,type,
sk26: '$world' > '$world' ).
thf(sk27_decl,type,
sk27: '$world' ).
thf(sk28_decl,type,
sk28: '$world' ).
thf(sk29_decl,type,
sk29: '$world' ).
thf(sk30_decl,type,
sk30: '$world' > '$world' ).
thf(sk31_decl,type,
sk31: '$world' > '$world' ).
thf(sk32_decl,type,
sk32: '$world' ).
thf(sk33_decl,type,
sk33: '$world' ).
thf(sk34_decl,type,
sk34: '$world' ).
thf(sk35_decl,type,
sk35: '$world' > '$world' ).
thf(sk36_decl,type,
sk36: '$world' > '$world' ).
thf(sk37_decl,type,
sk37: '$world' > '$world' ).
thf(sk38_decl,type,
sk38: '$world' ).
thf(sk39_decl,type,
sk39: '$world' ).
thf(sk40_decl,type,
sk40: '$world' ).
thf(sk41_decl,type,
sk41: $o ).
thf(sk42_decl,type,
sk42: '$world' ).
thf(sk43_decl,type,
sk43: '$world' > $o ).
thf(sk44_decl,type,
sk44: '$world' > $o ).
thf(sk45_decl,type,
sk45: '$world' > '$world' > '$world' ).
thf(sk46_decl,type,
sk46: '$world' > '$world' > '$world' ).
thf(sk47_decl,type,
sk47: '$world' > '$world' ).
thf(sk48_decl,type,
sk48: '$world' > '$world' ).
thf(sk49_decl,type,
sk49: '$world' > '$world' > '$world' ).
thf(sk50_decl,type,
sk50: '$world' > '$world' > '$world' ).
thf(sk51_decl,type,
sk51: '$world' > $o ).
thf(sk52_decl,type,
sk52: '$world' > '$world' > '$world' ).
thf(sk53_decl,type,
sk53: '$world' > '$world' > '$world' > '$world' > '$world' ).
thf(sk54_decl,type,
sk54: '$world' > '$world' > '$world' > '$world' > '$world' ).
thf(sk55_decl,type,
sk55: $o ).
thf(sk56_decl,type,
sk56: '$world' > '$world' ).
thf(sk57_decl,type,
sk57: '$world' > '$world' ).
thf(sk58_decl,type,
sk58: '$world' ).
thf(sk59_decl,type,
sk59: '$world' ).
thf(sk60_decl,type,
sk60: '$world' ).
thf(sk61_decl,type,
sk61: '$world' ).
thf(sk62_decl,type,
sk62: $o ).
thf(sk63_decl,type,
sk63: '$world' ).
thf(sk64_decl,type,
sk64: '$world' > '$world' > '$world' ).
thf(sk65_decl,type,
sk65: '$world' > '$world' > '$world' ).
thf(sk66_decl,type,
sk66: '$world' > '$world' ).
thf(sk67_decl,type,
sk67: '$world' > '$world' ).
thf(sk68_decl,type,
sk68: '$world' ).
thf(sk69_decl,type,
sk69: '$world' > '$world' ).
thf(sk70_decl,type,
sk70: '$world' > '$world' ).
thf(sk71_decl,type,
sk71: '$world' ).
thf(sk72_decl,type,
sk72: '$world' > '$world' ).
thf(sk73_decl,type,
sk73: '$world' > '$world' ).
thf(sk74_decl,type,
sk74: '$world' ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: '$world'] : ( A @ ( sk2 @ '$accessible_world' ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: '$world'] : ( A @ ( sk5 @ '$accessible_world' ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: '$world'] : ( A @ ( sk8 @ '$accessible_world' ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: '$world'] : ( A @ ( sk11 @ '$accessible_world' ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ sk15 @ '$accessible_world' ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: '$world'] :
~ ( ( A @ ( sk14 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: '$world'] : ( A @ ( sk17 @ '$accessible_world' ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ sk20 @ '$accessible_world' ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( @+[A: '$world'] :
~ ( ( A @ ( sk19 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk23_def,definition,
( sk23
= ( @+[A: '$world'] : ( A @ ( sk22 @ '$accessible_world' ) ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) ) ) ).
thf(sk25_def,definition,
( sk25
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk26_def,definition,
( sk26
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ sk25 @ '$accessible_world' ) ) ) ) ).
thf(sk27_def,definition,
( sk27
= ( @+[A: '$world'] :
~ ( ( A @ ( sk24 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk28_def,definition,
( sk28
= ( @+[A: '$world'] : ( A @ ( sk27 @ '$accessible_world' ) ) ) ) ).
thf(sk29_def,definition,
( sk29
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) ) ) ).
thf(sk30_def,definition,
( sk30
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk31_def,definition,
( sk31
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ sk30 @ '$accessible_world' ) ) ) ) ).
thf(sk32_def,definition,
( sk32
= ( @+[A: '$world'] :
~ ( ( A @ ( sk29 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk33_def,definition,
( sk33
= ( @+[A: '$world'] : ( A @ ( sk32 @ '$accessible_world' ) ) ) ) ).
thf(sk34_def,definition,
( sk34
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ~ ? [F: '$world'] : ( F @ ( E @ '$accessible_world' ) ) ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) ) ) ) ) ) ) ).
thf(sk35_def,definition,
( sk35
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) ) ) ) ).
thf(sk36_def,definition,
( sk36
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk35 @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk37_def,definition,
( sk37
= ( ^ [A: '$world'] :
@+[B: '$world'] : ( B @ ( A @ sk36 @ '$accessible_world' ) ) ) ) ).
thf(sk38_def,definition,
( sk38
= ( @+[A: '$world'] :
~ ( ( A @ ( sk34 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: '$world'] :
~ ( ( A @ ( sk38 @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) ) ).
thf(sk40_def,definition,
( sk40
= ( @+[A: '$world'] : ( A @ ( sk39 @ '$accessible_world' ) ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) ) ) )
& ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( ( F @ p2 )
=> ! [G: '$world'] :
( ( G @ ( F @ '$accessible_world' ) )
=> ( G @ p2 ) ) ) )
=> ( E @ p2 ) ) ) ) )
& ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) )
& ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) ) ) ) ).
thf(sk45_def,definition,
( sk45
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( A @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) ) ) ) ).
thf(sk46_def,definition,
( sk46
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( B @ ( A @ sk45 ) @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) ).
thf(sk47_def,definition,
( sk47
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) ) ).
thf(sk48_def,definition,
( sk48
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk47 @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) ) ).
thf(sk49_def,definition,
( sk49
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( A @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) ) ) ) ).
thf(sk50_def,definition,
( sk50
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( B @ ( A @ sk49 ) @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) ).
thf(sk52_def,definition,
( sk52
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( A @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) ).
thf(sk53_def,definition,
( sk53
= ( ^ [A: '$world',B: '$world',C: '$world',D: '$world'] :
@+[E: '$world'] :
~ ( ( E @ ( A @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) ) ) ) ).
thf(sk54_def,definition,
( sk54
= ( ^ [A: '$world',B: '$world',C: '$world',D: '$world'] :
@+[E: '$world'] :
~ ( ( E @ ( D @ ( C @ ( B @ ( A @ sk53 ) ) ) @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) ) ).
thf(sk56_def,definition,
( sk56
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) ) ) ).
thf(sk57_def,definition,
( sk57
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk56 @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ).
thf(sk58_def,definition,
( sk58
= ( @+[A: '$world'] :
~ ( ( A @ ( sk42 @ '$accessible_world' ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) ) ) ).
thf(sk59_def,definition,
( sk59
= ( @+[A: '$world'] :
~ ( ( A @ ( sk58 @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) ) ).
thf(sk60_def,definition,
( sk60
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p2 )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ) ) ).
thf(sk61_def,definition,
( sk61
= ( @+[A: '$world'] :
~ ( ( A @ ( sk60 @ '$accessible_world' ) )
=> ( A @ p2 ) ) ) ) ).
thf(sk63_def,definition,
( sk63
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) ) ).
thf(sk64_def,definition,
( sk64
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( A @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) ) ) ) ).
thf(sk65_def,definition,
( sk65
= ( ^ [A: '$world',B: '$world'] :
@+[C: '$world'] :
~ ( ( C @ ( B @ ( A @ sk64 ) @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) ).
thf(sk66_def,definition,
( sk66
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p1 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) ) ) ) ) ) ).
thf(sk67_def,definition,
( sk67
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk66 @ '$accessible_world' ) )
=> ( B @ p1 ) ) ) ) ).
thf(sk68_def,definition,
( sk68
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p1 ) ) ) ) ).
thf(sk69_def,definition,
( sk69
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) ) ) ).
thf(sk70_def,definition,
( sk70
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk69 @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ).
thf(sk71_def,definition,
( sk71
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p2 ) ) ) ) ).
thf(sk72_def,definition,
( sk72
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p3 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) ) ) ) ).
thf(sk73_def,definition,
( sk73
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ sk72 @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) ).
thf(sk74_def,definition,
( sk74
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p3 ) ) ) ) ).
thf(1,conjecture,
( ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) ) ) )
& ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( ( F @ p2 )
=> ! [G: '$world'] :
( ( G @ ( F @ '$accessible_world' ) )
=> ( G @ p2 ) ) ) )
=> ( E @ p2 ) ) ) ) )
& ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) )
& ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p2 )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
=> ( '$local_world' @ p2 ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ( A @ p2 ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p3 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) )
=> ( A @ p3 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p3 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p2 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p1 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) ) ) )
=> ( A @ p1 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p1 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',10) ).
thf(2,negated_conjecture,
~ ( ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) ) ) )
& ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( ( F @ p2 )
=> ! [G: '$world'] :
( ( G @ ( F @ '$accessible_world' ) )
=> ( G @ p2 ) ) ) )
=> ( E @ p2 ) ) ) ) )
& ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) )
& ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p2 )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
=> ( '$local_world' @ p2 ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> $false ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> $false ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> $false ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> $false ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> $false ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ( A @ p2 ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p3 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) )
=> ( A @ p3 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p3 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p2 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p1 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) ) ) )
=> ( A @ p1 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p1 ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(4,plain,
~ ( ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) ) ) )
& ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( ( F @ p2 )
=> ! [G: '$world'] :
( ( G @ ( F @ '$accessible_world' ) )
=> ( G @ p2 ) ) ) )
=> ( E @ p2 ) ) ) ) )
& ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) )
& ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p2 )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
=> ( '$local_world' @ p2 ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
~ ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ! [F: '$world'] :
~ ( F @ ( E @ '$accessible_world' ) ) ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
~ ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
~ ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
~ ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
~ ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
~ ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
~ ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
~ ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ( A @ p2 ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p3 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) )
=> ( A @ p3 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p3 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p2 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p1 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) ) ) )
=> ( A @ p1 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p1 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(5,plain,
~ ( ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) ) ) )
& ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p2 )
=> ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( F @ p2 ) ) ) )
=> ( D @ p2 ) ) )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ! [F: '$world'] :
( ( F @ ( E @ '$accessible_world' ) )
=> ( ( F @ p2 )
=> ! [G: '$world'] :
( ( G @ ( F @ '$accessible_world' ) )
=> ( G @ p2 ) ) ) )
=> ( E @ p2 ) ) ) ) )
& ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p2 )
=> ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( E @ p2 ) ) ) )
=> ( C @ p2 ) ) ) ) )
& ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p2 )
=> ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
=> ( '$local_world' @ p2 ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ! [E: '$world'] :
( ( E @ ( D @ '$accessible_world' ) )
=> ( ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ~ ? [F: '$world'] : ( F @ ( E @ '$accessible_world' ) ) ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( ( D @ p4 )
| ( D @ p3 )
| ( D @ p2 )
| ( D @ p1 )
| ~ ? [E: '$world'] : ( E @ ( D @ '$accessible_world' ) ) ) ) ) ) ) )
=> ( ( A @ p1 )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ? [A: '$world'] : ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ? [A: '$world'] : ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
| ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
| ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p2 )
| ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ? [A: '$world'] : ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
| ~ ? [C: '$world'] : ( C @ ( B @ '$accessible_world' ) ) )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p1 )
| ~ ? [D: '$world'] : ( D @ ( C @ '$accessible_world' ) ) ) ) ) )
=> ( ( A @ p1 )
| ~ ? [B: '$world'] : ( B @ ( A @ '$accessible_world' ) ) ) ) )
=> ( ( '$local_world' @ p1 )
| ~ ? [A: '$world'] : ( A @ ( '$local_world' @ '$accessible_world' ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( ( C @ p2 )
=> ! [D: '$world'] :
( ( D @ ( C @ '$accessible_world' ) )
=> ( D @ p2 ) ) ) )
=> ( B @ p2 ) ) )
=> ( A @ p2 ) ) ) )
=> ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p3 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) )
=> ( A @ p3 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p3 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p2 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) )
=> ( A @ p2 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p2 ) ) )
| ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( B @ p1 )
=> ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) ) ) )
=> ( A @ p1 ) ) )
=> ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( A @ p1 ) ) ) ) ),
inference(miniscope,[status(thm)],[4]) ).
thf(6,plain,
! [ZZV: '$world',ZZU: '$world',ZZT: '$world',ZZS: '$world',ZZR: '$world',ZZQ: '$world',ZZP: '$world',ZZO: '$world',ZZN: '$world',ZZM: '$world',ZZL: '$world',ZZK: '$world',ZZJ: '$world',ZZI: '$world',ZZH: '$world',ZZG: '$world',ZZF: '$world',ZZE: '$world',ZZD: '$world',ZZC: '$world',ZZB: '$world',ZZA: '$world',ZZ: '$world',ZY: '$world',ZX: '$world',ZW: '$world',ZV: '$world',ZU: '$world',ZT: '$world',ZS: '$world',ZR: '$world',ZQ: '$world',ZP: '$world',ZO: '$world',ZN: '$world',ZM: '$world',ZL: '$world',ZK: '$world',ZJ: '$world',ZI: '$world',ZH: '$world',ZG: '$world',ZF: '$world',ZE: '$world',ZD: '$world',ZC: '$world',ZB: '$world',ZA: '$world',Z: '$world',Y: '$world',X: '$world',W: '$world',V: '$world',U: '$world',T: '$world',S: '$world',R: '$world',Q: '$world',P: '$world',O: '$world',N: '$world',M: '$world',L: '$world',K: '$world',J: '$world',I: '$world',H: '$world',G: '$world',F: '$world',E: '$world',D: '$world',C: '$world',B: '$world',A: '$world'] :
( ~ ( sk74 @ p3 )
& ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
& ( ( ZZV @ p3 )
| ~ ( ZZV @ sk73 @ p3 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZV @ p3 )
| ( ZZV @ sk73 @ ( ZZV @ sk72 @ '$accessible_world' ) )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZV @ p3 )
| ( ZZV @ sk72 @ p3 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZV @ p3 )
| ( ZZV @ sk72 @ ( ZZV @ '$accessible_world' ) )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) ) )
& ~ ( sk71 @ p2 )
& ( sk71 @ ( '$local_world' @ '$accessible_world' ) )
& ( ( ZZU @ p2 )
| ~ ( ZZU @ sk70 @ p2 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZU @ p2 )
| ( ZZU @ sk70 @ ( ZZU @ sk69 @ '$accessible_world' ) )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZU @ p2 )
| ( ZZU @ sk69 @ p2 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZU @ p2 )
| ( ZZU @ sk69 @ ( ZZU @ '$accessible_world' ) )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) ) )
& ~ ( sk68 @ p1 )
& ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
& ( ( ZZT @ p1 )
| ~ ( ZZT @ sk67 @ p1 )
| ~ ( ZZT @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZT @ p1 )
| ( ZZT @ sk67 @ ( ZZT @ sk66 @ '$accessible_world' ) )
| ~ ( ZZT @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZT @ p1 )
| ( ZZT @ sk66 @ p1 )
| ~ ( ZZT @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZT @ p1 )
| ( ZZT @ sk66 @ ( ZZT @ '$accessible_world' ) )
| ~ ( ZZT @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( ZZS @ p2 )
| ~ ( ZZR @ ( ZZS @ sk65 ) @ p2 )
| ~ ( ZZS @ ( ZZR @ '$accessible_world' ) )
| ~ ( ZZR @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 )
& ( ( ZZS @ p2 )
| ( ZZR @ ( ZZS @ sk65 ) @ ( ZZR @ ( ZZS @ sk64 ) @ '$accessible_world' ) )
| ~ ( ZZS @ ( ZZR @ '$accessible_world' ) )
| ~ ( ZZR @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 )
& ( ( ZZS @ p2 )
| ( ZZR @ ( ZZS @ sk64 ) @ p2 )
| ~ ( ZZS @ ( ZZR @ '$accessible_world' ) )
| ~ ( ZZR @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 )
& ( ( ZZS @ p2 )
| ( ZZR @ ( ZZS @ sk64 ) @ ( ZZS @ '$accessible_world' ) )
| ~ ( ZZS @ ( ZZR @ '$accessible_world' ) )
| ~ ( ZZR @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 )
& ( sk62
| ~ ( sk63 @ p2 )
| ~ sk41 )
& ( sk62
| ( ZZQ @ p2 )
| ~ ( ZZQ @ ( ZZP @ '$accessible_world' ) )
| ~ ( ZZP @ p2 )
| ~ ( ZZP @ ( sk63 @ '$accessible_world' ) )
| ~ sk41 )
& ( sk62
| ( sk63 @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk41 )
& ( ( '$local_world' @ p2 )
| ~ ( sk61 @ p2 )
| ~ sk41 )
& ( ( '$local_world' @ p2 )
| ( sk61 @ ( sk60 @ '$accessible_world' ) )
| ~ sk41 )
& ( ( '$local_world' @ p2 )
| ( sk60 @ p2 )
| ~ sk41 )
& ( ( '$local_world' @ p2 )
| ( sk60 @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk41 )
& ( sk41
| ~ ( sk59 @ p2 )
| sk55 )
& ( sk41
| ( ZZO @ p2 )
| ~ ( ZZO @ ( ZZN @ '$accessible_world' ) )
| ~ ( ZZN @ p2 )
| ~ ( ZZN @ ( sk59 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( sk59 @ ( sk58 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( sk58 @ ( sk42 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( ZZM @ p2 )
| ~ ( ZZM @ sk57 @ p2 )
| ~ ( ZZM @ ( sk42 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( ZZM @ p2 )
| ( ZZM @ sk57 @ ( ZZM @ sk56 @ '$accessible_world' ) )
| ~ ( ZZM @ ( sk42 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( ZZM @ p2 )
| ( ZZM @ sk56 @ p2 )
| ~ ( ZZM @ ( sk42 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ( ZZM @ p2 )
| ( ZZM @ sk56 @ ( ZZM @ '$accessible_world' ) )
| ~ ( ZZM @ ( sk42 @ '$accessible_world' ) )
| sk55 )
& ( sk41
| ~ sk55
| ~ ( sk42 @ p2 ) )
& ( sk41
| ~ sk55
| ( ZZL @ p2 )
| ~ ( ZZL @ ( ZZK @ '$accessible_world' ) )
| ~ ( ZZK @ p2 )
| ~ ( ZZK @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZJ @ p2 )
| ~ ( ZZ @ ( ZZF @ ( ZZI @ ( ZZJ @ sk54 ) ) ) @ p2 )
| ~ ( ZZJ @ ( ZZI @ '$accessible_world' ) )
| ~ ( ZZI @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ sk51 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZJ @ p2 )
| ( ZZ @ ( ZZF @ ( ZZI @ ( ZZJ @ sk54 ) ) ) @ ( ZZ @ ( ZZF @ ( ZZI @ ( ZZJ @ sk53 ) ) ) @ '$accessible_world' ) )
| ~ ( ZZJ @ ( ZZI @ '$accessible_world' ) )
| ~ ( ZZI @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ sk51 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZJ @ p2 )
| ( ZZ @ ( ZZF @ ( ZZI @ ( ZZJ @ sk53 ) ) ) @ p2 )
| ~ ( ZZJ @ ( ZZI @ '$accessible_world' ) )
| ~ ( ZZI @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ sk51 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZJ @ p2 )
| ( ZZ @ ( ZZF @ ( ZZI @ ( ZZJ @ sk53 ) ) ) @ ( ZZJ @ '$accessible_world' ) )
| ~ ( ZZJ @ ( ZZI @ '$accessible_world' ) )
| ~ ( ZZI @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ sk51 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ sk51 )
| ~ ( ZZ @ ( ZZF @ sk52 ) @ p2 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ sk51 )
| ( ZZH @ p2 )
| ~ ( ZZH @ ( ZZG @ '$accessible_world' ) )
| ~ ( ZZG @ p2 )
| ~ ( ZZG @ ( ZZ @ ( ZZF @ sk52 ) @ '$accessible_world' ) )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ sk51 )
| ( ZZ @ ( ZZF @ sk52 ) @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ p2 )
| ~ ( ZZ @ ( ZZF @ sk50 ) @ p2 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ p2 )
| ( ZZ @ ( ZZF @ sk50 ) @ ( ZZ @ ( ZZF @ sk49 ) @ '$accessible_world' ) )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ p2 )
| ( ZZ @ ( ZZF @ sk49 ) @ p2 )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZF @ p2 )
| ( ZZ @ ( ZZF @ sk49 ) @ ( ZZF @ '$accessible_world' ) )
| ~ ( ZZF @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ sk43 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ~ ( ZZ @ sk48 @ p2 )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZE @ p2 )
| ~ ( ZZE @ ( ZZD @ '$accessible_world' ) )
| ~ ( ZZD @ p2 )
| ~ ( ZZD @ ( ZZ @ sk48 @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZ @ sk48 @ ( ZZ @ sk47 @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZ @ sk47 @ ( ZZ @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZC @ p2 )
| ~ ( ZZ @ ( ZZC @ sk46 ) @ p2 )
| ~ ( ZZC @ ( ZZ @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZC @ p2 )
| ( ZZ @ ( ZZC @ sk46 ) @ ( ZZ @ ( ZZC @ sk45 ) @ '$accessible_world' ) )
| ~ ( ZZC @ ( ZZ @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZC @ p2 )
| ( ZZ @ ( ZZC @ sk45 ) @ p2 )
| ~ ( ZZC @ ( ZZ @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ( ZZC @ p2 )
| ( ZZ @ ( ZZC @ sk45 ) @ ( ZZC @ '$accessible_world' ) )
| ~ ( ZZC @ ( ZZ @ '$accessible_world' ) )
| ( ZZ @ sk44 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ~ ( ZZ @ sk44 )
| ~ ( ZZ @ p2 )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( ZZ @ sk43 )
| ~ ( ZZ @ sk44 )
| ( ZZB @ p2 )
| ~ ( ZZB @ ( ZZA @ '$accessible_world' ) )
| ~ ( ZZA @ p2 )
| ~ ( ZZA @ ( ZZ @ '$accessible_world' ) )
| ~ ( ZZ @ ( sk42 @ '$accessible_world' ) ) )
& ( sk41
| ( sk42 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk34 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk38 @ p4 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk38 @ p3 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk38 @ p2 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk38 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk39 @ p4 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk39 @ p3 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk39 @ p2 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk39 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( sk40 @ ( sk39 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( sk39 @ ( sk38 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( sk38 @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ p1 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk35 @ p4 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk35 @ p3 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk35 @ p2 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk35 @ p1 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk36 @ p4 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk36 @ p3 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk36 @ p2 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ sk36 @ p1 )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ( ZR @ sk37 @ ( ZR @ sk36 @ '$accessible_world' ) )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ( ZR @ sk36 @ ( ZR @ sk35 @ '$accessible_world' ) )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( ZS @ p1 )
| ( ZT @ p4 )
| ( ZT @ p3 )
| ( ZT @ p2 )
| ( ZT @ p1 )
| ( ZU @ p4 )
| ( ZU @ p3 )
| ( ZU @ p2 )
| ( ZU @ p1 )
| ~ ( ZV @ ( ZU @ '$accessible_world' ) )
| ~ ( ZU @ ( ZT @ '$accessible_world' ) )
| ~ ( ZT @ ( ZS @ '$accessible_world' ) )
| ~ ( ZS @ ( ZR @ '$accessible_world' ) )
| ( ZR @ sk35 @ ( ZR @ '$accessible_world' ) )
| ~ ( ZR @ ( sk34 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( ZW @ p4 )
| ( ZW @ p3 )
| ( ZW @ p2 )
| ( ZW @ p1 )
| ( ZX @ p4 )
| ( ZX @ p3 )
| ( ZX @ p2 )
| ( ZX @ p1 )
| ~ ( ZY @ ( ZX @ '$accessible_world' ) )
| ~ ( ZX @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ( sk34 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk29 @ p4 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk29 @ p3 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk29 @ p2 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk29 @ p1 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk32 @ p4 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk32 @ p3 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk32 @ p2 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk32 @ p1 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( sk33 @ ( sk32 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( sk32 @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ p4 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ p3 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ p2 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ p1 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ sk30 @ p4 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ sk30 @ p3 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ sk30 @ p2 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ sk30 @ p1 )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ( ZL @ sk31 @ ( ZL @ sk30 @ '$accessible_world' ) )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZM @ p4 )
| ( ZM @ p3 )
| ( ZM @ p2 )
| ( ZM @ p1 )
| ( ZN @ p4 )
| ( ZN @ p3 )
| ( ZN @ p2 )
| ( ZN @ p1 )
| ~ ( ZO @ ( ZN @ '$accessible_world' ) )
| ~ ( ZN @ ( ZM @ '$accessible_world' ) )
| ~ ( ZM @ ( ZL @ '$accessible_world' ) )
| ( ZL @ sk30 @ ( ZL @ '$accessible_world' ) )
| ~ ( ZL @ ( sk29 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZP @ p4 )
| ( ZP @ p3 )
| ( ZP @ p2 )
| ( ZP @ p1 )
| ~ ( ZQ @ ( ZP @ '$accessible_world' ) )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( sk29 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk24 @ p3 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk24 @ p2 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk24 @ p1 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p4 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p3 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p2 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p1 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( sk28 @ ( sk27 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( sk27 @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ p3 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ p2 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ p1 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ sk25 @ p4 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ sk25 @ p3 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ sk25 @ p2 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ sk25 @ p1 )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ( ZF @ sk26 @ ( ZF @ sk25 @ '$accessible_world' ) )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p3 )
| ( ZG @ p2 )
| ( ZG @ p1 )
| ( ZH @ p4 )
| ( ZH @ p3 )
| ( ZH @ p2 )
| ( ZH @ p1 )
| ~ ( ZI @ ( ZH @ '$accessible_world' ) )
| ~ ( ZH @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ ( ZF @ '$accessible_world' ) )
| ( ZF @ sk25 @ ( ZF @ '$accessible_world' ) )
| ~ ( ZF @ ( sk24 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZJ @ p4 )
| ( ZJ @ p3 )
| ( ZJ @ p2 )
| ( ZJ @ p1 )
| ~ ( ZK @ ( ZJ @ '$accessible_world' ) )
| ~ ( ZJ @ ( '$local_world' @ '$accessible_world' ) )
| ( sk24 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk19 @ p2 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk19 @ p1 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk22 @ p4 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk22 @ p3 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk22 @ p2 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk22 @ p1 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( sk23 @ ( sk22 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( sk22 @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ p2 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ p1 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ sk20 @ p4 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ sk20 @ p3 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ sk20 @ p2 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ sk20 @ p1 )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ( Z @ sk21 @ ( Z @ sk20 @ '$accessible_world' ) )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZA @ p2 )
| ( ZA @ p1 )
| ( ZB @ p4 )
| ( ZB @ p3 )
| ( ZB @ p2 )
| ( ZB @ p1 )
| ~ ( ZC @ ( ZB @ '$accessible_world' ) )
| ~ ( ZB @ ( ZA @ '$accessible_world' ) )
| ~ ( ZA @ ( Z @ '$accessible_world' ) )
| ( Z @ sk20 @ ( Z @ '$accessible_world' ) )
| ~ ( Z @ ( sk19 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( ZD @ p4 )
| ( ZD @ p3 )
| ( ZD @ p2 )
| ( ZD @ p1 )
| ~ ( ZE @ ( ZD @ '$accessible_world' ) )
| ~ ( ZD @ ( '$local_world' @ '$accessible_world' ) )
| ( sk19 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk14 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk17 @ p4 ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk17 @ p3 ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk17 @ p2 ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk17 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( sk18 @ ( sk17 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( sk17 @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ~ ( T @ p1 )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ~ ( T @ sk15 @ p4 )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ~ ( T @ sk15 @ p3 )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ~ ( T @ sk15 @ p2 )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ~ ( T @ sk15 @ p1 )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ( T @ sk16 @ ( T @ sk15 @ '$accessible_world' ) )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( U @ p1 )
| ( V @ p4 )
| ( V @ p3 )
| ( V @ p2 )
| ( V @ p1 )
| ~ ( W @ ( V @ '$accessible_world' ) )
| ~ ( V @ ( U @ '$accessible_world' ) )
| ~ ( U @ ( T @ '$accessible_world' ) )
| ( T @ sk15 @ ( T @ '$accessible_world' ) )
| ~ ( T @ ( sk14 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ( X @ p4 )
| ( X @ p3 )
| ( X @ p2 )
| ( X @ p1 )
| ~ ( Y @ ( X @ '$accessible_world' ) )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( sk14 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk11 @ p4 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk11 @ p3 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk11 @ p2 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk11 @ p1 ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( sk13 @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( Q @ p4 )
| ( Q @ p3 )
| ( Q @ p2 )
| ( Q @ p1 )
| ~ ( R @ ( Q @ '$accessible_world' ) )
| ~ ( Q @ ( P @ '$accessible_world' ) )
| ~ ( P @ p4 )
| ~ ( P @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( Q @ p4 )
| ( Q @ p3 )
| ( Q @ p2 )
| ( Q @ p1 )
| ~ ( R @ ( Q @ '$accessible_world' ) )
| ~ ( Q @ ( P @ '$accessible_world' ) )
| ~ ( P @ p3 )
| ~ ( P @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( Q @ p4 )
| ( Q @ p3 )
| ( Q @ p2 )
| ( Q @ p1 )
| ~ ( R @ ( Q @ '$accessible_world' ) )
| ~ ( Q @ ( P @ '$accessible_world' ) )
| ~ ( P @ p2 )
| ~ ( P @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( Q @ p4 )
| ( Q @ p3 )
| ( Q @ p2 )
| ( Q @ p1 )
| ~ ( R @ ( Q @ '$accessible_world' ) )
| ~ ( Q @ ( P @ '$accessible_world' ) )
| ~ ( P @ p1 )
| ~ ( P @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( Q @ p4 )
| ( Q @ p3 )
| ( Q @ p2 )
| ( Q @ p1 )
| ~ ( R @ ( Q @ '$accessible_world' ) )
| ~ ( Q @ ( P @ '$accessible_world' ) )
| ( P @ sk12 @ ( P @ '$accessible_world' ) )
| ~ ( P @ ( sk11 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( S @ ( '$local_world' @ '$accessible_world' ) )
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk8 @ p3 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk8 @ p2 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk8 @ p1 ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( sk10 @ ( sk8 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( M @ p3 )
| ( M @ p2 )
| ( M @ p1 )
| ~ ( N @ ( M @ '$accessible_world' ) )
| ~ ( M @ ( L @ '$accessible_world' ) )
| ~ ( L @ p3 )
| ~ ( L @ ( sk8 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( M @ p3 )
| ( M @ p2 )
| ( M @ p1 )
| ~ ( N @ ( M @ '$accessible_world' ) )
| ~ ( M @ ( L @ '$accessible_world' ) )
| ~ ( L @ p2 )
| ~ ( L @ ( sk8 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( M @ p3 )
| ( M @ p2 )
| ( M @ p1 )
| ~ ( N @ ( M @ '$accessible_world' ) )
| ~ ( M @ ( L @ '$accessible_world' ) )
| ~ ( L @ p1 )
| ~ ( L @ ( sk8 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( M @ p3 )
| ( M @ p2 )
| ( M @ p1 )
| ~ ( N @ ( M @ '$accessible_world' ) )
| ~ ( M @ ( L @ '$accessible_world' ) )
| ( L @ sk9 @ ( L @ '$accessible_world' ) )
| ~ ( L @ ( sk8 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ( sk8 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk5 @ p2 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk5 @ p1 ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ( sk7 @ ( sk5 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ( I @ p2 )
| ( I @ p1 )
| ~ ( J @ ( I @ '$accessible_world' ) )
| ~ ( I @ ( H @ '$accessible_world' ) )
| ~ ( H @ p2 )
| ~ ( H @ ( sk5 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ( I @ p2 )
| ( I @ p1 )
| ~ ( J @ ( I @ '$accessible_world' ) )
| ~ ( I @ ( H @ '$accessible_world' ) )
| ~ ( H @ p1 )
| ~ ( H @ ( sk5 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ( I @ p2 )
| ( I @ p1 )
| ~ ( J @ ( I @ '$accessible_world' ) )
| ~ ( I @ ( H @ '$accessible_world' ) )
| ( H @ sk6 @ ( H @ '$accessible_world' ) )
| ~ ( H @ ( sk5 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( K @ ( '$local_world' @ '$accessible_world' ) )
| ( sk5 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk2 @ p1 ) )
& ( ( '$local_world' @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ( sk4 @ ( sk2 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ( E @ p1 )
| ~ ( F @ ( E @ '$accessible_world' ) )
| ~ ( E @ ( D @ '$accessible_world' ) )
| ~ ( D @ p1 )
| ~ ( D @ ( sk2 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ( E @ p1 )
| ~ ( F @ ( E @ '$accessible_world' ) )
| ~ ( E @ ( D @ '$accessible_world' ) )
| ( D @ sk3 @ ( D @ '$accessible_world' ) )
| ~ ( D @ ( sk2 @ '$accessible_world' ) ) )
& ( ( '$local_world' @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( A @ p2 )
| ( C @ p2 )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ p2 )
| ~ ( B @ ( A @ sk1 @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ) ),
inference(cnf,[status(esa)],[5]) ).
thf(151,plain,
( ( '$local_world' @ p2 )
| ( sk60 @ p2 )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(25,plain,
( ( '$local_world' @ p2 )
| ~ ( sk61 @ p2 )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(522,plain,
( ( ( sk61 @ p2 )
!= ( sk60 @ p2 ) )
| ( '$local_world' @ p2 )
| ~ $true
| ~ sk41
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[151,25]) ).
thf(523,plain,
( ( ( sk61 @ p2 )
!= ( sk60 @ p2 ) )
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(simp,[status(thm)],[522]) ).
thf(541,plain,
( ( sk61 != sk60 )
| ~ sk41
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[523]) ).
thf(21,plain,
sk74 @ ( '$local_world' @ '$accessible_world' ),
inference(cnfConj,[status(thm)],[6]) ).
thf(7,plain,
! [A: '$world'] :
( ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(420,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,7]) ).
thf(421,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[420]) ).
thf(422,plain,
( ( sk74 @ p2 )
| ( sk74 @ sk1 @ ( sk74 @ '$accessible_world' ) ) ),
inference(pattern_uni,[status(thm)],[421:[bind(A,$thf( sk74 ))]]) ).
thf(34,plain,
! [B: '$world',A: '$world'] :
( ( B @ p2 )
| ~ ( A @ ( B @ sk65 ) @ p2 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(277,plain,
! [B: '$world',A: '$world'] :
( ( B @ p2 )
| ~ ( A @ ( B @ sk65 ) @ p2 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 ),
inference(simp,[status(thm)],[34]) ).
thf(378,plain,
! [B: '$world',A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( B @ ( A @ '$accessible_world' ) ) )
| ( B @ p2 )
| ~ ( A @ ( B @ sk65 ) @ p2 )
| ~ $true
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[21,277]) ).
thf(379,plain,
! [B: '$world',A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( B @ ( A @ '$accessible_world' ) ) )
| ( B @ p2 )
| ~ ( A @ ( B @ sk65 ) @ p2 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 ),
inference(simp,[status(thm)],[378]) ).
thf(380,plain,
( ( sk74 @ p2 )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ ( '$local_world' @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41 ),
inference(pattern_uni,[status(thm)],[379:[bind(A,$thf( '$local_world' )),bind(B,$thf( sk74 ))]]) ).
thf(445,plain,
( ( ( sk74 @ sk1 @ ( sk74 @ '$accessible_world' ) )
!= ( '$local_world' @ ( '$local_world' @ '$accessible_world' ) ) )
| ( sk74 @ p2 )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ $true
| ~ sk62
| ~ sk41
| ( sk74 @ p2 ) ),
inference(paramod_ordered,[status(thm)],[422,380]) ).
thf(446,plain,
( ( ( sk74 @ sk1 @ ( sk74 @ '$accessible_world' ) )
!= ( '$local_world' @ ( '$local_world' @ '$accessible_world' ) ) )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ sk62
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[445]) ).
thf(454,plain,
( ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ sk62
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[446]) ).
thf(560,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ $true
| ~ sk62
| ~ sk41
| ( sk74 @ p2 )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[541,454]) ).
thf(561,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk74 @ p2 )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[560]) ).
thf(570,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) )
!= '$local_world' )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk61 != sk60 )
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[561]) ).
thf(132,plain,
( sk62
| ~ ( sk63 @ p2 )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(552,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ~ $true
| ~ sk41
| ( sk61 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[541,132]) ).
thf(553,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[552]) ).
thf(574,plain,
( ( sk63 != '$local_world' )
| ( sk61 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[553]) ).
thf(540,plain,
( ~ $true
| ( ( sk60 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(eqfactor_ordered,[status(thm)],[151]) ).
thf(545,plain,
( ( sk60 != '$local_world' )
| ~ sk41
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[540]) ).
thf(198,plain,
~ ( sk71 @ p2 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(602,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[545,198]) ).
thf(603,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[602]) ).
thf(610,plain,
( ( sk71 != '$local_world' )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[603]) ).
thf(96,plain,
( sk41
| ~ sk55
| ~ ( sk42 @ p2 ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(92,plain,
( sk41
| ( sk42 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(423,plain,
! [A: '$world'] :
( ( ( sk42 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true
| sk41 ),
inference(paramod_ordered,[status(thm)],[92,7]) ).
thf(424,plain,
! [A: '$world'] :
( ( ( sk42 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| sk41 ),
inference(simp,[status(thm)],[423]) ).
thf(425,plain,
( ( sk42 @ p2 )
| ( sk42 @ sk1 @ ( sk42 @ '$accessible_world' ) )
| sk41 ),
inference(pattern_uni,[status(thm)],[424:[bind(A,$thf( sk42 ))]]) ).
thf(566,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk61 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[541,198]) ).
thf(567,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[566]) ).
thf(572,plain,
( ( sk71 != '$local_world' )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[567]) ).
thf(588,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ~ $true
| ~ sk41
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[545,132]) ).
thf(589,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[588]) ).
thf(608,plain,
( ( sk63 != '$local_world' )
| ( sk60 != '$local_world' )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[589]) ).
thf(524,plain,
( ( ( sk63 @ p2 )
!= ( sk60 @ p2 ) )
| sk62
| ~ $true
| ~ sk41
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[151,132]) ).
thf(525,plain,
( ( ( sk63 @ p2 )
!= ( sk60 @ p2 ) )
| sk62
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(simp,[status(thm)],[524]) ).
thf(548,plain,
( ( sk63 != sk60 )
| ~ sk41
| sk62
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[525]) ).
thf(544,plain,
( ( ( sk60 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ sk41
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[540]) ).
thf(538,plain,
( ( ( sk71 @ p2 )
!= ( sk60 @ p2 ) )
| ~ $true
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[151,198]) ).
thf(539,plain,
( ( ( sk71 @ p2 )
!= ( sk60 @ p2 ) )
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(simp,[status(thm)],[538]) ).
thf(549,plain,
( ( sk71 != sk60 )
| ~ sk41
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[539]) ).
thf(627,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk71 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[549,198]) ).
thf(628,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[627]) ).
thf(629,plain,
( ( sk71 != '$local_world' )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[628]) ).
thf(153,plain,
sk68 @ ( '$local_world' @ '$accessible_world' ),
inference(cnfConj,[status(thm)],[6]) ).
thf(170,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(204,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(1293,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p1 )
| ~ $true
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(paramod_ordered,[status(thm)],[153,204]) ).
thf(1294,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p1 )
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[1293]) ).
thf(1295,plain,
( ( '$local_world' @ p1 )
| ( sk2 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(pattern_uni,[status(thm)],[1294:[bind(A,$thf( sk68 ))]]) ).
thf(28,plain,
! [A: '$world'] :
( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(245,plain,
! [A: '$world'] :
( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[28]) ).
thf(681,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ $true
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(paramod_ordered,[status(thm)],[21,245]) ).
thf(682,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[681]) ).
thf(683,plain,
( ( '$local_world' @ p4 )
| ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( sk11 @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(pattern_uni,[status(thm)],[682:[bind(A,$thf( sk74 ))]]) ).
thf(120,plain,
( sk41
| ( sk58 @ ( sk42 @ '$accessible_world' ) )
| sk55 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(91,plain,
sk71 @ ( '$local_world' @ '$accessible_world' ),
inference(cnfConj,[status(thm)],[6]) ).
thf(168,plain,
! [A: '$world'] :
( ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(802,plain,
! [A: '$world'] :
( ( ( sk71 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[91,168]) ).
thf(803,plain,
! [A: '$world'] :
( ( ( sk71 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[802]) ).
thf(804,plain,
( ( sk71 @ p2 )
| ~ ( sk71 @ sk1 @ p2 ) ),
inference(pattern_uni,[status(thm)],[803:[bind(A,$thf( sk71 ))]]) ).
thf(864,plain,
( $false
| ~ ( sk71 @ sk1 @ p2 ) ),
inference(rewrite,[status(thm)],[804,198]) ).
thf(865,plain,
~ ( sk71 @ sk1 @ p2 ),
inference(simp,[status(thm)],[864]) ).
thf(874,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( sk60 @ p2 ) )
| ~ $true
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[151,865]) ).
thf(875,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( sk60 @ p2 ) )
| ( '$local_world' @ p2 )
| ~ sk41 ),
inference(simp,[status(thm)],[874]) ).
thf(878,plain,
( ( ( sk71 @ sk1 )
!= sk60 )
| ~ sk41
| ( '$local_world' @ p2 ) ),
inference(simp,[status(thm)],[875]) ).
thf(101,plain,
! [D: '$world',C: '$world',B: '$world',A: '$world'] :
( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( D @ ( '$local_world' @ '$accessible_world' ) )
| ( B @ p2 )
| ( B @ p1 )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ p1 )
| ~ ( A @ ( sk5 @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(202,plain,
! [D: '$world',C: '$world',B: '$world',A: '$world'] :
( ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ~ ( D @ ( '$local_world' @ '$accessible_world' ) )
| ( B @ p2 )
| ( B @ p1 )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ p1 )
| ~ ( A @ ( sk5 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(10,plain,
~ ( sk68 @ p1 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(174,plain,
! [C: '$world',B: '$world',A: '$world'] :
( ( A @ p2 )
| ( C @ p2 )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ p2 )
| ~ ( B @ ( A @ sk1 @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(1384,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true
| ( '$local_world' @ p1 ) ),
inference(paramod_ordered,[status(thm)],[1295,7]) ).
thf(1385,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ( '$local_world' @ p1 ) ),
inference(simp,[status(thm)],[1384]) ).
thf(1386,plain,
( ( sk2 @ p2 )
| ( sk2 @ sk1 @ ( sk2 @ '$accessible_world' ) )
| ( '$local_world' @ p1 ) ),
inference(pattern_uni,[status(thm)],[1385:[bind(A,$thf( sk2 ))]]) ).
thf(93,plain,
( sk62
| ( sk63 @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(57,plain,
( sk41
| ( sk59 @ ( sk58 @ '$accessible_world' ) )
| sk55 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(868,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[545,865]) ).
thf(869,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[868]) ).
thf(877,plain,
( ( ( sk71 @ sk1 )
!= '$local_world' )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[869]) ).
thf(438,plain,
! [A: '$world'] :
( ( ( sk71 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[91,7]) ).
thf(439,plain,
! [A: '$world'] :
( ( ( sk71 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[438]) ).
thf(440,plain,
( ( sk71 @ p2 )
| ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) ) ),
inference(pattern_uni,[status(thm)],[439:[bind(A,$thf( sk71 ))]]) ).
thf(473,plain,
( $false
| ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) ) ),
inference(rewrite,[status(thm)],[440,198]) ).
thf(474,plain,
sk71 @ sk1 @ ( sk71 @ '$accessible_world' ),
inference(simp,[status(thm)],[473]) ).
thf(811,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[474,168]) ).
thf(812,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[811]) ).
thf(826,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 )
!= A )
| ( sk71 != '$local_world' )
| ~ ( A @ sk1 @ p2 )
| ( A @ p2 ) ),
inference(simp,[status(thm)],[812]) ).
thf(833,plain,
( ( sk71 != '$local_world' )
| ~ ( sk71 @ sk1 @ sk1 @ p2 )
| ( sk71 @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[826]) ).
thf(1103,plain,
( ( sk71 != '$local_world' )
| ~ ( sk71 @ sk1 @ sk1 @ p2 )
| $false ),
inference(rewrite,[status(thm)],[833,865]) ).
thf(1104,plain,
( ( sk71 != '$local_world' )
| ~ ( sk71 @ sk1 @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[1103]) ).
thf(138,plain,
! [B: '$world',A: '$world'] :
( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p3 ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(201,plain,
! [B: '$world',A: '$world'] :
( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( A @ p4 )
| ( A @ p3 )
| ( A @ p2 )
| ( A @ p1 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk27 @ p3 ) ),
inference(simp,[status(thm)],[138]) ).
thf(613,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ~ $true
| ~ sk41
| ( sk71 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[549,132]) ).
thf(614,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[613]) ).
thf(630,plain,
( ( sk63 != '$local_world' )
| ( sk71 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[614]) ).
thf(475,plain,
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( '$local_world' @ ( '$local_world' @ '$accessible_world' ) ) )
| ( sk74 @ p2 )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ $true
| ~ sk62
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[474,380]) ).
thf(476,plain,
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( '$local_world' @ ( '$local_world' @ '$accessible_world' ) ) )
| ( sk74 @ p2 )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ sk62
| ~ sk41 ),
inference(simp,[status(thm)],[475]) ).
thf(484,plain,
( ( ( sk71 @ sk1 )
!= '$local_world' )
| ( sk71 != '$local_world' )
| ~ ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
| ~ sk62
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[476]) ).
thf(197,plain,
( sk41
| ~ ( sk59 @ p2 )
| sk55 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(866,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk61 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[541,865]) ).
thf(867,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[866]) ).
thf(879,plain,
( ( ( sk71 @ sk1 )
!= '$local_world' )
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[867]) ).
thf(157,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk4 @ ( sk2 @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(218,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ( sk4 @ ( sk2 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(1872,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p1 )
| ~ $true
| ( sk4 @ ( sk2 @ '$accessible_world' ) )
| ( '$local_world' @ p1 ) ),
inference(paramod_ordered,[status(thm)],[1295,218]) ).
thf(1873,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( sk4 @ ( sk2 @ '$accessible_world' ) )
| ( '$local_world' @ p1 ) ),
inference(simp,[status(thm)],[1872]) ).
thf(1874,plain,
( ( sk4 @ ( sk2 @ '$accessible_world' ) )
| ( '$local_world' @ p1 ) ),
inference(pattern_uni,[status(thm)],[1873:[bind(A,$thf( sk2 ))]]) ).
thf(558,plain,
! [B: '$world',A: '$world'] :
( ( ( A @ ( B @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( B @ p2 )
| ~ $true
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ~ sk41
| ( sk61 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[541,277]) ).
thf(559,plain,
! [B: '$world',A: '$world'] :
( ( ( A @ ( B @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( B @ p2 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ( sk61 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[558]) ).
thf(569,plain,
! [B: '$world',A: '$world'] :
( ( ( A @ ( B @ sk65 ) )
!= '$local_world' )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk62
| ( sk61 != sk60 )
| ~ sk41
| ( B @ p2 ) ),
inference(simp,[status(thm)],[559]) ).
thf(790,plain,
! [A: '$world'] :
( ( ( sk42 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true
| sk41 ),
inference(paramod_ordered,[status(thm)],[92,168]) ).
thf(791,plain,
! [A: '$world'] :
( ( ( sk42 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| sk41 ),
inference(simp,[status(thm)],[790]) ).
thf(792,plain,
( ( sk42 @ p2 )
| ~ ( sk42 @ sk1 @ p2 )
| sk41 ),
inference(pattern_uni,[status(thm)],[791:[bind(A,$thf( sk42 ))]]) ).
thf(760,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(paramod_ordered,[status(thm)],[548,198]) ).
thf(761,plain,
( ( ( sk71 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[760]) ).
thf(765,plain,
( ( sk71 != '$local_world' )
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[761]) ).
thf(1387,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true
| ( '$local_world' @ p1 ) ),
inference(paramod_ordered,[status(thm)],[1295,168]) ).
thf(1388,plain,
! [A: '$world'] :
( ( ( sk2 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ( '$local_world' @ p1 ) ),
inference(simp,[status(thm)],[1387]) ).
thf(1389,plain,
( ( sk2 @ p2 )
| ~ ( sk2 @ sk1 @ p2 )
| ( '$local_world' @ p1 ) ),
inference(pattern_uni,[status(thm)],[1388:[bind(A,$thf( sk2 ))]]) ).
thf(782,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[153,168]) ).
thf(783,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[782]) ).
thf(784,plain,
( ( sk68 @ p2 )
| ~ ( sk68 @ sk1 @ p2 ) ),
inference(pattern_uni,[status(thm)],[783:[bind(A,$thf( sk68 ))]]) ).
thf(81,plain,
( ( '$local_world' @ p2 )
| ( sk60 @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(746,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| sk62
| ~ $true
| ~ sk41
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(paramod_ordered,[status(thm)],[548,132]) ).
thf(747,plain,
( ( ( sk63 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[746]) ).
thf(764,plain,
( ( sk63 != '$local_world' )
| ( sk63 != sk60 )
| ~ sk41
| sk62 ),
inference(simp,[status(thm)],[747]) ).
thf(596,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ $true
| ~ sk62
| ~ sk41
| ( sk74 @ p2 )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[545,454]) ).
thf(597,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk74 @ p2 )
| ( sk60 != '$local_world' )
| ~ sk41 ),
inference(simp,[status(thm)],[596]) ).
thf(604,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) )
!= '$local_world' )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk60 != '$local_world' )
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[597]) ).
thf(621,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ $true
| ~ sk62
| ~ sk41
| ( sk74 @ p2 )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[549,454]) ).
thf(622,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) @ p2 )
!= ( '$local_world' @ p2 ) )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk74 @ p2 )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[621]) ).
thf(631,plain,
( ( ( '$local_world' @ ( sk74 @ sk65 ) )
!= '$local_world' )
| ( ( sk74 @ sk1 )
!= '$local_world' )
| ( sk74 != '$local_world' )
| ~ sk62
| ( sk71 != sk60 )
| ~ sk41
| ( sk74 @ p2 ) ),
inference(simp,[status(thm)],[622]) ).
thf(14,plain,
! [A: '$world'] :
( ( A @ p2 )
| ~ ( A @ sk70 @ p2 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(213,plain,
! [A: '$world'] :
( ( A @ p2 )
| ~ ( A @ sk70 @ p2 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[14]) ).
thf(108,plain,
~ ( sk74 @ p3 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(477,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[474,7]) ).
thf(478,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 @ ( sk71 @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[477]) ).
thf(485,plain,
! [A: '$world'] :
( ( ( sk71 @ sk1 )
!= A )
| ( sk71 != '$local_world' )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[478]) ).
thf(487,plain,
( ( sk71 != '$local_world' )
| ( sk71 @ sk1 @ p2 )
| ( sk71 @ sk1 @ sk1 @ ( sk71 @ sk1 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[485]) ).
thf(2721,plain,
( ( sk71 != '$local_world' )
| $false
| ( sk71 @ sk1 @ sk1 @ ( sk71 @ sk1 @ '$accessible_world' ) ) ),
inference(rewrite,[status(thm)],[487,865]) ).
thf(2722,plain,
( ( sk71 != '$local_world' )
| ( sk71 @ sk1 @ sk1 @ ( sk71 @ sk1 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[2721]) ).
thf(872,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ~ $true
| ( sk71 != sk60 )
| ~ sk41 ),
inference(paramod_ordered,[status(thm)],[549,865]) ).
thf(873,plain,
( ( ( sk71 @ sk1 @ p2 )
!= ( '$local_world' @ p2 ) )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[872]) ).
thf(876,plain,
( ( ( sk71 @ sk1 )
!= '$local_world' )
| ( sk71 != sk60 )
| ~ sk41 ),
inference(simp,[status(thm)],[873]) ).
thf(88,plain,
! [F: '$world',E: '$world',D: '$world',C: '$world',B: '$world',A: '$world'] :
( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ~ ( F @ ( E @ '$accessible_world' ) )
| ~ ( E @ ( '$local_world' @ '$accessible_world' ) )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ( D @ ( C @ '$accessible_world' ) )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ( A @ sk25 @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( sk24 @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(203,plain,
! [F: '$world',E: '$world',D: '$world',C: '$world',B: '$world',A: '$world'] :
( ( '$local_world' @ p3 )
| ( '$local_world' @ p2 )
| ( '$local_world' @ p1 )
| ( E @ p4 )
| ( E @ p3 )
| ( E @ p2 )
| ( E @ p1 )
| ~ ( F @ ( E @ '$accessible_world' ) )
| ~ ( E @ ( '$local_world' @ '$accessible_world' ) )
| ( B @ p3 )
| ( B @ p2 )
| ( B @ p1 )
| ( C @ p4 )
| ( C @ p3 )
| ( C @ p2 )
| ( C @ p1 )
| ~ ( D @ ( C @ '$accessible_world' ) )
| ~ ( C @ ( B @ '$accessible_world' ) )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ( A @ sk25 @ ( A @ '$accessible_world' ) )
| ~ ( A @ ( sk24 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(769,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,168]) ).
thf(770,plain,
! [A: '$world'] :
( ( ( sk74 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ~ ( A @ sk1 @ p2 ) ),
inference(simp,[status(thm)],[769]) ).
thf(771,plain,
( ( sk74 @ p2 )
| ~ ( sk74 @ sk1 @ p2 ) ),
inference(pattern_uni,[status(thm)],[770:[bind(A,$thf( sk74 ))]]) ).
thf(3,axiom,
! [A: '$world',B: '$world',C: '$world'] :
( ( ( C @ ( B @ '$accessible_world' ) )
& ( B @ ( A @ '$accessible_world' ) ) )
=> ( C @ ( A @ '$accessible_world' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_transitive) ).
thf(373,plain,
! [A: '$world',B: '$world',C: '$world'] :
( ( ( C @ ( B @ '$accessible_world' ) )
& ( B @ ( A @ '$accessible_world' ) ) )
=> ( C @ ( A @ '$accessible_world' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(435,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[153,7]) ).
thf(436,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( A @ p2 )
| ( A @ sk1 @ ( A @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[435]) ).
thf(437,plain,
( ( sk68 @ p2 )
| ( sk68 @ sk1 @ ( sk68 @ '$accessible_world' ) ) ),
inference(pattern_uni,[status(thm)],[436:[bind(A,$thf( sk68 ))]]) ).
thf(95,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk2 @ p1 ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(317,plain,
! [A: '$world'] :
( ( '$local_world' @ p1 )
| ~ ( A @ ( '$local_world' @ '$accessible_world' ) )
| ~ ( sk2 @ p1 ) ),
inference(simp,[status(thm)],[95]) ).
thf(1127,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p1 )
| ~ $true
| ~ ( sk2 @ p1 ) ),
inference(paramod_ordered,[status(thm)],[153,317]) ).
thf(1128,plain,
! [A: '$world'] :
( ( ( sk68 @ ( '$local_world' @ '$accessible_world' ) )
!= ( A @ ( '$local_world' @ '$accessible_world' ) ) )
| ( '$local_world' @ p1 )
| ~ ( sk2 @ p1 ) ),
inference(simp,[status(thm)],[1127]) ).
thf(1129,plain,
( ( '$local_world' @ p1 )
| ~ ( sk2 @ p1 ) ),
inference(pattern_uni,[status(thm)],[1128:[bind(A,$thf( sk68 ))]]) ).
thf(69,plain,
! [B: '$world',A: '$world'] :
( sk41
| ( B @ p2 )
| ~ ( A @ ( B @ sk50 ) @ p2 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ sk43 )
| ~ ( A @ ( sk42 @ '$accessible_world' ) ) ),
inference(cnfConj,[status(thm)],[6]) ).
thf(200,plain,
! [B: '$world',A: '$world'] :
( sk41
| ( B @ p2 )
| ~ ( A @ ( B @ sk50 ) @ p2 )
| ~ ( B @ ( A @ '$accessible_world' ) )
| ~ ( A @ sk43 )
| ~ ( A @ ( sk42 @ '$accessible_world' ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(111,plain,
( ( '$local_world' @ p2 )
| ( sk61 @ ( sk60 @ '$accessible_world' ) )
| ~ sk41 ),
inference(cnfConj,[status(thm)],[6]) ).
thf(46803,plain,
$false,
inference(e,[status(thm)],[570,574,610,96,425,572,608,548,544,549,629,1295,683,120,878,202,10,153,174,1386,25,93,57,877,132,1104,380,201,630,21,92,484,197,879,1874,569,792,541,765,1389,545,784,81,7,764,604,631,213,91,198,108,2722,876,203,771,151,168,422,865,373,4,437,474,1129,200,277,111,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYP033_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.16/0.40 % Computer : n015.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Sat Sep 26 20:26:44 UTC 2026
% 0.16/0.40 % CPUTime :
% 0.16/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.84/0.97 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.20/1.19 % [INFO] Parsing done (209ms).
% 1.43/1.21 % [INFO] Input problem is non-classical (logic $modal). Running HOL transformation from semantics specification contained in the problem file ...
% 1.43/1.23 %%% First-order logic specification detected, trying modal-logic-to-TXF embedding (redirected from embedding '$$modal' to embedding '$$fomlModel' version 1.3.7) ... Use flag -p FORCE_HIGHERORDER if you want to have THF output instead.
% 1.63/1.34 % [INFO] Running in sequential loop mode.
% 2.43/1.72 % [INFO] eprover registered as external prover.
% 2.43/1.73 % [INFO] Scanning for conjecture ...
% 2.85/1.98 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 3.14/2.06 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 3.14/2.07 % [INFO] Problem is typed first-order (TPTP TFF).
% 3.14/2.08 % [INFO] Type checking passed.
% 3.14/2.09 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 102.67/24.10 % External prover 'e' found a proof!
% 102.67/24.11 % [INFO] Killing All external provers ...
% 102.67/24.11 % Time passed: 23562ms (effective reasoning time: 22763ms)
% 102.67/24.11 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 102.67/24.11 % Axioms used in derivation (1): mrel_transitive
% 102.67/24.11 % No. of inferences in proof: 175
% 102.67/24.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 23562 ms resp. 22763 ms w/o parsing
% 100.85/24.53 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 100.85/24.54 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------