%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYP017_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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:51:44 AM UTC 2026
% Result : Theorem 8.58s 4.23s
% Output : Refutation 9.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 73
% Syntax : Number of formulae : 80 ( 76 unt; 0 typ; 72 def)
% Number of atoms : 3306 ( 72 equ; 0 cnn)
% Maximal formula atoms : 1430 ( 41 avg)
% Number of connectives : 7595 ( 999 ~;1305 |; 855 &;3442 @)
% ( 0 <=>; 994 =>; 0 <=; 0 <~>)
% Maximal formula depth : 402 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 117 ( 115 usr; 84 con; 0-2 aty)
% Number of variables : 738 ( 20 ^; 646 !; 0 ?; 738 :)
% ( 0 !>; 0 ?*; 0 @-; 72 @+)
% 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(p10_decl,type,
p10: '$world' > $o ).
thf(p3_decl,type,
p3: '$world' > $o ).
thf(p11_decl,type,
p11: '$world' > $o ).
thf(p2_decl,type,
p2: '$world' > $o ).
thf(p9_decl,type,
p9: '$world' > $o ).
thf(p1_decl,type,
p1: '$world' > $o ).
thf(p4_decl,type,
p4: '$world' > $o ).
thf(p7_decl,type,
p7: '$world' > $o ).
thf(p5_decl,type,
p5: '$world' > $o ).
thf(p6_decl,type,
p6: '$world' > $o ).
thf(p8_decl,type,
p8: '$world' > $o ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: $o ).
thf(sk3_decl,type,
sk3: '$world' ).
thf(sk4_decl,type,
sk4: $o ).
thf(sk5_decl,type,
sk5: '$world' ).
thf(sk6_decl,type,
sk6: '$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' > '$world' ).
thf(sk11_decl,type,
sk11: $o ).
thf(sk12_decl,type,
sk12: $o ).
thf(sk13_decl,type,
sk13: '$world' ).
thf(sk14_decl,type,
sk14: $o ).
thf(sk15_decl,type,
sk15: '$world' ).
thf(sk16_decl,type,
sk16: '$world' ).
thf(sk17_decl,type,
sk17: '$world' ).
thf(sk18_decl,type,
sk18: '$world' ).
thf(sk19_decl,type,
sk19: '$world' > '$world' ).
thf(sk20_decl,type,
sk20: '$world' > '$world' ).
thf(sk21_decl,type,
sk21: $o ).
thf(sk22_decl,type,
sk22: $o ).
thf(sk23_decl,type,
sk23: '$world' ).
thf(sk24_decl,type,
sk24: $o ).
thf(sk25_decl,type,
sk25: '$world' ).
thf(sk26_decl,type,
sk26: '$world' ).
thf(sk27_decl,type,
sk27: '$world' ).
thf(sk28_decl,type,
sk28: '$world' ).
thf(sk29_decl,type,
sk29: '$world' > '$world' ).
thf(sk30_decl,type,
sk30: '$world' > '$world' ).
thf(sk31_decl,type,
sk31: '$world' ).
thf(sk32_decl,type,
sk32: '$world' ).
thf(sk33_decl,type,
sk33: $o ).
thf(sk34_decl,type,
sk34: $o ).
thf(sk35_decl,type,
sk35: '$world' ).
thf(sk36_decl,type,
sk36: $o ).
thf(sk37_decl,type,
sk37: '$world' ).
thf(sk38_decl,type,
sk38: '$world' ).
thf(sk39_decl,type,
sk39: '$world' ).
thf(sk40_decl,type,
sk40: '$world' ).
thf(sk41_decl,type,
sk41: '$world' > '$world' ).
thf(sk42_decl,type,
sk42: '$world' > '$world' ).
thf(sk43_decl,type,
sk43: $o ).
thf(sk44_decl,type,
sk44: $o ).
thf(sk45_decl,type,
sk45: '$world' ).
thf(sk46_decl,type,
sk46: $o ).
thf(sk47_decl,type,
sk47: '$world' ).
thf(sk48_decl,type,
sk48: '$world' ).
thf(sk49_decl,type,
sk49: '$world' ).
thf(sk50_decl,type,
sk50: '$world' ).
thf(sk51_decl,type,
sk51: '$world' > '$world' ).
thf(sk52_decl,type,
sk52: '$world' > '$world' ).
thf(sk53_decl,type,
sk53: $o ).
thf(sk54_decl,type,
sk54: $o ).
thf(sk55_decl,type,
sk55: '$world' ).
thf(sk56_decl,type,
sk56: $o ).
thf(sk57_decl,type,
sk57: '$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' > '$world' ).
thf(sk62_decl,type,
sk62: '$world' > '$world' ).
thf(sk63_decl,type,
sk63: $o ).
thf(sk64_decl,type,
sk64: $o ).
thf(sk65_decl,type,
sk65: '$world' ).
thf(sk66_decl,type,
sk66: $o ).
thf(sk67_decl,type,
sk67: '$world' ).
thf(sk68_decl,type,
sk68: '$world' ).
thf(sk69_decl,type,
sk69: '$world' ).
thf(sk70_decl,type,
sk70: '$world' ).
thf(sk71_decl,type,
sk71: '$world' > '$world' ).
thf(sk72_decl,type,
sk72: '$world' > '$world' ).
thf(sk73_decl,type,
sk73: $o ).
thf(sk74_decl,type,
sk74: $o ).
thf(sk75_decl,type,
sk75: '$world' ).
thf(sk76_decl,type,
sk76: $o ).
thf(sk77_decl,type,
sk77: '$world' ).
thf(sk78_decl,type,
sk78: '$world' ).
thf(sk79_decl,type,
sk79: '$world' ).
thf(sk80_decl,type,
sk80: '$world' ).
thf(sk81_decl,type,
sk81: '$world' > '$world' ).
thf(sk82_decl,type,
sk82: '$world' > '$world' ).
thf(sk83_decl,type,
sk83: $o ).
thf(sk84_decl,type,
sk84: $o ).
thf(sk85_decl,type,
sk85: '$world' ).
thf(sk86_decl,type,
sk86: $o ).
thf(sk87_decl,type,
sk87: '$world' ).
thf(sk88_decl,type,
sk88: '$world' ).
thf(sk89_decl,type,
sk89: '$world' ).
thf(sk90_decl,type,
sk90: '$world' ).
thf(sk91_decl,type,
sk91: '$world' > '$world' ).
thf(sk92_decl,type,
sk92: '$world' > '$world' ).
thf(sk93_decl,type,
sk93: $o ).
thf(sk94_decl,type,
sk94: $o ).
thf(sk95_decl,type,
sk95: '$world' ).
thf(sk96_decl,type,
sk96: $o ).
thf(sk97_decl,type,
sk97: '$world' ).
thf(sk98_decl,type,
sk98: '$world' ).
thf(sk99_decl,type,
sk99: '$world' ).
thf(sk100_decl,type,
sk100: '$world' ).
thf(sk101_decl,type,
sk101: '$world' > '$world' ).
thf(sk102_decl,type,
sk102: '$world' > '$world' ).
thf(sk3_def,definition,
( sk3
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) )
& ( B @ p1 ) )
=> ( B @ p2 ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: '$world'] :
~ ( ( A @ ( sk5 @ '$accessible_world' ) )
=> ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p1 )
=> ~ ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: '$world'] :
~ ( ( A @ ( sk7 @ '$accessible_world' ) )
=> ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) )
& ( B @ p2 ) )
=> ( B @ p3 ) ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( @+[A: '$world'] :
~ ( ( A @ ( sk15 @ '$accessible_world' ) )
=> ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p2 )
=> ~ ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: '$world'] :
~ ( ( A @ ( sk17 @ '$accessible_world' ) )
=> ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) ).
thf(sk23_def,definition,
( sk23
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) ) ) ).
thf(sk25_def,definition,
( sk25
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) )
& ( B @ p3 ) )
=> ( B @ p4 ) ) ) ) ) ) ) ).
thf(sk26_def,definition,
( sk26
= ( @+[A: '$world'] :
~ ( ( A @ ( sk25 @ '$accessible_world' ) )
=> ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) ) ).
thf(sk27_def,definition,
( sk27
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p3 )
=> ~ ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) ) ) ).
thf(sk28_def,definition,
( sk28
= ( @+[A: '$world'] :
~ ( ( A @ ( sk27 @ '$accessible_world' ) )
=> ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) ) ) ) ).
thf(sk29_def,definition,
( sk29
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) ).
thf(sk30_def,definition,
( sk30
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) ).
thf(sk31_def,definition,
( sk31
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) ) ) ) ).
thf(sk32_def,definition,
( sk32
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) ) ) ) ).
thf(sk35_def,definition,
( sk35
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) ) ) ).
thf(sk37_def,definition,
( sk37
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) )
& ( B @ p4 ) )
=> ( B @ p5 ) ) ) ) ) ) ) ).
thf(sk38_def,definition,
( sk38
= ( @+[A: '$world'] :
~ ( ( A @ ( sk37 @ '$accessible_world' ) )
=> ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p4 )
=> ~ ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) ) ) ).
thf(sk40_def,definition,
( sk40
= ( @+[A: '$world'] :
~ ( ( A @ ( sk39 @ '$accessible_world' ) )
=> ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) ) ) ) ).
thf(sk41_def,definition,
( sk41
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) ).
thf(sk45_def,definition,
( sk45
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) ) ) ).
thf(sk47_def,definition,
( sk47
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) )
& ( B @ p5 ) )
=> ( B @ p6 ) ) ) ) ) ) ) ).
thf(sk48_def,definition,
( sk48
= ( @+[A: '$world'] :
~ ( ( A @ ( sk47 @ '$accessible_world' ) )
=> ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) ) ).
thf(sk49_def,definition,
( sk49
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p5 )
=> ~ ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) ) ) ).
thf(sk50_def,definition,
( sk50
= ( @+[A: '$world'] :
~ ( ( A @ ( sk49 @ '$accessible_world' ) )
=> ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) ) ) ) ).
thf(sk51_def,definition,
( sk51
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) ).
thf(sk52_def,definition,
( sk52
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) ).
thf(sk55_def,definition,
( sk55
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) ) ) ).
thf(sk57_def,definition,
( sk57
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) )
& ( B @ p6 ) )
=> ( B @ p7 ) ) ) ) ) ) ) ).
thf(sk58_def,definition,
( sk58
= ( @+[A: '$world'] :
~ ( ( A @ ( sk57 @ '$accessible_world' ) )
=> ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) ) ).
thf(sk59_def,definition,
( sk59
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p6 )
=> ~ ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) ) ) ).
thf(sk60_def,definition,
( sk60
= ( @+[A: '$world'] :
~ ( ( A @ ( sk59 @ '$accessible_world' ) )
=> ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) ) ) ) ).
thf(sk61_def,definition,
( sk61
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) ).
thf(sk62_def,definition,
( sk62
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) ).
thf(sk65_def,definition,
( sk65
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) ) ) ).
thf(sk67_def,definition,
( sk67
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) )
& ( B @ p7 ) )
=> ( B @ p8 ) ) ) ) ) ) ) ).
thf(sk68_def,definition,
( sk68
= ( @+[A: '$world'] :
~ ( ( A @ ( sk67 @ '$accessible_world' ) )
=> ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) ) ).
thf(sk69_def,definition,
( sk69
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p7 )
=> ~ ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) ) ) ).
thf(sk70_def,definition,
( sk70
= ( @+[A: '$world'] :
~ ( ( A @ ( sk69 @ '$accessible_world' ) )
=> ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) ) ) ) ).
thf(sk71_def,definition,
( sk71
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) ).
thf(sk72_def,definition,
( sk72
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) ).
thf(sk75_def,definition,
( sk75
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) ) ) ).
thf(sk77_def,definition,
( sk77
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) )
& ( B @ p8 ) )
=> ( B @ p9 ) ) ) ) ) ) ) ).
thf(sk78_def,definition,
( sk78
= ( @+[A: '$world'] :
~ ( ( A @ ( sk77 @ '$accessible_world' ) )
=> ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) ) ).
thf(sk79_def,definition,
( sk79
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p8 )
=> ~ ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) ) ) ).
thf(sk80_def,definition,
( sk80
= ( @+[A: '$world'] :
~ ( ( A @ ( sk79 @ '$accessible_world' ) )
=> ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) ) ) ) ).
thf(sk81_def,definition,
( sk81
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) ).
thf(sk82_def,definition,
( sk82
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) ).
thf(sk85_def,definition,
( sk85
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) ) ) ).
thf(sk87_def,definition,
( sk87
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) )
& ( B @ p9 ) )
=> ( B @ p10 ) ) ) ) ) ) ) ).
thf(sk88_def,definition,
( sk88
= ( @+[A: '$world'] :
~ ( ( A @ ( sk87 @ '$accessible_world' ) )
=> ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) ) ).
thf(sk89_def,definition,
( sk89
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p9 )
=> ~ ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) ) ) ).
thf(sk90_def,definition,
( sk90
= ( @+[A: '$world'] :
~ ( ( A @ ( sk89 @ '$accessible_world' ) )
=> ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) ) ) ) ).
thf(sk91_def,definition,
( sk91
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) ).
thf(sk92_def,definition,
( sk92
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) ).
thf(sk95_def,definition,
( sk95
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) ) ) ).
thf(sk97_def,definition,
( sk97
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) )
& ( B @ p10 ) )
=> ( B @ p11 ) ) ) ) ) ) ) ).
thf(sk98_def,definition,
( sk98
= ( @+[A: '$world'] :
~ ( ( A @ ( sk97 @ '$accessible_world' ) )
=> ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) ) ).
thf(sk99_def,definition,
( sk99
= ( @+[A: '$world'] :
~ ( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p10 )
=> ~ ( ( B @ p11 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p11 ) ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) ) ) ).
thf(sk100_def,definition,
( sk100
= ( @+[A: '$world'] :
~ ( ( A @ ( sk99 @ '$accessible_world' ) )
=> ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) ) ) ) ) ).
thf(sk101_def,definition,
( sk101
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) ).
thf(sk102_def,definition,
( sk102
= ( ^ [A: '$world'] :
@+[B: '$world'] :
~ ( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) ) ).
thf(1,conjecture,
( ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p10 )
=> ~ ( ( B @ p11 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p11 ) ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) )
& ( B @ p10 ) )
=> ( B @ p11 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p9 )
=> ~ ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) )
& ( B @ p9 ) )
=> ( B @ p10 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p8 )
=> ~ ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) )
& ( B @ p8 ) )
=> ( B @ p9 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p7 )
=> ~ ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) )
& ( B @ p7 ) )
=> ( B @ p8 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p6 )
=> ~ ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) )
& ( B @ p6 ) )
=> ( B @ p7 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p5 )
=> ~ ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) )
& ( B @ p5 ) )
=> ( B @ p6 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p4 )
=> ~ ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) )
& ( B @ p4 ) )
=> ( B @ p5 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p3 )
=> ~ ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) )
& ( B @ p3 ) )
=> ( B @ p4 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p2 )
=> ~ ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) )
& ( B @ p2 ) )
=> ( B @ p3 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p1 )
=> ~ ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) )
& ( B @ p1 ) )
=> ( B @ p2 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ),
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' ) )
=> ( ~ ( B @ p10 )
=> ~ ( ( B @ p11 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p11 ) ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) )
& ( B @ p10 ) )
=> ( B @ p11 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p9 )
=> ~ ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) )
& ( B @ p9 ) )
=> ( B @ p10 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p8 )
=> ~ ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) )
& ( B @ p8 ) )
=> ( B @ p9 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p7 )
=> ~ ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) )
& ( B @ p7 ) )
=> ( B @ p8 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p6 )
=> ~ ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) )
& ( B @ p6 ) )
=> ( B @ p7 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p5 )
=> ~ ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) )
& ( B @ p5 ) )
=> ( B @ p6 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p4 )
=> ~ ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) )
& ( B @ p4 ) )
=> ( B @ p5 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p3 )
=> ~ ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) )
& ( B @ p3 ) )
=> ( B @ p4 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p2 )
=> ~ ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) )
& ( B @ p2 ) )
=> ( B @ p3 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p1 )
=> ~ ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) )
& ( B @ p1 ) )
=> ( B @ p2 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p10 )
=> ~ ( ( B @ p11 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p11 ) ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) )
& ( B @ p10 ) )
=> ( B @ p11 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) )
| ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p10 )
=> ~ ( ( A @ p11 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p11 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p11 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p9 )
=> ~ ( ( B @ p10 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p10 ) ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) )
& ( B @ p9 ) )
=> ( B @ p10 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) )
| ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p9 )
=> ~ ( ( A @ p10 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) )
& ( A @ p9 ) )
=> ( A @ p10 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p8 )
=> ~ ( ( B @ p9 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p9 ) ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) )
& ( B @ p8 ) )
=> ( B @ p9 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) )
| ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p8 )
=> ~ ( ( A @ p9 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p9 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) )
& ( A @ p8 ) )
=> ( A @ p9 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p7 )
=> ~ ( ( B @ p8 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p8 ) ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) )
& ( B @ p7 ) )
=> ( B @ p8 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) )
| ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p7 )
=> ~ ( ( A @ p8 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p8 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) )
& ( A @ p7 ) )
=> ( A @ p8 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p6 )
=> ~ ( ( B @ p7 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p7 ) ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) )
& ( B @ p6 ) )
=> ( B @ p7 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) )
| ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p6 )
=> ~ ( ( A @ p7 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p7 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) )
& ( A @ p6 ) )
=> ( A @ p7 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p5 )
=> ~ ( ( B @ p6 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p6 ) ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) )
& ( B @ p5 ) )
=> ( B @ p6 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) )
| ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p5 )
=> ~ ( ( A @ p6 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p6 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) )
& ( A @ p5 ) )
=> ( A @ p6 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p4 )
=> ~ ( ( B @ p5 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p5 ) ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) )
& ( B @ p4 ) )
=> ( B @ p5 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) )
| ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p4 )
=> ~ ( ( A @ p5 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) )
& ( A @ p4 ) )
=> ( A @ p5 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p10 ) )
& ( A @ p10 ) )
=> ( A @ p10 ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p3 )
=> ~ ( ( B @ p4 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p4 ) ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) )
& ( B @ p3 ) )
=> ( B @ p4 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) )
| ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p3 )
=> ~ ( ( A @ p4 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p4 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) )
& ( A @ p3 ) )
=> ( A @ p4 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p2 )
=> ~ ( ( B @ p3 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p3 ) ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) )
& ( B @ p2 ) )
=> ( B @ p3 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) )
| ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p2 )
=> ~ ( ( A @ p3 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p3 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) )
& ( A @ p2 ) )
=> ( A @ p3 ) ) ) ) )
| ~ ( ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ~ ( B @ p1 )
=> ~ ( ( B @ p2 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p2 ) ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( ( ( B @ p1 )
& ! [C: '$world'] :
( ( C @ ( B @ '$accessible_world' ) )
=> ( C @ p1 ) )
& ( B @ p1 ) )
=> ( B @ p2 ) ) ) ) )
& ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) )
| ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) )
=> ( ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ~ ( A @ p1 )
=> ~ ( ( A @ p2 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p2 ) ) ) ) )
| ! [A: '$world'] :
( ( A @ ( '$local_world' @ '$accessible_world' ) )
=> ( ( ( A @ p1 )
& ! [B: '$world'] :
( ( B @ ( A @ '$accessible_world' ) )
=> ( B @ p1 ) )
& ( A @ p1 ) )
=> ( A @ p2 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [ZZZD: '$world',ZZZC: '$world',ZZZB: '$world',ZZZA: '$world',ZZZ: '$world',ZZY: '$world',ZZX: '$world',ZZW: '$world',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'] :
( ( ~ ( ZZZD @ p11 )
| ~ ( ZZZD @ sk102 @ p11 )
| ( ZZZD @ p10 )
| ~ ( ZZZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZZC @ p11 )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ sk101 @ p10 )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk93 )
& ( ~ ( ZZZD @ p11 )
| ( ZZZD @ sk102 @ ( ZZZD @ '$accessible_world' ) )
| ( ZZZD @ p10 )
| ~ ( ZZZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZZC @ p11 )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ sk101 @ p10 )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk93 )
& ( ~ ( ZZZD @ p11 )
| ~ ( ZZZD @ sk102 @ p11 )
| ( ZZZD @ p10 )
| ~ ( ZZZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZZC @ p11 )
| ~ ( ZZZC @ p10 )
| ( ZZZC @ sk101 @ ( ZZZC @ '$accessible_world' ) )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk93 )
& ( ~ ( ZZZD @ p11 )
| ( ZZZD @ sk102 @ ( ZZZD @ '$accessible_world' ) )
| ( ZZZD @ p10 )
| ~ ( ZZZD @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZZC @ p11 )
| ~ ( ZZZC @ p10 )
| ( ZZZC @ sk101 @ ( ZZZC @ '$accessible_world' ) )
| ~ ( ZZZC @ p10 )
| ~ ( ZZZC @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk93 )
& ( sk93
| ( sk100 @ p11 )
| sk96
| sk94 )
& ( sk93
| ( ZZZB @ p11 )
| ~ ( ZZZB @ ( sk100 @ '$accessible_world' ) )
| sk96
| sk94 )
& ( sk93
| ~ ( sk100 @ p10 )
| sk96
| sk94 )
& ( sk93
| ( sk100 @ ( sk99 @ '$accessible_world' ) )
| sk96
| sk94 )
& ( sk93
| ~ ( sk99 @ p11 )
| sk96
| sk94 )
& ( sk93
| ( sk99 @ p10 )
| sk96
| sk94 )
& ( sk93
| ( ZZZA @ p10 )
| ~ ( ZZZA @ ( sk99 @ '$accessible_world' ) )
| sk96
| sk94 )
& ( sk93
| ( sk99 @ p10 )
| sk96
| sk94 )
& ( sk93
| ( sk99 @ ( '$local_world' @ '$accessible_world' ) )
| sk96
| sk94 )
& ( sk93
| ~ sk96
| ( sk97 @ p11 )
| sk94 )
& ( sk93
| ~ sk96
| ( ZZZ @ p11 )
| ~ ( ZZZ @ ( sk97 @ '$accessible_world' ) )
| sk94 )
& ( sk93
| ~ sk96
| ~ ( sk97 @ p10 )
| sk94 )
& ( sk93
| ~ sk96
| ~ ( sk98 @ p11 )
| sk94 )
& ( sk93
| ~ sk96
| ( sk98 @ p10 )
| sk94 )
& ( sk93
| ~ sk96
| ( ZZY @ p10 )
| ~ ( ZZY @ ( sk98 @ '$accessible_world' ) )
| sk94 )
& ( sk93
| ~ sk96
| ( sk98 @ p10 )
| sk94 )
& ( sk93
| ~ sk96
| ( sk98 @ ( sk97 @ '$accessible_world' ) )
| sk94 )
& ( sk93
| ~ sk96
| ( sk97 @ ( '$local_world' @ '$accessible_world' ) )
| sk94 )
& ( sk93
| ~ sk94
| ( sk95 @ p11 ) )
& ( sk93
| ~ sk94
| ( ZZX @ p11 )
| ~ ( ZZX @ ( sk95 @ '$accessible_world' ) ) )
& ( sk93
| ~ sk94
| ~ ( sk95 @ p10 ) )
& ( sk93
| ~ sk94
| ~ ( sk95 @ p11 ) )
& ( sk93
| ~ sk94
| ( sk95 @ p10 ) )
& ( sk93
| ~ sk94
| ( ZZW @ p10 )
| ~ ( ZZW @ ( sk95 @ '$accessible_world' ) ) )
& ( sk93
| ~ sk94
| ( sk95 @ p10 ) )
& ( sk93
| ~ sk94
| ( sk95 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZZV @ p10 )
| ~ ( ZZV @ sk92 @ p10 )
| ( ZZV @ p9 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZU @ p10 )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ sk91 @ p9 )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk83 )
& ( ~ ( ZZV @ p10 )
| ( ZZV @ sk92 @ ( ZZV @ '$accessible_world' ) )
| ( ZZV @ p9 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZU @ p10 )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ sk91 @ p9 )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk83 )
& ( ~ ( ZZV @ p10 )
| ~ ( ZZV @ sk92 @ p10 )
| ( ZZV @ p9 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZU @ p10 )
| ~ ( ZZU @ p9 )
| ( ZZU @ sk91 @ ( ZZU @ '$accessible_world' ) )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk83 )
& ( ~ ( ZZV @ p10 )
| ( ZZV @ sk92 @ ( ZZV @ '$accessible_world' ) )
| ( ZZV @ p9 )
| ~ ( ZZV @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZU @ p10 )
| ~ ( ZZU @ p9 )
| ( ZZU @ sk91 @ ( ZZU @ '$accessible_world' ) )
| ~ ( ZZU @ p9 )
| ~ ( ZZU @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk83 )
& ( sk83
| ( sk90 @ p10 )
| sk86
| sk84 )
& ( sk83
| ( ZZT @ p10 )
| ~ ( ZZT @ ( sk90 @ '$accessible_world' ) )
| sk86
| sk84 )
& ( sk83
| ~ ( sk90 @ p9 )
| sk86
| sk84 )
& ( sk83
| ( sk90 @ ( sk89 @ '$accessible_world' ) )
| sk86
| sk84 )
& ( sk83
| ~ ( sk89 @ p10 )
| sk86
| sk84 )
& ( sk83
| ( sk89 @ p9 )
| sk86
| sk84 )
& ( sk83
| ( ZZS @ p9 )
| ~ ( ZZS @ ( sk89 @ '$accessible_world' ) )
| sk86
| sk84 )
& ( sk83
| ( sk89 @ p9 )
| sk86
| sk84 )
& ( sk83
| ( sk89 @ ( '$local_world' @ '$accessible_world' ) )
| sk86
| sk84 )
& ( sk83
| ~ sk86
| ( sk87 @ p10 )
| sk84 )
& ( sk83
| ~ sk86
| ( ZZR @ p10 )
| ~ ( ZZR @ ( sk87 @ '$accessible_world' ) )
| sk84 )
& ( sk83
| ~ sk86
| ~ ( sk87 @ p9 )
| sk84 )
& ( sk83
| ~ sk86
| ~ ( sk88 @ p10 )
| sk84 )
& ( sk83
| ~ sk86
| ( sk88 @ p9 )
| sk84 )
& ( sk83
| ~ sk86
| ( ZZQ @ p9 )
| ~ ( ZZQ @ ( sk88 @ '$accessible_world' ) )
| sk84 )
& ( sk83
| ~ sk86
| ( sk88 @ p9 )
| sk84 )
& ( sk83
| ~ sk86
| ( sk88 @ ( sk87 @ '$accessible_world' ) )
| sk84 )
& ( sk83
| ~ sk86
| ( sk87 @ ( '$local_world' @ '$accessible_world' ) )
| sk84 )
& ( sk83
| ~ sk84
| ( sk85 @ p10 ) )
& ( sk83
| ~ sk84
| ( ZZP @ p10 )
| ~ ( ZZP @ ( sk85 @ '$accessible_world' ) ) )
& ( sk83
| ~ sk84
| ~ ( sk85 @ p9 ) )
& ( sk83
| ~ sk84
| ~ ( sk85 @ p10 ) )
& ( sk83
| ~ sk84
| ( sk85 @ p9 ) )
& ( sk83
| ~ sk84
| ( ZZO @ p9 )
| ~ ( ZZO @ ( sk85 @ '$accessible_world' ) ) )
& ( sk83
| ~ sk84
| ( sk85 @ p9 ) )
& ( sk83
| ~ sk84
| ( sk85 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZZN @ p9 )
| ~ ( ZZN @ sk82 @ p9 )
| ( ZZN @ p8 )
| ~ ( ZZN @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZM @ p9 )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ sk81 @ p8 )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk73 )
& ( ~ ( ZZN @ p9 )
| ( ZZN @ sk82 @ ( ZZN @ '$accessible_world' ) )
| ( ZZN @ p8 )
| ~ ( ZZN @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZM @ p9 )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ sk81 @ p8 )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk73 )
& ( ~ ( ZZN @ p9 )
| ~ ( ZZN @ sk82 @ p9 )
| ( ZZN @ p8 )
| ~ ( ZZN @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZM @ p9 )
| ~ ( ZZM @ p8 )
| ( ZZM @ sk81 @ ( ZZM @ '$accessible_world' ) )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk73 )
& ( ~ ( ZZN @ p9 )
| ( ZZN @ sk82 @ ( ZZN @ '$accessible_world' ) )
| ( ZZN @ p8 )
| ~ ( ZZN @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZM @ p9 )
| ~ ( ZZM @ p8 )
| ( ZZM @ sk81 @ ( ZZM @ '$accessible_world' ) )
| ~ ( ZZM @ p8 )
| ~ ( ZZM @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk73 )
& ( sk73
| ( sk80 @ p9 )
| sk76
| sk74 )
& ( sk73
| ( ZZL @ p9 )
| ~ ( ZZL @ ( sk80 @ '$accessible_world' ) )
| sk76
| sk74 )
& ( sk73
| ~ ( sk80 @ p8 )
| sk76
| sk74 )
& ( sk73
| ( sk80 @ ( sk79 @ '$accessible_world' ) )
| sk76
| sk74 )
& ( sk73
| ~ ( sk79 @ p9 )
| sk76
| sk74 )
& ( sk73
| ( sk79 @ p8 )
| sk76
| sk74 )
& ( sk73
| ( ZZK @ p8 )
| ~ ( ZZK @ ( sk79 @ '$accessible_world' ) )
| sk76
| sk74 )
& ( sk73
| ( sk79 @ p8 )
| sk76
| sk74 )
& ( sk73
| ( sk79 @ ( '$local_world' @ '$accessible_world' ) )
| sk76
| sk74 )
& ( sk73
| ~ sk76
| ( sk77 @ p9 )
| sk74 )
& ( sk73
| ~ sk76
| ( ZZJ @ p9 )
| ~ ( ZZJ @ ( sk77 @ '$accessible_world' ) )
| sk74 )
& ( sk73
| ~ sk76
| ~ ( sk77 @ p8 )
| sk74 )
& ( sk73
| ~ sk76
| ~ ( sk78 @ p9 )
| sk74 )
& ( sk73
| ~ sk76
| ( sk78 @ p8 )
| sk74 )
& ( sk73
| ~ sk76
| ( ZZI @ p8 )
| ~ ( ZZI @ ( sk78 @ '$accessible_world' ) )
| sk74 )
& ( sk73
| ~ sk76
| ( sk78 @ p8 )
| sk74 )
& ( sk73
| ~ sk76
| ( sk78 @ ( sk77 @ '$accessible_world' ) )
| sk74 )
& ( sk73
| ~ sk76
| ( sk77 @ ( '$local_world' @ '$accessible_world' ) )
| sk74 )
& ( sk73
| ~ sk74
| ( sk75 @ p9 ) )
& ( sk73
| ~ sk74
| ( ZZH @ p9 )
| ~ ( ZZH @ ( sk75 @ '$accessible_world' ) ) )
& ( sk73
| ~ sk74
| ~ ( sk75 @ p8 ) )
& ( sk73
| ~ sk74
| ~ ( sk75 @ p9 ) )
& ( sk73
| ~ sk74
| ( sk75 @ p8 ) )
& ( sk73
| ~ sk74
| ( ZZG @ p8 )
| ~ ( ZZG @ ( sk75 @ '$accessible_world' ) ) )
& ( sk73
| ~ sk74
| ( sk75 @ p8 ) )
& ( sk73
| ~ sk74
| ( sk75 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZZF @ p8 )
| ~ ( ZZF @ sk72 @ p8 )
| ( ZZF @ p7 )
| ~ ( ZZF @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZE @ p8 )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ sk71 @ p7 )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk63 )
& ( ~ ( ZZF @ p8 )
| ( ZZF @ sk72 @ ( ZZF @ '$accessible_world' ) )
| ( ZZF @ p7 )
| ~ ( ZZF @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZE @ p8 )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ sk71 @ p7 )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk63 )
& ( ~ ( ZZF @ p8 )
| ~ ( ZZF @ sk72 @ p8 )
| ( ZZF @ p7 )
| ~ ( ZZF @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZE @ p8 )
| ~ ( ZZE @ p7 )
| ( ZZE @ sk71 @ ( ZZE @ '$accessible_world' ) )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk63 )
& ( ~ ( ZZF @ p8 )
| ( ZZF @ sk72 @ ( ZZF @ '$accessible_world' ) )
| ( ZZF @ p7 )
| ~ ( ZZF @ ( '$local_world' @ '$accessible_world' ) )
| ( ZZE @ p8 )
| ~ ( ZZE @ p7 )
| ( ZZE @ sk71 @ ( ZZE @ '$accessible_world' ) )
| ~ ( ZZE @ p7 )
| ~ ( ZZE @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk63 )
& ( sk63
| ( sk70 @ p8 )
| sk66
| sk64 )
& ( sk63
| ( ZZD @ p8 )
| ~ ( ZZD @ ( sk70 @ '$accessible_world' ) )
| sk66
| sk64 )
& ( sk63
| ~ ( sk70 @ p7 )
| sk66
| sk64 )
& ( sk63
| ( sk70 @ ( sk69 @ '$accessible_world' ) )
| sk66
| sk64 )
& ( sk63
| ~ ( sk69 @ p8 )
| sk66
| sk64 )
& ( sk63
| ( sk69 @ p7 )
| sk66
| sk64 )
& ( sk63
| ( ZZC @ p7 )
| ~ ( ZZC @ ( sk69 @ '$accessible_world' ) )
| sk66
| sk64 )
& ( sk63
| ( sk69 @ p7 )
| sk66
| sk64 )
& ( sk63
| ( sk69 @ ( '$local_world' @ '$accessible_world' ) )
| sk66
| sk64 )
& ( sk63
| ~ sk66
| ( sk67 @ p8 )
| sk64 )
& ( sk63
| ~ sk66
| ( ZZB @ p8 )
| ~ ( ZZB @ ( sk67 @ '$accessible_world' ) )
| sk64 )
& ( sk63
| ~ sk66
| ~ ( sk67 @ p7 )
| sk64 )
& ( sk63
| ~ sk66
| ~ ( sk68 @ p8 )
| sk64 )
& ( sk63
| ~ sk66
| ( sk68 @ p7 )
| sk64 )
& ( sk63
| ~ sk66
| ( ZZA @ p7 )
| ~ ( ZZA @ ( sk68 @ '$accessible_world' ) )
| sk64 )
& ( sk63
| ~ sk66
| ( sk68 @ p7 )
| sk64 )
& ( sk63
| ~ sk66
| ( sk68 @ ( sk67 @ '$accessible_world' ) )
| sk64 )
& ( sk63
| ~ sk66
| ( sk67 @ ( '$local_world' @ '$accessible_world' ) )
| sk64 )
& ( sk63
| ~ sk64
| ( sk65 @ p8 ) )
& ( sk63
| ~ sk64
| ( ZZ @ p8 )
| ~ ( ZZ @ ( sk65 @ '$accessible_world' ) ) )
& ( sk63
| ~ sk64
| ~ ( sk65 @ p7 ) )
& ( sk63
| ~ sk64
| ~ ( sk65 @ p8 ) )
& ( sk63
| ~ sk64
| ( sk65 @ p7 ) )
& ( sk63
| ~ sk64
| ( ZY @ p7 )
| ~ ( ZY @ ( sk65 @ '$accessible_world' ) ) )
& ( sk63
| ~ sk64
| ( sk65 @ p7 ) )
& ( sk63
| ~ sk64
| ( sk65 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZX @ p7 )
| ~ ( ZX @ sk62 @ p7 )
| ( ZX @ p6 )
| ~ ( ZX @ ( '$local_world' @ '$accessible_world' ) )
| ( ZW @ p7 )
| ~ ( ZW @ p6 )
| ~ ( ZW @ sk61 @ p6 )
| ~ ( ZW @ p6 )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk53 )
& ( ~ ( ZX @ p7 )
| ( ZX @ sk62 @ ( ZX @ '$accessible_world' ) )
| ( ZX @ p6 )
| ~ ( ZX @ ( '$local_world' @ '$accessible_world' ) )
| ( ZW @ p7 )
| ~ ( ZW @ p6 )
| ~ ( ZW @ sk61 @ p6 )
| ~ ( ZW @ p6 )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk53 )
& ( ~ ( ZX @ p7 )
| ~ ( ZX @ sk62 @ p7 )
| ( ZX @ p6 )
| ~ ( ZX @ ( '$local_world' @ '$accessible_world' ) )
| ( ZW @ p7 )
| ~ ( ZW @ p6 )
| ( ZW @ sk61 @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ p6 )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk53 )
& ( ~ ( ZX @ p7 )
| ( ZX @ sk62 @ ( ZX @ '$accessible_world' ) )
| ( ZX @ p6 )
| ~ ( ZX @ ( '$local_world' @ '$accessible_world' ) )
| ( ZW @ p7 )
| ~ ( ZW @ p6 )
| ( ZW @ sk61 @ ( ZW @ '$accessible_world' ) )
| ~ ( ZW @ p6 )
| ~ ( ZW @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk53 )
& ( sk53
| ( sk60 @ p7 )
| sk56
| sk54 )
& ( sk53
| ( ZV @ p7 )
| ~ ( ZV @ ( sk60 @ '$accessible_world' ) )
| sk56
| sk54 )
& ( sk53
| ~ ( sk60 @ p6 )
| sk56
| sk54 )
& ( sk53
| ( sk60 @ ( sk59 @ '$accessible_world' ) )
| sk56
| sk54 )
& ( sk53
| ~ ( sk59 @ p7 )
| sk56
| sk54 )
& ( sk53
| ( sk59 @ p6 )
| sk56
| sk54 )
& ( sk53
| ( ZU @ p6 )
| ~ ( ZU @ ( sk59 @ '$accessible_world' ) )
| sk56
| sk54 )
& ( sk53
| ( sk59 @ p6 )
| sk56
| sk54 )
& ( sk53
| ( sk59 @ ( '$local_world' @ '$accessible_world' ) )
| sk56
| sk54 )
& ( sk53
| ~ sk56
| ( sk57 @ p7 )
| sk54 )
& ( sk53
| ~ sk56
| ( ZT @ p7 )
| ~ ( ZT @ ( sk57 @ '$accessible_world' ) )
| sk54 )
& ( sk53
| ~ sk56
| ~ ( sk57 @ p6 )
| sk54 )
& ( sk53
| ~ sk56
| ~ ( sk58 @ p7 )
| sk54 )
& ( sk53
| ~ sk56
| ( sk58 @ p6 )
| sk54 )
& ( sk53
| ~ sk56
| ( ZS @ p6 )
| ~ ( ZS @ ( sk58 @ '$accessible_world' ) )
| sk54 )
& ( sk53
| ~ sk56
| ( sk58 @ p6 )
| sk54 )
& ( sk53
| ~ sk56
| ( sk58 @ ( sk57 @ '$accessible_world' ) )
| sk54 )
& ( sk53
| ~ sk56
| ( sk57 @ ( '$local_world' @ '$accessible_world' ) )
| sk54 )
& ( sk53
| ~ sk54
| ( sk55 @ p7 ) )
& ( sk53
| ~ sk54
| ( ZR @ p7 )
| ~ ( ZR @ ( sk55 @ '$accessible_world' ) ) )
& ( sk53
| ~ sk54
| ~ ( sk55 @ p6 ) )
& ( sk53
| ~ sk54
| ~ ( sk55 @ p7 ) )
& ( sk53
| ~ sk54
| ( sk55 @ p6 ) )
& ( sk53
| ~ sk54
| ( ZQ @ p6 )
| ~ ( ZQ @ ( sk55 @ '$accessible_world' ) ) )
& ( sk53
| ~ sk54
| ( sk55 @ p6 ) )
& ( sk53
| ~ sk54
| ( sk55 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZP @ p6 )
| ~ ( ZP @ sk52 @ p6 )
| ( ZP @ p5 )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZO @ p6 )
| ~ ( ZO @ p5 )
| ~ ( ZO @ sk51 @ p5 )
| ~ ( ZO @ p5 )
| ~ ( ZO @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk43 )
& ( ~ ( ZP @ p6 )
| ( ZP @ sk52 @ ( ZP @ '$accessible_world' ) )
| ( ZP @ p5 )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZO @ p6 )
| ~ ( ZO @ p5 )
| ~ ( ZO @ sk51 @ p5 )
| ~ ( ZO @ p5 )
| ~ ( ZO @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk43 )
& ( ~ ( ZP @ p6 )
| ~ ( ZP @ sk52 @ p6 )
| ( ZP @ p5 )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZO @ p6 )
| ~ ( ZO @ p5 )
| ( ZO @ sk51 @ ( ZO @ '$accessible_world' ) )
| ~ ( ZO @ p5 )
| ~ ( ZO @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk43 )
& ( ~ ( ZP @ p6 )
| ( ZP @ sk52 @ ( ZP @ '$accessible_world' ) )
| ( ZP @ p5 )
| ~ ( ZP @ ( '$local_world' @ '$accessible_world' ) )
| ( ZO @ p6 )
| ~ ( ZO @ p5 )
| ( ZO @ sk51 @ ( ZO @ '$accessible_world' ) )
| ~ ( ZO @ p5 )
| ~ ( ZO @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk43 )
& ( sk43
| ( sk50 @ p6 )
| sk46
| sk44 )
& ( sk43
| ( ZN @ p6 )
| ~ ( ZN @ ( sk50 @ '$accessible_world' ) )
| sk46
| sk44 )
& ( sk43
| ~ ( sk50 @ p5 )
| sk46
| sk44 )
& ( sk43
| ( sk50 @ ( sk49 @ '$accessible_world' ) )
| sk46
| sk44 )
& ( sk43
| ~ ( sk49 @ p6 )
| sk46
| sk44 )
& ( sk43
| ( sk49 @ p5 )
| sk46
| sk44 )
& ( sk43
| ( ZM @ p5 )
| ~ ( ZM @ ( sk49 @ '$accessible_world' ) )
| sk46
| sk44 )
& ( sk43
| ( sk49 @ p5 )
| sk46
| sk44 )
& ( sk43
| ( sk49 @ ( '$local_world' @ '$accessible_world' ) )
| sk46
| sk44 )
& ( sk43
| ~ sk46
| ( sk47 @ p6 )
| sk44 )
& ( sk43
| ~ sk46
| ( ZL @ p6 )
| ~ ( ZL @ ( sk47 @ '$accessible_world' ) )
| sk44 )
& ( sk43
| ~ sk46
| ~ ( sk47 @ p5 )
| sk44 )
& ( sk43
| ~ sk46
| ~ ( sk48 @ p6 )
| sk44 )
& ( sk43
| ~ sk46
| ( sk48 @ p5 )
| sk44 )
& ( sk43
| ~ sk46
| ( ZK @ p5 )
| ~ ( ZK @ ( sk48 @ '$accessible_world' ) )
| sk44 )
& ( sk43
| ~ sk46
| ( sk48 @ p5 )
| sk44 )
& ( sk43
| ~ sk46
| ( sk48 @ ( sk47 @ '$accessible_world' ) )
| sk44 )
& ( sk43
| ~ sk46
| ( sk47 @ ( '$local_world' @ '$accessible_world' ) )
| sk44 )
& ( sk43
| ~ sk44
| ( sk45 @ p6 ) )
& ( sk43
| ~ sk44
| ( ZJ @ p6 )
| ~ ( ZJ @ ( sk45 @ '$accessible_world' ) ) )
& ( sk43
| ~ sk44
| ~ ( sk45 @ p5 ) )
& ( sk43
| ~ sk44
| ~ ( sk45 @ p6 ) )
& ( sk43
| ~ sk44
| ( sk45 @ p5 ) )
& ( sk43
| ~ sk44
| ( ZI @ p5 )
| ~ ( ZI @ ( sk45 @ '$accessible_world' ) ) )
& ( sk43
| ~ sk44
| ( sk45 @ p5 ) )
& ( sk43
| ~ sk44
| ( sk45 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( ZH @ p5 )
| ~ ( ZH @ sk42 @ p5 )
| ( ZH @ p4 )
| ~ ( ZH @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p5 )
| ~ ( ZG @ p4 )
| ~ ( ZG @ sk41 @ p4 )
| ~ ( ZG @ p4 )
| ~ ( ZG @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk33 )
& ( ~ ( ZH @ p5 )
| ( ZH @ sk42 @ ( ZH @ '$accessible_world' ) )
| ( ZH @ p4 )
| ~ ( ZH @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p5 )
| ~ ( ZG @ p4 )
| ~ ( ZG @ sk41 @ p4 )
| ~ ( ZG @ p4 )
| ~ ( ZG @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk33 )
& ( ~ ( ZH @ p5 )
| ~ ( ZH @ sk42 @ p5 )
| ( ZH @ p4 )
| ~ ( ZH @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p5 )
| ~ ( ZG @ p4 )
| ( ZG @ sk41 @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ p4 )
| ~ ( ZG @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk33 )
& ( ~ ( ZH @ p5 )
| ( ZH @ sk42 @ ( ZH @ '$accessible_world' ) )
| ( ZH @ p4 )
| ~ ( ZH @ ( '$local_world' @ '$accessible_world' ) )
| ( ZG @ p5 )
| ~ ( ZG @ p4 )
| ( ZG @ sk41 @ ( ZG @ '$accessible_world' ) )
| ~ ( ZG @ p4 )
| ~ ( ZG @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk33 )
& ( sk33
| ( sk40 @ p5 )
| sk36
| sk34 )
& ( sk33
| ( ZF @ p5 )
| ~ ( ZF @ ( sk40 @ '$accessible_world' ) )
| sk36
| sk34 )
& ( sk33
| ~ ( sk40 @ p4 )
| sk36
| sk34 )
& ( sk33
| ( sk40 @ ( sk39 @ '$accessible_world' ) )
| sk36
| sk34 )
& ( sk33
| ~ ( sk39 @ p5 )
| sk36
| sk34 )
& ( sk33
| ( sk39 @ p4 )
| sk36
| sk34 )
& ( sk33
| ( ZE @ p4 )
| ~ ( ZE @ ( sk39 @ '$accessible_world' ) )
| sk36
| sk34 )
& ( sk33
| ( sk39 @ p4 )
| sk36
| sk34 )
& ( sk33
| ( sk39 @ ( '$local_world' @ '$accessible_world' ) )
| sk36
| sk34 )
& ( sk33
| ~ sk36
| ( sk37 @ p5 )
| sk34 )
& ( sk33
| ~ sk36
| ( ZD @ p5 )
| ~ ( ZD @ ( sk37 @ '$accessible_world' ) )
| sk34 )
& ( sk33
| ~ sk36
| ~ ( sk37 @ p4 )
| sk34 )
& ( sk33
| ~ sk36
| ~ ( sk38 @ p5 )
| sk34 )
& ( sk33
| ~ sk36
| ( sk38 @ p4 )
| sk34 )
& ( sk33
| ~ sk36
| ( ZC @ p4 )
| ~ ( ZC @ ( sk38 @ '$accessible_world' ) )
| sk34 )
& ( sk33
| ~ sk36
| ( sk38 @ p4 )
| sk34 )
& ( sk33
| ~ sk36
| ( sk38 @ ( sk37 @ '$accessible_world' ) )
| sk34 )
& ( sk33
| ~ sk36
| ( sk37 @ ( '$local_world' @ '$accessible_world' ) )
| sk34 )
& ( sk33
| ~ sk34
| ( sk35 @ p5 ) )
& ( sk33
| ~ sk34
| ( ZB @ p5 )
| ~ ( ZB @ ( sk35 @ '$accessible_world' ) ) )
& ( sk33
| ~ sk34
| ~ ( sk35 @ p4 ) )
& ( sk33
| ~ sk34
| ~ ( sk35 @ p5 ) )
& ( sk33
| ~ sk34
| ( sk35 @ p4 ) )
& ( sk33
| ~ sk34
| ( ZA @ p4 )
| ~ ( ZA @ ( sk35 @ '$accessible_world' ) ) )
& ( sk33
| ~ sk34
| ( sk35 @ p4 ) )
& ( sk33
| ~ sk34
| ( sk35 @ ( '$local_world' @ '$accessible_world' ) ) )
& ~ ( sk32 @ p10 )
& ( ( Z @ p10 )
| ~ ( Z @ ( sk32 @ '$accessible_world' ) ) )
& ( sk32 @ p10 )
& ( sk32 @ ( '$local_world' @ '$accessible_world' ) )
& ~ ( sk31 @ p10 )
& ( ( Y @ p10 )
| ~ ( Y @ ( sk31 @ '$accessible_world' ) ) )
& ( sk31 @ p10 )
& ( sk31 @ ( '$local_world' @ '$accessible_world' ) )
& ( ~ ( X @ p4 )
| ~ ( X @ sk30 @ p4 )
| ( X @ p3 )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( W @ p4 )
| ~ ( W @ p3 )
| ~ ( W @ sk29 @ p3 )
| ~ ( W @ p3 )
| ~ ( W @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk21 )
& ( ~ ( X @ p4 )
| ( X @ sk30 @ ( X @ '$accessible_world' ) )
| ( X @ p3 )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( W @ p4 )
| ~ ( W @ p3 )
| ~ ( W @ sk29 @ p3 )
| ~ ( W @ p3 )
| ~ ( W @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk21 )
& ( ~ ( X @ p4 )
| ~ ( X @ sk30 @ p4 )
| ( X @ p3 )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( W @ p4 )
| ~ ( W @ p3 )
| ( W @ sk29 @ ( W @ '$accessible_world' ) )
| ~ ( W @ p3 )
| ~ ( W @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk21 )
& ( ~ ( X @ p4 )
| ( X @ sk30 @ ( X @ '$accessible_world' ) )
| ( X @ p3 )
| ~ ( X @ ( '$local_world' @ '$accessible_world' ) )
| ( W @ p4 )
| ~ ( W @ p3 )
| ( W @ sk29 @ ( W @ '$accessible_world' ) )
| ~ ( W @ p3 )
| ~ ( W @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk21 )
& ( sk21
| ( sk28 @ p4 )
| sk24
| sk22 )
& ( sk21
| ( V @ p4 )
| ~ ( V @ ( sk28 @ '$accessible_world' ) )
| sk24
| sk22 )
& ( sk21
| ~ ( sk28 @ p3 )
| sk24
| sk22 )
& ( sk21
| ( sk28 @ ( sk27 @ '$accessible_world' ) )
| sk24
| sk22 )
& ( sk21
| ~ ( sk27 @ p4 )
| sk24
| sk22 )
& ( sk21
| ( sk27 @ p3 )
| sk24
| sk22 )
& ( sk21
| ( U @ p3 )
| ~ ( U @ ( sk27 @ '$accessible_world' ) )
| sk24
| sk22 )
& ( sk21
| ( sk27 @ p3 )
| sk24
| sk22 )
& ( sk21
| ( sk27 @ ( '$local_world' @ '$accessible_world' ) )
| sk24
| sk22 )
& ( sk21
| ~ sk24
| ( sk25 @ p4 )
| sk22 )
& ( sk21
| ~ sk24
| ( T @ p4 )
| ~ ( T @ ( sk25 @ '$accessible_world' ) )
| sk22 )
& ( sk21
| ~ sk24
| ~ ( sk25 @ p3 )
| sk22 )
& ( sk21
| ~ sk24
| ~ ( sk26 @ p4 )
| sk22 )
& ( sk21
| ~ sk24
| ( sk26 @ p3 )
| sk22 )
& ( sk21
| ~ sk24
| ( S @ p3 )
| ~ ( S @ ( sk26 @ '$accessible_world' ) )
| sk22 )
& ( sk21
| ~ sk24
| ( sk26 @ p3 )
| sk22 )
& ( sk21
| ~ sk24
| ( sk26 @ ( sk25 @ '$accessible_world' ) )
| sk22 )
& ( sk21
| ~ sk24
| ( sk25 @ ( '$local_world' @ '$accessible_world' ) )
| sk22 )
& ( sk21
| ~ sk22
| ( sk23 @ p4 ) )
& ( sk21
| ~ sk22
| ( R @ p4 )
| ~ ( R @ ( sk23 @ '$accessible_world' ) ) )
& ( sk21
| ~ sk22
| ~ ( sk23 @ p3 ) )
& ( sk21
| ~ sk22
| ~ ( sk23 @ p4 ) )
& ( sk21
| ~ sk22
| ( sk23 @ p3 ) )
& ( sk21
| ~ sk22
| ( Q @ p3 )
| ~ ( Q @ ( sk23 @ '$accessible_world' ) ) )
& ( sk21
| ~ sk22
| ( sk23 @ p3 ) )
& ( sk21
| ~ sk22
| ( sk23 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( P @ p3 )
| ~ ( P @ sk20 @ p3 )
| ( P @ p2 )
| ~ ( P @ ( '$local_world' @ '$accessible_world' ) )
| ( O @ p3 )
| ~ ( O @ p2 )
| ~ ( O @ sk19 @ p2 )
| ~ ( O @ p2 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk11 )
& ( ~ ( P @ p3 )
| ( P @ sk20 @ ( P @ '$accessible_world' ) )
| ( P @ p2 )
| ~ ( P @ ( '$local_world' @ '$accessible_world' ) )
| ( O @ p3 )
| ~ ( O @ p2 )
| ~ ( O @ sk19 @ p2 )
| ~ ( O @ p2 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk11 )
& ( ~ ( P @ p3 )
| ~ ( P @ sk20 @ p3 )
| ( P @ p2 )
| ~ ( P @ ( '$local_world' @ '$accessible_world' ) )
| ( O @ p3 )
| ~ ( O @ p2 )
| ( O @ sk19 @ ( O @ '$accessible_world' ) )
| ~ ( O @ p2 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk11 )
& ( ~ ( P @ p3 )
| ( P @ sk20 @ ( P @ '$accessible_world' ) )
| ( P @ p2 )
| ~ ( P @ ( '$local_world' @ '$accessible_world' ) )
| ( O @ p3 )
| ~ ( O @ p2 )
| ( O @ sk19 @ ( O @ '$accessible_world' ) )
| ~ ( O @ p2 )
| ~ ( O @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk11 )
& ( sk11
| ( sk18 @ p3 )
| sk14
| sk12 )
& ( sk11
| ( N @ p3 )
| ~ ( N @ ( sk18 @ '$accessible_world' ) )
| sk14
| sk12 )
& ( sk11
| ~ ( sk18 @ p2 )
| sk14
| sk12 )
& ( sk11
| ( sk18 @ ( sk17 @ '$accessible_world' ) )
| sk14
| sk12 )
& ( sk11
| ~ ( sk17 @ p3 )
| sk14
| sk12 )
& ( sk11
| ( sk17 @ p2 )
| sk14
| sk12 )
& ( sk11
| ( M @ p2 )
| ~ ( M @ ( sk17 @ '$accessible_world' ) )
| sk14
| sk12 )
& ( sk11
| ( sk17 @ p2 )
| sk14
| sk12 )
& ( sk11
| ( sk17 @ ( '$local_world' @ '$accessible_world' ) )
| sk14
| sk12 )
& ( sk11
| ~ sk14
| ( sk15 @ p3 )
| sk12 )
& ( sk11
| ~ sk14
| ( L @ p3 )
| ~ ( L @ ( sk15 @ '$accessible_world' ) )
| sk12 )
& ( sk11
| ~ sk14
| ~ ( sk15 @ p2 )
| sk12 )
& ( sk11
| ~ sk14
| ~ ( sk16 @ p3 )
| sk12 )
& ( sk11
| ~ sk14
| ( sk16 @ p2 )
| sk12 )
& ( sk11
| ~ sk14
| ( K @ p2 )
| ~ ( K @ ( sk16 @ '$accessible_world' ) )
| sk12 )
& ( sk11
| ~ sk14
| ( sk16 @ p2 )
| sk12 )
& ( sk11
| ~ sk14
| ( sk16 @ ( sk15 @ '$accessible_world' ) )
| sk12 )
& ( sk11
| ~ sk14
| ( sk15 @ ( '$local_world' @ '$accessible_world' ) )
| sk12 )
& ( sk11
| ~ sk12
| ( sk13 @ p3 ) )
& ( sk11
| ~ sk12
| ( J @ p3 )
| ~ ( J @ ( sk13 @ '$accessible_world' ) ) )
& ( sk11
| ~ sk12
| ~ ( sk13 @ p2 ) )
& ( sk11
| ~ sk12
| ~ ( sk13 @ p3 ) )
& ( sk11
| ~ sk12
| ( sk13 @ p2 ) )
& ( sk11
| ~ sk12
| ( I @ p2 )
| ~ ( I @ ( sk13 @ '$accessible_world' ) ) )
& ( sk11
| ~ sk12
| ( sk13 @ p2 ) )
& ( sk11
| ~ sk12
| ( sk13 @ ( '$local_world' @ '$accessible_world' ) ) )
& ( ~ ( H @ p2 )
| ~ ( H @ sk10 @ p2 )
| ( H @ p1 )
| ~ ( H @ ( '$local_world' @ '$accessible_world' ) )
| ( G @ p2 )
| ~ ( G @ p1 )
| ~ ( G @ sk9 @ p1 )
| ~ ( G @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk1 )
& ( ~ ( H @ p2 )
| ( H @ sk10 @ ( H @ '$accessible_world' ) )
| ( H @ p1 )
| ~ ( H @ ( '$local_world' @ '$accessible_world' ) )
| ( G @ p2 )
| ~ ( G @ p1 )
| ~ ( G @ sk9 @ p1 )
| ~ ( G @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk1 )
& ( ~ ( H @ p2 )
| ~ ( H @ sk10 @ p2 )
| ( H @ p1 )
| ~ ( H @ ( '$local_world' @ '$accessible_world' ) )
| ( G @ p2 )
| ~ ( G @ p1 )
| ( G @ sk9 @ ( G @ '$accessible_world' ) )
| ~ ( G @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk1 )
& ( ~ ( H @ p2 )
| ( H @ sk10 @ ( H @ '$accessible_world' ) )
| ( H @ p1 )
| ~ ( H @ ( '$local_world' @ '$accessible_world' ) )
| ( G @ p2 )
| ~ ( G @ p1 )
| ( G @ sk9 @ ( G @ '$accessible_world' ) )
| ~ ( G @ p1 )
| ~ ( G @ ( '$local_world' @ '$accessible_world' ) )
| ~ sk1 )
& ( sk1
| ( sk8 @ p2 )
| sk4
| sk2 )
& ( sk1
| ( F @ p2 )
| ~ ( F @ ( sk8 @ '$accessible_world' ) )
| sk4
| sk2 )
& ( sk1
| ~ ( sk8 @ p1 )
| sk4
| sk2 )
& ( sk1
| ( sk8 @ ( sk7 @ '$accessible_world' ) )
| sk4
| sk2 )
& ( sk1
| ~ ( sk7 @ p2 )
| sk4
| sk2 )
& ( sk1
| ( sk7 @ p1 )
| sk4
| sk2 )
& ( sk1
| ( E @ p1 )
| ~ ( E @ ( sk7 @ '$accessible_world' ) )
| sk4
| sk2 )
& ( sk1
| ( sk7 @ p1 )
| sk4
| sk2 )
& ( sk1
| ( sk7 @ ( '$local_world' @ '$accessible_world' ) )
| sk4
| sk2 )
& ( sk1
| ~ sk4
| ( sk5 @ p2 )
| sk2 )
& ( sk1
| ~ sk4
| ( D @ p2 )
| ~ ( D @ ( sk5 @ '$accessible_world' ) )
| sk2 )
& ( sk1
| ~ sk4
| ~ ( sk5 @ p1 )
| sk2 )
& ( sk1
| ~ sk4
| ~ ( sk6 @ p2 )
| sk2 )
& ( sk1
| ~ sk4
| ( sk6 @ p1 )
| sk2 )
& ( sk1
| ~ sk4
| ( C @ p1 )
| ~ ( C @ ( sk6 @ '$accessible_world' ) )
| sk2 )
& ( sk1
| ~ sk4
| ( sk6 @ p1 )
| sk2 )
& ( sk1
| ~ sk4
| ( sk6 @ ( sk5 @ '$accessible_world' ) )
| sk2 )
& ( sk1
| ~ sk4
| ( sk5 @ ( '$local_world' @ '$accessible_world' ) )
| sk2 )
& ( sk1
| ~ sk2
| ( sk3 @ p2 ) )
& ( sk1
| ~ sk2
| ( B @ p2 )
| ~ ( B @ ( sk3 @ '$accessible_world' ) ) )
& ( sk1
| ~ sk2
| ~ ( sk3 @ p1 ) )
& ( sk1
| ~ sk2
| ~ ( sk3 @ p2 ) )
& ( sk1
| ~ sk2
| ( sk3 @ p1 ) )
& ( sk1
| ~ sk2
| ( A @ p1 )
| ~ ( A @ ( sk3 @ '$accessible_world' ) ) )
& ( sk1
| ~ sk2
| ( sk3 @ p1 ) )
& ( sk1
| ~ sk2
| ( sk3 @ ( '$local_world' @ '$accessible_world' ) ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(237,plain,
sk31 @ p10,
inference(cnfConj,[status(thm)],[4]) ).
thf(159,plain,
~ ( sk31 @ p10 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(384,plain,
$false,
inference(rewrite,[status(thm)],[237,159]) ).
thf(385,plain,
$false,
inference(simp,[status(thm)],[384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYP017_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.14/0.40 % Computer : n009.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sat Sep 26 20:22:45 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 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.88/0.98 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.44/1.21 % [INFO] Parsing done (226ms).
% 1.44/1.23 % [INFO] Input problem is non-classical (logic $modal). Running HOL transformation from semantics specification contained in the problem file ...
% 1.44/1.25 %%% 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.81/1.36 % [INFO] Running in sequential loop mode.
% 2.48/1.74 % [INFO] eprover registered as external prover.
% 2.48/1.75 % [INFO] Scanning for conjecture ...
% 3.22/2.03 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 3.22/2.13 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 3.51/2.13 % [INFO] Problem is typed first-order (TPTP TFF).
% 3.51/2.15 % [INFO] Type checking passed.
% 3.51/2.15 % [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 ...
% 8.58/4.22 % [INFO] Killing All external provers ...
% 8.58/4.23 % Time passed: 3680ms (effective reasoning time: 2857ms)
% 8.58/4.23 % 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)>
% 8.58/4.23 % Axioms used in derivation (0):
% 8.58/4.23 % No. of inferences in proof: 8
% 8.58/4.23 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3680 ms resp. 2857 ms w/o parsing
% 9.76/4.57 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 9.76/4.57 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------