%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:53:23 AM UTC 2026
% Result : Theorem 41.00s 13.19s
% Output : Refutation 36.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 44
% Syntax : Number of formulae : 172 ( 51 unt; 0 typ; 23 def)
% Number of atoms : 2080 ( 133 equ; 0 cnn)
% Maximal formula atoms : 173 ( 12 avg)
% Number of connectives : 9063 ( 453 ~; 406 |; 485 &;6789 @)
% ( 0 <=>; 930 =>; 0 <=; 0 <~>)
% Maximal formula depth : 73 ( 9 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 48 ( 45 usr; 36 con; 0-3 aty)
% Number of variables : 1046 ( 6 ^;1015 !; 2 ?;1046 :)
% ( 0 !>; 0 ?*; 0 @-; 23 @+)
% Comments :
%------------------------------------------------------------------------------
thf('$ki_world_type',type,
'$ki_world': $tType ).
thf('$ki_local_world_decl',type,
'$ki_local_world': '$ki_world' ).
thf('$ki_accessible_decl',type,
'$ki_accessible': '$ki_world' > '$ki_world' > $o ).
thf(unit_decl,type,
unit: $i ).
thf(e0_decl,type,
e0: $i ).
thf(e1_decl,type,
e1: $i ).
thf(e2_decl,type,
e2: $i ).
thf(e3_decl,type,
e3: $i ).
thf(qmltpeq_decl,type,
qmltpeq: '$ki_world' > $i > $i > $o ).
thf(inv_decl,type,
inv: $i > $i ).
thf(op_decl,type,
op: $i > $i > $i ).
thf('$ki_exists_in_world_$i_decl',type,
'$ki_exists_in_world_$i': '$ki_world' > $i > $o ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: '$ki_world' ).
thf(sk3_decl,type,
sk3: $o ).
thf(sk4_decl,type,
sk4: '$ki_world' ).
thf(sk5_decl,type,
sk5: '$ki_world' ).
thf(sk6_decl,type,
sk6: '$ki_world' ).
thf(sk7_decl,type,
sk7: $o ).
thf(sk8_decl,type,
sk8: '$ki_world' ).
thf(sk9_decl,type,
sk9: $o ).
thf(sk10_decl,type,
sk10: '$ki_world' ).
thf(sk11_decl,type,
sk11: '$ki_world' ).
thf(sk12_decl,type,
sk12: '$ki_world' ).
thf(sk13_decl,type,
sk13: $o ).
thf(sk14_decl,type,
sk14: '$ki_world' ).
thf(sk15_decl,type,
sk15: $o ).
thf(sk16_decl,type,
sk16: '$ki_world' ).
thf(sk17_decl,type,
sk17: '$ki_world' ).
thf(sk18_decl,type,
sk18: '$ki_world' ).
thf(sk19_decl,type,
sk19: $o ).
thf(sk20_decl,type,
sk20: '$ki_world' ).
thf(sk21_decl,type,
sk21: $o ).
thf(sk22_decl,type,
sk22: '$ki_world' ).
thf(sk23_decl,type,
sk23: '$ki_world' ).
thf(sk24_decl,type,
sk24: '$ki_world' ).
thf(sk25_decl,type,
sk25: '$ki_world' ).
thf(sk26_decl,type,
sk26: $o ).
thf(sk27_decl,type,
sk27: $o ).
thf(sk28_decl,type,
sk28: $o ).
thf(sk80_decl,type,
sk80: '$ki_world' > '$ki_world' ).
thf(sk81_decl,type,
sk81: '$ki_world' > '$ki_world' ).
thf(sk82_decl,type,
sk82: '$ki_world' > '$ki_world' ).
thf(sk83_decl,type,
sk83: '$ki_world' > '$ki_world' ).
thf(sk84_decl,type,
sk84: '$ki_world' > '$ki_world' ).
thf(sk85_decl,type,
sk85: '$ki_world' > '$ki_world' ).
thf(sk2_def,definition,
( sk2
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk23_def,definition,
( sk23
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ) ).
thf(sk25_def,definition,
( sk25
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ( ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ) ) ) ) ).
thf(sk80_def,definition,
( sk80
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(sk81_def,definition,
( sk81
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(sk82_def,definition,
( sk82
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(sk83_def,definition,
( sk83
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(sk84_def,definition,
( sk84
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(sk85_def,definition,
( sk85
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( B @ qmltpeq ) ) ) ) ) ) ).
thf(9,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e2 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e1 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e1 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
thf(249,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e2 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e1 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e1 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e0 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e3 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e2 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e1 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(8,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
thf(120,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e3 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e2 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e1 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e3 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e2 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e1 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e3 @ op ) @ ( e0 @ ( e0 @ ( e3 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e3 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e2 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e1 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e3 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e2 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e1 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e2 @ op ) @ ( e0 @ ( e0 @ ( e2 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e3 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e2 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e1 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e3 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e2 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e1 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e1 @ op ) @ ( e0 @ ( e0 @ ( e1 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e3 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e2 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e1 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e3 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e2 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e1 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ op ) @ ( e0 @ op ) @ ( e0 @ ( e0 @ ( e0 @ op ) @ op ) @ ( A @ qmltpeq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(11,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( B @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
thf(443,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( B @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(19,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
thf(607,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(608,plain,
! [A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnf,[status(esa)],[607]) ).
thf(6,axiom,
! [A: '$ki_world',B: '$ki_world'] : ( B @ ( A @ '$ki_accessible' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_universal) ).
thf(112,plain,
! [A: '$ki_world',B: '$ki_world'] : ( B @ ( A @ '$ki_accessible' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(113,plain,
! [B: '$ki_world',A: '$ki_world'] : ( B @ ( A @ '$ki_accessible' ) ),
inference(cnf,[status(esa)],[112]) ).
thf(720,plain,
! [A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[608,113]) ).
thf(721,plain,
! [A: '$ki_world'] : ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) ),
inference(simp,[status(thm)],[720]) ).
thf(444,plain,
! [F: '$ki_world',E: '$ki_world',D: '$ki_world',C: '$ki_world',B: '$ki_world',A: '$ki_world'] :
( ( ~ ( e3 @ ( e2 @ ( F @ sk85 @ qmltpeq ) ) )
| ~ ( F @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( F @ sk85 @ ( F @ '$ki_accessible' ) )
| ~ ( F @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e3 @ ( e1 @ ( E @ sk84 @ qmltpeq ) ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( E @ sk84 @ ( E @ '$ki_accessible' ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e2 @ ( e1 @ ( D @ sk83 @ qmltpeq ) ) )
| ~ ( D @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( D @ sk83 @ ( D @ '$ki_accessible' ) )
| ~ ( D @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e3 @ ( e0 @ ( C @ sk82 @ qmltpeq ) ) )
| ~ ( C @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( C @ sk82 @ ( C @ '$ki_accessible' ) )
| ~ ( C @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e2 @ ( e0 @ ( B @ sk81 @ qmltpeq ) ) )
| ~ ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( B @ sk81 @ ( B @ '$ki_accessible' ) )
| ~ ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e1 @ ( e0 @ ( A @ sk80 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( A @ sk80 @ ( A @ '$ki_accessible' ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ) ),
inference(cnf,[status(esa)],[443]) ).
thf(451,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e0 @ ( A @ sk81 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(462,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e0 @ ( A @ sk81 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[451]) ).
thf(697,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e0 @ ( A @ sk81 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[462,113]) ).
thf(698,plain,
! [A: '$ki_world'] :
~ ( e2 @ ( e0 @ ( A @ sk81 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[697]) ).
thf(730,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( B @ sk81 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[721,698]) ).
thf(731,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( B @ sk81 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[730]) ).
thf(759,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e2 != unit )
| ( ( unit @ inv )
!= e0 )
| ( A
!= ( B @ sk81 ) ) ),
inference(simp,[status(thm)],[731]) ).
thf(773,plain,
( ( e2 != unit )
| ( ( unit @ inv )
!= e0 ) ),
inference(simp,[status(thm)],[759]) ).
thf(1,conjecture,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ( ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',verify) ).
thf(2,negated_conjecture,
~ ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ( ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(23,plain,
~ ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ( ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) )
| ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) ) )
& ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( B @ qmltpeq ) ) ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
| ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(24,plain,
! [P: '$ki_world',O: '$ki_world',N: '$ki_world',M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: '$ki_world',G: '$ki_world',F: '$ki_world',E: '$ki_world',D: '$ki_world',C: '$ki_world',B: '$ki_world',A: '$ki_world'] :
( ( ( e3 @ ( e3 @ ( e3 @ op ) @ ( P @ qmltpeq ) ) )
| ~ ( P @ ( sk25 @ '$ki_accessible' ) )
| ~ sk28
| ~ sk27
| ~ sk26 )
& ( ( e3 @ ( e2 @ ( e2 @ op ) @ ( O @ qmltpeq ) ) )
| ~ ( O @ ( sk25 @ '$ki_accessible' ) )
| ~ sk28
| ~ sk27
| ~ sk26 )
& ( ( e3 @ ( e1 @ ( e1 @ op ) @ ( N @ qmltpeq ) ) )
| ~ ( N @ ( sk25 @ '$ki_accessible' ) )
| ~ sk28
| ~ sk27
| ~ sk26 )
& ( ( e3 @ ( e0 @ ( e0 @ op ) @ ( M @ qmltpeq ) ) )
| ~ ( M @ ( sk25 @ '$ki_accessible' ) )
| ~ sk28
| ~ sk27
| ~ sk26 )
& ( sk28
| ( e2 @ ( e3 @ ( e3 @ op ) @ ( L @ qmltpeq ) ) )
| ~ ( L @ ( sk25 @ '$ki_accessible' ) )
| ~ sk27
| ~ sk26 )
& ( sk28
| ( e2 @ ( e2 @ ( e2 @ op ) @ ( K @ qmltpeq ) ) )
| ~ ( K @ ( sk25 @ '$ki_accessible' ) )
| ~ sk27
| ~ sk26 )
& ( sk28
| ( e2 @ ( e1 @ ( e1 @ op ) @ ( J @ qmltpeq ) ) )
| ~ ( J @ ( sk25 @ '$ki_accessible' ) )
| ~ sk27
| ~ sk26 )
& ( sk28
| ( e2 @ ( e0 @ ( e0 @ op ) @ ( I @ qmltpeq ) ) )
| ~ ( I @ ( sk25 @ '$ki_accessible' ) )
| ~ sk27
| ~ sk26 )
& ( sk27
| ( e1 @ ( e3 @ ( e3 @ op ) @ ( H @ qmltpeq ) ) )
| ~ ( H @ ( sk25 @ '$ki_accessible' ) )
| ~ sk26 )
& ( sk27
| ( e1 @ ( e2 @ ( e2 @ op ) @ ( G @ qmltpeq ) ) )
| ~ ( G @ ( sk25 @ '$ki_accessible' ) )
| ~ sk26 )
& ( sk27
| ( e1 @ ( e1 @ ( e1 @ op ) @ ( F @ qmltpeq ) ) )
| ~ ( F @ ( sk25 @ '$ki_accessible' ) )
| ~ sk26 )
& ( sk27
| ( e1 @ ( e0 @ ( e0 @ op ) @ ( E @ qmltpeq ) ) )
| ~ ( E @ ( sk25 @ '$ki_accessible' ) )
| ~ sk26 )
& ( sk26
| ( e0 @ ( e3 @ ( e3 @ op ) @ ( D @ qmltpeq ) ) )
| ~ ( D @ ( sk25 @ '$ki_accessible' ) ) )
& ( sk26
| ( e0 @ ( e2 @ ( e2 @ op ) @ ( C @ qmltpeq ) ) )
| ~ ( C @ ( sk25 @ '$ki_accessible' ) ) )
& ( sk26
| ( e0 @ ( e1 @ ( e1 @ op ) @ ( B @ qmltpeq ) ) )
| ~ ( B @ ( sk25 @ '$ki_accessible' ) ) )
& ( sk26
| ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) )
| ~ ( A @ ( sk25 @ '$ki_accessible' ) ) )
& ( sk25 @ ( '$ki_local_world' @ '$ki_accessible' ) )
& ( ~ ( e3 @ ( e3 @ ( e3 @ op ) @ ( sk24 @ qmltpeq ) ) )
| ~ ( e3 @ ( e2 @ ( e2 @ op ) @ ( sk23 @ qmltpeq ) ) )
| sk21
| sk19 )
& ( ( sk24 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( e3 @ ( e2 @ ( e2 @ op ) @ ( sk23 @ qmltpeq ) ) )
| sk21
| sk19 )
& ( ~ ( e3 @ ( e3 @ ( e3 @ op ) @ ( sk24 @ qmltpeq ) ) )
| ( sk23 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk21
| sk19 )
& ( ( sk24 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ( sk23 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk21
| sk19 )
& ( ~ sk21
| ~ ( e3 @ ( e1 @ ( e1 @ op ) @ ( sk22 @ qmltpeq ) ) )
| sk19 )
& ( ~ sk21
| ( sk22 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk19 )
& ( ~ sk19
| ~ ( e3 @ ( e0 @ ( e0 @ op ) @ ( sk20 @ qmltpeq ) ) ) )
& ( ~ sk19
| ( sk20 @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e2 @ ( e3 @ ( e3 @ op ) @ ( sk18 @ qmltpeq ) ) )
| ~ ( e2 @ ( e2 @ ( e2 @ op ) @ ( sk17 @ qmltpeq ) ) )
| sk15
| sk13 )
& ( ( sk18 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( e2 @ ( e2 @ ( e2 @ op ) @ ( sk17 @ qmltpeq ) ) )
| sk15
| sk13 )
& ( ~ ( e2 @ ( e3 @ ( e3 @ op ) @ ( sk18 @ qmltpeq ) ) )
| ( sk17 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk15
| sk13 )
& ( ( sk18 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ( sk17 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk15
| sk13 )
& ( ~ sk15
| ~ ( e2 @ ( e1 @ ( e1 @ op ) @ ( sk16 @ qmltpeq ) ) )
| sk13 )
& ( ~ sk15
| ( sk16 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk13 )
& ( ~ sk13
| ~ ( e2 @ ( e0 @ ( e0 @ op ) @ ( sk14 @ qmltpeq ) ) ) )
& ( ~ sk13
| ( sk14 @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e1 @ ( e3 @ ( e3 @ op ) @ ( sk12 @ qmltpeq ) ) )
| ~ ( e1 @ ( e2 @ ( e2 @ op ) @ ( sk11 @ qmltpeq ) ) )
| sk9
| sk7 )
& ( ( sk12 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( e1 @ ( e2 @ ( e2 @ op ) @ ( sk11 @ qmltpeq ) ) )
| sk9
| sk7 )
& ( ~ ( e1 @ ( e3 @ ( e3 @ op ) @ ( sk12 @ qmltpeq ) ) )
| ( sk11 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk9
| sk7 )
& ( ( sk12 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ( sk11 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk9
| sk7 )
& ( ~ sk9
| ~ ( e1 @ ( e1 @ ( e1 @ op ) @ ( sk10 @ qmltpeq ) ) )
| sk7 )
& ( ~ sk9
| ( sk10 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk7 )
& ( ~ sk7
| ~ ( e1 @ ( e0 @ ( e0 @ op ) @ ( sk8 @ qmltpeq ) ) ) )
& ( ~ sk7
| ( sk8 @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ~ ( e0 @ ( e3 @ ( e3 @ op ) @ ( sk6 @ qmltpeq ) ) )
| ~ ( e0 @ ( e2 @ ( e2 @ op ) @ ( sk5 @ qmltpeq ) ) )
| sk3
| sk1 )
& ( ( sk6 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( e0 @ ( e2 @ ( e2 @ op ) @ ( sk5 @ qmltpeq ) ) )
| sk3
| sk1 )
& ( ~ ( e0 @ ( e3 @ ( e3 @ op ) @ ( sk6 @ qmltpeq ) ) )
| ( sk5 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk3
| sk1 )
& ( ( sk6 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ( sk5 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk3
| sk1 )
& ( ~ sk3
| ~ ( e0 @ ( e1 @ ( e1 @ op ) @ ( sk4 @ qmltpeq ) ) )
| sk1 )
& ( ~ sk3
| ( sk4 @ ( '$ki_local_world' @ '$ki_accessible' ) )
| sk1 )
& ( ~ sk1
| ~ ( e0 @ ( e0 @ ( e0 @ op ) @ ( sk2 @ qmltpeq ) ) ) )
& ( ~ sk1
| ( sk2 @ ( '$ki_local_world' @ '$ki_accessible' ) ) ) ),
inference(cnf,[status(esa)],[23]) ).
thf(45,plain,
( ~ sk19
| ~ ( e3 @ ( e0 @ ( e0 @ op ) @ ( sk20 @ qmltpeq ) ) ) ),
inference(cnfConj,[status(thm)],[24]) ).
thf(455,plain,
! [A: '$ki_world'] :
( ~ ( e1 @ ( e0 @ ( A @ sk80 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(635,plain,
! [A: '$ki_world'] :
( ~ ( e1 @ ( e0 @ ( A @ sk80 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[455,113]) ).
thf(636,plain,
! [A: '$ki_world'] :
~ ( e1 @ ( e0 @ ( A @ sk80 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[635]) ).
thf(726,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( B @ sk80 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[721,636]) ).
thf(727,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( B @ sk80 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[726]) ).
thf(758,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e1 != unit )
| ( ( unit @ inv )
!= e0 )
| ( A
!= ( B @ sk80 ) ) ),
inference(simp,[status(thm)],[727]) ).
thf(772,plain,
( ( e1 != unit )
| ( ( unit @ inv )
!= e0 ) ),
inference(simp,[status(thm)],[758]) ).
thf(21,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( F @ op ) @ ( B @ ( F @ op ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_substitution_2) ).
thf(613,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( F @ op ) @ ( B @ ( F @ op ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(10,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( A @ qmltpeq ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
thf(441,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( A @ qmltpeq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(442,plain,
! [A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnf,[status(esa)],[441]) ).
thf(647,plain,
! [A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[442,113]) ).
thf(648,plain,
! [A: '$ki_world'] : ( e0 @ ( unit @ ( A @ qmltpeq ) ) ),
inference(simp,[status(thm)],[647]) ).
thf(445,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e1 @ ( A @ sk83 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(461,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e1 @ ( A @ sk83 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[445]) ).
thf(691,plain,
! [A: '$ki_world'] :
( ~ ( e2 @ ( e1 @ ( A @ sk83 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[461,113]) ).
thf(692,plain,
! [A: '$ki_world'] :
~ ( e2 @ ( e1 @ ( A @ sk83 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[691]) ).
thf(693,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e1 @ ( B @ sk83 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,692]) ).
thf(694,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e1 @ ( B @ sk83 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[693]) ).
thf(695,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e2 != e0 )
| ( e1 != unit )
| ( A
!= ( B @ sk83 ) ) ),
inference(simp,[status(thm)],[694]) ).
thf(696,plain,
( ( e2 != e0 )
| ( e1 != unit ) ),
inference(simp,[status(thm)],[695]) ).
thf(13,axiom,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e3 @ ( e3 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e3 @ inv @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e2 @ ( e2 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e2 @ inv @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e1 @ ( e1 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e1 @ inv @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e0 @ ( e0 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e0 @ inv @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
thf(500,plain,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ ( A @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e3 @ ( e3 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e3 @ inv @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e2 @ ( e2 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e2 @ inv @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e1 @ ( e1 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e1 @ inv @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e0 @ ( e0 @ inv @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( unit @ ( e0 @ inv @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(454,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e2 @ ( A @ sk85 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(466,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e2 @ ( A @ sk85 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[454]) ).
thf(714,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e2 @ ( A @ sk85 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[466,113]) ).
thf(715,plain,
! [A: '$ki_world'] :
~ ( e3 @ ( e2 @ ( A @ sk85 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[714]) ).
thf(716,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e2 @ ( B @ sk85 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,715]) ).
thf(717,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e2 @ ( B @ sk85 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[716]) ).
thf(718,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e3 != e0 )
| ( e2 != unit )
| ( A
!= ( B @ sk85 ) ) ),
inference(simp,[status(thm)],[717]) ).
thf(719,plain,
( ( e3 != e0 )
| ( e2 != unit ) ),
inference(simp,[status(thm)],[718]) ).
thf(699,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( B @ sk81 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,698]) ).
thf(700,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( B @ sk81 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[699]) ).
thf(701,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e2 != e0 )
| ( e0 != unit )
| ( A
!= ( B @ sk81 ) ) ),
inference(simp,[status(thm)],[700]) ).
thf(702,plain,
( ( e2 != e0 )
| ( e0 != unit ) ),
inference(simp,[status(thm)],[701]) ).
thf(452,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e0 @ ( A @ sk82 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(459,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e0 @ ( A @ sk82 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[452]) ).
thf(637,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e0 @ ( A @ sk82 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[459,113]) ).
thf(638,plain,
! [A: '$ki_world'] :
~ ( e3 @ ( e0 @ ( A @ sk82 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[637]) ).
thf(5,axiom,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( A @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( unit @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( unit @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( unit @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
thf(93,plain,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( unit @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( A @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( unit @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( unit @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( unit @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( unit @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( unit @ op ) @ ( A @ qmltpeq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(728,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e2 @ ( B @ sk85 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[721,715]) ).
thf(729,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e2 @ ( B @ sk85 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[728]) ).
thf(752,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e3 != unit )
| ( ( unit @ inv )
!= e2 )
| ( A
!= ( B @ sk85 ) ) ),
inference(simp,[status(thm)],[729]) ).
thf(766,plain,
( ( e3 != unit )
| ( ( unit @ inv )
!= e2 ) ),
inference(simp,[status(thm)],[752]) ).
thf(61,plain,
( ~ sk3
| ~ ( e0 @ ( e1 @ ( e1 @ op ) @ ( sk4 @ qmltpeq ) ) )
| sk1 ),
inference(cnfConj,[status(thm)],[24]) ).
thf(734,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e1 @ ( B @ sk83 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[721,692]) ).
thf(735,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e1 @ ( B @ sk83 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[734]) ).
thf(760,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e2 != unit )
| ( ( unit @ inv )
!= e1 )
| ( A
!= ( B @ sk83 ) ) ),
inference(simp,[status(thm)],[735]) ).
thf(774,plain,
( ( e2 != unit )
| ( ( unit @ inv )
!= e1 ) ),
inference(simp,[status(thm)],[760]) ).
thf(3,axiom,
! [A: '$ki_world'] :
? [B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$ki_exists_in_world_$i_nonempty') ).
thf(89,plain,
! [A: '$ki_world'] :
? [B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(60,plain,
( ~ sk1
| ~ ( e0 @ ( e0 @ ( e0 @ op ) @ ( sk2 @ qmltpeq ) ) ) ),
inference(cnfConj,[status(thm)],[24]) ).
thf(30,plain,
( ~ sk7
| ~ ( e1 @ ( e0 @ ( e0 @ op ) @ ( sk8 @ qmltpeq ) ) ) ),
inference(cnfConj,[status(thm)],[24]) ).
thf(657,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( e0 @ op ) @ ( sk8 @ qmltpeq ) ) ) )
| ~ sk7
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,30]) ).
thf(658,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( e0 @ op ) @ ( sk8 @ qmltpeq ) ) ) )
| ~ sk7 ),
inference(simp,[status(thm)],[657]) ).
thf(669,plain,
! [A: '$ki_world'] :
( ( e1 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ( A != sk8 )
| ~ sk7 ),
inference(simp,[status(thm)],[658]) ).
thf(678,plain,
( ( e1 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ~ sk7 ),
inference(simp,[status(thm)],[669]) ).
thf(15,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ inv @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
thf(529,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ inv @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ~ ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ inv @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(28,plain,
( ~ ( e2 @ ( e3 @ ( e3 @ op ) @ ( sk18 @ qmltpeq ) ) )
| ~ ( e2 @ ( e2 @ ( e2 @ op ) @ ( sk17 @ qmltpeq ) ) )
| sk15
| sk13 ),
inference(cnfConj,[status(thm)],[24]) ).
thf(70,plain,
( ~ sk13
| ~ ( e2 @ ( e0 @ ( e0 @ op ) @ ( sk14 @ qmltpeq ) ) ) ),
inference(cnfConj,[status(thm)],[24]) ).
thf(4,axiom,
! [A: '$ki_world',B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$ki_exists_in_world_$i_const') ).
thf(91,plain,
! [A: '$ki_world',B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(92,plain,
! [B: $i,A: '$ki_world'] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
inference(cnf,[status(esa)],[91]) ).
thf(12,axiom,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
thf(467,plain,
( ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e3 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e2 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e1 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) )
& ( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) )
| ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ ( e0 @ op ) @ ( A @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(456,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e1 @ ( A @ sk84 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[444]) ).
thf(460,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e1 @ ( A @ sk84 @ qmltpeq ) ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[456]) ).
thf(685,plain,
! [A: '$ki_world'] :
( ~ ( e3 @ ( e1 @ ( A @ sk84 @ qmltpeq ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[460,113]) ).
thf(686,plain,
! [A: '$ki_world'] :
~ ( e3 @ ( e1 @ ( A @ sk84 @ qmltpeq ) ) ),
inference(simp,[status(thm)],[685]) ).
thf(655,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( B @ sk80 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,636]) ).
thf(656,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e1 @ ( e0 @ ( B @ sk80 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[655]) ).
thf(670,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e1 != e0 )
| ( e0 != unit )
| ( A
!= ( B @ sk80 ) ) ),
inference(simp,[status(thm)],[656]) ).
thf(679,plain,
( ( e1 != e0 )
| ( e0 != unit ) ),
inference(simp,[status(thm)],[670]) ).
thf(18,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ( B @ ( B @ ( C @ qmltpeq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
thf(605,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ( B @ ( B @ ( C @ qmltpeq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(20,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ( ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ inv @ ( B @ inv @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inv_substitution_1) ).
thf(609,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ( ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ inv @ ( B @ inv @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(649,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( B @ sk82 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,638]) ).
thf(650,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( B @ sk82 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[649]) ).
thf(666,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e3 != e0 )
| ( e0 != unit )
| ( A
!= ( B @ sk82 ) ) ),
inference(simp,[status(thm)],[650]) ).
thf(675,plain,
( ( e3 != e0 )
| ( e0 != unit ) ),
inference(simp,[status(thm)],[666]) ).
thf(651,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e0 @ ( e0 @ ( e0 @ op ) @ ( sk2 @ qmltpeq ) ) ) )
| ~ sk1
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,60]) ).
thf(652,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e0 @ ( e0 @ ( e0 @ op ) @ ( sk2 @ qmltpeq ) ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[651]) ).
thf(671,plain,
! [A: '$ki_world'] :
( ( e0 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ( A != sk2 )
| ~ sk1 ),
inference(simp,[status(thm)],[652]) ).
thf(680,plain,
( ( ( e0 @ ( e0 @ op ) )
!= unit )
| ~ sk1 ),
inference(simp,[status(thm)],[671]) ).
thf(22,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ inv @ ( A @ qmltpeq ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
thf(617,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ inv @ ( A @ qmltpeq ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ inv @ ( A @ qmltpeq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(16,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ( ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( B @ ( D @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry) ).
thf(553,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ( ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( B @ ( D @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(14,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( D @ op ) @ ( F @ ( B @ op ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_substitution_1) ).
thf(525,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( D @ op ) @ ( F @ ( B @ op ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(709,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e0 @ ( e1 @ ( e1 @ op ) @ ( sk4 @ qmltpeq ) ) ) )
| ~ sk3
| ~ $true
| sk1 ),
inference(paramod_ordered,[status(thm)],[648,61]) ).
thf(710,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e0 @ ( e1 @ ( e1 @ op ) @ ( sk4 @ qmltpeq ) ) ) )
| ~ sk3
| sk1 ),
inference(simp,[status(thm)],[709]) ).
thf(711,plain,
! [A: '$ki_world'] :
( ( e0 != e0 )
| ( ( e1 @ ( e1 @ op ) )
!= unit )
| ( A != sk4 )
| ~ sk3
| sk1 ),
inference(simp,[status(thm)],[710]) ).
thf(712,plain,
( ( ( e1 @ ( e1 @ op ) )
!= unit )
| ~ sk3
| sk1 ),
inference(simp,[status(thm)],[711]) ).
thf(17,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
thf(557,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e3 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e3 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e2 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e2 @ inv @ ( B @ qmltpeq ) ) ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e1 @ ( e0 @ inv @ ( B @ qmltpeq ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( e0 @ ( e1 @ inv @ ( B @ qmltpeq ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(687,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e1 @ ( B @ sk84 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,686]) ).
thf(688,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e1 @ ( B @ sk84 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[687]) ).
thf(689,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e3 != e0 )
| ( e1 != unit )
| ( A
!= ( B @ sk84 ) ) ),
inference(simp,[status(thm)],[688]) ).
thf(690,plain,
( ( e3 != e0 )
| ( e1 != unit ) ),
inference(simp,[status(thm)],[689]) ).
thf(63,plain,
( ~ sk9
| ~ ( e1 @ ( e1 @ ( e1 @ op ) @ ( sk10 @ qmltpeq ) ) )
| sk7 ),
inference(cnfConj,[status(thm)],[24]) ).
thf(663,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( e0 @ op ) @ ( sk14 @ qmltpeq ) ) ) )
| ~ sk13
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,70]) ).
thf(664,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e2 @ ( e0 @ ( e0 @ op ) @ ( sk14 @ qmltpeq ) ) ) )
| ~ sk13 ),
inference(simp,[status(thm)],[663]) ).
thf(672,plain,
! [A: '$ki_world'] :
( ( e2 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ( A != sk14 )
| ~ sk13 ),
inference(simp,[status(thm)],[664]) ).
thf(673,plain,
( ( e2 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ~ sk13 ),
inference(simp,[status(thm)],[672]) ).
thf(7,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( D @ ( H @ qmltpeq ) ) ) )
& ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( B @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
thf(114,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ! [B: $i] :
( ( B @ ( A @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ '$ki_accessible' ) )
=> ! [D: $i] :
( ( D @ ( C @ '$ki_exists_in_world_$i' ) )
=> ! [E: '$ki_world'] :
( ( E @ ( C @ '$ki_accessible' ) )
=> ! [F: $i] :
( ( F @ ( E @ '$ki_exists_in_world_$i' ) )
=> ! [G: '$ki_world'] :
( ( G @ ( E @ '$ki_accessible' ) )
=> ( ( ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( D @ ( H @ qmltpeq ) ) ) )
& ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( B @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(51,plain,
( ~ sk15
| ~ ( e2 @ ( e1 @ ( e1 @ op ) @ ( sk16 @ qmltpeq ) ) )
| sk13 ),
inference(cnfConj,[status(thm)],[24]) ).
thf(722,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( B @ sk82 @ qmltpeq ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[721,638]) ).
thf(723,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( unit @ ( unit @ inv @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( B @ sk82 @ qmltpeq ) ) ) ),
inference(simp,[status(thm)],[722]) ).
thf(761,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( e3 != unit )
| ( ( unit @ inv )
!= e0 )
| ( A
!= ( B @ sk82 ) ) ),
inference(simp,[status(thm)],[723]) ).
thf(775,plain,
( ( e3 != unit )
| ( ( unit @ inv )
!= e0 ) ),
inference(simp,[status(thm)],[761]) ).
thf(653,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( e0 @ op ) @ ( sk20 @ qmltpeq ) ) ) )
| ~ sk19
| ~ $true ),
inference(paramod_ordered,[status(thm)],[648,45]) ).
thf(654,plain,
! [A: '$ki_world'] :
( ( ( e0 @ ( unit @ ( A @ qmltpeq ) ) )
!= ( e3 @ ( e0 @ ( e0 @ op ) @ ( sk20 @ qmltpeq ) ) ) )
| ~ sk19 ),
inference(simp,[status(thm)],[653]) ).
thf(667,plain,
! [A: '$ki_world'] :
( ( e3 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ( A != sk20 )
| ~ sk19 ),
inference(simp,[status(thm)],[654]) ).
thf(676,plain,
( ( e3 != e0 )
| ( ( e0 @ ( e0 @ op ) )
!= unit )
| ~ sk19 ),
inference(simp,[status(thm)],[667]) ).
thf(15171,plain,
$false,
inference(e,[status(thm)],[249,120,443,773,45,772,113,636,613,696,607,500,715,698,719,702,638,93,766,61,692,774,89,60,678,529,28,70,92,467,686,679,721,605,609,91,675,680,648,112,617,553,525,712,557,690,63,673,441,114,23,30,51,775,676]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.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/5.41 % Computer : n002.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Fri Sep 25 23:53:10 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.18/5.71 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.18/5.95 % [INFO] Parsing done (239ms).
% 0.18/5.96 % [INFO] Running in sequential loop mode.
% 2.25/6.16 % [INFO] eprover registered as external prover.
% 2.25/6.16 % [INFO] Scanning for conjecture ...
% 2.42/6.29 % [INFO] Found a conjecture (or negated_conjecture) and 20 axioms. Running axiom selection ...
% 2.74/6.37 % [INFO] Axiom selection finished. Selected 20 axioms (removed 0 axioms).
% 3.54/6.56 % [INFO] Problem is typed first-order (TPTP TFF).
% 3.54/6.57 % [INFO] Type checking passed.
% 3.54/6.58 % [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 ...
% 41.00/13.18 % External prover 'e' found a proof!
% 41.00/13.18 % [INFO] Killing All external provers ...
% 41.00/13.19 % Time passed: 7687ms (effective reasoning time: 7226ms)
% 41.00/13.19 % 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)>
% 41.00/13.19 % Axioms used in derivation (20): ax9, ax6, op_substitution_2, ax8, ax10, ax11, ax2, $ki_exists_in_world_$i_const, transitivity, inv_substitution_1, symmetry, $ki_exists_in_world_$i_nonempty, ax4, op_substitution_1, ax1, ax7, reflexivity, mrel_universal, ax3, ax5
% 41.00/13.19 % No. of inferences in proof: 149
% 41.00/13.19 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 7687 ms resp. 7226 ms w/o parsing
% 36.99/13.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 36.99/13.44 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------